Exact finite randomness for GSW

One flat uniform tape realizes the complete joint law of key generation and encryption. Its length is n*w + m*n*w + 2*m*η + (n+1)*w*m: the secret, public matrix, signed errors, and binary encryption matrix consume disjoint blocks. No noise tails or rejection sampling are involved. The law includes the secret key, so it preserves more than ciphertext marginals.

These are distribution identities. Native efficiency of the serialized random-input samplers is proved separately; matrix computation and cryptographic security remain separate obligations.

Main results

• exists_uniform_seed_sampleKeyInputs: one tape supplies all independent key inputs.
• exists_uniform_seed_sampleCoins: one tape supplies all encryption coins.
• exists_uniform_seed_keyGen_encrypt: exact joint key/ciphertext law from a tape of the stated length, including zero dimensions or zero noise width.

References

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

theorem Cslib.Crypto.Homomorphic.GSW.exists_uniform_seed_sampleResidue (w : ℕ) : ∃ (evaluate : List Bool → ZMod (2 ^ w)), (sampleResidue w).eval = PMF.map evaluate (BitString.uniformList w)

A residue uses a uniform word of exactly its binary width.

theorem Cslib.Crypto.Homomorphic.GSW.exists_uniform_seed_sampleVector (count w : ℕ) : ∃ (evaluate : List Bool → Fin count → ZMod (2 ^ w)), (sampleVector count w).eval = PMF.map evaluate (BitString.uniformList (count * w))

Independent residues use disjoint width-sized blocks.

theorem Cslib.Crypto.Homomorphic.GSW.exists_uniform_seed_sampleMatrix (rows cols w : ℕ) : ∃ (evaluate : List Bool → Matrix (Fin rows) (Fin cols) (ZMod (2 ^ w))), (sampleMatrix rows cols w).eval = PMF.map evaluate (BitString.uniformList (rows * (cols * w)))

Independent rows use disjoint row-sized blocks.

theorem Cslib.Crypto.Homomorphic.GSW.exists_uniform_seed_sampleCoins (n m w : ℕ) : ∃ (evaluate : List Bool → Matrix (Fin (n + 1) × Fin w) (Fin m) Bool), (sampleCoins n m w).eval = PMF.map evaluate (BitString.uniformList ((n + 1) * (w * m)))

The complete binary coin matrix uses one bit for each entry.

theorem Cslib.Crypto.Homomorphic.GSW.exists_uniform_seed_sampleKeyInputs (n m w η : ℕ) : ∃ (evaluate : List Bool → KeyInputs n m w), (sampleKeyInputs n m w η).eval = PMF.map evaluate (BitString.uniformList (n * w + m * (n * w) + m * (2 * η)))

All key-generation inputs are independent functions of disjoint parts of one finite tape.

theorem Cslib.Crypto.Homomorphic.GSW.exists_uniform_seed_keyGen_encrypt (n m w η : ℕ) (μ : Bool) : ∃ (evaluate : List Bool → (Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w)) × (Fin n → ZMod (2 ^ w))) × Ciphertext n w), (do let keys ← keyGen n m w η let ciphertext ← encrypt keys.1 μ pure (keys, ciphertext)).eval = PMF.map evaluate (BitString.uniformList (n * w + m * n * w + 2 * m * η + (n + 1) * w * m))

A single flat tape realizes the joint key and ciphertext distribution of the actual programs. The equality keeps the secret key as well as the public key and ciphertext.