From 03131e530cf1f482f0288b1aa62978439fe15f7e Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 8 Sep 2026 11:17:11 +0200 Subject: [PATCH 1/7] 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 2/7] 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 3/7] 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 4/7] 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 5/7] 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 6/7] 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 7/7] 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")