3
$\begingroup$

I am dealing with the bounding of compression and decompression functions in CRYSTALS-Kyber, see the lemma in this post or the original reference KYBER, section 2.2 topic "Compression and Decompression".

I have not yet found a formal proof of the assertion and have tried to construct my own proof at this point.

As for the proof itself, I must note that I would like a correction. There are one or two places in it that might be relatively far-fetched. That is why I am asking here, hoping for constructive criticism of the proof.


Lemma: $$|x'-x \text{ mod}^{\pm} \, q| \leq \left\lceil \frac{q}{2^{d+1}} \right\rfloor,$$

where $x \in \mathbb{Z}_q$ and $x' = Decompress_q(Compress_q(x,d),d)$ and the Compression and Decompression functions are defined as: $$Compress_q(x,d)= \lceil (2^d / q) \cdot x \rfloor \text{ mod}^+ \, 2^d$$ $$Decompress_q(x,d) = \lceil (q/2^d) \cdot x \rfloor$$


Proof: For the proof we use the facts that $\lceil x \rfloor = x + \epsilon$, where $-\frac{1}{2} < \epsilon \leq \frac{1}{2}$ and $x$ is a rational number, together with $a \text{ mod } b = a - b \left\lfloor \frac{a}{b} \right\rfloor$ where $a$ and $b$ are integers. \begin{align} &|x'-x \text{ mod}^{\pm} \, q| \\ &=\left| \left\lceil \frac{q}{2^d} \left( \left\lceil \frac{2^d}{q}x \text{ mod}^{+} \, 2^d \right\rfloor \right) \right\rfloor - x \text{ mod}^{\pm} \, q \right| \\ &=\left| \left\lceil \frac{q}{2^d} \left( \frac{2^d}{q}x + \epsilon_1 \text{ mod}^{+} \, 2^d \right) \right\rfloor -x \text{ mod}^{\pm} \, q \right| \\ &=\left| \left\lceil \frac{q}{2^d} \left( \frac{2^d}{q}x - 2^d \left\lfloor \frac{x}{q} \right\rfloor + \epsilon_1 \right) \right\rfloor -x \text{ mod}^{\pm} \, q\right| \\ &=\left| \left\lceil x - q \left\lfloor \frac{x}{q} \right\rfloor + \frac{q}{2^d}\epsilon_1 \right\rfloor - x \text{ mod}^{\pm} \, q \right| \\ &=\left| x - q \left\lfloor \frac{x}{q} \right\rfloor + \frac{q}{2^d}\epsilon_1 + \epsilon_2 - x \text{ mod}^{\pm} \, q \right| \\ &=\left| - q \left\lfloor \frac{x}{q} \right\rfloor + \frac{q}{2^d}\epsilon_1 + \epsilon_2 \text{ mod}^{\pm} \, q \right| \\ &=\left| \frac{q}{2^d}\epsilon_1 + \epsilon_2 \text{ mod}^{\pm} \, q \right| \\ &=\left| \frac{q}{2^d}\epsilon_1 + \epsilon_2 \right| \\ &= \left\lceil \frac{q}{2^d} \epsilon_1 \right\rfloor \\ &\leq \left\lceil \frac{q}{2^{d+1}} \right\rfloor \end{align}

For the inequality the fact that the absolute value of $\epsilon_1$ is at most $\frac{1}{2}$ was used.

$\endgroup$
1
  • 1
    $\begingroup$ Looks correct to me $\endgroup$
    – Daniel S
    Apr 26, 2023 at 7:17

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.