trees.c.build.complete.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Proof.«trees.c.build.tail»
2import ZlibF.Proof.«trees.c.build.forest»
3
4/-! # trees.c: deriving the code-generation context from actual tree building -/
5
6namespace Zlib.Trees.Proofs
7open C Zlib.Trees
8
9/-- Readable static descriptor data for tree construction. These are storage
10and table-value facts for all symbols in the alphabet. No execution or
11called-function specification is a field of this representation. -/
12structure BTBuildStatic (h0 : Heap) (id : Nat) (sd : StaticTreeDesc)
13    (xb : Nat → Nat) (slOpt : Option (Nat → Nat)) : Prop where
14  base_nonneg : 0 ≤ sd.extra_base.toInt
15  length_pos : 1 ≤ sd.max_length.toInt
16  length_limit : sd.max_length.toInt ≤ 15
17  length_capacity : sd.elems.toInt.toNat ≤ 2 ^ sd.max_length.toInt.toNat
18  extra : ∀ n < sd.elems.toInt.toNat,
19    (sd.extra_base.toInt.toNat ≤ n → ∃ (r : IRef) (ex : Array Int32), sd.extra_bits = .ref r 0 ∧
20      (∀ e, Space.get (setD h0 id e) r = some ex) ∧ n - sd.extra_base.toInt.toNat < ex.size ∧
21      0 ≤ ex[n - sd.extra_base.toInt.toNat]!.toInt ∧ ex[n - sd.extra_base.toInt.toNat]!.toInt ≤ 1000 ∧
22      xb n = ex[n - sd.extra_base.toInt.toNat]!.toInt.toNat) ∧
23    (n < sd.extra_base.toInt.toNat → xb n = 0)
24  static : (sd.static_tree = .null ∧ slOpt = none) ∨
25    ∃ (r : CtDataRef) (st : Array CtData) (sl : Nat → Nat), sd.static_tree = .ref r 0 ∧ slOpt = some sl ∧
26      (∀ e, Space.get (setD h0 id e) r = some st) ∧
27      ∀ n < sd.elems.toInt.toNat, n < st.size ∧ st[n]!.dl.toNat ≤ 15 ∧ sl n = st[n]!.dl.toNat
28
29/-- The static table facts also supply the representation used by the actual
30two-leaf repair. Its source reads 16-bit lengths without changing the table. -/
31theorem BTBuildStatic.repair {h0 : Heap} {id : Nat} {sd : StaticTreeDesc}
32    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)} (hs : BTBuildStatic h0 id sd xb slOpt) :
33    ∃ sl : Option (Nat → UInt16), BTStatic h0 id sd.static_tree sd.elems.toInt.toNat sl := by
34  rcases hs.static with ⟨ht, hsl⟩ | ⟨r, st, sl, ht, hsl, hr, hvals⟩
35  · exact ⟨none, Or.inl ⟨ht, rfl⟩⟩
36  · exact ⟨some (fun n => st[n]!.dl), Or.inr ⟨r, st, (fun n => st[n]!.dl), ht, rfl, hr,
37      fun n hn => ⟨(hvals n hn).1, rfl⟩⟩⟩
38
39/-- The precise bit-length context is derived from the built tree layout and
40static table data. All dynamic shape, parent and maximum-symbol facts come
41from actual tree building. -/
42theorem BTBuilt.bitlen_ctx {h0 : Heap} {id : Nat} {tk : TK} {d0 d : DeflateState}
43    {N K : Nat} {mc : Int32} {sd : StaticTreeDesc} {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
44    (hi : BTBuilt tk N K mc d0 d) (hs : BTBuildStatic h0 id sd xb slOpt)
45    (hN : sd.elems.toInt.toNat = N) (hB : d.bl_count.size = 16) (hT : (tk.arr d).size ≤ 600) :
46    P1Ctx h0 id tk d sd.static_tree sd.extra_bits mc sd.extra_base sd.max_length
47      (574 - 2 * K) (K - 1) N mc.toInt.toNat sd.max_length.toInt.toNat sd.extra_base.toInt.toNat xb slOpt := by
48  have hL1 := hs.length_pos
49  have hL15 := hs.length_limit
50  have hb := hs.base_nonneg
51  have hmc := hi.shape.maxc_lt
52  have hK2 := hi.k2
53  refine ⟨hi.heap, hB, hi.nonneg, hi.shape, by have := hi.capacity; omega, hT,
54    by have := hi.max_nonneg; omega, by omega, by omega, by omega, by omega, ?_, ?_, ?_⟩
55  · intro i hiB
56    exact hi.parent (574 - 2 * K + 1 + i) (by omega) (by have := hi.shape.hm_eq; omega)
57  · intro n hn
58    exact hs.extra n (by omega)
59  · rcases hs.static with hnull | ⟨r, st, sl, ht, hsl, hr, hv⟩
60    · exact Or.inl hnull
61    · exact Or.inr ⟨r, st, sl, ht, hsl, hr, fun n hn => hv n (by omega)⟩
62
63/-- The scan preserves the bit-count array in addition to its recorded sizes. -/
64theorem BTScanInv.bl_count {tk : TK} {d e : DeflateState} {N : Nat} {mc : Int32}
65    (hi : BTScanInv tk d N mc e) : e.bl_count = d.bl_count := by
66  obtain ⟨T, H, D, hl, rfl, rest⟩ := hi
67  cases tk <;> rfl
68
69/-- Every actual repair update preserves the bit-count array. -/
70theorem BTForceTrace.bl_count {tk : TK} {sl : Option (Nat → UInt16)}
71    {k : Nat} {mc0 mc : Int32} {d0 d : DeflateState} (hi : BTForceTrace tk sl k mc0 d0 mc d) :
72    d.bl_count = d0.bl_count := by
73  obtain ⟨T, H, D, hl, O, S, rfl⟩ := hi.frame
74  cases tk <;> rfl
75
76/-- The complete actual leaf preparation and heapify retain the bit-count
77array. This supplements the checked prefix with a separate frame property. -/
78theorem ws_btSortedStart_bl_count {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
79    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc} {sl : Option (Nat → UInt16)}
80    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
81    (hsd : StaticTreeDescRef.get h0 sref = some sd)
82    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
83    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
84    (hT : sd.elems.toInt ≤ (tk.arr d).size) (hD : sd.elems.toInt ≤ d.depth.size)
85    (hH : d.heap.size = 573) (hs : BTStatic h0 id sd.static_tree sd.elems.toInt.toNat sl) :
86    WS h0 id (btSortedStart (Sp id) (some (dk.descRef id))) d (fun _ e => e.bl_count = d.bl_count) := by
87  unfold btSortedStart
88  refine WS.bind' (ws_btLeavesStart hdd hsd hstat htree he3 he286 hT hD hH hs)
89    fun a mid ⟨ht, hst, he, hleaf, scan, scanMc, k, hscan, hlen, hk, hkexact, htrace⟩ => ?_
90  rcases a with ⟨tree, stree, elems, mc⟩
91  dsimp only at ht hst he hleaf htrace ⊢
92  subst tree; subst stree; subst elems
93  have hB : mid.bl_count = d.bl_count := htrace.bl_count.trans hscan.bl_count
94  refine WS.bind' (ws_btOrder_leaf tk dk mid sd.elems.toInt.toNat mc hleaf)
95    fun _ e ⟨hleaf', H, he, hsH, hf, hp, ho, hdesc', hmin⟩ => ?_
96  subst e
97  refine WS.pure' ?_
98  cases dk <;> exact hB
99
100/-- A descriptor field read is its record projection on this heap. -/
101theorem bt_desc_get (dk : TK) (h0 : Heap) (id : Nat) (d : DeflateState) :
102    (dk.descRef id).get (setD h0 id d) = some (dk.getDesc d) := by
103  cases dk <;> simp [TK.descRef, TK.getDesc, TreeDescRef.get, setD]
104
105/-- Complete actual heap construction establishes the retained tree layout
106and keeps the descriptor maximum and count-array storage. All dynamic
107representation premises for merging come from actual leaf preparation. -/
108theorem ws_btHeap_built {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
109    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc} {sl : Option (Nat → UInt16)}
110    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
111    (hsd : StaticTreeDescRef.get h0 sref = some sd)
112    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
113    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
114    (hT : 2 * sd.elems.toInt.toNat - 1 ≤ (tk.arr d).size) (hTbig : (tk.arr d).size ≤ 600)
115    (hD : 2 * sd.elems.toInt.toNat - 1 ≤ d.depth.size)
116    (hH : d.heap.size = 573) (hB : d.bl_count.size = 16)
117    (hs : BTStatic h0 id sd.static_tree sd.elems.toInt.toNat sl) :
118    WS h0 id (btHeap (Sp id) (some (dk.descRef id))) d (fun a e =>
119      a.1 = .ref (tk.ref id) 0 ∧ ∃ (prepared : DeflateState) (K : Nat),
120        BTBuilt tk sd.elems.toInt.toNat K a.2 prepared e ∧
121        (dk.descRef id).get (setD h0 id e) = some { dd with max_code := a.2 } ∧
122        e.bl_count.size = 16 ∧ (tk.arr e).size ≤ 600) := by
123  have hT0 : sd.elems.toInt ≤ (tk.arr d).size := by omega
124  have hD0 : sd.elems.toInt ≤ d.depth.size := by omega
125  unfold btHeap btMergedStart
126  simp only [M_bind_assoc, M_pure_bind]
127  refine WS.bind' (merge_ws_and (merge_ws_and
128    (ws_btSortedStart hdd hsd hstat htree he3 he286 hT0 hD0 hH hs)
129    (ws_btSortedStart_sizes hdd hsd hstat htree he3 he286 hT0 hD0 hH hs))
130    (ws_btSortedStart_bl_count hdd hsd hstat htree he3 he286 hT0 hD0 hH hs))
131    fun a prepared ⟨⟨⟨ht, hst, he, hleaf, h2, hm, hdesc, ho, hmin⟩, hTs, hDs⟩, hBs⟩ => ?_
132  rcases a with ⟨tree, stree, elems, mc⟩
133  dsimp only at ht hst he hleaf hdesc ⊢
134  subst tree; subst stree; subst elems
135  have hcnt := hleaf.count
136  have hKN := Math.scanCount_le (btFreq tk prepared) sd.elems.toInt.toNat
137  have hI := BTForest.of_leaf hleaf h2 hm (node := sd.elems) (by omega)
138    (by rw [hTs]; omega) (by rw [hDs]; omega) ho
139  refine WS.bind' (ws_btMergeLoop_forest hI) fun next merged ⟨hforest, hframe, hlen⟩ => ?_
140  refine WS.bind' (ws_btSaveRoot_forest hforest hframe) fun _ e hbuilt => ?_
141  have hmeta := hbuilt.frame.metadata dk
142  have hDesc : dk.getDesc prepared = { dd with max_code := mc } :=
143    Option.some.inj ((bt_desc_get dk h0 id prepared).symm.trans hdesc)
144  have hDesc' : (dk.descRef id).get (setD h0 id e) = some { dd with max_code := mc } := by
145    rw [bt_desc_get, hmeta.1, hDesc]
146  have heB : e.bl_count.size = 16 := by rw [hmeta.2, hBs]; exact hB
147  have heT : (tk.arr e).size = (tk.arr prepared).size := by
148    obtain ⟨T, H, D, hl, hm, he, hT, hH, hD⟩ := hbuilt.frame
149    rw [he]
150    cases tk <;> exact hT
151  exact WS.pure' ⟨rfl, prepared, prepared.heap_len.toInt.toNat, hbuilt, hDesc', heB, by rw [heT, hTs]; exact hTbig⟩
152
153/-- The complete actual build_tree executes through length limiting and
154canonical code assignment. Its dynamic tree context is established by the
155actual prefix. Preconditions concern explicit internal storage and static
156tables, not assumed specifications of any called function. This is a local
157construction result; public caller reachability, emission and compression
158correctness are separate obligations. -/
159theorem ws_build_tree_complete {h0 : Heap} {id : Nat} {tk dk : TK} {d : DeflateState}
160    {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc}
161    {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
162    (hdd : (dk.descRef id).get (setD h0 id d) = some dd)
163    (hsd : StaticTreeDescRef.get h0 sref = some sd)
164    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = .ref (tk.ref id) 0)
165    (he3 : 3 ≤ sd.elems.toInt) (he286 : sd.elems.toInt ≤ 286)
166    (hT : 2 * sd.elems.toInt.toNat - 1 ≤ (tk.arr d).size) (hTbig : (tk.arr d).size ≤ 600)
167    (hD : 2 * sd.elems.toInt.toNat - 1 ≤ d.depth.size)
168    (hH : d.heap.size = 573) (hB : d.bl_count.size = 16)
169    (hs : BTBuildStatic h0 id sd xb slOpt) :
170    WS h0 id (build_tree (Sp id) (some (dk.descRef id))) d (fun _ e =>
171      ∃ (prepared built mid : DeflateState) (mc : Int32) (K : Nat),
172        BTBuilt tk sd.elems.toInt.toNat K mc prepared built ∧
173        GBDone tk built (574 - 2 * K) (K - 1) mc.toInt.toNat sd.max_length.toInt.toNat xb slOpt mid ∧
174        ∃ a : Array CtData, e = tk.setArr mid a ∧ a.size = (tk.arr mid).size ∧
175          ∀ i < a.size, a[i]! =
176            if i < (mc.toInt + 1).toNat ∧ (tk.arr mid)[i]!.dl ≠ 0 then
177              { (tk.arr mid)[i]! with fc := UInt16.ofNat (Math.storedCode
178                (fun b => mid.bl_count[b]!.toNat) (fun v => (tk.arr mid)[v]!.dl.toNat) i) }
179            else (tk.arr mid)[i]!) := by
180  obtain ⟨sl, hsRepair⟩ := hs.repair
181  rw [build_tree_eq_heap_codes]
182  refine WS.bind' (ws_btHeap_built hdd hsd hstat htree he3 he286 hT hTbig hD hH hB hsRepair)
183    fun a built ⟨ht, prepared, K, hbuilt, hdesc, hBs, hTs⟩ => ?_
184  rcases a with ⟨tree, mc⟩
185  dsimp only at ht hbuilt hdesc ⊢
186  subst tree
187  have hctx := hbuilt.bitlen_ctx hs rfl hBs hTs
188  have hcodes := ws_btCodes (h0 := h0) (id := id) (tk := tk) (d := built)
189    (r := dk.descRef id) (sref := sref) (dd := { dd with max_code := mc }) (sd := sd)
190    (hm := 574 - 2 * K) (J := K - 1) (elems := sd.elems.toInt.toNat) (maxc := mc.toInt.toNat)
191    (L := sd.max_length.toInt.toNat) (baseN := sd.extra_base.toInt.toNat) (xb := xb) (slOpt := slOpt)
192    hdesc hsd hstat htree hctx hbuilt.heap_max hs.length_capacity (by omega) hbuilt.unused
193  refine WS.mono hcodes ?_
194  intro _ e ⟨mid, hdone, hcode⟩
195  exact ⟨prepared, built, mid, mc, K, hbuilt, hdone, hcode⟩
196
197end Zlib.Trees.Proofs