compress.c.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Zlib.«deflate.c»
2
3/-!
4# compress.c — faithful translation
5
6Source: `compress.c` of the verified source. `z_size_t *destLen` and `uLongf *destLen` are modelled as an input
7value (`none` is a NULL pointer) and a result (the value stored through the pointer); the runtime has no pointer to a
8scalar cell. `compress2` reads `*destLen` before any NULL test (R-2 of the notes), so a NULL `destLen` there is
9`Fault.ub`. `deflateInit(&stream, level)` is `deflateInit_(&stream, level, ZLIB_VERSION, (int)sizeof(z_stream))`.
10`z_stream stream` is an automatic record in the `streams` table. Creating it cannot fail or
11consume a default-allocator call; it is freed before the returns.
12-/
13
14namespace Zlib.Compress
15open C Zlib.Deflate
16
17/-- Pointer difference `p - q` with the model's allowance for `NULL - NULL` (D-4). -/
18def ptrDiff (p q : BPtr) : M Int64 :=
19  if p == .null && q == .null then pure 0 else Ptr.diff p q
20
21/-- Automatic storage for the local `z_stream`. As in `uncompr.c`, the runtime creates a fresh
22record without consulting or advancing the allocation-failure oracle. Only the subsequent
23`deflateInit` allocations are default-allocator calls in the C. -/
24def allocLocalZ : M ZStreamPtr := fun h =>
25  match allocZStream { h with allocOk := fun _ => true } with
26  | .ok (p, h') => .ok (p, { h' with allocOk := h.allocOk, nalloc := h.nalloc })
27  | .error e => .error e
28
29/-- `int ZEXPORT compress2_z(Bytef *dest, z_size_t *destLen, const Bytef *source, z_size_t sourceLen, int level)`;
30the result is the return value and the value stored in `*destLen` (unchanged `none` when NULL). -/
31def compress2_z (dest : BPtr) (destLen : Option UInt64) (source : BPtr) (sourceLen : UInt64) (level : Int32) :
32    M (Int32 × Option UInt64) := do
33  let max : UInt32 := 0xffffffff                       -- const uInt max = (uInt)-1;
34  -- if ((sourceLen > 0 && source == Z_NULL) || destLen == Z_NULL || (*destLen > 0 && dest == Z_NULL)) return Z_STREAM_ERROR;
35  let some dl := destLen | return (Z_STREAM_ERROR, none)
36  if (sourceLen > 0 && source == .null) || (dl > 0 && dest == .null) then return (Z_STREAM_ERROR, destLen)
37  -- left = *destLen; *destLen = 0;
38  let mut left : UInt64 := dl
39  -- z_stream stream;  stream.zalloc = 0; stream.zfree = 0; stream.opaque = 0;
40  let strm ← allocLocalZ
41  zwr strm (fun z => { z with zalloc := FnPtr.null, zfree := FnPtr.null, «opaque» := .null })
42  -- err = deflateInit(&stream, level); if (err != Z_OK) return err;
43  let ver ← Zlib.Zutil.zlibVersion
44  let mut err ← deflateInit_ strm level ver sizeof_z_stream
45  if err != Z_OK then
46    freeZStream strm
47    return (err, some 0)
48  -- stream.next_out = dest; stream.avail_out = 0; stream.next_in = source; stream.avail_in = 0;
49  zwr strm (fun z => { z with next_out := dest, avail_out := 0, next_in := source, avail_in := 0 })
50  let mut sourceLen := sourceLen
51  -- do { ... } while (err == Z_OK);
52  let (e, l, sl) ← cdoWhile
53    (fun ((_, left, sourceLen) : Int32 × UInt64 × UInt64) => do
54      let mut left := left
55      let mut sourceLen := sourceLen
56      -- if (stream.avail_out == 0) { stream.avail_out = left > (z_size_t)max ? max : (uInt)left; left -= stream.avail_out; }
57      if (← zrd strm (·.avail_out)) == 0 then
58        let ao : UInt32 := if left > max.toUInt64 then max else left.toUInt32
59        zwr strm (fun z => { z with avail_out := ao })
60        left := left - ao.toUInt64
61      -- if (stream.avail_in == 0) { stream.avail_in = sourceLen > (z_size_t)max ? max : (uInt)sourceLen; sourceLen -= stream.avail_in; }
62      if (← zrd strm (·.avail_in)) == 0 then
63        let ai : UInt32 := if sourceLen > max.toUInt64 then max else sourceLen.toUInt32
64        zwr strm (fun z => { z with avail_in := ai })
65        sourceLen := sourceLen - ai.toUInt64
66      -- err = deflate(&stream, sourceLen ? Z_NO_FLUSH : Z_FINISH);
67      let err ← deflate strm (if sourceLen != 0 then Z_NO_FLUSH else Z_FINISH)
68      pure (err, left, sourceLen))
69    (fun (st : Int32 × UInt64 × UInt64) => pure (st.1 == Z_OK, st))
70    (err, left, sourceLen)
71  err := e
72  left := l
73  sourceLen := sl
74  -- *destLen = (z_size_t)(stream.next_out - dest);
75  let no ← zrd strm (·.next_out)
76  let n ← ptrDiff no dest
77  -- deflateEnd(&stream);
78  let _ ← deflateEnd strm
79  freeZStream strm
80  -- return err == Z_STREAM_END ? Z_OK : err;
81  return (if err == Z_STREAM_END then Z_OK else err, some n.toUInt64)
82
83/-- `int ZEXPORT compress2(Bytef *dest, uLongf *destLen, const Bytef *source, uLong sourceLen, int level)`;
84`destLen` is the value of `*destLen`, `none` for NULL (undefined: `*destLen` is read first). -/
85def compress2 (dest : BPtr) (destLen : Option UInt64) (source : BPtr) (sourceLen : UInt64) (level : Int32) :
86    M (Int32 × UInt64) := do
87  -- z_size_t got = *destLen;
88  let some got := destLen | ub "null dereference of destLen"
89  -- ret = compress2_z(dest, &got, source, sourceLen, level);
90  let (ret, g) ← compress2_z dest (some got) source sourceLen level
91  -- *destLen = (uLong)got;
92  return (ret, g.getD got)
93
94/-- `int ZEXPORT compress_z(Bytef *dest, z_size_t *destLen, const Bytef *source, z_size_t sourceLen)` -/
95def compress_z (dest : BPtr) (destLen : Option UInt64) (source : BPtr) (sourceLen : UInt64) :
96    M (Int32 × Option UInt64) :=
97  compress2_z dest destLen source sourceLen Z_DEFAULT_COMPRESSION
98
99/-- `int ZEXPORT compress(Bytef *dest, uLongf *destLen, const Bytef *source, uLong sourceLen)` -/
100def compress (dest : BPtr) (destLen : Option UInt64) (source : BPtr) (sourceLen : UInt64) :
101    M (Int32 × UInt64) :=
102  compress2 dest destLen source sourceLen Z_DEFAULT_COMPRESSION
103
104/-- `z_size_t ZEXPORT compressBound_z(z_size_t sourceLen)` -/
105def compressBound_z (sourceLen : UInt64) : UInt64 :=
106  let bound := sourceLen + (sourceLen >>> 12) + (sourceLen >>> 14) + (sourceLen >>> 25) + 13
107  if bound < sourceLen then 0xffffffffffffffff else bound
108
109/-- `uLong ZEXPORT compressBound(uLong sourceLen)` -/
110def compressBound (sourceLen : UInt64) : UInt64 :=
111  -- (uLong)bound != bound is always false: both are 64 bits
112  compressBound_z sourceLen
113
114end Zlib.Compress