Compress.lean

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

1import ZlibF.Spec.Api.Deflate
2
3/-!
4# API model: `compress`, `compress2`, `compressBound`, `uncompress`, `uncompress2`
5
6The one-call utility functions of `compress.c` and `uncompr.c`, as relations between the source
7bytes, the room in the destination, and the result. The data-only core records the bytes written.
8`Compress2Z` separately records null checks, the stored length and the compatibility wrapper.
9On an argument error, the stored length can remain the initial capacity although no bytes were written.
10-/
11
12namespace ZlibF.Spec.Api
13
14open ZlibF.Spec
15
16/-- `compressBound(sourceLen)` (`compress.c`): `n + (n >> 12) + (n >> 14) + (n >> 25) + 13`,
17`2^64 - 1` on overflow (`uLong` is 64 bits). -/
18def compressBound (n : Nat) : Nat :=
19  let b := n + n / 2 ^ 12 + n / 2 ^ 14 + n / 2 ^ 25 + 13
20  if b ≥ 2 ^ 64 then 2 ^ 64 - 1 else b
21
22/-- The parameters that `compress2` gives `deflateInit`: zlib wrapper, 15 window bits,
23`memLevel` 8, default strategy. -/
24def compressParams (level : Int) : Option DeflParams :=
25  deflInit? level 8 15 8 0
26
27/-- `compress2(dest, &destLen, source, sourceLen, level)`: `cap` is `*destLen` on entry; the result
28is the return code and the bytes written. `argsOK` is a coarse rejection flag
29(`Z_STREAM_ERROR`). It does not describe all pointer shapes or the stored length; those are in
30`Compress2Z` and `Compress2Wrapper`. `Z_MEM_ERROR` is an allocation failure.
31
32* `Z_OK`: `dst` is a valid zlib stream of `src` of at most `cap` bytes.
33* `Z_BUF_ERROR`: the room was used up (`|dst| = cap`) and was smaller than `compressBound`.
34* `Z_STREAM_ERROR` (bad `level`, or null arguments) and `Z_MEM_ERROR`: nothing was written.
35* In every case `|dst|` is at most `compressBound |src|` and, for `Z_OK`, a valid stream. -/
36def Compress2 (argsOK : Bool) (level : Int) (src : List UInt8) (cap : Nat) (rc : Int)
37    (dst : List UInt8) : Prop :=
38  if argsOK = false then rc = Z.streamError ∧ dst = []
39  else match compressParams level with
40    | none => rc = Z.streamError ∧ dst = []
41    | some p =>
42      (rc = Z.memError ∧ dst = []) ∨
43      (rc = Z.ok ∧ (DeflState.fresh p).Valid dst src ∧ dst.length ≤ cap ∧
44        dst.length ≤ compressBound src.length) ∨
45      (rc = Z.bufError ∧ dst.length = cap ∧ cap < compressBound src.length ∧
46        ∃ out, (DeflState.fresh p).Valid out src ∧ dst <+: out)
47
48/-- Pointer shape and input values at the `compress2_z` boundary. The source bytes are meaningful
49only when the source is readable; a null source is valid exactly for an empty source. `capacity`
50is the initial scalar value and is not read when `lengthNull` is true. Heap bounds, aliasing and
51representable sizes belong to the concrete argument relation. -/
52structure CompressCall where
53  source : List UInt8
54  capacity : Nat
55  level : Int
56  sourceNull : Bool
57  destNull : Bool
58  lengthNull : Bool
59
60/-- Data returned by a compressor call. `storedLength` is the scalar value after the call, not
61the number of bytes written on all error paths: argument rejection preserves the original
62capacity. A missing scalar pointer is represented by `none`. -/
63structure CompressResult where
64  rc : Int
65  produced : List UInt8
66  storedLength : Option Nat
67
68/-- The argument rejection that occurs before `*destLen = 0` or initialisation. A null
69destination with zero capacity passes these checks and is refused by the inner `deflate`. -/
70def CompressCall.rejected (c : CompressCall) : Prop :=
71  (c.sourceNull = true ∧ c.source ≠ []) ∨ c.lengthNull = true ∨
72    (c.destNull = true ∧ 0 < c.capacity)
73
74instance (c : CompressCall) : Decidable c.rejected := by
75  unfold CompressCall.rejected
76  infer_instance
77
78/-- `int compress2_z(Bytef *dest, z_size_t *destLen, const Bytef *source, z_size_t sourceLen, int level)`.
79The default LP64 entry-point contract, with null checks and error ordering. Argument rejection
80leaves the scalar unchanged. A bad level is rejected before allocator failure can occur. A null
81destination with zero capacity reaches initialisation: it can report `Z_MEM_ERROR`, otherwise
82`Z_STREAM_ERROR`, and writes no bytes. With valid pointers, the data-only core `Compress2`
83applies and the scalar is exactly the number of bytes written. No clause assumes a callee
84contract; proving this relation for the concrete execution is a separate refinement theorem. -/
85def Compress2Z (c : CompressCall) (r : CompressResult) : Prop :=
86  if c.rejected then
87    r.rc = Z.streamError ∧ r.produced = [] ∧
88      r.storedLength = (if c.lengthNull then none else some c.capacity)
89  else match compressParams c.level with
90    | none => r.rc = Z.streamError ∧ r.produced = [] ∧ r.storedLength = some 0
91    | some _ =>
92      if c.destNull then
93        (r.rc = Z.memError ∨ r.rc = Z.streamError) ∧ r.produced = [] ∧
94          r.storedLength = some 0
95      else Compress2 true c.level c.source c.capacity r.rc r.produced ∧
96        r.storedLength = some r.produced.length
97
98/-- `int compress2(Bytef *dest, uLongf *destLen, const Bytef *source, uLong sourceLen, int level)`.
99The wrapper reads the scalar before the `_z` checks. Its defined-execution domain therefore
100requires a nonnull readable and writable scalar pointer; `lengthNull = true` is a fault, not
101a clean `Z_STREAM_ERROR`. The concrete execution definition preserves that fault. -/
102def Compress2Wrapper (c : CompressCall) (r : CompressResult) : Prop :=
103  c.lengthNull = false ∧ Compress2Z c r
104
105/-- `compress(dest, &destLen, source, sourceLen)`: `compress2` with `Z_DEFAULT_COMPRESSION`. -/
106def Compress (argsOK : Bool) (src : List UInt8) (cap : Nat) (rc : Int) (dst : List UInt8) : Prop :=
107  Compress2 argsOK (-1) src cap rc dst
108
109/-- `uncompress2(dest, &destLen, source, &sourceLen)`: `cap` is `*destLen`, `used` the new
110`*sourceLen`. The stream is zlib, with a 15-bit window and no dictionary.
111
112* `Z_OK`: the first `used` bytes of `src` are a complete zlib stream that decodes to `dst`,
113  which fits in `cap`.
114* `Z_BUF_ERROR`: `dst` filled the room and unused source bytes remain. This does not require
115  unused trailing bytes to extend a valid stream.
116* `Z_DATA_ERROR`: the input is corrupt or an incomplete stream, or it asks for a dictionary
117  (`Z_NEED_DICT` becomes `Z_DATA_ERROR`).
118* `Z_STREAM_ERROR` (null arguments, `argsOK` false): nothing was written.
119* `Z_MEM_ERROR` can follow partial output. Concrete contracts distinguish initialisation
120  failure, which preserves the length cells, from a later failure, which stores actual counts.
121* Output is bounded by `cap`; consumption is bounded by the available source.
122
123Liveness: a source that begins with a complete stream (that needs no dictionary) whose decoding
124fits in `cap` gives `Z_OK` and that decoding, unless memory fails; if the decoding does not fit,
125the result is `Z_BUF_ERROR` or `Z_MEM_ERROR`. Every compatible complete prefix determines the
126output, including output before a memory failure. -/
127def Uncompress2 (argsOK : Bool) (src : List UInt8) (cap : Nat) (rc : Int) (dst : List UInt8)
128    (used : Nat) : Prop :=
129  if argsOK = false then rc = Z.streamError ∧ dst = [] ∧ used = 0
130  else
131    used ≤ src.length ∧ dst.length ≤ cap ∧
132    (rc = Z.ok ∨ rc = Z.bufError ∨ rc = Z.dataError ∨ rc = Z.memError) ∧
133    (rc = Z.ok → Zlib.Decodes [] (src.take used) dst) ∧
134    (rc = Z.bufError → dst.length = cap ∧ used < src.length) ∧
135    Layer.Determined .zlib 15 [] (src.take used) dst ∧
136    Layer.OutputEvidence .zlib 15 (fun dictionary => dictionary = []) (src.take used) dst ∧
137    (∀ n o, n ≤ src.length → Zlib.Decodes [] (src.take n) o →
138      dst <+: o ∧ (¬ HdrNeedsDict .zlib 15 (src.take n) →
139        (o.length ≤ cap → rc = Z.ok ∨ rc = Z.memError) ∧
140        (cap < o.length → rc = Z.bufError ∨ rc = Z.memError)))
141
142/-- `uncompress(dest, &destLen, source, sourceLen)`: `uncompress2` without the count of used
143source bytes. -/
144def Uncompress (argsOK : Bool) (src : List UInt8) (cap : Nat) (rc : Int) (dst : List UInt8) : Prop :=
145  ∃ used, Uncompress2 argsOK src cap rc dst used
146
147end ZlibF.Spec.Api