fix(symbolic): find writes beyond materialized_size in dynamic memory reads

[gomesalexandre]

Summary

byte_dynamic_with_delta (the dynamic-offset read path used by MLOAD and memory-copy opcodes when the read offset is symbolic) enumerated candidate positions only within 0..materialized_size. store_symbolic_bytes records a write without ever bumping materialized_size -- there's no single concrete candidate to extend it to for a write whose offset the store dispatch treated as symbolic -- so such a write could land at a position the enumeration never reaches, and the read silently returned zero instead of the write's real value.

In a soundness-sensitive symbolic execution engine, a false negative like this can hide a genuine violation behind an apparently-"Safe" result.

This closes the one write path that #16240 (which introduced the materialized_size / logical_size split, explicitly to avoid false proofs) didn't yet cover.

Root cause

Store dispatch (store_word_offset / store_byte_offset / store_bytes_offset) decides whether a write's offset is "concrete" using offset.as_const() -- a shallow check that only matches a literal Const node. SymbolicMemoryWrite::concrete_offset() instead uses offset.eval() -- full recursive evaluation, strictly broader. A write whose offset happens to be const-evaluable but never folds down to a literal Const at construction time (e.g. Keccak(constant_preimage) & 0xff, since the mask-folding rules have no case for a bare Keccak operand) gets dispatched through store_symbolic_bytes and never bumps materialized_size, while concrete_offset() still reports it as "concrete."

A naive fast-path predicate that trusts concrete_offset().is_some() alone would wrongly treat materialized_size as a valid bound for such a write.

Fix

byte_dynamic_with_delta now only takes the bounded-enumeration fast path when it can prove, for every recorded write, that the write's full extent -- not just its offset -- fits inside materialized_size (offset.checked_add(len) some end <= materialized_size, checked arithmetic). Otherwise it falls back to folding every recorded write directly against the symbolic read target via nested ite, mirroring byte()'s own already-sound technique for a symbolic write offset against a concrete read target, generalized to a symbolic one.

load_word_offset's dynamic-offset branch now delegates through this same fixed path instead of the separately-buggy load_word_dynamic (deleted), which had the identical defect for full 32-byte word reads -- plus its own byte-by-byte-vs-whole-word enumeration mismatch.

No other read/write path is touched. SymBytes (byte_dynamic_with_delta in bytes.rs -- different struct, same name) and the storage layer (StorageWrite::select_from) already use the sound fold-every-write technique unconditionally, which is what confirms the approach here matches established convention rather than introducing a new one.

Testing

• Added regression tests reproducing the false negative directly: a write whose offset is const-evaluable via Keccak(const) & 0xff but not as_const()-able (dispatched as symbolic, materialized_size never bumped), a write straddling the materialized_size boundary (starts inside, ends past it), and the exact byte-beyond-bound / word-read-starting-at-a-different-offset shape the deleted load_word_dynamic got wrong.
• Verified genuine red-before-green: reverting only the new bound check back to the old (buggy) concrete_offset().is_some() predicate reproduces the exact silent-zero failure on the new tests; restoring the fix makes them pass.
• Full crate suite: 323 passed, 0 failed.
• cargo clippy -p foundry-evm-symbolic --lib -- -D warnings: clean.
• cargo fmt --check -p foundry-evm-symbolic: clean, no diff.
• This is a pure library/engine change with no CLI-visible surface, so no runtime CLI receipt is possible or claimed -- soundness is demonstrated via the unit-test suite above, including the actual counterexamples the bug produced.

Disclosure note

This defect sits in the symbolic execution engine's soundness guarantees (a false negative in a security-analysis tool). No separate private disclosure was made since it requires no live/deployed target to exploit -- it's a correctness bug in the local analysis tool itself, not a vulnerability in code the tool analyzes.

[github-actions]

✅ Changelog found

The deterministic check will validate the changed entry.