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.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hpk : Turing.MultiTapeTM.ComputableTidilyInPolyTime pk input Turing.MultiTapeTM.encBits) (hbits : Turing.MultiTapeTM.ComputableTidilyInPolyTime bits input Turing.MultiTapeTM.encBits) (hcut : Turing.MultiTapeTM.ComputableTidilyInPolyTime 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.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hpk : Turing.MultiTapeTM.ComputableTidilyInPolyTime pk input Turing.MultiTapeTM.encBits) (hbefore : Turing.MultiTapeTM.ComputableTidilyInPolyTime before input Turing.MultiTapeTM.encUnary) (hafter : Turing.MultiTapeTM.ComputableTidilyInPolyTime after input Turing.MultiTapeTM.encBits) (hchallenge : Turing.MultiTapeTM.ComputableTidilyInPolyTime 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.