From 51855e5fc65ec7c75559445b02ab44e883fdd569 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 16 Apr 2024 11:02:09 -0500 Subject: [PATCH] Update cell to use List sort (#3) See https://github.com/runtimeverification/evm-semantics/pull/2364 --- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 76 ++++---- .../kproj/evm-semantics/optimizations.md | 40 ++-- .../kproj/evm-semantics/state-utils.md | 2 +- .../ContractCreationSpam_d0g0v0.json.expected | 2 +- ...ecall_110_OOGMAfter_2_d0g0v0.json.expected | 2 +- tests/templates/output-success-haskell.json | 2 +- tests/templates/output-success-java.json | 173 ------------------ tests/templates/output-success-llvm.json | 2 +- 8 files changed, 63 insertions(+), 236 deletions(-) delete mode 100644 tests/templates/output-success-java.json 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 423715ea68..d72c96f36a 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 @@ -358,11 +358,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] // ----------------------------------------------------------------------- @@ -411,12 +411,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 @@ -451,17 +451,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 ``` @@ -471,8 +471,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 @@ -484,11 +484,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 ... @@ -760,9 +760,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 ``` @@ -906,8 +906,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)] @@ -1182,10 +1182,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 @@ -1414,12 +1414,12 @@ The various `CALL*` (and other inter-contract control flow) operations will be d syntax KItem ::= "#initVM" // -------------------------- - rule #initVM => .K ... - _ => 0 - _ => 0 - _ => .Bytes - _ => .WordStack - _ => .Bytes + rule #initVM => .K ... + _ => 0 + _ => 0 + _ => .Bytes + _ => .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 3baa1f292f..15ec1d0e90 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 b0025afeb5..1c9406b59b 100644 --- a/tests/failing/ContractCreationSpam_d0g0v0.json.expected +++ b/tests/failing/ContractCreationSpam_d0g0v0.json.expected @@ -48,7 +48,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 af76afc026..18718ea3f2 100644 --- a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected +++ b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected @@ -48,7 +48,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 - - - - - .WordStack - - - .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""