runtimeverification · dwightguth · Mar 1, 2024 · Mar 19, 2024 · Mar 19, 2024 · Mar 25, 2024
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.520"
+version = "1.0.521"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.520'
+VERSION: Final = '1.0.521'
diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py
@@ -254,7 +254,7 @@ def _kevm_patch_symbol_table(cls, symbol_table: SymbolTable) -> None:
             '_Set_',
             'typedArgs',
             '_up/Int__EVM-TYPES_Int_Int_Int',
-            '_:__EVM-TYPES_WordStack_Int_WordStack',
+            '_WS_',
         ]
         for symb in paren_symbols:
             if symb in symbol_table:
@@ -298,7 +298,7 @@ def _add_account_invariant(account: KApply) -> list[KApply]:
         constraints = []
         word_stack = cterm.cell('WORDSTACK_CELL')
         if type(word_stack) is not KVariable:
-            word_stack_items = flatten_label('_:__EVM-TYPES_WordStack_Int_WordStack', word_stack)
+            word_stack_items = flatten_label('_WS_', word_stack)
             for i in word_stack_items[:-1]:
                 constraints.append(mlEqualsTrue(KEVM.range_uint(256, i)))
 
@@ -520,7 +520,7 @@ def account_cell(
 
     @staticmethod
     def wordstack_len(wordstack: KInner) -> int:
-        return len(flatten_label('_:__EVM-TYPES_WordStack_Int_WordStack', wordstack))
+        return len(flatten_label('_WS_', wordstack))
 
     @staticmethod
     def parse_bytestack(s: KInner) -> KApply:

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
@@ -227,9 +227,11 @@ A cons-list is used for the EVM wordstack.
 -   `_:_` serves as the "cons" operator.
 
 ```k
-    syntax WordStack ::= ".WordStack"      [smtlib(_dotWS)]
-                       | Int ":" WordStack [smtlib(_WS_)]
- // -----------------------------------------------------
+    syntax List ::= ".WordStack"      [symbol(dotWS), macro]
+                  | Int ":" List [macro, symbol(_WS_)]
+ // ---------------------------------------------------------
+    rule .WordStack => .List
+    rule I : L => ListItem(I) L
 ```
 
 ```k
@@ -238,83 +240,15 @@ A cons-list is used for the EVM wordstack.
     rule I : BS => Int2Bytes(1, I, BE) +Bytes BS requires I <Int 256
 ```
 
--   `#take(N , WS)` keeps the first `N` elements of a `WordStack` (passing with zeros as needed).
--   `#drop(N , WS)` removes the first `N` elements of a `WordStack`.
-
-```k
-    syntax WordStack ::= #take ( Int , WordStack ) [klabel(takeWordStack), function, total]
- // ---------------------------------------------------------------------------------------
-    rule [#take.base]:      #take(N, _WS)                => .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
-
-    syntax WordStack ::= #drop ( Int , WordStack ) [klabel(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
-```
-
-### Element Access
-
--   `WS [ N ]` accesses element `N` of `WS`.
--   `WS [ N := W ]` sets element `N` of `WS` to `W` (padding with zeros as needed).
-
-```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  <Int 0
-
-    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  <Int 0
-    rule .WordStack           [ N := W ] => (0 : .WordStack) [ N := W ]
-```
-
 -   `#sizeWordStack` calculates the size of a `WordStack`.
 -   `_in_` determines if a `Int` occurs in a `WordStack`.
 
 ```k
-    syntax Int ::= #sizeWordStack ( WordStack )       [klabel(#sizeWordStack), function, total, smtlib(sizeWordStack)]
-                 | #sizeWordStack ( WordStack , Int ) [klabel(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)
+    syntax Int ::= #sizeWordStack ( List )       [macro]
+ // ----------------------------------------------------
+    rule #sizeWordStack ( WS ) => size ( 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 )            [klabel(#replicate), function, total]
-                       | #replicateAux ( Int, Int, WordStack ) [klabel(#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
-```
-
--   `WordStack2List` converts a term of sort `WordStack` to a term of sort `List`.
-
-```k
-    syntax List ::= WordStack2List ( WordStack ) [klabel(WordStack2List), function, total]
- // --------------------------------------------------------------------------------------
-    rule WordStack2List(.WordStack) => .List
-    rule WordStack2List(W : WS) => ListItem(W) WordStack2List(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/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -64,12 +64,12 @@ In the comments next to each cell, we've marked which component of the YellowPap
               <callValue> 0        </callValue>             // I_v
 
               // \mu_*
-              <wordStack>   .WordStack </wordStack>           // \mu_s
-              <localMem>    .Bytes     </localMem>            // \mu_m
-              <pc>          0          </pc>                  // \mu_pc
-              <gas>         0:Gas      </gas>                 // \mau_g
-              <memoryUsed>  0          </memoryUsed>          // \mu_i
-              <callGas>     0:Gas      </callGas>
+              <wordStack>   .List  </wordStack>           // \mu_s
+              <localMem>    .Bytes </localMem>            // \mu_m
+              <pc>          0      </pc>                  // \mu_pc
+              <gas>         0:Gas  </gas>                 // \mau_g
+              <memoryUsed>  0      </memoryUsed>          // \mu_i
+              <callGas>     0:Gas  </callGas>
 
               <static>    false </static>
               <callDepth> 0     </callDepth>
@@ -351,11 +351,11 @@ The `#next [_]` operator initiates execution by:
 -   `#stackDelta` is the delta the stack will have after the opcode executes.
 
 ```k
-    syntax Bool ::= #stackUnderflow ( WordStack , OpCode ) [klabel(#stackUnderflow), macro]
-                  | #stackOverflow  ( WordStack , OpCode ) [klabel(#stackOverflow), macro]
+    syntax Bool ::= #stackUnderflow ( List , OpCode ) [klabel(#stackUnderflow), macro]
+                  | #stackOverflow  ( List , OpCode ) [klabel(#stackOverflow), macro]
  // ---------------------------------------------------------------------------------------
-    rule #stackUnderflow(WS, OP:OpCode) => #sizeWordStack(WS) <Int #stackNeeded(OP)
-    rule #stackOverflow (WS, OP) => #sizeWordStack(WS) +Int #stackDelta(OP) >Int 1024
+    rule #stackUnderflow(WS, OP:OpCode) => size(WS) <Int #stackNeeded(OP)
+    rule #stackOverflow (WS, OP) => size(WS) +Int #stackDelta(OP) >Int 1024
 
     syntax Int ::= #stackNeeded ( OpCode ) [klabel(#stackNeeded), function]
  // -----------------------------------------------------------------------
@@ -404,12 +404,12 @@ The `#next [_]` operator initiates execution by:
 -   `#changesState` is true if the given opcode will change `<network>` state given the arguments.
 
 ```k
-    syntax Bool ::= #changesState ( OpCode , WordStack ) [klabel(#changesState), function]
- // --------------------------------------------------------------------------------------
+    syntax Bool ::= #changesState ( OpCode , List ) [klabel(#changesState), function]
+ // ---------------------------------------------------------------------------------
 ```
 
 ```k
-    rule #changesState(CALL         , _ : _ : VALUE : _) => true  requires VALUE =/=Int 0
+    rule #changesState(CALL         , ListItem(_) ListItem(_) ListItem(VALUE) _) => true  requires VALUE =/=Int 0
     rule #changesState(LOG(_)       , _)                 => true
     rule #changesState(SSTORE       , _)                 => true
     rule #changesState(CREATE       , _)                 => true
@@ -443,17 +443,17 @@ Here we load the correct number of arguments from the `wordStack` based on the s
                         | TernStackOp Int Int Int
                         | QuadStackOp Int Int Int Int
  // -------------------------------------------------
-    rule <k> #exec [ UOP:UnStackOp   ] => #gas [ UOP , UOP W0          ] ~> UOP W0          ... </k> <wordStack> W0 : WS                => WS </wordStack>
-    rule <k> #exec [ BOP:BinStackOp  ] => #gas [ BOP , BOP W0 W1       ] ~> BOP W0 W1       ... </k> <wordStack> W0 : W1 : WS           => WS </wordStack>
-    rule <k> #exec [ TOP:TernStackOp ] => #gas [ TOP , TOP W0 W1 W2    ] ~> TOP W0 W1 W2    ... </k> <wordStack> W0 : W1 : W2 : WS      => WS </wordStack>
-    rule <k> #exec [ QOP:QuadStackOp ] => #gas [ QOP , QOP W0 W1 W2 W3 ] ~> QOP W0 W1 W2 W3 ... </k> <wordStack> W0 : W1 : W2 : W3 : WS => WS </wordStack>
+    rule <k> #exec [ UOP:UnStackOp   ] => #gas [ UOP , UOP W0          ] ~> UOP W0          ... </k> <wordStack> ListItem(W0) => .List ...</wordStack>
+    rule <k> #exec [ BOP:BinStackOp  ] => #gas [ BOP , BOP W0 W1       ] ~> BOP W0 W1       ... </k> <wordStack> ListItem(W0) ListItem(W1) => .List ...</wordStack>
+    rule <k> #exec [ TOP:TernStackOp ] => #gas [ TOP , TOP W0 W1 W2    ] ~> TOP W0 W1 W2    ... </k> <wordStack> ListItem(W0) ListItem(W1) ListItem(W2) => .List ...</wordStack>
+    rule <k> #exec [ QOP:QuadStackOp ] => #gas [ QOP , QOP W0 W1 W2 W3 ] ~> QOP W0 W1 W2 W3 ... </k> <wordStack> ListItem(W0) ListItem(W1) ListItem(W2) ListItem(W3) => .List ...</wordStack>
 ```
 
 `StackOp` is used for opcodes which require a large portion of the stack.
 
 ```k
-    syntax InternalOp ::= StackOp WordStack
- // ---------------------------------------
+    syntax InternalOp ::= StackOp List
+ // ----------------------------------
     rule <k> #exec [ SO:StackOp ] => #gas [ SO , SO WS ] ~> SO WS ... </k> <wordStack> WS </wordStack>
 ```
 
@@ -463,8 +463,8 @@ The `CallOp` opcodes all interperet their second argument as an address.
     syntax InternalOp ::= CallSixOp Int Int     Int Int Int Int
                         | CallOp    Int Int Int Int Int Int Int
  // -----------------------------------------------------------
-    rule <k> #exec [ CSO:CallSixOp ] => #gas [ CSO , CSO W0 W1    W2 W3 W4 W5 ] ~> CSO W0 W1    W2 W3 W4 W5 ... </k> <wordStack> W0 : W1 : W2 : W3 : W4 : W5 : WS      => WS </wordStack>
-    rule <k> #exec [ CO:CallOp     ] => #gas [ CO  , CO  W0 W1 W2 W3 W4 W5 W6 ] ~> CO  W0 W1 W2 W3 W4 W5 W6 ... </k> <wordStack> W0 : W1 : W2 : W3 : W4 : W5 : W6 : WS => WS </wordStack>
+    rule <k> #exec [ CSO:CallSixOp ] => #gas [ CSO , CSO W0 W1    W2 W3 W4 W5 ] ~> CSO W0 W1    W2 W3 W4 W5 ... </k> <wordStack> ListItem(W0) ListItem(W1) ListItem(W2) ListItem(W3) ListItem(W4) ListItem(W5) => .List ...</wordStack>
+    rule <k> #exec [ CO:CallOp     ] => #gas [ CO  , CO  W0 W1 W2 W3 W4 W5 W6 ] ~> CO  W0 W1 W2 W3 W4 W5 W6 ... </k> <wordStack> ListItem(W0) ListItem(W1) ListItem(W2) ListItem(W3) ListItem(W4) ListItem(W5) ListItem(W6) => .List ...</wordStack>
 ```
 
 ### Address Conversion
@@ -476,12 +476,12 @@ We make sure the given arguments (to be interpreted as addresses) are with 160 b
     syntax InternalOp ::= "#addr" "[" OpCode "]"
  // --------------------------------------------
     rule <k> #addr [ OP:OpCode ] => .K ... </k>
-         <wordStack> (W0 => #addr(W0)) : _WS </wordStack>
-      requires isAddr1Op(OP)
+         <wordStack> WS => WS [ 0 <- #addr({WS [ 0 ]}:>Int) ] </wordStack>
+      requires isAddr1Op(OP) [preserves-definedness]
 
     rule <k> #addr [ OP:OpCode ] => .K ... </k>
-         <wordStack> _W0 : (W1 => #addr(W1)) : _WS </wordStack>
-      requires isAddr2Op(OP)
+         <wordStack> WS => WS [ 1 <- #addr({WS [ 1 ]}:>Int) ] </wordStack>
+      requires isAddr2Op(OP) [preserves-definedness]
 
     rule <k> #addr [ OP:OpCode ] => .K ... </k>
       requires notBool ( isAddr1Op(OP) orBool isAddr2Op(OP) )
@@ -736,9 +736,9 @@ These are just used by the other operators for shuffling local execution state a
 -   `#setStack_` will set the current stack to the given one.
 
 ```k
-    syntax InternalOp ::= "#push" | "#setStack" WordStack
- // -----------------------------------------------------
-    rule <k> W0:Int ~> #push => .K ... </k> <wordStack> WS => W0 : WS </wordStack>
+    syntax InternalOp ::= "#push" | "#setStack" List
+ // ------------------------------------------------
+    rule <k> W0:Int ~> #push => .K ... </k> <wordStack> WS => pushList(W0, WS) </wordStack>
     rule <k> #setStack WS    => .K ... </k> <wordStack> _  => WS      </wordStack>
 ```
 
@@ -860,8 +860,8 @@ Some operators don't calculate anything, they just push the stack around a bit.
     syntax StackOp ::= DUP  ( Int ) [klabel(DUP)]
                      | SWAP ( Int ) [klabel(SWAP)]
  // ----------------------------------------------
-    rule <k> DUP(N)  WS:WordStack => #setStack ((WS [ N -Int 1 ]) : WS)                      ... </k>
-    rule <k> SWAP(N) (W0 : WS)    => #setStack ((WS [ N -Int 1 ]) : (WS [ N -Int 1 := W0 ])) ... </k>
+    rule <k> DUP(N)  WS:List => #setStack (pushList(WS [ N -Int 1 ], WS))                      ... </k>
+    rule <k> SWAP(N) (ListItem(W0) WS)    => #setStack (pushList(WS [ N -Int 1 ], (WS [ N -Int 1 <- W0 ]))) ... </k>
 
     syntax PushOp ::= "PUSHZERO"
                     | PUSH ( Int ) [klabel(PUSH)]
@@ -1131,10 +1131,10 @@ These operators query about the current return data buffer.
  // ------------------------------------------
     rule <k> LOG(N) MEMSTART MEMWIDTH => .K ... </k>
          <id> ACCT </id>
-         <wordStack> WS => #drop(N, WS) </wordStack>
+         <wordStack> WS => range(WS, N, 0) </wordStack>
          <localMem> LM </localMem>
-         <log> L => L ListItem({ ACCT | WordStack2List(#take(N, WS)) | #range(LM, MEMSTART, MEMWIDTH) }) </log>
-      requires #sizeWordStack(WS) >=Int N
+         <log> L => L ListItem({ ACCT | range(WS, 0, size(WS) -Int N) | #range(LM, MEMSTART, MEMWIDTH) }) </log>
+      requires size(WS) >=Int N
 ```
 
 Ethereum Network OpCodes
@@ -1341,12 +1341,12 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
 
     syntax KItem ::= "#initVM"
  // --------------------------
-    rule <k> #initVM      => .K ...      </k>
-         <pc>           _ => 0          </pc>
-         <memoryUsed>   _ => 0          </memoryUsed>
-         <output>       _ => .Bytes     </output>
-         <wordStack>    _ => .WordStack </wordStack>
-         <localMem>     _ => .Bytes     </localMem>
+    rule <k> #initVM      => .K ... </k>
+         <pc>           _ => 0      </pc>
+         <memoryUsed>   _ => 0      </memoryUsed>
+         <output>       _ => .Bytes </output>
+         <wordStack>    _ => .List  </wordStack>
+         <localMem>     _ => .Bytes </localMem>
 
     syntax KItem ::= "#loadProgram" Bytes
  // -------------------------------------

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
@@ -39,7 +39,7 @@ module LEMMAS [symbolic]
   // Word Reasoning
   // ########################
 
-    rule 0 <=Int #sizeWordStack ( _ , N ) => true requires 0 <=Int N [simplification, smt-lemma]
+    rule 0 <=Int size( _:List ) => true [simplification, smt-lemma]
 
     // bool2Word range & simplification
     rule 0 <=Int bool2Word(_B)             => true   [simplification]
Original file line number	Diff line number	Diff line change
Expand Up		@@ -6,4 +6,4 @@
		from typing import Final


		VERSION: Final = '1.0.520'
		VERSION: Final = '1.0.521'