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; the AST of the three Python files
  is 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.

• Adds combinatorics.py, which checks the premises the ρ result rests 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, and the
  pi offsets are even so a pi halfword reads a single source halfword.

• 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, two of twenty-five output lanes differing from
  FIPS-202.

• Replaces the README's "both are load-bearing" with the table above, and states that
  the 24/24 UNSAT verdict is conditional on the range checks existing.

• 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

• combinatorics.py, necessity_theta.py, necessity_rho.py and
  witness_fullchip.py pass. The sound results need no solver: they are exact
  integer-bounding arguments over finite, complete enumerations, so they run in
  seconds.
• The existing board is unchanged: test_ref.py, test_dataflow.py,
  z3_parallel.py (24/24 UNSAT, 5/5 negative controls SAT, positive control PASS),
  tamper_test.py (clean UNSAT, 4/4 tampers SAT).
• 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.