Skip to content

RQ-61-DANGLE (#1102): a retained function relocating against a DECLINED function refuses loudly on every backend - #1104

Merged
avrabe merged 2 commits into
mainfrom
fix/dangling-declined-callee-1102
Aug 28, 2026
Merged

avrabe merged 2 commits into
mainfrom
fix/dangling-declined-callee-1102

Conversation

@avrabe

@avrabe avrabe commented Aug 28, 2026

Copy link
Copy Markdown
Contributor

RQ-61-DANGLE (#1102) — an unlinkable object shipped with exit 0

A retained function calling a function this compile declined shipped an object with exit 0 that could never link — the undefined symbol names a function the module itself defines, so no linker input can resolve it. #952 keys on declined requested exports; #1013 lives only in the aarch64 ELF builder. An internal decline referenced by a retained export slipped past both.

The fix: one backend-agnostic driver gate

In compile_all_exports, after the #952 export gate and before any ELF builder runs: a retained function's relocation whose symbol is a skipped function's index label (func_{idx} on ARM/A32/aarch64, synth_func_{idx} on RV32 — direct calls are always index-labelled) bails with a #1102 error naming every dangling caller→callee edge. No object is written.

Why the driver, not the ELF builders: the two facts already meet there — the driver owns skipped_funcs (now carrying wasm indices) and compiled_funcs[].relocations for all four backends, whose ELF paths are three separate crates (rv32 in main.rs, ARM in synth-backend, aarch64 in its own crate; only aarch64's had a symbol-placement view). One gate, one message, all backends; aarch64's builder Err (#851) stays as defense-in-depth for un-placed symbols that are not skip-related.

--allow-skipped-exports does NOT waive it (pinned by a test): that flag accepts a partial object (a requested export absent — the corpus-sweep shape), which is categorically different from an unlinkable one. aarch64's #1013 refusal was already unconditional; this is the same policy applied where it was missing. No stub, no trap body, no dropped call — both would turn an unlinkable object into a wrong one.

ARM characterised — same defect, and the probe that settled it

arm-none-eabi-readelf -sW -r on the unfixed binary, module every backend declines (#1093 block-type):

leg before after
rv32 --relocatable exit 0, synth_func_0 GLOBAL UNDEF, ld.lld refuses exit 1, #1102
ARM Thumb-2 --relocatable exit 0, func_0 GLOBAL UNDEF + retained R_ARM_THM_CALL exit 1, #1102
ARM Thumb-2 default exit 0, silently flips to ET_REL with the same dangle exit 1, #1102
A32 cortex-r5 exit 0, same shape as Thumb-2 exit 1, #1102
aarch64 exit 1 (#1013 builder guard) exit 1 (driver #1102, builder guard retained)

The "ARM relocatable objects have no .symtab" report was a probe artifact: the ARM builder emits its symtab section with an empty name string, so a probe by section NAME misses what a probe by section TYPE (readelf -sW) finds. ARM was not fine; it was the same defect.

Red-first, both directions

Loud: baseline exits 0 on the minimal module, gale's multi-export shape (both callers named in the refusal), and the ARM/A32 f64-helper shape; fixed binary exits 1 on all, leaves no partial object. New dangling_declined_callee_1102.rs: 8 tests — four backend legs, flag-no-waiver, two negative controls.

Silent (the one that matters more): 835 (fixture,leg) pairs — scripts/repro/*.wat + in-tree .wasm × 5 legs — baseline vs fixed binary:

identical bytes:        666
fail identically:       166
DIFFERING BYTES:          0
newly-declined (#1102):   3   (all rv32)

Each of the 3 newly-declined pairs (aarch64_f32_unsupported_554, popcnt_r11_clobber_1021, recursive_shadow_stack — rv32 leg only) was proven unlinkable before the change: the baseline object carries an UNDEF synth_func_N for a module-defined function. No CI job compiles any of the three on rv32 (the popcnt differential is Thumb-2-only, the shadow-stack fixture is consumed by scry analysis, the f32 fixture by an aarch64 test).

Deliberate test fallout

  • a64_dangling_reloc_decline_1013.rs: the refusal now fires at the driver, so the message assertion moved to #1102; the exit-1/no-panic/no-object contract is unchanged, and the header documents that seeing #851 again means the driver gate was removed — a real signal.
  • skipped_export_exit_952.rs: its "helper-only skips stay exit 0" negative control was, measured, this defect — the fixture's retained f carried a dangling func_1 GLOBAL UNDEF. Restated: a decline that leaves no dangling reference (full cascade + --allow-skipped-exports) stays exit 0 with the object emitted; the old fixture is now a RED case in the new test file.

Honest residual

The gate matches direct-call index labels only. A declined function referenced solely from a funcref table entry (call_indirect elem segment) is outside this gate and keeps its pre-existing behaviour — same class, different reference kind, left for its own increment rather than widened here without a repro.

Gates

cargo fmt --check / clippy --workspace --all-targets -D warnings / cargo test --workspace (156 suites green, incl. the three touched test files) / claim_check 52/52 / status_evidence 0 failures. BRANCH_POPULATION untouched (main.rs is not on the MC/DC scored surface). Local rivet validate (0.32.0, newer than the CI pin): 40 errors with and without this change — pre-existing version drift, none mine. Status record RQ-61-DANGLE → implemented with verified-by, riding on this branch (R4 first-parent rule).

Refs #1102.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

avrabe and others added 2 commits August 28, 2026 05:42
…ED function refuses loudly on every backend

A retained function calling a function this compile declined shipped an
object with exit 0 that could NEVER link: the undefined symbol names a
function the module itself DEFINES, so no linker input can resolve it
(measured: `ld.lld: undefined symbol: synth_func_0` on the minimal rv32
repro and on gale's multi-export gpio shape). #952 keys on declined
REQUESTED EXPORTS and #1013 lives only in the aarch64 ELF builder — an
INTERNAL decline referenced by a retained export slipped past both.

ARM CHARACTERISED, NOT ASSUMED FINE: `arm-none-eabi-readelf -sW -r` on
the unfixed binary shows ARM Thumb-2 AND A32 relocatable objects carrying
`func_N` as a GLOBAL SHN_UNDEF with the R_ARM_THM_CALL retained, exit 0 —
the SAME defect. The "ARM has no .symtab" report was a probe artifact:
the ARM builder emits the symtab section with an EMPTY name string, so a
probe by section NAME misses what a probe by section TYPE finds. Without
--relocatable the dangling reloc even counted as an external reference
and silently flipped the output to ET_REL.

THE FIX: one backend-agnostic gate in `compile_all_exports`, after the
#952 export gate and before any ELF builder runs — the driver is the one
site where the two facts already meet (`skipped_funcs`, now carrying wasm
indices, and `compiled_funcs[].relocations`), where the four backends'
ELF paths are three separate crates. A retained relocation whose symbol
is a skipped function's index label (`func_{idx}` from the ARM/A32/
aarch64 selectors, `synth_func_{idx}` from RV32 — direct calls are always
index-labelled) bails with an error naming EVERY dangling caller->callee
edge. No object is written.

Deliberately NOT waived by --allow-skipped-exports: that flag accepts a
PARTIAL object (a requested export absent, the corpus-sweep shape), not
an UNLINKABLE one — and aarch64's #1013 refusal was already
unconditional; this is the same policy applied where it was missing.
Deliberately NOT a stub/trap body and NOT a dropped call: both would
turn an unlinkable object into a WRONG one.

Fallout, each deliberate:
- a64_dangling_reloc_decline_1013.rs: the refusal now fires at the
  driver, so the asserted message is #1102's; the builder's #851 Err
  stays as defense-in-depth. Exit-1/no-panic/no-object contract
  unchanged.
- skipped_export_exit_952.rs: its "helper-only skips stay exit 0"
  negative control was, measured, THIS defect — the fixture's retained
  `f` carried a dangling `func_1` (GLOBAL UNDEF). Restated: a decline
  that leaves NO dangling reference stays exit 0 (new cascade fixture,
  under --allow-skipped-exports); the old fixture is now a RED case in
  dangling_declined_callee_1102.rs.

Red-first both directions:
- Loud: baseline exits 0 on the minimal module, the multi-export shape,
  ARM/A32 f64-helper shape; fixed binary exits 1 naming the class and
  every edge, leaves no partial object (8 tests, all four backend legs +
  flag-no-waiver + two negative controls).
- Silent: 835 (fixture,leg) pairs — scripts/repro/*.wat + in-tree .wasm
  x 5 legs (arm-m3-reloc, a32-r5-reloc, rv32-reloc, aarch64-reloc,
  arm-m4f-image) — baseline vs fixed: 666 byte-identical, 166
  fail-identically, 0 DIFFERING, 3 rv32 pairs newly-declined
  (aarch64_f32_unsupported_554, popcnt_r11_clobber_1021,
  recursive_shadow_stack), each PROVEN unlinkable-before by an UNDEF
  `synth_func_N` in the baseline object; no CI job compiles any of the
  three on rv32.

HONEST RESIDUAL: the gate matches direct-call index labels only — a
declined function referenced solely from a funcref TABLE entry
(call_indirect) is outside this gate and keeps its pre-existing
behaviour.

Refs #1102, refs #952, refs #1013.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… the #952 negative control was shipping it

The status flip rides ON THIS BRANCH (R4 is first-parent-evaluated: an
id-naming delivery commit with no acknowledgement reddens main the moment
it merges). `verified-by` records the probe that settled the ARM open
question — the baseline's ARM/A32 objects carry the dangling GLOBAL
SHN_UNDEF `func_N` (the 'no .symtab' report was a probe-by-section-NAME
artifact; the ARM builder names its symtab section with an empty string),
the 835-pair / 0-differing byte-identity sweep, the 3 rv32 pairs
newly-declined and proven unlinkable-before, and the honest residual
(funcref-table references to a declined function are outside the gate).

Gate after this commit: status-evidence 0 failures, claim_check 52/52.

Refs #1102.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
@codecov

codecov Bot commented Aug 28, 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 1d9188b into main Aug 28, 2026
62 of 63 checks passed
@avrabe
avrabe deleted the fix/dangling-declined-callee-1102 branch August 28, 2026 04:19
avrabe added a commit that referenced this pull request Sep 1, 2026
…alf (13 -> 14)

Found while repairing the aarch64 import-dispatch oracle in this same PR. An
`emulations` floor counts only emulator entries; a decline probe runs a compile
that fails and therefore emulates nothing, so it contributes ZERO to the
counter its own oracle is floored on. Four oracles have that shape — one fixed
here, three still open:

  aarch64_import_dispatch_1017_differential.py   >= 6    fixed in this PR
  multi_segment_static_data_differential.py      >= 27   open
  riscv_extern_call_871_differential.py          >= 20   open
  rv32_label_882_differential.py                 >= 15   open

The count matters less than how it was found: not by audit, but because #1104
happened to trip a WORDING pin. Had it deleted the probe instead, the floor
would still have been met and nothing would have reddened. The failure mode of
the remaining three is silence.

Same family as #1085 (evidence that cannot fail) and #1091 (a gate that prints
instead of asserting) — the check exists, is wired, and is pinned, and the pin
cannot see half of what the check asserts.

ARTIFACT_FLOOR 486 -> 487.

Refs #1113

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
…acle pinned to the superseded wording (#1112)

* fix(oracle): #1104 shadowed the aarch64 builder guard and left its oracle pinned to the superseded wording

main has been red since 1d9188b (#1104, RQ-61-DANGLE) on the non-required
`aarch64 backend execution + decline oracle` job. Measured against the
baseline: green at 23a0b54, red at 1d9188b and every commit since — the two
dependabot merges on top are innocent.

NOT a behavioural regression. The compiler still refuses this class correctly
(exit 1, names the dangling symbol, writes no object). What changed is WHICH
guard refuses: #1104 added a driver-level pre-flight that fires before the
aarch64 ELF builder's #851/#1013 refusal ever runs. The oracle's
decline-honesty probe asserted the phrase `does not place` — the builder's
wording — which that fixture can no longer reach. #1104 updated the Rust
integration test (a64_dangling_reloc_decline_1013.rs now asserts `#1102`) and
missed the Python oracle.

The deeper guard did NOT lose coverage: `dangling_reloc_symbol_is_err_not_panic`
in synth-backend-aarch64 calls `build_relocatable_object` directly, bypassing
the driver, so the driver guard cannot shadow it.

Rather than swapping one wording for another that will drift again, the probe
now asserts the durable contract:
  * exit != 0
  * no panic (a clean refusal, not exit 101)
  * the dangling symbol is named
  * NO OBJECT IS WRITTEN — the actual #1102 safety property, and the only
    assertion that is wording-free
  * the refusal comes from a KNOWN guard of this class (#1102 driver OR
    #851/#1013 builder), so an unrelated failure cannot pass as a refusal

Potency proven, not assumed: run against a module whose callee does NOT
decline (br_table under the threshold), three independent assertions fire —
exit-0, wrong-class, and "an object was written despite the refusal (736
bytes)".

Second finding, fixed here: the `# ci-checks: emulations >= 6` floor counts
ONLY the six wasmtime/unicorn differentials. It cannot see the decline half,
which emulates nothing — so deleting or neutering the decline probe would
still report `measured=6 floor=6` and the job would go green. That half now
carries its own non-vacuity floor (`refusals: N`, VACUOUS on zero), mirrored
by a grep in ci.yml. Only one `ci-checks:` header is permitted per oracle and
`emulations >= 6` is the stronger of the two, so the second floor lives in the
script and the workflow rather than replacing the header.

Also verified while here, against the compiler rather than the comment: the
#1102 guard's completeness claim ("direct-call relocations are always
index-labelled, never export-named") holds for the case that would break it —
a declined callee that IS exported, compiled with --allow-skipped-exports so
the #952 guard is waived. riscv still refuses via #1102 and writes no object.

Refs #1102

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* plan(v0.61): scope #1113 — an oracle's floor cannot see its decline half (13 -> 14)

Found while repairing the aarch64 import-dispatch oracle in this same PR. An
`emulations` floor counts only emulator entries; a decline probe runs a compile
that fails and therefore emulates nothing, so it contributes ZERO to the
counter its own oracle is floored on. Four oracles have that shape — one fixed
here, three still open:

  aarch64_import_dispatch_1017_differential.py   >= 6    fixed in this PR
  multi_segment_static_data_differential.py      >= 27   open
  riscv_extern_call_871_differential.py          >= 20   open
  rv32_label_882_differential.py                 >= 15   open

The count matters less than how it was found: not by audit, but because #1104
happened to trip a WORDING pin. Had it deleted the probe instead, the floor
would still have been met and nothing would have reddened. The failure mode of
the remaining three is silence.

Same family as #1085 (evidence that cannot fail) and #1091 (a gate that prints
instead of asserting) — the check exists, is wired, and is pinned, and the pin
cannot see half of what the check asserts.

ARTIFACT_FLOOR 486 -> 487.

Refs #1113

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* fix(oracle): sweep the CLASS — the second floor-blind oracle, and the count corrected 4 -> 2

Finishing #1113 in the PR that found it rather than leaving three instances as
a backlog entry. The v0.56.2 lesson applies: three releases ran instance fixes
on the sentinel/value-0 collision before someone swept the class.

THE COUNT WAS WRONG AND THE ERROR IS THE USEFUL PART. I derived "4 oracles" by
regex — a `# ci-checks: emulations >= N` header plus an `if <proc>.returncode
== 0:` failure branch. Reading the four sites reduced it to two:
`riscv_extern_call_871_differential.py` and `rv32_label_882_differential.py`
match because their `returncode == 0` branch is a TOOLCHAIN PROBE ("does this
clang accept rv32imac?"), not a decline assertion. A grep is a hypothesis; the
code is the oracle. Issue #1113 and the artifact are corrected rather than
quietly restated.

The real class, both fixed now:

  aarch64_import_dispatch_1017_differential.py  >= 6   (previous commit)
  multi_segment_static_data_differential.py     >= 27  (here — the #1041
                                                        red-first refusal)

`assert_relocatable_refuses_dataseg` now returns a count, `main` floors it
(`refusals: N`, VACUOUS on zero), and ci.yml greps it. While there, the same
two durable assertions the aarch64 probe gained: the refusal must not PANIC
(exit 101 reads as a synth bug, not a decline), and it must write NO OBJECT —
wording-free, and the actual fail-closed property.

Potency proven, not assumed. Simulating the probe's deletion (`refusals = 0`):

    VACUOUS: refusals=0 — the #1041 refusal half asserted nothing
    EXIT=1

Before this change that same deletion left `measured=27 floor=27` and the
oracle printed ORACLE: PASS.

Refs #1113

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* plan(v0.61): RQ-61-EXTRACT — the scope is 61 files across FOUR directories, and the copies disagree with each other

Measured while #1112's CI ran, following #1080's own verification note: the
build files are the oracle, so I checked every workflow, *.bazel, Makefile and
script rather than one grep.

The artifact recorded 19 snapshots in coq/. It is 61 .ml files across four
directories, two of which are dune build units:

  coq/          19 .ml
  extracted/    18 .ml + .mli   a dune LIBRARY, `synth_extracted`
  validation/   23 .ml          THREE dune executables
  compiler/      1 .ml

They are not one artifact with a staleness problem — they are mutually
inconsistent. coq/ and extracted/ share 18 basenames and DIFFER on 8. Not
drift, different eras: Compilation.ml is 316 lines in coq/ and 72 in
extracted/, 258 differing lines.

And NOTHING RUNS DUNE — not in any workflow, *.bazel, Makefile or script. So
extracted/ is a library nothing links and validation/ is three executables
nothing executes. That weakens the "regenerate and gate" disposition: there is
no consumer to keep them correct for.

Also recorded, because it is how this survived: VALIDATION_STATUS.md opens with
"this infrastructure has not been implemented ... does not exist" and its body
then says "Successfully implemented", "40 files total", and marks sections
"Complete and ready for use" with green checks. A disclaimer the body
contradicts is not a correction; it is two claims, and the louder one wins.

done-when now also requires `bazel test //coq:verify_proofs` to pass after the
change — deleting the .ml outputs must not disturb the .v extraction target
that produces them, and that needs proving rather than assuming.

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
… subjects (14 -> 15)

Found while flipping the two artifacts in the previous commit: the reason
nothing caught them is itself a gate blind spot, so it gets an artifact rather
than a footnote.

R4 anchors on the subject PREFIX. Lane PRs name their artifact first and are
seen; conventional-commit subjects are not:

  RQ-61-A32RELOC    #1116  "fix(#1040): A32 BL sites carry ..."    unseen
  RQ-61-ORACLEFLOOR #1112  "fix(oracle): #1104 shadowed the ..."   unseen

Both shipped complete while status_evidence_check reported 0 failures.

The artifact records what the fix must NOT break, so it is not re-litigated:
the prefix anchor is what stops a passing cross-reference from reading as a
delivery claim, and R4 must stay first-parent so a merged branch's internal
commits do not each count as a delivery. Resolving through `fields.issue` is
the only option that would have caught both instances, and it needs a marker
discipline to avoid false positives on reverts and partial fixes.

RED-FIRST IS FREE and required: b4860e4 and eefa19e are an already-measured
regression corpus, and a fix that does not flag both has not fixed the
reported thing. The done-when says so, and also requires the negative
direction — it must NOT fire on a subject that merely cross-references an id.

ARTIFACT_FLOOR 495 -> 496, re-derived with `rivet list`, not computed.

Refs #1119

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
…d — their work shipped in #1116 and #1112 (#1120)

* chore(rivet): flip RQ-61-A32RELOC and RQ-61-ORACLEFLOOR to implemented — their work shipped in #1116 and #1112

Both artifacts' `done-when` conditions are fully met by merged code, and both
still read `proposed`. Caught by reading the release status, NOT by a gate.

WHY NO GATE CAUGHT IT, which is the more interesting half. R4 fires on a
first-parent commit whose SUBJECT STARTS WITH a known artifact id. Every lane
PR in this release names its artifact first ("RQ-61-VCLOSURE (#1091): ..."), so
R4 sees them. My own two commits used conventional-commit prefixes —
"fix(oracle): ..." and "fix(#1040): ..." — so the subjects never matched, the
artifacts stayed `proposed`, and status_evidence_check reported 0 failures the
whole time. The gate is not wrong; it is blind to a delivery-commit shape that
this repo also uses, and the blindness is silent in the direction that matters
(work landed, artifact says nothing).

This is the v0.59 "orphaned status flips" class recurring, and the same family
as everything else in v0.61: a check that exists, is wired, and cannot see part
of what it is for. Filed separately rather than fixed here.

RQ-61-A32RELOC (#1040, PR #1116): A32 BL sites emit R_ARM_CALL (28), Thumb
sites keep type 10, the #1021 harness's execution-mode workaround is removed —
all three clauses. `verified-by` records the unfiled SECOND defect (the
`eb000000` vs `ebfffffe` addend) and the real-linker evidence that the pre-fix
object linked to `eaca0000` with the opcode corrupted from BL to B.

RQ-61-ORACLEFLOOR (#1113, PR #1112): both oracles print `refusals: N`, return
non-zero at zero, and ci.yml greps it; each proven red-first. `landed` records
that the published count was corrected 4 -> 2 because two matches were
toolchain probes, not decline assertions.

status_evidence_check: 0 failures. claim_check: 54/54.

Refs #1040, #1113

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* plan(v0.61): scope #1119 — R4 cannot see conventional-commit delivery subjects (14 -> 15)

Found while flipping the two artifacts in the previous commit: the reason
nothing caught them is itself a gate blind spot, so it gets an artifact rather
than a footnote.

R4 anchors on the subject PREFIX. Lane PRs name their artifact first and are
seen; conventional-commit subjects are not:

  RQ-61-A32RELOC    #1116  "fix(#1040): A32 BL sites carry ..."    unseen
  RQ-61-ORACLEFLOOR #1112  "fix(oracle): #1104 shadowed the ..."   unseen

Both shipped complete while status_evidence_check reported 0 failures.

The artifact records what the fix must NOT break, so it is not re-litigated:
the prefix anchor is what stops a passing cross-reference from reading as a
delivery claim, and R4 must stay first-parent so a merged branch's internal
commits do not each count as a delivery. Resolving through `fields.issue` is
the only option that would have caught both instances, and it needs a marker
discipline to avoid false positives on reverts and partial fixes.

RED-FIRST IS FREE and required: b4860e4 and eefa19e are an already-measured
regression corpus, and a fix that does not flag both has not fixed the
reported thing. The done-when says so, and also requires the negative
direction — it must NOT fire on a subject that merely cross-references an id.

ARTIFACT_FLOOR 495 -> 496, re-derived with `rivet list`, not computed.

Refs #1119

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
…tion floor — red-first on b4860e4/eefa19ef (+ RQ-61-EXTRACT flip) (#1124)

* RQ-61-R4BLIND (#1119): R4-issue scope resolution + R10 window attribution floor — red-first on b4860e4 and eefa19e

R4 only saw delivery commits whose subject STARTS with an artifact id, so
two v0.61 artifacts shipped via conventional-commit subjects and stayed
proposed with the gate green (#1119). Two rules, because the measured
corpus refutes half of option 2 as filed:

- R4-issue: a conventional-commit subject whose SCOPE names a
  fields.issue (fix(#1040): ...) resolves to that issue's highest-release
  holder and gets R4's acknowledgment demand. Scope-position ONLY — the
  description position is measured to name a CAUSE (eefa19e's #1104 is
  the PR that introduced the defect; resolving it would misattribute).
  Windowed to commits since the previous minor's tag, because
  fix(#1085) (#1090) is v0.60-era work on the issue RQ-61-EVIDENCE now
  holds — frozen history must not match the current issue map.

- R10: eefa19e names neither its artifact nor its issue, so NO resolver
  can attribute it — but its silence can be NOTICED. Every delivery-typed
  (feat/fix/perf/proof/test) first-parent commit in the release window
  must be attributable to SOME artifact: a known id anywhere in the
  subject, a known issue anywhere, or its PR in any landed:/verified-by:.
  The red forces exactly the landed: line #1120 wrote by hand.

RED-FIRST at 331bbd8 (last pre-flip commit, old gate 0 failures): the
fixed gate reports exactly 2 failures — R4 RQ-61-A32RELOC (fix(#1040) /
PR #1116) and R10 on 'fix(oracle): #1104 shadowed ...' (#1112) — and 0 on
main after the flip. Negative direction: 0cb36bc (fix(rivet): ...
RQ-61-VCLOSURE's ...) stays green — a mention is attribution, never a
delivery claim; Revert / description-position / ambiguous-issue shapes
all green (R4BlindSpot1119, 9 tests, mutation-verified: neutering
SCOPE_ISSUE or DELIVERY_TYPES each kills tests). ci.yml greps the new
status-evidence-window line so an underivable window is a CI red, not a
quiet skip.

Refs #1119

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* chore(rivet): flip RQ-61-EXTRACT to implemented — #1121's delivery re-verified clause by clause on main

All three done-when clauses verified independently rather than from the
PR body: the 98 snapshot .ml/.mli files across coq/, extracted/,
validation/, compiler/ are gone from the tree (delivery diff deletes
exactly 98); VALIDATION_STATUS.md is rewritten and no longer contradicts
its own header (the 'Successfully implemented' / 'Complete and ready'
body claims grep to nothing); the .v extraction target is untouched and
CI's 'Bazel Build & Proofs' passed on PR #1121, with main green at the
merge.

Note for #1119: a5c75ca was never in the R4 blind class — its subject
is id-first and its landed: names PR #1121, so old and fixed R4 both see
and accept it.

Refs #1080, #1121

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant