GzRead.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.GzOpen
2
3namespace ZlibF.Spec.Public
4open C Zlib.GzFs
5
6def ReadEffect (h after : Heap) (fs fs' : Fs) (i : Nat) (s s' : GzState)
7    (requested : Nat) (out : List UInt8) (regions : List Region) : Prop :=
8  GzStateFrame h after fs fs' i s s' regions ∧ out.length ≤ requested ∧
9  (s.mode ≠ GZ_READ → out = []) ∧
10  (s.skip = 0 → s'.x.pos.toInt = s.x.pos.toInt + (out.length : Int)) ∧
11  (∀ decoded buffered, FileData fs s decoded → Buffered h s buffered →
12    out <+: availableRead s buffered decoded ∧
13    (NoAllocationFailure h → s.mode = GZ_READ → s.err = Z_OK ∨ s.err = Z_BUF_ERROR →
14      out = (availableRead s buffered decoded).take requested))
15
16def ReturnedBytes (h : Heap) (p : BPtr) (bytes : List UInt8) : Prop :=
17  bytes = [] ∨ Bytes h p bytes.length bytes
18
19/-- `int gzread(gzFile file, voidp buf, unsigned len)`.
20Return bytes, EOF zero, or -1. Requests above INT_MAX fail before touching the output.
21Buffered bytes precede a later error; partial output remains part of the result. -/
22def Goal.gzread : Prop :=
23  (∀ h fs p n, Zlib.Gzread.gzread none p n fs h = .ok ((-1, fs), h)) ∧
24  (∀ h fs i s p n, GzReachable h fs i → GzValid h i s →
25    (n.toNat < 2 ^ 31 → GzRange h i s p n.toNat true) →
26    ∃ rc fs' after s' out,
27      Zlib.Gzread.gzread (some (.in_gzstate_x i)) p n fs h = .ok ((rc, fs'), after) ∧
28      ReturnedBytes after p out ∧
29      ReadEffect h after fs fs' i s s' (if n.toNat < 2 ^ 31 then n.toNat else 0) out [⟨p, out.length⟩] ∧
30      (rc = -1 ∧ out = [] ∨ 0 ≤ rc.toInt ∧ rc.toInt = (out.length : Int)) ∧
31      (2 ^ 31 ≤ n.toNat → rc = -1) ∧
32      (s.mode ≠ GZ_READ → rc = -1 ∧ after = h ∧ fs' = fs))
33
34/-- `z_size_t gzfread(voidp buf, z_size_t size, z_size_t nitems, gzFile file)`.
35Report complete items. A final partial item is still written and consumed. Multiplication
36overflow and zero-sized requests do not touch the destination. -/
37def Goal.gzfread : Prop :=
38  (∀ h fs p size n, Zlib.Gzread.gzfread p size n none fs h = .ok ((0, fs), h)) ∧
39  (∀ h fs i s p size n, GzReachable h fs i → GzValid h i s →
40    (size.toNat * n.toNat < 2 ^ 64 → GzRange h i s p (size.toNat * n.toNat) true) →
41    ∃ items fs' after s' out,
42      Zlib.Gzread.gzfread p size n (some (.in_gzstate_x i)) fs h = .ok ((items, fs'), after) ∧
43      ReturnedBytes after p out ∧
44      ReadEffect h after fs fs' i s s'
45        (if size.toNat * n.toNat < 2 ^ 64 then size.toNat * n.toNat else 0)
46        out [⟨p, out.length⟩] ∧
47      items.toNat = (if size = 0 then 0 else out.length / size.toNat) ∧ items ≤ n ∧
48      (2 ^ 64 ≤ size.toNat * n.toNat → items = 0 ∧ out = []))
49
50def GetcContract (program : GzFilePtr → G Int32) : Prop :=
51  (∀ h fs, program none fs h = .ok ((-1, fs), h)) ∧
52  (∀ h fs i s, GzReachable h fs i → GzValid h i s →
53    ∃ rc fs' after s' out, program (some (.in_gzstate_x i)) fs h = .ok ((rc, fs'), after) ∧
54      ReadEffect h after fs fs' i s s' 1 out [] ∧
55      ((rc = -1 ∧ out = []) ∨ ∃ b, out = [b] ∧ rc.toInt = b.toNat))
56
57/-- `int gzgetc(gzFile file)`; byte values are unsigned 0..255, distinct from EOF -1. -/
58def Goal.gzgetc : Prop := GetcContract Zlib.Gzread.gzgetc
59
60/-- `int gzgetc_(gzFile file)`; the exported wrapper retains the byte/EOF distinction. -/
61def Goal.gzgetc_ : Prop := GetcContract Zlib.Gzread.gzgetc_
62
63/-- `int gzungetc(int c, gzFile file)`.
64On success store the low byte but return the original nonnegative integer. Clear past-EOF.
65The initial look and pending skip can precede rejection of a negative character. -/
66def Goal.gzungetc : Prop :=
67  (∀ h fs c, Zlib.Gzread.gzungetc c none fs h = .ok ((-1, fs), h)) ∧
68  (∀ h fs i s c, GzReachable h fs i → GzValid h i s →
69    ∃ rc fs' after s',
70      Zlib.Gzread.gzungetc c (some (.in_gzstate_x i)) fs h = .ok ((rc, fs'), after) ∧
71      GzStateFrame h after fs fs' i s s' [] ∧
72      (rc = -1 ∨ (rc = c ∧ 0 ≤ c.toInt ∧ s'.past = 0 ∧
73        ∃ rest, Buffered after s' (c.toUInt32.toUInt8 :: rest))) ∧
74      (c.toInt < 0 ∨ s.mode ≠ GZ_READ → rc = -1) ∧
75      (rc ≠ -1 → s.skip = 0 → s'.x.pos.toInt = s.x.pos.toInt - 1))
76
77/-- `char *gzgets(gzFile file, char *buf, int len)`.
78Copy at most len-1 bytes, stopping after the first newline, and append a NUL on success.
79Length one succeeds with an empty string; an EOF with no bytes returns null for larger lengths. -/
80def Goal.gzgets : Prop :=
81  (∀ h fs p n, Zlib.Gzread.gzgets none p n fs h = .ok ((.null, fs), h)) ∧
82  (∀ h fs i s p n, GzReachable h fs i → GzValid h i s →
83    (0 < n.toInt → p ≠ .null → GzRange h i s p n.toInt.toNat true) →
84    ∃ result fs' after s' out,
85      Zlib.Gzread.gzgets (some (.in_gzstate_x i)) p n fs h = .ok ((result, fs'), after) ∧
86      GzStateFrame h after fs fs' i s s' [⟨p, if result = .null then out.length else out.length + 1⟩] ∧
87      out.length ≤ n.toInt.toNat - 1 ∧
88      (result = .null → out = []) ∧
89      (result = .null ∨ result = p ∧ Bytes after p (out.length + 1) (out ++ [0])) ∧
90      (∀ left right, out = left ++ 10 :: right → right = []) ∧
91      (p = .null ∨ n.toInt < 1 ∨ s.mode ≠ GZ_READ → result = .null ∧ after = h ∧ fs' = fs) ∧
92      (∀ decoded buffered, FileData fs s decoded → Buffered h s buffered →
93        out <+: availableRead s buffered decoded ∧
94        (NoAllocationFailure h → s.mode = GZ_READ → p ≠ .null → 0 < n.toInt →
95          s.err = Z_OK ∨ s.err = Z_BUF_ERROR →
96          let line := ((availableRead s buffered decoded).takeWhile (fun b => b != 10))
97          let full := if line.length < (availableRead s buffered decoded).length then line ++ [10] else line
98          out = full.take (n.toInt.toNat - 1) ∧
99            (n = 1 ∨ full ≠ [] → result = p))))
100
101/-- `int gzdirect(gzFile file)`.
102The query may initialize and inspect a reader. Its result is exactly the resulting direct-mode flag. -/
103def Goal.gzdirect : Prop :=
104  (∀ h fs, Zlib.Gzread.gzdirect none fs h = .ok ((0, fs), h)) ∧
105  (∀ h fs i s, GzReachable h fs i → GzValid h i s →
106    ∃ rc fs' after s', Zlib.Gzread.gzdirect (some (.in_gzstate_x i)) fs h = .ok ((rc, fs'), after) ∧
107      GzStateFrame h after fs fs' i s s' [] ∧
108      rc = (if s'.direct = 1 then 1 else 0) ∧
109      (s.mode ≠ GZ_READ ∨ s.how ≠ LOOK ∨ s.x.have ≠ 0 → after = h ∧ fs' = fs))
110
111end ZlibF.Spec.Public