From c11d527142d17be67c2e201fc47476dfccf27745 Mon Sep 17 00:00:00 2001 From: Daira Hopwood Date: Fri, 8 Jul 2022 14:58:40 +0100 Subject: [PATCH 1/4] [book] WIP: full-width variable-base scalar mul allowing the scalar to be outside the base field. Signed-off-by: Daira Hopwood --- book/src/design/gadgets/ecc/var-base-scalar-mul.md | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/book/src/design/gadgets/ecc/var-base-scalar-mul.md b/book/src/design/gadgets/ecc/var-base-scalar-mul.md index 1098b185ac..2260c2933a 100644 --- a/book/src/design/gadgets/ecc/var-base-scalar-mul.md +++ b/book/src/design/gadgets/ecc/var-base-scalar-mul.md @@ -306,16 +306,25 @@ $\mathbf{z}_i$ cannot overflow for any $i \geq 1$, because it is a weighted sum However, $\mathbf{z}_0 = \alpha + t_q$ *can* overflow $[0, p)$. +> Note: for full-width scalar mul, it may not be possible to represent $\mathbf{z}_0$ in the base field (e.g. when the base field is Pasta's $\mathbb{F}_p$ and $p < q$). +> In that case, we need to special-case the row that would mention $\mathbf{z}_0$ so that it is correct for whatever representation we use for a full-width scalar. +> Our representation for $k$ will be the pair $(\mathbb{k}_{254}, k' = k - 2^{254} \cdot \mathbb{k}_{254})$. +> We'll use $k'$ in place of $\alpha + t_q$ for $\mathbf{z}_0$, constraining $k'$ to 254 bits so that it fits in an $\mathbb{F}_p$ element. +> Then we just have to generalize the argument below to work for $k' \in [0, 2 \cdot t_q)$ (because the maximum value of $\alpha + t_q$ is $q - 1 + t_q = 2^{254} + t_q - 1 + t_q$). + Since overflow can only occur in the final step that constrains $\mathbf{z}_0 = 2 \cdot \mathbf{z}_1 + \mathbf{k}_0$, we have $\mathbf{z}_0 = k \pmod{p}$. It is then sufficient to also check that $\mathbf{z}_0 = \alpha + t_q \pmod{p}$ (so that $k = \alpha + t_q \pmod{p}$) and that $k \in [t_q, p + t_q)$. These conditions together imply that $k = \alpha + t_q$ as an integer, and so $2^{254} + k = \alpha \pmod{q}$ as required. > Note: the bits $\mathbf{k}_{254..0}$ do not represent a value reduced modulo $q$, but rather a representation of the unreduced $\alpha + t_q$. ### Optimized check for $k \in [t_q, p + t_q)$ -Since $t_p + t_q < 2^{130}$, we have $$[t_q, p + t_q) = [t_q, t_q + 2^{130}) \;\cup\; [2^{130}, 2^{254}) \;\cup\; \big([2^{254}, 2^{254} + 2^{130}) \;\cap\; [p + t_q - 2^{130}, p + t_q)\big).$$ +Since $t_p + t_q < 2^{130}$ (also true if $p$ and $q$ are swapped), we have $$[t_q, p + t_q) = [t_q, t_q + 2^{130}) \;\cup\; [2^{130}, 2^{254}) \;\cup\; \big([2^{254}, 2^{254} + 2^{130}) \;\cap\; [p + t_q - 2^{130}, p + t_q)\big).$$ We may assume that $k = \alpha + t_q \pmod{p}$. +(This is true for the use of variable-base scalar mul in Orchard, where we know that $\alpha < p$. If is also true if we swap $p$ and $q$ so that we have $p > q$. +It is *not* true for a full-width scalar $\alpha \geq p$ when $p < q$.) + Therefore, $\begin{array}{rcl} k \in [t_q, p + t_q) &\Leftrightarrow& \big(k \in [t_q, t_q + 2^{130}) \;\vee\; k \in [2^{130}, 2^{254})\big) \;\vee\; \\ From 6396a0ec19755898dec63ad576bd218f160094cb Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Fri, 19 Aug 2022 17:16:46 -0700 Subject: [PATCH 2/4] [book] var-base-scalar-mul: Include general overflow check. Co-authored-by: Daira Hopwood --- .../design/gadgets/ecc/var-base-scalar-mul.md | 75 +++++++++++++++++++ 1 file changed, 75 insertions(+) diff --git a/book/src/design/gadgets/ecc/var-base-scalar-mul.md b/book/src/design/gadgets/ecc/var-base-scalar-mul.md index 2260c2933a..e9a14663a7 100644 --- a/book/src/design/gadgets/ecc/var-base-scalar-mul.md +++ b/book/src/design/gadgets/ecc/var-base-scalar-mul.md @@ -401,3 +401,78 @@ where $(s - \sum\limits_{i=0}^{129} 2^i \cdot \mathbf{s}_i)/2^{130}$ can be comp #### Running sum range check We make use of a $10$-bit [lookup range check](../decomposition.md#lookup-decomposition) 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}.$ + +## Overflow check (general) +Recall that we defined $\mathbf{z}_j = \sum_{i=j}^n (\mathbf{k}_i \cdot 2^{i−j})$, where $n = 254$. + +$\mathbf{z}_j$ cannot overflow for any $j \geq 1$, because it is a weighted sum of bits only up to $2^{n-j}$, which can be at most $2^{254} - 1$ when $j = 1$; this is smaller than $p$ (and also $q$). + +However, for full-width scalar mul, it may not be possible to represent $\mathbf{z}_0$ in the base field (e.g. when the base field is Pasta's $\mathbb{F}_p$ and $p < q$). In that case $\mathbf{z}_0 = \alpha + t_q$ *can* overflow $[0, p)$. + +So, we need to special-case the row that would mention $\mathbf{z}_0$ so that it is correct for whatever representation we use for a full-width scalar. + +Our representation for $k$ will be the pair $(\mathbf{k}_{254}, k' = k - 2^{254} \cdot \mathbf{k}_{254})$. We'll use $k'$ in place of $\alpha + t_q$ for $\mathbf{z}_0$, constraining $k'$ to 254 bits so that it fits in an $\mathbb{F}_p$ element. + +Then we just have to generalize the [overflow check used for variable-base scalar mul in the Orchard circuit](https://zcash.github.io/halo2/design/gadgets/ecc/var-base-scalar-mul.html#overflow-check) to work for $k' \in [0, 2 \cdot t_q)$ (because the maximum value of $\alpha + t_q$ is $q - 1 + t_q = 2^{254} + t_q - 1 + t_q$). + + +> Note: the bits $\mathbf{k}_{254..0}$ do not represent a value reduced modulo $q$, but rather a representation of the unreduced $\alpha + t_q$. + +Overflow can only occur in the final step that constrains $\mathbf{z}_0 = 2 \cdot \mathbf{z}_1 + \mathbf{k}_0$, and only if $\mathbf{z}_1$ has the bit with weight $2^{253}$ set (i.e. if $\mathbf{k}_{254} = 1$). If we instead set $\mathbf{z}_0 = 2 \cdot \mathbf{z}_1 - 2^{254} \cdot \mathbf{k}_{254} + \mathbf{k}_0$, now $\mathbf{z}_0$ cannot overflow and should be equal to $k'$. + +It is then sufficient to also check that $\mathbf{z}_0 + 2^{254} \cdot \mathbf{k}_{254} = \alpha + t_q$ as an integer where $\alpha \in [0, q)$. + +Represent $\alpha$ as $2^{254} \cdot \boldsymbol\alpha_{254} + 2^{253} \cdot \boldsymbol\alpha_{253} + \alpha''$ where we constrain $\alpha'' \in [0, 2^{253})$ and $\boldsymbol\alpha_{253}$ and $\boldsymbol\alpha_{254}$ to boolean. For this to be a canonical representation we also need $\boldsymbol \alpha_{254} = 1 \implies (\boldsymbol \alpha_{253} = 0 \;\wedge\; \alpha'' \in [0, t_q))$. + +Let $\alpha' = 2^{253} \cdot \boldsymbol\alpha_{253} + \alpha''$. + +If $\boldsymbol\alpha_{254} = 1$: +* constrain $\mathbf{k}_{254} = 1$ and $\mathbf{z}_0 = \alpha' + t_q$. This cannot overflow because in this case $\alpha' \in [0, t_q)$ and so $\mathbf{z}_0 \in [0, 2 \cdot t_q)$. + +If $\boldsymbol\alpha_{254} = 0$: +* we should have $\mathbf{k}_{254} = 1$ iff $\alpha' \in [2^{254} - t_q, 2^{254})$, i.e. witness $\mathbf{k}_{254}$ as boolean and then + * If $\mathbf{k}_{254} = 0$ then constrain $\alpha' \not\in [2^{254} - t_q, 2^{254})$. + * This can be done by constraining either $\boldsymbol\alpha_{253} = 0$ or $\alpha'' + t_q \in [0, 2^{253})$. ($\alpha'' + t_q$ cannot overflow.) + * If $\mathbf{k}_{254} = 1$ then constrain $\alpha' \in [2^{254} - t_q, 2^{254})$. + * This can be done by constraining $\alpha' - (2^{254} - t_q) \in [0, 2^{130})$ and $\alpha' - 2^{254} + 2^{130} \in [0, 2^{130})$. + +### Overflow check constraints (general) + +Represent $\alpha$ as $2^{254} \cdot \boldsymbol\alpha_{254} + 2^{253} \cdot \boldsymbol\alpha_{253} + \alpha''$ as above. + +The constraints for the overflow check are: + +$$ +\begin{aligned} +&\alpha'' \in [0, 2^{253}) \\ +&\boldsymbol\alpha_{253} \in \{0,1\} \\ +&\boldsymbol\alpha_{254} \in \{0,1\} \\ +&\mathbf{k}_{254} \in \{0,1\} \\ +\boldsymbol \alpha_{254} = 1 \implies &\boldsymbol \alpha_{253} = 0 \\ +\boldsymbol \alpha_{254} = 1 \implies &\alpha'' \in [0, 2^{130}) \;❁ \\ +\boldsymbol \alpha_{254} = 1 \implies &\alpha'' + 2^{130} - t_q \in [0, 2^{130}) \;❁ \\ +\boldsymbol\alpha_{254} = 1 \implies &\mathbf{k}_{254} = 1 \\ +\boldsymbol\alpha_{254} = 1 \implies &\mathbf{z}_0 = \alpha' + t_q \\ +\boldsymbol\alpha_{254} = 0 \;\wedge\; \boldsymbol\alpha_{253} = 1 \;\wedge\; \mathbf{k}_{254} = 0 &\implies \alpha'' + t_q \in [0, 2^{253}) \\ +\boldsymbol\alpha_{254} = 0 \;\wedge\; \mathbf{k}_{254} = 1 &\implies \alpha' - 2^{254} + t_q \in [0, 2^{130}) \;❁ \\ +\boldsymbol\alpha_{254} = 0 \;\wedge\; \mathbf{k}_{254} = 1 &\implies \alpha' - 2^{254} + 2^{130} \in [0, 2^{130}) \;❁ \\ +\end{aligned} +$$ + +Note that the four 130-bit constraints marked $❁$ are in two pairs that occur in disjoint cases. We can therefore combine them into two 130-bit constraints using a new witness variable $u$; the other constraint always being on $u + 2^{130} - t_q$: + +$$ +\begin{aligned} +\boldsymbol \alpha_{254} = 1 \implies &u = \alpha'' \\ +\boldsymbol\alpha_{254} = 0 \;\wedge\; \mathbf{k}_{254} = 1 \implies &u = \alpha' - 2^{254} + t_q \\ +&u \in [0, 2^{130}) \\ +&u + 2^{130} - t_q \in [0, 2^{130}) \\ +\end{aligned} +$$ + +($u$ is unconstrained and can be witnessed as $0$ in the case $\boldsymbol\alpha_{254} = 0 \;\wedge\; \mathbf{k}_{254} = 0$.) + +### Cost + +* 25 10-bit and one 3-bit range check, to constrain $\alpha''$ to 253 bits; +* 25 10-bit and one 3-bit range check, to constrain $\alpha'' + t_q$ to 253 bits when $\boldsymbol\alpha_{254} = 0 \;\wedge\; \boldsymbol\alpha_{253} = 1 \;\wedge\; \mathbf{k}_{254} = 0$; From c7d645997d3bda0a3d6626ce18d7efa8370bf24c Mon Sep 17 00:00:00 2001 From: Daira Hopwood Date: Fri, 2 Sep 2022 16:13:44 +0100 Subject: [PATCH 3/4] Apply suggestions from code review Co-authored-by: ying tong --- book/src/design/gadgets/ecc/var-base-scalar-mul.md | 1 + 1 file changed, 1 insertion(+) diff --git a/book/src/design/gadgets/ecc/var-base-scalar-mul.md b/book/src/design/gadgets/ecc/var-base-scalar-mul.md index e9a14663a7..49338d278b 100644 --- a/book/src/design/gadgets/ecc/var-base-scalar-mul.md +++ b/book/src/design/gadgets/ecc/var-base-scalar-mul.md @@ -476,3 +476,4 @@ $$ * 25 10-bit and one 3-bit range check, to constrain $\alpha''$ to 253 bits; * 25 10-bit and one 3-bit range check, to constrain $\alpha'' + t_q$ to 253 bits when $\boldsymbol\alpha_{254} = 0 \;\wedge\; \boldsymbol\alpha_{253} = 1 \;\wedge\; \mathbf{k}_{254} = 0$; +* two times 13 10-bit range checks. From 3abf14e273e4091fc294cc7e9c1f98c4efc6c375 Mon Sep 17 00:00:00 2001 From: Daira Hopwood Date: Fri, 2 Sep 2022 16:26:12 +0100 Subject: [PATCH 4/4] Clarify overflow condition --- book/src/design/gadgets/ecc/var-base-scalar-mul.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/book/src/design/gadgets/ecc/var-base-scalar-mul.md b/book/src/design/gadgets/ecc/var-base-scalar-mul.md index 49338d278b..d2109e08a4 100644 --- a/book/src/design/gadgets/ecc/var-base-scalar-mul.md +++ b/book/src/design/gadgets/ecc/var-base-scalar-mul.md @@ -405,7 +405,7 @@ We make use of a $10$-bit [lookup range check](../decomposition.md#lookup-decomp ## Overflow check (general) Recall that we defined $\mathbf{z}_j = \sum_{i=j}^n (\mathbf{k}_i \cdot 2^{i−j})$, where $n = 254$. -$\mathbf{z}_j$ cannot overflow for any $j \geq 1$, because it is a weighted sum of bits only up to $2^{n-j}$, which can be at most $2^{254} - 1$ when $j = 1$; this is smaller than $p$ (and also $q$). +$\mathbf{z}_j$ cannot overflow for any $j \geq 1$, because it is a weighted sum of bits only up to and including $2^{n-j}$. When $n = 254$ and $j = 1$ this sum can be at most $2^{254} - 1$, which is smaller than $p$ (and also $q$). However, for full-width scalar mul, it may not be possible to represent $\mathbf{z}_0$ in the base field (e.g. when the base field is Pasta's $\mathbb{F}_p$ and $p < q$). In that case $\mathbf{z}_0 = \alpha + t_q$ *can* overflow $[0, p)$.