feat(verify): validator pattern prototype — CertifiedSelection + Z3 for I32Add (#76)#113
Open
avrabe wants to merge 2 commits into
Open
feat(verify): validator pattern prototype — CertifiedSelection + Z3 for I32Add (#76)#113avrabe wants to merge 2 commits into
avrabe wants to merge 2 commits into
Conversation
…or I32Add Closes the architectural commitment for issue #76 and opens the path toward retiring issue #73's divergent-Rocq-proofs credibility gap. ## Architecture CompCert's certifying-algorithm pattern: don't verify the (NP-hard, heuristic, frequently-changing) instruction selector — verify a small, formally-checkable validator that consumes the selector's output and confirms each concrete selection is semantically equivalent to the WASM op it replaces. * New `CertifiedSelection<W, A>` type carries (wasm_op, arm_instrs, witness). Selectors emit witness-less selections; validators accept-or-reject and attach a Witness. * New `Validator<W, A>` trait + `Z3ArmValidator` implementation (prototype handles `WasmOp::I32Add` mapped to `ArmOp::Add` as the worked example). * Counterexample-driven rejection: a buggy selector that emits SUB instead of ADD gets caught with concrete input values (R0=5, R1=3 → arm=2, wasm=8). ## Migration path (from docs/validator-pattern.md) * Keep existing T1 Rocq proofs (35 ops) — they're correct already. * Validator covers everything else. T2 existence proofs (143) become redundant once their ops are validator-certified. * T3 admits (10) get re-examined — most should close via the validator since they were re-admitted for ARM-vs-Rocq divergence. ## Tests (in crates/synth-verify/src/validator_pattern.rs) * `i32_add_certifies` — selector picks ADD, validator accepts * (wrong-selection test, in the same module) — selector picks SUB, validator rejects with Counterexample * `unsupported_op_returns_structured_error` — non-I32Add ops return `UnsupportedOp`, not a panic * `certified_selection_witness_roundtrip` — plumbing ## What this PR is NOT This is the architectural commitment + one worked example. It does NOT validate all 150 wasm ops — that's the v0.5/v0.6 work this scaffolding enables. Per-op validator extension is structurally trivial now; the hard part was deciding the pattern. References: docs/validator-pattern.md (314 lines), issue #76, issue #73, issue #105's spectre-policy doc (cites the same Crocus paper). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Run cargo fmt -p synth-verify to bring encode_arm_sequence's signature to single-line form. No semantic change. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This was referenced May 15, 2026
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
3 tasks
Contributor
Author
|
The gating fuzz failure on this PR ( Not a regression introduced by this PR — same crash exists on |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Architectural commitment + worked example for the CompCert-style certifying-validator pattern. Opens the path toward retiring issue #73's divergent-Rocq-proofs credibility gap.
What's in scope
docs/validator-pattern.md(314 lines) — architecture rationale, per-op validation flow, migration plan from the existing Rocq-T1/T2/T3 proof tiers, and what subsequent PRs need to do per opcrates/synth-verify/src/validator_pattern.rs(376 lines) — Rust prototype:CertifiedSelection<W, A>carries (wasm_op, arm_instrs, witness)Validator<W, A>traitZ3ArmValidatorimplementation — prototype handlesWasmOp::I32AddonlyWhy this matters
Issue #73 says
compile_wasm_to_armin Rocq diverges from the actual Rust selector in 5 documented ways (trap guards, comparison count, regalloc, MOVW+MOVT, i64). The 233 Qed proofs are internally valid but don't establish correctness of the shipped binary.The validator-pattern fix isn't to repair the divergence per-op — it's to replace the proof obligation: prove one meta-theorem ("if validator accepts, selection is correct") and validate each concrete selection at compile time. Each new wasm op is structurally easy to add; no new Rocq lemma required.
What this PR is NOT
This PR validates one op (I32Add). The remaining ~150 wasm ops are mechanical extension work, slated for v0.5/v0.6. The doc enumerates them with a coverage matrix and migration timeline.
Verification
Local cargo build OOM'd on the z3-sys parallel build pressure — relying on CI to verify with feature flags
z3-solver,arm. Tests are #[cfg(all(feature = "z3-solver", feature = "arm"))], same gating as the existingtranslation_validatormodule.🤖 Generated with Claude Code