Skip to content

Commit

Permalink
Generalising bitwise simplifications (#2251)
Browse files Browse the repository at this point in the history 
* Generalising bitwise simplifications

* Set Version: 1.0.411

* Set Version: 1.0.413

* Set Version: 1.0.414

* #rangeUInt

* Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k

Co-authored-by: Everett Hildenbrandt <[email protected]>

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>
  • Loading branch information
@PetarMax @ehildenb
3 people authored Jan 11, 2024
1 parent dca9426 commit 1c48ff2
Show file tree
Hide file tree
Showing 5 changed files with 69 additions and 64 deletions.
2 changes: 1 addition & 1 deletion kevm-pyk/pyproject.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "kevm-pyk"
version = "1.0.413"
version = "1.0.414"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/__init__.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,4 +6,4 @@
from typing import Final


VERSION: Final = '1.0.413'
VERSION: Final = '1.0.414'
57 changes: 25 additions & 32 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,11 +34,12 @@ module BITWISE-SIMPLIFICATION [symbolic]
rule maxUInt48 &Int X <Int pow48 => true requires 0 <=Int X [simplification, smt-lemma]
rule maxUInt160 &Int X <Int pow160 => true requires 0 <=Int X [simplification, smt-lemma]

rule [bitwise-and-identity]:
// Generalization of: maxUIntXXX &Int Y => Y requires #rangeUInt(XXX, Y)
rule [bitwise-and-maxUInt-identity]:
X &Int Y => Y
requires 0 <=Int X
andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
andBool 0 <=Int Y andBool Y <Int 2 ^Int log2Int(X +Int 1)
andBool 0 <=Int Y andBool Y <Int X +Int 1
[concrete(X), simplification, comm]

rule [bitwise-or-geq-zero]: 0 <=Int (X |Int Y) => true requires 0 <=Int X andBool 0 <=Int Y [simplification]
Expand All @@ -47,36 +48,28 @@ module BITWISE-SIMPLIFICATION [symbolic]
rule [bitwise-and-lt]: (X &Int Y) <Int Z => true requires 0 <=Int X andBool 0 <=Int Y andBool (X <Int Z orBool Y <Int Z) [simplification]
rule [bitwise-or-lt-pow256]: (X |Int Y) <Int pow256 => true requires 0 <=Int X andBool 0 <=Int Y andBool X <Int pow256 andBool Y <Int pow256 [simplification]

// We should probably generalize the simplifications below for relevant powers of two.
rule notMaxUInt5 &Int X => 0 requires #rangeUInt( 5, X) [simplification]
rule notMaxUInt8 &Int X => 0 requires #rangeUInt( 8, X) [simplification]
rule notMaxUInt16 &Int X => 0 requires #rangeUInt( 16, X) [simplification]
rule notMaxUInt32 &Int X => 0 requires #rangeUInt( 32, X) [simplification]
rule notMaxUInt64 &Int X => 0 requires #rangeUInt( 64, X) [simplification]
rule notMaxUInt96 &Int X => 0 requires #rangeUInt( 96, X) [simplification]
rule notMaxUInt128 &Int X => 0 requires #rangeUInt(128, X) [simplification]
rule notMaxUInt160 &Int X => 0 requires #rangeUInt(160, X) [simplification]
rule notMaxUInt192 &Int X => 0 requires #rangeUInt(192, X) [simplification]
rule notMaxUInt208 &Int X => 0 requires #rangeUInt(208, X) [simplification]
rule notMaxUInt224 &Int X => 0 requires #rangeUInt(224, X) [simplification]
rule notMaxUInt240 &Int X => 0 requires #rangeUInt(240, X) [simplification]
rule notMaxUInt248 &Int X => 0 requires #rangeUInt(248, X) [simplification]

rule notMaxUInt240 &Int (X <<Int 240) => X <<Int 240 requires #rangeUInt(16, X) [simplification]
rule notMaxUInt248 &Int (X <<Int 248) => X <<Int 248 requires #rangeUInt( 8, X) [simplification]

rule maxUInt8 &Int (X |Int (notMaxUInt8 &Int _)) => maxUInt8 &Int X [simplification]
rule maxUInt16 &Int (X |Int (notMaxUInt16 &Int _)) => maxUInt16 &Int X [simplification]
rule maxUInt32 &Int (X |Int (notMaxUInt32 &Int _)) => maxUInt32 &Int X [simplification]
rule maxUInt64 &Int (X |Int (notMaxUInt64 &Int _)) => maxUInt64 &Int X [simplification]
rule maxUInt96 &Int (X |Int (notMaxUInt96 &Int _)) => maxUInt96 &Int X [simplification]
rule maxUInt128 &Int (X |Int (notMaxUInt128 &Int _)) => maxUInt128 &Int X [simplification]
rule maxUInt160 &Int (X |Int (notMaxUInt160 &Int _)) => maxUInt160 &Int X [simplification]
rule maxUInt192 &Int (X |Int (notMaxUInt192 &Int _)) => maxUInt192 &Int X [simplification]
rule maxUInt208 &Int (X |Int (notMaxUInt208 &Int _)) => maxUInt208 &Int X [simplification]
rule maxUInt224 &Int (X |Int (notMaxUInt224 &Int _)) => maxUInt224 &Int X [simplification]
rule maxUInt240 &Int (X |Int (notMaxUInt240 &Int _)) => maxUInt240 &Int X [simplification]
rule maxUInt248 &Int (X |Int (notMaxUInt248 &Int _)) => maxUInt248 &Int X [simplification]
// Generalization of: notMaxUIntXXX &Int Y => 0 requires #rangeUInt(XXX, Y)
rule [bitwise-and-notMaxUInt-zero]:
X &Int Y => 0
requires #rangeUInt(256, X)
andBool 2 ^Int ( log2Int ( pow256 -Int X ) ) ==Int pow256 -Int X
andBool 0 <=Int Y andBool Y <Int pow256 -Int X
[simplification, concrete(X)]

// Generalization of: notMaxUIntXXX &Int (Y <<Int XXX) => Y <<Int XXX requires #rangeUInt(256 -Int XXX, Y)
rule X &Int (Y <<Int Z) => Y <<Int Z
requires #rangeUInt(256, X)
andBool 2 ^Int ( log2Int ( pow256 -Int X ) ) ==Int pow256 -Int X
andBool Z ==Int log2Int ( pow256 -Int X )
andBool 0 <=Int Y andBool Y <Int 2 ^Int ( 256 -Int Z )
[simplification, concrete(X, Z), comm]

// Generalization of: maxUIntXXX &Int (Y |Int (notMaxUIntXXX &Int T)) => maxUIntXXX &Int Y
rule X &Int (Y |Int (Z &Int T)) => X &Int Y
requires 0 <=Int X andBool 0 <=Int Y andBool 0 <=Int Z andBool 0 <=Int T
andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
andBool X +Int Z ==Int maxUInt256
[simplification, concrete(X, Z), comm]

rule [lengthBytes-upInt-32-lower-bound]:
lengthBytes(X) <=Int notMaxUInt5 &Int ( lengthBytes(X) +Int 31 ) => true
Expand Down
2 changes: 1 addition & 1 deletion package/version
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
1.0.413
1.0.414
70 changes: 41 additions & 29 deletions tests/specs/functional/lemmas-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -465,35 +465,47 @@ module LEMMAS-SPEC
// bitwise
// -------

claim <k> runLemma ( notMaxUInt5 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 5 , X )
claim <k> runLemma ( notMaxUInt8 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 8 , X )
claim <k> runLemma ( notMaxUInt16 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 16 , X )
claim <k> runLemma ( notMaxUInt32 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 32 , X )
claim <k> runLemma ( notMaxUInt64 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 64 , X )
claim <k> runLemma ( notMaxUInt96 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 96 , X )
claim <k> runLemma ( notMaxUInt128 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 128 , X )
claim <k> runLemma ( notMaxUInt160 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 160 , X )
claim <k> runLemma ( notMaxUInt192 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 192 , X )
claim <k> runLemma ( notMaxUInt208 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 208 , X )
claim <k> runLemma ( notMaxUInt224 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 224 , X )
claim <k> runLemma ( notMaxUInt240 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 240 , X )
claim <k> runLemma ( notMaxUInt248 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 248 , X )

claim <k> runLemma ( notMaxUInt240 &Int ( X <<Int 240 ) ) => doneLemma( X <<Int 240 ) ... </k> requires #rangeUInt ( 16 , X )
claim <k> runLemma ( notMaxUInt248 &Int ( X <<Int 248 ) ) => doneLemma( X <<Int 248 ) ... </k> requires #rangeUInt ( 8 , X )

claim <k> runLemma ( maxUInt8 &Int ( X |Int ( notMaxUInt8 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 8 , X )
claim <k> runLemma ( maxUInt16 &Int ( X |Int ( notMaxUInt16 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 16 , X )
claim <k> runLemma ( maxUInt32 &Int ( X |Int ( notMaxUInt32 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 32 , X )
claim <k> runLemma ( maxUInt64 &Int ( X |Int ( notMaxUInt64 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 64 , X )
claim <k> runLemma ( maxUInt96 &Int ( X |Int ( notMaxUInt96 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 96 , X )
claim <k> runLemma ( maxUInt128 &Int ( X |Int ( notMaxUInt128 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 128 , X )
claim <k> runLemma ( maxUInt160 &Int ( X |Int ( notMaxUInt160 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 160 , X )
claim <k> runLemma ( maxUInt192 &Int ( X |Int ( notMaxUInt192 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 192 , X )
claim <k> runLemma ( maxUInt208 &Int ( X |Int ( notMaxUInt208 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 208 , X )
claim <k> runLemma ( maxUInt224 &Int ( X |Int ( notMaxUInt224 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 224 , X )
claim <k> runLemma ( maxUInt240 &Int ( X |Int ( notMaxUInt240 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 240 , X )
claim <k> runLemma ( maxUInt248 &Int ( X |Int ( notMaxUInt248 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 248 , X )
claim [bit-n005-0]: <k> runLemma ( notMaxUInt5 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 5 , X )
claim [bit-n008-0]: <k> runLemma ( notMaxUInt8 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 8 , X )
claim [bit-n016-0]: <k> runLemma ( notMaxUInt16 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 16 , X )
claim [bit-n032-0]: <k> runLemma ( notMaxUInt32 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 32 , X )
claim [bit-n064-0]: <k> runLemma ( notMaxUInt64 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 64 , X )
claim [bit-n096-0]: <k> runLemma ( notMaxUInt96 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 96 , X )
claim [bit-n128-0]: <k> runLemma ( notMaxUInt128 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 128 , X )
claim [bit-n160-0]: <k> runLemma ( notMaxUInt160 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 160 , X )
claim [bit-n192-0]: <k> runLemma ( notMaxUInt192 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 192 , X )
claim [bit-n208-0]: <k> runLemma ( notMaxUInt208 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 208 , X )
claim [bit-n224-0]: <k> runLemma ( notMaxUInt224 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 224 , X )
claim [bit-n240-0]: <k> runLemma ( notMaxUInt240 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 240 , X )
claim [bit-n248-0]: <k> runLemma ( notMaxUInt248 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 248 , X )

claim [bit-n005-shl]: <k> runLemma ( notMaxUInt5 &Int ( X <<Int 5 ) ) => doneLemma( X <<Int 5 ) ... </k> requires 0 <=Int X andBool X <Int 2 ^Int 249
claim [bit-n008-shl]: <k> runLemma ( notMaxUInt8 &Int ( X <<Int 8 ) ) => doneLemma( X <<Int 8 ) ... </k> requires #rangeUInt ( 248 , X )
claim [bit-n016-shl]: <k> runLemma ( notMaxUInt16 &Int ( X <<Int 16 ) ) => doneLemma( X <<Int 16 ) ... </k> requires #rangeUInt ( 240 , X )
claim [bit-n032-shl]: <k> runLemma ( notMaxUInt32 &Int ( X <<Int 32 ) ) => doneLemma( X <<Int 32 ) ... </k> requires #rangeUInt ( 224 , X )
claim [bit-n064-shl]: <k> runLemma ( notMaxUInt64 &Int ( X <<Int 64 ) ) => doneLemma( X <<Int 64 ) ... </k> requires #rangeUInt ( 192 , X )
claim [bit-n096-shl]: <k> runLemma ( notMaxUInt96 &Int ( X <<Int 96 ) ) => doneLemma( X <<Int 96 ) ... </k> requires #rangeUInt ( 160 , X )
claim [bit-n128-shl]: <k> runLemma ( notMaxUInt128 &Int ( X <<Int 128 ) ) => doneLemma( X <<Int 128 ) ... </k> requires #rangeUInt ( 128 , X )
claim [bit-n160-shl]: <k> runLemma ( notMaxUInt160 &Int ( X <<Int 160 ) ) => doneLemma( X <<Int 160 ) ... </k> requires #rangeUInt ( 96 , X )
claim [bit-n192-shl]: <k> runLemma ( notMaxUInt192 &Int ( X <<Int 192 ) ) => doneLemma( X <<Int 192 ) ... </k> requires #rangeUInt ( 64 , X )
claim [bit-n208-shl]: <k> runLemma ( notMaxUInt208 &Int ( X <<Int 208 ) ) => doneLemma( X <<Int 208 ) ... </k> requires #rangeUInt ( 48 , X )
claim [bit-n224-shl]: <k> runLemma ( notMaxUInt224 &Int ( X <<Int 224 ) ) => doneLemma( X <<Int 224 ) ... </k> requires #rangeUInt ( 32 , X )
claim [bit-n240-shl]: <k> runLemma ( notMaxUInt240 &Int ( X <<Int 240 ) ) => doneLemma( X <<Int 240 ) ... </k> requires #rangeUInt ( 16 , X )
claim [bit-n248-shl]: <k> runLemma ( notMaxUInt248 &Int ( X <<Int 248 ) ) => doneLemma( X <<Int 248 ) ... </k> requires #rangeUInt ( 8 , X )

claim [bit-005-m-or-nm]: <k> runLemma ( maxUInt5 &Int ( X |Int ( notMaxUInt5 &Int T ) ) ) => doneLemma( X ) ... </k> requires 0 <=Int X andBool X <Int 2 ^Int 5 andBool 0 <=Int T
claim [bit-008-m-or-nm]: <k> runLemma ( maxUInt8 &Int ( X |Int ( notMaxUInt8 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 8 , X ) andBool 0 <=Int T
claim [bit-016-m-or-nm]: <k> runLemma ( maxUInt16 &Int ( X |Int ( notMaxUInt16 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 16 , X ) andBool 0 <=Int T
claim [bit-032-m-or-nm]: <k> runLemma ( maxUInt32 &Int ( X |Int ( notMaxUInt32 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 32 , X ) andBool 0 <=Int T
claim [bit-064-m-or-nm]: <k> runLemma ( maxUInt64 &Int ( X |Int ( notMaxUInt64 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 64 , X ) andBool 0 <=Int T
claim [bit-096-m-or-nm]: <k> runLemma ( maxUInt96 &Int ( X |Int ( notMaxUInt96 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 96 , X ) andBool 0 <=Int T
claim [bit-128-m-or-nm]: <k> runLemma ( maxUInt128 &Int ( X |Int ( notMaxUInt128 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 128 , X ) andBool 0 <=Int T
claim [bit-160-m-or-nm]: <k> runLemma ( maxUInt160 &Int ( X |Int ( notMaxUInt160 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 160 , X ) andBool 0 <=Int T
claim [bit-192-m-or-nm]: <k> runLemma ( maxUInt192 &Int ( X |Int ( notMaxUInt192 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 192 , X ) andBool 0 <=Int T
claim [bit-208-m-or-nm]: <k> runLemma ( maxUInt208 &Int ( X |Int ( notMaxUInt208 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 208 , X ) andBool 0 <=Int T
claim [bit-224-m-or-nm]: <k> runLemma ( maxUInt224 &Int ( X |Int ( notMaxUInt224 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 224 , X ) andBool 0 <=Int T
claim [bit-240-m-or-nm]: <k> runLemma ( maxUInt240 &Int ( X |Int ( notMaxUInt240 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 240 , X ) andBool 0 <=Int T
claim [bit-248-m-or-nm]: <k> runLemma ( maxUInt248 &Int ( X |Int ( notMaxUInt248 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 248 , X ) andBool 0 <=Int T

claim <k> runLemma ( #buf ( 32 , #asWord ( X ) ) ) => doneLemma( X ) </k> requires lengthBytes(X) ==Int 32
claim <k> runLemma ( #buf ( 32 , X <<Int 248 ) ) => doneLemma( #buf ( 1 , X ) +Bytes #buf ( 31 , 0 ) ) ... </k> requires #rangeUInt ( 8 , X )
Expand Down

0 comments on commit 1c48ff2

Please sign in to comment.