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..ff3b6dae3 --- /dev/null +++ b/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") diff --git a/spec/src/lt.toml b/spec/src/lt.toml new file mode 100644 index 000000000..1a441c2b3 --- /dev/null +++ b/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`" +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 = "-μ"