Spec: limb decomposition discussion#669
Conversation
Codex Code ReviewFindings
No Rust/VM/security-relevant implementation changes are in this diff. I did not run a Typst build because |
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
Co-authored-by: claude[bot] <209825114+claude[bot]@users.noreply.github.com> Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>
|
The three points from Codex's review have been addressed in the previous commit (7111791) |
|
|
||
| Note that $x_i = 0$ for all $i >= n$, since $L^i >= L^n = S > x$. | ||
| As a result, the sum's range can be lowered from $oo$ to $n-1$. | ||
| In practice, we often include $x_i$ with $i >= n$ in equations to simplify notation. |
There was a problem hiding this comment.
I would suggest writing the sum and first definition of the x_i with the narrow range, and if we want to simplify notation, we can suggest here that we let x_i = 0 for any other value of i >= n
| 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[ |
There was a problem hiding this comment.
There's something weird with the lemma numbering, it has a leading 0.
| :=(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 in [0, i]$. |
There was a problem hiding this comment.
Technically the [0, i] should be [0, i), I suppose. Maybe just "for all i < j"
| &overline(w)_0 | ||
| &=& alpha dot z_0 + mu dot sum_(j=0)^0 x_(0-j) dot y_j\ | ||
| &&<=& alpha (L-1) + mu (L - 1)^2 \ | ||
| &&=& (alpha - delta) L + mu (L^2 - 2L) + delta L + mu - alpha,\ |
There was a problem hiding this comment.
| &&=& (alpha - delta) L + mu (L^2 - 2L) + delta L + mu - alpha,\ | |
| &&=& (alpha - delta) L + delta L - alpha + mu (L^2 - 2L) + mu,\ |
makes the transformation a bit more explicit
| This includes $k = n-1$, which yields $c_(n+(n-1)) = c_(2n-1) <= mu - delta'$. | ||
| Moreover, $c_(2n) <= floor.l (mu - delta') dot L^(-1) floor.r = 0$ since $mu in [L]$ and thus $c_(2n + i) = 0$ for all $i >= 0$. | ||
| Applying this to @lm:wi_decomp_f, we conclude that $(w_0, w_1, ..., w_(2n-1), 0, 0, ...) in [L]^*$ is the unique limb decomposition | ||
| of $f_(alpha, mu) (x, y, z)$ when $mu = 0$ and $alpha < L$, or $mu = 1$ and $alpha <= 2$. |
There was a problem hiding this comment.
There bounds don't match the μ, α ∈ [L/2 - 1] from @lm:wi_decomp_f
|
|
||
| Now, observe that | ||
| $ | ||
| &max_(i in [2n]) min(mu (i+1) (L-1) + alpha - mu - delta, mu (2n-i-1)(L-2) + mu (2n-i) - delta')\ |
There was a problem hiding this comment.
I don't fully understand where this comes from, in particular the min.
I can see the 2n coming from n - (i - n), but somehow this assumes that the correct bound for one half is the minimum out of the two possible values, which is not a priori obvious.
e.g. for i = n - 1, we get min(μ n (L - 1) + α - μ - δ, μ n (L - 1) + μ - δ'), which would depend on the relation between μ and α, and for e.g. the case α = L/2 - 2, μ = 1 this would (wrongly) choose the second as upper bound.
Or in the degenerate case where μ = 0, we'd get min(α - 1, 0) = 0 everywhere as upper bound.
Probably the correct rephrasing is to take max(max_{i ∈ [n}(...), max_{k ∈ n}(...)) instead
2 participants
This PR introduces a section that discusses (and proves) some properties of performing operations on limb decompositions.