gzlib.c.error.lean

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

1import ZlibF.Proof.«gzlib.c.base»
2
3/-!
4# gzlib.c: `gz_error` without a message, `gz_reset`, `gzclearerr`
5
6`gz_error(state, err, NULL)` frees the old message, records `err` and clears the message. `gz_reset` is made of plain
7field writes and one such call. Both keep `GzGood` (the message block is the only block that goes away) and give the
8ownership statement: the live blocks afterwards are those before, without the old message block.
9-/
10
11namespace Zlib.Gzlib.Spec
12open C Zlib.GzFs Zlib.Gzguts
13
14/-- The record `gz_error(state, err, NULL)` leaves: no message, the new error code. -/
15def errNull (s : GzState) (e : Int32) : GzState := { s with msg := .null, err := e }
16
17/-- The record `gz_reset` leaves (`gz_reset(state)` after `gz_open` and in `gzrewind`): the buffered bytes and the
18position are cleared, the reader goes back to `LOOK`, the writer clears `reset`, the error is `Z_OK` without a message,
19and the embedded stream has no input. -/
20def resetRec (s : GzState) : GzState :=
21  { (if s.mode == GZ_READ then { s with eof := 0, how := LOOK, junk := -1 } else { s with reset := 0 }) with
22    x := { s.x with «have» := 0, pos := 0 }, past := 0, again := 0, skip := 0, msg := .null, err := Z_OK,
23    strm := { s.strm with avail_in := 0 } }
24
25end Zlib.Gzlib.Spec
26
27namespace Zlib.Gzlib.Proofs
28open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib Zlib.Gzlib.Spec
29
30theorem blk_ne_msg {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) {mb : Nat} (hm : s.msg = .ref (.blk mb) 0) :
31    (∀ b, s.path = .ref (.blk b) 0 → b ≠ mb) ∧ (∀ b, s.in = .ref (.blk b) 0 → b ≠ mb) ∧
32    (∀ b, s.out = .ref (.blk b) 0 → b ≠ mb) := by
33  have hn := hG.nodup
34  rcases hG.path with ⟨pb, hp, -⟩
35  rcases hG.inb with hi | ⟨ib, ia, hi, -⟩ <;> rcases hG.outb with ho | ⟨ob, oa, ho, -⟩ <;>
36    simp [hp, hm, hi, ho, ptrBlk, List.nodup_cons] at hn ⊢ <;> omega
37
38theorem Uniq.freeBytes {h : Heap} (hU : Uniq h) (mb : Nat) : Uniq { h with bytes := upd h.bytes mb none } := by
39  intro b
40  by_cases hb : b = mb
41  · subst hb
42    have := hU b
43    simp only [upd_same, cnt_none]
44    omega
45  · have := hU b
46    simpa only [upd_ne _ _ _ _ hb] using this
47
48theorem live_freeBytes {h : Heap} (hU : Uniq h) {mb : Nat} {a : Array UInt8} (ha : h.bytes mb = some a) (b : Nat) :
49    ({ h with bytes := upd h.bytes mb none } : Heap).live b ↔ h.live b ∧ b ≠ mb := by
50  by_cases hb : b = mb
51  · subst hb
52    have := hU b
53    simp only [Heap.live, ha, cnt_some] at this ⊢
54    simp only [upd_same]
55    have h1 : h.words b = none := by
56      cases hh : h.words b <;> simp [hh] at this ⊢ <;> omega
57    have h2 : h.streams b = none := by
58      cases hh : h.streams b <;> simp [hh] at this ⊢ <;> omega
59    have h3 : h.gzheaders b = none := by
60      cases hh : h.gzheaders b <;> simp [hh] at this ⊢ <;> omega
61    have h4 : h.dstates b = none := by
62      cases hh : h.dstates b <;> simp [hh] at this ⊢ <;> omega
63    have h5 : h.istates b = none := by
64      cases hh : h.istates b <;> simp [hh] at this ⊢ <;> omega
65    have h6 : h.gzstates b = none := by
66      cases hh : h.gzstates b <;> simp [hh] at this ⊢ <;> omega
67    simp [h1, h2, h3, h4, h5, h6]
68  · simp [Heap.live, upd_ne _ _ _ _ hb, hb]
69
70theorem Fresh.freeBytes {h : Heap} (hF : Fresh h) (mb : Nat) : Fresh { h with bytes := upd h.bytes mb none } := by
71  intro b hb hl
72  apply hF b hb
73  by_cases hbm : b = mb
74  · subst hbm
75    simp only [Heap.live, upd_same] at hl ⊢
76    rcases hl with hl | hl
77    · exact absurd rfl hl
78    · exact Or.inr hl
79  · simpa [Heap.live, upd_ne _ _ _ _ hbm] using hl
80
81theorem nodup_drop_msg {a c d : BPtr} (b : BPtr) (hn : ([a, b, c, d].filterMap ptrBlk).Nodup) :
82    ([a, (.null : BPtr), c, d].filterMap ptrBlk).Nodup := by
83  have e : ([a, (.null : BPtr), c, d].filterMap ptrBlk) = ([a, c, d].filterMap ptrBlk) := by
84    simp [List.filterMap_cons, ptrBlk]
85  rw [e]
86  exact List.Nodup.sublist (List.Sublist.filterMap ptrBlk (by simp)) hn
87
88/-- `gz_error(state, e, NULL)` keeps the invariant (the old message block is freed). -/
89theorem GzGood.afterErr {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (e : Int32) :
90    GzGood (setS (freeStr h s.msg) gs (errNull s e)) gs (errNull s e) := by
91  rcases hG.msg with hn | ⟨mb, hm, a, ha, hro, k, hz⟩
92  · rw [hn]; simp only [freeStr_null]
93    exact GzGood.withRec hG (Or.inl rfl) rfl (by simp [errNull, hn]) rfl rfl (by simp [errNull])
94  · obtain ⟨hpn, hin, hon⟩ := blk_ne_msg hG hm
95    rw [hm]; simp only [freeStr_blk]
96    have hU := Uniq.freeBytes hG.uniq mb
97    have hF := Fresh.freeBytes hG.fresh mb
98    have hS := shape_setS (h := ({ h with bytes := upd h.bytes mb none } : Heap)) (gs := gs) (s0 := s) hG.hs (errNull s e)
99    refine ⟨by simp, hG.mode, ?_, Or.inl rfl, ?_, ?_, nodup_drop_msg s.msg hG.nodup, fun _ => rfl,
100      Shape.uniq hS hU, Shape.fresh hS rfl hF⟩
101    · obtain ⟨pb, hp, a', ha', hro', k', hz'⟩ := hG.path
102      have hne := hpn pb hp
103      exact ⟨pb, hp, a', by simp [setS, upd_ne _ _ _ _ hne, ha'], by simpa using hro', k', hz'⟩
104    · rcases hG.inb with hi | ⟨ib, ia, hi, hia, hiro⟩
105      · exact Or.inl hi
106      · have hne := hin ib hi
107        exact Or.inr ⟨ib, ia, hi, by simp [setS, upd_ne _ _ _ _ hne, hia], by simpa using hiro⟩
108    · rcases hG.outb with hi | ⟨ib, ia, hi, hia, hiro⟩
109      · exact Or.inl hi
110      · have hne := hon ib hi
111        exact Or.inr ⟨ib, ia, hi, by simp [setS, upd_ne _ _ _ _ hne, hia], by simpa using hiro⟩
112
113
114@[simp] theorem freeStr_setS (h : Heap) (gs : Nat) (s : GzState) (p : BPtr) :
115    freeStr (setS h gs s) p = setS (freeStr h p) gs s := by
116  cases p with
117  | null => rfl
118  | ref r o => cases r <;> rfl
119
120theorem freeB_blk_run {h : Heap} {mb : Nat} {a : Array UInt8} (ha : h.bytes mb = some a) (hro : h.ro mb = false) :
121    freeB (.ref (.blk mb) 0) h = .ok ((), { h with bytes := upd h.bytes mb none }) := by
122  simp [freeB, ha, hro]
123
124theorem freeB_blk_setS {h : Heap} {mb : Nat} {a : Array UInt8} (ha : h.bytes mb = some a) (hro : h.ro mb = false)
125    (gs : Nat) (s' : GzState) :
126    freeB (.ref (.blk mb) 0) (setS h gs s') = .ok ((), setS { h with bytes := upd h.bytes mb none } gs s') := by
127  simp [freeB, setS, ha, hro]
128
129theorem record_msg_null {s : GzState} (hn : s.msg = .null) : { s with msg := .null } = s := by
130  cases s; simp_all
131
132/-- `gz_error(state, err, NULL)`: the old message is freed (the only change of the heap besides the record), the error
133code is `err` and there is no message. -/
134theorem gz_error_null_run {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (e : Int32) :
135    gz_error (some (.tab gs)) e .null h = .ok ((), setS (freeStr h s.msg) gs (errNull s e)) := by
136  have hs := hG.hs
137  unfold gz_error
138  rcases hG.msg with hn | ⟨mb, hm, a, ha, hro, k, hz⟩
139  · gsimp [hs, hn, errNull]
140  · have hne : s.err ≠ Z_MEM_ERROR := fun h' => by have := hG.memerr h'; rw [hm] at this; cases this
141    gsimp [hs, hm, hne, freeB_blk_run ha hro, freeB_blk_setS ha hro, errNull]
142
143
144/-- `gz_reset(state)`. -/
145theorem gz_reset_run {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) :
146    gz_reset (some (.tab gs)) h = .ok ((), setS (freeStr h s.msg) gs (resetRec s)) := by
147  have hs := hG.hs
148  unfold gz_reset
149  rcases hG.msg with hn | ⟨mb, hm, a, ha, hro, k, hz⟩
150  · by_cases hmo : s.mode = GZ_READ
151    · gsimp [hs, hn, hmo, gz_error, resetRec]
152    · gsimp [hs, hn, hmo, gz_error, resetRec]
153  · have hne : s.err ≠ Z_MEM_ERROR := fun h' => by have := hG.memerr h'; rw [hm] at this; cases this
154    by_cases hmo : s.mode = GZ_READ
155    · gsimp [hs, hm, hne, hmo, freeB_blk_setS ha hro, gz_error, resetRec]
156    · gsimp [hs, hm, hne, hmo, freeB_blk_setS ha hro, gz_error, resetRec]
157
158theorem GzGood.afterReset {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) :
159    GzGood (setS (freeStr h s.msg) gs (resetRec s)) gs (resetRec s) := by
160  have h1 := GzGood.withRec (GzGood.afterErr hG Z_OK) (s' := resetRec s) (Or.inl (by unfold resetRec errNull; split <;> rfl))
161    (by unfold resetRec errNull; split <;> rfl) (by unfold resetRec errNull; split <;> rfl)
162    (by unfold resetRec errNull; split <;> rfl) (by unfold resetRec errNull; split <;> rfl)
163    (by intro _; unfold resetRec; split <;> rfl)
164  simpa using h1
165
166/-- **gz_reset, safety and effect.** On a handle that satisfies the invariant the call does not fault; the old message
167block is the only block freed; the record is `resetRec s`. -/
168theorem gz_reset_safe {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) :
169    ∃ h', C.run (gz_reset (some (.tab gs))) h = .ok ((), h') ∧ h' = setS (freeStr h s.msg) gs (resetRec s) ∧
170      GzGood h' gs (resetRec s) ∧
171      (∀ S, h.Owns S → h'.Owns (fun b => S b ∧ s.msg ≠ .ref (.blk b) 0)) := by
172  refine ⟨_, gz_reset_run hG, rfl, GzGood.afterReset hG, ?_⟩
173  intro S hO
174  rcases hG.msg with hn | ⟨mb, hm, a, ha, hro, k, hz⟩
175  · simp only [hn, freeStr_null]
176    have := Shape.owns (shape_setS hG.hs (resetRec s)) hO
177    simpa [hn] using this
178  · rw [hm]; simp only [freeStr_blk]
179    have hO1 : ({ h with bytes := upd h.bytes mb none } : Heap).Owns (fun b => S b ∧ b ≠ mb) := by
180      intro b; rw [live_freeBytes hG.uniq ha b, hO b]
181    have := Shape.owns (shape_setS (h := ({ h with bytes := upd h.bytes mb none } : Heap)) (gs := gs) (s0 := s) hG.hs (resetRec s)) hO1
182    intro b
183    rw [this b]
184    simp [hm, eq_comm]
185
186end Zlib.Gzlib.Proofs