trees.c.build.format.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.emit»
2import ZlibF.Math.DeflateKraft
3import ZlibF.Proof.Format.Huffman
4
5/-! # trees.c: the independent format view of actual constructed codes -/
6
7namespace Zlib.Trees.Proofs
8open C Zlib.Trees
9
10/-- A symbol has a nonzero actual length exactly when it is represented as
11a retained non-root leaf. Zero unused lengths come from actual tree building. -/
12theorem GBDone.length_seen {tk : TK} {built mid : DeflateState} {hm J N maxc L : Nat}
13    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
14    (hshape : GB.PShape (Hn built) hm J N maxc)
15    (hzero : ∀ v ≤ maxc, (∀ q, hm ≤ q → q < 573 → Hn built q ≠ v) → (tk.arr built)[v]!.dl = 0)
16    (hdone : GBDone tk built hm J maxc L xb slOpt mid) :
17    ∀ v ≤ maxc, (tk.arr mid)[v]!.dl.toNat ≠ 0 ↔ ∃ q : Nat, hm < q ∧ q < 573 ∧ Hn built q = v := by
18  classical
19  intro v hv
20  constructor
21  · intro hnz
22    by_cases hs : ∃ q : Nat, hm < q ∧ q < 573 ∧ Hn built q = v
23    · exact hs
24    exfalso
25    have hno : ∀ q : Nat, hm ≤ q → q < 573 → Hn built q ≠ v := by
26      intro q hq1 hq2 he
27      by_cases hroot : q = hm
28      · subst q
29        have hr := hshape.root
30        have hJ := hshape.J1
31        have hmc := hshape.maxc_lt
32        omega
33      · exact hs ⟨q, by omega, hq2, he⟩
34    have hout : (tk.arr mid)[v]!.dl = (tk.arr built)[v]!.dl := by
35      obtain ⟨T, B, O, S, he, hT, hB, hfreq, hout, rest⟩ := hdone
36      rw [he, tk_arr_mkP1]
37      exact hout v hno
38    have hz : (tk.arr mid)[v]!.dl.toNat = 0 := by rw [hout, hzero v hv hno]; rfl
39    exact hnz hz
40  · intro ⟨q, hq1, hq2, hqv⟩
41    have hpos := hdone.supported_length hshape q v hq1 hq2 hqv hv
42    omega
43
44/-- The position-level Kraft equality is an equality for the actual length
45array produced by the translated function. -/
46theorem GBDone.position_kraft {tk : TK} {built mid : DeflateState} {hm J maxc L : Nat}
47    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
48    (hdone : GBDone tk built hm J maxc L xb slOpt mid) :
49    GB.rs (fun i => if Hn built (hm + 1 + i) ≤ maxc then
50      2 ^ (L - (tk.arr mid)[Hn built (hm + 1 + i)]!.dl.toNat) else 0) (2 * J) = 2 ^ L := by
51  obtain ⟨T, B, O, S, he, hT, hB, hfreq, hout, hlen, hk, rest⟩ := hdone
52  rw [he, tk_arr_mkP1]
53  exact hk
54
55/-- The actual count-array cells contain the position-level leaf counts. -/
56theorem GBDone.position_counts {tk : TK} {built mid : DeflateState} {hm J maxc L : Nat}
57    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
58    (hdone : GBDone tk built hm J maxc L xb slOpt mid) (b : Nat) (hb : b < 16) :
59    mid.bl_count[b]! = UInt16.ofNat (if b = 0 then 0 else GB.blP (Hn built) hm maxc
60      (fun v => (tk.arr mid)[v]!.dl.toNat) (2 * J) b) := by
61  obtain ⟨T, B, O, S, he, hT, hB, hfreq, hout, hlen, hk, hc, rest⟩ := hdone
62  rw [he, tk_arr_mkP1]
63  exact hc b hb
64
65/-- Actual lengths form a complete Kraft code over symbol indices, and
66every positive count cell counts those same symbol indices. -/
67theorem GBDone.symbolic_lengths {tk : TK} {built mid : DeflateState} {hm J N maxc L : Nat}
68    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
69    (hshape : GB.PShape (Hn built) hm J N maxc)
70    (hzero : ∀ v ≤ maxc, (∀ q, hm ≤ q → q < 573 → Hn built q ≠ v) → (tk.arr built)[v]!.dl = 0)
71    (hdone : GBDone tk built hm J maxc L xb slOpt mid) :
72    (∀ v ≤ maxc, (tk.arr mid)[v]!.dl.toNat ≤ L) ∧
73    GB.kraftSum (fun v => (tk.arr mid)[v]!.dl.toNat) (maxc + 1) L = 2 ^ L ∧
74    ∀ b : Nat, 1 ≤ b → b < 16 → mid.bl_count[b]! = UInt16.ofNat
75      (GB.countBefore (fun v => (tk.arr mid)[v]!.dl.toNat) b (maxc + 1)) := by
76  let len : Nat → Nat := fun v => (tk.arr mid)[v]!.dl.toNat
77  have hseen : ∀ v ≤ maxc, len v ≠ 0 ↔ ∃ q : Nat, hm < q ∧ q < 573 ∧ Hn built q = v :=
78    hdone.length_seen hshape hzero
79  refine ⟨?_, ?_, ?_⟩
80  · intro v hv
81    by_cases hz : len v = 0
82    · change len v ≤ L; omega
83    · obtain ⟨q, hq1, hq2, hqv⟩ := (hseen v hv).mp hz
84      exact (hdone.supported_length hshape q v hq1 hq2 hqv hv).2
85  · have hk := hdone.position_kraft
86    have hs := hshape.leaf_sum (fun v => len v ≠ 0) hseen (fun v => 2 ^ (L - len v))
87    change GB.rs (fun i => if Hn built (hm + 1 + i) ≤ maxc then
88      2 ^ (L - len (Hn built (hm + 1 + i))) else 0) (2 * J) = 2 ^ L at hk
89    rw [hs] at hk
90    rw [GB.kraftSum_rs]
91    exact hk
92  · intro b hb1 hb16
93    rw [hdone.position_counts b hb16, ite_eq_right (by omega)]
94    congr 1
95    have hpos : GB.blP (Hn built) hm maxc len (2 * J) b =
96        GB.rs (fun i => if Hn built (hm + 1 + i) ≤ maxc then
97          (if len (Hn built (hm + 1 + i)) = b then 1 else 0) else 0) (2 * J) := by
98      unfold GB.blP
99      apply GB.rs_congr
100      intro i hi
101      by_cases hv : Hn built (hm + 1 + i) ≤ maxc <;>
102        by_cases hl : len (Hn built (hm + 1 + i)) = b <;> simp only [hv, hl, and_self, and_true, and_false, ite_true, ite_false, false_and, true_and]
103    rw [hpos, hshape.leaf_sum (fun v => len v ≠ 0) hseen (fun v => if len v = b then 1 else 0), GB.countBefore_rs]
104    apply GB.rs_congr
105    intro v hv
106    change (if len v ≠ 0 then (if len v = b then 1 else 0) else 0) = (if len v = b then 1 else 0)
107    by_cases hz : len v ≠ 0
108    · rw [ite_eq_left hz]
109    · rw [ite_eq_right hz, ite_eq_right (by omega)]
110
111/-- The actual generated lengths satisfy the independent format's complete
112code rule for every code kind, including the bit-length alphabet. -/
113theorem GBDone.format_acceptable {tk : TK} {built mid : DeflateState} {hm J N maxc L : Nat}
114    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
115    (hshape : GB.PShape (Hn built) hm J N maxc) (hL : L ≤ 15)
116    (hzero : ∀ v ≤ maxc, (∀ q, hm ≤ q → q < 573 → Hn built q ≠ v) → (tk.arr built)[v]!.dl = 0)
117    (hdone : GBDone tk built hm J maxc L xb slOpt mid) :
118    ∀ kind : ZlibF.Spec.CodeKind, ZlibF.Spec.Acceptable kind
119      (Zlib.Inftrees.Proofs.lensOf (fun v => (tk.arr mid)[v]!.dl.toNat) (maxc + 1)) := by
120  obtain ⟨hlen, hk, hcounts⟩ := hdone.symbolic_lengths hshape hzero
121  apply GB.format_code_complete _ (maxc + 1) L hL (fun i hi => hlen i (by omega))
122  rwa [← GB.kraftSum_rs]
123
124
125/-- Positive count cells equal the independent format's symbol counts.
126The alphabet-size bound prevents 16-bit count truncation. -/
127theorem GBDone.format_counts {tk : TK} {built mid : DeflateState} {hm J N maxc L : Nat}
128    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
129    (hshape : GB.PShape (Hn built) hm J N maxc) (hmax : maxc + 1 < 65536)
130    (hzero : ∀ v ≤ maxc, (∀ q, hm ≤ q → q < 573 → Hn built q ≠ v) → (tk.arr built)[v]!.dl = 0)
131    (hdone : GBDone tk built hm J maxc L xb slOpt mid) :
132    mid.bl_count[0]!.toNat = 0 ∧
133    ∀ b : Nat, 1 ≤ b → b < 16 → mid.bl_count[b]!.toNat = ZlibF.Spec.count
134      (Zlib.Inftrees.Proofs.lensOf (fun v => (tk.arr mid)[v]!.dl.toNat) (maxc + 1)) b := by
135  obtain ⟨hlen, hk, hcounts⟩ := hdone.symbolic_lengths hshape hzero
136  constructor
137  · rw [hdone.position_counts 0 (by omega), ite_eq_left rfl]
138    rfl
139  · intro b hb1 hb16
140    rw [hcounts b hb1 hb16, UInt16.toNat_ofNat']
141    have hle : GB.countBefore (fun v => (tk.arr mid)[v]!.dl.toNat) b (maxc + 1) ≤ maxc + 1 := by
142      rw [GB.countBefore_rs]
143      have hs := GB.rs_le (n := maxc + 1)
144        (F := fun i => if (tk.arr mid)[i]!.dl.toNat = b then 1 else 0) (G := fun _ => 1)
145        (fun i hi => by split <;> omega)
146      rw [GB.rs_const] at hs
147      omega
148    rw [Nat.mod_eq_of_lt (by omega), Zlib.Inftrees.Proofs.count_lensOf, GB.decoder_count_rs, GB.countBefore_rs]
149
150/-- The mathematical word written by actual code generation has the
151independent format meaning for every symbol in the generated alphabet. -/
152theorem GBDone.format_code_bits {tk : TK} {built mid : DeflateState} {hm J N maxc L : Nat}
153    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
154    (hshape : GB.PShape (Hn built) hm J N maxc) (hmax : maxc + 1 < 65536) (hL : L ≤ 15)
155    (hzero : ∀ v ≤ maxc, (∀ q, hm ≤ q → q < 573 → Hn built q ≠ v) → (tk.arr built)[v]!.dl = 0)
156    (hdone : GBDone tk built hm J maxc L xb slOpt mid) (v : Nat) (hv : v ≤ maxc) :
157    Out.natBits (Math.storedCode (fun b => mid.bl_count[b]!.toNat) (fun n => (tk.arr mid)[n]!.dl.toNat) v)
158      (tk.arr mid)[v]!.dl.toNat = ZlibF.Spec.codeOf
159        (Zlib.Inftrees.Proofs.lensOf (fun n => (tk.arr mid)[n]!.dl.toNat) (maxc + 1)) v := by
160  have hlen := (hdone.symbolic_lengths hshape hzero).1 v hv
161  obtain ⟨h0, hc⟩ := hdone.format_counts hshape hmax hzero
162  exact GB.stored_bits_format _ _ (maxc + 1) v (by omega) (by omega) h0 hc
163
164/-- Bit-length generation changes no descriptor field. -/
165theorem GBDone.descriptor {tk : TK} {built mid : DeflateState} {hm J maxc L : Nat}
166    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
167    (hdone : GBDone tk built hm J maxc L xb slOpt mid) (dk : TK) :
168    dk.getDesc mid = dk.getDesc built := by
169  obtain ⟨T, B, O, S, rfl, rest⟩ := hdone
170  cases tk <;> cases dk <;> rfl
171
172/-- Complete actual tree construction produces format-acceptable lengths
173and the independent format code for every originally used symbol. The
174alphabet boundary is the actual final descriptor maximum. Buffer emission
175and the whole compression stream remain separate obligations. -/
176theorem ws_build_tree_format {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
177    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc}
178    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
179    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
180    (hsd : StaticTreeDescRef.get h0 sref = some sd)
181    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
182    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
183    (hT : 2 * sd.elems.toInt.toNat - 1 ≤ (tk.arr d).size) (hTbig : (tk.arr d).size ≤ 600)
184    (hD : 2 * sd.elems.toInt.toNat - 1 ≤ d.depth.size)
185    (hH : d.heap.size = 573) (hB : d.bl_count.size = 16)
186    (hs : BTBuildStatic h0 id sd xb slOpt) :
187    WS h0 id (build_tree (Sp id) (some (dk.descRef id))) d (fun _ e =>
188      ∃ maxc : Nat, maxc < sd.elems.toInt.toNat ∧ (dk.getDesc e).max_code.toInt = maxc ∧
189        (∀ kind : ZlibF.Spec.CodeKind, ZlibF.Spec.Acceptable kind
190          (Zlib.Inftrees.Proofs.lensOf (fun v => (tk.arr e)[v]!.dl.toNat) (maxc + 1))) ∧
191        ∀ v < sd.elems.toInt.toNat, btFreq tk d v ≠ 0 → v ≤ maxc ∧
192          1 ≤ (tk.arr e)[v]!.dl.toNat ∧ (tk.arr e)[v]!.dl.toNat ≤ sd.max_length.toInt.toNat ∧
193          Out.natBits (tk.arr e)[v]!.fc.toNat (tk.arr e)[v]!.dl.toNat = ZlibF.Spec.codeOf
194            (Zlib.Inftrees.Proofs.lensOf (fun n => (tk.arr e)[n]!.dl.toNat) (maxc + 1)) v) := by
195  obtain ⟨sl, hsRepair⟩ := hs.repair
196  rw [build_tree_eq_heap_codes]
197  refine WS.bind' (ws_btHeap_supported hdd hsd hstat htree he3 he286 hT hTbig hD hH hB hsRepair)
198    fun a built ⟨ht, prepared, K, hbuilt, hdesc, hBs, hTs, hsupport⟩ => ?_
199  rcases a with ⟨tree, mc⟩
200  dsimp only at ht hbuilt hdesc hsupport ⊢
201  subst tree
202  have hctx := hbuilt.bitlen_ctx hs rfl hBs hTs
203  have hcodes := ws_btCodes (h0 := h0) (id := id) (tk := tk) (d := built)
204    (r := dk.descRef id) (sref := sref) (dd := { dd with max_code := mc }) (sd := sd)
205    (hm := 574 - 2 * K) (J := K - 1) (elems := sd.elems.toInt.toNat) (maxc := mc.toInt.toNat)
206    (L := sd.max_length.toInt.toNat) (baseN := sd.extra_base.toInt.toNat) (xb := xb) (slOpt := slOpt)
207    hdesc hsd hstat htree hctx hbuilt.heap_max hs.length_capacity (by omega) hbuilt.unused
208  refine WS.mono hcodes ?_
209  intro _ e ⟨mid, hdone, a, he, hsize, hstores⟩
210  have hlens := code_stores_lengths he hsize hstores
211  have hfun : (fun n : Nat => (tk.arr e)[n]!.dl.toNat) = (fun n : Nat => (tk.arr mid)[n]!.dl.toNat) := by
212    funext n; rw [hlens]
213  have hL1 := hs.length_pos
214  have hL15 := hs.length_limit
215  have hL : sd.max_length.toInt.toNat ≤ 15 := by omega
216  have hmaxc := hbuilt.shape.maxc_lt
217  have hmaxWord : mc.toInt.toNat + 1 < 65536 := by omega
218  have hBuiltDesc : dk.getDesc built = { dd with max_code := mc } :=
219    Option.some.inj ((bt_desc_get dk h0 id built).symm.trans hdesc)
220  have hDesc : dk.getDesc e = { dd with max_code := mc } := by
221    rw [he]
222    have heD : dk.getDesc (tk.setArr mid a) = dk.getDesc mid := by cases tk <;> cases dk <;> rfl
223    rw [heD, hdone.descriptor dk, hBuiltDesc]
224  refine ⟨mc.toInt.toNat, hmaxc, by rw [hDesc]; have := hbuilt.max_nonneg; dsimp only; omega, ?_, ?_⟩
225  · rw [hfun]
226    exact hdone.format_acceptable hbuilt.shape hL hbuilt.unused
227  · intro v hv hfv
228    obtain ⟨hvc, q, hq1, hq2, hqv⟩ := hsupport v hv hfv
229    have hlen := hdone.supported_length hbuilt.shape q v hq1 hq2 hqv hvc
230    have hpos : (tk.arr mid)[v]!.dl ≠ 0 := by
231      intro hz; rw [hz] at hlen; have hzN : (0 : UInt16).toNat = 0 := rfl; rw [hzN] at hlen; omega
232    have hMidSize : (tk.arr mid).size = (tk.arr built).size := by
233      obtain ⟨T, B, O, S, rfl, hT, rest⟩ := hdone
234      simpa only [tk_arr_mkP1] using hT
235    have hvA : v < a.size := by have := hbuilt.capacity; have := hbuilt.k2; omega
236    have hvRange : v < (mc.toInt + 1).toNat := by have := hbuilt.max_nonneg; omega
237    have hCodeLt := Math.storedCode_lt (fun b => mid.bl_count[b]!.toNat) (fun n => (tk.arr mid)[n]!.dl.toNat) v
238    have hPow : 2 ^ (tk.arr mid)[v]!.dl.toNat ≤ 2 ^ 15 := Nat.pow_le_pow_right (by omega) (by omega)
239    have hWord : Math.storedCode (fun b => mid.bl_count[b]!.toNat) (fun n => (tk.arr mid)[n]!.dl.toNat) v < 65536 := by
240      have h15 : 2 ^ 15 < 65536 := by decide +kernel
241      omega
242    have hval : (tk.arr e)[v]!.fc.toNat = Math.storedCode
243        (fun b => mid.bl_count[b]!.toNat) (fun n => (tk.arr mid)[n]!.dl.toNat) v := by
244      rw [he, tk_arr_setArr, hstores v hvA, ite_eq_left ⟨hvRange, hpos⟩, UInt16.toNat_ofNat', Nat.mod_eq_of_lt hWord]
245    refine ⟨hvc, by rw [hlens]; exact hlen.1, by rw [hlens]; exact hlen.2, ?_⟩
246    rw [hval, hlens, hfun]
247    exact hdone.format_code_bits hbuilt.shape hmaxWord hL hbuilt.unused v hvc
248
249
250/-- A complete acceptable canonical code is decoded as its own symbol on
251every trailing bit suffix. The proof uses the existing format prefix-free
252theorem and the actual format decoder's bounded symbol search. -/
253theorem format_decode_code {kind : ZlibF.Spec.CodeKind} {ls : List Nat}
254    (hacc : ZlibF.Spec.Acceptable kind ls) (s : Nat) (hs : ls.getD s 0 ≠ 0) (suffix : List Bool) :
255    ZlibF.Spec.decodeSym ls (ZlibF.Spec.codeOf ls s ++ suffix) = some (s, suffix) := by
256  let inp := ZlibF.Spec.codeOf ls s ++ suffix
257  have hlen := ZlibF.Spec.Proofs.getD_ne_zero_lt ls s hs
258  have hpreS : ZlibF.Spec.codeOf ls s <+: inp := List.prefix_append _ _
259  have hpred : (ls.getD s 0 != 0 && (ZlibF.Spec.codeOf ls s).isPrefixOf inp) = true := by
260    rw [List.isPrefixOf_iff_prefix.mpr hpreS]
261    simp only [Bool.and_true, bne_iff_ne]
262    exact hs
263  have hfind : ∃ t : Nat, (List.range ls.length).find?
264      (fun k => ls.getD k 0 != 0 && (ZlibF.Spec.codeOf ls k).isPrefixOf inp) = some t := by
265    cases he : (List.range ls.length).find?
266        (fun k => ls.getD k 0 != 0 && (ZlibF.Spec.codeOf ls k).isPrefixOf inp) with
267    | some t => exact ⟨t, rfl⟩
268    | none =>
269      have hn := List.find?_eq_none.mp he s (List.mem_range.mpr hlen)
270      rw [hpred] at hn
271      contradiction
272  obtain ⟨t, ht⟩ := hfind
273  have hpt := List.find?_some ht
274  simp only [Bool.and_eq_true, bne_iff_ne, ne_eq] at hpt
275  have hpreT := List.isPrefixOf_iff_prefix.mp hpt.2
276  have hts : t = s := by
277    rcases Nat.le_total (ZlibF.Spec.codeOf ls t).length (ZlibF.Spec.codeOf ls s).length with hle | hle
278    · exact ZlibF.Spec.Proofs.prefixFree hacc.1 hacc.2.1 hpt.1 hs
279        (List.isPrefixOf_iff_prefix.mpr (List.prefix_of_prefix_length_le hpreT hpreS hle))
280    · exact (ZlibF.Spec.Proofs.prefixFree hacc.1 hacc.2.1 hs hpt.1
281        (List.isPrefixOf_iff_prefix.mpr (List.prefix_of_prefix_length_le hpreS hpreT hle))).symm
282  subst t
283  change ZlibF.Spec.decodeSym ls inp = _
284  unfold ZlibF.Spec.decodeSym
285  rw [ht]
286  have hCodeLen : (ZlibF.Spec.codeOf ls s).length = ls.getD s 0 := by
287    simp only [ZlibF.Spec.codeOf, ZlibF.Spec.Proofs.natToBitsMSB_length]
288  dsimp only [inp]
289  rw [← hCodeLen, List.drop_left]
290
291/-- Actual tree construction gives every originally used symbol code bits
292that the independent format decoder reads back as that symbol, regardless
293of the following bits. This is a symbol-level correctness result, not a
294complete compressed-block or streaming theorem. -/
295theorem ws_build_tree_decodable {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
296    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc}
297    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
298    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
299    (hsd : StaticTreeDescRef.get h0 sref = some sd)
300    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
301    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
302    (hT : 2 * sd.elems.toInt.toNat - 1 ≤ (tk.arr d).size) (hTbig : (tk.arr d).size ≤ 600)
303    (hD : 2 * sd.elems.toInt.toNat - 1 ≤ d.depth.size)
304    (hH : d.heap.size = 573) (hB : d.bl_count.size = 16)
305    (hs : BTBuildStatic h0 id sd xb slOpt) :
306    WS h0 id (build_tree (Sp id) (some (dk.descRef id))) d (fun _ e =>
307      ∃ maxc : Nat, maxc < sd.elems.toInt.toNat ∧ (dk.getDesc e).max_code.toInt = maxc ∧
308        (∀ kind : ZlibF.Spec.CodeKind, ZlibF.Spec.Acceptable kind
309          (Zlib.Inftrees.Proofs.lensOf (fun v => (tk.arr e)[v]!.dl.toNat) (maxc + 1))) ∧
310        ∀ v < sd.elems.toInt.toNat, btFreq tk d v ≠ 0 → ∀ suffix : List Bool,
311          ZlibF.Spec.decodeSym (Zlib.Inftrees.Proofs.lensOf (fun n => (tk.arr e)[n]!.dl.toNat) (maxc + 1))
312            (Out.natBits (tk.arr e)[v]!.fc.toNat (tk.arr e)[v]!.dl.toNat ++ suffix) = some (v, suffix)) := by
313  refine WS.mono (ws_build_tree_format hdd hsd hstat htree he3 he286 hT hTbig hD hH hB hs) ?_
314  intro _ e ⟨maxc, hmax, hdesc, hacc, hcodes⟩
315  refine ⟨maxc, hmax, hdesc, hacc, ?_⟩
316  intro v hv hf suffix
317  obtain ⟨hvc, hlen1, hlenL, hbits⟩ := hcodes v hv hf
318  rw [hbits]
319  apply format_decode_code (hacc .codeLength) v
320  have hlen : (Zlib.Inftrees.Proofs.lensOf (fun n => (tk.arr e)[n]!.dl.toNat) (maxc + 1)).getD v 0 =
321      (tk.arr e)[v]!.dl.toNat := by
322    simp [Zlib.Inftrees.Proofs.lensOf, List.getD_eq_getElem?_getD, show v < maxc + 1 by omega]
323  rw [hlen]
324  omega
325
326/-- The existing initialization representation supplies the local format
327and decoder theorem for each of the three actual dynamic trees. -/
328theorem ws_build_tree_decodable_initialized {h0 : Heap} {id : Nat} {d : DeflateState}
329    (tk : TK) (hwf : d.WellFormed) (hs : Out.TreesStatic h0.static) (hr : Out.TreesRun0 id d) :
330    WS h0 id (build_tree (Sp id) (some (tk.descRef id))) d (fun _ e =>
331      ∃ maxc : Nat, maxc < tk.buildDesc.elems.toInt.toNat ∧ (tk.getDesc e).max_code.toInt = maxc ∧
332        (∀ kind : ZlibF.Spec.CodeKind, ZlibF.Spec.Acceptable kind
333          (Zlib.Inftrees.Proofs.lensOf (fun v => (tk.arr e)[v]!.dl.toNat) (maxc + 1))) ∧
334        ∀ v < tk.buildDesc.elems.toInt.toNat, btFreq tk d v ≠ 0 → ∀ suffix : List Bool,
335          ZlibF.Spec.decodeSym (Zlib.Inftrees.Proofs.lensOf (fun n => (tk.arr e)[n]!.dl.toNat) (maxc + 1))
336            (Out.natBits (tk.arr e)[v]!.fc.toNat (tk.arr e)[v]!.dl.toNat ++ suffix) = some (v, suffix)) := by
337  obtain ⟨hLT, hDT, hBT, hBC, hH, hD⟩ := hwf
338  have he3 : 3 ≤ tk.buildDesc.elems.toInt := by cases tk <;> decide +kernel
339  have he286 : tk.buildDesc.elems.toInt ≤ 286 := by cases tk <;> decide +kernel
340  have hT : 2 * tk.buildDesc.elems.toInt.toNat - 1 ≤ (tk.arr d).size := by
341    cases tk
342    · change 571 ≤ d.dyn_ltree.size; omega
343    · change 59 ≤ d.dyn_dtree.size; omega
344    · change 37 ≤ d.bl_tree.size; omega
345  have hTbig : (tk.arr d).size ≤ 600 := by
346    cases tk
347    · change d.dyn_ltree.size ≤ 600; omega
348    · change d.dyn_dtree.size ≤ 600; omega
349    · change d.bl_tree.size ≤ 600; omega
350  have hDepth : 2 * tk.buildDesc.elems.toInt.toNat - 1 ≤ d.depth.size := by
351    cases tk
352    · change 571 ≤ d.depth.size; omega
353    · change 59 ≤ d.depth.size; omega
354    · change 37 ≤ d.depth.size; omega
355  have hstat : (tk.getDesc d).stat_desc = some tk.buildStaticRef := by
356    cases tk
357    · exact hr.lstat
358    · exact hr.dstat
359    · exact hr.blstat
360  have htree : (tk.getDesc d).dyn_tree = .ref (tk.ref id) 0 := by
361    cases tk
362    · exact hr.ldyn
363    · exact hr.ddyn
364    · exact hr.bldyn
365  exact ws_build_tree_decodable (bt_desc_get tk h0 id d) (trees_build_desc_get hs tk) hstat htree
366    he3 he286 hT hTbig hDepth hH hBC (trees_build_static hs tk)
367
368
369/-- Symbol decoding correctness for actual initialized caller storage. -/
370theorem build_tree_decodable_initialized {h : Heap} {id : Nat} {d : DeflateState}
371    (tk : TK) (hd : h.dstates id = some d) (hwf : d.WellFormed)
372    (hs : Out.TreesStatic h.static) (hr : Out.TreesRun0 id d) :
373    ∃ e : DeflateState, build_tree (Sp id) (some (tk.descRef id)) h = .ok ((), setD h id e) ∧
374      ∃ maxc : Nat, maxc < tk.buildDesc.elems.toInt.toNat ∧ (tk.getDesc e).max_code.toInt = maxc ∧
375        (∀ kind : ZlibF.Spec.CodeKind, ZlibF.Spec.Acceptable kind
376          (Zlib.Inftrees.Proofs.lensOf (fun v => (tk.arr e)[v]!.dl.toNat) (maxc + 1))) ∧
377        ∀ v < tk.buildDesc.elems.toInt.toNat, btFreq tk d v ≠ 0 → ∀ suffix : List Bool,
378          ZlibF.Spec.decodeSym (Zlib.Inftrees.Proofs.lensOf (fun n => (tk.arr e)[n]!.dl.toNat) (maxc + 1))
379            (Out.natBits (tk.arr e)[v]!.fc.toNat (tk.arr e)[v]!.dl.toNat ++ suffix) = some (v, suffix) := by
380  obtain ⟨a, e, he, hresult⟩ := ws_build_tree_decodable_initialized (h0 := h) tk hwf hs hr
381  have ha : a = () := Subsingleton.elim _ _
382  subst a
383  rw [setD_self hd] at he
384  exact ⟨e, he, hresult⟩
385
386end Zlib.Trees.Proofs