Open dddejan opened 4 years ago
A straightforward solution would be of course to have __verifier_old_uintN
for N=8, ..., 256
. But if I remember correctly, our plan was to rather support some kind of polymorphism.
This happens because in the case of VERIFIER_*
functions there is an if
statement when converting arguments that skips temp variables for arguments. I guess this is a hack to prevent side-effects. We need a more pragmatic way to deal with functions that can be used in specification. I am trying to figure out, e.g., how to use keccak
in specification and I'm running into similar issues.
Incorporating those temp variables could make this example work, because it would translate to bvzeroext_8_to_256(x#3[__this]) == old(bvzeroext_8_to_256(x#3[__this]))
. However, this would not work for #85. What we'd really like to have here is x#3[__this] == old(x#3[__this])
, i.e., no casts at all. For this, we would need the Solidity AST for the spec expression to have the old expression return type uint8
. Then the operator ==
will see that both of its arguments are uint8
and no casting is needed.
Of course there might be some special functions where the casting is needed, e.g., if keccak
takes uint256
then the temp variables should be included because those will do the cast. But for old
, there should be no casting.
Gives
The culprit is the old expression
bvzeroext_8_to_256(x#3[__this]) == old(x#3[__this])
.