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..84e94ebec --- /dev/null +++ b/spec/chapters/field_vm.typ @@ -0,0 +1,220 @@ +#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`. +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 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. +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 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. +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, +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 input-hinted, so no collision is possible there. +] + +== Instruction notation + +A potential way to write down an FMA instruction would be the following: +``` +FMA [1 * X + 2] == [3 * Y + 4] * (5 * Z) + [W + 6], hint out + Z +``` + +- `[]` indicate memory access +- `()` indicate grouping to separate the arguments +- `X, Y, Z, W` are placeholder register names +- `hint` notation indicates which registers are hinted (default unhinted), `hint out` means hinting `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 --- +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 == (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). + +== 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 to first compute the values of +$#`argument_registers[i]`^(d - 1)$, $#`argument_registers[i]`^(2d - 3)$ and so on +to `arg_register_powers` with constraints of degree $<= d$, +and then compute $#`args_premem[i]` = #`argument_scalars[i]` dot sum_(j = 0)^(N + 1) #`registers[j]` dot f_(j)(#`argument_registers[i]`) + #`argument_offsets[i]`$. +The coefficients for all $f_(i, k)$ are pre-computed once, based on the choices of `N`, `d` and `t`, +and used through the `MUX` constant columns. +#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. +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. + +#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 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. + +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") + +== 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: + - 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..a984ecd60 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..67ef6b7a5 --- /dev/null +++ b/spec/src/field_vm.toml @@ -0,0 +1,216 @@ +name = "FIELD_VM" +code = "FVM" + +[[variables.input]] +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 = ["cast", "ZERO", "ExtField"]}, + {iter = ["i", 1], poly = ["cast", "pc", "ExtField"]}, + {iter = ["i", 2, 6], poly = ["idx", "registers", ["-", "i", 2]]}, # PARAM: iter = ["i", 2, N + 1] +]} + +[[variables.virtual]] +name = "arg_register_powers" +type = [["BaseField", 2], 4] # PARAM: [["BaseField", T + 1], 4] +desc = "A virtual wrapper 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", "i"], ["-", "j", 1]]} # PARAM: iters = ["i", 0, 3], ["j", 1, T]] + ]} + +[[variables.constant]] +name = "MUX" +type = [[["BaseField", 4], 2], 7] # PARAM: [[["BaseField", d - 1], t + 1], N + 2] +desc = "The MUX polynomial coefficients" +pad = ["arr", 1, 1, 1, 1, 1, 1, 1] # Slightly hacky way to make the typechecker not crash out on the pc constraint + +[[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) = #`argument_registers`_i^4$" # PARAM: power = d - 1 +poly = ["-", ["idx", ["idx", "arg_reg_pows_computed", "i"], 0], + ["*", + ["idx", "argument_registers", "i"], + ["idx", "argument_registers", "i"], + ["idx", "argument_registers", "i"], + ["idx", "argument_registers", "i"]]] +iter = ["i", 0, 3] + +# PARAM: If T > 1, we need to populate arg_reg_pows_computed[i][j], j > 0, too, with power j * (d - 2) + (d - 1) + +[[constraints.mux]] +kind = "arith" +# PARAM: $#`args_premem`_i = #`argument_offsets`_i + #`argument_scalars`_i dot limits(sum)_(j = 0)^(N + 1) #`all_regs`_j dot (limits(sum)_(k = 0)^T #`arg_register_powers`_(i,k) dot (limits(sum_(l = 0)^(d - 2) #`argument_registers`_i^l dot #`MUX`_(j,k,l)))$ +constraint = "$#`args_premem`_i = #`argument_offsets`_i + #`argument_scalars`_i dot limits(sum)_(j = 0)^6 #`all_regs`_j dot (limits(sum)_(k = 0)^1 #`arg_register_powers`_(i,k) dot (limits(sum)_(l = 0)^3 #`argument_registers`_i^l dot #`MUX`_(j,k,l)))$" +# PARAM: ["-", ["idx", "args_premem", "i"], ["idx", "argument_offsets", "i"], ["*", ["idx", "argument_scalars", "i"], ["sum", ["=", "j", 0], ["+", "N", 1], ["*", ["idx", "all_regs", "j"], ["sum", ["=", "k", 0], "T", ["*", ["idx", ["idx", "arg_register_powers", "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 = "FIELD_VM_MEM" +input = [["cast", ["idx", "args_premem", "i"], "BaseField"]] +output = ["idx", "args", "i"] +multiplicity = ["idx", "mem_flags", "i"] +iter = ["i", 0, 3] + +[[constraint_groups]] +name = "fma" + +[[constraints.fma]] +kind = "arith" +constraint = "$#`args[0]` = #`args[1]` dot #`args[2]` + #`args[3]`$" +poly = ["-", ["idx", "args", 0], + ["*", ["idx", "args", 1], ["idx", "args", 2]], + ["idx", "args", 3]] + +[[constraint_groups]] +name = "transition" + +[[constraints.transition]] +kind = "arith" +constraint = "$!#`hint_input`'_i and !#`hint_output` => #`registers`'_i = #`registers`_i$" +poly = ["*", ["not", ["idx", ["next", "hint_input"], "i"]], ["not", "hint_output"], ["-", ["idx", ["next", "registers"], "i"], ["idx", "registers", "i"]]] +iter = ["i", 0, 4] # PARAM: ["i", 0, N - 1] + +[[constraints.transition]] +kind = "arith" +# PARAM: $!#`hint_input`'_i and !(limits(sum)_(j = 0)^T #`arg_register_powers`_(0,j) dot limits(sum)_(k = 0)^(d - 2) #`MUX`_(i+2,j,k) dot #`argument_registers`_0^k) => #`registers`'_i = #`registers`_i$ +constraint = "$!#`hint_input`'_i and !(limits(sum)_(j = 0)^1 #`arg_register_powers`_(0,j) dot limits(sum)_(k = 0)^3 #`MUX`_(i+2,j,k) dot #`argument_registers`_0^k) => #`registers`'_i = #`registers`_i$" +# PARAM: ["*", ["not", ["idx", ["next", "hint_input"], "i"]], ["-", 1, ["sum", ["=", "j", 0], "T", ["*", ["idx", ["idx", "arg_register_powers", 0], "j"], ["sum", ["=", "k", 0], ["-", "d", 2], ["*", ["idx", ["idx", ["idx", "MUX", ["+", "i", 2]], "j"], "k"], ["^", ["idx", "argument_registers", 0], "k"]]]]]], ["-", ["idx", ["next", "registers"], "i"], ["idx", "registers", "i"]]] +poly = ["*", ["not", ["idx", ["next", "hint_input"], "i"]], ["-", 1, ["sum", ["=", "j", 0], 1, ["*", ["idx", ["idx", "arg_register_powers", 0], "j"], ["sum", ["=", "k", 0], 3, ["*", ["idx", ["idx", ["idx", "MUX", ["+", "i", 2]], "j"], "k"], ["^", ["idx", "argument_registers", 0], "k"]]]]]], ["-", ["idx", ["next", "registers"], "i"], ["idx", "registers", "i"]]] +iter = ["i", 0, 4] # PARAM: ["i", 0, N - 1] + +[[constraints.transition]] +kind = "arith" +constraint = "$!#`hint_output` => #`pc`' = #`pc` + 1$" +poly = ["*", ["not", "hint_output"], ["-", ["next", "pc"], "pc", 1]] + +[[constraints.transition]] +kind = "arith" +# PARAM: $!(limits(sum)_(j = 0)^1 #`arg_register_powers`_(0,j) dot limits(sum)_(k = 0)^3 #`MUX`_(1,j,k) dot #`argument_registers`_0^k) => #`pc`' = #`pc` + 1$ +constraint = "$!(limits(sum)_(j = 0)^1 #`arg_register_powers`_(0,j) dot limits(sum)_(k = 0)^3 #`MUX`_(1,j,k) dot #`argument_registers`_0^k) => #`pc`' = #`pc` + 1$" +# PARAM: ["*", ["-", 1, ["sum", ["=", "j", 0], "T", ["*", ["idx", ["idx", "arg_register_powers", 0], "j"], ["sum", ["=", "k", 0], ["-", "d", 2], ["*", ["idx", ["idx", ["idx", "MUX", 1], "j"], "k"], ["^", ["idx", "argument_registers", 0], "k"]]]]]], ["-", ["next", "pc"], ["+", "pc", 1]]] +poly = ["*", ["-", 1, ["sum", ["=", "j", 0], 1, ["*", ["idx", ["idx", "arg_register_powers", 0], "j"], ["sum", ["=", "k", 0], 3, ["*", ["idx", ["idx", ["idx", "MUX", 1], "j"], "k"], ["^", ["idx", "argument_registers", 0], "k"]]]]]], ["-", ["next", "pc"], ["+", "pc", 1]]] + +[[constraints.transition]] +kind = "template" +tag = "IS_BIT" +input = ["ZERO"] + +[[constraints.transition]] +kind = "arith" +constraint = "$#`ZERO`' => #`args`_0 = 0$" +poly = ["*", ["next", "ZERO"], ["idx", "args", 0]] + +[[constraints.transition]] +kind = "arith" +constraint = "$!#`ZERO`' => #`args`_0 dot #`out_inverse` = 1$" +poly = ["*", ["not", ["next", "ZERO"]], ["-", 1, ["*", ["idx", "args", 0], "out_inverse"]]] diff --git a/spec/src/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 fe36b2f39..ea017de61 100644 --- a/spec/tooling/chip.py +++ b/spec/tooling/chip.py @@ -46,7 +46,7 @@ def asserts(self, condition: bool, message: str): def assert_no_unexpected(data: dict, possible_keys: Iterable[str]): - for key in data.keys(): + for key in data: reporter.asserts(key in possible_keys, f"Unexpected key: {key!r}") @@ -70,16 +70,23 @@ def get_const(self) -> int: return self.low -type Type = list[Type] | Range +@dataclass(frozen=True) +class Opaque: + tag: str + + +type Type = list[Type] | Range | Opaque DEFAULT_TYPE: Type = Range.const(0) def structure_matches(a: Type, b: Type) -> bool: - if isinstance(a, Range) and isinstance(b, (Range, type(None))): + if isinstance(a, Range) and isinstance(b, Range): return True elif isinstance(a, list) and isinstance(b, list): return len(a) == len(b) and all(structure_matches(x, y) for x, y in zip(a, b)) + elif isinstance(a, Opaque) and isinstance(b, Opaque): + return a.tag == b.tag else: return False @@ -87,9 +94,12 @@ def structure_matches(a: Type, b: Type) -> bool: def constant_fits(cst: int, target: Type) -> bool: if isinstance(target, Range): return target.low <= cst <= target.high - else: + elif isinstance(target, list): return constant_fits(cst, target[0]) - + else: + assert isinstance(target, Opaque) + # Let's assume this fits in an opaque + return True type Expr = ( LitExpr @@ -104,6 +114,7 @@ def constant_fits(cst: int, target: Type) -> bool: | PowExpr | SumExpr | NotExpr + | NextExpr | DummyExpr ) @@ -162,7 +173,7 @@ def typecheck(self, env: Environment) -> Type: reporter.error(f"Invalid index: {idx!r}") return Range.const(-1) idxconst = idx.get_const() - if isinstance(base, Range): + if not isinstance(base, list): reporter.error(f"Indexing into non-array type: {self!r}") return DEFAULT_TYPE if not (0 <= idxconst < len(base)): @@ -195,12 +206,17 @@ def typecheck(self, env: Environment) -> Type: CastExpr(LitExpr(base.get_const() if i == 0 else 0), t).typecheck(env) for i, t in enumerate(self.type) ] + elif isinstance(self.type, Opaque): + return self.type return base if isinstance(base, list) and all(b == Range.const(0) for b in base): # Workaround for casts of constant zero, to make padding work nicely # This may become cleaner if we eventually get to the cast rework from #326 if isinstance(self.type, Range): return Range.const(0) + elif isinstance(self.type, Opaque): + # We assume this works for an opaque type, as it's an explicit cast + return self.type else: return [CastExpr(LitExpr(0), t).typecheck(env) for t in self.type] return self.type @@ -214,10 +230,17 @@ def typecheck_binop(self, a: Type, b: Type) -> Type: if isinstance(a, list) and isinstance(b, list): reporter.error(f"Multiplication of non-scalar types: {self!r}") return DEFAULT_TYPE - elif not isinstance(a, Range): + elif isinstance(a, list): return [self.typecheck_binop(x, b) for x in a] elif isinstance(b, list): return self.typecheck_binop(b, a) + elif isinstance(a, Opaque): + if isinstance(b, Opaque): + reporter.asserts(a.tag == b.tag, f"Multiplication of two distinct opaque types: {self!r}") + # Works to multiply with a constant/Range + return a + elif isinstance(b, Opaque): + return self.typecheck_binop(b, a) else: extrema = [x * y for x in [a.low, a.high] for y in [b.low, b.high]] return Range(min(extrema), max(extrema)) @@ -243,6 +266,13 @@ def typecheck_binop(self, a: Type, b: Type) -> Type: elif isinstance(a, list) or isinstance(b, list): reporter.error(f"Adding of scalar and array types {self!r}") return DEFAULT_TYPE + elif isinstance(a, Opaque): + if isinstance(b, Opaque): + reporter.asserts(a.tag == b.tag, f"Addition of two distinct opaque types: {self!r}") + # Still works adding Ranges to it + return a + elif isinstance(b, Opaque): + return self.typecheck_binop(b, a) else: return Range(a.low + b.low, a.high + b.high) @@ -270,16 +300,27 @@ def typecheck_binop(self, a: Type, b: Type) -> Type: elif isinstance(a, list) or isinstance(b, list): reporter.error(f"Subtraction of scalar and array types {self!r}") return DEFAULT_TYPE + elif isinstance(a, Opaque): + if isinstance(b, Opaque): + reporter.asserts(a.tag == b.tag, f"Subtraction of two distinct opaque types: {self!r}") + # We allow subtracting Ranges + return a + elif isinstance(b, Opaque): + # Flipping the order doesn't matter, as we're returning an Opaque anyway + return self.typecheck_binop(b, a) else: return Range(a.low - b.high, a.high - b.low) def typecheck(self, env: Environment) -> Type: t = self.head.typecheck(env) if not self.subs: - if not isinstance(t, Range): + if isinstance(t, Range): + return Range(-t.high, -t.low) + elif isinstance(t, Opaque): + return t + else: reporter.error(f"Negating a non-scalar type: {self!r}") return t - return Range(-t.high, -t.low) for term in self.subs: t = self.typecheck_binop(t, term.typecheck(env)) return t @@ -294,6 +335,10 @@ def typecheck(self, env: Environment) -> Type: elt = self.elt.typecheck(env) modulus = self.modulus.typecheck(env) + if isinstance(elt, Opaque) or isinstance(modulus, Opaque): + reporter.error(f"Cannot take a mod with opaque types: {self!r}") + return elt + if isinstance(modulus, list) or not modulus.is_const(): reporter.error(f"Invalid non-constant modulus: {self.modulus!r}") return Range.const(0) @@ -316,14 +361,27 @@ class PowExpr: def typecheck(self, env: Environment) -> Type: base = self.base.typecheck(env) exp = self.exp.typecheck(env) - if isinstance(base, list) or not base.is_const(): - reporter.error(f"Invalid exponentiation with non-const base: {self.base!r}") + if isinstance(base, list): + reporter.error(f"Invalid exponentiation of a list: {self.base!r}") return DEFAULT_TYPE - if isinstance(exp, list) or not exp.is_const(): + if not (isinstance(exp, Range) and exp.is_const()): reporter.error(f"Invalid exponentiation with non-const exponent: {self.exp!r}") return DEFAULT_TYPE - val = pow(base.get_const(), exp.get_const(), env.config.variables.prime) - return Range.const(val) + + if isinstance(base, Opaque): + return base + + # If const base, we have a const result + if base.is_const(): + return Range.const(pow(base.get_const(), exp.get_const(), env.config.variables.prime)) + # If we have no modular wrap, we have a correct range + e, p = exp.get_const(), env.config.variables.prime + small_pow = e * max(0, base.high.bit_length() - 1) <= p.bit_length() + if base.low >= 0 and small_pow and base.high ** e < p: + return Range(pow(base.low, e, p), pow(base.high, e, p)) + # Else, escape hatch to the full base type + else: + return Range(0, env.config.variables.prime - 1) @dataclass @@ -340,6 +398,12 @@ def typecheck_binop(self, a: Type, b: Type) -> Type: elif isinstance(a, list) or isinstance(b, list): reporter.error(f"Summing of scalar and array types {self!r}") return DEFAULT_TYPE + elif isinstance(a, Opaque): + if isinstance(b, Opaque): + reporter.asserts(a.tag == b.tag, f"Summation of two distinct opaque types: {self!r}") + return a + elif isinstance(b, Opaque): + return self.typecheck_binop(b, a) else: return Range(a.low + b.low, a.high + b.high) @@ -356,12 +420,20 @@ class NotExpr: def typecheck(self, env: Environment) -> Type: inner = self.inner.typecheck(env) - if isinstance(inner, list) or not inner.is_bool(): + if not (isinstance(inner, Range) and inner.is_bool()): reporter.error(f"Not a bool passed to `not`: {self.inner!r}") return Range(0, 1) return Range(1 - inner.high, 1 - inner.low) +@dataclass +class NextExpr: + inner: VarExpr + + def typecheck(self, env: Environment) -> Type: + return self.inner.typecheck(env) + + @dataclass class DummyExpr: def typecheck(self, _env: Environment) -> Type: @@ -404,6 +476,10 @@ def build_expr(config: Optional["Config"], data: object) -> Expr: return SumExpr(Iter(config, var, start, stop), build_expr(config, terms)) case ["not", e]: return NotExpr(build_expr(config, e)) + case ["next", str(var)]: + inner = build_expr(config, var) + assert isinstance(inner, VarExpr), f"Invalid transition variable: {var!r}" + return NextExpr(inner) case other: reporter.error(f"Unknown expression: {other!r}") return DummyExpr() @@ -435,11 +511,11 @@ def __init__(self, config: "Config", name: str, start: object, stop: object): def typecheck[T](self, env: Environment, callback: Callable[[Environment], Iterable[T]]) -> Iterable[T]: start = self.start.typecheck(env) - if isinstance(start, list) or not start.is_const(): + if not (isinstance(start, Range) and start.is_const()): reporter.error(f"Starting value of iterator not a const: {self!r}") start = Range.const(0) stop = self.stop.typecheck(env) - if isinstance(stop, list) or not stop.is_const(): + if not (isinstance(stop, Range) and stop.is_const()): reporter.error(f"Ending value of iterator not a const: {self!r}") stop = Range.const(start.get_const()) @@ -482,12 +558,12 @@ def clean_iter(it): class TypeConfig: label: str subtypes: list[Type] - range: Optional[Range] + scalar_type: Range | Opaque | None desc: str preprocessed: bool def __init__(self, default_name: str, lookup: Callable[[str], Type], data: dict): - assert_no_unexpected(data, type(self).__annotations__.keys()) + assert_no_unexpected(data, type(self).__annotations__.keys() - {"scalar_type"} | {"range"}) self.label = data["label"] if "range" in data: reporter.asserts( @@ -506,16 +582,19 @@ def __init__(self, default_name: str, lookup: Callable[[str], Type], data: dict) reporter.error(f"Range end not an int: {data!r}") stop = start reporter.asserts(int(start) <= int(stop), f"Inverted range: {data!r}") - self.range = Range(int(start), int(stop)) + self.scalar_type = Range(int(start), int(stop)) + self.subtypes = [] + elif data["subtypes"] == [data["label"]]: + self.scalar_type = Opaque(data["label"]) self.subtypes = [] else: - self.range = None + self.scalar_type = None self.subtypes = [lookup(tp) for tp in data["subtypes"]] self.desc = data["desc"] self.preprocessed = data.get("preprocessed", False) def as_type(self) -> Type: - return self.range or self.subtypes[:] + return self.scalar_type or self.subtypes[:] @dataclass @@ -712,15 +791,15 @@ def handle_iters( # Some duplicated code/concepts from Iter.typecheck # But threading the extra needed state through overly complicates everything start = it.start.typecheck(env) - if isinstance(start, list) or not start.is_const(): + if not (isinstance(start, Range) and start.is_const()): reporter.error(f"Starting value of virtual def iter not a const: {self!r}") start = Range.const(0) stop = it.stop.typecheck(env) - if isinstance(stop, list) or not stop.is_const(): + if not (isinstance(stop, Range) and stop.is_const()): reporter.error(f"Ending value of virtual def iter not a const: {self!r}") stop = Range.const(start.get_const()) - if isinstance(expected, Range): + if not isinstance(expected, list): reporter.error(f"Virtual definition has an iter for a scalar: {self!r}") return @@ -747,7 +826,7 @@ def is_covered(seen: set[tuple], indices: list[int]) -> bool: return False def check_covered(t: Type, seen: set[tuple], indices: list[int]): - if isinstance(t, Range): + if not isinstance(t, list): reporter.asserts( is_covered(seen, indices), f"Virtual column {self.name!r} not completely defined", @@ -757,15 +836,24 @@ def check_covered(t: Type, seen: set[tuple], indices: list[int]): check_covered(elt, seen, indices + [i]) # Special case for better error messages - if isinstance(self.type, Range): + if not isinstance(self.type, list): reporter.asserts( len(self.def_.defs) == 1 and not self.def_.defs[0].iters, f"Invalid def for scalar column: {self!r}", ) assigned_type = self.def_.defs[0].poly.typecheck(env) - if not isinstance(assigned_type, Range): + if isinstance(assigned_type, list): reporter.error(f"Assigning non-scalar type to scalar virtual column: {self!r}") return self.type + + if isinstance(self.type, Range) and not isinstance(assigned_type, Range): + reporter.error(f"Incompatible virtual column type assignment: {self!r}") + return self.type + + if isinstance(self.type, Opaque) and (not isinstance(assigned_type, Opaque) or assigned_type.tag != self.type.tag): + reporter.error(f"Incompatible virtual column opaque type assignment: {self!r}") + return self.type + # Check type fits? # Leaving this out because it produces too much noise with one-hot assumptions # reporter.asserts(self.type.low <= assigned_type.low <= assigned_type.high <= self.type.high, f"Definition may not fit in virtual column: {self!r}") @@ -846,7 +934,7 @@ def check_includes_zero(t: Type): t.low <= 0 <= t.high, f"Unsatisfiable constraint, 0 not in range: {self!r} {t}", ) - else: + elif not isinstance(t, Opaque): reporter.error(f"Non-scalar value for polynomial constraint: {self!r} {t}") for t in all_iters(self.iters, env, lambda e: [self.poly.typecheck(e)]): @@ -857,9 +945,9 @@ def check_includes_zero(t: Type): @dataclass class Signature: tag: str - condition: Optional[Type] + condition: Type | None input: list[Type] - output: Optional[Type] + output: Type | None def matches(self, other: Self) -> bool: if not isinstance(other, type(self)): @@ -886,8 +974,8 @@ class InteractionLike: tag: str desc: str input: list[Expr] - output: Optional[Expr] - conditional: Optional[Expr] + output: Expr | None + conditional: Expr | None iters: list[Iter] def __init__(self, config: Config, data: dict): @@ -1081,7 +1169,7 @@ def check_assignment( values: dict[str, Type], ): reporter.asserts( - set(values.keys()) <= set(v.name for v in self.concrete_vars), + set(values.keys()) <= {v.name for v in self.concrete_vars}, f"Passing unrecognized variable to `check_assignment` of chip {self.name!r}", ) env = Environment(self.config, {}, {}) @@ -1109,7 +1197,7 @@ def check_assignment( def build_signature(config: Config, data: dict) -> Signature: assert_no_unexpected(data, {"tag", "kind", "input", "output", "cond"}) Sig: type[Signature] - cond: Optional[Type] = None + cond: Type | None = None match data["kind"]: case "template": if "cond" in data: