From 61f5b578ba1f5dca32239a625d2854049eac65c3 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 25 Oct 2026 13:47:57 -0400 Subject: [PATCH 1/3] feat(abstracts): formal abstract for fully homomorphic encryption from GSW (#486) Add the `gsw-fhe` formal abstract. It names the library construction, GSW at the logarithmic-depth family and Gentry's leveled and self-loop schemes over its decryption circuits, and states in elementary terms the decision-LWE and one-key circular-security assumptions, correctness, fixed widths, polynomial-size decryption circuits, native strict PPT algorithms and IND-CPA. The leveled theorem holds for every budget computable in unary polynomial time, after one decryption-circuit family is chosen. `base_scheme` identifies the named GSW key generation and encryption with the explicit laws the assumptions are stated on. Move `uniformBits`, `StrictPPT`, `Negligible`, `probability` and `Indistinguishable` from the cryptography abstract into the shared `ComplexityAbstracts.Randomized` foundation so both abstracts use them, and drop the cryptography bridge's copies. Record the abstract in the catalogue, the abstracts README and ROADMAP landmark 3. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- ROADMAP.md | 7 +- abstracts/ComplexityAbstracts.lean | 3 + .../CryptographyAbstract.lean | 59 +-- .../CryptographyBridge.lean | 28 +- .../ComplexityAbstracts/GSWFHEAbstract.lean | 499 ++++++++++++++++++ .../ComplexityAbstracts/GSWFHEBridge.lean | 419 +++++++++++++++ .../GSWSecurityBridge.lean | 6 +- abstracts/ComplexityAbstracts/Randomized.lean | 72 +++ abstracts/README.md | 9 +- abstracts/catalogue.json | 23 +- 10 files changed, 1047 insertions(+), 78 deletions(-) create mode 100644 abstracts/ComplexityAbstracts/GSWFHEAbstract.lean create mode 100644 abstracts/ComplexityAbstracts/GSWFHEBridge.lean create mode 100644 abstracts/ComplexityAbstracts/Randomized.lean diff --git a/ROADMAP.md b/ROADMAP.md index 3ac7f40ea..214f68d87 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -63,9 +63,10 @@ Priorities live in this list and in the tiers of [#897]. - **Gentry's bootstrapping, instantiated** ([#486]). GSW at its logarithmic-depth parameter family instantiates the generic theorem: leveled FHE under decision LWE with quasi-polynomial modulus for exactly that family, and FHE under the additional one-key circular-security - assumption. Open: the checked formal abstract of these endpoints, a uniform generator for the - leveled scheme's wrapper decryption circuits (uniform compactness), reuse of evaluated - ciphertexts as fresh inputs (multi-hop evaluation), and Gentry's exact concrete-security loss. + assumption. The checked formal abstract `gsw-fhe` names this construction. Open: a uniform + generator for the leveled scheme's wrapper decryption circuits (uniform compactness), reuse of + evaluated ciphertexts as fresh inputs (multi-hop evaluation), and Gentry's exact + concrete-security loss. - **Completeness of oblivious transfer.** In the ideal OT-hybrid model, every polynomial-time multiparty functionality admits a protocol secure against static malicious corruptions, with real/ideal simulation and abort, under the standard communication assumptions. diff --git a/abstracts/ComplexityAbstracts.lean b/abstracts/ComplexityAbstracts.lean index 784d928e4..63b35af18 100644 --- a/abstracts/ComplexityAbstracts.lean +++ b/abstracts/ComplexityAbstracts.lean @@ -17,12 +17,15 @@ import ComplexityAbstracts.FaginAbstract import ComplexityAbstracts.FaginBridge import ComplexityAbstracts.FormulaBoundsAbstract import ComplexityAbstracts.FormulaBoundsBridge +import ComplexityAbstracts.GSWFHEAbstract +import ComplexityAbstracts.GSWFHEBridge import ComplexityAbstracts.GSWSecurityAbstract import ComplexityAbstracts.GSWSecurityBridge import ComplexityAbstracts.ImmermanSzelepcsenyiAbstract import ComplexityAbstracts.ImmermanSzelepcsenyiBridge import ComplexityAbstracts.PCPAbstract import ComplexityAbstracts.PCPBridge +import ComplexityAbstracts.Randomized import ComplexityAbstracts.ResolutionAbstract import ComplexityAbstracts.ResolutionBridge import ComplexityAbstracts.SavitchAbstract diff --git a/abstracts/ComplexityAbstracts/CryptographyAbstract.lean b/abstracts/ComplexityAbstracts/CryptographyAbstract.lean index 80370c9ee..d692f6629 100644 --- a/abstracts/ComplexityAbstracts/CryptographyAbstract.lean +++ b/abstracts/ComplexityAbstracts/CryptographyAbstract.lean @@ -9,6 +9,7 @@ Authors: Samuel Schlesinger import ComplexityAbstracts.Check import ComplexityAbstracts.Encoding import ComplexityAbstracts.Computation +import ComplexityAbstracts.Randomized import ComplexityAbstracts.CryptographyBridge /-! # One-way functions, generators and adaptive pseudorandom functions @@ -20,7 +21,9 @@ than its seed and computationally indistinguishable from uniform bits. The Goldreich–Goldwasser–Micali construction then produces a keyed function that looks like one consistently chosen random function even when each query depends on earlier answers. Existence of a one-way function remains a hypothesis; efficiency and security use uniform -finite-control machines with strict polynomial bounds and independent fair coins. +finite-control machines with strict polynomial bounds and independent fair coins. These +conventions, `Randomized.StrictPPT`, `Randomized.Negligible` and `Randomized.Indistinguishable`, +are the shared foundations displayed in the appendix. The definitions and theorem statements below specify the claim; Lean checks their proofs through `CryptographyBridge`. The audit allows only the listed foundational program, interpretation and machine modules across the implementation boundary, without importing a security definition. @@ -40,51 +43,16 @@ as credited in `Complexity.Languages.Probabilistic.Basic`. namespace ComplexityTests.Abstracts.CryptographyAbstract -/-- Exactly `n` independent fair bits, as a word of length `n`. -/ -noncomputable def uniformBits (n : ℕ) : PMF (List Bool) := - (Cslib.Probability.PMF.uniformOfFintype (Fin n → Bool)).map List.ofFn - -/-- A uniformly strict polynomial-time probability law: one deterministic evaluator, supplied -with polynomially many independent fair bits, realizes every input's law exactly. Its time -includes reading the coin tape and writing the encoded output. Both evaluator and polynomial -are fixed before the input. This also bounds every execution, rather than its expectation. -/ -def StrictPPT {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) - (law : α → PMF β) : Prop := - ∃ (c d : ℕ) (evaluate : α → List Bool → β), - Computation.PolyTime (fun p : α × List Bool => evaluate p.1 p.2) - (Encoding.encPair a Encoding.encBits) b ∧ - ∀ x, law x = (uniformBits (c * ((a x).length + 1) ^ d)).map (evaluate x) - -/-- A nonnegative error is negligible if multiplication by every fixed power of the security -parameter still tends to zero. The threshold and decay bound may depend on the whole adversary. -/ -def Negligible (ε : ℕ → NNReal) : Prop := - ∀ k : ℕ, Filter.Tendsto (fun n : ℕ => (n : NNReal) ^ k * ε n) - Filter.atTop (nhds 0) - -/-- Probability that a Boolean experiment returns true. -/ -noncomputable def probability (p : PMF Bool) : NNReal := (p true).toNNReal - -/-- Every one uniform strict PPT test has negligible distinguishing advantage. -The test receives the unary seed length and a sample. `bind` samples the word and then runs -the test with independent coins; `nndist` is the absolute difference of success probabilities. -/ -def Indistinguishable (X Y : ℕ → PMF (List Bool)) : Prop := - ∀ test : ℕ → List Bool → PMF Bool, - StrictPPT (Encoding.encPair Encoding.encUnary Encoding.encBits) Encoding.encBool - (fun p => test p.1 p.2) → - Negligible (fun n => nndist - (probability (do let sample ← X n; test n sample)) - (probability (do let sample ← Y n; test n sample))) - /-- A polynomial-time function is one-way if every strict PPT inverter, given unary `n` and `f(x)` for a uniform `n`-bit `x`, finds any preimage only with negligible probability. The candidate's length is unrestricted, and recovering the sampled `x` is unnecessary. -/ def OneWay (f : List Bool → List Bool) : Prop := Computation.PolyTime f Encoding.encBits Encoding.encBits ∧ ∀ inverter : ℕ → List Bool → PMF (List Bool), - StrictPPT (Encoding.encPair Encoding.encUnary Encoding.encBits) Encoding.encBits + Randomized.StrictPPT (Encoding.encPair Encoding.encUnary Encoding.encBits) Encoding.encBits (fun p => inverter p.1 p.2) → - Negligible (fun n => probability (do - let x ← uniformBits n + Randomized.Negligible (fun n => Randomized.probability (do + let x ← Randomized.uniformBits n (inverter n (f x)).map fun candidate => f candidate == f x)) /-- A deterministic polynomial-time generator has exact seed-dependent output length, @@ -94,7 +62,8 @@ seed length. The function need not be injective. -/ def PseudorandomGenerator (g : List Bool → List Bool) (length : ℕ → ℕ) : Prop := Computation.PolyTime g Encoding.encBits Encoding.encBits ∧ (∀ seed, (g seed).length = length seed.length) ∧ (∀ n, n < length n) ∧ - Indistinguishable (fun n => (uniformBits n).map g) (fun n => uniformBits (length n)) + Randomized.Indistinguishable (fun n => (Randomized.uniformBits n).map g) + (fun n => Randomized.uniformBits (length n)) /-- **Håstad–Impagliazzo–Levin–Luby:** any uniform one-way function yields a deterministic uniform polynomial-time generator stretching every `n`-bit seed to `n+1` bits. The proof follows @@ -169,7 +138,7 @@ with that key's function. Wrong-length queries return the empty word. The advers unary `n` and an empty auxiliary input. -/ noncomputable def realPRF (family : List Bool → List Bool → List Bool) (adversary : ℕ → List Bool → OracleProgram Bool) (n : ℕ) : PMF Bool := do - let key ← uniformBits n + let key ← Randomized.uniformBits n evaluateOracle (adversary n []) (fun query => if query.length = n then family key query else []) @@ -190,8 +159,8 @@ def PseudorandomFunction (family : List Bool → List Bool → List Bool) : Prop (Encoding.encPair Encoding.encBits Encoding.encBits) Encoding.encBits ∧ (∀ key query, query.length = key.length → (family key query).length = key.length) ∧ ∀ adversary : ℕ → List Bool → OracleProgram Bool, OraclePPT adversary → - Negligible (fun n => nndist (probability (realPRF family adversary n)) - (probability (idealPRF adversary n))) + Randomized.Negligible (fun n => nndist (Randomized.probability (realPRF family adversary n)) + (Randomized.probability (idealPRF adversary n))) /-- **One-way functions imply adaptive pseudorandom functions:** HILL, polynomial stretching and the Goldreich–Goldwasser–Micali tree construction give an efficient family satisfying the @@ -217,11 +186,11 @@ abbrev OracleResponse : Sum ℕ (Unit × List Bool) → Type := Cslib.probOracleSpec (fun _ : Unit × List Bool => List Bool) /-- -info: abstract audit passed for `ComplexityTests.Abstracts.CryptographyAbstract`: 21 root declarations, 254 dependencies checked +info: abstract audit passed for `ComplexityTests.Abstracts.CryptographyAbstract`: 15 root declarations, 254 dependencies checked -/ #guard_msgs (whitespace := lax) in #check_abstract ComplexityTests.Abstracts.CryptographyAbstract allowing [ - ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation, + ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation, ComplexityAbstracts.Randomized, Complexity.Languages.Probabilistic.Basic, Complexity.Languages.Probabilistic.Oracle, Complexity.Languages.Probabilistic.Sum, diff --git a/abstracts/ComplexityAbstracts/CryptographyBridge.lean b/abstracts/ComplexityAbstracts/CryptographyBridge.lean index bca0b76ed..4cce6f6e7 100644 --- a/abstracts/ComplexityAbstracts/CryptographyBridge.lean +++ b/abstracts/ComplexityAbstracts/CryptographyBridge.lean @@ -7,6 +7,7 @@ Authors: Samuel Schlesinger -- upstream: local-only (formal abstract library) import ComplexityAbstracts.CookLevinBridge +import ComplexityAbstracts.Randomized import Complexity.Crypto.Computational.OneWayToPRG import Complexity.Crypto.Computational.PRGToOneWay import Complexity.Crypto.Computational.GoldreichLevin.HardCore @@ -26,6 +27,7 @@ semantic interface with the library's strict fair-coin Turing-machine certificat namespace ComplexityTests.Abstracts.CryptographyBridge open Cslib Cslib.Probability Turing.MultiTapeTM +open ComplexityTests.Abstracts.Randomized open scoped NNReal def frame (w : List Bool) : List Bool := w.flatMap (fun b => [true, b]) ++ [false] @@ -54,15 +56,6 @@ theorem polyTime_iff {α β : Type} {f : α → β} {a : α ↪ List Bool} {b : PolyTime f a b ↔ ComputableTidilyInPolyTime f a b := Turing.MultiTapeTM.computableTidilyInPolyTime_iff_exists_computableInTimeAndSpaceOfLength.symm -noncomputable def uniformBits (n : ℕ) : PMF (List Bool) := - (Cslib.Probability.PMF.uniformOfFintype (Fin n → Bool)).map List.ofFn - -def StrictPPT {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) - (law : α → PMF β) : Prop := - ∃ (c d : ℕ) (evaluate : α → List Bool → β), - PolyTime (fun p : α × List Bool => evaluate p.1 p.2) (pairEncoding a bitsEncoding) b ∧ - ∀ x, law x = (uniformBits (c * ((a x).length + 1) ^ d)).map (evaluate x) - theorem strictPPT_iff {α β : Type} {a : α ↪ List Bool} {b : β ↪ List Bool} {law : α → PMF β} : StrictPPT a b law ↔ ∃ program : α → ProbComp β, @@ -85,24 +78,11 @@ theorem strictPPT_iff {α β : Type} {a : α ↪ List Bool} {b : β ↪ List Boo exact ⟨c, d, evaluate, polyTime_iff.mpr hevaluate, fun x => (hlaw x).symm.trans (heq x)⟩ -def Negligible (ε : ℕ → ℝ≥0) : Prop := - ∀ k : ℕ, Filter.Tendsto (fun n : ℕ => (n : ℝ≥0) ^ k * ε n) - Filter.atTop (nhds 0) - -noncomputable def probability (p : PMF Bool) : ℝ≥0 := (p true).toNNReal - -def Indistinguishable (X Y : ℕ → PMF (List Bool)) : Prop := - ∀ test : ℕ → List Bool → PMF Bool, - StrictPPT (pairEncoding unaryEncoding bitsEncoding) boolEncoding - (fun p => test p.1 p.2) → - Negligible (fun n => nndist (probability ((X n).bind (test n))) - (probability ((Y n).bind (test n)))) - theorem indistinguishable_iff {X Y : ℕ → PMF (List Bool)} : Indistinguishable X Y ↔ Crypto.ComputationallyIndistinguishable X Y := by rw [Crypto.computationallyIndistinguishable_iff_tests] have hadmissible (test : ℕ → List Bool → PMF Bool) : - StrictPPT (pairEncoding unaryEncoding bitsEncoding) boolEncoding + StrictPPT (Encoding.encPair Encoding.encUnary Encoding.encBits) Encoding.encBool (fun p => test p.1 p.2) ↔ Crypto.IsPPTTest test := by rw [strictPPT_iff] constructor @@ -111,7 +91,7 @@ theorem indistinguishable_iff {X Y : ℕ → PMF (List Bool)} : · rintro ⟨program, hp, heq⟩ exact ⟨fun p => program p.1 p.2, hp, fun p => heq p.1 p.2⟩ simp only [Indistinguishable, hadmissible, Crypto.Game.Indistinguishable, - Crypto.Game.advantage, Crypto.Game.succProbability, probability, + Crypto.Game.advantage, Crypto.Game.succProbability, probability, PMF.monad_bind_eq_bind, Negligible, Crypto.Negligible, Asymptotics.SuperpolynomialDecay] def OneWay (f : List Bool → List Bool) : Prop := diff --git a/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean b/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean new file mode 100644 index 000000000..968c7aab0 --- /dev/null +++ b/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean @@ -0,0 +1,499 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +-- upstream: local-only (formal abstract library) + +import ComplexityAbstracts.Check +import ComplexityAbstracts.Encoding +import ComplexityAbstracts.Computation +import ComplexityAbstracts.Randomized +import ComplexityAbstracts.GSWFHEBridge + +/-! # Fully homomorphic encryption from GSW and decision LWE + +Gentry's bootstrapping turns an encryption scheme that can homomorphically evaluate its own +decryption circuit, also when two copies are joined by a NAND gate, into a scheme that evaluates +circuits of any prescribed depth. Applied to the Gentry–Sahai–Waters (GSW) scheme at an explicit +parameter family, it gives leveled fully homomorphic encryption assuming only decision LWE for +that family. Publishing an encryption of the secret key under its own public key gives fully +homomorphic encryption, under a second, separately stated assumption: this self-encryption is +indistinguishable from an encryption of zeros. + +The construction is named, not restated. The theorems concern the library's GSW scheme +`Cslib.Crypto.Homomorphic.GSW.DepthParameters.scheme`, its raw-input decryption circuits +`DepthParameters.decryptionCircuits`, Gentry's acyclic leveled construction +`Cslib.Crypto.Homomorphic.Leveled.scheme` and the self-loop construction +`Cslib.Crypto.Homomorphic.FixedKey.scheme`. A reader inspects these algorithms in the library: +GSW key generation, encryption, decryption and layered NAND evaluation; the logarithmic-depth +decryption circuit; the key chain, refreshing and serialization of the bootstrapped schemes; and +the compilation of De Morgan circuits into NAND layers. `#check_abstract` permits exactly the +modules these definitions need, and the shared foundations. + +Both assumptions, and every property claimed of the construction, are stated below. Besides +upstream mathematics, plain machines and the shared foundations, the statements use only three +library notions, each explained where it first appears: the record `Cslib.Crypto.Homomorphic.Scheme` +of four algorithms, the output distribution `Cslib.ProbComp.eval` of a randomized program, and +the binary circuit code `Cslib.Circuits.Boolean.encCircuit`. `base_scheme` identifies the named +GSW key generation and encryption with the explicit laws on which the assumptions are stated. + +The claims are perfect correctness on supported fresh encryptions, fixed key and ciphertext +widths, polynomial-size decryption circuits, uniform native strict polynomial-time algorithms and +asymptotic IND-CPA security against uniform classical adversaries. They do not include lattice +hardness or a worst-case reduction, circuit privacy, evaluation of already evaluated ciphertexts, +a uniform generator for the leveled decryption circuits, or the concrete loss of Gentry's +Theorem 4. + +## References + +* [C. Gentry, *Fully homomorphic encryption using ideal lattices*][Gentry2009]: Section 1.1, + pp. 169–170, with Definitions 1–3; Section 2, p. 171, with Definitions 4–5 and Theorems 3–4; + and the self-loop construction at the end of Section 2, p. 172. +* [C. Gentry, A. Sahai and B. Waters, *Homomorphic Encryption from Learning with Errors: + Conceptually-Simpler, Asymptotically-Faster, Attribute-Based*][GentrySahaiWaters2013], + Sections 3.1–3.4. +-/ + +namespace ComplexityTests.Abstracts.GSWFHEAbstract + +/-! ## The parameter family + +The security parameter is supplied in unary. With `t = 1 + ⌈log₂(security + 2)⌉`, every residue +has `w = 16384 t²` binary digits, so the modulus `2 ^ w` is quasi-polynomial. The secret +dimension and the noise width are `n = security + 1`. A ciphertext is an `N × N` bit matrix with +`N = (n + 1) w`, and the public matrix has `m = N + 2 · security` rows. +-/ + +/-- The logarithmic size `t = 1 + ⌈log₂(security + 2)⌉`; `Nat.clog 2` is the ceiling logarithm. -/ +def logSize (security : ℕ) : ℕ := 1 + Nat.clog 2 (security + 2) + +/-- Binary digits per residue, `w = 16384 t²`; the modulus is `2 ^ width security`. -/ +def width (security : ℕ) : ℕ := 16384 * logSize security ^ 2 + +/-- The LWE secret dimension `n`. The centered-binomial noise has the same width. -/ +def dimension (security : ℕ) : ℕ := security + 1 + +/-- Ciphertext rows and columns, `N = (n + 1) w`. -/ +def rows (security : ℕ) : ℕ := (dimension security + 1) * width security + +/-- Rows of the public matrix, `m = N + 2 · security`. -/ +def samples (security : ℕ) : ℕ := rows security + 2 * security + +/-- Bits of a GSW secret key: `n` residues of `w` bits each. -/ +def secretWidth (security : ℕ) : ℕ := dimension security * width security + +/-- Bits of a GSW ciphertext: an `N × N` bit matrix. -/ +def ciphertextWidth (security : ℕ) : ℕ := rows security * rows security + +/-! ## Representation details + +Residues modulo `2 ^ w` are written with exactly `w` bits, least significant first. A public key +is the matrix `[B t + e | B]` in row-major order, its noisy column first; a secret key lists the +residues of `t`; a ciphertext lists every bit of `μ G + R A`, its rows indexed by `(i, k)` and its +columns by `(j, l)`. These words are the actual inputs and outputs of the native algorithms. +-/ + +/-- Write exactly `w` digits, least significant first, including leading zeros. -/ +def lowBits (w value : ℕ) : List Bool := (List.range w).map value.testBit + +/-- The leading entry of `[B t + e | B]`, reduced by signed Euclidean remainder. -/ +def rowHead (n w : ℕ) (inputs : List ℕ × (List (List ℕ) × List ℤ)) (i : ℕ) : ℕ := + (((((List.range n).map fun j => + (inputs.2.1.getD i []).getD j 0 * inputs.1.getD j 0).sum : ℕ) + + inputs.2.2.getD i 0 : ℤ) % (2 ^ w : ℤ)).toNat + +/-- Row-major serialization of the public matrix, with its noisy column first. -/ +def publicWord (n m w : ℕ) (inputs : List ℕ × (List (List ℕ) × List ℤ)) : List Bool := + (List.range m).flatMap fun i => + lowBits w (rowHead n w inputs i) ++ + (List.range n).flatMap fun j => lowBits w ((inputs.2.1.getD i []).getD j 0 % 2 ^ w) + +/-- Serialize the secret residues; these bits are not given to the adversary. -/ +def secretWord (n w : ℕ) (secret : List ℕ) : List Bool := + (List.range n).flatMap fun j => lowBits w (secret.getD j 0 % 2 ^ w) + +/-- Read a fixed-width matrix entry. Missing bits are zero, and excess bits are ignored. -/ +def matrixEntry (cols w : ℕ) (word : List Bool) (i j : ℕ) : ℕ := + ((word.drop ((i * cols + j) * w) ++ List.replicate w false).take w).foldr Nat.bit 0 + +/-- An entry of `message * G + R * A`, before binary decomposition. -/ +def ciphertextEntry (n m w : ℕ) (publicKey : List Bool) (message : Bool) + (coins : List (List (List Bool))) (i k j : ℕ) : ℕ := + ((if i = j then message.toNat * 2 ^ k else 0) + + ((List.range m).map fun r => + if ((coins.getD i []).getD k []).getD r false then + matrixEntry (n + 1) w publicKey r j else 0).sum) % 2 ^ w + +/-- Write every bit of the square ciphertext. Its row order is `(i, k)` and column order +`(j, l)`; this is the bit decomposition of `message * G + R * A`, which equals GSW's +`Flatten(μ I_N + BitDecomp(R A))`. -/ +def ciphertextWord (n m w : ℕ) (publicKey : List Bool) (message : Bool) + (coins : List (List (List Bool))) : List Bool := + (List.range (n + 1)).flatMap fun i => + (List.range w).flatMap fun k => + (List.range (n + 1)).flatMap fun j => + lowBits w (ciphertextEntry n m w publicKey message coins i k j) + +/-! ## GSW key generation and encryption + +Key generation samples a uniform secret `t`, a uniform matrix `B` and independent signed errors +`e`, and publishes `[B t + e | B]`. Encryption of a bit `μ` samples a uniform 0/1 matrix `R` and +outputs the bits of `μ G + R A` [GentrySahaiWaters2013, Sections 3.1–3.2]. +-/ + +/-- Collect independent draws in their original order; the empty list requires no draw. -/ +noncomputable def independentList {α : Type} (count : ℕ) (law : PMF α) : PMF (List α) := + (List.replicate count ()).mapM (fun _ => law) + +/-- A canonical residue representative chosen uniformly from `0, …, 2 ^ w - 1`. -/ +noncomputable def residueLaw (w : ℕ) : PMF ℕ := + (Cslib.Probability.PMF.uniformOfFintype (Fin (2 ^ w))).map Fin.val + +/-- The signed noise is the difference of the counts of ones in two independent uniform words +of length `noiseWidth`. Its support is `[-noiseWidth, noiseWidth]`; this is a centered binomial +law, not a discrete Gaussian. -/ +noncomputable def errorLaw (noiseWidth : ℕ) : PMF ℤ := do + let positive ← Randomized.uniformBits noiseWidth + let negative ← Randomized.uniformBits noiseWidth + return (positive.count true : ℤ) - negative.count true + +/-- Generate the public and secret key words. The secret, the matrix rows and the signed errors +are sampled independently, with dimension and noise width both `security + 1`. -/ +noncomputable def keyGeneration (security : ℕ) : PMF (List Bool × List Bool) := do + let secret ← independentList (dimension security) (residueLaw (width security)) + let matrix ← independentList (samples security) + (independentList (dimension security) (residueLaw (width security))) + let errors ← independentList (samples security) (errorLaw (dimension security)) + return (publicWord (dimension security) (samples security) (width security) + (secret, (matrix, errors)), secretWord (dimension security) (width security) secret) + +/-- Encrypt a bit using only the public word and independent fair matrix coins. This law is +defined on every public word, including malformed ones. -/ +noncomputable def encryption (security : ℕ) (publicKey : List Bool) (message : Bool) : + PMF (List Bool) := do + let coins ← independentList (dimension security + 1) + (independentList (width security) (independentList (samples security) + (Cslib.Probability.PMF.uniformOfFintype Bool))) + return ciphertextWord (dimension security) (samples security) (width security) + publicKey message coins + +/-! ## The two assumptions + +Both are computational indistinguishability against uniform classical strict PPT tests, as +defined in the shared foundations. Neither is proved; each theorem below lists the assumptions +it uses. +-/ + +/-- A uniformly random `m × k` matrix of residues modulo `2 ^ w`, written row by row with `w` +bits per entry, least significant first. -/ +noncomputable def uniformMatrixWord (m k w : ℕ) : PMF (List Bool) := + (Cslib.Probability.PMF.uniformOfFintype (Fin m → Fin k → ZMod (2 ^ w))).map + (fun A => (List.ofFn fun i => (List.ofFn fun j => lowBits w (A i j).val).flatten).flatten) + +/-- The decision-LWE comparison: a uniform matrix of the same shape and modulus as the public +key, encoded in the same order. -/ +noncomputable def uniformPublic (security : ℕ) : PMF (List Bool) := + uniformMatrixWord (samples security) (dimension security + 1) (width security) + +/-- **Decision LWE for exactly this family.** The public matrix `[B t + e | B]`, with uniform +secret, uniform matrix and the independent centered-binomial errors above, is indistinguishable +from a uniform matrix. Neither the secret nor the errors are exposed. No lattice reduction or +hardness theorem is asserted. -/ +def DecisionLWE : Prop := + Randomized.Indistinguishable (fun security => (keyGeneration security).map Prod.fst) + uniformPublic + +/-- Sample one key pair, then encrypt either every secret-key bit or equally many zero bits under +that public key. The public key and the complete vector of encryptions are published together, +encoded as a pair of the public word and the framed list of ciphertexts. -/ +noncomputable def selfEncryption (real : Bool) (security : ℕ) : PMF (List Bool) := do + let keys ← keyGeneration security + let encrypted ← (if real then keys.2 else List.replicate keys.2.length false).mapM + (encryption security keys.1) + return Encoding.encPair Encoding.encBits (Encoding.encList Encoding.encBits) (keys.1, encrypted) + +/-- **One-key circular security of GSW at this family.** Encryptions of the secret key under its +own public key are indistinguishable from encryptions of zeros. This is the one-key, bitwise +case of the key-dependent-message security that Gentry's self-loop construction assumes +[Gentry2009, Section 2]. It is a separate assumption: it is not derived from decision LWE or +from IND-CPA. -/ +def CircularSecure : Prop := + Randomized.Indistinguishable (selfEncryption true) (selfEncryption false) + +/-! ## The named construction + +A `Cslib.Crypto.Homomorphic.Scheme` is a record of four algorithms on bit strings, each taking +the security parameter: `keyGen` samples a public and a secret key; `encrypt` encrypts one bit +under a public key; `decrypt` is deterministic; and `evaluate` receives a public key, a +single-output De Morgan circuit with its number of inputs, and a list of ciphertexts. A fifth +field, `permitted`, is not used by any claim below. Randomized algorithms are terminating +programs whose only randomness is uniform choice from finite ranges (`Cslib.ProbComp`), and +`Cslib.ProbComp.eval` is their output distribution. +-/ + +/-- GSW at this family. Evaluation compiles the circuit into NAND layers, evaluates them with +GSW's homomorphic NAND, and ignores the public key. -/ +noncomputable def baseScheme : Cslib.Crypto.Homomorphic.Scheme := + Cslib.Crypto.Homomorphic.GSW.DepthParameters.scheme + +/-- The named GSW algorithms have exactly the key-generation and encryption laws above, so the +two assumptions concern the actual base scheme. -/ +theorem base_scheme (security : ℕ) : + Cslib.ProbComp.eval (baseScheme.keyGen security) = keyGeneration security ∧ + ∀ publicKey message, Cslib.ProbComp.eval (baseScheme.encrypt security publicKey message) = + encryption security publicKey message := + GSWFHEBridge.base_scheme security + +/-- GSW's raw-input decryption circuit, secret-key bits first. It is the circuit that the +bootstrapped schemes evaluate homomorphically. -/ +def decryptionCircuit (security : ℕ) : + Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature + (secretWidth security + ciphertextWidth security) 1 := + Cslib.Crypto.Homomorphic.GSW.DepthParameters.decryptionCircuits.circuit security + +/-- **Gentry's acyclic leveled scheme** [Gentry2009, Section 2]. For a depth budget `budget`, +key generation samples `2 · budget + 1` independent GSW keys and encrypts each secret key under +the next public key. Evaluation compiles the circuit into NAND layers, padded to exactly +`2 · budget` layers, and each layer moves every wire to the next key. A NAND gate encrypts the +bits of its two input ciphertexts under the next key and homomorphically evaluates two copies of +the decryption circuit joined by NAND, using the encrypted previous secret key; a carried wire +uses the decryption circuit alone; a constant is a fresh encryption. A one-bit tag tells +decryption whether to use the first or the last secret key. -/ +noncomputable def leveledScheme (budget : ℕ → ℕ) : Cslib.Crypto.Homomorphic.Scheme := + Cslib.Crypto.Homomorphic.Leveled.scheme + Cslib.Crypto.Homomorphic.GSW.DepthParameters.decryptionCircuits budget + +/-- **Gentry's self-loop scheme** [Gentry2009, Section 2]. The public key is one GSW public key +together with encryptions of its own secret-key bits. Evaluation is layered as in the leveled +scheme, with as many layers as the circuit needs, but every layer uses that same key. The secret +key and the ciphertexts are those of GSW. -/ +noncomputable def fixedKeyScheme : Cslib.Crypto.Homomorphic.Scheme := + Cslib.Crypto.Homomorphic.FixedKey.scheme + Cslib.Crypto.Homomorphic.GSW.DepthParameters.decryptionCircuits + +/-! ## Homomorphic encryption + +Circuits are single-output De Morgan circuits (constants, negation, binary conjunction and +disjunction) given as a pair of their number of inputs `C.1` and the circuit `C.2`. The upstream +`depth` is the largest number of gates on a path to the output, where inputs have depth zero and +every gate, including a constant, adds one; `size` is the number of gates. +-/ + +/-- **Correctness for a class of circuits** [Gentry2009, Section 1.1]. Under every supported key +pair, every supported fresh encryption decrypts to its bit; and every allowed circuit, evaluated +on supported fresh encryptions of its input bits, yields only ciphertexts that decrypt to the +circuit's output. Inputs may repeat a ciphertext or share randomness; `List.Forall₂` pairs each +bit with its ciphertext and fixes the number of ciphertexts. -/ +def Homomorphic (S : Cslib.Crypto.Homomorphic.Scheme) + (allowed : ℕ → (Σ k, Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature k 1) → Prop) : + Prop := + ∀ security keys, keys ∈ (Cslib.ProbComp.eval (S.keyGen security)).support → + (∀ bit ciphertext, + ciphertext ∈ (Cslib.ProbComp.eval (S.encrypt security keys.1 bit)).support → + S.decrypt security keys.2 ciphertext = bit) ∧ + ∀ C bits inputs, allowed security C → bits.length = C.1 → + List.Forall₂ (fun bit ciphertext => + ciphertext ∈ (Cslib.ProbComp.eval (S.encrypt security keys.1 bit)).support) bits inputs → + ∀ ciphertext ∈ (Cslib.ProbComp.eval (S.evaluate security keys.1 C inputs)).support, + S.decrypt security keys.2 ciphertext = + C.2.eval Cslib.Circuits.Boolean.interpretation (fun i => bits.getD i false) 0 + +/-- **Compactness by fixed widths** [Gentry2009, Section 1.1]. Supported secret keys have +`keyBits` bits, and supported fresh ciphertexts and every ciphertext evaluated from them by an +allowed circuit have `cipherBits` bits, independently of the circuit's size and depth. -/ +def FixedWidths (S : Cslib.Crypto.Homomorphic.Scheme) + (allowed : ℕ → (Σ k, Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature k 1) → Prop) + (keyBits cipherBits : ℕ → ℕ) : Prop := + ∀ security keys, keys ∈ (Cslib.ProbComp.eval (S.keyGen security)).support → + keys.2.length = keyBits security ∧ + (∀ bit ciphertext, + ciphertext ∈ (Cslib.ProbComp.eval (S.encrypt security keys.1 bit)).support → + ciphertext.length = cipherBits security) ∧ + ∀ C bits inputs, allowed security C → bits.length = C.1 → + List.Forall₂ (fun bit ciphertext => + ciphertext ∈ (Cslib.ProbComp.eval (S.encrypt security keys.1 bit)).support) bits inputs → + ∀ ciphertext ∈ (Cslib.ProbComp.eval (S.evaluate security keys.1 C inputs)).support, + ciphertext.length = cipherBits security + +/-- **Decryption by one circuit per parameter** [Gentry2009, Definition 1]. On every secret key +of `keyBits` bits and every ciphertext of `cipherBits` bits, the circuit computes decryption +from the key bits followed by the ciphertext bits. -/ +def DecryptsWith (S : Cslib.Crypto.Homomorphic.Scheme) (keyBits cipherBits : ℕ → ℕ) + (circuit : ∀ security, Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature + (keyBits security + cipherBits security) 1) : Prop := + ∀ security (secret ciphertext : List Bool), secret.length = keyBits security → + ciphertext.length = cipherBits security → + (circuit security).eval Cslib.Circuits.Boolean.interpretation + (fun i => (secret ++ ciphertext).getD i false) 0 = S.decrypt security secret ciphertext + +/-- **Native efficiency.** Key generation, encryption and evaluation are uniform strict PPT, and +decryption is deterministic polynomial time; each is one machine for all parameters and runs on +all raw inputs, including malformed keys and ciphertexts. Time is measured in the length of the +encoded input: the unary parameter, the words and, for evaluation, the circuit in the binary +code `Cslib.Circuits.Boolean.encCircuit 1` (its input count in unary, then its gates and output +wires with wire numbers in binary) followed by the framed list of input ciphertexts. -/ +def Native (S : Cslib.Crypto.Homomorphic.Scheme) : Prop := + Randomized.StrictPPT Encoding.encUnary (Encoding.encPair Encoding.encBits Encoding.encBits) + (fun security => Cslib.ProbComp.eval (S.keyGen security)) ∧ + Randomized.StrictPPT + (Encoding.encPair Encoding.encUnary (Encoding.encPair Encoding.encBits Encoding.encBool)) + Encoding.encBits (fun p => Cslib.ProbComp.eval (S.encrypt p.1 p.2.1 p.2.2)) ∧ + Computation.PolyTime (fun p : ℕ × List Bool × List Bool => S.decrypt p.1 p.2.1 p.2.2) + (Encoding.encPair Encoding.encUnary (Encoding.encPair Encoding.encBits Encoding.encBits)) + Encoding.encBool ∧ + Randomized.StrictPPT + (Encoding.encPair Encoding.encUnary (Encoding.encPair Encoding.encBits + (Encoding.encPair (Cslib.Circuits.Boolean.encCircuit 1) + (Encoding.encList Encoding.encBits)))) + Encoding.encBits (fun p => Cslib.ProbComp.eval (S.evaluate p.1 p.2.1 p.2.2.1 p.2.2.2)) + +/-- Generate keys, let the adversary choose two messages after seeing the public key, encrypt +the selected message, and pass the saved word and the challenge ciphertext to the guessing +stage. The secret key is never given to the adversary. -/ +noncomputable def chosenMessageGame (S : Cslib.Crypto.Homomorphic.Scheme) + (choose : ℕ → List Bool → PMF ((Bool × Bool) × List Bool)) + (guess : ℕ → List Bool → List Bool → PMF Bool) (bit : Bool) (security : ℕ) : + PMF Bool := do + let keys ← Cslib.ProbComp.eval (S.keyGen security) + let choice ← choose security keys.1 + let ciphertext ← Cslib.ProbComp.eval + (S.encrypt security keys.1 (if bit then choice.1.2 else choice.1.1)) + guess security choice.2 ciphertext + +/-- **IND-CPA**: every two-stage uniform strict PPT adversary has negligible advantage in +telling apart the two challenge bits. Both stages are charged for the unary parameter and their +complete inputs; the saved word may contain the public key. The adversary is fixed before the +parameter, without nonuniform advice. -/ +def ChosenMessageSecure (S : Cslib.Crypto.Homomorphic.Scheme) : Prop := + ∀ (choose : ℕ → List Bool → PMF ((Bool × Bool) × List Bool)) + (guess : ℕ → List Bool → List Bool → PMF Bool), + Randomized.StrictPPT (Encoding.encPair Encoding.encUnary Encoding.encBits) + (Encoding.encPair (Encoding.encPair Encoding.encBool Encoding.encBool) Encoding.encBits) + (fun p => choose p.1 p.2) → + Randomized.StrictPPT + (Encoding.encPair Encoding.encUnary (Encoding.encPair Encoding.encBits Encoding.encBits)) + Encoding.encBool (fun p => guess p.1 p.2.1 p.2.2) → + Randomized.Negligible (fun security => + nndist (Randomized.probability (chosenMessageGame S choose guess false security)) + (Randomized.probability (chosenMessageGame S choose guess true security))) + +/-! ## Main results + +Gentry's Definition 3 asks for one decryption circuit shared by all depths, correctness for +every circuit up to the depth, and algorithms polynomial in the parameter and the depth +[Gentry2009, Definition 3]. In `leveled`, one polynomial-size circuit family is chosen first. +Then for every depth budget computable in unary polynomial time, the leveled scheme with that +budget decrypts with this circuit family, is correct for every circuit of depth at most the +budget, has fixed polynomial widths, native algorithms and IND-CPA security. Any polynomially +bounded depth `d(security) ≤ c (security + 1) ^ e` is covered by the budget +`c (security + 1) ^ e`. The runtime polynomial may depend on the budget function. +-/ + +/-- **Leveled fully homomorphic encryption from decision LWE** [Gentry2009, Theorem 3]. Only the +decision-LWE assumption for this family is used; there is no circular-security assumption. +IND-CPA is the asymptotic consequence of [Gentry2009, Theorem 4], without its exact loss. -/ +theorem leveled (hLWE : DecisionLWE) : + ∃ circuit : ∀ security, Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature + ((3 * secretWidth security + 1) + (ciphertextWidth security + 1)) 1, + Cslib.PolynomiallyBounded (fun security => (circuit security).size) ∧ + Cslib.PolynomiallyBounded (fun security => 3 * secretWidth security + 1) ∧ + Cslib.PolynomiallyBounded (fun security => ciphertextWidth security + 1) ∧ + ∀ budget : ℕ → ℕ, Computation.PolyTime budget Encoding.encUnary Encoding.encUnary → + DecryptsWith (leveledScheme budget) (fun security => 3 * secretWidth security + 1) + (fun security => ciphertextWidth security + 1) circuit ∧ + Homomorphic (leveledScheme budget) (fun security C => C.2.depth ≤ budget security) ∧ + FixedWidths (leveledScheme budget) (fun security C => C.2.depth ≤ budget security) + (fun security => 3 * secretWidth security + 1) + (fun security => ciphertextWidth security + 1) ∧ + Native (leveledScheme budget) ∧ ChosenMessageSecure (leveledScheme budget) := by + unfold leveledScheme; exact GSWFHEBridge.leveled hLWE + +/-- **Fully homomorphic encryption from decision LWE and circular security** [Gentry2009, +Definition 2 and Section 2]. The self-loop scheme decrypts with GSW's decryption circuit, is +correct for every circuit, keeps GSW's widths, has native algorithms and is IND-CPA, assuming +decision LWE for this family and, separately, one-key circular security of GSW. -/ +theorem fullyHomomorphic (hLWE : DecisionLWE) (hcircular : CircularSecure) : + DecryptsWith fixedKeyScheme secretWidth ciphertextWidth decryptionCircuit ∧ + Cslib.PolynomiallyBounded (fun security => (decryptionCircuit security).size) ∧ + Cslib.PolynomiallyBounded secretWidth ∧ Cslib.PolynomiallyBounded ciphertextWidth ∧ + Homomorphic fixedKeyScheme (fun _ _ => True) ∧ + FixedWidths fixedKeyScheme (fun _ _ => True) secretWidth ciphertextWidth ∧ + Native fixedKeyScheme ∧ ChosenMessageSecure fixedKeyScheme := by + unfold fixedKeyScheme decryptionCircuit; exact GSWFHEBridge.fullyHomomorphic hLWE hcircular + +end ComplexityTests.Abstracts.GSWFHEAbstract + +/-- +info: abstract audit passed for `ComplexityTests.Abstracts.GSWFHEAbstract`: 41 root declarations, +593 dependencies checked +-/ +#guard_msgs (whitespace := lax) in +#check_abstract ComplexityTests.Abstracts.GSWFHEAbstract allowing [ + -- shared foundations + ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation, ComplexityAbstracts.Randomized, + -- the bit-encryption interface, GSW and its parameter family + Complexity.Crypto.Computational.Homomorphic.Basic, + Complexity.Crypto.Computational.Homomorphic.GSW.Parameters, + Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters, + Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters.Scheme, + Complexity.Crypto.Computational.Homomorphic.GSW.Sampling.Serialized, + Complexity.Crypto.Computational.Homomorphic.GSW.Serialized, + Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Evaluation, + Complexity.Crypto.Computational.Homomorphic.GSW.CircuitEvaluation, + -- the logarithmic-depth decryption circuit + Complexity.Crypto.Computational.Homomorphic.GSW.DecryptionCircuit, + Complexity.Computability.Circuit.Balanced, + Complexity.Computability.Circuit.Boolean.CarryLookahead, + Complexity.Computability.Circuit.Boolean.CarrySave, + Complexity.Computability.Circuit.Boolean.CarrySave.Reduce, + Complexity.Computability.Circuit.Boolean.Formula, + Complexity.Computability.Circuit.Boolean.Gates, + Complexity.Computability.Circuit.Boolean.Modular.InnerProduct, + Complexity.Computability.Circuit.Boolean.Modular.Multiply, + Complexity.Computability.Circuit.Boolean.Modular.PartialProduct, + Complexity.Computability.Circuit.Boolean.Modular.Subtract, + Complexity.Computability.Circuit.Formula, + Complexity.Computability.Circuit.Parallel, + Complexity.Computability.Circuit.Pi, + Complexity.Foundations.Data.List.BalancedFold, + -- Gentry's bootstrapping constructions + Complexity.Crypto.Computational.Encryption.Circular, + Complexity.Crypto.Computational.Homomorphic.Circuit, + Complexity.Crypto.Computational.Homomorphic.Evaluation, + Complexity.Crypto.Computational.Homomorphic.FixedKey.Basic, + Complexity.Crypto.Computational.Homomorphic.FixedKey.Encoding, + Complexity.Crypto.Computational.Homomorphic.KeyChain, + Complexity.Crypto.Computational.Homomorphic.Layered, + Complexity.Crypto.Computational.Homomorphic.Leveled.Basic, + Complexity.Crypto.Computational.Homomorphic.Leveled.Encoding, + Complexity.Crypto.Computational.Homomorphic.Refresh, + -- circuit codes, depth and NAND layering + Complexity.Computability.Circuit.Boolean.DepthTime, + Complexity.Computability.Circuit.Boolean.Encoding, + Complexity.Computability.Circuit.Boolean.EvaluationTime, + Complexity.Computability.Circuit.Boolean.Layered, + Complexity.Computability.Circuit.Boolean.Layered.Compile, + Complexity.Computability.Circuit.Boolean.Layered.Padding, + Complexity.Computability.Circuit.Depth, + -- binary encodings and decoders + Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree, + Complexity.Computability.Machines.Turing.MultiTape.Complexity.Primitives, + Complexity.Computability.Machines.Turing.MultiTape.Encodings.Basic, + Complexity.Computability.Machines.Turing.MultiTape.Encodings.Decoder, + Complexity.Computability.Machines.Turing.MultiTape.Encodings.List, + Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat, + Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair, + Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds.Degree, + Complexity.Foundations.Data.BitString.List, + Complexity.Foundations.Data.BitString.List.Binary, + Complexity.Foundations.Data.Matrix.Binary, + -- probabilistic programs and their samplers + Complexity.Languages.Probabilistic.Basic, + Complexity.Languages.Probabilistic.BitString, + Complexity.Languages.Probabilistic.CenteredBinomial, + Complexity.Languages.Probabilistic.Iteration, + Complexity.Languages.Probabilistic.Repeat, + Complexity.Languages.Probabilistic.UniformNat +] diff --git a/abstracts/ComplexityAbstracts/GSWFHEBridge.lean b/abstracts/ComplexityAbstracts/GSWFHEBridge.lean new file mode 100644 index 000000000..f915fd091 --- /dev/null +++ b/abstracts/ComplexityAbstracts/GSWFHEBridge.lean @@ -0,0 +1,419 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +-- upstream: local-only (formal abstract library) + +import ComplexityAbstracts.CryptographyBridge +import ComplexityAbstracts.Randomized +import Complexity.Crypto.Computational.Homomorphic.GSW.FullyHomomorphic + +/-! # Bridge for fully homomorphic encryption from GSW + +The public abstract states the GSW laws, both assumptions and every claimed property in +elementary terms. This bridge identifies them with the library's serialized programs, its +decision-LWE and circular-security experiments, `Scheme.Correct`, `Scheme.FixedWidth`, native +certificates and `Encryption.INDCPA`, and assembles the leveled endpoint for every efficiently +computable budget from the generic bootstrapping lemmas. The bridge introduces no notation or +elaboration rules. +-/ + +namespace ComplexityTests.Abstracts.GSWFHEBridge + +open Cslib Cslib.ProbComp Cslib.Probability Turing.MultiTapeTM +open Cslib.Crypto Cslib.Crypto.Homomorphic + +def logSize (security : ℕ) : ℕ := 1 + Nat.clog 2 (security + 2) + +def width (security : ℕ) : ℕ := 16384 * logSize security ^ 2 + +def dimension (security : ℕ) : ℕ := security + 1 + +def rows (security : ℕ) : ℕ := (dimension security + 1) * width security + +def samples (security : ℕ) : ℕ := rows security + 2 * security + +def secretWidth (security : ℕ) : ℕ := dimension security * width security + +def ciphertextWidth (security : ℕ) : ℕ := rows security * rows security + +def lowBits (w value : ℕ) : List Bool := (List.range w).map value.testBit + +def rowHead (n w : ℕ) (inputs : List ℕ × (List (List ℕ) × List ℤ)) (i : ℕ) : ℕ := + (((((List.range n).map fun j => + (inputs.2.1.getD i []).getD j 0 * inputs.1.getD j 0).sum : ℕ) + + inputs.2.2.getD i 0 : ℤ) % (2 ^ w : ℤ)).toNat + +def publicWord (n m w : ℕ) (inputs : List ℕ × (List (List ℕ) × List ℤ)) : List Bool := + (List.range m).flatMap fun i => + lowBits w (rowHead n w inputs i) ++ + (List.range n).flatMap fun j => lowBits w ((inputs.2.1.getD i []).getD j 0 % 2 ^ w) + +def secretWord (n w : ℕ) (secret : List ℕ) : List Bool := + (List.range n).flatMap fun j => lowBits w (secret.getD j 0 % 2 ^ w) + +def matrixEntry (cols w : ℕ) (word : List Bool) (i j : ℕ) : ℕ := + ((word.drop ((i * cols + j) * w) ++ List.replicate w false).take w).foldr Nat.bit 0 + +def ciphertextEntry (n m w : ℕ) (publicKey : List Bool) (message : Bool) + (coins : List (List (List Bool))) (i k j : ℕ) : ℕ := + ((if i = j then message.toNat * 2 ^ k else 0) + + ((List.range m).map fun r => + if ((coins.getD i []).getD k []).getD r false then + matrixEntry (n + 1) w publicKey r j else 0).sum) % 2 ^ w + +def ciphertextWord (n m w : ℕ) (publicKey : List Bool) (message : Bool) + (coins : List (List (List Bool))) : List Bool := + (List.range (n + 1)).flatMap fun i => + (List.range w).flatMap fun k => + (List.range (n + 1)).flatMap fun j => + lowBits w (ciphertextEntry n m w publicKey message coins i k j) + +noncomputable def independentList {α : Type} (count : ℕ) (law : PMF α) : PMF (List α) := + (List.replicate count ()).mapM (fun _ => law) + +noncomputable def residueLaw (w : ℕ) : PMF ℕ := + (Cslib.Probability.PMF.uniformOfFintype (Fin (2 ^ w))).map Fin.val + +noncomputable def errorLaw (noiseWidth : ℕ) : PMF ℤ := do + let positive ← Randomized.uniformBits noiseWidth + let negative ← Randomized.uniformBits noiseWidth + return (positive.count true : ℤ) - negative.count true + +noncomputable def keyGeneration (security : ℕ) : PMF (List Bool × List Bool) := do + let secret ← independentList (dimension security) (residueLaw (width security)) + let matrix ← independentList (samples security) + (independentList (dimension security) (residueLaw (width security))) + let errors ← independentList (samples security) (errorLaw (dimension security)) + return (publicWord (dimension security) (samples security) (width security) + (secret, (matrix, errors)), secretWord (dimension security) (width security) secret) + +noncomputable def encryption (security : ℕ) (publicKey : List Bool) (message : Bool) : + PMF (List Bool) := do + let coins ← independentList (dimension security + 1) + (independentList (width security) (independentList (samples security) + (Cslib.Probability.PMF.uniformOfFintype Bool))) + return ciphertextWord (dimension security) (samples security) (width security) + publicKey message coins + +noncomputable def uniformMatrixWord (m k w : ℕ) : PMF (List Bool) := + (Cslib.Probability.PMF.uniformOfFintype (Fin m → Fin k → ZMod (2 ^ w))).map + (fun A => (List.ofFn fun i => (List.ofFn fun j => lowBits w (A i j).val).flatten).flatten) + +noncomputable def uniformPublic (security : ℕ) : PMF (List Bool) := + uniformMatrixWord (samples security) (dimension security + 1) (width security) + +def DecisionLWE : Prop := + Randomized.Indistinguishable (fun security => (keyGeneration security).map Prod.fst) + uniformPublic + +noncomputable def selfEncryption (real : Bool) (security : ℕ) : PMF (List Bool) := do + let keys ← keyGeneration security + let encrypted ← (if real then keys.2 else List.replicate keys.2.length false).mapM + (encryption security keys.1) + return Encoding.encPair Encoding.encBits (Encoding.encList Encoding.encBits) (keys.1, encrypted) + +def CircularSecure : Prop := + Randomized.Indistinguishable (selfEncryption true) (selfEncryption false) + +def Homomorphic (S : Homomorphic.Scheme) + (allowed : ℕ → (Σ k, Circuits.Circuit Circuits.Boolean.signature k 1) → Prop) : Prop := + ∀ security keys, keys ∈ (ProbComp.eval (S.keyGen security)).support → + (∀ bit ciphertext, + ciphertext ∈ (ProbComp.eval (S.encrypt security keys.1 bit)).support → + S.decrypt security keys.2 ciphertext = bit) ∧ + ∀ C bits inputs, allowed security C → bits.length = C.1 → + List.Forall₂ (fun bit ciphertext => + ciphertext ∈ (ProbComp.eval (S.encrypt security keys.1 bit)).support) bits inputs → + ∀ ciphertext ∈ (ProbComp.eval (S.evaluate security keys.1 C inputs)).support, + S.decrypt security keys.2 ciphertext = + C.2.eval Circuits.Boolean.interpretation (fun i => bits.getD i false) 0 + +def FixedWidths (S : Homomorphic.Scheme) + (allowed : ℕ → (Σ k, Circuits.Circuit Circuits.Boolean.signature k 1) → Prop) + (keyBits cipherBits : ℕ → ℕ) : Prop := + ∀ security keys, keys ∈ (ProbComp.eval (S.keyGen security)).support → + keys.2.length = keyBits security ∧ + (∀ bit ciphertext, + ciphertext ∈ (ProbComp.eval (S.encrypt security keys.1 bit)).support → + ciphertext.length = cipherBits security) ∧ + ∀ C bits inputs, allowed security C → bits.length = C.1 → + List.Forall₂ (fun bit ciphertext => + ciphertext ∈ (ProbComp.eval (S.encrypt security keys.1 bit)).support) bits inputs → + ∀ ciphertext ∈ (ProbComp.eval (S.evaluate security keys.1 C inputs)).support, + ciphertext.length = cipherBits security + +def DecryptsWith (S : Homomorphic.Scheme) (keyBits cipherBits : ℕ → ℕ) + (circuit : ∀ security, Circuits.Circuit Circuits.Boolean.signature + (keyBits security + cipherBits security) 1) : Prop := + ∀ security (secret ciphertext : List Bool), secret.length = keyBits security → + ciphertext.length = cipherBits security → + (circuit security).eval Circuits.Boolean.interpretation + (fun i => (secret ++ ciphertext).getD i false) 0 = S.decrypt security secret ciphertext + +def Native (S : Homomorphic.Scheme) : Prop := + Randomized.StrictPPT Encoding.encUnary (Encoding.encPair Encoding.encBits Encoding.encBits) + (fun security => ProbComp.eval (S.keyGen security)) ∧ + Randomized.StrictPPT + (Encoding.encPair Encoding.encUnary (Encoding.encPair Encoding.encBits Encoding.encBool)) + Encoding.encBits (fun p => ProbComp.eval (S.encrypt p.1 p.2.1 p.2.2)) ∧ + Computation.PolyTime (fun p : ℕ × List Bool × List Bool => S.decrypt p.1 p.2.1 p.2.2) + (Encoding.encPair Encoding.encUnary (Encoding.encPair Encoding.encBits Encoding.encBits)) + Encoding.encBool ∧ + Randomized.StrictPPT + (Encoding.encPair Encoding.encUnary (Encoding.encPair Encoding.encBits + (Encoding.encPair (Circuits.Boolean.encCircuit 1) + (Encoding.encList Encoding.encBits)))) + Encoding.encBits (fun p => ProbComp.eval (S.evaluate p.1 p.2.1 p.2.2.1 p.2.2.2)) + +noncomputable def chosenMessageGame (S : Homomorphic.Scheme) + (choose : ℕ → List Bool → PMF ((Bool × Bool) × List Bool)) + (guess : ℕ → List Bool → List Bool → PMF Bool) (bit : Bool) (security : ℕ) : + PMF Bool := do + let keys ← ProbComp.eval (S.keyGen security) + let choice ← choose security keys.1 + let ciphertext ← ProbComp.eval + (S.encrypt security keys.1 (if bit then choice.1.2 else choice.1.1)) + guess security choice.2 ciphertext + +def ChosenMessageSecure (S : Homomorphic.Scheme) : Prop := + ∀ (choose : ℕ → List Bool → PMF ((Bool × Bool) × List Bool)) + (guess : ℕ → List Bool → List Bool → PMF Bool), + Randomized.StrictPPT (Encoding.encPair Encoding.encUnary Encoding.encBits) + (Encoding.encPair (Encoding.encPair Encoding.encBool Encoding.encBool) Encoding.encBits) + (fun p => choose p.1 p.2) → + Randomized.StrictPPT + (Encoding.encPair Encoding.encUnary (Encoding.encPair Encoding.encBits Encoding.encBits)) + Encoding.encBool (fun p => guess p.1 p.2.1 p.2.2) → + Randomized.Negligible (fun security => + nndist (Randomized.probability (chosenMessageGame S choose guess false security)) + (Randomized.probability (chosenMessageGame S choose guess true security))) + +/-! ### The GSW laws are the library's serialized programs -/ + +private theorem independentList_eval {α : Type} (count : ℕ) (program : ProbComp α) : + independentList count (ProbComp.eval program) = + ProbComp.eval (OracleComp.replicate count program) := by + induction count with + | zero => rfl + | succ count ih => + simp only [independentList] at ih + simp only [independentList, List.replicate_succ, List.mapM_cons, + OracleComp.replicate_succ, ProbComp.eval_bind, + ProbComp.eval_map, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.map, + Function.comp_def, ih] + +private theorem keyGeneration_eq (security : ℕ) : + keyGeneration security = ProbComp.eval + (GSW.keyGenSerialized (dimension security) (samples security) (width security) + (dimension security)) := by + simp only [keyGeneration, GSW.keyGenSerialized, GSW.sampleKeyInputsSerialized, + ProbComp.eval_bind, ProbComp.eval_pure, ← independentList_eval, eval_sampleBinaryNat, + eval_sampleCenteredBinomial, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind, + PMF.pure_bind, errorLaw, Randomized.uniformBits] + rfl + +private theorem encryption_eq (security : ℕ) (publicKey : List Bool) (message : Bool) : + encryption security publicKey message = ProbComp.eval + (GSW.encryptSerialized (dimension security) (samples security) (width security) + publicKey message) := by + simp only [encryption, GSW.encryptSerialized, GSW.sampleCoinsSerialized, ProbComp.eval_bind, + ProbComp.eval_pure, ← independentList_eval, ProbComp.eval_uniform, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure] + rfl + +/-- The named GSW key generation and encryption have exactly the explicit laws. -/ +theorem base_scheme (security : ℕ) : + ProbComp.eval (GSW.DepthParameters.scheme.keyGen security) = keyGeneration security ∧ + ∀ publicKey message, + ProbComp.eval (GSW.DepthParameters.scheme.encrypt security publicKey message) = + encryption security publicKey message := + ⟨(keyGeneration_eq security).symm, fun publicKey message => + (encryption_eq security publicKey message).symm⟩ + +/-! ### The two assumptions -/ + +private theorem uniformMatrixWord_eq (m k w : ℕ) : + uniformMatrixWord m (k + 1) w = + LWE.uniformEnsemble (fun _ => k) (fun _ => m) (fun _ => w) 0 := by + unfold uniformMatrixWord LWE.uniformEnsemble + congr 1 + funext A + simpa only [← BitString.lowBits_eq_ofFn, BitString.lowBits, lowBits] using + (Matrix.toBinary_eq A).symm + +private theorem uniformPublic_eq (security : ℕ) : + uniformPublic security = LWE.uniformEnsemble dimension samples width security := + uniformMatrixWord_eq _ _ _ + +theorem decisionLWE_iff : DecisionLWE ↔ + Crypto.DecisionLWE GSW.Parameters.dimension GSW.DepthParameters.samples + GSW.DepthParameters.width + (fun security => GSW.noiseLaw (GSW.DepthParameters.width security) + (GSW.Parameters.noise security)) := by + change Randomized.Indistinguishable _ _ ↔ _ + rw [CryptographyBridge.indistinguishable_iff] + change ComputationallyIndistinguishable _ _ ↔ ComputationallyIndistinguishable _ _ + have hreal : (fun security => (keyGeneration security).map Prod.fst) = + LWE.realEnsemble dimension samples width + (fun security => GSW.noiseLaw (width security) (dimension security)) := by + funext security + rw [keyGeneration_eq, GSW.eval_keyGenSerialized_publicWord] + rw [hreal, show uniformPublic = LWE.uniformEnsemble dimension samples width + from funext uniformPublic_eq] + rfl + +private theorem mapM_eval {α β : Type} (program : α → ProbComp β) (inputs : List α) : + inputs.mapM (fun a => ProbComp.eval (program a)) = ProbComp.eval (inputs.mapM program) := by + induction inputs with + | nil => simp only [List.mapM_nil, ProbComp.eval_pure, PMF.monad_pure_eq_pure] + | cons a inputs ih => + simp only [List.mapM_cons, ProbComp.eval_bind, ProbComp.eval_pure, ih, + PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure] + +private theorem selfEncryption_eq (real : Bool) (security : ℕ) : + selfEncryption real security = + (ProbComp.eval (Encryption.circularPublicKey GSW.DepthParameters.scheme.keyGen + GSW.DepthParameters.scheme.encrypt real security)).map + Encryption.encCircularPublicKey := by + have hencrypt : encryption security = fun publicKey message => + ProbComp.eval (GSW.DepthParameters.scheme.encrypt security publicKey message) := by + funext publicKey message + exact encryption_eq security publicKey message + simp only [selfEncryption, Encryption.circularPublicKey, hencrypt, mapM_eval, + ProbComp.eval_bind, ProbComp.eval_pure, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, + PMF.map_bind, PMF.pure_map, (base_scheme security).1] + rfl + +theorem circularSecure_iff : CircularSecure ↔ + Encryption.CircularSecure GSW.DepthParameters.scheme.keyGen + GSW.DepthParameters.scheme.encrypt := by + change Randomized.Indistinguishable _ _ ↔ _ + rw [CryptographyBridge.indistinguishable_iff] + have h (real : Bool) : selfEncryption real = fun security => + (ProbComp.eval (Encryption.circularPublicKey GSW.DepthParameters.scheme.keyGen + GSW.DepthParameters.scheme.encrypt real security)).map + Encryption.encCircularPublicKey := + funext (selfEncryption_eq real) + rw [h true, h false] + rfl + +/-! ### The claimed properties from the library's notions -/ + +theorem homomorphic_of_correct {S : Homomorphic.Scheme} (hS : S.Correct) + {allowed : ℕ → (Σ k, Circuits.Circuit Circuits.Boolean.signature k 1) → Prop} + (hallowed : ∀ security C, allowed security C → S.permitted security C) : + Homomorphic S allowed := fun security keys hkeys => + ⟨hS.decrypt_encrypt security keys hkeys, fun C bits inputs hC hbits hinputs => + hS.decrypt_evaluate security keys hkeys C (hallowed security C hC) bits inputs hbits + hinputs⟩ + +theorem fixedWidths_of_fixedWidth {S : Homomorphic.Scheme} {keyBits cipherBits : ℕ → ℕ} + (hS : S.FixedWidth keyBits cipherBits) + {allowed : ℕ → (Σ k, Circuits.Circuit Circuits.Boolean.signature k 1) → Prop} + (hallowed : ∀ security C, allowed security C → S.permitted security C) : + FixedWidths S allowed keyBits cipherBits := fun security keys hkeys => + ⟨hS.secret_length security keys hkeys, hS.encrypt_length security keys hkeys, + fun C bits inputs hC hbits hinputs => + hS.evaluate_length security keys hkeys C (hallowed security C hC) bits inputs hbits + hinputs⟩ + +theorem native_of {S : Homomorphic.Scheme} + (hkeyGen : IsPPTOn encUnary (encPair encBits encBits) S.keyGen) + (hencrypt : IsPPTOn (encPair encUnary (encPair encBits encBool)) encBits + (fun p => S.encrypt p.1 p.2.1 p.2.2)) + (hdecrypt : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => S.decrypt p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBool) + (hevaluate : IsPPTOn + (encPair encUnary (encPair encBits (encPair (Circuits.Boolean.encCircuit 1) + (encList encBits)))) + encBits (fun p => S.evaluate p.1 p.2.1 p.2.2.1 p.2.2.2)) : + Native S := + ⟨CryptographyBridge.strictPPT_iff.mpr ⟨S.keyGen, hkeyGen, fun _ => rfl⟩, + CryptographyBridge.strictPPT_iff.mpr ⟨_, hencrypt, fun _ => rfl⟩, hdecrypt, + CryptographyBridge.strictPPT_iff.mpr ⟨_, hevaluate, fun _ => rfl⟩⟩ + +theorem chosenMessageSecure_of_indCPA {S : Homomorphic.Scheme} + (hS : Encryption.INDCPA S.keyGen S.encrypt) : ChosenMessageSecure S := by + intro choose guess hchoose hguess + obtain ⟨chooseProgram, hchooseProgram, hchooseLaw⟩ := + CryptographyBridge.strictPPT_iff.mp hchoose + obtain ⟨guessProgram, hguessProgram, hguessLaw⟩ := + CryptographyBridge.strictPPT_iff.mp hguess + let adversary : Encryption.Adversary := + ⟨fun security pk => chooseProgram (security, pk), + fun security state ciphertext => guessProgram (security, state, ciphertext)⟩ + have h := hS adversary ⟨hchooseProgram, hguessProgram⟩ + simpa only [Encryption.game, adversary, ProbComp.eval_bind, hchooseLaw, hguessLaw, + chosenMessageGame, PMF.monad_bind_eq_bind, Randomized.Negligible, Crypto.Negligible, + Asymptotics.SuperpolynomialDecay, Crypto.Game.advantage, Crypto.Game.succProbability, + Randomized.probability] using h + +/-! ### The headline theorems -/ + +theorem leveled (hLWE : DecisionLWE) : + ∃ circuit : ∀ security, Circuits.Circuit Circuits.Boolean.signature + ((3 * secretWidth security + 1) + (ciphertextWidth security + 1)) 1, + PolynomiallyBounded (fun security => (circuit security).size) ∧ + PolynomiallyBounded (fun security => 3 * secretWidth security + 1) ∧ + PolynomiallyBounded (fun security => ciphertextWidth security + 1) ∧ + ∀ budget : ℕ → ℕ, Computation.PolyTime budget Encoding.encUnary Encoding.encUnary → + DecryptsWith (Leveled.scheme GSW.DepthParameters.decryptionCircuits budget) + (fun security => 3 * secretWidth security + 1) + (fun security => ciphertextWidth security + 1) circuit ∧ + Homomorphic (Leveled.scheme GSW.DepthParameters.decryptionCircuits budget) + (fun security C => C.2.depth ≤ budget security) ∧ + FixedWidths (Leveled.scheme GSW.DepthParameters.decryptionCircuits budget) + (fun security C => C.2.depth ≤ budget security) + (fun security => 3 * secretWidth security + 1) + (fun security => ciphertextWidth security + 1) ∧ + Native (Leveled.scheme GSW.DepthParameters.decryptionCircuits budget) ∧ + ChosenMessageSecure (Leveled.scheme GSW.DepthParameters.decryptionCircuits budget) := by + let D := GSW.DepthParameters.decryptionCircuits + have hD := GSW.DepthParameters.computableInPolyTime_decryptionCircuits.tidy + have hkeyGen := GSW.DepthParameters.isPPTOn_keyGen + have hencrypt := GSW.DepthParameters.isPPTOn_encrypt + have hevaluate := GSW.DepthParameters.isPPTOn_evaluate + obtain ⟨circuits, hsize, hcircuits⟩ := Leveled.exists_decrypt_circuits D hD + obtain ⟨hsecret, hciphertext⟩ := Leveled.polynomiallyBounded_widths D hD + refine ⟨circuits, hsize, hsecret, hciphertext, fun budget hbudget => ?_⟩ + have hb : ComputableTidilyInPolyTime budget encUnary encUnary := + CryptographyBridge.polyTime_iff.mp hbudget + obtain ⟨hcorrect, hwidth, -, -, hsecure⟩ := + Leveled.correct_fixedWidth_indCPA D GSW.DepthParameters.correct + GSW.DepthParameters.fixedWidth GSW.DepthParameters.bootstrappable + (GSW.DepthParameters.indCPA_scheme (decisionLWE_iff.mp hLWE)) hkeyGen hencrypt hD hb + exact ⟨fun security => hcircuits budget security, + homomorphic_of_correct hcorrect fun _ _ h => h, + fixedWidths_of_fixedWidth hwidth fun _ _ h => h, + native_of (Leveled.isPPTOn_scheme_keyGen hkeyGen hencrypt D budget hb) + (Leveled.isPPTOn_scheme_encrypt hencrypt D budget) + (Leveled.computableTidilyInPolyTime_scheme_decrypt D hD budget).computableInPolyTime + (Leveled.isPPTOn_scheme_evaluate hencrypt D hD hevaluate budget hb), + chosenMessageSecure_of_indCPA hsecure⟩ + +theorem fullyHomomorphic (hLWE : DecisionLWE) (hcircular : CircularSecure) : + DecryptsWith (FixedKey.scheme GSW.DepthParameters.decryptionCircuits) secretWidth + ciphertextWidth GSW.DepthParameters.decryptionCircuits.circuit ∧ + PolynomiallyBounded + (fun security => (GSW.DepthParameters.decryptionCircuits.circuit security).size) ∧ + PolynomiallyBounded secretWidth ∧ PolynomiallyBounded ciphertextWidth ∧ + Homomorphic (FixedKey.scheme GSW.DepthParameters.decryptionCircuits) (fun _ _ => True) ∧ + FixedWidths (FixedKey.scheme GSW.DepthParameters.decryptionCircuits) (fun _ _ => True) + secretWidth ciphertextWidth ∧ + Native (FixedKey.scheme GSW.DepthParameters.decryptionCircuits) ∧ + ChosenMessageSecure (FixedKey.scheme GSW.DepthParameters.decryptionCircuits) := by + obtain ⟨hcorrect, hpermitted, hwidth, hsecret, hciphertext, hsize, hkeyGen, hencrypt, + hdecrypt, hevaluate, hsecure⟩ := + GSW.DepthParameters.fullyHomomorphic_of_decisionLWE_of_circularSecure + (decisionLWE_iff.mp hLWE) (circularSecure_iff.mp hcircular) + exact ⟨(FixedKey.decryptionCircuits GSW.DepthParameters.decryptionCircuits).correct, hsize, + hsecret, hciphertext, + homomorphic_of_correct hcorrect fun security C _ => hpermitted security C, + fixedWidths_of_fixedWidth hwidth fun security C _ => hpermitted security C, + native_of hkeyGen hencrypt hdecrypt hevaluate, chosenMessageSecure_of_indCPA hsecure⟩ + +end ComplexityTests.Abstracts.GSWFHEBridge diff --git a/abstracts/ComplexityAbstracts/GSWSecurityBridge.lean b/abstracts/ComplexityAbstracts/GSWSecurityBridge.lean index baa9d8247..d64a6ac11 100644 --- a/abstracts/ComplexityAbstracts/GSWSecurityBridge.lean +++ b/abstracts/ComplexityAbstracts/GSWSecurityBridge.lean @@ -257,7 +257,7 @@ private theorem decisionLWE_iff : DecisionLWE ↔ (fun security => Crypto.Homomorphic.GSW.noiseLaw (Crypto.Homomorphic.GSW.Parameters.width security) (Crypto.Homomorphic.GSW.Parameters.noise security)) := by - change CryptographyBridge.Indistinguishable _ _ ↔ _ + change Randomized.Indistinguishable _ _ ↔ _ rw [CryptographyBridge.indistinguishable_iff] change Crypto.ComputationallyIndistinguishable _ _ ↔ Crypto.ComputationallyIndistinguishable _ _ @@ -277,7 +277,7 @@ theorem native_algorithms : StrictPPT (pairEncoding unaryEncoding (pairEncoding bitsEncoding boolEncoding)) bitsEncoding (fun p => encryption p.1 p.2.1 p.2.2) := by constructor - · change CryptographyBridge.StrictPPT _ _ _ + · change Randomized.StrictPPT _ _ _ apply CryptographyBridge.strictPPT_iff.mpr refine ⟨fun security => Crypto.Homomorphic.GSW.keyGenSerialized (dimension security) (sampleCount security) (digitWidth security) (dimension security), ?_, ?_⟩ @@ -287,7 +287,7 @@ theorem native_algorithms : Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_width Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_noise · exact fun security => (keyGeneration_eq security).symm - · change CryptographyBridge.StrictPPT _ _ _ + · change Randomized.StrictPPT _ _ _ apply CryptographyBridge.strictPPT_iff.mpr refine ⟨fun p => Crypto.Homomorphic.GSW.encryptSerialized (dimension p.1) (sampleCount p.1) (digitWidth p.1) p.2.1 p.2.2, ?_, ?_⟩ diff --git a/abstracts/ComplexityAbstracts/Randomized.lean b/abstracts/ComplexityAbstracts/Randomized.lean new file mode 100644 index 000000000..57ac89fce --- /dev/null +++ b/abstracts/ComplexityAbstracts/Randomized.lean @@ -0,0 +1,72 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +-- upstream: local-only (formal abstract foundations) + +import ComplexityAbstracts.Check +import ComplexityAbstracts.Encoding +import ComplexityAbstracts.Computation +import Cslib.Probability.PMF + +/-! # Randomized polynomial time and computational indistinguishability + +A randomized algorithm is a deterministic polynomial-time evaluator supplied with polynomially +many independent fair bits. Its law on each input is the image of that coin tape. The evaluator, +the polynomial and the machine are fixed before the input, so the algorithm is uniform, and the +bound holds for every execution rather than in expectation. + +Two ensembles indexed by a unary security parameter are computationally indistinguishable when +every such test, which receives the parameter and one sample, has negligible advantage: its +advantage multiplied by any fixed power of the parameter tends to zero. +-/ + +namespace ComplexityTests.Abstracts.Randomized + +/-- Exactly `n` independent fair bits, as a word of length `n`. -/ +noncomputable def uniformBits (n : ℕ) : PMF (List Bool) := + (Cslib.Probability.PMF.uniformOfFintype (Fin n → Bool)).map List.ofFn + +/-- A uniformly strict polynomial-time probability law: one deterministic evaluator, supplied +with polynomially many independent fair bits, realizes every input's law exactly. Its time +includes reading the coin tape and writing the encoded output. Both evaluator and polynomial +are fixed before the input. This also bounds every execution, rather than its expectation. -/ +def StrictPPT {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) + (law : α → PMF β) : Prop := + ∃ (c d : ℕ) (evaluate : α → List Bool → β), + Computation.PolyTime (fun p : α × List Bool => evaluate p.1 p.2) + (Encoding.encPair a Encoding.encBits) b ∧ + ∀ x, law x = (uniformBits (c * ((a x).length + 1) ^ d)).map (evaluate x) + +/-- A nonnegative error is negligible if multiplication by every fixed power of the security +parameter still tends to zero. The threshold and decay bound may depend on the whole adversary. -/ +def Negligible (ε : ℕ → NNReal) : Prop := + ∀ k : ℕ, Filter.Tendsto (fun n : ℕ => (n : NNReal) ^ k * ε n) + Filter.atTop (nhds 0) + +/-- Probability that a Boolean experiment returns true. -/ +noncomputable def probability (p : PMF Bool) : NNReal := (p true).toNNReal + +/-- Every one uniform strict PPT test has negligible distinguishing advantage. +The test receives the unary security parameter and a sample. `bind` samples the word and then runs +the test with independent coins; `nndist` is the absolute difference of success probabilities. -/ +def Indistinguishable (X Y : ℕ → PMF (List Bool)) : Prop := + ∀ test : ℕ → List Bool → PMF Bool, + StrictPPT (Encoding.encPair Encoding.encUnary Encoding.encBits) Encoding.encBool + (fun p => test p.1 p.2) → + Negligible (fun n => nndist + (probability (do let sample ← X n; test n sample)) + (probability (do let sample ← Y n; test n sample))) + +end ComplexityTests.Abstracts.Randomized + +/-- +info: abstract audit passed for `ComplexityTests.Abstracts.Randomized`: +6 root declarations, 91 dependencies checked +-/ +#guard_msgs (whitespace := lax) in +#check_abstract ComplexityTests.Abstracts.Randomized allowing [ + ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation +] diff --git a/abstracts/README.md b/abstracts/README.md index 90d685dba..40603857e 100644 --- a/abstracts/README.md +++ b/abstracts/README.md @@ -1,10 +1,13 @@ # Selected formal abstracts -The catalogue promotes fifteen major result groups. Each has a checked Lean abstract with the +The catalogue promotes seventeen major result groups. Each has a checked Lean abstract with the definitions needed to understand its statement, a bridge to the library proof, and an audited dependency boundary. Some abstracts also allowlist a few library modules for foundational models (for example circuit signatures or oracle runs); each such abstract names them in its docstring, and -a reader must inspect them as well. The generated PDFs present the mathematical definitions and +a reader must inspect them as well. The fully homomorphic encryption abstract is the exception to +"a few": it names the library's construction instead of restating it, so it allowlists the modules +that define the construction, while stating both assumptions and every claimed property itself. +The generated PDFs present the mathematical definitions and selected statements first, followed by exact representation details and any shared foundations in appendices. Proof bodies are omitted. Lean checks the proofs; independent review must still check their intended meaning. @@ -44,9 +47,11 @@ former paper/TeX index is retired; Git history retains its sources. | [Håstad and Razborov–Smolensky: parity resists shallow circuits](ComplexityAbstracts/ConstantDepthAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/constant-depth.pdf) | Explicit finite bounds, gate semantics and depth conventions; nonuniform lower bounds. | | [Formula lower bounds: parity and Andreev](ComplexityAbstracts/FormulaBoundsAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/formula-bounds.pdf) | De Morgan formulas, literal leaves, explicit block indexing and finite quantitative bounds; no general-circuit lower bound. | | [One-way functions yield pseudorandom generators and adaptive functions](ComplexityAbstracts/CryptographyAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/cryptography.pdf) | Uniform probabilistic polynomial time with explicit native evaluators, negligible advantage and full stateful oracle semantics; asymptotic security, not a concrete implementation audit. | +| [Gentry and GSW: fully homomorphic encryption from LWE](ComplexityAbstracts/GSWFHEAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/gsw-fhe.pdf) | The named construction at an explicit LWE family with quasi-polynomial modulus; correctness, fixed widths, polynomial-size decryption circuits, native algorithms and IND-CPA, with circular security as a separate hypothesis. | | [Haken: pigeonhole formulas require long resolution proofs](ComplexityAbstracts/ResolutionAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/resolution.pdf) | The non-onto pigeonhole formula and a line-based resolution rule, with bound 2^(floor(n/24)); proof size is not solver runtime. | | [Communication: disjointness and inner product resist randomness](ComplexityAbstracts/CommunicationAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/communication.pdf) | Shared randomness, per-input error at most one third and explicit linear bounds; exact deterministic equality records the final-answer convention. | | [Sipser–Gács–Lautemann: BPP lies in the second polynomial level](ComplexityAbstracts/SipserLautemannAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/sipser-lautemann.pdf) | Fair random bits, explicit quantifier blocks and total native polynomial-time tests. | +| [Chor–Goldreich: the inner product extracts from two weak sources](ComplexityAbstracts/ChorGoldreichAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/chor-goldreich.pdf) | Arbitrary sources with real min-entropy bounds, the exact bias bound and its strong form, sharpness at k1 + k2 = n; information-theoretic. | ## Generate and review PDFs diff --git a/abstracts/catalogue.json b/abstracts/catalogue.json index dc391237d..3a1b5a9ed 100644 --- a/abstracts/catalogue.json +++ b/abstracts/catalogue.json @@ -157,7 +157,28 @@ "namespace": "ComplexityTests.Abstracts.CryptographyAbstract", "foundations": [ "ComplexityAbstracts.Encoding", - "ComplexityAbstracts.Computation" + "ComplexityAbstracts.Computation", + "ComplexityAbstracts.Randomized" + ] + }, + { + "id": "gsw-fhe", + "title": "Gentry and GSW: fully homomorphic encryption from LWE", + "module": "ComplexityAbstracts.GSWFHEAbstract", + "headline_theorems": [ + "ComplexityTests.Abstracts.GSWFHEAbstract.leveled", + "ComplexityTests.Abstracts.GSWFHEAbstract.fullyHomomorphic" + ], + "supporting_theorems": [ + "ComplexityTests.Abstracts.GSWFHEAbstract.base_scheme" + ], + "summary": "Bootstrapping the GSW scheme gives leveled fully homomorphic encryption from decision LWE, and fully homomorphic encryption under an additional circular-security assumption.", + "scope": "The named library construction at an explicit centered-binomial LWE family with quasi-polynomial modulus; perfect correctness on fresh encryptions, fixed widths, polynomial-size decryption circuits, native strict PPT algorithms and asymptotic IND-CPA. Circular security is a separate hypothesis; no lattice hardness, circuit privacy, multi-hop evaluation or concrete loss.", + "namespace": "ComplexityTests.Abstracts.GSWFHEAbstract", + "foundations": [ + "ComplexityAbstracts.Encoding", + "ComplexityAbstracts.Computation", + "ComplexityAbstracts.Randomized" ] }, { From c2086c32d2c2002fd39cc857ba8fdb901623d4db Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 25 Oct 2026 15:00:25 -0400 Subject: [PATCH 2/3] feat(abstracts): pin GSW's algorithms in the FHE abstract and allow only foundational models (#486) The headline theorems no longer name the library's `Leveled.scheme` and `FixedKey.scheme`. GSW key generation, encryption and decryption are written out, and the theorems assert schemes whose encryption and decryption are exactly these algorithms (behind a tag and a framed key pair for the leveled scheme) and whose fixed-key generation is Gentry's self-loop key. Only the evaluator, the leveled key chain and the decryption circuits are existential. `GSWFHEBridge.leveled_witness` and `fullyHomomorphic_witness` prove that the library's constructions are the witnesses. The `#check_abstract` allowlist drops from 57 library modules to 8: the scheme record, randomized programs, the binary circuit code and the encodings it is built from. Adds regression tests for the budget hypothesis, the framing decoders and the pinned decryption, and points the ROADMAP to the follow-up issue #1104. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- ComplexityTests/Abstracts/GSWFHETests.lean | 90 +++++ ROADMAP.md | 13 +- .../ComplexityAbstracts/GSWFHEAbstract.lean | 334 ++++++++++-------- .../ComplexityAbstracts/GSWFHEBridge.lean | 323 +++++++++++++++-- abstracts/README.md | 7 +- abstracts/catalogue.json | 5 +- 6 files changed, 589 insertions(+), 183 deletions(-) create mode 100644 ComplexityTests/Abstracts/GSWFHETests.lean diff --git a/ComplexityTests/Abstracts/GSWFHETests.lean b/ComplexityTests/Abstracts/GSWFHETests.lean new file mode 100644 index 000000000..8e77b3ea9 --- /dev/null +++ b/ComplexityTests/Abstracts/GSWFHETests.lean @@ -0,0 +1,90 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +-- upstream: local-only (formal abstract tests) + +import ComplexityAbstracts.GSWFHEAbstract + +/-! # Clients of the GSW fully homomorphic encryption abstract + +The leveled theorem quantifies over depth budgets computable in unary polynomial time; every +polynomial budget `c (security + 1) ^ e` qualifies, so the hypothesis is satisfiable. The +abstract's framing decoders invert the shared framing, so the fixed algorithms read the keys the +way their docstrings describe: the self-loop public key yields its GSW public key, the leveled +public key its first key, and the leveled secret key its two endpoint keys. On a secret key of +the GSW width, decryption of the joined word is GSW decryption. +-/ + +namespace ComplexityTests.Abstracts.GSWFHETests + +open ComplexityTests.Abstracts +open ComplexityTests.Abstracts.GSWFHEAbstract + +/-- Every polynomial depth budget satisfies the hypothesis of `leveled`. -/ +example (c e : ℕ) : + Computation.PolyTime (fun security : ℕ => c * (security + 1) ^ e) + Encoding.encUnary Encoding.encUnary := + CryptographyBridge.polyTime_iff.mpr (by fun_prop) + +/-- `unframe` reads back a framed word, whatever follows it. -/ +theorem unframe_frame_append (u v : List Bool) : unframe (Encoding.frame u ++ v) = u := by + induction u with + | nil => rfl + | cons b u ih => + simp only [Encoding.frame, List.flatMap_cons, List.cons_append, List.nil_append, + List.append_assoc, unframe] at ih ⊢ + rw [ih] + +/-- `dropFrame` returns what follows a framed word. -/ +theorem dropFrame_frame_append (u v : List Bool) : dropFrame (Encoding.frame u ++ v) = v := by + induction u with + | nil => rfl + | cons b u ih => + simpa only [Encoding.frame, List.flatMap_cons, List.cons_append, List.nil_append, + List.append_assoc, dropFrame] using ih + +/-- Self-loop encryption uses the GSW public key of a self-loop public key. -/ +example (security : ℕ) (publicKey : List Bool) (encryptedKey : List (List Bool)) (bit : Bool) : + selfLoopEncryption security + (Encoding.encPair Encoding.encBits (Encoding.encList Encoding.encBits) + (publicKey, encryptedKey)) bit = + encryption security publicKey bit := by + simp only [selfLoopEncryption, Encoding.encPair, Encoding.encodePair, Encoding.encBits, + Function.Embedding.coeFn_mk, Function.Embedding.refl_apply, unframe_frame_append] + +/-- Leveled encryption uses the first public key of a framed list of public keys. -/ +example (security : ℕ) (first : List Bool) (rest : List (List Bool)) (links : List Bool) + (bit : Bool) : + leveledEncryption security + (Encoding.encPair (Encoding.encList Encoding.encBits) Encoding.encBits + (first :: rest, links)) bit = + (encryption security first bit).map (List.cons false) := by + simp only [leveledEncryption, Encoding.encPair, Encoding.encodePair, Encoding.encList, + Encoding.encodeList, Encoding.encBits, Function.Embedding.coeFn_mk, + Function.Embedding.refl_apply, Function.comp_apply, List.flatMap_cons, + unframe_frame_append] + +/-- On a GSW secret key of the right width, decryption of the joined word is GSW decryption. -/ +theorem decryptionWord_append (security : ℕ) (secret ciphertext : List Bool) + (hsecret : secret.length = secretWidth security) : + decryptionWord security (secret ++ ciphertext) = decryption security secret ciphertext := by + rw [decryptionWord, List.take_left' hsecret, List.drop_left' hsecret] + +/-- Leveled decryption of a fresh (`false`-tagged) ciphertext uses the first endpoint key, and of +an evaluated (`true`-tagged) ciphertext the last. -/ +example (security : ℕ) (first last ciphertext : List Bool) + (hfirst : first.length = secretWidth security) (hlast : last.length = secretWidth security) : + leveledDecryption security (Encoding.encPair Encoding.encBits Encoding.encBits (first, last)) + (false :: ciphertext) = decryption security first ciphertext ∧ + leveledDecryption security (Encoding.encPair Encoding.encBits Encoding.encBits (first, last)) + (true :: ciphertext) = decryption security last ciphertext := by + simp only [leveledDecryption, Encoding.encPair, Encoding.encodePair, Encoding.encBits, + Function.Embedding.coeFn_mk, Function.Embedding.refl_apply, List.headD_cons, List.tail_cons, + Bool.false_eq_true, ite_false, ite_true, unframe_frame_append, dropFrame_frame_append, + decryptionWord_append security _ _ hfirst, decryptionWord_append security _ _ hlast, + and_self] + +end ComplexityTests.Abstracts.GSWFHETests diff --git a/ROADMAP.md b/ROADMAP.md index 214f68d87..b0e9e674a 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -21,7 +21,7 @@ the FHE industrial context, the first-order design decisions and the repository' | Metacomplexity: time-bounded Kolmogorov complexity, partial MCSP, hardness magnification | [#798], audit [#884] | | Plain computability: delete the tidy calculus, keeping a machine-level kernel | [#862], from [#456] | | Consolidation: duplicates, accurate statements and docs, less churn | [#949], [#939] | -| A concrete LWE-based fully homomorphic scheme | [#486] | +| A concrete LWE-based fully homomorphic scheme | [#486]; follow-ups [#1104] | | Boneh–Shoup cryptography tracks; zero-knowledge architecture | [#640], [#643] | | Crypto frontier tracks: Kilian's succinct arguments, chosen-ciphertext security, signatures from one-way functions | [#999], [#1000], [#1001] | | OpenAI math TCS results: review Fortnow's rewrites and extract in-scope results | [#1002] | @@ -33,7 +33,7 @@ Priorities live in this list and in the tiers of [#897]. 1. [Goldreich–Micali–Wigderson zero knowledge in full](#cryptographic-landmarks) 2. [Rompel's signature theorem](#cryptographic-landmarks) ([#1001]) -3. [Gentry's bootstrapping, instantiated](#cryptographic-landmarks) ([#486]) +3. [Gentry's bootstrapping, instantiated](#cryptographic-landmarks) ([#486]; follow-ups [#1104]) 4. [Completeness of oblivious transfer](#cryptographic-landmarks) 5. [Håstad's optimal MAX-E3SAT hardness](#approximation-and-pcp) ([#886]) 6. [Williams's NEXP ⊄ ACC⁰](#circuits-and-algebraic-complexity) ([#889]) @@ -63,10 +63,10 @@ Priorities live in this list and in the tiers of [#897]. - **Gentry's bootstrapping, instantiated** ([#486]). GSW at its logarithmic-depth parameter family instantiates the generic theorem: leveled FHE under decision LWE with quasi-polynomial modulus for exactly that family, and FHE under the additional one-key circular-security - assumption. The checked formal abstract `gsw-fhe` names this construction. Open: a uniform - generator for the leveled scheme's wrapper decryption circuits (uniform compactness), reuse of - evaluated ciphertexts as fresh inputs (multi-hop evaluation), and Gentry's exact - concrete-security loss. + assumption. The checked formal abstract `gsw-fhe` states both endpoints with GSW's algorithms + written out. Open in [#1104]: a uniform generator for the leveled scheme's wrapper decryption + circuits (uniform compactness), reuse of evaluated ciphertexts as fresh inputs (multi-hop + evaluation), and Gentry's exact concrete-security loss. - **Completeness of oblivious transfer.** In the ideal OT-hybrid model, every polynomial-time multiparty functionality admits a protocol secure against static malicious corruptions, with real/ideal simulation and abort, under the standard communication assumptions. @@ -481,3 +481,4 @@ not planned, not as proved. [#1000]: https://github.com/cslib-community/complexitylib/issues/1000 [#1001]: https://github.com/cslib-community/complexitylib/issues/1001 [#1002]: https://github.com/cslib-community/complexitylib/issues/1002 +[#1104]: https://github.com/cslib-community/complexitylib/issues/1104 diff --git a/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean b/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean index 968c7aab0..a57a44430 100644 --- a/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean +++ b/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean @@ -22,22 +22,48 @@ that family. Publishing an encryption of the secret key under its own public key homomorphic encryption, under a second, separately stated assumption: this self-encryption is indistinguishable from an encryption of zeros. -The construction is named, not restated. The theorems concern the library's GSW scheme -`Cslib.Crypto.Homomorphic.GSW.DepthParameters.scheme`, its raw-input decryption circuits -`DepthParameters.decryptionCircuits`, Gentry's acyclic leveled construction -`Cslib.Crypto.Homomorphic.Leveled.scheme` and the self-loop construction -`Cslib.Crypto.Homomorphic.FixedKey.scheme`. A reader inspects these algorithms in the library: -GSW key generation, encryption, decryption and layered NAND evaluation; the logarithmic-depth -decryption circuit; the key chain, refreshing and serialization of the bootstrapped schemes; and -the compilation of De Morgan circuits into NAND layers. `#check_abstract` permits exactly the -modules these definitions need, and the shared foundations. - -Both assumptions, and every property claimed of the construction, are stated below. Besides -upstream mathematics, plain machines and the shared foundations, the statements use only three -library notions, each explained where it first appears: the record `Cslib.Crypto.Homomorphic.Scheme` -of four algorithms, the output distribution `Cslib.ProbComp.eval` of a randomized program, and -the binary circuit code `Cslib.Circuits.Boolean.encCircuit`. `base_scheme` identifies the named -GSW key generation and encryption with the explicit laws on which the assumptions are stated. +**The core is written out.** GSW key generation, encryption and decryption at the parameter +family are stated below as explicit algorithms, and both assumptions are stated on them. The +leveled scheme of `leveled` encrypts and decrypts exactly with these algorithms behind a one-bit +tag and a framed pair of secret keys. The fully homomorphic scheme of `fullyHomomorphic` encrypts +and decrypts exactly with them, and its key generation is exactly Gentry's self-loop key: a GSW +key pair together with encryptions of its secret-key bits under its own public key. + +**Only the bootstrapping machinery is existential:** homomorphic evaluation, the leveled scheme's +key chain and the polynomial-size decryption circuits. The theorems state that such machinery +exists with elementary properties: correctness for the allowed circuits, fixed key and ciphertext +widths, one decryption circuit family for all depths, native efficiency and IND-CPA security. +These properties exclude trivial witnesses. Decryption is the fixed GSW decryption, and +evaluated ciphertexts have the fixed ciphertext width, so evaluation cannot leave the computation +to decryption: it must output a word of that width that GSW decryption maps to the circuit's +output. Nor can evaluation work in the clear. Evaluation is efficient and accepts the challenge +ciphertext of the IND-CPA game, so if the public key revealed the secret key that decrypts +evaluated ciphertexts, an adversary could evaluate a depth-zero circuit, whose output is its +input, on the challenge and read the hidden bit. + +**Provenance (not part of the checked statements).** The library's constructions witness both +theorems. In the namespace `Cslib.Crypto.Homomorphic`, write `D` for GSW's decryption circuits +`GSW.DepthParameters.decryptionCircuits`. Then `GSWFHEBridge.leveled_witness` proves the +properties of `leveled` for `Leveled.scheme D budget`, and +`GSWFHEBridge.fullyHomomorphic_witness` proves those of `fullyHomomorphic` for +`FixedKey.scheme D`. A reader need not inspect them: the statements below do not depend on their +definitions. + +**What a reader inspects.** The definitions and statements in this file, the displayed shared +foundations, and the eight library modules that `#check_abstract` allows at the end of the file, +each a foundational model: +* `Crypto.Computational.Homomorphic.Basic`: the record `Cslib.Crypto.Homomorphic.Scheme` of four + algorithms, with an unused fifth field, explained before `EncryptsAndDecrypts`. +* `Languages.Probabilistic.Basic`: randomized programs `Cslib.ProbComp`, whose only randomness is + uniform choice from finite ranges, and their output law `Cslib.ProbComp.eval`. +* `Computability.Circuit.Boolean.Encoding`: the binary circuit code + `Cslib.Circuits.Boolean.encCircuit`, the input format of native evaluation, explained before + `Native`. +* Under `Computability.Machines.Turing.MultiTape`, the encodings from which that code is + assembled: framing (`Encodings.Basic`), pairs (`Encodings.Pair`), lists (`Encodings.List`), + binary numbers (`Encodings.Nat`), and unary numbers, `n` written as `n` ones + (`Complexity.Primitives`; only `encUnary` is reached there, and no tidy notion is). +Lean checks every proof through `GSWFHEBridge`. The claims are perfect correctness on supported fresh encryptions, fixed key and ciphertext widths, polynomial-size decryption circuits, uniform native strict polynomial-time algorithms and @@ -93,6 +119,10 @@ Residues modulo `2 ^ w` are written with exactly `w` bits, least significant fir is the matrix `[B t + e | B]` in row-major order, its noisy column first; a secret key lists the residues of `t`; a ciphertext lists every bit of `μ G + R A`, its rows indexed by `(i, k)` and its columns by `(j, l)`. These words are the actual inputs and outputs of the native algorithms. + +Keys of the bootstrapped schemes are framed words (`Encoding.frame` in the shared foundations). +`unframe` reads the first framed word and `dropFrame` returns what follows it; both are defined +on every word. -/ /-- Write exactly `w` digits, least significant first, including leading zeros. -/ @@ -136,11 +166,26 @@ def ciphertextWord (n m w : ℕ) (publicKey : List Bool) (message : Bool) (List.range (n + 1)).flatMap fun j => lowBits w (ciphertextEntry n m w publicKey message coins i k j) -/-! ## GSW key generation and encryption +/-- The first framed word: keep `b` from each leading pair `true, b`, and stop at the first +`false` or when fewer than two bits remain. Thus `unframe (Encoding.frame u ++ v) = u`. -/ +def unframe : List Bool → List Bool + | true :: b :: rest => b :: unframe rest + | _ => [] + +/-- What follows the first framed word: skip the leading pairs `true, b` and one `false`. Thus +`dropFrame (Encoding.frame u ++ v) = v`; a word that ends inside its first frame leaves nothing. -/ +def dropFrame : List Bool → List Bool + | true :: _ :: rest => dropFrame rest + | false :: rest => rest + | _ => [] + +/-! ## GSW key generation, encryption and decryption Key generation samples a uniform secret `t`, a uniform matrix `B` and independent signed errors `e`, and publishes `[B t + e | B]`. Encryption of a bit `μ` samples a uniform 0/1 matrix `R` and -outputs the bits of `μ G + R A` [GentrySahaiWaters2013, Sections 3.1–3.2]. +outputs the bits of `μ G + R A`. Decryption multiplies one row of a ciphertext by `(1, -t)`, +which for a fresh ciphertext gives `μ 2 ^ (w - 1)` plus the small error `⟨R_i, e⟩`, and rounds +[GentrySahaiWaters2013, Sections 3.1–3.2]. -/ /-- Collect independent draws in their original order; the empty list requires no draw. -/ @@ -179,6 +224,29 @@ noncomputable def encryption (security : ℕ) (publicKey : List Bool) (message : return ciphertextWord (dimension security) (samples security) (width security) publicKey message coins +/-- **GSW decryption** [GentrySahaiWaters2013, Section 3.1]. Take row `(0, w - 1)` of the +ciphertext matrix, whose gadget entry is `2 ^ (w - 1)` in column `0`, and multiply it by +`(1, -t)` modulo `2 ^ w`. For a fresh encryption `μ G + R A` this gives +`value = μ 2 ^ (w - 1) + ⟨R_(0, w - 1), e⟩`. Decryption outputs `true` exactly when `value` lies +in the middle half `[2 ^ w / 4, 3 · 2 ^ w / 4)` of the residues: GSW's rounding of +`value / 2 ^ (w - 1)` to the nearest integer, read modulo 2, with halves rounded up. It reads +the first `n w` bits of the secret word and is defined on every pair of words. -/ +def decryption (security : ℕ) (secret ciphertext : List Bool) : Bool := + let n := dimension security + let w := width security + let value := (((matrixEntry (n + 1) w ciphertext (w - 1) 0 : ℤ) - + (((List.range n).map fun j => + matrixEntry (n + 1) w ciphertext (w - 1) (j + 1) * matrixEntry n w secret 0 j).sum : ℕ)) % + (2 ^ w : ℤ)).toNat + decide (2 ^ w ≤ 4 * value ∧ 4 * value < 3 * 2 ^ w) + +/-- GSW decryption of one word that holds a secret key followed by a ciphertext, the input +order of a decryption circuit: the first `secretWidth` bits are the key and the rest is the +ciphertext. For a key of exactly `secretWidth` bits, +`decryptionWord security (secret ++ ciphertext) = decryption security secret ciphertext`. -/ +def decryptionWord (security : ℕ) (word : List Bool) : Bool := + decryption security (word.take (secretWidth security)) (word.drop (secretWidth security)) + /-! ## The two assumptions Both are computational indistinguishability against uniform classical strict PPT tests, as @@ -217,12 +285,57 @@ noncomputable def selfEncryption (real : Bool) (security : ℕ) : PMF (List Bool /-- **One-key circular security of GSW at this family.** Encryptions of the secret key under its own public key are indistinguishable from encryptions of zeros. This is the one-key, bitwise case of the key-dependent-message security that Gentry's self-loop construction assumes -[Gentry2009, Section 2]. It is a separate assumption: it is not derived from decision LWE or -from IND-CPA. -/ +[Gentry2009, Section 2, p. 172]. It is a separate assumption: it is not derived from decision +LWE or from IND-CPA. -/ def CircularSecure : Prop := Randomized.Indistinguishable (selfEncryption true) (selfEncryption false) -/-! ## The named construction +/-! ## The algorithms fixed by the theorems + +The leveled scheme adds a one-bit tag to GSW ciphertexts. Its secret key frames two GSW secret +keys: one for fresh ciphertexts (tag `false`) and one for evaluated ciphertexts (tag `true`). +The fully homomorphic scheme uses GSW ciphertexts and secret keys unchanged; its public key +frames a GSW public key followed by the framed list of encryptions of the secret-key bits. +-/ + +/-- **Leveled encryption.** A fresh ciphertext is the tag bit `false` followed by a GSW +encryption under `unframe (unframe publicKey)`, the first framed word inside the first framed +component of the public key. A public key that frames a list of GSW public keys, followed by any +further data, is thus used through the first key in the list. -/ +noncomputable def leveledEncryption (security : ℕ) (publicKey : List Bool) (bit : Bool) : + PMF (List Bool) := + (encryption security (unframe (unframe publicKey)) bit).map (List.cons false) + +/-- **Leveled decryption.** A secret key `Encoding.frame first ++ last` holds two GSW secret +keys. The leading tag bit of the ciphertext selects `first` (`unframe secret`) when `false` and +`last` (`dropFrame secret`) when `true`; GSW decryption then reads the selected key followed by +the rest of the ciphertext. -/ +def leveledDecryption (security : ℕ) (secret ciphertext : List Bool) : Bool := + decryptionWord security + ((if ciphertext.headD false then dropFrame secret else unframe secret) ++ ciphertext.tail) + +/-- **Gentry's self-loop key** [Gentry2009, Section 2, p. 172]. Sample one GSW key pair and +encrypt every secret-key bit under its own public key. The public key is the GSW public key +together with these encryptions, in the encoding of `selfEncryption true`; the secret key is the +GSW secret key. -/ +noncomputable def selfLoopKeyGeneration (security : ℕ) : PMF (List Bool × List Bool) := do + let keys ← keyGeneration security + let encryptedKey ← keys.2.mapM (encryption security keys.1) + return (Encoding.encPair Encoding.encBits (Encoding.encList Encoding.encBits) + (keys.1, encryptedKey), keys.2) + +/-- **Self-loop encryption.** GSW encryption under the first framed component of the public +key, which is the GSW public key in a key from `selfLoopKeyGeneration`. -/ +noncomputable def selfLoopEncryption (security : ℕ) (publicKey : List Bool) (bit : Bool) : + PMF (List Bool) := + encryption security (unframe publicKey) bit + +/-- **Self-loop decryption.** GSW decryption of the secret key followed by the ciphertext; for a +secret key of `secretWidth` bits this is `decryption security secret ciphertext`. -/ +def selfLoopDecryption (security : ℕ) (secret ciphertext : List Bool) : Bool := + decryptionWord security (secret ++ ciphertext) + +/-! ## Homomorphic encryption A `Cslib.Crypto.Homomorphic.Scheme` is a record of four algorithms on bit strings, each taking the security parameter: `keyGen` samples a public and a secret key; `encrypt` encrypts one bit @@ -231,49 +344,6 @@ single-output De Morgan circuit with its number of inputs, and a list of ciphert field, `permitted`, is not used by any claim below. Randomized algorithms are terminating programs whose only randomness is uniform choice from finite ranges (`Cslib.ProbComp`), and `Cslib.ProbComp.eval` is their output distribution. --/ - -/-- GSW at this family. Evaluation compiles the circuit into NAND layers, evaluates them with -GSW's homomorphic NAND, and ignores the public key. -/ -noncomputable def baseScheme : Cslib.Crypto.Homomorphic.Scheme := - Cslib.Crypto.Homomorphic.GSW.DepthParameters.scheme - -/-- The named GSW algorithms have exactly the key-generation and encryption laws above, so the -two assumptions concern the actual base scheme. -/ -theorem base_scheme (security : ℕ) : - Cslib.ProbComp.eval (baseScheme.keyGen security) = keyGeneration security ∧ - ∀ publicKey message, Cslib.ProbComp.eval (baseScheme.encrypt security publicKey message) = - encryption security publicKey message := - GSWFHEBridge.base_scheme security - -/-- GSW's raw-input decryption circuit, secret-key bits first. It is the circuit that the -bootstrapped schemes evaluate homomorphically. -/ -def decryptionCircuit (security : ℕ) : - Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature - (secretWidth security + ciphertextWidth security) 1 := - Cslib.Crypto.Homomorphic.GSW.DepthParameters.decryptionCircuits.circuit security - -/-- **Gentry's acyclic leveled scheme** [Gentry2009, Section 2]. For a depth budget `budget`, -key generation samples `2 · budget + 1` independent GSW keys and encrypts each secret key under -the next public key. Evaluation compiles the circuit into NAND layers, padded to exactly -`2 · budget` layers, and each layer moves every wire to the next key. A NAND gate encrypts the -bits of its two input ciphertexts under the next key and homomorphically evaluates two copies of -the decryption circuit joined by NAND, using the encrypted previous secret key; a carried wire -uses the decryption circuit alone; a constant is a fresh encryption. A one-bit tag tells -decryption whether to use the first or the last secret key. -/ -noncomputable def leveledScheme (budget : ℕ → ℕ) : Cslib.Crypto.Homomorphic.Scheme := - Cslib.Crypto.Homomorphic.Leveled.scheme - Cslib.Crypto.Homomorphic.GSW.DepthParameters.decryptionCircuits budget - -/-- **Gentry's self-loop scheme** [Gentry2009, Section 2]. The public key is one GSW public key -together with encryptions of its own secret-key bits. Evaluation is layered as in the leveled -scheme, with as many layers as the circuit needs, but every layer uses that same key. The secret -key and the ciphertexts are those of GSW. -/ -noncomputable def fixedKeyScheme : Cslib.Crypto.Homomorphic.Scheme := - Cslib.Crypto.Homomorphic.FixedKey.scheme - Cslib.Crypto.Homomorphic.GSW.DepthParameters.decryptionCircuits - -/-! ## Homomorphic encryption Circuits are single-output De Morgan circuits (constants, negation, binary conjunction and disjunction) given as a pair of their number of inputs `C.1` and the circuit `C.2`. The upstream @@ -281,6 +351,16 @@ disjunction) given as a pair of their number of inputs `C.1` and the circuit `C. every gate, including a constant, adds one; `size` is the number of gates. -/ +/-- The scheme encrypts with the law `encrypt` and decrypts with the function `decrypt`, on every +security parameter, key and bit or ciphertext, including malformed keys and ciphertexts. -/ +def EncryptsAndDecrypts (S : Cslib.Crypto.Homomorphic.Scheme) + (encrypt : ℕ → List Bool → Bool → PMF (List Bool)) + (decrypt : ℕ → List Bool → List Bool → Bool) : Prop := + (∀ security publicKey bit, + Cslib.ProbComp.eval (S.encrypt security publicKey bit) = encrypt security publicKey bit) ∧ + ∀ security secret ciphertext, S.decrypt security secret ciphertext = + decrypt security secret ciphertext + /-- **Correctness for a class of circuits** [Gentry2009, Section 1.1]. Under every supported key pair, every supported fresh encryption decrypts to its bit; and every allowed circuit, evaluated on supported fresh encryptions of its input bits, yields only ciphertexts that decrypt to the @@ -381,14 +461,18 @@ def ChosenMessageSecure (S : Cslib.Crypto.Homomorphic.Scheme) : Prop := /-! ## Main results +`Cslib.PolynomiallyBounded f` means that a fixed power bounds `f` eventually: some `d` has +`f security ≤ security ^ d` for all large `security`. + Gentry's Definition 3 asks for one decryption circuit shared by all depths, correctness for every circuit up to the depth, and algorithms polynomial in the parameter and the depth [Gentry2009, Definition 3]. In `leveled`, one polynomial-size circuit family is chosen first. -Then for every depth budget computable in unary polynomial time, the leveled scheme with that -budget decrypts with this circuit family, is correct for every circuit of depth at most the -budget, has fixed polynomial widths, native algorithms and IND-CPA security. Any polynomially -bounded depth `d(security) ≤ c (security + 1) ^ e` is covered by the budget -`c (security + 1) ^ e`. The runtime polynomial may depend on the budget function. +Then for every depth budget computable in unary polynomial time, a scheme exists that encrypts +and decrypts with the leveled algorithms above, decrypts with this circuit family, is correct for +every circuit of depth at most the budget, has fixed polynomial widths, native algorithms and +IND-CPA security. Any polynomially bounded depth `d(security) ≤ c (security + 1) ^ e` is covered +by the budget `c (security + 1) ^ e`. The runtime polynomial may depend on the budget function, +so it need not be one polynomial in the parameter and the depth. -/ /-- **Leveled fully homomorphic encryption from decision LWE** [Gentry2009, Theorem 3]. Only the @@ -401,99 +485,57 @@ theorem leveled (hLWE : DecisionLWE) : Cslib.PolynomiallyBounded (fun security => 3 * secretWidth security + 1) ∧ Cslib.PolynomiallyBounded (fun security => ciphertextWidth security + 1) ∧ ∀ budget : ℕ → ℕ, Computation.PolyTime budget Encoding.encUnary Encoding.encUnary → - DecryptsWith (leveledScheme budget) (fun security => 3 * secretWidth security + 1) - (fun security => ciphertextWidth security + 1) circuit ∧ - Homomorphic (leveledScheme budget) (fun security C => C.2.depth ≤ budget security) ∧ - FixedWidths (leveledScheme budget) (fun security C => C.2.depth ≤ budget security) - (fun security => 3 * secretWidth security + 1) - (fun security => ciphertextWidth security + 1) ∧ - Native (leveledScheme budget) ∧ ChosenMessageSecure (leveledScheme budget) := by - unfold leveledScheme; exact GSWFHEBridge.leveled hLWE + ∃ S : Cslib.Crypto.Homomorphic.Scheme, + EncryptsAndDecrypts S leveledEncryption leveledDecryption ∧ + DecryptsWith S (fun security => 3 * secretWidth security + 1) + (fun security => ciphertextWidth security + 1) circuit ∧ + Homomorphic S (fun security C => C.2.depth ≤ budget security) ∧ + FixedWidths S (fun security C => C.2.depth ≤ budget security) + (fun security => 3 * secretWidth security + 1) + (fun security => ciphertextWidth security + 1) ∧ + Native S ∧ ChosenMessageSecure S := + GSWFHEBridge.leveled + (GSWFHEBridge.unframe_eq_of rfl rfl (fun _ => rfl) (fun _ _ => rfl)) + (GSWFHEBridge.dropFrame_eq_of rfl rfl (fun _ => rfl) (fun _ _ => rfl)) hLWE /-- **Fully homomorphic encryption from decision LWE and circular security** [Gentry2009, -Definition 2 and Section 2]. The self-loop scheme decrypts with GSW's decryption circuit, is -correct for every circuit, keeps GSW's widths, has native algorithms and is IND-CPA, assuming -decision LWE for this family and, separately, one-key circular security of GSW. -/ +Definition 2 and Section 2]. A scheme whose key generation is the self-loop key and which +encrypts and decrypts with GSW is correct for every circuit, keeps GSW's widths, decrypts with +polynomial-size circuits, has native algorithms and is IND-CPA, assuming decision LWE for this +family and, separately, one-key circular security of GSW. -/ theorem fullyHomomorphic (hLWE : DecisionLWE) (hcircular : CircularSecure) : - DecryptsWith fixedKeyScheme secretWidth ciphertextWidth decryptionCircuit ∧ - Cslib.PolynomiallyBounded (fun security => (decryptionCircuit security).size) ∧ + ∃ circuit : ∀ security, Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature + (secretWidth security + ciphertextWidth security) 1, + Cslib.PolynomiallyBounded (fun security => (circuit security).size) ∧ Cslib.PolynomiallyBounded secretWidth ∧ Cslib.PolynomiallyBounded ciphertextWidth ∧ - Homomorphic fixedKeyScheme (fun _ _ => True) ∧ - FixedWidths fixedKeyScheme (fun _ _ => True) secretWidth ciphertextWidth ∧ - Native fixedKeyScheme ∧ ChosenMessageSecure fixedKeyScheme := by - unfold fixedKeyScheme decryptionCircuit; exact GSWFHEBridge.fullyHomomorphic hLWE hcircular + ∃ S : Cslib.Crypto.Homomorphic.Scheme, + (∀ security, Cslib.ProbComp.eval (S.keyGen security) = selfLoopKeyGeneration security) ∧ + EncryptsAndDecrypts S selfLoopEncryption selfLoopDecryption ∧ + DecryptsWith S secretWidth ciphertextWidth circuit ∧ + Homomorphic S (fun _ _ => True) ∧ + FixedWidths S (fun _ _ => True) secretWidth ciphertextWidth ∧ + Native S ∧ ChosenMessageSecure S := + GSWFHEBridge.fullyHomomorphic + (GSWFHEBridge.unframe_eq_of rfl rfl (fun _ => rfl) (fun _ _ => rfl)) hLWE hcircular end ComplexityTests.Abstracts.GSWFHEAbstract /-- -info: abstract audit passed for `ComplexityTests.Abstracts.GSWFHEAbstract`: 41 root declarations, -593 dependencies checked +info: abstract audit passed for `ComplexityTests.Abstracts.GSWFHEAbstract`: 56 root declarations, +313 dependencies checked -/ #guard_msgs (whitespace := lax) in #check_abstract ComplexityTests.Abstracts.GSWFHEAbstract allowing [ -- shared foundations ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation, ComplexityAbstracts.Randomized, - -- the bit-encryption interface, GSW and its parameter family + -- the scheme record and randomized programs Complexity.Crypto.Computational.Homomorphic.Basic, - Complexity.Crypto.Computational.Homomorphic.GSW.Parameters, - Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters, - Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters.Scheme, - Complexity.Crypto.Computational.Homomorphic.GSW.Sampling.Serialized, - Complexity.Crypto.Computational.Homomorphic.GSW.Serialized, - Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Evaluation, - Complexity.Crypto.Computational.Homomorphic.GSW.CircuitEvaluation, - -- the logarithmic-depth decryption circuit - Complexity.Crypto.Computational.Homomorphic.GSW.DecryptionCircuit, - Complexity.Computability.Circuit.Balanced, - Complexity.Computability.Circuit.Boolean.CarryLookahead, - Complexity.Computability.Circuit.Boolean.CarrySave, - Complexity.Computability.Circuit.Boolean.CarrySave.Reduce, - Complexity.Computability.Circuit.Boolean.Formula, - Complexity.Computability.Circuit.Boolean.Gates, - Complexity.Computability.Circuit.Boolean.Modular.InnerProduct, - Complexity.Computability.Circuit.Boolean.Modular.Multiply, - Complexity.Computability.Circuit.Boolean.Modular.PartialProduct, - Complexity.Computability.Circuit.Boolean.Modular.Subtract, - Complexity.Computability.Circuit.Formula, - Complexity.Computability.Circuit.Parallel, - Complexity.Computability.Circuit.Pi, - Complexity.Foundations.Data.List.BalancedFold, - -- Gentry's bootstrapping constructions - Complexity.Crypto.Computational.Encryption.Circular, - Complexity.Crypto.Computational.Homomorphic.Circuit, - Complexity.Crypto.Computational.Homomorphic.Evaluation, - Complexity.Crypto.Computational.Homomorphic.FixedKey.Basic, - Complexity.Crypto.Computational.Homomorphic.FixedKey.Encoding, - Complexity.Crypto.Computational.Homomorphic.KeyChain, - Complexity.Crypto.Computational.Homomorphic.Layered, - Complexity.Crypto.Computational.Homomorphic.Leveled.Basic, - Complexity.Crypto.Computational.Homomorphic.Leveled.Encoding, - Complexity.Crypto.Computational.Homomorphic.Refresh, - -- circuit codes, depth and NAND layering - Complexity.Computability.Circuit.Boolean.DepthTime, + Complexity.Languages.Probabilistic.Basic, + -- the binary circuit code and the encodings it is assembled from Complexity.Computability.Circuit.Boolean.Encoding, - Complexity.Computability.Circuit.Boolean.EvaluationTime, - Complexity.Computability.Circuit.Boolean.Layered, - Complexity.Computability.Circuit.Boolean.Layered.Compile, - Complexity.Computability.Circuit.Boolean.Layered.Padding, - Complexity.Computability.Circuit.Depth, - -- binary encodings and decoders - Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree, - Complexity.Computability.Machines.Turing.MultiTape.Complexity.Primitives, Complexity.Computability.Machines.Turing.MultiTape.Encodings.Basic, - Complexity.Computability.Machines.Turing.MultiTape.Encodings.Decoder, + Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair, Complexity.Computability.Machines.Turing.MultiTape.Encodings.List, Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat, - Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair, - Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds.Degree, - Complexity.Foundations.Data.BitString.List, - Complexity.Foundations.Data.BitString.List.Binary, - Complexity.Foundations.Data.Matrix.Binary, - -- probabilistic programs and their samplers - Complexity.Languages.Probabilistic.Basic, - Complexity.Languages.Probabilistic.BitString, - Complexity.Languages.Probabilistic.CenteredBinomial, - Complexity.Languages.Probabilistic.Iteration, - Complexity.Languages.Probabilistic.Repeat, - Complexity.Languages.Probabilistic.UniformNat + Complexity.Computability.Machines.Turing.MultiTape.Complexity.Primitives ] diff --git a/abstracts/ComplexityAbstracts/GSWFHEBridge.lean b/abstracts/ComplexityAbstracts/GSWFHEBridge.lean index f915fd091..1d0a7b6e0 100644 --- a/abstracts/ComplexityAbstracts/GSWFHEBridge.lean +++ b/abstracts/ComplexityAbstracts/GSWFHEBridge.lean @@ -12,12 +12,16 @@ import Complexity.Crypto.Computational.Homomorphic.GSW.FullyHomomorphic /-! # Bridge for fully homomorphic encryption from GSW -The public abstract states the GSW laws, both assumptions and every claimed property in -elementary terms. This bridge identifies them with the library's serialized programs, its -decision-LWE and circular-security experiments, `Scheme.Correct`, `Scheme.FixedWidth`, native -certificates and `Encryption.INDCPA`, and assembles the leveled endpoint for every efficiently -computable budget from the generic bootstrapping lemmas. The bridge introduces no notation or -elaboration rules. +The public abstract states the GSW algorithms, both assumptions and every claimed property in +elementary terms, and asserts that suitable bootstrapping machinery exists. This bridge proves +that the library's constructions are such machinery: `leveled_witness` for +`Leveled.scheme GSW.DepthParameters.decryptionCircuits budget` and `fullyHomomorphic_witness` for +`FixedKey.scheme GSW.DepthParameters.decryptionCircuits`. It identifies their encryption, +decryption and fixed-key generation with the explicit GSW algorithms, identifies the assumptions +with the library's decision-LWE and circular-security experiments, and derives the elementary +properties from `Scheme.Correct`, `Scheme.FixedWidth`, the native certificates and +`Encryption.INDCPA`. The leveled endpoint is assembled for every efficiently computable budget +from the generic bootstrapping lemmas. The bridge introduces no notation or elaboration rules. -/ namespace ComplexityTests.Abstracts.GSWFHEBridge @@ -98,6 +102,18 @@ noncomputable def encryption (security : ℕ) (publicKey : List Bool) (message : return ciphertextWord (dimension security) (samples security) (width security) publicKey message coins +def decryption (security : ℕ) (secret ciphertext : List Bool) : Bool := + let n := dimension security + let w := width security + let value := (((matrixEntry (n + 1) w ciphertext (w - 1) 0 : ℤ) - + (((List.range n).map fun j => + matrixEntry (n + 1) w ciphertext (w - 1) (j + 1) * matrixEntry n w secret 0 j).sum : ℕ)) % + (2 ^ w : ℤ)).toNat + decide (2 ^ w ≤ 4 * value ∧ 4 * value < 3 * 2 ^ w) + +def decryptionWord (security : ℕ) (word : List Bool) : Bool := + decryption security (word.take (secretWidth security)) (word.drop (secretWidth security)) + noncomputable def uniformMatrixWord (m k w : ℕ) : PMF (List Bool) := (Cslib.Probability.PMF.uniformOfFintype (Fin m → Fin k → ZMod (2 ^ w))).map (fun A => (List.ofFn fun i => (List.ofFn fun j => lowBits w (A i j).val).flatten).flatten) @@ -118,6 +134,45 @@ noncomputable def selfEncryption (real : Bool) (security : ℕ) : PMF (List Bool def CircularSecure : Prop := Randomized.Indistinguishable (selfEncryption true) (selfEncryption false) +noncomputable def selfLoopKeyGeneration (security : ℕ) : PMF (List Bool × List Bool) := do + let keys ← keyGeneration security + let encryptedKey ← keys.2.mapM (encryption security keys.1) + return (Encoding.encPair Encoding.encBits (Encoding.encList Encoding.encBits) + (keys.1, encryptedKey), keys.2) + +/-! The abstract defines its framing decoders by recursion. Recursive definitions in two files +are not definitionally equal, so the definitions that read framed keys take the decoders as +parameters, and the theorems assume only that they agree with the library's decoders. -/ + +section Decoders + +variable (unframe dropFrame : List Bool → List Bool) + +noncomputable def leveledEncryption (security : ℕ) (publicKey : List Bool) (bit : Bool) : + PMF (List Bool) := + (encryption security (unframe (unframe publicKey)) bit).map (List.cons false) + +def leveledDecryption (security : ℕ) (secret ciphertext : List Bool) : Bool := + decryptionWord security + ((if ciphertext.headD false then dropFrame secret else unframe secret) ++ ciphertext.tail) + +noncomputable def selfLoopEncryption (security : ℕ) (publicKey : List Bool) (bit : Bool) : + PMF (List Bool) := + encryption security (unframe publicKey) bit + +end Decoders + +def selfLoopDecryption (security : ℕ) (secret ciphertext : List Bool) : Bool := + decryptionWord security (secret ++ ciphertext) + +def EncryptsAndDecrypts (S : Homomorphic.Scheme) + (encrypt : ℕ → List Bool → Bool → PMF (List Bool)) + (decrypt : ℕ → List Bool → List Bool → Bool) : Prop := + (∀ security publicKey bit, + ProbComp.eval (S.encrypt security publicKey bit) = encrypt security publicKey bit) ∧ + ∀ security secret ciphertext, S.decrypt security secret ciphertext = + decrypt security secret ciphertext + def Homomorphic (S : Homomorphic.Scheme) (allowed : ℕ → (Σ k, Circuits.Circuit Circuits.Boolean.signature k 1) → Prop) : Prop := ∀ security keys, keys ∈ (ProbComp.eval (S.keyGen security)).support → @@ -191,6 +246,44 @@ def ChosenMessageSecure (S : Homomorphic.Scheme) : Prop := nndist (Randomized.probability (chosenMessageGame S choose guess false security)) (Randomized.probability (chosenMessageGame S choose guess true security))) +/-! ### The framing decoders -/ + +/-- A function with the defining equations of the abstract's `unframe` is the library's +`unframe`. -/ +theorem unframe_eq_of {unframe : List Bool → List Bool} (hnil : unframe [] = []) + (hone : unframe [true] = []) (hfalse : ∀ rest, unframe (false :: rest) = []) + (hpair : ∀ b rest, unframe (true :: b :: rest) = b :: unframe rest) : + ∀ word, unframe word = Turing.MultiTapeTM.unframe word + | [] => hnil + | [true] => hone + | false :: rest => hfalse rest + | true :: b :: rest => by + rw [hpair, unframe_eq_of hnil hone hfalse hpair rest] + rfl + +/-- A function with the defining equations of the abstract's `dropFrame` is the library's +`dropFrame`. -/ +theorem dropFrame_eq_of {dropFrame : List Bool → List Bool} (hnil : dropFrame [] = []) + (hone : dropFrame [true] = []) (hfalse : ∀ rest, dropFrame (false :: rest) = rest) + (hpair : ∀ b rest, dropFrame (true :: b :: rest) = dropFrame rest) : + ∀ word, dropFrame word = Turing.MultiTapeTM.dropFrame word + | [] => hnil + | [true] => hone + | false :: rest => hfalse rest + | true :: b :: rest => by + rw [hpair, dropFrame_eq_of hnil hone hfalse hpair rest] + rfl + +/-- The first framed word of a list of framed words, or the empty word if there is none. -/ +private theorem getD_frames (word : List Bool) : + ((frames word).map Decoder.bits.decode).getD 0 [] = Turing.MultiTapeTM.unframe word := by + by_cases h : word = [] + · subst h + rw [frames_nil] + rfl + · rw [frames_of_ne_nil h] + rfl + /-! ### The GSW laws are the library's serialized programs -/ private theorem independentList_eval {α : Type} (count : ℕ) (program : ProbComp α) : @@ -224,7 +317,7 @@ private theorem encryption_eq (security : ℕ) (publicKey : List Bool) (message PMF.monad_pure_eq_pure] rfl -/-- The named GSW key generation and encryption have exactly the explicit laws. -/ +/-- The library's GSW key generation and encryption have exactly the explicit laws. -/ theorem base_scheme (security : ℕ) : ProbComp.eval (GSW.DepthParameters.scheme.keyGen security) = keyGeneration security ∧ ∀ publicKey message, @@ -233,6 +326,81 @@ theorem base_scheme (security : ℕ) : ⟨(keyGeneration_eq security).symm, fun publicKey message => (encryption_eq security publicKey message).symm⟩ +/-- Serialized decryption reads only the first `n w` secret bits and the first `N²` ciphertext +bits, with missing bits read as `false`. -/ +private theorem decryptSerialized_congr {n w : ℕ} + {secret secret' ciphertext ciphertext' : List Bool} + (hsecret : ∀ i < n * w, secret.getD i false = secret'.getD i false) + (hciphertext : ∀ i < (n + 1) * w * ((n + 1) * w), + ciphertext.getD i false = ciphertext'.getD i false) : + GSW.decryptSerialized n w secret ciphertext = + GSW.decryptSerialized n w secret' ciphertext' := by + have hs : Cslib.Matrix.ofBinary 1 n w secret = Cslib.Matrix.ofBinary 1 n w secret' := by + have h : BitString.ofList (1 * (n * w)) secret = BitString.ofList (1 * (n * w)) secret' := by + funext i + exact hsecret i (by have := i.2; omega) + unfold Cslib.Matrix.ofBinary + rw [h] + have hc : GSW.decodeCiphertext n w ciphertext = GSW.decodeCiphertext n w ciphertext' := by + have h : BitString.ofList ((n + 1) * (w * ((n + 1) * w))) ciphertext = + BitString.ofList ((n + 1) * (w * ((n + 1) * w))) ciphertext' := by + funext i + exact hciphertext i (by have := i.2; rwa [Nat.mul_assoc]) + unfold GSW.decodeCiphertext + rw [h] + rw [GSW.decryptSerialized_eq, GSW.decryptSerialized_eq, GSW.decodeSecret, GSW.decodeSecret, + hs, hc] + +/-- **The decryption circuit computes `decryptionWord` on every word.** The circuit reads the +word padded with `false` or truncated to its input width, and GSW decryption ignores the bits +beyond its widths. -/ +theorem eval_decryptionCircuit (security : ℕ) (word : List Bool) : + (GSW.DepthParameters.decryptionCircuits.circuit security).eval Circuits.Boolean.interpretation + (BitString.ofList (GSW.DepthParameters.secretWidth security + + GSW.DepthParameters.ciphertextWidth security) word) 0 = + decryptionWord security word := by + have hsw : GSW.DepthParameters.secretWidth security = secretWidth security := rfl + have hcw : GSW.DepthParameters.ciphertextWidth security = + (dimension security + 1) * width security * ((dimension security + 1) * width security) := + rfl + obtain ⟨full, hfull⟩ : ∃ full, full = List.ofFn (BitString.ofList + (GSW.DepthParameters.secretWidth security + GSW.DepthParameters.ciphertextWidth security) + word) := ⟨_, rfl⟩ + have hlength : full.length = + GSW.DepthParameters.secretWidth security + GSW.DepthParameters.ciphertextWidth security := by + rw [hfull, List.length_ofFn] + have hget : ∀ i < GSW.DepthParameters.secretWidth security + + GSW.DepthParameters.ciphertextWidth security, full[i]? = word[i]?.getD false := by + intro i hi + rw [List.getElem?_eq_getElem (by rw [hlength]; exact hi)] + simp only [hfull, List.getElem_ofFn, BitString.ofList, List.getD_eq_getElem?_getD] + have hsplit : BitString.ofList + (GSW.DepthParameters.secretWidth security + GSW.DepthParameters.ciphertextWidth security) + word = BitString.ofList + (GSW.DepthParameters.secretWidth security + GSW.DepthParameters.ciphertextWidth security) + (full.take (GSW.DepthParameters.secretWidth security) ++ + full.drop (GSW.DepthParameters.secretWidth security)) := by + rw [List.take_append_drop, hfull, BitString.ofList_ofFn] + rw [hsplit, GSW.DepthParameters.decryptionCircuits.correct security _ _ + (by rw [List.length_take, hlength]; omega) (by rw [List.length_drop, hlength]; omega)] + change GSW.decryptSerialized (dimension security) (width security) _ _ = + decryption security (word.take (secretWidth security)) (word.drop (secretWidth security)) + rw [decryptSerialized_congr (secret' := word.take (secretWidth security)) + (ciphertext' := word.drop (secretWidth security))] + · have hw : width security ≠ 0 := (GSW.DepthParameters.width_pos security).ne' + unfold GSW.decryptSerialized + simp only [hw, ite_false] + rfl + · intro i hi + have hi' : i < secretWidth security := hi + simp only [List.getD_eq_getElem?_getD, + List.getElem?_take_of_lt (show i < GSW.DepthParameters.secretWidth security from hi'), + List.getElem?_take_of_lt hi', hget i (by rw [hsw]; omega), Option.getD_some] + · intro i hi + simp only [List.getD_eq_getElem?_getD, List.getElem?_drop] + rw [hget _ (by rw [hsw, hcw]; omega), Option.getD_some] + rfl + /-! ### The two assumptions -/ private theorem uniformMatrixWord_eq (m k w : ℕ) : @@ -248,6 +416,7 @@ private theorem uniformPublic_eq (security : ℕ) : uniformPublic security = LWE.uniformEnsemble dimension samples width security := uniformMatrixWord_eq _ _ _ +/-- The elementary decision-LWE assumption is the library's, for this family. -/ theorem decisionLWE_iff : DecisionLWE ↔ Crypto.DecisionLWE GSW.Parameters.dimension GSW.DepthParameters.samples GSW.DepthParameters.width @@ -273,20 +442,23 @@ private theorem mapM_eval {α β : Type} (program : α → ProbComp β) (inputs simp only [List.mapM_cons, ProbComp.eval_bind, ProbComp.eval_pure, ih, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure] +private theorem encryption_fun_eq (security : ℕ) : encryption security = + fun publicKey message => + ProbComp.eval (GSW.DepthParameters.scheme.encrypt security publicKey message) := by + funext publicKey message + exact encryption_eq security publicKey message + private theorem selfEncryption_eq (real : Bool) (security : ℕ) : selfEncryption real security = (ProbComp.eval (Encryption.circularPublicKey GSW.DepthParameters.scheme.keyGen GSW.DepthParameters.scheme.encrypt real security)).map Encryption.encCircularPublicKey := by - have hencrypt : encryption security = fun publicKey message => - ProbComp.eval (GSW.DepthParameters.scheme.encrypt security publicKey message) := by - funext publicKey message - exact encryption_eq security publicKey message - simp only [selfEncryption, Encryption.circularPublicKey, hencrypt, mapM_eval, + simp only [selfEncryption, Encryption.circularPublicKey, encryption_fun_eq, mapM_eval, ProbComp.eval_bind, ProbComp.eval_pure, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.map_bind, PMF.pure_map, (base_scheme security).1] rfl +/-- The elementary circular-security assumption is the library's, for GSW at this family. -/ theorem circularSecure_iff : CircularSecure ↔ Encryption.CircularSecure GSW.DepthParameters.scheme.keyGen GSW.DepthParameters.scheme.encrypt := by @@ -300,7 +472,52 @@ theorem circularSecure_iff : CircularSecure ↔ rw [h true, h false] rfl -/-! ### The claimed properties from the library's notions -/ +/-! ### The library's bootstrapped schemes use the explicit algorithms -/ + +/-- The library's leveled scheme, for every budget, encrypts with a tag and GSW encryption under +the chain's first public key, and decrypts with the tag-selected endpoint secret. -/ +theorem leveled_encryptsAndDecrypts (budget : ℕ → ℕ) : + EncryptsAndDecrypts (Leveled.scheme GSW.DepthParameters.decryptionCircuits budget) + (leveledEncryption Turing.MultiTapeTM.unframe) + (leveledDecryption Turing.MultiTapeTM.unframe Turing.MultiTapeTM.dropFrame) := by + refine ⟨fun security publicKey bit => ?_, fun security secret ciphertext => ?_⟩ + · have hkey : (Leveled.publicKeyDecoder.decode publicKey).1.getD 0 [] = + Turing.MultiTapeTM.unframe (Turing.MultiTapeTM.unframe publicKey) := + getD_frames _ + change ProbComp.eval (List.cons false <$> GSW.DepthParameters.scheme.encrypt security + ((Leveled.publicKeyDecoder.decode publicKey).1.getD 0 []) bit) = _ + rw [ProbComp.eval_map, (base_scheme security).2, hkey] + rfl + · have hkey : Leveled.secretKeyDecoder.decode secret = + (Turing.MultiTapeTM.unframe secret, Turing.MultiTapeTM.dropFrame secret) := rfl + simp only [Leveled.scheme, Leveled.decrypt, hkey, eval_decryptionCircuit] + rfl + +/-- The library's fixed-key key generation is the self-loop key generation. -/ +theorem fixedKey_keyGen (security : ℕ) : + ProbComp.eval ((FixedKey.scheme GSW.DepthParameters.decryptionCircuits).keyGen security) = + selfLoopKeyGeneration security := by + simp only [FixedKey.scheme, FixedKey.keyGen, Scheme.encryptBits, selfLoopKeyGeneration, + encryption_fun_eq, mapM_eval, ProbComp.eval_bind, ProbComp.eval_pure, + PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, (base_scheme security).1] + rfl + +/-- The library's fixed-key scheme encrypts with GSW under the first framed component of its +public key and decrypts with GSW on the concatenated key and ciphertext. -/ +theorem fixedKey_encryptsAndDecrypts : + EncryptsAndDecrypts (FixedKey.scheme GSW.DepthParameters.decryptionCircuits) + (selfLoopEncryption Turing.MultiTapeTM.unframe) selfLoopDecryption := by + refine ⟨fun security publicKey bit => ?_, fun security secret ciphertext => ?_⟩ + · change ProbComp.eval (GSW.DepthParameters.scheme.encrypt security + (FixedKey.publicKeyDecoder.decode publicKey).1 bit) = _ + rw [(base_scheme security).2] + rfl + · simp only [FixedKey.scheme, FixedKey.decrypt, selfLoopDecryption, eval_decryptionCircuit] + +/-! ### The claimed properties from the library's notions + +Each lemma proves the direction the conclusions need: the library's notion implies the +elementary one. -/ theorem homomorphic_of_correct {S : Homomorphic.Scheme} (hS : S.Correct) {allowed : ℕ → (Σ k, Circuits.Circuit Circuits.Boolean.signature k 1) → Prop} @@ -352,15 +569,22 @@ theorem chosenMessageSecure_of_indCPA {S : Homomorphic.Scheme} Asymptotics.SuperpolynomialDecay, Crypto.Game.advantage, Crypto.Game.succProbability, Randomized.probability] using h -/-! ### The headline theorems -/ +/-! ### Provenance: the library's schemes are the witnesses -/ -theorem leveled (hLWE : DecisionLWE) : +/-- **The library's leveled scheme witnesses `leveled`.** For every budget computable in unary +polynomial time, `Leveled.scheme GSW.DepthParameters.decryptionCircuits budget` has every +property that the abstract's `leveled` asserts, with one decryption circuit family chosen +before the budget. -/ +theorem leveled_witness (hLWE : DecisionLWE) : ∃ circuit : ∀ security, Circuits.Circuit Circuits.Boolean.signature ((3 * secretWidth security + 1) + (ciphertextWidth security + 1)) 1, PolynomiallyBounded (fun security => (circuit security).size) ∧ PolynomiallyBounded (fun security => 3 * secretWidth security + 1) ∧ PolynomiallyBounded (fun security => ciphertextWidth security + 1) ∧ ∀ budget : ℕ → ℕ, Computation.PolyTime budget Encoding.encUnary Encoding.encUnary → + EncryptsAndDecrypts (Leveled.scheme GSW.DepthParameters.decryptionCircuits budget) + (leveledEncryption Turing.MultiTapeTM.unframe) + (leveledDecryption Turing.MultiTapeTM.unframe Turing.MultiTapeTM.dropFrame) ∧ DecryptsWith (Leveled.scheme GSW.DepthParameters.decryptionCircuits budget) (fun security => 3 * secretWidth security + 1) (fun security => ciphertextWidth security + 1) circuit ∧ @@ -386,7 +610,7 @@ theorem leveled (hLWE : DecisionLWE) : Leveled.correct_fixedWidth_indCPA D GSW.DepthParameters.correct GSW.DepthParameters.fixedWidth GSW.DepthParameters.bootstrappable (GSW.DepthParameters.indCPA_scheme (decisionLWE_iff.mp hLWE)) hkeyGen hencrypt hD hb - exact ⟨fun security => hcircuits budget security, + exact ⟨leveled_encryptsAndDecrypts budget, fun security => hcircuits budget security, homomorphic_of_correct hcorrect fun _ _ h => h, fixedWidths_of_fixedWidth hwidth fun _ _ h => h, native_of (Leveled.isPPTOn_scheme_keyGen hkeyGen hencrypt D budget hb) @@ -395,12 +619,19 @@ theorem leveled (hLWE : DecisionLWE) : (Leveled.isPPTOn_scheme_evaluate hencrypt D hD hevaluate budget hb), chosenMessageSecure_of_indCPA hsecure⟩ -theorem fullyHomomorphic (hLWE : DecisionLWE) (hcircular : CircularSecure) : - DecryptsWith (FixedKey.scheme GSW.DepthParameters.decryptionCircuits) secretWidth - ciphertextWidth GSW.DepthParameters.decryptionCircuits.circuit ∧ - PolynomiallyBounded +/-- **The library's fixed-key scheme witnesses `fullyHomomorphic`**, with GSW's own decryption +circuits `GSW.DepthParameters.decryptionCircuits.circuit`. -/ +theorem fullyHomomorphic_witness (hLWE : DecisionLWE) (hcircular : CircularSecure) : + PolynomiallyBounded (fun security => (GSW.DepthParameters.decryptionCircuits.circuit security).size) ∧ PolynomiallyBounded secretWidth ∧ PolynomiallyBounded ciphertextWidth ∧ + (∀ security, ProbComp.eval + ((FixedKey.scheme GSW.DepthParameters.decryptionCircuits).keyGen security) = + selfLoopKeyGeneration security) ∧ + EncryptsAndDecrypts (FixedKey.scheme GSW.DepthParameters.decryptionCircuits) + (selfLoopEncryption Turing.MultiTapeTM.unframe) selfLoopDecryption ∧ + DecryptsWith (FixedKey.scheme GSW.DepthParameters.decryptionCircuits) secretWidth + ciphertextWidth GSW.DepthParameters.decryptionCircuits.circuit ∧ Homomorphic (FixedKey.scheme GSW.DepthParameters.decryptionCircuits) (fun _ _ => True) ∧ FixedWidths (FixedKey.scheme GSW.DepthParameters.decryptionCircuits) (fun _ _ => True) secretWidth ciphertextWidth ∧ @@ -410,10 +641,58 @@ theorem fullyHomomorphic (hLWE : DecisionLWE) (hcircular : CircularSecure) : hdecrypt, hevaluate, hsecure⟩ := GSW.DepthParameters.fullyHomomorphic_of_decisionLWE_of_circularSecure (decisionLWE_iff.mp hLWE) (circularSecure_iff.mp hcircular) - exact ⟨(FixedKey.decryptionCircuits GSW.DepthParameters.decryptionCircuits).correct, hsize, - hsecret, hciphertext, + exact ⟨hsize, hsecret, hciphertext, fixedKey_keyGen, fixedKey_encryptsAndDecrypts, + (FixedKey.decryptionCircuits GSW.DepthParameters.decryptionCircuits).correct, homomorphic_of_correct hcorrect fun security C _ => hpermitted security C, fixedWidths_of_fixedWidth hwidth fun security C _ => hpermitted security C, native_of hkeyGen hencrypt hdecrypt hevaluate, chosenMessageSecure_of_indCPA hsecure⟩ +/-! ### The headline theorems + +The decoders are those of the abstract; they agree with the library's on every word. -/ + +theorem leveled {unframe dropFrame : List Bool → List Bool} + (hunframe : ∀ word, unframe word = Turing.MultiTapeTM.unframe word) + (hdropFrame : ∀ word, dropFrame word = Turing.MultiTapeTM.dropFrame word) + (hLWE : DecisionLWE) : + ∃ circuit : ∀ security, Circuits.Circuit Circuits.Boolean.signature + ((3 * secretWidth security + 1) + (ciphertextWidth security + 1)) 1, + PolynomiallyBounded (fun security => (circuit security).size) ∧ + PolynomiallyBounded (fun security => 3 * secretWidth security + 1) ∧ + PolynomiallyBounded (fun security => ciphertextWidth security + 1) ∧ + ∀ budget : ℕ → ℕ, Computation.PolyTime budget Encoding.encUnary Encoding.encUnary → + ∃ S : Homomorphic.Scheme, + EncryptsAndDecrypts S (leveledEncryption unframe) + (leveledDecryption unframe dropFrame) ∧ + DecryptsWith S (fun security => 3 * secretWidth security + 1) + (fun security => ciphertextWidth security + 1) circuit ∧ + Homomorphic S (fun security C => C.2.depth ≤ budget security) ∧ + FixedWidths S (fun security C => C.2.depth ≤ budget security) + (fun security => 3 * secretWidth security + 1) + (fun security => ciphertextWidth security + 1) ∧ + Native S ∧ ChosenMessageSecure S := by + obtain rfl : unframe = Turing.MultiTapeTM.unframe := funext hunframe + obtain rfl : dropFrame = Turing.MultiTapeTM.dropFrame := funext hdropFrame + obtain ⟨circuit, hsize, hsecret, hciphertext, h⟩ := leveled_witness hLWE + exact ⟨circuit, hsize, hsecret, hciphertext, fun budget hbudget => + ⟨_, h budget hbudget⟩⟩ + +theorem fullyHomomorphic {unframe : List Bool → List Bool} + (hunframe : ∀ word, unframe word = Turing.MultiTapeTM.unframe word) + (hLWE : DecisionLWE) (hcircular : CircularSecure) : + ∃ circuit : ∀ security, Circuits.Circuit Circuits.Boolean.signature + (secretWidth security + ciphertextWidth security) 1, + PolynomiallyBounded (fun security => (circuit security).size) ∧ + PolynomiallyBounded secretWidth ∧ PolynomiallyBounded ciphertextWidth ∧ + ∃ S : Homomorphic.Scheme, + (∀ security, ProbComp.eval (S.keyGen security) = selfLoopKeyGeneration security) ∧ + EncryptsAndDecrypts S (selfLoopEncryption unframe) selfLoopDecryption ∧ + DecryptsWith S secretWidth ciphertextWidth circuit ∧ + Homomorphic S (fun _ _ => True) ∧ + FixedWidths S (fun _ _ => True) secretWidth ciphertextWidth ∧ + Native S ∧ ChosenMessageSecure S := by + obtain rfl : unframe = Turing.MultiTapeTM.unframe := funext hunframe + obtain ⟨hsize, hsecret, hciphertext, h⟩ := fullyHomomorphic_witness hLWE hcircular + exact ⟨_, hsize, hsecret, hciphertext, _, h⟩ + end ComplexityTests.Abstracts.GSWFHEBridge diff --git a/abstracts/README.md b/abstracts/README.md index 40603857e..e7931ab16 100644 --- a/abstracts/README.md +++ b/abstracts/README.md @@ -4,10 +4,7 @@ The catalogue promotes seventeen major result groups. Each has a checked Lean ab definitions needed to understand its statement, a bridge to the library proof, and an audited dependency boundary. Some abstracts also allowlist a few library modules for foundational models (for example circuit signatures or oracle runs); each such abstract names them in its docstring, and -a reader must inspect them as well. The fully homomorphic encryption abstract is the exception to -"a few": it names the library's construction instead of restating it, so it allowlists the modules -that define the construction, while stating both assumptions and every claimed property itself. -The generated PDFs present the mathematical definitions and +a reader must inspect them as well. The generated PDFs present the mathematical definitions and selected statements first, followed by exact representation details and any shared foundations in appendices. Proof bodies are omitted. Lean checks the proofs; independent review must still check their intended meaning. @@ -47,7 +44,7 @@ former paper/TeX index is retired; Git history retains its sources. | [Håstad and Razborov–Smolensky: parity resists shallow circuits](ComplexityAbstracts/ConstantDepthAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/constant-depth.pdf) | Explicit finite bounds, gate semantics and depth conventions; nonuniform lower bounds. | | [Formula lower bounds: parity and Andreev](ComplexityAbstracts/FormulaBoundsAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/formula-bounds.pdf) | De Morgan formulas, literal leaves, explicit block indexing and finite quantitative bounds; no general-circuit lower bound. | | [One-way functions yield pseudorandom generators and adaptive functions](ComplexityAbstracts/CryptographyAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/cryptography.pdf) | Uniform probabilistic polynomial time with explicit native evaluators, negligible advantage and full stateful oracle semantics; asymptotic security, not a concrete implementation audit. | -| [Gentry and GSW: fully homomorphic encryption from LWE](ComplexityAbstracts/GSWFHEAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/gsw-fhe.pdf) | The named construction at an explicit LWE family with quasi-polynomial modulus; correctness, fixed widths, polynomial-size decryption circuits, native algorithms and IND-CPA, with circular security as a separate hypothesis. | +| [Gentry and GSW: fully homomorphic encryption from LWE](ComplexityAbstracts/GSWFHEAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/gsw-fhe.pdf) | Explicit GSW algorithms at an LWE family with quasi-polynomial modulus and Gentry's self-loop key; an existential evaluator, key chain and decryption circuits with correctness, fixed widths, polynomial-size decryption circuits, native algorithms and IND-CPA; circular security as a separate hypothesis. | | [Haken: pigeonhole formulas require long resolution proofs](ComplexityAbstracts/ResolutionAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/resolution.pdf) | The non-onto pigeonhole formula and a line-based resolution rule, with bound 2^(floor(n/24)); proof size is not solver runtime. | | [Communication: disjointness and inner product resist randomness](ComplexityAbstracts/CommunicationAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/communication.pdf) | Shared randomness, per-input error at most one third and explicit linear bounds; exact deterministic equality records the final-answer convention. | | [Sipser–Gács–Lautemann: BPP lies in the second polynomial level](ComplexityAbstracts/SipserLautemannAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/sipser-lautemann.pdf) | Fair random bits, explicit quantifier blocks and total native polynomial-time tests. | diff --git a/abstracts/catalogue.json b/abstracts/catalogue.json index 3a1b5a9ed..2627bfb65 100644 --- a/abstracts/catalogue.json +++ b/abstracts/catalogue.json @@ -169,11 +169,8 @@ "ComplexityTests.Abstracts.GSWFHEAbstract.leveled", "ComplexityTests.Abstracts.GSWFHEAbstract.fullyHomomorphic" ], - "supporting_theorems": [ - "ComplexityTests.Abstracts.GSWFHEAbstract.base_scheme" - ], "summary": "Bootstrapping the GSW scheme gives leveled fully homomorphic encryption from decision LWE, and fully homomorphic encryption under an additional circular-security assumption.", - "scope": "The named library construction at an explicit centered-binomial LWE family with quasi-polynomial modulus; perfect correctness on fresh encryptions, fixed widths, polynomial-size decryption circuits, native strict PPT algorithms and asymptotic IND-CPA. Circular security is a separate hypothesis; no lattice hardness, circuit privacy, multi-hop evaluation or concrete loss.", + "scope": "Explicit GSW key generation, encryption and decryption at a centered-binomial LWE family with quasi-polynomial modulus, and Gentry's self-loop key; the evaluator, the leveled key chain and the decryption circuits are existential. Perfect correctness on fresh encryptions, fixed widths, polynomial-size decryption circuits, native strict PPT algorithms and asymptotic IND-CPA. Circular security is a separate hypothesis; no lattice hardness, circuit privacy, multi-hop evaluation or concrete loss.", "namespace": "ComplexityTests.Abstracts.GSWFHEAbstract", "foundations": [ "ComplexityAbstracts.Encoding", From 84e61cd37b9bf9cd6cc16706c8d1755016e5deee Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 25 Oct 2026 15:25:25 -0400 Subject: [PATCH 3/3] fix(abstracts): pin the leveled fresh-ciphertext key law in the FHE abstract (#486) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rebased onto main after #671, which moved `frame`, `encNat` and `encUnary`. The `#check_abstract` allowlist now names `Encodings.Frame.Basic`, `Encodings.Nat.Bits` and `Encodings.Unary` in place of `Encodings.Basic`, `Encodings.Nat` and `Complexity.Primitives`; the closure is exactly these eight library modules plus the three shared foundations, and the audit message is unchanged. `leveled` now also states that the key pair read from the first framed words of the keys, which fresh encryption and decryption use, has the law `keyGeneration`. The bridge proves it in `leveled_keyGen`: the library's leveled key generation publishes the first pair of the replicated base key generation, sampled before the links, and `base_scheme` gives its law. Only this marginal law is fixed; the later keys and links stay existential, as the docstrings and catalogue scope now say. Also reword the `fullyHomomorphic` docstring as an existential claim, and record that GSW writes `ℓ = ⌊log q⌋ + 1 = w + 1` bits per coefficient where the abstract writes `w`, which drops only the zero top digit. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../ComplexityAbstracts/GSWFHEAbstract.lean | 97 +++++++++++-------- .../ComplexityAbstracts/GSWFHEBridge.lean | 44 +++++++-- abstracts/README.md | 2 +- abstracts/catalogue.json | 2 +- 4 files changed, 96 insertions(+), 49 deletions(-) diff --git a/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean b/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean index a57a44430..f002401d2 100644 --- a/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean +++ b/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean @@ -25,21 +25,24 @@ indistinguishable from an encryption of zeros. **The core is written out.** GSW key generation, encryption and decryption at the parameter family are stated below as explicit algorithms, and both assumptions are stated on them. The leveled scheme of `leveled` encrypts and decrypts exactly with these algorithms behind a one-bit -tag and a framed pair of secret keys. The fully homomorphic scheme of `fullyHomomorphic` encrypts -and decrypts exactly with them, and its key generation is exactly Gentry's self-loop key: a GSW -key pair together with encryptions of its secret-key bits under its own public key. - -**Only the bootstrapping machinery is existential:** homomorphic evaluation, the leveled scheme's -key chain and the polynomial-size decryption circuits. The theorems state that such machinery -exists with elementary properties: correctness for the allowed circuits, fixed key and ciphertext -widths, one decryption circuit family for all depths, native efficiency and IND-CPA security. -These properties exclude trivial witnesses. Decryption is the fixed GSW decryption, and -evaluated ciphertexts have the fixed ciphertext width, so evaluation cannot leave the computation -to decryption: it must output a word of that width that GSW decryption maps to the circuit's -output. Nor can evaluation work in the clear. Evaluation is efficient and accepts the challenge -ciphertext of the IND-CPA game, so if the public key revealed the secret key that decrypts -evaluated ciphertexts, an adversary could evaluate a depth-zero circuit, whose output is its -input, on the challenge and read the hidden bit. +tag and a framed pair of secret keys, and the key pair for fresh ciphertexts, read from the first +framed words of its keys, has exactly the GSW key-generation law. The fully homomorphic scheme of +`fullyHomomorphic` encrypts and decrypts exactly with them, and its key generation is exactly +Gentry's self-loop key: a GSW key pair together with encryptions of its secret-key bits under its +own public key. + +**Only the bootstrapping machinery is existential:** homomorphic evaluation, the rest of the leveled +scheme's keys and the polynomial-size decryption circuits. For `leveled` only the marginal law of +the fresh-ciphertext key pair is fixed; the later keys of the chain, the encrypted links and their +joint law with that pair are not. The theorems state that such machinery exists with elementary +properties: correctness for the allowed circuits, fixed key and ciphertext widths, one decryption +circuit family for all depths, native efficiency and IND-CPA security. These properties exclude +trivial witnesses. Decryption is the fixed GSW decryption, and evaluated ciphertexts have the fixed +ciphertext width, so evaluation cannot leave the computation to decryption: it must output a word of +that width that GSW decryption maps to the circuit's output. Nor can evaluation work in the clear. +Evaluation is efficient and accepts the challenge ciphertext of the IND-CPA game, so if the public +key revealed the secret key that decrypts evaluated ciphertexts, an adversary could evaluate a +depth-zero circuit, whose output is its input, on the challenge and read the hidden bit. **Provenance (not part of the checked statements).** The library's constructions witness both theorems. In the namespace `Cslib.Crypto.Homomorphic`, write `D` for GSW's decryption circuits @@ -60,9 +63,9 @@ each a foundational model: `Cslib.Circuits.Boolean.encCircuit`, the input format of native evaluation, explained before `Native`. * Under `Computability.Machines.Turing.MultiTape`, the encodings from which that code is - assembled: framing (`Encodings.Basic`), pairs (`Encodings.Pair`), lists (`Encodings.List`), - binary numbers (`Encodings.Nat`), and unary numbers, `n` written as `n` ones - (`Complexity.Primitives`; only `encUnary` is reached there, and no tidy notion is). + assembled: framing (`Encodings.Frame.Basic`), pairs (`Encodings.Pair`), lists + (`Encodings.List`), binary numbers (`Encodings.Nat.Bits`), and unary numbers, `n` written as + `n` ones (`Encodings.Unary`). Lean checks every proof through `GSWFHEBridge`. The claims are perfect correctness on supported fresh encryptions, fixed key and ciphertext @@ -115,10 +118,15 @@ def ciphertextWidth (security : ℕ) : ℕ := rows security * rows security /-! ## Representation details -Residues modulo `2 ^ w` are written with exactly `w` bits, least significant first. A public key -is the matrix `[B t + e | B]` in row-major order, its noisy column first; a secret key lists the -residues of `t`; a ciphertext lists every bit of `μ G + R A`, its rows indexed by `(i, k)` and its -columns by `(j, l)`. These words are the actual inputs and outputs of the native algorithms. +Residues modulo `2 ^ w` are written with exactly `w` bits, least significant first. GSW writes each +coefficient with `ℓ` bits, one more than the floor of `log q` [GentrySahaiWaters2013, Section 3.1], +which is `w + 1` for `q = 2 ^ w`, so its `N` is `(n + 1)(w + 1)`. This file omits the top digit +position, whose power of two `2 ^ w` is zero modulo `q` and whose bit is zero in every canonical +residue; decryption reads the same row in both layouts, the one whose gadget coefficient +`2 ^ (w - 1)` lies in `(q / 4, q / 2]`. A public key is the matrix `[B t + e | B]` in row-major +order, its noisy column first; a secret key lists the residues of `t`; a ciphertext lists every +bit of `μ G + R A`, its rows indexed by `(i, k)` and its columns by `(j, l)`. These words are the +actual inputs and outputs of the native algorithms. Keys of the bootstrapped schemes are framed words (`Encoding.frame` in the shared foundations). `unframe` reads the first framed word and `dropFrame` returns what follows it; both are defined @@ -464,20 +472,25 @@ def ChosenMessageSecure (S : Cslib.Crypto.Homomorphic.Scheme) : Prop := `Cslib.PolynomiallyBounded f` means that a fixed power bounds `f` eventually: some `d` has `f security ≤ security ^ d` for all large `security`. -Gentry's Definition 3 asks for one decryption circuit shared by all depths, correctness for -every circuit up to the depth, and algorithms polynomial in the parameter and the depth -[Gentry2009, Definition 3]. In `leveled`, one polynomial-size circuit family is chosen first. -Then for every depth budget computable in unary polynomial time, a scheme exists that encrypts -and decrypts with the leveled algorithms above, decrypts with this circuit family, is correct for -every circuit of depth at most the budget, has fixed polynomial widths, native algorithms and -IND-CPA security. Any polynomially bounded depth `d(security) ≤ c (security + 1) ^ e` is covered -by the budget `c (security + 1) ^ e`. The runtime polynomial may depend on the budget function, -so it need not be one polynomial in the parameter and the depth. +Gentry's Definition 3 asks for one decryption circuit shared by all depths, correctness for every +circuit up to the depth, and algorithms polynomial in the parameter and the depth [Gentry2009, +Definition 3]. In `leveled`, one polynomial-size circuit family is chosen first. Then for every +depth budget computable in unary polynomial time, a scheme exists whose key pair for fresh +ciphertexts has the GSW key-generation law, that encrypts and decrypts with the leveled algorithms +above, decrypts with this circuit family, is correct for every circuit of depth at most the budget, +has fixed polynomial widths, native algorithms and IND-CPA security. Any polynomially bounded depth +`d(security) ≤ c (security + 1) ^ e` is covered by the budget `c (security + 1) ^ e`. The runtime +polynomial may depend on the budget function, so it need not be one polynomial in the parameter and +the depth. -/ -/-- **Leveled fully homomorphic encryption from decision LWE** [Gentry2009, Theorem 3]. Only the -decision-LWE assumption for this family is used; there is no circular-security assumption. -IND-CPA is the asymptotic consequence of [Gentry2009, Theorem 4], without its exact loss. -/ +/-- **Leveled fully homomorphic encryption from decision LWE** [Gentry2009, Theorem 3]. In each +scheme, the first framed word of the first framed component of the public key and the first +framed word of the secret key, the key pair under which fresh bits are encrypted and decrypted, +are jointly distributed as `keyGeneration`. Only this marginal law is fixed; the rest of the key +is not. Only the decision-LWE assumption for this family is used; there is no circular-security +assumption. IND-CPA is the asymptotic consequence of [Gentry2009, Theorem 4], without its exact +loss. -/ theorem leveled (hLWE : DecisionLWE) : ∃ circuit : ∀ security, Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature ((3 * secretWidth security + 1) + (ciphertextWidth security + 1)) 1, @@ -486,6 +499,8 @@ theorem leveled (hLWE : DecisionLWE) : Cslib.PolynomiallyBounded (fun security => ciphertextWidth security + 1) ∧ ∀ budget : ℕ → ℕ, Computation.PolyTime budget Encoding.encUnary Encoding.encUnary → ∃ S : Cslib.Crypto.Homomorphic.Scheme, + (∀ security, (Cslib.ProbComp.eval (S.keyGen security)).map + (fun keys => (unframe (unframe keys.1), unframe keys.2)) = keyGeneration security) ∧ EncryptsAndDecrypts S leveledEncryption leveledDecryption ∧ DecryptsWith S (fun security => 3 * secretWidth security + 1) (fun security => ciphertextWidth security + 1) circuit ∧ @@ -499,10 +514,10 @@ theorem leveled (hLWE : DecisionLWE) : (GSWFHEBridge.dropFrame_eq_of rfl rfl (fun _ => rfl) (fun _ _ => rfl)) hLWE /-- **Fully homomorphic encryption from decision LWE and circular security** [Gentry2009, -Definition 2 and Section 2]. A scheme whose key generation is the self-loop key and which -encrypts and decrypts with GSW is correct for every circuit, keeps GSW's widths, decrypts with -polynomial-size circuits, has native algorithms and is IND-CPA, assuming decision LWE for this -family and, separately, one-key circular security of GSW. -/ +Definition 2 and Section 2]. There is a scheme whose key generation is the self-loop key and +which encrypts and decrypts with GSW that is correct for every circuit, keeps GSW's widths, +decrypts with polynomial-size circuits, has native algorithms and is IND-CPA, assuming decision +LWE for this family and, separately, one-key circular security of GSW. -/ theorem fullyHomomorphic (hLWE : DecisionLWE) (hcircular : CircularSecure) : ∃ circuit : ∀ security, Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature (secretWidth security + ciphertextWidth security) 1, @@ -533,9 +548,9 @@ info: abstract audit passed for `ComplexityTests.Abstracts.GSWFHEAbstract`: 56 r Complexity.Languages.Probabilistic.Basic, -- the binary circuit code and the encodings it is assembled from Complexity.Computability.Circuit.Boolean.Encoding, - Complexity.Computability.Machines.Turing.MultiTape.Encodings.Basic, + Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame.Basic, Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair, Complexity.Computability.Machines.Turing.MultiTape.Encodings.List, - Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat, - Complexity.Computability.Machines.Turing.MultiTape.Complexity.Primitives + Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Bits, + Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary ] diff --git a/abstracts/ComplexityAbstracts/GSWFHEBridge.lean b/abstracts/ComplexityAbstracts/GSWFHEBridge.lean index 1d0a7b6e0..0b9f567a6 100644 --- a/abstracts/ComplexityAbstracts/GSWFHEBridge.lean +++ b/abstracts/ComplexityAbstracts/GSWFHEBridge.lean @@ -17,11 +17,12 @@ elementary terms, and asserts that suitable bootstrapping machinery exists. This that the library's constructions are such machinery: `leveled_witness` for `Leveled.scheme GSW.DepthParameters.decryptionCircuits budget` and `fullyHomomorphic_witness` for `FixedKey.scheme GSW.DepthParameters.decryptionCircuits`. It identifies their encryption, -decryption and fixed-key generation with the explicit GSW algorithms, identifies the assumptions -with the library's decision-LWE and circular-security experiments, and derives the elementary -properties from `Scheme.Correct`, `Scheme.FixedWidth`, the native certificates and -`Encryption.INDCPA`. The leveled endpoint is assembled for every efficiently computable budget -from the generic bootstrapping lemmas. The bridge introduces no notation or elaboration rules. +decryption and fixed-key generation, and the law of the leveled chain's first key pair, with the +explicit GSW algorithms, identifies the assumptions with the library's decision-LWE and +circular-security experiments, and derives the elementary properties from `Scheme.Correct`, +`Scheme.FixedWidth`, the native certificates and `Encryption.INDCPA`. The leveled endpoint is +assembled for every efficiently computable budget from the generic bootstrapping lemmas. The +bridge introduces no notation or elaboration rules. -/ namespace ComplexityTests.Abstracts.GSWFHEBridge @@ -493,6 +494,30 @@ theorem leveled_encryptsAndDecrypts (budget : ℕ → ℕ) : simp only [Leveled.scheme, Leveled.decrypt, hkey, eval_decryptionCircuit] rfl +/-- The library's leveled key generation, for every budget, publishes the chain's first public key +and keeps its secret as the first endpoint; that key pair has GSW's key-generation law. The rest +of the chain is sampled after it and is projected away. -/ +theorem leveled_keyGen (budget : ℕ → ℕ) (security : ℕ) : + (ProbComp.eval ((Leveled.scheme GSW.DepthParameters.decryptionCircuits budget).keyGen + security)).map (fun keys => (Turing.MultiTapeTM.unframe + (Turing.MultiTapeTM.unframe keys.1), Turing.MultiTapeTM.unframe keys.2)) = + keyGeneration security := by + have hproj (first : List Bool × List Bool) (rest : List (List Bool × List Bool)) + (links : List (List (List Bool))) : + (Turing.MultiTapeTM.unframe (Turing.MultiTapeTM.unframe + (Leveled.keyPair (2 * budget security) (first :: rest) links).1), + Turing.MultiTapeTM.unframe + (Leveled.keyPair (2 * budget security) (first :: rest) links).2) = first := by + simp only [Leveled.keyPair, Leveled.encPublicKey, Leveled.encSecretKey, encPair, encList, + encBits, Function.Embedding.coeFn_mk, Function.Embedding.refl_apply, List.map_cons, + List.flatMap_cons, Function.comp_apply, unframe_frame_append, List.getD_cons_zero] + change (ProbComp.eval ((fun chain => Leveled.keyPair (2 * budget security) chain.1 chain.2) <$> + GSW.DepthParameters.scheme.generateKeyChain security (2 * budget security))).map _ = _ + simp only [Scheme.generateKeyChain, Scheme.generateKeys, OracleComp.replicate_succ, + ProbComp.eval_map, ProbComp.eval_bind, ProbComp.eval_pure, PMF.map_bind, PMF.bind_bind, + PMF.pure_map, PMF.bind_map, Function.comp_apply, hproj, PMF.bind_const, PMF.bind_pure, + (base_scheme security).1] + /-- The library's fixed-key key generation is the self-loop key generation. -/ theorem fixedKey_keyGen (security : ℕ) : ProbComp.eval ((FixedKey.scheme GSW.DepthParameters.decryptionCircuits).keyGen security) = @@ -582,6 +607,10 @@ theorem leveled_witness (hLWE : DecisionLWE) : PolynomiallyBounded (fun security => 3 * secretWidth security + 1) ∧ PolynomiallyBounded (fun security => ciphertextWidth security + 1) ∧ ∀ budget : ℕ → ℕ, Computation.PolyTime budget Encoding.encUnary Encoding.encUnary → + (∀ security, (ProbComp.eval + ((Leveled.scheme GSW.DepthParameters.decryptionCircuits budget).keyGen security)).map + (fun keys => (Turing.MultiTapeTM.unframe (Turing.MultiTapeTM.unframe keys.1), + Turing.MultiTapeTM.unframe keys.2)) = keyGeneration security) ∧ EncryptsAndDecrypts (Leveled.scheme GSW.DepthParameters.decryptionCircuits budget) (leveledEncryption Turing.MultiTapeTM.unframe) (leveledDecryption Turing.MultiTapeTM.unframe Turing.MultiTapeTM.dropFrame) ∧ @@ -610,7 +639,8 @@ theorem leveled_witness (hLWE : DecisionLWE) : Leveled.correct_fixedWidth_indCPA D GSW.DepthParameters.correct GSW.DepthParameters.fixedWidth GSW.DepthParameters.bootstrappable (GSW.DepthParameters.indCPA_scheme (decisionLWE_iff.mp hLWE)) hkeyGen hencrypt hD hb - exact ⟨leveled_encryptsAndDecrypts budget, fun security => hcircuits budget security, + exact ⟨leveled_keyGen budget, leveled_encryptsAndDecrypts budget, + fun security => hcircuits budget security, homomorphic_of_correct hcorrect fun _ _ h => h, fixedWidths_of_fixedWidth hwidth fun _ _ h => h, native_of (Leveled.isPPTOn_scheme_keyGen hkeyGen hencrypt D budget hb) @@ -662,6 +692,8 @@ theorem leveled {unframe dropFrame : List Bool → List Bool} PolynomiallyBounded (fun security => ciphertextWidth security + 1) ∧ ∀ budget : ℕ → ℕ, Computation.PolyTime budget Encoding.encUnary Encoding.encUnary → ∃ S : Homomorphic.Scheme, + (∀ security, (ProbComp.eval (S.keyGen security)).map + (fun keys => (unframe (unframe keys.1), unframe keys.2)) = keyGeneration security) ∧ EncryptsAndDecrypts S (leveledEncryption unframe) (leveledDecryption unframe dropFrame) ∧ DecryptsWith S (fun security => 3 * secretWidth security + 1) diff --git a/abstracts/README.md b/abstracts/README.md index e7931ab16..816fc59eb 100644 --- a/abstracts/README.md +++ b/abstracts/README.md @@ -44,7 +44,7 @@ former paper/TeX index is retired; Git history retains its sources. | [Håstad and Razborov–Smolensky: parity resists shallow circuits](ComplexityAbstracts/ConstantDepthAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/constant-depth.pdf) | Explicit finite bounds, gate semantics and depth conventions; nonuniform lower bounds. | | [Formula lower bounds: parity and Andreev](ComplexityAbstracts/FormulaBoundsAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/formula-bounds.pdf) | De Morgan formulas, literal leaves, explicit block indexing and finite quantitative bounds; no general-circuit lower bound. | | [One-way functions yield pseudorandom generators and adaptive functions](ComplexityAbstracts/CryptographyAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/cryptography.pdf) | Uniform probabilistic polynomial time with explicit native evaluators, negligible advantage and full stateful oracle semantics; asymptotic security, not a concrete implementation audit. | -| [Gentry and GSW: fully homomorphic encryption from LWE](ComplexityAbstracts/GSWFHEAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/gsw-fhe.pdf) | Explicit GSW algorithms at an LWE family with quasi-polynomial modulus and Gentry's self-loop key; an existential evaluator, key chain and decryption circuits with correctness, fixed widths, polynomial-size decryption circuits, native algorithms and IND-CPA; circular security as a separate hypothesis. | +| [Gentry and GSW: fully homomorphic encryption from LWE](ComplexityAbstracts/GSWFHEAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/gsw-fhe.pdf) | Explicit GSW algorithms at an LWE family with quasi-polynomial modulus, the GSW key law for the leveled scheme's fresh ciphertexts and Gentry's self-loop key; an existential evaluator, remaining key chain and decryption circuits with correctness, fixed widths, polynomial-size decryption circuits, native algorithms and IND-CPA; circular security as a separate hypothesis. | | [Haken: pigeonhole formulas require long resolution proofs](ComplexityAbstracts/ResolutionAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/resolution.pdf) | The non-onto pigeonhole formula and a line-based resolution rule, with bound 2^(floor(n/24)); proof size is not solver runtime. | | [Communication: disjointness and inner product resist randomness](ComplexityAbstracts/CommunicationAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/communication.pdf) | Shared randomness, per-input error at most one third and explicit linear bounds; exact deterministic equality records the final-answer convention. | | [Sipser–Gács–Lautemann: BPP lies in the second polynomial level](ComplexityAbstracts/SipserLautemannAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/sipser-lautemann.pdf) | Fair random bits, explicit quantifier blocks and total native polynomial-time tests. | diff --git a/abstracts/catalogue.json b/abstracts/catalogue.json index 2627bfb65..c041767b4 100644 --- a/abstracts/catalogue.json +++ b/abstracts/catalogue.json @@ -170,7 +170,7 @@ "ComplexityTests.Abstracts.GSWFHEAbstract.fullyHomomorphic" ], "summary": "Bootstrapping the GSW scheme gives leveled fully homomorphic encryption from decision LWE, and fully homomorphic encryption under an additional circular-security assumption.", - "scope": "Explicit GSW key generation, encryption and decryption at a centered-binomial LWE family with quasi-polynomial modulus, and Gentry's self-loop key; the evaluator, the leveled key chain and the decryption circuits are existential. Perfect correctness on fresh encryptions, fixed widths, polynomial-size decryption circuits, native strict PPT algorithms and asymptotic IND-CPA. Circular security is a separate hypothesis; no lattice hardness, circuit privacy, multi-hop evaluation or concrete loss.", + "scope": "Explicit GSW key generation, encryption and decryption at a centered-binomial LWE family with quasi-polynomial modulus. The leveled scheme's fresh-ciphertext key pair has the GSW key-generation law, and the fully homomorphic scheme's key generation is Gentry's self-loop key; the evaluator, the rest of the leveled keys and the decryption circuits are existential. Perfect correctness on fresh encryptions, fixed widths, polynomial-size decryption circuits, native strict PPT algorithms and asymptotic IND-CPA. Circular security is a separate hypothesis; no lattice hardness, circuit privacy, multi-hop evaluation or concrete loss.", "namespace": "ComplexityTests.Abstracts.GSWFHEAbstract", "foundations": [ "ComplexityAbstracts.Encoding",