Components and theorems

The detailed reference of what CompStark implements and proves, component by component: files, theorem names, assumptions and benchmark commands. The README gives the overview.

Poseidon2 (CompStark/Poseidon2): the specification permute runs on any field. A field's implementation of an instance is a permutation with a proof that it is the specification (Poseidon2.Impl, CompStark/Poseidon2/Impl.lean), and Poseidon2Field F gives Plonky3's instances of widths 16 and 24 with their implementations, on which Plonky3's hashes and challenger are built; the specification itself is the default implementation (Poseidon2Field.ofSpec). Plonky3's default constants over KoalaBear (S-box x ^ 3, CompStark/Poseidon2/KoalaBear.lean, the round constants Plonky3 regenerated with the Grain LFSR) and BabyBear (S-box x ^ 7, CompStark/Poseidon2/BabyBear.lean); tests check Plonky3's outputs. permute_map transports a run along any ring homomorphism, so the permutation on CompPoly's Montgomery field is the specification (KoalaBear.fast_width16, BabyBear.fast_width16, …). KoalaBear's and BabyBear's implementations are the packed kernels below, one state in lane 0 of a group, for any round constants of the field's shape (CompStark/Poseidon2/PackedInstances.lean: Instances p holds both widths' constants with their shape proofs, Instances.field and Instances.packed give their Poseidon2Field and packed kernels, Instances.perm16_eq, Instances.perm24_eq; KoalaBear.Instances and BabyBear.Instances in CompStark/KoalaBear/Poseidon2.lean and CompStark/BabyBear/Poseidon2.lean, whose default instances are Plonky3's, and fixtures/CompStarkFixtures/Poseidon2Example.lean holds the ones Plonky3's example prove_prime_field_31 draws with new_from_rng_128 from SmallRng seeded with 1, generated by compstark-bench keccak-example-constants). The interpreter cannot run the packed kernels (CompPoly's inline C stores), so the known answers that use them run compiled (tests/CompStarkNativeTests.lean, the test driver); the prover and the benchmarks run them too. The specification is ArkLib's Poseidon2, a translation of leanSpec's, at both widths (permute_arkLib16, permute_arkLib24, CompStark/Poseidon2/ArkLib.lean), at Plonky3's current KoalaBear constants, which ArkLib's parameters predate; proving it found two indexing bugs in ArkLib's round constants, fixed in ArkLib#1316.
Packed Poseidon2 (CompStark/Poseidon2/Packed.lean, PackedKernels.lean): eight states at a time, one per vector lane, with round kernels on Montgomery words that Unrolled.lean generates for a field's shape: its modulus p = r · 2 ^ s + 1, its S-box degree and the tails of its internal diagonals, whose entries after the ninth are ±2 ^ (-k) and cost a shift and a subtraction (mulInvPow2). The word arithmetic (Arithmetic.lean, ArithmeticLemmas.lean), the models of the kernels (PackedLanes.lean) and the correctness of the round loops (PackedCorrectness.lean, PackedCorrectness24.lean: permute16_spec, permute24_spec) are generic over a 31-bit Montgomery field with a PackedKernels p instance; a field's module generates its kernels and proves each equal to its model with the shared tactics (PackedKoalaBear.lean, S-box x ^ 3; PackedBabyBear.lean, S-box x ^ 7), and KoalaBear.Packed.permute16_width16, BabyBear.Packed.permute24_width24 and their siblings read Plonky3's instances in the spec field. Every kernel first writes eight words of its group back unchanged, so the compiler knows the buffer is exclusive and interleaves loads with stores instead of holding all loaded words until the first exclusivity check. The multiplier-bound S-box kernel leaves its powers below 2 p (cubeLazy, pow7Lazy) and the mat4 kernel reduces them; a partial round's sum is a tree beside its S-box, and coordinate 0 is rest - y. The round loops carry a buffer of fixed size and check the group and the constant tables once per permutation. A field's partial rounds are one loop of its own with the kernel inlined (PackedKernels.partials16, partials24, on partialsLoop16), so a partial round makes no call. Single thread, on an 8-core Ryzen 7 3700X: about 157 ns per width-16 permutation and 255 ns per width-24 one over KoalaBear, against 118 ns and 193 ns for Plonky3's AVX2-packed Poseidon2KoalaBear and 676 ns for its scalar width-16 one (CompStarkBench poseidon2-packed 14, CompStarkBench perm24 14, bench/rust: compstark-bench bench 14); over BabyBear about 243 ns and 410 ns on a loaded host, against 213 ns and 318 ns for Plonky3's AVX2-packed Poseidon2BabyBear and 148 µs for the specification on one state, which BabyBear's provers and verifier ran before (CompStarkBench babybear-perm 14).
Hashing and Merkle commitments (CompStark/Hash/Sponge.lean, CompStark/Merkle/Tree.lean, CompStark/Plonky3/Hash.lean): Plonky3's PaddingFreeSponge and TruncatedPermutation, and MerkleTree::new over lists of matrices of mixed heights, with the Poseidon2 instances of Plonky3's Poseidon2MerkleMmcs (width-24 sponge for leaves, width-16 compression). Tests check digests and roots against Plonky3, including odd heights and injected smaller matrices. The tree is VCVio's Merkle tree with injected payloads (MixedMerkleTree, CompStark/Merkle/VCVio.lean, CompStark/Merkle/Mixed.lean): the leaves hash the rows of the tallest matrices, and the rows of a shorter matrix are injected at the depth of its height (injNode). Plonky3's single and pruned multi-openings are VCVio's climbs and walks at the injection schedule read off the height groups (climb_eq, walkM_eq, sched_eq_find), so VCVio's restoration of the paths of a multi-opening, its honest-opening theorems and its extraction from a cache of answered hash queries (MixedMerkleTree.extract, stable under cache growth that predicts no reachable digest) carry over (CompStark/Merkle/MixedMulti.lean, CompStark/Merkle/ExtractMixed.lean). For matrices of one height, the tree is VCVio's inductive Merkle tree: the root is buildMerkleTreeWithHash's, openings are generateProof's paths read from the leaves up, honest openings verify, and two accepted openings of different rows at one index give a collision of the compression or of the leaf hash (verifyBatch_binding). VCVio is pinned at the merkle-mixed branch of the bot fork, which adds these trees. Commitments are Merkle caps, Plonky3's MerkleTreeMmcs cap_height (Fri.Params.capHeight, Stark.Cap): the 2 ^ h digests of the layer h levels below the root, h capped at the tree's levels, the root alone for h = 0 (Merkle.capOf); the transcript observes a cap's digests in order (capElems), and a multi-opening is checked against the cap entry above each index (Merkle.verifyMultiM, which rejects a cap of another size and matrices injected above the cap; verifyBatch_of_verifyMulti and verifyBatch_of_verifyMulti_mixed give every query an accepted opening of the subtree under its cap entry).
Packed Merkle commitment (CompStark/Merkle/Packed.lean): the root of one matrix given as chunks of rows, leaves hashed eight rows at a time by the packed width-24 sponge in parallel chunk tasks (the fast prover hashes its extension in place, in tasks over ranges of 512 rows, leavesIn), layers compressed eight pairs at a time by the packed width-16 permutation in parallel range tasks. root_eq (RootCorrectness.lean, on PackedCorrectness.lean) proves it is Merkle.Poseidon2.root of that matrix. For $2^{14}$ rows of 64 elements: about 3.8 ms on 16 chunks and 25.6 ms on one core, against 2.1 ms and 15.6 ms for Plonky3's MerkleTreeMmcs::commit on its default rayon pool and on one thread (CompStarkBench merkle 14 64 16, taskset -c 5 CompStarkBench merkle 14 64 1, bench/rust: compstark-bench merkle 14 64, RAYON_NUM_THREADS=1).
STARK prover and verifier (CompStark/Stark/Prover.lean, CompStark/Stark/Verifier.lean, on CompStark/Challenger.lean, CompStark/Merkle/Mmcs.lean, CompStark/Fri/Prover.lean and CompStark/Fri/Verifier.lean): Plonky3's uni-stark prove and verify with the two-adic FRI commitment scheme at Plonky3 revision a4982ec, including FRI folds of higher arity, over any base field with a BaseField instance and any extension field of it with a Challenge instance (CompStark/Stark/Challenge.lean: coordinates, base embedding and a ring isomorphism with CompPoly's spec field over the base field), with the Poseidon2 Merkle commitment above and the width-24 duplex challenger. The fast backend runs over any fast extension of a Montgomery field: the quartic and KoalaBear's quintic. AIRs are lists of constraint expressions (CompStark/Stark/Air.lean); as in Plonky3 (main_next_row_columns), an AIR that does not read the trace's next row (Air.mainNextRow) has its trace opened at ζ only, and the verifier rejects a next row opened for it. The transcript is Plonky3's typed Fiat–Shamir layer: the STARK, the commitment scheme and FRI each observe a domain separator first (CompStark/DomainSeparator.lean: the protocol's name, the Keccak-256 hash of its interaction pattern and the instance's shape), the duplex challenger tags each absorb with its length, and besides the fold and query rounds the rounds of ζ and of the batching challenge may grind too. FRI opens its queries as Merkle multi-openings with pruned paths (Merkle.verifyMultiM, CompStark/Merkle/Multi.lean: an accepted multi-opening gives every query an accepted single opening, and honest pruned paths verify). Preprocessed columns follow Plonky3's setup_preprocessed and verify_with_preprocessed: an AIR carries its preprocessed trace (Air.preprocessed, Air.preprocessedWidth), constraints read its current and next rows (Expr.prepCur, Expr.prepNext), and setup computes its verifying key (PreprocessedKey: the width, the trace's log height and the Merkle cap of its low-degree extension). The transcript observes the preprocessed cap after the trace cap; the commitment scheme opens the preprocessed trace at ζ, and at ζ ω only if the AIR reads its next row (Air.preprocessedNextRow); the verifier rejects a key or openings that do not match the AIR's shape. It also rejects an empty quotient cap, and FRI an empty commit-phase cap, before observing them: observing nothing would merge two duplexing rounds of the challenger, and Plonky3 rejects such a cap when it checks the openings against it. Periodic columns follow Plonky3's periodic_columns: an AIR lists one period per column (Air.periodic, read by Expr.periodic), of a length that is a power of two dividing the trace's height; as a polynomial a column of period p is f(Xⁿᐟᵖ), f its period's interpolant (periodicPoly). Periodic columns are neither committed nor opened: the domain separator carries their number, the verifier interpolates each at ζ ^ (n / p) (periodicAt), and the prover extends each period onto the quotient domain (periodicOnQuotient). With periodic columns Plonky3 sizes the quotient by the constraints' polynomial degrees on the trace (Expr.degBound, a periodic column of degree n - n / p) rather than by degree_multiple, so the chunk count depends on the trace length (Air.logQuotientChunks). On Plonky3's proofs of a Fibonacci AIR, of a degree-3 AIR with a two-chunk quotient, of an AIR with preprocessed columns, with and without next-row reads, and of AIRs with periodic columns (Plonky3's PeriodicAir and a degree-3 AIR whose quotient the periodic sizing halves), for several FRI parameter sets (tests/data), grinding at every site included, the verifier accepts them and the prover reproduces them exactly, grinding witnesses included. Both are reference implementations: the prover's speed comes from the fast backend below. No zero knowledge yet. The verifier is written once over its hash functions (CompStark/Primitives.lean: a challenger that observes and samples base elements, the Merkle leaf hash and compression, all in a monad): verify is verifyWith (poseidon2 F), and the same code runs on random oracles. FRI folds by Plonky3's schedule for the input heights (foldSchedule), which proofs no longer carry.
Base field (CompStark/BaseField.lean): the verifier, the specification prover and the whole analysis (soundness, the verifier on random oracles, the spec field and its error terms) are generic over a prime field F of odd characteristic with a BaseField instance: finiteness as a proposition (Finite F, so no executable enumerates the field; the analysis counts it by Nat.card F), a prime number p = |F| of elements (card_prime, so the characteristic is p, ringChar_eq_card), a canonical value F → ℕ, a bijection onto [0, p) for p = |F| (CompPoly's CanonicalNat, of which sampleBits keeps the low bits); two-adic generators twoAdicGen k of order 2 ^ k for k ≤ twoAdicity, each the square of the next, so that 2 ^ twoAdicity ∣ p - 1; and a coset shift gen ≠ 0 with gen ^ 2 ^ twoAdicity ≠ 1. The domains of a configuration must be two-adic subgroups: logN + logBlowup ≤ twoAdicity (ValidConfig). The bias of sampleBits is bounded for 2 ^ b ∣ p - 1 (CompStark/Sound/Sampling.lean), which the query indices satisfy, and the grinding probability is powFraction F bits = ((p - 1) / 2 ^ bits + 1) / p for any p. CompPoly's fast Montgomery field FastField p of any prime with a Mont32Field p instance is a base field given its domain data, Mont32BaseField p: the two-adicity, the two-adic generators and the shift with their proofs (CompStark/Mont32/BaseField.lean); its field structure is CompPoly's, so CompPoly's fast quartic extension Ext4 p over any Binomial4 p is a challenge field (CompStark/Mont32/Challenge.lean). KoalaBear (CompStark/KoalaBear/Field.lean: Plonky3's shift 3 and TWO_ADIC_GENERATORS, two-adicity 24) and BabyBear (CompStark/BabyBear/Field.lean: Plonky3's shift 31 and TWO_ADIC_GENERATORS, two-adicity 27) are instances, with their quartic extensions; KoalaBear's quintic one is a challenge field too (CompStark/KoalaBear/Challenge.lean). Plonky3's primitives over any base field with Poseidon2 instances, the duplex challenger, the Poseidon2 Merkle hashes, poseidon2, verify and the specification prover prove, live in CompStark/Plonky3/, and the JSON proof format of Montgomery fields in CompStark/Mont32/Json.lean; Plonky3's proofs over BabyBear verify and are reproduced like KoalaBear's (tests/CompStarkTests/BabyBear.lean). The fast backend and the completeness proof are generic too (below); the concrete numbers (CompStark/Calculator/Security.lean) are KoalaBear's.
Fast prover backend (CompStark/Stark/Fast.lean), over any 32-bit Montgomery field FastField p with its domains (Mont32BaseField p), any CompPoly fast extension of it (FastExt p EF, of any degree d and monic modulus, with its algebra id Mont32.AlgebraId EF and its inversion of coordinate planes PlanesInv p EF: the quartic extensions Ext4 p of Binomial4 p, KoalaBear's quintic KoalaBear.Fast.Ext5), Poseidon2 instances (Poseidon2Field) with permutations of packed groups of eight states (PackedPoseidon2 p, CompStark/Poseidon2/PackedField.lean; KoalaBear's vectorized kernels, or any field's implementation state by state, PackedPoseidon2.ofLanes) and CompPoly's compiled coset LDE kernels. Each field instantiates it in the CPU-targeted native library, where the compiler specializes the generic code with the field's Montgomery constants as immediates: CompStark/KoalaBear/Fast.lean and CompStark/BabyBear/Fast.lean (backendFor; over KoalaBear on any Poseidon2 instances Instances.backendFor, correct by Instances.prove_fast). proveWith runs on a Backend of kernels: the transcript's permutation and grinding, low-degree extension, the Merkle digest layers, row access, the quotient values, and the openings: the opened values and, for the batching challenge α drawn after them, the rows batched by powers of α (Backend.openings). The fast backend keeps matrices as packed Montgomery words by columns, in blocks of the trace's height (PMat), uses the packed Poseidon2 (eight grinding candidates per permutation as Plonky3, in parallel waves), CompPoly's coset LDE with plans and quotient tables prepared per instance shape (backendFor logBlowup shapes), column by column (ldeColumns: ranges of 256 rows of the trace transposed into columns, every column extended into its blocks, no transpose or join of the output; columns of $2^{20}$ rows and more in columnChains chains of tasks, so that the columns extended at once stay within the caches), the quotient values as coordinate planes in the extension's bit-reversed order, the order the quotient evaluates its rows in (Backend.Q, QRel), every coordinate of every quotient chunk extended by a task of its own from its column, gathered from its plane by bit reversal (chunksWith, chunksWith_rel), the packed Merkle tree, which commits to matrices of mixed heights by hashing the tallest ones' rows side by side, eight rows per packed group loaded from the columns by one vectorized load per block of sixteen columns, a partial block's other coordinates loaded from the group itself (Merkle.Packed.hashColumns, CompStark/Merkle/PackedColumns.lean), and injecting each smaller height into the layer of its height with one more packed compression (commitLayers; commitLayers_eq proves it is the specification's tree), CompPoly's vectorized word kernels (Montgomery.Native32.Words, CompPoly/Fields/Montgomery/Native32Words.lean, four products summed in 64 bits and reduced once per word, Words.mulAdd4: the opened values dot every column with the barycentric weights, and the batched rows multiply-add four columns at a time into four coordinate planes at a time, every column word read once per four planes, a last group of fewer planes one plane at a time (Words.mulAdd4Into), Words.mulAdd4x4Into), the openings' stored points and inverse denominators 1 / (z - x) computed once per point on the tallest height, whose prefixes are the smaller heights', for both the opened values, every matrix's in a task of its own, and the reduction (denoms, DenomsOk), and the reduction summing per point its matrices' batched rows and values, one product by 1 / (z - x) per point and row (reduceRange), FRI's folds of any arity as one kernel (Backend.fold, Fri.foldOnce: arity 2 on planes with the inverses of 2 x of every layer computed once per backend (foldTables, invTwoX), larger arities group by group in parallel ranges, lagrange compiled with one inversion per point by the csimp lemma lagrange_eq_lagrangeFast), extension vectors as CompPoly's coordinate planes, generic over the modulus and the degree, with inverse denominators by the norm polynomial (Montgomery.Native32.ExtPlanes, CompPoly/Fields/Montgomery/Native32ExtPlanes.lean, proved in Native32ExtPlanesCorrectness.lean; inverses by the norm for the quartic, by Montgomery's batch inversion for the quintic) and parallel tasks throughout, and reproduces Plonky3's proofs like the specification backend (CompStarkBench prove fast AIR … JSON). On the representative configuration, wide 64 (64 columns, degree-3 transitions, two quotient chunks) with blowup 2, 100 queries and 16-bit query grinding, Plonky3 is faster: on a quiet Ryzen 7 3700X about 0.12 s against Plonky3's 0.11 s for $2^{16}$ rows and 0.44 s against 0.41 s for $2^{18}$ on 16 threads, 0.85 s against 0.39 s and 2.9 s against 1.59 s on one thread (medians of three interleaved rounds) (CompStarkBench prove fast wide 16 1 0 1 100 0 16, bench/rust: compstark-bench prove-bench wide 16 1 0 1 100 0 16, LEAN_NUM_THREADS=1, RAYON_NUM_THREADS=1; CompStarkBench phases quartic 16 and compstark-bench prove-trace … break the time down by phase). The fast prover produces the specification's proof: prove_fast (CompStark/Stark/Fast/Refines.lean) proves proveWith (backendFor …) params air logN words publicValues = prove EF params air logN trace publicValues for a trace given to the fast prover as row chunks of packed Montgomery words words that encode trace (encoded : RT logN air.width words trace, CompStark/Stark/Fast/Rel.lean), under explicit assumptions, for a field whose largest domains of extension elements are addressable (DomainsAddressable); KoalaBear.prove_fast and KoalaBear.prove_fast_quintic discharge it (KoalaBear.backendForQuintic, KoalaBear.verifyFastQuintic). Over the quintic extension the fast prover reproduces Plonky3's proofs (tests/data/quintic_*.json, compstark-bench stark-quintic …) and takes about 1.1 times its quartic time on wide 64 and 1.03 to 1.13 times on Keccak-f, against Plonky3's 1.05 to 1.09 and 1.00 to 1.03 (CompStarkBench prove fast-quintic wide …, CompStarkBench keccak-prove (quartic|quintic) LOG_N, compstark-bench prove-bench-quintic wide …, compstark-bench keccak-prove-bench (quartic|quintic) LOG_N; the numbers are in the README). On the input (InputOk, CompStark/Stark/Refines.lean): the trace has 2 ^ logN rows of the AIR's positive width, the AIR reads only its own columns, logN + logBlowup ≤ twoAdicity so that the extension stays within the two-adic subgroups, the quotient's chunks fit the blowup, and the extended trace and quotient are addressable by machine indices. On the run: the specification's out-of-domain point ζ (outOfDomainPoint) lies outside the base field. The last one is the interesting one: for ζ in the base field, which happens over KoalaBear with probability about $2^{-93}$, some ζ - x vanishes, and the two backends compute different garbage from batch inversion and the norm. proveWith_refines reduces the theorem to laws of the backend's kernels (Fri.Refines), each stating the shapes it needs (CompStark/Fri/Assumptions.lean) and proved in CompStark/Stark/Fast/: the transcript, with the smallest grinding witness from the parallel waves, CompPoly's LDE, every Merkle layer and opening, the quotient, the opened values with inverses by the norm, the batched reduction and the folds; the generic proof carries the shapes through the FRI commit phase (CompStark/Fri/Shapes.lean). Packed values relate to the specification's by their encoding. A backend takes the main trace in its own representation (Backend.Trace), for its extension and its permutation trace: the fast one takes row chunks of packed words, the form a parallel trace generator writes, and extends them column by column without joining them (ldeWordsWith_rel). The quotient's constraints compile once per AIR into a straight-line program (Prog.compile, CompStark/Stark/Prog.lean): a hash-consed DAG with constant folding, scheduled and allocated to registers by liveness, accumulating every constraint with the coordinates of its weight. The backend runs it on blocks of up to 1024 rows in the extension's bit-reversed order on the group machine (Prog.groupMachine, CompStark/Stark/ProgGroup.lean): the block's d accumulators and registers in one buffer, every instruction one call of a kernel that runs sixteen words at a time over the block in place, reading the block's rows copied from the extension's columns, and its next rows copied in one piece when they are consecutive, every accumulation adding the operand times the weight's d words to the d accumulators, four accumulators per pass over the block with their weights and offsets read once (Prog.accPassesS and its kin), multiplications with Plonky3's form of the Montgomery reduction (Prog.mulM: the high words of the product and of its quotient times p, subtracted; mulM_eq proves it is the field's multiplication); blocks of fewer than sixteen rows, or not a multiple of sixteen, run on the block interpreter (Prog.runBlock, CompStark/Stark/ProgWords.lean). The compiler is proved (compile_run: on a row, the program accumulates the constraints' values with their weights) and so are the group machine (runGroup_rel, CompStark/Stark/Fast/ProgGroup.lean: on every row of a block, it runs the program on the field's values) and the block interpreter (runBlock_rel), which give the quotient's law (quotientWith_rel). A program can also run as straight-line code generated for it (CompStark/Stark/ProgGen.lean): #gen_group_chunks evaluates the program during elaboration, cuts its code into chunks of about 2000 instructions, each one compiled function of kernel calls with the field's constants as immediates (group_kernels p, CompStark/KoalaBear/Group.lean), and checks each by the kernel's rfl equal to the code's run on the group machine: both reduce to the same kernel calls, so no kernel and no field arithmetic unfolds; chunks of one program can be generated in separate modules built in parallel, and #gen_group_kernel assembles them into a Prog.GroupKernel, with the program Prog.compile cs of the constraints cs it was generated from (Fast.AirKernel, evaluated once). backendFor kernels checks once that each kernel's code is its program's (checkedKernels), takes an AIR's program from the kernel generated for its constraints instead of compiling them, and runs any other program by the kernel whose code it is (kernelFor), the proofs unchanged (prove_fast and proveBatch_fast hold for any kernels). The Keccak fixture's kernel (fixtures/CompStarkFixtures/KeccakKernel.lean, 19 chunks in four modules) is checked against the AIR's program and used by the Keccak example's proof test and benchmarks. verifyFast (CompStark/Stark/Fast/Verify.lean; KoalaBear.verifyFast, KoalaBear.Instances.verifyFast) is Plonky3's verifier on a 32-bit Montgomery field with packed Poseidon2 kernels, computed faster and proved equal to verify (verifyFast_eq): the leaves of every Merkle multi-opening are hashed eight at a time in packed groups, and a query's batched quotient ∑ αⁱ (pᵢ(z) - pᵢ(x)) / (z - x) of a matrix is (∑ αⁱ pᵢ(z) - ∑ αⁱ pᵢ(x)) / (z - x), the opened values' sums computed once for all queries and the row's by multiplications by base elements.
AIR fingerprints, the Keccak fixture and Plonky3's Keccak example. Air.fingerprint (CompStark/Stark/Fingerprint.lean) evaluates every constraint and every lookup of an AIR at one point of the quartic extension drawn from SplitMix64 and hashes them with the AIR's shape by Plonky3's Poseidon2 sponge, with a JSON report of one constraint per line; compstark-bench fingerprint AIR LOG_N (bench/rust/src/fingerprint.rs) computes the same from any Plonky3 Air through upstream's symbolic builder, and the tests match the example AIRs and Plonky3's KeccakAir (2633 columns, 3182 constraints) line for line. Plonky3's Keccak AIR is a fixture of the tests and benchmarks (fixtures/CompStarkFixtures/Keccak.lean); its traces are Plonky3's, as data. Trace generation is Clean's: Clean's CompStark backend (backends/compstark) proves its own keccak-air component, Plonky3's layout and constraints proved sound against Keccak-f, with CompStark from Clean's packed trace, and its keccak-air showcase checks the trace, the quotient kernel and the proofs against Plonky3's and benchmarks whole proofs. Plonky3's example prove_prime_field_31 for Keccak-f over KoalaBear with Poseidon2 Merkle hashes uses caps of height 3 and the Poseidon2 constants new_from_rng_128 draws from SmallRng seeded with 1; the example binary does not write its proof, so compstark-bench keccak-example L DIR reproduces its configuration from the same upstream functions and writes the proof, whose postcard size equals the binary's reported Proof size (1027222 bytes at L = 6), with its inputs and trace. The verifier accepts it, and the fast prover, with the AIR's generated quotient kernel, and the specification prover reproduce it from Plonky3's trace (tests/CompStarkTests/Keccak.lean). End to end at the example's configuration (blowup 2, arity up to 8, 87 queries, 16 bits of query grinding and 10 of batching grinding, caps of height 3), in Clean's showcase on a shared Ryzen 7 3700X (8 cores, 16 threads), against Plonky3 built for the native CPU: proofs from the trace take 0.82 s against Plonky3's 0.82 s for $2^{15}$ rows, 1.90 s against 1.85 s for $2^{16}$, 3.81 s against 4.60 s for $2^{17}$ and 6.46 s against 11.24 s for $2^{18}$ on 16 threads, and about 1.5 times Plonky3's time on one thread (12.2 s against 7.9 s for $2^{16}$); the process peaks at 1.4 GB, 2.4 GB, 4.4 GB and 8.4 GB of memory on $2^{15}$ to $2^{18}$ rows against Plonky3's 0.7 GB, 1.4 GB, 2.8 GB and 5.5 GB; the fast verifier takes about 45 ms against Plonky3's 11 ms. The prover's work does not depend on the trace's values, so CompStark times the phases of a Keccak proof on a pseudorandom trace of the AIR's width (keccakShapedTrace). By phase on 16 threads at $2^{16}$ (CompStarkBench keccak-phases quartic 16): the trace's extension 0.52–0.56 s, its commitment 0.83 s, the quotient 0.33 s and the openings 0.28–0.29 s (opened values 0.10 s, batched rows 0.09–0.10 s, commit phase 0.04 s), against Plonky3's 1.43 s to commit to the trace, 0.25 s for the quotient and 0.13 s to open (compstark-bench keccak-prove-trace 16). The commitment's cost is the width-24 Poseidon2 permutation, about 1.3 times Plonky3's: the commitment alone takes about 0.44 s and 0.86 s on 16 threads for $2^{15}$ and $2^{16}$ rows and 3.0 s on one thread for $2^{15}$, against about 0.30 s, 0.62 s and 2.15 s for Plonky3's Merkle tree on the same extensions (compstark-bench merkle LOG_H 2633). The extension's cost is CompPoly's NTT; the trace is transposed for its extension in ranges of 256 columns that are freed as they are extended. The benchmarks: CompStarkBench keccak-phases (quartic|quintic) LOG_N, CompStarkBench lde LOG_N 2633 REPS, CompStarkBench openings-phase (wide|keccak) LOG_N REPS (the values at the out-of-domain points and the batched reduction of the trace's extension and two quotient chunks), CompStarkBench quotient-phase keccak LOG_N REPS, and compstark-bench keccak-prove-trace LOG_N for Plonky3's phases.
Completeness (CompStark/Complete/Stark.lean): over any base field with Poseidon2 instances, if a trace satisfies the AIR, the honest prover's proof verifies (KoalaBear.completeness instantiates it):
```
theorem completeness (config : ValidConfig params air logN)
    (luck : NoBadLuck EF params air logN trace publicValues) :
    air.Satisfied logN trace publicValues → publicValues.length = air.numPublicValues →
      verify params air (setup params air logN) (prove EF params air logN trace publicValues)
        publicValues = .ok ()
```
The verifier checks that there are as many public values as the AIR declares (Air.numPublicValues), as Plonky3 does. air.Satisfied (CompStark/Stark/Satisfied.lean) says the trace is a 2 ^ logN × width matrix on whose rows every constraint vanishes, with Plonky3's selector values there. ValidConfig collects the conditions on the configuration, checkable before proving: the constraints read only the AIR's columns (a next row only if the AIR declares it reads it), the preprocessed trace has 2 ^ logN rows of the AIR's preprocessed width, the periodic columns' periods are powers of two dividing 2 ^ logN, the constraints' degrees fit the quotient's chunks (Air.DegreeFits, which counts the transition selector as degree 1 where Plonky3's degree_multiple counts 0), the extended trace domain is a two-adic subgroup of the base field, the chunks fit the blowup, which is positive, FRI folds at least once per round down to a final polynomial no longer than the trace, and makes at least one query. NoBadLuck collects the two unlikely events in which the honest run fails: the out-of-domain point ζ lands in the base field (probability $p^{1-d}$ for an extension of degree $d$, about $2^{-93}$ for the quartic and $2^{-124}$ for the quintic one), or a proof-of-work search finds no witness, which the transcript records (proveTranscript, where Plonky3's grinder would panic). The proof (CompStark/Complete/) replays the prover's transcript in the verifier; the honest Merkle openings verify through the VCVio bridge; the batched DEEP quotients of the committed low-degree extensions are low degree and the verifier recomputes them at each query; FRI's folds keep low degree, for inputs of mixed heights, and each query's folds replay the prover's down to the final polynomial; and the quotient's chunks recompose at ζ to the folded constraints over Z_H(ζ). The theorem holds for every challenge field EF with a Challenge instance (CompStark/Stark/Challenge.lean), such as KoalaBear.Fast.Ext4 and KoalaBear.Fast.Ext5. Soundness: see below.

On the interaction layer (CompStark/Iop/StarkCompleteness.lean), the honest prover of a satisfying trace (Iop.Setup.honestProver: the trace's and the quotient chunks' extensions onto L and their polynomials' values at ζ and ζ ω_n) is accepted by the oracle protocol on every execution whose out-of-domain point ζ avoids the base field (Iop.Setup.completeness, for a ValidConfig): the honest quotient makes the check at ζ hold, and DEEP quotients of codewords are codewords (deepWord_mem_code). FRI runs in Plonky3's coordinate, on the subgroup ⟨ω⟩ whose coset L is (Setup.friDomain); its codes there are those on L.
Knowledge soundness (CompStark/Iop/StarkSoundness.lean), of the STARK as an oracle protocol on ArkLib's interaction layer (CompStark/Iop/Stark.lean, on the setups and checks of CompStark/Iop/StarkSetup.lean): the protocol behind verify with oracles in place of the Merkle commitments and uniform challenges in place of Fiat–Shamir. The prover's first message is the trace length, a public move the verifier admits (Statement.Length), so that every later shape is a function of it; then the trace oracle, α, the quotient oracle, ζ, the claimed values in the clear, the batching challenge, and ArkLib's FRI on the batched DEEP word along Plonky3's schedule (Fri.Interaction.protocol, Setup.friSchedule). The verifier holds the extension of the AIR's preprocessed trace as words of its own (Setup.preprocessedWord), reads the DEEP word at a point through a query program on the trace and quotient oracles (Setup.readDeep), and accepts if FRI accepts and the constraints hold at ζ. The prover is any strategy; an Iop.Prover, words and messages as functions of the challenges, plays with FRI's honest prover (Prover.strategy) and is accepted on every run where its claimed values pass the check and its DEEP word has low degree (Prover.strategy_accepts). The extractor list-decodes the committed trace: closeTraces are the traces whose columns are polynomials of degree at most n agreeing with the committed words on a common set of (1 - δ') N points. FRI tests proximity δ, and the extractor list-decodes at δ' ≥ δ. Statement.farAcceptance is the probability that the verifier accepts while no trace close to the committed one satisfies the AIR at the claimed length:
```
theorem knowledgeSoundness (C : Statement F) (publicValues : List F)
    {OutP : (C.protocol EF).tree.ExecutionPath → Type}
    (prover : Interaction.Oracle.Prover.Strategy unifSpec (C.protocol EF).tree
      (C.protocol EF).roles OutP)
    (δ δ' : ℕ → NNReal) (hδ' : ∀ n, C.Admits n → (δ' n : ℝ) < 1 - C.rate) :
    C.farAcceptance EF publicValues δ' prover ≤ C.knowledgeError EF δ δ'
```
The statement (Statement: FRI parameters and an AIR reading only its columns) has no trace length: the prover claims one the verifier admits (Statement.Admits: SoundConfig, the verifier's checks on the length and the parameters, and the preprocessed trace's length) and the protocol is the STARK there (Statement.setupAt), and the bound is the largest knowledge error over the admitted lengths (Statement.knowledgeError), every admitted length covered, FRI's unfolded one included. The proof is a round-by-round knowledge certificate (CompStark/Iop/StarkKnowledge.lean): the doomed-transcript states of CompStark/Sound/Rbr.lean for α, ζ and a (AlphaBad, ZetaBad, BatchBad, each with its error term below), with the trace oracle mapped to the extracted trace, appended with KnowledgeCertificate.append to ArkLib's FRI certificate on the DEEP word (Fri.Interaction.certificate), gated by the constraint check at ζ (gateCertificate); ArkLib's executeStrategies_extraction_le turns it into the bound at each length (Setup.extraction_le_knowledgeError), and whatever length the prover sends, the certificate there bounds the rest. FRI's error is ArkLib's (friErrorWith_eq). The knowledge error at a length (CompStark/Iop/StarkError.lean) has one term per challenge, with ℓ the list sizes of the committed words' interleaved codes at δ' (Setup.listSize): ℓ (#constraints - 1) / |𝕂| for α, (ℓ · identityDegree + n + N) / |𝕂| for ζ (Schwartz–Zippel on the constraint identity of each candidate of the committed words, and ζ landing on the trace domain or on L, where the DEEP quotients divide by zero, and so then does ζ ω_n, L being a coset of a group holding ω_n; decoding finds the trace, permutation trace and quotient polynomials on one common set, so the candidates are those of the committed words as one family, Setup.Committed, and the term is linear in the list size, as in Haböck's DEEP-ALI analysis, https://eprint.iacr.org/2022/1216, Theorem 8), the correlated-agreement error of the powers of the batching challenge (the batched word δ-close although the words are not on a common set at δ'; for δ ≤ δ' at most the mutual correlated-agreement error at δ, batchingError_le_mcaError), and FRI's soundness error at δ (Fri.Interaction.error, the error of ArkLib's interaction-layer FRI certificate, from ArkLib's FRI query and folding analysis of ArkLib#992, after Garreta–Mohnblatt–Wagner, with injected inputs). FRI's tree is Plonky3's commit phase: each fold round is the prover's word at the layer, the first being the batched DEEP word, then the folding challenge; the last layer has no word, only the final polynomial; and each query checks every committed word against the verifier's word there, the DEEP word computed from the trace and quotient openings at the first layer and the fold of the previous committed word after. The theorem holds for every δ and every δ' below 1 - rate; the error is small up to the Johnson bound 1 - √rate, where the list sizes are, and below the unique-decoding radius ℓ ≤ 1 (listSize_le_johnson, listSize_le_one, CompStark/Sound/Johnson.lean). Concrete security (CompStark/Calculator/Security.lean): for the Fibonacci AIR with blowup 16, FRI folding by arity 2 and 110 queries, at every trace length the verifier admits (up to $2^{20}$ rows), the knowledge error with FRI at δ = 15/32 - 2^{-15} and the extractor at δ' = 15/32 - 2^{-19}, below the unique-decoding radius $15/32$, is at most $2^{-98}$ (fibonacci_knowledgeError_le, about $2^{-98.95}$ exactly on $2^{20}$ rows, $2^{-100.37}$ on $2^{10}$). Batching all opened words by powers of one challenge needs correlated agreement for curves: ArkLib bounds it by k · N / |𝕂| below the unique-decoding radius (ProximityGap.exists_exactPowerAgreement_unique with ProximityGap.mcaError_powers_le_of_exactPowerAgreement, on [BCIKS20] Theorem 6.1 for curves; McaBound.uniqueDecoding_holds), and with a proximity loss δ < δ' the error is independent of N (batchingError_le_curve, from ArkLib's CodingTheory.UniqueDecoding.card_goodCoeffs_le). FRI's folds use the same argument through lossy correlated agreement, at any arity: friError is the lossy FRI error at the best proximity loss, and a fold by $2^k$ onto a domain L' costs (2^k - 1) min(B, |L'|) / |𝕂| (one more word if it injects an input), with B = max(T₁, δ_int / loss) independent of |L'| for δ ≤ (1 - rate) / 2 - 1/|L'| and the powers MCA bound |L'| otherwise (friErrorWith_le, lossyLevel_le, from ArkLib's CodingTheory.UniqueDecoding.lossyMcaError_le), at the price of #folds · loss in the query term. With it, wide 64 (64 columns, degree-3 constraints, 136 opened words) with blowup 4, arity 2 and 150 queries has knowledge error at most $2^{-98}$ at every admitted length, up to $2^{22}$ rows, with FRI at δ = 3/8 - 2^{-12} and the extractor at δ' = 3/8 - 2^{-14} (wide_knowledgeError_le, about $2^{-98.71}$ exactly on $2^{22}$ rows, $2^{-100.17}$ on $2^{20}$), dominated by the out-of-domain term (identityDegree + n + N) / |𝕂|, about $2^{-98.95}$ on $2^{22}$ rows, and FRI's queries. Since that term grows with the list size, the extractor stays below the unique-decoding radius at this size. Every term but the queries is an integer over $|\mathbb{K}|$, so the quartic extension ($p^4 \approx 2^{124}$) caps every configuration near 100 bits at these sizes (the interactive error cannot credit grinding, which only costs a prover that pays for its oracle calls; on Plonky3's verifier below, grinding lifts the cap to about 118 bits per duplex call); the analysis is generic in the extension field, and over the quintic one ($p^5 \approx 2^{155}$) wide 64 with blowup 4 and 190 queries has knowledge error at most $2^{-128}$ at every admitted length (wide5i_knowledgeError_le, about $2^{-128.22}$ on $2^{22}$ rows). The non-interactive verifier is covered in the random-oracle model, next. State restoration (CompStark/Iop/StarkStateRestoration.lean, CompStark/Iop/BatchStateRestoration.lean): the STARK and the batch STARK are public-coin (Statement.publicCoin: the lengths the prover's first move, every challenge with one continuation, FRI's presentation Fri.Interaction.publicCoin appended), their certificates with uniform query positions sample every challenge uniformly, and the verifier's checks are a program of the branch (Statement.terminal). ArkLib's KnowledgeCertificate.stateRestoration_extraction_le then bounds the state-restoration game, where the adversary queries a random oracle for each challenge at its erased prefix and chooses the public values and every message: the checks pass while no trace of the claimed length close to the committed one satisfies the AIR with probability at most Q · maxError + sumError of the node errors (Statement.stateRestoration_le): at each length the folding, out-of-domain and batching errors, each FRI fold's error and FRI's query error at the length's proximity loss, whose path sum is the interactive error at that loss (Statement.pathError_nodeErrors). For the batch, a node's error is the largest over the instances (Batch.Setup.nodeErrors). The random-oracle theorems below are proved directly on Plonky3's verifier and do not go through this game.
Knowledge soundness of Plonky3's verifier as it runs (CompStark/Fs/StarkBcs.lean), from ArkLib's BCS theorem (KnowledgeCertificate.bcs_knowledge_soundness): verifyWith itself, with Merkle commitments, Fiat–Shamir and grinding, run on random oracles in place of Poseidon2's three roles (CompStark/Fs/RandomOracle.lean): the duplex challenger, which takes the capacity and the elements observed since the last squeeze and answers a new capacity and K samples; the Merkle leaf hash; and the compression. The statement is a Statement, FRI parameters and an AIR with no trace length: the verifier takes the length from the proof, as Plonky3's does, and the theorem covers every length it admits (Statement.Admits), with the STARK at each (Statement.setupAt). The game (Statement.starkGame) computes the verifying key of the AIR's preprocessed trace on the oracles, runs an adversary that outputs public values and a proof, and runs Plonky3's verifier on them, all against one logged lazy random oracle (ArkLib's Bcs.realImpl, the verifier's oracles read as a duplex chain and two Merkle hashes by translate, CompStark/Fs/HashChain.lean). The extractor reads the trace off the log's hash answers under the proof's trace commitment (traceMessageOf, merkleCache, hashCacheOf):
```
theorem knowledgeSoundness_bcs (h8 : 2 ^ 8 ≤ Nat.card F) (h64 : twoAdicity F < 2 ^ 64)
    (hK : 0 < K) (δ δ' : ℕ → ℝ≥0) (hδ' : ∀ n, C.Admits n → (δ' n : ℝ) < 1 - C.rate)
    (loss : C.Length → ℝ≥0) (adversary : OracleComp (spec F K) (List F × Proof F EF)) {Q q : ℕ}
    (hQ : IsQueryBoundP adversary (fun t => isDuplex t = true) Q)
    (hq : IsTotalQueryBound adversary q) :
    Pr{let z ← (simulateQ Bcs.realImpl
        (simulateQ translate (C.starkGame EF K adversary))).run []}[
      z.1.2.2.2 = .ok () ∧ ∀ h : C.Admits z.1.2.2.1.degreeBits,
        ∀ trace ∈ closeTraces (C.setupAt EF _ h) (δ' z.1.2.2.1.degreeBits)
          ((C.setupAt EF _ h).traceWords ((C.setupAt EF _ h).traceMessageOf
            (merkleCache (Bcs.hashCacheOf z.2)) z.1.2.2.1.traceCommit)),
        ¬ C.air.Satisfied z.1.2.2.1.degreeBits trace z.1.2.1] ≤
      chainError (Digest F) (Q + C.verifierQueries EF + 3 * C.verifierChainQueries EF K) +
        hashBadError F (2 ^ C.params.capHeight) (C.capOffsets EF).length
          (q + C.verifierQueries EF) +
        (maxError (fun (_ : C.Input) node ↦
            C.ratio EF node * C.nodeErrors EF δ δ' loss (1 / Nat.card F) node) *
            (Q + C.verifierQueries EF + 3 * C.verifierChainQueries EF K : ℕ) +
          sumError (fun (_ : C.Input) node ↦
            C.ratio EF node * C.nodeErrors EF δ δ' loss (1 / Nat.card F) node))
```
The protocol is the STARK's public-coin presentation with every challenge drawn as Plonky3's verifier draws it (Fs/Draws.lean: extDraw for an extension element, after a grinding sample if the round grinds and with no witness at 0 bits, queryDraw for the query positions, each the low bits of one sample), from the answers of the challenge's squeezes, K samples each: a challenge needing more samples than one squeeze holds squeezes again with the empty input. Its layout (Setup.layout, Statement.layout, CompStark/Fs/Stark.lean) is what the verifier observes before each challenge, as Plonky3 observes it: the domain separators, the public values, the claimed values, the final polynomial, the grinding witnesses, and each committed word's Merkle cap, 2 ^ min capHeight depth digests, opened to the word read off a snapshot of the hash answers under it (merkleCache, StarkWords.lean). The observations are prefix-free (Statement.layout_prefixFree) through the domain separator's length bytes (DomainSeparator.starkSeedOf_inj, which needs the challenger's byte chunks of ⌊log₂ p / 8⌋ ≥ 1 bytes and lengths within the domain separator's eight bytes: h8, h64). Each draw is bounded by its ratio against the law the knowledge certificate samples at its node (Statement.bounded_decoder): the grinding's powFraction F bits, with FRI's query positions drawn from the law Plonky3's verifier draws them from, the low bits of uniform base elements (Setup.queryPositions, slack 1/p), so the positions' bias is paid inside the query error, (1 - δ + #folds · loss + 1/p) ^ numQueries. The node errors are the state-restoration theorem's (Statement.nodeErrors), each times its draw's ratio.

The BCS theorem's adversary runs the game with its own log, reads the proof's selection off it (Statement.parse, CompStark/Fs/StarkParse.lean) and fills its snapshots from the log (Statement.bcsAdversary). On a run without digest clashes (HashBad: a hash answer equal to a digest known before it), extraction under an absorbed cap is the same from the cap's snapshot and from the whole log (extractRow_snapshotAt, CompStark/Fs/MerkleLog.lean, opensStable_parse), and an accepted opening opens the extracted rows (capBinding_of_log), so the verifier's acceptance gives the STARK's terminal on the extracted words (Setup.terminal_of_verifyWith, CompStark/Fs/StarkTerminal.lean) while a far trace makes the extraction fail (Statement.bcsEvent_of_mem_support). Digest clashes cost hashBadError F capLen m q = (2 + m capLen) q² / |F|⁸ (prEvent_hashBad_le), m the offsets at which the verifier's inputs carry caps (capOffsets, twoAdicity F + 3 of them) and capLen = 2 ^ capHeight; the capacities' collisions and predictions cost ArkLib's chainError (Digest F) Q' = ⌊Q' (Q' + 1) / 2⌋ / |F|⁸. verifierQueries counts the setup's and the verifier's oracle calls on a proof of any length (verifierCallsAt, isTotalQueryBound_verifyWith, CompStark/Fs/StarkCalls.lean), the setup's 2 · |L| - 1 calls none without preprocessed columns, and verifierChainQueries the duplex calls of the verifier's completion, at most maxChallenges = twoAdicity F + 4 challenges (Setup.challengesLE_publicCoin) of at most coinCount squeezes each, which the BCS theorem's adversary runs once and ArkLib's simulation charges twice more, hence Q' = Q + verifierQueries + 3 verifierChainQueries. The theorem does not cover Poseidon2 itself or Plonky3's sponge and duplex constructions (rate/capacity chaining, length-tagged absorption, no padding): it idealizes each role of the hash as a random oracle.

Each node error times its ratio is one of the security calculator's round terms (below; Setup.ratio_mul_nodeErrors_le, CompStark/Calculator/FiatShamir.lean), so the round error's bound (Statement.roundErrorBound) is the error per duplex call, and a path of at most maxChallenges challenges sums to at most maxChallenges times it: the calculator's C.SecureRo EF p B A bits gives chainError Q' + hashBadError + (Q' + maxChallenges) · 2 ^ (-bits) (Statement.knowledgeSoundness_bcs_of_secureRo), which Statement.bcsBound evaluates with the round error's bound in place of 2 ^ (-bits). The verifier's duplex calls count both in Q' and in the path sum. Per duplex call, Plonky3's Keccak example has 52.11 bits on 2 ^ 23 rows, wide 64 with wideGrindParams 117.37, and with SP1's parameters 98.95 at its longest admitted length; at Q = q = 2 ^ 64 calls and K = 8, the bounds are about $2^{-53.37}$ for wideGrindStatement, $2^{-34.95}$ for SP1's parameters and $2^{-64.49}$ for wide5Statement, Q' times the per-call error dominating the capacities' $2^{-120.91}$ and the digest clashes' $2^{-115.05}$. tests/CompStarkTests/Security.lean instantiates the theorem at 117 bits (wideGrind_knowledgeSoundness_bcs), and tests/CompStarkTests/KeccakSecurity.lean for Keccak at 128 and, beyond the unique-decoding radius, 100 bits (knowledgeSoundness_bcs_quintic, johnson_knowledgeSoundness_bcs_quintic).
Batch-STARK prover and verifier (CompStark/Batch/, CompStark/Plonky3/Batch.lean): Plonky3's batch-stark prove_batch and verify_batch at revision a4982ec, LogUp lookups included: several AIR instances (Batch.Instance: an AIR, its trace length and its lookups, packed at keygen, Instance.ofAir) of mixed heights, with preprocessed and periodic columns, under one main commitment, one quotient commitment and one opening argument over matrices of mixed heights. The common data (Batch.Common, setupBatch, Plonky3's CommonData) is the cap of one commitment to all preprocessed traces with every instance's keygen height and packed lookups. The transcript is Plonky3's typed one for p3-batch-stark (DomainSeparator.batchSeed: every instance's degree bits observed as extension elements, the out-of-domain grinding step present at zero difficulty too). The verifier (verifyBatchWith, CompStark/Batch/Verifier.lean) takes the AIRs and the common data, and, as Plonky3's, every instance's trace length from the proof (instancesOf): it checks that an instance with preprocessed columns has its keygen height (keyOk, Plonky3's preprocessed metadata), then every instance as uni-stark does at the proof's heights, against one α and one ζ, with Plonky3's shape checks (verifyInstancesWith). LogUp lookups follow Plonky3's single-terminal gadget (CompStark/Lookup/): an AIR declares its lookups (Air.lookups, Lookup: tuples of expressions with signed multiplicities, each with its weight (Count), local or on a named bus), and keygen fixes the batch's layout in the common data: same-bus lookups packed into shared fraction columns within the quotient's degree budget (Air.packedLookups, pack_same_bus_with_degree), one tuple width per lookup and per bus and the multiplicity bound ∑ᵢ wᵢ nᵢ < p at the proof's heights checked (widthsOk, heightBoundOk), and one challenge pair (α_L, β_L) for the batch, bus b separated by the base α_L + (b + 1) β_Lᵂ (challengeLayout). After lookup grinding and the pair, the prover commits to every permutation trace, an accumulator and a fraction column per lookup over the challenge field in base coordinates (permutationTrace), and observes the terminals; each instance's LogUp constraints (logUpConstraints, expressions over the traces, the permutation columns, the challenges and the terminal, ExtExpr) follow its own in Horner's order, its quotient chunks sized by both (Instance.logQuotientChunks), the permutation traces open at ζ and ζ ω, and the verifier checks that the terminals sum to zero. On Plonky3's batch proofs of the test AIRs of batch-stark/tests/simple.rs (three instances of mixed heights, mixed preprocessed columns, a periodic AIR, a single instance, and preprocessed traces of mixed heights with and without next-row reads, and an AIR that does not read the next row; with lookups, MulAirLookups, FibAirLookups and SingleTableLocalLookupAir: local lookups, global buses across instances of mixed heights, packed same-bus lookups, lookup grinding, and two unbalanced batches; and a range table with its queries; tests/data/batch_*.json), the verifier accepts them, rejects them tampered, with other degree bits, with reordered instances, against other preprocessed traces, with a tampered, missing or spurious terminal or permutation opening, and the unbalanced ones by the terminals' sum, and the specification prover proveBatch reproduces them exactly. The fast prover reproduces them too, over KoalaBear and over BabyBear (tests/data/babybear_batch_*.json), and KoalaBear.proveBatch_fast proves it is the specification: proveBatchWith (backendFor params.logBlowup (Batch.shapes instances)) params instances traces publicValues = proveBatch (Ext4 p) params instances traces publicValues for one list of public values per instance, when ζ (Batch.batchOutOfDomainPoint) lies outside the base field, on batches of the prover's shapes (Batch.InputOk, CompStark/Batch/Refines.lean: at least one instance, every trace's InputOk, every instance's lookups reading only its AIR's columns, and the extensions addressable side by side at the tallest height); Batch.proveBatchWith_refines reduces it to the same backend laws as uni-stark, every instance's quotient by uni-stark's argument (batchQuotientChunks_refines), plus two LogUp kernels. The fast backend generates every permutation trace block by block (Fast.permutationWords), the lookups' expressions one compiled program (Prog.compileOuts) and the fractions on planes of extension coordinates: every denominator α - ∑ⱼ tⱼ βᵏ⁻¹⁻ʲ inverted through the norm N(d) = g₀² - W g₁² with one zero-safe batch inversion per tuple and block (invPlanes_rel), blocks of up to 1024 rows, each block's rows the transpose of its planes (rowsOfColumns), the accumulator's planes the running sums of the rows' fractions coordinate by coordinate (blockRows_eq), in parallel ranges of blocks with the accumulator from the range's start, then shifted by the sums before it (assembleRanges_eq); it extends the words with CompPoly's coset LDE, and permutationLdeWith_rel (CompStark/Stark/Fast/Permutation.lean) proves the extension and terminal are the specification's (permutationLdeOf). The LogUp constraints compile like the AIR's into a program over the extension's base coordinates, every extension node d coordinate nodes and products by their convolution reduced by the table of Xᵏ mod f (Prog.compileExt, over CompPoly's ExtensionParams of the extension), every coordinate j of constraint k accumulated with the weight Xʲ α^(K-1-k), and run on the same blocks (Fast.lookupQuotientWith, lookupQuotientWith_rel in CompStark/Stark/Fast/LookupQuotient.lean). On three wide 64 tables of $2^{20}$, $2^{19}$ and $2^{16}$ rows with blowup 2, 100 queries and 16-bit query grinding, the fast batch prover takes about 3.2 s against 2.0 s for Plonky3's prove_batch on 16 threads, and 15.0 s against 9.6 s on one thread; on a lookup batch with the same parameters (mulAirLookups 8 on $2^{18}$ rows with local lookups and eight sends on a global bus, fibonacciLookups receiving them on $2^{18}$ rows, and mulAirLookups 8 with local lookups on $2^{16}$ rows), it takes about 1.22 s against 0.57 s on 16 threads, and 6.8 s against 3.4 s on one thread (medians of three interleaved rounds on a quiet Ryzen 7 3700X, Plonky3 built for the native CPU; CompStarkBench prove-batch 1 0 1 100 0 16, CompStarkBench prove-batch-lookup 1 0 1 100 0 16, bench/rust: compstark-bench batch-bench wide 1 0 1 100 0 16 and batch-bench lookup-bench 1 0 1 100 0 16, LEAN_NUM_THREADS=1, RAYON_NUM_THREADS=1). By phase on 16 threads on the wide 64 batch (CompStarkBench phases-batch): the traces' extension 1.09 s, their commitment 0.66 s, the quotients 0.31 s, the quotient chunks' extension 0.74 s and commitment 0.36 s, the opened values 0.24 s, the batched reduction 0.40 s and FRI's commit phase 0.31 s, against Plonky3's 0.83 s for its commit phase (compstark-bench batch-trace wide …). Every instance with lookups computes its permutation trace and its extension in a task of its own from the backend's trace, for the fast backend its row chunks of packed words (permutationsWith, Backend.permutation).
Completeness of the batch STARK (CompStark/Complete/Batch.lean): over any base field with Poseidon2 instances, if every instance's trace satisfies its AIR, every bus balances and the multiplicities stay below the characteristic, the honest prover's batch proof verifies against the batch's common data (KoalaBear.batchCompleteness instantiates it):
```
theorem Batch.completeness (config : Batch.ValidConfig params instances)
    (luck : Batch.NoBadLuck EF params instances traces publicValues) :
    Batch.Satisfied instances traces publicValues →
      verifyBatch params (instances.map (·.air)) (setupBatch params instances)
        (proveBatch EF params instances traces publicValues) publicValues = .ok ()
```
Batch.Satisfied gives one trace and one list of public values per instance, every trace satisfying its AIR (Air.Satisfied) with as many public values as the AIR declares, every bus balanced (Batch.Balanced: for every bus and tuple of values, the multiplicities of the batch's messages, Batch.messages, sum to zero in the field) and the verifier's multiplicity bound. Batch.ValidConfig asks for at least one instance and a ValidConfig for every instance, every instance's quotient, LogUp constraints included, within the blowup and its constraints within the chunks, row-local lookups reading the AIR's columns (Lookup.Fits) and one tuple width per lookup and per bus; as the instances share FRI's parameters, FRI's final polynomial is then no longer than the shortest trace; and no instance's extension lies above another's Merkle cap (capFits), since the verifier rejects matrices injected above the cap. Batch.NoBadLuck is NoBadLuck for the batch's run (batchOutOfDomainPoint, proveBatchTranscript), plus no pole: under the run's lookup challenges no tuple of non-zero multiplicity has a zero denominator (NoPoleAt, probability 1/|EF| per bus and tuple). The proof (CompStark/Complete/Batch.lean) replays the transcript and reads every instance's opened values as uni-stark's honest openings, so each instance's constraint check passes as in completeness; the opening argument over matrices of mixed heights is complete for any honest rounds (verifyPcs_openPcs, CompStark/Complete/Pcs.lean): the Merkle trees with injected matrices open honestly (verifyMulti_prune_mixed, CompStark/Merkle/Mixed.lean), the batched quotients at a query are recomputed with every matrix's row at its own height, and FRI rolls each shorter input in when its folds reach that height (verifyFri_proveFri, Sched, foldSchedule_sched). For lookups (CompStark/Complete/LogUp.lean, CompStark/Complete/LogUpQuotient.lean), the honest permutation trace satisfies the LogUp constraints on every row (logUpConstraints_honest: a fraction pin U f - V vanishes on f = ∑ m / d when no tuple of non-zero multiplicity has d = 0), its column polynomials over the spec extension make every LogUp constraint Z_H times a quotient (extPoly_eq), the prover's quotient values are the constraints' folded quotient times α ^ L plus the LogUp constraints' (toSpec_batchQuotientValues), so every instance's check passes (instanceCheck_honest), and the terminals sum to the batch's messages weighted by their denominators, zero when every bus balances (terminals_sum_eq_zero).

On the interaction layer (CompStark/Iop/BatchCompleteness.lean), a batch prover's strategy is accepted whenever the checks in the clear pass and every domain's batched DEEP word is a codeword on that domain g ⟨ω_m⟩ (Iop.Batch.Prover.strategy_accepts): a codeword on a coset is one on every coset of the same subgroup, so FRI injects each shorter word in its code (ArkLib's inputsInCode_plonky3). The honest prover of a batch's traces (Iop.Batch.Setup.honestProver: every instance's trace, permutation trace and quotient chunks extended onto its domain, its terminal, and their polynomials' values at ζ and ζ ω_n, over the specification's layout of the lookup challenges) meets both conditions: for a Batch.ValidConfig and traces satisfying the batch (Iop.Batch.Setup.Satisfied), it is accepted on every execution whose ζ avoids the base field and under whose lookup challenges no denominator vanishes (Iop.Batch.Setup.completeness, Setup.NoPole). The terminals sum to zero by terminals_sum_eq_zero, every instance's check at ζ passes by instanceCheck_honest, and every word opened on a domain is a polynomial of degree below its trace length claimed at its value (OpensLow), so the domain's batched DEEP word is a codeword (deepQuotient_mem_code). The multiplicity bound belongs to the lengths the verifier admits (Statement.Admits), not to its checks, so the theorem does not assume it.
Knowledge soundness of the batch STARK (CompStark/Iop/BatchSoundness.lean), as an oracle protocol on ArkLib's interaction layer (CompStark/Iop/Batch.lean, on CompStark/Iop/BatchSetup.lean): k ≥ 1 AIRs, instance i on 2 ^ logN i rows (Batch.Setup), each a STARK of its own (Setup.instanceSetup) on its own domain, under one α, one ζ and one batching challenge. The prover sends the lengths, every instance's trace as one oracle, the permutation traces as one oracle and the terminals of the instances with lookups (Setup.Terminals, as Plonky3's proof carries them) after the lookup challenges, the quotients after α and the claimed values after ζ. As Plonky3's commitment scheme reduces the openings by height, the DEEP quotients of the instances of each domain size are batched by the powers of the batching challenge, starting over at each size, in Plonky3's order (the main traces, the quotients, the preprocessed traces; groupDeepWord), and ArkLib's FRI runs on the tallest batched word and injects each shorter one when its folds reach that size (Setup.friHeights); the verifier reads a batched word at a point through the values of the instances of that size (Setup.readGroupDeep). The extractor outputs one trace per instance, each list-decoded from its committed trace (Batch.closeTraces), and Batch.Statement.farAcceptance is the probability that the verifier accepts while no close tuple satisfies a relation R:
```
theorem batchKnowledgeSoundness (C : Batch.Statement F) (publicValues : Fin C.k → List F)
    {OutP : (C.protocol EF).tree.ExecutionPath → Type}
    (prover : Interaction.Oracle.Prover.Strategy unifSpec (C.protocol EF).tree
      (C.protocol EF).roles OutP)
    (δ δ' : (Fin C.k → ℕ) → NNReal) (hδ' : ∀ n, C.Admits n → (δ' n : ℝ) < 1 - C.rate) :
    C.farAcceptance EF publicValues δ'
      (fun n traces ↦ (C.setup EF n).Satisfied traces publicValues) prover ≤
      C.knowledgeError EF δ δ'
```
As for the STARK, the batch statement (Batch.Statement: FRI parameters, the AIRs and their keygen heights, below) has no trace lengths: the prover claims a vector the verifier admits, and the bound is the largest knowledge error over the admitted vectors (Batch.Statement.knowledgeError). The certificate (CompStark/Iop/BatchKnowledge.lean) appends the doomed-transcript states of CompStark/Sound/BatchRbr.lean (LookupBad, then the failing instance's AlphaBad, ZetaBad and BatchBad with that instance's errors, so that each path's errors sum to its instance error) to ArkLib's FRI certificate on the batched words, gated by the terminal sum and the constraint checks.

Setup.Satisfied asks every trace to satisfy its AIR and every bus to balance in the field (Setup.Balanced, over the batch's messages Setup.messages); the extractor outputs the main traces only, the permutation traces are auxiliary. The verifier first draws the lookup challenges (α_L, β_L) and accepts only if the instances' terminals sum to zero. If every close tuple satisfying every AIR leaves a bus unbalanced, the pair is bad with probability at most lookupError: for each such tuple the messages' fractions, with every denominator α_L + (b + 1) β_Lᵂ - ∑ⱼ tⱼ β_Lʲ cleared, give a nonzero polynomial of degree at most T + (T - 1) W in (α_L, β_L) over the T interactions of width at most W, and a pole of any tuple, of zero multiplicity or not, counts as bad too (Schwartz–Zippel, CompStark/Sound/LogUp.lean, CompStark/Sound/BatchLogUp.lean); Plonky3's p3-security estimates N (W + 2) / |EF|. Otherwise the terminals of close permutation traces satisfying their LogUp constraints telescope to the messages' nonzero fraction sum (CompStark/Sound/Telescope.lean), so the verifier rejects, or some instance has no close trace and permutation trace satisfying all its constraints, and the proof runs the single STARK's argument on it among the instances of its domain's size: the DEEP quotients of that size near on a common set make that instance's near too. So the knowledge error (CompStark/Iop/BatchError.lean) is lookupError plus the worst instance's foldingError + outOfDomainError, with its own list sizes and identityDegree, and batching of its size's opened words (batchingErrorOf, decoding losing two points of its domain), plus FRI's error with the shorter words injected (friErrorWith). FRI with inputs injected mid-folding is ArkLib's interaction-layer FRI certificate: a fold that injects a word is bad when the powers of its challenge over its 2 ^ k coefficient words and the injected word make them agree with the code although they do not on a common set (the lossy correlated-agreement event of 2 ^ k + 1 words), and FRI rejects when any input is far; its error is friErrorWith (friErrorWith_eq). This covers every schedule Plonky3's verifier accepts: an instance at FRI's final length is injected by the last fold, at the final height, and with every instance there FRI does not fold and the queries check the batched words against the final polynomial (Fri.Interaction.Schedule.Fits, Fri.Interaction.Schedule.plonky3). The STARK's FRI is this FRI without injected inputs. A lookup's tuples are queries, of positive weight, or provided table entries, of weight 0 and any multiplicity (Plonky3's Count::bounded and Count::provided). Balance in the base field ℤ/p makes the queries included in what is provided: with the verifier's multiplicity bound ∑ᵢ wᵢ 2 ^ logNᵢ < p (Setup.HeightBounded), one of its checks on every length vector it admits (Statement.Admits), and AIRs keeping every row's query multiplicities within their weights (Air.CountsBounded, Plonky3's count_weight, an obligation of the AIR the verifier does not check), for every bus and tuple of values some row of some instance provides it with a nonzero multiplicity (Setup.Provides, exposing the instance and row so the provider's AIR applies there), or its queries' multiplicities, read as the integers of magnitude below p / 2 they stand for (intValue), sum to zero over ℤ (Setup.Included, Sound.Batch.included_of_balanced, CompStark/Sound/Inclusion.lean): without a provider, balance makes the queries' sum vanish modulo p, and the height bound keeps it below p in magnitude. So the knowledge error also bounds acceptance while no close tuple satisfies every AIR with lookup inclusion (Setup.SatisfiedWithInclusion):
```
theorem batchKnowledgeSoundness_inclusion (C : Batch.Statement F)
    (publicValues : Fin C.k → List F) {OutP : (C.protocol EF).tree.ExecutionPath → Type}
    (prover : Interaction.Oracle.Prover.Strategy unifSpec (C.protocol EF).tree
      (C.protocol EF).roles OutP)
    (δ δ' : (Fin C.k → ℕ) → NNReal) (hδ' : ∀ n, C.Admits n → (δ' n : ℝ) < 1 - C.rate)
    (hcounts : ∀ n, C.Admits n → ∀ i, (C.air i).CountsBounded (n i)) :
    C.farAcceptance EF publicValues δ'
      (fun n traces ↦ (C.setup EF n).SatisfiedWithInclusion traces publicValues) prover ≤
      C.knowledgeError EF δ δ'
```
A decidable check discharges Air.CountsBounded for any AIR (Air.countsChecked, sound by countsBounded_of_countsChecked, CompStark/Sound/Counts.lean): every lookup's query multiplicities have syntactic bounds summing to at most its count weight, a bound being 1 for a row selector or a boolean column, k for a constant ±k, and sums and products of bounds; a column is boolean when the AIR asserts x (x - 1) for it (assert_bool) on every row, or on transitions and on the last row, since a transition constraint leaves the last row free. The wideBus 64 batches pass it by decide (wideBus_countsChecked, CompStark/Iop/LookupInclusion.lean). A range check shows inclusion at work: range tables (rangeTable, a preprocessed row index provided on the bus range with an unconstrained multiplicity column) and range queries (rangeQuery, a value queried with a boolean multiplicity s) pass the check, and lookup inclusion puts every query with s = 1 in some table's range (rangeChecked_of_satisfiedWithInclusion, CompStark/Sound/Range.lean), so acceptance is bounded while no close tuple satisfies the AIRs with every real query in range (rangeKnowledgeSoundness, and on Plonky3's batch verifier Batch.Statement.rangeKnowledgeSoundness_bcs). Plonky3 proves such a batch (compstark-bench batch range, tests/data/batch_range_*.json), and the verifier and both provers agree with it.

Concretely, three wideBus 64 instances (wide 64 exchanging two tuples of width 4 per row on one global bus) of keygen heights $2^{20}$, $2^{19}$ and $2^{16}$ over the quintic extension, with blowup 4 and 190 queries, have knowledge error at most $2^{-127}$ at every admitted vector of lengths (wideBatch_knowledgeError_le, about $2^{-127.11}$, the largest per-vector bound, with every instance on $2^{22}$ rows and the lookup challenges about $2^{-128.04}$; at the keygen heights alone the batch reached $2^{-128.34}$). The random-oracle model of the batch follows.
Knowledge soundness of Plonky3's batch verifier as it runs (CompStark/Fs/BatchBcs.lean), LogUp lookups included: Batch.Statement.knowledgeSoundness_bcs, the same bound as the STARK's for verifyBatchWith itself on the same three oracles (CompStark/Fs/BatchRandomOracle.lean), against an adversary that outputs public values and a batch proof. The statement is a batch Statement (CompStark/Iop/BatchSetup.lean): FRI parameters, the AIRs and their keygen heights, at which their lookups are packed, with the lookups' fit to their AIRs' columns and BusesValid, properties of the keygen data; it has no trace lengths. The verifier takes every instance's length from the proof's degree bits, as Plonky3's does, and the theorem covers every vector of lengths it admits (Statement.Admits: per instance SoundConfig, the quotient domain with the lookups' LogUp constraints within the two-adic subgroups, the keygen height for an instance with preprocessed columns, and the multiplicity bound, all checked by an accepting verifier, Statement.admits_of_ok, FRI's final height included: every query folds every height down to it), with the batch at each (Statement.setupAt). The game (Statement.batchGame) computes the common data, the commitment to the instances' preprocessed traces at their keygen heights, on the oracles (Batch.commonWith), and runs verifyBatchWith on the adversary's proof against it; the extractor reads every instance's trace off the log under the main commitment, at the instance's offset among the matrices of its height (Merkle.matColumn), at the proof's lengths (Statement.lengthsOf). The lengths are told apart by the degree bits the verifier observes right after the batch's domain separator, extension elements whose first coordinate is the length, and an admitted length is at most the two-adicity, below p, so the batch needs no assumption on the field. Plonky3's verifier clamps every cap to its tree, and an accepted opening has every committed matrix at least as tall as its cap (cap_le_of_verifyMulti_mixed); the commitments bind the trees of mixed heights the prover committed to (capBindingM_of_log, Fs/MixedBinding.lean), and the verifier's checks hold for the extracted words (Fs/BatchExtract.lean), which give the batch's terminal, FRI's checks with the shorter heights injected included (Setup.terminal_of_verifyWith, CompStark/Fs/BatchTerminal.lean). verifierQueries counts the setup's calls (at most four per leaf of the preprocessed traces' tree, isTotalQueryBound_commonWith) and the verifier's on a proof of any lengths, the largest over the vectors of lengths up to the two-adicity (verifierCallsOf: a leaf hash, a compression per level and a hash and a compression per injected height for every opening of a commitment); verifierCalls_le bounds it in closed form, checked by decide +kernel. The batch has at most twoAdicity F + 5 challenges, the lookup challenges included (Batch.Setup.challengesLE_publicCoin). The calculator's certificate (Batch.Statement.SecureRo, implying the batch's SecureRo at every admitted vector, secureRo_setupAt) bounds every node (Batch.Setup.ratio_mul_nodeErrors_le; without lookups, LogUp's error is 0), so Batch.Statement.knowledgeSoundness_bcs_of_secureRo gives chainError Q' + hashBadError + (Q' + maxChallenges) · 2 ^ (-bits). Concretely, the three wideBus 64 instances above, of keygen heights $2^{20}$, $2^{19}$ and $2^{16}$, with zkDTVM's FRI over the quintic extension (160 queries, 20 bits of query grinding) have every round term at most $2^{-128}$ at every admitted vector (wideBatch5Statement_secureRo, verifierQueries ≤ 134253): the worst vector puts every instance on $2^{22}$ rows, the lookup challenges at $2^{-128.04}$ and batching all 474 opened words on one domain size at $2^{-128.06}$. Over the quartic extension with 144 queries and grinding at every site, as wideGrindSetup, and 18 bits before the lookup challenges, the bound per duplex call is $2^{-115}$ (wideBatchGrindStatement_secureRo, verifierQueries ≤ 120816, wideBatchGrind_knowledgeSoundness_bcs in tests/CompStarkTests/Security.lean, about $2^{-51.05}$ at $2^{64}$ calls), the lookup challenges at $2^{-115.05}$ on $2^{22}$ rows per instance ($2^{-117.99}$ at the keygen heights alone). A fold by $2^k$ that injects a word batches $2^k$ words besides the first instead of $2^k - 1$. With lookup inclusion, Batch.Statement.knowledgeSoundness_bcs_inclusion (CompStark/Iop/LookupInclusion.lean) gives the same bound with SatisfiedWithInclusion in place of Satisfied, for AIRs that bound their query multiplicities at every admitted vector (hcounts), and Batch.Statement.rangeKnowledgeSoundness_bcs for range checks; the multiplicity bound needs no hypothesis here, since an accepting verifier checked it.
Security calculator (CompStark/Calculator/Bounds.lean): every error term above depends on the AIR only through a few numbers, its Shape (its constraint count and identityDegree, its opened words, whether it has lookups, its lookups' interactions T and widest tuple W), and on the heights and FRI's parameters. The calculator computes, for a setup, a base field of p elements, an MCA bound B and an Analysis (FRI's radius δ, the extractor's δ' ≥ δ below the Johnson radius 1 - √rate, and a proximity loss, all rationals), a rational bound on each term of the knowledge error and of the round error, at any FRI arity: the bounds of CompStark/Calculator/Numbers.lean, with the list sizes at δ' at most 1 below the unique-decoding radius and the Johnson bound ⌊(1 - δ' - rate) / ((1 - δ')² - rate)⌋ above it (listSize_le_listBound), batching at the better of B's count and the curve bound, and FRI's folds read off Plonky3's schedule as a plan of folds (ArkLib's Fri.Interaction.Schedule.folds: each fold's arity, the domain it folds onto, and whether it injects a word), each at the better of B's count and the lossy bound. The MCA bound (McaBound, CompStark/Calculator/McaBound.lean) is computable data: where it admits a Reed–Solomon code of degree below k on N points at radius δ, a count of the exceptional seeds for power curves of degree M; B.Holds says that the counts bound the mutual correlated-agreement error of the powers over every finite field and domain. McaBound.uniqueDecoding counts M N within the unique-decoding radius, 2 ⌊δ N⌋ ≤ N - k (uniqueDecoding_holds), McaBound.johnson counts M times the Dao–Kominers–Thaler exception count for lines ([DKT26] Theorem 5.12) up to the Johnson radius 1 - √ρ₋, ρ₋ = (k - 1) / N, exactly as ArkLib's johnsonExceptionCount (johnsonLineCount: (2μ - 1) h + θ (h + μ + 4 D μ h) + (n - D - 1) μ with μ = ⌈t / √ρ₋⌉ - 1, h = ⌈t² / (3 ρ₋)⌉ - 1, θ = (n - D) / (A - D) at the agreement threshold A = ⌈(1 - δ) N⌉ and the multiplicity m = t - 1/2 = max(⌈r / (2 (1 - δ - r))⌉, 3) for a dyadic r ≥ √ρ₋), in Nat and ℚ arithmetic with ⌈√·⌉ through Nat.sqrt, and McaBound.uniqueOrJohnson combines the two. S.Secure p B A bits (and S.SecureRo p B A bits per oracle answer, and the batch's) says that the analysis fits the setup, B admitting its batching and its folds, and the bound is at most 2 ^ (-bits); it is decidable in Nat and ℚ arithmetic, so decide +kernel checks it with the kernel evaluating the AIR's constraints, widths and lookups (a wide 4096 table, 4096 constraints, takes about seven seconds, with maxRecDepth raised for its list of constraints). The analysis need not be picked by hand: S.bestAnalysis p B (and bestAnalysisRo, and the batch's) searches FRI's radius, the extractor's and the loss by coordinate descent over a grid for the smallest bound; it is computation only, so soundness rests on the check of what it finds, and every analysis of CompStark/Calculator/Security.lean is the search's. For a large AIR, secure_of_shape (and secureRo_of_shape) takes the shape as a fact proved once, and shape_eq_of_profileFits proves it from a one-pass kernel check of the constraints' degree profiles (Air.ProfileFits), so that each certificate evaluates only rationals. One theorem per headline turns a certificate into the bound (CompStark/Calculator/Security.lean), given that the MCA bound holds:
```
theorem knowledgeSoundness_of_secure (C : Statement F) (hp : Nat.card F = p) {B : McaBound}
    (hB : B.Holds) (A : Analysis) {bits : ℕ} (h : C.Secure EF p B A bits) (δ' : NNReal)
    (hδ' : (δ' : ℝ) = A.δ') (publicValues : List F)
    {OutP : (C.protocol EF).tree.ExecutionPath → Type}
    (prover : Interaction.Oracle.Prover.Strategy unifSpec (C.protocol EF).tree
      (C.protocol EF).roles OutP) :
    C.farAcceptance EF publicValues (fun _ ↦ δ') prover ≤ (2 ^ bits)⁻¹
```
and likewise batchKnowledgeSoundness_of_secure (with Statement.knowledgeError_le_of_secure and the batch statement's for the errors themselves), and on Plonky3's verifiers Statement.knowledgeSoundness_bcs_of_secureRo and Batch.Statement.knowledgeSoundness_bcs_of_secureRo (CompStark/Calculator/FiatShamir.lean, above). A statement's certificate (Statement.Secure, Statement.SecureRo) checks every admitted length below the two-adicity; a batch statement's (Batch.Statement.Secure, Batch.Statement.SecureRo) bounds every admitted vector's per-vector bound, the vectors being too many to enumerate (secure_setupAt, secureRo_setupAt). Up to an input, FRI's plan is the plan without it down to at most maxLogArity above the input's height (Fri.Interaction.Schedule.folds_plonky3_cons_split), so each input adds at most a per-height amount to the folds' bound, the folds and the largest fold, exactly that at arity 2. The round error's bound is the largest term, so its largest over the vectors is each term's: LogUp at every instance's longest admitted length, the instance terms at every instance's shape at every admitted length, batching on each domain size with every instance admitting it there, FRI's folds from every top length and at every input, and the queries at the most folds. The knowledge error sums its terms: at each top length every instance takes the length of the largest share, its LogUp interactions and, below the top, what its input adds to FRI's folds and queries, with the instance terms at their worst; that bounds every vector of that top length and is the per-vector bound of the vector it picks when the instance terms are worst there and its inputs sit at distinct heights, as for the wideBus batches, whose worst vector has every instance at the longest length. Every concrete bound above is such a check with the unique-decoding bound (fibonacci_secure, wide_secure, …, wideBatchGrindStatement_secureRo).

What is proven and what is not: the list sizes up to the Johnson radius are proven (CompStark/Sound/Johnson.lean), so the extractor's δ' may go beyond the unique-decoding radius, with the folding and out-of-domain terms multiplied by the list sizes. FRI's soundness holds at every radius δ (ArkLib's Fri.Interaction.acceptance_le, Garreta–Mohnblatt–Wagner's round-by-round argument: each fold's MCA error, a curve of degree 2^k - 1, or 2^k when it injects an input, and (1 - δ)^t for the queries), and so does batching; the radius is limited by the MCA bound the calculator uses. Within the unique-decoding radius it is proven (uniqueDecoding_holds, from ArkLib's unique-decoding curve bound, with ArkLib's curve and lossy bounds in the unique-decoding range, CodingTheory.UniqueDecoding), so each query is worth at most $\log_2 (4/3) \approx 0.415$ bits at blowup 2 and $\log_2 (8/5) \approx 0.678$ at blowup 4. Up to the Johnson radius it is proven too (johnson_holds, uniqueOrJohnson_holds): ArkLib's Johnson-regime mutual correlated agreement for power curves (ReedSolomon.exists_johnson_curve_exactPowerAgreement_line_mul_of_fintype, Dao–Kominers–Thaler's line count with the curve degree as a factor, in any characteristic and on any domain, branch fri-interaction of the ArkLib fork, on ArkLib main), which brings a query up to $\log_2 (1/(1 - \delta))$ bits for δ up to 1 - √rate, about 0.5 bits at blowup 2 and 1 at blowup 4.

Plonky3's Keccak example (tests/CompStarkTests/KeccakSecurity.lean): KeccakAir, 3182 constraints of degree 3 over 2633 columns, every column opened at the next row, as a statement whose proofs may claim any trace length the verifier admits, $2^0$ to $2^{23}$ rows at blowup 2 and to $2^{22}$ at blowup 4, every certificate covering all of them at one analysis (secureRo_of_lengths, secure_of_lengths). With the example's FRI (blowup 2, arity 8, 87 queries, 16 bits of query grinding and 10 of batching grinding, caps of height 3) over KoalaBear's quartic extension it has 52 proven bits per duplex call and 36 interactively (example_secureRo, example_secure). Over the quartic extension the out-of-domain term caps the bits near 98.4 on $2^{23}$ rows and 99.0 on $2^{22}$, so 203 and 244 queries at blowup 2 and 124 and 149 at blowup 4 give 98 bits per duplex call and interactively; over the quintic extension 270 and 310 queries at blowup 2 give 128 and 127 bits, 166 and 190 at blowup 4 give 128 and 128. Up to the Johnson radius (McaBound.uniqueOrJohnson), over the quintic extension with Plonky3's grinding, 169 queries give 100 bits per duplex call and 205 give 98 interactively at blowup 2, 85 and 102 give 100 and 99 at blowup 4 (johnson_knowledgeSoundness_bcs_quintic on Plonky3's verifier); the batching curve's degree 5273 multiplies the Johnson count, which grows with the trace, so with 0, 30 and 12 bits of grinding before ζ, the batching challenge and each fold, 230 and 115 queries give 125 and 126 bits per duplex call over the quintic extension, and with 1, 30 and 16 bits over the quartic one 172 and 86 queries give 96 and 97.

Development tools

The Rust side lives in bench/rust, built for the native CPU (bench/rust/.cargo/config.toml), without which Plonky3's fields lose their vectorized arithmetic; cargo run --release prints the Poseidon2 known answers used by the tests, compstark-bench challenger the challenger's, compstark-bench stark AIR LOG_N LOG_BLOWUP LOG_FINAL MAX_LOG_ARITY QUERIES COMMIT_POW QUERY_POW [BATCH_POW OOD_POW] a proof of the fib, cube, square (no next row read), wide, prep or prep0 (preprocessed columns, read at the next row or not), periodic, periodic-wide, periodic-tiny or pcube (periodic columns) AIR as JSON, and compstark-bench seeds Plonky3's interaction patterns and domain separators of the tests' configurations; compstark-bench babybear and compstark-bench stark-babybear AIR … print the same over BabyBear, and compstark-bench batch CASE LOG_BLOWUP LOG_FINAL MAX_LOG_ARITY QUERIES COMMIT_POW QUERY_POW [BATCH_POW OOD_POW [LOOKUP_POW]] a batch-stark proof of the batch three, mixed, periodic, single, prepmul, square, or with lookups local1, local, global, both, lookups, single-local, heights, failed-global or failed-local as JSON (batch-babybear CASE … over BabyBear; batch-bench wide … times prove_batch on the benchmark's three wide tables, batch-bench lookup-bench … on the lookup benchmark's batch). Run the challengers and proofs with RAYON_NUM_THREADS=1, so that grinding returns the smallest witness. lake test builds the #guard library CompStarkTests and runs the compiled test driver CompStarkNativeTests: the known answers on the packed kernels, and Plonky3's proofs verified, rejected when tampered, and reproduced by the specification prover and the fast prover (KoalaBear and BabyBear). Lake does not track tests/data: after replacing a proof there, rerun lake exe CompStarkNativeTests (or lake env lean tests/CompStarkTests/BabyBear.lean).

For the Keccak fixture, compstark-bench fingerprint AIR LOG_N prints an AIR's fingerprint report (tests/data/fingerprint), compstark-bench keccak-example-constants the module of the example's Poseidon2 constants, RAYON_NUM_THREADS=1 compstark-bench keccak-example L DIR the example's proof, inputs and trace, and compstark-bench lde LOG_N WIDTH REPS times Plonky3's trace extension (CompStarkBench lde LOG_N WIDTH REPS CompStark's).

Possible improvements

Custom externs for the Poseidon2 kernels. Every ByteArray store in Lean carries an exclusivity check, so a loop over the eight lanes stays scalar, and clang's SLP vectorizer only handles one round at a time. Written as one loop over the lanes, the whole width-24 permutation keeps its state in registers and vectorizes cleanly: 211 ns in a C model of the Lean kernels, against 289 ns for the split Lean kernels and 179 ns for Plonky3. A check-free store primitive would unlock that shape, at the price of trusting an extern.
Extending wide matrices across columns. The extension transforms one column at a time, vectorized along it, so its last layers shuffle within vectors, its inverse transform reverses bits, and the trace is transposed into columns first; Plonky3 transforms rows of the row-major matrix, eight columns per vector, with neither. On one thread the transforms are as fast as Plonky3's for a few dozen columns, but at Keccak-f's 2633 columns they take about 1.7 times its instructions (24.8 against 14.3 billion for $2^{16}$ rows, CompStarkBench lde 16 2633 REPS, compstark-bench lde 16 2633 REPS). Transforming strips of eight columns interleaved word by word, the trace's own layout, would remove the transposes, the shuffles and the reversal. Strips of eight interleaved columns, every butterfly between rows one vector with a broadcast twiddle, took that extension from 24.8 to 21.3 billion instructions, but its time on one thread from 2.15 to 2.35 s and on 16 threads from 0.30 to 0.75 s ($2^{18}$ rows of 64 columns: 0.042 to 0.15 s on 16 threads): a strip of $2^{16}$ rows is 2 MB, so its passes stream from L3 instead of L2, and sixteen at once exceed it. Transforming eight columns at once pays only with the passes blocked to the caches across columns and rows, as Plonky3 blocks its row-major matrix.
Faster Poseidon2 kernels. Merkle hashing and grinding are most of a proof on one thread: on wide 64 at $2^{16}$ rows the width-24 and width-16 permutations take about half the instructions of FRI's commit phase and of the commitments, at about 1.3 times Plonky3's time per permutation. Per group of eight width-16 states the kernels run about 13,300 instructions against 11,500 for Plonky3 (21,400 against 18,500 at width 24): a partial round about 276 against about 250, most of the difference the loads and stores of the state and the constants each round reloads, and a full round 880 against about 760, mostly in the S-box, whose Montgomery products the compiler widens to 64-bit lanes and narrows back where Plonky3 multiplies even and odd lanes in place, and whose constant additions are reduced where Plonky3 adds constants in [-p, 0] to signed products. Fusing round parts so that the state stays in locals does not pay with the compiler's SLP vectorizer: a full round in one kernel takes 2,150 instructions against 880 split, mat4 with the block-sum mixing 823 against 385, two and four partial rounds per call 357 and 413 per round against 292, even with its recursion depth raised (-mllvm -slp-recursion-max-depth), because values shared between rows of one kernel are vectorized tree by tree and spilled; the mixing fused with the next S-boxes saves 31 of 635 instructions and no time. Interleaving two groups per call leaves the time per permutation unchanged, so the partial rounds are not latency bound. Carrying the state from round to round in the arguments of the partial-round loop instead of the buffer takes 357 instructions per round against 309 for the loop over the buffer: the state's 128 words are loop-carried scalars, which the vectorizer gathers and scatters every round. BabyBear's S-box x ^ 7 as five products left in 64-bit lanes (x ^ 2, x ^ 4, x ^ 5, x ^ 6, x ^ 7, every lazy product below 2 ^ 32 for BabyBear), without the two reductions and narrowings between them, takes 1.2% fewer instructions per permutation and no less time. A full round's three kernels inlined into one function, each still a separate pass over the state, take 900 instructions against 938 for the three calls, in the same time.
Hashing FRI's folded layers from their coordinate planes. Every folded layer is gathered into columns (leaves, every k-th word of a plane sixteen words at a time, FoldWords.strided) before it is hashed. Hashing the planes in place takes a leaf loader that reads a plane's pairs with a stride, beside Merkle.Packed.hashColumns's loader of contiguous column lines, and a matrix type for strided columns. The arity-2 fold reads its pairs in place (CompStark/Fri/FoldWords.lean: halves and diffs, sixteen pairs per vectorized kernel, then halves + β · diffs on planes), which took the commit phase on wide 64 from 1.02 to 0.89 billion instructions.

Keccak hash kernels

CompStark.Keccak provides pure-Lean Keccak-f[1600] and original Keccak-256, with no new externs or inline C. scripts/gen_keccak.py generates the straight-line round in Scalar.lean and the sponge in Sponge.lean. Both retain 25 unboxed UInt64 lanes across rounds; the sponge retains them across absorption too, with no boxed lane arrays or padded message allocation. Complete lanes load directly from the input through two approved ByteArray.ugetUInt32LE accesses. The final partial lane supplies the 0x01 delimiter, lane 16 supplies the final 0x80 bit, and eight approved usetUInt32LE stores write the 32-byte digest. Each 136-byte block, including the final padding block, executes one absorption transition and 24 rounds in a structurally recursive scalar loop. Both kernels use the packed-native library's -march=native -mstackrealign compilation flags.

Refines.lean proves each scalar round agrees with VCVio (roundWith_eq), then any number of rounds (permute_eq, permute_succ_eq) and the complete permutation (f1600_eq). The named sponge lemmas loadLane_eq, partialLane_eq, lastLane_eq, digest_eq, absorbWith_eq, run_rounds_eq and run_blocks_eq establish the packed accesses, padding and scalar transitions; keccak256_eq proves exact equality with VCVio.Algorithms.Keccak.keccak256. The public hash requires input.size < USize.size: the approved word accessor uses machine-sized offsets, while Lean's abstract ByteArray admits larger sizes. keccak256Batch takes the corresponding membership proof for every input and preserves input order, with its _eq refinement. These proofs are erased by compilation. The independent permutation API f1600Batch also preserves input order and uses the scalar kernel serially. hashNode left right hashes two 32-byte child digests in left/right order; hashLeaf payload hashes a 512-byte payload. Their existing length proofs discharge machine addressability, and hashNode_eq/hashLeaf_eq establish the reference digests. The complete hash and batch refinements depend only on Lean's standard logical axioms (propext, Classical.choice, Quot.sound).

tests/CompStarkTests/KeccakHash.lean checks the empty and abc known answers, 26 lengths around byte/lane/rate boundaries and the 512-byte leaf size with four byte patterns, nonzero independent permutation states, both empty batches, and node/leaf framing. These checks run in the compiled test driver because the approved word accessors execute through their native implementations. The performance gate includes keccak-scalar (10,000 dependent permutations and 10,000 hashes of each message size) and keccak-batch (ten batches of 1,024 independent states/messages), with a phase for each operation and reference-checked sinks outside the measurements.

Build the Lean benchmark with systemd-run --user --scope -p MemoryMax=12G -p MemorySwapMax=0 -- lake build CompStarkBench and the pinned Plonky3 comparison with cd bench/rust && cargo build --release --bin keccak-kernels. Run LEAN_NUM_THREADS=1 flock /tmp/compstark-bench.lock taskset -c 5 .lake/build/bin/CompStarkBench keccak-kernels 10000 from the repository root and flock /tmp/compstark-bench.lock taskset -c 5 bench/rust/target/release/keccak-kernels 10000 for Rust. The scalar initial state, patterned 64/512-byte messages, batch inputs and consumed 64-bit sinks match on both sides. Rust uses black_box, and its batch hashes use Plonky3's runtime-selected vector backend. The compiled Lean hash is called from a separate module, and every output contributes to the sink. Wall-clock runs hold the shared lock; the instruction counts from scripts/perf-gate decide regressions under host load.

scripts/bench-keccak compares the median instructions per operation of three runs of each Lean workload and the Rust kernel binary, using the gate's acknowledged FIFO protocol. It takes no wall-clock lock because its comparisons use instruction counts.

Kernel measurement: 2026-11-06

On the shared Ryzen 7 3700X, three interleaved Lean/Rust process pairs, one thread pinned to CPU 5 under the shared lock, execute 100,000 scalar operations and 100,352 independent operations in groups of 1,024. The table gives median ns/op; instruction counts are medians from three separate acknowledged counter runs at the gate's 10,000/10,240 operation counts. Every one of the six sinks matches Rust in every interleaved round. Rust's runtime batch backend uses four AVX2 lanes on this CPU; the binary's max_compiled_lanes=8 reports its widest compiled backend, including AVX-512, rather than the selected hardware backend.

Operation	Lean ns/op	Rust ns/op	Lean instructions/op	Rust instructions/op	Instruction ratio
Keccak-f dependent chain	919	492	7,742.2	4,689.1	1.65×
Keccak-256, 64 bytes	879	534	6,487.6	4,890.1	1.33×
Keccak-256, 512 bytes	3,282	2,013	23,994.3	19,187.1	1.25×
Keccak-f independent states	951	487	7,722.0	4,690.1	1.65×
Keccak-256 batch, 64 bytes	890	225	6,525.7	1,697.3	3.84×
Keccak-256 batch, 512 bytes	3,294	871	24,031.6	6,599.5	3.64×

The 1/5/15-minute load averages were 4.085/5.681/6.189 before the wall-clock runs and 4.078/5.652/6.177 afterward. These are loaded-host measurements, not quiet-host performance claims. The survey's Rust reference was 301 ns for the permutation, 287/1,101 ns for scalar 64/512-byte hashes, and 136/545 ns for its AVX2 batch hashes. Instruction counts decide the A/B results: the scalar packed sponge reduces the 64/512-byte hash counts from 37,541.7/76,448.4 to 6,487.6/23,994.3 per operation, reductions of 83%/69%. CPU targeting also reduces the permutation count from 9,987.2 to 7,742.2. A 512-byte hash executes four permutations and costs 3.70 times the instructions of a 64-byte hash, which executes one.

Batch vectorization and interleaving

Two- and four-state packed prototypes use structure-of-arrays storage at byte offset (lane * states + state) * 8, paired approved word accesses, and straight-line operations grouped across independent states. Separate scalar prototypes carry 50 or 100 unboxed lane parameters across all rounds. Lean's emitted C represents the lanes as individual uint64_t locals. With the bundled clang at -O3 -march=native -mstackrealign, all four hot bodies (round2, round4, scalar2, scalar4) contain zero packed arithmetic instructions and zero YMM register references. YMM copies appear only in interface wrappers. The four-state packed round uses scalar instructions such as:

69e: rorx $0x3f,%rbx,%rdx
6bc: rorx $0x3f,%rcx,%rcx
6e5: rorx $0x15,%rdx,%r8
724: rorx $0x3f,%r11,%rdx
76a: rorx $0x14,%r15,%rdi
780: andn %r8,%rdi,%rcx

In particular, its round arithmetic has no vpxor, vpand, vpandn, vpsllq, vpsrlq or vpor. Recompiling the emitted C with -Rpass=slp-vectorizer -Rpass-missed=slp-vectorizer -Rpass-analysis=slp-vectorizer reports “Cannot SLP vectorize list: vectorization was impossible with available vectorization factors” and “List vectorization was possible but not beneficial with cost 0 >= 0”. This establishes the outcome for these tested formulations, rather than ruling out all pure-Lean SIMD formulations. The packed two/four-state round stack frames are 496/1,008 bytes; the scalar interleaved bodies use 464/976 bytes, exposing the register pressure from many live lanes.

The following counter measurements are per independent permutation, including each candidate's interface. Cycle counts and IPC are representative medians on the loaded host and are secondary to instructions.

Candidate	Instructions/state	Cycles/state	IPC
Packed two-state, reload/store each round	7,630.7	2,379.9	3.21
Packed four-state, reload/store each round	7,601.1	2,650.5	2.87
Scalar interleave two, packed interface	5,080.8	1,694.1	3.00
Scalar interleave four, packed interface	5,300.6	2,003.7	2.65
Scalar interleave two, public array interface	7,720.9	2,559.4	3.02

The retained scalar array mapping takes about 7,722 instructions and 2,228 cycles per independent permutation. Converting the public arrays consumes the packed two-state interleaving's instruction advantage, and its public interface is instruction-flat with worse cycles. A paired scalar sponge also costs 22%/24% more instructions per 64/512-byte hash than the single-state sponge measured alongside it. None of these batch candidates improves the public API enough to retain, so production batches map the scalar kernel. Scalar hashes cost 1.33/1.25 times Rust's instructions; batches remain at 3.84/3.64 times Rust because the tested Lean formulations do not obtain Rust's four-lane AVX2 arithmetic.

Streaming Keccak Merkle commitments and overwrite duplex

CompStark/Keccak/Merkle.lean implements a binary root-only commitment to packed 64-bit rows. Row carries a complete, addressable leaf image in little-endian bytes, and Row.ofWords packs arbitrary lane values. The caller supplies lane permutations, zero prefixes and field-limb order. Builder.absorb consumes encoder tiles in row order, hashes each arriving row and merges completed subtrees by binary carry. finish rejects empty and incomplete trees. The returned Subtree owns both the complete leaf payloads and every cached digest; Tree.root is the public commitment. There is no cap, implicit leaf padding or protocol tag.

Tree.nodes_eq and Tree.root_eq identify the cache and commitment with VCVio's buildMerkleTreeWithHash, using VCVio's Keccak-256 for leaves and the concatenation of left and right digests for nodes. The cache certificate is erased at runtime. carry_rows, Builder.absorb_rows, Builder.finish_rows and commit_rows preserve the complete input payload sequence, including across tile boundaries. Tree.open sorts and deduplicates queries, returns their rows in ascending order, and uses VCVio's MixedMerkleTree.prune on cached authentication paths for the canonical bottom-up sibling stream. Tree.open_eq identifies every sibling with the reference tree's pruned paths. Empty or out-of-domain query sets are rejected. verify checks the row count, reconstructs the root with VCVio's walk and rejects leftover siblings. Tree.batchProof exposes the same retained cache through VCVio's intrinsic selector API; Tree.batch_complete proves honest multi-opening completeness.

CompStark/Keccak/Duplex.lean supplies an overwrite-duplex engine with a positive rate below 25 lanes, a bounded pending cursor, and a generic observer accumulator. Absorption overwrites rate lanes; a full rate flushes when another lane arrives. Every sample performs a fresh permutation, returns the requested output prefix and zeroes the rate while retaining capacity. The observer receives every exact permutation input and output in execution order. Writer.write transmits and binds one caller-framed message together; Writer.sample leaves the transmitted stream unchanged. absorb_eq, sample_eq and Writer.write_eq prove complete state, observer and output equality with the same engine over VCVio's Keccak-f. Framing and tags are supplied by the caller. grind probes a bounded interval in increasing order, observes only the accepted transition and returns exhaustion explicitly. findNonce_min proves minimality, and grind_eq proves equality with VCVio. Grinding is serial; the generic engine imposes no field or nonce encoding.

The compiled tests in tests/CompStarkTests/KeccakMerkle.lean, included in lake test, compare 72 exact roots, complete opened leaf images and canonical openings, 11 complete permutation checkpoints, and smallest nonces at 0, 8 and 13 bits with leanMultisig 9d8bce818aa7c7e18e67026e522a9b1539d0a57d. The tree cases cover one, two, eight and 32 leaves; widths 1, 8, 16, 17, 34 and 64 words; duplicate and unsorted queries, all leaves and single leaves. Native negative checks cover missing rows, surplus siblings, empty and out-of-range queries, empty commitments and non-power-of-two row counts. The duplex fixtures cover empty samples, exact rate fills, automatic flushes, repeated samples and full capacity carry. Axiom reports for the refinement and completeness theorems permit only Lean's standard logical axioms.

scripts/check-keccak-merkle-reference clones the pinned Rust source into a fresh temporary directory, builds its unchanged production crates, links the external read-only harness tests/rust/keccak-merkle.rs, checks the committed vectors with one and 16 Rust workers, and deletes the temporary checkout. The reference executable remains in .lake/keccak-merkle-reference. scripts/bench-keccak-merkle reproduces the reference check, builds the Lean benchmark, runs native correctness tests, measures three interleaved Lean/Rust rounds on CPU 5 under the shared wall-clock lock, and counts instructions for the same phases. Its JSON output in .lake/keccak-merkle-measurements.json records every run, load averages, toolchains, CPU, affinity, output sinks and per-process peak RSS. The keccak-merkle push-gate workload commits 4,096 64-word leaves, opens 100 distinct queries, transmits and samples 10,000 messages and performs an eight-bit grind. Each phase checks its root, shape, output-dependent sink or smallest nonce against the Rust reference.

On the Ryzen 7 3700X, Lean 4.35.0 and Rust 1.99.1 with native CPU targeting, the median of three single-threaded, CPU-5-pinned interleaved rounds gives:

Phase	Lean ms	Rust ms	Lean instructions	Rust instructions	Instruction ratio
Commit 4,096 × 64-word rows	12.273	2.924	129,349,892	32,077,409	4.03×
Open 100 queries	1.012	1.185	8,950,976	12,474,244	0.72×
Write and sample 10,000 messages	11.680	3.192	137,601,082	47,820,313	2.88×
Eight-bit grind, smallest nonce 73	0.094	0.021	1,070,464	357,761	2.99×

Load averages ranged from 6.73/9.56/10.34 to 6.67/9.50/10.31; the wall times are loaded-host diagnostics. Median process peak RSS was 94,976 KiB for Lean and 5,632 KiB for Rust, including input packing, module startup and retained data rather than a phase-specific allocation measurement. Input packing and seeding are outside the phase timers. Both writers retain their complete transmitted streams. The commitment root, opening row/sibling counts, writer sink and grinding nonce match. Rust uses its AVX2 hash batches and cuts the retained tree at large sizes, reconstructing lower nodes during opening; Lean uses the scalar Keccak kernel and retains every node and leaf image. This accounts for different commitment/opening tradeoffs. The commitment and duplex instruction gaps remain performance work; these measurements establish component baselines, without establishing the survey's proposed end-to-end comparability target.

Shared-challenge cubic-extension folds

CompStark/Sumcheck/Fold.lean folds pairs of interleaved BF64.WordExt3 rows. Each row has a fixed column width; rows = 1 gives a high-variable restriction, and width four gives the four child tables of a radix-four GKR layer. The input and output lengths are carried by Vector, including empty shapes. prepare constructs six base-field byte maps for one shared extension challenge. Prepared.mul uses those maps in the cubic extension's six-product Karatsuba formula. prepared_mul_eq equates it with the existing word kernel, and fold_refines proves every output coordinate is (1-r)*lo + r*hi in BF64.Ext3.

lake test compares prepared multiplication and folds with the scalar kernel for zero, one and full-limb challenges, empty shapes and several row widths. It also checks every byte of a 17-row, four-column fold against unchanged leanMultisig interpolation at revision 9d8bce818aa7c7e18e67026e522a9b1539d0a57d. scripts/check-sumcheck-fold-reference reproduces that reference in a disposable checkout and retains its benchmark executable at .lake/sumcheck-fold-reference. The sumcheck-fold performance-gate workload prepares one challenge and folds 16,384 pairs of four-column rows, with independent scalar validation outside the measured phases. Plonky3's prime-field extensions do not implement this binary cubic extension; the arithmetic comparison uses leanMultisig's matching field.

scripts/bench-sumcheck-fold reproduces the native and Rust checks and three interleaved instruction-count comparisons under the shared benchmark lock. The checked-in bench/sumcheck-fold.json records the phase counters and host loads. On the Ryzen 7 3700X with Lean 4.35.0, the median fold counts are 59,849,311 Lean instructions and 6,361,317 Rust instructions (9.41×); preparing the shared maps costs another 14,863,654 instructions. Loads were 22.97/30.13/37.66 through 23.62/30.14/37.62, so wall times are loaded-host diagnostics. The Rust driver invokes its production interp on the same interleaved rows and challenge; the Lean driver validates every output against the scalar word kernel outside the counted regions. These counts expose the remaining binary-extension performance gap.

Shared-challenge preparation

The cubic-extension fold prepares its six fixed multipliers with the certified masked-integer base-field kernel. Sumcheck.byteMap_eq identifies each resulting byte map with Word.ByteMap.ofScalar; prepared_mul_eq and fold_refines carry that equality through interpolation and every output coordinate. The native fixture checks all coordinates against the original word multiplication and the pinned leanMultisig reference.

The instruction gate's three-run median for sumcheck-fold/prepare is 8,965,331 instructions, compared with 14,865,628 for preparation through the structural word multiplier, a 39.7% reduction. The prepared fold workload itself retains its 59,849,263-instruction baseline; the change affects preparation alone.

The shared-challenge fold uses eight USize-indexed packed loads per base-field lookup product. Sumcheck.ByteMap.mapMul_eq identifies these reads with the canonical byte-map multiplication, including byte selection and exact machine offsets. Native regressions compare the complete fold with the scalar kernel and the pinned Rust buffer. The fold gate median is 58,014,024 instructions, down from 59,849,263; preparation is unchanged. Fixed position coordinates use explicit Fin constructors, keeping delayed numeral reduction out of the hot kernel.

Byte-map preparation constructs 256 masked nibble products and joins each low/high pair into the 2,048-entry byte map. Sumcheck.byte_split proves the disjoint four-bit decomposition by kernel reduction; byteMap_eq proves equality of the complete packed buffer with the canonical multiplier map. The full library, native reference checks, namespace axiom audit and instruction gate cover this path. The preparation gate median is 8,268,550 instructions, 7.8% below 8,965,331; the fold median remains 58,017,433. Packed-map construction and lookup overhead account for most of the preparation cost even with fewer arithmetic products.

Packed map construction uses bounded USize stores and specializes its coordinate function; nibble lookups use machine-size indices and loads. Sumcheck.Buffer proves the exact word offsets and equality of both reads and writes to BF64.Packed operations. fillWords_eq lifts the store equality to the complete buffer. The map's nibble indices and final packed result are kernel-checked by nibbleIndices and byteMap_eq.

The packed-construction gate median is 4,371,073 instructions for preparation, 47.1% below the 8,268,550-instruction nibble-construction baseline, and 51.2% below the 8,965,331-instruction masked-product baseline. The fold median is stable at 58,017,035. Full library, native Rust conformance, namespace axiom checks and the instruction gate pass.

Packed extension folds

CompStark.Sumcheck.PackedFold stores cubic-extension tables in three contiguous word planes. Its specialized fill and fold loops use USize indices and bounded native word loads/stores. fillScalarsLoop_read proves the entire mutable fill invariant; foldPacked_toArray proves exact agreement with the scalar-array fold, and foldPacked_refines gives the affine restriction in the specification field. Optional-index reads implement explicit identity or zero padding. CompStark.Sumcheck.IndexFold supplies a specialized machine-index accumulator with an ordered natural-range fold theorem.

The sumcheck-fold/packed-fold gate phase folds the same 16,384 pairs of four-column rows as the array phase. Packing and scalar validation occur outside the measured fold. Three interleaved repetitions in bench/sumcheck-fold.json give 31,703,278 packed-fold instructions against 58,015,770 for the array fold and 6,361,317 for Rust, a 45.4% reduction and 4.98× Rust's instructions. Shared challenge preparation costs another 4,371,119 instructions. Tests compare the packed and array folds across empty shapes, row widths 0/1/4/15 and zero/one/full-limb challenges, then check the exact independent Rust fixture. The full library/native suite and namespace axiom audit cover the packed kernels.

Native-indexed challenge preparation

Sumcheck.fillWordBuffer specializes its word-producing function into a bounded USize loop. fillWordLoop_eq proves the complete remaining-coordinate fold invariant and fillWordBuffer_eq identifies its output with the canonical packed buffer. Challenge maps share the sixty-four polynomial shifts, select nibble products by XOR, and join the two nibble lookups with native indices. nibbleProducts_eq and byteMap_eq certify both stages.

The three interleaved repetitions in bench/sumcheck-fold.json measure 2,375,934 instructions for preparation, a 45.6% reduction from 4,371,119. Packed folding measures 31,703,278 instructions against Rust’s 6,361,317 (4.98×); the preparation and fold are separate counted phases. Full library and native tests, exact Rust fixture comparison, the sumcheck namespace axiom audit and the performance gate validate these kernels.

The binary-field sumcheck plan (CompStark/Sumcheck/Fold.lean) retains its shared cubic-extension scalar and a kernel-checked agreement theorem for its six byte maps. Prepared.interpolateShared_eq certifies the equal-endpoint shortcut: constant pairs require no map loads, while ordinary pairs use the same six-map Karatsuba product. CompStarkBench sumcheck-fold checks both ordinary and constant row pairs in array and packed storage; all four fold phases are covered by the instruction gate.

Prepared multiplication also certifies its three coordinate maps on base-field inputs. Prepared.mulSubfield_eq proves that using those three maps when the higher input coordinates vanish preserves the full product. The instruction gate covers ordinary, base-field and constant row pairs in array and packed storage. Three interleaved repetitions in bench/sumcheck-fold.json measure 24,028,339 instructions for the packed ordinary fold (3.78× Rust) and 20,360,250 for the packed base-field fold (3.20× Rust); the corresponding Rust phases use 6,361,318 and 6,361,901 instructions. Shared preparation costs 1,184,736 instructions. Native tests compare full-limb and subfield multiplication with the scalar word kernel and retain the exact Rust fixture check.

Five-product binary cubic multiplication

Sumcheck.extMulFive multiplies BF64.WordExt3 values with five base-field products, evaluating the coefficient polynomials at zero, one, infinity, the base generator X and X+1. Multiplication by X is a shift and reduction; division by X uses one shift and correction, while division by X+1 uses six prefix-XOR stages and a low-bit correction. timesX_divideX, timesXOne_divideXOne, divideDenominator_toField and extMulFive_eq prove exact agreement with the existing six-product kernel. The proofs use kernel-checked bit identities and field algebra.

Native regressions compare generated full-coordinate pairs and every pair of monomial basis coordinates in all nine limb placements with the independent six-product kernel. The sumcheck namespace axiom audit includes the multiplication theorem and its inverse identities. The sumcheck-fold/products gate phase multiplies 65,536 pairs and validates every result outside the counters.

The product phase's three-run median is 81,477,926 instructions (65,536 extension products), with a largest deviation of 0.000007. Its baseline is added alongside the existing prepared-fold entries; the existing phase baselines are retained.

Sparse and split-tensor query induction

Pcs.DenseInduction caches normalized subspace factors per query, builds low/high novel-basis tensors and scales each high factor once per query and limb. induceSplitRows_refines identifies every packed output coordinate with the certified encoder transpose. Pcs.SparseInduction scatters ordered query weights, enumerates only occupied parent blocks at each transpose stage and collapses the replicas. QuerySupport certifies that omitted blocks are zero; induceOccupiedRows_refines preserves all coordinates, including repeated query positions. These kernels follow the dense split and sparse support strategies of leanMultisig's whir_induce.rs; occupied stages retain full-domain storage rather than Rust's window/strip cache layout.

Native tests cover empty dimensions, no queries, zero lanes, rate zero, duplicate positions and three extension limbs. The independent Rust fixture includes a 12-bit message, rate exponent two and 137 ordered queries spread across the domain, with both unchanged Rust induction kernels agreeing on every output byte at one and sixteen workers. The namespace axiom audit includes both refinements.

Pcs.InductionDot specializes a tail-recursive accumulator into split-matrix reconstruction. inductionDotLoop_eq certifies its finite sum and induceSplitRows_code replaces the complete dense entry point, preserving the coordinate refinement. Three interleaved instruction-count repetitions in bench/pcs.json measure the 12-bit split kernel at 671,652,284 instructions against Rust's 8,113,825 (82.78×); occupied sparse induction uses 183,150,206 against 2,810,986 (65.15×). Plans are constructed outside both counted regions. The six-bit fixture uses 2,119,745 split instructions and 1,499,663 occupied instructions, against 1,868,780 for the complete-domain native transpose. These counters expose remaining scalar-product and occupied-stage overhead; these algorithms alone do not establish a production speedup. All four added induction phases are covered by the instruction gate.

Occupied sweeps retain the block array and stride outside their butterfly loops. occupiedPairCached_eq and occupiedIndexCached_eq certify direct arithmetic addresses; occupiedStage_eq transfers the full support and transpose proofs to the cached implementation. Shared Basis projection resolves each point window once per term with projectionAddresses; projectColumnsIndexed_eq preserves every lane projection without repeating structural window searches per lane. The small shared-column gate measures 70,068,452 instructions, with the existing tolerance retained.

Pcs.DirectSums accumulates the two quadratic coefficients and compact Basis reconstruction directly in three native word registers. Its compiler refinements preserve the complete extension sums. The Rust round fixture and all six projected-round checks cover the replacement. Three-run instruction medians are 441,786 for the isolated round (from 526,231) and 93,133,518 for the projected Basis workload (from 95,179,854); both phases are tracked by the instruction gate.

Prepared Basis projections read binary selections directly from their fixed witness offsets, without an indirect accessor call per word. Compact point windows use direct coordinate accumulators, and window-address preparation shares the distinct-window list before resolving terms. Kernel refinements preserve both projection matrices. The point/binary Basis workload uses 57,839,807 instructions and the general projected workload uses 86,726,223; native tests and the instruction gate cover both.

SparseInduction.sparseInductionPlan prepares nibble-built byte maps in the final 256-block frontier, with certified machine-size table lookups. inductionTwiddles_eq proves that direct scalar subset sums retain the complete generic twiddle table. The 12-bit occupied transform uses 153,329,912 instructions; its plan costs 108,944,961. The scalar-only plan costs 250,044,494 and its transform 183,149,947, so complete setup plus execution falls from 433,194,441 to 262,274,873 instructions. Separate setup phases and both output checks are included in the gate; these counts include the generic normalized-subspace evaluation.

Round message products specialize zero, unit and base-field factors, and full cubic-extension factors use the certified five-product interpolation kernel. roundProduct_eq retains the complete reference product and roundCoefficients_code preserves both authored message scalars. The full-extension Rust round fixture uses 431,302 instructions; the kernel refinement covers every branch, and native PCS conformance tests plus the instruction gate check the compiled message entry.

Keccak.MerkleGenerate builds complete power-of-two row families directly into retained cache-resident subtrees. The consuming thread generates rows and hashes both leaves and internal nodes, retaining allocator ownership through later openings and reclamation. commitGenerated_eq equates the complete result, including payloads and every cached digest, with the streaming commit interface. The commit-generated instruction gate checks its root against the streaming path and the native Rust fixture.

Generated Keccak Merkle subtrees use one row accessor with absolute offsets, avoiding nested index callbacks. Each contiguous batch retains the full leaf payloads and cached internal digests on the consuming thread. Tree.generateAt_eq and commitGenerated_eq equate this path with the certified streaming builder.

Keccak.MerkleRows hashes completed encoder windows into flat digest buffers on their worker. HashedRows.get copies each retained digest onto the consumer, and Tree.generateCachedAt allocates the payloads and retained tree nodes there. The exact refinement includes every private row and cached node, while temporary hashing allocations are reclaimed on their creating worker.

Navigation Menu

Repository navigation

components.md

components.md

Components and theorems

Development tools

Possible improvements

Keccak hash kernels

Kernel measurement: 2026-11-06

Batch vectorization and interleaving

Streaming Keccak Merkle commitments and overwrite duplex

Shared-challenge cubic-extension folds

Shared-challenge preparation

Packed extension folds

Native-indexed challenge preparation

Five-product binary cubic multiplication

Sparse and split-tensor query induction

FilesExpand file tree

components.md

Latest commit

History

components.md

File metadata and controls

Components and theorems

Development tools

Possible improvements

Keccak hash kernels

Kernel measurement: 2026-11-06

Batch vectorization and interleaving

Streaming Keccak Merkle commitments and overwrite duplex

Shared-challenge cubic-extension folds

Shared-challenge preparation

Packed extension folds

Native-indexed challenge preparation

Five-product binary cubic multiplication

Sparse and split-tensor query induction