From 699434b90dcdaccfbfb844a82ae12e02ea776a29 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 1 Mar 2024 10:25:08 -0600 Subject: [PATCH 01/12] use List instead of WordStack for wordStack cell --- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 74 +++++++++---------- .../kproj/evm-semantics/optimizations.md | 40 +++++----- .../kproj/evm-semantics/state-utils.md | 2 +- 3 files changed, 58 insertions(+), 58 deletions(-) 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 54cbaa3bc2..26606d31ae 100644 --- 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 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 @@ -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) #sizeWordStack(WS) +Int #stackDelta(OP) >Int 1024 + rule #stackUnderflow(WS, OP:OpCode) => size(WS) 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 `` 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 #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 ``` @@ -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 #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 @@ -476,11 +476,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 ... @@ -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 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 ``` @@ -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 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 ) [klabel(PUSH)] @@ -1131,10 +1131,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 @@ -1341,12 +1341,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 // ------------------------------------- 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 4248d1dc5a..54e211ad5a 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md @@ -37,7 +37,7 @@ module EVM-OPTIMIZATIONS - ( WS => 0 : WS ) + ( WS => pushList(0, WS) ) ( PCOUNT => ( PCOUNT +Int 1 ) ) @@ -54,7 +54,7 @@ module EVM-OPTIMIZATIONS ... requires ( #if USEGAS #then Gbase < SCHED > <=Gas GAVAIL #else true #fi ) - andBool ( #sizeWordStack( 0 : WS ) <=Int 1024 ) + andBool ( size(WS) <=Int 1023 ) [priority(40)] rule @@ -75,7 +75,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 ) ) @@ -92,7 +92,7 @@ module EVM-OPTIMIZATIONS ... requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi ) - andBool ( #sizeWordStack( #asWord( #range(PGM, PCOUNT +Int 1, N) ) : WS ) <=Int 1024 ) + andBool ( size( WS ) <=Int 1023 ) [priority(40)] rule @@ -110,7 +110,7 @@ module EVM-OPTIMIZATIONS - ( WS => WS [ ( N +Int -1 ) ] : WS ) + ( WS => pushList(WS [ ( N +Int -1 ) ], WS) ) ( PCOUNT => ( PCOUNT +Int 1 ) ) @@ -126,9 +126,9 @@ module EVM-OPTIMIZATIONS ... - requires #stackNeeded(DUP(N)) <=Int #sizeWordStack(WS) + requires #stackNeeded(DUP(N)) <=Int size(WS) andBool ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi ) - andBool ( #sizeWordStack( WS [ ( N +Int -1 ) ] : WS ) <=Int 1024 ) + andBool ( size( WS ) <=Int 1023 ) [priority(40)] rule @@ -146,7 +146,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 ) ) @@ -162,9 +162,9 @@ module EVM-OPTIMIZATIONS ... - requires #stackNeeded(SWAP(N)) <=Int #sizeWordStack(W0 : WS) + requires #stackNeeded(SWAP(N)) <=Int size(WS) +Int 1 andBool ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi ) - andBool ( #sizeWordStack( WS [ ( N +Int -1 ) ] : ( WS [ ( N +Int -1 ) := W0 ] ) ) <=Int 1024 ) + andBool ( size( WS ) <=Int 1023 ) [priority(40)] rule @@ -182,7 +182,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 ) ) @@ -199,7 +199,7 @@ module EVM-OPTIMIZATIONS ... requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi ) - andBool ( #sizeWordStack( chop( ( W0 +Int W1 ) ) : WS ) <=Int 1024 ) + andBool ( size( WS ) <=Int 1023 ) [priority(40)] rule @@ -217,7 +217,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 ) ) @@ -234,7 +234,7 @@ module EVM-OPTIMIZATIONS ... requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi ) - andBool ( #sizeWordStack( chop( ( W0 -Int W1 ) ) : WS ) <=Int 1024 ) + andBool ( size( WS ) <=Int 1023 ) [priority(40)] rule @@ -252,7 +252,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 ) ) @@ -269,7 +269,7 @@ module EVM-OPTIMIZATIONS ... requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi ) - andBool ( #sizeWordStack( W0 &Int W1 : WS ) <=Int 1024 ) + andBool ( size( WS ) <=Int 1023 ) [priority(40)] rule @@ -287,7 +287,7 @@ module EVM-OPTIMIZATIONS - ( W0 : W1 : WS => bool2Word( W0 pushList(bool2Word( W0 ( PCOUNT => ( PCOUNT +Int 1 ) ) @@ -304,7 +304,7 @@ module EVM-OPTIMIZATIONS ... requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi ) - andBool ( #sizeWordStack( bool2Word( W0 - ( W0 : W1 : WS => bool2Word( W1 pushList(bool2Word( W1 ( PCOUNT => ( PCOUNT +Int 1 ) ) @@ -339,7 +339,7 @@ module EVM-OPTIMIZATIONS ... requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi ) - andBool ( #sizeWordStack( bool2Word( W1 _ => .Account _ => .Bytes _ => 0 - _ => .WordStack + _ => .List _ => .Bytes _ => 0 _ => 0 From 7406739a175a53cdbf4eff520b38e99ab25b11bf Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 19 Mar 2024 12:21:25 -0500 Subject: [PATCH 02/12] update templates --- tests/templates/output-success-haskell.json | 2 +- tests/templates/output-success-java.json | 2 +- tests/templates/output-success-llvm.json | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/templates/output-success-haskell.json b/tests/templates/output-success-haskell.json index 5f8fca8169..4f1964e7de 100644 --- a/tests/templates/output-success-haskell.json +++ b/tests/templates/output-success-haskell.json @@ -51,7 +51,7 @@ 0 - .WordStack + .List b"" diff --git a/tests/templates/output-success-java.json b/tests/templates/output-success-java.json index aa8fad8c45..980d372f52 100644 --- a/tests/templates/output-success-java.json +++ b/tests/templates/output-success-java.json @@ -51,7 +51,7 @@ 0 - .WordStack + .List .Map diff --git a/tests/templates/output-success-llvm.json b/tests/templates/output-success-llvm.json index 50fe02f21c..b2ca90feda 100644 --- a/tests/templates/output-success-llvm.json +++ b/tests/templates/output-success-llvm.json @@ -51,7 +51,7 @@ 0 - .WordStack + .List b"" From 57e39aa7678318e4f3134c3785c66704195f5752 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 19 Mar 2024 14:01:40 -0500 Subject: [PATCH 03/12] update failing test outputs --- tests/failing/ContractCreationSpam_d0g0v0.json.expected | 2 +- ...ic_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/failing/ContractCreationSpam_d0g0v0.json.expected b/tests/failing/ContractCreationSpam_d0g0v0.json.expected index af9c8c9aef..311dc19574 100644 --- a/tests/failing/ContractCreationSpam_d0g0v0.json.expected +++ b/tests/failing/ContractCreationSpam_d0g0v0.json.expected @@ -54,7 +54,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 e43ece4a53..ef3ade4799 100644 --- a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected +++ b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected @@ -54,7 +54,7 @@ 0 - .WordStack + .List b"" From 09ce031636784f67bfabb9918c843e2a03fecb1f Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 25 Mar 2024 13:15:08 -0500 Subject: [PATCH 04/12] remove dead java backend code --- tests/templates/output-success-java.json | 173 ----------------------- 1 file changed, 173 deletions(-) delete mode 100644 tests/templates/output-success-java.json diff --git a/tests/templates/output-success-java.json b/tests/templates/output-success-java.json deleted file mode 100644 index 980d372f52..0000000000 --- a/tests/templates/output-success-java.json +++ /dev/null @@ -1,173 +0,0 @@ - - - . - - - 0 - - - SUCCESS - - - DEFAULT - - - true - - - - - .WordStack - - - .StatusCode - - - .List - - - .List - - - .Set - - - - .WordStack - - - .Set - - - .Account - - - .Account - - - .WordStack - - - 0 - - - .List - - - .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 - - - - From ee8f53890f0d7edd7d0a89ae3c32f5e5bee6609e Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 25 Mar 2024 13:16:12 -0500 Subject: [PATCH 05/12] make WordStack constructors macros --- .../kevm_pyk/kproj/evm-semantics/evm-types.md | 85 ++----------------- 1 file changed, 5 insertions(+), 80 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 index 8255fe104f..0521784925 100644 --- 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:Int : L:List => ListItem(I) L ``` ```k @@ -238,83 +240,6 @@ A cons-list is used for the EVM wordstack. rule I : BS => Int2Bytes(1, I, BE) +Bytes BS requires I .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 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 (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) -``` - -- `#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. From b472aecd34e4e8071a6232870dcf7add018c29d3 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 25 Mar 2024 13:16:22 -0500 Subject: [PATCH 06/12] update kevm.py with new symbol names for WS constructors --- kevm-pyk/src/kevm_pyk/kevm.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index b44a4eb442..c0410c5f7a 100644 --- 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: From ce44b1ab7e09249f658dfe834fd170136f284b8a Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 25 Mar 2024 13:16:34 -0500 Subject: [PATCH 07/12] remove or fix lemmas that are now dead --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 2 +- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) 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 index e9abc747bb..8e6bf40112 100644 --- 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] 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 54e211ad5a..7d8ad7e05a 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md @@ -10,10 +10,8 @@ requires "lemmas/int-simplification.k" module EVM-OPTIMIZATIONS-LEMMAS imports EVM - rule #sizeWordStack(WS , N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0 [simplification] - rule #sizeWordStack(WS [ I := _ ], N) => #sizeWordStack(WS, N) requires I true [simplification] - rule #sizeWordStack(_ , 0) false requires N <=Int 0 [simplification] + rule 0 <=Int size(_:List) => true [simplification] + rule size(_:List) false requires N <=Int 0 [simplification] endmodule From e5f77cdfd4e07c821048b2e8a31bc19a6e4095bd Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 25 Mar 2024 13:22:11 -0500 Subject: [PATCH 08/12] fix format --- kevm-pyk/src/kevm_pyk/kevm.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index c0410c5f7a..c5173a079a 100644 --- 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', - '_WS_' + '_WS_', ] for symb in paren_symbols: if symb in symbol_table: From c0a7dfbf39f017ee543a6b9cd8a9202401e7f784 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 26 Mar 2024 11:36:10 -0500 Subject: [PATCH 09/12] fix uses of sizeWordStack in specs --- .../src/kevm_pyk/kproj/evm-semantics/evm-types.md | 9 +++++++++ tests/specs/benchmarks/verification.k | 11 ----------- tests/specs/examples/sum-to-n-spec.k | 6 +----- tests/specs/mcd/verification.k | 2 -- tests/specs/opcodes/verification.k | 3 +-- 5 files changed, 11 insertions(+), 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 index 0521784925..bde0f97a3d 100644 --- 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 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 index 5421baf819..bac88a47c3 100644 --- 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) #sizeWordStack(WS, 0) +Int N SIZELIMIT SIZELIMIT #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 index 21b945af6d..f2d4e15e55 100644 --- 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 index 3f5f7b22f2..260de26ca7 100644 --- 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 index 8f22daaf66..5a2982369c 100644 --- 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 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 From ed829d8ff8182aa6fba524800fe7171ab47f05d1 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 26 Mar 2024 12:52:53 -0500 Subject: [PATCH 10/12] fix booster aborting early --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 26606d31ae..91643edbf1 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -477,11 +477,11 @@ We make sure the given arguments (to be interpreted as addresses) are with 160 b // -------------------------------------------- rule #addr [ OP:OpCode ] => .K ... WS => WS [ 0 <- #addr({WS [ 0 ]}:>Int) ] - requires isAddr1Op(OP) + requires isAddr1Op(OP) [preserves-definedness] rule #addr [ OP:OpCode ] => .K ... WS => WS [ 1 <- #addr({WS [ 1 ]}:>Int) ] - requires isAddr2Op(OP) + requires isAddr2Op(OP) [preserves-definedness] rule #addr [ OP:OpCode ] => .K ... requires notBool ( isAddr1Op(OP) orBool isAddr2Op(OP) ) From 3021a471e4c4bd3b9e3445da0545911c746e0ac3 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 26 Mar 2024 14:50:39 -0500 Subject: [PATCH 11/12] fix compile error --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 index bde0f97a3d..6b69d78538 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -231,7 +231,7 @@ A cons-list is used for the EVM wordstack. | Int ":" List [macro, symbol(_WS_)] // --------------------------------------------------------- rule .WordStack => .List - rule I:Int : L:List => ListItem(I) L + rule I : L => ListItem(I) L ``` ```k From 15a332f0caa40a8666303104c50df0efd0a61e24 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 5 Apr 2024 16:55:19 +0000 Subject: [PATCH 12/12] Set Version: 1.0.521 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index d1690bc8f9..816742a244 100644 --- 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. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index a439c8484e..80373a1a39 100644 --- 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/package/version b/package/version index 9b522976a0..f7dc9a7a4c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.520 +1.0.521