Skip to content

Commit

Permalink
Stabilising bool2Word reasoning (#2605)
Browse files Browse the repository at this point in the history 
* stabilising bool2word

* removing unneeded test

* adding rangeBool lemmas

* reformulation

* correction

* improving simplifications

* injectivity of bool2Word

* correction

* removing lemmas

* correction

* correction

* review corrections

* review corrections

* stabilising CI

* alignment

* alignment

* alignment

* alignment

* alignment

* Update test-pr.yml

* tests

* consistent naming of lemmas

---------

Co-authored-by: Andrei Văcaru <[email protected]>
  • Loading branch information
@PetarMax @anvacaru
PetarMax and anvacaru authored Sep 6, 2024
1 parent de6b0d8 commit c6e01ac
Show file tree
Hide file tree
Showing 6 changed files with 102 additions and 31 deletions.
4 changes: 2 additions & 2 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,8 +27,8 @@ Primitives provide the basic conversion from K's sorts `Int` and `Bool` to EVM's
- `word2Bool` interprets a `Int` as a `Bool`.

```k
syntax Int ::= bool2Word ( Bool ) [symbol(bool2Word), function, total, smtlib(bool2Word)]
// -----------------------------------------------------------------------------------------
syntax Int ::= bool2Word ( Bool ) [symbol(bool2Word), function, total, injective, smtlib(bool2Word)]
// ----------------------------------------------------------------------------------------------------
rule bool2Word( true ) => 1
rule bool2Word( false ) => 0
Expand Down
74 changes: 56 additions & 18 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,23 +48,69 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]

rule 0 <=Int #sizeWordStack ( _ , N ) => true requires 0 <=Int N [simplification, smt-lemma]

// bool2Word range & simplification
rule 0 <=Int bool2Word(_B) => true [simplification]
rule bool2Word(_B) <Int pow256 => true [simplification]

rule bool2Word(A) |Int bool2Word(B) => bool2Word(A orBool B) [simplification]
rule bool2Word(A) &Int bool2Word(B) => bool2Word(A andBool B) [simplification]

rule 1 |Int bool2Word(_B) => 1 [simplification]
rule 1 &Int bool2Word( B) => bool2Word(B) [simplification]

// #newAddr range
rule 0 <=Int #newAddr(_,_) => true [simplification]
rule #newAddr(_,_) <Int pow160 => true [simplification]
rule #newAddr(_,_) <Int pow256 => true [simplification]

rule #isPrecompiledAccount(#newAddr(_, _), _) => false [simplification]

// ########################
// #rangeBool reasoning
// ########################

rule [rangeBool-not-zero-l]: notBool (X ==Int 0) => X ==Int 1 requires #rangeBool(X) [simplification]
rule [rangeBool-not-zero-r]: notBool (0 ==Int X) => X ==Int 1 requires #rangeBool(X) [simplification]
rule [rangeBool-not-one-l]: notBool (X ==Int 1) => X ==Int 0 requires #rangeBool(X) [simplification]
rule [rangeBool-not-one-r]: notBool (1 ==Int X) => X ==Int 0 requires #rangeBool(X) [simplification]

// ########################
// bool2Word reasoning
// ########################

// Range
rule [b2w-lb]: 0 <=Int bool2Word(_) => true [simplification, smt-lemma]
rule [b2w-ub]: bool2Word(_) <=Int 1 => true [simplification, smt-lemma]

// Relationship with equality
rule [b2w-eq-zero]: bool2Word(B) ==Int 0 => notBool B [simplification(30), comm]
rule [b2w-eq-one]: bool2Word(B) ==Int 1 => B [simplification(30), comm]

// Relationship with other comparators
rule [b2w-lt-one]: bool2Word(B) <Int 1 => notBool B [simplification(30)]
rule [b2w-gt-zero]: 0 <Int bool2Word(B) => B [simplification(30)]

rule [b2w-lt-true]: bool2Word(_) <Int X:Int => true requires 1 <Int X [simplification(30), concrete(X)]
rule [b2w-gt-false]: X:Int <Int bool2Word(_) => false requires 1 <=Int X [simplification(30), concrete(X)]

rule [b2w-lt-b2w]: bool2Word(A) <Int bool2Word(B) => notBool A andBool B [simplification(30)]
rule [b2w-le-b2w]: bool2Word(A) <=Int bool2Word(B) => A orBool notBool B [simplification(30)]

// Relationship with `&Int`
rule [b2w-band-one]: 1 &Int bool2Word(B) => bool2Word(B) [simplification]
rule [b2w-band]: bool2Word(A) &Int bool2Word(B) => bool2Word(A andBool B) [simplification]

// Relationship with `|Int`
rule [b2w-bor-one]: 1 |Int bool2Word(_) => 1 [simplification]
rule [b2w-bor]: bool2Word(A) |Int bool2Word(B) => bool2Word(A orBool B) [simplification]

// Relationship with `xorInt`
rule [b2w-bxor-zero]: 0 xorInt bool2Word(Y) => bool2Word(Y) [simplification, comm]
rule [b2w-bxor-one]: 1 xorInt bool2Word(Y) => bool2Word(notBool Y) [simplification, comm]
rule [b2w-bxor]: bool2Word(X) xorInt bool2Word(Y) => bool2Word ( (X andBool notBool Y) orBool (notBool X andBool Y) ) [simplification]

// As part of multiplication
rule [b2w-mul-lt-l]: bool2Word(B) *Int C <Int A => (B andBool C <Int A) orBool (notBool B andBool 0 <Int A) [simplification]
rule [b2w-mul-le-l]: bool2Word(B) *Int C <=Int A => (B andBool C <=Int A) orBool (notBool B andBool 0 <=Int A) [simplification]
rule [b2w-mul-eq-l]: bool2Word(B) *Int C ==Int A => (B andBool C ==Int A) orBool (notBool B andBool A ==Int 0) [simplification, comm]

rule [b2w-mul-lt-r]: C *Int bool2Word(B) <Int A => (B andBool C <Int A) orBool (notBool B andBool 0 <Int A) [simplification]
rule [b2w-mul-le-r]: C *Int bool2Word(B) <=Int A => (B andBool C <=Int A) orBool (notBool B andBool 0 <=Int A) [simplification]
rule [b2w-mul-eq-r]: C *Int bool2Word(B) ==Int A => (B andBool C ==Int A) orBool (notBool B andBool A ==Int 0) [simplification, comm]

// As part of how the compiler returns a bool from storage
rule [b2w-storage]: bool2Word(X ==Int 1) => X requires #rangeBool(X) [simplification]

// ########################
// Keccak
// ########################
Expand Down Expand Up @@ -161,14 +207,6 @@ module LEMMAS-HASKELL [symbolic]
requires 0 <Int D andBool D <Int pow256 andBool D ==Int 256 ^Int log256Int(D)
andBool log256Int(D) <=Int lengthBytes(BUF) [simplification, preserves-definedness]

rule notBool (X ==Int 0) => X ==Int 1 requires #rangeBool(X) [simplification]
rule notBool (X ==Int 1) => X ==Int 0 requires #rangeBool(X) [simplification]
rule bool2Word(X ==Int 1) => X requires #rangeBool(X) [simplification]

//Simplification of bool2Word() ==Int CONCRETE, #buf() ==K CONCRETE
rule I ==Int bool2Word( B:Bool ) => bool2Word(B) ==Int I [simplification, concrete(I)]
rule bool2Word( B:Bool ) ==Int I => B ==K word2Bool(I) [simplification, concrete(I)]

// ########################
// Arithmetic
// ########################
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -481,7 +481,7 @@ Range of types
| #rangeSmall ( Int ) [symbol(rangeSmall) , alias]
| #rangeBlockNum ( Int ) [symbol(rangeBlockNum), alias]
// ---------------------------------------------------------------------------------
rule #rangeBool ( X ) => X ==Int 0 orBool X ==Int 1
rule #rangeBool ( X ) => #range ( 0 <= X < 2 )
rule #rangeSInt ( 8 , X ) => #range ( minSInt8 <= X <= maxSInt8 )
rule #rangeSInt ( 16 , X ) => #range ( minSInt16 <= X <= maxSInt16 )
Expand Down
48 changes: 43 additions & 5 deletions tests/specs/functional/lemmas-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,11 +18,6 @@ endmodule
module LEMMAS-SPEC
imports VERIFICATION

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

claim <k> runLemma ( bool2Word((UINT8 ==K 0) ==K false) ) => doneLemma ( UINT8 ) ... </k> requires #rangeBool(UINT8)

// sizeBytes
// -------------

Expand Down Expand Up @@ -654,6 +649,49 @@ module LEMMAS-SPEC
) ... </k>
requires lengthBytes ( VV0_data_114b9705:Bytes ) <=Int 1073741824

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

// b2w-gt-zero, b2w-lt-b2w, b2w-band-one, b2w-band, b2w-mul-lt-l
claim [b2w-01]:
<k> runLemma (
( bool2Word( 0 <=Int X:Int ) &Int 1 ) *Int bool2Word( X <Int -5 ) <Int ( bool2Word( 5 <=Int X ) &Int bool2Word( X <=Int 10 ) )
) => doneLemma (
5 <=Int X andBool X <=Int 10
) ... </k>

// b2w-eq-zero, b2w-xor-zero, b2w-xor-one, b2w-xor, b2w-mul-eq-l
claim [b2w-02]:
<k> runLemma (
( bool2Word( 0 <=Int X:Int ) *Int ( 0 xorInt bool2Word( X <=Int 0 ) ) ) ==Int 1 xorInt ( bool2Word( X <=Int 0 ) xorInt bool2Word( X >=Int 0 ) )
) => doneLemma (
true
) ... </k>

// b2w-lt-one, b2w-bor-one, b2w-mul-le-l
claim [b2w-03]:
<k> runLemma (
( bool2Word ( 0 <=Int X:Int ) *Int bool2Word( 0 <Int X ) ) <Int 1 |Int bool2Word( X =/=Int X )
) => doneLemma (
X <=Int 0
) ... </k>

// b2w-gt-false, b2w-mul-lt-r
claim [b2w-04]:
<k> runLemma (
( bool2Word ( notBool X ) *Int 42 ) <Int bool2Word ( Y )
) => doneLemma (
X andBool Y
) ... </k>

// b2w-lt-true
claim [b2w-05]:
<k> runLemma (
bool2Word ( _X ) *Int bool2Word ( _Y ) <Int 42
) => doneLemma (
true
) ... </k>

// ecrecover
// ---------

Expand Down
2 changes: 0 additions & 2 deletions tests/specs/mcd-structured/verification.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,8 +63,6 @@ module LEMMAS-MCD [symbolic]

rule chop(X) ==Int 0 => X ==Int 0 requires #rangeSInt(256, X) [simplification]

rule bool2Word( X:Bool ) |Int bool2Word( Y:Bool ) => bool2Word(X orBool Y) [simplification]

rule [add-cancel-ml-01]: { A +Int B #Equals A } => { B #Equals 0 } [simplification]
rule [add-cancel-ml-02]: { A +Int B #Equals C +Int B } => { A #Equals C } [simplification]

Expand Down
3 changes: 0 additions & 3 deletions tests/specs/mcd/verification.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,9 +63,6 @@ module LEMMAS-MCD [symbolic]

rule chop(X) ==Int 0 => X ==Int 0 requires #rangeSInt(256, X) [simplification, comm]

rule bool2Word( X:Bool ) |Int bool2Word( Y:Bool ) => bool2Word(X orBool Y) [simplification]
rule bool2Word( X:Bool ) ==Int 0 => notBool X [simplification]

// ### vat-subui-fail-rough
//
// Via Z3 4.8.7
Expand Down

0 comments on commit c6e01ac

Please sign in to comment.