CompStark

Fast, formally verified components of a STARK prover and verifier in Lean 4, benchmarked against Plonky3.

CompStark builds on CompPoly, which provides the fields, packed storage and transforms: KoalaBear in Montgomery form, its quartic and quintic extensions, parallel NTTs and the batched coset low-degree extension. CompStark adds the protocol layers on top: hashing, Merkle commitments, FRI and the prover and verifier. Every fast implementation comes with a proof that it computes its specification, and with a benchmark against the corresponding Plonky3 component.

Status

• 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 implementation is the packed kernels below, one state in lane 0 of a group, for any round constants of KoalaBear's shape (CompStark/KoalaBear/Poseidon2.lean: Instances 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; the 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); BabyBear's is the specification on its Montgomery field (CompStark/BabyBear/Poseidon2.lean). 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, which CompStark pins through ArkLib#1317, a Lean v4.35 bump stacked on the FRI soundness proof of ArkLib#992.

• Packed Poseidon2 (CompStark/Poseidon2/Packed.lean): eight states at a time, one per vector lane, with macro-generated round kernels on Montgomery words. permute16_width16 and permute24_width24 (PackedCorrectness.lean, PackedCorrectness24.lean, on the width-generic PackedLanes.lean) prove that on every group of eight states they compute Plonky3's width-16 and width-24 permutations, read in the spec field, and leave the rest of the buffer unchanged. 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 cubes below 2 p (cubeLazy) 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. Single thread, on an 8-core Ryzen 7 3700X: about 157 ns per width-16 permutation and 255 ns per width-24 one, 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).

• 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. For matrices of one height, the tree is VCVio's verified Merkle tree (CompStark/Merkle/VCVio.lean): 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 ArkLib's revision with small fixes for Lean v4.35's Mathlib. 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 is quartic only. 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 random-oracle model, 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/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), the quartic extension Ext4 p (Binomial4 p), 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, opened values and rows batched by powers of α. 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), 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 (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), vectorized word kernels (CompStark/Stark/Words.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 the four coordinate planes, every column word read once, Words.mulAdd4x4Into), FRI's folds of any arity as one kernel (Backend.fold, Fri.foldOnce: arity 2 on planes, 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 coordinate planes with inverse denominators by the norm (CompStark/Stark/ExtWords.lean) 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, it is on par with Plonky3 on 16 threads: about 333 ms against 345 ms for $2^{16}$ rows, 99 ms against 88 ms for $2^{14}$, 1.14 s against 1.20 s for $2^{18}$; with one worker thread about 1.32 s against Plonky3's 1.96 s on one thread for $2^{16}$, 0.36 s against 0.49 s for $2^{14}$ and 4.8 s against 7.9 s for $2^{18}$ (medians of three interleaved rounds on a shared 16-core host under load) (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 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 (Ext4 p) 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 with a fourth root of unity (2 ≤ twoAdicity, for the norm) whose largest domains of extension elements are addressable (DomainsAddressable); KoalaBear.prove_fast discharges both. 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, read back by traceValues): 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 256 rows in the extension's bit-reversed order on the group machine (Prog.groupMachine, CompStark/Stark/ProgGroup.lean): the block's four 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 four words to the four accumulators in one pass, 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. backendFor kernels runs a quotient's program by the kernel of kernels 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), with a parallel trace generator writing row chunks of packed words, checked row by row against upstream's generate_trace_rows. 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). The verifier accepts it, and the fast prover from the generated trace and the specification prover reproduce it (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), whole proofs from the generated trace, medians of three interleaved rounds on a shared Ryzen 7 3700X (8 cores, 16 threads; load averages 3 to 11), against Plonky3 built for the native CPU: on 16 threads 0.99 s against Plonky3's 0.84 s for $2^{15}$ rows, 1.96 s against 1.82 s for $2^{16}$, 3.85 s against 4.52 s for $2^{17}$, and 8.2 s against 10.9 s for $2^{18}$ (one round); on one thread 3.43 s against 2.05 s for $2^{14}$ and 6.93 s against 4.07 s for $2^{15}$ (two rounds). Trace generation takes 56 ms, 110 ms and 234 ms against Plonky3's 23 ms, 43 ms and 85 ms on 16 threads. By phase on 16 threads at $2^{16}$ (CompStarkBench keccak-phases 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. 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 proof peaks at 1.5 GB, 2.8 GB, 5.1 GB and 9.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, within a 12 GB limit at $2^{18}$. The fast verifier takes about 50 ms against Plonky3's 11 ms, the specification verifier about 155 ms. The benchmarks: CompStarkBench keccak LOG_N REPS, CompStarkBench keccak-prove LOG_N (one proof alone in the process, for its peak memory, and the verifiers), CompStarkBench keccak-phases LOG_N, bench/rust: compstark-bench keccak-bench LOG_N REPS, and compstark-bench keccak-prove-trace LOG_N for Plonky3's phases.

• Completeness (CompStark/Completeness.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.

• Knowledge soundness (CompStark/Soundness.lean), of the STARK as an interactive oracle proof (CompStark/Iop.lean): the protocol behind verify with oracles in place of the Merkle commitments and uniform challenges in place of Fiat–Shamir. The verifier holds the extension of the AIR's preprocessed trace as oracles of its own (Setup.preprocessedWord). A prover is a trace word per column on the extension domain, quotient chunk words after α, and claimed values after α and ζ, followed by FRI on the batched DEEP word, where it may follow any strategy. 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 δ' ≥ δ.

  theorem knowledgeSoundness (S : Setup) (publicValues : List F) (prover : Prover S)
      (δ δ' : NNReal) (hδ' : (δ' : ℝ) < 1 - S.rate) :
      (∀ trace ∈ closeTraces S δ' prover.trace, ¬ S.air.Satisfied S.logN trace publicValues) →
        acceptance publicValues prover ≤ knowledgeError S δ δ'

  A Setup is a valid configuration with at least one FRI fold, whose Merkle cap fits below FRI's first commit-phase tree (capFits : capHeight ≤ logN + logBlowup - maxLogArity, which holds without caps). A STARK is a batch of one instance (Setup.toBatch), and the theorem is the batch STARK's (below) for one instance. The knowledge error (CompStark/SoundnessError.lean) has one term per challenge, with ℓ the list sizes of the trace's and the quotient's interleaved codes at δ' (Setup.listSize): ℓ (#constraints - 1) / |𝕂| for α, (ℓ² · identityDegree + n) / |𝕂| for ζ (Schwartz–Zippel on the constraint identity of each pair of candidates, and ζ landing on the trace domain), 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 δ' - 2/N, as decoding loses the up to two points of L where ζ or ζ ω_n lies; for δ ≤ δ' - 2/N at most the mutual correlated-agreement error at δ, batchingError_le_mcaError), and FRI's soundness error at δ (FriGame.error, from ArkLib's FRI query and folding analysis of ArkLib#992, after Garreta–Mohnblatt–Wagner, extended to injected inputs below). FRI is Plonky3's (CompStark/Sound/FriGame.lean): the prover commits to the batched DEEP word again and to its folds, each after the challenge before it, and the queries check them against each other and against the DEEP word. 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/Security.lean): for the Fibonacci AIR on $2^{10}$ rows with blowup 16, FRI folding by arity 2 and 110 queries, the knowledge error with FRI at δ = 15/32 - 2^{-40} and the extractor at δ' = 4227071/8388608 ≈ 0.504, beyond the unique-decoding radius $15/32$, with lists of at most two candidates by the Johnson bound, is at most $2^{-100}$ (fibonacci_knowledgeError_le, about $2^{-100.36}$ exactly). Batching all opened words by powers of one challenge needs correlated agreement for curves: mcaError_powers_le (CompStark/Sound/PowersMca.lean) bounds it by k · N / |𝕂| below the unique-decoding radius, on [BCIKS20] Theorem 6.1 for curves, vendored in CompStark/Sound/CurveBW.lean from the open ArkLib#1311 until it lands, and with a proximity loss δ < δ' the error is independent of N (batchingError_le_curve, CompStark/Sound/CurveCA.lean). 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, levelError_le, CompStark/Sound/LossyMca.lean), at the price of #folds · loss in the query term. With it, wide 64 (64 columns, degree-3 constraints, 136 opened words) on $2^{20}$ rows, blowup 4, arity 2 and 149 queries has knowledge error at most $2^{-100}$ with FRI at δ = 3/8 - 2^{-12} and the extractor at δ' = 3/8 - 2^{-15} (wide_knowledgeError_le, about $2^{-100.26}$ exactly), dominated by FRI's queries and the out-of-domain term (identityDegree + n) / |𝕂|; on $2^{21}$ rows it takes 150 queries, with the extractor at 3/8 - 2^{-14} (wide21_knowledgeError_le, about $2^{-100.16}$ exactly). Since that term grows with the list size squared, 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 101 bits at these sizes (the interactive error cannot credit grinding, which only costs a prover that pays for its oracle calls; in the random-oracle model below, grinding lifts the cap to about 118 bits); the analysis is generic in the extension field, and over the quintic one ($p^5 \approx 2^{155}$) wide 64 on $2^{21}$ rows with blowup 4 and 190 queries has knowledge error at most $2^{-128}$ (wide5i_knowledgeError_le, about $2^{-128.59}$). The non-interactive verifier is covered in the random-oracle model, next.

• Knowledge soundness of the non-interactive STARK in the random-oracle model (CompStark/NonInteractive.lean): verifyWith itself, with Merkle commitments, Fiat–Shamir and grinding, run on random oracles in place of Poseidon2's three roles (CompStark/RandomOracle.lean): the duplex challenger, which takes the capacity and the elements observed since the last squeeze and answers a new capacity and a stream of samples, so that every challenge round, grinding sample included, is one answer; the Merkle leaf hash; and the compression. A prover is any oracle computation making at most Q calls, and the extractor reads the committed trace off its hash queries (committedTrace):

  theorem knowledgeSoundness_ro (S : Setup EF) (publicValues : List F) (δ δ' : NNReal)
      (hδ' : (δ' : ℝ) < 1 - S.rate) (Q : Nat) (prover : NIProver S)
      (hQ : prover.IsTotalQueryBound Q) :
      Pr{let (proof, log, verdict) ← run S publicValues prover}[
        verdict = .ok () ∧ proof.degreeBits = S.logN ∧
          ∀ trace ∈ closeTraces S δ' (committedTrace S log proof),
            ¬ S.air.Satisfied S.logN trace publicValues] ≤
        (Q + S.verifierQueries) * roundError S δ δ' +
        hashError F S.params.capHeight (Q + S.verifierQueries)

  roundError (CompStark/NonInteractiveError.lean) is the largest error of one oracle answer: the interactive terms above round by round, with every round after α (ζ, the batching challenge, FRI's folds and queries) multiplied by the probability powFraction F bits that a uniform base element passes its grinding check, since one answer gives both the grinding sample and the round's challenges: the verifier observes the grinding witness after the round's commitment or openings, and the next squeeze duplexes once, its first sample checked and the challenge read from the next ones. This is where grinding pays: Q counts the prover's grinding attempts. The query term also carries the bias of sampleBits (+ 1/p per index). hashError F h q = (2 + 2^h) q² / |F|^8, 3q² / |F|^8 without caps (h = 0), bounds digest collisions and predictions, a commitment round's duplex call binding the 2^h digests of the cap its input observes (boundDigests), read at the offset of the round, which FRI's first fold round's input length tells apart (capFits); verifierQueries is a closed-form count of the verifier's calls. With SP1's FRI parameters (rate 1/4, arity 2, a constant final polynomial, 124 queries and 16 bits of query grinding, as in soundcalc), wide 64 on $2^{21}$ rows has roundError at most $2^{-100}$ (wideSp1_roundError_le, wideSp1_knowledgeSoundness_ro): soundcalc's 100 bits for SP1, made precise as $q \cdot 2^{-100} + 3q^2/|\mathbb{F}|^8$. With grinding at every site, the quartic extension goes further: wide 64 on $2^{21}$ rows with rate 1/4, arity 2, a constant final polynomial, 144 queries and 20, 12, 8 and 20 bits of grinding before ζ, the batching challenge, each fold and the queries has roundError at most $2^{-117}$ (wideGrind_roundError_le, wideGrind_knowledgeSoundness_ro). FRI's folds and queries dominate (about $2^{-117.37}$); the cap is constraint folding, $63/|\mathbb{K}| \approx 2^{-117.98}$, since Plonky3 does not grind before α. The theorem holds for every challenge field EF with a Challenge instance; over the quintic extension, wide 64 on $2^{21}$ rows with zkDTVM's FRI (rate 1/4, arity 2, 160 queries, 20 bits of query grinding) has roundError at most $2^{-128}$ (wide5_roundError_le, wide5_knowledgeSoundness_ro). 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. The verifier trusts proof.degreeBits, so the event, and the game's verifier (Setup.verifyRo), fix it to the setup's trace length. The preprocessed trace is part of the AIR, so of the statement: the game computes its verifying key on the oracles before the prover runs (Setup.setupRo, Plonky3's setup on random oracles), the extractor outputs only the main trace, and verifierQueries adds the setup's 2 · |L| - 1 calls to the verifier's (none, and the numbers above unchanged, without preprocessed columns).

• 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 and its trace length) 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) is the cap of one commitment to all preprocessed traces. 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) checks every instance as uni-stark does, against one α and one ζ, and makes Plonky3's shape checks; unlike Plonky3 it fixes every instance's trace length to the statement's. 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 the verifier derives the batch's layout from the AIRs, as Plonky3's keygen does for its 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 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), the rows written in parallel ranges of blocks with the accumulator from the range's start and 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 four coordinate nodes and products over X⁴ = W (Prog.compileExt), 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 6.0 s against 6.3 s for Plonky3's prove_batch on 16 threads, and 26.7 s against 42.0 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 2.1 s against 1.7 s on 16 threads, and 10.9 s against 12.7 s on one thread (medians of six interleaved rounds on 16 threads and three on one thread, each run started on a shared 16-core host with a one-minute load below 4, single wide rounds on 16 threads ranging 5.5–6.5 s and 5.8–11.1 s; 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).

• Completeness of the batch STARK (CompStark/BatchCompleteness.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 (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).

• Knowledge soundness of the batch STARK (CompStark/BatchSoundness.lean), as an interactive oracle proof (CompStark/BatchIop.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. 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 FRI runs on the tallest batched word and injects each shorter one when its folds reach that size (friAcceptanceWith). The extractor outputs one trace per instance, each list-decoded from its committed trace (Batch.closeTraces):

  theorem batchKnowledgeSoundness (S : Batch.Setup EF withLookups)
      (publicValues : Fin S.k → List F) (prover : Batch.Prover S) (δ δ' : NNReal)
      (hδ' : (δ' : ℝ) < 1 - S.rate) :
      (∀ traces ∈ Batch.closeTraces S δ' prover.trace, ¬ S.Satisfied traces publicValues) →
        Batch.acceptance publicValues prover ≤ Batch.knowledgeError S δ δ'

  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/BatchSoundnessError.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 proved in CompStark (CompStark/Sound/FriInject.lean, CompStark/Sound/FriGame.lean), from ArkLib's query analysis (Fri.FoldTrace): 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, lossyInjectFailure_prob_le), and on a run without a bad fold, a large set of passing queries gives agreement down to every injected word (exists_codeword_agree_on_lossy), so FRI rejects when any input is far (FriGame.acceptance_le). 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) 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 (S : Batch.Setup EF withLookups)
      (publicValues : Fin S.k → List F) (prover : Batch.Prover S) (δ δ' : NNReal)
      (hδ' : (δ' : ℝ) < 1 - S.rate) (hbound : S.HeightBounded)
      (hcounts : ∀ i, (S.air i).CountsBounded (S.logN i)) :
      (∀ traces ∈ Batch.closeTraces S δ' prover.trace,
        ¬ S.SatisfiedWithInclusion traces publicValues) →
        Batch.acceptance publicValues prover ≤ Batch.knowledgeError S δ δ'

  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/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, rangeKnowledgeSoundness_ro). 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) on $2^{20}$, $2^{19}$ and $2^{16}$ rows over the quintic extension, with blowup 4 and 190 queries, have knowledge error at most $2^{-128}$ (wideBatch_knowledgeError_le, about $2^{-128.39}$ exactly, the lookup challenges about $2^{-130.98}$). The random-oracle model of the batch follows.

• Knowledge soundness of the non-interactive batch STARK in the random-oracle model (CompStark/BatchNonInteractive.lean), LogUp lookups included: verifyBatchWith itself run on the same three oracles as the STARK (CompStark/BatchRandomOracle.lean), the batch's common data, the commitment to the instances' preprocessed traces, computed on the oracles before the prover runs (Setup.setupRo, Batch.commonWith), and the extractor reading every instance's trace off the prover's hash queries under the main commitment, at the instance's offset among the matrices of its height (committedTraces); the permutation traces the analysis needs on the way are read off the queries under the permutation commitment:

  theorem batchKnowledgeSoundness_ro (S : Setup EF) (publicValues : Fin S.k → List F)
      (δ δ' : NNReal) (hδ' : (δ' : ℝ) < 1 - S.rate) (Q : Nat) (prover : NIProver S)
      (hQ : prover.IsTotalQueryBound Q) :
      Pr{let (proof, log, verdict) ← run S publicValues prover}[
        verdict = .ok () ∧ proof.degreeBits.toList = List.ofFn S.logN ∧
          ∀ traces ∈ closeTraces S δ' (committedTraces S log proof),
            ¬ S.Satisfied traces publicValues] ≤
        (Q + S.verifierQueries) * roundError S δ δ' +
          hashError F S.params.capHeight (Q + S.verifierQueries)

  roundError (CompStark/BatchNonInteractiveError.lean) is the largest error of one oracle answer: the lookup challenges (lookupError, credited with the lookup grinding), α, ζ and the batching challenge at their worst instance (its folding and out-of-domain errors, and the batching of its domain size's opened words), each FRI fold with the shorter instances' words injected (Rounds.foldErrorAt, the summand of friErrorWith), and the queries, every round after α credited with its grinding. verifierQueries counts the setup's calls (at most four per leaf of the preprocessed traces' tree) and the verifier's, a leaf hash, a compression per level and a hash and a compression per injected height for every opening of a commitment; it is computable, and its closed forms are checked by decide +kernel. hashError F h q = (2 + 2^h) q² / |F|^8, as for the STARK: a duplex call's key protects its capacity and the cap's digests its input binds (boundDigestsB); a batch Setup's cap fits every instance's first FRI tree (capFits), so every round's cap has 2^h entries. The permutation commitment and the terminals may have the length of FRI's first fold round's input, so the second round is told apart by its capacity instead, an answer to a call on the initial capacity among the queries before (initAnswers, noClash_initAnswers): a capacity that a key holds is answered before it, unless a fresh answer clashes. The proof (CompStark/Ni/Batch*.lean) follows the STARK's: the batch IOP's rounds are events on the transcript round by round (CompStark/Sound/BatchRbr.lean, FRI fold by fold in CompStark/Sound/FriRun.lean), the commitments bind the trees of mixed heights the prover committed to (Merkle/ExtractMixed.lean, Ni/BatchBind.lean), and the verifier's checks hold for the extracted transcript (Ni/BatchBcs.lean). It is not the single theorem's generalization: the batch verifier's transcript and checks differ from verifyWith's, so the two theorems are proved side by side. Concretely, the three wideBus 64 instances above with zkDTVM's FRI over the quintic extension (160 queries, 20 bits of query grinding) have roundError at most $2^{-128}$ (wideBatch5_roundError_le, wideBatch5_knowledgeSoundness_ro, verifierQueries = 99669), and over the quartic extension with 144 queries and grinding at every site, as wideGrindSetup, and 18 bits before the lookup challenges, at most $2^{-117}$ (wideBatchGrind_roundError_le, wideBatchGrind_knowledgeSoundness_ro, verifierQueries = 89692); the quartic extension cannot do better, constraint folding, which Plonky3 does not grind, being about $2^{-117.89}$. A fold by $2^k$ that injects a word batches $2^k$ words besides the first instead of $2^k - 1$. With lookup inclusion, batchKnowledgeSoundness_ro_inclusion gives the same bound with S.SatisfiedWithInclusion in place of S.Satisfied, for AIRs that bound their query multiplicities (hcounts, as above); the multiplicity bound needs no hypothesis here, since an accepting verifier checked it.

• Security calculator (CompStark/SecurityCalculator.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 and an Analysis (FRI's radius δ up to the unique-decoding 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/Sound/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 the MCA and the curve bound, and FRI's folds read off Plonky3's schedule as a plan of folds (FriGame.Rounds.plan: each fold's arity, the domain it folds onto, and whether it injects a word). S.Secure p A bits (and S.SecureRo p A bits per oracle answer, and the batch's) says that the analysis fits the setup 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 (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/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/Security.lean):

  theorem knowledgeSoundness_of_secure (S : Setup EF) (hp : Nat.card F = p) (A : Analysis)
      {bits : ℕ} (h : S.Secure p A bits) (δ' : NNReal) (hδ' : (δ' : ℝ) = A.δ')
      (publicValues : List F) (prover : Prover S) :
      (∀ trace ∈ closeTraces S δ' prover.trace, ¬ S.air.Satisfied S.logN trace publicValues) →
        acceptance publicValues prover ≤ (2 ^ bits)⁻¹

  and likewise knowledgeSoundness_ro_of_secureRo, batchKnowledgeSoundness_of_secure and Batch.batchKnowledgeSoundness_ro_of_secureRo (with knowledgeError_le_of_secure, roundError_le_of_secureRo and the batch's for the errors themselves). Every concrete bound above is such a check (fibonacci_secure, wide_secure, …, wideBatchGrind_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 radius δ stays at most the unique-decoding radius (1 - rate) / 2: FRI's folds and the batching of the opened words rest on correlated agreement for the powers of one challenge, which is proven there (CompStark/Sound/CurveCA.lean, LossyMca.lean, PowersMca.lean). Beyond it, correlated agreement in the list-decoding regime up to the Johnson bound ([BCIKS20] Theorems 1.4 and 1.5, for lines and curves) is stated in ArkLib with sorry (BCIKS20/AffineLines/Main.lean, BCIKS20/Curves.lean) and not used; ArkLib's proven bounds beyond unique decoding, for lines and powers (after Gao–Kopparty–Lovett and Bafna–Choudhary–Guruswami–Mardia, ProximityGap/CapacityBounds/JohnsonMca.lean, Powers.lean), reach only 1 - (rate + η)^{1/(k+2)} for k + 1 words, below the unique-decoding radius at rates $1/2$ and $1/4$ and for the thousands of words batching combines. 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.

  Plonky3's Keccak example (tests/CompStarkTests/KeccakSecurity.lean): KeccakAir, 3182 constraints of degree 3 over 2633 columns, every column opened at the next row, on $2^{15}$ to $2^{18}$ rows 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 has 52 proven bits per oracle answer and 36 interactively (example_secureRo, example_secure). 100 bits over the quartic extension take 203 queries per oracle answer and 244 interactively at blowup 2, 124 and 149 at blowup 4; the out-of-domain term caps the quartic extension at 104 to 107 bits on these heights, so 128 bits take the quintic extension, with 270 and 310 queries at blowup 2 and 166 and 190 at blowup 4.

Security of your own AIR

1. Build a Setup (or Batch.Setup) for your AIR, trace length and FRI parameters, at any folding arity.

2. Let the calculator search the analysis, and read the bits of each term:

   #eval mySetup.knowledgeErrorReport 2130706433 (mySetup.bestAnalysis 2130706433)
   #eval mySetup.roundErrorReport 2130706433 (mySetup.bestAnalysisRo 2130706433)

   The report shows the analysis it found: FRI's radius δ, the extractor's δ' and the loss. Change the FRI parameters until the total reaches your target, or pick an analysis by hand: δ ≤ (1 - rate) / 2, δ ≤ δ' - 2/N, δ' below the Johnson radius 1 - √rate, and a positive loss (fits: false otherwise).

3. Check it in the kernel and apply the theorem (KoalaBear.card_eq : Nat.card F = 2130706433), with the analysis the search found written out:

   def myAnalysis : Analysis := ⟨3/8 - 1/2^14, 3/8 - 1/2^17, 1/2^19⟩
   theorem my_secure : mySetup.Secure 2130706433 myAnalysis 128 := by decide +kernel
   theorem my_knowledgeSoundness (publicValues : List F) (prover : Prover mySetup) :
       (∀ trace ∈ closeTraces mySetup (49151 / 131072 : NNReal) prover.trace,
         ¬ mySetup.air.Satisfied mySetup.logN trace publicValues) →
         acceptance publicValues prover ≤ (2 ^ 128)⁻¹ :=
     knowledgeSoundness_of_secure _ KoalaBear.card_eq _ my_secure _
       (by norm_num [myAnalysis]) publicValues prover

   The kernel can also run the search itself (mySetup.Secure 2130706433 (mySetup.bestAnalysis 2130706433) 128 := by decide +kernel), at a few hundred evaluations of the bound. For a large AIR, prove its shape once (shape_eq_of_profileFits) and certify with secure_of_shape, as tests/CompStarkTests/KeccakSecurity.lean does for Keccak.

   The kernel evaluates the AIR's structure but never a field operation; keep every number of the check in Nat and ℚ.

Building

lake exe cache get   # Mathlib's prebuilt oleans
lake build
lake test

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-trace INPUTS the trace known answers, 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 and inputs, and compstark-bench lde LOG_N WIDTH times Plonky3's trace extension.

Later

• 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.

Roadmap

1. Plonky3's multi-table STARK: batch-stark with preprocessed columns and LogUp lookups (done, sound interactively and in the random-oracle model).
2. Binary fields, following leanVM: a binary tower field, WHIR, and Binius-style ring switching.
3. Multilinear proving, following SP1 Hypercube: zerocheck by sumcheck, LogUp-GKR, and Basefold behind the jagged commitment, over KoalaBear with Poseidon2.