From e3f0920866006c60f02cd4eb26a579e9a563f5ef Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Sat, 3 Jan 2026 14:44:00 +0100 Subject: [PATCH 1/6] spec: ADD draft --- spec/add.typ | 38 ++++++++++++++++++++++++++++ spec/book.typ | 1 + spec/src/add.toml | 64 +++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 103 insertions(+) create mode 100644 spec/add.typ create mode 100644 spec/src/add.toml diff --git a/spec/add.typ b/spec/add.typ new file mode 100644 index 000000000..32bf3467f --- /dev/null +++ b/spec/add.typ @@ -0,0 +1,38 @@ +#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 the variable `sum` is the sum of the variables `lhs` and `rhs`, 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")) +where `cond` is any value described by an expression _of degree at most $1$_. +Note that #highlighted_code("ADD") can be used to denote the _unconditional_ application of the #add template to `lhs`, `rhs`, and `sum`. + +== 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) diff --git a/spec/book.typ b/spec/book.typ index dcf1d0c1b..6717198ed 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -8,6 +8,7 @@ summary: [ #chapter("variables.typ")[Variables] #chapter("is_bit.typ")[IS_BIT template] + #chapter("add.typ")[ADD template] ] ) diff --git a/spec/src/add.toml b/spec/src/add.toml new file mode 100644 index 000000000..a37ef2a64 --- /dev/null +++ b/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", 4] +def = {idx="i", polys=[ + {range=0, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "lhs", 0], ["idx", "rhs", 0]], ["idx", "sum", 0]]]}, + {range=[1, 3], poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "lhs", "i"], ["idx", "rhs", "i"], ["idx", "carry", ["-", "i", 1]]], ["idx", "sum", "i"]]]}, +]} + + +# Assumptions + +[[assumptions]] +desc = "`IS_WORD[lhs[i]]`" +range = ["i", 0, 3] +ref = "add:a:lhs" + +[[assumptions]] +desc = "`IS_WORD[rhs[i]]`" +range = ["i", 0, 3] +ref = "add:a:rhs" + +[[assumptions]] +desc = "`IS_WORD[sum[i]]`" +range = ["i", 0, 3] +ref = "add:a:sum" + +# Constraints + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "template" +tag = "IS_BIT" +input = [["idx", "carry", "i"]] +range = ["i", 0, 3] +cond = "cond" +ref = "add:c:carry" + From e6a254532023e25b4f4bccdc5175aeb2d68fe0c5 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 5 Jan 2026 15:45:46 +0100 Subject: [PATCH 2/6] spec: ADD: fix `carry` size --- spec/src/add.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/src/add.toml b/spec/src/add.toml index a37ef2a64..535c9918c 100644 --- a/spec/src/add.toml +++ b/spec/src/add.toml @@ -25,10 +25,10 @@ desc = "$#`lhs` + #`rhs`$" [[variables.virtual]] name = "carry" desc = "Carry values used to constrain the addition" -type = ["Bit", 4] +type = ["Bit", 2] def = {idx="i", polys=[ {range=0, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "lhs", 0], ["idx", "rhs", 0]], ["idx", "sum", 0]]]}, - {range=[1, 3], poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "lhs", "i"], ["idx", "rhs", "i"], ["idx", "carry", ["-", "i", 1]]], ["idx", "sum", "i"]]]}, + {range=1, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "lhs", 1], ["idx", "rhs", 1], ["idx", "carry", 0]], ["idx", "sum", 1]]]}, ]} From af5c41dda90cba25137e4965a2cecb844d6b5651 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 5 Jan 2026 15:47:52 +0100 Subject: [PATCH 3/6] spec: ADD: clarify sum is mod 2^64 --- spec/add.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/add.typ b/spec/add.typ index 32bf3467f..15bfda9fe 100644 --- a/spec/add.typ +++ b/spec/add.typ @@ -19,7 +19,7 @@ } = #add template -#add is a constraint template that is used to assert that the variable `sum` is the sum of the variables `lhs` and `rhs`, under the condition that `cond` is non-zero. +#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: From 424d4db294e6ecfa6742cd9d8c705dbcf6774c97 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 8 Jan 2026 12:13:54 +0100 Subject: [PATCH 4/6] spec: introduce `SUB` template notation. --- spec/add.typ | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/spec/add.typ b/spec/add.typ index 15bfda9fe..45fa7bdde 100644 --- a/spec/add.typ +++ b/spec/add.typ @@ -27,6 +27,16 @@ The #add constraint template has the following interface: where `cond` is any value described by an expression _of degree at most $1$_. Note that #highlighted_code("ADD") 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. +It's interface +#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => SUB")) +maps onto the #add template as +#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => ADD")) +It constrains that $#`diff` = #`lhs` - #`rhs` mod 2^64$ when the expression `cond` is non-zero. +As with #add, #highlighted_code("SUB") can be used to denote the _unconditional_ application of the template. + == Variables #render_chip_column_table(chip, config) From ddb9183b4f0e8e56a15a1cf33d2dc66ad9c788fc Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Fri, 9 Jan 2026 09:14:44 +0100 Subject: [PATCH 5/6] Fix assumption indices Co-authored-by: Robin Jadoul --- spec/src/add.toml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/spec/src/add.toml b/spec/src/add.toml index 535c9918c..a0ccf6942 100644 --- a/spec/src/add.toml +++ b/spec/src/add.toml @@ -36,17 +36,17 @@ def = {idx="i", polys=[ [[assumptions]] desc = "`IS_WORD[lhs[i]]`" -range = ["i", 0, 3] +range = ["i", 0, 1] ref = "add:a:lhs" [[assumptions]] desc = "`IS_WORD[rhs[i]]`" -range = ["i", 0, 3] +range = ["i", 0, 1] ref = "add:a:rhs" [[assumptions]] desc = "`IS_WORD[sum[i]]`" -range = ["i", 0, 3] +range = ["i", 0, 1] ref = "add:a:sum" # Constraints @@ -58,7 +58,7 @@ name = "all" kind = "template" tag = "IS_BIT" input = [["idx", "carry", "i"]] -range = ["i", 0, 3] +range = ["i", 0, 1] cond = "cond" ref = "add:c:carry" From 9de2bb224a981d5a543e853570cc5d4b1fd6f735 Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Fri, 9 Jan 2026 09:15:52 +0100 Subject: [PATCH 6/6] Fix typos Co-authored-by: Robin Jadoul --- spec/add.typ | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/add.typ b/spec/add.typ index 45fa7bdde..0dade7b01 100644 --- a/spec/add.typ +++ b/spec/add.typ @@ -25,12 +25,12 @@ The #add constraint template has the following interface: #block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => ADD")) where `cond` is any value described by an expression _of degree at most $1$_. -Note that #highlighted_code("ADD") can be used to denote the _unconditional_ application of the #add template to `lhs`, `rhs`, and `sum`. +#highlighted_code("ADD") 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. -It's interface +Its interface #block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => SUB")) maps onto the #add template as #block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => ADD"))