spec: Materialize SUB in sub.toml for improved machine-readability

spec/add.typ

@@ -4,30 +4,46 @@
 
 #let config = load_config()
 #let chip = load_chip("src/add.toml", config)
+#let subchip = load_chip("src/sub.toml", config)
 
 #show: book-page(chip.name)
 
 #set_nr_interactions(chip, name: "SUB")
 #let nr_interactions = compute_nr_interactions(chip)
 
 #let add = raw(chip.name)
-#let sub = raw("SUB")
+#let sub = raw(subchip.name)
 
+= #add
 #add is a constraint template that is used to assert that $#`sum` equiv #`lhs` + #`rhs` (mod 2^64)$, under the condition that `cond` is non-zero.
+
+== Variables
+This template introduces #nr_interactions interaction(s).
+#render_chip_variable_table(chip, config)
+
+== Assumptions
+#render_chip_assumptions(chip, config)
+
+== Constraints
+This template introduces the following constraints
+#render_constraint_table(chip, config)
+
+= #sub
+
 For ease of notation, we moreover introduce the #sub constraint template
 $
-#`SUB<diff; lhs, rhs>` := #`ADD<lhs; rhs, diff>`,
+#`SUB<diff; lhs, rhs>` := #`ADD<lhs; diff, rhs>`,
 $
 in both conditional and unconditional versions.
 It constrains that $#`diff` equiv #`lhs` - #`rhs` (mod 2^64)$ when the expression `cond` is non-zero.
 
-= Variables
+== Variables
 This template introduces #nr_interactions interaction(s).
-#render_chip_variable_table(chip, config)
+#render_chip_variable_table(subchip, config)
 
-= Assumptions
-#render_chip_assumptions(chip, config)
+== Assumptions
+#render_chip_assumptions(subchip, config)
 
-= Constraints
+== Constraints
 This template introduces the following constraints
-#render_constraint_table(chip, config)
+#render_constraint_table(subchip, config)

spec/src/sub.toml

@@ -0,0 +1,46 @@
+name = "SUB"
+
+[[variables.condition]]
+name = "cond"
+type = "BaseField"
+desc = "Whether the relation should be enforced ($eq.not 0$) or not ($0$)."
+
+[[variables.input]]
+name = "lhs"
+type = "DWordWL"
+desc = "left-hand operator"
+
+[[variables.input]]
+name = "rhs"
+type = "DWordWL"
+desc = "right-hand operator"
+
+[[variables.output]]
+name = "diff"
+type = "DWordWL"
+desc = "$#`lhs` - #`rhs`$"
+
+[[assumptions]]
+desc = "`IS_WORD[lhs[i]]`"
+iter = ["i", 0, 1]
+ref = "sub:a:lhs"
+
+[[assumptions]]
+desc = "`IS_WORD[rhs[i]]`"
+iter = ["i", 0, 1]
+ref = "sub:a:rhs"
+
+[[assumptions]]
+desc = "`IS_WORD[diff[i]]`"
+iter = ["i", 0, 1]
+ref = "sub:a:diff"
+
+[[constraint_groups]]
+name = "all"
+
+[[constraints.all]]
+kind = "template"
+tag = "ADD"
+input = ["diff", "rhs"]
+output = "lhs"
+cond = "cond"