trees.c.build.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.build.static»
2
3/-! # trees.c: original nonzero frequencies obtain usable codes -/
4
5namespace Zlib.Trees.Proofs
6open C Zlib.Trees
7
8/-- The actual first scan changes only code lengths, so every represented
9frequency is retained. -/
10theorem BTScanInv.frequency {tk : TK} {d e : DeflateState} {N : Nat} {mc : Int32}
11    (hi : BTScanInv tk d N mc e) (v : Nat) (hv : v < (tk.arr d).size) :
12    btFreq tk e v = btFreq tk d v := by
13  obtain ⟨T, H, D, hl, rfl, hT, hH, hD, hlen, hmax, hcells, rest⟩ := hi
14  unfold btFreq
15  rw [btScanState_tree, hcells v (by omega)]
16  split <;> rfl
17
18/-- A dummy-leaf update writes frequency one. Thus it cannot erase any
19original nonzero frequency, even without using freshness of the dummy. -/
20theorem BTForceTrace.nonzero {tk : TK} {sl : Option (Nat → UInt16)}
21    {k : Nat} {mc0 mc : Int32} {d0 d : DeflateState} (hi : BTForceTrace tk sl k mc0 d0 mc d)
22    (v : Nat) (hv : btFreq tk d0 v ≠ 0) : btFreq tk d v ≠ 0 := by
23  induction hi with
24  | nil => exact hv
25  | snoc node hl before hn hnT hm hhl ih =>
26    rw [btForceState_freq tk _ node hl sl hnT]
27    dsimp only
28    split
29    · decide +kernel
30    · exact ih hv
31
32/-- The complete actual prepared-leaf prefix retains every original
33positive-frequency symbol. No assumption about the original heap or lengths
34is used, and the repair's frequency writes are included. -/
35theorem ws_btSortedStart_nonzero {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
36    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc} {sl : Option (Nat → UInt16)}
37    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
38    (hsd : StaticTreeDescRef.get h0 sref = some sd)
39    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
40    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
41    (hT : sd.elems.toInt ≤ (tk.arr d).size) (hD : sd.elems.toInt ≤ d.depth.size)
42    (hH : d.heap.size = 573) (hs : BTStatic h0 id sd.static_tree sd.elems.toInt.toNat sl) :
43    WS h0 id (btSortedStart (Sp id) (some (dk.descRef id))) d (fun _ e =>
44      ∀ v < sd.elems.toInt.toNat, btFreq tk d v ≠ 0 → btFreq tk e v ≠ 0) := by
45  unfold btSortedStart
46  refine WS.bind' (ws_btLeavesStart hdd hsd hstat htree he3 he286 hT hD hH hs)
47    fun a mid ⟨ht, hst, he, hleaf, scan, scanMc, k, hscan, hlen, hk, hkexact, htrace⟩ => ?_
48  rcases a with ⟨tree, stree, elems, mc⟩
49  dsimp only at ht hst he hleaf htrace ⊢
50  subst tree; subst stree; subst elems
51  have hused : ∀ v < sd.elems.toInt.toNat, btFreq tk d v ≠ 0 → btFreq tk mid v ≠ 0 := by
52    intro v hv hfv
53    have hreset : tk.arr { d with heap_len := 0, heap_max := HEAP_SIZE } = tk.arr d := by cases tk <;> rfl
54    have hscanfr := hscan.frequency v (by rw [hreset]; omega)
55    change btFreq tk scan v = btFreq tk { d with heap_len := 0, heap_max := HEAP_SIZE } v at hscanfr
56    have hscanfr' : btFreq tk scan v = btFreq tk d v := by
57      simpa only [btFreq, hreset] using hscanfr
58    exact htrace.nonzero v (by rw [hscanfr']; exact hfv)
59  refine WS.bind' (ws_btOrder_leaf tk dk mid sd.elems.toInt.toNat mc hleaf)
60    fun _ e ⟨hleaf', H, he, hsH, hf, hp, ho, hdesc', hmin⟩ => ?_
61  subst e
62  refine WS.pure' ?_
63  intro v hv hfv
64  simp only [btFreq, tk_arr_heap, tk_arr_setDesc]
65  exact hused v hv hfv
66
67/-- Every used prepared leaf remains in the non-root retained interval
68after the actual root store. Completeness is derived from the forest count,
69and the unique root is an internal node. -/
70theorem ws_btSaveRoot_support {h0 : Heap} {id : Nat} {tk : TK} {d0 d : DeflateState}
71    {N K : Nat} {mc node : Int32} (hi : BTForest tk N K (K - 1) mc d0 node d) :
72    WS h0 id (btSaveRoot (Sp id)) d (fun _ e =>
73      ∀ v < N, btFreq tk d0 v ≠ 0 → v ≤ mc.toInt.toNat ∧
74        ∃ q : Nat, 574 - 2 * K < q ∧ q < 573 ∧ Hn e q = v) := by
75  have hK2 := hi.queue.k2
76  have hKN := hi.queue.kN
77  have hNb := hi.queue.n286
78  have hsize := hi.queue.heap
79  have hlen := hi.queue.len
80  have hmax := hi.queue.max
81  have hlast := hi.last_root (by omega)
82  have hrootN : N ≤ Hn d 1 := by unfold Hn; omega
83  refine WS.mono (ws_btSaveRoot d (by omega) (by omega) (by omega) (by omega)) ?_
84  intro _ e ⟨hm, hhm, he, hsz, hroot, hframe⟩
85  intro v hv hfv
86  obtain ⟨q, hq, hqv⟩ := hi.used_position v hv hfv
87  have hqtail : 573 - 2 * (K - 1) ≤ q ∧ q < 573 := by
88    rcases hq with hq | hq
89    · have hq1 : q = 1 := by omega
90      rw [hq1] at hqv
91      omega
92    · exact hq
93  have hvc : v ≤ mc.toInt.toNat := by
94    rcases hi.kind q (Or.inr hqtail) with hqmc | hqN
95    · rwa [hqv] at hqmc
96    · omega
97  refine ⟨hvc, q, by omega, hqtail.2, ?_⟩
98  unfold Hn
99  rw [hframe q (by omega)]
100  exact hqv
101
102/-- Exact final-code stores preserve every length, including cells outside
103the symbol range and indices outside both arrays. -/
104theorem code_stores_lengths {tk : TK} {mid e : DeflateState} {mc : Int32} {a : Array CtData}
105    (he : e = tk.setArr mid a) (hs : a.size = (tk.arr mid).size)
106    (ha : ∀ i < a.size, a[i]! =
107      if i < (mc.toInt + 1).toNat ∧ (tk.arr mid)[i]!.dl ≠ 0 then
108        { (tk.arr mid)[i]! with fc := UInt16.ofNat (Math.storedCode
109          (fun b => mid.bl_count[b]!.toNat) (fun v => (tk.arr mid)[v]!.dl.toNat) i) }
110      else (tk.arr mid)[i]!) :
111    ∀ v : Nat, (tk.arr e)[v]!.dl = (tk.arr mid)[v]!.dl := by
112  subst e
113  intro v
114  rw [tk_arr_setArr]
115  by_cases hv : v < a.size
116  · rw [ha v hv]
117    split <;> rfl
118  · rw [getElem!_neg a v hv, getElem!_neg (tk.arr mid) v (by omega)]
119
120/-- The actual bit-length result assigns a positive limited length to each
121represented non-root leaf. -/
122theorem GBDone.supported_length {tk : TK} {built mid : DeflateState} {hm J N maxc L : Nat}
123    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
124    (hshape : GB.PShape (Hn built) hm J N maxc)
125    (hdone : GBDone tk built hm J maxc L xb slOpt mid)
126    (q v : Nat) (hq1 : hm < q) (hq2 : q < 573) (hqv : Hn built q = v) (hv : v ≤ maxc) :
127    1 ≤ (tk.arr mid)[v]!.dl.toNat ∧ (tk.arr mid)[v]!.dl.toNat ≤ L := by
128  obtain ⟨T, B, O, S, rfl, hsT, hsB, hfreq, hout, hlengths, rest⟩ := hdone
129  rw [tk_arr_mkP1]
130  have hi : q - hm - 1 < 2 * J := by have := hshape.hm_eq; omega
131  have heq : hm + 1 + (q - hm - 1) = q := by omega
132  have hlen := hlengths (q - hm - 1) hi (by rw [heq, hqv]; exact hv)
133  rw [heq, hqv] at hlen
134  exact hlen
135
136
137/-- Actual heap construction retains a represented non-root leaf for every
138symbol whose frequency was nonzero at function entry. Prepared-state
139frequencies are connected back to the original input here. -/
140theorem ws_btHeap_supported {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
141    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc} {sl : Option (Nat → UInt16)}
142    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
143    (hsd : StaticTreeDescRef.get h0 sref = some sd)
144    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
145    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
146    (hT : 2 * sd.elems.toInt.toNat - 1 ≤ (tk.arr d).size) (hTbig : (tk.arr d).size ≤ 600)
147    (hD : 2 * sd.elems.toInt.toNat - 1 ≤ d.depth.size)
148    (hH : d.heap.size = 573) (hB : d.bl_count.size = 16)
149    (hs : BTStatic h0 id sd.static_tree sd.elems.toInt.toNat sl) :
150    WS h0 id (btHeap (Sp id) (some (dk.descRef id))) d (fun a e =>
151      a.1 = .ref (tk.ref id) 0 ∧ ∃ (prepared : DeflateState) (K : Nat),
152        BTBuilt tk sd.elems.toInt.toNat K a.2 prepared e ∧
153        (dk.descRef id).get (setD h0 id e) = some { dd with max_code := a.2 } ∧
154        e.bl_count.size = 16 ∧ (tk.arr e).size ≤ 600 ∧
155        ∀ v < sd.elems.toInt.toNat, btFreq tk d v ≠ 0 → v ≤ a.2.toInt.toNat ∧
156          ∃ q : Nat, 574 - 2 * K < q ∧ q < 573 ∧ Hn e q = v) := by
157  have hT0 : sd.elems.toInt ≤ (tk.arr d).size := by omega
158  have hD0 : sd.elems.toInt ≤ d.depth.size := by omega
159  unfold btHeap btMergedStart
160  simp only [M_bind_assoc, M_pure_bind]
161  refine WS.bind' (merge_ws_and (merge_ws_and (merge_ws_and
162    (ws_btSortedStart hdd hsd hstat htree he3 he286 hT0 hD0 hH hs)
163    (ws_btSortedStart_sizes hdd hsd hstat htree he3 he286 hT0 hD0 hH hs))
164    (ws_btSortedStart_bl_count hdd hsd hstat htree he3 he286 hT0 hD0 hH hs))
165    (ws_btSortedStart_nonzero hdd hsd hstat htree he3 he286 hT0 hD0 hH hs))
166    fun a prepared ⟨⟨⟨⟨ht, hst, he, hleaf, h2, hm, hdesc, ho, hmin⟩, hTs, hDs⟩, hBs⟩, hused⟩ => ?_
167  rcases a with ⟨tree, stree, elems, mc⟩
168  dsimp only at ht hst he hleaf hdesc ⊢
169  subst tree; subst stree; subst elems
170  have hcnt := hleaf.count
171  have hKN := Math.scanCount_le (btFreq tk prepared) sd.elems.toInt.toNat
172  have hI := BTForest.of_leaf hleaf h2 hm (node := sd.elems) (by omega)
173    (by rw [hTs]; omega) (by rw [hDs]; omega) ho
174  refine WS.bind' (ws_btMergeLoop_forest hI) fun next merged ⟨hforest, hframe, hlen⟩ => ?_
175  refine WS.bind' (merge_ws_and (ws_btSaveRoot_forest hforest hframe) (ws_btSaveRoot_support hforest))
176    fun _ e ⟨hbuilt, hsupport⟩ => ?_
177  have hmeta := hbuilt.frame.metadata dk
178  have hDesc : dk.getDesc prepared = { dd with max_code := mc } :=
179    Option.some.inj ((bt_desc_get dk h0 id prepared).symm.trans hdesc)
180  have hDesc' : (dk.descRef id).get (setD h0 id e) = some { dd with max_code := mc } := by
181    rw [bt_desc_get, hmeta.1, hDesc]
182  have heB : e.bl_count.size = 16 := by rw [hmeta.2, hBs]; exact hB
183  have heT : (tk.arr e).size = (tk.arr prepared).size := by
184    obtain ⟨T, H, D, hl, hm, he, hT, hH, hD⟩ := hbuilt.frame
185    rw [he]
186    cases tk <;> exact hT
187  refine WS.pure' ⟨rfl, prepared, prepared.heap_len.toInt.toNat, hbuilt, hDesc', heB,
188    by rw [heT, hTs]; exact hTbig, ?_⟩
189  intro v hv hfv
190  exact hsupport v hv (hused v hv hfv)
191
192/-- Every originally used symbol obtains a positive limited length and its
193exact stored canonical code. The canonical expression refers to the final
194count and length arrays, so no unconstrained intermediate state stands in
195for the original-frequency connection. -/
196theorem ws_build_tree_used_codes {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
197    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc}
198    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
199    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
200    (hsd : StaticTreeDescRef.get h0 sref = some sd)
201    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
202    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
203    (hT : 2 * sd.elems.toInt.toNat - 1 ≤ (tk.arr d).size) (hTbig : (tk.arr d).size ≤ 600)
204    (hD : 2 * sd.elems.toInt.toNat - 1 ≤ d.depth.size)
205    (hH : d.heap.size = 573) (hB : d.bl_count.size = 16)
206    (hs : BTBuildStatic h0 id sd xb slOpt) :
207    WS h0 id (build_tree (Sp id) (some (dk.descRef id))) d (fun _ e =>
208      ∀ v < sd.elems.toInt.toNat, btFreq tk d v ≠ 0 →
209        1 ≤ (tk.arr e)[v]!.dl.toNat ∧ (tk.arr e)[v]!.dl.toNat ≤ sd.max_length.toInt.toNat ∧
210        (tk.arr e)[v]!.fc = UInt16.ofNat (Math.storedCode
211          (fun b => e.bl_count[b]!.toNat) (fun n => (tk.arr e)[n]!.dl.toNat) v)) := by
212  obtain ⟨sl, hsRepair⟩ := hs.repair
213  rw [build_tree_eq_heap_codes]
214  refine WS.bind' (ws_btHeap_supported hdd hsd hstat htree he3 he286 hT hTbig hD hH hB hsRepair)
215    fun a built ⟨ht, prepared, K, hbuilt, hdesc, hBs, hTs, hsupport⟩ => ?_
216  rcases a with ⟨tree, mc⟩
217  dsimp only at ht hbuilt hdesc hsupport ⊢
218  subst tree
219  have hctx := hbuilt.bitlen_ctx hs rfl hBs hTs
220  have hcodes := ws_btCodes (h0 := h0) (id := id) (tk := tk) (d := built)
221    (r := dk.descRef id) (sref := sref) (dd := { dd with max_code := mc }) (sd := sd)
222    (hm := 574 - 2 * K) (J := K - 1) (elems := sd.elems.toInt.toNat) (maxc := mc.toInt.toNat)
223    (L := sd.max_length.toInt.toNat) (baseN := sd.extra_base.toInt.toNat) (xb := xb) (slOpt := slOpt)
224    hdesc hsd hstat htree hctx hbuilt.heap_max hs.length_capacity (by omega) hbuilt.unused
225  refine WS.mono hcodes ?_
226  intro _ e ⟨mid, hdone, a, he, hsize, hstores⟩
227  have hlens := code_stores_lengths he hsize hstores
228  have hcounts : e.bl_count = mid.bl_count := by rw [he]; exact tk_setArr_bl_count tk a
229  intro v hv hfv
230  obtain ⟨hvc, q, hq1, hq2, hqv⟩ := hsupport v hv hfv
231  have hlen := hdone.supported_length hbuilt.shape q v hq1 hq2 hqv hvc
232  have hpos : (tk.arr mid)[v]!.dl ≠ 0 := by intro hz; rw [hz] at hlen; have hzN : (0 : UInt16).toNat = 0 := rfl; rw [hzN] at hlen; omega
233  have hMidSize : (tk.arr mid).size = (tk.arr built).size := by
234    obtain ⟨T, B, O, S, rfl, hT, rest⟩ := hdone
235    simpa only [tk_arr_mkP1] using hT
236  have hvA : v < a.size := by have := hbuilt.capacity; have := hbuilt.k2; omega
237  have hvRange : v < (mc.toInt + 1).toNat := by have := hbuilt.max_nonneg; omega
238  refine ⟨by rw [hlens]; exact hlen.1, by rw [hlens]; exact hlen.2, ?_⟩
239  have hfun : (fun n : Nat => (tk.arr e)[n]!.dl.toNat) = (fun n : Nat => (tk.arr mid)[n]!.dl.toNat) := by
240    funext n
241    rw [hlens]
242  rw [hcounts, hfun, he, tk_arr_setArr, hstores v hvA, ite_eq_left ⟨hvRange, hpos⟩]
243
244
245/-- A stored canonical value of length at most fifteen is represented
246exactly by the 16-bit cell and fits in the declared number of bits. -/
247theorem canonical_word_value (tk : TK) (d : DeflateState) (v : Nat)
248    (hl : (tk.arr d)[v]!.dl.toNat ≤ 15)
249    (hc : (tk.arr d)[v]!.fc = UInt16.ofNat (Math.storedCode
250      (fun b => d.bl_count[b]!.toNat) (fun n => (tk.arr d)[n]!.dl.toNat) v)) :
251    (tk.arr d)[v]!.fc.toNat = Math.storedCode
252      (fun b => d.bl_count[b]!.toNat) (fun n => (tk.arr d)[n]!.dl.toNat) v ∧
253    (tk.arr d)[v]!.fc.toNat < 2 ^ (tk.arr d)[v]!.dl.toNat := by
254  have hfit := Math.storedCode_lt (fun b => d.bl_count[b]!.toNat) (fun n => (tk.arr d)[n]!.dl.toNat) v
255  have hpow : 2 ^ (tk.arr d)[v]!.dl.toNat ≤ 2 ^ 15 := Nat.pow_le_pow_right (by omega) hl
256  have hword : Math.storedCode (fun b => d.bl_count[b]!.toNat) (fun n => (tk.arr d)[n]!.dl.toNat) v < 65536 := by
257    have h15 : 2 ^ 15 < 65536 := by decide +kernel
258    omega
259  have hval : (tk.arr d)[v]!.fc.toNat = Math.storedCode
260      (fun b => d.bl_count[b]!.toNat) (fun n => (tk.arr d)[n]!.dl.toNat) v := by
261    rw [hc, UInt16.toNat_ofNat', Nat.mod_eq_of_lt hword]
262  exact ⟨hval, by rw [hval]; exact hfit⟩
263
264/-- Complete actual construction gives every originally used symbol a
265positive limited length, an exact untruncated reversed canonical value,
266and the value bound consumed by the bit emitter. -/
267theorem ws_build_tree_usable_codes {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
268    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc}
269    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
270    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
271    (hsd : StaticTreeDescRef.get h0 sref = some sd)
272    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
273    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
274    (hT : 2 * sd.elems.toInt.toNat - 1 ≤ (tk.arr d).size) (hTbig : (tk.arr d).size ≤ 600)
275    (hD : 2 * sd.elems.toInt.toNat - 1 ≤ d.depth.size)
276    (hH : d.heap.size = 573) (hB : d.bl_count.size = 16)
277    (hs : BTBuildStatic h0 id sd xb slOpt) :
278    WS h0 id (build_tree (Sp id) (some (dk.descRef id))) d (fun _ e =>
279      ∀ v < sd.elems.toInt.toNat, btFreq tk d v ≠ 0 →
280        1 ≤ (tk.arr e)[v]!.dl.toNat ∧ (tk.arr e)[v]!.dl.toNat ≤ sd.max_length.toInt.toNat ∧
281        (tk.arr e)[v]!.fc.toNat = Math.storedCode
282          (fun b => e.bl_count[b]!.toNat) (fun n => (tk.arr e)[n]!.dl.toNat) v ∧
283        (tk.arr e)[v]!.fc.toNat < 2 ^ (tk.arr e)[v]!.dl.toNat) := by
284  refine WS.mono (ws_build_tree_used_codes hdd hsd hstat htree he3 he286 hT hTbig hD hH hB hs) ?_
285  intro _ e hcodes v hv hf
286  obtain ⟨hl1, hlL, hc⟩ := hcodes v hv hf
287  have hL := hs.length_limit
288  have hL0 := hs.length_pos
289  obtain ⟨hval, hfit⟩ := canonical_word_value tk e v (by omega) hc
290  exact ⟨hl1, hlL, hval, hfit⟩
291
292/-- Actual initialization facts discharge the entire domain for all three
293installed dynamic trees. Every originally used symbol receives an exact
294canonical word that fits a positive limited length. -/
295theorem ws_build_tree_usable_initialized {h0 : Heap} {id : Nat} {d : DeflateState}
296    (tk : TK) (hwf : d.WellFormed) (hs : Out.TreesStatic h0.static) (hr : Out.TreesRun0 id d) :
297    WS h0 id (build_tree (Sp id) (some (tk.descRef id))) d (fun _ e =>
298      ∀ v < tk.buildDesc.elems.toInt.toNat, btFreq tk d v ≠ 0 →
299        1 ≤ (tk.arr e)[v]!.dl.toNat ∧ (tk.arr e)[v]!.dl.toNat ≤ tk.buildDesc.max_length.toInt.toNat ∧
300        (tk.arr e)[v]!.fc.toNat = Math.storedCode
301          (fun b => e.bl_count[b]!.toNat) (fun n => (tk.arr e)[n]!.dl.toNat) v ∧
302        (tk.arr e)[v]!.fc.toNat < 2 ^ (tk.arr e)[v]!.dl.toNat) := by
303  obtain ⟨hLT, hDT, hBT, hBC, hH, hD⟩ := hwf
304  have he3 : 3 ≤ tk.buildDesc.elems.toInt := by cases tk <;> decide +kernel
305  have he286 : tk.buildDesc.elems.toInt ≤ 286 := by cases tk <;> decide +kernel
306  have hT : 2 * tk.buildDesc.elems.toInt.toNat - 1 ≤ (tk.arr d).size := by
307    cases tk
308    · change 571 ≤ d.dyn_ltree.size; omega
309    · change 59 ≤ d.dyn_dtree.size; omega
310    · change 37 ≤ d.bl_tree.size; omega
311  have hTbig : (tk.arr d).size ≤ 600 := by
312    cases tk
313    · change d.dyn_ltree.size ≤ 600; omega
314    · change d.dyn_dtree.size ≤ 600; omega
315    · change d.bl_tree.size ≤ 600; omega
316  have hDepth : 2 * tk.buildDesc.elems.toInt.toNat - 1 ≤ d.depth.size := by
317    cases tk
318    · change 571 ≤ d.depth.size; omega
319    · change 59 ≤ d.depth.size; omega
320    · change 37 ≤ d.depth.size; omega
321  have hstat : (tk.getDesc d).stat_desc = some tk.buildStaticRef := by
322    cases tk
323    · exact hr.lstat
324    · exact hr.dstat
325    · exact hr.blstat
326  have htree : (tk.getDesc d).dyn_tree = .ref (tk.ref id) 0 := by
327    cases tk
328    · exact hr.ldyn
329    · exact hr.ddyn
330    · exact hr.bldyn
331  exact ws_build_tree_usable_codes (bt_desc_get tk h0 id d) (trees_build_desc_get hs tk) hstat htree
332    he3 he286 hT hTbig hDepth hH hBC (trees_build_static hs tk)
333
334/-- The supported-code result runs on the actual initialized caller heap. -/
335theorem build_tree_usable_initialized {h : Heap} {id : Nat} {d : DeflateState}
336    (tk : TK) (hd : h.dstates id = some d) (hwf : d.WellFormed)
337    (hs : Out.TreesStatic h.static) (hr : Out.TreesRun0 id d) :
338    ∃ e : DeflateState, build_tree (Sp id) (some (tk.descRef id)) h = .ok ((), setD h id e) ∧
339      ∀ v < tk.buildDesc.elems.toInt.toNat, btFreq tk d v ≠ 0 →
340        1 ≤ (tk.arr e)[v]!.dl.toNat ∧ (tk.arr e)[v]!.dl.toNat ≤ tk.buildDesc.max_length.toInt.toNat ∧
341        (tk.arr e)[v]!.fc.toNat = Math.storedCode
342          (fun b => e.bl_count[b]!.toNat) (fun n => (tk.arr e)[n]!.dl.toNat) v ∧
343        (tk.arr e)[v]!.fc.toNat < 2 ^ (tk.arr e)[v]!.dl.toNat := by
344  obtain ⟨a, e, he, hresult⟩ := ws_build_tree_usable_initialized tk hwf hs hr
345  have ha : a = () := Subsingleton.elim _ _
346  subst a
347  rw [setD_self hd] at he
348  exact ⟨e, he, hresult⟩
349
350end Zlib.Trees.Proofs