Make the gates real: CI-wire the gpio-thin + rv32-boot oracles (#879), claim-pin template prose (#880)

[avrabe]

Closes #879. Closes #880. Two defects, one class: gates that look like gates but don't bite.

#879 — the gpio differential is now CI-enforced

scripts/repro/gpio_thin_846_differential.py — the gate behind the v0.50.1 (534→506 B) and v0.52.0 (506→502 B) headline size claims, and the only harness executing gale's REAL gpio-thin driver across a pin sweep including pin ≥ 32 (the mod-32 boundary an unsound shift-mask elision would corrupt) — appeared nowhere in CI.

• Wired into the ARM trap-semantics oracle job, right after the thumb-2: elide the #682 mod-32 shift mask when the shift amount is statically <32 (constant/range-carried) — measured 12% on gale gust_mix #686 mask-elision oracle it complements. capstone added to that job's pip line (the mask census disassembles .text; the job previously installed only wasmtime/unicorn/pyelftools).
• Non-zero check count asserted, not just exit 0: the script now prints a machine-readable #846 CHECKS=75/75 trace_events=N summary and the CI step greps the pinned 75/75. Script-side anti-vacuity added: hard-fail on empty/short sweeps, zero mmio trace events, or a reloc walk that finds no import call sites (a missing-import path can no longer skip).
• Same audit found a second shelfware oracle: rv32_data_798_boot_differential.py (the RV32: active data-segment initializers are silently dropped — ship them (linker-script placement + startup copy) and hard-decline until then #798 full-boot gate — clang+lld build the bare-metal riscv32 firmware, unicorn boots it from _reset). Wired into the same job. Both wirings are pinned in claims.yaml (SYNTH-GPIO-846-ORACLE-CI-WIRED, SYNTH-MATRIX-RV32-DATA-SHIP) so they cannot be silently un-wired again.

Red-first evidence (local, hardened script + fresh debug binary):

• Green: 75/75 match, 105 mmio trace events, 534→502 B / 10→3 masks; rv32 boot oracle PASS.
• RED 1: simulated broken reloc walk (no call sites) → VACUOUS: no mmio import call sites found, exit 1.
• RED 2: silently shrunk pin sweep → script self-consistent at CHECKS=70/70 but the CI-side grep "^#846 CHECKS=75/75" exits 1 — the pinned count bites where exit-0 would not.

#880 — template prose is now claim-gated (approach 3 + oracle binding, limits stated)

The staleness gate proves doc == render(template); wrong template prose renders faithfully and stays green (the v0.51 "div/rem declined" / v0.52 "OOB-trap is a follow-on" cold-read defects). Chosen approach: pin the template's load-bearing capability phrases verbatim in claims.yaml (mechanism already existed), each bound to independent evidence — the oracle script that executes the capability exists and is CI-wired (count-min over ci.yml, the #879 lesson generalized), plus a stable code anchor where one exists (MemBounds::Software, validate_served_image). 8 new SYNTH-MATRIX-* / gpio-wiring claims; 34/34 hold.

Red-first evidence: replaced the template's **BOUNDS-CHECKED by default** … phrase with "bounds checking is a follow-on" (the literal v0.52 defect), regenerated so the old staleness gate stays green → claim_check exits 1 with FAIL SYNTH-MATRIX-AARCH64-BOUNDS-DEFAULT. Reverted. (Incidentally re-proven a second time when a careless git checkout of the template reverted the legit fixes — the new pins went red on that too.)

Honest limit: verbatim pins catch drift of pinned phrases (weakening a shipped-capability claim forces a deliberate ledger bump next to its evidence); they cannot catch a brand-new false claim typed into the template. That residual stays on review + on extending the pin list when new load-bearing phrases land. Deriving the prose from the selector's decline sites (option 1) remains the stronger end-state.

Template/README audit — six live defects of exactly the #880 class, fixed here

1. Matrix said "RV32 warns loudly on dropped initializer bytes" — RV32: active data-segment initializers are silently dropped — ship them (linker-script placement + startup copy) and hard-decline until then #798 (v0.48) ships the segments and hard-errors on served/runtime disagreement; four releases stale.
2. WCET decline row listed "calls" as blanket-D — phase-3 inter-procedural composition (v0.48) bounds direct local calls; phases 4–5 (hint-gated recursion depth / masked-ceiling loops) were absent entirely.
3. Matrix + README said trunc_sat "not decoded" and "a pressure-dependent f32 class still tracked in #369 marked closed, but the real falcon-flight-v1.123 fused core still skips 26/156 on --relocatable cortex-m7dp (incl. run-stabilization); trunc_sat unsupported + a pressure-dependent 'integer popped f32' class #782" — trunc_sat shipped v0.49; #369 marked closed, but the real falcon-flight-v1.123 fused core still skips 26/156 on --relocatable cortex-m7dp (incl. run-stabilization); trunc_sat unsupported + a pressure-dependent 'integer popped f32' class #782 is closed, successor residual is GI-FPU-002 + RA tail is now the ONLY gate between the falcon cascade and the M7 — 5 entry-point symbols; phase-2 D-register pressure is new in v0.52 (inline-f64 #869 lowering) #881.
4. "dissolve: bind passed-through embedder import cabi-arena-realloc to the native TCB arena allocator #418 partially open" — closed with the v0.47 arena-bind.
5. Multi-memory row said "D — module-level loud decline" while the Multi-memory structural isolation: lower N wasm memories to N distinct native bases (memidx-through-IR, cross-memory ops, expose base/size for MPU/PMP) #406 per-memory lowering (N distinct base regions, CI-wired execution differential) had been shipping — the v0.51 understatement class.
6. Honest-summary "open residuals" examples cited two closed issues; now cite the actually-open GI-FPU-002 + RA tail is now the ONLY gate between the falcon cascade and the M7 — 5 entry-point symbols; phase-2 D-register pressure is new in v0.52 (inline-f64 #869 lowering) #881/RV32 (0.52.0): two real-driver fixtures still decline — BrTable unsupported, and an undefined label Lend0 in i2c_step #882/range-realloc: segment-local liveness treats cross-barrier live-ins as dead — unmodeled (reg_effect=None) readers after the segment are invisible, and the segment validator shares the blind spot (accepted a wrong rewrite) #872.

Remaining unpinned load-bearing prose (reported, not pinned — candidates for follow-up): the A32 "221-variant no-wildcard tripwire" hand-carried number; the RV32 #871 relocation/arity-marshalling sentence; per-row f32/f64 "Complete" wording (README analogue is pinned); issue-number open-state citations have no offline check (a closed issue cited as open only reddens when its phrase is pinned).

Gates

• claim_check 34/34 (incl. staleness re-render), model_coverage_audit --check ok, ci.yml parses
• frozen_codegen_bytes 10/10 — lane is byte-invisible to codegen
• gpio oracle green (75/75, non-vacuous), rv32 RV32: active data-segment initializers are silently dropped — ship them (linker-script placement + startup copy) and hard-decline until then #798 boot oracle green, both locally with the fresh worktree binary
• fmt clean; workspace tests + clippy running at PR time (no Rust code touched — Python/YAML/docs only)

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!