trees.c.build.forest.lean

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

1import ZlibF.Proof.«trees.c.build.merge»
2import ZlibF.Proof.«trees.c.heap.gbre»
3import ZlibF.Math.DeflateForest
4
5/-! # trees.c: retaining the forest represented by the heap queue and tail -/
6
7namespace Zlib.Trees.Proofs
8open C Zlib.Trees
9
10/-- The actual two-node selection and child stores preserve every previously
11stored tail cell. The queue/tail gap is numeric data, not a callee contract. -/
12theorem ws_btMergeOpen_tail {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (len : Nat)
13    (hlen : d.heap_len.toInt = len) (h2 : 2 ≤ len) (hsz : len < d.heap.size)
14    (hbig : d.heap.size ≤ 573) (hmH : d.heap_max.toInt ≤ d.heap.size)
15    (hgap : (len : Int) < d.heap_max.toInt - 1)
16    (hval : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr d) d.depth d.heap[i]!)
17    (hinj : ∀ i j, 1 ≤ i → i ≤ len → 1 ≤ j → j ≤ len → d.heap[i]! = d.heap[j]! → i = j)
18    (ho : HeapOK (sm (tk.arr d) d.depth) (fun i => d.heap[i]!) len 0) :
19    WS h0 id (btMergeOpen (Sp id) (.ref (tk.ref id) 0)) d (fun _ e =>
20      ∀ q : Nat, d.heap_max.toInt ≤ (q : Int) → e.heap[q]! = d.heap[q]!) := by
21  unfold btMergeOpen
22  refine WS.bind' (ws_btPick2 tk d len hlen h2 hsz hbig hval hinj ho)
23    fun pair e1 ⟨hl, H, hn, hm, hhl, he1, hsH, hframe, hp, horder, hnv, hmv, hnm,
24      hminn, hminm, horigin, hcomplete, hno, hHinj, hcount⟩ => ?_
25  subst e1
26  rcases pair with ⟨n, m⟩
27  refine WS.bind' (ws_btKeepChildren { d with heap := H, heap_len := hl } n m
28    (by dsimp only; omega) (by dsimp only; omega) (by dsimp only; omega))
29    fun _ e2 ⟨hm1, hm2, hh1, hh2, he2, hsH', hnKeep, hmKeep, hKeepFrame⟩ => ?_
30  subst e2
31  refine WS.pure' ?_
32  intro q hq
33  have hqH := hKeepFrame q (by dsimp only at hh1; omega) (by dsimp only at hh2; omega)
34  change ((H.set! hm1.toInt.toNat n).set! hm2.toInt.toNat m)[q]! = d.heap[q]!
35  rw [hqH]
36  exact hframe q (by omega)
37
38/-- Parent creation sees the same tree and depth through heap-control-only
39updates. This is a record identity, not an assumed functional contract. -/
40theorem btParentState_heap_view (tk : TK) (d : DeflateState) (H : Array Int32) (hl hm n m node : Int32) :
41    tk.arr (btParentState tk { d with heap := H, heap_len := hl, heap_max := hm } n m node) =
42      tk.arr (btParentState tk d n m node) ∧
43    (btParentState tk { d with heap := H, heap_len := hl, heap_max := hm } n m node).depth =
44      (btParentState tk d n m node).depth := by
45  cases tk <;> exact ⟨rfl, rfl⟩
46
47/-- A singleton permutation of a root-replaced queue contains that root. -/
48theorem PermOn.singleton_root {A H : Nat → Int32} {node : Int32}
49    (hp : PermOn A (fun i => if i = 1 then node else H i) 1) : A 1 = node := by
50  obtain ⟨q, hq1, hq2, hq⟩ := hp.preimage 1 (by omega) (by omega)
51  have hq' : q = 1 := by omega
52  simpa only [hq', ite_true] using hq
53
54/-- A whole actual merge retains the old tail, gives exact parent-array
55effects, and retains exact queue counts. Both selected nodes came from the
56old queue. When this is the last merge, its new singleton root is the fresh
57parent. All called-function behavior is supplied by checked execution
58proofs. -/
59theorem ws_btMergeBody_forest {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (len : Nat) (node : Int32)
60    (hlen : d.heap_len.toInt = len) (h2 : 2 ≤ len) (hsz : len < d.heap.size)
61    (hbig : d.heap.size ≤ 573) (hmH : d.heap_max.toInt ≤ d.heap.size)
62    (hgap : (len : Int) < d.heap_max.toInt - 1)
63    (hp : NV (tk.arr d) d.depth node) (hinc : node.toInt < 2147483647)
64    (hbefore : ∀ i, 1 ≤ i → i ≤ len → 0 ≤ d.heap[i]!.toInt ∧ d.heap[i]!.toInt < node.toInt)
65    (hinj : ∀ i j, 1 ≤ i → i ≤ len → 1 ≤ j → j ≤ len → d.heap[i]! = d.heap[j]! → i = j)
66    (ho : HeapOK (sm (tk.arr d) d.depth) (fun i => d.heap[i]!) len 0) :
67    WS h0 id (btMergeBody (Sp id) (.ref (tk.ref id) 0) node) d (fun next e =>
68      next.toInt = node.toInt + 1 ∧ ∃ n m : Int32, n ≠ m ∧
69        (∃ q : Nat, 1 ≤ q ∧ q ≤ len ∧ n = d.heap[q]!) ∧
70        (∃ q : Nat, 1 ≤ q ∧ q ≤ len ∧ m = d.heap[q]!) ∧
71        e.heap_len.toInt = (len : Int) - 1 ∧ e.heap_max.toInt = d.heap_max.toInt - 2 ∧
72        e.heap[(d.heap_max.toInt - 1).toNat]! = n ∧ e.heap[(d.heap_max.toInt - 2).toNat]! = m ∧
73        (∀ q : Nat, d.heap_max.toInt ≤ (q : Int) → e.heap[q]! = d.heap[q]!) ∧
74        tk.arr e = tk.arr (btParentState tk d n m node) ∧ e.depth = (btParentState tk d n m node).depth ∧
75        (len = 2 → e.heap[1]! = node) ∧
76        ∀ F : Int32 → Nat, GB.rs (fun i => F e.heap[i + 1]!) (len - 1) + F n + F m =
77          GB.rs (fun i => F d.heap[i + 1]!) len + F node) := by
78  have hv : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr d) d.depth d.heap[i]! := by
79    intro i hi1 hi2
80    have hb := hbefore i hi1 hi2
81    exact ⟨hb.1, by have := hp.2.1; omega, by have := hp.2.2; omega⟩
82  unfold btMergeBody
83  refine WS.bind' (merge_ws_and
84    (ws_btMergeOpen tk d len hlen h2 hsz hbig hmH hgap hv hinj ho)
85    (ws_btMergeOpen_tail tk d len hlen h2 hsz hbig hmH hgap hv hinj ho))
86    fun pair e1 ⟨⟨hl, hm1, hm2, H, hn, hm, hnm, hhl, hh1, hh2, he1, hsH, hkeepn, hkeepm,
87      hnv, hmv, horder, hminn, hminm, horigin, hcomplete, hno, hHi, hcount⟩, htail⟩ => ?_
88  rcases pair with ⟨n, m⟩
89  dsimp only at hn hm hnm hnv hmv hkeepn hkeepm hno hcount ⊢
90  subst e1
91  let d1 := { d with heap := H, heap_len := hl, heap_max := hm2 }
92  have hT1 : tk.arr d1 = tk.arr d := by cases tk <;> rfl
93  have hD1 : d1.depth = d.depth := rfl
94  have hp1 : NV (tk.arr d1) d1.depth node := by rw [hT1, hD1]; exact hp
95  have hn1 : NV (tk.arr d1) d1.depth n := by rw [hT1, hD1]; exact hnv
96  have hm1v : NV (tk.arr d1) d1.depth m := by rw [hT1, hD1]; exact hmv
97  have hB : ∀ i, 1 ≤ i → i ≤ len - 1 → 0 ≤ H[i]!.toInt ∧ H[i]!.toInt < node.toInt := by
98    intro i hi1 hi2
99    obtain ⟨j, hj1, hj2, heq⟩ := horigin i hi1 hi2
100    rw [heq]
101    exact hbefore j (by omega) hj2
102  refine WS.bind' (ws_btMakeParent tk d1 n m node hn1 hm1v hp1) fun _ e2 he2 => ?_
103  subst e2
104  let d2 := btParentState tk d1 n m node
105  have hp2 : NV (tk.arr d2) d2.depth node := by
106    simpa only [d2, NV, btParentState_tree_size, btParentState_depth_size] using hp1
107  have hv2 : ∀ i, 1 ≤ i → i ≤ len - 1 → NV (tk.arr d2) d2.depth d2.heap[i]! := by
108    intro i hi1 hi2
109    have hb := hB i hi1 hi2
110    simp only [d2, btParentState_heap, d1, NV, btParentState_tree_size, btParentState_depth_size, hT1]
111    exact ⟨hb.1, by have := hp.2.1; omega, by have := hp.2.2; omega⟩
112  have ho2 : HeapOK (sm (tk.arr d2) d2.depth) (fun i => d2.heap[i]!) (len - 1) 1 := by
113    intro c hc2 hcl hcp
114    have hb := hB c (by omega) hcl
115    have hb' := hB (c / 2) (by omega) (by omega)
116    dsimp only [d2]
117    rw [btParentState_heap]
118    change sm (tk.arr (btParentState tk d1 n m node)) (btParentState tk d1 n m node).depth H[c / 2]! H[c]! = true
119    rw [btParentState_sm tk d1 n m node _ _ hn1 hm1v hp1 hb'.1 hb'.2 hb.1 hb.2, hT1, hD1]
120    exact horder c hc2 hcl (by omega)
121  refine WS.mono (ws_btMergeClose tk d2 (len - 1) node
122    (by simpa only [d2, btParentState_len] using hhl.trans (by omega)) (by omega)
123    (by simpa only [d2, btParentState_heap] using (show len - 1 < H.size by omega))
124    (by simpa only [d2, btParentState_heap] using (show H.size ≤ 573 by omega)) hp2 hinc hv2 ho2) ?_
125  intro next e3 ⟨hnext, H', he3, hsH', hframe, hperm, horder', hmin', hcount'⟩
126  subst e3
127  have hHeap2 : d2.heap = H := by simp only [d2, btParentState_heap]; rfl
128  have hroot : d2.heap[1]! = m := by rw [hHeap2]; exact hm.symm
129  have hmorigin : ∃ q : Nat, 1 ≤ q ∧ q ≤ len ∧ m = d.heap[q]! := by
130    obtain ⟨q, hq1, hq2, hq⟩ := horigin 1 (by omega) (by omega)
131    exact ⟨q, by omega, hq2, hm.trans hq⟩
132  have hview := btParentState_heap_view tk d H hl hm2 n m node
133  refine ⟨hnext, n, m, hnm, ⟨1, by omega, by omega, hn⟩, hmorigin,
134    by simpa only [d2, btParentState_len] using hhl, by simpa only [d2, btParentState_max] using hh2,
135    ?_, ?_, ?_, ?_, hview.2, ?_, ?_⟩
136  · change H'[(d.heap_max.toInt - 1).toNat]! = n
137    rw [← hh1, hframe _ (by omega), hHeap2]
138    exact hkeepn
139  · change H'[(d.heap_max.toInt - 2).toNat]! = m
140    rw [← hh2, hframe _ (by omega), hHeap2]
141    exact hkeepm
142  · intro q hq
143    change H'[q]! = d.heap[q]!
144    rw [hframe q (by omega), hHeap2]
145    exact htail q hq
146  · rw [tk_arr_heap]
147    exact hview.1
148  · intro hlen2
149    have hp' : PermOn (fun i => H'[i]!) (fun i => if i = 1 then node else d2.heap[i]!) 1 := by
150      simpa only [hlen2] using hperm
151    exact hp'.singleton_root
152  · intro F
153    have hc := hcount F
154    have hc' := hcount' F
155    rw [hroot, hHeap2] at hc'
156    change GB.rs (fun i => F H'[i + 1]!) (len - 1) + F n + F m = _
157    omega
158
159
160/-- A forest consists of the active queue and the descending retained tail.
161Its observations are exactly the original leaves plus every parent created
162so far. Parent links and placement describe the actual source layout. -/
163structure BTForest (tk : TK) (N K j : Nat) (mc : Int32) (d0 : DeflateState)
164    (node : Int32) (d : DeflateState) : Prop where
165  initial : BTLeafInv tk N mc d0
166  initial_len : d0.heap_len.toInt = K
167  queue : BTMergeQueue tk N K j node d
168  observations : ∀ F : Nat → Nat,
169    GB.poolSum (Hn d) (K - j) (2 * j) F =
170      GB.rs (fun i => F (Hn d0 (i + 1))) K + GB.rs (fun i => F (N + i)) j
171  tail_valid : ∀ q : Nat, 573 - 2 * j ≤ q → q < 573 →
172    0 ≤ d.heap[q]!.toInt ∧ d.heap[q]!.toInt < node.toInt
173  parent : ∀ q : Nat, 573 - 2 * j ≤ q → q < 573 →
174    (tk.arr d)[Hn d q]!.dl = UInt16.ofNat (GB.dadP N q)
175  placement : ∀ q : Nat, 573 - 2 * j ≤ q → q < 573 → N ≤ Hn d q →
176    q < 571 - 2 * (Hn d q - N)
177  leaf_freq : ∀ v < N, (tk.arr d)[v]!.fc = (tk.arr d0)[v]!.fc
178  unused : ∀ v < N, btFreq tk d0 v = 0 → (tk.arr d)[v]!.dl = 0
179  leaf_depth : ∀ v < N, btFreq tk d0 v ≠ 0 → d.depth[v]! = 0
180  last_root : j + 1 = K → d.heap[1]!.toInt = (N + j - 1 : Nat)
181
182/-- The actual prepared leaves establish the complete initial forest.
183The tail is empty at this stage, so its link and placement facts are derived
184without assumptions about old heap contents. -/
185theorem BTForest.of_leaf {tk : TK} {d : DeflateState} {N : Nat} {mc node : Int32}
186    (hi : BTLeafInv tk N mc d) (h2 : 2 ≤ d.heap_len.toInt) (hm : d.heap_max = HEAP_SIZE)
187    (hn : node.toInt = N)
188    (hT : N + d.heap_len.toInt.toNat - 1 ≤ (tk.arr d).size)
189    (hD : N + d.heap_len.toInt.toNat - 1 ≤ d.depth.size)
190    (ho : HeapOK (sm (tk.arr d) d.depth) (fun i => d.heap[i]!) d.heap_len.toInt.toNat 0) :
191    BTForest tk N d.heap_len.toInt.toNat 0 mc d node d := by
192  refine ⟨hi, by omega, BTMergeQueue.of_leaf hi h2 hm hn hT hD ho, ?_, ?_, ?_, ?_,
193    by intros; rfl, hi.unusedLength, hi.usedDepth, ?_⟩
194  · intro F
195    simp only [Nat.sub_zero, Nat.mul_zero, GB.poolSum, GB.rs_zero, Nat.add_zero]
196  · intro q hq hq'; omega
197  · intro q hq hq'; omega
198  · intro q hq hq'; omega
199  · intro heq; omega
200
201/-- Initial queue indices are distinct natural-valued leaf nodes below N. -/
202theorem BTForest.initial_nodes {tk : TK} {d0 d : DeflateState} {N K j : Nat} {mc node : Int32}
203    (hi : BTForest tk N K j mc d0 node d) :
204    (∀ i < K, Hn d0 (i + 1) < N) ∧
205    (∀ i i', i < K → i' < K → Hn d0 (i + 1) = Hn d0 (i' + 1) → i = i') := by
206  have hlen := hi.initial_len
207  constructor
208  · intro i hiK
209    have hv := hi.initial.valid (i + 1) (by omega) (by omega)
210    unfold Hn
211    omega
212  · intro i i' hiK hiK' heq
213    have hv := hi.initial.valid (i + 1) (by omega) (by omega)
214    have hv' := hi.initial.valid (i' + 1) (by omega) (by omega)
215    have he : d0.heap[i + 1]! = d0.heap[i' + 1]! := Int32.toInt_inj.mp (by unfold Hn at heq; omega)
216    have := hi.initial.injective (i + 1) (i' + 1) (by omega) (by omega) (by omega) (by omega) he
217    omega
218
219/-- Exact observations establish uniqueness across the queue and tail,
220including between those two regions. -/
221theorem BTForest.injective {tk : TK} {d0 d : DeflateState} {N K j : Nat} {mc node : Int32}
222    (hi : BTForest tk N K j mc d0 node d) :
223    ∀ q q', ((1 ≤ q ∧ q ≤ K - j) ∨ (573 - 2 * j ≤ q ∧ q < 573)) →
224      ((1 ≤ q' ∧ q' ≤ K - j) ∨ (573 - 2 * j ≤ q' ∧ q' < 573)) → Hn d q = Hn d q' → q = q' := by
225  have hinit := hi.initial_nodes
226  have hseq := GB.pool_unique (Hn d) (Hn d0) (K - j) (2 * j) K N j hinit.1 hinit.2 hi.observations
227  have hbound : K - j + 2 * j = K + j := by have := hi.queue.stage; omega
228  rw [hbound] at hseq
229  exact GB.pool_heap_injective (Hn d) K j (by have := hi.queue.kN; have := hi.queue.n286; omega)
230    hi.queue.stage hseq
231
232/-- Every active leaf came from the prepared nonzero-frequency leaf set. -/
233theorem BTForest.leaf_used {tk : TK} {d0 d : DeflateState} {N K j : Nat} {mc node : Int32}
234    (hi : BTForest tk N K j mc d0 node d) (q : Nat)
235    (hq : (1 ≤ q ∧ q ≤ K - j) ∨ (573 - 2 * j ≤ q ∧ q < 573)) (hN : Hn d q < N) :
236    btFreq tk d0 (Hn d q) ≠ 0 := by
237  have hK : K ≤ 286 := by have := hi.queue.kN; have := hi.queue.n286; omega
238  obtain ⟨i, hiB, hei⟩ := GB.poolAt_preimage (Hn d) K j q hK hi.queue.stage hq
239  have hiB' : i < K - j + 2 * j := by have := hi.queue.stage; omega
240  rcases GB.pool_origin (Hn d) (Hn d0) (K - j) (2 * j) K N j hi.observations i hiB' with
241    ⟨a, ha, he⟩ | he
242  · have hv := hi.initial.valid (a + 1) (by omega) (by have := hi.initial_len; omega)
243    rw [hei] at he
244    change (d0.heap[a + 1]!).toInt.toNat = Hn d q at he
245    rw [he] at hv
246    exact hv.2.2
247  · rw [hei] at he
248    omega
249
250/-- All retained old tail nodes are distinct from a selected old queue node. -/
251theorem BTForest.queue_not_tail {tk : TK} {d0 d : DeflateState} {N K j : Nat} {mc node : Int32}
252    (hi : BTForest tk N K j mc d0 node d) (p q : Nat)
253    (hp1 : 1 ≤ p) (hp2 : p ≤ K - j) (hq1 : 573 - 2 * j ≤ q) (hq2 : q < 573) :
254    Hn d q ≠ Hn d p := by
255  intro heq
256  have he := hi.injective q p (Or.inr ⟨hq1, hq2⟩) (Or.inl ⟨hp1, hp2⟩) heq
257  have := hi.queue.stage
258  have := hi.queue.kN
259  have := hi.queue.n286
260  omega
261
262
263/-- The actual merge preserves the full queue/tail forest. Old parent links
264and heap-tail entries are framed; the two new children point to the numeric
265fresh parent. Leaf frequencies, unused lengths and initialized leaf depths
266are preserved. The initial leaf representation is carried from the actual
267prefix, not supplied as a called-function contract. -/
268theorem ws_btMergeBody_forest_inv {h0 : Heap} {id : Nat} {tk : TK} {d0 d : DeflateState}
269    {N K j : Nat} {mc node : Int32} (hi : BTForest tk N K j mc d0 node d) (hmore : j + 1 < K) :
270    WS h0 id (btMergeBody (Sp id) (.ref (tk.ref id) 0) node) d
271      (fun next e => BTForest tk N K (j + 1) mc d0 next e) := by
272  have hK : K ≤ 286 := by have := hi.queue.kN; have := hi.queue.n286; omega
273  have hj := hi.queue.stage
274  have hcounter := hi.queue.counter
275  have hlen := hi.queue.len
276  have hmax := hi.queue.max
277  have hsize := hi.queue.heap
278  have hTsize := hi.queue.tree
279  have hDsize := hi.queue.depth
280  have hN3 := hi.queue.n3
281  have hNb := hi.queue.n286
282  have hKN := hi.queue.kN
283  have hnode : NV (tk.arr d) d.depth node := ⟨by omega, by omega, by omega⟩
284  refine WS.mono (merge_ws_and (ws_btMergeBody_queue hi.queue hmore)
285    (ws_btMergeBody_forest tk d (K - j) node hlen (by omega) (by omega) (by omega)
286      (by omega) (by omega) hnode (by omega)
287      (fun i hi1 hi2 => hi.queue.valid i hi1 (by omega))
288      (fun i i' hi1 hi2 hi'1 hi'2 => hi.queue.injective i i' hi1 (by omega) hi'1 (by omega)) hi.queue.order)) ?_
289  intro next e ⟨hq, hnext, n, m, hnm, ⟨pn, hpn1, hpn2, hpn⟩, ⟨pm, hpm1, hpm2, hpm⟩,
290    hlen', hmax', hkeepn, hkeepm, htail, htree, hdepth, hroot, hcount⟩
291  have hnv := hi.queue.valid pn hpn1 (by omega)
292  have hmv := hi.queue.valid pm hpm1 (by omega)
293  rw [← hpn] at hnv
294  rw [← hpm] at hmv
295  have hnV : NV (tk.arr d) d.depth n := ⟨hnv.1, by omega, by omega⟩
296  have hmV : NV (tk.arr d) d.depth m := ⟨hmv.1, by omega, by omega⟩
297  have hnodeN : node.toInt.toNat = N + j := by omega
298  have hpnN : Hn d pn = n.toInt.toNat := congrArg (fun x : Int32 => x.toInt.toNat) hpn.symm
299  have hpmN : Hn d pm = m.toInt.toNat := congrArg (fun x : Int32 => x.toInt.toNat) hpm.symm
300  have hboundary : d.heap_max.toInt = (573 - 2 * j : Nat) := by omega
301  have hnidx : (d.heap_max.toInt - 1).toNat = 572 - 2 * j := by omega
302  have hmidx : (d.heap_max.toInt - 2).toNat = 571 - 2 * j := by omega
303  rw [hnidx] at hkeepn
304  rw [hmidx] at hkeepm
305  have hkeepnN : Hn e (572 - 2 * j) = n.toInt.toNat := congrArg (fun x : Int32 => x.toInt.toNat) hkeepn
306  have hkeepmN : Hn e (571 - 2 * j) = m.toInt.toNat := congrArg (fun x : Int32 => x.toInt.toNat) hkeepm
307  have htailN : ∀ q : Nat, 573 - 2 * j ≤ q → Hn e q = Hn d q := by
308    intro q hq
309    exact congrArg (fun x : Int32 => x.toInt.toNat) (htail q (by omega))
310  have hnotn : ∀ q : Nat, 573 - 2 * j ≤ q → q < 573 → Hn d q ≠ n.toInt.toNat := by
311    intro q hq1 hq2
312    rw [← hpnN]
313    exact hi.queue_not_tail pn q hpn1 hpn2 hq1 hq2
314  have hnotm : ∀ q : Nat, 573 - 2 * j ≤ q → q < 573 → Hn d q ≠ m.toInt.toNat := by
315    intro q hq1 hq2
316    rw [← hpmN]
317    exact hi.queue_not_tail pm q hpm1 hpm2 hq1 hq2
318  have hcast : i2us node = UInt16.ofNat (N + j) := by
319    rw [i2us_eq node (by omega) (by omega), hnodeN]
320  have hsplit : ∀ q : Nat, 573 - 2 * (j + 1) ≤ q → q < 573 →
321      q = 572 - 2 * j ∨ q = 571 - 2 * j ∨ 573 - 2 * j ≤ q := by intros; omega
322  refine ⟨hi.initial, hi.initial_len, hq, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
323  · intro F
324    have hs := GB.poolSum_step (Hn d) (Hn e) K j n.toInt.toNat m.toInt.toNat (N + j) hK hmore
325      hkeepnN hkeepmN (fun i hi => htailN (572 - i) (by omega)) (fun G => ?_) F
326    · rw [hs, hi.observations, GB.rs_succ]
327      omega
328    · have hc := hcount (fun x => G x.toInt.toNat)
329      simpa only [Hn, hnodeN] using hc
330  · intro q hq1 hq2
331    rcases hsplit q hq1 hq2 with he | he | hqold
332    · subst q; rw [hkeepn]; exact ⟨hnv.1, by omega⟩
333    · subst q; rw [hkeepm]; exact ⟨hmv.1, by omega⟩
334    · rw [htail q (by omega)]
335      have hv := hi.tail_valid q hqold hq2
336      exact ⟨hv.1, by omega⟩
337  · intro q hq1 hq2
338    rw [htree, btParentState_dad tk d n m node hnV hmV hnode]
339    rcases hsplit q hq1 hq2 with he | he | hqold
340    · subst q; rw [hkeepnN, ite_eq_left (Or.inl rfl), hcast]
341      congr 1
342      unfold GB.dadP
343      omega
344    · subst q; rw [hkeepmN, ite_eq_left (Or.inr rfl), hcast]
345      congr 1
346      unfold GB.dadP
347      omega
348    · rw [htailN q hqold, ite_eq_right (by intro he; rcases he with he | he; exact hnotn q hqold hq2 he; exact hnotm q hqold hq2 he)]
349      exact hi.parent q hqold hq2
350  · intro q hq1 hq2 hqN
351    rcases hsplit q hq1 hq2 with he | he | hqold
352    · subst q; rw [hkeepnN] at hqN ⊢; omega
353    · subst q; rw [hkeepmN] at hqN ⊢; omega
354    · rw [htailN q hqold] at hqN ⊢
355      exact hi.placement q hqold hq2 hqN
356  · intro v hv
357    rw [htree, btParentState_fc tk d n m node hnV hmV hnode, ite_eq_right (by omega)]
358    exact hi.leaf_freq v hv
359  · intro v hv hz
360    have hvn : v ≠ n.toInt.toNat := by
361      intro he
362      have hu := hi.leaf_used pn (Or.inl ⟨hpn1, hpn2⟩) (by rw [hpnN, ← he]; exact hv)
363      rw [hpnN, ← he] at hu
364      exact hu hz
365    have hvm : v ≠ m.toInt.toNat := by
366      intro he
367      have hu := hi.leaf_used pm (Or.inl ⟨hpm1, hpm2⟩) (by rw [hpmN, ← he]; exact hv)
368      rw [hpmN, ← he] at hu
369      exact hu hz
370    rw [htree, btParentState_dad tk d n m node hnV hmV hnode,
371      ite_eq_right (by intro he; rcases he with he | he; exact hvn he; exact hvm he)]
372    exact hi.unused v hv hz
373  · intro v hv hz
374    rw [hdepth, btParentState_depth tk d n m node hnode, ite_eq_right (by omega)]
375    exact hi.leaf_depth v hv hz
376  · intro hlast
377    have hlen2 : K - j = 2 := by omega
378    have hr := hroot hlen2
379    have hrI := congrArg Int32.toInt hr
380    omega
381
382
383/-- Exact footprint of merging: only the selected tree, heap, depth and
384the two heap controls can change. Every array retains its size. -/
385def BTForestFrame (tk : TK) (d0 d : DeflateState) : Prop :=
386  ∃ (T : Array CtData) (H : Array Int32) (D : Array UInt8) (hl hm : Int32),
387    d = { btScanState tk d0 T H D hl with heap_max := hm } ∧
388    T.size = (tk.arr d0).size ∧ H.size = d0.heap.size ∧ D.size = d0.depth.size
389
390theorem BTForestFrame.refl (tk : TK) (d : DeflateState) : BTForestFrame tk d d := by
391  refine ⟨tk.arr d, d.heap, d.depth, d.heap_len, d.heap_max, ?_, rfl, rfl, rfl⟩
392  cases tk <;> rfl
393
394theorem BTForestFrame.trans {tk : TK} {a b c : DeflateState}
395    (hab : BTForestFrame tk a b) (hbc : BTForestFrame tk b c) : BTForestFrame tk a c := by
396  obtain ⟨T, H, D, hl, hm, rfl, hT, hH, hD⟩ := hab
397  obtain ⟨T', H', D', hl', hm', rfl, hT', hH', hD'⟩ := hbc
398  refine ⟨T', H', D', hl', hm', ?_, ?_, hH'.trans hH, hD'.trans hD⟩
399  · cases tk <;> rfl
400  · cases tk <;> exact hT'.trans hT
401
402/-- Descriptor and bit-count metadata survive the exact merge footprint. -/
403theorem BTForestFrame.metadata {tk : TK} {a b : DeflateState} (hi : BTForestFrame tk a b) (dk : TK) :
404    dk.getDesc b = dk.getDesc a ∧ b.bl_count = a.bl_count := by
405  obtain ⟨T, H, D, hl, hm, rfl, rest⟩ := hi
406  cases tk <;> cases dk <;> exact ⟨rfl, rfl⟩
407
408/-- The actual full iteration has precisely the merging footprint. -/
409theorem ws_btMergeBody_frame {h0 : Heap} {id : Nat} {tk : TK} {d : DeflateState}
410    {N K j : Nat} {node : Int32} (hi : BTMergeQueue tk N K j node d) (hmore : j + 1 < K) :
411    WS h0 id (btMergeBody (Sp id) (.ref (tk.ref id) 0) node) d
412      (fun _ e => BTForestFrame tk d e) := by
413  have hN3 := hi.n3
414  have hNb := hi.n286
415  have hK2 := hi.k2
416  have hKN := hi.kN
417  have hj := hi.stage
418  have hn := hi.counter
419  have hl := hi.len
420  have hm := hi.max
421  have hH := hi.heap
422  have hT := hi.tree
423  have hD := hi.depth
424  have hp : NV (tk.arr d) d.depth node := ⟨by omega, by omega, by omega⟩
425  refine WS.mono (ws_btMergeBody tk d (K - j) node hl (by omega) (by omega)
426    (by omega) (by omega) (by omega) hp (by omega)
427    (fun i hi1 hi2 => hi.valid i hi1 (by omega))
428    (fun i i' hi1 hi2 hi'1 hi'2 => hi.injective i i' hi1 (by omega) hi'1 (by omega)) hi.order) ?_
429  intro next e ⟨hnext, n, m, hlen, hm1, hm2, H, H', hn', hm', hnm, hlen', hm1', hm2', he,
430    hsize, htailn, htailm, horder, hvalid, hinj, hcount⟩
431  subst e
432  let mid := btParentState tk { d with heap := H, heap_len := hlen, heap_max := hm2 } n m node
433  refine ⟨tk.arr mid, H', mid.depth, hlen, hm2, ?_, ?_, hsize, ?_⟩
434  · cases tk <;> rfl
435  · dsimp only [mid]
436    rw [btParentState_tree_size]
437    cases tk <;> rfl
438  · dsimp only [mid]
439    rw [btParentState_depth_size]
440
441/-- The full actual merge loop preserves the forest layout and exact frame.
442The singleton last root and every earlier child link follow from the
443iteration proof; none is supplied as a callee contract premise. -/
444theorem ws_btMergeLoop_forest {h0 : Heap} {id : Nat} {tk : TK} {d : DeflateState}
445    {N K : Nat} {mc node : Int32} (hi : BTForest tk N K 0 mc d node d) :
446    WS h0 id (btMergeLoop (Sp id) (.ref (tk.ref id) 0) node) d (fun next e =>
447      BTForest tk N K (K - 1) mc d next e ∧ BTForestFrame tk d e ∧ e.heap_len.toInt = 1) := by
448  let Inv : Int32 → DeflateState → Prop := fun node e =>
449    ∃ j : Nat, BTForest tk N K j mc d node e ∧ BTForestFrame tk d e ∧ j + 1 < K
450  let Q : Int32 → DeflateState → Prop := fun node e =>
451    BTForest tk N K (K - 1) mc d node e ∧ BTForestFrame tk d e ∧ e.heap_len.toInt = 1
452  unfold btMergeLoop
453  refine WS.cdoWhile2 Inv (fun _ e => e.heap_len.toInt.toNat) Q ?_
454    ⟨0, hi, BTForestFrame.refl tk d, by have := hi.queue.k2; omega⟩
455    (by have := hi.queue.len; have := hi.queue.kN; have := hi.queue.n286; dsimp only [fuel]; omega)
456  intro current e ⟨j, hj, hfr, hmore⟩
457  refine WS.mono (merge_ws_and (ws_btMergeBody_forest_inv hj hmore) (ws_btMergeBody_frame hj.queue hmore)) ?_
458  intro next e' ⟨hj', hfr'⟩
459  have hframe := hfr.trans hfr'
460  refine WS.bind' ws_rd fun got e'' ⟨hgot, he''⟩ => ?_
461  subst e''; subst got
462  have hlen := hj'.queue.len
463  have hstage := hj'.queue.stage
464  have hK := hj'.queue.k2
465  by_cases hcontinue : e'.heap_len.toInt ≥ 2
466  · have hjnext : j + 1 + 1 < K := by omega
467    refine WS.pure' (Or.inr ⟨by simp only [hcontinue, decide_true], ⟨j + 1, hj', hframe, hjnext⟩, ?_⟩)
468    have hlen0 := hj.queue.len
469    omega
470  · have hjend : j + 1 = K - 1 := by omega
471    refine WS.pure' (Or.inl ⟨by simp only [hcontinue, decide_false], ?_⟩)
472    change Q next e'
473    rw [hjend] at hj'
474    exact ⟨hj', hframe, by omega⟩
475
476
477/-- The exact prepared maximum bounds every original leaf, and is a valid
478nonnegative symbol. Nonemptiness comes from the actual two-leaf repair. -/
479theorem BTForest.max_leaf {tk : TK} {d0 d : DeflateState} {N K j : Nat} {mc node : Int32}
480    (hi : BTForest tk N K j mc d0 node d) :
481    0 ≤ mc.toInt ∧ mc.toInt < N ∧ ∀ q : Nat, 1 ≤ q → q ≤ K → Hn d0 q ≤ mc.toInt.toNat := by
482  have hlen := hi.initial_len
483  have hK2 := hi.queue.k2
484  have hmc := hi.initial.maxCode
485  have hv := hi.initial.valid 1 (by omega) (by omega)
486  have hvN : (d0.heap[1]!).toInt.toNat < N := by omega
487  rcases Math.scanMax_spec (btFreq tk d0) N with ⟨hmax, hz⟩ | ⟨v, hmax, hvN', hfreq, hz⟩
488  · exact False.elim (hv.2.2 (hz _ hvN))
489  · have hmc' : mc.toInt = v := hmc.trans hmax
490    refine ⟨by omega, by omega, ?_⟩
491    intro q hq1 hq2
492    have hvq := hi.initial.valid q hq1 (by omega)
493    have hvqN : Hn d0 q < N := by unfold Hn; omega
494    have hvbound : Hn d0 q ≤ v := by
495      by_cases he : Hn d0 q ≤ v
496      · exact he
497      · have hzq := hz (Hn d0 q) (by omega) hvqN
498        exact False.elim (hvq.2.2 hzq)
499    omega
500
501/-- Pool membership has the leaf/internal-node split required by the tree
502layout specification. It is derived from exact observations. -/
503theorem BTForest.kind {tk : TK} {d0 d : DeflateState} {N K j : Nat} {mc node : Int32}
504    (hi : BTForest tk N K j mc d0 node d) (q : Nat)
505    (hq : (1 ≤ q ∧ q ≤ K - j) ∨ (573 - 2 * j ≤ q ∧ q < 573)) :
506    Hn d q ≤ mc.toInt.toNat ∨ (N ≤ Hn d q ∧ Hn d q < N + j) := by
507  have hK : K ≤ 286 := by have := hi.queue.kN; have := hi.queue.n286; omega
508  obtain ⟨i, hiB, hei⟩ := GB.poolAt_preimage (Hn d) K j q hK hi.queue.stage hq
509  have hiB' : i < K - j + 2 * j := by have := hi.queue.stage; omega
510  rcases GB.pool_origin (Hn d) (Hn d0) (K - j) (2 * j) K N j hi.observations i hiB' with
511    ⟨a, ha, he⟩ | he
512  · have hv := hi.max_leaf.2.2 (a + 1) (by omega) (by omega)
513    rw [hei] at he
514    exact Or.inl (he ▸ hv)
515  · rw [hei] at he
516    exact Or.inr he
517
518/-- Every created internal node has a represented position below its own
519children. Queue positions satisfy this bound by the queue/tail geometry;
520retained positions satisfy the preserved placement property. -/
521theorem BTForest.internal_position {tk : TK} {d0 d : DeflateState} {N K j : Nat} {mc node : Int32}
522    (hi : BTForest tk N K j mc d0 node d) (a : Nat) (ha : a < j) :
523    ∃ q : Nat, ((1 ≤ q ∧ q ≤ K - j) ∨ (573 - 2 * j ≤ q ∧ q < 573)) ∧
524      q < 571 - 2 * a ∧ Hn d q = N + a := by
525  have hK : K ≤ 286 := by have := hi.queue.kN; have := hi.queue.n286; omega
526  have hj := hi.queue.stage
527  obtain ⟨i, hiB, hei⟩ := GB.pool_internal (Hn d) (Hn d0) (K - j) (2 * j) K N j hi.observations a ha
528  have hiB' : i < K + j := by omega
529  obtain ⟨q, hq, hval⟩ := GB.poolAt_position (Hn d) K j i hK hj hiB'
530  have hqval : Hn d q = N + a := hval.symm.trans hei
531  refine ⟨q, hq, ?_, hqval⟩
532  rcases hq with hq | hq
533  · omega
534  · have hp := hi.placement q hq.1 hq.2 (by omega)
535    rw [hqval] at hp
536    simpa only [Nat.add_sub_cancel_left] using hp
537
538/-- Every initially used leaf has a represented queue or retained-tail
539position after merging. -/
540theorem BTForest.used_position {tk : TK} {d0 d : DeflateState} {N K j : Nat} {mc node : Int32}
541    (hi : BTForest tk N K j mc d0 node d) (v : Nat) (hv : v < N) (hf : btFreq tk d0 v ≠ 0) :
542    ∃ q : Nat, ((1 ≤ q ∧ q ≤ K - j) ∨ (573 - 2 * j ≤ q ∧ q < 573)) ∧ Hn d q = v := by
543  have hK : K ≤ 286 := by have := hi.queue.kN; have := hi.queue.n286; omega
544  have hj := hi.queue.stage
545  obtain ⟨q0, hq01, hq02, hval0⟩ := hi.initial.complete v hv hf
546  have hq0K : q0 ≤ K := by have := hi.initial_len; omega
547  have hval0N : Hn d0 q0 = v := by unfold Hn; omega
548  obtain ⟨i, hiB, hei⟩ := GB.pool_leaf (Hn d) (Hn d0) (K - j) (2 * j) K N j hi.observations (q0 - 1) (by omega)
549  rw [show q0 - 1 + 1 = q0 by omega, hval0N] at hei
550  have hiB' : i < K + j := by omega
551  obtain ⟨q, hq, hval⟩ := GB.poolAt_position (Hn d) K j i hK hj hiB'
552  exact ⟨q, hq, hval.symm.trans hei⟩
553
554
555/-- The tree layout established by the actual completed heap prefix. The
556root and all children occur exactly once in the retained interval. These
557are data results used to build the bit-length generator's context. -/
558structure BTBuilt (tk : TK) (N K : Nat) (mc : Int32) (d0 d : DeflateState) : Prop where
559  k2 : 2 ≤ K
560  kN : K ≤ N
561  n286 : N ≤ 286
562  max_nonneg : 0 ≤ mc.toInt
563  heap : d.heap.size = 573
564  heap_max : d.heap_max.toInt = (574 - 2 * K : Nat)
565  heap_len : d.heap_len.toInt = 1
566  shape : GB.PShape (Hn d) (574 - 2 * K) (K - 1) N mc.toInt.toNat
567  nonneg : ∀ q : Nat, 574 - 2 * K ≤ q → q < 573 → 0 ≤ d.heap[q]!.toInt
568  capacity : N + K - 1 ≤ (tk.arr d).size
569  parent : ∀ q : Nat, 574 - 2 * K < q → q < 573 →
570    (tk.arr d)[Hn d q]!.dl = UInt16.ofNat (GB.dadP N q)
571  unused : ∀ v ≤ mc.toInt.toNat, (∀ q, 574 - 2 * K ≤ q → q < 573 → Hn d q ≠ v) → (tk.arr d)[v]!.dl = 0
572  leaf_freq : ∀ v < N, (tk.arr d)[v]!.fc = (tk.arr d0)[v]!.fc
573  frame : BTForestFrame tk d0 d
574
575/-- The actual root store converts the complete forest into the precise
576retained tree layout. Its shape, parent links and inactive-symbol lengths
577are derived from merging, not assumed as a bit-length callee contract. -/
578theorem ws_btSaveRoot_forest {h0 : Heap} {id : Nat} {tk : TK} {d0 d : DeflateState}
579    {N K : Nat} {mc node : Int32} (hi : BTForest tk N K (K - 1) mc d0 node d)
580    (hfr : BTForestFrame tk d0 d) :
581    WS h0 id (btSaveRoot (Sp id)) d (fun _ e => BTBuilt tk N K mc d0 e) := by
582  have hK2 := hi.queue.k2
583  have hKN := hi.queue.kN
584  have hNb := hi.queue.n286
585  have hN3 := hi.queue.n3
586  have hj := hi.queue.stage
587  have hsize := hi.queue.heap
588  have hlen := hi.queue.len
589  have hmax := hi.queue.max
590  have hmBounds := hi.queue.tail_bounds
591  have hmc := hi.max_leaf
592  let b := 574 - 2 * K
593  have hb2 : 2 ≤ b := by dsimp only [b]; omega
594  have hb573 : b < 573 := by dsimp only [b]; omega
595  have hbmax : d.heap_max.toInt = (b + 1 : Nat) := by dsimp only [b]; omega
596  have hbtail : 573 - 2 * (K - 1) = b + 1 := by dsimp only [b]; omega
597  have hlast := hi.last_root (by omega)
598  refine WS.mono (ws_btSaveRoot d (by omega) (by omega) (by omega) (by omega)) ?_
599  intro _ e ⟨hm, hhm, he, hsz, hroot, hframe⟩
600  have hhmB : hm.toInt = b := by omega
601  have hhmBN : hm.toInt.toNat = b := by omega
602  have hHeap : ∀ q : Nat, e.heap[q]! = if q = b then d.heap[1]! else d.heap[q]! := by
603    intro q
604    rw [he]
605    change (d.heap.set! hm.toInt.toNat d.heap[1]!)[q]! = _
606    rw [hhmBN, getD_set _ _ _ _ (by omega)]
607  have hHN : ∀ q : Nat, Hn e q = if q = b then Hn d 1 else Hn d q := by
608    intro q
609    unfold Hn
610    rw [hHeap q]
611    split <;> rfl
612  have hTree : tk.arr e = tk.arr d := by rw [he]; cases tk <;> rfl
613  have hLen : e.heap_len.toInt = 1 := by rw [he]; dsimp only; omega
614  have hMax : e.heap_max.toInt = b := by rw [he]; exact hhmB
615  have hFrame : BTForestFrame tk d e := by
616    refine ⟨tk.arr d, e.heap, d.depth, d.heap_len, hm, ?_, rfl, hsz, rfl⟩
617    rw [he]
618    cases tk <;> rfl
619  let P : Nat → Nat := fun q => if q = b then 1 else q
620  have hP : ∀ q : Nat, b ≤ q → q < 573 →
621      (1 ≤ P q ∧ P q ≤ K - (K - 1)) ∨ (573 - 2 * (K - 1) ≤ P q ∧ P q < 573) := by
622    intro q hq1 hq2
623    dsimp only [P]
624    split
625    · exact Or.inl ⟨by omega, by omega⟩
626    · exact Or.inr ⟨by omega, hq2⟩
627  have hVal : ∀ q : Nat, Hn e q = Hn d (P q) := by
628    intro q
629    rw [hHN]
630    dsimp only [P]
631    split <;> rfl
632  have hPi : ∀ q q' : Nat, b ≤ q → q < 573 → b ≤ q' → q' < 573 → P q = P q' → q = q' := by
633    intro q q' hq1 hq2 hq'1 hq'2 heq
634    dsimp only [P] at heq
635    split at heq <;> split at heq <;> omega
636  have hLift : ∀ q : Nat,
637      ((1 ≤ q ∧ q ≤ K - (K - 1)) ∨ (573 - 2 * (K - 1) ≤ q ∧ q < 573)) →
638      ∃ q' : Nat, b ≤ q' ∧ q' < 573 ∧ Hn e q' = Hn d q ∧ (q ≠ 1 → q' = q) := by
639    intro q hq
640    by_cases hq1 : q = 1
641    · refine ⟨b, by omega, hb573, ?_, ?_⟩
642      · rw [hHN, ite_eq_left rfl, hq1]
643      · intro hh; exact False.elim (hh hq1)
644    · have hqtail : b + 1 ≤ q ∧ q < 573 := by rcases hq with hq | hq <;> omega
645      refine ⟨q, by omega, hqtail.2, ?_, fun _ => rfl⟩
646      rw [hHN, ite_eq_right (by omega)]
647  have hshape : GB.PShape (Hn e) b (K - 1) N mc.toInt.toNat := by
648    refine ⟨by dsimp only [b]; omega, by omega, by omega, ?_, ?_, ?_, ?_⟩
649    · intro q q' hq1 hq2 hq'1 hq'2 heq
650      rw [hVal, hVal] at heq
651      exact hPi q q' hq1 hq2 hq'1 hq'2 (hi.injective _ _ (hP q hq1 hq2) (hP q' hq'1 hq'2) heq)
652    · intro q hq1 hq2
653      rw [hVal]
654      exact hi.kind _ (hP q hq1 hq2)
655    · rw [hHN, ite_eq_left rfl]
656      unfold Hn
657      omega
658    · intro a ha
659      obtain ⟨q, hq, hpos, hqval⟩ := hi.internal_position a ha
660      obtain ⟨q', hq'1, hq'2, hval, hsame⟩ := hLift q hq
661      refine ⟨q', hq'1, ?_, hval.trans hqval⟩
662      by_cases hq1 : q = 1
663      · have heq : q' = b := by
664          rcases hq with hq | hq
665          · have hpe := hP q' hq'1 hq'2
666            have hinj := hi.injective (P q') 1 hpe (Or.inl ⟨by omega, by omega⟩)
667              (by rw [← hVal, hval, hq1])
668            dsimp only [P] at hinj
669            split at hinj <;> omega
670          · omega
671        rw [heq]
672        dsimp only [b]
673        omega
674      · rw [hsame hq1]
675        exact hpos
676  refine ⟨hK2, hKN, hNb, hmc.1, hsz.trans hsize, hMax, hLen, hshape, ?_, ?_, ?_, ?_, ?_, hfr.trans hFrame⟩
677  · intro q hq1 hq2
678    rw [hHeap]
679    split
680    · exact (hi.queue.valid 1 (by omega) (by omega)).1
681    · exact (hi.tail_valid q (by omega) hq2).1
682  · rw [hTree]
683    exact hi.queue.tree
684  · intro q hq1 hq2
685    rw [hTree, hHN, ite_eq_right (by omega)]
686    exact hi.parent q (by omega) hq2
687  · intro v hv hnone
688    have hvN : v < N := by omega
689    have hz : btFreq tk d0 v = 0 := by
690      by_cases hz : btFreq tk d0 v = 0
691      · exact hz
692      · obtain ⟨q, hq, hqval⟩ := hi.used_position v hvN hz
693        obtain ⟨q', hq'1, hq'2, hval, hsame⟩ := hLift q hq
694        exact False.elim (hnone q' hq'1 hq'2 (hval.trans hqval))
695    rw [hTree]
696    exact hi.unused v hvN hz
697  · intro v hv
698    rw [hTree]
699    exact hi.leaf_freq v hv
700
701end Zlib.Trees.Proofs