Module expansion_validator 

Expansion-level certifying validation for the i64 pseudo-ops (#667 move 2).

The crate::validator_pattern validator certifies (WasmOp, [ArmOp]) selections — but for the i64 pseudo-ops (I64Mul, the I64SetCond family, I64Clz/I64Ctz/I64Popcnt, the i64 shifts and rotates) the ArmOp is itself a compound: the encoder (synth-backend/src/arm_encoder.rs::encode_thumb) expands each into a multi-instruction Thumb-2 sequence (UMULL + MLA cross products, IT-block flag materialisation, CMP/BEQ diamonds, the HAKMEM popcount fold with its scratch push/pop). Modeling the pseudo-op with its reference semantics — what validator_pattern does — certifies the register wiring but is circular about the expansion itself. The expansion is exactly where the #615 (A32 silent NOP), #632 (popcnt result clobbered by the scratch restore POP), and #633 (missing i64 div_s overflow guard) miscompiles lived.

This module closes that gap for the branch-free and forward-branch pseudo-ops: it takes the literal bytes the shipped encoder emitted, decodes them with a small Thumb-2 decoder (loud Err on anything outside the modeled subset — never a silent skip), symbolically executes the decoded sequence over QF_BV terms (path conditions for forward branches, IT-block predication, a concrete-offset stack model for the scratch push/pop), and discharges

UNSAT( wasm_op_semantics(inputs) != sequence_semantics(inputs) )

through crate::solver::BvSolver (ordeal by default — every Unsat carries an LRAT certificate checked before it is reported; Z3 remains the feature-gated differential oracle).

Covered (validated at the emitted-sequence level)

pseudo-op	expansion shape
I64Mul	MUL + MLA cross products + UMULL + ADD (branch-free)
I64SetCond (EQ/NE/LT/LE/GT/GE/LO/LS/HI/HS)	CMP (+IT CMP) / SBCS + ITE + MOV pair
I64SetCondZ (i64.eqz)	ORR.W + CMP + ITE + MOV pair
I64Clz / I64Ctz	CMP.W + BEQ diamond, CLZ / RBIT+CLZ, +32 arm
I64Popcnt	HAKMEM fold ×2 with PUSH/POP scratch discipline (#632)
I64Shl / I64ShrU / I64ShrS	small/large split, one BPL diamond
I64Rotl / I64Rotr	#610 fixed-ABI wrapper (stack marshaling) + diamond

Held out, honestly

• I64DivS / I64DivU / I64RemS / I64RemU — the Thumb-2 expansions contain a 64-round binary long-division loop (backward branches). The symbolic executor here is a forward-only DAG executor; sound validation of the division cores needs bounded loop unrolling (64 iterations of a ~10-instruction body is far past the bit-blasting budget) or loop-invariant reasoning. The decoder rejects backward branches with a loud error, so these can never be silently green-washed. This also means the #633 missing-overflow-guard shape is not expressible here yet: the guard sits inside the div expansion, and guard/trap equivalence additionally needs UDF-reachability (trap-state) modeling, not just value-domain equivalence. Documented as future work in docs/validator-pattern.md.
• Trap guards in general — like validator_pattern, this module certifies value-domain equivalence; trap paths are control flow.

Trusted base

The decoder (~25 instruction forms, each a direct transcription of the ARM ARM encoding diagram), the micro-op semantics below, and the solver. The encoder — the thing that has actually been wrong (#615/#632/#633) — is not trusted: its output bytes are the artifact being checked, so encoder/validator drift is structurally impossible (there is no second hand-maintained copy of the expansion to drift).

Structs

ExpansionWitness

Witness that an emitted expansion was certified: Unsat of the negated equivalence, discharged through the certificate-checked solver.

Enums

ExpansionError

Expansion validation failure reasons. Everything is loud: an instruction or shape outside the modeled subset is an error, never a silent accept.

Functions

covered_i64_pseudo_selections

The covered (WasmOp, pseudo ArmOp) surface with the canonical selector-shaped register assignment: operand a in (R0, R1), operand b / amount in (R2, R3), result in R0 / (R0, R1). Callers (the synth verify driver and the oracle tests) encode each pseudo-op through the shipped ArmEncoder and feed the bytes to validate_expansion.

validate_expansion

Validate that the encoder’s emitted code for pseudo implements wasm.