trees.c.bl-support.lean

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

1import ZlibF.Proof.«trees.c.bl-tree»
2import ZlibF.Proof.«trees.c.build.lengths»
3import ZlibF.Math.DeflateRunSupport
4
5/-! # trees.c: deriving the minimum dynamic-header length count
6
7The search's lower bound comes from actual source-frequency support and
8zero initialization, not an assumed result of the search.
9-/
10
11namespace Zlib.Trees.Proofs
12open C Zlib.Trees
13
14/-- A successful independent decoder result is an actual alphabet index. -/
15theorem decodeSym_index_bound {lens : List Nat} {bits rest : List Bool} {v : Nat}
16    (hd : ZlibF.Spec.decodeSym lens bits = some (v, rest)) : v < lens.length := by
17  unfold ZlibF.Spec.decodeSym at hd
18  split at hd
19  · rename_i w hw
20    have hm := List.mem_of_find?_eq_some hw
21    simp only [Option.some.injEq, Prod.mk.injEq] at hd
22    obtain ⟨rfl, hrest⟩ := hd
23    exact List.mem_range.mp hm
24  · contradiction
25
26/-- Two actual runs of the same computation have the same live record. -/
27theorem same_record_of_runs {α : Type} {m : M α} {h : Heap} {id : Nat}
28    {a a' : α} {d d' : DeflateState}
29    (hr : m h = .ok (a, setD h id d)) (hr' : m h = .ok (a', setD h id d')) : d = d' := by
30  have hp := (Prod.mk.inj (Except.ok.inj (hr.symm.trans hr'))).2
31  have hs := congrArg (fun heap : Heap => heap.dstates id) hp
32  exact Option.some.inj (by simpa only [setD_dstates_same] using hs)
33
34/-- A positive literal-tree length contributes positive ordinary-symbol
35frequency to the actual scan model. The sentinel completes its pending run. -/
36theorem blScanCount_literal_support (d : DeflateState) (hin : BLInput d) (v : Nat)
37    (hv : v ≤ d.l_desc.max_code.toInt.toNat) (hp : 0 < d.dyn_ltree[v]!.dl.toNat) :
38    0 < blScanCount d d.dyn_ltree[v]!.dl.toNat := by
39  let L := fun i : Nat => d.dyn_ltree[i]!.dl.toNat
40  let M := d.l_desc.max_code.toInt.toNat
41  have hdone := scan_guard_finishes L M hin.llen
42  have hseen : Out.guarded L M v = L v := by
43    simp only [Out.guarded, ite_eq_right (show v ≠ M + 1 by omega)]
44  have hf := Out.scanFreq_seen_done (Out.guarded L M) (M + 1) v (L v) (by omega) hp hseen hdone
45  dsimp only [L, M] at hf
46  unfold blScanCount
47  omega
48
49/-- The actual literal/distance constructor pair retains a positive length
50and a containing final alphabet for every originally used literal symbol. -/
51theorem bl_prepare_used {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
52    (hI : Out.TreesInvAt h id d b buf) (v : Nat) (hv : v < 286) (hf : d.dyn_ltree[v]!.fc ≠ 0) :
53    ∃ e : DeflateState, blPrepare (Sp id) h = .ok ((), setD h id e) ∧
54      1 ≤ e.dyn_ltree[v]!.dl.toNat ∧ v ≤ e.l_desc.max_code.toInt.toNat := by
55  obtain ⟨aL, lit, hrL, hframeL, husable, M, hM, hmax, haccept, hdecode⟩ := merge_ws_and
56    (ws_build_tree_frame_initialized (h0 := h) .lit hI.base.wf hI.base.static hI.run.to0)
57    (merge_ws_and (ws_build_tree_usable_initialized (h0 := h) .lit hI.base.wf hI.base.static hI.run.to0)
58      (ws_build_tree_decodable_initialized (h0 := h) .lit hI.base.wf hI.base.static hI.run.to0))
59  have haL : aL = () := Subsingleton.elim _ _
60  subst aL
61  rw [setD_self hI.base.dstate] at hrL
62  have hIL := hframeL.treesInvAt hI
63  obtain ⟨aD, dist, hrD, hframeD⟩ := ws_build_tree_frame_initialized (h0 := h) .dist
64    hIL.base.wf hIL.base.static hIL.run.to0
65  have haD : aD = () := Subsingleton.elim _ _
66  subst aD
67  have hlDesc := hframeD.other_desc .lit (by decide +kernel)
68  have hlTree := hframeD.other_tree .lit (by decide +kernel)
69  simp only [TK.getDesc, TK.arr] at hlDesc hlTree hmax
70  have hlen := (husable v hv hf).1
71  have hbound := decodeSym_index_bound (hdecode v hv hf [])
72  simp only [Zlib.Inftrees.Proofs.lensOf, List.length_map, List.length_range] at hbound
73  simp only [TK.descRef] at hrL hrD
74  refine ⟨dist, ?_, ?_, ?_⟩
75  · have hpL : pLdesc (Sp id) h = .ok (some (.in_dstate_l_desc id), h) := by
76      unfold pLdesc
77      rw [bind_app, Out.sid_run hI.base.dstate]
78      rfl
79    have hpD : pDdesc (Sp id) (setD h id lit) =
80        .ok (some (.in_dstate_d_desc id), setD h id lit) := by
81      unfold pDdesc
82      rw [bind_app, Out.sid_run (setD_dstates_same h id lit)]
83      rfl
84    unfold blPrepare
85    rw [bind_app, hpL]
86    simp only []
87    rw [bind_app, hrL]
88    simp only []
89    rw [bind_app, hpD]
90    exact hrD
91  · rw [hlTree]
92    exact hlen
93  · rw [hlDesc]
94    omega
95
96/-- Nonzero END_BLOCK frequency and the cleared bit-length frequencies are
97internal block data. Actual constructors and scans turn them into a search
98index at least three. No index bound or callee contract is assumed. The
99following theorem establishes both data premises by actual init_block. -/
100theorem prepare_build_bl_min {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
101    (hI : Out.TreesInvAt h id d b buf) (hEOB : d.dyn_ltree[256]!.fc ≠ 0)
102    (hzero : ∀ k < 19, d.bl_tree[k]!.fc = 0) :
103    ∃ (mb : Int32) (e : DeflateState),
104      (do blPrepare (Sp id); build_bl_tree (Sp id)) h = .ok (mb, setD h id e) ∧
105      3 ≤ mb.toInt ∧ mb.toInt ≤ 18 ∧
106      Out.TreesInvAt (setD h id e) id e b buf ∧ Out.outBits buf e = Out.outBits buf d := by
107  obtain ⟨ready, hready, hin, hIR, hBready, houtR⟩ := bl_prepare hI
108  obtain ⟨used, hused, hpos, hcontained⟩ := bl_prepare_used hI 256 (by decide +kernel) hEOB
109  have heq : used = ready := same_record_of_runs hused hready
110  subst used
111  let code := ready.dyn_ltree[256]!.dl.toNat
112  have hc0 : 0 < code := by dsimp [code]; omega
113  have hc16 : code < 16 := by have := hin.llen 256 hcontained; dsimp [code]; omega
114  have hcount : 0 < blScanCount ready code := blScanCount_literal_support ready hin 256 hcontained hc0
115  have hbound := blScanCount_le ready hin code
116  have hzeroR : ready.bl_tree[code]!.fc = 0 := by rw [hBready]; exact hzero code (by omega)
117  obtain ⟨mb, scanned, built, e, B, hbuild, hs, hfreq, hframe, he, hmb, hlo, hhi, htail, hIe, hout, hcodes⟩ :=
118    build_bl_tree_checked hIR hin
119  have hBnat : B[code]!.fc.toNat = blScanCount ready code := by
120    rw [hfreq code, hzeroR, UInt16.zero_add, UInt16.toNat_ofNat']
121    exact Nat.mod_eq_of_lt (by omega)
122  have hsource : scanned.bl_tree[code]!.fc ≠ 0 := by
123    rw [hs]
124    change B[code]!.fc ≠ 0
125    intro hz
126    rw [hz] at hBnat
127    change 0 = blScanCount ready code at hBnat
128    omega
129  obtain ⟨maxc, hmaxc, hdesc, haccept, hsymbols⟩ := hcodes
130  have hlen := (hsymbols code (by omega) hsource).1.1
131  have hnonzero : e.bl_tree[code]!.dl ≠ 0 := by
132    intro hz
133    rw [hz] at hlen
134    change 1 ≤ 0 at hlen
135    omega
136  have hindex := bl_index_ge_of_nonrepeat e code hc16 hnonzero
137  have husedEq : blUsed e = blUsed built := by rw [he]; rfl
138  rw [husedEq] at hindex
139  rw [setD_setD] at hbuild hIe
140  refine ⟨mb, e, ?_, by omega, hhi, hIe, hout.trans houtR⟩
141  rw [bind_app, hready]
142  exact hbuild
143
144/-- Actual block initialization discharges END_BLOCK support and cleared
145bit-length frequencies. The actual constructor/search sequence then returns
1463..18, so its transmitted entry count is 4..19. Streaming tally preservation
147and full block emission remain separate obligations. -/
148theorem init_prepare_build_bl_min {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
149    (hI : Out.TreesInvAt h id d b buf) :
150    ∃ (mb : Int32) (e : DeflateState),
151      (do init_block (Sp id); blPrepare (Sp id); build_bl_tree (Sp id)) h =
152        .ok (mb, setD h id e) ∧
153      3 ≤ mb.toInt ∧ mb.toInt ≤ 18 ∧
154      Out.TreesInvAt (setD h id e) id e b buf := by
155  obtain ⟨aL, aD, aB, initialized, hinit, hII, heI, hLs, hDs, hBs,
156    hLzero, hEOB, hDzero, hBzero, hLdl, hDdl, hBdl⟩ := Out.init_block_spec0 hI.base hI.run.to0
157  change init_block (Sp id) h = .ok ((), setD h id initialized) at hinit
158  change Out.TreesInvAt (setD h id initialized) id initialized b buf at hII
159  have hEOBI : initialized.dyn_ltree[256]!.fc ≠ 0 := by
160    rw [heI]
161    change aL[256]!.fc ≠ 0
162    rw [hEOB]
163    decide +kernel
164  have hzI : ∀ k < 19, initialized.bl_tree[k]!.fc = 0 := by
165    intro k hk
166    rw [heI]
167    exact hBzero k hk
168  obtain ⟨mb, e, hbuild, hlo, hhi, hIe, hout⟩ := prepare_build_bl_min hII hEOBI hzI
169  rw [setD_setD] at hbuild hIe
170  refine ⟨mb, e, ?_, hlo, hhi, hIe⟩
171  rw [bind_app, hinit]
172  exact hbuild
173
174/-- Complete actual bit-length construction bounds all nineteen lengths,
175including unused symbols above the final alphabet maximum. -/
176theorem build_bl_tree_all_lengths {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
177    (hI : Out.TreesInvAt h id d b buf) (hin : BLInput d) :
178    ∃ (mb : Int32) (e : DeflateState),
179      build_bl_tree (Sp id) h = .ok (mb, setD h id e) ∧
180      (∀ v < 19, e.bl_tree[v]!.dl.toNat ≤ 7) ∧
181      (∀ v < 19, e.bl_desc.max_code.toInt.toNat < v → e.bl_tree[v]!.dl = 0) ∧
182      Out.TreesInvAt (setD h id e) id e b buf ∧ Out.outBits buf e = Out.outBits buf d := by
183  obtain ⟨scanned, B, hscan, hs, hIS, houtS, hBs, hdl, hfreq⟩ := bl_scan_pair hI hin
184  obtain ⟨a, built, hcodes, hframe, hlen, hupper⟩ := merge_ws_and
185    (ws_build_tree_frame_initialized (h0 := h) .bl hIS.base.wf hIS.base.static hIS.run.to0)
186    (ws_build_tree_all_lengths_initialized (h0 := h) .bl hIS.base.wf hIS.base.static hIS.run.to0)
187  have ha : a = () := Subsingleton.elim _ _
188  subst a
189  have hIB := hframe.treesInvAt hIS
190  rw [setD_setD] at hIB
191  have hbuild : blBuild (Sp id) h = .ok ((), setD h id built) := by
192    have hp : pBldesc (Sp id) (setD h id scanned) =
193        .ok (some (.in_dstate_bl_desc id), setD h id scanned) := by
194      unfold pBldesc
195      rw [bind_app, Out.sid_run (setD_dstates_same h id scanned)]
196      rfl
197    unfold blBuild
198    rw [bind_app, hscan]
199    simp only []
200    rw [bind_app, hp]
201    exact hcodes
202  obtain ⟨mb, e, hfinish, hmb, he⟩ := ws_blFinish (h0 := h) (id := id) (d := built)
203    (by obtain ⟨hl, hd, hbl, rest⟩ := hIB.base.wf; omega)
204  have hcost := blCost_frame built (built.opt_len + blHeaderCost (Math.blMaxIdx (blUsed built) 18))
205  have hIe := hcost.treesInvAt hIB
206  rw [setD_setD] at hIe
207  refine ⟨mb, e, ?_, ?_, ?_, ?_, ?_⟩
208  · rw [build_bl_tree_eq, bind_app, hbuild]
209    exact hfinish
210  · rw [he]
211    exact hlen
212  · rw [he]
213    exact hupper
214  · rw [he]; exact hIe
215  · rw [he]
216    exact (hcost.outBits buf).trans ((hframe.outBits buf).trans houtS)
217
218/-- All dynamic-header count ranges and all nineteen three-bit length
219values are derived on the same returned heap. END_BLOCK and cleared BL
220frequencies are internal block data, not assumed callee specifications. -/
221theorem prepare_build_bl_fields {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
222    (hI : Out.TreesInvAt h id d b buf) (hEOB : d.dyn_ltree[256]!.fc ≠ 0)
223    (hzero : ∀ k < 19, d.bl_tree[k]!.fc = 0) :
224    ∃ (mb : Int32) (e : DeflateState),
225      (do blPrepare (Sp id); build_bl_tree (Sp id)) h = .ok (mb, setD h id e) ∧
226      3 ≤ mb.toInt ∧ mb.toInt ≤ 18 ∧
227      257 ≤ e.l_desc.max_code.toInt + 1 ∧ e.l_desc.max_code.toInt + 1 ≤ 286 ∧
228      1 ≤ e.d_desc.max_code.toInt + 1 ∧ e.d_desc.max_code.toInt + 1 ≤ 30 ∧
229      (∀ v < 19, e.bl_tree[v]!.dl.toNat ≤ 7) ∧
230      (∀ v < 19, e.bl_desc.max_code.toInt.toNat < v → e.bl_tree[v]!.dl = 0) ∧
231      Out.TreesInvAt (setD h id e) id e b buf ∧ Out.outBits buf e = Out.outBits buf d := by
232  obtain ⟨ready, hready, hin, hIR, hBready, houtR⟩ := bl_prepare hI
233  obtain ⟨used, hused, hpos, hcontained⟩ := bl_prepare_used hI 256 (by decide +kernel) hEOB
234  have heq : used = ready := same_record_of_runs hused hready
235  subst used
236  obtain ⟨mb, e, hr, hlen, hupper, hIe, hout⟩ := build_bl_tree_all_lengths hIR hin
237  obtain ⟨mbS, eS, hrS, hLdesc, hDdesc, hLtree, hDtree, hIS, houtS⟩ :=
238    build_bl_preserves_source_codes hIR hin
239  have heqS : eS = e := same_record_of_runs hrS hr
240  subst eS
241  rw [setD_setD] at hr hIe
242  have hfull : (do blPrepare (Sp id); build_bl_tree (Sp id)) h = .ok (mb, setD h id e) := by
243    rw [bind_app, hready]
244    exact hr
245  obtain ⟨mbMin, eMin, hrMin, hlo, hhi, hIMin, houtMin⟩ := prepare_build_bl_min hI hEOB hzero
246  have hv : mb = mbMin := (Prod.mk.inj (Except.ok.inj (hfull.symm.trans hrMin))).1
247  rw [← hv] at hlo hhi
248  have hl0 := hin.l0
249  have hl286 := hin.l286
250  have hd0 := hin.d0
251  have hd30 := hin.d30
252  refine ⟨mb, e, hfull, hlo, hhi, ?_, ?_, ?_, ?_, hlen, hupper, hIe, hout.trans houtR⟩
253  · rw [hLdesc]
254    omega
255  · rw [hLdesc]
256    omega
257  · rw [hDdesc]
258    omega
259  · rw [hDdesc]
260    omega
261
262/-- Actual initialization and the complete actual tree-description prefix
263supply the format's HLIT, HDIST and HCLEN ranges and every transmitted
264three-bit length bound. This theorem does not yet execute send_all_trees or
265prove preservation through intervening streaming tallies. -/
266theorem init_prepare_build_bl_fields {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
267    (hI : Out.TreesInvAt h id d b buf) :
268    ∃ (mb : Int32) (e : DeflateState),
269      (do init_block (Sp id); blPrepare (Sp id); build_bl_tree (Sp id)) h = .ok (mb, setD h id e) ∧
270      3 ≤ mb.toInt ∧ mb.toInt ≤ 18 ∧
271      257 ≤ e.l_desc.max_code.toInt + 1 ∧ e.l_desc.max_code.toInt + 1 ≤ 286 ∧
272      1 ≤ e.d_desc.max_code.toInt + 1 ∧ e.d_desc.max_code.toInt + 1 ≤ 30 ∧
273      (∀ v < 19, e.bl_tree[v]!.dl.toNat ≤ 7) ∧
274      (∀ v < 19, e.bl_desc.max_code.toInt.toNat < v → e.bl_tree[v]!.dl = 0) ∧
275      Out.TreesInvAt (setD h id e) id e b buf := by
276  obtain ⟨aL, aD, aB, initialized, hinit, hII, heI, hLs, hDs, hBs,
277    hLzero, hEOB, hDzero, hBzero, hLdl, hDdl, hBdl⟩ := Out.init_block_spec0 hI.base hI.run.to0
278  change init_block (Sp id) h = .ok ((), setD h id initialized) at hinit
279  change Out.TreesInvAt (setD h id initialized) id initialized b buf at hII
280  have hEOBI : initialized.dyn_ltree[256]!.fc ≠ 0 := by
281    rw [heI]
282    change aL[256]!.fc ≠ 0
283    rw [hEOB]
284    decide +kernel
285  have hzI : ∀ k < 19, initialized.bl_tree[k]!.fc = 0 := by
286    intro k hk
287    rw [heI]
288    exact hBzero k hk
289  obtain ⟨mb, e, hbuild, hlo, hhi, hlL, hlH, hdL, hdH, hlen, hupper, hIe, hout⟩ :=
290    prepare_build_bl_fields hII hEOBI hzI
291  rw [setD_setD] at hbuild hIe
292  refine ⟨mb, e, ?_, hlo, hhi, hlL, hlH, hdL, hdH, hlen, hupper, hIe⟩
293  rw [bind_app, hinit]
294  exact hbuild
295
296end Zlib.Trees.Proofs