diff --git a/spec/assets/style.css b/spec/assets/style.css index 75a27dbc7..9230eac78 100644 --- a/spec/assets/style.css +++ b/spec/assets/style.css @@ -649,3 +649,17 @@ dt::after { dd { grid-column-start: 2; } + +/* Notelist */ +.notelist > ul { + list-style: none; + padding-left: 1em; +} + +.notelist > ul > li figure { + display: none; +} + +sup { + font-size: 0.8em; +} diff --git a/spec/chapters/decode.typ b/spec/chapters/decode.typ index 8e923dbb3..0103de54a 100644 --- a/spec/chapters/decode.typ +++ b/spec/chapters/decode.typ @@ -8,7 +8,7 @@ render_chip_padding_table, ) #import "/expr.typ": expr_to_math -#import "/meta.typ": stripe_tables +#import "/meta.typ": stripe_tables, notelist #let config = load_config() #let chip = load_chip("src/decode.toml", config) @@ -82,11 +82,6 @@ For the purpose of brevity and readability, the table uses the following rules-o Further clarification is provided in the notes following the table. -/// Add a reference to one or more notes following this table. -#let ref_note(..refs) = { - super("[" + refs.pos().map(r => ref(r)).join(",") + "]") -} - #let decoding_table(lines) = { show figure: set block(breakable: true) show: stripe_tables @@ -107,55 +102,55 @@ Further clarification is provided in the notes following the table. #let decoding = ( // OP-IMM - ([`ADDI[W] rd, rs1, imm`], [`ADD`], [`[W]`], [], [], [#ref_note()]), - ([`SLTI[U] rd, rs1, imm`], [`LT`], [], [#sym.not`[U]`], [], [#ref_note()]), + ([`ADDI[W] rd, rs1, imm`], [`ADD`], [`[W]`], [], [], [@decode:note:word_instr]), + ([`SLTI[U] rd, rs1, imm`], [`LT`], [], [#sym.not`[U]`], [], [@decode:note:signed]), ([`ANDI rd, rs1, imm`], [`AND`], [], [], [], []), ([`ORI rd, rs1, imm`], [`OR`], [], [], [], []), ([`XORI rd, rs1, imm`], [`XOR`], [], [], [], []), - ([`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()]), + ([`SLLI[W] rd, rs1, imm`], [`SHIFT[W]`], [`[W]`], [], [], [@decode:note:word_instr]), + ([`SRLI[W] rd, rs1, imm`], [`SHIFT[W]`], [`[W]`], [], [`invert`], [@decode:note:word_instr]), + ([`SRAI[W] rd, rs1, imm`], [`SHIFT[W]`], [`[W]`], [1], [`invert`], [@decode:note:word_instr]), // OP - ([`ADD[W] rd, rs1, rs2`], [`ADD`], [`[W]`], [], [], [#ref_note()]), - ([`SUB[W] rd, rs1, rs2`], [`SUB`], [`[W]`], [], [], [#ref_note()]), - ([`SLT[U] rd, rs1, rs2`], [`LT`], [], [#sym.not`[U]`], [], [#ref_note()]), + ([`ADD[W] rd, rs1, rs2`], [`ADD`], [`[W]`], [], [], [@decode:note:word_instr]), + ([`SUB[W] rd, rs1, rs2`], [`SUB`], [`[W]`], [], [], [@decode:note:word_instr]), + ([`SLT[U] rd, rs1, rs2`], [`LT`], [], [#sym.not`[U]`], [], [@decode:note:signed]), ([`AND rd, rs1, rs2`], [`AND`], [], [], [], []), ([`OR rd, rs1, rs2`], [`OR`], [], [], [], []), ([`XOR rd, rs1, rs2`], [`XOR`], [], [], [], []), - ([`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()]), + ([`SLL[W] rd, rs1, rs2`], [`SHIFT[W]`], [`[W]`], [], [], [@decode:note:word_instr]), + ([`SRL[W] rd, rs1, rs2`], [`SHIFT[W]`], [`[W]`], [], [`invert`], [@decode:note:word_instr]), + ([`SRA[W] rd, rs1, rs2`], [`SHIFT[W]`], [`[W]`], [1], [`invert`], [@decode:note:word_instr]), // OP - M - ([`MUL[W] rd, rs1, rs2`], [`MUL`], [`[W]`], [1], [`signed2`], [#ref_note()]), + ([`MUL[W] rd, rs1, rs2`], [`MUL`], [`[W]`], [1], [`signed2`], [@decode:note:word_instr]), ([`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(, )]), - ([`REM[U][W] rd, rs1, rs2`], [`DIVREM`], [`[W]`], [#sym.not`[U]`], [`muldiv_selector`], [#ref_note(, )]), + ([`DIV[U][W] rd, rs1, rs2`], [`DIVREM`], [`[W]`], [#sym.not`[U]`], [], [@decode:note:word_instr@decode:note:signed]), + ([`REM[U][W] rd, rs1, rs2`], [`DIVREM`], [`[W]`], [#sym.not`[U]`], [`muldiv_selector`], [@decode:note:word_instr@decode:note:signed]), // LUI/AUIPC - ([`LUI rd, imm`], [`ADD`], [], [], [], [#ref_note()]), - ([`AUIPC rd, imm`], [`ADD`], [], [], [`rs1 := x255`], [#ref_note()]), - ([`JAL rd, imm`], [], [], [], [`BRANCH`, `JALR`, `rs1 := x255`], [#ref_note()]), + ([`LUI rd, imm`], [`ADD`], [], [], [], [@decode:note:lui]), + ([`AUIPC rd, imm`], [`ADD`], [], [], [`rs1 := x255`], [@decode:note:auipc]), + ([`JAL rd, imm`], [], [], [], [`BRANCH`, `JALR`, `rs1 := x255`], [@decode:note:jal]), // Branching ([`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()]), + ([`BLT[U] rs1, rs2, imm`], [`LT`], [], [#sym.not`[U]`], [`BRANCH`], [@decode:note:signed]), + ([`BGE[U] rs1, rs2, imm`], [`LT`], [], [#sym.not`[U]`], [`BRANCH`, `invert`], [@decode:note:signed]), // 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()]), - ([`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()]), + ([`LW[U] rd, rs1, imm`], [`ADD`], [], [], [`MEMORY`, `mem_signed := `#sym.not`[U]`, `mem_4B`], [@decode:note:signed]), + ([`LH[U] rd, rs1, imm`], [`ADD`], [], [], [`MEMORY`, `mem_signed := `#sym.not`[U]`, `mem_2B`], [@decode:note:signed]), + ([`LB[U] rd, rs1, imm`], [`ADD`], [], [], [`MEMORY`, `mem_signed := `#sym.not`[U]`], [@decode:note:signed]), // 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()]), + ([`ECALL`], [], [], [], [`ECALL`, $#`rs1` := #`x17`$], [@decode:note:ecall]), // FENCE - ([`FENCE`], [`ADD`], [], [], [], [#ref_note()]), + ([`FENCE`], [`ADD`], [], [], [], [@decode:note:fence]), ) #decoding_table(decoding) @@ -172,63 +167,21 @@ It is represented as half the number of bytes in the instruction to make misalig 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` -#let referenceable_note(lbl, note) = { - show figure: (it) => align(left, [#it]) - [#figure(kind: "note", supplement: [], [#note]) #label(lbl)] -} - == Notes We note the following about the above decoding table: -#enum(numbering: "[1]", - 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. Similarly, `SHIFT[W]` indicates the `SHIFTW` operation for the `W`-variant, and `SHIFT` otherwise.] - ) - ), - enum.item( - referenceable_note( - "note_signed", - [`signed`: #sym.not`[U]` indicates that $#`signed` = 1$ for the *non-`U`*-variant of the operation, and $0$ for the `U`-variant.] - ) - ), - enum.item( - referenceable_note( - "note-lui", - [`LUI`: this operation loads the 20-bit `imm` in the upper bits of `rd`. +#notelist("decode")[ + / word_instr: `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. + / signed: `signed`: #sym.not`[U]` indicates that $#`signed` = 1$ for the *non-`U`*-variant of the operation, and $0$ for the `U`-variant. + / lui: `LUI`: this operation loads the 20-bit `imm` in the upper bits of `rd`. Observe that this can be represented using `ADDI rd, x0, imm`. - As such, *we expect the decoding to take care of writing the immediate in bit range $[12:32]$ of `imm` and extending it to 64 bits.*] - ) - ), - enum.item( - referenceable_note( - "note-auipc", - [`AUIPC`: this operation adds the 20-bit immediate to the upper bits of `pc` and stores the result in `rd`. + As such, *we expect the decoding to take care of writing the immediate in bit range $[12:32]$ of `imm` and extending it to 64 bits.* + / auipc: `AUIPC`: this operation adds the 20-bit immediate to the upper bits of `pc` and stores the result in `rd`. Given that the `pc` is stored in `x255`, this operation can be represented using `ADDI rd, x255, imm`. - As such, *we expect the decoding to take care of writing the immediate in bit range $[12:32]$ of `imm` and extending it to 64 bits.*] - ) - ), - enum.item( - referenceable_note( - "note-jal", - [`JAL`: this operation stores $#`pc` + #`2 * half_instruction_length`$ in `rd` and adds two times the sign-extended 20-bit immediate to the `pc`. + As such, *we expect the decoding to take care of writing the immediate in bit range $[12:32]$ of `imm` and extending it to 64 bits.* + / jal: `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.*] - ) - ), - enum.item( - referenceable_note( - "note-ecall", - [`ECALL`: + 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.* + / ecall: `ECALL`: "On RISC-V a system call has its own instruction: `ECALL`. [...] A7 [= register `x17`] contains the system call number." #link("https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[[source]] - ] - ) - ), - enum.item( - referenceable_note( - "note-fence", - [`FENCE`: currently, the VM interprets this operation as `ADDI x0 x0 0`; a no-op.] - ) - ) -) + / fence: `FENCE`: currently, the VM interprets this operation as `ADDI x0 x0 0`; a no-op. +] diff --git a/spec/chapters/ecsm.typ b/spec/chapters/ecsm.typ index 210c418ac..de25c04a6 100644 --- a/spec/chapters/ecsm.typ +++ b/spec/chapters/ecsm.typ @@ -12,8 +12,6 @@ #let config = load_config() -#show math.equation.where(block: false): box - #let ecsm_chip = load_chip("src/ecsm.toml", config) #let ecsm = raw(ecsm_chip.name) diff --git a/spec/chapters/field.typ b/spec/chapters/field.typ deleted file mode 100644 index 1333ed77b..000000000 --- a/spec/chapters/field.typ +++ /dev/null @@ -1 +0,0 @@ -TODO diff --git a/spec/chapters/field_decode.typ b/spec/chapters/field_decode.typ deleted file mode 100644 index 6921ceac3..000000000 --- a/spec/chapters/field_decode.typ +++ /dev/null @@ -1,2 +0,0 @@ - -TODO diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ new file mode 100644 index 000000000..55e106aad --- /dev/null +++ b/spec/chapters/field_vm.typ @@ -0,0 +1,357 @@ +#import "/meta.typ": aside, notelist +#import "/src.typ": load_config, load_chip +#import "/chip.typ": render_chip_variable_table, total_nr_variables, total_nr_instantiated_columns, compute_nr_interactions, render_constraint_table, render_chip_padding_table +#import "/expr.typ": expr_to_math + +#let next(x) = expr_to_math(("next", x)) + +This chapter describes, in line with the split between a binary and a field VM from @recursion, +the ISA and an arithmetization of a dedicated field VM. +The ISA is centered around a single, versatile instruction, that can handle both +extension field arithmetic and program flow. + += ISA + +The field VM is a machine that has access to a read-only memory `MEM`, modeled as a flat array +that can be indexed by base field elements. +This `MEM` can be implemented as a committed table containing the memory as well as the multiplicities for +the number of times each cell was accessed. +As additional memory, the VM has a set of $N + 2$ mutable registers that are not part of the `MEM` array. + +The central instruction of the ISA is a constraint for a fused multiply-add over the extension field: +`FMA d == a * b + c`. +Here all of `d`, `a`, `b` and `c` are arguments following the addressing scheme described below. + +This constraint-based view generally goes well with a read-only memory. +The memory system gives us the guarantee that whenever we access `MEM` at the same index, +we get the same value back, and the constraint allows us to enforce that these +values in memory are consistent with the structure we want it to have.#footnote[ + In the most central application of the VM, we check that the memory consists of a correct proof + and any auxiliary data needed for this verification. +] +For the mutable registers, however, this approach is insufficient, as the instruction does not have +a way to actually mutate a register. +We deal with this through a system we call _register hinting_ --- which can be further distinguished +into _input hinting_ and _output hinting_ --- described further below. + + +== Arguments and addressing + +The execution of a guest program can be seen as a succession of _states_ of the machine. +A state is then the tuple of all values the registers have at a given point in time during the execution.#footnote[ + If we consider states across different executions, the contents of `MEM` should also be considered part of the state. +] +Each instruction acts upon the _current state_ to produce the _future state_.#footnote[ + And since the program counter is part of the current state, + each possible state has at most one associated instruction. +] +Or rather --- since instructions are constraints --- each instruction constrains +a correct transition from the current state to the future state. +We write $next("x")$ for the register `x` in the future state, both in prose and later in the constraints. + +The $N + 2$ registers making up a state of the VM are: +a `ZERO` bit-register, the base field `PC` register and $N$ general purpose extension field registers. +The number of registers was chosen as a tradeoff between the versatility of having more mutable state, +and the extra cost in committed columns and decoding logic that grows with $N$. +We index the registers from $0$ to $N + 1$ in the order above, so `ZERO` gets index $0$, +`PC` gets index $1$ and then follow $N$ general purpose registers with indices $2...N+1$. + +The `ZERO` register indicates whether the previous instruction had a zero result, +i.e. $next("ZERO") <=> #`d` = 0$. +The `PC` register stores the program counter: the address of the current instruction. +It is generally incremented by $1$ for every consecutive state, +except for when handling a branching instruction (that output-hints the `PC` register). +As the name implies, the general purpose registers are available for arbitrary usage. + +Each argument to the `FMA` constraint has either of the two following composite forms, which we call addressing modes: +- $#`imm`_0 dot #`reg` + #`imm`_1$ +- $#`MEM[`#`imm`_0 dot #`reg` + #`imm`_1#`]`$ +where each immediate is a base field element, encoded in the instruction for a specific argument. +The `d` argument to the instruction obtains its register value from the future state. + +== Register hinting + +By default, a general-purpose register will have the same value across two consecutive states. +To change register values, each general-purpose register in the current state +can be marked as _hinted_ by the acting instruction. +This means that the register receives a new value in the current state, which it will keep +until the register is hinted again. +The new value is independent from the previous value or state, +except as constrained by the instruction. +Additionally, the _output_ can be marked as hinted, meaning that the register used in the `d` argument +will change in the future state, as such impacting the value of the `d` argument. +This applies to the _register_ of the `d` argument, regardless of the additional immediates and `MEM[]` +access that may happen in the instruction. +We distinguish between these two types by naming them respectively _input hinting_ and _output hinting_. + +The clearest use of output hinting is to enable the `FMA` instruction to perform computation. +If, for instance, $#`d` = 1 dot #`reg` + 0$, then we can interpret the instruction +as computing $#`a` dot #`b` + #`c`$ and assigning the result to $next("reg")$. +Performing the hint only in the future state ensures that the original value of `reg` remains +available throughout the computation. +Additionally, output hinting allows for `PC` to be hinted,#footnote[ + Note that we disallow this in input hinting, as it would allow for instructions + that can effectively hijack program execution. +] enabling causal jumps and control flow in the program. + +In contrast, input hinting does not look like any traditional model of execution, +instead allowing to update one or more values in the state, as long as the resulting state still satisfies +the `FMA` constraint. +This can, e.g., be used to compute field inverses and square roots, which have a degree-2 constraint +on the result. +There may even be situations where hinting multiple values can be chosen simultaneously, such as a decomposition +$a = b + c$ in a divide-and-conquer algorithm. +Even hinting registers that are not used in the current instruction may prove useful in limited situations. +Though we approach it differently in @field-VM:sec:calling, one can imagine a calling convention +where the frame pointer is updated directly during the jump instruction, without being further involved +in the computation of the next `PC`. + +Any register that is not output hinted in the current instruction nor input hinted in the future instruction +will have the same value in the future state as in the current state, +with the appropriate exceptions in behaviour for the `ZERO` and `PC` registers. +More example uses of register hinting can be found below in our suggested pseudoinstructions. + +#aside("Hint collisions")[ +One may observe that an output hint for state `i` and an input hint on state `i + 1` can affect +the same register in a single state. +While this is true in theory, it is not a problem in practice, as two successive states are, +in almost all cases, operated on by two consecutive --- in the program text --- instructions. +As such, hinting collisions can be easily identified, and most actual programs +should have no reason to have hinting collisions. +The most likely practical collision scenario would be that instruction `i` does not +output-hint, but instruction `i + 1` input-hints the output register of state `i`. +This would lead to confusing behaviour on instruction `i`, as it may not be operating on the output +value a programmer would assume it to be. +As input hints are likely to occur only seldom, we advise extra care for the surrounding +instructions of any input-hinting instruction. + +The only case in which two consecutive states are not operated on by two consecutive instructions +is when a jump occurs, which necessarily implies that `PC` was output-hinted in the earlier instruction. +`PC` can, however, not be input-hinted, so no collision is possible there. +] + +== Instruction notation + +A potential way to write down an FMA instruction would be the following: +``` +FMA [1 * X + 2] == [3 * Y + 4] * (5 * Z) + [W + 6], hint out + Z +``` + +- `[]` indicate memory access +- `()` indicate grouping to separate the arguments +- `X, Y, Z, W` are placeholder register names +- `hint` notation indicates which registers are hinted (default unhinted), `hint out` means hinting `d` as above + +We note that this may be insufficient for the execution/prover side of the program, +as this provides no information on _which_ value exactly should be hinted, +but leave this as an implementation detail to be decided upon based on practical experience. + +We label the instruction with an `FMA` mnemonic --- even though that is the only possible "real" instruction --- +to allow program listings to include other mnemonics to indicate pseudoinstructions that +map more specialized semantics onto the FMA functionality. +Next, we suggest some potential pseudoinstructions along with their translation. +This list is meant as an example, rather than an exhaustive enumeration; +implementers and practitioners are encouraged to discover and use their own, +as experience may point out further useful abstractions. + +#table(columns: (auto, 2fr, 1fr), + stroke: 0pt, + inset: (right: .5em), + table.header[*Pseudoinstr.*][*Translation*][*Comment*], table.hline(stroke: 1.5pt))[ + `ADD d, a, b`][`FMA d == (0 * X + 1) * a + b, hint out` ][Addition + @field-VM:note:fullarg][ + `MUL d, a, b`][`FMA d == a * b + (0), hint out` ][Multiplication + @field-VM:note:fullarg][ + `INV d, a` ][`FMA d == (a + 1) * d + (-1), hint ` ][Extension field inversion + @field-VM:note:fullarg@field-VM:note:imm_mod@field-VM:note:inv][ + `J a` ][`FMA PC == a, hint out` ][Jump + @field-VM:note:fullarg@field-VM:note:pcrel][ + `JZA imm` ][`FMA PC == (ZERO)*(-1 * PC + (imm-1)) + (PC + 1), hint out`][Jump if ZERO, absolute target address + @field-VM:note:immarg][ + `JZR a` ][`FMA PC == (ZERO) * (a - 1) + (PC + 1), hint out` ][Jump if ZERO, PC-relative target address + @field-VM:note:fullarg@field-VM:note:imm_mod][ + `JNZA imm` ][`FMA PC == ZERO * (PC + (-imm)) + (ZERO + imm), hint out` ][Jump if not ZERO, absolute target address + @field-VM:note:immarg][ + `JNZR a` ][`FMA PC == (a - 1) * (-1 * ZERO + 1) + (PC + 1), hint out` ][Jump if not ZERO, PC-relative target address + @field-VM:note:fullarg@field-VM:note:imm_mod] + +#notelist("field-VM")[ + / fullarg: The `a`, `b` and `d` arguments are complete arguments that can take the form of any addressing mode + / immarg: The `imm` argument is a single base field immediate value. If operated on in the translation (e.g. `(imm-1)`), the resulting value should instead be used for the translated version. + / imm_mod: For arguments with an extra immediate in the translation, the immediates of the original form should be appropriately adapted, and the argument can no longer use a memory addressing mode. + / inv: Since `d` gets input-hinted, `a` and `d` should use distinct registers. + / pcrel: The jump may be relative to `PC`, depending on the register used in the arguments. +] + +Eventually, usage may inform a set of common pseudoinstructions, +along with informing potential optimizations that remove unused capabilities +(e.g. reducing the number of immediates involved). + +== Calling convention + +Since the VM makes use of read-only memory, traditional usage of a program stack does not work. +We assume that each function invocation (unless other optimizations apply) will have an associated _frame_, +pointed to by a _frame pointer_ `fp`. +We assume here that one of the general-purpose registers takes the role of `fp`. +In this frame, the following data is stored: + +/ `MEM[fp - k]...MEM[fp - 1]`: `k` saved registers from the calling function +/ `MEM[fp + 0]`: The stored parent frame pointer +/ `MEM[fp + 1]`: The return address +/ `MEM[fp + 2]...MEM[fp + l]`: Additional information required by the function + +Observe that we let `fp` point into the middle of the frame, such that the information relevant to the callee +starts at offset 0. + +Then, to facilitate function calls, we describe a possible implementation of the `CALL` and `RET` pseudoinstructions, that, respectively, perform a new function call and return back to the caller. + +``` +CALL target: + FMA [fp] == fp, hint out // Hint a new frame address, store the old fp + FMA [fp - i] == STORED_REG_i // Store on the caller side of the frame + FMA [fp + 1] == (PC + 2) // Store the return address to the frame + FMA PC == target, hint out // Hint the PC to jump + // Returning jumps here + FMA fp == [fp], hint out // Hint the old frame pointer to restore it + +RET: + FMA PC == [fp + 1], hint out // Hint the PC to jump to the stored + // return address +``` + +As a halting state, we choose to let the VM loop to itself at `PC = 0`, hinting all inputs. +That means the decoding will always contain `FMA PC == PC, hint out, hint 2, ..., hint (N + 1)` at that address. +For technical reasons, in @field-VM:sec:boundary, execution of the VM starts at `PC = 1`, with `FMA 0 = 0` and no hinting. + += Arithmetization + +#let config = load_config() +#let chip = load_chip("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/src/field_vm.toml", config) +#let fieldvm = raw(chip.name) + +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) +#let nr_interactions = compute_nr_interactions(chip) + +The #fieldvm is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): + +== Variables +#render_chip_variable_table(chip, config) + +== Constraints + +First, we compute all values $#`imm`_0 dot #`reg` + #`imm`_1$, +where we need to multiplex out of `registers`, based on `argument_registers[i]`. +We do this by constructing the Lagrange basis polynomials $f_(i)(x)$ such that $f_(i)(j) = 1$ +for $i = j in [0, N + 1]$ and $f_(i)(j) = 0$ for $i != j in [0, N + 1]$.#footnote[ + Note that we allow ourselves to multiplex $N + 2$ registers here, + combining the $N$ general purpose registers, the PC and the `ZERO` register. +] +Since the degree of these $f_(i)(x)$ can grow too large to express in a single polynomial constraint, +we perform a _"degree split"_: +$ f_(i)(x) &= f_(i, 0)(x) + x^(d - 1) (f_(i, 1)(x) + x^(d - 2) (f_(i, 2) + x^(d - 2) (f_(i, 3) + ...)))\ + &= 1 dot f_(i,0)(x) + x^(d - 1) f_(i,1)(x) + ... + x^(d - 1 + (t - 1) dot (d - 2)) f_(i, t)(x), $ +for a maximal constraint degree $d$. +Here, $deg(f_(i, 0)) <= d - 2$ and $deg(f_(i, k)) <= d - 3$. +We denote by $t + 1$ the number of non-zero $f_(i, k)$ for fixed $i$. +This allows us to first compute the values of +$#`argument_registers[i]`^(d - 1)$, $#`argument_registers[i]`^(2d - 3)$ and so on +to `arg_register_powers` with constraints of degree $<= d$, +and then compute +$ + #`args_premem[i]` &= #`argument_scalars[i]` dot sum_(j = 0)^(N + 1) #`registers[j]` dot f_(j)(#`argument_registers[i]`)\ + &+ #`argument_offsets[i]`. +$ +The coefficients for all $f_(i, k)$ are pre-computed once, based on the choices of $N$, $d$ and $t$, +and used through the `MUX` constant columns. +In this way, $f_(i, 0)$ can have degree at most $d - 2$, as it gets multiplied with $#`imm`_0$ and the register value, +and the other $f_(i, k)$ can have degree at most $d - 3$, as they also get multiplied with the appropriate power of $x$. +This leads to a total degree of $deg(f_(i)) = d - 1 + t dot (d - 2) - 1$ for a maximal number of registers $N + 2 <= deg(f_(i)) + 1$. +Hence, for a fixed choice of $d$ and $t$, this scheme can support up to $N <= (t + 1) dot (d - 2) - 1$ general purpose registers. +Currently, the parametrization is set to be $(d, N, t) = (5, 5, 1)$. + +While @field-VM:c:first-mux, and the other constraints using this multiplexing technique, look like they have +a total degree of $d + 1$, this is purely a syntactical matter. +Due to our choices to set `arg_register_powers[0] = 1` and `MUX[j][k][d - 2] = 0` for $k != 0$ (by construction of the $f_(j,k)$ polynomials), we stay at a total degree $d$. +Also observe that the handling for `argument_registers[0]` is separated as @field-VM:c:out-mux, +as this represents the output argument, which should take its values from the next row in the table. + +#render_constraint_table(chip, config, groups: "mux") + +Once we have these values, we can then perform an optional indexing into memory, and copy over the values otherwise. +The cast of the `ExtField` value into `BaseField` is mostly technical here, as a means to make the signature look reasonable. +Verification should fail if the value does not fit. +This failure is automatically satisfied by keeping the `ExtField` value as-is, since the `BaseField` would get reinterpreted as `ExtField` +in the LogUp, and the memory table should only provide `BaseField` addresses. + +#render_constraint_table(chip, config, groups: "memory") + +Now everything is in place to check the core operation of the VM: the FMA constraint. + +#render_constraint_table(chip, config, groups: "fma") + +We must ensure the consistency between consecutive rows of the table, and allow for hinting. +We again make use of the multiplexing machinery from before. +The constraints we want to enforce on a register index $r$ are as follows: +- $!next("hint_input")_r and !#`hint_output` => next("registers")_r = #`registers`_r$,\ `r` could not have been hinted, + since it was not input-hinted in the next row, and there was no output hint, so $next("r")$ should remain the same. +- $!next("hint_input")_r and f_(r)(#`argument_registers`_0) = 0 => next("registers")_r = #`registers`_r$,\ + `r` was not input-hinted in the next row, and it was not the output register, so it once again stays the same. + +Together, these constraints are logically equivalent to $!next("hint_input")_r and not (#`hint_output` and f_(r)(#`argument_registers`_0) = 1) => next("registers")_r = #`registers`_r$, but expressed in a way that polynomial constraints can more easily handle. + +Naturally, the `PC` and `ZERO` registers are exceptions since we need $next("pc") = #`pc` + 1$ if it is not (output-)hinted, +and $next("ZERO")$ purely depends on $#`args`_0$ and not on `ZERO`. + +#render_constraint_table(chip, config, groups: "transition") + +Finally, to decode the instruction at the current PC, we would like to compress the information coming from +the decoding table to reduce its number of columns. +Doing so would require the elements being combined into one column to be range checked on this side +of the interaction, ideally without needing any extra interactions or committed columns. +For `Bit` variables, this is no problem with the `IS_BIT` template from @isbit. +For `argument_registers` however, which should be in the range $[0, N + 1]$, +a first attempt to range-check with a constraint of degree $<= d$ fails. +The standard way to construct the range-check polynomial $g$ would be to choose +$ g(x) = (x - 0) dot (x - 1) dot ... dot (x - (N + 1)), $ +which has degree $N + 2$. +Our polynomial approach to multiplexing already provides a way to evaluate a polynomial of degree $<= N + 1$, +which falls short of one coefficient to evaluate $g$. +However, recall that $deg(f_(i,t)) <= d - 2$, and unlike in multiplexing, +$g$ needs no further multiplications to be used in an arithmetic constraint. +So we can simply add one extra coefficient to the last split polynomial to achieve our goal.#footnote[ + We can in theory choose any of the split polynomials to increase, but we need to ensure + that we can still use the same `arg_register_powers` as before to recombine the results, + so as to avoid the need for extra columns. +] +In the constraints, we write `RANGE` for the coefficients of $g$, in a similar structure to `MUX[r]`. +We assume $N <= 254$, such that each register index takes up at most 8 bits in the compressed column. + +To compress base field columns, we can batch 3 base field columns as coefficients of an extension field element. +In order to do so, we write the constant column `X` as the extension field element, such that $(1, #`X`, #`X`^2)$ +is the canonical basis of the extension field over the base field. + +#render_constraint_table(chip, config, groups: "decode") + +== Boundary constraints + +Besides enforcing the FMA constraints and the correct transitions between states, we also need to ensure that execution +starts at the correct instruction and ends with a halting instruction. +This means that the verifier must check that the first row of the table corresponds to a state at `PC = 1` and all other variables set to $0$; +as well as that the last row of the table corresponds to the halt/padding state. +This is also why the halt state has all inputs hinted, so that all registers can be set to zero and be known. + +== Padding + +The halting self-loop also functions as a padding state. + +#render_chip_padding_table(chip, config) + += Notes and potential optimizations + +- Depending on observed use, in the future, we can restrict this design in some potential ways, to make proving it faster, without sacrificing too much utility: + - We can restrict the amount or targets of hinting allowed + - We can reduce the places in which immediates are valid + - We can reduce for which arguments a memory access can be specified + - Do we need input hinting per register, or can we reduce things to input hinting for (some of) the used registers only +- Since memory accesses can probably be presumed to have `BaseField` indices, we may be able to reduce area/hashing somewhat by working with the overlap of `args_premem` and `args` diff --git a/spec/chapters/field_vm_decode.typ b/spec/chapters/field_vm_decode.typ new file mode 100644 index 000000000..0dfb91c18 --- /dev/null +++ b/spec/chapters/field_vm_decode.typ @@ -0,0 +1,24 @@ +#import "/src.typ": load_config, load_chip +#import "/chip.typ": render_chip_variable_table, render_constraint_table +#let config = load_config() +#let chip = load_chip("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/src/field_vm_decode.toml", config) +#let decode = raw(chip.name) + +In this chapter, we provide a brief overview of the #decode chip, +that corresponds to the instruction decoding for @field-VM. +As the ISA from @field-VM:sec:isa was designed to have a simple mapping +onto AIR tables, the decoding table is itself also simple. + +We present the table in its uncompressed form, but in practice, any +implementation would materialize the _virtual_ and _multiplicity_ columns only, +similar to the approach in @decode. +Due to its relative simplicity, we do not present both compressed and uncompressed +variants of the table separately. + += Variables + +#render_chip_variable_table(chip, config) + += Constraints + +#render_constraint_table(chip, config) diff --git a/spec/chapters/limbs_and_carries.typ b/spec/chapters/limbs_and_carries.typ index e31861066..353dcd144 100644 --- a/spec/chapters/limbs_and_carries.typ +++ b/spec/chapters/limbs_and_carries.typ @@ -4,7 +4,6 @@ // Equation formatting #show: equate.with(breakable: true, sub-numbering: true, number-mode: "label") #set math.equation(numbering: "(1.1)") -#show math.equation.where(block: false): box In this section, we discuss, in order, + the multiplication and addition of limb-decomposed integers (involving carries), diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index 481d6733a..92d0941e9 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -26,8 +26,6 @@ #let prob = $PP$ #let to = math.arrow.r -#show math.equation.where(block: false): box - #set list(marker: [---]) = Proof recursion diff --git a/spec/expr.typ b/spec/expr.typ index 16ac94867..f3c70733c 100644 --- a/spec/expr.typ +++ b/spec/expr.typ @@ -46,6 +46,7 @@ // | ["-", expr] ; -expr // | ["-", expr1, expr2, ...] ; expr1 - expr2 - ... // | ["cast", expr, type] ; expr as type +// | ["next", var] ; var' // // // To limit the number of parentheses that are placed in an expression, @@ -54,19 +55,20 @@ #let PREC = ( "MIN": -1, // - "idx": 0, // [] - "pow": 1, // ^ - "neg": 2, // Unary - - "cast": 3, // cast - "mul": 4, // * - "div": 5, // / - "mod": 6, // mod - "sum": 7, // Σ - "not": 8, // not - "sub": 9, // - - "add": 10, // + - "eq": 11, // = and := - "MAX": 12, // + "next": 0, // var' + "idx": 1, // [] + "pow": 2, // ^ + "neg": 3, // Unary - + "cast": 4, // cast + "mul": 5, // * + "div": 6, // / + "mod": 7, // mod + "sum": 8, // Σ + "not": 9, // not + "sub": 10, // - + "add": 11, // + + "eq": 12, // = and := + "MAX": 13, // ) // Mutual recursion through a trick from https://github.com/typst/typst/issues/744 @@ -114,7 +116,7 @@ `⧼` + 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)) + `]`, + "idx": (pp, rec, e) => cwrap(rec(PREC.idx, e.at(1)) + `[` + rec(PREC.MAX, e.at(2)) + `]`, pp < PREC.idx), "not": (pp, rec, e) => cwrap(rec(PREC.not, 1) + ` - ` + rec(PREC.not, e.at(1)), pp < PREC.not), "+": (pp, rec, e) => cwrap(e.slice(1).map(rec.with(PREC.add)).join(` + `), pp < PREC.add), "sum": (pp, rec, e) => assert(false, message: "sum is unsupported in code."), @@ -136,9 +138,8 @@ }, "/": (pp, rec, e) => cwrap(rec(PREC.div, e.at(1)), pp < PREC.div) + ` / ` + rec(PREC.div, e.at(2)), "^": (pp, rec, e) => { - assert(type(e.at(1)) == int and type(e.at(2)) == int, message: "Can only exponentiate constants") - // technically wrong associativity, but it's a constant - rec(PREC.pow, e.at(1)) + `^` + rec(PREC.pow, e.at(2)) + // `<=` in the wrap to deal with right associativity + cwrap(rec(PREC.pow, e.at(1)) + `^` + rec(PREC.pow, e.at(2)), pp <= PREC.pow) }, "=": (pp, rec, e) => rec(PREC.eq, e.at(1)) + ` = ` + rec(PREC.eq, e.at(2)), ":=": (pp, rec, e) => rec(PREC.eq, e.at(1)) + ` := ` + rec(PREC.eq, e.at(2)), @@ -155,6 +156,10 @@ assert(e.len() == 3, message: "Invalid type cast: " + repr(e)) cwrap(rec(PREC.cast, e.at(1)) + ` as ` + type_to_code(e.at(2)), pp < PREC.cast) }, + "next": (pp, rec, e) => { + assert(e.len() == 2 and type(e.at(1)) == str, message: "Invalid transition variable: " + repr(e)) + cwrap(rec(PREC.next, e.at(1)) + `'`, pp < PREC.next) + }, ), num: (n) => raw(str(n)), flatten: flatten_code @@ -217,8 +222,7 @@ }, "/": (pp, rec, e) => $#rec(PREC.div, e.at(1)) / #rec(PREC.div, e.at(2))$, "^": (pp, rec, e) => { - assert(type(e.at(1)) == int, message: "Can only exponentiate constants") - $#e.at(1)^#rec(PREC.MAX, e.at(2))$ + mwrap($#rec(PREC.pow, e.at(1))^#rec(PREC.MAX, e.at(2))$, pp <= PREC.pow) }, "=": (pp, rec, e) => $#rec(PREC.eq, e.at(1)) = #rec(PREC.eq, e.at(2))$, ":=": (pp, rec, e) => $#rec(PREC.eq, e.at(1)) := #rec(PREC.eq, e.at(2))$, @@ -236,7 +240,11 @@ }, "cast": (pp, rec, e) => { assert(e.len() == 3, message: "Invalid type cast: " + repr(e)) - cwrap($#rec(PREC.cast, e.at(1)) colon.double #type_to_math(e.at(2))$, pp < PREC.cast) + mwrap($#rec(PREC.cast, e.at(1)) colon.double #type_to_math(e.at(2))$, pp < PREC.cast) + }, + "next": (pp, rec, e) => { + assert(e.len() == 2 and type(e.at(1)) == str, message: "Invalid transition variable: " + repr(e)) + mwrap($#rec(PREC.next, e.at(1))'$, pp < PREC.next) }, ), var: v => if v.len() == 1 { $#v$ } else { $#raw(v)$ }, diff --git a/spec/meta.typ b/spec/meta.typ index eea8f6e4a..f0995bc8a 100644 --- a/spec/meta.typ +++ b/spec/meta.typ @@ -55,8 +55,8 @@ )), ("RECURSION", ( ("recursion", [Recursive verification], ), - ("field", [`Field` VM], ), - ("field_decode", [`Field` `DECODE` table], ), + ("field_vm", [Field VM], ), + ("field_vm_decode", [Field `DECODE` table], ), )), ("MATHEMATICS", ( ("limbs_and_carries", [On limb decomposition and carries], ), @@ -102,10 +102,37 @@ assert(false, message: "Unsupported target: " + target()) } +#let notelist(prefix, body) = { + show list: it => context if target() == "html" { + html.div(class: "notelist", it) + } else { + it + } + show figure.where(kind: "note"): it => super(it.counter.display(it.numbering)) + it + show terms: it => list(marker: none, indent: 0pt, ..it.children.map(c => { + let labelname = if c.term.has("text") { + c.term.text + } else { + c.term.children.map(x => x.text).join() + } + list.item[ + #box[#figure(numbering: "[1]", kind: "note", supplement: [], none)#label(prefix + ":note:" + labelname)] + #c.description + ] + })) + body +} + #let common-formatting(body) = { set footnote(numbering: "[1]") show raw.where(block: true): it => block(it, inset: 1em, width: 100%, radius: 5pt) + show math.equation.where(block: false): box // Don't line-break inline equations by default show ref: equate.with(sub-numbering: true, breakable: true, number-mode: "label") + show ref: it => if it.element != none and it.element.func() == figure and it.element.kind == "note" { + super[[#it]] + } else { + it + } show selector.or(..highlights.keys().map(k => figure.where(kind: k))): it => { set figure.caption(position: top) show figure.caption: cap => block( diff --git a/spec/src/config.toml b/spec/src/config.toml index abb671815..a4816f2b0 100644 --- a/spec/src/config.toml +++ b/spec/src/config.toml @@ -7,6 +7,11 @@ subtypes = ["BaseField"] range = [0, "18446744069414584320"] desc = "Variable that can assume any value in the base field." +[[variables.types]] +label = "ExtField" +subtypes = ["ExtField"] +desc = "Variables that can assume any value in the extension field." + [[variables.types]] label = "Bit" subtypes = ["BaseField"] diff --git a/spec/src/field_vm.toml b/spec/src/field_vm.toml new file mode 100644 index 000000000..1a9188b45 --- /dev/null +++ b/spec/src/field_vm.toml @@ -0,0 +1,295 @@ +name = "FIELD_VM" +code = "FVM" + +[[variables.input]] +name = "pc" +type = "BaseField" +desc = "The program counter" +pad = 0 + +[[variables.input]] +name = "argument_registers" +type = ["BaseField", 4] +desc = "The register numbers of the arguments `d`, `a`, `b`, `c`, in that order" +pad = ["arr", 1, 0, 0, 1] + +[[variables.input]] +name = "argument_scalars" +type = ["BaseField", 4] +desc = "The `imm_0` scalars for the arguments `d`, `a`, `b`, `c`, in that order" +pad = ["arr", 1, 0, 0, 1] + +[[variables.input]] +name = "argument_offsets" +type = ["BaseField", 4] +desc = "The `imm_1` offsets for the arguments `d`, `a`, `b`, `c`, in that order" +pad = 0 + +[[variables.input]] +name = "mem_flags" +type = ["Bit", 4] +desc = "Whether the argument (`d`, `a`, `b`, `c`, in that order) comes from a memory lookup" +pad = 0 + +[[variables.input]] +name = "hint_input" +type = ["Bit", 5] # PARAM: ["Bit", N] +desc = "Whether each general purpose register is input hinted this cycle" +pad = ["arr", 1, 1, 1, 1, 1] # PARAM: N long + +[[variables.input]] +name = "hint_output" +type = "Bit" +desc = "Whether the output register is hinted this cycle" +pad = 1 + +[[variables.auxiliary]] +name = "registers" +type = ["ExtField", 5] # PARAM: ["ExtField", N] +desc = "The general purpose registers" +pad = 0 + +[[variables.auxiliary]] +name = "ZERO" +type = "Bit" +desc = "Whether the output of the previous instruction was zero" +pad = 1 + +[[variables.auxiliary]] +name = "out_inverse" +type = "ExtField" +desc = "The multiplicative inverse of the output, used to check `ZERO`" +pad = 0 + +[[variables.auxiliary]] +name = "arg_reg_pows_computed" +type = [["BaseField", 1], 4] # PARAM: [["BaseField", T], 4] +desc = "Powers of the argument register indices to split the MUX polynomials into lower degree parts" +pad = ["arr", 1, 0, 0, 1] + +[[variables.auxiliary]] +name = "args_premem" +type = ["ExtField", 4] +desc = "The argument values, before a potential memory lookup" +pad = 0 + +[[variables.auxiliary]] +name = "args" +type = ["ExtField", 4] +desc = "The argument values, after a potential memory lookup" +pad = 0 + +[[variables.virtual]] +name = "all_regs" +type = ["ExtField", 7] # PARAM: ["ExtField", N + 2] +desc = "All registers, in register index order" +def = {polys = [ + {iter = ["i", 0], poly = ["cast", "ZERO", "ExtField"]}, + {iter = ["i", 1], poly = ["cast", "pc", "ExtField"]}, + {iter = ["i", 2, 6], poly = ["idx", "registers", ["-", "i", 2]]}, # PARAM: iter = ["i", 2, N + 1] +]} + +[[variables.virtual]] +name = "arg_register_powers" +type = [["BaseField", 2], 4] # PARAM: [["BaseField", T + 1], 4] +desc = "A virtual wrapper around `arg_reg_pows_computed` to have a 1 at index 0" +def = {polys = [ + {iters = [["i", 0, 3], ["j", 0]], poly = 1}, + {iters = [["i", 0, 3], ["j", 1, 1]], poly = ["idx", ["idx", "arg_reg_pows_computed", "i"], ["-", "j", 1]]} # PARAM: iters = ["i", 0, 3], ["j", 1, T]] + ]} + +[[variables.constant]] +name = "MUX" +type = [[["BaseField", 4], 2], 7] # PARAM: [[["BaseField", d - 1], t + 1], N + 2] +desc = "The MUX polynomial coefficients" +pad = ["arr", 1, 1, 1, 1, 1, 1, 1] # Slightly hacky way to make the typechecker not crash out on the pc constraint + +[[variables.constant]] +name = "RANGE" +type = [["BaseField", 5], 2] # PARAM: [["BaseField", d], t + 1] +desc = "The RANGE polynomial coefficients, to range-check register indices" +pad = 0 + +[[variables.constant]] +name = "X" +type = "ExtField" +desc = "A primitive element of the extension field, such that $(1, #`X`, #`X`^2)$ is a basis for the extension field over the base field" +pad = 0 + +[[constraint_groups]] +name = "decode" + +[[constraints.decode]] +kind = "template" +tag = "IS_BIT" +input = [["idx", "mem_flags", "i"]] +iter = ["i", 0, 3] + +[[constraints.decode]] +kind = "template" +tag = "IS_BIT" +input = [["idx", "hint_input", "i"]] +iter = ["i", 0, 4] # PARAM: ["i", 0, N - 1] + +[[constraints.decode]] +kind = "template" +tag = "IS_BIT" +input = ["hint_output"] + +[[constraints.decode]] +kind = "arith" +# PARAM: $limits(sum)_(j = 0)^T #`arg_register_powers`_(i,j) dot limits(sum)_(k = 0)^(d - 1) #`argument_registers`_i^k dot #`RANGE`_(j,k) = 0$ +constraint = "$limits(sum)_(j = 0)^1 #`arg_register_powers`_(i,j) dot limits(sum)_(k = 0)^4 #`argument_registers`_i^k dot #`RANGE`_(j,k) = 0$" +# PARAM: ["sum", ["=", "j", 0], T, ["*", ["idx", ["idx", "arg_register_powers", "i"], "j"], ["sum", ["=", "k", 0], ["-", "d", 1], ["*", ["^", ["idx", "argument_registers", "i"], "k"], ["idx", ["idx", "RANGE", "j"], "k"]]]]] +poly = ["sum", ["=", "j", 0], 1, ["*", ["idx", ["idx", "arg_register_powers", "i"], "j"], ["sum", ["=", "k", 0], 4, ["*", ["^", ["idx", "argument_registers", "i"], "k"], ["idx", ["idx", "RANGE", "j"], "k"]]]]] +iter = ["i", 0, 3] + +[[constraints.decode]] +kind = "interaction" +tag = "FIELD_VM_DECODE" +input = [ + ["+", + "pc", + ["*", "X", ["idx", "argument_scalars", 3]], + ["*", ["^", "X", 2], ["idx", "argument_offsets", 3]], + ], + + ["+", + ["idx", "argument_scalars", 0], + ["*", "X", ["idx", "argument_scalars", 1]], + ["*", ["^", "X", 2], ["idx", "argument_scalars", 2]], + ], + + ["+", + ["idx", "argument_offsets", 0], + ["*", "X", ["idx", "argument_offsets", 1]], + ["*", ["^", "X", 2], ["idx", "argument_offsets", 2]], + ], + + ["+", + ["idx", "mem_flags", 0], + ["*", ["^", 2, 1], ["idx", "mem_flags", 1]], + ["*", ["^", 2, 2], ["idx", "mem_flags", 2]], + ["*", ["^", 2, 3], ["idx", "mem_flags", 3]], + + ["*", ["^", 2, 4], "hint_output"], + + # PARAM: N rows + ["*", ["^", 2, 5], ["idx", "hint_input", 0]], + ["*", ["^", 2, 6], ["idx", "hint_input", 1]], + ["*", ["^", 2, 7], ["idx", "hint_input", 2]], + ["*", ["^", 2, 8], ["idx", "hint_input", 3]], + ["*", ["^", 2, 9], ["idx", "hint_input", 4]], + + ["*", "X", ["+", + ["idx", "argument_registers", 0], + ["*", ["^", 2, 8], ["idx", "argument_registers", 1]], + ["*", ["^", 2, 16], ["idx", "argument_registers", 2]], + ["*", ["^", 2, 24], ["idx", "argument_registers", 3]]]], + ], +] +multiplicity = 1 + +[[constraint_groups]] +name = "mux" + +[[constraints.mux]] +kind = "arith" +constraint = "$#`arg_reg_pows_computed`_(i,0) = #`argument_registers`_i^4$" # PARAM: power = d - 1 +poly = ["-", ["idx", ["idx", "arg_reg_pows_computed", "i"], 0], + ["*", + ["idx", "argument_registers", "i"], + ["idx", "argument_registers", "i"], + ["idx", "argument_registers", "i"], + ["idx", "argument_registers", "i"]]] +iter = ["i", 0, 3] + +# PARAM: If T > 1, we need to populate arg_reg_pows_computed[i][j], j > 0, too, with power j * (d - 2) + (d - 1) + +[[constraints.mux]] +kind = "arith" +# PARAM: $#`args_premem`_i = #`argument_offsets`_i + #`argument_scalars`_i dot limits(sum)_(j = 0)^(N + 1) #`all_regs`_j dot (limits(sum)_(k = 0)^T #`arg_register_powers`_(i,k) dot (limits(sum_(l = 0)^(d - 2) #`argument_registers`_i^l dot #`MUX`_(j,k,l)))$ +constraint = "$#`args_premem`_i = #`argument_offsets`_i + #`argument_scalars`_i dot limits(sum)_(j = 0)^6 #`all_regs`_j dot (limits(sum)_(k = 0)^1 #`arg_register_powers`_(i,k) dot (limits(sum)_(l = 0)^3 #`argument_registers`_i^l dot #`MUX`_(j,k,l)))$" +# PARAM: ["-", ["idx", "args_premem", "i"], ["idx", "argument_offsets", "i"], ["*", ["idx", "argument_scalars", "i"], ["sum", ["=", "j", 0], ["+", "N", 1], ["*", ["idx", "all_regs", "j"], ["sum", ["=", "k", 0], "T", ["*", ["idx", ["idx", "arg_register_powers", "i"], "k"], ["sum", ["=", "l", 0], ["-", "d", 2], ["*", ["^", ["idx", "argument_registers", "i"], "l"], ["idx", ["idx", ["idx", "MUX", "l"], "k"], "j"]]]]]]]]] +poly = ["-", ["idx", "args_premem", "i"], ["idx", "argument_offsets", "i"], ["*", ["idx", "argument_scalars", "i"], ["sum", ["=", "j", 0], 6, ["*", ["idx", "all_regs", "j"], ["sum", ["=", "k", 0], 1, ["*", ["idx", ["idx", "arg_register_powers", "i"], "k"], ["sum", ["=", "l", 0], 3, ["*", ["^", ["idx", "argument_registers", "i"], "l"], ["idx", ["idx", ["idx", "MUX", "j"], "k"], "l"]]]]]]]]] +iter = ["i", 1, 3] +ref = "field-VM:c:first-mux" + +[[constraints.mux]] +kind = "arith" +# PARAM: $#`args_premem`_0 = #`argument_offsets`_0 + #`argument_scalars`_0 dot limits(sum)_(j = 0)^(N + 1) #`all_regs`_j dot (limits(sum)_(k = 0)^T #`arg_register_powers`_(i,k) dot (limits(sum_(l = 0)^(d - 2) #`argument_registers`_0^l dot #`MUX`_(j,k,l)))$ +constraint = "$#`args_premem`_0 = #`argument_offsets`_0 + #`argument_scalars`_0 dot limits(sum)_(j = 0)^6 #`all_regs`'_j dot (limits(sum)_(k = 0)^1 #`arg_register_powers`_(i,k) dot (limits(sum)_(l = 0)^3 #`argument_registers`_0^l dot #`MUX`_(j,k,l)))$" +# PARAM: ["-", ["idx", "args_premem", 0], ["idx", "argument_offsets", 0], ["*", ["idx", "argument_scalars", 0], ["sum", ["=", "j", 0], ["+", "N", 1], ["*", ["idx", ["next", "all_regs"], "j"], ["sum", ["=", "k", 0], "T", ["*", ["idx", ["idx", "arg_register_powers", 0], "k"], ["sum", ["=", "l", 0], ["-", "d", 2], ["*", ["^", ["idx", "argument_registers", 0], "l"], ["idx", ["idx", ["idx", "MUX", "l"], "k"], "j"]]]]]]]]] +poly = ["-", ["idx", "args_premem", 0], ["idx", "argument_offsets", 0], ["*", ["idx", "argument_scalars", 0], ["sum", ["=", "j", 0], 6, ["*", ["idx", ["next", "all_regs"], "j"], ["sum", ["=", "k", 0], 1, ["*", ["idx", ["idx", "arg_register_powers", 0], "k"], ["sum", ["=", "l", 0], 3, ["*", ["^", ["idx", "argument_registers", 0], "l"], ["idx", ["idx", ["idx", "MUX", "j"], "k"], "l"]]]]]]]]] +ref = "field-VM:c:out-mux" + +[[constraint_groups]] +name = "memory" + +[[constraints.memory]] +kind = "arith" +constraint = "$!#`mem_flags[i]` => #`args[i]` = #`args_premem[i]`$" +poly = ["*", ["not", ["idx", "mem_flags", "i"]], ["-", ["idx", "args", "i"], ["idx", "args_premem", "i"]]] +iter = ["i", 0, 3] + +[[constraints.memory]] +kind = "interaction" +tag = "FIELD_VM_MEM" +input = [["cast", ["idx", "args_premem", "i"], "BaseField"]] +output = ["idx", "args", "i"] +multiplicity = ["idx", "mem_flags", "i"] +iter = ["i", 0, 3] + +[[constraint_groups]] +name = "fma" + +[[constraints.fma]] +kind = "arith" +constraint = "$#`args[0]` = #`args[1]` dot #`args[2]` + #`args[3]`$" +poly = ["-", ["idx", "args", 0], + ["*", ["idx", "args", 1], ["idx", "args", 2]], + ["idx", "args", 3]] + +[[constraint_groups]] +name = "transition" + +[[constraints.transition]] +kind = "arith" +constraint = "$!#`hint_input`'_i and !#`hint_output` => #`registers`'_i = #`registers`_i$" +poly = ["*", ["not", ["idx", ["next", "hint_input"], "i"]], ["not", "hint_output"], ["-", ["idx", ["next", "registers"], "i"], ["idx", "registers", "i"]]] +iter = ["i", 0, 4] # PARAM: ["i", 0, N - 1] + +[[constraints.transition]] +kind = "arith" +# PARAM: $!#`hint_input`'_i and !(limits(sum)_(j = 0)^T #`arg_register_powers`_(0,j) dot limits(sum)_(k = 0)^(d - 2) #`MUX`_(i+2,j,k) dot #`argument_registers`_0^k) => #`registers`'_i = #`registers`_i$ +constraint = "$!#`hint_input`'_i and !(limits(sum)_(j = 0)^1 #`arg_register_powers`_(0,j) dot limits(sum)_(k = 0)^3 #`MUX`_(i+2,j,k) dot #`argument_registers`_0^k) => #`registers`'_i = #`registers`_i$" +# PARAM: ["*", ["not", ["idx", ["next", "hint_input"], "i"]], ["-", 1, ["sum", ["=", "j", 0], "T", ["*", ["idx", ["idx", "arg_register_powers", 0], "j"], ["sum", ["=", "k", 0], ["-", "d", 2], ["*", ["idx", ["idx", ["idx", "MUX", ["+", "i", 2]], "j"], "k"], ["^", ["idx", "argument_registers", 0], "k"]]]]]], ["-", ["idx", ["next", "registers"], "i"], ["idx", "registers", "i"]]] +poly = ["*", ["not", ["idx", ["next", "hint_input"], "i"]], ["-", 1, ["sum", ["=", "j", 0], 1, ["*", ["idx", ["idx", "arg_register_powers", 0], "j"], ["sum", ["=", "k", 0], 3, ["*", ["idx", ["idx", ["idx", "MUX", ["+", "i", 2]], "j"], "k"], ["^", ["idx", "argument_registers", 0], "k"]]]]]], ["-", ["idx", ["next", "registers"], "i"], ["idx", "registers", "i"]]] +iter = ["i", 0, 4] # PARAM: ["i", 0, N - 1] + +[[constraints.transition]] +kind = "arith" +constraint = "$!#`hint_output` => #`pc`' = #`pc` + 1$" +poly = ["*", ["not", "hint_output"], ["-", ["next", "pc"], "pc", 1]] + +[[constraints.transition]] +kind = "arith" +# PARAM: $!(limits(sum)_(j = 0)^1 #`arg_register_powers`_(0,j) dot limits(sum)_(k = 0)^3 #`MUX`_(1,j,k) dot #`argument_registers`_0^k) => #`pc`' = #`pc` + 1$ +constraint = "$!(limits(sum)_(j = 0)^1 #`arg_register_powers`_(0,j) dot limits(sum)_(k = 0)^3 #`MUX`_(1,j,k) dot #`argument_registers`_0^k) => #`pc`' = #`pc` + 1$" +# PARAM: ["*", ["-", 1, ["sum", ["=", "j", 0], "T", ["*", ["idx", ["idx", "arg_register_powers", 0], "j"], ["sum", ["=", "k", 0], ["-", "d", 2], ["*", ["idx", ["idx", ["idx", "MUX", 1], "j"], "k"], ["^", ["idx", "argument_registers", 0], "k"]]]]]], ["-", ["next", "pc"], ["+", "pc", 1]]] +poly = ["*", ["-", 1, ["sum", ["=", "j", 0], 1, ["*", ["idx", ["idx", "arg_register_powers", 0], "j"], ["sum", ["=", "k", 0], 3, ["*", ["idx", ["idx", ["idx", "MUX", 1], "j"], "k"], ["^", ["idx", "argument_registers", 0], "k"]]]]]], ["-", ["next", "pc"], ["+", "pc", 1]]] + +[[constraints.transition]] +kind = "template" +tag = "IS_BIT" +input = ["ZERO"] + +[[constraints.transition]] +kind = "arith" +constraint = "$#`ZERO`' => #`args`_0 = 0$" +poly = ["*", ["next", "ZERO"], ["idx", "args", 0]] + +[[constraints.transition]] +kind = "arith" +constraint = "$!#`ZERO`' => #`args`_0 dot #`out_inverse` = 1$" +poly = ["*", ["not", ["next", "ZERO"]], ["-", 1, ["*", ["idx", "args", 0], "out_inverse"]]] diff --git a/spec/src/field_vm_decode.toml b/spec/src/field_vm_decode.toml new file mode 100644 index 000000000..865a95fc6 --- /dev/null +++ b/spec/src/field_vm_decode.toml @@ -0,0 +1,87 @@ +name = "FIELD_VM_DECODE" +code = "FVD" + +[[variables.output]] +name = "pc" +type = "BaseField" +desc = "The program counter" + +[[variables.output]] +name = "argument_registers" +type = ["BaseField", 4] +desc = "The register numbers of the arguments `d`, `a`, `b`, `c`, in that order" + +[[variables.output]] +name = "argument_scalars" +type = ["BaseField", 4] +desc = "The `imm_0` scalars for the arguments `d`, `a`, `b`, `c`, in that order" + +[[variables.output]] +name = "argument_offsets" +type = ["BaseField", 4] +desc = "The `imm_1` offsets for the arguments `d`, `a`, `b`, `c`, in that order" + +[[variables.output]] +name = "mem_flags" +type = ["Bit", 4] +desc = "Whether the argument (`d`, `a`, `b`, `c`, in that order) comes from a memory lookup" + +[[variables.output]] +name = "hint_input" +type = ["Bit", 5] # PARAM: ["Bit", N] +desc = "Whether each input register is hinted by this instruction" + +[[variables.output]] +name = "hint_output" +type = "Bit" +desc = "Whether the output register is hinted by this instruction" + +[[variables.multiplicity]] +name = "μ" +type = "BaseField" +desc = "" + +[[variables.virtual]] +name = "scalars" +type = "ExtField" +def = ["sum", ["=", "i", 0], 2, ["*", ["^", "X", "i"], ["idx", "argument_scalars", "i"]]] +desc = "The packed column containing most of the `imm_0`s" + +[[variables.virtual]] +name = "offsets" +type = "ExtField" +def = ["sum", ["=", "i", 0], 2, ["*", ["^", "X", "i"], ["idx", "argument_offsets", "i"]]] +desc = "The packed column containing most of the `imm_1`s" + +[[variables.virtual]] +name = "pc_and_leftovers" +type = "ExtField" +def = ["+", "pc", ["*", "X", ["idx", "argument_scalars", 3]], ["*", ["^", "X", 2], ["idx", "argument_offsets", 3]]] +desc = "The packed column containing `pc` and the remaining `imm`s" + +[[variables.virtual]] +name = "flags_and_registers" +type = "ExtField" +def = ["+", + ["sum", ["=", "i", 0], 3, ["*", ["^", 2, "i"], ["idx", "mem_flags", "i"]]], + ["*", ["^", 2, 4], "hint_output"], + # PARAM: ["sum", ["=", "i", 0], N-1, ["*", ["^", 2, ["+", "i", 5]], ["idx", "hint_input", "i"]]], + ["sum", ["=", "i", 0], 4, ["*", ["^", 2, ["+", "i", 5]], ["idx", "hint_input", "i"]]], + + ["*", "X", ["sum", ["=", "i", 0], 3, ["*", ["^", 2, ["*", 8, "i"]], ["idx", "argument_registers", "i"]]]], +] +desc = "The packed column containing bit flags and argument register indices" + +[[variables.constant]] +name = "X" +type = "ExtField" +desc = "A primitive element of the extension field, such that $(1, #`X`, #`X`^2)$ is a basis for the extension field over the base field" + +[[constraint_groups]] +name = "decode" + +[[constraints.decode]] +kind = "interaction" +tag = "FIELD_VM_DECODE" +input = ["pc_and_leftovers", "scalars", "offsets", "flags_and_registers"] +multiplicity = ["-", "μ"] diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index bdc85f9bf..2cae7b670 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -236,3 +236,16 @@ input = ["Bit", "Word", "U256BL", "U256BL", "U256BL", "U256BL", "Byte", "Bit"] kind = "interaction" tag = "BIT" input = ["Word", "Byte"] + + +# Field VM +[[signatures]] +kind = "interaction" +tag = "FIELD_VM_MEM" +input = ["BaseField"] +output = "ExtField" + +[[signatures]] +kind = "interaction" +tag = "FIELD_VM_DECODE" +input = ["ExtField", "ExtField", "ExtField", "ExtField"] diff --git a/spec/tooling/chip.py b/spec/tooling/chip.py index fe36b2f39..ea017de61 100644 --- a/spec/tooling/chip.py +++ b/spec/tooling/chip.py @@ -46,7 +46,7 @@ def asserts(self, condition: bool, message: str): def assert_no_unexpected(data: dict, possible_keys: Iterable[str]): - for key in data.keys(): + for key in data: reporter.asserts(key in possible_keys, f"Unexpected key: {key!r}") @@ -70,16 +70,23 @@ def get_const(self) -> int: return self.low -type Type = list[Type] | Range +@dataclass(frozen=True) +class Opaque: + tag: str + + +type Type = list[Type] | Range | Opaque DEFAULT_TYPE: Type = Range.const(0) def structure_matches(a: Type, b: Type) -> bool: - if isinstance(a, Range) and isinstance(b, (Range, type(None))): + if isinstance(a, Range) and isinstance(b, Range): return True elif isinstance(a, list) and isinstance(b, list): return len(a) == len(b) and all(structure_matches(x, y) for x, y in zip(a, b)) + elif isinstance(a, Opaque) and isinstance(b, Opaque): + return a.tag == b.tag else: return False @@ -87,9 +94,12 @@ def structure_matches(a: Type, b: Type) -> bool: def constant_fits(cst: int, target: Type) -> bool: if isinstance(target, Range): return target.low <= cst <= target.high - else: + elif isinstance(target, list): return constant_fits(cst, target[0]) - + else: + assert isinstance(target, Opaque) + # Let's assume this fits in an opaque + return True type Expr = ( LitExpr @@ -104,6 +114,7 @@ def constant_fits(cst: int, target: Type) -> bool: | PowExpr | SumExpr | NotExpr + | NextExpr | DummyExpr ) @@ -162,7 +173,7 @@ def typecheck(self, env: Environment) -> Type: reporter.error(f"Invalid index: {idx!r}") return Range.const(-1) idxconst = idx.get_const() - if isinstance(base, Range): + if not isinstance(base, list): reporter.error(f"Indexing into non-array type: {self!r}") return DEFAULT_TYPE if not (0 <= idxconst < len(base)): @@ -195,12 +206,17 @@ def typecheck(self, env: Environment) -> Type: CastExpr(LitExpr(base.get_const() if i == 0 else 0), t).typecheck(env) for i, t in enumerate(self.type) ] + elif isinstance(self.type, Opaque): + return self.type return base if isinstance(base, list) and all(b == Range.const(0) for b in base): # Workaround for casts of constant zero, to make padding work nicely # This may become cleaner if we eventually get to the cast rework from #326 if isinstance(self.type, Range): return Range.const(0) + elif isinstance(self.type, Opaque): + # We assume this works for an opaque type, as it's an explicit cast + return self.type else: return [CastExpr(LitExpr(0), t).typecheck(env) for t in self.type] return self.type @@ -214,10 +230,17 @@ def typecheck_binop(self, a: Type, b: Type) -> Type: if isinstance(a, list) and isinstance(b, list): reporter.error(f"Multiplication of non-scalar types: {self!r}") return DEFAULT_TYPE - elif not isinstance(a, Range): + elif isinstance(a, list): return [self.typecheck_binop(x, b) for x in a] elif isinstance(b, list): return self.typecheck_binop(b, a) + elif isinstance(a, Opaque): + if isinstance(b, Opaque): + reporter.asserts(a.tag == b.tag, f"Multiplication of two distinct opaque types: {self!r}") + # Works to multiply with a constant/Range + return a + elif isinstance(b, Opaque): + return self.typecheck_binop(b, a) else: extrema = [x * y for x in [a.low, a.high] for y in [b.low, b.high]] return Range(min(extrema), max(extrema)) @@ -243,6 +266,13 @@ def typecheck_binop(self, a: Type, b: Type) -> Type: elif isinstance(a, list) or isinstance(b, list): reporter.error(f"Adding of scalar and array types {self!r}") return DEFAULT_TYPE + elif isinstance(a, Opaque): + if isinstance(b, Opaque): + reporter.asserts(a.tag == b.tag, f"Addition of two distinct opaque types: {self!r}") + # Still works adding Ranges to it + return a + elif isinstance(b, Opaque): + return self.typecheck_binop(b, a) else: return Range(a.low + b.low, a.high + b.high) @@ -270,16 +300,27 @@ def typecheck_binop(self, a: Type, b: Type) -> Type: elif isinstance(a, list) or isinstance(b, list): reporter.error(f"Subtraction of scalar and array types {self!r}") return DEFAULT_TYPE + elif isinstance(a, Opaque): + if isinstance(b, Opaque): + reporter.asserts(a.tag == b.tag, f"Subtraction of two distinct opaque types: {self!r}") + # We allow subtracting Ranges + return a + elif isinstance(b, Opaque): + # Flipping the order doesn't matter, as we're returning an Opaque anyway + return self.typecheck_binop(b, a) else: return Range(a.low - b.high, a.high - b.low) def typecheck(self, env: Environment) -> Type: t = self.head.typecheck(env) if not self.subs: - if not isinstance(t, Range): + if isinstance(t, Range): + return Range(-t.high, -t.low) + elif isinstance(t, Opaque): + return t + else: reporter.error(f"Negating a non-scalar type: {self!r}") return t - return Range(-t.high, -t.low) for term in self.subs: t = self.typecheck_binop(t, term.typecheck(env)) return t @@ -294,6 +335,10 @@ def typecheck(self, env: Environment) -> Type: elt = self.elt.typecheck(env) modulus = self.modulus.typecheck(env) + if isinstance(elt, Opaque) or isinstance(modulus, Opaque): + reporter.error(f"Cannot take a mod with opaque types: {self!r}") + return elt + if isinstance(modulus, list) or not modulus.is_const(): reporter.error(f"Invalid non-constant modulus: {self.modulus!r}") return Range.const(0) @@ -316,14 +361,27 @@ class PowExpr: def typecheck(self, env: Environment) -> Type: base = self.base.typecheck(env) exp = self.exp.typecheck(env) - if isinstance(base, list) or not base.is_const(): - reporter.error(f"Invalid exponentiation with non-const base: {self.base!r}") + if isinstance(base, list): + reporter.error(f"Invalid exponentiation of a list: {self.base!r}") return DEFAULT_TYPE - if isinstance(exp, list) or not exp.is_const(): + if not (isinstance(exp, Range) and exp.is_const()): reporter.error(f"Invalid exponentiation with non-const exponent: {self.exp!r}") return DEFAULT_TYPE - val = pow(base.get_const(), exp.get_const(), env.config.variables.prime) - return Range.const(val) + + if isinstance(base, Opaque): + return base + + # If const base, we have a const result + if base.is_const(): + return Range.const(pow(base.get_const(), exp.get_const(), env.config.variables.prime)) + # If we have no modular wrap, we have a correct range + e, p = exp.get_const(), env.config.variables.prime + small_pow = e * max(0, base.high.bit_length() - 1) <= p.bit_length() + if base.low >= 0 and small_pow and base.high ** e < p: + return Range(pow(base.low, e, p), pow(base.high, e, p)) + # Else, escape hatch to the full base type + else: + return Range(0, env.config.variables.prime - 1) @dataclass @@ -340,6 +398,12 @@ def typecheck_binop(self, a: Type, b: Type) -> Type: elif isinstance(a, list) or isinstance(b, list): reporter.error(f"Summing of scalar and array types {self!r}") return DEFAULT_TYPE + elif isinstance(a, Opaque): + if isinstance(b, Opaque): + reporter.asserts(a.tag == b.tag, f"Summation of two distinct opaque types: {self!r}") + return a + elif isinstance(b, Opaque): + return self.typecheck_binop(b, a) else: return Range(a.low + b.low, a.high + b.high) @@ -356,12 +420,20 @@ class NotExpr: def typecheck(self, env: Environment) -> Type: inner = self.inner.typecheck(env) - if isinstance(inner, list) or not inner.is_bool(): + if not (isinstance(inner, Range) and inner.is_bool()): reporter.error(f"Not a bool passed to `not`: {self.inner!r}") return Range(0, 1) return Range(1 - inner.high, 1 - inner.low) +@dataclass +class NextExpr: + inner: VarExpr + + def typecheck(self, env: Environment) -> Type: + return self.inner.typecheck(env) + + @dataclass class DummyExpr: def typecheck(self, _env: Environment) -> Type: @@ -404,6 +476,10 @@ def build_expr(config: Optional["Config"], data: object) -> Expr: return SumExpr(Iter(config, var, start, stop), build_expr(config, terms)) case ["not", e]: return NotExpr(build_expr(config, e)) + case ["next", str(var)]: + inner = build_expr(config, var) + assert isinstance(inner, VarExpr), f"Invalid transition variable: {var!r}" + return NextExpr(inner) case other: reporter.error(f"Unknown expression: {other!r}") return DummyExpr() @@ -435,11 +511,11 @@ def __init__(self, config: "Config", name: str, start: object, stop: object): def typecheck[T](self, env: Environment, callback: Callable[[Environment], Iterable[T]]) -> Iterable[T]: start = self.start.typecheck(env) - if isinstance(start, list) or not start.is_const(): + if not (isinstance(start, Range) and start.is_const()): reporter.error(f"Starting value of iterator not a const: {self!r}") start = Range.const(0) stop = self.stop.typecheck(env) - if isinstance(stop, list) or not stop.is_const(): + if not (isinstance(stop, Range) and stop.is_const()): reporter.error(f"Ending value of iterator not a const: {self!r}") stop = Range.const(start.get_const()) @@ -482,12 +558,12 @@ def clean_iter(it): class TypeConfig: label: str subtypes: list[Type] - range: Optional[Range] + scalar_type: Range | Opaque | None desc: str preprocessed: bool def __init__(self, default_name: str, lookup: Callable[[str], Type], data: dict): - assert_no_unexpected(data, type(self).__annotations__.keys()) + assert_no_unexpected(data, type(self).__annotations__.keys() - {"scalar_type"} | {"range"}) self.label = data["label"] if "range" in data: reporter.asserts( @@ -506,16 +582,19 @@ def __init__(self, default_name: str, lookup: Callable[[str], Type], data: dict) reporter.error(f"Range end not an int: {data!r}") stop = start reporter.asserts(int(start) <= int(stop), f"Inverted range: {data!r}") - self.range = Range(int(start), int(stop)) + self.scalar_type = Range(int(start), int(stop)) + self.subtypes = [] + elif data["subtypes"] == [data["label"]]: + self.scalar_type = Opaque(data["label"]) self.subtypes = [] else: - self.range = None + self.scalar_type = None self.subtypes = [lookup(tp) for tp in data["subtypes"]] self.desc = data["desc"] self.preprocessed = data.get("preprocessed", False) def as_type(self) -> Type: - return self.range or self.subtypes[:] + return self.scalar_type or self.subtypes[:] @dataclass @@ -712,15 +791,15 @@ def handle_iters( # Some duplicated code/concepts from Iter.typecheck # But threading the extra needed state through overly complicates everything start = it.start.typecheck(env) - if isinstance(start, list) or not start.is_const(): + if not (isinstance(start, Range) and start.is_const()): reporter.error(f"Starting value of virtual def iter not a const: {self!r}") start = Range.const(0) stop = it.stop.typecheck(env) - if isinstance(stop, list) or not stop.is_const(): + if not (isinstance(stop, Range) and stop.is_const()): reporter.error(f"Ending value of virtual def iter not a const: {self!r}") stop = Range.const(start.get_const()) - if isinstance(expected, Range): + if not isinstance(expected, list): reporter.error(f"Virtual definition has an iter for a scalar: {self!r}") return @@ -747,7 +826,7 @@ def is_covered(seen: set[tuple], indices: list[int]) -> bool: return False def check_covered(t: Type, seen: set[tuple], indices: list[int]): - if isinstance(t, Range): + if not isinstance(t, list): reporter.asserts( is_covered(seen, indices), f"Virtual column {self.name!r} not completely defined", @@ -757,15 +836,24 @@ def check_covered(t: Type, seen: set[tuple], indices: list[int]): check_covered(elt, seen, indices + [i]) # Special case for better error messages - if isinstance(self.type, Range): + if not isinstance(self.type, list): reporter.asserts( len(self.def_.defs) == 1 and not self.def_.defs[0].iters, f"Invalid def for scalar column: {self!r}", ) assigned_type = self.def_.defs[0].poly.typecheck(env) - if not isinstance(assigned_type, Range): + if isinstance(assigned_type, list): reporter.error(f"Assigning non-scalar type to scalar virtual column: {self!r}") return self.type + + if isinstance(self.type, Range) and not isinstance(assigned_type, Range): + reporter.error(f"Incompatible virtual column type assignment: {self!r}") + return self.type + + if isinstance(self.type, Opaque) and (not isinstance(assigned_type, Opaque) or assigned_type.tag != self.type.tag): + reporter.error(f"Incompatible virtual column opaque type assignment: {self!r}") + return self.type + # Check type fits? # Leaving this out because it produces too much noise with one-hot assumptions # reporter.asserts(self.type.low <= assigned_type.low <= assigned_type.high <= self.type.high, f"Definition may not fit in virtual column: {self!r}") @@ -846,7 +934,7 @@ def check_includes_zero(t: Type): t.low <= 0 <= t.high, f"Unsatisfiable constraint, 0 not in range: {self!r} {t}", ) - else: + elif not isinstance(t, Opaque): reporter.error(f"Non-scalar value for polynomial constraint: {self!r} {t}") for t in all_iters(self.iters, env, lambda e: [self.poly.typecheck(e)]): @@ -857,9 +945,9 @@ def check_includes_zero(t: Type): @dataclass class Signature: tag: str - condition: Optional[Type] + condition: Type | None input: list[Type] - output: Optional[Type] + output: Type | None def matches(self, other: Self) -> bool: if not isinstance(other, type(self)): @@ -886,8 +974,8 @@ class InteractionLike: tag: str desc: str input: list[Expr] - output: Optional[Expr] - conditional: Optional[Expr] + output: Expr | None + conditional: Expr | None iters: list[Iter] def __init__(self, config: Config, data: dict): @@ -1081,7 +1169,7 @@ def check_assignment( values: dict[str, Type], ): reporter.asserts( - set(values.keys()) <= set(v.name for v in self.concrete_vars), + set(values.keys()) <= {v.name for v in self.concrete_vars}, f"Passing unrecognized variable to `check_assignment` of chip {self.name!r}", ) env = Environment(self.config, {}, {}) @@ -1109,7 +1197,7 @@ def check_assignment( def build_signature(config: Config, data: dict) -> Signature: assert_no_unexpected(data, {"tag", "kind", "input", "output", "cond"}) Sig: type[Signature] - cond: Optional[Type] = None + cond: Type | None = None match data["kind"]: case "template": if "cond" in data: