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..ef1f80616b 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(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(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
+
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..20557eca3f 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