Skip to content

Upstream first batch of lemmas from Lido engagement #2787

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open

Upstream first batch of lemmas from Lido engagement #2787

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
6c91e85
Upstream first batch of lemmas from Lido engagement
lucasmt Jul 28, 2025
f432111
Add import of the WORD module for maxUInt256
lucasmt Jul 30, 2025
4377112
Add nonzero constraint to xorInt-lt lemma
lucasmt Aug 4, 2025
8826f77
Add non-negative constraints to xorInt-lt lemma
lucasmt Aug 6, 2025
716b22c
Remove redundant lemma (already in lemmas.k as b2w-mul-lt-l)
lucasmt Aug 6, 2025
6950359
Normalize subtraction lemmas
lucasmt Aug 11, 2025
db01bb4
Add tests for upstreamed lemmas
lucasmt Aug 12, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,4 +79,25 @@ module BITWISE-SIMPLIFICATION [symbolic]

rule 0 <=Int (X <<Int Y) => true requires 0 <=Int X andBool 0 <=Int Y [simplification]

// ###########################################################################
// bit-xor
// ###########################################################################

// Simplifications for the OpenZeppelin ternary operator function

rule [xorInt-ge-zero]:
0 <=Int X xorInt Y => true
requires 0 <=Int X andBool 0 <=Int Y
[simplification]

rule [xorInt-lt]:
X xorInt Y <Int Z => true
requires 0 <=Int X andBool 0 <=Int Y andBool 0 <Int Z
andBool X <Int ( 2 ^Int log2Int ( Z ) ) andBool Y <Int ( 2 ^Int log2Int ( Z ) )
[simplification, concrete(Z)]

rule [xorInt-to-if]:
X xorInt ( bool2Word ( B ) *Int ( X xorInt Y ) ) => #if B #then Y #else X #fi
[simplification]

endmodule
6 changes: 6 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,12 @@ module BYTES-SIMPLIFICATION [symbolic]
rule [bytes-concat-right-assoc-symb-r]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B2), simplification(40)]
rule [bytes-concat-left-assoc-conc]: B1:Bytes +Bytes (B2:Bytes +Bytes B3:Bytes) => (B1 +Bytes B2) +Bytes B3 [concrete(B1, B2), symbolic(B3), simplification(40)]

// Can ignore lower bytes for <Int if the corresponding bytes in X are 0 (note this does not apply to <=Int)
rule [asWord-lt-concat-left]:
#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]

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

// #buf

rule [buf-empty]: #buf(N:Int, _) => b"" requires N ==Int 0 [simplification]
Expand Down
37 changes: 37 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,11 +96,17 @@ module INT-SIMPLIFICATION-HASKELL [symbolic]
rule { A +Int B #Equals C +Int B } => { A #Equals C } [simplification(40)]
rule { A +Int B #Equals C +Int D } => { A -Int C #Equals D -Int B } [simplification(45), symbolic(A, C), concrete(B, D)]

rule 0 <Int A -Int B => B <Int A [simplification, symbolic(A, B)]
rule 0 <=Int A -Int B => B <=Int A [simplification, symbolic(A, B)]
rule A -Int B <Int 0 => A <Int B [simplification, symbolic(A, B)]
rule A -Int B <=Int 0 => A <=Int B [simplification, symbolic(A, B)]

endmodule

module INT-SIMPLIFICATION-COMMON
imports INT
imports BOOL
imports WORD

// ###########################################################################
// add, sub
Expand Down Expand Up @@ -148,6 +154,24 @@ module INT-SIMPLIFICATION-COMMON

rule (E *Int A) +Int B +Int C +Int D +Int (F *Int A) => ((E +Int F) *Int A) +Int B +Int C +Int D [simplification]

// Simplification of concrete multiplication

rule A *Int B <Int C => B <Int C /Int A
requires 0 <Int A andBool 0 <=Int C andBool C modInt A ==Int 0
[simplification(40), concrete(A, C), preserves-definedness]

rule A *Int B <=Int C => B <=Int C /Int A
requires 0 <Int A andBool 0 <=Int C andBool C modInt A ==Int 0
[simplification(40), concrete(A, C), preserves-definedness]

rule C <=Int A *Int B => C /Int A <=Int B
requires 0 <Int A andBool 0 <=Int C andBool C modInt A ==Int 0
[simplification(40), concrete(A, C), preserves-definedness]

rule C <Int A *Int B => C /Int A <Int B
requires 0 <Int A andBool 0 <=Int C andBool C modInt A ==Int 0
[simplification(40), concrete(A, C), preserves-definedness]

// ###########################################################################
// div
// ###########################################################################
Expand All @@ -169,6 +193,13 @@ module INT-SIMPLIFICATION-COMMON
requires 0 <=Int A andBool 0 <=Int B andBool 0 <Int C andBool A <=Int D andBool B <=Int C
[simplification, preserves-definedness]

rule ( A /Int B ) /Int C => 0
requires 0 <=Int A
andBool 0 <Int B
andBool 0 <Int C
andBool A <Int ( C *Int B )
[simplification, symbolic(A, B), concrete(C), preserves-definedness]

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a fairly specific lemma, but I suppose it might be worth having if we run into an expression like this again.

// ###########################################################################
// mod
// ###########################################################################
Expand Down Expand Up @@ -223,4 +254,10 @@ module INT-SIMPLIFICATION-COMMON

rule A -Int B +Int C <=Int D => false requires D <Int A -Int B andBool 0 <=Int C [simplification]

rule A ==Int B => false requires 0 <=Int A andBool B <Int 0 [simplification, concrete(B)]

rule 0 <Int X => true requires 0 <=Int X andBool notBool (X ==Int 0) [simplification(60)]

rule X <=Int maxUInt256 => X <Int pow256 [simplification]

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

endmodule
3 changes: 3 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -252,4 +252,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)]

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Set a later priority for these rules so they don't conflict with the preceding ones.

endmodule
62 changes: 62 additions & 0 deletions tests/specs/functional/lemmas-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,27 @@ module LEMMAS-SPEC
) ... </k>
requires 0 <=Int X andBool X <Int 2 ^Int 144

claim [div-div]: <k> runLemma ( ( A /Int B ) /Int 1024 ) => doneLemma ( 0 ) ... </k>
requires 0 <=Int A andBool 0 <Int B andBool A <Int ( 1024 *Int B )

// Booleans
// ---------

claim [notBool-or]:
<k> runLemma (
notBool ( ( X <Int LOWER ) orBool ( UPPER <=Int X ) )
) => doneLemma (
( notBool ( X <Int LOWER ) ) andBool ( notBool ( UPPER <=Int X ) )
) ...
</k>

claim [notBool-and]:
<k> runLemma (
notBool ( ( LOWER <=Int X ) andBool ( X <Int UPPER ) )
) => doneLemma (
( notBool ( LOWER <=Int X ) ) orBool ( notBool ( X <Int UPPER ) )
) ...
</k>

// Comparisons
// -----------
Expand Down Expand Up @@ -130,6 +151,34 @@ module LEMMAS-SPEC
) ...
</k>

claim [zero-lt-sub]: <k> runLemma ( 0 <Int A -Int B ) => doneLemma ( B <Int A ) ... </k>
claim [zero-le-sub]: <k> runLemma ( 0 <=Int A -Int B ) => doneLemma ( B <=Int A ) ... </k>
claim [zero-gt-sub]: <k> runLemma ( 0 >Int A -Int B ) => doneLemma ( B >Int A ) ... </k>
claim [zero-ge-sub]: <k> runLemma ( 0 >=Int A -Int B ) => doneLemma ( B >=Int A ) ... </k>

claim [sub-gt-zero]: <k> runLemma ( A -Int B >Int 0 ) => doneLemma ( A >Int B ) ... </k>
claim [sub-ge-zero]: <k> runLemma ( A -Int B >=Int 0 ) => doneLemma ( A >=Int B ) ... </k>
claim [sub-lt-zero]: <k> runLemma ( A -Int B <Int 0 ) => doneLemma ( A <Int B ) ... </k>
claim [sub-le-zero]: <k> runLemma ( A -Int B <=Int 0 ) => doneLemma ( A <=Int B ) ... </k>

claim [mul-lt-const]: <k> runLemma ( 36 *Int B <Int 1728 ) => doneLemma ( B <Int 48 ) ... </k>
claim [mul-le-const]: <k> runLemma ( 36 *Int B <=Int 1728 ) => doneLemma ( B <=Int 48 ) ... </k>
claim [mul-gt-const]: <k> runLemma ( 36 *Int B >Int 1728 ) => doneLemma ( B >Int 48 ) ... </k>
claim [mul-ge-const]: <k> runLemma ( 36 *Int B >=Int 1728 ) => doneLemma ( B >=Int 48 ) ... </k>

claim [const-gt-mul]: <k> runLemma ( 1728 >Int 36 *Int B ) => doneLemma ( 48 >Int B ) ... </k>
claim [const-ge-mul]: <k> runLemma ( 1728 >=Int 36 *Int B ) => doneLemma ( 48 >=Int B ) ... </k>
claim [const-lt-mul]: <k> runLemma ( 1728 <Int 36 *Int B ) => doneLemma ( 48 <Int B ) ... </k>
claim [const-le-mul]: <k> runLemma ( 1728 <=Int 36 *Int B ) => doneLemma ( 48 <=Int B ) ... </k>

claim [eq-neg]: <k> runLemma ( A ==Int -1 ) => doneLemma ( false ) ... </k>
requires 0 <=Int A

claim [nonneg-and-nonzero]: <k> runLemma ( 0 <Int X ) => doneLemma ( true ) ... </k>
requires 0 <=Int X andBool notBool ( X ==Int 0 )

claim [le-maxuint256]: <k> runLemma ( X <=Int maxUInt256 ) => doneLemma ( X <Int pow256 ) ... </k>

Comment on lines +154 to +181
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These claims pass even without the corresponding lemmas, but only because the SMT solver can prove the implication. The lemmas are needed if we want to actually simplify the expressions.


// Sets
// ----
Expand Down Expand Up @@ -657,6 +706,12 @@ module LEMMAS-SPEC
claim [shift-range]: <k> runLemma ( #rangeUInt ( 256 , X <<Int 16 ) ) => doneLemma ( true ) ... </k> requires #rangeUInt ( 16 , X )
claim [shift-mod]: <k> runLemma ( ( X <<Int 16 ) modInt pow256 ) => doneLemma ( X <<Int 16 ) ... </k> requires #rangeUInt ( 16 , X )

// xor
// -----

claim [xorInt-range]: <k> runLemma ( #rangeUInt ( 256 , X xorInt Y ) ) => doneLemma ( true ) ... </k> requires #rangeUInt ( 256 , X ) andBool #rangeUInt ( 256 , Y )
claim [xorInt-to-if]: <k> runLemma ( A xorInt ( bool2Word ( A <=Int B ) *Int ( A xorInt B ) ) ) => doneLemma ( #if ( A <=Int B ) #then B #else A #fi ) ... </k>

// concat
// ------

Expand Down Expand Up @@ -769,6 +824,13 @@ module LEMMAS-SPEC
requires #asWord ( BA3 ) ==Int X modInt ( 2 ^Int ( 8 *Int lengthBytes ( BA3 ) ) )
andBool 0 <Int lengthBytes(BA1) andBool lengthBytes(BA2 +Bytes BA3) ==Int 32

claim [asWord-lt-concat-left]:
<k> runLemma (
#asWord ( B1 +Bytes b"\xde\xad\xbe\xef" ) <Int #asWord ( b"\xfa\xca\xde\x00\x00\x00\x00" )
) => doneLemma (
#asWord ( B1 ) <Int #asWord ( b"\xfa\xca\xde")
) ... </k>

// bool2Word
// ---------

Expand Down