aere-docs/AERE-STARK-AIR-QUOTIENT-SUMMARY.md

Component (e): GENERIC AIR quotient-consistency check for STARK-verify precompile 0x0AE8

Scope caveat (2026-07-19 finding). This generic DEEP-ALI quotient check is conformance-confirmed against Plonky3 p3-uni-stark 0.4.3-succinct (Aere's OWN BabyBear + FRI STARK stack), NOT against SP1 6.1.0. SP1 6.1.0 is a Hypercube release (KoalaBear multilinear), and its inner recursion proof uses a sumcheck-based zerocheck plus LogUp-GKR, not a DEEP-ALI univariate quotient check, so this generic quotient mechanism (one of the two largest confirmed pieces) does NOT apply to SP1 6.1.0 at all and this work does not verify SP1 6.1.0 proofs. Note the "six generic components confirmed" claim below means a BabyBear+FRI STARK verifier skeleton, NOT an SP1 6.1.0 verifier. Replacing the SP1 BN254 Groth16 wrap is a separate ~22 to 32 person-week retarget. See AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md.

Date: 2026-07-19. Scope: implement + conformance-confirm the GENERIC AIR constraint / quotient consistency MECHANISM (the final generic piece of a BabyBear STARK verifier), keep the real SP1-proof path fail-closed.

Bottom line

• The GENERIC AIR quotient-consistency MECHANISM (component (e)'s DEEP-ALI identity) is now IMPLEMENTED and CONFORMANCE-CONFIRMED against the pinned Plonky3 p3-uni-stark 0.4.3-succinct via a REAL known answer test. KAT: pqc-fork/pq-stark/test_air_quotient.py PASS=18 FAIL=0 (Python + Node + standalone Java byte-identical). Accept genuine + reject tampered, on two known example AIRs.
• With this, all SIX generic components of a BabyBear STARK verifier skeleton (a, b, c, d, e-generic, f) are conformance-confirmed against the pinned crates.
• The top level STAYS FAIL-CLOSED for real SP1 proofs. The SP1-recursion-SPECIFIC AIR (its exact constraint set + interactions + public-value layout) and the vkey digest that binds it are NOT ported (StarkConstraints.SP1_RECURSION_AIR_PORTED = false), so StarkConstraints.evaluateAtZeta returns UNAVAILABLE on the real path and ACCEPT is unreachable. VERIFIED by a runtime check that drives the real precompile classes (computePrecompile returns EMPTY for a well-formed AS1 wire input).

1. The exact GENERIC quotient identity, confirmed from pinned source

Traced from p3-uni-stark 0.4.3-succinct verifier.rs (lines 90-141), p3-commit domain.rs (TwoAdicMultiplicativeCoset), and p3-air folder.rs / air.rs (VerifierConstraintFolder):

• Trace domain: TwoAdicMultiplicativeCoset { log_n = degree_bits, shift = 1 }, g = two_adic_generator(degree_bits).
• log_quotient_degree = log2_ceil(max_constraint_degree - 1); quotient_degree = 1 << log_quotient_degree.
• Quotient domain (create_disjoint_domain): log_n = degree_bits + log_quotient_degree, shift = trace.shift * Val::generator() = GENERATOR (= 31, confirmed via the extractor's val_generator). Chunk i (split_domains): log_n = degree_bits, shift = GENERATOR * two_adic_generator(degree_bits+log_quotient_degree)^i.
• alpha = sample_ext_element() after observing the trace commitment; zeta = sample() after observing the quotient-chunks commitment; zeta_next = zeta * g.
• Selectors at zeta (selectors_at_point, shift=1): z_h = zeta^(2^degree_bits) - 1; is_first_row = z_h/(zeta-1); is_last_row = z_h/(zeta - g^-1); is_transition = zeta - g^-1; inv_zeroifier = z_h^-1.
• Quotient reconstruction: zps[i] = prod_{j!=i} zp_j(zeta) * zp_j(chunk_i.first_point())^-1, where zp_D(pt) = (pt*shift_D^-1)^(2^log_n_D) - 1; then quotient(zeta) = sum_i zps[i] * sum_e monomial(e) * quotient_chunks[i][e], monomial(e)=x^e in F_{p^4}.
• Constraint fold (Horner in VerifierConstraintFolder.assert_zero): acc = acc*alpha + constraint, over the AIR eval() emission order; when_first_row/when_transition/when_last_row multiply the constraint by the corresponding selector. Rows: trace_local (zeta), trace_next (g*zeta).
• The identity (verifier.rs 137-141): folded_constraints * inv_zeroifier == quotient, i.e. folded_constraints(zeta) == Z_H(zeta) * quotient(zeta); OodEvaluationMismatch otherwise.

2. Ground-truth extractor (real p3-uni-stark proofs)

pqc-fork/pq-stark/airquotient-extractor/ (Cargo.toml + Cargo.lock + src/main.rs), depending on pinned p3-uni-stark / p3-air / p3-baby-bear / p3-commit 0.4.3-succinct (checksums fc3dfdeb... / d3a5de20... / d69e6e9a... / 50acacc7...; the last two match the Poseidon2/MMCS components). Built + run in a scratch target dir (never in the repo target); deterministic (regenerated byte-identical). For two KNOWN example AIRs it runs p3_uni_stark::prove then p3_uni_stark::verify, asserts the library ACCEPTS, and emits degree_bits / quotient_degree / trace openings / quotient-chunk openings / alpha / zeta (alpha, zeta re-derived by replaying the verifier's exact transcript prefix; the opened_values / commitments are recovered from the proof's own serde serialization):

• fibonacci_n8: Fibonacci AIR verbatim from p3-uni-stark's own tests/fib_air.rs (n=8, pis=[0,1,21]), 1 quotient chunk (log_quotient_degree=0).
• mul_deg3_n16: degree-3 multiply AIR matching tests/mul_air.rs (a^2*b - c, boundary b=a^2+1, transition next_a=a+1; n=16), 2 quotient chunks (log_quotient_degree=1) => exercises the zps product.

Output: pqc-fork/pq-stark/air_quotient_ground_truth.json.

3. Generic reference + KAT (RAN, PASS)

Three independent implementations of the generic identity: air_quotient_reference.py, air_quotient_reference.mjs, AirQuotientSelfTest.java. Harness test_air_quotient.py:

• Accept: the generic identity holds for both genuine proofs (matches the library ACCEPT).
• Reject: corrupt a trace opening -> identity fails; wrong quotient chunk -> fails; wrong alpha -> fails.
• Cross-language: Python/Node/Java produce byte-identical reconstructed quotient(zeta) and folded_constraints(zeta).
• Sanity: extractor perm_zeros == confirmed Poseidon2 "zeros" vector; val_generator == 31.

RESULT: PASS=18 FAIL=0. Recorded in pqc-fork/results/kat-results-air-quotient.json.

4. Wired into the precompile, GATED, fail-closed (RAN, PASS)

StarkConstraints in Sp1StarkVerifierPrecompiledContract.java:

• GENERIC_QUOTIENT_CHECK_CONFIRMED = true, checkGenericQuotient(...) implements the identity over BabyBearExt4 (component (a)); exercised only for a SUPPLIED example AIR under the KAT.
• SP1_RECURSION_AIR_PORTED = false (THE gate). evaluateAtZeta (real path) returns UNAVAILABLE while it is false; driver checks it at stage 4 before the query loop and before the single return ACCEPT.
• Runtime check PrecompileAirCheck (drives the REAL precompile classes, compiled against minimal Besu stubs): PASS=12 FAIL=0. Confirms the generic check accepts the ground truth + rejects tampers, evaluateAtZeta(null,null) == UNAVAILABLE, gate flags correct, and computePrecompile on a well-formed AS1 wire input returns EMPTY (ACCEPT unreachable for a real SP1 proof).

5. What remains (honest, out of scope here)

The SP1-recursion-SPECIFIC AIR + vkey binding (spec section 6.2): the entire sp1-recursion-core / sp1-stark symbolic constraint system (many columns, selectors, interaction/permutation argument, public-value bindings) and the vkey digest that commits to it. Plus a real end-to-end SP1-proof KAT (needs the SP1 toolchain + an exported SP1 v6.1.0 inner proof + the WireReader proof-body parser). Effort ~3 to 4 person-weeks + specialist STARK review. Marked [MEASURE].

The honest bottom line: the GENERIC BabyBear STARK verifier skeleton is now complete and conformance-confirmed on all 6 generic components (a-f), but verifying a real SP1 proof still needs the SP1-recursion-specific AIR + vkey, a real end-to-end proof KAT, an external audit, and founder activation. On-chain ZK verifiers on Aere remain classical BN254 Groth16 until the whole verifier is real and founder-activated. DO NOT ACTIVATE.

Files

• New: pqc-fork/pq-stark/air_quotient_reference.py / .mjs, AirQuotientSelfTest.java, test_air_quotient.py, air_quotient_ground_truth.json, airquotient-extractor/ (Cargo.toml + Cargo.lock + src/main.rs), pqc-fork/results/kat-results-air-quotient.json.
• Edited: pqc-fork/precompiles/Sp1StarkVerifierPrecompiledContract.java (StarkConstraints: generic mechanism + gate; class banner + stage-4 comment), docs/AERE-STARK-VERIFIER-PORT-SPEC.md (status header, section 6 rewritten into 6.1 generic + 6.2 SP1-specific, section 9 table, files), pqc-fork/pq-stark/README.md (status bullets, new (e) section, layout table, reproduce commands).