redesigning #sizeWordStack

runtimeverification · Sep 26, 2024 · 8e98c87 · 8e98c87
1 parent 1bd8e09
commit 8e98c87
Show file tree

Hide file tree

Showing 7 changed files with 15 additions and 48 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
@@ -277,32 +277,15 @@ 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)]
-                 | #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-08]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : WS) => 8 +Int #sizeWordStack(WS)
+    rule [ws-size-04]: #sizeWordStack (_ : _ : _ : _ : WS) => 4 +Int #sizeWordStack(WS)
+    rule [ws-size-02]: #sizeWordStack (_ : _ : WS) => 2 +Int #sizeWordStack(WS)
+    rule [ws-size-01]: #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/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 [simplification]
 
     // #newAddr range
     rule 0 <=Int #newAddr(_,_)             => true   [simplification]

diff --git 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 <Int #sizeWordStack(WS) [simplification]
-    rule 0 <=Int #sizeWordStack(_ , 0)    => true                                                            [simplification]
-    rule #sizeWordStack(_ , 0) <Int N     => false                        requires N <=Int 0                 [simplification]
+    rule #sizeWordStack(WS [ I := _ ]) => #sizeWordStack(WS) requires I <Int #sizeWordStack(WS) [simplification]
+    rule 0 <=Int #sizeWordStack(_)     => true                                                  [simplification, smt-lemma]
+    rule #sizeWordStack(_) <Int N      => false              requires N <=Int 0                 [simplification, smt-lemma]
 
 endmodule
 

diff --git 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) <Int SIZE => #sizeWordStack(WS, 0) +Int N <Int SIZE  requires N =/=Int 0 [simplification]
-
-    rule SIZELIMIT <Int #sizeWordStack(WS, N) +Int DELTA  => SIZELIMIT <Int (#sizeWordStack(WS, 0) +Int N) +Int DELTA  requires N =/=Int 0 [simplification]
-    rule SIZELIMIT <Int #sizeWordStack(WS, N)             => SIZELIMIT <Int  #sizeWordStack(WS, 0) +Int N              requires N =/=Int 0 [simplification]
-
-    rule #sizeWordStack(WS, N) <=Int SIZE => #sizeWordStack(WS, 0) +Int N <=Int SIZE  requires N =/=Int 0 [simplification]
-
   // ########################
   // Range
   // ########################

diff --git 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
@@ -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
@@ -5,8 +5,8 @@ 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 <Int #sizeWordStack(WS) [simplification]
-    rule 0 <=Int #sizeWordStack(_ , 0)    => true                                                            [simplification]
-    rule #sizeWordStack(_ , 0) <Int N     => false                        requires N <=Int 0                 [simplification]
+    rule #sizeWordStack(WS [ I := _ ]) => #sizeWordStack(WS) requires I <Int #sizeWordStack(WS) [simplification]
+    rule 0 <=Int #sizeWordStack(_)     => true                                                  [simplification, smt-lemma]
+    rule #sizeWordStack(_) <Int N      => false              requires N <=Int 0                 [simplification, smt-lemma]
+
 endmodule