reverting the computation of sizeWordStack

runtimeverification · Sep 27, 2024 · 3801e92 · 3801e92
1 parent 3d7c9c2
commit 3801e92
Show file tree

Hide file tree

Showing 8 changed files with 37 additions and 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
@@ -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
@@ -46,9 +46,7 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
   // Word Reasoning
   // ########################
 
-    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]
+    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
@@ -10,9 +10,10 @@ requires "lemmas/int-simplification.k"
 module EVM-OPTIMIZATIONS-LEMMAS [symbolic]
     imports EVM
 
-    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]
+    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]
 
 endmodule
 

diff --git 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) <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/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
@@ -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
@@ -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
@@ -5,8 +5,9 @@ module VERIFICATION
     imports EVM
     imports INT-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]
+    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]
 
 endmodule