EIP-2935: Serve historical block hashes from state

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

@@ -771,7 +771,7 @@ After executing a transaction, it's necessary to have the effect of the substate
 ```k
     syntax EthereumCommand ::= "#startBlock"
  // ----------------------------------------
-    rule <k> #startBlock => #executeBeaconRoots ... </k>
+    rule <k> #startBlock => #executeBeaconRoots ~> #executeBlockHashHistory ... </k>
          <gasUsed> _ => 0 </gasUsed>
          <log> _ => .List </log>
          <logsBloom> _ => #padToWidth(256, .Bytes) </logsBloom>
@@ -867,6 +867,30 @@ Read more about EIP-4788 here [https://eips.ethereum.org/EIPS/eip-4788](https://
     rule <k> #executeBeaconRoots => .K ... </k> [owise]
 ```
 
+If `block.timestamp >= PRAGUE_FORK_TIMESTAMP`:
+Before executing any transaction, the `HISTORY_STORAGE_ADDRESS` (`0x0000F90827F1C53a10cb7A02335B175320002935`) storage is modified as following:
+ - Set the storage value at `(block.number-1) % HISTORY_SERVE_WINDOW` to be ` block.parent.hash`
+where `HISTORY_SERVE_WINDOW == 8191`.
+
+Read more about EIP-4788 here [https://eips.ethereum.org/EIPS/eip-2935](https://eips.ethereum.org/EIPS/eip-42935).
+
+```k
+    syntax EthereumCommand ::= "#executeBlockHashHistory" [symbol(#executeBlockHashHistory)]
+ // ----------------------------------------------------------------------------------------
+    rule <k> #executeBlockHashHistory => .K ... </k>
+         <schedule> SCHED </schedule>
+         <previousHash> HP </previousHash>
+         <number> BN </number>
+         <account>
+           <acctID> 21693734551179282564423033930679318143314229 </acctID>
+           <storage> M:Map => M [((BN -Int 1) modInt 8191) <- HP] </storage>
+           ...
+         </account>
+      requires Ghashistory << SCHED >>
+
+    rule <k> #executeBlockHashHistory => .K ... </k> [owise]
+```
+
 EVM Programs
 ============
 

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

@@ -30,6 +30,7 @@ module SCHEDULE
                           | "Ghasrejectedfirstbyte"   | "Ghasprevrandao"   | "Ghasmaxinitcodesize" | "Ghaspushzero"
                           | "Ghaswarmcoinbase"        | "Ghaswithdrawals"  | "Ghastransient"       | "Ghasmcopy"
                           | "Ghasbeaconroot"          | "Ghaseip6780"      | "Ghasblobbasefee"     | "Ghasblobhash"
+                          | "Ghashistory"
 ```
 
 ### Schedule Constants
@@ -156,6 +157,8 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule [GhasbeaconrootDefault]:          Ghasbeaconroot          << DEFAULT >> => false
     rule [Ghaseip6780Default]:             Ghaseip6780             << DEFAULT >> => false
     rule [GhasblobhashDefault]:            Ghasblobhash            << DEFAULT >> => false
+    rule [GhashistoryDefault]:             Ghashistory             << DEFAULT >> => false
+
 ```
 
 ### Frontier Schedule
@@ -423,8 +426,9 @@ A `ScheduleConst` is a constant determined by the fee schedule.
  // --------------------------------------------------------------------------
     rule [SCHEDCONSTPrague]: SCHEDCONST < PRAGUE > => SCHEDCONST < CANCUN >
 
-    rule [SCHEDFLAGPrague]: SCHEDFLAG  << PRAGUE >> => SCHEDFLAG << CANCUN >>
-
+    rule [GhashistoryPrague]:  Ghashistory << PRAGUE >> => true
+    rule [SCHEDFLAGPrague]:    SCHEDFLAG   << PRAGUE >> => SCHEDFLAG << CANCUN >>
+      requires (notBool SCHEDFLAG ==K Ghashistory)
 ```
 
 ```k