one proof — the repair of zheng

hemera note (2026-10-16): the hash row below is decided — hemera 0.4 (hemera#15: x⁷ in every round, 6 + 6 + 48 rounds, Poseidon2 reference matrices, 32-byte digest kept) is frozen on hemera release/0.4 and under the public cryptanalysis campaign (hemera/audit/campaign.md); the "experimental / inverse-S-box" statements below are the 0.3 record.

0. goal

fixed by the owner on 2026-10-09:

and, fixed by the owner on 2026-10-10, the prover:

and, fixed by the owner on 2026-10-14 ("the product doesn't exist without it"), the gate on the user's device:

measured 2026-10-14 (audit/proof-latency-2026-10.md; zheng#64, lens#25): profile 1 meets the gate cold and warm on Metal for every product-shaped statement up to Merkle depth 16 (hash.tri 0.07 s, a ticket 0.10 s, a 4-ticket seal 0.19 s, depth-12 balance opening 0.36 s, depth-16 membership 0.48 s; ≤ 64 KB, ≥ 128 bits). Depth-32 membership takes 1.13 s cold and 0.61 s warm with a held key. Veil (P1) passes to depth 12 (0.71 s); depth 16+ is over 1 s. P2, P3 and oikos have no statement yet.

measured 2026-10-10…13 (Apple M4 Max, machine shared, load 25–156; zheng audit/prover-profile-2026-10.md, zheng#59, lens#23, joy#40; proofs byte-identical on every backend): profile 1 hash.tri 17.7 s → 1.4 s Metal, 2.8 s WebGPU, 5.5 s CPU (joy prove --succinct; 0.4 s in the library on Metal); profile 5 (IVC, one 2¹⁵-row step) 9.6 s Metal against 22.6 s CPU on zheng#58's head; the wrap chain (profile 6) 115 s Metal against 239 s CPU in the same window (zheng#58 alone: 83 s on a quieter machine), CPU time 330 s against 1,771 s. what reaches seconds today is the one-relation class and, on a GPU, one IVC step; the wrap chain is about two minutes — what remains is constraint evaluation in the zerocheck (CPU in every backend), the coset NTTs of streamed words, and the chain's size.

and the system that produces it is simple, reliable and flexible. this page records what is broken in zheng and lens, the design with the fewest parts, where recursion is and is not needed, and the gates that decide each phase, and how the change rides the release train through nine repositories. it closes on the last merge. the boundaries it respects are component boundaries; the sibling proposals are network-planes and tade-one-exchange.

1. where the numbers stand

sources: zheng/audit/compact-relation-2026-10-09.md, WHIR 2024/1586, SmallWood, LaBinius 2026/2103, SoK repricing 2026/1367; the lineage of the commitment choice is told in fri-to-whir and whirlaway, and the comparison with STARKs in zheng-vs-starks. the smallest post-quantum proof anyone has shown is ~50 KB; a 10 KB one for arbitrary computation does not exist; 64 KB is reachable hash-only and beats every production chain 3–15×.

2. what is broken

the old "constant proof" of zheng 0.3.x rested on eight false or unproven things, and the hash beneath all of them is not yet analysed (last row). none was the Merkle tree (merklezation).

the owner's 2026-09-11 fallback — derive the relation on the verifier, disclose the witness, check every row — is sound and stays as the public profile.

3. the design

seven rules, each a removal:

1. one field — Goldilocks (nebu) for everything committed; its cubic extension fp3 (extension-fields) for every challenge and evaluation point.
2. one hash — hemera (Poseidon2 over Goldilocks) for Merkle trees, Fiat–Shamir and program digests. the only assumption: hemera is a random oracle (hash function selection).
3. one code — Reed–Solomon over Goldilocks (NTT in nebu, polynomial-arithmetic). no expander codes, no conjectured distance.
4. one IOP — Spartan sumcheck over CCS of any degree (zheng#45).
5. one accumulation — ARC: hash-based, unbounded depth, up to list-decoding radius, random oracle only (2024/1731); WARP (2025/753) as the linear-time fallback. it replaces folding by homomorphism, which the stack never had.
6. one wire format, three profiles — public (disclosed witness, linear check), succinct (committed witness, ≤ 64 KB), zk (succinct + VEIL masking, 2026/683; the stack's zero knowledge page). one magic, one version, one profile byte, carried by tade.
7. the verifier derives everything it checks — the relation from the program, the public prefix from the statement — and trusts nothing from the prover but field elements and hashes (verification).

the proof, succinct profile: relation (prover and verifier compile the same CCS; only w is committed) → vk (the verifier recompiles, hashes once, absorbs the digest) → commit (w as a multilinear polynomial, RS-encoded, one hemera root) → IOP (Spartan with fp3 challenges, one claim w̃(r) = v) → open (Johnson-bound parameters, 128 bit) → wire (statement · program · profile · root · sumcheck polynomials · evaluations · opening).

byte budget for one hash (n = 2¹⁰, degree-7 CCS, 128-bit Johnson, fp3 at 24 B), WHIR as the worked example: statement 0.3 KB · Spartan 3 KB · opening 28–36 KB · final polynomial 0.5 KB → 32–40 KB expected, 64 KB the ceiling; 16–20 KB at 100 bit. verify ≈ 2,000 hemera permutations ≈ 0.5–1 ms. at n = 2²⁰: 56–70 KB, WHIR's published number.

unbounded programs: a uniform step relation (one CCS for one nox reduction step with continuity and memory arguments, zheng/audit/general-nox-relation-review.md:160-173); each step yields one proximity claim; ARC folds claims into one accumulator of fixed size (one root, one fp3 point, one value, a few cosets of openings per step); one opening decides it. proof size is independent of length only once each step's openings are checked inside the next step (IVC, §4); without it the proof grows per segment.

4. recursion — what it is here, and where it is needed

two words that the old specs (recursion, accumulator) used as one:

• accumulation — folding claims without verifying proofs: each step batches the claims of its input words into one accumulator — one root and a fixed number of claims, whatever the depth — and one decider opens the last accumulator. the accumulator is constant; the proof is not. every step leaves spot-check openings in every word it folded, and without a verifier for them inside the computation the final verifier checks every step: bytes and verify time grow per segment. measured on zheng#51 (zheng/audit/accumulation-2026-10.md): ~96 KB per 2¹⁴-row segment (~8 KB of AIR messages, ~88 KB of accumulation openings), hash.tri verifies in 5.4 ms, three segments in 40 ms; 512 statements fold into one 35 KB decider but 8.9 MB with their per-step proofs. accumulation alone saves openings, not size. it is the default step.
• recursion — a proof that verifies a proof: IVC and PCD proper. constant size comes from IVC: the accumulation verifier — not the whole proof verifier — runs inside the next step's relation, so each step's openings are checked in-relation and consumed, and what travels is one accumulator plus one decider, independent of length (ARC §2.3, WARP §1). this, and not accumulation alone, is how "any computation" is proven at constant size; it is work package R1 of the release plan, in progress. the full verifier as a nox program, verify(verify(π)), does not shrink a single proof in a hash-only world — the outer proof carries its own Merkle paths again — so it is a tool for composition.

where the stack needs recursion proper, and what each costs:

so IVC — the accumulation verifier as part of the step relation — is built in phase 3 and is what makes size constant: one step at ℓ = 20 checks 3 × 53 leaves with ~15-level paths, ≈ 3,000 hemera permutations plus byte decompositions, a ≈ 2¹⁷-row relation per step before the segment's own rows (zheng audit §7). full recursion is built once — as the second verifier of §3, in Trident — and used for composition and as the fallback; accumulation does the daily work, inside IVC. the two numbers the old specs carried for recursion, "~825 constraints per level" and "1000 levels → 2⁻¹¹⁸", described a nox verifier that was never built and are retired in §C.

5. phases and gates

every gate is a fixture and a command, not an opinion. a phase closes when its row is green on CI.

phases 1 and 2 are a month each; 3 is research-grade and measures before it commits; 4 and 5 are weeks. until 3 lands, succinct covers one relation of ≤ 2¹⁵ rows, and the "any computation" row of §0 is open.

6. how it stays sound

• soundness ledger (zheng/specs/soundness.md): one row per component — assumption, bits claimed, proven or conjectured, paper, controlling parameter. the release gate fails on any "conjectured" row in a production profile.
• attack fixtures that must be rejected: meaningless witness, zeroed constant, forged io, forged vk, truncated path, query-index replay, challenge reuse. each one a release gate.
• bit-flip scan over every byte of every fixture proof — the method that found the 2,080 dead bytes.
• differential against native: circuit digests against nox::data::hash, outputs against nox::reduce.
• two verifiers, Rust and Trident, agreeing on every fixture.
• frozen fixtures: a proof produced for a release stays accepted by every later verifier, or the format version moves.
• security parameters are data — queries, rate, grinding, extension degree in one struct, printed in the header, checked against the verifier's policy.

7. what disappears

zheng/folding (HyperNova over hemera) → zheng/accumulate (ARC). the lens loser of the bake-off; UnsupportedRecursiveOpening; the flat-hash Tensor opening; expander codes, MIN_ABS_WEIGHT, num_queries = 100·EXPANSION·k2. formats zheng-hypernova-tensor-merkle-v2, JOYEXEC1, JOYEXEC2, JOYZK003 → one format, read by a legacy tool for one release. the experimental kernels on release/0.4 leave the production path when zk lands. PublicTensor stays as the public profile. the proving path — relation, IOP, commitment, accumulation, wire — fits in ~12k lines against ~25k today.

8. open, and who closes it

9. release — this proposal as the first run of the train

the repair touches nine repositories and every product that verifies a proof. it is therefore the first change shipped end to end by the release train: candidates cut from origin on fridays, gates executable, bumps as pull requests, promotion by the owner only. the proposal is the test of that process as much as of the proofs.

propagation order — each row pins the one above it; a bump is one PR chore: <component> <version> touching Cargo.toml, CHANGELOG.md and the sibling pins:

what each soft3 version means: 0.11 — every proof the node accepts is sound (the public profile, fp3, bound statements); 0.12 — succinct proofs ≤ 16 / 64 KB on the wire, the first version a phone verifies in a millisecond; 0.13 — any computation at constant size, settlement on accumulation. the next soft3 version is 0.11 and it ships phase 1 alone.

the train's rules apply unchanged: one candidate per friday from origin/main of every repo in the closure; sources.json and receipts in <repo>/audit/release-<date>/; freeze from cut to verdict; a red gate ships as a red candidate; the owner merges bumps, promotes, publishes. two gates join the train's set for this work: the soundness ledger has no "conjectured" row on the production profile (from 0.11), and scripts/stale-proof-claims.nu returns zero (from 0.13). the launch page gets one row per candidate.

A. decisions recorded, with the argument compressed

the Merkle question. the owner asked whether the trees can go. they cannot: a flat hash C = hemera(Enc(w)) has no local opening, and the column check Enc(y)[j] = q₁ᵀ·col_j is satisfiable by a prover who never touches C (pick y', solve one linear equation per queried column). in a hash-only world a local opening costs Θ(log n) digests — a lower bound, not a layout; every hash-based system carries paths (merklezation, hash chain). the only escape is a homomorphism, i.e. lattices, at ~50 KB. the sound half of the old idea — Ligero geometry, RS rows, a column tree, y in the clear — is today's TensorMerkle and is a bake-off candidate; at n = 2¹⁰ it and WHIR land in the same 25–40 KB band, at 2²⁰ folding wins. no version brings back C = hemera(w) or 1.3 KB.

the levers on the trees, from ~36 KB for one hash: a code with a proven distance (queries from every column to ~64 — the largest win); path deduplication −30…45 %; rate 1/32 −20 % at ×2 prover; grinding 20 bits −12 %; folding factor 5 −10 %; fp3 at 24 B −3 %. honest floor 25–40 KB at 128 bit; 15–20 KB if the levers compose; zip ×0.6 on top of either.

B. lattices and the frontier, 2026-10-09

what lattices buy is the shape of accumulation, not the final byte count: a homomorphic fold with a tiny in-flight object (Neo/SuperNeo 2025/294, LatticeFold+ 2025/247, Symphony 2025/1905, PikkuFold ~5.7 KB per step 2026/1809) at the price of a second assumption (Module-SIS) and norm bookkeeping. LaBinius (2026/2103) now wins the bytes at 2²⁴ — 82.9 KiB against WHIR's 300.9 at rate ¼ — and loses the verifier 650× (713 ms against 1.1). under the goal as fixed, hash-only stands; the spike's one question is whether any lattice verifier gets under 10 ms. the binary-tower track (Binius, lens/specs/binary-tower.md) is the wrong field for a Goldilocks stack and stays out.

the scale in nox terms after zheng#45 (a hemera permutation is 176 wires and 176 rows): a hash 2–4 permutations (~2^10), a transfer with nullifier ~15 (~2^12), an ICBS position or a vote 20–40 (~2^12–2^13), a depth-32 Merkle membership ~770 (~2^17), a block, an inference step or an epoch settlement 10^4–10^7 (2^20–2^30). the small class ends at ~2^16 witness elements ≈ 370 permutations: what a person does in one signal lives below it, what a network does lives above it. this is one system with two openings behind one trait, not two proof systems.

SmallWood (2025/1085) reaches 14.1–16.5 KB on Kyber and 17.5–22.7 KB on Dilithium because their constraints are parallel — the same polynomial on many lanes — against 47–50 KB for a generic 2^12-gate circuit. a hemera permutation is parallel (sixteen lanes, one S-box, one MDS), so the lever is to describe the rounds once as a parallel sub-relation; interpolated estimate for hash.tri, not a measurement: 15–25 KB as parallel constraints, 30–40 KB as a generic CCS.

designated-verifier lattice SNARGs go lower than any public one — LUNA+ (2026/1639): 4.22 KB for R1CS 2^16 — but with a 0.54 GB CRS and a verifier holding a secret; a public network cannot use that trade.

zip (2025/1446): black-box compression of hash-based proofs to ~60 %, standard assumptions. it composes with every lever because it acts on the finished proof; phase 2 measures it.

the in-proof digest: hemera profile v2 (hemera#15) raises the identity digest to 48 or 64 bytes for post-quantum collision resistance. a Merkle node inside a proof is ephemeral — it must be forged before the verifier runs, so "harvest now, break later" does not apply — and stays 32 bytes. one permutation, two squeeze lengths; a 48-byte node would add 50 % to the dominant term for nothing.

what this proposal does not claim: no 2 KB, no 100 ns, no "Merkle-free", no proof smaller than the authentication of its own queries.

C. the ledger of stale claims

every place in the stack that still presents the old design as current — ~2 KB proofs, ~5 μs verification, "Merkle-free" Brakedown, HyperNova over hemera, the ~825/~89-constraint decider, algebraic Fiat–Shamir, "the accumulator is the proof" — swept on 2026-10-09 across every repository under ~/cyber (archives, vendored trees and zheng-pin/, a worktree of zheng, excluded). one row per document; the line numbers are in the sweep's output and in the script.

the rule is executable: scripts/stale-proof-claims.nu greps the workspace for every family of stale claim and exits 1 on any hit outside a short allow-list of dated posts and changelogs (736 raw hits in 214 files today). it is the phase-5 gate and, from the 0.13 candidate on, a gate of the release train. each earlier phase closes its own rows — phase 1 the security claims, phase 2 the sizes and the Merkle-free pages, phase 3 the fold, decider and recursion pages — so the table shrinks with the work.

actions: delete — built on the old design, no other content · superseded — keep with a banner pointing here · rewrite — the section is rewritten against §3 · number — the figure becomes the measured or target one (≤ 16 KB small, ≤ 64 KB any, ≤ 1 ms) · code — goes with the phase-5 code removal · leave — dated post or audit snapshot, erratum link only.

zheng

lens

nox

bbg

hemera

soft3

cyber — site, whitepaper, research

other repositories

pages already bannered — and whether the banner is enough

generic STARK/SNARK comparison figures that are not zheng claims (cybics/crypto/zero-knowledge, trident's stark-proofs, verifying-proofs, provable-computing, privacy trilateral) stay.

the long form of every argument above is in this file's history (git log -p proposals/proof-system-repair.md before this revision).