public-compress-bound.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Spec.Public.Queries
2
3namespace ZlibF.Spec.Public.Proofs
4open ZlibF.Spec.Api
5
6private theorem bound_z_value (s : UInt64) :
7    (Zlib.Compress.compressBound_z s).toNat = compressBound s.toNat := by
8  have h12 : (s >>> 12).toNat = s.toNat / 4096 := by
9    rw [UInt64.toNat_shiftRight, Nat.shiftRight_eq_div_pow]
10    rfl
11  have h14 : (s >>> 14).toNat = s.toNat / 16384 := by
12    rw [UInt64.toNat_shiftRight, Nat.shiftRight_eq_div_pow]
13    rfl
14  have h25 : (s >>> 25).toNat = s.toNat / 33554432 := by
15    rw [UInt64.toNat_shiftRight, Nat.shiftRight_eq_div_pow]
16    rfl
17  have hs := s.toNat_lt
18  have hsum : (s + (s >>> 12) + (s >>> 14) + (s >>> 25) + 13).toNat =
19      (s.toNat + s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13) % 2 ^ 64 := by
20    simp only [UInt64.toNat_add, h12, h14, h25]
21    rw [show (13 : UInt64).toNat = 13 from rfl]
22    simp only [Nat.mod_add_mod]
23  have hinc : s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13 < 2 ^ 64 := by
24    omega
25  have hB2 : s.toNat + s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13 <
26      2 ^ 64 + 2 ^ 64 := by omega
27  unfold Zlib.Compress.compressBound_z compressBound
28  by_cases hB : s.toNat + s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13 < 2 ^ 64
29  · have hm : (s.toNat + s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13) % 2 ^ 64 =
30        s.toNat + s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13 := Nat.mod_eq_of_lt hB
31    have hnlt : ¬ s + (s >>> 12) + (s >>> 14) + (s >>> 25) + 13 < s := by
32      rw [UInt64.lt_iff_toNat_lt, hsum, hm]
33      omega
34    rw [ite_eq_right hnlt, hsum, hm, ite_eq_right (by omega)]
35  · have hm : (s.toNat + s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13) % 2 ^ 64 =
36        s.toNat + s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13 - 2 ^ 64 := by
37      rw [Nat.mod_eq_sub_mod (by omega), Nat.mod_eq_of_lt (by omega)]
38    have hlt : s + (s >>> 12) + (s >>> 14) + (s >>> 25) + 13 < s := by
39      rw [UInt64.lt_iff_toNat_lt, hsum, hm]
40      omega
41    rw [ite_eq_left hlt, ite_eq_left (by omega)]
42    rfl
43
44
45/-- `z_size_t compressBound_z(z_size_t sourceLen)` returns the saturated bound. -/
46theorem compressBound_z : Goal.compressBound_z := bound_z_value
47
48/-- `uLong compressBound(uLong sourceLen)` returns the saturated bound. -/
49theorem compressBound : Goal.compressBound := by
50  intro n
51  exact bound_z_value n
52
53#print axioms compressBound_z
54#print axioms compressBound
55end ZlibF.Spec.Public.Proofs