From 40cc0bc341348eff75e846fa915df92b4153e624 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 26 May 2026 13:14:11 +0200 Subject: [PATCH 01/25] spec: Draft CPU rework, still missing updates for all ALU chips, DECODE and CPU32 --- spec/cpu.typ | 72 +++-- spec/decode.typ | 3 +- spec/src/cpu.toml | 627 +++++++++------------------------------ spec/src/load.toml | 1 + spec/src/signatures.toml | 64 ++-- 5 files changed, 217 insertions(+), 550 deletions(-) diff --git a/spec/cpu.typ b/spec/cpu.typ index 2ee85befa..f597e907b 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -31,35 +31,49 @@ The #cpu chip is comprised of #nr_variables variables that are expressed using # #render_chip_assumptions(chip, config) = Constraints + First, we perform a decoding lookup for the current PC. +Instructions having the `word_instr` flag set are not decoded here, as they are delegated to the `CPU32` chip. +In that case, we ensure that the current row of the CPU cannot have any other observable effects. #render_constraint_table(chip, config, groups: "decode") == Range checks We constrain all columns to have the appropriate ranges. -The flags and register indices looked up from the decoding need to be checked, -as they are communicated through the interaction in a packed form. +All values in `packed_decode` need to be checked to ensure +the packing is correct for the interaction. In contrast, we know ahead of time that decoding will ensure proper range checks for `pc` and `imm`. Similarly, since `next_pc` will propagate through the memory argument and be looked up -in the instruction decoding on the next cycle, it is forced to be in the correct range.#rj[is this true, do we need this elsewhere for chip assumptions?] -For the auxiliary columns, we need to check the limbs of `arg1`, `arg2`, and `res`. +in the instruction decoding on the next cycle, it is forced to be in the correct range. +The final value for `next_pc` is similarly fixed by the memory finalization. +For the auxiliary columns, we need to check the limbs of `res`, since +`rv1` and `rv2` are enforced by the memory argument, and `rvd` is correct by the correctness of the dependent chips. The ranges of the other auxiliary columns are enforced through later constraints. -#rj[Make sure we argue for every column here] -#rj[is `rvd` still sufficiently constrained? (can also be done through the memory argument like `pc`?)] #render_constraint_table(chip, config, groups: "range") == ALU -The ALU functionality is then obtained through judicious dispatching to the corresponding chips. +The ALU functionality is then obtained through delegation to the `ALU` signature, backed by the various ALU chips, +or by using the appropriate template. +For the pure ALU path, `arg2` is computed as `rv2 + imm`, which relies on @cpu:a:arg2-multiplex to +be either `rv2` or `imm`, depending on the instruction. +The other contributions for `arg2` are specific to the (mutually exclusive, @cpu:a:mem-branch-mutex) +`MEMORY` and `BRANCH` flags: +- For the `MEMORY` path, we want the output of the ALU to be $#`rv1` + #`imm`$, as that is the + address at which the memory access occurs. +- For the `BRANCH` path, when we do not have a JALR instruction, we want the ALU output to reflect the branch condition. +- For the `BRANCH` path, when it is a JALR instruction, we want the ALU output to contain the next instructions PC value, to store into `rd`. + +Instructions having the `word_instr` flag set are delegated to the `CPU32` chip, which will do its own decoding and execution of the instruction. #render_constraint_table(chip, config, groups: "alu") == Memory -The interactions with the memory, both for register loading and storing, as for `LOAD` and `STORE` instructions are handled. -Note that since registers need no byte-addressing, we store them in the memory argument with `Word` limbs. +Note that since registers need no byte-addressing, we store them in the memory argument with `Word` limbs, +simultaneously ensuring that register reads are properly range checked as long as all writes are. The `pc` register behaves very predictably with respect to its timestamps and when it is being read, so for performance reasons, we inline its memory interactions directly into the #cpu chip. @@ -70,32 +84,36 @@ Constraints regarding whether `pc_double_read` corresponds to an `AUIPC` instruc as regardless of its value, the old timestamp is guaranteed smaller than the new timestamp, and the integrity of the memory argument therefore ensures the correctness of this bit. -#render_constraint_table(chip, config, groups: "mem") - -=== Potential optimizations - -- `double_pc_read` could be integrated into decoding, so that `AUIPC` could set `read_register1 = 0` and no extra MEMW access for `rv1` is needed at this point. +The memory interaction itself is handled by the `MEMORY` signature, +which will read the `mem_flags` argument to perform either a `LOAD` or a `STORE`. +We refer to the previous section's description of `arg2` for how +the address is computed. -== System +The value to (potentially) be written back to `rd` is stored in `rvd`, +which can either come from either the ALU, in case of an ALU operation or a JALR branch, +or from the MEMORY interaction. -The interactions with the wider system. +#render_constraint_table(chip, config, groups: "mem") -#render_constraint_table(chip, config, groups: "sys") +== Branching -== Input and output to the ALU +A branch is expressed by having the `BRANCH` flag set to 1. +Since `BRANCH` and `MEMORY` are mutually exclusive (@cpu:a:mem-branch-mutex), +we can repurpose the `mem_flags` field to indicate a JALR instruction. +When JALR is not set, we have a conditional branch that is decided upon by the result of the ALU instructions, +as set in the `res` variable. +As such, we can set `branch_cond` appropriately as multiplicity flag for the `BRANCH` chip. -We constrain `arg1`, `arg2` and `rvd` to correspond to the wanted values, -including the appropriate sign/zero extension, depending on `word_instr`. +#render_constraint_table(chip, config, groups: "branch") -#render_constraint_table(chip, config, groups: "ext") +== System -== Other constraints -For @cpu:c:is_equal, note that @cpu:c:sub sets `res` to be the difference between `arg1` and `arg2` whenever `BEQ` is $1$. -Given that this difference is $0$ when both are equal, @cpu:c:is_equal ensures `is_equal` is set to $1$ if and only if $#`arg1` = #`arg2`$ and `BEQ` is set. +The interactions with the wider system go through the `ECALL` interface. +Since we treat `EBREAK` instructions as unprovable traps, we avoid emitting `DECODE` rows +for these, and do not need any further handling in the CPU. -#render_constraint_table(chip, config, groups: "misc") +#render_constraint_table(chip, config, groups: "sys") -#rj[Document the choice to not have a multiplicity column here for padding] = Padding @@ -104,4 +122,4 @@ in the DECODE table, at the _odd_ address 1, only reachable through a HALT ecall #render_chip_padding_table(chip, config) -This approach minimizes the number of dependent lookups, increasing only multiplicities in the DECODE table and the IS_BYTE lookup. +This approach minimizes the number of dependent lookups, increasing only multiplicities in the `DECODE` table and the `IS_BYTE` and `IS_HALF` lookups. diff --git a/spec/decode.typ b/spec/decode.typ index 21cd26acb..c839287f8 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -34,8 +34,9 @@ Empty rows with the following content can be added to achieve this: #render_chip_padding_table(chip, config) +#rj[note to self: remove EBREAK rows] Note that this row sets the `EBREAK` flag. -Given that `CPU` asserts that `EBREAK = 0` (see @cpu:c:ebreak_traps), using this "padding-instruction" would immediately make the CPU table unprovable. +Given that `CPU` asserts that `EBREAK = 0`, using this "padding-instruction" would immediately make the CPU table unprovable. Note moreover that the `pc` is set to $7$. This value is the _smallest odd number_ (i.e., not reachable during regular execution) that is more than _$4$_ (i.e., the max `pc`-increment) greater than _$1$_ (i.e., the `pc`-value used in the #link()[additional instruction] referred to by `CPU`-padding lines). diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index a0bd3925c..358651585 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -7,7 +7,7 @@ name = "CPU" [[variables.input]] name = "timestamp" type = "Timestamp" -desc = "A preprocessed timestamp to coordinate the memory argument. Since we have at most 3 non-disjoint memory accesses (`(rs1, rs2, rd)`, `(rs1, pc, pc)`, `(LOAD)` or `(STORE)`) a maximum of 4 slots is enough." +desc = "A preprocessed timestamp to coordinate the memory argument. Since we have at most 3 non-disjoint memory accesses (`(rs1, rs2, rd)`, `(rs1, pc, pc)`, `MEMORY`) a maximum of 4 slots is enough." [[variables.input]] name = "pc" @@ -51,58 +51,18 @@ type = "Bit" desc = "Whether to write back to the destination register" pad = 0 -# TODO: can we compress this to a single value? (1: is it worth it, 2: does it work) -[[variables.input]] -name = "memory_2bytes" -type = "Bit" -desc = "Whether the memory access (read or write) touches exactly 2 bytes" -pad = 0 - -[[variables.input]] -name = "memory_4bytes" -type = "Bit" -desc = "Whether the memory access (read or write) touches exactly 4 bytes" -pad = 0 - -[[variables.input]] -name = "memory_8bytes" -type = "Bit" -desc = "Whether the memory access (read or write) touches exactly 8 bytes" -pad = 0 - -# TODO: Are there usecases where it's nicer to just have this as a length constant? -[[variables.input]] -name = "c_type_instruction" -type = "Bit" -desc = "Whether the instruction is of C type, i.e., whether it is 2 bytes long instead of 4" -pad = 0 - [[variables.input]] name = "imm" type = "DWordWL" desc = "The fully extended 64-bit version of the immediate" pad = 0 +# We encode C-type instructions with a length of 2, as this generality allows fusing common instruction combos [[variables.input]] -name = "signed" -type = "Bit" -desc = "Indicates whether we're dealing with a signed or unsigned instruction" -pad = 0 - -[[variables.input]] -name = "mp_selector" -type = "Bit" -desc = """Multi-purpose selector used by different ALU operations for different purposes. Currently, it is used - - by the `MUL` chip to select between `MUL`/`MULH` and `MULH[S]U`, and - - as flag for inverting the condition of conditional branches (see `branch_cond`) - - as direction (left or right) for `SHIFT`""" -pad = 0 - -[[variables.input]] -name = "muldiv_selector" -type = "Bit" -desc = "Selects which output of `MUL` (lo/hi) or `DIV` (quo/rem) is wanted" -pad = 0 +name = "instruction_length" +type = "Byte" +desc = "The number of bytes consumed by this instruction, commonly used to indicate whether the instruction is of C type, i.e., whether it is 2 bytes long instead of 4" +pad = 4 [[variables.input]] name = "word_instr" @@ -111,102 +71,53 @@ desc = "Whether the instruction is a \\*W instruction, requiring the inputs and pad = 0 [[variables.input]] -name = "ADD" +name = "ALU" type = "Bit" -desc = "One-hot ALU selector flag" +desc = "Whether to use the ALU for this instruction" pad = 0 [[variables.input]] -name = "SUB" -type = "Bit" -desc = "One-hot ALU selector flag" -pad = 0 - -[[variables.input]] -name = "SLT" -type = "Bit" -desc = "One-hot ALU selector flag" -pad = 0 - -[[variables.input]] -name = "AND" -type = "Bit" -desc = "One-hot ALU selector flag" -pad = 0 - -[[variables.input]] -name = "OR" -type = "Bit" -desc = "One-hot ALU selector flag" -pad = 0 - -[[variables.input]] -name = "XOR" -type = "Bit" -desc = "One-hot ALU selector flag" -pad = 0 - -[[variables.input]] -name = "SHIFT" -type = "Bit" -desc = "One-hot ALU selector flag" -pad = 0 - -[[variables.input]] -name = "JALR" -type = "Bit" -desc = "One-hot ALU selector flag" -pad = 0 - -[[variables.input]] -name = "BEQ" -type = "Bit" -desc = "One-hot ALU selector flag" +name = "alu_flags" +type = "Byte" +desc = "The ALU operation + flags (interpreting things as signed/unsigned, choosing the MUL/DVRM output, ...) to pass to the ALU" pad = 0 [[variables.input]] -name = "BLT" +name = "ADD" type = "Bit" -desc = "One-hot ALU selector flag" +desc = "Addition fast-path bypassing the ALU" pad = 0 [[variables.input]] -name = "LOAD" +name = "SUB" type = "Bit" -desc = "One-hot ALU selector flag" +desc = "Subtraction fast-path bypassing the ALU" pad = 0 [[variables.input]] -name = "STORE" +name = "MEMORY" type = "Bit" -desc = "One-hot ALU selector flag" +desc = "Whether this instruction touches memory (LOAD/STORE)" pad = 0 [[variables.input]] -name = "MUL" -type = "Bit" -desc = "One-hot ALU selector flag" +name = "mem_flags" +type = "Byte" +desc = "The flags to pass for MEMORY operations (LOAD vs STORE, number of bytes touched, signed)" pad = 0 [[variables.input]] -name = "DIVREM" +name = "BRANCH" type = "Bit" -desc = "One-hot ALU selector flag" +desc = "Whether this instruction is a conditional branch (BLT, BEQ)" pad = 0 [[variables.input]] name = "ECALL" type = "Bit" -desc = "One-hot ALU selector flag" -pad = 0 - -[[variables.input]] -name = "EBREAK" -type = "Bit" -desc = "One-hot ALU selector flag" +desc = "Whether this instruction is an ECALL" pad = 0 - # Output [[variables.output]] name = "next_pc" @@ -235,65 +146,41 @@ pad = 0 [[variables.auxiliary]] name = "rv1" -type = "DWordWHH" +type = "DWordWL" desc = "The value of register `rs1`" pad = 0 [[variables.auxiliary]] name = "rv2" -type = "DWordWHH" +type = "DWordWL" desc = "The value of register `rs2`" pad = 0 -[[variables.auxiliary]] -name = "rv1_ext_bit" -type = "Bit" -desc = "The sign bit of `rv1` if seen as a 32-bit word, used for sign extension with `word_instr`" -pad = 0 - -[[variables.auxiliary]] -name = "arg1" -type = "DWordBL" -desc = "The extended version of `rv1`, depending on `word_instr`" -pad = 0 - -[[variables.auxiliary]] -name = "rv2_ext_bit" -type = "Bit" -desc = "The sign bit of `rv2` if seen as a 32-bit word, used for sign extension with `word_instr`" -pad = 0 - [[variables.auxiliary]] name = "arg2" -type = "DWordBL" +type = "DWordWL" desc = "A multiplexed version of `rv2` and `imm`, to be used as second argument to ALU calls" pad = 0 -[[variables.auxiliary]] -name = "res_ext_bit" -type = "Bit" -desc = "The sign bit of `res`, if seen as a 32-bit word, used for sign extension with `word_instr`" -pad = 0 - [[variables.auxiliary]] name = "res" -type = "DWordBL" +type = "DWordHL" desc = "The ALU result" pad = 0 -[[variables.auxiliary]] -name = "is_equal" -type = "Bit" -desc = "Whether `rv1` and `arg2` are equal" -pad = 0 - [[variables.auxiliary]] name = "branch_cond" type = "Bit" -desc = "Whether a branch is taken, i.e., the branch condition" +desc = "Whether a branch is taken, the branch condition evaluates to true, or we are doing an unconditional jump" pad = 0 # Virtual +[[variables.virtual]] +name = "JALR" +type = "Bit" +desc = "Read whether our BRANCH corresponds to a JAL(R) instruction from `mem_flags`, as `MEMORY` and `BRANCH` are mutually exclusive" +def = "mem_flags" + [[variables.virtual]] name = "packed_decode" type = "BaseField" @@ -302,48 +189,28 @@ def = ["+", ["*", ["^", 2, 0], "read_register1"], ["*", ["^", 2, 1], "read_register2"], ["*", ["^", 2, 2], "write_register"], - ["*", ["^", 2, 3], "memory_2bytes"], - ["*", ["^", 2, 4], "memory_4bytes"], - ["*", ["^", 2, 5], "memory_8bytes"], - ["*", ["^", 2, 6], "c_type_instruction"], - ["*", ["^", 2, 7], "signed"], - ["*", ["^", 2, 8], "mp_selector"], - ["*", ["^", 2, 9], "muldiv_selector"], - ["*", ["^", 2, 10], "word_instr"], - ["*", ["^", 2, 11], "ADD"], - ["*", ["^", 2, 12], "SUB"], - ["*", ["^", 2, 13], "SLT"], - ["*", ["^", 2, 14], "AND"], - ["*", ["^", 2, 15], "OR"], - ["*", ["^", 2, 16], "XOR"], - ["*", ["^", 2, 17], "SHIFT"], - ["*", ["^", 2, 18], "JALR"], - ["*", ["^", 2, 19], "BEQ"], - ["*", ["^", 2, 20], "BLT"], - ["*", ["^", 2, 21], "LOAD"], - ["*", ["^", 2, 22], "STORE"], - ["*", ["^", 2, 23], "MUL"], - ["*", ["^", 2, 24], "DIVREM"], - ["*", ["^", 2, 25], "ECALL"], - ["*", ["^", 2, 26], "EBREAK"], - ["*", ["^", 2, 27], "rs1"], - ["*", ["^", 2, 35], "rs2"], - ["*", ["^", 2, 43], "rd"], + ["*", ["^", 2, 3], "word_instr"], + ["*", ["^", 2, 4], "ALU"], + ["*", ["^", 2, 5], "ADD"], + ["*", ["^", 2, 6], "SUB"], + ["*", ["^", 2, 7], "MEMORY"], + ["*", ["^", 2, 8], "BRANCH"], + ["*", ["^", 2, 9], "ECALL"], + ["*", ["^", 2, 10], "rs1"], + ["*", ["^", 2, 18], "rs2"], + ["*", ["^", 2, 26], "rd"], + ["*", ["^", 2, 34], "instruction_length"], + ["*", ["^", 2, 42], "alu_flags"], + ["*", ["^", 2, 50], "mem_flags"], ] -[[variables.virtual]] -name = "pad" -type = "Bit" -desc = "When no flags are set, we must be in a padding row." -def = ["-", 1, "ADD", "SUB", "SLT", "AND", "OR", "XOR", "SHIFT", "JALR", "BEQ", "BLT", "LOAD", "STORE", "MUL", "DIVREM", "ECALL", "EBREAK"] - [[assumptions]] -desc = "At most one ALU selector flag is 1 by the decoding, and every other flag is 0." -ref = "cpu:a:one-hot" +desc = "`MEMORY` and `BRANCH` are mutually exclusive" +ref = "cpu:a:mem-branch-mutex" [[assumptions]] -desc = "When `STORE + LOAD + BEQ + BLT = 0`, either `rs2 = 0` or `imm = 0` should be enforced by the decoding. This is needed for `arg2`." +desc = "When `MEMORY + BRANCH = 0`, either `rs2 = 0` or `imm = 0` should be enforced by the decoding. This is needed for `arg2`." ref = "cpu:a:arg2-multiplex" [[constraint_groups]] @@ -353,7 +220,22 @@ name = "decode" kind = "interaction" tag = "DECODE" input = ["pc", "imm", "packed_decode"] -multiplicity = 1 +multiplicity = ["not", "word_instr"] + +[[constraints.decode]] +kind = "arith" +constraint = "$#`word_instr` => #`MEMORY = 0`$" +poly = ["*", "word_instr", "MEMORY"] + +[[constraints.decode]] +kind = "arith" +constraint = "$#`word_instr` => #`BRANCH = 0`$" +poly = ["*", "word_instr", "BRANCH"] + +[[constraints.decode]] +kind = "arith" +constraint = "$#`word_instr` => #`ECALL = 0`$" +poly = ["*", "word_instr", "ECALL"] [[constraint_groups]] @@ -379,52 +261,30 @@ input = ["write_register"] ref = "cpu:c:range_write_register" [[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["memory_2bytes"] -ref = "cpu:c:range_memory_2bytes" - -[[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["memory_4bytes"] -ref = "cpu:c:range_memory_4bytes" - -[[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["memory_8bytes"] -ref = "cpu:c:range_memory_8bytes" - -[[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["c_type_instruction"] +kind = "interaction" +tag = "IS_BYTE" +input = ["instruction_length"] +multiplicity = 1 ref = "cpu:c:range_c_type_instruction" [[constraints.range]] kind = "template" tag = "IS_BIT" -input = ["signed"] -ref = "cpu:c:range_signed" - -[[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["mp_selector"] -ref = "cpu:c:range_mp_selector" +input = ["word_instr"] +ref = "cpu:c:range_word_instr" [[constraints.range]] kind = "template" tag = "IS_BIT" -input = ["muldiv_selector"] -ref = "cpu:c:range_muldiv_selector" +input = ["ALU"] +ref = "cpu:c:range_ALU" [[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["word_instr"] -ref = "cpu:c:range_word_instr" +kind = "interaction" +tag = "IS_BYTE" +input = ["alu_flags"] +multiplicity = 1 +ref = "cpu:c:range_alu_flags" [[constraints.range]] kind = "template" @@ -441,74 +301,21 @@ ref = "cpu:c:range_SUB" [[constraints.range]] kind = "template" tag = "IS_BIT" -input = ["SLT"] -ref = "cpu:c:range_SLT" +input = ["MEMORY"] +ref = "cpu:c:range_MEMORY" [[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["AND"] -ref = "cpu:c:range_AND" - -[[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["OR"] -ref = "cpu:c:range_OR" - -[[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["XOR"] -ref = "cpu:c:range_XOR" - -[[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["SHIFT"] -ref = "cpu:c:range_SHIFT" - -[[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["JALR"] -ref = "cpu:c:range_JALR" - -[[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["BEQ"] -ref = "cpu:c:range_BEQ" - -[[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["BLT"] -ref = "cpu:c:range_BLT" - -[[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["LOAD"] -ref = "cpu:c:range_LOAD" - -[[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["STORE"] -ref = "cpu:c:range_STORE" - -[[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["MUL"] -ref = "cpu:c:range_MUL" +kind = "interaction" +tag = "IS_BYTE" +input = ["mem_flags"] +multiplicity = 1 +ref = "cpu:c:range_mem_flags" [[constraints.range]] kind = "template" tag = "IS_BIT" -input = ["DIVREM"] -ref = "cpu:c:range_DIVREM" +input = ["BRANCH"] +ref = "cpu:c:range_BRANCH" [[constraints.range]] kind = "template" @@ -516,12 +323,6 @@ tag = "IS_BIT" input = ["ECALL"] ref = "cpu:c:range_ECALL" -[[constraints.range]] -kind = "template" -tag = "IS_BIT" -input = ["EBREAK"] -ref = "cpu:c:range_EBREAK" - [[constraints.range]] kind = "template" tag = "IS_BYTE" @@ -538,22 +339,11 @@ tag = "IS_BYTE" input = ["rd"] [[constraints.range]] -kind = "template" -tag = "IS_BYTE" -input = [["idx", "arg1", "i"]] -iter = ["i", 0, 7] - -[[constraints.range]] -kind = "template" -tag = "IS_BYTE" -input = [["idx", "arg2", "i"]] -iter = ["i", 0, 7] - -[[constraints.range]] -kind = "template" -tag = "IS_BYTE" +kind = "interaction" +tag = "IS_HALF" input = [["idx", "res", "i"]] -iter = ["i", 0, 7] +multiplicity = 1 +iter = ["i", 0, 3] [[constraint_groups]] @@ -561,91 +351,44 @@ name = "alu" prefix = "A" [[constraints.alu]] -kind = "template" -tag = "ADD" -cond = ["+", "ADD", "LOAD"] -input = [["cast", "arg1", "DWordWL"], ["cast", "arg2", "DWordWL"]] -output = ["cast", "res", "DWordWL"] +kind = "arith" +constraint = "$#`arg2` = #`MEMORY` * #`imm` + #`BRANCH` * (1 - #`JALR`) * #`instruction_length` * #`BRANCH` * #`JALR` * #`rv2` + (1 - #`MEMORY`) * (1 - #`BRANCH`) * (#`rv2` + #`imm`)$" +poly = ["-", ["idx", "arg2", "i"], + ["*", "MEMORY", ["idx", "imm", "i"]], + ["*", "BRANCH", ["not", "JALR"], "instruction_length"], + ["*", "BRANCH", "JALR", ["idx", "rv2", "i"]], + ["*", ["not", "MEMORY"], ["not", "BRANCH"], ["idx", ["+", "rv2", "imm"], "i"]] +] +iter = ["i", 0, 1] [[constraints.alu]] kind = "template" tag = "ADD" -cond = "STORE" -input = [["cast", "arg1", "DWordWL"], "imm"] +cond = "ADD" +input = ["rv1", "arg2"] output = ["cast", "res", "DWordWL"] [[constraints.alu]] kind = "template" tag = "SUB" -cond = ["+", "SUB", "BEQ"] -input = [["cast", "arg1", "DWordWL"], ["cast", "arg2", "DWordWL"]] +cond = "SUB" +input = ["rv1", "arg2"] output = ["cast", "res", "DWordWL"] ref = "cpu:c:sub" [[constraints.alu]] kind = "interaction" -tag = "LT" -input = [["cast", "arg1", "DWordWL"], ["cast", "arg2", "DWordWL"], "signed"] -output = ["idx", "res", 0] -multiplicity = ["+", "SLT", "BLT"] - -[[constraints.alu]] -kind = "arith" -constraint = "$#`SLT` + #`BLT` => #`res[i]` = 0$" -poly = ["*", ["+", "SLT", "BLT"], ["idx", "res", "i"]] -iter = ["i", 1, 7] - -[[constraints.alu]] -kind = "interaction" -tag = "AND_BYTE" -input = [["idx", "arg1", "i"], ["idx", "arg2", "i"]] -output = ["idx", "res", "i"] -multiplicity = "AND" -iter = ["i", 0, 7] - -[[constraints.alu]] -kind = "interaction" -tag = "OR_BYTE" -input = [["idx", "arg1", "i"], ["idx", "arg2", "i"]] -output = ["idx", "res", "i"] -multiplicity = "OR" -iter = ["i", 0, 7] - -[[constraints.alu]] -kind = "interaction" -tag = "XOR_BYTE" -input = [["idx", "arg1", "i"], ["idx", "arg2", "i"]] -output = ["idx", "res", "i"] -multiplicity = "XOR" -iter = ["i", 0, 7] - -[[constraints.alu]] -kind = "interaction" -tag = "SHIFT" -input = [["cast", "arg1", "DWordHL"], ["idx", "arg2", 0], "mp_selector", "signed", "word_instr"] -output = ["cast", "res", "DWordWL"] -multiplicity = "SHIFT" - -[[constraints.alu]] -kind = "template" -tag = "ADD" -input = ["pc", ["*", ["+", ["*", 2, "c_type_instruction"], ["*", 4, ["not", "c_type_instruction"]]], ["cast", 1, "DWordWL"]]] -output = ["cast", "res", "DWordWL"] -cond = "JALR" - -[[constraints.alu]] -kind = "interaction" -tag = "MUL" -input = [["cast", "arg1", "DWordHL"], "signed", ["cast", "arg2", "DWordHL"], "mp_selector", "muldiv_selector"] +tag = "ALU" +input = ["rv1", "arg2", "alu_flags"] output = ["cast", "res", "DWordWL"] -multiplicity = "MUL" +multiplicity = "ALU" +# TODO: double check [[constraints.alu]] kind = "interaction" -tag = "DVRM" -input = [["cast", "arg1", "DWordHL"], ["cast", "arg2", "DWordHL"], "signed", "muldiv_selector"] -output = ["cast", "res", "DWordWL"] -multiplicity = "DIVREM" +tag = "CPU32" +input = ["timestamp", "pc"] +multiplicity = "word_instr" [[constraint_groups]] @@ -655,8 +398,8 @@ prefix = "M" [[constraints.mem]] kind = "interaction" tag = "MEMW" -input = [1, ["*", ["cast", 2, "DWordWL"], "rs1"], ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", ["cast", "rv1", "DWordWL"], 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 0, "DWordWL"]], 1, 0, 0] -output = ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", ["cast", "rv1", "DWordWL"], 1], 0, 0, 0, 0, 0, 0] +input = [1, ["*", ["cast", 2, "DWordWL"], "rs1"], ["arr", ["idx", "rv1", 0], ["idx", "rv1", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 0, "DWordWL"]], 1, 0, 0] +output = ["arr", ["idx", "rv1", 0], ["idx", "rv1", 1], 0, 0, 0, 0, 0, 0] multiplicity = "read_register1" ref = "cpu:c:read_rv1" @@ -664,20 +407,20 @@ ref = "cpu:c:read_rv1" kind = "arith" constraint = "$#`!read_register1` => #`rv1[i]` = 0$" poly = ["*", ["not", "read_register1"], ["idx", "rv1", "i"]] -iter = ["i", 0, 2] +iter = ["i", 0, 1] [[constraints.mem]] kind = "interaction" tag = "MEMW" -input = [1, ["*", ["cast", 2, "DWordWL"], "rs2"], ["arr", ["idx", ["cast", "rv2", "DWordWL"], 0], ["idx", ["cast", "rv2", "DWordWL"], 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0] -output = ["arr", ["idx", ["cast", "rv2", "DWordWL"], 0], ["idx", ["cast", "rv2", "DWordWL"], 1], 0, 0, 0, 0, 0, 0] +input = [1, ["*", ["cast", 2, "DWordWL"], "rs2"], ["arr", ["idx", "rv2", 0], ["idx", "rv2", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0] +output = ["arr", ["idx", "rv2", 0], ["idx", "rv2", 1], 0, 0, 0, 0, 0, 0] multiplicity = "read_register2" [[constraints.mem]] kind = "arith" constraint = "$#`!read_register2` => #`rv2[i]` = 0$" poly = ["*", ["not", "read_register2"], ["idx", "rv2", "i"]] -iter = ["i", 0, 2] +iter = ["i", 0, 1] [[constraints.mem]] kind = "interaction" @@ -687,16 +430,16 @@ multiplicity = "write_register" [[constraints.mem]] kind = "interaction" -tag = "LOAD" -input = [["cast", "res", "DWordWL"], ["+", "timestamp", ["cast", 0, "DWordWL"]], "memory_2bytes", "memory_4bytes", "memory_8bytes", "signed"] +tag = "MEMORY" +input = ["timestamp", "res", "rv2", "mem_flags"] output = "rvd" -multiplicity = "LOAD" +multiplicity = "MEMORY" [[constraints.mem]] -kind = "interaction" -tag = "MEMW" -input = [0, ["cast", "res", "DWordWL"], ["cast", "arg2", ["Byte", 8]], ["+", "timestamp", ["cast", 1, "DWordWL"]], "memory_2bytes", "memory_4bytes", "memory_8bytes"] -multiplicity = "STORE" +kind = "arith" +constraint = "$!#`MEMORY` => #`rvd` = #`res`$" +poly = ["*", ["not", "MEMORY"], ["-", ["idx", "rvd", "i"], ["idx", ["cast", "res", "DWordWL"], "i"]]] +iter = ["i", 0, 1] [[constraints.mem]] kind = "template" @@ -712,124 +455,50 @@ input = ["prev_pc_timestamp_borrow"] kind = "interaction" tag = "memory" input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["arr", ["+", ["-", ["idx", "timestamp", 0], ["*", 3, ["not", "pc_double_read"]]], ["*", ["^", 2, 32], "prev_pc_timestamp_borrow"]], ["-", ["idx", "timestamp", 1], "prev_pc_timestamp_borrow"]], ["idx", "pc", "i"]] -multiplicity = ["not", "pad"] iter = ["i", 0, 1] +multiplicity = 1 [[constraints.mem]] kind = "interaction" tag = "memory" input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], ["idx", "next_pc", "i"]] -multiplicity = ["-", ["not", "pad"]] iter = ["i", 0, 1] - - -[[constraint_groups]] -name = "sys" -prefix = "S" - -[[constraints.sys]] -kind = "arith" -constraint = "`!EBREAK`" -desc = "We treat `EBREAK` as an unprovable trap" -poly = ["not", "EBREAK"] -ref = "cpu:c:ebreak_traps" - -[[constraints.sys]] -kind = "interaction" -tag = "ECALL" -input = ["timestamp", ["cast", "rv1", "DWordWL"]] -multiplicity = "ECALL" - - -[[constraint_groups]] -name = "ext" -prefix = "E" - -[[constraints.ext]] -kind = "template" -tag = "SIGN" -input = [["idx", "rv1", 1], "word_instr"] -output = "rv1_ext_bit" - -[[constraints.ext]] -kind = "arith" -constraint = "$#`arg1[:4]` = #`rv1[:2]`$" -poly = ["-", ["idx", ["cast", "arg1", "DWordWL"], 0], ["idx", ["cast", "rv1", "DWordWL"], 0]] - -[[constraints.ext]] -kind = "arith" -constraint = "$#`arg1[4:]` = #`rv1[2]` dot (1 - #`word_instr`) + (2^(32) - 1) dot #`rv1_ext_bit` dot #`signed`$" -poly = ["-", ["idx", ["cast", "arg1", "DWordWL"], 1], ["*", ["not", "word_instr"], ["idx", "rv1", 2]], ["*", "signed", "rv1_ext_bit", ["-", ["^", 2, 32], 1]]] - -[[constraints.ext]] -kind = "template" -tag = "SIGN" -input = [["idx", "rv2", 1], "word_instr"] -output = "rv2_ext_bit" - -[[constraints.ext]] -kind = "arith" -constraint = "$#`arg2[:4]` = (1 - #`LOAD`) dot #`rv2[:2]` + (1 - #`BEQ` - #`BLT` - #`STORE`) dot #`imm[0]`$" -poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 0], ["*", ["not", "LOAD"], ["idx", ["cast", "rv2", "DWordWL"], 0]], ["*", ["-", 1, "BEQ", "BLT", "STORE"], ["idx", "imm", 0]]] - -[[constraints.ext]] -kind = "arith" -constraint = "$#`arg2[4:]` = (1 - #`LOAD`) dot ((1 - #`word_instr`) dot #`rv2[2]` + #`signed` dot #`rv2_ext_bit` dot (2^(32) - 1)) + (1 - #`BEQ` - #`BLT` - #`STORE`) dot #`imm[1]`$" -poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 1], ["*", ["not", "LOAD"], ["not", "word_instr"], ["idx", "rv2", 2]], ["*", ["not", "LOAD"], "signed", "rv2_ext_bit", ["-", ["^", 2, 32], 1]], ["*", ["-", 1, "BEQ", "BLT", "STORE"], ["idx", "imm", 1]]] - -[[constraints.ext]] -kind = "template" -tag = "SIGN" -input = [["idx", ["cast", "res", "DWordHL"], 1], "word_instr"] -output = "res_ext_bit" - -[[constraints.ext]] -kind = "arith" -constraint = "$#`!LOAD` => #`rvd[0]` = #`res[:4]`$" -poly = ["*", ["not", "LOAD"], ["-", ["idx", "rvd", 0], ["idx", ["cast", "res", "DWordWL"], 0]]] - -[[constraints.ext]] -kind = "arith" -constraint = "$#`!LOAD` => #`rvd[1]` = (1 - #`word_instr`) dot #`res[4:]` + #`res_ext_bit` dot (2^(32) - 1)$" -desc = "_Sign_ extend the output if it wasn't a `LOAD`. Only `LOAD` has both `write_register = 1` and `rvd ≠ res`. `LOAD` and `word_instr` are disjoint" -poly = ["*", ["not", "LOAD"], ["-", ["idx", "rvd", 1], ["*", ["not", "word_instr"], ["idx", ["cast", "res", "DWordWL"], 1]], ["*", "res_ext_bit", ["-", ["^", 2, 32], 1]]]] - +multiplicity = 1 [[constraint_groups]] -name = "misc" -prefix = "O" +name = "branch" +prefix = "B" -[[constraints.misc]] -kind = "interaction" -tag = "ZERO" -input = [["+", ["idx", "res", 0], ["idx", "res", 1], ["idx", "res", 2], ["idx", "res", 3], ["idx", "res", 4], ["idx", "res", 5], ["idx", "res", 6], ["idx", "res", 7]]] -output = "is_equal" -multiplicity = "BEQ" -ref = "cpu:c:is_equal" - -[[constraints.misc]] +[[constraints.branch]] kind = "arith" -constraint = "$#`branch_cond` = #`JALR` or (#`BLT` and (#`res` xor #`invert`)) or (#`BEQ` and (#`is_equal` xor #`invert`))$" -desc = "where `invert` is represented by `mp_selector`" +constraint = "$#`branch_cond` = #`BRANCH` and (#`JALR` or #`res`)$" poly = ["+", ["-", "branch_cond"], - "JALR", - ["*", ["idx", "res", 0], ["not", "mp_selector"], "BLT"], - ["*", ["-", 1, ["idx", "res", 0]], "mp_selector", "BLT"], - ["*", "is_equal", ["not", "mp_selector"], "BEQ"], - ["*", ["not", "is_equal"], "mp_selector", "BEQ"] + ["*", "BRANCH", "JALR"], + ["*", "BRANCH", ["-", 1, "JALR"], ["idx", "res", 0]] ] -[[constraints.misc]] +[[constraints.branch]] kind = "interaction" tag = "BRANCH" -input = ["pc", "imm", ["cast", "arg1", "DWordWL"], "JALR"] +input = ["pc", "imm", "rv1", "JALR"] output = "next_pc" multiplicity = "branch_cond" -[[constraints.misc]] +[[constraints.branch]] kind = "template" tag = "ADD" -input = ["pc", ["*", ["+", ["*", 2, "c_type_instruction"], ["*", 4, ["not", "c_type_instruction"]]], ["cast", 1, "DWordWL"]]] +input = ["pc", ["arr", "instruction_length", 0]] output = "next_pc" desc = "Increment `pc` to `next_pc` if we're not branching" + + +[[constraint_groups]] +name = "sys" +prefix = "S" + +[[constraints.sys]] +kind = "interaction" +tag = "ECALL" +input = ["timestamp", "rv1"] +multiplicity = "ECALL" diff --git a/spec/src/load.toml b/spec/src/load.toml index f8a974c9a..587ecd3d7 100644 --- a/spec/src/load.toml +++ b/spec/src/load.toml @@ -110,6 +110,7 @@ input = [0, "base_address", ["cast", "res", ["BaseField", 8]], "timestamp", "rea output = "res" multiplicity = "μ" +# TODO? MSB8 batching? [[constraints.all]] kind = "interaction" tag = "MSB8" diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index e93c87b05..a6cfbee54 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -49,11 +49,24 @@ tag = "DECODE" kind = "interaction" input = ["DWordWL", "DWordWL", "BaseField"] -# SHIFT[out; in, shift, direction, signed, word_instr] +# CPU32[timestamp, pc] [[signatures]] -tag = "SHIFT" +tag = "CPU32" kind = "interaction" -input = ["DWordHL", "Byte", "Bit", "Bit", "Bit"] +input = ["DWordWL", "DWordWL"] + +# ALU[out; in1, in2, flags] +[[signatures]] +tag = "ALU" +kind = "interaction" +input = ["DWordWL", "DWordWL", "Byte"] +output = "DWordWL" + +# MEMORY[out; timestamp, address, value, flags] +[[signatures]] +tag = "MEMORY" +kind = "interaction" +input = ["DWordWL", "DWordHL", "DWordWL", "Byte"] output = "DWordWL" # BRANCH[next_pc; pc, offset, register, JALR] @@ -76,32 +89,11 @@ tag = "MEMW" kind = "interaction" input = ["Bit", "DWordWL", ["BaseField", 8], "DWordWL", "Bit", "Bit", "Bit"] -# LT[lt; lhs, rhs, signed] -[[signatures]] -tag = "LT" -kind = "interaction" -input = ["DWordWL", "DWordWL", "Bit"] -output = "Bit" - -# MUL[lo/hi; lhs, lhs_signed, rhs, rhs_signed, 0/1] -[[signatures]] -tag = "MUL" -kind = "interaction" -input = ["DWordHL", "Bit", "DWordHL", "Bit", "Bit"] -output = "DWordWL" - -# DVRM[q/r; n, d, signed, 0/1] -[[signatures]] -tag = "DVRM" -kind = "interaction" -input = ["DWordHL", "DWordHL", "Bit", "Bit"] -output = "DWordWL" - -# LOAD[res; base_address, timestamp, read2, read4, read8, signed] +# LOAD[res; base_address, timestamp, flags] [[signatures]] tag = "LOAD" kind = "interaction" -input = ["DWordWL", "DWordWL", "Bit", "Bit", "Bit", "Bit"] +input = ["DWordWL", "DWordWL", "Byte"] output = "DWordWL" # ECALL[timestamp, syscallnr] @@ -122,25 +114,11 @@ tag = "COMMIT" kind = "interaction" input = ["BaseField", "Byte"] -# AND_BYTE[res; X, Y] +# ALU_BYTE[res; selector, X, Y] [[signatures]] -tag = "AND_BYTE" +tag = "ALU_BYTE" kind = "interaction" -input = ["Byte", "Byte"] -output = "Byte" - -# OR_BYTE[res; X, Y] -[[signatures]] -tag = "OR_BYTE" -kind = "interaction" -input = ["Byte", "Byte"] -output = "Byte" - -# XOR_BYTE[res; X, Y] -[[signatures]] -tag = "XOR_BYTE" -kind = "interaction" -input = ["Byte", "Byte"] +input = ["Byte", "Byte", "Byte"] output = "Byte" # MSB8[msb; X] From eaffb54bc4471a5a111e0b1d1c1e98b1e99fc0bb Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 26 May 2026 15:39:59 +0200 Subject: [PATCH 02/25] Decoding for the new CPU --- spec/decode.typ | 98 +++++++++++--------- spec/src/cpu.toml | 4 +- spec/src/decode.toml | 44 +++------ spec/src/decode_uncompressed.toml | 148 ++++++++++++++---------------- 4 files changed, 143 insertions(+), 151 deletions(-) diff --git a/spec/decode.typ b/spec/decode.typ index c839287f8..3f1bb9758 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -34,25 +34,42 @@ Empty rows with the following content can be added to achieve this: #render_chip_padding_table(chip, config) -#rj[note to self: remove EBREAK rows] -Note that this row sets the `EBREAK` flag. -Given that `CPU` asserts that `EBREAK = 0`, using this "padding-instruction" would immediately make the CPU table unprovable. -Note moreover that the `pc` is set to $7$. -This value is the _smallest odd number_ (i.e., not reachable during regular execution) that is more than _$4$_ (i.e., the max `pc`-increment) greater than _$1$_ (i.e., the `pc`-value used in the #link()[additional instruction] referred to by `CPU`-padding lines). +This is simultaneously the row that is used for padding rows in the CPU, +if the multiplicity if nonzero, +so we need to ensure that this table has at least one row of padding. = Decoding For the purposes of explaining decoding, we decompress #decode's `packed_decode` variable into its constituent variables. Note that the below table is _not_ used in practice: it is solely used for the purposes of this explanation. +The construction of the `alu_flags` and `mem_flags` columns is given here through virtual columns. #let config = load_config() #let uncompressed_chip = load_chip("src/decode_uncompressed.toml", config) #render_chip_variable_table(uncompressed_chip, config) +First, we provide a mapping from an an ALU operation "descriptor" to the numerical value as used for the `alu_op` column: + +#figure( + table(columns: (auto, auto), + stroke: 0pt, + inset: (right: .5em), + align: (left, left), table.header[*Descriptor*][*value*], table.hline(stroke: 1.5pt))[ + *AND*][0][ + *OR*][1][ + *XOR*][2][ + *EQ*][3][ + *LT*][4][ + *SHIFT*][5][ + *MUL*][6][ + *DIVREM*][7] +) + We will illustrate how each instruction should be expressed in this (uncompressed) decoding table. The columns of the accompanying table represent the following: - *`operation`*: the assembly operation being encoded. -- *`op-flag`*: which of the "`ALU` selector flags" operation flags to set. Each operation sets exactly one. +- *`alu`*: Set to the descriptor of the ALU operation to be used for `alu_op`. + If listed as `ADD` or `SUB`, the corresponding flag should be set, otherwise set `ALU = 1` when this column is not empty. - *`w_instr`*, *`signed`*: whether to set the `word_instr` and `signed` flags, respectively. - *other*: the other flags that should be set or variables that should be given specific values. @@ -60,8 +77,6 @@ For the purpose of brevity and readability, the table uses the following rules-o + `rd`, `rs1`, `rs2`, and `imm` are mapped to the values provided by the instruction; when a value is not specified by an instruction it defaults to $0$. + `read_register1`, `read_register2` and `write_register` are set to $1$ when respectively $#`rs1` != 0$, $#`rs2` != 0$, or $#`rd` != 0$. -+ Any flag that is not listed is set to $0$, with the exception of the `c_type` flag. - *The `c_type` flag is set independently of the below table*, as explained next. Further clarification is provided in the notes following the table. @@ -82,38 +97,38 @@ Further clarification is provided in the notes following the table. // Overlay a low-opacity fill color to distinguish the different rows better if calc.odd(y) and y <= lines.len() { color.rgb(0, 0, 100, 20) } else { color.rgb(255, 255, 255, 20) }, - table.header([*Operation*], [*op-flag*], [*`w_instr`*], [*`signed`*], [*other*], []), + table.header([*Operation*], [*alu*], [*`w_instr`*], [*`signed`*], [*other*], []), table.hline(stroke: 1.5pt), table.vline(x: 1, start: 1, end: lines.len() + 1, stroke: .5pt), ..lines.flatten(), table.hline(stroke: 1.5pt), - table.footer([*Operation*], [*op-flag*], [*`w_instr`*], [*`signed`*], [*other*]), + table.footer([*Operation*], [*alu*], [*`w_instr`*], [*`signed`*], [*other*]), )) } #let decoding = ( // OP-IMM ([`ADDI[W] rd, rs1, imm`], [`ADD`], [`[W]`], [], [], [#ref_note()]), - ([`SLTI[U] rd, rs1, imm`], [`SLT`], [], [#sym.not`[U]`], [], [#ref_note()]), + ([`SLTI[U] rd, rs1, imm`], [`LT`], [], [#sym.not`[U]`], [], [#ref_note()]), ([`ANDI rd, rs1, imm`], [`AND`], [], [], [], []), ([`ORI rd, rs1, imm`], [`OR`], [], [], [], []), ([`XORI rd, rs1, imm`], [`XOR`], [], [], [], []), ([`SLLI[W] rd, rs1, imm`], [`SHIFT`], [`[W]`], [], [], []), - ([`SRLI[W] rd, rs1, imm`], [`SHIFT`], [`[W]`], [], [`mp_selector`], [#ref_note()]), - ([`SRAI[W] rd, rs1, imm`], [`SHIFT`], [`[W]`], [1], [`mp_selector`], [#ref_note()]), + ([`SRLI[W] rd, rs1, imm`], [`SHIFT`], [`[W]`], [], [`invert`], [#ref_note()]), + ([`SRAI[W] rd, rs1, imm`], [`SHIFT`], [`[W]`], [1], [`invert`], [#ref_note()]), // OP ([`ADD[W] rd, rs1, rs2`], [`ADD`], [`[W]`], [], [], [#ref_note()]), ([`SUB[W] rd, rs1, rs2`], [`SUB`], [`[W]`], [], [], [#ref_note()]), - ([`SLT[U] rd, rs1, rs2`], [`SLT`], [], [#sym.not`[U]`], [], [#ref_note()]), + ([`SLT[U] rd, rs1, rs2`], [`LT`], [], [#sym.not`[U]`], [], [#ref_note()]), ([`AND rd, rs1, rs2`], [`AND`], [], [], [], []), ([`OR rd, rs1, rs2`], [`OR`], [], [], [], []), ([`XOR rd, rs1, rs2`], [`XOR`], [], [], [], []), ([`SLL[W] rd, rs1, rs2`], [`SHIFT`], [`[W]`], [], [], [#ref_note()]), - ([`SRL[W] rd, rs1, rs2`], [`SHIFT`], [`[W]`], [], [`mp_selector`], [#ref_note()]), - ([`SRA[W] rd, rs1, rs2`], [`SHIFT`], [`[W]`], [1], [`mp_selector`], [#ref_note()]), + ([`SRL[W] rd, rs1, rs2`], [`SHIFT`], [`[W]`], [], [`invert`], [#ref_note()]), + ([`SRA[W] rd, rs1, rs2`], [`SHIFT`], [`[W]`], [1], [`invert`], [#ref_note()]), // OP - M - ([`MUL[W] rd, rs1, rs2`], [`MUL`], [`[W]`], [1], [`mp_selector`], [#ref_note()]), - ([`MULH rd, rs1, rs2`], [`MUL`], [], [1], [`mp_selector`, `muldiv_selector`], []), + ([`MUL[W] rd, rs1, rs2`], [`MUL`], [`[W]`], [1], [`signed2`], [#ref_note()]), + ([`MULH rd, rs1, rs2`], [`MUL`], [], [1], [`signed2`, `muldiv_selector`], []), ([`MULHU rd, rs1, rs2`], [`MUL`], [], [], [`muldiv_selector`], []), ([`MULHSU rd, rs1, rs2`], [`MUL`], [], [1], [`muldiv_selector`], []), ([`DIV[U][W] rd, rs1, rs2`], [`DIVREM`], [`[W]`], [#sym.not`[U]`], [], [#ref_note(, )]), @@ -121,37 +136,41 @@ Further clarification is provided in the notes following the table. // LUI/AUIPC ([`LUI rd, imm`], [`ADD`], [], [], [], [#ref_note()]), ([`AUIPC rd, imm`], [`ADD`], [], [], [`rs1 := x255`], [#ref_note()]), - ([`JAL rd, imm`], [`JALR`], [], [], [`rs1 := x255`], [#ref_note()]), + ([`JAL rd, imm`], [`ADD`], [], [], [`BRANCH`, `JALR`, `rs1 := x255`], [#ref_note()]), // Branching - ([`JALR rd, rs1, imm`], [`JALR`], [], [], [], []), - ([`BEQ rs1, rs2, imm`], [`BEQ`], [], [], [], []), - ([`BNE rs1, rs2, imm`], [`BEQ`], [], [], [`mp_selector`], []), - ([`BLT[U] rs1, rs2, imm`], [`BLT`], [], [#sym.not`[U]`], [], [#ref_note()]), - ([`BGE[U] rs1, rs2, imm`], [`BLT`], [], [#sym.not`[U]`], [`mp_selector`], [#ref_note()]), + ([`JALR rd, rs1, imm`], [`ADD`], [], [], [`BRANCH`, `JALR`], []), + ([`BEQ rs1, rs2, imm`], [`EQ`], [], [], [], []), + ([`BNE rs1, rs2, imm`], [`EQ`], [], [], [`invert`], []), + ([`BLT[U] rs1, rs2, imm`], [`LT`], [], [#sym.not`[U]`], [], [#ref_note()]), + ([`BGE[U] rs1, rs2, imm`], [`LT`], [], [#sym.not`[U]`], [`invert`], [#ref_note()]), // LOAD - ([`LD rd, rs1, imm`], [`LOAD`], [], [], [`mem_8B`], []), - ([`LW[U] rd, rs1, imm`], [`LOAD`], [], [#sym.not`[U]`], [`mem_4B`], [#ref_note()]), - ([`LH[U] rd, rs1, imm`], [`LOAD`], [], [#sym.not`[U]`], [`mem_2B`], [#ref_note()]), - ([`LB[U] rd, rs1, imm`], [`LOAD`], [], [#sym.not`[U]`], [], [#ref_note()]), + ([`LD rd, rs1, imm`], [`ADD`], [], [], [`MEMORY`, `mem_8B`], []), + ([`LW[U] rd, rs1, imm`], [`ADD`], [], [#sym.not`[U]`], [`MEMORY`, `mem_4B`], [#ref_note()]), + ([`LH[U] rd, rs1, imm`], [`ADD`], [], [#sym.not`[U]`], [`MEMORY`, `mem_2B`], [#ref_note()]), + ([`LB[U] rd, rs1, imm`], [`ADD`], [], [#sym.not`[U]`], [`MEMORY`, ], [#ref_note()]), // STORE - ([`SD rs1, rs2, imm`], [`STORE`], [], [], [`mem_8B`], []), - ([`SW rs1, rs2, imm`], [`STORE`], [], [], [`mem_4B`], []), - ([`SH rs1, rs2, imm`], [`STORE`], [], [], [`mem_2B`], []), - ([`SB rs1, rs2, imm`], [`STORE`], [], [], [], []), + ([`SD rs1, rs2, imm`], [`ADD`], [], [], [`MEMORY`, `memory_op`, `mem_8B`], []), + ([`SW rs1, rs2, imm`], [`ADD`], [], [], [`MEMORY`, `memory_op`, `mem_4B`], []), + ([`SH rs1, rs2, imm`], [`ADD`], [], [], [`MEMORY`, `memory_op`, `mem_2B`], []), + ([`SB rs1, rs2, imm`], [`ADD`], [], [], [`MEMORY`, `memory_op`], []), // ECALL/EBREAK - ([`ECALL`], [`ECALL`], [], [], [$#`rs1` := #`x17`$], [#ref_note()]), - ([`EBREAK`], [`EBREAK`], [], [], [], []), + ([`ECALL`], [], [], [], [`ECALL`, $#`rs1` := #`x17`$], [#ref_note()]), // FENCE ([`FENCE`], [`ADD`], [], [], [], [#ref_note()]), ) #decoding_table(decoding) +Note that the above table has no entry for the `EBREAK` instruction. +We treat `EBREAK` as an unprovable trap, and its absence from the table enables +this by having no valid decoding available for when the instruction is encountered. + == C-type instructions The `RV64C` extension for compressed instructions specifies that \~50% of all instructions can be represented using a 16-bit instruction (rather than 32-bits), saving \~25% in code size. This execution of assembly code is _not_ agnostic to an instruction's compression state; after executing a compressed instruction, the `pc` should be incremented by $2$ rather than $4$. -To indicate an instruction is provided in compressed form, the `c_type` flag is introduced. -*This flag should be set to $1$ whenever the decoded instruction is provided in compressed form and $0$ otherwise.* +As such, we provide the `instruction_length` column that *must take on the value $2$ for compressed instructions and $4$ for regular instructions*. +This additionally opens the door for future optimizations involving "fused" instructions, where common sequences +of instructions are merged into a single decoded version and need only a single CPU row to prove. // Construct a note that can be referenced through `lbl` #let referenceable_note(lbl, note) = { @@ -213,10 +232,3 @@ We note the following about the above decoding table: ) ) ) - -== One more instruction -In addition to decoding all instructions provided in the ELF and adding a corresponding entry to the #decode table, one must include an entry that has $#`pc` = 1$ and every other variable set to $0$. -Note that this will never conflict with any entry in the ELF, since it has an odd `pc` value. - -This entry is used to pad the `CPU` table. -More details on this matter are provided in the `CPU` chip. diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 358651585..4f98b26ca 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -62,7 +62,7 @@ pad = 0 name = "instruction_length" type = "Byte" desc = "The number of bytes consumed by this instruction, commonly used to indicate whether the instruction is of C type, i.e., whether it is 2 bytes long instead of 4" -pad = 4 +pad = 0 [[variables.input]] name = "word_instr" @@ -123,7 +123,7 @@ pad = 0 name = "next_pc" type = "DWordWL" desc = "The program counter for the next instruction" -pad = 5 +pad = 1 [[variables.output]] name = "rvd" diff --git a/spec/src/decode.toml b/spec/src/decode.toml index 367db1568..17a10f57c 100644 --- a/spec/src/decode.toml +++ b/spec/src/decode.toml @@ -4,7 +4,7 @@ name = "DECODE" name = "pc" type = "DWordWL" desc = "value of the program counter this instruction is associated with." -pad = 7 +pad = 1 [[variables.output]] name = "packed_decode" @@ -15,36 +15,22 @@ A list of each variable and the bit(-range) in which it is located:\\ [0] `read_register1`, \\ [1] `read_register2`, \\ [2] `write_register`, \\ -[3] `memory_2bytes`, \\ -[4] `memory_4bytes`, \\ -[5] `memory_8bytes`, \\ -[6] `c_type`, \\ -[7] `signed`, \\ -[8] `mp_selector`, \\ -[9] `muldiv_selector`, \\ -[10] `word_instr`, \\ -[11] `ADD`, \\ -[12] `SUB`, \\ -[13] `SLT`, \\ -[14] `AND`, \\ -[15] `OR`, \\ -[16] `XOR`, \\ -[17] `SHIFT`, \\ -[18] `JALR`, \\ -[19] `BEQ`, \\ -[20] `BLT`, \\ -[21] `LOAD`, \\ -[22] `STORE`, \\ -[23] `MUL`, \\ -[24] `DIVREM`, \\ -[25] `ECALL`, \\ -[26] `EBREAK`; \\ -[27:35] `rs1`, \\ -[35:43] `rs2`, \\ -[43:51] `rd`, \\ +[3] `word_instr`, \\ +[4] `ALU`, \\ +[5] `ADD`, \\ +[6] `SUB`, \\ +[7] `MEMORY`, \\ +[8] `BRANCH`, \\ +[9] `ECALL`, \\ +[10:17] `rs1`, \\ +[18:25] `rs2`, \\ +[26:33] `rd`, \\ +[34:41] `instruction_length`, \\ +[42:49] `alu_flags`, \\ +[50:57] `mem_flags`, \\ the remaining bits are set to zero. """ -pad = ["^", 2, 26] +pad = 0 [[variables.output]] name = "imm" diff --git a/spec/src/decode_uncompressed.toml b/spec/src/decode_uncompressed.toml index 0f6c931c2..ce31573b5 100644 --- a/spec/src/decode_uncompressed.toml +++ b/spec/src/decode_uncompressed.toml @@ -35,131 +35,125 @@ name = "write_register" type = "Bit" desc = "whether the result should be written to `rd` ($=0$ for memory write and when $#`rd` = #`x0`$." -[[variables.output]] -name = "mem_2B" -type = "Bit" -desc = "whether the memory access (read or write) touches exactly $2$ bytes." - -[[variables.output]] -name = "mem_4B" -type = "Bit" -desc = "whether the memory access (read or write) touches exactly $4$ bytes." - -[[variables.output]] -name = "mem_8B" -type = "Bit" -desc = "whether the memory access (read or write) touches exactly $8$ bytes." - -[[variables.output]] -name = "c_type" -type = "Bit" -desc = "Whether the instruction is of type `C`, i.e., whether it is $2$ bytes long instead of $4$." - [[variables.output]] name = "imm" type = "DWordWL" desc = "the *fully extended (!)* 64-bit version of the immediate." [[variables.output]] -name = "signed" -type = "Bit" -desc = "selector used to indicate signed or unsigned input interpretation." - -[[variables.output]] -name = "mp_selector" -type = "Bit" -desc = """Multi-purpose selector used by the CPU to to configure several ALU operations in different ways. - See the `CPU` chip for more details.""" - -[[variables.output]] -name = "muldiv_selector" +name = "word_instr" type = "Bit" -desc = "selects which output of `MUL` (lo/hi) or `DVRM` (quo/rem) is wanted." +desc = "Whether the instruction is a `*W` instruction, requiring the inputs and outputs to be (sign) extended." [[variables.output]] -name = "word_instr" +name = "ALU" type = "Bit" -desc = "Whether the instruction is a `*W` instruction, requiring the inputs and outputs to be (sign) extended." +desc = "Enable the ALU" [[variables.output]] name = "ADD" type = "Bit" -desc = "ALU selector flag" +desc = "ALU does an ADD" [[variables.output]] name = "SUB" type = "Bit" -desc = "ALU selector flag" +desc = "ALU does a SUB" [[variables.output]] -name = "SLT" +name = "BRANCH" type = "Bit" -desc = "ALU selector flag" +desc = "The instruction is a branch" [[variables.output]] -name = "AND" +name = "MEMORY" type = "Bit" -desc = "ALU selector flag" +desc = "The instruction is a memory access" [[variables.output]] -name = "OR" +name = "ECALL" type = "Bit" -desc = "ALU selector flag" +desc = "Perform an ECALL" [[variables.output]] -name = "XOR" -type = "Bit" -desc = "ALU selector flag" +name = "instruction_length" +type = "Byte" +desc = "How many bytes is this instruction in the program" -[[variables.output]] -name = "SHIFT" -type = "Bit" -desc = "ALU selector flag" +[[variables.auxiliary]] +name = "alu_op" +type = "Byte" +desc = "Operation selector value for the ALU" -[[variables.output]] -name = "JALR" +[[variables.auxiliary]] +name = "signed" type = "Bit" -desc = "ALU selector flag" +desc = "selector used to indicate signed or unsigned input interpretation." -[[variables.output]] -name = "BEQ" +[[variables.auxiliary]] +name = "signed2" type = "Bit" -desc = "ALU selector flag" +desc = """A second signed bit, useful for MUL instructions""" -[[variables.output]] -name = "BLT" +[[variables.auxiliary]] +name = "muldiv_selector" type = "Bit" -desc = "ALU selector flag" +desc = "selects which output of `MUL` (lo/hi) or `DVRM` (quo/rem) is wanted." -[[variables.output]] -name = "LOAD" +[[variables.auxiliary]] +name = "invert" type = "Bit" -desc = "ALU selector flag" +desc = "Instructs the EQ or LT chip to invert its result, or inverts the direction of the SHIFT chip (right instead of left)" -[[variables.output]] -name = "STORE" +[[variables.auxiliary]] +name = "memory_op" type = "Bit" -desc = "ALU selector flag" +desc = "Selects whether to LOAD (0) or STORE (1)" -[[variables.output]] -name = "MUL" +[[variables.auxiliary]] +name = "mem_2B" type = "Bit" -desc = "ALU selector flag" +desc = "whether the memory access (read or write) touches exactly $2$ bytes." -[[variables.output]] -name = "DIVREM" +[[variables.auxiliary]] +name = "mem_4B" type = "Bit" -desc = "ALU selector flag" +desc = "whether the memory access (read or write) touches exactly $4$ bytes." -[[variables.output]] -name = "ECALL" +[[variables.auxiliary]] +name = "mem_8B" type = "Bit" -desc = "ALU selector flag" +desc = "whether the memory access (read or write) touches exactly $8$ bytes." -[[variables.output]] -name = "EBREAK" +[[variables.auxiliary]] +name = "JALR" type = "Bit" -desc = "ALU selector flag" +desc = "The branch is a JAL(R)" + +[[variables.virtual]] +name = "alu_flags" +type = "Byte" +desc = "The combined ALU flags" +def = ["+", + "alu_op", + ["*", 32, "signed"], + ["*", 64, ["+", "signed2", "invert"]], + ["*", 128, "muldiv_selector"] +] + +[[variables.virtual]] +name = "mem_flags" +type = "Byte" +desc = "The combined memory flags (or JALR when BRANCHing)" +def = ["+", + "JALR", + "memory_op", + ["*", 2, "signed"], + ["*", 4, "mem_2B"], + ["*", 8, "mem_4B"], + ["*", 16, "mem_8B"] +] + [[variables.multiplicity]] name = "μ" From 97c17ce46f94ccf5ef9ee57c9b1adfff53ffc745 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 26 May 2026 15:49:20 +0200 Subject: [PATCH 03/25] Bitwise using BYTE_ALU --- spec/bitwise.typ | 4 ++++ spec/src/bitwise.toml | 12 ++++++------ spec/src/signatures.toml | 4 ++-- 3 files changed, 12 insertions(+), 8 deletions(-) diff --git a/spec/bitwise.typ b/spec/bitwise.typ index 332bef3d9..1babeefcc 100644 --- a/spec/bitwise.typ +++ b/spec/bitwise.typ @@ -26,11 +26,15 @@ and convenience functionalities over small domains. 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_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)$. +We use the ALU operation descriptors from @decode to identify the operations in the `BYTE_ALU` interaction. +Since each of the three columns is only $2^16$ rows long, they can be combined in a single $2^20$ column (with room to spare). + = Lookup This chip adds the following interactions to the lookup: #render_constraint_table(chip, config) diff --git a/spec/src/bitwise.toml b/spec/src/bitwise.toml index 30875a810..a89f7fcb6 100644 --- a/spec/src/bitwise.toml +++ b/spec/src/bitwise.toml @@ -127,22 +127,22 @@ name = "contributions" [[constraints.contributions]] kind = "interaction" -tag = "AND_BYTE" -input = ["X", "Y"] +tag = "BYTE_ALU" +input = [0, "X", "Y"] output = "AND" multiplicity = ["-", "μ_AND"] [[constraints.contributions]] kind = "interaction" -tag = "OR_BYTE" -input = ["X", "Y"] +tag = "BYTE_ALU" +input = [1, "X", "Y"] output = "OR" multiplicity = ["-", "μ_OR"] [[constraints.contributions]] kind = "interaction" -tag = "XOR_BYTE" -input = ["X", "Y"] +tag = "BYTE_ALU" +input = [2, "X", "Y"] output = "XOR" multiplicity = ["-", "μ_XOR"] diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index a6cfbee54..babcc1650 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -114,9 +114,9 @@ tag = "COMMIT" kind = "interaction" input = ["BaseField", "Byte"] -# ALU_BYTE[res; selector, X, Y] +# BYTE_ALU[res; selector, X, Y] [[signatures]] -tag = "ALU_BYTE" +tag = "BYTE_ALU" kind = "interaction" input = ["Byte", "Byte", "Byte"] output = "Byte" From c003b616af6876d9c9a6484a60186fd0fdc7b5f6 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 26 May 2026 17:34:19 +0200 Subject: [PATCH 04/25] Update old chips for the new CPU --- spec/decode.typ | 17 ++++----- spec/dvrm.typ | 11 ++++-- spec/expr.typ | 8 +++++ spec/mul.typ | 6 ++-- spec/src/bitwise.toml | 6 ++-- spec/src/branch.toml | 4 +-- spec/src/config.toml | 9 +++++ spec/src/cpu.toml | 9 ++--- spec/src/dvrm.toml | 55 ++++++++++++++++------------ spec/src/keccak_round.toml | 28 +++++++-------- spec/src/load.toml | 50 +++++++++++++++----------- spec/src/lt.toml | 16 +++++---- spec/src/memw.toml | 24 ++++++------- spec/src/memw_aligned.toml | 6 ++-- spec/src/mul.toml | 34 ++++++++++-------- spec/src/rotxor.toml | 8 ++--- spec/src/sha256round.toml | 20 +++++------ spec/src/shift.toml | 73 +++++++++++++++++++++++++------------- spec/tooling/chip.py | 7 ++++ 19 files changed, 233 insertions(+), 158 deletions(-) diff --git a/spec/decode.typ b/spec/decode.typ index 3f1bb9758..6b6c51454 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -61,8 +61,9 @@ First, we provide a mapping from an an ALU operation "descriptor" to the numeric *EQ*][3][ *LT*][4][ *SHIFT*][5][ - *MUL*][6][ - *DIVREM*][7] + *SHIFTW*][6][ + *MUL*][7][ + *DIVREM*][8] ) We will illustrate how each instruction should be expressed in this (uncompressed) decoding table. @@ -113,9 +114,9 @@ Further clarification is provided in the notes following the table. ([`ANDI rd, rs1, imm`], [`AND`], [], [], [], []), ([`ORI rd, rs1, imm`], [`OR`], [], [], [], []), ([`XORI rd, rs1, imm`], [`XOR`], [], [], [], []), - ([`SLLI[W] rd, rs1, imm`], [`SHIFT`], [`[W]`], [], [], []), - ([`SRLI[W] rd, rs1, imm`], [`SHIFT`], [`[W]`], [], [`invert`], [#ref_note()]), - ([`SRAI[W] rd, rs1, imm`], [`SHIFT`], [`[W]`], [1], [`invert`], [#ref_note()]), + ([`SLLI[W] rd, rs1, imm`], [`SHIFT[W]`], [`[W]`], [], [], []), + ([`SRLI[W] rd, rs1, imm`], [`SHIFT[W]`], [`[W]`], [], [`invert`], [#ref_note()]), + ([`SRAI[W] rd, rs1, imm`], [`SHIFT[W]`], [`[W]`], [1], [`invert`], [#ref_note()]), // OP ([`ADD[W] rd, rs1, rs2`], [`ADD`], [`[W]`], [], [], [#ref_note()]), ([`SUB[W] rd, rs1, rs2`], [`SUB`], [`[W]`], [], [], [#ref_note()]), @@ -123,9 +124,9 @@ Further clarification is provided in the notes following the table. ([`AND rd, rs1, rs2`], [`AND`], [], [], [], []), ([`OR rd, rs1, rs2`], [`OR`], [], [], [], []), ([`XOR rd, rs1, rs2`], [`XOR`], [], [], [], []), - ([`SLL[W] rd, rs1, rs2`], [`SHIFT`], [`[W]`], [], [], [#ref_note()]), - ([`SRL[W] rd, rs1, rs2`], [`SHIFT`], [`[W]`], [], [`invert`], [#ref_note()]), - ([`SRA[W] rd, rs1, rs2`], [`SHIFT`], [`[W]`], [1], [`invert`], [#ref_note()]), + ([`SLL[W] rd, rs1, rs2`], [`SHIFT[W]`], [`[W]`], [], [], [#ref_note()]), + ([`SRL[W] rd, rs1, rs2`], [`SHIFT[W]`], [`[W]`], [], [`invert`], [#ref_note()]), + ([`SRA[W] rd, rs1, rs2`], [`SHIFT[W]`], [`[W]`], [1], [`invert`], [#ref_note()]), // OP - M ([`MUL[W] rd, rs1, rs2`], [`MUL`], [`[W]`], [1], [`signed2`], [#ref_note()]), ([`MULH rd, rs1, rs2`], [`MUL`], [], [1], [`signed2`, `muldiv_selector`], []), diff --git a/spec/dvrm.typ b/spec/dvrm.typ index 1118aa10a..053155b40 100644 --- a/spec/dvrm.typ +++ b/spec/dvrm.typ @@ -27,10 +27,14 @@ The #dvrm chip provides division and remainder functionality, both signed and un The #dvrm chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): #render_chip_variable_table(chip, config) -= Assumptions -#render_chip_assumptions(chip, config) +// = Assumptions +// #render_chip_assumptions(chip, config) = Constraints + +First, we range-check all inputs. +#render_constraint_table(chip, config, groups: "range") + From the ISA, we gather five requirements for the `DIV[U][W]` and `REM[U][W]` instructions: #enum(numbering: "R1.", enum.item([ @@ -106,7 +110,8 @@ Rewriting R1, we find the constraint $not#`overflow` => #`n` - #`r` = #`qd`$. #footnote([Recall that @dvrm:c:sign_q allows to assert this equality even when `overflow`.]) Since `n`, `d`, `q` and `r` are all 64-bit integers, we must assert this equality $mod 2^128$, rather than $mod 2^64$. To this end, we introduce `extended_n_sub_r` and leverage the `MUL` chip to verify that it is equal to $#`qd` mod 2^128$ using constraints @dvrm:c:mul_lower and @dvrm:c:mul_upper; -@dvrm:c:q_range is included to uphold assumption @mul:a:rhs. +@dvrm:c:q_range is included to uphold assumption @mul:c:rhs. +// TODO: Update because this is now checked by MUL #render_constraint_table(chip, config, groups:("equality", )) diff --git a/spec/expr.typ b/spec/expr.typ index 20a55d753..98f9ee890 100644 --- a/spec/expr.typ +++ b/spec/expr.typ @@ -99,6 +99,10 @@ // Typeset an expression as code #let expr_to_code = make_expr_formatter( ( + "opsel": (pp, rec, e) => { + assert(type(e.at(1)) == type(""), message: "opsel expects a string") + repr(e.at(1)) + }, "arr": (pp, rec, e) => `[` + e.slice(1).map(rec.with(PREC.MAX)).join(`, `) + `]`, "idx": (pp, rec, e) => rec(PREC.MIN, e.at(1)) + `[` + rec(PREC.MAX, e.at(2)) + `]`, "not": (pp, rec, e) => cwrap(rec(PREC.not, 1) + ` - ` + rec(PREC.not, e.at(1)), pp < PREC.not), @@ -165,6 +169,10 @@ // Typeset an expression as math #let expr_to_math = make_expr_formatter( ( + "opsel": (pp, rec, e) => { + assert(type(e.at(1)) == type(""), message: "opsel expects a string") + $#repr(e.at(1))$ + }, "arr": (pp, rec, e) => $[#e.slice(1).map(rec.with(PREC.MAX)).join($, $)]$, "idx": (pp, rec, e) => { let (val, idxs) = flat_idxs(e) diff --git a/spec/mul.typ b/spec/mul.typ index 6e6de12e0..25a5e9884 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -32,9 +32,9 @@ The #mul chip is comprised of #nr_variables variables that are expressed using # $mat(delim: #none, top; bottom)$ } -= Assumptions -The following range checks are assumed to be performed/enforced outside of this chip: -#render_chip_assumptions(chip, config) +// = Assumptions +// The following range checks are assumed to be performed/enforced outside of this chip: +// #render_chip_assumptions(chip, config) = Constraints == Overview diff --git a/spec/src/bitwise.toml b/spec/src/bitwise.toml index a89f7fcb6..24b54442a 100644 --- a/spec/src/bitwise.toml +++ b/spec/src/bitwise.toml @@ -128,21 +128,21 @@ name = "contributions" [[constraints.contributions]] kind = "interaction" tag = "BYTE_ALU" -input = [0, "X", "Y"] +input = [["opsel", "AND"], "X", "Y"] output = "AND" multiplicity = ["-", "μ_AND"] [[constraints.contributions]] kind = "interaction" tag = "BYTE_ALU" -input = [1, "X", "Y"] +input = [["opsel", "OR"], "X", "Y"] output = "OR" multiplicity = ["-", "μ_OR"] [[constraints.contributions]] kind = "interaction" tag = "BYTE_ALU" -input = [2, "X", "Y"] +input = [["opsel", "XOR"], "X", "Y"] output = "XOR" multiplicity = ["-", "μ_XOR"] diff --git a/spec/src/branch.toml b/spec/src/branch.toml index 49a7833a3..07af5f7c9 100644 --- a/spec/src/branch.toml +++ b/spec/src/branch.toml @@ -123,8 +123,8 @@ cond = "μ" [[constraints.all]] kind = "interaction" -tag = "AND_BYTE" -input = ["unmasked_low_byte", 254] +tag = "BYTE_ALU" +input = [["opsel", "AND"], "unmasked_low_byte", 254] output = ["idx", "next_pc_low", 0] multiplicity = "μ" diff --git a/spec/src/config.toml b/spec/src/config.toml index 9ced2ce0d..9eac1d8c8 100644 --- a/spec/src/config.toml +++ b/spec/src/config.toml @@ -91,6 +91,15 @@ desc = """\ The `Word` is the *most* significant digit. """ +[[variables.types]] +label = "DWordWHBB" +subtypes = ["Byte", "Byte", "Half", "Word"] +desc = """\ + Variable that can only assume values in the range $[0, 2^64)$. \\ + Represented as a `Word`, a `Half` and two `Byte` variables. \ + The `Word` is the *most* significant digit. + """ + [[variables.types]] label = "WordBL" subtypes = ["Byte", "Byte", "Byte", "Byte"] diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 4f98b26ca..e32c45da6 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -261,10 +261,9 @@ input = ["write_register"] ref = "cpu:c:range_write_register" [[constraints.range]] -kind = "interaction" +kind = "template" tag = "IS_BYTE" input = ["instruction_length"] -multiplicity = 1 ref = "cpu:c:range_c_type_instruction" [[constraints.range]] @@ -280,10 +279,9 @@ input = ["ALU"] ref = "cpu:c:range_ALU" [[constraints.range]] -kind = "interaction" +kind = "template" tag = "IS_BYTE" input = ["alu_flags"] -multiplicity = 1 ref = "cpu:c:range_alu_flags" [[constraints.range]] @@ -305,10 +303,9 @@ input = ["MEMORY"] ref = "cpu:c:range_MEMORY" [[constraints.range]] -kind = "interaction" +kind = "template" tag = "IS_BYTE" input = ["mem_flags"] -multiplicity = 1 ref = "cpu:c:range_mem_flags" [[constraints.range]] diff --git a/spec/src/dvrm.toml b/spec/src/dvrm.toml index 52583907c..6ff9b994c 100644 --- a/spec/src/dvrm.toml +++ b/spec/src/dvrm.toml @@ -182,23 +182,32 @@ desc = "" pad = 0 -# Assumptions +# Constraints -[[assumptions]] -desc = "`IS_HALF[n[i]]`" -iter = ["i", 0, 3] -ref = "lt:a:range_n" +[[constraint_groups]] +name = "range" -[[assumptions]] -desc = "`IS_HALF[d[i]]`" +[[constraints.range]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "n", "i"]] iter = ["i", 0, 3] -ref = "lt:a:range_d" +multiplicity = "μ_sum" +ref = "lt:c:range_n" -[[assumptions]] -desc = "`IS_BIT`" -ref = "lt:a:range_signed" +[[constraints.range]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "d", "i"]] +iter = ["i", 0, 3] +multiplicity = "μ_sum" +ref = "lt:c:range_d" -# Constraints +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["signed"] +ref = "lt:c:range_signed" [[constraint_groups]] name = "sign_equality" @@ -214,9 +223,9 @@ name = "abs_diff" [[constraints.abs_diff]] kind = "interaction" -tag = "LT" -input = ["abs_r", "abs_d", 0] -output = ["not", "div_by_zero"] +tag = "ALU" +input = ["abs_r", "abs_d", ["opsel", "LT"]] +output = ["arr", ["not", "div_by_zero"], 0] multiplicity = "μ_sum" ref ="dvrm:c:abs_r_lt_abs_d" @@ -304,16 +313,16 @@ name = "equality" [[constraints.equality]] kind = "interaction" -tag = "MUL" -input = ["d", "signed", "q", "sign_q", 0] +tag = "ALU" +input = [["cast", "d", "DWordWL"], ["cast", "q", "DWordWL"], ["+", ["opsel", "MUL"], ["*", 32, "signed"], ["*", 64, "sign_q"]]] output = ["cast", "n_sub_r", "DWordWL"] multiplicity = "μ_sum" ref = "dvrm:c:mul_lower" [[constraints.equality]] kind = "interaction" -tag = "MUL" -input = ["d", "signed", "q", "sign_q", 1] +tag = "ALU" +input = [["cast", "d", "DWordWL"], ["cast", "q", "DWordWL"], ["+", ["opsel", "MUL"], ["*", 32, "signed"], ["*", 64, "sign_q"], 128]] output = ["cast", "extension_n_sub_r", "DWordWL"] multiplicity = "μ_sum" ref = "dvrm:c:mul_upper" @@ -375,14 +384,14 @@ desc = "Each row contributes the following to the LogUp sum" [[constraints.output]] kind = "interaction" -tag = "DVRM" -input = ["n", "d", "signed", 0] +tag = "ALU" +input = [["cast", "n", "DWordWL"], ["cast", "d", "DWordWL"], ["+", ["opsel", "DIVREM"], ["*", 32, "signed"]]] output = ["cast", "q", "DWordWL"] multiplicity = ["-", "μ_q"] [[constraints.output]] kind = "interaction" -tag = "DVRM" -input = ["n", "d", "signed", 1] +tag = "ALU" +input = [["cast", "n", "DWordWL"], ["cast", "d", "DWordWL"], ["+", ["opsel", "DIVREM"], ["*", 32, "signed"], 128]] output = ["cast", "r", "DWordWL"] multiplicity = ["-", "μ_r"] diff --git a/spec/src/keccak_round.toml b/spec/src/keccak_round.toml index 59daba923..6ee05e29a 100644 --- a/spec/src/keccak_round.toml +++ b/spec/src/keccak_round.toml @@ -191,8 +191,8 @@ name = "theta" [[constraints.theta]] kind = "interaction" -tag = "XOR_BYTE" -input = [["idx", ["idx", ["idx", "start", "x"], 0], "z"], ["idx", ["idx", ["idx", "start", "x"], 1], "z"]] +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "start", "x"], 0], "z"], ["idx", ["idx", ["idx", "start", "x"], 1], "z"]] output = ["idx", ["idx", ["idx", "Cxz", "x"], 0], "z"] iters = [["x", 0, 4], ["z", 0, 7]] multiplicity = "μ" @@ -200,8 +200,8 @@ ref = "keccak:c:theta_cxz_start" [[constraints.theta]] kind = "interaction" -tag = "XOR_BYTE" -input = [["idx", ["idx", ["idx", "Cxz", "x"], ["-", "y", 2]], "z"], ["idx", ["idx", ["idx", "start", "x"], "y"], "z"]] +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "Cxz", "x"], ["-", "y", 2]], "z"], ["idx", ["idx", ["idx", "start", "x"], "y"], "z"]] output = ["idx", ["idx", ["idx", "Cxz", "x"], ["-", "y", 1]], "z"] iters = [["x", 0, 4], ["y", 2, 4], ["z", 0, 7]] multiplicity = "μ" @@ -237,8 +237,8 @@ iters = [["x", 0, 4], ["z", 0, 3]] [[constraints.theta]] kind = "interaction" -tag = "XOR_BYTE" -input = [["idx", ["idx", ["idx", "Cxz", ["mod", ["-", "x", 1], 5]], 3], "z"], ["idx", ["idx", "rotated_Cxz", ["mod", ["+", "x", 1], 5]], "z"]] +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "Cxz", ["mod", ["-", "x", 1], 5]], 3], "z"], ["idx", ["idx", "rotated_Cxz", ["mod", ["+", "x", 1], 5]], "z"]] output = ["idx", ["idx", "Dxz", "x"], "z"] iters = [["x", 0, 4], ["z", 0, 7]] multiplicity = "μ" @@ -246,8 +246,8 @@ ref = "keccak:c:Dxz" [[constraints.theta]] kind = "interaction" -tag = "XOR_BYTE" -input = [["idx", ["idx", ["idx", "start", "x"], "y"], "z"], ["idx", ["idx", "Dxz", "x"], "z"]] +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "start", "x"], "y"], "z"], ["idx", ["idx", "Dxz", "x"], "z"]] output = ["idx", ["idx", ["idx", "theta", "x"], "y"], "z"] iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] multiplicity = "μ" @@ -289,16 +289,16 @@ name = "chi" [[constraints.chi]] kind = "interaction" -tag = "AND_BYTE" -input = [["-", 255, ["idx", ["idx", ["idx", "pi", ["mod", ["+", "x", 1], 5]], "y"], "z"]], ["idx",["idx",["idx", "pi", ["mod", ["+", "x", 2], 5]], "y"], "z"]] +tag = "BYTE_ALU" +input = [["opsel", "AND"], ["-", 255, ["idx", ["idx", ["idx", "pi", ["mod", ["+", "x", 1], 5]], "y"], "z"]], ["idx",["idx",["idx", "pi", ["mod", ["+", "x", 2], 5]], "y"], "z"]] output = ["idx", ["idx", ["idx", "chi_ANDs", "x"], "y"], "z"] iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] multiplicity = "μ" [[constraints.chi]] kind = "interaction" -tag = "XOR_BYTE" -input = [["idx", ["idx", ["idx", "pi", "x"], "y"], "z"], ["idx",["idx",["idx", "chi_ANDs", "x"], "y"], "z"]] +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "pi", "x"], "y"], "z"], ["idx",["idx",["idx", "chi_ANDs", "x"], "y"], "z"]] output = ["idx", ["idx", ["idx", "chi", "x"], "y"], "z"] iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] multiplicity = "μ" @@ -308,8 +308,8 @@ name = "iota" [[constraints.iota]] kind = "interaction" -tag = "XOR_BYTE" -input = [["idx", ["idx", ["idx", "chi", 0], 0], "z"], ["idx","rc","z"]] +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "chi", 0], 0], "z"], ["idx","rc","z"]] output = ["idx", "iota", "z"] iter = ["z", 0, 7] multiplicity = "μ" diff --git a/spec/src/load.toml b/spec/src/load.toml index 587ecd3d7..e439eb147 100644 --- a/spec/src/load.toml +++ b/spec/src/load.toml @@ -4,7 +4,7 @@ name = "LOAD" [[variables.input]] name = "base_address" -type = "DWordWL" +type = "DWordHL" desc = "The base address to read/write from/to, gets offset by $[0, 7]$, depending on how big the access is" pad = 0 @@ -72,31 +72,41 @@ pad = 0 [[assumptions]] -desc = "`IS_WORD[base_address[i]]`" -iter = ["i", 0, 1] +desc = "`IS_HALF[base_address[i]]`" +iter = ["i", 0, 3] [[assumptions]] -desc = "`IS_BIT`" +desc = "`IS_WORD[timestamp[i]]`" +iter = ["i", 0, 1] -[[assumptions]] -desc = "`IS_BIT`" -[[assumptions]] -desc = "`IS_BIT`" +[[constraint_groups]] +name = "all" -[[assumptions]] -desc = "`IS_BIT`" +[[constraints.all]] +kind = "template" +tag = "IS_BIT" +input = ["signed"] -[[assumptions]] -desc = "`IS_BIT`" +[[constraints.all]] +kind = "template" +tag = "IS_BIT" +input = ["read2"] -[[assumptions]] -desc = "`IS_WORD[timestamp[i]]`" -iter = ["i", 0, 1] +[[constraints.all]] +kind = "template" +tag = "IS_BIT" +input = ["read4"] +[[constraints.all]] +kind = "template" +tag = "IS_BIT" +input = ["read8"] -[[constraint_groups]] -name = "all" +[[constraints.all]] +kind = "template" +tag = "IS_BIT" +input = [["+", "read2", "read4", "read8"]] [[constraints.all]] kind = "arith" @@ -106,7 +116,7 @@ poly = ["*", ["+", "read2", "read4", "read8"], ["not", "μ"]] [[constraints.all]] kind = "interaction" tag = "MEMW" -input = [0, "base_address", ["cast", "res", ["BaseField", 8]], "timestamp", "read2", "read4", "read8"] +input = [0, ["cast", "base_address", "DWordWL"], ["cast", "res", ["BaseField", 8]], "timestamp", "read2", "read4", "read8"] output = "res" multiplicity = "μ" @@ -155,7 +165,7 @@ name = "output" [[constraints.output]] kind = "interaction" -tag = "LOAD" -input = ["base_address", "timestamp", "read2", "read4", "read8", "signed"] +tag = "MEMORY" +input = ["timestamp", "base_address", ["cast", 0, "DWordWL"], ["+", ["*", 2, "signed"], ["*", 4, "read2"], ["*", 8, "read4"], ["*", 16, "read8"]]] output = ["cast", "res", "DWordWL"] multiplicity = ["-", "μ"] diff --git a/spec/src/lt.toml b/spec/src/lt.toml index 70d25c919..2cb45d2f0 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -85,15 +85,17 @@ ref = "lt:a:range_lhs" desc = "`IS_WORD[rhs[0]]`" ref = "lt:a:range_rhs" -[[assumptions]] -desc = "`IS_BIT`" -ref = "lt:a:range_signed" - [[constraint_groups]] name = "defs" desc = "Enforce that variables have been correctly computed" +[[constraints.defs]] +kind = "template" +tag = "IS_BIT" +input = ["signed"] +ref = "lt:c:range_signed" + [[constraints.defs]] kind = "interaction" tag = "MSB16" @@ -157,7 +159,7 @@ desc = "Each row contributes the following to the LogUp sum" [[constraints.output]] kind = "interaction" -tag = "LT" -input = [["cast", "lhs", "DWordWL"], ["cast", "rhs", "DWordWL"], "signed"] -output = "lt" +tag = "ALU" +input = [["cast", "lhs", "DWordWL"], ["cast", "rhs", "DWordWL"], ["+", ["opsel", "LT"], ["*", 32, "signed"]]] +output = ["arr", "lt", 0] multiplicity = ["-", "μ"] diff --git a/spec/src/memw.toml b/spec/src/memw.toml index 1cc0dd3c2..330383e41 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -162,31 +162,31 @@ iter = ["i", 0, 6] [[constraints.consistency]] kind = "interaction" -tag = "LT" -input = [["idx", "old_timestamp", 0], "timestamp", 0] -output = 1 +tag = "ALU" +input = [["idx", "old_timestamp", 0], "timestamp", ["opsel", "LT"]] +output = ["arr", 1, 0] multiplicity = "μ_sum" [[constraints.consistency]] kind = "interaction" -tag = "LT" -input = [["idx", "old_timestamp", 1], "timestamp", 0] -output = 1 +tag = "ALU" +input = [["idx", "old_timestamp", 1], "timestamp", ["opsel", "LT"]] +output = ["arr", 1, 0] multiplicity = "w2" [[constraints.consistency]] kind = "interaction" -tag = "LT" -input = [["idx", "old_timestamp", "i"], "timestamp", 0] -output = 1 +tag = "ALU" +input = [["idx", "old_timestamp", "i"], "timestamp", ["opsel", "LT"]] +output = ["arr", 1, 0] iter = ["i", 2, 3] multiplicity = "w4" [[constraints.consistency]] kind = "interaction" -tag = "LT" -input = [["idx", "old_timestamp", "i"], "timestamp", 0] -output = 1 +tag = "ALU" +input = [["idx", "old_timestamp", "i"], "timestamp", ["opsel", "LT"]] +output = ["arr", 1, 0] iter = ["i", 4, 7] multiplicity = "write8" diff --git a/spec/src/memw_aligned.toml b/spec/src/memw_aligned.toml index 93a636aba..ee63398bf 100644 --- a/spec/src/memw_aligned.toml +++ b/spec/src/memw_aligned.toml @@ -150,9 +150,9 @@ poly = ["*", "w2", ["not", "μ_sum"]] [[constraints.consistency]] kind = "interaction" -tag = "LT" -input = ["old_timestamp", "timestamp", 0] -output = 1 +tag = "ALU" +input = ["old_timestamp", "timestamp", ["opsel", "LT"]] +output = ["arr", 1, 0] multiplicity = "μ_sum" [[constraint_groups]] diff --git a/spec/src/mul.toml b/spec/src/mul.toml index a798c682d..fee7a8e34 100644 --- a/spec/src/mul.toml +++ b/spec/src/mul.toml @@ -121,22 +121,26 @@ type = "BaseField" desc = "" pad = 0 -# Assumptions - -[[assumptions]] -desc = "`IS_HALF[lhs[i]]`" -iter = ["i", 0, 3] - -[[assumptions]] -desc = "`IS_HALF[rhs[i]]`" -iter = ["i", 0, 3] -ref = "mul:a:rhs" - # Constraints [[constraint_groups]] name = "def" +[[constraints.def]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "lhs", "i"]] +multiplicity = "μ_sum" +iter = ["i", 0, 3] + +[[constraints.def]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "rhs", "i"]] +multiplicity = "μ_sum" +iter = ["i", 0, 3] +ref = "mul:c:rhs" + [[constraints.def]] kind = "template" tag = "SIGN" @@ -191,16 +195,16 @@ name = "lookup" [[constraints.lookup]] kind = "interaction" -tag = "MUL" -input = ["lhs", "lhs_signed", "rhs", "rhs_signed", 0] +tag = "ALU" +input = [["cast", "lhs", "DWordWL"], ["cast", "rhs", "DWordWL"], ["+", ["opsel", "MUL"], ["*", 32, "lhs_signed"], ["*", 64, "rhs_signed"]]] output = ["cast", "lo", "DWordWL"] multiplicity = ["-", "μ_lo"] ref = "mul:c:lookup_lo" [[constraints.lookup]] kind = "interaction" -tag = "MUL" -input = ["lhs", "lhs_signed", "rhs", "rhs_signed", 1] +tag = "ALU" +input = [["cast", "lhs", "DWordWL"], ["cast", "rhs", "DWordWL"], ["+", ["opsel", "MUL"], ["*", 32, "lhs_signed"], ["*", 64, "rhs_signed"], 128]] output = ["cast", "hi", "DWordWL"] multiplicity = ["-", "μ_hi"] ref = "mul:c:lookup_hi" diff --git a/spec/src/rotxor.toml b/spec/src/rotxor.toml index 730e9bda5..822b1d2f2 100644 --- a/spec/src/rotxor.toml +++ b/spec/src/rotxor.toml @@ -161,16 +161,16 @@ name = "xor" [[constraints.xor]] kind = "interaction" -tag = "XOR_BYTE" -input = [["idx", "a0", "i"], ["idx", "a1", "i"]] +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", "a0", "i"], ["idx", "a1", "i"]] output = ["idx", "a01", "i"] multiplicity = "μ" iter = ["i", 0, 3] [[constraints.xor]] kind = "interaction" -tag = "XOR_BYTE" -input = [["idx", "a01", "i"], ["idx", "a2", "i"]] +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", "a01", "i"], ["idx", "a2", "i"]] output = ["idx", "out", "i"] multiplicity = "μ" iter = ["i", 0, 3] diff --git a/spec/src/sha256round.toml b/spec/src/sha256round.toml index 2469b560c..45da4d452 100644 --- a/spec/src/sha256round.toml +++ b/spec/src/sha256round.toml @@ -177,40 +177,40 @@ name = "value" [[constraints.value]] kind = "interaction" -tag = "AND_BYTE" -input = [["idx", "a", "i"], ["idx", "b", "i"]] +tag = "BYTE_ALU" +input = [["opsel", "AND"], ["idx", "a", "i"], ["idx", "b", "i"]] output = ["idx", "a_and_b", "i"] multiplicity = "μ" iter = ["i", 0, 3] [[constraints.value]] kind = "interaction" -tag = "XOR_BYTE" -input = [["idx", "a", "i"], ["idx", "b", "i"]] +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", "a", "i"], ["idx", "b", "i"]] output = ["idx", "a_xor_b", "i"] multiplicity = "μ" iter = ["i", 0, 3] [[constraints.value]] kind = "interaction" -tag = "AND_BYTE" -input = [["idx", "c", "i"], ["idx", "a_xor_b", "i"]] +tag = "BYTE_ALU" +input = [["opsel", "AND"], ["idx", "c", "i"], ["idx", "a_xor_b", "i"]] output = ["idx", "c_and_a_xor_b", "i"] multiplicity = "μ" iter = ["i", 0, 3] [[constraints.value]] kind = "interaction" -tag = "AND_BYTE" -input = [["idx", "e", "i"], ["idx", "f", "i"]] +tag = "BYTE_ALU" +input = [["opsel", "AND"], ["idx", "e", "i"], ["idx", "f", "i"]] output = ["idx", "e_and_f", "i"] multiplicity = "μ" iter = ["i", 0, 3] [[constraints.value]] kind = "interaction" -tag = "AND_BYTE" -input = [["-", 255, ["idx", "e", "i"]], ["idx", "g", "i"]] +tag = "BYTE_ALU" +input = [["opsel", "AND"], ["-", 255, ["idx", "e", "i"]], ["idx", "g", "i"]] output = ["idx", "not_e_and_g", "i"] multiplicity = "μ" iter = ["i", 0, 3] diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 18c03ecad..47dfbec59 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -10,7 +10,7 @@ pad = 0 [[variables.input]] name = "shift" -type = "Byte" +type = "DWordWHBB" desc = "Number of bits to shift `in` by." pad = 0 @@ -138,31 +138,54 @@ desc = "" pad = 0 - # Assumptions [[assumptions]] -desc = "`IS_HALF[in[i]]`" +desc = "`IS_WORD[shift[3]]`" + +# Constraints + +[[constraint_groups]] +name = "input" + +[[constraints.input]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "in", "i"]] iter = ["i", 0, 3] -ref = "shift:a:range_in" +multiplicity = "μ" +ref = "shift:c:range_in" -[[assumptions]] -desc = "`IS_BYTE`" -ref = "shift:a:range_shift" +[[constraints.input]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "shift", 2]] +multiplicity = "μ" -[[assumptions]] -desc = "`IS_BIT`" -ref = "shift:a:direction" +[[constraints.input]] +kind = "template" +tag = "IS_BYTE" +input = [["idx", "shift", "i"]] +iter = ["i", 0, 1] +ref = "shift:c:range_shift" -[[assumptions]] -desc = "`IS_BIT`" -ref = "shift:a:signed" +[[constraints.input]] +kind = "template" +tag = "IS_BIT" +input = ["direction"] +ref = "shift:c:direction" -[[assumptions]] -desc = "`IS_BIT`" -ref = "shift:a:word_instr" +[[constraints.input]] +kind = "template" +tag = "IS_BIT" +input = ["signed"] +ref = "shift:c:signed" -# Constraints +[[constraints.input]] +kind = "template" +tag = "IS_BIT" +input = ["word_instr"] +ref = "shift:c:word_instr" [[constraint_groups]] name = "left_flag" @@ -192,16 +215,16 @@ name = "bit_shift" [[constraints.bit_shift]] kind = "interaction" -tag = "AND_BYTE" -input = ["shift", 0x0F] +tag = "BYTE_ALU" +input = [["opsel", "AND"], ["idx", "shift", 0], 0x0F] output = "bit_shift" ref = "shift:c:bit_shift_if_left" multiplicity = "left" [[constraints.bit_shift]] kind = "interaction" -tag = "AND_BYTE" -input = [["-", ["^", 2, 8], ["*", 16, "zbs"], "shift"], 0x0F] +tag = "BYTE_ALU" +input = [["opsel", "AND"], ["-", ["^", 2, 8], ["*", 16, "zbs"], ["idx", "shift", 0]], 0x0F] output = "bit_shift" ref = "shift:c:bit_shift_if_right" multiplicity = "right" @@ -268,8 +291,8 @@ ref = "shift:c:limb_shift_is_bit" [[constraints.limb_shifting]] kind = "interaction" -tag = "AND_BYTE" -input = ["shift", ["-", 0x30, ["*", 0x20, "word_instr"]]] +tag = "BYTE_ALU" +input = [["opsel", "AND"], ["idx", "shift", 0], ["-", 0x30, ["*", 0x20, "word_instr"]]] output = ["+", ["-", 1, ["idx", "limb_shift", 0]], ["*", 15, ["idx", "limb_shift", 1]], ["*", 31, ["idx", "limb_shift", 2]], ["*", 47, ["idx", "limb_shift", 3]]] ref = "shift:c:limb_shift_lookup" multiplicity = "μ" @@ -289,8 +312,8 @@ name = "lookups" [[constraints.lookups]] kind = "interaction" -tag = "SHIFT" -input = ["in", "shift", "direction", "signed", "word_instr"] +tag = "ALU" +input = [["cast", "in", "DWordWL"], ["cast", "shift", "DWordWL"], ["+", ["opsel", "SHIFT"], "word_instr", ["*", 32, "signed"], ["*", 64, "direction"]]] output = "out" multiplicity = ["-", "μ"] ref = "shift:c:lookup" diff --git a/spec/tooling/chip.py b/spec/tooling/chip.py index 7f7ecca81..44cbbed83 100644 --- a/spec/tooling/chip.py +++ b/spec/tooling/chip.py @@ -92,6 +92,8 @@ def constant_fits(cst: int, target: Type) -> bool: | DummyExpr ) +OPSEL = ["AND", "OR", "XOR", "EQ", "LT", "SHIFT", "SHIFTW", "MUL", "DIVREM"] + @dataclass class Environment: @@ -351,6 +353,11 @@ def build_expr(config: Optional["Config"], data: object) -> Expr: x.isidentifier(), f"Invalid identifier name for variable {x!r}" ) return VarExpr(x) + case ["opsel", str(x)]: + if x not in OPSEL: + reporter.error(f"Unknown operation selector: {x!r}") + return LitExpr(0) + return LitExpr(OPSEL.index(x)) case ["arr", *elems]: return ArrExpr([build_expr(config, e) for e in elems]) case ["idx", x, y]: From dd81c6bcd9d1f8f9152d7f01809590cb8f601000 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 26 May 2026 17:38:28 +0200 Subject: [PATCH 05/25] Fix decode for MEMORY signed flag --- spec/decode.typ | 6 +++--- spec/src/decode_uncompressed.toml | 7 ++++++- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/spec/decode.typ b/spec/decode.typ index 6b6c51454..33c85c968 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -146,9 +146,9 @@ Further clarification is provided in the notes following the table. ([`BGE[U] rs1, rs2, imm`], [`LT`], [], [#sym.not`[U]`], [`invert`], [#ref_note()]), // LOAD ([`LD rd, rs1, imm`], [`ADD`], [], [], [`MEMORY`, `mem_8B`], []), - ([`LW[U] rd, rs1, imm`], [`ADD`], [], [#sym.not`[U]`], [`MEMORY`, `mem_4B`], [#ref_note()]), - ([`LH[U] rd, rs1, imm`], [`ADD`], [], [#sym.not`[U]`], [`MEMORY`, `mem_2B`], [#ref_note()]), - ([`LB[U] rd, rs1, imm`], [`ADD`], [], [#sym.not`[U]`], [`MEMORY`, ], [#ref_note()]), + ([`LW[U] rd, rs1, imm`], [`ADD`], [], [], [`MEMORY`, `mem_signed := `#sym.not`[U]`, `mem_4B`], [#ref_note()]), + ([`LH[U] rd, rs1, imm`], [`ADD`], [], [], [`MEMORY`, `mem_signed := `#sym.not`[U]`, `mem_2B`], [#ref_note()]), + ([`LB[U] rd, rs1, imm`], [`ADD`], [], [], [`MEMORY`, `mem_signed := `#sym.not`[U]`], [#ref_note()]), // STORE ([`SD rs1, rs2, imm`], [`ADD`], [], [], [`MEMORY`, `memory_op`, `mem_8B`], []), ([`SW rs1, rs2, imm`], [`ADD`], [], [], [`MEMORY`, `memory_op`, `mem_4B`], []), diff --git a/spec/src/decode_uncompressed.toml b/spec/src/decode_uncompressed.toml index ce31573b5..dc6891f92 100644 --- a/spec/src/decode_uncompressed.toml +++ b/spec/src/decode_uncompressed.toml @@ -125,6 +125,11 @@ name = "mem_8B" type = "Bit" desc = "whether the memory access (read or write) touches exactly $8$ bytes." +[[variables.auxiliary]] +name = "mem_signed" +type = "Bit" +desc = "Whether the memory operation is a signed one, this is distinct from `signed` to enable the `JALR` flag to alias `mem_flags`" + [[variables.auxiliary]] name = "JALR" type = "Bit" @@ -148,7 +153,7 @@ desc = "The combined memory flags (or JALR when BRANCHing)" def = ["+", "JALR", "memory_op", - ["*", 2, "signed"], + ["*", 2, "mem_signed"], ["*", 4, "mem_2B"], ["*", 8, "mem_4B"], ["*", 16, "mem_8B"] From cc50d006d1c204e1ff93776d44780213c345f857 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 26 May 2026 17:38:44 +0200 Subject: [PATCH 06/25] Add input range check to SHIFTs typ --- spec/shift.typ | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/spec/shift.typ b/spec/shift.typ index c464d5d55..8f7af6a9f 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -109,7 +109,10 @@ Copies of this variable are used for any full limbs shifted in when $#`right` = Moreover, `X[4]` contains a copy of `extension` shifted over by the right number of bits, to allow the construction of $#`in >>> shift` mod 16$ as the appropriate intermediate. = Constraints -First, we constrain `bit_shift` based on whether we are left or right-shifting. +First, we range check our inputs appropriately. +#render_constraint_table(chip, config, groups: "input") + +Then, we constrain `bit_shift` based on whether we are left or right-shifting. @shift:c:zbs makes sure `zbs` is set to `1` if and only if `bit_shift = 0`. This flag is used to indicate the special case that $#`right` = 1$ and $#`shift` = 0 mod 16$. #render_constraint_table(chip, config, groups: "bit_shift") From 720512c6b0aad9cf6fe74093613ee9f7e0f5370b Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 26 May 2026 17:57:30 +0200 Subject: [PATCH 07/25] MEMORY signature HL -> WL --- spec/src/cpu.toml | 2 +- spec/src/load.toml | 8 ++++---- spec/src/signatures.toml | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index e32c45da6..020402e17 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -428,7 +428,7 @@ multiplicity = "write_register" [[constraints.mem]] kind = "interaction" tag = "MEMORY" -input = ["timestamp", "res", "rv2", "mem_flags"] +input = ["timestamp", ["cast", "res", "DWordWL"], "rv2", "mem_flags"] output = "rvd" multiplicity = "MEMORY" diff --git a/spec/src/load.toml b/spec/src/load.toml index e439eb147..88e6392a6 100644 --- a/spec/src/load.toml +++ b/spec/src/load.toml @@ -4,7 +4,7 @@ name = "LOAD" [[variables.input]] name = "base_address" -type = "DWordHL" +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 @@ -72,8 +72,8 @@ pad = 0 [[assumptions]] -desc = "`IS_HALF[base_address[i]]`" -iter = ["i", 0, 3] +desc = "`IS_WORD[base_address[i]]`" +iter = ["i", 0, 1] [[assumptions]] desc = "`IS_WORD[timestamp[i]]`" @@ -116,7 +116,7 @@ poly = ["*", ["+", "read2", "read4", "read8"], ["not", "μ"]] [[constraints.all]] kind = "interaction" tag = "MEMW" -input = [0, ["cast", "base_address", "DWordWL"], ["cast", "res", ["BaseField", 8]], "timestamp", "read2", "read4", "read8"] +input = [0, "base_address", ["cast", "res", ["BaseField", 8]], "timestamp", "read2", "read4", "read8"] output = "res" multiplicity = "μ" diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index babcc1650..a2d70a51d 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -66,7 +66,7 @@ output = "DWordWL" [[signatures]] tag = "MEMORY" kind = "interaction" -input = ["DWordWL", "DWordHL", "DWordWL", "Byte"] +input = ["DWordWL", "DWordWL", "DWordWL", "Byte"] output = "DWordWL" # BRANCH[next_pc; pc, offset, register, JALR] From ce1a06af571608cc46be17af39e465cb3cf11788 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 26 May 2026 18:03:43 +0200 Subject: [PATCH 08/25] Clarify SHIFTW decoding --- spec/decode.typ | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/decode.typ b/spec/decode.typ index 33c85c968..e2098b1eb 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -114,7 +114,7 @@ Further clarification is provided in the notes following the table. ([`ANDI rd, rs1, imm`], [`AND`], [], [], [], []), ([`ORI rd, rs1, imm`], [`OR`], [], [], [], []), ([`XORI rd, rs1, imm`], [`XOR`], [], [], [], []), - ([`SLLI[W] rd, rs1, imm`], [`SHIFT[W]`], [`[W]`], [], [], []), + ([`SLLI[W] rd, rs1, imm`], [`SHIFT[W]`], [`[W]`], [], [], [#ref_note()]), ([`SRLI[W] rd, rs1, imm`], [`SHIFT[W]`], [`[W]`], [], [`invert`], [#ref_note()]), ([`SRAI[W] rd, rs1, imm`], [`SHIFT[W]`], [`[W]`], [1], [`invert`], [#ref_note()]), // OP @@ -185,7 +185,7 @@ We note the following about the above decoding table: enum.item( referenceable_note( "note_word_instr", - [`word_instr`: `[W]` indicates that $#`word_instr` = 1$ for the `W`-variant of the operation, and $0$ for the non-`W`-variant.] + [`word_instr`: `[W]` indicates that $#`word_instr` = 1$ for the `W`-variant of the operation, and $0$ for the non-`W`-variant. Similarly, `SHIFT[W]` indicates the `SHIFTW` operation for the `W`-variant, and `SHIFT` otherwise.] ) ), enum.item( From 51585133520b8293a13a030c9508e80caf84fd5f Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Wed, 27 May 2026 13:58:49 +0200 Subject: [PATCH 09/25] Further updates and new chips for the new CPU --- spec/book.typ | 12 +- spec/bytewise.typ | 38 ++++ spec/cpu32.typ | 56 ++++++ spec/eq.typ | 37 ++++ spec/lt.typ | 5 + spec/src/bytewise.toml | 49 +++++ spec/src/cpu.toml | 1 - spec/src/cpu32.toml | 393 +++++++++++++++++++++++++++++++++++++++++ spec/src/eq.toml | 93 ++++++++++ spec/src/load.toml | 2 +- spec/src/lt.toml | 59 +++++-- spec/src/store.toml | 116 ++++++++++++ spec/store.typ | 47 +++++ 13 files changed, 884 insertions(+), 24 deletions(-) create mode 100644 spec/bytewise.typ create mode 100644 spec/cpu32.typ create mode 100644 spec/eq.typ create mode 100644 spec/src/bytewise.toml create mode 100644 spec/src/cpu32.toml create mode 100644 spec/src/eq.toml create mode 100644 spec/src/store.toml create mode 100644 spec/store.typ diff --git a/spec/book.typ b/spec/book.typ index f4e95e493..8bf8612af 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -23,21 +23,25 @@ ("add.typ", [`ADD`/`SUB` template], ), ("neg.typ", [`NEG` template], ), )), - ("MEMORY", ( - ("memw.typ", [`MEMW` chip], ), - )), ("CPU", ( ("decode.typ", [`DECODE` table], ), ("cpu.typ", [`CPU` chip], ), + ("cpu32.typ", [`CPU32` chip], ), )), ("ALU", ( ("shift.typ", [`SHIFT` chip], ), ("branch.typ", [`BRANCH` chip], ), ("lt.typ", [`LT` chip], ), + ("eq.typ", [`EQ` chip], ), ("mul.typ", [`MUL` chip], ), ("dvrm.typ", [`DVRM` chip], ), - ("load.typ", [`LOAD` chip], ), ("bitwise.typ", [`BITWISE` chips], ), + ("bytewise.typ", [`BYTEWISE` chip], ) + )), + ("MEMORY", ( + ("memw.typ", [`MEMW` chip], ), + ("load.typ", [`LOAD` chip], ), + ("store.typ", [`STORE` chip], ), )), ("ECALLS", ( ("about_ecalls.typ", [About `ECALL`], ), diff --git a/spec/bytewise.typ b/spec/bytewise.typ new file mode 100644 index 000000000..452e4fdbc --- /dev/null +++ b/spec/bytewise.typ @@ -0,0 +1,38 @@ +#import "/book.typ": book-page, rj +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_assumptions, + render_chip_variable_table, + total_nr_variables, + total_nr_instantiated_columns, + compute_nr_interactions, + render_constraint_table, + render_chip_padding_table, +) + +#let config = load_config() +#let chip = load_chip("src/bytewise.toml", config) + +#show: book-page(chip.name) +#let bytewise = raw(chip.name) + +The #bytewise chip is an ALU chip that decomposes the input `DWordWL` values into bytes and +performs a `BITWISE` operation pairwise (AND, OR, XOR). +The `BITWISE` lookup inherently performs a range check, so no further constraints are necessary. + += 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 #bytewise chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): +#render_chip_variable_table(chip, config) + += Constraints + +#render_constraint_table(chip, config) + += Padding + +The chip can be padded with the following values: +#render_chip_padding_table(chip, config) diff --git a/spec/cpu32.typ b/spec/cpu32.typ new file mode 100644 index 000000000..6114ed5e7 --- /dev/null +++ b/spec/cpu32.typ @@ -0,0 +1,56 @@ +#import "/book.typ": book-page, rj +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_assumptions, + render_chip_variable_table, + render_chip_padding_table, + render_constraint_table, + compute_nr_interactions, + total_nr_instantiated_columns, + total_nr_variables, +) + +#let config = load_config() +#let chip = load_chip("src/cpu32.toml", config) + +#show: book-page(chip.name) +#let cpu32 = raw(chip.name) + +The #cpu32 chip is used to delegate the 32-bit instructions of the RV64I instruction set +from the main CPU table (@cpu). +All 32-bit instructions are ALU-only instructions, so the BRANCH, MEMORY and ECALL paths need no elaboration. +The timestamp and PC have already been read by the CPU table at this point, and need no further checking, +the PC for the next instruction will also already be handled by CPU. + +The structure follows the regular ALU path, with some extra variables and constraints to contain the required sign extensions. + += 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 #cpu32 chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): +#render_chip_variable_table(chip, config) + += Assumptions + +#render_chip_assumptions(chip, config) + += Constraints + +Most constraints correspond to those already present in the CPU, and we present them here first, +including some updates to the range checking corresponding to the differing types. + +#render_constraint_table(chip, config, groups: ("decode", "range", "alu", "mem")) + +Then, we have the constraints corresponding to the sign-extension and definition of `arg1`, `arg2` and `rd`. +This includes a step where we extract the `signed` bit from the `alu_flags`, as this determines +whether to sign extend the inputs or not. + +#render_constraint_table(chip, config, groups: "ext") + += Padding + +The table can be padded with the following values: +#render_chip_padding_table(chip, config) + diff --git a/spec/eq.typ b/spec/eq.typ new file mode 100644 index 000000000..f6d63fea4 --- /dev/null +++ b/spec/eq.typ @@ -0,0 +1,37 @@ +#import "/book.typ": book-page, rj +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_assumptions, + render_chip_variable_table, + total_nr_variables, + total_nr_instantiated_columns, + compute_nr_interactions, + render_constraint_table, + render_chip_padding_table, +) + +#let config = load_config() +#let chip = load_chip("src/eq.toml", config) + +#show: book-page(chip.name) +#let eq = raw(chip.name) + +The #eq chip is an ALU chip that compares two values and outputs a bit indicating whether they are equal or not. +It optionally inverts the result if the `invert` flag is set. + += 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 #eq chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): +#render_chip_variable_table(chip, config) + += Constraints + +#render_constraint_table(chip, config) + += Padding + +The chip can be padded with the following values: +#render_chip_padding_table(chip, config) diff --git a/spec/lt.typ b/spec/lt.typ index 2e0ac8be4..126e78269 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -17,6 +17,7 @@ #let lt = raw(chip.name) The #lt chip constrains an indicator bit for the less-than relation, signed or unsigned. +If the `invert` flag is set, it inverts the result. = Variables #let nr_variables = total_nr_variables(chip) @@ -90,3 +91,7 @@ The chip contributes the following to the lookup argument. The table can be padded to the next power of two with the following value assignments: #render_chip_padding_table(chip, config) + += Potential optimizations + +- Split the chip into a signed and an unsigned chip, making the unsigned version cheaper. diff --git a/spec/src/bytewise.toml b/spec/src/bytewise.toml new file mode 100644 index 000000000..b315a92b3 --- /dev/null +++ b/spec/src/bytewise.toml @@ -0,0 +1,49 @@ +name = "BYTEWISE" + +[[variables.input]] +name = "a" +type = "DWordBL" +desc = "The first input" +pad = 0 + +[[variables.input]] +name = "b" +type = "DWordBL" +desc = "The second input" +pad = 0 + +[[variables.input]] +name = "op" +type = "Byte" +desc = "The operation to perform" +pad = 0 + +[[variables.output]] +name = "res" +type = "DWordBL" +desc = "The result" +pad = 0 + +[[variables.multiplicity]] +name = "μ" +type = "BaseField" +desc = "" +pad = 0 + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "interaction" +tag = "BYTE_ALU" +input = ["op", ["idx", "a", "i"], ["idx", "b", "i"]] +output = ["idx", "res", "i"] +multiplicity = "μ" +iter = ["i", 0, 7] + +[[constraints.all]] +kind = "interaction" +tag = "ALU" +input = [["cast", "a", "DWordWL"], ["cast", "b", "DWordWL"], "op"] +output = ["cast", "res", "DWordWL"] +multiplicity = ["-", "μ"] diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 020402e17..99a37a46a 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -380,7 +380,6 @@ input = ["rv1", "arg2", "alu_flags"] output = ["cast", "res", "DWordWL"] multiplicity = "ALU" -# TODO: double check [[constraints.alu]] kind = "interaction" tag = "CPU32" diff --git a/spec/src/cpu32.toml b/spec/src/cpu32.toml new file mode 100644 index 000000000..584ddb10d --- /dev/null +++ b/spec/src/cpu32.toml @@ -0,0 +1,393 @@ +name = "CPU32" + +[[variables.input]] +name = "timestamp" +type = "DWordWL" +desc = "The timestamp for the CPU row" +pad = 0 + +[[variables.input]] +name = "pc" +type = "DWordWL" +desc = "The PC at which the instruction occurs" +pad = 0 + +[[variables.auxiliary]] +name = "rs1" +type = "Byte" +desc = "Source register 1" +pad = 0 + +[[variables.auxiliary]] +name = "read_register1" +type = "Bit" +desc = "Whether to read from `rs1` or not" +pad = 0 + +# Note in case we inline register accesses here: We don't need the upper word +[[variables.auxiliary]] +name = "rv1" +type = "DWordWHH" +desc = "The value in register `rs1`" +pad = 0 + +[[variables.auxiliary]] +name = "rv1_sign" +type = "Bit" +desc = "The sign bit of the lower word of `rv1`" +pad = 0 + +[[variables.auxiliary]] +name = "arg1" +type = "DWordWL" +desc = "The sign-extended version of `rv1`" +pad = 0 + +[[variables.auxiliary]] +name = "rs2" +type = "Byte" +desc = "Source register 2" +pad = 0 + +[[variables.auxiliary]] +name = "read_register2" +type = "Bit" +desc = "Whether to read from `rs2`" +pad = 0 + +[[variables.auxiliary]] +name = "rv2" +type = "DWordWHH" +desc = "The value in register `rs2`" +pad = 0 + +[[variables.auxiliary]] +name = "rv2_sign" +type = "Bit" +desc = "The sign bit of the lower word of `rv2`" +pad = 0 + +[[variables.auxiliary]] +name = "imm" +type = "DWordWL" +desc = "The fully sign-extended immediate to use" +pad = 0 + +[[variables.auxiliary]] +name = "arg2" +type = "DWordWL" +desc = "Either the sign-extended version of `rv2` or all of `imm`" +pad = 0 + +[[variables.auxiliary]] +name = "res" +type = "DWordHL" +desc = "The ALU result" +pad = 0 + +[[variables.auxiliary]] +name = "res_sign" +type = "Bit" +desc = "The sign bit of the lower word of `res`" +pad = 0 + +[[variables.auxiliary]] +name = "rd" +type = "Byte" +desc = "Destination register" +pad = 0 + +[[variables.auxiliary]] +name = "write_register" +type = "Bit" +desc = "Whether to write back to `rd`" +pad = 0 + +[[variables.auxiliary]] +name = "rvd" +type = "DWordWL" +desc = "The value to write back to `rd`, the sign-extended version of `res`" +pad = 0 + +[[variables.auxiliary]] +name = "ALU" +type = "Bit" +desc = "Whether the full ALU is active" +pad = 0 + +[[variables.auxiliary]] +name = "alu_flags" +type = "Byte" +desc = "The ALU operation + flags" +pad = 0 + +[[variables.auxiliary]] +name = "ADD" +type = "Bit" +desc = "Whether the full ALU is active" +pad = 0 + +[[variables.auxiliary]] +name = "SUB" +type = "Bit" +desc = "Whether the full ALU is active" +pad = 0 + +[[variables.auxiliary]] +name = "instruction_length" +type = "Byte" +desc = "The length of this instruction" +pad = 4 + +[[variables.auxiliary]] +name = "signed" +type = "Bit" +desc = "Whether the instruction is signed or not. Extracted from `alu_flags`, used to determine the extension for the inputs" +pad = 0 + +[[variables.virtual]] +name = "packed_decode" +type = "BaseField" +desc = "The packed representation of all flags and information from the decode table" +def = ["+", + ["*", ["^", 2, 0], "read_register1"], + ["*", ["^", 2, 1], "read_register2"], + ["*", ["^", 2, 2], "write_register"], + ["*", ["^", 2, 3], 1], # word_instr + ["*", ["^", 2, 4], "ALU"], + ["*", ["^", 2, 5], "ADD"], + ["*", ["^", 2, 6], "SUB"], + ["*", ["^", 2, 10], "rs1"], + ["*", ["^", 2, 18], "rs2"], + ["*", ["^", 2, 26], "rd"], + ["*", ["^", 2, 34], "instruction_length"], + ["*", ["^", 2, 42], "alu_flags"], +] + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" +pad = 0 + +[[assumptions]] +desc = "`IS_WORD[timestamp[i]]`" +iter = ["i", 0, 1] + +[[assumptions]] +desc = "`IS_WORD[pc[i]]`" +iter = ["i", 0, 1] + +[[assumptions]] +desc = "`read_register2 = 0` or `imm = 0`, enforced by decoding." + +[[constraint_groups]] +name = "decode" + +[[constraints.decode]] +kind = "interaction" +tag = "DECODE" +input = ["pc", "imm", "packed_decode"] +multiplicity = "μ" + +[[constraint_groups]] +name = "range" +prefix = "R" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["read_register1"] + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["read_register2"] + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["write_register"] + +[[constraints.range]] +kind = "template" +tag = "IS_BYTE" +input = ["instruction_length"] + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["ALU"] + +# Technically constraint by the BYTE_ALU in `ext`, but this is safer/cleaner +[[constraints.range]] +kind = "template" +tag = "IS_BYTE" +input = ["alu_flags"] + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["ADD"] + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["SUB"] + +[[constraints.range]] +kind = "template" +tag = "IS_BYTE" +input = ["rs1"] + +[[constraints.range]] +kind = "template" +tag = "IS_BYTE" +input = ["rs2"] + +[[constraints.range]] +kind = "template" +tag = "IS_BYTE" +input = ["rd"] + +[[constraints.range]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "rv1", "i"]] +multiplicity = "μ" +iter = ["i", 0, 1] + +[[constraints.range]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "rv2", "i"]] +multiplicity = "μ" +iter = ["i", 0, 1] + +[[constraints.range]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "res", "i"]] +multiplicity = "μ" +iter = ["i", 0, 3] + + +[[constraint_groups]] +name = "alu" +prefix = "A" + +[[constraints.alu]] +kind = "template" +tag = "ADD" +cond = "ADD" +input = ["arg1", "arg2"] +output = ["cast", "res", "DWordWL"] + +[[constraints.alu]] +kind = "template" +tag = "SUB" +cond = "SUB" +input = ["arg1", "arg2"] +output = ["cast", "res", "DWordWL"] + +[[constraints.alu]] +kind = "interaction" +tag = "ALU" +input = ["arg1", "arg2", "alu_flags"] +output = ["cast", "res", "DWordWL"] +multiplicity = "ALU" + +[[constraint_groups]] +name = "mem" +prefix = "M" + + +[[constraints.mem]] +kind = "interaction" +tag = "MEMW" +input = [1, ["*", ["cast", 2, "DWordWL"], "rs1"], ["arr", ["idx", "rv1", 0], ["idx", "rv1", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 0, "DWordWL"]], 1, 0, 0] +output = ["arr", ["idx", "rv1", 0], ["idx", "rv1", 1], 0, 0, 0, 0, 0, 0] +multiplicity = "read_register1" + +[[constraints.mem]] +kind = "arith" +constraint = "$#`!read_register1` => #`rv1[i]` = 0$" +poly = ["*", ["not", "read_register1"], ["idx", "rv1", "i"]] +iter = ["i", 0, 1] + +[[constraints.mem]] +kind = "interaction" +tag = "MEMW" +input = [1, ["*", ["cast", 2, "DWordWL"], "rs2"], ["arr", ["idx", "rv2", 0], ["idx", "rv2", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0] +output = ["arr", ["idx", "rv2", 0], ["idx", "rv2", 1], 0, 0, 0, 0, 0, 0] +multiplicity = "read_register2" + +[[constraints.mem]] +kind = "arith" +constraint = "$#`!read_register2` => #`rv2[i]` = 0$" +poly = ["*", ["not", "read_register2"], ["idx", "rv2", "i"]] +iter = ["i", 0, 1] + +[[constraints.mem]] +kind = "interaction" +tag = "MEMW" +input = [1, ["*", ["cast", 2, "DWordWL"], "rd"], ["arr", ["idx", "rvd", 0], ["idx", "rvd", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 2, "DWordWL"]], 1, 0, 0] +multiplicity = "write_register" + +[[constraint_groups]] +name = "ext" + +[[constraints.ext]] +kind = "interaction" +tag = "BYTE_ALU" +input = [["opsel", "AND"], 32, "alu_flags"] +output = ["*", 32, "signed"] +multiplicity = "μ" + +[[constraints.ext]] +kind = "template" +tag = "SIGN" +input = [["idx", "rv1", 1], 1] +output = "rv1_sign" + +[[constraints.ext]] +kind = "arith" +constraint = "$#`arg1[0]` = #`rv1[:2]`$" +poly = ["-", ["idx", "arg1", 0], ["idx", ["cast", "rv1", "DWordWL"], 0]] + +[[constraints.ext]] +kind = "arith" +constraint = "$#`arg1[1]` = (2^(32) - 1) #`signed` dot #`rv1_sign`$" +poly = ["-", ["idx", "arg1", 1], ["*", ["-", ["^", 2, 32], 1], "signed", "rv1_sign"]] + +[[constraints.ext]] +kind = "template" +tag = "SIGN" +input = [["idx", "rv2", 1], 1] +output = "rv2_sign" + +[[constraints.ext]] +kind = "arith" +constraint = "$#`arg2[0]` = #`rv2[:2]` + #`imm[0]`$" +poly = ["-", ["idx", "arg2", 0], ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", "imm", 0]] + +[[constraints.ext]] +kind = "arith" +constraint = "$#`arg2[1]` = (2^(32) - 1) dot #`signed` dot #`rv2_sign` + #`imm[1]`$" +poly = ["-", ["idx", "arg2", 1], ["*", ["-", ["^", 2, 32], 1], "signed", "rv2_sign"], ["idx", "imm", 1]] + +[[constraints.ext]] +kind = "template" +tag = "SIGN" +input = [["idx", "res", 1], 1] +output = "res_sign" + +[[constraints.ext]] +kind = "arith" +constraint = "$#`rvd[0]` = #`res[:2]`$" +poly = ["-", ["idx", "rvd", 0], ["idx", ["cast", "res", "DWordWL"], 0]] + +[[constraints.ext]] +kind = "arith" +constraint = "$#`rvd[1]` = (2^(32) - 1) dot #`res_sign`$" +poly = ["-", ["idx", "rvd", 1], ["*", ["-", ["^", 2, 32], 1], "res_sign"]] diff --git a/spec/src/eq.toml b/spec/src/eq.toml new file mode 100644 index 000000000..c5a7e5b55 --- /dev/null +++ b/spec/src/eq.toml @@ -0,0 +1,93 @@ +name = "EQ" + +[[variables.input]] +name = "a" +type = "DWordWL" +desc = "The first input" +pad = 0 + +[[variables.input]] +name = "b" +type = "DWordWL" +desc = "The second input" +pad = 0 + +[[variables.input]] +name = "invert" +type = "Bit" +desc = "Whether to invert the result" +pad = 0 + +[[variables.output]] +name = "res" +type = "Bit" +desc = "The result" +pad = 1 + +[[variables.auxiliary]] +name = "diff" +type = "DWordHL" +desc = "The difference `a - b`" +pad = 0 + +[[variables.auxiliary]] +name = "eq" +type = "Bit" +desc = "The bit indicating `a == b`" +pad = 1 + +[[variables.multiplicity]] +name = "μ" +type = "BaseField" +desc = "" +pad = 0 + + +[[assumptions]] +desc = "`IS_WORD[a[i]]`" +iter = ["i", 0, 1] + +[[assumptions]] +desc = "`IS_WORD[b[i]]`" +iter = ["i", 0, 1] + + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "diff", "i"]] +multiplicity = "μ" +iter = ["i", 0, 3] + +[[constraints.all]] +kind = "template" +tag = "IS_BIT" +input = ["invert"] + +[[constraints.all]] +kind = "template" +tag = "SUB" +input = ["a", "b"] +output = ["cast", "diff", "DWordWL"] + +[[constraints.all]] +kind = "interaction" +tag = "ZERO" +input = [["+", ["idx", "diff", 0], ["idx", "diff", 1], ["idx", "diff", 2], ["idx", "diff", 3]]] +output = "eq" +multiplicity = "μ" + +[[constraints.all]] +kind = "arith" +constraint = "$#`res` = #`eq` xor #`invert`$" +poly = ["-", ["+", "res", ["*", 2, "eq", "invert"]], "eq", "invert"] + +[[constraints.all]] +kind = "interaction" +tag = "ALU" +input = [["cast", "a", "DWordWL"], ["cast", "b", "DWordWL"], ["+", ["opsel", "EQ"], ["*", 64, "invert"]]] +output = ["arr", "res", 0] +multiplicity = ["-", "μ"] diff --git a/spec/src/load.toml b/spec/src/load.toml index 88e6392a6..c9e91c4ea 100644 --- a/spec/src/load.toml +++ b/spec/src/load.toml @@ -5,7 +5,7 @@ name = "LOAD" [[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" +desc = "The base address to read from, gets offset by $[0, 7]$, depending on how big the access is" pad = 0 [[variables.input]] diff --git a/spec/src/lt.toml b/spec/src/lt.toml index 2cb45d2f0..40d48d73c 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -21,12 +21,18 @@ type = "Bit" desc = "whether to interpret `lhs` and `rhs` as signed integers (1) or not (0)" pad = 0 +[[variables.input]] +name = "invert" +type = "Bit" +desc = "Whether to invert the result" +pad = 0 + # Output [[variables.output]] -name = "lt" +name = "res" type = "Bit" -desc = "Whether $#`lhs` < #`rhs`$, taking `signed` into account" +desc = "The result" pad = 0 @@ -50,6 +56,12 @@ type = "Bit" desc = "The most significant bit of `rhs`" pad = 0 +[[variables.auxiliary]] +name = "lt" +type = "Bit" +desc = "Whether $#`lhs` < #`rhs`$, taking `signed` into account" +pad = 0 + # Virtual [[variables.virtual]] @@ -90,12 +102,32 @@ ref = "lt:a:range_rhs" name = "defs" desc = "Enforce that variables have been correctly computed" +[[constraints.defs]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "lhs", 1]] +multiplicity = "μ" +ref = "lt:c:range_lhs" + +[[constraints.defs]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "rhs", 1]] +multiplicity = "μ" +ref = "lt:c:range_rhs" + [[constraints.defs]] kind = "template" tag = "IS_BIT" input = ["signed"] ref = "lt:c:range_signed" +[[constraints.defs]] +kind = "template" +tag = "IS_BIT" +input = ["invert"] +ref = "lt:c:range_invert" + [[constraints.defs]] kind = "interaction" tag = "MSB16" @@ -119,6 +151,11 @@ desc = "Where $A = #`lhs_msb`$, $B = #`rhs_msb`$ and $C = #`carry[1]`$" poly = ["-", "lt", ["*", "signed", ["+", ["*", "lhs_msb", ["not", "rhs_msb"]], ["*", "lhs_msb", ["idx", "carry", 1]], ["*", ["not", "rhs_msb"], ["idx", "carry", 1]]]], ["*", ["-", 1, "signed"], "unsigned_lt"]] ref = "lt:c:lt" +[[constraints.defs]] +kind = "arith" +constraint = "$#`res` = #`lt` xor #`invert`$" +poly = ["-", ["+", "res", ["*", 2, "lt", "invert"]], "lt", "invert"] + [[constraint_groups]] name = "sub" @@ -130,20 +167,6 @@ tag = "IS_BIT" input = [["idx", "carry", "i"]] iter = ["i", 0, 1] -[[constraints.defs]] -kind = "interaction" -tag = "IS_HALF" -input = [["idx", "lhs", 1]] -multiplicity = "μ" -ref = "lt:c:range_lhs" - -[[constraints.defs]] -kind = "interaction" -tag = "IS_HALF" -input = [["idx", "rhs", 1]] -multiplicity = "μ" -ref = "lt:c:range_rhs" - [[constraints.sub]] kind = "interaction" tag = "IS_HALF" @@ -160,6 +183,6 @@ desc = "Each row contributes the following to the LogUp sum" [[constraints.output]] kind = "interaction" tag = "ALU" -input = [["cast", "lhs", "DWordWL"], ["cast", "rhs", "DWordWL"], ["+", ["opsel", "LT"], ["*", 32, "signed"]]] -output = ["arr", "lt", 0] +input = [["cast", "lhs", "DWordWL"], ["cast", "rhs", "DWordWL"], ["+", ["opsel", "LT"], ["*", 32, "signed"], ["*", 64, "invert"]]] +output = ["arr", "res", 0] multiplicity = ["-", "μ"] diff --git a/spec/src/store.toml b/spec/src/store.toml new file mode 100644 index 000000000..25b4161a3 --- /dev/null +++ b/spec/src/store.toml @@ -0,0 +1,116 @@ +name = "STORE" + +# Input + +[[variables.input]] +name = "base_address" +type = "DWordWL" +desc = "The base address to write 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 = "write2" +type = "Bit" +desc = "Whether to write exactly 2 bytes" +pad = 0 + +[[variables.input]] +name = "write4" +type = "Bit" +desc = "Whether to write exactly 4 bytes" +pad = 0 + +[[variables.input]] +name = "write8" +type = "Bit" +desc = "Whether to write exactly 8 bytes" +pad = 0 + +[[variables.input]] +name = "value" +type = "DWordBL" +desc = "The value to store" +pad = 0 + +# Virtual + +[[variables.virtual]] +name = "write1" +type = "Bit" +desc = "Whether to write exactly 1 byte" +def = ["-", "μ", "write2", "write4", "write8"] + +# Multiplicity + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" +pad = 0 + + +[[assumptions]] +desc = "`IS_WORD[base_address[i]]`" +iter = ["i", 0, 1] + +[[assumptions]] +desc = "`IS_WORD[timestamp[i]]`" +iter = ["i", 0, 1] + + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "template" +tag = "IS_BIT" +input = ["write2"] + +[[constraints.all]] +kind = "template" +tag = "IS_BIT" +input = ["write4"] + +[[constraints.all]] +kind = "template" +tag = "IS_BIT" +input = ["write8"] + +[[constraints.all]] +kind = "template" +tag = "IS_BIT" +input = [["+", "write2", "write4", "write8"]] + +[[constraints.all]] +kind = "arith" +constraint = "$#`write2` + #`write4` + #`write8` => #`μ`$" +poly = ["*", ["+", "write2", "write4", "write8"], ["not", "μ"]] + +[[constraints.all]] +kind = "template" +tag = "IS_BYTE" +input = [["idx", "value", "i"]] +iter = ["i", 0, 7] + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [0, "base_address", "value", "timestamp", "write2", "write4", "write8"] +multiplicity = "μ" + + +[[constraint_groups]] +name = "output" + +[[constraints.output]] +kind = "interaction" +tag = "MEMORY" +input = ["timestamp", "base_address", ["cast", "value", "DWordWL"], ["+", ["*", 4, "write2"], ["*", 8, "write4"], ["*", 16, "write8"]]] +output = ["cast", 0, "DWordWL"] +multiplicity = ["-", "μ"] diff --git a/spec/store.typ b/spec/store.typ new file mode 100644 index 000000000..5b9872b58 --- /dev/null +++ b/spec/store.typ @@ -0,0 +1,47 @@ +#import "/book.typ": book-page, rj +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_assumptions, + render_chip_variable_table, + render_chip_padding_table, + render_constraint_table, + compute_nr_interactions, + total_nr_instantiated_columns, + total_nr_variables, +) + +#let config = load_config() +#let chip = load_chip("src/store.toml", config) + +#show: book-page(chip.name) +#let store = raw(chip.name) + +The #store chip provides functionality to store a value to memory. +It decomposes a `DWord` into bytes and delegates low-level memory handling to the `MEMW` chip (@memw). + += 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 #store chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): +#render_chip_variable_table(chip, config) + += Assumptions +#render_chip_assumptions(chip, config) + += Constraints +The chip delegates the actual memory interaction to the `MEMW` chip, +and ensures the values are proper bytes. + +#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) From d90ebc65ffc65965322f617bcea07ca3db061117 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Wed, 27 May 2026 14:14:14 +0200 Subject: [PATCH 10/25] Fix arg2 muxes --- spec/src/cpu.toml | 6 +++--- spec/src/cpu32.toml | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 99a37a46a..eed35dc23 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -349,11 +349,11 @@ prefix = "A" [[constraints.alu]] kind = "arith" -constraint = "$#`arg2` = #`MEMORY` * #`imm` + #`BRANCH` * (1 - #`JALR`) * #`instruction_length` * #`BRANCH` * #`JALR` * #`rv2` + (1 - #`MEMORY`) * (1 - #`BRANCH`) * (#`rv2` + #`imm`)$" +constraint = "$#`arg2` = #`MEMORY` * #`imm` + #`BRANCH` * (1 - #`JALR`) * #`rv2` * #`BRANCH` * #`JALR` * #`instruction_length` + (1 - #`MEMORY`) * (1 - #`BRANCH`) * (#`rv2` + #`imm`)$" poly = ["-", ["idx", "arg2", "i"], ["*", "MEMORY", ["idx", "imm", "i"]], - ["*", "BRANCH", ["not", "JALR"], "instruction_length"], - ["*", "BRANCH", "JALR", ["idx", "rv2", "i"]], + ["*", "BRANCH", ["not", "JALR"], ["idx", "rv2", "i"]], + ["*", "BRANCH", "JALR", ["idx", ["arr", "instruction_length", 0], "i"]], ["*", ["not", "MEMORY"], ["not", "BRANCH"], ["idx", ["+", "rv2", "imm"], "i"]] ] iter = ["i", 0, 1] diff --git a/spec/src/cpu32.toml b/spec/src/cpu32.toml index 584ddb10d..12aeaf8df 100644 --- a/spec/src/cpu32.toml +++ b/spec/src/cpu32.toml @@ -369,7 +369,7 @@ output = "rv2_sign" [[constraints.ext]] kind = "arith" constraint = "$#`arg2[0]` = #`rv2[:2]` + #`imm[0]`$" -poly = ["-", ["idx", "arg2", 0], ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", "imm", 0]] +poly = ["-", ["idx", "arg2", 0], ["idx", ["cast", "rv2", "DWordWL"], 0], ["idx", "imm", 0]] [[constraints.ext]] kind = "arith" From 8c0b399b5f83445a2a92ee597608e0d2c6694f1b Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Wed, 27 May 2026 14:14:51 +0200 Subject: [PATCH 11/25] Link instruction length to CPU32 --- spec/cpu32.typ | 2 +- spec/src/cpu.toml | 2 +- spec/src/cpu32.toml | 9 +++++++++ spec/src/signatures.toml | 4 ++-- 4 files changed, 13 insertions(+), 4 deletions(-) diff --git a/spec/cpu32.typ b/spec/cpu32.typ index 6114ed5e7..fa4ae6f63 100644 --- a/spec/cpu32.typ +++ b/spec/cpu32.typ @@ -41,7 +41,7 @@ The #cpu32 chip is comprised of #nr_variables variables that are expressed using Most constraints correspond to those already present in the CPU, and we present them here first, including some updates to the range checking corresponding to the differing types. -#render_constraint_table(chip, config, groups: ("decode", "range", "alu", "mem")) +#render_constraint_table(chip, config, groups: ("decode", "range", "alu", "mem", "logup")) Then, we have the constraints corresponding to the sign-extension and definition of `arg1`, `arg2` and `rd`. This includes a step where we extract the `signed` bit from the `alu_flags`, as this determines diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index eed35dc23..93fd2d01f 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -383,7 +383,7 @@ multiplicity = "ALU" [[constraints.alu]] kind = "interaction" tag = "CPU32" -input = ["timestamp", "pc"] +input = ["timestamp", "pc", "instruction_length"] multiplicity = "word_instr" diff --git a/spec/src/cpu32.toml b/spec/src/cpu32.toml index 12aeaf8df..9bd0fc147 100644 --- a/spec/src/cpu32.toml +++ b/spec/src/cpu32.toml @@ -334,6 +334,15 @@ tag = "MEMW" input = [1, ["*", ["cast", 2, "DWordWL"], "rd"], ["arr", ["idx", "rvd", 0], ["idx", "rvd", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 2, "DWordWL"]], 1, 0, 0] multiplicity = "write_register" +[[constraint_groups]] +name = "logup" + +[[constraints.logup]] +kind = "interaction" +tag = "CPU32" +input = ["timestamp", "pc", "instruction_length"] +multiplicity = ["-", "μ"] + [[constraint_groups]] name = "ext" diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index a2d70a51d..042817cac 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -49,11 +49,11 @@ tag = "DECODE" kind = "interaction" input = ["DWordWL", "DWordWL", "BaseField"] -# CPU32[timestamp, pc] +# CPU32[timestamp, pc, instruction_length] [[signatures]] tag = "CPU32" kind = "interaction" -input = ["DWordWL", "DWordWL"] +input = ["DWordWL", "DWordWL", "Byte"] # ALU[out; in1, in2, flags] [[signatures]] From 761abbd8b630d63e18af241f90b336649b4341ee Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 29 May 2026 13:13:23 +0200 Subject: [PATCH 12/25] Apply easy changes from code review Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/cpu.typ | 2 +- spec/cpu32.typ | 2 +- spec/decode.typ | 2 +- spec/dvrm.typ | 2 -- spec/mul.typ | 3 --- spec/src/cpu.toml | 6 +++--- spec/src/cpu32.toml | 2 +- spec/src/decode_uncompressed.toml | 2 +- spec/src/store.toml | 4 ++-- 9 files changed, 10 insertions(+), 15 deletions(-) diff --git a/spec/cpu.typ b/spec/cpu.typ index f597e907b..1c578c911 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -90,7 +90,7 @@ We refer to the previous section's description of `arg2` for how the address is computed. The value to (potentially) be written back to `rd` is stored in `rvd`, -which can either come from either the ALU, in case of an ALU operation or a JALR branch, +which can either come from the ALU --- in case of an ALU operation or a JALR branch --- or from the MEMORY interaction. #render_constraint_table(chip, config, groups: "mem") diff --git a/spec/cpu32.typ b/spec/cpu32.typ index fa4ae6f63..8bc7cb427 100644 --- a/spec/cpu32.typ +++ b/spec/cpu32.typ @@ -19,7 +19,7 @@ The #cpu32 chip is used to delegate the 32-bit instructions of the RV64I instruction set from the main CPU table (@cpu). All 32-bit instructions are ALU-only instructions, so the BRANCH, MEMORY and ECALL paths need no elaboration. -The timestamp and PC have already been read by the CPU table at this point, and need no further checking, +The timestamp and PC have already been read by the CPU table at this point, and need no further checking; the PC for the next instruction will also already be handled by CPU. The structure follows the regular ALU path, with some extra variables and constraints to contain the required sign extensions. diff --git a/spec/decode.typ b/spec/decode.typ index e2098b1eb..16a1e8faf 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -35,7 +35,7 @@ Empty rows with the following content can be added to achieve this: #render_chip_padding_table(chip, config) This is simultaneously the row that is used for padding rows in the CPU, -if the multiplicity if nonzero, +if the multiplicity is nonzero, so we need to ensure that this table has at least one row of padding. = Decoding diff --git a/spec/dvrm.typ b/spec/dvrm.typ index 053155b40..3b026a107 100644 --- a/spec/dvrm.typ +++ b/spec/dvrm.typ @@ -27,8 +27,6 @@ The #dvrm chip provides division and remainder functionality, both signed and un The #dvrm chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): #render_chip_variable_table(chip, config) -// = Assumptions -// #render_chip_assumptions(chip, config) = Constraints diff --git a/spec/mul.typ b/spec/mul.typ index 25a5e9884..e5dc0de7c 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -32,9 +32,6 @@ The #mul chip is comprised of #nr_variables variables that are expressed using # $mat(delim: #none, top; bottom)$ } -// = Assumptions -// The following range checks are assumed to be performed/enforced outside of this chip: -// #render_chip_assumptions(chip, config) = Constraints == Overview diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 93fd2d01f..6caa7f9b1 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -171,7 +171,7 @@ pad = 0 [[variables.auxiliary]] name = "branch_cond" type = "Bit" -desc = "Whether a branch is taken, the branch condition evaluates to true, or we are doing an unconditional jump" +desc = "Whether a branch is taken: the branch condition evaluates to true, or we are doing an unconditional jump" pad = 0 # Virtual @@ -349,7 +349,7 @@ prefix = "A" [[constraints.alu]] kind = "arith" -constraint = "$#`arg2` = #`MEMORY` * #`imm` + #`BRANCH` * (1 - #`JALR`) * #`rv2` * #`BRANCH` * #`JALR` * #`instruction_length` + (1 - #`MEMORY`) * (1 - #`BRANCH`) * (#`rv2` + #`imm`)$" +constraint = "$#`arg2` = #`MEMORY` dot #`imm` + #`BRANCH` dot (1 - #`JALR`) dot #`rv2` + #`BRANCH` dot #`JALR` dot #`instruction_length` + (1 - #`MEMORY`) dot (1 - #`BRANCH`) dot (#`rv2` + #`imm`)$" poly = ["-", ["idx", "arg2", "i"], ["*", "MEMORY", ["idx", "imm", "i"]], ["*", "BRANCH", ["not", "JALR"], ["idx", "rv2", "i"]], @@ -433,7 +433,7 @@ multiplicity = "MEMORY" [[constraints.mem]] kind = "arith" -constraint = "$!#`MEMORY` => #`rvd` = #`res`$" +constraint = "$#`!MEMORY` => #`rvd` = #`res`$" poly = ["*", ["not", "MEMORY"], ["-", ["idx", "rvd", "i"], ["idx", ["cast", "res", "DWordWL"], "i"]]] iter = ["i", 0, 1] diff --git a/spec/src/cpu32.toml b/spec/src/cpu32.toml index 9bd0fc147..8ec91d9d9 100644 --- a/spec/src/cpu32.toml +++ b/spec/src/cpu32.toml @@ -366,7 +366,7 @@ poly = ["-", ["idx", "arg1", 0], ["idx", ["cast", "rv1", "DWordWL"], 0]] [[constraints.ext]] kind = "arith" -constraint = "$#`arg1[1]` = (2^(32) - 1) #`signed` dot #`rv1_sign`$" +constraint = "$#`arg1[1]` = (2^(32) - 1) dot #`signed` dot #`rv1_sign`$" poly = ["-", ["idx", "arg1", 1], ["*", ["-", ["^", 2, 32], 1], "signed", "rv1_sign"]] [[constraints.ext]] diff --git a/spec/src/decode_uncompressed.toml b/spec/src/decode_uncompressed.toml index dc6891f92..38d98c2b2 100644 --- a/spec/src/decode_uncompressed.toml +++ b/spec/src/decode_uncompressed.toml @@ -33,7 +33,7 @@ desc = "whether to load the contents of address `rs2` (1) or `0` (0) into `rv2`. [[variables.output]] name = "write_register" type = "Bit" -desc = "whether the result should be written to `rd` ($=0$ for memory write and when $#`rd` = #`x0`$." +desc = "whether the result should be written to `rd` ($=0$ for memory write and when $#`rd` = #`x0`)$." [[variables.output]] name = "imm" diff --git a/spec/src/store.toml b/spec/src/store.toml index 25b4161a3..06ae1bf44 100644 --- a/spec/src/store.toml +++ b/spec/src/store.toml @@ -89,7 +89,7 @@ input = [["+", "write2", "write4", "write8"]] [[constraints.all]] kind = "arith" -constraint = "$#`write2` + #`write4` + #`write8` => #`μ`$" +constraint = "$#`write2` + #`write4` + #`write8` => #`μ` = 1$" poly = ["*", ["+", "write2", "write4", "write8"], ["not", "μ"]] [[constraints.all]] @@ -111,6 +111,6 @@ name = "output" [[constraints.output]] kind = "interaction" tag = "MEMORY" -input = ["timestamp", "base_address", ["cast", "value", "DWordWL"], ["+", ["*", 4, "write2"], ["*", 8, "write4"], ["*", 16, "write8"]]] +input = ["timestamp", "base_address", ["cast", "value", "DWordWL"], ["+", 1, ["*", 4, "write2"], ["*", 8, "write4"], ["*", 16, "write8"]]] output = ["cast", 0, "DWordWL"] multiplicity = ["-", "μ"] From 013b8657839fb8922f93e05fc2777d51b0ebc157 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 29 May 2026 14:26:01 +0200 Subject: [PATCH 13/25] Address more review comments --- spec/cpu.typ | 6 +++--- spec/decode.typ | 4 +++- spec/eq.typ | 4 ++++ spec/expr.typ | 4 ++-- spec/lt.typ | 4 ++-- spec/shift.typ | 3 --- spec/src/cpu.toml | 28 ++++++++++++++++++--------- spec/src/cpu32.toml | 32 ++++++++++++++++++------------- spec/src/decode_uncompressed.toml | 2 +- spec/src/eq.toml | 6 +++--- spec/src/load.toml | 2 +- spec/src/lt.toml | 17 +++++++++------- spec/src/mul.toml | 10 ++++++++++ spec/src/shift.toml | 6 ------ spec/src/signatures.toml | 9 +++++---- spec/src/store.toml | 8 +++++++- 16 files changed, 89 insertions(+), 56 deletions(-) diff --git a/spec/cpu.typ b/spec/cpu.typ index 1c578c911..d1a8529e9 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -17,7 +17,7 @@ #let cpu = raw(chip.name) 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). +It bases its decisions on the entry of the `DECODE` table (@decode) corresponding the current program counter (PC). = Variables #let nr_variables = total_nr_variables(chip) @@ -45,8 +45,8 @@ All values in `packed_decode` need to be checked to ensure the packing is correct for the interaction. In contrast, we know ahead of time that decoding will ensure proper range checks for `pc` and `imm`. Similarly, since `next_pc` will propagate through the memory argument and be looked up -in the instruction decoding on the next cycle, it is forced to be in the correct range. -The final value for `next_pc` is similarly fixed by the memory finalization. +in the instruction decoding on the next cycle, it is forced to be in the correct range; +the final value for `next_pc` is similarly fixed by the memory finalization. For the auxiliary columns, we need to check the limbs of `res`, since `rv1` and `rv2` are enforced by the memory argument, and `rvd` is correct by the correctness of the dependent chips. The ranges of the other auxiliary columns are enforced through later constraints. diff --git a/spec/decode.typ b/spec/decode.typ index 16a1e8faf..f413a8512 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -8,6 +8,7 @@ render_constraint_table, render_chip_padding_table, ) +#import "/expr.typ": expr_to_math #let config = load_config() #let chip = load_chip("src/decode.toml", config) @@ -48,7 +49,8 @@ The construction of the `alu_flags` and `mem_flags` columns is given here throug #render_chip_variable_table(uncompressed_chip, config) -First, we provide a mapping from an an ALU operation "descriptor" to the numerical value as used for the `alu_op` column: +First, we provide a mapping from an an ALU operation "descriptor" to the numerical value as used for the `alu_op` column. +This is the table used to find the value for the #expr_to_math(("opsel", "OPERATION")) notation when performing `ALU` or `BYTE_ALU` interactions. #figure( table(columns: (auto, auto), diff --git a/spec/eq.typ b/spec/eq.typ index f6d63fea4..379df796d 100644 --- a/spec/eq.typ +++ b/spec/eq.typ @@ -27,6 +27,10 @@ It optionally inverts the result if the `invert` flag is set. The #eq chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): #render_chip_variable_table(chip, config) += Assumptions + +#render_chip_assumptions(chip, config) + = Constraints #render_constraint_table(chip, config) diff --git a/spec/expr.typ b/spec/expr.typ index 98f9ee890..5a275f47e 100644 --- a/spec/expr.typ +++ b/spec/expr.typ @@ -101,7 +101,7 @@ ( "opsel": (pp, rec, e) => { assert(type(e.at(1)) == type(""), message: "opsel expects a string") - repr(e.at(1)) + `⧼` + raw(e.at(1)) + `⧽` }, "arr": (pp, rec, e) => `[` + e.slice(1).map(rec.with(PREC.MAX)).join(`, `) + `]`, "idx": (pp, rec, e) => rec(PREC.MIN, e.at(1)) + `[` + rec(PREC.MAX, e.at(2)) + `]`, @@ -171,7 +171,7 @@ ( "opsel": (pp, rec, e) => { assert(type(e.at(1)) == type(""), message: "opsel expects a string") - $#repr(e.at(1))$ + $lr(chevron.l.curly#raw(e.at(1))chevron.r.curly)$ }, "arr": (pp, rec, e) => $[#e.slice(1).map(rec.with(PREC.MAX)).join($, $)]$, "idx": (pp, rec, e) => { diff --git a/spec/lt.typ b/spec/lt.typ index 126e78269..6dd60b236 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -32,7 +32,7 @@ We assume the inputs `lhs`, `rhs` and `signed` are partially range checked. #render_chip_assumptions(chip, config) = Constraints -We first constrain that all variables correspond to their definition. +We first constrain that all inputs are range checked and all variables correspond to their definition. For the defining constraint of `lt`, @lt:c:lt, observe that it is a choice between two options, depending on the input flag `signed`. In the case of unsigned comparison, we simply need `unsigned_lt`, indicating @@ -75,7 +75,7 @@ However, the left hand side of this is at least $3 dot 2^31$, as $(A, C) = (1, 1 and the right hand side is at most $(2^31 - 1) + (2^32 - 1) + 1 = 3 dot 2^31 - 1$. Therefore, we can use $Q$ to constrain `lt` when `signed = 1`. -#render_constraint_table(chip, config, groups: "defs") +#render_constraint_table(chip, config, groups: ("range", "defs")) And then we constrain the subtraction, taking care of the remaining range checking not yet covered by the assumptions or the `MSB16` lookup. diff --git a/spec/shift.typ b/spec/shift.typ index 8f7af6a9f..a1583e3e7 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -42,9 +42,6 @@ Here, `<<` and `>>` denote the _logical_ left and right shift operations, while The `SHIFT` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): #render_chip_variable_table(chip, config) -= Assumptions -#render_chip_assumptions(chip, config) - = Explanation This chip has a rather complex design as a result of designing it to fit in as few columns possible. We briefly discuss the intricacies of the design, attempting to illustrate its correctness. diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 6caa7f9b1..61b962908 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -213,6 +213,9 @@ ref = "cpu:a:mem-branch-mutex" desc = "When `MEMORY + BRANCH = 0`, either `rs2 = 0` or `imm = 0` should be enforced by the decoding. This is needed for `arg2`." ref = "cpu:a:arg2-multiplex" +[[assumptions]] +desc = "$#`!MEMORY` => #`IS_BIT Date: Fri, 29 May 2026 15:07:48 +0200 Subject: [PATCH 14/25] Fix CPU32 register interactions --- spec/src/cpu32.toml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/spec/src/cpu32.toml b/spec/src/cpu32.toml index 058d571b5..604a1c1d2 100644 --- a/spec/src/cpu32.toml +++ b/spec/src/cpu32.toml @@ -310,28 +310,28 @@ prefix = "M" [[constraints.mem]] kind = "interaction" tag = "MEMW" -input = [1, ["*", ["cast", 2, "DWordWL"], "rs1"], ["arr", ["idx", "rv1", 0], ["idx", "rv1", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 0, "DWordWL"]], 1, 0, 0] -output = ["arr", ["idx", "rv1", 0], ["idx", "rv1", 1], 0, 0, 0, 0, 0, 0] +input = [1, ["*", ["cast", 2, "DWordWL"], "rs1"], ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", "rv1", 2], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 0, "DWordWL"]], 1, 0, 0] +output = ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", "rv1", 2], 0, 0, 0, 0, 0, 0] multiplicity = "read_register1" [[constraints.mem]] kind = "arith" constraint = "$#`!read_register1` => #`rv1[i]` = 0$" poly = ["*", ["not", "read_register1"], ["idx", "rv1", "i"]] -iter = ["i", 0, 1] +iter = ["i", 0, 2] [[constraints.mem]] kind = "interaction" tag = "MEMW" -input = [1, ["*", ["cast", 2, "DWordWL"], "rs2"], ["arr", ["idx", "rv2", 0], ["idx", "rv2", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0] -output = ["arr", ["idx", "rv2", 0], ["idx", "rv2", 1], 0, 0, 0, 0, 0, 0] +input = [1, ["*", ["cast", 2, "DWordWL"], "rs2"], ["arr", ["idx", ["cast", "rv2", "DWordWL"], 0], ["idx", "rv2", 2], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0] +output = ["arr", ["idx", ["cast", "rv2", "DWordWL"], 0], ["idx", "rv2", 2], 0, 0, 0, 0, 0, 0] multiplicity = "read_register2" [[constraints.mem]] kind = "arith" constraint = "$#`!read_register2` => #`rv2[i]` = 0$" poly = ["*", ["not", "read_register2"], ["idx", "rv2", "i"]] -iter = ["i", 0, 1] +iter = ["i", 0, 2] [[constraints.mem]] kind = "interaction" From 88fc8cf24deb9976c41a27e11a69f91e3e988e09 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 29 May 2026 16:41:21 +0200 Subject: [PATCH 15/25] Fix CPUs PC write multiplicity --- spec/src/cpu.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 61b962908..ab5947d7a 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -468,7 +468,7 @@ kind = "interaction" tag = "memory" input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], ["idx", "next_pc", "i"]] iter = ["i", 0, 1] -multiplicity = 1 +multiplicity = -1 [[constraint_groups]] name = "branch" From 7d145017bdbd51a8bc10172579f8350cd026e439 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 29 May 2026 16:41:37 +0200 Subject: [PATCH 16/25] Fix HALT's interaction with the CPU padding --- spec/halt.typ | 7 +++++-- spec/src/halt.toml | 19 ++++++++++++++++--- 2 files changed, 21 insertions(+), 5 deletions(-) diff --git a/spec/halt.typ b/spec/halt.typ index 691154f61..50a39ac40 100644 --- a/spec/halt.typ +++ b/spec/halt.typ @@ -32,9 +32,12 @@ It is assumed the input is range checked: The #halt chip: + makes sure register `x10` (containing the exit code) equals $0$ (@halt:c:read_zero_exit_code), + writes $0$ to all other registers (@halt:c:zeroize_registers_lo/@halt:c:zeroize_registers_hi), and -+ sets `pc` equal to $1$ (@halt:c:pc). -Note that the writes performed by all these interactions are accompanied by the timestamp $2^64-1$; the maximum timestamp. ++ sets `pc` equal to $1$ (@halt:c:consume_pc, @halt:c:emit_pc). +Note that the writes performed by all these interactions --- except for the `pc` --- are accompanied by the timestamp $2^64-1$; the maximum timestamp. This prevents any other operation involving memory from being executed hereafter. +The `pc` is consumed and re-emitted at the same timestamp to enable padding rows for the CPU. +This means that the verifier will have to know the final timestamp at which a CPU padding `pc` was written +to be able to balance the final LogUp. #render_constraint_table(chip, config, groups: "all") #aside("Note on register clean up", diff --git a/spec/src/halt.toml b/spec/src/halt.toml index 9fee04877..6adc1efdb 100644 --- a/spec/src/halt.toml +++ b/spec/src/halt.toml @@ -5,6 +5,10 @@ name = "timestamp" type = "DWordWL" desc = "timestamp at which to halt the program" +[[variables.auxiliary]] +name = "pc" +type = "DWordWL" +desc = "The `next_pc` value the CPU wrote during the instruction HALT was invoked" [[assumptions]] desc = "`IS_WORD[timestamp[i]]`" @@ -40,10 +44,19 @@ ref = "halt:c:zeroize_registers_hi" [[constraints.all]] kind = "interaction" -tag = "MEMW" -input = [1, ["cast", ["*", 2, 255], "DWordWL"], ["arr", 1, 0, 0, 0, 0, 0, 0, 0], ["cast", ["-", ["^", 2, 64], 1], "DWordWL"], 1, 0, 0] +tag = "memory" +input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["arr", ["+", ["idx", "timestamp", 0], 1], ["idx", "timestamp", 1]], ["idx", "pc", "i"]] multiplicity = 1 -ref = "halt:c:pc" +iter = ["i", 0, 1] +ref = "halt:c:consume_pc" + +[[constraints.all]] +kind = "interaction" +tag = "memory" +input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["arr", ["+", ["idx", "timestamp", 0], 1], ["idx", "timestamp", 1]], ["idx", ["arr", 1, 0], "i"]] +multiplicity = -1 +iter = ["i", 0, 1] +ref = "halt:c:emit_pc" [[constraint_groups]] name = "lookup" From 9b30b9ed745a6df05e165cbab33e6a6dc7ca23a0 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 29 May 2026 19:11:13 +0200 Subject: [PATCH 17/25] Add some optional extra arith constraints to enforce the "easy" assumptions --- spec/branch.typ | 5 +++++ spec/cpu.typ | 5 +++++ spec/cpu32.typ | 5 +++++ spec/memw.typ | 13 ++++++++++++- spec/src/branch.toml | 7 +++++++ spec/src/cpu.toml | 25 +++++++++++++++++++++++-- spec/src/cpu32.toml | 9 +++++++++ spec/src/memw.toml | 22 ++++++++++++++++++++++ spec/src/memw_aligned.toml | 22 ++++++++++++++++++++++ 9 files changed, 110 insertions(+), 3 deletions(-) diff --git a/spec/branch.typ b/spec/branch.typ index 0743ae2f9..d6ab53a18 100644 --- a/spec/branch.typ +++ b/spec/branch.typ @@ -30,6 +30,11 @@ The #branch chip is comprised of #nr_variables variables that are expressed usin #render_chip_assumptions(chip, config) +Some of the assumptions can be checked with only arithmetic constraints, so we +provide these below. + +#render_constraint_table(chip, config, groups: "assumptions") + = Constraints We constrain `next_pc` to be $#`base_address` + #`offset`$, diff --git a/spec/cpu.typ b/spec/cpu.typ index d1a8529e9..307e1bb41 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -30,6 +30,11 @@ The #cpu chip is comprised of #nr_variables variables that are expressed using # = Assumptions #render_chip_assumptions(chip, config) +Additionally, the following constraints can be used to provide defense-in-depth +validation of the assumptions. + +#render_constraint_table(chip, config, groups: "assumptions") + = Constraints First, we perform a decoding lookup for the current PC. diff --git a/spec/cpu32.typ b/spec/cpu32.typ index 8bc7cb427..e5e8963bc 100644 --- a/spec/cpu32.typ +++ b/spec/cpu32.typ @@ -36,6 +36,11 @@ The #cpu32 chip is comprised of #nr_variables variables that are expressed using #render_chip_assumptions(chip, config) +Some of the assumptions can be checked with only arithmetic constraints, so we +provide these below. + +#render_constraint_table(chip, config, groups: "assumptions") + = Constraints Most constraints correspond to those already present in the CPU, and we present them here first, diff --git a/spec/memw.typ b/spec/memw.typ index 425508597..b963ea562 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -34,6 +34,11 @@ The #memw chip is comprised of #nr_variables variables that are expressed using #render_chip_assumptions(chip, config) +Some of the assumptions can be checked with only arithmetic constraints, so we +provide these below. + +#render_constraint_table(chip, config, groups: "assumptions") + Our assumptions do not explicitly cover any range checks for the `is_register` and `value` columns, as these are not necessary for the correctness of this chip in isolation. Still, these properties are necessary for the consistency of the system as a whole, and therefore @@ -93,6 +98,12 @@ Further logic remains essentially the same, so we briefly present the relevant t The #aligned chip only needs #nr_variables variables, expressed through #nr_columns columns; it leverages #nr_aligned_interactions interactions. #render_chip_variable_table(alignedchip, config) #render_chip_assumptions(alignedchip, config) + +Some of the assumptions can be checked with only arithmetic constraints, so we +provide these below. + +#render_constraint_table(alignedchip, config, groups: "assumptions") + #render_constraint_table(alignedchip, config) == Padding @@ -159,4 +170,4 @@ The table can be padded to the next power of two with the following value assign The following ideas may prove to be optimizations for the #memw/#aligned/#reg chip: - `MEMB` chip that does a one-byte write to remove old_timestamp from here (uncertain tradeoffs) - Adding `μ_sum`/`w2`/`w4`/`write8` multiplicities to the `IS_HALF` lookups may make some GKR things faster if there are known zeroes. -- For the register fast-path, one may upgrade the `IS_HALF` check to an `IS_B20` check for extended range at the cost of looking through a larger table. \ No newline at end of file +- For the register fast-path, one may upgrade the `IS_HALF` check to an `IS_B20` check for extended range at the cost of looking through a larger table. diff --git a/spec/src/branch.toml b/spec/src/branch.toml index 07af5f7c9..92b93d015 100644 --- a/spec/src/branch.toml +++ b/spec/src/branch.toml @@ -97,6 +97,13 @@ iter = ["i", 0, 1] desc = "`IS_BIT`" +[[constraint_groups]] +name = "assumptions" + +[[constraints.assumptions]] +kind = "template" +tag = "IS_BIT" +input = ["JALR"] [[constraint_groups]] name = "all" diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index ab5947d7a..d62078a10 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -210,11 +210,32 @@ desc = "`MEMORY` and `BRANCH` are mutually exclusive" ref = "cpu:a:mem-branch-mutex" [[assumptions]] -desc = "When `MEMORY + BRANCH = 0`, either `rs2 = 0` or `imm = 0` should be enforced by the decoding. This is needed for `arg2`." +desc = "When `MEMORY + BRANCH = 0`, either `read_register2 = 0` or `imm = 0` should be enforced by the decoding. This is needed for `arg2`." ref = "cpu:a:arg2-multiplex" [[assumptions]] -desc = "$#`!MEMORY` => #`IS_BIT Date: Mon, 1 Jun 2026 16:56:25 +0200 Subject: [PATCH 18/25] Combine assumptions constraints --- spec/src/cpu.toml | 3 +-- spec/src/cpu32.toml | 3 +-- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index d62078a10..ea878848b 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -227,8 +227,7 @@ poly = ["*", "MEMORY", "BRANCH"] [[constraints.assumptions]] kind = "arith" constraint = "$(1 - #`MEMORY` - #`BRANCH`) => (#`read_register2` = 0 or #`imm[i]` = 0)$" -poly = ["*", ["-", 1, "MEMORY", "BRANCH"], "read_register2", ["idx", "imm", "i"]] -iter = ["i", 0, 1] +poly = ["*", ["-", 1, "MEMORY", "BRANCH"], "read_register2", ["+", ["idx", "imm", 0], ["idx", "imm", 1]]] [[constraints.assumptions]] kind = "template" diff --git a/spec/src/cpu32.toml b/spec/src/cpu32.toml index 767eccae5..3aa3a8875 100644 --- a/spec/src/cpu32.toml +++ b/spec/src/cpu32.toml @@ -187,8 +187,7 @@ name = "assumptions" [[constraints.assumptions]] kind = "arith" constraint = "$#`read_register2` = 0 or #`imm[i] = 0`$" -poly = ["*", "read_register2", ["idx", "imm", "i"]] -iter = ["i", 0, 1] +poly = ["*", "read_register2", ["+", ["idx", "imm", 0], ["idx", "imm", 1]]] [[constraint_groups]] name = "decode" From 322bfbcf6df30b96f5640fc777de16de8ade1090 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 1 Jun 2026 16:58:06 +0200 Subject: [PATCH 19/25] Remove todo comments that got a tracking issue --- spec/dvrm.typ | 1 - spec/src/load.toml | 1 - 2 files changed, 2 deletions(-) diff --git a/spec/dvrm.typ b/spec/dvrm.typ index 3b026a107..c2d1c6450 100644 --- a/spec/dvrm.typ +++ b/spec/dvrm.typ @@ -109,7 +109,6 @@ Rewriting R1, we find the constraint $not#`overflow` => #`n` - #`r` = #`qd`$. Since `n`, `d`, `q` and `r` are all 64-bit integers, we must assert this equality $mod 2^128$, rather than $mod 2^64$. To this end, we introduce `extended_n_sub_r` and leverage the `MUL` chip to verify that it is equal to $#`qd` mod 2^128$ using constraints @dvrm:c:mul_lower and @dvrm:c:mul_upper; @dvrm:c:q_range is included to uphold assumption @mul:c:rhs. -// TODO: Update because this is now checked by MUL #render_constraint_table(chip, config, groups:("equality", )) diff --git a/spec/src/load.toml b/spec/src/load.toml index 2fe1e0bbc..e6cf56f00 100644 --- a/spec/src/load.toml +++ b/spec/src/load.toml @@ -120,7 +120,6 @@ input = [0, "base_address", ["cast", "res", ["BaseField", 8]], "timestamp", "rea output = "res" multiplicity = "μ" -# TODO? MSB8 batching? [[constraints.all]] kind = "interaction" tag = "MSB8" From 1dee915220cb79045f67f0198b8f0e835a43d14a Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 1 Jun 2026 17:17:38 +0200 Subject: [PATCH 20/25] word_instr gate for read_registerX out of caution --- spec/src/cpu.toml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index ea878848b..5f110e4d3 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -260,6 +260,16 @@ kind = "arith" constraint = "$#`word_instr` => #`ECALL = 0`$" poly = ["*", "word_instr", "ECALL"] +[[constraints.decode]] +kind = "arith" +constraint = "$#`word_instr` => #`read_register1 = 0`$" +poly = ["*", "word_instr", "read_register1"] + +[[constraints.decode]] +kind = "arith" +constraint = "$#`word_instr` => #`read_register2 = 0`$" +poly = ["*", "word_instr", "read_register2"] + [[constraints.decode]] kind = "arith" constraint = "$#`word_instr` => #`write_register = 0`$" From c9540a55fee9141b1f2d4b860892b36042a850a4 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 1 Jun 2026 17:38:50 +0200 Subject: [PATCH 21/25] Fix JAL(R) decoding and ALU --- spec/cpu.typ | 3 +-- spec/decode.typ | 14 +++++++------- spec/src/cpu.toml | 17 ++++++++++++----- 3 files changed, 20 insertions(+), 14 deletions(-) diff --git a/spec/cpu.typ b/spec/cpu.typ index 307e1bb41..6fd2c0023 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -68,8 +68,7 @@ The other contributions for `arg2` are specific to the (mutually exclusive, @cpu `MEMORY` and `BRANCH` flags: - For the `MEMORY` path, we want the output of the ALU to be $#`rv1` + #`imm`$, as that is the address at which the memory access occurs. -- For the `BRANCH` path, when we do not have a JALR instruction, we want the ALU output to reflect the branch condition. -- For the `BRANCH` path, when it is a JALR instruction, we want the ALU output to contain the next instructions PC value, to store into `rd`. +- For the `BRANCH` path, we want the ALU output to reflect the branch condition (or just be inactive for JALR). Instructions having the `word_instr` flag set are delegated to the `CPU32` chip, which will do its own decoding and execution of the instruction. diff --git a/spec/decode.typ b/spec/decode.typ index f413a8512..eb3e348f8 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -139,13 +139,13 @@ Further clarification is provided in the notes following the table. // LUI/AUIPC ([`LUI rd, imm`], [`ADD`], [], [], [], [#ref_note()]), ([`AUIPC rd, imm`], [`ADD`], [], [], [`rs1 := x255`], [#ref_note()]), - ([`JAL rd, imm`], [`ADD`], [], [], [`BRANCH`, `JALR`, `rs1 := x255`], [#ref_note()]), + ([`JAL rd, imm`], [], [], [], [`BRANCH`, `JALR`, `rs1 := x255`], [#ref_note()]), // Branching - ([`JALR rd, rs1, imm`], [`ADD`], [], [], [`BRANCH`, `JALR`], []), - ([`BEQ rs1, rs2, imm`], [`EQ`], [], [], [], []), - ([`BNE rs1, rs2, imm`], [`EQ`], [], [], [`invert`], []), - ([`BLT[U] rs1, rs2, imm`], [`LT`], [], [#sym.not`[U]`], [], [#ref_note()]), - ([`BGE[U] rs1, rs2, imm`], [`LT`], [], [#sym.not`[U]`], [`invert`], [#ref_note()]), + ([`JALR rd, rs1, imm`], [], [], [], [`BRANCH`, `JALR`], []), + ([`BEQ rs1, rs2, imm`], [`EQ`], [], [], [`BRANCH`], []), + ([`BNE rs1, rs2, imm`], [`EQ`], [], [], [`BRANCH`, `invert`], []), + ([`BLT[U] rs1, rs2, imm`], [`LT`], [], [#sym.not`[U]`], [`BRANCH`], [#ref_note()]), + ([`BGE[U] rs1, rs2, imm`], [`LT`], [], [#sym.not`[U]`], [`BRANCH`, `invert`], [#ref_note()]), // LOAD ([`LD rd, rs1, imm`], [`ADD`], [], [], [`MEMORY`, `mem_8B`], []), ([`LW[U] rd, rs1, imm`], [`ADD`], [], [], [`MEMORY`, `mem_signed := `#sym.not`[U]`, `mem_4B`], [#ref_note()]), @@ -215,7 +215,7 @@ We note the following about the above decoding table: enum.item( referenceable_note( "note-jal", - [`JAL`: this operation stores $#`pc` + 4$ in `rd` and adds two times the sign-extended 20-bit immediate to the `pc`. + [`JAL`: this operation stores $#`pc` + #`instruction_length`$ in `rd` and adds two times the sign-extended 20-bit immediate to the `pc`. Note that this can be represented using `JALR rd, x255, imm`. As such, *we expect the decoding to take care of writing the immediate in bit range $[1:21]$ of `imm` and extending it to 64 bits; the least significant bit should always be 0.*] ) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 5f110e4d3..cf424435f 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -394,11 +394,10 @@ prefix = "A" [[constraints.alu]] kind = "arith" -constraint = "$#`arg2` = #`MEMORY` dot #`imm` + #`BRANCH` dot (1 - #`JALR`) dot #`rv2` + #`BRANCH` dot #`JALR` dot #`instruction_length` + (1 - #`MEMORY`) dot (1 - #`BRANCH`) dot (#`rv2` + #`imm`)$" +constraint = "$#`arg2` = #`MEMORY` dot #`imm` + #`BRANCH` dot #`rv2` + (1 - #`MEMORY`) dot (1 - #`BRANCH`) dot (#`rv2` + #`imm`)$" poly = ["-", ["idx", "arg2", "i"], ["*", "MEMORY", ["idx", "imm", "i"]], - ["*", "BRANCH", ["not", "JALR"], ["idx", "rv2", "i"]], - ["*", "BRANCH", "JALR", ["idx", ["arr", "instruction_length", 0], "i"]], + ["*", "BRANCH", ["idx", "rv2", "i"]], ["*", ["not", "MEMORY"], ["not", "BRANCH"], ["idx", ["+", "rv2", "imm"], "i"]] ] iter = ["i", 0, 1] @@ -472,8 +471,8 @@ multiplicity = "MEMORY" [[constraints.mem]] kind = "arith" -constraint = "$#`!MEMORY` => #`rvd` = #`res`$" -poly = ["*", ["not", "MEMORY"], ["-", ["idx", "rvd", "i"], ["idx", ["cast", "res", "DWordWL"], "i"]]] +constraint = "$#`!MEMORY` and #`!BRANCH` => #`rvd` = #`res`$" +poly = ["*", ["not", ["+", "MEMORY", "BRANCH"]], ["-", ["idx", "rvd", "i"], ["idx", ["cast", "res", "DWordWL"], "i"]]] iter = ["i", 0, 1] [[constraints.mem]] @@ -528,6 +527,14 @@ output = "next_pc" cond = ["not", "branch_cond"] desc = "Increment `pc` to `next_pc` if we're not branching" +[[constraints.branch]] +kind = "template" +tag = "ADD" +input = ["pc", ["arr", "instruction_length", 0]] +output = "rvd" +cond = ["BRANCH"] +desc = "Compute the next instruction address in `rvd` when BRANCH is active to enable JALR" + [[constraint_groups]] name = "sys" From dad2eeabff2e0c88e3e828cffd8942a526dadbcd Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 1 Jun 2026 17:46:41 +0200 Subject: [PATCH 22/25] Placate the type checker --- spec/src/cpu.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index cf424435f..787e669c9 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -472,7 +472,7 @@ multiplicity = "MEMORY" [[constraints.mem]] kind = "arith" constraint = "$#`!MEMORY` and #`!BRANCH` => #`rvd` = #`res`$" -poly = ["*", ["not", ["+", "MEMORY", "BRANCH"]], ["-", ["idx", "rvd", "i"], ["idx", ["cast", "res", "DWordWL"], "i"]]] +poly = ["*", ["-", 1, ["+", "MEMORY", "BRANCH"]], ["-", ["idx", "rvd", "i"], ["idx", ["cast", "res", "DWordWL"], "i"]]] iter = ["i", 0, 1] [[constraints.mem]] @@ -532,7 +532,7 @@ kind = "template" tag = "ADD" input = ["pc", ["arr", "instruction_length", 0]] output = "rvd" -cond = ["BRANCH"] +cond = "BRANCH" desc = "Compute the next instruction address in `rvd` when BRANCH is active to enable JALR" From b1b51c9d4df6b8675ba884efaa203f7abc9afe3f Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 2 Jun 2026 11:29:24 +0200 Subject: [PATCH 23/25] Represent instruction length as half --- spec/decode.typ | 7 ++++--- spec/src/cpu.toml | 14 +++++++------- spec/src/cpu32.toml | 10 +++++----- spec/src/decode.toml | 2 +- spec/src/decode_uncompressed.toml | 4 ++-- spec/src/signatures.toml | 2 +- 6 files changed, 20 insertions(+), 19 deletions(-) diff --git a/spec/decode.typ b/spec/decode.typ index eb3e348f8..6defcdc84 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -171,8 +171,9 @@ this by having no valid decoding available for when the instruction is encounter == C-type instructions The `RV64C` extension for compressed instructions specifies that \~50% of all instructions can be represented using a 16-bit instruction (rather than 32-bits), saving \~25% in code size. This execution of assembly code is _not_ agnostic to an instruction's compression state; after executing a compressed instruction, the `pc` should be incremented by $2$ rather than $4$. -As such, we provide the `instruction_length` column that *must take on the value $2$ for compressed instructions and $4$ for regular instructions*. -This additionally opens the door for future optimizations involving "fused" instructions, where common sequences +As such, we provide the `half_instruction_length` column that *must take on the value $1$ for compressed instructions and $2$ for regular instructions*. +It is represented as half the number of bytes in the instruction to make misaligned instructions lengths unrepresentable. +Additionally, having the variable opens the door for future optimizations involving "fused" instructions, where common sequences of instructions are merged into a single decoded version and need only a single CPU row to prove. // Construct a note that can be referenced through `lbl` @@ -215,7 +216,7 @@ We note the following about the above decoding table: enum.item( referenceable_note( "note-jal", - [`JAL`: this operation stores $#`pc` + #`instruction_length`$ in `rd` and adds two times the sign-extended 20-bit immediate to the `pc`. + [`JAL`: this operation stores $#`pc` + #`2 * half_instruction_length`$ in `rd` and adds two times the sign-extended 20-bit immediate to the `pc`. Note that this can be represented using `JALR rd, x255, imm`. As such, *we expect the decoding to take care of writing the immediate in bit range $[1:21]$ of `imm` and extending it to 64 bits; the least significant bit should always be 0.*] ) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 787e669c9..ec9c851f2 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -59,10 +59,10 @@ pad = 0 # We encode C-type instructions with a length of 2, as this generality allows fusing common instruction combos [[variables.input]] -name = "instruction_length" +name = "half_instruction_length" type = "Byte" desc = "The number of bytes consumed by this instruction, commonly used to indicate whether the instruction is of C type, i.e., whether it is 2 bytes long instead of 4" -pad = 0 +pad = 2 [[variables.input]] name = "word_instr" @@ -199,7 +199,7 @@ def = ["+", ["*", ["^", 2, 10], "rs1"], ["*", ["^", 2, 18], "rs2"], ["*", ["^", 2, 26], "rd"], - ["*", ["^", 2, 34], "instruction_length"], + ["*", ["^", 2, 34], "half_instruction_length"], ["*", ["^", 2, 42], "alu_flags"], ["*", ["^", 2, 50], "mem_flags"], ] @@ -279,7 +279,7 @@ poly = ["*", "word_instr", "write_register"] kind = "interaction" tag = "CPU32" input = ["timestamp", "pc"] -output = "instruction_length" +output = "half_instruction_length" multiplicity = "word_instr" @@ -308,7 +308,7 @@ ref = "cpu:c:range_write_register" [[constraints.range]] kind = "template" tag = "IS_BYTE" -input = ["instruction_length"] +input = ["half_instruction_length"] ref = "cpu:c:range_c_type_instruction" [[constraints.range]] @@ -522,7 +522,7 @@ multiplicity = "branch_cond" [[constraints.branch]] kind = "template" tag = "ADD" -input = ["pc", ["arr", "instruction_length", 0]] +input = ["pc", ["arr", ["*", 2, "half_instruction_length"], 0]] output = "next_pc" cond = ["not", "branch_cond"] desc = "Increment `pc` to `next_pc` if we're not branching" @@ -530,7 +530,7 @@ desc = "Increment `pc` to `next_pc` if we're not branching" [[constraints.branch]] kind = "template" tag = "ADD" -input = ["pc", ["arr", "instruction_length", 0]] +input = ["pc", ["arr", ["*", 2, "half_instruction_length"], 0]] output = "rvd" cond = "BRANCH" desc = "Compute the next instruction address in `rvd` when BRANCH is active to enable JALR" diff --git a/spec/src/cpu32.toml b/spec/src/cpu32.toml index 3aa3a8875..f26ce0e8c 100644 --- a/spec/src/cpu32.toml +++ b/spec/src/cpu32.toml @@ -13,10 +13,10 @@ desc = "The PC at which the instruction occurs" pad = 0 [[variables.output]] -name = "instruction_length" +name = "half_instruction_length" type = "Byte" desc = "The length of this instruction" -pad = 4 +pad = 2 [[variables.auxiliary]] name = "rs1" @@ -160,7 +160,7 @@ def = ["+", ["*", ["^", 2, 10], "rs1"], ["*", ["^", 2, 18], "rs2"], ["*", ["^", 2, 26], "rd"], - ["*", ["^", 2, 34], "instruction_length"], + ["*", ["^", 2, 34], "half_instruction_length"], ["*", ["^", 2, 42], "alu_flags"], ] @@ -225,7 +225,7 @@ input = ["write_register"] [[constraints.range]] kind = "template" tag = "IS_BYTE" -input = ["instruction_length"] +input = ["half_instruction_length"] [[constraints.range]] kind = "template" @@ -354,7 +354,7 @@ name = "logup" kind = "interaction" tag = "CPU32" input = ["timestamp", "pc"] -output = "instruction_length" +output = "half_instruction_length" multiplicity = ["-", "μ"] [[constraint_groups]] diff --git a/spec/src/decode.toml b/spec/src/decode.toml index 17a10f57c..1e0c6dd8f 100644 --- a/spec/src/decode.toml +++ b/spec/src/decode.toml @@ -25,7 +25,7 @@ A list of each variable and the bit(-range) in which it is located:\\ [10:17] `rs1`, \\ [18:25] `rs2`, \\ [26:33] `rd`, \\ -[34:41] `instruction_length`, \\ +[34:41] `half_instruction_length`, \\ [42:49] `alu_flags`, \\ [50:57] `mem_flags`, \\ the remaining bits are set to zero. diff --git a/spec/src/decode_uncompressed.toml b/spec/src/decode_uncompressed.toml index 45ad40f95..692ac4acd 100644 --- a/spec/src/decode_uncompressed.toml +++ b/spec/src/decode_uncompressed.toml @@ -76,9 +76,9 @@ type = "Bit" desc = "Perform an ECALL" [[variables.output]] -name = "instruction_length" +name = "half_instruction_length" type = "Byte" -desc = "How many bytes is this instruction in the program" +desc = "Half of how many bytes this instruction takes up in the program" [[variables.auxiliary]] name = "alu_op" diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index 810d865fe..6ea23bb9e 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -49,7 +49,7 @@ tag = "DECODE" kind = "interaction" input = ["DWordWL", "DWordWL", "BaseField"] -# CPU32[instruction_length; timestamp, pc] +# CPU32[half_instruction_length; timestamp, pc] [[signatures]] tag = "CPU32" kind = "interaction" From fdcf023b22332d926302738e36e1a45369edb4d0 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 2 Jun 2026 15:04:37 +0200 Subject: [PATCH 24/25] Update spec/src/cpu.toml Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/src/cpu.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index ec9c851f2..39bdb9bbf 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -472,7 +472,7 @@ multiplicity = "MEMORY" [[constraints.mem]] kind = "arith" constraint = "$#`!MEMORY` and #`!BRANCH` => #`rvd` = #`res`$" -poly = ["*", ["-", 1, ["+", "MEMORY", "BRANCH"]], ["-", ["idx", "rvd", "i"], ["idx", ["cast", "res", "DWordWL"], "i"]]] +poly = ["*", ["-", 1, "MEMORY", "BRANCH"], ["-", ["idx", "rvd", "i"], ["idx", ["cast", "res", "DWordWL"], "i"]]] iter = ["i", 0, 1] [[constraints.mem]] From 9be4ecd217ff1cbf728d09d1e71a5f3084584901 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 2 Jun 2026 15:06:36 +0200 Subject: [PATCH 25/25] fixes --- spec/cpu.typ | 2 -- spec/src/cpu.toml | 6 +++--- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/spec/cpu.typ b/spec/cpu.typ index 6fd2c0023..cb11661f3 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -70,8 +70,6 @@ The other contributions for `arg2` are specific to the (mutually exclusive, @cpu address at which the memory access occurs. - For the `BRANCH` path, we want the ALU output to reflect the branch condition (or just be inactive for JALR). -Instructions having the `word_instr` flag set are delegated to the `CPU32` chip, which will do its own decoding and execution of the instruction. - #render_constraint_table(chip, config, groups: "alu") == Memory diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 39bdb9bbf..85c3aaf70 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -61,7 +61,7 @@ pad = 0 [[variables.input]] name = "half_instruction_length" type = "Byte" -desc = "The number of bytes consumed by this instruction, commonly used to indicate whether the instruction is of C type, i.e., whether it is 2 bytes long instead of 4" +desc = "Half the number of bytes consumed by this instruction, commonly used to indicate whether the instruction is of C type, i.e., whether it is 2 bytes long (= 1) instead of 4 (= 2)" pad = 2 [[variables.input]] @@ -394,11 +394,11 @@ prefix = "A" [[constraints.alu]] kind = "arith" -constraint = "$#`arg2` = #`MEMORY` dot #`imm` + #`BRANCH` dot #`rv2` + (1 - #`MEMORY`) dot (1 - #`BRANCH`) dot (#`rv2` + #`imm`)$" +constraint = "$#`arg2` = #`MEMORY` dot #`imm` + #`BRANCH` dot #`rv2` + (1 - #`MEMORY` - #`BRANCH`) dot (#`rv2` + #`imm`)$" poly = ["-", ["idx", "arg2", "i"], ["*", "MEMORY", ["idx", "imm", "i"]], ["*", "BRANCH", ["idx", "rv2", "i"]], - ["*", ["not", "MEMORY"], ["not", "BRANCH"], ["idx", ["+", "rv2", "imm"], "i"]] + ["*", ["-", 1, "MEMORY", "BRANCH"], ["idx", ["+", "rv2", "imm"], "i"]] ] iter = ["i", 0, 1]