fix uses of sizeWordStack in specs

runtimeverification · Mar 26, 2024 · bfbe036 · bfbe036
1 parent bae7ee7
commit bfbe036
Show file tree

Hide file tree

Showing 5 changed files with 11 additions and 20 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
@@ -240,6 +240,15 @@ A cons-list is used for the EVM wordstack.
     rule I : BS => Int2Bytes(1, I, BE) +Bytes BS requires I <Int 256
 ```
 
+-   `#sizeWordStack` calculates the size of a `WordStack`.
+-   `_in_` determines if a `Int` occurs in a `WordStack`.
+
+```k
+    syntax Int ::= #sizeWordStack ( List )       [macro]
+ // ----------------------------------------------------
+    rule #sizeWordStack ( WS ) => size ( WS )
+```
+
 -   `WS [ START := WS' ]` assigns a contiguous chunk of `WS'` to `WS` starting at position `START`.
 -   `#write(WM, IDX, VAL)` assigns a value `VAL` at position `IDX` in `WM`.
 -   TODO: remove the first rule for `:=` when [#1844](https://github.com/runtimeverification/evm-semantics/issues/1844) is fixed.

diff --git a/tests/specs/benchmarks/verification.k b/tests/specs/benchmarks/verification.k
@@ -64,17 +64,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/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/verification.k b/tests/specs/mcd/verification.k
@@ -150,8 +150,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
@@ -33,6 +33,5 @@ module VERIFICATION
 
     rule chop(I) => I  requires 0 <=Int I andBool I <Int pow256 [simplification]
 
-    rule 0 <=Int #sizeWordStack ( _  , N ) => true                             requires 0  <=Int N [simplification, smt-lemma]
-    rule         #sizeWordStack ( WS , N ) => N +Int #sizeWordStack ( WS , 0 ) requires N =/=Int 0 [simplification]
+    rule 0 <=Int #sizeWordStack ( _ ) => true                              [simplification, smt-lemma]
 endmodule