Repository navigation
Author leanVM circuits in Clean, prove them, and export them to Rust - #595
Open
kevaundray wants to merge 80 commits into
Open
kevaundray wants to merge 80 commits into
kevaundray wants to merge 80 commits into
Conversation
Benchmarks: base against this PR, on one runner7cca49c merged into its base, against the base b094d00: 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; leanXMSS
Prover stages
Every resultBLAKE2s
Prover stages
Fibonacci
Prover stages
Field and transpose kernels
Flock
PCS
leanSPHINCS
Prover stages
leanXMSS
Prover stages
|
kevaundray
changed the title
kevaundray
changed the title
…an-circuits-shift-20261010
…' into kw/clean-hashrec-20261010
…ash circuit from it The Hash class's gate list is now flock::clean::blake2s, generated from the Clean circuit LeanVMCircuits.Blake2s.Compress. Compress.soundness proves every satisfying witness outputs RFC 7693's F for the two legal finalization words, Rfc7693.abc checks the specification against the RFC's test vector in the kernel, and Compress.lowered proves the exact lowered artifact, whose additions are proven calls of the exported 32- and 31-bit adders. The hand-written G loop is removed; the word witness and its pin to the gate walk are unchanged, as are the product slots.
… for the prover K is (ZMod 2)[X]/(x^64+x^4+x^3+x+1) with Rec.modulus_irreducible checked in the kernel from carry-less certificates, a Clean FiniteField whose value is the machine's coefficient word; E is K[y]/(y^3+y+1) with its limb formulas. Every slot of EMUL, EXK, HASH, SPLIT and CAST is Form data with its theorem (emul_spec, exk_spec, hash_mux, split_spec), the HASH and SPLIT identities a Clean assertion, and GenerateRec.lean prints them as rec/clean.rs, which Table::slot and Table::identities now read instead of the hand-written forms.
Rec.Rows proves, from the table theorems and the bus equalities a pattern holds its slots to: an EMUL row held to one makes its factor the unique inverse, add sums, a SPLIT row with zeroed high bits packs a number below 2^n, the CAST views, a hash row's challenge words, and a Merkle node's placement of its child by a Boolean bit.
…to the proven ones Rec.hash_row_compress proves a hash row's output columns are RFC 7693's compression of its input columns when its packed witness satisfies the exported BLAKE2s artifact and its ports are its columns' words. Tests check that inv, pack and node emit the row shapes Rec.inverse_row, Rec.pack_row, Rec.node_row and Rec.hash_row_compress assume.
…tement digest in rows against RFC 7693 Rec.Merkle: hash rows chained output to chaining value output BLAKE2s-256 of their message columns; node rows up a path output the Merkle root of the leaf and their bits and siblings; parent rows over a subtree's levels output its root. Rec.Statement: Builder::chain's rows output the hash of a word message, and a tree statement's digest rows the hash of its header and items. Drop the row-shape tests, which only restated the builder's wiring.
…ts step port proven to be the clock reference
…k_circuit, pinned to the handwritten gate list
…ws give Clock.Holds, and build Clock::builder from the generated gates
…ist is pinned to them
…m over the exported clock circuits
…ck against Clock::step, and make the clock builder crate-internal
… keep the multiplier plan for native witnesses
…rd helpers left without callers
…an-circuits-shift-20261010 # Conflicts: # crates/leanvm_core/src/rec/circuit/builder/arith.rs
…e session seed, words absorbed and squeezed, the digest, the new proof of work; trace k_to_d and model it The duplex core (counters, hold-back, output blocks) is unchanged by leanEthereum#607. What changed and is modelled: the seed node is init(session) (the old seed with a zero statement half), the instance is the first message, roots are four words, COMMIT/POW_BASE/NONCE are gone (the terminal binding is four squeezed words), and proof of work hashes a squeezed challenge with a u64 nonce and checks the trial word's top bits. Builder::k_to_d, now used by the transcript, is traced, with a Lean model and contract, so checkrec replays tree circuits.
# Conflicts: # crates/leanvm_core/src/rec/circuit/builder/hash.rs
…model them: Model.hashBlock, Model.dToHalves, their contracts, leafBlock_eq leaf_block is d_const of its counter word then block's row (Model.leafBlock_eq, by rfl); checkrec parses block and d_to_halves. No tree or signature dump calls them yet; the claim-set trees of leanEthereum#614 will.
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.
Changes
Shift::circuit,Load::circuitandStore::circuitconsume generatedflock::cleanartifacts. Preserve native optimized witnesses, ordered product slots, structural zeros, padding and proof formats.LdandSduse the exported wrapping adder.Alu::circuitconsumesflock::clean::alu64; its optimized native witness, private product ordering and directly committed jump products are preserved.ClockandExt::clock_circuit, and remove the handwritten builders. Prove their clock and address contracts for arbitrary satisfying witnesses without changing native witness kernels.Hash::circuit, retaining its optimized witness and product ordering. Recursion HASH rows use the same circuit.Boolean circuit proofs
The adder theorems prove the modular wrapping result or exact sum including carry. Shift soundness covers amount masking, both directions, word extension and arithmetic fill, under exactly the six legal flag words.
Flock.Load.source_eqandFlock.Store.source_eqlink lowering of the actual Clean sources to their artifacts. Soundness specifies the bus word and loaded value or updated cell for arbitrary satisfying assignments. Legal load flags are0, 1, 2, 4, 5, 6; legal store flags are0, 1, 2. Store's contiguous replacement specification exposes effective address alignment.Memory.bus_aligned_iffconnects that premise to the low three bits of the bus address. Layout checks preserve 253 load and 309 store products; well formedness and completeness extend every input assignment. Binding the supplied cell to a memory table key, instruction decoding and the global table/bus argument are not yet proved by these local theorems.Flock.Alu.source_eqlinks the actual Clean ALU to its checked artifact.soundnessproves raw Boolean semantics for arbitrary satisfying witnesses and arbitrary flag bits;soundness_referenceproves ADD/SUB, word sign extension, logic, signed/unsigned comparisons, all branch polarities and JAL/JALR for the 17 explicit legal flag words. Layout checks preserve 551 products, including the final 64 committed jump products. Completeness extends every assignment to its 335 input bits. Decoding, preparation ofdtandpc4, and global next-PC binding remain outside these local theorems.BLAKE2s
Compress.soundnessandExport.soundnessprove RFC 7693 compression for arbitrary satisfying witnesses and finalization words0or0xFFFFFFFF.Compress.loweredproves exact source linkage; addition call theorems identify bound adder artifacts. The RFC Appendix B vector is checked in the kernel. Register program printing, small Rust word helpers and port binding remain trusted.Multiplication and division
MulDiv.mul_eq,mulh_eqanddiv_eqidentify circuit arithmetic with the independent RV64IM M extension specification, including zero divisors, signed overflow, rounding toward zero and word sign extension. The production carry save multiplier plan is checked by kernel reduction at 64 and 128 bits; its arbitrary satisfying assignments compute the modular product.MulDivExport.Mul,MulhandDivsource theorems identify the actual Clean sources with their artifacts, soundness covers arbitrary satisfying witnesses, and completeness extends every port assignment. Division proves the integer quotient/remainder check and architectural output whenbadis clear; honest hints clearbad.Production
Mul::circuit,Mulh::circuitandDiv::circuitconsume generatedflock::cleanfunctions. The multiplier functions use checked in step tables interpreted by a small Rustreplay; surrounding gates are emitted directly. Remaining trust includes Lean runtime emission, the Rust table interpreter and call/port binding, native optimized witnesses and protocol acceptance implying artifact satisfaction.Clock and instruction tables
Flock.Clock.*.soundnessproves clock bounds, live increment and failure marking, and access ordering for the exact exported rows. Source linkage, product layouts and completeness are checked for the register, load, store, hash and EXT slot lists.Clock::builderandClock::circuitare now crate private and support exactly these five production lists, not arbitrary slot lists. Every production caller is migrated.Flock.ExtClock.soundnessproves flag bits and wrapped pointer offsets, including BASE gatedbaddresses; its 479 product layout and source linkage are checked.ClassTable.tables_correct_of_clockderives C1 through C3 from exported artifact satisfaction with explicit word-to-column bindings, concludesMachine.Correct, and proves each row reads its decoded entry at its own PC. The production layouts and ordered flush plans now come from the same Clean source, as described below. Native field/coordinate interpretation, concrete port packing, EXT's separately assumed Boolean BASE column and verifier bus correspondence remain trusted; this conditional clock theorem does not itself prove the decoder or instruction bindings.EXT field identities
ExtensionProduct.sourceandsource_holdslink the actual Clean assertion to the exact three exported degree-two identities.soundness_iffproves arbitrary field witnesses compute the cubic extension product plus the scaled old destination; Boolean accumulation selects MUL/MAC, and zero upper operand limbs give the scalar forms.witness_existsextends every assignment to all ten inputs without an honest-witness premise. ProductionClassTable::identitiesconsumes generatedtables/clean.rs; the handwritten identity builder is removed and optimized native arithmetic is unchanged.Remaining trust includes the emitter/compiler, native
BusForminterpretation, logical-to-table column binding and Rust field representation/arithmetic. Boolean accumulation and zero upper scalar limbs are explicit instruction premises, not silently inferred from honest witnesses.Integer-multiplicity bus
Clean channels separate message fields from multiplicity types, preserving existing defaults and allowing
ℤcounts. The Bus modules prove exact symbolic fingerprint balance, bytecode lookup correctness, the state walk and memory consistency, including RAM/advice composition under disjoint address ranges.machine_correctandmachine_correct_of_product_checkcompose these for abstract machine rows; the clock/table theorem above discharges C1 through C3 and PC/read-address linkage under its explicit artifact and column premises. Schwartz-Zippel error, GKR/sumcheck, PCS binding and Boolean producer bits remain outside these integer bus theorems.Instruction table layouts and bus plans
GenerateTables.leanexports all elevenClassTablelayouts, shared aliases and ordered state, decoded bytecode, register, RAM, hash-block and EXT access tuples to productiontables/clean.rs. Every caller consumes the generated functions; the handwritten allocator, flush builders, obsolete helpers and copied fixtures are removed.Coord.eval_expr,sourceTuple_eqandSpec.source_eqprove the exact exported coordinate source evaluates to the integer-multiplicity Clean interactions used by the bus theorems, for arbitrary field rows.The existing tracing-gated
circuitsCLI writes the actual native table dump.checkflushesstill guards nativeClassSpecclass order and slot lists andColumns::column's clock-port projection; those bindings are not generated by this stage. Remaining trust includes the printer/compiler, native coordinate and field interpretation, decoder and filled word bindings, Boolean producer bits and verifier bus correspondence.A release before-and-after smoke exercises every class, both hash forms and all four EXT forms, verifies serialized real proofs and rejects false public outputs. Proof bytes and table heights are byte-identical across this cutover, with no protocol version change.
Partial recursion circuit
Rec.modulus_irreducible,Rec.card_KandRec.extModulus_irreducibleestablish GF(2^64) and its cubic extension; arithmetic linkage and nonzero inverse completeness are proved. Generatedrec/clean.rssupplies production table forms and identities. Row contracts cover arithmetic, bits and packing, CAST views, RFC 7693 HASH ports, Merkle paths, tree roots and statement digests. The whole word duplex model follows the deployed spongefish session seed, first instance message, digest challenges and nonce/top-bit proof of work, with explicit bounded counter and tweak/tag separation results. It is not a formal equivalence proof for Rust's byte duplex or session derivation.Model.Call.exec_goodandModel.replay_soundprove the Lean builder's operation contracts under its explicit satisfying row and public value semantics.Rec.copy_argumentproves the copy consequence under its balancing hypotheses. Tracing is compile time gated and absent from ordinary builds.checkrecchecks native calls, finished rows, public row order and fixed copy links for eight leanXMSS output-tree configurations and all positions of one-tier and two-tier claim-set examples, including multi-bit kind selectors and the wrap. All fifteen pass with the existing Lean model and parser. This is finite checking, not general Rust builder equivalence.Remaining trust includes Rust field representation and arithmetic, the printer, parser and executable class/link computation, chosen session constants, which verifier calls are made, the circuit-index binding to the tier's fixed polynomial, accepted proofs implying
Model.Sat, table sumcheck, HASH Flock soundness and native public value columns. Other configurations retain transcription trust. No complete recursion circuit, union soundness or Fiat Shamir security claim is made.Upstream #607 changes proof bytes, not only the API, with a length-prefixed NARG section followed by hints. After #614, #618 and #626, the current envelopes are
LVMP16 andLVMT17, and the tree session domain isleanvm-tree-14. Claim-set begin-bit words are absorbed before the fingerprint challenge; the verifier's message schedule and union soundness remain outside these proofs.Upstream #611, #612, #615 and #613 are merged normally. The recursion model follows the explicit-tweak
blockbuilder call:Model.hashBlock_goodproves compression under the stated finalization flag premise,Model.leafBlock_eqidentifies the constant-tweak wrapper, andModel.dToHalves_goodproves the CAST halves. The claim-set and canonical union machinery is not formally modeled here. The merged-tree release smoke verifies serialized leaves and 2 to 1 first/node aggregation and rejects altered outputs, reordered statements and foreign envelopes.Upstream
b094d006is merged normally. The tracing API now selects circuits and fixed columns by positional index. Compared withdc57267d, all eight existing dumps change only session-derived seed constants in calls and public rows; rows, classes, public order and copy links are unchanged. The eleven-table dump is identical. A release smoke verifies serialized leaves, output-tree first/node aggregation, a single-tier union, a two-tier large node and its automatic wrap, and rejects false leaf outputs, reordered output statements, foreign envelopes and altered claims.Verification
The merged Lean build, transitive axiom audit, stock leanchecker replay of all 105 source modules, imports only root and compiled module guards,
checkflushesand all three deterministic Rust regeneration checks pass. The two integer-multiplicity Clean modules were also checked at the pinned fork commit. CI derives the module list mechanically and replays it sequentially, trading wall time for bounded memory without a custom kernel checker.An actual release ALU smoke executed overflow/carry boundaries, word sign extension, signed/unsigned comparisons, logic, every branch polarity, JAL and odd-target JALR, verified an encoded leaf proof and rejected a changed public output. The permanent Flock regression proves unchanged native witnesses for all 17 legal flags and rejects false value/jump outputs, a private product, an unused flag bit and padding. Earlier release memory smoke covered every width, encoded leaf and 2 to 1 recursive proofs, false statements and misaligned traps. All eight shipped recursion configurations passed
checkrec, including fixed bus links.A release clock/EXT smoke exercised all five generated clock configurations through register, load, store, hash and all four extension forms, verified serialized real VM proofs and rejected changed public outputs. Scoped Flock regressions reject false clock steps, private products, padding and altered EXT flag/address products. The complete local release workspace suite passed for the merged clock stage under the required resource cap.
A release multiply/divide smoke exercised all thirteen RV64IM forms at zero, sign, word and overflow boundaries, compared execution to independent host arithmetic, verified a serialized real leaf proof and rejected a changed public output. Scoped Flock regressions rejected mutated multiplication bits and an incorrect quotient whose
badverdict was cleared. The merged native, haswell, AVX2, AVX512, ARM library and tracing/system allocator CLI lint checks and rustdoc passed. Local full testall was skipped at 45 GiB available; the full CI workspace suite passed.A release EXT field smoke exercised all four forms with zero and high-bit operands and nonzero old destinations, checked host field results, verified serialized real leaf proofs and rejected altered outputs. The existing field-identity regression rejects mutated result limbs, and an executable exporter smoke rejects unsupported columns, linear shapes and coefficients. Formatting, native/haswell/AVX2/AVX512 Clippy, ARM leanvm-library Clippy with circuit tracing, tracing/system allocator CLI Clippy, rustdoc and the complete local release workspace suite pass. The broader local ARM workspace lint could not configure cross-compiled jemalloc; native ARM CI supplies that workspace coverage.
The merged clock tree passes formatting, Rust 1.97 native, AVX2 and AVX512 Clippy, Rust 1.99 haswell Clippy, ARM library Clippy with tracing enabled, tracing enabled CLI Clippy, rustdoc and the complete local release workspace suite. The previous ALU/bus stage also passed the complete CI matrix.
The EXT field and upstream spongefish integration stages, including audit repair
02bb568d, pass the complete CI matrix: Clean export and per-module kernel replay, all eight recursion builder replays, full workspace tests, ARM and x86 SIMD checks, RISC-V guests, ACT4 and benchmarks. The large multiplier plan and its export build sequentially before the remaining build, trading additional build serialization for lower concurrent proof memory use. The merged local checks above, including the complete release workspace suite, also pass.The table-source cutover passes the complete local release workspace suite, formatting, Rust 1.97 native/AVX2/AVX512 Clippy, Rust 1.99 haswell Clippy, ARM library Clippy with tracing, tracing/system allocator CLI Clippy and rustdoc. Its executable exporter smoke rejects unsupported indices, coefficient words, column references, truncating tuples and colliding access slots, and accepts the sixteen-coordinate boundary.
The subsequent upstream merge also passes the complete local release workspace suite, the same lint and rustdoc matrix, all eight recursion builder replays, the eleven-table binding check and all three regeneration diffs. Generators explicitly use Rust's workspace edition 2024 so temporary output formatting matches checked-in consumers.
The table-source and subsequent upstream integration head
dc57267dpass the complete CI matrix, including Clean export and kernel replay, native recursion and table binding replay, full workspace tests, ARM/x86 SIMD, guest linting, ACT4 and benchmarks.For the
b094d006integration, the Lean build, Audit, stock replay of the four recursion contract modules, all three regeneration diffs, fifteencheckrecconfigurations,checkflushes, formatting, native/haswell/AVX2/AVX512 Clippy, ARM library Clippy with tracing, tracing/system allocator CLI Clippy and rustdoc pass. Mobile CI is re-enabled. The local release workspace suite finds upstream's failinga_tiered_first_level_and_union_stay_within_their_capacitiesassertion; CI's Test leg remains red until upstream #627 fixes lone-child tier aggregation. No competing capacity fix is included here.At
7cca49c7, every CI job other than that upstream Test assertion passes, including Clean export and per-module kernel replay, all fifteen recursion replays and table bindings, Android and iOS. Test's failure is exactly the lone-child tier assertion above.Boundaries
Theorem dependencies are only
propext,Classical.choiceandQuot.sound, with no admissions or native decision axiom. Lean runtime generation, Rust compilation, native gate/coordinate interpretation, slot packing and optimized Rust witnesses remain trusted. Decoder legality and filled word bindings, EXT's explicit Boolean/scalar premises, Boolean producer bits and verifier protocol correspondence are not discharged by the local circuit or conditional bus theorems. No whole VM or Flock, PCS or Fiat Shamir cryptographic security claim is made. Exact contracts and regeneration commands are inverification/circuits/README.md.