Pin prime subfield koalabear#264
Merged
Merged
Conversation
Replace the self-referential bound `EF: ExtensionField<PF<EF>>` (where
`PF<EF> = <EF as PrimeCharacteristicRing>::PrimeSubfield`) with a named bound
that states what the codebase already relies on:
pub trait KoalaBearExtension:
Field + ExtensionField<KoalaBear> + PrimeCharacteristicRing<PrimeSubfield = KoalaBear> {}
Both accept exactly the same types -- there is one prime field and one extension
field in the tree -- so this is a no-op for type checking. What changes is that
`PF<EF>` now *normalizes* to the concrete `KoalaBear` instead of remaining an
opaque projection, which pays off three ways:
1. Aeneas extraction. The old form made Charon diverge: translating the
projection `PF<EF>` needs a proof of `EF: PrimeCharacteristicRing`, and with
only that bound in scope the proof was rooted at a predicate that itself
mentioned `PF<EF>`. Naming the base concretely removes the cycle at the root.
`sumcheck::verify::sumcheck_verify` goes from stack overflow to a 1.3 MB
LLBC; `whir::verify` and `lean_prover::verify_execution` also extract.
2. `EF: Algebra<KoalaBear>` now follows from `ExtensionField`'s supertrait, so
code can operate on prime-field constants directly.
3. `PF<EF> == KoalaBear` becomes a fact the compiler knows. Clippy immediately
flagged the two transmutes in `restore_merkle_paths` as transmutes-to-self,
so that `TypeId` assert and both `unsafe` blocks are deleted. 16 `TypeId`
sites remain elsewhere and are now provably unnecessary in the same way.
Also drops 12 `PF<EF>: TwoAdicField` / `PrimeField64` bounds that the pinning
makes redundant. One `WhirConfig` impl keeps its `PF<EF>: TwoAdicField` because
it only requires `EF: Field`, so the projection stays opaque there; and
`ConstraintFolderPacked`'s `AirBuilder` impl keeps the old bound because its
`low_degree_block` override mentions `&mut Self` in a higher-ranked closure
bound, where the solver will not look through the blanket-implemented alias.
Verified: 66 tests pass, clippy -Dwarnings and rustfmt clean, and the workspace
builds under no-SIMD, AVX2 and AVX-512.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`AirBuilder::IF` now requires `Algebra<KoalaBear>` alongside `Algebra<Self::F>`: round constants are plain `KoalaBear` scalars while `Self::F` may be a SIMD packing, so `Algebra<PackedKoalaBear>` gave `+= PackedKoalaBear` but not `+= KoalaBear`. That gap is the entire reason the Poseidon AIR reached for `TypeId` + pointer casts. With the bound in place `add_kb(s, c)` becomes `*s += c` and `mul_kb(x, c)` becomes `x * c`, and both helpers are deleted along with `mds_air_16`'s five-way numeric dispatch -- 55 lines and 11 unsafe pointer casts, replaced by ordinary arithmetic. `mds_air_16` keeps its `SymbolicExpression` check, which is a real semantic fork (the dense matrix makes the zkDSL emit `dot_product_be` instead of Karatsuba), not type recovery. This is what `trace_gen.rs` already did with `F: Algebra<KoalaBear>`; the AIR side can now do the same. Pinning the prime subfield in the previous commit is what made this affordable. `PF<EF>` normalizes to `KoalaBear`, so the normal constraint folder satisfies `Algebra<KoalaBear>` for free and only one obligation propagates -- `EFPacking<EF>: Algebra<KoalaBear>`, since `PackedFieldExtension` supplies `Algebra<KoalaBear::Packing>` but not the unpacked scalar. Adding that to `PackedFieldExtension` directly is not possible: the quintic impl would then need a blanket `Algebra<F>` that overlaps its existing `Algebra<PF>` when the packing degenerates. So the two `Algebra<KoalaBear>`/`From<KoalaBear>` impls for `PackedQuinticExtensionField` are declared per concrete packing, and the bound is carried explicitly through the packed sumcheck path. One call site needed disambiguating: with the new bound in scope the solver has a second `PackedFieldExtension` candidate and can no longer infer the trait's parameters for `to_ext_iter`. Verified: 66 tests pass (including `test_prove_poseidon` and `display_poseidon_air_in_zk_dsl`, which exercise both the numeric and symbolic paths), clippy -Dwarnings and rustfmt clean, no-SIMD/AVX2/AVX-512 all build, and Charon still extracts `sumcheck_verify` and `verify_execution`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`merkle_commit`, `merkle_open` and `merkle_verify` were generic over `<F: Field, EF: ExtensionField<F>>` but each dispatched at runtime on `TypeId::of::<(F, EF)>()` against `(KoalaBear, QuinticExtensionFieldKB)` and `(KoalaBear, KoalaBear)`, transmuting into the concrete types and falling into `unimplemented!()` otherwise. `F` was only ever `PF<EF>`, which now normalizes to `KoalaBear`, so it stops being a parameter. That removes the reason for the dispatch: the two arms were the same code at `BasedVectorSpace::DIMENSION` 5 and 1, and the flattening helpers (`flatten_to_base_arena`, `reconstitute_from_base`, `flatten_to_base`) are already generic over the degree. Each function collapses to a single body generic in `EF`, with the degree-1 case falling out of the reflexive `ExtensionField<F> for F` impl. merkle.rs goes from 224 to 161 lines and from 12 `unsafe` blocks to one (`ArenaVec::uninitialized`, unrelated). Workspace `TypeId::of` sites: 13 -> 7. Verified both degrees are actually exercised, not just compiled: instrumenting `test_run_whir` shows commit/open/verify each running at dim=1 (round 0, base field leaves) and dim=5 (later rounds), and the prove/verify roundtrip passes -- a width or flattening mistake in either path would break the Merkle root. 66 tests pass, clippy -Dwarnings and rustfmt clean, no-SIMD/AVX2/AVX-512 build, and `whir::verify` still extracts through Charon. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Aeneas rejects a trait declaration whose default method bodies contain
closures: the closure types are children of the trait, but reference `Self`,
so they land in the same dependency group and Aeneas reports "groups of mixed
mutually recursive definitions". Two groups blocked the sumcheck verifier.
`PackedFieldExtension::to_ext_iter` loses its default body and becomes a
required method. `PackedQuinticExtensionField` already provided one; the
reflexive `PackedFieldExtension<F, F> for F::Packing` impl gets an explicit
body, which for DIMENSION = 1 reduces to picking lane `i` and so is equivalent
to the default it replaces.
`RawDataSerializable` is deleted outright rather than rewritten. Every one of
its methods and its `NUM_BYTES` constant has zero callers anywhere in the
workspace -- it is inherited from Plonky3 and only reached extraction because
`Field` listed it as a supertrait. That removes the trait, the two
`impl_raw_serializable_primefield{32,64}` macros, and both impls: 307 lines of
dead code, and with them the second recursive group.
Verified against Aeneas (HEAD 3a8586f, built against Charon 527ea8e3): both
recursive groups are gone and Aeneas now proceeds through 62 prepasses into
global translation before hitting an unrelated blocker.
66 tests pass, clippy -Dwarnings and rustfmt clean, no-SIMD/AVX2/AVX-512 build.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two more Aeneas blockers on the sumcheck verifier, both in the packing traits. `PackedFieldExtension` declared `ExtField: ExtensionField<BaseField, ExtensionPacking = Self>`. Aeneas asserts signatures carry no associated-type equality constraints and reports an internal error otherwise. The equality is not needed to compile: every impl satisfies it anyway, and dropping it leaves the workspace building unchanged. `to_ext_iter(iter: impl IntoIterator<Item = Self>) -> impl Iterator<Item = ExtField>` is replaced by `to_ext_lanes(self) -> impl Iterator<Item = ExtField>`. The `impl IntoIterator` argument adds a hidden type parameter to the method, so the `aeneas` preset lifted the return type into an associated type *with* that parameter -- a GAT, which Aeneas cannot extract. Unpacking one element at a time needs no method generics. Eleven of the sixteen call sites passed a single-element array, so they get shorter: `EFPacking::<EF>::to_ext_iter([x])` becomes `x.to_ext_lanes()`. The genuine iterator sites use `.flat_map(_::to_ext_lanes)`, which is what the old body did internally. One site in `air_sumcheck` needs the qualified form because with a generic `EF` both `PackedFieldExtension` impls are candidates. Aeneas now gets past both traits. The remaining blocker is not fixable this way: `Field::Packing` and `ExtensionField::ExtensionPacking` are associated types Charon cannot lift, because `Field`/`PackedField` and `ExtensionField`/`PackedFieldExtension` are mutually recursive -- each names the other. Aeneas cannot handle un-lifted associated types, and the 12 errors it reports all trace back to those two. 66 tests pass, clippy -Dwarnings and rustfmt clean, no-SIMD/AVX2/AVX-512 build. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.