spec: Field VM

spec/chapters/ecsm.typ

@@ -12,8 +12,6 @@
 
 #let config = load_config()
 
-#show math.equation.where(block: false): box
-
 #let ecsm_chip = load_chip("src/ecsm.toml", config)
 #let ecsm = raw(ecsm_chip.name)
 

spec/chapters/field_vm_decode.typ

@@ -0,0 +1,24 @@
+#import "/src.typ": load_config, load_chip
+#import "/chip.typ": render_chip_variable_table, render_constraint_table
+#let config = load_config()
+#let chip = load_chip("/src/field_vm_decode.toml", config)
+#let decode = raw(chip.name)
+
+In this chapter, we provide a brief overview of the #decode chip,
+that corresponds to the instruction decoding for @field-VM.
+As the ISA from @field-VM:sec:isa was designed to have a simple mapping
+onto AIR tables, the decoding table is itself also simple.
+
+We present the table in its uncompressed form, but in practice, any
+implementation would materialize the _virtual_ and _multiplicity_ columns only,
+similar to the approach in @decode.
+Due to its relative simplicity, we do not present both compressed and uncompressed
+variants of the table separately.
+
+= Variables
+
+#render_chip_variable_table(chip, config)
+
+= Constraints
+
+#render_constraint_table(chip, config)

spec/chapters/limbs_and_carries.typ

@@ -4,7 +4,6 @@
 // Equation formatting
 #show: equate.with(breakable: true, sub-numbering: true, number-mode: "label")
 #set math.equation(numbering: "(1.1)")
-#show math.equation.where(block: false): box
 
 In this section, we discuss, in order, 
 + the multiplication and addition of limb-decomposed integers (involving carries), 

spec/chapters/recursion.typ

@@ -26,8 +26,6 @@
 #let prob = $PP$
 #let to = math.arrow.r
 
-#show math.equation.where(block: false): box
-
 #set list(marker: [---])
 
 = Proof recursion <proof-recursion>

spec/expr.typ

@@ -46,6 +46,7 @@
 //          | ["-", expr]                  ; -expr
 //          | ["-", expr1, expr2, ...]     ; expr1 - expr2 - ...
 //          | ["cast", expr, type]         ; expr as type
+//          | ["next", var]                ; var'
 // 
 // 
 // To limit the number of parentheses that are placed in an expression,
@@ -54,19 +55,20 @@
 
 #let PREC = (
   "MIN": -1, // <the most secret heart of any expression>
-  "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, // <the void outside every expression>
+  "next": 0, // var'
+  "idx": 1,  // []
+  "pow": 2,  // ^
+  "neg": 3,  // Unary -
+  "cast": 4, // cast
+  "mul": 5,  // *
+  "div": 6,  // /
+  "mod": 7,  // mod
+  "sum": 8,  // Σ
+  "not": 9,  // not
+  "sub": 10,  // -
+  "add": 11,  // +  
+  "eq": 12,   // = and :=
+  "MAX": 13, // <the void outside every expression>
 )
 
 // Mutual recursion through a trick from https://github.com/typst/typst/issues/744
@@ -114,7 +116,7 @@
       `⧼` + raw(e.at(1)) + `⧽`
     },
     "arr": (pp, rec, e) => `[` + e.slice(1).map(rec.with(PREC.MAX)).join(`, `) + `]`,
-    "idx": (pp, rec, e) => rec(PREC.MIN, e.at(1)) + `[` + rec(PREC.MAX, e.at(2)) + `]`,
+    "idx": (pp, rec, e) => cwrap(rec(PREC.idx, e.at(1)) + `[` + rec(PREC.MAX, e.at(2)) + `]`, pp < PREC.idx),
     "not": (pp, rec, e) => cwrap(rec(PREC.not, 1) + ` - ` + rec(PREC.not, e.at(1)), pp < PREC.not),
     "+": (pp, rec, e) => cwrap(e.slice(1).map(rec.with(PREC.add)).join(` + `), pp < PREC.add),
     "sum": (pp, rec, e) => assert(false, message: "sum is unsupported in code."),
@@ -136,9 +138,8 @@
     },
     "/": (pp, rec, e) => cwrap(rec(PREC.div, e.at(1)), pp < PREC.div) + ` / ` + rec(PREC.div, e.at(2)),
     "^": (pp, rec, e) => {
-      assert(type(e.at(1)) == int and type(e.at(2)) == int, message: "Can only exponentiate constants")
-      // technically wrong associativity, but it's a constant
-      rec(PREC.pow, e.at(1)) + `^` + rec(PREC.pow, e.at(2))
+      // `<=` in the wrap to deal with right associativity
+      cwrap(rec(PREC.pow, e.at(1)) + `^` + rec(PREC.pow, e.at(2)), pp <= PREC.pow)
     },
     "=": (pp, rec, e) => rec(PREC.eq, e.at(1)) + ` = ` + rec(PREC.eq, e.at(2)),
     ":=": (pp, rec, e) => rec(PREC.eq, e.at(1)) + ` := ` + rec(PREC.eq, e.at(2)),
@@ -155,6 +156,10 @@
       assert(e.len() == 3, message: "Invalid type cast: " + repr(e))
       cwrap(rec(PREC.cast, e.at(1)) + ` as ` + type_to_code(e.at(2)), pp < PREC.cast)
     },
+    "next": (pp, rec, e) =>  {
+      assert(e.len() == 2 and type(e.at(1)) == str, message: "Invalid transition variable: " + repr(e))
+      cwrap(rec(PREC.next, e.at(1)) + `'`, pp < PREC.next)
+    },
   ),
   num: (n) => raw(str(n)),
   flatten: flatten_code
@@ -217,8 +222,7 @@
     },
     "/": (pp, rec, e) => $#rec(PREC.div, e.at(1)) / #rec(PREC.div, e.at(2))$,
     "^": (pp, rec, e) => {
-      assert(type(e.at(1)) == int, message: "Can only exponentiate constants")
-      $#e.at(1)^#rec(PREC.MAX, e.at(2))$
+      mwrap($#rec(PREC.pow, e.at(1))^#rec(PREC.MAX, e.at(2))$, pp <= PREC.pow)
     },
     "=": (pp, rec, e) => $#rec(PREC.eq, e.at(1)) = #rec(PREC.eq, e.at(2))$,
     ":=": (pp, rec, e) => $#rec(PREC.eq, e.at(1)) := #rec(PREC.eq, e.at(2))$,
@@ -236,7 +240,11 @@
     },
     "cast": (pp, rec, e) => {
       assert(e.len() == 3, message: "Invalid type cast: " + repr(e))
-      cwrap($#rec(PREC.cast, e.at(1)) colon.double #type_to_math(e.at(2))$, pp < PREC.cast)
+      mwrap($#rec(PREC.cast, e.at(1)) colon.double #type_to_math(e.at(2))$, pp < PREC.cast)
+    },
+    "next": (pp, rec, e) =>  {
+      assert(e.len() == 2 and type(e.at(1)) == str, message: "Invalid transition variable: " + repr(e))
+      mwrap($#rec(PREC.next, e.at(1))'$, pp < PREC.next)
     },
   ),
   var: v => if v.len() == 1 { $#v$ } else { $#raw(v)$ },

spec/meta.typ

@@ -55,8 +55,8 @@
     )),
     ("RECURSION", (
       ("recursion", [Recursive verification], <recursion>),
-      ("field", [`Field` VM], <field-VM>),
-      ("field_decode", [`Field` `DECODE` table], <field-decode>),
+      ("field_vm", [Field VM], <field-VM>),
+      ("field_vm_decode", [Field `DECODE` table], <field-decode>),
     )),
     ("MATHEMATICS", (
       ("limbs_and_carries", [On limb decomposition and carries], <limbs>),
@@ -105,6 +105,7 @@
 #let common-formatting(body) = {
   set footnote(numbering: "[1]")
   show raw.where(block: true): it => block(it, inset: 1em, width: 100%, radius: 5pt)
+  show math.equation.where(block: false): box // Don't line-break inline equations by default
   show ref: equate.with(sub-numbering: true, breakable: true, number-mode: "label")
   show selector.or(..highlights.keys().map(k => figure.where(kind: k))): it => {
     set figure.caption(position: top)

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"]