Repository navigation
Conversation
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 PR supplies a useful executable reference joining the existing field-switch, trinomial arithmetic, challenge-profile, and source-comparison components. The arithmetic oracles and isolated endpoint rejection tests provide concrete value for later succinct implementations. Two additional crates and a small documented equality-expansion duplication add maintenance cost, but the feature-gated API, shared protocol helpers, and unchanged existing proof path keep that cost proportionate. Production admission and projection/composition obligations are explicitly outside this slice rather than implicitly claimed as solved.
Recommended for approval: no unresolved findings in this automated review.
|
Superseded by #228, which keeps a transparent, non-succinct opening only as a differential oracle for the reduction. The earlier stack was re-cut into four pull requests: #226 (arithmetic), #227 (parameters), #228 (root reduction) and #229 (polynomial commitment). Closing without merging; the branch is left in place. |
Summary
This PR adds two opt-in crates,
akita-labinius-verifierandakita-labinius-prover, that implement the clear binary opening from the LaBinius tracking issue (#45) as a differential oracle.It now:
u128for the F128 host,u64for the F192 host) asY_col = A * W_coloverTrinomialRing<F, D, M>withD = 162*k,kin {1, 2, 4}, and an odd coefficient prime (Prime64Offset23703orPrime128OffsetA7F7);sum_j eq_H(r,j) * embed_source(w_j) = tto one F162 source evaluation through the merged field switch (SwitchPartials,ncharacteristic-two product-sumcheck rounds);U,Cbinary fold challenges from the admittedBinaryChallengeProfile, and a signed integer response checked directly against the prime equation, the parity equation in F162, and the accepted interval.It is the reference that the succinct root reduction will be tested against. It is not a production PCS and admits no production parameter set; see "What this does not provide".
Normative design:
specs/labinius-clear-opening.md.Diff metadata
3d69096eadb129c097e4fc2e4f2d289e82e0ea1a(dev)2396930e7b7673af44a13a93190cc3df865336adMotivation
The merged LaBinius foundations (binary fields and field switch, trinomial ring and NTT, binary challenge profiles, source-comparison bounds, the infinity-norm width table) have no consumer that exercises them together. Before a succinct binary root is wired into the fold, the direct protocol needs one executable definition: exact transcript order, byte encodings, endpoint equations, and rejection behaviour. Every later slice (lowered root relation, combined range/relation sumcheck, fused mixed root) can then be checked against it instead of against prose.
Protocol in this PR
flowchart LR S["source words w (N = k*m*C)"] --> C["commit: Y_col = A * pack(W_col)"] S --> F["frontend.rs: host claim -> partials -> n sumcheck rounds"] F --> E["BinaryEvaluationClaim { point z, value t' }"] E --> U["U_col, left expansion check"] U --> Ch["C binary fold challenges"] Ch --> V["integer response v = sum_col c_col * W_col"] V --> P["prime: A*pack(v) = sum c_col * Y_col"] V --> B["binary: sum eq(z_row,row)*(v mod 2) = sum U_col*(c_col mod 2)"] V --> R["range: lower <= v <= upper"]frontend.rs(steps 1 to 4 of the spec) returnsBinaryEvaluationClaimand is the boundary the later mixed-root integration consumes unchanged.endpoint.rsholds the three direct checks. All three read the same decoded integer response.profile.rsholdsBinaryClearSetup::new, which rejects instead of clamping.channel.rsis the only module that touchesakita-transcript.Change-surface overview
akita-labinius-verifier,akita-labinius-prover, both gated by an off-by-defaultlabiniusfeatureCargo.toml, two package stanzas inCargo.locktest-labinius-clear-opening(both transcript backends: tests, Clippy with the feature, Clippy without it); twocheck-crate-deps.shlinesscripts/check-crate-deps.shAGENTS.mdpreflight linesExtension contract (
docs/branches.md)mainchange only to register them (the table above).labiniusfeature is off by default. With it off, the crates enable none oflabinius-binary,labinius-trinomial,labinius-challenges,labinius-sison their dependencies (checked on the Cargo feature tree of each crate, for both transcript backends).main: there is no affected configuration.git diff origin/dev...HEAD -- crates/touches only the two new crates, and theCargo.lockdiff adds only their two package stanzas. No proof-byte experiment was run for this PR.Security and verifier safety
Uis bound before the fold challenges are drawn.i128accumulators and reduces byZ^162 = -Z^81 - 1before any prime embedding or parity read. Parity usesrem_euclid(2).BinaryChallenge::canonical_support_encoding(profile); there is one definition of that encoding.AkitaError::InvalidProof; setup and statement failures returnInvalidSetup,InvalidInput, or dimension errors. Extents useakita_error::checkedarithmetic.What this does not provide
A; there is no seed expander, so nothing here stops a caller from committing under a degenerate matrix.BinaryClearSetup::newenforces geometry, the fold-challenge entropy budget (profile.meets_budget(C, lambda_fold)), and the no-wrap source-comparison bound (eta = 4 * Gamma_inf * Delta < P). It does not consult the width table. Runtime rank admission is the next PR.commitment::apply_matrixmultiplies element by element throughTrinomialNttDomain::multiply_with_workspace; it is a reference, not the commit kernel.specs/labinius-field-switch.mdremain open.Known duplication and interactions
akita-labinius-verifier/src/source.rsrepeats the recurrence of the privaterow_weightshelper inakita-algebra/src/binary/field_switch.rs, because that helper admits only the host batching dimensions. The doc comment records this and the replacement condition.akita-transcript. Onlychannel.rshere uses it; whichever of the two lands second needs to port that one module.Commit map
5d2ce2c24— the two crates, spec, registration.c04c01b51— regressions that isolate the binary endpoint comparison and the prime check, the adjacent no-wrap admission pair, canonical challenge parity, the bounded-weight D648/P128 roundtrip, the D324 matrix-action oracle; removes the prover's unused direct transcript dependency.8d23fa20c,2396930e7— documentation only (crate-graph edge, architecture sentence, one spec sentence).Validation
At
c04c01b51(the last commit that changes code):cargo test -p akita-labinius-verifier -p akita-labinius-prover --no-default-features --features labinius,transcript-blake2b --locked: 20 passed. Same withtranscript-keccak: 20 passed.cargo clippy -p akita-labinius-verifier -p akita-labinius-prover --all-targets --no-default-features --features <f> --locked -- -D warningsforlabinius,transcript-blake2b,transcript-blake2b,labinius,transcript-keccak,transcript-keccak: clean.--all --all-targets --release --no-default-features --features parallel,disk-persistence,transcript-blake2band--features transcript-blake2b): clean.cargo fmt --all --check,taplo fmt --check, both Rust line-cap scripts, the 179 Python script tests, all elevencheck-crate-deps.shinvocations,check-shared-field-identity.sh,check-external-schedule-artifacts.sh,cargo machete --with-metadata,typos: clean.binary_lhs != binary_rhscomparison inverify_endpointsremoved,binary_endpoint_rejects_an_unselected_column_at_scalar_degree,..._at_packed_degreeandpacked_response_component_cancellation_preserves_prime_but_fails_binaryfail (the verifier accepts); with it restored all 20 tests pass. This was the gap in the first review round: no test rejected on the binary comparison alone.At
2396930e7:./scripts/check-doc-guardrails.sh,typoson the changed documents,cargo fmt --all --check.Not run locally: workspace Clippy configuration 3 (
-p akita-pcswithresponse-model-diagnostics), the full workspace test pass, portability, Jolt compatibility, fuzzing.Remaining work under #45
main, then the fused mixed root, planner and catalog rows.Reviewer map
specs/labinius-clear-opening.mdcrates/akita-labinius-verifier/src/profile.rs(admission)crates/akita-labinius-verifier/src/frontend.rs, thenendpoint.rscrates/akita-labinius-prover/src/lib.rscrates/akita-labinius-prover/tests/tamper.rs,admission.rs,oracles.rs