Skip to content

Commit

Permalink
Upstream lemmas from Wormhole engagement (#1866)
Browse files Browse the repository at this point in the history 
* Add notMaxUInt constants

* Add bitwise-arithmetic lemmas

* Upstream bytes-simplification lemmas from Wormhole

* Upstream lemmas from Wormhole engagement

* Set Version: 1.0.187

* Revert "Upstream lemmas from Wormhole engagement"

This reverts commit 22f8392.

* Set Version: 1.0.210

* Update include/kframework/word.md

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

* Set Version: 1.0.211

* Set Version: 1.0.212

* Set Version: 1.0.213

* Set Version: 1.0.219

* Set Version: 1.0.227

* Set Version: 1.0.228

* generalize lemmas

* Set Version: 1.0.244

* Set Version: 1.0.249

* Set Version: 1.0.296

* Set Version: 1.0.309

* cleanup

* simplification fix

* Set Version: 1.0.310

* removing simplification

* Fix simplification

* Add claims for lemmas

* Update bytes-simplification.k

* Add more claims for lemmas

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>
  • Loading branch information
@qian-hu @ehildenb @PetarMax
5 people authored Oct 3, 2023
1 parent 7c27cbe commit b1de680
Show file tree
Hide file tree
Showing 7 changed files with 127 additions and 6 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.309"
version = "1.0.310"
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.309'
VERSION: Final = '1.0.310'
47 changes: 45 additions & 2 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 @@ -5,17 +5,24 @@ module BITWISE-SIMPLIFICATION [symbolic]
imports WORD

// ###########################################################################
// inc-or
// bit-or
// ###########################################################################

rule 0 |Int A => A [simplification]
rule A |Int 0 => A [simplification]
rule A |Int A => A [simplification]

rule A |Int B => B |Int A [simplification(40), concrete(B), symbolic(A)]

rule X |Int _ ==Int 0 => false requires 0 <Int X [simplification, concrete(X)]
rule (A |Int B) ==Int (B |Int A) => true [simplification, smt-lemma]

// ###########################################################################
// bit-and
// ###########################################################################

rule A &Int B => B &Int A [symbolic(A), concrete(B), simplification]

rule 0 &Int _ => 0 [simplification]
rule _ &Int 0 => 0 [simplification]
rule A &Int A => A [simplification]
Expand All @@ -40,8 +47,36 @@ 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 maxUInt160 &Int (X |Int (notMaxUInt160 &Int Y:Int)) => X requires #rangeUInt(160, X) andBool 0 <=Int Y [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]

rule [lengthBytes-upInt-32-lower-bound]:
lengthBytes(X) <=Int notMaxUInt5 &Int ( lengthBytes(X) +Int 31 ) => true
Expand All @@ -52,4 +87,12 @@ module BITWISE-SIMPLIFICATION [symbolic]
lengthBytes(X) +Int 32 >Int notMaxUInt5 &Int ( lengthBytes(X) +Int 31 ) => true
[simplification, smt-lemma]

// ###########################################################################
// shift
// ###########################################################################

rule (X <<Int Y) <Int pow256 => true requires 0 <=Int X andBool 0 <=Int Y andBool Y <Int 256 andBool X <Int 2 ^Int (256 -Int Y) [simplification]

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

endmodule
10 changes: 9 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 @@ -69,6 +69,13 @@ module BYTES-SIMPLIFICATION [symbolic]
requires 0 <=Int W1 andBool 0 <=Int W2
[simplification]

rule [buf-shift]:
#buf(W:Int, X <<Int Y) => #buf(W -Int (Y /Int 8), X) +Bytes #buf(Y /Int 8, 0)
requires 0 <=Int W andBool W <=Int 32
andBool 0 <=Int X andBool X <Int 2 ^Int (256 -Int Y)
andBool 0 <=Int Y andBool ( Y <Int W *Int 8 ) andBool Y modInt 8 ==Int 0
[simplification]

// #range

rule [range-empty]:
Expand Down Expand Up @@ -225,7 +232,8 @@ module BYTES-SIMPLIFICATION [symbolic]

rule #asWord(WS) >>Int M => #asWord(#range(WS, 0, lengthBytes(WS) -Int (M /Int 8) )) requires 0 <=Int M andBool M modInt 8 ==Int 0 [simplification]

rule #asWord(#padRightToWidth(32, BUF)) &Int notMaxUInt224 => #asWord(#padRightToWidth(32, BUF))
// This simplification needs to be generalised properly
rule notMaxUInt224 &Int #asWord(#padRightToWidth(32, BUF)) => #asWord(#padRightToWidth(32, BUF))
requires lengthBytes(BUF) <=Int 4 [simplification]

rule #padToWidth(32, #asByteStack(V)) => #buf(32, V) requires #rangeUInt(256, V) [simplification]
Expand Down
12 changes: 12 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -426,20 +426,32 @@ The maximum and minimum values of each type are defined below.
rule maxUFixed128x10 => 3402823669209384634633746074317682114550000000000 /* ( 2^128 - 1) * 10^10 */
syntax Int ::= "notMaxUInt5" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFE0 */
| "notMaxUInt8" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00 */
| "notMaxUInt16" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF0000 */
| "notMaxUInt32" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00000000 */
| "notMaxUInt64" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF0000000000000000 */
| "notMaxUInt96" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF000000000000000000000000 */
| "notMaxUInt128" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00000000000000000000000000000000 */
| "notMaxUInt160" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFF0000000000000000000000000000000000000000 */
| "notMaxUInt192" [alias] /* FFFFFFFFFFFFFFFF000000000000000000000000000000000000000000000000 */
| "notMaxUInt208" [alias] /* FFFFFFFFFFFF0000000000000000000000000000000000000000000000000000 */
| "notMaxUInt224" [alias] /* FFFFFFFF00000000000000000000000000000000000000000000000000000000 */
| "notMaxUInt240" [alias] /* FFFF000000000000000000000000000000000000000000000000000000000000 */
| "notMaxUInt248" [alias] /* FF00000000000000000000000000000000000000000000000000000000000000 */
// -------------------------------------------------------------------------------------------------------------
rule notMaxUInt5 => 115792089237316195423570985008687907853269984665640564039457584007913129639904
rule notMaxUInt8 => 115792089237316195423570985008687907853269984665640564039457584007913129639680
rule notMaxUInt16 => 115792089237316195423570985008687907853269984665640564039457584007913129574400
rule notMaxUInt32 => 115792089237316195423570985008687907853269984665640564039457584007908834672640
rule notMaxUInt64 => 115792089237316195423570985008687907853269984665640564039439137263839420088320
rule notMaxUInt96 => 115792089237316195423570985008687907853269984665561335876943319670319585689600
rule notMaxUInt128 => 115792089237316195423570985008687907852929702298719625575994209400481361428480
rule notMaxUInt160 => 115792089237316195423570985007226406215939081747436879206741300988257197096960
rule notMaxUInt192 => 115792089237316195417293883273301227089434195242432897623355228563449095127040
rule notMaxUInt208 => 115792089237315784047431654707177369110974345328014318355491175612947292487680
rule notMaxUInt224 => 115792089210356248756420345214020892766250353992003419616917011526809519390720
rule notMaxUInt240 => 115790322390251417039241401711187164934754157181743688420499462401711837020160
rule notMaxUInt248 => 115339776388732929035197660848497720713218148788040405586178452820382218977280
syntax Int ::= "eth" [macro]
| "maxBlockNum" [macro] /* 7FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF == (2 ^ 256) - (2 ^ 255) - 1 */
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.309
1.0.310
58 changes: 58 additions & 0 deletions tests/specs/functional/lemmas-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -402,6 +402,64 @@ module LEMMAS-SPEC
claim <k> runLemma ( N &Int maxUInt8 ) => doneLemma ( N ) ... </k> requires #rangeUInt(8, N)
claim <k> runLemma ( maxUInt8 &Int N ) => doneLemma ( N ) ... </k> requires #rangeUInt(8, N)

// 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 Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 8 , X )
claim <k> runLemma ( maxUInt16 &Int ( X |Int ( notMaxUInt16 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 16 , X )
claim <k> runLemma ( maxUInt32 &Int ( X |Int ( notMaxUInt32 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 32 , X )
claim <k> runLemma ( maxUInt64 &Int ( X |Int ( notMaxUInt64 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 64 , X )
claim <k> runLemma ( maxUInt96 &Int ( X |Int ( notMaxUInt96 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 96 , X )
claim <k> runLemma ( maxUInt128 &Int ( X |Int ( notMaxUInt128 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 128 , X )
claim <k> runLemma ( maxUInt160 &Int ( X |Int ( notMaxUInt160 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 160 , X )
claim <k> runLemma ( maxUInt192 &Int ( X |Int ( notMaxUInt192 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 192 , X )
claim <k> runLemma ( maxUInt208 &Int ( X |Int ( notMaxUInt208 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 208 , X )
claim <k> runLemma ( maxUInt224 &Int ( X |Int ( notMaxUInt224 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 224 , X )
claim <k> runLemma ( maxUInt240 &Int ( X |Int ( notMaxUInt240 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 240 , X )
claim <k> runLemma ( maxUInt248 &Int ( X |Int ( notMaxUInt248 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 248 , X )

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 )
claim <k> runLemma ( #buf ( 32 , X <<Int 240 ) ) => doneLemma( #buf ( 2 , X ) +Bytes #buf ( 30 , 0 ) ) ... </k> requires #rangeUInt ( 16 , X )

// shift
// -----

claim [shift-16] : <k> runLemma ( ( X <<Int 16 ) <Int pow256 ) => doneLemma ( true ) ... </k> requires #rangeUInt ( 240 , X )
claim [shift-240]: <k> runLemma ( ( X <<Int 240 ) <Int pow256 ) => doneLemma ( true ) ... </k> requires #rangeUInt ( 16 , X )
claim [shift-248]: <k> runLemma ( ( X <<Int 248 ) <Int pow256 ) => doneLemma ( true ) ... </k> requires #rangeUInt ( 8 , X )

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 )

// concat
// ------

claim <k> runLemma ( lengthBytes ( #range ( #buf ( 32 , _X ) , 3 , 29 ) +Bytes b"\x01" +Bytes #buf ( 2 , Y ) ) )
=> doneLemma ( 32 ) ... </k>
requires #rangeUInt ( 16 , Y )

claim <k> runLemma ( #asWord ( #range ( #buf ( 32 , X ) , 0 , 29 ) +Bytes #range ( #buf ( 32 , X ) , 29 , 3 ) ) )
=> doneLemma ( X ) ... </k>
requires #rangeUInt ( 256 , X )

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

Expand Down

0 comments on commit b1de680

Please sign in to comment.