Native runtime of bit-encryption hybrids

The certificates construct the zero prefix, encrypt the surrounding words, and copy the supplied challenge ciphertext into its final position. All supplied data and every output ciphertext are charged. No semantic correctness or width assumption is needed.

Main results

• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_encryptBitsHybrid: encrypt the actual mixed word.
• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_spliceEncryptedBit: insert an encrypted challenge between independently encrypted surrounding words.

References

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

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_encryptBitsHybrid {E : Scheme} (hencrypt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Bool) => E.encrypt p.1 p.2.1 p.2.2) {α : Type} {input : α ↪ List Bool} {n cut : α → ℕ} {pk bits : α → List Bool} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hpk : Turing.MultiTapeTM.ComputableInPolyTime pk input Turing.MultiTapeTM.encBits) (hbits : Turing.MultiTapeTM.ComputableInPolyTime bits input Turing.MultiTapeTM.encBits) (hcut : Turing.MultiTapeTM.ComputableInPolyTime cut input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) fun (a : α) => E.encryptBitsHybrid (n a) (pk a) (bits a) (cut a)

Encrypt the mixed word, preserving its length even when the unary cut exceeds it.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_spliceEncryptedBit {E : Scheme} (hencrypt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Bool) => E.encrypt p.1 p.2.1 p.2.2) {α : Type} {input : α ↪ List Bool} {n before : α → ℕ} {pk after challenge : α → List Bool} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hpk : Turing.MultiTapeTM.ComputableInPolyTime pk input Turing.MultiTapeTM.encBits) (hbefore : Turing.MultiTapeTM.ComputableInPolyTime before input Turing.MultiTapeTM.encUnary) (hafter : Turing.MultiTapeTM.ComputableInPolyTime after input Turing.MultiTapeTM.encBits) (hchallenge : Turing.MultiTapeTM.ComputableInPolyTime challenge input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) fun (a : α) => E.spliceEncryptedBit (n a) (pk a) (before a) (after a) (challenge a)

Copy the full supplied ciphertext between independently encrypted zero and original words.