inftrees.c.content.data.lean

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

1import ZlibF.Proof.«inftrees.c.content.codes»
2import ZlibF.Math.InflateTableCoverage
3import ZlibF.Proof.«inftrees.c.cover.leaf»
4
5/-! The actual constructor's retained leaves and links establish decoder
6table safety for complete literal/length and distance alphabets. -/
7
8namespace Zlib.Inftrees.Proofs
9open C Zlib.Inftrees Zlib.Inftrees.Spec Zlib.Inftrees.Canon Zlib.Inffast.Spec
10set_option autoImplicit false
11
12theorem Env.completeCode (e : Env) (complete : Kc e.f e.n 15 = 2 ^ 15) :
13    CompleteCode e.ls e.R e.mx := by
14  refine ⟨?_, Cover.complete_of_Kc complete, e.h_R1, e.h_Rmx, ?_, ?_⟩
15  · change 0 < Canon.nz (lensOf e.f e.n)
16    rw [Zlib.Inftrees.Proofs.nz_eq]
17    exact e.h_pos
18  · change mxl e.f e.n = Canon.L (lensOf e.f e.n) (Canon.nz (lensOf e.f e.n) - 1)
19    rw [Zlib.Inftrees.Proofs.nz_eq, L_eq e.f e.n (by have := e.h_pos; omega)]
20    rfl
21  · change Canon.L (lensOf e.f e.n) 0 ≤ e.R
22    rw [L_eq e.f e.n e.h_pos]
23    exact e.h_R0
24
25private theorem hereC_lens_leaf {c : Ctx} {w : UInt16} {bits : UInt8} {drop : Nat}
26    (base : c.base = lbase) (extra : c.extra = lext) (matchValue : c.match_ = 257)
27    (symbol : w.toNat < 288) (bitBound : bits.toNat + drop ≤ 15) :
28    LenLeaf drop (hereC c w bits) := by
29  have word : w.toUInt32.toNat = w.toNat := UInt16.toNat_toUInt32 w
30  have succ : (w.toUInt32 + 1).toNat = w.toNat + 1 := by
31    rw [u32_succ (by rw [word]; omega), word]
32  have storedBits : (hereC c w bits).bits = bits := by
33    unfold hereC
34    split <;> (try split) <;> rfl
35  apply Cover.lenLeaf_of drop w.toNat symbol _ (by rw [storedBits]; exact bitBound)
36  · intro literal
37    have test : w.toUInt32 + 1 < c.match_ := by
38      rw [matchValue]
39      apply UInt32.lt_iff_toNat_lt.mpr
40      rw [succ]
41      change w.toNat + 1 < 257
42      omega
43    simp only [hereC, test, ite_true]
44  · intro endBlock
45    have test : ¬ w.toUInt32 + 1 < c.match_ := by
46      rw [matchValue]
47      rw [UInt32.lt_iff_toNat_lt, succ]
48      change ¬ w.toNat + 1 < 257
49      omega
50    have test2 : ¬ w.toUInt32 ≥ c.match_ := by
51      change ¬ c.match_ ≤ w.toUInt32
52      rw [matchValue, UInt32.le_iff_toNat_le, word]
53      change ¬ 257 ≤ w.toNat
54      omega
55    simp only [hereC, test, test2, ite_false]
56  · intro length
57    have test : ¬ w.toUInt32 + 1 < c.match_ := by
58      rw [matchValue, UInt32.lt_iff_toNat_lt, succ]
59      change ¬ w.toNat + 1 < 257
60      omega
61    have test2 : c.match_ ≤ w.toUInt32 := by
62      rw [matchValue, UInt32.le_iff_toNat_le, word]
63      exact length
64    have index : (w.toUInt32 - c.match_).toNat = w.toNat - 257 := by
65      rw [UInt32.toNat_sub_of_le _ _ test2, word, matchValue]
66      rfl
67    simp only [hereC, test, test2, ite_false, ite_true, extra, base, index,
68      Array.getElem!_eq_getD]
69    exact ⟨rfl, rfl⟩
70
71private theorem hereC_dist_leaf {c : Ctx} {w : UInt16} {bits : UInt8} {drop : Nat}
72    (base : c.base = dbase) (extra : c.extra = dext) (matchValue : c.match_ = 0)
73    (symbol : w.toNat < 32) (bitBound : bits.toNat + drop ≤ 15) :
74    DistLeaf drop (hereC c w bits) := by
75  have storedBits : (hereC c w bits).bits = bits := by
76    unfold hereC
77    split <;> (try split) <;> rfl
78  apply Cover.distLeaf_of drop w.toNat symbol _ (by rw [storedBits]; exact bitBound)
79  simp only [hereC, matchValue, UInt32.not_lt_zero, ite_false, UInt32.zero_le,
80    ite_true, UInt32.sub_zero, UInt16.toNat_toUInt32, extra, base,
81    Array.getElem!_eq_getD]
82  exact ⟨rfl, rfl⟩
83
84theorem here_data_leaf_of_drop {e : Env} {j : Nat} (index : j < e.m)
85    (dropBound : (e.D j).drop ≤ Canon.L e.ls j)
86    (lengthBound : Canon.L e.ls j ≤ 15) :
87    (e.c.type = LENS → LenLeaf (e.D j).drop (e.here j)) ∧
88    (e.c.type = DISTS → DistLeaf (e.D j).drop (e.here j)) := by
89  have bits : ((Canon.L e.ls j - (e.D j).drop).toUInt8).toNat + (e.D j).drop ≤ 15 := by
90    rw [UInt8.toNat_ofNat', Nat.mod_eq_of_lt (by omega)]
91    omega
92  have symbol := ws_getD_lt index
93  have word : (UInt16.ofNat ((wsAux e.f e.n 15).getD j 0)).toNat =
94      (wsAux e.f e.n 15).getD j 0 := by
95    rw [UInt16.toNat_ofNat', Nat.mod_eq_of_lt (by have := e.h_n; omega)]
96  constructor
97  · intro type
98    obtain ⟨count, base, extra, matchValue⟩ := e.h_lens' type
99    exact hereC_lens_leaf base extra matchValue (by rw [word]; omega) bits
100  · intro type
101    obtain ⟨count, base, extra, matchValue⟩ := e.h_dists type
102    exact hereC_dist_leaf base extra matchValue (by rw [word]; omega) bits
103
104theorem here_data_leaf {e : Env} (code : CompleteCode e.ls e.R e.mx)
105    {j : Nat} (index : j < e.m) :
106    (e.c.type = LENS → LenLeaf (e.D j).drop (e.here j)) ∧
107    (e.c.type = DISTS → DistLeaf (e.D j).drop (e.here j)) := by
108  have listIndex : j < Canon.nz e.ls := by
109    change j < Canon.nz (lensOf e.f e.n)
110    rwa [Zlib.Inftrees.Proofs.nz_eq]
111  have fits := desc_fits code listIndex
112  have length := Canon.L_interval e.ls listIndex
113  have dropBound : (e.D j).drop ≤ Canon.L e.ls j := fits.1
114  have lengthBound : Canon.L e.ls j ≤ 15 := length.2.1
115  exact here_data_leaf_of_drop index dropBound lengthBound
116
117private theorem getD_of_written {ca : Array Code} {i : Nat} {value : Code}
118    (get : ca[i]? = some value) : ca.getD i default = value := by
119  simp only [Array.getD_eq_getD_getElem?, get, Option.getD_some]
120
121private theorem size_of_entry {ca : Array Code} {i : Nat} {value : Code}
122    (get : ca[i]? = some value) : i < ca.size := by
123  by_cases inside : i < ca.size
124  · exact inside
125  · rw [Array.getElem?_eq_none (by omega)] at get
126    contradiction
127
128private theorem complete_data_table {e : Env} {ca : Array Code}
129    (complete : Kc e.f e.n 15 = 2 ^ 15)
130    (written : Written e e.m ca) (links : Links e e.m ca)
131    (P : Nat → Code → Prop) (L : Code → Prop) [DecidablePred L]
132    (leaves : ∀ j, j < e.m → P (e.D j).drop (e.here j) ∧ ¬ L (e.here j))
133    (linkTest : ∀ a, 1 ≤ a → a < e.m → Canon.startsAt e.ls e.R (a - 1) → L (e.link a)) :
134    TableSafe P L ca e.oc e.R := by
135  have code := e.completeCode complete
136  have listIndex : ∀ j, j < e.m ↔ j < Canon.nz e.ls := by
137    intro j
138    change j < Tc e.f e.n 15 ↔ j < Canon.nz (lensOf e.f e.n)
139    rw [Zlib.Inftrees.Proofs.nz_eq]
140  have rootEntries : ∀ cell, cell < 2 ^ e.R →
141      ∃ value, ca[e.oc + cell]? = some value ∧
142        (if L value then LinkOK P ca e.oc value else P 0 value) := by
143    intro cell inside
144    rcases Cover.root_cover_complete_fn e.h_fits complete
145        (Nat.le_trans code.root_le code.mx_le) inside with
146      ⟨j, short, _, _⟩ | ⟨⟨j, long⟩, _⟩
147    · have shortList := (Cover.shortAt_iff e.f e.n e.R cell j).mpr short
148      obtain ⟨replica, bound, address⟩ := short_root_replica (mx := e.mx)
149        shortList.1 shortList.2.1 inside shortList.2.2
150      have get := written j short.1 replica bound
151      change gAddr e.ls e.R e.mx j replica = cell at address
152      rw [address] at get
153      have leaf := leaves j short.1
154      have drop : (e.D j).drop = 0 := by
155        change (Canon.desc e.ls e.R e.mx j).drop = 0
156        rw [Canon.desc_short e.ls shortList.1 shortList.2.1]
157        rfl
158      exact ⟨e.here j, get, by rw [ite_eq_right leaf.2, ← drop]; exact leaf.1⟩
159    · have longList := (Cover.longAt_iff e.f e.n e.R cell j).mpr long
160      have jIndex : j < e.m := long.1
161      obtain ⟨a, order, start, group, drop, width, _⟩ :=
162        desc_long (mx := e.mx) code.min_le longList.1 longList.2.1
163      have startIndex : a + 1 < e.m := by have := long.1; omega
164      have aList : a + 1 < Canon.nz e.ls := (listIndex _).mp startIndex
165      have aLong : e.R < Canon.L e.ls (a + 1) := start.1
166      have get := links (a + 1) (by omega) (by omega) startIndex
167        (by simpa only [Nat.add_sub_cancel] using start)
168      have slot : gSlot e.ls e.R (a + 1) = cell := by
169        unfold gSlot
170        rw [group]
171        rw [← Canon.H_mod_root e.ls (root := e.R) longList.1 (Nat.le_of_lt longList.2.1)]
172        exact longList.2.2
173      rw [slot] at get
174      have dsame : e.D (a + 1) = e.D j :=
175        desc_same_group aList longList.1 aLong longList.2.1 group
176      have info := width_spec e.ls aList code.mx_le aLong (code.L_le_mx aList)
177      have op : ((Canon.width e.ls (a + 1) e.R e.mx).toUInt8).toNat =
178          Canon.width e.ls (a + 1) e.R e.mx := by
179        rw [UInt8.toNat_ofNat', Nat.mod_eq_of_lt (by have := code.mx_le; omega)]
180      have root : (e.R.toUInt8).toNat = e.R := by
181        rw [UInt8.toNat_ofNat', Nat.mod_eq_of_lt (by have := code.mx_le; have := code.root_le; omega)]
182      have base : ((e.D (a + 1)).base.toUInt16).toNat = (e.D (a + 1)).base := by
183        rw [UInt16.toNat_ofNat']
184        exact Nat.mod_eq_of_lt (desc_base_lt_u16 code aList)
185      have test := linkTest (a + 1) (by omega) startIndex (by simpa only [Nat.add_sub_cancel] using start)
186      refine ⟨e.link (a + 1), get, ?_⟩
187      rw [ite_eq_left test]
188      change (e.R.toUInt8).toNat ≤ 15 ∧ _
189      rw [root]
190      dsimp only [Env.link]
191      rw [root, op, base]
192      have localEntries : ∀ t, t < 2 ^ Canon.width e.ls (a + 1) e.R e.mx →
193          ∃ j', j' < e.m ∧ (e.D j').drop = e.R ∧
194            ca[e.oc + (e.D (a + 1)).base + t]? = some (e.here j') := by
195        intro t bounded
196        have dc : (e.D (a + 1)).curr = Canon.width e.ls (a + 1) e.R e.mx := by
197          change (desc e.ls e.R e.mx (a + 1)).curr = _
198          rw [desc_succ_of_starts e.ls e.R e.mx a start]
199        obtain ⟨j', replica, member, same, repBound, address⟩ := long_subtable_replica
200          code aList aLong (by change t < 2 ^ (e.D (a + 1)).curr; rw [dc]; exact bounded)
201        have value := written j' ((listIndex _).mpr member) replica repBound
202        rw [address, ← Nat.add_assoc] at value
203        refine ⟨j', (listIndex _).mpr member, ?_, value⟩
204        change (Canon.desc e.ls e.R e.mx j').drop = e.R
205        rw [same, desc_succ_of_starts e.ls e.R e.mx a start]
206      have final := localEntries (2 ^ Canon.width e.ls (a + 1) e.R e.mx - 1)
207        (by have := Nat.two_pow_pos (Canon.width e.ls (a + 1) e.R e.mx); omega)
208      obtain ⟨last, _, _, lastGet⟩ := final
209      have arrayBound := size_of_entry lastGet
210      refine ⟨by have := code.mx_le; have := code.root_le; omega,
211        by omega, by have := code.mx_le; omega, by omega, ?_⟩
212      intro t bounded
213      obtain ⟨j', member, drop, value⟩ := localEntries t bounded
214      rw [getD_of_written value, ← drop]
215      exact (leaves j' member).1
216  have positive := Nat.two_pow_pos e.R
217  obtain ⟨last, lastGet, _⟩ := rootEntries (2 ^ e.R - 1) (by omega)
218  have arrayBound := size_of_entry lastGet
219  refine ⟨Nat.le_trans code.root_le code.mx_le, by omega, ?_⟩
220  intro cell inside
221  obtain ⟨value, get, safe⟩ := rootEntries cell inside
222  rwa [getD_of_written get]
223
224private theorem low_link_flags (op : UInt8) (lo : 1 ≤ op.toNat) (hi : op.toNat ≤ 15) :
225    op ≠ 0 ∧ op &&& 16 = 0 ∧ op &&& 64 = 0 := by
226  have all : ∀ n : Fin 256, let op := UInt8.ofNat n.val
227      1 ≤ op.toNat → op.toNat ≤ 15 →
228      op ≠ 0 ∧ op &&& 16 = 0 ∧ op &&& 64 = 0 := by decide +kernel
229  have result := all ⟨op.toNat, op.toNat_lt⟩
230  dsimp only at result
231  rw [UInt8.ofNat_toNat] at result
232  exact result lo hi
233
234private theorem actual_link_flags {e : Env} (code : CompleteCode e.ls e.R e.mx)
235    {a : Nat} (positive : 1 ≤ a) (index : a < e.m)
236    (start : Canon.startsAt e.ls e.R (a - 1)) :
237    LenLink (e.link a) ∧ DistLink (e.link a) := by
238  have listIndex : a < Canon.nz e.ls := by rw [e.nz_eq]; exact index
239  have long : e.R < Canon.L e.ls a := by
240    have := start.1
241    simpa only [show a - 1 + 1 = a by omega] using this
242  have info := width_spec e.ls listIndex code.mx_le long (code.L_le_mx listIndex)
243  have op : ((Canon.width e.ls a e.R e.mx).toUInt8).toNat = Canon.width e.ls a e.R e.mx := by
244    rw [UInt8.toNat_ofNat', Nat.mod_eq_of_lt (by have := code.mx_le; omega)]
245  have flags := low_link_flags (Canon.width e.ls a e.R e.mx).toUInt8
246    (by rw [op]; omega) (by rw [op]; have := code.mx_le; omega)
247  exact ⟨flags, flags.2⟩
248
249/-- The complete length alphabet's actual written cells meet the decoder
250predicate. No premise about the unused part or size of the caller array
251is needed: cell presence supplies the bounds. -/
252theorem complete_len_table_of_content {e : Env} {ca : Array Code}
253    (type : e.c.type = LENS) (complete : Kc e.f e.n 15 = 2 ^ 15)
254    (written : Written e e.m ca) (links : Links e e.m ca) :
255    LenTableSafe ca e.oc e.R := by
256  have code := e.completeCode complete
257  apply complete_data_table complete written links LenLeaf LenLink
258  · intro j index
259    have leaf := (here_data_leaf code index).1 type
260    refine ⟨leaf, ?_⟩
261    rintro ⟨nonzero, bit16, bit64⟩
262    rcases leaf.2 with literal | length | invalid
263    · exact nonzero literal
264    · exact length.1 bit16
265    · exact invalid.2 bit64
266  · intro a positive index start
267    exact (actual_link_flags code positive index start).1
268
269/-- The complete distance alphabet includes the reserved invalid symbols;
270the translated dbase/dext entries supply their exact leaf flags. -/
271theorem complete_dist_table_of_content {e : Env} {ca : Array Code}
272    (type : e.c.type = DISTS) (complete : Kc e.f e.n 15 = 2 ^ 15)
273    (written : Written e e.m ca) (links : Links e e.m ca) :
274    DistTableSafe ca e.oc e.R := by
275  have code := e.completeCode complete
276  apply complete_data_table complete written links DistLeaf DistLink
277  · intro j index
278    have leaf := (here_data_leaf code index).2 type
279    refine ⟨leaf, ?_⟩
280    rintro ⟨bit16, bit64⟩
281    rcases leaf.2 with distance | invalid
282    · exact distance.1 bit16
283    · exact invalid.2 bit64
284  · intro a positive index start
285    exact (actual_link_flags code positive index start).2
286
287/-- `int inflate_table(codetype type, unsigned short *lens, unsigned codes,
288code **table, unsigned *bits, unsigned short *work)`.
289For a complete input alphabet, actual successful construction establishes
290the decoder predicates for the exact returned heap and width. Capacity
291errors remain included. The explicit complete-alphabet premise excludes
292the empty and accepted incomplete single-symbol cases, which need their
293final invalid-cell writes retained separately. This is not the full
294Goal.inflate_table_decoder_safe. -/
295theorem inflate_table_complete_decoder_safe
296    {h : Heap} {type : UInt32} {rl rw : WRef} {ol ow oc : Nat} {codes bits : UInt32} {rc : CodeRef}
297    (pre : CallPre h type rl ol codes rc oc bits rw ow)
298    (complete : Kc pre.f codes.toNat 15 = 2 ^ 15) :
299    ∃ result after,
300      C.run (inflate_table type (.ref rl ol) codes (.ref rc oc) bits (.ref rw ow)) h =
301        .ok (result, after) ∧
302      Result h rw rc ow oc (capOf type) codes.toNat pre.wa pre.ca (.ref rc oc) bits result after ∧
303      (result.1 = 0 → ∃ ca : Array Code, Space.get after rc = some ca ∧
304        1 ≤ result.2.2.toNat ∧ result.2.2.toNat ≤ 15 ∧
305        (type = CODES → CodeLengthTableSafe ca oc result.2.2.toNat) ∧
306        (type = LENS → LenTableSafe ca oc result.2.2.toNat) ∧
307        (type = DISTS → DistTableSafe ca oc result.2.2.toNat)) := by
308  by_cases codeLength : type = CODES
309  · subst type
310    obtain ⟨result, after, run, frame, safe⟩ := inflate_table_codes_decoder_safe pre
311    refine ⟨result, after, run, frame, ?_⟩
312    intro success
313    obtain ⟨ca, get, table⟩ := safe success
314    refine ⟨ca, get, table.1, by have := table.2.1; omega, fun _ => table, ?_, ?_⟩
315    · intro impossible
316      cases impossible
317    · intro impossible
318      cases impossible
319  · obtain ⟨result, after, run, frame, _, content⟩ :=
320      inflate_table_content h type rl ol codes rc oc bits rw ow pre
321    refine ⟨result, after, run, frame, ?_⟩
322    intro success
323    rcases content success with ⟨empty, _⟩ |
324      ⟨_, e, ca, function, count, width, reference, offset, kind, get, written, links⟩
325    · have zero : Kc pre.f codes.toNat 15 = 0 := by
326        have gap := Kc_gap (f := pre.f) (n := codes.toNat) 0 15 (by simpa [Tc] using empty)
327        simpa [Kc] using gap
328      omega
329    · have full : Kc e.f e.n 15 = 2 ^ 15 := by rw [function, count]; exact complete
330      have code := e.completeCode full
331      refine ⟨ca, get, ?_, ?_, ?_, ?_, ?_⟩
332      · rw [← width]
333        exact e.h_R1
334      · rw [← width]
335        exact Nat.le_trans code.root_le code.mx_le
336      · intro impossible
337        exact False.elim (codeLength impossible)
338      · intro lens
339        rw [← offset, ← width]
340        exact complete_len_table_of_content (kind.trans lens) full written links
341      · intro dists
342        rw [← offset, ← width]
343        exact complete_dist_table_of_content (kind.trans dists) full written links
344
345end Zlib.Inftrees.Proofs