public-deflate-getdict.lean

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

1import ZlibF.Spec.Public.Lifecycle
2import ZlibF.Proof.«deflate.c.public-getdict»
3
4open C Zlib.Deflate Zlib.Deflate.Spec Zlib.Deflate.Proofs Zlib.Deflate.Engine.Proofs ZlibF.Spec.Public
5
6namespace ZlibF.Spec.Public.DeflateDictionaryProof
7
8/-- `int deflateGetDictionary(z_streamp strm, Bytef *dictionary, uInt *dictLength)`
9The exact public result, state, frame and ownership contract. -/
10theorem deflate_getdict_public : Goal.deflateGetDictionary := by
11  intro h r i z s dest hasLength xs hG hdict hdest
12  obtain ⟨w,p,q,b,hB⟩ := hG.inv.blocks
13  obtain ⟨wa,hwa,hwaSize⟩ := hB.wa
14  obtain ⟨src, off, a, hwindow, hget, hfit, hxs⟩ := hdict
15  rw [hB.win] at hwindow
16  cases hwindow
17  have ha : wa = a := Option.some.inj (hwa.symm.trans hget)
18  subst a
19  have hfill : s.strstart.toNat + s.lookahead.toNat ≤ s.window_size.toNat := by
20    have := hG.inv.wsz
21    simp at hfit
22    omega
23  have hws : s.w_size.toNat ≤ 32768 := by
24    have := hG.inv.wsize
25    have := hG.inv.wbits_hi
26    have := Nat.pow_le_pow_right (n := 2) (by decide) hG.inv.wbits_hi
27    omega
28  have hlen := dictLen_toNat hG.inv.wsz hws hfill
29  let n := (dictLen s).toNat
30  let start := s.strstart.toNat + s.lookahead.toNat - n
31  have hsource : start + n ≤ wa.size := by
32    dsimp [start,n]
33    simp at hfit
34    omega
35  have hxs' : xs = (wa.toList.drop start).take n := by
36    simpa [start,n,hlen,Nat.min_comm] using hxs
37  have hxslen : xs.length = n := by
38    rw [hxs']
39    simp only [List.length_take, List.length_drop, Array.length_toList]
40    omega
41  have hlength : UInt32.ofNat xs.length = dictLen s := by
42    apply UInt32.toNat_inj.mp
43    rw [hxslen]
44    simp [n]
45  by_cases hnone : dest = .null ∨ dictLen s = 0
46  · refine ⟨h, ?_, Or.inl ⟨?_,rfl⟩⟩
47    · simpa [C.run, hlength] using deflateGetDictionary_run_nocopy hG.live dest hasLength hnone
48    · rcases hnone with hn | hn
49      · simp [hn]
50      · have hzero : n = 0 := by simp [n, hn]
51        simp [hxs', hzero]
52  · have hnon : dest ≠ .null := fun e => hnone (Or.inl e)
53    have hnz : dictLen s ≠ 0 := fun e => hnone (Or.inr e)
54    obtain ⟨hwrite,hsep⟩ := hdest hnon
55    rcases hwrite with ⟨hn,_⟩ | ⟨rd,od,da,hd,hda,hro,hroom⟩
56    · exact (hnon hn).elim
57    · have hdroom : od + n ≤ da.size := by simpa [hxslen] using hroom
58      have hsep' : rd ≠ .blk w ∨ od + n ≤ start ∨ start + n ≤ od := by
59        simp [Separate, hd, hB.win, hxslen] at hsep
60        rcases hsep with h | h | h | h
61        · exact (hnz (UInt32.toNat_inj.mp (by simpa [n] using h))).elim
62        · have : s.window_size = 0 := UInt64.toNat_inj.mp (by simpa using h)
63          have := hG.inv.wsize
64          have := hG.inv.wbits_lo
65          have := hG.inv.wsz
66          have := Nat.pow_le_pow_right (n := 2) (by decide) hG.inv.wbits_lo
67          simp at this
68          omega
69        · exact Or.inl h
70        · exact Or.inr (Or.inr (by dsimp [start,n]; omega))
71      have hwaSize' : wa.size = s.window_size.toNat := by have := hG.inv.wsz; omega
72      have hrun := deflateGetDictionary_run_copy_general hG.live hB hfill dest hasLength hd hda hro hdroom hwa hlen hnz hsep' hwaSize'
73      refine ⟨Space.put h rd (copyRange da wa od start n), ?_, ?_⟩
74      · simpa [C.run, hlength] using hrun
75      · simp only [ite_eq_right hnon]
76        right
77        have hseg : xs.toArray = wa.extract start (start+n) := by
78          rw [hxs']
79          apply Array.toList_inj.mp
80          simp [Array.toList_extract, List.extract_eq_take_drop]
81        refine ⟨rd,od,da,hd,hda,hro,by simpa [hxslen] using hdroom, ?_⟩
82        rw [hseg, hxslen]
83        congr 1
84        exact copyRange_extract da wa od start n hdroom hsource
85
86#print axioms deflate_getdict_public
87
88end ZlibF.Spec.Public.DeflateDictionaryProof