Skip to content

test(model): check Triage's rules across event orders with the real workflows - #746

Merged
TheGreatAxios merged 8 commits into
mainfrom
cl-11739-model-check-proof
Oct 29, 2026
Merged

TheGreatAxios merged 8 commits into
mainfrom
cl-11739-model-check-proof

Conversation

@TheGreatAxios

@TheGreatAxios TheGreatAxios commented Oct 29, 2026 •

Copy link
Copy Markdown
Contributor

Triage's real listener and manager workflows now run in one test process. The test plays many orders of pull request events through them and, once each pull request settles, checks three of Triage's rules: R1, R3 and R5 in docs/INVARIANTS.md. This branch builds on #748, which moves the chain helpers.

What the test runs:

  • tests/model/ runs the real GitHub listener and manager definitions through Interchange's runLocal and the stock step invoker. They run against the hub's own intake and manager routes on a database of their own, with the chain's fake GitHub.
  • The definitions are built from the manager release, the same way the published entries build them.
  • Steps authorize through Interchange's credentials-backed authorize against the grants a deployed run holds. Those come from the definition's capability walk, its credential bindings, and the grants recorded for it at deploy. Each consumer of the hub credential gets a run token, as deploy mints them.
  • Events: open, push, CI pending, success, failure, cancelled or stale, edit, draft, ready, a mail delivered twice, and which queued mail runs next.
  • Every sequence of none to two events after the open is played and checked, 121 in all, as no sequence with an event that changes nothing is extended; plus 300 seeded random walks of ten. A failure names its sequence, and a walk's seed, so it replays. A sequence that throws, or a run that ends other than completed, fails too.

The rules checked once a pull request has settled (ready, CI finished, every mail delivered):

  • R1: exactly one current Triage comment. It is a verdict, not the in-progress comment, and it names the head. The waiting label is gone.
  • R3: across every write the pull request received, whichever pass made it, comment edits and label removals included: a Triage comment is created only while none is current (so never twice unless the one before was superseded), and no label is added while it is on.
  • R5: none of the pull request's managers is live, no live manager was deployed for no single pull request, and no mail for it was lost to a run that had ended. The deploy stand-in ties each manager to the pull request named by the mail its listener was running, so a manager the hub was never told about is still seen. Settling delivers every queued mail, so no mail is left waiting by construction and that is not checked.

Stand-ins and what they leave out (also in docs/INVARIANTS.md and docs/DEV.md):

  • Stock's deploy route records the run, its grant requirements as creator grants, and its run tokens. It checks the caller holds the deploy and the asset's read. It refuses a body that does not name a published release exactly. It does not resolve requirements against the creator's own grants.
  • Stock's stop-run route checks the caller's manage grant and ends the run at once, so the cancellation window is not played.
  • Mail waits in a queue the test delivers. Stock's mailAccept check and its mail hold on a just-deployed run are bypassed. Mail to a run that has ended is refused at send and dropped at delivery, and the hub's deliver throws RunUnavailableError for a run that is not live.
  • Webhooks enter at the hub's intake as the coalescer flushes them. The bridge and coalescer do not run, and the test plays the bridge's rule that a draft's webhooks are dropped.
  • The intake's hooks are fixed: the listener is routable, nothing is paused, the App login is fixed, and code review and backlog reads are not served.
  • Runs use the real clock. The policy is deterministic only, with no judge, no code review and no model.

Not covered yet: interleaving inside a pass (a push or a second manager while a pass runs, and contention for the claim), the cancellation window, mailAccept and the real coalescer, a fake clock, judge and review stand-ins (so R2), and every sequence of three events.

Docs: docs/INVARIANTS.md lists all ten rules from the issue, each with its check or "No automated check yet". AGENTS.md says what the model check covers and that a change to the listener, manager, workflows or contracts names the rules it touches. DEV.md and IMPLEMENTATION.md describe the test.

Verification:

  • bun run check and bun run lint pass.
  • tests/model passed on the final code: 121 sequences checked plus 300 walks, with no rule broken, in 58 s.
  • To show each rule can fail, I made one change per rule, ran the test, saw it fail, and reverted the change:
    • R1: settling without finishing CI. It reported "the Triage comment is no verdict: Triage: In progress", that the comment names no head, and that the waiting label is still on.
    • R3, comment across passes: the fake GitHub hiding existing comments, so a later pass creates a second one. It reported "a Triage comment was created while one was current".
    • R3, label across passes: the GitHub label write re-adding labels already on. It reported "Triage: Waiting for CI was added while it was on" (seeds 41, 58, 70) and "Triage: Needs Human Review was added while it was on" (seed 21).
    • R3, within a pass: the GitHub comment write posting twice. It reported "pass … posted 2 comments" (run against the earlier per-pass check, which the cross-pass check now covers).
    • R5, unnamed manager left running: the listener skipping /manager/deployed and the stop route not ending the run. It reported "managers still live: run_…" even though the hub was never told about those managers. Skipping /manager/deployed alone breaks no rule.
    • R5, a manager left running: the stop route not ending the run. It reported "managers still live".
    • R5, lost mail: ending the manager once the listener named it to the hub. It reported "mail no run took: run_…".
    • Authorization: deploying the manager without its self-run grant made its stop forbidden, so the run failed and stayed live. Deploying the listener without its deployed grant made the listener's run fail.

Part of CL-11739

@linear-code

linear-code Bot commented Oct 29, 2026 •

Copy link
Copy Markdown

CL-11739

CL-11771

CL-11680

@TheGreatAxios
TheGreatAxios force-pushed the cl-11739-model-check-proof branch from 480f108 to 805c033 Compare October 29, 2026 07:21
@TheGreatAxios
TheGreatAxios force-pushed the cl-11739-model-check-proof branch from 3db42ea to e38817f Compare October 29, 2026 08:30
@TheGreatAxios
TheGreatAxios marked this pull request as ready for review October 29, 2026 08:30
@corbits-triage

corbits-triage Bot commented Oct 29, 2026 •

Copy link
Copy Markdown
Contributor

Triage: Pass

No changes needed from you. A maintainer will review this pull request.

Notes:

  • added code matches a code pattern: tests/chain/github.ts:207 Invented fallback `?? []`; handle the missing value instead., tests/model/stack.ts:222 Invented fallback `?? []`; handle the missing value instead., tests/model/stack.ts:334 Invented fallback `?? []`; handle the missing value instead.
  • changes sensitive paths: locks: bun.lock
  • Risk: medium (locks paths, 1 recently fixed file)

Approve held: code review did not read the whole change on this head.

@corbits-triage corbits-triage Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Adds a model test that runs Triage's real GitHub listener and manager workflows through Interchange's runLocal, plays many orders of pull request events, and checks rules R1, R3 and R5 once each pull request settles. The most important defect is that deployRun keeps only the first run-token row, so every hub consumer of a run gets the same token, which overstates the authorization coverage.

This review did not read the whole change; approve and merge are held until a review does.

Comment thread tests/model/stack.ts Resolved
Comment thread tests/model/rules.postgres.test.ts Resolved

@corbits-triage corbits-triage Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Adds a model test that runs Triage's real GitHub listener and manager workflows through many orders of pull request events, then checks rules R1, R3 and R5 once each pull request settles. The main defect is that the unattributed-manager check can record managers as reported inside checks whose results are then discarded, so the R5 failure for those managers never surfaces.

This review did not read the whole change; approve and merge are held until a review does.

Comment thread tests/model/stack.ts Resolved

@corbits-triage corbits-triage Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Adds a model-check test that runs Triage's real GitHub listener and manager workflows through Interchange's runLocal against stand-ins for deploy, stop, mail delivery and GitHub. It plays every sequence of up to two events after open, plus 300 seeded random walks, then checks rules R1, R3 and R5 once each pull request settles. No findings were raised in this review.

This review did not read the whole change; approve and merge are held until a review does.

@TheGreatAxios
TheGreatAxios merged commit 131c290 into main Oct 29, 2026
18 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant