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]

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]

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.

[erik-3milabs]

How safe is this?

I seem to recall that one of our strategies is to range check (address, value, timestamp) for all writes. As a result, all reads can now be assumed safe.
When we adhere to this rule, I believe the tagged assumption to be safe.

Reasoning:
Suppose addr_xG (or addr_k or addr_R for that matter) violates the tagged assumption.
That would mean that at least one of the interactions in ec:c:read_xG would read a value from an invalid address.
To balance the LogUp, one would have had to (previously) perform a write-only interaction for this same, illegal address.
Under the assumption that all writes range check their address, this should be impossible.

Note: performing a read&write-interaction would not cut it, as this would just move the problem.

that is pushed down into the guest program

You're right that this is indeed pushed down to the guest program.

Note that this is not the first time this is done; the SHA256-C3 and SHA256-C7 essentially leverage the same trick: if the addresses for h_addr and m_addr don't align, C2 and C6 will fail.

[RobinJadoul]

I think the SHA256 version actually works regardless of the alignment?
SHA256-C3 and SHA256-C7 both use a full ADD so there's no requirement on being small enough, since ADD can deal with overlow correctly. And if it's not dword-aligned, then you get the fallback to slow version of MEMW, but besides performance, there's no safety or correctness assumption on the guest that I see there.
Please do correct me if I'm reading that wrong.

I think it is just a completeness thing and indeed not soundness as you argue, as long as we keep the initialization of addresses correctly range-checked, which is already a hard requirement due to MEMW.
We can make this assumption, but then I would put it more visibly, as this becomes critical knowledge for consumers, and not just for implementing the spec.

[erik-3milabs]

1. You're right: SHA is alignment-agnostic
2. As discussed, we're sticking with having no soundness gaps for now. I updated the spec accordingly.

[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]

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

[RobinJadoul]

Mostly concerned about the idx_k thing, the rest is either a quick edit or double checking calculations

[RobinJadoul]

and verifying x_G < p

[RobinJadoul]

Suggested change

	- the design of these chip is generic, and makes no assumptions on the parameters $b$, $p$ and $N$.
	- the design of these chip is generic, and makes no assumptions on the parameters $a$, $b$, $p$ and $N$.

[RobinJadoul]

Technically not a bit if we want it to be extensible

[RobinJadoul]

I think we're trading off padding simplicity for degree 3 constraints where otherwise we only need degree 2. Minor, but potentially worth a mention in the notes

[RobinJadoul]

But what about a greater idx_k? We'd probably need to check that k[idx_k] = 1, which seems annoying.

[RobinJadoul]

I think you're off by a few from what I tried to compute quickly, but it's wider than what I got, so should be safe anyway

[RobinJadoul]

I got -8418 (μ=1, α = 5, δ=1)

[RobinJadoul]

I think 33658

[erik-3milabs]

@claude