aere-docs/AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC.md

AERE STARK verifier: SP1-recursion AIR port specification (precompile 0x0AE8, part 2)

Spec date: 2026-07-19 Status: RESEARCH + PORTING PLAN, not an implementation. This document scopes the ONE remaining crypto-core piece of the native STARK-verify port (the SP1-recursion-specific constraint system and its verifying key) against the REAL, pinned SP1 source. It does NOT port it. The top-level precompile 0x0AE8 stays fail-closed and is not touched by this document.

Companion: docs/AERE-STARK-VERIFIER-PORT-SPEC.md (the six generic components + their confirmed status), docs/PQ-STARK-VERIFIER-PRECOMPILE-2026-07-18.md (design/encoding/gas), docs/PQ-STARK-VERIFIER-ACTIVATION-2026-07-18.md (gated activation).

Citations use the pinned upstream tag v6.1.0 (commit d454975ac7c1126097e36eceda9bce2cb9899da4, github.com/succinctlabs/sp1). [VERIFY] marks a value or convention not read byte-exact from source in this pass. [MEASURE] marks a validation that needs the compiled SP1 toolchain and a real proof.

---

0. Headline finding (read first): the pinned SP1 6.1.0 is Hypercube, not Turbo

This research turned up a correctness finding that changes the scope of the remaining work, so it goes first and plainly.

The generic-component work in the companion spec was implemented and conformance-confirmed against Plonky3 0.4.3-succinct: the BabyBear field, Poseidon2-over-BabyBear, a Merkle/MMCS, the FRI low-degree test, a p3-uni-stark DEEP-ALI quotient check, and a p3-challenger duplex transcript. That is a faithful BabyBear + FRI + univariate-STARK verifier skeleton, and it is real.

It is, however, the WRONG proof system for the version of SP1 that Aere actually pins. SP1 =6.1.0 (pinned in rollup-evm-validity/host/Cargo.toml, rollup-evm-validity/guest/Cargo.toml, batch-prover-recovered/bin/aere-prover/Cargo.toml, all sp1-sdk/sp1-prover/sp1-verifier/sp1-zkvm = "=6.1.0") is an SP1 Hypercube release. Its proving stack is not AIR + FRI. It is a multilinear system: KoalaBear field, a BaseFold + Stacked + Jagged polynomial commitment scheme, a sumcheck-based constraint check (zerocheck), and a LogUp-GKR interaction argument with a degree-7 septic-curve global cumulative digest. There is no BabyBear ShardProof<BabyBearPoseidon2> and no FRI low-degree test anywhere in the SP1 6.1.0 proof that 0x0AE8 would verify.

Evidence, from both upstream source and the repo's own resolved lockfiles:

• Upstream Cargo.toml at tag v6.1.0 (workspace.package.version = "6.1.0") lists workspace members slop/crates/{jagged, whir, basefold, sumcheck, multilinear, stacked, tensor, koala-bear, ...} and sp1-gpu/crates/{jagged_sumcheck, logup_gkr, zerocheck, ...}, and pins Plonky3 at 0.3.2-succinct. Source: https://github.com/succinctlabs/sp1/blob/v6.1.0/Cargo.toml
• crates/primitives/src/lib.rs defines pub type SP1Field = KoalaBear; and pub type SP1ExtensionField = BinomialExtensionField<SP1Field, 4>; with SP1GlobalContext = KoalaBearDegree4Duplex (Poseidon2 width 16, 30 total rounds). Source: https://github.com/succinctlabs/sp1/blob/v6.1.0/crates/primitives/src/lib.rs
• crates/prover/src/recursion.rs builds the compress/shrink/wrap recursion verifiers from RecursiveBasefoldVerifier + RecursiveMerkleTreeTcs + RecursiveStackedPcsVerifier + RecursiveJaggedPcsVerifier over SP1Field. There is no FRI verifier in that path. Source: https://github.com/succinctlabs/sp1/blob/v6.1.0/crates/prover/src/recursion.rs
• The repo's OWN resolved lock rollup-evm-validity/host/Cargo.lock (the crate that pins SP1 =6.1.0) resolves sp1-sdk 6.1.0, sp1-prover 6.1.0, sp1-verifier 6.1.0 on top of sp1-hypercube 6.3.1, sp1-recursion-machine 6.3.1, sp1-recursion-executor 6.3.1, slop-basefold 6.3.1, slop-jagged 6.3.1, slop-multilinear 6.3.1, slop-sumcheck 6.3.1. The SP1 6.1.0 facade crates sit on the 6.3.1 Hypercube internals. The p3-* 0.4.3-succinct entries in the same lock (including p3-koala-bear, p3-fri, p3-uni-stark) are Aere's own separate Plonky3 circuits' dependencies (zk-circuits/*, the recursive-aggregation / zkml / attr provers), not the SP1 recursion proof.

Consequence for scope. The remaining work is not "add the SP1 AIR on top of a finished FRI skeleton." It is "build a KoalaBear multilinear (BaseFold + Jagged + sumcheck + LogUp-GKR) machine verifier and then add the SP1 recursion machine's chips on top." Of the six confirmed generic components, only the SHAPES of three carry over (Poseidon2 sponge, Merkle tree, duplex challenger), and even those need the KoalaBear field and the KoalaBear Poseidon2 constants. The two largest confirmed pieces, the FRI low-degree test and the DEEP-ALI univariate quotient check, are not used by SP1 6.1.0 at all; they are replaced by BaseFold and by sumcheck-zerocheck respectively. This is stated bluntly because it enlarges the honest estimate (section 11) well beyond the companion spec's "3 to 4 person-weeks for the AIR."

Two clean options follow from this finding; both are out of scope to decide here but are named so the founder can choose (section 13): retarget 0x0AE8 to the SP1 6.1.0 Hypercube recursion proof (the plan below), or keep the existing BabyBear + FRI skeleton and point it at Aere's OWN Plonky3 STARKs (the zk-circuits/* provers), which is a real but different capability and does not remove the SP1 BN254 Groth16 wrap.

Nothing in this document changes the fail-closed contract. On-chain ZK verification on Aere stays on the classical BN254 Groth16 gateway (0x9ca479C8c52C0EbB4599319a36a5a017BCC70628) until the whole verifier is real, KAT-green against a real exported SP1 proof, externally audited, and founder-activated.

---

1. Exact pinned version

item	pin	source
SP1 facade crates	sp1-sdk, sp1-prover, sp1-verifier, sp1-zkvm, sp1-build = "=6.1.0"	rollup-evm-validity/{host,guest}/Cargo.toml, batch-prover-recovered/**/Cargo.toml
SP1 upstream tag	v6.1.0, commit d454975ac7c1126097e36eceda9bce2cb9899da4	github.com/succinctlabs/sp1 release v6.1.0
SP1 recursion machine (resolved)	sp1-hypercube 6.3.1, sp1-recursion-machine 6.3.1, sp1-recursion-executor 6.3.1	rollup-evm-validity/host/Cargo.lock
PCS / sumcheck stack (resolved)	slop-basefold 6.3.1, slop-jagged 6.3.1, slop-multilinear 6.3.1, slop-sumcheck 6.3.1	rollup-evm-validity/host/Cargo.lock
rsp executor	git succinctlabs/rsp tag reth-1.9.3-sp1-6.1.0	rollup-evm-validity/host/Cargo.toml
field	SP1Field = KoalaBear (p = 2^31 - 2^24 + 1 = 2130706433 = 0x7F000001), ext degree 4	crates/primitives/src/lib.rs @ v6.1.0
Poseidon2	width 16, 30 total rounds, KoalaBearDegree4Duplex	crates/primitives/src/lib.rs @ v6.1.0

Version-skew note [VERIFY]: the SP1 facade crates carry 6.1.0 while the recursion/PCS internals resolve to 6.3.1. The port must be pinned to the exact sp1-recursion-machine / slop-* 6.3.1 revisions that the Aere lock resolves, not to a generic "6.1.0", because chip layouts and PCS parameters can move between patch releases.

Reference implementation to follow (not a bundled dependency): Succinct's standalone github.com/succinctlabs/hypercube-verifier (crates algebra, basefold, commit, jagged, merkle-tree, multilinear, stacked, sumcheck, tensor, stark, recursion, primitives, ... plus a jagged-polynomial-commitments.pdf). It is a clean, self-contained verifier for exactly this proof system and is the best porting reference. Caveat [VERIFY]: its README marks it a research prototype as of 2025-05-20, so its constants and shapes must be reconciled against the pinned 6.3.1 crates before they are trusted byte-exact.

---

2. What 0x0AE8 would actually verify (the recursion / shrink / wrap proof shape)

The SP1 pipeline at v6.1.0 is: core RISC-V proof (RiscvAir<SP1Field>, Jagged PCS + LogUp-GKR + sumcheck over KoalaBear) -> compress (recursively verify + fold shard proofs) -> shrink (compress to a single small shard) -> wrap (re-prove under a BN254-friendly config) -> BN254 Groth16/PLONK. The only Shor-breakable link is the final Groth16 wrap. The post-quantum replacement 0x0AE8 targets the proof BEFORE that wrap: the shrink shard proof (configId 1) and/or the wrap-input shard proof (configId 2).

That proof is a ShardProof of the SP1 recursion machine (RecursionAir / CompressAir), verified by verify_shard. Its shape, from crates/hypercube/src/verifier/shard.rs @ v6.1.0:

• main_commitment: Merkle (TCS) root over Poseidon2-KoalaBear of the main trace.
• opened_values (ShardOpenedValues): per-chip trace column evaluations at the sampled multilinear point (there is no univariate zeta; evaluations are at a random point in the boolean-hypercube extension domain).
• zerocheck_proof: the constraint sumcheck (point + claimed sum) that replaces the DEEP-ALI quotient.
• logup_gkr_proof: the LogUp-GKR interaction/lookup proof (per-chip evaluations).
• evaluation_proof: the Jagged / BaseFold PCS evaluation proof binding the opened values to the commitment.
• public_values: the shard public values (for the recursion machine, RecursionPublicValues).

verify_shard steps (source order): observe public values and commitments into the Poseidon2-KoalaBear challenger; validate proof shape against the machine config in the vk (chip counts, widths, heights); verify the LogUp-GKR proof; verify the zerocheck proof (sample constraint-merging challenge alpha, check merged constraint evaluations against the sumcheck claim, cross-check against the GKR evaluations); verify the PCS opening via jagged_pcs_verifier.verify_trusted_evaluations; cross-check row counts and the global cumulative sum. Source: https://github.com/succinctlabs/sp1/blob/v6.1.0/crates/hypercube/src/verifier/shard.rs

The precompile wire format in pqc-fork/pq-stark/export-inner-stark-vector.md (magic AS1\0, version, configId, vkeyDigest(32), publicValues, friProof) is broadly reusable, but two of its assumptions are wrong for 6.1.0 and MUST be corrected: the body is a Hypercube ShardProof (bincode of the 6.3.1 type), not a ShardProof<BabyBearPoseidon2>; and the vkey digest is hash_koalabear() packed (KoalaBear), not hash_babybear(). See section 8.

---

3. Component map: what is done vs what this piece needs

layer	confirmed generic skeleton (companion spec)	SP1 6.1.0 target (this spec)	reusable?
base field	BabyBear (0x78000001), F_{p^4}, W=11	KoalaBear (0x7F000001), F_{p^4}	structure yes, constants NO
hash	Poseidon2-BabyBear, 8+13 rounds, 141 consts	Poseidon2-KoalaBear, 30 rounds	structure yes, constants NO
transcript	duplex challenger over BabyBear Poseidon2	duplex over KoalaBear Poseidon2	structure yes, re-field
vector commit	FieldMerkleTreeMmcs (Poseidon2)	Merkle TCS (Poseidon2-KoalaBear)	mostly yes
low-degree test	FRI fold + query (CONFIRMED)	BaseFold multilinear (sumcheck fold)	NO, different scheme
PCS wrapper	(FRI is the PCS)	Stacked + Jagged over BaseFold	NO, new
constraint check	DEEP-ALI univariate quotient (CONFIRMED)	zerocheck (sumcheck over merged constraints)	NO, different mechanism
interaction arg	none (out of generic scope)	LogUp-GKR + septic degree-7 global digest	NO, new, biggest specific add
machine AIR	example AIRs (Fibonacci, mul)	RecursionAir chip set (section 4)	NO, program-specific
vk binding	not on real path	KoalaBear Poseidon2 vk digest (section 8)	NO, new
public values	not on real path	RecursionPublicValues (section 9)	NO, new

Reads as: the three "shape" rows (field, hash, transcript, merkle) port with a field swap plus new constants; every other row is either a different scheme (BaseFold vs FRI, zerocheck vs DEEP-ALI) or an entirely new component (Jagged, LogUp-GKR, the recursion chips, vk, public values).

---

4. The SP1 recursion machine AIR (RecursionAir): the chip set

RecursionAir<F: PrimeField32 + BinomiallyExtendable<D>, const DEGREE, const VAR_EVENTS_PER_ROW>, an AIR machine derived with sp1_derive::MachineAir. Source: https://github.com/succinctlabs/sp1/blob/v6.1.0/crates/recursion/machine/src/machine.rs Chip files: https://github.com/succinctlabs/sp1/tree/v6.1.0/crates/recursion/machine/src/chips

Full chip set (machine_wide_with_all_chips): MemoryConst, MemoryVar, BaseAlu, ExtAlu, Poseidon2Wide, Poseidon2LinearLayer, Poseidon2SBox, ExtFeltConvert, PrefixSumChecks, Select, PublicValues.

The two configs 0x0AE8 would verify use a subset:

• compress_machine: MemoryConst, MemoryVar, BaseAlu, ExtAlu, Poseidon2Wide, PrefixSumChecks, Select, PublicValues (8 chips).
• wrap_machine: MemoryConst, MemoryVar, BaseAlu, ExtAlu, Poseidon2LinearLayer, Poseidon2SBox, ExtFeltConvert, Select, PublicValues (9 chips; the wide Poseidon2 is split into linear-layer + s-box chips for the BN254-friendly wrap).

Note the departure from SP1 Turbo: there is no FriFold, no ExpReverseBitsLen, and no BatchFRI chip (those existed only because Turbo's recursion verified a FRI proof in-circuit). Their absence is itself confirmation that the recursion layer no longer runs FRI. PrefixSumChecks and ExtFeltConvert are the new arithmetic that the BaseFold/Jagged/sumcheck verification compiles down to.

Per-chip porting notes. For each chip the port must reproduce, in KoalaBear, its column layout and its eval() constraint emission order exactly (a single mis-ordered or mis-filtered constraint makes the folded constraint silently wrong):

• MemoryConst, MemoryVar (chips/mem/): the recursion VM's read/write memory tables; correctness of addresses/timestamps is enforced through the interaction bus (section 5), so most of their weight is in the LogUp argument, not local constraints. Constraint count per row: small (a handful) [VERIFY].
• BaseAlu (chips/alu_base.rs), ExtAlu (chips/alu_ext.rs): field and extension-field add/sub/mul (and the ext ALU carries F_{p^4} arithmetic). A few constraints each [VERIFY].
• Poseidon2Wide / Poseidon2LinearLayer / Poseidon2SBox (chips/poseidon2_wide/, poseidon2_helper/): the Poseidon2 permutation used inside the recursion VM (this is the in-circuit hash the recursion program itself computes). Highest per-row constraint count of the set; the wide variant is one row per permutation, the split variants spread it across rows for the wrap. Constraint count: large (the dominant chip) [VERIFY].
• ExtFeltConvert (chips/): base/extension felt conversion glue for the wrap.
• Select (chips/select.rs): conditional selection (multiplexer) constraints.
• PrefixSumChecks (chips/prefix_sum_checks.rs): running/prefix-sum constraints used by the sumcheck/BaseFold verification the recursion program runs; medium constraint count [VERIFY].
• PublicValues (chips/public_values.rs): binds the RecursionPublicValues (section 9) into the trace.

The overall DEGREE and VAR_EVENTS_PER_ROW const parameters and each chip's exact constraint count were not read line-by-line in this pass and are [VERIFY] / [MEASURE]; the ground-truth method (section 10) emits them directly from the compiled machine, which is the only trustworthy way to count them (do not hand-estimate).

---

5. The interaction argument (LogUp-GKR + septic digest): the biggest specific addition

The chips do not talk to each other through shared columns; they talk through a multiset (lookup) bus proved with LogUp-GKR, and this is the single largest component the generic quotient check does NOT cover. Sources: crates/hypercube/src/logup_gkr/ and crates/hypercube/src/lookup/, crates/hypercube/src/septic_{curve,digest,extension}.rs @ v6.1.0.

Mechanism, as read from source:

• Every send/receive interaction a chip emits is reduced to a field element via a random linear combination of the (kind, values) tuple with verifier challenges, then batched with the RLC challenge.
• The per-shard consistency of all sends and receives is proved with LogUp-GKR (a GKR circuit over the rational LogUp identity), whose proof is logup_gkr_proof in the shard proof and is verified before the zerocheck.
• The GLOBAL bus (cross-shard, e.g. memory that persists across the shard boundary) is accumulated into a SepticDigest: a point on an elliptic curve defined over the degree-7 "septic" extension of KoalaBear (SepticExtension, [u32; 7] coordinates). Each chip contributes a curve point; the digest is a special offset-corrected cumulative sum start + sum_i (digest_i - offset) + offset - start (the offset avoids Weierstrass addition exceptions), with start/offset points derived from sqrt(2) and sqrt(3) constants (CURVE_CUMULATIVE_SUM_START_*, DIGEST_SUM_START_*). The verifier checks the machine-level global cumulative sum equals the expected value (for a complete proof, the buses net to the identity). Source: https://github.com/succinctlabs/sp1/blob/v6.1.0/crates/hypercube/src/septic_digest.rs

Why this is the hard part. Porting it faithfully requires: the exact interaction-kind enumeration and field encoding per chip; the exact challenge-derivation order for the RLC and batching (a transcript contract shared with the challenger); the full LogUp-GKR verifier (layer-by-layer sumcheck over the GKR circuit); and the septic curve arithmetic (degree-7 extension mul, curve addition, the offset-sum convention, the two magic start points). None of it exists in the confirmed skeleton, and any off-by-one in the interaction encoding or the GKR layer order presents as a global "everything rejects" with no localized error. The septic curve constants and the exact interaction encoding are [VERIFY] / [MEASURE] (emit from the compiled machine).

---

6. The low-degree test: BaseFold (replaces FRI), plus Stacked + Jagged

FRI is not used. The PCS is a multilinear BaseFold committed over a Merkle TCS, wrapped by a Stacked PCS (for batching columns of different heights) and a Jagged PCS (the "pay for what you use" evaluation argument that reduces jagged, variable-length columns to a single multilinear evaluation via sumcheck). Sources: crates/prover/src/recursion.rs (RecursiveBasefoldVerifier, RecursiveMerkleTreeTcs, RecursiveStackedPcsVerifier, RecursiveJaggedPcsVerifier); reference crates hypercube-verifier/crates/{basefold, stacked, jagged, tensor, multilinear, sumcheck, merkle-tree}.

What the port needs:

• BaseFold verifier: the multilinear analogue of FRI. Commit-phase folding driven by sumcheck rounds (not the FRI fold relation), query openings against the Merkle TCS at each folded layer, final evaluation check. The confirmed FRI verify_query does not apply; this is a new verifier.
• Stacked PCS: batches the per-chip column groups (different heights) into one commitment; the verifier reconciles the per-group claims.
• Jagged PCS: verify_trusted_evaluations runs the jagged sumcheck that binds the opened multilinear evaluations (opened_values) to the committed data at the sampled point. This is where the bulk of the PCS soundness lives.
• Parameters ([MEASURE]): the BaseFold log_blowup / folding-arity / query count / proof-of-work bits for the compress, shrink, and wrap configs, and the resulting soundness (score with the Hypercube soundness analysis, not ethSTARK soundcalc, since this is not FRI). Whether the wrap config (CircuitWrapConfig) uses different PCS parameters or a different field embedding than compress/shrink is [VERIFY].

---

7. The constraint check: zerocheck sumcheck (replaces DEEP-ALI quotient)

The confirmed generic quotient-consistency identity (folded_constraints * inv_zeroifier == quotient from p3-uni-stark) is a UNIVARIATE-STARK mechanism and is not what SP1 6.1.0 checks. Instead the merged AIR constraint is verified by a sumcheck (zerocheck): the verifier samples the constraint-merging challenge alpha, the prover claims the merged constraint polynomial sums to zero over the boolean hypercube, and the sumcheck reduces that claim to a single evaluation at a random point, which is then opened through the PCS (section 6) and cross-checked against the LogUp-GKR evaluations. Source: crates/hypercube/src/verifier/shard.rs verify step 4, and hypercube-verifier/crates/stark/folder.rs

• sumcheck.

The port needs: the sumcheck verifier (round polynomials, challenge derivation, final-evaluation reduction); the constraint folder that reproduces each chip's eval() emission order and its first-row/last-row/transition filters in the multilinear setting; and the binding of the sumcheck's final point to the PCS opening. The generic DEEP-ALI code is not reusable here beyond the high-level idea of merging constraints with a random alpha.

---

8. The verifying key (vk) and its digest binding

MachineVerifyingKey fields (from crates/hypercube/src/verifier/hashable_key.rs @ v6.1.0): preprocessed_commit (Merkle root of the preprocessed/selector trace), pc_start, initial_global_cumulative_sum (a septic curve point, x and y), enable_untrusted_programs, plus the machine shape (chip ordering, widths, heights) carried by the associated Machine. Source: https://github.com/succinctlabs/sp1/blob/v6.1.0/crates/hypercube/src/verifier/hashable_key.rs

Digest binding. HashableKey provides hash_koalabear() (Poseidon2 over KoalaBear of [preprocessed_commit, pc_start, initial_global_cumulative_sum.x, initial_global_cumulative_sum.y, enable_untrusted_programs], producing an 8-element SP1Field digest), hash_u32(), hash_bytes(), and hash_bn254() (via koalabears_to_bn254(), the digest the on-chain Groth16 path currently binds).

For 0x0AE8 the verifier must (a) recompute hash_koalabear() over the supplied vk fields, (b) check it equals the 32-byte vkeyDigest in the AS1 wire envelope, and (c) use the vk's machine shape to drive the shape checks in verify_shard. The export doc's vk.hash_babybear() is WRONG for 6.1.0 and must be hash_koalabear(); the packing is 8 KoalaBear limbs, big-endian per limb. [VERIFY] the exact limb order and the exact field list that feeds hash_koalabear at the pinned 6.3.1 revision.

---

9. The public-values layout

RecursionPublicValues<T> (from crates/recursion/executor/src/public_values.rs @ v6.1.0), field type KoalaBear (T = SP1Field) on the real path. Fields (source order, as read): prev_committed_value_digest, committed_value_digest, prev_deferred_proofs_digest, deferred_proofs_digest, pc_start, next_pc, initial_timestamp, last_timestamp, memory/page indices, sp1_vk_digest, vk_root, global_cumulative_sum (septic point), digest, proof_nonce, contains_first_shard, num_included_shard, is_complete, exit_code, commit_syscall, commit_deferred_syscall. Total element count is RECURSIVE_PROOF_NUM_PV_ELTS = size_of::<RecursionPublicValues<u8>>(); the exact integer is [VERIFY] (emit from the compiled crate). Source: https://github.com/succinctlabs/sp1/blob/v6.1.0/crates/recursion/executor/src/public_values.rs

The verifier must: parse these from the wire publicValues; observe them into the challenger in the exact source order (they bind the transcript, so a wrong order diverges every challenge); check the internal digest consistency; and expose committed_value_digest / sp1_vk_digest / vk_root / is_complete / exit_code as the verified outputs the AerePQStarkVerifier adapter returns. The committed-value digest and sp1_vk_digest are what a caller uses to bind a specific guest program and its output, exactly as the BN254 path does today.

---

10. Ground-truth method (the only trustworthy validation)

Every constraint count, parameter, and layout marked [VERIFY] / [MEASURE] above must be produced from the compiled pinned toolchain, never hand-derived. The method, on a throwaway non-infra prover box (never the live infra host, never a validator; see the no-heavy-compute-on-infra rule):

1. Pin a Rust workspace to the exact resolved revisions in rollup-evm-validity/host/Cargo.lock: sp1-sdk = "=6.1.0", and let it resolve sp1-hypercube, sp1-recursion-machine, sp1-recursion-executor, slop-basefold, slop-jagged, slop-multilinear, slop-sumcheck at 6.3.1. Vendor them for reproducibility.
2. Emit machine metadata directly: for compress_machine() and wrap_machine(), print each chip's name, width, and its symbolic constraint count and max degree; print RECURSIVE_PROOF_NUM_PV_ELTS; print the BaseFold/Jagged config parameters; print the septic curve constants and the interaction-kind encoding. This replaces every [VERIFY] count with a measured one.
3. Produce a real proof: run a tiny guest (fibonacci or aere-client) through prove(...).compressed(), stopping before the Groth16 wrap; serialize the shrink ShardProof (bincode), the vk, and its hash_koalabear() digest and public_values. This is the sp1_shrink_valid_01.bin corpus vector (correcting the export doc to KoalaBear + Hypercube).
4. Instrument verify_shard to dump the exact challenger transcript (observe order, sampled alpha, the sumcheck points, the query indices) so each ported sub-verifier can be diffed byte-for-byte against the reference, the same KAT discipline the generic components used.

Follow the hypercube-verifier reference crate structure (section 1) so the port is a component-by-component mirror of a maintained verifier, not a from-scratch reading of the prover.

---

11. Effort, hardest parts, honest estimates

Realistic single-specialist estimates (STARK/sumcheck specialist with the SP1 toolchain). These are deliberately not optimistic; the two generic pieces the companion spec counted as done (FRI, DEEP-ALI) do not carry over, so the remaining surface is larger than that spec's "3 to 4 weeks for the AIR."

piece	effort (person-weeks)	risk
KoalaBear field + F_{p^4} (re-field the confirmed BabyBear code, new prime/constants)	~0.5 to 1	low
Poseidon2-KoalaBear (width 16, 30 rounds, new constants) + duplex challenger re-field	~1 to 1.5	medium (constants)
Merkle TCS over KoalaBear (re-field the confirmed MMCS)	~0.5 to 1	low
BaseFold multilinear verifier (new, replaces FRI)	~3 to 4	high
Stacked + Jagged PCS verifier (new, the jagged sumcheck)	~3 to 4	high
sumcheck + zerocheck constraint check (new, replaces DEEP-ALI)	~2 to 3	high
LogUp-GKR + septic degree-7 global digest (new, biggest specific add)	~3 to 4	HARDEST
RecursionAir chip constraints (8 to 11 chips, KoalaBear, exact eval order)	~3 to 4	high
vk binding (hash_koalabear) + RecursionPublicValues + shape checks	~1 to 2	medium
wire parser (WireReader for the Hypercube ShardProof) + adapter wiring	~1 to 2	medium
integration, gas benchmark under EIP-7825, KAT corpus, soundness scoring, audit prep	~4 to 6	high
total	~22 to 32 person-weeks	multi-month

That is roughly 5 to 8 months of focused single-specialist work plus an external audit, materially more than the companion spec's figure because the target is Hypercube, not Turbo. Hardest parts, ranked: (1) LogUp-GKR + septic digest interaction argument (section 5); (2) BaseFold + Jagged PCS (section 6); (3) the sumcheck zerocheck constraint mechanism (section 7); (4) the RecursionAir chips at exact eval order (section 4). Each is multi-week on its own.

Given this, the design doc's recommendation (companion spec section 5.1) is even more compelling: wrap a pinned, reproducible NATIVE build of the maintained Rust verifier (the hypercube-verifier crates or the sp1-verifier 6.1.0 inner path) as the precompile's crypto core, rather than hand-port a KoalaBear BaseFold + Jagged + sumcheck + LogUp-GKR verifier into Java. A hand port multiplies the audit surface and the "two wrong copies agree" risk across every one of the pieces above.

---

12. End-to-end conformance KAT (the final gate)

The single test that proves the whole verifier, once the pieces above exist:

1. Export a real SP1 6.1.0 shrink (configId 1) and wrap-input (configId 2) proof + vk + public values by the section-10 method; wrap each into the AS1 envelope (KoalaBear hash_koalabear vkey digest).
2. sp1_shrink_valid_01.bin, sp1_wrap_valid_01.bin: 0x0AE8 must ACCEPT (return the verified committed-value digest / vk digest), and the SAME public values verified through the live BN254 gateway (0x9ca479...) must agree on accept.
3. Negatives, each must REJECT (return EMPTY): flip one byte inside a query opening (*_tampered_*); mutate one byte of publicValues (*_wrongpub_*, the transcript binds them); swap in a vk with a different hash_koalabear digest (*_wrongvk_*); tamper one sumcheck round polynomial and one LogUp-GKR layer (*_badsumcheck_*, *_badgkr_*).
4. Cross-field regression: the confirmed BabyBear + FRI skeleton must continue to reject these KoalaBear Hypercube inputs (it is a different verifier), confirming the two are not conflated.

Until a real exported SP1 6.1.0 proof exists and passes this, the precompile verifies nothing and stays fail-closed. There is no offline substitute for this KAT.

---

13. Bottom line for the whole #2 effort

• What is real today: a BabyBear + FRI + univariate-STARK verifier SKELETON with six conformance-confirmed generic components (field, Poseidon2, MMCS, FRI, transcript, DEEP-ALI quotient) against Plonky3 0.4.3-succinct. That is genuine, tested work, and it is the correct verifier for Aere's OWN Plonky3 STARKs (zk-circuits/*).
• What is NOT true: that this skeleton is most of an SP1 6.1.0 verifier. SP1 6.1.0 is Hypercube. Its inner recursion proof is a KoalaBear multilinear proof (BaseFold + Stacked + Jagged PCS, sumcheck zerocheck, LogUp-GKR with a degree-7 septic global digest) over the RecursionAir chip set. The FRI and DEEP-ALI pieces do not apply to it; only the Poseidon2/Merkle/challenger SHAPES carry over, and those need the KoalaBear field and constants.
• What stands between here and a live native post-quantum STARK verifier that replaces the classical BN254 Groth16 gateway: (1) a KoalaBear re-field of the shape components; (2) the four new components (BaseFold, Jagged/Stacked, sumcheck-zerocheck, LogUp-GKR + septic digest); (3) the RecursionAir chips; (4) the vk binding and RecursionPublicValues; (5) a real exported SP1 6.1.0 end-to-end proof KAT; (6) soundness scoring and an EIP-7825 gas benchmark; (7) an external audit; (8) founder activation.
• Realistic total remaining: on the order of 22 to 32 person-weeks (roughly 5 to 8 months) of a STARK/sumcheck specialist plus an external audit, whether hand-ported or (recommended) wrapped as a pinned native build of the maintained Rust verifier. The top-level 0x0AE8 stays fail-closed the entire time; on-chain ZK verification remains classical BN254 Groth16 until all eight gates are met and the founder activates.

---

14. Open [VERIFY] / [MEASURE] flags

1. [VERIFY] Version skew: pin the exact sp1-recursion-machine / slop-* 6.3.1 revisions the Aere lock resolves; the 6.1.0 facade sits on 6.3.1 internals.
2. [VERIFY]/[MEASURE] Per-chip constraint counts, DEGREE, VAR_EVENTS_PER_ROW (emit from the compiled machine, section 10).
3. [VERIFY]/[MEASURE] RECURSIVE_PROOF_NUM_PV_ELTS exact integer and the exact PV field ordering.
4. [VERIFY]/[MEASURE] BaseFold / Jagged parameters (blowup, folding arity, query count, pow bits) for compress, shrink, and wrap; whether CircuitWrapConfig differs.
5. [VERIFY]/[MEASURE] Septic curve constants (a, b, sqrt(2)/sqrt(3) start points) and the exact per-chip interaction-kind encoding + challenge order.
6. [VERIFY] Exact hash_koalabear() input field list and limb packing at 6.3.1.
7. [VERIFY] KoalaBear Poseidon2 external/internal round split within the 30 total rounds, and its constants.
8. [VERIFY] Exact-constant conformance of the hypercube-verifier reference (2025-05-20 prototype) against the pinned 6.3.1 crates.
9. [MEASURE] The end-to-end KAT (section 12): needs a real exported SP1 6.1.0 proof; nothing offline substitutes for it.

15. Files

• docs/AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC.md (this document).
• docs/AERE-STARK-VERIFIER-PORT-SPEC.md (the generic skeleton + its confirmed status; note its BabyBear/FRI premise for SP1 6.1.0 is corrected here).
• pqc-fork/pq-stark/export-inner-stark-vector.md (real-vector export; correct hash_babybear -> hash_koalabear and the ShardProof type to the Hypercube 6.3.1 type per section 8).
• pqc-fork/precompiles/Sp1StarkVerifierPrecompiledContract.java (fail-closed skeleton; unchanged).
• contracts/contracts/zkverify/AerePQStarkVerifier.sol (fail-closed adapter; unchanged).