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 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.
There was a problem hiding this comment.
Definitely fixed. Open question from me whether we prefer a global namespace for lemmas/theorems of if we want to keep them grouped by chapter (e.g. lemma 29.1)
| :=(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"
There was a problem hiding this comment.
Nope: [0, i]: c_i is defined in terms of overline(w)_i and thus, it is maximized when all overline(w)_j are for j <= i.
Also, i<j would be swapping the terms.
There was a problem hiding this comment.
Inclusion: yeah, fair
The second part was me swapping the operands accidentally, but I suppose the question then becomes whether j ≤ i is nicer to read that j ∈ [0, i]
| 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.