GzWrite.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.GzRead
2
3namespace ZlibF.Spec.Public
4open C Zlib.GzFs
5
6def WriteRoom (fs : Fs) (s : GzState) (n : Nat) : Prop :=
7  ∃ file node, 0 ≤ s.fd.toInt ∧ fs.fds[s.fd.toInt.toNat]? = some (some file) ∧
8    file.wr = true ∧ fs.nodes[file.node]? = some node ∧ node.isDir = false ∧
9    max node.data.size file.pos + 2 * (n + s.strm.avail_in.toNat +
10      s.skip.toInt.toNat + 2 * s.size.toNat) + 1024 ≤ fs.fsizeLimit ∧
11    s.x.pos.toInt + s.skip.toInt + (n : Int) < 2 ^ 63
12
13def WriterReady (s : GzState) : Prop :=
14  s.mode = GZ_WRITE ∧ (s.err = Z_OK ∨ s.again ≠ 0) ∧
15  -1 ≤ s.level.toInt ∧ s.level.toInt ≤ 9 ∧ 0 ≤ s.strategy.toInt ∧ s.strategy.toInt ≤ 4
16
17/-- Account for accepted input separately from the reported count. A hard write error can
18return zero after accepting a prefix. A pending forward seek contributes zero-filled input. -/
19def WriteEffect (h after : Heap) (fs fs' : Fs) (i : Nat) (s s' : GzState)
20    (input : List UInt8) (accepted : Nat) : Prop :=
21  GzStateFrame h after fs fs' i s s' [] ∧ accepted ≤ input.length ∧
22  ∃ zeros, zeros ≤ s.skip.toInt.toNat ∧
23    s'.x.pos.toInt = s.x.pos.toInt + (zeros : Int) + (accepted : Int)
24
25/-- `int gzwrite(gzFile file, voidpc buf, unsigned len)`.
26Requests above INT_MAX return zero. A positive result counts accepted bytes. Allocation,
27descriptor and size-limit failures retain the prefix already accepted by the encoder. -/
28def Goal.gzwrite : Prop :=
29  (∀ h fs p n, Zlib.Gzwrite.gzwrite none p n fs h = .ok ((0, fs), h)) ∧
30  (∀ h fs i s p n input, GzReachable h fs i → GzValid h i s →
31    (n.toNat < 2 ^ 31 → Bytes h p n.toNat input ∧ GzRange h i s p n.toNat false) →
32    ∃ rc fs' after s' accepted,
33      Zlib.Gzwrite.gzwrite (some (.in_gzstate_x i)) p n fs h = .ok ((rc, fs'), after) ∧
34      WriteEffect h after fs fs' i s s' (if n.toNat < 2 ^ 31 then input else []) accepted ∧
35      0 ≤ rc.toInt ∧ rc.toInt ≤ (accepted : Int) ∧
36      (rc ≠ 0 → rc.toInt = accepted) ∧
37      (2 ^ 31 ≤ n.toNat ∨ s.mode ≠ GZ_WRITE → rc = 0) ∧
38      (NoAllocationFailure h → WriterReady s → WriteRoom fs s n.toNat → n.toNat < 2 ^ 31 →
39        rc.toInt = n.toNat))
40
41/-- `z_size_t gzfwrite(voidpc buf, z_size_t size, z_size_t nitems, gzFile file)`.
42Return whole items. Zero-sized and overflowing products report zero without reading input. -/
43def Goal.gzfwrite : Prop :=
44  (∀ h fs p size n, Zlib.Gzwrite.gzfwrite p size n none fs h = .ok ((0, fs), h)) ∧
45  (∀ h fs i s p size n input, GzReachable h fs i → GzValid h i s →
46    (size.toNat * n.toNat < 2 ^ 64 →
47      Bytes h p (size.toNat * n.toNat) input ∧ GzRange h i s p (size.toNat * n.toNat) false) →
48    ∃ items fs' after s' accepted,
49      Zlib.Gzwrite.gzfwrite p size n (some (.in_gzstate_x i)) fs h = .ok ((items, fs'), after) ∧
50      WriteEffect h after fs fs' i s s'
51        (if size.toNat * n.toNat < 2 ^ 64 then input else []) accepted ∧
52      items ≤ n ∧ (items = 0 ∨ items.toNat = accepted / size.toNat) ∧
53      (size = 0 ∨ 2 ^ 64 ≤ size.toNat * n.toNat ∨ s.mode ≠ GZ_WRITE → items = 0) ∧
54      (NoAllocationFailure h → WriterReady s → WriteRoom fs s (size.toNat * n.toNat) →
55        0 < size.toNat → size.toNat * n.toNat < 2 ^ 64 → items = n))
56
57/-- `int gzputc(gzFile file, int c)`.
58Convert to an unsigned byte. Success returns that byte even when the original integer was negative. -/
59def Goal.gzputc : Prop :=
60  (∀ h fs c, Zlib.Gzwrite.gzputc none c fs h = .ok ((-1, fs), h)) ∧
61  (∀ h fs i s c, GzReachable h fs i → GzValid h i s →
62    ∃ rc fs' after s' accepted,
63      Zlib.Gzwrite.gzputc (some (.in_gzstate_x i)) c fs h = .ok ((rc, fs'), after) ∧
64      WriteEffect h after fs fs' i s s' [c.toUInt32.toUInt8] accepted ∧
65      (rc = -1 ∨ rc = (c &&& 255) ∧ accepted = 1) ∧
66      (NoAllocationFailure h → WriterReady s → WriteRoom fs s 1 → rc = (c &&& 255)))
67
68/-- `int gzputs(gzFile file, const char *str)`.
69Write the characters before NUL. An empty string returns zero; a nonempty string that accepts
70nothing returns -1, unlike `gzwrite`'s zero. -/
71def Goal.gzputs : Prop :=
72  (∀ h fs p, Zlib.Gzwrite.gzputs none p fs h = .ok ((-1, fs), h)) ∧
73  (∀ h fs i s p input, GzReachable h fs i → GzValid h i s →
74    CString h p input → GzRange h i s p (input.length + 1) false →
75    ∃ rc fs' after s' accepted,
76      Zlib.Gzwrite.gzputs (some (.in_gzstate_x i)) p fs h = .ok ((rc, fs'), after) ∧
77      WriteEffect h after fs fs' i s s' input accepted ∧
78      (rc = -1 ∨ 0 ≤ rc.toInt ∧ rc.toInt = accepted) ∧
79      (2 ^ 31 ≤ input.length ∨ s.mode ≠ GZ_WRITE → rc = -1) ∧
80      (NoAllocationFailure h → WriterReady s → WriteRoom fs s input.length → input.length < 2 ^ 31 →
81        rc.toInt = input.length))
82
83def FormatCaller (h : Heap) (i : Nat) (s : GzState) (format : BPtr) (args : List VaArg) : Prop :=
84  (∃ bytes, CString h format bytes ∧ GzRange h i s format (bytes.length + 1) false) ∧
85  ∀ p, VaArg.str p ∈ args → p = .null ∨ ∃ bytes, CString h p bytes ∧ GzRange h i s p (bytes.length + 1) false
86
87def PrintContract (program : GzFilePtr → BPtr → List VaArg → G Int32) : Prop :=
88  (∀ h fs format args, program none format args fs h = .ok ((Z_STREAM_ERROR, fs), h)) ∧
89  (∀ h fs i s format args text, GzReachable h fs i → GzValid h i s →
90    Formatted h format args text → FormatCaller h i s format args →
91    ∃ rc fs' after s' accepted,
92      program (some (.in_gzstate_x i)) format args fs h = .ok ((rc, fs'), after) ∧
93      WriteEffect h after fs fs' i s s' text accepted ∧
94      (0 < rc.toInt → rc.toInt = text.length ∧ accepted = text.length) ∧
95      (s.mode ≠ GZ_WRITE → rc = Z_STREAM_ERROR) ∧
96      (NoAllocationFailure h → WriterReady s → WriteRoom fs s text.length →
97        rc.toInt = if text.length < (if s.size = 0 then s.want.toNat else s.size.toNat) then text.length else 0))
98
99/-- `int gzvprintf(gzFile file, const char *format, va_list va)`.
100The fixed external formatter supplies the formatted bytes. Wrong mode and serious errors
101return a negative zlib code; an empty or oversized formatted result returns zero. -/
102def Goal.gzvprintf : Prop := PrintContract Zlib.Gzwrite.gzvprintf
103
104/-- `int gzprintf(gzFile file, const char *format, ...)`.
105The variadic wrapper uses the same typed argument sequence and error/result contract. -/
106def Goal.gzprintf : Prop := PrintContract Zlib.Gzwrite.gzprintf
107
108/-- `int gzflush(gzFile file, int flush)`.
109Finish pending zeros and flush the encoder. Invalid modes and flush values return a stream
110error. Z_FINISH completes a gzip member; later writes can start another member. -/
111def Goal.gzflush : Prop :=
112  (∀ h fs flush, Zlib.Gzwrite.gzflush none flush fs h = .ok ((Z_STREAM_ERROR, fs), h)) ∧
113  (∀ h fs i s flush, GzReachable h fs i → GzValid h i s →
114    ∃ rc fs' after s',
115      Zlib.Gzwrite.gzflush (some (.in_gzstate_x i)) flush fs h = .ok ((rc, fs'), after) ∧
116      GzStateFrame h after fs fs' i s s' [] ∧
117      (s.mode ≠ GZ_WRITE ∨ flush.toInt < 0 ∨ 4 < flush.toInt → rc = Z_STREAM_ERROR) ∧
118      (s.mode = GZ_WRITE → s.err = Z_OK ∨ s.again ≠ 0 →
119        0 ≤ flush.toInt → flush.toInt ≤ 4 → rc = s'.err) ∧
120      (NoAllocationFailure h → WriterReady s → WriteRoom fs s 0 →
121        0 ≤ flush.toInt → flush.toInt ≤ 4 → rc = Z_OK ∧ s'.skip = 0))
122
123/-- `int gzsetparams(gzFile file, int level, int strategy)`.
124Only a compressed writer can change parameters. Preserve previously buffered input while
125flushing the old settings. The header does not promise rejection of invalid level/strategy
126values. The current entry stores those values even if the inner parameter change refuses them;
127do not invent a Z_STREAM_ERROR guarantee for that case. -/
128def Goal.gzsetparams : Prop :=
129  (∀ h fs level strategy, Zlib.Gzwrite.gzsetparams none level strategy fs h = .ok ((Z_STREAM_ERROR, fs), h)) ∧
130  (∀ h fs i s level strategy, GzReachable h fs i → GzValid h i s →
131    ∃ rc fs' after s',
132      Zlib.Gzwrite.gzsetparams (some (.in_gzstate_x i)) level strategy fs h = .ok ((rc, fs'), after) ∧
133      GzStateFrame h after fs fs' i s s' [] ∧
134      (rc = Z_OK ∨ rc = Z_STREAM_ERROR ∨ rc = Z_ERRNO ∨ rc = Z_MEM_ERROR ∨ rc = Z_BUF_ERROR) ∧
135      (s.mode ≠ GZ_WRITE ∨ s.direct ≠ 0 ∨ (s.err ≠ Z_OK ∧ s.again = 0) →
136        rc = Z_STREAM_ERROR ∧ after = h ∧ fs' = fs) ∧
137      (rc = Z_OK → s'.level = level ∧ s'.strategy = strategy) ∧
138      (rc = Z_OK → s.size ≠ 0 → -1 ≤ level.toInt → level.toInt ≤ 9 →
139        0 ≤ strategy.toInt → strategy.toInt ≤ 4 →
140        ∃ state inner, s'.strm.state = some (.deflate state) ∧ after.dstates state = some inner ∧
141          inner.level = (if level = -1 then 6 else level) ∧ inner.strategy = strategy) ∧
142      (NoAllocationFailure h → WriterReady s → s.direct = 0 → WriteRoom fs s 0 →
143        -1 ≤ level.toInt → level.toInt ≤ 9 → 0 ≤ strategy.toInt → strategy.toInt ≤ 4 → rc = Z_OK))
144
145end ZlibF.Spec.Public