Support of OPCODE BLOBBASEFEE , BLOBHASH and CLZ

BUILDING.md

@@ -0,0 +1 @@
+pip install -e ".[dev]"

src/halmos/bitvec.py

@@ -1,3 +1,4 @@
+
 # SPDX-License-Identifier: AGPL-3.0
 
 from typing import Any, TypeAlias
@@ -843,6 +844,51 @@ def ashr(self, shift: BV) -> "HalmosBitVec":
 
         return HalmosBitVec(self.as_z3() >> shift.value, size=self.size)
 
+    def clz(self) -> "HalmosBitVec":
+        """
+        Count Leading Zeros — EVM opcode CLZ (0x1E, EIP-7939 / Fusaka).
+
+        Stack semantics: [x] -> [clz(x)]
+          clz(0)      == size  (256 for a standard EVM word)
+          clz(1)      == 255
+          clz(2^255)  == 0
+
+        Concrete: O(1) via int.bit_length().
+        Symbolic: binary-search tree of 8 nested If() nodes (one per
+        bit-doubling level: 128/64/32/16/8/4/2/1), O(log n) Z3 terms.
+
+        Algorithm: at each level `shift`, inspect the top `shift` bits of cur.
+          - If zero: add `shift` to acc, slide window left to expose next band.
+          - If nonzero: isolate this band for the next level.
+        """
+        size = self._size  # 256 in standard EVM context
+
+        # --- concrete fast path ---
+        if self.is_concrete:
+            v = self._value
+            return HalmosBitVec(size if v == 0 else size - v.bit_length(), size=size)
+
+        # --- symbolic path: binary search over bit-levels ---
+        x = self.as_z3()
+        zero = BitVecVal(0, size)
+
+        acc = zero
+        cur = x
+
+        for shift in (128, 64, 32, 16, 8, 4, 2, 1):
+            top_bits = LShR(cur, BitVecVal(size - shift, size))
+            top_zero = top_bits == zero
+            acc = If(top_zero, acc + BitVecVal(shift, size), acc)
+            cur = If(
+                top_zero,
+                cur << BitVecVal(shift, size),              # expose next band at MSB
+                top_bits << BitVecVal(size - shift, size),  # keep current band aligned
+            )
+
+        # x == 0 -> every bit is a leading zero, result is `size`.
+        result = If(x == zero, BitVecVal(size, size), acc)
+        return HalmosBitVec(result, size=size)
+
     def bitwise_not(self) -> BV:
         if self.is_concrete:
             return HalmosBitVec(~self._value & ((1 << self._size) - 1), size=self._size)
@@ -961,4 +1007,4 @@ def byte(self, idx: int, *, output_size: int = 8) -> BV:
 FALSE.sym_val = None
 
 ZERO = HalmosBitVec(0, size=256)
-ONE = HalmosBitVec(1, size=256)
+ONE = HalmosBitVec(1, size=256)

src/halmos/contract.py

@@ -1,3 +1,4 @@
+
 # SPDX-License-Identifier: AGPL-3.0
 
 from collections import defaultdict
@@ -54,6 +55,7 @@
 OP_SHL = 0x1B
 OP_SHR = 0x1C
 OP_SAR = 0x1D
+OP_CLZ = 0x1E
 OP_SHA3 = 0x20
 OP_ADDRESS = 0x30
 OP_BALANCE = 0x31
@@ -80,6 +82,8 @@
 OP_CHAINID = 0x46
 OP_SELFBALANCE = 0x47
 OP_BASEFEE = 0x48
+OP_BLOBHASH = 0x49
+OP_BLOBBASEFEE = 0x4A
 OP_POP = 0x50
 OP_MLOAD = 0x51
 OP_MSTORE = 0x52
@@ -536,4 +540,4 @@ def generate_lcov_report(self) -> str:
             # End of file
             lcov_lines.append("end_of_record")
 
-        return "\n".join(lcov_lines)
+        return "\n".join(lcov_lines)

src/halmos/sevm.py

@@ -1,3 +1,4 @@
+
 # SPDX-License-Identifier: AGPL-3.0
 
 import itertools
@@ -29,6 +30,7 @@
     ArrayRef,
     BitVec,
     BitVecRef,
+    BitVecVal,
     BoolRef,
     BoolVal,
     CheckSatResult,
@@ -71,6 +73,8 @@
     OP_AND,
     OP_BALANCE,
     OP_BASEFEE,
+    OP_BLOBHASH,
+    OP_BLOBBASEFEE,
     OP_BLOCKHASH,
     OP_BYTE,
     OP_CALL,
@@ -130,6 +134,7 @@
     OP_RETURNDATASIZE,
     OP_REVERT,
     OP_SAR,
+    OP_CLZ,
     OP_SDIV,
     OP_SELFBALANCE,
     OP_SGT,
@@ -710,6 +715,8 @@ class Block:
     gaslimit: BitVecRef
     number: BitVecRef
     timestamp: BitVecRef
+    blobbasefee: BitVecRef  # EIP-4844 / Cancun — opcode 0x4A
+    blobhashes: list        # EIP-4844 / Cancun — opcode 0x49, list of BitVecRef (256-bit)
 
     def __init__(self, **kwargs) -> None:
         self.basefee = kwargs["basefee"]
@@ -719,6 +726,8 @@ def __init__(self, **kwargs) -> None:
         self.gaslimit = kwargs["gaslimit"]
         self.number = kwargs["number"]
         self.timestamp = kwargs["timestamp"]
+        self.blobbasefee = kwargs.get("blobbasefee", ZERO)  # 0 par défaut
+        self.blobhashes = kwargs.get("blobhashes", [])      # pas de blobs par défaut
 
         assert_address(self.coinbase)
 
@@ -3531,6 +3540,30 @@ def finalize(ex: Exec):
                 elif opcode == OP_BASEFEE:
                     state.push_any(ex.block.basefee)
 
+                elif opcode == OP_BLOBBASEFEE:
+                    # EIP-4844 / Cancun (0x4A): blob base fee du bloc courant.
+                    state.push_any(ex.block.blobbasefee)
+
+                elif opcode == OP_BLOBHASH:
+                    # EIP-4844 / Cancun (0x49): versioned hash du blob a l'index i.
+                    # L'index peut etre symbolique : on construit un If-tree sur la
+                    # liste des blobs. Retourne 0 si hors range ou liste vide.
+                    index = state.popi()
+                    blobhashes = ex.block.blobhashes
+                    if not blobhashes:
+                        # Pas de blobs dans cette tx -> toujours 0
+                        state.push_any(ZERO)
+                    else:
+                        # Construire: If(i==0, h0, If(i==1, h1, ..., 0))
+                        result = ZERO
+                        for i in range(len(blobhashes) - 1, -1, -1):
+                            result = If(
+                                index.as_z3() == BitVecVal(i, 256),
+                                blobhashes[i],
+                                result,
+                            )
+                        state.push_any(result)
+
                 elif opcode == OP_PC:
                     state.push_any(ex.pc)
 
@@ -3578,6 +3611,11 @@ def finalize(ex: Exec):
                     w2 = state.popi()
                     state.push(w2.ashr(w1))  # bvashr
 
+                elif opcode == OP_CLZ:
+                    # EIP-7939 / Fusaka (0x1E): count leading zeros.
+                    w1 = state.popi()
+                    state.push(w1.clz())
+
                 elif opcode == OP_ADDMOD:
                     w1 = state.popi()
                     w2 = state.popi()
@@ -3706,4 +3744,4 @@ def get_top_instructions(self, n: int = 20) -> list[tuple[str, int]]:
         return [(key, count) for key, count in self.counters.most_common(n)]
 
     def reset(self) -> None:
-        raise NotImplementedError("Resetting the profiler is not supported")
+        raise NotImplementedError("Resetting the profiler is not supported")

src/halmos/utils.py

@@ -1,3 +1,4 @@
+
 # SPDX-License-Identifier: AGPL-3.0
 
 from __future__ import annotations
@@ -691,6 +692,7 @@ class EVM:
     SHL = 0x1B
     SHR = 0x1C
     SAR = 0x1D
+    CLZ = 0x1E
     SHA3 = 0x20
     ADDRESS = 0x30
     BALANCE = 0x31
@@ -717,6 +719,8 @@ class EVM:
     CHAINID = 0x46
     SELFBALANCE = 0x47
     BASEFEE = 0x48
+    BLOBHASH = 0x49
+    BLOBBASEFEE = 0x4A
     POP = 0x50
     MLOAD = 0x51
     MSTORE = 0x52
@@ -841,6 +845,7 @@ class EVM:
     EVM.SHL: "SHL",
     EVM.SHR: "SHR",
     EVM.SAR: "SAR",
+    EVM.CLZ: "CLZ",
     EVM.SHA3: "SHA3",
     EVM.ADDRESS: "ADDRESS",
     EVM.BALANCE: "BALANCE",
@@ -867,6 +872,8 @@ class EVM:
     EVM.CHAINID: "CHAINID",
     EVM.SELFBALANCE: "SELFBALANCE",
     EVM.BASEFEE: "BASEFEE",
+    EVM.BLOBHASH: "BLOBHASH",
+    EVM.BLOBBASEFEE: "BLOBBASEFEE",
     EVM.POP: "POP",
     EVM.MCOPY: "MCOPY",
     EVM.MLOAD: "MLOAD",
@@ -1714,4 +1721,4 @@ def wrapper(*args, **kwargs):
     0xF1AFE04D: "removeFile(string)",
     0x897E0A97: "writeFile(string,string)",
     0x619D897F: "writeLine(string,string)",
-}
+}