Skip to content

Commit 783c8bb

Browse files
RobertorosmaninhoRobertorosmaninho
committed
Addressing comments
1 parent c30f0ae commit 783c8bb

File tree

4 files changed

+27
-60
lines changed

4 files changed

+27
-60
lines changed

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

Lines changed: 17 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -70,37 +70,6 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
7070
rule <k> startTx => #finalizeBlock ... </k>
7171
<txPending> .List </txPending>
7272
73-
rule <k> startTx => loadTx( #sender( BlobTxData(TN, TPF, TM, TG, TT, TV, DATA, CID, TA, TB, TVH), TW, TR, TS, B ) ) ... </k>
74-
<txPending> ListItem(TXID:Int) ... </txPending>
75-
<chainID> B </chainID>
76-
<message>
77-
<msgID> TXID </msgID>
78-
<txNonce> TN </txNonce>
79-
<txGasPrice> TP </txGasPrice>
80-
<txGasLimit> TG </txGasLimit>
81-
<to> TT </to>
82-
<value> TV </value>
83-
<sigV> TW </sigV>
84-
<sigR> TR </sigR>
85-
<sigS> TS </sigS>
86-
<data> DATA </data>
87-
<txChainID> CID </txChainID>
88-
<txAccess> TA </txAccess>
89-
<txPriorityFee> TPF </txPriorityFee>
90-
<txMaxFee> TM </txMaxFee>
91-
<txMaxBlobFee> TB </txMaxBlobFee>
92-
<txVersionedHashes> TVH </txVersionedHashes>
93-
<txType> Blob </txType>
94-
...
95-
</message>
96-
<evm>
97-
<callState>
98-
<versionedHashes> _ => TVH </versionedHashes>
99-
...
100-
</callState>
101-
...
102-
</evm>
103-
10473
rule <k> startTx => loadTx( #sender( #getTxData(TXID), TW, TR, TS, B ) ) ... </k>
10574
<txPending> ListItem(TXID:Int) ... </txPending>
10675
<chainID> B </chainID>
@@ -110,7 +79,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
11079
<sigR> TR </sigR>
11180
<sigS> TS </sigS>
11281
...
113-
</message> [owise]
82+
</message>
11483
11584
syntax EthereumCommand ::= loadTx ( Account ) [symbol(loadTx)]
11685
// --------------------------------------------------------------
@@ -142,14 +111,16 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
142111
<txPending> ListItem(TXID:Int) ... </txPending>
143112
<coinbase> MINER </coinbase>
144113
<message>
145-
<msgID> TXID </msgID>
146-
<txGasLimit> GLIMIT </txGasLimit>
147-
<to> .Account </to>
148-
<value> VALUE </value>
149-
<data> CODE </data>
150-
<txAccess> TA </txAccess>
114+
<msgID> TXID </msgID>
115+
<txGasLimit> GLIMIT </txGasLimit>
116+
<to> .Account </to>
117+
<value> VALUE </value>
118+
<data> CODE </data>
119+
<txAccess> TA </txAccess>
120+
<txVersionedHashes> TVH </txVersionedHashes>
151121
...
152122
</message>
123+
<versionedHashes> _ => TVH </versionedHashes>
153124
<account>
154125
<acctID> ACCTFROM </acctID>
155126
<balance> BAL => BAL -Int (GLIMIT *Int #effectiveGasPrice(TXID)) </balance>
@@ -178,14 +149,16 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
178149
<txPending> ListItem(TXID:Int) ... </txPending>
179150
<coinbase> MINER </coinbase>
180151
<message>
181-
<msgID> TXID </msgID>
182-
<txGasLimit> GLIMIT </txGasLimit>
183-
<to> ACCTTO </to>
184-
<value> VALUE </value>
185-
<data> DATA </data>
186-
<txAccess> TA </txAccess>
152+
<msgID> TXID </msgID>
153+
<txGasLimit> GLIMIT </txGasLimit>
154+
<to> ACCTTO </to>
155+
<value> VALUE </value>
156+
<data> DATA </data>
157+
<txAccess> TA </txAccess>
158+
<txVersionedHashes> TVH </txVersionedHashes>
187159
...
188160
</message>
161+
<versionedHashes> _ => TVH </versionedHashes>
189162
<account>
190163
<acctID> ACCTFROM </acctID>
191164
<balance> BAL => BAL -Int (GLIMIT *Int #effectiveGasPrice(TXID)) </balance>

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

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -73,10 +73,10 @@ In the comments next to each cell, we've marked which component of the YellowPap
7373
7474
<static> false </static>
7575
<callDepth> 0 </callDepth>
76-
77-
<versionedHashes> .List </versionedHashes>
7876
</callState>
7977
78+
<versionedHashes> .List </versionedHashes>
79+
8080
// A_* (execution substate)
8181
<substate>
8282
<selfDestruct> .Set </selfDestruct> // A_s
@@ -1074,17 +1074,11 @@ The blockhash is calculated here using the "shortcut" formula used for running t
10741074
// -------------------------------
10751075
10761076
rule <k> BLOBHASH INDEX => 0 ~> #push ... </k>
1077-
<callState>
1078-
<versionedHashes> HASHES </versionedHashes>
1079-
...
1080-
</callState>
1077+
<versionedHashes> HASHES </versionedHashes>
10811078
requires INDEX >=Int size(HASHES)
10821079
10831080
rule <k> BLOBHASH INDEX => #asWord( {HASHES[INDEX]}:>Bytes ) ~> #push ... </k>
1084-
<callState>
1085-
<versionedHashes> HASHES </versionedHashes>
1086-
...
1087-
</callState>
1081+
<versionedHashes> HASHES </versionedHashes>
10881082
requires INDEX <Int size(HASHES)
10891083
```
10901084

‎tests/failing/ContractCreationSpam_d0g0v0.json.expected

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -74,10 +74,10 @@
7474
<callDepth>
7575
-1
7676
</callDepth>
77-
<versionedHashes>
78-
.List
79-
</versionedHashes>
8077
</callState>
78+
<versionedHashes>
79+
.List
80+
</versionedHashes>
8181
<substate>
8282
<selfDestruct>
8383
.Set

‎tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -74,10 +74,10 @@
7474
<callDepth>
7575
-1
7676
</callDepth>
77-
<versionedHashes>
78-
.List
79-
</versionedHashes>
8077
</callState>
78+
<versionedHashes>
79+
.List
80+
</versionedHashes>
8181
<substate>
8282
<selfDestruct>
8383
.Set

0 commit comments

Comments
 (0)