From 801f5ee95159b8e7c5401b457cc7d44f53d826ee Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 2 Feb 2026 11:25:24 +0100 Subject: [PATCH 1/9] spec: tweak code-rendering "not" --- spec/expr.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/expr.typ b/spec/expr.typ index a0530525b..0e41069da 100644 --- a/spec/expr.typ +++ b/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) => { From 70a8a2cd5df94b3df6667e763fb245189eb836ac Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 2 Feb 2026 11:42:28 +0100 Subject: [PATCH 2/9] spec: introduce NEG template --- spec/book.typ | 1 + spec/neg.typ | 48 +++++++++++++++++++++++++++++++++++++++++++ spec/src/neg.toml | 52 +++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 101 insertions(+) create mode 100644 spec/neg.typ create mode 100644 spec/src/neg.toml diff --git a/spec/book.typ b/spec/book.typ index b194b7f70..cf07e6498 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -11,6 +11,7 @@ ("variables.typ", [Variables], ), ("is_bit.typ", [IS_BIT template], ), ("add.typ", [ADD/SUB template], ), + ("neg.typ", [NEG template], ), ("decode.typ", [DECODE table], ), ("cpu.typ", [CPU chip], ), ("shift.typ", [SHIFT chip], ), diff --git a/spec/neg.typ b/spec/neg.typ new file mode 100644 index 000000000..5dac7512f --- /dev/null +++ b/spec/neg.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 + +#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")) +where `cond` is a bit value (i.e., lies in ${0, 1}$) described by an expression _of degree at most $1$_. +#highlighted_code("NEG") 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 +For `neg` to equal $-#`x`$, both values must add to $0 mod 2^64$. +Zooming in on the addition, we find that the carry values of adding the limbs must both equal to $1$, except when $#`x` = 0$, in which case they should both be $0$. + +To this end, we require $#`carry`_0$ is $1$, unless $#`x` = 0$ (@neg:c:carry) and +that both limbs of `carry` are identical (@neg:c:identical_carry ensuring). +Of course, both constraints are conditional on $#`cond` = 1$. +Lastly, note that this @neg:c:carry implicitly enforces that $#`carry`_0 in {0, 1}$, while @neg:c:identical_carry ensures $#`carry`_1$ must also be binary. + +#render_constraint_table(chip, config) + +== 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. diff --git a/spec/src/neg.toml b/spec/src/neg.toml new file mode 100644 index 000000000..1d86664f2 --- /dev/null +++ b/spec/src/neg.toml @@ -0,0 +1,52 @@ +name = "NEG" + +[[variables.input]] +name = "x" +type = "DWordWL" +desc = "value to compute negation of" + +[[variables.input]] +name = "cond" +type = "BaseField" +desc = "condition on whether to negate x" + +[[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", "x", 0], ["idx", "neg", 0]]]}, + {iter=1, poly=["*", ["^", 2, -32], ["+", ["idx", "x", 1], ["idx", "neg", 1], ["idx", "carry", 0]]]} +]} + + +[[assumptions]] +desc = "`IS_WORD[x[i]]`" +iter = ["i", 0, 1] + +[[assumptions]] +desc = "`IS_BIT`" + + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "arith" +constraint = "$#`cond` => #`carry`_0 = #`carry`_1$" +poly = ["*", "cond", ["-", ["idx", "carry", 0], ["idx", "carry", 1]]] +ref = "neg:c:identical_carry" + +[[constraints.all]] +kind = "template" +tag = "IsZero" +input = [["+", ["idx", "x", 0], ["idx", "x", 1]]] +output = ["not", ["idx", "carry", 0]] +multiplicity = "cond" +ref = "neg:c:carry" + From 8bd326091a1b3b2543afb8162248d5f59bfc0964 Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Mon, 2 Feb 2026 13:45:40 +0100 Subject: [PATCH 3/9] Update spec/book.typ Co-authored-by: greptile-apps[bot] <165735046+greptile-apps[bot]@users.noreply.github.com> --- spec/book.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/book.typ b/spec/book.typ index cf07e6498..fba5477b7 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -11,7 +11,7 @@ ("variables.typ", [Variables], ), ("is_bit.typ", [IS_BIT template], ), ("add.typ", [ADD/SUB template], ), - ("neg.typ", [NEG template], ), + ("neg.typ", [NEG template], ), ("decode.typ", [DECODE table], ), ("cpu.typ", [CPU chip], ), ("shift.typ", [SHIFT chip], ), From f53f6c9a7279202fc751d77a6a68fc78f5957d94 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 2 Feb 2026 16:48:25 +0100 Subject: [PATCH 4/9] spec: update NEG --- spec/neg.typ | 8 +------- spec/src/neg.toml | 25 +++++++++++++------------ 2 files changed, 14 insertions(+), 19 deletions(-) diff --git a/spec/neg.typ b/spec/neg.typ index 5dac7512f..e5b65ee19 100644 --- a/spec/neg.typ +++ b/spec/neg.typ @@ -33,13 +33,7 @@ where `cond` is a bit value (i.e., lies in ${0, 1}$) described by an expression == Constraints For `neg` to equal $-#`x`$, both values must add to $0 mod 2^64$. -Zooming in on the addition, we find that the carry values of adding the limbs must both equal to $1$, except when $#`x` = 0$, in which case they should both be $0$. - -To this end, we require $#`carry`_0$ is $1$, unless $#`x` = 0$ (@neg:c:carry) and -that both limbs of `carry` are identical (@neg:c:identical_carry ensuring). -Of course, both constraints are conditional on $#`cond` = 1$. -Lastly, note that this @neg:c:carry implicitly enforces that $#`carry`_0 in {0, 1}$, while @neg:c:identical_carry ensures $#`carry`_1$ must also be binary. - +This is constrained through the following: #render_constraint_table(chip, config) == Note diff --git a/spec/src/neg.toml b/spec/src/neg.toml index 1d86664f2..e99456ba2 100644 --- a/spec/src/neg.toml +++ b/spec/src/neg.toml @@ -2,7 +2,7 @@ name = "NEG" [[variables.input]] name = "x" -type = "DWordWL" +type = "DWordHL" desc = "value to compute negation of" [[variables.input]] @@ -20,8 +20,8 @@ name = "carry" type = ["Bit", 2] desc = "carries of the addition $#`neg` + #`x`$." def = {idx="i", polys=[ - {iter=0, poly=["*", ["^", 2, -32], ["+", ["idx", "x", 0], ["idx", "neg", 0]]]}, - {iter=1, poly=["*", ["^", 2, -32], ["+", ["idx", "x", 1], ["idx", "neg", 1], ["idx", "carry", 0]]]} + {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]]]} ]} @@ -37,16 +37,17 @@ desc = "`IS_BIT`" name = "all" [[constraints.all]] -kind = "arith" -constraint = "$#`cond` => #`carry`_0 = #`carry`_1$" -poly = ["*", "cond", ["-", ["idx", "carry", 0], ["idx", "carry", 1]]] -ref = "neg:c:identical_carry" - -[[constraints.all]] -kind = "template" -tag = "IsZero" +kind = "interaction" +tag = "ZERO" input = [["+", ["idx", "x", 0], ["idx", "x", 1]]] output = ["not", ["idx", "carry", 0]] multiplicity = "cond" -ref = "neg:c:carry" +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" From ac9d65dfa6d7716b7c0208f40b98ebbb726f12d2 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 3 Feb 2026 16:30:57 +0100 Subject: [PATCH 5/9] spec: NEG: refactor --- spec/neg.typ | 28 ++++++++++++++++++++++++++-- 1 file changed, 26 insertions(+), 2 deletions(-) diff --git a/spec/neg.typ b/spec/neg.typ index e5b65ee19..dcca84d5e 100644 --- a/spec/neg.typ +++ b/spec/neg.typ @@ -32,9 +32,33 @@ where `cond` is a bit value (i.e., lies in ${0, 1}$) described by an expression #render_chip_assumptions(chip, config) == Constraints -For `neg` to equal $-#`x`$, both values must add to $0 mod 2^64$. -This is constrained through the following: +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`, it holds that +$ + #`neg` + &= #`neg`_0 + 2^32 dot #`neg`_1 \ + &= (2^32 - (#`x as DWordWL`)_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^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. == Note It is worth noting that this construction does _not_ require the limbs of `neg` to be range checked, From b072055fc2133cde372179330d9bd577e606dd93 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 4 Feb 2026 14:26:53 +0100 Subject: [PATCH 6/9] spec: NEG: fix range-assumption on x --- spec/src/neg.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/src/neg.toml b/spec/src/neg.toml index e99456ba2..6b29e25f4 100644 --- a/spec/src/neg.toml +++ b/spec/src/neg.toml @@ -26,8 +26,8 @@ def = {idx="i", polys=[ [[assumptions]] -desc = "`IS_WORD[x[i]]`" -iter = ["i", 0, 1] +desc = "`IS_HALF[x[i]]`" +iter = ["i", 0, 3] [[assumptions]] desc = "`IS_BIT`" From a5455577f9b5a1d6af9b204718ef9bd7a55e0ed5 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 4 Feb 2026 14:28:21 +0100 Subject: [PATCH 7/9] spec: NEG: update cond --- spec/src/neg.toml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/spec/src/neg.toml b/spec/src/neg.toml index 6b29e25f4..2cd70f354 100644 --- a/spec/src/neg.toml +++ b/spec/src/neg.toml @@ -1,15 +1,15 @@ 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.input]] -name = "cond" -type = "BaseField" -desc = "condition on whether to negate x" - [[variables.output]] name = "neg" type = "DWordWL" From e4eb03d2803894ab35050e6e02a3706742cbeb4e Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 4 Feb 2026 14:32:40 +0100 Subject: [PATCH 8/9] spec: tweak math-rendering "not" Analogous to 801f5ee9 --- spec/expr.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/expr.typ b/spec/expr.typ index 0e41069da..1c6c7942e 100644 --- a/spec/expr.typ +++ b/spec/expr.typ @@ -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)) From dfa328cb0d46a825c36bfd13a93ced3cbadc09f9 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 4 Feb 2026 15:03:51 +0100 Subject: [PATCH 9/9] spec: NEG: add non-zero x case distinction --- spec/neg.typ | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/spec/neg.typ b/spec/neg.typ index dcca84d5e..b687e7333 100644 --- a/spec/neg.typ +++ b/spec/neg.typ @@ -47,18 +47,30 @@ $ 0 & "if" #`x` = 0 ) $ -Clearly, $#`neg` = 0$ when $#`x` = 0$ (and `cond` is set); for non-zero `x`, it holds that +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` - &= #`neg`_0 + 2^32 dot #`neg`_1 \ - &= (2^32 - (#`x as DWordWL`)_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 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. +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,