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

Memory update simplifications #2634

Merged
merged 5 commits into from
Oct 8, 2024
Merged

Memory update simplifications #2634

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
62bb884
memory update simplifications from Kontrol
PetarMax Oct 1, 2024
e1aa638
removing unneeded lemma
PetarMax Oct 1, 2024
7ca7945
Revert "removing unneeded lemma"
PetarMax Oct 1, 2024
dd676d3
Merge branch 'master' into petar/memupdate-lemmas
PetarMax Oct 7, 2024
207b42b
Merge branch 'master' into petar/memupdate-lemmas
PetarMax Oct 8, 2024
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
30 changes: 19 additions & 11 deletions 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 @@ -227,27 +227,35 @@ module BYTES-SIMPLIFICATION [symbolic]
requires S <Int 0
[simplification]

rule [memUpdate-as-concat-inside]:
B1:Bytes [ S:Int := B2:Bytes ] =>
#range(B1, 0, S) +Bytes B2 +Bytes #range (B1 , S +Int lengthBytes(B2), lengthBytes(B1) -Int (S +Int lengthBytes(B2)))
requires 0 <=Int S andBool S +Int lengthBytes(B2) <Int lengthBytes(B1)
[simplification(60)]
rule [memUpdate-concat-in-left]: (B1 +Bytes B2) [ S := B ] => (B1 [ S := B ]) +Bytes B2
requires 0 <=Int S andBool S +Int lengthBytes(B) <=Int lengthBytes(B1)
[simplification(40)]

rule [memUpdate-as-concat-outside-1]:
B1:Bytes [ S:Int := B2:Bytes ] => #range(B1, 0, S) +Bytes B2
requires 0 <=Int S andBool lengthBytes(B1) <=Int S +Int lengthBytes(B2)
[simplification(60)]
rule [memUpdate-concat-in-right]: (B1 +Bytes B2) [ S := B ] => B1 +Bytes (B2 [ S -Int lengthBytes(B1) := B ])
requires lengthBytes(B1) <=Int S
[simplification(40)]

rule [memUpdate-reorder]:
B:Bytes [ S1:Int := B1:Bytes] [ S2:Int := B2:Bytes ] => B [ S2 := B2 ] [ S1 := B1 ]
B:Bytes [ S1:Int := B1:Bytes ] [ S2:Int := B2:Bytes ] => B [ S2 := B2 ] [ S1 := B1 ]
requires 0 <=Int S2 andBool S2 <Int S1 andBool S2 +Int lengthBytes(B2) <=Int S1
[simplification]

rule [memUpdate-subsume]:
B:Bytes [ S1:Int := B1:Bytes] [ S2:Int := B2:Bytes ] => B [ S2 := B2 ]
B:Bytes [ S1:Int := B1:Bytes ] [ S2:Int := B2:Bytes ] => B [ S2 := B2 ]
requires 0 <=Int S2 andBool S2 <=Int S1 andBool S1 +Int lengthBytes(B1) <=Int S2 +Int lengthBytes(B2)
[simplification]

rule [memUpdate-as-concat-inside]:
B1:Bytes [ S:Int := B2:Bytes ] =>
#range(B1, 0, S) +Bytes B2 +Bytes #range(B1 , S +Int lengthBytes(B2), lengthBytes(B1) -Int (S +Int lengthBytes(B2)))
requires 0 <=Int S andBool S +Int lengthBytes(B2) <Int lengthBytes(B1)
[simplification(60)]

rule [memUpdate-as-concat-outside]:
B1:Bytes [ S:Int := B2:Bytes ] => #range(B1, 0, S) +Bytes B2
requires 0 <=Int S andBool lengthBytes(B1) <=Int S +Int lengthBytes(B2)
[simplification(60)]
ehildenb marked this conversation as resolved.
Show resolved Hide resolved

// lengthBytes

rule [lengthBytes-geq-zero]: 0 <=Int lengthBytes ( _ ) => true [simplification, smt-lemma]
Expand Down
13 changes: 9 additions & 4 deletions tests/specs/functional/lemmas-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,7 @@ module LEMMAS-SPEC
requires X =/=K Y


// Buffer write simplifications
// Memory update simplifications
// ----------------------------

// claim <k> runLemma ( M [ L := .Bytes ] [ N := WS:Bytes ] ) => doneLemma ( M [ N := WS ] ) ... </k> requires L <=Int N
Expand All @@ -164,9 +164,14 @@ module LEMMAS-SPEC
claim <k> runLemma( M:Bytes [ 32 := BA1 ] [ 32 := BA2 ] ) => doneLemma(M [ 32 := BA2 ] ) ... </k> requires lengthBytes(BA1) <=Int lengthBytes(BA2)
claim <k> runLemma( M:Bytes [ 32 := BA1 ] [ 32 := #padToWidth(32, #asByteStack(#hashedLocation("Solidity", 2, OWNER))) ] ) => doneLemma(M [ 32 := #padToWidth(32, #asByteStack(#hashedLocation("Solidity", 2, OWNER))) ] ) ... </k> requires lengthBytes(BA1) ==Int 32 andBool #rangeUInt(256, OWNER)

// Memory write past the end of the buffer
claim [write-past-end]: <k> runLemma ( #buf(160, A) [ 160 := #buf(32, B) ] [ 192 := #buf(32, C) ] [ 224 := #buf(32, D) ] [ 256 := #buf(32, E) ] )
=> doneLemma ( #buf(160, A) +Bytes #buf(32, B) +Bytes #buf(32, C) +Bytes #buf(32, D) +Bytes #buf(32, E) ) ... </k>
claim [memUpdate-past-end]: <k> runLemma ( #buf(160, A) [ 160 := #buf(32, B) ] [ 192 := #buf(32, C) ] [ 224 := #buf(32, D) ] [ 256 := #buf(32, E) ] )
=> doneLemma ( #buf(160, A) +Bytes #buf(32, B) +Bytes #buf(32, C) +Bytes #buf(32, D) +Bytes #buf(32, E) ) ... </k>

claim [memUpdate-pinpoint]: <k> runLemma ( ( B1 +Bytes B2 +Bytes B3 +Bytes B4 ) [ 70 := #buf(16, X:Int) ] )
=> doneLemma ( ( B1 +Bytes B2 +Bytes ( B3 [ 10 := #buf(16, X:Int) ] ) +Bytes B4 ) ) ... </k>
requires lengthBytes(B1) ==Int 20
andBool lengthBytes(B2) ==Int 40
andBool lengthBytes(B3) ==Int 60

// #lookup simplifications
// -----------------------
Expand Down
Loading