wrap steps — the recursive proof to ≤ 64 KB, 2026-10-10
superseded (2026-10-27): the chain measured here was replaced by 4i:16,8i,9f:24 (wrap-fastverify-2026-10.md) and then 4i:16,7i:22,9f:26 (zheng#61, wrap::SHIPPED, proof-stack-review-2026-10.md: final proof ≤ 64,213 B over every transcript).
Last gate of the proof-system repair (soft3
proposals/proof-system-repair.md): the constant-size recursive proof of
audit/recursion-2026-10.md (282–285 KB, verify 18–38 ms) shrunk by
proving its final verifier. Contract: specs/recursion.md § final
verifier, § field-native WHIR, § wrap; ledger: specs/soundness.md
§ field-native WHIR and wrap.
Stand: zheng feat/wrap (on feat/ivc 3148a42, with
feat/machine-opcodes 9d758ed merged), lens feat/field-native-whir (on
feat/accumulation). Apple M4 Max, 16 cores, 48 GB, rustc 1.95.0,
--release. The machine was shared with other agents (load 13–40);
times are single runs (verify: median of 5 or 11) and upper bounds of a
quiet machine. Sizes are deterministic.
1. what was built
| piece | where |
|---|---|
field-native batched WHIR (lens schedule; duplex transcript; field-native words; verifier over Ops); words sharing one tree; 4-ary trees; one-word openings with any weights (eq, pow, row × column, native linear) |
recursion/whir/, word.rs (Group, Arity); lens whir::batch (soundness rows) |
constraints over any arithmetic (air::num::Num: Fp3 or Sym, a recorded graph); graph → gates compiler (affine forms, fused products) |
air/num.rs, recursion/expr.rs; machine and circuit constraints made generic |
| the IVC decider field-native: the last accumulator a field-native word; one batched opening of [accumulator, the circuit key's two words under one tree] carries the deferred key claim | recursion/decide.rs |
the final verifier over Ops (last step, final-state checks, G through its graph, decider); ivc::verify runs it natively |
recursion/finalv.rs |
| wrap levels: inner (memory argument, committed key, 4-ary trees — verifiable by the circuit), final (one committed word, linear wiring, key evaluated by the verifier, binary tree) | recursion/wrap/ |
the outermost proof (FinalProof: header, deferred nox-public claim, final wrap) and its verifier from the statement |
wrap::verify_statement, wrap::verify_final |
The chain measured: IVC (rate 1/16) → wrap 0 inner (rate 1/64, the IVC final verifier, 53,042 rows → 2^16) → wrap 1 inner (rate 1/256, 24 grinding bits, 19,275 rows → 2^15) → wrap 2 final (rate 1/256, 30 grinding bits, 15,606 rows → 2^14, ℓ = 20). Circuit census of the final level: 19,015 gates, 97 decompositions, 2,616 permutation blocks.
2. gates
Command: ZHENG_WRAP=6i,8i,8f:30 wrap_bench <fixture> (IVC proofs stored
and reused, ZHENG_IVC_DIR). final B = FinalProof::to_bytes
(header 49 · nox-public claim 1,272 · AIR messages 4,736 · opening).
Prove = the IVC proof, then the three wrap levels.
| fixture | cycles | IVC steps | final B | verify ms (prepared) | IVC prove s | wrap 0 / 1 / 2 prove s |
|---|---|---|---|---|---|---|
| add.tri (7, 5) | 33 | 1 | 62,589 | 13.2–13.9 | 26.8 | 84.5 / 168.4 / 731.9 |
| hash.tri (7) | 61 | 1 | 62,781 | 12.4 | 42.9 | 173.2 / 276.9 / 756.9 |
| merkle-32 | 1,121 | 1 | 62,525 | 14.6 | 27.6 | 86.7 / 196.1 / 555.7 |
| tree-12 | 16,383 | 2 | 62,877 | 11.9 | 46.5 | 78.9 / 183.1 / 973.3 |
| rec-16 | 1,572,850 | 105 | 62,717 | 13.6 | 2,718.6 (45.3 min) | 131.8 / 282.8 / 464.0 |
(wrap_bench prints the proof without the 49-byte header; the table
adds it: 62,540 + 49 for add.tri, measured by wrap_flip.) Peak memory
32–38 GB (maximum resident set), from the 1/256 levels' codewords.
Against the goals:
| gate | measured | verdict |
|---|---|---|
| ≤ 64 KB (65,536 B) | 62,525–62,877 B, flat from 33 to 1.57M cycles | met |
| verify ≤ 1 ms | 6.4–7.2 ms on 16 threads, 10.1–10.9 ms on one (statement prepared; wrap_flip, after the final-pass optimisation 9ebea09); 11.9–14.6 ms in the table's wrap_bench runs (earlier code) |
missed (×6–15) |
| every ledger row ≥ 128 | weakest per level: 128.24 / 128.29 / 128.02 (wrap::ledger, checked in wrap_bench and wrap::tests) |
met; the wrap composition row is conjectured, as the IVC's |
| post-quantum, hash-only | hemera Merkle trees and transcripts; no pairing, no group | met |
| bit-flip scan of a final proof: 0 accepted | add.tri, 62,589 B: 500,712 flips, 499,813 decoded, 0 accepted, 0 panics (835 s; repeated twice on the final code: 0 accepted); rec-16, 62,717 B: 501,736 flips, 500,844 decoded, 0 accepted (twice, 679 / 554 s) (wrap_flip) |
met |
| wrong statements / tampering refused | tests/wrap.rs: wrong output, input, cycle count; wrong deferred claim (value, point); tampered root, OOD, zerocheck, column, successor, folding sumcheck, final polynomial, opened symbol, segments, chain, start; a tampered inner wrap |
met |
3. where the bytes and the time are
Final proof, 62,589 B: header 49, nox-public claim 1,272 (n + 37 Fp3:
statement data the verifier evaluates), AIR 4,736 (zerocheck 14 × 9 Fp3,
root, OOD, 49 columns at ρ, the 20 successor columns the constraints read),
opening 56,532 (rounds of 25 / 18 / 15 queries at rates 1/256, 1/2048,
1/16384; final polynomial 2^8 Fp3).
Verify (add.tri, ZHENG_TIMING): the opening ≈ 9–12 ms (round-0 leaf
sponges and paths, ≈ 1,000 permutations natively; the wiring weight's
closing term over 2^20 cells), the constraints' graph 1.5 ms, the key's
columns at ρ 1.5 ms, the nox-public claim and the public digest < 1 ms.
Prove: the final level's opening dominates (grinding 30 bits per round, 2–4 rounds; 5–12 min), then the 1/256 inner level (3–5 min).
4. what was tried
| design | final B (add.tri) | note |
|---|---|---|
| one inner level (1/16) → final with two trees (W1, W2) and the key evaluated natively | 118,664 | first chain |
| same, final level one word, linear wiring | 91,084 | the second tree is the memory argument's |
| inner 1/64 → inner 1/256 → final 1/256, binary inner trees | — | final circuit 20,430 rows (2^15) |
| 4-ary inner trees | — | final circuit 14,752–15,606 rows (2^14) |
| direct opening (claims as WHIR weights; only read successor columns) | 62,540 + 49 | shipped |
5. what is left
- verify ≤ 1 ms: missed by ×6–10 (6.4–7.2 ms on 16 threads). The opening's hashing (≈ 1,000
permutations, single-threaded) and the wiring weight's pass over the
word are the floor of this design at today's hemera speed; candidates:
batching the final opening's Merkle checks (the step verifier's batched
mode is not used by the direct opening yet), a structured wiring
(
u_λwith a closed-form MLE), fewer round-0 queries (rate 1/1024 at ≈ 4 GB more prover memory). - prover memory 32–38 GB and 13–20 min for the wrap chain: the 1/256 levels' Fp3 combinations and codewords; unoptimised.
- the deferred nox-public claim travels (1,272 B); in-circuit evaluation needs the statement's init entries as bounded witness.
- no envelope profile for wrapped proofs (joy).
- no external review of the wrap circuit or of the linear-wiring final mode; the tests check them against the native verifier and tampering.