aere-network/aere-docs
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
main
aere-docs/AERE-STARK-VERIFIER-PORT-SPEC.md
Aere Network e4cead319d Initial public release 
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.
2026-07-20 01:01:36 +03:00

59 KiB
Raw Permalink Blame History

AERE STARK verifier port specification (0x0AE8): component order, interfaces, vectors, effort

SCOPE CAVEAT (research finding, 2026-07-19; read before anything else). The six generic components below are real and conformance-confirmed, but they were confirmed against Plonky3 0.4.3-succinct (Aere's OWN BabyBear + FRI STARK stack, the zk-circuits/* provers), NOT against SP1 6.1.0. The pinned SP1 (facade = "=6.1.0", resolved internals sp1-hypercube 6.3.1) is a Hypercube release, not Turbo: its inner recursion proof is a KoalaBear multilinear proof (BaseFold + Jagged/Stacked PCS + sumcheck-zerocheck + LogUp-GKR with a septic-curve global digest), NOT a BabyBear FRI ShardProof. FRI and the DEEP-ALI univariate quotient check, the two largest confirmed pieces here, do NOT apply to SP1 6.1.0 at all (they are replaced by BaseFold and by sumcheck-zerocheck). So this document specifies a real BabyBear+FRI verifier skeleton that verifies Aere's own Plonky3 STARKs; it does NOT, and completing the "SP1 recursion AIR" line below would NOT, verify an SP1 6.1.0 proof. Replacing the BN254 Groth16 wrap on real SP1 proofs is a SEPARATE ~22 to 32 person-week effort and a founder retarget decision, specified in AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md and AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC.md. Read the whole of this document with "SP1 6.1.0 inner STARK" mentally replaced by "a BabyBear + FRI STARK (Aere's own Plonky3 circuits)", except where the retarget summary is cited.

Spec date: 2026-07-19 Status: PORT PLAN + sub-components implemented and tested; the Poseidon2 permutation (component (b)), the MMCS vector commitment (component (c)), the FRI FOLD + OPENING relation / low-degree test (component (d), verify_query), the Fiat-Shamir duplex-sponge transcript / challenger (component (f)), AND now the GENERIC AIR constraint / quotient-consistency MECHANISM (component (e), the DEEP-ALI identity) are all CONFORMANCE-CONFIRMED against the pinned Plonky3 (a real known-answer test PASSES for each). With component (e)'s generic mechanism confirmed, all SIX generic components of a BabyBear STARK verifier skeleton are now conformance-confirmed. The precompile 0x0AE8 is STILL a REFERENCE SKELETON that verifies NOTHING for a real SP1 proof and fail-closes (returns EMPTY for every input), because the SP1-recursion-SPECIFIC AIR (its exact constraint set + interactions + public-value layout) and the vkey digest that binds it are NOT ported. This document does not change the fail-closed contract. It specifies, component by component, the multi-week cryptography port that would make 0x0AE8 a real post-quantum STARK verifier, and it records the self-contained sub-components implemented and tested so far: the BabyBear field F_p and its degree-4 extension F_{p^4} (section 2, component (a), the FOUNDATION), the Poseidon2 permutation over BabyBear (section 3, component (b), the hash, now conformance-confirmed), the MMCS / FieldMerkleTreeMmcs vector commitment (section 4, component (c), now conformance-confirmed), the FRI query-index derivation (section 8, one slice of component (d)), the full FRI fold + opening verify_query (section 5, component (d), now conformance-confirmed against the pinned p3-fri), and the GENERIC AIR quotient-consistency check (section 6, component (e)'s generic mechanism, now conformance-confirmed against the pinned p3-uni-stark). These are building blocks, NOT a working verifier: (b), (c), (d)'s fold+opening, (f) the duplex-sponge Fiat-Shamir transcript, and (e)'s generic quotient identity now match Plonky3 (real KATs passed). Component (f) DERIVES the FRI betas / query indices / grinding IN-CIRCUIT from the transcript, and that closes the loop the FRI KAT left open: the derived betas/indices, fed into the confirmed (d) verify_query, accept the real FRI ground-truth proof and reject a tampered beta (pq-stark/test_challenger.py, PASS=44). Component (e)'s generic quotient check reproduces the pinned p3-uni-stark verifier's ACCEPT on two known example AIRs (Fibonacci + degree-3 mul) and rejects tampered openings/quotient/alpha (pq-stark/test_air_quotient.py, PASS=18). The remaining un-ported crypto-core piece is the SP1-recursion-SPECIFIC AIR + vkey binding (part of component (e), section 6.2), so the top level STAYS FAIL-CLOSED for real SP1 proofs: with StarkConstraints.SP1_RECURSION_AIR_PORTED = false, StarkConstraints.evaluateAtZeta returns UNAVAILABLE at the constraint stage, before the query loop and before the single return ACCEPT, so verify() returns EMPTY for every real input.

Companion documents (read together):

  • docs/PQ-STARK-VERIFIER-PRECOMPILE-2026-07-18.md (design, encoding, soundness, gas).
  • docs/PQ-STARK-VERIFIER-ACTIVATION-2026-07-18.md (gated activation plan).
  • pqc-fork/precompiles/Sp1StarkVerifierPrecompiledContract.java (the fail-closed skeleton).
  • contracts/contracts/zkverify/AerePQStarkVerifier.sol (the fail-closed ISP1Verifier adapter).

0. Honest scope and non-claims (read first)

  • The top-level verifier does NOT work. It has never verified a real STARK proof and it cannot in this build. Sp1StarkVerifierPrecompiledContract.verify(...) reaches the delegated crypto core, which returns UNAVAILABLE, so the driver returns EMPTY. The single return ACCEPT line is unreachable. Nothing in this document makes it reachable.
  • This is a multi-week port, stated plainly. The realistic effort for one STARK/FRI specialist is on the order of 3 to 4 months (roughly 11 to 16 person-weeks of focused work plus audit), and the two hardest components (the SP1 recursion AIR constraint evaluation and the FRI low-degree test) are each multi-week on their own. See section 9.
  • Until this port is complete, externally audited, and founder-activated, the on-chain ZK verifiers on Aere remain the CLASSICAL BN254 Groth16 gateway (0x9ca479C8c52C0EbB4599319a36a5a017BCC70628). That path is Shor-breakable. We say this plainly. 0x0AE8 is a post-quantum verifier skeleton being built, not a live capability, and (per the scope caveat at the top) the skeleton specified here targets BabyBear + FRI STARKs, i.e. Aere's own Plonky3 circuits, NOT SP1 6.1.0 proofs; replacing the SP1 BN254 Groth16 wrap is a separate founder-gated retarget to the SP1 6.1.0 Hypercube stack.
  • Consensus on chain 2800 is classical secp256k1 ECDSA QBFT (N=7, f=2). This precompile is an EVM-layer verifier and changes none of that.
  • [VERIFY] marks a constant, round count, or convention that must be confirmed against the pinned reference before it can be trusted (it is NOT invented here). [MEASURE] marks a validation that requires running the pinned reference or the SP1 prover and cannot be produced offline in this pass.

1. What is being verified, and the port decomposition

The target this document was originally written against is a BabyBear + FRI STARK: a Plonky3 ShardProof over the BabyBearPoseidon2 config. Correction (see the scope caveat at the top): the 2026-07-19 finding established that SP1 6.1.0 does NOT produce such a proof (it is Hypercube / KoalaBear multilinear), so this exact ShardProof<BabyBearPoseidon2> target is Aere's OWN Plonky3 circuits (zk-circuits/*), not SP1 6.1.0. Verifying such a BabyBear+FRI STARK directly on-chain is a real capability, but it does NOT remove the BN254 Groth16 wrap from an SP1 6.1.0 proof, because SP1 6.1.0 has no BabyBear FRI ShardProof in its chain. Removing the SP1 Groth16 wrap is the separate Hypercube retarget (AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md). Read the SP1-framed sentences below with that substitution in mind.

A faithful verifier decomposes into six components with a strict dependency order. Each higher component consumes the ones below it, so they MUST be ported bottom-up and each validated against its own vectors before the next is trusted.

  (f) Fiat-Shamir transcript (Poseidon2 duplex challenger)   <- pervasive, threads through d and e
  (e) AIR constraint evaluation + SP1 recursion vk binding    HARDEST
  (d) FRI folding + query-index derivation + low-degree test  HARD   <- section 8 implements one slice
  (c) Merkle / FRI vector-commitment scheme
  (b) Poseidon2 permutation over BabyBear (the hash)          error-prone (constants)
  (a) BabyBear field p = 2^31 - 2^27 + 1 and its degree-4 extension   FOUNDATION

Recommended port order: (a) then (b) then (f, the transcript, since it is just a Poseidon2 sponge) then (c) then (d) then (e). Component (f) is listed last in the decomposition because it is conceptually the glue, but in build order it comes right after Poseidon2 because everything above it needs a working challenger to derive the same randomness the prover used.

The rest of this section is one subsection per component: what it does, its interface, the exact test vectors that validate it and where they come from, an effort estimate, and the parts that are hardest or still [VERIFY].

2. Component (a): BabyBear field and degree-4 extension

What it does. Provides the base field F_p, p = 15 * 2^27 + 1 = 2013265921 = 0x78000001 (a 31-bit prime with 2^27 | (p-1), giving a large smooth two-adic subgroup for evaluation domains), and the degree-4 binomial extension F_{p^4} = F_p[x]/(x^4 - W). |F_{p^4}| is approximately 2^124.05. FRI folding challenges, the DEEP out-of-domain point zeta, and query soundness all live in F_{p^4}.

Interface.

  • Fp: add, sub, mul, neg, inv (Fermat a^(p-2)), pow, from/to canonical u32, two-adic generator of the order-2^27 subgroup and its powers.
  • Fp4: add, sub, mul (schoolbook convolution reduced by x^4 = W), inv, Frobenius, base embedding.

State in the skeleton (IMPLEMENTED + TESTED, 2026-07-19). BabyBear is COMPLETE (canonical, non-Montgomery, 64-bit intermediates): add, sub, neg, mul, pow, inv (Fermat a^(p-2)), plus the multiplicative generator (GENERATOR = 31) and the two-adic generator of the order-2^27 subgroup (twoAdicGenerator(bits)). BabyBearExt4 is now COMPLETE: W is PINNED to 11, and add, sub, neg, mul (schoolbook convolution reduced by x^4 = W), inv (Fermat a^(p^4-2)), Frobenius (a^p), and the base embedding are all implemented. The former W_UNSET/TODO(port) guard is removed. Wiring the completed field into the precompile does NOT make ACCEPT reachable: the field sits behind the still-UNAVAILABLE crypto core (Poseidon2, FRI fold arithmetic, AIR), so the top level still returns EMPTY for every input and the "DO NOT ACTIVATE / verifies nothing" contract is unchanged.

Validated offline (pqc-fork/pq-stark/test_babybear_field.py, ran 2026-07-19, PASS=396242 FAIL=0, Python + Node + Java byte-identical; standalone BabyBearFieldSelfTest PASS=360018 FAIL=0):

  • F_p and F_{p^4} field axioms (comm/assoc/distrib/identities/inverses) over many random cases;
  • Fermat inverse a^(p-2) equals an INDEPENDENT extended-Euclid bignum inverse (Python pow(a,-1,p));
  • GENERATOR = 31 has multiplicative order exactly p-1 (proven via the known p-1 = 2^27 * 3 * 5);
  • twoAdicGenerator(k) has order exactly 2^k for k = 1..27;
  • W = 11 is a quadratic non-residue and p == 1 mod 4, so x^4 - 11 is IRREDUCIBLE over F_p (Lidl-Niederreiter binomial criterion), i.e. F_{p^4} is a genuine field; x^4 == W holds in F_{p^4};
  • Frobenius^4 = identity, Frobenius fixes the base field, base embedding is a ring homomorphism.

[VERIFY] items (the field is real and self-consistent; these are the conformance-to-Plonky3 gaps).

  • W = 11: PROVEN here to yield an irreducible x^4 - 11 (hence a real field), but that 11 is Plonky3's exact BinomialExtensionField<BabyBear, 4> non-residue is [VERIFY]/[MEASURE] against p3_baby_bear at the pinned SP1 v6.1.0 revision. A wrong-but-still-irreducible W builds a valid field that silently DISAGREES with the prover, so irreducibility is necessary, not sufficient.
  • GENERATOR = 31: PROVEN here to have order p-1, but that it is Plonky3's chosen multiplicative generator (and that twoAdicGenerator(27) = 440564289 is Plonky3's stored root of unity) is [VERIFY]. The ORDER is a proven field fact; the exact VALUE is not confirmed offline.
  • Whether the production port uses Montgomery form (Plonky3 does, MontyField31) for performance. Canonical form is correct and simpler; Montgomery is a perf optimization to benchmark, not a correctness requirement.

Test vectors.

  • Field identities (a * inv(a) = 1, distributive/associative laws, generator order p-1, subgroup generator has order 2^27). Self-checkable offline, no external source. IMPLEMENTED + PASSING (test_babybear_field.py; Sp1StarkVerifierKat.fieldArithmeticKats also asserts a subset).
  • Extension: (x^4 - W) irreducibility for the pinned W; Fp4 inverse round-trips; Frobenius^4 = id. IMPLEMENTED + PASSING.
  • Conformance: a handful of p3-baby-bear / p3-field unit outputs (mul, inv, extension mul) for fixed inputs, cross-checked byte-for-byte. Source: Plonky3 p3-baby-bear tests. [MEASURE] (needs the pinned Plonky3 source; not fetched offline in this pass, marked not faked).

Effort. About 0.5 person-week. Low risk. IMPLEMENTED + TESTED in this pass; the remaining work is the [VERIFY]/[MEASURE] conformance of W / generator against Plonky3 and the Montgomery-vs-canonical gas decision.

3. Component (b): Poseidon2 permutation over BabyBear (the hash)

What it does. The fixed-width algebraic permutation that Plonky3 uses as both the Merkle/vector commitment compression function and the duplex-sponge Fiat-Shamir challenger. Everything hashed in the proof (commitments, transcript) is Poseidon2 over BabyBear.

Parameters (Plonky3 Poseidon2BabyBear, the SP1 config).

  • Width t = 16 field elements. [VERIFY] (SP1's BabyBear Poseidon2 permutation width; 16 is the Plonky3 default used by the recursion config).
  • S-box: x^7. Degree 7 is the smallest exponent d > 1 with gcd(d, p-1) = 1: p-1 = 2^27 * 3 * 5, so d must avoid factors 2, 3, 5, and the smallest such d is 7. x^7 is therefore a bijection on F_p. This is number-theoretically CONFIRMED offline (the section-3 harness asserts d=7 is the minimal coprime degree and that the monomial inverse round-trips). This one is solid, not [VERIFY].
  • External (full) rounds: 8 (4 initial + 4 terminal), applying the S-box to all 16 lanes. CONFIRMED (poseidon2_round_numbers_128(16, 7) returns (8, 13)).
  • Internal (partial) rounds: 13, applying the S-box to lane 0 only. CONFIRMED (poseidon2_round_numbers_128(16, 7) = (8, 13)).
  • External linear layer: the Poseidon2 M_E matrix, built from the fixed MDS matrix M4 = 2,3,1,1],[1,2,3,1],[1,1,2,3],[3,1,1,2 in the MDS-light block construction (diagonal blocks 2*M4, off-diagonal blocks M4). CONFIRMED: the full 16x16 external matrix recovered from Plonky3's Poseidon2ExternalMatrixGeneral (via basis-vector probes) equals this exact block form.
  • Internal linear layer: M_I = R^{-1} * (J + diag(D)) (J = all-ones), applied as state[i] = R_INV * (sum(state) + D[i]state[i]), with D = INTERNAL_DIAG_M1_16 and R_INV = 943718400 = (2^32)^{-1} mod p. CONFIRMED: this is p3-baby-bear's DiffusionMatrixBabyBear as a canonical map (the R^{-1} factor is a Montgomery-form artifact, recovered exactly from the library's 16x16 canonical matrix: off-diagonal = R^{-1}, diagonal = R^{-1}(1 + D[i])). The textbook form state[i]*D[i] + sum (a prior pass) is self-consistent but WRONG (the two-wrong-copies trap).
  • Round constants: 8 * 16 external + 13 internal = 141 BabyBear elements. CONFIRMED: extracted from the pinned crates (generated by Xoroshiro128Plus::seed_from_u64(1) via new_from_rng_128). THEY ARE NOT INVENTED HERE; they are copied byte-exact from the pinned reference.

Interface.

  • poseidon2_permute(state: [Fp; 16]) -> [Fp; 16] (the raw permutation).
  • poseidon2_compress(l: [Fp; 8], r: [Fp; 8]) -> [Fp; 8] (the 2-to-1 Merkle compression; typically a truncated permutation or a sponge, [VERIFY] which Plonky3 TruncatedPermutation shape SP1 uses).

State (IMPLEMENTED + CONFORMANCE CONFIRMED, 2026-07-19; real KAT PASSES). The permutation is implemented at width 16: the x^7 S-box, the 8 external rounds with the M4-based MDS-light layer, the 13 internal rounds with the R^{-1}*(J+diag(D)) diagonal layer, the initial external linear layer, and the 141-constant round schedule (external add to all 16 lanes, internal add to lane 0). It lives in Poseidon2Bb.permute in the precompile (with compress2to1) and in three independent references: pqc-fork/pq-stark/poseidon2_babybear_reference.py, .mjs (Node), and Poseidon2BabyBearSelfTest.java (standalone). Because the permutation is confirmed, Poseidon2Bb.available is now true. This does NOT make ACCEPT reachable: the duplex-sponge challenger is a separate un-ported component (Challenger.spongePorted = false), and the constraint eval and FRI are un-ported (StarkConstraints = UNAVAILABLE), so the top level returns EMPTY for every input.

CONFORMANCE CONFIRMED (pqc-fork/pq-stark/test_poseidon2_babybear.py, ran 2026-07-19, PASS=47017 FAIL=0, Python + Node + Java byte-identical; standalone Poseidon2BabyBearSelfTest PASS=13536 FAIL=0). The pinned crates p3-poseidon2 / p3-baby-bear at crates.io version 0.4.3-succinct (checksums 522986377b2164c5f94f2dae88e0e0a3d169cc6239202ef4aeb4322d60feffd0 / d69e6e9af4eaaaa60f7bb9f0e0f73ebcbaefe7e00974d97ad0fa542d6a4f0890, byte-identical to the repo's zk-circuits/*/Cargo.lock and rollup-evm-validity/*/Cargo.lock) were executed via cargo to emit the constants and three permutation known-answer vectors. The reference reproduces all three EXACTLY:

  • KAT zeros (input [0;16]) -> [1787823396, 953829438, 89382455, ...] (16 values);
  • KAT iota (input [0..15]) -> [157639285, 1851003038, 1852457045, ...];
  • KAT testvec(p3 test input) -> [512585766, 975869435, 1921378527, ...]. Full vectors + source URLs are recorded in pqc-fork/pq-stark/spec-poseidon2-constants.md. Additional self-consistency (also passing): x^7 bijection (7 = smallest coprime degree; inverse round-trips), the permutation is a genuine bijection (inverse round-trips + 0 collisions), M4 MDS, both linear layers invertible, and three-language byte-identity.

CONFIRMED items (all previously [VERIFY], now closed by the real KAT):

  • The 141 ROUND CONSTANTS are the CONFIRMED Xoroshiro128Plus::seed_from_u64(1) / new_from_rng_128 values, extracted (canonical) from the pinned crates. A prior pass used SHA-256 PLACEHOLDERS; those are replaced.
  • INTERNAL_DIAG_M1_16 = [p-2, 1, 2, 4, 8, ..., 8192, 32768] CONFIRMED (canonical) against p3-baby-bear's POSEIDON2_INTERNAL_MATRIX_DIAG_16_BABYBEAR_MONTY. The Montgomery subtlety is resolved: the internal LAYER carries a canonical R^{-1} factor (see the internal-linear-layer bullet above), which a prior pass missed.
  • ROUNDS_P = 13, ROUNDS_F = 8 CONFIRMED (poseidon2_round_numbers_128(16, 7) = (8, 13)).
  • M4 and the MDS-light M_E CONFIRMED (recovered byte-exact from Poseidon2ExternalMatrixGeneral).

Remaining [VERIFY] for this component: only the 2-to-1 Merkle compression convention (component (c)): which 8 output lanes / padding / rate SP1's TruncatedPermutation uses for compress2to1.

Hardest part (now done). Getting all 141 round constants, the internal diagonal, the internal-layer Montgomery R^{-1} factor, and M4 byte-exact. This was the classic footgun (two implementations sharing wrong constants agree with each other but not Plonky3); it is closed by executing the pinned crates and diffing the real known-answer vectors, which cannot be faked.

Test vectors.

  • Structural, self-checkable offline: PASSING (see the State paragraph): x^7 bijection, M4 MDS, external/internal layers invertible, permutation inverse round-trip, cross-language agreement.
  • Conformance (the real gate): PASSED. The pinned p3-baby-bear / p3-poseidon2 0.4.3-succinct crates were executed to produce known-answer outputs for fixed inputs (all-zero, [0..15], the p3 width-16 test vector); the port reproduces them byte-for-byte. Recorded in pqc-fork/pq-stark/spec-poseidon2-constants.md and ../results/kat-results-poseidon2-babybear.json.

Effort. Constants + internal-layer conformance: DONE. Remaining for a full component (c)/(d)/(e)/(f) port is the sponge transcript, Merkle/MMCS, FRI fold arithmetic, and the recursion AIR.

4. Component (c): Merkle / MMCS vector-commitment scheme (IMPLEMENTED + CONFORMANCE-CONFIRMED)

What it does. The commitment layer FRI (d) and the trace commitment are built on: a Merkle tree (Plonky3 FieldMerkleTreeMmcs) whose leaves are rows of field elements and whose internal nodes are Poseidon2 compressions, supporting batched, mixed-height openings (the "mixed matrix commitment scheme", MMCS). The verifier checks that a claimed opening (a row of values plus an authentication path) hashes up to a committed root.

State (IMPLEMENTED + CONFORMANCE CONFIRMED, 2026-07-19; real KAT PASSES). The MMCS is implemented as the EXACT SP1 inner config, confirmed verbatim from p3-merkle-tree's own mmcs.rs tests:

  • leaf hasher PaddingFreeSponge<Perm, WIDTH=16, RATE=8, OUT=8> (overwrite-mode, padding-free sponge);
  • 2-to-1 node compressor TruncatedPermutation<Perm, N=2, CHUNK=8, WIDTH=16> (i.e. compress([l,r]) = permute(l||r)[0..8], the Poseidon2Bb.compress2to1 already present);
  • FieldMerkleTreeMmcs<Packing, Packing, MyHash, MyCompress, DIGEST_ELEMS=8>, so a digest is 8 BabyBear elements (32 bytes). It lives in Mmcs in the precompile (hashIter, compress2to1, verifyBatch) and in three independent references: pqc-fork/pq-stark/mmcs_babybear_reference.py, .mjs (Node), and MmcsBabyBearSelfTest.java (standalone, which also builds/opens the tree for testing). Because the construction and outputs are confirmed, Mmcs.available is now true. This does NOT make ACCEPT reachable: the duplex-sponge challenger (Challenger.spongePorted = false, component (f)), the FRI fold arithmetic (component (d)), and the recursion AIR (StarkConstraints = UNAVAILABLE, component (e)) are un-ported, so the top level returns EMPTY for every input.

Interface.

  • verify_batch(root: Digest, dimensions: [(width, height)], index: usize, opened_rows: [[Fp]], proof: [Digest]) -> bool: recompute the root from the opened leaf rows and the sibling digests along the path, compare to root. This is the ONLY method the on-chain verifier needs; the tree build (commit) and open_batch are prover-side and live only in the offline references.

Dependencies. Poseidon2 (b) for the leaf hash and node compression, field (a) for the leaf encoding.

CONFORMANCE CONFIRMED (pqc-fork/pq-stark/test_mmcs_babybear.py, ran 2026-07-19, PASS=300 FAIL=0, Python + Node + Java byte-identical; standalone MmcsBabyBearSelfTest PASS=80 FAIL=0). The pinned crates p3-merkle-tree / p3-symmetric / p3-commit / p3-matrix at crates.io version 0.4.3-succinct (checksums d5703d92... / 9047ce85... / 50acacc7... / 75c3f150..., byte-identical to the repo Cargo.lock) were executed via cargo (extractor) to commit to six known matrix batches and emit the root plus an open_batch opening (opened rows + sibling path) for each; the extractor also asserts the library's OWN verify_batch accepts them. This reference reproduces every root, opening, and proof EXACTLY (canonical u32), and its verify_batch accepts the emitted openings and rejects tampered ones. The six cases exercise: single power-of-two height, single non-power-of-two height (zero-digest padding), a column vector, and three mixed-height batches (including one whose proof contains a default zero-digest sibling). Full vectors + source URLs are in pqc-fork/pq-stark/spec-mmcs-babybear.md. A perm-sanity KAT (the extractor's permute([0;16])) equals the confirmed Poseidon2 "zeros" vector, proving the extractor uses the same confirmed permutation.

CONFIRMED items (all previously [VERIFY], now closed by the real KAT).

  • The leaf-hashing convention (a row of width-w elements is absorbed by the overwrite-mode PaddingFreeSponge, RATE 8, over the concatenation of all matrices at that height) CONFIRMED.
  • The mixed-height batching rule (tallest-first, pad each layer to a power of two with the zero digest, inject shorter matrices via compress([node, hash(rows)]) at the layer whose padded length matches, index reduced by index >> (log_max_height - log2_ceil(height))) CONFIRMED.
  • The digest width (8 BabyBear elements = 32 bytes) and the TruncatedPermutation compression shape (permute(l||r) truncated to 8 lanes) CONFIRMED.

Multi-matrix generalization. The references and Mmcs.verifyBatch handle the full mixed-height MMCS, not just the single-matrix case: matrices are grouped tallest-first by padded height, the running root is seeded with the tallest group's hashed concatenated rows, and each shorter group is compressed in at the proof layer whose padded length matches its next_power_of_two height (Plonky3's height property guarantees every padded bucket holds one exact height). The KAT includes three genuine mixed batches (2 and 3 matrices, powers-of-two and non-powers-of-two), so this path is exercised, not just documented.

Remaining [MEASURE] for this component: conformance against a REAL exported SP1 v6.1.0 commitment root (the trace / FRI matrices from an actual proof), which needs an exported proof and the challenger. The construction is confirmed; matching a real proof's root is the end-to-end integration check.

Effort. Confirmed and implemented in this pass. The batching / mixed-height indexing was the fiddly part and is now traced against the pinned source and KAT-locked.

5. Component (d): FRI folding, query-index derivation, low-degree test

What it does. FRI (Fast Reed-Solomon IOP of Proximity) is the polynomial-commitment / low-degree test at the heart of the STARK. The verifier:

  1. observes the commit-phase Merkle roots, sampling a folding challenge beta_i in F_{p^4} per round;
  2. observes the final polynomial and checks the grinding (proof-of-work) witness;
  3. derives num_queries query indices from the transcript (the query-index derivation);
  4. for each query, walks the folding: opens the sibling pair at each layer against that layer's commitment (component c), checks the fold relation p_{i+1}(x^2) = fold(p_i, beta_i) at the query point, and confirms the final value matches the committed final polynomial.

State (IMPLEMENTED + CONFORMANCE CONFIRMED, 2026-07-19; real KAT PASSES for the FOLD + OPENING relation). Two slices are now real: (1) the query-index derivation and per-layer folding-index walk (section 8, FriQueryIndex), and (2) the full per-query FOLD + OPENING check verify_query (this section), traced verbatim from the pinned p3-fri verifier.rs and CONFORMANCE-CONFIRMED against a real FRI proof emitted by the pinned p3-fri prover. It lives in Fri.verifyQuery in the precompile (Fri.foldRelationConfirmed = true) and in three independent references (pqc-fork/pq-stark/fri_verify_reference.{py,mjs}, FriVerifySelfTest.java; harness test_fri_verify.py, PASS=55 FAIL=0). The fold ARITHMETIC (interpolate the two sibling evaluations through beta at the coset point, in F_{p^4}), the coset-point / bit-reversal mapping, and the per-layer MMCS opening (component (c)) are all now IMPLEMENTED, not delegated. The transcript BINDING that derives the betas / query indices / grinding IN-CIRCUIT from the Poseidon2 sponge (component (f)) is now ALSO confirmed (section 7): its derived betas/indices are re-verified end to end against this section's verify_query (transcript -> betas/indices -> FRI verify, PASS in test_challenger.py), so this section's KAT no longer needs the betas/indices as external inputs. What is still NOT ported is the AIR reduced-opening combination (component (e)). So even with the fold+opening AND the transcript confirmed, the top level stays FAIL-CLOSED (Fri.checkQuery returns UNAVAILABLE; the AIR StarkConstraints.evaluateAtZeta returns UNAVAILABLE before the query loop).

Interface.

  • derive_query_indices(challenger, num_queries, log_max_height) -> [usize; num_queries] (section 8: implemented as FriQueryIndex.sampleBits + the sampling loop; the challenger squeeze is component (f)).
  • query_fold_walk(index, log_max_height, log_final_poly_len) -> [FoldStep] where each FoldStep gives (index_in_layer, sibling = index ^ 1, index_pair = index >> 1, parity) (section 8: implemented as FriQueryIndex.walk).
  • verify_query(log_blowup, log_max_height, commits, betas, index, reduced_openings, sibling_values, opening_proofs) -> Fp4|null (IMPLEMENTED + CONFIRMED): walk the arity-2 folding, MMCS-open the sibling pair per layer (component (c)), interpolate the pair through beta at the coset point x = two_adic_generator(log_max_height)^reverse_bits_len(index) (the sibling point is -x), fold down to a single F_{p^4} constant. verify_challenges checks that constant equals final_poly for every query. betas / index / reduced_openings are INPUTS (transcript = component (f), AIR = component (e)).

CONFIRMED (all previously [VERIFY], now closed by the real KAT vs pinned p3-fri 0.4.3-succinct).

  • Arity-2 folding with index_sibling = index ^ 1, index_pair = index >> 1. CONFIRMED against p3-fri verifier.rs.
  • log_max_height = commit_phase_commits.len() + log_blowup; num_fold_rounds = log_max_height - log_blowup; the final polynomial is a single F_{p^4} CONSTANT (log_final_poly_len = 0). CONFIRMED.
  • The coset point x = two_adic_generator(log_max_height)^reverse_bits_len(index, log_max_height), in F_{p^4}; the sibling point is x * two_adic_generator(1) = -x. CONFIRMED (bit-reversal mapping).
  • two_adic_generator(bits) = Plonky3's stored value (the fold coset points come out right only if it matches). CONFIRMED. The F_{p^4} non-residue W = 11 is Plonky3's (the EF fold reproduces the interpolation). CONFIRMED.
  • The commit-phase MMCS is ExtensionMmcs<Val,Challenge,ValMmcs>: a leaf is a PAIR of F_{p^4} evals flattened to 8 BabyBear coords, opened by the CONFIRMED base FieldMerkleTreeMmcs (component (c)). CONFIRMED.

[VERIFY] / [MEASURE] items still open.

  • sample_bits LSB masking (section 8) and the transcript observe/sample ORDER are component (f), now CONFIRMED (section 7): the betas/indices are derived in-circuit from the transcript and re-verified end to end against this section's verify_query (transcript -> betas/indices -> FRI verify). The betas/indices are no longer taken as inputs in the closed-loop KAT.
  • The proximity parameters (num_queries, log_blowup, pow_bits) and the resulting soundness. The skeleton placeholders are {100, 1, 16} (inner) and {25, 4, 16} (wrap) and MUST be replaced by the frozen SP1 config, then scored by ethSTARK soundcalc (design doc section 4). [MEASURE].

Test vectors.

  • Implemented and validated (section 8): the query-index derivation and folding-index walk.
  • CONFORMANCE (the real gate for the fold+opening): PASSED. The pinned p3-fri 0.4.3-succinct crate was executed (pqc-fork/pq-stark/fri-extractor) to emit real FRI proofs over known low-degree polynomials (with the confirmed seed_from_u64(1) Poseidon2), confirmed accepted by the library's own verify_challenges; the references + Fri.verifyQuery reproduce the ACCEPT byte-for-byte and REJECT four tamper variants (corrupted opened value, corrupted MMCS sibling, wrong beta/fold, non-matching final poly). Recorded in pqc-fork/pq-stark/spec-fri-babybear.md, ../results/kat-results-fri-verify.json, and fri_ground_truth.json.
  • [MEASURE] remaining: the actual query indices and fold values for a REAL exported SP1 v6.1.0 inner proof (needs the Poseidon2 challenger, component (f), and the AIR reduced openings, component (e)).

Effort. The index logic (section 8) and the fold + opening relation (this section, verify_query) are DONE and conformance-confirmed in this pass: the fold arithmetic, the coset/bit-reversal mapping, and the per-layer MMCS opening all match the pinned p3-fri. What remains for a full component (d) in a real verifier is only its INPUTS: the proximity-parameter pinning against the frozen SP1 config ([MEASURE]) and the transcript that derives the betas/indices (component (f)) plus the AIR reduced openings (component (e)). Those are separate components; until they are ported the top level stays fail-closed.

6. Component (e): AIR constraint evaluation and quotient consistency (GENERIC mechanism now IMPLEMENTED + CONFORMANCE-CONFIRMED; SP1-recursion-specific AIR + vkey remain [MEASURE])

What it does. The STARK proper. It checks that the committed trace satisfies the AIR (Algebraic Intermediate Representation): evaluate every transition, boundary, and public-value constraint at the DEEP out-of-domain point zeta, combine them with a random challenge alpha into a single folded constraint value, and check that the quotient the prover committed is consistent (the DEEP-ALI / quotient consistency check). For SP1 it also binds the proof to the specific program by checking the verification-key digest and the public values.

This component SPLITS into two parts, and the split IS the fail-closed gate:

  • (1) the GENERIC quotient-consistency MECHANISM (AIR-agnostic; works for ANY AIR): now IMPLEMENTED + CONFORMANCE-CONFIRMED (2026-07-19). This is the tractable, ground-truth-confirmable piece.
  • (2) the SPECIFIC SP1 recursion AIR (its exact constraint set + interactions + public-value layout) and the vkey digest that commits to it: a large, program-specific, multi-week port needing the SP1 toolchain. UN-PORTED. This is what keeps the top level FAIL-CLOSED for real SP1 proofs.

6.1 The GENERIC quotient-consistency check (IMPLEMENTED + CONFORMANCE-CONFIRMED)

The exact generic identity a p3-uni-stark verifier checks, traced verbatim from the pinned p3-uni-stark 0.4.3-succinct verifier.rs (lines 90-141), p3-commit domain.rs (TwoAdicMultiplicativeCoset selectors), and p3-air folder.rs/air.rs (VerifierConstraintFolder):

  1. Trace domain = TwoAdicMultiplicativeCoset { log_n = degree_bits, shift = 1 } (TwoAdicFriPcs::natural_domain_for_degree). g = two_adic_generator(degree_bits).
  2. log_quotient_degree = log2_ceil(max_constraint_degree - 1); quotient_degree = 1 << log_quotient_degree.
  3. 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 domain i (split_domains): log_n = degree_bits, shift = GENERATOR * two_adic_generator(degree_bits + log_quotient_degree)^i.
  4. Selectors at zeta (selectors_at_point, trace domain, 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.
  5. Quotient reconstruction (verifier.rs lines 90-116): 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], with monomial(e) = x^e in F_{p^4} and quotient_chunks[i] the D=4 opened F_{p^4} coordinates of chunk i.
  6. Constraint fold (VerifierConstraintFolder, Horner): acc = acc * alpha + constraint, over the AIR eval() emission order; when_first_row/when_transition/when_last_row multiply the constraint by is_first_row/is_transition/is_last_row (p3-air air.rs FilteredAirBuilder). The trace openings trace_local (at zeta) and trace_next (at g*zeta) are the two AIR rows.
  7. The identity: folded_constraints * inv_zeroifier == quotient, i.e. folded_constraints(zeta) == Z_H(zeta) * quotient(zeta); OodEvaluationMismatch otherwise (verifier.rs lines 137-141).

Interface (implemented).

  • checkGenericQuotient(degree_bits, alpha, zeta, public_values, trace_local, trace_next, quotient_chunks, air_id) -> bool: the identity check above, for a SUPPLIED example AIR constraint evaluator (air_id). Lives in StarkConstraints.checkGenericQuotient in the precompile (StarkConstraints.GENERIC_QUOTIENT_CHECK_CONFIRMED = true) plus three independent references (pq-stark/air_quotient_reference.{py,mjs}, AirQuotientSelfTest.java).
  • Still NOT on the real path: bind_vk(vkey_digest, preprocessed_commitment) and the SP1 recursion AIR constraint evaluator (part 2 below).

CONFORMANCE CONFIRMED (pq-stark/test_air_quotient.py, ran 2026-07-19, PASS=18 FAIL=0, Python + Node + standalone Java byte-identical). The pinned crates p3-uni-stark / p3-air / p3-baby-bear / p3-commit 0.4.3-succinct (checksums fc3dfdeb... / d3a5de20... / d69e6e9a... / 50acacc7..., the last two byte-identical to the Poseidon2/MMCS components) were executed via cargo (pq-stark/airquotient-extractor) to run p3_uni_stark::prove then p3_uni_stark::verify on two KNOWN example AIRs and confirm the LIBRARY accepts, then emit the openings + alpha (sample_ext) + zeta (sample) by replaying the verifier's exact transcript prefix:

  • fibonacci_n8: the Fibonacci AIR verbatim from p3-uni-stark's own tests/fib_air.rs (n = 8, public values [0, 1, 21]), which has ONE quotient chunk (log_quotient_degree = 0);
  • mul_deg3_n16: a degree-3 multiply AIR matching tests/mul_air.rs (columns [a,b,c], constraint a^2*b - c plus a boundary b = a^2 + 1 and a transition next_a = a + 1, n = 16), which has TWO quotient chunks (log_quotient_degree = 1), so it exercises the split-domain zps product. The generic reference reproduces the library ACCEPT on both (the identity holds) and REJECTS three tamper variants per case: a corrupted trace opening, a wrong quotient chunk, a wrong alpha. Full vectors are in pq-stark/air_quotient_ground_truth.json and ../results/kat-results-air-quotient.json. The extractor's perm_zeros equals the confirmed Poseidon2 "zeros" vector and its val_generator equals 31, tying the ground truth to the confirmed sub-components.

6.2 The SPECIFIC SP1 recursion AIR + vkey binding (UN-PORTED, [MEASURE], the fail-closed gate)

Hardest part, and the hardest component overall. The GENERIC mechanism (6.1) working on a small example AIR does NOT let the precompile verify a real SP1 proof: the SP1 recursion machine AIR is not a short formula. It is the entire sp1-recursion-core / sp1-stark symbolic constraint system (many columns, selectors, the multiset/permutation interaction argument that links chips, and public-value bindings), plus the vkey digest that commits to it. Porting it means reproducing the exact constraint polynomials, the challenge derivation order, the interaction/permutation argument, and the DEEP quotient combination, all byte-consistent with StarkVerifier::verify_shard. A single off-by-one in a selector or a mis-ordered challenge makes the whole thing silently wrong.

[MEASURE] / [VERIFY] items (part 2, un-ported). The full recursion AIR (columns, constraints, interactions); the public-values layout and binding; the vkey_digest domain (vk.hash_babybear() packed). All against sp1-stark at the pinned v6.1.0 revision, and only a real exported SP1 inner proof exercises them end to end.

Fail-closed gate. In the precompile, StarkConstraints.SP1_RECURSION_AIR_PORTED = false. While it is false, StarkConstraints.evaluateAtZeta (the REAL verify path) returns UNAVAILABLE at stage 4 (before the query loop and before the single return ACCEPT), so computePrecompile returns EMPTY for a real SP1 proof and ACCEPT is unreachable. This is VERIFIED: a runtime check drives the real precompile classes (the generic check accepts the ground truth + rejects tampers; evaluateAtZeta(null,null) == UNAVAILABLE; computePrecompile on a well-formed AS1 wire input returns EMPTY).

Test vectors (end-to-end, part 2). Only real, exported SP1 inner proofs exercise this. [MEASURE] end-to-end: ACCEPT a valid exported shrink/wrap proof, REJECT one with a mutated public value or a flipped trace opening. This also needs the WireReader proof-body parser and the whole stack wired.

Effort. Part 1 (the generic mechanism): DONE + conformance-confirmed in this pass (~0.5 person-week of the estimate). Part 2 (the SP1 recursion AIR + vkey + end-to-end KAT): about 3 to 4 person-weeks, the largest single item, and the one most in need of a specialist STARK review. This is where "multi-week port" is most literally true.

7. Component (f): Fiat-Shamir transcript (Poseidon2 duplex challenger) (IMPLEMENTED + CONFORMANCE-CONFIRMED)

What it does. The non-interactive transcript. A duplex sponge over Poseidon2 that absorbs ("observe") the vkey digest, public values, and every commitment in a FIXED order, and squeezes ("sample") the verifier randomness (folding challenges, alpha, zeta, query indices, grinding challenge). If the observe/sample order does not match the prover exactly, every derived challenge diverges and nothing verifies.

State (IMPLEMENTED + CONFORMANCE CONFIRMED, 2026-07-19; real KAT PASSES). The challenger is the EXACT SP1 inner DuplexChallenger<BabyBear, Perm, WIDTH=16, RATE=8> plus the GrindingChallenger check_witness, traced verbatim from the pinned p3-challenger 0.4.3-succinct source (duplex_challenger.rs, grinding_challenger.rs) over the CONFIRMED Poseidon2 permutation (component (b)). It lives in Challenger in the precompile (Challenger.spongePorted = true) and in three independent references: pqc-fork/pq-stark/challenger_reference.py, .mjs (Node), and ChallengerSelfTest.java (standalone). CONFIRMED behaviour, all from source:

  • observe(felt): overwrite-mode absorb; clears the output buffer, pushes to the input buffer, and duplexes (permutes) once the input buffer reaches RATE=8. Digests/ext elements are observed element-by-element (observe_ext_element = observe the 4 base coords in order).
  • duplexing: overwrite the first input_buffer.len() (<= RATE) lanes of the 16-lane state with the buffered inputs, permute, then set the output buffer to state lanes [0..RATE).
  • sample() -> Fp / sample() -> Fp4: duplex if inputs are buffered OR the output buffer is empty, then pop() from the END of the output buffer (Vec::pop); an Fp4 sample is 4 sequential base pops [c0, c1, c2, c3] (sample_ext_element = sample_vec(4) then from_base_slice).
  • sample_bits(bits): the LOW bits bits of a base sample's as_canonical_u64 (CONFIRMED LSB, not MSB). This is the query-index reduction (section 8).
  • check_witness(pow_bits, witness): observe(witness) then sample_bits(pow_bits) == 0 (grinding).

Interface.

  • observe(felts: [Fp]), observe_digest(d: Digest), sample() -> Fp4, sample_bits(bits) -> usize, check_witness(pow_bits, witness) -> bool (grinding).

Dependencies. Poseidon2 (b). This is a thin, mostly-mechanical layer on top of the permutation, but its ORDER is a strict, pervasive contract shared with components (d) and (e).

CONFORMANCE CONFIRMED (pqc-fork/pq-stark/test_challenger.py, ran 2026-07-19, PASS=44 FAIL=0, Python + Node + standalone Java byte-identical; standalone ChallengerSelfTest PASS=31). The pinned crate p3-challenger 0.4.3-succinct (the exact challenger DuplexChallenger<Val, Perm, 16, 8> + GrindingChallenger), with the transcript ORDER taken from p3-fri 0.4.3-succinct verify_shape_and_sample_challenges, was executed via cargo (pqc-fork/pq-stark/challenger-extractor, byte-identical lockfile) to emit two ground-truth blocks, both reproduced EXACTLY by the references:

  • a fully-scripted observe/sample transcript: base samples, F_{p^4} ext samples, sample_bits, the full 16-lane sponge state at a checkpoint, and a check_witness accept/reject table (a real grinding witness accepts, fixed non-witnesses reject) all match byte-for-byte;
  • the FRI transcript closure: for the SAME three FRI cases the component (d) ground truth uses, the betas + query indices + grinding acceptance are DERIVED from the transcript (commit-phase commits + final poly + pow witness) and match BOTH the pinned p3-fri challenger AND fri_ground_truth.json. Fed into the CONFIRMED (d) verify_query, the derived betas/indices ACCEPT the real FRI proof and REJECT a tampered beta. This CLOSES the loop (d) left open (transcript -> betas/indices -> FRI verify); the betas/indices are now derived in-circuit, not taken as inputs. Recorded in pqc-fork/results/kat-results-challenger.json and pqc-fork/pq-stark/challenger_ground_truth.json.

CONFIRMED items (all previously [VERIFY], now closed by the real KAT).

  • The observe/sample SEQUENCE (verify_shape_and_sample_challenges): per commit-phase commit, observe the 8-element digest then sample one beta in F_{p^4}; then observe the final polynomial (4 base coords); then check_witness(pow_bits, pow_witness); then num_queries x sample_bits(log_max_height).
  • The sponge RATE/CAPACITY split for width 16 (RATE=8, capacity 8, overwrite-mode absorb) and the Vec::pop LIFO squeeze order.
  • The grinding convention (check_witness = observe then sample_bits == 0).

Remaining [MEASURE] for this component: the transcript of a REAL exported SP1 v6.1.0 proof (the exact observe order of the vkey digest, trace/quotient commitments, opened values, and DEEP zeta/alpha sampling for the AIR). That is part of component (e)'s integration and needs an exported proof.

Test vectors. Conformance (the real gate): PASSED (see the State paragraph). The transcript reproduces the pinned p3-challenger / p3-fri sampled values byte-for-byte and closes the FRI betas/indices loop.

Effort. Confirmed and implemented in this pass. The observe/sample ordering and the Vec::pop squeeze direction were the subtle parts (an order mismatch presents as "everything rejects" with no localized error); both are now traced against the pinned source and KAT-locked.

8. The ONE sub-component implemented and tested in this pass: FRI query-index derivation

Rationale for the choice. Of the two candidates the task names (the Poseidon2 permutation, or the FRI query-index derivation), the query-index derivation is the one that can be validated HONESTLY with RUNNING, PASSING tests offline in a single pass, because it is determined entirely by a public integer specification and depends on NO secret round constants. Poseidon2, by contrast, cannot be conformance-validated without the exact Plonky3 constants (section 3); implementing it and testing it only against a same-constants reference would prove self-consistency, not conformance, and would risk exactly the "two wrong copies agree" trap. So Poseidon2 is left as a fully-specified [VERIFY] port target (section 3) and the FRI query-index derivation is the piece implemented and tested here.

What is implemented (constant-free, spec-determined integer logic).

  • sample_bits(canonical_u32, bits): reduce a sampled BabyBear field element (its canonical u32 representative) to a query index in [0, 2^bits) by taking the low bits bits. This is the transcript-to-index step of derive_query_indices.
  • walk(index, log_max_height, log_final_poly_len): the per-layer folding-index walk, producing for each of the num_fold_rounds = log_max_height - log_final_poly_len FRI layers the tuple (index_in_layer, sibling = index ^ 1, index_pair = index >> 1, parity = index & 1), and the terminal final_index = index >> num_fold_rounds that must index the final polynomial's domain.

Where it lives.

  • Production side (Java, behind the still-fail-closed top level): a new FriQueryIndex static helper in pqc-fork/precompiles/Sp1StarkVerifierPrecompiledContract.java, referenced from Fri.checkQuery for the index-derivation step. Wiring it does NOT make ACCEPT reachable: the fold arithmetic and Poseidon2 Merkle opening are still delegated, so Fri.checkQuery still returns UNAVAILABLE and the driver still returns EMPTY. The top level stays fail-closed.
  • Independent references and tests: pqc-fork/pq-stark/fri_query_index_reference.py (Python), pqc-fork/pq-stark/fri_query_index_reference.mjs (Node, a genuinely different-language second implementation), pqc-fork/pq-stark/FriQueryIndexSelfTest.java (a standalone copy of the exact Java helper logic, compilable and runnable without the Besu classpath), and the harness pqc-fork/pq-stark/test_fri_query_index.py.

How it is validated (what actually ran).

  1. Hand-computed golden vectors (worked out by hand in the harness comments and asserted).
  2. Structural invariants over many random cases: sibling differs from index in exactly bit 0; each layer halves the index; after num_fold_rounds layers the index collapses into the final-poly domain ([0, 2^log_final_poly_len)); sample_bits output is always in range and equals the low bits; full-width sample_bits is the identity.
  3. Cross-language agreement: Python, Node, and Java implementations produce byte-identical walks and sample_bits outputs over a shared vector set. Three independent implementations (two languages plus a hand golden) agreeing validates the LOGIC against the public spec.

What this does and does NOT prove. It proves the index LOGIC matches the public Plonky3/FRI specification and is internally consistent across three implementations. It does NOT prove conformance to a real SP1 v6.1.0 trace, because the actual sampled indices come out of the Poseidon2 challenger on a real proof, which needs component (b) and an exported proof. That conformance is [MEASURE]:

# [MEASURE] conformance of derive_query_indices against a real SP1 inner proof.
# On a throwaway non-infra prover box (see pqc-fork/pq-stark/export-inner-stark-vector.md):
#   1. export an SP1 v6.1.0 shrink proof + its FriConfig (num_queries, log_blowup, pow_bits),
#   2. instrument the Plonky3 p3-fri verifier to print the sampled query indices and each layer's
#      (index, index_sibling, index_pair) for one query,
#   3. feed the same challenger transcript bytes into fri_query_index_reference and assert the
#      derived indices and fold walks match byte-for-byte.

Test result of this pass: see section 8 of pqc-fork/pq-stark/README.md and the machine-readable pqc-fork/results/kat-results-fri-query-index.json. Summary is recorded there and in the port summary; the top-level verifier remains fail-closed and unchanged in behavior.

9. Total effort, hardest parts, and the honest multi-week statement

component effort (person-weeks) risk status
(a) field + F_{p^4} ~0.5 low IMPLEMENTED + TESTED (2026-07-19); W pinned + proven-irreducible; [VERIFY] W/gen = Plonky3's
(b) Poseidon2-BabyBear ~1.5 to 2 medium (constants) IMPLEMENTED + CONFORMANCE-CONFIRMED (2026-07-19, PASS=47017; real KAT vs p3-* 0.4.3-succinct, checksums matched)
(c) Merkle / MMCS ~1 to 1.5 medium IMPLEMENTED + CONFORMANCE-CONFIRMED (2026-07-19, PASS=300; real KAT vs p3-merkle-tree/p3-symmetric/p3-commit 0.4.3-succinct); end-to-end vs a real proof root [MEASURE]
(d) FRI fold + query + LDT ~2 to 3 high index derivation (section 8) + FOLD+OPENING verify_query (section 5) IMPLEMENTED + CONFORMANCE-CONFIRMED (2026-07-19, PASS=55; real KAT vs p3-fri 0.4.3-succinct: accept genuine + reject tampered). Remaining: proximity params [MEASURE]; betas/indices come from the transcript (f)
(e) AIR + quotient consistency (GENERIC mechanism) ~0.5 medium IMPLEMENTED + CONFORMANCE-CONFIRMED (2026-07-19, PASS=18; real KAT vs p3-uni-stark/p3-air/p3-commit 0.4.3-succinct: the generic DEEP-ALI identity accepts two known example AIRs' proofs + rejects tampered)
(e) SP1-recursion-SPECIFIC AIR + vkey binding ~3 to 4 HARDEST [MEASURE] port target (the SP1 recursion machine AIR + vkey; keeps the top level fail-closed for real SP1 proofs; needs the SP1 toolchain + a real end-to-end proof KAT)
(f) Fiat-Shamir transcript ~0.5 to 1 medium (pervasive) IMPLEMENTED + CONFORMANCE-CONFIRMED (2026-07-19, PASS=44; real KAT vs p3-challenger/p3-fri 0.4.3-succinct: transcript reproduced byte-for-byte AND the derived FRI betas/indices close the loop into the confirmed (d) verify_query). Real SP1-proof transcript order [MEASURE] (part of (e))
integration, gas bench, conformance corpus, audit prep ~2 to 3 high not started
total ~11 to 16 multi-week / multi-month

Hardest parts, ranked: (1) the SP1-recursion-SPECIFIC AIR constraint evaluation + vkey binding (part 2 of component e, section 6.2), the single largest and most error-prone item, still un-ported and [MEASURE] (the GENERIC quotient mechanism of component (e) is now done + confirmed, section 6.1); (2) the FRI fold arithmetic and its coset/bit-reversal mapping plus proximity-parameter pinning (component d); (3) transcribing the Poseidon2 constants exactly (component b). None of these is a weekend job. A realistic single-specialist timeline is 3 to 4 months including the conformance corpus and audit preparation, which is why the production path the design doc recommends (section 5.1) is to wrap a pinned, reproducible native build of the maintained Rust references rather than hand-port all six components into Java.

Whichever path is taken, the gate is unchanged: the top-level 0x0AE8 stays fail-closed until the whole verifier is real, KAT-green against real vectors, soundcalc-scored, gas-benchmarked under the EIP-7825 cap, externally audited, isolated-soaked, and founder-activated (docs/PQ-STARK-VERIFIER-ACTIVATION-2026-07-18.md). Nothing short of that verifies a real proof.

Conclusion, scoped honestly (per the top caveat). The six generic components (a-f, minus the SP1-recursion-specific AIR) form a REAL, conformance-confirmed BabyBear + FRI STARK verifier skeleton, validated byte-for-byte against the pinned Plonky3 0.4.3-succinct crates. That skeleton verifies BabyBear + FRI STARKs, for example Aere's own Plonky3 zk-circuits. It does NOT verify SP1 6.1.0 proofs, and finishing the "SP1 recursion AIR" row above would NOT make it do so: SP1 6.1.0 is Hypercube (KoalaBear multilinear, BaseFold + Jagged + sumcheck-zerocheck + LogUp-GKR), a different proof system in which FRI and DEEP-ALI play no part. Replacing the BN254 Groth16 wrap on real SP1 proofs is therefore a separate ~22 to 32 person-week retarget and a founder decision, specified in AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md and AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC.md. The effort table above (~11 to 16 person-weeks) is the cost of a BabyBear+FRI verifier, not of an SP1 6.1.0 verifier.

10. Files

  • docs/AERE-STARK-VERIFIER-PORT-SPEC.md (this document).
  • pqc-fork/precompiles/Sp1StarkVerifierPrecompiledContract.java (fail-closed skeleton + the COMPLETE BabyBear / BabyBearExt4 field arithmetic from section 2, the Poseidon2Bb permutation from section 3 (available true, conformance-confirmed), the Mmcs vector commitment from section 4 (available true, conformance-confirmed), the FriQueryIndex helper from section 8, the FRI Fri.verifyQuery fold + opening relation from section 5 (Fri.foldRelationConfirmed true, conformance-confirmed; Fri.checkQuery stays gated), the Challenger duplex sponge from section 7 (Challenger.spongePorted true, conformance-confirmed), and the StarkConstraints.checkGenericQuotient generic AIR quotient-consistency mechanism from section 6.1 (StarkConstraints.GENERIC_QUOTIENT_CHECK_CONFIRMED true, conformance-confirmed), all wired behind the fail-closed top level. The remaining un-ported crypto-core piece is the SP1-recursion-SPECIFIC AIR + vkey binding (section 6.2): with StarkConstraints.SP1_RECURSION_AIR_PORTED = false, StarkConstraints.evaluateAtZeta (the real path) returns UNAVAILABLE at the constraint stage before the query loop and before the single return ACCEPT, so computePrecompile still returns EMPTY for every real SP1 proof input).
  • pqc-fork/pq-stark/babybear_field_reference.py, babybear_field_reference.mjs, BabyBearFieldSelfTest.java, test_babybear_field.py (the section-2 field sub-component + tests).
  • pqc-fork/results/kat-results-babybear-field.json (machine-readable field test result).
  • pqc-fork/pq-stark/poseidon2_babybear_reference.py, poseidon2_babybear_reference.mjs, Poseidon2BabyBearSelfTest.java, test_poseidon2_babybear.py (the section-3 Poseidon2 sub-component
    • tests; conformance to Plonky3 CONFIRMED via a real KAT, see spec-poseidon2-constants.md).
  • pqc-fork/results/kat-results-poseidon2-babybear.json (machine-readable Poseidon2 test result).
  • pqc-fork/pq-stark/mmcs_babybear_reference.py, mmcs_babybear_reference.mjs, MmcsBabyBearSelfTest.java, test_mmcs_babybear.py (the section-4 MMCS sub-component + tests; conformance to Plonky3 CONFIRMED via a real KAT, see spec-mmcs-babybear.md).
  • pqc-fork/results/kat-results-mmcs-babybear.json (machine-readable MMCS test result).
  • pqc-fork/pq-stark/fri_query_index_reference.py, fri_query_index_reference.mjs, FriQueryIndexSelfTest.java, test_fri_query_index.py (the section-8 sub-component + tests).
  • pqc-fork/results/kat-results-fri-query-index.json (machine-readable test result).
  • pqc-fork/pq-stark/fri_verify_reference.py, fri_verify_reference.mjs, FriVerifySelfTest.java, test_fri_verify.py (the section-5 FRI fold + opening verify_query sub-component + tests; conformance to Plonky3 p3-fri CONFIRMED via a real KAT, see spec-fri-babybear.md).
  • pqc-fork/pq-stark/challenger_reference.py, challenger_reference.mjs, ChallengerSelfTest.java, test_challenger.py (the section-7 Fiat-Shamir duplex-challenger sub-component + tests; conformance to Plonky3 p3-challenger / p3-fri CONFIRMED via a real KAT, and the FRI betas/indices loop closed).
  • pqc-fork/pq-stark/challenger-extractor/ (Cargo.toml + Cargo.lock + src/main.rs: the Rust ground-truth extractor depending on the pinned p3-challenger / p3-fri 0.4.3-succinct crates) and pqc-fork/pq-stark/challenger_ground_truth.json (its authoritative output: the scripted transcript outputs + the FRI transcript closure with pow_witness, reproduced by the references).
  • pqc-fork/results/kat-results-challenger.json (machine-readable challenger test result).
  • pqc-fork/pq-stark/fri-extractor/ (Cargo.toml + Cargo.lock + src/main.rs: the Rust ground-truth extractor depending on the pinned p3-fri 0.4.3-succinct crates) and pqc-fork/pq-stark/fri_ground_truth.json (its authoritative output: real FRI proofs re-verified by the references).
  • pqc-fork/results/kat-results-fri-verify.json (machine-readable FRI verify test result).
  • pqc-fork/pq-stark/air_quotient_reference.py, air_quotient_reference.mjs, AirQuotientSelfTest.java, test_air_quotient.py (the section-6.1 GENERIC AIR quotient-consistency sub-component + tests; conformance to Plonky3 p3-uni-stark CONFIRMED via a real KAT on the Fibonacci + degree-3 mul example AIRs).
  • pqc-fork/pq-stark/airquotient-extractor/ (Cargo.toml + Cargo.lock + src/main.rs: the Rust ground-truth extractor depending on the pinned p3-uni-stark / p3-air / p3-baby-bear / p3-commit 0.4.3-succinct crates) and pqc-fork/pq-stark/air_quotient_ground_truth.json (its authoritative output: real p3-uni-stark proofs of the two example AIRs, with the openings + alpha + zeta the generic identity re-checks).
  • pqc-fork/results/kat-results-air-quotient.json (machine-readable AIR quotient-consistency test result).
  • docs/PQ-STARK-VERIFIER-PRECOMPILE-2026-07-18.md, docs/PQ-STARK-VERIFIER-ACTIVATION-2026-07-18.md (design + activation), pqc-fork/pq-stark/export-inner-stark-vector.md (real-vector export).