fix(formal-verification): use unsigned ULE for the keccak gate's byte-range contract

[nicole-graus]

Motivation

The QF-BV byte-range assumption in byte_op_operand was written as field_expr16 <= BitVecVal(255, 16). In z3py, comparison operators on bitvectors are signed (SLE), so that also admits every value with the sign bit set:

BitVec('x',16), x <= 255, x == 0xFFFF -> sat (accepted)
BitVec('x',16), ULE(x,255), x == 0xFFFF -> unsat (rejected)

It is harmless today — both call sites pass sums of two zero-extended bytes (≤ 510), so the sign bit is unreachable — which is exactly why nothing in the directory would ever surface it. The README opens by telling the next chip to copy this contract library, and its own contract table lists 32-bit word recomposition as a next target; at that width expr <= 255 admits all of [2³¹, 2³²), silently accepting an out-of-range operand as a byte and turning a real SAT into a bogus UNSAT. That is the fail-open direction the README's Mandatory-discipline section exists to close.

Description

• z3_verify.py: byte_op_operand now uses ULE, with a comment explaining why unsigned is load-bearing. This was the only bitvector comparison in the directory.
• Dead code removed: the wrong-order in_lanes list overwritten two lines later, zref_round's accepted-and-ignored bug= parameter, keccak_ref.py's overwritten R assignment, and z3_parallel.py's unused tasks/pos locals and sat/unsat imports. python3 -m pyflakes *.py is now clean.

[MauroToscano]

Depends on #923 — that should merge first. This targets docs-keccak-formal-verification-baseline, so it can only land as part of that stack; noting it here so the ordering is explicit rather than implied by the base ref.

[MauroToscano]

Approving. The fix is correct and provably behaviour-preserving.

Verified rather than assumed:

• z3py's <= on bitvectors really is signed (bvsle), so the premise holds.
• The change is a logical no-op at the widths in use — both call sites feed sums of at most two ZeroExt(8, ·) values at width 16, so bit 15 is unreachable, and the SLE/ULE difference is machine-checked unsat. The pre-fix proof was neither vacuous nor wrong.
• Full board re-run at head: 24/24 rounds UNSAT, positive control PASS, 5/5 negative controls SAT, VERDICT: VERIFIED (7m29s). tamper_test.py 4/4.
• The "only bitvector comparison in the directory" claim checks out: AST scan plus a dynamic trace patching the BitVec comparison/shift/div operators and SignExt shows 0 signed-operator executions at head vs 6357 at base, all at the one fixed site. SignExt is never imported; all extension sites use ZeroExt.
• pyflakes: base 4 findings, head 0. Claim holds.
• The _rc_bit comment rewrite is accurate against FIPS-202 Algorithm 5 (checked by transcribing Alg. 5 independently and comparing the whole register, not just the returned bit) — and it replaced a comment that was genuinely wrong: the old "r0 = MSB per our shifting below" contradicted the R <<= 1 beneath it.

One thing I fixed directly (b973791c): the explanatory comment stated the direction of harm backwards — it called weakening the bound "the fail-open direction … turns a real SAT into a bogus UNSAT". The byte bound is a plain conjunct of the query and the goal is a separate positive conjunct, so weakening it can only turn UNSAT into a bogus SAT — a spurious counterexample against an honest chip, which the README classifies as the nuisance direction, not fail-open. Confirmed empirically: patching the gate back to signed <= left all five injected bugs SAT, none flipped. It mattered because that file is advertised as the template other chip gates copy.

Minor, for the record, no action needed: the description calls the removed in_lanes comprehension "wrong-order". It wasn't — [... for y in range(5) for x in range(5)] indexes as x + 5*y, the same order as the replacement. The removal is right; the value was simply redundant and dead.