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 a25c2b6bd7..935cfd6ff4 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -63,12 +63,12 @@ In the comments next to each cell, we've marked which component of the YellowPap
0 // I_v
// \mu_*
- .WordStack // \mu_s
- .Bytes // \mu_m
- 0 // \mu_pc
- 0:Gas // \mau_g
- 0 // \mu_i
- 0:Gas
+ .List // \mu_s
+ .Bytes // \mu_m
+ 0 // \mu_pc
+ 0:Gas // \mau_g
+ 0 // \mu_i
+ 0:Gas
false
0
@@ -355,11 +355,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 ) [symbol(#stackUnderflow), macro]
- | #stackOverflow ( WordStack , OpCode ) [symbol(#stackOverflow), macro]
- // ---------------------------------------------------------------------------------------
- rule #stackUnderflow(WS, OP:OpCode) => #sizeWordStack(WS) #sizeWordStack(WS) +Int #stackDelta(OP) >Int 1024
+ syntax Bool ::= #stackUnderflow ( List , OpCode ) [symbol(#stackUnderflow), macro]
+ | #stackOverflow ( List , OpCode ) [symbol(#stackOverflow), macro]
+ // ----------------------------------------------------------------------------------
+ rule #stackUnderflow(WS, OP:OpCode) => size(WS) size(WS) +Int #stackDelta(OP) >Int 1024
syntax Int ::= #stackNeeded ( OpCode ) [symbol(#stackNeeded), function]
// -----------------------------------------------------------------------
@@ -408,12 +408,12 @@ The `#next [_]` operator initiates execution by:
- `#changesState` is true if the given opcode will change `` state given the arguments.
```k
- syntax Bool ::= #changesState ( OpCode , WordStack ) [symbol(#changesState), function]
- // --------------------------------------------------------------------------------------
+ syntax Bool ::= #changesState ( OpCode , List ) [symbol(#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
@@ -448,17 +448,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 #exec [ UOP:UnStackOp ] => #gas [ UOP , UOP W0 ] ~> UOP W0 ... W0 : WS => WS
- rule #exec [ BOP:BinStackOp ] => #gas [ BOP , BOP W0 W1 ] ~> BOP W0 W1 ... W0 : W1 : WS => WS
- rule #exec [ TOP:TernStackOp ] => #gas [ TOP , TOP W0 W1 W2 ] ~> TOP W0 W1 W2 ... W0 : W1 : W2 : WS => WS
- rule #exec [ QOP:QuadStackOp ] => #gas [ QOP , QOP W0 W1 W2 W3 ] ~> QOP W0 W1 W2 W3 ... W0 : W1 : W2 : W3 : WS => WS
+ rule #exec [ UOP:UnStackOp ] => #gas [ UOP , UOP W0 ] ~> UOP W0 ... ListItem(W0) => .List ...
+ rule #exec [ BOP:BinStackOp ] => #gas [ BOP , BOP W0 W1 ] ~> BOP W0 W1 ... ListItem(W0) ListItem(W1) => .List ...
+ rule #exec [ TOP:TernStackOp ] => #gas [ TOP , TOP W0 W1 W2 ] ~> TOP W0 W1 W2 ... ListItem(W0) ListItem(W1) ListItem(W2) => .List ...
+ rule #exec [ QOP:QuadStackOp ] => #gas [ QOP , QOP W0 W1 W2 W3 ] ~> QOP W0 W1 W2 W3 ... ListItem(W0) ListItem(W1) ListItem(W2) ListItem(W3) => .List ...
```
`StackOp` is used for opcodes which require a large portion of the stack.
```k
- syntax InternalOp ::= StackOp WordStack
- // ---------------------------------------
+ syntax InternalOp ::= StackOp List
+ // ----------------------------------
rule #exec [ SO:StackOp ] => #gas [ SO , SO WS ] ~> SO WS ... WS
```
@@ -468,8 +468,8 @@ The `CallOp` opcodes all interpret their second argument as an address.
syntax InternalOp ::= CallSixOp Int Int Int Int Int Int
| CallOp Int Int Int Int Int Int Int
// -----------------------------------------------------------
- rule #exec [ CSO:CallSixOp ] => #gas [ CSO , CSO W0 W1 W2 W3 W4 W5 ] ~> CSO W0 W1 W2 W3 W4 W5 ... W0 : W1 : W2 : W3 : W4 : W5 : WS => WS
- rule #exec [ CO:CallOp ] => #gas [ CO , CO W0 W1 W2 W3 W4 W5 W6 ] ~> CO W0 W1 W2 W3 W4 W5 W6 ... W0 : W1 : W2 : W3 : W4 : W5 : W6 : WS => WS
+ rule #exec [ CSO:CallSixOp ] => #gas [ CSO , CSO W0 W1 W2 W3 W4 W5 ] ~> CSO W0 W1 W2 W3 W4 W5 ... ListItem(W0) ListItem(W1) ListItem(W2) ListItem(W3) ListItem(W4) ListItem(W5) => .List ...
+ rule #exec [ CO:CallOp ] => #gas [ CO , CO W0 W1 W2 W3 W4 W5 W6 ] ~> CO W0 W1 W2 W3 W4 W5 W6 ... ListItem(W0) ListItem(W1) ListItem(W2) ListItem(W3) ListItem(W4) ListItem(W5) ListItem(W6) => .List ...
```
### Address Conversion
@@ -481,11 +481,11 @@ We make sure the given arguments (to be interpreted as addresses) are with 160 b
syntax InternalOp ::= "#addr" "[" OpCode "]"
// --------------------------------------------
rule #addr [ OP:OpCode ] => .K ...
- (W0 => #addr(W0)) : _WS
+ WS => WS [ 0 <- #addr({WS [ 0 ]}:>Int) ]
requires isAddr1Op(OP)
rule #addr [ OP:OpCode ] => .K ...
- _W0 : (W1 => #addr(W1)) : _WS
+ WS => WS [ 1 <- #addr({WS [ 1 ]}:>Int) ]
requires isAddr2Op(OP)
rule #addr [ OP:OpCode ] => .K ...
@@ -756,9 +756,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 W0:Int ~> #push => .K ... WS => W0 : WS
+ syntax InternalOp ::= "#push" | "#setStack" List
+ // ------------------------------------------------
+ rule W0:Int ~> #push => .K ... WS => pushList(W0, WS)
rule #setStack WS => .K ... _ => WS
```
@@ -881,8 +881,8 @@ Some operators don't calculate anything, they just push the stack around a bit.
syntax StackOp ::= DUP ( Int ) [symbol(DUP)]
| SWAP ( Int ) [symbol(SWAP)]
// ----------------------------------------------
- rule DUP(N) WS:WordStack => #setStack ((WS [ N -Int 1 ]) : WS) ...
- rule SWAP(N) (W0 : WS) => #setStack ((WS [ N -Int 1 ]) : (WS [ N -Int 1 := W0 ])) ...
+ rule DUP(N) WS:List => #setStack (pushList(WS [ N -Int 1 ], WS)) ...
+ rule SWAP(N) (ListItem(W0) WS) => #setStack (pushList(WS [ N -Int 1 ], (WS [ N -Int 1 <- W0 ]))) ...
syntax PushOp ::= "PUSHZERO"
| PUSH ( Int ) [symbol(PUSH)]
@@ -1155,10 +1155,10 @@ These operators query about the current return data buffer.
// ------------------------------------------
rule LOG(N) MEMSTART MEMWIDTH => .K ...
ACCT
- WS => #drop(N, WS)
+ WS => range(WS, N, 0)
LM
- L => L ListItem({ ACCT | WordStack2List(#take(N, WS)) | #range(LM, MEMSTART, MEMWIDTH) })
- requires #sizeWordStack(WS) >=Int N
+ L => L ListItem({ ACCT | range(WS, 0, size(WS) -Int N) | #range(LM, MEMSTART, MEMWIDTH) })
+ requires size(WS) >=Int N
```
Ethereum Network OpCodes
@@ -1387,12 +1387,12 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
syntax KItem ::= "#initVM"
// --------------------------
- rule #initVM => .K ...
- _ => 0
- _ => 0
-
- _ => .WordStack
- _ => .Bytes
+ rule #initVM => .K ...
+ _ => 0
+ _ => 0
+
+ _ => .List
+ _ => .Bytes
syntax KItem ::= "#loadProgram" Bytes [symbol(loadProgram)]
// -----------------------------------------------------------
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
index 9809c65428..9a3d998de8 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
@@ -22,7 +22,7 @@ module EVM-OPTIMIZATIONS
- ( WS => 0 : WS )
+ ( WS => pushList(0, WS) )
( PCOUNT => ( PCOUNT +Int 1 ) )
@@ -39,7 +39,7 @@ module EVM-OPTIMIZATIONS
...
requires ( Gbase < SCHED > <=Gas GAVAIL )
- andBool ( #sizeWordStack( WS ) <=Int 1023 )
+ andBool ( size(WS) <=Int 1023 )
[priority(40)]
rule
@@ -58,7 +58,7 @@ module EVM-OPTIMIZATIONS
PGM
- ( WS => #asWord( #range(PGM, PCOUNT +Int 1, N) ) : WS )
+ ( WS => pushList(#asWord( #range(PGM, PCOUNT +Int 1, N) ), WS) )
( PCOUNT => ( ( PCOUNT +Int N ) +Int 1 ) )
@@ -75,7 +75,7 @@ module EVM-OPTIMIZATIONS
...
requires ( Gverylow < SCHED > <=Gas GAVAIL )
- andBool ( #sizeWordStack( WS ) <=Int 1023 )
+ andBool ( size( WS ) <=Int 1023 )
[priority(40)]
rule
@@ -91,7 +91,7 @@ module EVM-OPTIMIZATIONS
- ( WS => WS [ ( N +Int -1 ) ] : WS )
+ ( WS => pushList(WS [ ( N +Int -1 ) ], WS) )
( PCOUNT => ( PCOUNT +Int 1 ) )
@@ -107,9 +107,9 @@ module EVM-OPTIMIZATIONS
...
- requires N <=Int #sizeWordStack(WS)
+ requires #stackNeeded(DUP(N)) <=Int size(WS)
andBool ( Gverylow < SCHED > <=Gas GAVAIL )
- andBool ( #sizeWordStack( WS ) <=Int 1023 )
+ andBool ( size( WS ) <=Int 1023 )
[priority(40)]
rule
@@ -125,7 +125,7 @@ module EVM-OPTIMIZATIONS
- ( W0 : WS => WS [ ( N +Int -1 ) ] : ( WS [ ( N +Int -1 ) := W0 ] ) )
+ ( ListItem(W0) WS => pushList(WS [ ( N +Int -1 ) ], ( WS [ ( N +Int -1 ) <- W0 ] )) )
( PCOUNT => ( PCOUNT +Int 1 ) )
@@ -141,9 +141,9 @@ module EVM-OPTIMIZATIONS
...
- requires N <=Int #sizeWordStack(W0 : WS)
+ requires #stackNeeded(SWAP(N)) <=Int size(WS) +Int 1
andBool ( Gverylow < SCHED > <=Gas GAVAIL )
- andBool ( #sizeWordStack( WS ) <=Int 1023 )
+ andBool ( size( WS ) <=Int 1023 )
[priority(40)]
rule
@@ -159,7 +159,7 @@ module EVM-OPTIMIZATIONS
- ( W0 : W1 : WS => chop( ( W0 +Int W1 ) ) : WS )
+ ( ListItem(W0) ListItem(W1) WS => pushList(chop( ( W0 +Int W1 ) ), WS) )
( PCOUNT => ( PCOUNT +Int 1 ) )
@@ -176,7 +176,7 @@ module EVM-OPTIMIZATIONS
...
requires ( Gverylow < SCHED > <=Gas GAVAIL )
- andBool ( #sizeWordStack( WS ) <=Int 1023 )
+ andBool ( size( WS ) <=Int 1023 )
[priority(40)]
rule
@@ -192,7 +192,7 @@ module EVM-OPTIMIZATIONS
- ( W0 : W1 : WS => chop( ( W0 -Int W1 ) ) : WS )
+ ( ListItem(W0) ListItem(W1) WS => pushList(chop( ( W0 -Int W1 ) ), WS) )
( PCOUNT => ( PCOUNT +Int 1 ) )
@@ -209,7 +209,7 @@ module EVM-OPTIMIZATIONS
...
requires ( Gverylow < SCHED > <=Gas GAVAIL )
- andBool (#sizeWordStack( WS ) <=Int 1023 )
+ andBool ( size( WS ) <=Int 1023 )
[priority(40)]
rule
@@ -225,7 +225,7 @@ module EVM-OPTIMIZATIONS
- ( W0 : W1 : WS => W0 &Int W1 : WS )
+ ( ListItem(W0) ListItem(W1) WS => pushList(W0 &Int W1, WS) )
( PCOUNT => ( PCOUNT +Int 1 ) )
@@ -242,7 +242,7 @@ module EVM-OPTIMIZATIONS
...
requires ( Gverylow < SCHED > <=Gas GAVAIL )
- andBool ( #sizeWordStack( WS ) <=Int 1023 )
+ andBool ( size( WS ) <=Int 1023 )
[priority(40)]
rule
@@ -258,7 +258,7 @@ module EVM-OPTIMIZATIONS
- ( W0 : W1 : WS => bool2Word( W0 pushList(bool2Word( W0
( PCOUNT => ( PCOUNT +Int 1 ) )
@@ -275,7 +275,7 @@ module EVM-OPTIMIZATIONS
...
requires ( Gverylow < SCHED > <=Gas GAVAIL )
- andBool ( #sizeWordStack( WS ) <=Int 1023 )
+ andBool ( size( WS ) <=Int 1023 )
[priority(40)]
rule
@@ -291,7 +291,7 @@ module EVM-OPTIMIZATIONS
- ( W0 : W1 : WS => bool2Word( W1 pushList(bool2Word( W1
( PCOUNT => ( PCOUNT +Int 1 ) )
@@ -308,7 +308,7 @@ module EVM-OPTIMIZATIONS
...
requires ( Gverylow < SCHED > <=Gas GAVAIL )
- andBool ( #sizeWordStack( WS ) <=Int 1023 )
+ andBool ( size( WS ) <=Int 1023 )
[priority(40)]
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
index cd0f16c98a..f3e53c7b90 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
@@ -38,7 +38,7 @@ module STATE-UTILS
_ => .Account
_ => .Bytes
_ => 0
- _ => .WordStack
+ _ => .List
_ => .Bytes
_ => 0
_ => 0
diff --git a/tests/failing/ContractCreationSpam_d0g0v0.json.expected b/tests/failing/ContractCreationSpam_d0g0v0.json.expected
index 418ee98613..23cad71b7a 100644
--- a/tests/failing/ContractCreationSpam_d0g0v0.json.expected
+++ b/tests/failing/ContractCreationSpam_d0g0v0.json.expected
@@ -51,7 +51,7 @@
0
- .WordStack
+ .List
b""
diff --git a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected
index b738957f30..b8b15865bf 100644
--- a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected
+++ b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected
@@ -51,7 +51,7 @@
0
- .WordStack
+ .List
b""
diff --git a/tests/templates/output-success-haskell.json b/tests/templates/output-success-haskell.json
index e40fedeffe..0bd2762086 100644
--- a/tests/templates/output-success-haskell.json
+++ b/tests/templates/output-success-haskell.json
@@ -48,7 +48,7 @@
0
- .WordStack
+ .List
b""
diff --git a/tests/templates/output-success-java.json b/tests/templates/output-success-java.json
deleted file mode 100644
index f01a5ebaa1..0000000000
--- a/tests/templates/output-success-java.json
+++ /dev/null
@@ -1,173 +0,0 @@
-
-
- .
-
-
- 0
-
-
- SUCCESS
-
-
- HOMESTEAD
-
-
- true
-
-
-
-
-
- .StatusCode
-
-
- .List
-
-
- .List
-
-
- .Set
-
-
-
- .WordStack
-
-
- .Set
-
-
- .Account
-
-
- .Account
-
-
- .WordStack
-
-
- 0
-
-
- .WordStack
-
-
- .Map
-
-
- 0
-
-
- 0
-
-
- 0
-
-
- 0
-
-
- false
-
-
- 0
-
-
-
-
- .Set
-
-
- .List
-
-
- 0
-
-
- .Set
-
-
- .Map
-
-
-
- 0
-
-
- .Account
-
-
- .List
-
-
-
- 0
-
-
- 0
-
-
- 0
-
-
- 0
-
-
- 0
-
-
- 0
-
-
- .WordStack
-
-
- 0
-
-
- 0
-
-
- 0
-
-
- 0
-
-
- 0
-
-
- .WordStack
-
-
- 0
-
-
- 0
-
-
- [ .JSONs ]
-
-
-
-
-
- 1
-
-
- .Map
-
-
- .List
-
-
- .List
-
-
- .Map
-
-
-
-
diff --git a/tests/templates/output-success-llvm.json b/tests/templates/output-success-llvm.json
index 8f79f3d68a..e6e5c37593 100644
--- a/tests/templates/output-success-llvm.json
+++ b/tests/templates/output-success-llvm.json
@@ -48,7 +48,7 @@
0
- .WordStack
+ .List
b""