Basic.lean

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

1import ZlibF.Spec.Format
2
3/-!
4# API model: vocabulary
5
6Heap-free vocabulary for the model of the public API (`docs/design/api-model.md`): the return codes
7and flush values of `zlib.h`, the parameter checks of the `*Init2`/`*Reset2` functions (computable,
8copied from `deflate.c` and `inflate.c`), and the decoding oracle `Layer.Decodes` that the inflate
9model uses. Nothing here mentions a heap or a pointer.
10-/
11
12namespace ZlibF.Spec.Api
13
14open ZlibF.Spec
15
16/-! ## Return codes and flush values (`zlib.h`) -/
17
18-- The return codes of `zlib.h`.
19namespace Z
20def ok : Int := 0
21def streamEnd : Int := 1
22def needDict : Int := 2
23def errno : Int := -1
24def streamError : Int := -2
25def dataError : Int := -3
26def memError : Int := -4
27def bufError : Int := -5
28def versionError : Int := -6
29end Z
30
31/-- The flush values of `zlib.h` (`Z_NO_FLUSH` .. `Z_TREES`); `partialFlush` is deflate only,
32`trees` is inflate only. -/
33inductive Flush where
34  | noFlush | partialFlush | syncFlush | fullFlush | finish | block | trees
35  deriving DecidableEq, Repr
36
37/-- The integer value of a flush constant. -/
38def Flush.code : Flush → Int
39  | .noFlush => 0 | .partialFlush => 1 | .syncFlush => 2 | .fullFlush => 3
40  | .finish => 4 | .block => 5 | .trees => 6
41
42/-- `RANK` of `deflate.c`: the order used to refuse a repeated, useless flush. -/
43def Flush.rank (f : Int) : Int := f * 2 - (if f > 4 then 9 else 0)
44
45/-! ## Layers and window bits -/
46
47/-- The wrapper an inflate stream expects: raw deflate (`windowBits < 0`), zlib, gzip, or
48automatic detection of zlib or gzip (`windowBits >= 32`). -/
49inductive Wrap where
50  | raw | zlib | gzip | auto
51  deriving DecidableEq, Repr
52
53/-- `inflateInit2` / `inflateReset2` (inflate.c): the wrapper and the window bits (`0` means
54"take it from the zlib header") selected by `windowBits`, or `none` for `Z_STREAM_ERROR`.
55A gzip header with `windowBits = 0` uses 15 at run time, see `winBits`. -/
56def inflWbits (w : Int) : Option (Wrap × Nat) :=
57  if w < 0 then
58    if w < -15 then none
59    else if -w < 8 then none
60    else some (.raw, (-w).toNat)
61  else
62    let wrap : Option Wrap :=
63      if w / 16 = 0 then some .zlib else if w / 16 = 1 then some .gzip
64      else if w / 16 = 2 then some .auto else none
65    let wb : Int := if w < 48 then w % 16 else w
66    match wrap with
67    | none => none
68    | some wr => if wb ≠ 0 ∧ (wb < 8 ∨ wb > 15) then none else some (wr, wb.toNat)
69
70/-- The wrapper of a deflate stream. -/
71inductive DWrap where
72  | raw | zlib | gzip
73  deriving DecidableEq, Repr
74
75/-- The parameters fixed by `deflateInit2`; `level` is already `6` for `Z_DEFAULT_COMPRESSION`
76and `wbits` is already `9` for `windowBits = 8` (zlib wrapper). -/
77structure DeflParams where
78  level : Nat
79  wrap : DWrap
80  wbits : Nat
81  memLevel : Nat
82  strategy : Nat
83  deriving DecidableEq, Repr
84
85/-- `deflateInit2_` (deflate.c) without the version and allocation checks: the parameters, or `none`
86for `Z_STREAM_ERROR`. `method` must be `Z_DEFLATED = 8`. -/
87def deflInit? (level method wbits memLevel strategy : Int) : Option DeflParams :=
88  let level' : Int := if level = -1 then 6 else level
89  let wrapWb : Option (DWrap × Int) :=
90    if wbits < 0 then (if wbits < -15 then none else some (.raw, -wbits))
91    else if wbits > 15 then some (.gzip, wbits - 16) else some (.zlib, wbits)
92  match wrapWb with
93  | none => none
94  | some (wr, wb) =>
95    if memLevel < 1 ∨ memLevel > 9 ∨ method ≠ 8 ∨ wb < 8 ∨ wb > 15 ∨ level' < 0 ∨ level' > 9 ∨
96        strategy < 0 ∨ strategy > 4 ∨ (wb = 8 ∧ wr ≠ .zlib) then none
97    else some ⟨level'.toNat, wr, (if wb = 8 then 9 else wb).toNat, memLevel.toNat, strategy.toNat⟩
98
99/-- The input wrapper selected by the deflate wrapper. -/
100def DWrap.toWrap : DWrap → Wrap
101  | .raw => .raw | .zlib => .zlib | .gzip => .gzip
102
103/-! ## The decoding oracle -/
104
105/-- The window announced by a zlib header fits the window of the stream (`windowBits = 0`: any). -/
106def ZlibFits (wbits : Nat) (s : List UInt8) : Prop :=
107  wbits = 0 ∨ ∃ c, s.head? = some c ∧ c.toNat / 16 + 8 ≤ wbits
108
109/-- `Layer.Decodes w wbits dict s o`: `s` is exactly one complete stream of layer `w` (with
110configured window bits `wbits`) that decodes to `o` when the preset dictionary is `dict`.
111This is the format specification, selected by the configuration. For raw streams only the last
112`2^wbits` bytes of the dictionary are reachable.
113Distances larger than the window are the one place where the format specification is
114more permissive than zlib; see `FullWindow`. -/
115def Layer.Decodes (w : Wrap) (wbits : Nat) (dict s o : List UInt8) : Prop :=
116  match w with
117  | .raw => Deflate.Decodes (dict.drop (dict.length - 2 ^ wbits)) s o
118  | .zlib => Zlib.Decodes dict s o ∧ ZlibFits wbits s
119  | .gzip => Gzip.Decodes s o
120  | .auto => (Zlib.Decodes dict s o ∧ ZlibFits wbits s) ∨ Gzip.Decodes s o
121
122/-- The configurations in which zlib accepts every stream that the format specification accepts:
123the window is 32 KiB, which is the largest distance. This is `windowBits` 15 for every layer, and
124`windowBits` 0 when the window is taken from the header (zlib: it must announce 15; gzip: zlib uses
12515; auto: either). For a smaller window zlib may answer `Z_DATA_ERROR` for a valid stream with a
126distance larger than the window (the check counts only the window and the output of the current
127call, so it depends on how the caller splits the output; checked against the real library:
128a gzip stream with `windowBits` 16 + 8 to 13 and an output room of 100 bytes per call fails); the
129model then promises only "correct output or `Z_DATA_ERROR`". An empty prefix is full. -/
130def FullWindow (w : Wrap) (wbits : Nat) (s : List UInt8) : Prop :=
131  match w with
132  | .raw => wbits = 15
133  | .gzip => wbits = 0 ∨ wbits = 15
134  | .zlib => wbits = 15 ∨ (wbits = 0 ∧ ∀ c, s.head? = some c → c.toNat / 16 + 8 = 15)
135  | .auto => wbits = 15 ∨ (wbits = 0 ∧ (s.head? = some 31 ∨ ∀ c, s.head? = some c → c.toNat / 16 + 8 = 15))
136
137/-- Legacy abstract detection parameter. Eight is refuted by a dynamic-table counterexample:
138an impossible prefix of 230 bytes can be followed by a call that consumes 281 and returns OK.
139This is not an established bound for actual inflate. A replacement requires a separate
140source and format argument; the abstract rejection theorem alone cannot validate it. -/
141def detectLag : Nat := 8
142
143/-- The length of header that zlib needs before it can reject a stream: 2 bytes for a zlib header,
1444 for a gzip header (magic, method and flags), none for raw deflate; 4 when the layer is detected. -/
145def hdrLag : Wrap → Nat
146  | .raw => 0 | .zlib => 2 | .gzip => 4 | .auto => 4
147
148/-- `Viable`: `x` is the beginning of a stream that zlib has to accept: some stream of layer `w`
149(possibly followed by other bytes) starts with `x`, or ends inside `x`. The first `hdrLag` bytes
150are never rejected. -/
151def Layer.Viable (w : Wrap) (wbits : Nat) (dict x : List UInt8) : Prop :=
152  x.length < hdrLag w ∨ ∃ (t o : List UInt8) (n : Nat), Layer.Decodes w wbits dict ((x ++ t).take n) o
153
154/-- `Detectable`: `x` has a prefix that is not viable and is at least `detectLag` bytes shorter
155than `x`; a decoder that sees all of `x` and has room must answer `Z_DATA_ERROR`. -/
156def Layer.Detectable (w : Wrap) (wbits : Nat) (dict x : List UInt8) : Prop :=
157  ∃ m, m + detectLag ≤ x.length ∧ ¬ Layer.Viable w wbits dict (x.take m)
158
159/-- The zlib header at the start of `x` asks for a dictionary (`FDICT`, bit 5 of `FLG`) and fits
160the window; zlib then returns `Z_NEED_DICT` after reading the 6 bytes of header and `DICTID`. -/
161def HdrNeedsDict (w : Wrap) (wbits : Nat) (x : List UInt8) : Prop :=
162  (w = .zlib ∨ w = .auto) ∧ ∃ cmf flg r, x = cmf :: flg :: r ∧ Zlib.HeaderOK cmf flg ∧
163    flg.toNat / 32 % 2 = 1 ∧ ZlibFits wbits x
164
165end ZlibF.Spec.Api