diff --git a/ComplexityTests/Abstracts/GSWFHETests.lean b/ComplexityTests/Abstracts/GSWFHETests.lean new file mode 100644 index 0000000000..8e77b3ea9d --- /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 3ac7f40eae..b0e9e674af 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,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` 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. @@ -480,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.lean b/abstracts/ComplexityAbstracts.lean index 784d928e4f..63b35af184 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 80370c9eeb..d692f66291 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 bca0b76ed1..4cce6f6e7b 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 0000000000..f002401d2f --- /dev/null +++ b/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean @@ -0,0 +1,556 @@ +/- +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 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, 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 +`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.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 +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. 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 +on every word. +-/ + +/-- 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) + +/-- 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`. 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. -/ +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 + +/-- **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 +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, 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 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 +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. + +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. +-/ + +/-- 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 +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 + +`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 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]. 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, + 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 → + ∃ 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 ∧ + 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]. 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, + Cslib.PolynomiallyBounded (fun security => (circuit security).size) ∧ + Cslib.PolynomiallyBounded secretWidth ∧ Cslib.PolynomiallyBounded ciphertextWidth ∧ + ∃ 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`: 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 scheme record and randomized programs + Complexity.Crypto.Computational.Homomorphic.Basic, + 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.Frame.Basic, + Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair, + Complexity.Computability.Machines.Turing.MultiTape.Encodings.List, + 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 new file mode 100644 index 0000000000..0b9f567a69 --- /dev/null +++ b/abstracts/ComplexityAbstracts/GSWFHEBridge.lean @@ -0,0 +1,730 @@ +/- +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 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, 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 + +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 + +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) + +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) + +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 → + (∀ 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 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 α) : + 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 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, + 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⟩ + +/-- 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 : ℕ) : + 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 _ _ _ + +/-- 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 + (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 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 + 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 + 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 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 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) = + 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} + (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 + +/-! ### Provenance: the library's schemes are the witnesses -/ + +/-- **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 → + (∀ 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) ∧ + 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 ⟨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) + (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⟩ + +/-- **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 ∧ + 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 ⟨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, + (∀ 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) + (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/ComplexityAbstracts/GSWSecurityBridge.lean b/abstracts/ComplexityAbstracts/GSWSecurityBridge.lean index baa9d82476..d64a6ac110 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 0000000000..57ac89fce2 --- /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 90d685dba5..816fc59ebc 100644 --- a/abstracts/README.md +++ b/abstracts/README.md @@ -1,6 +1,6 @@ # 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 @@ -44,9 +44,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) | 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. | +| [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 dc391237d7..c041767b48 100644 --- a/abstracts/catalogue.json +++ b/abstracts/catalogue.json @@ -157,7 +157,25 @@ "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" + ], + "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. 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", + "ComplexityAbstracts.Computation", + "ComplexityAbstracts.Randomized" ] }, {