diff --git a/book/book.toml b/book/book.toml
index e86492cb..c1e225a2 100644
--- a/book/book.toml
+++ b/book/book.toml
@@ -6,3 +6,4 @@ src = "src"
title = "The Orchard Book"
[preprocessor.katex]
+macros = "macros.txt"
diff --git a/book/macros.txt b/book/macros.txt
new file mode 100644
index 00000000..f4beaea8
--- /dev/null
+++ b/book/macros.txt
@@ -0,0 +1,28 @@
+# Conventions
+
+\bconcat:{\mathop{\kern 0.1em||\kern 0.1em}}
+
+# Conversions
+
+\ItoLEBSP:{\mathsf{I2LEBSP}_{#1}}
+
+# Fields and curves
+
+\BaseLength:{\ell^\mathsf{#1\vphantom{p}}_{\mathsf{base}}}
+
+# Key components
+
+\AuthSignPublic:{\mathsf{ak}}
+\NullifierKey:{\mathsf{nk}}
+\InViewingKey:{\mathsf{ivk}}
+
+# Commitments and hashes
+
+\SinsemillaHash:{\mathsf{SinsemillaHash}}
+\SinsemillaShortCommit:{\mathsf{SinsemillaShortCommit}}
+\CommitIvk:{\mathsf{Commit}^{\InViewingKey}}
+
+# Circuit constraint helper methods
+
+\BoolCheck:{\texttt{bool\_check}({#1})}
+\ShortLookupRangeCheck:{\texttt{short\_lookup\_range\_check}({#1})}
diff --git a/book/src/design/circuit/gadgets/sinsemilla/commit-ivk.md b/book/src/design/circuit/gadgets/sinsemilla/commit-ivk.md
index 3cd56e9d..54c8e34d 100644
--- a/book/src/design/circuit/gadgets/sinsemilla/commit-ivk.md
+++ b/book/src/design/circuit/gadgets/sinsemilla/commit-ivk.md
@@ -1,76 +1,229 @@
# CommitIvk
## Message decomposition
-$\mathsf{SinsemillaShortCommit}$ is used in the [$\mathsf{CommitIvk}$ function](https://zips.z.cash/protocol/protocol.pdf#concretesinsemillacommit). The input to $\mathsf{SinsemillaShortCommit}$ is:
-$$\mathsf{I2LEBSP}_{\ell_{\textsf{base}}^{\textsf{Orchard}}}(ak) || \mathsf{I2LEBSP}_{\ell_{\textsf{base}}^{\textsf{Orchard}}}(nk),$$
+$\SinsemillaShortCommit$ is used in the
+[$\CommitIvk$ function](https://zips.z.cash/protocol/protocol.pdf#concretesinsemillacommit).
+The input to $\SinsemillaShortCommit$ is:
-where $\mathsf{ak, nk}$ are Pallas base field elements, and $\ell_{\textsf{base}}^{\textsf{Orchard}} = 255.$
+$$\ItoLEBSP{\BaseLength{Orchard}}(\AuthSignPublic) \bconcat \ItoLEBSP{\BaseLength{Orchard}}(\NullifierKey),$$
-We break these inputs into the following `MessagePiece`s:
+where $\AuthSignPublic$, $\NullifierKey$ are Pallas base field elements, and $\BaseLength{Orchard} = 255.$
+
+Sinsemilla operates on multiples of 10 bits, so we start by decomposing the message into
+chunks:
$$
-\begin{aligned}
-a \text{ (250 bits)} &= \text{bits } 0..=249 \text{ of } \mathsf{ak} \\
-b \text{ (10 bits)} &= b_0||b_1||b_2 \\
- &= (\text{bits } 250..=253 \text{ of } \mathsf{ak}) || (\text{bit } 254 \text{ of } \mathsf{ak}) || (\text{bits } 0..=4 \text{ of } \mathsf{nk}) \\
-c \text{ (240 bits)} &= \text{bits } 5..=244 \text{ of } \mathsf{nk} \\
-d \text{ (10 bits)} &= d_0||d_1 \\
- &= (\text{bits } 245..=253 \text{ of } \mathsf{nk}) || (\text{bit } 254 \text{ of } \mathsf{nk})
-\end{aligned}
+\begin{align}
+\ItoLEBSP{\BaseLength{Orchard}}(\AuthSignPublic) &= a \bconcat b_0 \bconcat b_1 \\
+ &= (\text{bits 0..=249 of } \AuthSignPublic) \bconcat
+ (\text{bits 250..=253 of } \AuthSignPublic) \bconcat
+ (\text{bit 254 of } \AuthSignPublic) \\
+\ItoLEBSP{\BaseLength{Orchard}}(\NullifierKey) &= b_2 \bconcat c \bconcat d_0 \bconcat d_1 \\
+ &= (\text{bits 0..=4 of } \NullifierKey) \bconcat
+ (\text{bits 5..=244 of } \NullifierKey) \bconcat
+ (\text{bits 245..=253 of } \NullifierKey) \bconcat
+ (\text{bit 254 of } \NullifierKey) \\
+\end{align}
$$
-$a,b,c,d$ are constrained by the $\textsf{SinsemillaHash}$ to be $250$ bits, $10$ bits, $240$ bits, and $10$ bits respectively.
+Then we recompose the chunks into message pieces:
-In a custom gate, we check this message decomposition by enforcing the following constraints:
+$$
+\begin{array}{|c|l|}
+\hline
+\text{Length (bits)} & \text{Piece} \\\hline
+250 & a \\
+10 & b = b_0 \bconcat b_1 \bconcat b_2 \\
+240 & c \\
+10 & d = d_0 \bconcat d_1 \\\hline
+\end{array}
+$$
-1. $b = b_0 + 2^4 \cdot b_1 + 2^5 \cdot b_2$
-
-$b_0, b_2$ are witnessed outside this gate, and constrained to be $4$ bits and $5$ bits respectively. $b_1$ is witnessed and boolean-constrained in this gate:
-$$(b_1)(1 - b_1) = 0.$$
-From these witnessed subpieces, we check that we recover the original `MessagePiece` input to the hash:
-$$b = b_0 + 2^4 \cdot b_1 + 2^5 \cdot b_2.$$
+Each message piece is constrained by $\SinsemillaHash$ to its stated length. Additionally,
+$\AuthSignPublic$ and $\NullifierKey$ are witnessed as field elements, so we know they are
+canonical. However, we need additional constraints to enforce that:
-2. $d = d_0 + 2^9 \cdot d_1$
-
-$d_0$ is witnessed outside this gate, and constrained to be $9$ bits. $d_1$ is witnessed and boolean-constrained in this gate:
-$$(d_1)(1 - d_1) = 0.$$
-From these witnessed subpieces, we check that we recover the original `MessagePiece` input to the hash:
-$$d = d_0 + 2^9 \cdot d_1.$$
+- The chunks are the correct bit lengths (or else they could overlap in the decompositions
+ and allow the prover to witness an arbitrary $\SinsemillaShortCommit$ message).
+- The chunks contain the canonical decompositions of $\AuthSignPublic$ and $\NullifierKey$
+ (or else the prover could witness an input to $\SinsemillaShortCommit$ that is
+ equivalent to $\AuthSignPublic$ and $\NullifierKey$ but not identical).
+
+Some of these constraints can be implemented with reusable circuit gadgets. We define a
+custom gate controlled by the selector $q_\CommitIvk$ to hold the remaining constraints.
+
+## Bit length constraints
+
+Chunks $a$ and $c$ are directly constrained by Sinsemilla. For the remaining chunks, we
+use the following constraints:
+
+$$
+\begin{array}{|c|l|}
+\hline
+\text{Degree} & \text{Constraint} \\\hline
+ & \ShortLookupRangeCheck{b_0, 4} \\\hline
+ & \ShortLookupRangeCheck{b_2, 5} \\\hline
+ & \ShortLookupRangeCheck{d_0, 9} \\\hline
+3 & q_\CommitIvk \cdot \BoolCheck{b_1} = 0 \\\hline
+3 & q_\CommitIvk \cdot \BoolCheck{d_1} = 0 \\\hline
+\end{array}
+$$
+
+where $\BoolCheck{x} = x \cdot (1 - x)$ and $\ShortLookupRangeCheck{}$ is a
+[short lookup range check](../lookup_range_check.md#short-range-check).
+
+## Decomposition constraints
We have now derived or witnessed every subpiece, and range-constrained every subpiece:
+- $a$ ($250$ bits) is witnessed and constrained outside the gate;
- $b_0$ ($4$ bits) is witnessed and constrained outside the gate;
- $b_1$ ($1$ bits) is witnessed and boolean-constrained in the gate;
- $b_2$ ($5$ bits) is witnessed and constrained outside the gate;
+- $c$ ($240$ bits) is witnessed and constrained outside the gate;
- $d_0$ ($9$ bits) is witnessed and constrained outside the gate;
-- $d_1$ ($1$ bits) is witnessed and boolean-constrained in the gate,
-and we use them to reconstruct the original field element inputs:
+- $d_1$ ($1$ bits) is witnessed and boolean-constrained in the gate.
-3. $\textsf{ak} = a + 2^{250} \cdot b_0 + 2^{254} \cdot b_1$
-4. $\textsf{nk} = b_2 + 2^5 \cdot c + 2^{245} \cdot d_0 + 2^{254} \cdot d_1$
+We can now use them to reconstruct both the (chunked) message pieces, and the original
+field element inputs:
-## Canonicity
-The modulus of the Pallas base field is $p = 2^{254} + t_p,$ where $t_p = 45560315531419706090280762371685220353 < 2^{126}.$
+$$
+\begin{align}
+b &= b_0 + 2^4 \cdot b_1 + 2^5 \cdot b_2 \\
+d &= d_0 + 2^9 \cdot d_1 \\
+\AuthSignPublic &= a + 2^{250} \cdot b_0 + 2^{254} \cdot b_1 \\
+\NullifierKey &= b_2 + 2^5 \cdot c + 2^{245} \cdot d_0 + 2^{254} \cdot d_1 \\
+\end{align}
+$$
-### $\textsf{ak} = a (250 \text{ bits}) || b_0 (4 \text{ bits}) || b_1 (1 \text{ bit})$
-We check that $\mathsf{I2LEBSP_{\ell_{base}^{Orchard}}(ak)}$ is a canonically-encoded $255$-bit value, i.e. $\textsf{ak} < p$. If the high bit is not set $b_1 = 0$, we are guaranteed that $\textsf{ak} < 2^{254}$. Thus, we are only interested in cases when $b_1 = 1 \implies \textsf{ak} \geq 2^{254}$. In these cases, we check that $\textsf{ak}_{0..=253} < t_p < 2^{126}$:
+$$
+\begin{array}{|c|l|}
+\hline
+\text{Degree} & \text{Constraint} \\\hline
+2 & q_\CommitIvk \cdot (b - (b_0 + b_1 \cdot 2^4 + b_2 \cdot 2^5)) = 0 \\\hline
+2 & q_\CommitIvk \cdot (d - (d_0 + d_1 \cdot 2^9)) = 0 \\\hline
+2 & q_\CommitIvk \cdot (a + b_0 \cdot 2^{250} + b_1 \cdot 2^{254} - \AuthSignPublic) = 0 \\\hline
+2 & q_\CommitIvk \cdot (b_2 + c \cdot 2^5 + d_0 \cdot 2^{245} + d_1 \cdot 2^{254} - \NullifierKey) = 0 \\\hline
+\end{array}
+$$
+
+## Canonicity checks
+
+At this point, we have constrained $\ItoLEBSP{\BaseLength{Orchard}}(\AuthSignPublic)$ and
+$\ItoLEBSP{\BaseLength{Orchard}}(\NullifierKey)$ to be 255-bit values, with top bits $b_1$
+and $d_1$ respectively. We have also constrained:
+
+$$
+\begin{align}
+\ItoLEBSP{\BaseLength{Orchard}}(\AuthSignPublic) &= \AuthSignPublic \pmod{q_\mathbb{P}} \\
+\ItoLEBSP{\BaseLength{Orchard}}(\NullifierKey) &= \NullifierKey \pmod{q_\mathbb{P}} \\
+\end{align}
+$$
+
+where $q_\mathbb{P}$ is the Pallas base field modulus. The remaining constraints will
+enforce that these are indeed canonically-encoded field elements, i.e.
+
+$$
+\begin{align}
+\ItoLEBSP{\BaseLength{Orchard}}(\AuthSignPublic) &< q_\mathbb{P} \\
+\ItoLEBSP{\BaseLength{Orchard}}(\NullifierKey) &< q_\mathbb{P} \\
+\end{align}
+$$
+
+The Pallas base field modulus has the form $q_\mathbb{P} = 2^{254} + t_\mathbb{P}$, where
+$$t_\mathbb{P} = \mathtt{0x224698fc094cf91b992d30ed00000001}$$
+is 126 bits. We therefore know that if the top bit is not set, then the remaining bits
+will always comprise a canonical encoding of a field element. Thus the canonicity checks
+below are enforced if and only if $b_1 = 1$ (for $\AuthSignPublic$) or $d_1 = 1$ (for
+$\NullifierKey$).
+
+> In the constraints below we use a base-$2^{10}$ variant of the method used in libsnark
+> (originally from [[SVPBABW2012](https://eprint.iacr.org/2012/598.pdf), Appendix C.1]) for
+> range constraints $0 \leq x < t$:
+>
+> - Let $t'$ be the smallest power of $2^{10}$ greater than $t$.
+> - Enforce $0 \leq x < t'$.
+> - Let $x' = x + t' - t$.
+> - Enforce $0 \leq x' < t'$.
+
+### $\AuthSignPublic$ with $b_1 = 1 \implies \AuthSignPublic \geq 2^{254}$
+
+In these cases, we check that $\textsf{ak}_{0..=253} < t_\mathbb{P} < 2^{126}$:
1. $b_1 = 1 \implies b_0 = 0.$
-Since $b_1 = 1 \implies \textsf{ak}_{0..=253} < 2^{126},$ we know that $\textsf{ak}_{126..=253} = 0,$ and in particular $b_0 = \textsf{ak}_{250..=253} = 0.$ So, we constrain $$b_1 \cdot b_0 = 0.$$
+
+ Since $b_1 = 1 \implies \AuthSignPublic_{0..=253} < 2^{126},$ we know that
+ $\AuthSignPublic_{126..=253} = 0,$ and in particular
+ $$b_0 := \AuthSignPublic_{250..=253} = 0.$$
2. $b_1 = 1 \implies 0 \leq a < 2^{126}.$
-To check that $a < 2^{126}$, we use two constraints:
- a) $0 \leq a < 2^{130}$. This is expressed in the custom gate as $$b_1 \cdot z_{13,a} = 0,$$ where $z_{13,a}$ is the index-13 running sum output by $\textsf{SinsemillaHash}(a).$
+ To check that $a < 2^{126}$, we use two constraints:
- b) $0 \leq a + 2^{130} - t_p < 2^{130}$. To check this, we decompose $a' = a + 2^{130} - t_p$ into thirteen 10-bit words (little-endian) using a running sum $z_{a'}$, looking up each word in a $10$-bit lookup table. We then enforce in the custom gate that $$b_1 \cdot z_{13, a'} = 0.$$
+ a) $0 \leq a < 2^{130}$. This is expressed in the custom gate as
+ $$b_1 \cdot z_{a,13} = 0,$$
+ where $z_{a,13}$ is the index-13 running sum output by $\SinsemillaHash(a).$
-### $\textsf{nk} = b_2 (5 \text{ bits}) || c (240 \text{ bits}) || d_0 (9 \text{ bits}) || d_1 (1 \text{ bit})$
-We check that $\mathsf{I2LEBSP}_{\ell_{\textsf{base}}^{\textsf{Orchard}}}(nk)$ is a canonically-encoded $255$-bit value, i.e. $\textsf{nk} < p$. If the high bit is not set $d_1 = 0$, we are guaranteed that $nk < 2^{254}$. Thus, we are only interested in cases when $d_1 = 1 \implies nk \geq 2^{254}$. In these cases, we check that $\textsf{nk}_{0..=253} < t_p < 2^{126}$:
+ b) $0 \leq a + 2^{130} - t_\mathbb{P} < 2^{130}$. To check this, we decompose
+ $a' = a + 2^{130} - t_\mathbb{P}$ into thirteen 10-bit words (little-endian) using
+ a running sum $z_{a'}$, looking up each word in a $10$-bit lookup table. We then
+ enforce in the custom gate that
+ $$b_1 \cdot z_{a',13} = 0.$$
-1. $d_1 = 1 \implies 0 \leq b_2 + 2^5 \cdot c < 2^{126}.$
-To check that $0 \leq b_2 + 2^5 \cdot c < 2^{126}$, we use two constraints:
+$$
+\begin{array}{|c|l|}
+\hline
+\text{Degree} & \text{Constraint} \\\hline
+3 & q_\CommitIvk \cdot b_1 \cdot b_0 = 0 \\\hline
+3 & q_\CommitIvk \cdot b_1 \cdot z_{a,13} = 0 \\\hline
+2 & q_\CommitIvk \cdot (a + 2^{130} - t_\mathbb{P} - a') = 0 \\\hline
+3 & q_\CommitIvk \cdot b_1 \cdot z_{a',13} = 0 \\\hline
+\end{array}
+$$
- a) $0 \leq b_2 + 2^5 \cdot c < 2^{140}$. $b_2$ is already constrained individually to be a $5$-bit value. $z_{13, c}$ is the index-13 running sum output by $\textsf{SinsemillaHash}(c).$ By constraining $$d_1 \cdot z_{13,c} = 0,$$ we constrain $b_2 + 2^5 \cdot c < 2^{135} < 2^{140}.$
+### $\NullifierKey$ with $d_1 = 1 \implies \NullifierKey \geq 2^{254}$
- b) $0 \leq b_2 + 2^5 \cdot c + 2^{140} - t_p < 2^{140}$. To check this, we decompose $b' = b_2 + 2^5 \cdot c + 2^{140} - t_p$ into fourteen 10-bit words (little-endian) using a running sum $z_{b'}$, looking up each word in a $10$-bit lookup table. We then enforce in the custom gate that $$d_1 \cdot z_{14, b'} = 0.$$
\ No newline at end of file
+In these cases, we check that $\textsf{nk}_{0..=253} < t_\mathbb{P} < 2^{126}$:
+
+1. $d_1 = 1 \implies d_0 = 0.$
+
+ Since $d_1 = 1 \implies \NullifierKey_{0..=253} < 2^{126},$ we know that $\NullifierKey_{126..=253} = 0,$ and in particular $$d_0 := \NullifierKey_{245..=253} = 0.$$
+
+2. $d_1 = 1 \implies 0 \leq b_2 + 2^5 \cdot c < 2^{126}.$
+
+ To check that $0 \leq b_2 + 2^5 \cdot c < 2^{126}$, we use two constraints:
+
+ a) $0 \leq b_2 + 2^5 \cdot c < 2^{140}$. $b_2$ is already constrained individually to
+ be a $5$-bit value. $z_{c,13}$ is the index-13 running sum output by
+ $\SinsemillaHash(c).$ By constraining $$d_1 \cdot z_{c,13} = 0,$$ we constrain
+ $b_2 + 2^5 \cdot c < 2^{135} < 2^{140}.$
+
+ b) $0 \leq b_2 + 2^5 \cdot c + 2^{140} - t_\mathbb{P} < 2^{140}$. To check this, we
+ decompose ${b_2}c' = b_2 + 2^5 \cdot c + 2^{140} - t_\mathbb{P}$ into fourteen
+ 10-bit words (little-endian) using a running sum $z_{{b_2}c'}$, looking up each
+ word in a $10$-bit lookup table. We then enforce in the custom gate that
+ $$d_1 \cdot z_{{b_2}c',14} = 0.$$
+
+$$
+\begin{array}{|c|l|}
+\hline
+\text{Degree} & \text{Constraint} \\\hline
+3 & q_\CommitIvk \cdot d_1 \cdot d_0 = 0 \\\hline
+3 & q_\CommitIvk \cdot d_1 \cdot z_{c,13} = 0 \\\hline
+2 & q_\CommitIvk \cdot (b_2 + c \cdot 2^5 + 2^{140} - t_\mathbb{P} - {b_2}c') = 0 \\\hline
+3 & q_\CommitIvk \cdot d_1 \cdot z_{{b_2}c',14} = 0 \\\hline
+\end{array}
+$$
+
+## Region layout
+
+The constraints controlled by the $q_\CommitIvk$ selector are arranged across all 10
+advice columns, requiring two rows.
+
+$$
+\begin{array}{|c|c|c|c|c|c|c|c|c|c|c}
+ & & & & & & & & & & q_\CommitIvk \\\hline
+a & b & c & d & \AuthSignPublic & \NullifierKey & b_0 & b_1 & b_2 & d_0 & 0 \\\hline
+d_1 & z_{a,13} & a' & z_{a',13} & z_{c,13} & {b_2}c' & z_{{b_2}c',14} & & & & 1 \\\hline
+\end{array}
+$$