Constant-size proofs + stateless verification (v0.3.0)#50
Open
adamkrellenstein wants to merge 11 commits into
Open
Constant-size proofs + stateless verification (v0.3.0)#50adamkrellenstein wants to merge 11 commits into
adamkrellenstein wants to merge 11 commits into
Conversation
Merging this PR will not alter performance
Comparing Footnotes
|
wilfreddenton
approved these changes
Jun 18, 2026
This was referenced Jun 18, 2026
Closed
…file-merkle-path); fixes Component + Monolithic matrix Errors
Carries the issue #46 soundness fix into the constant-size circuit. The Merkle path-selection indices were derived with non-strict `to_bits_le`, which only enforces Σ bitᵢ·2ⁱ ≡ x (mod p), not canonicity. Since the Pallas modulus is just above 2^254 (NUM_BITS=255, p ≡ 1 mod 2^32), a prover can witness the (x + p) decomposition whose low bits encode index+1 and open a leaf other than the challenged one (file tree) or steer the aggregation path off the public index. Switches the four index-derivation sites — challenge_with_idx and ledger_index_public in both synth.rs and formal_components.rs — to to_bits_le_strict. Completeness preserved; the idx+1 opening is closed. Verified: build + api_functionality, depth_zero_cheat_regression, security_malicious_prover, security_ledger all pass.
…e-identical to aggregate_root; removal out of scope)
Unify the constant-size proof work (wire v3: Proof carries only
compressed_snark + ledger_root + aggregated_tree_depth) with stateless
verification on one model.
- plan.rs: make_plan takes AggInputs; per-file ledger indices are always
resolved from a LedgerView (live FileLedger or stateless registry), never
read from the proof. AggInputs::Proof drops ledger_indices.
- verify.rs: LedgerView trait + registry-backed StatelessLedger
{valid_roots, files: file_id -> (slot, rc)} + verify_stateless, sharing
verify_with. The challenge_ids equality check is removed: public inputs
are rebuilt from the supplied challenges, so a mismatched proof fails the
SNARK regardless.
- ledger.rs: aggregate_root / aggregate_root_from_files take (rc, slot)
pairs and mirror rebuild_tree (append-only slots, zero-filled gaps,
sparsity guard, power-of-two padding), byte-identical to FileLedger::root.
Bump to 0.3.0 (breaking wire + API). Full suite green (294 passed);
stateless verify matches ledger verify for single- and multi-file proofs.
Crypto/incremental root perf
b83944f to
137bb9e
Compare
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
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.
Reconciles the two open PoR PRs — #44 (constant-size proof) and #49 (stateless verify) — into one coherent model. Supersedes both.
Why one PR
#44 and #49 branched independently off
mainand conflicted at the design level, not just textually: #44 makes the proof constant-size by droppingchallenge_ids/ledger_indicesand moves the ledger to stable append-only slots; #49 (written against the old format) still read those fields and assumed lexicographic ordering. Those index models are mutually exclusive, so this lands them together.The reconciled model
Proofis constant-size (wire v3):{compressed_snark, ledger_root, aggregated_tree_depth}. The challenge set is supplied out-of-band; the proof carries no per-file data, so its size is independent of challenge/file count.plan.rs:make_plantakesAggInputs; per-file ledger indices are resolved from aLedgerViewon both prove and verify paths (never read from the proof).AggInputs::Proofcarries only root + depth.verify.rs:LedgerViewtrait + registry-backedStatelessLedger { valid_roots, files: file_id → (slot, rc) }+verify_stateless, sharingverify_withwith the ledger path.ledger.rs:aggregate_root/aggregate_root_from_filestake(rc, slot)/(root, depth, slot)and mirrorrebuild_treeexactly (append-only slots, zero-filled gaps, sparsity guard, power-of-two padding) — byte-identical toFileLedger::root.Design decisions
challenge_idsequality check (from Add stateless PoR verification (verify_stateless + aggregate_root) #49). Safe: the verifier rebuilds every SNARK public input from the supplied challenges (incl.block_height/prover_id/num_challengesviaChallenge::id()→initial_state), so a mismatched proof fails SNARK verification regardless. Confirmed by the audit below.StatelessLedgerholdsfile_id → (slot, rc)(not just valid roots) so a contract keeping its file registry on-chain can resolve indices exactly as the live ledger does — enabling the host to drop its mutable in-memoryFileLedgerlater.Verification
security_ledger,security_malicious_prover,stateless_verify). Newstateless_verify.rsasserts stateless verify ≡ ledger verify (single + multi-file) andaggregate_root≡FileLedger::root(incl. sparse slots).aggregate_root, and single-file attack classes. One doc-hardening note added toStatelessLedger.cargo auditpassed (pre-push hook).Supersedes
Note
High Risk
Changes proof serialization, ledger index semantics, and verification public-input construction in a security-critical PoR/SNARK stack; incorrect registry or root handling could break binding or cross-block validity.
Overview
Breaking release (0.3.0) that unifies constant-size proofs and stateless verification around append-only ledger slots instead of lexicographic ordering.
Proof wire format v3 drops serialized
challenge_idsandledger_indices; proofs carry onlycompressed_snark,ledger_root, andaggregated_tree_depth. Verifiers must supply the exactChallengeset out-of-band; binding comes from canonical challenge ordering,initial_state, and SNARK public inputs—not from fields inside the proof bytes.Prove/verify planning uses
Plan::make_plan(challenges, AggInputs)so aggregation root/depth come from the live ledger (prove) or the proof (verify), while per-file ledger indices are always resolved viaLedgerViewon both paths. Newverify_stateless+StatelessLedger(valid_roots+file_id → (slot, rc)) shareverify_withwith the liveFileLedgerpath.FileLedgerassigns stable indices onadd_file;add_filesrequires explicitledger_indexfor reconstruction and rejects duplicatefile_ids. The aggregated tree is built by slot (zero-filled gaps, sparsity cap). Helpersaggregate_root,aggregate_root_from_files, and incrementalLedgerFrontiermatchFileLedger::rootfor on-chain-style registries. Ledger persistence bumps to format v2.Circuit hardening (#46): Merkle path selection uses
to_bits_le_strictfor challenge and ledger-index decompositions.Docs/tests/Picus constraint counts updated for the new model;
PorSystem::verifyno longer comparesproof.challenge_idsto caller challenges.Reviewed by Cursor Bugbot for commit 137bb9e. Bugbot is set up for automated code reviews on this repo. Configure here.
Closes #46 (strict bit-decomposition on both index sites).
Issue #19 (incremental tree-update) is addressed by the LedgerFrontier added here.