Repository navigation
Bind every PCS opening to an immutable commitment-time anchor - #600
Open
kevaundray wants to merge 42 commits into
Open
kevaundray wants to merge 42 commits into
kevaundray wants to merge 42 commits into
Conversation
# Conflicts: # crates/leanvm_core/src/cpu/reduce.rs # crates/pcs/src/stack_open/mod.rs
# Conflicts: # README.md
# Conflicts: # crates/fiat_shamir/src/lib.rs # crates/fiat_shamir/src/transcript.rs # crates/leanvm_core/src/cpu/program.rs # crates/leanvm_core/src/cpu/proof.rs # crates/leanvm_core/src/rec/transcript.rs # crates/leanvm_core/src/rec/tree/design.rs # crates/leanvm_core/src/rec/tree/mod.rs # doc/leanvm/body/08-end-to-end-protocol.tex # doc/leanvm/body/e-recursion.tex
Exact counts
|
Benchmarks: base against this PR, on one runnerc5acc61 merged into its base, against the base 37c1525: 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; BLAKE2s
Prover stages
Fibonacci
Prover stages
Flock
PCS
leanSPHINCS
Prover stages
leanXMSS
Prover stages
Every resultBLAKE2s
Prover stages
Fibonacci
Prover stages
Field and transpose kernels
Flock
PCS
leanSPHINCS
Prover stages
leanXMSS
Prover stages
|
…aeneas-current-20261010 # Conflicts: # crates/fiat_shamir/src/merkle.rs
# Conflicts: # crates/pcs/src/stack.rs
…eanVM into kw/whir-anchor-20261010
This was referenced Oct 11, 2026
…t into anchored PCS
…pening Flock's reductions now follow the completed commitment record in both verifiers and provers; the bus, tables and opening follow. Bump to LVMP 18, LVMT 20 and leanvm-tree-17, above upstream's.
…de APIs) into the anchored PCS opening Hiding commitments, the zero-knowledge stack's and the key commitment's, stay unanchored: an anchor's value would publish one more evaluation of the hidden witness. The anchored receivers refuse a padding configuration, the hiding ones a plain configuration, and weighted openings are refused on anchored commitments. LVMZ moves to 2 since its session names the program digest.
…dant clone in the anchoring test
This branch has not been deployed
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
1 participant
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.
Summary
Bind every public PCS opening to a complete immutable commitment record: Merkle root, public shape, exact original logical duplex context, the commitment-time extension-field point and its advertised MLE value. The original commitment binds whir-anchor-v1, shape and occupied lanes before its root and anchor draw. The point is derived once, not transmitted or resampled.
The normal merge 15a733d integrates upstream riscv-exploration at 37c1525: zero-knowledge leaves (#619 to #624: one-time-padded transcript messages, the hiding PCS commitment and opening, the zk outer proof, ZK leaf proofs and aggregation trees over ZK leaves), flock bit-pass tasks (#631), and the module layout and API cleanup of #633 and #634. The anchored record now lives on the new layout:
pcs::whir::commitbuilds the anchored record over upstream'sBaseCommitment,pcs::stack::{CommittedStack, StackCommitment, Statement}carry it (StackWeightinstack/weight.rsadds the occupied-prefix anchor),leanvm_core/src/commitment.rsreads it, and the WHIR verifier is upstream's, with this branch'scheck_config_shapeguard,WeightAtterminal weight and named verifier stages. c5acc61 is a clippy-only follow-up. The earlier normal merge cdb3423 integrated upstream at dfb7570, #630's reordering: the commitment, then flock's reductions, the bus, the table sumcheck and the opening, in the CPU prover and verifier and in the recursion machine's prover andTableArgument::verify_core, which every node circuit runs. Flock's reductions now follow the completed anchored commitment record (marker, shape, raw root, anchor point and value), and the bus and table challenges follow flock's messages; every opening still checks its whir-opening-v1 frame against that unchanged record before gamma, the ring map and lambda, with flock's ring-switched claims among the claims it binds. The pinned test offsets that locate flock's first message start past the complete record. The earlier normal merges bbeb1ba and 39ec6aa integrated upstream at 392e187, including program-owned signer sets (#611, #612, #615), claim sets and their union in rows (#613), claim-set trees (#614), height tiers (#618), the union binding fix (#626), lone children and absent places at claim-set nodes (#627) and the stacked-opening lint (#609). The earlier merge 75d4562 of #607's spongefish-style transcript and #608's claim-width checks, and the merges of #599's typed PCS rewrite, #555's scalar/batched Merkle hashing, #604's aligned AVX-512 loads and Aeneas preparation 7de1b28 remain intact. The public entry points are pcs::stack::CommittedStack, StackCommitment and Statement. WHIR kernels and dense-weight interfaces remain crate-private, not public root-only bypasses.The #607 migration preserves session-IV derivation, public-instance absorption, raw-byte root messages, codec/session APIs, zero-work no-op and positive-work nonce framing, hint framing and squeezed final digests. Native and constrained Rows use identical anchor framing. The commitment header is four F192 messages and one raw 32-byte root. An opening checks its whir-opening-v1 frame after metadata/configuration/statement/point guards and before gamma, the ring map and lambda. Its root and original context CV are raw 32-byte messages, not the historical two-scalar encodings. The remaining fields retain their order: shape, pending-byte count/first/previous, current squeeze cursor, normalized pending words, original point and value. The frame is 6 + log_n + ceil(pending_bytes / 24) F192 messages plus 64 raw bytes. Pending words use canonical zero padding in the final partial word and scalar.
Context capture does not flush, hash, sample, allocate or emit recursion rows. Cached output is excluded only because it is derivable for valid privately constructed duplex states; there is no arbitrary restore API. Openings can retain the original record across genuinely separate sessions. Anchor weights are restricted to occupied lanes, including non-power-of-two prefixes and omitted zero-tail lanes.
Every tree circuit reads each child's commitment through the same anchored record and verifies its opening in the same framing as the native verifier: first-level nodes, nodes of a tree of outputs, claim-set nodes of either tier (absent places included) and the wrap of a large proof. The pinned
leanvm-tree-12session tags in the tree and claim-set layout tests were refreshed for this branch's program digest domain; that domain is unchanged by the merge of dfb7570, so they still pass as pinned, with unchanged heights and statement layouts.Zero-knowledge leaves: hiding commitments are not anchored
This branch refuses anchoring for hiding commitments rather than covering them. A plain commitment publishes its anchor value, the stack's multilinear extension at a point drawn right after the root. On the hiding commitment of #621 that value would be one more evaluation of the hidden witness, which the PCS annex's zero-knowledge argument (
sec:pcs-zk: padding ofq_0 + 2coefficients per lane, the uniform group reserved for the lane fold) does not account for; sending it under a one-time pad is impossible for the zk key commitment, whose keys are the pads. So both hiding commitments, the ZK stack's and the key commitment's, keep upstream's root-only commitment and opening, and a zero-knowledge proof's core, its outer proof and the rows of a tree over ZK leaves run upstream's unanchored protocol unchanged:CommittedStack::new(ps, ..)(anchored) asserts a configuration without padding;CommittedStack::new_hidingstays root-only.StackCommitment::receiverefuses a padding configuration and the newStackCommitment::hiding(root, ..)refuses a plain one, both withWhirError::Anchoring;leanvm'sCommitment::readpicks by the announced shape'shidingflag.open_weighted,verify_weighted), which only the key commitment takes, are refused on anchored commitments.Recorderforwards the new verifier methods (context,zero_k,ensure_root_eq,begin_scope,end_scope) and implementsPublicMlefor any inner verifier that does.Annex B gains a "No anchor" paragraph in
sec:pcs-zk; Annex F and section 8 say the ZK stack's commitment carries no anchor.Reserved protocol identities
CPU envelope LVMP 18, zero-knowledge envelope LVMZ 2, tree envelope LVMT 20, program digest domain leanvm-rv64im-14, tree transcript domain leanvm-tree-17. Version checks compare only with upstream riscv-exploration at 37c1525. These identities are above upstream's LVMP 17, LVMZ 1, LVMT 19, rv64im-13 and tree-16 respectively. LVMZ moves because a zero-knowledge proof's session names the program digest, whose domain this branch changes; its wire format is otherwise upstream's. The CPU session tags are upstream's (
v2, andv1for zero knowledge), and the claim-union and reduction tags are unchanged. Legacy and foreign envelopes reject before interpreting their bodies.Security and correspondence boundary
Proof PR #551's checked anchor mathematics covers the ideal interactive model: a root-fixed supported list precedes a fresh uniform extension-field point, and arbitrary advertised values select at most one candidate outside a separately bounded ambiguity event. The 2^-124 anchor ambiguity term is not a whole-protocol security level.
PR #551's existing DuplexRefinement/Framing/WHIRNativeSecurity chain models the historical pre-#607 #552 transcript, with the #552 byte-identity audit pinned to its historical commit. Its corrected adaptive ideal-compression coupling loss is min(1,(2Q^2-Q)/2^256). Its conditional 2^-42 endpoint concerns the modeled historical unanchored event under explicit experiment/resource premises. It does not currently apply to #607's session-IV, raw-byte roots, new proof-of-work or squeezed digest, or to this branch's new anchor frames. The source adapter and anchored Fiat-Shamir composition are open proof gaps. The completed original-statement reset extractor is interactive only, with exact joint failure 1/2^50 + 2^-s and checked round/attempt/resource bounds; it is not a Fiat-Shamir knowledge theorem.
No whole-system 128-bit security level, complete deployed knowledge-soundness theorem, unconditional BLAKE2s security or universal Rust-to-Lean equivalence is claimed. Aeneas extraction is a separate source-pinned project. The ordinary full-public-view replacement shortcut for deterministic BLAKE2s cannot justify a small loss when efficient known-answer observers are allowed.
The complete caller statement must be fixed before opening gamma/lambda: values must already be observed or public and seeded; coordinates must be public constants or earlier verifier challenges; addressing and shape must follow that bound layout. Record identity binding does not bind arbitrary external claims. The production CPU and recursion callers retain their earlier Flock/bus/table observations and seeded layouts. #609's
disallowed-methodslint onCommittedStack::openandStackCommitment::verifyapplies here too: the anchoredCommitment::verifykeeps its expectation, and this branch's test callers with fixed public statements carry one.Exercised verification
On c5acc61 (the clippy-only follow-up of the merge 15a733d): Rust 1.99 formatting check; complete-workspace all-target release Clippy under Rust 1.97 and 1.99 with the haswell pin, Rust 1.99 native, the Rust 1.99 AVX-512 leg, AVX2 with VPCLMULQDQ and with GFNI/AES, the system-allocator CLI leg and the ARM64 neoverse-n2 cross leg (compiled, not executed); release rustdoc. On 15a733d: the complete Rust 1.97 release workspace suite with four test threads (536 tests). A separate public API caller built in release proved, serialized, decoded and verified CPU LVMP18 proofs, first-level and node LVMT20 proofs of a tree of outputs, a two-tier claim-set tree (small first levels, a large node, a wrapped large child under a large node and under a narrowing small node), zero-knowledge LVMZ2 proofs and a first-level LVMT20 proof over zero-knowledge leaves. It rejected every legacy CPU, zero-knowledge and tree envelope version, foreign envelopes, foreign programs and tree shapes, wrong outputs, wrong claim sets and truncation. New unit tests cover the refusals between anchored and hiding commitments and the anchor in the stack weight's fill and lane folds alongside an unanchored weight.
CI completed for c5acc61, on GitHub's merge with upstream 37c1525. Counts is the sole failing check, as detailed below. Every other non-skipped check passed, including Test, MSRV, Rustdoc, Rustfmt, Clippy on x86-64, ARM64 and RISC-V guests, Miri, the AVX2/GFNI, AVX2/VPCLMULQDQ and NEON jobs, ACT4, check-pdf, Cargo deny, unused dependencies, the Android and iOS release builds, the mobile benchmark source validation and the benchmark jobs. The workflow's build-pdf check was skipped.
Counts
The gate and baseline are unchanged. The completed Counts run compares c5acc61 with upstream at 37c1525 and fails on exactly these four row increases, the same rows as before the merge:
Every other program's cycles, proven rows and committed words equal the base's. The added work checks the immutable commitment record and evaluates the supported anchor weights inside the recursion verifier. A bounded duplicate-work review found each frame field checked once against its distinct expected record field; removing those comparisons would weaken identity binding. No reduction was landed merely to satisfy the gate. These measurements do not increase proven rows or committed words, so the added rows fit the existing padded tables. The row gate failure is expected for the added protocol work; cost acceptance remains a review decision.