spec: ECSM

spec/about_ecalls.typ

@@ -31,4 +31,5 @@ Negative numbers (represented as 2s complement 64-bit numbers), are used for our
 / 64: `write` (@commit)
 / 93: `exit` (@halt)
 / -1: `SHA256` (@sha256)
-/ -2: `KECCAK` (@keccak)
+/ -2: `KECCAK` (@keccak)
+/ -3: `ECSM` (@ecsm)

spec/book.typ

@@ -49,6 +49,7 @@
       ("commit.typ", [`COMMIT` chip], <commit>),
       ("sha256.typ", [`SHA256` accelerator], <sha256>),
       ("keccak.typ", [`KECCAK` accelerator], <keccak>),
+      ("ecsm.typ", [`ECSM` accelerator], <ecsm>),
     ))
   )
 )

spec/expr.typ

@@ -138,7 +138,7 @@
         cwrap(`-` + rec(PREC.neg, e.at(1)), pp < PREC.neg)
       } else {
         // Subtraction
-        cwrap(e.slice(1).map(rec.with(PREC.sub)).join(` - `), pp < PREC.sub)
+        cwrap(e.slice(1).map(rec.with(PREC.sub)).join(` - `), pp <= PREC.sub)
       }
     },
     "cast": (pp, rec, e) => {

spec/src/config.toml

@@ -132,6 +132,38 @@ desc = """\
        Represented as an array of four `Word` variables.\
        """
 
+[[variables.types]]
+label = "U256BL"
+subtypes = ["Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte"]
+desc = """\
+       Variable that can only assume values in the range $[0, 2^256)$. \\
+       Represented as an array of thirty-two `Byte` variables.\
+       """
+
+[[variables.types]]
+label = "U256HL"
+subtypes = ["Half", "Half", "Half", "Half", "Half", "Half", "Half", "Half", "Half", "Half", "Half", "Half", "Half", "Half", "Half", "Half"]
+desc = """\
+       Variable that can only assume values in the range $[0, 2^256)$. \\
+       Represented as an array of sixteen `Half` variables.\
+       """
+
+[[variables.types]]
+label = "U256WL"
+subtypes = ["Word", "Word", "Word", "Word", "Word", "Word", "Word", "Word"]
+desc = """\
+       Variable that can only assume values in the range $[0, 2^256)$. \\
+       Represented as an array of eight `Word` variables.\
+       """
+
+[[variables.types]]
+label = "U512BL"
+subtypes = ["Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte"]
+desc = """\
+       Variable that can only assume values in the range $[0, 2^512)$. \\
+       Represented as an array of sixty-four `Byte` variables.\
+       """
+
 [[variables.types]]
 label = "Timestamp"
 subtypes = ["DWordWL"]

spec/src/ec_scalar.toml

@@ -0,0 +1,117 @@
+name = "EC_SCALAR"
+
+[[variables.input]]
+name = "timestamp"
+type = "DWordWL"
+desc = "timestamp at which to serve the constant"
+pad = 0
+
+[[variables.input]]
+name = "ptr"
+type = "DWordWL"
+desc = "pointer to the first byte of the scalar"
+pad = 0
+
+[[variables.input]]
+name = "offset"
+type = "Byte"
+desc = "index of limb"
+pad = 0
+
+[[variables.auxiliary]]
+name = "limb_bits"
+type = ["Bit", 8]
+desc = "bit-decomposition of the limb being read"
+pad = ["arr", 0, 0, 0, 0, 0, 0, 0, 0]
+
+[[variables.auxiliary]]
+name = "last_limb"
+type = "Bit"
+desc = "whether this is the last limb to read"
+pad = 0
+
+[[variables.virtual]]
+name = "limb"
+type = "Byte"
+desc = "limb being read"
+def = {poly=["sum", ["=", "i", 0], 7, ["*", ["^", 2, "i"], ["idx", "limb_bits", "i"]]]}
+
+[[variables.multiplicity]]
+name = "μ"
+type = "Bit"
+desc = ""
+pad = 0
+
+[[assumptions]]
+desc = "$#`ptr` + #`offset`$ does not overflow the bottom limb"
+
+[[constraint_groups]]
+name = "recv"
+
+[[constraints.recv]]
+kind = "interaction"
+tag = "SERVE_K"
+input = ["timestamp", "ptr", "offset"]
+multiplicity = ["-", "μ"]
+
+[[constraints.recv]]
+kind = "template"
+tag = "IS_BIT"
+input = ["μ"]
+
+[[constraint_groups]]
+name = "read"
+
+[[constraints.read]]
+kind = "interaction"
+tag = "MEMW"
+input = [0, ["+", "ptr", ["arr", ["cast", "offset", "Word"], 0]], ["arr", "limb", 0, 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], 0, 0, 0]
+output = ["arr", "limb", 0, 0, 0, 0, 0, 0, 0]
+multiplicity = "μ"
+
+[[constraints.read]]
+kind = "template"
+tag = "IS_BIT"
+input = [["idx", "limb_bits", "i"]]
+iter = ["i", 0, 7]
+
+
+[[constraint_groups]]
+name = "serve"
+
+[[constraints.serve]]
+kind = "interaction"
+tag = "BIT"
+input = ["timestamp", ["+", ["*", 8, "offset"], "i"]]
+iter = ["i", 0, 7]
+multiplicity = ["idx", "limb_bits", "i"]
+
+[[constraints.serve]]
+kind = "arith"
+constraint = "$#`limb_bits`_i = 1 => #`μ` = 1$"
+poly = ["*", ["idx", "limb_bits", "i"], ["not", "μ"]]
+iter = ["i", 0, 7]
+
+[[constraint_groups]]
+name = "recurse"
+
+[[constraints.recurse]]
+kind = "template"
+tag = "IS_BIT"
+input = ["last_limb"]
+
+[[constraints.recurse]]
+kind = "arith"
+constraint = "$#`last_limb` = 1 => #`μ` = 1$"
+poly = ["*", "last_limb", ["not", "μ"]]
+
+[[constraints.recurse]]
+kind = "arith"
+constraint = "$#`last_limb` = 1 => #`offset` = 0$"
+poly = ["*", "last_limb", "offset"]
+
+[[constraints.recurse]]
+kind = "interaction"
+tag = "SERVE_K"
+input = ["timestamp", "ptr", ["-", "offset", 1]]
+multiplicity = ["-", "μ", "last_limb"]