From 91e5b179e8d2e909d970cb550c344304a0e50cd4 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Wed, 14 Jan 2026 15:22:43 +0100 Subject: [PATCH 1/2] spec: LOAD chip --- spec/book.typ | 1 + spec/load.typ | 42 +++++++++++++ spec/src/cpu.toml | 1 - spec/src/load.toml | 144 +++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 187 insertions(+), 1 deletion(-) create mode 100644 spec/load.typ create mode 100644 spec/src/load.toml diff --git a/spec/book.typ b/spec/book.typ index 1bf944862..277e652b5 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("load.typ")[LOAD chip] #chapter("bitwise.typ")[BITWISE] ] ) diff --git a/spec/load.typ b/spec/load.typ new file mode 100644 index 000000000..931611108 --- /dev/null +++ b/spec/load.typ @@ -0,0 +1,42 @@ +#import "/book.typ": book-page, rj +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_assumptions, + render_chip_column_table, + render_chip_padding_table, + render_constraint_table, + total_nr_instantiated_columns, + total_nr_variables, +) + +#let config = load_config() +#let chip = load_chip("src/load.toml", config) + +#show: book-page.with(title: "LOAD chip") + +== Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) + +The `LOAD` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: +#render_chip_column_table(chip, config) + +== Assumptions +#render_chip_assumptions(chip, config) + +== Constraints +The chip delegates the actual memory interaction to the `MEMW` chip, +and ensures correctness of the requested sign/zero extension. +The output `res` is correctly range-checked as long as the memory contents are. + +#render_constraint_table(chip, config, groups: "all") + +The chip contributes the following to the lookup argument. + +#render_constraint_table(chip, config, groups: "output") + +== Padding + +The table can be padded to the next power of two with the following value assignments: + +#render_chip_padding_table(chip, config) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 747497d44..1bd46ac00 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -582,7 +582,6 @@ kind = "interaction" tag = "MEMW" input = [1, ["*", 2, "rd"], "rvd", ["+", "timestamp", 2], 1, 0, 0] -# TODO: no types available, so no casting yet [[constraints.mem]] kind = "interaction" tag = "LOAD" diff --git a/spec/src/load.toml b/spec/src/load.toml new file mode 100644 index 000000000..93d7234c4 --- /dev/null +++ b/spec/src/load.toml @@ -0,0 +1,144 @@ +name = "LOAD" + +# Input + +[[variables.input]] +name = "base_address" +type = "DWordWL" +desc = "The base address to read/write from/to, gets offset by $[0, 7]$, depending on how big the access is" +pad = 0 + +[[variables.input]] +name = "timestamp" +type = "DWordWL" +desc = "The timestamp at which this memory access is said to occur" +pad = 0 + +[[variables.input]] +name = "read2" +type = "Bit" +desc = "Whether to read exactly 2 values" +pad = 0 + +[[variables.input]] +name = "read4" +type = "Bit" +desc = "Whether to read exactly 4 values" +pad = 0 + +[[variables.input]] +name = "read8" +type = "Bit" +desc = "Whether to read exactly 8 values" +pad = 0 + +[[variables.input]] +name = "signed" +type = "Bit" +desc = "Whether to sign-extend (1) or zero-extend (0)" +pad = 0 + +# Output + +[[variables.output]] +name = "res" +type = "DWordBL" +desc = "The result of reading (up to) 8 bytes from `base_address`, extended corresponding to `signed`." +pad = 0 + +# Auxiliary + +[[variables.auxiliary]] +name = "sign_bit" +type = "Bit" +desc = "The sign bit extracted from the bytes retrieved from memory" +pad = 0 + +# Virtual + +# Multiplicity + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" +pad = 0 + + +[[assumptions]] +desc = "`IS_WORD[base_address[i]]`" +iter = ["i", 0, 1] + +[[assumptions]] +desc = "`IS_BIT`" + +[[assumptions]] +desc = "`IS_BIT`" + +[[assumptions]] +desc = "`IS_BIT`" + +[[assumptions]] +desc = "`IS_BIT`" + +[[assumptions]] +desc = "`IS_WORD[timestamp[i]]`" +iter = ["i", 0, 1] + + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "arith" +constraint = "$#`read2` + #`read4` + #`read8` => #`μ`$" +poly = ["*", ["+", "read2", "read4", "read8"], ["not", "μ"]] + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [0, "base_address", ["cast", "res", ["BaseField", 8]], "timestamp", "read2", "read4", "read8"] +output = "res" +multiplicity = "μ" + +[[constraints.all]] +kind = "interaction" +tag = "MSB8" +input = [["idx", "res", 1]] +output = "sign_bit" +multiplicity = "read2" + +[[constraints.all]] +kind = "interaction" +tag = "MSB8" +input = [["idx", "res", 3]] +output = "sign_bit" +multiplicity = "read4" + +[[constraints.all]] +kind = "arith" +constraint = "$!#`read8` => #`res`_i = #`signed` dot #`sign_bit` dot 255$" +poly = ["*", ["not", "read8"], ["-", ["idx", "res", "i"], ["*", "signed", "sign_bit", 255]]] +iter = ["i", 4, 7] + +[[constraints.all]] +kind = "arith" +constraint = "$!(#`read4` + #`read8`) => #`res`_i = #`signed` dot #`sign_bit` dot 255$" +poly = ["*", ["-", 1, "read4", "read8"], ["-", ["idx", "res", "i"], ["*", "signed", "sign_bit", 255]]] +iter = ["i", 2, 3] + +[[constraints.all]] +kind = "arith" +constraint = "$!(#`read2` + #`read4` + #`read8`) => #`res`_i = #`signed` dot #`sign_bit` dot 255$" +poly = ["*", ["-", 1, "read2", "read4", "read8"], ["-", ["idx", "res", 1], ["*", "signed", "sign_bit", 255]]] + + +[[constraint_groups]] +name = "output" + +[[constraints.output]] +kind = "interaction" +tag = "LOAD" +input = ["base_address", "timestamp", "read2", "read4", "read8"] +output = ["cast", "res", "DWordWL"] +multiplicity = ["-", "μ"] From 90baa1246d2fbd9ebb5c87a3434ca3174c04642d Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Thu, 15 Jan 2026 14:26:13 +0100 Subject: [PATCH 2/2] Address review comments --- spec/src/load.toml | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/spec/src/load.toml b/spec/src/load.toml index 93d7234c4..fcbd2b87f 100644 --- a/spec/src/load.toml +++ b/spec/src/load.toml @@ -17,19 +17,19 @@ pad = 0 [[variables.input]] name = "read2" type = "Bit" -desc = "Whether to read exactly 2 values" +desc = "Whether to read exactly 2 bytes" pad = 0 [[variables.input]] name = "read4" type = "Bit" -desc = "Whether to read exactly 4 values" +desc = "Whether to read exactly 4 bytes" pad = 0 [[variables.input]] name = "read8" type = "Bit" -desc = "Whether to read exactly 8 values" +desc = "Whether to read exactly 8 bytes" pad = 0 [[variables.input]] @@ -56,6 +56,12 @@ pad = 0 # Virtual +[[variables.virtual]] +name = "read1" +type = "Bit" +desc = "Whether to read exactly 1 byte" +def = ["-", "μ", "read2", "read4", "read8"] + # Multiplicity [[variables.multiplicity]] @@ -69,6 +75,9 @@ pad = 0 desc = "`IS_WORD[base_address[i]]`" iter = ["i", 0, 1] +[[assumptions]] +desc = "`IS_BIT`" + [[assumptions]] desc = "`IS_BIT`" @@ -101,6 +110,13 @@ input = [0, "base_address", ["cast", "res", ["BaseField", 8]], "timestamp", "rea output = "res" multiplicity = "μ" +[[constraints.all]] +kind = "interaction" +tag = "MSB8" +input = [["idx", "res", 0]] +output = "sign_bit" +multiplicity = "read1" + [[constraints.all]] kind = "interaction" tag = "MSB8" @@ -129,7 +145,7 @@ iter = ["i", 2, 3] [[constraints.all]] kind = "arith" -constraint = "$!(#`read2` + #`read4` + #`read8`) => #`res`_i = #`signed` dot #`sign_bit` dot 255$" +constraint = "$!(#`read2` + #`read4` + #`read8`) => #`res`_1 = #`signed` dot #`sign_bit` dot 255$" poly = ["*", ["-", 1, "read2", "read4", "read8"], ["-", ["idx", "res", 1], ["*", "signed", "sign_bit", 255]]]