From c271c9309fd91b26f5d52e42dcd48d0ce93aeb54 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Sat, 3 Jan 2026 14:55:47 +0100
Subject: [PATCH 1/2] spec: introduce "condition" column type

---
 spec/src.typ         | 5 ++++-
 spec/src/config.toml | 2 +-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/spec/src.typ b/spec/src.typ
index 7c9e68487..8200b47c1 100644
--- a/spec/src.typ
+++ b/spec/src.typ
@@ -35,7 +35,10 @@
 #let _check_chip(chip, config) = {
   // Check that all variable categories are valid
   for category in chip.variables.keys() {
-    assert(category in config.variables.categories.all)
+    assert(
+      category in config.variables.categories.all, 
+      message: "invalid category: " + repr(category)
+    )
   }
 
   // Check that `def` is only contained in `virtual` variables
diff --git a/spec/src/config.toml b/spec/src/config.toml
index 29c0b9d83..28abdcbfc 100644
--- a/spec/src/config.toml
+++ b/spec/src/config.toml
@@ -82,5 +82,5 @@ desc = """\
        """
 
 [variables.categories]
-all = ["input", "output", "auxiliary", "virtual", "multiplicity"]
+all = ["input", "output", "auxiliary", "virtual", "multiplicity", "condition"]
 instantiated = ["input", "output", "auxiliary", "multiplicity"]

From a0801d9806e66e2b175a4d19d962d4c05cddf2d2 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Sat, 3 Jan 2026 16:24:33 +0100
Subject: [PATCH 2/2] spec: is_bit template

---
 spec/book.typ        |  1 +
 spec/is_bit.typ      | 47 ++++++++++++++++++++++++++++++++++++++++++++
 spec/src/is_bit.toml | 20 +++++++++++++++++++
 3 files changed, 68 insertions(+)
 create mode 100644 spec/is_bit.typ
 create mode 100644 spec/src/is_bit.toml

diff --git a/spec/book.typ b/spec/book.typ
index 8b5cae160..dcf1d0c1b 100644
--- a/spec/book.typ
+++ b/spec/book.typ
@@ -7,6 +7,7 @@
   title: "Lambda VM specification",
   summary: [
     #chapter("variables.typ")[Variables]
+    #chapter("is_bit.typ")[IS_BIT template]
   ]
 )
 
diff --git a/spec/is_bit.typ b/spec/is_bit.typ
new file mode 100644
index 000000000..c379080cd
--- /dev/null
+++ b/spec/is_bit.typ
@@ -0,0 +1,47 @@
+#import "/book.typ": book-page
+#import "/src.typ": load_config, load_chip
+#import "/chip.typ": render_chip_column_table, render_constraint_table
+
+#show: book-page.with(title: "IS_BIT template")
+
+#let config = load_config()
+#let chip = load_chip("src/is_bit.toml", config)
+
+#let is_bit = raw(chip.name)
+
+#let highlighted_code(code) = {
+  box(
+    inset: (left: 4pt, right: 4pt), 
+    outset: (top: 4pt, bottom: 4pt), 
+    radius: 2pt,
+    fill: luma(230), 
+    raw(code))
+}
+
+= #is_bit template
+#is_bit is a constraint template that is used to assert that a variable lies in the range ${0, 1}$ if some second variable is non-zero.
+Barring exceptional cases, this template is used to assert that a variable of type `Bit` assumes a valid value under some condition.
+
+== Interface
+The #is_bit constraint template has the following interface:
+#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => IS_BIT<X>"))
+where `cond` is any value described by an expression _of degree at most $1$_.
+Note that #highlighted_code("IS_BIT<X>") can be used to denote the _unconditional_ application of the #is_bit template to `X`.
+
+== Variables
+The #is_bit template operates on two variables: `cond` and `X`:
+#render_chip_column_table(chip, config)
+
+== Constraints
+It takes only one constraint to enforce that `X` must be either $0$ or $1$ whenever $#`cond` eq.not 0$:
+#render_constraint_table(chip, config)
+*Note*: 
+- In case of _unconditional_ template application, `cond` can be dropped from the constraint, simplifying it to $#`X` (1- #`X`) = 0$.
+- As described earlier, the `cond` variable must be describable by a degree-1 (i.e., linear) expression.
+  This is to make sure that @isbit:c:isbit's expression has degree at most 3.
+
+== Proof of correctness
+If `cond` is $0$, @isbit:c:isbit is trivially satisfied: `X` can assume any value and the polynomial constraint will evaluate to $0$ regardless. 
+When $#`cond` eq.not 0$, it follows that the statement can only be proven when $#`X` (1-#`X`) equiv 0 mod p$, with $p$ the modulus of the field.
+Because `BaseField` is a prime field, this equality is only satisfied if either $#`X` equiv 0 mod p$ or $1-#`X` equiv 0 mod p$.
+Hence, it is proven that when $#`cond` eq.not 0$, @isbit:c:isbit is only satisfied if $#`X` in {0, 1}$. #align(right, $qed$)
diff --git a/spec/src/is_bit.toml b/spec/src/is_bit.toml
new file mode 100644
index 000000000..47e96a27e
--- /dev/null
+++ b/spec/src/is_bit.toml
@@ -0,0 +1,20 @@
+name = "IS_BIT"
+
+[[variables.condition]]
+name = "cond"
+type = "BaseField"
+desc = "Whether the constraint should be applied ($eq.not 0$) or not ($0$)."
+
+[[variables.input]]
+name = "X"
+type = "BaseField"
+desc = "Value for which to assert that it lies in the range ${0, 1}$."
+
+[[constraint_groups]]
+name = "all"
+
+[[constraints.all]]
+kind = "arith"
+constraint = "$#`cond` => #`X` (1-#`X`) = 0$"
+poly = ["*", "cond", "X", ["not", "X"]]
+ref = "isbit:c:isbit"