deflate.c.init.failure.lean

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

1import ZlibF.Proof.«deflate.c.init.frame»
2
3/-! # deflate.c: actual default allocation failure and cleanup heap -/
4
5namespace Zlib.Deflate.Proofs.DefaultInit
6open C Zlib.Deflate Zlib.Deflate.Spec ZlibF.Spec.Public
7set_option autoImplicit false
8
9def failureState (ph : Heap) (r : ZStreamRef) : DeflateState :=
10  { bufferState ph (baseState r) with status := FINISH_STATE }
11
12def failureStream (h : Heap) (z : ZStream) (m : BPtr) : ZStream :=
13  { stateStream z h.nextBlk with msg := m }
14
15def failureMsgHeap (h : Heap) (r : ZStreamRef) (z : ZStream) (m : BPtr) : Heap :=
16  let ph := publishedHeap h r z
17  r.put (setD (buffersHeap ph) h.nextBlk (failureState ph r)) (failureStream h z m)
18
19def failureHeap (h : Heap) (r : ZStreamRef) (z : ZStream) (m : BPtr) : Heap :=
20  endHeap (failureMsgHeap h r z m) r h.nextBlk (failureStream h z m)
21    (failureState (publishedHeap h r z) r)
22
23def clearDHeap (h : Heap) (ds : Nat) : Heap := { h with dstates := upd h.dstates ds none }
24
25theorem failure_heap_eq (h : Heap) (r : ZStreamRef) (z : ZStream) (m : BPtr) :
26    failureHeap h r z m = clearDHeap
27      (r.put (rollbackBuffers (publishedHeap h r z) (failureMsgHeap h r z m))
28        { failureStream h z m with state := none }) h.nextBlk := by
29  unfold failureHeap endHeap clearDHeap
30  rw [ZStreamRef.put_dstates, (rollback_stable _ _).dstates]
31  rfl
32
33theorem get_failure_raw {h : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get h = some z) :
34    r.get (setD (buffersHeap (publishedHeap h r z)) h.nextBlk
35      (failureState (publishedHeap h r z) r)) = some (stateStream z h.nextBlk) := by
36  simp [publishedHeap, ZStreamRef.get_put_same hz]
37
38theorem get_failure_message {h : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get h = some z) (m : BPtr) :
39    r.get (failureMsgHeap h r z m) = some (failureStream h z m) := by
40  exact ZStreamRef.get_put_same (get_failure_raw hz) _
41
42theorem memory_message (h : Heap) : ∃ m, ERR_MSG Z_MEM_ERROR h = .ok (m, h) := by
43  obtain ⟨i, hr, _⟩ := Zlib.Zutil.Proofs.strLit_run h
44    (Zlib.Zutil.Spec.errText Z_MEM_ERROR.toInt) (Zlib.Zutil.Proofs.errText_lit _)
45  refine ⟨.ref (.str i) 0, ?_⟩
46  unfold ERR_MSG
47  rw [Zlib.Zutil.Proofs.zError_eval]
48  exact hr
49
50/-- The actual failed-buffer branch sets FINISH_STATE, obtains the actual
51error literal and invokes cleanup on the partially constructed stream. -/
52theorem finish_failure {h : Heap} {r : ZStreamRef} {z : ZStream}
53    (hz : r.get h = some z) (hd : DefAlloc z) (level : Int32)
54    (bad : ((bufferPointers (publishedHeap h r z)).1 == .null ||
55      (bufferPointers (publishedHeap h r z)).2.1 == .null ||
56      (bufferPointers (publishedHeap h r z)).2.2.1 == .null ||
57      (bufferPointers (publishedHeap h r z)).2.2.2 == .null) = true) :
58    ∃ m, finish (some r) (some (.tab h.nextBlk)) level (bufferPointers (publishedHeap h r z))
59        (setD (buffersHeap (publishedHeap h r z)) h.nextBlk
60          (bufferState (publishedHeap h r z) (baseState r))) =
61      .ok (Z_MEM_ERROR, failureHeap h r z m) := by
62  let ph := publishedHeap h r z
63  let gf := setD (buffersHeap ph) h.nextBlk (failureState ph r)
64  obtain ⟨m, hm⟩ := memory_message gf
65  have hzF : r.get gf = some (stateStream z h.nextBlk) := get_failure_raw hz
66  have hzM := get_failure_message hz m
67  have hl : DLive (failureMsgHeap h r z m) r h.nextBlk (failureStream h z m) (failureState ph r) := by
68    refine ⟨hzM, ?_, rfl, rfl, ?_, ?_, ?_⟩
69    · simp [failureMsgHeap, ph]
70    · simp [failureState, GoodStatus]
71    · simpa [failureStream, stateStream] using (show z.zalloc ≠ .null by rw [hd.1]; decide)
72    · simpa [failureStream, stateStream] using (show z.zfree ≠ .null by rw [hd.2]; decide)
73  obtain ⟨hw, hp, hq, hb, hwb, hpq⟩ := buffers_freeable ph
74  have release := end_partial_run hl (by simpa [failureStream, stateStream] using hd.2)
75    (by simpa [FreeableB, failureMsgHeap, failureState, bufferState, bufferPointers] using hb)
76    (by simpa [FreeableB, failureMsgHeap, failureState, bufferState, bufferPointers] using hw)
77    (by simpa [FreeableW, failureMsgHeap, failureState, bufferState, bufferPointers] using hq)
78    (by simpa [FreeableW, failureMsgHeap, failureState, bufferState, bufferPointers] using hp)
79    (by simpa [failureState, bufferState, bufferPointers] using hwb)
80    (by simpa [failureState, bufferState, bufferPointers] using hpq)
81  refine ⟨m, ?_⟩
82  unfold finish
83  simp only []
84  rw [bad]
85  simp only [ite_true, bind_app, wrD_eq, setD_dstates_same, setD_setD]
86  change (do
87    let m ← ERR_MSG Z_MEM_ERROR
88    zwr (some r) (fun z => { z with msg := m })
89    let _ ← deflateEnd (some r)
90    pure Z_MEM_ERROR) gf = _
91  rw [bind_app, hm]
92  simp only [bind_app, zwr_eq, hzF]
93  change (do let _ ← deflateEnd (some r); pure Z_MEM_ERROR) (failureMsgHeap h r z m) = _
94  rw [bind_app, release]
95  rfl
96
97theorem slot_clearD_except (h : Heap) (ds x : Nat) (hn : x ≠ ds) :
98    SlotSame h (clearDHeap h ds) x := by
99  simp [SlotSame, clearDHeap, upd_ne _ _ _ _ hn]
100
101theorem failure_count (h : Heap) (r : ZStreamRef) (z : ZStream) (m : BPtr) :
102    (failureHeap h r z m).nalloc = h.nalloc + 5 := by
103  simp only [failure_heap_eq, clearDHeap, ZStreamRef.put_nalloc, rollback_nalloc,
104    failureMsgHeap, ZStreamRef.put_nalloc, setD_nalloc, buffers_nalloc,
105    publishedHeap, stateHeap, ZStreamRef.put_nalloc, Nat.add_assoc]
106
107theorem failure_next (h : Heap) (r : ZStreamRef) (z : ZStream) (m : BPtr) :
108    h.nextBlk ≤ (failureHeap h r z m).nextBlk := by
109  have hb := buffers_next (publishedHeap h r z)
110  have hn : (publishedHeap h r z).nextBlk = h.nextBlk + 1 := by simp [publishedHeap, stateHeap]
111  have he : (failureHeap h r z m).nextBlk = (buffersHeap (publishedHeap h r z)).nextBlk := by
112    simp only [failure_heap_eq, clearDHeap, ZStreamRef.put_nextBlk, rollback_next,
113      failureMsgHeap, setD_nextBlk]
114  omega
115
116/-- Failure keeps every old object outside the stream; permission changes
117at newly allocated then freed slots are outside the old-object frame. -/
118theorem failure_frame {h : Heap} (r : ZStreamRef) (z : ZStream) (m : BPtr) (hf : Fresh h) :
119    Frame h (failureHeap h r z m) (StreamRoot r) := by
120  let ph := publishedHeap h r z
121  let gm := failureMsgHeap h r z m
122  have sb := buffers_stable ph
123  have sr := rollback_stable ph gm
124  refine frame_of_old (g := failureHeap h r z m) r hf ?_ ?_ ?_
125    (failure_next h r z m) (by rw [failure_count]; omega) ?_
126  · rw [failure_heap_eq]
127    change h.static = (r.put (rollbackBuffers ph gm) { failureStream h z m with state := none }).static
128    rw [ZStreamRef.put_static, sr.static]
129    change h.static = (r.put (setD (buffersHeap ph) h.nextBlk (failureState ph r)) (failureStream h z m)).static
130    rw [ZStreamRef.put_static, setD_static, sb.static]
131    simp [ph, publishedHeap, stateHeap]
132  · rw [failure_heap_eq]
133    change h.allocOk = (r.put (rollbackBuffers ph gm) { failureStream h z m with state := none }).allocOk
134    rw [ZStreamRef.put_allocOk, sr.allocOk]
135    change h.allocOk = (r.put (setD (buffersHeap ph) h.nextBlk (failureState ph r)) (failureStream h z m)).allocOk
136    rw [ZStreamRef.put_allocOk, setD_allocOk, sb.allocOk]
137    simp [ph, publishedHeap, stateHeap]
138  · rw [failure_heap_eq]
139    change h.garbage = (r.put (rollbackBuffers ph gm) { failureStream h z m with state := none }).garbage
140    rw [ZStreamRef.put_garbage, sr.garbage]
141    change h.garbage = (r.put (setD (buffersHeap ph) h.nextBlk (failureState ph r)) (failureStream h z m)).garbage
142    rw [ZStreamRef.put_garbage, setD_garbage, sb.garbage]
143    simp [ph, publishedHeap, stateHeap]
144  · intro x hx hn
145    have hp : h.nextBlk < ph.nextBlk := by simp [ph, publishedHeap, stateHeap]
146    have hds : x ≠ h.nextBlk := by omega
147    have a : SlotSame h ph x :=
148      (slot_put_except h r (stateStream z h.nextBlk) x hn).trans
149        (slot_stateHeap_old _ (baseState r) x (by simpa using hx))
150    have b := a.trans (buffers_old ph x (by omega))
151    have c := b.trans (slot_setD_except _ h.nextBlk (failureState ph r) x hds)
152    have d : SlotSame h gm x := c.trans (slot_put_except _ r (failureStream h z m) x hn)
153    have e := d.trans (rollback_old ph gm x (by omega))
154    have f := e.trans (slot_put_except _ r { failureStream h z m with state := none } x hn)
155    rw [failure_heap_eq]
156    exact f.trans (slot_clearD_except _ h.nextBlk x hds)
157
158/-- Cleanup restores the existence of exactly the original objects.
159This is pointwise: internal table capacities may remain enlarged. -/
160theorem failure_shape {h : Heap} {r : ZStreamRef} {z : ZStream}
161    (hz : r.get h = some z) (hf : Fresh h) (m : BPtr) : Shape h (failureHeap h r z m) := by
162  let ph := publishedHeap h r z
163  let gf := setD (buffersHeap ph) h.nextBlk (failureState ph r)
164  let gm := failureMsgHeap h r z m
165  let gr := rollbackBuffers ph gm
166  let zc : ZStream := { failureStream h z m with state := none }
167  have hfp : Fresh ph := fresh_stateHeap ((shape_put hz (stateStream z h.nextBlk)).fresh (by simp) hf) _
168  have hzF : r.get gf = some (stateStream z h.nextBlk) := get_failure_raw hz
169  have hzM : r.get gm = some (failureStream h z m) := get_failure_message hz m
170  have hzR : r.get gr = some (failureStream h z m) := by simpa [gr] using hzM
171  have si := shape_put hz (stateStream z h.nextBlk)
172  have sm := shape_put hzF (failureStream h z m)
173  have se := shape_put hzR zc
174  have sb := buffers_stable ph
175  have sr := rollback_stable ph gm
176  have hd : h.dstates h.nextBlk = none := (Heap.not_live.mp (hf _ (Nat.le_refl _))).2.2.2.2.1
177  intro x
178  have arrays := rollback_arrays_at (g := gm) hfp x
179    (by simp [gm, failureMsgHeap, ph]) (by simp [gm, failureMsgHeap, ph])
180  have bytes : (failureHeap h r z m).bytes x = h.bytes x := by
181    rw [failure_heap_eq]
182    simpa [clearDHeap, ph, publishedHeap, stateHeap, gr] using arrays.1
183  have words : (failureHeap h r z m).words x = h.words x := by
184    rw [failure_heap_eq]
185    simpa [clearDHeap, ph, publishedHeap, stateHeap, gr] using arrays.2
186  have dstates : (failureHeap h r z m).dstates x = h.dstates x := by
187    rw [failure_heap_eq]
188    change upd (r.put gr zc).dstates h.nextBlk none x = h.dstates x
189    rw [ZStreamRef.put_dstates, sr.dstates]
190    change upd (r.put gf (failureStream h z m)).dstates h.nextBlk none x = h.dstates x
191    rw [ZStreamRef.put_dstates]
192    simp only [gf, setD, upd_upd, buffers_dstates]
193    simp only [ph, publishedHeap, stateHeap_dstates, ZStreamRef.put_dstates,
194      ZStreamRef.put_nextBlk, upd_upd, upd_apply]
195    by_cases hx : x = h.nextBlk <;> simp [hx, hd]
196  refine ⟨congrArg Option.isSome bytes, congrArg Option.isSome words, ?_, ?_,
197    congrArg Option.isSome dstates, ?_, ?_⟩
198  · rw [failure_heap_eq]
199    change ((r.put gr zc).streams x).isSome = (h.streams x).isSome
200    rw [(se x).2.2.1, sr.streams]
201    change ((r.put gf (failureStream h z m)).streams x).isSome = _
202    rw [(sm x).2.2.1]
203    change ((buffersHeap ph).streams x).isSome = _
204    rw [sb.streams]
205    simpa [ph, publishedHeap, stateHeap] using (si x).2.2.1
206  · rw [failure_heap_eq]
207    change ((r.put gr zc).gzheaders x).isSome = _
208    rw [ZStreamRef.put_gzheaders, sr.gzheaders]
209    change ((r.put gf (failureStream h z m)).gzheaders x).isSome = _
210    rw [ZStreamRef.put_gzheaders]
211    change ((buffersHeap ph).gzheaders x).isSome = _
212    rw [sb.gzheaders]
213    simp [ph, publishedHeap, stateHeap]
214  · rw [failure_heap_eq]
215    change ((r.put gr zc).istates x).isSome = _
216    rw [ZStreamRef.put_istates, sr.istates]
217    change ((r.put gf (failureStream h z m)).istates x).isSome = _
218    rw [ZStreamRef.put_istates]
219    change ((buffersHeap ph).istates x).isSome = _
220    rw [sb.istates]
221    simp [ph, publishedHeap, stateHeap]
222  · rw [failure_heap_eq]
223    change ((r.put gr zc).gzstates x).isSome = (h.gzstates x).isSome
224    rw [(se x).2.2.2.2.2.2, sr.gzstates]
225    change ((r.put gf (failureStream h z m)).gzstates x).isSome = _
226    rw [(sm x).2.2.2.2.2.2]
227    change ((buffersHeap ph).gzstates x).isSome = _
228    rw [sb.gzstates]
229    simpa [ph, publishedHeap, stateHeap] using (si x).2.2.2.2.2.2
230
231theorem failure_stream_cleared {h : Heap} {r : ZStreamRef} {z : ZStream}
232    (hz : r.get h = some z) (m : BPtr) :
233    r.get (failureHeap h r z m) = some { failureStream h z m with state := none } := by
234  rw [failure_heap_eq]
235  simp only [clearDHeap, ZStreamRef.get_dstates]
236  exact ZStreamRef.get_put_same (by simpa using get_failure_message hz m) _
237
238end Zlib.Deflate.Proofs.DefaultInit