aere-network/aere-docs
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
main
aere-docs/AERE-STARK-FRI-SUMMARY.md
Aere Network e4cead319d Initial public release 
Aere Network public source. Everything here can be checked against the live
chain (chain id 2800, https://rpc.aere.network).

Scope note, stated up front rather than buried: consensus on chain 2800 is
classical secp256k1 ECDSA QBFT. The post-quantum work in this repository is at
the signature, precompile, account and transport layers. Nothing here makes the
consensus post-quantum, and no document in it should be read as claiming so.
2026-07-20 01:01:36 +03:00

5.8 KiB
Raw Permalink Blame History

Component (d) FRI verifier for Aere STARK-verify port (0x0AE8): summary

Scope caveat (2026-07-19 finding). This FRI verifier is conformance-confirmed against Plonky3 p3-fri 0.4.3-succinct (Aere's OWN BabyBear + FRI STARK stack), NOT against SP1 6.1.0. SP1 6.1.0 is a Hypercube release (KoalaBear multilinear), and its inner recursion proof uses BaseFold, not FRI, so this FRI low-degree test (one of the two largest confirmed pieces) does NOT apply to SP1 6.1.0 at all and this work does not verify SP1 6.1.0 proofs. Replacing the SP1 BN254 Groth16 wrap is a separate ~22 to 32 person-week retarget. See AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md.

Date: 2026-07-19. Outcome: the FRI FOLD + OPENING relation (verify_query, the low-degree test) is IMPLEMENTED and CONFORMANCE-CONFIRMED against the pinned Plonky3 p3-fri 0.4.3-succinct via a real KAT (accept genuine + reject tampered). The top-level precompile 0x0AE8 STAYS FAIL-CLOSED.

1. Confirmed FRI config (traced from pinned p3-fri 0.4.3-succinct source)

Read from the cargo cache of p3-fri (checksum 5cbc4965..., matches repo Cargo.lock):

  • Folding arity 2 (hard-coded): sibling = index ^ 1, index_pair = index >> 1 (verifier.rs verify_query).
  • FriConfig fields: { log_blowup, num_queries, proof_of_work_bits, mmcs } (config.rs).
  • log_max_height = commit_phase_commits.len() + log_blowup; num_fold_rounds = log_max_height - log_blowup.
  • Final polynomial is a SINGLE F_{p^4} CONSTANT (final_poly: F); verify_challenges checks folded == final for every query. (log_final_poly_len = 0 in this pinned version.)
  • Commit-phase MMCS = ExtensionMmcs<Val, Challenge=BinomialExtensionField<BabyBear,4>, ValMmcs> over the CONFIRMED FieldMerkleTreeMmcs (component (c)). A leaf is a PAIR of F_{p^4} evals flattened to 8 BabyBear coords (ExtensionMmcs::verify_batch, as_base_slice per element), a width-8 row of height 2^log_folded_height.
  • Grinding (proof_of_work_bits / check_witness) is in the transcript phase (verify_shape_and_sample_challenges), i.e. component (f), NOT part of the per-query fold+opening relation.
  • Fold: x = two_adic_generator(log_max_height)^reverse_bits_len(index, log_max_height) in F_{p^4}; sibling point = x * two_adic_generator(1) = -x; folded = e0 + (beta - x0)*(e1 - e0)/(x1 - x0); plus reduced_openings[log_folded_height+1] injected before each fold.

2. What I implemented

  • Ground-truth extractor pqc-fork/pq-stark/fri-extractor/ (Rust, depends on pinned p3-fri/p3-challenger/ p3-dft/p3-commit/p3-merkle-tree/p3-poseidon2/... =0.4.3-succinct; lockfile checksums matched). Builds the exact SP1 inner FRI config with the seed_from_u64(1) Poseidon2, constructs genuinely low-degree codewords, runs p3_fri::prover::prove to emit real FriProofs, and runs p3_fri::verifier::{verify_shape_and_sample_ challenges, verify_challenges} to confirm the LIBRARY accepts. Emits fri_ground_truth.json (roots, betas, query indices, reduced openings, per-query per-layer sibling values + MMCS proofs, final poly, all canonical u32) plus perm_zeros + two_adic_generators sanity anchors. 3 cases (blowup 1/2, height 6/7/8, 4/5/6 queries).
  • FRI verifier reference (verify_query / verify_challenges) in 3 languages, reusing the CONFIRMED sub-components (F_{p^4} = component (a), MMCS verifyBatch = component (c), Poseidon2 = component (b)): fri_verify_reference.py, fri_verify_reference.mjs, standalone FriVerifySelfTest.java.
  • Wired into the fail-closed Java precompile: Fri.verifyQuery (+ Fri.reverseBitsLen, Fri.foldRelationConfirmed = true) in Sp1StarkVerifierPrecompiledContract.java, using the existing BabyBearExt4 / Mmcs.verifyBatch / BabyBear.twoAdicGenerator. Fri.checkQuery kept GATED (returns UNAVAILABLE).
  • Harness test_fri_verify.py -> writes ../results/kat-results-fri-verify.json. Spec spec-fri-babybear.md. Updated port spec + pq-stark README.

3. Conformance KAT result: PASSED (accept + reject)

  • python test_fri_verify.py -> PASS=55 FAIL=0: sanity (perm_zeros == confirmed Poseidon2 zeros; 28 two-adic generators == component (a)); 3 cases each ACCEPT the genuine p3-fri proof and REJECT four tampers (corrupted opened value, corrupted MMCS sibling digest, wrong beta/fold, non-matching final poly); Python + Node + Java produce BYTE-IDENTICAL per-query folded values.
  • java FriVerifySelfTest fri_ground_truth.json -> PASS=44 FAIL=0.
  • The PRECOMPILE's own Sp1StarkVerifierPrecompiledContract.Fri.verifyQuery, driven directly against the ground truth, reproduces accept + reject for all 3 cases (15/15). So the wired code, not just parallel references, is conformant (no "two wrong copies agree").

Closed by this KAT (were [VERIFY]): arity-2 fold; num_fold_rounds = log_max_height - log_blowup + constant final poly; reverse_bits_len coset mapping; two_adic_generator(bits) == Plonky3's; F_{p^4} non-residue W = 11 == Plonky3's.

4. Top level stays FAIL-CLOSED (verified)

  • Challenger.spongePorted = false (component (f) un-ported) and StarkConstraints.evaluateAtZeta returns UNAVAILABLE (component (e) un-ported): verify() returns UNAVAILABLE at stage 4, never reaches ACCEPT.
  • computePrecompile returns VERIFIED only on ACCEPT, else Bytes.EMPTY -> EMPTY for every input.
  • The FRI fold+opening takes betas/indices/reduced-openings as INPUTS; deriving them trustlessly is component (f) (the duplex-sponge challenger), so Fri.checkQuery stays gated (UNAVAILABLE). WireReader also does not parse the commit-phase roots/openings. DO NOT ACTIVATE banner intact. Precompile compiles clean (Besu stubs, javac exit 0).

5. Scope boundary (unchanged)

On-chain ZK verifiers on Aere remain classical BN254 Groth16 until the whole verifier is real, audited, and founder-activated. This is one more component of a multi-week port. Rust compiled only in a scratch/temp dir; no live infra touched.