From 05446f7a47c3f9dc235edb0c18de46cc1eb9fffc Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Thu, 16 Jul 2026 18:38:58 +0300 Subject: [PATCH 1/2] kproj/{evm,schedule}.md: implement eip-8024 dupn/swapn/exchange Add the three backward-compatible stack opcodes (EIP-8024): DUPN (0xe6), SWAPN (0xe7), EXCHANGE (0xe8), each with a 1-byte immediate and Gverylow (3) cost, gated on the new Ghaseip8024 flag (true at AMSTERDAM). Modeled as StackOps that read and decode their immediate from at exec time (like PUSH): decode_single ((x+145)%256, valid x in [0,90]u[128,255]) for DUPN/SWAPN, decode_pair (k=x^143; divmod(k,16)) for EXCHANGE. DUPN(n)/SWAPN(n) reuse the DUP/SWAP stack logic; EXCHANGE swaps two arbitrary positions. Out-of-range immediates halt EVMC_INVALID_INSTRUCTION, insufficient depth halts EVMC_STACK_UNDERFLOW; #widthOp is 2 (pc advances past the immediate). Jumpdest analysis (#widthOpCode) is intentionally left unchanged: EIP-8024's immediates are constrained to never be a JUMPDEST or PUSH byte, so scanning the immediate as an ordinary opcode keeps old jumpdest analysis valid (the backward-compatibility property; confirmed by the jump_to_immediate_byte fixtures). Unmask all 53 eip8024 fixtures. Co-Authored-By: Claude Opus 4.8 --- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 77 ++++++++++++++++++- .../kevm_pyk/kproj/evm-semantics/schedule.md | 9 ++- 2 files changed, 81 insertions(+), 5 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 fe6317d3e4..9f21740e5c 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -410,6 +410,9 @@ The `#next [_]` operator initiates execution by: rule #stackNeeded(_QOP:QuadStackOp) => 4 rule #stackNeeded(DUP(N)) => N rule #stackNeeded(SWAP(N)) => N +Int 1 + rule #stackNeeded(DUPN) => 0 + rule #stackNeeded(SWAPN) => 0 + rule #stackNeeded(EXCHANGE) => 0 rule #stackNeeded(LOG(N)) => N +Int 2 rule #stackNeeded(_CSOP:CallSixOp) => 6 rule #stackNeeded(COP:CallOp) => 7 requires notBool isCallSixOp(COP) @@ -435,6 +438,9 @@ The `#next [_]` operator initiates execution by: rule #stackAdded(LOG(_)) => 0 rule #stackAdded(SWAP(N)) => N +Int 1 rule #stackAdded(DUP(N)) => N +Int 1 + rule #stackAdded(DUPN) => 1 + rule #stackAdded(SWAPN) => 0 + rule #stackAdded(EXCHANGE) => 0 rule #stackAdded(_IOP:InvalidOp) => 0 rule #stackAdded(_OP) => 1 [owise] @@ -560,8 +566,11 @@ The arguments to `PUSH` must be skipped over (as they are inline), and the opcod syntax Int ::= #widthOp ( OpCode ) [symbol(#widthOp), function, total] // ---------------------------------------------------------------------- - rule #widthOp(PUSH(N)) => 1 +Int N - rule #widthOp(_) => 1 [owise] + rule #widthOp(PUSH(N)) => 1 +Int N + rule #widthOp(DUPN) => 2 + rule #widthOp(SWAPN) => 2 + rule #widthOp(EXCHANGE) => 2 + rule #widthOp(_) => 1 [owise] ``` After executing a transaction, it's necessary to have the effect of the substate log recorded. @@ -1152,6 +1161,64 @@ Some operators don't calculate anything, they just push the stack around a bit. 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 ])) ... + syntax StackOp ::= "DUPN" | "SWAPN" | "EXCHANGE" + // ------------------------------------------------ + rule DUPN WS:WordStack => #setStack ((WS [ #decodeSingle(#immByte(PGM, PCOUNT)) -Int 1 ]) : WS) ... + PGM PCOUNT + requires #validSingle(#immByte(PGM, PCOUNT)) andBool #decodeSingle(#immByte(PGM, PCOUNT)) <=Int #sizeWordStack(WS) + rule DUPN WS:WordStack => #end EVMC_STACK_UNDERFLOW ... + PGM PCOUNT + requires #validSingle(#immByte(PGM, PCOUNT)) andBool #decodeSingle(#immByte(PGM, PCOUNT)) >Int #sizeWordStack(WS) + rule DUPN _:WordStack => #end EVMC_INVALID_INSTRUCTION ... + PGM PCOUNT + requires notBool #validSingle(#immByte(PGM, PCOUNT)) + + rule SWAPN (W0 : WS) => #setStack ((WS [ #decodeSingle(#immByte(PGM, PCOUNT)) -Int 1 ]) : (WS [ #decodeSingle(#immByte(PGM, PCOUNT)) -Int 1 := W0 ])) ... + PGM PCOUNT + requires #validSingle(#immByte(PGM, PCOUNT)) andBool #decodeSingle(#immByte(PGM, PCOUNT)) +Int 1 <=Int #sizeWordStack(W0 : WS) + rule SWAPN WS:WordStack => #end EVMC_STACK_UNDERFLOW ... + PGM PCOUNT + requires #validSingle(#immByte(PGM, PCOUNT)) andBool #decodeSingle(#immByte(PGM, PCOUNT)) +Int 1 >Int #sizeWordStack(WS) + rule SWAPN _:WordStack => #end EVMC_INVALID_INSTRUCTION ... + PGM PCOUNT + requires notBool #validSingle(#immByte(PGM, PCOUNT)) + + rule EXCHANGE WS:WordStack => #setStack (WS [ #decodePairA(#immByte(PGM, PCOUNT)) := WS [ #decodePairB(#immByte(PGM, PCOUNT)) ] ] [ #decodePairB(#immByte(PGM, PCOUNT)) := WS [ #decodePairA(#immByte(PGM, PCOUNT)) ] ]) ... + PGM PCOUNT + requires #validPair(#immByte(PGM, PCOUNT)) andBool maxInt(#decodePairA(#immByte(PGM, PCOUNT)), #decodePairB(#immByte(PGM, PCOUNT))) EXCHANGE WS:WordStack => #end EVMC_STACK_UNDERFLOW ... + PGM PCOUNT + requires #validPair(#immByte(PGM, PCOUNT)) andBool maxInt(#decodePairA(#immByte(PGM, PCOUNT)), #decodePairB(#immByte(PGM, PCOUNT))) >=Int #sizeWordStack(WS) + rule EXCHANGE _:WordStack => #end EVMC_INVALID_INSTRUCTION ... + PGM PCOUNT + requires notBool #validPair(#immByte(PGM, PCOUNT)) + + syntax Int ::= "#immByte" "(" Bytes "," Int ")" [function, total] + // ------------------------------------------------------------------ + rule #immByte(PGM, PCOUNT) => #asWord(#range(PGM, PCOUNT +Int 1, 1)) + + syntax Int ::= "#decodeSingle" "(" Int ")" [function, total] + | "#decodePairA" "(" Int ")" [function, total] + | "#decodePairB" "(" Int ")" [function, total] + | "#decodePairA" "(" Int "," Int ")" [function, total] + | "#decodePairB" "(" Int "," Int ")" [function, total] + // -------------------------------------------------------------------- + rule #decodeSingle(X) => (X +Int 145) modInt 256 + + rule #decodePairA(X) => #decodePairA((X xorInt 143) /Int 16, (X xorInt 143) modInt 16) + rule #decodePairA(HI, LO) => HI +Int 1 requires HI LO +Int 1 requires HI >=Int LO + + rule #decodePairB(X) => #decodePairB((X xorInt 143) /Int 16, (X xorInt 143) modInt 16) + rule #decodePairB(HI, LO) => LO +Int 1 requires HI 29 -Int HI requires HI >=Int LO + + syntax Bool ::= "#validSingle" "(" Int ")" [function, total] + | "#validPair" "(" Int ")" [function, total] + // ------------------------------------------------------------- + rule #validSingle(X) => X <=Int 90 orBool X >=Int 128 + rule #validPair(X) => X <=Int 81 orBool X >=Int 128 + syntax PushOp ::= "PUSHZERO" | PUSH ( Int ) [symbol(PUSH)] // --------------------------------------------- @@ -2993,6 +3060,9 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). rule #gasExec(SCHED, PUSH(_)) => Gverylow < SCHED > ... rule #gasExec(SCHED, DUP(_) _) => Gverylow < SCHED > ... rule #gasExec(SCHED, SWAP(_) _) => Gverylow < SCHED > ... + rule #gasExec(SCHED, DUPN _) => Gverylow < SCHED > ... + rule #gasExec(SCHED, SWAPN _) => Gverylow < SCHED > ... + rule #gasExec(SCHED, EXCHANGE _) => Gverylow < SCHED > ... rule #gasExec(SCHED, BLOBHASH _) => Gverylow < SCHED > ... // Wlow @@ -3336,6 +3406,9 @@ After interpreting the strings representing programs as a `WordStack`, it should rule #dasmOpCode( 162, _ ) => LOG(2) rule #dasmOpCode( 163, _ ) => LOG(3) rule #dasmOpCode( 164, _ ) => LOG(4) + rule #dasmOpCode( 230, SCHED ) => DUPN requires Ghaseip8024 << SCHED >> + rule #dasmOpCode( 231, SCHED ) => SWAPN requires Ghaseip8024 << SCHED >> + rule #dasmOpCode( 232, SCHED ) => EXCHANGE requires Ghaseip8024 << SCHED >> rule #dasmOpCode( 240, _ ) => CREATE rule #dasmOpCode( 241, _ ) => CALL rule #dasmOpCode( 242, _ ) => CALLCODE diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md index b5f4f3f157..80da63de2a 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md @@ -31,8 +31,8 @@ module SCHEDULE | "Ghaswarmcoinbase" | "Ghaswithdrawals" | "Ghastransient" | "Ghasmcopy" | "Ghasbeaconroot" | "Ghaseip6780" | "Ghasblobbasefee" | "Ghasblobhash" | "Ghasbls12msmdiscount" | "Ghashistory" | "Ghasrequests" | "Ghasauthority" - | "Ghasfloorcost" | "Ghasclz" - // ------------------------------------------------------------- + | "Ghasfloorcost" | "Ghasclz" | "Ghaseip8024" + // --------------------------------------------------------------------------------------- ``` ### Schedule Constants @@ -183,6 +183,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule [GhasauthorityDefault]: Ghasauthority << DEFAULT >> => false rule [GhasfloorcostDefault]: Ghasfloorcost << DEFAULT >> => false rule [GhasclzDefault]: Ghasclz << DEFAULT >> => false + rule [Ghaseip8024Default]: Ghaseip8024 << DEFAULT >> => false ``` ### Frontier Schedule @@ -526,7 +527,9 @@ A `ScheduleConst` is a constant determined by the fee schedule. orBool SCHEDCONST ==K Blobbasefeeupdatefraction ) - rule [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >> + rule [Ghaseip8024Amsterdam]: Ghaseip8024 << AMSTERDAM >> => true + rule [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >> + requires notBool ( SCHEDFLAG ==K Ghaseip8024 ) ``` ```k From 123e178b03aa8c9b99d0545fcb4e09fbfc9bfaa5 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Fri, 24 Jul 2026 23:17:06 +0300 Subject: [PATCH 2/2] formatting + renaming functions --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 14 +++++++------- .../src/kevm_pyk/kproj/evm-semantics/schedule.md | 4 ++-- 2 files changed, 9 insertions(+), 9 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 9f21740e5c..ef1f80616b 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1194,7 +1194,7 @@ Some operators don't calculate anything, they just push the stack around a bit. requires notBool #validPair(#immByte(PGM, PCOUNT)) syntax Int ::= "#immByte" "(" Bytes "," Int ")" [function, total] - // ------------------------------------------------------------------ + // ----------------------------------------------------------------- rule #immByte(PGM, PCOUNT) => #asWord(#range(PGM, PCOUNT +Int 1, 1)) syntax Int ::= "#decodeSingle" "(" Int ")" [function, total] @@ -1202,20 +1202,20 @@ Some operators don't calculate anything, they just push the stack around a bit. | "#decodePairB" "(" Int ")" [function, total] | "#decodePairA" "(" Int "," Int ")" [function, total] | "#decodePairB" "(" Int "," Int ")" [function, total] - // -------------------------------------------------------------------- + // ------------------------------------------------------------------- rule #decodeSingle(X) => (X +Int 145) modInt 256 rule #decodePairA(X) => #decodePairA((X xorInt 143) /Int 16, (X xorInt 143) modInt 16) - rule #decodePairA(HI, LO) => HI +Int 1 requires HI LO +Int 1 requires HI >=Int LO + rule #decodePairA(Q, R) => Q +Int 1 requires Q R +Int 1 requires Q >=Int R rule #decodePairB(X) => #decodePairB((X xorInt 143) /Int 16, (X xorInt 143) modInt 16) - rule #decodePairB(HI, LO) => LO +Int 1 requires HI 29 -Int HI requires HI >=Int LO + rule #decodePairB(Q, R) => R +Int 1 requires Q 29 -Int Q requires Q >=Int R syntax Bool ::= "#validSingle" "(" Int ")" [function, total] | "#validPair" "(" Int ")" [function, total] - // ------------------------------------------------------------- + // ------------------------------------------------------------ rule #validSingle(X) => X <=Int 90 orBool X >=Int 128 rule #validPair(X) => X <=Int 81 orBool X >=Int 128 diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md index 80da63de2a..20557eca3f 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md @@ -527,8 +527,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. orBool SCHEDCONST ==K Blobbasefeeupdatefraction ) - rule [Ghaseip8024Amsterdam]: Ghaseip8024 << AMSTERDAM >> => true - rule [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >> + rule [Ghaseip8024Amsterdam]: Ghaseip8024 << AMSTERDAM >> => true + rule [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >> requires notBool ( SCHEDFLAG ==K Ghaseip8024 ) ```