From b032a162f653b4db2b1782c6a9c2f0f9ef473cfd Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 31 Oct 2026 10:25:54 +0000 Subject: [PATCH 1/3] refactor(Crypto): replace projection chains across Pseudoentropy, Stretch, and DDH modules (#1764) --- .../Computational/DiffieHellman/MultiDDH.lean | 12 +++-- .../DiscreteLog/SchnorrGroup.lean | 48 ++++++++++--------- .../Crypto/Computational/GeneratorXor.lean | 13 ++--- .../Crypto/Computational/NaorReingold.lean | 9 ++-- .../Computational/NaorReingold/Security.lean | 18 ++++--- .../Crypto/Computational/OneWay/MCSP.lean | 3 +- .../Crypto/Computational/OneWay/NP.lean | 9 +++- .../Pseudoentropy/DenseMask.lean | 2 +- .../Computational/Pseudoentropy/HashPair.lean | 9 ++-- .../Pseudoentropy/LabelExtraction.lean | 10 ++-- .../Pseudoentropy/MatrixExtraction.lean | 19 +++++--- .../Pseudoentropy/RepeatedExtraction.lean | 4 +- .../Computational/Pseudoentropy/Seed.lean | 3 +- .../Pseudoentropy/Selection.lean | 4 +- .../Pseudoentropy/ThreeSource.lean | 13 ++--- .../ThreeSource/Amplification.lean | 9 ++-- .../Pseudoentropy/ThreeSource/Candidates.lean | 9 ++-- .../Pseudoentropy/ThreeSource/Padding.lean | 10 ++-- .../Pseudoentropy/ThreeSource/Seeded.lean | 9 ++-- .../Pseudoentropy/WordExtraction.lean | 13 +++-- .../PseudorandomFunction/Coins.lean | 3 +- Complexity/Crypto/Computational/Stretch.lean | 6 +-- .../Computational/Stretch/Quantitative.lean | 29 ++++++----- .../Crypto/Computational/UniformChoice.lean | 4 +- .../PRG/NisanWigderson/Sampling.lean | 5 +- 25 files changed, 164 insertions(+), 109 deletions(-) diff --git a/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean b/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean index 233ecc65e0..5f594098a0 100644 --- a/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean +++ b/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean @@ -76,8 +76,10 @@ theorem ddhFixedUWordRerandomize_encode (d : F.Desc) (u v w : F.Carrier d) (σ theorem computableInPolyTime_ddhFixedUWordRerandomize : ComputableInPolyTime (fun input : F.Desc × List Bool × List Bool × List Bool × ℕ × ℕ => - F.ddhFixedUWordRerandomize input.1 input.2.1 input.2.2.1 input.2.2.2.1 - input.2.2.2.2.1 input.2.2.2.2.2) + F.ddhFixedUWordRerandomize input.1 (Prod.fst input.2) (Prod.fst (Prod.snd input.2)) + (Prod.fst (Prod.snd (Prod.snd input.2))) + (Prod.fst (Prod.snd (Prod.snd (Prod.snd input.2)))) + (Prod.snd (Prod.snd (Prod.snd (Prod.snd input.2))))) (encPair F.encDesc (encPair encBits (encPair encBits (encPair encBits (encPair encNat encNat))))) (encPair encBits encBits) := by @@ -288,9 +290,11 @@ theorem advantage_multiDDH_le (d : F.Desc) (ι : Type*) [Fintype ι] [DecidableE (F.multiDDHIdealTupleLaw d ι).bind (test (α • F.generator d))) ≤ Game.advantage ((F.ddhRealTupleLaw d).bind fun t => - (F.multiDDHRerandomizeLaw d ι t.1 t.2.1 t.2.2).bind (test t.1)) + let vw := t.2 + (F.multiDDHRerandomizeLaw d ι t.1 vw.1 vw.2).bind (test t.1)) ((F.ddhIdealTupleLaw d).bind fun t => - (F.multiDDHRerandomizeLaw d ι t.1 t.2.1 t.2.2).bind (test t.1)) + + let vw := t.2 + (F.multiDDHRerandomizeLaw d ι t.1 vw.1 vw.2).bind (test t.1)) + (F.order d : ℝ≥0)⁻¹ := by have hreal : ((F.ddhRealTupleLaw d).bind fun t => diff --git a/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean b/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean index b2abfcbe5b..3429292f14 100644 --- a/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean +++ b/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean @@ -57,49 +57,51 @@ structure Valid (d : ℕ × ℕ × ℕ) : Prop where /-- The modulus is prime. -/ prime_modulus : d.1.Prime /-- The group order is prime. -/ - prime_order : d.2.1.Prime + prime_order : (Prod.fst d.2).Prime /-- The generator is not `0` or `1`. -/ - one_lt_generator : 1 < d.2.2 + one_lt_generator : 1 < Prod.snd d.2 /-- The generator is a reduced residue. -/ - generator_lt : d.2.2 < d.1 + generator_lt : Prod.snd d.2 < d.1 /-- The generator has order dividing `q`. -/ - generator_pow : d.2.2 ^ d.2.1 % d.1 = 1 + generator_pow : Prod.snd d.2 ^ Prod.fst d.2 % d.1 = 1 /-- Valid Schnorr-group descriptions. -/ abbrev Desc : Type := {d : ℕ × ℕ × ℕ // Valid d} /-- The generator as a unit modulo `p`. -/ -def generatorUnit (d : Desc) : (ZMod d.1.1)ˣ := - ZMod.unitOfCoprime d.1.2.2 ((Nat.coprime_comm.mp ((d.2.prime_modulus.coprime_iff_not_dvd).mpr - (Nat.not_dvd_of_pos_of_lt (by have := d.2.one_lt_generator; lia) d.2.generator_lt)))) +def generatorUnit (d : Desc) : (ZMod d.val.1)ˣ := + ZMod.unitOfCoprime (Prod.snd d.val.2) ((Nat.coprime_comm.mp + ((d.2.prime_modulus.coprime_iff_not_dvd).mpr + (Nat.not_dvd_of_pos_of_lt (by have := d.2.one_lt_generator; lia) d.2.generator_lt)))) /-- The Schnorr group of a description, written additively. -/ abbrev Carrier (d : Desc) : Type := Additive (Subgroup.zpowers (generatorUnit d)) -instance (d : Desc) : Fact d.1.2.1.Prime := ⟨d.2.prime_order⟩ +instance (d : Desc) : Fact (Prod.fst d.val.2).Prime := ⟨d.2.prime_order⟩ /-- The generator has order dividing `q`. -/ -theorem generatorUnit_pow_order (d : Desc) : generatorUnit d ^ d.1.2.1 = 1 := by +theorem generatorUnit_pow_order (d : Desc) : generatorUnit d ^ Prod.fst d.val.2 = 1 := by ext rw [Units.val_pow_eq_pow_val, generatorUnit, ZMod.coe_unitOfCoprime, Units.val_one, ← Nat.cast_pow, ← ZMod.natCast_mod, d.2.generator_pow, Nat.cast_one] /-- Every element of the Schnorr group has order dividing `q`. -/ -theorem pow_order (d : Desc) (x : Subgroup.zpowers (generatorUnit d)) : x ^ d.1.2.1 = 1 := by +theorem pow_order (d : Desc) (x : Subgroup.zpowers (generatorUnit d)) : + x ^ Prod.fst d.val.2 = 1 := by obtain ⟨k, hk⟩ := Subgroup.mem_zpowers_iff.mp x.2 ext rw [Subgroup.coe_pow, ← hk, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, generatorUnit_pow_order, one_zpow, Subgroup.coe_one] -instance (d : Desc) : Module (ZMod d.1.2.1) (Carrier d) := +instance (d : Desc) : Module (ZMod (Prod.fst d.val.2)) (Carrier d) := AddCommMonoid.zmodModule fun x => Additive.toMul.injective (by rw [toMul_nsmul, pow_order, toMul_zero]) -instance (d : Desc) : NeZero d.1.1 := ⟨d.2.prime_modulus.ne_zero⟩ +instance (d : Desc) : NeZero d.val.1 := ⟨d.2.prime_modulus.ne_zero⟩ /-- The generator is not the identity. -/ theorem generatorUnit_ne_one (d : Desc) : generatorUnit d ≠ 1 := fun h => by - have hval := congrArg (fun u : (ZMod d.1.1)ˣ => (u : ZMod d.1.1).val) h + have hval := congrArg (fun u : (ZMod d.val.1)ˣ => (u : ZMod d.val.1).val) h simp only [generatorUnit, ZMod.coe_unitOfCoprime, ZMod.val_natCast, Nat.mod_eq_of_lt d.2.generator_lt, Units.val_one, ZMod.val_one_eq_one_mod, Nat.mod_eq_of_lt d.2.prime_modulus.one_lt] at hval @@ -110,19 +112,19 @@ def generator (d : Desc) : Carrier d := Additive.ofMul ⟨generatorUnit d, Subgroup.mem_zpowers _⟩ /-- The Schnorr group has `q` elements. -/ -theorem card_carrier (d : Desc) : Nat.card (Carrier d) = d.1.2.1 := by +theorem card_carrier (d : Desc) : Nat.card (Carrier d) = Prod.fst d.val.2 := by change Nat.card (Subgroup.zpowers (generatorUnit d)) = d.1.2.1 rw [Nat.card_zpowers, orderOf_eq_prime (generatorUnit_pow_order d) (generatorUnit_ne_one d)] /-- The generator is not the identity of the Schnorr group. -/ theorem generator_ne_zero (d : Desc) : generator d ≠ 0 := fun h => generatorUnit_ne_one d (congrArg (fun x : Carrier d => ((Additive.toMul x : - Subgroup.zpowers (generatorUnit d)) : (ZMod d.1.1)ˣ)) h) + Subgroup.zpowers (generatorUnit d)) : (ZMod d.val.1)ˣ)) h) /-- Elements are encoded by the binary digits of their residues modulo `p`. -/ def encode (d : Desc) (x : Carrier d) : List Bool := - ((((Additive.toMul x : Subgroup.zpowers (generatorUnit d)) : (ZMod d.1.1)ˣ) : - ZMod d.1.1).val).bits + ((((Additive.toMul x : Subgroup.zpowers (generatorUnit d)) : (ZMod d.val.1)ˣ) : + ZMod d.val.1).val).bits /-- Distinct elements have distinct encodings. -/ theorem encode_injective (d : Desc) : Function.Injective (encode d) := fun _ _ h => @@ -134,7 +136,7 @@ private theorem ofBits_bits (n : ℕ) : ofBits n.bits = n := Nat.foldr_bit_bits /-- Multiplication modulo `p` of encoded residues. -/ def add (input : Desc × List Bool × List Bool) : List Bool := - (ofBits input.2.1 * ofBits input.2.2 % input.1.1.1).bits + (ofBits (Prod.fst input.2) * ofBits (Prod.snd input.2) % input.1.val.1).bits /-- `add` multiplies encoded group elements. -/ theorem add_encode (d : Desc) (x y : Carrier d) : @@ -143,17 +145,17 @@ theorem add_encode (d : Desc) (x y : Carrier d) : /-- Exponentiation modulo `p` of an encoded residue. -/ def smul (input : Desc × ℕ × List Bool) : List Bool := - (ofBits input.2.2 ^ input.2.1 % input.1.1.1).bits + (ofBits (Prod.snd input.2) ^ Prod.fst input.2 % input.1.val.1).bits /-- `smul` raises encoded group elements to natural powers. -/ theorem smul_encode (d : Desc) (a : ℕ) (x : Carrier d) : - smul (d, a, encode d x) = encode d ((a : ZMod d.1.2.1) • x) := by + smul (d, a, encode d x) = encode d ((a : ZMod (Prod.fst d.val.2)) • x) := by rw [Nat.cast_smul_eq_nsmul] simp only [smul, encode, ofBits_bits, toMul_nsmul, Subgroup.coe_pow, Units.val_pow_eq_pow_val] rw [← ZMod.val_natCast, Nat.cast_pow, ZMod.natCast_zmod_val] /-- The encoded generator is the binary digits of `g`. -/ -theorem encode_generator (d : Desc) : encode d (generator d) = d.1.2.2.bits := by +theorem encode_generator (d : Desc) : encode d (generator d) = (Prod.snd d.val.2).bits := by change (((generatorUnit d : (ZMod d.1.1)ˣ) : ZMod d.1.1).val).bits = _ rw [generatorUnit, ZMod.coe_unitOfCoprime, ZMod.val_natCast, Nat.mod_eq_of_lt d.2.generator_lt] @@ -170,7 +172,7 @@ private theorem computableInPolyTime_val : /-- The group order is computable in polynomial time from the description. -/ theorem computableInPolyTime_order : - ComputableInPolyTime (fun d : Desc => d.1.2.1) encDesc encNat := by + ComputableInPolyTime (fun d : Desc => Prod.fst d.val.2) encDesc encNat := by have := computableInPolyTime_val fun_prop @@ -208,7 +210,7 @@ of prime order with efficient operations. -/ def schnorrGroups : PrimeOrderGroupFamily where Desc := SchnorrGroup.Desc encDesc := SchnorrGroup.encDesc - order d := d.1.2.1 + order d := Prod.fst d.val.2 prime_order d := d.2.prime_order Carrier := Carrier generator := generator diff --git a/Complexity/Crypto/Computational/GeneratorXor.lean b/Complexity/Crypto/Computational/GeneratorXor.lean index 3a94453e20..1f6e257b72 100644 --- a/Complexity/Crypto/Computational/GeneratorXor.lean +++ b/Complexity/Crypto/Computational/GeneratorXor.lean @@ -71,8 +71,8 @@ theorem isPolyTime_generate {α : Type} {input : α ↪ List Bool} (hcount : ComputableInPolyTime count input encUnary) (hseedBits : ComputableInPolyTime seedBits input encUnary) (houtputBits : ComputableInPolyTime outputBits input encUnary) - (hgenerator : ComputableInPolyTime (fun pair => generator pair.1.1 pair.1.2 pair.2) - (encPair (encPair input encUnary) encBits) encBits) + (hgenerator : ComputableInPolyTime (fun pair => generator (Prod.fst pair.1) (Prod.snd pair.1) + pair.2) (encPair (encPair input encUnary) encBits) encBits) (hseed : ComputableInPolyTime seed input encBits) : ComputableInPolyTime (fun a => generate (count a) (seedBits a) (outputBits a) (generator a) (seed a)) input encBits := by @@ -198,8 +198,8 @@ theorem isPPTOn_test {α : Type} {input : α ↪ List Bool} (hseedBits : ComputableInPolyTime seedBits input encUnary) (houtputBits : ComputableInPolyTime outputBits input encUnary) (hindex : ComputableInPolyTime index input encUnary) - (hgenerator : ComputableInPolyTime (fun pair => generator pair.1.1 pair.1.2 pair.2) - (encPair (encPair input encUnary) encBits) encBits) + (hgenerator : ComputableInPolyTime (fun pair => generator (Prod.fst pair.1) (Prod.snd pair.1) + pair.2) (encPair (encPair input encUnary) encBits) encBits) (hadversary : IsPPTOn (encPair input encBits) encBool (fun pair => adversary pair.1 pair.2)) (hchallenge : ComputableInPolyTime challenge input encBits) : @@ -252,12 +252,13 @@ theorem indistinguishable {generator : ℕ → ℕ → List Bool → List Bool} (hcount : ComputableInPolyTime count encUnary encUnary) (hseedBits : ComputableInPolyTime seedBits encUnary encUnary) (houtputBits : ComputableInPolyTime outputBits encUnary encUnary) - (hgenerator : ComputableInPolyTime (fun input => generator input.1.1 input.1.2 input.2) + (hgenerator : ComputableInPolyTime + (fun input => generator (Prod.fst input.1) (Prod.snd input.1) input.2) (encPair (encPair encUnary encUnary) encBits) encBits) (hchoose : ∀ᶠ n in Filter.atTop, choose n < count n) (hsecure : ∀ adversary : ℕ → ℕ → List Bool → ProbComp Bool, IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => adversary input.1.1 input.1.2 input.2) → + encBool (fun input => adversary (Prod.fst input.1) (Prod.snd input.1) input.2) → Negligible (fun n => Game.advantage (((uniformList (seedBits n)).map (generator n (choose n))).bind (fun word => ProbComp.eval (adversary n (choose n) word))) diff --git a/Complexity/Crypto/Computational/NaorReingold.lean b/Complexity/Crypto/Computational/NaorReingold.lean index c89f2a3379..c9f2f38e0e 100644 --- a/Complexity/Crypto/Computational/NaorReingold.lean +++ b/Complexity/Crypto/Computational/NaorReingold.lean @@ -321,7 +321,8 @@ theorem computableInPolyTime_naorReingoldProdNat : theorem computableInPolyTime_naorReingoldWordSuffix : ComputableInPolyTime (fun input : F.Desc × List Bool × List ℕ × List Bool => - F.naorReingoldWordSuffix input.1 input.2.1 input.2.2.1 input.2.2.2) + F.naorReingoldWordSuffix input.1 (Prod.fst input.2) (Prod.fst (Prod.snd input.2)) + (Prod.snd (Prod.snd input.2))) (encPair F.encDesc (encPair encBits (encPair (encList encNat) encBits))) encBits := by have hd : ComputableInPolyTime (fun input : F.Desc × List Bool × List ℕ × List Bool => input.1) @@ -358,7 +359,8 @@ theorem computableInPolyTime_naorReingoldWordSuffix : theorem computableInPolyTime_naorReingoldWordEval : ComputableInPolyTime (fun input : F.Desc × ℕ × List ℕ × List Bool => - F.naorReingoldWordEval input.1 input.2.1 input.2.2.1 input.2.2.2) + F.naorReingoldWordEval input.1 (Prod.fst input.2) (Prod.fst (Prod.snd input.2)) + (Prod.snd (Prod.snd input.2))) (encPair F.encDesc (encPair encNat (encPair (encList encNat) encBits))) encBits := by have hd : ComputableInPolyTime (fun input : F.Desc × ℕ × List ℕ × List Bool => input.1) @@ -602,7 +604,8 @@ rerandomize it into a `BitString k`-indexed family via `multiDDHRerandomizeLaw` noncomputable def naorReingoldLevelDDHDistinguisher (d : F.Desc) {n : ℕ} (k : ℕ) (hk : k < n) (adv : OracleComp (fun _ : BitString n => F.Carrier d) Bool) (t : F.Carrier d × F.Carrier d × F.Carrier d) : PMF Bool := - (F.multiDDHRerandomizeLaw d (BitString k) t.1 t.2.1 t.2.2).bind + let vw := t.2 + (F.multiDDHRerandomizeLaw d (BitString k) t.1 vw.1 vw.2).bind (F.naorReingoldLevelTest d k hk adv t.1) /-- Under `multiDDHRealTupleLaw`, `naorReingoldLevelTest` reproduces `naorReingoldHybridGame` at diff --git a/Complexity/Crypto/Computational/NaorReingold/Security.lean b/Complexity/Crypto/Computational/NaorReingold/Security.lean index 19c11bef21..5d8b3d50a5 100644 --- a/Complexity/Crypto/Computational/NaorReingold/Security.lean +++ b/Complexity/Crypto/Computational/NaorReingold/Security.lean @@ -467,12 +467,16 @@ noncomputable def naorReingoldToDDHDistinguisher (inLen : ℕ → ℕ) let m := inLen n let k ← ProbComp.sampleDyadicIndex m if k < m then do - let αs ← OracleComp.replicate (m - (k + 1)) (F.sampleNaorReingoldExp n input.1) + let d := input.1 + let uvw := input.2 + let u := uvw.1 + let vw := uvw.2 + let αs ← OracleComp.replicate (m - (k + 1)) (F.sampleNaorReingoldExp n d) Prod.fst <$> (OracleComp.interpret (ProbOracleComp.handler (fun r => StateT.lift (ProbComp.unifFin r)) - (fun request => F.naorReingoldFrontierOracle n m k input.1 - input.2.1 input.2.2.1 input.2.2.2 αs request.2)) - (adversary n (F.encDesc input.1))).run [] + (fun request => F.naorReingoldFrontierOracle n m k d + u vw.1 vw.2 αs request.2)) + (adversary n (F.encDesc d))).run [] else pure false private theorem isPPTOn_sampleNaorReingoldPair (F : PrimeOrderGroupFamily) @@ -2009,8 +2013,10 @@ theorem computableInPolyTime_naorReingoldHashedWordEval {bound : F.Desc → ℕ} (hbound : ComputableInPolyTime bound F.encDesc encUnary) : ComputableInPolyTime (fun input : ℕ × F.Desc × List Bool × ℕ × List ℕ × List Bool => - F.naorReingoldHashedWordEval input.1 bound input.2.1 input.2.2.1 input.2.2.2.1 - input.2.2.2.2.1 input.2.2.2.2.2) + F.naorReingoldHashedWordEval input.1 bound (Prod.fst input.2) (Prod.fst (Prod.snd input.2)) + (Prod.fst (Prod.snd (Prod.snd input.2))) + (Prod.fst (Prod.snd (Prod.snd (Prod.snd input.2)))) + (Prod.snd (Prod.snd (Prod.snd (Prod.snd input.2))))) (encPair encUnary (encPair F.encDesc (encPair encBits (encPair encNat (encPair (encList encNat) encBits))))) diff --git a/Complexity/Crypto/Computational/OneWay/MCSP.lean b/Complexity/Crypto/Computational/OneWay/MCSP.lean index 2a3d0937e7..e7a03ae725 100644 --- a/Complexity/Crypto/Computational/OneWay/MCSP.lean +++ b/Complexity/Crypto/Computational/OneWay/MCSP.lean @@ -274,7 +274,8 @@ theorem computableInPolyTime_tableQueries (d : ℕ) : /-- The instance read from the answers is computed in polynomial time. -/ theorem computableInPolyTime_tableInstance (d : ℕ) : ComputableInPolyTime (fun pair : (ℕ × List Bool) × List Bool => - tableInstance (tableArity d pair.1.1) pair.2) (encPair (encPair encUnary encBits) encBits) + tableInstance (tableArity d (Prod.fst pair.1)) pair.2) + (encPair (encPair encUnary encBits) encBits) MCSP.encInstance := by refine .of_tidy ?_ have harity : ComputableTidilyInPolyTime (fun pair : (ℕ × List Bool) × List Bool => diff --git a/Complexity/Crypto/Computational/OneWay/NP.lean b/Complexity/Crypto/Computational/OneWay/NP.lean index bc97be611f..67954898cd 100644 --- a/Complexity/Crypto/Computational/OneWay/NP.lean +++ b/Complexity/Crypto/Computational/OneWay/NP.lean @@ -80,7 +80,7 @@ open Complexity Probability Turing.MultiTapeTM ComputableTidilyInPolyTime /-- **The preimage-prefix problem** of `f`: the instances `(n, y, u)` such that some input `x` of length `n` that starts with `u` satisfies `f x = y`. -/ def preimagePrefix (f : List Bool → List Bool) : Set (ℕ × List Bool × List Bool) := - {p | ∃ x : List Bool, x.length = p.1 ∧ p.2.2 <+: x ∧ f x = p.2.1} + {p | let yu := p.2; ∃ x : List Bool, x.length = p.1 ∧ yu.2 <+: x ∧ f x = yu.1} /-- The encoding of instances of the preimage-prefix problem: the length `n` in unary, then the image and the prefix. -/ @@ -95,7 +95,12 @@ variable {f : List Bool → List Bool} prefix. -/ def preimagePrefixVerifier (f : List Bool → List Bool) (p : (ℕ × List Bool × List Bool) × List Bool) : Bool := - decide (p.1.2.2.length ≤ p.1.1) && f (p.1.2.2 ++ p.2.take (p.1.1 - p.1.2.2.length)) == p.1.2.1 + let inst := p.1 + let n := inst.1 + let yu := inst.2 + let y := yu.1 + let u := yu.2 + decide (u.length ≤ n) && f (u ++ p.2.take (n - u.length)) == y /-- The unary length is at most as long as the encoded instance. -/ private theorem le_length_encPreimagePrefix (p : ℕ × List Bool × List Bool) : diff --git a/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean b/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean index 9ee9d0cdb5..f4aa76dce9 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean @@ -63,7 +63,7 @@ theorem HasGap.eventually_exists_indexed_mask {pair : SamplablePair} {gap : ℕ (hpair : pair.HasGap gap) (test : ℕ → ℕ → List (List Bool × Bool) → ProbComp Bool) (htest : IsPPTOn (encPair (encPair encUnary encUnary) (encList (encPair encBits encBool))) encBool - (fun input => test input.1.1 input.1.2 input.2)) + (fun input => test (Prod.fst input.1) (Prod.snd input.1) input.2)) {candidates count densityBound inverseGap : ℕ → ℕ} {numerator : ℕ → ℕ → ℕ} (hcandidates : ComputableInPolyTime candidates encUnary encUnary) (hcount : ComputableInPolyTime count encUnary encUnary) diff --git a/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean b/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean index ee66a2f55f..460dcd0a06 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean @@ -154,9 +154,12 @@ theorem computableInPolyTime_wordObservation {α : Type} {encode : α ↪ List B /-- Encode a finite public observation using the chosen image representation. -/ def encodeObservation {n count : ℕ} {Image : Type*} (encodeImage : Image → List Bool) (observation : Observation n count Image) : List Bool := - wordObservation (encodeImage observation.2.2.1) observation.1.val - (List.ofFn observation.2.1.1) (List.ofFn observation.2.2.2) - (List.ofFn observation.2.1.2) + let rest := observation.2 + let mq := rest.1 + let idig := rest.2 + wordObservation (encodeImage idig.1) observation.1.val + (List.ofFn mq.1) (List.ofFn idig.2) + (List.ofFn mq.2) /-- Encoding loses none of the public information, even though the digest's width varies. -/ theorem encodeObservation_injective {n count : ℕ} {Image : Type*} diff --git a/Complexity/Crypto/Computational/Pseudoentropy/LabelExtraction.lean b/Complexity/Crypto/Computational/Pseudoentropy/LabelExtraction.lean index e024fbe9ac..d7cfc9c845 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/LabelExtraction.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/LabelExtraction.lean @@ -63,8 +63,9 @@ theorem HasGap.indexed_extracted_advantage_negligible {pair : SamplablePair} {ga (test : ∀ n i, List (List Bool) × Seed n i × Output n i → ProbComp Bool) (htest : IsPPTOn (encPair (encPair encUnary encUnary) (encList (encPair encBits encBool))) encBool - (fun input => extractLabels (seed input.1.1 input.1.2) (hash input.1.1 input.1.2) - input.2 >>= test input.1.1 input.1.2)) + (fun input => extractLabels (seed (Prod.fst input.1) (Prod.snd input.1)) + (hash (Prod.fst input.1) (Prod.snd input.1)) + input.2 >>= test (Prod.fst input.1) (Prod.snd input.1))) {candidates count densityBound : ℕ → ℕ} {numerator : ℕ → ℕ → ℕ} {slack : ℕ → ℝ} (hcandidates : ComputableInPolyTime candidates encUnary encUnary) (hcount : ComputableInPolyTime count encUnary encUnary) @@ -178,8 +179,9 @@ theorem HasGap.extract_indexed_labels {pair : SamplablePair} {gap : ℕ → ℝ} (test : ∀ n i, List (List Bool) × Seed n i × BitString (outputBits n i) → ProbComp Bool) (htest : IsPPTOn (encPair (encPair encUnary encUnary) (encList (encPair encBits encBool))) encBool - (fun input => extractLabels (seed input.1.1 input.1.2) (hash input.1.1 input.1.2) - input.2 >>= test input.1.1 input.1.2)) + (fun input => extractLabels (seed (Prod.fst input.1) (Prod.snd input.1)) + (hash (Prod.fst input.1) (Prod.snd input.1)) + input.2 >>= test (Prod.fst input.1) (Prod.snd input.1))) (hcandidates : ComputableInPolyTime candidates encUnary encUnary) (hslack : ComputableInPolyTime inverseSlack encUnary encUnary) {numerator : ℕ → ℕ → ℕ} {densityBound : ℕ → ℕ} diff --git a/Complexity/Crypto/Computational/Pseudoentropy/MatrixExtraction.lean b/Complexity/Crypto/Computational/Pseudoentropy/MatrixExtraction.lean index 5c0ab5f876..faa9b4e46b 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/MatrixExtraction.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/MatrixExtraction.lean @@ -63,8 +63,9 @@ theorem extractMatrixLabels_result {Observation Label : Type} (inputBits outputB {result : List Observation × List Bool × List Bool} (hresult : result ∈ (ProbComp.eval (extractMatrixLabels inputBits outputBits prepare samples)).support) : - result.1 = samples.map Prod.fst ∧ result.2.1.length = outputBits * inputBits ∧ - result.2.2.length = outputBits := by + let sd := result.2 + result.1 = samples.map Prod.fst ∧ sd.1.length = outputBits * inputBits ∧ + sd.2.length = outputBits := by simp only [extractMatrixLabels, extractLabels, bind_pure_comp, ProbComp.eval_map, BitString.eval_sampleList, PMF.mem_support_map_iff] at hresult obtain ⟨seed, hseed, rfl⟩ := hresult @@ -104,7 +105,9 @@ theorem eval_extractMatrixLabels {Observation Label : Type} (inputBits outputBit (ProbComp.eval (extractLabels (ProbComp.uniform (BitString (outputBits * inputBits))) (fun seed labels => LinearHash.hash (blocksEquiv (m := outputBits) (k := inputBits) seed) (ofList inputBits (prepare labels))) samples)).map - (fun result => (result.1, List.ofFn result.2.1, List.ofFn result.2.2)) := by + (fun result => + let sd := result.2 + (result.1, List.ofFn sd.1, List.ofFn sd.2)) := by have hrow (word : List Bool) : listRow inputBits 0 word = List.ofFn (ofList inputBits word) := listRow_eq_ofFn inputBits (0 : Fin 1) word @@ -118,7 +121,9 @@ theorem eval_extractMatrixLabelsIdeal {Observation : Type} (source : ProbComp Ob ProbComp.eval (extractMatrixLabelsIdeal source count inputBits outputBits) = (extractLabelsIdeal (Output := BitString outputBits) source count (ProbComp.uniform (BitString (outputBits * inputBits)))).map - (fun result => (result.1, List.ofFn result.2.1, List.ofFn result.2.2)) := by + (fun result => + let sd := result.2 + (result.1, List.ofFn sd.1, List.ofFn sd.2)) := by simp only [extractMatrixLabelsIdeal, ProbComp.eval_bind, ProbComp.eval_pure, extractLabelsIdeal, ProbComp.eval_uniform, eval_sampleList, uniformList, Function.comp_def, PMF.map, PMF.bind_bind, PMF.pure_bind] @@ -131,7 +136,8 @@ theorem eval_extractMatrixLabelsIdeal_bind {Observation Output : Type} (next : List Observation → List Bool → ProbComp Output) : ProbComp.eval (do let result ← extractMatrixLabelsIdeal source count inputBits outputBits - next result.1 (result.2.1 ++ result.2.2)) = + let sd := result.2 + next result.1 (sd.1 ++ sd.2)) = ProbComp.eval (do let observations ← OracleComp.replicate count source let bits ← BitString.sampleList (outputBits * inputBits + outputBits) @@ -147,7 +153,8 @@ theorem eval_extractMatrixLabelsIdeal_append {Observation : Type} (next : List Observation → ProbComp (List Bool)) : ProbComp.eval (do let result ← extractMatrixLabelsIdeal source count inputBits outputBits - (fun front => front ++ (result.2.1 ++ result.2.2)) <$> next result.1) = + let sd := result.2 + (fun front => front ++ (sd.1 ++ sd.2)) <$> next result.1) = ProbComp.eval (do let observations ← OracleComp.replicate count source let front ← next observations diff --git a/Complexity/Crypto/Computational/Pseudoentropy/RepeatedExtraction.lean b/Complexity/Crypto/Computational/Pseudoentropy/RepeatedExtraction.lean index 8e472347b6..3c836e7c7e 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/RepeatedExtraction.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/RepeatedExtraction.lean @@ -128,7 +128,7 @@ theorem isPPTOn_extractLabels {Param Observation Seed Output : Type} {input : Pa {seed : Param → ProbComp Seed} {hash : Param → Seed → List Bool → Output} {samples : Param → List (Observation × Bool)} (hseed : IsPPTOn input key seed) - (hhash : ComputableInPolyTime (fun pair => hash pair.1.1 pair.1.2 pair.2) + (hhash : ComputableInPolyTime (fun pair => hash (Prod.fst pair.1) (Prod.snd pair.1) pair.2) (encPair (encPair input key) encBits) output) (hsamples : ComputableInPolyTime samples input (encList (encPair observation encBool))) : IsPPTOn input (encPair (encList observation) (encPair key output)) @@ -143,7 +143,7 @@ theorem isPPTOn_extractLabels_list {Param Observation Label Seed Output : Type} {seed : Param → ProbComp Seed} {hash : Param → Seed → List Label → Output} {samples : Param → List (Observation × Label)} (hseed : IsPPTOn input key seed) - (hhash : ComputableInPolyTime (fun pair => hash pair.1.1 pair.1.2 pair.2) + (hhash : ComputableInPolyTime (fun pair => hash (Prod.fst pair.1) (Prod.snd pair.1) pair.2) (encPair (encPair input key) (encList label)) output) (hsamples : ComputableInPolyTime samples input (encList (encPair observation label))) : IsPPTOn input (encPair (encList observation) (encPair key output)) diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Seed.lean b/Complexity/Crypto/Computational/Pseudoentropy/Seed.lean index 800fffd0a8..2c5898014d 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/Seed.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/Seed.lean @@ -212,7 +212,8 @@ theorem isPPTOn_sampleWithSeed : IsPPTOn encUnary /-- The efficient program exactly realizes the finite joint experiment with its retained seed. -/ theorem eval_sampleWithSeed (n : ℕ) : ProbComp.eval (seed.sampleWithSeed n) = (seed.jointWithSeed n).map (fun result => - ((pair.encode n result.1.1, result.1.2), List.ofFn result.2)) := by + let obs := result.1 + ((pair.encode n obs.1, obs.2), List.ofFn result.2)) := by simp only [sampleWithSeed, bind_pure_comp, ProbComp.eval_map, jointWithSeed, PMF.map_comp, Function.comp_def, seed.encode_output] simp only [BitString.eval_sampleList, BitString.uniformList, PMF.map_comp, Function.comp_def] diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Selection.lean b/Complexity/Crypto/Computational/Pseudoentropy/Selection.lean index 1fc8e8ad52..5e62b336a0 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/Selection.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/Selection.lean @@ -70,7 +70,7 @@ theorem isPPTOn_selectPredictor {α : Type} {input : α ↪ List Bool} (htrials : ComputableInPolyTime trials input encUnary) (hsource : IsPPTOn input (encPair encBits encBool) source) (hpredict : IsPPTOn (encPair (encPair input encUnary) encBits) - encBool (fun x => predict x.1.1 x.1.2 x.2)) + encBool (fun x => predict (Prod.fst x.1) (Prod.snd x.1) x.2)) (hobservation : ComputableInPolyTime observation input encBits) : IsPPTOn input encBool (fun a => selectPredictor (count a) (trials a) (source a) (predict a) (observation a)) := by @@ -124,7 +124,7 @@ theorem HasGap.eventually_indexed_error_ge {pair : SamplablePair} {gap : ℕ → (hgap : pair.HasGap gap) (predict : ℕ → ℕ → List Bool → ProbComp Bool) (hpredict : IsPPTOn (encPair (encPair encUnary encUnary) encBits) encBool - (fun x => predict x.1.1 x.1.2 x.2)) + (fun x => predict (Prod.fst x.1) (Prod.snd x.1) x.2)) {count inverseTolerance : ℕ → ℕ} (hcount : ComputableInPolyTime count encUnary encUnary) (htolerance : ComputableInPolyTime inverseTolerance encUnary encUnary) diff --git a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource.lean b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource.lean index 8c819ad906..da6d3f841c 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource.lean @@ -62,7 +62,7 @@ open Probability BitString Turing.MultiTapeTM noncomputable def finish (bound observationBits : ℕ) (middle : List (List Bool) × List Bool × List Bool) : ProbComp (List Bool) := do let first ← extractWordObservations bound observationBits middle.1 - return first ++ (middle.2.1 ++ middle.2.2) + return first ++ (Prod.fst middle.2 ++ Prod.snd middle.2) /-- The last observation hash composes with a certified intermediate result. -/ theorem isPPTOn_finish {α : Type} {input : α ↪ List Bool} {bound observationBits : α → ℕ} @@ -84,7 +84,7 @@ noncomputable def extract (count seedBits bound observationBits labelBits remain let third ← extractWordSeeds count seedBits remainingBits samples let middle ← extractWordLabels count labelBits third.1 let front ← finish bound observationBits middle - return front ++ (third.2.1 ++ third.2.2) + return front ++ (Prod.fst third.2 ++ Prod.snd third.2) /-- The complete three-component program is PPT from ordinary sampler and size certificates. -/ theorem isPPTOn_extract {α : Type} {input : α ↪ List Bool} @@ -177,7 +177,7 @@ def outputLength (count seedBits bound observationBits labelBits remainingBits : The statement also covers zero-sized components and malformed retained seeds. -/ theorem length_extract (count seedBits bound observationBits labelBits remainingBits : ℕ) (source : ProbComp ((List Bool × Bool) × List Bool)) - (hbound : ∀ sample ∈ (ProbComp.eval source).support, sample.1.1.length ≤ bound) + (hbound : ∀ sample ∈ (ProbComp.eval source).support, (Prod.fst sample.1).length ≤ bound) {output : List Bool} (houtput : output ∈ (ProbComp.eval (extract count seedBits bound observationBits labelBits remainingBits source)).support) : output.length = outputLength count seedBits bound observationBits labelBits remainingBits := by @@ -255,7 +255,8 @@ theorem eval_ideal_remaining let third ← extractMatrixLabelsIdeal source count (count * seedBits) remainingBits let middle ← extractWordLabels count labelBits third.1 let front ← finish bound observationBits middle - return front ++ (third.2.1 ++ third.2.2)) = + let thirdSd := third.2 + return front ++ (thirdSd.1 ++ thirdSd.2)) = ProbComp.eval (withoutSeeds count seedBits bound observationBits labelBits remainingBits source) := by simpa only [withoutSeeds, ProbComp.eval_bind, ProbComp.eval_map, ProbComp.eval_pure, @@ -382,7 +383,7 @@ theorem replace_indexed_labels {pair : SamplablePair} {gap : ℕ → ℝ} (hpair ((numerator n (choose n) : ℝ) / dyadicSize (densityBound n))) (adversary : ℕ → ℕ → List Bool → ProbComp Bool) (hadversary : IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => adversary input.1.1 input.1.2 input.2)) : + encBool (fun input => adversary (Prod.fst input.1) (Prod.snd input.1) input.2)) : let count := fun n => ExtractionSchedule.count n (saved.length n) (inverseSlack n) Negligible (fun n => Game.advantage (ProbComp.eval (withoutSeeds (count n) (saved.length n) (bound n) @@ -482,7 +483,7 @@ theorem SamplablePair.HasGap.extract_indexed_three {pair : SamplablePair} {gap : conditionalEntropy (pair.joint n))) (test : ℕ → ℕ → List Bool → ProbComp Bool) (htest : IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => test input.1.1 input.1.2 input.2)) : + encBool (fun input => test (Prod.fst input.1) (Prod.snd input.1) input.2)) : let count := fun n => ExtractionSchedule.count n (saved.length n) (inverseSlack n) Negligible (fun n => Game.advantage (ProbComp.eval (ThreeSource.extract (count n) (saved.length n) (bound n) diff --git a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Amplification.lean b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Amplification.lean index 77f1bee898..32161545be 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Amplification.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Amplification.lean @@ -58,9 +58,10 @@ theorem isPolyTime_amplifiedGenerate {pair : SamplablePair} (saved : pair.SeedRe (hdensity : ComputableInPolyTime densityBound encUnary encUnary) (hcommon : ComputableInPolyTime common encUnary encUnary) : ComputableInPolyTime - (fun input => amplifiedGenerate input.1.1 (saved.length input.1.1) - (observationBound input.1.1) (densityBound input.1.1) (common input.1.1) input.1.2 - (saved.evaluate input.1.1) input.2) + (fun input => amplifiedGenerate (Prod.fst input.1) (saved.length (Prod.fst input.1)) + (observationBound (Prod.fst input.1)) (densityBound (Prod.fst input.1)) + (common (Prod.fst input.1)) (Prod.snd input.1) + (saved.evaluate (Prod.fst input.1)) input.2) (encPair (encPair encUnary encUnary) encBits) encBits := by have hlength := saved.length_isPolyTime have hsize := isPolyTime_size hlength hdensity @@ -104,7 +105,7 @@ theorem exists_secure_amplified_choice {pair : SamplablePair} {gap : ℕ → ℝ (∀ᶠ n in atTop, choose n < size (saved.length n) (densityBound n)) ∧ ∀ test : ℕ → ℕ → List Bool → ProbComp Bool, IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => test input.1.1 input.1.2 input.2) → + encBool (fun input => test (Prod.fst input.1) (Prod.snd input.1) input.2) → Negligible (fun n => Game.advantage (((uniformList (common n)).map (amplifiedGenerate n (saved.length n) (observationBound n) (densityBound n) (common n) (choose n) (saved.evaluate n))).bind diff --git a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Candidates.lean b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Candidates.lean index f4555e5b49..b082e0e162 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Candidates.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Candidates.lean @@ -127,9 +127,10 @@ theorem isPolyTime_generate_of_realization {pair : SamplablePair} (saved : pair. {observationBound densityBound : ℕ → ℕ} (hobservation : ComputableInPolyTime observationBound encUnary encUnary) (hdensity : ComputableInPolyTime densityBound encUnary encUnary) : - ComputableInPolyTime (fun input => generate input.1.1 (saved.length input.1.1) - (observationBound input.1.1) (densityBound input.1.1) input.1.2 - (saved.evaluate input.1.1) input.2) + ComputableInPolyTime (fun input => generate (Prod.fst input.1) + (saved.length (Prod.fst input.1)) + (observationBound (Prod.fst input.1)) (densityBound (Prod.fst input.1)) (Prod.snd input.1) + (saved.evaluate (Prod.fst input.1)) input.2) (encPair (encPair encUnary encUnary) encBits) encBits := by have hlength := saved.length_isPolyTime have hevaluate := saved.efficient @@ -185,7 +186,7 @@ theorem exists_secure_choice {pair : SamplablePair} {gap : ℕ → ℝ} (∀ᶠ n in atTop, choose n < size (saved.length n) (densityBound n)) ∧ ∀ test : ℕ → ℕ → List Bool → ProbComp Bool, IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => test input.1.1 input.1.2 input.2) → + encBool (fun input => test (Prod.fst input.1) (Prod.snd input.1) input.2) → Negligible (fun n => Game.advantage (((uniformList (seedLength n (saved.length n) (observationBound n) (densityBound n) (choose n))).map (generate n (saved.length n) (observationBound n) (densityBound n) diff --git a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Padding.lean b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Padding.lean index 6be4636a75..a197bcb7ed 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Padding.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Padding.lean @@ -101,9 +101,11 @@ theorem isPolyTime_paddedGenerate {pair : SamplablePair} (saved : pair.SeedReali (hobservation : ComputableInPolyTime observationBound encUnary encUnary) (hdensity : ComputableInPolyTime densityBound encUnary encUnary) (hcommon : ComputableInPolyTime common encUnary encUnary) : - ComputableInPolyTime (fun input => paddedGenerate input.1.1 (saved.length input.1.1) - (observationBound input.1.1) (densityBound input.1.1) (common input.1.1) input.1.2 - (saved.evaluate input.1.1) input.2) + ComputableInPolyTime (fun input => paddedGenerate (Prod.fst input.1) + (saved.length (Prod.fst input.1)) + (observationBound (Prod.fst input.1)) (densityBound (Prod.fst input.1)) + (common (Prod.fst input.1)) (Prod.snd input.1) + (saved.evaluate (Prod.fst input.1)) input.2) (encPair (encPair encUnary encUnary) encBits) encBits := by have hobservation := hobservation.tidy have hdensity := hdensity.tidy @@ -143,7 +145,7 @@ theorem exists_secure_padded_choice {pair : SamplablePair} {gap : ℕ → ℝ} (∀ᶠ n in atTop, choose n < size (saved.length n) (densityBound n)) ∧ ∀ test : ℕ → ℕ → List Bool → ProbComp Bool, IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => test input.1.1 input.1.2 input.2) → + encBool (fun input => test (Prod.fst input.1) (Prod.snd input.1) input.2) → Negligible (fun n => Game.advantage (((uniformList (common n)).map (paddedGenerate n (saved.length n) (observationBound n) (densityBound n) (common n) (choose n) (saved.evaluate n))).bind diff --git a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Seeded.lean b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Seeded.lean index 0567d110ce..f5a165a3fe 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Seeded.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Seeded.lean @@ -53,8 +53,8 @@ open Probability BitString Turing.MultiTapeTM def hashSamples (count seedBits bound observationBits labelBits remainingBits : ℕ) (samples : List ((List Bool × Bool) × List Bool)) (firstKey middleKey lastKey : List Bool) : List Bool := - let observations := ((samples.map (fun sample => sample.1.1)).map (padWord bound)).flatten - let labels := listRow count 0 (samples.map (fun sample => sample.1.2)) + let observations := ((samples.map (fun sample => Prod.fst sample.1)).map (padWord bound)).flatten + let labels := listRow count 0 (samples.map (fun sample => Prod.snd sample.1)) let seeds := listRow (count * seedBits) 0 (samples.map Prod.snd).flatten ((firstKey ++ LinearHash.wordHash observationBits firstKey observations) ++ (middleKey ++ LinearHash.wordHash labelBits middleKey labels)) ++ @@ -202,12 +202,13 @@ theorem generate_distribution (count seedBits bound observationBits labelBits re probabilistic hashing calls exactly. Only the observation padding requires a size bound. -/ theorem eval_hashSamples (count seedBits bound observationBits labelBits remainingBits : ℕ) (samples : List ((List Bool × Bool) × List Bool)) (hcount : samples.length = count) - (hbound : ∀ sample ∈ samples, sample.1.1.length ≤ bound) : + (hbound : ∀ sample ∈ samples, (Prod.fst sample.1).length ≤ bound) : ProbComp.eval (do let third ← extractWordSeeds count seedBits remainingBits samples let middle ← extractWordLabels count labelBits third.1 let front ← finish bound observationBits middle - return front ++ (third.2.1 ++ third.2.2)) = + let thirdSd := third.2 + return front ++ (thirdSd.1 ++ thirdSd.2)) = (do let lastKey ← uniformList (remainingBits * (count * seedBits)) let middleKey ← uniformList (labelBits * count) diff --git a/Complexity/Crypto/Computational/Pseudoentropy/WordExtraction.lean b/Complexity/Crypto/Computational/Pseudoentropy/WordExtraction.lean index 9eef8c06e2..64438e12d2 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/WordExtraction.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/WordExtraction.lean @@ -81,7 +81,9 @@ theorem eval_extractWordLabels (count outputBits : ℕ) (samples : List (List Bo (ProbComp.eval (extractLabels (ProbComp.uniform (BitString (outputBits * count))) (fun seed bits => LinearHash.hash (blocksEquiv (m := outputBits) (k := count) seed) (ofList count bits)) - samples)).map (fun result => (result.1, List.ofFn result.2.1, List.ofFn result.2.2)) := by + samples)).map (fun result => + let sd := result.2 + (result.1, List.ofFn sd.1, List.ofFn sd.2)) := by exact eval_extractMatrixLabels count outputBits id samples /-- The ideal word program agrees with the finite ideal distribution and retains the full seed. -/ @@ -89,7 +91,9 @@ theorem eval_extractWordLabelsIdeal (source : ProbComp (List Bool)) (count outpu ProbComp.eval (extractWordLabelsIdeal source count outputBits) = (extractLabelsIdeal (Output := BitString outputBits) source count (ProbComp.uniform (BitString (outputBits * count)))).map - (fun result => (result.1, List.ofFn result.2.1, List.ofFn result.2.2)) := by + (fun result => + let sd := result.2 + (result.1, List.ofFn sd.1, List.ofFn sd.2)) := by exact eval_extractMatrixLabelsIdeal source count count outputBits /-- An ordinary word test after extraction gives the finite test required by the security @@ -109,7 +113,8 @@ theorem isPPTOn_extractedWordTest {α : Type} {input : α ↪ List Bool} {count (fun seed bits => LinearHash.hash (blocksEquiv (m := outputBits input.1) (k := count input.1) seed) (ofList (count input.1) bits)) input.2 - test input.1 (result.1, List.ofFn result.2.1, List.ofFn result.2.2)) := by + let sd := result.2 + test input.1 (result.1, List.ofFn sd.1, List.ofFn sd.2)) := by have hword : IsPPTOn (encPair input (encList (encPair encBits encBool))) encBool (fun input => extractWordLabels (count input.1) (outputBits input.1) input.2 >>= @@ -145,7 +150,7 @@ theorem SamplablePair.HasGap.extract_indexed_word_labels {pair : SamplablePair} (test : ℕ → ℕ → List (List Bool) × List Bool × List Bool → ProbComp Bool) (htest : IsPPTOn (encPair (encPair encUnary encUnary) (encPair (encList encBits) (encPair encBits encBits))) - encBool (fun input => test input.1.1 input.1.2 input.2)) : + encBool (fun input => test (Prod.fst input.1) (Prod.snd input.1) input.2)) : let count := fun n => ExtractionSchedule.count n (realization.length n) (inverseSlack n) Negligible (fun n => Game.advantage (ProbComp.eval (do diff --git a/Complexity/Crypto/Computational/PseudorandomFunction/Coins.lean b/Complexity/Crypto/Computational/PseudorandomFunction/Coins.lean index 4f9b3823e5..0f1409bae8 100644 --- a/Complexity/Crypto/Computational/PseudorandomFunction/Coins.lean +++ b/Complexity/Crypto/Computational/PseudorandomFunction/Coins.lean @@ -117,7 +117,8 @@ theorem length_prfCoins {family : List Bool → List Bool → List Bool} theorem computableInPolyTime_prfCoins {family : List Bool → List Bool → List Bool} (hF : ComputableInPolyTime (fun p : List Bool × List Bool => family p.1 p.2) (encPair encBits encBits) encBits) : - ComputableInPolyTime (fun p : List Bool × List Bool × ℕ => prfCoins family p.1 p.2.1 p.2.2) + ComputableInPolyTime + (fun p : List Bool × List Bool × ℕ => prfCoins family p.1 (Prod.fst p.2) (Prod.snd p.2)) (encPair encBits (encPair encBits encUnary)) encBits := by unfold prfCoins padRequest polytime diff --git a/Complexity/Crypto/Computational/Stretch.lean b/Complexity/Crypto/Computational/Stretch.lean index c1065b21cb..4eca932256 100644 --- a/Complexity/Crypto/Computational/Stretch.lean +++ b/Complexity/Crypto/Computational/Stretch.lean @@ -352,13 +352,13 @@ The choice is supplied only in the proof; each reduction receives its index as o theorem indexed_indistinguishable {generator : ℕ → ℕ → List Bool → List Bool} {seedBits count choose : ℕ → ℕ} (hgenerator : ComputableInPolyTime - (fun input => generator input.1.1 input.1.2 input.2) + (fun input => generator (Prod.fst input.1) (Prod.snd input.1) input.2) (encPair (encPair encUnary encUnary) encBits) encBits) (hseedBits : ComputableInPolyTime seedBits encUnary encUnary) (hcount : ComputableInPolyTime count encUnary encUnary) (hsecure : ∀ adversary : ℕ → ℕ → List Bool → ProbComp Bool, IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => adversary input.1.1 input.1.2 input.2) → + encBool (fun input => adversary (Prod.fst input.1) (Prod.snd input.1) input.2) → Negligible (fun n => Game.advantage (((uniformList (seedBits n)).map (generator n (choose n))).bind (fun word => ProbComp.eval (adversary n (choose n) word))) @@ -366,7 +366,7 @@ theorem indexed_indistinguishable {generator : ℕ → ℕ → List Bool → Lis (fun word => ProbComp.eval (adversary n (choose n) word))))) : ∀ adversary : ℕ → ℕ → List Bool → ProbComp Bool, IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => adversary input.1.1 input.1.2 input.2) → + encBool (fun input => adversary (Prod.fst input.1) (Prod.snd input.1) input.2) → Negligible (fun n => Game.advantage (((uniformList (seedBits n)).map (iterate (generator n (choose n)) (seedBits n) (count n))).bind diff --git a/Complexity/Crypto/Computational/Stretch/Quantitative.lean b/Complexity/Crypto/Computational/Stretch/Quantitative.lean index 6a3685017a..ab03a0ef43 100644 --- a/Complexity/Crypto/Computational/Stretch/Quantitative.lean +++ b/Complexity/Crypto/Computational/Stretch/Quantitative.lean @@ -686,15 +686,17 @@ theorem computableInTimeAndSpace_forwardIterate_captured {α : Type} (hgen : ComputableInTimeAndSpace (fun p : α × List Bool => generator p.1 p.2) (encPair encParam encBits) encBits tGen sGen) {Q : (α × List Bool) × ℕ → ℕ} - (hspace : ∀ x i, i < x.2 → sGen (x.1.1, seedAt (generator x.1.1) x.1.2 i) ≤ Q x) : + (hspace : ∀ x i, i < x.2 → + sGen (Prod.fst x.1, seedAt (generator (Prod.fst x.1)) (Prod.snd x.1) i) ≤ Q x) : ∃ c, ComputableInTimeAndSpace - (fun x : (α × List Bool) × ℕ => forwardIterate (generator x.1.1) x.2 x.1.2) + (fun x : (α × List Bool) × ℕ => + forwardIterate (generator (Prod.fst x.1)) x.2 (Prod.snd x.1)) (encPair (encPair encParam encBits) encUnary) encBits - (fun x => c * ((encParam x.1.1).length + x.1.2.length + x.2 + + (fun x => c * ((encParam (Prod.fst x.1)).length + (Prod.snd x.1).length + x.2 + (∑ i ∈ Finset.range x.2, - (tGen (x.1.1, seedAt (generator x.1.1) x.1.2 i) + - (encParam x.1.1).length + x.1.2.length + 1)) + 1)) - (fun x => c * (Q x + (encParam x.1.1).length + x.1.2.length + 1)) := by + (tGen (Prod.fst x.1, seedAt (generator (Prod.fst x.1)) (Prod.snd x.1) i) + + (encParam (Prod.fst x.1)).length + (Prod.snd x.1).length + 1)) + 1)) + (fun x => c * (Q x + (encParam (Prod.fst x.1)).length + (Prod.snd x.1).length + 1)) := by -- Retain the captured streaming construction as a proof-local raw witness. have build {α : Type} {encParam : α ↪ List Bool} {generator : α → List Bool → List Bool} @@ -835,15 +837,18 @@ theorem computableInTimeAndSpace_iterate_captured {α : Type} (hgen : ComputableInTimeAndSpace (fun p : α × List Bool => generator p.1 p.2) (encPair encParam encBits) encBits tGen sGen) {Q : (α × List Bool) × ℕ → ℕ} - (hspace : ∀ x i, i < x.2 → sGen (x.1.1, seedAt (generator x.1.1) x.1.2 i) ≤ Q x) : + (hspace : ∀ x i, i < x.2 → + sGen (Prod.fst x.1, seedAt (generator (Prod.fst x.1)) (Prod.snd x.1) i) ≤ Q x) : ∃ c, ComputableInTimeAndSpace - (fun x : (α × List Bool) × ℕ => iterate (generator x.1.1) x.1.2.length x.2 x.1.2) + (fun x : (α × List Bool) × ℕ => + iterate (generator (Prod.fst x.1)) (Prod.snd x.1).length x.2 (Prod.snd x.1)) (encPair (encPair encParam encBits) encUnary) encBits - (fun x => c * ((encParam x.1.1).length + x.1.2.length + x.2 + + (fun x => c * ((encParam (Prod.fst x.1)).length + (Prod.snd x.1).length + x.2 + (∑ i ∈ Finset.range x.2, - (tGen (x.1.1, seedAt (generator x.1.1) x.1.2 i) + - (encParam x.1.1).length + x.1.2.length + 1)) + 1)) - (fun x => c * (Q x + (encParam x.1.1).length + x.1.2.length + x.2 + 1)) := by + (tGen (Prod.fst x.1, seedAt (generator (Prod.fst x.1)) (Prod.snd x.1) i) + + (encParam (Prod.fst x.1)).length + (Prod.snd x.1).length + 1)) + 1)) + (fun x => + c * (Q x + (encParam (Prod.fst x.1)).length + (Prod.snd x.1).length + x.2 + 1)) := by obtain ⟨c, hfwd⟩ := computableInTimeAndSpace_forwardIterate_captured hlen hgen hspace have hcharged := hfwd.mono (fun _ => le_rfl) (fun x => show c * (Q x + (encParam x.1.1).length + x.1.2.length + 1) ≤ diff --git a/Complexity/Crypto/Computational/UniformChoice.lean b/Complexity/Crypto/Computational/UniformChoice.lean index a99d5c3ed6..70b38fa6b5 100644 --- a/Complexity/Crypto/Computational/UniformChoice.lean +++ b/Complexity/Crypto/Computational/UniformChoice.lean @@ -77,7 +77,7 @@ theorem isPPTOn_test {α : Type} {input : α ↪ List Bool} (hreal : IsPPTOn input encBits real) (hideal : IsPPTOn input encBits ideal) (hadversary : IsPPTOn (encPair (encPair input encUnary) encBits) encBool - (fun a => adversary a.1.1 a.1.2 a.2)) + (fun a => adversary (Prod.fst a.1) (Prod.snd a.1) a.2)) (hchallenge : ComputableInPolyTime challenge input encBits) : IsPPTOn input encBool (fun a => test (bound a) (real a) (ideal a) (adversary a) (challenge a)) := by @@ -149,7 +149,7 @@ theorem ComputationallyIndistinguishable.uniform_bound (hbound : ComputableInPolyTime bound encUnary encUnary) (adversary : ℕ → ℕ → List Bool → ProbComp Bool) (hadversary : IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun a => adversary a.1.1 a.1.2 a.2)) : + encBool (fun a => adversary (Prod.fst a.1) (Prod.snd a.1) a.2)) : ∃ ε : ℕ → ℝ≥0, Negligible ε ∧ ∀ n index, index ≤ bound n → Game.advantage (ProbComp.eval (real n >>= adversary n index)) (ProbComp.eval (ideal n >>= adversary n index)) ≤ ε n := by diff --git a/Complexity/Crypto/Primitives/PRG/NisanWigderson/Sampling.lean b/Complexity/Crypto/Primitives/PRG/NisanWigderson/Sampling.lean index b6e9ef29b5..cc2a4579c1 100644 --- a/Complexity/Crypto/Primitives/PRG/NisanWigderson/Sampling.lean +++ b/Complexity/Crypto/Primitives/PRG/NisanWigderson/Sampling.lean @@ -128,7 +128,10 @@ deriving DecidableEq, Fintype /-- A trial is its four random choices. -/ def Trial.equivProd : Trial ℓ m ≃ Fin m × (Fin ℓ → Bool) × Bool × (Fin m → Bool) where toFun t := (t.pos, t.seed, t.bit, t.pad) - invFun p := ⟨p.1, p.2.1, p.2.2.1, p.2.2.2⟩ + invFun p := + let rest := p.2 + let bp := rest.2 + ⟨p.1, rest.1, bp.1, bp.2⟩ instance [NeZero m] : Nonempty (Trial ℓ m) := ⟨⟨0, fun _ => false, false, fun _ => false⟩⟩ From 48dc42fc2f08189a1d2bf439878cbf825513b628 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 2 Nov 2026 15:31:54 +0000 Subject: [PATCH 2/3] refactor(Crypto/Pseudoentropy): address review feedback on projection chains (#1764) --- .../Computational/DiffieHellman/MultiDDH.lean | 21 +++--- .../DiscreteLog/SchnorrGroup.lean | 71 ++++++++++++------- .../Crypto/Computational/GeneratorXor.lean | 13 ++-- .../Crypto/Computational/NaorReingold.lean | 11 ++- .../Computational/NaorReingold/Security.lean | 14 ++-- .../Crypto/Computational/OneWay/MCSP.lean | 3 +- .../Crypto/Computational/OneWay/NP.lean | 34 +++++---- .../Pseudoentropy/DenseMask.lean | 2 +- .../Computational/Pseudoentropy/HashPair.lean | 10 ++- .../Pseudoentropy/LabelExtraction.lean | 10 ++- .../Pseudoentropy/MatrixExtraction.lean | 24 ++++--- .../Pseudoentropy/RepeatedExtraction.lean | 4 +- .../Pseudoentropy/Selection.lean | 4 +- .../Pseudoentropy/ThreeSource.lean | 21 +++--- .../ThreeSource/Amplification.lean | 9 ++- .../Pseudoentropy/ThreeSource/Candidates.lean | 9 ++- .../Pseudoentropy/ThreeSource/Padding.lean | 10 ++- .../Pseudoentropy/ThreeSource/Seeded.lean | 9 ++- .../Pseudoentropy/WordExtraction.lean | 12 ++-- .../PseudorandomFunction/Coins.lean | 3 +- Complexity/Crypto/Computational/Stretch.lean | 6 +- .../Computational/Stretch/Quantitative.lean | 29 ++++---- .../Crypto/Computational/UniformChoice.lean | 4 +- .../PRG/NisanWigderson/Sampling.lean | 5 +- 24 files changed, 173 insertions(+), 165 deletions(-) diff --git a/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean b/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean index 5f594098a0..fde1c9ebee 100644 --- a/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean +++ b/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean @@ -43,6 +43,15 @@ variable (F : PrimeOrderGroupFamily) /-! ### Fixed-$u$ DDH random self-reduction and Multi-DDH (I) (Exercises 10.8 & 10.11) -/ +/-- The first element `u` of a candidate Diffie–Hellman triple `(u, v, w)`. -/ +abbrev ddhU {G : Type*} (t : G × G × G) : G := t.1 + +/-- The second element `v` of a candidate Diffie–Hellman triple `(u, v, w)`. -/ +abbrev ddhV {G : Type*} (t : G × G × G) : G := t.2.1 + +/-- The third element `w` of a candidate Diffie–Hellman triple `(u, v, w)`. -/ +abbrev ddhW {G : Type*} (t : G × G × G) : G := t.2.2 + /-- Fixed-$u$ DDH rerandomization ([BonehShoup2023], Section 10.11, Exercise 10.8, p. 425): given `(u, v, w)` and exponents `σ, τ : ZMod (F.order d)`, output `(v*, w*) = (σ • g + τ • v, σ • u + τ • w)`. -/ @@ -76,10 +85,8 @@ theorem ddhFixedUWordRerandomize_encode (d : F.Desc) (u v w : F.Carrier d) (σ theorem computableInPolyTime_ddhFixedUWordRerandomize : ComputableInPolyTime (fun input : F.Desc × List Bool × List Bool × List Bool × ℕ × ℕ => - F.ddhFixedUWordRerandomize input.1 (Prod.fst input.2) (Prod.fst (Prod.snd input.2)) - (Prod.fst (Prod.snd (Prod.snd input.2))) - (Prod.fst (Prod.snd (Prod.snd (Prod.snd input.2)))) - (Prod.snd (Prod.snd (Prod.snd (Prod.snd input.2))))) + F.ddhFixedUWordRerandomize input.1 input.2.1 input.2.2.1 input.2.2.2.1 + input.2.2.2.2.1 input.2.2.2.2.2) (encPair F.encDesc (encPair encBits (encPair encBits (encPair encBits (encPair encNat encNat))))) (encPair encBits encBits) := by @@ -290,11 +297,9 @@ theorem advantage_multiDDH_le (d : F.Desc) (ι : Type*) [Fintype ι] [DecidableE (F.multiDDHIdealTupleLaw d ι).bind (test (α • F.generator d))) ≤ Game.advantage ((F.ddhRealTupleLaw d).bind fun t => - let vw := t.2 - (F.multiDDHRerandomizeLaw d ι t.1 vw.1 vw.2).bind (test t.1)) + (F.multiDDHRerandomizeLaw d ι (ddhU t) (ddhV t) (ddhW t)).bind (test (ddhU t))) ((F.ddhIdealTupleLaw d).bind fun t => - let vw := t.2 - (F.multiDDHRerandomizeLaw d ι t.1 vw.1 vw.2).bind (test t.1)) + + (F.multiDDHRerandomizeLaw d ι (ddhU t) (ddhV t) (ddhW t)).bind (test (ddhU t))) + (F.order d : ℝ≥0)⁻¹ := by have hreal : ((F.ddhRealTupleLaw d).bind fun t => diff --git a/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean b/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean index 3429292f14..5819540bf0 100644 --- a/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean +++ b/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean @@ -51,57 +51,75 @@ open Turing.MultiTapeTM namespace SchnorrGroup +/-- The prime modulus `p` of a raw Schnorr-group description `(p, q, g)`. -/ +abbrev rawModulus (d : ℕ × ℕ × ℕ) : ℕ := d.1 + +/-- The prime subgroup order `q` of a raw Schnorr-group description `(p, q, g)`. -/ +abbrev rawOrder (d : ℕ × ℕ × ℕ) : ℕ := d.2.1 + +/-- The subgroup generator residue `g` of a raw Schnorr-group description `(p, q, g)`. -/ +abbrev rawGenerator (d : ℕ × ℕ × ℕ) : ℕ := d.2.2 + /-- A valid description `(p, q, g)` of a Schnorr group: `p` and `q` are prime, and the residue `g` satisfies `1 < g < p` and `g ^ q ≡ 1 (mod p)`. -/ structure Valid (d : ℕ × ℕ × ℕ) : Prop where /-- The modulus is prime. -/ - prime_modulus : d.1.Prime + prime_modulus : (rawModulus d).Prime /-- The group order is prime. -/ - prime_order : (Prod.fst d.2).Prime + prime_order : (rawOrder d).Prime /-- The generator is not `0` or `1`. -/ - one_lt_generator : 1 < Prod.snd d.2 + one_lt_generator : 1 < rawGenerator d /-- The generator is a reduced residue. -/ - generator_lt : Prod.snd d.2 < d.1 + generator_lt : rawGenerator d < rawModulus d /-- The generator has order dividing `q`. -/ - generator_pow : Prod.snd d.2 ^ Prod.fst d.2 % d.1 = 1 + generator_pow : rawGenerator d ^ rawOrder d % rawModulus d = 1 /-- Valid Schnorr-group descriptions. -/ abbrev Desc : Type := {d : ℕ × ℕ × ℕ // Valid d} +/-- The prime modulus `p` of a valid Schnorr-group description `(p, q, g)`. -/ +abbrev Desc.modulus (d : Desc) : ℕ := rawModulus d.val + +/-- The prime subgroup order `q` of a valid Schnorr-group description `(p, q, g)`. -/ +abbrev Desc.order (d : Desc) : ℕ := rawOrder d.val + +/-- The subgroup generator residue `g` of a valid Schnorr-group description `(p, q, g)`. -/ +abbrev Desc.generator (d : Desc) : ℕ := rawGenerator d.val + /-- The generator as a unit modulo `p`. -/ -def generatorUnit (d : Desc) : (ZMod d.val.1)ˣ := - ZMod.unitOfCoprime (Prod.snd d.val.2) ((Nat.coprime_comm.mp +def generatorUnit (d : Desc) : (ZMod d.modulus)ˣ := + ZMod.unitOfCoprime d.generator ((Nat.coprime_comm.mp ((d.2.prime_modulus.coprime_iff_not_dvd).mpr (Nat.not_dvd_of_pos_of_lt (by have := d.2.one_lt_generator; lia) d.2.generator_lt)))) /-- The Schnorr group of a description, written additively. -/ abbrev Carrier (d : Desc) : Type := Additive (Subgroup.zpowers (generatorUnit d)) -instance (d : Desc) : Fact (Prod.fst d.val.2).Prime := ⟨d.2.prime_order⟩ +instance (d : Desc) : Fact d.order.Prime := ⟨d.2.prime_order⟩ /-- The generator has order dividing `q`. -/ -theorem generatorUnit_pow_order (d : Desc) : generatorUnit d ^ Prod.fst d.val.2 = 1 := by +theorem generatorUnit_pow_order (d : Desc) : generatorUnit d ^ d.order = 1 := by ext rw [Units.val_pow_eq_pow_val, generatorUnit, ZMod.coe_unitOfCoprime, Units.val_one, ← Nat.cast_pow, ← ZMod.natCast_mod, d.2.generator_pow, Nat.cast_one] /-- Every element of the Schnorr group has order dividing `q`. -/ theorem pow_order (d : Desc) (x : Subgroup.zpowers (generatorUnit d)) : - x ^ Prod.fst d.val.2 = 1 := by + x ^ d.order = 1 := by obtain ⟨k, hk⟩ := Subgroup.mem_zpowers_iff.mp x.2 ext rw [Subgroup.coe_pow, ← hk, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, generatorUnit_pow_order, one_zpow, Subgroup.coe_one] -instance (d : Desc) : Module (ZMod (Prod.fst d.val.2)) (Carrier d) := +instance (d : Desc) : Module (ZMod d.order) (Carrier d) := AddCommMonoid.zmodModule fun x => Additive.toMul.injective (by rw [toMul_nsmul, pow_order, toMul_zero]) -instance (d : Desc) : NeZero d.val.1 := ⟨d.2.prime_modulus.ne_zero⟩ +instance (d : Desc) : NeZero d.modulus := ⟨d.2.prime_modulus.ne_zero⟩ /-- The generator is not the identity. -/ theorem generatorUnit_ne_one (d : Desc) : generatorUnit d ≠ 1 := fun h => by - have hval := congrArg (fun u : (ZMod d.val.1)ˣ => (u : ZMod d.val.1).val) h + have hval := congrArg (fun u : (ZMod d.modulus)ˣ => (u : ZMod d.modulus).val) h simp only [generatorUnit, ZMod.coe_unitOfCoprime, ZMod.val_natCast, Nat.mod_eq_of_lt d.2.generator_lt, Units.val_one, ZMod.val_one_eq_one_mod, Nat.mod_eq_of_lt d.2.prime_modulus.one_lt] at hval @@ -112,19 +130,19 @@ def generator (d : Desc) : Carrier d := Additive.ofMul ⟨generatorUnit d, Subgroup.mem_zpowers _⟩ /-- The Schnorr group has `q` elements. -/ -theorem card_carrier (d : Desc) : Nat.card (Carrier d) = Prod.fst d.val.2 := by +theorem card_carrier (d : Desc) : Nat.card (Carrier d) = d.order := by change Nat.card (Subgroup.zpowers (generatorUnit d)) = d.1.2.1 rw [Nat.card_zpowers, orderOf_eq_prime (generatorUnit_pow_order d) (generatorUnit_ne_one d)] /-- The generator is not the identity of the Schnorr group. -/ theorem generator_ne_zero (d : Desc) : generator d ≠ 0 := fun h => generatorUnit_ne_one d (congrArg (fun x : Carrier d => ((Additive.toMul x : - Subgroup.zpowers (generatorUnit d)) : (ZMod d.val.1)ˣ)) h) + Subgroup.zpowers (generatorUnit d)) : (ZMod d.modulus)ˣ)) h) /-- Elements are encoded by the binary digits of their residues modulo `p`. -/ def encode (d : Desc) (x : Carrier d) : List Bool := - ((((Additive.toMul x : Subgroup.zpowers (generatorUnit d)) : (ZMod d.val.1)ˣ) : - ZMod d.val.1).val).bits + ((((Additive.toMul x : Subgroup.zpowers (generatorUnit d)) : (ZMod d.modulus)ˣ) : + ZMod d.modulus).val).bits /-- Distinct elements have distinct encodings. -/ theorem encode_injective (d : Desc) : Function.Injective (encode d) := fun _ _ h => @@ -136,7 +154,7 @@ private theorem ofBits_bits (n : ℕ) : ofBits n.bits = n := Nat.foldr_bit_bits /-- Multiplication modulo `p` of encoded residues. -/ def add (input : Desc × List Bool × List Bool) : List Bool := - (ofBits (Prod.fst input.2) * ofBits (Prod.snd input.2) % input.1.val.1).bits + (ofBits input.2.1 * ofBits input.2.2 % input.1.modulus).bits /-- `add` multiplies encoded group elements. -/ theorem add_encode (d : Desc) (x y : Carrier d) : @@ -145,17 +163,17 @@ theorem add_encode (d : Desc) (x y : Carrier d) : /-- Exponentiation modulo `p` of an encoded residue. -/ def smul (input : Desc × ℕ × List Bool) : List Bool := - (ofBits (Prod.snd input.2) ^ Prod.fst input.2 % input.1.val.1).bits + (ofBits input.2.2 ^ input.2.1 % input.1.modulus).bits /-- `smul` raises encoded group elements to natural powers. -/ theorem smul_encode (d : Desc) (a : ℕ) (x : Carrier d) : - smul (d, a, encode d x) = encode d ((a : ZMod (Prod.fst d.val.2)) • x) := by + smul (d, a, encode d x) = encode d ((a : ZMod d.order) • x) := by rw [Nat.cast_smul_eq_nsmul] simp only [smul, encode, ofBits_bits, toMul_nsmul, Subgroup.coe_pow, Units.val_pow_eq_pow_val] rw [← ZMod.val_natCast, Nat.cast_pow, ZMod.natCast_zmod_val] /-- The encoded generator is the binary digits of `g`. -/ -theorem encode_generator (d : Desc) : encode d (generator d) = (Prod.snd d.val.2).bits := by +theorem encode_generator (d : Desc) : encode d (generator d) = d.generator.bits := by change (((generatorUnit d : (ZMod d.1.1)ˣ) : ZMod d.1.1).val).bits = _ rw [generatorUnit, ZMod.coe_unitOfCoprime, ZMod.val_natCast, Nat.mod_eq_of_lt d.2.generator_lt] @@ -172,22 +190,23 @@ private theorem computableInPolyTime_val : /-- The group order is computable in polynomial time from the description. -/ theorem computableInPolyTime_order : - ComputableInPolyTime (fun d : Desc => Prod.fst d.val.2) encDesc encNat := by + ComputableInPolyTime Desc.order encDesc encNat := by have := computableInPolyTime_val + unfold Desc.order rawOrder fun_prop /-- The encoded generator is computable in polynomial time from the description. -/ theorem computableInPolyTime_generator : ComputableInPolyTime (fun d => encode d (generator d)) encDesc encBits := by have := computableInPolyTime_val - simp only [encode_generator] + simp only [encode_generator, Desc.generator, rawGenerator] fun_prop /-- Multiplication modulo `p` is computable in polynomial time. -/ theorem computableInPolyTime_add : ComputableInPolyTime add (encPair encDesc (encPair encBits encBits)) encBits := by have := computableInPolyTime_val - unfold add + unfold add Desc.modulus rawModulus fun_prop /-- Exponentiation modulo `p` is computable in polynomial time, by square-and-multiply. -/ @@ -199,7 +218,7 @@ theorem computableInPolyTime_smul : (encPair encDesc (encPair encNat encBits)) encNat := ComputableInPolyTime.binary_powMod (by fun_prop) (by fun_prop) (by fun_prop) fun input => input.1.2.prime_modulus.pos - unfold smul + unfold smul Desc.modulus rawModulus fun_prop end SchnorrGroup @@ -210,7 +229,7 @@ of prime order with efficient operations. -/ def schnorrGroups : PrimeOrderGroupFamily where Desc := SchnorrGroup.Desc encDesc := SchnorrGroup.encDesc - order d := Prod.fst d.val.2 + order := Desc.order prime_order d := d.2.prime_order Carrier := Carrier generator := generator diff --git a/Complexity/Crypto/Computational/GeneratorXor.lean b/Complexity/Crypto/Computational/GeneratorXor.lean index 1f6e257b72..3a94453e20 100644 --- a/Complexity/Crypto/Computational/GeneratorXor.lean +++ b/Complexity/Crypto/Computational/GeneratorXor.lean @@ -71,8 +71,8 @@ theorem isPolyTime_generate {α : Type} {input : α ↪ List Bool} (hcount : ComputableInPolyTime count input encUnary) (hseedBits : ComputableInPolyTime seedBits input encUnary) (houtputBits : ComputableInPolyTime outputBits input encUnary) - (hgenerator : ComputableInPolyTime (fun pair => generator (Prod.fst pair.1) (Prod.snd pair.1) - pair.2) (encPair (encPair input encUnary) encBits) encBits) + (hgenerator : ComputableInPolyTime (fun pair => generator pair.1.1 pair.1.2 pair.2) + (encPair (encPair input encUnary) encBits) encBits) (hseed : ComputableInPolyTime seed input encBits) : ComputableInPolyTime (fun a => generate (count a) (seedBits a) (outputBits a) (generator a) (seed a)) input encBits := by @@ -198,8 +198,8 @@ theorem isPPTOn_test {α : Type} {input : α ↪ List Bool} (hseedBits : ComputableInPolyTime seedBits input encUnary) (houtputBits : ComputableInPolyTime outputBits input encUnary) (hindex : ComputableInPolyTime index input encUnary) - (hgenerator : ComputableInPolyTime (fun pair => generator (Prod.fst pair.1) (Prod.snd pair.1) - pair.2) (encPair (encPair input encUnary) encBits) encBits) + (hgenerator : ComputableInPolyTime (fun pair => generator pair.1.1 pair.1.2 pair.2) + (encPair (encPair input encUnary) encBits) encBits) (hadversary : IsPPTOn (encPair input encBits) encBool (fun pair => adversary pair.1 pair.2)) (hchallenge : ComputableInPolyTime challenge input encBits) : @@ -252,13 +252,12 @@ theorem indistinguishable {generator : ℕ → ℕ → List Bool → List Bool} (hcount : ComputableInPolyTime count encUnary encUnary) (hseedBits : ComputableInPolyTime seedBits encUnary encUnary) (houtputBits : ComputableInPolyTime outputBits encUnary encUnary) - (hgenerator : ComputableInPolyTime - (fun input => generator (Prod.fst input.1) (Prod.snd input.1) input.2) + (hgenerator : ComputableInPolyTime (fun input => generator input.1.1 input.1.2 input.2) (encPair (encPair encUnary encUnary) encBits) encBits) (hchoose : ∀ᶠ n in Filter.atTop, choose n < count n) (hsecure : ∀ adversary : ℕ → ℕ → List Bool → ProbComp Bool, IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => adversary (Prod.fst input.1) (Prod.snd input.1) input.2) → + encBool (fun input => adversary input.1.1 input.1.2 input.2) → Negligible (fun n => Game.advantage (((uniformList (seedBits n)).map (generator n (choose n))).bind (fun word => ProbComp.eval (adversary n (choose n) word))) diff --git a/Complexity/Crypto/Computational/NaorReingold.lean b/Complexity/Crypto/Computational/NaorReingold.lean index c9f2f38e0e..c413028be3 100644 --- a/Complexity/Crypto/Computational/NaorReingold.lean +++ b/Complexity/Crypto/Computational/NaorReingold.lean @@ -321,8 +321,7 @@ theorem computableInPolyTime_naorReingoldProdNat : theorem computableInPolyTime_naorReingoldWordSuffix : ComputableInPolyTime (fun input : F.Desc × List Bool × List ℕ × List Bool => - F.naorReingoldWordSuffix input.1 (Prod.fst input.2) (Prod.fst (Prod.snd input.2)) - (Prod.snd (Prod.snd input.2))) + F.naorReingoldWordSuffix input.1 input.2.1 input.2.2.1 input.2.2.2) (encPair F.encDesc (encPair encBits (encPair (encList encNat) encBits))) encBits := by have hd : ComputableInPolyTime (fun input : F.Desc × List Bool × List ℕ × List Bool => input.1) @@ -359,8 +358,7 @@ theorem computableInPolyTime_naorReingoldWordSuffix : theorem computableInPolyTime_naorReingoldWordEval : ComputableInPolyTime (fun input : F.Desc × ℕ × List ℕ × List Bool => - F.naorReingoldWordEval input.1 (Prod.fst input.2) (Prod.fst (Prod.snd input.2)) - (Prod.snd (Prod.snd input.2))) + F.naorReingoldWordEval input.1 input.2.1 input.2.2.1 input.2.2.2) (encPair F.encDesc (encPair encNat (encPair (encList encNat) encBits))) encBits := by have hd : ComputableInPolyTime (fun input : F.Desc × ℕ × List ℕ × List Bool => input.1) @@ -604,9 +602,8 @@ rerandomize it into a `BitString k`-indexed family via `multiDDHRerandomizeLaw` noncomputable def naorReingoldLevelDDHDistinguisher (d : F.Desc) {n : ℕ} (k : ℕ) (hk : k < n) (adv : OracleComp (fun _ : BitString n => F.Carrier d) Bool) (t : F.Carrier d × F.Carrier d × F.Carrier d) : PMF Bool := - let vw := t.2 - (F.multiDDHRerandomizeLaw d (BitString k) t.1 vw.1 vw.2).bind - (F.naorReingoldLevelTest d k hk adv t.1) + (F.multiDDHRerandomizeLaw d (BitString k) (ddhU t) (ddhV t) (ddhW t)).bind + (F.naorReingoldLevelTest d k hk adv (ddhU t)) /-- Under `multiDDHRealTupleLaw`, `naorReingoldLevelTest` reproduces `naorReingoldHybridGame` at depth `k`. -/ diff --git a/Complexity/Crypto/Computational/NaorReingold/Security.lean b/Complexity/Crypto/Computational/NaorReingold/Security.lean index 5d8b3d50a5..3e764ebad3 100644 --- a/Complexity/Crypto/Computational/NaorReingold/Security.lean +++ b/Complexity/Crypto/Computational/NaorReingold/Security.lean @@ -468,14 +468,14 @@ noncomputable def naorReingoldToDDHDistinguisher (inLen : ℕ → ℕ) let k ← ProbComp.sampleDyadicIndex m if k < m then do let d := input.1 - let uvw := input.2 - let u := uvw.1 - let vw := uvw.2 + let u := ddhU input.2 + let v := ddhV input.2 + let w := ddhW input.2 let αs ← OracleComp.replicate (m - (k + 1)) (F.sampleNaorReingoldExp n d) Prod.fst <$> (OracleComp.interpret (ProbOracleComp.handler (fun r => StateT.lift (ProbComp.unifFin r)) (fun request => F.naorReingoldFrontierOracle n m k d - u vw.1 vw.2 αs request.2)) + u v w αs request.2)) (adversary n (F.encDesc d))).run [] else pure false @@ -2013,10 +2013,8 @@ theorem computableInPolyTime_naorReingoldHashedWordEval {bound : F.Desc → ℕ} (hbound : ComputableInPolyTime bound F.encDesc encUnary) : ComputableInPolyTime (fun input : ℕ × F.Desc × List Bool × ℕ × List ℕ × List Bool => - F.naorReingoldHashedWordEval input.1 bound (Prod.fst input.2) (Prod.fst (Prod.snd input.2)) - (Prod.fst (Prod.snd (Prod.snd input.2))) - (Prod.fst (Prod.snd (Prod.snd (Prod.snd input.2)))) - (Prod.snd (Prod.snd (Prod.snd (Prod.snd input.2))))) + F.naorReingoldHashedWordEval input.1 bound input.2.1 input.2.2.1 input.2.2.2.1 + input.2.2.2.2.1 input.2.2.2.2.2) (encPair encUnary (encPair F.encDesc (encPair encBits (encPair encNat (encPair (encList encNat) encBits))))) diff --git a/Complexity/Crypto/Computational/OneWay/MCSP.lean b/Complexity/Crypto/Computational/OneWay/MCSP.lean index e7a03ae725..2a3d0937e7 100644 --- a/Complexity/Crypto/Computational/OneWay/MCSP.lean +++ b/Complexity/Crypto/Computational/OneWay/MCSP.lean @@ -274,8 +274,7 @@ theorem computableInPolyTime_tableQueries (d : ℕ) : /-- The instance read from the answers is computed in polynomial time. -/ theorem computableInPolyTime_tableInstance (d : ℕ) : ComputableInPolyTime (fun pair : (ℕ × List Bool) × List Bool => - tableInstance (tableArity d (Prod.fst pair.1)) pair.2) - (encPair (encPair encUnary encBits) encBits) + tableInstance (tableArity d pair.1.1) pair.2) (encPair (encPair encUnary encBits) encBits) MCSP.encInstance := by refine .of_tidy ?_ have harity : ComputableTidilyInPolyTime (fun pair : (ℕ × List Bool) × List Bool => diff --git a/Complexity/Crypto/Computational/OneWay/NP.lean b/Complexity/Crypto/Computational/OneWay/NP.lean index 67954898cd..f74fb0d41f 100644 --- a/Complexity/Crypto/Computational/OneWay/NP.lean +++ b/Complexity/Crypto/Computational/OneWay/NP.lean @@ -80,7 +80,11 @@ open Complexity Probability Turing.MultiTapeTM ComputableTidilyInPolyTime /-- **The preimage-prefix problem** of `f`: the instances `(n, y, u)` such that some input `x` of length `n` that starts with `u` satisfies `f x = y`. -/ def preimagePrefix (f : List Bool → List Bool) : Set (ℕ × List Bool × List Bool) := - {p | let yu := p.2; ∃ x : List Bool, x.length = p.1 ∧ yu.2 <+: x ∧ f x = yu.1} + {(n, y, u) : ℕ × List Bool × List Bool | ∃ x : List Bool, x.length = n ∧ u <+: x ∧ f x = y} + +@[simp] theorem mem_preimagePrefix {f : List Bool → List Bool} {n : ℕ} {y u : List Bool} : + (n, y, u) ∈ preimagePrefix f ↔ ∃ x : List Bool, x.length = n ∧ u <+: x ∧ f x = y := by + simp [preimagePrefix] /-- The encoding of instances of the preimage-prefix problem: the length `n` in unary, then the image and the prefix. -/ @@ -95,12 +99,8 @@ variable {f : List Bool → List Bool} prefix. -/ def preimagePrefixVerifier (f : List Bool → List Bool) (p : (ℕ × List Bool × List Bool) × List Bool) : Bool := - let inst := p.1 - let n := inst.1 - let yu := inst.2 - let y := yu.1 - let u := yu.2 - decide (u.length ≤ n) && f (u ++ p.2.take (n - u.length)) == y + let ((n, y, u), rest) := p + decide (u.length ≤ n) && f (u ++ rest.take (n - u.length)) == y /-- The unary length is at most as long as the encoded instance. -/ private theorem le_length_encPreimagePrefix (p : ℕ × List Bool × List Bool) : @@ -112,14 +112,15 @@ private theorem le_length_encPreimagePrefix (p : ℕ × List Bool × List Bool) members. -/ theorem isVerifier_preimagePrefixVerifier (f : List Bool → List Bool) : IsVerifier encPreimagePrefix Polynomial.X (preimagePrefixVerifier f) (preimagePrefix f) := by - refine IsVerifier.of_padding (fun ⟨n, y, u⟩ w hw h => ?_) fun ⟨n, y, u⟩ ⟨x, hx, hux, hfx⟩ => ?_ + refine IsVerifier.of_padding (fun ⟨n, y, u⟩ w hw h => ?_) fun ⟨n, y, u⟩ hmem => ?_ · rw [Polynomial.eval_X] at hw have hn := le_length_encPreimagePrefix (n, y, u) simp only [preimagePrefixVerifier, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq] at h + rw [mem_preimagePrefix] refine ⟨u ++ w.take (n - u.length), ?_, List.prefix_append _ _, h.2⟩ simp only [List.length_append, List.length_take] at hw ⊢ omega - · obtain ⟨v, rfl⟩ := hux + · obtain ⟨x, hx, ⟨v, rfl⟩, hfx⟩ := mem_preimagePrefix.mp hmem have hn := le_length_encPreimagePrefix (n, y, u) simp only [List.length_append] at hx refine ⟨v, ?_, fun k => ?_⟩ @@ -136,7 +137,10 @@ theorem computableInPolyTime_preimagePrefixVerifier (hf : ComputableInPolyTime f encBits encBits) : ComputableInPolyTime (preimagePrefixVerifier f) (encPair encPreimagePrefix encBits) encBool := by - unfold preimagePrefixVerifier + change ComputableInPolyTime + (fun p : (ℕ × List Bool × List Bool) × List Bool => + decide (p.1.2.2.length ≤ p.1.1) && f (p.1.2.2 ++ p.2.take (p.1.1 - p.1.2.2.length)) == p.1.2.1) + (encPair encPreimagePrefix encBits) encBool fun_prop /-- **The preimage-prefix problem is in `NP`** for every function computable in polynomial @@ -176,15 +180,15 @@ theorem preimageSearchStep_mem {D : ℕ × List Bool × List Bool → Bool} (n, y, preimageSearchStep D (n, y) u) ∈ preimagePrefix f := by rw [preimageSearchStep] cases hb : D (n, y, u ++ [false]) - · obtain ⟨x, hx, ⟨v, rfl⟩, hfx⟩ := hu + · obtain ⟨x, hx, ⟨v, rfl⟩, hfx⟩ := mem_preimagePrefix.mp hu simp only [List.length_append] at hx obtain ⟨b, v, rfl⟩ : ∃ b v', v = b :: v' := List.exists_cons_of_length_pos (by omega) cases b · have hmem : (n, y, u ++ [false]) ∈ preimagePrefix f := - ⟨u ++ false :: v, by simpa using hx, ⟨v, by simp⟩, hfx⟩ + mem_preimagePrefix.mpr ⟨u ++ false :: v, by simpa using hx, ⟨v, by simp⟩, hfx⟩ rw [hD, hb] at hmem exact absurd hmem Bool.false_ne_true - · exact ⟨u ++ true :: v, by simpa using hx, ⟨v, by simp⟩, hfx⟩ + · exact mem_preimagePrefix.mpr ⟨u ++ true :: v, by simpa using hx, ⟨v, by simp⟩, hfx⟩ · exact (hD _).2 hb /-- **Search to decision.** With a decision procedure for the preimage-prefix problem, the search @@ -196,12 +200,12 @@ theorem apply_preimageSearch {D : ℕ × List Bool × List Bool → Bool} (x.length, f x, (preimageSearchStep D (x.length, f x))^[i] []) ∈ preimagePrefix f := by intro i hi induction i with - | zero => exact ⟨x, rfl, List.nil_prefix, rfl⟩ + | zero => exact mem_preimagePrefix.mpr ⟨x, rfl, List.nil_prefix, rfl⟩ | succ i ih => rw [Function.iterate_succ_apply'] exact preimageSearchStep_mem hD (ih (by omega)) (by rw [length_iterate_preimageSearchStep]; omega) - obtain ⟨x', hx', hpre, hfx'⟩ := hmem x.length le_rfl + obtain ⟨x', hx', hpre, hfx'⟩ := mem_preimagePrefix.mp (hmem x.length le_rfl) have heq := hpre.eq_of_length (by rw [length_iterate_preimageSearchStep]; exact hx'.symm) dsimp only at heq hfx' change f ((preimageSearchStep D (x.length, f x))^[x.length] []) = f x diff --git a/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean b/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean index f4aa76dce9..9ee9d0cdb5 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean @@ -63,7 +63,7 @@ theorem HasGap.eventually_exists_indexed_mask {pair : SamplablePair} {gap : ℕ (hpair : pair.HasGap gap) (test : ℕ → ℕ → List (List Bool × Bool) → ProbComp Bool) (htest : IsPPTOn (encPair (encPair encUnary encUnary) (encList (encPair encBits encBool))) encBool - (fun input => test (Prod.fst input.1) (Prod.snd input.1) input.2)) + (fun input => test input.1.1 input.1.2 input.2)) {candidates count densityBound inverseGap : ℕ → ℕ} {numerator : ℕ → ℕ → ℕ} (hcandidates : ComputableInPolyTime candidates encUnary encUnary) (hcount : ComputableInPolyTime count encUnary encUnary) diff --git a/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean b/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean index 460dcd0a06..4c3bef5021 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean @@ -154,12 +154,10 @@ theorem computableInPolyTime_wordObservation {α : Type} {encode : α ↪ List B /-- Encode a finite public observation using the chosen image representation. -/ def encodeObservation {n count : ℕ} {Image : Type*} (encodeImage : Image → List Bool) (observation : Observation n count Image) : List Bool := - let rest := observation.2 - let mq := rest.1 - let idig := rest.2 - wordObservation (encodeImage idig.1) observation.1.val - (List.ofFn mq.1) (List.ofFn idig.2) - (List.ofFn mq.2) + let (pos, (matrix, query), image, digest) := observation + wordObservation (encodeImage image) pos.val + (List.ofFn matrix) (List.ofFn digest) + (List.ofFn query) /-- Encoding loses none of the public information, even though the digest's width varies. -/ theorem encodeObservation_injective {n count : ℕ} {Image : Type*} diff --git a/Complexity/Crypto/Computational/Pseudoentropy/LabelExtraction.lean b/Complexity/Crypto/Computational/Pseudoentropy/LabelExtraction.lean index d7cfc9c845..e024fbe9ac 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/LabelExtraction.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/LabelExtraction.lean @@ -63,9 +63,8 @@ theorem HasGap.indexed_extracted_advantage_negligible {pair : SamplablePair} {ga (test : ∀ n i, List (List Bool) × Seed n i × Output n i → ProbComp Bool) (htest : IsPPTOn (encPair (encPair encUnary encUnary) (encList (encPair encBits encBool))) encBool - (fun input => extractLabels (seed (Prod.fst input.1) (Prod.snd input.1)) - (hash (Prod.fst input.1) (Prod.snd input.1)) - input.2 >>= test (Prod.fst input.1) (Prod.snd input.1))) + (fun input => extractLabels (seed input.1.1 input.1.2) (hash input.1.1 input.1.2) + input.2 >>= test input.1.1 input.1.2)) {candidates count densityBound : ℕ → ℕ} {numerator : ℕ → ℕ → ℕ} {slack : ℕ → ℝ} (hcandidates : ComputableInPolyTime candidates encUnary encUnary) (hcount : ComputableInPolyTime count encUnary encUnary) @@ -179,9 +178,8 @@ theorem HasGap.extract_indexed_labels {pair : SamplablePair} {gap : ℕ → ℝ} (test : ∀ n i, List (List Bool) × Seed n i × BitString (outputBits n i) → ProbComp Bool) (htest : IsPPTOn (encPair (encPair encUnary encUnary) (encList (encPair encBits encBool))) encBool - (fun input => extractLabels (seed (Prod.fst input.1) (Prod.snd input.1)) - (hash (Prod.fst input.1) (Prod.snd input.1)) - input.2 >>= test (Prod.fst input.1) (Prod.snd input.1))) + (fun input => extractLabels (seed input.1.1 input.1.2) (hash input.1.1 input.1.2) + input.2 >>= test input.1.1 input.1.2)) (hcandidates : ComputableInPolyTime candidates encUnary encUnary) (hslack : ComputableInPolyTime inverseSlack encUnary encUnary) {numerator : ℕ → ℕ → ℕ} {densityBound : ℕ → ℕ} diff --git a/Complexity/Crypto/Computational/Pseudoentropy/MatrixExtraction.lean b/Complexity/Crypto/Computational/Pseudoentropy/MatrixExtraction.lean index faa9b4e46b..7a9501f4a3 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/MatrixExtraction.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/MatrixExtraction.lean @@ -57,15 +57,20 @@ noncomputable def extractMatrixLabels {Observation Label : Type} (inputBits outp (fun seed labels => LinearHash.wordHash outputBits seed (listRow inputBits 0 (prepare labels))) samples +/-- The hash-seed component of an extraction result `(observations, seed, digest)`. -/ +abbrev extractedSeed {Obs Seed Digest : Type*} (r : Obs × Seed × Digest) : Seed := r.2.1 + +/-- The hash-digest component of an extraction result `(observations, seed, digest)`. -/ +abbrev extractedDigest {Obs Seed Digest : Type*} (r : Obs × Seed × Digest) : Digest := r.2.2 + /-- Every result preserves the observations and has the declared seed and digest lengths. -/ theorem extractMatrixLabels_result {Observation Label : Type} (inputBits outputBits : ℕ) (prepare : List Label → List Bool) (samples : List (Observation × Label)) {result : List Observation × List Bool × List Bool} (hresult : result ∈ (ProbComp.eval (extractMatrixLabels inputBits outputBits prepare samples)).support) : - let sd := result.2 - result.1 = samples.map Prod.fst ∧ sd.1.length = outputBits * inputBits ∧ - sd.2.length = outputBits := by + result.1 = samples.map Prod.fst ∧ (extractedSeed result).length = outputBits * inputBits ∧ + (extractedDigest result).length = outputBits := by simp only [extractMatrixLabels, extractLabels, bind_pure_comp, ProbComp.eval_map, BitString.eval_sampleList, PMF.mem_support_map_iff] at hresult obtain ⟨seed, hseed, rfl⟩ := hresult @@ -106,8 +111,7 @@ theorem eval_extractMatrixLabels {Observation Label : Type} (inputBits outputBit (fun seed labels => LinearHash.hash (blocksEquiv (m := outputBits) (k := inputBits) seed) (ofList inputBits (prepare labels))) samples)).map (fun result => - let sd := result.2 - (result.1, List.ofFn sd.1, List.ofFn sd.2)) := by + (result.1, List.ofFn (extractedSeed result), List.ofFn (extractedDigest result))) := by have hrow (word : List Bool) : listRow inputBits 0 word = List.ofFn (ofList inputBits word) := listRow_eq_ofFn inputBits (0 : Fin 1) word @@ -122,8 +126,7 @@ theorem eval_extractMatrixLabelsIdeal {Observation : Type} (source : ProbComp Ob (extractLabelsIdeal (Output := BitString outputBits) source count (ProbComp.uniform (BitString (outputBits * inputBits)))).map (fun result => - let sd := result.2 - (result.1, List.ofFn sd.1, List.ofFn sd.2)) := by + (result.1, List.ofFn (extractedSeed result), List.ofFn (extractedDigest result))) := by simp only [extractMatrixLabelsIdeal, ProbComp.eval_bind, ProbComp.eval_pure, extractLabelsIdeal, ProbComp.eval_uniform, eval_sampleList, uniformList, Function.comp_def, PMF.map, PMF.bind_bind, PMF.pure_bind] @@ -136,8 +139,7 @@ theorem eval_extractMatrixLabelsIdeal_bind {Observation Output : Type} (next : List Observation → List Bool → ProbComp Output) : ProbComp.eval (do let result ← extractMatrixLabelsIdeal source count inputBits outputBits - let sd := result.2 - next result.1 (sd.1 ++ sd.2)) = + next result.1 (extractedSeed result ++ extractedDigest result)) = ProbComp.eval (do let observations ← OracleComp.replicate count source let bits ← BitString.sampleList (outputBits * inputBits + outputBits) @@ -153,8 +155,8 @@ theorem eval_extractMatrixLabelsIdeal_append {Observation : Type} (next : List Observation → ProbComp (List Bool)) : ProbComp.eval (do let result ← extractMatrixLabelsIdeal source count inputBits outputBits - let sd := result.2 - (fun front => front ++ (sd.1 ++ sd.2)) <$> next result.1) = + (fun front => front ++ (extractedSeed result ++ extractedDigest result)) <$> + next result.1) = ProbComp.eval (do let observations ← OracleComp.replicate count source let front ← next observations diff --git a/Complexity/Crypto/Computational/Pseudoentropy/RepeatedExtraction.lean b/Complexity/Crypto/Computational/Pseudoentropy/RepeatedExtraction.lean index 3c836e7c7e..8e472347b6 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/RepeatedExtraction.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/RepeatedExtraction.lean @@ -128,7 +128,7 @@ theorem isPPTOn_extractLabels {Param Observation Seed Output : Type} {input : Pa {seed : Param → ProbComp Seed} {hash : Param → Seed → List Bool → Output} {samples : Param → List (Observation × Bool)} (hseed : IsPPTOn input key seed) - (hhash : ComputableInPolyTime (fun pair => hash (Prod.fst pair.1) (Prod.snd pair.1) pair.2) + (hhash : ComputableInPolyTime (fun pair => hash pair.1.1 pair.1.2 pair.2) (encPair (encPair input key) encBits) output) (hsamples : ComputableInPolyTime samples input (encList (encPair observation encBool))) : IsPPTOn input (encPair (encList observation) (encPair key output)) @@ -143,7 +143,7 @@ theorem isPPTOn_extractLabels_list {Param Observation Label Seed Output : Type} {seed : Param → ProbComp Seed} {hash : Param → Seed → List Label → Output} {samples : Param → List (Observation × Label)} (hseed : IsPPTOn input key seed) - (hhash : ComputableInPolyTime (fun pair => hash (Prod.fst pair.1) (Prod.snd pair.1) pair.2) + (hhash : ComputableInPolyTime (fun pair => hash pair.1.1 pair.1.2 pair.2) (encPair (encPair input key) (encList label)) output) (hsamples : ComputableInPolyTime samples input (encList (encPair observation label))) : IsPPTOn input (encPair (encList observation) (encPair key output)) diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Selection.lean b/Complexity/Crypto/Computational/Pseudoentropy/Selection.lean index 5e62b336a0..1fc8e8ad52 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/Selection.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/Selection.lean @@ -70,7 +70,7 @@ theorem isPPTOn_selectPredictor {α : Type} {input : α ↪ List Bool} (htrials : ComputableInPolyTime trials input encUnary) (hsource : IsPPTOn input (encPair encBits encBool) source) (hpredict : IsPPTOn (encPair (encPair input encUnary) encBits) - encBool (fun x => predict (Prod.fst x.1) (Prod.snd x.1) x.2)) + encBool (fun x => predict x.1.1 x.1.2 x.2)) (hobservation : ComputableInPolyTime observation input encBits) : IsPPTOn input encBool (fun a => selectPredictor (count a) (trials a) (source a) (predict a) (observation a)) := by @@ -124,7 +124,7 @@ theorem HasGap.eventually_indexed_error_ge {pair : SamplablePair} {gap : ℕ → (hgap : pair.HasGap gap) (predict : ℕ → ℕ → List Bool → ProbComp Bool) (hpredict : IsPPTOn (encPair (encPair encUnary encUnary) encBits) encBool - (fun x => predict (Prod.fst x.1) (Prod.snd x.1) x.2)) + (fun x => predict x.1.1 x.1.2 x.2)) {count inverseTolerance : ℕ → ℕ} (hcount : ComputableInPolyTime count encUnary encUnary) (htolerance : ComputableInPolyTime inverseTolerance encUnary encUnary) diff --git a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource.lean b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource.lean index da6d3f841c..fea61b87dc 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource.lean @@ -58,11 +58,17 @@ namespace Cslib.Crypto.Pseudoentropy.ThreeSource open Probability BitString Turing.MultiTapeTM +/-- The observation word of a labeled seeded sample `((observation, label), seed)`. -/ +abbrev sampleObservation {Obs Label Seed : Type*} (s : (Obs × Label) × Seed) : Obs := s.1.1 + +/-- The label of a labeled seeded sample `((observation, label), seed)`. -/ +abbrev sampleLabel {Obs Label Seed : Type*} (s : (Obs × Label) × Seed) : Label := s.1.2 + /-- Finish the first two components by hashing observations and retaining the label hash. -/ noncomputable def finish (bound observationBits : ℕ) (middle : List (List Bool) × List Bool × List Bool) : ProbComp (List Bool) := do let first ← extractWordObservations bound observationBits middle.1 - return first ++ (Prod.fst middle.2 ++ Prod.snd middle.2) + return first ++ (extractedSeed middle ++ extractedDigest middle) /-- The last observation hash composes with a certified intermediate result. -/ theorem isPPTOn_finish {α : Type} {input : α ↪ List Bool} {bound observationBits : α → ℕ} @@ -72,7 +78,7 @@ theorem isPPTOn_finish {α : Type} {input : α ↪ List Bool} {bound observation (hmiddle : ComputableInPolyTime middle input (encPair (encList encBits) (encPair encBits encBits))) : IsPPTOn input encBits (fun a => finish (bound a) (observationBits a) (middle a)) := by - unfold finish + unfold finish extractedSeed extractedDigest ppt attribute [program_certificate] isPPTOn_finish @@ -84,7 +90,7 @@ noncomputable def extract (count seedBits bound observationBits labelBits remain let third ← extractWordSeeds count seedBits remainingBits samples let middle ← extractWordLabels count labelBits third.1 let front ← finish bound observationBits middle - return front ++ (Prod.fst third.2 ++ Prod.snd third.2) + return front ++ (extractedSeed third ++ extractedDigest third) /-- The complete three-component program is PPT from ordinary sampler and size certificates. -/ theorem isPPTOn_extract {α : Type} {input : α ↪ List Bool} @@ -177,7 +183,7 @@ def outputLength (count seedBits bound observationBits labelBits remainingBits : The statement also covers zero-sized components and malformed retained seeds. -/ theorem length_extract (count seedBits bound observationBits labelBits remainingBits : ℕ) (source : ProbComp ((List Bool × Bool) × List Bool)) - (hbound : ∀ sample ∈ (ProbComp.eval source).support, (Prod.fst sample.1).length ≤ bound) + (hbound : ∀ sample ∈ (ProbComp.eval source).support, (sampleObservation sample).length ≤ bound) {output : List Bool} (houtput : output ∈ (ProbComp.eval (extract count seedBits bound observationBits labelBits remainingBits source)).support) : output.length = outputLength count seedBits bound observationBits labelBits remainingBits := by @@ -255,8 +261,7 @@ theorem eval_ideal_remaining let third ← extractMatrixLabelsIdeal source count (count * seedBits) remainingBits let middle ← extractWordLabels count labelBits third.1 let front ← finish bound observationBits middle - let thirdSd := third.2 - return front ++ (thirdSd.1 ++ thirdSd.2)) = + return front ++ (extractedSeed third ++ extractedDigest third)) = ProbComp.eval (withoutSeeds count seedBits bound observationBits labelBits remainingBits source) := by simpa only [withoutSeeds, ProbComp.eval_bind, ProbComp.eval_map, ProbComp.eval_pure, @@ -383,7 +388,7 @@ theorem replace_indexed_labels {pair : SamplablePair} {gap : ℕ → ℝ} (hpair ((numerator n (choose n) : ℝ) / dyadicSize (densityBound n))) (adversary : ℕ → ℕ → List Bool → ProbComp Bool) (hadversary : IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => adversary (Prod.fst input.1) (Prod.snd input.1) input.2)) : + encBool (fun input => adversary input.1.1 input.1.2 input.2)) : let count := fun n => ExtractionSchedule.count n (saved.length n) (inverseSlack n) Negligible (fun n => Game.advantage (ProbComp.eval (withoutSeeds (count n) (saved.length n) (bound n) @@ -483,7 +488,7 @@ theorem SamplablePair.HasGap.extract_indexed_three {pair : SamplablePair} {gap : conditionalEntropy (pair.joint n))) (test : ℕ → ℕ → List Bool → ProbComp Bool) (htest : IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => test (Prod.fst input.1) (Prod.snd input.1) input.2)) : + encBool (fun input => test input.1.1 input.1.2 input.2)) : let count := fun n => ExtractionSchedule.count n (saved.length n) (inverseSlack n) Negligible (fun n => Game.advantage (ProbComp.eval (ThreeSource.extract (count n) (saved.length n) (bound n) diff --git a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Amplification.lean b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Amplification.lean index 32161545be..77f1bee898 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Amplification.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Amplification.lean @@ -58,10 +58,9 @@ theorem isPolyTime_amplifiedGenerate {pair : SamplablePair} (saved : pair.SeedRe (hdensity : ComputableInPolyTime densityBound encUnary encUnary) (hcommon : ComputableInPolyTime common encUnary encUnary) : ComputableInPolyTime - (fun input => amplifiedGenerate (Prod.fst input.1) (saved.length (Prod.fst input.1)) - (observationBound (Prod.fst input.1)) (densityBound (Prod.fst input.1)) - (common (Prod.fst input.1)) (Prod.snd input.1) - (saved.evaluate (Prod.fst input.1)) input.2) + (fun input => amplifiedGenerate input.1.1 (saved.length input.1.1) + (observationBound input.1.1) (densityBound input.1.1) (common input.1.1) input.1.2 + (saved.evaluate input.1.1) input.2) (encPair (encPair encUnary encUnary) encBits) encBits := by have hlength := saved.length_isPolyTime have hsize := isPolyTime_size hlength hdensity @@ -105,7 +104,7 @@ theorem exists_secure_amplified_choice {pair : SamplablePair} {gap : ℕ → ℝ (∀ᶠ n in atTop, choose n < size (saved.length n) (densityBound n)) ∧ ∀ test : ℕ → ℕ → List Bool → ProbComp Bool, IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => test (Prod.fst input.1) (Prod.snd input.1) input.2) → + encBool (fun input => test input.1.1 input.1.2 input.2) → Negligible (fun n => Game.advantage (((uniformList (common n)).map (amplifiedGenerate n (saved.length n) (observationBound n) (densityBound n) (common n) (choose n) (saved.evaluate n))).bind diff --git a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Candidates.lean b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Candidates.lean index b082e0e162..f4555e5b49 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Candidates.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Candidates.lean @@ -127,10 +127,9 @@ theorem isPolyTime_generate_of_realization {pair : SamplablePair} (saved : pair. {observationBound densityBound : ℕ → ℕ} (hobservation : ComputableInPolyTime observationBound encUnary encUnary) (hdensity : ComputableInPolyTime densityBound encUnary encUnary) : - ComputableInPolyTime (fun input => generate (Prod.fst input.1) - (saved.length (Prod.fst input.1)) - (observationBound (Prod.fst input.1)) (densityBound (Prod.fst input.1)) (Prod.snd input.1) - (saved.evaluate (Prod.fst input.1)) input.2) + ComputableInPolyTime (fun input => generate input.1.1 (saved.length input.1.1) + (observationBound input.1.1) (densityBound input.1.1) input.1.2 + (saved.evaluate input.1.1) input.2) (encPair (encPair encUnary encUnary) encBits) encBits := by have hlength := saved.length_isPolyTime have hevaluate := saved.efficient @@ -186,7 +185,7 @@ theorem exists_secure_choice {pair : SamplablePair} {gap : ℕ → ℝ} (∀ᶠ n in atTop, choose n < size (saved.length n) (densityBound n)) ∧ ∀ test : ℕ → ℕ → List Bool → ProbComp Bool, IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => test (Prod.fst input.1) (Prod.snd input.1) input.2) → + encBool (fun input => test input.1.1 input.1.2 input.2) → Negligible (fun n => Game.advantage (((uniformList (seedLength n (saved.length n) (observationBound n) (densityBound n) (choose n))).map (generate n (saved.length n) (observationBound n) (densityBound n) diff --git a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Padding.lean b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Padding.lean index a197bcb7ed..6be4636a75 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Padding.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Padding.lean @@ -101,11 +101,9 @@ theorem isPolyTime_paddedGenerate {pair : SamplablePair} (saved : pair.SeedReali (hobservation : ComputableInPolyTime observationBound encUnary encUnary) (hdensity : ComputableInPolyTime densityBound encUnary encUnary) (hcommon : ComputableInPolyTime common encUnary encUnary) : - ComputableInPolyTime (fun input => paddedGenerate (Prod.fst input.1) - (saved.length (Prod.fst input.1)) - (observationBound (Prod.fst input.1)) (densityBound (Prod.fst input.1)) - (common (Prod.fst input.1)) (Prod.snd input.1) - (saved.evaluate (Prod.fst input.1)) input.2) + ComputableInPolyTime (fun input => paddedGenerate input.1.1 (saved.length input.1.1) + (observationBound input.1.1) (densityBound input.1.1) (common input.1.1) input.1.2 + (saved.evaluate input.1.1) input.2) (encPair (encPair encUnary encUnary) encBits) encBits := by have hobservation := hobservation.tidy have hdensity := hdensity.tidy @@ -145,7 +143,7 @@ theorem exists_secure_padded_choice {pair : SamplablePair} {gap : ℕ → ℝ} (∀ᶠ n in atTop, choose n < size (saved.length n) (densityBound n)) ∧ ∀ test : ℕ → ℕ → List Bool → ProbComp Bool, IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => test (Prod.fst input.1) (Prod.snd input.1) input.2) → + encBool (fun input => test input.1.1 input.1.2 input.2) → Negligible (fun n => Game.advantage (((uniformList (common n)).map (paddedGenerate n (saved.length n) (observationBound n) (densityBound n) (common n) (choose n) (saved.evaluate n))).bind diff --git a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Seeded.lean b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Seeded.lean index f5a165a3fe..90ca53efe5 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Seeded.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Seeded.lean @@ -53,8 +53,8 @@ open Probability BitString Turing.MultiTapeTM def hashSamples (count seedBits bound observationBits labelBits remainingBits : ℕ) (samples : List ((List Bool × Bool) × List Bool)) (firstKey middleKey lastKey : List Bool) : List Bool := - let observations := ((samples.map (fun sample => Prod.fst sample.1)).map (padWord bound)).flatten - let labels := listRow count 0 (samples.map (fun sample => Prod.snd sample.1)) + let observations := ((samples.map sampleObservation).map (padWord bound)).flatten + let labels := listRow count 0 (samples.map sampleLabel) let seeds := listRow (count * seedBits) 0 (samples.map Prod.snd).flatten ((firstKey ++ LinearHash.wordHash observationBits firstKey observations) ++ (middleKey ++ LinearHash.wordHash labelBits middleKey labels)) ++ @@ -202,13 +202,12 @@ theorem generate_distribution (count seedBits bound observationBits labelBits re probabilistic hashing calls exactly. Only the observation padding requires a size bound. -/ theorem eval_hashSamples (count seedBits bound observationBits labelBits remainingBits : ℕ) (samples : List ((List Bool × Bool) × List Bool)) (hcount : samples.length = count) - (hbound : ∀ sample ∈ samples, (Prod.fst sample.1).length ≤ bound) : + (hbound : ∀ sample ∈ samples, (sampleObservation sample).length ≤ bound) : ProbComp.eval (do let third ← extractWordSeeds count seedBits remainingBits samples let middle ← extractWordLabels count labelBits third.1 let front ← finish bound observationBits middle - let thirdSd := third.2 - return front ++ (thirdSd.1 ++ thirdSd.2)) = + return front ++ (extractedSeed third ++ extractedDigest third)) = (do let lastKey ← uniformList (remainingBits * (count * seedBits)) let middleKey ← uniformList (labelBits * count) diff --git a/Complexity/Crypto/Computational/Pseudoentropy/WordExtraction.lean b/Complexity/Crypto/Computational/Pseudoentropy/WordExtraction.lean index 64438e12d2..63a79e15c3 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/WordExtraction.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/WordExtraction.lean @@ -82,8 +82,7 @@ theorem eval_extractWordLabels (count outputBits : ℕ) (samples : List (List Bo (fun seed bits => LinearHash.hash (blocksEquiv (m := outputBits) (k := count) seed) (ofList count bits)) samples)).map (fun result => - let sd := result.2 - (result.1, List.ofFn sd.1, List.ofFn sd.2)) := by + (result.1, List.ofFn (extractedSeed result), List.ofFn (extractedDigest result))) := by exact eval_extractMatrixLabels count outputBits id samples /-- The ideal word program agrees with the finite ideal distribution and retains the full seed. -/ @@ -92,8 +91,7 @@ theorem eval_extractWordLabelsIdeal (source : ProbComp (List Bool)) (count outpu (extractLabelsIdeal (Output := BitString outputBits) source count (ProbComp.uniform (BitString (outputBits * count)))).map (fun result => - let sd := result.2 - (result.1, List.ofFn sd.1, List.ofFn sd.2)) := by + (result.1, List.ofFn (extractedSeed result), List.ofFn (extractedDigest result))) := by exact eval_extractMatrixLabelsIdeal source count count outputBits /-- An ordinary word test after extraction gives the finite test required by the security @@ -113,8 +111,8 @@ theorem isPPTOn_extractedWordTest {α : Type} {input : α ↪ List Bool} {count (fun seed bits => LinearHash.hash (blocksEquiv (m := outputBits input.1) (k := count input.1) seed) (ofList (count input.1) bits)) input.2 - let sd := result.2 - test input.1 (result.1, List.ofFn sd.1, List.ofFn sd.2)) := by + test input.1 + (result.1, List.ofFn (extractedSeed result), List.ofFn (extractedDigest result))) := by have hword : IsPPTOn (encPair input (encList (encPair encBits encBool))) encBool (fun input => extractWordLabels (count input.1) (outputBits input.1) input.2 >>= @@ -150,7 +148,7 @@ theorem SamplablePair.HasGap.extract_indexed_word_labels {pair : SamplablePair} (test : ℕ → ℕ → List (List Bool) × List Bool × List Bool → ProbComp Bool) (htest : IsPPTOn (encPair (encPair encUnary encUnary) (encPair (encList encBits) (encPair encBits encBits))) - encBool (fun input => test (Prod.fst input.1) (Prod.snd input.1) input.2)) : + encBool (fun input => test input.1.1 input.1.2 input.2)) : let count := fun n => ExtractionSchedule.count n (realization.length n) (inverseSlack n) Negligible (fun n => Game.advantage (ProbComp.eval (do diff --git a/Complexity/Crypto/Computational/PseudorandomFunction/Coins.lean b/Complexity/Crypto/Computational/PseudorandomFunction/Coins.lean index 0f1409bae8..4f9b3823e5 100644 --- a/Complexity/Crypto/Computational/PseudorandomFunction/Coins.lean +++ b/Complexity/Crypto/Computational/PseudorandomFunction/Coins.lean @@ -117,8 +117,7 @@ theorem length_prfCoins {family : List Bool → List Bool → List Bool} theorem computableInPolyTime_prfCoins {family : List Bool → List Bool → List Bool} (hF : ComputableInPolyTime (fun p : List Bool × List Bool => family p.1 p.2) (encPair encBits encBits) encBits) : - ComputableInPolyTime - (fun p : List Bool × List Bool × ℕ => prfCoins family p.1 (Prod.fst p.2) (Prod.snd p.2)) + ComputableInPolyTime (fun p : List Bool × List Bool × ℕ => prfCoins family p.1 p.2.1 p.2.2) (encPair encBits (encPair encBits encUnary)) encBits := by unfold prfCoins padRequest polytime diff --git a/Complexity/Crypto/Computational/Stretch.lean b/Complexity/Crypto/Computational/Stretch.lean index 4eca932256..c1065b21cb 100644 --- a/Complexity/Crypto/Computational/Stretch.lean +++ b/Complexity/Crypto/Computational/Stretch.lean @@ -352,13 +352,13 @@ The choice is supplied only in the proof; each reduction receives its index as o theorem indexed_indistinguishable {generator : ℕ → ℕ → List Bool → List Bool} {seedBits count choose : ℕ → ℕ} (hgenerator : ComputableInPolyTime - (fun input => generator (Prod.fst input.1) (Prod.snd input.1) input.2) + (fun input => generator input.1.1 input.1.2 input.2) (encPair (encPair encUnary encUnary) encBits) encBits) (hseedBits : ComputableInPolyTime seedBits encUnary encUnary) (hcount : ComputableInPolyTime count encUnary encUnary) (hsecure : ∀ adversary : ℕ → ℕ → List Bool → ProbComp Bool, IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => adversary (Prod.fst input.1) (Prod.snd input.1) input.2) → + encBool (fun input => adversary input.1.1 input.1.2 input.2) → Negligible (fun n => Game.advantage (((uniformList (seedBits n)).map (generator n (choose n))).bind (fun word => ProbComp.eval (adversary n (choose n) word))) @@ -366,7 +366,7 @@ theorem indexed_indistinguishable {generator : ℕ → ℕ → List Bool → Lis (fun word => ProbComp.eval (adversary n (choose n) word))))) : ∀ adversary : ℕ → ℕ → List Bool → ProbComp Bool, IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => adversary (Prod.fst input.1) (Prod.snd input.1) input.2) → + encBool (fun input => adversary input.1.1 input.1.2 input.2) → Negligible (fun n => Game.advantage (((uniformList (seedBits n)).map (iterate (generator n (choose n)) (seedBits n) (count n))).bind diff --git a/Complexity/Crypto/Computational/Stretch/Quantitative.lean b/Complexity/Crypto/Computational/Stretch/Quantitative.lean index ab03a0ef43..6a3685017a 100644 --- a/Complexity/Crypto/Computational/Stretch/Quantitative.lean +++ b/Complexity/Crypto/Computational/Stretch/Quantitative.lean @@ -686,17 +686,15 @@ theorem computableInTimeAndSpace_forwardIterate_captured {α : Type} (hgen : ComputableInTimeAndSpace (fun p : α × List Bool => generator p.1 p.2) (encPair encParam encBits) encBits tGen sGen) {Q : (α × List Bool) × ℕ → ℕ} - (hspace : ∀ x i, i < x.2 → - sGen (Prod.fst x.1, seedAt (generator (Prod.fst x.1)) (Prod.snd x.1) i) ≤ Q x) : + (hspace : ∀ x i, i < x.2 → sGen (x.1.1, seedAt (generator x.1.1) x.1.2 i) ≤ Q x) : ∃ c, ComputableInTimeAndSpace - (fun x : (α × List Bool) × ℕ => - forwardIterate (generator (Prod.fst x.1)) x.2 (Prod.snd x.1)) + (fun x : (α × List Bool) × ℕ => forwardIterate (generator x.1.1) x.2 x.1.2) (encPair (encPair encParam encBits) encUnary) encBits - (fun x => c * ((encParam (Prod.fst x.1)).length + (Prod.snd x.1).length + x.2 + + (fun x => c * ((encParam x.1.1).length + x.1.2.length + x.2 + (∑ i ∈ Finset.range x.2, - (tGen (Prod.fst x.1, seedAt (generator (Prod.fst x.1)) (Prod.snd x.1) i) + - (encParam (Prod.fst x.1)).length + (Prod.snd x.1).length + 1)) + 1)) - (fun x => c * (Q x + (encParam (Prod.fst x.1)).length + (Prod.snd x.1).length + 1)) := by + (tGen (x.1.1, seedAt (generator x.1.1) x.1.2 i) + + (encParam x.1.1).length + x.1.2.length + 1)) + 1)) + (fun x => c * (Q x + (encParam x.1.1).length + x.1.2.length + 1)) := by -- Retain the captured streaming construction as a proof-local raw witness. have build {α : Type} {encParam : α ↪ List Bool} {generator : α → List Bool → List Bool} @@ -837,18 +835,15 @@ theorem computableInTimeAndSpace_iterate_captured {α : Type} (hgen : ComputableInTimeAndSpace (fun p : α × List Bool => generator p.1 p.2) (encPair encParam encBits) encBits tGen sGen) {Q : (α × List Bool) × ℕ → ℕ} - (hspace : ∀ x i, i < x.2 → - sGen (Prod.fst x.1, seedAt (generator (Prod.fst x.1)) (Prod.snd x.1) i) ≤ Q x) : + (hspace : ∀ x i, i < x.2 → sGen (x.1.1, seedAt (generator x.1.1) x.1.2 i) ≤ Q x) : ∃ c, ComputableInTimeAndSpace - (fun x : (α × List Bool) × ℕ => - iterate (generator (Prod.fst x.1)) (Prod.snd x.1).length x.2 (Prod.snd x.1)) + (fun x : (α × List Bool) × ℕ => iterate (generator x.1.1) x.1.2.length x.2 x.1.2) (encPair (encPair encParam encBits) encUnary) encBits - (fun x => c * ((encParam (Prod.fst x.1)).length + (Prod.snd x.1).length + x.2 + + (fun x => c * ((encParam x.1.1).length + x.1.2.length + x.2 + (∑ i ∈ Finset.range x.2, - (tGen (Prod.fst x.1, seedAt (generator (Prod.fst x.1)) (Prod.snd x.1) i) + - (encParam (Prod.fst x.1)).length + (Prod.snd x.1).length + 1)) + 1)) - (fun x => - c * (Q x + (encParam (Prod.fst x.1)).length + (Prod.snd x.1).length + x.2 + 1)) := by + (tGen (x.1.1, seedAt (generator x.1.1) x.1.2 i) + + (encParam x.1.1).length + x.1.2.length + 1)) + 1)) + (fun x => c * (Q x + (encParam x.1.1).length + x.1.2.length + x.2 + 1)) := by obtain ⟨c, hfwd⟩ := computableInTimeAndSpace_forwardIterate_captured hlen hgen hspace have hcharged := hfwd.mono (fun _ => le_rfl) (fun x => show c * (Q x + (encParam x.1.1).length + x.1.2.length + 1) ≤ diff --git a/Complexity/Crypto/Computational/UniformChoice.lean b/Complexity/Crypto/Computational/UniformChoice.lean index 70b38fa6b5..a99d5c3ed6 100644 --- a/Complexity/Crypto/Computational/UniformChoice.lean +++ b/Complexity/Crypto/Computational/UniformChoice.lean @@ -77,7 +77,7 @@ theorem isPPTOn_test {α : Type} {input : α ↪ List Bool} (hreal : IsPPTOn input encBits real) (hideal : IsPPTOn input encBits ideal) (hadversary : IsPPTOn (encPair (encPair input encUnary) encBits) encBool - (fun a => adversary (Prod.fst a.1) (Prod.snd a.1) a.2)) + (fun a => adversary a.1.1 a.1.2 a.2)) (hchallenge : ComputableInPolyTime challenge input encBits) : IsPPTOn input encBool (fun a => test (bound a) (real a) (ideal a) (adversary a) (challenge a)) := by @@ -149,7 +149,7 @@ theorem ComputationallyIndistinguishable.uniform_bound (hbound : ComputableInPolyTime bound encUnary encUnary) (adversary : ℕ → ℕ → List Bool → ProbComp Bool) (hadversary : IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun a => adversary (Prod.fst a.1) (Prod.snd a.1) a.2)) : + encBool (fun a => adversary a.1.1 a.1.2 a.2)) : ∃ ε : ℕ → ℝ≥0, Negligible ε ∧ ∀ n index, index ≤ bound n → Game.advantage (ProbComp.eval (real n >>= adversary n index)) (ProbComp.eval (ideal n >>= adversary n index)) ≤ ε n := by diff --git a/Complexity/Crypto/Primitives/PRG/NisanWigderson/Sampling.lean b/Complexity/Crypto/Primitives/PRG/NisanWigderson/Sampling.lean index cc2a4579c1..86e0931aed 100644 --- a/Complexity/Crypto/Primitives/PRG/NisanWigderson/Sampling.lean +++ b/Complexity/Crypto/Primitives/PRG/NisanWigderson/Sampling.lean @@ -128,10 +128,7 @@ deriving DecidableEq, Fintype /-- A trial is its four random choices. -/ def Trial.equivProd : Trial ℓ m ≃ Fin m × (Fin ℓ → Bool) × Bool × (Fin m → Bool) where toFun t := (t.pos, t.seed, t.bit, t.pad) - invFun p := - let rest := p.2 - let bp := rest.2 - ⟨p.1, rest.1, bp.1, bp.2⟩ + invFun := fun (pos, seed, bit, pad) => ⟨pos, seed, bit, pad⟩ instance [NeZero m] : Nonempty (Trial ℓ m) := ⟨⟨0, fun _ => false, false, fun _ => false⟩⟩ From 9d4c554a88ae6ef3461889b5c942c4304984b414 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 2 Nov 2026 16:37:21 +0000 Subject: [PATCH 3/3] refactor(Crypto): rename Desc.generatorResidue and destructure tuples (#1764) --- .../Computational/DiffieHellman/MultiDDH.lean | 17 ++++------------- .../Computational/DiscreteLog/SchnorrGroup.lean | 16 ++++++++-------- .../Crypto/Computational/NaorReingold.lean | 5 +++-- .../Computational/NaorReingold/Security.lean | 5 +---- Complexity/Crypto/Computational/OneWay/NP.lean | 2 ++ .../Computational/Pseudoentropy/Seed.lean | 5 ++--- 6 files changed, 20 insertions(+), 30 deletions(-) diff --git a/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean b/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean index fde1c9ebee..039e5e294a 100644 --- a/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean +++ b/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean @@ -43,15 +43,6 @@ variable (F : PrimeOrderGroupFamily) /-! ### Fixed-$u$ DDH random self-reduction and Multi-DDH (I) (Exercises 10.8 & 10.11) -/ -/-- The first element `u` of a candidate Diffie–Hellman triple `(u, v, w)`. -/ -abbrev ddhU {G : Type*} (t : G × G × G) : G := t.1 - -/-- The second element `v` of a candidate Diffie–Hellman triple `(u, v, w)`. -/ -abbrev ddhV {G : Type*} (t : G × G × G) : G := t.2.1 - -/-- The third element `w` of a candidate Diffie–Hellman triple `(u, v, w)`. -/ -abbrev ddhW {G : Type*} (t : G × G × G) : G := t.2.2 - /-- Fixed-$u$ DDH rerandomization ([BonehShoup2023], Section 10.11, Exercise 10.8, p. 425): given `(u, v, w)` and exponents `σ, τ : ZMod (F.order d)`, output `(v*, w*) = (σ • g + τ • v, σ • u + τ • w)`. -/ @@ -296,10 +287,10 @@ theorem advantage_multiDDH_le (d : F.Desc) (ι : Type*) [Fintype ι] [DecidableE ((PMF.uniformOfFintype (ZMod (F.order d))).bind fun α => (F.multiDDHIdealTupleLaw d ι).bind (test (α • F.generator d))) ≤ Game.advantage - ((F.ddhRealTupleLaw d).bind fun t => - (F.multiDDHRerandomizeLaw d ι (ddhU t) (ddhV t) (ddhW t)).bind (test (ddhU t))) - ((F.ddhIdealTupleLaw d).bind fun t => - (F.multiDDHRerandomizeLaw d ι (ddhU t) (ddhV t) (ddhW t)).bind (test (ddhU t))) + + ((F.ddhRealTupleLaw d).bind fun (u, v, w) => + (F.multiDDHRerandomizeLaw d ι u v w).bind (test u)) + ((F.ddhIdealTupleLaw d).bind fun (u, v, w) => + (F.multiDDHRerandomizeLaw d ι u v w).bind (test u)) + (F.order d : ℝ≥0)⁻¹ := by have hreal : ((F.ddhRealTupleLaw d).bind fun t => diff --git a/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean b/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean index 5819540bf0..3b683198dc 100644 --- a/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean +++ b/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean @@ -58,7 +58,7 @@ abbrev rawModulus (d : ℕ × ℕ × ℕ) : ℕ := d.1 abbrev rawOrder (d : ℕ × ℕ × ℕ) : ℕ := d.2.1 /-- The subgroup generator residue `g` of a raw Schnorr-group description `(p, q, g)`. -/ -abbrev rawGenerator (d : ℕ × ℕ × ℕ) : ℕ := d.2.2 +abbrev rawGeneratorResidue (d : ℕ × ℕ × ℕ) : ℕ := d.2.2 /-- A valid description `(p, q, g)` of a Schnorr group: `p` and `q` are prime, and the residue `g` satisfies `1 < g < p` and `g ^ q ≡ 1 (mod p)`. -/ @@ -68,11 +68,11 @@ structure Valid (d : ℕ × ℕ × ℕ) : Prop where /-- The group order is prime. -/ prime_order : (rawOrder d).Prime /-- The generator is not `0` or `1`. -/ - one_lt_generator : 1 < rawGenerator d + one_lt_generator : 1 < rawGeneratorResidue d /-- The generator is a reduced residue. -/ - generator_lt : rawGenerator d < rawModulus d + generator_lt : rawGeneratorResidue d < rawModulus d /-- The generator has order dividing `q`. -/ - generator_pow : rawGenerator d ^ rawOrder d % rawModulus d = 1 + generator_pow : rawGeneratorResidue d ^ rawOrder d % rawModulus d = 1 /-- Valid Schnorr-group descriptions. -/ abbrev Desc : Type := {d : ℕ × ℕ × ℕ // Valid d} @@ -84,11 +84,11 @@ abbrev Desc.modulus (d : Desc) : ℕ := rawModulus d.val abbrev Desc.order (d : Desc) : ℕ := rawOrder d.val /-- The subgroup generator residue `g` of a valid Schnorr-group description `(p, q, g)`. -/ -abbrev Desc.generator (d : Desc) : ℕ := rawGenerator d.val +abbrev Desc.generatorResidue (d : Desc) : ℕ := rawGeneratorResidue d.val /-- The generator as a unit modulo `p`. -/ def generatorUnit (d : Desc) : (ZMod d.modulus)ˣ := - ZMod.unitOfCoprime d.generator ((Nat.coprime_comm.mp + ZMod.unitOfCoprime d.generatorResidue ((Nat.coprime_comm.mp ((d.2.prime_modulus.coprime_iff_not_dvd).mpr (Nat.not_dvd_of_pos_of_lt (by have := d.2.one_lt_generator; lia) d.2.generator_lt)))) @@ -173,7 +173,7 @@ theorem smul_encode (d : Desc) (a : ℕ) (x : Carrier d) : rw [← ZMod.val_natCast, Nat.cast_pow, ZMod.natCast_zmod_val] /-- The encoded generator is the binary digits of `g`. -/ -theorem encode_generator (d : Desc) : encode d (generator d) = d.generator.bits := by +theorem encode_generator (d : Desc) : encode d (generator d) = d.generatorResidue.bits := by change (((generatorUnit d : (ZMod d.1.1)ˣ) : ZMod d.1.1).val).bits = _ rw [generatorUnit, ZMod.coe_unitOfCoprime, ZMod.val_natCast, Nat.mod_eq_of_lt d.2.generator_lt] @@ -199,7 +199,7 @@ theorem computableInPolyTime_order : theorem computableInPolyTime_generator : ComputableInPolyTime (fun d => encode d (generator d)) encDesc encBits := by have := computableInPolyTime_val - simp only [encode_generator, Desc.generator, rawGenerator] + simp only [encode_generator, Desc.generatorResidue, rawGeneratorResidue] fun_prop /-- Multiplication modulo `p` is computable in polynomial time. -/ diff --git a/Complexity/Crypto/Computational/NaorReingold.lean b/Complexity/Crypto/Computational/NaorReingold.lean index c413028be3..c8ee48fac5 100644 --- a/Complexity/Crypto/Computational/NaorReingold.lean +++ b/Complexity/Crypto/Computational/NaorReingold.lean @@ -602,8 +602,9 @@ rerandomize it into a `BitString k`-indexed family via `multiDDHRerandomizeLaw` noncomputable def naorReingoldLevelDDHDistinguisher (d : F.Desc) {n : ℕ} (k : ℕ) (hk : k < n) (adv : OracleComp (fun _ : BitString n => F.Carrier d) Bool) (t : F.Carrier d × F.Carrier d × F.Carrier d) : PMF Bool := - (F.multiDDHRerandomizeLaw d (BitString k) (ddhU t) (ddhV t) (ddhW t)).bind - (F.naorReingoldLevelTest d k hk adv (ddhU t)) + let (u, v, w) := t + (F.multiDDHRerandomizeLaw d (BitString k) u v w).bind + (F.naorReingoldLevelTest d k hk adv u) /-- Under `multiDDHRealTupleLaw`, `naorReingoldLevelTest` reproduces `naorReingoldHybridGame` at depth `k`. -/ diff --git a/Complexity/Crypto/Computational/NaorReingold/Security.lean b/Complexity/Crypto/Computational/NaorReingold/Security.lean index 2cc412e4a3..ba90de50fe 100644 --- a/Complexity/Crypto/Computational/NaorReingold/Security.lean +++ b/Complexity/Crypto/Computational/NaorReingold/Security.lean @@ -467,10 +467,7 @@ noncomputable def naorReingoldToDDHDistinguisher (inLen : ℕ → ℕ) let m := inLen n let k ← ProbComp.sampleDyadicIndex m if k < m then do - let d := input.1 - let u := ddhU input.2 - let v := ddhV input.2 - let w := ddhW input.2 + let (d, u, v, w) := input let αs ← OracleComp.replicate (m - (k + 1)) (F.sampleNaorReingoldExp n d) Prod.fst <$> (OracleComp.interpret (OracleComp.sumHandler (fun r => StateT.lift (ProbComp.unifFin r)) diff --git a/Complexity/Crypto/Computational/OneWay/NP.lean b/Complexity/Crypto/Computational/OneWay/NP.lean index 3185953ad7..c1ea23559a 100644 --- a/Complexity/Crypto/Computational/OneWay/NP.lean +++ b/Complexity/Crypto/Computational/OneWay/NP.lean @@ -82,6 +82,8 @@ length `n` that starts with `u` satisfies `f x = y`. -/ def preimagePrefix (f : List Bool → List Bool) : Set (ℕ × List Bool × List Bool) := {(n, y, u) : ℕ × List Bool × List Bool | ∃ x : List Bool, x.length = n ∧ u <+: x ∧ f x = y} +/-- Membership in `preimagePrefix f`: `(n, y, u) ∈ preimagePrefix f` iff `y` has an `n`-bit +preimage under `f` with prefix `u`. -/ @[simp] theorem mem_preimagePrefix {f : List Bool → List Bool} {n : ℕ} {y u : List Bool} : (n, y, u) ∈ preimagePrefix f ↔ ∃ x : List Bool, x.length = n ∧ u <+: x ∧ f x = y := by simp [preimagePrefix] diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Seed.lean b/Complexity/Crypto/Computational/Pseudoentropy/Seed.lean index 2c5898014d..c82384af68 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/Seed.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/Seed.lean @@ -211,9 +211,8 @@ theorem isPPTOn_sampleWithSeed : IsPPTOn encUnary /-- The efficient program exactly realizes the finite joint experiment with its retained seed. -/ theorem eval_sampleWithSeed (n : ℕ) : ProbComp.eval (seed.sampleWithSeed n) = - (seed.jointWithSeed n).map (fun result => - let obs := result.1 - ((pair.encode n obs.1, obs.2), List.ofFn result.2)) := by + (seed.jointWithSeed n).map (fun ((obs, label), bits) => + ((pair.encode n obs, label), List.ofFn bits)) := by simp only [sampleWithSeed, bind_pure_comp, ProbComp.eval_map, jointWithSeed, PMF.map_comp, Function.comp_def, seed.encode_output] simp only [BitString.eval_sampleList, BitString.uniformList, PMF.map_comp, Function.comp_def]