feat(verify): expansion-level certifying validation for the i64 pseudo-ops (#667 move 2, #242)

[avrabe]

Part of #667 (move 2: extend the certifying validator) / epic #242 Track C.

What

The validator_pattern checker certifies (WasmOp, [ArmOp]) selections — but the i64 pseudo-ops are expanded to multi-instruction Thumb-2 sequences inside the encoder, and the pseudo-op-level check models them with their own reference semantics (circular about the expansion). The expansion is exactly where this cycle's miscompiles lived: #615 (A32 silent NOP), #632 (popcnt result clobbered by the scratch-restore POP), #633 (missing i64 div_s overflow guard).

New crates/synth-verify/src/expansion_validator.rs puts the shipped encoder's literal bytes on the checked path:

1. decode the emitted bytes (small Thumb-2 subset decoder — loud Err on anything unmodeled, never a silent skip),
2. symbolically execute the sequence: guarded/if-converted execution with path conditions for forward branches, IT-block predication, NZCV flag modeling (CMP/SUBS/SBCS/ADDS), and a concrete-offset stack model for the scratch PUSH/POP (the thumb-2: i64.popcnt result register (r5) clobbered by epilogue pop {r3,r4,r5} — silent wrong value #632 surface),
3. discharge UNSAT(wasm_op_semantics ≠ sequence_semantics) through the certificate-checked BvSolver (ordeal default per feat(verify): ordeal 0.4 solver backend behind a thin trait — Z3 demoted to differential oracle (#553) #595/chore(verify): drop static-link-z3 from the default build/CI path (#553 steps 3/4) #621 — every Unsat carries an LRAT proof checked before it is reported; Z3 stays the feature-gated differential oracle).

Because the checked artifact is the encoder's own output, encoder↔validator drift is unrepresentable — there is no second hand-maintained copy of the expansion.

Coverage

pseudo-op	expansion shape	status	query time
I64Mul	MUL/MLA cross products + UMULL + ADD	✅ validated	3.3 s
I64SetCond ×10 (EQ/NE/LT/LE/GT/GE/LO/LS/HI/HS)	CMP (+IT CMP) / CMP+SBCS + ITE + MOV pair	✅ validated	ms
I64SetCondZ (i64.eqz)	ORR.W + CMP + ITE + MOV pair	✅ validated	ms
I64Clz / I64Ctz	CMP.W + BEQ diamond; CLZ / RBIT+CLZ; +32 arm	✅ validated	0.07 s / 1.2 s
I64Popcnt	HAKMEM fold ×2 + PUSH/POP scratch discipline	✅ validated	23 s
I64Shl / I64ShrU / I64ShrS	small/large split, BPL diamond (path-condition encoded)	✅ validated	~1 s each
I64Rotl / I64Rotr	#610 fixed-ABI wrapper (stack marshaling) + diamond	✅ validated	~8.5 s each
I64DivS/DivU/RemS/RemU	64-round long-division loop	⛔ held out	—

Held out honestly: the div/rem cores contain backward branches (loops); the forward-only DAG executor rejects them with a loud decode error (backward branch (loop) — held out, needs loop unrolling), so the held-out surface cannot green-wash (test div_family_is_held_out_loudly). Sound coverage needs bounded unrolling (64 × ~10 instrs is past the bit-blasting budget) or invariant reasoning. Consequently the #633 missing-guard shape is not yet expressible at this layer: the guard sits inside the div expansion, and trap-guard equivalence needs UDF-reachability (trap-state) modeling on top of loop support — documented in docs/validator-pattern.md as the named next increment.

Red-on-#632-shape evidence

red_632_popcnt_result_in_restore_set_fails splices the literal pre-fix tail from the #632 disassembly (ADDS R5,R4,R5; POP {R3,R4,R5}; MOV rd,R5) onto the shipped popcount body (the shipped tail — ADD.W R12,R4,R5; POP; MOV rd,R12 — is byte-pinned so the test screams if the encoder changes):

✗ #632 shape rejected as required: I64Popcnt: a_lo=0x0, a_hi=0x0, b_lo=0x0, b_hi=0x0

(counterexample: the sequence returns the caller's dead R5 — the solver's model distinguishes via the unconstrained initial register, i.e. exactly the "stale stack garbage" the issue observed). Also red: a wrong-condition compare (i64.lt_s vs the GE sequence) and a Clz expansion with the +32 arm nulled. Green in the same suite: every shipped expansion, plus high-register variants (rd=R8 → MOV.W path #311; popcnt rd=R5, i.e. a destination inside the restore set — the exact #632 trigger — certifies on the fixed encoder).

Certificate logging at verify time

synth verify (verify feature path, ARM backend) now certifies all 20 covered expansions per run, one certificate line each:

Certifying i64 pseudo-op expansions (shipped Thumb-2 encoder):
✓ I64Mul expansion certified: 4 instrs, 14 bytes [unsat, LRAT-checked]
…
✓ I64Rotl expansion certified: 32 instrs, 102 bytes [unsat, LRAT-checked]
✓ I64Popcnt expansion certified: 48 instrs, 180 bytes [unsat, LRAT-checked]

Tractability notes (measured, documented in the module)

• i64.mul is checked against the textbook schoolbook limb form, whose multiply atoms structurally match UMULL/MUL/MLA. The symbolic schoolbook↔64-bit-bvmul identity does not converge (>400 s — same line as the documented i32 rem_s MLS scope-out); it is pinned on an edge-heavy concrete grid vs Rust's u64 multiply.
• i64.popcnt uses a two-link chain: ∀w. hakmem(w) == bit-sum(w) proved symbolically once (~7 s, unit test), then sequence == hakmem(lo)+hakmem(hi) per validation (23 s). The one-link query (sequence vs bit-sum over both words) does not converge (>570 s).
• i64.ctz is independent by construction: LSB-first ite-chain reference vs the sequence's CLZ(RBIT(x)).

Oracles / gates

• cargo test --workspace: 2066 passed / 0 failed (post-rebase on df982f1)
• new: 9 unit tests (synth-verify) + 6 integration tests (crates/synth-backend/tests/i64_expansion_certification.rs, ~50 s)
• cargo fmt --check + cargo clippy --workspace --all-targets -- -D warnings clean (also -p synth-cli --features verify)
• Verify-path only: no selector/encoder/codegen change — frozen anchors untouched by construction (synth-backend gains only a dev-dependency + tests)

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 92.71291% with 83 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-verify/src/expansion_validator.rs	92.57%	83 Missing ⚠️

📢 Thoughts on this report? Let us know!