e4cead319d
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.
86 lines
5.6 KiB
Markdown
86 lines
5.6 KiB
Markdown
# BabyBear field + F_{p^4}: component (a) of the STARK-verify port (0x0AE8)
|
|
|
|
> **Scope caveat (2026-07-19 finding).** This component is conformance-confirmed against Plonky3
|
|
> `0.4.3-succinct` (Aere's OWN BabyBear + FRI STARK stack, the `zk-circuits/*` provers), NOT against
|
|
> SP1 6.1.0. SP1 6.1.0 is a **Hypercube** release (KoalaBear multilinear: BaseFold + Jagged +
|
|
> sumcheck-zerocheck + LogUp-GKR), so FRI and DEEP-ALI do not apply to it and this skeleton does not
|
|
> verify SP1 6.1.0 proofs. Replacing the SP1 BN254 Groth16 wrap is a separate ~22 to 32 person-week
|
|
> retarget (a founder decision). See `AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md`.
|
|
|
|
Date: 2026-07-19. Task: implement + validate the NEXT sub-component of the native STARK-verify port
|
|
(#2, precompile 0x0AE8): the BabyBear field F_p and its degree-4 extension F_{p^4}, the foundation
|
|
layer everything else in the verifier is built on.
|
|
|
|
## What was implemented
|
|
|
|
Matched the existing pq-stark sub-component convention (the prior FRI query-index piece is
|
|
Python + Node + standalone Java + a Python cross-language harness, with the production logic living
|
|
in the Java precompile). The SP1 guest side is Rust/Plonky3, but the port TARGET for 0x0AE8 is the
|
|
Java Besu precompile and the direct sibling sub-component is Python/Node/Java, so I matched that.
|
|
|
|
Production side (Java precompile, behind the still-fail-closed top level):
|
|
`aerenew/pqc-fork/precompiles/Sp1StarkVerifierPrecompiledContract.java`
|
|
- `BabyBear` (was: add/sub/mul/pow/inv): ADDED `neg`, `GENERATOR = 31`, `TWO_ADICITY = 27`,
|
|
`twoAdicGenerator(bits)`.
|
|
- `BabyBearExt4` (was: add/mul with W as `W_UNSET`/`TODO(port)`): PINNED `W = 11`, removed the
|
|
unset-guard, ADDED `sub`, `neg`, `fromBase` (base embedding), `pow(BigInteger)`, `inv` (Fermat
|
|
a^(p^4-2)), `frobenius` (a^p).
|
|
- Updated the honest-status javadoc to note the extension is now complete. The DO NOT ACTIVATE /
|
|
verifies-nothing banner and the whole fail-closed driver are untouched.
|
|
|
|
Independent references + tests (new files in `aerenew/pqc-fork/pq-stark/`):
|
|
- `babybear_field_reference.py` - Python reference (Fp + Fp4).
|
|
- `babybear_field_reference.mjs` - Node/BigInt reference (second language).
|
|
- `BabyBearFieldSelfTest.java` - standalone (no-Besu-classpath) mirror of the precompile field
|
|
logic, self-tested, with `--emit` for cross-language comparison.
|
|
- `test_babybear_field.py` - harness: axioms + Fermat-vs-bignum inverse + generator/W proofs +
|
|
Python/Node/Java agreement. Writes `../results/kat-results-babybear-field.json`.
|
|
|
|
## REAL test result (ran 2026-07-19)
|
|
|
|
- `python test_babybear_field.py` -> PASS=396242 FAIL=0, Python + Node + Java byte-identical.
|
|
- `java BabyBearFieldSelfTest` -> PASS=360018 FAIL=0.
|
|
- Precompile field edits are compile-clean: `javac` on the precompile shows only the expected
|
|
missing-Besu-symbol errors (the Besu jars are on the infra box, not local); zero errors fall in the
|
|
field-class line range 217-403, and the byte-identical standalone mirror compiles + runs.
|
|
|
|
Proven OFFLINE (no external fetch), all passing:
|
|
- F_p and F_{p^4} field axioms (comm/assoc/distrib/identities, add/sub/neg/mul inverses).
|
|
- Fermat inverse a^(p-2) == an INDEPENDENT extended-Euclid bignum inverse (Python `pow(a,-1,p)`).
|
|
- p = 2^31 - 2^27 + 1 = 2013265921; p-1 = 2^27 * 3 * 5 (2-adicity 27); p == 1 mod 4.
|
|
- `GENERATOR = 31` has multiplicative order exactly p-1 (via the known factorization).
|
|
- `twoAdicGenerator(k)` has order exactly 2^k for k = 1..27; twoAdicGenerator(27) = 440564289.
|
|
- `W = 11` is a quadratic non-residue and p == 1 mod 4, so x^4 - 11 is IRREDUCIBLE over F_p
|
|
(Lidl-Niederreiter binomial criterion), i.e. F_{p^4} = F_p[x]/(x^4 - 11) is a genuine field;
|
|
x^4 == W holds in the extension; ord(W) = 2^27 * 5, ord(x) = 4*ord(W) divides 4(p-1).
|
|
- Frobenius^4 = identity, Frobenius fixes the base field, base embedding is a ring homomorphism.
|
|
|
|
## Extension constants: confirmed vs [VERIFY]
|
|
|
|
- The field being REAL is PROVEN offline: 31 is a full-order generator, and x^4 - 11 is irreducible
|
|
so F_{p^4} is a genuine field.
|
|
- Whether GENERATOR = 31, W = 11, and twoAdicGenerator(27) = 440564289 are Plonky3
|
|
`p3-baby-bear`'s EXACT chosen constants is **[VERIFY]/[MEASURE]** against the pinned SP1 v6.1.0
|
|
Plonky3 revision. Could not confirm offline in this pass; marked, not faked. A
|
|
wrong-but-still-irreducible W would build a valid field that silently disagrees with the prover, so
|
|
irreducibility is necessary but not sufficient. (W = 11 is the value the design doc / skeleton
|
|
already cited as likely; I did not invent it.)
|
|
|
|
## Fail-closed confirmation
|
|
|
|
The top-level 0x0AE8 precompile still verifies NOTHING and stays fail-closed: `Poseidon2Bb.available`
|
|
is false, `StarkConstraints.evaluateAtZeta` and `Fri.checkQuery` still return UNAVAILABLE, and
|
|
`computePrecompile` returns EMPTY for every input. The completed field is a library dependency behind
|
|
the un-ported crypto core; it does not make the single `return ACCEPT` line reachable. On-chain ZK
|
|
verifiers remain the classical BN254 Groth16 gateway (Shor-breakable) until the whole STARK verifier
|
|
is real, audited, and founder-activated. This remains a multi-week port: components (b) Poseidon2,
|
|
(c) Merkle/MMCS, the rest of (d) FRI, (e) the AIR, and (f) the transcript are still un-ported.
|
|
|
|
## Docs updated
|
|
|
|
- `aerenew/docs/AERE-STARK-VERIFIER-PORT-SPEC.md`: section 2 (component (a) status -> IMPLEMENTED +
|
|
TESTED, with the remaining [VERIFY]/[MEASURE] items), the section 9 effort-table row (a), the
|
|
top-level status line (ONE -> TWO validated sub-components), and the section 10 file list.
|
|
- `aerenew/pqc-fork/pq-stark/README.md`: status bullets, layout table, reproduce commands, and a new
|
|
component-(a) section.
|