public-inflate-getdict.lean

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

1import ZlibF.Spec.Public.Lifecycle
2import ZlibF.Proof.«inflate.c.public-getdict»
3
4open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs ZlibF.Spec.Public
5
6namespace ZlibF.Spec.Public.InflateDictionaryProof
7
8/-- `int inflateGetDictionary(z_streamp strm, Bytef *dictionary, uInt *dictLength)`
9The exact public result, state, frame and ownership contract. -/
10theorem inflate_getdict_public : Goal.inflateGetDictionary := by
11  intro h r i z s dest dl xs hG hdict hdest
12  have hwn : s.wnext.toNat ≤ s.whave.toNat := by
13    rcases Nat.lt_or_ge s.whave.toNat s.wsize.toNat with h | h
14    · have := hG.inv.win.eq h; omega
15    · have := hG.inv.win.wn; have := hG.inv.win.hv; omega
16  have hsub : (s.whave - s.wnext).toNat = s.whave.toNat - s.wnext.toNat :=
17    UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; exact hwn)
18  have hxslen : xs.length = s.whave.toNat := by
19    rcases hdict with ⟨hzero,rfl⟩ | ⟨rr,oo,aa,hwin,hget,hfit,hxs⟩
20    · simp [hzero]
21    · rw [hxs]
22      simp only [List.length_append, List.length_take, List.length_drop, Array.length_toList, hsub]
23      have hv := hG.inv.win.hv
24      omega
25  have hlength : UInt32.ofNat xs.length = s.whave := by
26    apply UInt32.toNat_inj.mp
27    rw [hxslen]
28    simp
29  by_cases hnone : dest = .null ∨ s.whave = 0
30  · refine ⟨h, ?_, Or.inl ⟨?_,rfl⟩⟩
31    · unfold C.run inflateGetDictionary
32      rcases hnone with hd | hw
33      · cases dl <;> simp [stateCheck_live hG.live, ldZ_eq, ldI_eq, hG.live.hz, hG.live.zst, castI, hG.live.hs, hd, hlength]
34      · cases dl <;> simp [stateCheck_live hG.live, ldZ_eq, ldI_eq, hG.live.hz, hG.live.zst, castI, hG.live.hs, hw, hlength]
35    · rcases hnone with hd | hw
36      · simp [hd]
37      · have : xs = [] := List.length_eq_zero_iff.mp (by simpa [hw] using hxslen)
38        simp [this]
39  · have hnon : dest ≠ .null := fun h => hnone (Or.inl h)
40    have hpos : s.whave ≠ 0 := fun h => hnone (Or.inr h)
41    have hposNat : 0 < s.whave.toNat := by
42      have : s.whave.toNat ≠ 0 := fun h => hpos (UInt32.toNat_inj.mp (by simpa using h))
43      omega
44    obtain ⟨w,a,hwin,ha,hro,hsize⟩ : ∃ w a, s.window = .ref (.blk w) 0 ∧ h.bytes w = some a ∧ h.ro w = false ∧ a.size = 2 ^ s.wbits.toNat := by
45      rcases hG.inv.win.block with hn | hx
46      · have := hG.inv.win.nullws hn
47        have := hG.inv.win.hv
48        simp_all
49      · exact hx
50    have hwsize : s.wsize.toNat = a.size := by
51      rcases hG.inv.win.ws with hz | hz
52      · have := hG.inv.win.hv; omega
53      · omega
54    have hwh : s.whave.toNat ≤ a.size := by have := hG.inv.win.hv; omega
55    have hxs : xs = (a.toList.drop s.wnext.toNat).take (s.whave.toNat - s.wnext.toNat) ++
56        a.toList.take s.wnext.toNat := by
57      rcases hdict with ⟨hz,_⟩ | ⟨rr,oo,aa,hp,hget,hfit,hxs⟩
58      · exact (hpos hz).elim
59      · rw [hwin] at hp
60        cases hp
61        have heq : a = aa := Option.some.inj (ha.symm.trans hget)
62        subst aa
63        simpa [hsub] using hxs
64    obtain ⟨hwrite,hsep⟩ := hdest hnon
65    rcases hwrite with ⟨hn,_⟩ | ⟨rd,od,D,hd,hD,hroD,hroom⟩
66    · exact (hnon hn).elim
67    · have hroom' : od + s.whave.toNat ≤ D.size := by simpa [hxslen] using hroom
68      have hne : rd ≠ BRef.blk w := by
69        intro he
70        subst rd
71        have hD' : D = a := Option.some.inj (hD.symm.trans ha)
72        subst D
73        simp [Separate, hd, hwin, hxslen] at hsep
74        omega
75      have hrun := inflateGetDictionary_copy_general (dl := dl) hG.live hwin ha hD hroD hne hpos hwn hwh hroom'
76      refine ⟨Space.put h rd (getDictBytes D a od s.wnext.toNat s.whave.toNat), ?_, ?_⟩
77      · simpa [C.run, hd, hlength] using hrun
78      · simp only [ite_eq_right hnon]
79        right
80        have hseg : xs.toArray = a.extract s.wnext.toNat s.whave.toNat ++ a.extract 0 s.wnext.toNat := by
81          rw [hxs]
82          apply Array.toList_inj.mp
83          simp [Array.toList_extract, List.extract_eq_take_drop, hwn]
84        refine ⟨rd,od,D,hd,hD,hroD,by simpa [hxslen] using hroom', ?_⟩
85        rw [hseg, hxslen]
86        congr 1
87        exact ring_copy_extract D a od s.wnext.toNat s.whave.toNat hwn hwh hroom'
88
89#print axioms inflate_getdict_public
90
91end ZlibF.Spec.Public.InflateDictionaryProof