# Variable-base scalar multiplication

In the Orchard circuit we need to check $pk_{d}=[ivk]g_{d}$ where $ivk∈[0,p)$ and the scalar field is $F_{q}$ with $p<q$.

We have $p=2_{254}+t_{p}$ and $q=2_{254}+t_{q}$, for $t_{p},t_{q}<2_{128}$.

## Witness scalar

We're trying to compute $[α]T$ for $α∈[0,q)$. Set $k=α+t_{q}$ and $n=254$. Then we can compute

$[2_{254}+(α+t_{q})]T =[2_{254}+(α+t_{q})−(2_{254}+t_{q})]T=[α]T $

provided that $α+t_{q}∈[0,2_{n+1})$, i.e. $α<2_{n+1}−t_{q}$ which covers the whole range we need because in fact $2_{255}−t_{q}>q$.

Thus, given a scalar $α$, we witness the boolean decomposition of $k=α+t_{q}.$ (We use big-endian bit order for convenient input into the variable-base scalar multiplication algorithm.)

$k=k_{254}⋅2_{254}+k_{253}⋅2_{253}+⋯+k_{0}.$

## Variable-base scalar multiplication

We use an optimized double-and-add algorithm, copied from "Faster variable-base scalar multiplication in zk-SNARK circuits" with some variable name changes:

```
Acc := [2] T
for i from n-1 down to 0 {
P := k_{i+1} ? T : −T
Acc := (Acc + P) + Acc
}
return (k_0 = 0) ? (Acc - T) : Acc
```

It remains to check that the x-coordinates of each pair of points to be added are distinct.

When adding points in a prime-order group, we can rely on Theorem 3 from Appendix C of the Halo paper, which says that if we have two such points with nonzero indices wrt a given odd-prime order base, where the indices taken in the range $−(q−1)/2..(q−1)/2$ are distinct disregarding sign, then they have different x-coordinates. This is helpful, because it is easier to reason about the indices of points occurring in the scalar multiplication algorithm than it is to reason about their x-coordinates directly.

So, the required check is equivalent to saying that the following "indexed version" of the above algorithm never asserts:

```
acc := 2
for i from n-1 down to 0 {
p = k_{i+1} ? 1 : −1
assert acc ≠ ± p
assert (acc + p) ≠ acc // X
acc := (acc + p) + acc
assert 0 < acc ≤ (q-1)/2
}
if k_0 = 0 {
assert acc ≠ 1
acc := acc - 1
}
```

The maximum value of `acc`

is:

```
<--- n 1s --->
1011111...111111
= 1100000...000000 - 1
```

= $2_{n+1}+2_{n}−1$

The assertion labelled X obviously cannot fail because $p=0$. It is possible to see that acc is monotonically increasing except in the last conditional. It reaches its largest value when $k$ is maximal, i.e. $2_{n+1}+2_{n}−1$.

So to entirely avoid exceptional cases, we would need $2_{n+1}+2_{n}−1<(q−1)/2$. But we can use $n$ larger by $c$ if the last $c$ iterations use complete addition.

The first $i$ for which the algorithm using **only** incomplete addition fails is going to be $252$, since $2_{252+1}+2_{252}−1>(q−1)/2$. We need $n=254$ to make the wraparound technique above work.

```
sage: q = 0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000001
sage: 2^253 + 2^252 - 1 < (q-1)//2
False
sage: 2^252 + 2^251 - 1 < (q-1)//2
True
```

So the last three iterations of the loop ($i=2..0$) need to use complete addition, as does the conditional subtraction at the end. Writing this out using ⸭ for incomplete addition (as we do in the spec), we have:

```
Acc := [2] T
for i from 253 down to 3 {
P := k_{i+1} ? T : −T
Acc := (Acc ⸭ P) ⸭ Acc
}
for i from 2 down to 0 {
P := k_{i+1} ? T : −T
Acc := (Acc + P) + Acc // complete addition
}
return (k_0 = 0) ? (Acc + (-T)) : Acc // complete addition
```

## Constraint program for optimized double-and-add

Define a running sum $z_{j}=∑_{i=j}(k_{i}⋅2_{i−j})$, where $n=254$ and:

$ z_{n+1}=0,z_{n}=k_{n},(most significant bit)z_{0}=k. $

$InitializeA_{254}=[2]T.forifrom254down to4:bool_check(k_{i})=0z_{i}=2z_{i+1}+k_{i}x_{P,i}=x_{T}y_{P,i}=(2k_{i}−1)⋅y_{T}(conditionally negate)λ_{1,i}⋅(x_{A,i}−x_{P,i})=y_{A,i}−y_{P,i}x_{R,i}=λ_{1,i}−x_{A,i}−x_{P,i}(λ_{1,i}+λ_{2,i})⋅(x_{A,i}−x_{R,i})=2y_{A,i}λ_{2,i}=x_{A,i−1}+x_{R,i}+x_{A,i}λ_{2,i}⋅(x_{A,i}−x_{A,i−1})=y_{A,i}+y_{A,i−1}. $

The helper $bool_check(x)=x⋅(1−x)$. After substitution of $x_{P,i},y_{P,i},x_{R,i},y_{A,i}$, and $y_{A,i−1}$, this becomes:

$InitializeA_{254}=[2]T.forifrom254down to4:// letk_{i}=z_{i}−2z_{i+1}// lety_{A,i}=2(λ_{1,i}+λ_{2,i})⋅(x_{A,i}−(λ_{1,i}−x_{A,i}−x_{T})) bool_check(k_{i})=0λ_{1,i}⋅(x_{A,i}−x_{T})=y_{A,i}−(2k_{i}−1)⋅y_{T}λ_{2,i}=x_{A,i−1}+λ_{1,i}−x_{T}{λ_{2,i}⋅(x_{A,i}−x_{A,i−1})=y_{A,i}+y_{A,i−1},λ_{2,4}⋅(x_{A,4}−x_{A,3})=y_{A,4}+y_{A,3}, ifi>4ifi=4. $

Here, $y_{A,3}$ is assigned to a cell. This is unlike previous $y_{A,i}$'s, which were implicitly derived from $λ_{1,i},λ_{2,i},x_{A,i},x_{T}$, but never actually assigned.

The bits $k_{3…1}$ are used in three further steps, using complete addition:

$forifrom3down to1:// letk_{i}=z_{i}−2z_{i+1}bool_check(k_{i})=0(x_{A,i−1},y_{A,i−1})=((x_{A,i},y_{A,i})+(x_{T},y_{T}))+(x_{A,i},y_{A,i}) $

If the least significant bit $k_{0}=1,$ we set $B=O,$ otherwise we set $B=−T$. Then we return $A+B$ using complete addition.

Let $B={(0,0),(x_{T},−y_{T}), ifk_{0}=1,otherwise. $

Output $(x_{A,0},y_{A,0})+B$.

(Note that $(0,0)$ represents $O$.)

## Incomplete addition

We need six advice columns to witness $(x_{T},y_{T},λ_{1},λ_{2},x_{A,i},z_{i})$. However, since $(x_{T},y_{T})$ are the same, we can perform two incomplete additions in a single row, reusing the same $(x_{T},y_{T})$. We split the scalar bits used in incomplete addition into $hi$ and $lo$ halves and process them in parallel. This means that we effectively have two for loops:

- the first, covering the $hi$ half for $i$ from $254$ down to $130$, with a special case at $i=130$; and
- the second, covering the $lo$ half for the remaining $i$ from $129$ down to $4$, with a special case at $i=4$.

$x_{T}x_{T}x_{T}⋮x_{T}x_{T} y_{T}y_{T}y_{T}⋮y_{T}y_{T} z_{hi}z_{255}=0z_{254}z_{253}⋮z_{130} x_{A}x_{A,254}=2[T]_{x}x_{A,253}⋮x_{A,130}x_{A,129} λ_{1}y_{A,254}=2[T]_{y}λ_{1,254}λ_{1,253}⋮λ_{1,130}y_{A,129} λ_{2}λ_{2,254}λ_{2,253}⋮λ_{2,130} q_{1}100⋮0 q_{2}011⋮0 q_{3}000⋮1 z_{lo}z_{130}z_{129}z_{128}⋮z_{5}z_{4} x_{A}x_{A,129}x_{A,128}⋮x_{A,5}x_{A,4}x_{A,3} λ_{1}y_{A,129}λ_{1,129}λ_{1,128}⋮λ_{1,5}λ_{1,4}y_{A,3} λ_{2}λ_{2,129}λ_{2,128}⋮λ_{2,5}λ_{2,4} q_{1}100⋮00 q_{2}011⋮10 q_{3}000⋮01 $

For each $hi$ and $lo$ half, we have three sets of gates. Note that $i$ is going from $255..=3$; $i$ is NOT indexing the rows.

### $q_{1}=1$

This gate is only used on the first row (before the for loop). We check that $λ_{1},λ_{2}$ are initialized to values consistent with the initial $y_{A}.$ $Degree4 Constraintq_{1}⋅(y_{A,n}−y_{A,n})=0 $ where $y_{A,n}y_{A,n} =2(λ_{1,n}+λ_{2,n})⋅(x_{A,n}−(λ_{1,n}−x_{A,n}−x_{T})) ,is witnessed. $

### $q_{2}=1$

This gate is used on all rows corresponding to the for loop except the last.

$Degree223433 Constraintq_{2}⋅(x_{T,cur}−x_{T,next})=0q_{2}⋅(y_{T,cur}−y_{T,next})=0q_{2}⋅bool_check(k_{i})=0,wherek_{i}=z_{i}−2z_{i+1}q_{2}⋅(λ_{1,i}⋅(x_{A,i}−x_{T,i})−y_{A,i}+(2k_{i}−1)⋅y_{T,i})=0q_{2}⋅(λ_{2,i}−x_{A,i−1}−x_{R,i}−x_{A,i})=0q_{2}⋅(λ_{2,i}⋅(x_{A,i}−x_{A,i−1})−y_{A,i}−y_{A,i−1})=0 $ where $x_{R,i}y_{A,i}y_{A,i−1} =λ_{1,i}−x_{A,i}−x_{T},=2(λ_{1,i}+λ_{2,i})⋅(x_{A,i}−(λ_{1,i}−x_{A,i}−x_{T})) ,=2(λ_{1,i−1}+λ_{2,i−1})⋅(x_{A,i−1}−(λ_{1,i−1}−x_{A,i−1}−x_{T})) , $

### $q_{3}=1$

This gate is used on the final iteration of the for loop, handling the special case where we check that the output $y_{A}$ has been witnessed correctly. $Degree3433 Constraintq_{3}⋅bool_check(k_{i})=0,wherek_{i}=z_{i}−2z_{i+1}q_{3}⋅(λ_{1,i}⋅(x_{A,i}−x_{T,i})−y_{A,i}+(2k_{i}−1)⋅y_{T,i})=0q_{3}⋅(λ_{2,i}−x_{A,i−1}−x_{R,i}−x_{A,i})=0q_{3}⋅(λ_{2,i}⋅(x_{A,i}−x_{A,i−1})−y_{A,i}−y_{A,i−1})=0 $ where $x_{R,i}y_{A,i}y_{A,i−1} =λ_{1,i}−x_{A,i}−x_{T},=2(λ_{1,i}+λ_{2,i})⋅(x_{A,i}−(λ_{1,i}−x_{A,i}−x_{T})) ,is witnessed. $

## Complete addition

We reuse the complete addition constraints to implement the final $c$ rounds of double-and-add. This requires two rows per round because we need 9 advice columns for each complete addition. In the 10th advice column we stash the other cells that we need to correctly implement the double-and-add:

- The base $y$ coordinate, so we can conditionally negate it as input to one of the complete additions.
- The running sum, which we constrain over two rows instead of sequentially.

### Layout

$a_{0}x_{T}x_{A} a_{1}y_{p}y_{A} a_{2}x_{A}x_{q}x_{r} a_{3}y_{A}y_{q}y_{r} a_{4}λ_{1}λ_{2} a_{5}α_{1}α_{2} a_{6}β_{1}β_{2} a_{7}γ_{1}γ_{2} a_{8}δ_{1}δ_{2} a_{9}z_{i+1}y_{T}z_{i} q_{mul_decompose_var}010 $

### Constraints

In addition to the complete addition constraints, we define the following gate:

$Degree Constraintq_{mul_decompose_var}⋅bool_check(k_{i})=0q_{mul_decompose_var}⋅ternary(k_{i},y_{T}−y_{p},y_{T}+y_{p})=0 $ where $k_{i}=z_{i}−2z_{i+1}$.

## LSB

### Layout

$a_{0}x_{p}x_{T} a_{1}y_{p}y_{T} a_{2}x_{A}x_{r} a_{3}y_{A}y_{r} a_{4}λ a_{5}α a_{6}β a_{7}γ a_{8}δ a_{9}z_{1}z_{0} q_{mul_lsb}10 $

### Constraints

$Degree Constraintq_{mul_lsb}⋅bool_check(k_{0})=0q_{mul_lsb}⋅ternary(k_{0},x_{p},x_{p}−x_{T})=0q_{mul_lsb}⋅ternary(k_{0},y_{p},y_{p}+y_{T})=0 $ where $k_{0}=z_{0}−2z_{1}$.

## Overflow check

$z_{i}$ cannot overflow for any $i≥1$, because it is a weighted sum of bits only up to $2_{n−1}=2_{253}$, which is smaller than $p$ (and also $q$).

However, $z_{0}=α+t_{q}$ *can* overflow $[0,p)$.

Note: for full-width scalar mul, it may not be possible to represent $z_{0}$ in the base field (e.g. when the base field is Pasta's $F_{p}$ and $p<q$). In that case, we need to special-case the row that would mention $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 $(k_{254},k_{′}=k−2_{254}⋅k_{254})$. We'll use $k_{′}$ in place of $α+t_{q}$ for $z_{0}$, constraining $k_{′}$ to 254 bits so that it fits in an $F_{p}$ element. Then we just have to generalize the argument below to work for $k_{′}∈[0,2⋅t_{q})$ (because the maximum value of $α+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 $z_{0}=2⋅z_{1}+k_{0}$, we have $z_{0}=k(modp)$. It is then sufficient to also check that $z_{0}=α+t_{q}(modp)$ (so that $k=α+t_{q}(modp)$) and that $k∈[t_{q},p+t_{q})$. These conditions together imply that $k=α+t_{q}$ as an integer, and so $2_{254}+k=α(modq)$ as required.

Note: the bits $k_{254..0}$ do not represent a value reduced modulo $q$, but rather a representation of the unreduced $α+t_{q}$.

### Optimized check for $k∈[t_{q},p+t_{q})$

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})∪[2_{130},2_{254})∪([2_{254},2_{254}+2_{130})∩[p+t_{q}−2_{130},p+t_{q})).$

We may assume that $k=α+t_{q}(modp)$.

(This is true for the use of variable-base scalar mul in Orchard, where we know that $α<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 $α≥p$ when $p<q$.)

Therefore, $k∈[t_{q},p+t_{q}) ⇔⇔⇔ (k∈[t_{q},t_{q}+2_{130})∨k∈[2_{130},2_{254}))∨(k∈[2_{254},2_{254}+2_{130})∧k∈[p+t_{q}−2_{130},p+t_{q}))(k_{254}=0⟹(k∈[t_{q},t_{q}+2_{130})∨k∈[2_{130},2_{254})))∧(k_{254}=1⟹(k∈[2_{254},2_{254}+2_{130})∧k∈[p+t_{q}−2_{130},p+t_{q})))(k_{254}=0⟹(α∈[0,2_{130})∨k∈[2_{130},2_{254})))∧(k_{254}=1⟹(k∈[2_{254},2_{254}+2_{130})∧(α+2_{130})modp∈[0,2_{130})))Ⓐ $

Given $k∈[2_{254},2_{254}+2_{130})$, we prove equivalence of $k∈[p+t_{q}−2_{130},p+t_{q})$ and $(α+2_{130})modp∈[0,2_{130})$ as follows:

- shift the range by $2_{130}−p−t_{q}$ to give $k+2_{130}−p−t_{q}∈[0,2_{130})$;
- observe that $k+2_{130}−p−t_{q}$ is guaranteed to be in $[2_{130}−t_{p}−t_{q},2_{131}−t_{p}−t_{q})$ and therefore cannot overflow or underflow modulo $p$;
- using the fact that $k=α+t_{q}(modp)$, observe that $(k+2_{130}−p−t_{q})modp=(α+t_{q}+2_{130}−p−t_{q})modp=(α+2_{130})modp$.
(We can see in a different way that this is correct by observing that it checks whether $αmodp∈[p−2_{130},p)$, so the upper bound is aligned as we would expect.)

Now, we can continue optimizing from $Ⓐ$:

$k∈[t_{q},p+t_{q}) ⇔⇔ (k_{254}=0⟹(α∈[0,2_{130})∨k∈[2_{130},2_{254}))∧(k_{254}=1⟹(k∈[2_{254},2_{254}+2_{130})∧(α+2_{130})modp∈[0,2_{130})))(k_{254}=0⟹(α∈[0,2_{130})∨k_{253..130}are not all0))∧(k_{254}=1⟹(k_{253..130}are all0∧(α+2_{130})modp∈[0,2_{130}))) $

Constraining $k_{253..130}$ to be all-$0$ or not-all-$0$ can be implemented almost "for free", as follows.

Recall that $z_{i}=∑_{h=i}(k_{h}⋅2_{h−i})$, so we have:

$z_{130}z_{130}z_{130}−k_{254}⋅2_{124} === ∑_{h=130}(k_{h}⋅2_{h−130})k_{254}⋅2_{254−130}+∑_{h=130}(k_{h}⋅2_{h−130})∑_{h=130}(k_{h}⋅2_{h−130}) $

So $k_{253..130}$ are all $0$ exactly when $z_{130}=k_{254}⋅2_{124}$.

Finally, we can merge the $130$-bit decompositions for the $k_{254}=0$ and $k_{254}=1$ cases by checking that $(α+k_{254}⋅2_{130})modp∈[0,2_{130})$.

### Overflow check constraints

Let $s=α+k_{254}⋅2_{130}$. The constraints for the overflow check are:

$z_{0}k_{254}=1⟹(z_{130}k_{254}=0⟹(z_{130} =α+t_{q}(modp)=2_{124}∧smodp∈[0,2_{130}))=0∨smodp∈[0,2_{130})) $

Define $inv0(x)={0,1/x, ifx=0otherwise. $

Witness $η=inv0(z_{130})$, and decompose $smodp$ as $s_{129..0}$.

Then the needed gates are:

$Degree22335 Constraintq_{mul_overflow}⋅(s−(α+k_{254}⋅2_{130}))=0q_{mul_overflow}⋅(z_{0}−α−t_{q})=0q_{mul_overflow}⋅(k_{254}⋅(z_{130}−2_{124}))=0q_{mul_overflow}⋅(k_{254}⋅(s−i=0∑129 2_{i}⋅s_{i})/2_{130})=0q_{mul_overflow}⋅((1−k_{254})⋅(1−z_{130}⋅η)⋅(s−i=0∑129 2_{i}⋅s_{i})/2_{130})=0 $ where $(s−i=0∑129 2_{i}⋅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.

#### Running sum range check

We make use of a $10$-bit lookup range check in the circuit to subtract the low $130$ bits of $s$. The range check subtracts the first $13⋅10$ bits of $s,$ and right-shifts the result to give $(s−i=0∑129 2_{i}⋅s_{i})/2_{130}.$

## Overflow check (general)

Recall that we defined $z_{j}=∑_{i=j}(k_{i}⋅2_{i−j})$, where $n=254$.

$z_{j}$ cannot overflow for any $j≥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 $z_{0}$ in the base field (e.g. when the base field is Pasta's $F_{p}$ and $p<q$). In that case $z_{0}=α+t_{q}$ *can* overflow $[0,p)$.

So, we need to special-case the row that would mention $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 $(k_{254},k_{′}=k−2_{254}⋅k_{254})$. We'll use $k_{′}$ in place of $α+t_{q}$ for $z_{0}$, constraining $k_{′}$ to 254 bits so that it fits in an $F_{p}$ element.

Then we just have to generalize the overflow check used for variable-base scalar mul in the Orchard circuit to work for $k_{′}∈[0,2⋅t_{q})$ (because the maximum value of $α+t_{q}$ is $q−1+t_{q}=2_{254}+t_{q}−1+t_{q}$).

Note: the bits $k_{254..0}$ do not represent a value reduced modulo $q$, but rather a representation of the unreduced $α+t_{q}$.

Overflow can only occur in the final step that constrains $z_{0}=2⋅z_{1}+k_{0}$, and only if $z_{1}$ has the bit with weight $2_{253}$ set (i.e. if $k_{254}=1$). If we instead set $z_{0}=2⋅z_{1}−2_{254}⋅k_{254}+k_{0}$, now $z_{0}$ cannot overflow and should be equal to $k_{′}$.

It is then sufficient to also check that $z_{0}+2_{254}⋅k_{254}=α+t_{q}$ as an integer where $α∈[0,q)$.

Represent $α$ as $2_{254}⋅α_{254}+2_{253}⋅α_{253}+α_{′′}$ where we constrain $α_{′′}∈[0,2_{253})$ and $α_{253}$ and $α_{254}$ to boolean. For this to be a canonical representation we also need $α_{254}=1⟹(α_{253}=0∧α_{′′}∈[0,t_{q}))$.

Let $α_{′}=2_{253}⋅α_{253}+α_{′′}$.

If $α_{254}=1$:

- constrain $k_{254}=1$ and $z_{0}=α_{′}+t_{q}$. This cannot overflow because in this case $α_{′}∈[0,t_{q})$ and so $z_{0}∈[0,2⋅t_{q})$.

If $α_{254}=0$:

- we should have $k_{254}=1$ iff $α_{′}∈[2_{254}−t_{q},2_{254})$, i.e. witness $k_{254}$ as boolean and then
- If $k_{254}=0$ then constrain $α_{′}∈[2_{254}−t_{q},2_{254})$.
- This can be done by constraining either $α_{253}=0$ or $α_{′′}+t_{q}∈[0,2_{253})$. ($α_{′′}+t_{q}$ cannot overflow.)

- If $k_{254}=1$ then constrain $α_{′}∈[2_{254}−t_{q},2_{254})$.
- This can be done by constraining $α_{′}−(2_{254}−t_{q})∈[0,2_{130})$ and $α_{′}−2_{254}+2_{130}∈[0,2_{130})$.

- If $k_{254}=0$ then constrain $α_{′}∈[2_{254}−t_{q},2_{254})$.

### Overflow check constraints (general)

Represent $α$ as $2_{254}⋅α_{254}+2_{253}⋅α_{253}+α_{′′}$ as above.

The constraints for the overflow check are:

$α_{254}=1⟹α_{254}=1⟹α_{254}=1⟹α_{254}=1⟹α_{254}=1⟹α_{254}=0∧α_{253}=1∧k_{254}=0α_{254}=0∧k_{254}=1α_{254}=0∧k_{254}=1 α_{′′}∈[0,2_{253})α_{253}∈{0,1}α_{254}∈{0,1}k_{254}∈{0,1}α_{253}=0α_{′′}∈[0,2_{130})❁α_{′′}+2_{130}−t_{q}∈[0,2_{130})❁k_{254}=1z_{0}=α_{′}+t_{q}⟹α_{′′}+t_{q}∈[0,2_{253})⟹α_{′}−2_{254}+t_{q}∈[0,2_{130})❁⟹α_{′}−2_{254}+2_{130}∈[0,2_{130})❁ $

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}$:

$α_{254}=1⟹α_{254}=0∧k_{254}=1⟹ u=α_{′′}u=α_{′}−2_{254}+t_{q}u∈[0,2_{130})u+2_{130}−t_{q}∈[0,2_{130}) $

($u$ is unconstrained and can be witnessed as $0$ in the case $α_{254}=0∧k_{254}=0$.)

### Cost

- 25 10-bit and one 3-bit range check, to constrain $α_{′′}$ to 253 bits;
- 25 10-bit and one 3-bit range check, to constrain $α_{′′}+t_{q}$ to 253 bits when $α_{254}=0∧α_{253}=1∧k_{254}=0$;
- two times 13 10-bit range checks.