diff --git a/kevm-pyk/src/kevm_pyk/gst_to_kore.py b/kevm-pyk/src/kevm_pyk/gst_to_kore.py
index fa7f92447c..eeb76fa7f3 100644
--- a/kevm-pyk/src/kevm_pyk/gst_to_kore.py
+++ b/kevm-pyk/src/kevm_pyk/gst_to_kore.py
@@ -7,7 +7,7 @@
from typing import TYPE_CHECKING
from pyk.cli.utils import file_path
-from pyk.kore.prelude import BOOL, INT, SORT_JSON, SORT_K_ITEM, bool_dv, inj, int_dv, json_to_kore, top_cell_initializer
+from pyk.kore.prelude import INT, SORT_JSON, SORT_K_ITEM, inj, int_dv, json_to_kore, top_cell_initializer
from pyk.kore.syntax import App, SortApp
from .cli import KEVMCLIArgs
@@ -39,7 +39,6 @@ def kore_pgm_to_kore(pgm: Pattern, pattern_sort: SortApp, schedule: str, mode: s
'$SCHEDULE': inj(SORT_SCHEDULE, SORT_K_ITEM, _schedule_to_kore(schedule)),
'$MODE': inj(SORT_MODE, SORT_K_ITEM, _mode_to_kore(mode)),
'$CHAINID': inj(INT, SORT_K_ITEM, int_dv(chainid)),
- '$USEGAS': inj(BOOL, SORT_K_ITEM, bool_dv(usegas)),
}
return top_cell_initializer(config)
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
index 40adff2f82..0cf1cb8feb 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
@@ -301,8 +301,6 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
rule loadCallState { "code" : (CODE:OpCodes), REST } => #loadProgram #asmOpCodes(CODE) ~> loadCallState { REST } ...
- rule loadCallState { "usegas" : (USEGAS:Bool), REST => REST } ... _ => USEGAS
-
rule loadCallState { KEY : ((VAL:String) => #parseWord(VAL)), _ } ...
requires KEY in (SetItem("gas") SetItem("gasPrice") SetItem("value"))
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..2a32b88d74 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -35,7 +35,6 @@ In the comments next to each cell, we've marked which component of the YellowPap
1
$MODE:Mode
$SCHEDULE:Schedule
- $USEGAS:Bool
@@ -552,7 +551,6 @@ After executing a transaction, it's necessary to have the effect of the substate
_ => .Map
rule #finalizeTx(false) ...
- true
SCHED
GAVAIL => G*(GAVAIL, GLIMIT, REFUND, SCHED)
REFUND => 0
@@ -565,7 +563,6 @@ After executing a transaction, it's necessary to have the effect of the substate
requires REFUND =/=Int 0
rule #finalizeTx(false => true) ...
- true
BFEE
ORG
MINER
@@ -592,7 +589,6 @@ After executing a transaction, it's necessary to have the effect of the substate
requires ORG =/=Int MINER
rule #finalizeTx(false => true) ...
- true
BFEE
ACCT
ACCT
@@ -612,14 +608,6 @@ After executing a transaction, it's necessary to have the effect of the substate
...
- rule #finalizeTx(false => true) ...
- false
- ListItem(MsgId:Int) REST => REST
-
- MsgId
- ...
-
-
rule (.K => #deleteAccounts(Set2List(ACCTS))) ~> #finalizeTx(true) ...
ACCTS => .Set
requires size(ACCTS) >Int 0
@@ -1319,13 +1307,12 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
=> #touchAccounts ACCTFROM ACCTTO ~> #accessAccounts ACCTFROM ACCTTO ~> #loadProgram BYTES ~> #initVM ~> #precompiled?(ACCTCODE, SCHED) ~> #execute
...
- USEGAS:Bool
CD => CD +Int 1
_ => ARGS
_ => APPVALUE
_ => ACCTTO
- GAVAIL:Gas => #if USEGAS #then GCALL:Gas #else GAVAIL:Gas #fi
- GCALL:Gas => #if USEGAS #then 0:Gas #else GCALL:Gas #fi
+ GAVAIL:Gas => GCALL:Gas
+ GCALL:Gas => 0:Gas
_ => ACCTFROM
OLDSTATIC:Bool => OLDSTATIC orBool STATIC
SCHED
@@ -1446,8 +1433,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
syntax InternalOp ::= "#refund" Gas
| "#setLocalMem" Int Int Bytes
// --------------------------------------------------
- rule [refund]: #refund G:Gas => .K ... GAVAIL => GAVAIL +Gas G true
- rule [refund.noGas]: #refund _ => .K ... false
+ rule [refund]: #refund G:Gas => .K ... GAVAIL => GAVAIL +Gas G
rule #setLocalMem START WIDTH WS => .K ...
@@ -1543,11 +1529,10 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
=> #touchAccounts ACCTFROM ACCTTO ~> #accessAccounts ACCTFROM ACCTTO ~> #loadProgram INITCODE ~> #initVM ~> #execute
...
- USEGAS
SCHED
_ => ACCTTO
- GAVAIL => #if USEGAS #then GCALL #else GAVAIL #fi
- GCALL => #if USEGAS #then 0 #else GCALL #fi
+ GAVAIL => GCALL
+ GCALL => 0
_ => ACCTFROM
CD => CD +Int 1
_ => .Bytes
@@ -1899,9 +1884,6 @@ Overall Gas
~> #access [ OP , AOP ]
...
- true
-
- rule #gas [ _ , _ ] => .K ... false
rule #gas [ OP ] => #gasExec(SCHED, OP) ~> #deductGas ...
SCHED
@@ -1919,9 +1901,8 @@ Overall Gas
MU => MU' SCHED
rule _G:Gas ~> (#deductMemoryGas => #deductGas) ... //Required for verification
- rule G:Gas ~> #deductGas => #end EVMC_OUT_OF_GAS ... GAVAIL:Gas true requires GAVAIL G:Gas ~> #deductGas => .K ... GAVAIL:Gas => GAVAIL -Gas G true requires G <=Gas GAVAIL
- rule _:Gas ~> #deductGas => .K ... false
+ rule G:Gas ~> #deductGas => #end EVMC_OUT_OF_GAS ... GAVAIL:Gas requires GAVAIL G:Gas ~> #deductGas => .K ... GAVAIL:Gas => GAVAIL -Gas G requires G <=Gas GAVAIL
syntax Bool ::= #inStorage ( Map , Account , Int ) [klabel(#inStorage), function, total]
| #inStorageAux1 ( KItem , Int ) [klabel(#inStorageAux1), function, total]
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..5050ea173a 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
@@ -30,9 +30,6 @@ module EVM-OPTIMIZATIONS
SCHED
-
- USEGAS
-
@@ -43,7 +40,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
- ( GAVAIL => ( #if USEGAS #then ( GAVAIL -Gas Gbase < SCHED > ) #else GAVAIL #fi ) )
+ ( GAVAIL => ( ( GAVAIL -Gas Gbase < SCHED > ) ) )
...
@@ -53,7 +50,7 @@ module EVM-OPTIMIZATIONS
...
- requires ( #if USEGAS #then Gbase < SCHED > <=Gas GAVAIL #else true #fi )
+ requires ( Gbase < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( 0 : WS ) <=Int 1024 )
[priority(40)]
@@ -65,9 +62,6 @@ module EVM-OPTIMIZATIONS
SCHED
-
- USEGAS
-
@@ -81,7 +75,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( ( PCOUNT +Int N ) +Int 1 ) )
- ( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
+ ( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
...
@@ -91,7 +85,7 @@ module EVM-OPTIMIZATIONS
...
- requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
+ requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( #asWord( #range(PGM, PCOUNT +Int 1, N) ) : WS ) <=Int 1024 )
[priority(40)]
@@ -103,9 +97,6 @@ module EVM-OPTIMIZATIONS
SCHED
-
- USEGAS
-
@@ -116,7 +107,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
- ( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
+ ( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
...
@@ -127,7 +118,7 @@ module EVM-OPTIMIZATIONS
...
requires #stackNeeded(DUP(N)) <=Int #sizeWordStack(WS)
- andBool ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
+ andBool ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( WS [ ( N +Int -1 ) ] : WS ) <=Int 1024 )
[priority(40)]
@@ -139,9 +130,6 @@ module EVM-OPTIMIZATIONS
SCHED
-
- USEGAS
-
@@ -152,7 +140,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
- ( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
+ ( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
...
@@ -163,7 +151,7 @@ module EVM-OPTIMIZATIONS
...
requires #stackNeeded(SWAP(N)) <=Int #sizeWordStack(W0 : WS)
- andBool ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
+ andBool ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( WS [ ( N +Int -1 ) ] : ( WS [ ( N +Int -1 ) := W0 ] ) ) <=Int 1024 )
[priority(40)]
@@ -175,9 +163,6 @@ module EVM-OPTIMIZATIONS
SCHED
-
- USEGAS
-
@@ -188,7 +173,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
- ( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
+ ( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
...
@@ -198,7 +183,7 @@ module EVM-OPTIMIZATIONS
...
- requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
+ requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( chop( ( W0 +Int W1 ) ) : WS ) <=Int 1024 )
[priority(40)]
@@ -210,9 +195,6 @@ module EVM-OPTIMIZATIONS
SCHED
-
- USEGAS
-
@@ -223,7 +205,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
- ( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
+ ( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
...
@@ -233,7 +215,7 @@ module EVM-OPTIMIZATIONS
...
- requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
+ requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( chop( ( W0 -Int W1 ) ) : WS ) <=Int 1024 )
[priority(40)]
@@ -245,9 +227,6 @@ module EVM-OPTIMIZATIONS
SCHED
-
- USEGAS
-
@@ -258,7 +237,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
- ( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
+ ( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
...
@@ -268,7 +247,7 @@ module EVM-OPTIMIZATIONS
...
- requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
+ requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( W0 &Int W1 : WS ) <=Int 1024 )
[priority(40)]
@@ -280,9 +259,6 @@ module EVM-OPTIMIZATIONS
SCHED
-
- USEGAS
-
@@ -293,7 +269,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
- ( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
+ ( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
...
@@ -303,7 +279,7 @@ module EVM-OPTIMIZATIONS
...
- requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
+ requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( bool2Word( W0
SCHED
-
- USEGAS
-
@@ -328,7 +301,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
- ( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
+ ( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
...
@@ -338,7 +311,7 @@ module EVM-OPTIMIZATIONS
...
- requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
+ requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( bool2Word( W1 loadCallState { "code" : CODE:Bytes, REST } => #loadProgram CODE ~> loadCallState { REST } ...
- rule loadCallState { "gas" : GLIMIT:Int, REST => REST } ... _ => GLIMIT true
- rule loadCallState { "gas" : _:Int, REST => REST } ... false
+ rule loadCallState { "gas" : GLIMIT:Int, REST => REST } ... _ => GLIMIT
rule loadCallState { "gasPrice" : GPRICE:Int, REST => REST } ... _ => GPRICE
rule loadCallState { "value" : VALUE:Int , REST => REST } ... _ => VALUE
diff --git a/tests/failing/ContractCreationSpam_d0g0v0.json.expected b/tests/failing/ContractCreationSpam_d0g0v0.json.expected
index af9c8c9aef..75be445773 100644
--- a/tests/failing/ContractCreationSpam_d0g0v0.json.expected
+++ b/tests/failing/ContractCreationSpam_d0g0v0.json.expected
@@ -11,9 +11,6 @@
BYZANTIUM
-
- true
-