spec: Draft FMA extension field accelerator

[RobinJadoul]

No description provided.

[github-actions]

Kimi Code Review

⚠️ Review failed: Kimi API request failed with status 401

---

Automated review by Kimi (Moonshot AI)

[github-actions]

Codex Code Review

• High – FMA drops two coefficients of c (fext_fma.toml): output[1] and output[2] omit c[1] and c[2]. Thus the chip computes a*b + (c₀,0,0), not a*b+c. Add the missing terms to both constraints and polynomials.

[erik-3milabs]

Am I correct in understanding that this PR is not yet complete? Right now, there does not seem to be a way to get the information out of the "Extension Field Realm" back to RAM/MEMORY land and interact with it. (I seem to recall we considered having assertions in the Fext-Realm, instead of the load-back, but I don't see any signs this PR introduces that solution yet)

[RobinJadoul]

Indeed, the intention was to have an FEXT_ZERO or similar chip. I'm now unsure if I had a reason to delay that, or if I was just forgetful.

[erik-3milabs]

You forgot to recompute #nr_variables, #nr_columns, and #nr_interactions.

[erik-3milabs]

Also, please highlight that the addr is read from A0.

[erik-3milabs]

Please rebase against spec/reg and update the six register accesses introduced in the fext_*.toml files.

[MauroToscano]

⚠️ AI-generated review. Produced by an automated agent and posted from this account — not written by hand. Findings below are leads to verify, not confirmed conclusions.

Review

This PR specs an Fp3 extension-field accelerator (FEXT_LOAD, FEXT_ZERO, FEXT_FMA) plus its chip TOMLs. The core algebra is correct — expanding a·b mod (X³−αX²−βX−γ) matches all three arith constraints term for term, including the (αβ+γ) and (α²+β) coefficients on a₂b₂ — the FMA timestamp separation resolves the a ← a*a+a case, and the FEXT_ZERO read-zero trick closes the loop without a load-back path. Two of the three chips are nonetheless unprovable as written, and the memory argument for the new domains is missing.

spec/src/fext_load.toml:58-59 — the MEMW interaction supplies both input and output as the same expression coeffs[i][1]·2³² + coeffs[i][0]. Presence of output is what selects the read-flavoured MEMW signature (signatures.toml:80 vs :95; Signature.matches at chip.py:869 discriminates on (self.output is None) != (other.output is None)), and MEMW binds output to old, the value already in the cell. The interaction therefore constrains old == value: FEXT_LOAD asserts the ABB slot already holds the coefficient instead of writing it. With zero-initialised field-storage the only loadable value is 0, contradicting fext.typ:37 ("write them as field elements into field-storage"). Dropping the output = [...] line selects the write-only signature, matching store.toml and the result write at fext_fma.toml:99-104. (FEXT_ZERO's read-flavoured MEMW is correct — that one wants old == 0.)

spec/src/fext_zero.toml:44 — the ECALL interaction uses multiplicity = "μ", but the CPU is the sender (cpu.toml:531, multiplicity = "ECALL") and every serving chip receives with a negated multiplicity: fext_load.toml:67 and fext_fma.toml:144 (["-", "μ"]), plus sha256:270, keccak:47, ecsm:703, halt:64, commit:78. As written a FEXT_ZERO row sends a second (timestamp, −22) token that nothing receives, so the ECALL bus cannot balance and the CPU's own token is left dangling. Should be ["-", "μ"].

spec/memory.typ:33 / spec/fext.typ:28 — domains 3/4/5 get a bullet and nothing else, yet all three chips access them only through MEMW, which always consumes a pre-existing memory token (memw.toml:218-228). Nothing in the PR emits the initial tokens or consumes the final ones, so field-storage has consumers with no producer. Existing mechanisms do not cover it: PAGE hardcodes domain 0 in both GLOBAL_MEM interactions and types init/fini as Byte (page.toml:16-23, :50, :56 — ABB cells hold full BaseField values, so it is not reusable even after parameterising the domain); streaming.typ:126-128 states PAGE "deals with boundaries on the RAM memory" with registers handled verifier-side; L2G only bridges an existing token across epochs. A subsection in fext.typ should state how field-storage is initialised/finalised (a BaseField-valued PAGE variant parameterised by domain, a verifier-side scheme like registers, or an explicit "must self-balance within an epoch" obligation on the guest), plus the at-most-once-initialisation argument that makes it sound and whatever bound applies to the 64-bit addr.

spec/fext.typ:61-63 — α, β, γ are declared as constant (preprocessed, verifier-known) columns, but their values are never pinned anywhere in the spec, leaving an implementer nothing to hardcode. The prover's own cubic extension is defined mod (w³ − 2) (Degree3GoldilocksExtensionField, crypto/math/src/field/extensions_goldilocks.rs:278), i.e. α = β = 0, γ = 2. An accelerator instantiated with any other triple computes in a different ring than the recursion verifier it exists to accelerate, and nothing here would catch it. The instantiation should be stated inline and required to agree with the STARK's extension field. Side effect worth a sentence: with α = β = 0 most terms in the three arith constraints vanish, so the rendered variable/column/degree numbers are pessimistic against the actual instantiation.

spec/src/fext_fma.toml:94, :102 (also fext_load.toml:58, fext_zero.toml:35) — all three chips pass ["+", 3, "d"] ∈ {3,4,5} as MEMW's first argument, but that slot is declared is_register of type Bit in memw.toml:6-9 and in both MEMW entries in signatures.toml:84/:99, and memw.typ:42 discusses it as a bit whose range check is documented "as a reading help". CI will not catch this: structure_matches (chip.py:78-84) compares shape and ignores ranges entirely. Now that memory.typ enumerates six separators the Bit typing is false, and an implementer working from the spec would bit-constrain that column and make FEXT unimplementable. Fix: rename to domain and retype to BaseField in memw.toml and both signatures (the memory and GLOBAL_MEM buses at signatures.toml:184/:190 and L2G already do this); REG/REGW pass a literal 1 and are unaffected. Alternatively, at minimum add a note in fext.typ that the argument is overloaded with domain separators and must not carry a bit range check.

spec/fext.typ:28 — the address encoding is recoverable only by reverse-engineering ["+", 3, "d"] out of the TOML. Neither fext.typ nor memory.typ states why there are three separators: one extension element lives at a single field-storage index addr with coefficient d at (domain 3+d, addr). Also unstated: whether addr is a byte address or an element index, the stride between consecutive elements, any alignment/bound, and that field-storage addresses are disjoint from RAM byte addresses. A short paragraph before the chip sections would make this implementable from the spec alone.

Nits:

• fext_load.toml:54 — leftover open question in a comment ("or we introduce another dedicated MEMW accelerator?"); resolve or promote to prose before merge.
• fext_fma.toml:39, :44, :49 — "definining" → "defining" in all three constant descriptions.

[RobinJadoul]

FEXT_LOAD asserts the ABB slot already holds the coefficient instead of writing it.

True, fixed

the ECALL interaction uses multiplicity = "μ"

Fixed

memory domains

Not broken, but now clarified

α, β, γ are declared as constant (preprocessed, verifier-known) columns, but their values are never pinned anywhere in the spec,

There's currently no specific field or extension pinned down in the spec itself, so there is nothing to relate it back to from here, and pinning it down only here would merely lead to confusion, imo.

so the rendered variable/column/degree numbers are pessimistic against the actual instantiation.

While it complicates the formulae a bit, I do not believe it impacts the number of columns, variables or even degree in any noticeable way.

an implementer working from the spec would bit-constrain that column and make FEXT unimplementable.

Which would technically not be following the spec, as this constraint is not specified, nor even implied by an assumption.
Which doesn't take away from the fact that updating this may make sense at this point.

Also unstated: whether addr is a byte address or an element index, the stride between consecutive elements, any alignment/bound, and that field-storage addresses are disjoint from RAM byte addresses

These are either unnecessary to state because they are unconstrained or irrelevant, or actually already stated.

leftover open question in a comment ("or we introduce another dedicated MEMW accelerator?"); resolve or promote to prose before merge.

Mainly a note for later in case we notice MEMW costs for this dominating too much.

"definining" → "defining"

Typo fixed