diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 5bbf5beb..d0406e86 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -342,6 +342,41 @@ artifacts: (select_default / select_with_stack / optimizer_bridge) into one verified source; and (iii) cross-backend op-parity — the concrete near-term increment, tracked as VCR-SEL-005 below. + + FIRST INCREMENT SCOPE (2026-07-03, docs/design/vcr-sel-001-first-increment.md): + (1) OP FAMILIES: exactly the pilot's tier-A no-scratch single-instruction + i32 ALU class — Add/Sub/Mul/And/Or/Xor, the measured 6/6 auto-discharge + set — plus, as the increment's stretch (proves the DSL can carry side + conditions), ONE scratch-using shape (i32.rotl: RSB scratch + ROR) with + the explicit rs<>rn non-aliasing hypothesis. Excluded from increment 1: + trap-guarded div/rem (Admitted upstream, gated on VCR-ISA-001's real + control-flow executor), i64 pairs, memory, control flow, and everything + the optimized path (select_with_stack/optimizer_bridge) does — the DSL + targets select_default's arms only. + (2) COEXISTENCE: the DSL is a checked-in rule table + (declarative op -> parameterized ARM sequence) + a generator emitting + plain Rust lowering fns committed to the tree (reviewable, no build-time + magic); select_default KEEPS dispatch ownership — a migrated op's match + arm delegates to the generated rule behind SYNTH_SEL_DSL (default off), + unmigrated arms untouched. OFF ≡ baseline byte-identical by construction. + (3) ROCQ OBLIGATION PER RULE: one universally-quantified T1 theorem per + rule in the VcrSelPilot.v form — forall rd rn rm (+ scratch hypotheses + where the shape needs them), exec of the rule's emitted sequence yields + the op's I32 semantics in rd — auto-discharged by synth_binop_proof_poly; + rule<->theorem naming is 1:1 and a coverage check fails the //coq build + if a rule lacks its Qed (a rule without a theorem cannot merge). + (4) FROZEN-ANCHOR GATE for the flip: per-op mirror-pinning first (the + #511/#513 pattern — a test lowers the probe set through BOTH the + hand-written arm and the generated rule and asserts byte-equality, so the + two must-agree implementations are pinned before any flip); then + SYNTH_SEL_DSL=1 must keep control_step 0x00210A55, flat+inlined + flight_algo 0x07FDF307, and divseam bit-identical (the generated rules + reproduce the current lowering EXACTLY — increment 1 migrates structure, + never bytes); only then may the flag default flip, one op-class per + release, full differential green. Success criterion for increment 1: the + six ALU arms + rotl are served from the DSL with their seven Qed theorems, + fixtures bit-identical, and deleting a hand-written arm body becomes a + no-op — the first structural (not additive) step of the migration. status: approved tags: [codegen, selector, isle, verified-dsl, rocq, track-a, novel, release-v0.12.1] links: @@ -1531,6 +1566,95 @@ artifacts: before/after; no frozen fixture changes a byte except via a deliberate, gale-confirmed re-freeze. + - id: VCR-PERF-002 + type: sw-req + title: "Proof-carrying specialization: consume loom wsc.facts premises to elide proven-dead guards (beat-LLVM, #494)" + description: > + DESIGN (2026-07-03, docs/design/proof-carrying-specialization.md; GitHub + #494 part (a), loom#240/loom#231 fact-passing contract, epic #242). + The below-native lever: gale measured the floor on gust_floor_bench + (gale PR pulseengine/gale#121, qemu -icount, re-run-identical) — eliding + gust_mix's dead clamp under a proven ch∈[524,1524] takes it from 0.825 to + 0.225 ticks/call = 0.45x of native LLVM, past the 0.70x target, a lowering + LLVM structurally cannot reach because it never had the bound. The span to + capture is 0.825 -> 0.225 (3.7x) on that one function; the enabling + information exists only in the verified pipeline (closed fused module + + machine-checked invariants). + + WHAT LOOM FORWARDS (the loom#231 contract; loom is the PROVER): a custom + section `wsc.facts` (sibling of wsc.transformation.attestation) carrying + invariants loom's validator already discharges, keyed by (function index, + value identification): value-range (v ∈ [lo,hi]), shift-bound (<32/<64), + divisor-nonzero, in-bounds access, memory disjointness, select-totality. + Fail-safe skew rule (loom#231 Q4): synth IGNORES unknown fact kinds and a + missing/unparseable section entirely — facts are optional accelerators, + and the facts-absent compile is byte-identical to today's baseline BY + CONSTRUCTION. + + HOW SYNTH CONSUMES THEM (synth is a CONDITIONAL optimizer, not a + re-prover): each fact becomes a premise available at selection time; a + specialization (dead clamp-branch elision first; later bounds-check / + trap-guard / mask-materialization elision) fires only with a PER-ELISION + PROOF OBLIGATION discharged before emission by the ordeal-backed + translation validator (#553/#595: certificate-checked QF_BV behind the + BvSolver trait, no C++ toolchain): assert the premise P as a hypothesis + and check general_lowering ≢ specialized_lowering under P is UNSAT — + certificate-checked, so the elision carries evidence, not trust in a + heuristic. Unknown/Sat/conflict-budget-exceeded => DECLINE loudly and emit + the general lowering (conservative; never a silent wrong-code path). + Trust split (loom#231 Q3): synth does NOT re-derive loom's fact — it + proves the conditional correctness of its OWN transformation given the + fact; fact validity stays loom's obligation (Z3 translation validation + upstream), attested via the existing wsc attestation channel. + + ORACLE STRATEGY (every elision gated twice): (1) certificate — the + per-elision ordeal obligation above, logged per function; (2) differential + — the specialized build must be result-identical to BOTH wasmtime and the + unspecialized synth build over the proven bound (and ONLY over the bound — + that side-condition IS the contract, exit-coded exactly like gale's + gust_floor_bench soundness gate mix_proven ≡ mix_native ≡ gust_mix on + [524,1524]). Frozen fixtures carry no wsc.facts section, so every frozen + anchor is bit-identical trivially; the lever is additionally flag-gated + (SYNTH_FACT_SPEC, default off) until gale confirms on silicon. + + PHASING (each phase its own oracle-gated PR): + Phase 1 — fact ingestion: parse wsc.facts, thread premises to + CompileConfig/selector, ZERO codegen change (byte-identical, frozen-safe); + schema versioned, unknown-kind-tolerant. + Phase 2 — single-elision prototype: value-range => dead conditional-branch + elision (the gust_mix clamp shape), flag-gated, per-elision validator + obligation + in-bounds differential red/green oracle. + Phase 3 — measurement vs the 0.45x floor: gale re-measures gust_mix on + gust_floor_bench (qemu -icount) and STM32F100 silicon (DWT CYCCNT); + kill-criterion unchanged from #494: shipped dissolved lane <1.0x then + <=0.70x vs native LLVM, bit-identical under the proven bound. The measured + floor (0.45x) gives the target 0.25x of headroom — if the productized + elision cannot land inside it, the premise-to-selector plumbing (not the + idea) is at fault and the phase re-plans. + status: proposed + tags: [codegen, perf, proof-carrying, specialization, wsc-facts, loom-integration, ordeal, beat-llvm, synth-494, gale-121] + links: + - type: derives-from + target: VCR-001 + - type: traces-to + target: VCR-PERF-001 + fields: + req-type: functional + priority: should + verification-criteria: > + Phase 1: a module with a wsc.facts section compiles byte-identical to + the same module with the section stripped (ingestion is codegen-neutral); + malformed/unknown-kind sections are ignored with a diagnostic, never an + error. Phase 2: each fired elision has (a) an ordeal certificate for + "general ≡ specialized under premise" logged per function and (b) a + differential PASS (wasmtime + unspecialized-build agreement) over the + proven bound; Unknown/Sat declines to the general lowering; all frozen + fixtures bit-identical (no facts => lever cannot fire); SYNTH_FACT_SPEC=0 + is byte-identical to baseline. Phase 3 (kill-criterion, gale-measured): + gust_mix on gust_floor_bench + STM32F100 DWT reaches <1.0x then <=0.70x + vs native LLVM with the soundness gate green; below-target after the + single-elision prototype => re-plan before widening fact kinds. + # --------------------------------------------------------------------------- # gale-proposed (issue #290, 2026-06-10): scry consumption at two trust levels # --------------------------------------------------------------------------- diff --git a/docs/design/proof-carrying-specialization.md b/docs/design/proof-carrying-specialization.md new file mode 100644 index 00000000..02c7cab7 --- /dev/null +++ b/docs/design/proof-carrying-specialization.md @@ -0,0 +1,115 @@ +# VCR-PERF-002 — Proof-carrying specialization design (#494) + +Status: **design** (no code yet). Tracks `VCR-PERF-002` in +`artifacts/verified-codegen-roadmap.yaml`, epic #242, GitHub #494 part (a). +Cross-repo contract: loom#240 / loom#231 (`wsc.facts`), gale PR +pulseengine/gale#121 (`gust_floor_bench`, the measured floor). + +## Why this document + +gale measured the payoff before we built anything: under qemu `-icount` +(deterministic, re-run-identical), three lowerings of `gust_mix` over the same +proven-range inputs: + +| lowering | fn-only ticks/call | ratio vs native | +|---|---|---| +| native (LLVM, full clamp) | 0.50 | 1.00× | +| dissolved today (synth ≥0.15.1) | 0.825 | 1.65× (in-range) | +| **proof-carrying floor** (`add #476` only) | **0.225** | **0.45×** | + +`gust_mix` is algebraically `clamp(ch+476, 1000, 2000)`. A composition that +proves `ch ∈ [524,1524]` makes **both clamp branches dead**; the function +collapses to `add r0, #476; bx lr`. LLVM never emits that — it never had the +bound. The bound exists only in the verified pipeline: meld fuses a closed +world, loom's validator + gale's Verus/Rocq/Kani primitives prove the ranges. +The design question is purely how the fact travels and how synth is allowed to +act on it *soundly*. Target: **≤0.70× of native**, kill-criterion per #494. + +## The contract (what loom forwards) + +Per loom#231: a custom section **`wsc.facts`** (sibling of +`wsc.transformation.attestation`), carrying invariants loom's Z3 translation +validator already discharges, keyed by `(function index, value id)`. Fact +kinds, in silicon-payoff order: + +1. **value-range** — `v ∈ [lo, hi]` (drives the clamp elision above) +2. **shift-bound** — shift amount `< 32`/`< 64` (bare `lsl/lsr`, no mask) +3. **divisor-nonzero** — drop the `div/rem` trap guard +4. **in-bounds access** — drop a bounds check +5. **select-totality** — branchless `IT` (pairs with VCR-SEL-004) +6. **memory disjointness** — keep values in registers across stores + +**Fail-safe skew rule (loom#231 Q4):** synth ignores unknown fact kinds, and a +missing or unparseable section entirely. Facts are optional accelerators. The +facts-absent compile is **byte-identical to today's baseline by construction** +— which is also why every frozen fixture (none carries the section) stays +bit-identical trivially at every phase. + +**Trust split (loom#231 Q3):** loom is the *prover* — fact validity is +loom's obligation, discharged by its validator and attested through the +existing `wsc` attestation channel. synth is a *conditional optimizer* — it +never re-derives the fact; it proves the conditional correctness of its **own +transformation given the fact** (next section). A forged fact is a contract +violation upstream, not a synth soundness hole: synth's certificate says +"correct **under P**", exactly the side-condition gale's bench encodes. + +## How synth consumes facts: the per-elision proof obligation + +Every specialization fires only after a machine-checked, per-site obligation, +discharged **before emission** by the ordeal-backed translation validator +(#553 / PR #595 — certificate-checked pure-Rust QF_BV behind the `BvSolver` +trait, so this runs on every dev machine and in CI with no C++ toolchain): + +``` +premise P (the wsc.facts invariant, asserted as a hypothesis) +obligation UNSAT( P ∧ (general_lowering(x) ≠ specialized_lowering(x)) ) +``` + +- **UNSAT (certificate-checked)** → the elision is admitted; the certificate is + logged per function (the evidence trail, not trust in a heuristic). +- **Sat / Unknown / conflict-budget exceeded** → **decline loudly**, emit the + general lowering. There is no silent wrong-code path; the conservative + fallback is today's codegen. + +This is deliberately the same shape as the existing translation-validation +flow — the premise is the only new ingredient. `SYNTH_ORDEAL_MAX_CONFLICTS` +bounds adversarial queries to a clean conservative decline. + +## Oracle strategy (every elision gated twice) + +1. **Certificate** — the per-elision ordeal obligation above. +2. **Differential** — the specialized build must be result-identical to BOTH + wasmtime and the unspecialized synth build **over the proven bound, and only + over the bound** (exit-coded, exactly like `gust_floor_bench`'s soundness + gate `mix_proven ≡ mix_native ≡ gust_mix` on `[524,1524]`). Out-of-bound + divergence is *expected and correct* — the bound is the contract. +3. **Frozen anchors** — no facts section on any frozen fixture ⇒ the lever + cannot fire ⇒ bit-identical trivially; additionally flag-gated + (`SYNTH_FACT_SPEC`, default off) until gale confirms on silicon. + +## Phasing (each phase its own oracle-gated PR) + +1. **Fact ingestion** — parse `wsc.facts`, thread premises into + `CompileConfig` / the selector. **Zero codegen change**; byte-identical, + frozen-safe. Schema versioned, unknown-kind-tolerant. Co-designed with + loom's emitter (loom#231 open questions 1/2 resolve here: keying + binary + encoding). +2. **Single-elision prototype** — value-range ⇒ dead conditional-branch + elision (the `gust_mix` clamp shape), behind `SYNTH_FACT_SPEC`, with the + per-elision obligation + a red/green in-bounds differential oracle. +3. **Measurement vs the 0.45× floor** — gale re-measures `gust_mix` on + `gust_floor_bench` (qemu `-icount`) and STM32F100 silicon (DWT CYCCNT). + Kill-criterion (#494, unchanged): shipped dissolved lane **<1.0× then + ≤0.70×** vs native LLVM, bit-identical under the proven bound. The measured + floor gives 0.25× of headroom; if the productized elision can't land inside + it, the premise-to-selector plumbing is at fault and the phase re-plans + before any widening of fact kinds. + +## Non-goals (this requirement) + +- Part (b) of #494 (exhaustive/optimal allocation on small whole-known + functions) — that is VCR-RA territory and independently unblocked. +- loom's algebraic mid-end (`256*x>>8 → x`, loom#240 ask 1) — a loom change; + it shrinks the input but is not fact-passing. +- Fact kinds beyond value-range in the prototype — ordered by silicon payoff + only after Phase 3 reports. diff --git a/docs/design/vcr-sel-001-first-increment.md b/docs/design/vcr-sel-001-first-increment.md new file mode 100644 index 00000000..a9239aff --- /dev/null +++ b/docs/design/vcr-sel-001-first-increment.md @@ -0,0 +1,105 @@ +# VCR-SEL-001 — First increment scope (Rocq-discharged selector DSL) + +Status: **design** (no code yet). Scopes the first wired increment of +`VCR-SEL-001` in `artifacts/verified-codegen-roadmap.yaml`, epic #242. +Evidence base: the pilot measurement `coq/Synth/Synth/VcrSelPilot.v` +(2026-06-20, 7 Qed / 0 Admitted, built green via `//coq:vcr_sel_pilot`). + +## Where the pilot left us + +The go/abandon question — "do the existing tactics still auto-discharge once a +rule is lifted from fixed R0/R1 to universally-quantified registers?" — came +back two-tier: + +- **Tier A (no-scratch, single-instruction i32 binops):** Add/Sub/Mul/And/Or/ + Xor — **6/6 auto-discharge unchanged** (`synth_binop_proof_poly` is verbatim + `synth_binop_proof` modulo the lowering-unfold target). One Qed per op covers + every register aliasing. +- **Tier B (scratch-using shapes):** `i32.rotl` (RSB scratch + ROR) + generalizes but needs an explicit `rs <> rn` non-aliasing hypothesis the DSL + must carry and feed the allocator. +- **Out of reach for now:** trap-guarded div/rem — their fixed-register proofs + are already Admitted, blocked on the flat executor's no-op `BCondOffset` + (VCR-ISA-001), not on register generalization. + +The pilot generated no Rust and replaced no selector arm. The first increment +is exactly that step: **the smallest wiring in which a hand-written arm is +served from a verified rule**, without moving a byte of frozen output. + +## Increment-1 scope + +### 1. Op families + +- **In:** the tier-A six — `i32.add`, `i32.sub`, `i32.mul`, `i32.and`, + `i32.or`, `i32.xor` — plus **one** tier-B shape, `i32.rotl`, included + deliberately so the DSL's rule format carries a scratch non-aliasing side + condition from day one (a DSL that can only express side-condition-free + rules would be a dead end). +- **Out:** div/rem (VCR-ISA-001-gated), i64 pairs, comparisons, shifts-by- + register, memory, control flow, and the optimized path entirely — the DSL + targets `select_default`'s arms only (`select_with_stack` / + `optimizer_bridge` are phase-later; collapsing the selector accretion is + motivation (ii), not increment 1). + +### 2. Coexistence with the hand-written selector + +- The DSL is a **checked-in rule table**: declarative + `op → parameterized ARM sequence` (registers as variables, side conditions + explicit), plus a generator that emits plain Rust lowering functions + **committed to the tree** — reviewable diffs, no build-time codegen magic. +- `select_default` **keeps dispatch ownership**. A migrated op's match arm + delegates to the generated rule behind `SYNTH_SEL_DSL` (default **off**); + unmigrated arms are untouched. `OFF ≡ baseline` byte-identical by + construction — the same landing pattern as every VCR-RA lever. +- The exhaustive `WasmOp` match (no `_ =>` wildcard) stays: compile-checked + coverage remains owned by the compiler, per the 2026-06-20 re-scoping. + +### 3. The Rocq obligation per rule + +One universally-quantified **T1 theorem per rule**, in the `VcrSelPilot.v` +form: + +```coq +Theorem rule_i32_add_correct : forall rd rn rm astate, + exists astate', + exec_program (rule_lowering I32Add rd rn rm) astate = Some astate' /\ + get_reg astate' rd = I32.add (get_reg astate rn) (get_reg astate rm). +``` + +(For `rotl`, with the explicit `rs <> rn` hypothesis.) Discharged by +`synth_binop_proof_poly`; **rule ↔ theorem naming is 1:1** and a coverage +check fails the `//coq` build if any rule lacks its Qed — a rule without a +theorem cannot merge. Honest T1 bound carried over from the pilot: the +theorems prove "the ARM sequence computes the named result", not full WASM +refinement (that upgrade is VCR-WASM-001/VCR-ISA-001 territory). + +### 4. Frozen anchors gate the migration + +Two gates, in order, before any default flip: + +1. **Mirror-pinning per op** (the #511/#513 pattern): a test lowers the probe + set through BOTH the hand-written arm and the generated rule and asserts + **byte-equality**. The two must-agree implementations are pinned before the + flag can matter. Increment 1 migrates *structure, never bytes* — the + generated rules must reproduce the current lowering exactly. +2. **Frozen fixtures under the flag**: `SYNTH_SEL_DSL=1` must keep + `control_step 0x00210A55`, flat+inlined `flight_algo 0x07FDF307`, and + `divseam` bit-identical, plus the full differential green. Only then may + the default flip — one op-class per release, never bundled with a + byte-changing lever. + +## Success criterion for increment 1 + +The six ALU arms + `rotl` are served from the DSL with their seven Qed +theorems; fixtures bit-identical under the flag; and deleting a hand-written +arm body is a no-op. That is the first *structural* (not additive) step of the +VCR-SEL-001 migration — after it, the per-op-class cadence is mechanical: +rule + theorem + mirror-pin + flip. + +## Kill-criterion (unchanged from the artifact) + +≥70% auto-discharge per attempted rule over the pilot class, and bit-for-bit +selector match. Increment 1's class is chosen to be at 100%/100% by +measurement — if even this class cannot wire bit-identically, the DSL +collapses into "CompCert with extra syntax" and the direct-proof path +(the existing T1 tactic suite against `exec_indexed`) wins instead.