trees.c.build.lengths.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.build.frame»
2
3/-! # trees.c: lengths of the entire alphabet after actual construction -/
4
5namespace Zlib.Trees.Proofs
6open C Zlib.Trees
7
8/-- Every leaf above the actual prepared maximum is unused and remains
9zero-length throughout merging. This also covers leaves outside 0..max_code. -/
10theorem BTForest.above_max_zero {tk : TK} {N K j : Nat} {mc node : Int32}
11    {d0 d : DeflateState} (hi : BTForest tk N K j mc d0 node d)
12    (v : Nat) (hv : v < N) (hmax : mc.toInt.toNat < v) : (tk.arr d)[v]!.dl = 0 := by
13  apply hi.unused v hv
14  have hm := hi.initial.maxCode
15  rcases Math.scanMax_spec (btFreq tk d0) N with ⟨he, hz⟩ | ⟨u, he, hu, hf, hz⟩
16  · exact hz v hv
17  · exact hz v (by omega) hv
18
19/-- Complete actual heap building retains zero lengths above its maximum.
20The property comes from the actual forest and the root store's exact frame. -/
21theorem ws_btHeap_upper_zero {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
22    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc} {sl : Option (Nat → UInt16)}
23    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
24    (hsd : StaticTreeDescRef.get h0 sref = some sd)
25    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
26    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
27    (hT : 2 * sd.elems.toInt.toNat - 1 ≤ (tk.arr d).size)
28    (hD : 2 * sd.elems.toInt.toNat - 1 ≤ d.depth.size)
29    (hH : d.heap.size = 573) (hs : BTStatic h0 id sd.static_tree sd.elems.toInt.toNat sl) :
30    WS h0 id (btHeap (Sp id) (some (dk.descRef id))) d (fun a e =>
31      ∀ v < sd.elems.toInt.toNat, a.2.toInt.toNat < v → (tk.arr e)[v]!.dl = 0) := by
32  have hT0 : sd.elems.toInt ≤ (tk.arr d).size := by omega
33  have hD0 : sd.elems.toInt ≤ d.depth.size := by omega
34  unfold btHeap btMergedStart
35  simp only [M_bind_assoc, M_pure_bind]
36  refine WS.bind' (merge_ws_and
37    (ws_btSortedStart hdd hsd hstat htree he3 he286 hT0 hD0 hH hs)
38    (ws_btSortedStart_sizes hdd hsd hstat htree he3 he286 hT0 hD0 hH hs))
39    fun a prepared ⟨⟨ht, hst, he, hleaf, h2, hm, hdesc, ho, hmin⟩, hTs, hDs⟩ => ?_
40  rcases a with ⟨tree, stree, elems, mc⟩
41  dsimp only at ht hst he hleaf hdesc ⊢
42  subst tree; subst stree; subst elems
43  have hcnt := hleaf.count
44  have hKN := Math.scanCount_le (btFreq tk prepared) sd.elems.toInt.toNat
45  have hI := BTForest.of_leaf hleaf h2 hm (node := sd.elems) (by omega)
46    (by rw [hTs]; omega) (by rw [hDs]; omega) ho
47  refine WS.bind' (ws_btMergeLoop_forest hI) fun next merged ⟨hforest, hframe, hlen⟩ => ?_
48  have hK2 := hforest.queue.k2
49  have hKN := hforest.queue.kN
50  have hN286 := hforest.queue.n286
51  have hsize := hforest.queue.heap
52  have hmax := hforest.queue.max
53  have hj := hforest.queue.stage
54  refine WS.bind' (ws_btSaveRoot merged (by omega) (by omega) (by omega) (by omega))
55    fun _ e ⟨hm, hhm, he, hsz, hroot, htail⟩ => ?_
56  refine WS.pure' ?_
57  intro v hv hmaxv
58  have hz := hforest.above_max_zero v hv hmaxv
59  rw [he]
60  cases tk <;> exact hz
61
62/-- Complete actual construction bounds every alphabet length, including
63zero-frequency symbols above max_code. Those omitted symbols are exactly
64zero, so subsequent header writes never read an unconstrained old length. -/
65theorem ws_build_tree_all_lengths {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
66    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc}
67    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
68    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
69    (hsd : StaticTreeDescRef.get h0 sref = some sd)
70    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
71    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
72    (hT : 2 * sd.elems.toInt.toNat - 1 ≤ (tk.arr d).size) (hTbig : (tk.arr d).size ≤ 600)
73    (hD : 2 * sd.elems.toInt.toNat - 1 ≤ d.depth.size)
74    (hH : d.heap.size = 573) (hB : d.bl_count.size = 16)
75    (hs : BTBuildStatic h0 id sd xb slOpt) :
76    WS h0 id (build_tree (Sp id) (some (dk.descRef id))) d (fun _ e =>
77      (∀ v < sd.elems.toInt.toNat, (tk.arr e)[v]!.dl.toNat ≤ sd.max_length.toInt.toNat) ∧
78      ∀ v < sd.elems.toInt.toNat, (dk.getDesc e).max_code.toInt.toNat < v → (tk.arr e)[v]!.dl = 0) := by
79  obtain ⟨sl, hsRepair⟩ := hs.repair
80  rw [build_tree_eq_heap_codes]
81  refine WS.bind' (merge_ws_and
82    (ws_btHeap_built hdd hsd hstat htree he3 he286 hT hTbig hD hH hB hsRepair)
83    (ws_btHeap_upper_zero hdd hsd hstat htree he3 he286 hT hD hH hsRepair))
84    fun a built ⟨⟨ht, prepared, K, hbuilt, hdesc, hBs, hTs⟩, habove⟩ => ?_
85  rcases a with ⟨tree, mc⟩
86  dsimp only at ht hbuilt hdesc habove ⊢
87  subst tree
88  have hctx := hbuilt.bitlen_ctx hs rfl hBs hTs
89  have hcodes := ws_btCodes (h0 := h0) (id := id) (tk := tk) (d := built)
90    (r := dk.descRef id) (sref := sref) (dd := { dd with max_code := mc }) (sd := sd)
91    (hm := 574 - 2 * K) (J := K - 1) (elems := sd.elems.toInt.toNat) (maxc := mc.toInt.toNat)
92    (L := sd.max_length.toInt.toNat) (baseN := sd.extra_base.toInt.toNat) (xb := xb) (slOpt := slOpt)
93    hdesc hsd hstat htree hctx hbuilt.heap_max hs.length_capacity (by omega) hbuilt.unused
94  refine WS.mono hcodes ?_
95  intro _ e ⟨mid, hdone, T, he, hT, hstores⟩
96  have hlens := code_stores_lengths he hT hstores
97  have hlow := (hdone.symbolic_lengths hbuilt.shape hbuilt.unused).1
98  have hupper : ∀ v < sd.elems.toInt.toNat, mc.toInt.toNat < v → (tk.arr mid)[v]!.dl = 0 := by
99    intro v hv hmv
100    have hnone : ∀ q, 574 - 2 * K ≤ q → q < 573 → Hn built q ≠ v := by
101      intro q hq1 hq2 hqv
102      have hk := hbuilt.shape.kind q hq1 hq2
103      omega
104    obtain ⟨Tf, Bf, O, S, hemid, hTf, hBf, hfreq, hout, rest⟩ := hdone
105    rw [hemid, tk_arr_mkP1, hout v hnone, habove v hv hmv]
106  have hmaxBuilt : (dk.getDesc built).max_code = mc := by
107    have hg := bt_desc_get dk h0 id built
108    rw [hg] at hdesc
109    exact congrArg TreeDesc.max_code (Option.some.inj hdesc)
110  have hmaxE : (dk.getDesc e).max_code = mc := by
111    rw [he]
112    have hdescmid := hdone.descriptor dk
113    cases tk <;> cases dk <;> exact (congrArg TreeDesc.max_code hdescmid).trans hmaxBuilt
114  constructor
115  · intro v hv
116    rw [hlens]
117    by_cases hvm : v ≤ mc.toInt.toNat
118    · exact hlow v hvm
119    · rw [hupper v hv (by omega)]
120      change 0 ≤ sd.max_length.toInt.toNat
121      omega
122  · intro v hv hmv
123    rw [hmaxE] at hmv
124    rw [hlens]
125    exact hupper v hv hmv
126
127/-- Every installed alphabet's full length bound follows from the existing
128initialization representation and actual constructor execution. -/
129theorem ws_build_tree_all_lengths_initialized {h0 : Heap} {id : Nat} {d : DeflateState}
130    (tk : TK) (hwf : d.WellFormed) (hs : Out.TreesStatic h0.static) (hr : Out.TreesRun0 id d) :
131    WS h0 id (build_tree (Sp id) (some (tk.descRef id))) d (fun _ e =>
132      (∀ v < tk.buildDesc.elems.toInt.toNat, (tk.arr e)[v]!.dl.toNat ≤ tk.buildDesc.max_length.toInt.toNat) ∧
133      ∀ v < tk.buildDesc.elems.toInt.toNat, (tk.getDesc e).max_code.toInt.toNat < v → (tk.arr e)[v]!.dl = 0) := by
134  obtain ⟨hLT, hDT, hBT, hBC, hH, hD⟩ := hwf
135  have he3 : 3 ≤ tk.buildDesc.elems.toInt := by cases tk <;> decide +kernel
136  have he286 : tk.buildDesc.elems.toInt ≤ 286 := by cases tk <;> decide +kernel
137  have hT : 2 * tk.buildDesc.elems.toInt.toNat - 1 ≤ (tk.arr d).size := by
138    cases tk
139    · change 571 ≤ d.dyn_ltree.size; omega
140    · change 59 ≤ d.dyn_dtree.size; omega
141    · change 37 ≤ d.bl_tree.size; omega
142  have hTbig : (tk.arr d).size ≤ 600 := by
143    cases tk
144    · change d.dyn_ltree.size ≤ 600; omega
145    · change d.dyn_dtree.size ≤ 600; omega
146    · change d.bl_tree.size ≤ 600; omega
147  have hDepth : 2 * tk.buildDesc.elems.toInt.toNat - 1 ≤ d.depth.size := by
148    cases tk
149    · change 571 ≤ d.depth.size; omega
150    · change 59 ≤ d.depth.size; omega
151    · change 37 ≤ d.depth.size; omega
152  have hstat : (tk.getDesc d).stat_desc = some tk.buildStaticRef := by
153    cases tk
154    · exact hr.lstat
155    · exact hr.dstat
156    · exact hr.blstat
157  have htree : (tk.getDesc d).dyn_tree = .ref (tk.ref id) 0 := by
158    cases tk
159    · exact hr.ldyn
160    · exact hr.ddyn
161    · exact hr.bldyn
162  exact ws_build_tree_all_lengths (bt_desc_get tk h0 id d) (trees_build_desc_get hs tk) hstat htree
163    he3 he286 hT hTbig hDepth hH hBC (trees_build_static hs tk)
164
165end Zlib.Trees.Proofs