The components of a multilinear proof system over the binary field BF64 and its cubic extension, as leanMultisig's leanVM uses them: the Keccak overwrite-duplex transcript and Keccak-256 Merkle commitment, a polynomial commitment from stacked additive Reed–Solomon codewords, ring switching and a WHIR opening, and the Keccak-f GKR argument. Each has a specification, a prover, a verifier and a soundness analysis; each fast implementation is proved equal to its specification. The tests compare them with leanMultisig 9d8bce818aa7c7e18e67026e522a9b1539d0a57d.
None of these components is at parity with the Rust reference. The table gives the measured gap where the Lean code and the workload match a Rust measurement, and says where a component is unmeasured.
| Component | Workload | Lean / Rust, single-thread instructions |
|---|---|---|
Keccak-f GKR prover (Keccak.GkrProver.prove) |
The reduction on 512 permutations (tests/data/keccak-gkr/active), output claims bound before the phase |
7.9× against leanMultisig's standalone reduction (291 million instructions), 10.5× against the same reduction inside its full Fibonacci proof (218 million) |
Merkle commitment (Keccak.Merkle) |
4,096 rows of 64 words; 100 queries (components) | 4.03× commit, 0.72× open |
Duplex writer (Keccak.Duplex) |
10,000 messages written and sampled; an eight-bit grind (components) | 2.88× write and sample, 2.99× grind |
PCS prover kernels (Pcs.RingSwitch, Pcs.Tensor) |
Six-map coordinates, 64 packed bit folds, 256 mapped weights (binary PCS) | 8.58×, 3.84×, 7.27× |
Honest PCS prover (Pcs.Honest) |
— | Unmeasured; a specification prover, not the fast opening |
PCS verifier and extractor (Pcs.Verifier, Pcs.Extraction, Pcs.ExtractorCache) |
— | Unmeasured as components |
Keccak-f GKR verifier (Keccak.Gkr.Executable) |
— | Unmeasured as a component |
Grand-product GKR (Multilinear.GrandProduct) |
— | Unmeasured; specification and soundness only |
Composed proof system over a System (Tables.Composed, Tables.Compiled) |
The program system and the hashes system (256 Keccak-f permutations with virtual output lanes) |
Unmeasured against Rust; leanMultisig has no proof system for an arbitrary set of tables. The tables performance-gate workload records the Lean prover and fast verifier on program |
The Keccak-f GKR count is the keccak-gkr performance-gate workload, 2.31 billion instructions. The Rust counts are single-thread user-space instruction counts of leanMultisig 9d8bce818aa7c7e18e67026e522a9b1539d0a57d on an AMD Ryzen 7 3700X, not re-measured here: 291 million for its Keccak reduction span on the same 512 permutations, run on its own after the output claims are bound, and 218 million for the same span inside the prover of a complete Fibonacci proof.
leanVM's complete proof system, measured the same way on the same host and revision, opens its PCS at 22× the Rust instructions and verifies at 4.6–4.9× (72–77 ms against 13 ms on the SET and Fibonacci programs); that opening driver and verifier are leanVM's composition and not part of this library.
scripts/check-binary-stack-reference /path/to/leanMultisig builds the harnesses tests/rust/keccak-gkr.rs, binary-pcs.rs, keccak-transport.rs and keccak-transcript.rs against an unchanged checkout of leanMultisig 9d8bce818aa7c7e18e67026e522a9b1539d0a57d, regenerates every fixture of tests/data/keccak-gkr, binary-pcs, keccak-transport and keccak-transcript with one and with sixteen Rust workers, and compares them byte for byte with the committed files; --write replaces them. The Keccak-f GKR fixture and the ring-switching slices are computed from tests/data/keccak-gkr/active/committed.bin, the 64-lane Keccak region of a leanVM execution with 512 padded permutations (input and middle lanes and nonzero metadata in the spare lanes); that input is data, not regenerated.
CompStark/BinaryFields fixes K = BF64 and E = BF64.Ext3 from CompPoly, the extension's limbs, and a kernel-checked certificate that g generates K's multiplicative group (Generator). Native and WordProduct replace the field operations in compiled code with CompPoly's word arithmetic and the five-product cubic multiplication, each by a csimp theorem equating them with the specification instances.
The specifications are Keccak.Transcript (Keccak/Transcript/Duplex.lean): a sixteen-lane overwrite duplex absorbing tagged extension scalars and nonces, squeezing one extension element per permutation, seeding from two digests and grinding by a discarded squeeze; and Keccak.Commit (Keccak/Commit): binary Keccak-256 trees over leaf images of field words, pruned multi-openings, their masked extraction and node-level binding (disagreement_bound), and the random-oracle trace of commitment and challenge queries with its exception bound (RandomOracleTrace.bad_probability_le). Correspondence proves the transcript's framing and replay, and Lanes maps lanes to field words. Keccak.Commit.Codec and MerkleCodec give the exact little-endian encodings of words, scalars, leaves and child pairs; Compiled.MerkleTrace recovers every checked path from a lazily sampled Keccak oracle's log and bounds the trace's exceptions by (max 2 roots + 1) Q² / 2^256 (exception_probability_le), and ChallengeSnapshot with FreshSnapshot and FreshOracleLog proves the recovery independent of each later challenge answer.
The fast implementations are CompStark's lane-level Keccak.Duplex and streaming Keccak.Merkle. Keccak.TranscriptDuplex (Keccak/Transcript/Native.lean) proves the writer equal to the specification: absorb_spec, absorbAll_spec and sample_spec at every item, including full-rate flushes, and grind_refines and grind_min for smallest-nonce grinding. Keccak.MerkleLeaves.merkleRow_hash identifies the streaming tree's leaf hash with the commitment's leaf digest.
tests/CompStarkTests/KeccakTranscript.lean checks 48 Rust vectors: seeds, squeezes across rate boundaries, repeated empty squeezes, digest absorption, grinding checks and pruned openings. tests/CompStarkTests/KeccakTransport.lean checks smallest-nonce grinding at 0, 5 and 9 bits and Merkle roots, rows and hints on field-word leaves.
Pcs.BinaryDomain fixes the basis 1, g, …, g^63 and the binary additive domain; Pcs.AdditiveEncoding proves ArkLib's Whir.EncodingContract for the novel-basis additive encoding over K and E for vars + rate ≤ 64 (encodingContract, extensionEncodingContract), and computableAdditiveNTT_eq_encode its agreement with CompPoly's executable additive NTT below 64. Pcs.Prover.Encoding.encode runs the native bit-plane encoder on extension rows.
Ring switching (Pcs.RingSwitch.Protocol) reduces 64 bit-slice claims at an extension point to one weighted claim on the base-field stack through six Frobenius maps, with its knowledge certificate, local bounds and terminal identity (terminal_iff); Pcs.RingSwitch.Prover computes the honest slices and target. Pcs.Honest.prove commits a base-field table and opens it with ArkLib's WHIR against explicit verifier coins, and proveRing batches the ring-switched claim into the same opening; prove_accepts and proveRing_accepts prove completeness for every schedule and every true claim. Pcs.Verifier gives cached refinements of WHIR's inner products, evaluations and acceptance.
The extractor decodes with CompPoly's Guruswami–Sudan decoder at exact integer Johnson cutoffs: Pcs.Radius computes the cutoff (agreementCutoff_le_iff), Pcs.Parameters selects multiplicities, and Pcs.Decoder.gsListDecoder_correct proves the interleaved list decoder correct with the real Johnson list bound. Pcs.Extraction and Pcs.ExtractorCache prove the cached extractor equal to ArkLib's WHIR extractor at every level (openingExtractorCached_eq, levelExtractorCached_eq).
Pcs.Errors lists WHIR's error per verifier message. Pcs.Levels reads a schedule's levels as natural numbers and decides rational bounds on every row in the kernel: whirErrorRows_le turns levelsCheck κ κq into 2^-κ on every algebraic row and 2^-κq on every column-query row, for any schedule, rate and dimension, the Johnson radius and MCA slack measured at the reduced rate. Pcs.Schedule is leanMultisig's ladder (initial fold 6, then 4, rate exponents r, r + 3, …, its query table and grinding), and Pcs.ProductionLevels.productionLevels_check certifies all 56 of its configurations at 2^-128 algebraic and 2^-111 per column query, 2^-128 after 17 bits of query grinding.
tests/CompStarkTests/BinaryPcs.lean checks cube indexing, the Johnson cutoffs and basis conversion. tests/CompStarkTests/BinaryPcsNative.lean checks that the honest opening is accepted and an inconsistent claim rejected, and compares the native extension encoding (98,304 bytes) and the six-map ring-switching target with Rust.
Keccak.Gkr is a public-coin reduction from claims on the outputs of 2^(p+4) Keccak-f permutations to claims on their inputs and committed middle states: twelve layers per segment of two twelve-round segments, the nonlinear layer through the sixteen-coordinate reverse multiplication-friendly embedding of Keccak.Embedding (injectivity and the CRT correspondence kernel-checked), pack and position sumchecks and the linear layer by its transpose. Gkr.soundness bounds acceptance for a wrong input table by (37 (p + 4) + 902) / |E| over any characteristic-two field E; Gkr.certificate is its knowledge certificate on ArkLib's interaction layer.
Keccak.GkrProver.prove is the word-level prover. specificationTranscript_complete proves the specification prover accepted for every challenge sequence; prove_eq_specificationTranscript and prove_buildWitness_eq_specificationTranscript prove the fast prover equal to it, and prove_complete and prove_buildWitness_complete transfer completeness. tests/CompStarkTests/KeccakGkr.lean compares every witness layer, transmitted scalar, challenge, batch claim and opening with Rust on 512 permutations, and the keccak-gkr performance-gate workload counts the reduction.
Multilinear.GrandProduct proves three batched product trees over any leaves: an odd root-most binary layer followed by radix-four layers, each a sumcheck of normalized messages carrying the cofactor of the known equality factor, then child interpolation. Its knowledge certificate carries riders, constraint-residual tables over an arbitrary witness (Riders W: a fit predicate, tables of fixed heights below a common bound, and their values on the Boolean rows); intermediate layers keep every rider zero on its Boolean rows, and the final layer restricts each rider at its own challenges. GrandProductDecision decides the riders by their finite mixed Boolean grid (ridersRestricted_iff_grid) and every layer relation, and GrandProductBadEvents bounds each normalized round and child interpolation of a fixed candidate list by its local error. WordGrandProduct evaluates the layers on machine words. tests/CompStarkTests/GrandProduct.lean checks layer schedules, layer claims and rider decisions. The prover is not part of the library and the component is unmeasured.
Multilinear.Basic defines low-bit-first multilinear extensions over E with their word-level evaluators; Multilinear.Algebra holds their linearity and interpolation, stacking, fingerprints, product trees and fixed-polynomial sumcheck bounds. Multilinear.Retained gives identity backward maps on concrete transcript trees. Compose.ListLift lifts a family of knowledge certificates over a candidate list fixed before any challenge, multiplying each error by the real list bound, and Compose.Reduction composes such reductions sequentially and appends an opening.
CompStark/Tables describes a statement for this stack: a System is a list of tables connected by named buses. A table is a Stark.Air whose constraints read only the current row of its trace and of its preprocessed trace (Expr.currentRow, unlike Expr.rowLocal of lookups, which also admits the next row and public values), with its bus interactions (on every executed row, push or pull the tuple of its expressions on a bus), the columns that must not vanish on executed rows, its virtual columns, bound by the system's external relation that other arguments establish, and its public padding row. The system lists its buses; the i-th is separated by g ^ i. A Layout gives each table its executed rows and its power-of-two height; rows past the executed count are padding: they hold arbitrary data that satisfies the constraints and take no part in buses or nonzero columns, and the bus argument corrects each by the public padding row, so a table with padding rows reads no preprocessed column in its tuples. Public data is preprocessed, so a data source that is not a table of the computation is a table whose tuple coordinates are preprocessed or committed columns. System.Satisfied is the relation; System.WellFormed the decidable side conditions. The description reuses Stark.Expr and Stark.Air (width, constraints, preprocessed columns) so that one AIR serves the FRI backend and this one, but not Air.lookups: their signed field-valued multiplicities are Plonky3's LogUp, which has no direction or natural multiplicity in characteristic two, so interactions carry a direction and multiplicities are natural through repeated tuples.
The bus argument starts from one multiset equality: every tuple is encoded with its bus's separator first, padded to 2 ^ k entries, and under BusShape (one width per bus) every bus balances exactly when the encoded pushes and pulls are equal (System.balanced_iff); an unbalanced system passes the grand-product test at a uniform (α, β) with probability at most max 1 k · cap / |E| (System.unbalanced_collision_le). The three trees of the grand-product GKR read System.leaves: one block per interaction or nonzero column, executed rows giving β minus a fingerprint or the column's value and padding rows that form corrected by the padding row's, stacked in decreasing height; with every padding row the padding row, root_eq_sideProduct identifies the pushed and pulled roots with the grand products of the encoded multisets, and nonzeroRoot_ne_zero_iff the nonzero root with the nonzero columns. System.riders gives the constraint residuals as the GKR's riders, which vanish exactly when every constraint holds on every row (ridersZero_iff).
The bus protocol (Tables/BusProtocol.lean) draws (α, β), receives the pushed and nonzero roots, runs the grand-product GKR over the three sides at the common depth System.depth (the largest side, the tallest table and at least one variable) with the constraint residuals as riders, and ends with the boundary values. A table is opened directly (System.Direct) when it has no constraints, no nonzero columns and no padding rows and its tuple entries are columns, preprocessed columns or constants; the committed columns its tuples read are the boundary columns, sent by the prover, and every other table's selector-weighted bus forms become one debt per side for the table sumcheck (leaf_decomposition: a side's leaf extension at the GKR point is the public part, computed from the boundary values, the preprocessed columns and the padding rows, plus the table debt). Bus.certificate is the knowledge certificate on GrandProduct.certificate, with the witness retained; Bus.knowledgeSoundness bounds extraction failure by Bus.error = (max 1 k · 2 ^ depth + GKR error numerator) / |E|, the first term the fingerprint collision of an unbalanced system (unbalanced_root_collision_le), and Bus.unbalanced_acceptance_le bounds a true endpoint for an unbalanced witness by the same error.
The table sumcheck (Tables/TableSumcheck.lean) covers the tables that are not opened directly. It draws ξ and batches, with consecutive powers, every constraint of every table in table order (directly opened tables have none) and the three bus debts, into one sumcheck over the tallest such table's variables, highest variable first; each table weighs its rows by the equality weight at the bus point on its own variables and by the product of the variables above its height. Rounds send compressed messages of degree TableSumcheck.degree + 1, where degree is the largest individual degree of a constraint or tuple entry, at least one; at the end the prover sends each table's transmitted columns, those its constraints, tuples or nonzero checks read, at the final point. TableSumcheck.certificate is the knowledge certificate from the bus endpoint, and TableSumcheck.knowledgeSoundness bounds failure by TableSumcheck.error = (constraintCount + 2 + (degree + 1) · height) / |E|: the ξ batch is a polynomial of degree constraintCount + 2 in ξ (debtPolynomial_eval), and each round costs degree + 1. Tables/Argument.lean runs the two in sequence: a witness that satisfies the external relation but not the system reaches true final claims with probability at most Bus.error + TableSumcheck.error (Argument.unsatisfied_acceptance_le), and at accepted endpoints the committed witness satisfies the system unless one of the two extractors failed (Argument.paths_satisfied_or_bad). The final claims, the boundary values and the transmitted values at their points, are the openings the commitment owes.
leanVM's counted lookups are this pattern. A source, memory or bytecode, is a table opened directly: its address and public data are preprocessed columns, its committed data and its finalize count are committed columns, and it pushes (address, 1, data) and pulls (address, final, data) on one bus. Every reading row pulls (address, c, data) and pushes (address, c · g, data), and declares c a nonzero column; the nonzero blocks are leanVM's count blocks and the nonzero tree its count tree, whose leaves are the count columns' values with the padding correction and whose nonzero root shows every executed count nonzero. With counts nonzero, fewer reads than the order of g and balance, each read returns its slot's data and final = g ^ reads; that cap is a condition on the layout and the conclusion a lemma of the instance, not part of the system. The state bus is a height-zero table opened directly whose tuples are the public initial and final states as constants. The program example is a bytecode source with its reading table, and its tests check that the program table is opened directly at its final counts.
The bus and table sumcheck are leanVM's choices stated for a general system: separators g ^ i in bus order, the public padding row, one GKR over three sides at a common depth, sorted blocks with selector weights, and one ξ batch and one sumcheck over the tallest table with back-loaded shorter tables. leanVM's protocol is an instance when its tables are declared in its table order, each with its columns in production order, the memory table before the bytecode table with its limbs before its finalize column (the boundary values are the directly opened tables' read committed columns, table by table, columns increasing), the tallest table has a block on some side and some side has at least two leaves (then System.depth is leanVM's busDepth), and every table column other than Keccak's committed middle-state lanes is read by a constraint, a tuple or a nonzero check (the table sumcheck transmits exactly the read columns); that these hold for leanVM's tables is not checked here. The Fiat–Shamir transcript, the commitment and the fast verifier are the composed system below.
CompStark/Tables/Examples.lean has two systems over BF64, proved well formed: squares (three tables of different heights, a tuple pulled twice, a virtual column) and program (a public program as a preprocessed source with padding, read by an execution table through counts that must be nonzero); tests/CompStarkTests/Tables.lean checks their witnesses, rejects tampered ones, and checks which tables the bus opens directly, the boundary columns, the transmitted columns and the sumcheck's degree and height.
CompStark/Tables/Composed composes the bus and the table sumcheck with the stacked commitment, ring switching and the WHIR opening, for any System and Layout. The committed object is the stack (System.stack): every committed column in decreasing height, each an aligned block of a table on M variables. The verifier's state is that stack; a Setup adds the side conditions (well formed, bus shape, the stack fits, the boundary columns are committed, the table sumcheck's degree fits the interpolation points) and an External argument for the virtual columns. An External says how a witness is read off a stack (interpret), carries a rider on the table sumcheck's draws (a relation the table phase restricts one coordinate at a time, so that the argument starts at the table's point instead of drawing its own), gives its start relation at the table sumcheck's output, its protocol, its parsed output and its weighted claims on the stack; External.Reductions gives its reductions and error and External.Honest its honest prover. External.none serves a system without virtual columns.
The outer reductions run the bus, the table sumcheck and the external argument on the stack; their outputs are pooled into weighted stack claims (openingClaims: the boundary values, the transmitted committed values, the argument's claims), which the WHIR opening checks. Composed.knowledgeSoundness bounds extraction failure of the composed certificate by totalError = initialListBound · (Bus.error + TableSumcheck.error + external error) + whirBudget, the WHIR errors from Pcs' certified levels, and extracted_satisfied turns extracted knowledge into a satisfying witness. Composed.completeness shows the honest prover's transcript accepted against every coin sequence for every satisfying witness whose padding rows are the padding row. Composed.verifyWith is the executable verifier, with certified evaluators for every claim weight, and verify_iff proves it equal to the specification's acceptance.
The Keccak table (Composed/Keccak) is the external argument for virtual output lanes: a table of 2 ^ (p + 4) permutations whose 64 committed slots are stacked as one aligned region and whose 25 output lanes are virtual. Its rider is the Keccak-f GKR's initial discrepancy on the instance coordinates; after the table sumcheck it runs the GKR without its instance draws, at the table's point, then six ring-switching draws on the slot region, leaving a word claim and one ring-switched claim. Its error is (36 (p + 4) + 902) / |E| + 6 / 2 ^ 192. Its honest prover is the GKR's specification transcript; the compiled tests use the native GKR prover, whose transcript is the specification's at its own challenges.
CompStark/Compiled and Tables/Compiled compile the composed system: the stack's initial word and WHIR's encoded words as Keccak Merkle roots, every coefficient message revealed, draws from the Keccak duplex seeded with an initialization vector and a statement digest. Tables.Compiled.knowledgeSoundness is standard-model knowledge soundness: a proof verifies while the extracted stack fails the composed input relation with probability at most the Merkle extractor's node failures plus, at each of the count draws, the correlation-intractability failure of the challenge table. The random-oracle bounds on those games are not instantiated for tables.
fixtures/CompStarkFixtures/Tables.lean runs the program system and fixtures/CompStarkFixtures/TablesKeccak.lean the hashes system (a Keccak table of 256 permutations with virtual output lanes, read by a user table that pulls one state twice) through the honest prover and the fast verifier; tests/CompStarkTests/TablesComposed.lean and the compiled tests/CompStarkTests/TablesKeccak.lean check acceptance and rejection. The tables performance-gate workload proves and verifies the program system.