spec: ADD template

spec/add.typ

@@ -0,0 +1,48 @@
+#import "/book.typ": book-page, et
+#import "/src.typ": load_config, load_chip
+#import "/chip.typ": render_chip_column_table, render_chip_assumptions, render_constraint_table
+
+#show: book-page.with(title: "ADD/SUB")
+
+#let config = load_config()
+#let chip = load_chip("src/add.toml", config)
+
+#let add = raw(chip.name)
+
+#let highlighted_code(code) = {
+  box(
+    inset: (left: 4pt, right: 4pt), 
+    outset: (top: 4pt, bottom: 4pt), 
+    radius: 2pt,
+    fill: luma(230), 
+    raw(code))
+}
+
+= #add template
+#add is a constraint template that is used to assert that $#`sum` = #`lhs` + #`rhs` mod 2^64$, under the condition that `cond` is non-zero.
+
+== Notation
+The #add constraint template has the following interface:
+#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => ADD<sum; lhs, rhs>"))
+where `cond` is any value described by an expression _of degree at most $1$_.
+#highlighted_code("ADD<sum; lhs, rhs>") can be used to denote the _unconditional_ application of the #add template to `lhs`, `rhs`, and `sum`.
+
+#let sub = raw("SUB")
+=== #sub
+For ease of notation, we moreover introduce the #sub constraint template.
+Its interface
+#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => SUB<diff; lhs, rhs>"))
+maps onto the #add template as 
+#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => ADD<lhs; rhs, diff>"))
+It constrains that $#`diff` = #`lhs` - #`rhs` mod 2^64$ when the expression `cond` is non-zero.
+As with #add, #highlighted_code("SUB<diff; lhs, rhs>") can be used to denote the _unconditional_ application of the template.
+
+== Variables
+#render_chip_column_table(chip, config)
+
+== Assumptions
+#render_chip_assumptions(chip, config)
+
+== Constraints
+This template introduces the following constraints
+#render_constraint_table(chip, config)

spec/book.typ

@@ -7,6 +7,7 @@
   summary: [
     #chapter("variables.typ")[Variables]
     #chapter("is_bit.typ")[IS_BIT template]
+    #chapter("add.typ")[ADD template]
     #chapter("cpu.typ")[CPU chip]
   ]
 )

spec/src/add.toml

@@ -0,0 +1,64 @@
+name = "ADD"
+
+# Variables
+
+[[variables.condition]]
+name = "cond"
+type = "BaseField"
+desc = "Whether the relation should be enforced ($eq.not 0$) or not ($0$)."
+
+[[variables.input]]
+name = "lhs"
+type = "DWordWL"
+desc = "left-hand operator"
+
+[[variables.input]]
+name = "rhs"
+type = "DWordWL"
+desc = "right-hand operator"
+
+[[variables.output]]
+name = "sum"
+type = "DWordWL"
+desc = "$#`lhs` + #`rhs`$"
+
+[[variables.virtual]]
+name = "carry"
+desc = "Carry values used to constrain the addition"
+type = ["Bit", 2]
+def = {idx="i", polys=[
+    {range=0, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "lhs", 0], ["idx", "rhs", 0]], ["idx", "sum", 0]]]},
+    {range=1, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "lhs", 1], ["idx", "rhs", 1], ["idx", "carry", 0]], ["idx", "sum", 1]]]},
+]}
+
+
+# Assumptions
+
+[[assumptions]]
+desc = "`IS_WORD[lhs[i]]`"
+range = ["i", 0, 1]
+ref = "add:a:lhs"
+
+[[assumptions]]
+desc = "`IS_WORD[rhs[i]]`"
+range = ["i", 0, 1]
+ref = "add:a:rhs"
+
+[[assumptions]]
+desc = "`IS_WORD[sum[i]]`"
+range = ["i", 0, 1]
+ref = "add:a:sum"
+
+# Constraints
+
+[[constraint_groups]]
+name = "all"
+
+[[constraints.all]]
+kind = "template"
+tag = "IS_BIT"
+input = [["idx", "carry", "i"]]
+range = ["i", 0, 1]
+cond = "cond"
+ref = "add:c:carry"
+