aere-research/pq-stark

pqc-fork/pq-stark - PQ STARK-verify precompile 0x0AE8 (BabyBear/Plonky3 FRI/STARK verify skeleton)

SCOPE CAVEAT (research finding, 2026-07-19; read before anything else). The generic components in this directory are real and conformance-confirmed, but they were confirmed against Plonky3 0.4.3-succinct, i.e. BabyBear + FRI STARKs, which is Aere's OWN zk-circuits/* proof stack, NOT 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 digest), NOT a BabyBear FRI ShardProof. FRI and the DEEP-ALI quotient check, the two largest confirmed pieces, do NOT apply to SP1 6.1.0 at all. So this is a real BabyBear+FRI verifier skeleton for Aere's own Plonky3 STARKs; it does NOT verify SP1 6.1.0 proofs, and completing the "SP1 recursion AIR" piece would NOT change that. Replacing the SP1 BN254 Groth16 wrap on real SP1 proofs is a SEPARATE ~22 to 32 person-week retarget and a founder decision, specified in ../../docs/AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md. Read the "SP1 inner STARK" wording below as "a BabyBear + FRI STARK (Aere's own Plonky3 circuits)" except where that retarget is cited.

A native post-quantum proof-verification precompile skeleton for the Aere Besu PQC fork that verifies a BabyBear/Plonky3 inner hash-based FRI/STARK (ShardProof<BabyBearPoseidon2>) directly, with NO BN254 Groth16 wrap. BN254 pairings are Shor-breakable; a BabyBear FRI/STARK rests only on hash collision-resistance + Reed-Solomon proximity gaps, so verifying such a proof directly needs no pairing. Per the scope caveat above, this BabyBear+FRI target is Aere's OWN Plonky3 circuits, NOT SP1 6.1.0 (which is Hypercube/KoalaBear-multilinear), so this does not remove the quantum-vulnerable link from an SP1 6.1.0 proof chain. Next free precompile address after Falcon-HashToPoint 0x0AE7.

HONEST STATUS (read this first)

REFERENCE SKELETON + DESIGN. NOT AUDITED. NOT A WORKING VERIFIER. NOT ACTIVATED anywhere.

• What is REAL and testable: BabyBear field arithmetic AND its degree-4 extension F_{p^4} (now COMPLETE: add/sub/neg/mul/inv/Frobenius, generator + two-adic generator, W pinned to a proven-irreducible non-residue; see section (a) below), the full wire-format parser/validator, the gas model, the verifier control flow, the fail-closed contract, and the complete ISP1Verifier Solidity adapter with a one-line consumer swap.
• What is DELEGATED or GATED (deliberately not trusted; TODO(port) / [VERIFY] with cited source): the Poseidon2-BabyBear permutation is now CONFIRMED conformant (see below, Poseidon2Bb.available = true), the MMCS / FieldMerkleTreeMmcs vector commitment is now CONFIRMED conformant (see below, Mmcs.available = true), and the FRI FOLD + OPENING relation / low-degree test (Fri.verifyQuery, Fri.foldRelationConfirmed = true) is now CONFIRMED conformant to the pinned p3-fri (see below). The duplex-sponge Fiat-Shamir challenger (Challenger.spongePorted = true, component (f)) that BINDS the transcript (derives the FRI betas / query indices / grinding) is now ALSO CONFIRMED conformant to the pinned p3-challenger / p3-fri (see section (f) below), and its derived betas/indices close the loop into the confirmed Fri.verifyQuery. And the GENERIC AIR constraint / quotient-consistency MECHANISM (component (e)'s generic DEEP-ALI identity, StarkConstraints.checkGenericQuotient, StarkConstraints.GENERIC_QUOTIENT_CHECK_CONFIRMED = true) is now CONFIRMED conformant to the pinned p3-uni-stark (see section (e) below). The remaining un-ported crypto-core piece is the SP1-recursion-SPECIFIC AIR (its exact constraint set + interactions + public-value layout) and the vkey digest that binds it (part of component (e)). Port target: SP1 sp1-stark / Plonky3 p3-uni-stark (or a pinned native wrap - recommended, spec section 5.1).
• Because the SP1-recursion-SPECIFIC AIR + vkey binding are un-ported, the precompile fail-closes for real SP1 proofs: it returns EMPTY ("not verified") for every input and CANNOT emit a false accept. With StarkConstraints.SP1_RECURSION_AIR_PORTED = false, StarkConstraints.evaluateAtZeta returns UNAVAILABLE at the constraint stage, which the driver checks BEFORE the query loop and BEFORE the single return ACCEPT, so ACCEPT is unreachable by construction. The Solidity adapter therefore reverts on every proof today. That is the safe direction. Nothing here verifies a real STARK proof yet, and nothing here is claimed to. The GENERIC (e) quotient mechanism being confirmed does NOT change this: it is exercised only for a SUPPLIED example AIR under the KAT, WireReader does not parse the proof body, and the SP1-recursion-specific AIR gates ACCEPT, so Fri.checkQuery stays gated (UNAVAILABLE) and the top level returns EMPTY. (A runtime check drives the real precompile: the generic check accepts the ground truth + rejects tampers, evaluateAtZeta returns UNAVAILABLE, and computePrecompile on a well-formed AS1 wire input returns EMPTY.)
• NEW (2026-07-19): the BabyBear field F_p AND its degree-4 extension F_{p^4} (component (a), the FOUNDATION) are COMPLETE and unit-tested (BabyBear / BabyBearExt4); the Poseidon2 permutation over BabyBear width 16 (component (b), the hash) is now CONFIRMED-CONFORMANT to the pinned Plonky3 (p3-baby-bear / p3-poseidon2 0.4.3-succinct) via a real known-answer test that PASSES (Poseidon2Bb in the precompile, plus Python/Node/standalone-Java references); the MMCS / FieldMerkleTreeMmcs vector commitment (component (c)) is now CONFIRMED-CONFORMANT to the pinned Plonky3 (p3-merkle-tree / p3-symmetric / p3-commit 0.4.3-succinct) via a real known-answer test that PASSES (Mmcs in the precompile, plus Python/Node/standalone-Java references); the FRI query-index derivation (one constant-free slice of component (d)) is REAL and unit-tested (FriQueryIndex); and the FRI FOLD + OPENING relation / low-degree test (Fri.verifyQuery, the rest of component (d)) is now CONFIRMED-CONFORMANT to the pinned Plonky3 p3-fri 0.4.3-succinct via a real known-answer test that PASSES (real FRI proofs from the p3-fri prover are re-verified byte-for-byte, accept-genuine + reject-tampered; Fri.verifyQuery in the precompile plus Python/Node/standalone-Java references); and the Fiat-Shamir duplex-sponge challenger (component (f)) is now CONFIRMED-CONFORMANT to the pinned Plonky3 p3-challenger / p3-fri 0.4.3-succinct via a real known-answer test that PASSES (a scripted transcript reproduced byte-for-byte AND the derived FRI betas/indices close the loop into the confirmed Fri.verifyQuery; Challenger.spongePorted = true in the precompile plus Python/Node/standalone-Java references); and the GENERIC AIR constraint / quotient-consistency MECHANISM (component (e)'s DEEP-ALI identity) is now CONFIRMED-CONFORMANT to the pinned Plonky3 p3-uni-stark 0.4.3-succinct via a real known-answer test that PASSES (real p3-uni-stark proofs of two KNOWN example AIRs, the Fibonacci AIR from tests/fib_air.rs and a degree-3 multiply AIR matching tests/mul_air.rs, are re-checked by the generic quotient identity, accept-genuine + reject-tampered-opening/quotient/alpha; StarkConstraints.checkGenericQuotient in the precompile plus Python/Node/standalone-Java references). NONE of these changes the fail-closed behavior: the field is arithmetic behind the un-ported core, deriving indices is only bookkeeping, and Poseidon2 / MMCS / the FRI fold+opening / the challenger / the GENERIC AIR quotient mechanism being confirmed does NOT port the SP1-recursion-SPECIFIC AIR + vkey binding (part of component (e); with StarkConstraints.SP1_RECURSION_AIR_PORTED = false, StarkConstraints.evaluateAtZeta = UNAVAILABLE on the real path), so the top level still returns EMPTY for every real SP1 proof. See sections (a), (b), (c), (d), (e), (f), and 8 below and ../../docs/AERE-STARK-VERIFIER-PORT-SPEC.md.
• Mainnet chain 2800 has exactly the FIVE PQC precompiles 0x0AE1..0x0AE5. 0x0AE8 is not on any Aere network. Consensus stays classical secp256k1 ECDSA QBFT - this is an EVM-layer precompile only.

Layout

file	what
../precompiles/Sp1StarkVerifierPrecompiledContract.java	the reference-skeleton fork precompile at 0x0AE8
besu-pqc-precompile-sp1stark.patch	Address constant (AERE_SP1_STARK_VERIFY = 0x0AE8) + populateForFutureEIPs registration
Sp1StarkVerifierKat.java	KAT/conformance scaffold: real field/parser/fail-closed checks; real-vector ACCEPT KATs marked PENDING (not faked)
export-inner-stark-vector.md	how to export a real SP1 v6.1.0 inner STARK vector on a throwaway prover box
babybear_field_reference.py / .mjs	independent Python + Node references for the BabyBear field F_p + extension F_{p^4} (component (a))
BabyBearFieldSelfTest.java	standalone (no-Besu-classpath) copy of the BabyBear / BabyBearExt4 field logic, self-tested
test_babybear_field.py	harness: field axioms + Fermat-vs-bignum inverse + generator/W proofs + cross-language (Python/Node/Java) agreement
../results/kat-results-babybear-field.json	machine-readable result of the BabyBear field KAT
poseidon2_babybear_reference.py / .mjs	independent Python + Node references for the Poseidon2-BabyBear width-16 permutation (component (b))
Poseidon2BabyBearSelfTest.java	standalone (no-Besu-classpath) copy of the Poseidon2Bb permutation logic, self-tested
test_poseidon2_babybear.py	harness: S-box/MDS/bijection self-consistency + cross-language agreement + CONFORMANCE (real KAT vs pinned crates)
../results/kat-results-poseidon2-babybear.json	machine-readable result of the Poseidon2-BabyBear KAT
spec-poseidon2-constants.md	Poseidon2-BabyBear constants provenance + conformance KAT (pinned p3-baby-bear / p3-poseidon2 0.4.3-succinct)
mmcs_babybear_reference.py / .mjs	independent Python + Node references for the MMCS / FieldMerkleTreeMmcs vector commitment (component (c))
MmcsBabyBearSelfTest.java	standalone (no-Besu-classpath) copy of the Mmcs build/open/verify logic, self-tested
test_mmcs_babybear.py	harness: open-every-leaf self-consistency + tamper-reject + cross-language agreement + CONFORMANCE (real KAT vs pinned crates)
../results/kat-results-mmcs-babybear.json	machine-readable result of the MMCS-BabyBear KAT
spec-mmcs-babybear.md	MMCS construction provenance + conformance KAT (pinned p3-merkle-tree / p3-symmetric / p3-commit 0.4.3-succinct)
fri_query_index_reference.py / .mjs	independent Python + Node references for the FRI query-index derivation (section 8)
FriQueryIndexSelfTest.java	standalone (no-Besu-classpath) copy of the FriQueryIndex helper logic, self-tested
test_fri_query_index.py	harness: goldens + invariants + alt-impl + cross-language (Python/Node/Java) agreement
../results/kat-results-fri-query-index.json	machine-readable result of the FRI query-index KAT
fri_verify_reference.py / .mjs	independent Python + Node references for the FRI fold + opening verify_query (component (d))
FriVerifySelfTest.java	standalone (no-Besu-classpath) FRI verifier reference, self-tested; --emit for cross-language
test_fri_verify.py	harness: CONFORMANCE (accept real p3-fri proof + reject tampered) + Python/Node/Java agreement
fri-extractor/	Rust ground-truth extractor (Cargo.toml + Cargo.lock + src/main.rs) depending on the pinned p3-fri 0.4.3-succinct
fri_ground_truth.json	the extractor's authoritative output: real FRI proofs (roots, betas, indices, openings, final poly)
../results/kat-results-fri-verify.json	machine-readable result of the FRI verify KAT
spec-fri-babybear.md	FRI config + fold/opening relation provenance + conformance KAT (pinned p3-fri / p3-challenger / p3-dft 0.4.3-succinct)
air_quotient_reference.py / .mjs	independent Python + Node references for the GENERIC AIR quotient-consistency check (component (e))
AirQuotientSelfTest.java	standalone (no-Besu-classpath) generic AIR quotient-consistency reference, self-tested; --emit for cross-language
test_air_quotient.py	harness: CONFORMANCE (accept real p3-uni-stark proof of example AIRs + reject tampered) + Python/Node/Java agreement
airquotient-extractor/	Rust ground-truth extractor (Cargo.toml + Cargo.lock + src/main.rs) depending on the pinned p3-uni-stark / p3-air / p3-baby-bear / p3-commit 0.4.3-succinct
air_quotient_ground_truth.json	the extractor's authoritative output: real p3-uni-stark proofs of the Fibonacci + degree-3 mul AIRs (openings, alpha, zeta)
../results/kat-results-air-quotient.json	machine-readable result of the AIR quotient-consistency KAT
challenger_reference.py / .mjs	independent Python + Node references for the Fiat-Shamir duplex challenger (component (f))
ChallengerSelfTest.java	standalone (no-Besu-classpath) copy of the Challenger duplex-sponge logic, self-tested; --emit for cross-language; includes the driver fail-closed gate model
test_challenger.py	harness: CONFORMANCE (scripted transcript + grinding table) + FRI betas/indices loop closure into verify_query + Python/Node/Java agreement
challenger-extractor/	Rust ground-truth extractor (Cargo.toml + Cargo.lock + src/main.rs) depending on the pinned p3-challenger / p3-fri 0.4.3-succinct
challenger_ground_truth.json	the extractor's authoritative output: the scripted transcript outputs + the FRI transcript closure (with pow_witness)
../results/kat-results-challenger.json	machine-readable result of the challenger KAT
../../docs/AERE-STARK-VERIFIER-PORT-SPEC.md	component-by-component port plan + the section-8 sub-component
../../contracts/contracts/zkverify/AerePQStarkVerifier.sol	ISP1Verifier-compatible adapter -> 0x0AE8 (one-line swap for existing consumers)
../../contracts/test/AerePQStarkVerifier.test.js	fail-closed + one-line-swap-into-AereEVMValidityV2 tests
../../docs/PQ-STARK-VERIFIER-PRECOMPILE-2026-07-18.md	design/spec: encoding, the exact SP1/Plonky3 STARK, soundness (EF soundcalc / FRI proximity-gap regime), gas, why direct-verify beats the BN254 wrap
../../docs/PQ-STARK-VERIFIER-ACTIVATION-2026-07-18.md	gated activation plan (P0 make-it-real prerequisite + external audit + founder GO, non-retroactive milestone)

Reproduce (what actually runs today)

# Solidity adapter: compiles + fail-closed / one-line-swap tests pass (precompile absent on test EVM).
cd ../../contracts && npx hardhat test test/AerePQStarkVerifier.test.js

# KAT scaffold: BabyBear field identities + wire parser + fail-closed contract (real).
#   Real SP1-vector ACCEPT KATs print PENDING and are skipped, never faked.
javac -cp <besu-evm-jars> ../precompiles/Sp1StarkVerifierPrecompiledContract.java Sp1StarkVerifierKat.java
java  -cp .:<besu-evm-jars> Sp1StarkVerifierKat

# BabyBear field + F_{p^4} KAT (component (a)): axioms + Fermat-vs-bignum inverse + generator/W
#   proofs + Python/Node/Java agreement. Needs python3 + node + javac on PATH; no Besu classpath.
python test_babybear_field.py

# FRI query-index derivation KAT (section 8): goldens + invariants + Python/Node/Java agreement.
#   Needs python3 + node + javac on PATH; runs standalone, no Besu classpath.
python test_fri_query_index.py

# Poseidon2-BabyBear (width 16) KAT (component (b)): x^7 bijection + M4-MDS + invertible layers +
#   permutation inverse round-trip + Python/Node/Java agreement + CONFORMANCE (reproduces real
#   known-answer vectors from the pinned p3-baby-bear / p3-poseidon2 0.4.3-succinct crates).
python test_poseidon2_babybear.py

# MMCS / FieldMerkleTreeMmcs KAT (component (c)): open-every-leaf self-consistency + tamper-reject +
#   Python/Node/Java agreement + CONFORMANCE (reproduces real roots/openings/proofs from the pinned
#   p3-merkle-tree / p3-symmetric / p3-commit 0.4.3-succinct crates). Needs python3 + node + javac.
python test_mmcs_babybear.py

# FRI verifier (fold + opening) KAT (component (d)): re-verify real FRI proofs emitted by the pinned
#   p3-fri 0.4.3-succinct prover (accept genuine + reject tampered opening/fold/final-poly) +
#   Python/Node/Java byte-identical folded values. Needs python3 + node + javac (uses fri_ground_truth.json).
python test_fri_verify.py

# GENERIC AIR quotient-consistency KAT (component (e), generic mechanism): re-check the DEEP-ALI identity
#   folded_constraints(zeta) == Z_H(zeta)*quotient(zeta) for real p3-uni-stark 0.4.3-succinct proofs of two
#   known example AIRs (Fibonacci + degree-3 mul; accept genuine + reject tampered trace/quotient/alpha) +
#   Python/Node/Java byte-identical quotient + folded. Needs python3 + node + javac (uses air_quotient_ground_truth.json).
python test_air_quotient.py

# (optional) regenerate the ground truth from the pinned crates (needs cargo; compile in a scratch dir):
#   cd fri-extractor && cargo run --release > ../fri_ground_truth.json
#   cd airquotient-extractor && cargo run --release > ../air_quotient_ground_truth.json

(a) BabyBear field F_p + degree-4 extension F_{p^4} (the FOUNDATION, implemented + tested)

Component (a) of the six-component port (spec section 2): the field everything else is built on.

• BabyBear: F_p with p = 2^31 - 2^27 + 1 = 2013265921. add, sub, neg, mul, pow, inv (Fermat a^(p-2)), the multiplicative generator (GENERATOR = 31), and the two-adic generator of the order-2^27 subgroup (twoAdicGenerator(bits)).
• BabyBearExt4: the degree-4 binomial extension F_p[x]/(x^4 - W) with W PINNED to 11. add, sub, neg, mul (schoolbook convolution reduced by x^4 = W), inv (Fermat a^(p^4-2)), Frobenius (a^p), and the base embedding.

REAL test result (ran 2026-07-19, python test_babybear_field.py): PASS=396242 FAIL=0, with Python + Node + Java producing byte-identical results on the shared vector set. The standalone Java self-test (java BabyBearFieldSelfTest) is PASS=360018 FAIL=0. Recorded in ../results/kat-results-babybear-field.json.

What is PROVEN offline (no external fetch): the F_p and F_{p^4} field axioms; the Fermat inverse equals an INDEPENDENT extended-Euclid bignum inverse (Python pow(a,-1,p)); GENERATOR = 31 has order exactly p-1 (via p-1 = 2^27 * 3 * 5); the two-adic generator has order exactly 2^27; and W = 11 is a quadratic non-residue with 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. Frobenius^4 = identity and the base field is fixed.

What this does NOT prove: that GENERATOR = 31, W = 11, and twoAdicGenerator(27) = 440564289 are Plonky3 p3-baby-bear's EXACT chosen constants. The field being real (generator-of-full-order, irreducible extension) is necessary but not sufficient: a wrong-but-irreducible W builds a valid field that silently disagrees with the prover. That conformance is [VERIFY]/[MEASURE] against the pinned SP1 v6.1.0 Plonky3 revision. Completing the field does NOT make the precompile verify anything: it sits behind the un-ported Poseidon2 / FRI / AIR core, so the top-level 0x0AE8 stays fail-closed (returns EMPTY for every input).

(b) Poseidon2 over BabyBear, width 16 (the hash: CONFIRMED-conformant, real KAT PASSES)

Component (b) of the six-component port (spec section 3): the algebraic permutation Plonky3/SP1 uses BOTH as the Merkle/MMCS compression and as the Fiat-Shamir duplex challenger. The permutation is implemented (Poseidon2Bb in the precompile, plus poseidon2_babybear_reference.{py,mjs} and Poseidon2BabyBearSelfTest.java) and its constants + structure are CONFIRMED against the pinned Plonky3 (see below):

• x^7 S-box (BabyBear: 7 is the smallest d>1 with gcd(d, p-1)=1, so it is a bijection on F_p);
• 8 external (full) rounds (4 initial + 4 terminal), S-box on all 16 lanes, then the MDS-light external layer M_E built from M4 = 2,3,1,1],[1,2,3,1],[1,1,2,3],[3,1,1,2 (diagonal blocks 2*M4, off-diagonal blocks M4). CONFIRMED: the full 16x16 external matrix recovered from Plonky3's Poseidon2ExternalMatrixGeneral equals this block form;
• 13 internal (partial) rounds, S-box on lane 0 only, then the internal layer M_I = R^{-1} * (J + diag(D)) applied as state[i] = R_INV * (sum + D[i]*state[i]), with R_INV = 943718400 = (2^32)^{-1} mod p. The R^{-1} factor is the Montgomery-form artifact of p3-baby-bear's DiffusionMatrixBabyBear (recovered exactly from its 16x16 canonical matrix);
• the 141 CONFIRMED round constants (128 external + 13 internal) from Xoroshiro128Plus::seed_from_u64(1) via new_from_rng_128, plus a compress2to1 truncated-permutation 2-to-1 compression for the Merkle layer.

REAL test result (ran 2026-07-19, python test_poseidon2_babybear.py): PASS=47017 FAIL=0, with Python + Node + Java producing byte-identical permutation outputs on a shared input set AND all three reproducing the pinned-library known-answer vectors. The standalone Java self-test (java Poseidon2BabyBearSelfTest) is PASS=13536 FAIL=0. Recorded in ../results/kat-results-poseidon2-babybear.json.

CONFORMANCE is CONFIRMED (real KAT PASSED). The pinned crates p3-baby-bear / p3-poseidon2 0.4.3-succinct (checksums d69e6e9a... / 52298637..., byte-identical to the repo Cargo.lock) were executed via cargo to emit the constants and three permutation known-answer vectors (all-zeros, [0,1,...,15], and the width-16 test vector). This reference reproduces all three EXACTLY. This closes the "two wrong copies agree" trap the spec warns about: in particular the internal layer's R^{-1} Montgomery factor was NOT in a prior pass (it used the textbook state[i]*D[i] + sum, which is self-consistent but silently disagrees with the prover) and is now fixed. Source URLs, commit/version, and the vectors are recorded in spec-poseidon2-constants.md.

What is also PROVEN offline (self-consistency): x^7 is a bijection (7 CONFIRMED as the minimal coprime degree; monomial inverse round-trips; S-box equals an independent pow(x,7,p)); the permutation is deterministic and a genuine bijection (explicit inverse round-trips, 0 collisions on the sample); M4 is MDS; the external and internal linear layers equal their explicit 16x16 matrices and both are invertible over F_p; three independent implementations agree byte-for-byte.

Because the permutation is confirmed, Poseidon2Bb.available is now true. This does NOT make the precompile verify anything: the SP1 recursion-AIR (component (e)) is un-ported (StarkConstraints returns UNAVAILABLE; the challenger (f), MMCS (c), and FRI fold+opening (d) are all now confirmed), so the top-level 0x0AE8 stays fail-closed (EMPTY) for every input.

(c) MMCS / FieldMerkleTreeMmcs vector commitment (CONFIRMED-conformant, real KAT PASSES)

Component (c) of the six-component port (spec section 4): the Merkle-tree vector commitment (the "mixed matrix commitment scheme") that FRI (d) and the trace commitment are built on. It is implemented (Mmcs in the precompile, plus mmcs_babybear_reference.{py,mjs} and MmcsBabyBearSelfTest.java) 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);
• mixed-height tree build (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), and the verify_batch that recomputes the root from opened rows + a sibling path.

REAL test result (ran 2026-07-19, python test_mmcs_babybear.py): PASS=300 FAIL=0, with Python + Node + Java producing byte-identical roots/openings/proofs AND all three reproducing the pinned-library known-answer vectors. The standalone Java self-test (java MmcsBabyBearSelfTest) is PASS=80 FAIL=0 (includes open-every-leaf). Recorded in ../results/kat-results-mmcs-babybear.json.

CONFORMANCE is CONFIRMED (real KAT PASSED). The pinned crates p3-merkle-tree / p3-symmetric / p3-commit / p3-matrix 0.4.3-succinct (checksums d5703d92... / 9047ce85... / 50acacc7... / 75c3f150..., byte-identical to the repo Cargo.lock) were executed via cargo to commit to six known matrix batches (single power-of-two height, single non-power-of-two height with zero-digest padding, a column vector, and three mixed-height batches including one whose proof contains a default zero-digest sibling) and emit the root plus an open_batch opening for each. This reference reproduces every root, opening, and proof EXACTLY and its verify_batch accepts the emitted openings and rejects tampered ones. The extractor's permute([0;16]) equals the confirmed Poseidon2 "zeros" vector, proving it uses the same confirmed permutation. Source URLs + vectors are in spec-mmcs-babybear.md.

Because the MMCS is confirmed, Mmcs.available is now true. This does NOT make the precompile verify anything: the SP1 recursion-AIR (component (e), StarkConstraints returns UNAVAILABLE) is un-ported (the challenger (f) and the FRI fold+opening (d) are now confirmed), so the top-level 0x0AE8 stays fail-closed (EMPTY) for every input. Conformance against a REAL exported SP1 v6.1.0 commitment root is a further [MEASURE] step (needs an exported proof).

(d) FRI verifier: fold + opening / low-degree test (CONFIRMED-conformant, real KAT PASSES)

Component (d) of the six-component port (spec section 5): the FRI low-degree test at the heart of the STARK. The per-query FOLD + OPENING relation verify_query is implemented (Fri.verifyQuery in the precompile, plus fri_verify_reference.{py,mjs} and FriVerifySelfTest.java) and CONFIRMED against the pinned Plonky3 p3-fri 0.4.3-succinct. For each query it:

• walks the arity-2 folding (index_sibling = index ^ 1, index_pair = index >> 1) for num_fold_rounds = log_max_height - log_blowup layers;
• at each layer checks the commit-phase MMCS opening of the sibling pair against that layer's root. 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.verifyBatch (component (c));
• interpolates the pair through the folding challenge beta at the coset point x = two_adic_generator(log_max_height)^reverse_bits_len(index) (the sibling point is -x), in F_{p^4} (component (a)), folding down to a single constant;
• verify_challenges accepts iff that constant equals the committed final_poly for EVERY query.

REAL test result (ran 2026-07-19, python test_fri_verify.py): PASS=55 FAIL=0, with Python + Node + Java producing byte-identical per-query folded values AND all re-verifying the real proof. The standalone Java self-test (java FriVerifySelfTest fri_ground_truth.json) is PASS=44 FAIL=0, and the precompile's OWN Sp1StarkVerifierPrecompiledContract.Fri.verifyQuery reproduces accept + reject for all three cases (15/15). Recorded in ../results/kat-results-fri-verify.json.

CONFORMANCE is CONFIRMED (real KAT PASSED). The pinned p3-fri / p3-challenger / p3-dft 0.4.3-succinct crates (checksums 5cbc4965... / b6a90892... / be6408b1..., byte-identical to the repo Cargo.lock) were executed via cargo (the extractor fri-extractor/) to build genuinely low-degree codewords, run the p3-fri PROVER to emit real FRI proofs (with the confirmed seed_from_u64(1) Poseidon2), and confirm the p3-fri VERIFIER accepts them; its output is fri_ground_truth.json. This reference reproduces the ACCEPT byte-for-byte and REJECTS four tamper variants: a corrupted opened value, a corrupted MMCS sibling digest, a wrong fold challenge beta (wrong fold), and a non-matching final polynomial. Source URLs + the config trace are in spec-fri-babybear.md.

CONFIRMED items (all previously [VERIFY], now closed by the real KAT): arity-2 fold; num_fold_rounds = log_max_height - log_blowup with a single-constant final poly; the reverse_bits_len index-to-coset mapping; that two_adic_generator(bits) matches Plonky3 (the coset points come out right); and that the F_{p^4} non-residue W = 11 is Plonky3's (the EF fold reproduces the interpolation).

Because the fold+opening is confirmed, Fri.foldRelationConfirmed is now true. This does NOT make the precompile verify anything. The betas / query indices that this fold+opening consumes are now DERIVED in-circuit by the confirmed duplex-sponge challenger (Challenger.spongePorted = true, component (f), see section (f) below), and that closed loop (transcript -> betas/indices -> Fri.verifyQuery) is KAT-proven in test_challenger.py. But the SP1 recursion-AIR (StarkConstraints.evaluateAtZeta UNAVAILABLE, component (e)) that supplies the reduced openings is still un-ported, and WireReader does not parse the proof body, so Fri.checkQuery stays gated (UNAVAILABLE) and the top-level 0x0AE8 stays fail-closed (EMPTY) for every input. Conformance against a REAL exported SP1 v6.1.0 inner proof's FRI section is a further [MEASURE] step (needs the exported proof + component (e)).

(e) GENERIC AIR constraint / quotient-consistency check (CONFIRMED-conformant, real KAT PASSES)

Component (e) of the six-component port (spec section 6): the STARK proper, the DEEP-ALI quotient consistency check. It SPLITS into a GENERIC mechanism (AIR-agnostic, now confirmed) and the SP1-recursion-SPECIFIC AIR + vkey binding (un-ported, the fail-closed gate).

The GENERIC quotient-consistency MECHANISM is implemented (StarkConstraints.checkGenericQuotient in the precompile, plus air_quotient_reference.{py,mjs} and AirQuotientSelfTest.java), traced verbatim from the pinned Plonky3 p3-uni-stark 0.4.3-succinct verifier.rs (lines 90-141), p3-commit domain.rs (the TwoAdicMultiplicativeCoset selectors / zp_at_point / split_domains), and p3-air folder.rs/air.rs (the VerifierConstraintFolder Horner fold + the when_first_row/when_transition/ when_last_row selector filters). Given the out-of-domain trace openings at zeta (trace_local) and at g*zeta (trace_next), a random challenge alpha, the quotient-chunk openings, and the trace-domain degree, it:

• folds the AIR's constraints with alpha into a single value (acc = acc*alpha + constraint, in the AIR eval() order);
• reconstructs quotient(zeta) from the chunk openings and the split-domain normalization zps[i] = prod_{j!=i} zp_j(zeta) * zp_j(chunk_i.first_point())^-1, via quotient = sum_i zps[i] * sum_e monomial(e) * chunk[i][e];
• computes the vanishing polynomial Z_H(zeta) = zeta^(2^degree_bits) - 1 and the first/last/transition selectors + inv_zeroifier = Z_H(zeta)^-1;
• checks the identity folded_constraints(zeta) == Z_H(zeta) * quotient(zeta) (OodEvaluationMismatch otherwise), all over F_{p^4}.

REAL test result (ran 2026-07-19, python test_air_quotient.py): PASS=18 FAIL=0, with Python + Node + Java producing byte-identical reconstructed quotient(zeta) and folded_constraints(zeta). Recorded in ../results/kat-results-air-quotient.json.

CONFORMANCE is CONFIRMED (real KAT PASSED). The pinned p3-uni-stark / p3-air / p3-baby-bear / p3-commit 0.4.3-succinct crates (checksums fc3dfdeb... / d3a5de20... / d69e6e9a... / 50acacc7..., the last two byte-identical to the Poseidon2/MMCS components) were executed via cargo (the extractor 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]), ONE quotient chunk;
• mul_deg3_n16: a degree-3 multiply AIR matching tests/mul_air.rs (columns [a,b,c]; a^2*b - c plus boundary b = a^2 + 1 and transition next_a = a + 1; n = 16), TWO quotient chunks (exercising the split-domain zps product).

The generic reference reproduces the library ACCEPT on both and REJECTS three tamper variants per case (a corrupted trace opening, a wrong quotient chunk, a wrong alpha). 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. Source + vectors are in air_quotient_ground_truth.json.

Because the generic mechanism is confirmed, StarkConstraints.GENERIC_QUOTIENT_CHECK_CONFIRMED is now true. This does NOT make the precompile verify a real SP1 proof. The generic mechanism working on a small example AIR does NOT port the SP1 recursion machine AIR (its exact multi-thousand-constraint set, interactions/permutation argument, public-value layout) or the vkey digest that binds it: that is a large, program-specific, multi-week piece needing the SP1 toolchain (spec section 6.2). With StarkConstraints.SP1_RECURSION_AIR_PORTED = false, StarkConstraints.evaluateAtZeta (the real path) returns UNAVAILABLE at stage 4 (before the query loop and before the single return ACCEPT), so the top-level 0x0AE8 stays fail-closed (EMPTY) for every real SP1 proof and ACCEPT is unreachable. A runtime check (PrecompileAirCheck) drives the real precompile classes and confirms: the generic check accepts the ground truth + rejects tampers, evaluateAtZeta(null,null) == UNAVAILABLE, and computePrecompile on a well-formed AS1 wire input returns EMPTY. The SP1-recursion-SPECIFIC AIR + vkey + a real end-to-end SP1-proof KAT remain [MEASURE] (need the SP1 toolchain and an exported proof).

(f) Fiat-Shamir transcript / Poseidon2 duplex challenger (CONFIRMED-conformant, real KAT PASSES)

The non-interactive transcript that BINDS the whole proof: the DuplexChallenger<BabyBear, Perm, WIDTH=16, RATE=8> plus the GrindingChallenger check_witness, over the confirmed Poseidon2 sponge. It observes (overwrite-mode absorb) the vkey digest, public values, and every commitment in a FIXED order, and samples the verifier randomness (the FRI folding challenges betas, the query indices, the grinding witness). It is IMPLEMENTED as Challenger in the precompile (Challenger.spongePorted = true) and independently in Python, Node, and standalone Java, traced verbatim from the pinned p3-challenger 0.4.3-succinct duplex_challenger.rs / grinding_challenger.rs, with the observe/sample ORDER from p3-fri verify_shape_and_sample_challenges.

Confirmed behaviour (from source): observe clears the output buffer, pushes to the input buffer, and duplexes when it reaches RATE=8; duplexing overwrites the first len lanes, permutes, and squeezes lanes [0..8); sample duplexes if inputs are buffered or outputs exhausted then pop()s from the END of the buffer (Vec::pop, LIFO); an F_{p^4} sample is 4 sequential base pops [c0,c1,c2,c3]; sample_bits masks the LOW bits of as_canonical_u64; check_witness = observe(witness) then sample_bits(bits) == 0.

REAL test result (ran 2026-07-19, python test_challenger.py): PASS=44 FAIL=0, with Python + Node + standalone Java byte-identical. The standalone Java self-test (java ChallengerSelfTest) is PASS=31 FAIL=0 (includes a driver control-flow gate model showing ACCEPT is unreachable). The pinned p3-challenger / p3-fri 0.4.3-succinct crates were executed via cargo (challenger-extractor/) to emit ground truth: (1) a fully-scripted observe/sample transcript (base + ext samples, the full 16-lane sponge state, and a check_witness accept/reject table), reproduced byte-for-byte; and (2) the FRI transcript closure for the same three cases as fri_ground_truth.json - the betas + query indices + grinding acceptance are DERIVED from the transcript and match BOTH the pinned p3-fri challenger AND the confirmed FRI ground truth, and fed into the confirmed Fri.verifyQuery they ACCEPT the real FRI proof and REJECT a tampered beta. This closes the loop component (d) left open (transcript -> betas/indices -> FRI verify). Recorded in ../results/kat-results-challenger.json and challenger_ground_truth.json.

This does NOT make the precompile verify anything: the challenger being confirmed is necessary but not sufficient. The SP1 recursion-AIR constraint evaluation (component (e), StarkConstraints.evaluateAtZeta) is un-ported and returns UNAVAILABLE at the constraint stage, which the driver checks BEFORE the query loop and BEFORE the single return ACCEPT, so the top-level 0x0AE8 stays fail-closed (EMPTY) for every input and ACCEPT is unreachable. A real exported SP1 v6.1.0 proof's full transcript order (vkey digest, trace/quotient commitments, DEEP zeta/alpha) is a further [MEASURE] step (part of component (e)).

8. FRI query-index derivation (a sub-component implemented + tested here)

One constant-free slice of FRI component (d), implemented as FriQueryIndex in the precompile and independently in Python, Node, and standalone Java. It does two things a real FRI verifier needs:

• sampleBits(canonicalU32, bits): reduce a Fiat-Shamir challenger sample (a BabyBear element's canonical u32) to a query index in [0, 2^bits) by taking the low bits bits (Plonky3 sample_bits).
• walk(index, logMaxHeight, logFinalPolyLen): the per-layer folding-index walk, giving (index, sibling = index^1, index_pair = index>>1, parity) for each of the logMaxHeight - logFinalPolyLen folding rounds, terminating in the final-poly domain.

Why this one and not Poseidon2: the index logic is fixed by the public Plonky3 spec with NO secret round constants, so it can be validated offline with running, passing tests. Poseidon2 cannot be conformance-tested without the exact Plonky3 constants (testing it only against a same-constants copy would prove self-consistency, not conformance), so it is left as a fully-specified [VERIFY] port target in the port-spec (section 3).

REAL test result (ran 2026-07-19, python test_fri_query_index.py): PASS=100021 FAIL=0, with Python + Node + Java producing byte-identical results on the shared vector set. The standalone Java self-test (java FriQueryIndexSelfTest) is PASS=80018 FAIL=0. Recorded in ../results/kat-results-fri-query-index.json.

What this proves and does NOT: it validates the index LOGIC against the public spec across three independent implementations. It does NOT prove conformance to a real SP1 v6.1.0 trace (the actual sampled indices come out of the Poseidon2 challenger on a real proof). That conformance is [MEASURE]: export a real inner proof (export-inner-stark-vector.md), instrument the Plonky3 p3-fri verifier to print its sampled indices + per-layer walk, and diff against fri_query_index_reference. The top-level 0x0AE8 verifier stays fail-closed throughout.

Flags: [VERIFY] sample_bits masks LOW bits (LSB) vs p3-challenger; [VERIFY] arity-2 fold (sibling = index^1, index_pair = index>>1) vs p3-fri verifier.rs; [VERIFY] logMaxHeight = log_max_degree + log_blowup and the final-poly length for the pinned config; [MEASURE] bit-reversal index-to-domain-point mapping and the end-to-end index conformance vs a real trace.

Next steps to make it real (gated)

1. Port the crypto core (or build the pinned native wrap) - spec section 5.
2. Export a real SP1 v6.1.0 inner vector - export-inner-stark-vector.md.
3. Pin configId FriConfig, run soundcalc, record the true soundness bits - spec section 4.3.
4. Benchmark gas under the EIP-7825 2^24 cap - spec section 6.
5. External audit + isolated soak + founder GO + non-retroactive milestone - activation plan.