Skip to content

feat(VCR-ISA-001): extend generate-not-mirror Rocq ISA model to nine i64 pseudo-ops (41→50) #773

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
avrabe merged 2 commits into from
Jul 15, 2026
Merged

feat(VCR-ISA-001): extend generate-not-mirror Rocq ISA model to nine i64 pseudo-ops (41→50) #773

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
cf6a7db
feat(VCR-ISA-001): extend generate-not-mirror Rocq ISA model to nine …
avrabe Jul 15, 2026
be9e6cb
docs(VCR-ISA-001): bump DSL rule + Qed counts for the nine i64 pseudo…
avrabe Jul 15, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions CLAUDE.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,8 +89,8 @@ cd coq && make proofs

### Proof Status

See `coq/STATUS.md` for the complete coverage matrix. Current: 476 Qed / 5 Admitted
(+2 `admit.` tactics) across `coq/Synth/`. The 41 selector-DSL rule theorems
See `coq/STATUS.md` for the complete coverage matrix. Current: 485 Qed / 5 Admitted
(+2 `admit.` tactics) across `coq/Synth/`. The 50 selector-DSL rule theorems
(`VcrSelRules.v`) are stated directly about the GENERATED model (VCR-ISA-001
#667: `rule_X := Gen.rule_X`, single source `VcrSelRulesGenerated.v` emitted
from the shipped `sel_dsl::RULES`); the former 40-lemma `VcrSelRulesGenCheck.v`
Expand Down Expand Up @@ -127,18 +127,18 @@ frozen and oracle-gated every step:
- **Track A (core):** `VCR-RA-001` allocator with Belady spilling — **verified,
default-on since v0.24.0** (`SYNTH_SPILL_REALLOC`; `SYNTH_SPILL_ON_EXHAUST`
built flag-off, silicon-gated #580). Next: `VCR-SEL-001` Rocq-discharged
verified selector DSL (increments 1–4 shipped **default-on**, 41 rules / 41 Qed,
verified selector DSL (increments 1–4 shipped **default-on**, 50 rules / 50 Qed,
`SYNTH_SEL_DSL`; the Rocq-proved rules are the SHIPPED lowering path for their
41 covered ops, opt-out `SYNTH_NO_SEL_DSL=1`, byte-invisible flip) and
50 covered ops, opt-out `SYNTH_NO_SEL_DSL=1`, byte-invisible flip) and
`VCR-PERF-002` proof-carrying specialization (#494,
0.45× floor; phase 1 facts ingestion landed, PR #624).
- **Track B (semantics):** `VCR-ISA-001` Sail-generated Rocq ISA model —
approved, Sail/ASL bridge spike landed (92 Qed, `coq/Synth/ARM/SailArmBridge.v`);
"generate, don't mirror" landed (#667): the shipped `sel_dsl::RULES` table
EMITS the 41 covered ops' Rocq lowerings
EMITS the 50 covered ops' Rocq lowerings
(`coq/Synth/Synth/VcrSelRulesGenerated.v`, `Module Gen`), and `VcrSelRules.v`
DEFINES `rule_X := Gen.rule_X` — the generated file is the single model
source, the 41 correctness Qed are stated directly about it, and a
source, the 50 correctness Qed are stated directly about it, and a
selector-table change regenerates `Gen` and breaks the matching proof, so the
#682 model↔selector drift is unrepresentable at the instruction-sequence level
for those ops (the interim `VcrSelRulesGenCheck.v` reflexivity gate was
Expand Down
12 changes: 6 additions & 6 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -109,7 +109,7 @@ synth verify examples/wat/simple_add.wat firmware.elf
| ELF output with vector table | Implemented | Thumb bit set on symbols; not linked on real hardware |
| Linker scripts (STM32, nRF52840, generic) | Implemented | Generated, not tested with real boards |
| Cross-compilation (`--link` flag) | Implemented | Requires `arm-none-eabi-gcc` in PATH; not CI-tested |
| Rocq mechanized proofs | 476 Qed / 5 Admitted | i32 + i64 T1 correctness proofs; the 41 selector-DSL rule theorems are stated directly about the GENERATED model (VCR-ISA-001 #667 — `rule_X := Gen.rule_X`, single source `VcrSelRulesGenerated.v`); all four i32 div/rem trap guards discharged against the branch-taking executor (#73) |
| Rocq mechanized proofs | 485 Qed / 5 Admitted | i32 + i64 T1 correctness proofs; the 50 selector-DSL rule theorems are stated directly about the GENERATED model (VCR-ISA-001 #667 — `rule_X := Gen.rule_X`, single source `VcrSelRulesGenerated.v`); all four i32 div/rem trap guards discharged against the branch-taking executor (#73) |
| SMT translation validation | ordeal (pure-Rust QF_BV) default | v0.27.0 (#553); Z3 demoted to feature-gated differential oracle — 141/141 agreement |
| WebAssembly spec test suite | 227/257 compile | Compilation only — not executed on emulator |

Expand Down Expand Up @@ -194,7 +194,7 @@ Per the [PulseEngine Verification Guide](https://pulseengine.eu/guides/VERIFICAT

| Track | Status | Coverage |
|-------|--------|----------|
| **Rocq** | Partial | 476 Qed / 5 Admitted (41 selector-DSL rule theorems stated directly about the GENERATED model, VCR-ISA-001 #667) — all four i32 div/rem trap guards discharged (#73) |
| **Rocq** | Partial | 485 Qed / 5 Admitted (50 selector-DSL rule theorems stated directly about the GENERATED model, VCR-ISA-001 #667) — all four i32 div/rem trap guards discharged (#73) |
| **Kani** | Starting | 18 bounded model checking harnesses for ARM encoder |
| **Verus** | Starting | 8 spec functions in `synth-synthesis/src/contracts.rs`; Bazel integration via `rules_verus` |
| **Lean** | Not started | — |
Expand All @@ -206,14 +206,14 @@ See `artifacts/verification-gaps.yaml` for the detailed gap analysis (VG-001 thr
Mechanized proofs in Rocq 9 show that `compile_wasm_to_arm` preserves WASM semantics for each operation. The proof suite lives in `coq/Synth/` and covers ARM instruction semantics, WASM stack-machine semantics, and per-operation correctness theorems.

```
476 Qed / 5 Admitted (+2 admit. tactics) [CI-gated: claims.yaml + scripts/claim_check.py]
485 Qed / 5 Admitted (+2 admit. tactics) [CI-gated: claims.yaml + scripts/claim_check.py]
T1 result-correspondence (ARM output = WASM result): all i32 ops and all
i64 ops — i64 T1 parity since v0.11.0, 0 i64 admits (coq/STATUS.md)
T2 existence-only: f32/f64 and remaining categories
T3 admitted (5): 2 Compilation.v, 1 CorrectnessSimple.v, 2 ArmRefinement.v
(0 division admits — all four i32 div/rem trap guards discharged against
exec_program_br, #73 closed at i32)
incl. 41 Qed selector-DSL rule theorems (Synth/VcrSelRules.v, 1:1 with
incl. 50 Qed selector-DSL rule theorems (Synth/VcrSelRules.v, 1:1 with
coq/vcr_sel_rules.manifest) — stated directly about the GENERATED model
(VCR-ISA-001 #667: rule_X := Gen.rule_X, single source
Synth/VcrSelRulesGenerated.v emitted from the shipped sel_dsl::RULES, so
Expand Down Expand Up @@ -262,10 +262,10 @@ The one-sentence version: moving synth's correctness from *"we patched every bug

| Track | Item | What it does | Status |
|-------|------|--------------|--------|
| **A — codegen core** | `VCR-SEL-001` | Rocq-discharged verified selector DSL — *"ISLE with a proof-assistant backend"*; a missing lowering rule becomes an enumerable coverage gap, not a silent miscompile | increments 1–4 shipped default-on (`SYNTH_SEL_DSL`, opt-out `SYNTH_NO_SEL_DSL=1`): 41 rules / 41 Qed theorems in `coq/Synth/Synth/VcrSelRules.v` (1:1 with `coq/vcr_sel_rules.manifest`, coverage-gated), plus 7 Qed pilot lemmas in `coq/Synth/Synth/VcrSelPilot.v`; the DSL is now the SHIPPED lowering path for its 41 covered ops (byte-invisible flip — every rule was mirror-pinned byte-identical to the hand-written arm it replaces, frozen anchors unmoved) |
| **A — codegen core** | `VCR-SEL-001` | Rocq-discharged verified selector DSL — *"ISLE with a proof-assistant backend"*; a missing lowering rule becomes an enumerable coverage gap, not a silent miscompile | increments 1–4 shipped default-on (`SYNTH_SEL_DSL`, opt-out `SYNTH_NO_SEL_DSL=1`): 50 rules / 50 Qed theorems in `coq/Synth/Synth/VcrSelRules.v` (1:1 with `coq/vcr_sel_rules.manifest`, coverage-gated), plus 7 Qed pilot lemmas in `coq/Synth/Synth/VcrSelPilot.v`; the DSL is now the SHIPPED lowering path for its 50 covered ops (byte-invisible flip — every rule was mirror-pinned byte-identical to the hand-written arm it replaces, frozen anchors unmoved) |
| | `VCR-PERF-002` | Proof-carrying specialization (#494): loom's `wsc.facts` invariants become premises for per-elision proof obligations, certificate-checked by the ordeal-backed validator — toward gale's measured **0.45× (below-native) floor** | design traced (v0.30.0); phase 1 (facts ingestion) landed ([PR #624](https://github.com/pulseengine/synth/pull/624), v0.31.0) |
| | `SYNTH_SPILL_ON_EXHAUST` | Replace the register-exhaustion decline with allocation-time Belady spilling (#580) — the last piece of the exhaustion hard-fail | built, flag-off; default-on held for silicon cycle numbers |
| **B — authoritative semantics** | `VCR-ISA-001` | Re-base ARM/RISC-V semantics on Sail-generated Rocq (the official ISA spec); generate the selector model, don't mirror it (#667) | approved — Sail/ASL bridge spike landed (92 Qed, `coq/Synth/ARM/SailArmBridge.v`); #667 "generate, don't mirror" landed: the shipped `sel_dsl::RULES` table emits the 41 covered ops' Rocq lowerings (`coq/Synth/Synth/VcrSelRulesGenerated.v`), and `VcrSelRules.v` DEFINES `rule_X := Gen.rule_X` — the generated file is the single model source, the 41 correctness Qed are stated directly about it, and a selector-table change breaks the matching proof (no hand-written copy left to drift) |
| **B — authoritative semantics** | `VCR-ISA-001` | Re-base ARM/RISC-V semantics on Sail-generated Rocq (the official ISA spec); generate the selector model, don't mirror it (#667) | approved — Sail/ASL bridge spike landed (92 Qed, `coq/Synth/ARM/SailArmBridge.v`); #667 "generate, don't mirror" landed: the shipped `sel_dsl::RULES` table emits the 50 covered ops' Rocq lowerings (`coq/Synth/Synth/VcrSelRulesGenerated.v`), and `VcrSelRules.v` DEFINES `rule_X := Gen.rule_X` — the generated file is the single model source, the 50 correctness Qed are stated directly about it, and a selector-table change breaks the matching proof (no hand-written copy left to drift) |
| | `VCR-WASM-001` | Anchor WASM source semantics on WasmCert-Coq | proposed |
| **Gate** | `VCR-VER-001` | Success = a previously load-bearing greedy-fix becomes *revertable*, with the full differential bit-identical and cycles equal-or-better | **demonstrated** (implemented; [evidence](scripts/repro/vcr_ver_001_gate.md)): the v0.11.20 reciprocal-mult cost-gate deleted outright (PR #322, bit-identical); the #496 exhaustion decline revertable behind `SYNTH_SPILL_ON_EXHAUST` — red case green, anchors byte-identical, declines 14→8; flip held on a measured i32-shape cycle regression |

Expand Down
28 changes: 14 additions & 14 deletions claims.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,16 +29,16 @@ claims:
# ---------------------------------------------------------------------------
- id: SYNTH-PROOF-COUNT-README
doc: README.md
text: "476 Qed / 5 Admitted"
text: "485 Qed / 5 Admitted"
evidence:
- kind: count-eq # ALL THREE README spots must agree —
pattern: '476 Qed / 5 Admitted' # a verbatim check alone greens if one
pattern: '485 Qed / 5 Admitted' # a verbatim check alone greens if one
glob: ['README.md'] # of them drifts while another matches
expect: 3
- kind: count-eq
pattern: 'Qed\.'
glob: ['coq/Synth/**/*.v']
expect: 476
expect: 485
- kind: count-eq
pattern: 'Admitted\.'
glob: ['coq/Synth/**/*.v']
Expand All @@ -50,29 +50,29 @@ claims:

- id: SYNTH-PROOF-COUNT-CLAUDE-MD
doc: CLAUDE.md
text: "476 Qed / 5 Admitted"
text: "485 Qed / 5 Admitted"
evidence:
- kind: count-eq
pattern: 'Qed\.'
glob: ['coq/Synth/**/*.v']
expect: 476
expect: 485
- kind: count-eq
pattern: 'Admitted\.'
glob: ['coq/Synth/**/*.v']
expect: 5

- id: SYNTH-PROOF-COUNT-STATUS-MD
doc: coq/STATUS.md
text: "476 Qed / 5 Admitted"
text: "485 Qed / 5 Admitted"
evidence:
- kind: count-eq # headline + Total line must both agree
pattern: '476 Qed / 5 Admitted'
pattern: '485 Qed / 5 Admitted'
glob: ['coq/STATUS.md']
expect: 2
- kind: count-eq
pattern: 'Qed\.'
glob: ['coq/Synth/**/*.v']
expect: 476
expect: 485
- kind: count-eq
pattern: 'Admitted\.'
glob: ['coq/Synth/**/*.v']
Expand Down Expand Up @@ -240,31 +240,31 @@ claims:
# ---------------------------------------------------------------------------
- id: SYNTH-SEL-DSL-RULES
doc: README.md
text: "41 rules / 41 Qed theorems"
text: "50 rules / 50 Qed theorems"
evidence:
- kind: count-eq # rules in the manifest
pattern: '^rule_'
glob: ['coq/vcr_sel_rules.manifest']
expect: 41
expect: 50
- kind: count-eq # 1:1 Qed theorems in VcrSelRules.v
pattern: '^(?:Theorem|Lemma) rule_\w+_correct'
glob: ['coq/Synth/Synth/VcrSelRules.v']
expect: 41
expect: 50
- kind: count-max # the rule table carries no admits
pattern: 'Admitted\.'
glob: ['coq/Synth/Synth/VcrSelRules.v']
max: 0

- id: SYNTH-SEL-DSL-COVERAGE-STATUS-MD
doc: coq/STATUS.md
text: "**41 (26%)**" # DSL-served column total, per-op-family table (#667)
text: "**50 (32%)**" # DSL-served column total, per-op-family table (#667)
evidence:
- kind: count-eq
pattern: '^rule_'
glob: ['coq/vcr_sel_rules.manifest']
expect: 41
expect: 50
- kind: verbatim
text: "**41 Qed / 0 Admitted**"
text: "**50 Qed / 0 Admitted**"

- id: SYNTH-SEL-DSL-PILOT
doc: README.md
Expand Down
28 changes: 15 additions & 13 deletions coq/STATUS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Rocq Proof Suite — Honest Status

**Last Updated: 2026-07-15 (recount: 476 Qed / 5 Admitted, +2 admit., crude
**Last Updated: 2026-07-15 (recount: 485 Qed / 5 Admitted, +2 admit., crude
`grep "Qed\."` over `coq/Synth/**/*.v` — same method as prior recounts; the
-40 vs the prior 512 are the retired VCR-ISA-001 #667 cross-check lemmas of
`VcrSelRulesGenCheck.v`: `VcrSelRules.v` now DEFINES every `rule_X` as the
Expand Down Expand Up @@ -167,7 +167,7 @@ and predates the VcrSelRules (42), VcrSelPilot (7) and SailArmBridge (92) Qed;
see the per-file breakdown below for current per-file counts. The T3 row and
the headline total are re-derived by the claim gate.

**Total: 476 Qed / 5 Admitted (+2 admit.) across all files** (recount 2026-07-15, CI-gated via `claims.yaml`)
**Total: 485 Qed / 5 Admitted (+2 admit.) across all files** (recount 2026-07-15, CI-gated via `claims.yaml`)

v0.10.0 PR 1: +2 T1 Qed (i64_add_correct, i64_sub_correct) and +9
infrastructure Qed (combine_i32_unsigned, carry_split_add,
Expand Down Expand Up @@ -485,7 +485,7 @@ stepped proof closing with `I32.clz_rbit`;
tier: the encoder's CMP-lo/SBCS-hi expansion is below the flat executor,
see `docs/design/vcr-sel-001-increment-4.md`).

**41 Qed / 0 Admitted**, same T1 bound as the pilot ("the ARM sequence
**50 Qed / 0 Admitted**, same T1 bound as the pilot ("the ARM sequence
computes the named result", not WASM refinement). These 48 Qed (pilot +
rules) are included in the recount above.

Expand Down Expand Up @@ -522,9 +522,9 @@ Every op family the shipped ARM selectors lower, as of increment 4
| i32.const | 1 | 0 | 1 | 0 |
| i64 pair ALU (add/sub/and/or/xor) | 5 | **5** | 0 | 0 |
| i64 comparisons (eqz + eq..ge_u) | 11 | **11**¹ | 0 | 0 |
| i64 mul/div/rem | 4 | 0 | 4 | 0 |
| i64 shifts/rotates (pair pseudo-ops) | 5 | 0 | 5 | 0 |
| i64 bit-manip (clz/ctz/popcnt) | 3 | 0 | 3 | 0 |
| i64 mul/div/rem | 4 | **1** | 3 | 0 |
| i64 shifts/rotates (pair pseudo-ops) | 5 | **5**¹ | 0 | 0 |
| i64 bit-manip (clz/ctz/popcnt) | 3 | **3**¹ | 0 | 0 |
| i64 wrap/extend (wrap_i64, extend_i32_s/u) | 3 | 0 | 3 | 0 |
| i64 sign-extend (extend8/16/32_s) | 3 | 0 | 0 | 3 |
| i64.const | 1 | 0 | 1 | 0 |
Expand All @@ -535,13 +535,15 @@ Every op family the shipped ARM selectors lower, as of increment 4
| locals/globals (get/set/tee) | 5 | 0 | 5 | 0 |
| parametric (drop/select/nop) | 3 | 0 | 3 | 0 |
| control flow (block/loop/br/br_if/return/call/…) | ~10 | 0 | 0 | ~10 |
| **Total (≈)** | **155** | **41 (26%)** | **95 (61%)** | **19 (12%)** |

¹ pseudo-op tier: `popcnt`, `i64.eqz` and the ten binary i64 comparisons are
proven at the `ArmOp` pseudo-op boundary (the selector's emission, which is
what the DSL owns); the encoder expansions below that boundary
(shift-and-add popcnt, the CMP-lo/SBCS-hi chain) are covered by the
differential oracles, not Rocq — see `docs/design/vcr-sel-001-increment-4.md`.
| **Total (≈)** | **155** | **50 (32%)** | **86 (55%)** | **19 (12%)** |

¹ pseudo-op tier: `i32.popcnt`, `i64.eqz`, the ten binary i64 comparisons, and
the VCR-ISA-001 wave-2 i64 shapes (`clz`/`ctz`/`popcnt`, `mul`/`shl`/`shr_u`/
`shr_s`, `rotl`/`rotr`) are proven at the `ArmOp` pseudo-op boundary (the
selector's emission, which is what the DSL owns); the encoder expansions below
that boundary (shift-and-add popcnt, the CMP-lo/SBCS-hi chain, the funnel-shift
and UMULL+MLA sequences) are covered by the differential oracles, not Rocq —
see `docs/design/vcr-sel-001-increment-4.md`.
² the 4 i32 div/rem model proofs are the T3 trap-guard admits (#73,
`BCondOffset` executor gap).
³ the f32/f64 model rows ride the 21 VFP axioms; the shipped ARM path
Expand Down
Loading
Loading