Uniform native GSW decryption and NAND

The actual serialized operations have uniform native polynomial-time certificates. Dimensions and loop indices are unary; modular values and signed differences are binary. Complete input words, intermediate sums and all output bits are charged. The certificates apply to arbitrary raw words, without shape, noise, support or security assumptions.

Main results

• computableTidilyInPolyTime_decryptSerialized: the actual total raw-word decryption test.
• computableTidilyInPolyTime_nandSerialized: the complete actual NAND ciphertext computation.

References

• Gentry, Sahai and Waters, Sections 3.1 and 3.3

theorem Cslib.Crypto.Homomorphic.GSW.computableTidilyInPolyTime_decryptResidue {α : Type} {input : α ↪ List Bool} {n w : α → ℕ} {secret ciphertext : α → List Bool} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w input Turing.MultiTapeTM.encUnary) (hsecret : Turing.MultiTapeTM.ComputableTidilyInPolyTime secret input Turing.MultiTapeTM.encBits) (hciphertext : Turing.MultiTapeTM.ComputableTidilyInPolyTime ciphertext input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => decryptResidue (n a) (w a) (secret a) (ciphertext a)) input Turing.MultiTapeTM.encNat

Compute the selected phase uniformly from every pair of raw secret and ciphertext words.

theorem Cslib.Crypto.Homomorphic.GSW.computableTidilyInPolyTime_decryptSerialized {α : Type} {input : α ↪ List Bool} {n w : α → ℕ} {secret ciphertext : α → List Bool} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w input Turing.MultiTapeTM.encUnary) (hsecret : Turing.MultiTapeTM.ComputableTidilyInPolyTime secret input Turing.MultiTapeTM.encBits) (hciphertext : Turing.MultiTapeTM.ComputableTidilyInPolyTime ciphertext input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => decryptSerialized (n a) (w a) (secret a) (ciphertext a)) input Turing.MultiTapeTM.encBool

The total decoder is polynomial-time on the complete inputs, including malformed words.

theorem Cslib.Crypto.Homomorphic.GSW.computableTidilyInPolyTime_nandEntry {α : Type} {input : α ↪ List Bool} {n w i k j : α → ℕ} {left right : α → List Bool} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w input Turing.MultiTapeTM.encUnary) (hleft : Turing.MultiTapeTM.ComputableTidilyInPolyTime left input Turing.MultiTapeTM.encBits) (hright : Turing.MultiTapeTM.ComputableTidilyInPolyTime right input Turing.MultiTapeTM.encBits) (hi : Turing.MultiTapeTM.ComputableTidilyInPolyTime i input Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableTidilyInPolyTime k input Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableTidilyInPolyTime j input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => nandEntry (n a) (w a) (left a) (right a) (i a) (k a) (j a)) input Turing.MultiTapeTM.encNat

Compute one actual NAND residue, keeping the complete binary sum before signed reduction.

theorem Cslib.Crypto.Homomorphic.GSW.computableTidilyInPolyTime_nandSerialized {α : Type} {input : α ↪ List Bool} {n w : α → ℕ} {left right : α → List Bool} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w input Turing.MultiTapeTM.encUnary) (hleft : Turing.MultiTapeTM.ComputableTidilyInPolyTime left input Turing.MultiTapeTM.encBits) (hright : Turing.MultiTapeTM.ComputableTidilyInPolyTime right input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => nandSerialized (n a) (w a) (left a) (right a)) input Turing.MultiTapeTM.encBits

Compute the full square ciphertext with a single uniform native polynomial clock.