Spec: limb decomposition discussion

[erik-3milabs]

This PR introduces a section that discusses (and proves) some properties of performing operations on limb decompositions.

[github-actions]

Codex Code Review

Findings

• Medium - Potential bug: spec/limbs_and_carries.typ:70 states the decomposition is (w_0, ..., w_(2n-2), 0, 0, ...) iff c_(2n-1) = 0, but the proof sums through w_(2n-1) and line 183 later concludes (w_0, ..., w_(2n-1), 0, ...). The lemma as written is false for products that need the top limb, e.g. L=10, n=2, x=y=99 needs w_3=9 while c_3=0. Fix the lemma to include w_(2n-1) or strengthen the condition if the high limb must be zero.

• Medium - Potential bug: spec/limbs_and_carries.typ:188 has - mu (2n-i) in the combined carry bound, contradicting the part 2 bound at lines 140 and 175, which use + mu (...). As written, the “upper bound” becomes negative near i = 2n-1 even though carries are nonnegative. This should likely be + mu (2n-i).

• Low - Potential bug: spec/limbs_and_carries.typ:48 drops the outer multiplication sum and leaves i free; line 50 similarly leaves r free in the second term. The intended formula is recovered later, but the derivation is invalid as written.

No Rust/VM/security-relevant implementation changes are in this diff. I did not run a Typst build because typst/shiroa are not installed in this environment.

[erik-3milabs]

The three points from Codex's review have been addressed in the previous commit (7111791)