trees.c.build.merge.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Math.DeflateHeapRemove
2import ZlibF.Proof.«trees.c.build.heapify»
3
4/-! # trees.c: the actual node-merging loop and its two selected nodes -/
5
6namespace Zlib.Trees.Proofs
7open C Zlib.Trees
8
9/-- Naming a conditional source fragment distributes its following
10continuation over the unchanged decision. -/
11theorem merge_ite_bind {α β : Type} (p : Prop) [Decidable p] (a b : M α) (f : α → M β) :
12    ((if p then a else b) >>= f) = (if p then a >>= f else b >>= f) := by
13  split <;> rfl
14
15/-- The actual root removal and next-root read, in source order. -/
16def btPick2 (s : DeflateStatePtr) (tree : CtDataPtr) : M (Int32 × Int32) := do
17  let n ← pqremove s tree
18  let m ← heapAt s 1
19  pure (n, m)
20
21/-- The two descending heap-tail stores, each with its own checked decrement
22and state write, exactly as in the two C statements. -/
23def btKeepChildren (s : DeflateStatePtr) (n m : Int32) : M Unit := do
24  let hm ← isub (← rd s).heap_max 1
25  md s fun d => { d with heap_max := hm }
26  heapSet s hm n
27  let hm ← isub (← rd s).heap_max 1
28  md s fun d => { d with heap_max := hm }
29  heapSet s hm m
30
31/-- The actual selection and two tail stores before creating the parent. -/
32def btMergeOpen (s : DeflateStatePtr) (tree : CtDataPtr) : M (Int32 × Int32) := do
33  let (n, m) ← btPick2 s tree
34  btKeepChildren s n m
35  pure (n, m)
36
37/-- The actual child comparison, selected-child reload and parent-depth store. -/
38def btSetDepth (s : DeflateStatePtr) (n m node : Int32) : M Unit := do
39  let dp ← pDepth s
40  let dn ← Ptr.index dp n.toInt
41  let dm ← Ptr.index dp m.toInt
42  let mx ← if dn ≥ dm then Ptr.index dp n.toInt else Ptr.index dp m.toInt
43  setAt dp node.toInt (mx + 1)
44
45/-- The actual child-frequency reads and parent-frequency store. -/
46def btSetFreq (tree : CtDataPtr) (n m node : Int32) : M Unit := do
47  let fn ← getFc tree n.toInt
48  let fm ← getFc tree m.toInt
49  setFc tree node.toInt (fn + fm)
50
51/-- The right-to-left stores of the chained parent assignment. -/
52def btSetParents (tree : CtDataPtr) (n m node : Int32) : M Unit := do
53  setDl tree m.toInt (i2us node)
54  setDl tree n.toInt (i2us node)
55
56/-- The actual parent frequency, depth, and two right-to-left `Dad` stores. -/
57def btMakeParent (s : DeflateStatePtr) (tree : CtDataPtr) (n m node : Int32) : M Unit := do
58  btSetFreq tree n m node
59  btSetDepth s n m node
60  btSetParents tree n m node
61
62/-- The actual root replacement, checked local increment and sift-down. -/
63def btMergeClose (s : DeflateStatePtr) (tree : CtDataPtr) (node : Int32) : M Int32 := do
64  heapSet s 1 node
65  let node' ← iadd node 1
66  pqdownheap s tree 1
67  pure node'
68
69/-- One actual merge iteration, with only its two-node selection named. -/
70def btMergeBody (s : DeflateStatePtr) (tree : CtDataPtr) (node : Int32) : M Int32 := do
71  -- pqremove(s, tree, n);  m = s->heap[SMALLEST];
72  let (n, m) ← btMergeOpen s tree
73  -- tree[node].Freq = tree[n].Freq + tree[m].Freq;
74  btMakeParent s tree n m node
75  -- s->heap[SMALLEST] = node++;
76  btMergeClose s tree node
77
78/-- The actual do-while guard is checked after each completed merge. -/
79def btMergeLoop (s : DeflateStatePtr) (tree : CtDataPtr) (node : Int32) : M Int32 :=
80  cdoWhile (btMergeBody s tree)
81    (fun node => do pure (decide ((← rd s).heap_len.toInt ≥ 2), node)) node
82
83/-- The actual final root read and predecremented tail store. -/
84def btSaveRoot (s : DeflateStatePtr) : M Unit := do
85  let top ← heapAt s 1
86  let hm ← isub (← rd s).heap_max 1
87  md s fun d => { d with heap_max := hm }
88  heapSet s hm top
89
90/-- The actual removal followed by the second-root read selects two distinct
91nodes. The first is minimal in the original queue; the second is minimal in
92the remaining queue. Deletion preserves all other entries and their exact
93counts, without a callee contract premise. -/
94theorem ws_btPick2 {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (len : Nat)
95    (hlen : d.heap_len.toInt = len) (h2 : 2 ≤ len) (hsz : len < d.heap.size)
96    (hbig : d.heap.size ≤ 573)
97    (hval : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr d) d.depth d.heap[i]!)
98    (hinj : ∀ i j, 1 ≤ i → i ≤ len → 1 ≤ j → j ≤ len → d.heap[i]! = d.heap[j]! → i = j)
99    (ho : HeapOK (sm (tk.arr d) d.depth) (fun i => d.heap[i]!) len 0) :
100    WS h0 id (btPick2 (Sp id) (.ref (tk.ref id) 0)) d (fun r e =>
101      ∃ (hl : Int32) (H : Array Int32), r.1 = d.heap[1]! ∧ r.2 = H[1]! ∧
102        hl.toInt = (len : Int) - 1 ∧ e = { d with heap := H, heap_len := hl } ∧
103        H.size = d.heap.size ∧
104        (∀ i, ¬ (1 ≤ i ∧ i ≤ len - 1) → H[i]! = d.heap[i]!) ∧
105        PermOn (fun i => H[i]!) (Hm (fun i => d.heap[i]!) len) (len - 1) ∧
106        HeapOK (sm (tk.arr d) d.depth) (fun i => H[i]!) (len - 1) 0 ∧
107        NV (tk.arr d) d.depth r.1 ∧ NV (tk.arr d) d.depth r.2 ∧ r.1 ≠ r.2 ∧
108        (∀ q, 1 ≤ q → q ≤ len → sm (tk.arr d) d.depth r.1 d.heap[q]! = true) ∧
109        (∀ q, 1 ≤ q → q ≤ len - 1 → sm (tk.arr d) d.depth r.2 H[q]! = true) ∧
110        (∀ q, 1 ≤ q → q ≤ len - 1 →
111          ∃ i : Nat, 2 ≤ i ∧ i ≤ len ∧ H[q]! = d.heap[i]!) ∧
112        (∀ i, 2 ≤ i → i ≤ len → ∃ q : Nat, 1 ≤ q ∧ q ≤ len - 1 ∧ H[q]! = d.heap[i]!) ∧
113        (∀ q, 1 ≤ q → q ≤ len - 1 → H[q]! ≠ r.1) ∧
114        (∀ q q', 1 ≤ q → q ≤ len - 1 → 1 ≤ q' → q' ≤ len - 1 → H[q]! = H[q']! → q = q') ∧
115        ∀ F : Int32 → Nat, GB.rs (fun q => F H[q + 1]!) (len - 1) + F r.1 =
116          GB.rs (fun q => F d.heap[q + 1]!) len) := by
117  unfold btPick2
118  refine WS.bind' (ws_pqremove tk d len hlen h2 hsz (by omega) hval ho)
119    fun n e1 ⟨hn, hl, H, hhl, he1, hsH, hframe, hp, horder⟩ => ?_
120  subst e1
121  refine WS.bind' (ws_heapAt 1 (by decide +kernel)
122    (by change (1 : Int) < H.size; omega)) fun m e1 ⟨hm, he1⟩ => ?_
123  subst e1
124  have hindex : (1 : Int32).toInt.toNat = 1 := rfl
125  change m = H[(1 : Int32).toInt.toNat]! at hm
126  rw [hindex] at hm
127  subst n; subst m
128  have hp' : PermOn (fun i => H[i]!) (Hm (fun i => d.heap[i]!) len) (len - 1) := hp
129  obtain ⟨hroot, hHinj⟩ := hp'.removed_injective h2 hinj
130  have hvH : ∀ q, 1 ≤ q → q ≤ len - 1 → NV (tk.arr d) d.depth H[q]! := by
131    intro q hq1 hq2
132    obtain ⟨i, hi1, hi2, hqi⟩ := hp'.removed_origin h2 q hq1 hq2
133    change H[q]! = d.heap[i]! at hqi
134    rw [hqi]
135    exact hval i (by omega) hi2
136  refine WS.pure' ⟨hl, H, rfl, rfl, hhl, rfl, hsH, hframe, hp', horder,
137    hval 1 (by omega) (by omega), ?_, ?_, ?_, ?_, ?_, ?_, hroot, hHinj, ?_⟩
138  · have hv := hvH 1 (by omega) (by omega)
139    exact hv
140  · have hr := hroot 1 (by omega) (by omega)
141    exact hr.symm
142  · exact ho.root_min (sm_ok (tk.arr d) d.depth)
143  · have hmin := horder.root_min (sm_ok (tk.arr d) d.depth)
144    exact hmin
145  · intro q hq1 hq2
146    exact hp'.removed_origin h2 q hq1 hq2
147  · intro i hi1 hi2
148    exact hp'.removed_preimage h2 i hi1 hi2
149  · intro F
150    exact hp'.removed_sum h2 F
151
152/-- The actual descending stores preserve both children in the correct
153order and leave every other heap cell untouched. Heap length and all fields
154outside the heap array and tail boundary are unchanged. -/
155theorem ws_btKeepChildren {h0 : Heap} {id : Nat} (d : DeflateState) (n m : Int32)
156    (hm2 : 2 ≤ d.heap_max.toInt) (hmH : d.heap_max.toInt ≤ d.heap.size) (hbig : d.heap.size ≤ 573) :
157    WS h0 id (btKeepChildren (Sp id) n m) d (fun _ e =>
158      ∃ hm1 hm2 : Int32, hm1.toInt = d.heap_max.toInt - 1 ∧ hm2.toInt = d.heap_max.toInt - 2 ∧
159        e = { d with heap_max := hm2, heap := (d.heap.set! hm1.toInt.toNat n).set! hm2.toInt.toNat m } ∧
160        e.heap.size = d.heap.size ∧ e.heap[hm1.toInt.toNat]! = n ∧ e.heap[hm2.toInt.toNat]! = m ∧
161        ∀ i, i ≠ hm1.toInt.toNat → i ≠ hm2.toInt.toNat → e.heap[i]! = d.heap[i]!) := by
162  have hi1 : (1 : Int32).toInt = 1 := rfl
163  unfold btKeepChildren
164  refine WS.bind' ws_rd fun dz e1 ⟨hdz, he1⟩ => ?_
165  subst e1; subst dz
166  refine WS.bind' (ws_isub d.heap_max 1 (by omega) (by omega)) fun hm1 e1 ⟨hh1, he1⟩ => ?_
167  subst e1
168  refine WS.bind' (ws_md _) fun _ e1 he1 => ?_
169  subst e1
170  unfold heapSet
171  simp only [M_bind_assoc]
172  refine WS.bind' ws_pHeap fun p e1 ⟨hp, he1⟩ => ?_
173  subst e1; subst p
174  refine WS.bind' (ws_setAt_heap hm1.toInt n (by omega) (by dsimp; omega)) fun _ e1 he1 => ?_
175  subst e1
176  refine WS.bind' ws_rd fun dz e1 ⟨hdz, he1⟩ => ?_
177  subst e1; subst dz
178  refine WS.bind' (ws_isub _ 1 (by dsimp; omega) (by dsimp; omega)) fun hm2 e1 ⟨hh2, he1⟩ => ?_
179  subst e1
180  refine WS.bind' (ws_md _) fun _ e1 he1 => ?_
181  subst e1
182  refine WS.bind' ws_pHeap fun p e1 ⟨hp, he1⟩ => ?_
183  subst e1; subst p
184  refine WS.mono (ws_setAt_heap hm2.toInt m (by dsimp at hh2; omega)
185    (by change hm2.toInt < ((d.heap.set! hm1.toInt.toNat n).size : Int); rw [size_set!]; dsimp at hh2; omega)) ?_
186  intro _ e1 he1
187  subst e1
188  have hh2 : hm2.toInt = d.heap_max.toInt - 2 := by dsimp at hh2; omega
189  have h1 : hm1.toInt.toNat < d.heap.size := by omega
190  have h2 : hm2.toInt.toNat < d.heap.size := by omega
191  have hne : hm1.toInt.toNat ≠ hm2.toInt.toNat := by omega
192  refine ⟨hm1, hm2, by omega, hh2, rfl, by simp only [size_set!], ?_, ?_, ?_⟩
193  · dsimp only
194    rw [getD_set _ hm2.toInt.toNat hm1.toInt.toNat m (by simpa only [size_set!] using h2), ite_eq_right hne,
195      getD_set _ hm1.toInt.toNat hm1.toInt.toNat n h1, ite_eq_left rfl]
196  · dsimp only
197    rw [getD_set _ hm2.toInt.toNat hm2.toInt.toNat m (by simpa only [size_set!] using h2), ite_eq_left rfl]
198  · intro i hi1 hi2
199    dsimp only
200    rw [getD_set _ hm2.toInt.toNat i m (by simpa only [size_set!] using h2), ite_eq_right hi2,
201      getD_set _ hm1.toInt.toNat i n h1, ite_eq_right hi1]
202
203/-- The complete opening of an actual merge keeps both selected nodes in
204the descending tail and preserves the remaining queue, its order, membership
205and counts. The queue/tail gap prevents overwriting any live queue entry. -/
206theorem ws_btMergeOpen {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (len : Nat)
207    (hlen : d.heap_len.toInt = len) (h2 : 2 ≤ len) (hsz : len < d.heap.size)
208    (hbig : d.heap.size ≤ 573) (hmH : d.heap_max.toInt ≤ d.heap.size)
209    (hgap : (len : Int) < d.heap_max.toInt - 1)
210    (hval : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr d) d.depth d.heap[i]!)
211    (hinj : ∀ i j, 1 ≤ i → i ≤ len → 1 ≤ j → j ≤ len → d.heap[i]! = d.heap[j]! → i = j)
212    (ho : HeapOK (sm (tk.arr d) d.depth) (fun i => d.heap[i]!) len 0) :
213    WS h0 id (btMergeOpen (Sp id) (.ref (tk.ref id) 0)) d (fun r e =>
214      ∃ (hl hm1 hm2 : Int32) (H : Array Int32),
215        r.1 = d.heap[1]! ∧ r.2 = H[1]! ∧ r.1 ≠ r.2 ∧
216        hl.toInt = (len : Int) - 1 ∧ hm1.toInt = d.heap_max.toInt - 1 ∧ hm2.toInt = d.heap_max.toInt - 2 ∧
217        e = { d with heap := H, heap_len := hl, heap_max := hm2 } ∧ H.size = d.heap.size ∧
218        H[hm1.toInt.toNat]! = r.1 ∧ H[hm2.toInt.toNat]! = r.2 ∧
219        NV (tk.arr d) d.depth r.1 ∧ NV (tk.arr d) d.depth r.2 ∧
220        HeapOK (sm (tk.arr d) d.depth) (fun i => H[i]!) (len - 1) 0 ∧
221        (∀ q, 1 ≤ q → q ≤ len → sm (tk.arr d) d.depth r.1 d.heap[q]! = true) ∧
222        (∀ q, 1 ≤ q → q ≤ len - 1 → sm (tk.arr d) d.depth r.2 H[q]! = true) ∧
223        (∀ q, 1 ≤ q → q ≤ len - 1 → ∃ i : Nat, 2 ≤ i ∧ i ≤ len ∧ H[q]! = d.heap[i]!) ∧
224        (∀ i, 2 ≤ i → i ≤ len → ∃ q : Nat, 1 ≤ q ∧ q ≤ len - 1 ∧ H[q]! = d.heap[i]!) ∧
225        (∀ q, 1 ≤ q → q ≤ len - 1 → H[q]! ≠ r.1) ∧
226        (∀ q q', 1 ≤ q → q ≤ len - 1 → 1 ≤ q' → q' ≤ len - 1 → H[q]! = H[q']! → q = q') ∧
227        ∀ F : Int32 → Nat, GB.rs (fun q => F H[q + 1]!) (len - 1) + F r.1 =
228          GB.rs (fun q => F d.heap[q + 1]!) len) := by
229  unfold btMergeOpen
230  refine WS.bind' (ws_btPick2 tk d len hlen h2 hsz hbig hval hinj ho)
231    fun r e1 ⟨hl, H, hn, hm, hhl, he1, hsH, hframe, hp, horder, hnv, hmv, hnm,
232      hminn, hminm, horigin, hcomplete, hno, hHinj, hcount⟩ => ?_
233  subst e1
234  rcases r with ⟨n, m⟩
235  dsimp only at hn hm hnv hmv hnm hminn hminm hno hcount ⊢
236  refine WS.bind' (ws_btKeepChildren { d with heap := H, heap_len := hl } n m
237    (by change 2 ≤ d.heap_max.toInt; omega) (by change d.heap_max.toInt ≤ (H.size : Int); omega)
238    (by change H.size ≤ 573; omega))
239    fun _ e2 ⟨hm1, hm2, hh1, hh2, he2, hsH', hnKeep, hmKeep, hKeepFrame⟩ => ?_
240  subst e2
241  let H' := (H.set! hm1.toInt.toNat n).set! hm2.toInt.toNat m
242  have hh1 : hm1.toInt = d.heap_max.toInt - 1 := hh1
243  have hh2 : hm2.toInt = d.heap_max.toInt - 2 := hh2
244  have hqueue : ∀ q, 1 ≤ q → q ≤ len - 1 → H'[q]! = H[q]! := by
245    intro q hq1 hq2
246    exact hKeepFrame q (by omega) (by omega)
247  have hroot : H'[1]! = m := (hqueue 1 (by omega) (by omega)).trans hm.symm
248  refine WS.pure' ⟨hl, hm1, hm2, H', hn, hroot.symm, hnm, hhl, hh1, hh2, rfl,
249    by dsimp only [H']; simp only [size_set!]; exact hsH,
250    hnKeep, hmKeep, hnv, hmv, ?_, hminn, ?_, ?_, ?_, ?_, ?_, ?_⟩
251  · intro c hc2 hcl hcp
252    dsimp only
253    rw [hqueue c (by omega) hcl, hqueue (c / 2) (by omega) (by omega)]
254    exact horder c hc2 hcl hcp
255  · intro q hq1 hq2
256    rw [hqueue q hq1 hq2]
257    exact hminm q hq1 hq2
258  · intro q hq1 hq2
259    obtain ⟨i, hi1, hi2, hqi⟩ := horigin q hq1 hq2
260    exact ⟨i, hi1, hi2, (hqueue q hq1 hq2).trans hqi⟩
261  · intro i hi1 hi2
262    obtain ⟨q, hq1, hq2, hqi⟩ := hcomplete i hi1 hi2
263    exact ⟨q, hq1, hq2, (hqueue q hq1 hq2).trans hqi⟩
264  · intro q hq1 hq2
265    rw [hqueue q hq1 hq2]
266    exact hno q hq1 hq2
267  · intro q q' hq1 hq2 hq'1 hq'2 heq
268    rw [hqueue q hq1 hq2, hqueue q' hq'1 hq'2] at heq
269    exact hHinj q q' hq1 hq2 hq'1 hq'2 heq
270  · intro F
271    rw [show GB.rs (fun q => F H'[q + 1]!) (len - 1) = GB.rs (fun q => F H[q + 1]!) (len - 1) by
272      apply GB.rs_congr
273      intro q hq
274      rw [hqueue (q + 1) (by omega) (by omega)]]
275    exact hcount F
276
277/-- The corrected source expression, including its third read, stores the
278selected child depth plus one modulo 256. Every other depth and state field
279is unchanged. No non-wrapping-depth assumption is required. -/
280theorem ws_btSetDepth {h0 : Heap} {id : Nat} (d : DeflateState) (n m node : Int32)
281    (hn0 : 0 ≤ n.toInt) (hnD : n.toInt < d.depth.size)
282    (hm0 : 0 ≤ m.toInt) (hmD : m.toInt < d.depth.size)
283    (hp0 : 0 ≤ node.toInt) (hpD : node.toInt < d.depth.size) :
284    WS h0 id (btSetDepth (Sp id) n m node) d (fun _ e =>
285      e = { d with
286        depth := d.depth.set! node.toInt.toNat
287          ((if d.depth[n.toInt.toNat]! ≥ d.depth[m.toInt.toNat]! then
288            d.depth[n.toInt.toNat]! else d.depth[m.toInt.toNat]!) + 1) }) := by
289  unfold btSetDepth
290  refine WS.bind' ws_pDepth fun p e1 ⟨hp, he1⟩ => ?_
291  subst e1; subst p
292  refine WS.bind' (ws_index_depth n.toInt hn0 hnD) fun dn e1 ⟨hdn, he1⟩ => ?_
293  subst e1; subst dn
294  refine WS.bind' (ws_index_depth m.toInt hm0 hmD) fun dm e1 ⟨hdm, he1⟩ => ?_
295  subst e1; subst dm
296  by_cases hc : d.depth[n.toInt.toNat]! ≥ d.depth[m.toInt.toNat]!
297  · simp only [hc, ite_true]
298    refine WS.bind' (ws_index_depth n.toInt hn0 hnD) fun mx e1 ⟨hmx, he1⟩ => ?_
299    subst e1; subst mx
300    exact ws_setAt_depth node.toInt _ hp0 hpD
301  · simp only [hc, ite_false]
302    refine WS.bind' (ws_index_depth m.toInt hm0 hmD) fun mx e1 ⟨hmx, he1⟩ => ?_
303    subst e1; subst mx
304    exact ws_setAt_depth node.toInt _ hp0 hpD
305
306/-- Exact parent-creation record, retaining source order even if the three
307indices alias. Parent-index casts and both byte/word arithmetic operations
308keep their unsigned wrapping behavior. -/
309def btParentState (tk : TK) (d : DeflateState) (n m node : Int32) : DeflateState :=
310  let T := tk.arr d
311  let T1 := T.set! node.toInt.toNat { T[node.toInt.toNat]! with fc := T[n.toInt.toNat]!.fc + T[m.toInt.toNat]!.fc }
312  let T2 := T1.set! m.toInt.toNat { T1[m.toInt.toNat]! with dl := i2us node }
313  let T3 := T2.set! n.toInt.toNat { T2[n.toInt.toNat]! with dl := i2us node }
314  { tk.setArr d T3 with
315    depth := d.depth.set! node.toInt.toNat
316      ((if d.depth[n.toInt.toNat]! ≥ d.depth[m.toInt.toNat]! then
317        d.depth[n.toInt.toNat]! else d.depth[m.toInt.toNat]!) + 1) }
318
319/-- Exact frequency store, including unsigned 16-bit addition wrap. -/
320theorem ws_btSetFreq {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (n m node : Int32)
321    (hn0 : 0 ≤ n.toInt) (hnT : n.toInt < (tk.arr d).size)
322    (hm0 : 0 ≤ m.toInt) (hmT : m.toInt < (tk.arr d).size)
323    (hp0 : 0 ≤ node.toInt) (hpT : node.toInt < (tk.arr d).size) :
324    WS h0 id (btSetFreq (.ref (tk.ref id) 0) n m node) d (fun _ e =>
325      e = tk.setArr d ((tk.arr d).set! node.toInt.toNat
326        { (tk.arr d)[node.toInt.toNat]! with fc := ((tk.arr d)[n.toInt.toNat]!).fc + ((tk.arr d)[m.toInt.toNat]!).fc })) := by
327  unfold btSetFreq
328  refine WS.bind' (ws_getFc tk n.toInt hn0 hnT) fun fn e1 ⟨hfn, he1⟩ => ?_
329  subst e1; subst fn
330  refine WS.bind' (ws_getFc tk m.toInt hm0 hmT) fun fm e1 ⟨hfm, he1⟩ => ?_
331  subst e1; subst fm
332  exact ws_setFc tk node.toInt _ hp0 hpT
333
334/-- Exact parent stores, including aliases between the two child indices. -/
335theorem ws_btSetParents {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (n m node : Int32)
336    (hn0 : 0 ≤ n.toInt) (hnT : n.toInt < (tk.arr d).size)
337    (hm0 : 0 ≤ m.toInt) (hmT : m.toInt < (tk.arr d).size) :
338    WS h0 id (btSetParents (.ref (tk.ref id) 0) n m node) d (fun _ e =>
339      let T1 := (tk.arr d).set! m.toInt.toNat { (tk.arr d)[m.toInt.toNat]! with dl := i2us node }
340      e = tk.setArr d (T1.set! n.toInt.toNat { T1[n.toInt.toNat]! with dl := i2us node })) := by
341  unfold btSetParents
342  refine WS.bind' (ws_setDl tk m.toInt (i2us node) hm0 hmT) fun _ e1 he1 => ?_
343  subst e1
344  refine WS.mono (ws_setDl tk n.toInt (i2us node) hn0
345    (by rw [tk_arr_setArr, size_set!]; exact hnT)) ?_
346  intro _ e1 he1
347  subst e1
348  simp only [tk_arr_setArr]
349  cases tk <;> rfl
350
351set_option maxRecDepth 4096 in
352/-- The entire actual parent-creation fragment has these exact record effects.
353No acyclicity, freshness, distinctness, non-wrapping weight, or callee contract
354is assumed. Those structural facts are obligations of the merge invariant. -/
355theorem ws_btMakeParent {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (n m node : Int32)
356    (hn : NV (tk.arr d) d.depth n) (hm : NV (tk.arr d) d.depth m)
357    (hp : NV (tk.arr d) d.depth node) :
358    WS h0 id (btMakeParent (Sp id) (.ref (tk.ref id) 0) n m node) d
359      (fun _ e => e = btParentState tk d n m node) := by
360  let T1 := (tk.arr d).set! node.toInt.toNat
361    { (tk.arr d)[node.toInt.toNat]! with fc := ((tk.arr d)[n.toInt.toNat]!).fc + ((tk.arr d)[m.toInt.toNat]!).fc }
362  have hsT1 : T1.size = (tk.arr d).size := by dsimp only [T1]; rw [size_set!]
363  let D := d.depth.set! node.toInt.toNat
364    ((if d.depth[n.toInt.toNat]! ≥ d.depth[m.toInt.toNat]! then
365      d.depth[n.toInt.toNat]! else d.depth[m.toInt.toNat]!) + 1)
366  let d1 := tk.setArr d T1
367  let d2 := { d1 with depth := D }
368  unfold btMakeParent
369  refine WS.bind' (ws_btSetFreq tk d n m node hn.1 hn.2.1 hm.1 hm.2.1 hp.1 hp.2.1)
370    fun _ e1 he1 => ?_
371  change e1 = d1 at he1
372  subst e1
373  have hd1 : d1.depth = d.depth := by exact tk_setArr_depth tk T1
374  refine WS.bind' (ws_btSetDepth d1 n m node hn.1
375    (by rw [hd1]; exact hn.2.2) hm.1 (by rw [hd1]; exact hm.2.2) hp.1
376    (by rw [hd1]; exact hp.2.2)) fun _ e1 he1 => ?_
377  rw [hd1] at he1
378  change e1 = d2 at he1
379  subst e1
380  have hT1 : tk.arr d2 = T1 := by cases tk <;> rfl
381  refine WS.mono (ws_btSetParents tk d2 n m node hn.1
382    (by rw [hT1, hsT1]; exact hn.2.1) hm.1 (by rw [hT1, hsT1]; exact hm.2.1)) ?_
383  intro _ e1 he1
384  subst e1
385  unfold btParentState
386  dsimp only [d2, d1, T1, D]
387  cases tk <;> rfl
388
389/-- The actual closing statements re-establish a fully ordered queue.
390The source's signed counter increment is checked. The exact count equation
391accounts for removing the old root and inserting the new parent. -/
392theorem ws_btMergeClose {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (len : Nat) (node : Int32)
393    (hlen : d.heap_len.toInt = len) (h1 : 1 ≤ len) (hsz : len < d.heap.size)
394    (hbig : d.heap.size ≤ 573) (hnode : NV (tk.arr d) d.depth node) (hinc : node.toInt < 2147483647)
395    (hval : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr d) d.depth d.heap[i]!)
396    (ho : HeapOK (sm (tk.arr d) d.depth) (fun i => d.heap[i]!) len 1) :
397    WS h0 id (btMergeClose (Sp id) (.ref (tk.ref id) 0) node) d (fun r e =>
398      r.toInt = node.toInt + 1 ∧ ∃ H : Array Int32, e = { d with heap := H } ∧ H.size = d.heap.size ∧
399        (∀ i, ¬ (1 ≤ i ∧ i ≤ len) → H[i]! = d.heap[i]!) ∧
400        PermOn (fun i => H[i]!) (fun i => if i = 1 then node else d.heap[i]!) len ∧
401        HeapOK (sm (tk.arr d) d.depth) (fun i => H[i]!) len 0 ∧
402        (∀ q, 1 ≤ q → q ≤ len → sm (tk.arr d) d.depth H[1]! H[q]! = true) ∧
403        ∀ F : Int32 → Nat, GB.rs (fun i => F H[i + 1]!) len + F d.heap[1]! =
404          GB.rs (fun i => F d.heap[i + 1]!) len + F node) := by
405  have hi1 : (1 : Int32).toInt = 1 := rfl
406  have hi1N : (1 : Int32).toInt.toNat = 1 := rfl
407  have hs1 : 1 < d.heap.size := by omega
408  unfold btMergeClose
409  refine WS.bind' (ws_heapSet 1 node (by decide +kernel) (by change (1 : Int) < d.heap.size; omega))
410    fun _ e1 he1 => ?_
411  simp only [hi1N] at he1
412  subst e1
413  refine WS.bind' (ws_iadd node 1 (by have := hnode.1; omega) (by omega)) fun next e1 ⟨hnxt, he1⟩ => ?_
414  subst e1
415  have hvals : ∀ i, 1 ≤ i → i ≤ len →
416      NV (tk.arr { d with heap := d.heap.set! 1 node }) d.depth (d.heap.set! 1 node)[i]! := by
417    intro i hi1 hi2
418    rw [tk_arr_heap, getD_set d.heap 1 i node hs1]
419    split
420    · exact hnode
421    · exact hval i hi1 hi2
422  have horder : HeapOK (sm (tk.arr { d with heap := d.heap.set! 1 node }) d.depth)
423      (fun i => (d.heap.set! 1 node)[i]!) len 1 := by
424    rw [tk_arr_heap]
425    intro c hc2 hcl hcp
426    dsimp only
427    rw [getD_set d.heap 1 (c / 2) node hs1, ite_eq_right (by omega),
428      getD_set d.heap 1 c node hs1, ite_eq_right (by omega)]
429    exact ho c hc2 hcl hcp
430  refine WS.bind' (ws_pqdownheap tk { d with heap := d.heap.set! 1 node } 1 1 len hi1
431    (by omega) h1 hlen (by dsimp only; rw [size_set!]; omega)
432    (by dsimp only; rw [size_set!]; omega) hvals horder)
433    fun _ e1 ⟨H, he1, hsH, hf, hp, hHeap⟩ => ?_
434  subst e1
435  simp only [tk_arr_heap] at hHeap
436  have hp' : PermOn (fun i => H[i]!) (fun i => if i = 1 then node else d.heap[i]!) len := by
437    have heq : (fun i => (d.heap.set! 1 node)[i]!) = (fun i => if i = 1 then node else d.heap[i]!) := by
438      funext i
439      exact getD_set d.heap 1 i node hs1
440    rwa [heq] at hp
441  refine WS.pure' ⟨by omega, H, rfl, by simpa only [size_set!] using hsH, ?_, hp', hHeap, ?_, ?_⟩
442  · intro i hi
443    have hfi := hf i hi
444    dsimp only at hfi
445    rw [hfi, getD_set d.heap 1 i node hs1, ite_eq_right (by omega)]
446  · exact hHeap.root_min (sm_ok (tk.arr d) d.depth)
447  · intro F
448    rw [hp'.sum F]
449    exact replace_root_sum (fun i => d.heap[i]!) node len h1 F
450
451
452/-- Updating the parent link does not change a frequency, including at the
453updated cell. -/
454theorem merge_setDad_fc (T : Array CtData) (k i : Nat) (dad : UInt16) (hk : k < T.size) :
455    ((T.set! k { T[k]! with dl := dad })[i]!).fc = T[i]!.fc := by
456  rw [getD_set T k i _ hk]
457  split <;> simp_all
458
459@[simp] theorem btParentState_heap (tk : TK) (d : DeflateState) (n m node : Int32) :
460    (btParentState tk d n m node).heap = d.heap := by cases tk <;> rfl
461
462@[simp] theorem btParentState_len (tk : TK) (d : DeflateState) (n m node : Int32) :
463    (btParentState tk d n m node).heap_len = d.heap_len := by cases tk <;> rfl
464
465@[simp] theorem btParentState_max (tk : TK) (d : DeflateState) (n m node : Int32) :
466    (btParentState tk d n m node).heap_max = d.heap_max := by cases tk <;> rfl
467
468@[simp] theorem btParentState_tree_size (tk : TK) (d : DeflateState) (n m node : Int32) :
469    (tk.arr (btParentState tk d n m node)).size = (tk.arr d).size := by
470  cases tk <;> simp only [btParentState, TK.arr, TK.setArr, size_set!]
471
472@[simp] theorem btParentState_depth_size (tk : TK) (d : DeflateState) (n m node : Int32) :
473    (btParentState tk d n m node).depth.size = d.depth.size := by
474  cases tk <;> simp only [btParentState, TK.arr, TK.setArr, size_set!]
475
476/-- All parent-link stores preserve frequencies. Only the fresh parent's
477frequency is replaced, with the source's wrapping sum. -/
478theorem btParentState_fc (tk : TK) (d : DeflateState) (n m node : Int32)
479    (hn : NV (tk.arr d) d.depth n) (hm : NV (tk.arr d) d.depth m)
480    (hp : NV (tk.arr d) d.depth node) (i : Nat) :
481    (tk.arr (btParentState tk d n m node))[i]!.fc =
482      if i = node.toInt.toNat then (tk.arr d)[n.toInt.toNat]!.fc + (tk.arr d)[m.toInt.toNat]!.fc
483      else (tk.arr d)[i]!.fc := by
484  have hnT : n.toInt.toNat < (tk.arr d).size := by have := hn.1; have := hn.2.1; omega
485  have hmT : m.toInt.toNat < (tk.arr d).size := by have := hm.1; have := hm.2.1; omega
486  have hpT : node.toInt.toNat < (tk.arr d).size := by have := hp.1; have := hp.2.1; omega
487  have harr : tk.arr (btParentState tk d n m node) =
488      let T := tk.arr d
489      let T1 := T.set! node.toInt.toNat { T[node.toInt.toNat]! with fc := T[n.toInt.toNat]!.fc + T[m.toInt.toNat]!.fc }
490      let T2 := T1.set! m.toInt.toNat { T1[m.toInt.toNat]! with dl := i2us node }
491      T2.set! n.toInt.toNat { T2[n.toInt.toNat]! with dl := i2us node } := by cases tk <;> rfl
492  rw [harr]
493  dsimp only
494  rw [merge_setDad_fc _ _ _ _ (by simp only [size_set!]; exact hnT),
495    merge_setDad_fc _ _ _ _ (by simp only [size_set!]; exact hmT), getD_set _ _ _ _ hpT]
496  split <;> rfl
497
498/-- Every old depth cell is unchanged when the fresh parent depth is written. -/
499theorem btParentState_depth (tk : TK) (d : DeflateState) (n m node : Int32)
500    (hp : NV (tk.arr d) d.depth node) (i : Nat) :
501    (btParentState tk d n m node).depth[i]! =
502      if i = node.toInt.toNat then
503        (if d.depth[n.toInt.toNat]! ≥ d.depth[m.toInt.toNat]! then
504          d.depth[n.toInt.toNat]! else d.depth[m.toInt.toNat]!) + 1
505      else d.depth[i]! := by
506  have hpD : node.toInt.toNat < d.depth.size := by have := hp.1; have := hp.2.2; omega
507  exact getD_set _ _ _ _ hpD
508
509/-- The ordering key of any two previously allocated nodes is preserved.
510Freshness is a numeric data condition, not a callee specification. -/
511theorem btParentState_sm (tk : TK) (d : DeflateState) (n m node a b : Int32)
512    (hn : NV (tk.arr d) d.depth n) (hm : NV (tk.arr d) d.depth m)
513    (hp : NV (tk.arr d) d.depth node)
514    (ha : 0 ≤ a.toInt) (hap : a.toInt < node.toInt)
515    (hb : 0 ≤ b.toInt) (hbp : b.toInt < node.toInt) :
516    sm (tk.arr (btParentState tk d n m node)) (btParentState tk d n m node).depth a b =
517      sm (tk.arr d) d.depth a b := by
518  have han : a.toInt.toNat ≠ node.toInt.toNat := by omega
519  have hbn : b.toInt.toNat ≠ node.toInt.toNat := by omega
520  simp only [sm, btParentState_fc tk d n m node hn hm hp, btParentState_depth tk d n m node hp,
521    han, hbn, ite_false]
522
523
524/-- One complete actual merge iteration terminates, creates its parent,
525retains both children in the tail and restores a distinct ordered queue.
526The explicit numeric freshness and queue/tail separation conditions are
527internal representation obligations; no called function's contract is a
528premise. The count equation holds for every node-counting function. -/
529theorem ws_btMergeBody {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (len : Nat) (node : Int32)
530    (hlen : d.heap_len.toInt = len) (h2 : 2 ≤ len) (hsz : len < d.heap.size)
531    (hbig : d.heap.size ≤ 573) (hmH : d.heap_max.toInt ≤ d.heap.size)
532    (hgap : (len : Int) < d.heap_max.toInt - 1)
533    (hp : NV (tk.arr d) d.depth node) (hinc : node.toInt < 2147483647)
534    (hbefore : ∀ i, 1 ≤ i → i ≤ len → 0 ≤ d.heap[i]!.toInt ∧ d.heap[i]!.toInt < node.toInt)
535    (hinj : ∀ i j, 1 ≤ i → i ≤ len → 1 ≤ j → j ≤ len → d.heap[i]! = d.heap[j]! → i = j)
536    (ho : HeapOK (sm (tk.arr d) d.depth) (fun i => d.heap[i]!) len 0) :
537    WS h0 id (btMergeBody (Sp id) (.ref (tk.ref id) 0) node) d (fun r e =>
538      r.toInt = node.toInt + 1 ∧ ∃ (n m hl hm1 hm2 : Int32) (H H' : Array Int32),
539        n = d.heap[1]! ∧ m = H[1]! ∧ n ≠ m ∧
540        hl.toInt = (len : Int) - 1 ∧ hm1.toInt = d.heap_max.toInt - 1 ∧ hm2.toInt = d.heap_max.toInt - 2 ∧
541        e = { btParentState tk { d with heap := H, heap_len := hl, heap_max := hm2 } n m node with heap := H' } ∧
542        H'.size = d.heap.size ∧ H'[hm1.toInt.toNat]! = n ∧ H'[hm2.toInt.toNat]! = m ∧
543        HeapOK (sm (tk.arr e) e.depth) (fun i => H'[i]!) (len - 1) 0 ∧
544        (∀ i, 1 ≤ i → i ≤ len - 1 → 0 ≤ H'[i]!.toInt ∧ H'[i]!.toInt ≤ node.toInt) ∧
545        (∀ i j, 1 ≤ i → i ≤ len - 1 → 1 ≤ j → j ≤ len - 1 → H'[i]! = H'[j]! → i = j) ∧
546        ∀ F : Int32 → Nat, GB.rs (fun i => F H'[i + 1]!) (len - 1) + F n + F m =
547          GB.rs (fun i => F d.heap[i + 1]!) len + F node) := by
548  have hv : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr d) d.depth d.heap[i]! := by
549    intro i hi1 hi2
550    have hb := hbefore i hi1 hi2
551    exact ⟨hb.1, by have := hp.2.1; omega, by have := hp.2.2; omega⟩
552  unfold btMergeBody
553  refine WS.bind' (ws_btMergeOpen tk d len hlen h2 hsz hbig hmH hgap hv hinj ho)
554    fun pair e1 ⟨hl, hm1, hm2, H, hn, hm, hnm, hhl, hh1, hh2, he1, hsH, hkeepn, hkeepm,
555      hnv, hmv, horder, hminn, hminm, horigin, hcomplete, hno, hHi, hcount⟩ => ?_
556  rcases pair with ⟨n, m⟩
557  dsimp only at hn hm hnm hnv hmv hminn hminm hkeepn hkeepm hno hcount ⊢
558  subst e1
559  let d1 := { d with heap := H, heap_len := hl, heap_max := hm2 }
560  have hT1 : tk.arr d1 = tk.arr d := by cases tk <;> rfl
561  have hD1 : d1.depth = d.depth := rfl
562  have hp1 : NV (tk.arr d1) d1.depth node := by rw [hT1, hD1]; exact hp
563  have hn1 : NV (tk.arr d1) d1.depth n := by rw [hT1, hD1]; exact hnv
564  have hm1v : NV (tk.arr d1) d1.depth m := by rw [hT1, hD1]; exact hmv
565  have hB : ∀ i, 1 ≤ i → i ≤ len - 1 → 0 ≤ H[i]!.toInt ∧ H[i]!.toInt < node.toInt := by
566    intro i hi1 hi2
567    obtain ⟨j, hj1, hj2, heq⟩ := horigin i hi1 hi2
568    rw [heq]
569    exact hbefore j (by omega) hj2
570  refine WS.bind' (ws_btMakeParent tk d1 n m node hn1 hm1v hp1) fun _ e2 he2 => ?_
571  subst e2
572  let d2 := btParentState tk d1 n m node
573  have hp2 : NV (tk.arr d2) d2.depth node := by
574    simpa only [d2, NV, btParentState_tree_size, btParentState_depth_size] using hp1
575  have hv2 : ∀ i, 1 ≤ i → i ≤ len - 1 → NV (tk.arr d2) d2.depth d2.heap[i]! := by
576    intro i hi1 hi2
577    have hb := hB i hi1 hi2
578    simp only [d2, btParentState_heap, d1, NV, btParentState_tree_size, btParentState_depth_size, hT1]
579    exact ⟨hb.1, by have := hp.2.1; omega, by have := hp.2.2; omega⟩
580  have ho2 : HeapOK (sm (tk.arr d2) d2.depth) (fun i => d2.heap[i]!) (len - 1) 1 := by
581    intro c hc2 hcl hcp
582    have hb := hB c (by omega) hcl
583    have hb' := hB (c / 2) (by omega) (by omega)
584    dsimp only [d2]
585    rw [btParentState_heap]
586    change sm (tk.arr (btParentState tk d1 n m node)) (btParentState tk d1 n m node).depth H[c / 2]! H[c]! = true
587    rw [btParentState_sm tk d1 n m node _ _ hn1 hm1v hp1 hb'.1 hb'.2 hb.1 hb.2, hT1, hD1]
588    exact horder c hc2 hcl (by omega)
589  refine WS.mono (ws_btMergeClose tk d2 (len - 1) node
590    (by simpa only [d2, btParentState_len] using hhl.trans (by omega)) (by omega)
591    (by simpa only [d2, btParentState_heap] using (show len - 1 < H.size by omega))
592    (by simpa only [d2, btParentState_heap] using (show H.size ≤ 573 by omega)) hp2 hinc hv2 ho2) ?_
593  intro next e3 ⟨hnext, H', he3, hsH', hframe, hperm, horder', hmin', hcount'⟩
594  subst e3
595  have hHeap2 : d2.heap = H := by simp only [d2, btParentState_heap]; rfl
596  have hlen1 : 1 ≤ len - 1 := by omega
597  have hroot : d2.heap[1]! = m := by rw [hHeap2]; exact hm.symm
598  have hRep : ∀ i, 1 ≤ i → i ≤ len - 1 →
599      0 ≤ (if i = 1 then node else H[i]!).toInt ∧ (if i = 1 then node else H[i]!).toInt ≤ node.toInt := by
600    intro i hi1 hi2
601    split
602    · exact ⟨hp.1, by omega⟩
603    · have hb := hB i hi1 hi2; exact ⟨hb.1, by omega⟩
604  have hRepInj : ∀ i j, 1 ≤ i → i ≤ len - 1 → 1 ≤ j → j ≤ len - 1 →
605      (if i = 1 then node else H[i]!) = (if j = 1 then node else H[j]!) → i = j := by
606    intro i j hi1 hi2 hj1 hj2 heq
607    by_cases hi : i = 1 <;> by_cases hj : j = 1
608    · omega
609    · simp only [hi, hj, ite_true, ite_false] at heq
610      have hb := hB j hj1 hj2
611      rw [← heq] at hb
612      omega
613    · simp only [hi, hj, ite_true, ite_false] at heq
614      have hb := hB i hi1 hi2
615      rw [heq] at hb
616      omega
617    · simp only [hi, hj, ite_false] at heq
618      exact hHi i j hi1 hi2 hj1 hj2 heq
619  have hp' : PermOn (fun i => H'[i]!) (fun i => if i = 1 then node else H[i]!) (len - 1) := by
620    simpa only [hHeap2] using hperm
621  refine ⟨hnext, n, m, hl, hm1, hm2, H, H', hn, hm, hnm, hhl, hh1, hh2, rfl,
622    hsH'.trans (by rw [hHeap2]; exact hsH), ?_, ?_, ?_, ?_, hp'.injective hRepInj, ?_⟩
623  · rw [hframe _ (by omega), hHeap2]
624    exact hkeepn
625  · rw [hframe _ (by omega), hHeap2]
626    exact hkeepm
627  · simpa only [tk_arr_heap] using horder'
628  · intro i hi1 hi2
629    obtain ⟨σ, hr, hi, he⟩ := hp'
630    have hei := he i hi1 hi2
631    dsimp only at hei
632    rw [hei]
633    exact hRep (σ i) (hr i hi1 hi2).1 (hr i hi1 hi2).2
634  · intro F
635    have hc := hcount F
636    have hc' := hcount' F
637    rw [hroot, hHeap2] at hc'
638    omega
639
640
641/-- Queue representation during actual node merging. The stage counts
642completed merges. This records numeric geometry and actual data; it contains
643no assumed execution contract. Tail shape and parent links are separate
644obligations of the tree-layout proof. -/
645structure BTMergeQueue (tk : TK) (N K j : Nat) (node : Int32) (d : DeflateState) : Prop where
646  n3 : 3 ≤ N
647  n286 : N ≤ 286
648  k2 : 2 ≤ K
649  kN : K ≤ N
650  stage : j < K
651  counter : node.toInt = (N + j : Nat)
652  len : d.heap_len.toInt = (K - j : Nat)
653  max : d.heap_max.toInt + 2 * (j : Int) = 573
654  tree : N + K - 1 ≤ (tk.arr d).size
655  depth : N + K - 1 ≤ d.depth.size
656  heap : d.heap.size = 573
657  valid : ∀ i : Nat, 1 ≤ i → (i : Int) ≤ d.heap_len.toInt →
658    0 ≤ d.heap[i]!.toInt ∧ d.heap[i]!.toInt < node.toInt
659  injective : ∀ i i' : Nat, 1 ≤ i → (i : Int) ≤ d.heap_len.toInt →
660    1 ≤ i' → (i' : Int) ≤ d.heap_len.toInt → d.heap[i]! = d.heap[i']! → i = i'
661  order : HeapOK (sm (tk.arr d) d.depth) (fun i => d.heap[i]!) (K - j) 0
662
663/-- Actual sorted leaves establish the initial queue representation.
664Internal-node array capacity is explicit; the old leaf-prefix theorem does
665not claim to supply that additional capacity. -/
666theorem BTMergeQueue.of_leaf {tk : TK} {d : DeflateState} {N : Nat} {mc node : Int32}
667    (hi : BTLeafInv tk N mc d) (h2 : 2 ≤ d.heap_len.toInt) (hm : d.heap_max = HEAP_SIZE)
668    (hn : node.toInt = N)
669    (hT : N + d.heap_len.toInt.toNat - 1 ≤ (tk.arr d).size)
670    (hD : N + d.heap_len.toInt.toNat - 1 ≤ d.depth.size)
671    (ho : HeapOK (sm (tk.arr d) d.depth) (fun i => d.heap[i]!) d.heap_len.toInt.toNat 0) :
672    BTMergeQueue tk N d.heap_len.toInt.toNat 0 node d := by
673  have hc := hi.count
674  have hKN := Math.scanCount_le (btFreq tk d) N
675  refine ⟨hi.n3, hi.n286, by omega, by omega, by omega, by omega, by omega,
676    by rw [hm]; rfl, hT, hD, hi.heap, ?_, hi.injective, ?_⟩
677  · intro i hi1 hi2
678    have hv := hi.valid i hi1 hi2
679    exact ⟨hv.1, by omega⟩
680  · simpa only [Nat.sub_zero] using ho
681
682/-- The checked whole iteration preserves the queue representation and
683advances its stage by one. Every bound for the called fragments is derived
684from this representation. -/
685theorem ws_btMergeBody_queue {h0 : Heap} {id : Nat} {tk : TK} {d : DeflateState}
686    {N K j : Nat} {node : Int32} (hi : BTMergeQueue tk N K j node d) (hmore : j + 1 < K) :
687    WS h0 id (btMergeBody (Sp id) (.ref (tk.ref id) 0) node) d
688      (fun next e => BTMergeQueue tk N K (j + 1) next e) := by
689  have hNs := hi.n3
690  have hNb := hi.n286
691  have hK2 := hi.k2
692  have hKN := hi.kN
693  have hj := hi.stage
694  have hn := hi.counter
695  have hl := hi.len
696  have hm := hi.max
697  have hH := hi.heap
698  have hT := hi.tree
699  have hD := hi.depth
700  have hp : NV (tk.arr d) d.depth node := ⟨by omega, by omega, by omega⟩
701  refine WS.mono (ws_btMergeBody tk d (K - j) node hl (by omega) (by omega)
702    (by omega) (by omega) (by omega) hp (by omega)
703    (fun i hi1 hi2 => hi.valid i hi1 (by omega))
704    (fun i i' hi1 hi2 hi'1 hi'2 => hi.injective i i' hi1 (by omega) hi'1 (by omega)) hi.order) ?_
705  intro next e ⟨hnext, n, m, hlen, hm1, hm2, H, H', hn', hm', hnm, hlen', hm1', hm2', he,
706    hsize, htailn, htailm, horder, hvalid, hinj, hcount⟩
707  subst e
708  have hT' : (tk.arr { btParentState tk { d with heap := H, heap_len := hlen, heap_max := hm2 } n m node with heap := H' }).size = (tk.arr d).size := by
709    rw [tk_arr_heap, btParentState_tree_size]
710    cases tk <;> rfl
711  refine ⟨hNs, hNb, hK2, hKN, hmore, by omega, ?_, ?_, by rw [hT']; exact hT,
712    by simpa only [btParentState_depth_size] using hD, by exact hsize.trans hH, ?_, ?_, ?_⟩
713  · simp only [btParentState_len]
714    omega
715  · simp only [btParentState_max]
716    omega
717  · intro i hi1 hi2
718    simp only [btParentState_len] at hi2
719    have hv := hvalid i hi1 (by omega)
720    change 0 ≤ H'[i]!.toInt ∧ H'[i]!.toInt < next.toInt
721    exact ⟨hv.1, by omega⟩
722  · intro i i' hi1 hi2 hi'1 hi'2 heq
723    simp only [btParentState_len] at hi2 hi'2
724    exact hinj i i' hi1 (by omega) hi'1 (by omega) heq
725  · have heq : K - (j + 1) = K - j - 1 := by omega
726    rwa [heq]
727
728/-- The complete actual merge loop terminates after exactly K-1 iterations.
729Its queue has one valid root and its counter and tail boundary have their
730exact source values. This is queue safety and order, not yet tree-layout or
731code-emission correctness. -/
732theorem ws_btMergeLoop {h0 : Heap} {id : Nat} {tk : TK} {d : DeflateState}
733    {N K : Nat} {node : Int32} (hi : BTMergeQueue tk N K 0 node d) :
734    WS h0 id (btMergeLoop (Sp id) (.ref (tk.ref id) 0) node) d
735      (fun next e => BTMergeQueue tk N K (K - 1) next e ∧ e.heap_len.toInt = 1) := by
736  let Inv : Int32 → DeflateState → Prop := fun node e =>
737    ∃ j : Nat, BTMergeQueue tk N K j node e ∧ j + 1 < K
738  let Q : Int32 → DeflateState → Prop := fun node e =>
739    BTMergeQueue tk N K (K - 1) node e ∧ e.heap_len.toInt = 1
740  unfold btMergeLoop
741  refine WS.cdoWhile2 Inv (fun _ e => e.heap_len.toInt.toNat) Q ?_
742    ⟨0, hi, by have := hi.k2; omega⟩ (by have := hi.len; have := hi.kN; have := hi.n286; dsimp only [fuel]; omega)
743  intro current e ⟨j, hj, hmore⟩
744  refine WS.mono (ws_btMergeBody_queue hj hmore) ?_
745  intro next e' hj'
746  refine WS.bind' ws_rd fun got e'' ⟨hgot, he''⟩ => ?_
747  subst e''; subst got
748  have hlen := hj'.len
749  have hstage := hj'.stage
750  have hK := hj'.k2
751  by_cases hcontinue : e'.heap_len.toInt ≥ 2
752  · have hjnext : j + 1 + 1 < K := by omega
753    refine WS.pure' (Or.inr ⟨by simp only [hcontinue, decide_true], ⟨j + 1, hj', hjnext⟩, ?_⟩)
754    have hlen0 := hj.len
755    omega
756  · have hjend : j + 1 = K - 1 := by omega
757    refine WS.pure' (Or.inl ⟨by simp only [hcontinue, decide_false], ?_⟩)
758    change Q next e'
759    rw [hjend] at hj'
760    exact ⟨hj', by omega⟩
761
762
763/-- Deterministic executions of the same fragment have the same result and
764state. Thus separately proved data properties can be combined. -/
765theorem merge_ws_and {α : Type} {h0 : Heap} {id : Nat} {m : M α} {d : DeflateState}
766    {Q R : α → DeflateState → Prop} (hq : WS h0 id m d Q) (hr : WS h0 id m d R) :
767    WS h0 id m d (fun a e => Q a e ∧ R a e) := by
768  obtain ⟨a, e, he, hQ⟩ := hq
769  obtain ⟨b, f, hf, hR⟩ := hr
770  have hp := Except.ok.inj (he.symm.trans hf)
771  have hab : a = b := congrArg Prod.fst hp
772  have hef : e = f := by
773    have hh := congrArg (fun p => p.2.dstates id) hp
774    simp only [setD_dstates_same] at hh
775    exact Option.some.inj hh
776  subst b; subst f
777  exact ⟨a, e, he, hQ, hR⟩
778
779/-- The final root store executes its checked decrement and keeps every
780other heap cell. Its exact record effect also frames the tree and depth. -/
781theorem ws_btSaveRoot {h0 : Heap} {id : Nat} (d : DeflateState)
782    (hroot : 1 < d.heap.size) (hm1 : 1 ≤ d.heap_max.toInt)
783    (hmH : d.heap_max.toInt ≤ d.heap.size) (hbig : d.heap.size ≤ 573) :
784    WS h0 id (btSaveRoot (Sp id)) d (fun _ e => ∃ hm : Int32,
785      hm.toInt = d.heap_max.toInt - 1 ∧
786      e = { d with heap := d.heap.set! hm.toInt.toNat d.heap[1]!, heap_max := hm } ∧
787      e.heap.size = d.heap.size ∧ e.heap[hm.toInt.toNat]! = d.heap[1]! ∧
788      ∀ i : Nat, i ≠ hm.toInt.toNat → e.heap[i]! = d.heap[i]!) := by
789  unfold btSaveRoot
790  refine WS.bind' (ws_heapAt 1 (by decide +kernel) (by change (1 : Int) < d.heap.size; omega))
791    fun top e1 ⟨htop, he1⟩ => ?_
792  subst e1
793  have hi1 : (1 : Int32).toInt.toNat = 1 := rfl
794  change top = d.heap[(1 : Int32).toInt.toNat]! at htop
795  rw [hi1] at htop
796  subst top
797  refine WS.bind' ws_rd fun got e1 ⟨hgot, he1⟩ => ?_
798  subst e1; subst got
799  refine WS.bind' (ws_isub d.heap_max 1 (by omega) (by omega)) fun hm e1 ⟨hhm, he1⟩ => ?_
800  subst e1
801  refine WS.bind' (ws_md (fun e => { e with heap_max := hm })) fun _ e1 he1 => ?_
802  subst e1
803  refine WS.mono (ws_heapSet hm d.heap[1]! (by omega) (by dsimp only; omega)) ?_
804  intro _ e he
805  subst e
806  have hi : hm.toInt.toNat < d.heap.size := by omega
807  refine ⟨hm, by omega, rfl, size_set! _ _ _, ?_, ?_⟩
808  · rw [getD_set d.heap hm.toInt.toNat _ _ hi, ite_eq_left rfl]
809  · intro i hne
810    rw [getD_set d.heap hm.toInt.toNat i _ hi, ite_eq_right hne]
811
812
813/-- The exact selected-tree array after parent creation. -/
814theorem btParentState_arr (tk : TK) (d : DeflateState) (n m node : Int32) :
815    tk.arr (btParentState tk d n m node) =
816      let T := tk.arr d
817      let T1 := T.set! node.toInt.toNat { T[node.toInt.toNat]! with fc := T[n.toInt.toNat]!.fc + T[m.toInt.toNat]!.fc }
818      let T2 := T1.set! m.toInt.toNat { T1[m.toInt.toNat]! with dl := i2us node }
819      T2.set! n.toInt.toNat { T2[n.toInt.toNat]! with dl := i2us node } := by cases tk <;> rfl
820
821/-- A frequency store preserves every parent-link cell. -/
822theorem merge_setFreq_dad (T : Array CtData) (k i : Nat) (freq : UInt16) (hk : k < T.size) :
823    ((T.set! k { T[k]! with fc := freq })[i]!).dl = T[i]!.dl := by
824  rw [getD_set T k i _ hk]
825  split <;> simp_all
826
827/-- A parent-link store replaces precisely one parent-link value. -/
828theorem merge_setDad_dad (T : Array CtData) (k i : Nat) (dad : UInt16) (hk : k < T.size) :
829    ((T.set! k { T[k]! with dl := dad })[i]!).dl = if i = k then dad else T[i]!.dl := by
830  rw [getD_set T k i _ hk]
831  split <;> rfl
832
833/-- Both selected children receive the new parent index. Every other link
834is unchanged, even if it is the parent node's old link. This states the
835source's 16-bit cast; lossless numeric parent indices follow from bounds. -/
836theorem btParentState_dad (tk : TK) (d : DeflateState) (n m node : Int32)
837    (hn : NV (tk.arr d) d.depth n) (hm : NV (tk.arr d) d.depth m)
838    (hp : NV (tk.arr d) d.depth node) (i : Nat) :
839    (tk.arr (btParentState tk d n m node))[i]!.dl =
840      if i = n.toInt.toNat ∨ i = m.toInt.toNat then i2us node else (tk.arr d)[i]!.dl := by
841  have hnT : n.toInt.toNat < (tk.arr d).size := by have := hn.1; have := hn.2.1; omega
842  have hmT : m.toInt.toNat < (tk.arr d).size := by have := hm.1; have := hm.2.1; omega
843  have hpT : node.toInt.toNat < (tk.arr d).size := by have := hp.1; have := hp.2.1; omega
844  rw [btParentState_arr]
845  dsimp only
846  rw [merge_setDad_dad _ _ _ _ (by simp only [size_set!]; exact hnT),
847    merge_setDad_dad _ _ _ _ (by simp only [size_set!]; exact hmT), merge_setFreq_dad _ _ _ _ hpT]
848  by_cases hin : i = n.toInt.toNat <;> by_cases him : i = m.toInt.toNat <;> simp only [hin, him, ite_true, ite_false, or_self, true_or, false_or, or_true, ite_self]
849
850/-- The queue representation leaves room for the final checked root store.
851This includes the largest admitted alphabet and leaf count. -/
852theorem BTMergeQueue.tail_bounds {tk : TK} {d : DeflateState} {N K j : Nat} {node : Int32}
853    (hi : BTMergeQueue tk N K j node d) : 3 ≤ d.heap_max.toInt ∧ d.heap_max.toInt ≤ 573 := by
854  have := hi.n286
855  have := hi.kN
856  have := hi.stage
857  have := hi.max
858  omega
859
860end Zlib.Trees.Proofs