LZ77Copy.lean

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

1import ZlibF.Math.LZ77CopySpec
2
3/-!
4# Bytewise array copies implement the independent LZ77 operation
5
6The proof follows one byte at a time. The source of an overlapping copy
7is read from the updated array, exactly as copyBack reads growing output.
8-/
9
10set_option autoImplicit false
11
12namespace ZlibF.Math.LZ77Copy
13open C ZlibF.Spec Zlib.Inffast.Proofs
14
15private theorem written_length (bytes : Array UInt8) (offset count : Nat)
16    (hc : count ≤ offset) (hb : offset ≤ bytes.size) :
17    (writtenBytes bytes offset count).length = count := by
18  simp only [writtenBytes, List.length_take, List.length_drop, Array.length_toList]
19  omega
20
21private theorem written_get (bytes : Array UInt8) (offset count i : Nat) :
22    (writtenBytes bytes offset count)[i]? =
23      if i < count then bytes[offset - count + i]? else none := by
24  simp only [writtenBytes, List.getElem?_take, List.getElem?_drop, Array.getElem?_toList]
25
26private theorem written_set_append (bytes : Array UInt8) (offset count : Nat)
27    (value : UInt8) (hc : count ≤ offset) (hb : offset < bytes.size) :
28    writtenBytes (bytes.set! offset value) (offset + 1) (count + 1) =
29      writtenBytes bytes offset count ++ [value] := by
30  apply List.ext_getElem?
31  intro i
32  rw [written_get, List.getElem?_append, written_length bytes offset count hc (by omega)]
33  have hstart : offset + 1 - (count + 1) = offset - count := by omega
34  rw [hstart]
35  by_cases hi : i < count
36  · have hne : offset ≠ offset - count + i := by omega
37    simp [hi, show i < count + 1 by omega, written_get, Array.set!_eq_setIfInBounds,
38      Array.getElem?_setIfInBounds, hne]
39  · by_cases he : i = count
40    · subst i
41      have hs : offset - count + count = offset := by omega
42      simp [show ¬ count < count by omega, show count < count + 1 by omega, hs,
43        Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds, hb]
44    · have hn : ¬ i < count + 1 := by omega
45      have hz : i - count ≠ 0 := by omega
46      simp [hi, hn, List.getElem?_singleton, hz]
47
48private theorem output_source (dict : List UInt8) (bytes : Array UInt8)
49    (offset count dist : Nat) (hc : count ≤ offset) (hb : offset ≤ bytes.size)
50    (hd : 0 < dist) (hcount : dist ≤ count) :
51    (dict ++ writtenBytes bytes offset count).getD
52      ((dict ++ writtenBytes bytes offset count).length - dist) 0 =
53        bytes.getD (offset - dist) 0 := by
54  rw [List.length_append, written_length bytes offset count hc hb]
55  have hidx : dict.length + count - dist = dict.length + (count - dist) := by omega
56  have hright : dict.length ≤ dict.length + (count - dist) := by omega
57  have hsmall : count - dist < count := by omega
58  have hsource : offset - count + (count - dist) = offset - dist := by omega
59  simp only [List.getD_eq_getElem?_getD, hidx,
60    List.getElem?_append_right hright, Nat.add_sub_cancel_left, written_get,
61    hsmall, ite_true, hsource, Array.getD_eq_getD_getElem?]
62
63/-- The byte source is in the current output; reads of earlier writes
64implement arbitrary overlapping matches. -/
65theorem output_copy_refines_lz77 : Goal.output_copy_refines_lz77 := by
66  intro dict bytes offset count dist n
67  induction n generalizing bytes offset count with
68  | zero => intro _ _ _ _; simp [cpyN, copyBack]
69  | succ n ih =>
70    intro hc hd hdist hb
71    have ho : offset < bytes.size := by omega
72    have hsrc : offset - dist + 1 = offset + 1 - dist := by omega
73    rw [cpyN, hsrc]
74    rw [show offset + (n + 1) = offset + 1 + n by omega,
75      show count + (n + 1) = count + 1 + n by omega]
76    rw [ih (bytes.set! offset (bytes.getD (offset - dist) 0)) (offset + 1) (count + 1)
77      (by omega) hd (by omega) (by simp only [Array.size_set!]; omega)]
78    rw [copyBack, written_set_append bytes offset count _ hc ho]
79    rw [output_source dict bytes offset count dist hc (by omega) hd hdist]
80
81private theorem window_source (dict : List UInt8) (bytes : Array UInt8)
82    (offset count dist : Nat) (hc : count ≤ offset) (hb : offset ≤ bytes.size)
83    (hd : count < dist) (hbound : dist ≤ dict.length + count) :
84    (dict ++ writtenBytes bytes offset count).getD
85      ((dict ++ writtenBytes bytes offset count).length - dist) 0 =
86        dict.getD (dict.length + count - dist) 0 := by
87  rw [List.length_append, written_length bytes offset count hc hb]
88  have hi : dict.length + count - dist < dict.length := by omega
89  simp only [List.getD_eq_getElem?_getD, List.getElem?_append_left hi]
90
91private theorem window_copy (dict : List UInt8) (window : Array UInt8)
92    (dist : Nat) : ∀ n (bytes : Array UInt8) (offset count sourceOffset : Nat),
93    count ≤ offset → count ≤ dist → dist ≤ dict.length + count →
94    n ≤ dist - count → offset + n ≤ bytes.size → sourceOffset + n ≤ window.size →
95    (∀ i, i < n → window.getD (sourceOffset + i) 0 =
96      dict.getD (dict.length + count - dist + i) 0) →
97    writtenBytes (blitN window n sourceOffset offset bytes) (offset + n) (count + n) =
98      copyBack dict dist n (writtenBytes bytes offset count) := by
99  intro n
100  induction n with
101  | zero => intro bytes offset count sourceOffset _ _ _ _ _ _ _; simp [blitN, copyBack]
102  | succ n ih =>
103    intro bytes offset count sourceOffset hc hd hbound hn hb hw hcells
104    have hlt : count < dist := by omega
105    have ho : offset < bytes.size := by omega
106    rw [blitN]
107    rw [show offset + (n + 1) = offset + 1 + n by omega,
108      show count + (n + 1) = count + 1 + n by omega]
109    rw [ih (bytes.set! offset (window.getD sourceOffset 0)) (offset + 1) (count + 1)
110      (sourceOffset + 1) (by omega) (by omega) (by omega) (by omega)
111      (by simp only [Array.size_set!]; omega) (by omega) ?_]
112    · rw [copyBack, written_set_append bytes offset count _ hc ho]
113      have h0 := hcells 0 (by omega)
114      simp only [Nat.add_zero] at h0
115      rw [window_source dict bytes offset count dist hc (by omega) hlt hbound, h0]
116    · intro i hi
117      have hnext := hcells (i + 1) (by omega)
118      have hp : dict.length + (count + 1) - dist + i =
119          dict.length + count - dist + (i + 1) := by omega
120      simpa only [hp, Nat.add_assoc, Nat.add_comm 1 i] using hnext
121
122/-- A fixed saved-window segment agrees with the same growing-history copy
123until the source reaches the current output. -/
124theorem window_copy_refines_lz77 : Goal.window_copy_refines_lz77 := by
125  intro dict bytes window offset count sourceOffset dist n hc hd hbound hn hb hw hcells
126  exact window_copy dict window dist n bytes offset count sourceOffset hc (by omega) hbound hn hb hw hcells
127
128end ZlibF.Math.LZ77Copy