Public artifacts for fixed-key bootstrapping

The public artifact is one base public key and one vector encrypting its secret-key bits. Its encoding is the same one used by the explicit circular-security experiment. A total native decoder handles arbitrary bit strings. The private key remains the base secret word.

Main definitions

• Cslib.Crypto.Homomorphic.FixedKey.encPublicKey: the serialized public artifact.
• Cslib.Crypto.Homomorphic.FixedKey.publicKeyDecoder: its total decoder.

References

• C. Gentry, Fully homomorphic encryption using ideal lattices, Section 2.

@[reducible, inline]

abbrev Cslib.Crypto.Homomorphic.FixedKey.encPublicKey : List Bool × List (List Bool) ↪ List Bool

Use the joint circular-experiment encoding for the fixed public artifact.

def Cslib.Crypto.Homomorphic.FixedKey.publicKeyDecoder : Turing.MultiTapeTM.Decoder encPublicKey

Decode every public string with the standard total framing behavior.

@[simp]

theorem Cslib.Crypto.Homomorphic.FixedKey.publicKeyDecoder_decode_enc (pk : List Bool) (encryptedKey : List (List Bool)) : publicKeyDecoder.decode (encPublicKey (pk, encryptedKey)) = (pk, encryptedKey)