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]

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

[RobinJadoul]

Technically not a bit if we want it to be extensible

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

Suggested change

	#`c1`_i &in [-24477, 24478].\
	#`c1`_i &in [-24478, 24477].\

[erik-3milabs]

@claude

[RobinJadoul]

Decided to quickly script the carry calculations to double check everything.

def M(n, L, mu, alpha):
    assert L >= 4
    delta = int(mu < alpha)
    return mu * n * (L - 1) + alpha - mu - delta

def bounds(n, L, mu_pos, alpha_pos, mu_neg, alpha_neg):
    min = -M(n, L, mu_neg, alpha_neg)
    max = M(n, L, mu_pos, alpha_pos)
    print(f"[{min}, {max}] => [0, {max - min}]")


print("ECSM")
bounds(32, 256, 1, 0, 1, 1)
bounds(32, 256, 3, 0, 3, 1)

print("\nECDA")
bounds(33, 256, 3, 0, 4, 1)
bounds(33, 256, 2, 0, 1, 3)
bounds(33, 256, 2, 0, 2, 2)

[RobinJadoul]

naming mismatch: offsets or carry_offsets

[RobinJadoul]

Suggested change

	#`c1`_i &in [-24477, 24478].\
	#`c1`_i &in [-24478, 24477].\

[RobinJadoul]

Suggested change

	When we selectc $#`carry_offsets` = (8160, 24477)$, we arrive at
	When we selectc $#`carry_offsets` = (8160, 24478)$, we arrive at