docs(verification): define verifier kernel proof plan

[quangvdao]

Summary

This PR proposes the formal verification plan for the low-level arithmetic used by the Akita verifier.

It does not change runtime code. It defines the targets, proof claims, dispatch rules, linkage checks, performance gates, and staged implementation work needed before Akita can claim that its production verifier kernels are proved down to machine code.

The proof plan now pins the combined s2n-bignum model revision db6d2002554d02a78cb4d6c183f16ecd75395691. This fork revision contains the initial AVX2 and NEON instruction semantics needed to begin the kernel proofs.

Why this is needed

The verifier currently relies on optimized CRT and NTT code, deferred fp128 accumulation, sparse challenge sampling, and a fixed-point operator-norm predicate. These paths have scalar differential tests, bounds checks, and security certificates, but most do not have a theorem about the exact instructions linked into the verifier binary.

The current exact fp128 path can also choose AVX-512 IFMA52 on capable x86 machines. The pinned s2n-bignum model has strong AVX2 and NEON proof support, but it does not model the IFMA52 path. A precise production policy is therefore needed before proof implementation starts.

Proposed design

The spec defines six claim layers for each kernel.

1. The mathematical algorithm is correct.
2. The exact instruction body implements that algorithm.
3. The complete symbol follows the platform ABI and memory frame.
4. The theorem bytes match the built object.
5. The final verifier binary contains those same bytes and calls that symbol.
6. Every supported runtime configuration selects a proved symbol or fails before verification.

The verified x86 profile uses AVX2 when available and a proved scalar symbol otherwise. It never selects AVX-512 IFMA52. This rule applies only to verifier-reachable cache construction and execution. The prover may keep IFMA52.

The AArch64 profile uses NEON with a proved scalar fallback where one remains supported. The RISC-V profile uses proved scalar objects and keeps the prepared cache artifact inside the stated setup and schedule binding.

Proof targets

The target registry covers:

• fp32, fp64, and fp128 base and extension field dependencies;
• i32 and i16 Montgomery conversion, range reduction, forward and inverse NTTs, pointwise dots, CRT reconstruction, and the complete exact matrix product;
• deferred fp128 product sums and accumulator headroom;
• signed sparse ring multiplication and multiply-add;
• unbiased range sampling, dense partial Fisher-Yates, sparse virtual permutation equivalence, sign assignment, and bounded rejection;
• D64 and D128 fixed-point root tables, integer no-wrap, AVX2 and NEON accumulation, the strict decision rule, and accepted-support certificate replay;
• selected hash and XOF objects as an explicit dependency for a complete challenge claim.

ISA audit findings

The pinned fork is based on upstream s2n-bignum revision ac31a43db30953037abd1b64b540e65cf31f4c67. It adds the four instruction families found missing by the source audit.

• Fork PR #4 adds VPSHUFHW and VPSHUFLW for the AVX2 i16 lane shuffles.
• Fork PR #3 adds VPMOVSXBW for signed i8 to i16 widening.
• Fork PR #2 adds the NEON LD4 and ST4 structure operations.
• Fork PR #1 adds NEON SHSUB signed halving subtraction.
• The AVX-512 IFMA52 path remains outside the current EVEX and instruction proof surface.

These PRs define and test instruction semantics. They do not prove the complete NTT, Montgomery multiplication, ABI symbol, linked object, or runtime dispatch. The exact production disassembly remains the source of truth because intrinsics do not fix the compiler's instruction choice.

Each extension still needs upstream review. The production proof profile records the fork while review is pending and must return to an upstream revision after acceptance.

Important boundaries

The spec keeps distinct claims separate.

• A CRT congruence theorem is not enough. The proof must also establish exact centered reconstruction and the capacity inequality.
• A SIMD accumulator theorem does not certify the fixed-point root table or accepted-support certificate.
• A Fisher-Yates theorem does not prove SHAKE256 or the random-oracle assumption.
• A proved object does not prove the final binary unless symbol resolution and bytes are checked after linking.
• The closed fp128 prototype in PR feat(fp128): prove production A7F7 add and sub #433 does not prove the later Jolt-owned production object. Akita must pin and check the actual linked theorem bundle.
• Constant-time execution is not an Akita acceptance criterion for this work. Verifier kernels may use variable-time behavior based on public data. The functional-correctness claim is not a side-channel claim.

Performance policy

The proposed large NTT symbols are out of line, but each call covers a complete transform, pointwise row dot, or matrix row. The spec forbids per-butterfly call boundaries.

Every replacement requires a named benchmark, raw before and after results, and an end-to-end verifier profile. The default limit is a two percent median regression unless maintainers approve the measured tradeoff. The IFMA52 to AVX2 verifier change must be measured on machines that currently select IFMA52.

Reviewer map

• specs/verifier-hol-light-kernels.md contains the complete goal, trust boundary, target registry, proof shape, implementation stages, tests, and performance gates.
• specs/PRUNING.md adds the proposal to the live specification set.
• book/src/foundations/spec-index.md exposes the new live proposal in the Book index.
• scripts/check-spec-references.sh includes the spec in the default dead-symbol scan.

Validation

• ./scripts/check-doc-guardrails.sh
• ./scripts/check-spec-references.sh
• typos specs/verifier-hol-light-kernels.md
• git diff --check

All commands pass locally.

Deferred work

This PR contains no proof objects and changes no production dispatch. The acceptance list remains open. The initial instruction definitions are available, but complete kernel theorems, upstream model review, standalone symbol boundaries, the x86 policy, and performance measurements remain deferred.

[cursor]

PR Summary

Low Risk
Documentation-only: no runtime, dispatch, or proof objects change. The spec later constrains verifier ISA policy, so review of those proposed rules still matters.

Overview
Adds a proposed live spec for proving Akita verifier arithmetic kernels in HOL Light against s2n-bignum processor models, from object bytes through final-binary linkage.

The spec is not a protocol proof. It defines six claim layers, a target registry (NTT/CRT matvec, deferred fp128, sampling, operator-norm), and a verified dispatch policy: AVX2 or scalar on x86 (no IFMA52), NEON on AArch64, scalar on RISC-V. Proofs must match linked production bytes; constant-time is explicitly out of scope.

Also wires verifier-hol-light-kernels.md into the Book spec index, PRUNING.md (15 live specs), and check-spec-references.sh. No implementation or proof objects land here.

^{Reviewed by Cursor Bugbot for commit 7082cf5. Bugbot is set up for automated code reviews on this repo. Configure here.}

[github-actions]

Documentation blast radius (advisory)

These regions may need doc/spec/book updates based on changed paths.
This is not a merge gate. See docs/documentation.md.

Changed files in this PR: 4

ci-tooling

CI workflows and repo scripts

Code paths touched:

• scripts/check-spec-references.sh

Consider updating:

• docs/ci-test-timing.md
• docs/documentation.md
• specs/archive/2026-Q3/ci-test-timing.md

book-tooling

Book structure and guardrails

Code paths touched:

• book/src/foundations/spec-index.md

Consider updating:

• book/README.md
• docs/documentation.md
• specs/PRUNING.md

---

Per-PR checklist: spec Status / acceptance criteria; book owning page; AGENTS.md if contracts changed; archive spec after fold.

[github-actions]

PCS Profile Benchmark

• Head: 7082cf5
• Workflow run: run 32616436851 attempt 1
• Merge base: 610f770 from the merge-base benchmarked on this runner.

13 of 13 profiles passed.

Times are medians of 3 measured runs after 1 discarded warmup run. Peak RSS is the largest measured value.

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 13 of 13 profiles. For matching profiles, the head and merge-base binaries ran interleaved on the same runner.

Benchmark shards

CI shard	Profiles
1-fp32-base	Fp32 dense nv30, direct setup check Fp32 one-hot nv34, direct setup check
2-fp64-base	Fp64 dense nv29, direct setup check Fp64 one-hot nv35, direct setup check
3-fp128-base	Fp128 dense nv28, direct setup check Fp128 one-hot nv36, direct setup check Fp128 one-hot nv36, recursive setup check
4-multi-group-direct	Fp128 multi-group, direct setup check
5-multi-group-recursive	Fp128 multi-group, recursive setup check
6-multi-group-recursive-w8r2	Fp128 multi-group W8R2, recursive setup check
7-distributed	Fp128 one-hot nv32 W2R2, direct setup check Fp128 one-hot nv32 W4R2, direct setup check Fp128 one-hot nv32 W8R2, direct setup check

Public opening statements

Public opening statement	Profiles
Over Fp32, one committed 30 variable multilinear polynomial with 2^30 coefficients is opened at one 30 coordinate point.	Fp32 dense nv30, direct setup check
Over Fp32, one committed 34 variable multilinear polynomial with 2^34 coefficients is opened at one 34 coordinate point.	Fp32 one-hot nv34, direct setup check
Over Fp64, one committed 29 variable multilinear polynomial with 2^29 coefficients is opened at one 29 coordinate point.	Fp64 dense nv29, direct setup check
Over Fp64, one committed 35 variable multilinear polynomial with 2^35 coefficients is opened at one 35 coordinate point.	Fp64 one-hot nv35, direct setup check
Over Fp128, one committed 28 variable multilinear polynomial with 2^28 coefficients is opened at one 28 coordinate point.	Fp128 dense nv28, direct setup check
Over Fp128, one committed 36 variable multilinear polynomial with 2^36 coefficients is opened at one 36 coordinate point.	Fp128 one-hot nv36, direct setup check Fp128 one-hot nv36, recursive setup check
Over Fp128, 4 polynomials in 3 groups: one 16 variable polynomial at its own point, one 16 variable polynomial at its own point, and 2 34 variable polynomials at one shared point.	Fp128 multi-group, direct setup check Fp128 multi-group, recursive setup check
Over Fp128, 4 polynomials in 3 groups: one 16 variable polynomial at its own point, one 16 variable polynomial at its own point, and 2 32 variable polynomials at one shared point.	Fp128 multi-group W8R2, recursive setup check
Over Fp128, one committed 32 variable multilinear polynomial with 2^32 coefficients is opened at one 32 coordinate point.	Fp128 one-hot nv32 W2R2, direct setup check Fp128 one-hot nv32 W4R2, direct setup check Fp128 one-hot nv32 W8R2, direct setup check

One-hot profiles generate deterministic witnesses with one 1 in every consecutive chunk of 256 coefficients. This witness shape is not a separate public claim.

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 W2R2, W4R2, W8R2 divide the witness relation into the stated number of exact chunks for the first two fold levels.

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

Profile	Setup	Commit	Prove	Verify, multi-threaded	Verify, single-threaded
Fp32 dense nv30, direct setup check	0.053 s -0.5%	2.370 s +0.5%	2.723 s -1.0%	15.4 ms +0.3%	40.1 ms -0.2%
Fp32 one-hot nv34, direct setup check	0.057 s +0.1%	2.272 s -0.4%	2.667 s +0.6%	17.7 ms +0.4%	54.0 ms -0.0%
Fp64 dense nv29, direct setup check	0.113 s +3.0%	4.454 s -2.4%	2.258 s +2.4%	13.9 ms -0.3%	42.5 ms +0.0%
Fp64 one-hot nv35, direct setup check	0.221 s -0.4%	3.354 s +0.2%	2.828 s +0.0%	16.5 ms -0.8%	75.9 ms -0.9%
Fp128 dense nv28, direct setup check	0.108 s -0.1%	8.518 s -0.0%	2.834 s -0.1%	18.8 ms +0.2%	69.7 ms +0.1%
Fp128 one-hot nv36, direct setup check	0.274 s -0.1%	8.010 s -0.1%	4.415 s -2.5%	27.1 ms +0.4%	159.2 ms +0.1%
Fp128 one-hot nv36, recursive setup check	0.889 s -0.5%	7.998 s +0.4%	5.090 s -0.5%	20.4 ms -0.6%	52.8 ms -0.4%
Fp128 multi-group, direct setup check	0.936 s -0.4%	8.421 s -0.3%	2.902 s -1.0%	22.9 ms -1.2%	124.1 ms +0.1%
Fp128 multi-group, recursive setup check	1.648 s +0.4%	7.485 s +1.0%	2.968 s -0.4%	18.5 ms +0.5%	31.1 ms +0.9%
Fp128 multi-group W8R2, recursive setup check	0.492 s +1.4%	2.157 s -0.0%	4.580 s +0.6%	27.7 ms -0.9%	79.4 ms +0.2%
Fp128 one-hot nv32 W2R2, direct setup check	0.209 s -0.8%	0.593 s +0.2%	1.288 s +0.1%	15.0 ms +0.5%	39.7 ms -0.3%
Fp128 one-hot nv32 W4R2, direct setup check	0.217 s +0.1%	0.590 s -0.2%	1.828 s +0.3%	16.0 ms -1.0%	52.2 ms +0.5%
Fp128 one-hot nv32 W8R2, direct setup check	0.211 s -0.0%	0.589 s -0.5%	2.579 s -0.0%	18.9 ms +1.1%	55.0 ms -0.3%

Proof size and protocol shape

Profile	Fold A/B/D schedule	Total proof	Fold payload	Terminal response	Fold levels	Grinding retries
Fp32 dense nv30, direct setup check	2048/256/256 → 256/256/256 → 128/128/128	68,762 bytes +0.0%	30,220 bytes +0.0%	38,542 bytes +0.0% z 20,622 · e 2,560 · t 15,360	7 +0.0%	None
Fp32 one-hot nv34, direct setup check	2048/256/256 → 256/256/256 → 128/128/128	69,193 bytes +0.0%	26,828 bytes +0.0%	42,365 bytes +0.0% z 20,861 · e 3,072 · t 18,432	7 +0.0%	None
Fp64 dense nv29, direct setup check	1024/256/64 → 128/64/64 → 64/64/64	70,755 bytes +0.0%	24,876 bytes +0.0%	45,879 bytes +0.0% z 20,791 · e 3,584 · t 21,504	7 +0.0%	None
Fp64 one-hot nv35, direct setup check	1024/256/64 → 512/256/64 → 64/64/64	71,174 bytes +0.0%	25,276 bytes +0.0%	45,898 bytes +0.0% z 20,810 · e 3,584 · t 21,504	7 +0.0%	None
Fp128 dense nv28, direct setup check	512/64/64 → 64/64/64	72,951 bytes +0.0%	19,916 bytes +0.0%	53,035 bytes +0.0% z 20,267 · e 8,192 · t 24,576	7 +0.0%	None
Fp128 one-hot nv36, direct setup check	512/64/64 → 256/64/64 → 64/64/64	73,996 bytes +0.0%	20,892 bytes +0.0%	53,104 bytes +0.0% z 20,336 · e 8,192 · t 24,576	7 +0.0%	None
Fp128 one-hot nv36, recursive setup check	512/64/64 → 256/64/64 → 64/64/64	76,414 bytes +0.0%	23,308 bytes +0.0%	53,106 bytes +0.0% z 20,338 · e 8,192 · t 24,576	7 +0.0%	None
Fp128 multi-group, direct setup check	512/64/64 → 64/64/64	73,502 bytes +0.0%	20,444 bytes +0.0%	53,058 bytes +0.0% z 20,290 · e 8,192 · t 24,576	7 +0.0%	None
Fp128 multi-group, recursive setup check	512/128/128 → 64/64/64	91,149 bytes +0.0%	33,152 bytes +0.0%	57,997 bytes +0.0% z 22,157 · e 7,168 · t 28,672	8 +0.0%	L7: 4 / 4 / 4
Fp128 multi-group W8R2, recursive setup check	256/64/64 → 64/64/64	79,497 bytes +0.0%	26,432 bytes +0.0%	53,065 bytes +0.0% z 20,297 · e 8,192 · t 24,576	8 +0.0%	None
Fp128 one-hot nv32 W2R2, direct setup check	512/64/64 → 64/64/64	73,443 bytes +0.0%	20,332 bytes +0.0%	53,111 bytes +0.0% z 20,343 · e 8,192 · t 24,576	7 +0.0%	None
Fp128 one-hot nv32 W4R2, direct setup check	512/64/64 → 256/64/64 → 64/64/64	73,966 bytes +0.0%	20,892 bytes +0.0%	53,074 bytes +0.0% z 20,306 · e 8,192 · t 24,576	7 +0.0%	None
Fp128 one-hot nv32 W8R2, direct setup check	512/64/64 → 64/64/64	74,689 bytes +0.0%	21,596 bytes +0.0%	53,093 bytes +0.0% z 20,325 · e 8,192 · t 24,576	7 +0.0%	None

Grinding retries are rejected attempts at each fold, listed in measured-run order. Zero means the first sampled nonce was accepted.

Memory and setup size

Profile	Setup vector	Prepared NTT cache	Verifier NTT cache	Peak RSS
Fp32 dense nv30, direct setup check	22.0 MiB +0.0%	206.0 MiB +0.0%	0.9 MiB +0.0%	5070.8 MiB +0.4%
Fp32 one-hot nv34, direct setup check	32.0 MiB +0.0%	234.0 MiB +0.0%	0.9 MiB +0.0%	1494.7 MiB -0.6%
Fp64 dense nv29, direct setup check	44.0 MiB +0.0%	478.0 MiB +0.0%	1.5 MiB +0.0%	5320.8 MiB +0.0%
Fp64 one-hot nv35, direct setup check	128.0 MiB +0.0%	960.0 MiB +0.0%	1.5 MiB +0.0%	2683.6 MiB -0.1%
Fp128 dense nv28, direct setup check	86.0 MiB +0.0%	424.0 MiB +0.0%	1.0 MiB +0.0%	5220.3 MiB -0.2%
Fp128 one-hot nv36, direct setup check	256.0 MiB +0.0%	1150.0 MiB +0.0%	1.0 MiB +0.0%	3817.4 MiB -0.1%
Fp128 one-hot nv36, recursive setup check	256.0 MiB +0.0%	1174.5 MiB +0.0%	1.0 MiB +0.0%	3866.0 MiB +0.1%
Fp128 multi-group, direct setup check	256.0 MiB +0.0%	1487.9 MiB +0.0%	1.2 MiB +0.0%	3338.8 MiB +0.3%
Fp128 multi-group, recursive setup check	256.0 MiB +0.0%	1614.9 MiB +0.0%	1.6 MiB +0.0%	3465.1 MiB -0.1%
Fp128 multi-group W8R2, recursive setup check	128.0 MiB +0.0%	542.9 MiB +0.0%	1.0 MiB +0.0%	2620.7 MiB +0.0%
Fp128 one-hot nv32 W2R2, direct setup check	64.0 MiB +0.0%	371.5 MiB +0.0%	1.2 MiB +0.0%	1042.3 MiB +0.2%
Fp128 one-hot nv32 W4R2, direct setup check	64.0 MiB +0.0%	405.8 MiB +0.0%	1.2 MiB +0.0%	1335.0 MiB -1.0%
Fp128 one-hot nv32 W8R2, direct setup check	64.0 MiB +0.0%	371.5 MiB +0.0%	1.2 MiB +0.0%	1653.4 MiB +0.2%

Deltas are shown only for profiles with a matching merge-base case. Negative is smaller or faster.

The uploaded report.md benchmark artifact contains the detailed fold schedule, proof-size breakdown, terminal response segments, and Golomb diagnostics.

[github-actions]

CI test timing

• Report generated: 2026-08-23T04:22:45Z.
• Source: 89d98e2 on codex/verifier-hollight-spec.
• Workflow run: 32616436835.
• Main baseline: 610f770.
• Previous run: f0afefe.

Run summary

Wall s	Main wall s	Main Δ	Ratio	Tests	Skipped	Failed	Status
512.0	344.0	+48.8%	1.49x	1703	0	0	ok

Wall time spans 2 parallel nextest slice shards.

Slowest tests

Rank	Duration s	Test
1	13.7	akita-pcs::akita_fp128_e2e::fp128_dense
2	12.2	akita-planner::schedule_params::adaptive_search_tests::uniform_suffix_dp_matches_unpruned_exact_cutover_search
3	9.6	akita-pcs::scheme::tests::onehot::multi_group_root_allows_precommitted_arity_above_final_group
4	7.3	akita-pcs::scheme::tests::onehot::selective_l2::selective_l2_proof_rejects_transcript_mutations
5	4.5	akita-planner::schedule_params::adaptive_search_tests::production_suffix_selects_l2_with_the_typed_response_model
6	4.1	akita-planner::planner::totality_tests::contractive_winner_remains_selected
7	4.0	akita-prover::kernels::linear::tests::chunking::q128_many_blocks_digits_chunk_instead_of_unsafe_block_parallel
8	3.9	akita-pcs::akita_small_field_e2e::selective_l2::fp32_ext4_multiblock_l2_pcs_roundtrip_and_stage2_rejections
9	3.4	akita-planner::schedule_params::adaptive_search_tests::adaptive_nv36_minimizes_first_direct_setup_before_proof_bytes
10	3.3	akita-pcs::akita_fp128_e2e::fp128_onehot
11	3.3	akita-pcs::akita_small_field_e2e::fp32_dense
12	3.2	akita-pcs::akita_small_field_e2e::fp64_dense_pre
13	3.2	akita-pcs::setup::adaptive_dense::large_setup_batch_passes
14	3.2	akita-pcs::akita_fp128_e2e::fp128_onehot_pre
15	3.1	akita-pcs::akita_small_field_e2e::selective_l2::fp32_nv20_shipped_terminal_route_roundtrip_and_rejections
16	3.0	akita-pcs::akita_small_field_e2e::fp32_onehot_pre
17	2.8	akita-pcs::akita_small_field_e2e::fp32_dense_pre
18	2.8	akita-planner::schedule_params::adaptive_search_tests::mixed_domain_search_beats_or_ties_uniform_d64
19	2.8	akita-pcs::protocol_soundness::dense_rejects_mismatched_committed_group_profile_geometry
20	2.7	akita-pcs::akita_fp128_e2e::fp128_onehot_batched

Regressions vs main

No per-test regressions above the threshold.

New slow tests

No new tests ≥30s vs main baseline.