dd1410c266
The published line and the local line of this repository had no common ancestor: the public one carried the hygiene pass (no host names, no internal paths), the local one carried a month of corrections that never shipped. This commit ports the local work onto the public line, keeping the public hygiene wording wherever the two touched the same sentence, and keeping the public version of AERE-CROSS-CLIENT-DETERMINISM.md entirely. Carried: LICENSE/LICENSING corrections, VERIFY-POLICY.md, CITATIONS-UNRESOLVED.md remeasured 2026-08-11, the 'audited' adjective removed from next to Bouncy Castle, citation paths rewritten to published form, AIP-8, the QA consolidation report, the second EIP validation pass, fork-height corrections, the AereSink / threshold-factory correction, the forge test floor, and the architecture-map updates.
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):
|
|
`aere-research/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.
|
|
- `aere-research/pq-stark/README.md`: status bullets, layout table, reproduce commands, and a new
|
|
component-(a) section.
|