Hekate v0.38.0 — Hekate ZK Engine

This release closes a soundness gap that every release from 0.29.1 to 0.37.0 carried: a cheating prover could make any bus balance while its sides carried different messages, with and without zero knowledge. Each bus now weights its consistency check and its bus-sum check with their own powers of α, at no cost in proof size. Upgrade is mandatory for any deployment that verifies a program with a bus. The postmortem covers the gap, its exposure and the fix.

For a verifier that runs inside a circuit, Merkle preimages end in their tag, the transcript absorbs on 8-byte lanes and every Merkle opening stops at a layer set by its query count. Config::code_rate adds rate 1/4.

Rebuilt integer atoms cut the NTT table of ML-DSA-44 from 5,928 constraint roots to 2,155. With zero knowledge on an Apple M3 Max, ML-KEM-768 and ML-DSA take 26 to 31% less time to prove than in 0.37.0, and their proofs are 11 to 13% smaller.

The proof wire moves to v8 and the bundle format to 8, and a 0.37.0 proof or bundle does not decode. program_id moves for programs with the IntArith chiplet, an ML-KEM or ML-DSA pipeline or a call to the integer atoms. A circuit that feeds those atoms plain Bit columns now asserts their booleanity itself. Pair with the signed prover cdylib 0.16.0.

§ Two powers of α per bus (#49)

Bus k now weights its consistency term, eq(r_zc, x) · (γ·h + h·key + s), with α^(o+2k) and its bus-sum term and claimed sum with α^(o+2k+1), where o counts the constraint roots, boundary constraints and blinding units ahead of the buses. permutation::bus_alpha_weights yields both weights, and the verifier's ZeroCheck and the zero-knowledge outer statement take every bus weight from it. No challenge is added and proof size does not change. The verifier spends two more field multiplications per bus, three with zero knowledge.

From 0.29.1 to 0.37.0 the two terms shared one power of α. A prover could commit h = (s + e) / (γ + key) for a constant e, and the consistency term then missed by e at every point. Under the shared power that miss paid for a claimed sum off by the same e, and on a bus whose honest sums add up to Δ ≠ 0 the prover could pick the e that cancels Δ. A Lookup bus was in reach too, because its r_bus is drawn before h is committed.

Every bus was exposed in both modes, which in Hekate covers every relation between tables, from memory and lookups to calls into the hash, cipher, ML-KEM and ML-DSA tables. A program without a bus was not.

A proof-of-concept prover commits h with a constant residual on one endpoint of an unbalanced Permutation bus. The verifier accepted its proof under the 0.37.0 weights in both modes and rejects it under the new weights in both.

§ Preimages and transcript on 8-byte lanes (#45)

A verifier that hashes with Keccak-f[1600] inside a circuit can now feed each child digest straight into its parent's preimage and replay the transcript lane by lane. In 0.37.0 the leading tag put every Merkle payload one byte off the 64-bit lane grid, and unpadded labels put transcript values off it too.

Every Merkle preimage now ends in a tag byte naming its kind, and the outer leaf moves from 0x00, which it shared with the part, to 0x03. No preimage changes length or block count under BLAKE3, SHA-256 or SHA3-256. Transcript v2 opens with a hekate-transcript-v2 frame, and every absorb fills a whole number of 8-byte words. A claimed value or public input absorbs 16 bytes against 27 or 28, one squeeze yields four query indices, and the number of public inputs enters the stream.

§ Openings to a level-L layer and rate 1/4 (#47)

A verifier whose hash schedule cannot depend on the query positions now spends 2,233 hashes on a depth-15 pool tree at 287 draws, against 4,305 for full paths. Every opening on the two pool trees and the two outer trees stops at level L = min(⌈log2 q⌉, depth) for q draws. It ships the siblings below the layer and the layer nodes no opened path reaches, and the verifier folds the layer to the root once. Nothing about the layer is read from the proof. By construction the layer adds about 6.7 KiB to a zero-knowledge proof that carries both pool trees.

Config::prod_at(rate) builds a configuration at rate 1/2 with 287 queries or at rate 1/4 with 153, both at 100 bits, and Config::prod() stays at rate 1/2. Both sides absorb the rate that Config::code_rate holds. At rate 1/4 a proof opens 153 columns of a codeword twice as wide, which about halves the opened bytes and doubles the symbols the prover encodes.

§ Integer atoms (#46)

The NTT table of ML-DSA-44 falls from 5,928 roots to 2,155 and from 97 packed words a row to 69, the ML-KEM NTT from 1,712 roots to 776, and the 32-bit IntArith chiplet from 445 to 252.

The atoms write a carry as (a + c)(b + c) + c and the borrow of a - b as (1 + a + w)(b + w) + w, one multiplication each. A chain over n bits emits 2n roots against 4n + 1 in 0.37.0, and its carry slot pinned to zero is gone. mod_add proves one addition and one subtraction from 3n cells and 4n + 1 roots, against 6n + 4 and 13n + 6, and range_check commits n - 1 borrow cells and no result bits. mul_const walks the signed digits of its constant, and 8380417 = 2^23 - 2^13 + 1 takes two stages for the work of ten additions. Codec and Sampler move to the same chains, and their subtractions commit only their borrows.

No atom asserts booleanity. Each sum, carry, borrow and scratch cell equals a polynomial in the atom's inputs, and boolean inputs give boolean cells. A bit expanded from a packed word is boolean by construction, and every table in this workspace feeds the atoms such bits.

§ Preflight and scribble (#50)

Each scribble case now re-checks only the rows its tamper wrote and the row before each, then the table's boundary constraints and the full bus check. HEKATE_SCRIBBLE_ORACLE=both runs the full preflight beside it and panics where the two verdicts differ.

assert_all_caught and assert_all_caught_all_targets preflight the witness before the first case and panic when it fails. In 0.37.0 a tamper that left an existing violation in place counted as caught, and a run on a dirty witness could pass without testing the AIR.

Preflight gains check_air_rows, which evaluates a table's constraints and fixed columns at the listed rows only. Its bus check reads only the selectors and source columns of each bus, in parallel chunks of 4,096 rows, each inverting its keys with one field inversion.

§ Examples and documentation

mldsa_batch proves --count ML-DSA verifications in one proof at --level 44, 65 or 87, each signature under its own key. Public keys and signatures are private inputs, and each signature's M' and tr = H(pk) are public. --count takes at most 128, or 64 at ML-DSA-87.
Every example takes --rate 1/2|1/4, --no-zk and --program-id <64 hex chars> (#47), and just example <name> <ct|public> [flags] forwards them.
The workspace README links the 0.38 postmortem beside the earlier ones and lists mldsa_batch among the examples. Its license note states that a product shipped under other terms, open source or closed, needs a commercial license.

§ Performance

With zero knowledge, ML-KEM-768 and ML-DSA take 26 to 31% less time to prove and 11 to 16% less to verify, their proofs are 11 to 13% smaller, and peak memory falls 12 to 22% on ML-KEM-768 and ML-DSA-44. Without zero knowledge their proving takes 22 to 31% less time and their proofs are 4 to 12% smaller.

On the other ten workloads, zero-knowledge verification time falls 15% on SHA-256 2^21, and the two smallest zero-knowledge proofs, Keccak 2^15 and SHA-256 2^11, grow by 9 KiB. Prove time and peak memory hold on all of them but RSA-2048. Its base prove time rises from 171 ms to 183 ms, with this release's three runs between 183 and 212 ms, and its zero-knowledge peak memory spread over 397 to 486 MiB in the 0.37.0 runs and 458 to 506 MiB in these.

Each release with the signed prover its tag pins, public variant for aarch64-apple-darwin: 0.37.0 with prover 0.15.0 (4e72a3c1…), 0.38.0 with prover 0.16.0 (654d3883…). Apple M3 Max, --release with fat LTO and one codegen unit, features std parallel blake3 table-math public, Config::prod(), best of three in each mode. The table shows zero-knowledge mode.

Workload	Proof, KiB	Verify, ms	Proving	Peak, MiB
Keccak 2^15	851 → 860	4.6 → 4.4	163 → 168 ms	143 → 145
Keccak 2^20	3,544 → 3,545	7.1 → 6.8	3.23 → 3.20 s	2,430 → 2,430
SHA-256 2^11	516 → 525	3.2 → 3.1	53 → 52 ms	62 → 65
SHA-256 2^21	5,485 → 5,486	11.3 → 9.6	8.72 → 8.82 s	5,099 → 5,104
ML-DSA-44	1,547 → 1,341	10.5 → 8.8	432 → 318 ms	219 → 193
ML-DSA-65	1,568 → 1,367	10.3 → 8.9	472 → 338 ms	207 → 202
ML-DSA-87	1,812 → 1,604	11.2 → 9.9	618 → 440 ms	308 → 288
RSA-2048	1,810 → 1,814	8.2 → 7.7	204 → 205 ms	397 → 458
ML-KEM-768 sender	1,544 → 1,347	11.6 → 10.3	408 → 283 ms	204 → 159
ML-KEM-768 receiver	1,884 → 1,665	13.9 → 12.2	552 → 411 ms	292 → 248
AES-128	2,970 → 2,970	6.4 → 6.2	920 → 910 ms	770 → 768
AES-256	3,198 → 3,201	6.5 → 6.2	975 ms → 1.01 s	961 → 974
Integer arithmetic 2^20	1,143 → 1,142	3.7 → 3.6	259 → 261 ms	252 → 252
Integer arithmetic 2^24	4,098 → 4,097	8.1 → 7.6	4.06 → 4.08 s	3,321 → 3,328
Integer arithmetic 2^26	8,021 → 8,019	12.4 → 12.1	19.27 → 18.63 s	13,003 → 13,066

§ Breaking

Each PR's Compatibility section lists the rest.

§ Not promised

Upgrading does not reach a proof that a verifier from 0.29.1 to 0.37.0 has already accepted, and such a proof is no evidence of what its buses carried.
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.
min_security_bits = 0 skips the support check that zero knowledge relies on, even with zero_knowledge: true.
MerkleTree::verify binds neither the path length nor the leaf index. Open through verify_batch with the padded leaf count, as the protocol does.
Whether a host program computes what its name says stays with its author.
This workspace has not had an independent audit.