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

Upstream lemmas from Wormhole engagement #1866

Merged
merged 40 commits into from
Oct 3, 2023
Merged

Upstream lemmas from Wormhole engagement #1866

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
40 commits
Select commit Hold shift + click to select a range
aa76e2c
Add notMaxUInt constants
qian-hu May 27, 2023
8327f39
Add bitwise-arithmetic lemmas
qian-hu May 27, 2023
26a1589
Upstream bytes-simplification lemmas from Wormhole
qian-hu May 27, 2023
22f8392
Upstream lemmas from Wormhole engagement
qian-hu May 27, 2023
f45dcab
Set Version: 1.0.187
May 27, 2023
dcca53c
Revert "Upstream lemmas from Wormhole engagement"
qian-hu May 27, 2023
1812eb9
Merge branch 'master' into wormhole-lemmas
qian-hu Jun 14, 2023
a975eb5
Set Version: 1.0.210
Jun 14, 2023
2f1dfaf
Update include/kframework/word.md
qian-hu Jun 14, 2023
214859c
Merge branch 'master' into wormhole-lemmas
qian-hu Jun 19, 2023
eab32d5
Set Version: 1.0.211
Jun 19, 2023
7137fac
Merge remote-tracking branch 'origin/master' into wormhole-lemmas
qian-hu Jun 20, 2023
97e4f9e
Set Version: 1.0.212
Jun 20, 2023
5789fc0
Merge branch 'master' into wormhole-lemmas
qian-hu Jun 21, 2023
3a66b8e
Set Version: 1.0.213
Jun 21, 2023
93abade
Merge branch 'master' into wormhole-lemmas
qian-hu Jun 22, 2023
ad7f4a4
Merge branch 'master' into wormhole-lemmas
qian-hu Jun 26, 2023
c79870e
Set Version: 1.0.219
Jun 26, 2023
17bd534
Merge branch 'master' into wormhole-lemmas
qian-hu Jul 4, 2023
384077f
Set Version: 1.0.227
Jul 4, 2023
e0b8a2d
Merge branch 'master' into wormhole-lemmas
qian-hu Jul 4, 2023
5fd741c
Set Version: 1.0.228
Jul 4, 2023
e8814f3
generalize lemmas
qian-hu Aug 1, 2023
3d48739
Merge branch 'master' into wormhole-lemmas
qian-hu Aug 1, 2023
d590543
Set Version: 1.0.244
Aug 1, 2023
9b7bb4f
Merge branch 'master' into wormhole-lemmas
qian-hu Aug 8, 2023
ec5beed
Set Version: 1.0.249
Aug 8, 2023
533dc1d
Merge branch 'master' into wormhole-lemmas
qian-hu Sep 19, 2023
63c4407
Set Version: 1.0.296
Sep 19, 2023
d9262f5
merge with master
PetarMax Oct 2, 2023
4a80da5
Set Version: 1.0.309
Oct 2, 2023
8cad2bb
cleanup
PetarMax Oct 2, 2023
3365bcd
simplification fix
PetarMax Oct 2, 2023
f575742
Merge branch 'master' into wormhole-lemmas
PetarMax Oct 2, 2023
10f6b18
Set Version: 1.0.310
Oct 2, 2023
4a726fa
removing simplification
PetarMax Oct 2, 2023
5647759
Fix simplification
qian-hu Oct 2, 2023
b3f8251
Add claims for lemmas
qian-hu Oct 2, 2023
8e0ff8c
Update bytes-simplification.k
qian-hu Oct 2, 2023
7d00d95
Add more claims for lemmas
qian-hu Oct 3, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
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.309"
version = "1.0.310"
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.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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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 )
Comment on lines +408 to +436
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These are direct uses of the simplifications - @qian-hu, have we got anything from the engagament that needed them? I have others from the other engagement, but they require further simplifications to pass.

I think we can merge with this for now, and then I will add mine once these further simplifications are upstreamed.


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