From f8461647c00344f651c81a360d3751e6cd947e59 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 26 Sep 2024 13:38:36 +0100 Subject: [PATCH 01/22] initial commit --- .../kevm_pyk/kproj/evm-semantics/evm-types.md | 134 +++++++++++++----- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 1 + .../kproj/evm-semantics/lemmas/lemmas.k | 2 +- optimizer/optimizations.md | 7 +- tests/specs/benchmarks/verification.k | 11 -- tests/specs/examples/sum-to-n-spec.k | 6 +- tests/specs/mcd-structured/verification.k | 2 - tests/specs/mcd/verification.k | 2 - tests/specs/opcodes/verification.k | 6 +- 9 files changed, 106 insertions(+), 65 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index 9c1efd77d1..473acdecc8 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -238,35 +238,99 @@ A cons-list is used for the EVM wordstack. rule I : BS => Int2Bytes(1, I, BE) +Bytes BS requires I .WordStack requires notBool N >Int 0 - rule [#take.zero-pad]: #take(N, .WordStack) => 0 : #take(N -Int 1, .WordStack) requires N >Int 0 - rule [#take.recursive]: #take(N, (W : WS):WordStack) => W : #take(N -Int 1, WS) requires N >Int 0 + // Expected use cases are from 0-4 + rule [ws-take.0]: #take(0, _) => .WordStack + rule [ws-take.1]: #take(1, W0 : _) => W0 : .WordStack + rule [ws-take.2]: #take(2, W0 : W1 : _) => W0 : W1 : .WordStack + rule [ws-take.3]: #take(3, W0 : W1 : W2 : _) => W0 : W1 : W2 : .WordStack + rule [ws-take.4]: #take(4, W0 : W1 : W2 : W3 : _) => W0 : W1 : W2 : W3 : .WordStack + // For unexpected cases + rule [ws-take.N]: #take(N, _ : _ : _ : _ : WS) => #take(N -Int 4, WS) requires 4 .WordStack [owise] syntax WordStack ::= #drop ( Int , WordStack ) [symbol(dropWordStack), function, total] // --------------------------------------------------------------------------------------- - rule #drop(N, WS:WordStack) => WS requires notBool N >Int 0 - rule #drop(N, .WordStack) => .WordStack requires N >Int 0 - rule #drop(N, (W : WS):WordStack) => #drop(1, #drop(N -Int 1, (W : WS))) requires N >Int 1 - rule #drop(1, (_ : WS):WordStack) => WS + // Expected use cases are from 0-4 + rule [ws-drop.0]: #drop(0, WS) => WS + rule [ws-drop.1]: #drop(1, _ : WS) => WS + rule [ws-drop.2]: #drop(2, _ : _ : WS) => WS + rule [ws-drop.3]: #drop(3, _ : _ : _ : WS) => WS + rule [ws-drop.4]: #drop(4, _ : _ : _ : _ : WS) => WS + // For unexpected cases + rule [ws-drop.N]: #drop(N, _ : _ : _ : _ : _ : WS) => #drop(N -Int 4, WS) requires 4 .WordStack [owise] ``` ### Element Access - `WS [ N ]` accesses element `N` of `WS`. -- `WS [ N := W ]` sets element `N` of `WS` to `W` (padding with zeros as needed). +- `WS [ N := W ]` sets element `N` of `WS` to `W`. ```k syntax Int ::= WordStack "[" Int "]" [function, total] // ------------------------------------------------------ - rule (W : _):WordStack [ N ] => W requires N ==Int 0 - rule WS:WordStack [ N ] => #drop(N, WS) [ 0 ] requires N >Int 0 - rule _:WordStack [ N ] => 0 requires N W + rule [ws-get-01]: ( _ : W : _):WordStack [ 1 ] => W + rule [ws-get-02]: ( _ : _ : W : _):WordStack [ 2 ] => W + rule [ws-get-03]: ( _ : _ : _ : W : _):WordStack [ 3 ] => W + rule [ws-get-04]: ( _ : _ : _ : _ : W : _):WordStack [ 4 ] => W + rule [ws-get-05]: ( _ : _ : _ : _ : _ : W : _):WordStack [ 5 ] => W + rule [ws-get-06]: ( _ : _ : _ : _ : _ : _ : W : _):WordStack [ 6 ] => W + rule [ws-get-07]: ( _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 7 ] => W + rule [ws-get-08]: ( _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 8 ] => W + rule [ws-get-09]: ( _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 9 ] => W + rule [ws-get-10]: ( _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 10 ] => W + rule [ws-get-11]: ( _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 11 ] => W + rule [ws-get-12]: ( _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 12 ] => W + rule [ws-get-13]: ( _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 13 ] => W + rule [ws-get-14]: ( _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 14 ] => W + rule [ws-get-15]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 15 ] => W + rule [ws-get-16]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + W : _):WordStack [ 16 ] => W + rule [ws-get-17]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : W : _):WordStack [ 17 ] => W + rule [ws-get-18]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : _ : W : _):WordStack [ 18 ] => W + rule [ws-get-19]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : _ : _ : W : _):WordStack [ 19 ] => W + rule [ws-get-20]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : _ : _ : _ : W : _):WordStack [ 20 ] => W + rule [ws-get-21]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : _ : _ : _ : _ : W : _):WordStack [ 21 ] => W + rule [ws-get-22]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : _ : _ : _ : _ : _ : W : _):WordStack [ 22 ] => W + rule [ws-get-23]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 23 ] => W + rule [ws-get-24]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 24 ] => W + rule [ws-get-25]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 25 ] => W + rule [ws-get-26]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 26 ] => W + rule [ws-get-27]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 27 ] => W + rule [ws-get-28]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 28 ] => W + rule [ws-get-29]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 29 ] => W + rule [ws-get-30]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 30 ] => W + rule [ws-get-31]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 31 ] => W + // For unexpected cases + rule [ws-get-N]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : + _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : WS):WordStack [ N ] => WS [ N -Int 32 ] requires 31 0 [owise] syntax WordStack ::= WordStack "[" Int ":=" Int "]" [function, total] // --------------------------------------------------------------------- @@ -280,29 +344,27 @@ A cons-list is used for the EVM wordstack. - `_in_` determines if a `Int` occurs in a `WordStack`. ```k - syntax Int ::= #sizeWordStack ( WordStack ) [symbol(#sizeWordStack), function, total, smtlib(sizeWordStack)] - | #sizeWordStack ( WordStack , Int ) [symbol(sizeWordStackAux), function, total, smtlib(sizeWordStackAux)] - // ----------------------------------------------------------------------------------------------------------------------- - rule #sizeWordStack ( WS ) => #sizeWordStack(WS, 0) - rule #sizeWordStack ( .WordStack, SIZE ) => SIZE - rule #sizeWordStack ( _ : WS, SIZE ) => #sizeWordStack(WS, SIZE +Int 1) - - syntax Bool ::= Int "in" WordStack [function] - // --------------------------------------------- - rule _ in .WordStack => false - rule W in (W' : WS) => (W ==K W') orElseBool (W in WS) -``` - -- `#replicateAux` pushes `N` copies of `A` onto a `WordStack`. -- `#replicate` is a `WordStack` of length `N` with `A` the value of every element. - -```k - syntax WordStack ::= #replicate ( Int, Int ) [symbol(#replicate), function, total] - | #replicateAux ( Int, Int, WordStack ) [symbol(#replicateAux), function, total] - // --------------------------------------------------------------------------------------------------- - rule #replicate ( N, A ) => #replicateAux(N, A, .WordStack) - rule #replicateAux( N, A, WS ) => #replicateAux(N -Int 1, A, A : WS) requires N >Int 0 - rule #replicateAux( N, _A, WS ) => WS requires notBool N >Int 0 + syntax Int ::= #sizeWordStack ( WordStack ) [symbol(#sizeWordStack), function, total, smtlib(sizeWordStack)] + // ------------------------------------------------------------------------------------------------------------ + rule [ws-size-00]: #sizeWordStack (.WordStack) => 0 + rule [ws-size-01]: #sizeWordStack (_ : .WordStack) => 1 + rule [ws-size-02]: #sizeWordStack (_ : _ : .WordStack) => 2 + rule [ws-size-03]: #sizeWordStack (_ : _ : _ : .WordStack) => 3 + rule [ws-size-04]: #sizeWordStack (_ : _ : _ : _ : .WordStack) => 4 + rule [ws-size-05]: #sizeWordStack (_ : _ : _ : _ : _ : .WordStack) => 5 + rule [ws-size-06]: #sizeWordStack (_ : _ : _ : _ : _ : _ : .WordStack) => 6 + rule [ws-size-07]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : .WordStack) => 7 + rule [ws-size-08]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 8 + rule [ws-size-09]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 9 + rule [ws-size-10]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 10 + rule [ws-size-11]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 11 + rule [ws-size-12]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 12 + rule [ws-size-13]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 13 + rule [ws-size-14]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 14 + rule [ws-size-15]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 15 + rule [ws-size-16]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 16 + + rule #sizeWordStack ( _ : WS ) => 1 +Int #sizeWordStack(WS) ``` - `WordStack2List` converts a term of sort `WordStack` to a term of sort `List`. diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index 99f8b4d449..979b858086 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1171,6 +1171,7 @@ These operators query about the current return data buffer. LM L => L ListItem({ ACCT | WordStack2List(#take(N, WS)) | #range(LM, MEMSTART, MEMWIDTH) }) requires #sizeWordStack(WS) >=Int N + [preserves-definedness] ``` Ethereum Network OpCodes diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 661fa1c143..90ebde1a69 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -46,7 +46,7 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic] // Word Reasoning // ######################## - rule 0 <=Int #sizeWordStack ( _ , N ) => true requires 0 <=Int N [simplification, smt-lemma] + rule 0 <=Int #sizeWordStack ( _ ) => true requires 0 <=Int N [simplification, smt-lemma] // #newAddr range rule 0 <=Int #newAddr(_,_) => true [simplification] diff --git a/optimizer/optimizations.md b/optimizer/optimizations.md index 76e704ed6c..e847fc52aa 100644 --- a/optimizer/optimizations.md +++ b/optimizer/optimizations.md @@ -10,10 +10,9 @@ requires "lemmas/int-simplification.k" module EVM-OPTIMIZATIONS-LEMMAS [symbolic] imports EVM - rule #sizeWordStack(WS , N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0 [simplification] - rule #sizeWordStack(WS [ I := _ ], N) => #sizeWordStack(WS, N) requires I true [simplification] - rule #sizeWordStack(_ , 0) false requires N <=Int 0 [simplification] + rule #sizeWordStack(WS [ I := _ ]) => #sizeWordStack(WS, N) requires I true [simplification] + rule #sizeWordStack(_) false requires N <=Int 0 [simplification] endmodule diff --git a/tests/specs/benchmarks/verification.k b/tests/specs/benchmarks/verification.k index dff254eb89..a572add2c3 100644 --- a/tests/specs/benchmarks/verification.k +++ b/tests/specs/benchmarks/verification.k @@ -62,17 +62,6 @@ module VERIFICATION rule 0 <=Int #memoryUsageUpdate(_MU, _START, _WIDTH) => true [simplification] - // ######################## - // Buffer Reasoning - // ######################## - - rule #sizeWordStack(WS, N) #sizeWordStack(WS, 0) +Int N SIZELIMIT SIZELIMIT #sizeWordStack(WS, 0) +Int N <=Int SIZE requires N =/=Int 0 [simplification] - // ######################## // Range // ######################## diff --git a/tests/specs/examples/sum-to-n-spec.k b/tests/specs/examples/sum-to-n-spec.k index 2ebeeaca83..14b2c449fc 100644 --- a/tests/specs/examples/sum-to-n-spec.k +++ b/tests/specs/examples/sum-to-n-spec.k @@ -5,15 +5,11 @@ module VERIFICATION imports EVM-ASSEMBLY imports LEMMAS - rule #sizeWordStack ( WS , N:Int ) - => N +Int #sizeWordStack ( WS , 0 ) - requires N =/=K 0 [simplification] - rule bool2Word(A) ==K 0 => notBool(A) [simplification] rule chop(I) => I requires #rangeUInt(256, I) [simplification] - rule 0 <=Int #sizeWordStack ( _ , _ ) => true [simplification, smt-lemma] + rule 0 <=Int #sizeWordStack ( _ ) => true [simplification, smt-lemma] syntax Bytes ::= "sumToN" [macro] // ------------------------------------- diff --git a/tests/specs/mcd-structured/verification.k b/tests/specs/mcd-structured/verification.k index 8078d1654c..40b38e4cfc 100644 --- a/tests/specs/mcd-structured/verification.k +++ b/tests/specs/mcd-structured/verification.k @@ -142,8 +142,6 @@ module LEMMAS-MCD [symbolic] // Word Reasoning // ######################## - rule #sizeWordStack(WS, N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0 [simplification] - // ### vat-addui-fail-rough // // Proof: diff --git a/tests/specs/mcd/verification.k b/tests/specs/mcd/verification.k index cf400bac8b..37f0a7e191 100644 --- a/tests/specs/mcd/verification.k +++ b/tests/specs/mcd/verification.k @@ -147,8 +147,6 @@ module LEMMAS-MCD [symbolic] // Word Reasoning // ######################## - rule #sizeWordStack(WS, N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0 [simplification] - // ### vat-addui-fail-rough // // Proof: diff --git a/tests/specs/opcodes/verification.k b/tests/specs/opcodes/verification.k index 16fc7281d3..01f62f62c3 100644 --- a/tests/specs/opcodes/verification.k +++ b/tests/specs/opcodes/verification.k @@ -5,8 +5,6 @@ module VERIFICATION imports EVM imports INT-SIMPLIFICATION - rule #sizeWordStack(WS , N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0 [simplification] - rule #sizeWordStack(WS [ I := _ ], N) => #sizeWordStack(WS, N) requires I true [simplification] - rule #sizeWordStack(_ , 0) false requires N <=Int 0 [simplification] + rule #sizeWordStack(WS [ I := _ ]) => #sizeWordStack(WS) requires I true [simplification] endmodule From 3c3fa5022aef9135236d77325c47bace6975bb9c Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 26 Sep 2024 15:14:08 +0100 Subject: [PATCH 02/22] corrections --- .../kevm_pyk/kproj/evm-semantics/evm-types.md | 64 +++++++++++++++++-- .../kproj/evm-semantics/lemmas/lemmas.k | 2 +- 2 files changed, 59 insertions(+), 7 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index 473acdecc8..5b7486f63b 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -328,16 +328,68 @@ A cons-list is used for the EVM wordstack. _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 31 ] => W // For unexpected cases rule [ws-get-N]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : WS):WordStack [ N ] => WS [ N -Int 32 ] requires 31 WS:WordStack [ N -Int 32 ] requires 31 0 [owise] + rule [ws-get-O]: _:WordStack [ _:Int ] => 0 [owise] syntax WordStack ::= WordStack "[" Int ":=" Int "]" [function, total] // --------------------------------------------------------------------- - rule (_W0 : WS):WordStack [ N := W ] => W : WS requires N ==Int 0 - rule ( W0 : WS):WordStack [ N := W ] => W0 : (WS [ N -Int 1 := W ]) requires N >Int 0 - rule WS :WordStack [ N := _ ] => WS requires N (0 : .WordStack) [ N := W ] + // Expected use cases are from 0-31 + rule [ws-set-00]: ( _ : WS):WordStack [ 0 := V ] => ( V : WS ):WordStack + rule [ws-set-01]: ( W0 : _ : WS):WordStack [ 1 := V ] => ( W0 : V : WS):WordStack + rule [ws-set-02]: ( W0 : W1 : _ : WS):WordStack [ 2 := V ] => ( W0 : W1 : V : WS):WordStack + rule [ws-set-03]: ( W0 : W1 : W2 : _ : WS):WordStack [ 3 := V ] => ( W0 : W1 : W2 : V : WS):WordStack + rule [ws-set-04]: ( W0 : W1 : W2 : W3 : _ : WS):WordStack [ 4 := V ] => ( W0 : W1 : W2 : W3 : V : WS):WordStack + rule [ws-set-05]: ( W0 : W1 : W2 : W3 : W4 : _ : WS):WordStack [ 5 := V ] => ( W0 : W1 : W2 : W3 : W4 : V : WS):WordStack + rule [ws-set-06]: ( W0 : W1 : W2 : W3 : W4 : W5 : _ : WS):WordStack [ 6 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : V : WS):WordStack + rule [ws-set-07]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : _ : WS):WordStack [ 7 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : V : WS):WordStack + rule [ws-set-08]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : _ : WS):WordStack [ 8 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : V : WS):WordStack + rule [ws-set-09]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : _ : WS):WordStack [ 9 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : V : WS):WordStack + rule [ws-set-10]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : _ : WS):WordStack [ 10 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : V : WS):WordStack + rule [ws-set-11]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : _ : WS):WordStack [ 11 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : V : WS):WordStack + rule [ws-set-12]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : _ : WS):WordStack [ 12 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : V : WS):WordStack + rule [ws-set-13]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : _ : WS):WordStack [ 13 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : V : WS):WordStack + rule [ws-set-14]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : _ : WS):WordStack [ 14 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : V : WS):WordStack + rule [ws-set-15]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : _ : WS):WordStack [ 15 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : V : WS):WordStack + rule [ws-set-16]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : V : WS):WordStack + rule [ws-set-17]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + W16 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : V : WS):WordStack + rule [ws-set-18]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + W16 : W17 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : V : WS):WordStack + rule [ws-set-19]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + W16 : W17 : W18 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : V : WS):WordStack + rule [ws-set-20]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + W16 : W17 : W18 : W19 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : V : WS):WordStack + rule [ws-set-21]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + W16 : W17 : W18 : W19 : W20 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : V : WS):WordStack + rule [ws-set-22]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + W16 : W17 : W18 : W19 : W20 : W21 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : V : WS):WordStack + rule [ws-set-23]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + W16 : W17 : W18 : W19 : W20 : W21 : W22 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : V : WS):WordStack + rule [ws-set-24]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : V : WS):WordStack + rule [ws-set-25]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : V : WS):WordStack + rule [ws-set-26]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : V : WS):WordStack + rule [ws-set-27]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : V : WS):WordStack + rule [ws-set-28]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : V : WS):WordStack + rule [ws-set-29]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : V : WS):WordStack + rule [ws-set-30]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : V : WS):WordStack + rule [ws-set-31]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : V : WS):WordStack + // For unexpected cases + rule [ws-set-N]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : V15 : + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : V31 : WS):WordStack [ N := V ] => + ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : V15 : + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : V31 : (WS [ N -Int 32 := V ] )):WordStack requires 31 .WordStack [owise] ``` - `#sizeWordStack` calculates the size of a `WordStack`. diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 90ebde1a69..609aebdbae 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -46,7 +46,7 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic] // Word Reasoning // ######################## - rule 0 <=Int #sizeWordStack ( _ ) => true requires 0 <=Int N [simplification, smt-lemma] + rule 0 <=Int #sizeWordStack ( _ ) => true [simplification, smt-lemma] // #newAddr range rule 0 <=Int #newAddr(_,_) => true [simplification] From ceacb63084c251e72c30450239e7d2aa27b954c2 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 26 Sep 2024 16:06:35 +0100 Subject: [PATCH 03/22] adding SMT lemmas --- optimizer/optimizations.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/optimizer/optimizations.md b/optimizer/optimizations.md index e847fc52aa..fd6f1418e1 100644 --- a/optimizer/optimizations.md +++ b/optimizer/optimizations.md @@ -11,8 +11,8 @@ module EVM-OPTIMIZATIONS-LEMMAS [symbolic] imports EVM rule #sizeWordStack(WS [ I := _ ]) => #sizeWordStack(WS, N) requires I true [simplification] - rule #sizeWordStack(_) false requires N <=Int 0 [simplification] + rule 0 <=Int #sizeWordStack(_) => true [simplification, smt-lemma] + rule #sizeWordStack(_) false requires N <=Int 0 [simplification, smt-lemma] endmodule From a3a1a5651d87b61f7eb82786e8ea6017f093e67f Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 26 Sep 2024 16:29:51 +0100 Subject: [PATCH 04/22] more smt lemmas --- tests/specs/examples/sum-to-n-spec.k | 2 -- tests/specs/opcodes/verification.k | 4 +++- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/specs/examples/sum-to-n-spec.k b/tests/specs/examples/sum-to-n-spec.k index 14b2c449fc..dc323c51a5 100644 --- a/tests/specs/examples/sum-to-n-spec.k +++ b/tests/specs/examples/sum-to-n-spec.k @@ -9,8 +9,6 @@ module VERIFICATION rule chop(I) => I requires #rangeUInt(256, I) [simplification] - rule 0 <=Int #sizeWordStack ( _ ) => true [simplification, smt-lemma] - syntax Bytes ::= "sumToN" [macro] // ------------------------------------- rule sumToN diff --git a/tests/specs/opcodes/verification.k b/tests/specs/opcodes/verification.k index 01f62f62c3..35a6be0e81 100644 --- a/tests/specs/opcodes/verification.k +++ b/tests/specs/opcodes/verification.k @@ -6,5 +6,7 @@ module VERIFICATION imports INT-SIMPLIFICATION rule #sizeWordStack(WS [ I := _ ]) => #sizeWordStack(WS) requires I true [simplification] + rule 0 <=Int #sizeWordStack(_) => true [simplification, smt-lemma] + rule #sizeWordStack(_) false requires N <=Int 0 [simplification, smt-lemma] + endmodule From 5e89634ed29c07dcdd92ffe3bf3f44f11658ec25 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 26 Sep 2024 16:54:02 +0100 Subject: [PATCH 05/22] correction --- .../kevm_pyk/kproj/evm-semantics/evm-types.md | 32 ++++++++--------- optimizer/optimizations.md | 36 +++++++++++++++++-- 2 files changed, 50 insertions(+), 18 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index 5b7486f63b..1de7914c7d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -354,35 +354,35 @@ A cons-list is used for the EVM wordstack. rule [ws-set-16]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : V : WS):WordStack rule [ws-set-17]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : V : WS):WordStack + W16 : _ : WS):WordStack [ 17 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : V : WS):WordStack rule [ws-set-18]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : V : WS):WordStack + W16 : W17 : _ : WS):WordStack [ 18 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : V : WS):WordStack rule [ws-set-19]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : V : WS):WordStack + W16 : W17 : W18 : _ : WS):WordStack [ 19 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : V : WS):WordStack rule [ws-set-20]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : V : WS):WordStack + W16 : W17 : W18 : W19 : _ : WS):WordStack [ 20 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : V : WS):WordStack rule [ws-set-21]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : V : WS):WordStack + W16 : W17 : W18 : W19 : W20 : _ : WS):WordStack [ 21 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : V : WS):WordStack rule [ws-set-22]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : V : WS):WordStack + W16 : W17 : W18 : W19 : W20 : W21 : _ : WS):WordStack [ 22 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : V : WS):WordStack rule [ws-set-23]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : V : WS):WordStack + W16 : W17 : W18 : W19 : W20 : W21 : W22 : _ : WS):WordStack [ 23 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : V : WS):WordStack rule [ws-set-24]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : V : WS):WordStack + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : _ : WS):WordStack [ 24 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : V : WS):WordStack rule [ws-set-25]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : V : WS):WordStack + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : _ : WS):WordStack [ 25 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : V : WS):WordStack rule [ws-set-26]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : V : WS):WordStack + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : _ : WS):WordStack [ 26 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : V : WS):WordStack rule [ws-set-27]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : V : WS):WordStack + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : _ : WS):WordStack [ 27 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : V : WS):WordStack rule [ws-set-28]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : V : WS):WordStack + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : _ : WS):WordStack [ 28 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : V : WS):WordStack rule [ws-set-29]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : V : WS):WordStack + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : _ : WS):WordStack [ 29 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : V : WS):WordStack rule [ws-set-30]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : V : WS):WordStack + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : _ : WS):WordStack [ 30 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : V : WS):WordStack rule [ws-set-31]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : V : WS):WordStack + W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : _ : WS):WordStack [ 31 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : V : WS):WordStack // For unexpected cases rule [ws-set-N]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : V15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : V31 : WS):WordStack [ N := V ] => @@ -416,7 +416,7 @@ A cons-list is used for the EVM wordstack. rule [ws-size-15]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 15 rule [ws-size-16]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 16 - rule #sizeWordStack ( _ : WS ) => 1 +Int #sizeWordStack(WS) + rule #sizeWordStack ( _ : WS ) => 1 +Int #sizeWordStack(WS) [owise] ``` - `WordStack2List` converts a term of sort `WordStack` to a term of sort `List`. diff --git a/optimizer/optimizations.md b/optimizer/optimizations.md index fd6f1418e1..2397e463fc 100644 --- a/optimizer/optimizations.md +++ b/optimizer/optimizations.md @@ -22,8 +22,40 @@ module EVM-OPTIMIZATIONS imports INT-SIMPLIFICATION -// {OPTIMIZATIONS} - + claim + [optimized.add]: + + + ( #next[ ADD ] => .K ) ... + + + SCHED + + + USEGAS + + + + + + ( W0 : W1 : WS => chop( ( W0 +Int W1 ) ) : WS ) + + + ( PCOUNT => ( PCOUNT +Int 1 ) ) + + + ( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi ) + + ... + + ... + + ... + + ... + + requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi ) + andBool ( #sizeWordStack( WS ) <=Int 1023 ) endmodule ``` From 1269317aab2690c34e6b7cb20a30af20638480ba Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 26 Sep 2024 17:26:39 +0100 Subject: [PATCH 06/22] correction --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md | 2 +- kevm-pyk/src/tests/integration/test_prove.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index 1de7914c7d..5a8cf9c3ef 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -416,7 +416,7 @@ A cons-list is used for the EVM wordstack. rule [ws-size-15]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 15 rule [ws-size-16]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 16 - rule #sizeWordStack ( _ : WS ) => 1 +Int #sizeWordStack(WS) [owise] + rule #sizeWordStack ( _ : WS ) => 1 +Int #sizeWordStack(WS) ``` - `WordStack2List` converts a term of sort `WordStack` to a term of sort `List`. diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index c49202a2d5..b0343d098a 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -425,7 +425,7 @@ def _get_optimization_proofs() -> list[APRProof]: kore_rpc_command = ('booster-dev',) if use_booster_dev else ('kore-rpc-booster',) with legacy_explore( - kevm, kcfg_semantics=KEVMSemantics(allow_symbolic_program=True), kore_rpc_command=kore_rpc_command + kevm, kcfg_semantics=KEVMSemantics(allow_symbolic_program=True), kore_rpc_command=kore_rpc_command, smt_timeout=1000 ) as kcfg_explore: prover = APRProver( kcfg_explore, From 7205c9bf97e664e18395d35ee597e1be13418ea3 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 26 Sep 2024 17:36:09 +0100 Subject: [PATCH 07/22] formatting correction --- kevm-pyk/src/tests/integration/test_prove.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index b0343d098a..621836dd11 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -425,7 +425,10 @@ def _get_optimization_proofs() -> list[APRProof]: kore_rpc_command = ('booster-dev',) if use_booster_dev else ('kore-rpc-booster',) with legacy_explore( - kevm, kcfg_semantics=KEVMSemantics(allow_symbolic_program=True), kore_rpc_command=kore_rpc_command, smt_timeout=1000 + kevm, + kcfg_semantics=KEVMSemantics(allow_symbolic_program=True), + kore_rpc_command=kore_rpc_command, + smt_timeout=1000, ) as kcfg_explore: prover = APRProver( kcfg_explore, From 5e1f9466a292187ebb4ea7f1be45e0029715f689 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 26 Sep 2024 23:05:32 +0100 Subject: [PATCH 08/22] further lemmas --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 609aebdbae..9cb1706607 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -46,7 +46,8 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic] // Word Reasoning // ######################## - rule 0 <=Int #sizeWordStack ( _ ) => true [simplification, smt-lemma] + rule 0 <=Int #sizeWordStack(_) => true [simplification, smt-lemma] + rule #sizeWordStack(_) false requires N <=Int 0 [simplification, smt-lemma] // #newAddr range rule 0 <=Int #newAddr(_,_) => true [simplification] From e2fb9092acead716088a8ce65adb2cb5e1bf76e4 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 27 Sep 2024 00:39:37 +0100 Subject: [PATCH 09/22] third lemma --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 9cb1706607..363a74a8aa 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -46,8 +46,9 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic] // Word Reasoning // ######################## - rule 0 <=Int #sizeWordStack(_) => true [simplification, smt-lemma] - rule #sizeWordStack(_) false requires N <=Int 0 [simplification, smt-lemma] + rule #sizeWordStack(WS [ I := _ ]) => #sizeWordStack(WS) requires I true [simplification, smt-lemma] + rule #sizeWordStack(_) false requires N <=Int 0 [simplification, smt-lemma] // #newAddr range rule 0 <=Int #newAddr(_,_) => true [simplification] From b4dc91f35d52e03057a94cd3ad6ea7c3a526fb02 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 27 Sep 2024 07:31:55 +0100 Subject: [PATCH 10/22] corrections --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md | 4 ++-- optimizer/optimizations.md | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index 5a8cf9c3ef..b5b75f92a8 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -251,7 +251,7 @@ A cons-list is used for the EVM wordstack. rule [ws-take.3]: #take(3, W0 : W1 : W2 : _) => W0 : W1 : W2 : .WordStack rule [ws-take.4]: #take(4, W0 : W1 : W2 : W3 : _) => W0 : W1 : W2 : W3 : .WordStack // For unexpected cases - rule [ws-take.N]: #take(N, _ : _ : _ : _ : WS) => #take(N -Int 4, WS) requires 4 W0 : W1 : W2 : W3 : #take(N -Int 4, WS) requires 4 .WordStack [owise] @@ -264,7 +264,7 @@ A cons-list is used for the EVM wordstack. rule [ws-drop.3]: #drop(3, _ : _ : _ : WS) => WS rule [ws-drop.4]: #drop(4, _ : _ : _ : _ : WS) => WS // For unexpected cases - rule [ws-drop.N]: #drop(N, _ : _ : _ : _ : _ : WS) => #drop(N -Int 4, WS) requires 4 #drop(N -Int 4, WS) requires 4 .WordStack [owise] ``` diff --git a/optimizer/optimizations.md b/optimizer/optimizations.md index 2397e463fc..c97a72208d 100644 --- a/optimizer/optimizations.md +++ b/optimizer/optimizations.md @@ -10,9 +10,9 @@ requires "lemmas/int-simplification.k" module EVM-OPTIMIZATIONS-LEMMAS [symbolic] imports EVM - rule #sizeWordStack(WS [ I := _ ]) => #sizeWordStack(WS, N) requires I true [simplification, smt-lemma] - rule #sizeWordStack(_) false requires N <=Int 0 [simplification, smt-lemma] + rule #sizeWordStack(WS [ I := _ ]) => #sizeWordStack(WS) requires I true [simplification, smt-lemma] + rule #sizeWordStack(_) false requires N <=Int 0 [simplification, smt-lemma] endmodule From b554704e76a939f9f4ac9674aef4033ea5e676ae Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 27 Sep 2024 07:43:48 +0100 Subject: [PATCH 11/22] sizeWordStack --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index b5b75f92a8..f1c53a4d37 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -415,8 +415,8 @@ A cons-list is used for the EVM wordstack. rule [ws-size-14]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 14 rule [ws-size-15]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 15 rule [ws-size-16]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 16 - - rule #sizeWordStack ( _ : WS ) => 1 +Int #sizeWordStack(WS) + rule [ws-size-N]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : WS) => 16 +Int #sizeWordStack(WS) + rule [ws-size-O]: #sizeWordStack ( _ : WS ) => 1 +Int #sizeWordStack(WS) ``` - `WordStack2List` converts a term of sort `WordStack` to a term of sort `List`. From 05cab845371ed3924dd7cbce924ea4b4ab0e74e1 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 27 Sep 2024 09:51:31 +0100 Subject: [PATCH 12/22] no owise --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index f1c53a4d37..da4e25f5a7 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -253,7 +253,7 @@ A cons-list is used for the EVM wordstack. // For unexpected cases rule [ws-take.N]: #take(N, W0 : W1 : W2 : W3 : WS) => W0 : W1 : W2 : W3 : #take(N -Int 4, WS) requires 4 .WordStack [owise] + rule [ws-take.O]: #take(_, _) => .WordStack syntax WordStack ::= #drop ( Int , WordStack ) [symbol(dropWordStack), function, total] // --------------------------------------------------------------------------------------- @@ -266,7 +266,7 @@ A cons-list is used for the EVM wordstack. // For unexpected cases rule [ws-drop.N]: #drop(N, _ : _ : _ : _ : WS) => #drop(N -Int 4, WS) requires 4 .WordStack [owise] + rule [ws-drop.O]: #drop(_, _) => .WordStack ``` ### Element Access @@ -330,7 +330,7 @@ A cons-list is used for the EVM wordstack. rule [ws-get-N]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : WS):WordStack [ N ] => WS:WordStack [ N -Int 32 ] requires 31 0 [owise] + rule [ws-get-O]: _:WordStack [ _:Int ] => 0 syntax WordStack ::= WordStack "[" Int ":=" Int "]" [function, total] // --------------------------------------------------------------------- @@ -389,7 +389,7 @@ A cons-list is used for the EVM wordstack. ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : V15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : V31 : (WS [ N -Int 32 := V ] )):WordStack requires 31 .WordStack [owise] + rule [ws-set-O]: _:WordStack [ _ := _ ] => .WordStack ``` - `#sizeWordStack` calculates the size of a `WordStack`. From bccdb04b06b1b7e7b8ddeb69cb586764f479b964 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 27 Sep 2024 10:05:15 +0100 Subject: [PATCH 13/22] rule enumeration --- .../kevm_pyk/kproj/evm-semantics/evm-types.md | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index da4e25f5a7..cc125abd66 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -245,28 +245,28 @@ A cons-list is used for the EVM wordstack. syntax WordStack ::= #take ( Int , WordStack ) [symbol(takeWordStack), function, total] // --------------------------------------------------------------------------------------- // Expected use cases are from 0-4 - rule [ws-take.0]: #take(0, _) => .WordStack - rule [ws-take.1]: #take(1, W0 : _) => W0 : .WordStack - rule [ws-take.2]: #take(2, W0 : W1 : _) => W0 : W1 : .WordStack - rule [ws-take.3]: #take(3, W0 : W1 : W2 : _) => W0 : W1 : W2 : .WordStack - rule [ws-take.4]: #take(4, W0 : W1 : W2 : W3 : _) => W0 : W1 : W2 : W3 : .WordStack + rule [ws-take-0]: #take(0, _) => .WordStack + rule [ws-take-1]: #take(1, W0 : _) => W0 : .WordStack + rule [ws-take-2]: #take(2, W0 : W1 : _) => W0 : W1 : .WordStack + rule [ws-take-3]: #take(3, W0 : W1 : W2 : _) => W0 : W1 : W2 : .WordStack + rule [ws-take-4]: #take(4, W0 : W1 : W2 : W3 : _) => W0 : W1 : W2 : W3 : .WordStack // For unexpected cases - rule [ws-take.N]: #take(N, W0 : W1 : W2 : W3 : WS) => W0 : W1 : W2 : W3 : #take(N -Int 4, WS) requires 4 W0 : W1 : W2 : W3 : #take(N -Int 4, WS) requires 4 .WordStack + rule [ws-take-O]: #take(_, _) => .WordStack [owise] syntax WordStack ::= #drop ( Int , WordStack ) [symbol(dropWordStack), function, total] // --------------------------------------------------------------------------------------- // Expected use cases are from 0-4 - rule [ws-drop.0]: #drop(0, WS) => WS - rule [ws-drop.1]: #drop(1, _ : WS) => WS - rule [ws-drop.2]: #drop(2, _ : _ : WS) => WS - rule [ws-drop.3]: #drop(3, _ : _ : _ : WS) => WS - rule [ws-drop.4]: #drop(4, _ : _ : _ : _ : WS) => WS + rule [ws-drop-0]: #drop(0, WS) => WS + rule [ws-drop-1]: #drop(1, _ : WS) => WS + rule [ws-drop-2]: #drop(2, _ : _ : WS) => WS + rule [ws-drop-3]: #drop(3, _ : _ : _ : WS) => WS + rule [ws-drop-4]: #drop(4, _ : _ : _ : _ : WS) => WS // For unexpected cases - rule [ws-drop.N]: #drop(N, _ : _ : _ : _ : WS) => #drop(N -Int 4, WS) requires 4 #drop(N -Int 4, WS) requires 4 .WordStack + rule [ws-drop-O]: #drop(_, _) => .WordStack [owise] ``` ### Element Access @@ -330,7 +330,7 @@ A cons-list is used for the EVM wordstack. rule [ws-get-N]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : WS):WordStack [ N ] => WS:WordStack [ N -Int 32 ] requires 31 0 + rule [ws-get-O]: _:WordStack [ _:Int ] => 0 [owise] syntax WordStack ::= WordStack "[" Int ":=" Int "]" [function, total] // --------------------------------------------------------------------- @@ -389,7 +389,7 @@ A cons-list is used for the EVM wordstack. ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : V15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : V31 : (WS [ N -Int 32 := V ] )):WordStack requires 31 .WordStack + rule [ws-set-O]: _:WordStack [ _ := _ ] => .WordStack [owise] ``` - `#sizeWordStack` calculates the size of a `WordStack`. From aaec015ca0f0a687de0eb2885600b7943674ffa1 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 27 Sep 2024 11:49:56 +0100 Subject: [PATCH 14/22] minor corrections --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index cc125abd66..935a12223d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -253,7 +253,7 @@ A cons-list is used for the EVM wordstack. // For unexpected cases rule [ws-take-N]: #take(N, W0 : W1 : W2 : W3 : WS) => W0 : W1 : W2 : W3 : #take(N -Int 4, WS) requires 4 .WordStack [owise] + rule [ws-take-O]: #take(_, _) => .WordStack [priority(75)] syntax WordStack ::= #drop ( Int , WordStack ) [symbol(dropWordStack), function, total] // --------------------------------------------------------------------------------------- @@ -266,7 +266,7 @@ A cons-list is used for the EVM wordstack. // For unexpected cases rule [ws-drop-N]: #drop(N, _ : _ : _ : _ : WS) => #drop(N -Int 4, WS) requires 4 .WordStack [owise] + rule [ws-drop-O]: #drop(_, _) => .WordStack [priority(75)] ``` ### Element Access @@ -330,7 +330,7 @@ A cons-list is used for the EVM wordstack. rule [ws-get-N]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : WS):WordStack [ N ] => WS:WordStack [ N -Int 32 ] requires 31 0 [owise] + rule [ws-get-O]: _:WordStack [ _:Int ] => 0 [priority(75)] syntax WordStack ::= WordStack "[" Int ":=" Int "]" [function, total] // --------------------------------------------------------------------- @@ -389,7 +389,7 @@ A cons-list is used for the EVM wordstack. ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : V15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : V31 : (WS [ N -Int 32 := V ] )):WordStack requires 31 .WordStack [owise] + rule [ws-set-O]: _:WordStack [ _ := _ ] => .WordStack [priority(75)] ``` - `#sizeWordStack` calculates the size of a `WordStack`. @@ -416,7 +416,7 @@ A cons-list is used for the EVM wordstack. rule [ws-size-15]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 15 rule [ws-size-16]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 16 rule [ws-size-N]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : WS) => 16 +Int #sizeWordStack(WS) - rule [ws-size-O]: #sizeWordStack ( _ : WS ) => 1 +Int #sizeWordStack(WS) + rule [ws-size-O]: #sizeWordStack (_ : WS) => 1 +Int #sizeWordStack(WS) [priority(75)] ``` - `WordStack2List` converts a term of sort `WordStack` to a term of sort `List`. From ff6adbee272cb519e98a4d5d95420ddb929ca327 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 27 Sep 2024 12:37:20 +0100 Subject: [PATCH 15/22] documentation correction --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md | 1 - 1 file changed, 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index 935a12223d..b00e81ff11 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -393,7 +393,6 @@ A cons-list is used for the EVM wordstack. ``` - `#sizeWordStack` calculates the size of a `WordStack`. -- `_in_` determines if a `Int` occurs in a `WordStack`. ```k syntax Int ::= #sizeWordStack ( WordStack ) [symbol(#sizeWordStack), function, total, smtlib(sizeWordStack)] From c0c088b7a1a5e3f75467c494de679cb86903f9a1 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 27 Sep 2024 12:41:35 +0100 Subject: [PATCH 16/22] adding tests to booster-dev ignore until booster improves indeterminate rule matching --- tests/failing-symbolic.haskell-booster-dev | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/tests/failing-symbolic.haskell-booster-dev b/tests/failing-symbolic.haskell-booster-dev index a3ab6a12db..70cd716094 100644 --- a/tests/failing-symbolic.haskell-booster-dev +++ b/tests/failing-symbolic.haskell-booster-dev @@ -135,4 +135,8 @@ tests/specs/mcd-structured/flopper-tick-pass-rough-spec.k tests/specs/mcd-structured/functional-spec.k tests/specs/mcd-structured/pot-join-pass-rough-spec.k tests/specs/mcd-structured/vow-fess-fail-rough-spec.k -tests/specs/mcd-structured/vow-flog-fail-rough-spec.k \ No newline at end of file +tests/specs/mcd-structured/vow-flog-fail-rough-spec.k +tests/specs/mcd/dai-adduu-fail-rough-spec.k +tests/specs/mcd/dai-adduu-fail-rough-spec.k +tests/specs/mcd-structured/dai-adduu-fail-rough-spec.k +tests/specs/mcd-structured/flipper-addu48u48-fail-rough-spec.k \ No newline at end of file From 5acb050d1911fd90d3e08b06696af3cdc47843f5 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 27 Sep 2024 13:01:28 +0100 Subject: [PATCH 17/22] correction --- tests/failing-symbolic.haskell-booster-dev | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/failing-symbolic.haskell-booster-dev b/tests/failing-symbolic.haskell-booster-dev index 70cd716094..dc5acb192a 100644 --- a/tests/failing-symbolic.haskell-booster-dev +++ b/tests/failing-symbolic.haskell-booster-dev @@ -137,6 +137,6 @@ tests/specs/mcd-structured/pot-join-pass-rough-spec.k tests/specs/mcd-structured/vow-fess-fail-rough-spec.k tests/specs/mcd-structured/vow-flog-fail-rough-spec.k tests/specs/mcd/dai-adduu-fail-rough-spec.k -tests/specs/mcd/dai-adduu-fail-rough-spec.k +tests/specs/mcd/flipper-addu48u48-fail-rough-spec.k tests/specs/mcd-structured/dai-adduu-fail-rough-spec.k tests/specs/mcd-structured/flipper-addu48u48-fail-rough-spec.k \ No newline at end of file From 7899ab3862caba4edeb70242b1fc07e0d217a18c Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 27 Sep 2024 15:09:23 +0100 Subject: [PATCH 18/22] corrections --- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 1 - optimizer/optimizations.md | 36 ++----------------- 2 files changed, 2 insertions(+), 35 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index 979b858086..99f8b4d449 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1171,7 +1171,6 @@ These operators query about the current return data buffer. LM L => L ListItem({ ACCT | WordStack2List(#take(N, WS)) | #range(LM, MEMSTART, MEMWIDTH) }) requires #sizeWordStack(WS) >=Int N - [preserves-definedness] ``` Ethereum Network OpCodes diff --git a/optimizer/optimizations.md b/optimizer/optimizations.md index c97a72208d..ef0c60bbea 100644 --- a/optimizer/optimizations.md +++ b/optimizer/optimizations.md @@ -22,40 +22,8 @@ module EVM-OPTIMIZATIONS imports INT-SIMPLIFICATION - claim - [optimized.add]: - - - ( #next[ ADD ] => .K ) ... - - - SCHED - - - USEGAS - - - - - - ( W0 : W1 : WS => chop( ( W0 +Int W1 ) ) : WS ) - - - ( PCOUNT => ( PCOUNT +Int 1 ) ) - - - ( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi ) - - ... - - ... - - ... - - ... - - requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi ) - andBool ( #sizeWordStack( WS ) <=Int 1023 ) +// {OPTIMIZATIONS} + endmodule ``` From 3d7c9c2b9419a663af0f7e3e8dfd4da50ee16892 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 27 Sep 2024 15:32:32 +0100 Subject: [PATCH 19/22] tail-recursive sizeWordStack --- .../kevm_pyk/kproj/evm-semantics/evm-types.md | 21 ++----------------- 1 file changed, 2 insertions(+), 19 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index b00e81ff11..e46164a776 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -397,25 +397,8 @@ A cons-list is used for the EVM wordstack. ```k syntax Int ::= #sizeWordStack ( WordStack ) [symbol(#sizeWordStack), function, total, smtlib(sizeWordStack)] // ------------------------------------------------------------------------------------------------------------ - rule [ws-size-00]: #sizeWordStack (.WordStack) => 0 - rule [ws-size-01]: #sizeWordStack (_ : .WordStack) => 1 - rule [ws-size-02]: #sizeWordStack (_ : _ : .WordStack) => 2 - rule [ws-size-03]: #sizeWordStack (_ : _ : _ : .WordStack) => 3 - rule [ws-size-04]: #sizeWordStack (_ : _ : _ : _ : .WordStack) => 4 - rule [ws-size-05]: #sizeWordStack (_ : _ : _ : _ : _ : .WordStack) => 5 - rule [ws-size-06]: #sizeWordStack (_ : _ : _ : _ : _ : _ : .WordStack) => 6 - rule [ws-size-07]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : .WordStack) => 7 - rule [ws-size-08]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 8 - rule [ws-size-09]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 9 - rule [ws-size-10]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 10 - rule [ws-size-11]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 11 - rule [ws-size-12]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 12 - rule [ws-size-13]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 13 - rule [ws-size-14]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 14 - rule [ws-size-15]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 15 - rule [ws-size-16]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 16 - rule [ws-size-N]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : WS) => 16 +Int #sizeWordStack(WS) - rule [ws-size-O]: #sizeWordStack (_ : WS) => 1 +Int #sizeWordStack(WS) [priority(75)] + rule [ws-size-base]: #sizeWordStack (.WordStack) => 0 + rule [ws-size-ind]: #sizeWordStack (_ : WS) => 1 +Int #sizeWordStack(WS) ``` - `WordStack2List` converts a term of sort `WordStack` to a term of sort `List`. From 3801e920c1a92353a81a18dd7193348fd3d9e6ab Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 27 Sep 2024 17:29:48 +0100 Subject: [PATCH 20/22] reverting the computation of sizeWordStack --- .../src/kevm_pyk/kproj/evm-semantics/evm-types.md | 11 +++++++---- .../src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 4 +--- optimizer/optimizations.md | 7 ++++--- tests/specs/benchmarks/verification.k | 11 +++++++++++ tests/specs/examples/sum-to-n-spec.k | 6 ++++++ tests/specs/mcd-structured/verification.k | 2 ++ tests/specs/mcd/verification.k | 2 ++ tests/specs/opcodes/verification.k | 7 ++++--- 8 files changed, 37 insertions(+), 13 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index e46164a776..74ef8aae1b 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -395,10 +395,13 @@ A cons-list is used for the EVM wordstack. - `#sizeWordStack` calculates the size of a `WordStack`. ```k - syntax Int ::= #sizeWordStack ( WordStack ) [symbol(#sizeWordStack), function, total, smtlib(sizeWordStack)] - // ------------------------------------------------------------------------------------------------------------ - rule [ws-size-base]: #sizeWordStack (.WordStack) => 0 - rule [ws-size-ind]: #sizeWordStack (_ : WS) => 1 +Int #sizeWordStack(WS) + syntax Int ::= #sizeWordStack ( WordStack ) [symbol(#sizeWordStack), function, total, smtlib(sizeWordStack)] + | #sizeWordStack ( WordStack , Int ) [symbol(sizeWordStackAux), function, total, smtlib(sizeWordStackAux)] + // ----------------------------------------------------------------------------------------------------------------------- + rule #sizeWordStack ( WS ) => #sizeWordStack(WS, 0) + + rule #sizeWordStack ( .WordStack, SIZE ) => SIZE + rule #sizeWordStack ( _ : WS, SIZE ) => #sizeWordStack(WS, SIZE +Int 1) ``` - `WordStack2List` converts a term of sort `WordStack` to a term of sort `List`. diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 363a74a8aa..661fa1c143 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -46,9 +46,7 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic] // Word Reasoning // ######################## - rule #sizeWordStack(WS [ I := _ ]) => #sizeWordStack(WS) requires I true [simplification, smt-lemma] - rule #sizeWordStack(_) false requires N <=Int 0 [simplification, smt-lemma] + rule 0 <=Int #sizeWordStack ( _ , N ) => true requires 0 <=Int N [simplification, smt-lemma] // #newAddr range rule 0 <=Int #newAddr(_,_) => true [simplification] diff --git a/optimizer/optimizations.md b/optimizer/optimizations.md index ef0c60bbea..76e704ed6c 100644 --- a/optimizer/optimizations.md +++ b/optimizer/optimizations.md @@ -10,9 +10,10 @@ requires "lemmas/int-simplification.k" module EVM-OPTIMIZATIONS-LEMMAS [symbolic] imports EVM - rule #sizeWordStack(WS [ I := _ ]) => #sizeWordStack(WS) requires I true [simplification, smt-lemma] - rule #sizeWordStack(_) false requires N <=Int 0 [simplification, smt-lemma] + rule #sizeWordStack(WS , N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0 [simplification] + rule #sizeWordStack(WS [ I := _ ], N) => #sizeWordStack(WS, N) requires I true [simplification] + rule #sizeWordStack(_ , 0) false requires N <=Int 0 [simplification] endmodule diff --git a/tests/specs/benchmarks/verification.k b/tests/specs/benchmarks/verification.k index a572add2c3..dff254eb89 100644 --- a/tests/specs/benchmarks/verification.k +++ b/tests/specs/benchmarks/verification.k @@ -62,6 +62,17 @@ module VERIFICATION rule 0 <=Int #memoryUsageUpdate(_MU, _START, _WIDTH) => true [simplification] + // ######################## + // Buffer Reasoning + // ######################## + + rule #sizeWordStack(WS, N) #sizeWordStack(WS, 0) +Int N SIZELIMIT SIZELIMIT #sizeWordStack(WS, 0) +Int N <=Int SIZE requires N =/=Int 0 [simplification] + // ######################## // Range // ######################## diff --git a/tests/specs/examples/sum-to-n-spec.k b/tests/specs/examples/sum-to-n-spec.k index dc323c51a5..2ebeeaca83 100644 --- a/tests/specs/examples/sum-to-n-spec.k +++ b/tests/specs/examples/sum-to-n-spec.k @@ -5,10 +5,16 @@ module VERIFICATION imports EVM-ASSEMBLY imports LEMMAS + rule #sizeWordStack ( WS , N:Int ) + => N +Int #sizeWordStack ( WS , 0 ) + requires N =/=K 0 [simplification] + rule bool2Word(A) ==K 0 => notBool(A) [simplification] rule chop(I) => I requires #rangeUInt(256, I) [simplification] + rule 0 <=Int #sizeWordStack ( _ , _ ) => true [simplification, smt-lemma] + syntax Bytes ::= "sumToN" [macro] // ------------------------------------- rule sumToN diff --git a/tests/specs/mcd-structured/verification.k b/tests/specs/mcd-structured/verification.k index 40b38e4cfc..8078d1654c 100644 --- a/tests/specs/mcd-structured/verification.k +++ b/tests/specs/mcd-structured/verification.k @@ -142,6 +142,8 @@ module LEMMAS-MCD [symbolic] // Word Reasoning // ######################## + rule #sizeWordStack(WS, N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0 [simplification] + // ### vat-addui-fail-rough // // Proof: diff --git a/tests/specs/mcd/verification.k b/tests/specs/mcd/verification.k index 37f0a7e191..cf400bac8b 100644 --- a/tests/specs/mcd/verification.k +++ b/tests/specs/mcd/verification.k @@ -147,6 +147,8 @@ module LEMMAS-MCD [symbolic] // Word Reasoning // ######################## + rule #sizeWordStack(WS, N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0 [simplification] + // ### vat-addui-fail-rough // // Proof: diff --git a/tests/specs/opcodes/verification.k b/tests/specs/opcodes/verification.k index 35a6be0e81..ec02a7c13a 100644 --- a/tests/specs/opcodes/verification.k +++ b/tests/specs/opcodes/verification.k @@ -5,8 +5,9 @@ module VERIFICATION imports EVM imports INT-SIMPLIFICATION - rule #sizeWordStack(WS [ I := _ ]) => #sizeWordStack(WS) requires I true [simplification, smt-lemma] - rule #sizeWordStack(_) false requires N <=Int 0 [simplification, smt-lemma] + rule #sizeWordStack(WS , N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0 [simplification] + rule #sizeWordStack(WS [ I := _ ], N) => #sizeWordStack(WS, N) requires I true [simplification] + rule #sizeWordStack(_ , 0) false requires N <=Int 0 [simplification] endmodule From f0bfa6ef9203f463bbea3cf7c9396fdc30f28097 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Sun, 29 Sep 2024 10:08:56 +0100 Subject: [PATCH 21/22] removing direct computations --- .../kevm_pyk/kproj/evm-semantics/evm-types.md | 142 ++---------------- 1 file changed, 16 insertions(+), 126 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index 74ef8aae1b..51461ed3d9 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -244,29 +244,19 @@ A cons-list is used for the EVM wordstack. ```k syntax WordStack ::= #take ( Int , WordStack ) [symbol(takeWordStack), function, total] // --------------------------------------------------------------------------------------- - // Expected use cases are from 0-4 - rule [ws-take-0]: #take(0, _) => .WordStack - rule [ws-take-1]: #take(1, W0 : _) => W0 : .WordStack - rule [ws-take-2]: #take(2, W0 : W1 : _) => W0 : W1 : .WordStack - rule [ws-take-3]: #take(3, W0 : W1 : W2 : _) => W0 : W1 : W2 : .WordStack - rule [ws-take-4]: #take(4, W0 : W1 : W2 : W3 : _) => W0 : W1 : W2 : W3 : .WordStack - // For unexpected cases - rule [ws-take-N]: #take(N, W0 : W1 : W2 : W3 : WS) => W0 : W1 : W2 : W3 : #take(N -Int 4, WS) requires 4 .WordStack + rule [ws-take-i]: #take(N, W0 : WS) => W0 : #take(N -Int 1, WS) requires 0 .WordStack [priority(75)] + rule [ws-take-o]: #take(_, _) => .WordStack [owise] syntax WordStack ::= #drop ( Int , WordStack ) [symbol(dropWordStack), function, total] // --------------------------------------------------------------------------------------- - // Expected use cases are from 0-4 - rule [ws-drop-0]: #drop(0, WS) => WS - rule [ws-drop-1]: #drop(1, _ : WS) => WS - rule [ws-drop-2]: #drop(2, _ : _ : WS) => WS - rule [ws-drop-3]: #drop(3, _ : _ : _ : WS) => WS - rule [ws-drop-4]: #drop(4, _ : _ : _ : _ : WS) => WS - // For unexpected cases - rule [ws-drop-N]: #drop(N, _ : _ : _ : _ : WS) => #drop(N -Int 4, WS) requires 4 WS + rule [ws-drop-i]: #drop(N, W0 : WS) => #drop(N -Int 1, WS) requires 0 .WordStack [priority(75)] + rule [ws-drop-O]: #drop(_, _) => .WordStack [owise] ``` ### Element Access @@ -277,119 +267,19 @@ A cons-list is used for the EVM wordstack. ```k syntax Int ::= WordStack "[" Int "]" [function, total] // ------------------------------------------------------ - // Expected use cases are from 0-31 - rule [ws-get-00]: ( W : _):WordStack [ 0 ] => W - rule [ws-get-01]: ( _ : W : _):WordStack [ 1 ] => W - rule [ws-get-02]: ( _ : _ : W : _):WordStack [ 2 ] => W - rule [ws-get-03]: ( _ : _ : _ : W : _):WordStack [ 3 ] => W - rule [ws-get-04]: ( _ : _ : _ : _ : W : _):WordStack [ 4 ] => W - rule [ws-get-05]: ( _ : _ : _ : _ : _ : W : _):WordStack [ 5 ] => W - rule [ws-get-06]: ( _ : _ : _ : _ : _ : _ : W : _):WordStack [ 6 ] => W - rule [ws-get-07]: ( _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 7 ] => W - rule [ws-get-08]: ( _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 8 ] => W - rule [ws-get-09]: ( _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 9 ] => W - rule [ws-get-10]: ( _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 10 ] => W - rule [ws-get-11]: ( _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 11 ] => W - rule [ws-get-12]: ( _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 12 ] => W - rule [ws-get-13]: ( _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 13 ] => W - rule [ws-get-14]: ( _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 14 ] => W - rule [ws-get-15]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 15 ] => W - rule [ws-get-16]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - W : _):WordStack [ 16 ] => W - rule [ws-get-17]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : W : _):WordStack [ 17 ] => W - rule [ws-get-18]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : W : _):WordStack [ 18 ] => W - rule [ws-get-19]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : _ : W : _):WordStack [ 19 ] => W - rule [ws-get-20]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : _ : _ : W : _):WordStack [ 20 ] => W - rule [ws-get-21]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : _ : _ : _ : W : _):WordStack [ 21 ] => W - rule [ws-get-22]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : _ : _ : _ : _ : W : _):WordStack [ 22 ] => W - rule [ws-get-23]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 23 ] => W - rule [ws-get-24]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 24 ] => W - rule [ws-get-25]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 25 ] => W - rule [ws-get-26]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 26 ] => W - rule [ws-get-27]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 27 ] => W - rule [ws-get-28]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 28 ] => W - rule [ws-get-29]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 29 ] => W - rule [ws-get-30]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 30 ] => W - rule [ws-get-31]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : W : _):WordStack [ 31 ] => W - // For unexpected cases - rule [ws-get-N]: (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : - _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : WS):WordStack [ N ] => WS:WordStack [ N -Int 32 ] requires 31 W + rule [ws-get-i]: (W : WS):WordStack [ N ] => WS:WordStack [ N -Int 1 ] requires 0 0 [priority(75)] + rule [ws-get-o]: _:WordStack [ _:Int ] => 0 [owise] syntax WordStack ::= WordStack "[" Int ":=" Int "]" [function, total] // --------------------------------------------------------------------- - // Expected use cases are from 0-31 - rule [ws-set-00]: ( _ : WS):WordStack [ 0 := V ] => ( V : WS ):WordStack - rule [ws-set-01]: ( W0 : _ : WS):WordStack [ 1 := V ] => ( W0 : V : WS):WordStack - rule [ws-set-02]: ( W0 : W1 : _ : WS):WordStack [ 2 := V ] => ( W0 : W1 : V : WS):WordStack - rule [ws-set-03]: ( W0 : W1 : W2 : _ : WS):WordStack [ 3 := V ] => ( W0 : W1 : W2 : V : WS):WordStack - rule [ws-set-04]: ( W0 : W1 : W2 : W3 : _ : WS):WordStack [ 4 := V ] => ( W0 : W1 : W2 : W3 : V : WS):WordStack - rule [ws-set-05]: ( W0 : W1 : W2 : W3 : W4 : _ : WS):WordStack [ 5 := V ] => ( W0 : W1 : W2 : W3 : W4 : V : WS):WordStack - rule [ws-set-06]: ( W0 : W1 : W2 : W3 : W4 : W5 : _ : WS):WordStack [ 6 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : V : WS):WordStack - rule [ws-set-07]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : _ : WS):WordStack [ 7 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : V : WS):WordStack - rule [ws-set-08]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : _ : WS):WordStack [ 8 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : V : WS):WordStack - rule [ws-set-09]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : _ : WS):WordStack [ 9 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : V : WS):WordStack - rule [ws-set-10]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : _ : WS):WordStack [ 10 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : V : WS):WordStack - rule [ws-set-11]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : _ : WS):WordStack [ 11 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : V : WS):WordStack - rule [ws-set-12]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : _ : WS):WordStack [ 12 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : V : WS):WordStack - rule [ws-set-13]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : _ : WS):WordStack [ 13 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : V : WS):WordStack - rule [ws-set-14]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : _ : WS):WordStack [ 14 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : V : WS):WordStack - rule [ws-set-15]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : _ : WS):WordStack [ 15 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : V : WS):WordStack - rule [ws-set-16]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - _ : WS):WordStack [ 16 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : V : WS):WordStack - rule [ws-set-17]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : _ : WS):WordStack [ 17 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : V : WS):WordStack - rule [ws-set-18]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : _ : WS):WordStack [ 18 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : V : WS):WordStack - rule [ws-set-19]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : _ : WS):WordStack [ 19 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : V : WS):WordStack - rule [ws-set-20]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : _ : WS):WordStack [ 20 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : V : WS):WordStack - rule [ws-set-21]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : _ : WS):WordStack [ 21 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : V : WS):WordStack - rule [ws-set-22]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : _ : WS):WordStack [ 22 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : V : WS):WordStack - rule [ws-set-23]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : _ : WS):WordStack [ 23 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : V : WS):WordStack - rule [ws-set-24]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : _ : WS):WordStack [ 24 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : V : WS):WordStack - rule [ws-set-25]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : _ : WS):WordStack [ 25 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : V : WS):WordStack - rule [ws-set-26]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : _ : WS):WordStack [ 26 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : V : WS):WordStack - rule [ws-set-27]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : _ : WS):WordStack [ 27 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : V : WS):WordStack - rule [ws-set-28]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : _ : WS):WordStack [ 28 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : V : WS):WordStack - rule [ws-set-29]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : _ : WS):WordStack [ 29 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : V : WS):WordStack - rule [ws-set-30]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : _ : WS):WordStack [ 30 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : V : WS):WordStack - rule [ws-set-31]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : _ : WS):WordStack [ 31 := V ] => ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : W15 : W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : V : WS):WordStack - // For unexpected cases - rule [ws-set-N]: ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : V15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : V31 : WS):WordStack [ N := V ] => - ( W0 : W1 : W2 : W3 : W4 : W5 : W6 : W7 : W8 : W9 : W10 : W11 : W12 : W13 : W14 : V15 : - W16 : W17 : W18 : W19 : W20 : W21 : W22 : W23 : W24 : W25 : W26 : W27 : W28 : W29 : W30 : V31 : (WS [ N -Int 32 := V ] )):WordStack requires 31 ( V : WS ):WordStack + rule [ws-set-i]: (W : WS):WordStack [ N := V ] => ( W : (WS [ N -Int 1 := V ]) ):WordStack requires 0 .WordStack [priority(75)] + rule [ws-set-O]: _:WordStack [ _ := _ ] => .WordStack [owise] ``` - `#sizeWordStack` calculates the size of a `WordStack`. From 550111f231cab9fbbf98d7a1dababeea965c1550 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Sun, 29 Sep 2024 18:42:40 +0100 Subject: [PATCH 22/22] bringing back booster tests --- tests/failing-symbolic.haskell-booster-dev | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/tests/failing-symbolic.haskell-booster-dev b/tests/failing-symbolic.haskell-booster-dev index dc5acb192a..a3ab6a12db 100644 --- a/tests/failing-symbolic.haskell-booster-dev +++ b/tests/failing-symbolic.haskell-booster-dev @@ -135,8 +135,4 @@ tests/specs/mcd-structured/flopper-tick-pass-rough-spec.k tests/specs/mcd-structured/functional-spec.k tests/specs/mcd-structured/pot-join-pass-rough-spec.k tests/specs/mcd-structured/vow-fess-fail-rough-spec.k -tests/specs/mcd-structured/vow-flog-fail-rough-spec.k -tests/specs/mcd/dai-adduu-fail-rough-spec.k -tests/specs/mcd/flipper-addu48u48-fail-rough-spec.k -tests/specs/mcd-structured/dai-adduu-fail-rough-spec.k -tests/specs/mcd-structured/flipper-addu48u48-fail-rough-spec.k \ No newline at end of file +tests/specs/mcd-structured/vow-flog-fail-rough-spec.k \ No newline at end of file