diff --git a/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean b/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean index 233ecc65e0..039e5e294a 100644 --- a/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean +++ b/Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean @@ -287,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 ι t.1 t.2.1 t.2.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)) + + ((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 b2abfcbe5b..3b683198dc 100644 --- a/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean +++ b/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean @@ -51,55 +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 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)`. -/ 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 : d.2.1.Prime + prime_order : (rawOrder d).Prime /-- The generator is not `0` or `1`. -/ - one_lt_generator : 1 < d.2.2 + one_lt_generator : 1 < rawGeneratorResidue d /-- The generator is a reduced residue. -/ - generator_lt : d.2.2 < d.1 + generator_lt : rawGeneratorResidue d < rawModulus d /-- The generator has order dividing `q`. -/ - generator_pow : d.2.2 ^ d.2.1 % d.1 = 1 + generator_pow : rawGeneratorResidue 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.generatorResidue (d : Desc) : ℕ := rawGeneratorResidue d.val + /-- 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.modulus)ˣ := + 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)))) /-- 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 d.order.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 ^ 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 ^ d.1.2.1 = 1 := by +theorem pow_order (d : Desc) (x : Subgroup.zpowers (generatorUnit d)) : + 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 d.1.2.1) (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.1.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.1.1)ˣ => (u : ZMod d.1.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 @@ -110,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) = d.1.2.1 := 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.1.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.1.1)ˣ) : - ZMod d.1.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 => @@ -134,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 input.2.1 * ofBits input.2.2 % input.1.1.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) : @@ -143,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 input.2.2 ^ input.2.1 % input.1.1.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 d.1.2.1) • 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) = d.1.2.2.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] @@ -170,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 => d.1.2.1) 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.generatorResidue, rawGeneratorResidue] 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. -/ @@ -197,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 @@ -208,7 +229,7 @@ of prime order with efficient operations. -/ def schnorrGroups : PrimeOrderGroupFamily where Desc := SchnorrGroup.Desc encDesc := SchnorrGroup.encDesc - order d := d.1.2.1 + 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 3a94453e20..9e65d78ea0 100644 --- a/Complexity/Crypto/Computational/GeneratorXor.lean +++ b/Complexity/Crypto/Computational/GeneratorXor.lean @@ -257,7 +257,7 @@ theorem indistinguishable {generator : ℕ → ℕ → List Bool → List Bool} (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 ((n, i), word) => adversary n i word) → 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..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) t.1 t.2.1 t.2.2).bind - (F.naorReingoldLevelTest d k hk adv t.1) + 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 049fbca1c2..ba90de50fe 100644 --- a/Complexity/Crypto/Computational/NaorReingold/Security.lean +++ b/Complexity/Crypto/Computational/NaorReingold/Security.lean @@ -467,12 +467,13 @@ 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, 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)) - (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 v w αs request.2)) + (adversary n (F.encDesc d))).run [] else pure false private theorem isPPTOn_sampleNaorReingoldPair (F : PrimeOrderGroupFamily) diff --git a/Complexity/Crypto/Computational/OneWay/NP.lean b/Complexity/Crypto/Computational/OneWay/NP.lean index bc97be611f..c1ea23559a 100644 --- a/Complexity/Crypto/Computational/OneWay/NP.lean +++ b/Complexity/Crypto/Computational/OneWay/NP.lean @@ -80,7 +80,13 @@ 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} + {(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] /-- The encoding of instances of the preimage-prefix problem: the length `n` in unary, then the image and the prefix. -/ @@ -95,7 +101,8 @@ 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 ((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) : @@ -107,14 +114,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 => ?_⟩ @@ -131,7 +139,11 @@ 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 @@ -171,15 +183,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 @@ -191,14 +203,13 @@ 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 rw [heq] exact hfx' diff --git a/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean b/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean index 9ee9d0cdb5..904335d07e 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 ((n, i), samples) => test n i samples)) {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..8b48ecfb14 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean @@ -154,9 +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 := - 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 ⟨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 e024fbe9ac..641bbb9ad4 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/LabelExtraction.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/LabelExtraction.lean @@ -63,8 +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 input.1.1 input.1.2) (hash input.1.1 input.1.2) - input.2 >>= test input.1.1 input.1.2)) + (fun ((n, i), samples) => extractLabels (seed n i) (hash n i) + samples >>= test n i)) {candidates count densityBound : ℕ → ℕ} {numerator : ℕ → ℕ → ℕ} {slack : ℕ → ℝ} (hcandidates : ComputableInPolyTime candidates encUnary encUnary) (hcount : ComputableInPolyTime count encUnary encUnary) @@ -134,8 +134,9 @@ theorem HasGap.indexed_extracted_advantage_negligible {pair : SamplablePair} {ga refine ⟨2, Filter.eventually_map.mpr ?_⟩ filter_upwards [hmasks, hmass, hchoose, hvalid, (herror' degree).eventually_le_const (by norm_num : (0 : ℝ) < 1)] with - n hmask hmass hindex hn hsmall - obtain ⟨mask, hdense, hpositive, hdistinguish⟩ := hmask (choose n) hindex hn.1 hn.2.1 hn.2.2 + n hmask hmass hindex ⟨hnumPos, hnumLe, hnumRatio⟩ hsmall + obtain ⟨mask, hdense, hpositive, hdistinguish⟩ := + hmask (choose n) hindex hnumPos hnumLe hnumRatio have hclose := maskedSample_extract_dist_bind_le (pair.latentSample n) (fun value => pair.encode n value.1) Prod.snd mask (count n) (realization.length n + n + 2) (hmass mask (fun value _ => hpositive value)) (seed n (choose n)) (hash n (choose n)) @@ -178,8 +179,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 input.1.1 input.1.2) (hash input.1.1 input.1.2) - input.2 >>= test input.1.1 input.1.2)) + (fun ((n, i), samples) => extractLabels (seed n i) (hash n i) + samples >>= test n i)) (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..fcd1c2e63b 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/MatrixExtraction.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/MatrixExtraction.lean @@ -57,14 +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) : - result.1 = samples.map Prod.fst ∧ result.2.1.length = outputBits * inputBits ∧ - result.2.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 @@ -104,7 +110,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 => + (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 @@ -118,7 +126,8 @@ 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 => + (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] @@ -131,7 +140,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 - next result.1 (result.2.1 ++ result.2.2)) = + next result.1 (extractedSeed result ++ extractedDigest result)) = ProbComp.eval (do let observations ← OracleComp.replicate count source let bits ← BitString.sampleList (outputBits * inputBits + outputBits) @@ -147,7 +156,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) = + (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/Seed.lean b/Complexity/Crypto/Computational/Pseudoentropy/Seed.lean index 800fffd0a8..c82384af68 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/Seed.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/Seed.lean @@ -211,8 +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 => - ((pair.encode n result.1.1, result.1.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] diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Selection.lean b/Complexity/Crypto/Computational/Pseudoentropy/Selection.lean index 1fc8e8ad52..29704dfab7 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/Selection.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/Selection.lean @@ -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 ((n, i), word) => predict n i word)) {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..533506e1f8 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 ++ (middle.2.1 ++ middle.2.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 ++ (third.2.1 ++ third.2.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, sample.1.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,7 +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 - return front ++ (third.2.1 ++ third.2.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, @@ -413,7 +419,7 @@ theorem replace_indexed_labels {pair : SamplablePair} {gap : ℕ → ℝ} (hpair adversary n i (front ++ suffix) have htest : IsPPTOn (encPair (encPair encUnary encUnary) (encPair (encList encBits) (encPair encBits encBits))) - encBool (fun input => test input.1.1 input.1.2 input.2) := by + encBool (fun ((n, i), middle) => test n i middle) := by dsimp only [test] apply IsPPTOn.bind_with (left := encBits) (by fun_prop) apply IsPPTOn.bind_with (left := encBits) (by fun_prop) @@ -482,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 input.1.1 input.1.2 input.2)) : + encBool (fun ((n, i), word) => test n i word)) : 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..24dc247974 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Amplification.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Amplification.lean @@ -104,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 input.1.1 input.1.2 input.2) → + encBool (fun ((n, i), word) => test n i word) → 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..b2b0a8d4b8 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Candidates.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Candidates.lean @@ -185,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 input.1.1 input.1.2 input.2) → + encBool (fun ((n, i), word) => test n i word) → 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..444c9acb38 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Padding.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Padding.lean @@ -143,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 input.1.1 input.1.2 input.2) → + encBool (fun ((n, i), word) => test n i word) → 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..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 => sample.1.1)).map (padWord bound)).flatten - let labels := listRow count 0 (samples.map (fun sample => sample.1.2)) + 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,12 +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, sample.1.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 - return front ++ (third.2.1 ++ third.2.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 9eef8c06e2..ee6c1d0bbe 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/WordExtraction.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/WordExtraction.lean @@ -81,7 +81,8 @@ 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 => + (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. -/ @@ -89,7 +90,8 @@ 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 => + (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 @@ -109,7 +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 - test input.1 (result.1, List.ofFn result.2.1, List.ofFn result.2.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 >>= @@ -145,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 input.1.1 input.1.2 input.2)) : + encBool (fun ((n, i), result) => test n i result)) : 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/Stretch.lean b/Complexity/Crypto/Computational/Stretch.lean index c1065b21cb..acb98160fe 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 ((n, i), seed) => generator n i seed) (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 ((n, i), word) => adversary n i word) → 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 ((n, i), word) => adversary n i word) → Negligible (fun n => Game.advantage (((uniformList (seedBits n)).map (iterate (generator n (choose n)) (seedBits n) (count n))).bind diff --git a/Complexity/Crypto/Primitives/PRG/NisanWigderson/Sampling.lean b/Complexity/Crypto/Primitives/PRG/NisanWigderson/Sampling.lean index b6e9ef29b5..84233a5911 100644 --- a/Complexity/Crypto/Primitives/PRG/NisanWigderson/Sampling.lean +++ b/Complexity/Crypto/Primitives/PRG/NisanWigderson/Sampling.lean @@ -128,7 +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 := ⟨p.1, p.2.1, p.2.2.1, p.2.2.2⟩ + invFun := fun (pos, seed, bit, pad) => ⟨pos, seed, bit, pad⟩ instance [NeZero m] : Nonempty (Trial ℓ m) := ⟨⟨0, fun _ => false, false, fun _ => false⟩⟩ @@ -165,7 +165,8 @@ theorem trialAgreement_le_one (t : Trial ℓ m) : trialAgreement D f test t ≤ /-- Averaging over a uniform trial averages over its four random choices in turn. -/ private theorem expect_trial {M : Type*} [AddCommMonoid M] [Module ℚ≥0 M] (g : Trial ℓ m → M) : 𝔼 t, g t = 𝔼 i, 𝔼 w, 𝔼 r, 𝔼 u, g ⟨i, w, r, u⟩ := by - rw [Fintype.expect_equiv Trial.equivProd g (fun p => g ⟨p.1, p.2.1, p.2.2.1, p.2.2.2⟩) + rw [Fintype.expect_equiv Trial.equivProd g + (fun (pos, seed, bit, pad) => g ⟨pos, seed, bit, pad⟩) fun _ => rfl] simp only [Fintype.expect_prod_type]