Add ECSM accelerator markdown spec

[MauroToscano]

Summary

• add the ECSM accelerator spec, including ECSM, ECDAS, and EC_SCALAR TOML/Typst sources
• regenerate the Markdown spec outputs, including docs/spec/ecsm.md and docs/spec/spec_full.md
• fix TOML-to-Markdown rendering for right-hand nested subtraction so expressions like round - (1 - next_op) keep their parentheses

Notes

The nested-subtraction fix corrects the generated ECDAS send interaction from the misleading round - 1 - next_op rendering to round - (1 - next_op), matching the TOML expression semantics and the prover implementation.

Validation

• python3 scripts/typst_to_md.py --output-dir docs/spec

[github-actions]

Codex Code Review

Finding

• High security: ECDAS/ECSM do not enforce canonical field coordinates < p for the input point or intermediate points. xG is only read as bytes, yG is only byte-checked, and ECDAS only byte-checks xR/yR; the only < p check is the final ECSM xR before writing. This breaks the prose arguments that cases like x_A = x_G or y_A = 0 cannot occur in F_p: a prover can use non-canonical representatives like v + p when they fit in 256 bits, absorb the extra multiple of p into the quotient, and make denominator-zero cases leave λ effectively unconstrained. Add < p checks/canonicalization for xG, yG, and every ECDAS-produced coordinate, or prove all ECDAS inputs are canonical by construction. See spec/src/ecdas.toml, spec/src/ecdas.toml, spec/src/ecsm.toml, and the exceptional-case reasoning in spec/ecsm.typ.

No other concrete issues found in the PR diff.

[claude]

Low — silent fallback for unknown types produces wrong bus sizes

When a type label is not found in config["variables"]["types"], the function returns factor (which is 1 by default) without any warning. This can silently produce incorrect bus sizes in the signatures table.

Suggested change

	typ = typ[0]
	for type_cfg in config.get("variables", {}).get("types", []):
	if type_cfg.get("label") == typ:
	return factor * len(type_cfg.get("subtypes", []))
	# Unknown primitive types (Bit, Byte, Half, etc.) have size 1
	return factor

Consider at minimum logging a warning if the type resolves to nothing, so spec authors know when a new type is missing from config.

[claude]

Medium — xG is not range-checked to [0, p)

The spec notes that xG is range-checked because it is read from memory (each byte is in [0, 255]), but that only guarantees xG ∈ [0, 2^256). There is no constraint that xG < p.

By contrast, xR is explicitly range-checked in ECSM-C28–C30 using the subtraction-overflow trick.

If a caller provides xG ≥ p, the polynomial constraints for yG will be satisfied for (xG mod p, yG) (since all arithmetic is mod p). The accelerator would silently compute k × (xG mod p, yG) instead of rejecting the input.

For secp256k1, p = 2^256 − 2^32 − 977, so inputs with xG ∈ [p, 2^256) are only ~2^32 values — a small but non-trivial set.

Recommend adding an assumption or a range-check constraint analogous to ECSM-C28–C30 for xG, or explicitly documenting this as a trusted-input assumption (analogous to the existing addr alignment assumptions).

[claude]

Low — empty placeholders throughout generated markdown

Several lines read like:

"The chip is comprised of variables that are expressed using columns and leverages interaction(s):"

The #nr_variables, #nr_columns, and #nr_interactions values are computed at Typst-render time and are not available in the TOML-to-Markdown conversion, so they appear as empty strings. This happens here and in the ECDAS and EC_SCALAR sections as well.

If this spec document is meant to be human-readable as committed markdown, consider either:

• Computing and injecting these numbers in typst_to_md.py, or
• Removing these sentences from the markdown output (they add more noise than value when empty).

[claude]

Typo: "remaing" → "remaining" (also appears in the generated docs/spec/ecsm.md and docs/spec/spec_full.md).

[claude]

Typo: "intial" → "initial".

[claude]

Review Summary

This PR adds the ECSM (Elliptic Curve Scalar Multiply) accelerator specification — covering the ECSM, ECDAS, and EC_SCALAR chips — along with TOML/Typst sources, regenerated Markdown outputs, and two rendering bug fixes.

Fixes (correct)

Nested-subtraction parenthesisation — both the Python fix (scripts/typst_to_md.py) and the Typst fix (spec/expr.typ) are correct:

• Python: the explicit parenthesis insertion for right-hand +/-/not operands handles the case that wrap doesn't cover because it only parenthesises when prec < parent_prec, not <=.
• Typst: changing pp < PREC.sub to pp <= PREC.sub correctly parenthesises a subtraction that appears as the right-hand operand of another subtraction.

Signatures rendering — the new render_signatures_doc / render_signature / signature_type_size functions cleanly replace the previously leaked Typst template code in the generated markdown.

Issues found

Severity	Location	Issue
Medium	docs/spec/ecsm.md:178 / spec/src/ecsm.toml	xG is not range-checked to [0, p); input bytes are individually range-checked but the combined 256-bit value can exceed the field modulus
Low	scripts/typst_to_md.py:79	signature_type_size silently returns 1 for unknown type labels, potentially producing wrong bus sizes with no diagnostic
Low	docs/spec/ecsm.md:49	Chip stats (nr_variables, nr_columns, nr_interactions) are empty strings throughout ECSM, ECDAS, and EC_SCALAR sections of the generated markdown
Low	spec/ecsm.typ:60, spec/ecsm.typ:262	Typos: "remaing" / "intial"

Spec correctness notes

• The double-and-add algorithm using len_k and round is correct, including the edge case k = 1 (no ECDAS rounds are needed; ECSM immediately receives the starting state back).
• The ZERO[...; sum_of_bytes] constraint with output = 0 correctly enforces k > 0.
• The termination condition round = -1 represented as 255 (Byte wrap) is unambiguous because the carry-based overflow check on k_sub_N guarantees k < N, so the sequence never legitimately starts at round 255.
• yG is reconstructed as a witness and verified via the curve equation rather than stored in memory — a valid and efficient design choice.