From 29ae66244b4866efc13680a018992e163927da5e Mon Sep 17 00:00:00 2001 From: Nicole Date: Tue, 11 Aug 2026 16:29:33 -0300 Subject: [PATCH 1/5] Spec the ECSM affine ecall variant and its IS_AFFINE selector --- spec/about_ecalls.typ | 6 +- spec/ecsm.typ | 85 +++++++++++++++++--- spec/src/ecsm.toml | 181 +++++++++++++++++++++++++++++++++++++++++- 3 files changed, 254 insertions(+), 18 deletions(-) diff --git a/spec/about_ecalls.typ b/spec/about_ecalls.typ index f4ae00a23..1b0971c96 100644 --- a/spec/about_ecalls.typ +++ b/spec/about_ecalls.typ @@ -32,8 +32,10 @@ Negative numbers (represented as 2s complement 64-bit numbers), are used for our / 93: `exit` (@halt) / -1: `SHA256` (@sha256) / -2: `KECCAK` (@keccak) -/ -11: `ECSM`/`secp256k1` (@ecsm) -/ -12: `ECSM`/`secp256r1` (@ecsm) +/ -11: `ECSM`/`secp256k1`, $x$-only (@ecsm) +/ -12: `ECSM`/`secp256k1`, affine (@ecsm) +/ -13: `ECSM`/`secp256r1`, $x$-only (@ecsm) +/ -14: `ECSM`/`secp256r1`, affine (@ecsm) / -20: `FEXT_LOAD` (@fext) / -21: `FEXT_FMA` (@fext) / -22: `FEXT_ZERO` (@fext) diff --git a/spec/ecsm.typ b/spec/ecsm.typ index 95e4ef67a..909edc5c5 100644 --- a/spec/ecsm.typ +++ b/spec/ecsm.typ @@ -51,9 +51,17 @@ When $x_P = x_Q$ and $y_P eq.not - y_Q$, one instead uses $lambda = frac(3x_P^2, The remaing case that $(x_P, y_P) = (x_Q, -y_Q)$ corresponds with $Q = -P$; the addition results in $#inf$. = Overview -This accelerator provides a compact way to prove the $x$-coordinate of the product $k times G$ for scalar $k in [1, N)$ and point $G in E(a, b, p) without {#inf}$ with $p in [3, 2^256)$ that induce curves of odd order. +This accelerator provides a compact way to prove the product $k times G$ for scalar $k in [1, N)$ and point $G in E(a, b, p) without {#inf}$ with $p in [3, 2^256)$ that induce curves of odd order. In particular, the accelerator supports the curves `secp256k1` and `secp256r1`. +The accelerator serves two ECALL variants, selected by the `is_affine` column: +/ $x$-only ($#`is_affine` = 0$): the guest supplies $x_G$ (32 bytes) and receives $x_R := (k times G)_x$ (32 bytes). The matching $y_G$ is never read from memory; the prover witnesses it and the chip merely proves it to be _a_ root of the curve equation. +/ affine ($#`is_affine` = 1$): the guest supplies the full point $x_G ‖ y_G$ (64 bytes) and receives the full point $x_R ‖ y_R$ (64 bytes). + +A single chip instance serves both variants: `is_affine` selects the ECALL-number the chip answers to, and gates the two memory accesses the affine variant adds (@ec:c:read_yG, @ec:c:write_yR) together with the address derivations they need. +Every other constraint is shared, and the $x$-only path is unchanged by the addition. +Returning $y_R$ spares the guest a second scalar multiplication: without it, the only way to recover $y(k times G)$ is to query $x((k+1) times G)$ as well and apply the chord-addition law. + #attention("Variable space.")[ This accelerator is _variable-space_ in the value of $k$; different values of $k$ may result in different table sizes. As such, *this accelerator should only be used for input sets with public $k$.* @@ -61,11 +69,11 @@ In particular, the accelerator supports the curves `secp256k1` and `secp256r1`. The accelerator comprises two chips: - *`ECSM` (Elliptic Curve Scalar Multiply)*. - This chip is responsible for + This chip is responsible for - loading $k$ from memory and verifying that it is contained in $[1, N)$, - - loading inputs $x_G$, verifying $x_G < p$, and reconstructing $y_G$, - - verifying $(k times G)_x < p$, and - - writing $(k times G)_x$ to memory. + - loading input $x_G$, verifying $x_G < p$, and either reconstructing $y_G$ ($x$-only) or loading it from memory (affine), + - verifying $(k times G)_x < p$ and $(k times G)_y < p$, and + - writing $(k times G)_x$ to memory, together with $(k times G)_y$ on the affine variant. It interacts with the `ECDAS` chip, sending $k$ and $G$ as input, and receiving $k times G$ as result. - *`ECDAS` (Elliptic Curve Double/Add Sequence)*. This chip computes $k times G$ by recursively interacting with itself. @@ -92,12 +100,26 @@ Here follows the present `id` mapping: )] Supporting other curves only requires assigning them a unique `id`.#footnote([Note that adding a curve does require `id`'s type to be updated as well, since its current type (`Bit`) is now saturated.]) -The chip is triggered by executing `ECALL`, with the ECALL-number set to $-11$ (`secp256k1`) or $-12$ (`secp256r1`). -The chip expects -- `x10` to contain the address where $x_R := (k times G)_x$ is to be stored, +The chip is triggered by executing `ECALL`, with the ECALL-number set to $-11 - 2 dot #`id` - #`is_affine`$: +#align(center)[#table( + columns: (auto, auto, auto), + table.header("ECALL number", "curve", "variant"), + "-11", `secp256k1`, [$x$-only], + "-12", `secp256k1`, "affine", + "-13", `secp256r1`, [$x$-only], + "-14", `secp256r1`, "affine", +)] +Since `id` is a per-instance constant, the ECALL-number is _linear_ in `is_affine`: the receiver (@ec:c:receive_ecall) reconstructs it as $(-11 - 2#`id`) - #`is_affine`$. +The `CPU` chip sends the guest's actual `A7` on the same bus, so a row that claims the wrong variant leaves the `ECALL` LogUp unbalanced. +This is what pins `is_affine`, and thereby the two memory accesses it gates, to the ECALL the guest really executed. + +The chip expects +- `x10` to contain the address where $x_R := (k times G)_x$ is to be stored, - `x11` to contain the address at which the least significant byte of $x_G$ is to be found, - `x12` to contain the address at which the least significant byte of $k$ is to be found, where it is assumed that $x_G$ and $k$ are provided as little-endian integers; $x_R$ is written to memory in little-endian form. +On the affine variant, the two point buffers are 64 bytes wide rather than 32: $y_G$ is read from $#`x11` + 32$ and $y_R$ is written to $#`x10` + 32$, both again little-endian. +No additional registers are consumed. == Columns #let nr_variables = total_nr_variables(ecsm_chip) @@ -110,13 +132,21 @@ The #ecsm chip is comprised of #nr_variables variables that are expressed using == Constraints === Interactions -This chip is triggered by an `ECALL` with the opcode indicating this chip: +This chip is triggered by an `ECALL` with the opcode indicating this chip and the requested variant. +Constraint @ec:c:is_affine_implies_mu forces $#`is_affine` = 0$ on padding rows, so the buses it gates cannot fire there. #render_constraint_table(ecsm_chip, config, groups: "ecall") === Read `xG` Once triggered, it loads register `x11` to see where $x_G$ is stored in memory (@ec:c:read_addr_xG) and subsequently loads $x_G$ into `xG` (@ec:c:read_xG). #render_constraint_table(ecsm_chip, config, groups: "read_xG") +=== Read `yG` +On the affine variant, the input point comes with its $y$-coordinate. +The four addresses at which it is stored are derived from `addr_xG[0]` rather than from a fourth register (@ec:c:extrapolate_addr_yG), since the guest passes $x_G ‖ y_G$ as one contiguous 64-byte buffer. +The read itself (@ec:c:read_yG) carries multiplicity `is_affine`, so it is inert on $x$-only rows — where the guest has no $y_G$ in memory to read — and on padding rows. +It shares its `timestamp` with the $x_G$-read (@ec:c:read_xG), which is sound because the two cover disjoint addresses. +#render_constraint_table(ecsm_chip, config, groups: "read_yG") + === Range check `xG` Before continuing, it is verified that $x_G in [0, p)$. To this end, witness $#`xG_sub_p` := #`xG` - p mod 2^256$ is added to `p`; if the addition sums to `xG` and overflows $mod 2^256$, it must hold that $#`xG` < p$. @@ -126,8 +156,9 @@ The addition is constrained by requiring that `c2` are bits (@ec:c:range_c2); an === Constrain `yG` With $x_G$ read and range checked, we direct our attention to $y_G$. -Rather than reading it from memory, the prover provides it as a witness and proves it to be correct. -In particular, the chip enforces the relations +On the $x$-only variant it is never read from memory; the prover provides it as a witness and proves it to be correct. +On the affine variant the same witness is additionally pinned to the caller's buffer by @ec:c:read_yG, but the relations below are enforced in both cases. +In particular, the chip enforces the relations $ x_G^2 - #`x2` - q_0 dot p &= 0,\ y_G^2 - x_G dot #`x2` - a dot x_G - b + (2p - q_1)p &= 0\ @@ -150,7 +181,15 @@ We must therefore support quotients $q_0 in [0, 2^256)$ and $q_1 in [0, 2^258)$. #aside("Two options for " + $y_G$)[ In most cases, $y_G^2$ has _two_ roots $mod p$. This means that enforcing the above relation does not fully constrain the prover: it can choose which of the two to provide as hint. - However, in this setting, this is not a problem: the `ECSM`-chip only outputs the $x$-coordinate of $k times G$, which is the same, irrespective of the chosen root. + On the $x$-only variant this is not a problem: the chip only outputs the $x$-coordinate of $k times G$, and $x(k times G) = x(k times (-G))$, so both choices yield the same output. +] + +#attention("The affine variant must pin the sign of " + $y_G$)[ + As soon as $y_R$ is published, the freedom described above becomes exploitable. + A prover that answers with $-y_G$ computes $k times (-G)$: a correct multiple of a _different_ point. + The curve equation cannot tell the two apart, and neither can the guest, which delegated the multiplication precisely because it cannot perform it. + Constraint @ec:c:read_yG is what closes this: it pins the `yG` witness to the bytes the caller placed at $#`addr_xG` + 32$. + This is also why the read fires with multiplicity `is_affine` rather than `μ` — the $x$-only path has nothing to pin it to, and does not need it. ] Below, we enforce the first of the two sub-relations. @@ -184,11 +223,33 @@ The addition is constrained by requiring that `c4` are bits (@ec:c:range_c4); an #render_constraint_table(ecsm_chip, config, groups: "range_xR") +=== Range check `yR` +The same treatment is given to $y_R$: witness $#`yR_sub_p` := #`yR` - p mod 2^256$ is added to `p`, and the addition is required to overflow (@ec:c:yR_addition_overflows), which holds if and only if $#`yR` < p$. + +Unlike the $y_G$-read, this check fires on _every_ active row rather than only on affine ones. +It is cheap, `yR` is witnessed in both variants anyway, and gating it on `is_affine` would buy nothing. + +#aside("Why " + $y_R$ + " needs a canonicality check at all")[ + The `ECDAS` relations that produce $y_R$ absorb a multiple of $p$ into their quotient columns, and the byte range checks only bound $y_R$ below $2^256$. + A prover could therefore publish $y_R + p$ whenever $y_R < 2^256 - p$ and still satisfy every other constraint. + For `secp256k1` that band has width $2^256 - p approx 2^32$, and it is populated: the curve has points with very small $y$. + Constraint @ec:c:yR_addition_overflows is what rules the non-canonical representative out. + $x_R$ was already covered by @ec:c:xR_addition_overflows; publishing $y_R$ is what makes _its_ representation observable too. +] + +#render_constraint_table(ecsm_chip, config, groups: "range_yR") + === Write `xR` We read `addr_xR` from register `x10` (@ec:c:load_addr_xR), and subsequently write `xR` to this address (@ec:c:write_xR). Note that the `timestamp` on both memory accesses is offset to allow `addr_xR` to equal `addr_xG` and thus for $x_R$ to overwrite $x_G$ in memory. #render_constraint_table(ecsm_chip, config, groups: "write_xR") +=== Write `yR` +On the affine variant, $y_R$ is written directly after $x_R$, at addresses derived from `addr_xR[0]` (@ec:c:extrapolate_addr_yR); as on the input side, the output buffer is one contiguous 64-byte region and no extra register is read. +The write carries multiplicity `is_affine` (@ec:c:write_yR) and uses $#`timestamp` + 3$, the fourth and last sub-timestamp of the instruction: $x_G$ and $y_G$ occupy `timestamp`, $k$ occupies $#`timestamp` + 1$ and $x_R$ occupies $#`timestamp` + 2$. +Placing it last also keeps $x_R ‖ y_R$ overwriting $x_G ‖ y_G$ legal. +#render_constraint_table(ecsm_chip, config, groups: "write_yR") + == Carry offsets We close by deriving the values of `offsets`. To this end, we decompose the formulae diff --git a/spec/src/ecsm.toml b/spec/src/ecsm.toml index 226c61816..a5f355f99 100644 --- a/spec/src/ecsm.toml +++ b/spec/src/ecsm.toml @@ -24,16 +24,34 @@ type = ["DWordHL", 4] desc = "address to which the `x`-coordinate of result point `R` is to be written" pad = 0 +[[variables.input]] +name = "is_affine" +type = "Bit" +desc = "whether the _affine_ (1) or the _`x`-only_ (0) variant of the ECALL is served" +pad = 0 + [[variables.output]] name = "xR" type = "U256BL" desc = "$(#`k` times #`G`)_x$" pad = 0 -[[variables.auxiliary]] +[[variables.output]] name = "yR" type = "U256BL" -desc = "$(#`k` times #`G`)_y$" +desc = "$(#`k` times #`G`)_y$; only written to memory when $#`is_affine` = 1$" +pad = 0 + +[[variables.auxiliary]] +name = "addr_yG" +type = ["DWordHL", 4] +desc = "address at which the `y`-coordinate of start point `G` is stored" +pad = 0 + +[[variables.auxiliary]] +name = "addr_yR" +type = ["DWordHL", 4] +desc = "address to which the `y`-coordinate of result point `R` is to be written" pad = 0 [[variables.auxiliary]] @@ -57,7 +75,7 @@ pad = 0 [[variables.auxiliary]] name = "yG" type = "U256BL" -desc = "$y_G$" +desc = "$y_G$; read from memory when $#`is_affine` = 1$, a free witness otherwise" pad = 0 [[variables.auxiliary]] @@ -108,6 +126,12 @@ type = "U256HL" desc = "$x_R - #`p` mod 2^256$" pad = 0 +[[variables.auxiliary]] +name = "yR_sub_p" +type = "U256HL" +desc = "$y_R - #`p` mod 2^256$" +pad = 0 + [[variables.virtual]] name = "byte_k" type = "U256BL" @@ -143,6 +167,15 @@ def = {polys=[ {iter=["i", 1, 7], poly=["*", ["^", 2, -32], ["-", ["+", ["idx", ["cast", "p", "U256WL"], "i"], ["idx", ["cast", "xR_sub_p", "U256WL"], "i"], ["idx", "c4", ["-", "i", 1]]], ["idx", ["cast", "xR", "U256WL"], "i"]]]}, ]} +[[variables.virtual]] +name = "c5" +type = ["Bit", 8] +desc = "carries for computing $#`p` + #`yR_sub_p`$" +def = {polys=[ + {iter=["i", 0], poly=["*", ["^", 2, -32], ["-", ["+", ["idx", ["cast", "p", "U256WL"], "i"], ["idx", ["cast", "yR_sub_p", "U256WL"], "i"]], ["idx", ["cast", "yR", "U256WL"], "i"]]]}, + {iter=["i", 1, 7], poly=["*", ["^", 2, -32], ["-", ["+", ["idx", ["cast", "p", "U256WL"], "i"], ["idx", ["cast", "yR_sub_p", "U256WL"], "i"], ["idx", "c5", ["-", "i", 1]]], ["idx", ["cast", "yR", "U256WL"], "i"]]]}, +]} + [[variables.virtual]] name = "XG" type = ["Byte", 64] @@ -314,6 +347,61 @@ iter = ["i", 0, 3] multiplicity = "μ" ref = "ec:c:read_xG" +# Load yG from memory (affine variant only) + +[[constraint_groups]] +name = "read_yG" + +[[constraints.read_yG]] +kind = "template" +tag = "ADD" +input = [["cast", ["idx", "addr_xG", 0], "DWordWL"], ["cast", ["+", 32, ["*", 8, "i"]], "DWordWL"]] +output = ["cast", ["idx", "addr_yG", "i"], "DWordWL"] +iter = ["i", 0, 3] +cond = "is_affine" +ref = "ec:c:extrapolate_addr_yG" + +[[constraints.read_yG]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", ["idx", "addr_yG", "i"], "j"]] +iters = [["i", 0, 3], ["j", 0, 3]] +multiplicity = "is_affine" +ref = "ec:c:range_addr_yG" + +[[constraints.read_yG]] +kind = "interaction" +tag = "MEMW" +input = [ + 0, + ["cast", ["idx", "addr_yG", "i"], "DWordWL"], + ["arr", + ["idx", "yG", ["+", ["*", 8, "i"], 0]], + ["idx", "yG", ["+", ["*", 8, "i"], 1]], + ["idx", "yG", ["+", ["*", 8, "i"], 2]], + ["idx", "yG", ["+", ["*", 8, "i"], 3]], + ["idx", "yG", ["+", ["*", 8, "i"], 4]], + ["idx", "yG", ["+", ["*", 8, "i"], 5]], + ["idx", "yG", ["+", ["*", 8, "i"], 6]], + ["idx", "yG", ["+", ["*", 8, "i"], 7]], + ], + "timestamp", + 0, 0, 1 +] +output = ["arr", + ["idx", "yG", ["+", ["*", 8, "i"], 0]], + ["idx", "yG", ["+", ["*", 8, "i"], 1]], + ["idx", "yG", ["+", ["*", 8, "i"], 2]], + ["idx", "yG", ["+", ["*", 8, "i"], 3]], + ["idx", "yG", ["+", ["*", 8, "i"], 4]], + ["idx", "yG", ["+", ["*", 8, "i"], 5]], + ["idx", "yG", ["+", ["*", 8, "i"], 6]], + ["idx", "yG", ["+", ["*", 8, "i"], 7]], +] +iter = ["i", 0, 3] +multiplicity = "is_affine" +ref = "ec:c:read_yG" + # Range check xG [[constraint_groups]] @@ -632,6 +720,33 @@ constraint = "$#`μ` => #`c4`_7 = 1$" poly = ["*", "μ", ["not", ["idx", "c4", 7]]] ref = "ec:c:xR_addition_overflows" +# Range check yR + +[[constraint_groups]] +name = "range_yR" + +[[constraints.range_yR]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "yR_sub_p", "i"]] +iter = ["i", 0, 15] +multiplicity = "μ" +ref = "ec:c:range_yR_sub_p" + +[[constraints.range_yR]] +kind = "template" +tag = "IS_BIT" +input = [["idx", "c5", "i"]] +iter = ["i", 0, 6] +cond = "μ" +ref = "ec:c:range_c5" + +[[constraints.range_yR]] +kind = "arith" +constraint = "$#`μ` => #`c5`_7 = 1$" +poly = ["*", "μ", ["not", ["idx", "c5", 7]]] +ref = "ec:c:yR_addition_overflows" + # Write R to memory @@ -686,6 +801,51 @@ iter = ["i", 0, 3] multiplicity = "μ" ref = "ec:c:write_xR" +# Write yR to memory (affine variant only) + +[[constraint_groups]] +name = "write_yR" + +[[constraints.write_yR]] +kind = "template" +tag = "ADD" +input = [["cast", ["idx", "addr_xR", 0], "DWordWL"], ["cast", ["+", 32, ["*", 8, "i"]], "DWordWL"]] +output = ["cast", ["idx", "addr_yR", "i"], "DWordWL"] +iter = ["i", 0, 3] +cond = "is_affine" +ref = "ec:c:extrapolate_addr_yR" + +[[constraints.write_yR]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", ["idx", "addr_yR", "i"], "j"]] +iters = [["i", 0, 3], ["j", 0, 3]] +multiplicity = "is_affine" +ref = "ec:c:range_addr_yR" + +[[constraints.write_yR]] +kind = "interaction" +tag = "MEMW" +input = [ + 0, + ["cast", ["idx", "addr_yR", "i"], "DWordWL"], + ["arr", + ["idx", "yR", ["+", ["*", 8, "i"], 0]], + ["idx", "yR", ["+", ["*", 8, "i"], 1]], + ["idx", "yR", ["+", ["*", 8, "i"], 2]], + ["idx", "yR", ["+", ["*", 8, "i"], 3]], + ["idx", "yR", ["+", ["*", 8, "i"], 4]], + ["idx", "yR", ["+", ["*", 8, "i"], 5]], + ["idx", "yR", ["+", ["*", 8, "i"], 6]], + ["idx", "yR", ["+", ["*", 8, "i"], 7]], + ], + ["+", "timestamp", 3], + 0, 0, 1 +] +iter = ["i", 0, 3] +multiplicity = "is_affine" +ref = "ec:c:write_yR" + [[constraint_groups]] name = "ecall" @@ -696,11 +856,24 @@ tag = "IS_BIT" input = ["μ"] ref = "ec:c:mu_isbit" +[[constraints.ecall]] +kind = "template" +tag = "IS_BIT" +input = ["is_affine"] +ref = "ec:c:is_affine_isbit" + +[[constraints.ecall]] +kind = "arith" +constraint = "$#`is_affine` != 0 => #`μ` != 0$" +poly = ["*", "is_affine", ["not", "μ"]] +ref = "ec:c:is_affine_implies_mu" + [[constraints.ecall]] kind = "interaction" tag = "ECALL" -input = ["timestamp", ["arr", ["-", ["^", 2, 32], 11, "id"], ["-", ["^", 2, 32], 1]]] +input = ["timestamp", ["arr", ["-", ["^", 2, 32], 11, ["*", 2, "id"], "is_affine"], ["-", ["^", 2, 32], 1]]] multiplicity = ["-", "μ"] +ref = "ec:c:receive_ecall" [[constraint_groups]] name = "delegate" From 3837f1d936422d193b707ab282aa02988435a8d9 Mon Sep 17 00:00:00 2001 From: Nicole Date: Tue, 11 Aug 2026 16:48:23 -0300 Subject: [PATCH 2/5] Cite the memory-granularity rule and correct the x-only claim --- spec/ecsm.typ | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/spec/ecsm.typ b/spec/ecsm.typ index 909edc5c5..64d2d6b16 100644 --- a/spec/ecsm.typ +++ b/spec/ecsm.typ @@ -59,7 +59,8 @@ The accelerator serves two ECALL variants, selected by the `is_affine` column: / affine ($#`is_affine` = 1$): the guest supplies the full point $x_G ‖ y_G$ (64 bytes) and receives the full point $x_R ‖ y_R$ (64 bytes). A single chip instance serves both variants: `is_affine` selects the ECALL-number the chip answers to, and gates the two memory accesses the affine variant adds (@ec:c:read_yG, @ec:c:write_yR) together with the address derivations they need. -Every other constraint is shared, and the $x$-only path is unchanged by the addition. +Every other constraint is shared between the two. +The one addition that is _not_ gated is the $y_R < p$ check (@ec:c:yR_addition_overflows): it applies on every active row, so the $x$-only path is now obliged to witness a canonical $y_R$ as well. Returning $y_R$ spares the guest a second scalar multiplication: without it, the only way to recover $y(k times G)$ is to query $x((k+1) times G)$ as well and apply the chord-addition law. #attention("Variable space.")[ @@ -144,7 +145,7 @@ Once triggered, it loads register `x11` to see where $x_G$ is stored in memory ( On the affine variant, the input point comes with its $y$-coordinate. The four addresses at which it is stored are derived from `addr_xG[0]` rather than from a fourth register (@ec:c:extrapolate_addr_yG), since the guest passes $x_G ‖ y_G$ as one contiguous 64-byte buffer. The read itself (@ec:c:read_yG) carries multiplicity `is_affine`, so it is inert on $x$-only rows — where the guest has no $y_G$ in memory to read — and on padding rows. -It shares its `timestamp` with the $x_G$-read (@ec:c:read_xG), which is sound because the two cover disjoint addresses. +It shares its `timestamp` with the $x_G$-read (@ec:c:read_xG); the two cover disjoint addresses, which is exactly the condition under which @memory:aside:granularity permits a shared timestamp. #render_constraint_table(ecsm_chip, config, groups: "read_yG") === Range check `xG` @@ -246,7 +247,7 @@ Note that the `timestamp` on both memory accesses is offset to allow `addr_xR` t === Write `yR` On the affine variant, $y_R$ is written directly after $x_R$, at addresses derived from `addr_xR[0]` (@ec:c:extrapolate_addr_yR); as on the input side, the output buffer is one contiguous 64-byte region and no extra register is read. -The write carries multiplicity `is_affine` (@ec:c:write_yR) and uses $#`timestamp` + 3$, the fourth and last sub-timestamp of the instruction: $x_G$ and $y_G$ occupy `timestamp`, $k$ occupies $#`timestamp` + 1$ and $x_R$ occupies $#`timestamp` + 2$. +The write carries multiplicity `is_affine` (@ec:c:write_yR) and uses $#`timestamp` + 3$, the fourth and last of the cycle's sub-timestamps (@memory:aside:granularity): $x_G$ and $y_G$ occupy `timestamp`, $k$ occupies $#`timestamp` + 1$ and $x_R$ occupies $#`timestamp` + 2$. Placing it last also keeps $x_R ‖ y_R$ overwriting $x_G ‖ y_G$ legal. #render_constraint_table(ecsm_chip, config, groups: "write_yR") From 312e183f2ae7affd85d51746a577c767550cda7b Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 12 Aug 2026 10:59:38 -0300 Subject: [PATCH 3/5] Correct the affine prose and document the address-limb and single-curve preconditions --- spec/ecsm.typ | 37 +++++++++++++++++++++++++++---------- 1 file changed, 27 insertions(+), 10 deletions(-) diff --git a/spec/ecsm.typ b/spec/ecsm.typ index 64d2d6b16..9b60d7b75 100644 --- a/spec/ecsm.typ +++ b/spec/ecsm.typ @@ -58,10 +58,10 @@ The accelerator serves two ECALL variants, selected by the `is_affine` column: / $x$-only ($#`is_affine` = 0$): the guest supplies $x_G$ (32 bytes) and receives $x_R := (k times G)_x$ (32 bytes). The matching $y_G$ is never read from memory; the prover witnesses it and the chip merely proves it to be _a_ root of the curve equation. / affine ($#`is_affine` = 1$): the guest supplies the full point $x_G ‖ y_G$ (64 bytes) and receives the full point $x_R ‖ y_R$ (64 bytes). -A single chip instance serves both variants: `is_affine` selects the ECALL-number the chip answers to, and gates the two memory accesses the affine variant adds (@ec:c:read_yG, @ec:c:write_yR) together with the address derivations they need. +A single chip instance serves both variants: `is_affine` selects the ECALL-number the chip answers to, and gates the two memory accesses the affine variant adds (@ec:c:read_yG, @ec:c:write_yR) together with the address derivations (@ec:c:extrapolate_addr_yG, @ec:c:extrapolate_addr_yR) and address range checks (@ec:c:range_addr_yG, @ec:c:range_addr_yR) they need. Every other constraint is shared between the two. -The one addition that is _not_ gated is the $y_R < p$ check (@ec:c:yR_addition_overflows): it applies on every active row, so the $x$-only path is now obliged to witness a canonical $y_R$ as well. -Returning $y_R$ spares the guest a second scalar multiplication: without it, the only way to recover $y(k times G)$ is to query $x((k+1) times G)$ as well and apply the chord-addition law. +Of the constraints this variant adds, the ones _not_ gated on `is_affine` are the three of the $y_R < p$ check (@ec:c:range_yR_sub_p, @ec:c:range_c5, @ec:c:yR_addition_overflows), which are gated on `μ` and so apply on every active row — obliging the $x$-only path to witness a canonical $y_R$ as well — and @ec:c:is_affine_isbit, which carries no condition at all. +Returning $y_R$ spares the guest a second scalar multiplication: without it, recovering $y(k times G)$ means either a second query $x((k+1) times G)$ plus the chord-addition law, or a modular square root of $x_R^3 + a x_R + b$, which leaves the sign undetermined. #attention("Variable space.")[ This accelerator is _variable-space_ in the value of $k$; different values of $k$ may result in different table sizes. @@ -99,7 +99,14 @@ Here follows the present `id` mapping: "0", `secp256k1`, "1", `secp256r1`, )] -Supporting other curves only requires assigning them a unique `id`.#footnote([Note that adding a curve does require `id`'s type to be updated as well, since its current type (`Bit`) is now saturated.]) +Supporting other curves only requires assigning them a unique `id`.#footnote([Note that adding a curve does require `id`'s type to be updated as well, since its current type (`Bit`) is now saturated. Since each curve now claims _two_ ECALL-numbers (see below), it also consumes the reserved range twice as fast: $#`id` = 4$ would collide with `FEXT_LOAD` at $-20$.]) + +#attention("Only " + `secp256k1` + " is instantiated.")[ + The constraints below are written generically in $a$, $b$, $p$ and $N$, but only $#`id` = 0$ has ever been instantiated, and that curve has $a = 0$. + The $y_G$ relation carries a single $p^2$ offset (@ec:c:c1_0, @ec:c:c1_i), which is enough to keep $q_1$ non-negative only while $a dot x_G$ is small. + For a curve with large $a$ --- `secp256r1` has $a = p - 3$ --- the offset is insufficient, and the more so on the affine variant, where @ec:c:read_yG pins $y_G$ and so removes the prover's freedom to pick whichever root gives a representable quotient. + Instantiating $#`id` = 1$ therefore requires widening the offset _and_ `q1`'s top limb; the ECALL-numbers $-13$ and $-14$ are reserved, not usable. +] The chip is triggered by executing `ECALL`, with the ECALL-number set to $-11 - 2 dot #`id` - #`is_affine`$: #align(center)[#table( @@ -119,9 +126,14 @@ The chip expects - `x11` to contain the address at which the least significant byte of $x_G$ is to be found, - `x12` to contain the address at which the least significant byte of $k$ is to be found, where it is assumed that $x_G$ and $k$ are provided as little-endian integers; $x_R$ is written to memory in little-endian form. -On the affine variant, the two point buffers are 64 bytes wide rather than 32: $y_G$ is read from $#`x11` + 32$ and $y_R$ is written to $#`x10` + 32$, both again little-endian. +On the affine variant, the two point buffers are 64 bytes wide rather than 32: $y_G$ is read from 32 bytes above the address held in `x11`, and $y_R$ is written 32 bytes above the address held in `x10`, both again little-endian. No additional registers are consumed. +Widening the buffers widens the caller's obligations, and neither is enforced by this chip. +The buffers must not overlap the scalar, since $x_G ‖ y_G$ is read at `timestamp` and $k$ at $#`timestamp` + 1$, and the memory argument cannot serve one address twice in one cycle. +An operand's address must also stay clear of a $2^32$ boundary --- by 64 bytes for the two point buffers and 32 for $k$ --- because the implementation adds each per-access offset to the low half of the address alone and cannot carry into the high half. +The constraints below abstract over that: they derive every address with a full 64-bit `ADD` (@ec:c:extrapolate_addr_yG, @ec:c:extrapolate_addr_yR), which carries correctly and so admits addresses the `ECALL` itself rejects. + == Columns #let nr_variables = total_nr_variables(ecsm_chip) #let nr_columns = total_nr_instantiated_columns(ecsm_chip, config) @@ -228,14 +240,19 @@ The addition is constrained by requiring that `c4` are bits (@ec:c:range_c4); an The same treatment is given to $y_R$: witness $#`yR_sub_p` := #`yR` - p mod 2^256$ is added to `p`, and the addition is required to overflow (@ec:c:yR_addition_overflows), which holds if and only if $#`yR` < p$. Unlike the $y_G$-read, this check fires on _every_ active row rather than only on affine ones. -It is cheap, `yR` is witnessed in both variants anyway, and gating it on `is_affine` would buy nothing. +`yR` is witnessed in both variants anyway, so gating it would save no columns; it would drop the 16 `IS_HALF` lookups of @ec:c:range_yR_sub_p and the 7 `IS_BIT` terms of @ec:c:range_c5 on $x$-only rows, which we judge not worth a second selector. #aside("Why " + $y_R$ + " needs a canonicality check at all")[ - The `ECDAS` relations that produce $y_R$ absorb a multiple of $p$ into their quotient columns, and the byte range checks only bound $y_R$ below $2^256$. + The relations that produce $y_R$ absorb a multiple of $p$ into their quotient columns, and $y_R$ is bounded only below $2^256$. A prover could therefore publish $y_R + p$ whenever $y_R < 2^256 - p$ and still satisfy every other constraint. For `secp256k1` that band has width $2^256 - p approx 2^32$, and it is populated: the curve has points with very small $y$. - Constraint @ec:c:yR_addition_overflows is what rules the non-canonical representative out. + Constraint @ec:c:yR_addition_overflows is what rules the non-canonical representative out, given that `c5` are bits (@ec:c:range_c5). $x_R$ was already covered by @ec:c:xR_addition_overflows; publishing $y_R$ is what makes _its_ representation observable too. + + The $2^256$ bound the argument rests on is worth locating precisely, because it is not local to this group. + On a row that delegates, it comes from the `ECDAS` chip, which range-checks its own $y_R$ bytes before sending them. + But when $#`k` = 1$ the delegation collapses: @ec:c:start_double_add and @ec:c:receive_double_add carry identical tuples and cancel on the bus, so no `ECDAS` row exists at all, and the bound then comes from @ec:c:range_yG via $y_R = y_G$. + Either way $y_R$ is byte-bounded, but this chip nowhere range-checks `yR` itself. ] #render_constraint_table(ecsm_chip, config, groups: "range_yR") @@ -248,7 +265,7 @@ Note that the `timestamp` on both memory accesses is offset to allow `addr_xR` t === Write `yR` On the affine variant, $y_R$ is written directly after $x_R$, at addresses derived from `addr_xR[0]` (@ec:c:extrapolate_addr_yR); as on the input side, the output buffer is one contiguous 64-byte region and no extra register is read. The write carries multiplicity `is_affine` (@ec:c:write_yR) and uses $#`timestamp` + 3$, the fourth and last of the cycle's sub-timestamps (@memory:aside:granularity): $x_G$ and $y_G$ occupy `timestamp`, $k$ occupies $#`timestamp` + 1$ and $x_R$ occupies $#`timestamp` + 2$. -Placing it last also keeps $x_R ‖ y_R$ overwriting $x_G ‖ y_G$ legal. +The two halves of the output cover disjoint addresses, so they could legally share a sub-timestamp; $#`timestamp` + 3$ is simply the slot left over, and taking it leaves this chip with no further headroom in the cycle. #render_constraint_table(ecsm_chip, config, groups: "write_yR") == Carry offsets @@ -424,7 +441,7 @@ $ = Notes / optimizations - To utilize the #ecsm / #ecdas chips for different curves, consider introducing a lookup table for the curve-constants $a$, $b$, $p$, $r$ and $N$, and look them up when a scalar multiplication selects them. - The selection procedure could be done through the `ECALL` number; the #ecsm chip would accept multiple numbers, setting an internal "curve-selector" field accordingly. + The selection procedure could be done through the `ECALL` number, in the same way `is_affine` already selects the variant: the #ecsm chip accepts several numbers and sets an internal selector column accordingly, pinned by the `ECALL` bus (@ec:c:receive_ecall). - Transitioning from `U256BL`s to `U256HL`s would roughly halve the number of columns in both the #ecsm and #ecdas chips. This would likely require increasing the sizes of the carries from 16 to 24 bits. Since the carries need to be range checked, one would have to investigate whether From 7e65c658debe9900c9d6434440b32c29d991e216 Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 12 Aug 2026 12:15:28 -0300 Subject: [PATCH 4/5] =?UTF-8?q?Flag=20that=20the=20exposition's=202p=C2=B2?= =?UTF-8?q?=20offset=20disagrees=20with=20the=20constraint's=20p=C2=B2?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- spec/ecsm.typ | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/spec/ecsm.typ b/spec/ecsm.typ index 9b60d7b75..214c230c4 100644 --- a/spec/ecsm.typ +++ b/spec/ecsm.typ @@ -103,7 +103,9 @@ Supporting other curves only requires assigning them a unique `id`.#footnote([No #attention("Only " + `secp256k1` + " is instantiated.")[ The constraints below are written generically in $a$, $b$, $p$ and $N$, but only $#`id` = 0$ has ever been instantiated, and that curve has $a = 0$. - The $y_G$ relation carries a single $p^2$ offset (@ec:c:c1_0, @ec:c:c1_i), which is enough to keep $q_1$ non-negative only while $a dot x_G$ is small. + The $y_G$ relation as constrained carries a single $p^2$ offset (@ec:c:c1_0, @ec:c:c1_i), which is enough to keep $q_1$ non-negative only while $a dot x_G$ is small. + Note that this disagrees with how the relation is written below, which states an offset of $2p^2$ and a bound $q_1 in [0, 3p)$: the constraints are authoritative, and their single $p^2$ is what makes `q1`'s declared width sufficient, since $q_1 < 2p < 2^257 < 3p$. + Reconciling the two --- either by correcting the exposition or by widening the constraint to $2p^2$ and `q1` with it --- is left as separate work, since only the latter changes the chip. For a curve with large $a$ --- `secp256r1` has $a = p - 3$ --- the offset is insufficient, and the more so on the affine variant, where @ec:c:read_yG pins $y_G$ and so removes the prover's freedom to pick whichever root gives a representable quotient. Instantiating $#`id` = 1$ therefore requires widening the offset _and_ `q1`'s top limb; the ECALL-numbers $-13$ and $-14$ are reserved, not usable. ] From ddab868508652944e698709ecaf48750fe9b1de1 Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 12 Aug 2026 16:03:58 -0300 Subject: [PATCH 5/5] Correct the operand-overlap rationale and qualify the ecall-number collision --- spec/ecsm.typ | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/spec/ecsm.typ b/spec/ecsm.typ index 214c230c4..9f00dd06f 100644 --- a/spec/ecsm.typ +++ b/spec/ecsm.typ @@ -99,7 +99,7 @@ Here follows the present `id` mapping: "0", `secp256k1`, "1", `secp256r1`, )] -Supporting other curves only requires assigning them a unique `id`.#footnote([Note that adding a curve does require `id`'s type to be updated as well, since its current type (`Bit`) is now saturated. Since each curve now claims _two_ ECALL-numbers (see below), it also consumes the reserved range twice as fast: $#`id` = 4$ would collide with `FEXT_LOAD` at $-20$.]) +Supporting other curves only requires assigning them a unique `id`.#footnote([Note that adding a curve does require `id`'s type to be updated as well, since its current type (`Bit`) is now saturated. Since each curve now claims _two_ ECALL-numbers (see below), it also consumes the reserved range twice as fast: the affine variant of $#`id` = 4$ would land on $-20$, which is `FEXT_LOAD`.]) #attention("Only " + `secp256k1` + " is instantiated.")[ The constraints below are written generically in $a$, $b$, $p$ and $N$, but only $#`id` = 0$ has ever been instantiated, and that curve has $a = 0$. @@ -132,7 +132,8 @@ On the affine variant, the two point buffers are 64 bytes wide rather than 32: $ No additional registers are consumed. Widening the buffers widens the caller's obligations, and neither is enforced by this chip. -The buffers must not overlap the scalar, since $x_G ‖ y_G$ is read at `timestamp` and $k$ at $#`timestamp` + 1$, and the memory argument cannot serve one address twice in one cycle. +The point buffers must not overlap the scalar. +This is a provability requirement rather than a soundness one: each operand is decomposed into doublewords at fixed offsets from its own base, so an overlap simply has no representation in the trace, and the `ECALL` rejects it by testing the two byte ranges directly. An operand's address must also stay clear of a $2^32$ boundary --- by 64 bytes for the two point buffers and 32 for $k$ --- because the implementation adds each per-access offset to the low half of the address alone and cannot carry into the high half. The constraints below abstract over that: they derive every address with a full 64-bit `ADD` (@ec:c:extrapolate_addr_yG, @ec:c:extrapolate_addr_yR), which carries correctly and so admits addresses the `ECALL` itself rejects.