Repository navigation
feat(labinius): polynomial commitment for binary and prime evaluation claims - #229
Merged
Merged
Conversation
Add SisModulusProfileId::Q128Offset275, the exact SIS modulus profile for q = 2^128 - 275, the modulus of jolt_field::Prime128Offset275. No preset selects it and no checked-in schedule artifact names it. The profile has its own modulus, name, catalog tag 5 and descriptor tag 4. It owns no generated SIS rows: SisModulusProfileId::row_owner maps it to Q128OffsetA7F7 and every row lookup resolves a profile through it, so the SIS table digest, existing commitments and schedule catalogs are unchanged. specs/sis-quantum128-scalar-n-table.md states when sharing the rows is sound. CommittedGroup decoding now rejects a matrix profile whose modulus is not the field's. It compared bit widths only, which the two 128-bit profiles share.
CommittedGroup::check compared the matrix profiles with the field by bit width only, so a commitment whose inner or outer matrix named the other 128-bit profile passed check and serialized to bytes the decoder rejects. check and the decoder now both call check_exact_field_modulus, which replaces the per-matrix comparison inside the decoder. The end-to-end test rebuilds the inner matrix, the outer matrix and both under the other profile and requires check and serialization to reject each.
… evaluations Adds to the `labinius-trinomial` feature: - `TrinomialLimbDomain`, `TrinomialLimbSlots` and `TrinomialLimbAccumulator`: exact arithmetic in `Z_p[Y]/(Y^648 - Y^324 + 1)` for four admitted primes below `2^28`, in signed 32-bit lanes with lazy reduction. The forward transform takes centered coefficients or 648 packed bits; a NEON backend and a portable backend return the same representatives. The magnitude bound of every retained stage is stated in the module and checked by shadow tests at extremal signs for every admitted prime. - `shifted_remainder_evaluations`: the values `(B * Y^t mod Phi)(alpha)` for all `t < D` over any field, by a one-term recurrence with no root of unity. Changes in the `labinius-binary` feature: - The packed F162 round-product and fold kernels take borrowed limbs, and with `parallel` both split tables above 16,384 elements into chunks. The parallel fold folds each chunk in place and then compacts. - With `parallel`, the field-switch partials, coefficients and equality weights split the same way. `SwitchField` and its `Source` now require `Send + Sync`. Nothing outside the crate calls the new items yet.
The chunked round-product, fold and field-switch kernels compile only with `parallel`, and no job built `akita-algebra` with `labinius-binary` and `parallel` together, so their tests never ran in CI.
The NEON limb backend compiles only on `aarch64`, and the job that tests `labinius-trinomial` runs on x86-64, so its tests against the portable backend never ran in CI.
The phase breakdown took its column by index and wrote a fixed prime into the Criterion group name, and the two disagreed. Select the column by prime and derive the group name from the column's domain. Run the rank sweep and the phases on the LaBinius commitment prime, and the other admitted primes at one rank.
Sizes the LaBinius root over q = 33,568,993 in Z_q[Y]/(Y^648 - Y^324 + 1): root shape and encoding, the fold-response and commitment-lift bounds, the proof-prime admission check, and the certified width cells for ranks 2 to 4. The estimator's staged profile becomes the commitment prime.
Add akita-labinius-verifier and akita-labinius-prover behind the labinius feature, off by default. They commit a binary source over the commitment prime and reduce an opening of that commitment, to a binary claim, a prime claim or both, to evaluation claims on committed digit tables. The claims leave through an oracle trait; only a transparent test oracle is included. The reduction is generic over a base prime field and a challenge field. Every challenge in the challenge field is a site of a grinding plan priced by Akita's loss functions, and a channel without a scheduled plan rejects round challenges. akita-types: PreparedTrinomialASetupWeights gains contract_matrix and loses modulus_evaluation, for the lowered layout. Specifications: root admission, setup contract, lowered root relation, root sumchecks, root reduction and the clear opening. Register both crates in the workspace, the crate-dependency script, the crate graph, the Book's crate table and one CI job on both transcript backends.
…s on dev The parallel fold copied 21 bytes per source word on the calling thread before every attempt, for a Sync bound that SwitchField::Source already carries. Rows now embed their words in the worker, as the serial path does, and the allocation-failure fallback that guarded the copy is gone. The rewrite of PreparedTrinomialASetupWeights had no caller: the lowered layout uses only TrinomialASetupView::new and its row count. Restore trinomial.rs and its bench to the dev versions, so this branch no longer changes akita-types.
… claims Add the opt-in crate akita-labinius-pcs. It discharges the evaluation claims of the root reduction with one nested Akita grouped opening over the image digits, the response digits and, for a prime claim, the prime left opening. It is generic over two proof-field families, Family64 and Family128, and ships a digit catalog and an element catalog for each in both protocol directories, with their offline generator. Register the crate: workspace member, dependency check, crate graph, the Book's crate table, the preflight list, a catalog drift job and a PCS test job. Extend the setup contract with the matrix-seed derivation of the PCS composition.
github-actions
Bot
added
spec
Documentation blast radius (advisory)These regions may need doc/spec/book updates based on changed paths. Changed files in this PR: 41
|
This was referenced Oct 10, 2026
…181) * docs(book): complete core commitment and opening chapters * docs(book): distinguish terminal Linf and L2 admission * docs(book): fix math rendering and clarify matrix views * docs(book): clarify claim reduction versus recursive witness size * docs(book): align implementation maps and setup offloading * docs(book): clarify fold progress and address review feedback
* fix: keep ring-switch event expansion in CPU consumers * fix: derive lazy CPU packing events from shared semantics
…decomposed digits (#237) * refactor(cpu-backend): delete the dense i8 mirror and commit-side predecomposed digits DensePoly no longer builds the serial small-i8 coefficient mirror; its only reader was the single-digit dense fold, which now uses the opening digit cache or live balanced decomposition of the same values. The commit-side PredecomposedDigits representation duplicated the dense field commit path. Recommits of an opened source now decompose the field values live, producing the same digits. DenseDigitCache remains the opening-side cache. * refactor(cpu-backend): fold the digit matvec into its only entry point mat_vec_mul_digits_i8_with_params always checked for zero planes, so its generic implementation, the CHECK_ZERO parameter of the two digit block-parallel helpers and the unchecked accumulation loop had no caller.
… BlockDigits seam (#238) * refactor(cpu-backend): route dense commit, fold and packing through a BlockDigits seam Add a crate-private `BlockDigits` seam in `sources/block_digits.rs` with `RingValueSource` as its supertrait. Cached digit planes, live rings, packed digits and pre-split digit rows implement it, and each supplies only the views it has (ring values, digit planes, i8 or i16 rows). Dense commit now builds one `LiveRings` source and calls `commit_rows` with the validated signed-digit kernel; `commit_rows` routes to the exact-i16 path or the block-batched i8 NTT matvec. Sparse decompose-fold uses `element_partitioned_decompose_fold` over either cached or live digits, and coefficient packing reads ring values through `RingValueSource`. Removes the per-source copies of the i8 matvec driver, the test-only `dense_commit_rows` shim and `DenseCommitInput`. Proof bytes are unchanged. * refactor(cpu-backend): split BlockDigits capabilities and batch ring decode BlockDigits, I8Rows and I16Rows are now separate traits, so each source implements only the views it supplies instead of erroring defaults. DigitRows indexes its block directly, and the i8 block drivers decode a pointwise-dot batch of rings at a time. Fold tests move to fold_tests.rs.
…lockDigits seam (#239) `PackedDigits` now supplies one-digit i8 and i16 rows and ring values. The recursive commit uses the shared block i8 driver with an `I8CommitPolicy` that keeps the per-block-tiled versus block-parallel choice; raw single-digit blocks use the digit LUT with a CRT bound taken from each block's rows. The one-digit exact-i16 commit, recursive sparse decompose-fold, coefficient packing and integer `evaluate_and_fold` run on the same seam. Removes `PackedI8Lift`, the packed and raw i8 matvec drivers and their NTT entries, `packed_tight_digit_fold_partitioned` and the recursive packing adapter. Proof bytes are unchanged. The coefficient-packing kernel and the standalone bench share one `suffix_witness_coefficient_packing_partials` helper.
…ger blocks (#240) Adds `SignedBlocks`, `SignedBlockDecoder` and the owned `SignedBlockPoly` to `custom_source`, with `AvailablePolynomialTypes::signed_blocks()` and `PolynomialRepresentation::signed_blocks`. A source can offer borrowed i8 or i16 coefficients, or a deterministic i8 decoder, in the flat order of `DensePoly::from_field_evals`, zero-extended to `2^num_vars`. `SignedBlockPoly` owns its values and imports as a backend source like `DensePoly`. Signed blocks implement `BlockDigits`, `I8Rows` and `I16Rows`: commits use the dense routing of `commit_rows`, opening folds and coefficient packing use the shared entries, and multi-digit rows come from the new `BalancedDecomposePow2Params::decompose_small_signed_into`. Commit fills check every live value against the schedule's accepted coefficient interval, which the owning backend threads to the inner commit as `AcceptedReach`. `SignedBlockPoly` computes the least and greatest coefficient once, in parallel and in the storage type, and caches them: admission derives the centered reach from them, and the commit uses them to prove that every row fits one digit or that the table meets the accepted interval, without a second pass over the values. The recursive multi-digit commit decomposes packed digits through `DecomposedPackedDigits` and routes through `commit_rows`, replacing the `F::from_i8` lift. Proof bytes for existing sources are unchanged.
) * fix(planner): gate evaluation modes on chunking Require coefficient packing and quotient lift throughout multi-chunk folds, without a minimum two-fold prefix on single-chunk paths. Preserve canonical extension-field root packing and support eligible base-field root trace replay. Regenerate catalogs and update admission checks, exact-search regressions, and documentation. * test: refresh planner catalog regression fixtures Update dense fp64 dimensions and the one-hot grinding-plan snapshot for the newly selected schedules. Use recursive fp64 rows to preserve the norm-route representative-selection regression, checking that norm routes are their only shape difference. * fix: align planner fixtures and eligibility contracts Remove remaining absolute-level restrictions from the reduced-evaluation specifications and implementation checklist. Require single-chunk direct evaluation trace throughout the suffix. Retarget the packing fixture from a grouped quotient successor and recompute its group arity. Reject extension roots and explicitly multi-chunk recursive evaluation trace at executable row admission. Keep the combined-family setup test on catalog sizes with distinct matrix capacities. * fix(planner): retain mandatory two-fold packing prefix Require packing and quotient lift at L0, L1, and every multi-chunk fold. Keep later single-chunk opening choices and the monotone reduced-evaluation suffix. Remove root evaluation-trace support, refresh catalogs and documentation, and allow cold transcript CI builds sufficient time. * test: cover setup-prefixed packing at level two Extend the checked packing fixture to consecutive setup-prefix consumers, with unsliced B commitments after level one. Prove and verify the explicit single-chunk L2 packing-plus-prefix schedule in both bases. Align remaining Book and specification passages with mandatory L0/L1 packing. * refactor(planner): fix root relation mode to quotient lift Remove root relation-domain inputs, the one-choice mode loop, and unreachable root trace/reduced branches in the reference search. Preserve recursive relation-mode selection and canonical runtime admission. * refactor(test): separate packing fixture construction Move packing-specific support out of the shared module. Build roots, complete setup-prefixed successors, frozen prefix groups, and terminal geometry at substantive module boundaries. Retain both L1 and L2 packing roundtrips in both opening bases.
* refactor: make witness chunking a runtime catalog policy * fix: pass runtime geometry in transcript catalog tests * fix: enforce catalog witness geometry during admission * fix: carry requested geometry through catalog generation
…iers (#189) * chore(deps): pin Jolt at the a16z/jolt#1911 head The guest inline backends and the row-kernel verifier paths use Jolt APIs added in a16z/jolt#1911: jolt-inlines-ntt, Blake2b::update_block_eager, and jolt-field's dot_base_rows, weighted_dot_base_rows, signed_sum, and sum_of_products::<K>. The pin is e19eda725, the first revision with the generalized sum_of_products. Repin to the merge commit once that PR lands. * feat: Blake2b, Keccak, and NTT inline backends for RISC-V guest verifiers Opt-in features route a guest verifier's hot primitives through Jolt inlines, which the Jolt zkVM expands into short proved instruction sequences instead of running the portable code. Every backend produces the same bytes or values as the portable path. Only riscv64 selects an inline; other targets, and default features, keep the portable paths. - blake2-inline: the Blake2b transcript sponge and descriptor digests over jolt-inlines-blake2. The sponge compresses each phase's constant 128-byte mask block once and clones the prepared hasher. It is exported as InlineBlake2bSponge so a host with the inline's software path (Jolt) pins it against spongefish's Blake2b512 byte for byte. - keccak-inline: Keccak-f[1600] for the SHAKE challenge samplers over jolt-inlines-keccak256. - ntt-inline: the 64-point i32 negacyclic NTT and the six-product pointwise dot over jolt-inlines-ntt, writing aligned residues with doubleword stores. One predicate (inline_ntt64) decides when the inline serves a width and degree. A host test pins the tables handed to the inline against the portable transform, and a CI lane runs it. * refactor: one transcript sponge, plan-selected NTT inlines, one XOF cursor - The guest transcript is spongefish's Blake2b512 sponge over the jolt-inlines-blake2 digest adapter, replacing the hand-written state machine; the adapter is pinned against the blake2 crate in Jolt. - NttKernelPlan gains a JoltInline kind, detected for i32 residues on a riscv64 guest with ntt-inline. Transforms, the centered-i16 converter, and the lazy i32 dot all dispatch on the prepared plan, so the SCALAR plan runs the portable kernels on every target. - The portable lazy dot is an explicit i32 kernel over the shared reduce_i32 Montgomery step. - XofCursor owns the squeezed SHAKE256 state and position directly; the separate reader is gone. - CI cross-checks akita-pcs for riscv64 with all three inline features, which compiles every guest-selected path; the pre-existing riscv64 unused-plan and dead-field warnings are fixed so it runs under -D warnings. * fix(ntt): build the R^2 twist table wherever transform_inline compiles transform_inline also compiles under cfg(test) with ntt-inline on any target, but psi_pows_r2 existed only on x86, AArch64, and riscv64, so unit-test builds elsewhere failed. The table's cfgs now match. * fix(ntt): take the packed residue store only on little-endian targets * fix(algebra): drop the dead-code expectation main's signed-block decomposition fulfils --------- Co-authored-by: Taghi B. <mtbadakhshan@gmail.com>
…186) * feat(verifier): view trusted setup and terminal NTT caches in place A verifier running as a RISC-V zkVM guest pays per instruction to copy and range-check setup payloads it already trusts. Trusted, uncompressed bytes that outlive the program can now be used where they lie: - AkitaVerifierSetup::borrow_trusted views the public matrix in place (FlatMatrix::borrow_trusted_with_expected_shape over AkitaDeserialize::borrow_many_trusted); coefficient_offset reports where the matrix begins so a caller can align it. The views take a TrustedBytes token: the words are used as field elements without a range check, and constructing the token (unsafe) is where the caller vouches that they are canonical. Little-endian targets only. - TrustedTerminalCache::View uses a scalar Q128 terminal NTT cache artifact without a copy or a residue range pass; TrustedTerminalCache::Decode keeps the existing checked copy. AkitaVerifier::for_selection takes Option<TrustedTerminalCache>. - Field arrays deserialize with one bulk read into initialized element storage, then the single-element rule per word (checked, or reduced for Validate::No); a test pins bulk against per-word decoding. docs/security-posture.md records the justification for the unsafe views, and the proof-input guardrail pins the files that may use them. Both views are trusted inputs: the matrix and residues are taken as seed-derived without re-deriving them, so the caller binds the bytes to setup provisioning or to the verifier program identity. The descriptor and prefix registry are still validated. The profile recursion host and guest pass TrustedTerminalCache::Decode, keeping their checked copy. * fix(verifier): bound bulk field decode and close in-place view review gaps - Bulk field decode grows its storage one 4096-element chunk per read, so a forged element count costs memory only for bytes that arrive; the per-element default reserves at most one chunk up front. A header-only run of 2^40 elements now fails as a truncated read. - AkitaVerifierSetup::borrow_trusted decodes the prefix registry exactly, so bytes after the setup are rejected (0x00 and 0xa5 suffix tests). - The scalar Q128 cache decoder is portable again (per-word little-endian fixup on big-endian targets); only the in-place view, whose words must already be in memory order, rejects a big-endian target. - The copying and in-place flat-matrix decoders share one expected-shape and field-count check. * fix(serialization): grow decoded runs fallibly per chunk The trait-default bulk decode reserved only its first chunk fallibly; later growth went through Vec::push and aborted on allocation failure. It now reserves each chunk with try_reserve_exact before filling it. The forged-count regression test uses usize::MAX so it compiles on 32-bit targets, and the big-endian prepared-cache fallback imports MontCoeff.
…S16) (#232) * feat(sis-estimator): price FIPS 204 ML-DSA MSIS instances under the Akita policy model Co-Authored-By: Claude <noreply@anthropic.com> * feat(sis)!: raise the SIS policy gate to 169 quantum Core-SVP bits Replace Quantum128BitADPS16 (tag 1) with Quantum169BitADPS16 (tag 2). 169 bits is the ADPS16 quantum Core-SVP cost of forging ML-DSA-65 (FIPS 204, NIST category 3): its UF-CMA SelfTargetMSIS instance needs BKZ block size 638. The infinity and Euclidean table targets both read the policy constraint. Generated tables are regenerated separately. Co-Authored-By: Claude <noreply@anthropic.com> * feat(compression)!: double the compression ladder for the 169-bit SIS gate At 169 bits a rank-one negative-binary map no longer admits the old ladder widths: q128 D=8 accepts 165 columns where the terminal map needs 256, and D=16 accepts 2400 where an 8 KiB source needs 4096. Every profile fails by the same factor. Doubling every ladder dimension restores both maps with wide margins (q128: D=32 accepts 60460 of 2048 needed, D=16 accepts 2400 of 256) at the cost of a 256-byte terminal image. The compression policy becomes V4 (tag 4). Co-Authored-By: Claude <noreply@anthropic.com> * chore(sis): regenerate SIS tables and goldens at 169 bits Regenerate the coefficient L-infinity table (21,100 ring-origin rows, 5,128 exact boundaries), the Euclidean L2 table, the compression certificate, the infinity smoke table, and the Euclidean goldens under Quantum169BitADPS16. The B = 1 rows reproduce the compression cells. Co-Authored-By: Claude <noreply@anthropic.com> * docs: describe the NIST category 3 SIS policy and 256-byte compression terminal Add the sis-nist-level3-policy spec with the collected FIPS 204, Dilithium round-3, and Kyber round-3 reference parameters, the estimator calibration against ML-DSA, the 169-bit decision, the compression ladder change, and the Fiat-Shamir parameters left at 128 bits. Update the book, planner README, and SIS golden runbook. Co-Authored-By: Claude <noreply@anthropic.com> * chore(schedules): regenerate every schedule artifact under the 169-bit policy All 115 catalog rows still plan. catalog_security --check prices every row at 169.07 bits (BKZ block size 638). Proof bytes rise 13-17% for almost every row; the evidence directory records the complete comparison with main. Co-Authored-By: Claude <noreply@anthropic.com> * docs(evidence): record the 169-bit catalog comparison and measured benchmark Co-Authored-By: Claude <noreply@anthropic.com> * fix(compression): admit only B/D ring dimensions the first ladder map divides Recomposition rebuilds each B/D ring element from whole first-map digit blocks, so the first compression dimension must divide the source dimension. The q32 ladder now starts at D=128, and the planner admitted compressed D=64 B/D images that failed at proving time with a malformed recomposition geometry. Planner admission, payload geometry, and setup-prefix compression now share one predicate. Move the remaining compression-dimension and 169-bit boundary fixtures to the new ladder and tables. Co-Authored-By: Claude <noreply@anthropic.com> * chore(schedules): regenerate fp32 one-hot rows after the compression admission fix Two fp32 one-hot rows move their compressed B/D images off D=64; proof and setup sizes are unchanged. catalog_security --check still prices all 115 rows at 169.07 bits. Co-Authored-By: Claude <noreply@anthropic.com> * test: move catalog-shape and table-boundary fixtures to the 169-bit catalogs Point the dynamic-backend, portable-import, combined-recursive, and setup-prefix challenge-hook tests at the smallest shipped rows that still exercise their feature (fp128 one-hot nv20x4, fp32 one-hot nv20, fp32 dense recursive nv28, the W8R3 recursive family). Move q32 setup-prefix and packing fixtures to D=128 compressed images, and update pinned snapshots, digests, and matrix shapes. Co-Authored-By: Claude <noreply@anthropic.com> * wip: planner fixtures under the 169-bit tables * wip: remaining planner fixtures * test: price the nv28 fp32 recursive opening without a 2^28 weight table The combined-recursive smoke now runs at nv28, the smallest fp32 recursive row that opens a setup prefix. Its affine table has a closed form opening, so the test no longer builds 2^28 Lagrange weights (above the verifier sequence bound). Update the W8R2 setup-prefix slot fixture (two slots under the 169-bit catalog). Co-Authored-By: Claude <noreply@anthropic.com> * test: rebuild planner fixtures that depended on 128-bit catalog shapes Move the contractive-root, setup-budget, guided-root-slice, restricted-query, adapted-skeleton, and chunk-ownership fixtures to sizes where their scenario still occurs under the 169-bit tables, and raise the reference oracle depth to five folds (small chunked schedules gain a fold). The incoming-width fixture moves to nv15 W2 at basis 4, where two consumers still emit equal witnesses. Its frontier test perturbs the wider suffix's local work by one element to recreate the reversal, which no real candidate pair in the family shows any more; the level-guard test now pins that the guard keeps both widths. Co-Authored-By: Claude <noreply@anthropic.com> * test: perturb only suffix work in the frontier reversal fixture Co-Authored-By: Claude <noreply@anthropic.com> * test: pin frontier width separation without a synthetic reversal Under the 169-bit tables the narrower successor is cheaper both locally and in the complete schedule, so collapsing the source-width key no longer loses the winner in this fixture. Assert the width key separates the two parent keys and that the winner survives either way, instead of fabricating a suffix cost. Co-Authored-By: Claude <noreply@anthropic.com> * docs: state the compression source-dimension rule Co-Authored-By: Claude <noreply@anthropic.com> * test: pin norm-route shape separation on bounded-dense rows Under the 169-bit tables the fp64 dense nv26 and nv28 rows share one schedule shape. The fp128 bounded-dense nv24 and nv26 rows still differ only in their norm route. Co-Authored-By: Claude <noreply@anthropic.com> * docs(spec): record the validation run Co-Authored-By: Claude <noreply@anthropic.com> * docs(spec): record the native AArch64 NEON kernel run Co-Authored-By: Claude <noreply@anthropic.com> * fix(planner): keep every recursive slice and prune only V5 root slices prune_locally_unprofitable_slices kept only the slice counts with the smallest padded setup at every level and under both objectives. That is exact only at the root under MinFirstDirectSetupThenExactProofAndWorkV5, where the root is the first direct edge and its padded setup leads the objective. A recursive fold's setup enters V5 only after proof bytes and work, and the V6 envelope is a schedule-wide maximum another level can tie, so both prunings could discard the complete winner. The fp128 one-hot W8 nv20 oracle case exposed it: the planner never generated the 256-position single-slice first fold that the exhaustive reference picks, and lost 116 proof bytes (112 at the root, 4 of nonce). Restore that case in the oracle comparison. Co-Authored-By: Claude <noreply@anthropic.com> * test: exercise guided root slices against the V5 root pruning Co-Authored-By: Claude <noreply@anthropic.com> * test(planner): restore the incoming-width tests on a 169-bit scenario The guard and frontier tests need two consumers that emit equal witness lengths, where the wider one dominates locally but loses the complete schedule through producer padding. Under the 169-bit tables the old nv16, eight-chunk, basis-2 fixture no longer had that balance, and the tests had been weakened to "keep both widths". A bounded search over this fixture family found the balance again at nv18 with two chunks and basis 4, between a 2048-position single-slice consumer and a 4096-position two-slice consumer. Every assertion from main is restored unchanged. Co-Authored-By: Claude <noreply@anthropic.com> * docs(book): describe root-only slice pruning The commitment chapter still said setup-focused selection keeps the smallest slice count at every level. After the slice-pruning fix the planner keeps every count at recursive levels and prunes only root counts under the first-direct setup objective. Explain why each objective admits or rejects that pruning. Co-Authored-By: Claude <noreply@anthropic.com> * chore(schedules): regenerate the catalog after the slice-pruning fix Regenerate every schedule artifact, the catalog snapshot, the main comparison, and the catalog security report at the fixed planner. Ten artifact files change. Every row still costs exactly 169.07 bits. Record the fix's effect in the evidence and the spec. Across all 123 planning calls, 105 are identical and 11 improve. Two layouts halve their first-direct setup, the leading objective coordinate. Two grouped rows plan against a producer row that improved, so their lookup key changed; replanning the pre-fix keys with the fixed planner reproduces the pre-fix schedules exactly. Co-Authored-By: Claude <noreply@anthropic.com> * docs(evidence): remeasure the profile benchmark at the final branch The slice-pruning fix changed two benchmarked schedules (the W2R2 and recursive W8R2 rows). Rerun all 13 cases interleaved against the same main binary and replace the table and summary. The medians stay at +16.5% proof bytes and +2.7% prove time, and the run-to-run spread is stated from the measured samples. Co-Authored-By: Claude <noreply@anthropic.com> * test(params): unroll the single remaining cutoff regression case Retiring the q32 D32 compression cell left a one-element loop, which Clippy's single_element_loop lint rejects under -D warnings. Assert the q32 D512 cell directly. Co-Authored-By: Claude <noreply@anthropic.com> * docs(evidence): record Jolt-scale planning coverage at 169 bits Plan Jolt's one-hot policies (K=16 and K=256 sources, every chunk profile, recursive setup planning) and its dense producers at trace lengths 2^30 and 2^31 with this branch's planner. All 190 shapes plan and validate; record proof, fold, and setup ranges per shape class. Co-Authored-By: Claude <noreply@anthropic.com> * refactor(params): own compressed-image admission in CompressionChainPlan The rule that the first ladder dimension must divide a compressed image's source ring dimension was assembled by hand at three call sites, each next to a separate width-cap check, and two other B admissions (commitment request validation and the planner's B candidates) checked only the width cap. CompressionChainPlan::for_image and try_for_image now derive an image's chain from its rows and ring dimension and enforce both halves of the rule. Level admission, commitment-request validation, the planner's B candidates, the relation layout, payload geometry, and setup-prefix compression all call them. The predicate is private to the compression module, the relation layout's local plan helper is gone, and one test pins the rule for every modulus profile. Co-Authored-By: Claude <noreply@anthropic.com> * refactor(planner): finalize recursive slices in the generating loop With slice pruning gone, the slice vectors only staged parameters for a second loop. Finalize each admitted slice where it is generated. Co-Authored-By: Claude <noreply@anthropic.com> * test(planner): pin both restricted-search folds by their full coordinates Matching only the level setup was ambiguous: two folds share each value and differ in their B source size, and find took whichever came first. Pin each fold by its full coordinate tuple and assert that the tuple is unique. Co-Authored-By: Claude <noreply@anthropic.com> * chore(estimator): derive the Euclidean table header from the policy target The infinity table header formats its target from the policy constraint; the Euclidean header hardcoded it. Format it from DEFAULT_EUCLIDEAN_TARGET_BITS. The generated text is unchanged. Co-Authored-By: Claude <noreply@anthropic.com> * docs: state current invariants and the current compression ladder The architecture chapter still listed the old compression ladder and called its map dimensions smaller than every commitment matrix, which the q32 D=128 first map is not. Several new code comments described the policy change rather than the code. Rewrite them as current invariants and rename the compression NTT selector test after what it checks. Co-Authored-By: Claude <noreply@anthropic.com> * refactor: derive every B/D image chain through CompressionChainPlan::for_image Committed-group decoding, the verifier's precommit check, the prover's handoff plans, setup envelopes, the SIS occurrence audit, the CPU commitment plan, and two examples still multiplied rows by the ring dimension and called for_complete_source, so they derived chains without the ladder's source-dimension rule. Route them through for_image. A caller-supplied precommit descriptor whose outer ring dimension the ladder cannot recompose is now rejected when the committed group decodes, instead of only failing the later catalog lookup. The committed-group fixture moves its q32 outer image to D=128, and a new test pins the decode-time rejection of a D=64 image. Only tests still call for_complete_source directly. Co-Authored-By: Claude <noreply@anthropic.com> * test(planner): check Jolt-scale planning for every chunk profile Plan Jolt's fp128 one-hot policies (K=16 and K=256 sources, every chunk profile, recursive setup planning) and its dense producers at trace lengths 2^30 and 2^31. The check takes minutes, so it is ignored by default; the evidence README records its command and results. Co-Authored-By: Claude <noreply@anthropic.com> * docs: separate the SIS target from Fiat-Shamir soundness in configuration The configuration chapter said the families target 169-bit quantum security, which read alone overstates the claim: only Module-SIS is priced at NIST category 3, and Fiat-Shamir soundness stays at 128 bits. Also reflow two lines the policy change left over-long. Co-Authored-By: Claude <noreply@anthropic.com> * refactor: name the group B and shared D compression chains once Deriving a group's B-image chain from its profile was spelled out at eight sites (verifier, committed-group decoding, prover handoff, CPU commitment plan, relation layout, setup envelopes, SIS occurrence audit, setup-prefix slots), and the shared D chain at three. The setup-prefix helper already computed the B chain for any profile under a narrower name. Add GroupCommitPhaseParams::outer_compression_plan (with a try_ form for admission) and CommittedGroupParams::opening_compression_plan, call them everywhere, and delete setup_prefix_compression_plan. Level admission now walks every group profile in one loop. Co-Authored-By: Claude <noreply@anthropic.com> * test: give compressed q32 fixtures a ring dimension the ladder can recompose Several geometry fixtures compressed q32 B or D images at D=32 or D=64. No q32 ladder can recompose those images, and now that every image chain is derived through CompressionChainPlan::for_image they are rejected. Move them to D=128, the first q32 ladder dimension. The committed-group fixture keeps A and B at one dimension, as a precommitted group requires, and its new rejection test covers validation and encoding. Co-Authored-By: Claude <noreply@anthropic.com> * docs(spec): link the NIST category 3 policy spec to its PR Co-Authored-By: Claude <noreply@anthropic.com> * test(pcs): make the proof-size byte-model capture race-free The byte-model harness captured the prover's width events with a scoped subscriber. While at most one dispatcher is registered, tracing-core computes a callsite's interest from the default of whichever thread reaches it first. A concurrent test that proves without a subscriber could cache both width callsites as never interested, and the capture then recorded nothing ("prover must report one terminal z payload and one nonce total"). The schedule-artifact-drift job hit this when two bounded-dense tests ran concurrently. Install the capture layer once as the global default and record into a thread-local capture. The layer is interested only in the two width events, so other callsites and tracing::enabled! diagnostics guards stay disabled as they would be with no subscriber. A new test forces the failing order: inside a capture, another thread proves first without one. Co-Authored-By: Claude <noreply@anthropic.com> * test: restore merge fixtures under the 169-bit catalog Two tests from main pick their fixture from the checked-in catalog, and the 169-bit catalog no longer contains it. - The setup-prefix challenge-hook binding test needs a recursive row whose setup prefix opens by evaluation trace. On main only the W8R2 recursive nv34x2 row had one; the merged catalog has none in any recursive family, because folds 0 and 1 and every multi-chunk fold now require packing. A bounded planner search finds W8R2 recursive nv38, which consumes prefixes at folds 1 and 2 and opens fold 2's by evaluation trace. Move the test to akita-planner, where it plans that row, and keep main's helpers and assertions unchanged. - The preplanned-row emitter test re-emits the first one-hot row under a single-group key. The first 169-bit row is grouped, so select the first row without precommitted groups. Co-Authored-By: Claude <noreply@anthropic.com> * test: fit main's new prefix and packing fixtures to the 169-bit ladder - cold_setup_prefix_rayon_acquisitions_complete built a q32 setup prefix at D=64. The q32 compression ladder starts at D=128, so the prefix B image cannot be compressed. Use D=128, as the audited setup-prefix fixture it reuses already does. - The level-two packing fixture repeated the grouped nv20 row's first recursive fold at both prefixed levels. Under the 169-bit tables that fold opens with 4-bit digits but takes 3-bit inner digits, so it cannot follow itself. Use the scalar row's own first recursive fold, which follows the same root and chains its digits at both levels. Folds 0 and 1 always use quotient lift with packing, so that fold is a packing-capable quotient successor.
… eq-factored replay and coefficient packing (#250) * perf(challenges): decide each operator-norm frequency once * perf(sumcheck): replay equality factors without unused split tables * perf(opening): keep coefficient-packing weight tables prover-owned * refactor(opening): bind coefficient-packing tables to their point Replace the free-standing SubringCoefficientPackingWeights with SubringCoefficientPackingTables, which owns the prepared point it was built from. Kernels and the Stage 2 plan carry the tables alone, so they can no longer be paired with a different point, and Stage 2 checks that the tables match the batch semantics' point. Gather Stage 2 tables inside the existing group loop instead of a second lookup, drop the crate-local opening alias, and shorten construction chains.
* feat(schedules): selected-row catalog views for verifiers A verifier checks proofs against the few schedule rows it selects, but loading a catalog audits every row and parses JSON. A verifier view keeps the parameters of only the requested rows, in a postcard encoding, plus the digests of every row. Loading it repeats the catalog's semantic audit for each carried row and recomputes the complete catalog digest, so the transcript binds the same identity as the full catalog. - ValidatedScheduleCatalog::to_verifier_view / from_verifier_view, and Config::from_verifier_view. - A view serves verification only: SetupRequirements now rejects it (validate_complete), since it cannot size a setup. CommittedGroupParams omits its unset multi-chunk fields (#175) only for human-readable formats: postcard carries no field names, so a view must always carry them for its decoder to read them back. JSON catalog rows keep their bytes. Co-authored-by: Michael Zhu <mchl.zhu.96@gmail.com> * test(config): move verifier catalog view tests to their own suite The binary verifier-view format gets its own test file, sharing the checked-in catalog fixture through tests/common. * fix(config): bind verifier catalog views to caller-selected chunking --------- Co-authored-by: Michael Zhu <mchl.zhu.96@gmail.com> Co-authored-by: Michael Zhu <8365992+moodlezoup@users.noreply.github.com>
* test(fuzz): add a resumable liveness-first fuzzing campaign Replace the three ad hoc cargo-fuzz targets with a campaign built on cargo-fuzz/libFuzzer, without changes to Akita's crates: - akita-fuzz (src/): engine-independent targets, generators, and oracles for fields, rings and NTTs, gadget decomposition, multilinear helpers, sumcheck, transcript, fold-challenge sampling, public deserialization, schedule artifacts, and end-to-end commit/prove/verify over every planned catalog row (completeness, binding, determinism, shared setups and backends, verifier and prover boundaries, and trusted terminal caches). - Liveness checks on every proof, read from the prover's response-model-diagnostics reports: fold grinds never run out, accepted responses stay within their caps, and the planner's response margins are reported to the engine as coverage. - akita-fuzz runner (runner/): prepares an instrumented distribution and runs unattended, resumable campaigns with per-worker memory limits, finding deduplication, replay, quarantine, corpus compaction, export, reproduce, and minimize. - akita-fuzz-dev (devtool/): uninstrumented smoke, replay, seeds, case listing, and a liveness sweep over every catalog row. CI fuzzes the primitive targets for a minute each; end-to-end targets need campaign resources. See fuzz/README.md and fuzz/COVERAGE.md. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * test(fuzz): generate schedule-artifact regression inputs from the shipped artifacts Each stored input was a full artifact with one field changed; deriving them in the seed generator keeps the repository free of half a megabyte of near-copies. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * ci(fuzz): allow nightly-only deprecation warnings in the fuzz job The fuzz harness links akita-cpu-backend, whose fetch_update calls are deprecated on nightly in favor of try_update, which the workspace's stable toolchain lacks; the job denies every other warning. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * test(fuzz): build only primitive targets in CI and keep error text out of failure messages The end-to-end harness instantiates every catalog family and is too large to build under ASan on a hosted runner; it now sits behind a default-on end-to-end feature that CI leaves off. Expectation failures report the error class rather than the full error text, which can carry protocol values. Also fix three clippy lints. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * test(fuzz): address AI review findings - CI fuzzes each primitive lane by its cargo-fuzz binary and variant environment (targets --kind primitive --cargo-fuzz), so ring_ntt's scalar lane runs instead of failing on a lane name. - reproduce and minimize run with harness stats disabled instead of writing through /dev/null. - The runner resolves filesystem arguments to absolute paths before workers change directory. - Compaction shares the fuzz jobs' coverage options (value profiling) and merges every variant lane of a shared corpus into one set before archiving. - Failure artifacts are recorded as findings for every job purpose before any cleanup, and kept when recording fails. - Job logs are pruned to the newest 16 per lane. - Planned case registries are keyed by cost limit, so fuzz_all plans each target's cases as its own binary would. - The rejection and parallel checks move out of family.rs into reject.rs and parallel.rs. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * test(fuzz): fuzz every cheap target in CI and harden the campaign runner - CI fuzzes the lanes `campaign/targets.toml` marks `ci`: every target that builds without `end-to-end`, which again includes the three original targets plus `public_deserialize` and `schedule_artifact`. It builds with the nightly pinned in `fuzz/rust-toolchain.toml` (as campaigns do), formats and type-checks the fuzz crates, including the end-to-end harness, and runs the runner's tests. - `prepare --out` replaces only an absent, empty, or previous distribution directory, checked before the build. - A baseline's watchdog budget scales with its seed count times the lane timeout instead of a fixed hour. - `export` skips corpus files a running campaign removes while archiving. - The runner no longer panics when started within five minutes of boot, and `status` tolerates a start time in the future. - Seeds and targets read each end-to-end and boundary target's case list from one place, and the boundary targets honor `AKITA_FUZZ_MAX_CASE_COEFFS` as documented. - Corpus compaction and failure recording move out of `runner.rs` into `runner/compaction.rs` and `runner/failures.rs`; the rejection check takes its case index instead of searching for it. Co-Authored-By: Claude <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
* fix(algebra): route NEON i16 transforms below eight coefficients to scalar
The NEON i16 twist, untwist, and range passes step eight coefficients
with no scalar tail, and the dispatch has no degree gate. Below D = 8
the negacyclic pair skipped its twist and D^{-1} psi^{-i} untwist, the
cyclic inverse skipped D^{-1} at D = 2, and the pointwise kernels were
no-ops at d = 2. Mirror the i32 kernels: a MIN_VECTOR_DEGREE gate that
re-enters the scalar transforms, and scalar tails in
pointwise_mul_acc_i16 and add_reduce_i16. Parity tests cover D = 2, 4,
8 and odd pointwise tails.
Co-Authored-By: Claude <noreply@anthropic.com>
* ci(portability): run the parallel-only NEON kernel tests on native ARM
add_reduce_i16 and add_reduce_i32, and their scalar-tail tests, compile
only with the parallel feature, which the native AArch64 job never
enabled. Add a parallel pass over ntt::neon.
Co-Authored-By: Claude <noreply@anthropic.com>
---------
Co-authored-by: Claude <noreply@anthropic.com>
Update ctutils 0.4.2 -> 0.4.5, which fixes non-constant-time mask generation and u128 comparisons reported in RUSTSEC-2026-0385.
Merge origin/main a4c7e09 into dev 827d1a5. The 2026-10-15 sync (#244) was squash-merged, so conflicts were resolved against the true base cf95fd0 rather than git's merge base 60b82bc. #232 raises Module-SIS to 169-bit category 3. On dev this regenerates the LaBinius commitment-prime width table (rank 2 no longer certifies, n_A 2 -> 3) and the dev-protocol schedule artifacts and catalog snapshot.
Bring in dev (#248, #249) and the 2026-10-25 main sync (#264). - Pass the runtime witness chunking #246 requires: shipped LaBinius catalogs are single-chunk (`shipped::WITNESS_CHUNKING`). - #246 removed the emitter's planning hooks; the generator now hands scalar and adapted grouped rows to the emitter as `preplanned`, keeping the grouped rows adapted from their scalar row as before. - #232 raises the root rank n_A from 2 to 3, so the image table doubles to 2^23 digits at (22, 8, 128). Regenerate schedules-labinius{,-dev} and update the pinned binary proof digests.
Three cold-cache test builds take about 46 minutes on a slow runner; the blake2b job hit the 45-minute limit twice after the dev sync.
* perf(labinius): commitment-row carry through limb transforms * perf(labinius): prime left opening from shared subset sums * perf(labinius): bit-sliced counters in the integer fold
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This PR adds the crate
akita-labinius-pcs, behind thelabiniusfeature, which is off by default. It turns the LaBinius root reduction (#228) into a polynomial commitment scheme for a binary source. The evaluation claims that the reduction leaves on committed tables are opened with one nested Akita grouped proof.One commitment can be opened to
The scheme is generic over two proof-field families:
Family64(Prime64Offset59withExt2challenges) andFamily128(Prime128Offset275). It ships its own schedule catalogs for four geometries.The PR also carries #230, squash-merged into this branch: three prover kernels of the root reduction in
akita-labinius-proverare replaced by faster ones that compute the same values. Proof bytes do not change.No Akita proof-path crate depends on the new crate, and no file of an Akita proof-path crate changes.
Normative design:
specs/labinius-pcs.md.Diff metadata
df08538d73665f615e8454d8131bc16d9a3e3a2d(dev)0ffc1ff8d(quang/labinius-pcs)mainthat reacheddevby squash or sync; their content is already ondev. The branch mergesdevseveral times, including themain→devsync chore(dev): sync main into dev (2026-10-25) #264 (169-bit ADPS16 SIS, compression policy V4, new schedules) and the Jolt repin chore(deps): pin dev's Jolt crates to Jolt main (f5c1947b1) #252. Everything below describesdf08538d7...0ffc1ff8donly..akscatalogs.Motivation
#228 landed the root reduction with an abstract commitment oracle (
RootProverOracle,RootVerifierOracle) and a transparent test oracle. Without a concrete oracle there is no commitment a caller can publish and no proof a verifier can check against it. This PR supplies that oracle with ordinary Akita, so that a binary source can be committed and opened end to end.Three prover kernels of the root opening (the integer fold, the commitment-row carry and the prime left opening) took a third or more of the opening time at the sample geometry. #230 replaces them.
Architecture
flowchart LR S[binary source] --> C[Prover::commit] C -->|clear root commitment| Y[image digits Y] Y -->|nested Akita commit, P::Digits| PC[public commitment] O[Prover::open] --> R[root reduction] R -->|prime claim only, before fold challenges| UP[prime left opening uP, P::Elements] R -->|after fold challenges| W[response digits W, P::Digits] R -->|returned evaluation claims| G[one grouped Akita proof over Y, uP, W] V[Verifier::verify] --> RV[reduction replay] --> GV[grouped batched_verify]Binary[Y, W]Prime[Y, uP, W]Both[Y, uP, W]No committed table is sent, and there is no second nested proof.
PrimeandBothselect the same three-group row; the reduction's mode binding tells their statements apart.Change-surface overview
dev)Prover::oracleandVerifier::oraclebacked by nested AkitaProver::{new, commit, open, root, oracle},Verifier::{new, verify, root, oracle},Committed,derive_root_setup,family,shippedAdmittedRootSetup::derivePrime128Offset275streamartifacts/schedules-labinius{,-dev}/, four catalogs each, with an offline generatorLaBinius PCS(both transcript backends) andLaBinius schedule artifact drift(both protocol directories)The crate
crates/akita-labinius-pcs(1,844 lines of library, 291 of generator, 1,100 of tests). The library deniesexpect,unwrap,panic,unreachableand unchecked indexing.family.FieldFamilyfixes the base field, the challenge field, and two Akita configurations:Digitsfor the base-16 digit tables Y and W, andElementsfor the full-width table uP.Digits64mirrorsproof_optimized::fp64::DenseandDigits128mirrorsproof_optimized::fp128::DenseBounded, withlog_commit_bound = 5(LOG_DIGIT_COMMIT_BOUND, the smallest signed width containing[0, 15]) andlog_open_boundset to the field width. The element configurations mirror the full-widthDensepresets. Both use the family's own SIS modulus profile,Q64Offset59orQ128Offset275.family::prime.flatten_prime_tablecommits uP as one base-field polynomial. OnFamily64the twoExt2coordinates become the lowest variable, andprime_opening_claimconverts the reduction's claim(point, value)into([omega/(1+omega), point...], value/(1+omega)). OnFamily128the claim is unchanged. Prover and verifier call the same conversion.family::tables,shipped.DigitTablesderives the three table lengths from the root shape.SUPPORTED_GEOMETRIESis the single list of geometries: profileD648Q25BoundedW46, fold-width log 8,lambda_fold = 128, cell-count logs 16, 18, 20 and 22.shipped_catalogloads the two catalogs of a family throughTrustedScheduleCatalog::from_artifact_bytes, the ordinary artifact admission, withWITNESS_CHUNKING(one chunk per table). It returnsShippedCatalogError::UnsupportedGeometrybefore any file access.DigitTables::setup_requirementssizes the nested setup for binary openings only (two groups) or for all three tables.setup.derive_root_setupcomputes the root matrix seed asBlake2b-256(LP("akita/labinius/root-matrix-seed/v1") || LP(nested_seed))and callsAdmittedRootSetup::derive::<Prime128Offset275>for both families. A 64-bit stream fails the derivation-bias check, and one stream field gives one clear image for both families. The label keeps the root matrix from being a reduced prefix of the nested Akita matrix.prover,verifier.Prover::commitcomputes the clear root commitment withcommit_binary_clear_preparedand commits its image digits Y underP::Digits; the public commitment is thatCommittedGroup.Prover::openrunsprove_root_reduction_byteswith the Akita-backed oracle.Verifier::verifyrunsverify_root_reduction_bytesand requires the whole proof to be consumed.binding,session. Transcript binding, fixed-size commitment exchange, and the nested session.bin/gen_labinius_schedule_artifacts. The offline generator, behindlabinius-catalog-gen, the only feature that pulls in the planner. Grouped rows are adapted from the scalar row of their final group, and each precommitted group is priced with its producer'scommitted_source_contract.Prover and verifier boundary
Both constructors take a
SupportedGeometry, aTrustedScheduleCatalog<P::Digits>, an optionalTrustedScheduleCatalog<P::Elements>and the nested Akita setup.Nonesupports binary openings;Someadds prime and combined openings. Before any proof is read, each constructor:Valid::check;setup_seed;TrustedScheduleCatalog::verifier_admitsandensure_prover_schedule_fits_setup, the verifier withAkitaVerifier::admitson the row digest.A failure is
AkitaError::InvalidSetup. A prover setup and a verifier setup of different provisioned capacity with the same seed interoperate, because the transcript binds the setup identity and not its capacity.Both sides trust their catalogs and setup. The verifier takes no row or size from the proof; the one length it reads, the nested proof length, is bounded by the trusted row.
Transcript binding and proof layout
The reduction absorbs its own domain label, root identity, field pair and grinding plan (with the opening mode) before the oracle runs. The oracle calls must then occur once each, in order.
binding::Orderputs the oracle into a failed state at the start of every call; only a successful call advances it. A repeated, out-of-order or wrong-mode call returnsInvalidProofand never touches the channel again.bind_imageLP("akita/labinius/pcs/v1"),LP(SetupSection),LP(digit schedule family name),LP(Y commitment)commit_prime_opening/bind_prime_openingcommit_response/bind_responsedischargeLP(transcript_instance_descriptor), then every point coordinate and value in group order; thenLP("akita/labinius/pcs-opening-session/v1")and onechallenge_blockas the nested session; then two messages: the u64 nested proof length and the nested proofSetupSectionis Akita's setup identity: decomposition, SIS modulus profile, compression policy, setup-seed digest and protocol features. It has no provisioned capacity.Proof layout:
BinaryisR + Kw + 8 + A;PrimeandBothareR + Kp + Kw + 8 + A, with R the reduction bytes and A the nested proof.Root prover kernels (#230)
All three compute the same values as before. The verifier, the catalogs and every public signature of the reduction are unchanged.
lowered/a_remainders.rs, new;lowered/a_carry.rs).matrix_remainders_limbcomputes the integer remainder ofsum_j A_ij * p_jmoduloY^648 - Y^324 + 1for all rows with the limb-prime transforms ofTrinomialLimbDomainand a signed CRT. Every remainder coefficient is bounded byB = 3*m*D*(q-1)*max|p|; it takes admitted limb primes, largest first, until their product exceeds2B. It returnsNone, anda_relation_carryfalls back tomatrix_row_remainder, for another degree or middle coefficient, an overflowing bound, too few primes, or when the reference limitD*q*max|p| <= i64::MAXfails, so the reference's errors are kept.lowered/prime.rs). Equality weights are grouped by up to eight. The 256 subset sums of a full group cost 255 additions in E and are shared by all columns and components. Eight source bytes are transposed as an 8×8 bit matrix, so one byte selects the subset sum for one output slot. Packing signs are applied once per slot.fold_kernel.rs). For each challenge sign, the shifted source words are counted in a streaming carry-save tree of 15 levels of 384-bit planes. The planes become integer coefficients and are reduced moduloY^162 + Y^81 + 1as before. A weight sum abovei16::MAXusesendpoint::fold_integer.specs/labinius-lowered-root.mdstates the carry computation and the new cost of the prime left opening.Measured in #230 on
a4eda6aa2againsteba92d343(before thedevmerges): six ignored(22, 8)sample tests with span tracing, best of three alternating runs, release withparallel, 16-core Apple M4 Max, load average about 12. Milliseconds, before → after:Family64BinaryFamily64PrimeFamily64BothFamily128BinaryFamily128PrimeFamily128BothThese kernel times are the kernels' own and are not repeated at this head. The Open column predates #264, which raised the root rank and doubled Y; current end-to-end numbers are in the next section.
Sizes and times at the sample geometry
2^22cells, which is a source of2^22128-bit words (64 MiB), at fold width2^8. The public commitment is 471 bytes.Family64BinaryFamily64PrimeFamily64BothFamily128BinaryFamily128PrimeFamily128BothThe rest of each proof is the 471-byte response commitment, the 471-byte commitment to the prime left opening when there is a prime claim, and 8 bytes of framing. Opening both claims costs 1,337 bytes (
Family64) or 1,078 bytes (Family128) more than the binary claim alone.Byte counts are exact for these inputs and identical across runs. Times are the best of three runs of the six ignored sample tests on
91724ae22, on a 16-core Apple M4 Max in release withparallelandtranscript-blake2b, main protocol, one test at a time. The one-minute load average was 12 to 14 when the runs started, mostly left over from the build. Of the opening time, the reduction takes 0.21 to 0.29 s, the nested proof 0.12 to 0.17 s and the response commitment 0.01 to 0.03 s. Of the verification time, the nested proof takes about 4 ms; the rest is the reduction replay.Security and verifier safety
commitment_sizederives Kp and Kw from the trusted profile withakita_error::checked.exchange_commitmentreads exactly that many bytes, requires exact decoding, the expected profile, and canonical re-encoding equal to the received bytes.expanded_schedule_proof_boundof the resolved row. Reservations are fallible.InvalidProof. The nested verifier's own error is passed through unchanged.bind_imagecallsCommittedGroup::checkon the public commitment and requires the image profile the selected row names.binding::Order, not by convention.What this does not establish
specs/labinius-pcs.md("Conditional guarantees and exclusions") and the open obligations ofspecs/labinius-root-reduction.mdstate this in full.Verifier::newmaterializes and the verifier scans the root setup.2^24cells at fold-width log 8 exceed the root matrix derivation caps and are not a supported geometry.Compatibility
labiniusfeatures it forwards toakita-labinius-verifierandakita-labinius-proveralready exist ondev. Withoutlabiniusthe crate compiles to nothing.akita-labinius-proverchanges only in the three perf(labinius): faster root opening kernels #230 kernels and one new test. The root reduction's pinned proof bytes (shipped_mode_and_field_pair_proof_bytes_are_pinned) are unchanged.Cargo.toml,Cargo.lock,AGENTS.md(preflight),scripts/check-crate-deps.sh,docs/crate-graph.md,book/src/how/architecture.mdand.github/workflows/ci.ymlchange only to register the crate and its CI jobs.check-crate-deps.sh akita-labinius-pcsalso checks that no runtime feature set reachesakita-planner.binary_proof_bytes_are_pinned_for_both_families), regenerated in the chore(dev): sync main into dev (2026-10-25) #264 merge.Commit map
The PR's own commits, oldest first. The
devmerges are listed because two of them change the PR's files.3ccb10365— the crate, catalogs, specification, registration and CI;4ec46aa3a,5d3c04135— spec cross-reference; remove the generator's unused probe mode;eba92d343— supported-geometry list, prover setup-capacity check, dev-protocol digests;41be5d04b,00f3602e1— bind the nested setup identity, not its provisioned capacity; test cleanup;a8d275661,843e6b4f1— merges ofdev, no change to PR files;5847a4084— merge ofdevwith themainsync chore(dev): sync main into dev (2026-10-25) #264: shipped catalogs are single-chunk (WITNESS_CHUNKING, for refactor: make witness chunking a runtime catalog policy #246); the generator hands its rows to the emitter aspreplanned; feat(sis)!: raise Module-SIS to NIST security category 3 (169-bit ADPS16) #232 raises the root rankn_Afrom 2 to 3, so Y doubles to2^23digits at(22, 8, 128); both catalog directories regenerated and the pinned digests updated;177541b56,258fdb6c8— merge ofdev;LaBinius PCSjob timeout raised to 60 minutes;bde940cb5— merge ofdevwith chore(deps): pin dev's Jolt crates to Jolt main (f5c1947b1) #252; the crate'sjolt-fieldpin moves tof5c1947b1;91724ae22— perf(labinius): faster root opening kernels #230, the faster root opening kernels;0ffc1ff8d— spec only: Y's prover memory at(22,8,128)is 128 MiB (Family128) or 64 MiB (Family64) after the rank increase.Tests
12 tests (11 on
transcript-keccak, where the pinned-digest test is compiled out), plus 6 ignored sample runs.binary_opening.rs,prime_opening.rs): the value, the point, the weights, a commitment to another message, each proof section, mode confusion, truncation and a trailing byte. Every row must returnAkitaError::InvalidProof. Proof-of-work nonces are covered by the reduction's own tests.prime_conversion.rs: the flattened polynomial against a direct extension-valued evaluation.to_verifier_setup: the verifier accepts, and the proof bytes equal those under the exact setup.UnsupportedGeometry.InvalidSetupfor a nested setup whose descriptor has one polynomial too few or one variable too few while its matrix is large enough.setup.rsunit test: the root matrix seed is the labelled digest, and the matrix differs from one derived from the nested seed directly.akita-labinius-prover/tests/a_carry.rs(perf(labinius): faster root opening kernels #230):matrix_remainders_limbagainstmatrix_row_remainderon every row, for fold widths 1 and 512 (two and three CRT primes), with random and extremal responses. The fold is covered by the nine existing tests oftests/fold_kernel.rs. The reduction's own tests use only short groups of equality weights; full groups of eight are exercised by the PCS prime and combined tests and by the samples, where the verifier checks the committed uP against the sumcheck claims.Validation at
91724ae220ffc1ff8dchanges onlyspecs/labinius-pcs.md; CI reruns on it.CI on
91724ae220e358ec79ed39be48ea74ccecf1d6bb, as of 2026-10-26 15:16 UTC: 59 checks succeeded, 6 were skipped, 1 is in progress, none failed.LaBinius PCSontranscript-blake2bandtranscript-keccak(serial, parallel, and parallel underakita-params/dev-protocol, plus the four Clippy configurations),LaBinius schedule artifact driftand-dev(the eight.aksfiles regenerate byte for byte),LaBinius root reductionon both backends (including the reduction's pinned proof bytes),Test (1/2),Test (2/2),Test dev protocol (1/2),Test dev protocol (2/2),Clippy,Dev protocol schedule artifact drift,Doc guardrails,Jolt pins on main,Unused dependenciesand the sevenBenchjobs.Deploy Akita Book,cleanup,collect,publish,reserve,review.Schedule artifact drift.The six ignored
(22, 8)sample tests also pass at this head (the runs above).Reviewer map
specs/labinius-pcs.md, then the new section "Matrix seed and stream field" ofspecs/labinius-setup-contract.md.crates/akita-labinius-pcs/src/family.rs,family/prime.rs: the configurations and the claim conversion.src/binding.rs,src/session.rs: transcript order, framing and allocation bounds.src/verifier.rs, thensrc/prover.rs.src/setup.rs,src/family/tables.rs,src/shipped.rs: root seed, sizing and catalog loading.src/bin/gen_labinius_schedule_artifacts.rsand the two CI jobs. The.aksfiles are generated; CI regenerates them byte for byte.tests/.crates/akita-labinius-prover/src/{fold_kernel.rs, lowered/a_remainders.rs, lowered/prime.rs}andtests/a_carry.rs.🤖 Generated with Claude Code