Adopt validator-based verification strategy (CompCert pattern) for i64/f32/f64 proof coverage

[avrabe]

Context

CompCert (formally verified C compiler, now DO-178C qualified for ATR 42/72 aircraft as of March 2026) uses a pattern where NP-hard problems like register allocation use an untrusted solver + trusted validator. The solver finds a solution; a simple, formally verified checker confirms it.

Problem

Synth currently uses per-instruction Rocq proofs for correctness (T1 coverage for i32). Extending this to full i64/f32/f64/SIMD coverage requires writing thousands of additional Rocq lemmas — labor-intensive and slow.

Proposal

Adopt the certifying algorithm pattern for instruction selection:

1. Untrusted selector: The existing heuristic instruction selector picks ARM instructions for each WASM operation
2. Trusted validator: A lightweight, formally verified checker (in Rocq or Z3) confirms each concrete selection is correct
3. Certification: The validator is the only component that needs a formal proof — the selector can be as complex as needed

Why this works

• A quadratic-time verified checker of a register allocation is far easier to prove correct than a verified graph-coloring algorithm
• Z3 translation validation infrastructure already exists in synth-verify
• CompCert's avionics qualification proves this approach satisfies certification authorities
• Could achieve full proof coverage 5-10x faster than per-instruction Rocq proofs

Implementation sketch

1. Define a CertifiedSelection type: (wasm_op, arm_instructions, z3_proof_witness)
2. After instruction selection, run the Z3 validator on each selection
3. For the Rocq side: prove that "if the Z3 validator accepts, the selection is correct" (a meta-theorem about the validator, not about each instruction)
4. Gradually replace per-instruction proofs with validator-based proofs where the effort is highest (i64 register pairs, f32 VFP sequences)

References

• CompCert: https://compcert.org/
• CompCert DO-178C qualification: ATR 42/72 (March 2026)
• "Translation Validation for a Verified OS Kernel" (Sewell et al.) for the validator pattern

Priority

High — this unblocks full proof coverage without proportional proof effort.

Labels

enhancement, verification, architecture