Skip to content
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

Jump to bottom

Generalising bitwise simplifications #2251

Merged
merged 8 commits into from
Jan 11, 2024
Merged

Generalising bitwise simplifications #2251

Show file tree
Hide file tree
Changes from 6 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
a01af41
Generalising bitwise simplifications
PetarMax Jan 10, 2024
3d99ad7
Set Version: 1.0.411
Jan 10, 2024
ad3809f
Merge branch 'master' into bitwise-simplifications
PetarMax Jan 11, 2024
61f0739
Set Version: 1.0.413
Jan 11, 2024
959c6a0
Merge branch 'master' into bitwise-simplifications
PetarMax Jan 11, 2024
3d90ec9
Set Version: 1.0.414
Jan 11, 2024
398523c
#rangeUInt
PetarMax Jan 11, 2024
808e551
Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simpl…
PetarMax Jan 11, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
2 changes: 1 addition & 1 deletion kevm-pyk/pyproject.toml
View file
Open in desktop
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. <contact@runtimeverification.com>",
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/__init__.py
View file
Open in desktop
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
Open in desktop
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 0 <=Int X andBool X <Int pow256
ehildenb marked this conversation as resolved.
Show resolved Hide resolved
andBool 2 ^Int ( log2Int ( pow256 -Int X ) ) ==Int pow256 -Int X
andBool 0 <=Int Y andBool Y <=Int pow256 -Int X
PetarMax marked this conversation as resolved.
Show resolved Hide resolved
[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 0 <=Int X andBool X <Int pow256
ehildenb marked this conversation as resolved.
Show resolved Hide resolved
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
Open in desktop
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
Open in desktop
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