docs(formal-verification): keccak z3/QF-BV gate — the verification baseline

[MauroToscano]

What this is

A standalone, reusable template for machine-checking that a bit/byte hash
chip's per-round transition wiring computes the function it claims, using z3 in
the quantifier-free bitvector theory (QF-BV). It lands the keccak
round-wiring verification under a clean, chip-agnostic home
(thoughts/formal-verification/keccak/) and rewrites the README as a generic
method the next chip gate should copy.

Verification code only — no constraint or performance change. python/z3, no
cargo. The z3 gate previously lived bundled inside an open perf PR
(feat/keccak-hwsl-inline); this extracts the core round-wiring verifier as a
baseline, off main, without any perf change.

The method (reusable)

• Oracle (human-owned, per-chip): an independent spec reference f
  (FIPS-202 here, anchored to hashlib SHA3 + repo constants), a column-role
  map, and a typed chip-contract library (ByteAlu XOR/AND/ADD, AreBytes
  0..256 range, the halfword-shift decomposition, word recomposition, KeccakRc).
• Checker (generic): every trace column a free bitvector; every bus
  interaction / eval constraint an equation under its contract; assert
  output ≠ reference(input) and ask for a counterexample. UNSAT ⇒ correct
  given the contracts; SAT ⇒ under-constrained, with a forging witness.
• Mandatory discipline (documented in the README): falsifiability via
  negative controls (injected bug must flip to SAT, else UNSAT is
  meaningless), a positive control (non-vacuity), the width audit (every
  field-lifted byte/word width must cite a real range-check contract + a
  non-overflow side condition, or a field-level attacker escapes the bitvector
  model), and the rule that fail-open is the only dangerous failure mode.

Which round variant it verifies

The shipped round on main as of #889 (perf(keccak): inline θ/ρ halfword shifts as μ-gated identities, commit 6a280121). On main the θ/ρ shifts are
inline μ-gated linear identities μ·(in·2^rnc − right·2¹⁶ − left)=0 with
range-checked byte-pair halves; the QF-BV model encodes each shift as the unique
(left, right) decomposition those identities force, so the gate is faithful to
the inlined round. Verified: main's keccak_rnd.rs is byte-identical to the
branch the model was authored against — the wiring transcribed is the wiring
shipped. (One documented follow-up: QF-BV cannot test that the range bounds are
sufficient mod p for the inline identities — that companion integer-mod-p
check ships with the perf PR and is the first extension of this template.)

Verified board (regenerated, par.log)

• positive control (non-vacuity): PASS — constraints uniquely pin output
• negative controls, all SAT (caught):
  theta_no_rot, rho_swap, chi_no_not, chi_swap, iota_no_rc
• tamper controls (changed + removed constraints), all SAT (caught):
  iota_wrong_rc, rho_off_by_one, drop_chi_xor_byte, drop_hwsl_carry
  (forged witnesses exhibited for the removed-constraint cases)
• main check: all 24 round indices UNSAT
• reference anchored to hashlib SHA3 + repo KECCAK_RC/KECCAK_RHO; concrete
  mirror matches FIPS-202 over 200 random rounds + 20 full permutations +
  structured inputs

Scope

QF-BV covers bit/byte hashes (Keccak/SHA-3, SHA-2, BLAKE3). Native-field chips
(Poseidon/Poseidon2) are out of scope — their round is field arithmetic and needs
a finite-field solver (cvc5 FF) or a proof assistant (Lean). The check is one
round's transition given the helper-chip contracts; it does not re-verify the
helper chips. The BLAKE3 chip gate and the keccak-sponge verification already
follow this method — this directory is the canonical template.

Running it

cd thoughts/formal-verification/keccak
python3 test_ref.py        # reference constants + SHA3 vs hashlib
python3 test_dataflow.py   # concrete mirror vs reference (+ bug sanity)
python3 z3_parallel.py     # the gate: 24 rounds + controls (see par.log)
python3 tamper_test.py     # changed + removed constraint controls