gzlib.c.seek.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.rewind»
2
3/-!
4# gzlib.c: `gzseek64`, `gzseek`
5
6`t` is the target position: `0` for `SEEK_SET`, `gztell64` for `SEEK_CUR`, plus `offset`. The function refuses
7(`-1`, nothing changes) when `t` is not a `z_off64_t` that is not negative; otherwise it returns `t`.
8
9The unpatched C faults in two places that the earlier repository patched (R-1, `docs/design/external-io.md`):
10`SEEK_CUR` while `gztell64 < 0` (the check `offset > GZ_OFF_MAX - pos` overflows), and `offset = pos - x.pos` while
11`x.pos < 0` (after `gzungetc` at the start). The theorems below that say what the function returns carry the
12hypothesis `0 ≤ x.pos`, which excludes both; the `*_ub` theorems show the fault in the excluded states.
13-/
14
15namespace Zlib.Gzlib.Spec
16open C Zlib.GzFs Zlib.Gzguts
17
18/-- `GZ_OFF_MAX` as a number. -/
19def OffMax : Int := 9223372036854775807
20
21/-- The position `gzseek64` starts from: 0 for `SEEK_SET`, the current position for `SEEK_CUR`. -/
22def seekBase (s : GzState) (whence : Int32) : Int := if whence = SEEK_SET then 0 else tellPos s
23
24/-- The position `gzseek64` goes to. -/
25def seekT (s : GzState) (offset : Int64) (whence : Int32) : Int := seekBase s whence + offset.toInt
26
27/-- A position `gzseek64` accepts. -/
28def SeekOk (t : Int) : Prop := 0 ≤ t ∧ t ≤ OffMax
29
30instance (t : Int) : Decidable (SeekOk t) := by unfold SeekOk; infer_instance
31
32theorem OffMax_val : OffMax = 9223372036854775807 := rfl
33
34
35/-- The fields a seek does not change. -/
36def SameCfg (s s' : GzState) : Prop :=
37  s'.mode = s.mode ∧ s'.fd = s.fd ∧ s'.path = s.path ∧ s'.size = s.size ∧ s'.want = s.want ∧ s'.in = s.in ∧
38  s'.out = s.out ∧ s'.direct = s.direct ∧ s'.start = s.start ∧ s'.level = s.level ∧ s'.strategy = s.strategy
39
40/-- What every outcome of `gzseek64` has in common: the handle still satisfies the invariants, and either nothing changed
41(result `-1`) or the result is the target `t` and the position fields say so: `gztell64` is `t`, except for a reader that
42has read past the end (`past`), whose `gztell64` is `x.pos` (the position of the end; the returned `t` is not what
43`gztell64` then reports, see the migration note). -/
44def SeekPost (h : Heap) (gs : Nat) (s : GzState) (t : Int) (r : Int64) (h' : Heap) (s' : GzState) : Prop :=
45  GzGood h' gs s' ∧ PosInv s' ∧ NextOk h' s' ∧ SameCfg s s' ∧
46  ((r = -1 ∧ h' = h ∧ s' = s) ∨
47   (SeekOk t ∧ r.toInt = t ∧ (s'.past = 0 → tellPos s' = t) ∧
48     (s'.past ≠ 0 → tellPos s' = s'.x.pos.toInt ∧ s'.x.pos.toInt ≤ t)))
49
50/-- The record after a seek inside the raw area (`how == COPY`): nothing buffered, the position is `t`, no pending skip,
51no error and no message, the stream has no input. -/
52def copyRec (s : GzState) (t : Int) : GzState :=
53  { s with x := { s.x with «have» := 0, pos := Int64.ofInt t }, eof := 0, past := 0, skip := 0, msg := .null, err := Z_OK,
54           strm := { s.strm with avail_in := 0 } }
55
56/-- How many buffered bytes a forward seek skips by advancing `x.next`: all of the distance if the buffer is longer than
57the distance, else the whole buffer. -/
58def fwdN (s : GzState) (off : Int) : Nat := if off < s.x.«have».toNat then off.toNat else s.x.«have».toNat
59
60/-- The record after a forward seek of a reader (target `t`, not before `x.pos`): the buffered bytes before the target
61are consumed, the rest of the distance becomes `skip`. -/
62def skipFwd (s : GzState) (t : Int) : GzState :=
63  let off := t - s.x.pos.toInt
64  let n := fwdN s off
65  { s with x := { «have» := s.x.«have» - UInt32.ofNat n, next := padv s.x.next n, pos := Int64.ofInt (s.x.pos.toInt + n) },
66           skip := Int64.ofInt (off - n) }
67
68/-- The code of `gzseek64` after `pos += offset` (`s` is the record read at the start). Written as in
69`gzlib.c.lean`; `gzseek64_head` shows that `gzseek64` is the checks followed by this. -/
70def seekTail (file : GzFilePtr) (s : GzState) (pos : Int64) : G Int64 := do
71  let state := castState file
72  -- if (state->mode == GZ_READ && state->how == COPY) { ... }
73  if s.mode == GZ_READ && s.how == GZ_COPY then
74    let d ← i64sub (← i64sub pos s.x.pos) (u32ToI64 s.x.«have»)
75    let ret ← fsLseek s.fd d SEEK_CUR
76    if ret == -1 then return -1
77    updX state fun x => { x with «have» := 0 }
78    updS state fun s => { s with eof := 0, past := 0, skip := 0 }
79    gz_error state Z_OK .null
80    updZ (strmOf state) fun z => { z with avail_in := 0 }
81    updX state fun x => { x with pos := pos }
82    return pos
83  -- if (pos < state->x.pos) { if (state->mode != GZ_READ) return -1; if (gzrewind(file) == -1) return -1; }
84  let s ← ldS state
85  if pos < s.x.pos then
86    if s.mode != GZ_READ then return -1
87    if (← gzrewind file) == -1 then return -1
88  -- offset = pos - state->x.pos;
89  let s ← ldS state
90  let mut offset ← i64sub pos s.x.pos
91  -- if (state->mode == GZ_READ) { ... }
92  if s.mode == GZ_READ then
93    let s ← ldS state
94    let n : UInt32 ← if (← GT_OFF s.x.«have») || u32ToI64 s.x.«have» > offset then pure offset.toUInt64.toUInt32
95      else pure s.x.«have»
96    updX state fun x => { x with «have» := x.«have» - n }
97    let s ← ldS state
98    let nx ← s.x.next.add n.toNat
99    updX state fun x => { x with next := nx }
100    let s ← ldS state
101    let np ← i64add s.x.pos (u32ToI64 n)
102    updX state fun x => { x with pos := np }
103    offset ← i64sub offset (u32ToI64 n)
104  -- state->skip = offset; return pos;
105  updS state fun s => { s with skip := offset }
106  return pos
107
108end Zlib.Gzlib.Spec
109
110namespace Zlib.Gzlib.Proofs
111open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib Zlib.Gzlib.Spec
112
113theorem GZ_OFF_MAX_toInt : GZ_OFF_MAX.toInt = OffMax := by
114  unfold GZ_OFF_MAX OffMax
115  exact i64_toInt_ofInt (by omega) (by omega)
116
117theorem int64_toInt_ge (x : Int64) : -9223372036854775808 ≤ x.toInt := x.le_toInt
118theorem int64_toInt_lt (x : Int64) : x.toInt < 9223372036854775808 := x.toInt_lt
119
120theorem i64_gt_iff (a b : Int64) : a > b ↔ b.toInt < a.toInt := by
121  show b < a ↔ _
122  exact Int64.lt_iff_toInt_lt
123
124theorem i64_lt_iff (a b : Int64) : a < b ↔ a.toInt < b.toInt := Int64.lt_iff_toInt_lt
125
126/-- The addition at the start of `gzseek64` for `SEEK_CUR`. -/
127theorem tell_add_run {s : GzState} (hP : PosInv s) (h : Heap) :
128    i64add s.x.pos (if s.past != 0 then 0 else s.skip) h = .ok (Int64.ofInt (tellPos s), h) := by
129  have e := i64add_run s.x.pos (tellSkip s) (by have := hP.lo; unfold tellPos at this; omega)
130    (by have := hP.hi; unfold tellPos at this; omega) h
131  simpa [tellSkip, tellPos] using e
132
133
134theorem tellPos_nonneg {s : GzState} (hP : PosInv s) (hnn : 0 ≤ s.x.pos.toInt) : 0 ≤ tellPos s := by
135  have := hP.skip_nonneg
136  unfold tellPos tellSkip
137  by_cases hp : s.past != 0
138  · simp [hp]; omega
139  · simp [hp]; omega
140
141theorem seekBase_nonneg {s : GzState} (hP : PosInv s) (hnn : 0 ≤ s.x.pos.toInt) (whence : Int32) :
142    0 ≤ seekBase s whence := by
143  unfold seekBase; split
144  · exact Int.le_refl 0
145  · exact tellPos_nonneg hP hnn
146
147theorem seekBase_le {s : GzState} (hP : PosInv s) (whence : Int32) : seekBase s whence ≤ OffMax := by
148  have := hP.hi
149  have hOM := OffMax_val
150  unfold seekBase; split
151  · omega
152  · omega
153
154/-- The three checks of `gzseek64` (`offset > GZ_OFF_MAX - pos`, `offset < -pos`, `pos += offset`) for `pos = p0`
155with `0 ≤ p0`: what they evaluate to. -/
156theorem seek_checks {p0 : Int64} (offset : Int64) (hp0 : 0 ≤ p0.toInt) (h : Heap) :
157    ∃ q1 q3 : Int64, i64sub GZ_OFF_MAX p0 h = .ok (q1, h) ∧ i64neg p0 h = .ok (q3, h) ∧
158      (q1 < offset ↔ OffMax < p0.toInt + offset.toInt) ∧ (offset < q3 ↔ p0.toInt + offset.toInt < 0) ∧
159      ((¬ OffMax < p0.toInt + offset.toInt) → ¬ (p0.toInt + offset.toInt < 0) →
160        ∃ q5 : Int64, i64add p0 offset h = .ok (q5, h) ∧ q5 = Int64.ofInt (p0.toInt + offset.toInt) ∧
161          q5.toInt = p0.toInt + offset.toInt) := by
162  have hOM := OffMax_val
163  have hg := GZ_OFF_MAX_toInt
164  have hlt := p0.toInt_lt
165  have f1 := i64sub_run GZ_OFF_MAX p0 (by omega) (by omega) h
166  have f3 := i64neg_run p0 (by omega) (by omega) h
167  have hq1 : (Int64.ofInt (GZ_OFF_MAX.toInt - p0.toInt)).toInt = OffMax - p0.toInt := by
168    rw [hg]; exact i64_toInt_ofInt (by omega) (by omega)
169  have hq3 : (Int64.ofInt (-p0.toInt)).toInt = -p0.toInt := i64_toInt_ofInt (by omega) (by omega)
170  refine ⟨_, _, f1, f3, ?_, ?_, ?_⟩
171  · rw [i64_lt_iff, hq1]; omega
172  · rw [i64_lt_iff, hq3]; omega
173  · intro h1 h2
174    exact ⟨_, i64add_run p0 offset (by omega) (by omega) h, rfl, i64_toInt_ofInt (by omega) (by omega)⟩
175
176/-- `gzseek64` on a handle with `GzGood` and `PosInv`, `x.pos >= 0`, no serious error and `whence` in {SEEK_SET, SEEK_CUR}: it is the checks followed by `seekTail`. The result is -1 with the heap unchanged when the target is outside `[0, GZ_OFF_MAX]`, otherwise `seekTail` at the target. -/
177theorem gzseek64_head {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hP : PosInv s)
178    (hnn : 0 ≤ s.x.pos.toInt) (he : s.err = Z_OK ∨ s.err = Z_BUF_ERROR) {whence : Int32}
179    (hw : whence = SEEK_SET ∨ whence = SEEK_CUR) (offset : Int64) (fs : Fs) :
180    gzseek64 (hnd gs) offset whence fs h =
181      if SeekOk (seekT s offset whence) then seekTail (hnd gs) s (Int64.ofInt (seekT s offset whence)) fs h
182      else Except.ok ((-1, fs), h) := by
183  have hs := hG.hs
184  have hOM := OffMax_val
185  have hb0 := seekBase_nonneg hP hnn whence
186  have hb1 := seekBase_le hP whence
187  have hne : ¬(¬ s.err = Z_OK ∧ ¬ s.err = Z_BUF_ERROR) := by rcases he with h1 | h1 <;> simp [h1]
188  have hmo : ¬ (s.mode ≠ GZ_READ ∧ s.mode ≠ GZ_WRITE) := by rcases hG.mode with h1 | h1 <;> simp [h1]
189  have hSC : SEEK_CUR ≠ SEEK_SET := by decide
190  have eT : i64add s.x.pos (if s.past = 0 then s.skip else 0) h = .ok (Int64.ofInt (tellPos s), h) := by
191    have := tell_add_run hP h
192    by_cases hh : s.past = 0
193    · simpa [hh] using this
194    · simpa [hh] using this
195  obtain ⟨p0, hp0⟩ : ∃ p0 : Int64, p0 = Int64.ofInt (seekBase s whence) := ⟨_, rfl⟩
196  have hp0i : p0.toInt = seekBase s whence := by rw [hp0]; exact i64_toInt_ofInt (by omega) (by omega)
197  obtain ⟨q1, q3, f1, f3, c1, c2, c5⟩ := seek_checks (p0 := p0) offset (by omega) h
198  rw [hp0i] at c1 c2 c5
199  have hbt : seekBase s whence + offset.toInt = seekT s offset whence := rfl
200  rw [hbt] at c1 c2 c5
201  have hpp : p0 = if whence = SEEK_SET then 0 else Int64.ofInt (tellPos s) := by
202    rw [hp0]; unfold seekBase; split
203    · rfl
204    · rfl
205  unfold gzseek64
206  by_cases r1 : OffMax < seekT s offset whence
207  · have hrhs : ¬ SeekOk (seekT s offset whence) := fun hh => by have := hh.2; omega
208    rw [ite_eq_right hrhs]
209    rcases hw with hw | hw <;> subst hw
210    · rw [ite_eq_left rfl] at hpp; subst hpp
211      ggsimp [hs, hmo, hne, f1, f3, c1, c2, r1]
212    · rw [ite_eq_right (by decide)] at hpp; subst hpp
213      ggsimp [hs, hmo, hne, f1, f3, c1, c2, r1, eT, hSC]
214  · by_cases r2 : seekT s offset whence < 0
215    · have hrhs : ¬ SeekOk (seekT s offset whence) := fun hh => by have := hh.1; omega
216      rw [ite_eq_right hrhs]
217      rcases hw with hw | hw <;> subst hw
218      · rw [ite_eq_left rfl] at hpp; subst hpp
219        ggsimp [hs, hmo, hne, f1, f3, c1, c2, r1, r2]
220      · rw [ite_eq_right (by decide)] at hpp; subst hpp
221        ggsimp [hs, hmo, hne, f1, f3, c1, c2, r1, r2, eT, hSC]
222    · obtain ⟨q5, f5, hq5, hq5i⟩ := c5 r1 r2
223      have hrhs : SeekOk (seekT s offset whence) := ⟨by omega, by omega⟩
224      rw [ite_eq_left hrhs, ← hq5]
225      rcases hw with hw | hw <;> subst hw
226      · rw [ite_eq_left rfl] at hpp; subst hpp
227        ggsimp [hs, hmo, hne, f1, f3, c1, c2, r1, r2, f5, seekTail]
228      · rw [ite_eq_right (by decide)] at hpp; subst hpp
229        ggsimp [hs, hmo, hne, f1, f3, c1, c2, r1, r2, eT, hSC, f5, seekTail]
230
231/-- `gzseek64` on a writer (preconditions as in `gzseek64_head`): the result is the target `t` and `skip` becomes `t - x.pos` when `t` is in range and not before `x.pos`; otherwise -1 and nothing changes. The world is unchanged. -/
232theorem gzseek64_write_run {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hP : PosInv s)
233    (hnn : 0 ≤ s.x.pos.toInt) (he : s.err = Z_OK ∨ s.err = Z_BUF_ERROR) {whence : Int32}
234    (hw : whence = SEEK_SET ∨ whence = SEEK_CUR) (hm : s.mode = GZ_WRITE) (offset : Int64) (fs : Fs) :
235    gzseek64 (hnd gs) offset whence fs h =
236      if SeekOk (seekT s offset whence) ∧ s.x.pos.toInt ≤ seekT s offset whence then
237        Except.ok ((Int64.ofInt (seekT s offset whence), fs),
238          setS h gs { s with skip := Int64.ofInt (seekT s offset whence - s.x.pos.toInt) })
239      else Except.ok ((-1, fs), h) := by
240  have hs := hG.hs
241  have hOM := OffMax_val
242  have hb0 := seekBase_nonneg hP hnn whence
243  have hb1 := seekBase_le hP whence
244  have hne : ¬(¬ s.err = Z_OK ∧ ¬ s.err = Z_BUF_ERROR) := by rcases he with h1 | h1 <;> simp [h1]
245  have hWR : GZ_WRITE ≠ GZ_READ := by decide
246  have hSC : SEEK_CUR ≠ SEEK_SET := by decide
247  have eT : i64add s.x.pos (if s.past = 0 then s.skip else 0) h = .ok (Int64.ofInt (tellPos s), h) := by
248    have := tell_add_run hP h
249    by_cases hh : s.past = 0
250    · simpa [hh] using this
251    · simpa [hh] using this
252  obtain ⟨p0, hp0⟩ : ∃ p0 : Int64, p0 = Int64.ofInt (seekBase s whence) := ⟨_, rfl⟩
253  have hp0i : p0.toInt = seekBase s whence := by rw [hp0]; exact i64_toInt_ofInt (by omega) (by omega)
254  obtain ⟨q1, q3, f1, f3, c1, c2, c5⟩ := seek_checks (p0 := p0) offset (by omega) h
255  rw [hp0i] at c1 c2 c5
256  have hbt : seekBase s whence + offset.toInt = seekT s offset whence := rfl
257  rw [hbt] at c1 c2 c5
258  have hpf : True ∧ (whence = SEEK_CUR → i64add s.x.pos (if s.past != 0 then 0 else s.skip) h =
259      .ok (Int64.ofInt (tellPos s), h)) := ⟨trivial, fun _ => tell_add_run hP h⟩
260  have hpp : p0 = if whence = SEEK_SET then 0 else Int64.ofInt (tellPos s) := by
261    rw [hp0]; unfold seekBase; split
262    · rfl
263    · rfl
264  unfold gzseek64
265  have hcases : (whence = SEEK_SET ∨ whence = SEEK_CUR) := hw
266  by_cases r1 : OffMax < seekT s offset whence
267  · have hrhs : ¬ (SeekOk (seekT s offset whence) ∧ s.x.pos.toInt ≤ seekT s offset whence) := fun hh => by
268      have := hh.1.2; omega
269    rw [ite_eq_right hrhs]
270    rcases hw with hw | hw <;> subst hw
271    · rw [ite_eq_left rfl] at hpp; subst hpp
272      ggsimp [hs, hm, hne, hWR, f1, f3, c1, c2, r1]
273    · rw [ite_eq_right (by decide)] at hpp; subst hpp
274      ggsimp [hs, hm, hne, hWR, f1, f3, c1, c2, r1, eT, hSC]
275  · by_cases r2 : seekT s offset whence < 0
276    · have hrhs : ¬ (SeekOk (seekT s offset whence) ∧ s.x.pos.toInt ≤ seekT s offset whence) := fun hh => by
277        have := hh.1.1; omega
278      rw [ite_eq_right hrhs]
279      rcases hw with hw | hw <;> subst hw
280      · rw [ite_eq_left rfl] at hpp; subst hpp
281        ggsimp [hs, hm, hne, hWR, f1, f3, c1, c2, r1, r2]
282      · rw [ite_eq_right (by decide)] at hpp; subst hpp
283        ggsimp [hs, hm, hne, hWR, f1, f3, c1, c2, r1, r2, eT, hSC]
284    · obtain ⟨q5, f5, hq5, hq5i⟩ := c5 r1 r2
285      have c6 : q5 < s.x.pos ↔ seekT s offset whence < s.x.pos.toInt := by rw [i64_lt_iff, hq5i]
286      have hlt := s.x.pos.toInt_lt
287      have f7 := i64sub_run q5 s.x.pos (by rw [hq5i]; omega) (by rw [hq5i]; omega) h
288      rw [hq5i] at f7
289      by_cases r3 : seekT s offset whence < s.x.pos.toInt
290      · have hrhs : ¬ (SeekOk (seekT s offset whence) ∧ s.x.pos.toInt ≤ seekT s offset whence) := fun hh => by
291          have := hh.2; omega
292        rw [ite_eq_right hrhs]
293        rcases hw with hw | hw <;> subst hw
294        · rw [ite_eq_left rfl] at hpp; subst hpp
295          ggsimp [hs, hm, hne, hWR, f1, f3, c1, c2, r1, r2, f5, c6, r3]
296        · rw [ite_eq_right (by decide)] at hpp; subst hpp
297          ggsimp [hs, hm, hne, hWR, f1, f3, c1, c2, r1, r2, eT, hSC, f5, c6, r3]
298      · have hrhs : SeekOk (seekT s offset whence) ∧ s.x.pos.toInt ≤ seekT s offset whence :=
299          ⟨⟨by omega, by omega⟩, by omega⟩
300        rw [ite_eq_left hrhs, ← hq5]
301        rcases hw with hw | hw <;> subst hw
302        · rw [ite_eq_left rfl] at hpp; subst hpp
303          ggsimp [hs, hm, hne, hWR, f1, f3, c1, c2, r1, r2, f5, c6, r3, f7]
304        · rw [ite_eq_right (by decide)] at hpp; subst hpp
305          ggsimp [hs, hm, hne, hWR, f1, f3, c1, c2, r1, r2, eT, hSC, f5, c6, r3, f7]
306
307
308theorem OffMax_lt : OffMax < 9223372036854775808 := by decide
309
310/-- **Seek inside the raw area** (`how == COPY`, a reader that passes the file through). The descriptor moves by
311`t - x.pos - have` (the bytes read ahead are given back); if `lseek` fails nothing changes but the world; otherwise
312the buffer is dropped (`have = 0`), the error is cleared (the message block is freed), `x.pos = t`. The hypothesis
313`hraw` is the signed-overflow condition of the C expression `pos - x.pos - have` (it fails only for positions within
314`2^32` of `2^63`). -/
315theorem seekTail_copy {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hm : s.mode = GZ_READ)
316    (hcopy : s.how = GZ_COPY) (hnn : 0 ≤ s.x.pos.toInt) {t : Int} (ht : SeekOk t)
317    (hraw : -9223372036854775808 ≤ t - s.x.pos.toInt - s.x.«have».toNat) (fs : Fs) :
318    seekTail (hnd gs) s (Int64.ofInt t) fs h =
319      if (lseekRes s.fd (Int64.ofInt (t - s.x.pos.toInt - s.x.«have».toNat)) SEEK_CUR fs).1 = -1 then
320        Except.ok ((-1, (lseekRes s.fd (Int64.ofInt (t - s.x.pos.toInt - s.x.«have».toNat)) SEEK_CUR fs).2), h)
321      else
322        Except.ok ((Int64.ofInt t, (lseekRes s.fd (Int64.ofInt (t - s.x.pos.toInt - s.x.«have».toNat)) SEEK_CUR fs).2),
323          setS (freeStr h s.msg) gs (copyRec s t)) := by
324  have hs := hG.hs
325  have hOM := OffMax_val
326  have hhv := s.x.«have».toNat_lt
327  have hlt := s.x.pos.toInt_lt
328  have hqi : (Int64.ofInt t).toInt = t := i64_toInt_ofInt (by have := ht.1; omega) (by have := ht.2; omega)
329  obtain ⟨q2, hq2d⟩ : ∃ q2 : Int64, q2 = Int64.ofInt (t - s.x.pos.toInt) := ⟨_, rfl⟩
330  have hq2 : q2.toInt = t - s.x.pos.toInt := by
331    rw [hq2d]; exact i64_toInt_ofInt (by have := ht.1; omega) (by have := ht.2; omega)
332  have fa : i64sub (Int64.ofInt t) s.x.pos h = .ok (q2, h) := by
333    have := i64sub_run (Int64.ofInt t) s.x.pos (by rw [hqi]; have := ht.1; omega) (by rw [hqi]; have := ht.2; omega) h
334    rw [hqi, ← hq2d] at this; exact this
335  obtain ⟨q3, hq3d⟩ : ∃ q3 : Int64, q3 = Int64.ofInt (t - s.x.pos.toInt - s.x.«have».toNat) := ⟨_, rfl⟩
336  have fb : i64sub q2 (u32ToI64 s.x.«have») h = .ok (q3, h) := by
337    have := i64sub_run q2 (u32ToI64 s.x.«have») (by rw [hq2, u32ToI64_toInt]; omega)
338      (by rw [hq2, u32ToI64_toInt]; have := ht.2; omega) h
339    rw [hq2, u32ToI64_toInt, ← hq3d] at this; exact this
340  obtain ⟨q, hqd⟩ : ∃ q : Int64, q = Int64.ofInt t := ⟨_, rfl⟩
341  rw [← hqd] at fa ⊢
342  rw [← hq3d]
343  unfold seekTail
344  by_cases hl : (lseekRes s.fd q3 SEEK_CUR fs).1 = -1
345  · rw [ite_eq_left hl]
346    ggsimp [hs, hm, hcopy, fa, fb, hl]
347  · rw [ite_eq_right hl]
348    rcases hG.msg with hn | ⟨mb, hmm, a, ha, hro, k, hz⟩
349    · ggsimp [hs, hm, hcopy, fa, fb, hl, hn, gz_error, copyRec, ← hqd]
350    · have hne : s.err ≠ Z_MEM_ERROR := fun h' => by have := hG.memerr h'; rw [hmm] at this; cases this
351      ggsimp [hs, hm, hcopy, fa, fb, hl, hmm, hne, freeB_blk_setS ha hro, freeB_blk_run ha hro, gz_error, copyRec, ← hqd]
352
353
354theorem space_get_setS (h : Heap) (gs : Nat) (s' : GzState) (r : BRef) : Space.get (setS h gs s') r = Space.get h r := by
355  cases r <;> rfl
356
357theorem i64_toU32_toNat (x : Int64) (hx : 0 ≤ x.toInt) : x.toUInt64.toUInt32.toNat = x.toInt.toNat % 2 ^ 32 := by
358  have h0 : (0 : Int64) ≤ x := by rw [Int64.le_iff_toInt_le]; simpa using hx
359  rw [UInt64.toNat_toUInt32, Int64.toNat_toUInt64_of_le h0, Int64.toNat_toInt]
360
361/-- `x.next + n` for `n ≤ x.have`: the pointer advanced by `n`. -/
362theorem next_add_run {h : Heap} {s : GzState} (hN : NextOk h s) {n : Nat} (hn : n ≤ s.x.«have».toNat) (gs : Nat) (s' : GzState) :
363    Ptr.add s.x.next (n : Int) (setS h gs s') = .ok (padv s.x.next n, setS h gs s') := by
364  rcases hN.1 with ⟨hnl, hh0⟩ | ⟨r, a, off, hr, hg, hle⟩
365  · have : n = 0 := by rw [hh0] at hn; simpa using hn
366    subst this
367    rw [hnl]
368    simp [Ptr.add, padv]
369  · rw [hr]
370    have hg' : Space.get (setS h gs s') r = some a := by rw [space_get_setS]; exact hg
371    have := Ptr.add_nat_ok (R := BRef) (h := setS h gs s') hg' (n := n) (off := off) (by omega)
372    exact this
373
374
375/-- The part of `gzseek64` after the checks, for a reader that is not in the raw area, with the target not before `x.pos`, `x.pos >= 0` and `NextOk`: the buffered bytes before the target are consumed (`have`, `next`, `pos` advance by `n`), the rest of the distance becomes `skip`; the result is the target; no fault. -/
376theorem seekTail_fwd {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hm : s.mode = GZ_READ)
377    (hhow : s.how ≠ GZ_COPY) (hnn : 0 ≤ s.x.pos.toInt) {t : Int} (ht : SeekOk t) (hfw : s.x.pos.toInt ≤ t)
378    (hN : NextOk h s) (fs : Fs) :
379    seekTail (hnd gs) s (Int64.ofInt t) fs h = Except.ok ((Int64.ofInt t, fs), setS h gs (skipFwd s t)) := by
380  have hs := hG.hs
381  have hOM := OffMax_val
382  have ht1 := ht.1
383  have ht2 := ht.2
384  have hhv := s.x.«have».toNat_lt
385  have hlt := s.x.pos.toInt_lt
386  have hqi : (Int64.ofInt t).toInt = t := i64_toInt_ofInt (by have := ht.1; omega) (by have := ht.2; omega)
387  obtain ⟨q, hqd⟩ : ∃ q : Int64, q = Int64.ofInt t := ⟨_, rfl⟩
388  have hqi' : q.toInt = t := by rw [hqd]; exact hqi
389  obtain ⟨q2, hq2d⟩ : ∃ q2 : Int64, q2 = Int64.ofInt (t - s.x.pos.toInt) := ⟨_, rfl⟩
390  have hq2 : q2.toInt = t - s.x.pos.toInt := by
391    rw [hq2d]; exact i64_toInt_ofInt (by have := ht.1; omega) (by have := ht.2; omega)
392  have fa : ∀ h', i64sub q s.x.pos h' = .ok (q2, h') := fun h' => by
393    have := i64sub_run q s.x.pos (by rw [hqi']; have := ht.1; omega) (by rw [hqi']; have := ht.2; omega) h'
394    rw [hqi', ← hq2d] at this; exact this
395  have c6 : ¬ (q < s.x.pos) := by rw [i64_lt_iff, hqi']; omega
396  have c : q2 < u32ToI64 s.x.«have» ↔ t - s.x.pos.toInt < s.x.«have».toNat := by
397    rw [i64_lt_iff, hq2, u32ToI64_toInt]
398  obtain ⟨nU, hA, hB, hnU, hn1, hn2⟩ : ∃ nU : UInt32, (q2 < u32ToI64 s.x.«have» → nU = q2.toUInt64.toUInt32) ∧
399      (¬ q2 < u32ToI64 s.x.«have» → nU = s.x.«have») ∧ nU.toNat = fwdN s (t - s.x.pos.toInt) ∧
400      nU.toNat ≤ s.x.«have».toNat ∧ (nU.toNat : Int) ≤ t - s.x.pos.toInt := by
401    by_cases hc : q2 < u32ToI64 s.x.«have»
402    · have hc' := c.mp hc
403      have h0 : 0 ≤ q2.toInt := by rw [hq2]; have := ht.1; omega
404      have e := i64_toU32_toNat q2 h0
405      rw [hq2] at e
406      have hl : (t - s.x.pos.toInt).toNat < 2 ^ 32 := by omega
407      rw [Nat.mod_eq_of_lt hl] at e
408      refine ⟨q2.toUInt64.toUInt32, fun _ => rfl, fun hh => absurd hc hh, ?_, ?_, ?_⟩
409      · rw [e]; unfold fwdN; rw [ite_eq_left hc']
410      · rw [e]; omega
411      · rw [e]; omega
412    · have hc' : ¬ (t - s.x.pos.toInt < s.x.«have».toNat) := fun hh => hc (c.mpr hh)
413      refine ⟨s.x.«have», fun hh => absurd hh hc, fun _ => rfl, ?_, Nat.le_refl _, ?_⟩
414      · unfold fwdN; rw [ite_eq_right hc']
415      · omega
416  have fn := next_add_run hN hn1 gs
417  have fpos : ∀ h', i64add s.x.pos (u32ToI64 nU) h' =
418      .ok (Int64.ofInt (s.x.pos.toInt + nU.toNat), h') := fun h' => by
419    have := i64add_run s.x.pos (u32ToI64 nU) (by rw [u32ToI64_toInt]; omega) (by rw [u32ToI64_toInt]; have := ht.2; omega) h'
420    rw [u32ToI64_toInt] at this; exact this
421  have fsk : ∀ h', i64sub q2 (u32ToI64 nU) h' = .ok (Int64.ofInt ((t - s.x.pos.toInt) - nU.toNat), h') := fun h' => by
422    have := i64sub_run q2 (u32ToI64 nU) (by rw [hq2, u32ToI64_toInt]; omega) (by rw [hq2, u32ToI64_toInt]; omega) h'
423    rw [hq2, u32ToI64_toInt] at this; exact this
424  rw [← hqd]
425  unfold seekTail
426  ggsimp [hs, hm, hhow, fa, c6, GT_OFF_run]
427  by_cases hc : q2 < u32ToI64 s.x.«have»
428  · rw [ite_eq_left hc, ← hA hc]
429    ggsimp [hs, fn, fpos, fsk, skipFwd, ← hnU]
430  · rw [ite_eq_right hc, ← hB hc]
431    ggsimp [hs, fn, fpos, fsk, skipFwd, ← hnU]
432
433
434theorem freeStr_get_other (h : Heap) (p : BPtr) (r : BRef) (hr : ∀ b, r ≠ .blk b) :
435    Space.get (freeStr h p) r = Space.get h r := by
436  cases r with
437  | blk b => exact absurd rfl (hr b)
438  | _ => cases p with
439    | null => rfl
440    | ref q o => cases q <;> rfl
441
442/-- `x.next + n` after `gz_reset` freed the message block: the pointer does not point into it. -/
443theorem next_add_run_reset {h : Heap} {s : GzState} (hN : NextOk h s) {n : Nat} (hn : n ≤ s.x.«have».toNat) (gs : Nat)
444    (s' : GzState) :
445    Ptr.add s.x.next (n : Int) (setS (freeStr h s.msg) gs s') = .ok (padv s.x.next n, setS (freeStr h s.msg) gs s') := by
446  rcases hN.1 with ⟨hnl, hh0⟩ | ⟨r, a, off, hr, hg, hle⟩
447  · have : n = 0 := by rw [hh0] at hn; simpa using hn
448    subst this
449    rw [hnl]
450    simp [Ptr.add, padv]
451  · rw [hr]
452    have hg' : Space.get (setS (freeStr h s.msg) gs s') r = some a := by
453      rw [space_get_setS]
454      cases r with
455      | blk b =>
456        have hb := hN.2 b (by rw [hr]; rfl)
457        cases hm : s.msg with
458        | null => simpa [hm, freeStr] using hg
459        | ref q o =>
460          cases q with
461          | blk mb =>
462            have : mb ≠ b := fun e => hb (by rw [hm, e]; rfl)
463            simpa [hm, freeStr, upd_ne _ _ _ _ this.symm] using hg
464          | _ => simpa [hm, freeStr] using hg
465      | str i => rw [freeStr_get_other _ _ _ (by intro b; simp)]; exact hg
466      | dstate_depth i => rw [freeStr_get_other _ _ _ (by intro b; simp)]; exact hg
467      | st_dist_code => rw [freeStr_get_other _ _ _ (by intro b; simp)]; exact hg
468      | st_length_code => rw [freeStr_get_other _ _ _ (by intro b; simp)]; exact hg
469    exact Ptr.add_nat_ok (R := BRef) (h := setS (freeStr h s.msg) gs s') hg' (n := n) (off := off) (by omega)
470
471
472theorem padv_zero (p : BPtr) : padv p 0 = p := by cases p <;> rfl
473
474/-- The part of `gzseek64` after the checks, for a reader that is not in the raw area, with the target before `x.pos` and `NextOk`: `gzrewind`, which fails with -1 and no change of the heap if `lseek` fails, otherwise the state is reset and the whole distance becomes `skip`; no fault. -/
475theorem seekTail_back {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hm : s.mode = GZ_READ)
476    (hhow : s.how ≠ GZ_COPY) (he : s.err = Z_OK ∨ s.err = Z_BUF_ERROR) (hnn : 0 ≤ s.x.pos.toInt) {t : Int}
477    (ht : SeekOk t) (hlt : t < s.x.pos.toInt) (hN : NextOk h s) (fs : Fs) :
478    seekTail (hnd gs) s (Int64.ofInt t) fs h =
479      if (lseekRes s.fd s.start SEEK_SET fs).1 = -1 then Except.ok ((-1, (lseekRes s.fd s.start SEEK_SET fs).2), h)
480      else Except.ok ((Int64.ofInt t, (lseekRes s.fd s.start SEEK_SET fs).2),
481        setS (freeStr h s.msg) gs (skipFwd (resetRec s) t)) := by
482  have hs := hG.hs
483  have hOM := OffMax_val
484  have ht1 := ht.1
485  have ht2 := ht.2
486  have hqi : (Int64.ofInt t).toInt = t := i64_toInt_ofInt (by omega) (by omega)
487  obtain ⟨q, hqd⟩ : ∃ q : Int64, q = Int64.ofInt t := ⟨_, rfl⟩
488  have hqi' : q.toInt = t := by rw [hqd]; exact hqi
489  have c6 : q < s.x.pos := by rw [i64_lt_iff, hqi']; omega
490  have hrw := gzrewind_run hG fs
491  have hcond : ¬ (s.mode ≠ GZ_READ ∨ (s.err ≠ Z_OK ∧ s.err ≠ Z_BUF_ERROR)) := by
492    rintro (h1 | ⟨h1, h2⟩)
493    · exact h1 hm
494    · rcases he with e | e <;> simp_all
495  rw [ite_eq_right hcond] at hrw
496  rw [← hqd]
497  unfold seekTail
498  by_cases hl : (lseekRes s.fd s.start SEEK_SET fs).1 = -1
499  · rw [ite_eq_left hl]
500    rw [ite_eq_left hl] at hrw
501    ggsimp [hs, hm, hhow, c6, hrw, hl]
502  · rw [ite_eq_right hl]
503    rw [ite_eq_right hl] at hrw
504    have z0 : (0 : Int64).toInt = 0 := rfl
505    have hq0 : ¬ q < 0 := by rw [i64_lt_iff, hqi', z0]; omega
506    have fa0 : ∀ h', i64sub q 0 h' = .ok (q, h') := fun h' => by
507      have := i64sub_run q 0 (by rw [hqi', z0]; omega) (by rw [hqi', z0]; omega) h'
508      simpa [hqi', ← hqd] using this
509    have fb0 : ∀ h', i64sub q (u32ToI64 0) h' = .ok (q, h') := fun h' => by
510      have := fa0 h'
511      simpa [u32ToI64] using this
512    have fc0 : ∀ h', i64add 0 (u32ToI64 0) h' = .ok (0, h') := fun h' => by
513      simp [i64add, i64chk, u32ToI64]
514    have fn0 : ∀ s', Ptr.add s.x.next 0 (setS (freeStr h s.msg) gs s') = .ok (s.x.next, setS (freeStr h s.msg) gs s') := fun s' => by
515      have := next_add_run_reset hN (n := 0) (Nat.zero_le _) gs s'
516      simpa [padv_zero] using this
517    have hGT : ¬ (u32ToI64 0 > q) := by rw [i64_gt_iff, u32ToI64_toInt, hqi']; simp; omega
518    have hnt : ¬ t < 0 := by omega
519    ggsimp [hs, hm, hhow, c6, hrw, hl, fa0, fb0, fc0, fn0, hGT, skipFwd, fwdN, resetRec, padv_zero, GT_OFF_run, hnt, ← hqd]
520
521
522/-! ### The invariants after a seek -/
523
524theorem fwdN_le {s : GzState} (off : Int) : fwdN s off ≤ s.x.«have».toNat := by
525  unfold fwdN; split <;> omega
526
527theorem fwdN_le_off {s : GzState} {off : Int} (h0 : 0 ≤ off) : (fwdN s off : Int) ≤ off := by
528  unfold fwdN; split <;> omega
529
530theorem GzGood.skipFwd {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (t : Int) :
531    GzGood (setS h gs (skipFwd s t)) gs (skipFwd s t) :=
532  GzGood.withRec hG (Or.inl rfl) rfl rfl rfl rfl (fun hh => hG.memerr hh)
533
534theorem PosInv_skipFwd {s : GzState} (hnn : 0 ≤ s.x.pos.toInt) {t : Int} (ht : SeekOk t) (hfw : s.x.pos.toInt ≤ t) :
535    PosInv (skipFwd s t) ∧ (s.past = 0 → tellPos (skipFwd s t) = t) ∧
536      (s.past ≠ 0 → tellPos (skipFwd s t) = s.x.pos.toInt + fwdN s (t - s.x.pos.toInt)) := by
537  have hOM := OffMax_val
538  have ht1 := ht.1
539  have ht2 := ht.2
540  have h1 := fwdN_le_off (s := s) (off := t - s.x.pos.toInt) (by omega)
541  have hlt := s.x.pos.toInt_lt
542  obtain ⟨P, hPd⟩ : ∃ P : Int64, P = Int64.ofInt (s.x.pos.toInt + (fwdN s (t - s.x.pos.toInt) : Int)) := ⟨_, rfl⟩
543  obtain ⟨K, hKd⟩ : ∃ K : Int64, K = Int64.ofInt (t - s.x.pos.toInt - (fwdN s (t - s.x.pos.toInt) : Int)) := ⟨_, rfl⟩
544  have e1 : P.toInt = s.x.pos.toInt + fwdN s (t - s.x.pos.toInt) := by
545    rw [hPd]; exact i64_toInt_ofInt (by omega) (by omega)
546  have e2 : K.toInt = t - s.x.pos.toInt - fwdN s (t - s.x.pos.toInt) := by
547    rw [hKd]; exact i64_toInt_ofInt (by omega) (by omega)
548  have hskip : (skipFwd s t).skip = K := by rw [hKd]; rfl
549  have hpos : (skipFwd s t).x.pos = P := by rw [hPd]; rfl
550  have hpast : (skipFwd s t).past = s.past := rfl
551  refine ⟨⟨?_, ?_, ?_⟩, ?_, ?_⟩
552  · rw [hskip, e2]; omega
553  · unfold tellPos tellSkip; rw [hpast, hpos]
554    by_cases hp : s.past != 0 <;> simp [hp, e1, hskip, e2] <;> omega
555  · unfold tellPos tellSkip; rw [hpast, hpos]
556    by_cases hp : s.past != 0 <;> simp [hp, e1, hskip, e2] <;> omega
557  · intro hp0
558    unfold tellPos tellSkip; rw [hpast, hpos]
559    simp [hp0, e1, hskip, e2]; omega
560  · intro hp0
561    unfold tellPos tellSkip; rw [hpast, hpos]
562    have : (s.past != 0) = true := by simpa using hp0
563    simp [this, e1]
564
565theorem NextOk_skipFwd {h : Heap} {s : GzState} (hN : NextOk h s) (t : Int) : NextOk h (skipFwd s t) := by
566  have hle := fwdN_le (s := s) (t - s.x.pos.toInt)
567  refine ⟨?_, ?_⟩
568  · rcases hN.1 with ⟨hnl, hh0⟩ | ⟨r, a, off, hr, hg, hl⟩
569    · have : fwdN s (t - s.x.pos.toInt) = 0 := by rw [hh0] at hle; simpa using hle
570      left; refine ⟨?_, ?_⟩
571      · show padv s.x.next _ = _; rw [hnl, this]; rfl
572      · show s.x.«have» - UInt32.ofNat _ = 0; rw [hh0, this]; rfl
573    · right
574      refine ⟨r, a, off + fwdN s (t - s.x.pos.toInt), ?_, hg, ?_⟩
575      · show padv s.x.next _ = _; rw [hr]; rfl
576      · show _ + (s.x.«have» - UInt32.ofNat _).toNat ≤ a.size
577        have hh := s.x.«have».toNat_lt
578        have hn32 : (UInt32.ofNat (fwdN s (t - s.x.pos.toInt))).toNat = fwdN s (t - s.x.pos.toInt) :=
579          UInt32.toNat_ofNat_of_lt' (by have hsz : UInt32.size = 4294967296 := rfl; omega)
580        have : (s.x.«have» - UInt32.ofNat (fwdN s (t - s.x.pos.toInt))).toNat = s.x.«have».toNat - fwdN s (t - s.x.pos.toInt) := by
581          rw [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le, hn32]; omega), hn32]
582        rw [this]; omega
583  · intro b hb
584    have : (skipFwd s t).x.next = padv s.x.next (fwdN s (t - s.x.pos.toInt)) := rfl
585    rw [this] at hb
586    have hb' : ptrBlk s.x.next = some b := by
587      cases hp : s.x.next with
588      | null => rw [hp] at hb; simp [padv, ptrBlk] at hb
589      | ref r o => rw [hp] at hb; cases r <;> simp [padv, ptrBlk] at hb ⊢ <;> exact hb
590    have := hN.2 b hb'
591    exact this
592
593
594theorem get_after_free {h : Heap} {s : GzState} (hn : ∀ b, ptrBlk s.x.next = some b → ptrBlk s.msg ≠ some b)
595    {r : BRef} {off : Nat} (hr : s.x.next = .ref r off) {a : Array UInt8} (hg : Space.get h r = some a) (gs : Nat)
596    (z : GzState) : Space.get (setS (freeStr h s.msg) gs z) r = some a := by
597  rw [space_get_setS]
598  cases r with
599  | blk b =>
600    have hb := hn b (by rw [hr]; rfl)
601    cases hm : s.msg with
602    | null => simpa [hm, freeStr] using hg
603    | ref q o =>
604      cases q with
605      | blk mb =>
606        have : mb ≠ b := fun e => hb (by rw [hm, e]; rfl)
607        simpa [hm, freeStr, upd_ne _ _ _ _ this.symm] using hg
608      | _ => simpa [hm, freeStr] using hg
609  | str i => rw [freeStr_get_other _ _ _ (by intro b; simp)]; exact hg
610  | dstate_depth i => rw [freeStr_get_other _ _ _ (by intro b; simp)]; exact hg
611  | st_dist_code => rw [freeStr_get_other _ _ _ (by intro b; simp)]; exact hg
612  | st_length_code => rw [freeStr_get_other _ _ _ (by intro b; simp)]; exact hg
613
614/-- After a call that frees the message block and leaves `x.next` alone, `x.next` is still usable. -/
615theorem NextOk_free {h : Heap} {s s' : GzState} (hN : NextOk h s) (gs : Nat) (z : GzState)
616    (hnx : s'.x.next = s.x.next) (hhv : s'.x.«have».toNat ≤ s.x.«have».toNat)
617    (hnull : s'.x.next = .null → s'.x.«have» = 0) (hm : s'.msg = .null) :
618    NextOk (setS (freeStr h s.msg) gs z) s' := by
619  refine ⟨?_, ?_⟩
620  · rcases hN.1 with ⟨hnl, hh0⟩ | ⟨r, a, off, hr, hg, hl⟩
621    · exact Or.inl ⟨by rw [hnx]; exact hnl, hnull (by rw [hnx]; exact hnl)⟩
622    · exact Or.inr ⟨r, a, off, by rw [hnx]; exact hr, get_after_free hN.2 hr hg gs z, by omega⟩
623  · intro b hb; rw [hm]; simp [ptrBlk]
624
625theorem PosInv_resetRec (s : GzState) : PosInv (resetRec s) ∧ tellPos (resetRec s) = 0 := by
626  have e1 : (resetRec s).skip = 0 := by unfold resetRec; split <;> rfl
627  have e2 : (resetRec s).x.pos = 0 := by unfold resetRec; split <;> rfl
628  have e3 : (resetRec s).past = 0 := by unfold resetRec; split <;> rfl
629  have z0 : (0 : Int64).toInt = 0 := rfl
630  have ht : tellPos (resetRec s) = 0 := by
631    unfold tellPos tellSkip; rw [e2, e3]; simp [z0, e1]
632  exact ⟨⟨by rw [e1, z0]; omega, by rw [ht]; omega, by rw [ht]; omega⟩, ht⟩
633
634theorem GzGood.afterCopy {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (t : Int) :
635    GzGood (setS (freeStr h s.msg) gs (copyRec s t)) gs (copyRec s t) := by
636  have h1 := GzGood.withRec (GzGood.afterErr hG Z_OK) (s' := copyRec s t) (Or.inl rfl) rfl rfl rfl rfl (fun _ => rfl)
637  simpa using h1
638
639theorem PosInv_copyRec (s : GzState) {t : Int} (ht : SeekOk t) : PosInv (copyRec s t) ∧ tellPos (copyRec s t) = t := by
640  have hOM := OffMax_val
641  have ht1 := ht.1
642  have ht2 := ht.2
643  have e1 : (copyRec s t).skip = 0 := rfl
644  have e2 : (copyRec s t).x.pos = Int64.ofInt t := rfl
645  have e3 : (copyRec s t).past = 0 := rfl
646  have z0 : (0 : Int64).toInt = 0 := rfl
647  have hq : (Int64.ofInt t).toInt = t := i64_toInt_ofInt (by omega) (by omega)
648  have htt : tellPos (copyRec s t) = t := by
649    unfold tellPos tellSkip; rw [e2, e3]; simp [z0, e1, hq, -Int64.toInt_ofInt]
650  exact ⟨⟨by rw [e1, z0]; omega, by rw [htt]; omega, by rw [htt]; omega⟩, htt⟩
651
652
653theorem sameCfg_refl (s : GzState) : SameCfg s s := ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
654
655theorem SameCfg.trans {a b c : GzState} (h1 : SameCfg a b) (h2 : SameCfg b c) : SameCfg a c := by
656  obtain ⟨a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11⟩ := h1
657  obtain ⟨b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11⟩ := h2
658  exact ⟨b1.trans a1, b2.trans a2, b3.trans a3, b4.trans a4, b5.trans a5, b6.trans a6, b7.trans a7, b8.trans a8,
659    b9.trans a9, b10.trans a10, b11.trans a11⟩
660
661theorem sameCfg_resetRec (s : GzState) : SameCfg s (resetRec s) := by
662  unfold resetRec; split <;> exact ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
663
664theorem sameCfg_skipFwd (s : GzState) (t : Int) : SameCfg s (skipFwd s t) :=
665  ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
666
667theorem sameCfg_copyRec (s : GzState) (t : Int) : SameCfg s (copyRec s t) :=
668  ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
669
670theorem NextOk_setS {h : Heap} {s' : GzState} (hN : NextOk h s') (gs : Nat) (z : GzState) : NextOk (setS h gs z) s' := by
671  refine ⟨?_, hN.2⟩
672  rcases hN.1 with hn | ⟨r, a, off, hr, hg, hl⟩
673  · exact Or.inl hn
674  · exact Or.inr ⟨r, a, off, hr, by rw [space_get_setS]; exact hg, hl⟩
675
676theorem seek_write_safe {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hP : PosInv s)
677    (hnn : 0 ≤ s.x.pos.toInt) (he : s.err = Z_OK ∨ s.err = Z_BUF_ERROR) {whence : Int32}
678    (hw : whence = SEEK_SET ∨ whence = SEEK_CUR) (hm : s.mode = GZ_WRITE) (hN : NextOk h s) (offset : Int64) (fs : Fs) :
679    ∃ r h' s', gzseek64 (hnd gs) offset whence fs h = .ok ((r, fs), h') ∧ SeekPost h gs s (seekT s offset whence) r h' s' := by
680  have hrun := gzseek64_write_run hG hP hnn he hw hm offset fs
681  have hOM := OffMax_val
682  by_cases hc : SeekOk (seekT s offset whence) ∧ s.x.pos.toInt ≤ seekT s offset whence
683  · rw [ite_eq_left hc] at hrun
684    obtain ⟨⟨ht1, ht2⟩, hfw⟩ := hc
685    have hlt := s.x.pos.toInt_lt
686    have eK : (Int64.ofInt (seekT s offset whence - s.x.pos.toInt)).toInt = seekT s offset whence - s.x.pos.toInt :=
687      i64_toInt_ofInt (by omega) (by omega)
688    obtain ⟨K, hKd⟩ : ∃ K : Int64, K = Int64.ofInt (seekT s offset whence - s.x.pos.toInt) := ⟨_, rfl⟩
689    rw [← hKd] at hrun
690    have eK' : K.toInt = seekT s offset whence - s.x.pos.toInt := by rw [hKd]; exact eK
691    have hG' := GzGood.withRec hG (s' := { s with skip := K }) (Or.inl rfl) rfl rfl rfl rfl (fun hh => hG.memerr hh)
692    have hts : ∀ pp : Int, tellPos { s with skip := K } = (if s.past != 0 then s.x.pos.toInt else s.x.pos.toInt + K.toInt) := by
693      intro _; unfold tellPos tellSkip; by_cases hp : s.past != 0 <;> simp [hp]
694    refine ⟨_, _, { s with skip := K }, hrun, hG', ⟨?_, ?_, ?_⟩, NextOk_setS hN gs _, ?_, Or.inr ⟨⟨ht1, ht2⟩, ?_, ?_, ?_⟩⟩
695    · exact eK' ▸ (by omega)
696    · rw [hts 0]; split <;> omega
697    · rw [hts 0]; split <;> omega
698    · exact ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
699    · exact i64_toInt_ofInt (by omega) (by omega)
700    · intro hp0; rw [hts 0]; have : ¬ (s.past != 0) = true := by simpa using hp0
701      simp [this]; omega
702    · intro hp0; have : (s.past != 0) = true := by simpa using hp0
703      rw [hts 0]; simp [this]; omega
704  · rw [ite_eq_right hc] at hrun
705    exact ⟨_, _, s, hrun, hG, hP, hN, sameCfg_refl s, Or.inl ⟨rfl, rfl, rfl⟩⟩
706
707
708theorem skipFwd_pos {s : GzState} (hnn : 0 ≤ s.x.pos.toInt) {t : Int} (ht : SeekOk t) (hfw : s.x.pos.toInt ≤ t) :
709    (skipFwd s t).x.pos.toInt = s.x.pos.toInt + fwdN s (t - s.x.pos.toInt) ∧ (skipFwd s t).x.pos.toInt ≤ t := by
710  have hOM := OffMax_val
711  have ht1 := ht.1
712  have ht2 := ht.2
713  have h1 := fwdN_le_off (s := s) (off := t - s.x.pos.toInt) (by omega)
714  have hlt := s.x.pos.toInt_lt
715  have e : (skipFwd s t).x.pos.toInt = s.x.pos.toInt + fwdN s (t - s.x.pos.toInt) :=
716    i64_toInt_ofInt (by omega) (by omega)
717  exact ⟨e, by omega⟩
718
719theorem tell_past {s : GzState} (hp : s.past ≠ 0) : tellPos s = s.x.pos.toInt := by
720  have : (s.past != 0) = true := by simpa using hp
721  unfold tellPos tellSkip; simp [this]
722
723theorem seek_fwd_safe {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hP : PosInv s)
724    (hnn : 0 ≤ s.x.pos.toInt) (he : s.err = Z_OK ∨ s.err = Z_BUF_ERROR) {whence : Int32}
725    (hw : whence = SEEK_SET ∨ whence = SEEK_CUR) (hm : s.mode = GZ_READ) (hhow : s.how ≠ GZ_COPY) (hN : NextOk h s)
726    (offset : Int64) (fs : Fs) (ht : SeekOk (seekT s offset whence)) (hfw : s.x.pos.toInt ≤ seekT s offset whence) :
727    ∃ r h' s', gzseek64 (hnd gs) offset whence fs h = .ok ((r, fs), h') ∧ SeekPost h gs s (seekT s offset whence) r h' s' := by
728  have hhead := gzseek64_head hG hP hnn he hw offset fs
729  rw [ite_eq_left ht, seekTail_fwd hG hm hhow hnn ht hfw hN fs] at hhead
730  have hpp := PosInv_skipFwd hnn ht hfw
731  have hps := skipFwd_pos hnn ht hfw
732  have hq : (Int64.ofInt (seekT s offset whence)).toInt = seekT s offset whence :=
733    i64_toInt_ofInt (by have := ht.1; omega) (by have := ht.2; have := OffMax_val; omega)
734  refine ⟨_, _, skipFwd s (seekT s offset whence), hhead, GzGood.skipFwd hG _, hpp.1,
735    NextOk_setS (NextOk_skipFwd hN _) gs _, sameCfg_skipFwd _ _, Or.inr ⟨ht, hq, hpp.2.1, ?_⟩⟩
736  intro hp0
737  have hpast : (skipFwd s (seekT s offset whence)).past ≠ 0 := hp0
738  exact ⟨tell_past hpast, hps.2⟩
739
740
741theorem seek_copy_safe {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hP : PosInv s)
742    (hnn : 0 ≤ s.x.pos.toInt) (he : s.err = Z_OK ∨ s.err = Z_BUF_ERROR) {whence : Int32}
743    (hw : whence = SEEK_SET ∨ whence = SEEK_CUR) (hm : s.mode = GZ_READ) (hcopy : s.how = GZ_COPY) (hN : NextOk h s)
744    (offset : Int64) (fs : Fs) (ht : SeekOk (seekT s offset whence))
745    (hraw : -9223372036854775808 ≤ seekT s offset whence - s.x.pos.toInt - s.x.«have».toNat) :
746    ∃ r fs' h', gzseek64 (hnd gs) offset whence fs h = .ok ((r, fs'), h') ∧
747      (∃ s', SeekPost h gs s (seekT s offset whence) r h' s') := by
748  have hhead := gzseek64_head hG hP hnn he hw offset fs
749  rw [ite_eq_left ht, seekTail_copy hG hm hcopy hnn ht hraw fs] at hhead
750  have hq : (Int64.ofInt (seekT s offset whence)).toInt = seekT s offset whence :=
751    i64_toInt_ofInt (by have := ht.1; omega) (by have := ht.2; have := OffMax_val; omega)
752  by_cases hl : (lseekRes s.fd (Int64.ofInt (seekT s offset whence - s.x.pos.toInt - s.x.«have».toNat)) SEEK_CUR fs).1 = -1
753  · rw [ite_eq_left hl] at hhead
754    exact ⟨_, _, _, hhead, s, hG, hP, hN, sameCfg_refl s, Or.inl ⟨rfl, rfl, rfl⟩⟩
755  · rw [ite_eq_right hl] at hhead
756    have hpc := PosInv_copyRec s ht
757    refine ⟨_, _, _, hhead, copyRec s (seekT s offset whence), GzGood.afterCopy hG _, hpc.1,
758      NextOk_free hN gs _ rfl (by show (0 : UInt32).toNat ≤ _; simp) (fun _ => rfl) rfl, sameCfg_copyRec _ _,
759      Or.inr ⟨ht, hq, fun _ => hpc.2, fun hp0 => absurd rfl hp0⟩⟩
760
761theorem fwdN_reset (s : GzState) {t : Int} (ht : 0 ≤ t) : fwdN (resetRec s) (t - (resetRec s).x.pos.toInt) = 0 := by
762  have e1 : (resetRec s).x.«have» = 0 := by unfold resetRec; split <;> rfl
763  have e2 : (resetRec s).x.pos = 0 := by unfold resetRec; split <;> rfl
764  have z0 : (0 : Int64).toInt = 0 := rfl
765  unfold fwdN; rw [e1, e2, z0]; simp; omega
766
767theorem seek_back_safe {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hP : PosInv s)
768    (hnn : 0 ≤ s.x.pos.toInt) (he : s.err = Z_OK ∨ s.err = Z_BUF_ERROR) {whence : Int32}
769    (hw : whence = SEEK_SET ∨ whence = SEEK_CUR) (hm : s.mode = GZ_READ) (hhow : s.how ≠ GZ_COPY) (hN : NextOk h s)
770    (offset : Int64) (fs : Fs) (ht : SeekOk (seekT s offset whence)) (hlt : seekT s offset whence < s.x.pos.toInt) :
771    ∃ r fs' h', gzseek64 (hnd gs) offset whence fs h = .ok ((r, fs'), h') ∧
772      (∃ s', SeekPost h gs s (seekT s offset whence) r h' s') := by
773  have hhead := gzseek64_head hG hP hnn he hw offset fs
774  rw [ite_eq_left ht, seekTail_back hG hm hhow he hnn ht hlt hN fs] at hhead
775  have hq : (Int64.ofInt (seekT s offset whence)).toInt = seekT s offset whence :=
776    i64_toInt_ofInt (by have := ht.1; omega) (by have := ht.2; have := OffMax_val; omega)
777  by_cases hl : (lseekRes s.fd s.start SEEK_SET fs).1 = -1
778  · rw [ite_eq_left hl] at hhead
779    exact ⟨_, _, _, hhead, s, hG, hP, hN, sameCfg_refl s, Or.inl ⟨rfl, rfl, rfl⟩⟩
780  · rw [ite_eq_right hl] at hhead
781    have hz : (resetRec s).x.pos.toInt = 0 := by
782      have e2 : (resetRec s).x.pos = 0 := by unfold resetRec; split <;> rfl
783      rw [e2]; rfl
784    have hfw : (resetRec s).x.pos.toInt ≤ seekT s offset whence := by rw [hz]; exact ht.1
785    have hpp := PosInv_skipFwd (s := resetRec s) (by rw [hz]; exact Int.le_refl 0) ht hfw
786    have hF := fwdN_reset s ht.1
787    have hGr := GzGood.skipFwd (GzGood.afterReset hG) (seekT s offset whence)
788    simp only [setS_setS] at hGr
789    have hpast : (resetRec s).past = 0 := by unfold resetRec; split <;> rfl
790    refine ⟨_, _, _, hhead, skipFwd (resetRec s) (seekT s offset whence), hGr, hpp.1, ?_,
791      SameCfg.trans (sameCfg_resetRec s) (sameCfg_skipFwd _ _), Or.inr ⟨ht, hq, fun _ => hpp.2.1 hpast, fun hp0 => absurd hpast hp0⟩⟩
792    refine NextOk_free hN gs _ ?_ ?_ ?_ rfl
793    · show padv (resetRec s).x.next _ = _
794      rw [hF]; unfold resetRec; split <;> simp [padv_zero]
795    · show ((resetRec s).x.«have» - _).toNat ≤ _
796      have e1 : (resetRec s).x.«have» = 0 := by unfold resetRec; split <;> rfl
797      rw [e1]; rw [hF]; simp
798    · intro _
799      show (resetRec s).x.«have» - _ = 0
800      have e1 : (resetRec s).x.«have» = 0 := by unfold resetRec; split <;> rfl
801      rw [e1, hF]; rfl
802
803
804/-- `gzseek64(NULL, offset, whence)` returns -1; the world and the heap are unchanged. -/
805theorem gzseek64_null (offset : Int64) (whence : Int32) (fs : Fs) (h : Heap) :
806    gzseek64 none offset whence fs h = .ok ((-1, fs), h) := rfl
807
808/-- **gzseek64, safety and effect** (reachable states with `x.pos ≥ 0`: no `gzungetc` right after `gzopen`, the case
809the unpatched C faults in; `NextOk`: `x.next` is not dangling; `hraw`: positions within `2^32` of `2^63`).
810The call does not fault; on success the handle satisfies the invariants again; the result is `-1` and nothing but the
811world changed, or it is the target `t` (the position `gztell64` reports is `t`, except after a read past the end). -/
812theorem gzseek64_safe {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hP : PosInv s)
813    (hnn : 0 ≤ s.x.pos.toInt) (he : s.err = Z_OK ∨ s.err = Z_BUF_ERROR) {whence : Int32}
814    (hw : whence = SEEK_SET ∨ whence = SEEK_CUR) (hN : NextOk h s) (offset : Int64) (fs : Fs)
815    (hraw : s.mode = GZ_READ → s.how = GZ_COPY → SeekOk (seekT s offset whence) →
816      -9223372036854775808 ≤ seekT s offset whence - s.x.pos.toInt - s.x.«have».toNat) :
817    ∃ r fs' h' s', gzseek64 (hnd gs) offset whence fs h = .ok ((r, fs'), h') ∧
818      SeekPost h gs s (seekT s offset whence) r h' s' := by
819  by_cases ht : SeekOk (seekT s offset whence)
820  · rcases hG.mode with hm | hm
821    · by_cases hc : s.how = GZ_COPY
822      · obtain ⟨r, fs', h', e, s', hp⟩ := seek_copy_safe hG hP hnn he hw hm hc hN offset fs ht (hraw hm hc ht)
823        exact ⟨r, fs', h', s', e, hp⟩
824      · by_cases hb : seekT s offset whence < s.x.pos.toInt
825        · obtain ⟨r, fs', h', e, s', hp⟩ := seek_back_safe hG hP hnn he hw hm hc hN offset fs ht hb
826          exact ⟨r, fs', h', s', e, hp⟩
827        · obtain ⟨r, h', s', e, hp⟩ := seek_fwd_safe hG hP hnn he hw hm hc hN offset fs ht (by omega)
828          exact ⟨r, fs, h', s', e, hp⟩
829    · obtain ⟨r, h', s', e, hp⟩ := seek_write_safe hG hP hnn he hw hm hN offset fs
830      exact ⟨r, fs, h', s', e, hp⟩
831  · have hhead := gzseek64_head hG hP hnn he hw offset fs
832    rw [ite_eq_right ht] at hhead
833    exact ⟨_, _, _, s, hhead, hG, hP, hN, sameCfg_refl s, Or.inl ⟨rfl, rfl, rfl⟩⟩
834
835/-- `gzseek64` refuses a handle with a serious error, and a `whence` other than `SEEK_SET` and `SEEK_CUR`: `-1`,
836nothing changes. -/
837theorem gzseek64_refuse {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) {whence : Int32} (offset : Int64) (fs : Fs)
838    (hb : (s.err ≠ Z_OK ∧ s.err ≠ Z_BUF_ERROR) ∨ (whence ≠ SEEK_SET ∧ whence ≠ SEEK_CUR)) :
839    gzseek64 (hnd gs) offset whence fs h = .ok ((-1, fs), h) := by
840  have hs := hG.hs
841  have hmo : ¬ (s.mode ≠ GZ_READ ∧ s.mode ≠ GZ_WRITE) := by rcases hG.mode with h1 | h1 <;> simp [h1]
842  unfold gzseek64
843  rcases hb with hb | hb
844  · ggsimp [hs, hmo, hb]
845  · by_cases he : ¬ s.err = Z_OK ∧ ¬ s.err = Z_BUF_ERROR
846    · ggsimp [hs, hmo, he]
847    · ggsimp [hs, hmo, he, hb]
848
849/-- `gzseek` is `gzseek64` (`z_off_t` is `long`: the range check `ret == (z_off_t)ret` always holds). -/
850theorem gzseek_eq (file : GzFilePtr) (offset : Int64) (whence : Int32) (fs : Fs) (h : Heap) :
851    gzseek file offset whence fs h = gzseek64 file offset whence fs h := by
852  unfold gzseek
853  simp only [G_bind_app]
854  cases hh : gzseek64 file offset whence fs h with
855  | error e => rfl
856  | ok v => obtain ⟨⟨a, fs1⟩, h1⟩ := v; simp [G_pure_app]
857
858
859/-! ### The undefined behaviour of the unpatched C (R-1)
860
861`gzseek(file, offset, SEEK_CUR)` while `gztell` is negative (right after `gzungetc` at the start of a file): the check
862`offset > GZ_OFF_MAX - pos` computes `GZ_OFF_MAX - pos` with `pos < 0`, which overflows. And `gzseek(file, offset,
863SEEK_SET)` with a negative `x.pos` and `offset - x.pos >= 2^63`: the subtraction `pos - x.pos` overflows. Both are
864`Fault.ub` in the translation. -/
865
866/-- The undefined behaviour of the unpatched C (the negative-position seek report in `docs/findings.md`): `SEEK_CUR` while `gztell` is negative (after `gzungetc` at the start of a file) makes `GZ_OFF_MAX - pos` overflow: `Fault.ub`, for every `offset`. -/
867theorem gzseek64_cur_negpos_ub {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s)
868    (he : s.err = Z_OK ∨ s.err = Z_BUF_ERROR) (hneg : tellPos s < 0) (hlo : -9223372036854775808 ≤ tellPos s)
869    (offset : Int64) (fs : Fs) :
870    gzseek64 (hnd gs) offset SEEK_CUR fs h = .error (.ub "signed overflow (long)") := by
871  have hs := hG.hs
872  have hOM := OffMax_val
873  have hne : ¬(¬ s.err = Z_OK ∧ ¬ s.err = Z_BUF_ERROR) := by rcases he with h1 | h1 <;> simp [h1]
874  have hmo : ¬ (s.mode ≠ GZ_READ ∧ s.mode ≠ GZ_WRITE) := by rcases hG.mode with h1 | h1 <;> simp [h1]
875  have hSC : SEEK_CUR ≠ SEEK_SET := by decide
876  have eT : i64add s.x.pos (if s.past = 0 then s.skip else 0) h = .ok (Int64.ofInt (tellPos s), h) := by
877    have := i64add_run s.x.pos (tellSkip s) (by unfold tellPos at hlo; omega) (by unfold tellPos at hneg; omega) h
878    by_cases hh : s.past = 0
879    · simpa [hh, tellSkip, tellPos] using this
880    · simpa [hh, tellSkip, tellPos] using this
881  have hp0 : (Int64.ofInt (tellPos s)).toInt = tellPos s := i64_toInt_ofInt hlo (by omega)
882  have hg := GZ_OFF_MAX_toInt
883  have fo : i64sub GZ_OFF_MAX (Int64.ofInt (tellPos s)) h = .error (.ub "signed overflow (long)") :=
884    i64sub_ub _ _ h (by rw [hp0, hg]; omega)
885  unfold gzseek64
886  ggsimp [hs, hmo, hne, hSC, eT, fo]
887
888/-- The undefined behaviour of the unpatched C: `SEEK_SET` at a negative `x.pos` with `offset - x.pos >= 2^63` makes `pos - x.pos` overflow: `Fault.ub`. -/
889theorem gzseek64_set_negpos_ub {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s)
890    (he : s.err = Z_OK ∨ s.err = Z_BUF_ERROR) (hneg : s.x.pos.toInt < 0) (offset : Int64) (hoff : 0 ≤ offset.toInt)
891    (hbig : 9223372036854775808 ≤ offset.toInt - s.x.pos.toInt) (fs : Fs) :
892    gzseek64 (hnd gs) offset SEEK_SET fs h = .error (.ub "signed overflow (long)") := by
893  have hs := hG.hs
894  have hOM := OffMax_val
895  have hne : ¬(¬ s.err = Z_OK ∧ ¬ s.err = Z_BUF_ERROR) := by rcases he with h1 | h1 <;> simp [h1]
896  have hmo : ¬ (s.mode ≠ GZ_READ ∧ s.mode ≠ GZ_WRITE) := by rcases hG.mode with h1 | h1 <;> simp [h1]
897  have hSC : SEEK_SET ≠ SEEK_CUR := by decide
898  have z0 : (0 : Int64).toInt = 0 := rfl
899  have hlt := offset.toInt_lt
900  have hgt := s.x.pos.le_toInt
901  obtain ⟨q1, q3, f1, f3, c1, c2, c5⟩ := seek_checks (p0 := 0) offset (by rw [z0]; exact Int.le_refl 0) h
902  rw [z0] at c1 c2 c5
903  obtain ⟨q5, f5, hq5, hq5i⟩ := c5 (by omega) (by omega)
904  have c6 : ¬ (q5 < s.x.pos) := by rw [i64_lt_iff, hq5i]; omega
905  have fo : ∀ h', i64sub q5 s.x.pos h' = .error (.ub "signed overflow (long)") := fun h' =>
906    i64sub_ub _ _ h' (by rw [hq5i]; omega)
907  unfold gzseek64
908  have r1 : ¬ OffMax < offset.toInt := by omega
909  have r2 : ¬ offset.toInt < 0 := by omega
910  by_cases hc : s.mode = GZ_READ ∧ s.how = GZ_COPY
911  · ggsimp [hs, hmo, hne, hSC, f1, f3, f5, c1, c2, c6, fo, r1, r2, hc]
912  · ggsimp [hs, hmo, hne, hSC, f1, f3, f5, c1, c2, c6, fo, r1, r2, hc]
913
914
915/-- **The dangling `x.next` (R-4).** A reader that is not in the raw area executes `x.next += n` on every forward seek;
916when `x.next` points to an object that no longer exists (the caller's buffer after a direct decompression, freed by the
917caller), the translation faults, although `n` is 0 and nothing is read through the pointer. Every other fault of the
918translation is excluded by the hypotheses. -/
919theorem seekTail_dangling_ub {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hm : s.mode = GZ_READ)
920    (hhow : s.how ≠ GZ_COPY) (hnn : 0 ≤ s.x.pos.toInt) {t : Int} (ht : SeekOk t) (hfw : s.x.pos.toInt ≤ t)
921    {r : BRef} {off : Nat} (hr : s.x.next = .ref r off) (hd : Space.get h r = none) (fs : Fs) :
922    seekTail (hnd gs) s (Int64.ofInt t) fs h = .error (.ub "arithmetic on a dangling pointer") := by
923  have hs := hG.hs
924  have hOM := OffMax_val
925  have ht1 := ht.1
926  have ht2 := ht.2
927  have hqi : (Int64.ofInt t).toInt = t := i64_toInt_ofInt (by omega) (by omega)
928  obtain ⟨q, hqd⟩ : ∃ q : Int64, q = Int64.ofInt t := ⟨_, rfl⟩
929  have hqi' : q.toInt = t := by rw [hqd]; exact hqi
930  obtain ⟨q2, hq2d⟩ : ∃ q2 : Int64, q2 = Int64.ofInt (t - s.x.pos.toInt) := ⟨_, rfl⟩
931  have hlt := s.x.pos.toInt_lt
932  have hq2 : q2.toInt = t - s.x.pos.toInt := by
933    rw [hq2d]; exact i64_toInt_ofInt (by omega) (by omega)
934  have fa : ∀ h', i64sub q s.x.pos h' = .ok (q2, h') := fun h' => by
935    have := i64sub_run q s.x.pos (by rw [hqi']; omega) (by rw [hqi']; omega) h'
936    rw [hqi', ← hq2d] at this; exact this
937  have c6 : ¬ (q < s.x.pos) := by rw [i64_lt_iff, hqi']; omega
938  have fn : ∀ (k : Int) (z : GzState), Ptr.add s.x.next k (setS h gs z) = .error (.ub "arithmetic on a dangling pointer") := by
939    intro k z
940    rw [hr]
941    have : Space.get (setS h gs z) r = none := by rw [space_get_setS]; exact hd
942    simp [Ptr.add, this]
943  rw [← hqd]
944  unfold seekTail
945  ggsimp [hs, hm, hhow, fa, c6, GT_OFF_run, fn]
946  by_cases hc : q2 < u32ToI64 s.x.«have»
947  · ggsimp [hs, hc, fn]
948  · ggsimp [hs, hc, fn]
949
950
951/-- The dangling `x.next` (the borrowed seek-pointer report in `docs/findings.md`): a forward seek of a reader outside the raw area executes `x.next += n` on a pointer to an object that no longer exists: `Fault.ub`, although nothing is read through it. -/
952theorem gzseek64_dangling_next_ub {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hP : PosInv s)
953    (hnn : 0 ≤ s.x.pos.toInt) (he : s.err = Z_OK ∨ s.err = Z_BUF_ERROR) {whence : Int32}
954    (hw : whence = SEEK_SET ∨ whence = SEEK_CUR) (hm : s.mode = GZ_READ) (hhow : s.how ≠ GZ_COPY)
955    (offset : Int64) (fs : Fs) (ht : SeekOk (seekT s offset whence)) (hfw : s.x.pos.toInt ≤ seekT s offset whence)
956    {r : BRef} {off : Nat} (hr : s.x.next = .ref r off) (hd : Space.get h r = none) :
957    gzseek64 (hnd gs) offset whence fs h = .error (.ub "arithmetic on a dangling pointer") := by
958  rw [gzseek64_head hG hP hnn he hw offset fs, ite_eq_left ht, seekTail_dangling_ub hG hm hhow hnn ht hfw hr hd fs]
959
960/-- A seek inside the raw area faults exactly when `hraw` of `seekTail_copy` fails: the C expression
961`pos - x.pos - have` overflows (positions within `2^32` of `2^63`). -/
962theorem seekTail_copy_ub {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (hm : s.mode = GZ_READ)
963    (hcopy : s.how = GZ_COPY) (hnn : 0 ≤ s.x.pos.toInt) {t : Int} (ht : SeekOk t)
964    (hraw : t - s.x.pos.toInt - s.x.«have».toNat < -9223372036854775808) (fs : Fs) :
965    seekTail (hnd gs) s (Int64.ofInt t) fs h = .error (.ub "signed overflow (long)") := by
966  have hs := hG.hs
967  have hOM := OffMax_val
968  have ht1 := ht.1
969  have ht2 := ht.2
970  have hhv := s.x.«have».toNat_lt
971  have hlt := s.x.pos.toInt_lt
972  have hqi : (Int64.ofInt t).toInt = t := i64_toInt_ofInt (by omega) (by omega)
973  obtain ⟨q2, hq2d⟩ : ∃ q2 : Int64, q2 = Int64.ofInt (t - s.x.pos.toInt) := ⟨_, rfl⟩
974  have hq2 : q2.toInt = t - s.x.pos.toInt := by
975    rw [hq2d]; exact i64_toInt_ofInt (by omega) (by omega)
976  have fa : i64sub (Int64.ofInt t) s.x.pos h = .ok (q2, h) := by
977    have := i64sub_run (Int64.ofInt t) s.x.pos (by rw [hqi]; omega) (by rw [hqi]; omega) h
978    rw [hqi, ← hq2d] at this; exact this
979  have fb : i64sub q2 (u32ToI64 s.x.«have») h = .error (.ub "signed overflow (long)") :=
980    i64sub_ub _ _ h (by rw [hq2, u32ToI64_toInt]; omega)
981  unfold seekTail
982  ggsimp [hs, hm, hcopy, fa, fb]
983
984end Zlib.Gzlib.Proofs