Serialized GSW random inputs

The key-input sampler returns a secret list, a list of public-matrix rows and a signed error list. The encryption coins retain the three indices (n + 1) × w × m as nested lists. All dimensions use unary encodings, residues use binary natural encodings, and errors use the signed binary integer encoding. The strict PPT certificates charge the complete framed output.

These certificates concern random-input generation. They do not certify modular matrix arithmetic, the complete GSW key-generation or encryption algorithms, or computational security.

Main definitions

• SerializedKeyInputs, SerializedCoins: finite list representations of the sampled inputs.
• sampleKeyInputsSerialized, sampleCoinsSerialized: actual list-valued sampling programs.
• serializeKeyInputs, serializeCoins, decodeKeyInputs, decodeCoins: canonical lists and total defaulted decoders for the typed random inputs.

Main results

• isPPTOn_sampleKeyInputsSerialized, isPPTOn_sampleCoinsSerialized: uniform native sampler certificates for efficiently computed dimensions.
• eval_sampleKeyInputsSerialized, eval_sampleCoinsSerialized: exact distribution bridges.
• eval_decodeKeyInputs_sampleKeyInputsSerialized, eval_decodeCoins_sampleCoinsSerialized: decoding the efficient samplers recovers the typed samplers' full joint laws.

References

• C. Gentry, A. Sahai and B. Waters, Homomorphic Encryption from Learning with Errors: Conceptually-Simpler, Asymptotically-Faster, Attribute-Based, Section 3.1
• NIST, Module-Lattice-Based Key-Encapsulation Mechanism Standard, Algorithm 8 for the exact finite noise construction.

@[reducible, inline]

abbrev Cslib.Crypto.Homomorphic.GSW.SerializedKeyInputs : Type

Secret entries, public-matrix rows and signed errors, without dependent dimensions.

@[reducible, inline]

abbrev Cslib.Crypto.Homomorphic.GSW.encSerializedKeyInputs : SerializedKeyInputs ↪ List Bool

Binary residues and signed binary errors, with all list and pair framing.

@[reducible, inline]

abbrev Cslib.Crypto.Homomorphic.GSW.SerializedCoins : Type

Encryption coins with the three indices (n + 1) × w × m kept in order.

@[reducible, inline]

abbrev Cslib.Crypto.Homomorphic.GSW.encSerializedCoins : SerializedCoins ↪ List Bool

Two framed list levels around each raw Boolean row.

noncomputable def Cslib.Crypto.Homomorphic.GSW.sampleKeyInputsSerialized (n m w η : ℕ) : ProbComp SerializedKeyInputs

Independently sample every key-input entry using binary residues and signed errors.

noncomputable def Cslib.Crypto.Homomorphic.GSW.sampleCoinsSerialized (n m w : ℕ) : ProbComp SerializedCoins

Independently sample the Boolean entries of the encryption matrix in index order.

def Cslib.Crypto.Homomorphic.GSW.serializeKeyInputs {n m w : ℕ} (inputs : KeyInputs n m w) : SerializedKeyInputs

List every residue's canonical representative and every signed error in coordinate order.

def Cslib.Crypto.Homomorphic.GSW.decodeKeyInputs (n m w : ℕ) (inputs : SerializedKeyInputs) : KeyInputs n m w

Read fixed dimensions from arbitrary lists, padding absent entries with zero and reducing natural representatives modulo 2 ^ w. Excess entries are ignored.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.decode_serializeKeyInputs {n m w : ℕ} (inputs : KeyInputs n m w) : decodeKeyInputs n m w (serializeKeyInputs inputs) = inputs

Canonical lists decode to their original typed key inputs, including empty dimensions.

def Cslib.Crypto.Homomorphic.GSW.serializeCoins {n m w : ℕ} (coins : Matrix (Fin (n + 1) × Fin w) (Fin m) Bool) : SerializedCoins

List all three encryption-coin indices without flattening or reordering them.

def Cslib.Crypto.Homomorphic.GSW.decodeCoins (n m w : ℕ) (coins : SerializedCoins) : Matrix (Fin (n + 1) × Fin w) (Fin m) Bool

Read the encryption-coin matrix from arbitrary nested lists, padding absent entries with false and ignoring excess entries.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.decode_serializeCoins {n m w : ℕ} (coins : Matrix (Fin (n + 1) × Fin w) (Fin m) Bool) : decodeCoins n m w (serializeCoins coins) = coins

Canonical coin lists decode to the original matrix, including empty dimensions.

theorem Cslib.Crypto.Homomorphic.GSW.eval_sampleKeyInputsSerialized (n m w η : ℕ) : (sampleKeyInputsSerialized n m w η).eval = PMF.map serializeKeyInputs (sampleKeyInputs n m w η).eval

The efficient key-input sampler has exactly the typed sampler's joint law, including the independence of the secret, public-matrix part and signed errors.

theorem Cslib.Crypto.Homomorphic.GSW.eval_sampleCoinsSerialized (n m w : ℕ) : (sampleCoinsSerialized n m w).eval = PMF.map serializeCoins (sampleCoins n m w).eval

The efficient coin sampler has exactly the typed binary matrix's full joint law.

theorem Cslib.Crypto.Homomorphic.GSW.eval_decodeKeyInputs_sampleKeyInputsSerialized (n m w η : ℕ) : (decodeKeyInputs n m w <$> sampleKeyInputsSerialized n m w η).eval = (sampleKeyInputs n m w η).eval

Decoding the efficient sampled lists recovers the mathematical key-input sampler.

theorem Cslib.Crypto.Homomorphic.GSW.eval_decodeCoins_sampleCoinsSerialized (n m w : ℕ) : (decodeCoins n m w <$> sampleCoinsSerialized n m w).eval = (sampleCoins n m w).eval

Decoding the efficient sampled lists recovers the mathematical encryption-coin sampler.

theorem Cslib.Crypto.Homomorphic.GSW.isPPTOn_sampleKeyInputsSerialized {α : Type} {input : α ↪ List Bool} {n m w η : α → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w input Turing.MultiTapeTM.encUnary) (hη : Turing.MultiTapeTM.ComputableTidilyInPolyTime η input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input encSerializedKeyInputs fun (a : α) => sampleKeyInputsSerialized (n a) (m a) (w a) (η a)

Uniform strict PPT generation of every serialized key input. The dimensions may depend on the caller's complete encoded input; no finite-rank output encoding is used.

theorem Cslib.Crypto.Homomorphic.GSW.isPPTOn_sampleCoinsSerialized {α : Type} {input : α ↪ List Bool} {n m w : α → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input encSerializedCoins fun (a : α) => sampleCoinsSerialized (n a) (m a) (w a)

Uniform strict PPT generation of the complete encryption coin matrix, including zero dimensions. Every row and outer list delimiter is charged by the output encoding.