From 53c3c5efb5c8ea03e0ed57178266095aef7d0dba Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 10 Aug 2026 17:58:26 -0300 Subject: [PATCH 1/3] =?UTF-8?q?docs(formal-verification):=20keccak=20z3/QF?= =?UTF-8?q?-BV=20gate=20=E2=80=94=20the=20verification=20baseline?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add a standalone, reusable template for machine-checking chip round-wiring with z3 in the quantifier-free bitvector theory (QF-BV). The worked instance verifies one Keccak-f[1600] round as shipped on main (#889's inlined θ/ρ shift identities); the README is written as a generic oracle+checker method to be copied for the next chip. Verification only — no constraint or performance change. python/z3, no cargo. Board (regenerated, par.log): - positive control (non-vacuity): PASS — constraints uniquely pin output - negative controls: all SAT (caught) — theta_no_rot, rho_swap, chi_no_not, chi_swap, iota_no_rc, plus tamper_test's iota_wrong_rc, rho_off_by_one, drop_chi_xor_byte, drop_hwsl_carry (changed + removed constraints) - main check: all 24 round indices UNSAT - reference anchored to hashlib SHA3 + repo constants; concrete mirror matches FIPS-202 over random/structured inputs Files: z3_verify.py (gate), keccak_ref.py (independent FIPS-202 reference), model_dataflow.py + test_dataflow.py (concrete mirror), z3_parallel.py (runner), tamper_test.py (controls), test_ref.py (reference tests), README.md (methodology + width audit + scope), par.log (captured board). --- thoughts/formal-verification/keccak/README.md | 191 ++++++++++++ .../formal-verification/keccak/keccak_ref.py | 136 ++++++++ .../keccak/model_dataflow.py | 158 ++++++++++ thoughts/formal-verification/keccak/par.log | 41 +++ .../formal-verification/keccak/tamper_test.py | 53 ++++ .../keccak/test_dataflow.py | 52 ++++ .../formal-verification/keccak/test_ref.py | 41 +++ .../formal-verification/keccak/z3_parallel.py | 67 ++++ .../formal-verification/keccak/z3_verify.py | 291 ++++++++++++++++++ 9 files changed, 1030 insertions(+) create mode 100644 thoughts/formal-verification/keccak/README.md create mode 100644 thoughts/formal-verification/keccak/keccak_ref.py create mode 100644 thoughts/formal-verification/keccak/model_dataflow.py create mode 100644 thoughts/formal-verification/keccak/par.log create mode 100644 thoughts/formal-verification/keccak/tamper_test.py create mode 100644 thoughts/formal-verification/keccak/test_dataflow.py create mode 100644 thoughts/formal-verification/keccak/test_ref.py create mode 100644 thoughts/formal-verification/keccak/z3_parallel.py create mode 100644 thoughts/formal-verification/keccak/z3_verify.py diff --git a/thoughts/formal-verification/keccak/README.md b/thoughts/formal-verification/keccak/README.md new file mode 100644 index 000000000..b540f7469 --- /dev/null +++ b/thoughts/formal-verification/keccak/README.md @@ -0,0 +1,191 @@ +# Formal verification of chip round-wiring — z3/QF-BV baseline + +This directory is the **canonical, reusable template** for machine-checking that a +bit/byte hash chip's per-round transition wiring computes the function it claims, +*given* the contracts of the helper chips it calls. The worked instance here is +`prover/src/tables/keccak_rnd.rs` (one Keccak-f[1600] round); the method is written +to be copied for the next chip (SHA-2/3 variants, BLAKE3, …). + +If you are verifying a new chip, read the **Method** and **Mandatory discipline** +sections, then clone this file layout and swap in your chip's reference + contracts. + +--- + +## What is proven, in one line + +For **every** constraint-satisfying assignment of the chip's trace columns, the +chip's declared output equals an **independent** reference implementation of the +round — *assuming* each helper-chip lookup obeys its typed contract. Formally: +assert `chip_output ≠ reference(input)` and ask z3 for a counterexample. + +- **UNSAT** ⇒ no such assignment exists ⇒ the wiring is correct (given the contracts). +- **SAT** ⇒ the constraints permit a wrong output ⇒ under-constrained / mis-wired, + and the model hands you the forging assignment. + +## Method: oracle + checker + +The verification is an **assume-guarantee** argument split into two halves with a +deliberate trust boundary: + +**Oracle (human-owned, per-chip).** Three artifacts a person writes and reviews: +1. **Reference `f`** — the round recomputed straight from the spec (FIPS-202 here), + in a representation *structurally independent* of the circuit's wiring. Here it is + 64-bit-lane bitvector ops (`RotateLeft`/`xor`/`and`/`not`) written from the + standard, in `keccak_ref.py` (`zref_round` in `z3_verify.py`), anchored against + Python's `hashlib` SHA3 and the repo constant tables (`test_ref.py`). +2. **Column-role map** — which trace column plays which algebraic role in the round + (which byte of which lane, which carry, which RC). This is the transcription of + the chip's `bus_interactions` / constraint set into equations. +3. **Chip-contract library** — the typed guarantee each helper lookup provides + (below). These are *assumed*; each is itself a separately-verified chip. + +**Checker (generic, reusable).** z3 in the quantifier-free bitvector theory +(**QF-BV**). Every trace column becomes a free bitvector; every bus interaction and +eval constraint becomes an equation over those frees under the referenced contract; +the output columns are whatever the constraints force. The checker is chip-agnostic +— only the oracle changes between chips. + +The trust boundary is the point: a mis-transcription in the oracle is caught by the +**concrete mirror** (`model_dataflow.py`, validated forward against the reference in +`test_dataflow.py` over random and structured inputs) and by the **negative +controls** (below). z3 never sees the Rust; faithfulness of the model to the Rust is +a human obligation, and the long-term fix is to *generate* the model from the +constraint IR instead of hand-transcribing it. + +## Typed contract library (assume-guarantee) + +Each helper lookup is modeled by its contract, not its implementation: + +| Contract | Guarantee modeled | +|---|---| +| `ByteAlu(op, a, b, c)` | `a,b,c` are bytes and `c = a op b`, `op ∈ {XOR, AND, ADD}`. Operands passed as linear combinations must themselves be bytes — the lookup table only has byte rows — modeled as `Σ ≤ 255` on the field value with the low 8 bits used. | +| `AreBytes(a, b)` | both `a` and `b` lie in `0..256` (a range check). In QF-BV this is supplied structurally by declaring the column an 8-bit vector and packing pairs into 16 bits. | +| `Hwsl(in16, s, left16, right16)` (halfword shift) | `left16 = (in16 << s) mod 2¹⁶`, `right16 = in16 >> (16 − s)` (with `right16 = 0` at `s = 0`). Keccak's θ/ρ shifts no longer *call* this lookup — they are inline linear identities (see "Which round variant") — but the QF-BV encoding of the decomposition is identical, so the same contract row models both. | +| 32-bit / word recomposition lookups | a wide value equals the range-checked recomposition of its limbs (`word = Σ limb_i · 2^{8i}`), each limb a byte. Not exercised by keccak_rnd; listed because the template's next targets (e.g. 32-bit-lane hashes) need it. | +| `KeccakRc(round, rc[8])` | `rc` = little-endian bytes of `KECCAK_RC[round]`. | + +## Mandatory discipline (do not skip any of these) + +1. **Negative controls are not optional.** "UNSAT = verified" is meaningless unless + you have shown the encoding is *falsifiable*: inject a bug into the model and + confirm it flips to **SAT**. If a bug does not flip the result, the encoding is + vacuous and every UNSAT it ever produced is worthless. This directory ships + controls of two kinds — **changed** constraints and **removed** constraints — + because an over-constrained model can hide a missing constraint. See + `tamper_test.py` and the `bug=` cases in `z3_verify.py`. + +2. **Positive control (non-vacuity).** Pin the input to a concrete value, drop the + diff assertion, and confirm the constraint system is **SAT** *and* uniquely pins + the output to the reference. This proves the UNSATs are "no counterexample", + not "no models at all". See `positive_control` in `z3_verify.py`. + +3. **Width audit — the field-lift trap.** The circuit lives over a large prime field; + the model lives in fixed-width bitvectors. That is only faithful if **every** + byte/word width in the model is backed, in the circuit, by (a) a real range-check + contract *and* (b) a non-overflow side condition guaranteeing the field arithmetic + never wraps the modulus. A field-level attacker who can make an "8-bit" value hold + `> 255`, or make a sum overflow `p`, escapes a bitvector model that silently + assumed the bound. For each lifted width, cite the exact contract that pins it + (here: `AreBytes` on `Cxz_left`/`rot_left`/`rot_right`, `IS_BIT` on the θ carry + `Cxz_right`) and confirm the operands cannot overflow. Where the circuit replaced + a lookup with a **linear identity** (keccak's inlined θ/ρ shifts), the bound is + *load-bearing at the field level* in a way QF-BV cannot see: `2¹⁶` is invertible + mod the Goldilocks prime, so without the range bound the `(left, right)` + decomposition is ambiguous. QF-BV proves the wiring given the bound; proving the + bound *suffices* mod `p` needs an integer/field model (see Scope + follow-ups). + +4. **Independent reference.** The reference must be derived from the spec, not from + the circuit or the repo's constant tables, then anchored to an outside + implementation (`hashlib`) and cross-checked against the repo constants. A + reference that copies the circuit proves only that the circuit equals itself. + +5. **Fail-open is the only dangerous failure mode.** A gate that wrongly rejects an + honest chip is a nuisance you will notice immediately. A gate that is **green for + the wrong reason** — vacuous encoding, a dropped constraint the model never had, + a width the model assumed but the circuit never checks — silently blesses an + unsound chip. Every item above exists to close a fail-open hole. When in doubt, + assume the gate is lying and add a control that would catch it. + +## Which round variant this instance verifies + +The model verifies the **shipped** Keccak round on `main` as of #889 +(`perf(keccak): inline θ/ρ halfword shifts as μ-gated identities`), commit +`6a280121`. On main the θ rotate-by-1 and the ρ per-lane shifts are enforced by +inline μ-gated linear identities in `KeccakRndConstraints`: + +``` +θ: μ · (in·2 − right·2¹⁶ − left) = 0 (right = 1-bit carry, IS_BIT-pinned) +ρ: μ · (in·2^rnc − right·2¹⁶ − left) = 0 (rnc = KECCAK_RHO[x][y] % 16) +``` + +with `left`/`right` the range-checked (`AreBytes`) byte-pair halves. The QF-BV model +encodes each shift as the *unique* decomposition those identities force — +`left = (in << rnc) mod 2¹⁶`, `right = in >> (16 − rnc)`, the byte-pair widths +supplying the `[0, 2¹⁶)` bound — so the gate is faithful to the inlined round even +though the module comments describe it as the pre-inline "HWSL" circuit; the two are +constraint-identical in QF-BV. Verified: main's `keccak_rnd.rs` is byte-identical to +the branch this model was authored against, so the wiring the model transcribes is +the shipped wiring. (The `rs:NNN` line citations in the code comments predate the +inline change and have drifted by a few dozen lines; the referenced constructs are +unchanged.) + +**Known scope gap carried as the first follow-up:** QF-BV cannot test that the +`AreBytes`/`IS_BIT` bounds are *sufficient* mod `p` for the inline identities (bit +vectors make `2¹⁶` a zero divisor, not the invertible element it is mod the +Goldilocks prime). That companion proof — an integer-mod-`p` model showing that +dropping a range bound makes the decomposition ambiguous (SAT) — was written for the +optimization PR that introduced the identities and is *not* included in this +baseline. Porting it here (or moving to a solver with native field support) is the +first extension of this template. + +## Scope + +- **In scope: bit/byte-oriented hashes** — Keccak/SHA-3, SHA-2, BLAKE3. Their round + functions are boolean/byte algebra, which QF-BV models exactly and z3 decides + efficiently. +- **Out of scope: native-field chips** — e.g. Poseidon/Poseidon2, whose round is + arithmetic in the STARK field. Bitvectors are the wrong theory; use a finite-field + solver (`cvc5` with the `FF` theory) or a proof assistant (Lean). This baseline + deliberately does not attempt them. +- The check is **one round's transition given the helper-chip contracts**. It does + not re-verify the helper chips (BITWISE is a fully enumerated `2²⁰`-row + preprocessed table; the range chips are separate), nor cross-row/multiplicity + gating beyond what the μ column expresses. + +## Sibling verifications following this method + +- The **BLAKE3 chip gate** and the **keccak-sponge** verification already use this + oracle+QF-BV+controls structure. This directory is the canonical write-up; new + chip gates should mirror its file layout and its Mandatory-discipline checklist. + +## Files + +- `z3_verify.py` — the gate: free-var QF-BV model of the round, the typed contracts, + the 24-round UNSAT check, the positive control, and the `bug=` negative controls. +- `z3_parallel.py`, `par.log` — parallel driver + captured board (all-UNSAT ×24 + + controls). +- `tamper_test.py` — changed-constraint **and** removed-constraint controls, with the + forged witnesses exhibited for the removed-constraint cases. +- `keccak_ref.py`, `test_ref.py` — independent FIPS-202 reference (RC/RHO generated + from the spec recurrences) + external anchoring against `hashlib` and the repo + constants. +- `model_dataflow.py`, `test_dataflow.py` — concrete byte-level forward mirror of the + modeled equations, validated against the reference over random/structured inputs + and confirmed to move under each injected bug. + +## Running the gate + +z3's Python bindings are the only dependency (no cargo, no repo build): + +``` +pip install z3-solver # if not already importable +cd thoughts/formal-verification/keccak +python3 test_ref.py # reference constants + SHA3 vs hashlib +python3 test_dataflow.py # concrete mirror vs reference (+ bug sanity) +python3 z3_parallel.py # the gate: 24 rounds + controls (see par.log) +# or, single-process with inline printout: +python3 z3_verify.py +``` + +Expected board: positive control PASS, all negative controls **SAT** (caught), all +24 rounds **UNSAT**. Anything else is a real signal — investigate before trusting. diff --git a/thoughts/formal-verification/keccak/keccak_ref.py b/thoughts/formal-verification/keccak/keccak_ref.py new file mode 100644 index 000000000..0c5ab61a3 --- /dev/null +++ b/thoughts/formal-verification/keccak/keccak_ref.py @@ -0,0 +1,136 @@ +""" +Independent Keccak-f[1600] reference, built from the FIPS-202 spec ALGORITHMS +(not by copying the circuit or the repo's constant tables). + + - RHO offsets generated from the FIPS-202 (x,y) walk with triangular offsets. + - RC round constants generated from the FIPS-202 LFSR (rc(t)). + - theta / rho / pi / chi / iota implemented per FIPS-202. + +Validation anchors (see run at bottom / test_ref.py): + - The permutation is wired into a SHA3-256 sponge and checked against + Python's hashlib (an independent NIST implementation). + - RHO/RC are separately cross-checked against the repo's KECCAK_RHO/KECCAK_RC. + +Lane indexing matches the circuit: state[x + 5*y], x = column, y = row. +""" + +MASK64 = (1 << 64) - 1 + + +def rotl64(v, r): + r &= 63 + if r == 0: + return v & MASK64 + return ((v << r) | (v >> (64 - r))) & MASK64 + + +# --- RHO offsets from the FIPS-202 recurrence (Algorithm 2, rho) --------------- +# Start at (x,y) = (1,0); for t = 0..23 the offset is (t+1)(t+2)/2 mod 64, +# then (x,y) <- (y, (2x+3y) mod 5). (0,0) keeps offset 0. +def gen_rho(): + rho = [[0] * 5 for _ in range(5)] # rho[x][y] + x, y = 1, 0 + for t in range(24): + rho[x][y] = ((t + 1) * (t + 2) // 2) % 64 + x, y = y, (2 * x + 3 * y) % 5 + return rho + + +RHO = gen_rho() + + +# --- RC round constants from the FIPS-202 LFSR (Algorithm 5, rc) --------------- +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. + R = 0x01 + for _ in range(t): + R <<= 1 + if R & 0x100: + R ^= 0x71 # x^8 + x^6 + x^5 + x^4 + 1 -> low byte feedback 0x71 + R &= 0xFF + return R & 1 + + +def gen_rc(): + rc = [] + for ir in range(24): + w = 0 + for j in range(7): # j = 0..6 -> bit positions 2^j - 1 + if _rc_bit(j + 7 * ir): + w |= 1 << ((1 << j) - 1) + rc.append(w & MASK64) + return rc + + +RC = gen_rc() + + +# --- The permutation, per FIPS-202 ------------------------------------------- +def keccak_round(state, rc): + """One round of Keccak-f[1600]. `state` is list[25] of u64, state[x+5y].""" + a = list(state) + + # theta + C = [a[x] ^ a[x + 5] ^ a[x + 10] ^ a[x + 15] ^ a[x + 20] for x in range(5)] + D = [C[(x + 4) % 5] ^ rotl64(C[(x + 1) % 5], 1) for x in range(5)] + for x in range(5): + for y in range(5): + a[x + 5 * y] ^= D[x] + + # rho + pi: B[X][Y] = rotl(A[(X+3Y)%5][X], RHO[(X+3Y)%5][X]) + B = [0] * 25 + for X in range(5): + for Y in range(5): + sx = (X + 3 * Y) % 5 + sy = X + B[X + 5 * Y] = rotl64(a[sx + 5 * sy], RHO[sx][sy]) + + # chi + out = [0] * 25 + for x in range(5): + for y in range(5): + out[x + 5 * y] = B[x + 5 * y] ^ ((~B[(x + 1) % 5 + 5 * y] & MASK64) & B[(x + 2) % 5 + 5 * y]) + + # iota + out[0] ^= rc + return out + + +def keccak_f1600(state): + s = list(state) + for r in range(24): + s = keccak_round(s, RC[r]) + return s + + +# --- SHA3-256 sponge on top of the permutation (for external validation) ------ +def sha3_256(msg: bytes) -> bytes: + rate = 136 # bytes (1088 bits) + # pad10*1 with SHA-3 domain separation 0x06 + m = bytearray(msg) + m.append(0x06) + while len(m) % rate != 0: + m.append(0x00) + m[-1] ^= 0x80 + + state = [0] * 25 + for off in range(0, len(m), rate): + block = m[off:off + rate] + for i in range(rate // 8): + lane = int.from_bytes(block[i * 8:i * 8 + 8], "little") + state[i] ^= lane + state = keccak_f1600(state) + + out = bytearray() + while len(out) < 32: + for i in range(rate // 8): + out += state[i].to_bytes(8, "little") + if len(out) >= 32: + break + if len(out) < 32: + state = keccak_f1600(state) + return bytes(out[:32]) diff --git a/thoughts/formal-verification/keccak/model_dataflow.py b/thoughts/formal-verification/keccak/model_dataflow.py new file mode 100644 index 000000000..9579a787b --- /dev/null +++ b/thoughts/formal-verification/keccak/model_dataflow.py @@ -0,0 +1,158 @@ +""" +Concrete byte-level mirror of the keccak_rnd circuit's contract dataflow. + +Every equation here corresponds 1:1 to a bus interaction / eval constraint in +prover/src/tables/keccak_rnd.rs, evaluated FORWARD with concrete ints. Its sole +job is to validate that the byte-level wiring I will hand-encode into z3 +actually reproduces the FIPS-202 reference round (guards against a wholesale +wrong model that a symbolic UNSAT could not reveal). + +The `bug` flag lets us confirm each negative control genuinely perturbs output. +Line-number citations (prover/src/tables/keccak_rnd.rs) in comments. +""" +from keccak_ref import RHO, RC + + +def lane_to_bytes(v): + return [(v >> (8 * b)) & 0xFF for b in range(8)] + + +def bytes_to_lane(bs): + return sum(int(bs[b]) << (8 * b) for b in range(8)) + + +def cxz_right_bit_for_byte(b): + # keccak_rnd.rs:126-132 -> even b: Some((b/2 + 3)%4); odd: None + return (b // 2 + 3) % 4 if b % 2 == 0 else None + + +def pi_src_bytes(X, Y, z): + # keccak_rnd.rs:161-174 pi_src_cols: (sx,sy)=((X+3Y)%5, X), rbc=RHO[sx][sy]//16 + sx = (X + 3 * Y) % 5 + sy = X + rbc = RHO[sx][sy] // 16 + if rbc == 0: + l, r = z, (z + 6) % 8 + elif rbc == 1: + l, r = (z + 6) % 8, (z + 4) % 8 + elif rbc == 2: + l, r = (z + 4) % 8, (z + 2) % 8 + else: + l, r = (z + 2) % 8, z + return sx, sy, l, r + + +def round_dataflow(start_lanes, r, bug=None): + """Forward-evaluate one round via the circuit's contract equations. + + start_lanes: list[25] u64. Returns list[25] u64 (out state).""" + S = [[lane_to_bytes(start_lanes[x + 5 * y]) for y in range(5)] for x in range(5)] + # index as S[x][y][b] + + # === theta: Cxz XOR chain === keccak_rnd.rs:539-588 + cxz = [[[0] * 8 for _ in range(4)] for _ in range(5)] + for x in range(5): + for b in range(8): + cxz[x][0][b] = S[x][0][b] ^ S[x][1][b] # :541-559 + for stage in range(1, 4): + y = stage + 1 + for b in range(8): + cxz[x][stage][b] = cxz[x][stage - 1][b] ^ S[x][y][b] # :567-585 + + # === theta: HWSL rotate-C-by-1 === keccak_rnd.rs:593-631 + cxz_left = [[0] * 8 for _ in range(5)] + cxz_right = [[0] * 4 for _ in range(5)] + for x in range(5): + for hw in range(4): + Chw = cxz[x][3][2 * hw] | (cxz[x][3][2 * hw + 1] << 8) # :600-609 input hw + left16 = (Chw << 1) & 0xFFFF # :613-622 shifted + cxz_left[x][2 * hw] = left16 & 0xFF + cxz_left[x][2 * hw + 1] = (left16 >> 8) & 0xFF + cxz_right[x][hw] = (Chw >> 15) & 1 # :624 carry bit + + def rotated_c(xp, b): + # keccak_rnd.rs:322-329 / 663-672 reconstruction + contrib = 0 + hw = cxz_right_bit_for_byte(b) + if hw is not None: + contrib = cxz_right[xp][hw] + val = cxz_left[xp][b] + contrib + assert val <= 255, "rotated_C operand exceeds a byte" + return val + + # === theta: Dxz XOR === keccak_rnd.rs:661-690 + Dxz = [[0] * 8 for _ in range(5)] + for x in range(5): + for b in range(8): + cm1 = cxz[(x + 4) % 5][3][b] # C[(x-1)%5] + rc1 = rotated_c((x + 1) % 5, b) # rot(C[(x+1)%5],1) + if bug == "theta_no_rot": + rc1 = cxz[(x + 1) % 5][3][b] # drop the rotate + Dxz[x][b] = cm1 ^ rc1 + + # === theta final XOR === keccak_rnd.rs:694-717 + theta = [[[0] * 8 for _ in range(5)] for _ in range(5)] + for x in range(5): + for y in range(5): + for b in range(8): + theta[x][y][b] = S[x][y][b] ^ Dxz[x][b] + + # === rho: HWSL === keccak_rnd.rs:723-766 + rho_tbl = [[RHO[x][y] for y in range(5)] for x in range(5)] + if bug == "rho_swap": + rho_tbl[1][0], rho_tbl[2][0] = rho_tbl[2][0], rho_tbl[1][0] + rot_left = [[[0] * 8 for _ in range(5)] for _ in range(5)] + rot_right = [[[0] * 8 for _ in range(5)] for _ in range(5)] + for x in range(5): + for y in range(5): + rnc = rho_tbl[x][y] % 16 + for hw in range(4): + Thw = theta[x][y][2 * hw] | (theta[x][y][2 * hw + 1] << 8) + left16 = (Thw << rnc) & 0xFFFF + right16 = (Thw >> (16 - rnc)) & 0xFFFF if rnc > 0 else 0 + rot_left[x][y][2 * hw] = left16 & 0xFF + rot_left[x][y][2 * hw + 1] = (left16 >> 8) & 0xFF + rot_right[x][y][2 * hw] = right16 & 0xFF + rot_right[x][y][2 * hw + 1] = (right16 >> 8) & 0xFF + + def pi(X, Y, z): + # keccak_rnd.rs:793-795 virtual pi = rot_left[l] + rot_right[r] + sx, sy, l, rr = pi_src_bytes(X, Y, z) + val = rot_left[sx][sy][l] + rot_right[sx][sy][rr] + assert val <= 255, "pi operand exceeds a byte" + return val + + # === chi: AND then XOR === keccak_rnd.rs:796-870 + chi = [[[0] * 8 for _ in range(5)] for _ in range(5)] + for x in range(5): + for y in range(5): + for b in range(8): + p0 = pi(x, y, b) + p1 = pi((x + 1) % 5, y, b) + p2 = pi((x + 2) % 5, y, b) + if bug == "chi_no_not": + ands = p1 & p2 # drop the NOT + elif bug == "chi_swap": + ands = (0xFF - p2) & p1 # swap the two operands + else: + ands = (0xFF - p1) & p2 # (255 - pi[x+1]) AND pi[x+2] + chi[x][y][b] = p0 ^ ands + + # === iota === keccak_rnd.rs:872-894 + rc_bytes = lane_to_bytes(RC[r]) + iota = [0] * 8 + for b in range(8): + if bug == "iota_no_rc": + iota[b] = chi[0][0][b] # drop rc XOR + else: + iota[b] = chi[0][0][b] ^ rc_bytes[b] + + # === output handoff === keccak_rnd.rs:496-509 + out = [0] * 25 + for x in range(5): + for y in range(5): + if x == 0 and y == 0: + out[0] = bytes_to_lane(iota) + else: + out[x + 5 * y] = bytes_to_lane(chi[x][y]) + return out diff --git a/thoughts/formal-verification/keccak/par.log b/thoughts/formal-verification/keccak/par.log new file mode 100644 index 000000000..42086a395 --- /dev/null +++ b/thoughts/formal-verification/keccak/par.log @@ -0,0 +1,41 @@ +DONE pos True -> output uniquely pinned to reference +DONE bug chi_swap -> sat +DONE bug rho_swap -> sat +DONE bug chi_no_not -> sat +DONE bug theta_no_rot -> sat +DONE bug iota_no_rc -> sat +DONE round 3 -> unsat +DONE round 2 -> unsat +DONE round 5 -> unsat +DONE round 0 -> unsat +DONE round 1 -> unsat +DONE round 9 -> unsat +DONE round 7 -> unsat +DONE round 8 -> unsat +DONE round 4 -> unsat +DONE round 6 -> unsat +DONE round 10 -> unsat +DONE round 12 -> unsat +DONE round 16 -> unsat +DONE round 17 -> unsat +DONE round 11 -> unsat +DONE round 13 -> unsat +DONE round 14 -> unsat +DONE round 18 -> unsat +DONE round 15 -> unsat +DONE round 19 -> unsat +DONE round 21 -> unsat +DONE round 22 -> unsat +DONE round 20 -> unsat +DONE round 23 -> unsat + +================ SUMMARY ================ +positive control (non-vacuity): PASS (output uniquely pinned to reference) +negative control theta_no_rot : sat OK +negative control rho_swap : sat OK +negative control chi_no_not : sat OK +negative control chi_swap : sat OK +negative control iota_no_rc : sat OK +main check: ALL 24 UNSAT + +VERDICT: VERIFIED (given contracts) diff --git a/thoughts/formal-verification/keccak/tamper_test.py b/thoughts/formal-verification/keccak/tamper_test.py new file mode 100644 index 000000000..c731a3cb3 --- /dev/null +++ b/thoughts/formal-verification/keccak/tamper_test.py @@ -0,0 +1,53 @@ +"""Tamper demo: CHANGED constraints and REMOVED constraints must both flip +the gate from UNSAT (verified) to SAT (forgeable). Clean model run first as +the control.""" +from z3 import Solver, And, Or, Concat, Extract, sat, unsat, is_true +import z3_verify as zv +from keccak_ref import RC + +ROUND = 1 + +print("=== control: clean model, round 1 ===") +r = zv.check_round(ROUND) +print(f" clean -> {r} (want unsat) {'OK' if r == unsat else '!!! BROKEN'}") +assert r == unsat + +CASES = [ + ("iota_wrong_rc", "CHANGED"), + ("rho_off_by_one", "CHANGED"), + ("drop_chi_xor_byte", "REMOVED"), + ("drop_hwsl_carry", "REMOVED"), +] + +print("\n=== tampered models: gate must catch every one (SAT) ===") +for bug, kind in CASES: + r = zv.check_round(ROUND, bug=bug) + ok = "OK — gate catches it" if r == sat else "!!! GATE MISSED THE BUG" + print(f" {kind} {bug:18s} -> {r} {ok}") + assert r == sat, f"gate failed to catch {bug}" + +# ---- exhibit the forged witnesses for the two REMOVED cases ----------------- +def exhibit(bug): + C, out_byte, start = zv.build_circuit(ROUND, f"cex_{bug}", bug=bug) + lanes = [[Concat(*[start[(x, y, b)] for b in reversed(range(8))]) + for y in range(5)] for x in range(5)] + ref = zv.zref_round(lanes, RC[ROUND]) + rb = lambda x, y, b: Extract(8 * b + 7, 8 * b, ref[x][y]) + s = Solver() + s.add(And(*C)) + s.add(Or(*[out_byte(x, y, b) != rb(x, y, b) + for x in range(5) for y in range(5) for b in range(8)])) + assert s.check() == sat + m = s.model() + bad = [(x, y, b) for x in range(5) for y in range(5) for b in range(8) + if is_true(m.evaluate(out_byte(x, y, b) != rb(x, y, b)))] + lanes_hit = sorted(set((x, y) for x, y, _ in bad)) + print(f" {bug}: forged witness makes {len(bad)} output bytes wrong; " + f"lanes hit: {lanes_hit[:8]}{'...' if len(lanes_hit) > 8 else ''}") + +print("\n=== forged-witness exhibits (REMOVED cases) ===") +exhibit("drop_chi_xor_byte") +exhibit("drop_hwsl_carry") + +print("\nVERDICT: clean=UNSAT, all 4 tampers=SAT -> gate is sensitive to both " + "changed AND removed constraints.") diff --git a/thoughts/formal-verification/keccak/test_dataflow.py b/thoughts/formal-verification/keccak/test_dataflow.py new file mode 100644 index 000000000..a0361f2cb --- /dev/null +++ b/thoughts/formal-verification/keccak/test_dataflow.py @@ -0,0 +1,52 @@ +"""Validate the concrete contract-dataflow against the independent reference.""" +import random +from keccak_ref import RC, keccak_round, keccak_f1600 +from model_dataflow import round_dataflow + +rng = random.Random(0xC0FFEE) +M = (1 << 64) - 1 + +print("=== per-round: contract dataflow vs FIPS-202 reference (random states) ===") +ok = True +for trial in range(200): + st = [rng.randrange(0, 1 << 64) for _ in range(25)] + r = rng.randrange(0, 24) + got = round_dataflow(st, r) + exp = keccak_round(st, RC[r]) + if got != exp: + ok = False + print(f" MISMATCH trial={trial} round={r}") + break +print(" 200 random single rounds match:", ok) +assert ok + +print("\n=== 24-round chain (full permutation) via dataflow vs reference ===") +ok2 = True +for trial in range(20): + st = [rng.randrange(0, 1 << 64) for _ in range(25)] + s = list(st) + for r in range(24): + s = round_dataflow(s, r) + if s != keccak_f1600(st): + ok2 = False + print(f" MISMATCH trial={trial}") + break +print(" 20 full 24-round permutations match:", ok2) +assert ok2 + +# Also: all-zero and specific structured inputs +for st in ([0] * 25, [1] * 25, list(range(25)), [M] * 25): + s = list(st) + for r in range(24): + s = round_dataflow(s, r) + assert s == keccak_f1600(st), st[:3] +print(" structured inputs (zeros/ones/range/all-FF) match: True") + +print("\n=== sanity: each injected bug DOES change output (concrete) ===") +st = [rng.randrange(0, 1 << 64) for _ in range(25)] +for bug in ["theta_no_rot", "rho_swap", "chi_no_not", "chi_swap", "iota_no_rc"]: + changed = any(round_dataflow(st, r, bug=bug) != keccak_round(st, RC[r]) for r in range(24)) + print(f" bug={bug:14s} perturbs output: {changed}") + assert changed, bug + +print("\nALL DATAFLOW VALIDATIONS PASSED") diff --git a/thoughts/formal-verification/keccak/test_ref.py b/thoughts/formal-verification/keccak/test_ref.py new file mode 100644 index 000000000..0f80d6eac --- /dev/null +++ b/thoughts/formal-verification/keccak/test_ref.py @@ -0,0 +1,41 @@ +"""Validate the independent reference: constants + full permutation.""" +import hashlib +from keccak_ref import RC, RHO, sha3_256 + +# Repo constants (from executor/src/vm/instruction/execution.rs:646-680), pasted +# here ONLY to cross-check my spec-generated values. Correctness is anchored to +# FIPS-202 (my generators) + hashlib, not to these. +REPO_RC = [ + 0x0000000000000001, 0x0000000000008082, 0x800000000000808A, 0x8000000080008000, + 0x000000000000808B, 0x0000000080000001, 0x8000000080008081, 0x8000000000008009, + 0x000000000000008A, 0x0000000000000088, 0x0000000080008009, 0x000000008000000A, + 0x000000008000808B, 0x800000000000008B, 0x8000000000008089, 0x8000000000008003, + 0x8000000000008002, 0x8000000000000080, 0x000000000000800A, 0x800000008000000A, + 0x8000000080008081, 0x8000000000008080, 0x0000000080000001, 0x8000000080008008, +] +# KECCAK_RHO[x][y] in the repo +REPO_RHO = [ + [0, 36, 3, 41, 18], + [1, 44, 10, 45, 2], + [62, 6, 43, 15, 61], + [28, 55, 25, 21, 56], + [27, 20, 39, 8, 14], +] + +print("=== constant cross-checks (spec-generated vs repo) ===") +print("RC match:", RC == REPO_RC) +print("RHO match:", RHO == REPO_RHO) +assert RC == REPO_RC, (RC, REPO_RC) +assert RHO == REPO_RHO, (RHO, REPO_RHO) + +print("\n=== SHA3-256 vs hashlib (external NIST impl) ===") +tests = [b"", b"abc", b"The quick brown fox jumps over the lazy dog", bytes(range(200))] +allok = True +for t in tests: + mine = sha3_256(t).hex() + ref = hashlib.sha3_256(t).hexdigest() + ok = mine == ref + allok &= ok + print(f" len={len(t):3d} match={ok} {mine}") +assert allok +print("\nALL REFERENCE VALIDATIONS PASSED") diff --git a/thoughts/formal-verification/keccak/z3_parallel.py b/thoughts/formal-verification/keccak/z3_parallel.py new file mode 100644 index 000000000..2797a7d84 --- /dev/null +++ b/thoughts/formal-verification/keccak/z3_parallel.py @@ -0,0 +1,67 @@ +"""Parallel driver: run all 24 round UNSAT checks + 5 negative controls + +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"] + + +def w_round(r): + return ("round", r, str(check_round(r))) + + +def w_bug(bug): + return ("bug", bug, str(check_round(1, bug=bug))) + + +def w_pos(): + ok, msg = positive_control(5, seed=1) + return ("pos", ok, msg) + + +def main(): + tasks = [] + with ProcessPoolExecutor(max_workers=10) as ex: + futs = [] + futs.append(ex.submit(w_pos)) + for bug in BUGS: + futs.append(ex.submit(w_bug, bug)) + for r in range(24): + futs.append(ex.submit(w_round, r)) + + results = {} + for f in as_completed(futs): + kind, key, val = f.result() + results[(kind, key)] = val + 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)) + print(f"positive control (non-vacuity): {'PASS' if pos_ok else 'FAIL'} ({pos_msg})") + + neg_ok = True + for bug in BUGS: + v = results[("bug", bug)] + ok = (v == "sat") + neg_ok &= ok + print(f"negative control {bug:14s}: {v:6s} {'OK' if ok else 'FAIL(!vacuous)'}") + + all_unsat = True + for r in range(24): + v = results[("round", r)] + all_unsat &= (v == "unsat") + bad = [r for r in range(24) if results[("round", r)] != "unsat"] + print(f"main check: {'ALL 24 UNSAT' if all_unsat else 'NOT ALL UNSAT: ' + str([(r, results[('round', r)]) for r in bad])}") + + verdict = pos_ok and neg_ok and all_unsat + print("\nVERDICT:", "VERIFIED (given contracts)" if verdict else "NOT VERIFIED — investigate") + sys.exit(0 if verdict else 1) + + +if __name__ == "__main__": + main() diff --git a/thoughts/formal-verification/keccak/z3_verify.py b/thoughts/formal-verification/keccak/z3_verify.py new file mode 100644 index 000000000..dc2a12148 --- /dev/null +++ b/thoughts/formal-verification/keccak/z3_verify.py @@ -0,0 +1,291 @@ +""" +Formal (z3 / QF_BV) assume-guarantee check that one `keccak_rnd` round, as +wired in prover/src/tables/keccak_rnd.rs, computes a correct Keccak-f[1600] +round GIVEN the helper-chip contracts (ByteAlu XOR/AND, Hwsl, KeccakRc; the +AreBytes/IS_BIT range checks are captured by byte-width + explicit bit/byte +domain constraints). + +Method: every trace column is a FREE bitvector. Each bus interaction and eval +constraint becomes an equation relating those free vars (under the referenced +chip's contract). The output lanes are whatever the constraints force. We assert +`output != reference_round(input)` and ask z3 for a counterexample: + UNSAT -> for all constraint-satisfying assignments, output == reference. + SAT -> the constraints permit a wrong output (under-constrained / mis-wired). + +The reference round (`zref_round`) is written directly from FIPS-202 with 64-bit +BV ops (RotateLeft / xor / and / not) — structurally independent of the circuit's +byte-level HWSL wiring. + +Contracts assumed (assume-guarantee): + ByteAlu(op,a,b,c): a,b,c are bytes and c = a `op` b (op in {XOR,AND}). Operands + given as linear combos are required to be bytes (the lookup only has byte + rows) -> modeled as `sum <= 255` on the field value, low 8 bits used. + Hwsl(in16, s, left16, right16): left16 = (in16 << s) mod 2^16, + right16 = in16 >> (16 - s) (right16 = 0 when s = 0). + KeccakRc(round, rc[8]): rc = little-endian bytes of KECCAK_RC[round]. +""" +import sys +from z3 import ( + BitVec, BitVecVal, Concat, Extract, LShR, RotateLeft, ZeroExt, Or, And, + Solver, sat, unsat, +) +from keccak_ref import RHO, RC + +# -------------------------------------------------------------------------- +# byte<->column helpers mirroring keccak_rnd.rs::cols +# -------------------------------------------------------------------------- +def cxz_right_bit_for_byte(b): # rs:126-132 + return (b // 2 + 3) % 4 if b % 2 == 0 else None + +def pi_src(X, Y, z): # rs:161-174 + sx = (X + 3 * Y) % 5 + sy = X + rbc = RHO[sx][sy] // 16 + l, r = [(z, (z + 6) % 8), + ((z + 6) % 8, (z + 4) % 8), + ((z + 4) % 8, (z + 2) % 8), + ((z + 2) % 8, z)][rbc] + return sx, sy, l, r + + +# -------------------------------------------------------------------------- +# 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). + 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)] + a = [[lanes[x][y] ^ D[x] for y in range(5)] for x in range(5)] + B = [[None] * 5 for _ in range(5)] + for X in range(5): + for Y in range(5): + sx = (X + 3 * Y) % 5 + sy = X + B[X][Y] = RotateLeft(a[sx][sy], RHO[sx][sy]) + out = [[None] * 5 for _ in range(5)] + for x in range(5): + for y in range(5): + out[x][y] = B[x][y] ^ ((~B[(x + 1) % 5][y]) & B[(x + 2) % 5][y]) + out[0][0] = out[0][0] ^ BitVecVal(rc_val, 64) + return out + + +# -------------------------------------------------------------------------- +# Build the circuit-model constraint system as free vars + equations. +# Returns (constraints, out_byte(x,y,b), start_byte(x,y,b)). +# -------------------------------------------------------------------------- +def build_circuit(round_idx, tag, bug=None): + C = [] # list of z3 Bool constraints + def V(name, w=8): # fresh free var + return BitVec(f"{tag}_{name}", w) + + # free columns ----------------------------------------------------------- + start = {(x, y, b): V(f"start_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + cxz = {(x, s, b): V(f"cxz_{x}_{s}_{b}") for x in range(5) for s in range(4) for b in range(8)} + cxzL = {(x, b): V(f"cxzL_{x}_{b}") for x in range(5) for b in range(8)} + cxzR = {(x, hw): V(f"cxzR_{x}_{hw}") for x in range(5) for hw in range(4)} + dxz = {(x, b): V(f"dxz_{x}_{b}") for x in range(5) for b in range(8)} + theta = {(x, y, b): V(f"theta_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + rotL = {(x, y, b): V(f"rotL_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + rotR = {(x, y, b): V(f"rotR_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + chA = {(x, y, b): V(f"chiand_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + chi = {(x, y, b): V(f"chi_{x}_{y}_{b}") for x in range(5) for y in range(5) for b in range(8)} + rc = {b: V(f"rc_{b}") for b in range(8)} + iota = {b: V(f"iota_{b}") for b in range(8)} + + def hw16(lo, hi): # 16-bit from (low byte, high byte) + return Concat(hi, lo) + + def byte_op_operand(field_expr16): + # ByteAlu operand contract: field value must be a byte. + C.append(field_expr16 <= BitVecVal(255, 16)) + return Extract(7, 0, field_expr16) + + # === theta: Cxz XOR chain === rs:539-588 + for x in range(5): + for b in range(8): + C.append(cxz[(x, 0, b)] == start[(x, 0, b)] ^ start[(x, 1, b)]) + for s in range(1, 4): + yy = s + 1 + for b in range(8): + C.append(cxz[(x, s, b)] == cxz[(x, s - 1, b)] ^ start[(x, yy, b)]) + + # === theta: HWSL rotate-C-by-1 === rs:593-631 (+ eval IS_BIT rs:914-924) + for x in range(5): + for hw in range(4): + inp = hw16(cxz[(x, 3, 2 * hw)], cxz[(x, 3, 2 * hw + 1)]) + left16 = inp << 1 + C.append(hw16(cxzL[(x, 2 * hw)], cxzL[(x, 2 * hw + 1)]) == left16) + if bug != "drop_hwsl_carry": + C.append(cxzR[(x, hw)] == ZeroExt(7, Extract(15, 15, inp))) # carry bit + # REMOVAL DEMO drop_hwsl_carry: no Hwsl lookup pins the carry — + # only the IS_BIT eval constraint below survives (carry forgeable). + C.append(Or(cxzR[(x, hw)] == 0, cxzR[(x, hw)] == 1)) # IS_BIT (redundant) + + def rotated_c(xp, b): # rs:322-329 / 663-672 + hw = cxz_right_bit_for_byte(b) + expr = ZeroExt(8, cxzL[(xp, b)]) + if hw is not None: + expr = expr + ZeroExt(8, cxzR[(xp, hw)]) + return byte_op_operand(expr) + + # === theta: Dxz XOR === rs:661-690 + for x in range(5): + for b in range(8): + cm1 = cxz[((x + 4) % 5, 3, b)] + if bug == "theta_no_rot": + rc1 = cxz[((x + 1) % 5, 3, b)] # drop rotate + else: + rc1 = rotated_c((x + 1) % 5, b) + C.append(dxz[(x, b)] == cm1 ^ rc1) + + # === theta final XOR === rs:694-717 + for x in range(5): + for y in range(5): + for b in range(8): + C.append(theta[(x, y, b)] == start[(x, y, b)] ^ dxz[(x, b)]) + + # === rho: HWSL === rs:723-766 + rho_tbl = [[RHO[x][y] for y in range(5)] for x in range(5)] + if bug == "rho_swap": + rho_tbl[1][0], rho_tbl[2][0] = rho_tbl[2][0], rho_tbl[1][0] + if bug == "rho_off_by_one": + rho_tbl[3][2] += 1 # one lane's shift amount off by 1 + for x in range(5): + for y in range(5): + rnc = rho_tbl[x][y] % 16 + for hw in range(4): + inp = hw16(theta[(x, y, 2 * hw)], theta[(x, y, 2 * hw + 1)]) + left16 = inp << rnc + C.append(hw16(rotL[(x, y, 2 * hw)], rotL[(x, y, 2 * hw + 1)]) == left16) + if rnc == 0: + C.append(rotR[(x, y, 2 * hw)] == 0) + C.append(rotR[(x, y, 2 * hw + 1)] == 0) + else: + right16 = LShR(inp, 16 - rnc) + C.append(hw16(rotR[(x, y, 2 * hw)], rotR[(x, y, 2 * hw + 1)]) == right16) + + def pi(X, Y, z): # rs:793-795 virtual pi + sx, sy, l, r = pi_src(X, Y, z) + return byte_op_operand(ZeroExt(8, rotL[(sx, sy, l)]) + ZeroExt(8, rotR[(sx, sy, r)])) + + # === chi: AND then XOR === rs:796-870 + for x in range(5): + for y in range(5): + for b in range(8): + if bug == "drop_chi_xor_byte" and (x, y, b) == (2, 3, 5): + continue # REMOVAL DEMO: this output byte's defining equations gone + p0 = pi(x, y, b) + p1 = pi((x + 1) % 5, y, b) + p2 = pi((x + 2) % 5, y, b) + if bug == "chi_no_not": + C.append(chA[(x, y, b)] == (p1 & p2)) + elif bug == "chi_swap": + C.append(chA[(x, y, b)] == ((BitVecVal(255, 8) - p2) & p1)) + else: + C.append(chA[(x, y, b)] == ((BitVecVal(255, 8) - p1) & p2)) + C.append(chi[(x, y, b)] == p0 ^ chA[(x, y, b)]) + + # === iota === rs:872-894 (rc pinned by KeccakRc contract rs:518-535) + rc_round = (round_idx + 1) % 24 if bug == "iota_wrong_rc" else round_idx + rc_bytes = [(RC[rc_round] >> (8 * b)) & 0xFF for b in range(8)] + for b in range(8): + C.append(rc[b] == BitVecVal(rc_bytes[b], 8)) + if bug == "iota_no_rc": + C.append(iota[b] == chi[(0, 0, b)]) + else: + C.append(iota[b] == chi[(0, 0, b)] ^ rc[b]) + + def out_byte(x, y, b): # rs:496-509 handoff + return iota[b] if (x == 0 and y == 0) else chi[(x, y, b)] + + return C, out_byte, start + + +# -------------------------------------------------------------------------- +def check_round(round_idx, bug=None): + tag = f"r{round_idx}" + (f"_{bug}" if bug else "") + C, out_byte, start = build_circuit(round_idx, tag, bug=bug) + + # symbolic input lanes from the SAME free start bytes + lanes = [[Concat(*[start[(x, y, b)] for b in reversed(range(8))]) for y in range(5)] + for x in range(5)] + ref = zref_round(lanes, RC[round_idx]) + ref_byte = lambda x, y, b: Extract(8 * b + 7, 8 * b, ref[x][y]) + + s = Solver() + s.add(And(*C)) + # counterexample: circuit output differs from reference somewhere + s.add(Or(*[out_byte(x, y, b) != ref_byte(x, y, b) + for x in range(5) for y in range(5) for b in range(8)])) + return s.check() + + +def positive_control(round_idx, seed): + # Non-vacuity: fix start to concrete bytes, solve the constraint system + # (no diff assertion), confirm SAT and that the pinned output == reference. + import random + rng = random.Random(seed) + tag = f"pos{round_idx}" + C, out_byte, start = build_circuit(round_idx, tag) + s = Solver() + s.add(And(*C)) + concrete = {} + for x in range(5): + for y in range(5): + for b in range(8): + v = rng.randrange(0, 256) + concrete[(x, y, b)] = v + s.add(start[(x, y, b)] == v) + if s.check() != sat: + return False, "constraint system UNSAT for a concrete input (VACUOUS!)" + m = s.model() + # reference from concrete input + 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): + in_lanes[x + 5 * y] = sum(concrete[(x, y, b)] << (8 * b) for b in range(8)) + exp = keccak_round(in_lanes, RC[round_idx]) + for x in range(5): + for y in range(5): + got = sum(int(str(m.evaluate(out_byte(x, y, b)))) << (8 * b) for b in range(8)) + if got != exp[x + 5 * y]: + return False, f"pinned output != reference at lane ({x},{y})" + return True, "output uniquely pinned to reference" + + +if __name__ == "__main__": + bugs = ["theta_no_rot", "rho_swap", "chi_no_not", "chi_swap", "iota_no_rc"] + + print("=== POSITIVE CONTROL (non-vacuity): constraints SAT & pin output ===") + ok, msg = positive_control(5, seed=1) + print(f" round 5: {ok} ({msg})") + assert ok + + print("\n=== NEGATIVE CONTROLS (round 1): each buggy model must be SAT ===") + for bug in bugs: + r = check_round(1, bug=bug) + print(f" bug={bug:14s} -> {r} (want sat)") + assert r == sat, f"VACUOUS ENCODING: buggy model {bug} returned {r}" + + print("\n=== MAIN CHECK: clean model, all 24 rounds must be UNSAT ===") + allunsat = True + for r in range(24): + res = check_round(r) + allunsat &= (res == unsat) + print(f" round {r:2d} -> {res}") + if res != unsat: + print(" !!! COUNTEREXAMPLE FOUND — investigate") + print() + if allunsat: + print("VERDICT: all 24 rounds UNSAT + all negative controls SAT + positive control OK") + print("=> keccak_rnd round is provably correct GIVEN the chip contracts.") + else: + print("VERDICT: at least one round SAT — see above.") + sys.exit(1) From 76ea1e11e840830f0767fad2e40a7e52c5b3ecc4 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 11 Aug 2026 11:51:13 -0300 Subject: [PATCH 2/3] refactor(formal-verification): move the keccak gate to top-level formal_verification/ thoughts/ is not a real home in this repo. The z3/QF-BV gates live under formal_verification//, one directory per verified chip, so the next gates (blake3, sha2, the sponge) land beside this one. --- .../keccak/README.md | 2 +- .../keccak/keccak_ref.py | 0 .../keccak/model_dataflow.py | 0 .../formal-verification => formal_verification}/keccak/par.log | 0 .../keccak/tamper_test.py | 0 .../keccak/test_dataflow.py | 0 .../keccak/test_ref.py | 0 .../keccak/z3_parallel.py | 0 .../keccak/z3_verify.py | 0 9 files changed, 1 insertion(+), 1 deletion(-) rename {thoughts/formal-verification => formal_verification}/keccak/README.md (99%) rename {thoughts/formal-verification => formal_verification}/keccak/keccak_ref.py (100%) rename {thoughts/formal-verification => formal_verification}/keccak/model_dataflow.py (100%) rename {thoughts/formal-verification => formal_verification}/keccak/par.log (100%) rename {thoughts/formal-verification => formal_verification}/keccak/tamper_test.py (100%) rename {thoughts/formal-verification => formal_verification}/keccak/test_dataflow.py (100%) rename {thoughts/formal-verification => formal_verification}/keccak/test_ref.py (100%) rename {thoughts/formal-verification => formal_verification}/keccak/z3_parallel.py (100%) rename {thoughts/formal-verification => formal_verification}/keccak/z3_verify.py (100%) diff --git a/thoughts/formal-verification/keccak/README.md b/formal_verification/keccak/README.md similarity index 99% rename from thoughts/formal-verification/keccak/README.md rename to formal_verification/keccak/README.md index b540f7469..b22c352ae 100644 --- a/thoughts/formal-verification/keccak/README.md +++ b/formal_verification/keccak/README.md @@ -179,7 +179,7 @@ z3's Python bindings are the only dependency (no cargo, no repo build): ``` pip install z3-solver # if not already importable -cd thoughts/formal-verification/keccak +cd formal_verification/keccak python3 test_ref.py # reference constants + SHA3 vs hashlib python3 test_dataflow.py # concrete mirror vs reference (+ bug sanity) python3 z3_parallel.py # the gate: 24 rounds + controls (see par.log) diff --git a/thoughts/formal-verification/keccak/keccak_ref.py b/formal_verification/keccak/keccak_ref.py similarity index 100% rename from thoughts/formal-verification/keccak/keccak_ref.py rename to formal_verification/keccak/keccak_ref.py diff --git a/thoughts/formal-verification/keccak/model_dataflow.py b/formal_verification/keccak/model_dataflow.py similarity index 100% rename from thoughts/formal-verification/keccak/model_dataflow.py rename to formal_verification/keccak/model_dataflow.py diff --git a/thoughts/formal-verification/keccak/par.log b/formal_verification/keccak/par.log similarity index 100% rename from thoughts/formal-verification/keccak/par.log rename to formal_verification/keccak/par.log diff --git a/thoughts/formal-verification/keccak/tamper_test.py b/formal_verification/keccak/tamper_test.py similarity index 100% rename from thoughts/formal-verification/keccak/tamper_test.py rename to formal_verification/keccak/tamper_test.py diff --git a/thoughts/formal-verification/keccak/test_dataflow.py b/formal_verification/keccak/test_dataflow.py similarity index 100% rename from thoughts/formal-verification/keccak/test_dataflow.py rename to formal_verification/keccak/test_dataflow.py diff --git a/thoughts/formal-verification/keccak/test_ref.py b/formal_verification/keccak/test_ref.py similarity index 100% rename from thoughts/formal-verification/keccak/test_ref.py rename to formal_verification/keccak/test_ref.py diff --git a/thoughts/formal-verification/keccak/z3_parallel.py b/formal_verification/keccak/z3_parallel.py similarity index 100% rename from thoughts/formal-verification/keccak/z3_parallel.py rename to formal_verification/keccak/z3_parallel.py diff --git a/thoughts/formal-verification/keccak/z3_verify.py b/formal_verification/keccak/z3_verify.py similarity index 100% rename from thoughts/formal-verification/keccak/z3_verify.py rename to formal_verification/keccak/z3_verify.py From cea5474e0d56adfaf771da710c4cecd7f80f2917 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 11 Aug 2026 13:48:02 -0300 Subject: [PATCH 3/3] feat(loc): report formal_verification/ lines as a standalone section MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The daily loc report only counts Rust, so the formal-verification harnesses (python/z3 today, possibly Lean or SMT later) were invisible. Count formal_verification/ per gate directory across all languages tokei recognizes and report it as its own section — excluded from the total and the crates walk — in the json/slack/github/shell outputs. --- tooling/loc/src/main.rs | 45 ++++++++++++++- tooling/loc/src/report.rs | 115 ++++++++++++++++++++++++++++++++++++-- 2 files changed, 153 insertions(+), 7 deletions(-) diff --git a/tooling/loc/src/main.rs b/tooling/loc/src/main.rs index c85527042..9ddde31a3 100644 --- a/tooling/loc/src/main.rs +++ b/tooling/loc/src/main.rs @@ -21,10 +21,13 @@ const EXCLUDED: &[&str] = &[ "*fuzz*", "*programs*", "*program_artifacts*", + // Formal-verification harnesses (z3/QF-BV gates, …): not Rust, not part of + // the zkVM itself — counted as their own standalone report section. + "formal_verification", ]; /// Directories counted separately (not as crates). -const CRATE_SKIPPED: &[&str] = &["tooling", "bin"]; +const CRATE_SKIPPED: &[&str] = &["tooling", "bin", "formal_verification"]; fn count_crates_loc(crates_path: &PathBuf, config: &Config) -> Vec<(String, usize)> { let top_level_crate_dirs = std::fs::read_dir(crates_path) @@ -98,6 +101,42 @@ fn count_tools_loc(bin_path: &PathBuf, config: &Config) -> Vec<(String, usize)> tools_loc } +fn count_formal_verification_loc(fv_path: &PathBuf, config: &Config) -> Vec<(String, usize)> { + if !fv_path.exists() { + return Vec::new(); + } + + let gate_dirs = std::fs::read_dir(fv_path) + .unwrap() + .filter_map(|e| e.ok()) + .collect::>(); + + let mut fv_loc: Vec<(String, usize)> = gate_dirs + .into_iter() + .filter_map(|gate_dir_entry| { + let gate_path = gate_dir_entry.path(); + + // Only count directories (one per verified chip/gate) + if !gate_path.is_dir() { + return None; + } + + let gate_name = gate_path.file_name().unwrap().to_str().unwrap().to_owned(); + + // The harnesses are not Rust (python/z3 today, possibly Lean or SMT + // later), so sum code lines across every language tokei recognizes. + let mut languages = Languages::new(); + languages.get_statistics(&[gate_path], &[], config); + let gate_loc: usize = languages.values().map(|language| language.code).sum(); + (gate_loc > 0).then_some((gate_name, gate_loc)) + }) + .collect(); + + fv_loc.sort_by_key(|(_gate_name, loc)| *loc); + fv_loc.reverse(); + fv_loc +} + fn main() { let opts = LinesOfCodeReporterOptions::parse(); @@ -110,11 +149,14 @@ fn main() { .unwrap(); let repo_crates_path = repo_path.join(""); // TODO: change to "crates" when crates directory exists let repo_bin_path = repo_path.join("bin"); + let repo_formal_verification_path = repo_path.join("formal_verification"); let config = Config::default(); let lambda_vm_loc = count_loc(repo_path.clone(), &config).unwrap(); let crates_loc = count_crates_loc(&repo_crates_path, &config); let tools_loc = count_tools_loc(&repo_bin_path, &config); + let formal_verification_loc = + count_formal_verification_loc(&repo_formal_verification_path, &config); spinner.success("Lines of code calculated!"); @@ -124,6 +166,7 @@ fn main() { lambda_vm: lambda_vm_loc.code, crates: crates_loc, tools: tools_loc, + formal_verification: formal_verification_loc, }; if opts.detailed { diff --git a/tooling/loc/src/report.rs b/tooling/loc/src/report.rs index 288506d4f..6fa8a488a 100644 --- a/tooling/loc/src/report.rs +++ b/tooling/loc/src/report.rs @@ -21,6 +21,8 @@ pub struct LinesOfCodeReport { pub crates: Vec<(String, usize)>, #[serde(default)] pub tools: Vec<(String, usize)>, + #[serde(default)] + pub formal_verification: Vec<(String, usize)>, } pub fn pr_message( @@ -195,6 +197,32 @@ pub fn slack_message(old_report: LinesOfCodeReport, new_report: LinesOfCodeRepor ) }); + let formal_verification_mrkdwn = + new_report + .formal_verification + .iter() + .fold(String::new(), |acc, (gate_name, loc)| { + let old_loc = old_report + .formal_verification + .iter() + .find(|(old_gate_name, _)| old_gate_name == gate_name) + .map(|(_, old_loc)| old_loc) + .unwrap_or(&0); + + let loc_diff = loc.abs_diff(*old_loc); + format!( + "{}*{}*: {} {}\\n", + acc, + gate_name, + loc, + match loc.cmp(old_loc) { + std::cmp::Ordering::Greater => format!("(+{loc_diff})"), + std::cmp::Ordering::Less => format!("(-{loc_diff})"), + std::cmp::Ordering::Equal => "".to_string(), + } + ) + }); + let tools_block = if !new_report.tools.is_empty() { format!( r#", @@ -218,6 +246,29 @@ pub fn slack_message(old_report: LinesOfCodeReport, new_report: LinesOfCodeRepor String::new() }; + let formal_verification_block = if !new_report.formal_verification.is_empty() { + format!( + r#", + {{ + "type": "header", + "text": {{ + "type": "plain_text", + "text": "Formal Verification" + }} + }}, + {{ + "type": "section", + "text": {{ + "type": "mrkdwn", + "text": "{}" + }} + }}"#, + formal_verification_mrkdwn + ) + } else { + String::new() + }; + format!( r#"{{ "blocks": [ @@ -258,7 +309,7 @@ pub fn slack_message(old_report: LinesOfCodeReport, new_report: LinesOfCodeRepor "type": "mrkdwn", "text": "{}" }} - }}{} + }}{}{} ] }}"#, new_report.lambda_vm, @@ -268,7 +319,8 @@ pub fn slack_message(old_report: LinesOfCodeReport, new_report: LinesOfCodeRepor std::cmp::Ordering::Equal => "".to_string(), }, crates_mrkdwn, - tools_block + tools_block, + formal_verification_block ) } @@ -330,6 +382,40 @@ pub fn github_step_summary(old_report: LinesOfCodeReport, new_report: LinesOfCod String::new() }; + let formal_verification_github = if !new_report.formal_verification.is_empty() { + let formal_verification_list = + new_report + .formal_verification + .iter() + .fold(String::new(), |acc, (gate_name, loc)| { + let old_loc = old_report + .formal_verification + .iter() + .find(|(old_gate_name, _)| old_gate_name == gate_name) + .map(|(_, old_loc)| old_loc) + .unwrap_or(&0); + + let loc_diff = loc.abs_diff(*old_loc); + format!( + "{}{}: {} {}\n", + acc, + gate_name, + loc, + match loc.cmp(old_loc) { + std::cmp::Ordering::Greater => format!("(+{loc_diff})"), + std::cmp::Ordering::Less => format!("(-{loc_diff})"), + std::cmp::Ordering::Equal => "".to_string(), + } + ) + }); + format!( + "\nlambda_vm formal verification loc (standalone)\n=================\n{}", + formal_verification_list + ) + } else { + String::new() + }; + format!( r#"``` lambda_vm loc summary @@ -338,7 +424,7 @@ lambda_vm (total): {} {} lambda_vm crates loc ================= -{}{} +{}{}{} ```"#, new_report.lambda_vm, if new_report.lambda_vm > old_report.lambda_vm { @@ -347,7 +433,8 @@ lambda_vm crates loc format!("(-{diff_total})") }, crates_github, - tools_github + tools_github, + formal_verification_github ) } @@ -367,8 +454,23 @@ pub fn shell_summary(new_report: LinesOfCodeReport) -> String { String::new() }; + let formal_verification_line = if !new_report.formal_verification.is_empty() { + format!( + "\n{} {}", + "formal verification:".bold(), + new_report + .formal_verification + .iter() + .map(|(name, loc)| format!("{}: {}", name, loc)) + .collect::>() + .join(", ") + ) + } else { + String::new() + }; + format!( - "{}\n{}\n{} {}\n{} {}{}", + "{}\n{}\n{} {}\n{} {}{}{}", "Lines of Code".bold(), "=============".bold(), "lambda_vm (total):".bold(), @@ -380,6 +482,7 @@ pub fn shell_summary(new_report: LinesOfCodeReport) -> String { .map(|(name, loc)| format!("{}: {}", name, loc)) .collect::>() .join(", "), - tools_line + tools_line, + formal_verification_line ) }