Upstream first batch of lemmas from Lido engagement #2787
Conversation
| rule 0 <Int X => true requires 0 <=Int X andBool notBool (X ==Int 0) [simplification(60)] | ||
|
|
||
| rule X <=Int maxUInt256 => X <Int pow256 [simplification] | ||
|
|
There was a problem hiding this comment.
Not entirely sure these three lemmas are strictly necessary. They seem to be things that the SMT solver could easily resolve, but maybe they can help trigger further simplifications.
| andBool 0 <Int C | ||
| andBool A <Int ( C *Int B ) | ||
| [simplification, symbolic(A, B), concrete(C), preserves-definedness] | ||
|
|
There was a problem hiding this comment.
This is a fairly specific lemma, but I suppose it might be worth having if we run into an expression like this again.
| @@ -239,4 +239,7 @@ module LEMMAS-HASKELL [symbolic] | |||
|
|
|||
| rule (notBool (A andBool B)) andBool A => (notBool B) andBool A [simplification] | |||
|
|
|||
| rule [notBool-or]: notBool ( A orBool B ) => ( notBool A ) andBool ( notBool B ) [simplification(60)] | |||
| rule [notBool-and]: notBool ( A andBool B ) => ( notBool A ) orBool ( notBool B ) [simplification(60)] | |||
|
|
|||
There was a problem hiding this comment.
Set a later priority for these rules so they don't conflict with the preceding ones.
| #asWord ( B1 +Bytes B2 ) <Int X => #asWord ( B1 ) <Int X /Int ( 2 ^Int ( 8 *Int lengthBytes ( B2 ) ) ) | ||
| requires X modInt ( 2 ^Int ( 8 *Int lengthBytes ( B2 ) ) ) ==Int 0 | ||
| [simplification, preserves-definedness] | ||
|
|
There was a problem hiding this comment.
Not sure if too specific. I considered if it should use the concrete(X) attribute, but if it didn't include it in the first place it's probably because the expression that originally motivated it had a symbolic X.
| rule [b2w-lt]: | ||
| bool2Word ( B:Bool ) *Int X <Int Y => | ||
| ( ( notBool B ) andBool 0 <Int Y ) orBool ( B andBool X <Int Y ) | ||
| [simplification, concrete(Y)] |
There was a problem hiding this comment.
In the original file this had a typo, ( notBool B ) andBool 0 <=Int Y.
| X xorInt Y <Int Z => true | ||
| requires X <Int ( 2 ^Int log2Int ( Z ) ) andBool Y <Int ( 2 ^Int log2Int ( Z ) ) | ||
| [simplification, concrete(Z)] |
There was a problem hiding this comment.
Does this need an additional constraint for Z >Int 0 to avoid the log2Int undefinedness?
There was a problem hiding this comment.
Good catch, I'll add the constraint
lucasmt
force-pushed
the
upstream-lido-lemmas
branch
from
2fdfcac to
f432111
Compare
Lemmas were taken from this file: https://github.com/runtimeverification/_audits_lidofinance_dual-governance_fork/blob/rv-extension-refactor-full-suite/test/kontrol/lido-lemmas.k. Not all of the lemmas have been included, as some of them require further analysis.