import ContractExact namespace FastAct @[inline] def midW (a b : UInt64) : UInt64 := (((a &&& (0xffffffff : UInt64)) * (b &&& (0xffffffff : UInt64))) >>> (32 : UInt64)) + (((a &&& (0xffffffff : UInt64)) * (b >>> (32 : UInt64))) &&& (0xffffffff : UInt64)) + (((a >>> (32 : UInt64)) * (b &&& (0xffffffff : UInt64))) &&& (0xffffffff : UInt64)) @[inline] def mulHiW (a b : UInt64) : UInt64 := (a >>> (32 : UInt64)) * (b >>> (32 : UInt64)) + (((a &&& (0xffffffff : UInt64)) * (b >>> (32 : UInt64))) >>> (32 : UInt64)) + (((a >>> (32 : UInt64)) * (b &&& (0xffffffff : UInt64))) >>> (32 : UInt64)) + (midW a b >>> (32 : UInt64)) @[inline] def mulLoW (a b : UInt64) : UInt64 := (midW a b <<< (32 : UInt64)) + ((a &&& (0xffffffff : UInt64)) * (b &&& (0xffffffff : UInt64)) &&& (0xffffffff : UInt64)) def mul128 (a b : UInt64) : UInt64 × UInt64 := (mulHiW a b, mulLoW a b) theorem toNat_and_mask (x : UInt64) : (x &&& 0xffffffff).toNat = x.toNat % 2 ^ 32 := by rw [UInt64.toNat_and] exact Nat.and_two_pow_sub_one_eq_mod x.toNat 32 theorem toNat_shr32 (x : UInt64) : (x >>> 32).toNat = x.toNat / 2 ^ 32 := by rw [UInt64.toNat_shiftRight] simp [Nat.shiftRight_eq_div_pow] theorem mul128_spec (a b : UInt64) : (mul128 a b).1.toNat * 2 ^ 64 + (mul128 a b).2.toNat = a.toNat * b.toNat := by have ha := a.toNat_lt have hb := b.toNat_lt have hk : a.toNat * b.toNat < 2 ^ 128 := calc a.toNat * b.toNat < 2 ^ 64 * 2 ^ 64 := Nat.mul_lt_mul'' ha hb _ = 2 ^ 128 := by norm_num simp only [mul128, mulHiW, mulLoW, midW, UInt64.toNat_add, UInt64.toNat_mul, UInt64.toNat_shiftLeft, toNat_and_mask, toNat_shr32] have h32 : (32 : UInt64).toNat % 64 = 32 := by decide rw [h32, Nat.shiftLeft_eq] have hA := (Nat.div_add_mod' a.toNat (2 ^ 32)).symm have hB := (Nat.div_add_mod' b.toNat (2 ^ 32)).symm have hA0 : a.toNat % 2 ^ 32 < 2 ^ 32 := Nat.mod_lt _ (by norm_num) have hB0 : b.toNat % 2 ^ 32 < 2 ^ 32 := Nat.mod_lt _ (by norm_num) have hA1 : a.toNat / 2 ^ 32 < 2 ^ 32 := by omega have hB1 : b.toNat / 2 ^ 32 < 2 ^ 32 := by omega generalize a.toNat / 2 ^ 32 = A1 at * generalize a.toNat % 2 ^ 32 = A0 at * generalize b.toNat / 2 ^ 32 = B1 at * generalize b.toNat % 2 ^ 32 = B0 at * have prod_lt : ∀ x y : Nat, x < 2 ^ 32 → y < 2 ^ 32 → x * y < 2 ^ 64 := fun x y hx hy => calc x * y < 2 ^ 32 * 2 ^ 32 := Nat.mul_lt_mul'' hx hy _ = 2 ^ 64 := by norm_num have m00 := prod_lt A0 B0 hA0 hB0 have m01 := prod_lt A0 B1 hA0 hB1 have m10 := prod_lt A1 B0 hA1 hB0 have m11 := prod_lt A1 B1 hA1 hB1 have hab : a.toNat * b.toNat = A1 * B1 * 2 ^ 64 + (A0 * B1 + A1 * B0) * 2 ^ 32 + A0 * B0 := by rw [hA, hB]; ring simp only [Nat.mod_eq_of_lt m00, Nat.mod_eq_of_lt m01, Nat.mod_eq_of_lt m10, Nat.mod_eq_of_lt m11] rw [hab] generalize A0 * B0 = p00 at * generalize A0 * B1 = p01 at * generalize A1 * B0 = p10 at * generalize A1 * B1 = p11 at * omega def one : Nat := 2 ^ 62 noncomputable def V (a : Nat) : ℝ := (a : ℝ) / 2 ^ 62 theorem V_nonneg (a : Nat) : 0 ≤ V a := by unfold V; positivity theorem V_one : V one = 1 := by norm_num [V, one] theorem V_mono {a b : Nat} (h : a ≤ b) : V a ≤ V b := by unfold V; gcongr theorem V_add (a b : Nat) : V (a + b) = V a + V b := by unfold V; push_cast; ring theorem V_sub_ge (a b : Nat) : V a - V b ≤ V (a - b) := by unfold V rcases le_total b a with h | h · rw [Nat.cast_sub h]; ring_nf; rfl · rw [Nat.sub_eq_zero_of_le h] have : (a : ℝ) ≤ b := by exact_mod_cast h simp only [Nat.cast_zero, zero_div] rw [div_sub_div_same] exact div_nonpos_of_nonpos_of_nonneg (by linarith) (by positivity) theorem V_sub_le_of_le {a b : Nat} (h : b ≤ a) : V (a - b) = V a - V b := by unfold V; rw [Nat.cast_sub h]; ring @[inline] def mulDnW (a b : UInt64) : UInt64 := (mulHiW a b <<< 2) + (mulLoW a b >>> 62) @[inline] def mulUpW (a b : UInt64) : UInt64 := if mulLoW a b &&& 0x3fffffffffffffff = 0 then mulDnW a b else mulDnW a b + 1 @[inline] def mulDn (a b : Nat) : Nat := (mulDnW a.toUInt64 b.toUInt64).toNat @[inline] def mulUp (a b : Nat) : Nat := (mulUpW a.toUInt64 b.toUInt64).toNat theorem toNat_toUInt64_le (a : Nat) : a.toUInt64.toNat ≤ a := by rw [UInt64.toNat_ofNat']; exact Nat.mod_le _ _ theorem toNat_toUInt64_of_lt {a : Nat} (h : a < 2 ^ 64) : a.toUInt64.toNat = a := by rw [UInt64.toNat_ofNat']; exact Nat.mod_eq_of_lt h theorem toNat_mulDnW (a b : UInt64) : (mulDnW a b).toNat = ((mulHiW a b).toNat * 4 % 2 ^ 64 + (mulLoW a b).toNat / 2 ^ 62) % 2 ^ 64 := by unfold mulDnW rw [UInt64.toNat_add, UInt64.toNat_shiftLeft, UInt64.toNat_shiftRight] have h2 : (2 : UInt64).toNat % 64 = 2 := by decide have h62 : (62 : UInt64).toNat % 64 = 62 := by decide rw [h2, h62, Nat.shiftLeft_eq, Nat.shiftRight_eq_div_pow] theorem low62_zero_iff (x : UInt64) : (x &&& 0x3fffffffffffffff = 0) ↔ x.toNat % 2 ^ 62 = 0 := by rw [← UInt64.toNat_inj, UInt64.toNat_and] have : (0x3fffffffffffffff : UInt64).toNat = 2 ^ 62 - 1 := by decide rw [this, Nat.and_two_pow_sub_one_eq_mod]; simp theorem halves {a b : Nat} (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) : (mulHiW a.toUInt64 b.toUInt64).toNat * 2 ^ 64 + (mulLoW a.toUInt64 b.toUInt64).toNat = a * b := by have hs := mul128_spec a.toUInt64 b.toUInt64 rwa [toNat_toUInt64_of_lt ha, toNat_toUInt64_of_lt hb] at hs theorem mulDn_mul_le (a b : Nat) : mulDn a b * 2 ^ 62 ≤ a * b := by have hs := mul128_spec a.toUInt64 b.toUInt64 have hle : a.toUInt64.toNat * b.toUInt64.toNat ≤ a * b := Nat.mul_le_mul (toNat_toUInt64_le a) (toNat_toUInt64_le b) simp only [mul128] at hs unfold mulDn rw [toNat_mulDnW] generalize (mulHiW a.toUInt64 b.toUInt64).toNat = h at * generalize (mulLoW a.toUInt64 b.toUInt64).toNat = l at * omega theorem mulUp_bounds {a b : Nat} (ha : a ≤ one) (hb : b ≤ one) : a * b ≤ mulUp a b * 2 ^ 62 ∧ mulUp a b * 2 ^ 62 < a * b + 2 ^ 62 := by have hs := halves (a := a) (b := b) (by unfold one at ha; omega) (by unfold one at hb; omega) have hab : a * b ≤ 2 ^ 62 * 2 ^ 62 := Nat.mul_le_mul ha hb have hl := (mulLoW a.toUInt64 b.toUInt64).toNat_lt unfold mulUp mulUpW split · rename_i h rw [low62_zero_iff] at h rw [toNat_mulDnW] generalize a * b = p at * generalize (mulHiW a.toUInt64 b.toUInt64).toNat = hi at * generalize (mulLoW a.toUInt64 b.toUInt64).toNat = l at * omega · rename_i h rw [low62_zero_iff] at h rw [UInt64.toNat_add, toNat_mulDnW, show (1 : UInt64).toNat = 1 from rfl] generalize a * b = p at * generalize (mulHiW a.toUInt64 b.toUInt64).toNat = hi at * generalize (mulLoW a.toUInt64 b.toUInt64).toNat = l at * omega theorem mulUp_mul_ge {a b : Nat} (ha : a ≤ one) (hb : b ≤ one) : a * b ≤ mulUp a b * 2 ^ 62 := (mulUp_bounds ha hb).1 theorem mulUp_le {a b : Nat} (ha : a ≤ one) (hb : b ≤ one) : mulUp a b ≤ one := by have h := (mulUp_bounds ha hb).2 have hab : a * b ≤ 2 ^ 62 * 2 ^ 62 := Nat.mul_le_mul ha hb unfold one at * generalize a * b = p at * omega theorem V_mulDn (a b : Nat) : V (mulDn a b) ≤ V a * V b := by have h := mulDn_mul_le a b unfold V rw [div_mul_div_comm, le_div_iff₀ (by positivity), div_mul_eq_mul_div, div_le_iff₀ (by positivity)] have : ((mulDn a b * 2 ^ 62 : Nat) : ℝ) ≤ ((a * b : Nat) : ℝ) := by exact_mod_cast h push_cast at this nlinarith [this] theorem V_mulUp {a b : Nat} (ha : a ≤ one) (hb : b ≤ one) : V a * V b ≤ V (mulUp a b) := by have h := mulUp_mul_ge ha hb unfold V rw [div_mul_div_comm, div_le_iff₀ (by positivity), div_mul_eq_mul_div, le_div_iff₀ (by positivity)] have : ((a * b : Nat) : ℝ) ≤ ((mulUp a b * 2 ^ 62 : Nat) : ℝ) := by exact_mod_cast h push_cast at this nlinarith [this] theorem V_mulDn_le {a b : Nat} {x y : ℝ} (ha : V a ≤ x) (hb : V b ≤ y) : V (mulDn a b) ≤ x * y := (V_mulDn a b).trans (mul_le_mul ha hb (V_nonneg b) ((V_nonneg a).trans ha)) theorem le_V_mulUp {a b : Nat} {x y : ℝ} (ha : x ≤ V a) (hb : y ≤ V b) (hy : 0 ≤ y) (ha1 : a ≤ one) (hb1 : b ≤ one) : x * y ≤ V (mulUp a b) := (mul_le_mul ha hb hy (V_nonneg a)).trans (V_mulUp ha1 hb1) theorem V_div_le (k : Nat) : V (one / k) ≤ 1 / k := by rcases Nat.eq_zero_or_pos k with rfl | hk · simp [V] have h : one / k * k ≤ one := Nat.div_mul_le_self one k have hc : ((one / k : Nat) : ℝ) * k ≤ (one : ℝ) := by exact_mod_cast h unfold V rw [div_le_div_iff₀ (by positivity) (by exact_mod_cast hk)] have : (one : ℝ) = 2 ^ 62 := by norm_num [one] linarith theorem le_V_divUp (k : Nat) (hk : 0 < k) : 1 / (k : ℝ) ≤ V ((one + k - 1) / k) := by have h : one ≤ (one + k - 1) / k * k := by have h2 := Nat.div_add_mod (one + k - 1) k have h3 := Nat.mod_lt (one + k - 1) hk have : (one + k - 1) / k * k = k * ((one + k - 1) / k) := Nat.mul_comm _ _ omega have hc : (one : ℝ) ≤ (((one + k - 1) / k : Nat) : ℝ) * k := by exact_mod_cast h unfold V rw [div_le_div_iff₀ (by exact_mod_cast hk) (by positivity)] have : (one : ℝ) = 2 ^ 62 := by norm_num [one] linarith def f2l : Nat := one / 2 def f3l : Nat := one / 6 def f4l : Nat := one / 24 def f5l : Nat := one / 120 def f6l : Nat := one / 720 def f2h : Nat := (one + 2 - 1) / 2 def f3h : Nat := (one + 6 - 1) / 6 def f4h : Nat := (one + 24 - 1) / 24 def f5h : Nat := (one + 120 - 1) / 120 def f6h : Nat := (one + 720 - 1) / 720 def remF : Nat := (one + 35280 - 1) / 35280 * 8 @[inline] def expSmall (rl rh : Nat) : Nat × Nat := let p2l := mulDn rl rl let p3l := mulDn p2l rl let p4l := mulDn p3l rl let p5l := mulDn p4l rl let p6l := mulDn p5l rl let p2h := mulUp rh rh let p3h := mulUp p2h rh let p4h := mulUp p3h rh let p5h := mulUp p4h rh let p6h := mulUp p5h rh let p7h := mulUp p6h rh let lo := (one + mulDn p2l f2l + mulDn p4l f4l + mulDn p6l f6l) - (rh + mulUp p3h f3h + mulUp p5h f5h + mulUp p7h remF) let hi := (one + mulUp p2h f2h + mulUp p4h f4h + mulUp p6h f6h + mulUp p7h remF) - (rl + mulDn p3l f3l + mulDn p5l f5l) (lo, min one hi) theorem exp_neg_taylor {r : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) : |Real.exp (-r) - (1 - r + r ^ 2 / 2 - r ^ 3 / 6 + r ^ 4 / 24 - r ^ 5 / 120 + r ^ 6 / 720)| ≤ r ^ 7 * (8 / 35280) := by have h := Real.exp_bound (x := -r) (by rw [abs_neg, abs_of_nonneg h0]; exact h1) (n := 7) (by norm_num) simp only [Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial] at h rw [abs_neg, abs_of_nonneg h0] at h convert h using 2 · norm_num; ring · norm_num theorem f_le_one {x : Nat} (k : Nat) (hk : 0 < k) (h : x = (one + k - 1) / k) : x ≤ one := by subst h; unfold one; apply Nat.div_le_of_le_mul; omega theorem expSmall_spec {rl rh : Nat} {r : ℝ} (hl : V rl ≤ r) (hh : r ≤ V rh) (hrh : rh ≤ one) : V (expSmall rl rh).1 ≤ Real.exp (-r) ∧ Real.exp (-r) ≤ V (expSmall rl rh).2 ∧ (expSmall rl rh).2 ≤ one := by have h0 : 0 ≤ r := (V_nonneg rl).trans hl have h1 : r ≤ 1 := hh.trans (V_one ▸ V_mono hrh) have hT := exp_neg_taylor h0 h1 have hp : ∀ n, 0 ≤ r ^ n := fun n => pow_nonneg h0 n have l2 : V (mulDn rl rl) ≤ r ^ 2 := by rw [sq]; exact V_mulDn_le hl hl have l3 : V (mulDn (mulDn rl rl) rl) ≤ r ^ 3 := by rw [pow_succ]; exact V_mulDn_le l2 hl have l4 : V (mulDn (mulDn (mulDn rl rl) rl) rl) ≤ r ^ 4 := by rw [pow_succ]; exact V_mulDn_le l3 hl have l5 : V (mulDn (mulDn (mulDn (mulDn rl rl) rl) rl) rl) ≤ r ^ 5 := by rw [pow_succ]; exact V_mulDn_le l4 hl have l6 : V (mulDn (mulDn (mulDn (mulDn (mulDn rl rl) rl) rl) rl) rl) ≤ r ^ 6 := by rw [pow_succ]; exact V_mulDn_le l5 hl have u2 : r ^ 2 ≤ V (mulUp rh rh) := by rw [sq]; exact le_V_mulUp hh hh h0 hrh hrh have b2 : mulUp rh rh ≤ one := mulUp_le hrh hrh have u3 : r ^ 3 ≤ V (mulUp (mulUp rh rh) rh) := by rw [pow_succ]; exact le_V_mulUp u2 hh h0 b2 hrh have b3 := mulUp_le b2 hrh have u4 : r ^ 4 ≤ V (mulUp (mulUp (mulUp rh rh) rh) rh) := by rw [pow_succ]; exact le_V_mulUp u3 hh h0 b3 hrh have b4 := mulUp_le b3 hrh have u5 : r ^ 5 ≤ V (mulUp (mulUp (mulUp (mulUp rh rh) rh) rh) rh) := by rw [pow_succ]; exact le_V_mulUp u4 hh h0 b4 hrh have b5 := mulUp_le b4 hrh have u6 : r ^ 6 ≤ V (mulUp (mulUp (mulUp (mulUp (mulUp rh rh) rh) rh) rh) rh) := by rw [pow_succ]; exact le_V_mulUp u5 hh h0 b5 hrh have b6 := mulUp_le b5 hrh have u7 : r ^ 7 ≤ V (mulUp (mulUp (mulUp (mulUp (mulUp (mulUp rh rh) rh) rh) rh) rh) rh) := by rw [pow_succ]; exact le_V_mulUp u6 hh h0 b6 hrh have b7 := mulUp_le b6 hrh have fl : ∀ (k : Nat) (x : Nat), x = one / k → V x ≤ 1 / k := fun k x h => h ▸ V_div_le k have fh : ∀ (k : Nat) (x : Nat), 0 < k → x = (one + k - 1) / k → 1 / (k : ℝ) ≤ V x := fun k x hk h => h ▸ le_V_divUp k hk have hf2l := fl 2 f2l rfl have hf3l := fl 6 f3l rfl have hf4l := fl 24 f4l rfl have hf5l := fl 120 f5l rfl have hf6l := fl 720 f6l rfl have hf2h := fh 2 f2h (by norm_num) rfl have hf3h := fh 6 f3h (by norm_num) rfl have hf4h := fh 24 f4h (by norm_num) rfl have hf5h := fh 120 f5h (by norm_num) rfl have hf6h := fh 720 f6h (by norm_num) rfl have hremF : 8 / (35280 : ℝ) ≤ V remF := by have h := fh 35280 ((one + 35280 - 1) / 35280) (by norm_num) rfl unfold remF V at * push_cast at * rw [mul_div_right_comm] nlinarith have bf2 := f_le_one 2 (by norm_num) (rfl : f2h = _) have bf3 := f_le_one 6 (by norm_num) (rfl : f3h = _) have bf4 := f_le_one 24 (by norm_num) (rfl : f4h = _) have bf5 := f_le_one 120 (by norm_num) (rfl : f5h = _) have bf6 := f_le_one 720 (by norm_num) (rfl : f6h = _) have brem : remF ≤ one := by unfold remF one; norm_num have c2 := V_mulDn_le l2 hf2l have c3 := V_mulDn_le l3 hf3l have c4 := V_mulDn_le l4 hf4l have c5 := V_mulDn_le l5 hf5l have c6 := V_mulDn_le l6 hf6l have d2 := le_V_mulUp u2 hf2h (by norm_num) b2 bf2 have d3 := le_V_mulUp u3 hf3h (by norm_num) b3 bf3 have d4 := le_V_mulUp u4 hf4h (by norm_num) b4 bf4 have d5 := le_V_mulUp u5 hf5h (by norm_num) b5 bf5 have d6 := le_V_mulUp u6 hf6h (by norm_num) b6 bf6 have d7 := le_V_mulUp u7 hremF (by norm_num) b7 brem have hexp1 : Real.exp (-r) ≤ 1 := Real.exp_le_one_iff.mpr (by linarith) have hab := abs_le.mp hT refine ⟨?_, ?_, min_le_left _ _⟩ · simp only [expSmall] refine le_trans (b := max 0 (V (one + mulDn (mulDn rl rl) f2l + mulDn (mulDn (mulDn (mulDn rl rl) rl) rl) f4l + mulDn (mulDn (mulDn (mulDn (mulDn (mulDn rl rl) rl) rl) rl) rl) f6l) - V (rh + mulUp (mulUp (mulUp rh rh) rh) f3h + mulUp (mulUp (mulUp (mulUp (mulUp rh rh) rh) rh) rh) f5h + mulUp (mulUp (mulUp (mulUp (mulUp (mulUp (mulUp rh rh) rh) rh) rh) rh) rh) remF))) ?_ ?_ · unfold V rw [le_max_iff] rcases le_total (rh + mulUp (mulUp (mulUp rh rh) rh) f3h + mulUp (mulUp (mulUp (mulUp (mulUp rh rh) rh) rh) rh) f5h + mulUp (mulUp (mulUp (mulUp (mulUp (mulUp (mulUp rh rh) rh) rh) rh) rh) rh) remF) (one + mulDn (mulDn rl rl) f2l + mulDn (mulDn (mulDn (mulDn rl rl) rl) rl) f4l + mulDn (mulDn (mulDn (mulDn (mulDn (mulDn rl rl) rl) rl) rl) rl) f6l) with h | h · right; rw [Nat.cast_sub h]; ring_nf; rfl · left; rw [Nat.sub_eq_zero_of_le h]; simp · apply max_le (Real.exp_pos _).le simp only [V_add, V_one] at * nlinarith · simp only [expSmall] rcases le_total one (one + mulUp (mulUp rh rh) f2h + mulUp (mulUp (mulUp (mulUp rh rh) rh) rh) f4h + mulUp (mulUp (mulUp (mulUp (mulUp (mulUp rh rh) rh) rh) rh) rh) f6h + mulUp (mulUp (mulUp (mulUp (mulUp (mulUp (mulUp rh rh) rh) rh) rh) rh) rh) remF - (rl + mulDn (mulDn (mulDn rl rl) rl) f3l + mulDn (mulDn (mulDn (mulDn (mulDn rl rl) rl) rl) rl) f5l)) with h | h · rw [min_eq_left h, V_one]; exact hexp1 · rw [min_eq_right h] refine le_trans ?_ (V_sub_ge _ _) simp only [V_add, V_one] linarith [hab.2] def Encl (iv : Nat × Nat) (b : ℝ) : Prop := V iv.1 ≤ Real.exp (-b) ∧ Real.exp (-b) ≤ V iv.2 ∧ iv.2 ≤ one def powOf (base : Nat × Nat) : Nat → Nat × Nat | 0 => (one, one) | j + 1 => let p := powOf base j; (mulDn p.1 base.1, min one (mulUp p.2 base.2)) theorem Encl.mul {x y : Nat × Nat} {a b : ℝ} (hx : Encl x a) (hy : Encl y b) : Encl (mulDn x.1 y.1, min one (mulUp x.2 y.2)) (a + b) := by have he : Real.exp (-(a + b)) = Real.exp (-a) * Real.exp (-b) := by rw [← Real.exp_add]; ring_nf refine ⟨?_, ?_, min_le_left _ _⟩ · rw [he]; exact V_mulDn_le hx.1 hy.1 · rw [he] rcases le_total one (mulUp x.2 y.2) with h | h · rw [min_eq_left h, V_one, ← he] exact Real.exp_le_one_iff.mpr (by have := Real.exp_le_one_iff.mp (le_trans hx.2.1 (V_one ▸ V_mono hx.2.2)) have := Real.exp_le_one_iff.mp (le_trans hy.2.1 (V_one ▸ V_mono hy.2.2)) linarith) · rw [min_eq_right h] exact le_V_mulUp hx.2.1 hy.2.1 (Real.exp_pos _).le hx.2.2 hy.2.2 theorem powOf_spec {base : Nat × Nat} {b : ℝ} (hb : Encl base b) : ∀ j : Nat, Encl (powOf base j) (j * b) | 0 => by refine ⟨?_, ?_, le_rfl⟩ <;> simp [powOf, V_one] | j + 1 => by have := (powOf_spec hb j).mul hb simp only [powOf] convert this using 2; push_cast; ring def sixtyFourth : Nat := 2 ^ 56 theorem V_sixtyFourth : V sixtyFourth = 1 / 64 := by norm_num [V, sixtyFourth] def base64 : Nat × Nat := expSmall sixtyFourth sixtyFourth theorem base64_spec : Encl base64 (1 / 64) := by exact expSmall_spec (rl := sixtyFourth) (rh := sixtyFourth) (r := 1 / 64) V_sixtyFourth.le V_sixtyFourth.ge (by norm_num [sixtyFourth, one]) def fracTab : Array (Nat × Nat) := Array.ofFn (n := 64) fun j => powOf base64 j.val def baseOne : Nat × Nat := powOf base64 64 def intTab : Array (Nat × Nat) := Array.ofFn (n := 17) fun n => powOf baseOne n.val theorem getElem!_ofFn' {α : Type} [Inhabited α] {n : Nat} (f : Fin n → α) {i : Nat} (h : i < n) : (Array.ofFn f)[i]! = f ⟨i, h⟩ := by rw [getElem!_pos (Array.ofFn f) i (by simpa using h)] simp theorem fracTab_spec {j : Nat} (h : j < 64) : Encl fracTab[j]! (j * (1 / 64)) := by rw [fracTab, getElem!_ofFn' _ h] exact powOf_spec base64_spec j theorem intTab_spec {n : Nat} (h : n < 17) : Encl intTab[n]! n := by rw [intTab, getElem!_ofFn' _ h] have h1 : Encl baseOne 1 := by have := powOf_spec base64_spec 64 simp only [baseOne]; convert this using 1; norm_num have := powOf_spec h1 n simpa using this @[inline] def scaled (m : Nat) (e : Int) : Nat × Nat := if 0 ≤ e + 56 then let v := m <<< (e + 56).toNat; (v, v) else let v := m >>> (-(e + 56)).toNat; (v, v + 1) theorem scaled_spec (m : Nat) (e : Int) : ((scaled m e).1 : ℝ) ≤ m * (2 : ℝ) ^ e * 2 ^ 56 ∧ (m : ℝ) * (2 : ℝ) ^ e * 2 ^ 56 ≤ (scaled m e).2 ∧ (scaled m e).1 ≤ (scaled m e).2 := by unfold scaled have hz : (m : ℝ) * (2 : ℝ) ^ e * 2 ^ 56 = m * (2 : ℝ) ^ (e + 56) := by rw [zpow_add₀ two_ne_zero]; norm_num; ring split · rename_i h have hk : ((2 : ℝ) ^ (e + 56)) = 2 ^ (e + 56).toNat := by rw [← zpow_natCast, Int.toNat_of_nonneg h] simp only [Nat.shiftLeft_eq, hz, hk]; push_cast; simp · rename_i h set k := (-(e + 56)).toNat have hk : ((2 : ℝ) ^ (e + 56)) = 1 / 2 ^ k := by rw [show e + 56 = -(k : Int) by omega, zpow_neg, zpow_natCast, one_div] simp only [Nat.shiftRight_eq_div_pow, hz, hk] have hp : (0 : ℝ) < 2 ^ k := by positivity have h1 := Nat.div_mul_le_self m (2 ^ k) have h2 := Nat.lt_succ_iff.mpr (le_refl (m / 2 ^ k)) have h3 : m < (m / 2 ^ k + 1) * 2 ^ k := by have := Nat.lt_mul_div_succ m (Nat.two_pow_pos k); linarith refine ⟨?_, ?_, Nat.le_succ _⟩ · rw [mul_one_div, le_div_iff₀ hp]; exact_mod_cast h1 · rw [mul_one_div, div_le_iff₀ hp]; push_cast; exact_mod_cast h3.le def lim17 : Nat := 17 * 2 ^ 56 @[inline] def expNeg (m : Nat) (e : Int) : Option (Nat × Nat) := let c := scaled m e if lim17 ≤ c.2 then none else let q := c.1 >>> 50 let rl := (c.1 - (q <<< 50)) <<< 6 let rh := (c.2 - (q <<< 50)) <<< 6 if one < rh then none else let P := expSmall rl rh let F := fracTab[q % 64]! let I := intTab[q >>> 6]! let IF := (mulDn I.1 F.1, min one (mulUp I.2 F.2)) some (mulDn IF.1 P.1, min one (mulUp IF.2 P.2)) theorem expNeg_spec {m : Nat} {e : Int} {iv : Nat × Nat} (h : expNeg m e = some iv) : Encl iv (m * (2 : ℝ) ^ e) := by unfold expNeg at h simp only [Nat.shiftRight_eq_div_pow, Nat.shiftLeft_eq] at h obtain ⟨hlo, hhi, hle⟩ := scaled_spec m e generalize (scaled m e).1 = cl at * generalize (scaled m e).2 = ch at * split at h · exact absurd h (by simp) rename_i hlim split at h · exact absurd h (by simp) rename_i hrh simp only [Option.some.injEq] at h subst h set q := cl / 2 ^ 50 have hq : q * 2 ^ 50 ≤ cl := Nat.div_mul_le_self cl _ have hqd : q = q / 2 ^ 6 * 64 + q % 64 := by have := Nat.div_add_mod q 64; omega have hn : q / 2 ^ 6 < 17 := by unfold lim17 at hlim; omega have hj : q % 64 < 64 := Nat.mod_lt _ (by norm_num) set C := (m : ℝ) * (2 : ℝ) ^ e set r := C - (q / 2 ^ 6 : Nat) - (q % 64 : Nat) * (1 / 64 : ℝ) have hr : C = (q / 2 ^ 6 : Nat) + (q % 64 : Nat) * (1 / 64 : ℝ) + r := by ring have hqr : ((q : Nat) : ℝ) * 2 ^ 50 = ((q / 2 ^ 6 : Nat) : ℝ) * 2 ^ 56 + ((q % 64 : Nat) : ℝ) * 2 ^ 50 := by have : ((q : Nat) : ℝ) = ((q / 2 ^ 6 * 64 + q % 64 : Nat) : ℝ) := by rw [← hqd] rw [this]; push_cast; ring have hrl : V ((cl - q * 2 ^ 50) * 2 ^ 6) ≤ r := by unfold V; rw [Nat.cast_mul, Nat.cast_sub hq]; push_cast rw [div_le_iff₀ (by positivity)] simp only [r]; nlinarith [hqr] have hrh' : r ≤ V ((ch - q * 2 ^ 50) * 2 ^ 6) := by unfold V; rw [Nat.cast_mul, Nat.cast_sub (hq.trans hle)]; push_cast rw [le_div_iff₀ (by positivity)] simp only [r]; nlinarith [hqr] have hP := expSmall_spec hrl hrh' (by omega) have hI := intTab_spec hn have hF := fracTab_spec hj rw [hr] exact (hI.mul hF).mul hP def two62f : Float := 4611686018427387904.0 @[inline] def mulLe (q d num : Nat) : Bool := let h := (mulHiW q.toUInt64 d.toUInt64).toNat let nh := num >>> 2 h < nh || (h == nh && mulLoW q.toUInt64 d.toUInt64 ≤ (num % 4).toUInt64 <<< 62) @[inline] def mulGe (q d num : Nat) : Bool := let h := (mulHiW q.toUInt64 d.toUInt64).toNat let nh := num >>> 2 nh < h || (h == nh && (num % 4).toUInt64 <<< 62 ≤ mulLoW q.toUInt64 d.toUInt64) theorem num_split (num : Nat) : ((num % 4).toUInt64 <<< 62).toNat = num % 4 * 2 ^ 62 := by have h4 : num % 4 < 4 := Nat.mod_lt _ (by norm_num) rw [UInt64.toNat_shiftLeft, toNat_toUInt64_of_lt (by omega)] have : (62 : UInt64).toNat % 64 = 62 := by decide rw [this, Nat.shiftLeft_eq, Nat.mod_eq_of_lt (by omega)] theorem mulLe_spec {q d num : Nat} (hq : q < 2 ^ 64) (hd : d < 2 ^ 64) (h : mulLe q d num = true) : q * d ≤ num * 2 ^ 62 := by have hs := halves hq hd unfold mulLe at h simp only [Nat.shiftRight_eq_div_pow, Bool.or_eq_true, decide_eq_true_eq, Bool.and_eq_true, beq_iff_eq, UInt64.le_iff_toNat_le, num_split] at h have hl := (mulLoW q.toUInt64 d.toUInt64).toNat_lt generalize (mulHiW q.toUInt64 d.toUInt64).toNat = a at * generalize (mulLoW q.toUInt64 d.toUInt64).toNat = b at * omega theorem mulGe_spec {q d num : Nat} (hq : q < 2 ^ 64) (hd : d < 2 ^ 64) (h : mulGe q d num = true) : num * 2 ^ 62 ≤ q * d := by have hs := halves hq hd unfold mulGe at h simp only [Nat.shiftRight_eq_div_pow, Bool.or_eq_true, decide_eq_true_eq, Bool.and_eq_true, beq_iff_eq, UInt64.le_iff_toNat_le, num_split] at h have hl := (mulLoW q.toUInt64 d.toUInt64).toNat_lt generalize (mulHiW q.toUInt64 d.toUInt64).toNat = a at * generalize (mulLoW q.toUInt64 d.toUInt64).toNat = b at * omega @[inline] def guess (num den : Nat) : Nat := ((num.toUInt64.toFloat * two62f) / den.toUInt64.toFloat).toUInt64.toNat def lim64 : Nat := 2 ^ 64 @[inline] def divLo (num den : Nat) : Option Nat := let g := guess num den let q := g - ((g >>> 50) + 2) if q < lim64 && den < lim64 && mulLe q den num then some q else none @[inline] def divHi (num den : Nat) : Option Nat := let g := guess num den let q := g + ((g >>> 50) + 2) if q < lim64 && den < lim64 && mulGe q den num then some q else none theorem V_mul_iff (a b c : Nat) : V a * V b ≤ V c ↔ a * b ≤ c * 2 ^ 62 := by unfold V rw [div_mul_div_comm, div_le_div_iff₀ (by positivity) (by positivity)] constructor · intro h have : ((a * b : Nat) : ℝ) * 2 ^ 62 ≤ ((c * 2 ^ 62 : Nat) : ℝ) * 2 ^ 62 := by push_cast; nlinarith exact_mod_cast le_of_mul_le_mul_right this (by positivity) · intro h have : ((a * b : Nat) : ℝ) ≤ ((c * 2 ^ 62 : Nat) : ℝ) := by exact_mod_cast h push_cast at this; nlinarith theorem divLo_spec {num den q : Nat} (h : divLo num den = some q) : V q * V den ≤ V num := by unfold divLo at h dsimp only at h generalize guess num den = g at h split at h · rename_i hc simp only [Bool.and_eq_true, decide_eq_true_eq] at hc simp only [Option.some.injEq] at h; subst h exact (V_mul_iff _ _ _).mpr (mulLe_spec hc.1.1 hc.1.2 hc.2) · simp at h theorem divHi_spec {num den q : Nat} (h : divHi num den = some q) : V num ≤ V q * V den := by unfold divHi at h dsimp only at h generalize guess num den = g at h split at h · rename_i hc simp only [Bool.and_eq_true, decide_eq_true_eq] at hc simp only [Option.some.injEq] at h; subst h have h2 := mulGe_spec hc.1.1 hc.1.2 hc.2 unfold V rw [div_mul_div_comm, div_le_div_iff₀ (by positivity) (by positivity)] have : ((num * 2 ^ 62 : Nat) : ℝ) ≤ (((g + (g >>> 50 + 2)) * den : Nat) : ℝ) := by exact_mod_cast h2 push_cast at this ⊢; nlinarith · simp at h open ExactRuntime FloatLib.Floats.Formats.BinaryInterchange FloatLib.Floats FloatLib.Numerics open ExactRuntime.FastRound def settleInt (lo hi : Int) : Option UInt32 := let a := finishWord lo (-62) false if lo ≠ 0 && hi ≠ 0 && a == finishWord hi (-62) false && expOf a != 255 && (decodeD a).significand != 0 then some a else none @[inline] def settle (neg : Bool) (a b : Nat) : Option UInt32 := let w := roundW neg a (-62) if a ≠ 0 && b ≠ 0 && w == roundW neg b (-62) && expOf w != 255 && (decodeD w).significand != 0 then some w else none theorem settle_eq (neg : Bool) (a b : Nat) : settle neg a b = settleInt (if neg then -(b : Int) else a) (if neg then -(a : Int) else b) := by unfold settle settleInt by_cases ha : a = 0 · subst ha; cases neg <;> simp by_cases hb : b = 0 · subst hb; cases neg <;> simp rw [roundW_signed neg a _ ha, roundW_signed neg b _ hb] cases neg · simp · simp only [ite_true] by_cases he : finishWord (-(a : Int)) (-62) false = finishWord (-(b : Int)) (-62) false · simp [ha, hb, he] · have he' : ¬ finishWord (-(b : Int)) (-62) false = finishWord (-(a : Int)) (-62) false := fun h => he h.symm simp [ha, hb, he, he'] theorem settleInt_spec {lo hi : Int} {a : UInt32} (h : settleInt lo hi = some a) {v : ℝ} (hl : (lo : ℝ) * 2 ^ (-62 : Int) ≤ v) (hh : v ≤ (hi : ℝ) * 2 ^ (-62 : Int)) {z : Model Fmt} (hz : Model.toReal z = Model.roundAt Fmt v) : toWord z = a := by unfold settleInt at h dsimp only at h split at h · rename_i hc simp only [Option.some.injEq] at h subst h simp only [Bool.and_eq_true, bne_iff_ne, ne_eq, decide_eq_true_eq, beq_iff_eq] at hc obtain ⟨⟨⟨⟨hlo, hhi⟩, heq⟩, hfin⟩, hsig⟩ := hc exact bracket_spec hlo hhi rfl heq.symm hfin hsig hl hh hz · simp at h theorem int_scale (n : Nat) : ((n : Int) : ℝ) * 2 ^ (-62 : Int) = V n := by unfold V; push_cast; rw [zpow_neg, zpow_ofNat]; ring theorem toReal_ofW_decode {w : UInt32} (hfin : expOf w ≠ 255) : Model.toReal (ofW w) = (if (decodeD w).negative then -1 else 1) * ((decodeD w).significand * (2 : ℝ) ^ (decodeD w).exponent) := by rw [Model.toReal_eq, ofW, toDyadic_ofUInt32 _ hfin] simp only [FloatLib.Numerics.Dyadic.toReal, FloatLib.Numerics.Dyadic.cast_signedSignificand] ring theorem realSigmoid_neg_eq (C : ℝ) : realSigmoid (-C) = Real.exp (-C) / (1 + Real.exp (-C)) := by unfold realSigmoid rw [neg_neg] have hp := Real.exp_pos (-C) have h : Real.exp C = 1 / Real.exp (-C) := by rw [Real.exp_neg, one_div, inv_inv] rw [h]; field_simp; ring def sigmoidFast (w : UInt32) : Option UInt32 := if expOf w = 255 then none else let d := decodeD w match expNeg d.significand d.exponent with | none => none | some t => if d.negative then match divLo t.1 (one + t.1), divHi t.2 (one + t.2) with | some ql, some qh => settle false ql qh | _, _ => none else match divLo one (one + t.2), divHi one (one + t.1) with | some ql, some qh => settle false ql qh | _, _ => none theorem sigmoidFast_spec {w a : UInt32} (h : sigmoidFast w = some a) : sigmoidCR w = a := by unfold sigmoidFast at h split at h · simp at h rename_i hfin dsimp only at h have hx := toReal_ofW_decode hfin generalize decodeD w = d at h hx have hspec := (toReal_sigmoidModel (fmt := Fmt) (by decide) (input := Model.ofUInt32 w) (by simp [isFinite_ofUInt32, hfin])).2 change Model.toReal (sigmoidModel (ofW w)) = Model.roundAt Fmt (realSigmoid (Model.toReal (ofW w))) at hspec rw [hx] at hspec change toWord (sigmoidModel (ofW w)) = a split at h · simp at h rename_i t ht have hE := expNeg_spec ht set C := (d.significand : ℝ) * (2 : ℝ) ^ d.exponent set T := Real.exp (-C) have hT : 0 < T := Real.exp_pos _ obtain ⟨h1, h2, h3⟩ := hE have v1 := V_nonneg t.1 have v2 := V_nonneg t.2 split at h · rename_i hneg split at h · rename_i ql qh hql hqh have bl := divLo_spec hql have bh := divHi_spec hqh rw [V_add, V_one] at bl bh rw [settle_eq] at h simp only [Bool.false_eq_true, ite_false] at h refine settleInt_spec h (v := realSigmoid (-C)) ?_ ?_ (by rw [hspec, hneg]; simp) · rw [int_scale] have : realSigmoid (-C) = T / (1 + T) := realSigmoid_neg_eq C rw [this, le_div_iff₀ (by linarith)] nlinarith · rw [int_scale] have : realSigmoid (-C) = T / (1 + T) := realSigmoid_neg_eq C rw [this, div_le_iff₀ (by linarith)] nlinarith · simp at h · rename_i hneg split at h · rename_i ql qh hql hqh have bl := divLo_spec hql have bh := divHi_spec hqh rw [V_add, V_one] at bl bh have hs : realSigmoid C = 1 / (1 + T) := rfl rw [settle_eq] at h simp only [Bool.false_eq_true, ite_false] at h refine settleInt_spec h (v := realSigmoid C) ?_ ?_ (by rw [hspec]; simp [hneg]) · rw [int_scale, hs, le_div_iff₀ (by linarith)] nlinarith · rw [int_scale, hs, div_le_iff₀ (by linarith)] nlinarith · simp at h def sigmoidF (w : UInt32) : UInt32 := (sigmoidFast w).getD (sigmoidCR w) theorem sigmoidF_eq : sigmoidF = sigmoidCR := by funext w unfold sigmoidF cases h : sigmoidFast w with | none => rfl | some a => exact (sigmoidFast_spec h).symm def tanhFast (w : UInt32) : Option UInt32 := if expOf w = 255 then none else let d := decodeD w match expNeg d.significand (d.exponent + 1) with | none => none | some t => if one < t.1 then none else match divLo (one - t.2) (one + t.2), divHi (one - t.1) (one + t.1) with | some ql, some qh => settle d.negative ql qh | _, _ => none theorem neg_int_scale (n : Nat) : ((-(n : Int) : Int) : ℝ) * 2 ^ (-62 : Int) = -V n := by rw [Int.cast_neg, neg_mul, int_scale] theorem tanhFast_spec {w a : UInt32} (h : tanhFast w = some a) : tanhCR w = a := by unfold tanhFast at h split at h · simp at h rename_i hfin dsimp only at h have hx := toReal_ofW_decode hfin generalize decodeD w = d at h hx have hspec := (toReal_tanhModel (fmt := Fmt) (by decide) (input := Model.ofUInt32 w) (by simp [isFinite_ofUInt32, hfin])).2 change Model.toReal (tanhModel (ofW w)) = Model.roundAt Fmt (Real.tanh (Model.toReal (ofW w))) at hspec rw [hx] at hspec change toWord (tanhModel (ofW w)) = a split at h · simp at h rename_i t ht have hE := expNeg_spec ht set C := (d.significand : ℝ) * (2 : ℝ) ^ d.exponent have h2C : (d.significand : ℝ) * (2 : ℝ) ^ (d.exponent + 1) = 2 * C := by rw [zpow_add₀ two_ne_zero]; simp only [C]; ring rw [h2C] at hE set T := Real.exp (-(2 * C)) have hT : 0 < T := Real.exp_pos _ have htanh : Real.tanh C = (1 - T) / (1 + T) := by rw [tanh_eq_exp_neg_two]; simp only [T]; ring_nf obtain ⟨h1, h2, h3⟩ := hE have v1 := V_nonneg t.1 have v2 := V_nonneg t.2 split at h · simp at h rename_i ht1 replace ht1 := not_lt.mp ht1 split at h · rename_i ql qh hql hqh have bl := divLo_spec hql have bh := divHi_spec hqh rw [V_add, V_one, V_sub_le_of_le h3, V_one] at bl rw [V_add, V_one, V_sub_le_of_le ht1, V_one] at bh have lo : V ql ≤ Real.tanh C := by rw [htanh, le_div_iff₀ (by linarith)]; nlinarith have hi : Real.tanh C ≤ V qh := by rw [htanh, div_le_iff₀ (by linarith)]; nlinarith rw [settle_eq] at h cases hneg : d.negative <;> simp only [hneg, ite_true, Bool.false_eq_true, ite_false] at h · refine settleInt_spec h (v := Real.tanh C) ?_ ?_ (by rw [hspec]; simp [hneg]) · rw [int_scale]; exact lo · rw [int_scale]; exact hi · refine settleInt_spec h (v := Real.tanh (-C)) ?_ ?_ (by rw [hspec, hneg]; simp) · rw [neg_int_scale, Real.tanh_neg]; linarith · rw [neg_int_scale, Real.tanh_neg]; linarith · simp at h def tanhF (w : UInt32) : UInt32 := (tanhFast w).getD (tanhCR w) theorem tanhF_eq : tanhF = tanhCR := by funext w unfold tanhF cases h : tanhFast w with | none => rfl | some a => exact (tanhFast_spec h).symm def expFast (w : UInt32) : Option UInt32 := if expOf w = 255 then none else let d := decodeD w if !d.negative && d.significand != 0 then none else match expNeg d.significand d.exponent with | none => none | some t => settle false t.1 t.2 theorem expFast_spec {w a : UInt32} (h : expFast w = some a) : expW w = a := by unfold expFast at h split at h · simp at h rename_i hfin dsimp only at h have hx := toReal_ofW_decode hfin generalize hd : decodeD w = d at h hx split at h · simp at h rename_i hsign simp only [Bool.and_eq_true, Bool.not_eq_true', bne_iff_ne, ne_eq, not_and, not_not] at hsign split at h · simp at h rename_i t ht obtain ⟨h1, h2, -⟩ := expNeg_spec ht set C := (d.significand : ℝ) * (2 : ℝ) ^ d.exponent have hxC : Model.toReal (ofW w) = -C := by rw [hx] by_cases hneg : d.negative = true · simp [hneg] · have hz : d.significand = 0 := hsign (by simpa using hneg) simp [C, hz] have hfinw : Model.isFinite (ofW w) = true := by simp [ofW, isFinite_ofUInt32, hfin] have hrange : Real.exp (Model.toReal (ofW w)) < (Model.Transcendentals.Certified.overflowThreshold Fmt : ℝ) := by have hC : 0 ≤ C := by simp only [C]; positivity have : Real.exp (-C) ≤ 1 := Real.exp_le_one_iff.mpr (by linarith) rw [hxC] exact lt_of_le_of_lt this (Model.Transcendentals.CorrectlyRounded.one_lt_overflowThreshold (by decide)) have hspec := Model.Transcendentals.CorrectlyRounded.toReal_exp_eq_roundAt (fmt := Fmt) (by decide) hfinw hrange (budget := {}) rw [hxC] at hspec rw [settle_eq] at h simp only [Bool.false_eq_true, ite_false] at h exact settleInt_spec h (v := Real.exp (-C)) (by rw [int_scale]; exact h1) (by rw [int_scale]; exact h2) hspec def expF (w : UInt32) : UInt32 := (expFast w).getD (expW w) theorem expF_eq : expF = expW := by funext w unfold expF cases h : expFast w with | none => rfl | some a => exact (expFast_spec h).symm end FastAct namespace Submission namespace I open ExactRuntime FloatLib.Floats.Formats.BinaryInterchange FloatLib.Floats @[specialize] def maxExp (fa fb : Nat → UInt32) (E index : Nat) : Nat → Option Nat | 0 => some E | count + 1 => let a := fa index let b := fb index if expOf a = 255 ∨ expOf b = 255 then none else maxExp fa fb (max E (idxOf a + idxOf b)) (index + 1) count theorem maxExp_spec (fa fb : Nat → UInt32) : ∀ (count E index E' : Nat), maxExp fa fb E index count = some E' → E ≤ E' ∧ ∀ k, index ≤ k → k < index + count → expOf (fa k) ≠ 255 ∧ expOf (fb k) ≠ 255 ∧ idxOf (fa k) + idxOf (fb k) ≤ E' | 0, E, index, E', h => by simp only [maxExp, Option.some.injEq] at h exact ⟨h.le, fun k h1 h2 => by omega⟩ | count + 1, E, index, E', h => by simp only [maxExp] at h split at h · simp at h · rename_i hs obtain ⟨hE, hall⟩ := maxExp_spec fa fb count _ _ _ h push_neg at hs refine ⟨le_trans (le_max_left _ _) hE, fun k h1 h2 => ?_⟩ rcases Nat.lt_or_ge k (index + 1) with hk | hk · have : k = index := by omega subst this exact ⟨hs.1, hs.2, le_trans (le_max_right _ _) hE⟩ · exact hall k hk (by omega) @[inline] def winTerm (t e Ec : Nat) : Nat := if Ec ≤ e then t <<< (e - Ec) else t >>> (Ec - e) theorem winTerm_bounds (t e Ec : Nat) : winTerm t e Ec * 2 ^ Ec ≤ t * 2 ^ e ∧ t * 2 ^ e < (winTerm t e Ec + 1) * 2 ^ Ec := by unfold winTerm split · rename_i h rw [Nat.shiftLeft_eq] have : 2 ^ e = 2 ^ (e - Ec) * 2 ^ Ec := by rw [← pow_add]; congr 1; omega rw [this] constructor · rw [Nat.mul_assoc] · have : 0 < 2 ^ Ec := Nat.two_pow_pos _ nlinarith · rename_i h rw [Nat.shiftRight_eq_div_pow] have hp : 2 ^ Ec = 2 ^ (Ec - e) * 2 ^ e := by rw [← pow_add]; congr 1; omega have hpos : 0 < 2 ^ e := Nat.two_pow_pos _ have hq := Nat.div_mul_le_self t (2 ^ (Ec - e)) have hr := Nat.lt_mul_div_succ t (Nat.two_pow_pos (Ec - e)) rw [hp] constructor · calc t / 2 ^ (Ec - e) * (2 ^ (Ec - e) * 2 ^ e) = t / 2 ^ (Ec - e) * 2 ^ (Ec - e) * 2 ^ e := by ring _ ≤ t * 2 ^ e := Nat.mul_le_mul_right _ hq · calc t * 2 ^ e < 2 ^ (Ec - e) * (t / 2 ^ (Ec - e) + 1) * 2 ^ e := Nat.mul_lt_mul_of_pos_right hr hpos _ = (t / 2 ^ (Ec - e) + 1) * (2 ^ (Ec - e) * 2 ^ e) := by ring def sumNat (fa fb : Nat → UInt32) (Ec index : Nat) : Nat → Nat × Nat | 0 => (0, 0) | count + 1 => let a := fa index let b := fb index let q := winTerm (mantOf a * mantOf b) (idxOf a + idxOf b) Ec let r := sumNat fa fb Ec (index + 1) count if signOf a != signOf b then (r.1, r.2 + q) else (r.1 + q, r.2) theorem sumNat_bounds (fa fb : Nat → UInt32) (A B : Array UInt32) (n Ec : Nat) (hA : ∀ k, k < n → A[k]! = fa k) (hB : ∀ k, k < n → B[k]! = fb k) : ∀ (count index : Nat), index + count ≤ n → (((sumNat fa fb Ec index count).1 : Int) - (sumNat fa fb Ec index count).2 - count) * 2 ^ Ec ≤ dsum A B index count ∧ dsum A B index count ≤ (((sumNat fa fb Ec index count).1 : Int) - (sumNat fa fb Ec index count).2 + count) * 2 ^ Ec | 0, index, _ => by simp [sumNat, dsum] | count + 1, index, h => by obtain ⟨ih1, ih2⟩ := sumNat_bounds fa fb A B n Ec hA hB count (index + 1) (by omega) simp only [sumNat, dsum] rw [hA index (by omega), hB index (by omega)] set a := fa index set b := fb index set r := sumNat fa fb Ec (index + 1) count obtain ⟨w1, w2⟩ := winTerm_bounds (mantOf a * mantOf b) (idxOf a + idxOf b) Ec set q := winTerm (mantOf a * mantOf b) (idxOf a + idxOf b) Ec have hsv := Pinned.sv_mul a b have c1 : ((q * 2 ^ Ec : Nat) : Int) ≤ ((mantOf a * mantOf b * 2 ^ (idxOf a + idxOf b) : Nat) : Int) := by exact_mod_cast w1 have c2 : ((mantOf a * mantOf b * 2 ^ (idxOf a + idxOf b) : Nat) : Int) < (((q + 1) * 2 ^ Ec : Nat) : Int) := by exact_mod_cast w2 push_cast at c1 c2 ih1 ih2 ⊢ split · rename_i hs have : sv a * sv b = -((mantOf a * mantOf b : Nat) : Int) := by rw [← hsv]; simp [show Bool.xor (signOf a) (signOf b) = true by simpa [bne_iff_ne] using hs] push_cast at this rw [this] push_cast constructor <;> (ring_nf; ring_nf at ih1 ih2 c1 c2; linarith) · rename_i hs have : sv a * sv b = ((mantOf a * mantOf b : Nat) : Int) := by rw [← hsv]; simp [show Bool.xor (signOf a) (signOf b) = false by simpa [bne_iff_ne] using hs] push_cast at this rw [this] push_cast constructor <;> (ring_nf; ring_nf at ih1 ih2 c1 c2; linarith) @[inline] def winTermW (a b : UInt32) (Ec : UInt64) : UInt64 := let t := (mantOf a).toUInt64 * (mantOf b).toUInt64 let e := (idxOf a + idxOf b).toUInt64 if Ec ≤ e then t <<< (e - Ec) else if Ec - e < 64 then t >>> (Ec - e) else 0 @[specialize] def sumWin64 (fa fb : Nat → UInt32) (Ec : UInt64) (P N : UInt64) (index : Nat) : Nat → UInt64 × UInt64 | 0 => (P, N) | count + 1 => let a := fa index let b := fb index let q := winTermW a b Ec if signOf a != signOf b then sumWin64 fa fb Ec P (N + q) (index + 1) count else sumWin64 fa fb Ec (P + q) N (index + 1) count theorem winTermW_eq (a b : UInt32) (Ec c : Nat) (hc : c ≤ 15) (hEc : Ec ≤ 600) (he : idxOf a + idxOf b ≤ Ec + c) : (winTermW a b Ec.toUInt64).toNat = winTerm (mantOf a * mantOf b) (idxOf a + idxOf b) Ec ∧ winTerm (mantOf a * mantOf b) (idxOf a + idxOf b) Ec < 2 ^ (48 + c) := by have ha := mantOf_lt_24 a have hb := mantOf_lt_24 b have hab : mantOf a * mantOf b < 2 ^ 48 := by calc mantOf a * mantOf b < 2 ^ 24 * 2 ^ 24 := Nat.mul_lt_mul'' ha hb _ = 2 ^ 48 := by norm_num have ht : ((mantOf a).toUInt64 * (mantOf b).toUInt64).toNat = mantOf a * mantOf b := by rw [UInt64.toNat_mul, FastAct.toNat_toUInt64_of_lt (by omega), FastAct.toNat_toUInt64_of_lt (by omega)] exact Nat.mod_eq_of_lt (by omega) have hix : idxOf a + idxOf b ≤ 615 := by omega have heN : (idxOf a + idxOf b).toUInt64.toNat = idxOf a + idxOf b := FastAct.toNat_toUInt64_of_lt (by omega) have hEN : Ec.toUInt64.toNat = Ec := FastAct.toNat_toUInt64_of_lt (by omega) unfold winTermW winTerm dsimp only by_cases h1 : Ec ≤ idxOf a + idxOf b · have hle : Ec.toUInt64 ≤ (idxOf a + idxOf b).toUInt64 := by rw [UInt64.le_iff_toNat_le, hEN, heN]; exact h1 simp only [hle, ite_true, h1] have hd : ((idxOf a + idxOf b).toUInt64 - Ec.toUInt64).toNat = idxOf a + idxOf b - Ec := by rw [UInt64.toNat_sub_of_le _ _ hle, heN, hEN] have hsh : idxOf a + idxOf b - Ec ≤ c := by omega have hlt : mantOf a * mantOf b * 2 ^ (idxOf a + idxOf b - Ec) < 2 ^ (48 + c) := by calc mantOf a * mantOf b * 2 ^ (idxOf a + idxOf b - Ec) < 2 ^ 48 * 2 ^ (idxOf a + idxOf b - Ec) := Nat.mul_lt_mul_of_pos_right hab (Nat.two_pow_pos _) _ ≤ 2 ^ 48 * 2 ^ c := Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by norm_num) hsh) _ = 2 ^ (48 + c) := by rw [← pow_add] have h63 : 2 ^ (48 + c) ≤ 2 ^ 63 := Nat.pow_le_pow_right (by norm_num) (by omega) rw [UInt64.toNat_shiftLeft, ht, hd, Nat.shiftLeft_eq, Nat.shiftLeft_eq, Nat.mod_eq_of_lt (by omega : idxOf a + idxOf b - Ec < 64)] exact ⟨Nat.mod_eq_of_lt (by omega), hlt⟩ · have hle : ¬ Ec.toUInt64 ≤ (idxOf a + idxOf b).toUInt64 := by rw [UInt64.le_iff_toNat_le, hEN, heN]; exact h1 simp only [hle, ite_false, h1] have hd : (Ec.toUInt64 - (idxOf a + idxOf b).toUInt64).toNat = Ec - (idxOf a + idxOf b) := by rw [UInt64.toNat_sub_of_le _ _ (by rw [UInt64.le_iff_toNat_le, hEN, heN]; omega), heN, hEN] have hsmall : (mantOf a * mantOf b) >>> (Ec - (idxOf a + idxOf b)) < 2 ^ (48 + c) := by rw [Nat.shiftRight_eq_div_pow] calc mantOf a * mantOf b / 2 ^ (Ec - (idxOf a + idxOf b)) ≤ mantOf a * mantOf b := Nat.div_le_self _ _ _ < 2 ^ 48 := hab _ ≤ 2 ^ (48 + c) := Nat.pow_le_pow_right (by norm_num) (by omega) refine ⟨?_, hsmall⟩ split · rename_i h64 rw [UInt64.lt_iff_toNat_lt, hd] at h64 rw [UInt64.toNat_shiftRight, ht, hd, Nat.mod_eq_of_lt (by simpa using h64)] · rename_i h64 rw [UInt64.lt_iff_toNat_lt, hd] at h64 simp only [UInt64.toNat_zero] rw [Nat.shiftRight_eq_div_pow, eq_comm, Nat.div_eq_zero_iff] right calc mantOf a * mantOf b < 2 ^ 48 := hab _ ≤ 2 ^ (Ec - (idxOf a + idxOf b)) := Nat.pow_le_pow_right (by norm_num) (by simp at h64; omega) theorem sumWin64_eq (fa fb : Nat → UInt32) (Ec c : Nat) (hc : c ≤ 15) (hEc : Ec ≤ 600) : ∀ (count index : Nat) (P N : UInt64), (∀ k, index ≤ k → k < index + count → idxOf (fa k) + idxOf (fb k) ≤ Ec + c) → P.toNat + N.toNat + count * 2 ^ (48 + c) < 2 ^ 64 → (sumWin64 fa fb Ec.toUInt64 P N index count).1.toNat = P.toNat + (sumNat fa fb Ec index count).1 ∧ (sumWin64 fa fb Ec.toUInt64 P N index count).2.toNat = N.toNat + (sumNat fa fb Ec index count).2 | 0, index, P, N, _, _ => by simp [sumWin64, sumNat] | count + 1, index, P, N, he, hb => by obtain ⟨hq, hqlt⟩ := winTermW_eq (fa index) (fb index) Ec c hc hEc (he index le_rfl (by omega)) simp only [sumWin64, sumNat] have hpow : count * 2 ^ (48 + c) + 2 ^ (48 + c) = (count + 1) * 2 ^ (48 + c) := by ring split · have hN : (N + winTermW (fa index) (fb index) Ec.toUInt64).toNat = N.toNat + winTerm (mantOf (fa index) * mantOf (fb index)) (idxOf (fa index) + idxOf (fb index)) Ec := by rw [UInt64.toNat_add, hq]; exact Nat.mod_eq_of_lt (by omega) obtain ⟨r1, r2⟩ := sumWin64_eq fa fb Ec c hc hEc count (index + 1) P _ (fun k h1 h2 => he k (by omega) (by omega)) (by rw [hN]; omega) refine ⟨r1, ?_⟩ rw [r2, hN]; ring · have hP : (P + winTermW (fa index) (fb index) Ec.toUInt64).toNat = P.toNat + winTerm (mantOf (fa index) * mantOf (fb index)) (idxOf (fa index) + idxOf (fb index)) Ec := by rw [UInt64.toNat_add, hq]; exact Nat.mod_eq_of_lt (by omega) obtain ⟨r1, r2⟩ := sumWin64_eq fa fb Ec c hc hEc count (index + 1) _ N (fun k h1 h2 => he k (by omega) (by omega)) (by rw [hP]; omega) refine ⟨?_, r2⟩ rw [r1, hP]; ring theorem dotLoop_special_false (fa fb : Nat → UInt32) : ∀ (count index : Nat) (pos neg : Array Nat) (nz : Bool), (∀ k, index ≤ k → k < index + count → expOf (fa k) ≠ 255 ∧ expOf (fb k) ≠ 255) → (Pinned.dotLoop fa fb pos neg false nz index count).special = false | 0, _, _, _, _, _ => by simp [Pinned.dotLoop] | count + 1, index, pos, neg, nz, hfin => by have h := hfin index le_rfl (by omega) simp only [Pinned.dotLoop] have hstep : (Pinned.dotStep ⟨pos, neg, false, nz⟩ (fa index) (fb index)).special = false := by unfold Pinned.dotStep rw [if_neg (by push_neg; exact h)] simp only [Pinned.Acc.add] split_ifs <;> rfl generalize Pinned.dotStep ⟨pos, neg, false, nz⟩ (fa index) (fb index) = acc at hstep obtain ⟨p, n, sp, z⟩ := acc simp only at hstep subst hstep exact dotLoop_special_false fa fb count (index + 1) p n z (fun k h1 h2 => hfin k (by omega) (by omega)) theorem dotFn_finite (n : Nat) (fa fb : Nat → UInt32) (hfin : ∀ k, k < n → expOf (fa k) ≠ 255 ∧ expOf (fb k) ≠ 255) : Pinned.dotFn n fa fb = finishWord (dsum (Array.ofFn (n := n) fun i => fa i) (Array.ofFn (n := n) fun i => fb i) 0 n) (-298) (n ≠ 0 && dallNZ (Array.ofFn (n := n) fun i => fa i) (Array.ofFn (n := n) fun i => fb i) 0 n) := by unfold Pinned.dotFn have hsp := dotLoop_special_false fa fb n 0 (Array.replicate 18 0) (Array.replicate 18 0) true (fun k _ hk => hfin k (by omega)) obtain ⟨-, -, hD, hz⟩ := Pinned.dotLoopFacts fa fb (Array.ofFn (n := n) fun i => fa i) (Array.ofFn (n := n) fun i => fb i) n (Pinned.getElem!_ofFn n fa) (Pinned.getElem!_ofFn n fb) Pinned.Acc.empty 0 n (by omega) (by simp [Pinned.Acc.empty]) (by simp [Pinned.Acc.empty]) hsp simp only [Pinned.Acc.empty] at hD hz hsp simp only [hsp, Bool.false_eq_true, ite_false] rw [Pinned.finishFast_eq] change finishWord (Pinned.Acc.total _) _ _ = _ have h0 : (⟨Array.replicate 18 0, Array.replicate 18 0, false, true⟩ : Pinned.Acc).total = 0 := Pinned.Acc.total_empty rw [hD, hz, h0] simp @[inline] def dotWin (n : Nat) (fa fb : Nat → UInt32) : Option UInt32 := match maxExp fa fb 0 0 n with | none => none | some E => if 600 < E ∨ 12 < n.log2 then none else let c := 13 - n.log2 let Ec := E - c let pn := sumWin64 fa fb Ec.toUInt64 0 0 0 n let P := pn.1.toNat let N := pn.2.toNat let neg := decide (P < N) let D := if neg then N - P else P - N if D ≤ n then none else let ex : Int := (Ec : Int) - 298 let w := FastRound.roundW neg (D - n) ex if w = FastRound.roundW neg (D + n) ex ∧ ((D + n).log2 : Int) + ex ≤ 126 ∧ expOf w ≠ 255 ∧ (decodeD w).significand ≠ 0 then some w else none theorem two_pow_127_le_posMax : (2 : ℝ) ^ (127 : Int) ≤ Model.toReal (Model.posMaxFinite Fmt) := by rw [Model.toReal_posMaxFinite] have h1 : Fmt.fracWidth = 23 := rfl have h2 : Fmt.maxNormalExponent = 127 := rfl have h3 : Fmt.maxFiniteFracField = 2 ^ 23 - 1 := rfl have hp : Model.pow2 23 = 2 ^ 23 := by simp [Model.pow2, Nat.shiftLeft_eq] rw [h1, h2, h3, hp] simp [FloatLib.Floats.Formats.Flocq.bpow, FloatLib.Numerics.binaryRadix, FloatLib.Numerics.Radix.toReal] norm_num theorem scale_ex (X : Int) (Ec : Nat) : (X : ℝ) * 2 ^ ((Ec : Int) - 298) = ((X * 2 ^ Ec : Int) : ℝ) * 2 ^ (-298 : Int) := by rw [zpow_sub₀ two_ne_zero, zpow_neg, zpow_natCast]; push_cast; ring theorem scale_le {X Y : Int} (h : X ≤ Y) : (X : ℝ) * 2 ^ (-298 : Int) ≤ (Y : ℝ) * 2 ^ (-298 : Int) := mul_le_mul_of_nonneg_right (by exact_mod_cast h) (by positivity) theorem dotWin_spec {n : Nat} {fa fb : Nat → UInt32} {w : UInt32} (h : dotWin n fa fb = some w) : Pinned.dotFn n fa fb = w := by unfold dotWin at h split at h · simp at h rename_i E hE split at h · simp at h rename_i hg push_neg at hg dsimp only at h obtain ⟨-, hall⟩ := maxExp_spec fa fb n 0 0 E hE have hfin : ∀ k, k < n → expOf (fa k) ≠ 255 ∧ expOf (fb k) ≠ 255 := fun k hk => ⟨(hall k (by omega) (by omega)).1, (hall k (by omega) (by omega)).2.1⟩ rw [dotFn_finite n fa fb hfin] set c := 13 - n.log2 with hc set Ec := E - c with hEc have hn2 : n < 2 ^ (n.log2 + 1) := Nat.lt_log2_self have hbound : (0 : UInt64).toNat + (0 : UInt64).toNat + n * 2 ^ (48 + c) < 2 ^ 64 := by have : n * 2 ^ (48 + c) < 2 ^ (n.log2 + 1) * 2 ^ (48 + c) := Nat.mul_lt_mul_of_pos_right hn2 (Nat.two_pow_pos _) have h62 : 2 ^ (n.log2 + 1) * 2 ^ (48 + c) = 2 ^ 62 := by rw [← pow_add]; congr 1; omega simp; omega obtain ⟨hP, hN⟩ := sumWin64_eq fa fb Ec c (by omega) (by omega) n 0 0 0 (fun k _ hk => by have := (hall k (by omega) hk).2.2; omega) hbound simp only [UInt64.toNat_zero, Nat.zero_add] at hP hN rw [hP, hN] at h set A := Array.ofFn (n := n) fun i => fa i set B := Array.ofFn (n := n) fun i => fb i obtain ⟨b1, b2⟩ := sumNat_bounds fa fb A B n Ec (Pinned.getElem!_ofFn n fa) (Pinned.getElem!_ofFn n fb) n 0 (by omega) set T := dsum A B 0 n set Pn := (sumNat fa fb Ec 0 n).1 set Nn := (sumNat fa fb Ec 0 n).2 have hpos : (0 : Int) < 2 ^ Ec := by positivity set ex : Int := (Ec : Int) - 298 with hex set v : ℝ := (T : ℝ) * 2 ^ (-298 : Int) have hrepr : (ofIntDyadic T (-298)).toReal = v := by rw [← FloatLib.Numerics.Dyadic.cast_toRat, toRat_ofIntDyadic]; push_cast; rfl have habs : ∀ M : Nat, M.log2 + ex ≤ 126 → (M : ℝ) * 2 ^ ex ≤ 2 ^ (127 : Int) := by intro M hl have hlt : M < 2 ^ (M.log2 + 1) := Nat.lt_log2_self have : (M : ℝ) ≤ (2 : ℝ) ^ ((M.log2 + 1 : Nat) : Int) := by rw [zpow_natCast]; exact_mod_cast hlt.le calc (M : ℝ) * 2 ^ ex ≤ 2 ^ ((M.log2 + 1 : Nat) : Int) * 2 ^ ex := mul_le_mul_of_nonneg_right this (by positivity) _ = 2 ^ (((M.log2 + 1 : Nat) : Int) + ex) := by rw [zpow_add₀ two_ne_zero] _ ≤ 2 ^ (127 : Int) := zpow_le_zpow_right₀ (by norm_num) (by push_cast; omega) have hfinish : ∀ (lo hi : Int) (M : Nat), lo ≠ 0 → hi ≠ 0 → finishWord lo ex false = w → finishWord hi ex false = w → lo * 2 ^ Ec ≤ T → T ≤ hi * 2 ^ Ec → -(M : Int) ≤ lo → hi ≤ M → M.log2 + ex ≤ 126 → expOf w ≠ 255 → (decodeD w).significand ≠ 0 → T ≠ 0 → finishWord T (-298) (n ≠ 0 && dallNZ A B 0 n) = w := by intro lo hi M hlo hhi f1 f2 l1 l2 m1 m2 hM g1 g2 hT have hv_lo : (lo : ℝ) * 2 ^ ex ≤ v := by rw [hex, scale_ex]; exact scale_le l1 have hv_hi : v ≤ (hi : ℝ) * 2 ^ ex := by rw [hex, scale_ex]; exact scale_le l2 have hp : (0 : ℝ) < 2 ^ ex := by positivity have m1' : -((M : ℝ) * 2 ^ ex) ≤ (lo : ℝ) * 2 ^ ex := by rw [← neg_mul]; exact mul_le_mul_of_nonneg_right (by exact_mod_cast m1) hp.le have m2' : (hi : ℝ) * 2 ^ ex ≤ (M : ℝ) * 2 ^ ex := mul_le_mul_of_nonneg_right (by exact_mod_cast m2) hp.le have hvb : |v| ≤ 2 ^ (127 : Int) := (abs_le.mpr ⟨m1'.trans hv_lo, hv_hi.trans m2'⟩).trans (habs M hM) have hzfin : Model.isFinite (Model.roundDyadic Fmt (ofIntDyadic T (-298))) = true := Model.isFinite_roundDyadic_of_isIEEE_of_abs_toReal_le_posMaxFinite Fmt (by decide) _ (by rw [hrepr]; exact hvb.trans two_pow_127_le_posMax) have hz : Model.toReal (Model.roundDyadic Fmt (ofIntDyadic T (-298))) = Model.roundAt Fmt v := by rw [Model.toReal_roundDyadic_eq_roundAt Fmt (by decide) _ hzfin, hrepr] have := FastRound.bracket_spec hlo hhi f1 f2 g1 g2 hv_lo hv_hi hz simp only [finishWord, hT, ite_false] exact this by_cases hneg : Pn < Nn · simp only [hneg, decide_true, ite_true] at h split at h · simp at h rename_i hDn split at h · rename_i hc simp only [Option.some.injEq] at h subst h obtain ⟨hw2, hlog, hfw, hsg⟩ := hc have hD : ((Nn - Pn : Nat) : Int) = Nn - Pn := by omega apply hfinish (-((Nn - Pn + n : Nat) : Int)) (-((Nn - Pn - n : Nat) : Int)) (Nn - Pn + n) (by omega) (by omega) · rw [hw2, FastRound.roundW_signed true _ _ (by omega)]; simp · rw [FastRound.roundW_signed true _ _ (by omega)]; simp · push_cast; rw [Nat.cast_sub (by omega)]; push_cast; nlinarith · push_cast; rw [Nat.cast_sub (by omega)]; push_cast; nlinarith · omega · omega · exact hlog · exact hfw · exact hsg · intro h0 have : T ≤ ((Pn : Int) - Nn + n) * 2 ^ Ec := b2 have hp' : (Pn : Int) - Nn + n < 0 := by omega nlinarith [mul_neg_of_neg_of_pos hp' hpos] · simp at h · simp only [hneg, decide_false, Bool.false_eq_true, ite_false] at h split at h · simp at h rename_i hDn split at h · rename_i hc simp only [Option.some.injEq] at h subst h obtain ⟨hw2, hlog, hfw, hsg⟩ := hc apply hfinish ((Pn - Nn - n : Nat) : Int) ((Pn - Nn + n : Nat) : Int) (Pn - Nn + n) (by omega) (by omega) · rw [FastRound.roundW_signed false _ _ (by omega)]; simp · rw [hw2, FastRound.roundW_signed false _ _ (by omega)]; simp · rw [Nat.cast_sub (by omega), Nat.cast_sub (by omega)]; nlinarith · push_cast; rw [Nat.cast_sub (by omega)]; nlinarith · omega · omega · exact hlog · exact hfw · exact hsg · intro h0 have : ((Pn : Int) - Nn - n) * 2 ^ Ec ≤ T := b1 have hp' : (0 : Int) < (Pn : Int) - Nn - n := by omega nlinarith [mul_pos hp' hpos] · simp at h @[inline] def dotW (n : Nat) (fa fb : Nat → UInt32) : UInt32 := (dotWin n fa fb).getD (Pinned.dotFn n fa fb) theorem dotW_eq : dotW = Pinned.dotFn := by funext n fa fb unfold dotW cases h : dotWin n fa fb with | none => rfl | some w => exact (dotWin_spec h).symm @[inline] def dotSel (n : Nat) (fa fb : Nat → UInt32) : UInt32 := if n ≤ 2 then Pinned.dotFn n fa fb else dotW n fa fb theorem dotSel_eq : dotSel = Pinned.dotFn := by funext n fa fb unfold dotSel split <;> simp [dotW_eq] @[specialize] def softmaxExp (dot : DotFn) (ex : Word → Word) (rows n : Nat) (x : Array Word) : Array Word := let mx := Array.ofFn (n := rows) fun r => rowMax n x r.val let e := Array.ofFn (n := rows * n) fun q => ex (toWord (Model.sub (ofW x[q.val]!) (ofW mx[q.val / n]!))) let s := Array.ofFn (n := rows) fun r => dot n (fun t => e[r.val * n + t]!) (fun _ => oneW) Array.ofFn (n := rows * n) fun q => toWord (Model.div (ofW e[q.val]!) (ofW s[q.val / n]!)) theorem softmaxExp_expW (dot : DotFn) : softmaxExp dot expW = softmaxWith dot := rfl def siluF (x : Array Word) : Array Word := x.map fun w => toWord (Model.mul (ofW w) (ofW (FastAct.sigmoidF w))) theorem siluF_eq : siluF = siluSpec := by funext x simp only [siluF, siluSpec, FastAct.sigmoidF_eq] def pointwiseConv (s : ConvShape) (relu : Bool) (inp wts b : Array Word) : Array Word := if s.kh = 1 ∧ s.kw = 1 ∧ s.strideH = 1 ∧ s.strideW = 1 ∧ s.padT = 0 ∧ s.padL = 0 ∧ s.padB = 0 ∧ s.padR = 0 ∧ s.dilH = 1 ∧ s.dilW = 1 ∧ s.groups = 1 then Array.ofFn (n := s.cout * (s.ho * s.wo)) fun q => let o := q.val / (s.ho * s.wo) let y := q.val / s.wo % s.ho let x := q.val % s.wo act relu <| dotSel (s.cin + 1) (fun t => if t < s.cin then if y >= s.h ∨ x >= s.w then 0 else inp[(t * s.h + y) * s.w + x]! else oneW) (fun t => if t < s.cin then wts[o * s.cin + t]! else b[o]!) else conv2dWith Pinned.dotFn s relu inp wts b theorem pointwiseConv_eq : pointwiseConv = conv2dWith Pinned.dotFn := by funext s relu inp wts b unfold pointwiseConv split_ifs with h · rcases h with ⟨hkh, hkw, hsh, hsw, hpt, hpl, hpb, hpr, hdh, hdw, hgrp⟩ have htaps : s.taps = s.cin := by simp [ConvShape.taps, ConvShape.cpg, hgrp, hkh, hkw] have hopg : s.opg = s.cout := by simp [ConvShape.opg, hgrp] apply Array.ext (by simp [conv2dWith, ConvShape.taps, ConvShape.cpg, hgrp, hkh, hkw]) intro q hq1 hq2 have hp : 0 < s.ho * s.wo := by have hh : 0 < s.ho := by simp [ConvShape.ho] have hw : 0 < s.wo := by simp [ConvShape.wo] exact Nat.mul_pos hh hw have hq : q < s.cout * (s.ho * s.wo) := by simpa [conv2dWith, ConvShape.taps, ConvShape.cpg, hgrp, hkh, hkw] using hq1 have hqout : q / (s.ho * s.wo) < s.cout := (Nat.div_lt_iff_lt_mul hp).2 hq have hgroup : q / (s.ho * s.wo) / s.cout = 0 := Nat.div_eq_of_lt hqout simp [conv2dWith, windowAt, hkh, hkw, hsh, hsw, hpt, hpl, hpb, hpr, hdh, hdw, ConvShape.cpg, hgrp, htaps, hopg, hgroup, Nat.mod_one, dotSel_eq] · simpa only [dotSel_eq] def convFast (s : ConvShape) (relu : Bool) (inp wts b : Array Word) : Array Word := if 0 < s.cin ∧ s.groups = s.cin ∧ s.cout = s.cin then Array.ofFn (n := s.cout * (s.ho * s.wo)) fun q => let o := q.val / (s.ho * s.wo) let y := q.val / s.wo % s.ho let x := q.val % s.wo act relu <| Pinned.dotFn (s.taps + 1) (fun t => if t < s.taps then windowAt s inp o y x t else oneW) (fun t => if t < s.taps then wts[o * s.taps + t]! else b[o]!) else pointwiseConv s relu inp wts b theorem convFast_eq : convFast = conv2dWith Pinned.dotFn := by funext s relu inp wts b unfold convFast split_ifs with h · rcases h with ⟨hcin, hgroups, hcout⟩ have hcpg : s.cpg = 1 := by simp [ConvShape.cpg, hgroups, Nat.div_self hcin] have hopg : s.opg = 1 := by simp [ConvShape.opg, hcout, hgroups, Nat.div_self hcin] apply Array.ext (by simp [conv2dWith]) intro q hq1 hq2 simp [conv2dWith, hopg, dotSel_eq] · simpa only [pointwiseConv_eq, dotSel_eq] def kernels : Kernels := { Pinned.kernels with conv := { Pinned.kernels.conv with conv2d := convFast } attn := ⟨scoresWith dotSel, mixWith dotSel, softmaxExp dotSel FastAct.expF, siluF⟩ rnn := ⟨lstmWith Pinned.dotFn FastAct.sigmoidF FastAct.tanhF, gruWith Pinned.dotFn FastAct.sigmoidF FastAct.tanhF⟩ } theorem correct : Obligation kernels := by have h := Pinned.correct simp only [Obligation, Pinned.kernels] at h simp only [Obligation, kernels, Pinned.kernels, siluF_eq, FastAct.sigmoidF_eq, FastAct.tanhF_eq, FastAct.expF_eq, softmaxExp_expW, dotSel_eq, convFast_eq, Pinned.dotFn_eq_dotOf] rw [← h] simp only [specAttn, specRnn, scoresSpec, mixSpec, softmaxSpec, siluSpec, lstmSpec, gruSpec, Pinned.dotFn_eq_dotOf] end I open ExactRuntime FloatLib.Floats.Formats.BinaryInterchange FloatLib.Floats open USize renaming lt_iff_toNat_lt→γ,le_size→ς,toNat_lt_size→Τ,size_eq_two_pow→Ϟ,toNat_zero→Ϥ,le_refl→Ϭ open Nat renaming and_two_pow_sub_one_eq_mod→θ,shiftRight_eq_div_pow→ι,mod_eq_of_lt→ξ,pow_le_pow_right→Ε,mul_le_mul_right→Ζ,shiftLeft_eq→Μ,succ_mul→ϋ,two_pow_add_eq_or_of_lt→ϓ,add_comm→ϔ,and_le_right→ϙ,toUSize_eq→ϛ,div_eq_of_lt→ϣ,add_sub_cancel_left→ϥ,le_log2→Ϧ,mul_comm→ϩ,add_zero→Ϫ,one_shiftLeft→ϭ,mul_one→ϱ,div_lt_of_lt_mul→ϲ,mod_lt→ϳ,add_mul_mod_self_right→ϵ,lt_log2_self→Ϸ open UInt64 renaming le_iff_toNat_le→κ,toNat_add→μ,lt_iff_toNat_lt→ν,toNat_sub_of_le→χ,toNat_and→ψ,toNat_shiftRight→Α,toNat_inj→Β,toNat_shiftLeft→Ι,toNat_sub→Κ,toNat_ofNat_of_lt'→Ξ,toNat_mul→Ϛ,toNat_toUInt32→ϟ,toNat_zero→Ϯ open Bool renaming false_eq_true→ο,and_eq_true→υ,eq_iff_iff→ϻ open UInt32 renaming toNat_inj→Η,toNat_and→Λ,toNat_shiftRight→Ρ,toNat_toUInt64→Χ,lt_iff_toNat_lt→ϖ open Model renaming toModel_ofFloatModel→Θ,isFinite_roundDyadic_of_isIEEE_of_abs_toReal_le_posMaxFinite→Υ,toReal_eq_unpackedToReal_toModel→ό,toDyadic?_ofFields_of_isFinite→ϒ,toReal_roundDyadic_eq_roundAt→ϗ,toDyadic?_isSome_eq_isFinite→Ϝ,abs_signed_mul_bpow_le_toReal_posMaxFinite→Ϡ,ofFloatModel_pack→Ϣ,toDyadic?_ieee_eq_model→ϧ,roundDyadicGeneral_eq_roundDyadic→ϰ,roundedMantissa_shift_quotient→Ϻ open Finset renaming mem_range→Ν,sum_congr→Ο,sum_le_sum→Ϗ,sum_Ico_succ_top→ϐ,sum_range_succ→ϝ,sum_nonneg→ϡ,sum_add_distrib→ϫ,card_range→ϯ,sum_mul→϶,sum_le_sum_of_subset_of_nonneg→ϸ,abs_sum_le_sum_abs→Ϲ open Real renaming sqrt_nonneg→ϊ open Float.Model.UnpackedFloat renaming unpackExponent_packComponents→ύ,unpackMantissa_packComponents→ώ open Array renaming size_uset→ϑ,getElem_ofFn→Ϩ,size_replicate→ϴ open Int renaming cast_abs→ϕ open FloatLib.Numerics.Dyadic renaming cast_toRat→Ϙ local notation "А" => by omega local notation "Б" => by decide local notation "В" => by positivity local notation "Г" => by norm_num local notation "Д" => UInt64 local notation "Е" => UInt32 local postfix:max "а"=>UInt64.toNat local postfix:max "б"=>USize.toNat local postfix:max "в"=>Array.size local postfix:max "г"=>Nat.toUSize local postfix:max "д"=>FloatArray.size local postfix:max "е"=>UInt32.toNat local postfix:max "ж"=>Nat.toUInt64 local postfix:max "з"=>Nat.log2 local postfix:max "и"=>Fin.val local postfix:max "й"=>Int.toNat local postfix:max "к"=>UInt32.toUInt64 local postfix:max "л"=>UInt64.toUInt32 local postfix:max "м"=>Int.natAbs local postfix:max "н"=>Int64.toInt open UInt64 renaming reduceToNat→iZ,toNat→jI,size→jT,toNat_or→kp,toUInt32→kr,toNat_one→kW,toNat_toBitVec→ll,ofNat→lP open Finset renaming range→i0,Ico→jr,sum_range_succ'→jY,sum_sub_distrib→j9,sum_const→kg,sum_Ico_eq_sum_range→kz,mul_sum→kJ open FloatLib.Floats.Formats.BinaryInterchange.FloatFormat renaming binary64→i5 open FloatLib.Floats.Formats.BinaryInterchange.Model renaming ofFloatModel→i6,roundDyadic→i8,unpackedToReal→jp,toReal→jJ,toReal_eq→jK,roundDyadic_of_representable→jO,roundAt_mono→jP,unpackedToDyadic?→jU,isFinite→jW,unpackSign_packComponents→kb,roundAt→kh,toModel→ki,toReal_add_eq_roundAt→kx,posMaxFinite→kG,pow2_eq_two_pow→ln,ofUInt32→ls,ofFloat32Model→ly,add→lB,ofModel→lH,modelSignBit→lL open ExactRuntime renaming expOf→i7,Word→i9,idxOf→je,rowVariance→jg,stableNormDomain→ji,sqrtRational→jk,rowMean→jo,signOf→jw,mantOf→jF,toWord→jH,layernormStable→jN,finiteWord→jS,oneW→kf,rmsnormStable→kj,mantOf_lt_24→kw,dotOf→kB,finishWord→kC,isFinite_ofUInt32→kM,ofIntDyadic→kN,finishWord_of_ne→kV,Fmt→lr,layernormSpec→lJ,fracOf→lW open Real renaming sqrt→ja,sq_sqrt→lb,le_sqrt_of_sq_le→lq,sqrt_mul→lI,sqrt_sq→lU open Nat renaming reduceMod→jb,toUInt64_eq→jL,testBit_eq_decide_div_mod_eq→jZ,cast_ofNat→j0,zero_add→j6,add_mul_div_right→kc,le_div_iff_mul_le→kd,zero_le→km,add_mul→ko,cast_natAbs→ku,pos_of_ne_zero→kD,and_one_is_mod→kF,lt_of_lt_of_le→kH,cast_zero→kS,log2_self_le→kU,le_mul_of_pos_right→kX,cast_sub→k9,zero_mul→la,and_two_pow→lc,two_pow_pos→ld,cast_nonneg→lj,div_add_mod→lk,log2_lt→lu,pow_lt_pow_right→lz,log2_eq_log_two→lC,mod_le→lK,cast_one→lQ,abs_cast→lS,one_mul→l0 open Float.Model.UnpackedFloat renaming unpack→jc,abs→jm,isFinite→jn,mul→jq,pack→jA,packedInfinity→jG,accuracyOfFraction→jQ,roundWithAccuracy→kR,unpackExponent→lp,packedZero→lD,round→lG,Sign→lR open USize renaming reduceToNat→jd,size→ke,toNat_add→ks,toNat_one→lf,toNat_mul→li open FloatLib.Numerics renaming Dyadic→jf,binaryRadix→jh,shiftRightJam→jx,roundShiftRightEven_shiftRightJam→jV,roundQuotientEven→kQ open UInt32 renaming reduceToNat→jj,toNat_zero→j5 open Float.Model renaming totalExponent→jl,pack→kY,sqrt→lZ,add→l4,mul→l5,sub→l7 open FloatLib.Numerics.Dyadic renaming ofScaledInt→js,toReal→jz,signedSignificand→jC,cast_signedSignificand→kP,toRat_eq_zero_iff→kZ,ofScaledInt_toRat→k8,toRat→lX open Float.Model.Format renaming binary64→jt,binary32→ju open Array renaming ofFn→jv,replicate→jM,all_eq_true→j8,usize→kk,getElem?_eq_getElem→kL,size_set→lA,setIfInBounds→lE,getElem?_ofFn→lF,getElem?_set→lM,ext_getElem?→lN,uset_eq_set→lT,getElem_set→lV,set!→l8,uset→l9 open FloatLib.Numerics.FixedWord renaming roundShiftRightEven→jy open Float.Model.UnpackedFloat.ExtendedMantissa renaming shiftRightOne→jB open FloatArray renaming size→jD,emptyWithCapacity→jE,set!→kt,uget→lh,usize→lY,uset→l6 open FloatLib.Floats.Formats.Flocq renaming bpow→jR open FloatLib.Numerics.RationalBinary renaming scaleByPowerOfTwo→j7 open FloatLib.Floats.ExecFloat.Binary renaming toModel_ofFloat_int64ToFloat→ka open Int renaming ofNat_eq_natCast→kl,toNat_of_nonneg→kv,log→ky,lt_zpow_succ_log_self→kK,abs_eq_natAbs→kO,zpow_log_le_self→lv open FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Semantics renaming finiteDot_toList_eq_slice→kA open BitVec renaming toInt_eq_toNat_cond→kE open Float32 renaming ofBits→kI open FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal renaming dotState_exact_toRat→kT,dotState→lO open Bool renaming or_eq_true→lg open Max renaming max→lm open FloatLib.Floats.Formats.Flocq.bpow renaming pos→lx open Or renaming inr→ma local notation "о"=>Nat local notation "п"=>Int local notation "р"=>Float local notation "с"=>USize local notation "т"=>Word local notation "у"=>Array local notation "ф"=>Bool section open FloatLib.Numerics lemma aD (s:ф) (m:о) (e:п) (j:о) (h:j+25<= mз): i8 lr ⟨s,jx m j,e+j⟩=i8 lr ⟨s,m,e⟩:=by have g:m≠0:=by rintro rfl;simp at h have o:2^mз<= m:=kU g;have u:2^(j+1)<= m:=le_trans (Ε Г А) o;have d:(jx m j)з=mз-j:=log2_shiftRightJam m j have t:jx m j≠0:= shiftRightJam_ne_zero m j (le_trans (Ε Г А) u) rw[<- ϰ,<- ϰ];unfold Model.roundDyadicGeneral;simp only[t,g,beq_iff_eq,ite_false,d];have q:((mз-j:о):п)+(e+j)=(mз:п)+e:=А;rw[q];have r:Fmt.fracWidth=23:=rfl;have p:Fmt.minSubnormalExponent=-149:=rfl;have l:Fmt.minNormalExponent=-126:=rfl;rw[r,p,l];split_ifs with h1 h2 h3 h4<;>try omega .rfl .congr 1 obtain ⟨a,v⟩:∃a:о,e- -149=Int.negSucc a:=⟨(-(e+149)-1)й,by omega⟩ have w:e+j- -149=Int.negSucc (a-j):=А;rw[v,w];dsimp only;rw[show a-j+1=(a+1)-j by omega] exact jV m j (a+1) А .congr 1 rw[show mз-j-23=(mз-23)-j by omega] exact jV m j _ А end lemma ae (n:о) (f:о-> Е) (k:о) (d:kf iи)[k]! =f k:=by rw[getElem!_pos _ k (by simpa using d),Ϩ] namespace Core def tm (a b:т):п:=sv a*sv b*2^(idxOf a+idxOf b) def ah (n:о) (fa fb:о-> т):п:=∑k∈Finset.range n,tm (fa k) (fb k) def am (n:о) (fa fb:о-> т):Prop:=∀k,k expOf (fa k)≠255/\expOf (fb k)≠255 lemma aE (n:о) (d e:о-> i9): ah (n+1) d e=ah n d e+tm (d n) (e n):=ϝ _ _ lemma aU (n:о) (m o:о-> i9) (l:am n m o): kB n m o=kC (ah n m o) (-298) (decide (n≠0)&& dallNZ (jv (n:=n) λi=>m iи) (jv (n:=n) λi=>o iи) 0 n):=by unfold kB dotSpec;set A:=jv (n:=n) λi=>m iи set B:=jv (n:=n) λi=>o iи set L:=A.map (ls (fmt:=lr));set R:=B.map (ls (fmt:=lr));have j:Lв=Rв:=by simp[L,R,A,B] have e:∀k (h:kby simp[L,A,kM] at h⊢;exact (l k h).1 have g:∀k (h:kby simp[R,B,kM] at h⊢;exact (l k h).2 have p:∀k,0<= k-> k<0+Lв-> i7 A[k]!≠255/\i7 B[k]!≠255:=λk _ h=>by simp[L,A] at h;simp only[A,B,ae n _ k h];exact l k h have v:∀i c,dsum A B i c=∑k∈i0 c,tm A[i+k]! B[i+k]!:=λi c=>by induction c generalizing i with | zero=>simp[dsum] | succ c w=> rw[dsum,w (i+1),jY,add_comm];exact congrArg₂ _ (Ο rfl λk _=>by rw[show i+1+k=i+(k+1) by omega]) rfl have d:=(finiteDotSlice_eq A B 0 Lв (by simp[L]) (by simp[j,R]) p).trans (c:=(ah n m o:ℚ)*2^(-298:ℤ)) (by simp only[v,ah,L,A,B,Array.size_map,Array.size_ofFn];congr 2;exact Ο rfl λk p=>by simp at p;simp[ae n _ k p]) have r:=kT (destination:=lr) L R j rw[<- Model.Reduction.map_value_dot] by_cases q:ah n m o=0 .have hz0:(Model.Reduction.Internal.dotState L R j:Model.Reduction.Internal.State lr).exact.significand=0:=by rw[<- kZ,r,d,q];simp rw[Model.Reduction.dot_status_eq_zero_of_finite lr L R .nearest j e g hz0,q,finishWord_zero] unfold lO obtain ⟨t,u⟩:=dotStateLoop_flags A B {} 0 Lв (by simp[L]) (by simp[j,R]) p simp only[Except.map];rw[t,u];simp[L,A] .have hnz:Model.Reduction.Semantics.finiteDot L.toList R.toList≠.ok 0:=by rw[kA L R j];intro h;injection h with h;rw[d] at h;simp at h;exact q h rw[Model.Reduction.dot_status_eq_round_of_finite_nonzero lr L R .nearest j e g hnz] simp only[Except.map] exact (kV _ (ah n m o) (-298) _ q (by rw[r,d])).symm lemma a9 (n:о) (d e:о-> i9) (g:am n d e) (h:ah n d e≠0): kB n d e=kC (ah n d e) (-298) false:=by simp[aU n d e g,kC,h] @[inline] def dq (w:Е):Д:=if (w>>>23)&&&0xFF!=0 then 1 else 0 @[inline] def mW (w:Е):Д:=(w&&&0x7FFFFF)к ||| (dq w<<<23) @[inline] def iW (w:Е):Д:=((w>>>23)&&&0xFF)к-dq w def bi (x:Д):п:=x.toBitVec.toInt lemma aN (w:Е):(mW w)а=jF w:=by have e:(w&&&0x7FFFFF)е<2^23:=by rw[Λ];exact lt_of_le_of_lt ϙ Б unfold mW dq jF i7 lW;by_cases d:(w>>>23)&&&0xFF=0 .simp[d] .simp only[show ((w>>>23)&&&0xFF!=0)=true by simpa using d,d,ite_true,ite_false] rw[kp,Χ,show ((1:Д)<<<23)а=2^23*1 from rfl,Nat.or_comm, <- ϓ e,ϱ,ϔ] lemma bf (w:Е):(iW w)а=je w:=by unfold iW dq je i7;have g:=expOf_toNat_lt w;unfold i7 at g;by_cases e:(w>>>23)&&&0xFF=0 .simp[e] .have d:1<=((w>>>23)&&&0xFF)е:= Nat.one_le_iff_ne_zero.2 λh=>e (Η.mp (by simpa using h)) simp only[show ((w>>>23)&&&0xFF!=0)=true by simpa using e,e,ite_true,ite_false] rw[χ _ _ (κ.mpr (by rw[Χ];simpa using d)), Χ] rfl lemma aP (w:Е):jw w=true↔2^31<= wе:=by have:=w.toNat_lt rw[jw,bne_iff_ne,ne_eq,<- Η,Λ,show (0x80000000:Е)е=2^31 from rfl, lc,jZ] by_cases h:wе/2^31%2=1<;>simp[h]<;>omega @[inline] def sx (k x:Д):Д:=bif x>>>k==0 then x else x>>>k @[inline] def sr (k x r:Д):Д:=bif x>>>k==0 then r else r+k @[inline] def an (x0:Д):Д:= let x1:=sx 32 x0 let r1:=sr 32 x0 0 let x2:=sx 16 x1 let r2:=sr 16 x1 r1 let x3:=sx 8 x2 let r3:=sr 8 x2 r2 let x4:=sx 4 x3 let r4:=sr 4 x3 r3 let x5:=sx 2 x4 let r5:=sr 2 x4 r4 sr 1 x5 r5 @[inline] def cq (value shift:Д):Д:= let quotient:=value>>>shift let remainder:=value&&&((1<<half then 1 else 0) @[inline] def aJ (value shift:Д):Д:= if shift==0 then value else if shift<64 then cq value shift else if shift==64 then (if value>0x8000000000000000 then 1 else 0) else 0 @[inline] def cd (sign:ф) (e f:Е):Е:= (if sign then (0x80000000:Е) else 0) ||| ((e&&&0xff)<<<23) ||| (f&&&0x007fffff) @[inline] def cj (n:Д):Е:= (if n<0x800000 then 0 else n-0x800000)л @[inline] def aC (sign:ф) (product scale:Д):Е:= if product==0 then if sign then 0x80000000 else 0 else let leading:=an product let position:=leading+scale if position<172 then let fraction:= if scale<149 then aJ product (149-scale) else product<<<(scale-149) if fraction==0 then (if sign then 0x80000000 else 0) else if fraction==0x800000 then cd sign 1 0 else cd sign 0 fractionл else let roundedMantissa:= if leading<23 then product<<<(23-leading) else aJ product (leading-23) let carry:=roundedMantissa==0x1000000 let normalizedPosition:=if carry then position+1 else position if normalizedPosition>425 then (if sign then 0xff800000 else 0x7f800000) else let normalizedMantissa:=if carry then 0x800000 else roundedMantissa cd sign (normalizedPosition-171)л (cj normalizedMantissa) open Model.NativeBinary32 in lemma cn (n k:о) (h:n>>>k≠0):nз=k+(n>>>k)з:=by rw[ι] at* have:=(Ϧ (by rintro rfl;simp at h)).2 (Nat.div_pos_iff.1 (kD h)).2 rw[lC,lC,Nat.log_div_base_pow] at*;omega lemma bs (e r x k:Д) (o:kа<=32) (l:0simp[h,lu,e.toNat_lt] have g:kа%64=kа:=ξ А;unfold sx sr;by_cases j:x>>>k=0<;>simp[j,g,d] .simpa[g,ι,Nat.div_eq_zero_iff] using congrArg jI j have:=cn xа kа (by simpa[<- Β,g] using j) refine ⟨by omega,?_⟩ rw[ι];exact ϲ (by rwa[<- Nat.pow_add,show kа+kа=2*kа by omega]) lemma aG (x:Д):an x=x.log2:=by apply Β.mp;obtain ⟨o,e⟩:=bs x 0 x 32 Б Б (by simp) x.toNat_lt obtain ⟨p,g⟩:=bs x _ _ 16 Б Б o e;obtain ⟨q,h⟩:=bs x _ _ 8 Б Б p g;obtain ⟨r,j⟩:=bs x _ _ 4 Б Б q h;obtain ⟨t,l⟩:=bs x _ _ 2 Б Б r j;obtain ⟨d,m⟩:=bs x _ _ 1 Б Б t l;rw[Nat.log2_def (sx 1 _)а,if_neg (by simpa using m)] at d unfold an;exact d.symm lemma cF (e d:Д): aJ e d=jy e dа:=by unfold aJ jy;by_cases g:d=0 .subst g;rfl have:=d.toNat_lt;have h:dа≠0:=by simpa[<- Β] using g simp only[g,h,beq_iff_eq,UInt64.ofNat_toNat,ν,↓reduceIte, show lP (dа-1)=d-1 from Β.mp (by simp[Κ];omega), show d=64↔dа=64 by rw[<- Β];rfl] refine ite_congr rfl (λj=>?_) λ_=>rfl have:(e&&&((1<<simp[κ, ξ j,ϭ,ξ (by omega:2^d.toNat<18446744073709551616),Nat.one_le_two_pow] exact (ϳ _ (ld _)).trans_le l have:((e>>>d)&&&1)а<=1:=by simp[ψ];omega have:=(e>>>d).toNat_lt simp only[cq,gt_iff_lt,ν,μ,beq_iff_eq,<- Β, apply_ite jI,kW,iZ] generalize (e&&&((1<<>>d)&&&1)а=b at* split_ifs<;>omega lemma bQ (n:Д):cj n=UInt32.ofNat (nа-0x800000):=by unfold cj;split<;>simp_all[kr,Nat.toUInt32,ν,χ,κ,Nat.sub_eq_zero_of_le,le_of_lt] open Model.NativeBinary32 in lemma bH (w:Е):jH (ofUInt32 w)=w:=by conv_rhs=>rw[<- toUInt32_ofUInt32 w] exact Η.mp (ξ (BitVec.isLt _)) open Model.NativeBinary32 in lemma ax (e:ф) (m d:Д) (g:dа<=506): aC e m d=jH (i8 lr ⟨e,mа,(dа:п)-298⟩):=by erw[<- ofUInt32_roundDyadic,bH,<- roundProduct_eq_roundDyadic _ _ _ g];unfold aC roundProduct cd mkBits;simp only[aG,cF,bQ,kr,Nat.toUInt32,FloatLib.Numerics.FixedWord.log2Word_eq_log2];rfl def az (hi lo:Д):п:=bi hi*2^64+loа @[inline] def bK (hi lo:Д):Д:=if hi>>>63!=0 then (0:Д)-lo else lo @[inline] def bJ (hi lo:Д):Д:= if hi>>>63!=0 then (if lo==0 then (0:Д)-hi else ~~~hi) else hi lemma ce (d:Д):(d>>>63!=0)=decide (2^63<= dа):=by have:=d.toNat_lt;rw[ϻ];simp[<- Β,ι] lemma a8 (d e:Д): az d e=(dа*2^64+eа:п)-(if 2^63<= dа then 2^128 else 0):=by unfold az bi;rw[kE,ll];omega lemma cT (d e:Д): (az d e)м=(bJ d e)а*2^64+(bK d e)а /\ decide (az d e<0)=(d>>>63!=0):=by have:=d.toNat_lt;have:=e.toNat_lt;unfold bJ bK;rw[a8,ce];by_cases g:2^63<= dа<;>simp only[g,decide_true,decide_false,ite_true,ite_false,ο] .split<;>simp_all[jT,UInt64.toNat_not,<- Β]<;>omega .simp;omega @[inline] def bm (hi lo B:Д):Д:= if hi==0&&lo==0 then 0x100000000 else if B>442 then 0x100000000 else let neg:=hi>>>63!=0 let mlo:=bK hi lo let mhi:=bJ hi lo if mhi==0 then (aC neg mlo B)к else if mhi>>>32==0 then let q:=(mhi<<<32)+(mlo>>>32) (aC neg (if mlo&&&0xFFFFFFFF==0 then q else q ||| 1) (B+32))к else (aC neg (if mlo==0 then mhi else mhi ||| 1) (B+64))к lemma bl (n:о) (m o:о-> i9) (e g B:Д) (q:am n m o) (j:ah n m o=az e g*2^Bа) (h:bm e g B<0x100000000):kB n m o=(bm e g B)л:=by obtain ⟨r,t⟩:=cT e g;have:=g.toNat_lt;have:=e.toNat_lt;simp only[bm] at h⊢;have w:¬(e==0&&g==0)=true:=λc=>by simp[c] at h have u:¬B>442:=λc=>by simp[c] at h simp only[w,u,ο,↓reduceIte];clear h have v:ah n m o≠0:=by rw[j];refine mul_ne_zero (λp=>w ?_) В rw[a8] at p;simp only[υ,beq_iff_eq,<- Β,Ϯ];split at p<;>omega rw[a9 n m o q v,kV (kN (az e g) ((Bа:п)-298)) _ _ _ v (by rw[toRat_ofIntDyadic,j];push_cast;rw[zpow_sub₀ two_ne_zero,zpow_natCast];field_simp),kN,t,r] symm;simp only[apply_ite kr,UInt32.toUInt32_toUInt64];generalize bJ e g=l at* generalize bK e g=d at* have:=d.toNat_lt;simp only[ν,gt_iff_lt,iZ,not_lt] at u;split<;>rename_i p<;>simp only[beq_iff_eq,<- Β,Ϯ] at p .simp[p,ax _ _ B А] split<;>rename_i z<;>simp[<- Β,ι] at z .rw[ax _ _ _ (by simp[μ];omega),<- aD _ (lа*2^64+dа) _ 32 ((Ϧ А).2 А)] congr 3 swap;. simp[μ];omega have x:(lа*2^64+dа)/2^32=(l<<<32+d>>>32)а:=by simp[Μ,ι];omega have y:(lа*2^64+dа)%2^32=(d&&&4294967295)а:=by rw[ψ,show (4294967295:Д)а=2^32-1 from rfl,θ];omega simp only[jx,iZ,x,y,apply_ite jI,kp,beq_iff_eq, <- Β] .rw[ax _ _ _ (by simp[μ];omega),<- aD _ (lа*2^64+dа) _ 64 ((Ϧ А).2 А)] congr 3 swap;. simp[μ];omega simp only[jx,iZ,show (lа*2^64+dа)/2^64=lа by omega,show (lа*2^64+dа)%2^64=dа by omega,apply_ite jI,kp,beq_iff_eq, <- Β] @[inline] def aj (N:Д):Д:=(N+(0x3FFFFFFFFF:Д)+((N>>>39)&&&1))>>>39 lemma dL (n:ф) (e f:Е): (cd n e f)е=(if n then 2^31 else 0)+eе%2^8*2^23+fе%2^23:=by have d:=ϳ fе (ld 23);have:=ϳ eе (ld 8) have g:((e&&&0xff)<<<23 ||| (f&&&0x007fffff))е=2^23*(eе%2^8)+fе%2^23:=by rw[UInt32.toNat_or,UInt32.toNat_shiftLeft,Λ,Λ,show (0xff:Е)е=2^8-1 from rfl, show (0x007fffff:Е)е=2^23-1 from rfl,θ, θ,show (23:Е)е%32=23 from rfl,Μ,ϩ,ξ (by simp;omega), <- ϓ d] unfold cd;rw[UInt32.or_assoc];cases n<;>simp only[ο,↓reduceIte,UInt32.zero_or,UInt32.toNat_or,g] .omega .rw[show (0x80000000:Е)е=2^31*1 from rfl,<- ϓ А];omega lemma bT (n:ф) (N g:Д) (l:2^62<= Nа) (m:Nа<2^63) (t:110<= gа) (j:gа<363): (aC n N g)е=(if n then 2^31 else 0)+((gа-110)*2^23+(aj N)а) /\ 2^23<=(aj N)а/\(aj N)а<=2^24:=by have o:(N>>>39)а=Nа/2^39:=by simp[ι] have e:((N>>>39)&&&1)а=Nа/2^39%2:=by simp[o,kF] have r:(aj N)а=Nа/2^39+if 2^38omega have h:2^23<= Nа/2^39/\Nа/2^39<2^24:=by clear*-l m;omega have d:(aJ N (62-23))а=(aj N)а/\2^23<=(aj N)а/\(aj N)а<=2^24:=by have p:(N&&&0x7FFFFFFFFF)а=Nа%2^39:=by rw[ψ];exact θ _ 39 rw[r];show (cq N 39)а=_/\_;unfold cq simp only[show ((1:Д)<<<39)-1=0x7FFFFFFFFF from rfl,show (1:Д)<<<(39-1)=0x4000000000 from rfl,gt_iff_lt,ν,μ,p,e,o,apply_ite jI,iZ] clear*-h;split_ifs<;>omega refine ⟨?_,d.2⟩;unfold aC simp only[show an N=62 by rw[aG,<- Β];exact (Nat.log2_eq_iff (by omega:N.toNat≠0)).2 ⟨l,m⟩, show (N==0)=false by simp[<- Β];omega,show ¬62+g<172 by simp[ν];omega, show ¬(62:Д)<23 by decide,ite_false,ο] obtain ⟨d,e⟩:=d;generalize aJ N (62-23)=R at d⊢;rw[<- d] at e⊢;clear*-e t j;by_cases q:Rа=16777216<;>simp[q,<- Β,bQ,ν]<;>split<;>(try omega)<;>simp[dL,UInt32.toNat_sub,UInt32.toNat_add]<;>omega lemma cD (n:ф) (M σ:Д) (e:Mа≠0) (d:σа<=506): aC n M σ=kC ((if n then-(Mа:п) else Mа)*2^σа) (-298) false:=by rw[ax _ _ _ d];refine (kV _ _ _ _ (mul_ne_zero (by split<;>omega) В) ?_).symm cases n<;>simp[lX,jC,zpow_sub₀]<;>field_simp end Core open Core namespace Dense lemma al {k n:с} (h:ksplit<;>push_cast<;>omega @[inline] def aS (x:Е):Е:=x&&&0x7FFFFFFF lemma aR (x:Е):(aS x)е=xе%2^31:=by unfold aS;rw[Λ];exact θ _ 31 lemma be (x:Е):(i7 x)е=(aS x)е/2^23:=by have:(i7 x)е=xе/2^23%2^8:=by unfold i7;rw[Λ,Ρ];simp only[jj,jb,ι];exact θ _ 8 rw[this,aR,show 2^31=2^23*2^8 by norm_num,Nat.mod_mul_right_div_self] lemma cM (x:Е):i7 x=0↔(aS x)е<2^23:=by rw[<- Η,be];simp;try omega lemma gI (x:Е):je x=(aS x)е/2^23-1:=by have:=be x;unfold je;split<;>rename_i h .have:=(cM x).mp h;omega .have:=mt (cM x).mpr h;omega lemma br (x:Е):je x=(i7 x)е-1:=by rw[gI,be] lemma gT (w:Е):wе/2^23=(i7 w)е+256*(wе/2^31):=by rw[be,aR];have:=w.toNat_lt;omega lemma bO (x:Е):(i7 x)е<256:=by rw[be,aR];omega lemma gG (w:Е):(w&&&0x7FFFFF)е=wе%2^23:=by rw[Λ];exact θ _ 23 lemma bV (w:Е): |sv w| <2^24:=by have:=kw w;unfold sv;split<;>simp<;>omega lemma ay {k:с} {a:у Е} (h:k>>1>>>(63-s))+(if l'simp only[iZ]<;>omega @[specialize] def go (fa fb:о-> т) (n t:о) (B:Д):Д:= if t т) (n:о) (B:Д) (t:о) (pH pL nH nL:Д):Д:= if tsplit<;>push_cast<;>omega lemma cZ (d g:о-> i9) (n:о) (B:Д) (hn:n<2^18): ∀k t (v w r u:Д),n-t=k-> t<= n-> am t d g -> vа*2^64+wа<= t*2^108-> rа*2^64+uа<= t*2^108 -> ah t d g=(((vа*2^64+wа:о):п)-((rа*2^64+uа:о):п))* 2^Bа -> bX d g n B t v w r u<0x100000000-> kB n d g=(bX d g n B t v w r u)л:=by intro k;induction k<;>intro t v w r u hk ht Z K J M j .obtain rfl:t=n:=А rw[bX,if_neg А] at j⊢;exact bl _ _ _ _ _ _ Z (by rw[M,iY _ _ _ _ А А]) j rename_i k Y;have W:t(Nat.lt_succ_iff_lt_or_eq.mp E).elim (Z s) λe=>e ▸ ⟨G,I⟩ have o:jF (d t)*jF (g t)<2^48:= (Nat.mul_lt_mul'' (kw _) (kw _)).trans_eq Г have S:(mW (d t)*mW (g t))а=jF (d t)*jF (g t):=by rw[Ϛ,aN,aN,ξ (o.trans Г)] have D:=aE t d g;have m:=Ζ (2^108) t.le_succ;split at j .rename_i F rw[if_pos F];have N:jF (d t)*jF (g t)=0:=by rw[<- S,beq_iff_eq.mp F];rfl refine Y (t+1) v w r u y z x (K.trans m) (J.trans m) ?_ j;rw[D,M,add_eq_left];unfold tm sv;rcases Nat.mul_eq_zero.mp N with h | h<;>simp[h] rename_i F;rw[if_neg F];obtain ⟨hB,O⟩:=hw λh=>F (by simp[h]) have a0:=idxOf_le _ G;have a1:=idxOf_le _ I have Q:(iW (d t)+iW (g t))а=je (d t)+je (g t):=by rw[μ,bf,bf,ξ А] rw[Q] at hB have E:(iW (d t)+iW (g t)-B)а=je (d t)+je (g t)-Bа:=by rw[χ _ _ (by rw[κ,Q];omega),Q] rw[E] at O have V:(2:п)^(je (d t)+je (g t))=2^(je (d t)+je (g t)-Bа)*2^Bа:=by rw[<- pow_add];congr 1;omega generalize l:(jF (d t)*jF (g t))*2^(je (d t)+je (g t)-Bа)=T have p:T<=2^108:= l ▸ (Nat.mul_le_mul o.le (Ε Г (by omega:_<=60))).trans_eq Г have A:tm (d t) (g t)=(if jw (d t)==jw (g t) then (T:п) else-T)*2^Bа:=by rw[<- l];unfold tm sv;rw[V];cases jw (d t)<;>cases jw (g t)<;>simp<;>ring have U:=λH L (as:Hа*2^64+Lа<= t*2^108)=>cY H L _ _ (by rw[E];omega) (by rw[S,E,l];omega) rw[S,E,l] at U;cases hg:(jw (d t)==jw (g t))<;>simp only[hg,ite_true,ite_false,ο] at A j⊢ .have q:=U r u J refine Y (t+1) v w _ _ y z x (K.trans m) (by rw[q];exact ϋ t _ ▸ Nat.add_le_add J p) ?_ j rw[D,M,q,A];push_cast;ring .have q:=U v w K refine Y (t+1) _ _ r u y z x (by rw[q];exact ϋ t _ ▸ Nat.add_le_add K p) (J.trans m) ?_ j rw[D,M,q,A];push_cast;ring @[inline] def eW (n:о) (fa fb:о-> т):т:= let r:=if n<262144 then bX fa fb n (go fa fb n 0 1023) 0 0 0 0 0 else 0x100000000 if r<0x100000000 then rл else Pinned.dotFn n fa fb lemma cJ (n:о) (d e:о-> i9):eW n d e=kB n d e:=by unfold eW;dsimp only;by_cases g:n<262144 .rw[if_pos g];split .exact (cZ d e n _ А _ 0 0 0 0 0 rfl А (λ_ h=>absurd h А) (by simp) (by simp) (by simp[ah]) ‹_›).symm .rw[Pinned.dotFn_eq_dotOf] .rw[if_neg g,if_neg Б,Pinned.dotFn_eq_dotOf] @[noinline] def ap (n:о) (relu:ф) (X W b:@& у т) (xo s j:о):т:= act relu (eW (n+1) (λt=>if tif trfl lemma dU (x y:р) (d:fv x) (e:fv y): i6 (x+y).toModel=lB (i6 x.toModel) (i6 y.toModel):=by change i6 (l4 x.toModel y.toModel)=_;rw[l4,Ϣ] have h:=Model.add_eq_ofModel_add_of_isFinite (fmt:=i5) Б (i6 x.toModel) (i6 y.toModel) (by rw[Θ];exact (bB x).1 d) (by rw[Θ];exact (bB y).1 e) rw[Θ,Θ] at h;exact h.symm lemma pm (E:п) (e:E<=971):(2:ℝ)^E<= jJ (kG i5):=by have d:FloatFormat.binary64.maxNormalExponent-Int.ofNat FloatFormat.binary64.fracWidth=971:=Б have h:=Ϡ i5 false 1 E Б (by rw[d];exact e) simp only[ο,ite_false,lQ,one_mul] at h;change |(2:ℝ)^E| <= _ at h simpa only[abs_of_pos (zpow_pos (by norm_num:(0:ℝ)<2) E)] using h open FloatLib.Floats.Formats.Flocq in lemma re (x:ℝ) (E:п) (g:-1021<= E) (e: |x| <(2:ℝ)^E): |Model.roundAt i5 x-x| <= (2:ℝ)^(E-53)/2:=by by_cases d:x=0 .subst x;rw[Model.roundAt_zero];simp only[sub_zero,abs_zero];positivity have h:magnitude jh x<= E:=magnitude_le_of_abs_lt_bpow _ x E d e;apply (Model.abs_roundAt_sub_le i5 x).trans;apply div_le_div_of_nonneg_right _ Г;change ulp jh (Model.fexpOf i5) x<=(2:ℝ)^(E-53);rw[ulp.of_ne_zero _ _ x d];change (2:ℝ)^(lm (magnitude jh x-53) (-1074))<=(2:ℝ)^(E-53);apply zpow_le_zpow_right₀ Г;omega lemma db (x y:р) (d:fv x) (e:fv y) (j: |rv x+rv y| <= jJ (kG i5)): fv (x+y)/\rv (x+y)=kh i5 (rv x+rv y):=by have h:=dU x y d e have g:=Model.isFinite_add_of_abs_toReal_add_le_posMaxFinite (i6 x.toModel) (i6 y.toModel) Б d e j refine ⟨by unfold fv;rw[h];exact g,?_⟩ unfold rv;rw[h];exact kx _ _ Б g lemma gF (x y:р) (l:fv x) (m:fv y) (E:п) (j:-1021<= E) (d:E<=971) (e: |rv x+rv y| <(2:ℝ)^E): fv (x+y) /\ |rv (x+y)-(rv x+rv y)| <= (2:ℝ)^(E-53)/2:=by obtain ⟨g,h⟩:=db x y l m (e.le.trans (pm E d));exact ⟨g,by rw[h];exact re _ E j e⟩ lemma rx (d:jf) (l:d.significand<2^53) (g:-1074<= d.exponent) (e: |d.toReal| <= (2:ℝ)^(971:п)): kh i5 d.toReal=d.toReal:=by obtain ⟨h,j⟩:=jO i5 Б d d.significand 0 (by simp) l g (e.trans (pm 971 le_rfl)) rw[<- ϗ _ Б d h,j] lemma gx (x y:р) (o:fv x) (p:fv y) (d:jf) (g:d.toReal=rv x+rv y) (m:d.significand<2^53) (l:-1074<= d.exponent) (e: |d.toReal| <= (2:ℝ)^(971:п)): fv (x+y)/\rv (x+y)=rv x+rv y:=by obtain ⟨h,j⟩:=db x y o p (by rw[<- g];exact e.trans (pm 971 le_rfl));exact ⟨h,by rw[j,<- g];exact rx d m l e⟩ lemma cy (i:Int64) (e:iнм<2^53):fv i.toFloat/\rv i.toFloat=iн:=by have g:i6 i.toFloat.toModel= i8 i5 (js iн 0):= ka i have d:(js iн 0).toReal=iн:=by rw[<- Ϙ,k8];simp obtain ⟨h,j⟩:=jO i5 Б (js iн 0) iнм 0 (ϱ _).symm e (by change _<=(0:ℤ);decide) (by rw[d,<- ϕ,kO];exact le_trans (by exact_mod_cast e.le) (pm 53 Г)) exact ⟨by unfold fv;rw[g];exact h,by unfold rv;rw[g,j,d]⟩ lemma gO (x y:р):i6 (x*y).toModel= lH i5 (jq jt x.toModel.unpack y.toModel.unpack):=by change i6 (l5 x.toModel y.toModel)=_;rw[l5,Ϣ] lemma eV (b:BitVec 64) (s:lR) (m:о) (e:п) (h:0< m) (d:jc jt b=.finite s m e h): 2^52<= m\/e=-1074:=by revert d;unfold jc;dsimp only;split .split<;>intro d<;>cases d .split .split .intro d;cases d .rename_i l _ intro d;injection d with _ _ j;right;rw[<- j,l];decide .intro d;injection d with _ g _ left;rw[<- g,BitVec.toNat_append];exact le_trans Б Nat.left_le_or lemma d4 (x y:р) (w:fv x) (z:fv y) (v: |rv x*rv y| <= (2:ℝ)^(971:п)): fv (x*y)/\rv (x*y)=kh i5 (rv x*rv y):=by simp only[bB] at w z;rw[cf x,cf y] at v⊢;unfold fv rv;rw[gO];generalize A:x.toModel.unpack=X at w v⊢;generalize B:y.toModel.unpack=Y at z v⊢;cases X<;>cases Y<;>simp only[jn,ο] at w z case finite.finite p j e t q l g u=> have D:=eV _ p j e t A;have E:=eV _ q l g u B have o:e+g<= Float.Model.Format.binary64.targetExponent (jl (j*l) (e+g)):=by change e+g<= lm ((Nat.log2 (j*l):п)+1+(e+g)-53) (-1074);have:=(Ϧ (n:=j*l) (k:=52) В).2;have:=kX j u;have:=Nat.le_mul_of_pos_left l t;omega let r:jf:=⟨xor (lL p) (lL q),j*l,e+g⟩ have h:lH i5 (jq jt (.finite p j e t) (.finite q l g u))=i8 i5 r:=by rw[jq,Model.roundWithAccuracy_exact_eq_round_of_le_targetExponent _ _ _ _ o];cases p<;>cases q<;>rfl have d:r.toReal=jp (.finite p j e t)*jp (.finite q l g u):= Model.Dyadic.toReal_mul ⟨_,j,e⟩ ⟨_,l,g⟩ have m:=Υ i5 Б r (by rw[d];exact v.trans (pm 971 le_rfl)) rw[h];exact ⟨m,by rw[ϗ _ Б r m,d]⟩ all_goals simp[jq,Model.isFinite_ofModel_zero i5 Б, Model.toReal_ofModel_zero i5 Б] lemma aw (s:ф) (m:о) (e:п): (⟨s,m,e⟩:jf).toReal=(if s then-(m:ℝ) else m)*(2:ℝ)^e:=by simp only[jz,kP];split<;>simp def pw:о-> р | 0=>(1:Int64).toFloat | k+1=>let p:=pw k;p+p lemma gh (k:о) (g:k<=900):fv (pw k)/\rv (pw k)=(2:ℝ)^k:=by induction k with | zero=>have:=cy 1 Б;simp only[pw];exact ⟨this.1,by rw[this.2];simp⟩ | succ k e=> obtain ⟨f,v⟩:=e А have d:(⟨false,1,((k+1:о):п)⟩:jf).toReal=(2:ℝ)^(k+1):=by rw[aw];simp only[ο,ite_false,lQ,one_mul];exact zpow_natCast 2 (k+1) have:=gx (pw k) (pw k) f f _ (by rw[d,v,pow_succ];ring) (show (1:о)<2^53 by norm_num) (show (-1074:п)<=((k+1:о):п) by omega) (by rw[d,abs_of_pos В,<- zpow_natCast];exact zpow_le_zpow_right₀ Г А) simp only[pw];exact ⟨this.1,by rw[this.2,v,pow_succ];ring⟩ def nm:р:=(-1:Int64).toFloat def P:FloatArray:=⟨Array.ofFn (n:=512) λi=>if iи<256 then pw (iи-1) else nm*pw (iи-256-1)⟩ lemma ag:Pд=512:=by simp[P,jD] lemma e8 (i:с) (h:iб>>23)е=wе/2^23:=by rw[Ρ];simp[ι] @[inline] def dw (w:Е):р:= (Core.mW w).toInt64.toFloat*P.uget (w>>>23).toUSize (by rw[ag,aH,cW];have:=w.toNat_lt;omega) lemma bn (z e:п):(kN z e).toReal=(z:ℝ)*(2:ℝ)^e:=by rw[<- Ϙ,toRat_ofIntDyadic];push_cast;rfl lemma cp (x y:р) (o:fv x) (p:fv y) (z e:п) (g:rv x*rv y=(z:ℝ)*(2:ℝ)^e) (m:zм<2^53) (l:-1074<= e) (d: |(z:ℝ)*(2:ℝ)^e| <= (2:ℝ)^(971:п)): fv (x*y)/\rv (x*y)=(z:ℝ)*(2:ℝ)^e:=by obtain ⟨h,j⟩:=d4 x y o p (by rw[g];exact d) have:=rx (kN z e) m l (by rw[bn];exact d) rw[bn] at this;exact ⟨h,by rw[j,g,this]⟩ lemma eT (w:Е):(sv w)м<2^24:=by have:=kw w;unfold sv;split<;>simp<;>omega lemma ez (a b c:о) (e:a+b<= c) (h:c<=971) (z:п) (g:zм<2^a): |(z:ℝ)*(2:ℝ)^(b:п)| <= (2:ℝ)^(971:п):=by rw[abs_mul,abs_of_pos (by positivity:(0:ℝ)<2^(b:п)),zpow_natCast] have d: |(z:ℝ)| <= 2^a:=by rw[<- ϕ,kO];exact_mod_cast g.le refine (mul_le_mul_of_nonneg_right d В).trans ?_;rw[<- pow_add,<- zpow_natCast];exact zpow_le_zpow_right₀ Г А lemma mV (u:Д) (n:о) (d:uа=n) (e:n<2^25): fv u.toInt64.toFloat/\rv u.toInt64.toFloat=(n:п):=by have:u.toInt64н=n:=by rw[show u.toInt64н=bi u from rfl,au,d];split<;>omega rw[<- this];exact cy _ (by rw[this];simp;omega) lemma qV (c:о) (A:FloatArray) (o:∀i h,A.uget i h=if iб<256 then pw (iб-c) else nm*pw (iб-256-c)) (w:Е) (h):fv (A.uget (w>>>23).toUSize h) /\ ∃σ:п, (∀v,jw v=jw w-> σ*jF v=sv v)/\σм=1 /\ rv (A.uget (w>>>23).toUSize h)=σ*2^((i7 w)е-c):=by have:=bO w;have:=w.toNat_lt;have d:=aP w;obtain ⟨j,l⟩:=gh ((i7 w)е-c) А;rw[o,aH,cW,gT];split .rw[show (i7 w)е+256*(wе/2^31)-c=(i7 w)е-c by omega] exact ⟨j,1,λv e=>by simp only[sv,e,d];split<;>omega,rfl,by rw[l];push_cast;ring⟩ .rw[show (i7 w)е+256*(wе/2^31)-256-c=(i7 w)е-c by omega] have g:=cy (-1) Б obtain ⟨m,p⟩:=cp _ _ g.1 j (-1) ((i7 w)е-c:ℕ) (by rw[g.2,l,zpow_natCast];rfl) Б А (ez 1 _ 971 А le_rfl _ Б) exact ⟨m,-1,λv e=>by simp only[sv,e,d];split<;>omega,rfl,by rw[<- zpow_natCast];exact p⟩ lemma dG (c q:о) (A:FloatArray) (o:∀i h,A.uget i h=if iб<256 then pw (iб-c) else nm*pw (iб-256-c)) (u:Д) (v w:Е) (h) (r:q<=2) (x:uа=q*jF v) (t:jw v=jw w) (p:(q:ℝ)*2^((i7 w)е-c)=2^je v): fv (u.toInt64.toFloat*A.uget (w>>>23).toUSize h) /\ rv (u.toInt64.toFloat*A.uget (w>>>23).toUSize h)=(sv v:ℝ)*2^je v:=by have:=kw v;have:=Ζ (jF v) r;have:=bO w;obtain ⟨g,j⟩:=mV u _ x А;obtain ⟨l,σ,d,m,y⟩:=qV c A o w h;have e:(((q*jF v:о):п)*σ)м<2^25:=by rw[Int.natAbs_mul,m];simp;omega have:=cp _ _ g l _ ((i7 w)е-c:о) (by rw[j,y,zpow_natCast];push_cast;ring) (e.trans Г) А (ez 25 _ 971 А le_rfl _ e) exact ⟨this.1,by rw[this.2,<- p,zpow_natCast,<- d v t];push_cast;ring⟩ lemma av (w:Е) (_:i7 w≠255):fv (dw w)/\rv (dw w)=(sv w:ℝ)*2^je w:= dG 1 1 P e8 _ w w _ А (by simp[aN]) rfl (by simp[br]) lemma ey (x w:Е) (j:i7 x≠255) (h:i7 w≠255): fv (dw x*dw w)/\rv (dw x*dw w)=(tm x w:ℝ):=by obtain ⟨e,l⟩:=av x j;obtain ⟨g,m⟩:=av w h have d:(sv x*sv w)м<2^48:=by rw[Int.natAbs_mul];exact (Nat.mul_lt_mul'' (eT x) (eT w)).trans_eq Г have:=cp _ _ e g (sv x*sv w) (je x+je w:о) (by rw[l,m,zpow_natCast,pow_add];push_cast;ring) (lt_trans d Г) А (ez 48 _ 971 (by rw[br,br];have:=bO x;have:=bO w;omega) le_rfl _ d) refine ⟨this.1,?_⟩;rw[this.2,tm,zpow_natCast];push_cast;ring @[inline] def eF (b:Д):Д:=(b>>>52)&&&2047 @[inline] def mF (b:Д):Д:=(b&&&0xfffffffffffff) ||| 0x10000000000000 lemma gP (u:Д):(u&&&0x8000000000000000!=0)=(u>>>63!=0):=by apply ϻ.mpr;simp only[bne_iff_ne,ne_eq,<- Β];rw[ψ,Α];change ¬uа&&&2^63=0↔¬uа>>>63=0;rw[lc,ι,jZ];have d:uа/2^63<2:=by have h:=UInt64.toNat_lt u;omega rw[ξ d];by_cases e:uа/2^63=1<;>simp<;>omega lemma dc (v:р):i6 v.toModel=Model.ofFields i5 (v.toBits>>>63!=0) (((v.toBits>>>52)&&&2047)а) ((v.toBits&&&0xfffffffffffff)а):=by rw[<- Model.ofFields_signBit_expField_fracField (i6 v.toModel)];congr 1;rw[<- gP];apply ϻ.mpr;simp only[Model.signBit,bne_iff_ne,ne_eq];rw[<- UInt64.toBitVec_inj];exact Iff.rfl lemma fq (v:р):((v.toBits>>>52)&&&2047)а<2^11/\(v.toBits&&&0xfffffffffffff)а<2^52:=by simp only[ψ];exact ⟨lt_of_le_of_lt ϙ Б,lt_of_le_of_lt ϙ Б⟩ lemma aK (v:р) (e:fv v) (g:¬eF v.toBits=0): rv v=(⟨v.toBits>>>63!=0,(v.toBits&&&0xfffffffffffff)а+2^52, ((eF v.toBits)а:п)-1075⟩:jf).toReal:=by unfold eF at g⊢;have j:=(fq v).1;have l:=(fq v).2;have d:((v.toBits>>>52)&&&2047)а≠0:=λh=>g (Β.mp (by simpa using h)) unfold fv at e;unfold rv;rw[dc] at e⊢;rw[jK,ϒ _ _ _ _ j l e,if_neg d] simp only[show FloatFormat.binary64.fracWidth=52 from rfl,show FloatFormat.binary64.exponentBias=1023 from rfl, ln] congr 2<;>(try simp only[kl,j0])<;>ring lemma bp (z:Model lr):ofW (jH z)=z:=by have h:z.toNatBits<2^32:=Model.toNatBits_lt_two_pow z;simp only[ofW,jH,ls,UInt32.toNat_ofNat',ξ h];exact Model.ofNatBits_toNatBits z lemma cs (w:i9) (d:i7 w≠255):jJ (ofW w)=(sv w:ℝ)*(2:ℝ)^((je w:п)-149):=by rw[ofW,jK,toDyadic_ofUInt32 w d];change (decodeD w).toReal=_;rw[<- Ϙ,decodeD_toRat];push_cast;rfl lemma ev (w:i9) (j:i7 w≠255) (m:w&&&0x7FFFFFFF≠0):jJ (ofW w)≠0:=by rw[cs w j];refine mul_ne_zero ?_ (zpow_ne_zero _ Г) have l:jF w≠0:=by unfold jF;split .rename_i d have e:=(cM w).mp d;rw[aR] at e;have g:(aS w)е≠0:=λh=>m (Η.mp (h.trans UInt32.toNat_zero.symm)) rw[aR] at g;unfold lW;rw[gG];omega .omega unfold sv;split<;>simp[l] lemma eM (d g h:jf) (m:d.toReal<= g.toReal) (o:g.toReal<= h.toReal) (w:jH (i8 lr d)=jH (i8 lr h)) (u:i7 (jH (i8 lr d))≠255) (x:jH (i8 lr d)&&&0x7FFFFFFF≠0) (v: |g.toReal| <= (2:ℝ)^(127:п)): jH (i8 lr g)=jH (i8 lr d):=by have e:=bp (i8 lr d);have j:jW (i8 lr d)=true:=by rw[<- e,ofW,kM];simpa using u have l:=Υ lr Б g (v.trans ((Ϡ lr false (2^23) 104 Б Б).trans' (by change _<= |(if false=true then (-1:ℝ) else 1)*((2^23:ℕ):ℝ)*(2:ℝ)^(104:ℤ)|;norm_num))) have t:i8 lr h=i8 lr d:=by rw[<- bp (i8 lr h),<- w,e] have r:=ϗ lr Б;have p:=jP lr m;have q:=jP lr o;rw[<- r d j,<- r g l] at p;rw[<- r g l,<- r h (by rw[t];exact j),t] at q rw[Model.eq_of_toReal_eq_of_nonzero (le_antisymm q p) (by rw[le_antisymm q p,<- e];exact ev _ u x)] lemma iF (x:о) (e:x<2^53) (d:x%2^29≠2^28): (aj (lP (x*2^10)))а=(x+2^28)/2^29:=by simp only[aj,Α,μ,ψ,iZ, Ξ (by simp only[jT];omega:x*2^10>>29 if d<=26&&E-1195<253&&u-(g+1)<0x1FFFFFFF-(g+g)&&r&&&0x7FFFFF!=0 then ((b>>>63)<<<31)+r-0x255000000 else 0x100000000 lemma rb (b:Д) (h:(((b&&&0x7FFFFFFFFFFFFFFF)+0x10000000)>>>29&&&0x7FFFFF!=0)=true): 2^28<=(b&&&0xfffffffffffff)а/\(b&&&0xfffffffffffff)а+2^28<2^52:=by simp only[bne_iff_ne,ne_eq,<- Β,ψ,Α,μ, iZ,jb,ι] at h⊢ rw[θ _ 63,θ _ 23] at h;rw[θ _ 52];omega lemma fJ (h E f:Д) (p:hа<2^63) (m:Eа<2048) (o:fа<2^52) (d:h+1075-E<=26) (g:E-1195<253) (e:((f+0x10000000)&&&0x1FFFFFFF)-(((1:Д)<<<(h+1075-E))+1)< 0x1FFFFFFF-(((1:Д)<<<(h+1075-E))+((1:Д)<<<(h+1075-E)))) (l:2^28<= fа/\fа+2^28<2^52): Eа<= hа+1075/\hа+1075-Eа<=26/\1195<= Eа/\Eа<=1447 /\ 2^(hа+1075-Eа)+1<=(fа+2^28)%2^29 /\ (fа+2^28)%2^29+2^(hа+1075-Eа)<2^29 /\ 2^(hа+1075-Eа)<= fа/\fа+2^(hа+1075-Eа)<2^52:=by simp only[κ,ν,Κ,μ,ψ, Ι,iZ,kW,ϭ] at d g e have j:(2^64-Eа+(hа+1075)%2^64)%2^64=hа+1075-Eа:=А;rw[j] at d e;have:=Ε (n:=2) Г d;rw[ξ (by omega:_<64),θ _ 29] at e omega lemma fK (b:Д) (d:1195<=(eF b)а): (((b>>>63)<<<31)+(((b&&&0x7FFFFFFFFFFFFFFF)+0x10000000)>>>29)-0x255000000)а= bа/2^63*2^31+(((eF b)а-1085-110)*2^23+ (2^23+((b&&&0xfffffffffffff)а+2^28)/2^29)):=by simp only[eF,Κ,μ,Ι,Α, ψ,iZ,jb,ι,Μ] at d⊢ rw[θ _ 11] at d⊢;rw[θ _ 63,θ _ 52];have:=b.toNat_lt;omega lemma ch (S:р) (hS:fv S) (h:Д) (hh:hа<2^63) (T:п) (x: |rv S-(T:ℝ)| <= (2:ℝ)^(hа:п)) (as: |(T:ℝ)| <= (2:ℝ)^(425:п)) (F:ai S h<0x100000000):T≠0/\(ai S h)л=kC T (-298) false:=by unfold ai at F⊢;dsimp only at F⊢ split;swap;. simp[*] at F rename_i u;simp only[υ,decide_eq_true_eq] at u;obtain ⟨⟨⟨X,Y⟩,Z⟩,c4⟩:=u have I:(if (S.toBits>>>63!=0)=true then 2^31 else 0)=S.toBitsа/2^63*2^31:=by simp only[ce,decide_eq_true_eq];have:=S.toBits.toNat_lt;split<;>omega obtain ⟨d1,d2,A,e2,u1,u2,f1,f2⟩:=fJ h (eF S.toBits) _ hh (fq S).1 (fq S).2 X Y Z (rb _ c4);have Q:=fK S.toBits A;have O:=aK S hS (λh0=>by rw[h0] at A;simp at A) rw[<- I] at Q have H:(eF S.toBits-1085)а=(eF S.toBits)а-1085:=by rw[Κ];simp only[iZ];omega generalize hW:kr _=W;generalize (S.toBits>>>63!=0)=y at* generalize (eF S.toBits)а=d at* generalize hG:2^(hа+1075-d)=G at* generalize (S.toBits&&&0xfffffffffffff)а=g at* have j:Wе=(if y then 2^31 else 0)+((d-1085-110)*2^23+(2^23+(g+2^28)/2^29)):=by rw[<- hW,ϟ,Q];split<;>omega have v:∀N,g+2^52<= N+G-> N<= g+2^52+G -> jH (i8 lr ⟨y,N*2^10,((d-1085:ℕ):ℤ)-298⟩)=W:=λN l r=>by have n:=Ξ (show N*2^10by have:=be W;simp only[J,aR,j,jj] at this;split at this<;>omega have V:W&&&0x7FFFFFFF≠0:=λJ=>by have:=aR W;simp only[aS,J,j,j5] at this;split at this<;>omega have o:=v (g+2^52-G) А А;have p:=v (g+2^52+G) А А;have D:Gby rw[Nat.cast_mul,mul_assoc,mul_assoc,Nat.cast_pow,j0,<- zpow_natCast (2:ℝ) 10,<- zpow_add₀ two_ne_zero, <- zpow_add₀ two_ne_zero,show ((10:ℕ):ℤ)+(((d-1085:ℕ):ℤ)-298)=(d:ℤ)-1075+-298 by omega] have hu:(0:ℝ)<(2:ℝ)^((d:п)-1075):=В;have e:(0:ℝ)<(2:ℝ)^(-298:п):=В have t: |(kN T (-298)).toReal| <= (2:ℝ)^(127:п):=by rw[bn,abs_mul,abs_of_pos e,show (127:ℤ)=425+-298 by norm_num,zpow_add₀ two_ne_zero];gcongr rw[hU,O] at x;generalize g+2^52=M at x o p D;have z:((M-G:ℕ):ℝ)=M-G:=k9 D.le;have E:(G:ℝ)simp only[ο,ite_false,ite_true] at x<;>obtain ⟨K,L⟩:=abs_le.mp x<;> have q:T≠0:=by rintro rfl;push_cast at K L;nlinarith only[K,L,E,hu] all_goals refine ⟨q,?_⟩;simp only[kC,q,↓reduceIte] on_goal 2=>refine ((eM _ _ _ ?_ ?_ (p.trans o.symm) (p ▸ U) (p ▸ V) t).trans p).symm refine ((eM _ _ _ ?_ ?_ (o.trans p.symm) (o ▸ U) (o ▸ V) t).trans o).symm;all_goals simp only[bn,aw,ο,ite_false,ite_true,neg_mul,B,z];push_cast;nlinarith only[K,L,e] @[specialize] def ac (p:о-> р) (n t:о) (a:р):р:= if t р | 0=>s.a0 | 1=>s.a1 | 2=>s.a2 | 3=>s.a3 | 4=>s.a4 | 5=>s.a5 | 6=>s.a6 | _=>s.a7 lemma uk {i k:с} {S:о} (d:kб<8) (h:iб+8<= S) (e:S<2^32): (i+k)бsimp[*,getElem!_pos] @[specialize] def bk (f:о-> р) (N:о) (Y:FloatArray):FloatArray:= if Yд р) (N:о):∀k (Y:FloatArray),N-Yд=k-> Yд<= N -> (bk f N Y)д=N/\(∀q q(bk f N Y).data[q]! =f q:=by intro k;induction k<;>intro Y r p .rw[bk,if_neg А];exact ⟨by omega,λq _=>rfl,λq h d=>by omega⟩ rename_i o;rw[bk,if_pos А];have t:=gf Y (f Yд);obtain ⟨l,g,m⟩:=o (Y.push (f Yд)) А А;refine ⟨l,λq j=>by rw[g q А,pg _ _ _ А,if_pos j],λq h d=>?_⟩ rcases eq_or_ne q Yд with rfl | e .rw[g _ А,pg _ _ _ А,if_neg (lt_irrefl _)] exact m q А d lemma f6 (v:р) (h:(eF v.toBits)а<2047):fv v:=by unfold fv;rw[dc];have e:=(fq v).1;have g:=(fq v).2;rw[Model.isFinite_ofFields _ _ _ _ e g];have d:FloatFormat.binary64.expAllOnesNat=2047:=Б;unfold eF at h;simp only[show FloatFormat.binary64.encoding=.ieee from rfl,d,bne_iff_ne,ne_eq];omega lemma bj (v:р) (g:fv v): |rv v| <(2:ℝ)^(((eF v.toBits)а:п)-1022):=by have d:∀(m k:ℕ) (e f:ℤ),m<2^k-> k+e<= f->(m:ℝ)*2^e<2^f:=λm k e f h j=> (mul_lt_mul_of_pos_right (by exact_mod_cast h:(m:ℝ)<2^k) (zpow_pos two_pos e)).trans_le (by rw[<- zpow_natCast,<- zpow_add₀ two_ne_zero];exact zpow_le_zpow_right₀ Г j) unfold rv eF;unfold fv at g;rw[dc] at g⊢;rw[jK,ϒ _ _ _ _ (fq v).1 (fq v).2 g];have:=(fq v).2;split_ifs with l<;>simp only[Model.Dyadic.abs_toReal] .simp;positivity .exact d _ 52 _ _ this (by rw[l];decide) .exact d _ 53 _ _ (by simp only[i5,ln];omega) (by simp[i5];omega) lemma iL (x y:р) (l:fv x) (m:fv y) (r:fv (x+y)) (E:п) (e:-1074<= E) (g:E<=971) (h: |rv (x+y)| <(2:ℝ)^E): |rv x+rv y| <(2:ℝ)^E:=by have j:=dU x y l m;have q:=kx (i6 x.toModel) (i6 y.toModel) Б (j ▸ r);unfold rv at h⊢;rw[j,q,abs_lt] at h;have p:=rx ⟨false,1,E⟩ Г e (by simp[aw];exact zpow_le_zpow_right₀ Г g) have o:=rx ⟨true,1,E⟩ Г e (by simp[aw];exact zpow_le_zpow_right₀ Г g) simp only[aw,ο,ite_false,ite_true,lQ,one_mul,neg_mul] at p o exact abs_lt.2 ⟨lt_of_not_ge λd=>by linarith[jP i5 d], lt_of_not_ge λd=>by linarith[jP i5 d]⟩ @[specialize] def sT (p:о-> р) (n t:о) (a:р) (m:Д):р×Д:= if trename_i h<;>simp only[ν] at h<;>omega lemma fn (p:о-> р) (n:о):∀k t a m,n-t=k-> mа<=(sT p n t a m).2а:=by intro k;induction k with | zero=>intro t a m h;rw[sT,if_neg А] | succ k d=> intro t a m h;rw[sT,if_pos А];dsimp only;have:=d (t+1) (a+p t) (if m р) (z:о-> п) (q:п) (n K:о) (u:1<= K) (v:K<=1993) (x:∀t t<= n-> fv a -> |rv a-((q:ℝ)+∑s∈i0 t,(z s:ℝ))| <= t*(2:ℝ)^((K:п)-1076) -> (sT p n t a M).2а<= K -> fv (sT p n t a M).1 /\ |rv (sT p n t a M).1-((q:ℝ)+∑s∈i0 n,(z s:ℝ))| <= n*(2:ℝ)^((K:п)-1076):=by intro m;induction m<;>intro t a M B D h g j .obtain rfl:t=n:=А rw[sT,if_neg (lt_irrefl _)];exact ⟨h,g⟩ rename_i y;have d:tlinarith only[e.1,e.2,g.1,g.2,A] lemma cw (n:о) (d e:о-> i9) (g:am n d e) (S:р) (m:fv S) (h:Д) (q:hа<2^63) (o: |rv S-(ah n d e:ℝ)| <= (2:ℝ)^(hа:п)) (l: |(ah n d e:ℝ)| <= (2:ℝ)^(425:п)) (p:ai S h<0x100000000): (ai S h)л=kB n d e:=by obtain ⟨j,r⟩:=ch S m h q _ o l p;rw[r,a9 n d e g j] def aI (A:у т) (i:с) (m:Е):Е:= if h:i>>23)&&&255 aI A (i+1) (if m mе<=(aI A i m)е /\ ∀q,iб<= q-> q(i7 A[q]!)е<=(aI A i m)е:=by intro k;induction k<;>intro i m u .have h:¬iby have:=ay h;omega rw[aI,dif_neg h];exact ⟨le_rfl,λq g d=>by omega⟩ rename_i t;have h:iby split<;>rename_i j<;>simp only[ϖ] at j<;>omega obtain ⟨p,r⟩:=t (i+1) (if m<(A.uget i (ay h)>>>23)&&&255 then (A.uget i (ay h)>>>23)&&&255 else m) (by rw[al h];omega) rw[o] at p;refine ⟨by omega,λq g d=>?_⟩ rcases eq_or_ne q iб with rfl | e .rw[<- bt A i (ay h)];unfold i7;omega exact r q (by rw[al h];omega) d lemma da (A:у i9) (j:Aвby rw[e] at d;simp at d g;omega,by rw[br];omega⟩ @[inline] def s8 (Y:FloatArray) (o:с) (e0 e1 e2 e3 e4 e5 e6 e7:р):FloatArray:= (((((((Y.set! oб e0).set! (o+1)б e1).set! (o+2)б e2).set! (o+3)б e3).set! (o+4)б e4).set! (o+5)б e5).set! (o+6)б e6).set! (o+7)б e7 lemma dQ (Y:FloatArray) (o:с) (e:о-> р) (h:oб+8?_⟩ simp (disch:=(try simp only[bD,USize.reduceToNat]);omega) only[s8,sg,ab,jd] split_ifs<;>first | rfl | omega | (congr 1;omega) lemma gD (X:у i9) (k:о):X.getD k 0=X[k]!:=by unfold Array.getD;split<;>rename_i h .rw[getElem!_pos X k h];rfl .rw[getElem!_neg X k h];rfl @[inline] def xr (X:у т) (q st:с) (r:о):р:=dw (X.getD (q+rг*st)б 0) def bx (X:у т) (st s:с):о-> с-> с-> FloatArray-> FloatArray | 0,_,_,Y=>Y | k+1,q,o,Y=>bx X st s k (q+s) (o+8) (s8 Y o (xr X q st 0) (xr X q st 1) (xr X q st 2) (xr X q st 3) (xr X q st 4) (xr X q st 5) (xr X q st 6) (xr X q st 7)) lemma dD (X:у i9) (d s:с):∀k (q o:с) (Y:FloatArray), qб+k*sб+8*dб+oб+8*k oб+8*k<= Yд -> (bx X d s k q o Y)д=Yд/\(∀p r<8->(bx X d s k q o Y).data[oб+8*τ+r]! =dw X[qб+τ*sб+r*dб]!:=by intro k;induction k with | zero=>intro q o Y _ _;exact ⟨rfl,λ_ _=>rfl,λτ r h=>absurd h А⟩ | succ k y=> intro q o Y v A;rw[ϋ] at v;have:=ς;have:=Ϟ;obtain ⟨l,t⟩:=dQ Y o (xr X q d) А;have u:(q+s)б=qб+sб:=ab А;have g:(o+8)б=oб+8:=by rw[ab (by simp;omega)];simp obtain ⟨w,e,x⟩:=y (q+s) (o+8) _ А (by rw[l];omega) rw[g] at e;rw[u,g] at x;refine ⟨by rw[bx,w,l],λp B=>by rw[bx,e p А,t p А,if_neg А],λτ r z j=>?_⟩ rw[bx];rcases τ with _ | τ .have m:(rг*d)б=r*dб:=by rw[li,aa А,ξ (by have:=Ζ dб j.le;omega)] rw[e _ А,t _ А,if_pos А,show oб+8*0+r-oб=r by omega,xr, ab (by rw[m];have:=Ζ dб j.le;omega),m,gD];simp .grind def ZT:у FloatArray:=Array.ofFn (n:=10) λk=>⟨Array.replicate (2^(kи+7)) 0⟩ def zT (n:о):FloatArray:= let k:=Nat.log2 (8*n)+1-7 if k<10 then ZT[k]! else ⟨Array.replicate (8*n) 0⟩ lemma gu (n:о):8*n<=(zT n)д/\((zT n)д=8*n\/(zT n)д<=2^16):=by unfold zT;dsimp only;split .rw[getElem!_pos ZT _ (by simp[ZT];omega)] simp only[ZT,Ϩ,jD,ϴ] exact ⟨(Ϸ (n:=8*n)).le.trans (Ε Б А), .inr (Ε Б А)⟩ .simp[jD] @[inline] def rX (X:у т) (i:с):р:=if h:i р) (bpf:Unit-> р) (fbk:Unit-> т):т:= let r:=sT p n 0 (bpf ()) 0 let c:=if 1<= r.2а/\r.2а<=1993/\1076<= r.2а+L then ai r.1 (r.2а+L-1076)ж else 0x100000000 if c<0x100000000 then act relu cл else fbk () @[inline] def tf (relu:ф) (S:р) (hh:Д) (sl:Unit-> т):т:= let c:=ai S hh if c<0x100000000 then act relu cл else sl () lemma gg (X:FloatArray) (i:о):X.get! i=X.data[i]!:=by rcases X with ⟨d⟩;rfl lemma gk (z:ℝ): |Model.roundAt i5 z-z| <= (2:ℝ)^(-53:п)* |z| +2^(-1075:п):=by by_cases h: |z| <(2:ℝ)^(-1021:п) .refine (re z (-1021) le_rfl h).trans ?_ rw[div_eq_mul_inv,<- zpow_sub_one₀ two_ne_zero];norm_num .have j:0< |z| :=lt_of_lt_of_le В (not_lt.1 h) have d:=lv (b:=2) Г j;have e:=kK (b:=2) Г |z| simp only[j0] at d e have g:(-1021:п)<= ky 2 |z| +1:=by by_contra l;linarith[zpow_le_zpow_right₀ (by norm_num:(1:ℝ)<=2) (by omega:Int.log 2 |z| +1<=-1021)] refine (re z _ g e).trans ?_ rw[div_eq_mul_inv,<- zpow_sub_one₀ two_ne_zero,show ky 2 |z| +1-53-1=-53+ky 2 |z| by ring, zpow_add₀ two_ne_zero] linarith[mul_le_mul_of_nonneg_left d (by positivity:(0:ℝ)<=2^(-53:п)), show (0:ℝ)<=2^(-1075:п) by positivity] lemma iN (x y:р) (g:fv x) (h:fv y) (d: |rv x+rv y| <= (2:ℝ)^(970:п)): fv (x+y) /\ |rv (x+y)-(rv x+rv y)| <= (2:ℝ)^(-53:п)* |rv x+rv y| +2^(-1075:п):=by obtain ⟨f,e⟩:=db x y g h (d.trans ((zpow_le_zpow_right₀ Г Г).trans (pm 971 le_rfl)));exact ⟨f,by rw[e];exact gk _⟩ lemma iO (x y:р) (g:fv x) (h:fv y) (d: |rv x*rv y| <= (2:ℝ)^(971:п)): fv (x*y) /\ |rv (x*y)-rv x*rv y| <= (2:ℝ)^(-53:п)* |rv x*rv y| +2^(-1075:п):=by obtain ⟨f,e⟩:=d4 x y g h d;exact ⟨f,by rw[e];exact gk _⟩ lemma fe (v:р) (d:fv v) (e:eF v.toBits=0): rv v=(⟨v.toBits>>>63!=0,(v.toBits&&&0xfffffffffffff)а,-1074⟩:jf).toReal:=by unfold eF at e;unfold fv at d;unfold rv;rw[dc] at d⊢;rw[jK,ϒ _ _ _ _ (fq v).1 (fq v).2 d,ite_eq_left (by rw[e];rfl)] split_ifs with g .dsimp only;rw[aw,aw,g];simp .rfl lemma bu (v:р) (e:fv v): |rv v| <(2:ℝ)^(((eF v.toBits)а:п)-1022):=by have g:=(fq v).2;by_cases d:eF v.toBits=0 .rw[fe v e d,aw,show (eF v.toBits)а=0 by rw[d];rfl, show (2:ℝ)^(((0:о):п)-1022)=2^52*2^(-1074:п) by rw[show (2:ℝ)^52=2^(52:п) by norm_num,<- zpow_add₀ two_ne_zero];norm_num] have:((v.toBits&&&0xfffffffffffff)а:ℝ)<2^52:=by exact_mod_cast g split<;>simp only[neg_mul,abs_neg,abs_mul,abs_zpow,abs_two,lS]<;> exact mul_lt_mul_of_pos_right this В .rw[aK v e d,aw,show (2:ℝ)^(((eF v.toBits)а:п)-1022)= 2^53*2^(((eF v.toBits)а:п)-1075) by rw[show (2:ℝ)^53=2^(53:п) by norm_num,<- zpow_add₀ two_ne_zero];congr 1;ring] have:(((v.toBits&&&0xfffffffffffff)а+2^52:о):ℝ)<2^53:=by exact_mod_cast (by omega:(v.toBits&&&0xfffffffffffff).toNat+2^52<2^53) split<;>simp only[neg_mul,abs_neg,abs_mul,abs_zpow,abs_two,lS]<;> exact mul_lt_mul_of_pos_right this В lemma gm (p:о-> р) (z:о-> ℝ) (d:ℝ) (n:о) (I:∀t t<= n-> fv a -> |rv a-(d+∑s∈i0 t,z s)| <= t*((2:ℝ)^(-53:п)*(1+2^(-20:п))*(|d| +∑s∈i0 t,|z s|)+2^(-1074:п)) -> fv (ac p n t a) /\ |rv (ac p n t a)-(d+∑s∈i0 n,z s)| <= n*((2:ℝ)^(-53:п)*(1+2^(-20:п))*(|d| +∑s∈i0 n,|z s|)+2^(-1074:п)):=by have j:(2:ℝ)^(970:п)=2^(968:п)*4:=by rw[show (970:п)=968+2 by norm_num,zpow_add₀ two_ne_zero];norm_num have K:(2:ℝ)^(-1075:п)=2^(-1074:п)/2:=by rw[show (-1074:п)=-1075+1 by norm_num,zpow_add_one₀ two_ne_zero];ring have r:(4294967296:ℝ)*2^(-1074:п)<=2^(968:п):=by rw[show (4294967296:ℝ)=2^(32:п) by norm_num,<- zpow_add₀ two_ne_zero] exact zpow_le_zpow_right₀ Г Г have l:(0:ℝ)<2^(-1074:п):=В;intro m;induction m with | zero=> intro t a G J o h;obtain rfl:t=n:=А;rw[ac,if_neg (lt_irrefl _)];exact ⟨o,h⟩ | succ m L=> intro t a G J o h;have g:tabs_nonneg (z i)) have w:=(abs_add_le d _).trans (add_le_add le_rfl (Ϲ z (i0 (t+1))));simp only[ϝ] at v w;have x:=abs_add_le (rv a-(d+∑s∈i0 t,z s)) (d+(∑s∈i0 t,z s+z t)) rw[show rv a-(d+∑s∈i0 t,z s)+(d+(∑s∈i0 t,z s+z t))=rv a+rv (p t) by rw[y];ring] at x have e:(t:ℝ)<=4294967296:=by exact_mod_cast (by omega:t<=2^32) have M:=mul_le_mul_of_nonneg_right e (abs_nonneg d);have N:=mul_le_mul_of_nonneg_right e (ϡ λi (_:i∈i0 t)=>abs_nonneg (z i)) have V:=mul_le_mul_of_nonneg_right e (abs_nonneg (z t));have O:=mul_le_mul_of_nonneg_right e l.le;have q:0<= ∑s∈i0 t,|z s| :=ϡ λi _=>abs_nonneg (z i) have W:=mul_nonneg (lj t:(0:ℝ)<= t) (abs_nonneg (z t));have Q:=abs_nonneg d;have S:=abs_nonneg (z t) have E: |rv a-(d+∑s∈i0 t,z s)| <= 1/9007199254740992*(1+1/1048576)*(t* |d|)+ 1/9007199254740992*(1+1/1048576)*(t*∑s∈i0 t,|z s|)+t*2^(-1074:п):=h.trans_eq (by ring) obtain ⟨B,A⟩:=iN a (p t) o D (by rw[j];generalize (2:ℝ)^(968:п)=H at*;generalize (2:ℝ)^(-1074:п)=η at* linarith only[x,E,w,v,F,M,N,O,r,q,Q,S,l]) refine L (t+1) (a+p t) А А B ?_;rw[K,show (2:ℝ)^(-53:п)=1/9007199254740992 by norm_num] at A have u:=abs_add_le (rv (a+p t)-(rv a+rv (p t))) (rv a-(d+∑s∈i0 t,z s)) rw[show rv (a+p t)-(rv a+rv (p t))+(rv a-(d+∑s∈i0 t,z s))= rv (a+p t)-(d+(∑s∈i0 t,z s+z t)) by rw[y];ring] at u simp only[ϝ];generalize (2:ℝ)^(-1074:п)=η at* calc _<=1/9007199254740992*(1+1/1048576)*(t* |d| +t*∑s∈i0 t,|z s| +t* |z t| + (|d| +(∑s∈i0 t,|z s| + |z t|)))+t*η+η:=by linarith _=_:=by push_cast;ring lemma fx (m:Float.Model):(kY m.unpack.abs).unpack=m.unpack.abs:=by have d:(kY m.unpack).unpack=m.unpack:=by have:=Model.toFloatModel_ofFloatModel m;conv_rhs=>rw[<- this] rfl generalize m.unpack=u at d⊢;simp only[kY,Float.Model.unpack,UInt64.toBitVec_ofBitVec] at d⊢;cases u with | notANumber=>exact d | finite s h e g=> simp only[jm,jA,jG] at d⊢;split_ifs at d⊢<;> simp only[jc,ύ, ώ,kb] at d⊢<;> split_ifs at d⊢<;>simp_all | _=> simp only[jm,jA,jG, lD,jc, ύ,ώ, kb] at d⊢ split_ifs at d⊢<;>simp_all lemma gE (v:р) (d:fv v):fv v.abs/\rv v.abs= |rv v| :=by have e:v.abs.toModel.unpack=v.toModel.unpack.abs:=fx v.toModel;rw[bB] at d⊢;rw[cf,cf,e];generalize v.toModel.unpack=u at d⊢;cases u with | notANumber | infinity _=>simp[jn] at d | zero _=>simp[jm,jn,jp,jU] | finite s j e h=> refine ⟨by simp[jm,jn],?_⟩ simp only[jm,Model.unpackedToReal_finite,abs_mul];have g:=lx jh e;split<;>split<;>simp_all[abs_of_pos g] lemma gX (S:р) (l:fv S) (h:Д) (B:hа<2^63) (T:ℝ) (A: |rv S-T| <= (2:ℝ)^(hа:п)) (d:ai S h<0x100000000): |T| <= (2:ℝ)^(425:п):=by unfold ai at d;dsimp only at d;split at d swap;. exact absurd d Б rename_i g;simp only[υ,decide_eq_true_eq] at g;obtain ⟨⟨⟨q,r⟩,t⟩,u⟩:=g;obtain ⟨v,w,j,x,-,-,-,m⟩:=fJ h (eF S.toBits) (S.toBits&&&0xfffffffffffff) B (fq S).1 (fq S).2 q r t (rb _ u);have e:=aK S l (λy=>by rw[y] at j;simp at j) rw[aw] at e;generalize (eF S.toBits)а=E at v w j x m e;generalize (S.toBits&&&0xfffffffffffff)а=f at m e;have p:(0:ℝ)<2^((E:п)-1075):=В have z:((f+2^52:о):ℝ)+((2^(hа+1075-E):о):ℝ)<=2^53:=by exact_mod_cast (by omega:f+2^52+2^(h.toNat+1075-E)<=2^53) have l: |rv S| =((f+2^52:о):ℝ)*2^((E:п)-1075):=by rw[e,abs_mul,abs_of_pos p];split<;>simp only[abs_neg,lS] have:=abs_sub (rv S) (rv S-T);rw[sub_sub_cancel,l] at this rw[show (2:ℝ)^(hа:п)=((2^(hа+1075-E):о):ℝ)*2^((E:п)-1075) by push_cast;rw[<- zpow_natCast,<- zpow_add₀ two_ne_zero];congr 1;omega] at A have o:(2:ℝ)^(53:о)*2^((E:п)-1075)<=2^(425:п):=by rw[<- zpow_natCast,<- zpow_add₀ two_ne_zero];exact zpow_le_zpow_right₀ Г А linarith[mul_le_mul_of_nonneg_right z p.le] lemma fO (n:о) (e g:о-> i9) (d:am n e g) (S:р) (j:fv S) (h:Д) (o:hа<2^63) (l: |rv S-(ah n e g:ℝ)| <= (2:ℝ)^(hа:п)) (m:ai S h<0x100000000):(ai S h)л=kB n e g:= cw n e g d S j h o l (gX S j h o _ l m) m lemma dx (Y:FloatArray) (g:Yд<2^32) (i:с) (v:р):wF Y i v=Y.set! iб v:=by rcases Y with ⟨d⟩;unfold wF;split next h=>simp only[l6,kt,l9,l8,lE];rw[dite_eq_left (show iб simp only[kt,l8,lE] rw[dite_eq_right λe=>h (by rw[γ,lY,aa (lt_of_lt_of_le g ς)];exact e)] lemma dr (X:у i9) (e:Xв<2^32) (i:с):rX X i=dw X[iб]!:=by unfold rX;split .rw[bt] next h=> rw[getElem!_neg X _ λd=>h (by rw[γ,kk,aa (lt_of_lt_of_le e ς)];exact d)];rfl lemma b7 (p:о-> р) (n:о):∀m t a,n-t=m -> ac p (n+1) (t+1) a=ac (λτ=>p (τ+1)) n t a:=by intro m;induction m with | zero=>intro t a h;unfold ac;rw[if_neg А,if_neg А] | succ m d=>intro t a h;unfold ac;rw[if_pos А,if_pos А];exact d (t+1) _ А lemma gW (n:ℕ) (σ j E A C H M:ℝ) (u:0<= σ) (d:0omega obtain ⟨w,h⟩:=cy (9*(n+1))ж.toInt64 (by rw[e];simp;omega) rw[e] at h;push_cast at h have r:(2:ℝ)^(((eF ((9*(n+1))ж.toInt64.toFloat*a).toBits)а:п)-1022) <= 2^(((cE (9*(n+1))ж.toInt64.toFloat a)а:п)+56):=by apply zpow_le_zpow_right₀ Г;unfold cE;dsimp only;split .rw[χ _ _ (UInt64.le_of_lt ‹_›)];have:=ν.mp ‹_› simp only[iZ] at this⊢;omega .have:=κ.mp (UInt64.not_lt.mp ‹_›);simp only[iZ] at this⊢;omega have t:(n:ℝ)<=536870912:=by exact_mod_cast H.le have I:(2:ℝ)^(-1074:п)=2^(-1075:п)*2:=by rw[<- zpow_add_one₀ two_ne_zero];norm_num have V:(2:ℝ)^(-1075:п)*2^64<=2^(-900:п):=by rw[<- zpow_natCast,<- zpow_add₀ two_ne_zero];exact zpow_le_zpow_right₀ Г Г have S:(2:ℝ)^40*2^(400:п)<=2^(971:п):=by rw[<- zpow_natCast,<- zpow_add₀ two_ne_zero];exact zpow_le_zpow_right₀ Г Г have U:(1:ℝ)<=2^(400:п):=one_le_zpow₀ Г Г;have g:(0:ℝ)<2^(-1075:п):=В;have F:(2:ℝ)^(-900:п)<=1:=zpow_le_one_of_nonpos₀ Г Г rw[show (2:ℝ)^(-53:п)=1/9007199254740992 by norm_num,show (2:ℝ)^(-20:п)=1/1048576 by norm_num, I,mul_add,<- mul_assoc] at d have W:=mul_le_mul_of_nonneg_right t g.le;generalize G:(n:ℝ)*(1/9007199254740992*(1+1/1048576))=K at d;have m:K<=1/8388608:=by rw[<- G];nlinarith have X:=mul_le_mul_of_nonneg_right m u have z: |rv a| <= 3*2^(400:п):=by have:=abs_sub_abs_le_abs_sub (rv a) σ;rw[abs_of_nonneg u] at this;generalize (2:ℝ)^(-1075:п)=y at*;generalize (2:ℝ)^(-900:п)=ε at* generalize (2:ℝ)^(400:п)=Z at*;linarith have E: |rv (9*(n+1))ж.toInt64.toFloat*rv a| <= 2^(971:п):=by rw[h,abs_mul,abs_of_pos В];have:=mul_le_mul_of_nonneg_left z (by positivity:(0:ℝ)<=9*(n+1)) have:=mul_le_mul_of_nonneg_right t (by positivity:(0:ℝ)<=2^(400:п)) generalize (2:ℝ)^(400:п)=Z at*;generalize (2:ℝ)^(971:п)=L at*;linarith obtain ⟨o,j⟩:=iO _ a w D E;have O:=lt_of_le_of_lt' r (lt_of_le_of_lt (abs_nonneg _) (bu _ o));have M:=lt_of_lt_of_le (lt_of_le_of_lt (le_abs_self _) (bu _ o)) r;rw[h,show (2:ℝ)^(-53:п)=1/9007199254740992 by norm_num] at j rw[show (2:ℝ)^(-20:п)=1/1048576 by norm_num] generalize (2:ℝ)^(((cE (9*(n+1))ж.toInt64.toFloat a)а:п)+56)=Q at* generalize rv ((9*(n+1))ж.toInt64.toFloat*a)=P at* generalize rv a=A at* generalize (2:ℝ)^(-1075:п)=y at* generalize (2:ℝ)^(-900:п)=ε at* have l:(n:ℝ)*(y*2)<=1073741824*y:=by linarith generalize (n:ℝ)*(y*2)=v at d l;have q:(0:ℝ)<=9*(n+1):=В;have B:=mul_le_mul_of_nonneg_right (by linarith:9*((n:ℝ)+1)<=2^33) g.le generalize 9*((n:ℝ)+1)=N at* obtain ⟨x,-⟩:=abs_le.mp d;rcases le_or_gt 0 A with p | p .rw[abs_of_nonneg (mul_nonneg q p)] at j have:=mul_le_mul_of_nonneg_left x (by linarith:0<= N*(1-1/9007199254740992)) nlinarith[(abs_le.mp j).1] .have:=mul_le_mul_of_nonneg_left (by linarith:σ<=2*v) q nlinarith lemma fW (x:i9) (d:i7 x≠255): |rv (dw x)| <= 2^(277:п):=by rw[(av x d).2,abs_mul,abs_pow,abs_two];have:(i7 x)е≠255:=λh=>d (Η.mp (by simpa using h)) have:=bO x calc _<=(2:ℝ)^24*2^253:=mul_le_mul (by rw[<- ϕ];exact_mod_cast (bV x).le) (pow_le_pow_right₀ Г (by rw[br];omega)) В В _=2^(277:п):=by rw[<- pow_add,<- zpow_natCast];rfl lemma f0:fv (0:р)/\rv (0:р)=0:=by have e:(0:р).toModel.unpack=.zero .positive:=rfl;refine ⟨by rw[bB,e];rfl,by rw[cf,e];simp[jp,jU]⟩ lemma io (b s d τ r:о) (o:s<2^32) (g:d<2^32) (p:τ<2^32) (l:r<2^32) (h:b+τ*s+r*d<2^32): (bг+τг*sг+rг*dг)б=b+τ*s+r*d:=by have:=ς;have:=Ϟ have m:∀x y:о,x<2^32-> y<2^32-> x*y<2^32->(xг*yг)б=x*y:= λx y q t h=>by rw[li,aa А,aa А,ξ А] have e:=m τ s p o А;have j:=m r d l g А rw[ab (by rw[ab (by rw[aa А,e];omega),aa А,e,j];omega), ab (by rw[aa А,e];omega),aa А,e,j] lemma fw (b:i9) (d:о) (g:je b<= d): |(tm kf b:ℝ)| <= 2^(173+d):=by unfold tm rw[show sv kf=2^23 by decide,show je kf=126 by decide,Int.cast_mul,Int.cast_mul,abs_mul,abs_mul, Int.cast_pow,Int.cast_pow,Int.cast_ofNat,abs_pow,abs_pow,abs_two] have e: |(sv b:ℝ)| <= 2^24:=by rw[<- ϕ];exact_mod_cast (bV _).le calc (2:ℝ)^23* |(sv b:ℝ)| *2^(126+je b)<=2^23*2^24*2^(126+d):=by gcongr;norm_num _=2^(173+d):=by rw[<- pow_add,<- pow_add];congr 1;omega lemma fh (b:Д):(eF b)а<=2047:=by unfold eF;simp only[ψ,iZ];exact ϙ lemma ff (F a:р):(cE F a)а<=969:=by unfold cE;dsimp only;split .rename_i h;have:=fh (F*a).toBits;have d:=ν.mp h rw[χ _ _ (UInt64.le_of_lt h)];simp only[iZ] at d⊢;omega .simp abbrev Iv (F:о-> т) (a:у т) (P:о-> Prop) (A:у т):Prop:= Aв=aв /\ ∀q,(A[q]?=a[q]? \/ A[q]?=some (F q))/\(P q-> q A[q]?=some (F q)) lemma cz (F:о-> i9) (e g:у i9) (S U:о-> Prop) (j:∀q,U q-> S q) (h:Iv F e S g):Iv F e U g:= ⟨h.1,λq=>⟨(h.2 q).1,λd l=>(h.2 q).2 (j q d) l⟩⟩ def aV (A:у т) (e:с) (he:e<= A.usize) (i:с) (m:Е):Е:= if h:i>>23)&&&255)) else m termination_by eб-iб decreasing_by have:=γ.mp h;rw[al h];omega lemma cL (A:у i9) (e:с) (d:e<= A.usize):∀k (i:с) (m:Е),eб-iб=k -> mе<=(aV A e d i m)е /\ ∀q,iб<= q-> q(i7 A[q]!)е<=(aV A e d i m)е:=by intro k;induction k with | zero=> intro i m o;rw[aV,dif_neg λh=>by have:=γ.mp h;omega];exact ⟨le_rfl,λq v g=>by omega⟩ | succ k u=> intro i m o;have h:i>>23)&&&255)) (by rw[al h];omega) rw[UInt32.toNat_max] at r;refine ⟨by omega,λq l g=>?_⟩ by_cases p:q=iб .subst p;rw[<- bt A i (ay j)];unfold i7;omega .exact t q (by rw[al h];omega) g lemma dN (n:о) (e d:о-> i9):∀c i,i+c=n -> dallNZ (jv (n:=n+1) λt=>if tиif tиe tи) (jv (n:=n) λt=>d tи) i c:=by intro c;induction c with | zero=> intro i h;obtain rfl:i=n:=А simp only[dallNZ,ae (i+1) (λt=>if t< i then d t else kf) i А, ae (i+1) (λt=>if t< i then e t else 0x80000000) i А,lt_irrefl,if_false];rfl | succ c g=> intro i h rw[dallNZ,g (i+1) А,dallNZ,ae (n+1) (λt=>if tif t i9) (h:0if tif tby split;exacts [(g t ‹_›).symm,by decide],aU _ _ _ g,aE, dN n d e n 0 А] congr 1 .simp only[lt_irrefl,if_false,show tm kf 0x80000000=0 by decide,add_zero] exact Ο rfl λt j=>by simp only[if_pos (Ν.mp j)];unfold tm;rw[ϔ];ring .simp[h.ne'] end F lemma co {a:о} (h:a<=4294967295):a<2^32:=А end Dense namespace Bn namespace NativeAdd lemma cu (x:Float32):ly x.toModel=ofW x.toBits:= congrArg Model.mk (ofUInt32_bits x.toBits).symm lemma fk (x:Float32):jH (ly x.toModel)=x.toBits:= UInt32.ofNat_toNat lemma aZ (a:i9) (h:i7 a≠255): (kI a).toBits=a/\(kI a).isFinite=true:=by have g:lp (spec:=ju) a.toBitVec≠-1#8:=λd=> h (Η.mp ((show (i7 a)е=(a.toBitVec.extractLsb' 23 8).toNat by simp only[i7,Λ,Ρ,BitVec.extractLsb'_toNat];exact θ _ 8).trans (congrArg BitVec.toNat d:))) have e:(kI a).toBits=a:=by change UInt32.ofBitVec (jA ju (jc ju a.toBitVec))=a rw[Model.pack_unpack_eq,if_neg (g ·.1)] refine ⟨e,?_⟩;change (jc ju (kI a).toBits.toBitVec).isFinite=true;simp only[e,jc,g,ite_false];split_ifs<;>rfl @[noinline] def cN (relu:ф) (a b:т):т:= act relu (toWord (Model.add (ofW a) (ofW b))) @[inline] def cK (relu:ф) (w:т):т:= w&&&~~~((0:т)-((if relu then w>>>31 else 0)&&&(if w&&&0x7FFFFFFF<=0x7F800000 then 1 else 0))) lemma gQ (w:i9):(w&&&0x80000000!=0)=decide (2^31<= wе):=by have e:=w.toNat_lt rw[ϻ,bne_iff_ne,ne_eq,<- Η,Λ,decide_eq_true_iff, show (0x80000000:Е)е=2^31 from rfl,lc] simp only[j5,Nat.testBit,ι,Nat.one_and_eq_mod_two];constructor .intro h;by_contra d;apply h;rw[ϣ А];simp .intro h;rw[show wе/2^31=1 by omega];simp lemma dA (d:ф) (w:i9):cK d w=act d w:=by have v:=w.toNat_lt;have t:(w>>>31)е=wе/2^31:=by rw[Ρ];simp[ι] have m:=Dense.aR w;have q:=Dense.be w have r:(lW w)е=wе%2^23:=by unfold lW;rw[Λ];exact θ _ 23 unfold Dense.aS at m q have o:∀x:i9,x&&&~~~((0:i9)-0)=x:=λx=>by apply Η.mp;rw[Λ];rw[show (~~~((0:i9)-0))е=2^32-1 from rfl,θ,ξ x.toNat_lt] have u:∀x:i9,x&&&~~~((0:i9)-1)=0:=λx=>by apply Η.mp;rw[Λ];simp have j:w>>>31=if 2^31<= wе then 1 else 0:=by apply Η.mp;rw[t];split<;>simp<;>omega have p:(w&&&0x7FFFFFFF<=0x7F800000)↔wе%2^31<=0x7F800000:=by rw[UInt32.le_iff_toNat_le,m];rfl have l:(w&&&0x80000000!=0&&!(i7 w=255&&lW w !=0))=true↔ (2^31<= wе/\wе%2^31<=0x7F800000):=by rw[gQ] simp only[υ,decide_eq_true_eq,Bool.not_eq_true',Bool.and_eq_false_iff,decide_eq_false_iff_not, bne_eq_false_iff_eq,<- Η,q,r,m,jj,j5] omega unfold cK act;cases d .simp only[ο,ite_false,UInt32.zero_and,o] simp only[ite_true];unfold reluW;rw[j];by_cases e:2^31<= wе .rw[if_pos e] by_cases g:wе%2^31<=0x7F800000 .rw[if_pos (p.mpr g),show (1:i9)&&&1=1 from rfl,u,if_pos (l.mpr ⟨e,g⟩)] .rw[if_neg (mt p.mp g),show (1:i9)&&&0=0 from rfl,o,if_neg (λh=>g (l.mp h).2)] .rw[if_neg e,UInt32.zero_and,o,if_neg (λh=>e (l.mp h).1)] @[inline] def add (relu:ф) (a b:т):т:= if expOf a !=255&&expOf b !=255 then cK relu (Float32.ofBits a+Float32.ofBits b).toBits else cN relu a b lemma dV (d:ф) (a b:i9): add d a b=act d (jH (lB (ofW a) (ofW b))):=by unfold add;split .rename_i h rw[dA];simp only[υ,bne_iff_ne] at h;have e:=aZ a h.1;have g:=aZ b h.2;have j:=ExecFloat.Binary.toModel_ofFloat32_add_of_isFinite _ _ e.2 g.2;simp only[ExecFloat.Binary.toModel_ofFloat32,cu,e.1,g.1] at j;rw[show lB (ofW a) (ofW b)=ofW (Float32.ofBits a+Float32.ofBits b).toBits from j.symm,<- cu,fk] .rfl end NativeAdd @[inline] def ad (rb:Е) (a b:т) (_slow:Unit-> т):т:=NativeAdd.add (rb !=0) a b @[specialize] def bW (stop:с) (f:(i:с)-> iб т-> т) (i:с) (x:у т) (h:stopб<= xв):у т:= if hi:i iб i9-> i9) (F:о-> i9-> i9) (l:∀i e w,f i e w=F iб w) (i:с) (x:у i9) (h:dб<= xв): (bW d f i x h)в=xв /\ ∀j,(bW d f i x h)[j]?=if iб<= j/\j refine ⟨by rw[g.1,ϑ],λj=>?_⟩ rw[g.2,Dense.al e,lT,lM А];split_ifs<;>first | rfl | omega | (subst_vars;rw[kL А,Option.map_some,l];rfl) .next i x h e=>exact ⟨rfl,λj=>by rw[if_neg (by rw[γ] at e;omega)]⟩ lemma fd (d:ф) (a b:i9) (e:Unit-> i9) (g:e ()=act d (jH (lB (ofW a) (ofW b)))): ad (if d then 1 else 0) a b e=act d (jH (lB (ofW a) (ofW b))):=by cases d<;>simp[ad,NativeAdd.dV] @[noinline] def gH (relu:ф) (x y:т):т:=act relu (toWord (Model.add (ofW x) (ofW y))) def bq (relu:ф) (a b:у т):у т:= if h:aв<= bв/\aв let y:=b.uget i (by rw[Dense.aa h.2] at hi;omega) ad rb x y λ_=>gH relu x y) 0 a (by rw[Dense.aa h.2]) else addReluSpec relu a b lemma cg:bq=addReluSpec:=by funext d a b;unfold bq;dsimp only split;swap;. rfl rename_i h;have g:=Dense.aa h.2;refine lN λj=>?_ rw[(cI _ _ (λj x=>act d (jH (lB (ofW x) (ofW b[j]!)))) (λi l x=>?_) 0 a _).2 j, addReluSpec,lF] .by_cases e:j>>31)-1) else w lemma fc (d:ф) (w:i9) (m:i7 w≠255):aF d w=act d w:=by unfold aF act reluW;cases d .simp have l:=aP w have j:(w>>>31)е=wе/2^31:=by rw[Ρ];simp[ι] have o:=w.toNat_lt;by_cases h:2^31<= wе .have g:w>>>31=1:=Η.mp (by rw[j];simp only[UInt32.toNat_one];omega) have e:jw w=true:=l.mpr h;unfold jw at e;simp[g,e,m] .have g:w>>>31=0:=Η.mp (by rw[j];simp only[j5];omega) have e:jw w≠true:=λq=>h (l.mp q) unfold jw at e;simp only[Bool.not_eq_true] at e;simp[g,e] lemma fg (S:р) (h:Д) (e:ai S h<0x100000000):i7 (ai S h)л≠255:=by unfold ai at e⊢;dsimp only at e⊢;split at e swap;. exact absurd e Б rename_i d;rw[if_pos d];simp only[υ,decide_eq_true_eq] at d;obtain ⟨⟨⟨-,l⟩,-⟩,-⟩:=d have m:(eF S.toBits)а<2048:=by unfold eF;rw[ψ];exact lt_of_le_of_lt ϙ Б have o:(S.toBits&&&0xfffffffffffff)а<2^52:=by rw[ψ];exact lt_of_le_of_lt ϙ Б rw[ν,Κ] at l;simp only[iZ] at l;have p:1195<=(eF S.toBits)а:=А;have r:=fK S.toBits p;have q:S.toBitsа/2^63<2:=by have:=S.toBits.toNat_lt;omega rw[ν] at e;simp only[iZ] at e;intro g;have j:=congrArg UInt32.toNat g;rw[i7,Λ,Ρ,ϟ] at j;simp only[jj,jb,ι] at j;rw[θ _ 8,ξ e,r] at j;omega @[inline] def cH (relu:ф) (S:р) (hh:Д) (sl:Unit-> т):т:= let c:=ai S hh if c<0x100000000 then aF relu cл else sl () lemma eU (d:ф) (S:р) (e:Д) (g:Unit-> i9):cH d S e g=tf d S e g:=by unfold cH tf;dsimp only;split .rename_i h;rw[fc _ _ (fg _ _ h)] .rfl lemma gS (x w:i9) (e:о) (d:(i7 w)е<= e): |(tm x w:ℝ)| <= |(sv x:ℝ)*2^je x| *2^(lm e 56+23):=by unfold tm;push_cast rw[show (sv x:ℝ)*sv w*2^(je x+je w)=(sv x*2^je x)*(sv w*2^je w) by rw[pow_add];ring,abs_mul] gcongr;rw[abs_mul,abs_pow,abs_two] refine (mul_le_mul (b:=2^24) (by rw[<- ϕ];exact_mod_cast (bV _).le) (pow_le_pow_right₀ Г (by rw[br];omega:_<= max e 56-1)) В В).trans_eq ?_ rw[<- pow_add];congr 1;omega lemma iD (l:ф) (n:о) (j g:о-> i9) (d:i9) (p:о-> р) (F v L:о) (e:i9) (c r:Д) (S:р) (o u:Unit-> i9) (E:∀s fv (p s)/\rv (p s)=tm (j s) (g s)) (Z:S=ac p n 0 (dw kf*dw d)) (N:∀sif sif s u ()=act l (kB (n+1) (λs=>if sif sif sif s(2:ℝ)^a<=2^b:=pow_le_pow_right₀ Г;generalize Y:(if eк<56 then 56 else eк)+23+c=q have hq:qа=lm eе 56+23+cа:=by have:=UInt32.toNat_lt e rw[<- Y];split<;>rename_i h<;>simp only[ν,Χ,μ, iZ] at h⊢<;>omega split;swap;. exact B rename_i hg;simp only[υ,decide_eq_true_eq,ϖ,κ, jj,iZ] at hg generalize W:(if qrename_i h<;>simp only[ν] at h<;>omega have D:∀sby have:=N s m;simp[h] at this;omega have K:=ey kf d Б t.1;generalize y:(∑s∈i0 n,|rv (dw (j s))|)=z at w have I:0<= z:=y ▸ ϡ λ_ _=>abs_nonneg _ rw[zpow_add₀ two_ne_zero,zpow_natCast] at w;have Q:=fw d v t.2;have J:(n:ℝ)<=2^32:=by exact_mod_cast (show n<=2^32 by omega) have X:z<= n*2^277:= y ▸ (Ϗ λs (m:s∈i0 n)=>fW _ (E s (Ν.1 m))).trans_eq (by simp) have hZ:∑s∈i0 n,|(tm (j s) (g s):ℝ)| <= 2^(lm eе 56+23)*z:=by rw[<- y,kJ] exact Ϗ λs m=>by rw[(av _ (E s (Ν.1 m))).2];exact (gS _ _ _ (N s (Ν.1 m))).trans_eq (mul_comm _ _) have U: |(tm kf d:ℝ)| +∑s∈i0 n,|(tm (j s) (g s):ℝ)| <= 2^(968:п):=by rw[show (2:ℝ)^(968:п)=2^967+2^967 by rw[<- two_mul,<- pow_succ'];norm_num] refine add_le_add (Q.trans (P А)) (hZ.trans ((mul_le_mul (P (by omega:_<=400)) (X.trans (mul_le_mul_of_nonneg_right J В)) I В).trans ?_)) rw[<- pow_add,<- pow_add];exact P Г obtain ⟨H,G⟩:=gm p (λs=>(tm (j s) (g s):ℝ)) (tm kf d:ℝ) n (λs m=>hp s m (D s m)) А U n 0 _ А (km _) K.1 (by rw[K.2];simp) rw[<- Z] at H G have hT:(ah (n+1) (λs=>if sif sby simp[Ν.1 m] have V: |rv S-(ah (n+1) (λs=>if sif sif sif sby by_cases h:ksimp only[h,↓reduceIte];exacts [⟨E k h,D k h⟩,⟨by decide,t.1⟩] rw[fO _ _ _ hf S H A А V x] .exact hk D lemma fu (d:ф) (n:о) (g h:о-> i9) (p:о-> р) (e:Unit-> р) (L:о) (m:Unit-> i9) (z:∀s split next y=> obtain ⟨l,j⟩:=eK _ _ (tm (g n) (h n)) n r.2а t.1 t.2.1 z n 0 _ 0 rfl А o.1 (by simp[o.2]) (by rw[w]) rw[w] at j l have x:((r.2а+L-1076)ж)а=r.2а+L-1076:=by rw[jL,Ξ (by simp only[jT];omega)] refine congrArg _ (fO _ _ _ q _ l _ (by rw[x];omega) ?_ y) rw[aE,x];unfold ah;push_cast;rw[add_comm] exact j.trans ((mul_le_mul_of_nonneg_right (by exact_mod_cast (by omega:n<=2^L):(n:ℝ)<=2^L) В).trans_eq (by rw[<- zpow_natCast,<- zpow_add₀ two_ne_zero];exact congrArg (2^·) А)) .exact v .rw[if_neg Б];exact v end F end Dense namespace Sr structure Ent {α:Type} (f:у т-> у т-> о-> α) where w:у т b:у т n:о v:α ok:v=f w b n a:с structure St {α:Type} (f:у т-> у т-> о-> α) where e:у (Ent f) x:ByteArray hd:о tl:о u:о structure Tab {α:Type} (f:у т-> у т-> о-> α) where r:ST.Ref Unit (St f) z:Ent f zx:ByteArray cap:о variable {α:Type} {f:у i9-> у i9-> о-> α} def Tab.gM (f:у т-> у т-> о-> α) (N cap:о):Tab f:= let z:Ent f:=⟨#[],#[],0,f #[] #[] 0,rfl,0⟩ let zx:ByteArray:=⟨Array.replicate (4*N) 0⟩ ⟨(ST.Prim.mkRef ⟨Array.replicate N z,zx,0,0,0⟩ (Void.mk ())).val,z,zx,cap⟩ @[inline] def Ent.dh (e:Ent f) (w b:у т) (n:о):ф:= e.n==n&&withPtrEq e.w w (λ_=>e.w==w) (λh=>by rw[h];simp)&& withPtrEq e.b b (λ_=>e.b==b) (λh=>by rw[h];simp) lemma Ent.cx {e:Ent f} {w b:у i9} {n:о} (h:e.dh w b n=true):e.v=f w b n:=by simp only[Ent.dh,withPtrEq,υ,beq_iff_eq] at h;obtain ⟨⟨d,g⟩,j⟩:=h;rw[e.ok,d,g,j] @[inline] def Ent.sz (e:Ent f):о:=e.wв+e.bв+64 @[inline] def hs (a:с):с:=(((a>>>4).toUInt64*0x9E3779B97F4A7C15)>>>48).toUSize lemma ul {β:Type} {a:у β} {i:с} (h:i с-> ByteArray | 0,_=>x | p+1,i=> let k:=i&&&m if h:k St f-> St f | 0,s=>s | p+1,s=>if s.u+sz<= t.cap then s else St.eH t sz p (s.dX t.z) @[noinline] def Tab.cU (t:Tab f) (w b:у т) (n:о) (a:с):{y // y=f w b n}:= let y:=f w b n let q:Ent f:=⟨w,b,n,y,rfl,a⟩ let sz:=q.sz if 4*sz<= t.cap then let s:=(ST.Prim.Ref.get t.r (Void.mk ())).val let s:=St.eH t sz s.eв s let s:=if (s.e.getD s.tl t.z).w.isEmpty then s else s.dX t.z let e:=s.e.setIfInBounds s.tl q let x:=eX e (t.zx.usize-1) 0 t.zx let o:=(ST.Prim.Ref.swap t.r ⟨e,x,s.hd,(s.tl+1)%eв,s.u+sz⟩ (Void.mk ())).val if o.u=0xFFFFFFFFFFFF then if h:(o.e.getD 0 t.z).dh w b n=true then ⟨_,Ent.cx h⟩ else ⟨y,rfl⟩ else ⟨y,rfl⟩ else ⟨y,rfl⟩ def St.cr (s:St f) (t:Tab f) (w b:у т) (n:о) (a m:с):о-> с-> {y // y=f w b n} | 0,_=>t.cU w b n a | p+1,i=> let k:=i&&&m if h:kSubtype.ext (p.2.trans q.2.symm)⟩ @[inline] def Tab.get (t:Tab f) (w b:у т) (n:о):{y // y=f w b n}:= withPtrAddr w (λa=> let s:=(ST.Prim.Ref.get t.r (Void.mk ())).val s.cr t w b n a (s.x.usize-1) s.x.size (hs a)) (λ_ _=>Subsingleton.elim _ _) end Sr open Sr namespace Dense namespace F namespace Pn def dR (X:у т) (st:с):о-> с-> с-> FloatArray-> р-> FloatArray | 0,_,o,Y,a=>wF Y o a | k+1,q,o,Y,a=>let v:=rX X q;dR X st k (q+st) (o+1) (wF Y o v) (a+v.abs) def dO (X:у т) (st s m:с) (n:о):о-> с-> с-> FloatArray-> FloatArray | 0,_,_,Y=>Y | k+1,q,o,Y=>dO X st s m n k (q+s) (o+m) (dR X st n q o Y 0) def qL (W:у т) (su m:с) (n:о):о-> с-> FloatArray-> FloatArray | 0,_,Y=>Y | k+1,q,Y=>qL W su m n k (q+m) (bx W su 1 n q (q+1) Y) lemma dv (q d:с) (τ:о):q+d+τг*d=q+(τ+1)г*d:=by rw[ϛ,ϛ,USize.ofNat_add,USize.add_mul,show USize.ofNat 1=1 from rfl,USize.one_mul, USize.add_assoc,USize.add_comm d] lemma uz (q d:с):q+(0:о)г*d=q:=by simp[ϛ,show USize.ofNat 0=0 from rfl] lemma dH (X:у i9) (d:с):∀k (q o:с) (Y:FloatArray) (a:р), Yд<2^32-> oб+k (dR X d k q o Y a)д=Yд /\ (∀i,i i(dR X d k q o Y a).data[i]! =Y.data[i]!) /\ (∀τ(rX X (q+τг*d)).abs) k 0 a:=by intro k;induction k with | zero=> intro q o Y a g l;rw[dR,dx Y g,ac,if_neg А];refine ⟨bD ..,λi e v=>?_,λτ h=>absurd h А,?_⟩ .rw[sg _ _ _ _ e,if_neg А] .rw[sg _ _ _ _ l,if_pos А] | succ k u=> intro q o Y a g l;have:=ς have e:(o+1)б=oб+1:=by rw[ab (by simp only[jd];omega)];simp only[jd] rw[dR,dx Y g] obtain ⟨m,p,r,t⟩:=u (q+d) (o+1) (Y.set! oб (rX X q)) (a+(rX X q).abs) (by rw[bD];exact g) (by rw[bD,e];omega) rw[bD] at m;refine ⟨m,λi j w=>?_,λτ h=>?_,?_⟩ .rw[p i (by rw[bD];exact j) А,sg _ _ _ _ j,if_neg А] .rcases τ with _ | τ .rw[p _ (by rw[bD];omega) А,sg _ _ _ _ А,if_pos А,uz] .have:=r τ А rw[e,show oб+1+τ=oб+(τ+1) by omega] at this rw[this,dv] .have:=t rw[e,show oб+1+k=oб+(k+1) by omega] at this rw[this];conv_rhs=>rw[ac,if_pos А,b7 _ k _ 0 _ rfl] simp only[dv,uz] lemma dF (X:у i9) (d s m:с) (n:о) (v:mб=n+1) (F:n+1<2^32): ∀k (q o:с) (Y:FloatArray),Yд<2^32-> oб+k*(n+1)<= Yд -> (dO X d s m n k q o Y)д=Yд /\ (∀i,i i(dO X d s m n k q o Y).data[i]! =Y.data[i]!) /\ (∀j(rX X (q+jг*s+τг*d)).abs) n 0 0):=by intro k;induction k with | zero=>intro q o Y _ _;exact ⟨rfl,λ_ _ _=>rfl,λj h=>absurd h А,λj h=>absurd h А⟩ | succ k z=> intro q o Y p w;rw[ϋ] at w;have:=ς;have g:(o+m)б=oб+(n+1):=by rw[ab А,v] obtain ⟨e,A,B,D⟩:=dH X d n q o Y 0 p А obtain ⟨u,l,x,y⟩:=z (q+s) (o+m) (dR X d n q o Y 0) (by rw[e];exact p) (by rw[e,g];omega) rw[e] at u;rw[dO];refine ⟨u,λi r E=>?_,λj h τ t=>?_,λj h=>?_⟩ .rw[l i (by rw[e];exact r) А,A i r А] .rcases j with _ | j .rw[la,Ϫ,l _ (by rw[e];omega) А,B τ t,uz] .have:=x j А τ t rw[g,show oб+(n+1)+j*(n+1)=oб+(j+1)*(n+1) by rw[ϋ];omega] at this rw[this,dv] .rcases j with _ | j .rw[la,Ϫ,l _ (by rw[e];omega) А,D] simp only[uz] .have:=y j А rw[g,show oб+(n+1)+j*(n+1)=oб+(j+1)*(n+1) by rw[ϋ];omega] at this rw[this];simp only[dv] lemma dP (W:у i9) (d m:с) (n:о) (A:mб=8*n) (B:dб=n): ∀k (q:с) (Y:FloatArray),2*(qб+k*(8*n))+32*n<2^32-> qб+k*(8*n)+1<= Yд -> (qL W d m n k q Y)д=Yд /\ (∀i,i(qL W d m n k q Y).data[i]! =Y.data[i]!) /\ ∀gintro q Y _ _;exact ⟨rfl,λ_ _=>rfl,λg h=>absurd h А⟩ | succ k E=> intro q Y x y;rw[ko,l0] at x y;have:=ς;have e:(q+m)б=qб+8*n:=by rw[ab А,A] have j:(q+1)б=qб+1:=by rw[ab (by simp only[jd];omega)];simp only[jd] obtain ⟨u,v,w⟩:=dD W d 1 n q (q+1) Y (by simp only[jd,j];omega) (by rw[j];omega) simp only[jd,ϱ,B,j] at v w;obtain ⟨p,t,D⟩:=E (q+m) (bx W d 1 n q (q+1) Y) (by rw[e];omega) (by rw[u,e];omega) rw[u] at p;rw[qL];refine ⟨p,λi z=>?_,λg h τ o r l=>?_⟩ .rw[t i А,v i z] .rcases g with _ | g .rw[la,Ϫ,t _ (by rw[e];omega),w τ r o l,Ϫ] .have:=D g А τ o r l rw[e,show qб+8*n+g*(8*n)=qб+(g+1)*(8*n) by rw[ko,l0];omega] at this exact this @[inline] def pp (V P:FloatArray) (vo xb r s:о):р:=V.get! (vo+s)*P.get! (xb+8*s+r) @[noinline] def sQ (n:о) (relu:ф) (X W b:@& у т) (V P:@& FloatArray) (vo xb r xo st j:о):т:= tS relu (Nat.log2 (n+1)+1) n (pp V P vo xb r) (λ_=>dw oneW*dw b[j]!) λ_=>ap n relu X W b xo st j @[inline] def pO (relu ok:ф) (hh:Д) (n:о) (X W b:у т) (xo st o r:о) (V P:FloatArray) (vo:с) (q:с) (on:ф) (acc:у т) (S:р):у т:= if h:on=true/\qsQ n relu X W b V P voб (o*n+1) r xo st (o+r)) else ap n relu X W b xo st (o+r)) (ay h.2) else acc @[noinline] def fP (relu ok:ф) (hh:Д) (n:о) (X W b:у т) (xo st o:о) (q0 so mu:с) (V P:FloatArray) (vo:с) (a0 a1 a2 a3 a4 a5 a6 a7:р) (acc:у т):у т:= pO relu ok hh n X W b xo st o 7 V P vo (q0+7*so) (decide (7< mu)) (pO relu ok hh n X W b xo st o 6 V P vo (q0+6*so) (decide (6< mu)) (pO relu ok hh n X W b xo st o 5 V P vo (q0+5*so) (decide (5< mu)) (pO relu ok hh n X W b xo st o 4 V P vo (q0+4*so) (decide (4< mu)) (pO relu ok hh n X W b xo st o 3 V P vo (q0+3*so) (decide (3< mu)) (pO relu ok hh n X W b xo st o 2 V P vo (q0+2*so) (decide (2< mu)) (pO relu ok hh n X W b xo st o 1 V P vo (q0+1*so) (decide (1< mu)) (pO relu ok hh n X W b xo st o 0 V P vo (q0+0*so) (decide (0< mu)) acc a0) a1) a2) a3) a4) a5) a6) a7 lemma dI (d Z:ф) (N:Д) (n:о) (X W b:у i9) (B A o:о) (r l p:с) (V P:FloatArray) (vo:с) (D E G H J K L M:р) (m:у i9) (F:о-> i9) (as:rб+8*lб<=4294967295) (hz:mв<=4294967295) (hv:∀k<8,k(if Z then cH d (A8.f ⟨D,E,G,H,J,K,L,M⟩ k) N (λ_=>sQ n d X W b V P voб (o*n+1) k B A (o+k)) else ap n d X W b B A (o+k))= F (rб+k*lб)): Iv F m (λq=>∃k,k<8/\k∃j,j k<8->(k USize.toNat z=I k)-> on=decide (k Q (k+1) (pO d Z N n X W b B A o k V P vo z on a (A8.f ⟨D,E,G,H,J,K,L,M⟩ k)):=by intro k a z on ⟨h1,y⟩ hk S x;unfold pO;split next v=> have w:k?_⟩ rw[lT,lM,hv k hk w];by_cases h:zб=q .subst h;simp[S w,I] .rw[if_neg h] exact ⟨(y q).1,λ⟨j,O,t,u⟩=>(y q).2 ⟨j,Nat.lt_of_le_of_ne (Nat.le_of_lt_succ O) λe=>by subst e;exact h ((S t).trans u.symm),t,u⟩⟩ next v=> refine ⟨h1,λq=>⟨(y q).1,λ⟨j,O,t,u⟩ U=>(y q).2 ⟨j,Nat.lt_of_le_of_ne (Nat.le_of_lt_succ O) λe=>v ⟨by simp[x];omega,?_⟩,t,u⟩ U⟩⟩ subst e;rw[γ,kk,aa А,S t,<- u];omega have Y:∀c:с,cб<8->(r+c*l)б=rб+cб*lб:=λc v=>by have m1:cб*lб<=8*lб:=Ζ _ v.le have e:(c*l)б=cб*lб:=by rw[li,<- Ϟ,ξ А] rw[ab А,e] unfold fP refine g 7 (g 6 (g 5 (g 4 (g 3 (g 2 (g 1 (g 0 ?_ ?_ ?_ ?_) ?_ ?_ ?_) ?_ ?_ ?_) ?_ ?_ ?_) ?_ ?_ ?_) ?_ ?_ ?_) ?_ ?_ ?_) ?_ ?_ ?_ all_goals first | decide | (intro _;rw[Y _ (by simp only[jd];omega)];simp only[jd,I]) | simp only[γ,jd] | simp[Q,Iv] def pk (V P:FloatArray) (vo nu:с) (hs:Vд<2^32/\Pд<2^32) (hV:voб+nuб<= Vд) (t i:с) (hi:iб+8*(nuб-tб)<= Pд) (a0 a1 a2 a3 a4 a5 a6 a7:р) (relu ok:ф) (hh:Д) (n:о) (X W b:у т) (xo st o:о) (q0 so mu:с) (acc:у т): у т:= if h:t iб=j+8*tб -> pk V P d g hs Y t i I v w x y z A B D l M H n X W b S Q o N O L u= fP l M H n X W b S Q o N O L V P d (ac (pp V P dб j 0) gб tб v) (ac (pp V P dб j 1) gб tб w) (ac (pp V P dб j 2) gб tб x) (ac (pp V P dб j 3) gб tб y) (ac (pp V P dб j 4) gб tб z) (ac (pp V P dб j 5) gб tб A) (ac (pp V P dб j 6) gб tб B) (ac (pp V P dб j 7) gб tб D) u:=by intro m;induction m<;>intro t i I v w x y z A B D hm K .rw[pk,dif_neg (by rw[γ];omega)] have e:∀p a,ac p gб tб a=a:=λp a=>by rw[ac,if_neg А] simp only[e] rename_i ih;have:=ς;have J:tбby rw[ac,if_pos J] have e:∀(c:с) (r:о) (G:cб=r) (Z:r<8) (E:(d+t)бby rw[ug,ug,pp,gg,gg,hw,ab А,K,G] rw[pk,dif_pos h] rw[ih (t+1) (i+8) _ _ _ _ _ _ _ _ _ (by rw[al h];omega) (by rw[al h,U,K];ring),al h, q 0 v,q 1 w,q 2 x,q 3 y,q 4 z,q 5 A,q 6 B,q 7 D] simp only[e 0 0 (by simp) А,e 1 1 (by simp) А,e 2 2 (by simp) А,e 3 3 (by simp) А, e 4 4 (by simp) А,e 5 5 (by simp) А,e 6 6 (by simp) А,e 7 7 (by simp) А] @[specialize] def l2 (U V:о) (f:о-> о-> у т-> у т) (u v:о) (a:у т):у т:= if u о-> у i9-> у i9) (F:о-> i9) (C:о-> о-> о-> Prop) (D:∀u v a,u v aв=N-> Iv F a (C u v) (f u v a)) (u v:о) (a:у i9): aв=N->(∀q,(∃d g,d q a[q]?=some (F q)) -> (l2 U V f u v a)в=aв /\ ∀q,(∃d g,d q(l2 U V f u v a)[q]?=some (F q):=by induction u,v,a using l2.induct U V f with | case1 u v a m x y=> intro w r;rw[l2,if_pos m,if_pos x];obtain ⟨E,z⟩:=D u v a m x w obtain ⟨G,H⟩:=y А λq ⟨d,g,o,p,A,l⟩ j=>by have t:qH q B А⟩ | case2 u v a m x y=> intro w r;rw[l2,if_pos m,if_neg x];exact y w λq ⟨d,g,o,p,A,l⟩ j=>r q ⟨d,g,o,p,by omega,l⟩ j | case3 u v a m=> intro w r;rw[l2,if_neg m];exact ⟨rfl,λq ⟨d,g,o,p,l⟩ j=>r q ⟨d,g,o,p,by omega,l⟩ j⟩ lemma d6 (U V N:о) (f:о-> о-> у i9-> у i9) (F:о-> i9) (C:о-> о-> о-> Prop) (l:∀u v a,u v aв=N-> Iv F a (C u v) (f u v a)) (j:∀q,q ∃u v,uF qи:=by obtain ⟨p,e⟩:=dJ U V N f F C l 0 0 (jM N 0) (by simp) λq ⟨r,t,_,_,h,_⟩ _=>А apply lN;intro q;by_cases d:qdw oneW*rX bw oг) (8*G) (FloatArray.emptyWithCapacity (8*G)),bw,aI W 0 0,aI bw 0 0⟩ def oF (t:ф) (R n ow:о) (relu:ф) (X W b:у т) (q:о):т:= act relu (dotOf (n+1) (λs=>if sif s о) (g:о-> р) (o:∀τ(g τ).abs) n 0 0))а:п)+56)+ 2^(-900:п):=by have m:0<= ∑τ∈i0 n,|rv (dw X[f τ]!)| :=ϡ λ_ _=>abs_nonneg _ have e:∑τ∈i0 n,|rv (dw X[f τ]!)| <= 2^(400:п):=by refine (Ϗ λτ _=>fW _ (j _)).trans ?_ have:(n:ℝ)<=2^29:=by exact_mod_cast h.le rw[kg,ϯ,nsmul_eq_mul] calc (n:ℝ)*2^(277:п)<=2^29*2^(277:п):=by gcongr _<=2^(400:п):=by rw[<- zpow_natCast,<- zpow_add₀ two_ne_zero];exact zpow_le_zpow_right₀ Г Г obtain ⟨l,d⟩:=gm (λτ=>(g τ).abs) (λτ=> |rv (dw X[f τ]!)|) 0 n (λτ p=>by rw[o τ p];exact gE _ (av _ (j _)).1) А (by simpa using e.trans (zpow_le_zpow_right₀ Г (by norm_num:(400:ℤ)<=968))) n 0 0 rfl (km _) f0.1 (by simp[f0.2]) simp only[abs_zero,zero_add,abs_abs] at d;exact dE n h _ _ l m e d lemma cX (t:ф) (R n d:о) (l:ф) (X W u:у i9) (Y Q B:FloatArray) (F:р) (hb e6:Д) (G:ф) (N:Yд<2^32/\Qд<2^32) (x:Bд<2^32) (e:i9) (S U L:о) (a1:L=Nat.log2 (n+1)+1) (a6:e6=if eк<56 then 56 else eк) (w:G=decide (e<255)) (hF:F=(9*(n+1))ж.toInt64.toFloat) (a7:hb=(S+L-50)ж) (hx:∀q:о,i7 X[q]!≠255) (A:∀q:о,i7 u[q]!≠255/\je u[q]! <= U) (ba:174+U<= S) (hL:n+2<=2^L) (z:L<=27) (H:S+L<=425) (hn:8*n<2^32) (he:∀q:о,(i7 W[q]!)е<= eе) (b1:R*(n+1)<= Yд) (a4:∀j∃k,k<8/\8*g+kby rw[ug,ab А,p,hc,as _ ho] have a3:∀h,Y.uget (r*(n+1)+n)г h=Y.data[r*(n+1)+n]!:=λh=>by rw[ug,ts h1.le N.1] have m1:8*g*R<= d*R:=Ζ R bz.le;have m2:r*d<= R*d:=Ζ d M.le;have cm:d*R=R*d:=ϩ _ _ have D:(if t then 8*g*R+r else r*d+8*g)гб=if t then 8*g*R+r else r*d+8*g:= aa (by cases t<;>simp only[ο,↓reduceIte]<;>omega) have E:(if t then R else 1)гб=if t then R else 1:= aa (by cases t<;>simp only[ο,↓reduceIte]<;>omega) have J:(min 8 (d-8*g))гб=min 8 (d-8*g):=aa А have hI:∀k,(if t then 8*g*R+r else r*d+8*g)+k*(if t then R else 1)= if t then (8*g+k)*R+r else r*d+(8*g+k):=λk=>by cases t<;>simp only[ο,↓reduceIte,ϱ,ko]<;>omega have dm:∀a c m:о,c< m->(a*m+c)/m=a/\(a*m+c)%m=c:=λa c m h=> ⟨by rw[ϔ,kc _ _ А,ϣ h,j6], by rw[ϔ,ϵ,ξ h]⟩ unfold eO;dsimp only;rw[dif_pos ⟨h1,h2,y⟩,fl _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (8*g*n+1) _ _ _ _ _ _ _ _ _ _ _ _ rfl (by rw[bv];simp)] simp only[a3,bo,O,Ϥ];refine cz _ _ _ _ _ (λq ⟨k,hk,w,hq⟩=>⟨k,hk,?_,?_⟩) (dI _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ a _ ?_ А λk hk bd=>?_) .rw[D,E];cases t<;>simp only[ο,↓reduceIte]<;>omega rotate_left .rw[J];omega .rw[D,E,hI];exact hq rw[J] at bd;have w:8*g+k(simp only[A8.f];exact congrArg (ac _ n 0) (a0 _ _ (by simp only[jd]) А _ w)) rw[hA];simp only[O] have K:∀s fv (pp Y Q (r*(n+1)) (8*g*n+1) k s) /\ rv (pp Y Q (r*(n+1)) (8*g*n+1) k s)=tm X[(if t then r else r*n)+s*(if t then R else 1)]! W[(8*g+k)*n+s]!:= λs v h=>by rw[pp,gg,gg,a4 r M s v,hQ g hg s v k hk];exact ey _ _ (hx _) h have I:ap n l X W u (if t then r else r*n) (if t then R else 1) (8*g+k)= act l (kB (n+1) (λs=>if sif sX[(if t then r else r*n)+s*(if t then R else 1)]!) (λs=>W[(8*g+k)*n+s]!) u[8*g+k]! (pp Y Q (r*(n+1)) (8*g*n+1) k) S U _ e _ _ _ (λ_=>ap n l X W u (if t then r else r*n) (if t then R else 1) (8*g+k)) (λ_=>sQ n l X W u Y Q (r*(n+1)) (8*g*n+1) k (if t then r else r*n) (if t then R else 1) (8*g+k)) (λs _=>hx _) (A _) ba hL z H hn K rfl (λs _=>he _) (a5 r M) (Nat.le_trans (ff _ _) (by decide:969<=1000)) ?_ I (λhw=>?_)).trans ?_ .rw[jL,Ξ (by simp only[jT];omega)] .refine fu _ _ _ _ _ _ _ _ (λs v=>?_) ?_ (λs _=>?_) hL z I .simpa only[if_pos v] using K s v (hw s v) .simpa only[lt_irrefl,↓reduceIte] using ey kf u[8*g+k]! Б (A _).1 .by_cases h:ssimp only[h,↓reduceIte] exacts [⟨hx _,hw s h⟩,⟨by decide,(A _).1⟩] .unfold oF cases t .obtain ⟨V,Z⟩:=dm r (8*g+k) d w simp only[V,Z,ο,↓reduceIte,ϱ] .obtain ⟨V,Z⟩:=dm (8*g+k) r R M simp only[V,Z,↓reduceIte] @[inline] def eI (t:ф) (R n ow:о) (relu:ф) (X W:у т) (d:PD) (ex:т) (Y:FloatArray):у т:= let L:=Nat.log2 (n+1)+1 let ib:=174+(d.ebе-1) if h:ex<255/\d.eb<255/\ib+L<=425/\L<=27/\0 ap n relu X W d.bw (if t then qи%R else qи/ow*n) (if t then R else 1) (if t then qи/R else qи%ow) @[inline] def dt (t:ф) (R n ow:о) (relu:ф) (X W:у т) (d:PD) (ex:т):у т:= eI t R n ow relu X W d ex (dO X (if t then R else 1)г (if t then 1 else n)г (n+1)г n R (0:о)г 0 (zT ((R*(n+1)+7)/8))) lemma dM (W b:у i9) (n d:о) (w:0dw kf*rX (pd W b n).bw oг) (8*((O+7)/8)) _ (jE (8*((O+7)/8))) rfl (km _) have p:(pd W b n).Q=qL W nг (8*n)г n ((O+7)/8) (0:о)г (zT (n*((O+7)/8)+1)):=by simp only[pd,q];rfl have m:(pd W b n).B=bk (λo=>dw kf*rX (pd W b n).bw oг) (8*((O+7)/8)) (jE (8*((O+7)/8))):=by simp only[pd,q] refine ⟨λg v=>?_,λg v τ A r z=>?_,?_,λo y=>?_⟩ .have:=Ζ (8*n) (show g+1<=(O+7)/8 by omega) rw[ko,l0] at this;rw[p,B,show 8*g*n=g*(8*n) by ac_rfl];omega .have:=D g А τ A r z rw[h,j6] at this;rw[p,show 8*g*n=g*(8*n) by ac_rfl,this] congr 2;rw[ko,show 8*g*n=g*(8*n) by ac_rfl];omega .rw[m,e.1];omega .rw[m,e.2.2 o (km _) А] rw[dr _ l,aa А] lemma dp {c:Prop} [Decidable c] {α:Type} {a:c-> α} {b:¬c-> α} {y:α} (d:∀h:c,a h=y) (e:∀h,b h=y):dite c a b=y:=by by_cases h:c .rw[dif_pos h];exact d h .rw[dif_neg h];exact e h lemma cG (t:ф) (R n d:о) (e:ф) (X W b:у i9) (A:i9) (x:A=aI X 0 0): dt t R n d e X W (pd W b n) A=jv (n:=R*d) λq=>oF t R n d e X W (pd W b n).bw qи:=by have ul:=ς;unfold dt eI;dsimp only;refine dp (λh=>?_) λ_=>?_ swap .congr 1;funext q;unfold oF;cases t<;>simp only[ap,cJ,ϱ,↓reduceIte,ο] obtain ⟨L,U,V,Z,g5,g6,g7,g8,g9,u,v,M,N,O,Q,S⟩:=h;obtain ⟨G,H,I,J⟩:=dM W b n d g5 g8 g9 (co u);have D:=da X А (x ▸ L);have w:=da (pd W b n).bw А U have he:∀q:о,(i7 W[q]!)е<=(pd W b n).eе:=λq=>by by_cases m:qomega have z:(if t then 1 else n)<2^32:=by cases t<;>simp only[ο,↓reduceIte]<;>omega have y:(if t then R else 1)<2^32:=by cases t<;>simp only[ο,↓reduceIte]<;>omega have K:=dF X (if t then R else 1)г (if t then 1 else n)г (n+1)г n (aa А) А R (0:о)г 0 _ hZ (by simp only[Ϥ,j6];omega) simp only[Ϥ,j6] at K;obtain ⟨K1,-,E,F⟩:=K have p:∀jby have m1:=Ζ (if t then 1 else n) l.le;have m2:=Ζ (if t then R else 1) (show τ<= n+1 by omega) rw[dr X А,io 0 _ _ j τ z y А А А];cases t<;>simp only[ο,↓reduceIte,j6,ϱ] generalize dO X (if t then R else 1)г (if t then 1 else n)г (n+1)г n R (0:о)г 0 _=Y at* refine d6 _ _ _ _ _ (λg r q=>∃k,k<8/\8*g+kcX t R n d e X W _ Y _ _ _ _ _ _ _ _ (pd W b n).e _ ((pd W b n).ebе-1) _ rfl rfl rfl rfl rfl (λq=>(D q).1) w le_rfl hL Z V А he А (λj l τ o=>by rw[E j l τ o,p j l τ o]) (λj l=>by rw[F j l] exact cR X n А (λq=>(D q).1) (λτ=>(if t then j else j*n)+τ*(if t then R else 1)) _ (λτ o=>p j l τ o)) G H I J v g r hg hr a ha) λq m=>?_ have hw:0by subst h;simp at m have hR:0by subst h;simp at m cases t .have h1:=lk q d have B:=ϳ q hw;refine ⟨q%d/8,q/d,by omega,ϲ (by rwa[ϩ]),q%d%8,by omega,by omega,?_⟩ simp only[ο,↓reduceIte];rw[ϩ (q/d)];omega .have h1:=lk q R have B:=ϳ q hR;have h3:q/R?_ simp only[Array.size_ofFn] at e;have r:q/n< m:=ϲ e have w:(pd A #[] k).bw[q/n]! =0x80000000:=by rw[p,getElem!_pos _ _ (by rw[ϴ];omega),Array.getElem_replicate] simp only[Ϩ,oF,↓reduceIte,w,act,ϣ (show q< m*n by rwa[ϩ]), ξ r,la,j6,ο] exact (F.dz k (λt=>A[q/n*k+t]!) (λt=>B[q%n+t*n]!) j λt _=>⟨(u _).1,(v _).1⟩).trans (by simp only[ϔ (q%n)]) end Pn end F end Dense namespace CV theorem dotOf_congr {n : Nat} {fa fb ga gb : Nat → Word} (h1 : ∀ t, t < n → fa t = ga t) (h2 : ∀ t, t < n → fb t = gb t) : dotOf n fa fb = dotOf n ga gb := by unfold dotOf congr 1 · apply Array.ext (by simp) intro i hi _ simp only [Array.size_ofFn] at hi simp [Array.getElem_ofFn, h1 i hi] · apply Array.ext (by simp) intro i hi _ simp only [Array.size_ofFn] at hi simp [Array.getElem_ofFn, h2 i hi] /-- Patch matrix: row `i` (output position) holds the `taps` window values of group 0. -/ @[inline] def im2col (s : ConvShape) (inp : Array Word) : Array Word := Array.ofFn (n := (s.ho * s.wo) * s.taps) fun r => windowAt s inp 0 (r.val / s.taps / s.wo % s.ho) (r.val / s.taps % s.wo) (r.val % s.taps) /-- Ungrouped convolution as `lin` over the patch matrix, transposed back to NCHW. -/ @[inline] def convL (lin : Nat → Nat → Nat → Bool → Array Word → Array Word → Array Word → Array Word) (fb : ConvShape → Bool → Array Word → Array Word → Array Word → Array Word) (s : ConvShape) (relu : Bool) (inp wts b : Array Word) : Array Word := if s.groups = 1 ∧ 0 < s.taps then let P := s.ho * s.wo let L := lin P s.taps s.cout relu (im2col s inp) wts b Array.ofFn (n := s.cout * P) fun q => L[(q.val % P) * s.cout + q.val / P]! else fb s relu inp wts b theorem getElem!_ofFn' {n : Nat} (f : Fin n → Word) (k : Nat) (hk : k < n) : (Array.ofFn f)[k]! = f ⟨k, hk⟩ := by rw [getElem!_pos _ k (by simpa using hk), Array.getElem_ofFn] theorem convL_eq (lin : Nat → Nat → Nat → Bool → Array Word → Array Word → Array Word → Array Word) (fb : ConvShape → Bool → Array Word → Array Word → Array Word → Array Word) (hl : lin = linearWith dotOf) (hf : fb = conv2dWith dotOf) : convL lin fb = conv2dWith dotOf := by funext s relu inp wts b unfold convL split_ifs with h · obtain ⟨hg, hk⟩ := h subst hl have hP : 0 < s.ho * s.wo := Nat.mul_pos (by simp [ConvShape.ho]) (by simp [ConvShape.wo]) apply Array.ext (by simp [conv2dWith]) intro q hq1 hq2 simp only [Array.size_ofFn] at hq1 have ho : q / (s.ho * s.wo) < s.cout := (Nat.div_lt_iff_lt_mul hP).2 hq1 have hp : q % (s.ho * s.wo) < s.ho * s.wo := Nat.mod_lt _ hP have hr : (q % (s.ho * s.wo)) * s.cout + q / (s.ho * s.wo) < (s.ho * s.wo) * s.cout := by calc (q % (s.ho * s.wo)) * s.cout + q / (s.ho * s.wo) < (q % (s.ho * s.wo)) * s.cout + s.cout := by omega _ = (q % (s.ho * s.wo) + 1) * s.cout := by ring _ ≤ (s.ho * s.wo) * s.cout := Nat.mul_le_mul_right _ hp have hc : 0 < s.cout := Nat.lt_of_le_of_lt (Nat.zero_le _) ho have hdiv : ((q % (s.ho * s.wo)) * s.cout + q / (s.ho * s.wo)) / s.cout = q % (s.ho * s.wo) := by rw [Nat.add_comm, Nat.add_mul_div_right _ _ hc, Nat.div_eq_of_lt ho, Nat.zero_add] have hmod : ((q % (s.ho * s.wo)) * s.cout + q / (s.ho * s.wo)) % s.cout = q / (s.ho * s.wo) := by rw [Nat.add_comm, Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt ho] have hopg : s.opg = s.cout := by simp [ConvShape.opg, hg] have hg0 : q / (s.ho * s.wo) / s.opg = 0 := by rw [hopg]; exact Nat.div_eq_of_lt ho have hy : q % (s.ho * s.wo) / s.wo % s.ho = q / s.wo % s.ho := by rw [Nat.mul_comm s.ho s.wo, Nat.mod_mul_right_div_self, Nat.mod_mod] have hx : q % (s.ho * s.wo) % s.wo = q % s.wo := Nat.mod_mul_left_mod _ _ _ simp only [Array.getElem_ofFn] unfold linearWith rw [getElem!_ofFn' _ _ hr] simp only [conv2dWith, Array.getElem_ofFn, hdiv, hmod, hg0] congr 1 apply dotOf_congr · intro t ht split_ifs with htk · have hi : (q % (s.ho * s.wo)) * s.taps + t < (s.ho * s.wo) * s.taps := by calc (q % (s.ho * s.wo)) * s.taps + t < (q % (s.ho * s.wo)) * s.taps + s.taps := by omega _ = (q % (s.ho * s.wo) + 1) * s.taps := by ring _ ≤ (s.ho * s.wo) * s.taps := Nat.mul_le_mul_right _ hp unfold im2col rw [getElem!_ofFn' _ _ hi] have e1 : ((q % (s.ho * s.wo)) * s.taps + t) / s.taps = q % (s.ho * s.wo) := by rw [Nat.add_comm, Nat.add_mul_div_right _ _ hk, Nat.div_eq_of_lt htk, Nat.zero_add] have e2 : ((q % (s.ho * s.wo)) * s.taps + t) % s.taps = t := by rw [Nat.add_comm, Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt htk] simp only [e1, e2, hy, hx] · rfl · intro t ht rfl · rw [hf] end CV namespace RN open FloatLib.Floats.Formats.BinaryInterchange theorem dc {n : Nat} {a b c d : Nat → Word} (h : ∀ t, t < n → a t = c t) (g : ∀ t, t < n → b t = d t) : dotOf n a b = dotOf n c d := by unfold dotOf congr 1 <;> apply Array.ext (by simp) <;> intro i j _ <;> simp only [Array.size_ofFn] at j <;> simp [h i j, g i j] theorem ge {n : Nat} (f : Fin n → Word) (k : Nat) (h : k < n) : (Array.ofFn f)[k]! = f ⟨k, h⟩ := by rw [getElem!_pos _ k (by simpa using h), Array.getElem_ofFn] /-- Gate weight matrix: row `k` is `[wih[k]; whh[k]; bih[k]]`. -/ def mkW (rows inW H : Nat) (wih whh bih : Array Word) : Array Word := Array.ofFn (n := rows * (inW + H + 1)) fun i => let k := i.val / (inW + H + 1) let j := i.val % (inW + H + 1) if j < inW then wih[k * inW + j]! else if j < inW + H then whh[k * H + (j - inW)]! else bih[k]! def mkB (rows off : Nat) (b : Array Word) : Array Word := Array.ofFn (n := rows) fun k => b[off + k.val]! /-- `[x_t; h; 1]`. -/ def mkX (inW H : Nat) (x h : Array Word) (t : Nat) : Array Word := Array.ofFn (n := inW + H + 1) fun j => if j.val < inW then x[t * inW + j.val]! else if j.val < inW + H then h[j.val - inW]! else oneW theorem mulDiv {k n t : Nat} (hn : 0 < n) (ht : t < n) : (k * n + t) / n = k := by rw [Nat.add_comm, Nat.add_mul_div_right _ _ hn, Nat.div_eq_of_lt ht, Nat.zero_add] theorem mulMod {k n t : Nat} (ht : t < n) : (k * n + t) % n = t := by rw [Nat.add_comm, Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt ht] theorem mulLt {k n t m : Nat} (hk : k < m) (ht : t < n) : k * n + t < m * n := calc k * n + t < k * n + n := by omega _ = (k + 1) * n := by ring _ ≤ m * n := Nat.mul_le_mul_right _ hk /-- Element `k` of the fused gate `linear` is gate row `k`. -/ theorem gate_get (lin : Nat → Nat → Nat → Bool → Array Word → Array Word → Array Word → Array Word) (hl : lin = linearWith dotOf) (rows inW H : Nat) (x wih whh bih bhh h : Array Word) (t k : Nat) (hk : k < rows) : (lin 1 (inW + H + 1) rows false (mkX inW H x h t) (mkW rows inW H wih whh bih) (mkB rows 0 bhh))[k]! = gateWith dotOf inW H x wih whh bih bhh h t k := by subst hl have hn : 0 < inW + H + 1 := by omega unfold linearWith rw [ge _ _ (by simpa using hk)] simp only [Nat.one_mul, Nat.div_eq_of_lt hk, Nat.mod_eq_of_lt hk, act, Bool.false_eq_true, ite_false, gateWith] apply dc · intro j hj by_cases h1 : j < inW + H + 1 · simp only [h1, ite_true, Nat.zero_mul, Nat.zero_add] unfold mkX rw [ge _ _ h1] · have : j = inW + H + 1 := by omega subst this simp only [lt_irrefl, ite_false] split_ifs with a b <;> first | rfl | exact absurd a (by omega) | exact absurd b (by omega) · intro j hj by_cases h1 : j < inW + H + 1 · simp only [h1, ite_true] unfold mkW rw [ge _ _ (mulLt hk h1)] simp only [mulDiv hn h1, mulMod h1] by_cases a : j < inW · simp [a] · by_cases b : j < inW + H · simp [a, b] · have : j = inW + H := by omega subst this simp · have : j = inW + H + 1 := by omega subst this unfold mkB rw [ge _ _ hk] simp only [lt_irrefl, ite_false, Nat.zero_add] split_ifs with a b c <;> first | rfl | exact absurd a (by omega) | exact absurd b (by omega) | exact absurd c (by omega) abbrev Lin := Nat → Nat → Nat → Bool → Array Word → Array Word → Array Word → Array Word def preF (lin : Lin) (rows inW H : Nat) (x W B h : Array Word) (t : Nat) : Array Word := lin 1 (inW + H + 1) rows false (mkX inW H x h t) W B theorem preF_eq (lin : Lin) (hl : lin = linearWith dotOf) (rows inW H : Nat) (x wih whh bih bhh h : Array Word) (t : Nat) : preF lin rows inW H x (mkW rows inW H wih whh bih) (mkB rows 0 bhh) h t = Array.ofFn (n := rows) fun k => gateWith dotOf inW H x wih whh bih bhh h t k.val := by apply Array.ext · subst hl; simp [preF, linearWith] · intro k h1 h2 simp only [Array.size_ofFn] at h2 rw [← getElem!_pos _ k h1] unfold preF rw [gate_get lin hl rows inW H x wih whh bih bhh h t k h2, Array.getElem_ofFn] def lstmStepF (lin : Lin) (pd : DotFn) (sig tanh : Word → Word) (inW H : Nat) (x W B : Array Word) (t : Nat) (st : Array Word × Array Word) : Array Word × Array Word := let pre := preF lin (4 * H) inW H x W B st.1 t let cell := Array.ofFn (n := H) fun u => pd 2 (fun j => if j = 0 then sig pre[H + u.val]! else sig pre[u.val]!) (fun j => if j = 0 then (st.2)[u.val]! else tanh pre[2 * H + u.val]!) let hidden := Array.ofFn (n := H) fun u => toWord (Model.mul (ofW (sig pre[3 * H + u.val]!)) (ofW (tanh (cell[u.val]!)))) (hidden, cell) def lstmF (lin : Lin) (pd : DotFn) (sig tanh : Word → Word) (T inW H : Nat) (x wih whh bih bhh : Array Word) : Array Word := recurWith T H (lstmStepF lin pd sig tanh inW H x (mkW (4 * H) inW H wih whh bih) (mkB (4 * H) 0 bhh)) (Array.replicate H 0, Array.replicate H 0) theorem lstmF_eq (lin : Lin) (pd : DotFn) (hl : lin = linearWith dotOf) (hp : pd = dotOf) (sig tanh : Word → Word) : lstmF lin pd sig tanh = lstmWith dotOf sig tanh := by funext T inW H x wih whh bih bhh unfold lstmF lstmWith congr 1 funext t st unfold lstmStepF lstmStepWith rw [preF_eq lin hl, hp] def gruStepF (lin : Lin) (pd : DotFn) (sig tanh : Word → Word) (inW H : Nat) (x wih bih W B Wn Bn : Array Word) (t : Nat) (st : Array Word × Array Word) : Array Word × Array Word := let h := st.1 let pre := preF lin (2 * H) inW H x W B h t let r := Array.ofFn (n := H) fun u => sig pre[u.val]! let z := Array.ofFn (n := H) fun u => sig pre[H + u.val]! let hn := lin 1 H H false h Wn Bn let n := Array.ofFn (n := H) fun u => tanh <| pd (inW + 2) (fun j => if j < inW then x[t * inW + j]! else if j = inW then oneW else hn[u.val]!) (fun j => if j < inW then wih[(2 * H + u.val) * inW + j]! else if j = inW then bih[2 * H + u.val]! else r[u.val]!) let h' := Array.ofFn (n := H) fun u => pd 3 (fun j => if j = 2 then h[u.val]! else n[u.val]!) (fun j => if j = 0 then oneW else if j = 1 then negW z[u.val]! else z[u.val]!) (h', st.2) def mkWn (H : Nat) (whh : Array Word) : Array Word := Array.ofFn (n := H * H) fun i => whh[2 * H * H + i.val]! theorem hn_eq (lin : Lin) (hl : lin = linearWith dotOf) (H : Nat) (whh bhh h : Array Word) : lin 1 H H false h (mkWn H whh) (mkB H (2 * H) bhh) = Array.ofFn (n := H) fun u => dotOf (H + 1) (fun j => if j < H then h[j]! else oneW) (fun j => if j < H then whh[(2 * H + u.val) * H + j]! else bhh[2 * H + u.val]!) := by subst hl apply Array.ext (by simp [linearWith]) intro u h1 h2 simp only [Array.size_ofFn] at h2 simp only [linearWith, Array.getElem_ofFn, Nat.one_mul, Nat.div_eq_of_lt h2, Nat.mod_eq_of_lt h2, Nat.zero_mul, Nat.zero_add, act, Bool.false_eq_true, ite_false] apply dc · intro j _; rfl · intro j _ split_ifs with a · unfold mkWn rw [ge _ _ (mulLt h2 a)] congr 1 ring · unfold mkB rw [ge _ _ h2] theorem r_eq (lin : Lin) (hl : lin = linearWith dotOf) (sig : Word → Word) (inW H : Nat) (x wih whh bih bhh h : Array Word) (t : Nat) : (Array.ofFn (n := H) fun u => sig (preF lin (2 * H) inW H x (mkW (2 * H) inW H wih whh bih) (mkB (2 * H) 0 bhh) h t)[u.val]!) = Array.ofFn (n := H) fun u => sig (gateWith dotOf inW H x wih whh bih bhh h t u.val) := by congr 1; funext u unfold preF rw [gate_get lin hl _ _ _ _ _ _ _ _ _ _ _ (by omega)] theorem z_eq (lin : Lin) (hl : lin = linearWith dotOf) (sig : Word → Word) (inW H : Nat) (x wih whh bih bhh h : Array Word) (t : Nat) : (Array.ofFn (n := H) fun u => sig (preF lin (2 * H) inW H x (mkW (2 * H) inW H wih whh bih) (mkB (2 * H) 0 bhh) h t)[H + u.val]!) = Array.ofFn (n := H) fun u => sig (gateWith dotOf inW H x wih whh bih bhh h t (H + u.val)) := by congr 1; funext u unfold preF rw [gate_get lin hl _ _ _ _ _ _ _ _ _ _ _ (by omega)] def gruF (lin : Lin) (pd : DotFn) (sig tanh : Word → Word) (T inW H : Nat) (x wih whh bih bhh : Array Word) : Array Word := recurWith T H (gruStepF lin pd sig tanh inW H x wih bih (mkW (2 * H) inW H wih whh bih) (mkB (2 * H) 0 bhh) (mkWn H whh) (mkB H (2 * H) bhh)) (Array.replicate H 0, #[]) theorem gruF_eq (lin : Lin) (pd : DotFn) (hl : lin = linearWith dotOf) (hp : pd = dotOf) (sig tanh : Word → Word) : gruF lin pd sig tanh = gruWith dotOf sig tanh := by funext T inW H x wih whh bih bhh unfold gruF gruWith congr 1 funext t st unfold gruStepF gruStepWith simp only [] rw [r_eq lin hl, z_eq lin hl, hn_eq lin hl, hp] end RN namespace DW theorem dc {n : Nat} {a b c d : Nat → Word} (h : ∀ t, t < n → a t = c t) (g : ∀ t, t < n → b t = d t) : dotOf n a b = dotOf n c d := by unfold dotOf congr 1 <;> apply Array.ext (by simp) <;> intro i j _ <;> simp only [Array.size_ofFn] at j <;> simp [h i j, g i j] theorem ge {α : Type} [Inhabited α] {n : Nat} (f : Fin n → α) (k : Nat) (h : k < n) : (Array.ofFn f)[k]! = f ⟨k, h⟩ := by rw [getElem!_pos _ k (by simpa using h), Array.getElem_ofFn] theorem mulDiv {k n t : Nat} (hn : 0 < n) (ht : t < n) : (k * n + t) / n = k := by rw [Nat.add_comm, Nat.add_mul_div_right _ _ hn, Nat.div_eq_of_lt ht, Nat.zero_add] theorem mulMod {k n t : Nat} (ht : t < n) : (k * n + t) % n = t := by rw [Nat.add_comm, Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt ht] theorem mulLt {k n t m : Nat} (hk : k < m) (ht : t < n) : k * n + t < m * n := calc k * n + t < k * n + n := by omega _ = (k + 1) * n := by ring _ ≤ m * n := Nat.mul_le_mul_right _ hk abbrev Lin := Nat → Nat → Nat → Bool → Array Word → Array Word → Array Word → Array Word /-- Channel `c`'s patch matrix of the depthwise geometry `d`: row `p`, column `t`. -/ def imC (d : ConvShape) (inp : Array Word) (c : Nat) : Array Word := Array.ofFn (n := (d.ho * d.wo) * (d.kh * d.kw)) fun r => windowAt d inp c (r.val / (d.kh * d.kw) / d.wo % d.ho) (r.val / (d.kh * d.kw) % d.wo) (r.val % (d.kh * d.kw)) def dwL (lin : Lin) (fb : ConvShape → Bool → Array Word → Array Word → Array Word → Array Word) (s : ConvShape) (relu : Bool) (inp wts b : Array Word) : Array Word := if 0 < s.cin ∧ 0 < s.kh * s.kw then let d := s.depthwise let k := s.kh * s.kw let outs := Array.ofFn (n := s.cin) fun c => lin (d.ho * d.wo) k 1 relu (imC d inp c.val) (Array.ofFn (n := k) fun t => wts[c.val * k + t.val]!) #[b[c.val]!] Array.ofFn (n := s.cin * (d.ho * d.wo)) fun q => (outs[q.val / (d.ho * d.wo)]!)[q.val % (d.ho * d.wo)]! else fb s relu inp wts b theorem dwL_eq (lin : Lin) (fb : ConvShape → Bool → Array Word → Array Word → Array Word → Array Word) (hl : lin = linearWith dotOf) (hf : fb = depthwiseWith dotOf) : dwL lin fb = depthwiseWith dotOf := by funext s relu inp wts b unfold dwL split_ifs with h · obtain ⟨hc, hk⟩ := h subst hl have hcpg : s.depthwise.cpg = 1 := by simp [ConvShape.depthwise, ConvShape.cpg, Nat.div_self hc] have hopg : s.depthwise.opg = 1 := by simp [ConvShape.depthwise, ConvShape.opg, Nat.div_self hc] have htaps : s.depthwise.taps = s.kh * s.kw := by simp only [ConvShape.taps, hcpg, Nat.one_mul]; rfl have hdk : s.depthwise.kh * s.depthwise.kw = s.kh * s.kw := rfl generalize hP : s.depthwise.ho * s.depthwise.wo = P have p0 : 0 < P := hP ▸ Nat.mul_pos (by simp [ConvShape.ho]) (by simp [ConvShape.wo]) apply Array.ext (by simp [depthwiseWith, conv2dWith, ConvShape.depthwise, hP]) intro q h1 _ simp only [Array.size_ofFn] at h1 rw [hP] at h1 try simp only [hP] have o : q / P < s.cin := (Nat.div_lt_iff_lt_mul p0).2 h1 have p : q % P < P := Nat.mod_lt _ p0 have y : q % P / s.depthwise.wo % s.depthwise.ho = q / s.depthwise.wo % s.depthwise.ho := by rw [← hP, Nat.mul_comm s.depthwise.ho s.depthwise.wo, Nat.mod_mul_right_div_self, Nat.mod_mod] have z : q % P % s.depthwise.wo = q % s.depthwise.wo := by rw [← hP]; exact Nat.mod_mul_left_mod _ _ _ simp only [Array.getElem_ofFn] rw [ge _ _ o] unfold linearWith rw [ge _ _ (by simpa using p)] simp only [depthwiseWith, conv2dWith, Array.getElem_ofFn, hP, Nat.div_one, Nat.mod_one, hopg, htaps, Nat.zero_mul, Nat.zero_add] have hcout : s.depthwise.cout = s.cin := rfl congr 1 apply dc · intro t _ split_ifs with kt · have i : q % P * (s.kh * s.kw) + t < P * (s.kh * s.kw) := mulLt p kt unfold imC rw [ge _ _ (by rw [hdk, hP]; exact i)] simp only [hdk, hP, mulDiv hk kt, mulMod kt, y, z] · rfl · intro t _ split_ifs with kt · rw [ge _ _ kt] · simp · rw [hf] end DW def kernels:Kernels:= {I.kernels with dense:=⟨Dense.F.Pn.cP,Dense.F.Pn.ck⟩ conv:={I.kernels.conv with conv2d:=CV.convL Dense.F.Pn.cP I.convFast,depthwise:=DW.dwL Dense.F.Pn.cP (depthwiseWith Pinned.dotFn)} elem:={I.kernels.elem with addRelu:=Bn.bq} rnn:=⟨RN.lstmF Dense.F.Pn.cP Pinned.dotFn FastAct.sigmoidF FastAct.tanhF, RN.gruF Dense.F.Pn.cP Pinned.dotFn FastAct.sigmoidF FastAct.tanhF⟩} theorem correct:Obligation kernels:=by have h:=I.correct have hl:Dense.F.Pn.cP=linearWith dotOf:=by rw[Dense.F.Pn.dK];rfl have hc:CV.convL Dense.F.Pn.cP I.convFast=conv2dWith dotOf:= CV.convL_eq _ _ hl (by rw[I.convFast_eq,Pinned.dotFn_eq_dotOf]) have h1:=RN.lstmF_eq Dense.F.Pn.cP Pinned.dotFn hl Pinned.dotFn_eq_dotOf FastAct.sigmoidF FastAct.tanhF have h2:=RN.gruF_eq Dense.F.Pn.cP Pinned.dotFn hl Pinned.dotFn_eq_dotOf FastAct.sigmoidF FastAct.tanhF have hd:DW.dwL Dense.F.Pn.cP (depthwiseWith Pinned.dotFn)=depthwiseWith dotOf:= DW.dwL_eq _ _ hl (by rw[Pinned.dotFn_eq_dotOf]) unfold Obligation at h ⊢ unfold kernels rw[h,hc,hd,h1,h2,Dense.F.Pn.dK,Dense.F.Pn.cO,cg,FastAct.sigmoidF_eq,FastAct.tanhF_eq] rfl end Submission