Skip to content

fix(rivet): un-red main's R4 — RQ-61-VCLOSURE's landed: named the ISSUE, not the PR - #1118

Merged
avrabe merged 1 commit into
mainfrom
fix/vclosure-r4-landed
Sep 1, 2026
Merged

fix(rivet): un-red main's R4 — RQ-61-VCLOSURE's landed: named the ISSUE, not the PR#1118
avrabe merged 1 commit into
mainfrom
fix/vclosure-r4-landed

Conversation

@avrabe

@avrabe avrabe commented Sep 1, 2026

Copy link
Copy Markdown
Contributor

main is red on R4

#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.
R4 then requires the commit's PR number in fields.landed. The field said:

landed: "#1091 increment 1 (asserting floor) + v0.60 backfill pilot"

#1091 is the issue. R4 matches on the PR, so main reddened the moment
the merge landed:

FAIL R4 RQ-61-VCLOSURE: delivery commit on main (RQ-61-VCLOSURE (#1091) / PR #1115)
but status is `proposed` and `landed:` does not acknowledge it

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 issue
number 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 proposed

That is precisely what R4's landed: escape hatch is for — increment landed,
stated outcome does not yet hold:

  • landed: the coverage step now asserts (V-closure floor, red-first proven
    at 62-vs-61); the v0.60 backfill moved covered 61 → 69.
  • not yet: v0.61's own artifacts still need verifies links, and the 52
    pre-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/54

Refs #1091

@avrabe @claude
fix(rivet): un-red main's R4 — RQ-61-VCLOSURE's landed: named the I…
4cdc65c 
…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

codecov Bot commented Sep 1, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

@avrabe
avrabe merged commit 0cb36bc into main Sep 1, 2026
59 checks passed
@avrabe
avrabe deleted the fix/vclosure-r4-landed branch September 1, 2026 20:03
@avrabe avrabe mentioned this pull request Sep 1, 2026
Merged
avrabe added a commit that referenced this pull request Sep 1, 2026
@avrabe @claude
RQ-61-EXTRACT (#1080): ledger — record the increment in fields.landed…
da252fb 
… (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
@avrabe @claude
chore(rivet): record RQ-61-MVORACLE's delivery PR in fields.landed
09f76ad 
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
@avrabe @claude
RQ-61-EXTRACT (#1080): delete 98 stale extraction snapshot files + th…
a5c75ca 
…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
@avrabe @claude
chore(rivet): record RQ-61-MVORACLE's delivery PR in fields.landed
5b1e7b6 
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
@avrabe @claude
RQ-61-MVORACLE (#1097): promote the #1093-class silent-miscompile dif…
465f23a 
…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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@avrabe