From dc1ea8a07d1ec61d53d9d462d7eb4f6a4624e90c Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 12 Aug 2026 13:11:19 -0300 Subject: [PATCH 1/2] Use unsigned ULE for the keccak gate's byte-range contract and remove dead code --- formal_verification/keccak/keccak_ref.py | 3 +-- formal_verification/keccak/z3_parallel.py | 3 --- formal_verification/keccak/z3_verify.py | 22 +++++++++++++--------- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/formal_verification/keccak/keccak_ref.py b/formal_verification/keccak/keccak_ref.py index 0c5ab61a3..5efeb84b4 100644 --- a/formal_verification/keccak/keccak_ref.py +++ b/formal_verification/keccak/keccak_ref.py @@ -44,8 +44,7 @@ def _rc_bit(t): t %= 255 if t == 0: return 1 - R = 0b10000000 # register holding r0..r7, r0 = MSB per our shifting below - # Use the standard byte-register formulation. + # Standard byte-register formulation: r0 in the low bit. R = 0x01 for _ in range(t): R <<= 1 diff --git a/formal_verification/keccak/z3_parallel.py b/formal_verification/keccak/z3_parallel.py index 2797a7d84..9eadd295f 100644 --- a/formal_verification/keccak/z3_parallel.py +++ b/formal_verification/keccak/z3_parallel.py @@ -2,7 +2,6 @@ positive control concurrently, print each result as it lands.""" import sys from concurrent.futures import ProcessPoolExecutor, as_completed -from z3 import sat, unsat from z3_verify import check_round, positive_control BUGS = ["theta_no_rot", "rho_swap", "chi_no_not", "chi_swap", "iota_no_rc"] @@ -22,7 +21,6 @@ def w_pos(): def main(): - tasks = [] with ProcessPoolExecutor(max_workers=10) as ex: futs = [] futs.append(ex.submit(w_pos)) @@ -38,7 +36,6 @@ def main(): print(f"DONE {kind} {key} -> {val}", flush=True) print("\n================ SUMMARY ================", flush=True) - pos = results[("pos", True)] if ("pos", True) in results else results.get(("pos", False)) # positive control stored under actual ok value; find it pos_ok = ("pos", True) in results pos_msg = results.get(("pos", True)) or results.get(("pos", False)) diff --git a/formal_verification/keccak/z3_verify.py b/formal_verification/keccak/z3_verify.py index dc2a12148..e23a5f6fc 100644 --- a/formal_verification/keccak/z3_verify.py +++ b/formal_verification/keccak/z3_verify.py @@ -26,7 +26,7 @@ """ import sys from z3 import ( - BitVec, BitVecVal, Concat, Extract, LShR, RotateLeft, ZeroExt, Or, And, + BitVec, BitVecVal, Concat, Extract, LShR, RotateLeft, ULE, ZeroExt, Or, And, Solver, sat, unsat, ) from keccak_ref import RHO, RC @@ -51,9 +51,9 @@ def pi_src(X, Y, z): # rs:161-174 # -------------------------------------------------------------------------- # Independent z3-native reference round (FIPS-202, 64-bit lanes) # -------------------------------------------------------------------------- -def zref_round(lanes, rc_val, bug=None): - # lanes[x][y] : 64-bit BV. Reference is ALWAYS correct (bug only perturbs - # the circuit model, never this). +def zref_round(lanes, rc_val): + # lanes[x][y] : 64-bit BV. The reference is ALWAYS correct — the `bug=` + # injections in build_circuit perturb the circuit model only, never this. C = [lanes[x][0] ^ lanes[x][1] ^ lanes[x][2] ^ lanes[x][3] ^ lanes[x][4] for x in range(5)] D = [C[(x + 4) % 5] ^ RotateLeft(C[(x + 1) % 5], 1) for x in range(5)] @@ -100,7 +100,14 @@ def hw16(lo, hi): # 16-bit from (low byte, high byte) def byte_op_operand(field_expr16): # ByteAlu operand contract: field value must be a byte. - C.append(field_expr16 <= BitVecVal(255, 16)) + # MUST be ULE, not `<=`: z3py's comparison operators on bitvectors are + # SIGNED (SLE), so `expr <= 255` would also admit every value with the + # sign bit set (e.g. 0xFFFF passes at width 16). That is the fail-open + # direction — an out-of-range operand accepted as a byte turns a real + # SAT into a bogus UNSAT. Harmless at the widths used here (the operands + # are sums of two zero-extended bytes, ≤ 510), which is exactly why it + # must be written correctly for the next chip that copies this contract. + C.append(ULE(field_expr16, BitVecVal(255, 16))) return Extract(7, 0, field_expr16) # === theta: Cxz XOR chain === rs:539-588 @@ -242,11 +249,8 @@ def positive_control(round_idx, seed): if s.check() != sat: return False, "constraint system UNSAT for a concrete input (VACUOUS!)" m = s.model() - # reference from concrete input + # reference from concrete input, indexed x + 5y from keccak_ref import keccak_round - in_lanes = [sum(concrete[(x, y, b)] << (8 * b) for b in range(8)) - for y in range(5) for x in range(5)] - # in_lanes indexed x+5y: in_lanes = [0] * 25 for x in range(5): for y in range(5): From b973791c706f4e8da2f3ab0081a1c892c847fcf1 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 13 Aug 2026 00:13:48 -0300 Subject: [PATCH 2/2] Correct the direction of harm in the ULE contract comment The byte bound is a plain conjunct of the solver query, and the goal is a separate positive conjunct, so weakening it can only enlarge the satisfying set: UNSAT can become a bogus SAT, never SAT into UNSAT. A bogus SAT is a spurious counterexample against an honest chip, which the README classifies as the nuisance direction rather than the fail-open one. The prescription (use ULE) was already right; only the rationale was inverted, in the file the README names as the template other chip gates copy. --- formal_verification/keccak/z3_verify.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/formal_verification/keccak/z3_verify.py b/formal_verification/keccak/z3_verify.py index e23a5f6fc..220b9fe31 100644 --- a/formal_verification/keccak/z3_verify.py +++ b/formal_verification/keccak/z3_verify.py @@ -102,9 +102,10 @@ def byte_op_operand(field_expr16): # ByteAlu operand contract: field value must be a byte. # MUST be ULE, not `<=`: z3py's comparison operators on bitvectors are # SIGNED (SLE), so `expr <= 255` would also admit every value with the - # sign bit set (e.g. 0xFFFF passes at width 16). That is the fail-open - # direction — an out-of-range operand accepted as a byte turns a real - # SAT into a bogus UNSAT. Harmless at the widths used here (the operands + # sign bit set (e.g. 0xFFFF passes at width 16). That models the + # contract too weakly: the solver may exhibit an operand the real lookup + # can never supply, reporting a spurious counterexample against an + # honest chip. Harmless at the widths used here (the operands # are sums of two zero-extended bytes, ≤ 510), which is exactly why it # must be written correctly for the next chip that copies this contract. C.append(ULE(field_expr16, BitVecVal(255, 16)))