Skip to content

fix(symbolic): relate nested and short Keccak preimages #18348

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
figtracer wants to merge 2 commits into
base: mablr/evm2-migration
Choose a base branch
from
+141 −58
Open

fix(symbolic): relate nested and short Keccak preimages #18348

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3d8d4c2
fix(symbolic): relate nested and short Keccak preimages
figtracer Nov 9, 2026
04b4f8c
perf(symbolic): share nested hash comparisons
figtracer Nov 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 26 additions & 20 deletions crates/evm/symbolic/src/runtime/expr/bool.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,13 +149,7 @@ impl SymBoolExpr {
// `keccak(a) == keccak(b) => len(a) == len(b) && bytes(a) == bytes(b)`.
let mut conditions =
vec![Self::eq(cx, left_len.clone(), right_len.clone())];
conditions.extend(
left_bytes
.iter()
.cloned()
.zip(right_bytes.iter().cloned())
.map(|(left, right)| Self::eq(cx, left, right)),
);
conditions.extend(Self::bytes_eq(cx, left_bytes, right_bytes));
Self::and(cx, conditions)
}
(
Expand All @@ -167,12 +161,7 @@ impl SymBoolExpr {
&& left_bytes.len() == right_bytes.len() =>
{
// `hash(a) == hash(b) => bytes(a) == bytes(b)`.
let conditions = left_bytes
.iter()
.cloned()
.zip(right_bytes.iter().cloned())
.map(|(left, right)| Self::eq(cx, left, right))
.collect();
let conditions = Self::bytes_eq(cx, left_bytes, right_bytes);
Self::and(cx, conditions)
}
_ => {
Expand Down Expand Up @@ -393,16 +382,33 @@ impl SymBoolExpr {
return Some(Self::constant(cx, false));
}
// `keccak(a) == keccak(b) => bytes(a) == bytes(b)`.
let conditions = bytes
.get(..preimage.len())?
.iter()
.cloned()
.zip(preimage.iter().cloned())
.map(|(byte, expected)| Self::eq(cx, byte, expected))
.collect();
let conditions = Self::bytes_eq(cx, bytes.get(..preimage.len())?, &preimage);
Some(Self::and(cx, conditions))
}

/// Compares two byte sequences, comparing words where both sides extract the bytes of one
/// word each.
///
/// A word comparison lets nested hashes inside a preimage go through the Keccak equality
/// rewrite instead of leaving their bytes as free solver symbols.
fn bytes_eq(cx: &mut SymCx, left: &[SymExpr], right: &[SymExpr]) -> Vec<Self> {
let mut conditions = Vec::with_capacity(left.len().min(right.len()));
let mut index = 0;
while index < left.len().min(right.len()) {
if let (Some(left_word), Some(right_word)) = (
word_from_extracted_bytes(&left[index..]),
word_from_extracted_bytes(&right[index..]),
) {
conditions.push(Self::eq(cx, left_word, right_word));

@mattsse mattsse Nov 10, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please preserve sharing or bound this recursive expansion. Starting with require(a != b), repeatedly assign a = uint256(keccak256(abi.encode(a, a))) and likewise b, then assert(a != b). Each round adds only two hash nodes, but this call compares the same inner pair twice, and Self::and flattens both results without deduplication, producing 2^n copies of the leaf equality. On this head, 16 rounds finished in 0.23s, 20 took 4.31s (both with zero SMT calls), and 24 did not finish within a 20-second external limit. Larger small loops can exhaust memory during expression construction. The previous byte comparisons did not recursively unfold the shared preimages. Memoizing compared pairs and avoiding duplicate conjunction expansion, or imposing a bounded fallback, would keep this rewrite from making these tests unusable.

index += 32;
} else {
conditions.push(Self::eq(cx, left[index].clone(), right[index].clone()));
index += 1;
}
}
conditions
}

/// Computes a conservative upper bound for the unfolded Boolean result without interning it.
///
/// Cached child costs are deliberately added again at each use. This keeps construction of a
Expand Down
6 changes: 2 additions & 4 deletions crates/evm/symbolic/src/runtime/expr/expr.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -324,7 +324,7 @@ pub(in crate::runtime::expr) fn low_masked_source_any(expr: &SymExpr) -> Option<
}
}

fn word_from_extracted_bytes(bytes: &[SymExpr]) -> Option<SymExpr> {
pub(in crate::runtime::expr) fn word_from_extracted_bytes(bytes: &[SymExpr]) -> Option<SymExpr> {
if bytes.len() < 32 {
return None;
}
Expand Down Expand Up @@ -2355,9 +2355,7 @@ pub(crate) fn keccak_word_with_len(cx: &mut SymCx, bytes: Vec<SymExpr>, len: Sym
&& let Ok(concrete) = concrete_expr_bytes(&bytes[..len], "symbolic keccak input")
{
let hash = Into::<U256>::into(keccak256(concrete));
if len == 32 || len == 64 {
cx.record_concrete_keccak_preimage(hash, bytes[..len].to_vec().into());
}
cx.record_concrete_keccak_preimage(hash, bytes[..len].to_vec().into());
return SymExpr::constant(cx, hash);
}

Expand Down
17 changes: 15 additions & 2 deletions crates/forge/tests/cli/test_cmd/symbolic_storage.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -676,6 +676,17 @@ contract SymbolicKeccakPreimage {
function checkKnownKeccakPreimage(uint256 x) public pure {
assert(keccak256(abi.encode(x)) != keccak256(abi.encode(uint256(42))));
}

function checkKnownShortKeccakPreimage(uint8 x) public pure {
assert(keccak256(abi.encodePacked(x)) != keccak256(abi.encodePacked(uint8(42))));
}

function checkNestedKeccakInjective(uint256 a, uint256 b) public pure {
require(a != b);
bytes32 left = keccak256(abi.encodePacked(hex"1901", bytes32(0), keccak256(abi.encode(a))));
bytes32 right = keccak256(abi.encodePacked(hex"1901", bytes32(0), keccak256(abi.encode(b))));
assert(left != right);
}
}
"#,
);
Expand All @@ -684,11 +695,13 @@ contract SymbolicKeccakPreimage {
.failure()
.stdout_eq(str![[r#"
...
Ran 3 tests for test/SymbolicKeccakPreimage.t.sol:SymbolicKeccakPreimage
Ran 5 tests for test/SymbolicKeccakPreimage.t.sol:SymbolicKeccakPreimage
[PASS] checkArrayElementSurvivesMappingWrite(address,uint256,uint256) ([METRICS])
[FAIL: panic: assertion failed (0x01); counterexample: [SENDER] [SENDER] calldata=0x4df8b26f000000000000000000000000000000000000000000000000000000000000002a args=[42]] checkKnownKeccakPreimage(uint256) ([METRICS])
[FAIL: panic: assertion failed (0x01); counterexample: [SENDER] [SENDER] calldata=0x78ccac51000000000000000000000000000000000000000000000000000000000000002a args=[42]] checkKnownShortKeccakPreimage(uint8) ([METRICS])
[PASS] checkNestedArraySurvivesMappingWrite(address,address,uint256,uint256) ([METRICS])
Suite result: FAILED. 2 passed; 1 failed; 0 skipped; [ELAPSED]
[PASS] checkNestedKeccakInjective(uint256,uint256) ([METRICS])
Suite result: FAILED. 3 passed; 2 failed; 0 skipped; [ELAPSED]
...
"#]]);
}
Loading