From f8c1d28b308c9700362c63a13e877114a885e968 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Wed, 2 Sep 2026 12:03:55 -0300 Subject: [PATCH 01/15] Cite the keccak gate's constructs by name --- formal_verification/keccak/model_dataflow.py | 37 ++++++++++---------- formal_verification/keccak/test_ref.py | 3 +- formal_verification/keccak/z3_verify.py | 29 ++++++++------- 3 files changed, 38 insertions(+), 31 deletions(-) diff --git a/formal_verification/keccak/model_dataflow.py b/formal_verification/keccak/model_dataflow.py index 9579a787b..238cf1b6d 100644 --- a/formal_verification/keccak/model_dataflow.py +++ b/formal_verification/keccak/model_dataflow.py @@ -8,7 +8,8 @@ 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. +Citations name the construct (banner title or cols::/KeccakRndConstraints +symbol) in prover/src/tables/keccak_rnd.rs, never a line number. """ from keccak_ref import RHO, RC @@ -22,12 +23,12 @@ def bytes_to_lane(bs): def cxz_right_bit_for_byte(b): - # keccak_rnd.rs:126-132 -> even b: Some((b/2 + 3)%4); odd: None + # cols::cxz_right_bit_for_byte -> 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 + # cols::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 @@ -49,29 +50,29 @@ def round_dataflow(start_lanes, r, bug=None): 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 + # === theta: Cxz XOR chain === banner "Theta: Cxz chain BYTE_ALU[XOR] (160)" 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 + cxz[x][0][b] = S[x][0][b] ^ S[x][1][b] # stage 0 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 + cxz[x][stage][b] = cxz[x][stage - 1][b] ^ S[x][y][b] # stages 1..3 - # === theta: HWSL rotate-C-by-1 === keccak_rnd.rs:593-631 + # === theta: HWSL rotate-C-by-1 === KeccakRndConstraints::eval, group (2) 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 + Chw = cxz[x][3][2 * hw] | (cxz[x][3][2 * hw + 1] << 8) # input halfword + left16 = (Chw << 1) & 0xFFFF # 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 + cxz_right[x][hw] = (Chw >> 15) & 1 # carry bit def rotated_c(xp, b): - # keccak_rnd.rs:322-329 / 663-672 reconstruction + # banner "Theta: Dxz BYTE_ALU[XOR] (40)" reconstruction contrib = 0 hw = cxz_right_bit_for_byte(b) if hw is not None: @@ -80,7 +81,7 @@ def rotated_c(xp, b): assert val <= 255, "rotated_C operand exceeds a byte" return val - # === theta: Dxz XOR === keccak_rnd.rs:661-690 + # === theta: Dxz XOR === banner "Theta: Dxz BYTE_ALU[XOR] (40)" Dxz = [[0] * 8 for _ in range(5)] for x in range(5): for b in range(8): @@ -90,14 +91,14 @@ def rotated_c(xp, b): rc1 = cxz[(x + 1) % 5][3][b] # drop the rotate Dxz[x][b] = cm1 ^ rc1 - # === theta final XOR === keccak_rnd.rs:694-717 + # === theta final XOR === banner "Theta final: BYTE_ALU[XOR] (200)" 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: HWSL === KeccakRndConstraints::eval, group (3) 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] @@ -116,13 +117,13 @@ def rotated_c(xp, b): 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] + # cols::pi_src_cols; 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: AND then XOR === banners "Chi: BYTE_ALU[AND] (200)" + [XOR] chi = [[[0] * 8 for _ in range(5)] for _ in range(5)] for x in range(5): for y in range(5): @@ -138,7 +139,7 @@ def pi(X, Y, z): ands = (0xFF - p1) & p2 # (255 - pi[x+1]) AND pi[x+2] chi[x][y][b] = p0 ^ ands - # === iota === keccak_rnd.rs:872-894 + # === iota === banner "Iota: BYTE_ALU[XOR] (8)" rc_bytes = lane_to_bytes(RC[r]) iota = [0] * 8 for b in range(8): @@ -147,7 +148,7 @@ def pi(X, Y, z): else: iota[b] = chi[0][0][b] ^ rc_bytes[b] - # === output handoff === keccak_rnd.rs:496-509 + # === output handoff === banner "IO group (3)", the KECCAK bus send out = [0] * 25 for x in range(5): for y in range(5): diff --git a/formal_verification/keccak/test_ref.py b/formal_verification/keccak/test_ref.py index 0f80d6eac..26a687fcb 100644 --- a/formal_verification/keccak/test_ref.py +++ b/formal_verification/keccak/test_ref.py @@ -2,7 +2,8 @@ import hashlib from keccak_ref import RC, RHO, sha3_256 -# Repo constants (from executor/src/vm/instruction/execution.rs:646-680), pasted +# Repo constants (KECCAK_RC / KECCAK_RHO in +# executor/src/vm/instruction/execution.rs), pasted # here ONLY to cross-check my spec-generated values. Correctness is anchored to # FIPS-202 (my generators) + hashlib, not to these. REPO_RC = [ diff --git a/formal_verification/keccak/z3_verify.py b/formal_verification/keccak/z3_verify.py index 220b9fe31..8ab9c7353 100644 --- a/formal_verification/keccak/z3_verify.py +++ b/formal_verification/keccak/z3_verify.py @@ -34,10 +34,10 @@ # -------------------------------------------------------------------------- # byte<->column helpers mirroring keccak_rnd.rs::cols # -------------------------------------------------------------------------- -def cxz_right_bit_for_byte(b): # rs:126-132 +def cxz_right_bit_for_byte(b): # cols::cxz_right_bit_for_byte return (b // 2 + 3) % 4 if b % 2 == 0 else None -def pi_src(X, Y, z): # rs:161-174 +def pi_src(X, Y, z): # cols::pi_src_cols sx = (X + 3 * Y) % 5 sy = X rbc = RHO[sx][sy] // 16 @@ -111,7 +111,7 @@ def byte_op_operand(field_expr16): C.append(ULE(field_expr16, BitVecVal(255, 16))) return Extract(7, 0, field_expr16) - # === theta: Cxz XOR chain === rs:539-588 + # === theta: Cxz XOR chain === banner "Theta: Cxz chain BYTE_ALU[XOR] (160)" for x in range(5): for b in range(8): C.append(cxz[(x, 0, b)] == start[(x, 0, b)] ^ start[(x, 1, b)]) @@ -120,7 +120,9 @@ def byte_op_operand(field_expr16): 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) + # === theta: HWSL rotate-C-by-1 === KeccakRndConstraints::eval, group (2) + # (the theta shift identity; group (1) is the IS_BIT on the carry). #889 + # deleted the BusId::Hwsl sender this used to name. for x in range(5): for hw in range(4): inp = hw16(cxz[(x, 3, 2 * hw)], cxz[(x, 3, 2 * hw + 1)]) @@ -132,14 +134,14 @@ def byte_op_operand(field_expr16): # 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 + def rotated_c(xp, b): # banner "Theta: Dxz BYTE_ALU[XOR] (40)" 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 + # === theta: Dxz XOR === banner "Theta: Dxz BYTE_ALU[XOR] (40)" for x in range(5): for b in range(8): cm1 = cxz[((x + 4) % 5, 3, b)] @@ -149,13 +151,14 @@ def rotated_c(xp, b): # rs:322-329 / 663-672 rc1 = rotated_c((x + 1) % 5, b) C.append(dxz[(x, b)] == cm1 ^ rc1) - # === theta final XOR === rs:694-717 + # === theta final XOR === banner "Theta final: BYTE_ALU[XOR] (200)" 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: HWSL === KeccakRndConstraints::eval, group (3) (the rho shift + # identity; #889 deleted the BusId::Hwsl sender this used to name) 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] @@ -175,11 +178,12 @@ def rotated_c(xp, b): # rs:322-329 / 663-672 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 + def pi(X, Y, z): # cols::pi_src_cols (pi is spec-virtual) 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 + # === chi: AND then XOR === banners "Chi: BYTE_ALU[AND] (200)" + + # "Chi: BYTE_ALU[XOR] (200)" for x in range(5): for y in range(5): for b in range(8): @@ -196,7 +200,8 @@ def pi(X, Y, z): # rs:793-795 virtual pi 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) + # === iota === banner "Iota: BYTE_ALU[XOR] (8)" (rc pinned by the KeccakRc + # sender in banner "IO group (3)") 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): @@ -206,7 +211,7 @@ def pi(X, Y, z): # rs:793-795 virtual pi else: C.append(iota[b] == chi[(0, 0, b)] ^ rc[b]) - def out_byte(x, y, b): # rs:496-509 handoff + def out_byte(x, y, b): # KECCAK bus send, banner "IO group (3)" return iota[b] if (x == 0 and y == 0) else chi[(x, y, b)] return C, out_byte, start From a6f6ce496b873e9404a43c31bd654704217104f7 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Wed, 2 Sep 2026 12:04:15 -0300 Subject: [PATCH 02/15] Drop the README's stale-citation catalogue --- formal_verification/keccak/README.md | 33 +++++++++++++--------------- 1 file changed, 15 insertions(+), 18 deletions(-) diff --git a/formal_verification/keccak/README.md b/formal_verification/keccak/README.md index 2cb7b579a..ed4f2a63d 100644 --- a/formal_verification/keccak/README.md +++ b/formal_verification/keccak/README.md @@ -80,8 +80,9 @@ Each helper lookup is modeled by its contract, not its implementation: declaring those variables 8-bit bitvectors, and the θ carry `Cxz_right` is pinned directly to `ZeroExt(7, Extract(15, 15, in))`, with the separate `IS_BIT` disjunct redundant *in the model*. Both are `load-bearing` in the circuit - (`keccak_rnd.rs:7-8`, `:840-842`: the 20 μ-gated `IS_BIT`s make the θ shift - decomposition unique). Because neither can be removed from the model's constraint + (the `keccak_rnd.rs` module doc-comment and the `KeccakRndConstraints` + doc-comment: the 20 μ-gated `IS_BIT`s make the θ shift decomposition + unique). Because neither can be removed from the model's constraint list, **deleting them from the Rust leaves this gate printing `VERIFIED`** while the θ `left` halfwords go free — `2¹⁶` is invertible mod `p`, so the forged assignment exists. The model's pin is a sound *consequence* of the shipped @@ -141,22 +142,18 @@ constraint-identical in QF-BV. Verified: `keccak_rnd.rs` is byte-identical acros `main`, this branch, and `6a280121` (same git blob `51b7759f`), so the wiring the model transcribes is the shipped wiring. -The `rs:NNN` line citations in the code comments are nevertheless **stale**. They were -written against the pre-#889 revision (`d83b4d9e`, blob `1b121a8b`, 926 lines), where -each lands exactly on the construct it names; **#889 — the change that inlined the -HWSL shifts — invalidated them all.** Most now point at a neighbouring construct: -`rs:539-588` ("theta: Cxz XOR chain") is the KeccakRc sender, the chain being at -`546-597`; `rs:796-870` ("chi: AND then XOR") is Iota, Chi's AND/XOR being at -`716-759` and `761-794`. - -Two cannot be repointed at all: `rs:593-631` (θ HWSL) and `rs:723-766` (ρ HWSL) cite -`BusInteraction::sender(BusId::Hwsl, …)` blocks that #889 **deleted outright** — the -file now contains zero `BusId::Hwsl` sends, and that content lives in the inline -identities at `:882-894` and `:896-920`. So it is not the case that every referenced -construct still exists. - -Locate a construct by its `// --- Step: … ---` banner rather than by these line -numbers. +The code comments cite each modeled equation by **construct name** — the +`// --- : () ---` banner it sits under, or the `cols::` / +`KeccakRndConstraints` symbol — never by line number. Names are the only citation +that survives: line numbers rot from churn with nothing to do with the chip. The +earlier `rs:NNN` citations were all invalidated by **#889** (which inlined the HWSL +shifts), two of them naming `BusInteraction::sender(BusId::Hwsl, …)` blocks that +#889 **deleted outright** — the file now contains zero `BusId::Hwsl` sends, and that +content lives in the inline identities in `KeccakRndConstraints`. The `execution.rs` +citation in `test_ref.py` was broken separately, by **#876** (an unrelated hint-ecall +PR) merely growing the file by 136 lines. + +If you copy this template, cite by name for the same reason. **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 From 3051bbf1b20cdd8dcad758674b8bcf84e858ed34 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Wed, 2 Sep 2026 16:21:09 -0300 Subject: [PATCH 03/15] Decide which keccak range checks are needed --- formal_verification/keccak/combinatorics.py | 65 ++++++++++ formal_verification/keccak/field_model.py | 107 ++++++++++++++++ formal_verification/keccak/necessity_rho.py | 117 ++++++++++++++++++ formal_verification/keccak/necessity_theta.py | 116 +++++++++++++++++ 4 files changed, 405 insertions(+) create mode 100644 formal_verification/keccak/combinatorics.py create mode 100644 formal_verification/keccak/field_model.py create mode 100644 formal_verification/keccak/necessity_rho.py create mode 100644 formal_verification/keccak/necessity_theta.py diff --git a/formal_verification/keccak/combinatorics.py b/formal_verification/keccak/combinatorics.py new file mode 100644 index 000000000..a31bbbdf4 --- /dev/null +++ b/formal_verification/keccak/combinatorics.py @@ -0,0 +1,65 @@ +""" +The pure-combinatorial premises the rho necessity argument rests on. + +No solver: these are facts about cols::pi_src_cols and KECCAK_RHO that must hold +before any claim about "this range check is implied by the pi operand" can mean +anything. If any of them breaks, necessity_rho.py's config-B result is void. +""" +from keccak_ref import RHO +from field_model import rho_pi_offsets + +FAIL = [] + + +def check(cond, msg): + print(f" {'OK ' if cond else 'FALLA'} {msg}") + if not cond: + FAIL.append(msg) + + +print("=== (1) pi is a bijection on the 25 lanes ===") +src_of = {(X, Y): ((X + 3 * Y) % 5, X) for X in range(5) for Y in range(5)} +images = list(src_of.values()) +check(len(set(images)) == 25, f"(X,Y) -> ((X+3Y)%5, X) covers {len(set(images))}/25 source lanes, no repeats") + +print("\n=== (2) every source lane is read by exactly one output lane, via 8 bytes ===") +readers = {} +for (X, Y), src in src_of.items(): + readers.setdefault(src, []).append((X, Y)) +check(all(len(v) == 1 for v in readers.values()), + "each source lane has exactly one reader lane") + +print("\n=== (3) every rot_left and rot_right byte column is read EXACTLY once ===") +bad = [] +for src, ((X, Y),) in ((s, tuple(r)) for s, r in readers.items()): + a = rho_pi_offsets(RHO[src[0]][src[1]] // 16) + left_hits = [0] * 8 + right_hits = [0] * 8 + for z in range(8): + left_hits[(z + a) % 8] += 1 + right_hits[(z + a - 2) % 8] += 1 + if left_hits != [1] * 8 or right_hits != [1] * 8: + bad.append((src, left_hits, right_hits)) +check(not bad, f"400/400 byte columns read exactly once (none zero times, none twice){'' if not bad else f' — {bad[:2]}'}") + +print("\n=== (4) the pi byte offsets are EVEN, so a pi halfword reads one source halfword ===") +odd = [(x, y) for x in range(5) for y in range(5) if rho_pi_offsets(RHO[x][y] // 16) % 2] +check(not odd, "a in {0,6,4,2} is always even -> P_h = L_(h+A) + R_(h+A-1), A = a/2") +mism = [] +for x in range(5): + for y in range(5): + a = rho_pi_offsets(RHO[x][y] // 16) + A = a // 2 + for h in range(4): + if ((2 * h + a) % 8) // 2 != (h + A) % 4 or ((2 * h + a - 2) % 8) // 2 != (h + A - 1) % 4: + mism.append((x, y, h)) +check(not mism, "the packed relation verified for all 25 lanes x 4 halfwords") + +print("\n=== (5) theta = all-ones saturates every pi halfword, for EVERY rotation ===") +# left + right = 0xFFFF whatever rnc is, which is why config C forges on all 25. +sat = all(((0xFFFF << (RHO[x][y] % 16)) & 0xFFFF) + (0xFFFF >> (16 - (RHO[x][y] % 16)) + if RHO[x][y] % 16 else 0) == 0xFFFF for x in range(5) for y in range(5)) +check(sat, "left + right = 0xFFFF for all 25 lanes -> pi = 0xFF..FF, the saturation config C needs") + +assert not FAIL, FAIL +print("\nALL COMBINATORIAL PREMISES HOLD") diff --git a/formal_verification/keccak/field_model.py b/formal_verification/keccak/field_model.py new file mode 100644 index 000000000..8ccdee2e8 --- /dev/null +++ b/formal_verification/keccak/field_model.py @@ -0,0 +1,107 @@ +""" +Shared integer-mod-`p` model of the inlined θ/ρ shift identities. + +WHY A SECOND MODEL. `z3_verify.py` proves the round wiring correct *given* the +byte bounds, and it structurally cannot ask whether those bounds are NEEDED: it +carries them as the WIDTH of its bitvectors, and in bitvector arithmetic `2**16` +is a zero divisor, so a widened model would wrongly keep the decomposition +pinned. Mod the Goldilocks prime `2**16` is invertible, which is exactly what +makes the question askable — and answerable. + +THE SHAPE OF THE QUESTION. Each shift is one identity per halfword, + + mu * (in * 2**rnc - right * 2**16 - left) = 0 (rnc = 1 for theta) + +over the field. One equation, two unknowns: for ANY `left` there is exactly one +`right = (in*2**rnc - left) * inv(2**16)`, so the identity alone pins nothing. +What pins it are the range checks on `left`/`right`. + +THE DIFFERENCE FORM (why no `% p` appears below). If `(L, R)` satisfies the +identity then so does `(L - 2**16 * d, R + d)` for any `d`, and those are the +ONLY other solutions. So instead of solving over the field we parameterise the +deviation directly by `d` per halfword. Every magnitude then stays under 2**18, +far below `p`, so the field equation and the integer equation coincide and the +whole analysis is exact integer arithmetic. The field enters in exactly one +place: a committed column may hold a NEGATIVE integer (as `p - k`), because +nothing bounds it once its range check is gone. `as_field` marks those. + +WHAT BOUNDS THE DEVIATION. Two things, and which one bites is the whole result: + * the range check on `left` (ARE_BYTES) confines `L' = L - 2**16*d` to + [0, 2**16), and any `d != 0` moves `L` by at least 2**16 -> `d = 0`; + * the downstream ByteAlu OPERAND that consumes the shift output. The BITWISE + table holds only byte rows, so the operand must be a byte, which leaves a + residual window on `left` even with no range check of its own. Whether + `d = +/-1` fits inside that window is what decides necessity. +""" + +P = 2**64 - 2**32 + 1 # Goldilocks +MASK16 = 0xFFFF + + +def as_field(v): + """A committed column holds `v` as a field element; negatives wrap to p-|v|.""" + return v % P + + +def pack(lo, hi): + """The halfword a (low byte, high byte) column pair denotes.""" + return lo + 256 * hi + + +def honest_shift(in_hw, rnc): + """The unique (left, right) the identity forces when both are byte-bounded. + + Euclidean division of `in_hw * 2**rnc` by `2**16`: right = quotient, + left = remainder. Valid for theta (rnc = 1) and every rho lane.""" + assert 0 <= in_hw <= MASK16 and 0 <= rnc < 16 + prod = in_hw << rnc + return prod & MASK16, prod >> 16 + + +def identity_holds(in_hw, rnc, left, right): + """The shipped constraint, evaluated over the field.""" + return (in_hw * (2**rnc) - right * (2**16) - left) % P == 0 + + +def deviate(left, right, d): + """The only other solution family: (L, R) -> (L - 2**16*d, R + d).""" + return left - (2**16) * d, right + d + + +# --- theta: rnc = 1, `right` is a single IS_BIT-pinned carry column ---------- +# The carry of halfword h lands on the LOW byte of halfword h+1 (cols:: +# cxz_right_bit_for_byte: even b -> (b/2 + 3) % 4), so within one x the four +# halfwords form a cycle of length 4. Odd bytes take no carry. +THETA_RNC = 1 + + +def theta_carry_source(h): + """Which halfword's carry is added to the low byte of halfword `h`.""" + return (h - 1) % 4 + + +def theta_operand_bytes(cxz_left, cxz_right): + """rotated_C[0..8): the ByteAlu operand the Dxz XOR consumes.""" + out = [] + for b in range(8): + v = cxz_left[b] + if b % 2 == 0: + v += cxz_right[theta_carry_source(b // 2)] + out.append(v) + return out + + +# --- rho: `right` is a byte pair, and pi pairs it with `left` ---------------- +def rho_pi_offsets(rbc): + """cols::pi_src_cols: l(z) = z + a mod 8, r(z) = z + a - 2 mod 8.""" + return [0, 6, 4, 2][rbc] + + +def rho_operand_bytes(rot_left, rot_right, rbc): + """pi[0..8) for the output lane that reads this source lane.""" + a = rho_pi_offsets(rbc) + return [rot_left[(z + a) % 8] + rot_right[(z + a - 2) % 8] for z in range(8)] + + +def is_byte(v): + return 0 <= v <= 255 diff --git a/formal_verification/keccak/necessity_rho.py b/formal_verification/keccak/necessity_rho.py new file mode 100644 index 000000000..3abfd79d6 --- /dev/null +++ b/formal_verification/keccak/necessity_rho.py @@ -0,0 +1,117 @@ +""" +Is each rho range check NECESSARY for the shipped inline identity? + +Shipped constraints (KeccakRndConstraints::eval group (3), plus the banner +"Rho: ARE_BYTES range checks on rot_left + rot_right (200 pairs)"): + + mu * (in*2**rnc - right*2**16 - left) = 0 100 identities, rnc = RHO[x][y] % 16 + ARE_BYTES(rot_left[x][y][b], rot_right[x][y][b]) 200 pairs + +Downstream, pi is virtual and is consumed as a ByteAlu OPERAND (banners +"Chi: BYTE_ALU[AND] (200)" and "Chi: BYTE_ALU[XOR] (200)"): + + pi[z] = rot_left[l(z)] + rot_right[r(z)] must be a byte + +Premises from combinatorics.py (run it first): the offsets are even, so a pi +halfword reads one source halfword as P_h = L_(h+A) + R_(h+A-1), and every one +of the 400 byte columns is read exactly once. + +RESULT, and it is asymmetric — unlike theta, here ONE check is load-bearing on +its own. `left` and `right` enter the identity with weights 1 and 2**16, so +bounding `left` kills the deviation while bounding `right` does not. +""" +from itertools import product +from keccak_ref import RHO +from field_model import (P, MASK16, as_field, honest_shift, identity_holds, + deviate, rho_pi_offsets, rho_operand_bytes, is_byte) + +FAIL = [] + + +def check(cond, msg): + print(f" {'OK ' if cond else 'FALLA'} {msg}") + if not cond: + FAIL.append(msg) + + +LANES = [(x, y) for x in range(5) for y in range(5)] + +print("=== A / B: left stays range-checked — d = 0 forced, on every lane ===") +# L' = L - 2**16*d with L, L' both in [0, 2**16) leaves no room for d != 0. This +# holds whatever `right` is allowed to be, so dropping rot_right's half of the +# pair changes nothing: its value is then recovered from the identity, uniquely, +# because 2**16 is invertible mod p. rot_right's check is IMPLIED. +check(2**16 > MASK16, "|2**16 * d| >= 2**16 > 65535 for d != 0 -> A and B sound for all 25 lanes") + +print("\n=== C: rot_left's check dropped — completeness of the search first ===") +# right stays in [0, 2**16), so d = right' - right has |d| <= 65535. And +# P'_h = P_h - 2**16*d_(h+A) + d_(h+A-1) in [0, 65535] with P_h in [0, 65535] +# forces |2**16*d_j - d_(j-1)| <= 65535, so |d_j| >= 2 would need +# |d_(j-1)| >= 2*2**16 - 65535 = 65537 > 65535. Hence |d_j| <= 1 for all j. +check(2 * 2**16 - MASK16 > MASK16, + f"|d| >= 2 would need a neighbour |d| >= {2 * 2**16 - MASK16} > {MASK16} -> d in {{-1,0,1}}, search complete") + +print("\n=== C: the forged witness, verified PER BYTE on every lane ===") +forged = 0 +for (sx, sy) in LANES: + rho = RHO[sx][sy] + rnc, rbc = rho % 16, rho // 16 + in_hws = [0xFFFF] * 4 # theta[sx][sy] = 0xFFFF...FF + honest = [honest_shift(i, rnc) for i in in_hws] + + # saturation: pi = 0xFF..FF, the only configuration d = +1 can survive + hon_left = [b for h in range(4) for b in (honest[h][0] & 0xFF, honest[h][0] >> 8)] + hon_right = [b for h in range(4) for b in (honest[h][1] & 0xFF, honest[h][1] >> 8)] + hon_pi = rho_operand_bytes(hon_left, hon_right, rbc) + + # forge with d = +1 on all four halfwords: right' = 2**rnc, and choose the + # byte split of left' so that every pi byte cancels to zero + dev = [deviate(honest[h][0], honest[h][1], 1) for h in range(4)] + frg_right = [b for h in range(4) for b in (dev[h][1] & 0xFF, dev[h][1] >> 8)] + frg_left = [-frg_right[(w - 2) % 8] for w in range(8)] + frg_pi = rho_operand_bytes(frg_left, frg_right, rbc) + + okid = all(identity_holds(in_hws[h], rnc, frg_left[2 * h] + 256 * frg_left[2 * h + 1], + frg_right[2 * h] + 256 * frg_right[2 * h + 1]) for h in range(4)) + good = (hon_pi == [0xFF] * 8 and okid and frg_pi == [0] * 8 + and all(is_byte(v) for v in frg_right) # rot_right stays byte-valued + and any(as_field(v) > 255 for v in frg_left)) # only rot_left goes out of range + forged += good + if (sx, sy) in ((0, 0), (2, 0), (4, 4)): + print(f" lane ({sx},{sy}) RHO={rho:2d} rnc={rnc:2d}: honest pi=0xFF*8 -> forged pi={frg_pi[:3]}..., " + f"rot_right bytes={all(is_byte(v) for v in frg_right)}, rot_left out-of-range={sum(as_field(v) > 255 for v in frg_left)}/8") +check(forged == 25, f"FORGEABLE on {forged}/25 lanes — rot_left's check is LOAD-BEARING") +print(" note this is strictly stronger than the spec's own witness: rot_right stays") +print(" byte-valued here, so only rot_left's check catches it.") + +print("\n=== D: both dropped — the lane's output is completely free ===") +# Eliminating left via the identity leaves a cyclic system in right: +# right'_(j-1) - 2**16 * right'_j = c_j, solvable because 1 - 2**64 is invertible. +INV = pow(1 - 2**64, -1, P) +free = 0 +for (sx, sy) in LANES: + rho = RHO[sx][sy] + rnc, rbc, a = rho % 16, rho // 16, rho_pi_offsets(rho // 16) + A = a // 2 + in_hws = [0x1234, 0xABCD, 0x0F0F, 0xFFFF] + target = [(7 * z + 3) % 256 for z in range(8)] # an arbitrary byte target + Q = [target[2 * h] + 256 * target[2 * h + 1] for h in range(4)] + c = [(Q[(j - A) % 4] - in_hws[j] * (2**rnc)) % P for j in range(4)] + r0 = ((c[1] + (2**16) * c[2] + (2**32) * c[3] + (2**48) * c[0]) * INV) % P + R = [0] * 4 + R[0] = r0 + for j in (1, 2, 3): + R[j] = ((R[j - 1] - c[(j + 1) % 4]) * pow(2**16, -1, P)) % P + L = [(in_hws[j] * (2**rnc) - (2**16) * R[j]) % P for j in range(4)] + okid = all(identity_holds(in_hws[j], rnc, L[j], R[j]) for j in range(4)) + free += okid +check(free == 25, f"the packed system is solvable for an arbitrary target on {free}/25 lanes " + f"(det = 1 - 2**64 = {(1 - 2**64) % P} mod p, invertible). Per-byte\n realizability is the construction exhibited in C.") + +print("\n=== VERDICT ===") +print(" A sound | B sound -> rot_right's check is IMPLIED by rot_left's + the pi operand") +print(" C FORGEABLE -> rot_left's check is LOAD-BEARING on its own") +print(" D output free -> the pair pins nothing without at least rot_left") +print(" Ceiling for any interaction saving is therefore 100 of 200, not 200.") +assert not FAIL, FAIL +print("\nALL RHO NECESSITY CHECKS PASSED") diff --git a/formal_verification/keccak/necessity_theta.py b/formal_verification/keccak/necessity_theta.py new file mode 100644 index 000000000..322309020 --- /dev/null +++ b/formal_verification/keccak/necessity_theta.py @@ -0,0 +1,116 @@ +""" +Is each theta range check NECESSARY for the shipped inline identity? + +Shipped constraints (KeccakRndConstraints::eval, groups (1) and (2), plus the +banner "Theta: ARE_BYTES range checks on Cxz_left (20 pairs)"): + + (i) mu * (in*2 - right*2**16 - left) = 0 20 identities + (ii) mu * right*(1 - right) = 0 20 IS_BIT on the carry + (iii) ARE_BYTES(Cxz_left[2i], Cxz_left[2i+1]) 20 pairs + +Downstream, rotated_C is a ByteAlu OPERAND (banner "Theta: Dxz BYTE_ALU[XOR] +(40)"), so it must be a byte: + + rotated_C[2h] = Cxz_left[2h] + Cxz_right[(h-1) % 4] (carry lands here) + rotated_C[2h+1] = Cxz_left[2h+1] (no carry) + +Four configurations, dropping (ii) and/or (iii). Board: A/B/C sound, D forgeable. +""" +from itertools import product +from field_model import (P, MASK16, THETA_RNC, as_field, honest_shift, + identity_holds, deviate, theta_carry_source, + theta_operand_bytes, is_byte) + +FAIL = [] + + +def check(cond, msg): + print(f" {'OK ' if cond else 'FALLA'} {msg}") + if not cond: + FAIL.append(msg) + + +print("=== premise the whole theta argument rests on ===") +# rnc = 1, so left = (in << 1) mod 2**16 is ALWAYS EVEN. This is what kills +# d = +1 in configuration B, and it is specific to a shift by one. +evens = all(honest_shift(i, THETA_RNC)[0] % 2 == 0 for i in range(1 << 16)) +check(evens, "left = (in<<1) mod 2**16 is even for all 2**16 inputs") +# and the carry never needs more than a bit: in*2 < 2**17 +carries = {honest_shift(i, THETA_RNC)[1] for i in range(1 << 16)} +check(carries <= {0, 1}, f"the honest carry only ever takes {sorted(carries)} -> one bit suffices") + +print("\n=== A: shipped (both checks) — d = 0 forced ===") +# L' = L - 2**16*d with L, L' both in [0, 2**16) forces |2**16 d| <= 65535 < 2**16. +check(2**16 > MASK16, "|2**16 * d| >= 2**16 > 65535 for any d != 0, so ARE_BYTES alone pins d = 0") + +print("\n=== C: IS_BIT dropped, ARE_BYTES kept — d = 0 forced, IS_BIT is IMPLIED ===") +check(2**16 > MASK16, "same bound: ARE_BYTES on left pins d = 0, hence right = honest quotient in {0,1}") + +print("\n=== B: ARE_BYTES dropped, IS_BIT kept — exhaustive over every reachable d ===") +# IS_BIT keeps right in {0,1}, so d = right' - right lies in {-1,0,1}: the search +# space is finite and the enumeration below is complete. No solver needed. +# +# With no range check on Cxz_left, the only bound left on L' is the operand: +# L' = lo + 256*hi, hi in [0,255] (hi IS the odd operand byte) +# lo in [-r', 255-r'] (lo + carry must be a byte) +# so L' ranges over [-r'_prev, 65535 - r'_prev] -- a window of width 2**16. +def theta_operand_window(right_prev): + """The interval L' may occupy when its own range check is gone.""" + return -right_prev, 65535 - right_prev + + +def config_b_survivor(in_hws): + """Return the first d != 0 that satisfies IS_BIT and every operand window.""" + honest = [honest_shift(i, THETA_RNC) for i in in_hws] + for d in product((-1, 0, 1), repeat=4): + if not any(d): + continue + dev = [deviate(honest[h][0], honest[h][1], d[h]) for h in range(4)] + if any(not 0 <= right <= 1 for _, right in dev): + continue # IS_BIT rejects it + lo_hi = [theta_operand_window(dev[theta_carry_source(h)][1]) for h in range(4)] + if all(lo <= dev[h][0] <= hi for h, (lo, hi) in enumerate(lo_hi)): + return in_hws, d, dev + return None + + +survivors = [config_b_survivor(c) for c in + ([0xFFFF] * 4, [0] * 4, [0xAAAA, 0x5555, 0xFFFF, 0x0001], [0x8000] * 4)] +check(not any(survivors), + "no d != 0 survives IS_BIT + the operand windows") +print(" why: d=+1 needs L' = L - 2**16 >= -r'_prev >= -1, i.e. L = 65535 -- but L is") +print(" EVEN (shift by one), so that is unreachable; d=-1 needs L' > 65535.") + +print("\n=== D: both dropped — FORGEABLE, explicit witness ===") +in_hws = [0xFFFF] * 4 # C = 0xFFFF...FF +honest = [honest_shift(i, THETA_RNC) for i in in_hws] +d = (1, 1, 1, 1) +dev = [deviate(honest[h][0], honest[h][1], d[h]) for h in range(4)] + +hon_left = [b for h in range(4) for b in (honest[h][0] & 0xFF, honest[h][0] >> 8)] +hon_right = [honest[h][1] for h in range(4)] +frg_left = [b for h in range(4) for b in (dev[h][0], 0)] # L' = -2 -> (-2, 0) +frg_right = [dev[h][1] for h in range(4)] + +hon_out = theta_operand_bytes(hon_left, hon_right) +frg_out = theta_operand_bytes(frg_left, frg_right) + +check(all(identity_holds(in_hws[h], THETA_RNC, dev[h][0], dev[h][1]) for h in range(4)), + "the forged (left, right) satisfies all four shipped identities") +check(all(is_byte(v) for v in frg_out), "every forged rotated_C byte is a byte (ByteAlu accepts it)") +check(any(a != b for a, b in zip(hon_out, frg_out)), "the theta output CHANGES") +check(any(as_field(v) > 255 for v in frg_left), "only Cxz_left holds non-bytes (its check is the one gone)") +print(f" honest rotated_C = {hon_out}") +print(f" FORGED rotated_C = {frg_out}") +print(f" forged Cxz_left (as field elements) = {[as_field(v) for v in frg_left[:2]]}...") +print(f" forged Cxz_right = {frg_right} (2 is not a bit -> IS_BIT would reject)") + +# generality: the four carries form a cycle, so an arbitrary target is reachable +det = (2**16) ** 4 - 1 +check(det % P != 0, f"det(2**16*I - S) = 2**64-1 = {det % P} mod p is invertible -> ANY target output") + +print("\n=== VERDICT ===") +print(" A sound | B sound (ARE_BYTES alone is redundant) | C sound (IS_BIT alone is redundant)") +print(" D FORGEABLE -> the PAIR is load-bearing; neither check is, on its own.") +assert not FAIL, FAIL +print("\nALL THETA NECESSITY CHECKS PASSED") From fd684a6ef8f3d85fb9c987f26499365be029dd27 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Wed, 2 Sep 2026 16:21:10 -0300 Subject: [PATCH 04/15] Exhibit the rho forgery as a complete round --- .../keccak/witness_fullchip.py | 165 ++++++++++++++++++ 1 file changed, 165 insertions(+) create mode 100644 formal_verification/keccak/witness_fullchip.py diff --git a/formal_verification/keccak/witness_fullchip.py b/formal_verification/keccak/witness_fullchip.py new file mode 100644 index 000000000..6a746d404 --- /dev/null +++ b/formal_verification/keccak/witness_fullchip.py @@ -0,0 +1,165 @@ +""" +The forgery as a COMPLETE KECCAK_RND row, not a lane in isolation. + +necessity_rho.py answers the algebra for one source lane. The fair objection is +that a lane is a fragment: show that a whole row of the chip accepts, with every +one of its 140 constraints and every one of its ByteAlu/AreBytes operands +satisfied, and still emits a state that is not Keccak-f. + +That is what this builds, for the tamper "the rho ARE_BYTES pair stops covering +rot_left" — which is a ONE-LINE edit in `bus_interactions()` (the pair's first +BusValue changed from cols::rot_left to cols::rot_right) and therefore leaves +the interaction count, the column count and the constraint count untouched. + +Reachability: the input is a real message state — all zeros except one lane at +0xFFFF...FF. That lane comes straight from the absorbed block, so this is +round 0 of a permutation an attacker can request. +""" +from keccak_ref import RHO, RC, keccak_round +from field_model import (P, as_field, honest_shift, identity_holds, deviate, + rho_pi_offsets, rho_operand_bytes, theta_carry_source, + theta_operand_bytes, is_byte, THETA_RNC) + +FAIL = [] + + +def check(cond, msg): + print(f" {'OK ' if cond else 'FALLA'} {msg}") + if not cond: + FAIL.append(msg) + + +ALL_ONES = (1 << 64) - 1 +ROUND = 0 +state = [0] * 25 +state[0] = ALL_ONES # one lane of the absorbed block +lanes = [[state[x + 5 * y] for y in range(5)] for x in range(5)] + + +def to_bytes(v): + return [(v >> (8 * b)) & 0xFF for b in range(8)] + + +# ---------------------------------------------------------------- honest row +S = [[to_bytes(lanes[x][y]) for y in range(5)] for x in range(5)] +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] + for st in range(1, 4): + for b in range(8): + cxz[x][st][b] = cxz[x][st - 1][b] ^ S[x][st + 1][b] + +cxz_left = [[0] * 8 for _ in range(5)] +cxz_right = [[0] * 4 for _ in range(5)] +for x in range(5): + for h in range(4): + inp = cxz[x][3][2 * h] | (cxz[x][3][2 * h + 1] << 8) + L, R = honest_shift(inp, THETA_RNC) + cxz_left[x][2 * h], cxz_left[x][2 * h + 1] = L & 0xFF, L >> 8 + cxz_right[x][h] = R + +dxz = [[0] * 8 for _ in range(5)] +for x in range(5): + rc_bytes = theta_operand_bytes(cxz_left[(x + 1) % 5], cxz_right[(x + 1) % 5]) + for b in range(8): + dxz[x][b] = cxz[(x + 4) % 5][3][b] ^ rc_bytes[b] + +theta = [[[S[x][y][b] ^ dxz[x][b] for b in range(8)] for y in range(5)] for x in range(5)] +theta_lane = [[sum(theta[x][y][b] << (8 * b) for b in range(8)) for y in range(5)] for x in range(5)] + +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[x][y] % 16 + for h in range(4): + inp = theta[x][y][2 * h] | (theta[x][y][2 * h + 1] << 8) + L, R = honest_shift(inp, rnc) + rot_left[x][y][2 * h], rot_left[x][y][2 * h + 1] = L & 0xFF, L >> 8 + rot_right[x][y][2 * h], rot_right[x][y][2 * h + 1] = R & 0xFF, R >> 8 + +# --------------------------------------------------- pick a saturated source lane +saturated = [(x, y) for x in range(5) for y in range(5) if theta_lane[x][y] == ALL_ONES] +check(bool(saturated), f"the message state reaches theta = 0xFFFF...FF on {len(saturated)} lanes: {saturated}") +TX, TY = saturated[0] +print(f" tampering source lane ({TX},{TY}), RHO={RHO[TX][TY]}") + +# --------------------------------------------------------------- forge that lane +rnc, rbc = RHO[TX][TY] % 16, RHO[TX][TY] // 16 +in_hws = [theta[TX][TY][2 * h] | (theta[TX][TY][2 * h + 1] << 8) for h in range(4)] +dev = [deviate(*honest_shift(in_hws[h], rnc), 1) for h in range(4)] +f_right = [b for h in range(4) for b in (dev[h][1] & 0xFF, dev[h][1] >> 8)] +f_left = [-f_right[(w - 2) % 8] for w in range(8)] +rot_left[TX][TY] = f_left +rot_right[TX][TY] = f_right + + +def pi(X, Y, z): + sx, sy = (X + 3 * Y) % 5, X + a = rho_pi_offsets(RHO[sx][sy] // 16) + return rot_left[sx][sy][(z + a) % 8] + rot_right[sx][sy][(z + a - 2) % 8] + + +# --------------------------------------------------- rebuild chi / iota downstream +chi_ands = [[[0] * 8 for _ in range(5)] for _ in range(5)] +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, p1, p2 = pi(x, y, b), pi((x + 1) % 5, y, b), pi((x + 2) % 5, y, b) + chi_ands[x][y][b] = (255 - as_field(p1) % 256) & (as_field(p2) % 256) + chi[x][y][b] = (as_field(p0) % 256) ^ chi_ands[x][y][b] +iota = [chi[0][0][b] ^ to_bytes(RC[ROUND])[b] for b in range(8)] + +# ------------------------------------------------------------------ verify the row +viol = [] +for x in range(5): # 20 IS_BIT + 20 theta + for h in range(4): + if cxz_right[x][h] not in (0, 1): + viol.append(f"IS_BIT x={x} h={h}") + inp = cxz[x][3][2 * h] | (cxz[x][3][2 * h + 1] << 8) + if not identity_holds(inp, THETA_RNC, + cxz_left[x][2 * h] + 256 * cxz_left[x][2 * h + 1], + cxz_right[x][h]): + viol.append(f"theta identity x={x} h={h}") +for x in range(5): # 100 rho identities + for y in range(5): + r = RHO[x][y] % 16 + for h in range(4): + inp = theta[x][y][2 * h] | (theta[x][y][2 * h + 1] << 8) + if not identity_holds(inp, r, + rot_left[x][y][2 * h] + 256 * rot_left[x][y][2 * h + 1], + rot_right[x][y][2 * h] + 256 * rot_right[x][y][2 * h + 1]): + viol.append(f"rho identity ({x},{y}) h={h}") +check(not viol, f"all 140 shipped constraints satisfied ({len(viol)} violations)") + +opviol = [f"pi({x},{y},{b})" for x in range(5) for y in range(5) for b in range(8) + if not is_byte(pi(x, y, b))] +opviol += [f"rotated_C({x},{b})" for x in range(5) + for b, v in enumerate(theta_operand_bytes(cxz_left[x], cxz_right[x])) if not is_byte(v)] +check(not opviol, f"every ByteAlu operand is a byte, so every lookup matches ({len(opviol)} bad)") + +kept = [f"({x},{y})" for x in range(5) for y in range(5) for b in range(8) + if not is_byte(rot_right[x][y][b])] +check(not kept, "rot_right stays byte-valued everywhere — the surviving check accepts it") +oor = sum(1 for x in range(5) for y in range(5) for b in range(8) + if as_field(rot_left[x][y][b]) > 255) +check(oor > 0, f"{oor} of 200 rot_left columns hold non-bytes — only the DROPPED check would object") + +# ------------------------------------------------------------------- vs FIPS-202 +ref = keccak_round(state, RC[ROUND]) +got = [0] * 25 +for x in range(5): + for y in range(5): + bs = iota if (x, y) == (0, 0) else chi[x][y] + got[x + 5 * y] = sum(bs[b] << (8 * b) for b in range(8)) +wrong = [(i % 5, i // 5) for i in range(25) if got[i] != ref[i]] +check(bool(wrong), f"{len(wrong)} of 25 output lanes differ from FIPS-202: {wrong}") + +print("\n=== VERDICT ===") +print(" A one-line change to the rho ARE_BYTES pair yields a complete, reachable") +print(" KECCAK_RND row with 0 constraint violations, every lookup matching, and a") +print(" wrong permutation output. Interaction/column/constraint counts unchanged.") +assert not FAIL, FAIL +print("\nFULL-CHIP WITNESS VERIFIED") From d193ef89d7d50ec0a106f915febcc979d4d4555e Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Wed, 2 Sep 2026 16:21:10 -0300 Subject: [PATCH 05/15] Record what each keccak range check is worth --- formal_verification/keccak/README.md | 85 +++++++++++++++++++++------- 1 file changed, 66 insertions(+), 19 deletions(-) diff --git a/formal_verification/keccak/README.md b/formal_verification/keccak/README.md index ed4f2a63d..9abc9ccfb 100644 --- a/formal_verification/keccak/README.md +++ b/formal_verification/keccak/README.md @@ -79,15 +79,33 @@ Each helper lookup is modeled by its contract, not its implementation: cannot reveal. Here, `AreBytes` on `Cxz_left`/`rot_left`/`rot_right` is carried by declaring those variables 8-bit bitvectors, and the θ carry `Cxz_right` is pinned directly to `ZeroExt(7, Extract(15, 15, in))`, with the separate `IS_BIT` disjunct - redundant *in the model*. Both are `load-bearing` in the circuit - (the `keccak_rnd.rs` module doc-comment and the `KeccakRndConstraints` - doc-comment: the 20 μ-gated `IS_BIT`s make the θ shift decomposition - unique). Because neither can be removed from the model's constraint - list, **deleting them from the Rust leaves this gate printing `VERIFIED`** while - the θ `left` halfwords go free — `2¹⁶` is invertible mod `p`, so the forged - assignment exists. The model's pin is a sound *consequence* of the shipped - constraints today, which is why the current board is meaningful; what it is not is - a test that those constraints are still there. + redundant *in the model*. Because none of them can be removed from the model's + constraint list, **deleting them from the Rust leaves this gate printing + `VERIFIED`**. `necessity_theta.py` / `necessity_rho.py` / `witness_fullchip.py` + measure exactly what each one is worth, and the answer is **not uniform** — do not + summarise it as "they are all load-bearing": + + | dropped | θ (`Cxz_left` / `Cxz_right`) | ρ (`rot_left` / `rot_right`) | + |---|---|---| + | the `left` range check | sound — implied | **FORGEABLE** | + | the `right` range check | sound — implied | sound — implied | + | both | **FORGEABLE** | **FORGEABLE**, output entirely free | + + So in θ the *pair* is load-bearing and neither half is on its own, while in ρ + **`rot_left`'s check is load-bearing by itself**. The asymmetry is not incidental: + `left` and `right` enter the identity with weights `1` and `2¹⁶`, so bounding + `left` kills the deviation `(L, R) → (L − 2¹⁶d, R + d)` outright, while bounding + `right` only narrows it — and whether `d = ±1` still fits depends on the residual + window the downstream ByteAlu operand leaves. In θ that window is closed by the + *parity* of `left` (the shift is by one, so `left` is always even) and by the carry + being a single bit; in ρ, `right` is a halfword and `d = ±1` fits exactly at + saturation. + + The model's pin is a sound *consequence* of the shipped constraints today, which is + why the current board is meaningful; what it is not is a test that those + constraints are still there. **The `24/24 UNSAT` verdict is conditional on the + range checks existing and must never be cited as evidence that they are + redundant.** 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 @@ -107,7 +125,10 @@ Each helper lookup is modeled by its contract, not its implementation: *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). + bound *suffices* mod `p` needs an integer/field model — that is what + `field_model.py` and the two `necessity_*.py` scripts are, and their result is the + table in discipline 1. Run them whenever the shift identities or their range + checks change. 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 @@ -155,14 +176,21 @@ PR) merely growing the file by 136 lines. If you copy this template, cite by name for the same reason. -**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. +**The scope gap this baseline declared is now closed.** QF-BV cannot test whether +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, so the question is not merely unanswered there but unaskable. +`field_model.py` supplies the companion integer-mod-`p` model, `necessity_theta.py` +and `necessity_rho.py` decide every configuration, and `witness_fullchip.py` exhibits +the ρ forgery as a complete, reachable round rather than an isolated lane. The result +is the table in discipline 1. + +One consequence is worth recording for whoever touches the round next: **#889, which +inlined the θ/ρ shifts to drop 120 HWSL sends per row, made `rot_left`'s range check +load-bearing.** Under the HWSL *lookup* the pair `(left, right)` was pinned +individually and dropping either check was harmless; under the shipped identity, +dropping `rot_left`'s is forgeable. The 100 saved ρ sends were paid for with a range +check that changed status, and nothing outside this directory records that. ## Scope @@ -199,6 +227,16 @@ first extension of this template. - `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. +- `field_model.py` — the companion **integer-mod-`p`** model of the inline θ/ρ shift + identities, with a switch per range check. This is the piece the next chip copies + when its bounds are enforced by an identity rather than a lookup. +- `combinatorics.py` — the solver-free premises the ρ result rests on: π is a + bijection on the lanes, all 400 byte columns are read exactly once by a pi operand, + the pi offsets are even, and `theta = 0xFFFF…FF` saturates every lane. +- `necessity_theta.py`, `necessity_rho.py` — which range checks are load-bearing and + which are implied, per configuration, with the forged witnesses. +- `witness_fullchip.py` — the ρ forgery as a complete KECCAK_RND row from a reachable + message state: 0 constraint violations, every lookup matching, wrong output. ## Running the gate @@ -213,10 +251,19 @@ python3 z3_parallel.py # the gate: 24 rounds + changed-constraint cont # or, single-process with inline printout: python3 z3_verify.py python3 tamper_test.py # the removed-constraint controls (see discipline 1) +python3 combinatorics.py # the solver-free premises for the rho result +python3 necessity_theta.py # which theta range checks are load-bearing +python3 necessity_rho.py # which rho range checks are load-bearing +python3 witness_fullchip.py # the rho forgery as a complete, reachable round ``` `tamper_test.py` is not optional: `z3_parallel.py` runs only the *changed*-constraint controls, so a run that skips it exercises no **removed**-constraint control at all. Expected board: positive control PASS, all negative controls **SAT** (caught), all -24 rounds **UNSAT**. Anything else is a real signal — investigate before trusting. +24 rounds **UNSAT**, every premise and necessity check **OK**, and the full-chip +witness **VERIFIED**. Anything else is a real signal — investigate before trusting. + +The necessity scripts need no solver for their UNSAT results — those are exact +integer-bounding arguments with finite, complete enumerations — so they run in +seconds. Only the QF-BV gate is slow (~3 min on ten cores). From ea575afacbdb9e10d78fd0a634d4548ac59f1981 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Wed, 2 Sep 2026 16:21:10 -0300 Subject: [PATCH 06/15] Pin the KECCAK_RND AIR structure, not its counts --- prover/src/tests/trace_builder_tests.rs | 69 +++++++++++++++++++++++++ 1 file changed, 69 insertions(+) diff --git a/prover/src/tests/trace_builder_tests.rs b/prover/src/tests/trace_builder_tests.rs index 428fd4700..f0acf54f0 100644 --- a/prover/src/tests/trace_builder_tests.rs +++ b/prover/src/tests/trace_builder_tests.rs @@ -772,6 +772,75 @@ mod keccak_tests { "KECCAK_RND: 20 IS_BIT(μ; Cxz_right_bit) + 20 θ + 100 ρ inline shift identities" ); } + + /// FNV-1a, spelled out because `std`'s hasher is explicitly not stable across + /// toolchains and the digests below are pinned in source. + fn fnv1a64(bytes: &[u8]) -> u64 { + let mut h: u64 = 0xcbf2_9ce4_8422_2325; + for &b in bytes { + h ^= b as u64; + h = h.wrapping_mul(0x0000_0100_0000_01b3); + } + h + } + + /// Pins the KECCAK_RND AIR's derived *structure*, not just its counts. + /// + /// The three count tests above catch anything that adds or removes an + /// interaction, a column or a constraint. They do not catch a **rewiring that + /// keeps the counts**. The concrete case: changing the first `BusValue` of the + /// "Rho: ARE_BYTES range checks on rot_left + rot_right" pair from + /// `cols::rot_left` to `cols::rot_right` leaves 1031/1480/140 untouched, is + /// still satisfied by every honest trace (so prove+verify passes), and makes + /// the ρ output forgeable. + /// + /// Nothing else in the tree would object. In particular the QF-BV gate in + /// `formal_verification/keccak/` cannot: it carries byte-ness as the *width* of + /// its bitvectors, so it prints `VERIFIED` either way — see its README, + /// discipline 1. `witness_fullchip.py` there exhibits the forgery as a + /// complete, reachable round with zero constraint violations, every lookup + /// matching, and two output lanes differing from FIPS-202. + /// + /// A failure here is not necessarily a bug: it means the round's wiring or its + /// constraint bodies changed. Re-run `formal_verification/keccak/` in full (the + /// four gates plus `combinatorics.py`, `necessity_theta.py`, + /// `necessity_rho.py`, `witness_fullchip.py`), confirm the expected board, then + /// update the digests below in the same commit. + #[test] + fn test_keccak_rnd_air_structure_is_pinned() { + use crate::tables::types::{GoldilocksExtension, GoldilocksField}; + use stark::constraints::builder::{CaptureBuilder, ConstraintSet}; + + // BusInteraction is not Debug, so serialise its public fields explicitly: + // bus id, direction, multiplicity, and every BusValue (which carries the + // column indices, packings and linear-term coefficients). + let bus: String = keccak_rnd::bus_interactions() + .iter() + .map(|i| { + format!( + "{}|{}|{:?}|{:?}\n", + i.bus_id, i.is_sender, i.multiplicity, i.values + ) + }) + .collect(); + assert_eq!( + fnv1a64(bus.as_bytes()), + 0x0027_e508_0abb_991f, + "KECCAK_RND bus wiring changed (bus ids, multiplicities, column indices \ + or linear-term coefficients). See this test's doc comment." + ); + + let n = keccak_rnd::KeccakRndConstraints.meta().len(); + let mut cb = CaptureBuilder::::new(); + keccak_rnd::KeccakRndConstraints.eval(&mut cb); + let (prog, _) = cb.finish(n); + assert_eq!( + fnv1a64(format!("{prog:?}").as_bytes()), + 0x83a3_3324_8bcb_a374, + "KECCAK_RND constraint IR changed (op tree, dimensions, field constants \ + or roots). See this test's doc comment." + ); + } } mod routing_tests { From 83aa3a3510799d7a7bcc4d06aaf58adc5fb4e364 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 3 Sep 2026 16:41:17 -0300 Subject: [PATCH 07/15] Check the rho config-D forgery hits its target Configuration D of the rho necessity analysis claims the lane's output is completely free: with neither range check present, the cyclic system in `right` solves for an arbitrary target. The check backing that claim only asked whether the shift identity holds for the constructed pair - and `L[j]` is derived FROM the identity, so it held by construction and could not fail. Nothing verified the target was reached. With the target now compared, it turns out it was not. The recurrence indexed `c[(j+1)%4]` while the closed form for `r0` directly above it solves `R[j-1] - 2**16*R[j] = c[j]`, so the two disagreed by one and the construction hit its intended pi halfwords on 0 of 25 lanes. Indexed `c[j]`, which is what `r0` was derived for, the lanes hit their target 25 of 25. The verdict for configuration D is unchanged - the system is solvable, the output is free - but the exhibited construction now demonstrates it. --- formal_verification/keccak/necessity_rho.py | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/formal_verification/keccak/necessity_rho.py b/formal_verification/keccak/necessity_rho.py index 3abfd79d6..d8592937e 100644 --- a/formal_verification/keccak/necessity_rho.py +++ b/formal_verification/keccak/necessity_rho.py @@ -87,6 +87,9 @@ def check(cond, msg): print("\n=== D: both dropped — the lane's output is completely free ===") # Eliminating left via the identity leaves a cyclic system in right: # right'_(j-1) - 2**16 * right'_j = c_j, solvable because 1 - 2**64 is invertible. +# The check verifies the TARGET is hit. `identity_holds` alone cannot fail here: +# L is DERIVED from the identity, so it is true by construction, and with it as +# the only check an index slip in the recurrence went unnoticed. INV = pow(1 - 2**64, -1, P) free = 0 for (sx, sy) in LANES: @@ -101,11 +104,14 @@ def check(cond, msg): R = [0] * 4 R[0] = r0 for j in (1, 2, 3): - R[j] = ((R[j - 1] - c[(j + 1) % 4]) * pow(2**16, -1, P)) % P + # R[j-1] - 2**16*R[j] = c[j] is the relation r0's closed form above + # solves; the target check below is what pins this index. + R[j] = ((R[j - 1] - c[j]) * pow(2**16, -1, P)) % P L = [(in_hws[j] * (2**rnc) - (2**16) * R[j]) % P for j in range(4)] okid = all(identity_holds(in_hws[j], rnc, L[j], R[j]) for j in range(4)) - free += okid -check(free == 25, f"the packed system is solvable for an arbitrary target on {free}/25 lanes " + hits = [(L[(h + A) % 4] + R[(h + A - 1) % 4]) % P for h in range(4)] == [q % P for q in Q] + free += okid and hits +check(free == 25, f"the forged pi halfwords equal the ARBITRARY target on {free}/25 lanes " f"(det = 1 - 2**64 = {(1 - 2**64) % P} mod p, invertible). Per-byte\n realizability is the construction exhibited in C.") print("\n=== VERDICT ===") From 7bd904de65d46872fdca113c709fa7f7ebabed1e Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 3 Sep 2026 16:41:37 -0300 Subject: [PATCH 08/15] Decide each keccak range check by a full sweep The board's three "sound - implied" cells were backed by `check(2**16 > MASK16)`: a comparison of two constants, true whatever the chip does. And the argument it stood for does not cover the two configurations where the column left unchecked is `right`, because there the deviation is not a small integer at all - over the field, any `left` in [0, 2**16) admits `right = (in*2**rnc - left)*inv(2**16)`, a full-size field element. What closes those configurations is the ByteAlu operand that reads the unchecked column. The BITWISE table holds byte rows only, so `checked_byte + this` in [0, 255] confines `this` to [-255, 255]; every term of the identity then stays under 2**33, the field identity IS the integer identity, and Euclidean division is unique. That chain is now in the model: `operand_summand_window` derives the window, `difference_form_is_exact` checks the magnitude step the difference form had silently assumed, and `surviving_deviation` sweeps all 2**16 input halfwords against one interval per column. It replaces both the constant comparisons and the four hand-picked inputs that stood in for theta's configuration B, and it asserts the honest pair lies inside the modelled intervals - the failure that would make a "pinned" verdict meaningless. The windows rest on each column being read by exactly ONE operand byte, so `combinatorics.py` grows the theta analogue of that premise: the four carries are a permutation of the four rotated_C low bytes. It is exposed as `premises()` and imported by both necessity scripts, rather than being a file whose docstring asks you to run it first. Verdicts are unchanged, but each is now the output of a sweep that fails when its inputs do: widening the left interval to a halfword and a bit, or dropping rot_left's check, both produce survivors. --- formal_verification/keccak/combinatorics.py | 132 +++++++++++------- formal_verification/keccak/field_model.py | 82 +++++++++++ formal_verification/keccak/necessity_rho.py | 77 ++++++---- formal_verification/keccak/necessity_theta.py | 104 +++++++------- 4 files changed, 264 insertions(+), 131 deletions(-) diff --git a/formal_verification/keccak/combinatorics.py b/formal_verification/keccak/combinatorics.py index a31bbbdf4..aa39521d9 100644 --- a/formal_verification/keccak/combinatorics.py +++ b/formal_verification/keccak/combinatorics.py @@ -1,65 +1,95 @@ """ -The pure-combinatorial premises the rho necessity argument rests on. +The pure-combinatorial premises the theta and rho necessity arguments rest on. -No solver: these are facts about cols::pi_src_cols and KECCAK_RHO that must hold -before any claim about "this range check is implied by the pi operand" can mean -anything. If any of them breaks, necessity_rho.py's config-B result is void. +No solver: these are facts about cols::pi_src_cols, cols::cxz_right_bit_for_byte +and KECCAK_RHO that must hold before any claim about "this range check is +implied by the ByteAlu operand" can mean anything. The load-bearing one is +READ-ONCE (sections 3 and 6): `operand_summand_window` bounds a column from the +single operand byte that reads it, and a column read twice would need the +intersection of two windows instead. + +`premises()` is imported and run by necessity_theta.py and necessity_rho.py, so +the checks below cannot be skipped by forgetting to run this file first. """ from keccak_ref import RHO -from field_model import rho_pi_offsets +from field_model import rho_pi_offsets, theta_carry_source + + +def premises(verbose=True): + """Assert every premise. Raises AssertionError naming the ones that fail.""" + failed = [] + + def check(cond, msg): + if verbose: + print(f" {'OK ' if cond else 'FAIL'} {msg}") + if not cond: + failed.append(msg) -FAIL = [] + def say(msg): + if verbose: + print(msg) + say("=== (1) pi is a bijection on the 25 lanes ===") + src_of = {(X, Y): ((X + 3 * Y) % 5, X) for X in range(5) for Y in range(5)} + images = list(src_of.values()) + check(len(set(images)) == 25, + f"(X,Y) -> ((X+3Y)%5, X) covers {len(set(images))}/25 source lanes, no repeats") -def check(cond, msg): - print(f" {'OK ' if cond else 'FALLA'} {msg}") - if not cond: - FAIL.append(msg) + say("\n=== (2) every source lane is read by exactly one output lane, via 8 bytes ===") + readers = {} + for (X, Y), src in src_of.items(): + readers.setdefault(src, []).append((X, Y)) + check(all(len(v) == 1 for v in readers.values()), + "each source lane has exactly one reader lane") + say("\n=== (3) every rot_left and rot_right byte column is read EXACTLY once ===") + bad = [] + for src, ((X, Y),) in ((s, tuple(r)) for s, r in readers.items()): + a = rho_pi_offsets(RHO[src[0]][src[1]] // 16) + left_hits = [0] * 8 + right_hits = [0] * 8 + for z in range(8): + left_hits[(z + a) % 8] += 1 + right_hits[(z + a - 2) % 8] += 1 + if left_hits != [1] * 8 or right_hits != [1] * 8: + bad.append((src, left_hits, right_hits)) + check(not bad, "400/400 rho byte columns read exactly once (none zero times, none twice)" + f"{'' if not bad else f' — {bad[:2]}'}") -print("=== (1) pi is a bijection on the 25 lanes ===") -src_of = {(X, Y): ((X + 3 * Y) % 5, X) for X in range(5) for Y in range(5)} -images = list(src_of.values()) -check(len(set(images)) == 25, f"(X,Y) -> ((X+3Y)%5, X) covers {len(set(images))}/25 source lanes, no repeats") + say("\n=== (4) the pi byte offsets are EVEN, so a pi halfword reads one source halfword ===") + odd = [(x, y) for x in range(5) for y in range(5) if rho_pi_offsets(RHO[x][y] // 16) % 2] + check(not odd, "a in {0,6,4,2} is always even -> P_h = L_(h+A) + R_(h+A-1), A = a/2") + mism = [] + for x in range(5): + for y in range(5): + a = rho_pi_offsets(RHO[x][y] // 16) + A = a // 2 + for h in range(4): + if ((2 * h + a) % 8) // 2 != (h + A) % 4 or ((2 * h + a - 2) % 8) // 2 != (h + A - 1) % 4: + mism.append((x, y, h)) + check(not mism, "the packed relation verified for all 25 lanes x 4 halfwords") -print("\n=== (2) every source lane is read by exactly one output lane, via 8 bytes ===") -readers = {} -for (X, Y), src in src_of.items(): - readers.setdefault(src, []).append((X, Y)) -check(all(len(v) == 1 for v in readers.values()), - "each source lane has exactly one reader lane") + say("\n=== (5) theta = all-ones saturates every pi halfword, for EVERY rotation ===") + # left + right = 0xFFFF whatever rnc is, which is why config C forges on all 25. + sat = all(((0xFFFF << (RHO[x][y] % 16)) & 0xFFFF) + (0xFFFF >> (16 - (RHO[x][y] % 16)) + if RHO[x][y] % 16 else 0) == 0xFFFF for x in range(5) for y in range(5)) + check(sat, "left + right = 0xFFFF for all 25 lanes -> pi = 0xFF..FF, the saturation config C needs") -print("\n=== (3) every rot_left and rot_right byte column is read EXACTLY once ===") -bad = [] -for src, ((X, Y),) in ((s, tuple(r)) for s, r in readers.items()): - a = rho_pi_offsets(RHO[src[0]][src[1]] // 16) - left_hits = [0] * 8 - right_hits = [0] * 8 - for z in range(8): - left_hits[(z + a) % 8] += 1 - right_hits[(z + a - 2) % 8] += 1 - if left_hits != [1] * 8 or right_hits != [1] * 8: - bad.append((src, left_hits, right_hits)) -check(not bad, f"400/400 byte columns read exactly once (none zero times, none twice){'' if not bad else f' — {bad[:2]}'}") + say("\n=== (6) the theta analogue: every Cxz_right carry column is read EXACTLY once ===") + # cols::cxz_right_bit_for_byte sends the carry of halfword h-1 to the LOW byte + # of halfword h and nothing to the odd bytes, so the four carries of one x are + # a permutation of the four rotated_C low bytes. Without this, the carry has no + # single operand window and theta's config C says nothing. + sources = [theta_carry_source(h) for h in range(4)] + check(sorted(sources) == [0, 1, 2, 3], + f"theta_carry_source is a bijection on the 4 halfwords ({sources})") + check(all(theta_carry_source(h) != h for h in range(4)), + "no carry lands on its own halfword -> the cycle has no fixed point") -print("\n=== (4) the pi byte offsets are EVEN, so a pi halfword reads one source halfword ===") -odd = [(x, y) for x in range(5) for y in range(5) if rho_pi_offsets(RHO[x][y] // 16) % 2] -check(not odd, "a in {0,6,4,2} is always even -> P_h = L_(h+A) + R_(h+A-1), A = a/2") -mism = [] -for x in range(5): - for y in range(5): - a = rho_pi_offsets(RHO[x][y] // 16) - A = a // 2 - for h in range(4): - if ((2 * h + a) % 8) // 2 != (h + A) % 4 or ((2 * h + a - 2) % 8) // 2 != (h + A - 1) % 4: - mism.append((x, y, h)) -check(not mism, "the packed relation verified for all 25 lanes x 4 halfwords") + assert not failed, failed + if verbose: + print("\nALL COMBINATORIAL PREMISES HOLD") -print("\n=== (5) theta = all-ones saturates every pi halfword, for EVERY rotation ===") -# left + right = 0xFFFF whatever rnc is, which is why config C forges on all 25. -sat = all(((0xFFFF << (RHO[x][y] % 16)) & 0xFFFF) + (0xFFFF >> (16 - (RHO[x][y] % 16)) - if RHO[x][y] % 16 else 0) == 0xFFFF for x in range(5) for y in range(5)) -check(sat, "left + right = 0xFFFF for all 25 lanes -> pi = 0xFF..FF, the saturation config C needs") -assert not FAIL, FAIL -print("\nALL COMBINATORIAL PREMISES HOLD") +if __name__ == "__main__": + premises() diff --git a/formal_verification/keccak/field_model.py b/formal_verification/keccak/field_model.py index 8ccdee2e8..5c68df0a6 100644 --- a/formal_verification/keccak/field_model.py +++ b/formal_verification/keccak/field_model.py @@ -105,3 +105,85 @@ def rho_operand_bytes(rot_left, rot_right, rbc): def is_byte(v): return 0 <= v <= 255 + + +# --- the contracts that bound a column, and what survives dropping one ------- +# +# Each interval below is the contract of a named construct, so that a change in +# the chip changes the number here rather than leaving a stale comment: +# +# ARE_BYTES pair the two columns it carries are bytes -> BYTE +# IS_BIT the theta carry column is a bit -> BIT +# ByteAlu OPERAND the BITWISE table holds byte rows only, so a virtual +# operand `a + b` must land in [0, 255]. That still bounds a +# column whose OWN range check is gone -- as long as the +# other summand is bounded -- and it is the whole reason the +# two "implied" verdicts hold. +BYTE = (0, 255) +BIT = (0, 1) + + +def operand_summand_window(other): + """What a ByteAlu operand alone leaves for one summand. + + `this + other` in [0, 255] with `other` in `other`, so `this` is confined to + [-max(other), 255 - min(other)] -- NOT to [0, 255], but small, which is the + only property the analysis needs. Requires the read-once premise (each + column read by exactly ONE operand byte: combinatorics sections 3 and 6) and + breaks down when BOTH summands are unchecked, since then the operand bounds + only their sum: that is configuration D, and it has no per-column window at + all, which is why its output is entirely free. + """ + return -other[1], 255 - other[0] + + +def packed_pair_bounds(lo, hi): + """The interval `lo_col + 256*hi_col` occupies, given per-byte intervals.""" + return lo[0] + 256 * hi[0], lo[1] + 256 * hi[1] + + +def difference_form_is_exact(rnc, left_bounds, right_bounds): + """Is the field identity the same statement as the integer identity? + + Everything below parameterises deviations by an INTEGER `d`, which is only + legitimate while every term stays far below `p`. This is the step the + difference form silently assumed: widen a bound enough -- a column with no + bound at all -- and `d` ranges over the whole field, `2**16` is invertible, + and no sweep over small `d` means anything. + """ + worst = ( + MASK16 * 2**rnc + + max(abs(right_bounds[0]), abs(right_bounds[1])) * 2**16 + + max(abs(left_bounds[0]), abs(left_bounds[1])) + ) + return worst < P // 2 + + +def surviving_deviation(rnc, left_bounds, right_bounds): + """Complete sweep: does any input halfword admit a second `(left, right)`? + + Returns `None` when all 2**16 inputs are pinned -- the configuration is + sound -- or `(in_hw, d)` for the first input that admits another solution. + + Complete, not sampled: the identity's solution set is exactly + `(L - 2**16*d, R + d)` over `d`, `difference_form_is_exact` keeps `d` an + integer, and `left_bounds` caps `|d|`, so the `d` range below is exhaustive. + Also asserts the HONEST pair lies inside the bounds, which catches a window + modelled wrongly (the failure that would make a `None` here meaningless). + """ + lo_l, hi_l = left_bounds + lo_r, hi_r = right_bounds + dmax = (hi_l - lo_l) // 2**16 + 1 + for in_hw in range(1 << 16): + left, right = honest_shift(in_hw, rnc) + assert lo_l <= left <= hi_l and lo_r <= right <= hi_r, ( + f"the honest pair for in={in_hw:#06x} falls outside the modelled " + f"bounds left={left_bounds} right={right_bounds}" + ) + for d in range(-dmax, dmax + 1): + if d == 0: + continue + dev_left, dev_right = deviate(left, right, d) + if lo_l <= dev_left <= hi_l and lo_r <= dev_right <= hi_r: + return in_hw, d + return None diff --git a/formal_verification/keccak/necessity_rho.py b/formal_verification/keccak/necessity_rho.py index d8592937e..5f0ac2474 100644 --- a/formal_verification/keccak/necessity_rho.py +++ b/formal_verification/keccak/necessity_rho.py @@ -12,44 +12,63 @@ pi[z] = rot_left[l(z)] + rot_right[r(z)] must be a byte -Premises from combinatorics.py (run it first): the offsets are even, so a pi -halfword reads one source halfword as P_h = L_(h+A) + R_(h+A-1), and every one -of the 400 byte columns is read exactly once. +so dropping one column's check does not free it: the operand still confines it +(`operand_summand_window`), which is what makes configurations A and B sound and +is the step a bound-vs-bound comparison cannot express. Premises live in +combinatorics.py and are imported below, not left to be run by hand: the +offsets are even, so a pi halfword reads one source halfword as +P_h = L_(h+A) + R_(h+A-1), and every one of the 400 byte columns is read exactly +once -- a column read twice would need the intersection of two windows. RESULT, and it is asymmetric — unlike theta, here ONE check is load-bearing on its own. `left` and `right` enter the identity with weights 1 and 2**16, so bounding `left` kills the deviation while bounding `right` does not. """ -from itertools import product from keccak_ref import RHO -from field_model import (P, MASK16, as_field, honest_shift, identity_holds, - deviate, rho_pi_offsets, rho_operand_bytes, is_byte) +from combinatorics import premises +from field_model import (P, BYTE, as_field, honest_shift, identity_holds, + deviate, difference_form_is_exact, operand_summand_window, + packed_pair_bounds, rho_pi_offsets, rho_operand_bytes, + surviving_deviation, is_byte) + +premises(verbose=False) FAIL = [] def check(cond, msg): - print(f" {'OK ' if cond else 'FALLA'} {msg}") + print(f" {'OK ' if cond else 'FAIL'} {msg}") if not cond: FAIL.append(msg) LANES = [(x, y) for x in range(5) for y in range(5)] - -print("=== A / B: left stays range-checked — d = 0 forced, on every lane ===") -# L' = L - 2**16*d with L, L' both in [0, 2**16) leaves no room for d != 0. This -# holds whatever `right` is allowed to be, so dropping rot_right's half of the -# pair changes nothing: its value is then recovered from the identity, uniquely, -# because 2**16 is invertible mod p. rot_right's check is IMPLIED. -check(2**16 > MASK16, "|2**16 * d| >= 2**16 > 65535 for d != 0 -> A and B sound for all 25 lanes") - -print("\n=== C: rot_left's check dropped — completeness of the search first ===") -# right stays in [0, 2**16), so d = right' - right has |d| <= 65535. And -# P'_h = P_h - 2**16*d_(h+A) + d_(h+A-1) in [0, 65535] with P_h in [0, 65535] -# forces |2**16*d_j - d_(j-1)| <= 65535, so |d_j| >= 2 would need -# |d_(j-1)| >= 2*2**16 - 65535 = 65537 > 65535. Hence |d_j| <= 1 for all j. -check(2 * 2**16 - MASK16 > MASK16, - f"|d| >= 2 would need a neighbour |d| >= {2 * 2**16 - MASK16} > {MASK16} -> d in {{-1,0,1}}, search complete") +RNCS = sorted({RHO[x][y] % 16 for (x, y) in LANES}) + +# Both halves are byte PAIRS here (unlike theta's single carry column), so each +# window is the packed span of two per-byte windows. +CHECKED = packed_pair_bounds(BYTE, BYTE) +OPERAND_ONLY = packed_pair_bounds(operand_summand_window(BYTE), operand_summand_window(BYTE)) + +print(f"=== A / B: left stays range-checked — complete sweep, all {len(RNCS)} distinct rotations ===") +# Dropping rot_right's check leaves it the pi operand window; the sweep then +# shows the honest pair is the only one, so rot_right's check is IMPLIED. +for name, left_b, right_b in (("A: both checked", CHECKED, CHECKED), + ("B: rot_right's check dropped", CHECKED, OPERAND_ONLY)): + surv = [(rnc, surviving_deviation(rnc, left_b, right_b)) for rnc in RNCS] + check(all(difference_form_is_exact(rnc, left_b, right_b) for rnc in RNCS), + f"{name}: every term < p/2, so the field identity IS the integer one") + check(all(s is None for _, s in surv), + f"{name}: left in {left_b}, right in {right_b} -> pinned on all " + f"{len(RNCS)} rotations x 2**16 inputs" + f"{'' if all(s is None for _, s in surv) else f' — SURVIVORS {[s for s in surv if s[1]][:2]}'}") + +print("\n=== C: rot_left's check dropped — the sweep already says forgeable ===") +surv_c = {rnc: surviving_deviation(rnc, OPERAND_ONLY, CHECKED) for rnc in RNCS} +check(all(s is not None for s in surv_c.values()), + f"a deviation survives on all {len(RNCS)} rotations, e.g. rnc={RNCS[0]} -> {surv_c[RNCS[0]]}") +check(all(d == 1 for _, d in surv_c.values()), + "and it is d = +1 every time -> the witness below is the general shape, not a special case") print("\n=== C: the forged witness, verified PER BYTE on every lane ===") forged = 0 @@ -85,11 +104,12 @@ def check(cond, msg): print(" byte-valued here, so only rot_left's check catches it.") print("\n=== D: both dropped — the lane's output is completely free ===") -# Eliminating left via the identity leaves a cyclic system in right: -# right'_(j-1) - 2**16 * right'_j = c_j, solvable because 1 - 2**64 is invertible. -# The check verifies the TARGET is hit. `identity_holds` alone cannot fail here: -# L is DERIVED from the identity, so it is true by construction, and with it as -# the only check an index slip in the recurrence went unnoticed. +# No per-column window survives (the operand bounds only the SUM of two +# unchecked columns), so eliminating left via the identity leaves a cyclic +# system in right: right'_(j-1) - 2**16 * right'_j = c_j, solvable because +# 1 - 2**64 is invertible. The check below verifies the TARGET is hit, not just +# that the identity holds -- the identity holds by construction, since L is +# derived from it. INV = pow(1 - 2**64, -1, P) free = 0 for (sx, sy) in LANES: @@ -112,7 +132,8 @@ def check(cond, msg): hits = [(L[(h + A) % 4] + R[(h + A - 1) % 4]) % P for h in range(4)] == [q % P for q in Q] free += okid and hits check(free == 25, f"the forged pi halfwords equal the ARBITRARY target on {free}/25 lanes " - f"(det = 1 - 2**64 = {(1 - 2**64) % P} mod p, invertible). Per-byte\n realizability is the construction exhibited in C.") + f"(det = 1 - 2**64 = {(1 - 2**64) % P} mod p, invertible). Per-byte\n" + f" realizability is the construction exhibited in C.") print("\n=== VERDICT ===") print(" A sound | B sound -> rot_right's check is IMPLIED by rot_left's + the pi operand") diff --git a/formal_verification/keccak/necessity_theta.py b/formal_verification/keccak/necessity_theta.py index 322309020..204e4b3ca 100644 --- a/formal_verification/keccak/necessity_theta.py +++ b/formal_verification/keccak/necessity_theta.py @@ -14,74 +14,71 @@ rotated_C[2h] = Cxz_left[2h] + Cxz_right[(h-1) % 4] (carry lands here) rotated_C[2h+1] = Cxz_left[2h+1] (no carry) -Four configurations, dropping (ii) and/or (iii). Board: A/B/C sound, D forgeable. +HOW A CONFIGURATION IS DECIDED. Dropping a check does not leave its column +free: whichever of the two the operand still reads alongside a bounded summand +keeps a window (`operand_summand_window`, premise section 6 of +combinatorics.py). So each configuration is a pair of intervals, and +`surviving_deviation` sweeps all 2**16 input halfwords against them -- +completely, not by sampling. Configuration D is the exception: both columns of +the same operand lose their check, the operand then bounds only their SUM, +there is no per-column window, and the explicit witness below is what decides +it. + +Board: A/B/C sound, D forgeable. """ -from itertools import product -from field_model import (P, MASK16, THETA_RNC, as_field, honest_shift, - identity_holds, deviate, theta_carry_source, - theta_operand_bytes, is_byte) +from combinatorics import premises +from field_model import (P, THETA_RNC, BYTE, BIT, as_field, honest_shift, + identity_holds, deviate, difference_form_is_exact, + operand_summand_window, packed_pair_bounds, + surviving_deviation, theta_operand_bytes, is_byte) + +premises(verbose=False) FAIL = [] def check(cond, msg): - print(f" {'OK ' if cond else 'FALLA'} {msg}") + print(f" {'OK ' if cond else 'FAIL'} {msg}") if not cond: FAIL.append(msg) -print("=== premise the whole theta argument rests on ===") +# The window each column occupies per configuration, derived from the contracts: +# Cxz_left ARE_BYTES pair, or -- with that gone -- the Dxz operand, whose low +# byte carries Cxz_right and whose high byte does not. +# Cxz_right IS_BIT, or -- with that gone -- the Dxz operand alongside a +# range-checked Cxz_left byte. +LEFT_CHECKED = packed_pair_bounds(BYTE, BYTE) +LEFT_OPERAND_ONLY = packed_pair_bounds(operand_summand_window(BIT), BYTE) +RIGHT_CHECKED = BIT +RIGHT_OPERAND_ONLY = operand_summand_window(BYTE) + +CONFIGS = [ + ("A: shipped, both checks", LEFT_CHECKED, RIGHT_CHECKED), + ("B: ARE_BYTES dropped, IS_BIT kept", LEFT_OPERAND_ONLY, RIGHT_CHECKED), + ("C: IS_BIT dropped, ARE_BYTES kept", LEFT_CHECKED, RIGHT_OPERAND_ONLY), +] + +print("=== the two facts that make theta's windows what they are ===") # rnc = 1, so left = (in << 1) mod 2**16 is ALWAYS EVEN. This is what kills # d = +1 in configuration B, and it is specific to a shift by one. evens = all(honest_shift(i, THETA_RNC)[0] % 2 == 0 for i in range(1 << 16)) check(evens, "left = (in<<1) mod 2**16 is even for all 2**16 inputs") -# and the carry never needs more than a bit: in*2 < 2**17 carries = {honest_shift(i, THETA_RNC)[1] for i in range(1 << 16)} check(carries <= {0, 1}, f"the honest carry only ever takes {sorted(carries)} -> one bit suffices") -print("\n=== A: shipped (both checks) — d = 0 forced ===") -# L' = L - 2**16*d with L, L' both in [0, 2**16) forces |2**16 d| <= 65535 < 2**16. -check(2**16 > MASK16, "|2**16 * d| >= 2**16 > 65535 for any d != 0, so ARE_BYTES alone pins d = 0") - -print("\n=== C: IS_BIT dropped, ARE_BYTES kept — d = 0 forced, IS_BIT is IMPLIED ===") -check(2**16 > MASK16, "same bound: ARE_BYTES on left pins d = 0, hence right = honest quotient in {0,1}") - -print("\n=== B: ARE_BYTES dropped, IS_BIT kept — exhaustive over every reachable d ===") -# IS_BIT keeps right in {0,1}, so d = right' - right lies in {-1,0,1}: the search -# space is finite and the enumeration below is complete. No solver needed. -# -# With no range check on Cxz_left, the only bound left on L' is the operand: -# L' = lo + 256*hi, hi in [0,255] (hi IS the odd operand byte) -# lo in [-r', 255-r'] (lo + carry must be a byte) -# so L' ranges over [-r'_prev, 65535 - r'_prev] -- a window of width 2**16. -def theta_operand_window(right_prev): - """The interval L' may occupy when its own range check is gone.""" - return -right_prev, 65535 - right_prev - - -def config_b_survivor(in_hws): - """Return the first d != 0 that satisfies IS_BIT and every operand window.""" - honest = [honest_shift(i, THETA_RNC) for i in in_hws] - for d in product((-1, 0, 1), repeat=4): - if not any(d): - continue - dev = [deviate(honest[h][0], honest[h][1], d[h]) for h in range(4)] - if any(not 0 <= right <= 1 for _, right in dev): - continue # IS_BIT rejects it - lo_hi = [theta_operand_window(dev[theta_carry_source(h)][1]) for h in range(4)] - if all(lo <= dev[h][0] <= hi for h, (lo, hi) in enumerate(lo_hi)): - return in_hws, d, dev - return None - - -survivors = [config_b_survivor(c) for c in - ([0xFFFF] * 4, [0] * 4, [0xAAAA, 0x5555, 0xFFFF, 0x0001], [0x8000] * 4)] -check(not any(survivors), - "no d != 0 survives IS_BIT + the operand windows") -print(" why: d=+1 needs L' = L - 2**16 >= -r'_prev >= -1, i.e. L = 65535 -- but L is") -print(" EVEN (shift by one), so that is unreachable; d=-1 needs L' > 65535.") - -print("\n=== D: both dropped — FORGEABLE, explicit witness ===") +print("\n=== A / B / C: complete sweep over every input halfword ===") +for name, left_b, right_b in CONFIGS: + check(difference_form_is_exact(THETA_RNC, left_b, right_b), + f"{name}: every term < p/2, so the field identity IS the integer one") + surv = surviving_deviation(THETA_RNC, left_b, right_b) + check(surv is None, + f"{name}: left in {left_b}, right in {right_b} -> " + f"{'no deviation survives any of the 2**16 inputs' if surv is None else f'SURVIVOR {surv}'}") +print(" B is the interesting one: d=+1 needs L' = L - 2**16 >= -1, i.e. L = 65535,") +print(" and L is EVEN, so the sweep finds nothing. d=-1 needs L' > 65535.") + +print("\n=== D: both dropped — no per-column window exists, so: explicit witness ===") in_hws = [0xFFFF] * 4 # C = 0xFFFF...FF honest = [honest_shift(i, THETA_RNC) for i in in_hws] d = (1, 1, 1, 1) @@ -100,10 +97,11 @@ def config_b_survivor(in_hws): check(all(is_byte(v) for v in frg_out), "every forged rotated_C byte is a byte (ByteAlu accepts it)") check(any(a != b for a, b in zip(hon_out, frg_out)), "the theta output CHANGES") check(any(as_field(v) > 255 for v in frg_left), "only Cxz_left holds non-bytes (its check is the one gone)") +check(any(v not in (0, 1) for v in frg_right), "and Cxz_right holds a non-bit (IS_BIT would reject it)") print(f" honest rotated_C = {hon_out}") print(f" FORGED rotated_C = {frg_out}") print(f" forged Cxz_left (as field elements) = {[as_field(v) for v in frg_left[:2]]}...") -print(f" forged Cxz_right = {frg_right} (2 is not a bit -> IS_BIT would reject)") +print(f" forged Cxz_right = {frg_right}") # generality: the four carries form a cycle, so an arbitrary target is reachable det = (2**16) ** 4 - 1 @@ -112,5 +110,7 @@ def config_b_survivor(in_hws): print("\n=== VERDICT ===") print(" A sound | B sound (ARE_BYTES alone is redundant) | C sound (IS_BIT alone is redundant)") print(" D FORGEABLE -> the PAIR is load-bearing; neither check is, on its own.") +print(" Note WHAT each half costs: Cxz_left's is 20 ARE_BYTES sends, Cxz_right's is") +print(" 20 degree-3 polynomial constraints -- the reason this AIR declares max_degree 3.") assert not FAIL, FAIL print("\nALL THETA NECESSITY CHECKS PASSED") From 4a29e2c02a398fbf742a4ab61ae117ccbe1bf1de Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 3 Sep 2026 16:41:41 -0300 Subject: [PATCH 09/15] Control the full-chip witness against FIPS-202 `witness_fullchip.py` asserted that at least one output lane differs from the reference - which is also what a bug in its own hand transcription of the round produces. Both failure modes were reachable: making Dxz read column (x+1) instead of (x+4), or dropping chi's NOT, left the script printing FULL-CHIP WITNESS VERIFIED while reporting 12 wrong lanes instead of 2. That is the fail-open direction discipline 1 of the README calls the only dangerous one. Honest and forged rows now come out of one `build_row(tamper=...)`, and the honest row must be EXACTLY the reference - cross-checked against keccak_ref and against model_dataflow's mirror, the one test_dataflow.py validates - before any claim about the forged row is made. Both mutations above now fail that control. The forgery is also no longer demonstrated on a lane picked by list order, which happened to be (0,0): the one lane with RHO = 0, no rotation at all. All 11 saturated lanes are forged in turn, 10 of them with a non-zero rotation, and the wrong output lanes must be a subset of the lanes that can move - the single pi lane reading the forged source, itself read by three chi lanes - which pins where the forgery leaks instead of only counting lanes. --- .../keccak/witness_fullchip.py | 275 ++++++++++-------- 1 file changed, 159 insertions(+), 116 deletions(-) diff --git a/formal_verification/keccak/witness_fullchip.py b/formal_verification/keccak/witness_fullchip.py index 6a746d404..0103b9dbe 100644 --- a/formal_verification/keccak/witness_fullchip.py +++ b/formal_verification/keccak/witness_fullchip.py @@ -11,20 +11,27 @@ BusValue changed from cols::rot_left to cols::rot_right) and therefore leaves the interaction count, the column count and the constraint count untouched. +WHY THERE IS A POSITIVE CONTROL. "The output differs from FIPS-202" is also what +a bug in the transcription BELOW produces, so on its own it proves nothing — +misreading one Dxz column, or dropping chi's NOT, both make lanes differ. So the +honest and the forged row come out of the SAME builder, and the honest one is +required to reproduce FIPS-202 exactly, cross-checked against the independent +reference and against the mirror test_dataflow.py already validates. + Reachability: the input is a real message state — all zeros except one lane at 0xFFFF...FF. That lane comes straight from the absorbed block, so this is round 0 of a permutation an attacker can request. """ from keccak_ref import RHO, RC, keccak_round +from model_dataflow import round_dataflow from field_model import (P, as_field, honest_shift, identity_holds, deviate, - rho_pi_offsets, rho_operand_bytes, theta_carry_source, - theta_operand_bytes, is_byte, THETA_RNC) + rho_pi_offsets, theta_operand_bytes, is_byte, THETA_RNC) FAIL = [] def check(cond, msg): - print(f" {'OK ' if cond else 'FALLA'} {msg}") + print(f" {'OK ' if cond else 'FAIL'} {msg}") if not cond: FAIL.append(msg) @@ -33,133 +40,169 @@ def check(cond, msg): ROUND = 0 state = [0] * 25 state[0] = ALL_ONES # one lane of the absorbed block -lanes = [[state[x + 5 * y] for y in range(5)] for x in range(5)] def to_bytes(v): return [(v >> (8 * b)) & 0xFF for b in range(8)] -# ---------------------------------------------------------------- honest row -S = [[to_bytes(lanes[x][y]) for y in range(5)] for x in range(5)] -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] - for st in range(1, 4): +def build_row(state, round_idx, tamper=None): + """One complete KECCAK_RND row. `tamper=(sx,sy)` forges that source lane's + rho decomposition with d = +1; `tamper=None` is the honest row. Returns + `(out_lanes, cols)` — every committed column the audit needs.""" + lanes = [[state[x + 5 * y] for y in range(5)] for x in range(5)] + S = [[to_bytes(lanes[x][y]) for y in range(5)] for x in range(5)] + + cxz = [[[0] * 8 for _ in range(4)] for _ in range(5)] + for x in range(5): for b in range(8): - cxz[x][st][b] = cxz[x][st - 1][b] ^ S[x][st + 1][b] - -cxz_left = [[0] * 8 for _ in range(5)] -cxz_right = [[0] * 4 for _ in range(5)] -for x in range(5): - for h in range(4): - inp = cxz[x][3][2 * h] | (cxz[x][3][2 * h + 1] << 8) - L, R = honest_shift(inp, THETA_RNC) - cxz_left[x][2 * h], cxz_left[x][2 * h + 1] = L & 0xFF, L >> 8 - cxz_right[x][h] = R - -dxz = [[0] * 8 for _ in range(5)] -for x in range(5): - rc_bytes = theta_operand_bytes(cxz_left[(x + 1) % 5], cxz_right[(x + 1) % 5]) - for b in range(8): - dxz[x][b] = cxz[(x + 4) % 5][3][b] ^ rc_bytes[b] - -theta = [[[S[x][y][b] ^ dxz[x][b] for b in range(8)] for y in range(5)] for x in range(5)] -theta_lane = [[sum(theta[x][y][b] << (8 * b) for b in range(8)) for y in range(5)] for x in range(5)] - -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[x][y] % 16 + cxz[x][0][b] = S[x][0][b] ^ S[x][1][b] + for st in range(1, 4): + for b in range(8): + cxz[x][st][b] = cxz[x][st - 1][b] ^ S[x][st + 1][b] + + cxz_left = [[0] * 8 for _ in range(5)] + cxz_right = [[0] * 4 for _ in range(5)] + for x in range(5): for h in range(4): - inp = theta[x][y][2 * h] | (theta[x][y][2 * h + 1] << 8) - L, R = honest_shift(inp, rnc) - rot_left[x][y][2 * h], rot_left[x][y][2 * h + 1] = L & 0xFF, L >> 8 - rot_right[x][y][2 * h], rot_right[x][y][2 * h + 1] = R & 0xFF, R >> 8 - -# --------------------------------------------------- pick a saturated source lane -saturated = [(x, y) for x in range(5) for y in range(5) if theta_lane[x][y] == ALL_ONES] -check(bool(saturated), f"the message state reaches theta = 0xFFFF...FF on {len(saturated)} lanes: {saturated}") -TX, TY = saturated[0] -print(f" tampering source lane ({TX},{TY}), RHO={RHO[TX][TY]}") - -# --------------------------------------------------------------- forge that lane -rnc, rbc = RHO[TX][TY] % 16, RHO[TX][TY] // 16 -in_hws = [theta[TX][TY][2 * h] | (theta[TX][TY][2 * h + 1] << 8) for h in range(4)] -dev = [deviate(*honest_shift(in_hws[h], rnc), 1) for h in range(4)] -f_right = [b for h in range(4) for b in (dev[h][1] & 0xFF, dev[h][1] >> 8)] -f_left = [-f_right[(w - 2) % 8] for w in range(8)] -rot_left[TX][TY] = f_left -rot_right[TX][TY] = f_right - - -def pi(X, Y, z): - sx, sy = (X + 3 * Y) % 5, X - a = rho_pi_offsets(RHO[sx][sy] // 16) - return rot_left[sx][sy][(z + a) % 8] + rot_right[sx][sy][(z + a - 2) % 8] - - -# --------------------------------------------------- rebuild chi / iota downstream -chi_ands = [[[0] * 8 for _ in range(5)] for _ in range(5)] -chi = [[[0] * 8 for _ in range(5)] for _ in range(5)] -for x in range(5): - for y in range(5): + inp = cxz[x][3][2 * h] | (cxz[x][3][2 * h + 1] << 8) + left, right = honest_shift(inp, THETA_RNC) + cxz_left[x][2 * h], cxz_left[x][2 * h + 1] = left & 0xFF, left >> 8 + cxz_right[x][h] = right + + dxz = [[0] * 8 for _ in range(5)] + for x in range(5): + rc_bytes = theta_operand_bytes(cxz_left[(x + 1) % 5], cxz_right[(x + 1) % 5]) for b in range(8): - p0, p1, p2 = pi(x, y, b), pi((x + 1) % 5, y, b), pi((x + 2) % 5, y, b) - chi_ands[x][y][b] = (255 - as_field(p1) % 256) & (as_field(p2) % 256) - chi[x][y][b] = (as_field(p0) % 256) ^ chi_ands[x][y][b] -iota = [chi[0][0][b] ^ to_bytes(RC[ROUND])[b] for b in range(8)] - -# ------------------------------------------------------------------ verify the row -viol = [] -for x in range(5): # 20 IS_BIT + 20 theta - for h in range(4): - if cxz_right[x][h] not in (0, 1): - viol.append(f"IS_BIT x={x} h={h}") - inp = cxz[x][3][2 * h] | (cxz[x][3][2 * h + 1] << 8) - if not identity_holds(inp, THETA_RNC, - cxz_left[x][2 * h] + 256 * cxz_left[x][2 * h + 1], - cxz_right[x][h]): - viol.append(f"theta identity x={x} h={h}") -for x in range(5): # 100 rho identities - for y in range(5): - r = RHO[x][y] % 16 + dxz[x][b] = cxz[(x + 4) % 5][3][b] ^ rc_bytes[b] + + theta = [[[S[x][y][b] ^ dxz[x][b] for b in range(8)] for y in range(5)] for x in range(5)] + + 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[x][y] % 16 + for h in range(4): + inp = theta[x][y][2 * h] | (theta[x][y][2 * h + 1] << 8) + left, right = honest_shift(inp, rnc) + rot_left[x][y][2 * h], rot_left[x][y][2 * h + 1] = left & 0xFF, left >> 8 + rot_right[x][y][2 * h], rot_right[x][y][2 * h + 1] = right & 0xFF, right >> 8 + + if tamper is not None: + # d = +1 on all four halfwords, with the byte split of left' chosen so + # every pi byte of the reader cancels to zero (necessity_rho.py, C). + tx, ty = tamper + rnc = RHO[tx][ty] % 16 + in_hws = [theta[tx][ty][2 * h] | (theta[tx][ty][2 * h + 1] << 8) for h in range(4)] + dev = [deviate(*honest_shift(in_hws[h], rnc), 1) for h in range(4)] + f_right = [b for h in range(4) for b in (dev[h][1] & 0xFF, dev[h][1] >> 8)] + rot_right[tx][ty] = f_right + rot_left[tx][ty] = [-f_right[(w - 2) % 8] for w in range(8)] + + def pi(X, Y, z): + sx, sy = (X + 3 * Y) % 5, X + a = rho_pi_offsets(RHO[sx][sy] // 16) + return rot_left[sx][sy][(z + a) % 8] + rot_right[sx][sy][(z + a - 2) % 8] + + chi_ands = [[[0] * 8 for _ in range(5)] for _ in range(5)] + 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, p1, p2 = pi(x, y, b), pi((x + 1) % 5, y, b), pi((x + 2) % 5, y, b) + chi_ands[x][y][b] = (255 - as_field(p1) % 256) & (as_field(p2) % 256) + chi[x][y][b] = (as_field(p0) % 256) ^ chi_ands[x][y][b] + iota = [chi[0][0][b] ^ to_bytes(RC[round_idx])[b] for b in range(8)] + + out = [0] * 25 + for x in range(5): + for y in range(5): + bs = iota if (x, y) == (0, 0) else chi[x][y] + out[x + 5 * y] = sum(bs[b] << (8 * b) for b in range(8)) + return out, dict(cxz=cxz, cxz_left=cxz_left, cxz_right=cxz_right, theta=theta, + rot_left=rot_left, rot_right=rot_right, pi=pi) + + +def constraint_violations(c): + """The 140 shipped constraints: 20 IS_BIT + 20 theta + 100 rho identities.""" + viol = [] + for x in range(5): for h in range(4): - inp = theta[x][y][2 * h] | (theta[x][y][2 * h + 1] << 8) - if not identity_holds(inp, r, - rot_left[x][y][2 * h] + 256 * rot_left[x][y][2 * h + 1], - rot_right[x][y][2 * h] + 256 * rot_right[x][y][2 * h + 1]): - viol.append(f"rho identity ({x},{y}) h={h}") -check(not viol, f"all 140 shipped constraints satisfied ({len(viol)} violations)") - -opviol = [f"pi({x},{y},{b})" for x in range(5) for y in range(5) for b in range(8) - if not is_byte(pi(x, y, b))] -opviol += [f"rotated_C({x},{b})" for x in range(5) - for b, v in enumerate(theta_operand_bytes(cxz_left[x], cxz_right[x])) if not is_byte(v)] -check(not opviol, f"every ByteAlu operand is a byte, so every lookup matches ({len(opviol)} bad)") - -kept = [f"({x},{y})" for x in range(5) for y in range(5) for b in range(8) - if not is_byte(rot_right[x][y][b])] -check(not kept, "rot_right stays byte-valued everywhere — the surviving check accepts it") -oor = sum(1 for x in range(5) for y in range(5) for b in range(8) - if as_field(rot_left[x][y][b]) > 255) -check(oor > 0, f"{oor} of 200 rot_left columns hold non-bytes — only the DROPPED check would object") - -# ------------------------------------------------------------------- vs FIPS-202 + if c["cxz_right"][x][h] not in (0, 1): + viol.append(f"IS_BIT x={x} h={h}") + inp = c["cxz"][x][3][2 * h] | (c["cxz"][x][3][2 * h + 1] << 8) + if not identity_holds(inp, THETA_RNC, + c["cxz_left"][x][2 * h] + 256 * c["cxz_left"][x][2 * h + 1], + c["cxz_right"][x][h]): + viol.append(f"theta identity x={x} h={h}") + for x in range(5): + for y in range(5): + rnc = RHO[x][y] % 16 + for h in range(4): + inp = c["theta"][x][y][2 * h] | (c["theta"][x][y][2 * h + 1] << 8) + if not identity_holds(inp, rnc, + c["rot_left"][x][y][2 * h] + 256 * c["rot_left"][x][y][2 * h + 1], + c["rot_right"][x][y][2 * h] + 256 * c["rot_right"][x][y][2 * h + 1]): + viol.append(f"rho identity ({x},{y}) h={h}") + return viol + + +def operand_violations(c): + bad = [f"pi({x},{y},{b})" for x in range(5) for y in range(5) for b in range(8) + if not is_byte(c["pi"](x, y, b))] + bad += [f"rotated_C({x},{b})" for x in range(5) + for b, v in enumerate(theta_operand_bytes(c["cxz_left"][x], c["cxz_right"][x])) + if not is_byte(v)] + return bad + + +def reader_lanes(sx, sy): + """The output lanes that can move when source lane (sx,sy) is forged. + + pi is a bijection, so exactly one pi lane (X,Y) reads (sx,sy) — X = sy and + Y = 2*(sx - sy) mod 5, since 3*2 = 1 mod 5 — and chi at (x,y) reads + pi(x), pi(x+1), pi(x+2), so the movable outputs are (X-k, Y), k in 0..2.""" + X = sy + Y = (2 * (sx - sy)) % 5 + return {((X - k) % 5, Y) for k in range(3)} + + +# ------------------------------------------------------------- positive control ref = keccak_round(state, RC[ROUND]) -got = [0] * 25 -for x in range(5): - for y in range(5): - bs = iota if (x, y) == (0, 0) else chi[x][y] - got[x + 5 * y] = sum(bs[b] << (8 * b) for b in range(8)) -wrong = [(i % 5, i // 5) for i in range(25) if got[i] != ref[i]] -check(bool(wrong), f"{len(wrong)} of 25 output lanes differ from FIPS-202: {wrong}") +honest, cols = build_row(state, ROUND) +check(honest == ref, "POSITIVE CONTROL: the untampered row is EXACTLY FIPS-202") +check(honest == round_dataflow(state, ROUND), + "and equals model_dataflow's mirror, the one test_dataflow.py validates") +check(not constraint_violations(cols) and not operand_violations(cols), + "the honest row satisfies all 140 constraints and every operand") + +# --------------------------------------------------------- the forgeable lanes +theta_lane = [[sum(cols["theta"][x][y][b] << (8 * b) for b in range(8)) + for y in range(5)] for x in range(5)] +saturated = [(x, y) for x in range(5) for y in range(5) if theta_lane[x][y] == ALL_ONES] +check(bool(saturated), f"the message state reaches theta = 0xFFFF...FF on {len(saturated)} lanes") +rotated = [l for l in saturated if RHO[l[0]][l[1]] % 16] +check(bool(rotated), f"{len(rotated)} of them have a NON-ZERO rotation: {rotated}") + +print("\n=== every saturated lane, forged in turn ===") +for (tx, ty) in saturated: + got, c = build_row(state, ROUND, tamper=(tx, ty)) + wrong = {(i % 5, i // 5) for i in range(25) if got[i] != ref[i]} + ok = (not constraint_violations(c) + and not operand_violations(c) + and all(is_byte(v) for x in range(5) for y in range(5) for v in c["rot_right"][x][y]) + and sum(1 for b in c["rot_left"][tx][ty] if as_field(b) > 255) > 0 + and wrong + and wrong <= reader_lanes(tx, ty)) + check(ok, f"lane ({tx},{ty}) RHO={RHO[tx][ty]:2d}: 0 violations, rot_right all bytes, " + f"{sum(1 for b in c['rot_left'][tx][ty] if as_field(b) > 255)}/8 rot_left out of range, " + f"output lanes {sorted(wrong)} wrong (readers {sorted(reader_lanes(tx, ty))})") print("\n=== VERDICT ===") print(" A one-line change to the rho ARE_BYTES pair yields a complete, reachable") print(" KECCAK_RND row with 0 constraint violations, every lookup matching, and a") -print(" wrong permutation output. Interaction/column/constraint counts unchanged.") +print(f" wrong permutation output — on all {len(saturated)} saturated lanes, {len(rotated)} of them") +print(" with a non-zero rotation. Interaction/column/constraint counts unchanged.") assert not FAIL, FAIL print("\nFULL-CHIP WITNESS VERIFIED") From 7804fa95cdb919729ac6262334517b7b7d16c4b5 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 3 Sep 2026 16:41:46 -0300 Subject: [PATCH 10/15] Run the solver-free keccak gates in CI Nothing in the repo ran anything under formal_verification/: no Makefile target, no workflow. The gate's only automated guard was the Rust digest test, and its documented remedy - re-run the directory, then update the digests - is satisfied by pasting the new constant without running anything. The daily LOC report meanwhile counts the directory as its own "formal verification" section, so those lines are reported under that heading with nothing executing them. `make verify-keccak` runs the half that needs no solver: the FIPS-202 reference anchors, the concrete mirror, the combinatorial premises, both necessity boards and the full-chip witness. About three seconds. A new workflow runs it on every pull request that touches the directory, on any base branch, so stacked PRs are covered too. The QF-BV gate itself stays manual - it needs z3's Python bindings and about three minutes - exactly as the directory README documents. --- .github/workflows/pr_formal_verification.yaml | 27 +++++++++++++++++++ Makefile | 17 +++++++++++- 2 files changed, 43 insertions(+), 1 deletion(-) create mode 100644 .github/workflows/pr_formal_verification.yaml diff --git a/.github/workflows/pr_formal_verification.yaml b/.github/workflows/pr_formal_verification.yaml new file mode 100644 index 000000000..94b31d5b3 --- /dev/null +++ b/.github/workflows/pr_formal_verification.yaml @@ -0,0 +1,27 @@ +name: Formal verification gates +on: + pull_request: + branches: ["**"] + paths: ["formal_verification/**", ".github/workflows/pr_formal_verification.yaml"] + push: + branches: ["main"] + paths: ["formal_verification/**"] + +permissions: + contents: read + +concurrency: + group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }} + cancel-in-progress: true + +jobs: + keccak: + # The solver-free scripts only. The QF-BV gate needs z3 and ~3 min; the + # directory README documents it as a manual step, and this job exists so + # that the parts which DO run unattended stop being a human obligation. + name: Keccak round gate (solver-free) + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v6 + - uses: actions/setup-python@v6 + - run: make verify-keccak diff --git a/Makefile b/Makefile index a4b05b507..8cb27bdf2 100644 --- a/Makefile +++ b/Makefile @@ -9,7 +9,7 @@ bench-math-cuda bench-prover bench-prover-cuda build check clippy fmt lint regen update-ethrex-fixture-checksums check-ethrex-fixture-checksums ethrex-real-block-fixture \ ethrex-real-block-cache ethrex-real-block-converter-cache print-real-block-fixture \ print-real-block-fixture-url \ -test-ethrex-real-block-converter regen-real-block-fixture +test-ethrex-real-block-converter regen-real-block-fixture verify-keccak UNAME := $(shell uname) @@ -640,5 +640,20 @@ lint: # too — no GPU required. Catches cuda-gated breakage that the non-cuda passes above miss. cargo clippy --workspace --all-targets --features lambda-vm-prover/cuda -- -D warnings -A clippy::op_ref +# The solver-free half of formal_verification/keccak: the FIPS-202 reference +# anchors, the concrete mirror of the round wiring, the combinatorial premises, +# the range-check necessity results and the full-chip forgery witness. Seconds, +# no solver, so CI runs it on every PR that touches the directory. The QF-BV gate +# itself (z3_parallel.py, tamper_test.py) needs z3 and ~3 min and stays manual — +# see formal_verification/keccak/README.md. +verify-keccak: + cd formal_verification/keccak && \ + python3 test_ref.py && \ + python3 test_dataflow.py && \ + python3 combinatorics.py && \ + python3 necessity_theta.py && \ + python3 necessity_rho.py && \ + python3 witness_fullchip.py + flamegraph-prover: cd crypto/stark && samply record cargo bench --bench profile_prover --features parallel From 6ddf0ba3c655e1283ec655e40c25fe308d67e049 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 3 Sep 2026 16:41:53 -0300 Subject: [PATCH 11/15] Record how each keccak necessity cell is decided The README promoted the necessity table to the headline result without saying how a cell is decided, which left the two "implied" rows reading as bare assertions. It now names the mechanism - the operand window, the integrality step, the complete sweep - and says which single configuration has no per-column window and is therefore decided by a witness instead. It also records what the two implied halves are worth, because they are not the same kind of saving: rho's is 100 AreBytes sends, theta's is 20 degree-3 polynomial constraints, which are the reason this AIR declares max_degree 3. Neither is proposed as an optimization here. The file list and the run instructions follow the code: `combinatorics.py` carries the theta premise and is imported rather than run by hand, the necessity scripts sweep rather than sample, the witness has a positive control, and `make verify-keccak` is the one command CI runs. --- formal_verification/keccak/README.md | 53 +++++++++++++++++++++++----- 1 file changed, 45 insertions(+), 8 deletions(-) diff --git a/formal_verification/keccak/README.md b/formal_verification/keccak/README.md index 9abc9ccfb..f7223f5a3 100644 --- a/formal_verification/keccak/README.md +++ b/formal_verification/keccak/README.md @@ -101,6 +101,29 @@ Each helper lookup is modeled by its contract, not its implementation: being a single bit; in ρ, `right` is a halfword and `d = ±1` fits exactly at saturation. + **How each cell is decided, and why not by comparing two bounds.** Dropping a + check does not free its column: the ByteAlu operand that reads it still + confines it to `[−255, 255]`, as long as the other summand is bounded + (`operand_summand_window`, resting on the read-once premise — + `combinatorics.py` sections 3 and 6; a column read *twice* would need the + intersection of two windows). Only with that window does the deviation `d` + become an integer at all, which is what `difference_form_is_exact` checks: + over the field `2¹⁶` is invertible, so an unbounded `right` admits a + full-size solution for *every* `left` and no argument about small `d` means + anything. With both intervals in hand, `surviving_deviation` sweeps **all + 2¹⁶ input halfwords** against them and returns either "pinned" or the first + survivor — and asserts the honest pair lies inside the modelled intervals, + which is what catches a window modelled wrongly. The "both dropped" row is + the one configuration with no per-column window at all (the operand bounds + only the *sum* of two unchecked columns), so it is decided by an explicit + witness instead. + + **The two implied halves are not the same kind of saving.** ρ's is 100 + `AreBytes` sends. θ's is 20 *polynomial* constraints (`IS_BIT`, μ-gated, + degree 3 — the reason `KeccakRndConstraints` declares `max_degree() = 3`). + Neither is proposed here as an optimization; what the result bounds is the + ceiling: 100 of ρ's 200 sends, not 200. + The model's pin is a sound *consequence* of the shipped constraints today, which is why the current board is meaningful; what it is not is a test that those constraints are still there. **The `24/24 UNSAT` verdict is conditional on the @@ -127,8 +150,9 @@ Each helper lookup is modeled by its contract, not its implementation: decomposition is ambiguous. QF-BV proves the wiring given the bound; proving the bound *suffices* mod `p` needs an integer/field model — that is what `field_model.py` and the two `necessity_*.py` scripts are, and their result is the - table in discipline 1. Run them whenever the shift identities or their range - checks change. + table in discipline 1. `make verify-keccak` runs them, and CI runs + that on every PR touching this directory — so unlike the QF-BV gate they are + not a human obligation. 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 @@ -230,17 +254,30 @@ check that changed status, and nothing outside this directory records that. - `field_model.py` — the companion **integer-mod-`p`** model of the inline θ/ρ shift identities, with a switch per range check. This is the piece the next chip copies when its bounds are enforced by an identity rather than a lookup. -- `combinatorics.py` — the solver-free premises the ρ result rests on: π is a - bijection on the lanes, all 400 byte columns are read exactly once by a pi operand, - the pi offsets are even, and `theta = 0xFFFF…FF` saturates every lane. +- `combinatorics.py` — the solver-free premises the θ and ρ results rest on: π is a + bijection on the lanes, all 400 ρ byte columns are read exactly once by a pi + operand, the pi offsets are even, `theta = 0xFFFF…FF` saturates every lane, and the + four θ carries are a permutation of the four `rotated_C` low bytes. Exposed as + `premises()` and **imported** by both necessity scripts, so it cannot be skipped. - `necessity_theta.py`, `necessity_rho.py` — which range checks are load-bearing and - which are implied, per configuration, with the forged witnesses. + which are implied: one interval per column per configuration, decided by a complete + sweep over all 2¹⁶ input halfwords, plus the forged witnesses for the + configurations that have no per-column window. - `witness_fullchip.py` — the ρ forgery as a complete KECCAK_RND row from a reachable - message state: 0 constraint violations, every lookup matching, wrong output. + message state: 0 constraint violations, every lookup matching, wrong output, on + every saturated lane. Honest and forged rows come from one builder and the honest + one is required to be exactly FIPS-202, because "the output differs" is also what a + bug in the script itself produces. ## Running the gate -z3's Python bindings are the only dependency (no cargo, no repo build): +The solver-free half is one command, and it is the half CI runs: + +``` +make verify-keccak # reference, mirror, premises, necessity, witness +``` + +The QF-BV gate itself needs z3's Python bindings (no cargo, no repo build): ``` pip install z3-solver # if not already importable From c98bca4559899dd9b7a61832486108b4508f5d02 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 8 Sep 2026 13:48:56 -0300 Subject: [PATCH 12/15] Decide the byte split, not just the halfword The necessity sweep parameterised deviations by `d` on the PACKED halfword, and the identity reads a byte pair only as `lo + 256*hi`: a pair also admits (lo, hi) -> (lo + 256k, hi - k), same packed value, identity satisfied exactly, invisible to any sweep over `d`. Chi and Dxz read the two bytes separately, so the two configurations whose unchecked column is a byte pair - rho B and theta B - were being decided on one axis out of two. Checked against the full-chip builder: redistributing rot_right by k = -1 leaves all 140 constraints satisfied, and only the pi operand objects. The verdicts do not change, the argument now covers them. Where the pair keeps its range checks the split is pinned by their width, and 256 admitted values is exactly the packing radix; where it does not, it is pinned by the single operand byte that reads each half next to a summand the checked side pinned, since that sum moves by 256k and was already a byte. That the split moves in integer steps of 256 at all is this axis's own integrality step, and it is checked alongside: over the field 256 is invertible, so the redistributions are the whole field until the operand windows on both bytes keep `lo + 256*hi` below p, which is what `difference_form_is_exact` does for the packed axis. All three checks are falsifiable and both boards run the controls: one bit wider and the range check stops pinning the split, an unbounded companion puts k back over the field, and in the "both dropped" configuration the unchecked companion absorbs the 256k, so the split is as free as the packed value. Two citations inside the same argument were wrong. The docstring claimed every magnitude stays under 2**18, which holds only for theta with its carry checked - it is 2**24 without it and 2**32.6 for every rho configuration, against a p/2 of 2**63 - and it now points at the per-configuration check instead of asserting a number. Theta's LEFT_OPERAND_ONLY took its high half from BYTE, the range check that configuration has just dropped, when the bound comes from the operand byte that reads that half alone. And the rho docstring credited the operand window for configuration A, which drops nothing. --- formal_verification/keccak/README.md | 28 +++++- formal_verification/keccak/field_model.py | 94 ++++++++++++++++++- formal_verification/keccak/necessity_rho.py | 45 +++++++-- formal_verification/keccak/necessity_theta.py | 45 ++++++++- 4 files changed, 194 insertions(+), 18 deletions(-) diff --git a/formal_verification/keccak/README.md b/formal_verification/keccak/README.md index f7223f5a3..99ad5783f 100644 --- a/formal_verification/keccak/README.md +++ b/formal_verification/keccak/README.md @@ -116,7 +116,30 @@ Each helper lookup is modeled by its contract, not its implementation: which is what catches a window modelled wrongly. The "both dropped" row is the one configuration with no per-column window at all (the operand bounds only the *sum* of two unchecked columns), so it is decided by an explicit - witness instead. + witness instead — and only ρ's is carried up to a complete row + (`witness_fullchip.py`), because ρ's is the claim this directory makes about + the *shipped* chip: a check the QF-BV gate treats as redundant is + load-bearing. θ's "both dropped" witness stays at four halfwords on purpose — + it bounds what θ could ever save, and an error in it would only keep a + redundant constraint, never license dropping a live one. + + **That sweep decides the packed halfword, which is only half the question.** + The identity reads a byte pair as `lo + 256·hi` and nothing else, so + `(lo + 256k, hi − k)` satisfies it exactly at an honest packed value — a + redistribution no sweep over `d` can see, while χ and Dxz read the two bytes + *separately*. The split is pinned by a second argument: where the pair keeps + its range checks, by their width (`checked_split_is_unique`, and 256 admitted + values is exactly the packing radix — a check one bit wider would not pin the + split, which is the control the boards run); where it does not, by the single + operand byte that reads each half (`surviving_byte_split`, read-once again), + whose sum moves by `256k` and was already a byte, so `k = 0`. That the split + moves in integer steps of 256 at all is the axis's own version of the + integrality step (`split_form_is_exact`): over the field `256` is invertible, + so the redistributions are the whole field until the operand windows on *both* + bytes keep `lo + 256·hi` below `p`. The negative + control for that one is the "both dropped" configuration itself: with nothing + checking the companion either, it absorbs the `256k` and the split is as free + as the packed value. **The two implied halves are not the same kind of saving.** ρ's is 100 `AreBytes` sends. θ's is 20 *polynomial* constraints (`IS_BIT`, μ-gated, @@ -252,7 +275,8 @@ check that changed status, and nothing outside this directory records that. modeled equations, validated against the reference over random/structured inputs and confirmed to move under each injected bug. - `field_model.py` — the companion **integer-mod-`p`** model of the inline θ/ρ shift - identities, with a switch per range check. This is the piece the next chip copies + identities, with a switch per range check, deciding both axes a byte pair has: + the packed deviation and the byte split. This is the piece the next chip copies when its bounds are enforced by an identity rather than a lookup. - `combinatorics.py` — the solver-free premises the θ and ρ results rest on: π is a bijection on the lanes, all 400 ρ byte columns are read exactly once by a pi diff --git a/formal_verification/keccak/field_model.py b/formal_verification/keccak/field_model.py index 5c68df0a6..2cd0ca5c0 100644 --- a/formal_verification/keccak/field_model.py +++ b/formal_verification/keccak/field_model.py @@ -19,10 +19,11 @@ THE DIFFERENCE FORM (why no `% p` appears below). If `(L, R)` satisfies the identity then so does `(L - 2**16 * d, R + d)` for any `d`, and those are the ONLY other solutions. So instead of solving over the field we parameterise the -deviation directly by `d` per halfword. Every magnitude then stays under 2**18, -far below `p`, so the field equation and the integer equation coincide and the -whole analysis is exact integer arithmetic. The field enters in exactly one -place: a committed column may hold a NEGATIVE integer (as `p - k`), because +deviation directly by `d` per halfword, which is exact integer arithmetic for +as long as every magnitude stays far below `p`: 2**18 for theta with its carry +checked, 2**24 without it, and 2**32.6 for every rho configuration, against a +`p/2` of 2**63. `difference_form_is_exact` checks that per configuration rather +than trusting this sentence. The field enters in exactly one place: a committed column may hold a NEGATIVE integer (as `p - k`), because nothing bounds it once its range check is gone. `as_field` marks those. WHAT BOUNDS THE DEVIATION. Two things, and which one bites is the whole result: @@ -32,6 +33,16 @@ table holds only byte rows, so the operand must be a byte, which leaves a residual window on `left` even with no range check of its own. Whether `d = +/-1` fits inside that window is what decides necessity. + +THE SECOND AXIS: THE BYTE SPLIT. `d` is not the only freedom, because the chip +commits BYTES and the identity reads a pair only as `lo + 256*hi`. So +`(lo + 256*k, hi - k)` satisfies the identity exactly, leaves the packed value +honest, and no sweep over `d` can see it -- while chi and Dxz read the two bytes +SEPARATELY. A pair whose packed value is pinned therefore still needs its split +pinned, and that is a second question with its own two answers: +`checked_split_is_unique` for a pair that kept its range checks, and +`surviving_byte_split` for one that lost them, whose split is pinned by the +operand byte that reads each half instead. """ P = 2**64 - 2**32 + 1 # Goldilocks @@ -121,6 +132,10 @@ def is_byte(v): # two "implied" verdicts hold. BYTE = (0, 255) BIT = (0, 1) +# Not a contract but a wiring fact (cols::cxz_right_bit_for_byte): the odd Dxz +# operand bytes take no carry, so such a byte IS the operand, and the window the +# operand leaves it is the whole byte range. +NO_CARRY = (0, 0) def operand_summand_window(other): @@ -187,3 +202,74 @@ def surviving_deviation(rnc, left_bounds, right_bounds): if lo_l <= dev_left <= hi_l and lo_r <= dev_right <= hi_r: return in_hw, d return None + + +def checked_split_is_unique(bounds=BYTE): + """Given a PINNED packed value, does a range check pin the two bytes? + + Uniqueness of a split is a property of the CHECK's width, not of the + identity, which sees only `lo + 256*hi`: complete over every `lo` the check + admits, `lo + 256*k` has to leave the interval for every `k != 0`; the two + tested cover all of them, since the deviation grows with `|k|`, so escaping + at one step escapes at every further one. It holds for a byte check, whose + 256 values are exactly the packing radix -- and it + stops holding one bit wider, which is the sensitivity control the necessity + boards run alongside. This is what makes the CHECKED side of a configuration + honest byte by byte, the premise `surviving_byte_split` then leans on. + """ + lo_b, hi_b = bounds + return all(not lo_b <= lo + 256 * k <= hi_b + for lo in range(lo_b, hi_b + 1) for k in (-1, 1)) + + +def split_form_is_exact(companion): + """Is `lo + 256*hi = packed` the same statement over the field and over Z? + + `surviving_byte_split` parameterises the split by an INTEGER `k`, and over + the field the packed value alone allows anything: `256` is invertible, so + every `lo` has its `hi` and the redistributions are the whole field, not a + sequence of steps of 256. What collapses them to integer ones is the operand + window on BOTH bytes of the pair -- each is read by one operand byte, so each + is small -- which keeps `lo + 256*hi` far below `p`, making the field + equation the integer equation and `k = hi_honest - hi` an integer. + + This is the split axis's analogue of `difference_form_is_exact`, and it fails + the same way: a byte with no window at all puts `k` back over the field. + """ + window = operand_summand_window(companion) + span = max(abs(window[0]), abs(window[1])) + return span + 256 * span < P // 2 + + +def surviving_byte_split(companion, companion_moves=(0,)): + """Is the split of an UNCHECKED pair pinned by the operand bytes reading it? + + The pair's packed value is pinned (`surviving_deviation`), each of its bytes + is read by exactly ONE ByteAlu operand byte (read-once, combinatorics + sections 3 and 6) alongside a summand in `companion`, and those windows are + what make `k` an integer in the first place (`split_form_is_exact`). + Redistributing the pair + by `k` moves that operand sum by `256*k`, so the sweep below asks, over every + (byte, companion) pair an honest row can present -- their sum is a byte, + since the honest row passes the operand lookup -- whether the moved sum is a + byte too. + + `companion_moves` is what that summand may do ITSELF, and it is the whole + reason the answer is configuration-dependent: `(0,)` when the checked side + pinned it to its honest value (`checked_split_is_unique`), and +/-256 when + nothing checks it either -- the "both dropped" configuration, where the + redistribution is absorbed and the split is as free as the packed value. + + Returns None when the split is pinned, else `(byte, companion, k, move)`. + With `companion_moves = (0,)` the two non-zero `k` are exhaustive: a survivor + needs both sums inside [0, 255], so it needs `|256*k| <= 255`. + """ + for byte in range(256): + for other in range(companion[0], companion[1] + 1): + if not is_byte(byte + other): + continue + for k in (-1, 1): + for move in companion_moves: + if is_byte(byte + 256 * k + other + move): + return byte, other, k, move + return None diff --git a/formal_verification/keccak/necessity_rho.py b/formal_verification/keccak/necessity_rho.py index 5f0ac2474..913b666cd 100644 --- a/formal_verification/keccak/necessity_rho.py +++ b/formal_verification/keccak/necessity_rho.py @@ -13,12 +13,19 @@ pi[z] = rot_left[l(z)] + rot_right[r(z)] must be a byte so dropping one column's check does not free it: the operand still confines it -(`operand_summand_window`), which is what makes configurations A and B sound and -is the step a bound-vs-bound comparison cannot express. Premises live in -combinatorics.py and are imported below, not left to be run by hand: the -offsets are even, so a pi halfword reads one source halfword as -P_h = L_(h+A) + R_(h+A-1), and every one of the 400 byte columns is read exactly -once -- a column read twice would need the intersection of two windows. +(`operand_summand_window`), which is what makes configuration B sound -- A drops +nothing, its two checks pin both pairs outright -- and is the step a +bound-vs-bound comparison cannot express. Premises live in combinatorics.py and +are imported below, not left to be run by hand: the offsets are even, so a pi +halfword reads one source halfword as P_h = L_(h+A) + R_(h+A-1), and every one +of the 400 byte columns is read exactly once -- a column read twice would need +the intersection of two windows. + +TWO AXES. The identity constrains the PACKED halfword, so every configuration +is decided twice. `surviving_deviation` settles the packed value; the byte split +`(lo, hi) -> (lo + 256k, hi - k)` keeps that value and the identity untouched, +so the first sweep is blind to it, and what settles it is pi reading the two +bytes separately. RESULT, and it is asymmetric — unlike theta, here ONE check is load-bearing on its own. `left` and `right` enter the identity with weights 1 and 2**16, so @@ -29,7 +36,8 @@ from field_model import (P, BYTE, as_field, honest_shift, identity_holds, deviate, difference_form_is_exact, operand_summand_window, packed_pair_bounds, rho_pi_offsets, rho_operand_bytes, - surviving_deviation, is_byte) + surviving_deviation, checked_split_is_unique, + split_form_is_exact, surviving_byte_split, is_byte) premises(verbose=False) @@ -63,6 +71,25 @@ def check(cond, msg): f"{len(RNCS)} rotations x 2**16 inputs" f"{'' if all(s is None for _, s in surv) else f' — SURVIVORS {[s for s in surv if s[1]][:2]}'}") +print("\n=== A / B: the byte SPLIT of each pair, which the packed sweep cannot see ===") +# A pinned packed value still admits (lo, hi) -> (lo + 256k, hi - k), which the +# identity accepts exactly. rot_left keeps its checks in both configurations, so +# they pin its split; rot_right, unchecked in B, is pinned by the single pi +# operand byte that reads each of its bytes next to a pinned rot_left byte. +check(checked_split_is_unique(BYTE), + "a range-checked pair has ONE split per pinned packed value -> rot_left's bytes are honest") +check(not checked_split_is_unique((0, 511)), + "control: it is the check's WIDTH doing that — one bit wider and the split is free again") +check(split_form_is_exact(BYTE), + "the pi operand windows keep lo + 256*hi below p -> the split moves in integer steps of 256") +check(not split_form_is_exact((0, P // 4)), + "control: with an unbounded companion it does not, and k is back over the whole field") +split = surviving_byte_split(BYTE) +check(split is None, + "B: redistributing rot_right by k moves its pi operand byte by 256k -> no " + "(rot_right byte, rot_left byte, k != 0) leaves that operand a byte" + f"{'' if split is None else f' — SURVIVOR {split}'}") + print("\n=== C: rot_left's check dropped — the sweep already says forgeable ===") surv_c = {rnc: surviving_deviation(rnc, OPERAND_ONLY, CHECKED) for rnc in RNCS} check(all(s is not None for s in surv_c.values()), @@ -131,6 +158,10 @@ def check(cond, msg): okid = all(identity_holds(in_hws[j], rnc, L[j], R[j]) for j in range(4)) hits = [(L[(h + A) % 4] + R[(h + A - 1) % 4]) % P for h in range(4)] == [q % P for q in Q] free += okid and hits +split_d = surviving_byte_split(BYTE, companion_moves=(-256, 256)) +check(split_d is not None, + f"and so is the byte SPLIT, since the companion rot_left byte can now absorb the " + f"redistribution: survivor (byte, companion, k, move) = {split_d}") check(free == 25, f"the forged pi halfwords equal the ARBITRARY target on {free}/25 lanes " f"(det = 1 - 2**64 = {(1 - 2**64) % P} mod p, invertible). Per-byte\n" f" realizability is the construction exhibited in C.") diff --git a/formal_verification/keccak/necessity_theta.py b/formal_verification/keccak/necessity_theta.py index 204e4b3ca..5b8ba220e 100644 --- a/formal_verification/keccak/necessity_theta.py +++ b/formal_verification/keccak/necessity_theta.py @@ -24,13 +24,20 @@ there is no per-column window, and the explicit witness below is what decides it. +THE SECOND AXIS. The identity only ever reads a byte pair as `lo + 256*hi`, so a +pinned packed value is half the question: the split `(lo + 256k, hi - k)` +satisfies the identity too, and what pins it is the Dxz operand bytes that read +the halves one at a time (`surviving_byte_split`). + Board: A/B/C sound, D forgeable. """ from combinatorics import premises -from field_model import (P, THETA_RNC, BYTE, BIT, as_field, honest_shift, - identity_holds, deviate, difference_form_is_exact, - operand_summand_window, packed_pair_bounds, - surviving_deviation, theta_operand_bytes, is_byte) +from field_model import (P, THETA_RNC, BYTE, BIT, NO_CARRY, as_field, + honest_shift, identity_holds, deviate, + difference_form_is_exact, operand_summand_window, + packed_pair_bounds, surviving_deviation, + checked_split_is_unique, split_form_is_exact, + surviving_byte_split, theta_operand_bytes, is_byte) premises(verbose=False) @@ -49,7 +56,8 @@ def check(cond, msg): # Cxz_right IS_BIT, or -- with that gone -- the Dxz operand alongside a # range-checked Cxz_left byte. LEFT_CHECKED = packed_pair_bounds(BYTE, BYTE) -LEFT_OPERAND_ONLY = packed_pair_bounds(operand_summand_window(BIT), BYTE) +LEFT_OPERAND_ONLY = packed_pair_bounds(operand_summand_window(BIT), + operand_summand_window(NO_CARRY)) RIGHT_CHECKED = BIT RIGHT_OPERAND_ONLY = operand_summand_window(BYTE) @@ -75,6 +83,28 @@ def check(cond, msg): check(surv is None, f"{name}: left in {left_b}, right in {right_b} -> " f"{'no deviation survives any of the 2**16 inputs' if surv is None else f'SURVIVOR {surv}'}") + +print("\n=== the byte SPLIT of Cxz_left, which the packed sweep cannot see ===") +# Same second axis: (lo, hi) -> (lo + 256k, hi - k) keeps both the packed value +# and the identity. A and C keep the ARE_BYTES pair, which pins the split; B +# drops it, and what pins it there is the Dxz operand byte reading the low half +# next to the carry (the odd half is read alone, the `NO_CARRY` end of the sweep). +check(checked_split_is_unique(BYTE), + "A/C: ARE_BYTES ships -> ONE split per pinned packed value") +check(not checked_split_is_unique((0, 511)), + "control: it is the check's WIDTH doing that — one bit wider and the split is free again") +check(split_form_is_exact(BIT), + "the Dxz operand windows keep lo + 256*hi below p -> the split moves in integer steps of 256") +check(not split_form_is_exact((0, P // 4)), + "control: with an unbounded companion it does not, and k is back over the whole field") +split = surviving_byte_split(BIT) +check(split is None, + "B: redistributing Cxz_left by k moves its rotated_C byte by 256k -> no " + "(Cxz_left byte, carry, k != 0) leaves that operand a byte" + f"{'' if split is None else f' — SURVIVOR {split}'}") +print(" C drops IS_BIT instead, and Cxz_right is a single column: no split to pin.") + +print("\n=== the parity argument behind B, spelled out ===") print(" B is the interesting one: d=+1 needs L' = L - 2**16 >= -1, i.e. L = 65535,") print(" and L is EVEN, so the sweep finds nothing. d=-1 needs L' > 65535.") @@ -103,6 +133,11 @@ def check(cond, msg): print(f" forged Cxz_left (as field elements) = {[as_field(v) for v in frg_left[:2]]}...") print(f" forged Cxz_right = {frg_right}") +split_d = surviving_byte_split(BIT, companion_moves=(-256, 256)) +check(split_d is not None, + f"and the byte SPLIT of Cxz_left is free too, since an unchecked carry absorbs the " + f"redistribution: survivor (byte, carry, k, move) = {split_d}") + # generality: the four carries form a cycle, so an arbitrary target is reachable det = (2**16) ** 4 - 1 check(det % P != 0, f"det(2**16*I - S) = 2**64-1 = {det % P} mod p is invertible -> ANY target output") From 28f9e9014595d9e1e49fac1861fcf7f2b1c2fd74 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 8 Sep 2026 13:48:57 -0300 Subject: [PATCH 13/15] Read the saturation premise through honest_shift Premise 5 was one expression whose meaning depended on counting parentheses to see that the conditional covered only the second summand. It reads the decomposition through `honest_shift` now - the same function the necessity boards use, so the premise and the boards cannot disagree about what the split is - and it names the offending lanes when it fails instead of collapsing to a bare False. Also drops an import left unused in the full-chip witness. --- formal_verification/keccak/combinatorics.py | 16 ++++++++++++---- formal_verification/keccak/witness_fullchip.py | 2 +- 2 files changed, 13 insertions(+), 5 deletions(-) diff --git a/formal_verification/keccak/combinatorics.py b/formal_verification/keccak/combinatorics.py index aa39521d9..dd72677a2 100644 --- a/formal_verification/keccak/combinatorics.py +++ b/formal_verification/keccak/combinatorics.py @@ -12,7 +12,7 @@ the checks below cannot be skipped by forgetting to run this file first. """ from keccak_ref import RHO -from field_model import rho_pi_offsets, theta_carry_source +from field_model import honest_shift, rho_pi_offsets, theta_carry_source def premises(verbose=True): @@ -71,9 +71,17 @@ def say(msg): say("\n=== (5) theta = all-ones saturates every pi halfword, for EVERY rotation ===") # left + right = 0xFFFF whatever rnc is, which is why config C forges on all 25. - sat = all(((0xFFFF << (RHO[x][y] % 16)) & 0xFFFF) + (0xFFFF >> (16 - (RHO[x][y] % 16)) - if RHO[x][y] % 16 else 0) == 0xFFFF for x in range(5) for y in range(5)) - check(sat, "left + right = 0xFFFF for all 25 lanes -> pi = 0xFF..FF, the saturation config C needs") + # Read through honest_shift rather than open-coded shifts, so this premise and + # the necessity boards cannot disagree about what the decomposition is. + unsaturated = [] + for x in range(5): + for y in range(5): + left, right = honest_shift(0xFFFF, RHO[x][y] % 16) + if left + right != 0xFFFF: + unsaturated.append((x, y, left, right)) + check(not unsaturated, + "left + right = 0xFFFF for all 25 lanes -> pi = 0xFF..FF, the saturation config C needs" + f"{'' if not unsaturated else f' — {unsaturated[:2]}'}") say("\n=== (6) the theta analogue: every Cxz_right carry column is read EXACTLY once ===") # cols::cxz_right_bit_for_byte sends the carry of halfword h-1 to the LOW byte diff --git a/formal_verification/keccak/witness_fullchip.py b/formal_verification/keccak/witness_fullchip.py index 0103b9dbe..13027648e 100644 --- a/formal_verification/keccak/witness_fullchip.py +++ b/formal_verification/keccak/witness_fullchip.py @@ -24,7 +24,7 @@ """ from keccak_ref import RHO, RC, keccak_round from model_dataflow import round_dataflow -from field_model import (P, as_field, honest_shift, identity_holds, deviate, +from field_model import (as_field, honest_shift, identity_holds, deviate, rho_pi_offsets, theta_operand_bytes, is_byte, THETA_RNC) FAIL = [] From 4b3efa817442049f9d0f8dd09df47ac5507c675d Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 8 Sep 2026 13:48:57 -0300 Subject: [PATCH 14/15] Run the keccak gate when its recipe moves The path filter listed the directory and the workflow but not the Makefile, so a pull request that edits the `verify-keccak` recipe - the one command this job runs - would not run it. Both triggers now include it. The python version is pinned as well: `setup-python` was left to install whatever the runner image ships, which drifts with the image. --- .github/workflows/pr_formal_verification.yaml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/.github/workflows/pr_formal_verification.yaml b/.github/workflows/pr_formal_verification.yaml index 94b31d5b3..2e0e7251e 100644 --- a/.github/workflows/pr_formal_verification.yaml +++ b/.github/workflows/pr_formal_verification.yaml @@ -2,10 +2,13 @@ name: Formal verification gates on: pull_request: branches: ["**"] - paths: ["formal_verification/**", ".github/workflows/pr_formal_verification.yaml"] + paths: + - "formal_verification/**" + - "Makefile" # the recipe this job runs + - ".github/workflows/pr_formal_verification.yaml" push: branches: ["main"] - paths: ["formal_verification/**"] + paths: ["formal_verification/**", "Makefile"] permissions: contents: read @@ -24,4 +27,8 @@ jobs: steps: - uses: actions/checkout@v6 - uses: actions/setup-python@v6 + with: + # Pinned: the scripts are pure integer arithmetic, so the version only + # matters for reproducing a failure, and an unpinned runner drifts. + python-version: "3.12" - run: make verify-keccak From 982d552fe2f6c6329c1317baef2345784a92f98d Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 8 Sep 2026 13:48:57 -0300 Subject: [PATCH 15/15] Report both keccak digests, not just the first The two assertions short-circuited, so a bus rewiring hid whether the constraint IR had moved as well, and the failure printed neither computed value. Both are computed up front and reported together with their digests, so an intentional change can be pasted back in one pass. The doc comment gains the failure that needs no python board at all: the IR digest is taken over ConstraintProgram's Debug output, so a field added to the IR types in stark, or a Debug reworded, moves it with this round untouched - check the IR's history before re-running the gates. It also said the witness leaves "two output lanes" differing from FIPS-202; measured, the set is one to three, exactly the lanes chi reaches from the forged source. --- prover/src/tests/trace_builder_tests.rs | 50 +++++++++++++++++-------- 1 file changed, 35 insertions(+), 15 deletions(-) diff --git a/prover/src/tests/trace_builder_tests.rs b/prover/src/tests/trace_builder_tests.rs index f0acf54f0..ee2ae33f3 100644 --- a/prover/src/tests/trace_builder_tests.rs +++ b/prover/src/tests/trace_builder_tests.rs @@ -799,13 +799,19 @@ mod keccak_tests { /// its bitvectors, so it prints `VERIFIED` either way — see its README, /// discipline 1. `witness_fullchip.py` there exhibits the forgery as a /// complete, reachable round with zero constraint violations, every lookup - /// matching, and two output lanes differing from FIPS-202. + /// matching, and one to three output lanes differing from FIPS-202 — exactly + /// the lanes χ can reach from the forged source. /// /// A failure here is not necessarily a bug: it means the round's wiring or its - /// constraint bodies changed. Re-run `formal_verification/keccak/` in full (the - /// four gates plus `combinatorics.py`, `necessity_theta.py`, - /// `necessity_rho.py`, `witness_fullchip.py`), confirm the expected board, then + /// constraint bodies changed. Re-run `formal_verification/keccak/` in full + /// (`make verify-keccak` plus the z3 gate), confirm the expected board, then /// update the digests below in the same commit. + /// + /// One failure needs no board at all: the IR digest is taken over + /// `ConstraintProgram`'s **`Debug`** output, so a change to that `Debug` — a + /// field added to the IR types in `stark`, a `Debug` impl reworded, a field + /// element printed differently — moves it with this round untouched. Check + /// `git log crypto/stark/src/constraint_ir/` before re-running anything. #[test] fn test_keccak_rnd_air_structure_is_pinned() { use crate::tables::types::{GoldilocksExtension, GoldilocksField}; @@ -814,6 +820,9 @@ mod keccak_tests { // BusInteraction is not Debug, so serialise its public fields explicitly: // bus id, direction, multiplicity, and every BusValue (which carries the // column indices, packings and linear-term coefficients). + const BUS_DIGEST: u64 = 0x0027_e508_0abb_991f; + const IR_DIGEST: u64 = 0x83a3_3324_8bcb_a374; + let bus: String = keccak_rnd::bus_interactions() .iter() .map(|i| { @@ -823,22 +832,33 @@ mod keccak_tests { ) }) .collect(); - assert_eq!( - fnv1a64(bus.as_bytes()), - 0x0027_e508_0abb_991f, - "KECCAK_RND bus wiring changed (bus ids, multiplicities, column indices \ - or linear-term coefficients). See this test's doc comment." - ); + let bus_digest = fnv1a64(bus.as_bytes()); let n = keccak_rnd::KeccakRndConstraints.meta().len(); let mut cb = CaptureBuilder::::new(); keccak_rnd::KeccakRndConstraints.eval(&mut cb); let (prog, _) = cb.finish(n); - assert_eq!( - fnv1a64(format!("{prog:?}").as_bytes()), - 0x83a3_3324_8bcb_a374, - "KECCAK_RND constraint IR changed (op tree, dimensions, field constants \ - or roots). See this test's doc comment." + let ir_digest = fnv1a64(format!("{prog:?}").as_bytes()); + + // Both are reported together: whoever updates one wants to know whether + // the other moved too, and a short-circuiting `assert_eq!` pair hides it. + let mut moved = Vec::new(); + if bus_digest != BUS_DIGEST { + moved.push(format!( + "bus wiring (bus ids, multiplicities, column indices or \ + linear-term coefficients): {bus_digest:#018x}" + )); + } + if ir_digest != IR_DIGEST { + moved.push(format!( + "constraint IR (op tree, dimensions, field constants or roots): \ + {ir_digest:#018x}" + )); + } + assert!( + moved.is_empty(), + "KECCAK_RND {} — see this test's doc comment for what to do", + moved.join(", and ") ); } }