public-gz-offset.lean

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

1import ZlibF.Spec.Public.GzControl
2import ZlibF.Proof.«gzlib.c.simple»
3
4namespace ZlibF.Spec.Public.OffsetProof
5open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib Zlib.Gzlib.Spec Zlib.Gzlib.Proofs
6
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
12
13theorem fsLseek_pure (fd : Int32) (off : Int64) (wh : Int32) (w : Fs) :
14    ∃ x, fsLseek fd off wh w = (pure x : M (Int64 × Fs)) ∧ (x.1 = -1 ∨ 0 ≤ x.1.toInt) := by
15  unfold fsLseek
16  repeat' first
17    | exact ⟨_, rfl, Or.inl rfl⟩
18    | (refine ⟨_, rfl, Or.inr ?_⟩
19       simp only []
20       rw [i64_toInt_ofInt (by omega) (by omega)]
21       omega)
22    | split
23    | dsimp only
24
25theorem fsLseek_eq (fd : Int32) (off : Int64) (wh : Int32) (w : Fs) (h : Heap) :
26    fsLseek fd off wh w h = .ok (lseekRes fd off wh w, h) := by
27  obtain ⟨x, hx, -⟩ := fsLseek_pure fd off wh w
28  unfold lseekRes
29  rw [hx]
30  rfl
31
32/-- `lseek` returns `-1` or a position that is not negative. -/
33theorem lseekRes_ret (fd : Int32) (off : Int64) (wh : Int32) (w : Fs) :
34    (lseekRes fd off wh w).1 = -1 ∨ 0 ≤ (lseekRes fd off wh w).1.toInt := by
35  obtain ⟨x, hx, hp⟩ := fsLseek_pure fd off wh w
36  unfold lseekRes
37  rw [hx]
38  exact hp
39
40theorem G_bind_app {α β : Type} (m : G α) (f : α → G β) (fs : Fs) (h : Heap) :
41    (m >>= f) fs h = match m fs h with | .ok ((a, fs1), h1) => f a fs1 h1 | .error e => .error e := by
42  simp only [bind, StateT.bind]
43  cases hm : m fs h with
44  | error e => rfl
45  | ok v => obtain ⟨⟨a, fs1⟩, h1⟩ := v; rfl
46
47theorem G_pure_app {α : Type} (a : α) (fs : Fs) (h : Heap) : (pure a : G α) fs h = .ok ((a, fs), h) := rfl
48
49theorem G_lift_app {α : Type} (m : M α) (fs : Fs) (h : Heap) :
50    (StateT.lift m : G α) fs h = match m h with | .ok (a, h1) => .ok ((a, fs), h1) | .error e => .error e := rfl
51
52/-- Evaluate a straight-line `G` computation on a `gz_state` record: the lifts, the binds, the field accesses and the
53file calls. -/
54macro "offsetsimp" "[" ts:Lean.Parser.Tactic.simpLemma,* "]" : tactic =>
55  `(tactic| simp [liftM, monadLift, MonadLift.monadLift, MonadLiftT.monadLift, G_bind_app, G_pure_app, G_lift_app,
56    bind_app, pure_app, ldS_eq, updS_eq, updX_eq, ldZ_eq, updZ_eq, castState_hnd, fsLseek_eq, $ts,*])
57
58theorem gzoffset64_null (fs : Fs) (h : Heap) : gzoffset64 none fs h = .ok ((-1, fs), h) := rfl
59
60theorem gzoffset_eq (file : GzFilePtr) (fs : Fs) (h : Heap) : gzoffset file fs h = gzoffset64 file fs h := by
61  unfold gzoffset
62  simp only [G_bind_app]
63  cases hh : gzoffset64 file fs h with
64  | error e => rfl
65  | ok v => obtain ⟨⟨a, fs1⟩, h1⟩ := v; simp [G_pure_app]
66
67
68theorem lseek_current_public (fd : Int32) (fs : Fs)
69    (hpos : ∀ (i : Nat) (f : OFile), fs.fds[i]? = some (some f) → f.pos ≤ 2 ^ 63 - 1) :
70    { (lseekRes fd 0 SEEK_CUR fs).2 with errno := fs.errno } = fs ∧
71    (if fd.toInt < 0 then (lseekRes fd 0 SEEK_CUR fs).1 = -1 else
72      match fs.fds[fd.toInt.toNat]? with
73      | some (some file) => (lseekRes fd 0 SEEK_CUR fs).1.toInt = (file.pos : Int)
74      | _ => (lseekRes fd 0 SEEK_CUR fs).1 = -1) := by
75  by_cases hn : fd.toInt < 0
76  · have hf : fd < 0 := Int32.lt_iff_toInt_lt.mpr (by simpa using hn)
77    simp [lseekRes, fsLseek, hn, hf, pure_app]
78  · have hfd : ¬ fd < 0 := fun hf => hn (by simpa using Int32.lt_iff_toInt_lt.mp hf)
79    by_cases hi : fd.toInt.toNat < fs.fds.size
80    · have hbound : ¬ fd.toInt ≥ (fs.fds.size : Int) := by omega
81      have hget := Array.getElem?_eq_getElem hi
82      cases hf : fs.fds[fd.toInt.toNat] with
83      | none =>
84        have hget' : fs.fds[fd.toInt.toNat]! = none := by rw [getElem!_pos fs.fds _ hi, hf]
85        simp only [lseekRes, fsLseek, hfd, hbound, Bool.false_eq_true, Bool.false_or, ite_false,
86          hget', pure_app, hget, hf, hn, ite_eq_right]
87        simp [pure_app]
88      | some f =>
89        have hvalid : fs.fds[fd.toInt.toNat]? = some (some f) := by rw [hget, hf]
90        have hp := hpos _ _ hvalid
91        have hget' : fs.fds[fd.toInt.toNat]! = some f := by rw [getElem!_pos fs.fds _ hi, hf]
92        have hself : fs.fds.set! fd.toInt.toNat (some f) = fs.fds := by
93          rw [← hf, Array.set!_eq_setIfInBounds]
94          simp [Array.setIfInBounds, hi]
95        simp only [lseekRes, fsLseek, hfd, hbound, Bool.false_eq_true, Bool.false_or, ite_false,
96          hget', pure_app, hvalid, hn, ite_eq_right, SEEK_CUR, SEEK_SET, beq_iff_eq, Int.reduceEq,
97          Int64.toInt_ofNat_of_lt, ite_true, Int.reduceAdd,
98          Int.toNat_natCast, hself, Prod.fst, Prod.snd]
99        have hne : ¬ (f.pos : Int) < 0 := by omega
100        have hmax : ¬ (9223372036854775807 : Int) < f.pos := by omega
101        have hnat : f.pos < 2 ^ 63 := by omega
102        simp only [Array.set!_eq_setIfInBounds] at hself
103        change fs.fds.setIfInBounds fd.toNatClampNeg (some f) = fs.fds at hself
104        have hto : (Int64.ofInt (f.pos : Int)).toInt = (f.pos : Int) :=
105          i64_toInt_ofInt (by omega) (by omega)
106        simp [pure_app, hne, hmax, hself, hto, SEEK_CUR, SEEK_SET]
107    · have hbound : fd.toInt ≥ (fs.fds.size : Int) := by omega
108      have hnone : fs.fds[fd.toInt.toNat]? = none := Array.getElem?_eq_none (by omega)
109      change fs.fds[fd.toNatClampNeg]? = none at hnone
110      simp [lseekRes, fsLseek, hn, hfd, hbound, hnone, pure_app]
111
112/-- `z_off64_t gzoffset64(gzFile file)` has the exact result of the descriptor
113query on any existing state record with a supported mode. -/
114theorem gzoffset64_record {h : Heap} {i : Nat} {s : GzState}
115    (hs : h.gzstates i = some s) (hm : s.mode = GZ_READ ∨ s.mode = GZ_WRITE) (fs : Fs) :
116    gzoffset64 (hnd i) fs h =
117      if (lseekRes s.fd 0 SEEK_CUR fs).1 = -1 then .ok ((-1, (lseekRes s.fd 0 SEEK_CUR fs).2), h)
118      else if s.mode = GZ_READ then
119        .ok ((Int64.ofInt ((lseekRes s.fd 0 SEEK_CUR fs).1.toInt - s.strm.avail_in.toNat),
120          (lseekRes s.fd 0 SEEK_CUR fs).2), h)
121      else .ok (((lseekRes s.fd 0 SEEK_CUR fs).1, (lseekRes s.fd 0 SEEK_CUR fs).2), h) := by
122  have hr := lseekRes_ret s.fd 0 SEEK_CUR fs
123  have hav := s.strm.avail_in.toNat_lt
124  unfold gzoffset64
125  by_cases hl : (lseekRes s.fd 0 SEEK_CUR fs).1 = -1
126  · rcases hm with hm | hm <;> offsetsimp [hs, hm, hl, GZ_READ, GZ_WRITE]
127  · have hr' : 0 ≤ (lseekRes s.fd 0 SEEK_CUR fs).1.toInt := hr.resolve_left hl
128    have hlt := (lseekRes s.fd 0 SEEK_CUR fs).1.toInt_lt
129    have e := i64sub_run (lseekRes s.fd 0 SEEK_CUR fs).1 (u32ToI64 s.strm.avail_in)
130      (by rw [u32ToI64_toInt]; omega) (by rw [u32ToI64_toInt]; omega) h
131    rw [u32ToI64_toInt] at e
132    rcases hm with hm | hm
133    · offsetsimp [hs, hm, hl, GZ_READ, GZ_WRITE, e]
134    · offsetsimp [hs, hm, hl, GZ_READ, GZ_WRITE]
135
136/-- `z_off64_t gzoffset64(gzFile file)` returns the descriptor position less
137buffered input. The heap and all filesystem fields except errno are unchanged. -/
138theorem gzoffset64_public {h : Heap} {i : Nat} {s : GzState}
139    (hs : h.gzstates i = some s) (hm : s.mode = GZ_READ ∨ s.mode = GZ_WRITE) (fs : Fs)
140    (hpos : ∀ (j : Nat) (f : OFile), fs.fds[j]? = some (some f) → f.pos ≤ 2 ^ 63 - 1) :
141    ∃ value fs', gzoffset64 (hnd i) fs h = .ok ((value, fs'), h) ∧
142      { fs' with errno := fs.errno } = fs ∧
143      (if s.fd.toInt < 0 then value = -1 else match fs.fds[s.fd.toInt.toNat]? with
144       | some (some file) => value.toInt = (file.pos : Int) -
145           (if s.mode = GZ_READ then s.strm.avail_in.toNat else 0)
146       | _ => value = -1) := by
147  obtain ⟨hfs, hres⟩ := lseek_current_public s.fd fs hpos
148  have hex := gzoffset64_record hs hm fs
149  by_cases hfd : s.fd.toInt < 0
150  · have he : (lseekRes s.fd 0 SEEK_CUR fs).1 = -1 := by simpa [hfd] using hres
151    exact ⟨-1, _, by simpa [he] using hex, hfs, by simp [hfd]⟩
152  · cases hf : fs.fds[s.fd.toInt.toNat]? with
153    | none =>
154      have he : (lseekRes s.fd 0 SEEK_CUR fs).1 = -1 := by
155        rw [ite_eq_right hfd, hf] at hres
156        exact hres
157      exact ⟨-1, _, by simpa [he] using hex, hfs, by simp [hfd, hf]⟩
158    | some slot =>
159      cases slot with
160      | none =>
161        have he : (lseekRes s.fd 0 SEEK_CUR fs).1 = -1 := by
162          rw [ite_eq_right hfd, hf] at hres
163          exact hres
164        exact ⟨-1, _, by simpa [he] using hex, hfs, by simp [hfd, hf]⟩
165      | some file =>
166        have hr : (lseekRes s.fd 0 SEEK_CUR fs).1.toInt = (file.pos : Int) := by
167          rw [ite_eq_right hfd, hf] at hres
168          exact hres
169        have he : (lseekRes s.fd 0 SEEK_CUR fs).1 ≠ -1 := by
170          intro he
171          rw [he] at hr
172          have : (0 : Int) ≤ file.pos := by omega
173          have : (-1 : Int) = file.pos := by simpa using hr
174          omega
175        by_cases hread : s.mode = GZ_READ
176        · refine ⟨Int64.ofInt ((lseekRes s.fd 0 SEEK_CUR fs).1.toInt - s.strm.avail_in.toNat), _,
177            by simpa [he, hread] using hex, hfs, ?_⟩
178          simp only [hfd, ite_false, hf, hread, ite_true]
179          rw [i64_toInt_ofInt (by have := s.strm.avail_in.toNat_lt; omega)
180            (by have := (lseekRes s.fd 0 SEEK_CUR fs).1.toInt_lt; omega), hr]
181        · exact ⟨_, _, by simpa [he, hread] using hex, hfs, by simpa [hfd, hf, hread] using hr⟩
182
183/-- `z_off_t gzoffset(gzFile file)` has the same LP64 result as `gzoffset64`. -/
184theorem gzoffset_public {h : Heap} {i : Nat} {s : GzState}
185    (hs : h.gzstates i = some s) (hm : s.mode = GZ_READ ∨ s.mode = GZ_WRITE) (fs : Fs)
186    (hpos : ∀ (j : Nat) (f : OFile), fs.fds[j]? = some (some f) → f.pos ≤ 2 ^ 63 - 1) :
187    ∃ value fs', gzoffset (hnd i) fs h = .ok ((value, fs'), h) ∧
188      { fs' with errno := fs.errno } = fs ∧
189      (if s.fd.toInt < 0 then value = -1 else match fs.fds[s.fd.toInt.toNat]? with
190       | some (some file) => value.toInt = (file.pos : Int) -
191           (if s.mode = GZ_READ then s.strm.avail_in.toNat else 0)
192       | _ => value = -1) := by
193  obtain ⟨value, fs', hr, hf, hv⟩ := gzoffset64_public hs hm fs hpos
194  exact ⟨value, fs', by rw [gzoffset_eq]; exact hr, hf, hv⟩
195
196
197/-- `z_off64_t gzoffset64(gzFile file)`
198The exact public result, state, frame and ownership contract. -/
199theorem gzoffset64_public_goal : Goal.gzoffset64 := by
200  constructor
201  · intro h fs
202    exact gzoffset64_null fs h
203  · intro h fs i s _ hv hfs
204    have hpos : ∀ (j : Nat) (f : OFile), fs.fds[j]? = some (some f) → f.pos ≤ 2 ^ 63 - 1 := by
205      intro j f hf
206      exact (hfs.2.2.1 j f hf).2.1
207    exact gzoffset64_public hv.1 hv.2.1 fs hpos
208
209/-- `z_off_t gzoffset(gzFile file)`; the LP64 wrapper has the same physical-position contract.
210The exact public result, state, frame and ownership contract. -/
211theorem gzoffset_public_goal : Goal.gzoffset := by
212  constructor
213  · intro h fs
214    rw [gzoffset_eq]
215    exact gzoffset64_null fs h
216  · intro h fs i s _ hv hfs
217    have hpos : ∀ (j : Nat) (f : OFile), fs.fds[j]? = some (some f) → f.pos ≤ 2 ^ 63 - 1 := by
218      intro j f hf
219      exact (hfs.2.2.1 j f hf).2.1
220    exact gzoffset_public hv.1 hv.2.1 fs hpos
221
222
223#print axioms gzoffset64_public_goal
224#print axioms gzoffset_public_goal
225end ZlibF.Spec.Public.OffsetProof