fix(rivet): un-red main's R4 — RQ-61-VCLOSURE's landed: named the ISSUE, not the PR - #1118
Merged
Conversation
…SSUE, not the PR #1115's squash merge put a delivery commit on main whose subject starts with RQ-61-VCLOSURE while the artifact's status is (correctly) still `proposed`, so R4 requires the commit's PR NUMBER in `fields.landed`. The field said "#1091 increment 1 ..." — #1091 is the ISSUE. R4 matches on the PR, so main went red the moment the merge landed. This is the second time this release: I merged #1101 with the same shape and had to un-red main in #1103. The pattern is that the PR number does not exist when the lane writes `landed:`, so an issue number goes in as a plausible stand-in and nothing catches it until the squash commit exists. Recorded here rather than just fixed, because the fix is one line and the trap is not. The status stays `proposed` DELIBERATELY, which is the whole point of the R4 `landed:` escape hatch — increment 1 landed (the coverage step asserts, red-first at 62-vs-61; the v0.60 backfill moved covered 61 -> 69), but the stated outcome also needs v0.61's own artifacts to carry `verifies` links, and the 52 pre-v0.60 artifacts are still undecided (the lane measured them as archaeology rather than transcription and recommended exempting them). The field now says exactly that, so a reader learns what did and did not land instead of just seeing a number. status_evidence_check: 0 failures. claim_check: 54/54. Refs #1091 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
avrabe
added a commit
that referenced
this pull request
Sep 1, 2026
… (PR #1121) Status stays proposed for the release status pass; landed: is the R4 machine-readable acknowledgment (the #1118 convention — PR number, not issue number). Refs #1080 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Sep 1, 2026
The PR number (#1122), not the issue number — the RQ-61-VCLOSURE confusion (#1118) applied preemptively. Refs #1097 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Sep 1, 2026
…e dune tree nothing runs; docs stop contradicting their own headers (#1121) * RQ-61-EXTRACT (#1080): delete the 98 stale extraction snapshot files and the dune tree nothing runs CI re-runs extraction from Synth/Extraction/CompilerExtract.v into the Bazel sandbox on every run and never reads these committed copies, which had drifted for up to nine months (coq/WasmInstructions.ml predates BrIf) and disagree with each other across directories (coq/Compilation.ml 316 lines vs extracted/Compilation.ml 72). Deleted (98 snapshot files = 61 .ml + 37 .mli, plus the dune plumbing): - coq/*.ml + coq/*.mli (19 + 19 — the .mli siblings were not in the issue's census; same class, same fate) - extracted/ (18 .ml + 18 .mli + dune — a library nothing links) - validation/ (23 .ml + dune + dune-project + poc_validator.md + README.md + test_cases/simple_add.wat — three executables nothing executes; the renode tests use //examples/wat:simple_add.wat, not this copy) - compiler/ (synth_compile.ml + dune) - dune-project (root; dune appears in no workflow, bazel file, Makefile or script) - BUILD.bazel //:test_data (filegroup globbing only validation/**/*.wat — zero consumers, and an empty glob is an error under Bazel 8) The .v extraction target (coq/BUILD.bazel rocq_library "extraction") is untouched; bazel test //coq:verify_proofs still exercises it. Refs #1080 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * RQ-61-EXTRACT (#1080): docs stop arguing with their own headers - docs/validation/VALIDATION_STATUS.md: BODY REWRITTEN. It opened with 'has not been implemented ... do not exist' and then said 'Successfully implemented', '40 files total, ~80KB', 'Status: Complete and ready for use'. Two claims, and the louder one wins. It now describes only what exists: extraction as the CI Bazel target, and the validation machinery that actually ships (proof suite, synth-verify, differential oracles). - docs/validation/COMPREHENSIVE_VALIDATION_REPORT.md: historical-record header — it reports a real 2025-11 run of executables #1080 removed; the reproduce commands no longer apply. - docs/build-systems/COQ_DUNE_SETUP_GUIDE.md: 'NOT adopted' header — the project built proofs under Bazel/rules_rocq, the opposite of this guide's recommendation, and the dune tree its plan produced is gone. - examples/pid-controller/COMPILER_DEMO.md: historical-demo header — the synth_compile.exe driver it builds was removed in #1080. validation/poc_validator.md and validation/README.md were deleted with their directory in the previous commit. Refs #1080 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * RQ-61-EXTRACT (#1080): ledger — record the increment in fields.landed (PR #1121) Status stays proposed for the release status pass; landed: is the R4 machine-readable acknowledgment (the #1118 convention — PR number, not issue number). Refs #1080 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Sep 1, 2026
The PR number (#1122), not the issue number — the RQ-61-VCLOSURE confusion (#1118) applied preemptively. Refs #1097 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Sep 1, 2026
…ferential into a CI-wired red-first oracle (#1122) * RQ-61-MVORACLE (#1097): the silent-miscompile evidence behind the #1093 decline, promoted into a CI-wired red-first oracle The #1096 guard survived; its justification lived in a lane scratchpad. This commits the demonstration: the PRE-#1096 compiler's own emitted objects (fixture rev b2abf95 = c4b463f^, regenerable via --capture) are re-executed under unicorn against wasmtime-first values on every CI run. Demonstrated SILENT-WRONG (exit 0, wrong value), pinned exactly: if/ARM ipe(0) -> 0xC0DE0003 (uninitialized-R3 canary), want 7 if/RV32 ipe(0) -> uninitialized-T2 canary, want 7 block/RV32 bpb(1) -> uninitialized-T2 canary (dropped br_if param), want 7 loop/RV32 lpb(3) -> 2 (mis-reconciled back-edge join), want 10 Negative results pinned as such, not manufactured: block/ARM was CORRECT pre-#1096 on all 7 probed vectors (that leg's decline is conservative); loop/ARM was already refused by the #509 back-edge decline (the fixture records that refusal, needle-checked). Green half: all six shape x backend legs decline cleanly on main (exit 1, not 101, no "panicked at", no object written, the shared #1093 needle), and a guard module of supported neighbours (plain `if (result)`, value-carrying forward br_if) still compiles and matches wasmtime on both backends — the decline covers the class, not everything. Floors: `# ci-checks: emulations >= 19` (11 fixture + 8 guard unicorn entries). That floor CANNOT see the decline half (#1113 — a refused compile emulates nothing), so the script carries refusals == 6 in-script (non-zero exit otherwise) and ci.yml greps `refusals:` plus the `silent-wrong vectors: 4 (of 4 pinned)` partition line (#1112 pattern). Red-first: pointing SYNTH at the pre-#1096 binary fails the oracle — all six legs accepted + refusals=0 VACUOUS, exit 1. Refs #1097 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * chore(rivet): record RQ-61-MVORACLE's delivery PR in fields.landed The PR number (#1122), not the issue number — the RQ-61-VCLOSURE confusion (#1118) applied preemptively. Refs #1097 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(oracle): register the three #1097 param-block fixtures as DESIGNED declines in the ARM corpus sweep The #973 sweep's EXPECTED_DECLINES is exact both ways, so the new declining fixtures reddened it on their own PR — correctly. Measured at the sweep's own flags (cortex-m4f --relocatable --all-exports): if/block/loop decline (rc=1, no object; the #1096 class, by design), guard COMPILES (rc=0) and is deliberately absent from the list — the sweep now also executes its 2 exports x 12 vectors (0 mismatches). Sweep re-run locally: 155/171 compiled, 2526 vectors, PASS, exit 0. Refs #1097 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Sep 2, 2026
….landed The placeholder could not be filled at authoring time — the PR number does not exist until `gh pr create` returns. That is exactly the sequencing trap that reddened main twice this release (#1103 after #1101, #1118 after #1115): an issue number goes in as a plausible stand-in and nothing catches it until the squash commit exists. Filled at PR-creation time, which is the first moment the number is knowable. Refs #1062 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Sep 2, 2026
…the idle rust-cpu pool (#1127) * RQ-61-CICAP (#1062) increment 2: move the required Clippy context to the idle rust-cpu pool Increment 1 retargeted ONE NON-REQUIRED job. This moves a REQUIRED context, so the reasoning is written down rather than assumed. WHY IT IS SAFE TO MOVE A REQUIRED JOB HERE: * Three jobs already run on rust-cpu, and increment 1's `synth-provenance-v1 reconciliation gate` has been green there for 5/5 consecutive main runs — the pool is proven for cargo work, not hoped at. * The job NAME is unchanged, so the required context still REPORTS. A failure would block PRs; it would not DEADLOCK them. The deadlock case is a required context that never runs (renamed, or conditionally skipped), which this is not. * Rollback is a revert, and a revert PR's own CI runs the reverted config, so the escape hatch cannot be blocked by the thing it is escaping. * Clippy is plain cargo — checkout, toolchain, cache, `cargo clippy`. No external toolchain, unlike Z3/Bazel/Kani, which the artifact deliberately holds back until their toolchains are proven on this pool. The job's own comment already said the z3-sys disk pressure that forced ubuntu-latest was gone (#553). THE CAPACITY READING BEHIND THIS IS A CORRECTION OF MY OWN. I earlier posted a point sample showing rust-cpu 7/7 busy and inferred the pool was saturated, concluding increment 2 should avoid it. Ten samples over ~9 minutes, with 2-5 runs QUEUED the entire time, show the opposite: 02:35:42 lean-mem=0/4 light=0/1 rust-cpu=2/7 queued_runs=5 ... 02:44:11 lean-mem=0/4 light=0/1 rust-cpu=0/7 queued_runs=2 All twelve self-hosted runners idle or near-idle throughout, while runs sat queued. The 7/7 was a merge-wave transient. The failure mode was reading a RATE off a single INSTANT; corrected on #1062 with the sampled window, and the original done-when stands. The structural finding is unchanged and is not sample-dependent: 56 of 65 job definitions (86.2%) target `ubuntu-latest`. The bottleneck is the GitHub-hosted quota, not the self-hosted fleet — which is the better problem, because the capacity to absorb the work already exists. Status stays `proposed`: the done-when asks for the plain-cargo required jobs, and `Test` is still on ubuntu-latest. One job per PR with its own green cycle is the artifact's own prescription and is why this is not a batch. Refs #1062 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * chore(rivet): record CICAP increment 2's delivery PR number in fields.landed The placeholder could not be filled at authoring time — the PR number does not exist until `gh pr create` returns. That is exactly the sequencing trap that reddened main twice this release (#1103 after #1101, #1118 after #1115): an issue number goes in as a plausible stand-in and nothing catches it until the squash commit exists. Filled at PR-creation time, which is the first moment the number is knowable. Refs #1062 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
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
1 participant
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.
main is red on R4
#1115's squash merge put a delivery commit on main whose subject starts withRQ-61-VCLOSUREwhile the artifact's status is (correctly) stillproposed.R4 then requires the commit's PR number in
fields.landed. The field said:#1091is the issue. R4 matches on the PR, so main reddened the momentthe merge landed:
Second time this release, and worth naming
I merged #1101 with the same shape and had to un-red main in #1103. The trap:
the PR number does not exist when the lane writes
landed:, so an issuenumber goes in as a plausible stand-in, and nothing catches it until the squash
commit exists. Not the lane's error so much as a sequencing hazard in the
workflow — recorded here because the fix is one line and the trap is not.
Status deliberately stays
proposedThat is precisely what R4's
landed:escape hatch is for — increment landed,stated outcome does not yet hold:
at 62-vs-61); the v0.60 backfill moved covered 61 → 69.
verifieslinks, and the 52pre-v0.60 artifacts are undecided — the lane measured them as archaeology
rather than transcription (they predate mandatory
done-when/verified-by)and recommended exempting them.
The field now says that in full, so a reader learns what did and did not land
rather than seeing a bare number.
Gates
status_evidence_check.py: 0 failures (was 1)claim_check.py: 54/54Refs #1091