diff --git a/spec/add.typ b/spec/add.typ index d2afb1788..7fb5cd43a 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, 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 diff --git a/spec/branch.typ b/spec/branch.typ index 90503e862..ee406f2e0 100644 --- a/spec/branch.typ +++ b/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 diff --git a/spec/chip.typ b/spec/chip.typ index f3ac28a74..8304717ff 100644 --- a/spec/chip.typ +++ b/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 `` 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().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)) ] + } +} + +#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)) + 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) = { diff --git a/spec/cpu.typ b/spec/cpu.typ index 08fe1533d..c5d693782 100644 --- a/spec/cpu.typ +++ b/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 diff --git a/spec/dvrm.typ b/spec/dvrm.typ index 920aec075..9afc3ed7f 100644 --- a/spec/dvrm.typ +++ b/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 diff --git a/spec/ecall.typ b/spec/ecall.typ index 3b82019db..2a7759876 100644 --- a/spec/ecall.typ +++ b/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 diff --git a/spec/is_bit.typ b/spec/is_bit.typ index b09242fe4..53a466501 100644 --- a/spec/is_bit.typ +++ b/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. diff --git a/spec/load.typ b/spec/load.typ index b12e1c04d..e7d6d3da5 100644 --- a/spec/load.typ +++ b/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 diff --git a/spec/lt.typ b/spec/lt.typ index 8e55b390b..c9e700310 100644 --- a/spec/lt.typ +++ b/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 diff --git a/spec/memw.typ b/spec/memw.typ index 1c7a1e6e5..fb5c93e90 100644 --- a/spec/memw.typ +++ b/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 diff --git a/spec/mul.typ b/spec/mul.typ index 68ab4a2b8..479c2f32d 100644 --- a/spec/mul.typ +++ b/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) = { diff --git a/spec/neg.typ b/spec/neg.typ index d700892cb..b2f75117a 100644 --- a/spec/neg.typ +++ b/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 diff --git a/spec/shift.typ b/spec/shift.typ index 289ade1d7..f356122a3 100644 --- a/spec/shift.typ +++ b/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 diff --git a/spec/sign.typ b/spec/sign.typ index 7135ba9c6..9e727e0ac 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, 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