e4cead319d
Aere Network public source. Everything here can be checked against the live chain (chain id 2800, https://rpc.aere.network). Scope note, stated up front rather than buried: consensus on chain 2800 is classical secp256k1 ECDSA QBFT. The post-quantum work in this repository is at the signature, precompile, account and transport layers. Nothing here makes the consensus post-quantum, and no document in it should be read as claiming so.
122 lines
8.5 KiB
Markdown
122 lines
8.5 KiB
Markdown
# 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).
|