From bb80f97c744c7139af70cb6cadbc71f306486163 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 24 Oct 2026 18:02:03 +0000 Subject: [PATCH] refactor: move Languages/Probabilistic samplers to Cslib.ProbComp (#614) --- .../Complexity/Classes/IP/TQBF/Words.lean | 2 +- .../Probabilistic/BoundedUniform.lean | 2 +- .../Probabilistic/CenteredBinomial.lean | 4 +-- .../Probabilistic/UniformNat.lean | 6 ++-- .../Crypto/Computational/GGM/Reduction.lean | 4 +-- .../Computational/Homomorphic/GSW/LWE.lean | 2 +- .../Homomorphic/GSW/Sampling.lean | 2 +- .../Homomorphic/GSW/Sampling/Randomness.lean | 2 +- .../Homomorphic/GSW/Sampling/Serialized.lean | 2 +- .../Homomorphic/KeyChain/Reduction.lean | 2 +- .../Homomorphic/KeyChain/Reduction/Game.lean | 2 +- .../Computational/Hybrid/SavedPrediction.lean | 2 +- .../Crypto/Computational/Hybrid/Sequence.lean | 2 +- .../Computational/OneWayToSignature.lean | 2 +- .../Pseudoentropy/Boosting/Clipped.lean | 2 +- .../Pseudoentropy/Boosting/Sampling.lean | 2 +- .../Pseudoentropy/DenseMask.lean | 2 +- .../Computational/Pseudoentropy/HashPair.lean | 2 +- .../Pseudoentropy/MaskedExtraction.lean | 2 +- .../Pseudoentropy/WordReduction.lean | 2 +- Complexity/Crypto/Computational/Stretch.lean | 4 +-- .../Crypto/Computational/UniformChoice.lean | 2 +- .../Probabilistic/BoundedUniform.lean | 27 +++++++++--------- .../Probabilistic/CenteredBinomial.lean | 17 ++++++----- .../Languages/Probabilistic/UniformNat.lean | 28 ++++++++++--------- ComplexityTests/Axioms.lean | 4 +-- ComplexityTests/BoundedUniform.lean | 4 +-- .../Crypto/GSWDepthParameters.lean | 2 +- ComplexityTests/Crypto/GSWParameters.lean | 2 +- ComplexityTests/Crypto/GSWSampling.lean | 2 +- ComplexityTests/Presample.lean | 2 +- ComplexityTests/PseudoentropyMasking.lean | 4 +-- ComplexityTests/UniformNat.lean | 2 +- .../GSWSecurityBridge.lean | 2 +- 34 files changed, 78 insertions(+), 72 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/IP/TQBF/Words.lean b/Complexity/Computability/Complexity/Classes/IP/TQBF/Words.lean index c60debcf3d..a3fb981440 100644 --- a/Complexity/Computability/Complexity/Classes/IP/TQBF/Words.lean +++ b/Complexity/Computability/Complexity/Classes/IP/TQBF/Words.lean @@ -73,7 +73,7 @@ All are polynomial-time in their unary or binary inputs. namespace Cslib.Complexity.QBFProtocol -open Cslib.Logic.PL Polynomial Turing.MultiTapeTM Cslib.Probability +open Cslib.Logic.PL Polynomial Turing.MultiTapeTM Cslib.Probability Cslib.ProbComp open scoped ENNReal /-! ### Arithmetic modulo `p` -/ diff --git a/Complexity/Computability/Probabilistic/BoundedUniform.lean b/Complexity/Computability/Probabilistic/BoundedUniform.lean index b76b317e01..52fab4bcae 100644 --- a/Complexity/Computability/Probabilistic/BoundedUniform.lean +++ b/Complexity/Computability/Probabilistic/BoundedUniform.lean @@ -36,7 +36,7 @@ Failure remains in the certified program's output. namespace Cslib.Probability -open Turing.MultiTapeTM +open ProbComp Turing.MultiTapeTM /-- Unary bounds and attempt counts give a uniform strict PPT sampler, including its failure result and every stored attempt. -/ diff --git a/Complexity/Computability/Probabilistic/CenteredBinomial.lean b/Complexity/Computability/Probabilistic/CenteredBinomial.lean index 77f156a605..caea285848 100644 --- a/Complexity/Computability/Probabilistic/CenteredBinomial.lean +++ b/Complexity/Computability/Probabilistic/CenteredBinomial.lean @@ -37,7 +37,7 @@ charges both blocks of independent trials, their counts, and signed subtraction. namespace Cslib.Probability -open Turing.MultiTapeTM +open ProbComp Turing.MultiTapeTM /-- The centered-binomial program is uniformly strict PPT, with a unary parameter and binary signed output. No fixed finite output type or finite-rank encoding is used. -/ @@ -69,5 +69,5 @@ theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.sampleCenteredBinomial {α {input : α ↪ List Bool} {parameter : α → ℕ} (hparameter : ComputableTidilyInPolyTime parameter input encUnary) : Cslib.Probability.IsPPTOn input encIntBin - (fun a => Cslib.Probability.sampleCenteredBinomial (parameter a)) := + (fun a => Cslib.ProbComp.sampleCenteredBinomial (parameter a)) := Cslib.Probability.isPPTOn_sampleCenteredBinomial.preprocess hparameter diff --git a/Complexity/Computability/Probabilistic/UniformNat.lean b/Complexity/Computability/Probabilistic/UniformNat.lean index 7a4869c3ed..7644c033e0 100644 --- a/Complexity/Computability/Probabilistic/UniformNat.lean +++ b/Complexity/Computability/Probabilistic/UniformNat.lean @@ -66,7 +66,7 @@ theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_dyadicSize : namespace Cslib.Probability -open Turing.MultiTapeTM +open ProbComp Turing.MultiTapeTM /-- A unary bit width gives a uniformly strict PPT sampler with binary natural output. -/ theorem isPPTOn_sampleBinaryNat : IsPPTOn encUnary encNat sampleBinaryNat := @@ -106,12 +106,12 @@ theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.sampleBinaryNat {α : Type {input : α ↪ List Bool} {width : α → ℕ} (hwidth : ComputableTidilyInPolyTime width input encUnary) : Cslib.Probability.IsPPTOn input encNat - (fun a => Cslib.Probability.sampleBinaryNat (width a)) := + (fun a => Cslib.ProbComp.sampleBinaryNat (width a)) := Cslib.Probability.isPPTOn_sampleBinaryNat.preprocess hwidth namespace Cslib.Probability -open Turing.MultiTapeTM +open ProbComp Turing.MultiTapeTM /-- Approximately uniform residues: reducing a computed number of fair bits modulo a computed modulus is uniformly strict PPT, with binary output. -/ diff --git a/Complexity/Crypto/Computational/GGM/Reduction.lean b/Complexity/Crypto/Computational/GGM/Reduction.lean index c0669623e0..b36f662e6a 100644 --- a/Complexity/Crypto/Computational/GGM/Reduction.lean +++ b/Complexity/Crypto/Computational/GGM/Reduction.lean @@ -157,7 +157,7 @@ theorem levelTest_gap (generator : List Bool → List Bool) (adversary : OracleD dyadic ranges, and unused indices reject. The query budget is a fixed function of the parameter. -/ noncomputable def reduction (generator : List Bool → List Bool) (adversary : OracleDistinguisher) (count : ℕ → ℕ) : Distinguisher := fun n challenge => do - let depth ← sampleDyadicIndex n + let depth ← ProbComp.sampleDyadicIndex n if depth < n then levelTest generator adversary n depth (count n) challenge else pure false /-- Efficient generation and an efficient query budget give one uniform PPT reduction. -/ @@ -194,7 +194,7 @@ theorem reduction_gap (generator : List Bool → List Bool) (adversary : OracleD (lt_dyadicSize n).le (dyadicSize (count n)) (fun depth hdepth => levelTest_gap generator adversary n depth (count n) hdepth hqueries) - simpa only [eval_bind_sampleDyadicIndex_guard, PMF.monad_bind_eq_bind, + simpa only [ProbComp.eval_bind_sampleDyadicIndex_guard, PMF.monad_bind_eq_bind, hybridGame_zero, hybridGame_self] using h /-- The real/ideal PRF advantage is the reduction's generator advantage times the two sampling diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/LWE.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/LWE.lean index d084353fe5..20001e3781 100644 --- a/Complexity/Crypto/Computational/Homomorphic/GSW/LWE.lean +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/LWE.lean @@ -37,7 +37,7 @@ the equality below exposes only the public marginal, as required by the security namespace Cslib.Crypto.Homomorphic.GSW -open Probability +open ProbComp Probability /-- Reduce the difference of two independent `η`-bit counts modulo the actual modulus. -/ noncomputable def noiseLaw (w η : ℕ) : PMF (ZMod (2 ^ w)) := diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling.lean index c9710a1799..694ceb02d4 100644 --- a/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling.lean +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling.lean @@ -49,7 +49,7 @@ encryption security, complete native algorithm certificate or bootstrappability namespace Cslib.Crypto.Homomorphic.GSW -open Probability +open ProbComp Probability /-- Sample one residue from `w` independent fair bits. -/ noncomputable def sampleResidue (w : ℕ) : ProbComp (ZMod (2 ^ w)) := diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling/Randomness.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling/Randomness.lean index 3d3b4fafe3..9eae36478a 100644 --- a/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling/Randomness.lean +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling/Randomness.lean @@ -37,7 +37,7 @@ is proved separately; matrix computation and cryptographic security remain separ namespace Cslib.Crypto.Homomorphic.GSW -open Probability +open ProbComp Probability /-- A residue uses a uniform word of exactly its binary width. -/ theorem exists_uniform_seed_sampleResidue (w : ℕ) : diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling/Serialized.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling/Serialized.lean index 697e296ed1..a0f990ee57 100644 --- a/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling/Serialized.lean +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling/Serialized.lean @@ -51,7 +51,7 @@ arithmetic, the complete GSW key-generation or encryption algorithms, or computa namespace Cslib.Crypto.Homomorphic.GSW -open Probability Turing.MultiTapeTM +open ProbComp Probability Turing.MultiTapeTM /-- Secret entries, public-matrix rows and signed errors, without dependent dimensions. -/ abbrev SerializedKeyInputs := List ℕ × (List (List ℕ) × List ℤ) diff --git a/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction.lean b/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction.lean index a081bd9e42..e21fb38762 100644 --- a/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction.lean +++ b/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction.lean @@ -48,7 +48,7 @@ its beginning. Dyadic padding coordinates reject, and decoding is total on every namespace Cslib.Crypto.Homomorphic.Scheme -open Probability Turing.MultiTapeTM +open ProbComp Probability Turing.MultiTapeTM /-- Active flag, earlier keys, predecessor, challenge public key, later keys, and unary bit index. Every saved secret belongs to a key generated by the reduction itself. -/ diff --git a/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction/Game.lean b/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction/Game.lean index b508fdedc4..1371766db4 100644 --- a/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction/Game.lean +++ b/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction/Game.lean @@ -39,7 +39,7 @@ outgoing link has been erased. namespace Cslib.Crypto.Homomorphic.Scheme -open Probability +open ProbComp Probability open scoped NNReal variable (E : Scheme) diff --git a/Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean b/Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean index e5e37a508c..ef775198f0 100644 --- a/Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean +++ b/Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean @@ -50,7 +50,7 @@ Adapted from the cslib `crypto` branch at namespace Cslib.Crypto.SavedPrediction -open Probability BitString Turing.MultiTapeTM +open ProbComp Probability BitString Turing.MultiTapeTM /-- Finite data needed to reuse one coordinate predictor on arbitrary observations. -/ structure Description where diff --git a/Complexity/Crypto/Computational/Hybrid/Sequence.lean b/Complexity/Crypto/Computational/Hybrid/Sequence.lean index 491cfe8036..248607acd6 100644 --- a/Complexity/Crypto/Computational/Hybrid/Sequence.lean +++ b/Complexity/Crypto/Computational/Hybrid/Sequence.lean @@ -48,7 +48,7 @@ Adapted from Crypto/Computational/Hybrid/Sequence.lean on the cslib `crypto` bra namespace Cslib.Crypto -open Probability Turing.MultiTapeTM +open ProbComp Probability Turing.MultiTapeTM open scoped NNReal variable {α : Type} diff --git a/Complexity/Crypto/Computational/OneWayToSignature.lean b/Complexity/Crypto/Computational/OneWayToSignature.lean index 077f84cdf9..efcf3a1a49 100644 --- a/Complexity/Crypto/Computational/OneWayToSignature.lean +++ b/Complexity/Crypto/Computational/OneWayToSignature.lean @@ -86,7 +86,7 @@ one-way hash functions and GMR/Merkle authentication trees. namespace Cslib.Crypto -open Filter Probability Turing.MultiTapeTM +open Filter ProbComp Probability Turing.MultiTapeTM open scoped NNReal ENNReal @[fun_prop] diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Clipped.lean b/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Clipped.lean index ffb485ff56..35bf002b58 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Clipped.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Clipped.lean @@ -49,7 +49,7 @@ Adapted from the cslib `crypto` branch at `5ff69ca93402e7c947208dc56396d6d86203c namespace Cslib.Crypto.Pseudoentropy.Boosting -open Probability BitString Turing.MultiTapeTM +open ProbComp Probability BitString Turing.MultiTapeTM /-- The clipped affine probability associated with a signed margin. -/ noncomputable def clippedProbability (slope margin : ℝ) : ℝ := diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Sampling.lean b/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Sampling.lean index ae9fbd0a52..0ee8fa8bc8 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Sampling.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Sampling.lean @@ -50,7 +50,7 @@ Crypto/Computational/Pseudoentropy/Boosting/Sampling.lean on the cslib `crypto` namespace Cslib.Crypto.Pseudoentropy.Boosting -open Probability BitString Turing.MultiTapeTM +open ProbComp Probability BitString Turing.MultiTapeTM /-- The numerator of a clipped linear weight, computed entirely with natural numbers. The excess of correct over incorrect votes is `2 * votes.count truth - votes.length` in diff --git a/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean b/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean index 24f148ece2..a44154809f 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean @@ -49,7 +49,7 @@ Adapted from the cslib `crypto` branch at namespace Cslib.Crypto.Pseudoentropy.SamplablePair -open Probability Probability.PMF BitString Boosting Filter Turing.MultiTapeTM +open ProbComp Probability Probability.PMF BitString Boosting Filter Turing.MultiTapeTM /-- All tests in a uniformly efficient polynomial-size family eventually admit dense soft masks with small distinguishing gap whenever their density is valid. The common eventual threshold diff --git a/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean b/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean index 2979df14e7..6b4b55490d 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean @@ -55,7 +55,7 @@ Adapted from Crypto/Computational/Pseudoentropy/HashPair.lean on the cslib `cryp namespace Cslib.Crypto.Pseudoentropy.HashPair -open Cslib.Probability Cslib.Probability.PMF BitString Turing.MultiTapeTM +open Cslib.ProbComp Cslib.Probability Cslib.Probability.PMF BitString Turing.MultiTapeTM /-- The number of possible hash lengths. Six extra lengths leave room for the truncation threshold in the inversion proof; rounding up makes sampling exact with fair bits. -/ diff --git a/Complexity/Crypto/Computational/Pseudoentropy/MaskedExtraction.lean b/Complexity/Crypto/Computational/Pseudoentropy/MaskedExtraction.lean index 69c35ac380..03eddd9e29 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/MaskedExtraction.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/MaskedExtraction.lean @@ -43,7 +43,7 @@ Adapted from the cslib `crypto` branch at namespace Cslib.Crypto.Pseudoentropy -open Probability Probability.PMF BitString +open ProbComp Probability Probability.PMF BitString open scoped NNReal diff --git a/Complexity/Crypto/Computational/Pseudoentropy/WordReduction.lean b/Complexity/Crypto/Computational/Pseudoentropy/WordReduction.lean index fd75314cee..89dc4acb3e 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/WordReduction.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/WordReduction.lean @@ -53,7 +53,7 @@ at `5ff69ca93402e7c947208dc56396d6d86203ccd8`, using typed saved seeds and the t namespace Cslib.Crypto.Pseudoentropy.HashPair -open Probability BitString GoldreichLevin Turing.MultiTapeTM +open ProbComp Probability BitString GoldreichLevin Turing.MultiTapeTM /-- One polynomial tape budget covers all digest lengths and parity queries for an image. -/ def coinBudget (c d n imageLength : ℕ) : ℕ := diff --git a/Complexity/Crypto/Computational/Stretch.lean b/Complexity/Crypto/Computational/Stretch.lean index 13cf9fe89e..b922fc5294 100644 --- a/Complexity/Crypto/Computational/Stretch.lean +++ b/Complexity/Crypto/Computational/Stretch.lean @@ -59,7 +59,7 @@ Adapted from Crypto/Computational/Stretch.lean on the cslib `crypto` branch at namespace Cslib.Crypto.PRGStretch -open Probability BitString Turing.MultiTapeTM +open ProbComp Probability BitString Turing.MultiTapeTM /-- Hybrid `i` has `i` genuinely random suffix bits and `total - i` seed expansions left. -/ noncomputable def hybrid (generator : List Bool → List Bool) (n total i : ℕ) : PMF (List Bool) := @@ -372,7 +372,7 @@ end Cslib.Crypto.PRGStretch namespace Cslib.Crypto -open Probability BitString Turing.MultiTapeTM +open ProbComp Probability BitString Turing.MultiTapeTM /-- Amplify a one-bit PRG to any efficiently computed, strictly larger output length. -/ theorem PseudorandomGenerator.amplify {generator : List Bool → List Bool} diff --git a/Complexity/Crypto/Computational/UniformChoice.lean b/Complexity/Crypto/Computational/UniformChoice.lean index 6605b21627..2e1149a344 100644 --- a/Complexity/Crypto/Computational/UniformChoice.lean +++ b/Complexity/Crypto/Computational/UniformChoice.lean @@ -52,7 +52,7 @@ nonnegative game API. namespace Cslib.Crypto -open Probability Turing.MultiTapeTM +open ProbComp Probability Turing.MultiTapeTM open scoped NNReal namespace UniformChoice diff --git a/Complexity/Languages/Probabilistic/BoundedUniform.lean b/Complexity/Languages/Probabilistic/BoundedUniform.lean index 7e6d49ee6e..600373cb8f 100644 --- a/Complexity/Languages/Probabilistic/BoundedUniform.lean +++ b/Complexity/Languages/Probabilistic/BoundedUniform.lean @@ -36,29 +36,30 @@ transcript/error and an extractor's implementation require separate proofs. ## Main definitions -* `Cslib.Probability.sampleUniformInterval`: bounded retry with an explicit failure result. -* `Cslib.Probability.intervalFailure`, `Cslib.Probability.intervalSuccess`: exact event masses. -* `Cslib.Probability.sampleIntegerBox`: coordinatewise finite-attempt integer-box sampling. -* `Cslib.Probability.integerBoxLaw`: the exact mathematical uniform reference law. +* `Cslib.ProbComp.sampleUniformInterval`: bounded retry with an explicit failure result. +* `Cslib.ProbComp.intervalFailure`, `Cslib.ProbComp.intervalSuccess`: exact event masses. +* `Cslib.ProbComp.sampleIntegerBox`: coordinatewise finite-attempt integer-box sampling. +* `Cslib.ProbComp.integerBoxLaw`: the exact mathematical uniform reference law. ## Main results -* `Cslib.Probability.eval_sampleUniformInterval_none`, - `Cslib.Probability.eval_sampleUniformInterval_some_toReal`: the full interval law. -* `Cslib.Probability.sampleUniformInterval_conditional`: conditional uniformity at observable +* `Cslib.ProbComp.eval_sampleUniformInterval_none`, + `Cslib.ProbComp.eval_sampleUniformInterval_some_toReal`: the full interval law. +* `Cslib.ProbComp.sampleUniformInterval_conditional`: conditional uniformity at observable success events. -* `Cslib.Probability.sampleUniformInterval_test_error_le`: unconditional interval error, +* `Cslib.ProbComp.sampleUniformInterval_test_error_le`: unconditional interval error, including the binary-bound implementation. -* `Cslib.Probability.eval_sampleIntegerBox_some`, `Cslib.Probability.eval_sampleIntegerBox_none`: +* `Cslib.ProbComp.eval_sampleIntegerBox_some`, `Cslib.ProbComp.eval_sampleIntegerBox_none`: the full joint success/failure law. -* `Cslib.Probability.sampleIntegerBox_test_error_le`: explicit unconditional statistical error. -* `Cslib.Probability.sampleIntegerBox_support`: exact output dimension and integer bounds. +* `Cslib.ProbComp.sampleIntegerBox_test_error_le`: explicit unconditional statistical error. +* `Cslib.ProbComp.sampleIntegerBox_support`: exact output dimension and integer bounds. -/ @[expose] public section -namespace Cslib.Probability +namespace Cslib.ProbComp +open Probability open scoped ENNReal NNReal /-- The probability that one capped draw is rejected. At bound zero every draw is rejected. -/ @@ -740,4 +741,4 @@ theorem integerBoxLaw_apply_index (radius dimension : ℕ) simp_rw [hcoord] simp -end Cslib.Probability +end Cslib.ProbComp diff --git a/Complexity/Languages/Probabilistic/CenteredBinomial.lean b/Complexity/Languages/Probabilistic/CenteredBinomial.lean index 3504cb5909..3ceb7fe3f7 100644 --- a/Complexity/Languages/Probabilistic/CenteredBinomial.lean +++ b/Complexity/Languages/Probabilistic/CenteredBinomial.lean @@ -24,14 +24,15 @@ or encryption-security property is asserted. Native runtime is certified separat ## Main definitions -* `sampleCenteredBinomial`: subtract two independently sampled Boolean counts. +* `Cslib.ProbComp.sampleCenteredBinomial`: subtract two independently sampled Boolean counts. ## Main results -* `eval_sampleCenteredBinomial`: the exact two-word distribution. -* `eval_sampleCenteredBinomial_eq_map`: the same law from one word of `2 * η` bits. -* `mem_support_sampleCenteredBinomial_iff`: support is exactly the closed integer interval. -* `map_neg_eval_sampleCenteredBinomial`: negation preserves the distribution. +* `Cslib.ProbComp.eval_sampleCenteredBinomial`: the exact two-word distribution. +* `Cslib.ProbComp.eval_sampleCenteredBinomial_eq_map`: the same law from one word of `2 * η` bits. +* `Cslib.ProbComp.mem_support_sampleCenteredBinomial_iff`: support is exactly the closed integer + interval. +* `Cslib.ProbComp.map_neg_eval_sampleCenteredBinomial`: negation preserves the distribution. ## References @@ -41,7 +42,9 @@ or encryption-security property is asserted. Native runtime is certified separat @[expose] public section -namespace Cslib.Probability +namespace Cslib.ProbComp + +open Probability /-- Subtract the true counts of two independent blocks of `η` fair bits. -/ noncomputable def sampleCenteredBinomial (η : ℕ) : ProbComp ℤ := do @@ -110,4 +113,4 @@ theorem map_neg_eval_sampleCenteredBinomial (η : ℕ) : PMF.pure_map, neg_sub] rw [PMF.bind_comm] -end Cslib.Probability +end Cslib.ProbComp diff --git a/Complexity/Languages/Probabilistic/UniformNat.lean b/Complexity/Languages/Probabilistic/UniformNat.lean index f3c23c8bc7..7be87d7023 100644 --- a/Complexity/Languages/Probabilistic/UniformNat.lean +++ b/Complexity/Languages/Probabilistic/UniformNat.lean @@ -31,19 +31,21 @@ range is at most `2 * (bound + 1)`. `sampleDyadicCoin bound numerator` compares ## Main definitions -* `sampleBinaryNat`: exact uniform sampling from a specified bit width. -* `sampleModNat`: approximately uniform sampling of residues modulo a given modulus. -* `sampleDyadicIndex`: exact uniform sampling in the power-of-two range. -* `sampleBoundedIndex`: a capped uniform index with a rejection sentinel. -* `sampleDyadicCoin`: an exact capped dyadic acceptance probability. +* `Cslib.ProbComp.sampleBinaryNat`: exact uniform sampling from a specified bit width. +* `Cslib.ProbComp.sampleModNat`: approximately uniform sampling of residues modulo a given modulus. +* `Cslib.ProbComp.sampleDyadicIndex`: exact uniform sampling in the power-of-two range. +* `Cslib.ProbComp.sampleBoundedIndex`: a capped uniform index with a rejection sentinel. +* `Cslib.ProbComp.sampleDyadicCoin`: an exact capped dyadic acceptance probability. ## Main results -* `eval_sampleBinaryNat`, `mem_support_sampleBinaryNat_iff`: the exact law and support. -* `eval_sampleModNat`, `dist_map_natCast_eval_sampleModNat_le`: the law of the residue sampler - and its distance from uniform on `ZMod q`. -* `eval_sampleDyadicIndex`, `eval_sampleBoundedIndex`: exact distribution laws. -* `eval_sampleDyadicCoin_true`: exact acceptance mass, including zero and one. +* `Cslib.ProbComp.eval_sampleBinaryNat`, `Cslib.ProbComp.mem_support_sampleBinaryNat_iff`: + the exact law and support. +* `Cslib.ProbComp.eval_sampleModNat`, `Cslib.ProbComp.dist_map_natCast_eval_sampleModNat_le`: + the law of the residue sampler and its distance from uniform on `ZMod q`. +* `Cslib.ProbComp.eval_sampleDyadicIndex`, `Cslib.ProbComp.eval_sampleBoundedIndex`: + exact distribution laws. +* `Cslib.ProbComp.eval_sampleDyadicCoin_true`: exact acceptance mass, including zero and one. ## References @@ -53,9 +55,9 @@ Adapted from Languages/Probabilistic/UniformNat.lean on the cslib `crypto` branc @[expose] public section -namespace Cslib.Probability +namespace Cslib.ProbComp -open BitString +open BitString Probability /-- Interpret exactly `width` independent fair bits as a binary natural number. -/ noncomputable def sampleBinaryNat (width : ℕ) : ProbComp ℕ := @@ -183,4 +185,4 @@ theorem eval_sampleBoundedIndex (bound : ℕ) : simp [sampleBoundedIndex, ProbComp.eval_map, BitString.eval_sampleList, uniformList_boundedBinaryValue] -end Cslib.Probability +end Cslib.ProbComp diff --git a/ComplexityTests/Axioms.lean b/ComplexityTests/Axioms.lean index c877c841a6..53ed8ba85c 100644 --- a/ComplexityTests/Axioms.lean +++ b/ComplexityTests/Axioms.lean @@ -4979,11 +4979,11 @@ info: 'Cslib.BitString.uniformList_binaryValue' depends on axioms: #print axioms Cslib.BitString.uniformList_binaryValue /-- -info: 'Cslib.Probability.eval_sampleBoundedIndex' depends on axioms: +info: 'Cslib.ProbComp.eval_sampleBoundedIndex' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in -#print axioms Cslib.Probability.eval_sampleBoundedIndex +#print axioms Cslib.ProbComp.eval_sampleBoundedIndex /-- info: 'Cslib.Probability.isPPTOn_sampleBoundedIndex' depends on axioms: diff --git a/ComplexityTests/BoundedUniform.lean b/ComplexityTests/BoundedUniform.lean index 1ec48e6e60..70a5887248 100644 --- a/ComplexityTests/BoundedUniform.lean +++ b/ComplexityTests/BoundedUniform.lean @@ -12,7 +12,7 @@ intervals have uniform certificates with runtime-varying budgets. -/ namespace ComplexityTests.BoundedUniform -open Cslib Cslib.Probability Turing.MultiTapeTM +open Cslib Cslib.ProbComp Cslib.Probability Turing.MultiTapeTM open scoped ENNReal NNReal example (attempts : ℕ) : @@ -94,7 +94,7 @@ example {radius dimension attempts : ℕ} {out : Option (List ℤ)} length_enc_sampleIntegerBox h /-- -info: 'Cslib.Probability.sampleIntegerBox_test_error_le' depends on axioms: +info: 'Cslib.ProbComp.sampleIntegerBox_test_error_le' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in diff --git a/ComplexityTests/Crypto/GSWDepthParameters.lean b/ComplexityTests/Crypto/GSWDepthParameters.lean index f4819d2adb..03d8bd718b 100644 --- a/ComplexityTests/Crypto/GSWDepthParameters.lean +++ b/ComplexityTests/Crypto/GSWDepthParameters.lean @@ -14,7 +14,7 @@ augmented decryption circuit fits the budget or assume security of an insecure f namespace ComplexityTests.GSWDepthParameters -open Cslib Cslib.Crypto Cslib.Probability Cslib.Crypto.Homomorphic.GSW +open Cslib Cslib.Crypto Cslib.ProbComp Cslib.Probability Cslib.Crypto.Homomorphic.GSW open Turing.MultiTapeTM -- Zero is included; neither the dimensions, noise nor depth collapses to an empty case. diff --git a/ComplexityTests/Crypto/GSWParameters.lean b/ComplexityTests/Crypto/GSWParameters.lean index 775158c426..8f1fa23338 100644 --- a/ComplexityTests/Crypto/GSWParameters.lean +++ b/ComplexityTests/Crypto/GSWParameters.lean @@ -16,7 +16,7 @@ checks supply no decision-LWE hardness or bootstrappability claim. namespace ComplexityTests.GSWParameters -open Cslib Cslib.Crypto Cslib.Probability Cslib.Crypto.Homomorphic.GSW +open Cslib Cslib.Crypto Cslib.ProbComp Cslib.Probability Cslib.Crypto.Homomorphic.GSW open Turing.MultiTapeTM open scoped NNReal diff --git a/ComplexityTests/Crypto/GSWSampling.lean b/ComplexityTests/Crypto/GSWSampling.lean index d5d90c85f2..392859c20b 100644 --- a/ComplexityTests/Crypto/GSWSampling.lean +++ b/ComplexityTests/Crypto/GSWSampling.lean @@ -17,7 +17,7 @@ are checked separately. No security or complete matrix-algorithm efficiency clai namespace ComplexityTests.GSWSampling -open Cslib Cslib.Probability Cslib.Crypto.Homomorphic.GSW +open Cslib Cslib.ProbComp Cslib.Probability Cslib.Crypto.Homomorphic.GSW open Turing.MultiTapeTM -- The smallest nontrivial noise law has masses 1/4, 1/2 and 1/4. diff --git a/ComplexityTests/Presample.lean b/ComplexityTests/Presample.lean index 0c0266f4e7..362c1bed0c 100644 --- a/ComplexityTests/Presample.lean +++ b/ComplexityTests/Presample.lean @@ -10,7 +10,7 @@ import Complexity.Tactic.PPT namespace ComplexityTests.Presample -open Cslib Cslib.Crypto Cslib.Probability Turing.MultiTapeTM +open Cslib Cslib.Crypto Cslib.ProbComp Cslib.Probability Turing.MultiTapeTM -- Infinite output types and computed repetition counts charge the entire framed result list. example : IsPPTOn encUnary (encList encBits) diff --git a/ComplexityTests/PseudoentropyMasking.lean b/ComplexityTests/PseudoentropyMasking.lean index 51123bbada..58ee6186d0 100644 --- a/ComplexityTests/PseudoentropyMasking.lean +++ b/ComplexityTests/PseudoentropyMasking.lean @@ -18,8 +18,8 @@ and exercise captured parameters in the complete masked-sequence predictor. namespace ComplexityTests.PseudoentropyMasking -open Cslib Cslib.Probability Cslib.Probability.PMF Cslib.Crypto Cslib.Crypto.Pseudoentropy - Cslib.Crypto.Pseudoentropy.Boosting Cslib.BitString Turing.MultiTapeTM +open Cslib Cslib.ProbComp Cslib.Probability Cslib.Probability.PMF Cslib.Crypto + Cslib.Crypto.Pseudoentropy Cslib.Crypto.Pseudoentropy.Boosting Cslib.BitString Turing.MultiTapeTM example : listStrictMajority [] = false ∧ listStrictMajority [true, false] = false ∧ listNonpositiveMargin [true, false] true = true := by decide diff --git a/ComplexityTests/UniformNat.lean b/ComplexityTests/UniformNat.lean index 0edb0cbd21..371125d5dd 100644 --- a/ComplexityTests/UniformNat.lean +++ b/ComplexityTests/UniformNat.lean @@ -12,7 +12,7 @@ import Mathlib.Data.ZMod.Basic namespace ComplexityTests.UniformNat -open Cslib Cslib.Probability Turing.MultiTapeTM +open Cslib Cslib.ProbComp Cslib.Probability Turing.MultiTapeTM -- Binary words are most significant bit first; long words saturate before unary output grows. example : BitString.binaryValue [true, false, false] = 4 := by decide diff --git a/abstracts/ComplexityAbstracts/GSWSecurityBridge.lean b/abstracts/ComplexityAbstracts/GSWSecurityBridge.lean index 4f53326116..baa9d82476 100644 --- a/abstracts/ComplexityAbstracts/GSWSecurityBridge.lean +++ b/abstracts/ComplexityAbstracts/GSWSecurityBridge.lean @@ -208,7 +208,7 @@ def ChosenMessageSecure : Prop := nndist (probability (chosenMessageGame choose guess false security)) (probability (chosenMessageGame choose guess true security))) -open Cslib Cslib.Probability Turing.MultiTapeTM +open Cslib Cslib.ProbComp Cslib.Probability Turing.MultiTapeTM private theorem independentList_eval {α : Type} (count : ℕ) (program : ProbComp α) : independentList count (ProbComp.eval program) =