eip-7939: implement the CLZ opcode

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

@@ -54,6 +54,14 @@ Primitives provide the basic conversion from K's sorts `Int` and `Bool` to EVM's
     rule abs(I) => 0         requires sgn(I) ==Int  0
 ```
 
+-   `clz` returns the number of leading zeros of a word, as specified in [EIP-7939](https://github.com/ethereum/EIPs/blob/31f1d01e474633119f9014765635346c06f5cc7d/EIPS/eip-7939.md).
+```k
+    syntax Int ::= clz ( Int ) [symbol(clz), function, total]
+ // ---------------------------------------------------------
+    rule clz(0) => 256
+    rule clz(I) => 255 -Int log2Int(I) requires 0 <Int I andBool I <Int pow256
+    rule clz(I) => -1                  requires I <Int 0 orBool pow256 <=Int I
+```
 Word Operations
 ---------------
 

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

@@ -1246,6 +1246,10 @@ NOTE: We have to call the opcode `OR` by `EVMOR` instead, because K has trouble
  // ----------------------------
     rule <k> SHA3 MEMSTART MEMWIDTH => keccak(#range(LM, MEMSTART, MEMWIDTH)) ~> #push ... </k>
          <localMem> LM </localMem>
+
+    syntax UnStackOp ::= "CLZ"
+ // -------------------------
+    rule <k> CLZ X => clz(X) ~> #push ... </k>
 ```
 
 ### Local State
@@ -3000,6 +3004,7 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H).
     rule <k> #gasExec(SCHED, SMOD _ _)       => Glow < SCHED > ... </k>
     rule <k> #gasExec(SCHED, SIGNEXTEND _ _) => Glow < SCHED > ... </k>
     rule <k> #gasExec(SCHED, SELFBALANCE)    => Glow < SCHED > ... </k>
+    rule <k> #gasExec(SCHED, CLZ _)          => Glow < SCHED > ... </k>
 
     // Wmid
     rule <k> #gasExec(SCHED, ADDMOD _ _ _) => Gmid < SCHED > ... </k>
@@ -3217,6 +3222,7 @@ After interpreting the strings representing programs as a `WordStack`, it should
     rule #dasmOpCode(  27, SCHED ) => SHL requires Ghasshift << SCHED >>
     rule #dasmOpCode(  28, SCHED ) => SHR requires Ghasshift << SCHED >>
     rule #dasmOpCode(  29, SCHED ) => SAR requires Ghasshift << SCHED >>
+    rule #dasmOpCode(  30, SCHED ) => CLZ requires Ghasclz << SCHED >>
     rule #dasmOpCode(  32,     _ ) => SHA3
     rule #dasmOpCode(  48,     _ ) => ADDRESS
     rule #dasmOpCode(  49,     _ ) => BALANCE

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

@@ -31,8 +31,8 @@ module SCHEDULE
                           | "Ghaswarmcoinbase"        | "Ghaswithdrawals"  | "Ghastransient"       | "Ghasmcopy"
                           | "Ghasbeaconroot"          | "Ghaseip6780"      | "Ghasblobbasefee"     | "Ghasblobhash"
                           | "Ghasbls12msmdiscount"    | "Ghashistory"      | "Ghasrequests"        | "Ghasauthority"
-                          | "Ghasfloorcost"
- // ---------------------------------------
+                          | "Ghasfloorcost"           | "Ghasclz"
+ // -------------------------------------------------------------
 ```
 
 ### Schedule Constants
@@ -182,6 +182,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule [Ghasbls12msmdiscountDefault]:    Ghasbls12msmdiscount    << DEFAULT >> => false
     rule [GhasauthorityDefault]:           Ghasauthority           << DEFAULT >> => false
     rule [GhasfloorcostDefault]:           Ghasfloorcost           << DEFAULT >> => false
+    rule [GhasclzDefault]:                 Ghasclz                 << DEFAULT >> => false
 ```
 
 ### Frontier Schedule
@@ -504,7 +505,11 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     syntax Schedule ::= "OSAKA" [symbol(OSAKA_EVM), smtlib(schedule_OSAKA)]
  // -----------------------------------------------------------------------
     rule [SCHEDCONSTOsaka]: SCHEDCONST < OSAKA > => SCHEDCONST < PRAGUE >
+
+    rule [GhasclzOsaka]:    Ghasclz    << OSAKA >> => true
     rule [SCHEDFLAGOsaka]:  SCHEDFLAG  << OSAKA >> => SCHEDFLAG << PRAGUE >>
+      requires notBool ( SCHEDFLAG ==K Ghasclz )
+
 ```
 
 ```k