Z3 verification for bulk memory operations (MemoryFill/MemoryCopy/MemoryInit)

[avrabe]

Context

PR #53 wired all bulk memory operations into the ISLE pipeline as side effects. They currently pass through without Z3 verification of their operands.

Current State

In loom-core/src/verify.rs, MemoryFill, MemoryCopy, MemoryInit, and DataDrop likely fall through to opaque symbolic handling. While these operations can't be constant-folded (they're side-effectful), their operands (dst, val, len) should be verified for equivalence when the optimizer transforms surrounding code.

TODO

1. Verify that Z3 correctly handles the stack effects (3 pops for fill/copy/init, 0 for data.drop)
2. Ensure operand expressions are verified for equivalence (if optimizer transforms i32.const 1 + i32.const 1 to i32.const 2 as a memory.fill argument, Z3 should confirm equivalence)
3. Add dedicated Z3 tests for bulk memory operations in optimized contexts

Files

• loom-core/src/verify.rs — Z3 verification handlers
• loom-core/src/lib.rs — tests section