gzlib.c.base.lean

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

1import ZlibF.Zlib.«gzlib.c»
2
3/-!
4# gzlib.c: the representation invariant of a gz handle and the rules that every proof of gzlib.c, gzread.c, gzwrite.c
5and gzclose.c uses
6
7A `gzFile` is a pointer into the `gzstates` table (`some (.in_gzstate_x gs)`); `gs` is the block number of the
8`gz_state` record `s`. The invariant `GzGood h gs s` has the shape of `Good` of `inflate.c.base`:
9
10* the record is live (`hs`) and its mode is `GZ_READ` or `GZ_WRITE` (what `gz_open` makes of the mode string);
11* `path` is a NUL-terminated writable byte block, `msg` is `NULL` or the same kind of block, `in` and `out` are `NULL` or
12  writable byte blocks, and the four blocks are pairwise different;
13* `Z_MEM_ERROR` goes with no message (`gz_error` frees the message before it records an error);
14* `Uniq` (a block number holds an object of at most one table) and `Fresh` (block numbers from `nextBlk` on are unused).
15
16What is not in `GzGood`, on purpose: the pointer `x.next` (it dangles after a direct read, issue 5 of
17`docs/spec/api/gz-file.md`; `NextOk` is a separate hypothesis of the theorems that dereference it), and the
18state of the embedded stream `strm` (the read and write proofs add it).
19-/
20
21namespace Zlib.Gzlib.Spec
22open C Zlib.GzFs Zlib.Gzguts
23
24/-- The heap with the `gz_state` record `gs` replaced. -/
25def setS (h : Heap) (gs : Nat) (s : GzState) : Heap := { h with gzstates := upd h.gzstates gs (some s) }
26
27/-- 1 if the table entry holds an object, else 0. -/
28def cnt {α : Type} (o : Option α) : Nat := if o.isSome then 1 else 0
29
30@[simp] theorem cnt_none {α : Type} : cnt (none : Option α) = 0 := rfl
31@[simp] theorem cnt_some {α : Type} (a : α) : cnt (some a) = 1 := rfl
32
33/-- A block number holds an object of at most one table. -/
34def Uniq (h : Heap) : Prop := ∀ b,
35  cnt (h.bytes b) + cnt (h.words b) + cnt (h.streams b) + cnt (h.gzheaders b) + cnt (h.dstates b) + cnt (h.istates b) +
36  cnt (h.gzstates b) ≤ 1
37
38/-- The two heaps hold an object in the same tables at the same block numbers (the objects may differ). -/
39def Shape (h h' : Heap) : Prop := ∀ b, (h'.bytes b).isSome = (h.bytes b).isSome ∧ (h'.words b).isSome = (h.words b).isSome ∧
40  (h'.streams b).isSome = (h.streams b).isSome ∧ (h'.gzheaders b).isSome = (h.gzheaders b).isSome ∧
41  (h'.dstates b).isSome = (h.dstates b).isSome ∧ (h'.istates b).isSome = (h.istates b).isSome ∧
42  (h'.gzstates b).isSome = (h.gzstates b).isSome
43
44/-- The block of a byte pointer into a heap block, if it is one. -/
45def ptrBlk : BPtr → Option Nat
46  | .ref (.blk b) _ => some b
47  | _ => none
48
49/-- `p` is the start of the writable byte block `b`, which holds a NUL byte (a C string owned by the handle). -/
50def StrBlk (h : Heap) (p : BPtr) (b : Nat) : Prop :=
51  p = .ref (.blk b) 0 ∧ ∃ a : Array UInt8, h.bytes b = some a ∧ h.ro b = false ∧ ∃ k : Nat, a[k]? = some 0
52
53/-- `NULL` or the start of a writable byte block. -/
54def OptBlk (h : Heap) (p : BPtr) : Prop := p = .null ∨ ∃ b a, p = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false
55
56/-- The representation invariant of the handle whose `gz_state` is the record `s` at block `gs`. -/
57structure GzGood (h : Heap) (gs : Nat) (s : GzState) : Prop where
58  hs : h.gzstates gs = some s
59  mode : s.mode = GZ_READ ∨ s.mode = GZ_WRITE
60  path : ∃ pb, StrBlk h s.path pb
61  msg : s.msg = .null ∨ ∃ mb, StrBlk h s.msg mb
62  inb : OptBlk h s.in
63  outb : OptBlk h s.out
64  nodup : ([s.path, s.msg, s.in, s.out].filterMap ptrBlk).Nodup
65  memerr : s.err = Z_MEM_ERROR → s.msg = .null
66  uniq : Uniq h
67  fresh : Fresh h
68
69/-- `x.next` can be advanced by up to `x.have` bytes: it is `NULL` with nothing buffered, or points into a live array with
70`x.have` bytes after it; and it does not point into the message block. (After a direct read it can dangle: that case is
71excluded by this hypothesis, and `seekTail_dangling_ub` shows the fault.) -/
72def NextOk (h : Heap) (s : GzState) : Prop :=
73  ((s.x.next = .null ∧ s.x.«have» = 0) ∨
74    ∃ r a off, s.x.next = .ref r off ∧ Space.get h r = some a ∧ off + s.x.«have».toNat ≤ a.size) ∧
75  (∀ b, ptrBlk s.x.next = some b → ptrBlk s.msg ≠ some b)
76
77/-- The pointer advanced by `n` bytes (`Ptr.add` when it does not fault). -/
78def padv : BPtr → Nat → BPtr
79  | .null, _ => .null
80  | .ref r o, n => .ref r (o + n)
81
82/-- The handle pointer of the record at block `gs`. -/
83def hnd (gs : Nat) : GzFilePtr := some (.in_gzstate_x gs)
84
85end Zlib.Gzlib.Spec
86
87namespace Zlib.Gzlib.Proofs
88open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib Zlib.Gzlib.Spec
89
90@[simp] theorem setS_gz_same (h : Heap) (gs : Nat) (s : GzState) : (setS h gs s).gzstates gs = some s := by
91  simp [setS]
92@[simp] theorem setS_gz_ne (h : Heap) (gs x : Nat) (s : GzState) (hx : x ≠ gs) :
93    (setS h gs s).gzstates x = h.gzstates x := by simp [setS, upd_ne _ _ _ _ hx]
94@[simp] theorem setS_bytes (h : Heap) (gs : Nat) (s : GzState) : (setS h gs s).bytes = h.bytes := rfl
95@[simp] theorem setS_words (h : Heap) (gs : Nat) (s : GzState) : (setS h gs s).words = h.words := rfl
96@[simp] theorem setS_streams (h : Heap) (gs : Nat) (s : GzState) : (setS h gs s).streams = h.streams := rfl
97@[simp] theorem setS_gzheaders (h : Heap) (gs : Nat) (s : GzState) : (setS h gs s).gzheaders = h.gzheaders := rfl
98@[simp] theorem setS_dstates (h : Heap) (gs : Nat) (s : GzState) : (setS h gs s).dstates = h.dstates := rfl
99@[simp] theorem setS_istates (h : Heap) (gs : Nat) (s : GzState) : (setS h gs s).istates = h.istates := rfl
100@[simp] theorem setS_ro (h : Heap) (gs : Nat) (s : GzState) : (setS h gs s).ro = h.ro := rfl
101@[simp] theorem setS_nextBlk (h : Heap) (gs : Nat) (s : GzState) : (setS h gs s).nextBlk = h.nextBlk := rfl
102@[simp] theorem setS_nalloc (h : Heap) (gs : Nat) (s : GzState) : (setS h gs s).nalloc = h.nalloc := rfl
103@[simp] theorem setS_allocOk (h : Heap) (gs : Nat) (s : GzState) : (setS h gs s).allocOk = h.allocOk := rfl
104@[simp] theorem setS_garbage (h : Heap) (gs : Nat) (s : GzState) : (setS h gs s).garbage = h.garbage := rfl
105@[simp] theorem setS_static (h : Heap) (gs : Nat) (s : GzState) : (setS h gs s).static = h.static := rfl
106@[simp] theorem setS_setS (h : Heap) (gs : Nat) (s s' : GzState) : setS (setS h gs s) gs s' = setS h gs s' := by
107  simp [setS, upd_upd]
108
109/-! ### Reading and writing the record and its fields -/
110
111@[simp] theorem castState_hnd (gs : Nat) : castState (hnd gs) = some (.tab gs) := rfl
112@[simp] theorem castFile_tab (gs : Nat) : castFile (some (.tab gs)) = hnd gs := rfl
113@[simp] theorem strmOf_tab (gs : Nat) : strmOf (some (.tab gs)) = some (.in_gzstate_strm gs) := rfl
114@[simp] theorem hnd_isNone (gs : Nat) : (hnd gs).isNone = false := rfl
115
116theorem ldS_run {h : Heap} {gs : Nat} {s : GzState} (e : h.gzstates gs = some s) :
117    ldS (some (.tab gs)) h = .ok (s, h) := ldGzState_tab e
118
119theorem updS_run {h : Heap} {gs : Nat} {s : GzState} (e : h.gzstates gs = some s) (f : GzState → GzState) :
120    updS (some (.tab gs)) f h = .ok ((), setS h gs (f s)) := by
121  unfold updS
122  simp [bind_app, ldGzState_tab e, stGzState_tab e, setS]
123
124theorem updX_run {h : Heap} {gs : Nat} {s : GzState} (e : h.gzstates gs = some s) (f : GzFile → GzFile) :
125    updX (some (.tab gs)) f h = .ok ((), setS h gs { s with x := f s.x }) := by
126  unfold updX; exact updS_run e _
127
128theorem ldZ_run {h : Heap} {gs : Nat} {s : GzState} (e : h.gzstates gs = some s) :
129    ldZ (some (.in_gzstate_strm gs)) h = .ok (s.strm, h) := by
130  unfold ldZ
131  exact ldZStream_ok (r := .in_gzstate_strm gs) (v := s.strm) (by simp [ZStreamRef.get, e])
132
133theorem updZ_run {h : Heap} {gs : Nat} {s : GzState} (e : h.gzstates gs = some s) (f : ZStream → ZStream) :
134    updZ (some (.in_gzstate_strm gs)) f h = .ok ((), setS h gs { s with strm := f s.strm }) := by
135  unfold updZ
136  have e1 : ldZStream (some (.in_gzstate_strm gs)) h = .ok (s.strm, h) := ldZ_run e
137  simp only [bind_app, e1]
138  rw [stZStream_ok (r := .in_gzstate_strm gs) (v := s.strm) (by simp [ZStreamRef.get, e]) rfl]
139  simp [ZStreamRef.put, e, setS]
140
141/-! ### The arithmetic of the translation -/
142
143theorem i64chk_ok (r : Int) (h : -9223372036854775808 ≤ r ∧ r < 9223372036854775808) :
144    i64chk r = pure (Int64.ofInt r) := by
145  simp [i64chk, h]
146
147theorem i64add_run (a b : Int64) (hlo : -9223372036854775808 ≤ a.toInt + b.toInt)
148    (hhi : a.toInt + b.toInt < 9223372036854775808) (h : Heap) :
149    i64add a b h = .ok (Int64.ofInt (a.toInt + b.toInt), h) := by
150  simp [i64add, i64chk, hlo, hhi]
151
152theorem i64sub_run (a b : Int64) (hlo : -9223372036854775808 ≤ a.toInt - b.toInt)
153    (hhi : a.toInt - b.toInt < 9223372036854775808) (h : Heap) :
154    i64sub a b h = .ok (Int64.ofInt (a.toInt - b.toInt), h) := by
155  simp [i64sub, i64chk, hlo, hhi]
156
157theorem i64neg_run (a : Int64) (hlo : -9223372036854775808 ≤ -a.toInt)
158    (hhi : -a.toInt < 9223372036854775808) (h : Heap) :
159    i64neg a h = .ok (Int64.ofInt (-a.toInt), h) := by
160  simp [i64neg, i64chk, hlo, hhi]
161
162theorem i64add_ub (a b : Int64) (h : Heap) (hb : ¬ (-9223372036854775808 ≤ a.toInt + b.toInt ∧ a.toInt + b.toInt < 9223372036854775808)) :
163    i64add a b h = .error (.ub "signed overflow (long)") := by
164  show i64chk _ h = _
165  unfold i64chk; simp only [hb, ite_false]; rfl
166
167theorem i64sub_ub (a b : Int64) (h : Heap) (hb : ¬ (-9223372036854775808 ≤ a.toInt - b.toInt ∧ a.toInt - b.toInt < 9223372036854775808)) :
168    i64sub a b h = .error (.ub "signed overflow (long)") := by
169  show i64chk _ h = _
170  unfold i64chk; simp only [hb, ite_false]; rfl
171
172theorem i64neg_ub (a : Int64) (h : Heap) (hb : ¬ (-9223372036854775808 ≤ -a.toInt ∧ -a.toInt < 9223372036854775808)) :
173    i64neg a h = .error (.ub "signed overflow (long)") := by
174  show i64chk _ h = _
175  unfold i64chk; simp only [hb, ite_false]; rfl
176
177theorem bmod64 (n : Int) (h1 : -9223372036854775808 ≤ n) (h2 : n < 9223372036854775808) :
178    n.bmod Int64.size = n := by
179  have : Int64.size = 18446744073709551616 := rfl
180  rw [this]
181  exact Int.bmod_eq_of_le (by omega) (by omega)
182
183theorem i64_toInt_ofInt {n : Int} (h1 : -9223372036854775808 ≤ n) (h2 : n < 9223372036854775808) :
184    (Int64.ofInt n).toInt = n := by
185  rw [Int64.toInt_ofInt]; exact bmod64 n h1 h2
186
187theorem u32ToI64_toInt (u : UInt32) : (u32ToI64 u).toInt = (u.toNat : Int) := by
188  unfold u32ToI64
189  rw [Int64.toInt_ofNat']
190  have := u.toNat_lt
191  exact bmod64 _ (by omega) (by omega)
192
193/-! ### Preserving the invariant -/
194
195theorem Shape.refl (h : Heap) : Shape h h := fun _ => ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
196
197theorem Shape.trans {h1 h2 h3 : Heap} (a : Shape h1 h2) (b : Shape h2 h3) : Shape h1 h3 := by
198  intro x
199  obtain ⟨a1, a2, a3, a4, a5, a6, a7⟩ := a x
200  obtain ⟨b1, b2, b3, b4, b5, b6, b7⟩ := b x
201  exact ⟨b1.trans a1, b2.trans a2, b3.trans a3, b4.trans a4, b5.trans a5, b6.trans a6, b7.trans a7⟩
202
203theorem Shape.uniq {h h' : Heap} (hS : Shape h h') (hU : Uniq h) : Uniq h' := by
204  intro b
205  obtain ⟨e1, e2, e3, e4, e5, e6, e7⟩ := hS b
206  have := hU b
207  simp only [cnt, e1, e2, e3, e4, e5, e6, e7] at this ⊢
208  exact this
209
210theorem Shape.live {h h' : Heap} (hS : Shape h h') (b : Nat) : h'.live b ↔ h.live b := by
211  obtain ⟨e1, e2, e3, e4, e5, e6, e7⟩ := hS b
212  simp only [Heap.live, ← Option.isSome_iff_ne_none, e1, e2, e3, e4, e5, e6, e7]
213
214theorem Shape.fresh {h h' : Heap} (hS : Shape h h') (hn : h'.nextBlk = h.nextBlk) (hF : Fresh h) : Fresh h' := by
215  intro b hb hl
216  exact hF b (by omega) ((Shape.live hS b).1 hl)
217
218theorem Shape.owns {h h' : Heap} (hS : Shape h h') {S : Nat → Prop} (hO : h.Owns S) : h'.Owns S :=
219  fun b => (Shape.live hS b).trans (hO b)
220
221theorem shape_setS {h : Heap} {gs : Nat} {s0 : GzState} (e : h.gzstates gs = some s0) (s : GzState) :
222    Shape h (setS h gs s) := by
223  intro b
224  by_cases hb : b = gs
225  · subst hb; simp [setS, e]
226  · simp [setS, upd_ne _ _ _ _ hb]
227
228/-- A heap that holds objects only where `h` does, with a `nextBlk` that is not smaller, is `Fresh` if `h` is. -/
229theorem Fresh.of_sub {h h' : Heap} (hF : Fresh h) (hn : h.nextBlk ≤ h'.nextBlk) (hl : ∀ b, h'.live b → h.live b) :
230    Fresh h' := fun b hb hb' => hF b (by omega) (hl b hb')
231
232/-- The record, with any other record in its place that keeps the strings, the buffers, the mode and the message
233rule, keeps the invariant. -/
234theorem GzGood.withRec {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) {s' : GzState}
235    (hm : s'.mode = s.mode ∨ (s'.mode = GZ_READ ∨ s'.mode = GZ_WRITE))
236    (hp : s'.path = s.path) (hmsg : s'.msg = s.msg) (hi : s'.in = s.in) (ho : s'.out = s.out)
237    (he : s'.err = Z_MEM_ERROR → s'.msg = .null) : GzGood (setS h gs s') gs s' := by
238  have hS : Shape h (setS h gs s') := shape_setS hG.hs s'
239  refine ⟨by simp, ?_, ?_, ?_, ?_, ?_, ?_, he, Shape.uniq hS hG.uniq, Shape.fresh hS (by simp) hG.fresh⟩
240  · rcases hm with h1 | h1
241    · rw [h1]; exact hG.mode
242    · exact h1
243  · rw [hp]; simpa [StrBlk] using hG.path
244  · rw [hmsg]; simpa [StrBlk] using hG.msg
245  · rw [hi]; simpa [OptBlk] using hG.inb
246  · rw [ho]; simpa [OptBlk] using hG.outb
247  · rw [hp, hmsg, hi, ho]; exact hG.nodup
248
249
250/-! ### Equation forms (for `simp`: no hypothesis to find) -/
251
252theorem ldS_eq (h : Heap) (gs : Nat) : ldS (some (.tab gs)) h = match h.gzstates gs with
253    | some v => .ok (v, h) | none => .error (.ub "access through a dangling pointer (gz_state)") := by
254  cases hh : h.gzstates gs with
255  | none => simp [ldS, ldGzState, GzStateRef.get, hh]
256  | some v => simp [ldS_run hh, hh]
257
258theorem updS_eq (h : Heap) (gs : Nat) (f : GzState → GzState) : updS (some (.tab gs)) f h = match h.gzstates gs with
259    | some v => .ok ((), setS h gs (f v)) | none => .error (.ub "access through a dangling pointer (gz_state)") := by
260  cases hh : h.gzstates gs with
261  | none => simp [updS, ldGzState, GzStateRef.get, hh, bind_app]
262  | some v => simp [updS_run hh, hh]
263
264theorem updX_eq (h : Heap) (gs : Nat) (f : GzFile → GzFile) : updX (some (.tab gs)) f h = match h.gzstates gs with
265    | some v => .ok ((), setS h gs { v with x := f v.x }) | none => .error (.ub "access through a dangling pointer (gz_state)") := by
266  unfold updX; exact updS_eq h gs _
267
268theorem ldZ_eq (h : Heap) (gs : Nat) : ldZ (some (.in_gzstate_strm gs)) h = match h.gzstates gs with
269    | some v => .ok (v.strm, h) | none => .error (.ub "access through a dangling pointer (z_stream)") := by
270  cases hh : h.gzstates gs with
271  | none => simp [ldZ, ldZStream, ZStreamRef.get, hh]
272  | some v => simp [ldZ_run hh, hh]
273
274theorem updZ_eq (h : Heap) (gs : Nat) (f : ZStream → ZStream) : updZ (some (.in_gzstate_strm gs)) f h = match h.gzstates gs with
275    | some v => .ok ((), setS h gs { v with strm := f v.strm }) | none => .error (.ub "access through a dangling pointer (z_stream)") := by
276  cases hh : h.gzstates gs with
277  | none => simp [updZ, ldZ, ldZStream, ZStreamRef.get, hh, bind_app]
278  | some v => simp [updZ_run hh, hh]
279
280/-- Evaluate a straight-line sequence of accesses to a `gz_state` record and its embedded stream. -/
281macro "gsimp" "[" ts:Lean.Parser.Tactic.simpLemma,* "]" : tactic =>
282  `(tactic| simp [bind_app, pure_app, ldS_eq, updS_eq, updX_eq, ldZ_eq, updZ_eq, castState_hnd, $ts,*])
283
284/-! ### Freeing a string block -/
285
286/-- The heap after `free(p)` of a byte block. -/
287def freeStr (h : Heap) (p : BPtr) : Heap :=
288  match p with
289  | .ref (.blk b) _ => { h with bytes := upd h.bytes b none }
290  | _ => h
291
292theorem freeB_run {h : Heap} {p : BPtr} {b : Nat} (hp : p = .ref (.blk b) 0) {a : Array UInt8}
293    (ha : h.bytes b = some a) (hro : h.ro b = false) : freeB p h = .ok ((), freeStr h p) := by
294  subst hp
295  simp [freeB, freeStr, ha, hro]
296
297theorem freeB_null (h : Heap) : freeB .null h = .ok ((), h) := rfl
298
299@[simp] theorem freeStr_null (h : Heap) : freeStr h .null = h := rfl
300
301@[simp] theorem freeStr_blk (h : Heap) (b : Nat) : freeStr h (.ref (.blk b) 0) = { h with bytes := upd h.bytes b none } := rfl
302
303/-- The block numbers a handle's strings and buffers take. -/
304def blocksOf (s : GzState) : List Nat := [s.path, s.msg, s.in, s.out].filterMap ptrBlk
305
306end Zlib.Gzlib.Proofs