spec: cleanup before v0.2

spec/about_ecalls.typ

@@ -1,7 +1,7 @@
 #import "/book.typ": book-page, aside
 #import "/src.typ": load_config, load_chip
 #import "/chip.typ": (
-  render_chip_column_table,
+  render_chip_variable_table,
   total_nr_variables,
   total_nr_instantiated_columns,
   render_constraint_table,

spec/add.typ

@@ -1,6 +1,6 @@
 #import "/book.typ": book-page, et
 #import "/src.typ": load_config, load_chip
-#import "/chip.typ": render_chip_column_table, render_chip_assumptions, render_constraint_table, set_nr_interactions, compute_nr_interactions,
+#import "/chip.typ": render_chip_variable_table, render_chip_assumptions, render_constraint_table, set_nr_interactions, compute_nr_interactions,
 
 #let config = load_config()
 #let chip = load_chip("src/add.toml", config)
@@ -23,7 +23,7 @@ It constrains that $#`diff` equiv #`lhs` - #`rhs` (mod 2^64)$ when the expressio
 
 = Variables
 This template introduces #nr_interactions interaction(s).
-#render_chip_column_table(chip, config)
+#render_chip_variable_table(chip, config)
 
 = Assumptions
 #render_chip_assumptions(chip, config)

spec/bitwise.typ

@@ -2,7 +2,7 @@
 #import "/src.typ": load_config, load_chip
 #import "/chip.typ": (
   render_chip_assumptions,
-  render_chip_column_table,
+  render_chip_variable_table,
   total_nr_variables,
   total_nr_instantiated_columns,
   render_constraint_table,
@@ -19,14 +19,14 @@
 The #bitwise chips deal with precomputed lookup tables for bitwise boolean operations
 and convenience functionalities over small domains.
 
-= Columns
+= Variables
 #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)
+#render_chip_variable_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)$.
@@ -35,7 +35,7 @@ As such, it has length $2^8 dot 2^8 dot 2^4 = 2^(20)$.
 This chip adds the following interactions to the lookup:
 #render_constraint_table(chip, config)
 
-= Areas of Optimization
+= Notes/Optimizations
 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]`.

spec/book.typ

@@ -9,39 +9,39 @@
   version: "0.2",
   summary: (
     ("PROOF SYSTEM", (
-        ("logup.typ", [LogUp argument], <logup>),
+        ("logup.typ", [`LogUp` argument], <logup>),
         ("memory.typ", [Memory argument], <memory>),
     )),
     ("OVERVIEW", (
         ("variables.typ", [Variables], <vars>),
         ("signatures.typ", [Signatures], <signatures>),
     )),
     ("TEMPLATES", (
-      ("is_bit.typ", [IS_BIT template], <isbit>),
-      ("sign.typ", [SIGN template], <sign>),
-      ("add.typ", [ADD/SUB template], <add>),
-      ("neg.typ", [NEG template], <neg>),
+      ("is_bit.typ", [`IS_BIT` template], <isbit>),
+      ("sign.typ", [`SIGN` template], <sign>),
+      ("add.typ", [`ADD`/`SUB` template], <add>),
+      ("neg.typ", [`NEG` template], <neg>),
     )),
     ("MEMORY", (
-      ("memw.typ", [MEMW chip], <memw>),
+      ("memw.typ", [`MEMW` chip], <memw>),
     )),
     ("CPU", (
-      ("decode.typ", [DECODE table], <decode>),
-      ("cpu.typ", [CPU chip], <cpu>),
+      ("decode.typ", [`DECODE` table], <decode>),
+      ("cpu.typ", [`CPU` chip], <cpu>),
     )),
     ("ALU", (
-      ("shift.typ", [SHIFT chip], <shift>),
-      ("branch.typ", [BRANCH chip], <branch>),
-      ("lt.typ", [LT chip], <lt>),
-      ("mul.typ", [MUL chip], <mul>),
-      ("dvrm.typ", [DVRM chip], <dvrm>),
-      ("load.typ", [LOAD chip], <load>),
-      ("bitwise.typ", [BITWISE chips], <bitwise>),
+      ("shift.typ", [`SHIFT` chip], <shift>),
+      ("branch.typ", [`BRANCH` chip], <branch>),
+      ("lt.typ", [`LT` chip], <lt>),
+      ("mul.typ", [`MUL` chip], <mul>),
+      ("dvrm.typ", [`DVRM` chip], <dvrm>),
+      ("load.typ", [`LOAD` chip], <load>),
+      ("bitwise.typ", [`BITWISE` chips], <bitwise>),
     )),
     ("ECALLS", (
-      ("about_ecalls.typ", [About ECALL], <ecall>),
-      ("halt.typ", [HALT chip], <halt>),
-      ("commit.typ", [COMMIT chip], <commit>),
+      ("about_ecalls.typ", [About `ECALL`], <ecall>),
+      ("halt.typ", [`HALT` chip], <halt>),
+      ("commit.typ", [`COMMIT` chip], <commit>),
     ))
   )
 )

spec/branch.typ

@@ -2,7 +2,7 @@
 #import "/src.typ": load_config, load_chip
 #import "/chip.typ": (
   render_chip_assumptions,
-  render_chip_column_table,
+  render_chip_variable_table,
   compute_nr_interactions,
   total_nr_variables,
   total_nr_instantiated_columns,
@@ -18,13 +18,13 @@
 
 The #branch chip computes the target address of a branching instruction.
 
-= Columns
+= Variables
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
 #let nr_interactions = compute_nr_interactions(chip)
 
 The #branch chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s):
-#render_chip_column_table(chip, config)
+#render_chip_variable_table(chip, config)
 
 = Assumptions
 

spec/chip.typ

@@ -142,11 +142,11 @@
         ([#raw(var.name)], [$:=$], [#expr_to_math(var.pad)],)
       }
     },
-  ), caption: [Overview of padding values for #chip.name chip.])
+  ))
 }
 
-/// Generates a table listing `chip`'s columns.
-#let render_chip_column_table(chip, config) = {
+/// Generates a table listing `chip`'s variables.
+#let render_chip_variable_table(chip, config) = {
 
   // Render a definition's iterators
   let render_def_iters(iters) = {
@@ -235,7 +235,7 @@
       }
       (table.cell(colspan: 4, []), )
     },
-  ), caption: [Column overview of #chip.name chip.])
+  ))
 }
 
 #let cref(obj, body) = {
@@ -278,7 +278,7 @@
     ..for assumption in chip.assumptions {
       ([#tag(assumption)], [#iters(assumption)], [#eval(assumption.desc, mode: "markup")])
     },
-  ), caption: [Assumption overview of #chip.name chip.])
+  ))
 }
 
 /// Generates a table listing all interactions initiated by `chip`'s.
@@ -389,5 +389,5 @@
         }
       }
     }
-  ), caption: [Constraint overview of #chip.name chip.])
+  ))
 }

spec/commit.typ

@@ -1,7 +1,7 @@
 #import "/book.typ": book-page, aside
 #import "/src.typ": load_config, load_chip
 #import "/chip.typ": (
-  render_chip_column_table,
+  render_chip_variable_table,
   total_nr_variables,
   total_nr_instantiated_columns,
   compute_nr_interactions,
@@ -16,13 +16,13 @@
 #let chip = load_chip("src/commit.toml", config)
 #let commit = raw(chip.name)
 
-= Columns
+= Variables
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
 #let nr_interactions = compute_nr_interactions(chip)
 
 The #commit chip leverages #nr_variables variables, spanning #nr_columns columns and leverages #nr_interactions interactions:
-#render_chip_column_table(chip, config)
+#render_chip_variable_table(chip, config)
 
 = Constraints
 In this VM, committing is considered equivalent to writing a value to `stdout`.

spec/cpu.typ

@@ -2,7 +2,7 @@
 #import "/src.typ": load_config, load_chip
 #import "/chip.typ": (
   render_chip_assumptions,
-  render_chip_column_table,
+  render_chip_variable_table,
   total_nr_variables,
   total_nr_instantiated_columns,
   compute_nr_interactions,
@@ -19,13 +19,13 @@
 The #cpu chip coordinates memory accesses and dispatches to other chips for arithmetic and logical operations.
 It bases its decisions on the entry of the `DECODE` table (@decode) corresponding the the current program counter (PC).
 
-= Columns
+= Variables
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
 #let nr_interactions = compute_nr_interactions(chip)
 
 The #cpu chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s):
-#render_chip_column_table(chip, config)
+#render_chip_variable_table(chip, config)
 
 = Assumptions
 #render_chip_assumptions(chip, config)

spec/decode.typ

@@ -2,7 +2,7 @@
 #import "/src.typ": load_config, load_chip
 #import "/chip.typ": (
   render_chip_assumptions,
-  render_chip_column_table,
+  render_chip_variable_table,
   total_nr_variables,
   total_nr_instantiated_columns,
   render_constraint_table,
@@ -21,12 +21,12 @@ For reasons of efficiency, data in this table is significantly compressed.
 Since reasoning about this compressed form is needlessly complex, the `decode (uncompressed)` section presents the same table in uncompressed form, and explains how to decode `RV64IM` assembly instructions to it.
 Instructions on how to compress the uncompressed table to form the compressed decode table, can be derived from the `packed_decode` variable provided below.
 
-= Columns
+= Variables
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
 
 The #decode table is comprised of #nr_variables variables that are expressed using #nr_columns columns:
-#render_chip_column_table(chip, config)
+#render_chip_variable_table(chip, config)
 
 = Padding
 The #decode table must be padded to a length that is a power of two.
@@ -46,7 +46,7 @@ Note that the below table is _not_ used in practice: it is solely used for the p
 #let config = load_config()
 #let uncompressed_chip = load_chip("src/decode_uncompressed.toml", config)
 
-#render_chip_column_table(uncompressed_chip, config)
+#render_chip_variable_table(uncompressed_chip, config)
 
 We will illustrate how each instruction should be expressed in this (uncompressed) decoding table.
 The columns of the accompanying table represent the following:
@@ -93,9 +93,7 @@ To indicate an instruction is provided in compressed form, the `c_type` flag is
     ..lines.flatten(),
     table.hline(stroke: 1.5pt),
     table.footer([*Operation*], [*op-flag*], [*`w_instr`*], [*`signed`*], [*other*]),
-    ),  
-    caption: [Decoding table]
-  )
+  ))
 }
 
 #let decoding = (

spec/dvrm.typ

@@ -1,7 +1,7 @@
 #import "/book.typ": book-page
 #import "/src.typ": load_config, load_chip
 #import "/chip.typ": (
-  render_chip_column_table,
+  render_chip_variable_table,
   total_nr_variables,
   total_nr_instantiated_columns,
   compute_nr_interactions,
@@ -19,13 +19,13 @@
 
 The #dvrm chip provides division and remainder functionality, both signed and unsigned.
 
-= Columns
+= Variables
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
 #let nr_interactions = compute_nr_interactions(chip)
 
 The #dvrm chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s):
-#render_chip_column_table(chip, config)
+#render_chip_variable_table(chip, config)
 
 = Assumptions
 #render_chip_assumptions(chip, config)

spec/halt.typ

@@ -1,7 +1,7 @@
 #import "/book.typ": book-page, aside
 #import "/src.typ": load_config, load_chip
 #import "/chip.typ": (
-  render_chip_column_table,
+  render_chip_variable_table,
   total_nr_variables,
   total_nr_instantiated_columns,
   compute_nr_interactions,
@@ -16,13 +16,13 @@
 #let chip = load_chip("src/halt.toml", config)
 #let halt = raw(chip.name)
 
-= Columns
+= Variables
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
 #let nr_interactions = compute_nr_interactions(chip)
 
-The #halt chip leverages #nr_variables variable, spanning #nr_columns columns and leverages #nr_interactions interactions::
-#render_chip_column_table(chip, config)
+The #halt chip leverages #nr_variables variable, spanning #nr_columns columns and leverages #nr_interactions interactions:
+#render_chip_variable_table(chip, config)
 
 = Assumptions
 It is assumed the input is range checked:

spec/is_bit.typ

@@ -1,22 +1,23 @@
 #import "/book.typ": book-page
 #import "/src.typ": load_config, load_chip
-#import "/chip.typ": render_chip_column_table, render_constraint_table, set_nr_interactions
+#import "/chip.typ": render_chip_variable_table, render_constraint_table, set_nr_interactions, total_nr_variables
 
 #let config = load_config()
 #let chip = load_chip("src/is_bit.toml", config)
 
 #show: book-page(chip.name)
 
 #set_nr_interactions(chip)
+#let nr_variables = total_nr_variables(chip)
 
 #let is_bit = raw(chip.name)
 
 #is_bit is a constraint template that is used to assert that a variable lies in the range ${0, 1}$ if some second variable is non-zero.
 Barring exceptional cases, this template is used to assert that a variable of type `Bit` assumes a valid value under some condition.
 
 = Variables
-The #is_bit template operates on two variables: `cond` and `X`:
-#render_chip_column_table(chip, config)
+The #is_bit template operates on #nr_variables variables:
+#render_chip_variable_table(chip, config)
 
 = Constraints
 It takes only one constraint to enforce that `X` must be either $0$ or $1$ whenever $#`cond` eq.not 0$:
@@ -26,7 +27,7 @@ It takes only one constraint to enforce that `X` must be either $0$ or $1$ whene
 - As described earlier, the `cond` variable must be describable by a degree-1 (i.e., linear) expression.
   This is to make sure that @isbit:c:isbit's expression has degree at most 3.
 
-= Proof of correctness
+== Correctness argument
 If `cond` is $0$, @isbit:c:isbit is trivially satisfied: `X` can assume any value and the polynomial constraint will evaluate to $0$ regardless. 
 When $#`cond` eq.not 0$, it follows that the statement can only be proven when $#`X` (1-#`X`) equiv 0 mod p$, with $p$ the modulus of the field.
 Because `BaseField` is a prime field, this equality is only satisfied if either $#`X` equiv 0 mod p$ or $1-#`X` equiv 0 mod p$.

spec/load.typ

@@ -2,7 +2,7 @@
 #import "/src.typ": load_config, load_chip
 #import "/chip.typ": (
   render_chip_assumptions,
-  render_chip_column_table,
+  render_chip_variable_table,
   render_chip_padding_table,
   render_constraint_table,
   compute_nr_interactions,
@@ -19,13 +19,13 @@
 The #load chip provides functionality to read values from memory and sign-extend them where appropriate.
 It delegates low-level memory handling to the `MEMW` chip (@memw).
 
-= Columns
+= Variables
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
 #let nr_interactions = compute_nr_interactions(chip)
 
 The #load chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s):
-#render_chip_column_table(chip, config)
+#render_chip_variable_table(chip, config)
 
 = Assumptions
 #render_chip_assumptions(chip, config)