public-gz-error.lean

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

1import ZlibF.Spec.Public.GzControl
2import ZlibF.Proof.«gzlib.c.base»
3
4namespace ZlibF.Spec.Public.GzErrorProof
5open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib Zlib.Gzlib.Spec Zlib.Gzlib.Proofs
6
7private def IsLit (r : BPtr) (t : String) : Prop :=
8  ∃ i, r = .ref (.str i) 0 ∧ strTable[i]? = some t
9
10private theorem gzerror_null_file (p : BPtr) (h : Heap) :
11    Zlib.Gzlib.gzerror none p h = .ok (.null, h) := rfl
12
13private theorem byte_get_put {h : Heap} {r : BRef} {a : Array UInt8}
14    (hg : Space.get h r = some a) (hro : Space.ro h r = false) (b : Array UInt8) :
15    Space.get (Space.put h r b) r = some b := by
16  cases r with
17  | blk id => simp [Space.get, Space.put]
18  | str id => simp [Space.ro] at hro
19  | dstate_depth id =>
20    cases hs : h.dstates id with
21    | none => simp [Space.get, hs] at hg
22    | some s => simp [Space.get, Space.put, hs]
23  | st_dist_code => simp [Space.ro] at hro
24  | st_length_code => simp [Space.ro] at hro
25
26private theorem byte_ro_put (h : Heap) (r : BRef) (a : Array UInt8) :
27    Space.ro (Space.put h r a) r = Space.ro h r := by
28  cases r <;> simp [Space.get, Space.put, Space.ro]
29
30private theorem byte_put_put {h : Heap} {r : BRef} {a : Array UInt8}
31    (hg : Space.get h r = some a) (hro : Space.ro h r = false) (b c : Array UInt8) :
32    Space.put (Space.put h r b) r c = Space.put h r c := by
33  cases r with
34  | blk id => simp [Space.put, upd_upd]
35  | str id => simp [Space.ro] at hro
36  | dstate_depth id =>
37    cases hs : h.dstates id with
38    | none => simp [Space.get, hs] at hg
39    | some s => simp [Space.put, hs, upd_upd]
40  | st_dist_code => simp [Space.ro] at hro
41  | st_length_code => simp [Space.ro] at hro
42
43/-- `void store32(int *p, int v)` writes the four little-endian bytes into an
44existing writable array and changes no other heap object. -/
45theorem store32_run {h : Heap} {r : BRef} {a : Array UInt8} {off : Nat}
46    (hg : Space.get h r = some a) (hro : Space.ro h r = false)
47    (hfit : off + 4 ≤ a.size) (v : Int32) :
48    store32 (.ref r off) v h = .ok ((), Space.put h r
49      ((((a.set! off v.toUInt32.toUInt8).set! (off + 1) (v.toUInt32 >>> 8).toUInt8).set! (off + 2) (v.toUInt32 >>> 16).toUInt8).set! (off + 3) (v.toUInt32 >>> 24).toUInt8)) := by
50  have add0 := Ptr.add_nat_ok (h := h) (r := r) (a := a) (off := off) (n := 0) hg (by omega)
51  have st0 := Ptr.store_ok (h := h) (r := r) (a := a) (off := off) (v := v.toUInt32.toUInt8) hg hro (by omega)
52  let a0 := a.set! off v.toUInt32.toUInt8
53  have hg0 := byte_get_put hg hro a0
54  have hr0 : Space.ro (Space.put h r a0) r = false := by rw [byte_ro_put, hro]
55  have add1 := Ptr.add_nat_ok (h := Space.put h r a0) (r := r) (a := a0) (off := off) (n := 1) hg0 (by simp [a0]; omega)
56  have st1 := Ptr.store_ok (h := Space.put h r a0) (r := r) (a := a0) (off := off + 1)
57    (v := (v.toUInt32 >>> 8).toUInt8) hg0 hr0 (by simp [a0]; omega)
58  let a1 := a0.set! (off + 1) (v.toUInt32 >>> 8).toUInt8
59  have hg1 : Space.get (Space.put (Space.put h r a0) r a1) r = some a1 := byte_get_put hg0 hr0 a1
60  have hr1 : Space.ro (Space.put (Space.put h r a0) r a1) r = false := by rw [byte_ro_put, byte_ro_put, hro]
61  have add2 := Ptr.add_nat_ok (h := Space.put (Space.put h r a0) r a1) (r := r) (a := a1) (off := off) (n := 2) hg1 (by simp [a1, a0]; omega)
62  have st2 := Ptr.store_ok (h := Space.put (Space.put h r a0) r a1) (r := r) (a := a1) (off := off + 2)
63    (v := (v.toUInt32 >>> 16).toUInt8) hg1 hr1 (by simp [a1, a0]; omega)
64  let a2 := a1.set! (off + 2) (v.toUInt32 >>> 16).toUInt8
65  have hg2 : Space.get (Space.put (Space.put (Space.put h r a0) r a1) r a2) r = some a2 := byte_get_put hg1 hr1 a2
66  have hr2 : Space.ro (Space.put (Space.put (Space.put h r a0) r a1) r a2) r = false := by rw [byte_ro_put, byte_ro_put, byte_ro_put, hro]
67  have add3 := Ptr.add_nat_ok (h := Space.put (Space.put (Space.put h r a0) r a1) r a2) (r := r) (a := a2) (off := off) (n := 3) hg2 (by simp [a2, a1, a0]; omega)
68  have st3 := Ptr.store_ok (h := Space.put (Space.put (Space.put h r a0) r a1) r a2) (r := r) (a := a2) (off := off + 3)
69    (v := (v.toUInt32 >>> 24).toUInt8) hg2 hr2 (by simp [a2, a1, a0]; omega)
70  unfold OkOn at add0 add1 add2 add3
71  have e0 : (Ptr.ref r off).add (0 : Int) h = .ok (.ref r off, h) := by simpa using add0
72  have e1 : (Ptr.ref r off).add (1 : Int) (Space.put h r a0) =
73      .ok (.ref r (off + 1), Space.put h r a0) := by simpa using add1
74  have e2 : (Ptr.ref r off).add (2 : Int) (Space.put (Space.put h r a0) r a1) =
75      .ok (.ref r (off + 2), Space.put (Space.put h r a0) r a1) := by simpa using add2
76  have e3 : (Ptr.ref r off).add (3 : Int) (Space.put (Space.put (Space.put h r a0) r a1) r a2) =
77      .ok (.ref r (off + 3), Space.put (Space.put (Space.put h r a0) r a1) r a2) := by simpa using add3
78  simp only [a0, a1, a2] at e1 e2 e3 st1 st2 st3
79  unfold store32
80  simp only [bind_app, e0, st0, e1, st1, e2, st2, e3, st3, pure_app]
81  simp only [a0, a1, a2] at *
82  rw [byte_put_put hg hro, byte_put_put hg hro, byte_put_put hg hro]
83
84/-- Four successive byte writes equal replacement of the corresponding array slice. -/
85theorem set_four_slice (a : Array UInt8) (off : Nat) (hfit : off + 4 ≤ a.size)
86    (b0 b1 b2 b3 : UInt8) :
87    (((a.set! off b0).set! (off + 1) b1).set! (off + 2) b2).set! (off + 3) b3 =
88      a.extract 0 off ++ #[b0, b1, b2, b3] ++ a.extract (off + 4) a.size := by
89  apply Array.ext_getElem?
90  intro j
91  simp only [Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds,
92    Array.getElem?_append, Array.size_append, Array.size_extract]
93  simp only [show (#[b0, b1, b2, b3] : Array UInt8).size = 4 from rfl]
94  have hm : min off a.size = off := Nat.min_eq_left (by omega)
95  have hlt0 : off < a.size := by omega
96  have hlt1 : off + 1 < a.size := by omega
97  have hlt2 : off + 2 < a.size := by omega
98  have hlt3 : off + 3 < a.size := by omega
99  by_cases h0 : j = off
100  · subst j
101    simp [Array.getElem?_extract, hm, hlt0, hlt1, hlt2, hlt3]
102  · by_cases h1 : j = off + 1
103    · subst j
104      simp [Array.getElem?_extract, hm, hlt0, hlt1, hlt2, hlt3,
105        show ¬ off + 1 < off from by omega]
106    · by_cases h2 : j = off + 2
107      · subst j
108        simp [Array.getElem?_extract, hm, hlt0, hlt1, hlt2, hlt3,
109          show ¬ off + 2 < off from by omega]
110      · by_cases h3 : j = off + 3
111        · subst j
112          simp [Array.getElem?_extract, hm, hlt0, hlt1, hlt2, hlt3,
113            show ¬ off + 3 < off from by omega]
114        · by_cases hbefore : j < off
115          · have hj4 : j < off + 4 := by omega
116            have hja : j < a.size := by omega
117            simp [h0, h1, h2, h3, Ne.symm h0, Ne.symm h1, Ne.symm h2, Ne.symm h3,
118              hbefore, hj4, hja, Array.getElem?_extract, hm, Array.getElem?_eq_getElem]
119          · have hafter : off + 4 ≤ j := by omega
120            have hj4 : ¬ j < off + 4 := by omega
121            have heq : off + 4 + (j - (off + 4)) = j := by omega
122            by_cases hja : j < a.size
123            · have htail : j - (off + 4) < a.size - (off + 4) := by omega
124              simp [h0, h1, h2, h3, Ne.symm h0, Ne.symm h1, Ne.symm h2, Ne.symm h3,
125                hbefore, hj4, htail, hja, heq, Array.getElem?_extract, hm]
126            · have htail : ¬ j - (off + 4) < a.size - (off + 4) := by omega
127              simp [h0, h1, h2, h3, Ne.symm h0, Ne.symm h1, Ne.symm h2, Ne.symm h3,
128                hbefore, hj4, htail, hja, Array.getElem?_extract, hm, Array.getElem?_eq_none]
129
130/-- The little-endian four-byte store replaces exactly its requested slice. -/
131theorem store32_slice_run {h : Heap} {r : BRef} {a : Array UInt8} {off : Nat}
132    (hg : Space.get h r = some a) (hro : Space.ro h r = false)
133    (hfit : off + 4 ≤ a.size) (v : Int32) :
134    store32 (.ref r off) v h = .ok ((), Space.put h r
135      (a.extract 0 off ++ #[v.toUInt32.toUInt8, (v.toUInt32 >>> 8).toUInt8,
136        (v.toUInt32 >>> 16).toUInt8, (v.toUInt32 >>> 24).toUInt8] ++
137        a.extract (off + 4) a.size)) := by
138  rw [store32_run hg hro hfit v, set_four_slice a off hfit]
139
140/-- The byte-shift expressions implement the mathematical little-endian encoding. -/
141theorem int32_bytes (v : Int32) :
142    (List.range 4).map (fun j => UInt8.ofNat (v.toUInt32.toNat / 256 ^ j % 256)) =
143      [v.toUInt32.toUInt8, (v.toUInt32 >>> 8).toUInt8,
144        (v.toUInt32 >>> 16).toUInt8, (v.toUInt32 >>> 24).toUInt8] := by
145  have hr : List.range 4 = [0, 1, 2, 3] := by decide
146  rw [hr]
147  simp only [List.map_cons, List.map_nil, List.cons.injEq, and_true,
148    Nat.pow_zero, Nat.reducePow, Nat.div_one]
149  repeat' constructor
150  all_goals apply UInt8.toNat_inj.mp
151  all_goals simp [UInt8.toNat_ofNat', UInt32.toNat_toUInt8, UInt32.toNat_shiftRight,
152    Nat.shiftRight_eq_div_pow]
153
154/-- The return-text part of `gzerror` after the optional error-code write. -/
155def errorMessage (s : GzState) : M BPtr := do
156  if s.err == Z_MEM_ERROR then Zlib.GzFs.strLit "out of memory"
157  else if s.msg == .null then Zlib.GzFs.strLit ""
158  else pure s.msg
159
160/-- A valid-mode `gzerror` reads the state once, performs the optional write,
161and returns the corresponding message. -/
162theorem gzerror_split {h : Heap} {i : Nat} {s : GzState}
163    (hs : h.gzstates i = some s) (hm : s.mode = GZ_READ ∨ s.mode = GZ_WRITE) (p : BPtr) :
164    Zlib.Gzlib.gzerror (hnd i) p h =
165      (do
166        if p != (Ptr.null : BPtr) then store32 p s.err
167        errorMessage s) h := by
168  unfold Zlib.Gzlib.gzerror errorMessage
169  rcases hm with hm | hm <;> gsimp [hs, hm, GZ_READ, GZ_WRITE]
170
171/-- Returning an error message never changes the heap. Literal results identify
172an actual static source string; otherwise the original message pointer is returned. -/
173theorem errorMessage_run (h : Heap) (s : GzState) :
174    ∃ p, errorMessage s h = .ok (p, h) ∧
175      (if s.err = Z_MEM_ERROR then IsLit p "out of memory"
176       else if s.msg = .null then IsLit p "" else p = s.msg) := by
177  have lit : ∀ t : String, t ∈ strTable → ∃ p, Zlib.GzFs.strLit t h = .ok (p, h) ∧ IsLit p t := by
178    intro t ht
179    obtain ⟨i, hr, hi⟩ := strLitRef_of_mem (h := h) ht
180    exact ⟨_, hr, i, rfl, hi⟩
181  by_cases he : s.err = Z_MEM_ERROR
182  · obtain ⟨p, hp, hl⟩ := lit "out of memory" (by decide +kernel)
183    exact ⟨p, by simpa [errorMessage, he] using hp, by simpa [he] using hl⟩
184  · by_cases hn : s.msg = .null
185    · obtain ⟨p, hp, hl⟩ := lit "" (by decide +kernel)
186      exact ⟨p, by simpa [errorMessage, he, hn] using hp, by simpa [he, hn] using hl⟩
187    · exact ⟨s.msg, by simp [errorMessage, he, hn], by simp [he, hn]⟩
188
189
190private theorem lit_static (h : Heap) (p : BPtr) (s : String) (hl : IsLit p s) :
191    StaticString h p s := by
192  obtain ⟨i, rfl, hi⟩ := hl
193  exact ⟨i, rfl, by simp [hi, strBytes], rfl⟩
194
195/-- `const char *gzerror(gzFile file, int *errnum)` returns the specified
196message and writes the optional error number without accessing unrelated memory. -/
197theorem gzerror : Goal.gzerror := by
198  constructor
199  · intro h p
200    exact gzerror_null_file p h
201  · intro h i s p hv hout
202    have hs := hv.1
203    have hm := hv.2.1
204    by_cases hp : p = .null
205    · subst p
206      obtain ⟨q, hmsg, hdesc⟩ := errorMessage_run h s
207      refine ⟨q, h, ?_, Or.inl ⟨rfl, rfl⟩, ?_⟩
208      · change Zlib.Gzlib.gzerror (hnd i) .null h = .ok (q, h)
209        rw [gzerror_split hs hm]
210        simpa using hmsg
211      · by_cases he : s.err = Z_MEM_ERROR
212        · simp only [he, ite_true] at hdesc ⊢
213          exact lit_static h q _ hdesc
214        · simp only [he, ite_false] at hdesc ⊢
215          by_cases hn : s.msg = .null
216          · simp only [hn, ite_true] at hdesc ⊢
217            exact lit_static h q _ hdesc
218          · simp only [hn, ite_false] at hdesc ⊢
219            exact hdesc
220    · have hbuf := hout hp
221      rcases hbuf with hn | ⟨_, hw, _⟩
222      · omega
223      · have hw' := hw rfl
224        rcases hw' with ⟨hnull, _⟩ | ⟨r, off, a, hp', hg, hro, hfit⟩
225        · exact (hp hnull).elim
226        · subst p
227          let arr := a.extract 0 off ++ #[s.err.toUInt32.toUInt8, (s.err.toUInt32 >>> 8).toUInt8,
228            (s.err.toUInt32 >>> 16).toUInt8, (s.err.toUInt32 >>> 24).toUInt8] ++ a.extract (off + 4) a.size
229          let after := Space.put h r arr
230          have hstore : store32 (.ref r off) s.err h = .ok ((), after) :=
231            store32_slice_run hg hro hfit s.err
232          obtain ⟨q, hmsg, hdesc⟩ := errorMessage_run after s
233          refine ⟨q, after, ?_, ?_, ?_⟩
234          · change Zlib.Gzlib.gzerror (hnd i) (.ref r off) h = .ok (q, after)
235            rw [gzerror_split hs hm]
236            simp [bind_app, hstore, hmsg]
237          · right
238            refine ⟨r, off, a, rfl, hg, hro, ?_, ?_⟩
239            · simpa [intBytes] using hfit
240            · simp [intBytes, int32_bytes, after, arr]
241          · by_cases he : s.err = Z_MEM_ERROR
242            · simp only [he, ite_true] at hdesc ⊢
243              exact lit_static after q _ hdesc
244            · simp only [he, ite_false] at hdesc ⊢
245              by_cases hn : s.msg = .null
246              · simp only [hn, ite_true] at hdesc ⊢
247                exact lit_static after q _ hdesc
248              · simp only [hn, ite_false] at hdesc ⊢
249                exact hdesc
250
251
252#print axioms gzerror
253end ZlibF.Spec.Public.GzErrorProof