docs(rivet): #494 proof-carrying design + VCR-SEL-001 first-increment scope (#242)

[avrabe]

Design/rivet artifacts only — no code files touched, so the frozen anchors (control_step 0x00210A55, flat+inlined flight_algo 0x07FDF307, divseam) are trivially safe by construction (stated, not run). Two rivet-traced designs in artifacts/verified-codegen-roadmap.yaml, each with a design doc under docs/design/ (the repo's convention, sibling of vcr-ra-allocator-wiring.md).

1. VCR-PERF-002 (new sw-req, proposed) — proof-carrying specialization (#494 part (a))

The below-native lever: gale measured the floor (pulseengine/gale#121, gust_floor_bench, qemu -icount) — eliding gust_mix's dead clamp under a proven ch∈[524,1524] is 0.45× of native LLVM (0.825 → 0.225 ticks/call), past the 0.70× target, a lowering LLVM structurally cannot reach.

• What loom forwards (loom#231/loom#240 contract): wsc.facts custom section — value-range, shift-bound, divisor-nonzero, in-bounds, disjointness, select-totality — keyed by (fn index, value id); unknown kinds ignored, facts-absent compile byte-identical by construction.
• How synth consumes them: as premises, never re-proved — each elision carries a per-elision obligation discharged pre-emission by the ordeal-backed validator (Adopt ordeal (pure-Rust QF_BV) in synth-verify; demote Z3 to differential oracle, then drop static-link-z3 #553/feat(verify): ordeal 0.4 solver backend behind a thin trait — Z3 demoted to differential oracle (#553) #595): UNSAT(P ∧ general ≠ specialized), certificate-checked; Sat/Unknown ⇒ loud decline to the general lowering.
• Oracle strategy: every elision certificate-logged and differential-gated (wasmtime + unspecialized build, over the proven bound and only over it — the exit-coded soundness gate from gale's bench); SYNTH_FACT_SPEC default-off; no frozen fixture carries facts ⇒ lever can't fire on them.
• Phasing: fact ingestion (codegen-neutral) → single-elision prototype (value-range ⇒ dead clamp branch) → gale measurement on gust_floor_bench + STM32F100 DWT vs the 0.45× floor; kill-criterion unchanged from Beyond parity: proof-carrying specialization + optimal-alloc to BEAT LLVM (0.7× target) #494 (<1.0× then ≤0.70×, bit-identical under the bound).

Design doc: docs/design/proof-carrying-specialization.md.

2. VCR-SEL-001 (updated, status stays approved) — first-increment scope

Concretizes the next big Track-A rivet from the 2026-06-20 pilot (VcrSelPilot.v, 7 Qed):

• Op families first: the tier-A no-scratch i32 ALU six (add/sub/mul/and/or/xor — measured 6/6 auto-discharge) + i32.rotl as the deliberate side-condition-carrying stretch (rs<>rn hypothesis). Div/rem excluded (VCR-ISA-001-gated); optimized path excluded.
• Coexistence: checked-in rule table + committed generated Rust; select_default keeps dispatch — migrated arms delegate behind SYNTH_SEL_DSL (default off, OFF ≡ baseline byte-identical); the exhaustive WasmOp match stays.
• Rocq obligation per rule: one universally-quantified T1 Qed per rule (synth_binop_proof_poly), 1:1 rule↔theorem naming, coverage check fails the //coq build if a rule lacks its proof.
• Frozen anchors gate the flip: per-op mirror-pinning byte-equality (the test(vcr-oracle): estimator↔encoder agreement oracle for the optimized path (#498, #242) #511/test(vcr-ra): reg_effect ↔ rewrite_op def/use consistency oracle (#242) #513 pattern) first, then SYNTH_SEL_DSL=1 must keep all frozen fixtures bit-identical + full differential green — increment 1 migrates structure, never bytes.

Design doc: docs/design/vcr-sel-001-first-increment.md.

Gate

• rivet validate (0.23.0): non-xref ERROR count 0 (exact CI formula), identical to baseline; the 51 pre-existing errors are all filtered cross-repo refs; the one new WARN is the standard not-yet-verified notice every proposed sw-req sibling carries. rivet coverage exit 0.
• Files touched: artifacts/verified-codegen-roadmap.yaml, docs/design/proof-carrying-specialization.md, docs/design/vcr-sel-001-first-increment.md — artifacts/docs only.

Refs #494, #242, pulseengine/loom#240, pulseengine/loom#231.

🤖 Generated with Claude Code

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!