Skip to content

Commit e039ead

Browse files
rv-auditorrv-auditor
committed
Merge remote-tracking branch 'origin/master' into release
2 parents b16492e + 5a72ed6 commit e039ead

File tree

5 files changed

+42
-170
lines changed

5 files changed

+42
-170
lines changed

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

Lines changed: 6 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -66,8 +66,8 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
6666
6767
syntax EthereumCommand ::= "flush"
6868
// ----------------------------------
69-
rule <mode> EXECMODE </mode> <statusCode> EVMC_SUCCESS </statusCode> <k> #halt ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ... </k>
70-
rule <mode> EXECMODE </mode> <statusCode> _:ExceptionalStatusCode </statusCode> <k> #halt ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ~> #halt ... </k>
69+
rule <mode> EXECMODE </mode> <statusCode> EVMC_SUCCESS </statusCode> <k> #halt ~> flush => #finalizeTx(EXECMODE ==K VMTESTS, 0) ... </k>
70+
rule <mode> EXECMODE </mode> <statusCode> _:ExceptionalStatusCode </statusCode> <k> #halt ~> flush => #finalizeTx(EXECMODE ==K VMTESTS, 0) ~> #halt ... </k>
7171
```
7272

7373
- `startTx` computes the sender of the transaction, and places loadTx on the `k` cell.
@@ -116,25 +116,13 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
116116
117117
syntax EthereumCommand ::= loadTx ( Account ) [symbol(loadTx)]
118118
// --------------------------------------------------------------
119-
rule <k> loadTx(_) => startTx ... </k>
120-
<statusCode> _ => EVMC_OUT_OF_GAS </statusCode>
121-
<txPending> ListItem(TXID:Int) REST => REST </txPending>
122-
<schedule> SCHED </schedule>
123-
<message>
124-
<msgID> TXID </msgID>
125-
<to> .Account </to>
126-
<data> CODE </data>
127-
...
128-
</message>
129-
requires notBool #hasValidInitCode(lengthBytes(CODE), SCHED)
130-
131119
rule <k> loadTx(ACCTFROM)
132120
=> #accessAccounts ACCTFROM #newAddr(ACCTFROM, NONCE) #precompiledAccountsSet(SCHED)
133121
~> #deductBlobGas
134122
~> #loadAccessList(TA)
135123
~> #checkCreate ACCTFROM VALUE
136124
~> #create ACCTFROM #newAddr(ACCTFROM, NONCE) VALUE CODE
137-
~> #finishTx ~> #finalizeTx(false) ~> startTx
125+
~> #finishTx ~> #finalizeTx(false, Ctxfloor(SCHED, CODE)) ~> startTx
138126
...
139127
</k>
140128
<schedule> SCHED </schedule>
@@ -163,15 +151,15 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
163151
<touchedAccounts> _ => SetItem(MINER) </touchedAccounts>
164152
requires #hasValidInitCode(lengthBytes(CODE), SCHED)
165153
andBool #isValidTransaction(TXID, ACCTFROM)
166-
154+
andBool GLIMIT >=Int maxInt(G0(SCHED, CODE, true), Ctxfloor(SCHED, CODE))
167155
168156
rule <k> loadTx(ACCTFROM)
169157
=> #accessAccounts ACCTFROM ACCTTO #precompiledAccountsSet(SCHED)
170158
~> #deductBlobGas
171159
~> #loadAccessList(TA)
172160
~> #checkCall ACCTFROM VALUE
173161
~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE DATA false
174-
~> #finishTx ~> #finalizeTx(false) ~> startTx
162+
~> #finishTx ~> #finalizeTx(false, Ctxfloor(SCHED, DATA)) ~> startTx
175163
...
176164
</k>
177165
<schedule> SCHED </schedule>
@@ -202,16 +190,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
202190
<touchedAccounts> _ => SetItem(MINER) </touchedAccounts>
203191
requires ACCTTO =/=K .Account
204192
andBool #isValidTransaction(TXID, ACCTFROM)
205-
206-
rule <k> loadTx(ACCTFROM) => startTx ... </k>
207-
<statusCode> _ => EVMC_INVALID_BLOCK </statusCode>
208-
<txPending> ListItem(_TXID:Int) REST => REST </txPending>
209-
<account>
210-
<acctID> ACCTFROM </acctID>
211-
<code> ACCTCODE </code>
212-
...
213-
</account>
214-
requires notBool ACCTCODE ==K .Bytes
193+
andBool GLIMIT >=Int maxInt(G0(SCHED, DATA, false), Ctxfloor(SCHED, DATA))
215194
216195
rule <k> loadTx(_) => startTx ... </k>
217196
<statusCode> _ => EVMC_OUT_OF_GAS </statusCode>

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

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -613,18 +613,18 @@ After executing a transaction, it's necessary to have the effect of the substate
613613
614614
rule <k> (.K => #newAccount ACCT) ~> #finalizeStorage(ListItem(ACCT) _ACCTS) ... </k> [owise]
615615
616-
syntax InternalOp ::= #finalizeTx ( Bool ) [symbol(#finalizeTx)]
616+
syntax InternalOp ::= #finalizeTx ( Bool , Int ) [symbol(#finalizeTx)]
617617
| #deleteAccounts ( List ) [symbol(#deleteAccounts)]
618618
// ------------------------------------------------------------------------
619-
rule <k> #finalizeTx(true) => #finalizeStorage(Set2List(SetItem(MINER) |Set ACCTS)) ... </k>
619+
rule <k> #finalizeTx(true, _) => #finalizeStorage(Set2List(SetItem(MINER) |Set ACCTS)) ... </k>
620620
<selfDestruct> .Set </selfDestruct>
621621
<coinbase> MINER </coinbase>
622622
<touchedAccounts> ACCTS => .Set </touchedAccounts>
623623
<accessedAccounts> _ => .Set </accessedAccounts>
624624
<accessedStorage> _ => .Map </accessedStorage>
625625
<createdAccounts> _ => .Set </createdAccounts>
626626
627-
rule <k> #finalizeTx(false) ... </k>
627+
rule <k> #finalizeTx(false, _) ... </k>
628628
<useGas> true </useGas>
629629
<schedule> SCHED </schedule>
630630
<gas> GAVAIL => G*(GAVAIL, GLIMIT, REFUND, SCHED) </gas>
@@ -637,25 +637,25 @@ 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 => true) ... </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>
646646
<gas> GAVAIL </gas>
647-
<gasUsed> GUSED => GUSED +Gas GLIMIT -Gas GAVAIL </gasUsed>
647+
<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>
650650
<refund> 0 </refund>
651651
<account>
652652
<acctID> ORG </acctID>
653-
<balance> ORGBAL => ORGBAL +Int GAVAIL *Int GPRICE </balance>
653+
<balance> ORGBAL => ORGBAL +Int minInt(GAVAIL, GLIMIT -Int GFLOOR) *Int GPRICE </balance>
654654
...
655655
</account>
656656
<account>
657657
<acctID> MINER </acctID>
658-
<balance> MINBAL => MINBAL +Int (GLIMIT -Int GAVAIL) *Int (GPRICE -Int BFEE) </balance>
658+
<balance> MINBAL => MINBAL +Int maxInt(GLIMIT -Int GAVAIL, GFLOOR) *Int (GPRICE -Int BFEE) </balance>
659659
...
660660
</account>
661661
<txPending> ListItem(MSGID:Int) REST => REST </txPending>
@@ -668,20 +668,20 @@ 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 => true) ... </k>
671+
rule <k> #finalizeTx(false => true, GFLOOR) ... </k>
672672
<useGas> true </useGas>
673673
<schedule> SCHED </schedule>
674674
<baseFee> BFEE </baseFee>
675675
<origin> ACCT </origin>
676676
<coinbase> ACCT </coinbase>
677677
<gas> GAVAIL </gas>
678-
<gasUsed> GUSED => GUSED +Gas GLIMIT -Gas GAVAIL </gasUsed>
678+
<gasUsed> GUSED => GUSED +Gas maxInt(GLIMIT -Int GAVAIL, GFLOOR) </gasUsed>
679679
<blobGasUsed> BLOB_GAS_USED => #if TXTYPE ==K Blob #then BLOB_GAS_USED +Int Ctotalblob(SCHED, size(TVH)) #else BLOB_GAS_USED #fi </blobGasUsed>
680680
<gasPrice> GPRICE </gasPrice>
681681
<refund> 0 </refund>
682682
<account>
683683
<acctID> ACCT </acctID>
684-
<balance> BAL => BAL +Int GLIMIT *Int GPRICE -Int (GLIMIT -Int GAVAIL) *Int BFEE </balance>
684+
<balance> BAL => BAL +Int GLIMIT *Int GPRICE -Int maxInt(GLIMIT -Int GAVAIL, GFLOOR) *Int BFEE </balance>
685685
...
686686
</account>
687687
<txPending> ListItem(MSGID:Int) REST => REST </txPending>
@@ -693,19 +693,19 @@ After executing a transaction, it's necessary to have the effect of the substate
693693
...
694694
</message>
695695
696-
rule <k> #finalizeTx(false => true) ... </k>
696+
rule <k> #finalizeTx(false => true, _) ... </k>
697697
<useGas> false </useGas>
698698
<txPending> ListItem(MSGID:Int) REST => REST </txPending>
699699
<message>
700700
<msgID> MSGID </msgID>
701701
...
702702
</message>
703703
704-
rule <k> (.K => #deleteAccounts(Set2List(ACCTS))) ~> #finalizeTx(true) ... </k>
704+
rule <k> (.K => #deleteAccounts(Set2List(ACCTS))) ~> #finalizeTx(true,_) ... </k>
705705
<selfDestruct> ACCTS => .Set </selfDestruct>
706706
requires size(ACCTS) >Int 0
707707
708-
rule <k> (.K => #newAccount MINER) ~> #finalizeTx(_) ... </k>
708+
rule <k> (.K => #newAccount MINER) ~> #finalizeTx(_,_) ... </k>
709709
<coinbase> MINER </coinbase> [owise]
710710
711711
rule <k> #deleteAccounts(ListItem(ACCT) ACCTS) => #deleteAccounts(ACCTS) ... </k>

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -125,6 +125,7 @@ module GAS-FEES
125125
| Cbasefeeperblob( Schedule , Int ) [symbol(Cbasefeeperblob),function, total, smtlib(gas_Cbasefeeperblob) ]
126126
| Cblobfee ( Schedule , Int , Int ) [symbol(Cblobfee), function, total, smtlib(gas_Cblobfee) ]
127127
| Cexcessblob ( Schedule , Int , Int ) [symbol(Cexcessblob), function, total, smtlib(gas_Cexcessblob) ]
128+
| Ctxfloor ( Schedule , Bytes ) [symbol(Ctxfloor), function, total, smtlib(gas_Ctxfloor) ]
128129
// ------------------------------------------------------------------------------------------------------------------------------------------
129130
rule [Cgascap]:
130131
Cgascap(SCHED, GCAP:Int, GAVAIL:Int, GEXTRA)
@@ -271,6 +272,16 @@ module GAS-FEES
271272
rule #adjustedExpLength(1) => 0
272273
rule #adjustedExpLength(N) => 1 +Int #adjustedExpLength(N /Int 2) requires N >Int 1
273274
275+
syntax Int ::= #tokensInCalldata( Bytes ) [symbol(#tokensInCalldata), function]
276+
| #tokensInCalldata( Bytes , Int , Int , Int ) [symbol(#tokensInCalldataAux), function]
277+
// ----------------------------------------------------------------------------------------------------
278+
rule #tokensInCalldata(WS) => #tokensInCalldata(WS, 0, lengthBytes(WS), 0)
279+
rule #tokensInCalldata(_, I, I, R) => R
280+
rule #tokensInCalldata(WS, I, J, R) => #tokensInCalldata(WS, I+Int 1, J, R +Int #if WS[I] ==Int 0 #then 1 #else 4 #fi) [owise]
281+
282+
rule Ctxfloor(SCHED, CODE) => Gtransaction < SCHED > +Int (Gtxdatafloor < SCHED > *Int #tokensInCalldata(CODE)) requires Ghasfloorcost << SCHED >>
283+
rule Ctxfloor( _, _) => 0 [owise]
284+
274285
syntax Int ::= Cbls12g1MsmDiscount( Schedule , Int ) [symbol(Cbls12g1MsmDiscount), function, total, smtlib(gas_Cbls12g1MsmDiscount)]
275286
| Cbls12g2MsmDiscount( Schedule , Int ) [symbol(Cbls12g2MsmDiscount), function, total, smtlib(gas_Cbls12g2MsmDiscount)]
276287
// ------------------------------------------------------------------------------------------------------------------------------------

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

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,8 @@ module SCHEDULE
3030
| "Ghasrejectedfirstbyte" | "Ghasprevrandao" | "Ghasmaxinitcodesize" | "Ghaspushzero"
3131
| "Ghaswarmcoinbase" | "Ghaswithdrawals" | "Ghastransient" | "Ghasmcopy"
3232
| "Ghasbeaconroot" | "Ghaseip6780" | "Ghasblobbasefee" | "Ghasblobhash"
33-
| "Ghasbls12msmdiscount" | "Ghashistory" | "Ghasrequests"
34-
// -----------------------------------------------------------------
33+
| "Ghasrequests" | "Ghashistory" | "Ghasfloorcost" | "Ghasbls12msmdiscount"
34+
// -----------------------------------------------------------------------------------------------------------------------
3535
```
3636

3737
### Schedule Constants
@@ -52,7 +52,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
5252
| "Gaccessliststoragekey" | "Rmaxquotient" | "Ginitcodewordcost" | "maxInitCodeSize" | "Gwarmstoragedirtystore"
5353
| "Gpointeval" | "Gmaxblobgas" | "Gminbasefee" | "Gtargetblobgas" | "Gperblob" | "Blobbasefeeupdatefraction"
5454
| "Gbls12g1add" | "Gbls12g1mul" | "Gbls12g2add" | "Gbls12g2mul" | "Gbls12mapfptog1" | "Gbls12PairingCheckMul"
55-
| "Gbls12PairingCheckAdd" | "Gbls12mapfp2tog2"
55+
| "Gbls12PairingCheckAdd" | "Gtxdatafloor" | "Gbls12mapfp2tog2"
5656
// -------------------------------------------------------------------------------------------------------------------------------------------------------
5757
```
5858

@@ -101,6 +101,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
101101
rule [GtxcreateDefault]: Gtxcreate < DEFAULT > => 53000
102102
rule [GtxdatazeroDefault]: Gtxdatazero < DEFAULT > => 4
103103
rule [GtxdatanonzeroDefault]: Gtxdatanonzero < DEFAULT > => 68
104+
rule [GtxdatafloorDefault]: Gtxdatafloor < DEFAULT > => 0
104105
105106
rule [GjumpdestDefault]: Gjumpdest < DEFAULT > => 1
106107
rule [GbalanceDefault]: Gbalance < DEFAULT > => 20
@@ -177,6 +178,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
177178
rule [GhashistoryDefault]: Ghashistory << DEFAULT >> => false
178179
rule [GhasrequestsDefault]: Ghasrequests << DEFAULT >> => false
179180
rule [Ghasbls12msmdiscountDefault]: Ghasbls12msmdiscount << DEFAULT >> => false
181+
rule [GhasfloorcostDefault]: Ghasfloorcost << DEFAULT >> => false
180182
```
181183

182184
### Frontier Schedule
@@ -463,6 +465,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
463465
rule [Gbls12PairingCheckAddPrague]: Gbls12PairingCheckAdd < PRAGUE > => 37700
464466
rule [Gbls12mapfptog1Prague]: Gbls12mapfptog1 < PRAGUE > => 5500
465467
rule [Gbls12mapfp2tog2Prague]: Gbls12mapfp2tog2 < PRAGUE > => 23800
468+
rule [GtxdatafloorPrague]: Gtxdatafloor < PRAGUE > => 10
466469
rule [SCHEDCONSTPrague]: SCHEDCONST < PRAGUE > => SCHEDCONST < CANCUN >
467470
requires notBool ( SCHEDCONST ==K Gmaxblobgas
468471
orBool SCHEDCONST ==K Gtargetblobgas
@@ -474,15 +477,18 @@ A `ScheduleConst` is a constant determined by the fee schedule.
474477
orBool SCHEDCONST ==K Gbls12PairingCheckMul
475478
orBool SCHEDCONST ==K Gbls12PairingCheckAdd
476479
orBool SCHEDCONST ==K Gbls12mapfptog1
477-
orBool SCHEDCONST ==K Gbls12mapfp2tog2 )
480+
orBool SCHEDCONST ==K Gbls12mapfp2tog2
481+
orBool SCHEDCONST ==K Gtxdatafloor )
478482
479483
rule [GhasrequestsPrague]: Ghasrequests << PRAGUE >> => true
480484
rule [GhashistoryPrague]: Ghashistory << PRAGUE >> => true
481485
rule [Ghasbls12msmdiscountPrague]: Ghasbls12msmdiscount << PRAGUE >> => true
486+
rule [GhasfloorcostPrague]: Ghasfloorcost << PRAGUE >> => true
482487
rule [SCHEDFLAGPrague]: SCHEDFLAG << PRAGUE >> => SCHEDFLAG << CANCUN >>
483488
requires notBool ( SCHEDFLAG ==K Ghasrequests
484489
orBool SCHEDFLAG ==K Ghashistory
485-
orBool SCHEDFLAG ==K Ghasbls12msmdiscount )
490+
orBool SCHEDFLAG ==K Ghasbls12msmdiscount
491+
orBool SCHEDFLAG ==K Ghasfloorcost )
486492
```
487493

488494
```k

0 commit comments

Comments
 (0)