trees.c.bl-tree.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Proof.«trees.c.scan-tree»
2import ZlibF.Math.DeflateBlIndex
3
4/-! # trees.c: constructing the bit-length alphabet
5
6The descending index search follows the reference EmitBlTree structure.
7All called-function behavior comes from proofs about the actual translation.
8-/
9
10namespace Zlib.Trees.Proofs
11open C Zlib.Trees
12
13/-- The actual two scans at the start of build_bl_tree. -/
14def blScanPair (s : DeflateStatePtr) : M Unit := do
15  scan_tree s (← pLtree s) (← rd s).l_desc.max_code
16  scan_tree s (← pDtree s) (← rd s).d_desc.max_code
17
18/-- The actual bit-length construction after frequency scanning. -/
19def blBuild (s : DeflateStatePtr) : M Unit := do
20  blScanPair s
21  build_tree s (← pBldesc s)
22
23def blIndexBody (s : DeflateStatePtr) : Int32 × Bool → M (Int32 × Bool) :=
24  fun (mb, _) => do
25    if (← getDl (← pBltree s) (u8i (← blOrder mb.toInt)).toInt) != 0 then return (mb, true)
26    pure (← isub mb 1, false)
27
28/-- The actual descending index search, including its break flag. -/
29def blIndexLoop (s : DeflateStatePtr) : M (Int32 × Bool) :=
30  cwhile (fun (mb, brk) => pure (!brk && decide (mb.toInt ≥ 3), (mb, brk)))
31    (blIndexBody s) (BL_CODES - 1, false)
32
33def blFinish (s : DeflateStatePtr) : M Int32 := do
34  let (mb, _) ← blIndexLoop s
35  md s fun d => { d with opt_len := d.opt_len + (3 * (i2ul mb + 1) + 5 + 5 + 4) }
36  return mb
37
38/-- Whole-function source equality, in the original call and statement order. -/
39theorem build_bl_tree_eq (s : DeflateStatePtr) :
40    build_bl_tree s = (do blBuild s; blFinish s) := by
41  unfold build_bl_tree blBuild blScanPair blFinish blIndexLoop blIndexBody
42  simp only [M_bind_assoc, M_pure_bind]
43
44/-- Literal and distance data needed by the actual scans. This is a state
45representation; it contains no callee specification or execution premise. -/
46structure BLInput (d : DeflateState) : Prop where
47  l0 : 0 ≤ d.l_desc.max_code.toInt
48  l286 : d.l_desc.max_code.toInt < 286
49  d0 : 0 ≤ d.d_desc.max_code.toInt
50  d30 : d.d_desc.max_code.toInt < 30
51  llen : ∀ i ≤ d.l_desc.max_code.toInt.toNat, d.dyn_ltree[i]!.dl.toNat ≤ 15
52  dlen : ∀ i ≤ d.d_desc.max_code.toInt.toNat, d.dyn_dtree[i]!.dl.toNat ≤ 15
53
54/-- The source alphabets with their actual sentinel writes. -/
55def blScannedState (d : DeflateState) (B : Array CtData) : DeflateState :=
56  { d with
57    dyn_ltree := scGuard d.dyn_ltree d.l_desc.max_code.toInt.toNat,
58    dyn_dtree := scGuard d.dyn_dtree d.d_desc.max_code.toInt.toNat, bl_tree := B }
59
60/-- Mathematical frequency increments of the two source alphabets. -/
61def blScanCount (d : DeflateState) (k : Nat) : Nat :=
62  Out.scanFreqUpTo (Out.guarded (fun i => d.dyn_ltree[i]!.dl.toNat) d.l_desc.max_code.toInt.toNat)
63    (d.l_desc.max_code.toInt.toNat + 1) k +
64  Out.scanFreqUpTo (Out.guarded (fun i => d.dyn_dtree[i]!.dl.toNat) d.d_desc.max_code.toInt.toNat)
65    (d.d_desc.max_code.toInt.toNat + 1) k
66
67/-- Both actual scans compose on one live heap. Their exact record effects
68retain both sentinels and sum their 16-bit frequency additions. -/
69theorem bl_scan_pair {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
70    (hI : Out.TreesInvAt h id d b buf) (hin : BLInput d) :
71    ∃ (e : DeflateState) (B : Array CtData),
72      blScanPair (Sp id) h = .ok ((), setD h id e) ∧ e = blScannedState d B ∧
73      Out.TreesInvAt (setD h id e) id e b buf ∧ Out.outBits buf e = Out.outBits buf d ∧
74      B.size = d.bl_tree.size ∧ (∀ k : Nat, B[k]!.dl = d.bl_tree[k]!.dl) ∧
75      ∀ k : Nat, B[k]!.fc = d.bl_tree[k]!.fc + UInt16.ofNat (blScanCount d k) := by
76  obtain ⟨e1, B1, hr1, he1, hI1, hout1, hB1, hdl1, hfc1⟩ :=
77    scan_tree_preserves hI .lit (by decide +kernel) d.l_desc.max_code hin.l0 hin.l286 hin.llen
78  have hdesc : e1.d_desc = d.d_desc := by rw [he1]; rfl
79  have htree : e1.dyn_dtree = d.dyn_dtree := by rw [he1]; rfl
80  have hdlen : ∀ i ≤ e1.d_desc.max_code.toInt.toNat, e1.dyn_dtree[i]!.dl.toNat ≤ 15 := by
81    rw [hdesc, htree]
82    exact hin.dlen
83  obtain ⟨e2, B2, hr2, he2, hI2, hout2, hB2, hdl2, hfc2⟩ :=
84    scan_tree_preserves hI1 .dist (by decide +kernel) e1.d_desc.max_code
85      (by rw [hdesc]; exact hin.d0) (by rw [hdesc]; exact hin.d30) hdlen
86  have heB1 : e1.bl_tree = B1 := by rw [he1]
87  rw [setD_setD] at hr2 hI2
88  simp only [TK.ref] at hr1 hr2
89  refine ⟨e2, B2, ?_, ?_, hI2, hout2.trans hout1, ?_, ?_, ?_⟩
90  · have hp1 := Out.pLtree_run hI.base.dstate
91    have hd1 := Out.rd_run hI.base.dstate
92    have hp2 := Out.pDtree_run (setD_dstates_same h id e1)
93    have hd2 := Out.rd_run (setD_dstates_same h id e1)
94    unfold blScanPair
95    rw [bind_app, hp1]
96    simp only []
97    rw [bind_app, hd1]
98    simp only []
99    rw [bind_app, hr1]
100    simp only []
101    rw [bind_app, hp2]
102    simp only []
103    rw [bind_app, hd2]
104    exact hr2
105  · rw [he2, he1]
106    rfl
107  · rw [hB2, heB1, hB1]
108  · intro k
109    rw [hdl2 k, heB1, hdl1 k]
110  · intro k
111    rw [hfc2 k, heB1, hfc1 k]
112    simp only [TK.arr, hdesc, htree, blScanCount, UInt16.ofNat_add, UInt16.add_assoc]
113
114/-- The bit-length symbol at each rank of the actual fixed permutation. -/
115def blUsed (d : DeflateState) (m : Nat) : Bool :=
116  d.bl_tree[bl_order[m]!.toNat]!.dl != 0
117
118theorem bl_order_bound (m : Nat) (hm : m < 19) : bl_order[m]!.toNat < 19 := by
119  have h : ∀ i : Fin 19, bl_order[i.val]!.toNat < 19 := by decide +kernel
120  exact h ⟨m, hm⟩
121
122theorem ws_blPtr {h0 : Heap} {id : Nat} {d : DeflateState} :
123    WS h0 id (pBltree (Sp id)) d (fun p e => p = .ref (.dstate_bl_tree id) 0 ∧ e = d) := by
124  unfold pBltree
125  refine WS.bind' ws_sid fun i e ⟨hi, he⟩ => ?_
126  subst i; subst e
127  exact WS.pure' ⟨rfl, rfl⟩
128
129theorem ws_blOrder {h0 : Heap} {id : Nat} {d : DeflateState} (i : Int)
130    (hi0 : 0 ≤ i) (hi19 : i < 19) :
131    WS h0 id (blOrder i) d (fun v e => v = bl_order[i.toNat]! ∧ e = d) := by
132  unfold blOrder
133  rw [ite_eq_left ⟨hi0, hi19⟩]
134  exact WS.pure' ⟨rfl, rfl⟩
135
136/-- The actual read/test/decrement body does not change the heap. -/
137theorem ws_blIndexBody {h0 : Heap} {id : Nat} {d : DeflateState} (mb : Int32) (m : Nat)
138    (hm : mb.toInt = m) (hm3 : 3 ≤ m) (hm18 : m ≤ 18) (hB : 19 ≤ d.bl_tree.size) :
139    WS h0 id (blIndexBody (Sp id) (mb, false)) d (fun r e => e = d ∧
140      ((r.1 = mb ∧ r.2 = true ∧ blUsed d m = true) ∨
141       (r.1.toInt = (m : Int) - 1 ∧ r.2 = false ∧ blUsed d m = false))) := by
142  have hmN : mb.toInt.toNat = m := by omega
143  unfold blIndexBody
144  refine WS.bind' ws_blPtr fun p e ⟨hp, he⟩ => ?_
145  subst p; subst e
146  refine WS.bind' (ws_blOrder mb.toInt (by omega) (by omega)) fun ord e ⟨ho, he⟩ => ?_
147  subst e; subst ord
148  rw [hmN]
149  have hu : (u8i bl_order[m]!).toInt = bl_order[m]!.toNat := by
150    unfold u8i
151    have hbyte := (bl_order[m]!).toNat_lt
152    exact Out.i32_ofInt_toInt (by omega) (by omega)
153  have hi := bl_order_bound m (by omega)
154  refine WS.bind' (ws_getDl .bl (u8i bl_order[m]!).toInt (by omega)
155    (by change (u8i bl_order[m]!).toInt < d.bl_tree.size; omega)) fun len e ⟨hlen, he⟩ => ?_
156  subst e; subst len
157  have hidx : (u8i bl_order[m]!).toInt.toNat = bl_order[m]!.toNat := by rw [hu]; rfl
158  simp only [hidx]
159  change WS h0 id (if blUsed d m = true then pure (mb, true) else do pure (← isub mb 1, false)) d _
160  by_cases hz : blUsed d m = true
161  · rw [ite_eq_left hz]
162    exact WS.pure' ⟨rfl, Or.inl ⟨rfl, rfl, hz⟩⟩
163  · rw [ite_eq_right hz]
164    have hone : (1 : Int32).toInt = 1 := rfl
165    refine WS.bind' (ws_isub mb 1 (by omega) (by omega)) fun mb1 e ⟨hmb1, he⟩ => ?_
166    subst e
167    exact WS.pure' ⟨rfl, Or.inr ⟨by dsimp only; omega, rfl, Bool.eq_false_iff.mpr hz⟩⟩
168
169/-- Complete actual descending search, with its exact mathematical maximum.
170The generic search can return two. A four-entry header requires the separate
171caller-history argument showing a used rank at least three. -/
172theorem ws_blIndexLoop {h0 : Heap} {id : Nat} {d : DeflateState} (hB : 19 ≤ d.bl_tree.size) :
173    WS h0 id (blIndexLoop (Sp id)) d (fun r e =>
174      e = d ∧ r.1.toInt = Math.blMaxIdx (blUsed d) 18) := by
175  let R := Math.blMaxIdx (blUsed d) 18
176  let Inv : Int32 × Bool → DeflateState → Prop := fun r e =>
177    e = d ∧ ∃ m : Nat, 2 ≤ m ∧ m ≤ 18 ∧ r.1.toInt = m ∧
178      ((r.2 = false ∧ Math.blMaxIdx (blUsed d) m = R) ∨ (r.2 = true ∧ m = R))
179  unfold blIndexLoop
180  refine WS.cwhile2 Inv (fun r _ => if r.2 then 0 else r.1.toInt.toNat) _ ?_
181    ⟨rfl, 18, by omega, by omega, rfl, Or.inl ⟨rfl, rfl⟩⟩ (by simp only [fuel]; decide +kernel)
182  rintro ⟨mb, brk⟩ e ⟨he, m, hm2, hm18, hm, hcase⟩
183  subst e
184  dsimp only at hm hcase ⊢
185  rcases hcase with ⟨hbrk, hmax⟩ | ⟨hbrk, hmax⟩
186  · subst brk
187    by_cases hm3 : 3 ≤ m
188    · refine WS.pure' (Or.inr ⟨by simp only [Bool.not_false, Bool.true_and, decide_eq_true_eq]; omega, ?_⟩)
189      refine WS.mono (ws_blIndexBody mb m hm hm3 hm18 hB) ?_
190      rintro r e ⟨he, hbranch⟩
191      subst e
192      rcases hbranch with hused | hzero
193      · obtain ⟨hr, hb, hu⟩ := hused
194        have hR : m = R := by
195          rw [Math.blMaxIdx_step (blUsed d) m hm3, ite_eq_left hu] at hmax
196          exact hmax
197        refine ⟨⟨rfl, m, hm2, hm18, by rw [hr]; exact hm, Or.inr ⟨hb, hR⟩⟩, ?_⟩
198        change (if r.2 then 0 else r.1.toInt.toNat) < mb.toInt.toNat
199        rw [hb]
200        change 0 < mb.toInt.toNat
201        omega
202      · obtain ⟨hr, hb, hu⟩ := hzero
203        have hmax' : Math.blMaxIdx (blUsed d) (m - 1) = R := by
204          rw [Math.blMaxIdx_step (blUsed d) m hm3, ite_eq_right (show ¬ blUsed d m = true by rw [hu]; decide +kernel)] at hmax
205          exact hmax
206        refine ⟨⟨rfl, m - 1, by omega, by omega, by omega, Or.inl ⟨hb, hmax'⟩⟩, ?_⟩
207        simp only [hb, Bool.false_eq_true, ite_false]
208        omega
209    · refine WS.pure' (Or.inl ⟨by simp only [Bool.not_false, Bool.true_and, decide_eq_false_iff_not]; omega, ?_⟩)
210      have hmval : m = 2 := by omega
211      rw [hmval] at hm hmax
212      exact ⟨rfl, hm.trans (show (2 : Int) = R from by change (2 : Int) = (R : Nat); rw [← hmax]; rfl)⟩
213  · subst brk
214    refine WS.pure' (Or.inl ⟨by simp, rfl, ?_⟩)
215    exact hm.trans (by rw [hmax])
216
217/-- Mathematical header cost, computed with the same unsigned arithmetic. -/
218def blHeaderCost (m : Nat) : UInt64 := 3 * (UInt64.ofNat m + 1) + 5 + 5 + 4
219
220/-- The actual search and unsigned cost update, with exact returned index. -/
221theorem ws_blFinish {h0 : Heap} {id : Nat} {d : DeflateState} (hB : 19 ≤ d.bl_tree.size) :
222    WS h0 id (blFinish (Sp id)) d (fun mb e =>
223      mb.toInt = Math.blMaxIdx (blUsed d) 18 ∧
224      e = { d with opt_len := d.opt_len + blHeaderCost (Math.blMaxIdx (blUsed d) 18) }) := by
225  have hlo := Math.blMaxIdx_ge (blUsed d) 18 (by omega)
226  have hhi := Math.blMaxIdx_le (blUsed d) 18
227  unfold blFinish
228  refine WS.bind' (ws_blIndexLoop hB) fun r e ⟨he, hmb⟩ => ?_
229  subst e
230  rcases r with ⟨mb, brk⟩
231  dsimp only at hmb ⊢
232  have hul : i2ul mb = UInt64.ofNat (Math.blMaxIdx (blUsed d) 18) := by
233    rw [i2ul_eq mb (by omega) (by omega)]
234    congr 1
235    omega
236  rw [hul]
237  refine WS.bind' (ws_md _) fun _ e he => ?_
238  subst e
239  refine WS.pure' ⟨hmb, ?_⟩
240  with_reducible dsimp only [blHeaderCost]
241
242/-- Code-array facts for the actual bit-length alphabet. The source state
243records the frequencies seen by build_tree. The result uses the independent
244format decoder, actual descriptor maximum and final stored code words. -/
245def BLCodeResult (source built : DeflateState) : Prop :=
246  ∃ maxc : Nat, maxc < 19 ∧ built.bl_desc.max_code.toInt = maxc ∧
247    ZlibF.Spec.Acceptable .codeLength
248      (Zlib.Inftrees.Proofs.lensOf (fun v => built.bl_tree[v]!.dl.toNat) (maxc + 1)) ∧
249    ∀ v < 19, source.bl_tree[v]!.fc ≠ 0 →
250      (1 ≤ built.bl_tree[v]!.dl.toNat ∧ built.bl_tree[v]!.dl.toNat ≤ 7 ∧
251        built.bl_tree[v]!.fc.toNat = Math.storedCode
252          (fun b => built.bl_count[b]!.toNat) (fun n => built.bl_tree[n]!.dl.toNat) v ∧
253        built.bl_tree[v]!.fc.toNat < 2 ^ built.bl_tree[v]!.dl.toNat) ∧
254      ∀ suffix : List Bool,
255        ZlibF.Spec.decodeSym
256          (Zlib.Inftrees.Proofs.lensOf (fun n => built.bl_tree[n]!.dl.toNat) (maxc + 1))
257          (Out.natBits built.bl_tree[v]!.fc.toNat built.bl_tree[v]!.dl.toNat ++ suffix) = some (v, suffix)
258
259/-- Scanning both source trees and constructing the bit-length tree compose
260using actual callees. Their exact frequency source and output frame remain
261available alongside the independent symbol-decoding result. -/
262theorem bl_build {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
263    (hI : Out.TreesInvAt h id d b buf) (hin : BLInput d) :
264    ∃ (scanned built : DeflateState) (B : Array CtData),
265      blBuild (Sp id) h = .ok ((), setD h id built) ∧
266      scanned = blScannedState d B ∧ B.size = d.bl_tree.size ∧
267      (∀ k : Nat, B[k]!.fc = d.bl_tree[k]!.fc + UInt16.ofNat (blScanCount d k)) ∧
268      BTBuildFrame .bl .bl scanned built ∧ Out.TreesInvAt (setD h id built) id built b buf ∧
269      Out.outBits buf built = Out.outBits buf d ∧ BLCodeResult scanned built := by
270  obtain ⟨scanned, B, hr, hs, hIS, houtS, hBs, hdl, hfreq⟩ := bl_scan_pair hI hin
271  obtain ⟨a, built, hbuild, hframe, husable, M, hM, hmax, haccept, hdecode⟩ := merge_ws_and
272    (ws_build_tree_frame_initialized (h0 := h) .bl hIS.base.wf hIS.base.static hIS.run.to0)
273    (merge_ws_and (ws_build_tree_usable_initialized (h0 := h) .bl hIS.base.wf hIS.base.static hIS.run.to0)
274      (ws_build_tree_decodable_initialized (h0 := h) .bl hIS.base.wf hIS.base.static hIS.run.to0))
275  have ha : a = () := Subsingleton.elim _ _
276  subst a
277  have hIB := hframe.treesInvAt hIS
278  rw [setD_setD] at hIB
279  refine ⟨scanned, built, B, ?_, hs, hBs, hfreq, hframe, hIB,
280    (hframe.outBits buf).trans houtS, ?_⟩
281  · have hp : pBldesc (Sp id) (setD h id scanned) =
282        .ok (some (.in_dstate_bl_desc id), setD h id scanned) := by
283      unfold pBldesc
284      rw [bind_app, Out.sid_run (setD_dstates_same h id scanned)]
285      rfl
286    unfold blBuild
287    rw [bind_app, hr]
288    simp only []
289    rw [bind_app, hp]
290    exact hbuild
291  · refine ⟨M, hM, hmax, haccept .codeLength, ?_⟩
292    intro v hv hf
293    exact ⟨husable v hv hf, hdecode v hv hf⟩
294
295/-- Changing the unsigned tree-description cost retains every code and
296output field. -/
297theorem blCost_frame (d : DeflateState) (O : UInt64) :
298    BTBuildFrame .bl .bl d { d with opt_len := O } := by
299  refine ⟨d.bl_tree, d.heap, d.depth, d.bl_count, d.heap_len, d.heap_max,
300    d.bl_desc.max_code, O, d.static_len, rfl, rfl, rfl, rfl, rfl⟩
301
302/-- `local int build_bl_tree(deflate_state *s)`.
303The complete actual function executes from the literal/distance data supplied
304by their constructors. It returns the exact descending-search index, applies
305the exact unsigned header cost, preserves output state and establishes the
306bit-length codes' independent decoder meaning. The generic index bound is
307two through eighteen; proving the four-code format minimum needs the actual
308source-tree/frequency history, not a stronger assumed search invariant. -/
309theorem build_bl_tree_checked {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
310    (hI : Out.TreesInvAt h id d b buf) (hin : BLInput d) :
311    ∃ (mb : Int32) (scanned built e : DeflateState) (B : Array CtData),
312      build_bl_tree (Sp id) h = .ok (mb, setD h id e) ∧
313      scanned = blScannedState d B ∧
314      (∀ k : Nat, B[k]!.fc = d.bl_tree[k]!.fc + UInt16.ofNat (blScanCount d k)) ∧
315      BTBuildFrame .bl .bl scanned built ∧
316      e = { built with opt_len := built.opt_len + blHeaderCost (Math.blMaxIdx (blUsed built) 18) } ∧
317      mb.toInt = Math.blMaxIdx (blUsed built) 18 ∧ 2 ≤ mb.toInt ∧ mb.toInt ≤ 18 ∧
318      (∀ rank, mb.toInt.toNat < rank → rank ≤ 18 → blUsed e rank = false) ∧
319      Out.TreesInvAt (setD h id e) id e b buf ∧ Out.outBits buf e = Out.outBits buf d ∧
320      BLCodeResult scanned e := by
321  obtain ⟨scanned, built, B, hb, hs, hBs, hfreq, hframe, hIB, houtB, hcodes⟩ := bl_build hI hin
322  obtain ⟨mb, e, hfinish, hmb, he⟩ := ws_blFinish (h0 := h) (id := id) (d := built)
323    (by obtain ⟨hl, hd, hbl, rest⟩ := hIB.base.wf; omega)
324  have hcost := blCost_frame built (built.opt_len + blHeaderCost (Math.blMaxIdx (blUsed built) 18))
325  have hIe := hcost.treesInvAt hIB
326  rw [setD_setD] at hIe
327  have hlo := Math.blMaxIdx_ge (blUsed built) 18 (by omega)
328  have hhi := Math.blMaxIdx_le (blUsed built) 18
329  refine ⟨mb, scanned, built, e, B, ?_, hs, hfreq, hframe, he, hmb, by omega, by omega, ?_, ?_, ?_, ?_⟩
330  · rw [build_bl_tree_eq, bind_app, hb]
331    exact hfinish
332  · intro rank hr hr18
333    rw [he]
334    change blUsed built rank = false
335    exact Math.blMaxIdx_suffix (blUsed built) 18 rank (by omega) hr18
336  · rw [he]; exact hIe
337  · rw [he]
338    exact (hcost.outBits buf).trans houtB
339  · rw [he]
340    exact hcodes
341
342/-- A tree constructor retains every other descriptor exactly. -/
343theorem BTBuildFrame.other_desc {tk dk : TK} {d e : DeflateState}
344    (hi : BTBuildFrame tk dk d e) (other : TK) (hne : other ≠ dk) :
345    other.getDesc e = other.getDesc d := by
346  obtain ⟨T, H, D, B, hl, hm, mc, O, S, rfl, rest⟩ := hi
347  cases tk <;> cases dk <;> cases other <;> first | exact False.elim (hne rfl) | rfl
348
349/-- The adjacent literal and distance construction calls in _tr_flush_block. -/
350def blPrepare (s : DeflateStatePtr) : M Unit := do
351  build_tree s (← pLdesc s)
352  build_tree s (← pDdesc s)
353
354/-- Actual literal and distance construction establishes the complete input
355representation for build_bl_tree. Their calls preserve the bit-length
356frequencies, so the later zero-initialization history can be transported. -/
357theorem bl_prepare {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
358    (hI : Out.TreesInvAt h id d b buf) :
359    ∃ e : DeflateState, blPrepare (Sp id) h = .ok ((), setD h id e) ∧
360      BLInput e ∧ Out.TreesInvAt (setD h id e) id e b buf ∧
361      e.bl_tree = d.bl_tree ∧ Out.outBits buf e = Out.outBits buf d := by
362  obtain ⟨aL, lit, hrL, hframeL, ML, hML, hmaxL, haccL, hdecodeL⟩ := merge_ws_and
363    (ws_build_tree_frame_initialized (h0 := h) .lit hI.base.wf hI.base.static hI.run.to0)
364    (ws_build_tree_decodable_initialized (h0 := h) .lit hI.base.wf hI.base.static hI.run.to0)
365  have haL : aL = () := Subsingleton.elim _ _
366  subst aL
367  rw [setD_self hI.base.dstate] at hrL
368  have hIL := hframeL.treesInvAt hI
369  obtain ⟨aD, dist, hrD, hframeD, MD, hMD, hmaxD, haccD, hdecodeD⟩ := merge_ws_and
370    (ws_build_tree_frame_initialized (h0 := h) .dist hIL.base.wf hIL.base.static hIL.run.to0)
371    (ws_build_tree_decodable_initialized (h0 := h) .dist hIL.base.wf hIL.base.static hIL.run.to0)
372  have haD : aD = () := Subsingleton.elim _ _
373  subst aD
374  simp only [TK.descRef] at hrL hrD
375  have hID := hframeD.treesInvAt hIL
376  rw [setD_setD] at hID
377  have hlDesc := hframeD.other_desc .lit (by decide +kernel)
378  have hlTree := hframeD.other_tree .lit (by decide +kernel)
379  have hbTreeL := hframeL.other_tree .bl (by decide +kernel)
380  have hbTreeD := hframeD.other_tree .bl (by decide +kernel)
381  have hlenL := acceptable_scan_lengths .lit lit ML (haccL .codeLength)
382  have hlenD := acceptable_scan_lengths .dist dist MD (haccD .codeLength)
383  simp only [TK.getDesc, TK.arr] at hlDesc hlTree hbTreeL hbTreeD hmaxL hmaxD hlenL hlenD
384  change ML < 286 at hML
385  change MD < 30 at hMD
386  have hin : BLInput dist := by
387    refine ⟨by rw [hlDesc]; omega, by rw [hlDesc]; omega, by omega, by omega, ?_, ?_⟩
388    · intro i hi
389      rw [hlDesc] at hi
390      rw [hlTree]
391      exact hlenL i (by omega)
392    · intro i hi
393      exact hlenD i (by omega)
394  refine ⟨dist, ?_, hin, hID, hbTreeD.trans hbTreeL,
395    (hframeD.outBits buf).trans (hframeL.outBits buf)⟩
396  have hpL : pLdesc (Sp id) h = .ok (some (.in_dstate_l_desc id), h) := by
397    unfold pLdesc
398    rw [bind_app, Out.sid_run hI.base.dstate]
399    rfl
400  have hpD : pDdesc (Sp id) (setD h id lit) =
401      .ok (some (.in_dstate_d_desc id), setD h id lit) := by
402    unfold pDdesc
403    rw [bind_app, Out.sid_run (setD_dstates_same h id lit)]
404    rfl
405  unfold blPrepare
406  rw [bind_app, hpL]
407  simp only []
408  rw [bind_app, hrL]
409  simp only []
410  rw [bind_app, hpD]
411  exact hrD
412
413/-- The three actual tree constructors and both actual code-length scans
414compose from the existing live tree representation. BLInput is established
415by actual earlier calls, rather than assumed at this entry. This remains a
416local tree-description theorem; full block emission and engine integration
417are separate obligations. -/
418theorem prepare_build_bl_tree {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
419    (hI : Out.TreesInvAt h id d b buf) :
420    ∃ (mb : Int32) (ready scanned built e : DeflateState) (B : Array CtData),
421      blPrepare (Sp id) h = .ok ((), setD h id ready) ∧ BLInput ready ∧
422      (do blPrepare (Sp id); build_bl_tree (Sp id)) h = .ok (mb, setD h id e) ∧
423      scanned = blScannedState ready B ∧
424      (∀ k : Nat, B[k]!.fc = d.bl_tree[k]!.fc + UInt16.ofNat (blScanCount ready k)) ∧
425      BTBuildFrame .bl .bl scanned built ∧
426      e = { built with opt_len := built.opt_len + blHeaderCost (Math.blMaxIdx (blUsed built) 18) } ∧
427      mb.toInt = Math.blMaxIdx (blUsed built) 18 ∧ 2 ≤ mb.toInt ∧ mb.toInt ≤ 18 ∧
428      Out.TreesInvAt (setD h id e) id e b buf ∧ Out.outBits buf e = Out.outBits buf d ∧
429      BLCodeResult scanned e := by
430  obtain ⟨ready, hready, hin, hIR, hBready, houtR⟩ := bl_prepare hI
431  obtain ⟨mb, scanned, built, e, B, hbuild, hs, hfreq, hframe, he, hmb, hlo, hhi, htail, hIe, hout, hcodes⟩ :=
432    build_bl_tree_checked hIR hin
433  rw [setD_setD] at hbuild hIe
434  refine ⟨mb, ready, scanned, built, e, B, hready, hin, ?_, hs, ?_, hframe, he, hmb, hlo, hhi,
435    hIe, hout.trans houtR, hcodes⟩
436  · rw [bind_app, hready]
437    exact hbuild
438  · intro k
439    rw [hfreq k, hBready]
440
441/-- Frequency increments are bounded by the finite alphabets, independently
442of total input size or the old frequency values. -/
443theorem blScanCount_le (d : DeflateState) (hin : BLInput d) (k : Nat) : blScanCount d k ≤ 316 := by
444  have hl : ∀ i, Out.guarded (fun i => d.dyn_ltree[i]!.dl.toNat) d.l_desc.max_code.toInt.toNat i < 65536 := by
445    intro i
446    unfold Out.guarded
447    split
448    · decide +kernel
449    · exact UInt16.toNat_lt _
450  have hd : ∀ i, Out.guarded (fun i => d.dyn_dtree[i]!.dl.toNat) d.d_desc.max_code.toInt.toNat i < 65536 := by
451    intro i
452    unfold Out.guarded
453    split
454    · decide +kernel
455    · exact UInt16.toNat_lt _
456  have hL := scanFreq_le _ hl (d.l_desc.max_code.toInt.toNat + 1) k
457  have hD := scanFreq_le _ hd (d.d_desc.max_code.toInt.toNat + 1) k
458  have hL0 := hin.l0
459  have hL286 := hin.l286
460  have hD0 := hin.d0
461  have hD30 := hin.d30
462  unfold blScanCount
463  omega
464
465/-- Zero initialization makes the actual two-scan frequency cells exact
466natural counts, with no 16-bit wrap. This is an internal data premise; the
467following init-to-scans theorem establishes it by actual initialization. -/
468theorem bl_scan_pair_zero {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
469    (hI : Out.TreesInvAt h id d b buf) (hin : BLInput d)
470    (hz : ∀ k < 19, d.bl_tree[k]!.fc = 0) :
471    ∃ (e : DeflateState) (B : Array CtData),
472      blScanPair (Sp id) h = .ok ((), setD h id e) ∧ e = blScannedState d B ∧
473      Out.TreesInvAt (setD h id e) id e b buf ∧
474      ∀ k < 19, B[k]!.fc.toNat = blScanCount d k ∧ B[k]!.fc.toNat ≤ 316 := by
475  obtain ⟨e, B, hr, he, hIe, hout, hBs, hdl, hfc⟩ := bl_scan_pair hI hin
476  refine ⟨e, B, hr, he, hIe, ?_⟩
477  intro k hk
478  have hb := blScanCount_le d hin k
479  have hv : B[k]!.fc.toNat = blScanCount d k := by
480    rw [hfc k, hz k hk, UInt16.zero_add, UInt16.toNat_ofNat']
481    exact Nat.mod_eq_of_lt (by omega)
482  exact ⟨hv, by omega⟩
483
484/-- Actual init_block establishes zero bit-length frequencies. Both actual
485source-tree constructors preserve them, and both scans then store their
486exact natural counts. This is an init-to-call composition; it is not yet the
487streaming proof that arbitrary intervening symbol tallies retain the same
488entry facts. -/
489theorem init_prepare_scans {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
490    (hI : Out.TreesInvAt h id d b buf) :
491    ∃ (initialized ready scanned : DeflateState) (B : Array CtData),
492      (do init_block (Sp id); blPrepare (Sp id); blScanPair (Sp id)) h =
493        .ok ((), setD h id scanned) ∧
494      init_block (Sp id) h = .ok ((), setD h id initialized) ∧
495      BLInput ready ∧ scanned = blScannedState ready B ∧
496      Out.TreesInvAt (setD h id scanned) id scanned b buf ∧
497      ∀ k < 19, B[k]!.fc.toNat = blScanCount ready k ∧ B[k]!.fc.toNat ≤ 316 := by
498  obtain ⟨aL, aD, aB, initialized, hinit, hII, heI, hLs, hDs, hBs,
499    hLzero, hEOB, hDzero, hBzero, hLdl, hDdl, hBdl⟩ := Out.init_block_spec0 hI.base hI.run.to0
500  change init_block (Sp id) h = .ok ((), setD h id initialized) at hinit
501  change Out.TreesInvAt (setD h id initialized) id initialized b buf at hII
502  have hzI : ∀ k < 19, initialized.bl_tree[k]!.fc = 0 := by
503    intro k hk
504    rw [heI]
505    exact hBzero k hk
506  obtain ⟨ready, hprepare, hin, hIR, hBready, hout⟩ := bl_prepare hII
507  have hzR : ∀ k < 19, ready.bl_tree[k]!.fc = 0 := by
508    rw [hBready]
509    exact hzI
510  obtain ⟨scanned, B, hscan, hs, hIS, hcounts⟩ := bl_scan_pair_zero hIR hin hzR
511  rw [setD_setD] at hprepare
512  simp only [setD_setD] at hscan hIS
513  refine ⟨initialized, ready, scanned, B, ?_, hinit, hin, hs, hIS, hcounts⟩
514  rw [bind_app, hinit]
515  simp only []
516  rw [bind_app, hprepare]
517  exact hscan
518
519/-- Scanning only changes the literal sentinel beyond the live alphabet. -/
520theorem blScannedState_lit_get (d : DeflateState) (B : Array CtData) (i : Nat)
521    (hi : i ≤ d.l_desc.max_code.toInt.toNat) :
522    (blScannedState d B).dyn_ltree[i]! = d.dyn_ltree[i]! := by
523  unfold blScannedState scGuard
524  rw [Out.getElem!_set!]
525  rw [ite_eq_right (show ¬ (d.l_desc.max_code.toInt.toNat + 1 = i ∧
526    d.l_desc.max_code.toInt.toNat + 1 < d.dyn_ltree.size) by omega)]
527
528/-- Scanning only changes the distance sentinel beyond the live alphabet. -/
529theorem blScannedState_dist_get (d : DeflateState) (B : Array CtData) (i : Nat)
530    (hi : i ≤ d.d_desc.max_code.toInt.toNat) :
531    (blScannedState d B).dyn_dtree[i]! = d.dyn_dtree[i]! := by
532  unfold blScannedState scGuard
533  rw [Out.getElem!_set!]
534  rw [ite_eq_right (show ¬ (d.d_desc.max_code.toInt.toNat + 1 = i ∧
535    d.d_desc.max_code.toInt.toNat + 1 < d.dyn_dtree.size) by omega)]
536
537/-- Complete actual build_bl_tree preserves both live source alphabets'
538code words, lengths and descriptors. This transports their decoder meaning
539to the same heap on which the tree descriptions and block will be emitted. -/
540theorem build_bl_preserves_source_codes {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
541    (hI : Out.TreesInvAt h id d b buf) (hin : BLInput d) :
542    ∃ (mb : Int32) (e : DeflateState),
543      build_bl_tree (Sp id) h = .ok (mb, setD h id e) ∧
544      e.l_desc = d.l_desc ∧ e.d_desc = d.d_desc ∧
545      (∀ i ≤ d.l_desc.max_code.toInt.toNat, e.dyn_ltree[i]! = d.dyn_ltree[i]!) ∧
546      (∀ i ≤ d.d_desc.max_code.toInt.toNat, e.dyn_dtree[i]! = d.dyn_dtree[i]!) ∧
547      Out.TreesInvAt (setD h id e) id e b buf ∧ Out.outBits buf e = Out.outBits buf d := by
548  obtain ⟨mb, scanned, built, e, B, hr, hs, hfreq, hframe, he, hmb, hlo, hhi, htail, hIe, hout, hcodes⟩ :=
549    build_bl_tree_checked hI hin
550  have hlDesc := hframe.other_desc .lit (by decide +kernel)
551  have hdDesc := hframe.other_desc .dist (by decide +kernel)
552  have hlTree := hframe.other_tree .lit (by decide +kernel)
553  have hdTree := hframe.other_tree .dist (by decide +kernel)
554  simp only [TK.getDesc, TK.arr] at hlDesc hdDesc hlTree hdTree
555  refine ⟨mb, e, hr, ?_, ?_, ?_, ?_, hIe, hout⟩
556  · rw [he]
557    change built.l_desc = d.l_desc
558    rw [hlDesc, hs]
559    rfl
560  · rw [he]
561    change built.d_desc = d.d_desc
562    rw [hdDesc, hs]
563    rfl
564  · intro i hi
565    rw [he]
566    change built.dyn_ltree[i]! = d.dyn_ltree[i]!
567    rw [hlTree, hs]
568    exact blScannedState_lit_get d B i hi
569  · intro i hi
570    rw [he]
571    change built.dyn_dtree[i]! = d.dyn_dtree[i]!
572    rw [hdTree, hs]
573    exact blScannedState_dist_get d B i hi
574
575/-- Every ordinary length symbol is beyond the first three repetition-only
576ranks of the actual fixed permutation. -/
577theorem bl_order_nonrepeat_rank (code : Nat) (hc : code < 16) :
578    ∃ rank : Nat, 3 ≤ rank ∧ rank ≤ 18 ∧ bl_order[rank]!.toNat = code := by
579  have h : ∀ c : Fin 16, ∃ r : Fin 19, 3 ≤ r.val ∧ bl_order[r.val]!.toNat = c.val := by
580    decide +kernel
581  obtain ⟨r, hr3, he⟩ := h ⟨code, hc⟩
582  exact ⟨r.val, hr3, by have := r.isLt; omega, he⟩
583
584/-- A represented non-repeat length code supplies the table/search part of
585the four-entry format minimum. Actual scan-frequency support must establish
586the premise; it is not a new caller precondition. -/
587theorem bl_index_ge_of_nonrepeat (d : DeflateState) (code : Nat) (hc : code < 16)
588    (hlen : d.bl_tree[code]!.dl ≠ 0) : 3 ≤ Math.blMaxIdx (blUsed d) 18 := by
589  obtain ⟨rank, hr3, hr18, he⟩ := bl_order_nonrepeat_rank code hc
590  have hu : blUsed d rank = true := by
591    unfold blUsed
592    rw [he]
593    exact bne_iff_ne.mpr hlen
594  have hb := Math.blMaxIdx_ge_of_used (blUsed d) 18 rank hr3 hr18 hu
595  omega
596
597end Zlib.Trees.Proofs