From edc561800385b0f1326d0e65ea43e0d3c66f61d5 Mon Sep 17 00:00:00 2001
From: Robin Jadoul <robin.jadoul@3milabs.tech>
Date: Mon, 22 Jun 2026 17:29:32 +0200
Subject: [PATCH] spec: Materialize SUB in sub.toml for improved
 machine-readability

---
 spec/add.typ      | 32 ++++++++++++++++++++++++--------
 spec/src/sub.toml | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 70 insertions(+), 8 deletions(-)
 create mode 100644 spec/src/sub.toml

diff --git a/spec/add.typ b/spec/add.typ
index 0772aa30b..21332e8f6 100644
--- a/spec/add.typ
+++ b/spec/add.typ
@@ -4,6 +4,7 @@
 
 #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)
 
@@ -11,23 +12,38 @@
 #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)
diff --git a/spec/src/sub.toml b/spec/src/sub.toml
new file mode 100644
index 000000000..55b8f53ba
--- /dev/null
+++ b/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"