From 6b8471f9cc0c2fa0f9b9c4bce52df0314d42984e Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 26 Mar 2026 16:31:57 +0100 Subject: [PATCH 1/9] spec: recursively compute chip interaction count --- spec/chip.typ | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/spec/chip.typ b/spec/chip.typ index f3ac28a74..78d7386e2 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -24,6 +24,49 @@ .sum() } +#let set_nr_interactions(chip) = { + let constraints = chip + .constraints + .values() + .flatten() + + // nr. of direct interactions + let nr-direct-interactions = constraints + .filter(c=>c.kind == "interaction") + .map(c => { + let x = c.at("iter", default: (0, 0, 0)) + x.at(2) - x.at(1) + 1 + }) + .sum(default: 0) + + let template-constraints = constraints.filter(c=>c.kind == "template") + + context { + let lookup-table = query().map(x => x.value).sum(default:(:)) + + // nr. of indirect interactions through templates + let nr-indirect-interactions = template-constraints + .map(c => { + let x = c.at("iter", default: (0, 0, 0)) + let iter-size = x.at(2) - x.at(1) + 1 + + let template-interactions = lookup-table.at(c.tag, default: 0) + iter-size * template-interactions + }) + .sum(default: 0) + + let total-nr-interactions = nr-direct-interactions + nr-indirect-interactions + + [#metadata((chip.name: total-nr-interactions)) ] + } +} + +#let get_nr_interactions(chip) = { + context { + query().map(c=>c.value).sum().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) = { From 9c18a2a580e11c8222f8b99af776b3d1637399a0 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 26 Mar 2026 16:32:39 +0100 Subject: [PATCH 2/9] spec: print interaction count per chip --- spec/add.typ | 6 +++++- spec/branch.typ | 6 +++++- spec/cpu.typ | 6 +++++- spec/dvrm.typ | 7 +++++-- spec/ecall.typ | 10 ++++++++-- spec/is_bit.typ | 5 ++++- spec/load.typ | 6 +++++- spec/lt.typ | 6 +++++- spec/memw.typ | 14 +++++++++++--- spec/mul.typ | 6 +++++- spec/neg.typ | 6 +++++- spec/shift.typ | 6 +++++- spec/sign.typ | 8 +++++--- 13 files changed, 73 insertions(+), 19 deletions(-) diff --git a/spec/add.typ b/spec/add.typ index d2afb1788..a678893e5 100644 --- a/spec/add.typ +++ b/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, get_nr_interactions, #let config = load_config() #let chip = load_chip("src/add.toml", config) #show: book-page(chip.name) +#set_nr_interactions(chip) +#let nr_interactions = get_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 diff --git a/spec/branch.typ b/spec/branch.typ index 90503e862..c6bb9254e 100644 --- a/spec/branch.typ +++ b/spec/branch.typ @@ -3,6 +3,8 @@ #import "/chip.typ": ( render_chip_assumptions, render_chip_column_table, + set_nr_interactions, + get_nr_interactions, total_nr_variables, total_nr_instantiated_columns, render_constraint_table, @@ -20,8 +22,10 @@ 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) +#set_nr_interactions(chip) +#let nr_interactions = get_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 diff --git a/spec/cpu.typ b/spec/cpu.typ index 08fe1533d..16fa4545b 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -5,6 +5,8 @@ render_chip_column_table, total_nr_variables, total_nr_instantiated_columns, + set_nr_interactions, + get_nr_interactions, render_constraint_table, render_chip_padding_table, ) @@ -21,8 +23,10 @@ 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) +#set_nr_interactions(chip) +#let nr_interactions = get_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 diff --git a/spec/dvrm.typ b/spec/dvrm.typ index 920aec075..a42f8dff6 100644 --- a/spec/dvrm.typ +++ b/spec/dvrm.typ @@ -4,12 +4,13 @@ render_chip_column_table, total_nr_variables, total_nr_instantiated_columns, + set_nr_interactions, + get_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 +23,10 @@ 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) +#set_nr_interactions(chip) +#let nr_interactions = get_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 diff --git a/spec/ecall.typ b/spec/ecall.typ index 3b82019db..754172bac 100644 --- a/spec/ecall.typ +++ b/spec/ecall.typ @@ -4,6 +4,8 @@ render_chip_column_table, total_nr_variables, total_nr_instantiated_columns, + set_nr_interactions, + get_nr_interactions, render_constraint_table, render_chip_assumptions, render_chip_padding_table, @@ -32,8 +34,10 @@ 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) +#set_nr_interactions(chip) +#let nr_halt_interactions = get_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 +80,10 @@ As such, no padding is defined. == Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) +#set_nr_interactions(chip) +#let nr_commit_interactions = get_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 diff --git a/spec/is_bit.typ b/spec/is_bit.typ index b09242fe4..bb2690afc 100644 --- a/spec/is_bit.typ +++ b/spec/is_bit.typ @@ -1,12 +1,15 @@ #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, get_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 nr_interactions = get_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. diff --git a/spec/load.typ b/spec/load.typ index b12e1c04d..a486e83cf 100644 --- a/spec/load.typ +++ b/spec/load.typ @@ -5,6 +5,8 @@ render_chip_column_table, render_chip_padding_table, render_constraint_table, + set_nr_interactions, + get_nr_interactions, total_nr_instantiated_columns, total_nr_variables, ) @@ -21,8 +23,10 @@ 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) +#set_nr_interactions(chip) +#let nr_interactions = get_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 diff --git a/spec/lt.typ b/spec/lt.typ index 8e55b390b..433abac18 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -7,6 +7,8 @@ render_constraint_table, total_nr_instantiated_columns, total_nr_variables, + set_nr_interactions, + get_nr_interactions, ) #let config = load_config() @@ -20,8 +22,10 @@ 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) +#set_nr_interactions(chip) +#let nr_interactions = get_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 diff --git a/spec/memw.typ b/spec/memw.typ index 1c7a1e6e5..49aff8a4d 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -5,6 +5,8 @@ render_chip_column_table, total_nr_variables, total_nr_instantiated_columns, + set_nr_interactions, + get_nr_interactions, render_constraint_table, render_chip_padding_table ) @@ -24,8 +26,10 @@ 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) +#set_nr_interactions(chip) +#let nr_memw_interactions = get_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 +77,8 @@ 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) +#set_nr_interactions(alignedchip) +#let nr_aligned_interactions = get_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 +93,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 +125,10 @@ 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) +#set_nr_interactions(register_chip) +#let nr_memw_r_interactions = get_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 diff --git a/spec/mul.typ b/spec/mul.typ index 68ab4a2b8..de4cc6fa3 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -4,6 +4,8 @@ render_chip_column_table, total_nr_variables, total_nr_instantiated_columns, + set_nr_interactions, + get_nr_interactions, render_constraint_table, render_chip_assumptions, render_chip_padding_table, @@ -22,8 +24,10 @@ 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) +#set_nr_interactions(chip) +#let nr_interactions = get_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) = { diff --git a/spec/neg.typ b/spec/neg.typ index d700892cb..bcab35cbf 100644 --- a/spec/neg.typ +++ b/spec/neg.typ @@ -1,17 +1,21 @@ #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, get_nr_interactions, #let config = load_config() #let chip = load_chip("src/neg.toml", config) #show: book-page(chip.name) +#set_nr_interactions(chip) +#let nr_interactions = get_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 diff --git a/spec/shift.typ b/spec/shift.typ index 289ade1d7..3b3478705 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -4,6 +4,8 @@ render_chip_column_table, total_nr_variables, total_nr_instantiated_columns, + set_nr_interactions, + get_nr_interactions, render_constraint_table, render_chip_assumptions, render_chip_padding_table, @@ -36,8 +38,10 @@ 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) +#set_nr_interactions(chip) +#let nr_interactions = get_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 diff --git a/spec/sign.typ b/spec/sign.typ index 7135ba9c6..06e766d5f 100644 --- a/spec/sign.typ +++ b/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, render_chip_assumptions, render_constraint_table, set_nr_interactions, get_nr_interactions, #let config = load_config() #let chip = load_chip("src/sign.toml", config) #show: book-page(chip.name) +#set_nr_interactions(chip) +#let nr_interactions = get_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 From 0ec9f7473b0d7a05325941505bae7054d86dd235 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 26 Mar 2026 16:34:24 +0100 Subject: [PATCH 3/9] spec: cleanup --- spec/branch.typ | 2 +- spec/cpu.typ | 2 +- spec/dvrm.typ | 2 +- spec/load.typ | 2 +- spec/lt.typ | 2 +- spec/memw.typ | 2 +- spec/mul.typ | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/spec/branch.typ b/spec/branch.typ index c6bb9254e..6a4d4feb1 100644 --- a/spec/branch.typ +++ b/spec/branch.typ @@ -25,7 +25,7 @@ The #branch chip computes the target address of a branching instruction. #set_nr_interactions(chip) #let nr_interactions = get_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): +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 diff --git a/spec/cpu.typ b/spec/cpu.typ index 16fa4545b..715b9d64d 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -26,7 +26,7 @@ It bases its decisions on the entry of the `DECODE` table (@decode) correspondin #set_nr_interactions(chip) #let nr_interactions = get_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): +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 diff --git a/spec/dvrm.typ b/spec/dvrm.typ index a42f8dff6..9a420d056 100644 --- a/spec/dvrm.typ +++ b/spec/dvrm.typ @@ -26,7 +26,7 @@ The #dvrm chip provides division and remainder functionality, both signed and un #set_nr_interactions(chip) #let nr_interactions = get_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): +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 diff --git a/spec/load.typ b/spec/load.typ index a486e83cf..8d1f61fdc 100644 --- a/spec/load.typ +++ b/spec/load.typ @@ -26,7 +26,7 @@ It delegates low-level memory handling to the `MEMW` chip (@memw). #set_nr_interactions(chip) #let nr_interactions = get_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): +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 diff --git a/spec/lt.typ b/spec/lt.typ index 433abac18..763227e53 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -25,7 +25,7 @@ The #lt chip constrains an indicator bit for the less-than relation, signed or u #set_nr_interactions(chip) #let nr_interactions = get_nr_interactions(chip) -The `LT` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): +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 diff --git a/spec/memw.typ b/spec/memw.typ index 49aff8a4d..2a77287b6 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -29,7 +29,7 @@ in order to satisfy the design of the memory argument (@memory). #set_nr_interactions(chip) #let nr_memw_interactions = get_nr_interactions(chip) -The `MEMW` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_memw_interactions interaction(s): +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 diff --git a/spec/mul.typ b/spec/mul.typ index de4cc6fa3..77d1cca43 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -27,7 +27,7 @@ as well as providing access to the low and high halfs of the multiplication resu #set_nr_interactions(chip) #let nr_interactions = get_nr_interactions(chip) -The `MUL` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): +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) = { From 1d8eb8ee38efaef3794d27115329d0752e071ef2 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 31 Mar 2026 15:03:54 +0200 Subject: [PATCH 4/9] spec/interaction-counter: add multi-dimensional iter support --- spec/chip.typ | 30 +++++++++++++++++++++++------- 1 file changed, 23 insertions(+), 7 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index 78d7386e2..0339b7912 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -24,6 +24,26 @@ .sum() } +// Given a constraint, compute the number of interactions it induces +#let get_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: "contains invalid iter: " + repr(i), + ) + i.at(2) - i.at(1) + 1 + }) + .product(default: 1) +} + #let set_nr_interactions(chip) = { let constraints = chip .constraints @@ -33,10 +53,7 @@ // nr. of direct interactions let nr-direct-interactions = constraints .filter(c=>c.kind == "interaction") - .map(c => { - let x = c.at("iter", default: (0, 0, 0)) - x.at(2) - x.at(1) + 1 - }) + .map(get_interaction_count) .sum(default: 0) let template-constraints = constraints.filter(c=>c.kind == "template") @@ -47,10 +64,9 @@ // nr. of indirect interactions through templates let nr-indirect-interactions = template-constraints .map(c => { - let x = c.at("iter", default: (0, 0, 0)) - let iter-size = x.at(2) - x.at(1) + 1 - + let iter-size = get_interaction_count(c) let template-interactions = lookup-table.at(c.tag, default: 0) + iter-size * template-interactions }) .sum(default: 0) From 29a2581389e3c195ba77f1161e172e776f46af5a Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 31 Mar 2026 15:15:10 +0200 Subject: [PATCH 5/9] spec/interaction-counter: count SUB interactions --- spec/add.typ | 1 + spec/chip.typ | 15 +++++++++++++-- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/spec/add.typ b/spec/add.typ index a678893e5..a41fd37b8 100644 --- a/spec/add.typ +++ b/spec/add.typ @@ -8,6 +8,7 @@ #show: book-page(chip.name) #set_nr_interactions(chip) +#set_nr_interactions(chip, name: "SUB") #let nr_interactions = get_nr_interactions(chip) #let add = raw(chip.name) diff --git a/spec/chip.typ b/spec/chip.typ index 0339b7912..eb65c5128 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -44,7 +44,16 @@ .product(default: 1) } -#let set_nr_interactions(chip) = { +// Compute the number of interactions performed by `chip` and +// store it as metadata under the `` label +// with tag `chip.name`. This tag is overwritten by `name` when specified. +#let set_nr_interactions(chip, name: none) = { + let chip-name = if name != none { + name + } else { + chip.name + } + let constraints = chip .constraints .values() @@ -73,7 +82,9 @@ let total-nr-interactions = nr-direct-interactions + nr-indirect-interactions - [#metadata((chip.name: total-nr-interactions)) ] + let entry = (:) + entry.insert(chip-name, total-nr-interactions) + [#metadata(entry) ] } } From a823099c4eedf3f2a2df82b825573bd09aa5bdb1 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 31 Mar 2026 15:18:37 +0200 Subject: [PATCH 6/9] spec/interaction-counter: drop silent lookup fails --- spec/chip.typ | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index eb65c5128..2634c3fa1 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -74,7 +74,11 @@ let nr-indirect-interactions = template-constraints .map(c => { let iter-size = get_interaction_count(c) - let template-interactions = lookup-table.at(c.tag, default: 0) + assert( + c.tag in lookup-table, + message: "cannot find interaction_count for " + repr(c) + ) + let template-interactions = lookup-table.at(c.tag) iter-size * template-interactions }) @@ -90,7 +94,9 @@ #let get_nr_interactions(chip) = { context { - query().map(c=>c.value).sum().at(chip.name) + let lut = query().map(c=>c.value).sum(default: (:)) + assert(chip.name in lut, message: "no interaction_count specified for " + repr(chip.name)) + lut.at(chip.name) } } From fcbd219d681b7f9122f674d1dbec3f4562168c0b Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 31 Mar 2026 15:23:44 +0200 Subject: [PATCH 7/9] spec/interaction-counter: remove superfluous code --- spec/is_bit.typ | 1 - 1 file changed, 1 deletion(-) diff --git a/spec/is_bit.typ b/spec/is_bit.typ index bb2690afc..1ed5e6284 100644 --- a/spec/is_bit.typ +++ b/spec/is_bit.typ @@ -8,7 +8,6 @@ #show: book-page(chip.name) #set_nr_interactions(chip) -#let nr_interactions = get_nr_interactions(chip) #let is_bit = raw(chip.name) From 6dae904025dd579f44dee8945258e462f7a899eb Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 1 Apr 2026 16:03:59 +0200 Subject: [PATCH 8/9] spec/interaction_count: merge getter and setter --- spec/add.typ | 5 ++--- spec/branch.typ | 6 ++---- spec/chip.typ | 3 ++- spec/cpu.typ | 6 ++---- spec/dvrm.typ | 6 ++---- spec/ecall.typ | 9 +++------ spec/is_bit.typ | 2 +- spec/load.typ | 6 ++---- spec/lt.typ | 6 ++---- spec/memw.typ | 12 ++++-------- spec/mul.typ | 6 ++---- spec/neg.typ | 5 ++--- spec/shift.typ | 6 ++---- spec/sign.typ | 6 +++--- 14 files changed, 31 insertions(+), 53 deletions(-) diff --git a/spec/add.typ b/spec/add.typ index a41fd37b8..7fb5cd43a 100644 --- a/spec/add.typ +++ b/spec/add.typ @@ -1,15 +1,14 @@ #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, get_nr_interactions, +#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) #set_nr_interactions(chip, name: "SUB") -#let nr_interactions = get_nr_interactions(chip) +#let nr_interactions = compute_nr_interactions(chip) #let add = raw(chip.name) #let sub = raw("SUB") diff --git a/spec/branch.typ b/spec/branch.typ index 6a4d4feb1..ee406f2e0 100644 --- a/spec/branch.typ +++ b/spec/branch.typ @@ -3,8 +3,7 @@ #import "/chip.typ": ( render_chip_assumptions, render_chip_column_table, - set_nr_interactions, - get_nr_interactions, + compute_nr_interactions, total_nr_variables, total_nr_instantiated_columns, render_constraint_table, @@ -22,8 +21,7 @@ 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) -#set_nr_interactions(chip) -#let nr_interactions = get_nr_interactions(chip) +#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) diff --git a/spec/chip.typ b/spec/chip.typ index 2634c3fa1..78247d35a 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -92,7 +92,8 @@ } } -#let get_nr_interactions(chip) = { +#let compute_nr_interactions(chip) = { + set_nr_interactions(chip) context { let lut = query().map(c=>c.value).sum(default: (:)) assert(chip.name in lut, message: "no interaction_count specified for " + repr(chip.name)) diff --git a/spec/cpu.typ b/spec/cpu.typ index 715b9d64d..c5d693782 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -5,8 +5,7 @@ render_chip_column_table, total_nr_variables, total_nr_instantiated_columns, - set_nr_interactions, - get_nr_interactions, + compute_nr_interactions, render_constraint_table, render_chip_padding_table, ) @@ -23,8 +22,7 @@ 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) -#set_nr_interactions(chip) -#let nr_interactions = get_nr_interactions(chip) +#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) diff --git a/spec/dvrm.typ b/spec/dvrm.typ index 9a420d056..9afc3ed7f 100644 --- a/spec/dvrm.typ +++ b/spec/dvrm.typ @@ -4,8 +4,7 @@ render_chip_column_table, total_nr_variables, total_nr_instantiated_columns, - set_nr_interactions, - get_nr_interactions, + compute_nr_interactions, render_constraint_table, render_chip_padding_table, render_chip_assumptions @@ -23,8 +22,7 @@ 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) -#set_nr_interactions(chip) -#let nr_interactions = get_nr_interactions(chip) +#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) diff --git a/spec/ecall.typ b/spec/ecall.typ index 754172bac..2a7759876 100644 --- a/spec/ecall.typ +++ b/spec/ecall.typ @@ -4,8 +4,7 @@ render_chip_column_table, total_nr_variables, total_nr_instantiated_columns, - set_nr_interactions, - get_nr_interactions, + compute_nr_interactions, render_constraint_table, render_chip_assumptions, render_chip_padding_table, @@ -34,8 +33,7 @@ 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) -#set_nr_interactions(chip) -#let nr_halt_interactions = get_nr_interactions(chip) +#let nr_halt_interactions = compute_nr_interactions(chip) The #halt chip leverages #nr_variables variable, spanning #nr_columns columns and leverages #nr_halt_interactions interaction(s): #render_chip_column_table(chip, config) @@ -80,8 +78,7 @@ As such, no padding is defined. == Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) -#set_nr_interactions(chip) -#let nr_commit_interactions = get_nr_interactions(chip) +#let nr_commit_interactions = compute_nr_interactions(chip) The #commit chip leverages #nr_variables variables, spanning #nr_columns columns and leverages #nr_commit_interactions interactions: #render_chip_column_table(chip, config) diff --git a/spec/is_bit.typ b/spec/is_bit.typ index 1ed5e6284..53a466501 100644 --- a/spec/is_bit.typ +++ b/spec/is_bit.typ @@ -1,6 +1,6 @@ #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, get_nr_interactions, +#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) diff --git a/spec/load.typ b/spec/load.typ index 8d1f61fdc..e7d6d3da5 100644 --- a/spec/load.typ +++ b/spec/load.typ @@ -5,8 +5,7 @@ render_chip_column_table, render_chip_padding_table, render_constraint_table, - set_nr_interactions, - get_nr_interactions, + compute_nr_interactions, total_nr_instantiated_columns, total_nr_variables, ) @@ -23,8 +22,7 @@ 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) -#set_nr_interactions(chip) -#let nr_interactions = get_nr_interactions(chip) +#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) diff --git a/spec/lt.typ b/spec/lt.typ index 763227e53..c9e700310 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -7,8 +7,7 @@ render_constraint_table, total_nr_instantiated_columns, total_nr_variables, - set_nr_interactions, - get_nr_interactions, + compute_nr_interactions, ) #let config = load_config() @@ -22,8 +21,7 @@ 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) -#set_nr_interactions(chip) -#let nr_interactions = get_nr_interactions(chip) +#let nr_interactions = compute_nr_interactions(chip) 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) diff --git a/spec/memw.typ b/spec/memw.typ index 2a77287b6..fb5c93e90 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -5,8 +5,7 @@ render_chip_column_table, total_nr_variables, total_nr_instantiated_columns, - set_nr_interactions, - get_nr_interactions, + compute_nr_interactions, render_constraint_table, render_chip_padding_table ) @@ -26,8 +25,7 @@ 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) -#set_nr_interactions(chip) -#let nr_memw_interactions = get_nr_interactions(chip) +#let nr_memw_interactions = compute_nr_interactions(chip) 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) @@ -77,8 +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) -#set_nr_interactions(alignedchip) -#let nr_aligned_interactions = get_nr_interactions(alignedchip) +#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), @@ -125,8 +122,7 @@ 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) -#set_nr_interactions(register_chip) -#let nr_memw_r_interactions = get_nr_interactions(register_chip) +#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 and leverages #nr_memw_r_interactions interactions: #render_chip_column_table(register_chip, config) diff --git a/spec/mul.typ b/spec/mul.typ index 77d1cca43..479c2f32d 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -4,8 +4,7 @@ render_chip_column_table, total_nr_variables, total_nr_instantiated_columns, - set_nr_interactions, - get_nr_interactions, + compute_nr_interactions, render_constraint_table, render_chip_assumptions, render_chip_padding_table, @@ -24,8 +23,7 @@ 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) -#set_nr_interactions(chip) -#let nr_interactions = get_nr_interactions(chip) +#let nr_interactions = compute_nr_interactions(chip) 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) diff --git a/spec/neg.typ b/spec/neg.typ index bcab35cbf..b2f75117a 100644 --- a/spec/neg.typ +++ b/spec/neg.typ @@ -1,13 +1,12 @@ #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, get_nr_interactions, +#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) -#set_nr_interactions(chip) -#let nr_interactions = get_nr_interactions(chip) +#let nr_interactions = compute_nr_interactions(chip) #let neg = raw(chip.name) diff --git a/spec/shift.typ b/spec/shift.typ index 3b3478705..f356122a3 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -4,8 +4,7 @@ render_chip_column_table, total_nr_variables, total_nr_instantiated_columns, - set_nr_interactions, - get_nr_interactions, + compute_nr_interactions, render_constraint_table, render_chip_assumptions, render_chip_padding_table, @@ -38,8 +37,7 @@ 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) -#set_nr_interactions(chip) -#let nr_interactions = get_nr_interactions(chip) +#let nr_interactions = compute_nr_interactions(chip) 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) diff --git a/spec/sign.typ b/spec/sign.typ index 06e766d5f..9e727e0ac 100644 --- a/spec/sign.typ +++ b/spec/sign.typ @@ -1,13 +1,13 @@ #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, set_nr_interactions, get_nr_interactions, +#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) -#set_nr_interactions(chip) -#let nr_interactions = get_nr_interactions(chip) +#let nr_variables = total_nr_variables(chip) +#let nr_interactions = compute_nr_interactions(chip) #let sign = raw(chip.name) From 27d9de10d003d4bd41e0d20da444363cd19f9d1d Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 1 Apr 2026 16:16:15 +0200 Subject: [PATCH 9/9] spec/interaction_counter: clean up --- spec/chip.typ | 33 +++++++++++++-------------------- 1 file changed, 13 insertions(+), 20 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index 78247d35a..8304717ff 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -25,7 +25,7 @@ } // Given a constraint, compute the number of interactions it induces -#let get_interaction_count(constraint) = { +#let get_constraint_interaction_count(constraint) = { let iters = if "iters" in constraint { constraint.iters } else if "iter" in constraint { @@ -37,7 +37,7 @@ iters.map(i => { assert( i.len() == 3 and type(i.at(1)) == int and type(i.at(2)) == int, - message: "contains invalid iter: " + repr(i), + message: "invalid iter: " + repr(i), ) i.at(2) - i.at(1) + 1 }) @@ -48,10 +48,8 @@ // store it as metadata under the `` label // with tag `chip.name`. This tag is overwritten by `name` when specified. #let set_nr_interactions(chip, name: none) = { - let chip-name = if name != none { - name - } else { - chip.name + if name == none { + name = chip.name } let constraints = chip @@ -61,41 +59,36 @@ // nr. of direct interactions let nr-direct-interactions = constraints - .filter(c=>c.kind == "interaction") - .map(get_interaction_count) + .filter(c => c.kind == "interaction") + .map(get_constraint_interaction_count) .sum(default: 0) - let template-constraints = constraints.filter(c=>c.kind == "template") + let template-constraints = constraints.filter(c => c.kind == "template") context { - let lookup-table = query().map(x => x.value).sum(default:(:)) + let lookup-table = query().map(x => x.value).sum(default: (:)) // nr. of indirect interactions through templates let nr-indirect-interactions = template-constraints .map(c => { - let iter-size = get_interaction_count(c) - assert( - c.tag in lookup-table, - message: "cannot find interaction_count for " + repr(c) - ) - let template-interactions = lookup-table.at(c.tag) + 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 - let entry = (:) - entry.insert(chip-name, total-nr-interactions) - [#metadata(entry) ] + [#metadata((str(name): total-nr-interactions)) ] } } #let compute_nr_interactions(chip) = { set_nr_interactions(chip) context { - let lut = query().map(c=>c.value).sum(default: (:)) + let lut = query().map(c => c.value).sum(default: (:)) assert(chip.name in lut, message: "no interaction_count specified for " + repr(chip.name)) lut.at(chip.name) }