soundness ledger
one row per component of a production profile: the assumption it rests on,
the bits claimed, whether that number is proven or conjectured, the argument,
and the parameter that controls it. a number appears here only if it is
derived on this page and checked by the named test. the release gate of the
proof-system repair (soft3 proposals/proof-system-repair.md §6) fails on any
"conjectured" row in a production profile. conjectured rows remain — the
relation compiler, the hash, the rows that rest on the hash alone (program
digests, field-native words, message digests) and the IVC and wrap
compositions — so the repair does not pass that gate yet. The succinct
profile and the zk profile add no conjectured row of their own: they
inherit the relation-compiler and hash rows exactly as public v3 does.
hash version: the code of this crate pins cyber-hemera 0.3 (0.3.1: 4 + 4
full rounds and 16 partial rounds with the inverse S-box). every gadget,
constraint count, parameter and bit figure on this page is computed on
hemera 0.3.1. the frozen material is hemera 0.4 (hemera#15); zheng's move
to it is the draft sweep zheng#69 / #73, and the figures of that branch are
not this page's.
notation: p = 2^64 − 2^32 + 1, log2 p = 63.9999999997; Q = hemera
queries an attacker makes; "bits" = −log2 of the success probability.
production profiles
| component | assumption | bits claimed | status | argument | controlling parameter | test |
|---|---|---|---|---|---|---|
public v3 certificate (execution::certificate, envelope profile 0) |
none beyond the relation compiler: the verifier recompiles the CCS from the program, places z[0] = 1, inputs, outputs and cost itself, and evaluates every row exactly |
soundness error 0 — the check is deterministic, no challenge is drawn | proven for the compiled relation | direct evaluation; specs/execution.md | — (limits: 4096 program nodes, 64 inputs, 4096 outputs, 2^20 columns) | rs/tests/certificate_v3.rs, rs/tests/attack_fixtures.rs, certificate::malleability |
| relation compiler (program + subject shape → CCS) | the compiled CCS is satisfiable with prefix (1, io, cycles) exactly when nox reduces the program to that output at that cost |
— | conjectured (tested, not proven) | differential tests against native nox, mutated witnesses, malleability analysis (every movable wire only multiplies a zero factor) | — | execution::relation::tests, execution::tagged::*, certificate::malleability |
relation compiler — hemera node jet (execution::node, relation_node.rs) |
as the relation-compiler row; the node formula is a pure Layer-1 nox program; hemera collision resistance for what a Merkle root then means (hash row) | — (adds no error term: the gadget is exact) | tested, inherits the relation-compiler row | the compiler substitutes one permutation gadget only for a formula equal, token for token, to node::formula(); the gadget computes permute(L ‖ R ‖ 0 ‖ flags ‖ 0⁶)[0..4] (the hash_permute gadget, itself checked against hemera) and charges node::COST; the formula reduces under native nox to the same digest at that same cost for every input — its branches test constants of the formula only (round kinds, exponent runs), and its inverse is x^(p−2) so 0 ↦ 0 as in hemera; any other subject shape fails closed in both |
the formula (node::COST = 39,818 cycles, 2,235 nodes, depth 39) |
execution::node::tests, tests/node_merkle.rs (relation = nox = hemera on random paths, output and cycles; tampered sibling / direction / flag; forged root claim; malformed subjects; nox depth headroom), tests/succinct_bitflip.rs (node path, ignored) |
state v3 certificate (execution::state, envelope profile 3; also the state statements of profile 1) |
as public v3, plus: zheng authenticates the reads' StateEvidence under the statement's own state_root — the leaves fold to the root by compress4 and every carried table matches its leaf (lens Brakedown::commit of the padded fields used as bbg's table digest — commit only, never opened — length in the header) — before any read is pinned |
error 0 in zheng given the hash; a read can be forged only by a hemera collision in the root fold or in a table commitment | proven for the compiled relation; reads: the hash row | verifier pins active flag, root limbs, namespace, key, value of every read and the root in the subject; no caller-side duty remains. The statement has no context field: with the witness disclosed no relation could bind one | MAX_READS = 4096, MAX_FIELDS = 2^20 |
execution::state_v3_tests (wrong_state_root_is_rejected, an_unauthenticated_read_is_rejected_by_zheng_alone), execution::state_evidence::tests, fixture_wrong_state_root_is_rejected, tests/succinct_state.rs |
private state (execution::private_state, veil and MITH) |
as the state v3 row: zheng authenticates the evidence under the statement's own root and requires all ten public tables before they become relation constants; PublicStateTables has crate-private fields |
the scheme's own bound (zk / MITH rows); the tables add only the hash row | proven given the hash | PrivateStateStatement::{prepare, verify_veil, verify_mith} |
10 namespaces, 2048 fields | private_state_tests::every_private_state_verifier_authenticates_the_evidence_itself (wrong root, foreign evidence, re-rooted statement, altered table, altered leaf, missing table — both schemes) |
verifying keys (execution::vk) |
hemera collision resistance (digest) | a key never widens what verifies: it is derived by the verifier from the statement and checked against the statement's program key; with a transcript, the digest binds the proof to its relation | proven (the check is exact); digest binding: the hash row | program_key covers program tokens, input count, statement kind; keys have no public constructor and no deserialiser |
— | execution::vk::tests, tests/verifying_key.rs, veil::tests::keys_must_be_derived_for_the_statement |
succinct profile (execution::succinct, envelope profile 1) — composition |
Spartan IOP over Fp3 (row below) + one PCS opening (rows below); Fiat–Shamir with hemera as a random oracle | interactive: ε ≤ ε_IOP + ε_PCS; at hash.tri (m = 2^10, ℓ = 10, d = 7, t = 5) `ε_IOP ≤ 116· |
Λ | /p³ ≤ 2^-174.4, ε_PCS ≤ 2^-128.00(WHIR 1/64, k = 4, 24 grinding bits,succinct::params_for) → 128.0 bits, set by the PCS; the default prover's succinct::device_params (folding 4 up to 2^16 variables and 5 above; grinding 16 bits up to 2^17, 22 at 2^18, 24 beyond) also reaches ≥ 128 at every size 2^1…2^20 (execution::succinct::choice::tests::device_parameters_meet_the_ledger_at_every_size; without grinding 112 bits up to 2^17, 106 at 2^18, 104 beyond); non-interactive: every component is round-by-round sound with per-round error ≤ 2^-128(grinding included), so a prover makingQhemera queries succeeds with probability≤ Q · 2^-128` plus hemera collisions (Merkle binding) |
IOP and PCS bounds proven; the round-by-round → Fiat–Shamir step proven in the ROM (Canetti et al. 2019, round-by-round soundness); hemera-as-RO conjectured (hash row) | the verifier derives the relation and the pinned half p of z' = (w ‖ p) itself; only w is committed (specs/execution.md § succinct); the policy rejects any parameter set for which lens proves < 128 bits at the proof's ℓ |
succinct — Spartan IOP over Fp3 (spartan::iop + spartan::reduce, F = Fp3) |
Schwartz–Zippel; sumcheck (Lund–Fortnow–Karloff–Nisan 1992) | `ε_IOP ≤ | Λ | ·(log m · (d + 2) + 2(ℓ + 1) + t − 1) / p³(the committed word is not OOD-bound before the IOP, so each round is a union over the listΛof codewords near it, |
Λ | ≤ μ/ρ ≤ 2^{10.7}for WHIR's Johnson round 0 at rate 1/64, WHIR Thm 4.3): outer sumchecklog mrounds of degreed + 1, τby Schwartz–Zippel oneq (log m / p³), γ batching ((t − 1)/p³), inner sumcheck ℓ + 1rounds of degree 2; atm = 2^20, ℓ = 20, d = 7, t = 5: 226· |
succinct — WHIR opening (lens Whir, id 1) |
Reed–Solomon proximity up to the Johnson bound; hemera Merkle trees binding | security_bits(params, ℓ) = min over WHIR's round-by-round terms (lens WhirConfig::terms), grinding included; the policy requires ≥ 128 |
proven (lens specs/whir.md, WHIR eprint 2024/1586 Thm 5.2/7.5; Johnson-regime MCA from BCGM eprint 2025/2051 Lemma 9.3) |
lens audit rs-whir-pcs-2026-10.md |
rate, folding factor, grinding, max_final_vars |
lens rspcs tests; tests/succinct_bitflip.rs |
succinct — TensorRs opening (lens TensorRs, id 2) |
Reed–Solomon proximity in the unique-decoding regime; hemera Merkle tree binding | min(α round, column round) from lens TensorConfig, grinding included; ≥ 128 by policy |
proven (lens specs/tensor-rs.md) |
as above | rate, grinding, shape | lens rspcs tests; tests/succinct_bitflip.rs |
zk profile (execution::veil, envelope profile 2 scheme 2) — knowledge soundness |
masked Spartan IOP over Fp3 (next row) + the hiding opening (row after); Fiat–Shamir with hemera as a random oracle | interactive: ε ≤ ε_IOP + ε_open; at the hash of a secret preimage (log m = 10, d + 1 = 8, ℓ = 11, t = 5): ε_IOP = 119/p³ = 2^-185.1, ε_open ≤ 2^-128.2 (rate 1/32, 16 grinding bits, 123 columns) → 128.2 bits, set by the opening; non-interactive: round-by-round with every round ≤ 2^-128, ≤ Q·2^-128 plus hemera collisions |
proven, as the succinct row; hemera-as-RO conjectured (hash row) | the masked relation is equisatisfiable with the statement's (every masking row holds for any value of its fresh columns); every committed value, including both masks, is fixed before the first challenge; the policy rejects any parameter set proven below 128 bits | rate, grinding, k, ℓ, log m, d, t |
execution::veil::tests, tests/veil_profile.rs (bit-flip scan) |
zk — masked Spartan IOP (veil::protocol) |
Schwartz–Zippel; sumcheck | ε_IOP ≤ (log m·(d + 2) + 2ℓ + t + 3)/p³: outer sumcheck log m rounds of degree d + 1 and τ (log m/p³), the mask sums bound by ρ1, ρ2 (1/p³ each: ρ is drawn after Σ g and g is committed), inner ℓ rounds of degree 2, γ ((t − 1)/p³), λ combining the two final claims (1/p³) |
proven | g1(ρ_x) is derived from the outer final claim and checked with C2 inside one opened linear claim; the pinned half's contribution P is computed by the verifier |
challenge field, d, log m, ℓ, t |
veil::tests, veil::libra::tests |
zk — hiding opening (veil::hiding) |
Reed–Solomon proximity, unique decoding; hemera Merkle binding | ε_open ≤ (T − 1)·N/p³ + ((1 + (2K − 1)/N)/2)^q·2^-pow + 1/p³: correlated agreement for the powers generator (BCIKS20, WHIR eprint 2024/1586 Thm 4.8) over the T codeword rows; per query ≤ max(1 − e/N, (2K − 1 + e)/N) with e = ⌊(N − 2K + 1)/2⌋, 2K bounding the true linear polynomial's degree; ρ_L binds the claimed value |
proven (veil::hiding module docs) |
Ligero (Ames, Hazay, Ishai, Venkitasubramaniam, CCS 2017) with RS rows and Fp3 challenges | rate, grinding, k (K = 2k) |
veil::hiding::tests, veil::tests::every_admissible_parameter_set_carries_128_proven_bits |
zk — zero knowledge (veil) |
hemera as a random oracle (salted leaves) | honest-verifier statistical zero knowledge of the interactive protocol, distance ≤ ε_v + 2/p³ + Q·2^-256, ε_v ≤ types·log m/p (types = 3 or 5) — at log m = 10, five types: ≤ 50/p = 2^-58.4; after Fiat–Shamir, zero knowledge in the random-oracle model |
proven (argument below); not constant time | (1) Libra masks: in every round the coefficients of degree ≥ 1 carry fresh uniform mask coefficients scaled by ρ·2^{R−1−j} ≠ 0, so the round messages are uniform among the transcripts passing the consistency checks, for any witness (Xie et al., Libra, CRYPTO 2019, eprint 2019/317, §4.1); neither mask's evaluation is ever sent alone; (2) the evaluations v are uniform on Fp3^t given ρ_x: each masking type adds Σ eq(ρ_x, row)·s with uniform s, uniform as soon as its three eq weights are F_p-independent (fails with probability ≤ log m/p per type: union over p² projective relations, Schwartz–Zippel over Fp3), and the five types are an invertible change of variables; (3) the opening: data rows' k ≥ t padding coefficients make their opened values uniform, p_P and q are one-time padded by m_P and m_a + X^K m_b except [X^{k−1}]q = V + ρ_L μ with μ uniform, the masking rows' opened values follow, and unopened leaves carry 256-bit salts; (4) the Fiat–Shamir step: Ben-Sasson, Chiesa, Spooner, "Interactive Oracle Proofs", TCC 2016-B, eprint 2016/116 (the BCS transformation preserves honest-verifier zero knowledge with salted leaves). VEIL (eprint 2026/683) is the target compiler named in the repair proposal; its full text was not accessible when this was built, and this construction is the standard zk-sumcheck + masked-PCS one, not VEIL |
masking rows per type (3), k > t, salt (4 limbs); prover coins from the counter-mode PRF of veil::coins add its advantage ≤ N/p^4 + N·q/p^8 + (q + N)²/p^16 (ideal permutation, q blocks, N offline hemera queries; audit/veil-coins-2026-10.md) |
veil::zk_tests (chi-square: revealed values uniform and identically distributed for two witnesses of one statement), veil::pad::tests |
private MITH (execution::zk, ZHMITH01, envelope profile 2 scheme 1) |
hemera commitments binding; Fiat–Shamir with hemera as a random oracle | interactive: (2/3)^219 = 2^-128.107, i.e. 128.1 bits; non-interactive (ROM): ≤ (Q + 1) · 2^-128.107 plus hemera collisions |
interactive bound proven (3-special soundness of the ZKBoo (2,3)-decomposition, Giacomelli–Madsen–Orlandi 2016); ROM transform proven; hemera-as-RO conjectured; post-quantum (QROM) not claimed | specs/native-private-ccs.md | REPETITIONS = 219 (218 would give 2^-127.5) |
zk::soundness_tests |
| MITH challenges | hemera XOF output limbs uniform on F_p | trits exactly uniform | proven given the limbs | rejection: limbs < p − 1, p − 1 ≡ 0 mod 3, trit = limb mod 3 |
— | zk::soundness_tests::challenge_trits_come_from_an_exact_rejection_sampler |
transcript, base-field challenge (Transcript::squeeze_challenge, wide rule) |
hemera XOF as a random oracle | statistical distance from uniform ≤ p / 2^192 < 2^-128 per limb for uniform bytes; exactly uniform for hemera's canonical-limb output |
proven | each limb is a 192-bit integer (three output limbs) reduced mod p | 24 bytes per limb | transcript::tests::reduce_192_is_the_integer_modulo_p, hemera_output_limbs_are_canonical |
transcript, extension challenge (Transcript::squeeze_fp3) |
as above; t³ − t − 1 irreducible over F_p |
three limbs, each < 2^-128 from uniform; field size p³ = 2^191.9999999990 |
proven | gcd(x^p − x, t³ − t − 1) = 1 computed in the test |
— | field::tests::fp3_modulus_has_no_root_in_goldilocks, transcript::tests::fp3_challenges_* |
| hash (hemera, 4-limb output) | collision resistance and random-oracle behaviour of Poseidon2 over Goldilocks with hemera's parameters | generic birthday bound p^2 = 2^127.9999999993 classical; p^(4/3) ≈ 2^85.3 quantum (BHT) |
conjectured. the code proves and hashes with hemera 0.3.1 (inverse S-box partial rounds, parameters marked experimental). the frozen material is hemera 0.4 (hemera#15: x⁷ in every round, 6 + 6 full and 48 partial rounds, Poseidon2 reference layers, frozen 2026-10-16), under the public cryptanalysis campaign (hemera audit/campaign.md, gate G3); zheng moves to it with zheng#69 / #73. generic bounds until the campaign passes |
generic bounds only | hemera round counts and output width (hemera repo) | — |
machine proofs and accumulation (envelope profile 4)
K = Fp3, |K| = p³ = 2^191.9999999990. Every term below is a
round-by-round error of one round; the bits of a proof are the minimum
over its rounds, and a proof of N steps has O(N) rounds (see the
composition row).
| component | assumption | bits claimed | status | argument | controlling parameter | test |
|---|---|---|---|---|---|---|
nox machine relation (machine, specs/machine.md) |
a trace satisfying every row constraint exists exactly when nox::reduce (no jets, unbounded arena) returns the statement's output after its cycles, for some call witnesses, with every look answered from the statement's authenticated state; nox's bound() is an upper bound of every covered formula's cost (native evaluation partitions the budget by it) |
— | tested, not proven: twenty single-opcode programs, 36 lt/word cases, axis addresses up to p − 1, calls with atom and pair witnesses, looks over authenticated tables, joy's hash.tri/add.tri (incl. p − 1), an 11-hash chain, Merkle paths, addition trees agree with nox::reduce on output and cycles; every native failure class fails; tampered traces violate it; non-canonical aliases (v + p) of lt operands and axis addresses violate exactly the canonical check; the phase-3 review found no under-constrained cell (the opcodes added afterwards — lt, word, call, look, 63-level axis — have had no independent review) |
specs/machine.md § transitions; eq on atoms by value and the look root check (digest of the root noun) assume hemera collision resistance (hash row); look reads are authenticated by zheng under the statement's root as state v3 (hash row) |
coverage: opcodes 0–17; axis < p |
machine::tests, machine::tests_ops, tests/machine.rs |
machine AIR fresh-word binding (air::commit_bound) |
out-of-domain samples (WHIR Lemma 4.25) | `( | Λ | ²/2)(2^ℓ/ | K | )^swiths = fresh_ood(whir, ℓ)→ ≥ 128 (e.g. 155 atℓ = 20, rate 1/16, s = 1`) |
machine AIR zerocheck (air::zerocheck) |
Schwartz–Zippel; sumcheck (on the one codeword left by the binding row) | μ: `(C − 1)/ |
K | (C= 604 constraints) → 182.8;τ: n/ |
K | ; per round (D + 1)/ |
machine AIR column reduction (air::shift) |
Schwartz–Zippel; sumcheck | γ: `log2(cols)/ |
K | ; β, ζ: 1/ |
K | ; per round 2/ |
machine memory (logUp, machine::memory) |
logarithmic-derivative uniqueness (Haböck, eprint 2022/1530, Lemma 5: Σ 1/(X − a_i) = Σ m_j/(X − b_j) as rational functions iff the multisets agree, for characteristic above the number of terms); fingerprint injectivity |
α: `T/ |
K | forT slot terms (T ≤ 2^{n+2}per segment, all segments together≤ 2^26here) → ≥ 166;β(fingerprint, degree 5, union overT²/2pairs of tuples):5·T²/(2 |
K | )→ 138.6 atT = 2^26; ≥ 128 needs T ≤ 2^31` |
accumulation step (accumulate::step, specs/accumulation.md) |
Johnson bound for RS and interleaved RS (WHIR Thm 4.3, Lemma 4.4); mutual correlated agreement of the powers generator (BCGM eprint 2025/2051 Lemma 9.3 / Thm 9.2; unique decoding WHIR Thm 4.8 with Cor 4.11) and its list-decoding consequence (the argument of WHIR Lemma 4.13 with BCGM Definition 3.14); OOD (WHIR Lemma 4.25); spot checks (WARP eprint 2025/753 Lemma 7.3); sumcheck | per round ≥ 128 with grinding: γ ` |
Λ | (J−1)/ | K | , sumcheck 2 |
decider (accumulate::decide) |
as the accumulation sumcheck rows (m = 1) and WHIR over an Fp3 word |
min( WHIR security_bits(whir, ℓ) , batching/sumcheck rows ) ≥ 128 |
proven (WHIR row; Fp3 commitments: lens specs/whir.md § Fp3 messages) |
— | WHIR parameters | accumulate::tests::decider_* |
composition over N steps (machine segments, CCS folds) |
Fiat–Shamir with hemera as a random oracle | interactive (no grinding): the sum over rounds (linear in N), dominated per step by the combination round 2^{-(128 − comb_pow(m))} and the positions round 2^{-(128 − query_pow)}; non-interactive (ROM, grinding priced in): every round ≤ 2^-128, so ≤ Q·2^-128 plus hemera collisions for a prover with Q hemera queries, independent of N |
RBR → FS proven (Canetti et al. 2019; WARP Appendix B for reductions); hemera-as-RO conjectured (hash row) | one transcript: statement, AIR rounds of every segment, every step, the decider | — | tests/machine.rs (segment swap rejected) |
program binding by digest (profiles 4–6, machine::program_digest) |
hemera collision resistance (hash row) | a proof for one program verifies against another only if their canonical token encodings collide under hemera (domain zheng-nox-program-v1): 2^128 classical |
conjectured (hash row) | the envelope carries the digest; the verifier recomputes it from the program it is given and checks equality before decoding the proof; MachineStatement::bytes v2 puts the same digest into the machine transcript and the IVC statement digest, and the init entries are derived from the given program |
— | tests/{machine,recursive_envelope,wrapped_envelope}.rs (another program refused at decode and at verify; a swapped digest refused) |
recursion (rs/src/recursion/, recursion.md; envelope profile 5)
Parameters measured here: WHIR rate 1/16, folding 4, 24 grinding bits,
Johnson; steps of 2^15 rows, words of ℓ = 21 variables; accumulation
of m = 4 words with J = 64 claims (t = 53, s = 1, query_pow = 24,
comb_pow = 22). Every number below is printed and checked ≥ 128 by
recursion::params::tests::every_ledger_row_of_the_recursion_profile_reaches_128_bits.
Shipped since audit/wrap-fastverify-2026-10.md (ivc::SHIPPED_POW):
the same profile with 16 grinding bits per challenge — J = 69
claims, t = 58 spot checks, query_pow = 16, comb_pow = 17; the
step circuit 29,628 of 2^15 rows (examples/ivc_plan). Its rows, checked
≥ 128 by the same test: combine 128.34, spot 128.28; decider batch
combine 128.92, fold ≥ 128.43, shift ≥ 128.22, fin 129.00, OOD ≥ 154.8;
the other rows as below (they do not depend on grinding). Interactively
(every grinding removed) the weakest round carries 111.34 bits (104.01
at 24 grinding bits).
Shipped under profile 6 since audit/ivc-speed-2026-10.md
(ivc::SHIPPED_RATE, every IVC tree 4-ary, the decider's schedule
rebalanced — recursion::whir::schedule): rate 1/8, 16 grinding bits —
J = 88 claims, t = 77 spot checks, query_pow = 16, comb_pow = 17;
the step circuit 24,259 of 2^15 rows. Rows: combine 128.19, spot 128.08;
decider batch combine 128.80, fold ≥ 128.24, shift ≥ 128.04, fin 128.11,
OOD ≥ 154.4; interactively the weakest round carries 111.04 bits (the
decider's second shift after its 17 query bits). The tree fan-in changes
no IOP row (binding is the words row).
| component | assumption | bits claimed | status | argument | controlling parameter | test |
|---|---|---|---|---|---|---|
field-native transcript (recursion::sponge) |
hemera's permutation as an ideal permutation; capacity 7 lanes | challenges: output limbs, exactly uniform on F_p (no byte reduction); indices: low k ≤ 32 bits of a limb v ≠ p − 1, exactly uniform since 2^k | p − 1; generic sponge bound 2^{c·64/2} = 2^{224} for 7 capacity lanes, above the hash row's 2^128 digest bound |
proven given the ideal permutation; hemera conjectured (hash row) | overwrite duplex with a fixed message schedule (every protocol absorbs a fixed number of items per round), domain tags per use | rate 9, tags | recursion::sponge via every recursion test |
field-native words (recursion::word) |
hemera collision resistance (4-limb digests) | binding as the hash row (2^128 classical) |
conjectured (hash row) | leaf = sponge (tag LEAF) over the symbols, node = perm(l ‖ r ‖ NODE_TAG ‖ 0⁷)[0..4], a 4-ary node (inner wrap levels and every IVC tree) the truncated permutation of its four children perm(c0 ‖ c1 ‖ c2 ‖ c3)[0..4] (ideal-permutation collision bound 2^{128} for 4-limb outputs; a 4-ary node's input carries no tag and its siblings are the prover's, so it can equal a binary node's or a leaf block's input — binding rests on the verifier's fixed level schedule (depth and fan-in per level from the shape, never parsed two ways) and on collision resistance of the truncated permutation, not on domain separation between the three kinds); words committed together may share a tree (a leaf hashes every member's symbols); code, domain and distance are lens's round-0 layout, so the accumulation rows are unchanged |
— | recursion::word::tests |
| step zerocheck (machine ‖ circuit) | Schwartz–Zippel; sumcheck on the one codeword each fresh word is OOD-bound to | μ structured powers μ1^a μ2^b μ3^c (B = 9): degree 3(B−1) = 24 → 187.4; τ: `n/ |
K | ; per round 10/ |
K | ` → 188.7 |
shift reduction and boundary claims (air/shift.rs over the duplex) |
Schwartz–Zippel | rounds of degree 2 → 191.0; ζ over three words, β → 191.0; column batching γ_s, γ_b (6 variables) → 189.4; τ (`n/ |
K | `) → 188.1 | proven | the local and successor claims of three words reduced to one point; the last row's successor is the boundary row (nox b_out, circuit b_v = its own row 0) |
| fresh-word binding (words a, b, c) | OOD (WHIR Lemma 4.25) | s = 1 → 155.5 |
proven | word a's OOD points come from its root alone (tag PRE) and its answers enter the chain before (α, β) |
s |
as the machine row |
deferred claims (constraints G, nox publics P̄_nox, circuit key P̄_V) |
Schwartz–Zippel on the line polynomial | `deg/ | K | ` per fold: 32 → 187.0; 52 → 186.3; 22 → 187.5 | proven | if either claim on the line is false the sent polynomial differs from G∘L (degree ≤ deg) and agrees at r with probability ≤ deg/ |
public-column batching γ_n, γ_v |
Schwartz–Zippel (multilinear in the column index) | `log₂(cols)/ | K | ` → 189.2 | proven | drawn after the publics are absorbed |
circuit memory (logUp over (address, value)) |
Haböck eprint 2022/1530 Lemma 5; fingerprint injectivity | α_V: `T/ |
K | , T = 17·2^15→ 172.9;β_V: T²/(2 |
K | )` → 154.8 |
| recursion circuit = the step verifier | the circuit's constraints force exactly the native verifier's computation | — | tested, not proven: the circuit builder and the native interpreter run one program and agree; every row constraint holds on honest runs; every phase-1 and phase-2 cell of an honest run is pinned by a constraint or by memory unless free by design (unused operands, scratch columns, padding); non-canonical and non-boolean decompositions refused; failed assertions refused; the base step's assertions off only with live = 0; the final verifier reads a state only if its base items are base (state::is_canonical), the condition under which the native state digest equals the circuit's (audit/recursion-review-2026-10.md F1) |
recursion::circuit::tests, recursion::review, tests/recursion.rs |
||
accumulation step, m = 4, J = 64 |
as the accumulation row | batch 177.8, sumcheck 182.8, combine 128.0 (22 grinding bits), OOD 155.5, spot 128.0 (24 grinding bits) | proven (as the accumulation row) | AccConfig::terms(4, 64) |
t, grinding |
recursion::params::tests |
decider (recursion::decide: one field-native batched WHIR opening of the last accumulator and the circuit key's two words under one tree, ℓ = 21) |
the field-native WHIR row; the key words are exact codewords fixed by the parameters | batch γ 177.9, sumcheck 182.8, combine 128.6 (grinding priced in), WHIR terms ≥ 128.0 (fold 128.4, shift 128.0, fin 130.7) | proven (WHIR row; batch: lens whir::batch) |
the deferred key claim splits as (1 − g_6)·K̃_lo + g_6·K̃_hi, both values sent and checked on the line |
WHIR parameters | recursion::params::tests, tests/recursion.rs |
| IVC composition | every row above; hemera as a random oracle also inside the circuit (step i recomputes step i − 1's transcript) |
per round ≥ 128 (non-interactive: Q·2^-128 per proof plus hemera collisions, if recursive Fiat–Shamir is sound) |
conjectured: knowledge soundness of a recursively composed Fiat–Shamir argument whose random oracle is evaluated in the relation has no proof in the random-oracle model (the standard heuristic of every deployed recursive system); the per-step reductions are proven | a final state is accepted only if it is a successor of the initial state through S verified steps: the step counter, the chain of pre-committed roots and the context are checked; a base step after the first restarts the counter |
— | tests/recursion.rs |
field-native WHIR and wrap (recursion::whir, recursion::wrap; envelope profile 6)
Every number below is printed and checked ≥ 128 by
recursion::wrap::tests::every_ledger_row_of_the_wrap_profiles_reaches_128_bits
(inner 1/16 with 16 grinding bits, inner 1/64 and 1/256 with 24, inner
1/128 with 22, final 1/256 with 30 and 1/512 with 24 and 26), by
recursion::wrap::review::the_shipped_wrap_levels_reach_128_bits_and_their_interactive_rows_are_stated
(the shipped chain wrap::SHIPPED = 4i:16,7i:22,9f:26, measured in
audit/wrap-fastverify-2026-10.md and audit/ivc-speed-2026-10.md:
inner 1/16 with 16 grinding bits (2^16 rows), inner 1/128 with 22 (2^15),
final 1/512 with 26 (2^14) — weakest rows 128.09 / 128.24 / 128.40) and by
examples/wrap_bench for the derived keys. Every field-native schedule
keeps lens's queries per round and re-chooses per round the Johnson
regime, OOD count and fold/query grinding for the least grinding work
(recursion::whir::schedule; each term recomputed by lens's ledger,
tests/ivc_speed_review.rs): the final level grinds fold 22/22/22 and
query 24/24/27 (was 17/20/25 and 26/26/26), level 1's combination 21
(was 26). The ≥ 128 figures price grinding as hemera work:
interactively (every grinding removed — fold, query and combination
challenges) the weakest rounds carry 110.23 / 104.24 / 101.89 bits
(the final level's fin after its 27-bit query grinding — the
queries 24/18/14 keep the proof ≤ 64,213 B over every transcript), so
the non-interactive bound Q·2^-128 assumes a prover's Q counts every
grinding permutation. The previous chain (6i,8i,8f:30,
audit/wrap-2026-10.md) carried 98.02 interactively at its final level.
| component | assumption | bits claimed | status | argument | controlling parameter | test |
|---|---|---|---|---|---|---|
field-native WHIR (recursion::whir) |
as lens's WHIR row (Johnson-regime MCA, BCGM eprint 2025/2051); the field-native words row | min over lens's WHIR terms at (whir, ℓ) and the batch's (lens whir::batch): claims γ ` |
Λ | (J−1)/ | K | , sumcheck 2 |
wrap zerocheck (recursion::wrap) |
Schwartz–Zippel; sumcheck on the one codeword each fresh word is OOD-bound to | μ powers over 267 (inner) / 249 (final) constraints → 183.9; τ `n/ |
K | → 188.2; per round10/ |
K | ` → 188.7 |
| wrap fresh-word binding | OOD (WHIR Lemma 4.25) | s = 1 → ≥ 150.7 |
proven | every committed word answers its OOD samples right after its root | s |
as above |
inner wrap memory (logUp over (address, value)) |
as the circuit memory row | α_V `T/ |
K | , T = 17·2^n→ ≥ 172.9;β_V` → ≥ 154.8 |
proven | as the circuit memory row |
| inner wrap shift reduction and key claim | Schwartz–Zippel | rounds of degree 2 → 191.0; β, ζ → 191.0; column batching (6 variables) → 189.4; γ_k (8 variables) → 189.0 |
proven | as the step's shift row; the key over the base field (recursion::splitkey): the prover sends every physical key column at ρ (each Fp3 column as its three limbs), absorbed before γ_k; the verifier rebuilds the logical columns for G (c = p₀ + T·p₁ + T²·p₂, exact) and checks Σ_p eq(γ_k, p)·P_p(ρ) = Σ_w eq(γ_hi, w)·v_w — a false physical value makes the multilinear difference nonzero, caught but with probability `8/ |
K | — and eachv_w` is opened from the key words (base words under one tree, their root the key's) |
| final wrap linear wiring | Schwartz–Zippel in λ |
`#reads/ | K | → 174.0 at2^18` reads |
proven | every read slot's value minus its write slot's value (linear in the row's phase-1 cells, the key fixed) batched with powers of λ drawn after W1 is bound; a nonzero difference vector makes ⟨u_λ, W1⟩ a nonzero polynomial of degree < #reads |
| final wrap column batching (local, successor) | Schwartz–Zippel (multilinear in the column index) | `6/ | K | ` → 189.4 | proven | the claims on W1 at ρ and its successor become weights of the direct opening; the successor claim covers the columns the constraints read (from the recorded graph); the others are not constrained and not read |
| recursion circuit = the wrapped verifier | as the "recursion circuit = the step verifier" row, for the final verifier, the field-native WHIR verifier and the wrap verifier | — | tested, not proven: the circuit and the native interpreter run one program (finalv, wrap::verify); honest runs satisfy every row; tampered proofs are refused by both |
recursion::whir::tests, tests/wrap.rs |
||
final-level message digests (recursion::msg) |
hemera collision resistance (4-limb digests) | binding as the hash row (2^128 classical) |
conjectured (hash row) | the final level's direct opening absorbs its final polynomial, and the final wrap absorbs its column values at ρ and their successors, as one digest: eight part sponges (tag MSG) and a sponge over the message's length and the parts' digests (the length fixes every part's size; a part zero-pads its last block, so without the length m ‖ 0 and m collide — zheng #58 review); the length is also the key's (check_shape, the parser); a second message with the same digest is a hemera collision, so the transcript binds the message as if absorbed whole (Fiat–Shamir over a collision-resistant message hash) |
— | recursion::msg::tests, wrap::fastverify_review::message_digests_bind_length_order_and_content, tests/wrap.rs |
| wrap composition | every row above; hemera as a random oracle inside the circuit (a level recomputes the transcript of the level below) | per round ≥ 128 (non-interactive: Q·2^-128 per proof plus hemera collisions, if recursive Fiat–Shamir is sound) |
conjectured — the IVC composition row's heuristic, one level per wrap | the outermost proof's public input binds the statement's context, chain, segment count, run challenges, constants and the deferred nox-public claim the verifier evaluates itself | — | tests/wrap.rs |
informational
| component | assumption | bits | status | argument | controlling parameter | test |
|---|---|---|---|---|---|---|
| the Spartan IOP over Goldilocks challenges | as the Fp3 row | 227 / 2^64 = 2^-56.2 at m = n = 2^20 |
proven, and too small for a 128-bit claim: no profile uses it | as the Fp3 row | — | spartan::iop::tests::goldilocks_iop_agrees_with_the_same_relation |
retired
| component | status |
|---|---|
legacy folded trace API (commit, open, verify_eval, verify, fold, decide, ccs, folding, phi; feature legacy, off by default) |
retired — unsound: the fold is unchecked, the statement is unbound and the constant wire is free (specs/decider.md §soundness; retired_path_hole_* tests pass because the path is broken); Brakedown's code distance is unproven (lens#6) |
direct proofs: public v2 (verify_execution), state v1 (StateStatement::verify_v1) |
retired — read for one release (JOYEXEC2, JOYST001). acceptance rests on the exact check of the complete table that PublicTensor authenticates under a hemera Merkle root (hash row); their Spartan transcript uses the earlier challenge rule (Transcript::new_v1, Goldilocks, 2^-56 at the sizes above) and is a consistency check only |