diff --git a/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean b/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean index 1e8e433436..9107c3a495 100644 --- a/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean +++ b/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean @@ -102,6 +102,12 @@ noncomputable def configurationInstance (w : List Bool) : STCONInstance where (startID_lt_vertexBound ntm c w.length).trans (Nat.lt_succ_self _)⟩ t := ⟨vertexBound (k := k) (radix (radixExponent State c) w.length), Nat.lt_succ_self _⟩ +/-- The arcs of `configurationInstance` are those of `sinkAdj`. -/ +private theorem adj_configurationInstance (w : List Bool) + (u v : Fin (configurationInstance ntm c w).n) : + (configurationInstance ntm c w).adj u v = sinkAdj ntm (radixExponent State c) w u v := by + simp only [configurationInstance] + /-- Every path from the source to the sink in `configurationInstance` passes through an accepting halted vertex just before the sink. -/ private theorem exists_bad_of_mem_configurationInstance {w : List Bool} @@ -124,8 +130,7 @@ private theorem exists_bad_of_mem_configurationInstance {w : List Bool} induction hx with | refl => exact ⟨fun _ => .refl, fun h => absurd h (Nat.ne_of_lt hstart)⟩ | @tail y z _ hyz ih => - change sinkAdj ntm D w y z = true at hyz - unfold sinkAdj at hyz + rw [STCONInstance.Adj, adj_configurationInstance, sinkAdj] at hyz split_ifs at hyz with hz · have hy := (lt_vertexBound_of_edgeWithSymbol (ntm := ntm) hyz).1 exact ⟨fun _ => (ih.1 hy).tail hyz, fun h => absurd h (Nat.ne_of_lt hz)⟩ @@ -157,11 +162,11 @@ theorem configurationInstance_mem_iff {w : List Bool} obtain ⟨hy, hpath⟩ := ih have hz := (lt_vertexBound_of_edgeWithSymbol (ntm := ntm) hyz).2 refine ⟨hz.trans (Nat.lt_succ_self _), hpath.tail ?_⟩ - change sinkAdj ntm D w y z = true - rw [sinkAdj, ite_eq_left hz] + rw [STCONInstance.Adj, adj_configurationInstance, sinkAdj, ite_eq_left hz] exact hyz obtain ⟨hu', hpath⟩ := hlift u hu refine hpath.tail ?_ + rw [STCONInstance.Adj, adj_configurationInstance] change sinkAdj ntm D w u (vertexBound (k := k) (radix D w.length)) = true rw [sinkAdj, ite_eq_right (lt_irrefl _)] exact hbad @@ -201,8 +206,46 @@ noncomputable def writer : CounterProgram where halt []] registers := 4 +/-- The blocks of `writer`'s code, in order; `code_writer` shows that they flatten to it. -/ +private noncomputable def writerBlocks : List (List Instr) := + [[read (mul (const 2) (reg 0)) 1 2 2, + assign 0 (add (reg 0) (const 1)) 0], + forCode 2 1 (numVerticesExpr (k := k) D) 5 6, [emit true 4, emit false 7], + forCode 7 1 (startIDExpr ntm (radixExpr D (reg 0))) 10 11, [emit true 9, emit false 12], + forCode 12 1 (vertexBoundExpr k (radixExpr D (reg 0))) 15 16, [emit true 14, emit false 17], + forCode 17 1 (numVerticesExpr (k := k) D) 20 33, + forCode 20 2 (numVerticesExpr (k := k) D) 23 19, + [lt (reg 2) (vertexBoundExpr k (radixExpr D (reg 0))) 24 30], + readSymbolCode 24 3 29 (reg 0) (queryIndexExpr k (radixExpr D (reg 0)) (reg 1)), + [lt (const 0) (edgeExpr ntm (radixExpr D (reg 0)) (reg 0) (reg 1) (reg 2) (reg 3)) 31 32, + lt (const 0) (badExpr k State (radixExpr D (reg 0)) (reg 0) (reg 1)) 31 32, + emit true 22, + emit false 22, + halt []]] + variable {ntm D} (w : List Bool) {B : ℕ} +private theorem code_writer : (writer ntm D).code = (writerBlocks ntm D).flatten := by + simp only [writer, writerBlocks, List.flatten_cons, List.flatten_nil, List.append_nil, + List.append_assoc] + +/-- **The instruction at label `c`**, read from the blocks of `writer`. Reduction finds a label +quickly in their flattening, but takes exponentially many steps in the left-nested appends that +define `writer`. -/ +private theorem instr_writer (c : ℕ) {i : Instr} + (h : (writerBlocks ntm D).flatten.getD c (halt []) = i) : (writer ntm D).instr c = i := by + rw [instr, code_writer, h] + +/-- A `forCode` block in `writer` is at `b` when instructions `b`, `b + 1`, `b + 2` match. -/ +private theorem codeAt_forCode {b u body exit : ℕ} {bound : Expr} + (h₀ : (writerBlocks ntm D).flatten.getD b (halt []) = .assign u (const 0) (b + 1)) + (h₁ : (writerBlocks ntm D).flatten.getD (b + 1) (halt []) = .lt (reg u) bound body exit) + (h₂ : (writerBlocks ntm D).flatten.getD (b + 2) (halt []) = + .assign u (add (reg u) (const 1)) (b + 1)) : + (writer ntm D).CodeAt b (forCode b u bound body exit) := by + simp only [forCode, codeAt_cons, codeAt_nil, and_true] + exact ⟨instr_writer _ h₀, instr_writer _ h₁, instr_writer _ h₂⟩ + private theorem flatMap_range_true (M : ℕ) : (List.range M).flatMap (fun _ => [true]) = List.replicate M true := by induction M with @@ -224,17 +267,17 @@ private theorem reachesOut_count (hL : w.length ≤ B) : ∀ j ≤ w.length, | zero => have : j = w.length := by omega subst this - refine ReachesOut.read (show (writer ntm D).instr 0 = _ from rfl) + refine ReachesOut.read (instr_writer 0 rfl) (bounded_regs hL (by omega) (by omega) (by omega)) ?_ simp only [eval_mul, eval_const, eval_reg, List.getD_cons_zero, getElem?_frame_two_mul_length, readLabel] exact ReachesOut.refl _ | succ m ih => - refine ReachesOut.read (show (writer ntm D).instr 0 = _ from rfl) + refine ReachesOut.read (instr_writer 0 rfl) (bounded_regs (by omega) (by omega) (by omega) (by omega)) ?_ simp only [eval_mul, eval_const, eval_reg, List.getD_cons_zero, getElem?_frame_two_mul (show j < w.length by omega), readLabel] - refine ReachesOut.assign (show (writer ntm D).instr 1 = _ from rfl) + refine ReachesOut.assign (instr_writer 1 rfl) (bounded_regs (by omega) (by omega) (by omega) (by omega)) ?_ simpa using ih (j + 1) (by omega) (by omega) @@ -272,8 +315,8 @@ private theorem reachesOut_bit {l : ℕ} {e : Expr} {regs : List ℕ} {b : Bool} refine ReachesOut.lt hl hB ?_ rw [eval_const, he] cases b - · exact ReachesOut.emit (show (writer ntm D).instr 32 = _ from rfl) hB (ReachesOut.refl _) - · exact ReachesOut.emit (show (writer ntm D).instr 31 = _ from rfl) hB (ReachesOut.refl _) + · exact ReachesOut.emit (instr_writer 32 rfl) hB (ReachesOut.refl _) + · exact ReachesOut.emit (instr_writer 31 rfl) hB (ReachesOut.refl _) private theorem flatMap_singleton_eq_map {β : Type} (l : List ℕ) (f : ℕ → β) : l.flatMap (fun x => [f x]) = l.map f := by @@ -293,7 +336,8 @@ private theorem reachesOut_entry_symbol (hL : w.length ≤ B) have hcode : (writer ntm D).CodeAt 24 (readSymbolCode 24 3 29 (reg 0) (queryIndexExpr k (radixExpr D (reg 0)) (reg 1))) := by simp only [readSymbolCode, codeAt_cons, codeAt_nil, and_true] - exact ⟨rfl, rfl, rfl, rfl, rfl⟩ + exact ⟨instr_writer _ rfl, instr_writer _ rfl, instr_writer _ rfl, instr_writer _ rfl, + instr_writer _ rfl⟩ refine ⟨_, Nat.le_of_lt_succ (symbolCode_lt _), rfl, ?_⟩ simpa using reachesOut_readSymbolCode (w := w) hcode (by simp) hB @@ -312,18 +356,18 @@ private theorem reachesOut_entry (hL : w.length ≤ B) · obtain ⟨y', hy', hsym, hreach⟩ := reachesOut_entry_symbol (ntm := ntm) (D := D) w hL hN h2 hu hv hy refine ⟨y', hy', ?_⟩ - refine ReachesOut.lt (show (writer ntm D).instr 23 = _ from rfl) (hB hy) ?_ + refine ReachesOut.lt (instr_writer 23 rfl) (hB hy) ?_ simp only [eval_reg, eval_vertexBoundExpr, eval_radixExpr, List.getD_cons_zero, List.getD_cons_succ, hvb, ↓reduceIte] - refine (hreach.trans (reachesOut_bit w (show (writer ntm D).instr 29 = _ from rfl) + refine (hreach.trans (reachesOut_bit w (instr_writer 29 rfl) (eval_edgeExpr ntm (symbol := w[queryIndex (k := k) (radix D w.length) u]?) (by simp [hsym])) (hB hy'))).of_eq ?_ simp [sinkAdj, hvb] · refine ⟨y, hy, ?_⟩ - refine ReachesOut.lt (show (writer ntm D).instr 23 = _ from rfl) (hB hy) ?_ + refine ReachesOut.lt (instr_writer 23 rfl) (hB hy) ?_ simp only [eval_reg, eval_vertexBoundExpr, eval_radixExpr, List.getD_cons_zero, List.getD_cons_succ, hvb, ↓reduceIte] - refine (reachesOut_bit w (show (writer ntm D).instr 30 = _ from rfl) eval_badExpr + refine (reachesOut_bit w (instr_writer 30 rfl) eval_badExpr (hB hy)).of_eq ?_ simp [sinkAdj, hvb] @@ -336,9 +380,8 @@ private theorem reachesOut_row (hL : w.length ≤ B) ∃ y' ≤ 2, (writer ntm D).ReachesOut (frame w) ((writer ntm D).Active B) (20, [w.length, u, x, y]) (19, [w.length, u, vertexBound (k := k) (radix D w.length) + 1, y']) ((List.range (vertexBound (k := k) (radix D w.length) + 1)).map (sinkAdj ntm D w u)) := by - have hcode : (writer ntm D).CodeAt 20 (forCode 20 2 (numVerticesExpr (k := k) D) 23 19) := by - simp only [forCode, codeAt_cons, codeAt_nil, and_true] - exact ⟨rfl, rfl, rfl⟩ + have hcode : (writer ntm D).CodeAt 20 (forCode 20 2 (numVerticesExpr (k := k) D) 23 19) := + codeAt_forCode rfl rfl rfl obtain ⟨regs', hreach, y', rfl, -, hy'⟩ := reachesOut_forCode (w := frame w) (o := fun v => [sinkAdj ntm D w u v]) (N := vertexBound (k := k) (radix D w.length) + 1) hcode (fun v regs => ∃ y, regs = [w.length, u, v, y] ∧ @@ -365,9 +408,8 @@ private theorem reachesOut_matrix (hL : w.length ≤ B) ((List.range (vertexBound (k := k) (radix D w.length) + 1)).flatMap fun u => (List.range (vertexBound (k := k) (radix D w.length) + 1)).map (sinkAdj ntm D w u)) ∧ ∀ r ∈ regs, r ≤ B := by - have hcode : (writer ntm D).CodeAt 17 (forCode 17 1 (numVerticesExpr (k := k) D) 20 33) := by - simp only [forCode, codeAt_cons, codeAt_nil, and_true] - exact ⟨rfl, rfl, rfl⟩ + have hcode : (writer ntm D).CodeAt 17 (forCode 17 1 (numVerticesExpr (k := k) D) 20 33) := + codeAt_forCode rfl rfl rfl obtain ⟨regs', hreach, x, y, rfl, -, hx, hy⟩ := reachesOut_forCode (w := frame w) (o := fun u => (List.range (vertexBound (k := k) (radix D w.length) + 1)).map (sinkAdj ntm D w u)) @@ -389,15 +431,6 @@ private theorem reachesOut_matrix (hL : w.length ≤ B) exact ⟨_, hreach, bounded_regs hL (by omega) (by omega) (by omega)⟩ -/-- A `forCode` block in `writer` is at `b` when instructions `b`, `b + 1`, `b + 2` match. -/ -private theorem codeAt_forCode {b u body exit : ℕ} {bound : Expr} - (h₀ : (writer ntm D).instr b = .assign u (const 0) (b + 1)) - (h₁ : (writer ntm D).instr (b + 1) = .lt (reg u) bound body exit) - (h₂ : (writer ntm D).instr (b + 2) = .assign u (add (reg u) (const 1)) (b + 1)) : - (writer ntm D).CodeAt b (forCode b u bound body exit) := by - simp only [forCode, codeAt_cons, codeAt_nil, and_true] - exact ⟨h₀, h₁, h₂⟩ - variable (ntm) in /-- **The instance is computed in logarithmic space** from the framed input. -/ theorem computableInLogSpace_configurationInstance : @@ -415,27 +448,27 @@ theorem computableInLogSpace_configurationInstance : bounded_regs hL hi (by omega) (by omega) have hones₁ := reachesOut_ones (ntm := ntm) (D := D) w (codeAt_forCode rfl rfl rfl) - (show (writer ntm D).instr 5 = _ from rfl) (M := VB + 1) (fun _ => by simp [VB]) hN hL + (instr_writer 5 rfl) (M := VB + 1) (fun _ => by simp [VB]) hN hL (i₀ := 0) (by omega) have hones₂ := reachesOut_ones (ntm := ntm) (D := D) w (codeAt_forCode rfl rfl rfl) - (show (writer ntm D).instr 10 = _ from rfl) (M := S) (fun _ => by simp [S]) (by omega) hL + (instr_writer 10 rfl) (M := S) (fun _ => by simp [S]) (by omega) hL (i₀ := VB + 1) hN have hones₃ := reachesOut_ones (ntm := ntm) (D := D) w (codeAt_forCode rfl rfl rfl) - (show (writer ntm D).instr 15 = _ from rfl) (M := VB) (fun _ => by simp [VB]) (by omega) hL + (instr_writer 15 rfl) (M := VB) (fun _ => by simp [VB]) (by omega) hL (i₀ := S) (by omega) obtain ⟨regs, hmat, hregs⟩ := reachesOut_matrix (ntm := ntm) (D := D) w hL hN h2 (i₀ := VB) (by omega) have hchain := (reachesOut_count (ntm := ntm) (D := D) w hL 0 (Nat.zero_le _)).trans - (hones₁.trans (ReachesOut.emit (show (writer ntm D).instr 6 = _ from rfl) + (hones₁.trans (ReachesOut.emit (instr_writer 6 rfl) (hreg _ (by omega)) (hones₂.trans (ReachesOut.emit - (show (writer ntm D).instr 11 = _ from rfl) (hreg _ (by omega)) - (hones₃.trans (ReachesOut.emit (show (writer ntm D).instr 16 = _ from rfl) + (instr_writer 11 rfl) (hreg _ (by omega)) + (hones₃.trans (ReachesOut.emit (instr_writer 16 rfl) (hreg _ (by omega)) hmat)))))) - refine ⟨(33, regs), _, [], hchain, rfl, ?_, hregs⟩ + refine ⟨(33, regs), _, [], hchain, instr_writer 33 rfl, ?_, hregs⟩ rw [encSTCON_apply, STCONInstance.encode, - STCONInstance.matrix_eq_flatMap _ (sinkAdj ntm D w) fun _ _ => rfl] + STCONInstance.matrix_eq_flatMap _ (sinkAdj ntm D w) (adj_configurationInstance ntm c w)] simp [configurationInstance, VB, S, D] diff --git a/Complexity/Crypto/Computational/OneWay/CondEPPRG.lean b/Complexity/Crypto/Computational/OneWay/CondEPPRG.lean index 6b28357072..d226d9a5de 100644 --- a/Complexity/Crypto/Computational/OneWay/CondEPPRG.lean +++ b/Complexity/Crypto/Computational/OneWay/CondEPPRG.lean @@ -469,8 +469,8 @@ theorem eventually_regularity_gap {g : List Bool → List Bool} (hg : OneWay g) have hpow_le : (2 : ℝ) ^ ((r k).val + D * Nat.log 2 k) ≤ (2 : ℝ) ^ k := by have hpos : (0 : ℝ) < k + 1 := by positivity have h1 : (2 : ℝ) ^ (r k).val * (k + 1 : ℝ) ^ D ≤ (2 : ℝ) ^ k := by - rw [hpow_D] at hcross - nlinarith + rw [hpow_D, mul_left_comm] at hcross + exact le_of_mul_le_mul_left hcross hpos calc (2 : ℝ) ^ ((r k).val + D * Nat.log 2 k) = (2 : ℝ) ^ (r k).val * ((2 : ℝ) ^ (Nat.log 2 k)) ^ D := by @@ -837,7 +837,9 @@ private theorem ofFn_packSeedEmb {imgLen : ℕ → ℕ} {d γ_core k n r : ℕ} (hr : r ≤ k) (hfits : coreSeedLen imgLen d γ_core k ≤ n) (t : SeedTuple imgLen d γ_core k n) : List.ofFn (packSeedEmb hr hfits t) = packSeedWords r t := - ofFn_ofList (length_packSeedWords hr hfits t) + -- Unfold the embedding first: unifying it with `ofList` directly takes seconds. + (congrArg List.ofFn (congrFun (Function.Embedding.coeFn_mk _ _) t)).trans + (ofFn_ofList (length_packSeedWords hr hfits t)) /-- Evaluating `rawGen` on a packed seed recovers the exact concatenation of `pad`, `h1`, `wordHash l1 h1 (g x)`, `h2`, and `wordHash (l2 + mActual) h2 x`. -/ @@ -994,7 +996,7 @@ private theorem dist_seededHash_regularityBucket_fiber_le {k m2 c2 : ℕ} {Image intro side source seed2 hash2 split_ifs with hm2_zero · subst m2 - have hsub : Subsingleton (BitString 0) := inferInstanceAs (Subsingleton (Fin 0 → Bool)) + have hsub : Subsingleton (BitString 0) := ⟨fun _ _ => funext fun i => i.elim0⟩ have heq : (side.bind fun x₀ => (seededHash seed2 (source x₀) hash2).map (x₀, ·)) = (side.bind fun x₀ => (seed2.bind fun h2 => (PMF.uniformOfFintype (BitString 0)).map (h2, ·)).map (x₀, ·)) := by @@ -1523,8 +1525,17 @@ private theorem computableTidilyInPolyTime_wordStepPredictor {α : Type} {encode (fun a => wordStepPredictor evaluate (n a) (k a) (m1 a) (idx a) (pad a) (h1 a) (image a) (h2 a) (digest a) (r_word a) (pol_word a) (z_tail a) (coins a) (query a)) encode encBool := by - unfold wordStepPredictor - fun_prop + -- `fun_prop` takes seconds to find this composition through the case split. + have heval : ComputableTidilyInPolyTime + (fun a => evaluate (n a, wordChallenge (k a) (m1 a) (idx a) (pad a) (h1 a) (image a) (h2 a) + (digest a) (r_word a) (z_tail a) (query a)) (coins a)) encode encBool := + hevaluate.comp' ((hn.prod (computableTidilyInPolyTime_wordChallenge hk hm1 hidx hpad hh1 + himage hh2 hdigest hr_word hz_tail hquery)).prod hcoins) + have hr_bit : ComputableTidilyInPolyTime (fun a => (r_word a).headD false) encode encBool := + (ComputableTidilyInPolyTime.headD false).comp' hr_word + exact ComputableTidilyInPolyTime.bool_xor.comp' + ((heval.ite' hr_bit (ComputableTidilyInPolyTime.bool_not.comp' hr_bit)).prod + ((ComputableTidilyInPolyTime.headD (encA := encBool) false).comp' hpol_word)) /-- Coin budget for the PRG distinguisher on an output of length `n + γ * Nat.log 2 n` at security parameter `n`. -/ @@ -1959,10 +1970,9 @@ private theorem fiber_step_diff_le {k imgLen_k : ℕ} · refine Finset.sum_congr rfl fun rows _ => ?_ rw [PMF.bind_apply_toReal, PMF.bind_apply_toReal] rw [← mul_sub, ← Finset.sum_sub_distrib, ← mul_assoc, mul_comm 2, mul_assoc, Finset.mul_sum] - congr 1 - refine Finset.sum_congr rfl fun x _ => ?_ + refine congrArg (_ * ·) (Finset.sum_congr rfl fun x _ => ?_) rw [← mul_sub, ← mul_assoc, mul_comm 2, mul_assoc] - congr 1 + refine congrArg (_ * ·) ?_ simp_rw [← hpred_eq _ rows x.val] exact (sum_bool_agreement_eq (evalBit rows x.val) x.val).symm · exact sum_mul_sum_mul_sum_comm _ _ _ _ @@ -2135,7 +2145,8 @@ private theorem fiberHybrid_step_le (g : List Bool → List Bool) (imgLen : ℕ (PMF.uniformOfFintype Aux).bind p_succ := by unfold fiberHybridAcceptDist rw [uniformList_four_bind_eq] - congr 1; funext a; congr 1; funext rows; congr 1; funext x + refine congrArg (PMF.bind _) (funext fun a => ?_) + congr 1; funext rows; congr 1; funext x simp only [h2Word, digestWord, m1, m2, idx, ofFn_hash_castLE_succ rows x.val hlen hidx_lt, List.append_assoc] have hcurr_eq : @@ -2157,7 +2168,8 @@ private theorem fiberHybrid_step_le (g : List Bool → List Bool) (imgLen : ℕ arg 2; ext pad; arg 2; ext h1 rw [bind_map_comm_four] rw [uniformList_four_bind_eq] - congr 1; funext a; congr 1; funext rows; congr 1; funext x; congr 1; funext b + refine congrArg (PMF.bind _) (funext fun a => ?_) + congr 1; funext rows; congr 1; funext x; congr 1; funext b simp only [h2Word, digestWord, m1, List.append_assoc, Function.comp_def] let invProb (a : Aux) (r_bit p : Bool) : PMF Bool := (Pseudoentropy.guessInverter f @@ -3140,7 +3152,7 @@ private theorem eventually_coreSeedLen_succ_le_pow {imgLen : ℕ → ℕ} {c_i d have hh2 : h2Rows d γ_core (k + 1) ≤ 2 * k ^ 2 := by have hm : mMax d γ_core (k + 1) ≤ (2 * d + γ_core + 2) * (k + 1) := by unfold mMax - nlinarith + linarith [Nat.mul_le_mul_left d hlog, Nat.mul_le_mul_left γ_core hlog] have hh : h2Rows d γ_core (k + 1) ≤ (2 * d + γ_core + 3) * (k + 1) := by unfold h2Rows linarith @@ -3158,8 +3170,10 @@ private theorem eventually_coreSeedLen_succ_le_pow {imgLen : ℕ → ℕ} {c_i d have hpow_le3 : k ^ 3 ≤ k ^ (d_i + 3) := Nat.pow_le_pow_right (by omega) (by omega) have hreg : regWidth (k + 1) + (k + 1) ≤ 2 * k ^ (d_i + 3) := by + have hk_sq : 8 * k ≤ k ^ 2 := by rw [sq]; exact Nat.mul_le_mul_right k hk8 + have hpow_le_sq : k ^ 2 ≤ k ^ (d_i + 3) := Nat.pow_le_pow_right (by omega) (by omega) unfold regWidth - nlinarith + omega calc coreSeedLen imgLen d γ_core (k + 1) = (regWidth (k + 1) + (k + 1)) + (k + 1) * imgLen (k + 1) + @@ -3178,8 +3192,9 @@ private theorem sqrt_lhl_err_le {E δ k n : ℕ} (hk : 8 ≤ k) (hn_pos : 1 ≤ set B := E * (2 * δ + 4) + 4 have hpow2 : k ^ B ≤ 2 ^ (d * Nat.log 2 k) := by simpa [d, mul_assoc] using pow_le_two_pow_two_mul_log B (by omega : 2 ≤ k) - have hk1 : 2 * (k + 1) ≤ k ^ 2 := by nlinarith - have hk16 : 16 ≤ k ^ 2 := by nlinarith + have hk_sq : 8 * k ≤ k ^ 2 := by rw [sq]; exact Nat.mul_le_mul_right k hk + have hk1 : 2 * (k + 1) ≤ k ^ 2 := by omega + have hk16 : 16 ≤ k ^ 2 := by omega have hn_pow : n ^ (2 * δ + 4) ≤ k ^ (E * (2 * δ + 4)) := (Nat.pow_le_pow_left hn (2 * δ + 4)).trans_eq (pow_mul k E (2 * δ + 4)).symm have hnat : 2 * (k + 1) * (16 * n ^ (2 * δ + 4)) ≤ 2 ^ (d * Nat.log 2 k) := by @@ -3211,7 +3226,7 @@ private theorem gl_err_le {E δ k n m : ℕ} (hk : 8 ≤ k) (hn_pos : 1 ≤ n) ( (m : ℝ) / (2 * (GoldreichLevin.precision deg k : ℝ)) ≤ 1 / (4 * (n : ℝ) ^ δ) := by intro deg have hn_rpos : (0 : ℝ) < n := Nat.cast_pos.mpr hn_pos - have h4 : 4 ≤ k ^ 2 := by nlinarith + have h4 : 4 ≤ k ^ 2 := (by omega : 4 ≤ k).trans (Nat.le_self_pow two_ne_zero k) have hn_pow : n ^ (δ + 2) ≤ k ^ (E * (δ + 2)) := (Nat.pow_le_pow_left hn (δ + 2)).trans_eq (pow_mul k E (δ + 2)).symm have hnat : 4 * n ^ δ * m ≤ 2 * GoldreichLevin.precision deg k := by @@ -3258,11 +3273,12 @@ private theorem inv_term_le {E δ d γ_core k n m cs_succ : ℕ} {succProb : ℝ _ = k ^ (2 * d + γ_core + 2) := (pow_succ' k (2 * d + γ_core + 1)).symm have h2 : dyadicSize m ≤ k ^ 3 := by have hm_k2 : m + 1 ≤ 2 * k ^ 2 := by - have hm_le_k : m + 1 ≤ (2 * d + γ_core + 2) * k := by nlinarith + have hm_le_k : m + 1 ≤ (2 * d + γ_core + 2) * k := by + linarith [Nat.mul_le_mul_left (2 * d + γ_core + 1) hlog_k] calc m + 1 ≤ (2 * d + γ_core + 2) * k := hm_le_k _ ≤ k * k := Nat.mul_le_mul_right k (by omega) - _ ≤ 2 * k ^ 2 := by nlinarith + _ ≤ 2 * k ^ 2 := by rw [sq]; omega calc dyadicSize m ≤ 2 * (m + 1) := dyadicSize_le m _ ≤ 4 * k ^ 2 := by omega @@ -3275,10 +3291,11 @@ private theorem inv_term_le {E δ d γ_core k n m cs_succ : ℕ} {succProb : ℝ _ ≤ 4 * k ^ E := by omega _ ≤ k * k ^ E := Nat.mul_le_mul_right _ (by omega) _ = k ^ (E + 1) := (pow_succ' k E).symm + have hk_sq : 8 * k ≤ k ^ 2 := by rw [sq]; exact Nat.mul_le_mul_right k hk8 have h4 : dyadicSize (k + 1) ≤ k ^ 2 := by have := dyadicSize_le (k + 1) - nlinarith - have h5 : 4 * (k + 1) ≤ k ^ 2 := by nlinarith + omega + have h5 : 4 * (k + 1) ≤ k ^ 2 := by omega have h6 : n ^ δ ≤ k ^ (E * δ) := (Nat.pow_le_pow_left hn δ).trans_eq (pow_mul k E δ).symm have hprod_nat : @@ -3388,10 +3405,8 @@ theorem OneWay.exists_condEPPRG {f : List Bool → List Bool} (hf : OneWay f) ( have hn_pos : 1 ≤ n := by omega have hlog_le : Nat.log 2 n ≤ 2 * E * Nat.log 2 k := log_le_two_mul_log_of_le_pow (by omega : 2 ≤ k) hn_le_pow - have hm_le_mMax : mActual d γ k n ≤ mMax d γ_core k := by - apply mActual_le_mMax - dsimp [γ_core] - nlinarith + have hm_le_mMax : mActual d γ k n ≤ mMax d γ_core k := + mActual_le_mMax ((Nat.mul_le_mul_left γ hlog_le).trans_eq (Nat.mul_assoc _ _ _).symm) have hm_le : l2Val d k (r k).val + mActual d γ k n ≤ h2Rows d γ_core k := by have := l2Val_le d k (r k).val unfold h2Rows @@ -3403,7 +3418,7 @@ theorem OneWay.exists_condEPPRG {f : List Bool → List Bool} (hf : OneWay f) ( have h2 : Nat.log 2 n ≤ n := Nat.log_le_self 2 n have h3 : mActual d γ k n ≤ (γ + 1) * n := by unfold mActual - nlinarith + linarith [Nat.mul_le_mul_left γ h2] have h4 : (γ + 1) * n ≤ n * n := Nat.mul_le_mul_right n (by omega) calc mActual d γ k n ≤ (γ + 1) * n := h3 @@ -3478,7 +3493,7 @@ theorem OneWay.exists_condEPPRG {f : List Bool → List Bool} (hf : OneWay f) ( have hn_pos : 1 ≤ n := by omega have hcs_def : coreSeedLen imgLen d γ_core k = (Nat.log 2 k + 1) + k + k * imgLen k + h2Rows d γ_core k * k := rfl - have hh2_pos : 1 ≤ h2Rows d γ_core k * k := by unfold h2Rows; nlinarith + have hh2_pos : 1 ≤ h2Rows d γ_core k * k := Nat.mul_pos (by unfold h2Rows; omega) (by omega) have hlhl_pos : 1 ≤ lhlPrefixLen d k n := by unfold lhlPrefixLen omega @@ -3520,7 +3535,7 @@ theorem OneWay.exists_condEPPRG {f : List Bool → List Bool} (hf : OneWay f) ( have hlog_n1_r : (1 : ℝ) ≤ (Nat.log 2 n : ℝ) := by exact_mod_cast hlog_n1 have hα_def : (α : ℝ) = 2 * (d : ℝ) + 4 := by dsimp [α]; push_cast; ring rw [hα_def] - nlinarith + linarith [mul_le_mul_of_nonneg_left hlog_kn_r (Nat.cast_nonneg (α := ℝ) d)] exact hloss_le.trans hent end Cslib.Crypto