Hekate v0.34.0

Two protocol rewrites, each closing a class rather than an instance. Every proof published the raw column evaluations of every committed column of every table, the ZeroCheck round polynomials above their linear coefficient, the LogUp claimed_sums and h_evals, the eval-sumcheck rounds and two bare tensor folds. Those are linear functionals of the witness at a point any observer recomputes from the transcript: an academic leak on a wide dense trace, exact recovery on a witness of a few secrets pinned to known rows, passive, from one proof, by every party that ever sees it. Separately, every bus selector in the workspace was a witness Bit. One write cleared a row from the bus and switched off every root gated on it, and the row stayed committed, opened and free; the verifier meanwhile evaluated whichever Program the caller handed it and walked the author's own declarations before doing algebra, accepting every shape it did not recognise.

0.34.0 one-time-pads every exposed scalar and re-proves the verifier's whole accept predicate in an outer zk-Ligero argument over GF(2^128), pins liveness to fixed columns on every shipped table and deletes the structural validators from the verify path, and makes verify take the audited program_id as its first argument. Proof wire v4 to v5, bundle v2 to v4, every program_id in the workspace changes. First AGPL-3.0-only release. Pair with the signed prover cdylib 0.12.0. Upgrade is mandatory and every proof must be re-proved.

Full analysis of the three gaps, what each one admitted, and the cost accounting: postmortem.

§ Zero knowledge (#26)

Masking the claims alone cannot work. The verifier's consistency check evaluates F(c) = Σ_k α^k · Constraint_k(c) at the AIR's degree from plaintext, and any scheme that lets it evaluate F on the true c reveals c; an additive mask published on the wire is public-coin arithmetic, subtracted by the verifier and by every observer alike. The nonlinearity is discharged into an argument instead.

• The recovery is arithmetic, not a side channel. For a witness constant over a known block of rows and zero elsewhere, W̃_j(r_final) = Σ_slot secret_slot · c_slot with every c_slot public, r_final re-derived from the transcript, and the row map fixed program structure. A secret at two known rows divides out of one equation; four candidate slots give two equations per column, and the active-slot mask is usually a public input. Values, keys and per-record randomness are all in that regime.
• Every exposed scalar is one-time padded. Pad::derive expands a 32-byte seed in counter mode, and the seed is bound to the statement rather than taken from the caller verbatim, hence a reused blinding seed still yields an independent pad. The pad is committed as a Ligero row oracle, and pad_root is absorbed after the main header and every chiplet header, before any challenge that depends on it. Pad indices are derived from the statement on both sides and never read from the wire. The statement size is a pure function of program and config, and a cursor that does not land exactly on masked_scalars is rejected.
• The verifier's predicate is re-proved in outer zk-Ligero. Over an additive-FFT coset of GF(2^128), with geometry derived on both sides from the statement size alone and never read from the proof, because a prover-chosen geometry is a free parameter that voids the query bound. Three tests over the two stacked oracles: interleaved, linear, quadratic.
• The mask rows reach the whole response space. A plain mask row cannot cover the high half of a product-code response. Each masked test uses u_a + Z · u_b with Z the novel-basis message vanisher at index k; the pair spans all of degree < 2k while every committed row stays inside RS[n, k]. Responses ship as novel-basis coefficients, which makes the degree bound structural rather than scanned and removes 3 · n · 16 bytes from the wire.
• Every moved check has a row. Fixed-column MLE compare, the AIR root sum, boundary, the blinding telescope, LogUp consistency and bus sum, h · key as a real product, both eval finals, the Mul operand triples, the ring-unit claims, and Σ claimed_sum = 0 per bus_id. Dropping a row silently un-enforces that check under ZK.
• Ring-unit claims needed their own gadget. The target there is F_2-linear rather than F-linear, and no affine row over GF(2^128) expresses it. A linearized polynomial evaluated by a Frobenius-Horner chain over the dual basis does, over pad unknowns only, with no claim and no public value entering the chain. Construction, completeness, uniqueness and cost are in docs/zk-ring-switching.pdf, which closes the open problem Diamond left in ring-switching.

§ Zero-trust verify path (#27)

One rule applied throughout: a verify-path check is safe iff its answer is a total function of data the verifier recomputes or compares by equality, with no case analysis over author-chosen structure.

• Liveness is a fixed column. 48 of 57 shipped endpoints selected on prover-written Bits. Every endpoint is now None or a member of its table's fixed_columns(), enforced by validate_fixed_selectors: exhaustive over the enum, no accepting arm, at ChipletDef::from_air, ChipletDef::from_wire, Circuit::compile, and verify entry for main and every chiplet. FirstRow, LastRow and Custom substitute a virtual poly the LogUp reader cannot consume and are refused as selector shapes. Two shapes carry the schedules: FixedShape::Cadence { stride, count, origin, values }, a strided block with a per-period pattern at any origin, and FixedShape::Segments, a disjoint union of them sorted by origin, with overlap or disorder rejected rather than normalised.
• The verifier pins its circuit. program_id is the first argument of verify, recomputed from the verifier's own Program, compared, and absorbed as the first transcript message. It never travels in the proof or the bundle: a proof-carried id is a label the adversary picks, and the bundle already carries the program the id derives from. The threat is drift in the operator's build, where a prover and verifier rebuilt from one drifted tree still agree with each other, and the pinned constant is the one value living outside the code that drifts.
• The structural validators are gone from verify. validate_clock_stitching, validate_bus_set, validate_paired_bus_mutex and unconstrained_bit_selectors each read author-chosen structure and each had an accepting default arm. The verify path now runs validate_fixed_selectors, validate_fixed_columns, sumcheck, Brakedown openings, LogUp consistency and cross-bus sum, the fixed-column MLE compare, and the boundary compare. Nothing reads the AST or the specs for shape. Clock waivers remain authoring-time documentation with a citation lint.
• Roots came out, not columns. A pinned selector is the same committed Bit column and the trace layout is unchanged. Deleted: selector booleanity everywhere, roughly 30 chain-shape roots each on Keccak and AES, 37 on the ML-DSA control table. ML-DSA also sheds the never-written kec_input_bind bus, whose endpoints were both inert, and thirteen dead columns at 33 physical cells per row.

§ Authoring

A host that takes the new crates without pinning its own bus selectors is rejected at circuit construction and again at verify entry.

• Circuit. column, schema, columns, expand_bits, reuse_pass_through, fix, boundary, call, bus, mount, mount_unlinked, attach, publish, compile. Column indices, chiplet offsets and inline kernel root offsets are derived, never hand-computed. publish(col, row) is the only public-input slot mint and records the BoundaryConstraint::with_public_input pin.
• Service and ServiceSlot. The serving chiplet declares its bus key schema once; request() and respond() derive both endpoint specs from it. Slots: Value, Const, RequestIdx, RequestIdxBytes.
• Constructors take the count that sizes the schedule. Keccak, both AES levels and the S-box ROM, RAM, ROM, integer arithmetic, NTT, twiddle ROM, base multiplication, norm check, high bits, and both post-quantum control tables. MlDsaChiplet::new takes msg_len, and that length lands in program_id: one id per accepted length. Trace generation errors upfront on schedule overflow instead of truncating silently.
• Preflight. BusDiagnostic::clock_collisions reports emit rows whose row-index clock bits fold to one value, masked to num_vars; BusDiagnostic::inert reports a bus no endpoint emits on. Witness deviation from a pin reports as fixed_column_violations.

§ Gauges

algebraic_and_evaluation_perfect_hiding was green and proved nothing: it asserted that a non-constant polynomial takes different values at different random points, and would have passed with trace-column hiding entirely absent.

• eval_claim_recovery.rs, zk_security.rs: recompute the MLE offline at the replayed r_final and flip. Raw mode recovers the secret, ZK mode does not.
• wire_census.rs: every published field element of a real proof maps to one line of the simulator's view inventory, destructuring every wire struct with no .., hence a new field element cannot reach the wire without breaking the build until someone classifies it.
• hiding_rejections.rs: bumps each absorbed value and each outer segment field in turn, pinning every moved check listed above.
• generator.rs: 64 fixed-seed samples over geometry, four gate families, bus topology and ZK on one seed in three. Per sample the honest proof verifies, a forged public input is rejected, a drifted id is rejected as ProgramIdMismatch. 1.3 s release.
• Checked-in floors and parity suites pin the rest: every selector None or fixed, the per-table roots that fire on a zero trace, empty-trace and short-chain forgeries, Circuit output against hand-authored twins, the statement compiler against ast.evaluate, and every declared fixed shape against its generated trace at all six post-quantum levels.
• hekate-scribble loses its control-language module and both transition-table suites; MutationKind::FlipSelector is now a fixed-column mismatch on every table.

§ Security accounting

The inner figure is min(ldt_bits, proximity_bits) with proximity_bits = field_bits - log2(encoded_width), the BCIKS20 proximity-gap term of the random column fold; it was previously capped at the field width, which credited a term the protocol does not deliver. At an 8192-wide row code the LDT term is over 160 bits and the proximity term is 115, and the smaller one governs. The outer figure takes the minimum of the Ligero query term and its additive (e + 1) / |F| term. MIN_PRODUCTION_BITS moves from 128 to 110 to match: nothing became weaker, the number became honest, and it is now a floor a real geometry can clear rather than a label.

§ Performance

Signed public cdylib 0.12.0, table-math, Apple M3 Max, -C target-cpu=native, three runs per cell: fastest for time, mean for proof size, lowest for peak. Peak is the larger of phys_footprint_peak and ru_maxrss. Cells are ZK / base, and ZK is the default from this release.

Against 0.33.0's published means the base arm proves 7 to 17% faster, and the ZK arm lands between 4% slower and 10% faster. Hiding is what consumes that window: up to 13% on prove time, 11 to 19% on proof size, and 1.3 to 3.2 times the verification. keccak_inline 2^15 pays 39% on proof size, being the one workload small enough for a fixed outer segment to dominate.

The outer argument is 160 to 260 KiB and tracks the statement shape rather than the trace height. Everything above it is the blind unit, one committed column per master. fibonacci_raw is five physical columns wide, and there the blind column pushes the commitment grid to the next power of two: at 2^26 the tensor vectors go 1,117,517 to 2,231,629 bytes, exactly grid_cols 2^16 to 2^17, which is also where its 58 to 75% proof-size delta and its peak memory go.

Pinned liveness costs one shape MLE per pinned column at verify: 0.5 to 1 µs per small-stride block, about 11 µs per 107-entry pattern block, height-independent. A full composite's pins land under 0.5 ms against the 38 to 62 ms composite verifies above.

§ License

Hekate moves to AGPL-3.0-only with this release. Every version up to and including 0.33.0 stays Apache-2.0 and that grant is not revoked. The project is dual-licensed: commercial licenses are available from Oumuamua Labs, info@oumuamua.dev.

Linking the open workspace against the proprietary prover shared library is covered by LICENSE-EXCEPTION, an additional permission under AGPL section 7. It covers that library and nothing else, grants no right in it, and does not relieve a network operator of section 13 with respect to the Hekate portion of a combined work.

§ Breaking

• Wire format. Proof v4 to v5, adding pad_root and an OuterProof of aux_root, three responses and two OuterOpening records. Bundle v2 to v4: the config table sheds inv_rate and sumcheck_blinding_factor and gains outer_queries and zero_knowledge; the fixed-column table carries Cadence and Segments, digest tags 6 and 7. Predecessors fail at deserialization. Re-prove.
• program_id. Changes for every program in the workspace. Fixed columns are part of identity and every table gained some; the domain tag is hekate-program-id-v2. Deployments pin the new constant.
• verify signature. verify(program_id: &[u8; 32], program, instance, proof, transcript, config), with Error::ProgramIdMismatch { actual } on mismatch.
• Transcript. program_id is absorbed first, before num_columns. zero_knowledge and outer_queries join the config values absorbed before the first challenge. pad_root follows the main and chiplet headers; the outer segment runs aux_root, outer_r, outer_w, outer_r_lin, outer_q, outer_r_quad, outer_p0, then one outer_idx per query.
• Config. inv_rate and sumcheck_blinding_factor removed, outer_queries and zero_knowledge added. inv_rate becomes the constant INV_RATE alongside OUTER_RATE_LOG2 and OUTER_ROWS, because a caller-tunable rate is a divergence waiting to happen. Callers that set a blinding factor use zero_knowledge and read blind_units(). Config::default() is prod() and proves in zero knowledge; the raw protocol is asked for.
• Security floor. MIN_PRODUCTION_BITS 128 to 110, with the proximity term now counted. A geometry that passed on the old cap and fails now was never delivering the number it reported.
• Admission. A bus selector that is not None or an overlay-shaped fixed column is rejected at ChipletDef::from_air, ChipletDef::from_wire, Circuit::compile and verify entry. An AIR whose num_columns disagrees with its virtual layout, or whose sumcheck degree needs more than 16 interpolation points, is rejected at admission instead of panicking later.
• Constructors. Every chiplet constructor gains its count or schedule parameter; MlDsaChiplet::new gains msg_len.
• Moves. hekate_sdk::{program_id, program_id_hex} are hekate_program::digest::{program_id, program_id_hex}, with program_id_of added.
• Deleted public API. validate_paired_bus_mutex, unconstrained_bit_selectors, assert_paired_bus_mutex, fixed_gated_witness_roots, fix_narrowed, validate_justification, the hekate_scribble control-language module, preflight selector_mutex_violations, and SecurityMetrics::soundness_error, the last reason hekate-core would not build as true no_std without rayon in the graph.
• New public API. Modules hekate_core::{outer, ligero}, hekate_program::{circuit, predicate, outer, linearized}, hekate_verifier::outer. Types FixedShape::{Cadence, Segments}, CadenceSegment, Service, ServiceSlot, NttSchedule, NttRun, OuterGeometry, Pad, Masking, RowEncoder, OpenedWeights, Opening, ProductMask. Functions validate_fixed_selectors, FixedColumn::{prefix, segments}, FixedShape::is_overlay, Config::{outer_geom, outer_security_bits, outer_field_term_bits, check_outer_security, blind_units}, verify_outer, weights_at_columns, mlkem::{ntt_forward_traced, ntt_inverse_traced}, BusDiagnostic::{clock_collisions, inert}, SecurityMetrics::proximity_bits.
• Features. hekate-core gains an optional rayon dependency behind its existing parallel feature; hekate-verifier's parallel now forwards to hekate-core and hekate-program.
• Prover cdylib 0.12.0, signed (SHA-256, Ed25519, ML-DSA-65). 0.11.0 neither produces nor reads v5 proofs.
• License. AGPL-3.0-only, or a commercial license from Oumuamua Labs.
• Version. Workspace 0.33.0 to 0.34.0; hekate-keccak and hekate-aes 0.7.0; hekate-pqc 0.8.0.

§ Not promised

• Circuit semantics. A pinned id binds which circuit is verified, not that it computes what its name says.
• Determination of the published cell by the AIR. The engine gives the construction and does not certify its use. A certifier answering an undecidable question over author-chosen structure maps every shape it fails to recognise to accept, which is the defect this release removed.
• Workload privacy. Fixed liveness makes activity patterns public by construction. Nothing new leaks in the shipped set.
• Data-dependent activity counts. Pin every row and fill with canonical no-ops. No shipped circuit needs the alternative.