Repository navigation
queen: an issue proof may cite the newest passed commit while HEAD's CI runs - #1564
Merged
Merged
Conversation
…CI runs (Closes #1563) The Corona and Memory proof readers required the canonical push CI to be green at the default-branch HEAD itself, so every merge turned all covered cells unknown until that CI finished (47 minutes on 2026-10-08). specs/queen/proof_commit.t27 now decides how a reader walks back from HEAD: WALK[state * 2 + skippable] selects a passed commit, stops at a failed one, and skips a pending one only while it is younger than PENDING_GRACE_MS and within MAX_BEHIND of HEAD. The pinned evidence must still be the pinned bytes at HEAD as well as at the cited commit, so changed evidence stays unknown at once. The proof and its links name the cited commit, never HEAD. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
dmitrii-f-t27
enabled auto-merge (squash)
October 8, 2026 19:12
Contributor
X Brain Health CheckScore: 100.0/100 X Brain is above merge threshold |
github-actions Bot
added a commit
that referenced
this pull request
Oct 8, 2026
queen: an issue proof may cite the newest passed commit while HEAD's CI runs (Closes #1563) (#1564) The Corona and Memory proof readers required the canonical push CI to be green at the default-branch HEAD itself, so every merge turned all covered cells unknown until that CI finished (47 minutes on 2026-10-08). specs/queen/proof_commit.t27 now decides how a reader walks back from HEAD: WALK[state * 2 + skippable] selects a passed commit, stops at a failed one, and skips a pending one only while it is younger than PENDING_GRACE_MS and within MAX_BEHIND of HEAD. The pinned evidence must still be the pinned bytes at HEAD as well as at the cited commit, so changed evidence stays unknown at once. The proof and its links name the cited commit, never HEAD. Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
Contributor
🧪 Brain Stress Test ResultsTests: 261/261 passed, 0 leaked |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
Closes #1563.
Both issue-proof readers (Corona and Memory) demanded a green push CI at the default-branch HEAD itself. A merge moves HEAD to a commit whose CI has not finished, so every covered cell fell back to
unknownuntil it did: about 47 minutes after the merge of trinity-memory PR #132 on 2026-10-08 (typical CI 35 minutes), and again after every later merge. The pinned evidence was byte-identical the whole time.Spec first
apps/website/specs/queen/proof_commit.t27(modulequeen_proof_commit, sealed with t27c 0.5.1, 3/3 tests):WALK[state*2+skippable]answers continue / select / stop for each candidate commit, newest first: a commit whose canonical push CI passed is selected, a failed one stops the walk, a pending one (queued, running, absent, cancelled) is skipped only while it is younger thanPENDING_GRACE_MS(2 h) and fewer thanMAX_BEHIND(4) commits behind HEAD. An unknown commit date is not young.scripts/proof-commit-from-spec.mjsruns the spec in the vendored compiler, derives the expected table from those three rules (it does not copy it from the spec), and writessrc/lib/queenProofCommit.generated.tsandconformance/queen_proof_commit.json;--checkfails on a stale file or seal. It is part ofnpm run check:queen-issue-proof.Code
src/lib/queenIssueProof.tsonly executes the table:MAX_BEHIND+1commits read, and one run lookup per candidate (at mostMAX_BEHIND+3= 7 requests).unknownat once, with or without CI. This is the property the old reader had and it is kept.verifyGroup(..., filesOnly)for HEAD).What is not done
Not released: app.t27.ai needs a
QUEEN_REFrelease PR in 999-multibots-telegraf and an approved deployment. The page does not yet tell the reader that HEAD is ahead of the cited commit. The live check (merge a harmless commit into trinity-memory and watch a covered cell) is not run. Details and the mutation results are in the report below.{ "version": 1, "head_sha": "0c5eab1539263baad5306c4952dcd166fabc4fc6", "summary": "After every merge into a covered repository the Corona and Memory proof readers marked all covered cells unknown until the canonical push CI of the new HEAD finished (about 47 minutes on 2026-10-08), although the pinned evidence had not changed. A reader now walks back from HEAD by the WALK table of a new sealed spec and cites the newest commit whose CI passed, while HEAD's pinned evidence must still be byte-identical.", "changes": [ "apps/website/specs/queen/proof_commit.t27 (new, sealed with t27c 0.5.1): WALK[state*2+skippable], MAX_BEHIND=4, PENDING_GRACE_MS=7200000, 3 tests", "apps/website/scripts/proof-commit-from-spec.mjs (new): runs the spec, derives the expected table from three rules, writes src/lib/queenProofCommit.generated.ts and conformance/queen_proof_commit.json; --check fails on a stale file or seal", "apps/website/src/lib/queenIssueProof.ts: selectProofCommit/ciState walk the newest MAX_BEHIND+1 commits; both readers verify pinned bytes at the cited commit and at HEAD; the grouped reader reads each group's replay workflow at the cited commit and its files at HEAD (verifyGroup filesOnly)", "apps/website/qa/queen-proof-commit.mjs (new, 54 cases) and package.json: check:queen-issue-proof now also runs the generator check and the new QA" ], "tests": [ { "command": "node scripts/proof-commit-from-spec.mjs --check (apps/website)", "status": "passed", "result": "Proof commit spec: 3 tests, 8 assertions; 6 conformance rows; generated policy, vectors and seal current", "evidence": "local run, node v24.13.0, head 0c5eab15" }, { "command": "node --experimental-strip-types qa/queen-proof-commit.mjs", "status": "passed", "result": "54 cases and 6 conformance vectors PASS: HEAD green costs 2 API requests; pending HEAD cites the previous passed commit; failed HEAD or failed commit in between is unknown; age and depth bounds; every pinned file changed at HEAD or at the cited commit is unknown (single and grouped readers); a list longer than asked is not read past the bound", "evidence": "local run, node v24.13.0, head 0c5eab15" }, { "command": "node --experimental-strip-types qa/queen-issue-proof.mjs (also runs the Memory and t27 readers' QA)", "status": "passed", "result": "unchanged results: Corona 44 cases, Memory 27 groups / 33 issues / 12315 cases, t27 79 cases", "evidence": "same results on pristine main before the change" }, { "command": "mutation run: 8 WALK mutants and 9 code mutants against qa/queen-proof-commit.mjs", "status": "passed", "result": "15 of 17 killed. The 2 survivors, 'depth ignored in young' and 'loop bound widened', each remove only one of two redundant depth guards; removing both is killed by the oversize-list case", "evidence": "local run, mutants applied one at a time to queenProofCommit.generated.ts and queenIssueProof.ts, files restored, baseline PASS afterwards" }, { "command": "t27c 0.5.1 test-report specs/queen/proof_commit.t27", "status": "passed", "result": "3/3 pass, but all 3 are reported VACUOUS (0 runtime asserts): they compare module constants, as the neighbouring issue_proof_refresh.t27 and world_pages.t27 do. The asserts that run are the generator's runSpecTests (8) plus the QA.", "evidence": "local run, t27c 0.5.1 (579bc55aa), zig 0.16.0" }, { "command": "tsc --noEmit --strict (TypeScript 5.6.3) on src/lib/queenIssueProof.ts", "status": "passed", "result": "exit 0, same as pristine main; a planted type error is reported", "evidence": "local run; not the project's tsc -b (node_modules not installed in the sparse worktree), CI runs it" }, { "command": "live check: merge a harmless commit into trinity-memory and watch a covered cell during its CI window", "status": "not_run", "result": "app.t27.ai pins this repository through QUEEN_REF in 999-multibots-telegraf; nothing is released yet", "evidence": "to be done after the release PR" } ], "limitations": [ "Not released: app.t27.ai keeps the old reader until a release PR changes QUEEN_REF and the deployment is approved.", "While a window is open the proof names an older commit (its spec and CI links point there); the page does not yet say that HEAD is ahead. A failed HEAD or a pending HEAD older than 2 hours or deeper than 4 commits is still unknown.", "The age rule trusts the committer date of HEAD; a commit pushed with an old committer date is not skipped (fails closed).", "Anonymous GitHub API budget: 2 requests as before when HEAD is green; at most MAX_BEHIND+3 = 7 while a window is open.", "Per-group evidence workflows are read at the cited commit: a group whose replay is still running at HEAD but passed at the cited commit stays covered, because its files are byte-identical at HEAD.", "The t27 per-PR reader is unchanged. The native test asserts of the new spec are vacuous (see the tests above)." ], "tags": [ "Engineering", "Verification" ], "blog": { "title": "The proof map went red for 47 minutes after every merge, and the evidence had not changed", "summary": "A reader that demanded green CI on the newest commit turned CI duration into a coverage outage; it now cites the newest commit that passed, but only while the pinned bytes are identical at HEAD.", "outline": [ "A merge into trinity-memory left every covered cell unknown for 47 minutes on 2026-10-08, because the reader required a green push CI at the exact new HEAD and that CI had not finished.", "A sealed spec now holds the walk: select a passed commit, stop at a failure, skip a pending one only while it is young and near HEAD, and require the pinned files to be identical at HEAD, so changed evidence is still unknown at once.", "Measured on fixtures only: 54 cases and 15 of 17 mutants killed, the other two redundant guards. Not released and not yet seen live; the page still does not say that HEAD is ahead." ], "reproduce": [ "cd apps/website && node --experimental-strip-types qa/queen-proof-commit.mjs" ] } }Dmitrii Fedorov (@dmitrii-f-t27)