public-inflate-setdict.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.«inflate.c.public-setdict-success»
3
4open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs Zlib.Adler32.Proofs ZlibF.Spec.Public
5
6namespace ZlibF.Spec.Public.Proofs
7
8theorem setdict_allocation_failure_public
9    {h : Heap} {r : ZStreamRef} {i : Nat} {z : ZStream} {s : InflateState}
10    {source : BPtr} {len : UInt32} {xs : List UInt8}
11    (hg : Good h r i z s) (hza : z.zalloc = .fn "zcalloc")
12    (hn : source ≠ .null) (hb : Bytes h source len.toNat xs)
13    (hwrap : s.wrap = 0 ∨ s.mode = DICT)
14    (hcheck : s.mode = DICT → (ZlibF.Spec.adler32 xs).toUInt64 = s.check)
15    (hw : s.window = .null) (hok : h.allocOk h.nalloc = false) :
16    ∃ after, C.run (inflateSetDictionary (some r) source len) h = .ok (Z_MEM_ERROR, after) ∧
17      AllocationFailed h after ∧
18      Good after r i z { s with mode := MEM } ∧
19      Frame h after (fun b => StreamRoot r b ∨ InflateOwned i s b) ∧
20      (∃ s', h.istates i = some s ∧ after.istates i = some s' ∧
21        LiveChange h after (fun b => InflateOwned i s' b ∧ ¬ h.live b) (fun _ => False)) := by
22  let after := setI (setI { h with nalloc := h.nalloc + 1 } i s) i { s with mode := MEM }
23  have hfalse : ¬ h.allocOk h.nalloc = true := by rw [hok]; decide
24  have hr : C.run (inflateSetDictionary (some r) source len) h = .ok (Z_MEM_ERROR, after) := by
25    rcases hb with ⟨he, _, _⟩ | ⟨ref, off, a, rfl, ha, hf, hs⟩
26    · exact (hn he).elim
27    · have hseg := seg_eq_slice a off len.toNat hf
28      rw [← hseg] at hs
29      subst xs
30      exact inflateSetDictionary_alloc_fail_any hg hza ha hf hwrap hcheck hw hfalse
31  have hshape1 : Shape h (setI { h with nalloc := h.nalloc + 1 } i s) :=
32    shape_setI hg.live.hs s
33  have hshape2 : Shape (setI { h with nalloc := h.nalloc + 1 } i s) after :=
34    shape_setI (s0 := s) (by simp) _
35  have hshape : Shape h after := hshape1.trans hshape2
36  refine ⟨after, hr, ?_, inflateSetDictionary_alloc_fail_good hg, ?_, ?_⟩
37  · exact ⟨h.nalloc, Nat.le_refl _, by simp [after, setI], hok⟩
38  · simp only [Frame, after, setI, true_and]
39    refine ⟨Nat.le_refl _, Nat.le_succ _, ?_⟩
40    intro b _ hb
41    have hbi : b ≠ i := fun e => hb (Or.inr (Or.inl e))
42    simp [upd_ne, hbi]
43  · refine ⟨{ s with mode := MEM }, hg.live.hs, by simp [after], ?_⟩
44    intro b
45    have hl := hshape.live b
46    have howned : InflateOwned i { s with mode := MEM } b → h.live b := by
47      intro ho
48      rcases ho with he | he
49      · subst b
50        simp [Heap.live, hg.live.hs]
51      · simp [hw] at he
52    simp only [LiveChange, not_false_eq_true, and_true]
53    constructor
54    · intro ha; exact Or.inl (hl.mp ha)
55    · intro ha
56      rcases ha with ha | ⟨ho, hn⟩
57      · exact hl.mpr ha
58      · exact (hn (howned ho)).elim
59
60private theorem frame_unchanged (h : Heap) (changed : Nat → Prop) : Frame h h changed := by
61  refine ⟨rfl, rfl, rfl, Nat.le_refl _, Nat.le_refl _, ?_⟩
62  intro b _ _
63  simp
64
65private theorem owned_already_live {h : Heap} {r : ZStreamRef} {i : Nat} {z : ZStream} {s : InflateState}
66    (hg : Good h r i z s) : ∀ b, InflateOwned i s b → h.live b := by
67  intro b ho
68  rcases ho with hi | hw
69  · subst b
70    simp [Heap.live, hg.live.hs]
71  · rcases hg.inv.win.block with hn | ⟨w, a, hwin, ha, _, _⟩
72    · rw [hn] at hw
73      cases hw
74    · rw [hwin] at hw
75      cases hw
76      simp [Heap.live, ha]
77
78private theorem live_unchanged {h : Heap} {r : ZStreamRef} {i : Nat} {z : ZStream} {s : InflateState}
79    (hg : Good h r i z s) :
80    LiveChange h h (fun b => InflateOwned i s b ∧ ¬ h.live b) (fun _ => False) := by
81  intro b
82  simp only [LiveChange, not_false_eq_true, and_true]
83  constructor
84  · exact Or.inl
85  · intro hh
86    rcases hh with hl | ⟨ho, hn⟩
87    · exact hl
88    · exact (hn (owned_already_live hg b ho)).elim
89
90/-- `int inflateSetDictionary(z_streamp strm, const Bytef *dictionary, uInt dictLength)`
91satisfies all public rejection, content, frame and allocation clauses. -/
92theorem inflateSetDictionary_public : Goal.inflateSetDictionary := by
93  intro h r i z s source n xs old hg hza hold hb hsep _
94  by_cases hrefused : source = .null ∨ (s.wrap ≠ 0 ∧ s.mode ≠ DICT)
95  · refine ⟨Z_STREAM_ERROR, h, inflateSetDictionary_refused_any hg.live source n hrefused, ?_, ?_,
96      frame_unchanged h _, ⟨s, hg.live.hs, hg.live.hs, live_unchanged hg⟩⟩
97    · intro _; exact ⟨rfl, rfl⟩
98    · intro hn hwrap
99      rcases hrefused with he | ⟨hwrap', hm⟩
100      · exact (hn he).elim
101      · rcases hwrap with he | he
102        · exact (hwrap' he).elim
103        · exact (hm he).elim
104  · have hn : source ≠ .null := fun he => hrefused (Or.inl he)
105    have hwrap : s.wrap = 0 ∨ s.mode = DICT := by
106      by_cases hw : s.wrap = 0
107      · exact Or.inl hw
108      · by_cases hm : s.mode = DICT
109        · exact Or.inr hm
110        · exact (hrefused (Or.inr ⟨hw, hm⟩)).elim
111    have hbytes := hb hn
112    by_cases hbad : s.mode = DICT ∧ s.check ≠ (ZlibF.Spec.adler32 xs).toUInt64
113    · have hrun : C.run (inflateSetDictionary (some r) source n) h = .ok (Z_DATA_ERROR, h) := by
114        rcases hbytes with ⟨he, _, _⟩ | ⟨ref, off, a, rfl, ha, hf, hs⟩
115        · exact (hn he).elim
116        · rw [← seg_eq_slice a off n.toNat hf] at hs
117          subst xs
118          exact inflateSetDictionary_dataerr_any hg.live ha hf hbad.1 (Ne.symm hbad.2)
119      refine ⟨Z_DATA_ERROR, h, hrun, ?_, ?_, frame_unchanged h _,
120        ⟨s, hg.live.hs, hg.live.hs, live_unchanged hg⟩⟩
121      · intro he; exact (hrefused he).elim
122      · intro _ _; simp [hbad]
123    · have hcheck : s.mode = DICT → (ZlibF.Spec.adler32 xs).toUInt64 = s.check := by
124        intro hm
125        by_cases he : (ZlibF.Spec.adler32 xs).toUInt64 = s.check
126        · exact he
127        · exact (hbad ⟨hm, Ne.symm he⟩).elim
128      rcases hbytes with ⟨he, _, _⟩ | ⟨ref, off, a, hsource, ha, hf, hxs⟩
129      · exact (hn he).elim
130      · subst source
131        have hcheck' : s.mode = DICT → (ZlibF.Spec.adler32 (seg a off n.toNat)).toUInt64 = s.check := by
132          rw [seg_eq_slice a off n.toNat hf]
133          simpa [hxs] using hcheck
134        obtain ⟨rc, after, state, hr, hgood, hcase⟩ :=
135          inflateSetDictionary_success_public hg hza ha hf hxs hold hsep hwrap hcheck'
136        rcases hcase with ⟨hrc, hhavedict, hmode, hdict, hframe, hlive⟩ |
137          ⟨hrc, hmode, hwin, halloc⟩
138        · refine ⟨rc, after, hr, ?_, ?_, hframe, ⟨state, hg.live.hs, hgood.live.hs, hlive⟩⟩
139          · intro he; exact (hrefused he).elim
140          · intro _ _
141            simp only [ite_eq_right hbad]
142            exact Or.inr ⟨hrc, state, hgood, hhavedict, hmode, hdict⟩
143        · obtain ⟨failed, hf, hallocation, hgood', hframe, hlive⟩ :=
144            setdict_allocation_failure_public hg hza (by simp) (Or.inr ⟨ref, off, a, rfl, ha, hf, hxs⟩)
145              hwrap hcheck hwin halloc
146          have he : after = failed := by
147            rw [hrc] at hr
148            rw [hr] at hf
149            cases hf
150            rfl
151          subst failed
152          refine ⟨rc, after, hr, ?_, ?_, hframe, hlive⟩
153          · intro he; exact (hrefused he).elim
154          · intro _ _
155            simp only [ite_eq_right hbad]
156            exact Or.inl ⟨hrc, hallocation, { s with mode := MEM }, hgood', rfl⟩
157
158#print axioms setdict_allocation_failure_public
159#print axioms inflateSetDictionary_public
160
161end ZlibF.Spec.Public.Proofs