Correct the keccak gate and prove bound necessity

[jotabulacios]

Motivation

The gate's line citations are its only audit trail into the Rust. The README states
that faithfulness of the model to the Rust is a human obligation, and the citations
are how someone discharges it. All of them are wrong. rs:539-588 ("theta: Cxz XOR
chain") lands on the KeccakRc sender, rs:796-870 ("chi: AND then XOR") lands on
Iota, and rs:593-631/rs:723-766 name BusInteraction::sender(BusId::Hwsl, …)
blocks that #889 deleted outright; the file now contains zero. test_ref.py cites
execution.rs:646-680 for KECCAK_RC/KECCAK_RHO, which sit at 782 and 810. They
were moved by #876, an unrelated hint-ecall PR that grew the file by 136 lines, so
the cited range is now ArithOp::Div and the citation was stale three days before
this branch opened.

The README also declares a scope gap as its first follow-up: QF-BV cannot test
whether the AreBytes/IS_BIT bounds are sufficient mod p. It cannot be closed
in the same model. The bounds are carried as the width of the bitvectors, and mod
2^n the factor 2^16 is a zero divisor, so even a widened model would report the
decomposition pinned. Mod the Goldilocks prime 2^16 is invertible.

Separately, the AIR's count tests (1031 interactions, 1480 columns, 140 constraints)
catch anything that adds or removes one of those, but not a rewiring that keeps them.
Changing the first BusValue of the ρ ARE_BYTES pair from cols::rot_left to
cols::rot_right leaves all three counts untouched, is satisfied by every honest
trace, and makes ρ forgeable.

Description

• Cites each modeled equation by the construct it names — the
  // --- <Group>: … --- banner title, or the cols:: / KeccakRndConstraints
  symbol — instead of a line number. Names survive the churn that broke these from
  two unrelated directions. No executable change in those three files: their ASTs are
  identical modulo docstrings, and the board is unchanged.

• Drops the README section that catalogued where the stale numbers really pointed,
  since with the citations fixed it no longer describes anything.

• Adds field_model.py, the companion integer-mod-p model of the inline θ/ρ
  identities, with a switch per range check. in · 2^rnc = right · 2^16 + left pins
  nothing on its own over a field, since for any left there is exactly one right.
  What the range checks do is rule out the deviation (L, R) → (L − 2^16·d, R + d),
  and they do not do it equally:

  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

  left and right enter with weights 1 and 2^16. Bounding left kills the
  deviation outright; bounding right only narrows it. In θ the residual window is
  closed by the parity of left, the shift being by one, and by the carry being a
  single bit. In ρ, right is a halfword and d = ±1 fits exactly at saturation,
  which theta = 0xFFFFFFFFFFFFFFFF reaches on all 25 lanes.

• How a cell is decided. Dropping a check does not free its column: the ByteAlu
  operand that reads it still confines it, because the BITWISE table holds byte rows
  only, so checked_byte + this ∈ [0,255] forces this ∈ [−255,255]. Only with that
  window is the deviation an integer at all — over the field an unbounded right
  admits a full-size solution for every left, and no argument about small d would
  mean anything. operand_summand_window derives the window,
  difference_form_is_exact checks the magnitude step (every term under 2^33 ≪ p,
  so the field identity is the integer identity and Euclidean division is unique),
  and surviving_deviation then sweeps all 2^16 input halfwords against one
  interval per column, returning either "pinned" or the first survivor. It also
  asserts the honest pair lies inside the modelled intervals, the failure that would
  make a "pinned" verdict meaningless. The "both dropped" row is the one
  configuration with no per-column window — the operand bounds only the sum of two
  unchecked columns — so it is decided by an explicit witness instead.

• Adds combinatorics.py, the premises the sweeps rest on, none of which had been
  checked: π is a bijection on the lanes, all 400 rot_left/rot_right byte columns
  are read exactly once by a pi operand, the pi offsets are even, and the four θ
  carries are a permutation of the four rotated_C low bytes. Read-once is the
  load-bearing one — a column read twice would need the intersection of two windows.
  It is exposed as premises() and imported by both necessity scripts, so it is not
  a file you are asked to remember to run.

• Adds witness_fullchip.py, which builds the ρ forgery as a whole KECCAK_RND row
  from a reachable message state instead of a lane in isolation: all 140 constraints
  and every ByteAlu operand satisfied, output lanes differing from FIPS-202. Honest
  and forged rows come from one builder and the honest row is required to be exactly
  the reference, because "the output differs" is also what a bug in the script itself
  produces. Every saturated lane is forged in turn — 11 of them, 10 with a non-zero
  rotation — and the wrong output lanes must be a subset of the lanes that can move.

• Replaces the README's "both are load-bearing" with the table above, states that the
  24/24 UNSAT verdict is conditional on the range checks existing, and records what
  the two implied halves are worth, since they are not the same kind of saving: ρ's is
  100 AreBytes sends, θ's is 20 degree-3 polynomial constraints — the reason
  KeccakRndConstraints declares max_degree() = 3. Neither is proposed here as an
  optimization; the result bounds the ceiling.

• Adds make verify-keccak and a workflow that runs it on every PR touching
  formal_verification/, on any base branch. Nothing in the repo ran anything under
  that directory before: the solver-free half takes about three seconds, and leaving
  it manual meant the only automated guard was a digest test whose documented remedy
  is satisfied by pasting a constant. The QF-BV gate stays manual — z3 bindings, about
  three minutes — as the README documents. It runs on this PR as
  Keccak round gate (solver-free), green in 6 s. The trigger filters by path without
  restricting the base branch, which is why it runs on a stacked PR at all —
  Spec structure test, which restricts to main, does not run here.

• Adds test_keccak_rnd_air_structure_is_pinned, which digests the bus wiring (ids,
  multiplicities, column indices, linear coefficients) and the captured constraint IR
  (ops, dimensions, field constants, roots). FNV-1a is written out because std's
  hasher is not stable across toolchains. When it fails the wiring changed, and the
  directory has to be re-run before the digests are updated.

#889 replaced the HWSL lookups with these identities and dropped 120 sends per row.
Under the lookup, left and right were pinned individually and dropping either
check was harmless; under the 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 it.

Tests

• make verify-keccak is green: test_ref.py, test_dataflow.py,
  combinatorics.py, necessity_theta.py, necessity_rho.py and
  witness_fullchip.py, about three seconds. The sound results need no solver — they
  are exact integer-bounding arguments over complete enumerations of all 2^16 input
  halfwords.
• The existing board's verdicts are unchanged: z3_parallel.py (24/24 UNSAT, 5/5
  negative controls SAT, positive control PASS) and tamper_test.py (clean UNSAT,
  4/4 tampers SAT). test_ref.py, model_dataflow.py and z3_verify.py are touched
  only in their citations, and their ASTs are identical modulo docstrings.
• Each new check was confirmed to fail when it should. Widening the left interval
  to a halfword and a bit, or dropping rot_left's check, produce survivors in the
  sweep. Making Dxz read column (x+1) instead of (x+4), or dropping χ's NOT,
  fail the full-chip positive control — both of those used to pass. Ignoring the
  target in configuration D fails its target check, which is how the off-by-one in
  that recurrence was found: it indexed c[(j+1)%4] while the closed form for r0
  above it solves for c[j], so it hit the intended pi halfwords on 0 of 25 lanes.
• test_keccak_rnd_air_structure_is_pinned was checked against the tamper it exists
  for. With cols::rot_left → cols::rot_right applied to the ρ ARE_BYTES pair,
  test_keccak_bus_interaction_counts, test_keccak_column_counts,
  test_keccak_constraint_counts, test_pi_virtual_matches_rotate and
  test_keccak_core_round_state_consistency all pass, and only the digest fails.
• cargo fmt --check and cargo clippy --all-targets -D warnings clean.