@@ -835,7 +835,7 @@ Terminates validation successfully when all conditions are met or when blob vali
835
835
``` k
836
836
syntax EthereumCommand ::= "#startBlock"
837
837
// ----------------------------------------
838
- rule <k> #startBlock => #validateBlockBlobs 0 TXS ~> #executeBeaconRoots ... </k>
838
+ rule <k> #startBlock => #validateBlockBlobs 0 TXS ~> #executeBeaconRoots ~> #executeBlockHashHistory ... </k>
839
839
<gasUsed> _ => 0 </gasUsed>
840
840
<blobGasUsed> _ => 0 </blobGasUsed>
841
841
<log> _ => .List </log>
@@ -939,6 +939,30 @@ Read more about EIP-4788 here [https://eips.ethereum.org/EIPS/eip-4788](https://
939
939
rule <k> #executeBeaconRoots => .K ... </k> [owise]
940
940
```
941
941
942
+ If ` block.timestamp >= PRAGUE_FORK_TIMESTAMP ` :
943
+ Before executing any transaction, the ` HISTORY_STORAGE_ADDRESS ` (` 0x0000F90827F1C53a10cb7A02335B175320002935 ` ) storage is modified as following:
944
+ - Set the storage value at ` (block.number-1) % HISTORY_SERVE_WINDOW ` to be ` block.parent.hash `
945
+ where ` HISTORY_SERVE_WINDOW == 8191 ` .
946
+
947
+ Read more about EIP-2935 here [ https://eips.ethereum.org/EIPS/eip-2935 ] ( https://eips.ethereum.org/EIPS/eip-2935 ) .
948
+
949
+ ``` k
950
+ syntax EthereumCommand ::= "#executeBlockHashHistory" [symbol(#executeBlockHashHistory)]
951
+ // ----------------------------------------------------------------------------------------
952
+ rule <k> #executeBlockHashHistory => .K ... </k>
953
+ <schedule> SCHED </schedule>
954
+ <previousHash> HP </previousHash>
955
+ <number> BN </number>
956
+ <account>
957
+ <acctID> 21693734551179282564423033930679318143314229 </acctID>
958
+ <storage> M:Map => M [((BN -Int 1) modInt 8191) <- HP] </storage>
959
+ ...
960
+ </account>
961
+ requires Ghashistory << SCHED >>
962
+
963
+ rule <k> #executeBlockHashHistory => .K ... </k> [owise]
964
+ ```
965
+
942
966
EVM Programs
943
967
============
944
968
0 commit comments