# 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
`observe`s (overwrite-mode absorb) the vkey digest, public values, and every commitment in a FIXED order,
and `sample`s 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.