Repository navigation
verification: the Rust WHIR verifier refines the Lean model, via Aeneas - #632
Draft
kevaundray wants to merge 115 commits into
Draft
kevaundray wants to merge 115 commits into
kevaundray wants to merge 115 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
…aeneas-current-20261010 # Conflicts: # crates/fiat_shamir/src/merkle.rs
…verify_eq_native and authenticated_native
…tion; relational transcript interface
…Model discharged for injective encode; committed table shapes
…s, source changes and tool patches
…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
…d module layout (PR 600, 15a733d) into the WHIR extraction Conflicts resolved on upstream's layout and names, keeping its behaviour and the extraction repairs: - fiat_shamir arith: Verifier::read_round sums the tail in an index loop; verifier: upstream's Hints reader. - pcs verifier: open_rows_native stays a free function over Openings::rows; merkle: the octopus rebuild, expansion, path lookups and hint decoding stay index-loop helpers, Openings::rows in an index loop. - ring_switch: the family loops stay helpers over slices and PrefixGroup names points by index, with upstream's crate visibility. - stack: spans_region, add_point_weights and add_point_targets on the optional anchor; WeightAt names its element type. - whir query: Stratum::batch and sample_queries in index loops (push_group, push_chunks). - whir verify: upstream's structure (RoundQuad, NovelBasis, hiding reveal and padding share) with the replay holding no configuration borrow, the query closure split into begin_query and finish_query, explicit out-of-domain and sum loops, and the literal grinding panic.
…aeneas-current-20261010
… the round quadratic read; OOD batching generic over Arith The verifier now reaches upstream's Hints::next, NovelBasis::new and normalized_at, and RoundQuad::read. Each reads by index instead of chunk splits, iterator adapters, closures or an array conversion, with the same calls in the same order and the same panics. The OOD batching loop moves into batch_oods, generic over Arith, so no loop instantiates the round quadratic's fold with the verifier's parent clause.
…d re-proved on RoundQuad and NovelBasis
…padding-aware level-0 sum
…nge and NovelBasis::new
…enerated Lean unchanged)
… requires no padding, so the reveal branch is not taken
…m_le_bytes, ProofOfWork::accepts and Hints
… changes and evidence, new roots and premises, the hiding branch, audit counts
Exact counts
|
Benchmarks: base against this PR, on one runner11d1ae8 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
Field and transpose kernels
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
|
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.
Stacked on #600 (it contains #600 at
c5acc61f5, so the diff includes #600 until that merges) and on the proof model of #551.Rust WHIR verifier to Lean model: conditional refinement of the generated native verifier
This builds on #600 (the anchored opening at
c5acc61f5, on upstream37c1525f: the zero-knowledge leaves #619 to #624 and #631, and the module layout and API cleanups #633 and #634) and on the proof model of #551 (fa13f619). It extracts the actual release-mode Rust verifier with Aeneas and proves that the generated code refines the model, under the premises listed below. Everything lives inverification/whir-aeneas;README.mdthere opens with the same summary and gives details per surface.What is proved
WhirAeneas.Native.verify_refines_native: when the generatedpcs::whir::verify::verify, instantiated with the generated native opening verifier (impl OpeningVerifier for VerifierStateover the BLAKE2s duplex,open_rows_native), returnsOk, the model'sProtocol.verifyaccepts the script's challenges and opening, with the committed oracle tables, against the first committed table and the caller's weight.WhirAeneas.Native.verify_eq_native: the generatedverifyreturnsOkexactly when the model'snativeVerifyaccepts.WhirAeneas.Native.authenticated_nativewithlevel_hints: under injective leaf and pair hashes, the opened rows are the committed tables' rows (AuthenticatedRows), the hints read off the same proof.WhirAeneas.Statement.check_eq/check_accept_model: the generatedStatement::checkis the model-side statement shape check.NativeReads.native_transcript), the Merkle opening and hint decoding (MerkleNative.open_rows_eq,hint_binding), the replay, fold, query, sampler and terminal steps, all against the generated code.All proofs are kernel-checked, without
sorry,admitornative_decide. The audits pass with onlypropext,Classical.choiceandQuot.sound:Audit446 theorems,StatementAudit227,MerkleAudit346,ReplayAudit1231,NativeAudit2010.Premises of
verify_refines_nativeusize.ArithModel,RowModel,NormalizerModel(onNovelBasis::new): the native field arithmetic computes the model's. This waits for Portable, single-threaded native verifier #606's portable arithmetic, which will be extracted and proved; the README gives the plan.Duplex,PowHash,RowHash,PairHash: content contracts of the BLAKE2s duplex mode and of the trial, leaf and pair hashes. The compression is x86 assembly and batched kernels that are not extracted.Function.Injective encode: theF192interpretation.EnsureModelfollows from it, and it is proved for the limb interpretation (limbs_injective).CallerModelplus the weight shape and multilinear-extension premises on the caller's weightb: the caller's contract, also a premise of the model'ssourceNativeVerify_refines.ConfigRel: the source configuration denotes the model's, within the source guards' bounds, and has no lane padding (padding = 0). The model has no zero-knowledge padding, so the theorems cover the configurations in whichverifydoes not take its hiding branch; that branch (WhirReplay::reveal,Padding::share) is extracted and audited, and its proofs are byte-identical, but no theorem relates it to a model.Challenges.valid,ScriptShape,GrindShape, the root equation,NativeAnswers: the proof bytes answer a script of the configuration's shape.Cwhose roots are the script's roots, each row of its level's row width.Source changes
All of these preserve behaviour and exist only so the code translates: index loops instead of iterator adaptors or verifier-capturing closures, no loop under a nested shared borrow, helpers with one early-return loop, rows and siblings read by index. Every change keeps the same calls, operands, order, errors and panics. Evidence for each:
1abc198a,a5781353: proof outputs and the compiled claim-guard probe are byte-identical, and pcs tests pass.826dd798: proof outputs agree with48a5d7cd, with no latency or throughput regression in paired runs.e07bcd58,113d8e61,827ba193,7c36bf96,d7f99e53,9ce194d1: serialized proofs are byte-identical toaeb0a330, and the paired runner detected no regression.660f5903,726f5290: proofs are byte-identical to each parent, and pairedscripts/ab.shflagged nothing.7d1224b2,457a1a09,54d6b710,86621974: all 25 proof outputs (native stack, recursive header and opening, 22 flock reductions) are byte-identical to75d4562b, tests and clippy pass, and pairedscripts/ab.shagainst75d4562bmoved nothing beyond the threshold (for86621974, two leanXMSS prover stages flagged once did not recur in a second paired leanXMSS run).627f2c4f(the merge of Bind every PCS opening to an immutable commitment-time anchor #600 at15a733df, carrying the repairs above onto upstream's new names:Verifier::read_round,Openings::rows,Stratum::batch,sample_queries,Padding::share, andbegin_query/finish_queryin place of the query closure),35ed8398(Hints::next,NovelBasis::newandnormalized_at,RoundQuad::readby index; the out-of-domain batching inbatch_oods, generic overArith) and the normal mergec14d27daof Bind every PCS opening to an immutable commitment-time anchor #600's headc5acc61f5: all 28 proof outputs (the 25 above plus the three seeded hiding proofs) are byte-identical toc5acc61f5; fmt, clippy with-D warnings(Rust 1.97.0 and 1.99, system allocator, native, AVX-512, x86-64-v3 with VPCLMULQDQ and with GFNI, ARM64), the MSRV check, docs and the release tests ofpcs,fiat_shamir,zkandleanvmpass; pairedscripts/ab.shagainstc5acc61f5moved nothing beyond the threshold in the PCS throughput, leanXMSS and kernel workloads, with identical proof sizes and peak heap.Tool patches
verification/whir-aeneas/toolchain/patch-provenance.jsonlists every carried patch with hash, rationale and reproducer. These are Lean 4.34 ports of the Aeneas backend, full-width shift semantics, a kernel proof replacing anative_decide, two guarded generator fixes (parent-trait field names, unreferenced impl metadata) and one Charon fix (monomorphic array builtins). The Box monomorphization patch is an inactive experiment.bootstrap.shapplies the backend patches withgit apply --unidiff-zero, because the kernel-proof patch has no context lines.How to reproduce
From
verification/whir-aeneas:./bootstrap.sh buildthen./bootstrap-tool.sh: install the checksum-pinned Aeneas release and source, Charon, the backend and its patches, and fetch the Mathlib cache../extract.sh statementand./extract.sh replay: regenerateWhirAeneas/Generated/StatementandWhirAeneas/Generated/Replayfrom the source. The root validator checks that every root body is retained and that no references are missing. The replay surface (replay, Merkle and native opening verifier roots), the statement surface and the portable surface were extracted from this branch's head.lake build WhirAeneas.Audit WhirAeneas.StatementAudit WhirAeneas.MerkleAudit WhirAeneas.ReplayAudit WhirAeneas.NativeAudit: checks every theorem and fails on any nonstandard axiom.Heavy steps should run serialized and memory-capped (
flock /tmp/leanvm-heavy.lock systemd-run --user --scope -p MemoryMax=20G ...), as the scripts do.Not covered
This PR claims no security level or knowledge soundness on its own; those come from the model through the premises. It does not relate the zero-knowledge hiding branch (
padding > 0) to a model. It also does not verify allocator, OOM or ABI behaviour, and it says nothing about debug-profile execution.CI and Counts
CI completed for
11d1ae8a: every non-skipped check passed except Counts; build-pdf was skipped. The Counts run fails on exactly the four recursion row increases #600 records for its anchored opening (leanxmss-400 2-to-1 first 138529 to 138941, 2-to-1 node 119413 to 119792, 4-to-1 first 275681 to 276497, 4-to-1 node 250195 to 250973; proven rows and committed words unchanged). This PR's source repairs keep every proof byte-identical to #600's head, so the increase is #600's, inherited through the merge.