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.
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;
When an address (i.e. that is already
u160) is masked to ensure it isu160it is useful to assert that theAndU160doesn'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: