trees.c.build.heapify.lean

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

1import ZlibF.Math.DeflateHeap
2import ZlibF.Proof.«trees.c.heap.pqrun»
3import ZlibF.Proof.«trees.c.build.force»
4
5/-! # trees.c: actual heap construction and preservation of its leaves -/
6
7namespace Zlib.Trees.Proofs
8open C Zlib.Trees
9
10/-- The actual descending `pqdownheap` loop, including the initial state
11read, signed division by two and separate checked decrement. -/
12def btHeapify (s : DeflateStatePtr) (tree : CtDataPtr) : M Int32 := do
13  cfor (σ := Int32) (fun n => pure (decide (n.toInt ≥ 1))) (fun n => isub n 1)
14    (fun n => do pqdownheap s tree n; pure n) ((← rd s).heap_len / 2)
15
16/-- Every leaf representation fact survives a permutation of the populated
17heap interval. Completeness uses surjectivity, not just forward validity. -/
18theorem BTLeafInv.heap_perm {tk : TK} {N : Nat} {mc : Int32} {d : DeflateState}
19    (hi : BTLeafInv tk N mc d) (H : Array Int32) (hsz : H.size = d.heap.size)
20    (hp : PermOn (fun q => H[q]!) (fun q => d.heap[q]!) d.heap_len.toInt.toNat) :
21    BTLeafInv tk N mc { d with heap := H } := by
22  have hlen0 : 0 ≤ d.heap_len.toInt := by have := hi.count; omega
23  have hfreq : btFreq tk { d with heap := H } = btFreq tk d := by
24    funext v; unfold btFreq; rw [tk_arr_heap]
25  obtain ⟨σ, hr, hinj, he⟩ := hp
26  dsimp only at hr hinj he
27  refine ⟨hi.n3, hi.n286, ?_, hi.depth, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
28  · rw [tk_arr_heap]; exact hi.tree
29  · change H.size = 573; rw [hsz, hi.heap]
30  · rw [hfreq]; exact hi.count
31  · rw [hfreq]; exact hi.maxCode
32  · intro q hq1 hq2
33    change (q : Int) ≤ d.heap_len.toInt at hq2
34    have hq : q ≤ d.heap_len.toInt.toNat := by omega
35    have hσ := hr q hq1 hq
36    have hv := hi.valid (σ q) hσ.1 (by omega)
37    change 0 ≤ H[q]!.toInt ∧ H[q]!.toInt < N ∧ _
38    rw [he q hq1 hq, hfreq]
39    exact hv
40  · intro q q' hq1 hq2 hq'1 hq'2 heq
41    have hq : q ≤ d.heap_len.toInt.toNat := by change (q : Int) ≤ d.heap_len.toInt at hq2; omega
42    have hq' : q' ≤ d.heap_len.toInt.toNat := by change (q' : Int) ≤ d.heap_len.toInt at hq'2; omega
43    have hσ := hr q hq1 hq
44    have hσ' := hr q' hq'1 hq'
45    change H[q]! = H[q']! at heq
46    rw [he q hq1 hq, he q' hq'1 hq'] at heq
47    exact hinj q q' hq1 hq hq'1 hq' (hi.injective _ _ hσ.1 (by omega) hσ'.1 (by omega) heq)
48  · intro v hv hfv
49    rw [hfreq] at hfv
50    obtain ⟨q, hq1, hq2, hqv⟩ := hi.complete v hv hfv
51    obtain ⟨q', hq'1, hq'2, hqeq⟩ := PermOn.preimage ⟨σ, hr, hinj, he⟩ q hq1 (by omega)
52    refine ⟨q', hq'1, by dsimp; omega, ?_⟩
53    change H[q']!.toInt = v
54    rw [hqeq]; exact hqv
55  · intro v hv hfv
56    rw [hfreq] at hfv
57    exact hi.usedDepth v hv hfv
58  · intro v hv hfv
59    rw [hfreq] at hfv
60    rw [tk_arr_heap]
61    exact hi.unusedLength v hv hfv
62
63/-- The complete actual heapify loop terminates with all parent/child edges
64ordered by zlib's frequency/depth comparison. Only the populated heap cells
65change, and their contents are a permutation of the original cells. No
66`pqdownheap` contract is assumed; its translated execution theorem is used. -/
67theorem ws_btHeapify {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (len : Nat)
68    (hlen : d.heap_len.toInt = len) (hsz : len < d.heap.size) (hbig : d.heap.size ≤ 573)
69    (hval : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr d) d.depth d.heap[i]!) :
70    WS h0 id (btHeapify (Sp id) (.ref (tk.ref id) 0)) d (fun r e =>
71      r.toInt = 0 ∧ ∃ H : Array Int32, e = { d with heap := H } ∧ H.size = d.heap.size ∧
72        (∀ i, ¬ (1 ≤ i ∧ i ≤ len) → H[i]! = d.heap[i]!) ∧
73        PermOn (fun i => H[i]!) (fun i => d.heap[i]!) len ∧
74        HeapOK (sm (tk.arr d) d.depth) (fun i => H[i]!) len 0) := by
75  have hi1 : (1 : Int32).toInt = 1 := rfl
76  have hi2 : (2 : Int32).toInt = 2 := rfl
77  have hstart : (d.heap_len / 2).toInt = (len / 2 : Nat) := by
78    rw [Int32.toInt_div_of_ne_right _ _ (by decide +kernel), hi2, hlen]
79    exact (Int.ofNat_tdiv len 2).symm
80  let Inv : Int32 → DeflateState → Prop := fun n e =>
81    0 ≤ n.toInt ∧ n.toInt ≤ (len / 2 : Nat) ∧ ∃ H : Array Int32,
82      e = { d with heap := H } ∧ H.size = d.heap.size ∧
83      (∀ i, ¬ (1 ≤ i ∧ i ≤ len) → H[i]! = d.heap[i]!) ∧
84      PermOn (fun i => H[i]!) (fun i => d.heap[i]!) len ∧
85      HeapOK (sm (tk.arr d) d.depth) (fun i => H[i]!) len n.toInt.toNat
86  unfold btHeapify
87  refine WS.bind' ws_rd fun dz e1 ⟨hdz, he1⟩ => ?_
88  subst e1; subst dz
89  refine WS.cfor2 Inv (fun n _ => n.toInt.toNat) _ ?_
90    ⟨by omega, by omega, d.heap, rfl, rfl, fun _ _ => rfl, PermOn.refl _ _, ?_⟩
91    (by simp only [fuel]; omega)
92  · intro n e ⟨hn0, hn1, H, he, hsH, hf, hp, hok⟩
93    subst e
94    refine WS.pure' ?_
95    by_cases hpos : 1 ≤ n.toInt
96    · refine Or.inr ⟨by simp only [decide_eq_true_eq]; exact hpos, ?_⟩
97      have hn : n.toInt = (n.toInt.toNat : Nat) := by omega
98      have hvals : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr { d with heap := H }) d.depth H[i]! := by
99        obtain ⟨σ, hr, hinj, heq⟩ := hp
100        dsimp only at hr hinj heq
101        intro i hi1 hi2
102        rw [tk_arr_heap, heq i hi1 hi2]
103        exact hval _ (hr i hi1 hi2).1 (hr i hi1 hi2).2
104      have horder : HeapOK (sm (tk.arr { d with heap := H }) d.depth) (fun i => H[i]!) len n.toInt.toNat := by
105        rw [tk_arr_heap]; exact hok
106      simp only [M_bind_assoc, M_pure_bind]
107      refine WS.bind' (ws_pqdownheap tk { d with heap := H } n n.toInt.toNat len hn (by omega)
108        (by omega) hlen (by dsimp; omega) (by dsimp; omega) hvals horder)
109        fun _ e1 ⟨H', he1, hsH', hf', hp', hok'⟩ => ?_
110      subst e1
111      refine WS.mono (ws_isub n 1 (by omega) (by omega)) ?_
112      intro n' e1 ⟨hn', he1⟩
113      subst e1
114      have hcut : n'.toInt.toNat = n.toInt.toNat - 1 := by omega
115      refine ⟨⟨by omega, by omega, H', rfl,
116        by dsimp at hsH'; omega, ?_, hp'.trans' hp, ?_⟩, by omega⟩
117      · intro i hi; exact (hf' i hi).trans (hf i hi)
118      · rw [tk_arr_heap] at hok'
119        simpa only [hcut] using hok'
120    · refine Or.inl ⟨by simp only [decide_eq_false_iff_not]; omega,
121        by omega, H, rfl, hsH, hf, hp, ?_⟩
122      have hn : n.toInt.toNat = 0 := by omega
123      simpa only [hn] using hok
124  · intro c hc1 hc2 hcp
125    omega
126
127/-- The actual heapify loop obtains its node bounds from the leaf invariant,
128preserves that invariant, and establishes both heap order and root minimality.
129The latter is the comparison used by the subsequent two-node merge. -/
130theorem ws_btHeapify_leaf {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (N : Nat) (mc : Int32)
131    (hi : BTLeafInv tk N mc d) :
132    WS h0 id (btHeapify (Sp id) (.ref (tk.ref id) 0)) d (fun r e =>
133      r.toInt = 0 ∧ BTLeafInv tk N mc e ∧ ∃ H : Array Int32,
134        e = { d with heap := H } ∧ H.size = d.heap.size ∧
135        (∀ i, ¬ (1 ≤ i ∧ i ≤ d.heap_len.toInt.toNat) → H[i]! = d.heap[i]!) ∧
136        PermOn (fun i => H[i]!) (fun i => d.heap[i]!) d.heap_len.toInt.toNat ∧
137        HeapOK (sm (tk.arr d) d.depth) (fun i => H[i]!) d.heap_len.toInt.toNat 0 ∧
138        ∀ q, 1 ≤ q → q ≤ d.heap_len.toInt.toNat → sm (tk.arr d) d.depth H[1]! H[q]! = true) := by
139  let len := d.heap_len.toInt.toNat
140  have hlen : d.heap_len.toInt = len := by have := hi.count; dsimp only [len]; omega
141  have hcount := Math.scanCount_le (btFreq tk d) N
142  have hlenN : len ≤ N := by have := hi.count; omega
143  have hval : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr d) d.depth d.heap[i]! := by
144    intro i hi1 hi2
145    obtain ⟨h0, hN, hf⟩ := hi.valid i hi1 (by omega)
146    exact ⟨h0, by have := hi.tree; omega, by have := hi.depth; omega⟩
147  refine WS.mono (ws_btHeapify tk d len hlen (by rw [hi.heap]; have := hi.n286; omega)
148    (by rw [hi.heap]; omega) hval) ?_
149  intro r e ⟨hr, H, he, hsz, hf, hp, ho⟩
150  subst e
151  refine ⟨hr, hi.heap_perm H hsz hp, H, rfl, hsz, hf, hp, ho, ?_⟩
152  exact ho.root_min (sm_ok (tk.arr d) d.depth)
153
154/-- The descriptor field selected by a dynamic-tree kind. -/
155def TK.descRef : TK → Nat → TreeDescRef
156  | .lit, id => .in_dstate_l_desc id
157  | .dist, id => .in_dstate_d_desc id
158  | .bl, id => .in_dstate_bl_desc id
159
160def TK.getDesc : TK → DeflateState → TreeDesc
161  | .lit, d => d.l_desc
162  | .dist, d => d.d_desc
163  | .bl, d => d.bl_desc
164
165def TK.setDesc : TK → DeflateState → TreeDesc → DeflateState
166  | .lit, d, v => { d with l_desc := v }
167  | .dist, d, v => { d with d_desc := v }
168  | .bl, d, v => { d with bl_desc := v }
169
170@[simp] theorem tk_arr_setDesc (tk dk : TK) (d : DeflateState) (v : TreeDesc) :
171    tk.arr (dk.setDesc d v) = tk.arr d := by cases tk <;> cases dk <;> rfl
172
173@[simp] theorem tk_setDesc_heap (dk : TK) (d : DeflateState) (v : TreeDesc) :
174    (dk.setDesc d v).heap = d.heap := by cases dk <;> rfl
175
176@[simp] theorem tk_setDesc_len (dk : TK) (d : DeflateState) (v : TreeDesc) :
177    (dk.setDesc d v).heap_len = d.heap_len := by cases dk <;> rfl
178
179@[simp] theorem tk_setDesc_depth (dk : TK) (d : DeflateState) (v : TreeDesc) :
180    (dk.setDesc d v).depth = d.depth := by cases dk <;> rfl
181
182/-- Storing a descriptor does not change any of the leaf data. -/
183theorem BTLeafInv.setDesc {tk : TK} {N : Nat} {mc : Int32} {d : DeflateState}
184    (hi : BTLeafInv tk N mc d) (dk : TK) (v : TreeDesc) : BTLeafInv tk N mc (dk.setDesc d v) := by
185  cases tk <;> cases dk <;>
186    exact ⟨hi.n3, hi.n286, hi.tree, hi.depth, hi.heap, hi.count, hi.maxCode,
187      hi.valid, hi.injective, hi.complete, hi.usedDepth, hi.unusedLength⟩
188
189/-- The actual descriptor read/store and heapify statements, in source order. -/
190def btOrder (s : DeflateStatePtr) (desc : TreeDescPtr) (tree : CtDataPtr) (mc : Int32) : M Unit := do
191  stTreeDesc desc { (← ldTreeDesc desc) with max_code := mc }
192  let _ ← btHeapify s tree
193
194/-- The maximum-symbol write is an actual typed descriptor access. -/
195theorem ws_btSaveMax {h0 : Heap} {id : Nat} (dk : TK) (d : DeflateState) (mc : Int32) :
196    WS h0 id (do
197      stTreeDesc (some (dk.descRef id)) { (← ldTreeDesc (some (dk.descRef id))) with max_code := mc }) d
198      (fun _ e => e = dk.setDesc d { dk.getDesc d with max_code := mc }) := by
199  refine WS.of_eq (a := ()) (d' := dk.setDesc d { dk.getDesc d with max_code := mc }) ?_ rfl
200  cases dk <;> simp [TK.descRef, TK.setDesc, TK.getDesc, ldTreeDesc, stTreeDesc,
201    TreeDescRef.get, TreeDescRef.put, TreeDescRef.isRo, bind_app, setD, upd_upd]
202
203/-- The actual descriptor write followed by the complete heapify loop.
204The selected descriptor gets the exact maximum; the same used leaves remain
205in a heap ordered by the source comparison, with a minimal root. -/
206theorem ws_btOrder_leaf {h0 : Heap} {id : Nat} (tk dk : TK) (d : DeflateState) (N : Nat) (mc : Int32)
207    (hi : BTLeafInv tk N mc d) :
208    WS h0 id (btOrder (Sp id) (some (dk.descRef id)) (.ref (tk.ref id) 0) mc) d (fun _ e =>
209      BTLeafInv tk N mc e ∧ ∃ H : Array Int32,
210        e = { dk.setDesc d { dk.getDesc d with max_code := mc } with heap := H } ∧
211        H.size = d.heap.size ∧
212        (∀ i, ¬ (1 ≤ i ∧ i ≤ d.heap_len.toInt.toNat) → H[i]! = d.heap[i]!) ∧
213        PermOn (fun i => H[i]!) (fun i => d.heap[i]!) d.heap_len.toInt.toNat ∧
214        HeapOK (sm (tk.arr d) d.depth) (fun i => H[i]!) d.heap_len.toInt.toNat 0 ∧
215        (dk.descRef id).get (setD h0 id e) = some { dk.getDesc d with max_code := mc } ∧
216        ∀ q, 1 ≤ q → q ≤ d.heap_len.toInt.toNat → sm (tk.arr d) d.depth H[1]! H[q]! = true) := by
217  unfold btOrder
218  rw [← M_bind_assoc]
219  refine WS.bind' (ws_btSaveMax dk d mc) fun _ e1 he1 => ?_
220  subst e1
221  refine WS.bind' (ws_btHeapify_leaf tk _ N mc (hi.setDesc dk _))
222    fun n e ⟨hn, hleaf, H, he, hsH, hf, hp, ho, hmin⟩ => ?_
223  subst e
224  simp only [tk_arr_setDesc, tk_setDesc_depth, tk_setDesc_len, tk_setDesc_heap] at hsH hf hp ho hmin
225  refine WS.pure' ⟨hleaf, H, rfl, hsH, hf, hp, ho, ?_, hmin⟩
226  cases dk <;> simp [TK.descRef, TK.getDesc, TK.setDesc, TreeDescRef.get, setD]
227
228/-- The scan preserves descriptors and the merge-tail boundary. -/
229theorem BTScanInv.desc_heap_max {tk : TK} {d e : DeflateState} {N : Nat} {mc : Int32}
230    (hi : BTScanInv tk d N mc e) (dk : TK) :
231    dk.getDesc e = dk.getDesc d ∧ e.heap_max = d.heap_max := by
232  obtain ⟨T, H, D, hl, rfl, rest⟩ := hi
233  cases tk <;> cases dk <;> exact ⟨rfl, rfl⟩
234
235/-- The exact repair trace preserves descriptors and the merge-tail boundary. -/
236theorem BTForceTrace.desc_heap_max {tk : TK} {sl : Option (Nat → UInt16)}
237    {k : Nat} {mc0 mc : Int32} {d0 d : DeflateState}
238    (h : BTForceTrace tk sl k mc0 d0 mc d) (dk : TK) :
239    dk.getDesc d = dk.getDesc d0 ∧ d.heap_max = d0.heap_max := by
240  obtain ⟨T, H, D, hl, O, S, rfl⟩ := h.frame
241  cases tk <;> cases dk <;> exact ⟨rfl, rfl⟩
242
243end Zlib.Trees.Proofs