Repository navigation
zk: zero-knowledge leaf proofs by composition (draft) - #532
Closed
kevaundray wants to merge 16 commits into
Closed
kevaundray wants to merge 16 commits into
kevaundray wants to merge 16 commits into
Conversation
An opt-in zk mode for RISC-V leaf proofs, by composition. - Stage 0: a zero-knowledge proof travels as LVMZ version 15 with its own transcript seed; the prover draws its randomness from ChaCha20 seeded by the OS or a test; Prover::zk and the CLI's --zk. Plain proofs are unchanged. - Stage 1: the hiding stacked WHIR: lanes padded past their power of two (one butterfly layer folded into the encode's first pass, the padding factor shifted so it vanishes nowhere on the domain), one uniform lane, the revealed claim after the lane fold and the padding's fold, the level-0 correction, a query table rederived for the padded code; Annex B describes it. - Stages 2 and 3: every scalar the plain protocol sends until its opening's lane fold ends travels under a one-time pad from a separate key commitment; the verifier runs its own code over a recording arithmetic whose canonical constraints a natively zero-knowledge Spartan over E proves (eq-weighted Libra mask, two dummy constraints); the final clock's free bits are hidden scalars constrained to be bits; the deferred claims become linear constraints. leanXMSS 400 at rate 1/4, single local runs at load about 5: proof 240.6 KiB plain, 350.3 KiB zk; proving 0.486 s and 0.511 s; verifying 3.5 ms and 12.0 ms. Not yet: the Python verifier's zk mode, the spec of the composition, zk variants of the integration tests, the tracked bench case.
Benchmarks: base against this PR, on one runnerf0322a9 merged into its base, against the base 5735b01: each benchmark run in turns on one runner, base and PR 5 times each. A size is shown when it changed; a time or a peak memory when it moved the same way in every round and its median by at least 1% (the change is the median ratio, with the rounds' range). Threads shows the named configuration; BLAKE2sProver stages
Flock
PCS
leanSPHINCSProver stages
leanXMSS
Prover stages
Every resultBLAKE2s
Prover stages
Fibonacci
Prover stages
Field and transpose kernels
Flock
PCS
leanSPHINCS
Prover stages
leanXMSS
Prover stages
|
Collaborator
Author
|
Haven't reviewed the agents work yet, leaving in draft |
Re-applies the zero-knowledge leaf proofs onto the BLAKE2s duplex transcript and upstream's encapsulated commitments: the hiding commitment and opening ride Committed and Commitment, chosen by the stack's random lane, and the NTT's padding rides upstream's reworked encode.
The Python verifier is gone upstream (leanEthereum#537) and its zero-knowledge mirror was never started, so nothing reads Program::zk_constraints.
Hiding carried the padding length beside the configuration that fixes it, and every caller passed config.padding(); the verifier's check of the two against each other and its error variant go with it. The transcript is unchanged.
SpartanError had one variant, the transcript's error, which the caller unwrapped back into it.
The specification has the hiding commitment (Annex B, sec:pcs-zk) but no sec:zk; the composition is described in the cpu::zk module docs.
…o-knowledge case No tracked benchmark proves in zero knowledge.
Only the commitment pads an encode, always in place; its test checks every plan against direct evaluation.
announced_hiding repeated announced around one step; a flag picks the stack instead, and the size check returns to upstream's form.
new_hiding only asserted the random lane before new_padded, whose padding-length check already ties the pads to the stack's configuration.
Announcement::write writes the shape through write_shape, then the final clock: the same scalars in the same order. The docs the zero-knowledge work added wrapped prose by hand, which the repository does not.
Clippy 1.99 refuses chunks_exact with a constant size.
Re-applies the hiding WHIR onto the pcs overhaul: CommittedStack::new_padded and a hiding configuration's Config::padding pick the hiding opening; the padding's share of level 0's queries is QueryBatch::padding_correction, its shift padding_shift over Normalizers; the NTT padding rides the merged ntt.rs. The key commitment's opening goes through whir::open_hiding and verify_hiding, over the dense weight the tests already used, now DenseWeight.
Rustdoc refused links to the plain commit, which is test-only now.
tcoratger
reviewed
Oct 11, 2026
Collaborator
There was a problem hiding this comment.
I've checked with the agent and I think some stuffs are missing to have full ZK like here my understanding is that the ZK is only for the leaves and also I think that ZK proofs are somehow leaking witness. I'm preparing a plan with Claude and I'll push a series of granular PRs to include full ZK in a gradual manner with you as an author for the credit so that we can have maybe a more complete review of each small PR and merge the whole stack at the end.
| \begin{itemize}[itemsep=1pt,topsep=2pt] | ||
| \item \emph{Level-$0$ answers.} For distinct $x_1, \dots, x_t \in \dom_0$ with $t \le \npad$, the map $\padc \mapsto \bigl(\Wn{\kappa}(x_i + \padshift) \sum_{j < \npad} \padc[j] \novel_j(x_i)\bigr)_i$ is onto $\K^t$: the $\novel_j$, $j < \npad$, span the polynomials of degree below $\npad$, which take any $t \le \npad$ values at $t$ points, and every factor is nonzero. So any $\npad$ symbols of a padded row are uniform whatever its message, the $(\nq_0 + 1)$-wise independence of the padded code~\cite{DHRR26,Dia25}, and a query message opens at most $\nq_0$ distinct columns. | ||
| \item \emph{Roots.} Given the opened columns, one more symbol of each row is still uniform ($\nq_0 + 1 \le \npad$), so each unopened leaf keeps one spare uniform symbol of $\K$ per row, $64$ bits of fresh entropy, and the root and the authentication paths are simulated in the random-oracle model with no salt. | ||
| \item \emph{After the lane fold.} No claim touches $\rlane$, so the lane fold gives $f^{(1)} = \sum_{u} \eq(\fc, u)\, f(u, \cdot)$ the term $\eq(\fc, \rlane)\, f(\rlane, \cdot)$, a nonzero multiple in $\E$ of a uniform vector of $\K^{2^\kappa}$ unless some $\fc_j$ is $0$ or $1$, which has probability at most $2\ell_0/|\E|$. Every later message is a linear functional of $f^{(1)}$, or for a root a random-oracle hash of the encoding of a fold of it: $c'$, the round and intro polynomials, the OOD answers, the values $c_q$, the opened rows of the levels past $0$, and $\ffinal$. An $\E$-valued functional is three $\K$-linear functionals of $f(\rlane, \cdot)$, and the configurations keep their number at most $2^{\kappa - 1}$, three per $\E$ scalar revealed, which is what fixes $\kappa \ge 14$; under that condition the random row makes them uniform, as VEIL's random column does~\cite[Lemma~4.7]{DHRR26}. The opened level-$0$ columns and $\padfold$ together determine the $c_q$, and reveal nothing more of the messages. This last step adapts VEIL's lemma to an $\E$-fold of $\K$-valued rows, with a random row of $\K$ and fold coefficients in $\E$: it is argued here, not proven. |
Collaborator
There was a problem hiding this comment.
I think this step breaks: a functional with coefficients in K (like c_q at level 0, or any opened symbol at level 1, whose twiddles are in K) only sees the random row along the line eq(r, R)·K, so dividing by eq(r, R) gives the verifier two K coordinates that depend only on the witness. I checked it with commit_hiding and ligero_commit_ext and it reproduces.
| let shape = w.layout.shape; | ||
| let committed = info_span!("Commit").in_scope(|| { | ||
| let lane = 1usize << (shape.mu - LOG_BATCH); | ||
| rng.fill_k(Purpose::RandomLane, &mut w.q[shape.n_lanes * lane..]); |
Collaborator
There was a problem hiding this comment.
With 4 uniform lanes instead of 1, their eq weights span E over K (with probability about 1 - 2^-128), so the folded vector becomes uniform in E^N and VEIL's lemma applies directly.
| \paragraph{Zero knowledge.} The argument is for an honest verifier and statistical, then Fiat-Shamir in the random-oracle model. Every scalar sent before the lane fold's end is uniform, each under its own key. What the opening reveals besides is simulated in three parts. | ||
| \begin{itemize}[itemsep=1pt,topsep=2pt] | ||
| \item \emph{Level-$0$ answers.} For distinct $x_1, \dots, x_t \in \dom_0$ with $t \le \npad$, the map $\padc \mapsto \bigl(\Wn{\kappa}(x_i + \padshift) \sum_{j < \npad} \padc[j] \novel_j(x_i)\bigr)_i$ is onto $\K^t$: the $\novel_j$, $j < \npad$, span the polynomials of degree below $\npad$, which take any $t \le \npad$ values at $t$ points, and every factor is nonzero. So any $\npad$ symbols of a padded row are uniform whatever its message, the $(\nq_0 + 1)$-wise independence of the padded code~\cite{DHRR26,Dia25}, and a query message opens at most $\nq_0$ distinct columns. | ||
| \item \emph{Roots.} Given the opened columns, one more symbol of each row is still uniform ($\nq_0 + 1 \le \npad$), so each unopened leaf keeps one spare uniform symbol of $\K$ per row, $64$ bits of fresh entropy, and the root and the authentication paths are simulated in the random-oracle model with no salt. |
Collaborator
There was a problem hiding this comment.
Once g_1 is revealed (3k K dimensions of the pads) the spare pad freedom is gone, so I think an unopened leaf only keeps the random lane's 64 bits here, which the 4-lane fix would also cover.
|
|
||
| /// The shared prover/verifier config of a hiding opening of a `K`-witness of `2^log_n` F64 words at L0 inverse-rate logarithm `log_inv_rate`. | ||
| /// | ||
| /// The ladder, grinding and OOD samples of [`config_for_rate`], the query counts of the padded L0 code, and its padding `k = q_0 + 2` ([`Config::padding`]): `q_0 + 1` uniform coefficients make any `q_0` opened symbols of a lane uniform, and one more keeps a uniform symbol in every unopened leaf. |
Collaborator
There was a problem hiding this comment.
Same point as the Roots paragraph: g_1 uses up the extra pad coefficient, so this sentence doesn't hold as stated.
| //! lane 1 uniform words | ||
| //! ``` | ||
| //! | ||
| //! Its opening's claim is public and its weight vanishes on lane 1, so the lane fold mixes the uniform lane into everything the opening reveals: it is the one commitment whose opening hides itself. |
Collaborator
There was a problem hiding this comment.
The key commitment has the same single uniform lane, so its level-1 symbols leak linear functionals of the keys; it's only hidden right now because about half the key slots go unused.
| } | ||
| // The residual, and the closing rounds but the last, which the residual answers. | ||
| scalars += (1 << residual) + 2 * residual.saturating_sub(1); | ||
| 3 * scalars |
Collaborator
There was a problem hiding this comment.
This counts 3 dimensions per E scalar but never checks the rank, which is why it passes even with the leak above; a rank check (or a test that two noise draws can't be told apart) would catch it.
| /// A fresh seed from the operating system for every proof. | ||
| Os, | ||
| /// One fixed seed, for reproducible tests: two proofs under one seed share their keys, so never reuse one in production. | ||
| #[doc(hidden)] |
Collaborator
There was a problem hiding this comment.
Small one: the derived Debug prints the seed, and two proofs under one seed share their keys, so it might be worth redacting it.
| }; | ||
| let (a, b, c) = match aux.kind { | ||
| Kind::Product => (row(&aux.a), row(&aux.b), row(&v)), | ||
| Kind::Inverse => (row(&aux.a), row(&v), constant(F192::ONE)), |
Collaborator
There was a problem hiding this comment.
Just noting that this is stricter than the native inv(0) = 0, which is fine for soundness, but an honest run that inverts a hidden zero couldn't be proven.
Collaborator
Author
|
After speaking to my boss @tcoratger , this will be closed |
This was referenced Oct 11, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Zero-knowledge leaf proofs (
zkmode), draftAn opt-in
zkmode for RISC-V leaf proofs, by composition: the plain protocol runs unchanged with every scalar it sends one-time padded under keys committed beforehand, its commitment made hiding, and a small zero-knowledge Spartan overEproves that the padded transcript passes the verifier's checks. Plain proofs are byte-identical to upstream's.Merged with
riscv-explorationat 5735b01: after the BLAKE2s duplex transcript (#552), the Python verifier's removal (#537), the commitment encapsulation (#536) and thepcsoverhaul (#599).What
zkhides, and what it does notProverand in the crate docs). The exact cycle count is not announced: the final clock's free bits are hidden scalars, each constrained to be a bit by the outer proof.Design
LVMZversion 15, its own magic, used by no other open PR. Its duplex is seeded with the domainBLAKE2s("leanvm-rv64im-zk" || 15 || digest)beside the output, so no challenge of one kind of proof is one of the other. Plain proofs keepLVMP15 and every upstream domain; no shared version moves.ProverStatepads each scalar sent whileset_hiddenholds with the next key; the duplex absorbs the padded value, so the BLAKE2s duplex needs no change and the verifier binds exactly the scalars on the wire. Roots are never hidden.Randomness::Os) or a test seed (Randomness::Seed), one stream per purpose. Nothing comes from the transcript.sec:pcs-zk). Each committed lane carriesk = q_0 + 2uniform coefficients past its power of two, folded into the NTT's first pass as one extra butterfly layer. The padding factor isW_m(X + s), nonzero on the whole domain (W_malone vanishes on the first2^mpoints). One uniform lane is committed last, under no claim. After the lane fold the prover reveals the running claim and the padding's foldg_1, and level 0 takes the padding off each query. The query tableWHIR_QUERIES_HIDINGis pinned to the derivation by a test.CommittedStack::new_paddedcommits a hiding stack; a hiding configuration (Config::padding) picks the hiding opening, andQueryBatch::padding_correctiontakes the padding off level 0's queries.2^20words: keys, the outer proof's dummies and Libra mask in lane 0, uniform words in lane 1), whose opening hides itself through its uniform lane. Its weight, the outer proof's linear claims on the keys, is neither a point nor a ring-switched claim, so nostack::Statementstates it:pcs::whir::open_hidingandverify_hidingare the one public WHIR entry point kept for it, over the dense weight (DenseWeight) the WHIR tests already used.zk/sym.rs): the verifier's own code over a third arithmetic. Hidden values are affine forms over the keys; products, inverses and bound values become auxiliary variables the prover sends padded after the transcript; equalities become linear constraints. What it records is canonical (monic operands, BLAKE2s digests, ordered and deduplicated), and the prover replays it on its own transcript.producer_twist_terms,MatrixForm::slice_weights), so they become linear constraints.zk/spartan.rs): one sumcheck with the eq-weighted Libra mask of the Binius64 whitepaper and two dummy constraints masking(a, b, c); its claims are discharged by the key commitment's opening.Arguments, unreviewed parts flagged
(q_0 + 1)-wise independence of the padded code; roots by one uniform symbol per lane per unopened leaf; everything after the lane fold by the random lane (VEIL Lemma 4.7); the outer proof by its mask, dummies and the self-hiding key opening.E-fold ofK-valued lanes is argued, not proven.L0_LIST_BITSstill bounds its lists) and the key commitment's opening. To be written as theorems in the spec.Status
Prover::zk,--zk; hiding WHIR and its Annex B subsection; keys, recording verifier, outer Spartan, key commitment, hidden final clock, hidden deferred claims).--zkis refused for aggregation and for benchmarks), and ZK recursion proofs.Tests
zk::spartan: completeness, unsatisfied witness, tampered rounds and openings, fresh masks share no scalar.pcs: padded encode against direct evaluation, hiding opening verifies, tampered claim andg_1refused, wrong pads refused, determinism, hiding table equals the derivation, revealed dimensions at most half a lane, list bound.cpu::zk: a ZK proof verifies, round-trips its bytes, is refused as a plain proof, is a function of its seed, other seeds share no revealed scalar past the announcement; tampered scalars across the stream, the outer proof and the key opening are refused without panic.