Found RED by the VCR-VER-002 derived-ARM-trap gate (#166, v0.43 verification-closure lane): the i32 load/store OOB trap-preservation VC rejects the SHIPPED --safety-bounds software guard shape for multi-byte accesses, with counterexamples pinned at the top of the address space.
The divergence
generate_load_with_bounds_check / the store twin (crates/synth-synthesis/src/instruction_selector.rs) emit:
ADD r12, addr, #(offset + size - 1) ; end address — WRAPPING 32-bit add
CMP r12, r10 ; r10 = linear-memory size
BLO +0 ; in-bounds skips the trap
UDF #0
LDR/STR ...
WASM Core's effective-address check is EXACT arithmetic: trap iff addr + offset + size > mem_size. The guard computes addr + (offset+size-1) mod 2^32: for addr >= 2^32 - (offset+size-1) the end address wraps to a small value, BLO passes, and the access goes through — reading/writing below the linear-memory base (the LDR [r11, addr, #offset] hardware address also wraps). Example (word load, offset 0): addr = 0xFFFF_FFFF → r12 = 3 < r10 → no trap; WASM requires one.
Byte accesses with offset 0 are exact (end = addr + 0 cannot wrap) — the gate verifies that case green, so this is specifically the multi-byte / non-zero-offset class.
Evidence
crates/synth-verify/src/translation_validator.rs test word_load_software_bounds_guard_wraps_at_address_top pins the divergence as Invalid with the counterexample restricted to addr >= 0xFFFF_FFFD (flip it to Verified when this is fixed).- Test
wraparound_safe_bounds_guard_verifies proves the gate is satisfiable by a correct guard, i.e. the red is not vacuous:
CMP r10, #k; BHS +0; UDF (bound < k ⇒ always trap) then SUB r12, r10, #k; CMP addr, r12; BLS +0; UDF with k = offset + size — exact on both paths, same instruction count +3.
Severity / exploitability
Requires a WASM-side address in the top ~3 bytes of the i32 address space, so any module whose index arithmetic can be attacker-influenced can escape the software bounds check downward by up to offset+size-1 bytes below the heap base. MPU/masking modes are unaffected (#651's masking clamps the effective address; MPU faults on the physical access).
Related: #377 (inline UDF bounds trap), #651 (masking mode), #166 (trap-preservation VC).
Found RED by the VCR-VER-002 derived-ARM-trap gate (#166, v0.43 verification-closure lane): the i32 load/store OOB trap-preservation VC rejects the SHIPPED
--safety-bounds softwareguard shape for multi-byte accesses, with counterexamples pinned at the top of the address space.The divergence
generate_load_with_bounds_check/ the store twin (crates/synth-synthesis/src/instruction_selector.rs) emit:WASM Core's effective-address check is EXACT arithmetic: trap iff
addr + offset + size > mem_size. The guard computesaddr + (offset+size-1)mod 2^32: foraddr >= 2^32 - (offset+size-1)the end address wraps to a small value,BLOpasses, and the access goes through — reading/writing below the linear-memory base (theLDR [r11, addr, #offset]hardware address also wraps). Example (word load, offset 0):addr = 0xFFFF_FFFF→r12 = 3 < r10→ no trap; WASM requires one.Byte accesses with offset 0 are exact (
end = addr + 0cannot wrap) — the gate verifies that case green, so this is specifically the multi-byte / non-zero-offset class.Evidence
crates/synth-verify/src/translation_validator.rstestword_load_software_bounds_guard_wraps_at_address_toppins the divergence asInvalidwith the counterexample restricted toaddr >= 0xFFFF_FFFD(flip it toVerifiedwhen this is fixed).wraparound_safe_bounds_guard_verifiesproves the gate is satisfiable by a correct guard, i.e. the red is not vacuous:CMP r10, #k; BHS +0; UDF(bound < k ⇒ always trap) thenSUB r12, r10, #k; CMP addr, r12; BLS +0; UDFwithk = offset + size— exact on both paths, same instruction count +3.Severity / exploitability
Requires a WASM-side address in the top ~3 bytes of the i32 address space, so any module whose index arithmetic can be attacker-influenced can escape the software bounds check downward by up to
offset+size-1bytes below the heap base. MPU/masking modes are unaffected (#651's masking clamps the effective address; MPU faults on the physical access).Related: #377 (inline UDF bounds trap), #651 (masking mode), #166 (trap-preservation VC).