You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Because of the sha3_expr mismatch, pairFor returns a different address (bbbb0011) than the address actually deployed (bbbb000b) and subsequent calls fail
Describe the bug
Different sha3_expr in in create2 init code lead to different inferred address vs actually deployed address.
In the example below,
uniswapV2Factory.createPair(address(token), address(weth))
results in the following sha3_expr:But in the pairFor helper function, this is the expression used:
(note the hardcoded initcode hash value)
On the halmos side, it results in the following sha3_expr:
If we were to evaluate
f_sha3_93088(...init code concrete value...)
concretely, we would indeed get the same value:Because of the sha3_expr mismatch, pairFor returns a different address (
bbbb0011
) than the address actually deployed (bbbb000b
) and subsequent calls failTo Reproduce
necessary steps from https://github.com/igorganich/damn-vulnerable-defi-halmos/blob/master/test/puppet-v2/PuppetV2_Halmos.t.sol#L86 (h/t @igorganich)
The text was updated successfully, but these errors were encountered: