public-gz-rewind.lean

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

1import ZlibF.Proof.«public-gz-offset»
2
3namespace ZlibF.Spec.Public.GzRewindProof
4open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib Zlib.Gzlib.Spec Zlib.Gzlib.Proofs ZlibF.Spec.Public.OffsetProof
5
6private theorem gzrewind_null (fs : Fs) (h : Heap) : gzrewind none fs h = .ok ((-1, fs), h) := rfl
7
8theorem gz_reset_record {h : Heap} {i : Nat} {s : GzState}
9    (hs : h.gzstates i = some s)
10    (hmsg : s.msg = .null ∨ ∃ b a, s.msg = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false)
11    (hmem : s.err = Z_MEM_ERROR → s.msg = .null) :
12    gz_reset (some (.tab i)) h = .ok ((), setS (freeStr h s.msg) i (resetRec s)) := by
13  unfold gz_reset
14  rcases hmsg with hn | ⟨mb,a,hm,ha,hro⟩
15  · by_cases hmo : s.mode = GZ_READ <;> gsimp [hs, hn, hmo, gz_error, resetRec]
16  · have hne : s.err ≠ Z_MEM_ERROR := fun he => by
17      have hnull := hmem he
18      rw [hm] at hnull
19      cases hnull
20    by_cases hmo : s.mode = GZ_READ <;>
21      gsimp [hs, hm, hne, hmo, freeB_blk_setS ha hro, gz_error, resetRec]
22
23/-- `int gzrewind(gzFile file)` gives the exact seek result and resets only on
24success. It requires no invariant on inactive data buffers. -/
25theorem gzrewind_record {h : Heap} {i : Nat} {s : GzState}
26    (hs : h.gzstates i = some s)
27    (hmsg : s.msg = .null ∨ ∃ b a, s.msg = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false)
28    (hmem : s.err = Z_MEM_ERROR → s.msg = .null) (fs : Fs) :
29    gzrewind (hnd i) fs h =
30      if s.mode ≠ GZ_READ ∨ (s.err ≠ Z_OK ∧ s.err ≠ Z_BUF_ERROR) then .ok ((-1, fs), h)
31      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)
32      else .ok ((0, (lseekRes s.fd s.start SEEK_SET fs).2), setS (freeStr h s.msg) i (resetRec s)) := by
33  unfold gzrewind
34  by_cases hc : s.mode ≠ GZ_READ ∨ (s.err ≠ Z_OK ∧ s.err ≠ Z_BUF_ERROR)
35  · offsetsimp [hs, hc]
36  · by_cases hl : (lseekRes s.fd s.start SEEK_SET fs).1 = -1
37    · offsetsimp [hs, hc, hl]
38    · offsetsimp [hs, hc, hl, gz_reset_record hs hmsg hmem]
39
40theorem lseek_set_success (fd : Int32) (off : Int64) (fs : Fs)
41    (hok : (lseekRes fd off SEEK_SET fs).1 ≠ -1) :
42    ∃ file, (lseekRes fd off SEEK_SET fs).2.fds[fd.toInt.toNat]? = some (some file) ∧
43      file.pos = off.toInt.toNat := by
44  by_cases hn : fd < 0
45  · simp [lseekRes, fsLseek, hn, pure_app] at hok
46  · by_cases hi : fd.toInt ≥ (fs.fds.size : Int)
47    · simp [lseekRes, fsLseek, hn, hi, pure_app] at hok
48    · have hidx : fd.toInt.toNat < fs.fds.size := by
49        have hnonneg : ¬ fd.toInt < 0 := fun he => hn (Int32.lt_iff_toInt_lt.mpr (by simpa using he))
50        omega
51      change fd.toNatClampNeg < fs.fds.size at hidx
52      have hget : fs.fds[fd.toNatClampNeg]! = fs.fds[fd.toNatClampNeg] := getElem!_pos fs.fds fd.toNatClampNeg hidx
53      cases hf : fs.fds[fd.toNatClampNeg] with
54      | none => simp [lseekRes, fsLseek, hn, hi, hget, hf, pure_app] at hok
55      | some f =>
56        by_cases hneg : off.toInt < 0
57        · simp [lseekRes, fsLseek, hn, hi, hget, hf, SEEK_SET, hneg, pure_app] at hok
58        · have hup : ¬ 9223372036854775807 < off.toInt := by have := off.toInt_lt; omega
59          refine ⟨{ f with pos := off.toInt.toNat }, ?_, rfl⟩
60          simp [lseekRes, fsLseek, hn, hi, hget, hf, SEEK_SET, hneg, hup, pure_app,
61            Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds, hidx]
62
63
64
65/-- `int gzrewind(gzFile file)`
66The exact public result, state, frame and ownership contract. -/
67theorem rewind_public : Goal.gzrewind := by
68  constructor
69  · intro h fs
70    exact gzrewind_null fs h
71  · intro h fs i s hreach hv
72    have hs := hv.1
73    have hmsg : s.msg = .null ∨ ∃ b a, s.msg = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false := by
74      rcases hv.2.2.2.2.2.2.1 with hn | ⟨msg,hc,b,a,hp,ha,hro,hsize⟩
75      · exact Or.inl hn
76      · exact Or.inr ⟨b,a,hp,ha,hro⟩
77    have hmem : s.err = Z_MEM_ERROR → s.msg = .null := hv.2.2.2.2.2.2.2.1
78    have hfree : freeStr h s.msg = dropWindow h s.msg := by
79      rcases hmsg with hn | ⟨b,a,hp,ha,hro⟩
80      · simp [hn, dropWindow]
81      · simp [hp, dropWindow]
82    have hr := gzrewind_record hs hmsg hmem fs
83    by_cases hc : s.mode ≠ GZ_READ ∨ (s.err ≠ Z_OK ∧ s.err ≠ Z_BUF_ERROR)
84    · refine ⟨-1,fs,h, ?_, Or.inl ⟨rfl,rfl⟩, fun _ => ⟨rfl,rfl⟩⟩
85      simpa [hc, hnd] using hr
86    · by_cases hl : (lseekRes s.fd s.start SEEK_SET fs).1 = -1
87      · refine ⟨-1,(lseekRes s.fd s.start SEEK_SET fs).2,h, ?_, Or.inl ⟨rfl,rfl⟩, ?_⟩
88        · simpa [hc,hl,hnd] using hr
89        · intro bad
90          exact (hc bad).elim
91      · have hread : s.mode = GZ_READ := by
92          by_cases hm : s.mode = GZ_READ
93          · exact hm
94          · exact (hc (Or.inl hm)).elim
95        have hex := lseek_set_success s.fd s.start fs hl
96        refine ⟨0,(lseekRes s.fd s.start SEEK_SET fs).2,setS (freeStr h s.msg) i (resetRec s), ?_, Or.inr ⟨rfl, ?_, hex⟩, ?_⟩
97        · simpa [hc,hl,hnd] using hr
98        · simp [setS, putGz, resetRec, rewoundState, hread, hfree]
99        · intro bad
100          exact (hc bad).elim
101
102
103#print axioms rewind_public
104end ZlibF.Spec.Public.GzRewindProof