diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index a55cc6b1..faa11f28 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -22,3 +22,4 @@ - [Fixed-base scalar multiplication](design/circuit/gadgets/ecc/fixed-base-scalar-mul.md) - [Variable-base scalar multiplication](design/circuit/gadgets/ecc/var-base-scalar-mul.md) - [Sinsemilla](design/circuit/gadgets/sinsemilla.md) + - [Lookup Range Check](design/circuit/gadgets/lookup_range_check.md) diff --git a/book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md b/book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md index e1ea1bd8..37d8c743 100644 --- a/book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md +++ b/book/src/design/circuit/gadgets/ecc/var-base-scalar-mul.md @@ -314,9 +314,11 @@ $$ 2 & q_\text{mul}^\text{overflow} \cdot \left(s - (\alpha + \mathbf{k}_{254} \cdot 2^{130})\right) = 0 \\\hline 2 & q_\text{mul}^\text{overflow} \cdot \left(\mathbf{z}_0 - \alpha - t_q\right) = 0 \\\hline 3 & q_\text{mul}^\text{overflow} \cdot \left(\mathbf{k}_{254} \cdot (\mathbf{z}_{130} - 2^{124})\right) = 0 \\\hline -3 & q_\text{mul}^\text{overflow} \cdot \left(\mathbf{k}_{254} \cdot (s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)\right) = 0 \\\hline -5 & q_\text{mul}^\text{overflow} \cdot \left((1 - \mathbf{k}_{254}) \cdot (1 - \mathbf{z}_{130} \cdot \eta) \cdot (s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)\right) = 0 \\\hline +3 & q_\text{mul}^\text{overflow} \cdot \left(\mathbf{k}_{254} \cdot (s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)/2^{130}\right) = 0 \\\hline +5 & q_\text{mul}^\text{overflow} \cdot \left((1 - \mathbf{k}_{254}) \cdot (1 - \mathbf{z}_{130} \cdot \eta) \cdot (s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)/2^{130}\right) = 0 \\\hline \end{array} $$ +where $(s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)/2^{130}$ can be computed by another running sum. Note that the factor of $1/2^{130}$ has no effect on the constraint, since the RHS is zero. -where $\sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i$ can be computed by another running sum. [TODO: be explicit about how to do that.] +#### Running sum range check +We make use of a $10$-bit [lookup range check](../lookup_range_check.md) in the circuit to subtract the low $130$ bits of $\mathbf{s}$. The range check subtracts the first $13 \cdot 10$ bits of $\mathbf{s},$ and right-shifts the result to give $(s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)/2^{130}.$ diff --git a/book/src/design/circuit/gadgets/lookup_range_check.md b/book/src/design/circuit/gadgets/lookup_range_check.md new file mode 100644 index 00000000..b81a9df9 --- /dev/null +++ b/book/src/design/circuit/gadgets/lookup_range_check.md @@ -0,0 +1,27 @@ +# Lookup decomposition +This gadget makes use of a $K$-bit lookup table to decompose a field element $\alpha$ into $K$-bit words. Firstly, express $$\alpha = k_0 + 2^{K} \cdot k_1 + 2^{2K} \cdot k_2 + \cdots,$$ where each $k_i$ a $K$-bit value. + +We initialize the running sum $z_0 = \mathbf{s},$ and compute subsequent terms $z_i = \frac{z_{i - 1} - k_{i-1}}{2^{K}}.$ This gives us: + +$$ +\begin{aligned} +z_0 &= \alpha \\ + &= k_0 + 2^{K} \cdot k_1 + 2^{2K} \cdot k_2 + 2^{3K} \cdot k_3 + \cdots, \\ +z_1 &= (z_0 - k_0) / 2^K \\ + &= k_1 + 2^{K} \cdot k_2 + 2^{2K} \cdot k_3 + \cdots, \\ +z_2 &= (z_1 - k_1) / 2^K \\ + &= k_2 + 2^{K} \cdot k_3 + \cdots, \\ + &\vdots +\end{aligned} +$$ + +Each $K$-bit word $k_i = z_i - 2^K \cdot z_{i+1}$ is range-constrained by a lookup in the $K$-bit table. This gadget takes in $\alpha, n$ and returns $(z_0, z_1, \cdots, z_n).$ + +## Strict mode +Strict mode constrains the running sum output $z_{n}$ to be zero, thus range-constraining the field element to be within $n \cdot K$ bits. + +## Short range check +Using two $K$-bit lookups, we can range-constrain a field element $\alpha$ to be $n$ bits, where $n \leq K.$ To do this: + +1. Constrain $0 \leq \alpha < 2^K$ to be within $K$ bits using a $K$-bit lookup. +2. Constrain $0 \leq \alpha \cdot 2^{K - n} < 2^K$ to be within $K$ bits using a $K$-bit lookup. \ No newline at end of file