spec: BITWISE chip

spec/bitwise.typ

@@ -0,0 +1,44 @@
+#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/bitwise.toml", config)
+
+#let bitwise = raw(chip.name)
+
+#show: book-page.with(title: "BRANCH chip")
+
+= #bitwise chip
+
+== Columns
+#let nr_variables = total_nr_variables(chip)
+#let nr_columns = total_nr_instantiated_columns(chip, config)
+#let nr_precomputed = ("input", "output").map(c => chip.variables.at(c)).flatten().len()
+
+The #bitwise chip is comprised of #nr_variables variables that are expressed using #nr_columns columns.
+Of these, the _input_ and _output_ variables (#nr_precomputed in total) are precomputed.
+#render_chip_column_table(chip, config)
+
+*Note*: This table contains one row for every possible value of `(X, Y, Z)`.
+As such, it has length $2^8 dot 2^8 dot 2^4 = 2^(20)$.
+
+== Lookup
+This chip adds the following interactions to the lookup:
+#render_constraint_table(chip, config)
+
+== Areas of Optimization
+The following ideas may prove to be optimizations for the #bitwise chip:
++ Extend `IS_BYTE[X]` to `ARE_BYTES[X, Y]`, such that two bytes are range checked at once. 
+  When only a single check is required, one can still execute `IS_BYTE[X] := ARE_BYTES[X, 0]`.
++ Drop `MSB8` column, and instead define the `MSB8` lookup as `MSB8<X> := MSB16[256X]`.
+  Note: currently, `MSB8` also implicity range checks the input `X` (the lookup fails if `X` is not a `Byte`).
+  This optimization should only be executed when all chips leveraging `MSB8` do _not_ need this implicit range check.
++ Place the 16-bit (`AND`, `OR`, `XOR`, `MSB16`, `ZERO`, etc.) and 20-bit (`HWSL`, `HWSLC`, `IS_B20`) lookups in separate tables.
++ Combine `HWSL` and `HWSLC` into a single lookup (see also \#119).

spec/book.typ

@@ -13,6 +13,7 @@
     #chapter("branch.typ")[BRANCH]
     #chapter("lt.typ")[LT]
     #chapter("mul.typ")[MUL chip]
+    #chapter("bitwise.typ")[BITWISE]
   ]
 )
 

spec/expr.typ

@@ -95,7 +95,15 @@
     "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) => {
+      if e.len() == 3 and type(e.at(1)) == int and type(e.at(2)) == str and e.at(2).len() == 1 {
+        // multiplication of a constant with one-letter variable. 
+        // Dropping the "dot"
+        cwrap(e.slice(1).map(rec.with(PREC.mul)).join(``), pp < PREC.mul)
+      } else {
+        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) => {
       assert(type(e.at(1)) == int and type(e.at(2)) == int, message: "Can only exponentiate constants")

spec/src/bitwise.toml

@@ -0,0 +1,200 @@
+name = "BITWISE"
+
+[[variables.input]]
+name = "X"
+type = "Byte"
+desc = ""
+precomputed = "true"
+
+[[variables.input]]
+name = "Y"
+type = "Byte"
+desc = ""
+precomputed = "true"
+
+[[variables.input]]
+name = "Z"
+type = "B4"
+desc = ""
+precomputed = "true"
+
+[[variables.output]]
+name = "AND"
+type = "Byte"
+desc = "the binary AND of `X` and `Y`"
+precomputed = "true"
+
+[[variables.output]]
+name = "OR"
+type = "Byte"
+desc = "the binary OR of `X` and `Y`"
+precomputed = "true"
+
+[[variables.output]]
+name = "XOR"
+type = "Byte"
+desc = "the binary XOR of `X` and `Y`"
+precomputed = "true"
+
+[[variables.output]]
+name = "MSB8"
+type = "Bit"
+desc = "the most significant bit of `X`"
+precomputed = "true"
+
+[[variables.output]]
+name = "MSB16"
+type = "Bit"
+desc = "the most significant bit of `Y`"
+precomputed = "true"
+
+[[variables.output]]
+name = "ZERO"
+type = "Bit"
+desc = "whether $#`X` = 0 and #`Y` = 0$"
+precomputed = "true"
+
+[[variables.output]]
+name = "SLL"
+type = "Half"
+desc = "`X||Y` logically left-shifted by `Z`: $((#`X` + 256#`Y`) #`<<` #`Z`) mod 2^16$"
+precomputed = "true"
+
+[[variables.output]]
+name = "SLLC"
+type = "Half"
+desc = "`X||Y` logically right-shifted by `Z`: $(#`X` + 256#`Y`) #`>>` (16 - #`Z`)$"
+precomputed = "true"
+
+[[variables.multiplicity]]
+name = "μ_AND"
+type = "BaseField"
+desc = ""
+
+[[variables.multiplicity]]
+name = "μ_OR"
+type = "BaseField"
+desc = ""
+
+[[variables.multiplicity]]
+name = "μ_XOR"
+type = "BaseField"
+desc = ""
+
+[[variables.multiplicity]]
+name = "μ_MSB8"
+type = "BaseField"
+desc = ""
+
+[[variables.multiplicity]]
+name = "μ_MSB16"
+type = "BaseField"
+desc = ""
+
+[[variables.multiplicity]]
+name = "μ_ZERO"
+type = "BaseField"
+desc = ""
+
+[[variables.multiplicity]]
+name = "μ_IS_BYTE"
+type = "BaseField"
+desc = ""
+
+[[variables.multiplicity]]
+name = "μ_IS_HALF"
+type = "BaseField"
+desc = ""
+
+[[variables.multiplicity]]
+name = "μ_IS_B20"
+type = "BaseField"
+desc = ""
+
+[[variables.multiplicity]]
+name = "μ_HWSL"
+type = "BaseField"
+desc = ""
+
+[[variables.multiplicity]]
+name = "μ_HWSLC"
+type = "BaseField"
+desc = ""
+
+
+[[constraint_groups]]
+name = "contributions"
+
+[[constraints.contributions]]
+kind = "interaction"
+tag = "AND_BYTE"
+input = ["X", "Y"]
+output = "AND"
+multiplicity = ["-", "μ_AND"]
+
+[[constraints.contributions]]
+kind = "interaction"
+tag = "OR_BYTE"
+input = ["X", "Y"]
+output = "OR"
+multiplicity = ["-", "μ_OR"]
+
+[[constraints.contributions]]
+kind = "interaction"
+tag = "XOR_BYTE"
+input = ["X", "Y"]
+output = "XOR"
+multiplicity = ["-", "μ_XOR"]
+
+[[constraints.contributions]]
+kind = "interaction"
+tag = "MSB8"
+input = ["X"]
+output = "MSB8"
+multiplicity = ["-", "μ_MSB8"]
+
+[[constraints.contributions]]
+kind = "interaction"
+tag = "MSB16"
+input = [["+", "X", ["*", 256, "Y"]]]
+output = "MSB16"
+multiplicity = ["-", "μ_MSB16"]
+
+[[constraints.contributions]]
+kind = "interaction"
+tag = "ZERO"
+input = [["+", "X", ["*", 256, "Y"]]]
+output = "ZERO"
+multiplicity = ["-", "μ_ZERO"]
+
+[[constraints.contributions]]
+kind = "interaction"
+tag = "IS_BYTE"
+input = ["X"]
+multiplicity = ["-", "μ_IS_BYTE"]
+
+[[constraints.contributions]]
+kind = "interaction"
+tag = "IS_HALF"
+input = [["+", "X", ["*", 256, "Y"]]]
+multiplicity = ["-", "μ_IS_HALF"]
+
+[[constraints.contributions]]
+kind = "interaction"
+tag = "IS_B20"
+input = [["+", "X", ["*", 256, "Y"], ["*", 65536, "Z"]]]
+multiplicity = ["-", "μ_IS_B20"]
+
+[[constraints.contributions]]
+kind = "interaction"
+tag = "HWSL"
+input = [["+", "X", ["*", 256, "Y"]], "Z"]
+output = "SLL"
+multiplicity = ["-", "μ_HWSL"]
+
+[[constraints.contributions]]
+kind = "interaction"
+tag = "HWSLC"
+input = [["+", "X", ["*", 256, "Y"]], "Z"]
+output = "SLLC"
+multiplicity = ["-", "μ_HWSLC"]