Hekate v0.36.0

This release closes five soundness gaps, three with forgeries that 0.35.0 accepted, and rebuilds the post-quantum crate. Through 0.35.0 any two Keccak or AES calls in one proof could swap their answers, an AES block could encrypt under another call's key, and ML-DSA's published c̃ reached no check; the ML-KEM and ML-DSA circuits proved almost nothing about the values they claimed to compute. Every service bus now pairs request t with response t through a clock the verifier computes, and every ML-KEM and ML-DSA value moves on a bus from the row that produces it to the row that consumes it. Every chiplet trace and its witness buffers also wipe on drop. Programs that embed Keccak, AES, IntArith, SHA-256, modexp, RAM or a post-quantum chiplet get a new program_id and must be re-proved. Pair with the signed prover cdylib 0.14.0. Upgrade is mandatory for any deployment verifying Keccak, AES, ML-KEM or ML-DSA statements.

Full analysis of the gaps, the forgeries and the fixes: postmortem.

§ Ordered service buses (#34, #36)

• The verifier computes every call's clock. Source::EmitRank labels the t-th emit of an endpoint ω^(base + t), counting the rows where its pinned selector is 1. ω has prime order 67,280,421,310,721, about 2^45.9. Request t meets only response t, and neither side commits a clock column.
• Checked at verify entry. HekateVerifier::verify checks every ordered bus before any transcript work: one rank source per endpoint at one key position, a pinned 0/1 selector, and a chiplet endpoint whose emit count follows its own height placed last on its side. The check is total and fails closed.
• Every service moved. Keccak, the AES link, key and S-box buses, IntArith, SHA-256, modexp and the post-quantum services clock by rank. The responder clock columns and the Keccak direction column are gone, and Service accepts rank clocks only. RAM answers in address order and keeps its committed clock under an audited waiver.
• Forgeries rejected. The swaps and rotations 0.35.0 accepted fail verification in every block order, at both AES key sizes, with zero knowledge off and on.

§ Post-quantum rebuild (#38)

• Each table is a function. FIPS 203 KeyGen_internal, Encaps_internal and Decaps_internal and FIPS 204 Verify_internal run as pipelines of tables at every parameter set. Each table proves outputs = f(inputs) for every call on its service bus, and values travel on buses keyed by labels or by emit rank. The memory table is gone.
• Host contract. The host trades 32-bit words with the pipeline over an ordered data bus and decides what is public. Decapsulation returns K and a validity bit, and ML-DSA compares c̃′ with c̃ over the full length of c̃.
• Checked against independent implementations. ML-KEM outputs match the ml-kem crate 0.3.2 at all three levels, and ml-dsa 0.1.1 signatures prove and verify at all three. Seventy forgery cases each prove a false witness that the verifier rejects.
• Engine additions. Secret traces that zeroize on drop, Config::min_table_rows(), Circuit::attach_namespaced, per-decode label interning in the bundle decoder and a bundle serializer that wipes its buffer.

§ Composition (#33, #40)

• Kernel hints survive composition. ChipletDef keeps the inline chiplets and kernel hints of the Air it snapshots, and the bundle carries them. Circuit reads committed columns through views without a second commitment.
• CompositeChiplet removed. The AES chiplets drop their field parameter and attach through Circuit::attach_namespaced with EXTERNAL_BUS_IDS.

§ Witness hygiene (#39)

• Every chiplet witness builder and the RSA PKCS#1 host build traces whose columns zeroize on drop. The buffers behind them wipe as well: AES calls and rows, the Keccak sponge and its call record, SHA-256 padding and scratch, the modexp witness.
• The AES S-box check and zero flags stop branching per witness byte, and the bignum subtraction and digit comparison move to subtle.
• Proving and verification run unchanged code. Each wiping buffer costs one pass when it drops.

§ Performance

Signed public cdylib 0.14.0, pre-release build, Apple M3 Max, --release, features std parallel blake3 table-math, Config::prod(), best of three, zero-knowledge arm. The base column and the reproduce commands are in the workspace README.

The rank clock moves proof size between −1.9 and +0.4 percent on the workloads it touches, and RSA-2048 proves 5 to 6 percent slower and awaits profiling. ML-DSA proves 35 to 42 percent faster than in 0.35.0, with proofs 29 to 39 percent smaller and peak memory 41 to 55 percent lower, on a circuit that now proves verification. ML-KEM has no like-for-like row: the sender and receiver examples replace the decapsulation example.

§ Breaking

• Bundles. Format 5 to 7, and a 0.35.0 bundle is rejected. Proof wire v6 and the transcript are unchanged.
• program_id. Every program that embeds Keccak, AES, IntArith, SHA-256, modexp, RAM or a post-quantum chiplet gets a new id. Re-prove against this release.
• Services. Service::respond takes (values, selector); the request-index slots, request_phased and clock_columns are removed. A responder's k-th emit answers the host's k-th request, and Keccak hosts drop their direction column.
• Post-quantum API. MlKemChiplet::new(params, &[MlKemCall]) and MlDsaChiplet::new(params, &[msg_len]). basemul, norm_check, twiddle_rom and both old composites are removed, and every pipeline table is at least 512 rows. The mlkem example becomes mlkem_sender and mlkem_receiver.
• Composition. CompositeChiplet and the compose helpers are removed, and Aes128Chiplet<F> becomes Aes128Chiplet, likewise for 256. The composite_chiplets example is removed, and keccak_inline folds into keccak.
• Wiping types. serialize_bundle returns Zeroizing<Vec<u8>>, hekate_sha2::pad_message returns Zeroizing blocks iterated with .iter(), and Sha256Call drops Debug, PartialEq and Eq.
• Prover cdylib 0.14.0, signed (SHA-256, Ed25519, ML-DSA-65). An older cdylib cannot read bundle format 7.
• Versions. Workspace 0.35.0 to 0.36.0; hekate-keccak and hekate-aes 0.9.0, hekate-pqc 0.10.0, hekate-sha2 and hekate-rsa 0.2.0.

§ Not promised

• Host emit order. A responder answers requests in order. Emitting each call's request before its response, without interleaving calls, is the host's job; rows in another order pair in that order.
• Circuit semantics. Whether a host program computes what its name says stays with its author.
• Narrow column types. A Bit, B8 or B16 column that is neither pinned nor bit-expanded is bound by the commitment to GF(2^32) only, and its AIR has to hold it to its declared width. Every such column in hekate-pqc is held by a constraint.
• Reference coverage. ML-KEM is checked against one independent implementation on fixed seeds, and the NIST test vector files are not run. ML-DSA's tr and μ are checked only against our own SHAKE.
• Independent audit. This workspace has not had one.