trees.c.build.static.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.complete»
2import ZlibF.Proof.«trees.c.inv»
3
4/-! # trees.c: the three installed static tree descriptors -/
5
6namespace Zlib.Trees.Proofs
7open C Zlib.Trees
8
9/-- The actual installed descriptor selected by a dynamic tree. -/
10def TK.buildDesc : TK → StaticTreeDesc
11  | .lit => (trees_statics default).static_l_desc
12  | .dist => (trees_statics default).static_d_desc
13  | .bl => (trees_statics default).static_bl_desc
14
15def TK.buildStaticRef : TK → StaticTreeDescRef
16  | .lit => .st_static_l_desc
17  | .dist => .st_static_d_desc
18  | .bl => .st_static_bl_desc
19
20/-- Extra-bit counts of the actual installed tables, including the literal
21prefix with no extra bits. -/
22def TK.buildExtra : TK → Nat → Nat
23  | .lit, n => if n < 257 then 0 else extra_lbits_tab[n - 257]!.toInt.toNat
24  | .dist, n => extra_dbits_tab[n]!.toInt.toNat
25  | .bl, n => extra_blbits_tab[n]!.toInt.toNat
26
27def TK.buildStaticLen : TK → Option (Nat → Nat)
28  | .lit => some (fun n => static_ltree_tab[n]!.dl.toNat)
29  | .dist => some (fun n => static_dtree_tab[n]!.dl.toNat)
30  | .bl => none
31
32/-- Installed descriptors are exactly the ones read by build_tree. -/
33theorem trees_build_desc_get {h : Heap} (hs : Out.TreesStatic h.static) (tk : TK) :
34    StaticTreeDescRef.get h tk.buildStaticRef = some tk.buildDesc := by
35  cases tk
36  · have he := congrArg Statics.static_l_desc hs
37    change some h.static.static_l_desc = _
38    rw [← he]
39    rfl
40  · have he := congrArg Statics.static_d_desc hs
41    change some h.static.static_d_desc = _
42    rw [← he]
43    rfl
44  · have he := congrArg Statics.static_bl_desc hs
45    change some h.static.static_bl_desc = _
46    rw [← he]
47    rfl
48
49set_option maxRecDepth 4096 in
50/-- Every static-data premise of the construction theorem holds for the
51actual installed tables. The finite value bounds are checked by the kernel. -/
52theorem trees_build_static {h0 : Heap} {id : Nat} (hs : Out.TreesStatic h0.static) (tk : TK) :
53    BTBuildStatic h0 id tk.buildDesc tk.buildExtra tk.buildStaticLen := by
54  have hL : ∀ i : Fin 29, 0 ≤ extra_lbits_tab[i.val]!.toInt ∧ extra_lbits_tab[i.val]!.toInt ≤ 1000 := by decide +kernel
55  have hD : ∀ i : Fin 30, 0 ≤ extra_dbits_tab[i.val]!.toInt ∧ extra_dbits_tab[i.val]!.toInt ≤ 1000 := by decide +kernel
56  have hB : ∀ i : Fin 19, 0 ≤ extra_blbits_tab[i.val]!.toInt ∧ extra_blbits_tab[i.val]!.toInt ≤ 1000 := by decide +kernel
57  have hSL : ∀ i : Fin 288, static_ltree_tab[i.val]!.dl.toNat ≤ 15 := by decide +kernel
58  have hSD : ∀ i : Fin 30, static_dtree_tab[i.val]!.dl.toNat ≤ 15 := by decide +kernel
59  cases tk
60  · refine ⟨by decide +kernel, by decide +kernel, by decide +kernel, by decide +kernel, ?_, ?_⟩
61    · intro n hn
62      change n < 286 at hn
63      constructor
64      · intro hbase
65        change 257 ≤ n at hbase
66        refine ⟨.st_extra_lbits, extra_lbits_tab, rfl, ?_, by change n - 257 < 29; omega, ?_, ?_, ?_⟩
67        · intro e
68          simp [Space.get, setD, hs.extra_lbits]
69        · exact (hL ⟨n - 257, by omega⟩).1
70        · exact (hL ⟨n - 257, by omega⟩).2
71        · simp only [TK.buildExtra, ite_eq_right (show ¬ n < 257 by omega)]
72          rfl
73      · intro hbase
74        change n < 257 at hbase
75        simp only [TK.buildExtra, hbase, ite_true]
76    · refine Or.inr ⟨.st_static_ltree, static_ltree_tab, (fun n => static_ltree_tab[n]!.dl.toNat), rfl, rfl, ?_, ?_⟩
77      · intro e
78        simp [Space.get, setD, hs.static_ltree]
79      · intro n hn
80        change n < 286 at hn
81        exact ⟨by change n < 288; omega, hSL ⟨n, by omega⟩, rfl⟩
82  · refine ⟨by decide +kernel, by decide +kernel, by decide +kernel, by decide +kernel, ?_, ?_⟩
83    · intro n hn
84      change n < 30 at hn
85      constructor
86      · intro hbase
87        refine ⟨.st_extra_dbits, extra_dbits_tab, rfl, ?_, ?_, ?_, ?_, ?_⟩
88        · intro e
89          simp [Space.get, setD, hs.extra_dbits]
90        · change n - 0 < 30; omega
91        · exact (hD ⟨n, hn⟩).1
92        · exact (hD ⟨n, hn⟩).2
93        · rfl
94      · intro hbase
95        change n < 0 at hbase
96        omega
97    · refine Or.inr ⟨.st_static_dtree, static_dtree_tab, (fun n => static_dtree_tab[n]!.dl.toNat), rfl, rfl, ?_, ?_⟩
98      · intro e
99        simp [Space.get, setD, hs.static_dtree]
100      · intro n hn
101        change n < 30 at hn
102        exact ⟨by change n < 30; exact hn, hSD ⟨n, hn⟩, rfl⟩
103  · refine ⟨by decide +kernel, by decide +kernel, by decide +kernel, by decide +kernel, ?_, Or.inl ⟨rfl, rfl⟩⟩
104    intro n hn
105    change n < 19 at hn
106    constructor
107    · intro hbase
108      refine ⟨.st_extra_blbits, extra_blbits_tab, rfl, ?_, ?_, ?_, ?_, ?_⟩
109      · intro e
110        simp [Space.get, setD, hs.extra_blbits]
111      · change n - 0 < 19; omega
112      · exact (hB ⟨n, hn⟩).1
113      · exact (hB ⟨n, hn⟩).2
114      · rfl
115    · intro hbase
116      change n < 0 at hbase
117      omega
118
119
120/-- Local construction result, retaining the built layout, actual bit-length
121result and exact canonical-code stores. Caller-to-input-frequency refinement
122and compressed-bit emission are separate obligations. -/
123def BTBuildResult (tk : TK) (N L : Nat) (xb : Nat → Nat) (slOpt : Option (Nat → Nat))
124    (e : DeflateState) : Prop :=
125  ∃ (prepared built mid : DeflateState) (mc : Int32) (K : Nat),
126    BTBuilt tk N K mc prepared built ∧
127    GBDone tk built (574 - 2 * K) (K - 1) mc.toInt.toNat L xb slOpt mid ∧
128    ∃ a : Array CtData, e = tk.setArr mid a ∧ a.size = (tk.arr mid).size ∧
129      ∀ i < a.size, a[i]! =
130        if i < (mc.toInt + 1).toNat ∧ (tk.arr mid)[i]!.dl ≠ 0 then
131          { (tk.arr mid)[i]! with fc := UInt16.ofNat (Math.storedCode
132            (fun b => mid.bl_count[b]!.toNat) (fun v => (tk.arr mid)[v]!.dl.toNat) i) }
133        else (tk.arr mid)[i]!
134
135/-- The state representation actually established by initialization supplies
136all tree-construction storage, descriptor and static-table premises for any
137of the three dynamic trees. Old frequencies, depths, lengths and heap
138contents are unrestricted. This is the local construction contract, not
139complete deflate correctness or a registered public goal. -/
140theorem ws_build_tree_initialized {h0 : Heap} {id : Nat} {d : DeflateState}
141    (tk : TK) (hwf : d.WellFormed) (hs : Out.TreesStatic h0.static) (hr : Out.TreesRun0 id d) :
142    WS h0 id (build_tree (Sp id) (some (tk.descRef id))) d (fun _ e =>
143      BTBuildResult tk tk.buildDesc.elems.toInt.toNat tk.buildDesc.max_length.toInt.toNat
144        tk.buildExtra tk.buildStaticLen e) := by
145  obtain ⟨hLT, hDT, hBT, hBC, hH, hD⟩ := hwf
146  have he3 : 3 ≤ tk.buildDesc.elems.toInt := by cases tk <;> decide +kernel
147  have he286 : tk.buildDesc.elems.toInt ≤ 286 := by cases tk <;> decide +kernel
148  have hT : 2 * tk.buildDesc.elems.toInt.toNat - 1 ≤ (tk.arr d).size := by
149    cases tk
150    · change 571 ≤ d.dyn_ltree.size; omega
151    · change 59 ≤ d.dyn_dtree.size; omega
152    · change 37 ≤ d.bl_tree.size; omega
153  have hTbig : (tk.arr d).size ≤ 600 := by
154    cases tk
155    · change d.dyn_ltree.size ≤ 600; omega
156    · change d.dyn_dtree.size ≤ 600; omega
157    · change d.bl_tree.size ≤ 600; omega
158  have hDepth : 2 * tk.buildDesc.elems.toInt.toNat - 1 ≤ d.depth.size := by
159    cases tk
160    · change 571 ≤ d.depth.size; omega
161    · change 59 ≤ d.depth.size; omega
162    · change 37 ≤ d.depth.size; omega
163  have hstat : (tk.getDesc d).stat_desc = some tk.buildStaticRef := by
164    cases tk
165    · exact hr.lstat
166    · exact hr.dstat
167    · exact hr.blstat
168  have htree : (tk.getDesc d).dyn_tree = .ref (tk.ref id) 0 := by
169    cases tk
170    · exact hr.ldyn
171    · exact hr.ddyn
172    · exact hr.bldyn
173  exact ws_build_tree_complete (bt_desc_get tk h0 id d) (trees_build_desc_get hs tk) hstat htree
174    he3 he286 hT hTbig hDepth hH hBC (trees_build_static hs tk)
175
176/-- The installed initialized-state theorem runs on the caller's actual
177heap, rather than a hypothetical replacement heap. The state and table
178representation is supplied by the existing actual initialization results. -/
179theorem build_tree_initialized {h : Heap} {id : Nat} {d : DeflateState}
180    (tk : TK) (hd : h.dstates id = some d) (hwf : d.WellFormed)
181    (hs : Out.TreesStatic h.static) (hr : Out.TreesRun0 id d) :
182    ∃ e : DeflateState, build_tree (Sp id) (some (tk.descRef id)) h = .ok ((), setD h id e) ∧
183      BTBuildResult tk tk.buildDesc.elems.toInt.toNat tk.buildDesc.max_length.toInt.toNat
184        tk.buildExtra tk.buildStaticLen e := by
185  obtain ⟨a, e, he, hresult⟩ := ws_build_tree_initialized tk hwf hs hr
186  have ha : a = () := Subsingleton.elim _ _
187  subst a
188  rw [setD_self hd] at he
189  exact ⟨e, he, hresult⟩
190
191end Zlib.Trees.Proofs