trees.c.build.order.lean

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

1import ZlibF.Proof.«trees.c.build.leaves»
2import ZlibF.Proof.«trees.c.build.heapify»
3
4/-! # trees.c: actual leaf preparation followed by heap ordering
5
6The existing leaf, heap and source-comparison facts are composed on one
7actual state. The residual suffix is named only for whole-function equality.
8No execution or correctness of that suffix is assumed.
9-/
10
11namespace Zlib.Trees.Proofs
12open C Zlib.Trees Zlib.Trees.Proofs.GB
13
14/-- Actual leaf preparation, descriptor maximum store and heap construction. -/
15def btSortedStart (s : DeflateStatePtr) (desc : TreeDescPtr) :
16    M (CtDataPtr × CtDataPtr × Int32 × Int32) := do
17  let (tree, stree, elems, mc) ← btLeavesStart s desc
18  btOrder s desc tree mc
19  pure (tree, stree, elems, mc)
20
21/-- The current source suffix after descriptor storage and heapify. -/
22def btAfterOrder (s : DeflateStatePtr) (desc : TreeDescPtr) (tree : CtDataPtr)
23    (elems max_code : Int32) : M Unit := do
24  -- node = elems;
25  -- do { ... } while (s->heap_len >= 2);
26  let _ ← cdoWhile (σ := Int32)
27    (fun node => do
28      -- pqremove(s, tree, n);  m = s->heap[SMALLEST];
29      let n ← pqremove s tree
30      let m ← heapAt s 1
31      -- s->heap[--(s->heap_max)] = n;  s->heap[--(s->heap_max)] = m;
32      let hm ← isub (← rd s).heap_max 1
33      md s fun d => { d with heap_max := hm }
34      heapSet s hm n
35      let hm ← isub (← rd s).heap_max 1
36      md s fun d => { d with heap_max := hm }
37      heapSet s hm m
38      -- tree[node].Freq = tree[n].Freq + tree[m].Freq;
39      let fn ← getFc tree n.toInt
40      let fm ← getFc tree m.toInt
41      setFc tree node.toInt (fn + fm)
42      -- s->depth[node] = (uch)((s->depth[n] >= s->depth[m] ? s->depth[n] : s->depth[m]) + 1);
43      let dp ← pDepth s
44      let dn ← Ptr.index dp n.toInt
45      let dm ← Ptr.index dp m.toInt
46      let mx ← if dn ≥ dm then Ptr.index dp n.toInt else Ptr.index dp m.toInt
47      setAt dp node.toInt (mx + 1)
48      -- tree[n].Dad = tree[m].Dad = (ush)node;
49      setDl tree m.toInt (i2us node)
50      setDl tree n.toInt (i2us node)
51      -- s->heap[SMALLEST] = node++;
52      heapSet s 1 node
53      let node' ← iadd node 1
54      pqdownheap s tree 1
55      pure node')
56    (fun node => do pure (decide ((← rd s).heap_len.toInt ≥ 2), node))
57    elems
58  -- s->heap[--(s->heap_max)] = s->heap[SMALLEST];
59  let top ← heapAt s 1
60  let hm ← isub (← rd s).heap_max 1
61  md s fun d => { d with heap_max := hm }
62  heapSet s hm top
63  -- gen_bitlen(s, (tree_desc *)desc);
64  gen_bitlen s desc
65  -- gen_codes ((ct_data *)tree, max_code, s->bl_count);
66  gen_codes tree max_code (← pBlCount s)
67
68/-- The actual leaf suffix begins with the named descriptor/heapify code. -/
69theorem btAfterLeaves_eq_order (s : DeflateStatePtr) (desc : TreeDescPtr)
70    (tree : CtDataPtr) (elems mc : Int32) :
71    btAfterLeaves s desc tree elems mc = (do
72      btOrder s desc tree mc
73      btAfterOrder s desc tree elems mc) := by
74  simp only [btAfterLeaves, btOrder, btHeapify, btAfterOrder, M_bind_assoc, M_pure_bind] <;> rfl
75
76/-- Complete actual-function equality retains the whole ordered prefix. -/
77theorem build_tree_eq_order (s : DeflateStatePtr) (desc : TreeDescPtr) :
78    build_tree s desc = (do
79      let (tree, _stree, elems, mc) ← btSortedStart s desc
80      btAfterOrder s desc tree elems mc) := by
81  rw [build_tree_eq_leaves]
82  simp only [btSortedStart, M_bind_assoc, M_pure_bind, btAfterLeaves_eq_order] <;> rfl
83
84/-- The actual scan invariant retains the sizes of the two arrays needed
85for internal-node creation. -/
86theorem BTScanInv.merge_sizes {tk : TK} {d e : DeflateState} {N : Nat} {mc : Int32}
87    (hi : BTScanInv tk d N mc e) :
88    (tk.arr e).size = (tk.arr d).size ∧ e.depth.size = d.depth.size := by
89  obtain ⟨T, H, D, hl, rfl, hT, hH, hD, rest⟩ := hi
90  exact ⟨by simpa only [btScanState_tree] using hT, hD⟩
91
92/-- Every actual dummy-leaf update retains both array sizes. -/
93theorem BTForceTrace.merge_sizes {tk : TK} {sl : Option (Nat → UInt16)}
94    {k : Nat} {mc0 mc : Int32} {d0 d : DeflateState} (hi : BTForceTrace tk sl k mc0 d0 mc d) :
95    (tk.arr d).size = (tk.arr d0).size ∧ d.depth.size = d0.depth.size := by
96  induction hi with
97  | nil => exact ⟨rfl, rfl⟩
98  | snoc node hl before hn hnT hm hhl ih =>
99    simpa only [btForceState_tree, btForceState_depth, size_set!] using ih
100
101
102/-- The complete actual prefix before merging: descriptors are read, the
103heap is reset, symbols are scanned, the alphabet is repaired, its maximum is
104stored, and the heap is constructed. It establishes the full live-leaf
105representation, heap order and root minimality on the same actual heap.
106No old length, depth, heap length or heap-order premise is required. -/
107theorem ws_btSortedStart {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
108    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc} {sl : Option (Nat → UInt16)}
109    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
110    (hsd : StaticTreeDescRef.get h0 sref = some sd)
111    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
112    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
113    (hT : sd.elems.toInt ≤ (tk.arr d).size) (hD : sd.elems.toInt ≤ d.depth.size)
114    (hH : d.heap.size = 573) (hs : BTStatic h0 id sd.static_tree sd.elems.toInt.toNat sl) :
115    WS h0 id (btSortedStart (Sp id) (some (dk.descRef id))) d (fun a e =>
116      a.1 = .ref (tk.ref id) 0 ∧ a.2.1 = sd.static_tree ∧ a.2.2.1 = sd.elems ∧
117        BTLeafInv tk sd.elems.toInt.toNat a.2.2.2 e ∧ 2 ≤ e.heap_len.toInt ∧ e.heap_max = HEAP_SIZE ∧
118        (dk.descRef id).get (setD h0 id e) = some { dd with max_code := a.2.2.2 } ∧
119        HeapOK (sm (tk.arr e) e.depth) (fun q => e.heap[q]!) e.heap_len.toInt.toNat 0 ∧
120        ∀ q : Nat, 1 ≤ q → (q : Int) ≤ e.heap_len.toInt →
121          sm (tk.arr e) e.depth e.heap[1]! e.heap[q]! = true) := by
122  unfold btSortedStart
123  refine WS.bind' (ws_btLeavesStart hdd hsd hstat htree he3 he286 hT hD hH hs)
124    fun a mid ⟨ht, hst, he, hleaf, scan, scanMc, k, hscan, hlen, hk, hkexact, htrace⟩ => ?_
125  rcases a with ⟨tree, stree, elems, mc⟩
126  dsimp only at ht hst he hleaf htrace ⊢
127  subst tree; subst stree; subst elems
128  have hmid := htrace.desc_heap_max dk
129  have hscanframe := hscan.desc_heap_max dk
130  have hresetdesc : dk.getDesc { d with heap_len := 0, heap_max := HEAP_SIZE } = dk.getDesc d := by cases dk <;> rfl
131  have hddval : dk.getDesc d = dd := by
132    cases dk <;> simpa [TK.descRef, TK.getDesc, TreeDescRef.get, setD] using hdd
133  have hdesc : dk.getDesc mid = dd := hmid.1.trans (hscanframe.1.trans (hresetdesc.trans hddval))
134  have hmax : mid.heap_max = HEAP_SIZE := hmid.2.trans hscanframe.2
135  have htwo : 2 ≤ mid.heap_len.toInt := by omega
136  refine WS.bind' (ws_btOrder_leaf tk dk mid sd.elems.toInt.toNat mc hleaf)
137    fun _ e ⟨hleaf', H, he, hsH, hf, hp, ho, hdesc', hmin⟩ => ?_
138  subst e
139  have hmax' : (dk.setDesc mid { dk.getDesc mid with max_code := mc }).heap_max = HEAP_SIZE := by
140    cases dk <;> exact hmax
141  refine WS.pure' ⟨rfl, rfl, rfl, hleaf', ?_, ?_, ?_, ?_, ?_⟩
142  · simp only [tk_setDesc_len]; exact htwo
143  · exact hmax'
144  · simpa only [hdesc] using hdesc'
145  · cases tk <;> cases dk <;> exact ho
146  · intro q hq1 hq2
147    simp only [tk_setDesc_len] at hq2
148    have hmin' := hmin q hq1 (by omega)
149    cases tk <;> cases dk <;> exact hmin'
150
151/-- The complete actual leaf prefix preserves internal-node array capacity.
152This supplements the already proved leaf/order result with a separate exact
153frame property. -/
154theorem ws_btSortedStart_sizes {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
155    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc} {sl : Option (Nat → UInt16)}
156    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
157    (hsd : StaticTreeDescRef.get h0 sref = some sd)
158    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
159    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
160    (hT : sd.elems.toInt ≤ (tk.arr d).size) (hD : sd.elems.toInt ≤ d.depth.size)
161    (hH : d.heap.size = 573) (hs : BTStatic h0 id sd.static_tree sd.elems.toInt.toNat sl) :
162    WS h0 id (btSortedStart (Sp id) (some (dk.descRef id))) d (fun _ e =>
163      (tk.arr e).size = (tk.arr d).size ∧ e.depth.size = d.depth.size) := by
164  unfold btSortedStart
165  refine WS.bind' (ws_btLeavesStart hdd hsd hstat htree he3 he286 hT hD hH hs)
166    fun a mid ⟨ht, hst, he, hleaf, scan, scanMc, k, hscan, hlen, hk, hkexact, htrace⟩ => ?_
167  rcases a with ⟨tree, stree, elems, mc⟩
168  dsimp only at ht hst he hleaf htrace ⊢
169  subst tree; subst stree; subst elems
170  have hsz := htrace.merge_sizes
171  have hsz0 := hscan.merge_sizes
172  have ht0 : tk.arr { d with heap_len := 0, heap_max := HEAP_SIZE } = tk.arr d := by cases tk <;> rfl
173  rw [ht0] at hsz0
174  have htMid : (tk.arr mid).size = (tk.arr d).size := hsz.1.trans hsz0.1
175  have hdMid : mid.depth.size = d.depth.size := hsz.2.trans hsz0.2
176  refine WS.bind' (ws_btOrder_leaf tk dk mid sd.elems.toInt.toNat mc hleaf)
177    fun _ e ⟨hleaf', H, he, hsH, hf, hp, ho, hdesc', hmin⟩ => ?_
178  subst e
179  refine WS.pure' ⟨?_, ?_⟩
180  · rw [tk_arr_heap, tk_arr_setDesc]
181    exact htMid
182  · cases dk <;> exact hdMid
183
184
185end Zlib.Trees.Proofs