Skip to content

fix(#739): static ABOVE sp_init — relocate (never bake) + de-vacuate the in-range oracle - #744

Merged
avrabe merged 3 commits into
mainfrom
fix/739-above-sp-static
Jul 15, 2026
Merged

avrabe merged 3 commits into
mainfrom
fix/739-above-sp-static

Conversation

@avrabe

@avrabe avrabe commented Jul 14, 2026

Copy link
Copy Markdown
Contributor

Fixes #739 (VCR-MEM-001; builds on #383 shrink, #678 down-shift, #707 multi-SP co-rebase).

Root cause

The sub-word i32 load/store arms (i32.load8/16*, i32.store8/16) never got the #359 native-pointer static classification that the word-sized I32Load/I32Store arms have. A dynamic-index access with a static-region memarg offset (the wit-bindgen byte-copy shape a meld --memory shared fused node produces — statics ABOVE the shared SP at 0x10000C) fell through to the raw [R11 + addr + #offset] lowering and baked the linmem offset as a plain un-relocated immediate:

movw r12, #0xc
movt r12, #0x10      ; 0x10000C — an immediate, NOT a reloc
add.w r12, r0, r12
ldrb.w r0, [r11, r12]

The #678 --shadow-stack-size rebase walks relocations, so it never touched the baked offset → OOB on the shrunk reservation (gale's zeroed log buffer). And the post-link "all reservation accesses in-range" oracle also walks relocations → vacuously green on the miscompile (the #712-class lesson: a gate that cannot see the access class it guards is a vacuous gate). On the minimal fixture the failure is even deeper: with ZERO relocs the whole native-pointer region was dropped and --shadow-stack-size silently ignored.

Fix (red-first)

  1. Repro scripts/repro/mem739_above_sp.wat (17-page memory, SP init 0x100000, BSS static at 0x10000C + (data) static at 0x100020) shows the exact baked signature on main.
  2. Selector (instruction_selector.rs): sub-word arms now mirror I32Load/I32Store — dynamic-index static accesses relocate the base to __synth_wasm_data + offset (+ Add index); folded const addresses classify via static_data_addend first. i64 accesses (full + sub-word) with a static-region offset decline loudly (typed Err, loud-skip) — pre-fix they silently miscompiled the same way; the pair lowering doesn't yet model the relocated base (follow-up candidate).
  3. Oracle de-vacuation (main.rs): the shrink now scans the encoded Thumb-2 text for un-relocated MOVW/MOVT pairs materializing a constant in [sp_init, linear_memory_bytes) and refuses loudly (find_baked_static_movw_movt, unit-tested against the exact pre-fix byte sequence). Scope honestly documented: pairs cover every 64 KiB+ sp_init (incl. this 1 MiB geometry); the sub-64 KiB lone-MOVW window is guarded by the selector-side classification (a lone-MOVW scan would false-positive on MOVW+MVN inverted constants). Plus: --shadow-stack-size on a module with no reloc into the region now refuses instead of silently no-op'ing.
  4. Execution differential scripts/repro/static_above_sp_739_differential.py (modeled on the --native-pointer-abi + --shadow-stack-size refuses wit-bindgen buffer node: inline linmem statics not down-shifted into .data (VCR-MEM-001 layer-2) #678 oracle): store/load through the above-SP static after the shrink == wasmtime, unicorn with .bss/.data at SEPARATE bases so a baked absolute offset cannot accidentally resolve; also pins the shrink fired and every .bss reloc lands in the shrunk reservation. RED on main (exit 1), GREEN here — wired into the trap-semantics-oracle CI job.

After the fix the fixture's static relocates as __synth_wasm_data + 0x10000C, down-shifted by #678 to budget + 12 = 2060 inside the 2088-B reservation; the (data) static retargets to __synth_wasm_seg_0.

Evidence

  • Differential: main → FAIL (region dropped) exit 1; branch → ORACLE: PASS (8/8 cases vs wasmtime).
  • New tests: 4 integration (static_above_sp_739.rs), 2 selector, 4 oracle-scan unit tests — all green.
  • Regressions: static_downshift_678 / multi_sp_rebase_707 / shadow_stack_shrink_383 suites green; native_pointer_static_downshift_678.py PASS; multi_sp_707_differential.py PASS (immutable-const discriminator stays 4096); frozen anchors 10/10; workspace 2166 passed / 0 failed; cargo fmt --check + clippy -D warnings clean; claim-check 18/18.

Maintainer note: please re-run the differential before merging (SYNTH=./target/debug/synth python scripts/repro/static_above_sp_739_differential.py).

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

avrabe and others added 3 commits July 15, 2026 04:45
…ke linmem offsets

A meld --memory shared fused node places component statics ABOVE the shared
SP (17-page linmem, sp_init 0x100000, static at 0x10000C). The wit-bindgen
byte-copy shape — dynamic index + static-region memarg offset on
i32.load8/16 / i32.store8/16 — fell through to the raw [R11 + addr + #offset]
lowering and BAKED the 1 MiB linmem offset as a plain un-relocated
`movw ip,#0xC; movt ip,#0x10`: invisible to the #678 --shadow-stack-size
reloc-walking rebase -> silent OOB on the shrunk reservation (gale's zeroed
gust:os log buffer).

- sub-word i32 load/store arms get the same static classification the
  word-sized I32Load/I32Store have had since #359: dynamic-index accesses
  relocate the base to `__synth_wasm_data + offset` + Add index; folded
  const addresses classify through static_data_addend before the [R11,#imm]
  form.
- i64 accesses (full, sub-word) with a static-region memarg offset DECLINE
  loudly (typed Err, loud-skip) — the pair lowering does not yet model the
  relocated base; pre-fix they silently miscompiled the same way. Never bake.
- fixture scripts/repro/mem739_above_sp.wat reproduces the exact red
  signature (`movw r12,#0xc; movt r12,#0x10; strb/ldrb [r11, r12]`, ZERO
  relocations) on main.

Part of VCR-MEM-001; refs #739 #678 #383 #707.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…fsets, refuse silent no-ops

Two vacuity holes in the --shadow-stack-size gate (the #712-class lesson: a
gate that cannot SEE the access class it guards passed green on a live
miscompile):

1. The post-link "all reservation accesses in-range" walk covered
   RELOCATIONS only, so a BAKED un-relocated MOVW/MOVT static-region address
   (the #739 miscompile) sailed through un-rebased. The shrink now scans the
   encoded Thumb-2 text for un-relocated MOVW/MOVT pairs (same rd)
   materializing a constant in [sp_init, linear_memory_bytes) and REFUSES
   loudly (find_baked_static_movw_movt + unit tests against the exact
   pre-fix byte sequence). Pairs-only scope documented: pairs cover every
   64 KiB+ sp_init (the meld shared-memory 1 MiB geometry); the sub-64 KiB
   lone-MOVW window is guarded by the selector-side classification itself
   (a lone-MOVW scan would false-positive on MOVW+MVN inverted constants).

2. --shadow-stack-size on a module whose code carries NO
   __synth_wasm_data/__synth_globals reloc silently skipped BOTH the region
   emission and the shrink — the pre-fix #739 fixture shipped a reloc-free
   object with its 1 MiB of statics dropped and the flag ignored. Now a
   typed refusal (mem739_no_static.wat pins it).

Part of VCR-MEM-001; refs #739 #678 #383 #707.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
- scripts/repro/static_above_sp_739_differential.py: store/load through the
  above-sp_init static after the shrink == wasmtime (unicorn Thumb-2,
  R11 = 0 native deref, .bss/.data mapped at SEPARATE bases so a baked
  absolute linmem offset cannot accidentally resolve). Also pins that the
  shrink FIRED (budget-sized .bss, not the 1 MiB page) and that every
  .bss-targeting reloc lands inside the shrunk reservation. RED on main
  (exit 1: region dropped entirely), GREEN with the fix. Wired into the
  trap-semantics-oracle CI job.
- crates/synth-cli/tests/static_above_sp_739.rs: down-shift to
  budget+12 = 2060, relocation without the shrink, loud refusal on the
  no-reloc module, loud i64 decline — plus a baked-pair text scan mirroring
  the oracle.

Regression evidence: #383/#678/#707 suites green (static_downshift_678,
multi_sp_rebase_707, shadow_stack_shrink_383 + both .py oracles), frozen
anchors 10/10, workspace 2166 passed / 0 failed, fmt + clippy -D warnings
clean.

Refs #739 #678 #383 #707, VCR-MEM-001.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
@avrabe
avrabe force-pushed the fix/739-above-sp-static branch from 9d383ef to 7725ee6 Compare July 15, 2026 02:45
@codecov

codecov Bot commented Jul 15, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 81.12450% with 47 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/synth-synthesis/src/instruction_selector.rs 75.93% 45 Missing ⚠️
crates/synth-cli/src/main.rs 96.77% 2 Missing ⚠️

📢 Thoughts on this report? Let us know!

@avrabe
avrabe merged commit 700b979 into main Jul 15, 2026
37 of 38 checks passed
@avrabe
avrabe deleted the fix/739-above-sp-static branch July 15, 2026 04:10
avrabe added a commit that referenced this pull request Jul 15, 2026
…n treatment (#747)

* fix(#746): relocate i64/wide static-region loads/stores (#744 treatment for the wide arms)

The #744 fix relocated the i32 sub-word static-region arms under the
native-pointer ABI; the i64 arms (i64.load/i64.store pair accesses and
the i64 narrow load8/16/32 + store8/16/32) still LOUD-DECLINED, so any
function bulk-copying an above-sp_init static via i64 (gale's gust:os
log.line emit path) was skipped and the object unlinkable.

Upgrade decline -> relocate, mirroring the I32Load #359 / #744 sub-word
branch exactly: materialize the base as __synth_wasm_data + offset
(LdrSym literal-pool load, reloc-visible to the #678 --shadow-stack-size
rebase and the post-link in-range oracle), Add the dynamic index, then

  * I64Load / I64Store: pair access through [base, #0] / [base, #4]
    (I64Ldr/I64Str, imm form — the base temp is kept disjoint from the
    dst pair since both halves read it);
  * i64 narrow loads: LDRB/LDRSB/LDRH/LDRSH/LDR of the low half through
    the relocated base + the sign/zero hi-half fill;
  * i64 narrow stores: STRB/STRH/STR of the low half (wrapping
    semantics, same as the raw path).

Below wasm_data_base the raw [R11 + addr + #offset] path is untouched
(frozen behavior), and the float arms keep their GI-FPU-002 loud
decline (documented on is_native_pointer_static_offset).

Unit tests: test_746_i64_wide_static_offset_is_relocated +
test_746_i64_narrow_static_offset_is_relocated (all nine arms assert
the LdrSym relocation, the correct memory-op form, the hi fill, and
that the offset is never baked as a Movt immediate); the pre-#746
decline test is superseded.

Refs #746 #739 #242 (VCR-MEM-001).

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

* test(#746): red-first i64/wide above-SP static shrink oracle + CLI gates, CI-wired

scripts/repro/wide_static_746_differential.py (+ mem746_wide_static.wat,
the #739 meld --memory shared geometry): i64 store/load round-trips and
narrow sign/zero-extend reads through statics ABOVE sp_init after the
--shadow-stack-size shrink, unicorn vs wasmtime with .bss/.data at
SEPARATE bases so a baked absolute linmem offset cannot accidentally
resolve. RED on v0.42.0 — the compile itself declines (all 7 fixture
functions loud-skip, 'no functions compiled successfully') — GREEN with
the relocated arms (25/25 cases match). Wired into the
trap-semantics-oracle CI job next to the #739 sub-word oracle.

CLI integration gates (static_above_sp_739.rs):
  * i64_static_offset_relocates_746 — the pre-#746 decline module now
    compiles with a __synth_wasm_data + 0x100008 reloc and no baked
    MOVW/MOVT static-region pair;
  * wide_static_relocates_and_downshifts_746 — the differential fixture
    down-shifts its BSS i64 statics to budget+16/budget+24, keeps the
    shrunk reservation, and ships no baked pair.

Refs #746 #739 #242 (VCR-MEM-001).

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

---------

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
avrabe added a commit that referenced this pull request Sep 18, 2026
…lanes, two deferrals measured, and the v0.70 steps-1-2 filing (#1340)

* RQ-70-NPA (#1331): static-data f32.load/f32.store relocate under the native-pointer ABI — cpetig's blocked exports go 4 of 6 to 2

REPRODUCED on the reporter's own command line first, and their issue excerpt
UNDERCOUNTS exactly as #1318's did: reported 2 functions, measured 6 of 22 (4 of
6 EXPORTS), rc=1 via #952, NO object — 4x f32.load and 3x f32.store "from/to the
static-data region under the native-pointer ABI".

AFTER: 2 of 22 functions, 2 of 6 exports. `rate#tick` and `attitude#tick`
compile; zero f32 static-data declines remain.

The machinery existed. `emit_wasm_data_addr` relocates a base to
`__synth_wasm_data + offset`; the i32 sub-word arms got it in #744 and the i64
arms in #746. The float arms declined loudly instead — and correctly: the raw
`[R11 + addr + #offset]` path BAKES the linmem offset as an un-relocated
MOVW/MOVT immediate, invisible to both the #678 `--shadow-stack-size` down-shift
and the post-link in-range oracle because each walks RELOCATIONS. That is the
#739 silent OOB, so this ships the relocation, not the bake.

No float address machinery was needed: both arms already route the 4 bytes
through a core register and bit-cast (VMOV), so only HOW THE ADDRESS IS FORMED
changed and the loaded/stored bytes are identical by construction.

NOT CLAIMED CLOSED. `position#tick` and `ekf#estimate` now reach a DIFFERENT
ceiling the f32 decline was hiding: `LdrSym literal pool out of range (#345):
imm12=11744 / 4344 > 4095`. Did the relocation's own pool entries cause it? The
magnitude answers — imm12 is the PC-to-pool distance, so 11744 is a ~11 KB
function, and each relocated access adds at most one 4-byte pool word; even 50
added entries leaves ~11.5 KB, still ~3x over the limit. A pre-existing
function-size wall, unmasked rather than introduced.

RED-FIRST: scripts/repro/npa_static_f32_1331.wat, a 20-line reduction carrying
one dynamic-index f32.load and one f32.store above the SP global's initializer.
Pre-fix 2 of 2 skipped with exactly the reporter's two decline strings; post-fix
an 813-byte object. Not on EXPECTED_DECLINES, so the wired sweep reds on a
regression.

The CONST static-data address declines (#237) are deliberately untouched: a
different address mode, measured to fire on none of the seven.

GATES: fmt, clippy -D warnings, ARM corpus sweep PASS (174/194 compiled,
3428/3428 vectors, 0 mismatches).

Refs #1331
Refs #1318

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

* RQ-70-FALCONCORPUS (#1318): two reduced fixtures land, and "the corpus" turns out to name THREE populations

v0.69 added only PAGESIZE's two .wat to scripts/repro; cpetig's fused.wasm and
opt.wasm were never committed, so FALCON's 826 identical / 209 identically
failing / 0 changed and its 1-of-21 / 7-of-17 counts cannot be reproduced from
this repository by anyone — and FALCON was that release's only must.

ROUTE B, TAKEN TWICE. Both of v0.70's downstream blockers now ship a committed
reduction that reproduces the reporter's decline: spill_slot_alias_1321.wat (54
lines, with RQ-70-ALIAS) and npa_static_f32_1331.wat (20 lines, here). Neither is
on EXPECTED_DECLINES, so the wired sweep reds if either regresses — verified by
running it against the pre-fix binaries.

RESIDUAL, NAMED: a reduction reproduces the DECLINE, not the module. FALCON's
826/209/0 stay non-re-derivable, and this does not claim otherwise.

THE SECOND FINDING. A census of every committed script walking scripts/repro/
finds THREE populations, not the two the plan noted: *.wat only (7 scripts, 193
modules), *.wat + *.wasm (5 scripts, 209), *.wasm only (1). That is how FALCON's
'1035 = 207 x 5' and SUBTRACT's '965 = 193 x 5' were both 'the corpus' in one
release. And 1035 is ALREADY STALE — re-derived today the populations are 193 and
209, because v0.69 itself added two .wat.

NOT unified, deliberately: the globs differ for real reasons (byte-triage needs
two binaries per module; a .wasm has no second source), and collapsing them would
move numbers across a dozen pinned gates for no correctness gain. The defect is
the unnamed attribution in PROSE, so the deliverable is the census.

Refs #1318

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

* RQ-70-CITEGAP (#1333): the citation gate had never scanned a single release artifact — recursive glob, the keys artifacts actually cite under, and two namespaces instead of one

The glob was non-recursive, so 105 of 135 artifact files were invisible,
including ALL 10 of v0.69's and ALL 8 of v0.70's. It read only `run:` keys,
which no release artifact has ever had. And it knew one citation form while
release artifacts use two: `--test <target>` names an integration-test FILE,
`--lib`/`--` are substrings over test PATHS — measured, 4 of v0.69's 5
citations are targets, so widening the glob ALONE would have produced four FALSE
FAILURES on valid citations.

RED-FIRST: planting `--test this_test_does_not_exist_9999` into implemented
RQ-69-ELFNAMES left the gate at rc=0 printing 'every cited test filter resolves'.
After the fix the same plant reds, naming artifact, status and missing target.

The widening then exposed a real scan bug: module paths were built only from
`mod` declarations, never from the FILE, so `--lib dwarf_line::` read as
dangling though dwarf_line.rs holds 3 tests and lib.rs declares the module.
Fixed; test names 5233 -> 7224. The header promises approximation failures are
loud, and this one was.

Keys are limited to run/done-when/verified-by, NOT description: RQ-69-PROSEGATE
refuted prose-scanning one release ago — it cannot tell a CLAIM from a MENTION.

AFTER: 135 files, 33 citations (15 target, 18 filter), 0 false claims.

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

* RQ-70-WINDOWVAC (#1334): R10's window was blind to this project's own delivery convention — teach it RQ-NN, and put the floor where it can say why

Re-derived per window with the script's own regex: delivery-shaped commits went
4, 8, 8, 11, 2, 0, 0 while RQ-style subjects went 3, 3, 2, 0, 3, 8, 8. The
convention became 'RQ-NN-NAME (#issue): ...' around v0.67 and R10's window loop
only matched 'type(scope): ', so the completeness floor that exists to notice
work landing with every artifact silent saw ZERO commits for two releases.

The recognizer already existed — ARTIFACT_ID is what R4 uses, which is why 88
delivery commits match overall. It was simply never applied in the window loop.

CI could not have caught it: the grep is '[0-9]+ delivery-shaped', and [0-9]+
matches 0 — #1243's shape, a floor regex that does not floor. So the floor moved
into the script, conditional on window size (6) because early in a cycle a window
legitimately holds only a plan commit.

PROVEN BOTH WAYS: replaying v0.68.0..v0.69.0 now reports 8 delivery-shaped, 8
attributed (was 0); rewriting those subjects RQ-69- -> DELIVERED-69-, simulating
the next convention change, FIRES the new floor.

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

* RQ-70-DONEWHEN (#1335): the conformance gate counted done-when DECLARATIONS and printed them as evaluation

Manual share per release: v0.61 11/15 ... v0.66 8/8, v0.67 7/7, v0.68 9/9,
v0.69 9/9 — four releases at 100%, all printing the same 'N/N done-when' line as
a release with everything machine-checked. A `manual:` signature is present and
evaluated by nothing; status_evidence's R3 fires only on contains:/file:.

NOT a ban. Reading all nine v0.69 predicates: each is a COMPOUND acceptance
statement (red-first AND a class sweep AND a named ceiling AND an execution
differential) that no single mechanical signature can carry. But most hide a
mechanical conjunct written in prose and checked by nothing — ELFNAMES,
PAGESIZE, PMPLIB and VFPUNKNOWN each name a real test, SUBTRACT's line IS a
claims.yaml ratchet. Five citations no gate read, which is RQ-70-CITEGAP's
finding from the other side. The evidence existed; manual: was where it went to
not be checked.

So the deliverable is honest output. On v0.69.0 the gate now prints
'9/9 done-when DECLARED — 0 mechanically evaluable (contains:/file:), 9 manual:
(declared only; R3 cannot fire on these)'. Verdict unchanged: still CONFORMS.

Pinned by two new unit tests that ci.yml runs.

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

* RQ-70-RIVETNOTES (#1337): derive the release's artifact section from rivet, and report the trace-graph delta nobody had looked at

The CHANGELOG's per-release section is hand-written prose about a typed set rivet
can diff. v0.66 filed two of its OWN artifacts under [Unreleased] because the
list was remembered rather than derived.

scripts/release_notes_from_rivet.py extracts the previous tag's rivet sources
with git archive — bounded by the paths rivet.yaml itself declares, so a moved
source is a loud extract failure, not a silently narrower diff — runs rivet diff,
and emits the artifact list AND the diagnostic delta.

THE DELTA IS THE NEW PART. v0.69.0 -> this tree with the pinned 0.37.0: 8 added,
0 new ERRORS, 22 NEW WARNINGS in three classes shipped unseen — RQ-NN ids are not
commit-trailer shaped (so rivet cannot trace them; the same convention WINDOWVAC
had to teach status_evidence, found from the other side), five artifacts use a
req-type the schema does not define, and none has an incoming verifies link.
None fixed here; all now reported.

THE VERSION CHECK IS LOAD-BEARING. This session's PATH rivet was 0.32.0 against a
0.37.0 CI pin (#1236/#1308), and 0.32 reports '0 broken cross-refs' on a tree
where resolution never RAN — a clean bill of health from a check that did not
happen. The generator refuses anything older than the CI pin, and
test_pin_is_not_below_ci RE-DERIVES that pin from ci.yml rather than restating
it, so the two cannot drift behind a green gate.

Anti-vacuity: zero added artifacts REFUSES rather than emitting an empty section
that would read as 'nothing shipped'.

8 unit tests, wired in ci.yml beside the loop-conformance and status-evidence
potency tests.

Refs #1337

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

* plan(v0.70): record RQ-70-PAGELIB (#1315) as DEFERRED to v0.71, with the measurement and the question posted

A deferral is not a delivery, so this deliberately does NOT wear the
`RQ-NN-NAME (#issue):` delivery subject — RQ-70-WINDOWVAC teaches that shape to
status_evidence's window in this same release, and R4 correctly refused the
earlier subject as a delivery claim for an artifact whose status is `proposed`.
The gate caught its author within the hour.

Verified at source: refuse_custom_page_size and refuse_shared_memory live only in
synth-cli/src/main.rs; synth-core's decoder decodes page_size_log2 and stops, its
own comment saying it is "Consumed by refuse_custom_page_size in synth-cli". So a
caller of the PUBLISHED synth-core still gets a custom page size silently
ignored, and __synth_mem_size_N inherits the over-grant — the same shape #1317
closed in the same release on the opposite principle.

NOT scoped here, deliberately. Pushing the refusal into synth-core forecloses a
choice that is not mine: a 1-byte page is exactly the granularity gale's
per-memory MPU region table (#1145) might WANT, and removing a mode before
knowing whether an executed criterion needs it is what v0.68 nearly did to
--safety-bounds mpu.

Asked on #1145 today, three questions, none answered yet. The measurement is
recorded so v0.71 need not re-derive it, and "CLI-only is correct" is an
acceptable answer that keeps this deferred WITH a reason rather than dropped.

Stays `proposed`, so #1315 is not closed on the tag.

Refs #1315

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

* plan(v0.70): file RQ-70-ARCHMODEL (#1136) — steps 1-2 N/A again, re-verified at the cut, tags checked BEFORE not after

The conformance gate reported `DERIVED-FAIL: the only filed steps-1-2 decision is
RQ-63-ARCHMODEL, scoped to release v0.63 - NOT v0.70` while there was still time
to file. v0.69 learned this the other way round: its ARCHMODEL had LOST the
`feature-loop` tag, so the artifact filed to keep a deferral VISIBLE was itself
invisible to the gate, and the release read DOES-NOT-CONFORM until the cold
review caught it. Checked against the predecessor's tags this time, before the
cut.

Re-verified rather than remembered, observed 2026-09-18T21:13:53Z:

    spar#445  state=OPEN  updatedAt=2026-09-03T10:57:37Z  comments=0

Unmoved since the v0.68 and v0.69 cuts. The count is the carried-from chain
walked back to the v0.63 head, not an asserted ordinal — release artifacts only
exist from v0.63, so "the Nth N/A" is not derivable and is not claimed.

A deferral filing is not a delivery, so this wears a `plan(...)` subject.

Refs #1136

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

* RQ-70-NPA (#1331): re-measure every pinned number on the rebased tree, and guard the empty-areas case

NUMBERS, MEASURED AFTER THE REBASE ONTO THE MERGED ALIAS WORK, never added to
the previous figures (the v0.69 lesson: 856 vs the 854 measured before the
cascade settled, which `cargo fmt` then moved twice more):

  selector_lines_code   19478 -> 19529   (+51, waived with the reason in claims.yaml)
  selector_lines_total  30071 -> 30122   (tracked, no waiver needed)
  home-alias audit      7203  -> 7207 functions, 8214 -> 8220 homes
                        (one new scripts/repro fixture x the two hard-float legs;
                         hits: 0 and 217081 attributed unchanged)

THE EMPTY-AREAS GUARD. `policed` answered `Some(areas) => areas.iter().any(..)`,
so `Some(&[])` would have disabled the #331 check entirely. Nothing produces it
today — select_with_stack collapses an empty list to None — but the degradation
belongs in the predicate rather than in one caller's care, and the load-bearing
question for any "unknown" value is whether it means POLICE EVERYTHING or POLICE
NOTHING. Pinned by ra003_areas_empty_is_unknown_not_permission_1321; ra003 is now
39 tests and RQ-70-ALIAS's artifact says 39 rather than 38.

RQ-70-DONEWHEN records its own measured outcome: manual-share went 100% for four
releases running to 22% here (7 of 9 done-when mechanically evaluable). Nothing
banned `manual:` — R9 refused RQ-70-ALIAS's first signature and the standard
spread. The two that remain manual are the two DEFERRALS, where no mechanical
predicate exists because nothing landed.

Refs #1321
Refs #1331
Refs #1335

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

* plan(v0.70): correct RQ-70-PAGELIB — #1315 was already CLOSED, so the gap gets its own issue (#1339)

A false statement in my own artifact, caught before the cold review and recorded
rather than quietly edited. The first draft said "#1315 stays OPEN; this artifact
is `proposed`, so the release does not close it." #1315 was CLOSED on the v0.69
tag at 2026-09-18T17:53:18Z by RQ-69-PAGESIZE, which shipped the CLI refusal.

The REASONING was right — do not close an issue whose artifact claims no
completion — and the FACT was wrong: I applied that rule to an issue another
artifact had already closed for its own valid reason.

So this is a follow-up to a CLOSED issue, not a deferral of an open one. It gets
its own tracking issue (#1339) rather than a reopen, because the library-side gap
is a different defect from the one v0.69 fixed, with a different fix site and a
different consumer — and reopening a correctly-closed issue would misreport what
v0.69 delivered. `fields.issue` now points at #1339.

Refs #1339

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

* RQ-70-FALCONCORPUS (#1318): pin the corpus counts to a REF, and show them drifting

The first draft said "193 modules on main" — already wrong by one, because the
ALIAS fixture had merged in between. A stale number inside the artifact that
exists to say numbers go stale is the R11 blind spot in its purest form.

Counted with the SAME non-recursive glob the scripts use (a recursive count
differs again — scripts/repro has subdirectories):

    at v0.69.0       A=193  B=209    x5 = 965 / 1045
    at main today    A=194  B=210    x5 = 970 / 1050
    with this PR     A=195  B=211    x5 = 975 / 1055

So the plan's "1035 = 207 x 5" was right for the tree it was measured on and
wrong two releases later, and "965" moves every time a fixture lands — including
the two this release adds. Showing the drift across three refs makes the point
the artifact is about far better than any single figure could.

Refs #1318

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

* RQ-70-CITEGAP (#1333): fix the two reds my own changes caused — a moved output format and a YAML shape rivet rejects

CI found both; neither was visible to any local gate, and both are instances of
the class this release is about.

1. THE NON-VACUITY FLOOR READ A FORMAT I HAD MOVED. ci.yml asserted
   `^artifact citations: N cited filters over M test names`. RQ-70-CITEGAP
   rewrote that summary line to carry the target/filter split and the file
   count, so the grep matched nothing and the STEP failed while the GATE
   passed. Changing a gate's output means changing whatever reads it.

   The replacement floor is STRONGER than the one it replaces: it pins the
   artifact-FILE count above 100. The pre-fix non-recursive glob saw 30 files
   and zero release artifacts, so a regression to it now fails here.
   NEGATIVE CONTROL, run: reverting the glob gives "30 artifact files" and the
   floor refuses it — while the gate itself still exits 0, which is exactly why
   the floor exists.

2. A YAML SHAPE PyYAML ACCEPTS AND RIVET REJECTS. RQ-70-ARCHMODEL's long
   one-line `verified-by` was dumped as a multi-line SINGLE-QUOTED flow scalar.
   PyYAML round-trips it, so claim_check, status_evidence and the citation gate
   all passed locally — and the required `Rivet Validation` job failed with
   `RQ-70-ARCHMODEL.yaml:65: expected ':' after mapping key`. Reproduced in
   isolation (it needs the `common` schema loaded) and bisected to the field.

   Fixed by emitting FOLDED block scalars (`>-`), which carry the same logical
   single-line value and are what the hand-written artifacts use. Swept the
   CLASS rather than the instance: RQ-70-PAGELIB had two more multi-line
   single-quoted values that happened not to trip the parser, and a scan now
   reports zero remaining across artifacts/release-v0.70/.

Refs #1333
Refs #1136

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

* RQ-70-NPA (#1331): re-anchor the mutation ledger after the empty-areas guard shifted liveness.rs again

`reanchor` moved 5 sites, 0 not found — pure relocation (17 insertions / 17
deletions, only the location keys and reanchored_at change). test_mutation_survey
and claim_check green on the re-anchored ledger; the `mutants_untested` ratchet
does not move, because relocating a site changes where it is, not whether it is
tested.

This is the SECOND re-anchor of this release: the first followed RQ-70-ALIAS's
~50 added lines, this one follows the 12-line empty-areas guard. Both were
correct and mechanical, and both cost a commit plus a full CI round — the ledger
pins sites by file:line:col, so any edit ABOVE a pinned site in an anchored file
invalidates it.

Worth noting rather than fixing here: the same file already anchors its one
borderline record by its `before` TEXT precisely because "line numbers move"
(see BORDERLINE_LOUD_BEFORE and the v0.66 incident its comment records). The
ledger itself could use that same stable anchor. Filed as a v0.71 candidate, not
smuggled into a release fix.

Refs #1189

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 22, 2026
…e cold review corrections that did not land (#1348)

* release(v0.70.0): "Evidence you can re-derive" — 9 artifacts, 7 implemented, 2 deferred with measurements, plus the cold review's 21 findings

The version bump, the CHANGELOG with a DERIVED artifact list, and the cold
review's corrections — which did not land before #1340 merged, the exact v0.69
failure mode this release is named against.

Every correction was independently re-derived before it was applied, so two
ended as refutations rather than fixes:

  - finding 16 REFUTED: all 8 non-test `spill.alloc()` sites are dominated by a
    guard, and an `assert!(self.area_reserved)` planted in `SpillState::alloc`
    fired 0 times over 766 tests and 3428 executed vectors, with a should_panic
    control proving the assert can fire. Probe reverted, sha256 restored.
  - finding 14 RECORDED, not back-filled: v0.70 has no `_release.yaml` and one
    is not written here, because it is a plan-time document and no gate reads
    it. v0.71's planning PR creates one.

Two gates that could not fail, both fixed red-first:

  - `artifact_citation_check.py` silently skipped any artifact it could not
    parse, and used last-wins `yaml.safe_load` beside a strict sibling. It now
    hard-fails and shares the sibling's StrictLoader — no second definition.
  - `liveness.rs`'s `policed` guarded `Some([])` but not `Some(&[a..a])`: a list
    of EMPTY ranges names no offset, so the check policed NOTHING while looking
    configured. One arm now covers both shapes; the new test FAILS against the
    old guard.

`test_release_notes_from_rivet.py` 8 -> 11: both generator refusals are pinned
against a fake rivet, with a negative control so the reds cannot be an
unreachable harness.

DISCLOSED: RQ-70-NPA's new f32 static-data branches bypass the bounds-check
helpers, so under `--native-pointer-abi --safety-bounds software|mask` an f32
access that previously loud-declined now emits UNGUARDED (class extension of
#744/#746). Those 13 comment lines are the whole +9 on `selector_lines_code`,
waived with that reason.

Re-derived at the cut, not carried: trace-graph delta 26 new warnings in four
classes (recorded as 25 with the fourth misattributed), citation gate 7242 test
names, corpus sweep compiled=175/195 executed=3428/3428 mismatches=0.

cargo fmt rc=0, clippy -D warnings rc=0, cargo test --workspace 168 suites /
0 failures, claim_check 75/75, status_evidence + check_version_pins +
oracle_wiring + artifact_citation all rc=0, rivet "ours" errors 0.

Refs #1321
Refs #1331
Refs #1333
Refs #1334
Refs #1335
Refs #1337
Refs #1318
Refs #1136
Refs #1339

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

* evidence(v0.70.0): cpetig CONFIRMED both must-lane fixes on their own module, and named the next wall themselves

Documentation and artifact evidence only — no code, no gate, no version change.

The blocked party rebuilt from c18c185 on their own toolchain (meld 0.56.2,
wac-cli 0.10.1, cortex-m7) and reported back on 2026-09-19:

  rc=0, "Compiled 21 functions" with 0 skipped, 68374 bytes of code, 70172-byte
  ELF, 66 relocations, and "verify-embedder OK: 0 reserved-register writes in
  19140 instructions across 21 symbols"

  "Previously this was rc=1, 1 of 21 functions skipped with `SpillSlotAliased`,
   no object — i.e. the #1321 fix lands."
  "The f32 static-data declines are gone ... the `GI-FPU-002 phase 1b` messages
   from the original report are gone."

That is an INDEPENDENT reproduction by the person the release was ordered
around, which is the only acceptance test these two lanes ever had.

The byte counts differ from the artifacts' own [REPORTER-ONLY] figures because
it is a NEWER build of their component (cascade-v1139-fused.wasm, 41055 bytes).
Both are recorded as two measurements rather than reconciled into one — the
release's own rule about not carrying a number between trees.

TWO THINGS THIS ALSO SETTLES:

  - The next wall on `--native-pointer-abi` is the one RQ-70-NPA PREDICTED, and
    the reporter hit it independently: `LdrSym literal pool out of range (#345)`
    in a single 50722-byte function. #1331 stays OPEN on their evidence, not on
    our caution.
  - v0.70 asked whether `--native-pointer-abi` is load-bearing for their build
    or merely preferred, and shipped without an answer. It is answered by
    demonstration: they are shipping via `--embedder-data-init
    --embedder-global-init` today. So it is a PREFERENCE blocker, which should
    have lowered this lane's rank against ALIAS — recorded so the v0.71 ranking
    starts from it rather than re-deriving it.

claim_check 75/75, status_evidence + check_version_pins + artifact_citation +
oracle_wiring all rc=0, rivet delta re-derived and unchanged at +26 warnings /
0 new errors. No Rust changed, so fmt/clippy/test are unaffected.

Refs #1321
Refs #1331

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

* review(v0.70.0): the RC cold review found 7 FALSE and 4 MISLEADING statements, one of them reddening a required gate — all corrected

Two fresh-context reviewers ran on 62993ad. Neither returned a BLOCKER in the
code, and the prose pass found the release doing the thing the release is named
against.

BLOCKING, and the gate caught it before I did. The review record declared two
passes, cross-referenced "pass 2, finding A", and contained no pass 2 — while
naming only `4e865f31`, an unmerged branch head. Conformance step 7 read
DERIVED-FAIL, "exists but names no commit that is an ancestor of the release
commit". Pass 2 is now written and the record declares `Commit reviewed:
62993ad`.

THE SHARED ROOT CAUSE, in the reviewer's words: "a number measured before the
last edit to the thing it measures."

  - `npa_static_f32_1331.wat`'s "41 total, 38 non-blank" was written by the hunk
    that split a comment line in two — it ADDED the lines it was counting.
    Correcting it in place to 43/40 made the file 47/44 and wrong a second time,
    in the same session. The header now quotes only the CODE-line count, the one
    figure that survives editing the prose around it.
  - CITEGAP's "5243 -> 7242" is derivable from NO single tree: 5243/7239 are
    this release's parent, 5245/7242 the cut. Only the `after` half had been
    re-derived. Both halves are now measured on the cut.
  - ALIAS's "ra003 34 -> 39" was right at the parent and made 40 by THIS
    release's own finding-18 test.

OTHER FALSE STATEMENTS, all corrected:

  - the cold review claimed NPA's "20-line reduction" was corrected; only the
    .wat header had been, and `RQ-70-NPA.yaml:75` still said it.
  - ARCHMODEL said "release artifacts only exist from v0.63". False —
    `release-v0.56.yaml` onwards exist, and RQ-69-ARCHMODEL had EXPLICITLY
    retracted that exact sentence. It returned because this artifact was written
    from its predecessor's SHAPE rather than its predecessor's CORRECTION.
  - "four sit under a retry rung" while listing five (2+4+1 against an asserted
    eight).
  - "all EIGHT non-test `spill.alloc()` sites": there are FIVE call sites, and
    all eight cited lines are GUARDS. Three of the five allocators are helpers
    reached from more than one guarded caller. The reviewer re-derived every
    caller set and agreed the narrowing is sound — the substance held, the
    citation did not.

MISLEADING, corrected: reporter-only figures presented as re-derivable (an
unmarked `opt.wasm` bullet under a "[REPORTER-ONLY] except where marked" header,
and the CHANGELOG's headline table unlabelled); "the committed 54-line fixture"
stating a convention on one fixture and not the other; "three gates that could
not fail" when there were four.

DISCLOSED rather than fixed: the `assert!(self.area_reserved)` probe was
reverted, so the central evidence for this release's one REFUTED finding is
unreproducible from the shipped tree. The static argument and guard line numbers
are re-derivable; the silent probe run is not. A permanent `debug_assert!` is a
v0.71 candidate, not a change to make at a cut.

Also from the code pass: the citation gate globbed only `*.yaml` while the
sibling it shares a loader with globs `*.yml` too — so a `.yml` artifact was
legal to the release gate and INVISIBLE here, unparseable ones included. Both
extensions now, through a single `artifact_files(root)` used by the scan AND the
reported count, which had been two separate globs. Proven: a `.yml` artifact
citing a non-existent test now reds. An empty or comment-only artifact also
vanished silently (`yaml.load` -> None); it now hard-fails, EXCEPT for
`_release.yaml`, whose required shape is comments-only — the first version of
that guard reddened all nine of them, a checker failing on the correct answer.

The fixture repo now neutralises the ambient git config wholesale
(GIT_CONFIG_GLOBAL/SYSTEM, NOSYSTEM) rather than `commit.gpgsign` alone, and the
stale-rivet test uses a non-empty diff so its returncode assertion is
load-bearing — verified by mutation: removing the version refusal now fails on
that line, where before only the message assertion could catch it.

The `selector_lines_code` waiver's own accounting was false: "13-4 across two
sites" against an actual +17/-8 across THREE, the third being a doc comment that
had claimed the float arms still decline. Total was right, the account of it was
not.

No Rust changed. claim_check 75/75, status_evidence + check_version_pins +
artifact_citation + oracle_wiring rc=0, gate unit tests rc=0, rivet +26/-0
re-derived, citation 7242 names / 136 files re-derived, ra003 40 passed.

Refs #1321
Refs #1331
Refs #1333
Refs #1337

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

* fix(mutants): re-anchor the pinned mutant ledger — v0.70's liveness.rs edits moved a pinned site four lines down

The `mutation survey` job went RED on the release PR while main (da110b8) and
c18c185 / 1da8c4c / bd65e45 were all GREEN on the same job, so the red
belonged to this PR and not to the runners. Asked that question first.

IT WAS NOT A COVERAGE REGRESSION, though the failing step says "controls must
die, survivors must reproduce", which is exactly what a coverage regression
looks like.

`docs/status/mutation_survey.json` pins every mutant by `file:line:col`. The
subset entry `R4-shared/REG/liveness.rs:7346:36` targeted

    let aapcs_dead_at_return = [Reg::R2, Reg::R3, Reg::R12, Reg::LR];

and this release's `policed` fix plus its red-first test added +27/-5 lines to
`liveness.rs`, ALL ABOVE that line. The statement moved to 7350; line 7346 now
holds `let ends_in_return = matches!(`. The pin was aimed at different code.

`reanchor` is the sanctioned remedy and says so in its own docstring — "the id
embeds the line number, so a shifted site must be re-resolved rather than
trusted". It re-locates by each mutant's stored `before` text:

    reanchor: 5 sites moved, 0 not found, tree c51823a
    ci_subset: R4-shared/REG/liveness.rs:7346:36 -> :7350:36

NOTHING WAS RE-BASELINED. mutants 34 -> 34, controls 3 -> 3, ci_subset 10 -> 10,
UNTESTED 4 -> 4 (the `mutants_untested` ratchet), claim_check 75/75. The replay
now passes on its own terms:

    MUTANTS-CI subset=10 controls=3 non-killed=7 failures=0
    MUTANTS-REACH-WIDE entries=4 reached=4 unreached=0
    MUTANTS-GATE ok — floors met, exact fields exact, reach complete

Filed for v0.71 rather than changed at a release cut: CI never runs `reanchor`
(`grep -c reanchor .github/workflows/ci.yml` = 0) and the failure names neither
line drift nor the remedy, so any PR that inserts a line above a pinned site
gets a red that reads as lost coverage — and the tempting fix, `pin-subset`,
would silently RE-BASELINE coverage instead of re-locating a site. That is the
same shape as this release's own `.wat` header counting the lines its hunk had
just added: an anchor that quietly means something else after an unrelated edit.

No Rust changed. All five gates rc=0.

Refs #1189
Refs #1321

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

1 participant