From 03131e530cf1f482f0288b1aa62978439fe15f7e Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 8 Sep 2026 11:17:11 +0200 Subject: [PATCH 01/22] Field VM, first edition --- spec/book.typ | 236 ------------------ spec/chapters/field_decode.typ | 2 - spec/chapters/field_vm.typ | 211 ++++++++++++++++ .../{field.typ => field_vm_decode.typ} | 0 spec/expr.typ | 38 +-- spec/meta.typ | 4 +- spec/src/config.toml | 5 + spec/src/field_vm.toml | 202 +++++++++++++++ spec/tooling/chip.py | 27 +- 9 files changed, 467 insertions(+), 258 deletions(-) delete mode 100644 spec/book.typ delete mode 100644 spec/chapters/field_decode.typ create mode 100644 spec/chapters/field_vm.typ rename spec/chapters/{field.typ => field_vm_decode.typ} (100%) create mode 100644 spec/src/field_vm.toml diff --git a/spec/book.typ b/spec/book.typ deleted file mode 100644 index 847730933..000000000 --- a/spec/book.typ +++ /dev/null @@ -1,236 +0,0 @@ -#import "@preview/shiroa:0.3.1": * -#import "/templates/page.typ": project -#import "@preview/equate:0.3.2": equate - -#show: book - -#let meta = ( - title: "Lambda VM specification", - authors: ("3MI Labs", "Aligned"), - version: "0.2", - summary: ( - ("PROOF SYSTEM", ( - ("logup.typ", [`LogUp` argument], ), - ("memory.typ", [Memory argument], ), - ("streaming.typ", [Streaming prover], ), - ("verifier.typ", [Verification], ) - )), - ("OVERVIEW", ( - ("variables.typ", [Variables], ), - ("signatures.typ", [Signatures], ), - )), - ("TEMPLATES", ( - ("is_bit.typ", [`IS_BIT` template], ), - ("is_byte.typ", [`IS_BYTE` template], ), - ("sign.typ", [`SIGN` template], ), - ("add.typ", [`ADD`/`SUB` template], ), - ("neg.typ", [`NEG` template], ), - ("reg.typ", [`REG`/`REGW` template], ), - )), - ("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], ), - ("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`], ), - ("halt.typ", [`HALT` chip], ), - ("commit.typ", [`COMMIT` chip], ), - ("sha256.typ", [`SHA256` accelerator], ), - ("keccak.typ", [`KECCAK` accelerator], ), - ("ecsm.typ", [`ECSM` accelerator], ), - ("fext.typ", [Extension field accelerator], ), - )), - ("RECURSION", ( - ("recursion.typ", [Recursive verification], ), - ("field.typ", [`Field` VM], ), - ("field_decode.typ", [`Field` `DECODE` table], ), - )), - ("MATHEMATICS", ( - ("limbs_and_carries.typ", [On limb decomposition and carries], ), - )) - ) -) -#let meta_sections = meta.summary.map(m => m.at(1)).sum() -#book-meta( - title: meta.title, - authors: meta.authors, - summary: prefix-chapter("front.typ", meta.title) - + meta.summary.map( - ((title, sections)) => { - heading(depth: 1, title) + sections.map(((ch, title, _ref)) => chapter(ch, title)).join() - } - ).join() -) - -#let highlights = ( - "aside": ("Aside", rgb("55aaff")), - "attention": ("Attention", rgb("ff2600")), -) - -#let highlight(title, body, ref: none, kind: "aside") = [ - #figure( - caption: title, - supplement: highlights.at(kind).at(0), - kind: kind, - body - )#ref -] - -#let aside = highlight.with(kind: "aside") -#let attention = highlight.with(kind: "attention") - -#let common-formatting(body) = { - set footnote(numbering: "[1]") - show raw.where(block: true): it => block(it, inset: 1em, width: 100%, radius: 5pt) - show ref: equate.with(sub-numbering: true, breakable: true, number-mode: "label") - show selector.or(..highlights.keys().map(k => figure.where(kind: k))): it => { - set figure.caption(position: top) - show figure.caption: cap => block( - inset: (left: 1em, right: 1em, top: .75em, bottom: .75em), - outset: (left: 1em), - width: 100% + 1em, - fill: highlights.at(it.kind).at(1), - stroke: luma(50%), - align(center, strong(text(fill: black, cap))) - ) - block(inset: (left: 1em, right: 1em, bottom: 1em), stroke: luma(50%), breakable: false, align(left, it)) - } - body -} - - -#let todo(background: white, foreground: black, name: none, body) = block(fill: background, outset: 0.4em, radius: 20%, stroke: black)[ - #set text(fill: foreground) - *TODO #if name != none { [(#name)] }*: #body -] -#let rj = todo.with(background: teal, name: "Robin") -#let et = todo.with(background: rgb("d4aa3a"), name: "Erik") -#let cdsg = todo.with(background: olive, name: "Cyprien") - - -#let is-shiroa = "x-target" in sys.inputs - -// Strip styling to keep only "pure" content. -// This is useful to avoid errors on the `set document(...)` in `project` -// when invisibly including other chapters to resolve xrefs. -#let strip-all(content) = { - if repr(content.func()) == "sequence" { - for c in content.children { - strip-all(c) - } - } else if repr(content.func()) == "styled" { - strip-all(content.child) - } else { - content - } -} - -#let _toplevel = state("_toplevel", none) -#let _xref-included = state("_xref-included", (:)) - -// Invisibly include another chapter, so that its labels can be resolved -#let xref-include(f) = { - show ref: none - context { - place(hide(box(width: auto, height: 0%, strip-all(include "/" + f)))) - } -} - -// Generate a cross-link for references to other chapters. -// Leaves the ref untouched if it can't be resolved or points to the current chapter. -#let xref(rf) = { - assert(is-shiroa, message: "xref should only be used when compiling for shiroa") - let lbl = rf.target - let found = meta_sections.find(((_, _, tag)) => str(lbl).starts-with(str(tag))) - context if found != none and found.at(0) != _toplevel.final() { - let (ch, title, ref) = found - if ref == lbl { - cross-link("/" + ch, [Chapter #(meta_sections.position(x => x == found) + 1)]) - } else { - // Because shiroa does weird url escaping - let shiroa-label = label(str(lbl).replace(":", "%3A")) - context _xref-included.update(x => x + ((ch): true)) - // The ideal would be to use `rf` directly as content argument to `cross-link`, - // as that would inherit any/all formatting of the ref we want or need. - // Unfortunately the ref link seems to take precedence over the cross-link hyperlink - // when clicking. - // There may still be some way around it by messing with some html output - let link-content = context { - let fig = query(lbl).first() - let counter = if fig.has("counter") { - fig.counter - } else { - counter(fig.func()) - } - - let supplement = if rf.supplement == auto { - fig.fields().at("supplement", default: none) - } else { - rf.supplement - } - [#supplement #numbering(fig.numbering, ..counter.at(lbl))] - } - cross-link("/" + ch, reference: shiroa-label, link-content) - } - } else { - rf - } -} - -#let book-page(file, ..args) = { - if not file.ends-with(".typ") { - file = lower(file) + ".typ" - } - - assert(meta_sections.find(s => s.at(0) == file) != none, message: "Couldn't resolve typst source file " + file) - - if is-shiroa { - (body) => { - show: common-formatting - context _toplevel.update(s => { - if s == none { - file - } else { - s - } - }) - let cond() = _toplevel.final() == file - show ref: it => context if cond() { xref(it) } - let title = context { - // Strip raw, because shiroa already makes the title raw - show raw: it => it.text - meta_sections.find(x => x.at(0) == _toplevel.final()).at(1) - } - project.with(..args, title: title, description: plain-text(meta_sections.find(x => x.at(0) == file).at(1)), cond: cond)([ - #context _xref-included.final().pairs().map(((key, value)) => context if value and cond() { - xref-include(key) - }).join() - #metadata(json("interaction_count.json").sum(default: (:))) - - #let chapter-index = meta_sections.position(x => x.at(0) == file) + 1 - #set heading(numbering: (..args) => [#chapter-index.#numbering("1.1", ..args)]) - #counter(heading).update(0) - - #body - ]) - } - } else { - body => body - } -} 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..4938b9df1 --- /dev/null +++ b/spec/chapters/field_vm.typ @@ -0,0 +1,211 @@ +#import "/meta.typ": rj, aside +#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 + +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 central instruction of the ISA is a constraint for a fused multiply-add over the extension field: +`FMA o == a * b + c`. +Here all of `o`, `a`, `b` and `c` are arguments following the addressing scheme described below. +The field VM uses only read-only memory, which is implemented as a committed table, +together with the multiplicities with which each element is accessed. + +== Arguments and addressing + +The VM has a state consisting of $N$ general purpose extension field registers, +a base-field `PC` register, and a bit-register `ZERO` bit-register `ZERO`. +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$. +#rj[Register index for `ZERO` = $0$ and `PC` = $1$ and gp register `Ri` = $i + 2$] + +Each argument to the FMA constraint has either of the two following forms: +- `imm_0 * reg + imm_1` +- `MEM[imm_0 * reg + imm_1]` +where each immediate is a base field element, encoded in the instruction for a specific argument, +and `MEM[...]` reads memory. +The `o` argument to the instruction obtains its register values from the _future_ state. +That is, the state from which the next instruction will get its input register values. +The `ZERO` register of the future state contains a bit (as a base field element) that indicates whether or not +the `o` value was zero for the current instruction. +The `PC` register contains the program counter (as a base field element) and indicates which instruction is to be executed. +Every other register can hold an arbitrary extension field element. + +== Register hints + +Each register (other than `ZERO` and `PC`) in the current state can be marked as _hinted_ in an instruction. +This means that its value from the current instruction onward can get a new value +that is independent from the previous value, except as constrained by the instruction. +Additionally, the _output_ can be marked as hinted, meaning that the register used in the `o` argument +whether wrapped in a `MEM[]` lookup or not, will change in the future state, and as such in the `o` argument too. +Output hinting is commonly used to assign the result of a computation: `FMA X == X * X, hint out` would +compute `X * X` and re-assign it to `X` in the future state. +The output hint, in contradiction with the input hints, does allow `PC` to be hinted, so as to enable +causal jumps and control flow in the program. +Any register that is not hinted 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. + +#aside("Hint collisions")[ +One may observe that an output hint for state `i` and an input hint on state `i + 1` can affect +an identical register in an identical 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, +and 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 output-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 `o` 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, +in order 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. + +/ `ADD o, a, b`: Addition: `FMA o == (0 * X + 1) * a + b, hint out` +/ `MUL o, a, b`: Multiplication: `FMA o == a * b + (0 * X), hint out` +/ `INV o, a`: Extension field inversion. Note: `o` and `a` cannot use the same register here: `FMA o == (a + 1) * o - 1, hint ` +/ `J a`: Jump. Can be to a register, memory content, or absolute address, depending on the addressing mode of `a`, even relative to PC: `FMA PC == a, hint out` +/ `JZA imm`: Jump if ZERO, absolute target address: `FMA PC == (-1 * ZERO + 1) * (PC - imm) + (imm + 1), hint out` +/ `JZR a`: Jump if ZERO, PC-relative target address: `FMA PC == (ZERO) * (a - 1) + (PC + 1), hint out` +/ `JNZA imm`: Jump if not ZERO, absolute target address: `FMA PC == ZERO * (PC - imm) + (ZERO + imm), hint out` +/ `JNZR a`: Jump if not ZERO, PC-relative target address: `FMA PC == (a - 1) * (-1 * ZERO + 1) + (PC + 1), hint out` + +Eventually, we hope that a set of common pseudoinstructions can be extracted from actual usage, +and inform 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`, one of the general purpose registers. +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 + +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 + FMA [fp - i] == STORED_REG_i + FMA [fp + 1] == (PC + 2) + FMA PC == target, hint out + FMA fp == [fp], hint out + +RET: + FMA PC == [fp + 1], hint out +``` + +#rj[Figure out halting, can be a simple self-loop, just have to figure out how to have the verifier assert this] + += Arithmetization + +#let config = load_config() +#let chip = load_chip("/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 + +We first decode the instruction at the current PC. + +#render_constraint_table(chip, config, groups: "decode") + +Then, 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) + ...))), $ +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 we to compute first 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. +#rj[Analysis of relation between $d$, $N$, $t$; mention current choice of $(d, N, t) = (5, 5, 1)$] +Observe that the handling for `argument_registers[0]` is separate, 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. +#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") + +Finally, 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: +- $!#`hint_input`_r and !#`hint_output` => #`registers`'_r = #`registers`_r$, `r` could not have been hinted, + since it was not input-hinted, and there was not output hint, so the next `r` should remain the same. +- $!#`hint_input`_r and f_r(#`argument_registers`_0) = 0 => #`registers`'_r = #`registers_r`$ + `r` was not input-hinted, and it was not the output register, so it once again stays the same. + +This is equivalent to the logical statement $!#`hint_input`_r and not (#`hint_output` and f_r(#`argument_registers`_0) = 1) => #`registers`'_r = #`registers`_r$, but expressed in a way that polynomial constraints can more easily handle. +Naturally, the PC gets and exception since if it is not (output-)hinted, we need $#`pc`' = #`pc` + 1$, +and the $#`ZERO`'$ register purely depends on $#`args`_0$ and not on `ZERO`. + +#render_constraint_table(chip, config, groups: "transition") + += 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 +- The `FIELD_VM_DECODE` table can be further compressed, including potentially fitting multiple base field elements into single extension field elements +- 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.typ b/spec/chapters/field_vm_decode.typ similarity index 100% rename from spec/chapters/field.typ rename to spec/chapters/field_vm_decode.typ diff --git a/spec/expr.typ b/spec/expr.typ index 16ac94867..716551f05 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, @@ -57,16 +58,17 @@ "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": 3, // var' + "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 @@ -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))$, @@ -238,6 +242,10 @@ 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) }, + "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) + }, ), var: v => if v.len() == 1 { $#v$ } else { $#raw(v)$ }, num: n => math.equation[#n], diff --git a/spec/meta.typ b/spec/meta.typ index eea8f6e4a..9e5852c9e 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], ), 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..35dbb8469 --- /dev/null +++ b/spec/src/field_vm.toml @@ -0,0 +1,202 @@ +name = "FIELD_VM" +code = "FVM" + +[[variables.input]] +name = "pc" +type = "BaseField" +desc = "The program counter" + +[[variables.input]] +name = "argument_registers" +type = ["BaseField", 4] +desc = "The register numbers of the arguments `o`, `a`, `b`, `c`, in that order" + +[[variables.input]] +name = "argument_scalars" +type = ["BaseField", 4] +desc = "The `imm_0` scalars for the arguments `o`, `a`, `b`, `c`, in that order" + +[[variables.input]] +name = "argument_offsets" +type = ["BaseField", 4] +desc = "The `imm_1` offsets for the arguments `o`, `a`, `b`, `c`, in that order" + +[[variables.input]] +name = "mem_flags" +type = ["Bit", 4] +desc = "Whether the argument (`o`, `a`, `b`, `c`, in that order) comes from a memory lookup" + +[[variables.input]] +name = "hint_input" +type = ["Bit", 5] # PARAM: ["Bit", N] +desc = "Whether each input register is hinted this cycle" + +[[variables.input]] +name = "hint_output" +type = "Bit" +desc = "Whether the output register is hinted this cycle" + +[[variables.auxiliary]] +name = "registers" +type = ["ExtField", 5] # PARAM: ["ExtField", N] +desc = "The general purpose registers" + +[[variables.auxiliary]] +name = "ZERO" +type = "Bit" +desc = "Whether the output of the previous instruction was zero" + +[[variables.auxiliary]] +name = "out_inverse" +type = "ExtField" +desc = "The multiplicative inverse of the output, used to check `ZERO`" + +[[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" + +[[variables.auxiliary]] +name = "args_premem" +type = ["ExtField", 4] +desc = "The argument values, before a potential memory lookup" + +[[variables.auxiliary]] +name = "args" +type = ["ExtField", 4] +desc = "The argument values, after a potential memory lookup" + +[[variables.virtual]] +name = "all_regs" +type = ["ExtField", 7] # PARAM: ["ExtField", N + 2] +desc = "All general purpose registers, followed by `pc` and `ZERO`, matching the decoding indices" +def = {polys = [ + {iter = ["i", 0], poly = "ZERO"}, + {iter = ["i", 1], poly = "pc"}, + {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 aroung `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", "j"], ["-", "j", 1]]} # PARAM: iters = ["i", 0, 3], ["j", 1, T]] + ]} + +[[variables.constant]] +name = "MUX" +type = [[["BaseField", 4], 2], 6] # PARAM: [[["BaseField", d - 1], t + 1], N + 1] +desc = "The MUX polynomial coefficients" + +[[constraint_groups]] +name = "decode" + +[[constraints.decode]] +kind = "interaction" +tag = "FIELD_VM_DECODE" +input = ["pc", "argument_registers", "argument_scalars", "argument_offsets", "mem_flags", "hint_input", "hint_output"] +multiplicity = 1 + +[[constraint_groups]] +name = "mux" + +[[constraints.mux]] +kind = "arith" +constraint = "$#`arg_reg_pows_computed`_(i,0) = #`arg_registers`_i^4$" # PARAM: power = d - 1 +poly = ["-", ["idx", ["idx", "arg_reg_pows_computed", "i"], 0], + ["*", + ["idx", "arg_registers", "i"], + ["idx", "arg_registers", "i"], + ["idx", "arg_registers", "i"], + ["idx", "arg_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", "k"], "i"], ["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] + +[[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", "k"], 0], ["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"]]]]]]]]] + +[[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 = "MEMORY" +input = [["idx", "args_premem", "i"]] +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", "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", "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"]]]]]], ["-", ["next", "pc"], ["+", "pc", 1]]] +poly = ["*", ["not", ["idx", "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"]]]]]], ["-", ["next", "pc"], ["+", "pc", 1]]] +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 = ["*", ["not", ["idx", "hint_input", "i"]], ["-", 1, ["sum", ["=", "j", 0], 1, ["*", ["idx", ["idx", "arg_register_powers", 0], "j"], ["sum", ["=", "k", 0], 3, ["*", ["idx", ["idx", ["idx", "MUX", "i"], "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/tooling/chip.py b/spec/tooling/chip.py index fe36b2f39..1302bad66 100644 --- a/spec/tooling/chip.py +++ b/spec/tooling/chip.py @@ -104,6 +104,7 @@ def constant_fits(cst: int, target: Type) -> bool: | PowExpr | SumExpr | NotExpr + | NextExpr | DummyExpr ) @@ -316,14 +317,22 @@ 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(): + if isinstance(base, list): reporter.error(f"Invalid exponentiation with non-const base: {self.base!r}") return DEFAULT_TYPE if isinstance(exp, list) or not 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 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 + elif float(base.high)**exp.get_const() < env.config.variables.prime: + e, p = exp.get_const(), env.config.variables.prime + 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 @@ -362,6 +371,14 @@ def typecheck(self, env: Environment) -> Type: 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 +421,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() From c4b58ab8f02b79b3fede6ce4eb2ead1cc1282dc2 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 8 Sep 2026 17:26:15 +0200 Subject: [PATCH 02/22] Silly oversights --- spec/src/field_vm.toml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/spec/src/field_vm.toml b/spec/src/field_vm.toml index 35dbb8469..fab74f464 100644 --- a/spec/src/field_vm.toml +++ b/spec/src/field_vm.toml @@ -82,7 +82,7 @@ type = [["BaseField", 2], 4] # PARAM: [["BaseField", T + 1], 4] desc = "A virtual wrapper aroung `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", "j"], ["-", "j", 1]]} # PARAM: iters = ["i", 0, 3], ["j", 1, T]] + {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]] @@ -154,8 +154,8 @@ name = "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]]] + ["*", ["idx", "args", 1], ["idx", "args", 2]], + ["idx", "args", 3]] [[constraint_groups]] name = "transition" @@ -170,8 +170,8 @@ iter = ["i", 0, 4] # PARAM: ["i", 0, N - 1] 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", "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"]]]]]], ["-", ["next", "pc"], ["+", "pc", 1]]] -poly = ["*", ["not", ["idx", "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"]]]]]], ["-", ["next", "pc"], ["+", "pc", 1]]] +# PARAM: ["*", ["not", ["idx", "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", "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]] @@ -184,7 +184,7 @@ 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 = ["*", ["not", ["idx", "hint_input", "i"]], ["-", 1, ["sum", ["=", "j", 0], 1, ["*", ["idx", ["idx", "arg_register_powers", 0], "j"], ["sum", ["=", "k", 0], 3, ["*", ["idx", ["idx", ["idx", "MUX", "i"], "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" From d5644dd01faa02d62ecc625b5b28250540dda766 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 8 Sep 2026 18:24:40 +0200 Subject: [PATCH 03/22] Typechecker working for opaque types (as generalization of ExtField) --- spec/chapters/field_vm.typ | 4 ++ spec/src/field_vm.toml | 34 ++++++++++----- spec/src/signatures.toml | 14 +++++++ spec/tooling/chip.py | 85 ++++++++++++++++++++++++++++---------- 4 files changed, 106 insertions(+), 31 deletions(-) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index 4938b9df1..5844970c0 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -200,6 +200,10 @@ and the $#`ZERO`'$ register purely depends on $#`args`_0$ and not on `ZERO`. #render_constraint_table(chip, config, groups: "transition") +== Padding + +#rj[...] + = 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: diff --git a/spec/src/field_vm.toml b/spec/src/field_vm.toml index fab74f464..ab49370aa 100644 --- a/spec/src/field_vm.toml +++ b/spec/src/field_vm.toml @@ -5,74 +5,87 @@ code = "FVM" name = "pc" type = "BaseField" desc = "The program counter" +pad = 0 # TODO? Make this a reserved address containing the self loop [[variables.input]] name = "argument_registers" type = ["BaseField", 4] desc = "The register numbers of the arguments `o`, `a`, `b`, `c`, in that order" +pad = ["arr", 1, 1, 1, 1] [[variables.input]] name = "argument_scalars" type = ["BaseField", 4] desc = "The `imm_0` scalars for the arguments `o`, `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 `o`, `a`, `b`, `c`, in that order" +pad = 0 [[variables.input]] name = "mem_flags" type = ["Bit", 4] desc = "Whether the argument (`o`, `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 input register is hinted this cycle" +pad = 0 [[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 = 0 [[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", ["arr", 1], ["arr", 1], ["arr", 1], ["arr", 1]] [[variables.auxiliary]] name = "args_premem" type = ["ExtField", 4] desc = "The argument values, before a potential memory lookup" +pad = ["arr", ["-", 1], 0, 0, ["-", 1]] [[variables.auxiliary]] name = "args" type = ["ExtField", 4] desc = "The argument values, after a potential memory lookup" +pad = ["arr", ["-", 1], 0, 0, ["-", 1]] [[variables.virtual]] name = "all_regs" type = ["ExtField", 7] # PARAM: ["ExtField", N + 2] desc = "All general purpose registers, followed by `pc` and `ZERO`, matching the decoding indices" def = {polys = [ - {iter = ["i", 0], poly = "ZERO"}, - {iter = ["i", 1], poly = "pc"}, + {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] ]} @@ -87,8 +100,9 @@ def = {polys = [ [[variables.constant]] name = "MUX" -type = [[["BaseField", 4], 2], 6] # PARAM: [[["BaseField", d - 1], t + 1], N + 1] +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 [[constraint_groups]] name = "decode" @@ -104,13 +118,13 @@ name = "mux" [[constraints.mux]] kind = "arith" -constraint = "$#`arg_reg_pows_computed`_(i,0) = #`arg_registers`_i^4$" # PARAM: power = d - 1 +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", "arg_registers", "i"], - ["idx", "arg_registers", "i"], - ["idx", "arg_registers", "i"], - ["idx", "arg_registers", "i"]]] + ["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) @@ -141,8 +155,8 @@ iter = ["i", 0, 3] [[constraints.memory]] kind = "interaction" -tag = "MEMORY" -input = [["idx", "args_premem", "i"]] +tag = "FIELD_VM_MEM" +input = [["cast", ["idx", "args_premem", "i"], "BaseField"]] output = ["idx", "args", "i"] multiplicity = ["idx", "mem_flags", "i"] iter = ["i", 0, 3] diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index bdc85f9bf..0c6f0e8f5 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -236,3 +236,17 @@ 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" +# PARAM: ["BaseField", ["BaseField", 4], ["BaseField", 4], ["BaseField", 4], ["Bit", 4], ["Bit", N], "Bit"] +input = ["BaseField", ["BaseField", 4], ["BaseField", 4], ["BaseField", 4], ["Bit", 4], ["Bit", 5], "Bit"] diff --git a/spec/tooling/chip.py b/spec/tooling/chip.py index 1302bad66..e2863b34d 100644 --- a/spec/tooling/chip.py +++ b/spec/tooling/chip.py @@ -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 @@ -163,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)): @@ -202,6 +212,9 @@ def typecheck(self, env: Environment) -> Type: # 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 @@ -215,10 +228,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) and isinstance(b, Opaque): + reporter.asserts(a.tag == b.tag, f"Multiplication of opaque types with mismatching tags: {a!r} * {b!r}") + return a + elif isinstance(a, Opaque): + return a + elif isinstance(b, Opaque): + return b else: extrema = [x * y for x in [a.low, a.high] for y in [b.low, b.high]] return Range(min(extrema), max(extrema)) @@ -244,6 +264,10 @@ 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): + return a + elif isinstance(b, Opaque): + return b else: return Range(a.low + b.low, a.high + b.high) @@ -271,6 +295,10 @@ 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): + return a + elif isinstance(b, Opaque): + return b else: return Range(a.low - b.high, a.high - b.low) @@ -295,6 +323,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) @@ -318,11 +350,15 @@ def typecheck(self, env: Environment) -> Type: base = self.base.typecheck(env) exp = self.exp.typecheck(env) if isinstance(base, list): - reporter.error(f"Invalid exponentiation with non-const base: {self.base!r}") + 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 + + 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)) @@ -349,6 +385,10 @@ 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): + return a + elif isinstance(b, Opaque): + return b else: return Range(a.low + b.low, a.high + b.high) @@ -365,7 +405,7 @@ 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) @@ -456,11 +496,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()) @@ -503,12 +543,12 @@ def clean_iter(it): class TypeConfig: label: str subtypes: list[Type] - range: Optional[Range] + scalar_type: Optional[Range | Opaque] 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( @@ -527,16 +567,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 @@ -733,15 +776,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 @@ -768,7 +811,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", @@ -867,7 +910,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)]): From 8339204c29e965e07b59bec76804fe2de8dfdc53 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 8 Sep 2026 18:37:24 +0200 Subject: [PATCH 04/22] Make ruff happier --- spec/tooling/chip.py | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/spec/tooling/chip.py b/spec/tooling/chip.py index e2863b34d..a093aed7a 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}") @@ -543,7 +543,7 @@ def clean_iter(it): class TypeConfig: label: str subtypes: list[Type] - scalar_type: Optional[Range | Opaque] + scalar_type: Range | Opaque | None desc: str preprocessed: bool @@ -921,9 +921,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)): @@ -950,8 +950,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): @@ -1145,7 +1145,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, {}, {}) @@ -1173,7 +1173,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: From 29f0a576a7d93bafe9ac387e7b1ea4d30cfefb6d Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 8 Sep 2026 19:28:28 +0200 Subject: [PATCH 05/22] Various fixes --- spec/chapters/field_vm.typ | 17 ++++++++----- spec/expr.typ | 2 +- spec/tooling/chip.py | 52 ++++++++++++++++++++++++++++---------- 3 files changed, 50 insertions(+), 21 deletions(-) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index 5844970c0..8851ef658 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -18,7 +18,7 @@ together with the multiplicities with which each element is accessed. == Arguments and addressing The VM has a state consisting of $N$ general purpose extension field registers, -a base-field `PC` register, and a bit-register `ZERO` bit-register `ZERO`. +a base-field `PC` register, and a bit-register `ZERO`. 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$. #rj[Register index for `ZERO` = $0$ and `PC` = $1$ and gp register `Ri` = $i + 2$] @@ -65,7 +65,7 @@ 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 output-hinted, so no collision is possible there. +`PC` can, however, not be input-hinted, so no collision is possible there. ] == Instruction notation @@ -96,7 +96,7 @@ as experience may point out further useful abstractions. / `MUL o, a, b`: Multiplication: `FMA o == a * b + (0 * X), hint out` / `INV o, a`: Extension field inversion. Note: `o` and `a` cannot use the same register here: `FMA o == (a + 1) * o - 1, hint ` / `J a`: Jump. Can be to a register, memory content, or absolute address, depending on the addressing mode of `a`, even relative to PC: `FMA PC == a, hint out` -/ `JZA imm`: Jump if ZERO, absolute target address: `FMA PC == (-1 * ZERO + 1) * (PC - imm) + (imm + 1), hint out` +/ `JZA imm`: Jump if ZERO, absolute target address: `FMA PC == (ZERO)*(-1*PC+(imm-1))+(1*PC+1), hint out` / `JZR a`: Jump if ZERO, PC-relative target address: `FMA PC == (ZERO) * (a - 1) + (PC + 1), hint out` / `JNZA imm`: Jump if not ZERO, absolute target address: `FMA PC == ZERO * (PC - imm) + (ZERO + imm), hint out` / `JNZR a`: Jump if not ZERO, PC-relative target address: `FMA PC == (a - 1) * (-1 * ZERO + 1) + (PC + 1), hint out` @@ -166,7 +166,7 @@ $ f_(i)(x) = f_(i, 0)(x) + x^(d - 1) (f_(i, 1)(x) + x^(d - 2) (f_(i, 2) + x^(d - 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 we to compute first the values of +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]`$. @@ -179,6 +179,11 @@ 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 case 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. @@ -190,12 +195,12 @@ 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: - $!#`hint_input`_r and !#`hint_output` => #`registers`'_r = #`registers`_r$, `r` could not have been hinted, - since it was not input-hinted, and there was not output hint, so the next `r` should remain the same. + since it was not input-hinted, and there was no output hint, so the next `r` should remain the same. - $!#`hint_input`_r and f_r(#`argument_registers`_0) = 0 => #`registers`'_r = #`registers_r`$ `r` was not input-hinted, and it was not the output register, so it once again stays the same. This is equivalent to the logical statement $!#`hint_input`_r and not (#`hint_output` and f_r(#`argument_registers`_0) = 1) => #`registers`'_r = #`registers`_r$, but expressed in a way that polynomial constraints can more easily handle. -Naturally, the PC gets and exception since if it is not (output-)hinted, we need $#`pc`' = #`pc` + 1$, +Naturally, the PC gets an exception since if it is not (output-)hinted, we need $#`pc`' = #`pc` + 1$, and the $#`ZERO`'$ register purely depends on $#`args`_0$ and not on `ZERO`. #render_constraint_table(chip, config, groups: "transition") diff --git a/spec/expr.typ b/spec/expr.typ index 716551f05..a984ecd60 100644 --- a/spec/expr.typ +++ b/spec/expr.typ @@ -158,7 +158,7 @@ }, "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) + cwrap(rec(PREC.next, e.at(1)) + `'`, pp < PREC.next) }, ), num: (n) => raw(str(n)), diff --git a/spec/tooling/chip.py b/spec/tooling/chip.py index a093aed7a..ea017de61 100644 --- a/spec/tooling/chip.py +++ b/spec/tooling/chip.py @@ -206,6 +206,8 @@ 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 @@ -232,13 +234,13 @@ def typecheck_binop(self, a: Type, b: Type) -> Type: return [self.typecheck_binop(x, b) for x in a] elif isinstance(b, list): return self.typecheck_binop(b, a) - elif isinstance(a, Opaque) and isinstance(b, Opaque): - reporter.asserts(a.tag == b.tag, f"Multiplication of opaque types with mismatching tags: {a!r} * {b!r}") - return 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 b + 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)) @@ -265,9 +267,12 @@ def typecheck_binop(self, a: Type, b: Type) -> Type: 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 b + return self.typecheck_binop(b, a) else: return Range(a.low + b.low, a.high + b.high) @@ -296,19 +301,26 @@ def typecheck_binop(self, a: Type, b: Type) -> Type: 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): - return b + # 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 @@ -363,8 +375,9 @@ def typecheck(self, env: Environment) -> Type: 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 - elif float(base.high)**exp.get_const() < env.config.variables.prime: - e, p = exp.get_const(), env.config.variables.prime + 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: @@ -386,9 +399,11 @@ def typecheck_binop(self, a: Type, b: Type) -> Type: 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 b + return self.typecheck_binop(b, a) else: return Range(a.low + b.low, a.high + b.high) @@ -776,7 +791,7 @@ 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 not (isinstance(start, Range) and 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) @@ -821,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}") From cba75046d4561cdcc55939ee3073cad55b66b46c Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 8 Sep 2026 20:02:37 +0200 Subject: [PATCH 06/22] Fix input hinting constraints to take hint_input from the next row --- spec/chapters/field_vm.typ | 10 +++++----- spec/src/field_vm.toml | 12 ++++++------ 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index 8851ef658..3f3923cca 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -194,12 +194,12 @@ Finally, 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: -- $!#`hint_input`_r and !#`hint_output` => #`registers`'_r = #`registers`_r$, `r` could not have been hinted, - since it was not input-hinted, and there was no output hint, so the next `r` should remain the same. -- $!#`hint_input`_r and f_r(#`argument_registers`_0) = 0 => #`registers`'_r = #`registers_r`$ - `r` was not input-hinted, and it was not the output register, so it once again stays the same. +- $!#`hint_input`'_r and !#`hint_output` => #`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 the next `r` should remain the same. +- $!#`hint_input`'_r and f_r(#`argument_registers`_0) = 0 => #`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. -This is equivalent to the logical statement $!#`hint_input`_r and not (#`hint_output` and f_r(#`argument_registers`_0) = 1) => #`registers`'_r = #`registers`_r$, but expressed in a way that polynomial constraints can more easily handle. +This is equivalent to the logical statement $!#`hint_input`'_r and not (#`hint_output` and f_r(#`argument_registers`_0) = 1) => #`registers`'_r = #`registers`_r$, but expressed in a way that polynomial constraints can more easily handle. Naturally, the PC gets an exception since if it is not (output-)hinted, we need $#`pc`' = #`pc` + 1$, and the $#`ZERO`'$ register purely depends on $#`args`_0$ and not on `ZERO`. diff --git a/spec/src/field_vm.toml b/spec/src/field_vm.toml index ab49370aa..67ef6b7a5 100644 --- a/spec/src/field_vm.toml +++ b/spec/src/field_vm.toml @@ -176,16 +176,16 @@ name = "transition" [[constraints.transition]] kind = "arith" -constraint = "$!#`hint_input`_i and !#`hint_output` => #`registers`'_i = #`registers`_i$" -poly = ["*", ["not", ["idx", "hint_input", "i"]], ["not", "hint_output"], ["-", ["idx", ["next", "registers"], "i"], ["idx", "registers", "i"]]] +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", "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", "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"]]] +# 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]] From 49d4cf82b680ece081426101fab3846fc8ad2e56 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Thu, 10 Sep 2026 12:03:23 +0200 Subject: [PATCH 07/22] Apply batched suggestions from code review Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> Co-authored-by: Robin Jadoul --- spec/chapters/field_vm.typ | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index 3f3923cca..84e94ebec 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -23,12 +23,12 @@ The number of registers was chosen as a tradeoff between the versatility of havi and the extra cost in committed columns and decoding logic that grows with $N$. #rj[Register index for `ZERO` = $0$ and `PC` = $1$ and gp register `Ri` = $i + 2$] -Each argument to the FMA constraint has either of the two following forms: -- `imm_0 * reg + imm_1` -- `MEM[imm_0 * reg + imm_1]` +Each argument to the `FMA` constraint has either of the two following forms: +- $#`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, and `MEM[...]` reads memory. -The `o` argument to the instruction obtains its register values from the _future_ state. +The `o` argument to the instruction obtains its register value from the _future_ state. That is, the state from which the next instruction will get its input register values. The `ZERO` register of the future state contains a bit (as a base field element) that indicates whether or not the `o` value was zero for the current instruction. @@ -37,13 +37,13 @@ Every other register can hold an arbitrary extension field element. == Register hints -Each register (other than `ZERO` and `PC`) in the current state can be marked as _hinted_ in an instruction. +Each general-purpose register in the current state can be marked as _hinted_ in an instruction. This means that its value from the current instruction onward can get a new value that is independent from the previous value, except as constrained by the instruction. -Additionally, the _output_ can be marked as hinted, meaning that the register used in the `o` argument -whether wrapped in a `MEM[]` lookup or not, will change in the future state, and as such in the `o` argument too. +Additionally, the _output_ can be marked as hinted, meaning that the register used in the `o` argument --- +whether wrapped in a `MEM[]` lookup or not --- will change in the future state, and as such in the `o` argument too. Output hinting is commonly used to assign the result of a computation: `FMA X == X * X, hint out` would -compute `X * X` and re-assign it to `X` in the future state. +compute $#`X` dot #`X`$ and assign the result to `X` in the future state. The output hint, in contradiction with the input hints, does allow `PC` to be hinted, so as to enable causal jumps and control flow in the program. Any register that is not hinted will have the same value in the future state as in the current state, @@ -84,8 +84,8 @@ We note that this may be insufficient for the execution/prover side of the progr 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, -in order to allow program listings to include other mnemonics to indicate pseudoinstructions that +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; @@ -196,12 +196,12 @@ We again make use of the multiplexing machinery from before. The constraints we want to enforce on a register index $r$ are as follows: - $!#`hint_input`'_r and !#`hint_output` => #`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 the next `r` should remain the same. -- $!#`hint_input`'_r and f_r(#`argument_registers`_0) = 0 => #`registers`'_r = #`registers_r`$ +- $!#`hint_input`'_r and f_(r)(#`argument_registers`_0) = 0 => #`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. -This is equivalent to the logical statement $!#`hint_input`'_r and not (#`hint_output` and f_r(#`argument_registers`_0) = 1) => #`registers`'_r = #`registers`_r$, but expressed in a way that polynomial constraints can more easily handle. -Naturally, the PC gets an exception since if it is not (output-)hinted, we need $#`pc`' = #`pc` + 1$, -and the $#`ZERO`'$ register purely depends on $#`args`_0$ and not on `ZERO`. +Together, these constraints are logically equivalent to $!#`hint_input`'_r and not (#`hint_output` and f_(r)(#`argument_registers`_0) = 1) => #`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 $#`pc`' = #`pc` + 1$ if it is not (output-)hinted, +and $#`ZERO`'$ purely depends on $#`args`_0$ and not on `ZERO`. #render_constraint_table(chip, config, groups: "transition") From 47a2a049190551767b61fee941cabc79e76f9abd Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 14 Sep 2026 14:53:22 +0200 Subject: [PATCH 08/22] Improve expression rendering --- spec/expr.typ | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/spec/expr.typ b/spec/expr.typ index a984ecd60..f3c70733c 100644 --- a/spec/expr.typ +++ b/spec/expr.typ @@ -55,10 +55,10 @@ #let PREC = ( "MIN": -1, // - "idx": 0, // [] - "pow": 1, // ^ - "neg": 2, // Unary - - "next": 3, // var' + "next": 0, // var' + "idx": 1, // [] + "pow": 2, // ^ + "neg": 3, // Unary - "cast": 4, // cast "mul": 5, // * "div": 6, // / @@ -116,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."), @@ -240,11 +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)) - cwrap($#rec(PREC.next, e.at(1))'$, pp < PREC.next) + mwrap($#rec(PREC.next, e.at(1))'$, pp < PREC.next) }, ), var: v => if v.len() == 1 { $#v$ } else { $#raw(v)$ }, From 72c7c703070cacbc72dbdddea9edd98ee20daa8a Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 14 Sep 2026 14:57:14 +0200 Subject: [PATCH 09/22] Field is not a code-term in the titles, imo --- spec/meta.typ | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/meta.typ b/spec/meta.typ index 9e5852c9e..f863a7762 100644 --- a/spec/meta.typ +++ b/spec/meta.typ @@ -55,8 +55,8 @@ )), ("RECURSION", ( ("recursion", [Recursive verification], ), - ("field_vm", [`Field` VM], ), - ("field_vm_decode", [`Field` `DECODE` table], ), + ("field_vm", [Field VM], ), + ("field_vm_decode", [Field `DECODE` table], ), )), ("MATHEMATICS", ( ("limbs_and_carries", [On limb decomposition and carries], ), From 14ea6b62b75f4491d97dd9947620827bceac3800 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 14 Sep 2026 15:23:19 +0200 Subject: [PATCH 10/22] Rename o register to d --- spec/chapters/field_vm.typ | 25 +++++++++++-------------- spec/src/field_vm.toml | 8 ++++---- 2 files changed, 15 insertions(+), 18 deletions(-) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index 84e94ebec..3bcd03405 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -10,10 +10,8 @@ extension field arithmetic and program flow. = ISA The central instruction of the ISA is a constraint for a fused multiply-add over the extension field: -`FMA o == a * b + c`. -Here all of `o`, `a`, `b` and `c` are arguments following the addressing scheme described below. -The field VM uses only read-only memory, which is implemented as a committed table, -together with the multiplicities with which each element is accessed. +`FMA d == a * b + c`. +Here all of `d`, `a`, `b` and `c` are arguments following the addressing scheme described below. == Arguments and addressing @@ -26,12 +24,11 @@ and the extra cost in committed columns and decoding logic that grows with $N$. Each argument to the `FMA` constraint has either of the two following forms: - $#`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, -and `MEM[...]` reads memory. -The `o` argument to the instruction obtains its register value from the _future_ state. +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. That is, the state from which the next instruction will get its input register values. The `ZERO` register of the future state contains a bit (as a base field element) that indicates whether or not -the `o` value was zero for the current instruction. +the `d` value was zero for the current instruction. The `PC` register contains the program counter (as a base field element) and indicates which instruction is to be executed. Every other register can hold an arbitrary extension field element. @@ -40,8 +37,8 @@ Every other register can hold an arbitrary extension field element. Each general-purpose register in the current state can be marked as _hinted_ in an instruction. This means that its value from the current instruction onward can get a new value that is independent from the previous value, except as constrained by the instruction. -Additionally, the _output_ can be marked as hinted, meaning that the register used in the `o` argument --- -whether wrapped in a `MEM[]` lookup or not --- will change in the future state, and as such in the `o` argument too. +Additionally, the _output_ can be marked as hinted, meaning that the register used in the `d` argument --- +whether wrapped in a `MEM[]` lookup or not --- will change in the future state, and as such in the `d` argument too. Output hinting is commonly used to assign the result of a computation: `FMA X == X * X, hint out` would compute $#`X` dot #`X`$ and assign the result to `X` in the future state. The output hint, in contradiction with the input hints, does allow `PC` to be hinted, so as to enable @@ -78,7 +75,7 @@ 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 `o` as above +- `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, @@ -92,9 +89,9 @@ 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. -/ `ADD o, a, b`: Addition: `FMA o == (0 * X + 1) * a + b, hint out` -/ `MUL o, a, b`: Multiplication: `FMA o == a * b + (0 * X), hint out` -/ `INV o, a`: Extension field inversion. Note: `o` and `a` cannot use the same register here: `FMA o == (a + 1) * o - 1, hint ` +/ `ADD d, a, b`: Addition: `FMA d == (0 * X + 1) * a + b, hint out` +/ `MUL d, a, b`: Multiplication: `FMA d == a * b + (0 * X), hint out` +/ `INV d, a`: Extension field inversion. Note: `d` and `a` cannot use the same register here: `FMA d == (a + 1) * d - 1, hint ` / `J a`: Jump. Can be to a register, memory content, or absolute address, depending on the addressing mode of `a`, even relative to PC: `FMA PC == a, hint out` / `JZA imm`: Jump if ZERO, absolute target address: `FMA PC == (ZERO)*(-1*PC+(imm-1))+(1*PC+1), hint out` / `JZR a`: Jump if ZERO, PC-relative target address: `FMA PC == (ZERO) * (a - 1) + (PC + 1), hint out` diff --git a/spec/src/field_vm.toml b/spec/src/field_vm.toml index 67ef6b7a5..d6c70709d 100644 --- a/spec/src/field_vm.toml +++ b/spec/src/field_vm.toml @@ -10,25 +10,25 @@ pad = 0 # TODO? Make this a reserved address containing the self loop [[variables.input]] name = "argument_registers" type = ["BaseField", 4] -desc = "The register numbers of the arguments `o`, `a`, `b`, `c`, in that order" +desc = "The register numbers of the arguments `d`, `a`, `b`, `c`, in that order" pad = ["arr", 1, 1, 1, 1] [[variables.input]] name = "argument_scalars" type = ["BaseField", 4] -desc = "The `imm_0` scalars for the arguments `o`, `a`, `b`, `c`, in that order" +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 `o`, `a`, `b`, `c`, in that order" +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 (`o`, `a`, `b`, `c`, in that order) comes from a memory lookup" +desc = "Whether the argument (`d`, `a`, `b`, `c`, in that order) comes from a memory lookup" pad = 0 [[variables.input]] From 186a681e13354d3cb51ef31319d3437c3843d0b3 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 14 Sep 2026 15:32:59 +0200 Subject: [PATCH 11/22] More elaborate VM architecture to intro --- spec/chapters/field_vm.typ | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index 3bcd03405..21e4adc64 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -9,12 +9,32 @@ 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 that 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 +#rj[Clarify state and registers being part of the state; state vs instruction] The VM has a state consisting of $N$ general purpose extension field registers, a base-field `PC` register, and a bit-register `ZERO`. The number of registers was chosen as a tradeoff between the versatility of having more mutable state, From c447faaf2dd7e26e5c013090a4f25fb220f8f3a7 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 15 Sep 2026 13:46:01 +0200 Subject: [PATCH 12/22] Instructions vs states --- spec/chapters/field_vm.typ | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index 21e4adc64..c9acfe000 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -1,6 +1,9 @@ #import "/meta.typ": rj, aside #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 +#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. @@ -34,9 +37,20 @@ into _input hinting_ and _output hinting_ --- described further below. == Arguments and addressing -#rj[Clarify state and registers being part of the state; state vs instruction] -The VM has a state consisting of $N$ general purpose extension field registers, -a base-field `PC` register, and a bit-register `ZERO`. +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 _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$. #rj[Register index for `ZERO` = $0$ and `PC` = $1$ and gp register `Ri` = $i + 2$] @@ -54,8 +68,8 @@ Every other register can hold an arbitrary extension field element. == Register hints -Each general-purpose register in the current state can be marked as _hinted_ in an instruction. -This means that its value from the current instruction onward can get a new value +Each general-purpose register in the current state can be marked as _hinted_ by the acting instruction. +This means that from the current state onwards, the register can take a value that is independent from the previous value, except as constrained by the instruction. Additionally, the _output_ can be marked as hinted, meaning that the register used in the `d` argument --- whether wrapped in a `MEM[]` lookup or not --- will change in the future state, and as such in the `d` argument too. @@ -68,7 +82,7 @@ with the appropriate exceptions in behaviour for the `ZERO` and `PC` registers. #aside("Hint collisions")[ One may observe that an output hint for state `i` and an input hint on state `i + 1` can affect -an identical register in an identical state. +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, and as such, hinting collisions can be easily identified, and most actual programs From 09e64bef5003383a347f58c4a58ad5f4baa0d09d Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 15 Sep 2026 13:47:55 +0200 Subject: [PATCH 13/22] Registers and hinting --- spec/chapters/field_vm.typ | 68 +++++++++++++++++++++++++++----------- 1 file changed, 48 insertions(+), 20 deletions(-) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index c9acfe000..b698cd49c 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -53,39 +53,66 @@ 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$. -#rj[Register index for `ZERO` = $0$ and `PC` = $1$ and gp register `Ri` = $i + 2$] +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, +and --- except when branches are taken, through register hinting --- is incremented by one +for every consecutive state. +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 forms: - $#`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. -That is, the state from which the next instruction will get its input register values. -The `ZERO` register of the future state contains a bit (as a base field element) that indicates whether or not -the `d` value was zero for the current instruction. -The `PC` register contains the program counter (as a base field element) and indicates which instruction is to be executed. -Every other register can hold an arbitrary extension field element. +The `d` argument to the instruction obtains its register value from the future state. -== Register hints +== Register hinting Each general-purpose register in the current state can be marked as _hinted_ by the acting instruction. This means that from the current state onwards, the register can take a value that is independent from the previous value, except as constrained by the instruction. -Additionally, the _output_ can be marked as hinted, meaning that the register used in the `d` argument --- -whether wrapped in a `MEM[]` lookup or not --- will change in the future state, and as such in the `d` argument too. -Output hinting is commonly used to assign the result of a computation: `FMA X == X * X, hint out` would -compute $#`X` dot #`X`$ and assign the result to `X` in the future state. -The output hint, in contradiction with the input hints, does allow `PC` to be hinted, so as to enable -causal jumps and control flow in the program. -Any register that is not hinted will have the same value in the future state as in the current state, +Additionally, the _output_ can be marked as hinted, meaning that the register used in the `d` argument +will change from the future state onwards, and as such in the `d` argument too. +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 provide 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, -and as such, hinting collisions can be easily identified, and most actual programs +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`. @@ -135,7 +162,7 @@ as experience may point out further useful abstractions. Eventually, we hope that a set of common pseudoinstructions can be extracted from actual usage, and inform potential optimizations that remove unused capabilities (e.g. reducing the number of immediates involved). -== Calling convention +== 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_, @@ -225,12 +252,13 @@ Finally, 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: -- $!#`hint_input`'_r and !#`hint_output` => #`registers`'_r = #`registers`_r$, `r` could not have been hinted, +- $!#`hint_input`'_r and !#`hint_output` => #`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 the next `r` should remain the same. -- $!#`hint_input`'_r and f_(r)(#`argument_registers`_0) = 0 => #`registers`'_r = #`registers`_r$ +- $!#`hint_input`'_r and f_(r)(#`argument_registers`_0) = 0 => #`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 $!#`hint_input`'_r and not (#`hint_output` and f_(r)(#`argument_registers`_0) = 1) => #`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 $#`pc`' = #`pc` + 1$ if it is not (output-)hinted, and $#`ZERO`'$ purely depends on $#`args`_0$ and not on `ZERO`. From 0ed78ce1531c543499b6a4ea0faf29b683126117 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 15 Sep 2026 13:48:15 +0200 Subject: [PATCH 14/22] pseudoinstructions as a table --- spec/chapters/field_vm.typ | 27 ++++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index b698cd49c..83294c5c5 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -150,17 +150,22 @@ 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. -/ `ADD d, a, b`: Addition: `FMA d == (0 * X + 1) * a + b, hint out` -/ `MUL d, a, b`: Multiplication: `FMA d == a * b + (0 * X), hint out` -/ `INV d, a`: Extension field inversion. Note: `d` and `a` cannot use the same register here: `FMA d == (a + 1) * d - 1, hint ` -/ `J a`: Jump. Can be to a register, memory content, or absolute address, depending on the addressing mode of `a`, even relative to PC: `FMA PC == a, hint out` -/ `JZA imm`: Jump if ZERO, absolute target address: `FMA PC == (ZERO)*(-1*PC+(imm-1))+(1*PC+1), hint out` -/ `JZR a`: Jump if ZERO, PC-relative target address: `FMA PC == (ZERO) * (a - 1) + (PC + 1), hint out` -/ `JNZA imm`: Jump if not ZERO, absolute target address: `FMA PC == ZERO * (PC - imm) + (ZERO + imm), hint out` -/ `JNZR a`: Jump if not ZERO, PC-relative target address: `FMA PC == (a - 1) * (-1 * ZERO + 1) + (PC + 1), hint out` - -Eventually, we hope that a set of common pseudoinstructions can be extracted from actual usage, -and inform potential optimizations that remove unused capabilities (e.g. reducing the number of immediates involved). +#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][ + `MUL d, a, b`][`FMA d == a * b + (0 * X), hint out`][Multiplication][ + `INV d, a`][`fma d == (a + 1) * d - 1, hint `][extension field inversion. note: `d` and `a` cannot use the same register here][ + `J a`][`FMA PC == a, hint out`][Jump. Can be to a register, memory content, or absolute address, depending on the addressing mode of `a`, even relative to PC][ + `JZA imm`][`FMA PC == (ZERO)*(-1*PC+(imm-1))+(1*PC+1), hint out`][Jump if ZERO, absolute target address][ + `JZR a`][`FMA PC == (ZERO) * (a - 1) + (PC + 1), hint out`][Jump if ZERO, PC-relative target address][ + `JNZA imm`][`FMA PC == ZERO * (PC - imm) + (ZERO + imm), hint out`][Jump if not ZERO, absolute target address][ + `JNZR a`][`FMA PC == (a - 1) * (-1 * ZERO + 1) + (PC + 1), hint out`][Jump if not ZERO, PC-relative target address] + +Eventually, usage may inform a set of common pseudoinstructions, +along with inform potential optimizations that remove unused capabilities +(e.g. reducing the number of immediates involved). == Calling convention From c49f79659066877d1866b58caaf74477c931dcad Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 15 Sep 2026 13:48:34 +0200 Subject: [PATCH 15/22] Clarify negative offsets into frame --- spec/chapters/field_vm.typ | 2 ++ 1 file changed, 2 insertions(+) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index 83294c5c5..b09829a61 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -172,6 +172,8 @@ along with inform potential optimizations that remove unused capabilities 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`, one of the general purpose registers. +Observe that we let `fp` point into the middle of the frame, such that the information relevant to the callee +starts at offset 0. In this frame, the following data is stored: / `MEM[fp - k]...MEM[fp - 1]`: `k` saved registers from the calling function From f014a2edf194bfde40787fdbc3fe260300edad15 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 15 Sep 2026 13:49:00 +0200 Subject: [PATCH 16/22] clarify syntactic degree being too high for mux --- spec/chapters/field_vm.typ | 22 +++++++++++++++++----- spec/src/field_vm.toml | 2 ++ 2 files changed, 19 insertions(+), 5 deletions(-) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index b09829a61..d5f7b74b0 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -234,12 +234,24 @@ 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 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. -#rj[Analysis of relation between $d$, $N$, $t$; mention current choice of $(d, N, t) = (5, 5, 1)$] -Observe that the handling for `argument_registers[0]` is separate, as this represents the output argument, -which should take its values from the next row in the table. +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 $op("deg") f_(i) = d - 1 + t dot (d - 2) - 1$ for a maximal number of registers $N + 2 <= op("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][5] = 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") diff --git a/spec/src/field_vm.toml b/spec/src/field_vm.toml index d6c70709d..967ad4d22 100644 --- a/spec/src/field_vm.toml +++ b/spec/src/field_vm.toml @@ -136,6 +136,7 @@ constraint = "$#`args_premem`_i = #`argument_offsets`_i + #`argument_scalars`_i # 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", "k"], "i"], ["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" @@ -143,6 +144,7 @@ kind = "arith" 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", "k"], 0], ["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" From fae3ab7f2e6fb84112c3af5cee3aa018cd594237 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 15 Sep 2026 14:34:07 +0200 Subject: [PATCH 17/22] typo --- spec/chapters/field_vm.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index d5f7b74b0..348da4477 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -256,7 +256,7 @@ as this represents the output argument, which should take its values from the ne #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 case of the `ExtField` value into `BaseField` is mostly technical here, as a means to make the signature look reasonable. +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. From 1fbfdd8b16cf5c7a80c963b7beff1e694101dcff Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 15 Sep 2026 15:18:02 +0200 Subject: [PATCH 18/22] Switch everything to next(...) notation --- spec/chapters/field_vm.typ | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index 348da4477..833cb806d 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -271,15 +271,15 @@ Finally, 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: -- $!#`hint_input`'_r and !#`hint_output` => #`registers`'_r = #`registers`_r$,\ `r` could not have been hinted, +- $!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 the next `r` should remain the same. -- $!#`hint_input`'_r and f_(r)(#`argument_registers`_0) = 0 => #`registers`'_r = #`registers`_r$,\ +- $!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 $!#`hint_input`'_r and not (#`hint_output` and f_(r)(#`argument_registers`_0) = 1) => #`registers`'_r = #`registers`_r$, but expressed in a way that polynomial constraints can more easily handle. +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 $#`pc`' = #`pc` + 1$ if it is not (output-)hinted, -and $#`ZERO`'$ purely depends on $#`args`_0$ and not on `ZERO`. +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") From f3f282fd95bf357da7dd473a7177bbaf8cb0f7c8 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Thu, 17 Sep 2026 12:22:19 +0200 Subject: [PATCH 19/22] Compression in the decode lookup --- spec/chapters/field_vm.typ | 38 ++++++++++++++---- spec/src/field_vm.toml | 79 +++++++++++++++++++++++++++++++++++++- spec/src/signatures.toml | 3 +- 3 files changed, 109 insertions(+), 11 deletions(-) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index 833cb806d..96743dc08 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -214,11 +214,7 @@ The #fieldvm is comprised of #nr_variables variables that are expressed using #n == Constraints -We first decode the instruction at the current PC. - -#render_constraint_table(chip, config, groups: "decode") - -Then, we compute all values $#`imm`_0 dot #`reg` + #`imm`_1$, +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[ @@ -267,8 +263,7 @@ Now everything is in place to check the core operation of the VM: the FMA constr #render_constraint_table(chip, config, groups: "fma") -Finally, we must ensure the consistency between consecutive rows of the table, -and allow for hinting. +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, @@ -283,6 +278,34 @@ 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]$, +which upon first attempt cannot be checked with a constraint of degree $<= d$. +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 $op("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") + == Padding #rj[...] @@ -294,5 +317,4 @@ and $next("ZERO")$ purely depends on $#`args`_0$ and not on `ZERO`. - 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 -- The `FIELD_VM_DECODE` table can be further compressed, including potentially fitting multiple base field elements into single extension field elements - 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/src/field_vm.toml b/spec/src/field_vm.toml index 967ad4d22..faf1e23a0 100644 --- a/spec/src/field_vm.toml +++ b/spec/src/field_vm.toml @@ -104,13 +104,90 @@ 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)$ +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)$" +# 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", "argument_registers", "argument_scalars", "argument_offsets", "mem_flags", "hint_input", "hint_output"] +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]] diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index 0c6f0e8f5..2cae7b670 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -248,5 +248,4 @@ output = "ExtField" [[signatures]] kind = "interaction" tag = "FIELD_VM_DECODE" -# PARAM: ["BaseField", ["BaseField", 4], ["BaseField", 4], ["BaseField", 4], ["Bit", 4], ["Bit", N], "Bit"] -input = ["BaseField", ["BaseField", 4], ["BaseField", 4], ["BaseField", 4], ["Bit", 4], ["Bit", 5], "Bit"] +input = ["ExtField", "ExtField", "ExtField", "ExtField"] From b9f413479b295326be88639b9041f74dfabe0c61 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Thu, 17 Sep 2026 13:41:51 +0200 Subject: [PATCH 20/22] padding --- spec/chapters/field_vm.typ | 22 +++++++++++++++++----- spec/src/field_vm.toml | 14 +++++++------- 2 files changed, 24 insertions(+), 12 deletions(-) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index 96743dc08..d5fea5e69 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -1,6 +1,6 @@ -#import "/meta.typ": rj, aside +#import "/meta.typ": aside #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 +#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)) @@ -195,7 +195,9 @@ RET: FMA PC == [fp + 1], hint out ``` -#rj[Figure out halting, can be a simple self-loop, just have to figure out how to have the verifier assert this] +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 R_1, ..., hint R_N` 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 @@ -245,7 +247,7 @@ 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][5] = 0` for $k != 0$ (by construction of the $f_(j,k)$ polynomials), we stay at a total degree $d$. +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. @@ -306,9 +308,19 @@ 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 -#rj[...] +The halting self-loop also functions as a padding state. + +#render_chip_padding_table(chip, config) = Notes and potential optimizations diff --git a/spec/src/field_vm.toml b/spec/src/field_vm.toml index faf1e23a0..e43064226 100644 --- a/spec/src/field_vm.toml +++ b/spec/src/field_vm.toml @@ -5,13 +5,13 @@ code = "FVM" name = "pc" type = "BaseField" desc = "The program counter" -pad = 0 # TODO? Make this a reserved address containing the self loop +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, 1, 1, 1] +pad = ["arr", 1, 0, 0, 1] [[variables.input]] name = "argument_scalars" @@ -35,7 +35,7 @@ pad = 0 name = "hint_input" type = ["Bit", 5] # PARAM: ["Bit", N] desc = "Whether each input register is hinted this cycle" -pad = 0 +pad = ["arr", 1, 1, 1, 1, 1] # PARAM: N long [[variables.input]] name = "hint_output" @@ -53,7 +53,7 @@ pad = 0 name = "ZERO" type = "Bit" desc = "Whether the output of the previous instruction was zero" -pad = 0 +pad = 1 [[variables.auxiliary]] name = "out_inverse" @@ -65,19 +65,19 @@ pad = 0 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", ["arr", 1], ["arr", 1], ["arr", 1], ["arr", 1]] +pad = ["arr", 1, 1, 1, 1] [[variables.auxiliary]] name = "args_premem" type = ["ExtField", 4] desc = "The argument values, before a potential memory lookup" -pad = ["arr", ["-", 1], 0, 0, ["-", 1]] +pad = 0 [[variables.auxiliary]] name = "args" type = ["ExtField", 4] desc = "The argument values, after a potential memory lookup" -pad = ["arr", ["-", 1], 0, 0, ["-", 1]] +pad = 0 [[variables.virtual]] name = "all_regs" From 3b942febc189a8ab7e6d04e3e915c0237e605e72 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Thu, 17 Sep 2026 14:12:33 +0200 Subject: [PATCH 21/22] Decode table --- spec/chapters/field_vm.typ | 2 +- spec/chapters/field_vm_decode.typ | 25 ++++++++- spec/src/field_vm_decode.toml | 87 +++++++++++++++++++++++++++++++ 3 files changed, 112 insertions(+), 2 deletions(-) create mode 100644 spec/src/field_vm_decode.toml diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index d5fea5e69..26a92fa20 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -10,7 +10,7 @@ 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 += 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. diff --git a/spec/chapters/field_vm_decode.typ b/spec/chapters/field_vm_decode.typ index 1333ed77b..0dfb91c18 100644 --- a/spec/chapters/field_vm_decode.typ +++ b/spec/chapters/field_vm_decode.typ @@ -1 +1,24 @@ -TODO +#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("/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/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 = ["-", "μ"] From 38faf798121930926deff26032a19d0c8205e33d Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Thu, 17 Sep 2026 14:33:27 +0200 Subject: [PATCH 22/22] Minor --- spec/chapters/field_vm.typ | 6 +++--- spec/src/field_vm.toml | 10 +++++----- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/spec/chapters/field_vm.typ b/spec/chapters/field_vm.typ index 26a92fa20..687214163 100644 --- a/spec/chapters/field_vm.typ +++ b/spec/chapters/field_vm.typ @@ -156,7 +156,7 @@ as experience may point out further useful abstractions. table.header[*Pseudoinstr.*][*Translation*][*Comment*], table.hline(stroke: 1.5pt))[ `ADD d, a, b`][`FMA d == (0 * X + 1) * a + b, hint out`][Addition][ `MUL d, a, b`][`FMA d == a * b + (0 * X), hint out`][Multiplication][ - `INV d, a`][`fma d == (a + 1) * d - 1, hint `][extension field inversion. note: `d` and `a` cannot use the same register here][ + `INV d, a`][`FMA d == (a + 1) * d - 1, hint `][Extension field inversion. Note: `d` and `a` cannot use the same register here, and `d` should not be input-hinted in the next instruction.][ `J a`][`FMA PC == a, hint out`][Jump. Can be to a register, memory content, or absolute address, depending on the addressing mode of `a`, even relative to PC][ `JZA imm`][`FMA PC == (ZERO)*(-1*PC+(imm-1))+(1*PC+1), hint out`][Jump if ZERO, absolute target address][ `JZR a`][`FMA PC == (ZERO) * (a - 1) + (PC + 1), hint out`][Jump if ZERO, PC-relative target address][ @@ -164,7 +164,7 @@ as experience may point out further useful abstractions. `JNZR a`][`FMA PC == (a - 1) * (-1 * ZERO + 1) + (PC + 1), hint out`][Jump if not ZERO, PC-relative target address] Eventually, usage may inform a set of common pseudoinstructions, -along with inform potential optimizations that remove unused capabilities +along with informing potential optimizations that remove unused capabilities (e.g. reducing the number of immediates involved). == Calling convention @@ -196,7 +196,7 @@ RET: ``` 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 R_1, ..., hint R_N` at that address. +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 diff --git a/spec/src/field_vm.toml b/spec/src/field_vm.toml index e43064226..568c31cb4 100644 --- a/spec/src/field_vm.toml +++ b/spec/src/field_vm.toml @@ -65,7 +65,7 @@ pad = 0 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, 1, 1, 1] +pad = ["arr", 1, 0, 0, 1] [[variables.auxiliary]] name = "args_premem" @@ -82,7 +82,7 @@ pad = 0 [[variables.virtual]] name = "all_regs" type = ["ExtField", 7] # PARAM: ["ExtField", N + 2] -desc = "All general purpose registers, followed by `pc` and `ZERO`, matching the decoding indices" +desc = "All registers, in register index order" def = {polys = [ {iter = ["i", 0], poly = ["cast", "ZERO", "ExtField"]}, {iter = ["i", 1], poly = ["cast", "pc", "ExtField"]}, @@ -92,7 +92,7 @@ def = {polys = [ [[variables.virtual]] name = "arg_register_powers" type = [["BaseField", 2], 4] # PARAM: [["BaseField", T + 1], 4] -desc = "A virtual wrapper aroung `arg_reg_pows_computed` to have a 1 at index 0" +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]] @@ -210,7 +210,7 @@ iter = ["i", 0, 3] 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", "k"], "i"], ["sum", ["=", "l", 0], ["-", "d", 2], ["*", ["^", ["idx", "argument_registers", "i"], "l"], ["idx", ["idx", ["idx", "MUX", "l"], "k"], "j"]]]]]]]]] +# 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" @@ -219,7 +219,7 @@ ref = "field-VM:c:first-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", "k"], 0], ["sum", ["=", "l", 0], ["-", "d", 2], ["*", ["^", ["idx", "argument_registers", 0], "l"], ["idx", ["idx", ["idx", "MUX", "l"], "k"], "j"]]]]]]]]] +# 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"