gzlib.c.simple.lean

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

1import ZlibF.Proof.«gzlib.c.error»
2
3/-!
4# gzlib.c: `gz_intmax`, `GT_OFF`, `gzbuffer`, `gzeof`, `gztell64`, `gztell`, `gzerror`, `gzclearerr`
5
6The functions that read or write a few fields. Each theorem says exactly what is returned and what the heap becomes;
7the null-handle case is separate (`*_null`).
8
9`PosInv s` is the numeric part of the position bookkeeping (`docs/proof/gzip.md`, "Positions, seeking and error ownership"):
10`skip` is not negative and `x.pos + skip` is a `z_off64_t`. `gz_reset` establishes it (`resetRec_posInv`), `gzseek64`
11keeps it (`gzlib.c.seek`); the read and write functions have to keep it, and `gztell64` needs it to avoid signed overflow.
12-/
13
14namespace Zlib.Gzlib.Spec
15open C Zlib.GzFs Zlib.Gzguts
16
17/-- The distance `gztell64` adds to `x.pos`: `skip`, unless a read has come up short. -/
18def tellSkip (s : GzState) : Int64 := if s.past != 0 then 0 else s.skip
19
20/-- `gztell64`'s result as a number. -/
21def tellPos (s : GzState) : Int := s.x.pos.toInt + (tellSkip s).toInt
22
23/-- The numeric invariant of the position fields. -/
24structure PosInv (s : GzState) : Prop where
25  skip_nonneg : 0 ≤ s.skip.toInt
26  lo : -9223372036854775808 ≤ tellPos s
27  hi : tellPos s < 9223372036854775808
28
29/-- `z_off_t` is `long`: the same 64 bits as `z_off64_t`. -/
30def IsLit (r : BPtr) (t : String) : Prop := ∃ i, r = .ref (.str i) 0 ∧ strTable[i]? = some t
31
32/-- The record `gzclearerr` has before it calls `gz_error`: a reader clears `eof` and `past`. -/
33def clearRec (s : GzState) : GzState := if s.mode == GZ_READ then { s with eof := 0, past := 0 } else s
34
35end Zlib.Gzlib.Spec
36
37namespace Zlib.Gzlib.Proofs
38open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib Zlib.Gzlib.Spec
39
40/-! ## gz_intmax, GT_OFF -/
41
42/-- `gz_intmax()` returns `INT_MAX` (2147483647) and does not change the heap. No precondition. -/
43theorem gz_intmax_run (h : Heap) : gz_intmax h = .ok (2147483647, h) := rfl
44
45/-- `GT_OFF(x)` is false for every `x`: `sizeof(int) == sizeof(z_off64_t)` is false, and `gz_intmax` is not called. -/
46theorem GT_OFF_run (x : UInt32) (h : Heap) : GT_OFF x h = .ok (false, h) := by
47  simp [GT_OFF]
48
49/-! ## gzbuffer -/
50
51/-- `gzbuffer(NULL, size)` returns -1 and does not change the heap, for every `size`. -/
52theorem gzbuffer_null (size : UInt32) (h : Heap) : gzbuffer none size h = .ok (-1, h) := rfl
53
54/-- Doubling `size` overflows exactly when `size` is `2^31` or more. -/
55theorem double_overflow_iff (size : UInt32) : (size <<< 1) < size ↔ 2 ^ 31 ≤ size.toNat := by
56  rw [UInt32.lt_iff_toNat_lt, UInt32.toNat_shiftLeft]
57  have := size.toNat_lt
58  simp only [UInt32.toNat_ofNat, Nat.reducePow] at *
59  rcases Nat.lt_or_ge size.toNat (2 ^ 31) with h1 | h1
60  · have : (1 : UInt32).toNat % 32 = 1 := rfl
61    simp [this]; omega
62  · have : (1 : UInt32).toNat % 32 = 1 := rfl
63    simp [this]; omega
64
65/-- **gzbuffer.** `-1` and no change when buffers exist (`size ≠ 0`) or `size` cannot be doubled; otherwise `want` becomes
66`max(size, 8)` and the result is 0. -/
67theorem gzbuffer_run {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (size : UInt32) :
68    gzbuffer (hnd gs) size h =
69      if s.size ≠ 0 ∨ (size <<< 1) < size then .ok (-1, h)
70      else .ok (0, setS h gs { s with want := if size < 8 then 8 else size }) := by
71  have hs := hG.hs
72  have hm : s.mode = GZ_READ ∨ s.mode = GZ_WRITE := hG.mode
73  have hne : s.mode ≠ GZ_READ ∨ s.mode ≠ GZ_WRITE := by
74    rcases hm with h1 | h1 <;> simp [h1, GZ_READ, GZ_WRITE]
75  unfold gzbuffer
76  by_cases h1 : s.size ≠ 0
77  · gsimp [hs, h1, hm]
78  · have h1' : s.size = 0 := by simpa using h1
79    by_cases h2 : (size <<< 1) < size
80    · gsimp [hs, h1', h2, hm]
81    · rcases hm with hm | hm <;> gsimp [hs, h1', h2, hm, GZ_READ, GZ_WRITE]
82
83/-- `gzbuffer` on a handle with `GzGood`: no fault; either the result is -1 and the heap is unchanged (buffers exist, or `size >= 2^31`), or the result is 0, `want` is `max(size, 8)`, nothing else changes and `GzGood` still holds. Caller condition: a handle returned by `gzopen`/`gzdopen`, not closed. -/
84theorem gzbuffer_safe {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (size : UInt32) :
85    ∃ r h', C.run (gzbuffer (hnd gs) size) h = .ok (r, h') ∧
86      ((s.size ≠ 0 ∨ 2 ^ 31 ≤ size.toNat) ∧ r = -1 ∧ h' = h ∨
87       (s.size = 0 ∧ size.toNat < 2 ^ 31) ∧ r = 0 ∧
88        h' = setS h gs { s with want := if size < 8 then 8 else size } ∧
89        GzGood h' gs { s with want := if size < 8 then 8 else size }) := by
90  have hr := gzbuffer_run hG size
91  have hd := double_overflow_iff size
92  by_cases hc : s.size ≠ 0 ∨ (size <<< 1) < size
93  · rw [ite_eq_left hc] at hr
94    refine ⟨-1, h, hr, Or.inl ⟨?_, rfl, rfl⟩⟩
95    rcases hc with hc | hc
96    · exact Or.inl hc
97    · exact Or.inr (hd.mp hc)
98  · rw [ite_eq_right hc] at hr
99    have hc1 : s.size = 0 := Classical.byContradiction fun hh => hc (Or.inl hh)
100    have hc2 : ¬ (size <<< 1) < size := fun hh => hc (Or.inr hh)
101    refine ⟨0, _, hr, Or.inr ⟨⟨hc1, ?_⟩, rfl, rfl, ?_⟩⟩
102    · exact Classical.byContradiction fun hh => hc2 (hd.mpr (by omega))
103    · exact GzGood.withRec hG (Or.inl rfl) rfl rfl rfl rfl (fun hh => hG.memerr hh)
104
105/-! ## gzeof -/
106
107/-- `gzeof(NULL)` returns 0 and does not change the heap. -/
108theorem gzeof_null (h : Heap) : gzeof none h = .ok (0, h) := rfl
109
110/-- `gzeof` on a handle with `GzGood`: returns `past` for a reader and 0 for a writer; the heap is unchanged. -/
111theorem gzeof_run {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) :
112    gzeof (hnd gs) h = .ok ((if s.mode = GZ_READ then s.past else 0), h) := by
113  have hs := hG.hs
114  unfold gzeof
115  rcases hG.mode with hm | hm
116  · gsimp [hs, hm]
117  · gsimp [hs, hm, GZ_READ, GZ_WRITE]
118
119/-! ## gztell64, gztell -/
120
121/-- `gztell64(NULL)` returns -1 and does not change the heap. -/
122theorem gztell64_null (h : Heap) : gztell64 none h = .ok (-1, h) := rfl
123
124theorem gztell64_run {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hP : PosInv s) :
125    gztell64 (hnd gs) h = .ok (Int64.ofInt (tellPos s), h) := by
126  have hs := hG.hs
127  have e := i64add_run s.x.pos (tellSkip s) (by have := hP.lo; unfold tellPos at this; omega)
128    (by have := hP.hi; unfold tellPos at this; omega) h
129  unfold gztell64
130  rcases hG.mode with hm | hm
131  · by_cases hp : s.past = 0
132    · gsimp [hs, hm, hp]
133      simpa [tellSkip, tellPos, hp] using e
134    · gsimp [hs, hm, hp]
135      simpa [tellSkip, tellPos, hp] using e
136  · by_cases hp : s.past = 0
137    · gsimp [hs, hm, hp, GZ_READ, GZ_WRITE]
138      simpa [tellSkip, tellPos, hp] using e
139    · gsimp [hs, hm, hp, GZ_READ, GZ_WRITE]
140      simpa [tellSkip, tellPos, hp] using e
141
142/-- **gztell64.** The result is `x.pos + (past ? 0 : skip)` as a number; the heap is unchanged. -/
143theorem gztell64_spec {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hP : PosInv s) :
144    ∃ r, C.run (gztell64 (hnd gs)) h = .ok (r, h) ∧ r.toInt = tellPos s := by
145  refine ⟨_, gztell64_run hG hP, i64_toInt_ofInt hP.lo hP.hi⟩
146
147/-- `gztell` on a handle with `GzGood` and `PosInv`: returns `x.pos + (past ? 0 : skip)` as a number; no fault (`PosInv` rules out signed overflow); the heap is unchanged. -/
148theorem gztell_run {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hP : PosInv s) :
149    gztell (hnd gs) h = .ok (Int64.ofInt (tellPos s), h) := by
150  unfold gztell
151  simp [bind_app, gztell64_run hG hP]
152
153/-- `gztell(NULL)` returns -1 and does not change the heap. -/
154theorem gztell_null (h : Heap) : gztell none h = .ok (-1, h) := rfl
155
156/-! ## gzerror -/
157
158/-- `gzerror(NULL, errnum)` returns NULL and does not change the heap, whatever `errnum` is. -/
159theorem gzerror_null_file (errnum : BPtr) (h : Heap) : gzerror none errnum h = .ok (.null, h) := rfl
160
161/-- **gzerror, no `errnum`.** The result is the static text `"out of memory"` for `Z_MEM_ERROR`, else the message of the
162handle, else the static empty text. The heap is unchanged. -/
163theorem gzerror_run {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) :
164    ∃ r, gzerror (hnd gs) .null h = .ok (r, h) ∧
165      ((s.err = Z_MEM_ERROR ∧ IsLit r "out of memory") ∨
166       (s.err ≠ Z_MEM_ERROR ∧ s.msg = .null ∧ IsLit r "") ∨
167       (s.err ≠ Z_MEM_ERROR ∧ s.msg ≠ .null ∧ r = s.msg)) := by
168  have hs := hG.hs
169  have lit : ∀ t : String, t ∈ strTable → ∃ r, strLit t h = .ok (r, h) ∧ IsLit r t := fun t ht => by
170    obtain ⟨i, e, hi⟩ := strLitRef_of_mem (h := h) ht
171    exact ⟨_, e, i, rfl, hi⟩
172  have hm : s.mode = GZ_READ ∨ s.mode = GZ_WRITE := hG.mode
173  by_cases he : s.err = Z_MEM_ERROR
174  · obtain ⟨r, e1, e2⟩ := lit "out of memory" (by decide +kernel)
175    refine ⟨r, ?_, Or.inl ⟨he, e2⟩⟩
176    unfold gzerror
177    rcases hm with hm | hm <;> gsimp [hs, hm, he, GZ_READ, GZ_WRITE, e1]
178  · by_cases hn : s.msg = .null
179    · obtain ⟨r, e1, e2⟩ := lit "" (by decide +kernel)
180      refine ⟨r, ?_, Or.inr (Or.inl ⟨he, hn, e2⟩)⟩
181      unfold gzerror
182      rcases hm with hm | hm <;> gsimp [hs, hm, he, hn, GZ_READ, GZ_WRITE, e1]
183    · refine ⟨s.msg, ?_, Or.inr (Or.inr ⟨he, hn, rfl⟩)⟩
184      unfold gzerror
185      rcases hm with hm | hm <;> gsimp [hs, hm, he, hn, GZ_READ, GZ_WRITE]
186
187
188/-! ## gzclearerr -/
189
190/-- `gzclearerr(NULL)` does nothing: no fault, the heap is unchanged. -/
191theorem gzclearerr_null (h : Heap) : gzclearerr none h = .ok ((), h) := rfl
192
193theorem GzGood.clearRec {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) : GzGood (setS h gs (clearRec s)) gs (clearRec s) := by
194  refine GzGood.withRec hG (Or.inl (by unfold Spec.clearRec; split <;> rfl)) (by unfold Spec.clearRec; split <;> rfl)
195    (by unfold Spec.clearRec; split <;> rfl) (by unfold Spec.clearRec; split <;> rfl) (by unfold Spec.clearRec; split <;> rfl)
196    (by intro hh; have := hG.memerr (by unfold Spec.clearRec at hh; split at hh <;> exact hh); unfold Spec.clearRec; split <;> exact this)
197
198/-- `gzclearerr` on a handle with `GzGood`: a reader clears `eof` and `past`; the error code becomes `Z_OK` and the message block is freed (`gz_error(state, Z_OK, NULL)`); nothing else changes. Caller condition: an open handle. -/
199theorem gzclearerr_run {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) :
200    gzclearerr (hnd gs) h = .ok ((), setS (freeStr h s.msg) gs (errNull (clearRec s) Z_OK)) := by
201  have hs := hG.hs
202  unfold gzclearerr
203  rcases hG.msg with hn | ⟨mb, hm, a, ha, hro, k, hz⟩
204  · rcases hG.mode with hmo | hmo <;> gsimp [hs, hn, hmo, gz_error, clearRec, errNull, GZ_READ, GZ_WRITE]
205  · have hne : s.err ≠ Z_MEM_ERROR := fun h' => by have := hG.memerr h'; rw [hm] at this; cases this
206    rcases hG.mode with hmo | hmo <;>
207      gsimp [hs, hm, hne, hmo, freeB_blk_setS ha hro, freeB_blk_run ha hro, gz_error, clearRec, errNull, GZ_READ, GZ_WRITE]
208
209/-- **gzclearerr, safety and effect.** -/
210theorem gzclearerr_safe {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) :
211    ∃ h', C.run (gzclearerr (hnd gs)) h = .ok ((), h') ∧ h' = setS (freeStr h s.msg) gs (errNull (clearRec s) Z_OK) ∧
212      GzGood h' gs (errNull (clearRec s) Z_OK) := by
213  refine ⟨_, gzclearerr_run hG, rfl, ?_⟩
214  have := GzGood.afterErr (GzGood.clearRec hG) Z_OK
215  have e : (clearRec s).msg = s.msg := by unfold Spec.clearRec; split <;> rfl
216  rw [e] at this
217  simpa using this
218
219end Zlib.Gzlib.Proofs