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 diff --git a/formal_verification/keccak/README.md b/formal_verification/keccak/README.md index 2cb7b579a..f7223f5a3 100644 --- a/formal_verification/keccak/README.md +++ b/formal_verification/keccak/README.md @@ -79,14 +79,56 @@ 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 - (`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 - 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. + + **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 + 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 @@ -106,7 +148,11 @@ 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. `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 @@ -141,31 +187,34 @@ 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. - -**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 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. + +**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 @@ -202,10 +251,33 @@ 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 θ 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: 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, 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 @@ -216,10 +288,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). diff --git a/formal_verification/keccak/combinatorics.py b/formal_verification/keccak/combinatorics.py new file mode 100644 index 000000000..aa39521d9 --- /dev/null +++ b/formal_verification/keccak/combinatorics.py @@ -0,0 +1,95 @@ +""" +The pure-combinatorial premises the theta and rho necessity arguments rest on. + +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, 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) + + 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") + + 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]}'}") + + 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") + + 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") + + 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") + + assert not failed, failed + if verbose: + 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 new file mode 100644 index 000000000..5c68df0a6 --- /dev/null +++ b/formal_verification/keccak/field_model.py @@ -0,0 +1,189 @@ +""" +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 + + +# --- 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/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/necessity_rho.py b/formal_verification/keccak/necessity_rho.py new file mode 100644 index 000000000..5f0ac2474 --- /dev/null +++ b/formal_verification/keccak/necessity_rho.py @@ -0,0 +1,144 @@ +""" +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 + +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 keccak_ref import RHO +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 'FAIL'} {msg}") + if not cond: + FAIL.append(msg) + + +LANES = [(x, y) for x in range(5) for y in range(5)] +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 +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 ===") +# 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: + 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-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)) + 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" + 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") +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..204e4b3ca --- /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) + +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 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 'FAIL'} {msg}") + if not cond: + FAIL.append(msg) + + +# 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") +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 / 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) +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)") +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}") + +# 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.") +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") 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/witness_fullchip.py b/formal_verification/keccak/witness_fullchip.py new file mode 100644 index 000000000..0103b9dbe --- /dev/null +++ b/formal_verification/keccak/witness_fullchip.py @@ -0,0 +1,208 @@ +""" +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. + +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, theta_operand_bytes, is_byte, THETA_RNC) + +FAIL = [] + + +def check(cond, msg): + print(f" {'OK ' if cond else 'FAIL'} {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 + + +def to_bytes(v): + return [(v >> (8 * b)) & 0xFF for b in range(8)] + + +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][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) + 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): + 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): + 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]) +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(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") 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 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 {