spec: interaction counter

spec/add.typ

@@ -1,12 +1,15 @@
 #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
+#import "/chip.typ": render_chip_column_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)
 
 #show: book-page(chip.name)
 
+#set_nr_interactions(chip, name: "SUB")
+#let nr_interactions = compute_nr_interactions(chip)
+
 #let add = raw(chip.name)
 #let sub = raw("SUB")
 
@@ -19,6 +22,7 @@ in both conditional and unconditional versions.
 It constrains that $#`diff` equiv #`lhs` - #`rhs` (mod 2^64)$ when the expression `cond` is non-zero.
 
 = Variables
+This template introduces #nr_interactions interaction(s).
 #render_chip_column_table(chip, config)
 
 = Assumptions

spec/branch.typ

@@ -3,6 +3,7 @@
 #import "/chip.typ": (
   render_chip_assumptions,
   render_chip_column_table,
+  compute_nr_interactions,
   total_nr_variables,
   total_nr_instantiated_columns,
   render_constraint_table,
@@ -20,8 +21,9 @@ The #branch chip computes the target address of a branching instruction.
 = Columns
 #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:
+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)
 
 = Assumptions

spec/chip.typ

@@ -24,6 +24,76 @@
   .sum()
 }
 
+// Given a constraint, compute the number of interactions it induces
+#let get_constraint_interaction_count(constraint) = {
+  let iters = if "iters" in constraint {
+    constraint.iters
+  } else if "iter" in constraint {
+    (constraint.iter,)
+  } else {
+    ()
+  }
+
+  iters.map(i => {
+    assert(
+      i.len() == 3 and type(i.at(1)) == int and type(i.at(2)) == int,
+      message: "invalid iter: " + repr(i),
+    )
+    i.at(2) - i.at(1) + 1
+  })
+  .product(default: 1)
+}
+
+// Compute the number of interactions performed by `chip` and
+// store it as metadata under the `<interaction_count>` label
+// with tag `chip.name`. This tag is overwritten by `name` when specified.
+#let set_nr_interactions(chip, name: none) = {
+  if name == none {
+      name = chip.name
+    }
+
+  let constraints = chip
+    .constraints
+    .values()
+    .flatten()
+
+  // nr. of direct interactions
+  let nr-direct-interactions = constraints
+    .filter(c => c.kind == "interaction")
+    .map(get_constraint_interaction_count)
+    .sum(default: 0)
+
+  let template-constraints = constraints.filter(c => c.kind == "template")
+
+  context {
+    let lookup-table = query(<interaction_count>).map(x => x.value).sum(default: (:))
+
+    // nr. of indirect interactions through templates
+    let nr-indirect-interactions = template-constraints
+      .map(c => {
+        assert(c.tag in lookup-table, message: "cannot find interaction_count for " + repr(c))
+
+        let template-interactions = lookup-table.at(c.tag)
+        let iter-size = get_constraint_interaction_count(c)
+        iter-size * template-interactions 
+      })
+      .sum(default: 0)
+
+    let total-nr-interactions = nr-direct-interactions + nr-indirect-interactions
+
+    [#metadata((str(name): total-nr-interactions)) <interaction_count>]
+  }
+}
+
+#let compute_nr_interactions(chip) = {
+  set_nr_interactions(chip)
+  context {
+    let lut = query(<interaction_count>).map(c => c.value).sum(default: (:))
+    assert(chip.name in lut, message: "no interaction_count specified for " + repr(chip.name))
+    lut.at(chip.name)
+  }
+}
+
 // Return a list of iterators needed by `obj`. Taken from `iters` or `iter`.
 // Prepend `name` to every iterator, if given.
 #let iters_of(obj, name: none) = {

spec/cpu.typ

@@ -5,6 +5,7 @@
   render_chip_column_table,
   total_nr_variables,
   total_nr_instantiated_columns,
+  compute_nr_interactions,
   render_constraint_table,
   render_chip_padding_table,
 )
@@ -21,8 +22,9 @@ It bases its decisions on the entry of the `DECODE` table (@decode) correspondin
 = Columns
 #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:
+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)
 
 = Assumptions

spec/dvrm.typ

@@ -4,12 +4,12 @@
   render_chip_column_table,
   total_nr_variables,
   total_nr_instantiated_columns,
+  compute_nr_interactions,
   render_constraint_table,
   render_chip_padding_table,
   render_chip_assumptions
 )
 
-
 #let config = load_config()
 #let chip = load_chip("src/dvrm.toml", config)
 
@@ -22,8 +22,9 @@ The #dvrm chip provides division and remainder functionality, both signed and un
 = Columns
 #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:
+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)
 
 = Assumptions

spec/ecall.typ

@@ -4,6 +4,7 @@
   render_chip_column_table,
   total_nr_variables,
   total_nr_instantiated_columns,
+  compute_nr_interactions,
   render_constraint_table,
   render_chip_assumptions,
   render_chip_padding_table,
@@ -32,8 +33,9 @@ where `A0`-`A7` are symbolic names for the registers `x10`-`x17`
 == Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
+#let nr_halt_interactions = compute_nr_interactions(chip)
 
-The #halt chip leverages #nr_variables variable, spanning #nr_columns columns:
+The #halt chip leverages #nr_variables variable, spanning #nr_columns columns and leverages #nr_halt_interactions interaction(s):
 #render_chip_column_table(chip, config)
 
 == Assumptions
@@ -76,8 +78,9 @@ As such, no padding is defined.
 == Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
+#let nr_commit_interactions = compute_nr_interactions(chip)
 
-The #commit chip leverages #nr_variables variables, spanning #nr_columns columns:
+The #commit chip leverages #nr_variables variables, spanning #nr_columns columns and leverages #nr_commit_interactions interactions:
 #render_chip_column_table(chip, config)
 
 == Constraints

spec/is_bit.typ

@@ -1,12 +1,14 @@
 #import "/book.typ": book-page
 #import "/src.typ": load_config, load_chip
-#import "/chip.typ": render_chip_column_table, render_constraint_table
+#import "/chip.typ": render_chip_column_table, render_constraint_table, set_nr_interactions
 
 #let config = load_config()
 #let chip = load_chip("src/is_bit.toml", config)
 
 #show: book-page(chip.name)
 
+#set_nr_interactions(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.

spec/load.typ

@@ -5,6 +5,7 @@
   render_chip_column_table,
   render_chip_padding_table,
   render_constraint_table,
+  compute_nr_interactions,
   total_nr_instantiated_columns,
   total_nr_variables,
 )
@@ -21,8 +22,9 @@ It delegates low-level memory handling to the `MEMW` chip (@memw).
 = Columns
 #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:
+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)
 
 = Assumptions

spec/lt.typ

@@ -7,6 +7,7 @@
   render_constraint_table,
   total_nr_instantiated_columns,
   total_nr_variables,
+  compute_nr_interactions,
 )
 
 #let config = load_config()
@@ -20,8 +21,9 @@ The #lt chip constrains an indicator bit for the less-than relation, signed or u
 = Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
+#let nr_interactions = compute_nr_interactions(chip)
 
-The `LT` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns:
+The #lt 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)
 
 = Assumptions

spec/memw.typ

@@ -5,6 +5,7 @@
   render_chip_column_table,
   total_nr_variables,
   total_nr_instantiated_columns,
+  compute_nr_interactions,
   render_constraint_table,
   render_chip_padding_table
 )
@@ -24,8 +25,9 @@ in order to satisfy the design of the memory argument (@memory).
 = Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
+#let nr_memw_interactions = compute_nr_interactions(chip)
 
-The `MEMW` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns:
+The #memw chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_memw_interactions interaction(s):
 #render_chip_column_table(chip, config)
 
 = Assumptions
@@ -73,6 +75,7 @@ The table can be padded to the next power of two with the following value assign
 
 #let alignedchip = load_chip("src/memw_aligned.toml", config)
 #let aligned = raw(alignedchip.name)
+#let nr_aligned_interactions = compute_nr_interactions(alignedchip)
 
 When a memory access happens at an address with proper alignment for its access size
 (i.e., adding the access size to `base_address`'s lowest limb does not overflow), 
@@ -87,7 +90,7 @@ Further logic remains essentially the same, so we briefly present the relevant t
 #let nr_variables = total_nr_variables(alignedchip)
 #let nr_columns = total_nr_instantiated_columns(alignedchip, config)
 
-The #aligned chip only needs #nr_variables variables, expressed through #nr_columns columns.
+The #aligned chip only needs #nr_variables variables, expressed through #nr_columns columns; it leverages #nr_aligned_interactions interactions.
 #render_chip_column_table(alignedchip, config)
 #render_chip_assumptions(alignedchip, config)
 #render_constraint_table(alignedchip, config)
@@ -119,8 +122,9 @@ Note moreover that this chip does not guard against misaligned register access f
 == Columns
 #let nr_variables = total_nr_variables(register_chip)
 #let nr_columns = total_nr_instantiated_columns(register_chip, config)
+#let nr_memw_r_interactions = compute_nr_interactions(register_chip)
 
-The #reg chip is comprised of #nr_variables variables that are expressed using #nr_columns columns:
+The #reg chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_memw_r_interactions interactions:
 #render_chip_column_table(register_chip, config)
 
 == Assumptions

spec/mul.typ

@@ -4,6 +4,7 @@
   render_chip_column_table,
   total_nr_variables,
   total_nr_instantiated_columns,
+  compute_nr_interactions,
   render_constraint_table,
   render_chip_assumptions,
   render_chip_padding_table,
@@ -22,8 +23,9 @@ as well as providing access to the low and high halfs of the multiplication resu
 = Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
+#let nr_interactions = compute_nr_interactions(chip)
 
-The `MUL` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns:
+The #mul 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)
 
 #let stackrel(top, bottom) = {

spec/neg.typ

@@ -1,17 +1,20 @@
 #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
+#import "/chip.typ": render_chip_column_table, render_chip_assumptions, render_constraint_table, compute_nr_interactions,
 
 #let config = load_config()
 #let chip = load_chip("src/neg.toml", config)
 #show: book-page(chip.name)
 
+#let nr_interactions = compute_nr_interactions(chip)
+
 #let neg = raw(chip.name)
 
 #neg is a constraint template that is used to assert that $#`neg` = -#`x`$, under the condition that `cond` is non-zero.
 It requires `cond` to be a bit.
 
 = Variables
+This template introduces #nr_interactions interaction(s).
 #render_chip_column_table(chip, config)
 
 = Assumptions

spec/shift.typ

@@ -4,6 +4,7 @@
   render_chip_column_table,
   total_nr_variables,
   total_nr_instantiated_columns,
+  compute_nr_interactions,
   render_constraint_table,
   render_chip_assumptions,
   render_chip_padding_table,
@@ -36,8 +37,9 @@ Here, `<<` and `>>` denote the _logical_ left and right shift operations, while
 = Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
+#let nr_interactions = compute_nr_interactions(chip)
 
-The `SHIFT` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns:
+The `SHIFT` 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)
 
 = Assumptions

spec/sign.typ

@@ -1,19 +1,21 @@
 #import "/book.typ": book-page
 #import "/src.typ": load_config, load_chip
-#import "/chip.typ": render_chip_column_table,   render_chip_assumptions, render_constraint_table
-
+#import "/chip.typ": render_chip_column_table, total_nr_variables, render_chip_assumptions, render_constraint_table, compute_nr_interactions,
 
 #let config = load_config()
 #let chip = load_chip("src/sign.toml", config)
 #show: book-page(chip.name)
 
+#let nr_variables = total_nr_variables(chip)
+#let nr_interactions = compute_nr_interactions(chip)
+
 #let sign = raw(chip.name)
 
 #sign is a constraint template that is used to extract a `Half`word's sign.
 It constrains that `sign` is set to `1` when both `X`'s most significant bit and `signed` are $1$, and $0$ otherwise.
 
 = Variables
-The #sign template operates on three variables:
+The #sign template operates on three variables and introduces #nr_interactions interaction(s):
 #render_chip_column_table(chip, config)
 
 = Assumptions