diff --git a/BUILDING.md b/BUILDING.md new file mode 100644 index 00000000..0021730f --- /dev/null +++ b/BUILDING.md @@ -0,0 +1 @@ +pip install -e ".[dev]" diff --git a/src/halmos/bitvec.py b/src/halmos/bitvec.py index e1d6ac3b..4856e331 100644 --- a/src/halmos/bitvec.py +++ b/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) \ No newline at end of file diff --git a/src/halmos/contract.py b/src/halmos/contract.py index 560c22ee..0146e216 100644 --- a/src/halmos/contract.py +++ b/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) \ No newline at end of file diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 3d2ead17..707f837f 100644 --- a/src/halmos/sevm.py +++ b/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") \ No newline at end of file diff --git a/src/halmos/utils.py b/src/halmos/utils.py index b2b21278..63691f90 100644 --- a/src/halmos/utils.py +++ b/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)", -} +} \ No newline at end of file