gzlib.c.rewind.lean

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

1import ZlibF.Proof.«gzlib.c.simple»
2
3namespace Zlib.Gzlib.Spec
4open C Zlib.GzFs Zlib.Gzguts
5
6/-- The result and the world of `lseek(fd, off, whence)` (it does not look at the heap). -/
7def lseekRes (fd : Int32) (off : Int64) (wh : Int32) (w : Fs) : Int64 × Fs :=
8  match fsLseek fd off wh w Heap.empty with
9  | .ok (r, _) => r
10  | .error _ => (-1, w)
11
12end Zlib.Gzlib.Spec
13
14namespace Zlib.Gzlib.Proofs
15open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib Zlib.Gzlib.Spec
16
17theorem fsLseek_pure (fd : Int32) (off : Int64) (wh : Int32) (w : Fs) :
18    ∃ x, fsLseek fd off wh w = (pure x : M (Int64 × Fs)) ∧ (x.1 = -1 ∨ 0 ≤ x.1.toInt) := by
19  unfold fsLseek
20  repeat' first
21    | exact ⟨_, rfl, Or.inl rfl⟩
22    | (refine ⟨_, rfl, Or.inr ?_⟩
23       simp only []
24       rw [i64_toInt_ofInt (by omega) (by omega)]
25       omega)
26    | split
27    | dsimp only
28
29theorem fsLseek_eq (fd : Int32) (off : Int64) (wh : Int32) (w : Fs) (h : Heap) :
30    fsLseek fd off wh w h = .ok (lseekRes fd off wh w, h) := by
31  obtain ⟨x, hx, -⟩ := fsLseek_pure fd off wh w
32  unfold lseekRes
33  rw [hx]
34  rfl
35
36/-- `lseek` returns `-1` or a position that is not negative. -/
37theorem lseekRes_ret (fd : Int32) (off : Int64) (wh : Int32) (w : Fs) :
38    (lseekRes fd off wh w).1 = -1 ∨ 0 ≤ (lseekRes fd off wh w).1.toInt := by
39  obtain ⟨x, hx, hp⟩ := fsLseek_pure fd off wh w
40  unfold lseekRes
41  rw [hx]
42  exact hp
43
44theorem G_bind_app {α β : Type} (m : G α) (f : α → G β) (fs : Fs) (h : Heap) :
45    (m >>= f) fs h = match m fs h with | .ok ((a, fs1), h1) => f a fs1 h1 | .error e => .error e := by
46  simp only [bind, StateT.bind]
47  cases hm : m fs h with
48  | error e => rfl
49  | ok v => obtain ⟨⟨a, fs1⟩, h1⟩ := v; rfl
50
51theorem G_pure_app {α : Type} (a : α) (fs : Fs) (h : Heap) : (pure a : G α) fs h = .ok ((a, fs), h) := rfl
52
53theorem G_lift_app {α : Type} (m : M α) (fs : Fs) (h : Heap) :
54    (StateT.lift m : G α) fs h = match m h with | .ok (a, h1) => .ok ((a, fs), h1) | .error e => .error e := rfl
55
56/-- Evaluate a straight-line `G` computation on a `gz_state` record: the lifts, the binds, the field accesses and the
57file calls. -/
58macro "ggsimp" "[" ts:Lean.Parser.Tactic.simpLemma,* "]" : tactic =>
59  `(tactic| simp [liftM, monadLift, MonadLift.monadLift, MonadLiftT.monadLift, G_bind_app, G_pure_app, G_lift_app,
60    bind_app, pure_app, ldS_eq, updS_eq, updX_eq, ldZ_eq, updZ_eq, castState_hnd, fsLseek_eq, $ts,*])
61
62/-- `gzrewind` on a handle that satisfies the invariant. -/
63theorem gzrewind_run {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (fs : Fs) :
64    gzrewind (hnd gs) fs h =
65      if s.mode ≠ GZ_READ ∨ (s.err ≠ Z_OK ∧ s.err ≠ Z_BUF_ERROR) then .ok ((-1, fs), h)
66      else if (lseekRes s.fd s.start SEEK_SET fs).1 = -1 then .ok ((-1, (lseekRes s.fd s.start SEEK_SET fs).2), h)
67      else .ok ((0, (lseekRes s.fd s.start SEEK_SET fs).2), setS (freeStr h s.msg) gs (resetRec s)) := by
68  have hs := hG.hs
69  unfold gzrewind
70  by_cases hc : s.mode ≠ GZ_READ ∨ (s.err ≠ Z_OK ∧ s.err ≠ Z_BUF_ERROR)
71  · ggsimp [hs, hc]
72  · by_cases hl : (lseekRes s.fd s.start SEEK_SET fs).1 = -1
73    · ggsimp [hs, hc, hl]
74    · ggsimp [hs, hc, hl, gz_reset_run hG]
75
76
77
78
79/-- `gzrewind(NULL)` returns -1; the world and the heap are unchanged. No precondition. -/
80theorem gzrewind_null (fs : Fs) (h : Heap) : gzrewind none fs h = .ok ((-1, fs), h) := rfl
81
82/-- **gzrewind.** On a handle that satisfies the invariant: `-1` and no change when the handle is not a reader or has a
83serious error; `-1` and only the world changed (`errno`) when `lseek` to `start` fails; otherwise `0`, the world is the one
84`lseek` leaves (the descriptor is at `start`), and the state is reset (`gz_reset`). -/
85theorem gzrewind_spec {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (fs : Fs) :
86    ∃ r fs' h', gzrewind (hnd gs) fs h = .ok ((r, fs'), h') ∧
87      ((s.mode ≠ GZ_READ ∨ (s.err ≠ Z_OK ∧ s.err ≠ Z_BUF_ERROR)) ∧ r = -1 ∧ fs' = fs ∧ h' = h ∨
88       ¬(s.mode ≠ GZ_READ ∨ (s.err ≠ Z_OK ∧ s.err ≠ Z_BUF_ERROR)) ∧ (lseekRes s.fd s.start SEEK_SET fs).1 = -1 ∧
89         r = -1 ∧ fs' = (lseekRes s.fd s.start SEEK_SET fs).2 ∧ h' = h ∨
90       ¬(s.mode ≠ GZ_READ ∨ (s.err ≠ Z_OK ∧ s.err ≠ Z_BUF_ERROR)) ∧ (lseekRes s.fd s.start SEEK_SET fs).1 ≠ -1 ∧
91         r = 0 ∧ fs' = (lseekRes s.fd s.start SEEK_SET fs).2 ∧ h' = setS (freeStr h s.msg) gs (resetRec s) ∧
92         GzGood h' gs (resetRec s) ∧ (∀ S, h.Owns S → h'.Owns (fun b => S b ∧ s.msg ≠ .ref (.blk b) 0))) := by
93  have e := gzrewind_run hG fs
94  by_cases hc : s.mode ≠ GZ_READ ∨ (s.err ≠ Z_OK ∧ s.err ≠ Z_BUF_ERROR)
95  · rw [ite_eq_left hc] at e
96    exact ⟨_, _, _, e, Or.inl ⟨hc, rfl, rfl, rfl⟩⟩
97  · rw [ite_eq_right hc] at e
98    by_cases hl : (lseekRes s.fd s.start SEEK_SET fs).1 = -1
99    · rw [ite_eq_left hl] at e
100      exact ⟨_, _, _, e, Or.inr (Or.inl ⟨hc, hl, rfl, rfl, rfl⟩)⟩
101    · rw [ite_eq_right hl] at e
102      obtain ⟨h1, -, he, hg, ho⟩ := gz_reset_safe hG
103      subst he
104      exact ⟨_, _, _, e, Or.inr (Or.inr ⟨hc, hl, rfl, rfl, rfl, hg, ho⟩)⟩
105
106
107/-! ## gzoffset64, gzoffset -/
108
109/-- `gzoffset64(NULL)` returns -1; the world and the heap are unchanged. No precondition. -/
110theorem gzoffset64_null (fs : Fs) (h : Heap) : gzoffset64 none fs h = .ok ((-1, fs), h) := rfl
111
112/-- `gzoffset64`. The result is `-1` when `lseek(fd, 0, SEEK_CUR)` fails; otherwise the descriptor's position, less the
113input the inflate stream holds but has not used (`strm.avail_in`) for a reader. -/
114theorem gzoffset64_run {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (fs : Fs) :
115    gzoffset64 (hnd gs) fs h =
116      if (lseekRes s.fd 0 SEEK_CUR fs).1 = -1 then .ok ((-1, (lseekRes s.fd 0 SEEK_CUR fs).2), h)
117      else if s.mode = GZ_READ then
118        .ok ((Int64.ofInt ((lseekRes s.fd 0 SEEK_CUR fs).1.toInt - s.strm.avail_in.toNat), (lseekRes s.fd 0 SEEK_CUR fs).2), h)
119      else .ok (((lseekRes s.fd 0 SEEK_CUR fs).1, (lseekRes s.fd 0 SEEK_CUR fs).2), h) := by
120  have hs := hG.hs
121  have hr := lseekRes_ret s.fd 0 SEEK_CUR fs
122  have hav := s.strm.avail_in.toNat_lt
123  unfold gzoffset64
124  by_cases hl : (lseekRes s.fd 0 SEEK_CUR fs).1 = -1
125  · rcases hG.mode with hm | hm <;> ggsimp [hs, hm, hl, GZ_READ, GZ_WRITE]
126  · have hr' : 0 ≤ (lseekRes s.fd 0 SEEK_CUR fs).1.toInt := hr.resolve_left hl
127    have hlt := (lseekRes s.fd 0 SEEK_CUR fs).1.toInt_lt
128    have e := i64sub_run (lseekRes s.fd 0 SEEK_CUR fs).1 (u32ToI64 s.strm.avail_in)
129      (by rw [u32ToI64_toInt]; omega) (by rw [u32ToI64_toInt]; omega) h
130    rw [u32ToI64_toInt] at e
131    rcases hG.mode with hm | hm
132    · ggsimp [hs, hm, hl, GZ_READ, GZ_WRITE, e]
133    · ggsimp [hs, hm, hl, GZ_READ, GZ_WRITE]
134
135/-- `gzoffset` is `gzoffset64` (`z_off_t` is `long`, so the range check `ret == (z_off_t)ret` always holds). -/
136theorem gzoffset_eq (file : GzFilePtr) (fs : Fs) (h : Heap) : gzoffset file fs h = gzoffset64 file fs h := by
137  unfold gzoffset
138  simp only [G_bind_app]
139  cases hh : gzoffset64 file fs h with
140  | error e => rfl
141  | ok v => obtain ⟨⟨a, fs1⟩, h1⟩ := v; simp [G_pure_app]
142
143end Zlib.Gzlib.Proofs