spec: Introduce LT chip

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],
   ]
 )
 

spec/lt.typ

@@ -0,0 +1,79 @@
+#import "/book.typ": book-page, rj
+#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.
+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 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 $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)$
++ $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$.
+
+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 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`.
+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'$ 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)$,
+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")
+
+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")

spec/src/lt.toml

@@ -0,0 +1,143 @@
+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 (1) or not (0)"
+
+# Output
+
+[[variables.output]]
+name = "lt"
+type = "Bit"
+desc = "Whether $#`lhs` < #`rhs`$, taking `signed` into account"
+
+
+# Auxiliary
+
+[[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`"
+
+# Virtual
+
+[[variables.virtual]]
+name = "carry"
+type = ["Bit", 2]
+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]]]},
+]}
+
+[[variables.virtual]]
+name = "unsigned_lt"
+type = "Bit"
+desc = "Whether $#`lhs` < #`rhs`$, as unsigned integers"
+def = ["idx", "carry", 1]
+
+
+# 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 = "arith"
+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"
+
+
+[[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 = "-μ"