diff --git a/spec/book.typ b/spec/book.typ index 7787acbce..6652ed646 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -8,8 +8,9 @@ #chapter("variables.typ")[Variables] #chapter("is_bit.typ")[IS_BIT template] #chapter("cpu.typ")[CPU chip] + #chapter("shift.typ")[SHIFT chip] #chapter("branch.typ")[BRANCH] - #chapter("lt.typ")[LT], + #chapter("lt.typ")[LT] ] ) diff --git a/spec/expr.typ b/spec/expr.typ index ae7bd0792..547f2cad2 100644 --- a/spec/expr.typ +++ b/spec/expr.typ @@ -31,6 +31,7 @@ // | ["idx", expr1, expr2] ; expr1[expr2] // | ["not", expr] ; !expr // | ["+", expr1, expr2, ...] ; expr1 + expr2 + ... +// | ["sum", expr1, expr2, expr3] ; Σ_expr1^expr2 expr3 // | ["*", expr1, expr2, ...] ; expr1 * expr2 * ... // | ["/", expr1, expr2] ; expr1 / expr2 // | ["^", expr1, expr2] ; expr1^expr2 @@ -51,12 +52,13 @@ "cast": 2, // cast "mul": 3, // * "div": 4, // / - "not": 5, // not - "add": 6, // + - "sub": 7, // - - "idx": 8, // [] - "eq": 9, // = and := - "MAX": 10, // + "sum": 5, // Σ + "not": 6, // not + "add": 7, // + + "sub": 8, // - + "idx": 9, // [] + "eq": 10, // = and := + "MAX": 11, // ) // Mutual recursion through a trick from https://github.com/typst/typst/issues/744 @@ -92,6 +94,7 @@ "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), "+": (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) => cwrap(e.slice(1).map(rec.with(PREC.mul)).join(` ` + sym.dot + ` `), pp < PREC.mul), "/": (pp, rec, e) => cwrap(rec(PREC.div, e.at(1)), pp < PREC.div) + ` / ` + rec(PREC.div, e.at(2)), "^": (pp, rec, e) => { @@ -132,6 +135,13 @@ "idx": (pp, rec, e) => $#rec(PREC.idx, e.at(1))_(#rec(PREC.idx, e.at(2)))$, "not": (pp, rec, e) => mwrap($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)) + mwrap( + $sum_(#rec(PREC.MAX, e.at(1)))^#rec(PREC.MAX, e.at(2)) #rec(if pp <= PREC.sub {PREC.MAX} else {PREC.sum}, e.at(3))$, + pp <= PREC.sub + ) + }, "*": (pp, rec, e) => mwrap($#e.slice(1).map(rec.with(PREC.mul)).join($dot$)$, pp < PREC.mul), "/": (pp, rec, e) => $#rec(PREC.div, e.at(1)) / #rec(PREC.div, e.at(2))$, "^": (pp, rec, e) => { diff --git a/spec/shift.typ b/spec/shift.typ new file mode 100644 index 000000000..3555d64e4 --- /dev/null +++ b/spec/shift.typ @@ -0,0 +1,175 @@ +#import "/book.typ": book-page, et +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_column_table, + total_nr_variables, + total_nr_instantiated_columns, + render_constraint_table, + render_chip_assumptions, +) + +#let config = load_config() +#let chip = load_chip("src/shift.toml", config) + +#let shift = raw(chip.name) + +#show: book-page.with(title: "SHIFT chip") + += #shift chip + +== Interface +The #shift chip has the following interface: +#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(240), +``` +// param in: the value being shifted +// param shift: the number of bits to shift `in` by +// param direction: whether to shift left (0) or right (1) +// param signed: whether to interpret `in` as a signed (1) or unsigned (0) integer +// param word_instr: whether to execute the SLL/SR* (0) or SLLW/SR*W (1) instruction +// out shifted: the resulting value +SHIFT[shifted: DWord; in: DWord, shift: Byte, direction: Bit, signed: Bit, word_instr: Bit] +``` +) +In other words, the #shift chip is designed to constrain that +$ +#`shifted` := cases( + #`in` #`<<` #`s` " if" #`direction` = 0, + #`in` #`>>` #`s` " if" #`direction` = 1 and #`signed` = 0, + #`in` #`>>>` #`s` "if" #`direction` = 1 and #`signed` = 1, +) +$ +where +$ +#`s` := cases( + #`shift` mod 32 "if" #`word_instr` = 1, + #`shift` mod 64 "if" #`word_instr` = 0, +) +$ +Here, `<<` and `>>` denote the _logical_ left and right shift operations, while `>>>` denotes the _arithmetic_ right shift operation. + +== Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) + +The `SHIFT` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: +#render_chip_column_table(chip, config) + +== Assumptions +#render_chip_assumptions(chip, config) + +== Explanation +This chip has a rather complex design as a result of designing it to fit in as few columns possible. +We briefly discuss the intricacies of the design, attempting to illustrate its correctness. + +The chip's design revolves around a two-phase shifting process: +1. shift `in` by $x := #`shift` mod 16$ bits, +2. shift that result by $(#`shift`-x) mod 64$ (or $mod 32$ if $ #`word_instr` = 1$). +The intermediate value representing the state between the two phases is stored in the scratch variables `X` and `Y`. +The definition of `shifted` describes how one can combine the `X`, `Y` and `extension` variables to construct the output value as described using `Half`-limbs. +The output variable `out` is equivalent to `shifted`, but expressed using `Word`-limbs. + +In the following, we cover how these two phases were designed to complement one another. +Here, we start with discussing the _logical_ left/right shift operations only; the modifications required to compute the _arithmetic_ right shift will be discussed at the end. + +=== First phase +We zoom in on the first step. +Here, we make use of the two lookup operations +- $#`HWSL[x: Half, y: B4]` := (#`x` #`<<` #`y`) mod 2^16$ (short for "HalfWord Shift Left"), and +- $#`HWSLC[x: Half, y: B4]` := #`x` #`>>` (16-#`y`)$ (short for "HalfWord Shift Left's Carry") +Note here that one can use these two lookups to compute `out: Half[4] := in << y` as: +$ + #`out[`i#`]` = cases( + #`HWSL[in[`0#`], y]` &"if" i = 0, + #`HWSL[in[`i#`], y] | HWSLC[in[`i-1#`], y]` &"if" i in [1, 3] + ) +$ +as long as $#`y` < 16$. +Observing that +$#`HWSL[x,` 16-#`y]` = (#`x` #`<<` (16-#`y`)) mod 2^16$, and +$#`HWSLC[x,` 16-#`y]` = #`x` #`>>` #`y`$ for $#`y` in [1, 15]$, +one can also use these lookups to compute `out := in >> y` as +$ + #`out[`i#`]` = cases( + #`HWSLC[in[`i#`],` 16-#`y] | HWSL[in[`i+1#`], y]` &"if" i in [0, 2], + #`HWSLC[in[`3#`],` 16-#`y]` &"if" i = 3 + ) +$ +as long as $0 < #`y` < 16$. + +Observe now that the values being looked up are (almost) independent from the direction of the shift: only the shift-amount varies slightly. +When we now define +$ + #`bit_shift` := cases( + #`shift` mod 16 & "when shifting left", + (16-#`shift`) mod 16 & "when shifting right" + ), +$ +it only takes some rearranging and combining of the values $#`X[`i#`] := HWSL[in[`i#`], bit_shift]`$ and $#`Y[`i#`] := HWSLC[in[`i#`], bit_shift]`$ to form the limbs of $#`in <> shift` mod 16$. +In the remaining case that $#`right` = 1$ and $#`shift` = 0 mod 16$, the limbs of $#`in <> shift` mod 16$ simply match those of `in`. + +=== Second phase +Since we're operating on 16-bit limbs, all the limbs in $#`in <> shift`$ must also occur somewhere in $#`in <> shift` mod 16$. +The number of full-limbs we still need to shift is determined by the fifth and sixth least significant bit of `shift`. +With `limb_shift` containing a unary decoding of the integer represented by these two bits, we find that the intermediate value needs to be shifted over by $i$ limbs (to the `left` or `right`) when $#`limb_shift[`i#`]` = 1$. +These things combined yield `shifted`'s definition. + +Of course, when $#`word_instr` = 1$ and, thus, only $#`shift` mod 32$ should be considered, the bit-mask for the lookup constraining `limb_shift` is adjusted appropriately (see @shift:c:limb_shift_lookup). + +=== Arithmetic right shift +Lastly, we discuss the case of performing the _arithmetic_ right shift. +Here, `extension` is constrained to contain a repetition of `in`'s most significant bit. +Copies of this variable are used for any full limbs shifted in when $#`right` = #`signed` = 1$. +Moreover, `X[4]` contains a copy of `extension` shifted over by the right number of bits, to allow the construction of $#`in >>> shift` mod 16$ as the appropriate intermediate. + +== Constraints +First, we constrain `bit_shift` based on whether we are left or right-shifting. +@shift:c:zbs makes sure `zbs` is set to `1` if and only if `bit_shift = 0`. +This flag is used to indicate the special case that $#`right` = 1$ and $#`shift` = 0 mod 16$. +#render_constraint_table(chip, config, groups: "bit_shift") + +Next, we shift the limbs of `in` left and right by the appropriate amount, storing the results in `X` and `Y` respectively. +When `zbs = 1`, the output cannot be used to compose $#`in >>/>>> shift` mod 16$. +To resolve this, we override `Y[i] := in[i]` and `X[i] := 0` in this case. + +The case of `left`-shifting and $#`bit_shift` = 0$ will be used for padding rows. +To prevent unnecessary lookups in padding rows, we override $#`X[i]` := #`in[i]`$ and $#`Y[i]` := 0$ here. +#render_constraint_table(chip, config, groups: "intra_limb_shift") + +=== Full-limb shifting +Next, we constrain that `limb_shift` is a proper unary encoding of the fifth (and sixth if $#`word_instr` = 0$) bit of `shift`. +For this to be the case, three requirements must be satisfied: ++ *unary(0)*: $#`limb_shift[`i#`]` in {0, 1}$ for $i in [0, 3]$, ++ *unary(1)*: $#`limb_shift[`i#`]` = 1$ for exactly one $i$, and ++ *proper encoding*: $#`limb_shift[`i#`]` = 1 <=> 1/16 (#`shift &` (48-32 dot #`word_instr`)) = i$ +The first requirement is enforced by constraint @shift:c:limb_shift_is_bit. +To construct a constraint for the second and third requirement, observe that +$ +1/16 dot (#`shift &` (48-32 dot #`word_instr`)) in cases( + {0, 1, 2, 3} &"if" #`word_instr` = 0, + {0, 1} &"if" #`word_instr` = 1 +) +$ +Observe moreover that, assuming *unary(0)*, the expression +$ + 1/16 dot (1 + sum_(i=0)^3 (16i-1) dot #`limb_shift[`i#`]`) +$ +can evaluate to $i$ if and only if $#`limb_shift[`i#`]` = 1$, while the others are $0$. +This means that the relation +$ + 1 + sum_(i=0)^3 (16i-1) dot #`limb_shift[`i#`]` = #`shift &` (48-32 dot #`word_instr`) +$ +enforces both *unary(1)* and *proper encoding*. +This is the exact relation @shift:c:limb_shift_lookup enforces. + + +Hereafter, one must only check that `out` is the proper cast of `shifted` into a `DWordWL`. +#render_constraint_table(chip, config, groups: "limb_shifting") + +=== Miscellaneous +#render_constraint_table(chip, config, groups: ("left_flag", "is_negative")) +*Note*: `is_negative` is not used when `signed = 0`. +As such, there is no problem with it being unconstrained in this case. + +=== Lookups +This chip adds the following interaction to the lookup. +#render_constraint_table(chip, config, groups: "lookups") diff --git a/spec/src/shift.toml b/spec/src/shift.toml new file mode 100644 index 000000000..e2ddfa12b --- /dev/null +++ b/spec/src/shift.toml @@ -0,0 +1,283 @@ +name = "SHIFT" + +# Input + +[[variables.input]] +name = "in" +type = "DWordHL" +desc = "The value being shifted" + +[[variables.input]] +name = "shift" +type = "Byte" +desc = "Number of bits to shift `in` by." + +[[variables.input]] +name = "direction" +type = "Bit" +desc = "Whether to shift left (0) or right (1)." + +[[variables.input]] +name = "signed" +type = "Bit" +desc = "Whether to interpret `in` as a signed integer." + +[[variables.input]] +name = "word_instr" +type = "Bit" +desc = "Whether this is a Word-instruction (1) or not (0)." + + +# Output + +[[variables.output]] +name = "out" +type = "DWordWL" +desc = "$#`in <>/>>>` (#`shift` mod 32 dot (2 - #`word_instr`))$" + +# Auxiliary + +[[variables.auxiliary]] +name = "is_negative" +type = "Bit" +desc = "Whether `in` is negative" + +[[variables.auxiliary]] +name = "bit_shift" +type = "Byte" +desc = "Value by which to shift `in` to obtain `X` and `Y`" + +[[variables.auxiliary]] +name = "zbs" +type = "Bit" +desc = "Whether `bit_shift` is zero (1) or not (0)." + +[[variables.auxiliary]] +name = "X" +type = ["Half", 5] +desc = "scratch variable." + +[[variables.auxiliary]] +name = "Y" +type = ["Half", 4] +desc = "scratch variable." + +[[variables.auxiliary]] +name = "limb_shift" +type = ["Bit", 4] +desc = "One-hot vector indicating whether $floor.l #`shift` / 16 floor.r equiv i mod s$, where $s = 2$ when $#`word_instr` = 1$ and $4$ otherwise." + +# Virtual + +[[variables.virtual]] +name = "extension" +type = "Half" +desc = "sign extension of `in`." +def = ["*", 65535, "is_negative"] + +[[variables.virtual]] +name = "left" +type = "Bit" +desc = "Whether to perform a left-shift." +def = ["-", "μ", "direction"] + +[[variables.virtual]] +name = "right" +type = "Bit" +desc = "Whether to perform a right-shift." +def = "direction" + +[[variables.virtual]] +name = "intra_limb_left" +type = "DWordHL" +desc = "`in << (shift % 16)` if `left`" +def = {idx="i", polys=[ + {range=0, poly=["idx", "X", 0]}, + {range=[1, 3], poly=["+", ["idx", "X", "i"], ["idx", "Y", ["-", "i", 1]]]}, +]} + +[[variables.virtual]] +name = "intra_limb_right" +type = "DWordHL" +desc = "`in >>> (shift % 16)` if `right` and `signed`;\\ `in >> (shift % 16)` if `right` and `!signed`" +def = {idx="i", range=[0, 3], poly=["+", ["idx", "Y", "i"], ["idx", "X", ["+", "i", 1]]]} + +[[variables.virtual]] +name = "shifted" +type = "DWordHL" +desc = "$#`in <>/>>>` (#`shift` mod 32 dot (2 - #`word_instr`))$" +def = {idx="i", range=[0, 3], poly=["+", ["*", "left", ["sum", ["=", "j", 0], "i", ["*", ["idx", "limb_shift", "j"], ["idx", "intra_limb_left", ["-", "i", "j"]]]]], ["*", "right", ["+", ["sum", ["=", "j", 0], ["-", 3, "i"], ["*", ["idx", "limb_shift", "j"], ["idx", "intra_limb_right", ["+", "i", "j"]]]], ["*", "extension", ["sum", ["=", "j", ["-", 3, "i"]], 3, ["idx", "limb_shift", "j"]]]]]]} + +# Multiplicities + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" + + + +# Assumptions + +[[assumptions]] +desc = "`IS_HALFWORD[in[i]]`" +range = ["i", 0, 3] +ref = "shift:a:range_in" + +[[assumptions]] +desc = "`IS_BYTE[shift]`" +ref = "shift:a:range_shift" + +[[assumptions]] +desc = "`IS_BIT`" +ref = "shift:a:direction" + +[[assumptions]] +desc = "`IS_BIT`" +ref = "shift:a:signed" + +[[assumptions]] +desc = "`IS_BIT`" +ref = "shift:a:word_instr" + +# Constraints + +[[constraint_groups]] +name = "left_flag" + +[[constraints.left_flag]] +kind = "arith" +desc = "enforces `left` is `Bit`." +constraint = "$#`direction` => #`μ` = 1$" +poly = ["*", "direction", ["not", "μ"]] +ref = "shift:c:direction_implies_mu" + + +[[constraint_groups]] +name = "is_negative" + +[[constraints.is_negative]] +kind = "interaction" +tag = "MSB16" +input = [["idx", "in", 3]] +output = "is_negative" +multiplicity = "signed" +ref = "shift:c:is_negative_if_signed" + + +[[constraint_groups]] +name = "bit_shift" + +[[constraints.bit_shift]] +kind = "interaction" +tag = "AND_BYTE" +input = ["shift", 0x0F] +output = "bit_shift" +ref = "shift:c:bit_shift_if_left" +multiplicity = "left" + +[[constraints.bit_shift]] +kind = "interaction" +tag = "AND_BYTE" +input = [["-", ["^", 2, 8], "shift"], 0x0F] +output = "bit_shift" +ref = "shift:c:bit_shift_if_right" +multiplicity = "right" + +[[constraints.bit_shift]] +kind = "template" +tag = "IsZero" +input = ["bit_shift"] +output = "zbs" +ref = "shift:c:zbs" +multiplicity = "μ" + + +[[constraint_groups]] +name = "intra_limb_shift" + +[[constraints.intra_limb_shift]] +kind = "interaction" +tag = "HWSL" +input = [["idx", "in", "i"], "bit_shift"] +output = ["idx", "X", "i"] +range = ["i", 0, 3] +ref = "shift:c:hwsl_if_not_zero" +multiplicity = ["not", "zbs"] + +[[constraints.intra_limb_shift]] +kind = "arith" +constraint = "$#`zbs` => #`X[i]` = #`in[i]` dot #`left`$" +poly = ["*", "zbs", ["-", ["idx", "X", "i"], ["*", ["idx", "in", "i"], "left"]]] +range = ["i", 0, 3] +ref = "shift:c:zbs_implies_X" + +[[constraints.intra_limb_shift]] +kind = "interaction" +tag = "HWSL" +input = ["extension", "bit_shift"] +output = ["idx", "X", 4] +ref = "shift:c:hwsl_x4_if_not_zero" +multiplicity = ["not", "zbs"] + +[[constraints.intra_limb_shift]] +kind = "arith" +constraint = "$#`zbs` => #`X[4]` = 0$" +poly = ["*", "zbs", ["idx", "X", 4]] +ref = "shift:c:zbs_implies_X_4" + +[[constraints.intra_limb_shift]] +kind = "interaction" +tag = "HWSLC" +input = [["idx", "in", "i"], "bit_shift"] +output = ["idx", "Y", "i"] +range = ["i", 0, 3] +ref = "shift:c:hwslc_if_not_zero" +multiplicity = ["not", "zbs"] + +[[constraints.intra_limb_shift]] +kind = "arith" +constraint = "$#`zbs` => #`Y[i]` = #`in[i]` dot #`right`$" +poly = ["*", "zbs", ["-", ["idx", "Y", "i"], ["*", ["idx", "in", "i"], "right"]]] +range = ["i", 0, 3] +ref = "shift:c:zbs_implies_Y" + + +[[constraint_groups]] +name = "limb_shifting" + +[[constraints.limb_shifting]] +kind = "template" +tag = "IS_BIT" +input = [["idx", "limb_shift", "i"]] +range = ["i", 0, 3] +ref = "shift:c:limb_shift_is_bit" + +[[constraints.limb_shifting]] +kind = "interaction" +tag = "AND_BYTE" +input = ["shift", ["-", 0x30, ["*", 0x20, "word_instr"]]] +output = ["+", ["-", 1, ["idx", "limb_shift", 0]], ["*", 15, ["idx", "limb_shift", 1]], ["*", 31, ["idx", "limb_shift", 2]], ["*", 47, ["idx", "limb_shift", 3]]] +ref = "shift:c:limb_shift_lookup" +multiplicity = "μ" + +[[constraints.limb_shifting]] +kind = "arith" +constraint = "$#`out[:2]` = #`shifted[:4]`$" +poly = ["-", ["idx", "out", "i"], ["idx", ["cast", "shifted", "DWordWL"], "i"]] +range = ["i", 0, 1] +ref = "shift:c:out_eq_shifted" + + +# Lookups + +[[constraint_groups]] +name = "lookups" + +[[constraints.lookups]] +kind = "interaction" +tag = "SHIFT" +input = ["in", "shift", "direction", "signed", "word_instr"] +output = "out" +multiplicity = "-μ" +ref = "shift:c:lookup"