GzControl.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.GzState
2import ZlibF.Spec.Public.Queries
3
4namespace ZlibF.Spec.Public
5open C Zlib.GzFs
6
7def putGz (h : Heap) (i : Nat) (s : GzState) : Heap :=
8  { h with gzstates := upd h.gzstates i (some s) }
9
10/-- `int gzbuffer(gzFile file, unsigned size)`.
11The current source clamps to eight bytes. It refuses initialized buffers and doubled-size overflow. -/
12def Goal.gzbuffer : Prop :=
13  (∀ h size, C.run (Zlib.Gzlib.gzbuffer none size) h = .ok (-1, h)) ∧
14  (∀ h i s size, h.gzstates i = some s →
15    C.run (Zlib.Gzlib.gzbuffer (some (.in_gzstate_x i)) size) h =
16      if (s.mode ≠ GZ_READ ∧ s.mode ≠ GZ_WRITE) ∨ s.size ≠ 0 ∨ 2 ^ 31 ≤ size.toNat then
17        .ok (-1, h)
18      else .ok (0, putGz h i { s with want := UInt32.ofNat (max size.toNat 8) }))
19
20/-- `int gzeof(gzFile file)`.
21Report a read past the end, rather than merely the last successful byte. Writers report zero. -/
22def Goal.gzeof : Prop :=
23  (∀ h, C.run (Zlib.Gzlib.gzeof none) h = .ok (0, h)) ∧
24  (∀ h i s, h.gzstates i = some s → C.run (Zlib.Gzlib.gzeof (some (.in_gzstate_x i))) h =
25    .ok ((if s.mode = GZ_READ then s.past else 0), h))
26
27def tellValue (s : GzState) : Int := s.x.pos.toInt + if s.past ≠ 0 then 0 else s.skip.toInt
28
29def TellContract (program : GzFilePtr → M Int64) : Prop :=
30  (∀ h, C.run (program none) h = .ok (-1, h)) ∧
31  (∀ h fs i s, GzReachable h fs i → GzValid h i s →
32    C.run (program (some (.in_gzstate_x i))) h =
33      .ok ((if -(2 ^ 63) ≤ tellValue s ∧ tellValue s < 2 ^ 63 then Int64.ofInt (tellValue s) else -1), h))
34
35/-- `z_off64_t gztell64(gzFile file)`; uncompressed position, including a pending seek except after EOF. -/
36def Goal.gztell64 : Prop := TellContract Zlib.Gzlib.gztell64
37
38/-- `z_off_t gztell(gzFile file)`; the LP64 wrapper retains the signed 64-bit range. -/
39def Goal.gztell : Prop := TellContract Zlib.Gzlib.gztell
40
41def OffsetContract (program : GzFilePtr → G Int64) : Prop :=
42  (∀ h fs, program none fs h = .ok ((-1, fs), h)) ∧
43  (∀ h fs i s, GzReachable h fs i → GzValid h i s → FileSystem fs →
44    ∃ value fs', program (some (.in_gzstate_x i)) fs h = .ok ((value, fs'), h) ∧
45      { fs' with errno := fs.errno } = fs ∧
46      (if s.fd.toInt < 0 then value = -1 else match fs.fds[s.fd.toInt.toNat]? with
47       | some (some file) => value.toInt = (file.pos : Int) -
48           (if s.mode = GZ_READ then s.strm.avail_in.toNat else 0)
49       | _ => value = -1))
50
51/-- `z_off64_t gzoffset64(gzFile file)`.
52The physical descriptor position excludes compressed input already buffered by a reader. -/
53def Goal.gzoffset64 : Prop := OffsetContract Zlib.Gzlib.gzoffset64
54
55/-- `z_off_t gzoffset(gzFile file)`; the LP64 wrapper has the same physical-position contract. -/
56def Goal.gzoffset : Prop := OffsetContract Zlib.Gzlib.gzoffset
57
58def intBytes (n : Int32) : List UInt8 :=
59  (List.range 4).map fun j => UInt8.ofNat (n.toUInt32.toNat / 256 ^ j % 256)
60
61/-- `const char *gzerror(gzFile file, int *errnum)`.
62Store the optional error code and return a borrowed message pointer. The query allocates nothing. -/
63def Goal.gzerror : Prop :=
64  (∀ h errnum, C.run (Zlib.Gzlib.gzerror none errnum) h = .ok (.null, h)) ∧
65  (∀ h i s errnum, GzValid h i s →
66    (errnum ≠ .null → GzRange h i s errnum 4 true) →
67    ∃ pointer after, C.run (Zlib.Gzlib.gzerror (some (.in_gzstate_x i)) errnum) h = .ok (pointer, after) ∧
68      Store h errnum (if errnum = .null then [] else intBytes s.err) after ∧
69      (if s.err = Z_MEM_ERROR then StaticString after pointer "out of memory"
70       else if s.msg = .null then StaticString after pointer "" else pointer = s.msg))
71
72/-- `void gzclearerr(gzFile file)`.
73Clear the error and message, and rearm EOF detection for readers. Free the old owned message. -/
74def Goal.gzclearerr : Prop :=
75  (∀ h, C.run (Zlib.Gzlib.gzclearerr none) h = .ok ((), h)) ∧
76  (∀ h i s, GzValid h i s →
77    C.run (Zlib.Gzlib.gzclearerr (some (.in_gzstate_x i))) h = .ok ((),
78      putGz (dropWindow h s.msg) i { s with
79        eof := if s.mode = GZ_READ then 0 else s.eof
80        past := if s.mode = GZ_READ then 0 else s.past
81        err := Z_OK, msg := .null }))
82
83def rewoundState (s : GzState) : GzState :=
84  { s with
85    eof := 0, past := 0, how := LOOK, junk := -1, again := 0, skip := 0, err := Z_OK, msg := .null
86    x := { s.x with «have» := 0, pos := 0 }
87    strm := { s.strm with avail_in := 0 } }
88
89/-- `int gzrewind(gzFile file)`.
90Seek back to the saved descriptor start, discard buffered output and reset reader bookkeeping. -/
91def Goal.gzrewind : Prop :=
92  (∀ h fs, Zlib.Gzlib.gzrewind none fs h = .ok ((-1, fs), h)) ∧
93  (∀ h fs i s, GzReachable h fs i → GzValid h i s →
94    ∃ rc fs' after, Zlib.Gzlib.gzrewind (some (.in_gzstate_x i)) fs h = .ok ((rc, fs'), after) ∧
95      ((rc = -1 ∧ after = h) ∨
96       (rc = 0 ∧ after = putGz (dropWindow h s.msg) i (rewoundState s) ∧
97        ∃ file, fs'.fds[s.fd.toInt.toNat]? = some (some file) ∧ file.pos = s.start.toInt.toNat)) ∧
98      (s.mode ≠ GZ_READ ∨ (s.err ≠ Z_OK ∧ s.err ≠ Z_BUF_ERROR) → rc = -1 ∧ fs' = fs))
99
100def SeekContract (program : GzFilePtr → Int64 → Int32 → G Int64) : Prop :=
101  (∀ h fs offset whence, program none offset whence fs h = .ok ((-1, fs), h)) ∧
102  (∀ h fs i s offset whence, GzReachable h fs i → GzValid h i s → FileSystem fs →
103    ∃ rc fs' after s', program (some (.in_gzstate_x i)) offset whence fs h = .ok ((rc, fs'), after) ∧
104      GzStateFrame h after fs fs' i s s' [] ∧
105      (rc = -1 ∨ (0 ≤ rc.toInt ∧ rc.toInt =
106        (if whence = 0 then 0 else tellValue s) + offset.toInt)) ∧
107      (whence ≠ 0 ∧ whence ≠ 1 → rc = -1 ∧ after = h) ∧
108      (rc = -1 → after = h) ∧
109      (0 ≤ rc.toInt → s'.x.pos.toInt + s'.skip.toInt = rc.toInt ∧
110        s'.skip.toInt ≥ 0) ∧
111      (s.mode = GZ_WRITE → rc.toInt < s.x.pos.toInt → rc = -1))
112
113/-- `z_off64_t gzseek64(gzFile file, z_off64_t offset, int whence)`.
114Signed range checks are obligations, including negative positions created by pushback.
115A successful seek can remain pending; EOF affects the separate tell query. -/
116def Goal.gzseek64 : Prop := SeekContract Zlib.Gzlib.gzseek64
117
118/-- `z_off_t gzseek(gzFile file, z_off_t offset, int whence)`; the LP64 conversion preserves the result. -/
119def Goal.gzseek : Prop := SeekContract Zlib.Gzlib.gzseek
120
121end ZlibF.Spec.Public