Skip to content

Commit

Permalink
Update <wordstack> cell to use List sort (#3)
Browse files Browse the repository at this point in the history 
See runtimeverification#2364
  • Loading branch information
@Robertorosmaninho
Dwight Guth authored and Robertorosmaninho committed Jul 5, 2024
1 parent 97f02ee commit a1b9739
Show file tree
Hide file tree
Showing 8 changed files with 63 additions and 236 deletions.
76 changes: 38 additions & 38 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,12 +63,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>
Expand Down Expand Up @@ -354,11 +354,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) <Int #stackNeeded(OP)
rule #stackOverflow (WS, OP) => #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) <Int #stackNeeded(OP)
rule #stackOverflow (WS, OP) => size(WS) +Int #stackDelta(OP) >Int 1024
syntax Int ::= #stackNeeded ( OpCode ) [symbol(#stackNeeded), function]
// -----------------------------------------------------------------------
Expand Down Expand Up @@ -407,12 +407,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 ) [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
Expand Down Expand Up @@ -446,17 +446,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>
```

Expand All @@ -466,8 +466,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
Expand All @@ -479,11 +479,11 @@ 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>
<wordStack> WS => WS [ 0 <- #addr({WS [ 0 ]}:>Int) ] </wordStack>
requires isAddr1Op(OP)
rule <k> #addr [ OP:OpCode ] => .K ... </k>
<wordStack> _W0 : (W1 => #addr(W1)) : _WS </wordStack>
<wordStack> WS => WS [ 1 <- #addr({WS [ 1 ]}:>Int) ] </wordStack>
requires isAddr2Op(OP)
rule <k> #addr [ OP:OpCode ] => .K ... </k>
Expand Down Expand Up @@ -729,9 +729,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>
```

Expand Down Expand Up @@ -853,8 +853,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 <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 ) [symbol(PUSH)]
Expand Down Expand Up @@ -1122,10 +1122,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
Expand Down Expand Up @@ -1331,12 +1331,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 [symbol(loadProgram)]
// -----------------------------------------------------------
Expand Down
40 changes: 20 additions & 20 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ module EVM-OPTIMIZATIONS
<evm>
<callState>
<wordStack>
( WS => 0 : WS )
( WS => pushList(0, WS) )
</wordStack>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
Expand All @@ -39,7 +39,7 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires ( Gbase < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( 0 : WS ) <=Int 1024 )
andBool ( size(WS) <=Int 1023 )
[priority(40)]
rule
Expand All @@ -58,7 +58,7 @@ module EVM-OPTIMIZATIONS
PGM
</program>
<wordStack>
( WS => #asWord( #range(PGM, PCOUNT +Int 1, N) ) : WS )
( WS => pushList(#asWord( #range(PGM, PCOUNT +Int 1, N) ), WS) )
</wordStack>
<pc>
( PCOUNT => ( ( PCOUNT +Int N ) +Int 1 ) )
Expand All @@ -75,7 +75,7 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( #asWord( #range(PGM, PCOUNT +Int 1, N) ) : WS ) <=Int 1024 )
andBool ( size( WS ) <=Int 1023 )
[priority(40)]
rule
Expand All @@ -91,7 +91,7 @@ module EVM-OPTIMIZATIONS
<evm>
<callState>
<wordStack>
( WS => WS [ ( N +Int -1 ) ] : WS )
( WS => pushList(WS [ ( N +Int -1 ) ], WS) )
</wordStack>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
Expand All @@ -107,9 +107,9 @@ module EVM-OPTIMIZATIONS
</ethereum>
...
</kevm>
requires #stackNeeded(DUP(N)) <=Int #sizeWordStack(WS)
requires #stackNeeded(DUP(N)) <=Int size(WS)
andBool ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( WS [ ( N +Int -1 ) ] : WS ) <=Int 1024 )
andBool ( size( WS ) <=Int 1023 )
[priority(40)]
rule
Expand All @@ -125,7 +125,7 @@ module EVM-OPTIMIZATIONS
<evm>
<callState>
<wordStack>
( W0 : WS => WS [ ( N +Int -1 ) ] : ( WS [ ( N +Int -1 ) := W0 ] ) )
( ListItem(W0) WS => pushList(WS [ ( N +Int -1 ) ], ( WS [ ( N +Int -1 ) <- W0 ] )) )
</wordStack>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
Expand All @@ -141,9 +141,9 @@ module EVM-OPTIMIZATIONS
</ethereum>
...
</kevm>
requires #stackNeeded(SWAP(N)) <=Int #sizeWordStack(W0 : WS)
requires #stackNeeded(SWAP(N)) <=Int size(WS) +Int 1
andBool ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( WS [ ( N +Int -1 ) ] : ( WS [ ( N +Int -1 ) := W0 ] ) ) <=Int 1024 )
andBool ( size( WS ) <=Int 1023 )
[priority(40)]
rule
Expand All @@ -159,7 +159,7 @@ module EVM-OPTIMIZATIONS
<evm>
<callState>
<wordStack>
( W0 : W1 : WS => chop( ( W0 +Int W1 ) ) : WS )
( ListItem(W0) ListItem(W1) WS => pushList(chop( ( W0 +Int W1 ) ), WS) )
</wordStack>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
Expand All @@ -176,7 +176,7 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( chop( ( W0 +Int W1 ) ) : WS ) <=Int 1024 )
andBool ( size( WS ) <=Int 1023 )
[priority(40)]
rule
Expand All @@ -192,7 +192,7 @@ module EVM-OPTIMIZATIONS
<evm>
<callState>
<wordStack>
( W0 : W1 : WS => chop( ( W0 -Int W1 ) ) : WS )
( ListItem(W0) ListItem(W1) WS => pushList(chop( ( W0 -Int W1 ) ), WS) )
</wordStack>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
Expand All @@ -209,7 +209,7 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( chop( ( W0 -Int W1 ) ) : WS ) <=Int 1024 )
andBool ( size( WS ) <=Int 1023 )
[priority(40)]
rule
Expand All @@ -225,7 +225,7 @@ module EVM-OPTIMIZATIONS
<evm>
<callState>
<wordStack>
( W0 : W1 : WS => W0 &Int W1 : WS )
( ListItem(W0) ListItem(W1) WS => pushList(W0 &Int W1, WS) )
</wordStack>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
Expand All @@ -242,7 +242,7 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( W0 &Int W1 : WS ) <=Int 1024 )
andBool ( size( WS ) <=Int 1023 )
[priority(40)]
rule
Expand All @@ -258,7 +258,7 @@ module EVM-OPTIMIZATIONS
<evm>
<callState>
<wordStack>
( W0 : W1 : WS => bool2Word( W0 <Int W1 ) : WS )
( ListItem(W0) ListItem(W1) WS => pushList(bool2Word( W0 <Int W1 ), WS) )
</wordStack>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
Expand All @@ -275,7 +275,7 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( bool2Word( W0 <Int W1 ) : WS ) <=Int 1024 )
andBool ( size( WS ) <=Int 1023 )
[priority(40)]
rule
Expand All @@ -291,7 +291,7 @@ module EVM-OPTIMIZATIONS
<evm>
<callState>
<wordStack>
( W0 : W1 : WS => bool2Word( W1 <Int W0 ) : WS )
( ListItem(W0) ListItem(W1) WS => pushList(bool2Word( W1 <Int W0 ), WS) )
</wordStack>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
Expand All @@ -308,7 +308,7 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( bool2Word( W1 <Int W0 ) : WS ) <=Int 1024 )
andBool ( size( WS ) <=Int 1023 )
[priority(40)]
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ module STATE-UTILS
<caller> _ => .Account </caller>
<callData> _ => .Bytes </callData>
<callValue> _ => 0 </callValue>
<wordStack> _ => .WordStack </wordStack>
<wordStack> _ => .List </wordStack>
<localMem> _ => .Bytes </localMem>
<pc> _ => 0 </pc>
<gas> _ => 0 </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/failing/ContractCreationSpam_d0g0v0.json.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@
0
</callValue>
<wordStack>
.WordStack
.List
</wordStack>
<localMem>
b""
Expand Down
2 changes: 1 addition & 1 deletion tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@
0
</callValue>
<wordStack>
.WordStack
.List
</wordStack>
<localMem>
b""
Expand Down
2 changes: 1 addition & 1 deletion tests/templates/output-success-haskell.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@
0
</callValue>
<wordStack>
.WordStack
.List
</wordStack>
<localMem>
b""
Expand Down
Loading

0 comments on commit a1b9739

Please sign in to comment.