Repository navigation
Conversation
…d encoding; admitted setup drives the lowered fixture
…ntract as its sources
…t real setup shape, and state what the lowered challenges need fixed
Documentation blast radius (advisory)These regions may need doc/spec/book updates based on changed paths. Changed files in this PR: 24
|
PCS Profile Benchmark
13 of 13 profiles passed. Times are medians of Each sample verifies the same proof first with the configured multi-threaded pool and then with one thread. Both timings reuse the same verifier setup. Merge-base comparisons are available for Benchmark shards
Public opening statements
One-hot profiles generate deterministic witnesses with one Direct evaluates the public setup contribution during Stage 2. Recursive carries the same check through a Stage 3 setup-product sumcheck. Both modes execute the complete fold schedule and terminal verification. The chunked profiles Generated profiles may select different A, B, and D ring dimensions at different fold levels. The short profile names omit those dimensions. Each sample generates deterministic witnesses and opening points, prepares setup, commits, proves, serializes the proof, checks its size, prepares verifier setup, and verifies the claimed openings. It does not test malformed proofs. Phase time
Proof size and protocol shape
Grinding retries are rejected attempts at each fold, listed in measured-run order. Zero means the first sampled nonce was accepted. Each multi-group profile has two precommitted nv16 singleton polynomials and two polynomials in the displayed final group. Native proof accounting
Memory and setup size
Deltas are shown only for profiles with a matching merge-base case. Negative is smaller or faster. The uploaded |
CI test timing
Run summary
Wall time spans 2 parallel nextest slice shards. Slowest tests
Regressions vs mainNo per-test regressions above the threshold. New slow testsNo new tests ≥30s vs main baseline. |
|
/ai-review |
|
AI review attempt 1/3 reserved. Failed or incomplete attempts also count toward this PR's limit. |
There was a problem hiding this comment.
Usefulness: benefit supported. The repository evidence supports both additions: AdmittedRootSetup combines existing shape admission with canonical seed expansion, while the lowered modules bridge the clear endpoints to an explicit field relation using existing encoding and setup-layout contracts. Differential, quotient, boundary and tamper tests provide useful regression coverage. The additions are feature-gated and leave existing proof-path behavior unchanged. Materialization and schoolbook-product costs are substantial but disclosed and proportionate to this reference-building-block scope; transcript integration and composition proofs remain explicitly separate work.
Recommended for approval: no unresolved findings in this automated review.
Summary
This PR adds the two pieces a succinct LaBinius root needs before any sumcheck or commitment exists: a root setup whose matrix nobody chooses, and the root's acceptance condition restated as a digit alphabet, two clear integer range checks and one linear relation over the coefficient field. Both live in the existing opt-in crates
akita-labinius-verifierandakita-labinius-prover, behind the off-by-defaultlabiniusfeature. Tracking issue: #45.It provides:
AdmittedRootSetup::<F, D, M>::derive(profile, log_num_cells, log_fold_width, lambda_fold, seed): derivesLabiniusRootShapefrom the profile, takes the certified rank from the width table, expands the trinomial matrix from anAkitaSetupSeedthrough the shared public prefix, and returns aBinaryClearSetupthat cannot be built from a caller-supplied matrix.identity_bytes::<H>()gives a canonical, length-framed identity over every derivation input.LoweredRootLayout,LoweredPublic, the witness and image weights (dense and structured multilinear evaluation),check_lowered_clear, and the two decoded residualsa_row_residualandparity_row_residual, in the verifier crate.encode_witness(response digit table in the canonicalTrinomialResponseLayoutorder),flatten_image,a_relation_quotients,parity_quotient_and_carry.The modules take explicit field challenges
(alpha, xi, gamma). They define no transcript, no sumcheck, no commitment to the digit table, no polynomial opening and no wire encoding. Nothing on the Akita proof path calls them.Normative text:
specs/labinius-setup-contract.mdandspecs/labinius-lowered-root.md.Diff metadata
f1957d8bceb84edfefd156732f5cee121488267b(quang/labinius-stack)f082ef4e968eeafbb9010559cab27677b37e22b1Why the base is not
devThis work needs both #198 (the clear opening it lowers) and #199 (the root profile, shape and digit encoding it reads), and neither is merged.
quang/labinius-stackis the merge of their current heads and nothing else:The diff shown here is therefore exactly this PR's surface. Once #198 and #199 land on
dev, this PR should be retargeted todev; the stack branch carries no change of its own and can then be deleted.Motivation
#198 verifies a binary opening by sending the whole integer response and recomputing two ring equations. #199 fixes the ranges and table lengths a succinct root will commit. What was missing between them is the statement a sumcheck can reduce: which table entries are constrained, by which public weights, to which public constant, and which matrix the weights are computed from.
Two concrete gaps close here:
BinaryClearSetup::newaccepts any matrix and does no SIS lookup. A root that claims binding needs a matrix derived from a public seed at the certified rank.AdmittedRootSetupis that construction, and it is the only way to obtain one.<W, K_W> + <Y, K_Y> = c_pub.Change-surface overview
BinaryClearSetup::new)admitted.rs: seed-derived matrix at the certified rank, canonical identitylowered/{layout,public,weights,check}.rslowered/{witness,quotient,parity}.rsakita-labinius-verifierdepsakita-typesedgeakita-types, enabled only bylabiniusakita-labinius-proverdepsakita-typesedgeakita-typeswith default features offdocs/crate-graph.mdakita-pcsAdmitted setup
derive_trinomial_matrixexpands exactlyrows * columns * Dfield elements withderive_public_matrix_prefix::<F>and the caller's seed unchanged. CoefficienttofA[i, j]is the public element at(i * columns + j) * D + t, which isTrinomialASetupView::setup_address(i, j, t)with setup offset zero. The matrix is one view of the shared public prefix: a deployment may store the prefix once for this view and for ordinary Akita matrix views over the same field and seed. Each view is uniform under the expander's random-oracle assumption; no independence between views is claimed.For an admitted root the matrix is
n_Abym. The fold widthCcounts source columns and does not set the matrix's column count.Identity bytes, in order: the domain string
akita/labinius/admitted-root-setup/v1, the root profile's identity (which binds the certified width-table digest),log_num_cells,log_fold_width,lambda_fold, the admitted rank, the seed derivation tag, the 32 seed bytes, and the nestedBinaryClearSetupidentity, which binds the matrix-view digest. No second matrix digest is introduced.The materialising API rejects, before expanding the seed: zero dimensions, zero or odd degree, more than 64 MiB for either the flat prefix or the matrix backing, and more than 64 KiB per ring element. These are host-resource limits, not limits of the numerical admission. The first profile at
(log_num_cells, log_fold_width, lambda_fold) = (22, 8, 128)has rank 1,m = 4096,C = 256and 2,654,208 matrix coefficients (40.5 MiB at 16 bytes each), and a test derives it in full. A shape can pass numerical admission and still exceed the budget: a test derives the shape at(32, 0, 128)and checks thatAdmittedRootSetup::derivereturnsInvalidSetupfor it without panicking.Lowered relation
Write
d = 162,Phi(Z) = Z^162 + Z^81 + 1,D = d*k,Phi_Dfor the commitment trinomial,P_c = D.next_power_of_two(),bfor the digit width anddcfor the digit count.Tables. The response digit table uses the canonical layout
where
pis the signed packing of the scalar response andoff(t)isoffat positive packing signs andoff - 1at negative signs, so both signs accept exactly the same scalar interval. The image table isY[t + P_c*e] = images[e].coefficients()[t], padded to a power of two. Layout sizes are read fromLabiniusRootEncoding, not recomputed.Rows. Over the coefficient field,
and over the integers,
QA_ihasD - 1coefficients;Qhas 161 andKhas 162, each checked in the clear against its enforced interval.Batched relation. At explicit
alpha, xi, gamma, withg = gamma^n_A, acceptance istogether with the alphabet check on every table position and the two clear range checks.
K_W,K_Yandc_pubare defined once in the spec. Weights are zero at coefficient tailst >= Dand at image padding; every position is still alphabet-checked. There is no selector and no zero-tail acceptance check.Structured evaluation.
witness_weight_mleandimage_weight_mleevaluate the multilinear extensions ofK_WandK_Yat a point without building the dense vectors, usingTrinomialASetupView::preparefor the matrix part and a product of block factors for the parity part. Tests compare them with the dense weights at random and at Boolean points.Extension contract (
docs/branches.md)dev, under#![cfg(feature = "labinius")].main:Cargo.lock(twoakita-typesdependency edges for the LaBinius crates) anddocs/crate-graph.md(one reworded row, one edge). Neither is compiled.labiniusoff, the verifier crate has noakita-typesedge at all (cargo tree -p akita-labinius-verifier --no-default-features --features transcript-blake2b --edges normal --depth 1lists none); with it on, nothing is selected, since no proof-path code calls these functions.main: there is no affected configuration. No file on the setup, commitment, prover or verifier path changes, so no proof-byte comparison was run.Security and verifier safety
What the code establishes, and what it leaves to the protocol that will use it:
alphawith probability at most(2D - 2)/|F|(1294/|F| at D = 648); a parity row false modulo P survives uniformxiwith probability at most322/|F|; batching bygammaadds at mostn_A/|F|. If the parity row holds modulo P, the alphabet, the clear range checks and the admitted inequalityH + 3*2^(e_Q-1) + 2*2^(e_K-1) < Pforce it to hold over the integers, hence modulo 2 andPhi.alphaandxi, together withW,QA,QandK; all evaluated rows must be fixed beforegamma. These helpers take challenges as arguments and cannot enforce this. Degenerate explicit challenges can hide false rows.eta_A = 4*Gamma_inf*Delta < P, SIS at the admitted rank) and lists what remains open.bind_statementbinds the nested clear identity only. A caller that needs the profile, shape inputs and seed bound must absorbAdmittedRootSetup::identity_bytesitself. The root reduction that follows in the stack is specified to absorb it first; that code is not in this PR.AkitaError::InvalidSetup; the setup tests run each case undercatch_unwindand requireOk(Err(InvalidSetup)), so a panic fails the test. Extent products are checked before the seed is expanded.Commit map
9da768dd1: seed-derived admitted root setup and identity.22b6a3881: lowered root relation over the canonical response layout.86e06910c: the layout reads table sizes from the admitted encoding; the admitted setup drives the lowered fixture.df21b0b92: the lowered-root spec names the encoding and the setup contract as its sources.161943079: review fixes. The verifier'sakita-typesedge is gated on the feature, a test derives the first real setup shape, and the spec states what must be fixed before the challenges.f082ef4e9: the two crate-level doc comments nameadmitted,lowered,BinaryClearSetup::newandAdmittedRootSetup::deriveas code spans instead of intra-doc links. Each crate is#![cfg(feature = "labinius")], so with the feature off those items do not exist and the CIDocumentationjob (-D warnings, extension off) failed on the first push of this PR withunresolved link to lowered.33a604086,692fc3921,23afd6304: merges that bring the stack's inputs together.Validation
All at head
f082ef4e968eeafbb9010559cab27677b37e22b1, clean worktree, withPKGS = -p akita-labinius-verifier -p akita-labinius-prover:cargo test $PKGS --no-default-features --features labinius,transcript-blake2b: 45 passed (13 suites).cargo test $PKGS --no-default-features --features labinius,transcript-keccak: 45 passed (13 suites).cargo clippy $PKGS --all-targets --no-default-features --features labinius,transcript-blake2b -- -D warnings: no issues.cargo clippy $PKGS --all-targets --no-default-features --features transcript-blake2b -- -D warnings(extension off): no issues.cargo fmt --all --check,taplo fmt --check: clean.scripts/check-crate-deps.shforakita-labinius-verifier,akita-labinius-prover,akita-verifier,akita-prover,akita-params: passed.scripts/check-rust-file-lines.sh --no-baseline,typos,./scripts/check-doc-guardrails.sh,cargo machete --with-metadata: clean.crates/outside the two LaBinius crates differs from the base.cargo tree -p akita-labinius-prover -e features --no-default-features --features transcript-blake2bshows nolabinius-*feature enabled with the extension off.git diff --check: clean.RUSTDOCFLAGS='-D warnings' cargo doc -q --release --no-deps $PKGS --no-default-features --features transcript-blake2b(extension off) andRUSTDOCFLAGS='-D warnings' cargo doc -q --no-deps $PKGS --no-default-features --features labinius,transcript-blake2b: both clean. The CI command documents the whole workspace; locally that stops inakita-algebraon an x86-only link on this ARM host before reaching these crates, so the two crates were documented on their own.Tests added (25): 13 for the admitted setup in
tests/admitted.rs, 7 intests/lowered.rs, 1 intests/lowered_oracle.rs, 4 intests/lowered_tamper.rs. The oracle test recomputes every quotient and carry coefficient with an independent big-integer division and a schoolbook field product. The tamper tests include a mutation that keeps the A row satisfied and breaks parity.Not run: the full workspace test pass, the three workspace Clippy configurations, schedule regeneration, portability, Jolt compatibility and fuzzing. The lowered relation is exercised at the small admitted geometry
(4, 1, 128)for all three digit bases; the(22, 8, 128)shape is derived and checked for its dimensions only, not run through the relation.Review
Two independent reviews at
df21b0b92(setup contract; lowered relation) both approved with minor findings. Three of the four are fixed in161943079. The fourth is test coverage and is listed below.Remaining work
For this surface:
t = 4) for each base; malformed fold-challenge and wrong-left-expansion cases forLoweredPublic::new; a padding mutation pinning that arbitrary image tails are accepted.a_relation_quotientsis a schoolbook product (about 1.83e9 coefficient products), andwitness_weight_mlescans all 2,654,208 matrix coefficients and materialises 4,194,304 field weights (about 64 MiB). Both are correct and slow; neither is on any proof path yet.Under #45, next in the stack:
Wand one onY.dev-protocolschedule artifacts.Reviewer map
specs/labinius-setup-contract.md, thencrates/akita-labinius-verifier/src/admitted.rsspecs/labinius-lowered-root.mdcrates/akita-labinius-verifier/src/lowered/layout.rs,public.rs,weights.rs,check.rscrates/akita-labinius-prover/src/lowered/witness.rs,quotient.rs,parity.rscrates/akita-labinius-prover/tests/lowered_oracle.rsandlowered_tamper.rs, thenadmitted.rsandlowered.rs