Repository navigation
Conversation
The Keccak equality rewrite compared preimages byte by byte, so a hash nested inside a preimage, the EIP-712 digest shape, left its bytes as free solver symbols and the model check rejected the collision. Compare 32-byte runs that extract one word each as words, so nested hashes go through the same rewrite. Also record every concrete preimage length, not only 32 and 64 bytes, so a runtime hash of short data decides equality with a symbolic hash.
mattsse
left a comment
mattsse
left a comment
There was a problem hiding this comment.
Please bound the expansion of shared nested-hash comparisons; the inline comment includes a reproducer.
| word_from_extracted_bytes(&left[index..]), | ||
| word_from_extracted_bytes(&right[index..]), | ||
| ) { | ||
| conditions.push(Self::eq(cx, left_word, right_word)); |
There was a problem hiding this comment.
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.
Memoize compared hash pairs within one equality and remove duplicate preimage conditions before conjunction flattening. A 16-round shared comparison shrinks from 65,536 Boolean terms to one; a 25-round symbolic property changes from incomplete on the PR base to pass in 12.7 ms.
mattsse
left a comment
mattsse
left a comment
There was a problem hiding this comment.
The shared-preimage expansion finding remains for overlapping subtrees. Starting with require(a != b), repeat (a, c) = (c, uint256(keccak256(abi.encode(a, c)))) and (b, d) = (d, uint256(keccak256(abi.encode(b, d)))), then assert(c != d). In and_unique, the two child conjunctions differ, so deduplicating before Self::and flattens them still leaves exponentially many repeated leaves. On this head, 32 rounds took 1.40s, 36 took 9.55s (zero SMT calls), and 40 exceeded a 20-second external limit. Please deduplicate flattened terms or preserve sharing between conjunctions as well.
Why
Before: Nested symbolic Keccak equalities could end incomplete, and concrete preimages shorter than 32 bytes were missed. The initial rewrite also expanded shared nested comparisons repeatedly.
After: The nested property proves under the existing hash assumption, and shared comparisons remain small.
Change
Compare whole words inside hash preimages and record short concrete preimages. Cache compared hash pairs for one equality and remove duplicate conditions before flattening them.
Results
Downstream
forge test --symboliccan prove these bounded nested-hash cases; no API or data-format change. A compiler-folded constant hash still needs an observed preimage. AI assistance was used.