Skip to content

Commit 234170f

Browse files
committed
revert debug edits
1 parent 76dac24 commit 234170f

1 file changed

Lines changed: 3 additions & 3 deletions

File tree

  • kevm-pyk/src/kevm_pyk/kproj/evm-semantics

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -637,13 +637,13 @@ After executing a transaction, it's necessary to have the effect of the substate
637637
</message>
638638
requires REFUND =/=Int 0
639639
640-
rule <k> #finalizeTx(false, GFLOOR) => #finalizeTx(true, GFLOOR) ... </k>
640+
rule <k> #finalizeTx(false => true, GFLOOR) ... </k>
641641
<useGas> true </useGas>
642642
<schedule> SCHED </schedule>
643643
<baseFee> BFEE </baseFee>
644644
<origin> ORG </origin>
645645
<coinbase> MINER </coinbase>
646-
<gas> GAVAIL => minInt (GAVAIL, GLIMIT -Int GFLOOR) </gas>
646+
<gas> GAVAIL </gas>
647647
<gasUsed> GUSED => GUSED +Gas maxInt(GLIMIT -Int GAVAIL, GFLOOR) </gasUsed>
648648
<blobGasUsed> BLOB_GAS_USED => #if TXTYPE ==K Blob #then BLOB_GAS_USED +Int Ctotalblob(SCHED, size(TVH)) #else BLOB_GAS_USED #fi </blobGasUsed>
649649
<gasPrice> GPRICE </gasPrice>
@@ -668,7 +668,7 @@ After executing a transaction, it's necessary to have the effect of the substate
668668
</message>
669669
requires ORG =/=Int MINER
670670
671-
rule <k> #finalizeTx(false, GFLOOR) => #finalizeTx(true, GFLOOR) ... </k>
671+
rule <k> #finalizeTx(false => true, GFLOOR) ... </k>
672672
<useGas> true </useGas>
673673
<schedule> SCHED </schedule>
674674
<baseFee> BFEE </baseFee>

0 commit comments

Comments
 (0)