DavePearce / DevmProofGen

Dafny Evm Proof Generator (experimental)
1 stars 1 forks source link

Asserts for masked addresses #103

Open booleanfunction opened 2 hours ago

booleanfunction commented 2 hours ago

When an address (i.e. that is already u160) is masked to ensure it is u160 it is useful to assert that the AndU160 doesn't change the value.

This isn't necessary in every case but has helped when specific reference to that address is required in the preconditions of the following block.

For example:

st := Caller(st);
//|fp=0x0060|st.evm.context.sender as u256,0x0,hash,wad,0x0,wad,dst*,src*,0x229,transferFrom|
st := PushN(st,20,0xffffffffffffffffffffffffffffffffffffffff);
//|fp=0x0060|0xffffffffffffffffffffffffffffffffffffffff,st.evm.context.sender as u256,0x0,hash,wad,0x0,wad,dst*,src*,0x229,transferFrom|
st := AndU160(st);
//|fp=0x0060|st.evm.context.sender as u256,0x0,hash,wad,0x0,wad,dst*,src*,0x229,transferFrom|
assert st.Peek(0) == st.evm.context.sender as u256;
booleanfunction commented 2 hours ago

PS - This is of course only relevant if we track things like st.evm.context.senderon the stack.

I have also used this type of assert when tracking additional parameters such as say src and dst in the WETH transferFrom function. Even if it isn't possible to automate the tracking on these types of parameters (though I do have some ideas!) a placeholder assert would still be convenient; maybe // assert st.Peek(0) == (or assert st.Peek(0) == to force the user to either delete or complete the assert).