Lemmas review #71
Lemmas review #71
Conversation
|
|
||
| rule 75506153327051474587906755573858019282972751592871715030499431892688993766217 ==K keccakIntList(A B) => false | ||
| requires A =/=Int 0 | ||
|
|
||
| rule 78338746147236970124700731725183845421594913511827187288591969170390706184117 ==K keccakIntList(A B) => false |
There was a problem hiding this comment.
What is this number?
There was a problem hiding this comment.
this is the slot for balanceOf[0]. both the two lines you deleted above are required afaik. They flip the order in the requires. I really had to add all four rules here or I would sometimes get stupid non deterministic failures.
| @@ -75,20 +75,6 @@ library to the logical `#rangeUInt` conditions expressed within the specs. | |||
| rule A -Word B <=Int A => #rangeUInt(256, A -Int B) | |||
| requires #rangeUInt(256, A) | |||
| andBool #rangeUInt(256, B) | |||
|
|
|||
| // add | |||
| rule (chop(X +Int Y) >=Int X) => #rangeUInt(256, X +Int Y) | |||
There was a problem hiding this comment.
When we have iff in range uint256 \ X + Y, there would be no chop by the time we get to the add.
Is this here for the fail spec?
There was a problem hiding this comment.
can't remember where these came from, they all turned up in the debugger at some point iirc.
|
See also #63. |
The base case is sufficient.
By removing extra boolean check.
The terms that end up in add/sub/mul are constrained in iff blocks, so there's no chop.
asymmetric
force-pushed
the
lemma-comments
branch
from
ffd56db to
31268e0
Compare
| @@ -75,20 +75,6 @@ library to the logical `#rangeUInt` conditions expressed within the specs. | |||
| rule A -Word B <=Int A => #rangeUInt(256, A -Int B) | |||
| requires #rangeUInt(256, A) | |||
| andBool #rangeUInt(256, B) | |||
|
|
|||
| // add | |||
| rule (chop(X +Int Y) >=Int X) => #rangeUInt(256, X +Int Y) | |||
There was a problem hiding this comment.
can't remember where these came from, they all turned up in the debugger at some point iirc.
|
|
||
| rule 75506153327051474587906755573858019282972751592871715030499431892688993766217 ==K keccakIntList(A B) => false | ||
| requires A =/=Int 0 | ||
|
|
||
| rule 78338746147236970124700731725183845421594913511827187288591969170390706184117 ==K keccakIntList(A B) => false |
There was a problem hiding this comment.
this is the slot for balanceOf[0]. both the two lines you deleted above are required afaik. They flip the order in the requires. I really had to add all four rules here or I would sometimes get stupid non deterministic failures.
|
Non-deterministic failures suck, yes. Otherwise I'd be fine with cosmetic cleanups, as long as everything is green. |
|
They are obviously low-prio. |
I've been very trigger happy here, sometimes removing things I'm not 100% sure about, so we can have a discussion around the diff.