diff --git a/spec/bitwise.typ b/spec/bitwise.typ new file mode 100644 index 000000000..34ec6dd10 --- /dev/null +++ b/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 := 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). diff --git a/spec/book.typ b/spec/book.typ index 01a362879..1bf944862 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -13,6 +13,7 @@ #chapter("branch.typ")[BRANCH] #chapter("lt.typ")[LT] #chapter("mul.typ")[MUL chip] + #chapter("bitwise.typ")[BITWISE] ] ) diff --git a/spec/expr.typ b/spec/expr.typ index bf705b462..751493619 100644 --- a/spec/expr.typ +++ b/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") diff --git a/spec/src/bitwise.toml b/spec/src/bitwise.toml new file mode 100644 index 000000000..2eeec4059 --- /dev/null +++ b/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"] \ No newline at end of file