Calls.lean

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

1import ZlibF.Zlib.«adler32.c»
2import ZlibF.Zlib.«compress.c»
3import ZlibF.Zlib.«crc32.c»
4import ZlibF.Zlib.«deflate.c»
5import ZlibF.Zlib.«gzclose.c»
6import ZlibF.Zlib.«gzlib.c»
7import ZlibF.Zlib.«gzread.c»
8import ZlibF.Zlib.«gzwrite.c»
9import ZlibF.Zlib.«infback.c»
10import ZlibF.Zlib.«inflate.c»
11import ZlibF.Zlib.«uncompr.c»
12import ZlibF.Zlib.«zutil.c»
13
14/-!
15# Concrete public calls
16
17Generated by `scripts/gen_public_calls.py`. The inventory fixes the exported entry names.
18Arguments and results retain the types of the actual translations. Every constructor runs
19that entry directly. No replaceable execution relation or callee contract occurs here.
20The shared state includes the runtime heap and, for gz operations, the file-system model.
21This catalogue defines execution, not the permitted caller domain or the final contract.
22-/
23
24namespace ZlibF.Spec.Public
25open C Zlib.GzFs Zlib.Infback
26
27/-- Public entry calls for the default LP64 Linux build. Macro aliases use their C entries. -/
28inductive Call where
29  | adler32 (adler : UInt64) (buf : BPtr) (len : UInt32)
30  | adler32_combine (adler1 adler2 : UInt64) (len2 : Int64)
31  | adler32_combine64 (adler1 adler2 : UInt64) (len2 : Int64)
32  | adler32_z (adler : UInt64) (buf : BPtr) (len : UInt64)
33  | compress (dest : BPtr) (destLen : Option UInt64) (source : BPtr) (sourceLen : UInt64)
34  | compress2 (dest : BPtr) (destLen : Option UInt64) (source : BPtr) (sourceLen : UInt64) (level : Int32)
35  | compress2_z (dest : BPtr) (destLen : Option UInt64) (source : BPtr) (sourceLen : UInt64) (level : Int32)
36  | compressBound (sourceLen : UInt64)
37  | compressBound_z (sourceLen : UInt64)
38  | compress_z (dest : BPtr) (destLen : Option UInt64) (source : BPtr) (sourceLen : UInt64)
39  | crc32 (crc : UInt64) (buf : BPtr) (len : UInt32)
40  | crc32_combine (crc1 crc2 : UInt64) (len2 : Int64)
41  | crc32_combine64 (crc1 crc2 : UInt64) (len2 : Int64)
42  | crc32_combine_gen (len2 : Int64)
43  | crc32_combine_gen64 (len2 : Int64)
44  | crc32_combine_op (crc1 crc2 op : UInt64)
45  | crc32_z (crc : UInt64) (buf : BPtr) (len : UInt64)
46  | deflate (strm : ZStreamPtr) (flush : Int32)
47  | deflateBound (strm : ZStreamPtr) (sourceLen : UInt64)
48  | deflateBound_z (strm : ZStreamPtr) (sourceLen : UInt64)
49  | deflateCopy (dest source : ZStreamPtr)
50  | deflateEnd (strm : ZStreamPtr)
51  | deflateGetDictionary (strm : ZStreamPtr) (dictionary : BPtr) (hasDictLength : Bool)
52  | deflateInit2_ (strm : ZStreamPtr) (level method windowBits memLevel strategy : Int32) (version : BPtr) (stream_size : Int32)
53  | deflateInit_ (strm : ZStreamPtr) (level : Int32) (version : BPtr) (stream_size : Int32)
54  | deflateParams (strm : ZStreamPtr) (level strategy : Int32)
55  | deflatePending (strm : ZStreamPtr) (hasPending hasBits : Bool)
56  | deflatePrime (strm : ZStreamPtr) (bits value : Int32)
57  | deflateReset (strm : ZStreamPtr)
58  | deflateResetKeep (strm : ZStreamPtr)
59  | deflateSetDictionary (strm : ZStreamPtr) (dictionary : BPtr) (dictLength : UInt32)
60  | deflateSetHeader (strm : ZStreamPtr) (head : GzHeaderPtr)
61  | deflateTune (strm : ZStreamPtr) (good_length max_lazy nice_length max_chain : Int32)
62  | deflateUsed (strm : ZStreamPtr) (hasBits : Bool)
63  | get_crc_table
64  | gzbuffer (file : GzFilePtr) (size : UInt32)
65  | gzclearerr (file : GzFilePtr)
66  | gzclose (file : GzFilePtr)
67  | gzclose_r (file : GzFilePtr)
68  | gzclose_w (file : GzFilePtr)
69  | gzdirect (file : GzFilePtr)
70  | gzdopen (fd : Int32) (mode : BPtr)
71  | gzeof (file : GzFilePtr)
72  | gzerror (file : GzFilePtr) (errnum : BPtr)
73  | gzflush (file : GzFilePtr) (flush : Int32)
74  | gzfread (buf : BPtr) (size nitems : UInt64) (file : GzFilePtr)
75  | gzfwrite (buf : BPtr) (size nitems : UInt64) (file : GzFilePtr)
76  | gzgetc (file : GzFilePtr)
77  | gzgetc_ (file : GzFilePtr)
78  | gzgets (file : GzFilePtr) (buf : BPtr) (len : Int32)
79  | gzoffset (file : GzFilePtr)
80  | gzoffset64 (file : GzFilePtr)
81  | gzopen (path mode : BPtr)
82  | gzopen64 (path mode : BPtr)
83  | gzprintf (file : GzFilePtr) (format : BPtr) (va : List VaArg)
84  | gzputc (file : GzFilePtr) (c : Int32)
85  | gzputs (file : GzFilePtr) (str : BPtr)
86  | gzread (file : GzFilePtr) (buf : BPtr) (len : UInt32)
87  | gzrewind (file : GzFilePtr)
88  | gzseek (file : GzFilePtr) (offset : Int64) (whence : Int32)
89  | gzseek64 (file : GzFilePtr) (offset : Int64) (whence : Int32)
90  | gzsetparams (file : GzFilePtr) (level strategy : Int32)
91  | gztell (file : GzFilePtr)
92  | gztell64 (file : GzFilePtr)
93  | gzungetc (c : Int32) (file : GzFilePtr)
94  | gzvprintf (file : GzFilePtr) (format : BPtr) (va : List VaArg)
95  | gzwrite (file : GzFilePtr) (buf : BPtr) (len : UInt32)
96  | inflate (strm : ZStreamPtr) (flush : Int32)
97  | inflateBack (strm : ZStreamPtr) (inCb : InCb) (in_desc : BPtr) (outCb : OutCb) (out_desc : BPtr)
98  | inflateBackEnd (strm : ZStreamPtr)
99  | inflateBackInit_ (strm : ZStreamPtr) (windowBits : Int32) (window : BPtr) (version : BPtr) (stream_size : Int32)
100  | inflateCodesUsed (strm : ZStreamPtr)
101  | inflateCopy (dest source : ZStreamPtr)
102  | inflateEnd (strm : ZStreamPtr)
103  | inflateGetDictionary (strm : ZStreamPtr) (dictionary : BPtr) (dictLength : Option UInt32)
104  | inflateGetHeader (strm : ZStreamPtr) (head : GzHeaderPtr)
105  | inflateInit2_ (strm : ZStreamPtr) (windowBits : Int32) (version : BPtr) (stream_size : Int32)
106  | inflateInit_ (strm : ZStreamPtr) (version : BPtr) (stream_size : Int32)
107  | inflateMark (strm : ZStreamPtr)
108  | inflatePrime (strm : ZStreamPtr) (bits : Int32) (value : Int32)
109  | inflateReset (strm : ZStreamPtr)
110  | inflateReset2 (strm : ZStreamPtr) (windowBits : Int32)
111  | inflateResetKeep (strm : ZStreamPtr)
112  | inflateSetDictionary (strm : ZStreamPtr) (dictionary : BPtr) (dictLength : UInt32)
113  | inflateSync (strm : ZStreamPtr)
114  | inflateSyncPoint (strm : ZStreamPtr)
115  | inflateUndermine (strm : ZStreamPtr) (_subvert : Int32)
116  | inflateValidate (strm : ZStreamPtr) (check : Int32)
117  | uncompress (dest : BPtr) (destLen : BPtr) (source : BPtr) (sourceLen : UInt64)
118  | uncompress2 (dest : BPtr) (destLen : BPtr) (source : BPtr) (sourceLen : BPtr)
119  | uncompress2_z (dest : BPtr) (destLen : BPtr) (source : BPtr) (sourceLen : BPtr)
120  | uncompress_z (dest : BPtr) (destLen : BPtr) (source : BPtr) (sourceLen : UInt64)
121  | zError (err : Int32)
122  | zlibCompileFlags
123  | zlibVersion
124
125/-- The result type of the selected public entry. -/
126def Call.Result : Call → Type
127  | .adler32 _ _ _ => UInt64
128  | .adler32_combine _ _ _ => UInt64
129  | .adler32_combine64 _ _ _ => UInt64
130  | .adler32_z _ _ _ => UInt64
131  | .compress _ _ _ _ => (Int32 × UInt64)
132  | .compress2 _ _ _ _ _ => (Int32 × UInt64)
133  | .compress2_z _ _ _ _ _ => (Int32 × Option UInt64)
134  | .compressBound _ => UInt64
135  | .compressBound_z _ => UInt64
136  | .compress_z _ _ _ _ => (Int32 × Option UInt64)
137  | .crc32 _ _ _ => UInt64
138  | .crc32_combine _ _ _ => UInt64
139  | .crc32_combine64 _ _ _ => UInt64
140  | .crc32_combine_gen _ => UInt64
141  | .crc32_combine_gen64 _ => UInt64
142  | .crc32_combine_op _ _ _ => UInt64
143  | .crc32_z _ _ _ => UInt64
144  | .deflate _ _ => Int32
145  | .deflateBound _ _ => UInt64
146  | .deflateBound_z _ _ => UInt64
147  | .deflateCopy _ _ => Int32
148  | .deflateEnd _ => Int32
149  | .deflateGetDictionary _ _ _ => (Int32 × Option UInt32)
150  | .deflateInit2_ _ _ _ _ _ _ _ _ => Int32
151  | .deflateInit_ _ _ _ _ => Int32
152  | .deflateParams _ _ _ => Int32
153  | .deflatePending _ _ _ => (Int32 × Option UInt32 × Option Int32)
154  | .deflatePrime _ _ _ => Int32
155  | .deflateReset _ => Int32
156  | .deflateResetKeep _ => Int32
157  | .deflateSetDictionary _ _ _ => Int32
158  | .deflateSetHeader _ _ => Int32
159  | .deflateTune _ _ _ _ _ => Int32
160  | .deflateUsed _ _ => (Int32 × Option Int32)
161  | .get_crc_table => UPtr
162  | .gzbuffer _ _ => Int32
163  | .gzclearerr _ => Unit
164  | .gzclose _ => Int32
165  | .gzclose_r _ => Int32
166  | .gzclose_w _ => Int32
167  | .gzdirect _ => Int32
168  | .gzdopen _ _ => GzFilePtr
169  | .gzeof _ => Int32
170  | .gzerror _ _ => BPtr
171  | .gzflush _ _ => Int32
172  | .gzfread _ _ _ _ => UInt64
173  | .gzfwrite _ _ _ _ => UInt64
174  | .gzgetc _ => Int32
175  | .gzgetc_ _ => Int32
176  | .gzgets _ _ _ => BPtr
177  | .gzoffset _ => Int64
178  | .gzoffset64 _ => Int64
179  | .gzopen _ _ => GzFilePtr
180  | .gzopen64 _ _ => GzFilePtr
181  | .gzprintf _ _ _ => Int32
182  | .gzputc _ _ => Int32
183  | .gzputs _ _ => Int32
184  | .gzread _ _ _ => Int32
185  | .gzrewind _ => Int32
186  | .gzseek _ _ _ => Int64
187  | .gzseek64 _ _ _ => Int64
188  | .gzsetparams _ _ _ => Int32
189  | .gztell _ => Int64
190  | .gztell64 _ => Int64
191  | .gzungetc _ _ => Int32
192  | .gzvprintf _ _ _ => Int32
193  | .gzwrite _ _ _ => Int32
194  | .inflate _ _ => Int32
195  | .inflateBack _ _ _ _ _ => Int32
196  | .inflateBackEnd _ => Int32
197  | .inflateBackInit_ _ _ _ _ _ => Int32
198  | .inflateCodesUsed _ => UInt64
199  | .inflateCopy _ _ => Int32
200  | .inflateEnd _ => Int32
201  | .inflateGetDictionary _ _ _ => (Int32 × Option UInt32)
202  | .inflateGetHeader _ _ => Int32
203  | .inflateInit2_ _ _ _ _ => Int32
204  | .inflateInit_ _ _ _ => Int32
205  | .inflateMark _ => Int64
206  | .inflatePrime _ _ _ => Int32
207  | .inflateReset _ => Int32
208  | .inflateReset2 _ _ => Int32
209  | .inflateResetKeep _ => Int32
210  | .inflateSetDictionary _ _ _ => Int32
211  | .inflateSync _ => Int32
212  | .inflateSyncPoint _ => Int32
213  | .inflateUndermine _ _ => Int32
214  | .inflateValidate _ _ => Int32
215  | .uncompress _ _ _ _ => Int32
216  | .uncompress2 _ _ _ _ => Int32
217  | .uncompress2_z _ _ _ _ => Int32
218  | .uncompress_z _ _ _ _ => Int32
219  | .zError _ => BPtr
220  | .zlibCompileFlags => UInt64
221  | .zlibVersion => BPtr
222
223/-- Lift a heap computation without changing or hiding its outcome. -/
224def heapCall {α : Type} (program : C.M α) : G α := fun fs h =>
225  match program h with
226  | .error fault => .error fault
227  | .ok (value, after) => .ok ((value, fs), after)
228
229/-- Execute the actual translated entry with every argument and result preserved. -/
230def Call.execute : (call : Call) → G call.Result
231  | .adler32 adler buf len => heapCall (Zlib.Adler32.adler32 adler buf len)
232  | .adler32_combine adler1 adler2 len2 => heapCall (Zlib.Adler32.adler32_combine adler1 adler2 len2)
233  | .adler32_combine64 adler1 adler2 len2 => heapCall (Zlib.Adler32.adler32_combine64 adler1 adler2 len2)
234  | .adler32_z adler buf len => heapCall (Zlib.Adler32.adler32_z adler buf len)
235  | .compress dest destLen source sourceLen => heapCall (Zlib.Compress.compress dest destLen source sourceLen)
236  | .compress2 dest destLen source sourceLen level => heapCall (Zlib.Compress.compress2 dest destLen source sourceLen level)
237  | .compress2_z dest destLen source sourceLen level => heapCall (Zlib.Compress.compress2_z dest destLen source sourceLen level)
238  | .compressBound sourceLen => pure (Zlib.Compress.compressBound sourceLen)
239  | .compressBound_z sourceLen => pure (Zlib.Compress.compressBound_z sourceLen)
240  | .compress_z dest destLen source sourceLen => heapCall (Zlib.Compress.compress_z dest destLen source sourceLen)
241  | .crc32 crc buf len => heapCall (Zlib.Crc32.crc32 crc buf len)
242  | .crc32_combine crc1 crc2 len2 => heapCall (Zlib.Crc32.crc32_combine crc1 crc2 len2)
243  | .crc32_combine64 crc1 crc2 len2 => heapCall (Zlib.Crc32.crc32_combine64 crc1 crc2 len2)
244  | .crc32_combine_gen len2 => heapCall (Zlib.Crc32.crc32_combine_gen len2)
245  | .crc32_combine_gen64 len2 => heapCall (Zlib.Crc32.crc32_combine_gen64 len2)
246  | .crc32_combine_op crc1 crc2 op => heapCall (Zlib.Crc32.crc32_combine_op crc1 crc2 op)
247  | .crc32_z crc buf len => heapCall (Zlib.Crc32.crc32_z crc buf len)
248  | .deflate strm flush => heapCall (Zlib.Deflate.deflate strm flush)
249  | .deflateBound strm sourceLen => heapCall (Zlib.Deflate.deflateBound strm sourceLen)
250  | .deflateBound_z strm sourceLen => heapCall (Zlib.Deflate.deflateBound_z strm sourceLen)
251  | .deflateCopy dest source => heapCall (Zlib.Deflate.deflateCopy dest source)
252  | .deflateEnd strm => heapCall (Zlib.Deflate.deflateEnd strm)
253  | .deflateGetDictionary strm dictionary hasDictLength => heapCall (Zlib.Deflate.deflateGetDictionary strm dictionary hasDictLength)
254  | .deflateInit2_ strm level method windowBits memLevel strategy version stream_size => heapCall (Zlib.Deflate.deflateInit2_ strm level method windowBits memLevel strategy version stream_size)
255  | .deflateInit_ strm level version stream_size => heapCall (Zlib.Deflate.deflateInit_ strm level version stream_size)
256  | .deflateParams strm level strategy => heapCall (Zlib.Deflate.deflateParams strm level strategy)
257  | .deflatePending strm hasPending hasBits => heapCall (Zlib.Deflate.deflatePending strm hasPending hasBits)
258  | .deflatePrime strm bits value => heapCall (Zlib.Deflate.deflatePrime strm bits value)
259  | .deflateReset strm => heapCall (Zlib.Deflate.deflateReset strm)
260  | .deflateResetKeep strm => heapCall (Zlib.Deflate.deflateResetKeep strm)
261  | .deflateSetDictionary strm dictionary dictLength => heapCall (Zlib.Deflate.deflateSetDictionary strm dictionary dictLength)
262  | .deflateSetHeader strm head => heapCall (Zlib.Deflate.deflateSetHeader strm head)
263  | .deflateTune strm good_length max_lazy nice_length max_chain => heapCall (Zlib.Deflate.deflateTune strm good_length max_lazy nice_length max_chain)
264  | .deflateUsed strm hasBits => heapCall (Zlib.Deflate.deflateUsed strm hasBits)
265  | .get_crc_table => heapCall (Zlib.Crc32.get_crc_table)
266  | .gzbuffer file size => heapCall (Zlib.Gzlib.gzbuffer file size)
267  | .gzclearerr file => heapCall (Zlib.Gzlib.gzclearerr file)
268  | .gzclose file => Zlib.Gzclose.gzclose file
269  | .gzclose_r file => Zlib.Gzread.gzclose_r file
270  | .gzclose_w file => Zlib.Gzwrite.gzclose_w file
271  | .gzdirect file => Zlib.Gzread.gzdirect file
272  | .gzdopen fd mode => Zlib.Gzlib.gzdopen fd mode
273  | .gzeof file => heapCall (Zlib.Gzlib.gzeof file)
274  | .gzerror file errnum => heapCall (Zlib.Gzlib.gzerror file errnum)
275  | .gzflush file flush => Zlib.Gzwrite.gzflush file flush
276  | .gzfread buf size nitems file => Zlib.Gzread.gzfread buf size nitems file
277  | .gzfwrite buf size nitems file => Zlib.Gzwrite.gzfwrite buf size nitems file
278  | .gzgetc file => Zlib.Gzread.gzgetc file
279  | .gzgetc_ file => Zlib.Gzread.gzgetc_ file
280  | .gzgets file buf len => Zlib.Gzread.gzgets file buf len
281  | .gzoffset file => Zlib.Gzlib.gzoffset file
282  | .gzoffset64 file => Zlib.Gzlib.gzoffset64 file
283  | .gzopen path mode => Zlib.Gzlib.gzopen path mode
284  | .gzopen64 path mode => Zlib.Gzlib.gzopen64 path mode
285  | .gzprintf file format va => Zlib.Gzwrite.gzprintf file format va
286  | .gzputc file c => Zlib.Gzwrite.gzputc file c
287  | .gzputs file str => Zlib.Gzwrite.gzputs file str
288  | .gzread file buf len => Zlib.Gzread.gzread file buf len
289  | .gzrewind file => Zlib.Gzlib.gzrewind file
290  | .gzseek file offset whence => Zlib.Gzlib.gzseek file offset whence
291  | .gzseek64 file offset whence => Zlib.Gzlib.gzseek64 file offset whence
292  | .gzsetparams file level strategy => Zlib.Gzwrite.gzsetparams file level strategy
293  | .gztell file => heapCall (Zlib.Gzlib.gztell file)
294  | .gztell64 file => heapCall (Zlib.Gzlib.gztell64 file)
295  | .gzungetc c file => Zlib.Gzread.gzungetc c file
296  | .gzvprintf file format va => Zlib.Gzwrite.gzvprintf file format va
297  | .gzwrite file buf len => Zlib.Gzwrite.gzwrite file buf len
298  | .inflate strm flush => heapCall (Zlib.Inflate.inflate strm flush)
299  | .inflateBack strm inCb in_desc outCb out_desc => heapCall (Zlib.Infback.inflateBack strm inCb in_desc outCb out_desc)
300  | .inflateBackEnd strm => heapCall (Zlib.Infback.inflateBackEnd strm)
301  | .inflateBackInit_ strm windowBits window version stream_size => heapCall (Zlib.Infback.inflateBackInit_ strm windowBits window version stream_size)
302  | .inflateCodesUsed strm => heapCall (Zlib.Inflate.inflateCodesUsed strm)
303  | .inflateCopy dest source => heapCall (Zlib.Inflate.inflateCopy dest source)
304  | .inflateEnd strm => heapCall (Zlib.Inflate.inflateEnd strm)
305  | .inflateGetDictionary strm dictionary dictLength => heapCall (Zlib.Inflate.inflateGetDictionary strm dictionary dictLength)
306  | .inflateGetHeader strm head => heapCall (Zlib.Inflate.inflateGetHeader strm head)
307  | .inflateInit2_ strm windowBits version stream_size => heapCall (Zlib.Inflate.inflateInit2_ strm windowBits version stream_size)
308  | .inflateInit_ strm version stream_size => heapCall (Zlib.Inflate.inflateInit_ strm version stream_size)
309  | .inflateMark strm => heapCall (Zlib.Inflate.inflateMark strm)
310  | .inflatePrime strm bits value => heapCall (Zlib.Inflate.inflatePrime strm bits value)
311  | .inflateReset strm => heapCall (Zlib.Inflate.inflateReset strm)
312  | .inflateReset2 strm windowBits => heapCall (Zlib.Inflate.inflateReset2 strm windowBits)
313  | .inflateResetKeep strm => heapCall (Zlib.Inflate.inflateResetKeep strm)
314  | .inflateSetDictionary strm dictionary dictLength => heapCall (Zlib.Inflate.inflateSetDictionary strm dictionary dictLength)
315  | .inflateSync strm => heapCall (Zlib.Inflate.inflateSync strm)
316  | .inflateSyncPoint strm => heapCall (Zlib.Inflate.inflateSyncPoint strm)
317  | .inflateUndermine strm _subvert => heapCall (Zlib.Inflate.inflateUndermine strm _subvert)
318  | .inflateValidate strm check => heapCall (Zlib.Inflate.inflateValidate strm check)
319  | .uncompress dest destLen source sourceLen => heapCall (Zlib.Uncompr.uncompress dest destLen source sourceLen)
320  | .uncompress2 dest destLen source sourceLen => heapCall (Zlib.Uncompr.uncompress2 dest destLen source sourceLen)
321  | .uncompress2_z dest destLen source sourceLen => heapCall (Zlib.Uncompr.uncompress2_z dest destLen source sourceLen)
322  | .uncompress_z dest destLen source sourceLen => heapCall (Zlib.Uncompr.uncompress_z dest destLen source sourceLen)
323  | .zError err => heapCall (Zlib.Zutil.zError err)
324  | .zlibCompileFlags => heapCall (Zlib.Zutil.zlibCompileFlags)
325  | .zlibVersion => heapCall (Zlib.Zutil.zlibVersion)
326
327/-- A concrete total-correctness schema. Final goals must fix `pre` and `post` in
328reviewed definitions and establish their domain from init. This schema is not itself
329a completed per-function contract. Successful execution is required explicitly. -/
330def Correct (call : Call) (pre : Heap → Fs → Prop)
331    (post : Heap → Fs → call.Result → Heap → Fs → Prop) : Prop :=
332  ∀ before fs, pre before fs → ∃ value after fs',
333    call.execute fs before = .ok ((value, fs'), after) ∧
334    post before fs value after fs'
335
336end ZlibF.Spec.Public