feat(security): certify selective L2 fold sizing - #369
Open
quangvdao wants to merge 20 commits into
Open
Conversation
Delete the stale global L2 cutover design and replace it with a candidate-local late-fold route. Document physical-coordinate A-role sizing, the redundant Hachi factor, and complete-vector Euclidean table semantics.
PR SummaryHigh Risk Overview Physical A-role sizing no longer applies the removed The planner keeps ordinary L∞ search and, at an exact cap state, adds one L2 candidate only if it lowers A rank; suffix DP still picks the cheaper full proof. fp128 D64 one-hot (and fp32/fp64 caps) wire preset caps into Proving/verification: Stage 1 can fuse a complete physical response norm into the final range leaf ( Book and security docs describe selective caps, dual tables, and sumcheck stages; planner policy validation moves toward Reviewed by Cursor Bugbot for commit e2adafb. Bugbot is set up for automated code reviews on this repo. Configure here. |
Remove the redundant Hachi embedding factor from physical A-role sizing and bind terminal admission to its selected SIS bucket. Add the complete-vector L2 collision formula, quantum ADPS16 Euclidean estimator path, separate generated L2 table and digest, golden replay metadata, and regenerated schedules.
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
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: 142
|
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. |
Benchmark Report
Negative deltas are improvements for time, memory, and proof size. Terminal response component breakdown
The Detailed schedule and proof-size breakdowns by fold level are available in the uploaded |
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
Reviewed by Cursor Bugbot for commit c064889. Configure here.
Preserve main’s tensor-challenge removal and unified signed-sparse sizing while porting selective L2 security routes, physical Hachi sizing, and complete suffix comparison onto the new APIs. Regenerate the combined schedule catalog.
quangvdao
marked this pull request as ready for review
August 7, 2026 12:43
Fuse the optional norm relation into the existing compact Stage 1 range path and reuse paired-equality relation terms in Stage 2. Remove dense replay tables and test-only wrappers. Restore the ordinary single-candidate Linf planner search, admit only one exact L2 alternative at a measured state, and drop the artificial contiguous cap window. Keep generated SIS evidence reproducible without checking in the 2.4 MB audit CSV.
quangvdao
changed the title
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
2 participants
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 a sound, selective L2 security route for measured later folds. L infinity remains the ordinary route at every fold. A fold uses L2 only when its schedule contains an exact public cap, the proof certifies the complete physical response norm, and the resulting full suffix is smaller.
The final implementation is deliberately narrow:
It also removes a separate Hachi embedding factor from current physical A-role sizing. Both the challenge and response are already physical ring coefficient vectors at this boundary, so applying that conversion again double counts it.
Normative design:
specs/selective-l2-fold-security-sizing.md.Diff metadata
4068d713849215d2035bd0599b72a7c06cf5bec4(main)e2adafbab6d3d3c10fce3feda04f99023bab31aaThe preceding version had 34,100 insertions. The final cleanup removes the separate dense proof paths, the planner split frontier added only for L2, and a checked-in 25,201-line audit CSV.
Motivation
The coefficient L infinity bound is sound but can overprice a later folded response. An exact Euclidean cap can lower the A rank when the folded witness has small complete L2 norm. For the fp128 D64 one-hot nv32 profile, the selected L5 cap lowers A rank from 5 to 4 and reduces the complete proof.
The route must remain selective. Without a norm proof, the planner has only the existing L infinity certificate and must size A from that bound. This PR does not infer an L2 norm from the digit envelope and does not apply an L2 model throughout recursion.
Before and after
DigitRangeProver::proveremains the sole entry point; the optional norm relation reuses the compact range prefix and expands coefficients directlyEqPairTensorFamilyandAdditionalRelationTermsmachinerySecurity contract
For the existing L infinity route, the physical collision bound is
For a selected L2 route with certified complete physical squared norm
S, it isThe production Euclidean estimator uses the 128-bit quantum ADPS16 model with
There is no second width multiplier and no Hachi embedding factor in either formula. The inputs have already been mapped to physical ring coefficients. An L2-selected fold still carries the existing digit range certificate; L2 is an alternative A-role security theorem, not a replacement for range membership.
The schedule fixes the cap. The prover may grind the existing fold nonce, but the verifier checks the sum-check claim and rejects a claimed norm above the scheduled cap. Small fields use bounded limb Gram subclaims so integer reconstruction cannot wrap the base field.
This PR does not use a Gaussian tail model, a claimed operator norm such as 17, or the older BDGL16 Euclidean path.
Canonical protocol path
Stage 1
The optional physical norm term is fused into the existing digit range leaf. It shares the product prefix and final range state, then adds the norm polynomial in coefficient form. This removes dense equality tables and
UniPoly::from_evalsinterpolation from the prover.The two relations have different factors, so an L2-selected round still transmits the one additional coefficient required by the protocol. No such coefficient exists on an L infinity fold.
Stage 2
PhysicalResponsePlanis the checked owner of the physical-to-digit geometry. It exposes paired-equality tensor families. The prover feeds them through the existing additional-relation terms, and the verifier contracts the same families directly. It does not materialize and scan a 65,536-entry sparse replay table.Planner
The ordinary L infinity candidate search is unchanged. At an exact
(fold level, input witness length)cap match, the cap's physical response length determines one block split. The planner constructs that one L2 alternative, keeps it only if it lowers A rank for the split, and lets the existing suffix dynamic program compare the two complete suffixes.There is no future-cap state expansion and no L2-specific frontier oracle.
Proof size and runtime
Paired local profiles ran the final head and exact base binary interleaved, with one warmup followed by three measured samples.
fp32 and fp64 select L infinity at every fold. Their proof reduction comes from removing the redundant physical Hachi factor, and their timings show that an available L2 policy adds no meaningful work to an unselected path.
fp128 selects L2 only at L5:
The L5 public squared norm cap is
4,294,967,296; the measured proof used nonce 0 and had no rejected draw.Against the earlier PR binary, the final fp128 implementation has the same proof size and is 13.92% faster to prove and 14.91% faster to verify. The removed cost was implementation overhead, not a required cost of the L2 certificate.
Generated estimator evidence
The checked-in Rust lookup rows and table digest remain the runtime source of truth. The generator emits all 25,200 accepted-boundary and rejected-successor audit rows, hashes that CSV into the table digest, and leaves the reproducible CSV as an ignored local artifact:
Breaking changes
This is an intentional protocol cutover. It changes transcript binding, proof serialization, schedule identity, generated tables, and selected A matrices. The repository provides no backward-compatibility guarantee, so no dual wire format or compatibility wrapper is retained.
Validation at
e2adafbabThe following passed locally on the exact head:
cargo machete --with-metadata;Repository-wide Taplo and typos still report only pre-existing findings in
third_party/lattice-estimator; every changed file passes the scoped checks.The new remote CI and benchmark runs are in progress on this exact head. No remote failure was present when this description was published.
Specification status and follow-ups
This PR completes the sound selective certificate, estimator, planner, and verifier cutover. Two possible tighter models remain separate work because each needs its own security and completeness argument:
Reviewer map
Suggested order:
specs/selective-l2-fold-security-sizing.mdandbook/src/how/security.md;crates/akita-types/src/sis/physical_l2.rs,l2_table.rs, andrelation_range_image.rs;crates/akita-prover/src/protocol/sumcheck/digit_range/andphysical_l2_norm.rs;crates/akita-verifier/src/stages/physical_l2_norm.rs,stage1.rs, andstage2.rs;crates/akita-planner/src/schedule_params/candidate/recursive.rsandsuffix_dp.rs;