spec: NEG template

spec/book.typ

@@ -11,6 +11,7 @@
     ("variables.typ", [Variables], <vars>),
     ("is_bit.typ", [IS_BIT template], <isbit>),
     ("add.typ", [ADD/SUB template], <add>),
+    ("neg.typ", [NEG template], <neg>),
     ("decode.typ", [DECODE table], <decode>),
     ("cpu.typ", [CPU chip], <cpu>),
     ("shift.typ", [SHIFT chip], <shift>),

spec/expr.typ

@@ -92,7 +92,7 @@
 #let expr_to_code = make_expr_formatter(
   (
     "idx": (pp, rec, e) => rec(PREC.MIN, e.at(1)) + `[` + rec(PREC.MAX, e.at(2)) + `]`,
-    "not": (pp, rec, e) => cwrap(`1 - ` + rec(PREC.not, e.at(1)), pp < PREC.not),
+    "not": (pp, rec, e) => cwrap(rec(PREC.not, 1) + ` - ` + rec(PREC.not, e.at(1)), pp < PREC.not),
     "+": (pp, rec, e) => cwrap(e.slice(1).map(rec.with(PREC.add)).join(` + `), pp < PREC.add),
     "sum": (pp, rec, e) => assert(false, message: "sum is unsupported in code."),
     "*": (pp, rec, e) => {
@@ -153,7 +153,7 @@
       let (val, idxs) = flat_idxs(e)
       $#rec(PREC.idx, val)_(#idxs.map(idx => rec(PREC.idx, idx)).join($, $))$
     },
-    "not": (pp, rec, e) => mwrap($1 - #rec(PREC.not, e.at(1))$, pp < PREC.not),
+    "not": (pp, rec, e) => mwrap(rec(PREC.not, 1) + $ - #rec(PREC.not, e.at(1))$, pp < PREC.not),
     "+": (pp, rec, e) => mwrap($#e.slice(1).map(rec.with(PREC.add)).join($+$)$, pp < PREC.add),
     "sum": (pp, rec, e) => {
       assert(e.len() == 4, message: "invalid sum:" + repr(e))

spec/neg.typ

@@ -0,0 +1,78 @@
+#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
+
+#let config = load_config()
+#let chip = load_chip("src/neg.toml", config)
+#show: book-page(chip.name)
+
+#let neg = 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))
+}
+
+#neg is a constraint template that is used to assert that $#`neg` = -#`x`$, under the condition that `cond` is non-zero.
+
+== Notation
+The #neg constraint template has the following interface:
+#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => NEG<neg; x>"))
+where `cond` is a bit value (i.e., lies in ${0, 1}$)  described by an expression _of degree at most $1$_.
+#highlighted_code("NEG<neg; x>") can be used to denote the _unconditional_ application of the #neg template to `x` and `neg` (which is equivalent to $#`cond` = 1$).
+
+== Variables
+#render_chip_column_table(chip, config)
+
+== Assumptions
+#render_chip_assumptions(chip, config)
+
+== Constraints
+We constrain this equality using two constraints:
+#render_constraint_table(chip, config)
+The constraints force the `carry` values to be fixed.
+Writing `carry`'s definition, we then find that
+$
+  #`neg`_0 &= 2^32 dot #`carry`_0 - (#`x as DWordWL`)_0
+ = cases(
+  2^32 - (#`x as DWordWL`)_0 & "if" (#`x as DWordWL`)_0 != 0,
+  0 & "if" (#`x as DWordWL`)_0 = 0
+ ),\
+  #`neg`_1 &= 2^32 dot #`carry`_1 - (#`x as DWordWL`)_1 - #`carry`_0 = cases(
+  2^32 - (#`x as DWordWL`)_1 - 1 & "if" #`x` != 0,
+  0 & "if" #`x` = 0
+ )
+$
+Clearly, $#`neg` = 0$ when $#`x` = 0$ (and `cond` is set).
+For non-zero `x`, we distinguish two cases.
+When $(#`x as DWordWL`)_0 = 0$,
+$
+  #`neg` 
+  &= 2^32 dot #`neg`_1 + #`neg`_0\
+  &= 2^32 dot (2^32 - (#`x as DWordWL`)_1) + 0\
+  &= 2^32 dot (2^32 - (#`x as DWordWL`)_1) + (#`x as DWordWL`)_0\
+  &= 2^64 - (2^32 dot (#`x as DWordWL`)_1 + (#`x as DWordWL`)_0)\
+  &= 2^64 - #`x`\
+  &equiv -x mod 2^64,
+$
+while when $(#`x as DWordWL`)_0 != 0$,
+$
+  #`neg` 
+  &= 2^32 dot #`neg`_1 + #`neg`_0\
+  &= 2^32 dot (2^32 - (#`x as DWordWL`)_1 - 1) + (2^32 - (#`x as DWordWL`)_0)  \
+  &= 2^64 - 2^32 dot (#`x as DWordWL`)_1 - 2^32 + 2^32 - (#`x as DWordWL`)_0  \
+  &= 2^64 - ((#`x as DWordWL`)_0 + 2^32 dot (#`x as DWordWL`)_1) \
+  &= 2^64 - #`x`\
+  &equiv -x mod 2^64
+$
+when `cond` is set.
+When `cond` is not set, the two lookups are not executed, allowing `neg` to take any value in either case.
+
+== Note
+It is worth noting that this construction does _not_ require the limbs of `neg` to be range checked, 
+thus allowing it be represented by the unrangecheckable `DWordWL` rather than a `DWordHL`.
+The input value `x` is still assumed to be range-checked, however.

spec/src/neg.toml

@@ -0,0 +1,53 @@
+name = "NEG"
+
+[[variables.condition]]
+name = "cond"
+type = "Bit"
+desc = "condition on whether to negate x"
+
+[[variables.input]]
+name = "x"
+type = "DWordHL"
+desc = "value to compute negation of"
+
+[[variables.output]]
+name = "neg"
+type = "DWordWL"
+desc = "negation of `x` if $#`cond` != 0$; unconstrained otherwise."
+
+[[variables.virtual]]
+name = "carry"
+type = ["Bit", 2]
+desc = "carries of the addition $#`neg` + #`x`$."
+def = {idx="i", polys=[
+    {iter=0, poly=["*", ["^", 2, -32], ["+", ["idx", ["cast", "x", "DWordWL"], 0], ["idx", "neg", 0]]]},
+    {iter=1, poly=["*", ["^", 2, -32], ["+", ["idx", ["cast", "x", "DWordWL"], 1], ["idx", "neg", 1], ["idx", "carry", 0]]]}
+]}
+
+
+[[assumptions]]
+desc = "`IS_HALF[x[i]]`"
+iter = ["i", 0, 3]
+
+[[assumptions]]
+desc = "`IS_BIT<cond>`"
+
+
+[[constraint_groups]]
+name = "all"
+
+[[constraints.all]]
+kind = "interaction"
+tag = "ZERO"
+input = [["+", ["idx", "x", 0], ["idx", "x", 1]]]
+output = ["not", ["idx", "carry", 0]]
+multiplicity = "cond"
+ref = "neg:c:carry_0"
+
+[[constraints.all]]
+kind = "interaction"
+tag = "ZERO"
+input = [["+", ["idx", "x", 0], ["idx", "x", 1], ["idx", "x", 2], ["idx", "x", 3]]]
+output = ["not", ["idx", "carry", 1]]
+multiplicity = "cond"
+ref = "neg:c:carry_1"