trees.c.build.frame.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.format»
2
3/-! # trees.c: caller state retained by complete tree construction -/
4
5namespace Zlib.Trees.Proofs
6open C Zlib.Trees
7
8/-- The complete record footprint of tree construction. Only the selected
9tree, selected descriptor maximum, work arrays, heap controls and costs may
10change. The replacement arrays have the original sizes. -/
11def BTBuildFrame (tk dk : TK) (d e : DeflateState) : Prop :=
12  ∃ (T : Array CtData) (H : Array Int32) (D : Array UInt8) (B : Array UInt16)
13    (hl hm mc : Int32) (O S : UInt64),
14    e = { tk.setArr (dk.setDesc d { dk.getDesc d with max_code := mc }) T with
15      heap := H, depth := D, bl_count := B, heap_len := hl, heap_max := hm,
16      opt_len := O, static_len := S } ∧
17    T.size = (tk.arr d).size ∧ H.size = d.heap.size ∧
18    D.size = d.depth.size ∧ B.size = d.bl_count.size
19
20theorem BTBuildFrame.refl (tk dk : TK) (d : DeflateState) : BTBuildFrame tk dk d d := by
21  refine ⟨tk.arr d, d.heap, d.depth, d.bl_count, d.heap_len, d.heap_max,
22    (dk.getDesc d).max_code, d.opt_len, d.static_len, ?_, rfl, rfl, rfl, rfl⟩
23  cases tk <;> cases dk <;> simp only [TK.setArr, TK.setDesc, TK.getDesc, TK.arr] <;> rfl
24
25theorem BTBuildFrame.trans {tk dk : TK} {a b c : DeflateState}
26    (hab : BTBuildFrame tk dk a b) (hbc : BTBuildFrame tk dk b c) :
27    BTBuildFrame tk dk a c := by
28  obtain ⟨T, H, D, B, hl, hm, mc, O, S, rfl, hT, hH, hD, hB⟩ := hab
29  obtain ⟨T', H', D', B', hl', hm', mc', O', S', rfl, hT', hH', hD', hB'⟩ := hbc
30  refine ⟨T', H', D', B', hl', hm', mc', O', S', ?_, ?_, ?_, ?_, ?_⟩
31  · cases tk <;> cases dk <;> simp only [TK.setArr, TK.setDesc, TK.getDesc] <;> rfl
32  · have hT'' : T'.size = T.size := by
33      cases tk <;> cases dk <;> exact hT'
34    exact hT''.trans hT
35  · exact hH'.trans hH
36  · exact hD'.trans hD
37  · exact hB'.trans hB
38
39/-- The forest's checked exact write frame is contained in the complete
40construction footprint. -/
41theorem BTForestFrame.build_frame {tk : TK} {d e : DeflateState}
42    (hi : BTForestFrame tk d e) (dk : TK) : BTBuildFrame tk dk d e := by
43  obtain ⟨T, H, D, hl, hm, rfl, hT, hH, hD⟩ := hi
44  refine ⟨T, H, D, d.bl_count, hl, hm, (dk.getDesc d).max_code,
45    d.opt_len, d.static_len, ?_, hT, hH, hD, rfl⟩
46  cases tk <;> cases dk <;> simp only [TK.setArr, TK.setDesc, TK.getDesc, btScanState] <;> rfl
47
48/-- Repair never changes the heap's allocated length. -/
49theorem BTForceTrace.heap_size {tk : TK} {sl : Option (Nat → UInt16)}
50    {k : Nat} {mc0 mc : Int32} {d e : DeflateState} (hi : BTForceTrace tk sl k mc0 d mc e) :
51    e.heap.size = d.heap.size := by
52  induction hi with
53  | nil => rfl
54  | snoc node hl before hn hnT hm hhl ih =>
55    simpa only [btForceState_heap, Array.size_set!] using ih
56
57/-- The actual reset, scan, repair, maximum store and heapify retain all
58caller fields outside the complete construction footprint. -/
59theorem ws_btSortedStart_frame {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
60    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc} {sl : Option (Nat → UInt16)}
61    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
62    (hsd : StaticTreeDescRef.get h0 sref = some sd)
63    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
64    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
65    (hT : sd.elems.toInt ≤ (tk.arr d).size) (hD : sd.elems.toInt ≤ d.depth.size)
66    (hH : d.heap.size = 573) (hs : BTStatic h0 id sd.static_tree sd.elems.toInt.toNat sl) :
67    WS h0 id (btSortedStart (Sp id) (some (dk.descRef id))) d
68      (fun _ e => BTBuildFrame tk dk d e) := by
69  unfold btSortedStart
70  refine WS.bind' (ws_btLeavesStart hdd hsd hstat htree he3 he286 hT hD hH hs)
71    fun a mid ⟨ht, hst, he, hleaf, scan, scanMc, k, hscan, hlen, hk, hkexact, htrace⟩ => ?_
72  rcases a with ⟨tree, stree, elems, mc⟩
73  dsimp only at ht hst he hleaf htrace ⊢
74  subst tree; subst stree; subst elems
75  have hsz := htrace.merge_sizes
76  have hheap := htrace.heap_size
77  have hB := htrace.bl_count
78  obtain ⟨Ts, Hs, Ds, hls, hscanEq, hsT, hsH, hsD, rest⟩ := hscan
79  obtain ⟨T, H, D, hl, O, S, hmid⟩ := htrace.frame
80  refine WS.bind' (ws_btOrder_leaf tk dk mid sd.elems.toInt.toNat mc hleaf)
81    fun _ e ⟨hleaf', H', he, hsH', hf, hp, ho, hdesc', hmin⟩ => ?_
82  refine WS.pure' ?_
83  refine ⟨T, H', D, d.bl_count, hl, HEAP_SIZE, mc, O, S, ?_, ?_, ?_, ?_, rfl⟩
84  · rw [he, hmid, hscanEq]
85    cases tk <;> cases dk <;> simp only [TK.setArr, TK.setDesc, TK.getDesc, btScanState] <;> rfl
86  · rw [hmid] at hsz
87    have hszt : T.size = (tk.arr scan).size := by
88      cases tk <;> exact hsz.1
89    rw [hscanEq, btScanState_tree] at hszt
90    have hsT' : Ts.size = (tk.arr d).size := by
91      cases tk <;> exact hsT
92    exact hszt.trans hsT'
93  · rw [hsH', hheap, hscanEq]
94    exact hsH
95  · rw [hmid, hscanEq] at hsz
96    exact hsz.2.trans hsD
97
98/-- The actual complete heap-building prefix keeps the caller frame.
99Its forest premises come from the actual sorted-leaf prefix. -/
100theorem ws_btHeap_frame {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
101    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc} {sl : Option (Nat → UInt16)}
102    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
103    (hsd : StaticTreeDescRef.get h0 sref = some sd)
104    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
105    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
106    (hT : 2 * sd.elems.toInt.toNat - 1 ≤ (tk.arr d).size)
107    (hD : 2 * sd.elems.toInt.toNat - 1 ≤ d.depth.size)
108    (hH : d.heap.size = 573) (hs : BTStatic h0 id sd.static_tree sd.elems.toInt.toNat sl) :
109    WS h0 id (btHeap (Sp id) (some (dk.descRef id))) d
110      (fun _ e => BTBuildFrame tk dk d e) := by
111  have hT0 : sd.elems.toInt ≤ (tk.arr d).size := by omega
112  have hD0 : sd.elems.toInt ≤ d.depth.size := by omega
113  unfold btHeap btMergedStart
114  simp only [M_bind_assoc, M_pure_bind]
115  refine WS.bind' (merge_ws_and (merge_ws_and
116    (ws_btSortedStart hdd hsd hstat htree he3 he286 hT0 hD0 hH hs)
117    (ws_btSortedStart_sizes hdd hsd hstat htree he3 he286 hT0 hD0 hH hs))
118    (ws_btSortedStart_frame hdd hsd hstat htree he3 he286 hT0 hD0 hH hs))
119    fun a prepared ⟨⟨⟨ht, hst, he, hleaf, h2, hm, hdesc, ho, hmin⟩, hTs, hDs⟩, hframe⟩ => ?_
120  rcases a with ⟨tree, stree, elems, mc⟩
121  dsimp only at ht hst he hleaf hdesc ⊢
122  subst tree; subst stree; subst elems
123  have hcnt := hleaf.count
124  have hKN := Math.scanCount_le (btFreq tk prepared) sd.elems.toInt.toNat
125  have hI := BTForest.of_leaf hleaf h2 hm (node := sd.elems) (by omega)
126    (by rw [hTs]; omega) (by rw [hDs]; omega) ho
127  refine WS.bind' (ws_btMergeLoop_forest hI) fun next merged ⟨hforest, hmerge, hlen⟩ => ?_
128  refine WS.bind' (ws_btSaveRoot_forest hforest hmerge) fun _ e hbuilt => ?_
129  exact WS.pure' (hframe.trans (hbuilt.frame.build_frame dk))
130
131/-- Length generation has the complete caller footprint. -/
132theorem GBDone.build_frame {tk : TK} {d e : DeflateState} {hm J maxc L : Nat}
133    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
134    (hi : GBDone tk d hm J maxc L xb slOpt e) (hB : d.bl_count.size = 16) (dk : TK) :
135    BTBuildFrame tk dk d e := by
136  obtain ⟨T, B, O, S, rfl, hT, hBs, rest⟩ := hi
137  refine ⟨T, d.heap, d.depth, B, d.heap_len, d.heap_max, (dk.getDesc d).max_code,
138    O, S, ?_, hT, rfl, rfl, hBs.trans hB.symm⟩
139  cases tk <;> cases dk <;> simp only [mkP1, TK.setArr, TK.setDesc, TK.getDesc] <;> rfl
140
141/-- Canonical code stores keep the complete caller footprint. -/
142theorem BTBuildFrame.codes (tk dk : TK) (d : DeflateState) (T : Array CtData)
143    (hT : T.size = (tk.arr d).size) : BTBuildFrame tk dk d (tk.setArr d T) := by
144  refine ⟨T, d.heap, d.depth, d.bl_count, d.heap_len, d.heap_max, (dk.getDesc d).max_code,
145    d.opt_len, d.static_len, ?_, hT, rfl, rfl, rfl⟩
146  cases tk <;> cases dk <;> simp only [TK.setArr, TK.setDesc, TK.getDesc] <;> rfl
147
148/-- Complete actual build_tree retains all caller state outside its exact
149record footprint. No postcondition of a callee is assumed. -/
150theorem ws_build_tree_frame {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
151    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc}
152    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
153    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
154    (hsd : StaticTreeDescRef.get h0 sref = some sd)
155    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
156    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
157    (hT : 2 * sd.elems.toInt.toNat - 1 ≤ (tk.arr d).size) (hTbig : (tk.arr d).size ≤ 600)
158    (hD : 2 * sd.elems.toInt.toNat - 1 ≤ d.depth.size)
159    (hH : d.heap.size = 573) (hB : d.bl_count.size = 16)
160    (hs : BTBuildStatic h0 id sd xb slOpt) :
161    WS h0 id (build_tree (Sp id) (some (dk.descRef id))) d
162      (fun _ e => BTBuildFrame tk dk d e) := by
163  obtain ⟨sl, hsRepair⟩ := hs.repair
164  rw [build_tree_eq_heap_codes]
165  refine WS.bind' (merge_ws_and
166    (ws_btHeap_built hdd hsd hstat htree he3 he286 hT hTbig hD hH hB hsRepair)
167    (ws_btHeap_frame hdd hsd hstat htree he3 he286 hT hD hH hsRepair))
168    fun a built ⟨⟨ht, prepared, K, hbuilt, hdesc, hBs, hTs⟩, hframe⟩ => ?_
169  rcases a with ⟨tree, mc⟩
170  dsimp only at ht hbuilt hdesc ⊢
171  subst tree
172  have hctx := hbuilt.bitlen_ctx hs rfl hBs hTs
173  have hcodes := ws_btCodes (h0 := h0) (id := id) (tk := tk) (d := built)
174    (r := dk.descRef id) (sref := sref) (dd := { dd with max_code := mc }) (sd := sd)
175    (hm := 574 - 2 * K) (J := K - 1) (elems := sd.elems.toInt.toNat) (maxc := mc.toInt.toNat)
176    (L := sd.max_length.toInt.toNat) (baseN := sd.extra_base.toInt.toNat) (xb := xb) (slOpt := slOpt)
177    hdesc hsd hstat htree hctx hbuilt.heap_max hs.length_capacity (by omega) hbuilt.unused
178  refine WS.mono hcodes ?_
179  intro _ e ⟨mid, hdone, T, he, hT, hstores⟩
180  subst e
181  exact hframe.trans ((hdone.build_frame hBs dk).trans (BTBuildFrame.codes tk dk mid T hT))
182
183/-- The construction footprint preserves every array size in WellFormed. -/
184theorem BTBuildFrame.wellFormed {tk dk : TK} {d e : DeflateState}
185    (hi : BTBuildFrame tk dk d e) (hw : d.WellFormed) : e.WellFormed := by
186  obtain ⟨T, H, D, B, hl, hm, mc, O, S, rfl, hT, hH, hD, hB⟩ := hi
187  obtain ⟨hLT, hDT, hBT, hBC, hHeap, hDepth⟩ := hw
188  cases tk <;> cases dk <;>
189    simp only [TK.setArr, TK.setDesc, DeflateState.WellFormed] <;>
190    simp_all only [TK.arr, and_self]
191
192/-- Tree construction retains the live output buffer, descriptor pointers,
193symbol count and bit-buffer invariant. -/
194theorem BTBuildFrame.treesInvAt {tk dk : TK} {h : Heap} {id b : Nat}
195    {d e : DeflateState} {buf : Array UInt8} (hi : BTBuildFrame tk dk d e)
196    (hI : Out.TreesInvAt h id d b buf) : Out.TreesInvAt (setD h id e) id e b buf := by
197  have hw := hi.wellFormed hI.base.wf
198  obtain ⟨T, H, D, B, hl, hm, mc, O, S, rfl, rest⟩ := hi
199  cases tk <;> cases dk <;>
200    exact ⟨⟨by simp [setD], hw, hI.base.static, hI.base.pbuf, hI.base.bytes, hI.base.rw,
201      hI.base.size, hI.base.psize, hI.base.sym, hI.base.lit_lo, hI.base.lit_hi,
202      hI.base.sym_end, hI.base.pending_le⟩,
203      ⟨hI.run.ldyn, hI.run.lstat, hI.run.ddyn, hI.run.dstat, hI.run.bldyn, hI.run.blstat,
204        hI.run.bi_lo, hI.run.bi_hi, hI.run.bi_buf, hI.run.sym_next_le, hI.run.sym_next_mod⟩⟩
205
206/-- Building codes changes no pending output bits. -/
207theorem BTBuildFrame.outBits {tk dk : TK} {d e : DeflateState}
208    (hi : BTBuildFrame tk dk d e) (buf : Array UInt8) : Out.outBits buf e = Out.outBits buf d := by
209  obtain ⟨T, H, D, B, hl, hm, mc, O, S, rfl, rest⟩ := hi
210  cases tk <;> cases dk <;> rfl
211
212/-- Building a different alphabet retains this tree exactly, including all
213code words and lengths needed for subsequent emission. -/
214theorem BTBuildFrame.other_tree {tk dk : TK} {d e : DeflateState}
215    (hi : BTBuildFrame tk dk d e) (other : TK) (hne : other ≠ tk) :
216    other.arr e = other.arr d := by
217  obtain ⟨T, H, D, B, hl, hm, mc, O, S, rfl, rest⟩ := hi
218  cases tk <;> cases other <;> cases dk <;> first | exact False.elim (hne rfl) | rfl
219
220/-- The installed descriptors and existing initialization representation
221supply every premise of the complete caller-frame proof. -/
222theorem ws_build_tree_frame_initialized {h0 : Heap} {id : Nat} {d : DeflateState}
223    (tk : TK) (hwf : d.WellFormed) (hs : Out.TreesStatic h0.static) (hr : Out.TreesRun0 id d) :
224    WS h0 id (build_tree (Sp id) (some (tk.descRef id))) d
225      (fun _ e => BTBuildFrame tk tk d e) := by
226  obtain ⟨hLT, hDT, hBT, hBC, hH, hD⟩ := hwf
227  have he3 : 3 ≤ tk.buildDesc.elems.toInt := by cases tk <;> decide +kernel
228  have he286 : tk.buildDesc.elems.toInt ≤ 286 := by cases tk <;> decide +kernel
229  have hT : 2 * tk.buildDesc.elems.toInt.toNat - 1 ≤ (tk.arr d).size := by
230    cases tk
231    · change 571 ≤ d.dyn_ltree.size; omega
232    · change 59 ≤ d.dyn_dtree.size; omega
233    · change 37 ≤ d.bl_tree.size; omega
234  have hTbig : (tk.arr d).size ≤ 600 := by
235    cases tk
236    · change d.dyn_ltree.size ≤ 600; omega
237    · change d.dyn_dtree.size ≤ 600; omega
238    · change d.bl_tree.size ≤ 600; omega
239  have hDepth : 2 * tk.buildDesc.elems.toInt.toNat - 1 ≤ d.depth.size := by
240    cases tk
241    · change 571 ≤ d.depth.size; omega
242    · change 59 ≤ d.depth.size; omega
243    · change 37 ≤ d.depth.size; omega
244  have hstat : (tk.getDesc d).stat_desc = some tk.buildStaticRef := by
245    cases tk
246    · exact hr.lstat
247    · exact hr.dstat
248    · exact hr.blstat
249  have htree : (tk.getDesc d).dyn_tree = .ref (tk.ref id) 0 := by
250    cases tk
251    · exact hr.ldyn
252    · exact hr.ddyn
253    · exact hr.bldyn
254  exact ws_build_tree_frame (bt_desc_get tk h0 id d) (trees_build_desc_get hs tk) hstat htree
255    he3 he286 hT hTbig hDepth hH hBC (trees_build_static hs tk)
256
257/-- Complete tree construction preserves the actual caller's live output
258invariant and pending bits, without assuming either fact after the call. -/
259theorem build_tree_preserves {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
260    (hI : Out.TreesInvAt h id d b buf) (tk : TK) :
261    ∃ e : DeflateState, build_tree (Sp id) (some (tk.descRef id)) h = .ok ((), setD h id e) ∧
262      BTBuildFrame tk tk d e ∧ Out.TreesInvAt (setD h id e) id e b buf ∧
263      Out.outBits buf e = Out.outBits buf d := by
264  obtain ⟨a, e, he, hframe⟩ := ws_build_tree_frame_initialized (h0 := h) tk
265    hI.base.wf hI.base.static hI.run.to0
266  have ha : a = () := Subsingleton.elim _ _
267  subst a
268  rw [setD_self hI.base.dstate] at he
269  exact ⟨e, he, hframe, hframe.treesInvAt hI, hframe.outBits buf⟩
270
271/-- Building the actual tree and then sending one originally used symbol
272runs on one caller heap. The appended output decodes to that symbol under
273the independently specified decoder, with every following suffix retained.
274The fifteen-bit room premise is an internal caller obligation. It still
275needs to be derived from block output and overlay bounds. This is a symbol
276result, not a complete block or public deflate theorem. -/
277theorem build_tree_send_decodable {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
278    (hI : Out.TreesInvAt h id d b buf) (tk : TK) (v : Nat)
279    (hv : v < tk.buildDesc.elems.toInt.toNat) (hfreq : btFreq tk d v ≠ 0)
280    (hroom : 8 * d.pending.toNat + d.bi_valid.toInt.toNat + 15 ≤ 8 * buf.size) :
281    ∃ (built e : DeflateState) (buf' : Array UInt8) (maxc : Nat),
282      build_tree (Sp id) (some (tk.descRef id)) h = .ok ((), setD h id built) ∧
283      (do build_tree (Sp id) (some (tk.descRef id))
284          send_code (Sp id) (v : Int) (.ref (tk.ref id) 0)) h =
285        .ok ((), Out.setD (Out.setB h b buf') id e) ∧
286      Out.TreesInvAt (Out.setD (Out.setB h b buf') id e) id e b buf' ∧
287      BTBuildFrame tk tk d built ∧ Out.BitsDiff built e ∧
288      (tk.getDesc built).max_code.toInt = maxc ∧
289      maxc < tk.buildDesc.elems.toInt.toNat ∧
290      Out.outBits buf' e = Out.outBits buf d ++
291        Out.natBits (tk.arr built)[v]!.fc.toNat (tk.arr built)[v]!.dl.toNat ∧
292      ∀ suffix : List Bool,
293        ZlibF.Spec.decodeSym
294          (Zlib.Inftrees.Proofs.lensOf (fun n => (tk.arr built)[n]!.dl.toNat) (maxc + 1))
295          (Out.natBits (tk.arr built)[v]!.fc.toNat (tk.arr built)[v]!.dl.toNat ++ suffix) =
296            some (v, suffix) := by
297  obtain ⟨a, built, hbuild, hframe, husable, maxc, hmax, hdesc, haccept, hdecode⟩ :=
298    merge_ws_and (ws_build_tree_frame_initialized (h0 := h) tk hI.base.wf hI.base.static hI.run.to0)
299      (merge_ws_and (ws_build_tree_usable_initialized (h0 := h) tk hI.base.wf hI.base.static hI.run.to0)
300        (ws_build_tree_decodable_initialized (h0 := h) tk hI.base.wf hI.base.static hI.run.to0))
301  have ha : a = () := Subsingleton.elim _ _
302  subst a
303  rw [setD_self hI.base.dstate] at hbuild
304  have hIbuilt := hframe.treesInvAt hI
305  have hbits := hframe.outBits buf
306  have hcount := congrArg List.length hbits
307  simp only [Out.outBits_length] at hcount
308  have hused := husable v hv hfreq
309  have hL : tk.buildDesc.max_length.toInt.toNat ≤ 15 := by cases tk <;> decide +kernel
310  have hsize : tk.buildDesc.elems.toInt.toNat ≤ (tk.arr built).size := by
311    obtain ⟨hLT, hDT, hBT, hBC, hH, hD⟩ := hIbuilt.base.wf
312    cases tk
313    · change 286 ≤ built.dyn_ltree.size; omega
314    · change 30 ≤ built.dyn_dtree.size; omega
315    · change 19 ≤ built.bl_tree.size; omega
316  have hg := tk_get (h0 := h) (id := id) (d := built) tk
317  have hdl : getDl (.ref (tk.ref id) 0) (v : Int) (setD h id built) =
318      .ok ((tk.arr built)[v]!.dl, setD h id built) := by
319    simpa only [getElem!_pos, show v < (tk.arr built).size by omega] using
320      Out.getDl_gen hg (show v < (tk.arr built).size by omega)
321  have hfc : getFc (.ref (tk.ref id) 0) (v : Int) (setD h id built) =
322      .ok ((tk.arr built)[v]!.fc, setD h id built) := by
323    simpa only [getElem!_pos, show v < (tk.arr built).size by omega] using
324      Out.getFc_gen hg (show v < (tk.arr built).size by omega)
325  obtain ⟨buf', e, hsend, hIe, hout, hsize', houtside, hlow, hupp, hdiff⟩ :=
326    Out.send_code_emit hIbuilt (v : Int) (.ref (tk.ref id) 0) _ _ hdl hfc
327      (by omega) hused.2.2.2 (by omega)
328  have hheap : Out.setD (Out.setB (setD h id built) b buf') id e =
329      Out.setD (Out.setB h b buf') id e := by
330    change Out.setD (Out.setB (Out.setD h id built) b buf') id e = _
331    rw [Out.setB_setD, Out.setD_setD]
332  rw [hheap] at hsend hIe
333  have hsend' : send_code (Sp id) (v : Int) (.ref (tk.ref id) 0) (setD h id built) =
334      .ok ((), Out.setD (Out.setB h b buf') id e) := by
335    exact hsend
336  have hIe' : Out.TreesInvAt (Out.setD (Out.setB h b buf') id e) id e b buf' := by
337    exact hIe
338  refine ⟨built, e, buf', maxc, hbuild, ?_, hIe', hframe, hdiff, hdesc, hmax, ?_, hdecode v hv hfreq⟩
339  · rw [bind_app, hbuild]
340    exact hsend'
341  · rw [hout, hbits]
342
343end Zlib.Trees.Proofs