inflate.c.public-setdict-success.lean

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

1import ZlibF.Proof.«inflate.c.window-public-mode»
2import ZlibF.Proof.«inflate.c.public-setdict»
3
4namespace Zlib.Inflate.Proofs
5open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Adler32.Proofs ZlibF.Spec.Public
6
7private theorem dictionary_set_havedict {h : Heap} {zs : Nat} {st : InflateState} {xs : List UInt8}
8    (hd : InflateDictionary h st xs) : InflateDictionary (setI h zs { st with havedict := 1 })
9      { st with havedict := 1 } xs := by
10  rcases hd with ⟨hz, hxs⟩ | ⟨ref, off, a, hp, ha, hf, hxs⟩
11  · exact Or.inl ⟨hz, hxs⟩
12  · refine Or.inr ⟨ref, off, a, hp, ?_, hf, hxs⟩
13    cases ref <;> simpa [Space.get, setI] using ha
14
15private theorem frame_after_setI {before mid : Heap} {zs : Nat} {changed : Nat → Prop}
16    {st : InflateState} (hf : Frame before mid changed) (hc : changed zs) :
17    Frame before (setI mid zs st) changed := by
18  rcases hf with ⟨hstatic, horacle, hgarbage, hnext, halloc, hframe⟩
19  refine ⟨hstatic, horacle, hgarbage, hnext, halloc, ?_⟩
20  intro b hl hn
21  have hne : b ≠ zs := fun he => hn (he ▸ hc)
22  have h := hframe b hl hn
23  simpa [setI, upd_ne _ _ _ _ hne] using h
24
25private theorem live_after_setI {before mid : Heap} {zs : Nat} {st : InflateState}
26    (hs : mid.istates zs = some st)
27    (hl : LiveChange before mid (fun b => InflateOwned zs st b ∧ ¬ before.live b) (fun _ => False)) :
28    LiveChange before (setI mid zs { st with havedict := 1 })
29      (fun b => InflateOwned zs { st with havedict := 1 } b ∧ ¬ before.live b) (fun _ => False) := by
30  have hshape := shape_setI hs { st with havedict := 1 }
31  intro b
32  simpa [LiveChange, InflateOwned] using (hshape.live b).trans (hl b)
33
34/-- `int inflateSetDictionary(z_streamp strm, const Bytef *dictionary, uInt dictLength)`
35with an accepted checksum appends the exact retained dictionary or returns a
36genuine window-allocation error. -/
37theorem inflateSetDictionary_success_public {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
38    {off : Nat} {source : BRef} {D : Array UInt8} {L : UInt32} {old xs : List UInt8}
39    (hG : Good H r zs z st) (hza : z.zalloc = .fn "zcalloc") (hD : Space.get H source = some D) (hfit : off + L.toNat ≤ D.size)
40    (hxs : xs = (D.toList.drop off).take L.toNat) (hold : ZlibF.Spec.Public.InflateDictionary H st old)
41    (hsep : ZlibF.Spec.Public.Separate (.ref source off) L.toNat st.window (2 ^ st.wbits.toNat)) (hwrap : st.wrap = 0 ∨ st.mode = DICT)
42    (hadler : st.mode = DICT → (ZlibF.Spec.adler32 (Zlib.Adler32.Proofs.seg D off L.toNat)).toUInt64 = st.check) :
43    ∃ v H' st', C.run (inflateSetDictionary (some r) (.ref source off) L) H = .ok (v, H') ∧ Good H' r zs z st' ∧
44      ((v = Z_OK ∧ st'.havedict = 1 ∧ st'.mode = st.mode ∧
45          ZlibF.Spec.Public.InflateDictionary H' st' ((old ++ xs).drop ((old ++ xs).length - 2 ^ st.wbits.toNat)) ∧
46          Frame H H' (fun b => StreamRoot r b ∨ InflateOwned zs st b) ∧
47          LiveChange H H' (fun b => InflateOwned zs st' b ∧ ¬ H.live b) (fun _ => False)) ∨
48       (v = Z_MEM_ERROR ∧ st'.mode = MEM ∧ st.window = .null ∧ H.allocOk H.nalloc = false)) := by
49  have hL := hG.live
50  obtain ⟨v0, H1, st1, hr1, hG1, hcase⟩ := updatewindow_dictionary_public (copy := L) (source := source) (off := off) (bytes := D)
51    hG hza hD hfit hxs hold hsep
52  have hadd : OkOn H (Ptr.add (Ptr.ref source off) (L.toNat : Int)) (Ptr.ref source (off + L.toNat)) :=
53    Ptr.add_nat_ok (a := D) (by simpa using hD) hfit
54  have hadd' : Ptr.add (Ptr.ref source off) (L.toNat : Int) H = .ok (Ptr.ref source (off + L.toNat), H) := hadd
55  have hnn : (Ptr.ref source off == (Ptr.null : BPtr)) = false := by simp
56  have hr1' : updatewindow (some r) (Ptr.ref source (off + L.toNat)) L H = .ok (v0, H1) := hr1
57  have hstate : H.istates zs = some st := hL.hs
58  have hrun : inflateSetDictionary (some r) (.ref source off) L H =
59      (if v0 = 0 then .ok (Z_OK, setI H1 zs { st1 with havedict := 1 })
60       else .ok (Z_MEM_ERROR, setI H1 zs { st1 with mode := MEM })) := by
61    have hs1 : H1.istates zs = some st1 := hG1.live.hs
62    unfold inflateSetDictionary
63    simp only [bind_app, stateCheck_live hL, ldZ_eq, ldI_eq, hL.hz, hL.zst, castI, hL.hs, hnn, bne_self_eq_false,
64      Bool.or_self, Bool.false_eq_true, ite_false]
65    by_cases hm : st.mode = DICT
66    · have hra := adler32_dict_any hD L hfit
67      have hck := hadler hm
68      have hmb : (st.mode == DICT) = true := by simpa using hm
69      simp only [hmb, adler32_init, hra, hck, bne_self_eq_false, hadd', hr1', ite_true, Bool.false_eq_true, ite_false, Bool.and_false, hmb, hm, beq_self_eq_true]
70      simp only [bind_app, adler32_init, hra, hck, bne_self_eq_false, hadd', hr1', Bool.false_eq_true, ite_false, setMode, wrI_eq, hs1]
71      by_cases hv0 : v0 = 0
72      · simp only [hv0, bne_self_eq_false, Bool.false_eq_true, ite_false, ite_true, bind_app, wrI_eq, hs1, pure_app, setI]
73      · have hb : (v0 != 0) = true := by simpa using hv0
74        simp only [hb, ite_true, hv0, ite_false, setMode, bind_app, wrI_eq, hs1, pure_app, setI]
75    · have hw0 : st.wrap = 0 := by rcases hwrap with h | h; exact h; exact absurd h hm
76      have hmb : (st.mode == DICT) = false := by simpa using hm
77      simp only [hmb, hw0, hadd', hr1', bne_self_eq_false, Bool.false_and, Bool.false_eq_true, ite_false, Bool.and_false]
78      simp only [bind_app, hadd', hr1', Bool.false_eq_true, ite_false, setMode, wrI_eq, hs1]
79      by_cases hv0 : v0 = 0
80      · simp only [hv0, bne_self_eq_false, Bool.false_eq_true, ite_false, ite_true, bind_app, wrI_eq, hs1, pure_app, setI]
81      · have hb : (v0 != 0) = true := by simpa using hv0
82        simp only [hb, ite_true, hv0, ite_false, setMode, bind_app, wrI_eq, hs1, pure_app, setI]
83  have hs1 : H1.istates zs = some st1 := hG1.live.hs
84  by_cases hv0 : v0 = 0
85  · rcases hcase with ⟨_, hdict⟩ | ⟨h1, _⟩
86    · have hmode : st1.mode = st.mode := by
87        apply updatewindow_mode_public hG hza hD hfit hsep
88        · simpa [hv0] using hr1
89        · exact hG1.live.hs
90      refine ⟨Z_OK, setI H1 zs { st1 with havedict := 1 }, { st1 with havedict := 1 }, ?_, ?_, Or.inl ⟨rfl, rfl, hmode, ?_, ?_, ?_⟩⟩
91      · rw [C.run, hrun, ite_eq_left hv0]
92      · exact good_state hG1 rfl hG1.live.mode (hG1.inv.of_fields rfl rfl rfl rfl rfl rfl rfl rfl rfl hG1.inv.bits rfl rfl rfl)
93      · exact dictionary_set_havedict hdict
94      · have hframe := updatewindow_frame_public hG hza hD hfit hsep (by simpa [hv0] using hr1)
95        exact frame_after_setI hframe (Or.inr (Or.inl rfl))
96      · have hlive := updatewindow_live_public hG hza hD hfit hsep (by simpa [hv0] using hr1) hG1.live.hs
97        exact live_after_setI hG1.live.hs hlive
98    · rw [hv0] at h1; exact absurd h1 (by decide)
99  · rcases hcase with ⟨h1, _⟩ | ⟨_, hw0, hnok, _, _⟩
100    · exact absurd h1 hv0
101    · refine ⟨Z_MEM_ERROR, setI H1 zs { st1 with mode := MEM }, { st1 with mode := MEM }, ?_, ?_, Or.inr ⟨rfl, rfl, hw0, hnok⟩⟩
102      · rw [C.run, hrun, ite_eq_right hv0]
103      · exact good_state hG1 rfl mode_mem (hG1.inv.of_fields rfl rfl rfl rfl rfl rfl rfl rfl rfl hG1.inv.bits rfl rfl rfl)
104
105#print axioms inflateSetDictionary_success_public
106end Zlib.Inflate.Proofs