trees.c.build.leaves.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.force»
2import ZlibF.Proof.«trees.c.heap.gbtop»
3
4/-! # trees.c: actual descriptor/reset/scan/repair prefix
5
6The two prefix definitions and execution statements retain their saved
7statements. The suffix is copied from current main only to check the complete
8source decomposition; no safety or correctness of that suffix is assumed.
9-/
10
11namespace Zlib.Trees.Proofs
12open C Zlib.Trees Zlib.Trees.Proofs.GB
13
14/-- The actual descriptor reads, heap reset and first symbol scan. -/
15def btScanStart (s : DeflateStatePtr) (desc : TreeDescPtr) :
16    M (CtDataPtr × CtDataPtr × Int32 × Int32) := do
17  let dd ← ldTreeDesc desc
18  let tree := dd.dyn_tree
19  let sd ← ldStaticTreeDesc dd.stat_desc
20  let stree := sd.static_tree
21  let elems := sd.elems
22  md s fun d => { d with heap_len := 0 }
23  md s fun d => { d with heap_max := HEAP_SIZE }
24  let max_code ← btScan s tree elems
25  pure (tree, stree, elems, max_code.2)
26
27/-- The actual scan followed by the actual two-leaf repair. -/
28def btLeavesStart (s : DeflateStatePtr) (desc : TreeDescPtr) :
29    M (CtDataPtr × CtDataPtr × Int32 × Int32) := do
30  let (tree, stree, elems, mc) ← btScanStart s desc
31  let mc ← btForce s tree stree mc
32  pure (tree, stree, elems, mc)
33
34/-- The unchanged main suffix after leaf preparation, in source order.
35This definition names code; it does not assert a callee specification. -/
36def btAfterLeaves (s : DeflateStatePtr) (desc : TreeDescPtr) (tree : CtDataPtr)
37    (elems max_code : Int32) : M Unit := do
38  -- desc->max_code = max_code;
39  stTreeDesc desc { (← ldTreeDesc desc) with max_code := max_code }
40  -- for (n = s->heap_len/2; n >= 1; n--) pqdownheap(s, tree, n);
41  let _ ← cfor (σ := Int32) (fun n => pure (decide (n.toInt ≥ 1))) (fun n => isub n 1)
42    (fun n => do pqdownheap s tree n; pure n) ((← rd s).heap_len / 2)
43  -- node = elems;
44  -- do { ... } while (s->heap_len >= 2);
45  let _ ← cdoWhile (σ := Int32)
46    (fun node => do
47      -- pqremove(s, tree, n);  m = s->heap[SMALLEST];
48      let n ← pqremove s tree
49      let m ← heapAt s 1
50      -- s->heap[--(s->heap_max)] = n;  s->heap[--(s->heap_max)] = m;
51      let hm ← isub (← rd s).heap_max 1
52      md s fun d => { d with heap_max := hm }
53      heapSet s hm n
54      let hm ← isub (← rd s).heap_max 1
55      md s fun d => { d with heap_max := hm }
56      heapSet s hm m
57      -- tree[node].Freq = tree[n].Freq + tree[m].Freq;
58      let fn ← getFc tree n.toInt
59      let fm ← getFc tree m.toInt
60      setFc tree node.toInt (fn + fm)
61      -- s->depth[node] = (uch)((s->depth[n] >= s->depth[m] ? s->depth[n] : s->depth[m]) + 1);
62      let dp ← pDepth s
63      let dn ← Ptr.index dp n.toInt
64      let dm ← Ptr.index dp m.toInt
65      let mx ← if dn ≥ dm then Ptr.index dp n.toInt else Ptr.index dp m.toInt
66      setAt dp node.toInt (mx + 1)
67      -- tree[n].Dad = tree[m].Dad = (ush)node;
68      setDl tree m.toInt (i2us node)
69      setDl tree n.toInt (i2us node)
70      -- s->heap[SMALLEST] = node++;
71      heapSet s 1 node
72      let node' ← iadd node 1
73      pqdownheap s tree 1
74      pure node')
75    (fun node => do pure (decide ((← rd s).heap_len.toInt ≥ 2), node))
76    elems
77  -- s->heap[--(s->heap_max)] = s->heap[SMALLEST];
78  let top ← heapAt s 1
79  let hm ← isub (← rd s).heap_max 1
80  md s fun d => { d with heap_max := hm }
81  heapSet s hm top
82  -- gen_bitlen(s, (tree_desc *)desc);
83  gen_bitlen s desc
84  -- gen_codes ((ct_data *)tree, max_code, s->bl_count);
85  gen_codes tree max_code (← pBlCount s)
86
87/-- Complete actual-function equality independently ties the proved prefix
88to main. No statement in the residual suffix is reordered or dropped. -/
89theorem build_tree_eq_leaves (s : DeflateStatePtr) (desc : TreeDescPtr) :
90    build_tree s desc = (do
91      let (tree, _stree, elems, max_code) ← btLeavesStart s desc
92      btAfterLeaves s desc tree elems max_code) := by
93  simp only [build_tree, btLeavesStart, btScanStart, btScan, btScanBody,
94    btForce, btForceBody, btAfterLeaves, M_bind_assoc, M_pure_bind]
95  rfl
96
97/-- The actual start of `build_tree` establishes the scan invariant. Neither
98the old heap length, the old depths nor the old code lengths are restricted.
99Both heap-control writes preceding the scan execute on the actual heap. -/
100theorem ws_btScanStart {h0 : Heap} {id : Nat} {tk : TK} {d : DeflateState}
101    {r : TreeDescRef} {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc}
102    (hdd : r.get (setD h0 id d) = some dd) (hsd : StaticTreeDescRef.get h0 sref = some sd)
103    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
104    (he0 : 0 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
105    (hT : sd.elems.toInt ≤ (tk.arr d).size) (hD : sd.elems.toInt ≤ d.depth.size)
106    (hH : d.heap.size = 573) :
107    WS h0 id (btScanStart (Sp id) (some r)) d (fun a e =>
108      a.1 = .ref (tk.ref id) 0 ∧ a.2.1 = sd.static_tree ∧ a.2.2.1 = sd.elems ∧
109        BTScanInv tk { d with heap_len := 0, heap_max := HEAP_SIZE } sd.elems.toInt.toNat a.2.2.2 e) := by
110  unfold btScanStart
111  refine WS.bind' (ws_ldTreeDesc r dd hdd) fun dd' e1 ⟨hdd', he1⟩ => ?_
112  subst e1; subst dd'
113  rw [hstat]
114  refine WS.bind' (ws_ldStaticTreeDesc sref sd hsd) fun sd' e1 ⟨hsd', he1⟩ => ?_
115  subst e1; subst sd'
116  rw [htree]
117  refine WS.bind' (ws_md (fun e => { e with heap_len := 0 })) fun _ e1 he1 => ?_
118  subst e1
119  refine WS.bind' (ws_md (fun e => { e with heap_max := HEAP_SIZE })) fun _ e1 he1 => ?_
120  subst e1
121  let d0 : DeflateState := { d with heap_len := 0, heap_max := HEAP_SIZE }
122  have ht0 : tk.arr d0 = tk.arr d := by cases tk <;> rfl
123  refine WS.bind' (ws_btScan tk d0 sd.elems he0 he286 (by rw [ht0]; exact hT)
124    hD (by change sd.elems.toInt < (d.heap.size : Int); omega)
125    (by change d.heap.size ≤ 573; omega) rfl) fun a e ⟨hn, hi⟩ => ?_
126  exact WS.pure' ⟨rfl, rfl, rfl, hi⟩
127
128/-- The actual descriptor/reset/scan/repair prefix establishes the live leaf
129representation needed by heap construction. Every repair premise comes from
130the actual scan result. The postcondition retains the exact intermediate
131scan state and the repair's bounded update trace and final heap length. -/
132theorem ws_btLeavesStart {h0 : Heap} {id : Nat} {tk : TK} {d : DeflateState}
133    {r : TreeDescRef} {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc}
134    {sl : Option (Nat → UInt16)}
135    (hdd : r.get (setD h0 id d) = some dd) (hsd : StaticTreeDescRef.get h0 sref = some sd)
136    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
137    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
138    (hT : sd.elems.toInt ≤ (tk.arr d).size) (hD : sd.elems.toInt ≤ d.depth.size)
139    (hH : d.heap.size = 573) (hs : BTStatic h0 id sd.static_tree sd.elems.toInt.toNat sl) :
140    WS h0 id (btLeavesStart (Sp id) (some r)) d (fun a e =>
141      a.1 = .ref (tk.ref id) 0 ∧ a.2.1 = sd.static_tree ∧ a.2.2.1 = sd.elems ∧
142        BTLeafInv tk sd.elems.toInt.toNat a.2.2.2 e ∧
143          ∃ (mid : DeflateState) (mc : Int32) (k : Nat),
144            BTScanInv tk { d with heap_len := 0, heap_max := HEAP_SIZE } sd.elems.toInt.toNat mc mid ∧
145            e.heap_len.toInt = max 2 mid.heap_len.toInt ∧ k ≤ 2 ∧
146            k = (2 - mid.heap_len.toInt).toNat ∧ BTForceTrace tk sl k mc mid a.2.2.2 e) := by
147  unfold btLeavesStart
148  refine WS.bind' (ws_btScanStart hdd hsd hstat htree (by omega) he286 hT hD hH)
149    fun a mid ⟨ht, hst, he, hscan⟩ => ?_
150  rcases a with ⟨tree, stree, elems, mc⟩
151  dsimp only at ht hst he hscan ⊢
152  subst tree; subst stree; subst elems
153  let d0 : DeflateState := { d with heap_len := 0, heap_max := HEAP_SIZE }
154  have ht0 : tk.arr d0 = tk.arr d := by cases tk <;> rfl
155  have hleaf := BTLeafInv.of_scan hscan (by omega) (by omega)
156    (by change _ ≤ (tk.arr d0).size; rw [ht0]; omega) (by change _ ≤ d.depth.size; omega) hH
157  refine WS.bind' (ws_btForce tk mid mc sd.elems.toInt.toNat sd.static_tree sl hs hleaf)
158    fun mc' e ⟨hleaf', hlen, k, hk, hkexact, htrace⟩ => ?_
159  exact WS.pure' ⟨rfl, rfl, rfl, hleaf', mid, mc, k, hscan, hlen, hk, hkexact, htrace⟩
160
161
162end Zlib.Trees.Proofs