Scalar decoding for GSW ciphertexts

For modulus 2 ^ w, a bit is represented by zero or 2 ^ (w - 1), with an integer error. The decoder selects the half-open middle half of the canonical residue interval. Thus the lower quarter boundary decodes to true and the upper quarter boundary to false. Correctness uses a strict error bound, which excludes both ties and handles negative errors by modular wraparound.

Main definitions

• Cslib.Crypto.Homomorphic.GSW.decode: the scalar bit decoder.

Main results

• Cslib.Crypto.Homomorphic.GSW.decode_eq_of_error: errors of magnitude strictly below one quarter of the modulus preserve the encoded bit.
• Cslib.Crypto.Homomorphic.GSW.decode_eq_xor_highBits: for width at least two, decoding is exclusive-or of the two highest bits of the canonical residue, on every input.

References

• C. Gentry, A. Sahai, B. Waters, Homomorphic Encryption from Learning with Errors: Conceptually-Simpler, Asymptotically-Faster, Attribute-Based, Section 3.1.

def Cslib.Crypto.Homomorphic.GSW.decode (w : ℕ) (x : ZMod (2 ^ w)) : Bool

Decode the half-open middle half of the canonical residue interval as true.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.decode_eq_true_iff (w : ℕ) (x : ZMod (2 ^ w)) : decode w x = true ↔ 2 ^ w ≤ 4 * x.val ∧ 4 * x.val < 3 * 2 ^ w

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.decode_zero (x : ZMod (2 ^ 0)) : decode 0 x = false

Width zero has only the zero residue, which decodes to false.

theorem Cslib.Crypto.Homomorphic.GSW.decode_one (x : ZMod (2 ^ 1)) : decode 1 x = x.val.testBit 0

At width one, the single bit is already the decoded message.

theorem Cslib.Crypto.Homomorphic.GSW.decode_eq_xor_highBits {w : ℕ} (hw : 2 ≤ w) (x : ZMod (2 ^ w)) : decode w x = (x.val.testBit (w - 1) ^^ x.val.testBit (w - 2))

The half-open middle interval is exactly the set where the two highest bits differ. This identity holds on every residue, including both quarter-boundary ties.

theorem Cslib.Crypto.Homomorphic.GSW.decode_eq_of_error {w : ℕ} (hw : 0 < w) (μ : Bool) (error : ℤ) (herror : 4 * error.natAbs < 2 ^ w) : decode w ↑(↑μ.toNat * 2 ^ (w - 1) + error) = μ

Decoding recovers a bit whenever its integer error has magnitude strictly below one quarter of the modulus. The strict inequality excludes the decoder's asymmetric ties.