From 65b38403ad256c442d7568e41ad4245d58b0f68d Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 24 Dec 2025 15:05:22 +0100 Subject: [PATCH 01/10] spec: Introduce LT chip --- spec/book.typ | 1 + spec/lt.typ | 38 +++++++++++ spec/src/lt.toml | 162 +++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 201 insertions(+) create mode 100644 spec/lt.typ create mode 100644 spec/src/lt.toml diff --git a/spec/book.typ b/spec/book.typ index af747c88c..7787acbce 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -9,6 +9,7 @@ #chapter("is_bit.typ")[IS_BIT template] #chapter("cpu.typ")[CPU chip] #chapter("branch.typ")[BRANCH] + #chapter("lt.typ")[LT], ] ) diff --git a/spec/lt.typ b/spec/lt.typ new file mode 100644 index 000000000..1afb4f434 --- /dev/null +++ b/spec/lt.typ @@ -0,0 +1,38 @@ +#import "/book.typ": book-page +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_assumptions, + render_chip_column_table, + total_nr_variables, + total_nr_instantiated_columns, + render_constraint_table, +) + +#let config = load_config() +#let chip = load_chip("src/lt.toml", config) + +#show: book-page.with(title: "LT chip") + +== Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) + +The `LT` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: +#render_chip_column_table(chip, config) + +== Assumptions +We assume the inputs `lhs`, `rhs` and `signed` are appropriately range checked. +#render_chip_assumptions(chip, config) + +== Constraints +We first constrain that all variables correspond to their definition. + +#render_constraint_table(chip, config, groups: "defs") + +And then we constrain the subtraction. + +#render_constraint_table(chip, config, groups: "sub") + +The chip contributes the following to the lookup argument. + +#render_constraint_table(chip, config, groups: "output") diff --git a/spec/src/lt.toml b/spec/src/lt.toml new file mode 100644 index 000000000..a355eca35 --- /dev/null +++ b/spec/src/lt.toml @@ -0,0 +1,162 @@ +name = "LT" + + +# Input + +[[variables.input]] +name = "lhs" +type = "DWordHHW" +desc = "The left operand" + +[[variables.input]] +name = "rhs" +type = "DWordHHW" +desc = "The right operand" + +[[variables.input]] +name = "signed" +type = "Bit" +desc = "whether to interpret `lhs` and `rhs` as signed integers" + +# Output + +[[variables.output]] +name = "lt" +type = "Bit" +desc = "Whether $#`lhs` < #`rhs`$, taking `signed` into account" + + +# Auxiliary + +[[variables.auxiliary]] +name = "signed_lt" +type = "Bit" +desc = "Whether $#`lhs` < #`rhs`$, as signed integers" + +[[variables.auxiliary]] +name = "lhs_sub_rhs" +type = "DWordHL" +desc = "$#`lhs` - #`rhs`$" + +[[variables.auxiliary]] +name = "lhs_msb" +type = "Bit" +desc = "The most significant bit of `lhs`" + +[[variables.auxiliary]] +name = "rhs_msb" +type = "Bit" +desc = "The most significant bit of `rhs`" + +[[variables.auxiliary]] +name = "lhs_sub_rhs_msb" +type = "Bit" +desc = "The most significant bit of $#`lhs` - #`rhs`$" + + +# Virtual + +[[variables.virtual]] +name = "carry" +type = "Bit[3]" +desc = "The carry of subtracting limbs of `rhs` from those of `lhs`" +polys = [ + ["/", ["-", ["+", ["idx", "rhs", 0], ["idx", "lhs_sub_rhs", 0]], ["idx", "lhs", 0]], ["^", 2, 32]], + ["/", ["-", ["+", ["idx", "rhs", 1], ["idx", "lhs_sub_rhs", 1], ["idx", "carry", 0]], ["idx", "lhs", 1]], ["^", 2, 16]], + ["/", ["-", ["+", ["idx", "rhs", 2], ["idx", "lhs_sub_rhs", 2], ["idx", "carry", 1]], ["idx", "lhs", 2]], ["^", 2, 16]] +] + +[[variables.virtual]] +name = "unsigned_lt" +type = "Bit" +desc = "Whether $#`lhs` < #`rhs`$, as unsigned integers" +poly = ["idx", "carry", 2] + + +# Multiplicity + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" + + +[[assumptions]] +desc = "`IS_HALFWORD[lhs[i]]` and `IS_WORD[lhs[0]]`" +range = ["i", 1, 2] +ref = "lt:a:range_lhs" + +[[assumptions]] +desc = "`IS_HALFWORD[rhs[i]]` and `IS_WORD[rhs[0]]`" +range = ["i", 1, 2] +ref = "lt:a:range_rhs" + +[[assumptions]] +desc = "`IS_BIT[signed]`" +ref = "lt:a:range_signed" + + +[[constraint_groups]] +name = "defs" +desc = "Enforce that variables have been correctly computed" + +[[constraints.defs]] +kind = "interaction" +tag = "MSB16" +input = [["idx", "lhs", 2]] +output = "lhs_msb" +multiplicity = "μ" +ref = "lt:c:lhs_msb" + +[[constraints.defs]] +kind = "interaction" +tag = "MSB16" +input = [["idx", "rhs", 2]] +output = "rhs_msb" +multiplicity = "μ" +ref = "lt:c:rhs_msb" + +[[constraints.defs]] +kind = "interaction" +tag = "MSB16" +input = [["idx", "lsb_sub_rhs", 2]] +output = "lhs_sub_rhs_msb" +multiplicity = "μ" +ref = "lt:c:lhs_sub_rhs_msb" + +[[constraints.defs]] +kind = "arith" +constraint = "$#`lt` = #`signed` dot #`signed_lt` + (1 - #`signed`) dot #`unsigned_lt`$" +desc = "where some shorthand means something" +poly = ["+", ["-", "lt"], ["*", "signed", "signed_lt"], ["*", ["-", 1, "signed"], "unsigned_lt"]] + + +[[constraint_groups]] +name = "sub" +desc = "Constrain the subtraction" + +[[constraints.sub]] +kind = "template" +tag = "IS_BIT" +input = [["idx", "carry", "i"]] +range = ["i", 0, 1] + +[[constraints.sub]] +kind = "interaction" +tag = "IS_HALFWORD" +input = [["idx", "lhs_sub_rhs", "i"]] +range = ["i", 0, 3] +multiplicity = "μ" +ref = "lt:c:lhs_sub_rhs_range" + + +[[constraint_groups]] +name = "output" +desc = "Each row contributes the following to the LogUp sum" + +[[constraints.output]] +kind = "interaction" +tag = "LT" +input = ["lhs", "rhs", "signed"] +output = "lt" +multiplicity = "-μ" From b69ca492dffe6ebdea45a002d798da93323473fd Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 2 Jan 2026 10:40:02 +0100 Subject: [PATCH 02/10] Address review comments Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/src/lt.toml | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/spec/src/lt.toml b/spec/src/lt.toml index a355eca35..cdec3a835 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -16,7 +16,7 @@ desc = "The right operand" [[variables.input]] name = "signed" type = "Bit" -desc = "whether to interpret `lhs` and `rhs` as signed integers" +desc = "whether to interpret `lhs` and `rhs` as signed integers (1) or not (0)" # Output @@ -58,12 +58,12 @@ desc = "The most significant bit of $#`lhs` - #`rhs`$" [[variables.virtual]] name = "carry" -type = "Bit[3]" +type = ["Bit", 3] desc = "The carry of subtracting limbs of `rhs` from those of `lhs`" polys = [ - ["/", ["-", ["+", ["idx", "rhs", 0], ["idx", "lhs_sub_rhs", 0]], ["idx", "lhs", 0]], ["^", 2, 32]], - ["/", ["-", ["+", ["idx", "rhs", 1], ["idx", "lhs_sub_rhs", 1], ["idx", "carry", 0]], ["idx", "lhs", 1]], ["^", 2, 16]], - ["/", ["-", ["+", ["idx", "rhs", 2], ["idx", "lhs_sub_rhs", 2], ["idx", "carry", 1]], ["idx", "lhs", 2]], ["^", 2, 16]] + ["*", ["^", 2, -32], ["-", ["+", ["idx", "rhs", 0], ["idx", ["cast", "lhs_sub_rhs", "DWordWL"], 0]], ["idx", "lhs", 0]]], + ["*", ["^", 2, -16], ["-", ["+", ["idx", "rhs", 1], ["idx", "lhs_sub_rhs", 2], ["idx", "carry", 0]], ["idx", "lhs", 1]]], + ["*", ["^", 2, -16], ["-", ["+", ["idx", "rhs", 2], ["idx", "lhs_sub_rhs", 3], ["idx", "carry", 1]], ["idx", "lhs", 2]]] ] [[variables.virtual]] @@ -127,9 +127,14 @@ ref = "lt:c:lhs_sub_rhs_msb" [[constraints.defs]] kind = "arith" constraint = "$#`lt` = #`signed` dot #`signed_lt` + (1 - #`signed`) dot #`unsigned_lt`$" -desc = "where some shorthand means something" poly = ["+", ["-", "lt"], ["*", "signed", "signed_lt"], ["*", ["-", 1, "signed"], "unsigned_lt"]] +[[constraints.defs]] +kind = "arith" +constraint = "$(1 - a) dot b + a dot b dot c + (1 - a) dot (1 - b) dot c$" +desc = "Where $a = #`lhs_msb`$, $b = #`rhs_msb`$ and $c = #`lhs_sub_rhs_msb`$" +poly = ["+", ["*", ["not", "lhs_msb"], "rhs_msb"], ["*", "lhs_msb", "rhs_msb", "lhs_sub_rhs_msb"], ["*", ["not", "lhs_msb"], ["not", "rhs_msb"], "lhs_sub_rhs_msb"]] + [[constraint_groups]] name = "sub" @@ -139,7 +144,7 @@ desc = "Constrain the subtraction" kind = "template" tag = "IS_BIT" input = [["idx", "carry", "i"]] -range = ["i", 0, 1] +range = ["i", 0, 2] [[constraints.sub]] kind = "interaction" From 3560d63034264b060fa088c22cabd94aa97cf51d Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 2 Jan 2026 12:03:05 +0100 Subject: [PATCH 03/10] Update LT virtual defs to new format --- spec/src/lt.toml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/spec/src/lt.toml b/spec/src/lt.toml index cdec3a835..2ab6159bc 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -60,17 +60,16 @@ desc = "The most significant bit of $#`lhs` - #`rhs`$" name = "carry" type = ["Bit", 3] desc = "The carry of subtracting limbs of `rhs` from those of `lhs`" -polys = [ - ["*", ["^", 2, -32], ["-", ["+", ["idx", "rhs", 0], ["idx", ["cast", "lhs_sub_rhs", "DWordWL"], 0]], ["idx", "lhs", 0]]], - ["*", ["^", 2, -16], ["-", ["+", ["idx", "rhs", 1], ["idx", "lhs_sub_rhs", 2], ["idx", "carry", 0]], ["idx", "lhs", 1]]], - ["*", ["^", 2, -16], ["-", ["+", ["idx", "rhs", 2], ["idx", "lhs_sub_rhs", 3], ["idx", "carry", 1]], ["idx", "lhs", 2]]] -] +def = {idx = "i", polys = [ + {range = [0], poly = ["*", ["^", 2, -32], ["-", ["+", ["idx", "rhs", 0], ["idx", ["cast", "lhs_sub_rhs", "DWordWL"], 0]], ["idx", "lhs", 0]]]}, + {range = [1, 2], poly = ["*", ["^", 2, -16], ["-", ["+", ["idx", "rhs", "i"], ["idx", "lhs_sub_rhs", ["+", "i", 1]], ["idx", "carry", ["-", "i", 1]]], ["idx", "lhs", "i"]]]}, +]} [[variables.virtual]] name = "unsigned_lt" type = "Bit" desc = "Whether $#`lhs` < #`rhs`$, as unsigned integers" -poly = ["idx", "carry", 2] +def = ["idx", "carry", 2] # Multiplicity From 31e0c354c44084c97bb20b88928d6dfa6843ff3e Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 2 Jan 2026 14:44:24 +0100 Subject: [PATCH 04/10] Fix signed_lt constraint to actually constraint signed_lt --- spec/src/lt.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/src/lt.toml b/spec/src/lt.toml index 2ab6159bc..470df7214 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -130,9 +130,9 @@ poly = ["+", ["-", "lt"], ["*", "signed", "signed_lt"], ["*", ["-", 1, "signed"] [[constraints.defs]] kind = "arith" -constraint = "$(1 - a) dot b + a dot b dot c + (1 - a) dot (1 - b) dot c$" +constraint = "#`signed_lt` = $(1 - a) dot b + a dot b dot c + (1 - a) dot (1 - b) dot c$" desc = "Where $a = #`lhs_msb`$, $b = #`rhs_msb`$ and $c = #`lhs_sub_rhs_msb`$" -poly = ["+", ["*", ["not", "lhs_msb"], "rhs_msb"], ["*", "lhs_msb", "rhs_msb", "lhs_sub_rhs_msb"], ["*", ["not", "lhs_msb"], ["not", "rhs_msb"], "lhs_sub_rhs_msb"]] +poly = ["-", "signed_lt", ["*", ["not", "lhs_msb"], "rhs_msb"], ["*", "lhs_msb", "rhs_msb", "lhs_sub_rhs_msb"], ["*", ["not", "lhs_msb"], ["not", "rhs_msb"], "lhs_sub_rhs_msb"]] [[constraint_groups]] From c87e8906fa65435833f1f63328a706ad4f8d3fb3 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 2 Jan 2026 16:48:02 +0100 Subject: [PATCH 05/10] Thanks Erik :) Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/src/lt.toml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/spec/src/lt.toml b/spec/src/lt.toml index 470df7214..c25ddc16c 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -91,7 +91,7 @@ range = ["i", 1, 2] ref = "lt:a:range_rhs" [[assumptions]] -desc = "`IS_BIT[signed]`" +desc = "`IS_BIT`" ref = "lt:a:range_signed" @@ -118,7 +118,7 @@ ref = "lt:c:rhs_msb" [[constraints.defs]] kind = "interaction" tag = "MSB16" -input = [["idx", "lsb_sub_rhs", 2]] +input = [["idx", "lsb_sub_rhs", 3]] output = "lhs_sub_rhs_msb" multiplicity = "μ" ref = "lt:c:lhs_sub_rhs_msb" @@ -126,11 +126,11 @@ ref = "lt:c:lhs_sub_rhs_msb" [[constraints.defs]] kind = "arith" constraint = "$#`lt` = #`signed` dot #`signed_lt` + (1 - #`signed`) dot #`unsigned_lt`$" -poly = ["+", ["-", "lt"], ["*", "signed", "signed_lt"], ["*", ["-", 1, "signed"], "unsigned_lt"]] +poly = ["-", "lt", ["*", "signed", "signed_lt"], ["*", ["-", 1, "signed"], "unsigned_lt"]] [[constraints.defs]] kind = "arith" -constraint = "#`signed_lt` = $(1 - a) dot b + a dot b dot c + (1 - a) dot (1 - b) dot c$" +constraint = "$#`signed_lt` = (1 - a) dot b + a dot b dot c + (1 - a) dot (1 - b) dot c$" desc = "Where $a = #`lhs_msb`$, $b = #`rhs_msb`$ and $c = #`lhs_sub_rhs_msb`$" poly = ["-", "signed_lt", ["*", ["not", "lhs_msb"], "rhs_msb"], ["*", "lhs_msb", "rhs_msb", "lhs_sub_rhs_msb"], ["*", ["not", "lhs_msb"], ["not", "rhs_msb"], "lhs_sub_rhs_msb"]] From 54dc14f9f3a9ef40a79a76392cfce32cc4990d26 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 5 Jan 2026 13:48:09 +0100 Subject: [PATCH 06/10] Logic fix --- spec/lt.typ | 3 ++- spec/src/lt.toml | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/spec/lt.typ b/spec/lt.typ index 1afb4f434..d65b0bf82 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page +#import "/book.typ": book-page, rj #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -26,6 +26,7 @@ We assume the inputs `lhs`, `rhs` and `signed` are appropriately range checked. == Constraints We first constrain that all variables correspond to their definition. +#rj[Explain formulae properly, including sign bit logic and how overflow only matters if signs differ] #render_constraint_table(chip, config, groups: "defs") diff --git a/spec/src/lt.toml b/spec/src/lt.toml index c25ddc16c..248d2f126 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -130,9 +130,9 @@ poly = ["-", "lt", ["*", "signed", "signed_lt"], ["*", ["-", 1, "signed"], "unsi [[constraints.defs]] kind = "arith" -constraint = "$#`signed_lt` = (1 - a) dot b + a dot b dot c + (1 - a) dot (1 - b) dot c$" +constraint = "$#`signed_lt` = a (1 - b) + a b c + (1 - a) (1 - b) c$" desc = "Where $a = #`lhs_msb`$, $b = #`rhs_msb`$ and $c = #`lhs_sub_rhs_msb`$" -poly = ["-", "signed_lt", ["*", ["not", "lhs_msb"], "rhs_msb"], ["*", "lhs_msb", "rhs_msb", "lhs_sub_rhs_msb"], ["*", ["not", "lhs_msb"], ["not", "rhs_msb"], "lhs_sub_rhs_msb"]] +poly = ["-", "signed_lt", ["*", "lhs_msb", ["not", "rhs_msb"]], ["*", "lhs_msb", "rhs_msb", "lhs_sub_rhs_msb"], ["*", ["not", "lhs_msb"], ["not", "rhs_msb"], "lhs_sub_rhs_msb"]] [[constraint_groups]] From 5d8834ffbcb983061b8110214586efadbe911b5b Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 5 Jan 2026 19:03:06 +0100 Subject: [PATCH 07/10] Optimize away two columns of LT and do some proving that that works --- spec/lt.typ | 38 +++++++++++++++++++++++++++++++++++++- spec/src/lt.toml | 39 ++++++++------------------------------- 2 files changed, 45 insertions(+), 32 deletions(-) diff --git a/spec/lt.typ b/spec/lt.typ index d65b0bf82..f489ff95e 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -26,7 +26,43 @@ We assume the inputs `lhs`, `rhs` and `signed` are appropriately range checked. == Constraints We first constrain that all variables correspond to their definition. -#rj[Explain formulae properly, including sign bit logic and how overflow only matters if signs differ] +For the defining constraint of `lt`, @lt:c:lt, observe that it is a choice +between two options, depending on the input flag `signed`. +In the case of unsigned comparison, we simply need `unsigned_lt`, indicating +that a wraparound (carry bit) modulo $2^64$ is needed to go from `rhs` to `lhs` via addition. +For the case of signed comparison, we first need some case analysis. +We can conclude that $a < b$ exactly when any of the following disjoint events happens. + +- $(a < 0) and (b >= 0)$ +- $(a < 0) and (b < 0) and (a < b)$ +- $(a >= 0) and (b >= 0) and (a < b)$ + +We represent can the comparisons of inputs to zero as the MSB or sign bits, +which we shall denote as $A$ for `lhs` and $B$ for `rhs`. +From this, we obtain the boolean formula $A dash(B) or A B C or dash(A) dash(B) C$, +where we let $C$ also denote the indicator of $(a - b < 0) and (A == B)$. +Since our cases were disjoint, this can be computed as the binary-valued polynomial +$P(A, B, C) = A dot (1 - B) + A dot B dot C + (1 - A) dot (1 - B) dot C$. + +Observe that after modular reduction to the range $[0, 2^64)$, +when $A == B$, the ordering $a < b$ is preserved, so $C$ can be expressed +---just as in the unsigned case--- by the overflow of the addition. + +The polynomial $P$ can be further simplified to a total degree of two. +We claim that the polynomial $Q(A, B, C) = A dot (1 - B) + A dot C + (1 - B) dot C$ +is, for the purposes of this chip, equivalent to $P$. +Through exhaustive checking, one can verify that the only binary input +for which $P(A, B, C) != Q(A, B, C)$, is the triple $(A, B, C) = (1, 0, 1)$. +This however, corresponds to the case where $a > b$ in the reduction to $[0, 2^64)$, +*and* an overflow is said to occur to go $b$ to $a$ by addition, +which is a contradiction with the correctness of the addition. +In more detail, if we let $s$ be the (range-checked) difference $a - b$ +(so the equivalent of the #`lhs_sub_rhs` column), +and $x'$ be the most significant word of $x$, +we need $c dot 2^32 + a' = b' + s' + #`carry[0]`$, by the definition of `carry`. +However, the left hand side of this, is at least $3 dot 2^31$, as $(a, c) = (1, 1)$, +and the right hand side is at most $(2^31 - 1) + (2^32 - 1) + 1 = 3 dot 2^31 - 1$. +Therefore, we can use $Q$ to constrain `lt` when `signed = 1`. #render_constraint_table(chip, config, groups: "defs") diff --git a/spec/src/lt.toml b/spec/src/lt.toml index 248d2f126..1bf51edda 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -28,11 +28,6 @@ desc = "Whether $#`lhs` < #`rhs`$, taking `signed` into account" # Auxiliary -[[variables.auxiliary]] -name = "signed_lt" -type = "Bit" -desc = "Whether $#`lhs` < #`rhs`$, as signed integers" - [[variables.auxiliary]] name = "lhs_sub_rhs" type = "DWordHL" @@ -48,28 +43,22 @@ name = "rhs_msb" type = "Bit" desc = "The most significant bit of `rhs`" -[[variables.auxiliary]] -name = "lhs_sub_rhs_msb" -type = "Bit" -desc = "The most significant bit of $#`lhs` - #`rhs`$" - - # Virtual [[variables.virtual]] name = "carry" -type = ["Bit", 3] +type = ["Bit", 2] desc = "The carry of subtracting limbs of `rhs` from those of `lhs`" def = {idx = "i", polys = [ {range = [0], poly = ["*", ["^", 2, -32], ["-", ["+", ["idx", "rhs", 0], ["idx", ["cast", "lhs_sub_rhs", "DWordWL"], 0]], ["idx", "lhs", 0]]]}, - {range = [1, 2], poly = ["*", ["^", 2, -16], ["-", ["+", ["idx", "rhs", "i"], ["idx", "lhs_sub_rhs", ["+", "i", 1]], ["idx", "carry", ["-", "i", 1]]], ["idx", "lhs", "i"]]]}, + {range = [1], poly = ["*", ["^", 2, -32], ["-", ["+", ["idx", ["cast", "rhs", "DWordWL"], 1], ["idx", ["cast", "lhs_sub_rhs", "DWordWL"], 1], ["idx", "carry", 0]], ["idx", ["cast", "lhs", "DWordWL"], 1]]]}, ]} [[variables.virtual]] name = "unsigned_lt" type = "Bit" desc = "Whether $#`lhs` < #`rhs`$, as unsigned integers" -def = ["idx", "carry", 2] +def = ["idx", "carry", 1] # Multiplicity @@ -115,24 +104,12 @@ output = "rhs_msb" multiplicity = "μ" ref = "lt:c:rhs_msb" -[[constraints.defs]] -kind = "interaction" -tag = "MSB16" -input = [["idx", "lsb_sub_rhs", 3]] -output = "lhs_sub_rhs_msb" -multiplicity = "μ" -ref = "lt:c:lhs_sub_rhs_msb" - -[[constraints.defs]] -kind = "arith" -constraint = "$#`lt` = #`signed` dot #`signed_lt` + (1 - #`signed`) dot #`unsigned_lt`$" -poly = ["-", "lt", ["*", "signed", "signed_lt"], ["*", ["-", 1, "signed"], "unsigned_lt"]] - [[constraints.defs]] kind = "arith" -constraint = "$#`signed_lt` = a (1 - b) + a b c + (1 - a) (1 - b) c$" -desc = "Where $a = #`lhs_msb`$, $b = #`rhs_msb`$ and $c = #`lhs_sub_rhs_msb`$" -poly = ["-", "signed_lt", ["*", "lhs_msb", ["not", "rhs_msb"]], ["*", "lhs_msb", "rhs_msb", "lhs_sub_rhs_msb"], ["*", ["not", "lhs_msb"], ["not", "rhs_msb"], "lhs_sub_rhs_msb"]] +constraint = "$#`lt` = #`signed` dot (A dot (1 - B) + A dot C + (1 - B) dot C) + (1 - #`signed`) dot #`unsigned_lt`$" +desc = "Where $A = #`lhs_msb`$, $B = #`rhs_msb`$ and $C = #`carry[1]`$" +poly = ["-", "lt", ["*", "signed", ["+", ["*", "lhs_msb", ["not", "rhs_msb"]], ["*", "lhs_msb", ["idx", "carry", 1]], ["*", ["not", "rhs_msb"], ["idx", "carry", 1]]]], ["*", ["-", 1, "signed"], "unsigned_lt"]] +ref = "lt:c:lt" [[constraint_groups]] @@ -143,7 +120,7 @@ desc = "Constrain the subtraction" kind = "template" tag = "IS_BIT" input = [["idx", "carry", "i"]] -range = ["i", 0, 2] +range = ["i", 0, 1] [[constraints.sub]] kind = "interaction" From f0ad43f705390462f3366ce24d34041d428b6d64 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Wed, 7 Jan 2026 12:09:47 +0100 Subject: [PATCH 08/10] Apply suggestions from code review Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/lt.typ | 8 ++++---- spec/src/lt.toml | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/spec/lt.typ b/spec/lt.typ index f489ff95e..2b84628b1 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -42,25 +42,25 @@ which we shall denote as $A$ for `lhs` and $B$ for `rhs`. From this, we obtain the boolean formula $A dash(B) or A B C or dash(A) dash(B) C$, where we let $C$ also denote the indicator of $(a - b < 0) and (A == B)$. Since our cases were disjoint, this can be computed as the binary-valued polynomial -$P(A, B, C) = A dot (1 - B) + A dot B dot C + (1 - A) dot (1 - B) dot C$. +$P(A, B, C) = A (1 - B) + A B C + (1 - A) (1 - B) C$. Observe that after modular reduction to the range $[0, 2^64)$, when $A == B$, the ordering $a < b$ is preserved, so $C$ can be expressed ---just as in the unsigned case--- by the overflow of the addition. -The polynomial $P$ can be further simplified to a total degree of two. +The polynomial $P$ can be simplified to a total degree of two. We claim that the polynomial $Q(A, B, C) = A dot (1 - B) + A dot C + (1 - B) dot C$ is, for the purposes of this chip, equivalent to $P$. Through exhaustive checking, one can verify that the only binary input for which $P(A, B, C) != Q(A, B, C)$, is the triple $(A, B, C) = (1, 0, 1)$. -This however, corresponds to the case where $a > b$ in the reduction to $[0, 2^64)$, +This, however, corresponds to the case where $a > b$ in the reduction to $[0, 2^64)$, *and* an overflow is said to occur to go $b$ to $a$ by addition, which is a contradiction with the correctness of the addition. In more detail, if we let $s$ be the (range-checked) difference $a - b$ (so the equivalent of the #`lhs_sub_rhs` column), and $x'$ be the most significant word of $x$, we need $c dot 2^32 + a' = b' + s' + #`carry[0]`$, by the definition of `carry`. -However, the left hand side of this, is at least $3 dot 2^31$, as $(a, c) = (1, 1)$, +However, the left hand side of this, is at least $3 dot 2^31$, as $(A, C) = (1, 1)$, and the right hand side is at most $(2^31 - 1) + (2^32 - 1) + 1 = 3 dot 2^31 - 1$. Therefore, we can use $Q$ to constrain `lt` when `signed = 1`. diff --git a/spec/src/lt.toml b/spec/src/lt.toml index 1bf51edda..7959a0276 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -106,7 +106,7 @@ ref = "lt:c:rhs_msb" [[constraints.defs]] kind = "arith" -constraint = "$#`lt` = #`signed` dot (A dot (1 - B) + A dot C + (1 - B) dot C) + (1 - #`signed`) dot #`unsigned_lt`$" +constraint = "$#`lt` = #`signed` dot (A (1 - B) + A C + (1 - B) C) + (1 - #`signed`) dot #`unsigned_lt`$" desc = "Where $A = #`lhs_msb`$, $B = #`rhs_msb`$ and $C = #`carry[1]`$" poly = ["-", "lt", ["*", "signed", ["+", ["*", "lhs_msb", ["not", "rhs_msb"]], ["*", "lhs_msb", ["idx", "carry", 1]], ["*", ["not", "rhs_msb"], ["idx", "carry", 1]]]], ["*", ["-", 1, "signed"], "unsigned_lt"]] ref = "lt:c:lt" From 9b163c2683ab95baef2ac3d7dc76917770fc9f60 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Wed, 7 Jan 2026 13:07:22 +0100 Subject: [PATCH 09/10] Proof rewrite for clarity --- spec/lt.typ | 41 ++++++++++++++++++++++------------------- 1 file changed, 22 insertions(+), 19 deletions(-) diff --git a/spec/lt.typ b/spec/lt.typ index 2b84628b1..d793a1982 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -31,31 +31,34 @@ between two options, depending on the input flag `signed`. In the case of unsigned comparison, we simply need `unsigned_lt`, indicating that a wraparound (carry bit) modulo $2^64$ is needed to go from `rhs` to `lhs` via addition. For the case of signed comparison, we first need some case analysis. -We can conclude that $a < b$ exactly when any of the following disjoint events happens. -- $(a < 0) and (b >= 0)$ -- $(a < 0) and (b < 0) and (a < b)$ -- $(a >= 0) and (b >= 0) and (a < b)$ +We split $a < b$ into four disjoint cases, conditioned on the sign of $a$ and $b$. +Recall that the sign of a number in two's complement can be read off from the MSB, +being $1$ for a negative number and $0$ for a positive one. +For this analysis, we denote the MSB of `lhs` as $A$ and the MSB of `rhs` as $B$. -We represent can the comparisons of inputs to zero as the MSB or sign bits, -which we shall denote as $A$ for `lhs` and $B$ for `rhs`. -From this, we obtain the boolean formula $A dash(B) or A B C or dash(A) dash(B) C$, -where we let $C$ also denote the indicator of $(a - b < 0) and (A == B)$. -Since our cases were disjoint, this can be computed as the binary-valued polynomial -$P(A, B, C) = A (1 - B) + A B C + (1 - A) (1 - B) C$. ++ $dash(A) and B and (a < b)$ ++ $A and dash(B) and (a < b)$ ++ $A and B and (a < b)$ ++ $dash(A) and dash(B) and (a < b)$ + +The first case is evidently false, while the second case simplifies to $A and dash(B)$. +For the third and fourth case, observe that when $A = B$, the $<$ relation is preserved +by the modular correspondence between $[-2^(31), 2^(31))$ and $[0, 2^(64))$. +Importantly, this modular correspondence is merely a reinterpretation of the +bits or values of $a$ and $b$, due to the representation in two's complement. +Hence, we can introduce the value $C = #`unsigned_lt`$, that accurately represents +the relation $a < b$ when $A = B$. -Observe that after modular reduction to the range $[0, 2^64)$, -when $A == B$, the ordering $a < b$ is preserved, so $C$ can be expressed ----just as in the unsigned case--- by the overflow of the addition. +Combining our three remaining cases, we obtain the boolean formula $A dash(B) or A B C or dash(A) dash(B) C$. +Since the cases are disjoint, this can be computed as the binary-valued polynomial +$P(A, B, C) = A (1 - B) + A B C + (1 - A) (1 - B) C$. The polynomial $P$ can be simplified to a total degree of two. -We claim that the polynomial $Q(A, B, C) = A dot (1 - B) + A dot C + (1 - B) dot C$ +We claim that the polynomial $Q(A, B, C) = A (1 - B) + A C + (1 - B) C$ is, for the purposes of this chip, equivalent to $P$. -Through exhaustive checking, one can verify that the only binary input -for which $P(A, B, C) != Q(A, B, C)$, is the triple $(A, B, C) = (1, 0, 1)$. -This, however, corresponds to the case where $a > b$ in the reduction to $[0, 2^64)$, -*and* an overflow is said to occur to go $b$ to $a$ by addition, -which is a contradiction with the correctness of the addition. +An exhaustive check shows that $P(A, B, C) != Q(A, B, C)$, only for the triple $(A, B, C) = (1, 0, 1)$. +This is however impossible due to the correctness of `ADD`. In more detail, if we let $s$ be the (range-checked) difference $a - b$ (so the equivalent of the #`lhs_sub_rhs` column), and $x'$ be the most significant word of $x$, From 691e8e29b6272e4651a6cdcef16689fd95bb64d7 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Thu, 8 Jan 2026 11:14:21 +0100 Subject: [PATCH 10/10] More review comments --- spec/lt.typ | 13 +++++++------ spec/src/lt.toml | 2 +- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/spec/lt.typ b/spec/lt.typ index d793a1982..ff3b6dae3 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -35,7 +35,8 @@ For the case of signed comparison, we first need some case analysis. We split $a < b$ into four disjoint cases, conditioned on the sign of $a$ and $b$. Recall that the sign of a number in two's complement can be read off from the MSB, being $1$ for a negative number and $0$ for a positive one. -For this analysis, we denote the MSB of `lhs` as $A$ and the MSB of `rhs` as $B$. +For this analysis, we denote the MSB of $a$ as $A$ and the MSB of $b$ as $B$. +The four disjoint cases then become: + $dash(A) and B and (a < b)$ + $A and dash(B) and (a < b)$ @@ -51,19 +52,19 @@ Hence, we can introduce the value $C = #`unsigned_lt`$, that accurately represen the relation $a < b$ when $A = B$. Combining our three remaining cases, we obtain the boolean formula $A dash(B) or A B C or dash(A) dash(B) C$. -Since the cases are disjoint, this can be computed as the binary-valued polynomial +Since the cases are disjoint, this can be computed with the binary-valued polynomial $P(A, B, C) = A (1 - B) + A B C + (1 - A) (1 - B) C$. The polynomial $P$ can be simplified to a total degree of two. We claim that the polynomial $Q(A, B, C) = A (1 - B) + A C + (1 - B) C$ is, for the purposes of this chip, equivalent to $P$. -An exhaustive check shows that $P(A, B, C) != Q(A, B, C)$, only for the triple $(A, B, C) = (1, 0, 1)$. -This is however impossible due to the correctness of `ADD`. +An exhaustive check shows that $P(A, B, C) != Q(A, B, C)$ only for the triple $(A, B, C) = (1, 0, 1)$. +This is, however, impossible due to the correctness of `ADD`. In more detail, if we let $s$ be the (range-checked) difference $a - b$ (so the equivalent of the #`lhs_sub_rhs` column), -and $x'$ be the most significant word of $x$, +and $x'$ denote the most significant word of a variable $x$, we need $c dot 2^32 + a' = b' + s' + #`carry[0]`$, by the definition of `carry`. -However, the left hand side of this, is at least $3 dot 2^31$, as $(A, C) = (1, 1)$, +However, the left hand side of this is at least $3 dot 2^31$, as $(A, C) = (1, 1)$, and the right hand side is at most $(2^31 - 1) + (2^32 - 1) + 1 = 3 dot 2^31 - 1$. Therefore, we can use $Q$ to constrain `lt` when `signed = 1`. diff --git a/spec/src/lt.toml b/spec/src/lt.toml index 7959a0276..1a441c2b3 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -48,7 +48,7 @@ desc = "The most significant bit of `rhs`" [[variables.virtual]] name = "carry" type = ["Bit", 2] -desc = "The carry of subtracting limbs of `rhs` from those of `lhs`" +desc = "The carry for adding `lhs_sub_rhs` back to `rhs`" def = {idx = "i", polys = [ {range = [0], poly = ["*", ["^", 2, -32], ["-", ["+", ["idx", "rhs", 0], ["idx", ["cast", "lhs_sub_rhs", "DWordWL"], 0]], ["idx", "lhs", 0]]]}, {range = [1], poly = ["*", ["^", 2, -32], ["-", ["+", ["idx", ["cast", "rhs", "DWordWL"], 1], ["idx", ["cast", "lhs_sub_rhs", "DWordWL"], 1], ["idx", "carry", 0]], ["idx", ["cast", "lhs", "DWordWL"], 1]]]},