Uniform native GSW circuit evaluation

The layered evaluator has one uniform polynomial clock in its full encoded input: the unary dimensions, the circuit code and every input ciphertext. Copies are cut to the ciphertext width and constants and NAND outputs have exactly that width, so every layer's encoding is bounded by its node count times the ciphertext width, even on malformed circuits, references and words. No correctness, key or noise hypothesis is used.

Main results

• Cslib.Crypto.Homomorphic.GSW.computableInPolyTime_constSerialized: noiseless constants.
• Cslib.Crypto.Homomorphic.GSW.computableInPolyTime_evaluateNode, .computableInPolyTime_evaluateLayer, .computableInPolyTime_evaluateLayers: layers.
• Cslib.Crypto.Homomorphic.GSW.computableInPolyTime_evaluateCircuit: compile and evaluate a circuit, including the selection of its output wire.

References

• C. Gentry, A. Sahai and B. Waters, Section 3.3

theorem Cslib.Crypto.Homomorphic.GSW.computableInPolyTime_constSerialized {α : Type} {input : α ↪ List Bool} {n w : α → ℕ} {μ : α → Bool} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w input Turing.MultiTapeTM.encUnary) (hμ : Turing.MultiTapeTM.ComputableInPolyTime μ input Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => constSerialized (n a) (w a) (μ a)) input Turing.MultiTapeTM.encBits

Write a noiseless constant ciphertext, charging every output bit.

theorem Cslib.Crypto.Homomorphic.GSW.computableInPolyTime_evaluateNode {α : Type} {input : α ↪ List Bool} {n w : α → ℕ} {wires : α → List (List Bool)} {node : α → Circuits.Boolean.Layered.Node} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w input Turing.MultiTapeTM.encUnary) (hwires : Turing.MultiTapeTM.ComputableInPolyTime wires input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hnode : Turing.MultiTapeTM.ComputableInPolyTime node input Circuits.Boolean.Layered.encNode) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => evaluateNode (n a) (w a) (wires a) (node a)) input Turing.MultiTapeTM.encBits

Evaluate one node on arbitrary wires, including invalid binary references.

theorem Cslib.Crypto.Homomorphic.GSW.computableInPolyTime_evaluateLayer {α : Type} {input : α ↪ List Bool} {n w : α → ℕ} {wires : α → List (List Bool)} {layer : α → List Circuits.Boolean.Layered.Node} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w input Turing.MultiTapeTM.encUnary) (hwires : Turing.MultiTapeTM.ComputableInPolyTime wires input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hlayer : Turing.MultiTapeTM.ComputableInPolyTime layer input (Turing.MultiTapeTM.encList Circuits.Boolean.Layered.encNode)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => evaluateLayer (n a) (w a) (wires a) (layer a)) input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

Evaluate every node of a computed layer, charging the complete output list.

theorem Cslib.Crypto.Homomorphic.GSW.length_evaluateNode_le (n w : ℕ) (wires : List (List Bool)) (node : Circuits.Boolean.Layered.Node) : (evaluateNode n w wires node).length ≤ ((n + 1) * w) ^ 2

Every node output has at most the square ciphertext width, on arbitrary wires.

theorem Cslib.Crypto.Homomorphic.GSW.computableInPolyTime_evaluateLayers {α : Type} {input : α ↪ List Bool} {n w : α → ℕ} {wires : α → List (List Bool)} {layers : α → List (List Circuits.Boolean.Layered.Node)} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w input Turing.MultiTapeTM.encUnary) (hwires : Turing.MultiTapeTM.ComputableInPolyTime wires input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hlayers : Turing.MultiTapeTM.ComputableInPolyTime layers input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Circuits.Boolean.Layered.encNode))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => evaluateLayers (n a) (w a) (wires a) (layers a)) input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

Evaluate all layers in order, with a uniform polynomial clock on arbitrary inputs. Each layer adds at most its node count times the encoded ciphertext width.

theorem Cslib.Crypto.Homomorphic.GSW.computableInPolyTime_evaluateCircuit {α : Type} {input : α ↪ List Bool} {n w : α → ℕ} {C : α → (k : ℕ) × Circuits.Circuit Circuits.Boolean.signature k 1} {inputs : α → List (List Bool)} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w input Turing.MultiTapeTM.encUnary) (hC : Turing.MultiTapeTM.ComputableInPolyTime C input (Circuits.Boolean.encCircuit 1)) (hinputs : Turing.MultiTapeTM.ComputableInPolyTime inputs input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => evaluateCircuit (n a) (w a) (C a) (inputs a)) input Turing.MultiTapeTM.encBits

Compile a circuit given by its unary arity and code, evaluate it on arbitrary ciphertext words and select its first designated output, in native polynomial time.