diff --git a/spec/add.typ b/spec/add.typ index 21332e8f6..1f9e1698d 100644 --- a/spec/add.typ +++ b/spec/add.typ @@ -28,6 +28,11 @@ This template introduces #nr_interactions interaction(s). This template introduces the following constraints #render_constraint_table(chip, config) +Note that the correctness of these constraints follows from @lm:limb-decomposition-constraint-correctness, when applied to $(S, L, C, alpha, mu) = (2^64, 2^32, 2, 2, 0)$: +- the definition of `carry` matches that of @eq:def_ci and @eq:c_-1_is_zero, +- @eq:range_ci is enforced by @add:c:carry, and +- @eq:range_wi follows from @add:a:sum. + = #sub For ease of notation, we moreover introduce the #sub constraint template diff --git a/spec/book.typ b/spec/book.typ index 8bf8612af..6d7554455 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -49,6 +49,9 @@ ("commit.typ", [`COMMIT` chip], ), ("sha256.typ", [`SHA256` accelerator], ), ("keccak.typ", [`KECCAK` accelerator], ), + )), + ("MATHEMATICS", ( + ("limbs_and_carries.typ", [On limb decomposition and carries], ), )) ) ) diff --git a/spec/limbs_and_carries.typ b/spec/limbs_and_carries.typ new file mode 100644 index 000000000..061ca1fc9 --- /dev/null +++ b/spec/limbs_and_carries.typ @@ -0,0 +1,240 @@ +#import "/book.typ": book-page +#import "@preview/ctheorems:1.1.3": * +#import "@preview/equate:0.3.2": equate + + +// Theorem/lemma formatting +#show: thmrules.with(qed-symbol: $square$) +#let lemma = thmbox("lemma", "Lemma", fill: rgb("#eee"),base_level: 0) +#let corollary = thmbox("lemma", "Corrollary", fill: rgb("#eee"), base_level: 0) +#let proof = thmproof("proof", "Proof") + +// Equation formatting +#show: equate.with(breakable: true, sub-numbering: true) +#set math.equation(numbering: "(1.1)") +#show math.equation.where(block: false): box + +#show: book-page("limbs_and_carries.typ") + +In this section, we discuss, in order, ++ the multiplication and addition of limb-decomposed integers (involving carries), ++ prove an upper bound on the size of the carries in terms of the number of + multiplications and additions, and ++ prove correctness of a set of constraints that can be used to constrain quadratic relations. + += Limb decomposition +Let $[X]$ denote the set ${0, ..., X-1} subset.eq NN$. +Let $S := L^n in NN$ be an upper bound on the integers we want to represent, +where $L in NN without {0, 1}$ is the number of values a limb can represent +and $n in N$ denotes the number of limbs. + +Observe that for all $x in [S]$, there exists a unique tuple of integers +$(x_0, x_1, x_2, x_(n-1)) in [L]^(n)$ such that +$ + x + = sum_(i=0)^(n-1) x_i dot L^i. +$ # +To simplify future notation, we define $x_i := 0$ for all $i >= n$. +Next, we define the family of multi-linear functions +$ +f_(mu, alpha) (x, y, z) := sum_(m in [mu]) (x^((m)) dot y^((m))) + sum_(a in [alpha]) z^((a)) +$ +over variables $x, y in [S]^mu$ and $z in [S]^alpha$, with parameters $mu, alpha in NN$. +Working towards the limb-decomposition of $f_(mu, alpha)$, we rewrite + +$ + f_(mu, alpha) (x, y, z) + &= sum_(m in [mu]) (sum_(i=0)^(n-1) x^((m))_i dot L^i) (sum_(j=0)^(n-1) y^((m))_j dot L^j) + sum_(a in [alpha]) (sum_(k=0)^(n-1) z^((a))_k dot L^k)\ + &= sum_(m in [mu]) (sum_(i=0)^(n-1) sum_(j=0)^(n-1) x^((m))_i dot y^((m))_j dot L^(i+j)) + sum_(a in [alpha]) (sum_(k=0)^(n-1) z^((a))_k dot L^k)\ + &= sum_(i=0)^(n-1) sum_(j=0)^(n-1) (sum_(m in [mu]) x^((m))_i dot y^((m))_j dot L^(i+j)) + sum_(k=0)^(n-1) (sum_(a in [alpha]) z^((a))_k dot L^k)\ + &= sum_(i=0)^(n-1) (sum_(j=0)^(n-1) (sum_(m in [mu]) x^((m))_i dot y^((m))_j dot L^(i+j)) + sum_(a in [alpha]) z^((a))_i dot L^i )\ + &= sum_(r=0)^(2(n-1)) (sum_(j=0)^(r) (sum_(m in [mu]) x^((m))_(r-j) dot y^((m))_j dot L^r) + sum_(a in [alpha]) z^((a))_r dot L^r )\ + &= sum_(r=0)^(2(n-1)) (sum_(j=0)^(r) (sum_(m in [mu]) x^((m))_(r-j) dot y^((m))_j) + sum_(a in [alpha]) z^((a))_r) dot L^r\ + &= sum_(r=0)^(2(n-1)) overline(w)_r dot L^r, # +$ +where +$ + overline(w)_i := sum_(m in [mu]) (sum_(j=0)^(i) x^((m))_(i-j) dot y^((m))_j) + sum_(a in [alpha]) z^((a))_i. +$ + +While @eq:f-semi-decomposition closely resembles that of a limb-decomposition (@eq:decomposition), +there is the problem that $overline(w)_i$ will exceed $L$ for sufficiently large $alpha, mu, x, y, z$, and $i$. +We therefore introduce helper sequence $c_i$ to transform $overline(w)_i$ into a proper decomposition $w_i$ as: +$ + w_i &:= overline(w)_i + c_(i-1) mod L &text("for") i >= 0,\ + c_i &:= (overline(w)_i + c_(i-1) - w_i )/L &text("for") i >= 0,\ +$ +with $c_i in NN$ and $c_(-1) := 0$. +Note that these $c_i$ effectively move the "overflow" from one limb to the next limb up; +they're commonly referred to as the _carry_ values. + +#lemma[ + For all $g >= 2n-1$, + $(w_0, w_1, ..., w_(g-1)) in [L]^(g)$ + is the unique $g$-limb decomposition of $f_(mu, alpha)$ + if and only if $c_(g-1) = 0$. +] +#proof[ + Reordering the definition of $c_i$, we find the equality $w_i = overline(w)_i + c_(i-1) - c_i dot L$. + Leveraging this, we see that + $ + sum_(r=0)^(g-1) w_r dot L^r + &= sum_(r=0)^(g-1) (overline(w)_r + c_(r-1) - c_r dot L) dot L^r\ + &= (sum_(r=0)^(g-1) overline(w)_r dot L^r) + (sum_(s=0)^(g-1) c_(s-1) dot L^s) - (sum_(t=0)^(g-1) c_t dot L^(t+1))\ + &= (sum_(r=0)^(g-1) overline(w)_r dot L^r) + (sum_(s=-1)^(g-2) c_(s) dot L^(s+1)) - (sum_(t=0)^(g-1) c_t dot L^(t+1))\ + &= (sum_(r=0)^(g-1) overline(w)_r dot L^r) + c_(-1) - c_(g-1) dot L^(g-1+1)\ + &= (sum_(r=0)^(g-1) overline(w)_r dot L^r) - c_(g-1) dot L^(g),\ + &= (sum_(r=0)^(2(n-1)) overline(w)_r dot L^r) - c_(g-1) dot L^(g),\ + &= f_(mu, alpha)(x, y, z) - c_(g-1) dot L^(g),\ + $ + where the second-to-last step follows from the observation that $overline(w)_j = 0$ for $j > 2(n-1)$. + We conclude that $w_i$ is a proper $g$-limb decomposition of $f_(mu,alpha)$ if and only if $c_(g-1) = 0$. +] + += Upper bounding the carry +To find some of the conditions under which $c_(g-1) = 0$, we prove two upperbounds for $c_i$. + +#lemma("Carry upper bound [part 1]")[ + For $alpha, mu in [L]$, it holds that + $ + c_i <= mu (i+1) (L-1) + alpha - mu - delta_(mu < alpha) + $ + where kronecker delta $delta_x$ equals $1$ if $x$ holds, and $0$ otherwise. +] + +#proof[ + Since $w_i in [L]$, + $c_i + :=(overline(w)_i + c_(i-1) - w_i ) dot L^(-1) + = floor.l (overline(w)_i + c_(i-1)) dot L^(-1) floor.r.$ + Hence, $c_i$ is maximized when both $overline(w)_i$ and $c_(i-1)$ are, and thus, + by induction, when $overline(w)_j$ is maximized for all $j <= i$. + Given that $x^((m))_i, y^((m))_i, z^((a))_i <= L-1$ for all $m < mu, a < alpha, i < n$, it follows that + $ + + &overline(w)_0 + &=& sum_(m in [mu]) (x^((m))_0 dot y^((m))_0) + sum_(a in [alpha]) z^((a))_0\ + &&<=& mu (L - 1)^2 + alpha (L-1)\ + &&=& mu (L - 2)L + mu + (alpha - delta) L + delta L - alpha\ + &&=& mu (L - 2)L + (alpha - delta) L + delta L + mu - alpha,\ + text("and hence") &c_0 + &<=& lr(floor.l (mu (L - 2)L + (alpha - delta) L + delta L + mu - alpha)/ L floor.r)\ + &&=& mu (L - 2) + alpha - delta \ + &&=& mu dot 1 dot (L - 1) + alpha - mu - delta \ + $ + where $delta := delta_(mu < alpha)$. + Assuming the statement holds for up to some $i >= 0$, we find that + $ + overline(w)_(i+1) + &= sum_(m in [mu]) (sum_(j=0)^(i+1) x^((m))_(i+1-j) dot y^((m))_j) + sum_(a in [alpha]) z^((a))_(i+1) \ + &<= mu (i+2)(L-1)^2 + alpha (L-1),\ + c_(i+1) + &<= lr(floor.l (mu (i+2) (L-1)^2 + alpha (L-1) + mu (i+1) (L-1) + alpha - mu - delta)/L floor.r)\ + &= lr(floor.l (mu (i+2) (L - 2)L + mu (i+1) L + (alpha - delta) L + delta (L-1))/ L floor.r)\ + &= mu (i+2) (L - 2) + mu (i+1) + alpha - delta\ + &= mu (i+2) (L - 1) + alpha - mu - delta. + $ +] + +Inspecting this upper bound, we find that it is _tight_ for all $i= n$, we introduce a second lemma: + +#lemma("Carry upper bound [part 2]")[ + For $alpha in [L], mu in [L/2]$, it holds that + $ + c_(n+k) <= mu (n - k - 1)(L-2) + mu (n-k) - delta_(alpha < 2mu + delta) + $ + for $k in [n]$. +] + +#proof[ + Starting with $k=0$, we find + $ + overline(w)_n + &= sum_(m in [mu]) (sum_(j=0)^(n) x^((m))_(n-j) dot y^((m))_j) + sum_(a in [alpha]) z^((a))_n\ + &<= mu (n-1) (L-1)^2 + $ + since $x^((m))_i$, $y^((m))_i$, and $z^((a))$ are $0$ for $i >= n$. + Applying this upper bound to $c_n$, we obtain + $ + c_(n) + &= lr(floor.l (overline(w)_n + c_(n-1))/ L floor.r)\ + &<= lr(floor.l (mu (n-1) (L-1)^2 + mu n (L-1) + alpha - mu - delta)/ L floor.r)\ + &= lr(floor.l (mu (n-1) (L-2)L + mu (n-1) + mu n (L-1) + alpha - mu - delta) / L floor.r)\ + &= lr(floor.l (mu (n-1) (L-2)L + (mu n - delta') L + delta'L + alpha - 2mu - delta) / L floor.r)\ + &= mu (n-1) (L-2) + mu n - delta'\ + &= mu (n-0-1) (L-2) + mu (n-0) - delta'\ + $ + where $delta' := delta_(alpha < 2mu + delta)$. + When the bound holds for some $i=n+k-1$ with $k in [1, n)$, it follows that + $ + overline(w)_(n+k) + &= sum_(m in [mu]) (sum_(j=0)^(n+k) x^((m))_(n+k-j) dot y^((m))_j) + sum_(a in [alpha]) z^((a))_(n+k)\ + &<= mu (n-k-1) (L-1)^2\ + c_(n+k) + &<= lr(floor.l (mu (n-k-1) (L-1)^2 + mu (n-k)(L-2) + mu (n - k + 1) - delta') / L floor.r)\ + &= lr(floor.l (mu (n-k-1) (L-2)L + mu (n-k)L - delta') / L floor.r)\ + &= lr(floor.l (mu (n-k-1) (L-2)L + mu (n-k)L - delta'L + delta'(L-1)) / L floor.r)\ + &= mu (n-k-1) (L-2) + mu (n-k)-delta'. + $ + The claimed upper bound now follows for all $k in [0, n)$ by induction. +] + +Combining both upper bounds, we now find that + +#corollary[ +Given $alpha in [L]$ and $mu in [L/2]$, then for all $i <= 2n$: +$ +c_i <= &max(&max_(i in [n]) #h(1em) mu (i+1) (L-1) + alpha - mu - delta,\ + &max_(k in [n]) #h(1em) mu (2n-k-1)(L-2) + mu (2n-k) - delta')\ +&= max(& mu n (L-1) + alpha - mu - delta, mu (2n-1)(L-2) + 2 mu n - delta')\ +&= mu n (L-1) + alpha - mu - delta +$ +] + +Note that this upper bound is tight: +$c_(n+k)$ achieves the bound for all $k in [n]$ when $x^((m)) = y^((m)) = z^((a)) = S-1$ for all $m in [mu]$ and $a in [alpha]$. +For $k = n-1$, this yields $c_(n+(n-1)) = c_(2n-1) <= mu - delta'$, which evaluates to zero when $mu = 0$ and $alpha < L$, or $mu = 1$ and $alpha <= 2$. +We can therefore conclude that $(w_0, w_1, ..., w_(2n-1)) in [L]^(2n)$ is a valid $2n$-limb decomposition of $f_(mu, alpha) (x, y, z)$ in these cases. +For larger values of $mu in [2, L/2]$, we note that $c_(2n) <= floor.l frac((mu - delta'), L, style: "horizontal") floor.r = 0$ and thus $c_(2n + i) = 0$ for all $i >= 0$. +Hence, attaching extra limb $w_(2n) := c_(2n)$ yields a $(2n+1)$-limb decomposition for these cases. + += Proof of Correctness +Lastly, we prove that there exists a correct method of constraining the relation between $overline(w)_i$, $w_i$ and $c_i$ inside this VM: + +#lemma("Constraint correctness")[ + Let $c_i, w_i in FF_p$ with $p$ prime. + The constraints + $ + c_i &= (overline(w)_i + c_(i-1) - w_i) dot L^(-1), #\ + c_i &in [C], #\ + c_(-1) &= 0, #\ + w_i &in [L] # + $ + together enforce $w_i = overline(w)_i + c_(i-1) mod L$ as long as $C in [mu n L + alpha, frac(p,L, style:"horizontal"))$. +] + +#proof[ + Combining @eq:def_ci and @eq:range_ci, we find that + $ + &&c_i &in [C]\ + &<=>& overline(w)_i + c_(i-1) - w_i &in {0, L, ..., (C-1)L},\ + &<=>& w_i &in {overline(w)_i + c_(i-1), overline(w)_i + c_(i-1) - L, ..., overline(w)_i + c_(i-1) - (C-1)L}. + $ + Let us use $X_(i)$ to refer to this last set. + Now --- under the assumption that $c_(i-1)$ is correct --- + observe that $w_i := overline(w)_i + c_(i-1) mod L in X_i$, since + $ + overline(w)_i + c_(i-1) + &<= (mu n (L-1)^2 + alpha (L-1)) + (mu (n-1) (L-1) + alpha - mu - delta)\ + &<= mu n L^2 + alpha L\ + &<= C L,\ + $ + where the utilized upper bound + $overline(w)_i <= mu n(L-1)^2 + alpha (L-1)$ + can be extracted from the proofs of @lm:carry-upperbound-pt1 and @lm:carry-upperbound-pt2. + Moreover, observe that $|X_i inter [L]| <= 1$ since $C < frac(p,L, style:"horizontal")$. + Constraint @eq:range_wi therefore enforces that $w_i = overline(w)_i + c_(i-1) mod L$ if $c_(i-1)$ (and therefore $w_(i-1)$) is correct, + and as a result, $c_i = floor.l frac(overline(w)_i + c_(i-1), L, style: "horizontal") floor.r$ is correct. + The proof now follows by induction, with @eq:c_-1_is_zero enforcing the base case. +]