Module halo2_gadgets::utilities::decompose_running_sum
source · [−]Expand description
Decomposes an $n$-bit field element $\alpha$ into $W$ windows, each window being a $K$-bit word, using a running sum $z$. We constrain $K \leq 3$ for this helper. $$\alpha = k_0 + (2^K) k_1 + (2^{2K}) k_2 + … + (2^{(W-1)K}) k_{W-1}$$
$z_0$ is initialized as $\alpha$. Each successive $z_{i+1}$ is computed as
$$z_{i+1} = (z_{i} - k_i) / (2^K).$$
$z_W$ is constrained to be zero.
The difference between each interstitial running sum output is constrained
to be $K$ bits, i.e.
range_check($k_i$, $2^K$),
where
range_check(word, range)
= word * (1 - word) * (2 - word) * ... * ((range - 1) - word)Given that the range_check constraint will be toggled by a selector, in
practice we will have a selector * range_check(word, range) expression
of degree range + 1.
This means that $2^K$ has to be at most degree_bound - 1 in order for
the range check constraint to stay within the degree bound.
Structs
The running sum $[z_0, …, z_W]$. If created in strict mode, $z_W = 0$.
Configuration that provides methods for running sum decomposition.