# Proof on the bound of Compression and Decompression in CRYSTALS-Kyber

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.

• Looks correct to me Apr 26, 2023 at 7:17