components.md

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

• 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 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), 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, 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), 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.3 GB, 2.2 GB, 3.9 GB and 6.8 GB of memory on $2^{15}$ to $2^{18}$ rows, the trace transposed for its extension in ranges of 256 columns that are freed as they are extended, 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, CompStarkBench openings-phase LOG_N REPS (the values at the out-of-domain points and the batched reduction of the trace's extension), bench/rust: compstark-bench keccak-bench 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 δ (FriRounds.error, the error of ArkLib's interaction-layer FRI certificate, Fri.Interaction.error, 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, 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, lossyLevel_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) 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), 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/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; CompStark's rounds with injected inputs (CompStark/Sound/FriRounds.lean, CompStark/Sound/FriInject.lean) carry the same error (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 (FriRounds.Rounds.Fits, FriRounds.Rounds.schedule). 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, FRI with the shorter heights injected in Fs/FriInjected.lean), which give the batch's terminal (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 (FriRounds.Rounds.plan: 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 (FriRounds.Rounds.plan_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 the lossy and curve bounds of CurveCA.lean and LossyMca.lean), 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-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.

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.