spec: ECSM

[erik-3milabs]

This PR introduces the ECSM (Elliptic Curve Scalar Multiplication) accelerator.

[github-actions]

Codex Code Review

Findings

• High: inactive EC_SCALAR rows emit SERVE_K tokens. In spec/src/ec_scalar.toml, the recursive SERVE_K interaction uses multiplicity = ["not", "last_limb"], independent of μ. Since line 99 forces last_limb = 0 when μ = 0, every inactive/padding row emits a free SERVE_K token. Those can be consumed by active scalar rows and produce BIT tokens not rooted in the ECSM request’s addr_k, breaking the binding between k and the double-and-add sequence. Gate this by activity, e.g. μ * (1 - last_limb) or μ - last_limb with the existing implication.

• High: ECDAS lambda carry recurrence uses c0[0] instead of c0[i]. In spec/src/ecdas.toml, the i = 1..63 lambda constraint starts with 2^8 * c0[0]. The rendered constraint and carry pattern require 2^8 * c0[i]. As written, most lambda carry limbs are not tied into the recurrence correctly, so the modular relation for λ is underconstrained for higher limbs. This can let invalid EC add/double steps satisfy the spec.

No other concrete PR-diff issues found in this pass.

[claude]

Low — Inconsistent assumption bound for addr_k

k is 32 bytes, read in four 8-byte chunks at offsets 0, 8, 16, 24 — the same access pattern as xG. The assumption for addr_xG correctly uses + 24, but this one says + 31. The bound should be + 24 for consistency and to match what is actually constrained.

Suggested change

	desc = "$(#`addr_xR` mod 2^32) + 24 < 2^32$"
	desc = "$(#`addr_k` mod 2^32) + 24 < 2^32$"

[erik-3milabs]

This + 31 is on purpose, to make sure the EC_SCALAR chip doesn't trip up.
This comment can be disregarded.

[claude]

Code Review — ECSM Accelerator Spec

Good overall structure. The three-chip decomposition (ECSM → ECDAS → EC_SCALAR) is clean, and the soundness argument for why the point-at-infinity can never appear during double-and-add is well-reasoned.

Issues found

Mathematical error (spec/ecsm.typ:23)
The non-singularity condition is written as $a^3+27b^2 \neq 0$, but the correct Weierstrass discriminant is $4a^3+27b^2 \neq 0$. Harmless for secp256k1 (a=0) but incorrect in general. See inline comment.

Typo (spec/ecsm.typ:158)
$q_0 \in [0, 2p)$ should be $q_1 \in [0, 2p)$ — copy-paste error in the quotient bound discussion.

Ref typo (spec/src/ecdas.toml:316)
"ecda:c:range_c0" is missing the trailing s — should be "ecdas:c:range_c0".

Assumption inconsistency (spec/src/ecsm.toml:199)
The alignment assumption for addr_k uses + 31 but the actual memory reads are in four 8-byte chunks at offsets 0, 8, 16, 24 — identical to addr_xG and addr_xR, which both use + 24. The bound should be + 24 for consistency.

Minor observations

• The doubling formula is silently specialized to a=0; the general theory section (which still writes E(a,b,p)) could note this specialization explicitly.
• Several new files are missing a trailing newline (about_ecalls.typ, ec_scalar.toml, ecdas.toml).
• The aside explaining why y_A != 0 for secp256k1 says "as previously established" but the establishment is not in this document — citing the odd-order argument explicitly would make it self-contained.

[erik-3milabs]

Codex Code Review

Findings

High: inactive EC_SCALAR rows emit SERVE_K tokens. In spec/src/ec_scalar.toml, the recursive SERVE_K interaction uses multiplicity = ["not", "last_limb"], independent of μ. Since line 99 forces last_limb = 0 when μ = 0, every inactive/padding row emits a free SERVE_K token. Those can be consumed by active scalar rows and produce BIT tokens not rooted in the ECSM request’s addr_k, breaking the binding between k and the double-and-add sequence. Gate this by activity, e.g. μ * (1 - last_limb) or μ - last_limb with the existing implication.

Indeed. Fixed it.

High: ECDAS lambda carry recurrence uses c0[0] instead of c0[i]. In spec/src/ecdas.toml, the i = 1..63 lambda constraint starts with 2^8 * c0[0]. The rendered constraint and carry pattern require 2^8 * c0[i]. As written, most lambda carry limbs are not tied into the recurrence correctly, so the modular relation for λ is underconstrained for higher limbs. This can let invalid EC add/double steps satisfy the spec.

Fixed it

[erik-3milabs]

Code Review — ECSM Accelerator Spec

Minor observations

• The doubling formula is silently specialized to a=0; the general theory section (which still writes E(a,b,p)) could note this specialization explicitly.

Technically, this is already addressed: the introduction mentions that it accelerates points in E(0, b, p)

• Several new files are missing a trailing newline (about_ecalls.typ, ec_scalar.toml, ecdas.toml).

Fixed

• The aside explaining why y_A != 0 for secp256k1 says "as previously established" but the establishment is not in this document — citing the odd-order argument explicitly would make it self-contained.

It is in the same document, but a section earlier. Disregarding the comment.

[RobinJadoul]

• I do wonder how much potential optimization we're leaving on the table by treating p as a generic prime, rather than using the structure it has
• A more descriptive name for the BIT and SERVE_K interactions may be in order
• The complex arith constraints for equalities mod p tend to have a different order between their "constraint" and "poly", which makes checking correspondence a bit tedious and error-prone
• I have some thoughts about the presentation of the "theory"/background, but trying to focus on the more technical things first

[RobinJadoul]

Maybe interesting to make this -11 instead, so that we essentially reserve some extra space for more hashes?

[RobinJadoul]

How safe is this? The fact that this comes from an ECALL means that it is not an assumption we can ensure at the spec level, and rather something that is pushed down into the guest program.

[RobinJadoul]

Suggested change

	=== Constrain `Gy`
	=== Constrain `yG`

For consistency

[RobinJadoul]

Does it stop working for p < 2^248, or is it just wasteful?

[RobinJadoul]

Why are we doing a bunch of MEMWs in this chip? The calling ECSM has already read all of K into byte limbs, so we can just take in the limb as input and decompose it, right?

I guess the reason is that EC_SCALAR recurses onto itself, reducing the interactions in the ECSM table, but I think for total area it'd be better feed in the bytes directly; at which point, there may be some tradeoff between how many bits EC_SCALAR does at once for width vs depth, but again probably total area tells us to just make it 256 wide?
In the case 256 columns wide wouldn't be the right call, just making multiple calls into EC_SCALAR from ECSM should nevertheless still be the same area cost as the recursion, but simpler because there's no recursion logic to be performed.

[RobinJadoul]

There may even be some approach where we avoid the recursion of ECDAS as well, and simply let the EC_SCALAR chip emit the sequence of double/add steps that need to be performed. Not entirely sure if that wouldn't introduce too many more interactions atm, but it's potentially cleaner than having to reason about the recursion stopping.

[RobinJadoul]

Feels a bit weird to have manual lemma/corollary numbering in the a title. Probably best to switch to some typst package for those, if we're intending to formalize/prove more anyway.

[RobinJadoul]

Can we maybe move these magic constant columns into a constant column of the chip? It's nicer to have them all in the same place to check correspondence with the analysis and make sure everything is up-to-date if we do change the analysis at some point (e.g. because we get Half limbs)

[RobinJadoul]

Having x_G in there looks wrong and propagates a bit further

[RobinJadoul]

I'd keep the positive here and the negative in EC_SCALAR, to keep with the usual interpretation of μ = -1 meaning that you've "shown" the relation to hold

[RobinJadoul]

The LogUp should take care of it, but probably good to still bit-check op itself too