trees.c.build.tail.lean

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

1import ZlibF.Proof.«deflate.c.engine.loops»
2import ZlibF.Proof.«trees.c.heap.gbtop»
3import ZlibF.Proof.«trees.c.codes»
4import ZlibF.Proof.«trees.c.build.order»
5import ZlibF.Proof.«trees.c.build.force»
6import ZlibF.Proof.«trees.c.build.heapify»
7import ZlibF.Proof.«trees.c.build.merge»
8
9/-!
10# trees.c: the heap-building prefix and the code-assignment suffix
11
12The prefix copies the actual translation in source order. The suffix uses
13proved executions of both callees, rather than assumed callee contracts.
14-/
15
16namespace Zlib.Trees.Proofs
17open C Zlib.Trees Zlib.Trees.Proofs.GB
18
19/-- The actual ordered leaf prefix followed by the full merge loop. -/
20def btMergedStart (s : DeflateStatePtr) (desc : TreeDescPtr) : M (CtDataPtr × Int32) := do
21  let (tree, _stree, elems, mc) ← btSortedStart s desc
22  let _ ← btMergeLoop s tree elems
23  pure (tree, mc)
24
25/-- `build_tree` up to the root heap store. -/
26def btHeap (s : DeflateStatePtr) (desc : TreeDescPtr) : M (CtDataPtr × Int32) := do
27  let (tree, max_code) ← btMergedStart s desc
28  -- s->heap[--(s->heap_max)] = s->heap[SMALLEST];
29  btSaveRoot s
30  pure (tree, max_code)
31
32/-- The final two calls of `build_tree`, verbatim. -/
33def btCodes (s : DeflateStatePtr) (desc : TreeDescPtr) (tree : CtDataPtr) (max_code : Int32) : M Unit := do
34  gen_bitlen s desc
35  gen_codes tree max_code (← pBlCount s)
36
37set_option maxHeartbeats 1000000 in
38/-- Naming the two source fragments leaves the actual function unchanged. -/
39theorem build_tree_eq_heap_codes (s : DeflateStatePtr) (desc : TreeDescPtr) :
40    build_tree s desc = (do
41      let (tree, max_code) ← btHeap s desc
42      btCodes s desc tree max_code) := by
43  simp only [build_tree, btHeap, btMergedStart, btSortedStart, btLeavesStart, btScanStart, btScan, btScanBody, btForce, btForceBody, btOrder, btHeapify, btMergeBody, btPick2, btCodes, M_bind_assoc, M_pure_bind]
44  unfold btSaveRoot btMergeLoop btMergeBody btMergeOpen btPick2 btKeepChildren btMakeParent btSetFreq btSetDepth btSetParents btMergeClose
45  simp only [M_bind_assoc, M_pure_bind, merge_ite_bind]
46  rfl
47
48/-- The actual descriptor/reset/scan/repair/heapify prefix and full merging
49loop compose on one heap. Array capacity is an explicit internal storage
50condition. Every queue representation premise is established by the actual
51prefix, rather than assumed as a called function contract. Tree-layout,
52parent-link and inactive-symbol bridges to bit-length generation remain open. -/
53theorem ws_btMergedStart {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
54    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc} {sl : Option (Nat → UInt16)}
55    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
56    (hsd : StaticTreeDescRef.get h0 sref = some sd)
57    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
58    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
59    (hT : 2 * sd.elems.toInt.toNat - 1 ≤ (tk.arr d).size)
60    (hD : 2 * sd.elems.toInt.toNat - 1 ≤ d.depth.size)
61    (hH : d.heap.size = 573) (hs : BTStatic h0 id sd.static_tree sd.elems.toInt.toNat sl) :
62    WS h0 id (btMergedStart (Sp id) (some (dk.descRef id))) d (fun a e =>
63      a.1 = .ref (tk.ref id) 0 ∧ ∃ (K : Nat) (next : Int32),
64        BTMergeQueue tk sd.elems.toInt.toNat K (K - 1) next e ∧ e.heap_len.toInt = 1) := by
65  have hT0 : sd.elems.toInt ≤ (tk.arr d).size := by omega
66  have hD0 : sd.elems.toInt ≤ d.depth.size := by omega
67  unfold btMergedStart
68  refine WS.bind' (merge_ws_and
69    (ws_btSortedStart hdd hsd hstat htree he3 he286 hT0 hD0 hH hs)
70    (ws_btSortedStart_sizes hdd hsd hstat htree he3 he286 hT0 hD0 hH hs))
71    fun a mid ⟨⟨ht, hst, he, hleaf, h2, hm, hdesc, ho, hmin⟩, hTs, hDs⟩ => ?_
72  rcases a with ⟨tree, stree, elems, mc⟩
73  dsimp only at ht hst he hleaf hdesc ⊢
74  subst tree; subst stree; subst elems
75  have hcnt := hleaf.count
76  have hKN := Math.scanCount_le (btFreq tk mid) sd.elems.toInt.toNat
77  have hI := BTMergeQueue.of_leaf hleaf h2 hm (node := sd.elems) (by omega)
78    (by rw [hTs]; omega) (by rw [hDs]; omega) ho
79  refine WS.bind' (ws_btMergeLoop hI) fun next e he => ?_
80  exact WS.pure' ⟨rfl, mid.heap_len.toInt.toNat, next, he⟩
81
82/-- The complete actual heap-building prefix, including the final root
83store, ends without a fault. The postcondition retains its pre-store queue
84and the exact root-store effect. This does not assert the still-open tree
85shape or parent-link contract needed by bit-length generation. -/
86theorem ws_btHeap {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
87    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc} {sl : Option (Nat → UInt16)}
88    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
89    (hsd : StaticTreeDescRef.get h0 sref = some sd)
90    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
91    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
92    (hT : 2 * sd.elems.toInt.toNat - 1 ≤ (tk.arr d).size)
93    (hD : 2 * sd.elems.toInt.toNat - 1 ≤ d.depth.size)
94    (hH : d.heap.size = 573) (hs : BTStatic h0 id sd.static_tree sd.elems.toInt.toNat sl) :
95    WS h0 id (btHeap (Sp id) (some (dk.descRef id))) d (fun a e =>
96      a.1 = .ref (tk.ref id) 0 ∧ ∃ (K : Nat) (next hm : Int32) (before : DeflateState),
97        BTMergeQueue tk sd.elems.toInt.toNat K (K - 1) next before ∧ before.heap_len.toInt = 1 ∧
98        hm.toInt = before.heap_max.toInt - 1 ∧
99        e = { before with heap := before.heap.set! hm.toInt.toNat before.heap[1]!, heap_max := hm } ∧
100        e.heap.size = 573 ∧ e.heap[hm.toInt.toNat]! = before.heap[1]! ∧
101        ∀ i : Nat, i ≠ hm.toInt.toNat → e.heap[i]! = before.heap[i]!) := by
102  unfold btHeap
103  refine WS.bind' (ws_btMergedStart hdd hsd hstat htree he3 he286 hT hD hH hs)
104    fun a before ⟨ht, K, next, hi, hlen⟩ => ?_
105  rcases a with ⟨tree, mc⟩
106  dsimp only at ht ⊢
107  subst tree
108  have hmax := hi.max
109  have hsize := hi.heap
110  have hK2 := hi.k2
111  have hKN := hi.kN
112  have hNb := hi.n286
113  refine WS.bind' (ws_btSaveRoot before (by omega) (by omega) (by omega) (by omega))
114    fun _ e ⟨hm, hhm, he, hsH, htop, hframe⟩ => ?_
115  exact WS.pure' ⟨rfl, K, next, hm, before, hi, hlen, hhm, he, hsH.trans hsize, htop, hframe⟩
116
117/-- The actual bit-length result supplies all length and count-array bounds
118needed by code assignment. Symbols absent from the heap have the zero length
119written by the first `build_tree` scan. -/
120theorem GBDone.code_inputs {tk : TK} {d e : DeflateState}
121    {hm J elems maxc L : Nat} {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
122    (shape : PShape (Hn d) hm J elems maxc) (hfit : elems ≤ (tk.arr d).size)
123    (hL : L ≤ 15)
124    (hzero : ∀ v ≤ maxc, (∀ q, hm ≤ q → q < 573 → Hn d q ≠ v) → ((tk.arr d)[v]!).dl = 0)
125    (done : GBDone tk d hm J maxc L xb slOpt e) :
126    e.bl_count.size = 16 ∧ maxc + 1 ≤ (tk.arr e).size ∧
127      ∀ v ≤ maxc, ((tk.arr e)[v]!).dl.toNat ≤ 15 := by
128  obtain ⟨T, B, O, S, rfl, hsz, hbsz, hfreq, hout, hlengths, rest⟩ := done
129  simp only [mkP1_bl_count, tk_arr_mkP1]
130  refine ⟨hbsz, by have := shape.maxc_lt; omega, ?_⟩
131  intro v hv
132  by_cases hseen : ∃ q, hm ≤ q ∧ q < 573 ∧ Hn d q = v
133  · obtain ⟨q, hq1, hq2, hqv⟩ := hseen
134    have hqne : q ≠ hm := by
135      intro heq; subst q
136      have hr := shape.root
137      have hj := shape.J1
138      have hc := shape.maxc_lt
139      omega
140    have hidx : q - hm - 1 < 2 * J := by have := shape.hm_eq; omega
141    have hq : hm + 1 + (q - hm - 1) = q := by omega
142    have hl := (hlengths (q - hm - 1) hidx (by rw [hq, hqv]; exact hv)).2
143    rw [hq, hqv] at hl
144    exact Nat.le_trans hl hL
145  · have hnone : ∀ q, hm ≤ q → q < 573 → Hn d q ≠ v := by
146      intro q hq1 hq2 heq
147      exact hseen ⟨q, hq1, hq2, heq⟩
148    rw [hout v hnone, hzero v hv hnone]
149    decide
150
151/-- The actual final two calls compose on one heap. The length limit and
152count-array size passed to `gen_codes` are conclusions of `gen_bitlen`.
153The zero-length condition concerns only symbols absent from the heap; the
154first scan establishes it. No callee specification appears as a hypothesis. -/
155theorem ws_btCodes {h0 : Heap} {id : Nat} {tk : TK} {d : DeflateState}
156    {r : TreeDescRef} {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc}
157    {hm J elems maxc L baseN : Nat} {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
158    (hdd : r.get (setD h0 id d) = some dd) (hsd : StaticTreeDescRef.get h0 sref = some sd)
159    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
160    (ctx : P1Ctx h0 id tk d sd.static_tree sd.extra_bits dd.max_code sd.extra_base sd.max_length
161      hm J elems maxc L baseN xb slOpt)
162    (hHM : d.heap_max.toInt = hm) (hel : elems ≤ 2 ^ L) (helem : elems ≤ 286)
163    (hzero : ∀ v ≤ maxc, (∀ q, hm ≤ q → q < 573 → Hn d q ≠ v) → ((tk.arr d)[v]!).dl = 0) :
164    WS h0 id (btCodes (Sp id) (some r) (.ref (tk.ref id) 0) dd.max_code) d
165      (fun _ e => ∃ mid : DeflateState, GBDone tk d hm J maxc L xb slOpt mid ∧
166        ∃ a : Array CtData, e = tk.setArr mid a ∧ a.size = (tk.arr mid).size ∧
167          ∀ j < a.size, a[j]! =
168            if j < (dd.max_code.toInt + 1).toNat ∧ ((tk.arr mid)[j]!).dl ≠ 0 then
169              { (tk.arr mid)[j]! with fc := UInt16.ofNat (Math.storedCode
170                (fun i => mid.bl_count[i]!.toNat) (fun i => ((tk.arr mid)[i]!).dl.toNat) j) }
171            else (tk.arr mid)[j]!) := by
172  unfold btCodes
173  refine WS.bind' (ws_gen_bitlen hdd hsd hstat htree ctx hHM hel) fun _ mid hdone => ?_
174  have hfit : elems ≤ (tk.arr d).size := by have := ctx.nc; omega
175  obtain ⟨hbsz, hsize, hlengths⟩ := hdone.code_inputs ctx.shape hfit ctx.L15 hzero
176  have hm : dd.max_code.toInt = maxc := ctx.mcv
177  have hmc : maxc < elems := ctx.shape.maxc_lt
178  have hrange : (dd.max_code.toInt + 1).toNat = maxc + 1 := by omega
179  refine WS.bind' ws_pBlCount fun p e1 ⟨hp, he1⟩ => ?_
180  subst e1; subst p
181  refine WS.mono (ws_gen_codes mid tk dd.max_code (by omega) (by omega) (by omega)
182    (by rw [hrange]; exact hsize) ?_) ?_
183  · intro j hj
184    exact hlengths j (by rw [hrange] at hj; omega)
185  · intro _ e he
186    exact ⟨mid, hdone, he⟩
187
188end Zlib.Trees.Proofs