Skip to content

Commit

Permalink
Adding further lemmas for bitwise reasoning (#2270)
Browse files Browse the repository at this point in the history 
* adding further lemmas for bitwise reasoning

* Set Version: 1.0.431

* prioritising simplifications

* Set Version: 1.0.432

* adding additional lemmas to attempt to make the tests pass

* correcting claims

* further lemmas

* refining lemmas

* refining lemmas

* upper limit on #asWord of #range

* Set Version: 1.0.433

* adding further simplifications

* Set Version: 1.0.436

* additional lemma for symbolic bytes reasoning

* Set Version: 1.0.438

* removing superflous simplifications

* Set Version: 1.0.439

* removing incorrect simplification

* Set Version: 1.0.441

* Set Version: 1.0.443

* Set Version: 1.0.444

* changing order of requires to try to preserve definedness

* Set Version: 1.0.445

* merge with master

* Set Version: 1.0.446

* Set Version: 1.0.447

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Andrei Văcaru <[email protected]>
  • Loading branch information
@PetarMax @anvacaru
3 people authored Feb 8, 2024
1 parent e2d5d20 commit 4e6b958
Show file tree
Hide file tree
Showing 9 changed files with 171 additions and 34 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.446"
version = "1.0.447"
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.446'
VERSION: Final = '1.0.447'
41 changes: 30 additions & 11 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
@@ -1,6 +1,7 @@
requires "word.md"

module BITWISE-SIMPLIFICATION [symbolic]
imports EVM-TYPES
imports INT-SYMBOLIC
imports WORD

Expand Down Expand Up @@ -34,14 +35,6 @@ 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]

// 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 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, smt-lemma]
rule [bitwise-and-geq-zero]: 0 <=Int (X &Int Y) => true requires 0 <=Int X andBool 0 <=Int Y [simplification, smt-lemma]

Expand All @@ -51,14 +44,38 @@ 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]

// 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 X +Int 1
[concrete(X), simplification, comm]

// 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 pow256 -Int X ==Int 2 ^Int ( log2Int ( pow256 -Int X ) )
andBool 0 <=Int Y andBool Y <Int pow256 -Int X
[simplification, concrete(X)]

// Generalization of: maxUIntXXX &Int #asWord ( BA )
rule X &Int #asWord ( BA ) => #asWord ( #range(BA, 32 -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) )
requires #rangeUInt(256, X)
andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
andBool log2Int (X +Int 1) modInt 8 ==Int 0
andBool lengthBytes(BA) ==Int 32
[simplification, concrete(X), preserves-definedness]

// Generalization of: notMaxUIntXXX &Int #asWord ( BA )
rule X &Int #asWord ( BA ) => #asWord ( #range ( BA, 0, 32 -Int log2Int(pow256 -Int X) /Int 8 ) +Bytes padRightBytes(.Bytes, log2Int(pow256 -Int X) /Int 8, 0 ) )
requires #rangeUInt(256, X)
andBool pow256 -Int X ==Int 2 ^Int ( log2Int ( pow256 -Int X ) )
andBool log2Int ( pow256 -Int X ) modInt 8 ==Int 0
andBool lengthBytes(BA) ==Int 32
[simplification, concrete(X), preserves-definedness]

// 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)
Expand All @@ -67,10 +84,12 @@ module BITWISE-SIMPLIFICATION [symbolic]
andBool 0 <=Int Y andBool Y <Int 2 ^Int ( 256 -Int Z )
[simplification, concrete(X, Z), comm, preserves-definedness]

// Generalization of: maxUIntXXX &Int (Y |Int (notMaxUIntXXX &Int T)) => maxUIntXXX &Int Y
// Generalization of: maxUIntXXX &Int (Y |Int (notMaxUIntXXX &Int T)) => maxUIntXXX &Int Y
// and notMaxUIntXXX &Int (Y |Int ( maxUIntXXX &Int T)) => notMaxUIntXXX &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 1 ==Int 2 ^Int log2Int ( X +Int 1 ) orBool // X is a maxUInt
pow256 -Int X ==Int 2 ^Int log2Int ( pow256 -Int X ) ) // X is a notMaxUInt
andBool X +Int Z ==Int maxUInt256
[simplification, concrete(X, Z), comm]

Expand Down
51 changes: 50 additions & 1 deletion kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,11 +59,24 @@ module BYTES-SIMPLIFICATION [symbolic]
requires lengthBytes(B) <=Int 32
andBool #rangeUInt(256, X) [simplification, concrete(B), comm]

rule [buf-asWord-invert]:
rule [buf-asWord-invert-lr]:
#buf (W:Int , #asWord(B:Bytes)) => #buf(W -Int lengthBytes(B), 0) +Bytes B
requires lengthBytes(B) <=Int W andBool W <=Int 32
[simplification]

rule [buf-asWord-invert-rl]:
#asWord ( #buf ( WB:Int, X:Int ) ) => X
requires 0 <=Int WB andBool WB <=Int 32
andBool 0 <=Int X andBool X <Int 2 ^Int (WB *Int 8)
[simplification, concrete(WB)]

rule [buf-asWord-invert-rl-range]:
#asWord ( #range ( #buf ( WB:Int, X:Int ), S:Int, WR:Int ) ) => X
requires 0 <=Int WB andBool 0 <=Int X andBool 0 <=Int S andBool 0 <=Int WR
andBool S +Int WR ==Int WB
andBool X <Int 2 ^Int (WR *Int 8)
[simplification, concrete(WB, S, WR)]

rule [buf-zero-concat-base]:
#buf(W1:Int, 0) +Bytes #buf(W2:Int, 0) => #buf(W1 +Int W2, 0)
requires 0 <=Int W1 andBool 0 <=Int W2
Expand Down Expand Up @@ -166,6 +179,18 @@ module BYTES-SIMPLIFICATION [symbolic]
andBool #asInteger(B) ==Int 0
[concrete(B), simplification]

rule [range-buf-zero-concat]:
B:Bytes +Bytes #buf(W:Int, X:Int) => #buf(lengthBytes(B) +Int W, X)
requires 0 <=Int W andBool 0 <=Int X andBool X <Int 2 ^Int (W *Int 8)
andBool #asInteger(B) ==Int 0
[concrete(B, W), simplification]

rule [range-buf-zero-concat-extend]:
B1:Bytes +Bytes #buf(W:Int, X:Int) +Bytes B2 => #buf(lengthBytes(B1) +Int W, X) +Bytes B2
requires 0 <=Int W andBool 0 <=Int X andBool X <Int 2 ^Int (W *Int 8)
andBool #asInteger(B1) ==Int 0
[concrete(B1, W), simplification]

rule [range-memUpdate-before]:
#range(B1:Bytes [ S1:Int := B2:Bytes ], S2:Int, W2:Int) =>
#let W = minInt(W2, S1 -Int S2) #in
Expand All @@ -191,10 +216,34 @@ module BYTES-SIMPLIFICATION [symbolic]
andBool 0 <=Int S2 andBool 0 <=Int W2 andBool S2 +Int W2 <=Int W1
[simplification, concrete(W1, S2, W2)]

rule [range-buf-value]:
#range (#buf(W1:Int, X:Int), S2:Int, W2:Int) => #buf(W2, X)
requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int W2)
andBool 0 <=Int S2 andBool 0 <=Int W2 andBool W1 ==Int S2 +Int W2
[simplification, concrete(W1, S2, W2)]

rule [range-padRightToWidth]:
#range(#padRightToWidth(_, BUF), 0, WIDTH) => BUF
requires lengthBytes(BUF) ==Int WIDTH [simplification]

rule [range-eq-check]:
BZ +Bytes #range ( B, S, W ) ==K B => true
requires 0 <=Int S andBool 0 <=Int W
andBool lengthBytes( B ) ==Int S +Int W
andBool #asInteger( BZ ) ==Int 0
andBool lengthBytes( BZ ) ==Int S
andBool #asWord ( B ) <Int 2 ^Int ( 8 *Int W )
[simplification, concrete(BZ, S, W), comm]

rule [range-eq-check-ml]:
{ BZ +Bytes #range ( B, S, W ) #Equals B } => #Top
requires 0 <=Int S andBool 0 <=Int W
andBool lengthBytes( B ) ==Int S +Int W
andBool #asInteger( BZ ) ==Int 0
andBool lengthBytes( BZ ) ==Int S
andBool #asWord ( B ) <Int 2 ^Int ( 8 *Int W )
[simplification, concrete(BZ, S, W), comm]

// Memory update

rule [memUpdate-is-empty]:
Expand Down
23 changes: 23 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,29 @@ module EVM-INT-SIMPLIFICATION-COMMON
requires 0 <Int Y
[simplification, comm, preserves-definedness]

// ###########################################################################
// #asWord
// ###########################################################################

rule [asWord-lt]:
#asWord ( BA ) <Int X => true
requires 2 ^Int ( lengthBytes(BA) *Int 8) <=Int X
[concrete(X), simplification]

rule [asWord-lt-range]:
#asWord ( #range ( _:Bytes, S, W ) ) <Int X => true
requires 0 <=Int S andBool 0 <=Int W
andBool 2 ^Int ( 8 *Int W ) <=Int X
andBool X ==Int 2 ^Int log2Int( X )
[simplification, concrete(S, W, X)]

rule [lt-asWord-range]:
X <Int #asWord ( #range ( B:Bytes, S, W ) ) => X <Int #asWord ( B )
requires 0 <=Int S andBool 0 <=Int W
andBool lengthBytes(B) ==Int S +Int W
andBool #asWord ( B ) <Int 2 ^Int ( 8 *Int W )
[simplification, concrete(X, S, W)]

// ###########################################################################
// chop
// ###########################################################################
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.446
1.0.447
8 changes: 4 additions & 4 deletions tests/specs/benchmarks/verification.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,10 @@ module VERIFICATION-COMMON
rule lengthBytes(#ecrec(HASH, SIGV, SIGR, SIGS)) => 32 requires notBool #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
rule lengthBytes(#ecrec(HASH, SIGV, SIGR, SIGS)) => 0 requires #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]

rule #asWord(#ecrec(HASH, SIGV, SIGR, SIGS)) => 0 requires #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
rule 0 <Int #asWord(#ecrec(HASH, SIGV, SIGR, SIGS)) => true requires notBool #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
rule 0 <=Int #asWord(#ecrec(_ , _ , _ , _ )) => true [simplification]
rule #asWord(#ecrec(_ , _ , _ , _ )) <=Int maxUInt160 => true [simplification]
rule #asWord(#ecrec(HASH, SIGV, SIGR, SIGS)) => 0 requires #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
rule 0 <Int #asWord(#ecrec(HASH, SIGV, SIGR, SIGS)) => true requires notBool #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
rule 0 <=Int #asWord(#ecrec(_ , _ , _ , _ )) => true [simplification]
rule #asWord(#ecrec(_ , _ , _ , _ )) <Int pow160 => true [simplification]

rule #Ceil( #ecrec(HASH, SIGV, SIGR, SIGS) ) => #Top
requires #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
Expand Down
Loading

0 comments on commit 4e6b958

Please sign in to comment.