Hekate v0.33.0

Seven chiplet soundness gaps, three in Keccak and four in AES, each sufficient on its own to forge the statement the chiplet exists to prove. Both chiplets computed their round functions correctly; neither proved its cipher. Round constants sat in witness columns the prover chose, nothing said where a block may open or that it must close, bus keys never said which end of a block an emit was, and the S-box bus had no clock. Sixteen forgery tests pin these shut; six of them, run against the shipped 0.32.0 prover and verifier, were accepted. Separately, the Brakedown commitment stops encoding a second next-row codeword; shifted claims ride weights the verifier evaluates itself. Half the codeword, 20 to 29% off proof size, wire format v4; with hekate-math 0.10.0 and a new prover build in the same window, prove time lands 31 to 49% below 0.32.0. The chiplet fixes change committed layouts, and with them program_id for every program embedding Keccak, AES, or the S-box ROM. Pair with the signed prover cdylib 0.11.0. Upgrade is mandatory and every proof must be re-proved.

Full analysis of the seven gaps, the tests that missed them, and the cost accounting: postmortem.

§ Soundness

Everything here was committed and opened. What was missing was a constraint saying what a committed column may hold, and bus keys rich enough to tell two emissions apart. The Keccak gaps reach every SHA-3 and SHAKE statement proved against the chiplet, ML-KEM-768 and ML-DSA-65 included; the AES gaps reach every AES-128 and AES-256 statement, counter mode worst of all.

• The Keccak round schedule is forced by the AIR. RC_BITS was 64 committed bit columns that no constraint root touched: 24 free round constants, 1536 bits of freedom over the block's final state, and the last round's constant set lane (0,0) outright. The column is gone. A one-hot round index, expanded from one committed B32, drives Iota as a coefficient sum, and no round constant appears as a witness.
• A Keccak chain opens on an input emit. The AIR said what follows a round row, never where a run may start: a two-row block from an invented state could aim a chosen digest at a CPU row expecting one. Three roots close it. A non-round row carries no round bit, its successor none above round(0), and a row carrying round(0) is an input emit.
• The Keccak bus key says which end of a block an emit is. Both emit rows fired on the same selector; swapping a block's two request indices handed the consumer keccak-f inverted, at the cost of one keccak-f. In a sponge each call flips independently, putting 2^calls digests within reach of one message. IS_OUTPUT joins the key on both endpoints, pinned on emit and non-emit rows alike.
• Every AES emit has a full block behind it. A row carrying the emit selector alone satisfied every equation in the chiplet, its STATE_IN free and on the bus: a CTR host's keystream was the prover's to choose. The doubling counter was no backstop: it pinned a value rather than a count, and a run could stop early (a two-row block computes one round, trivially invertible), never start (a lone final row with a free ROUND_KEY), or wrap (0x02 has order 51 in GF(2^8), and a 60-round AES-128 block fit the shipped 2^19 trace thousands of times over). Both levels replace the counter with a one-hot round index. Every selector is a function of the index, and every maximal run opens on an input emit, runs the full schedule, closes on the final round, and is followed by exactly one output emit. Rcon leaves the witness the way iota did.
• The AES link key says which end an emit is. The same substitution one chiplet over: the consumer reads its ciphertext where it expects its whitened plaintext, at the cost of one AES decryption. S_INPUT, a function of the round index now, joins the key on both levels.
• The S-box bus has a clock. The key was 16 state bytes plus 16 S-box bytes. Encrypting the same block twice gave every S-box emission multiplicity two, and in characteristic two an even multiplicity is a deletion: the pair cancels before cross-bus matching and SBOX_OUT goes back to being free. The AES side appends its row index to the key, the ROM commits the matching request-index column, and no clock waiver remains in the crate.

§ The host half of the fix

A direction source binds the chiplet's two emits to each other. It does not say which row of the consumer's trace is the request, and leaving that to convention reopens both direction gaps by a second route. Hosts migrate too:

• AES: CpuAes256Unit::linking_spec_at gains a direction column and will not build without it. Each level pins that column with its own unit, CpuAes128Unit::constrain or CpuAes256Unit::constrain_at, on the same selector and direction columns; the five roots supersede any standalone selector pins. They require each call's two emit rows to be adjacent; a host that splits them pins the direction column from its own semantics instead.
• Keccak: IS_OUTPUT becomes a running value between emits, and CpuKeccakUnit::direction_boundary joins the boundary constraints. A host whose emit pairs sit on adjacent rows already writes the correct column and needs the anchor alone. The pinning recurrence is cyclic and its complement is the reversal; the anchor is not optional.

Nothing at the API level forces the pairing, and a host that skips it compiles, proves, and stays forgeable. hekate_scribble::language::assert_direction_pinned closes that from the test side, rejecting any host AIR that admits more than idle, request, response, idle. Run it against every host mounting either chiplet.

§ Control-language enumeration

The old suite was green because every exploit test tampered one cell of an honest trace, breaking a relation the AIR already enforced. The witness an attacker builds is consistent under its substitution, and the suite now lays exactly those: sixteen forgeries through the real prove and verify pipeline, none ignored. The AES forgeries additionally pin whether rejection must come from a constraint root or from the bus. The tamper helpers wrote raw flat values, skipping the basis map and landing a named delta on an unrelated value; they are fixed, and a test that says it corrupts byte 0 now corrupts byte 0.

hekate-scribble gains a language module: hold the data plane at zero, enumerate the control plane, and compare the admitted transition relation against the honest automaton. Roots mixing control and data are skipped, making the result a superset of the AIR's real language; a core equal to the automaton bounds it from above. AES-128 enumerates all 2^16 index values, AES-256 the same shape, Keccak bounded to Hamming weight 3 and stated as a bound. A missing bus-key source is invisible to it; three of the seven gaps sat exactly there, found by reading the key construction.

§ Base-only commitment

The commitment encoded every physical column twice, base and shifted by one row, because the evaluation argument had to open the next-row polynomial at the same point. The second copy is gone. Shifted claims now ride two transparent weights the verifier evaluates for itself in O(n): a carry-chain form of eq(prev(·), P) paired with the whole-column master, and its ring-switch counterpart paired with the bit-plane master. Same hash, same code, same Merkle structure, half the codeword.

Binding does not move. The deleted copy was a second opening of data the first copy already committed, never an independent constraint, and the weights are evaluated from r_final and the verifier's own sumcheck challenges, leaving the prover nothing to choose. The wrap term must agree bit-exact with what the ZeroCheck consumes as the next row; a regression test pins that agreement directly.

Geometry moves with it: the split is priced at the widths the opened leaf actually carries rather than raw byte size, and the per-table master-vector count is absorbed into the transcript, keeping that model on bound inputs. One guard rides along: an expansion set that does not tile the physical layout is rejected at ChipletDef::from_air; such a column was previously committed and bound by nothing.

§ Performance

Signed public cdylib 0.11.0, table-math, Apple M3 Max, -C target-cpu=native, mean of three runs, quiesced host. Peak memory is the larger of phys_footprint_peak and ru_maxrss. The 0.32.0 column is that release's published measurement.

Verification stays flat at 6 to 32 ms: two opened halves are traded for two weight evaluations. The soundness fixes on their own move prove time within 6% and proof size within 1%. The rest is the commitment layout, 20 to 29% off proof size and 13 to 31% off peak memory measured in isolation: a byte the codeword no longer carries is a byte not encoded, not hashed into the tree, and not opened at a query.

The prove column is not the layout alone. It stacks three changes landing together: the layout, hekate-math 0.10.0 (NEON flat-multiply kernels moved to the vector domain, Block128 dependent-chain latency 7.27 to 4.64 ns/mul), and prover-internal work that ships with the cdylib either way; the three are not separated by measurement. The six PQC and AES workloads all prove faster than in 0.29.1, before any of the protocol fixes existed. keccak_inline 2^24 was not re-measured.

§ Breaking

• Wire format. WIRE_PROOF_VERSION 3 -> 4; a v3 proof fails at deserialization. Re-prove. EvalBatchProof collapses to a single point_evaluation.
• program_id. Committed layouts change on the Keccak chiplet, both AES levels, and the S-box ROM. Every program embedding any of them gets a new program_id. Config is unchanged.
• Transcript. rho is no longer drawn; each table's master-vector count is absorbed with its header before the first challenge.
• Verifier API. EvalVerifyContext carries point, claimed_values and shifted_claims; BrakedownVerifier::verify takes split_vars; compute_split_vars gains num_vectors; absorb_chiplet_header gains num_master_vectors.
• Hosts. CpuAes256Unit::linking_spec_at takes a direction column and pairs with constrain_at. Keccak hosts write IS_OUTPUT as a running value and add direction_boundary; that half compiles unchanged and must be migrated by hand.
• ChipletDef::from_air rejects expansion entries that do not tile column_layout(). Such a column was previously committed and bound by nothing.
• Prover cdylib 0.11.0, signed (SHA-256, Ed25519, ML-DSA-65). 0.10.0 neither produces nor reads v4 proofs.
• macOS linking. The staged prover dylib carries an absolute install name; tests and examples linking it need no manual rpath. A redistributed binary still does.
• Version. Workspace 0.32.0 -> 0.33.0; hekate-keccak and hekate-aes 0.6.0, hekate-pqc 0.7.0; hekate-math 0.10.0.