Wrapper.lean

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

1import ZlibF.Spec.Format.Deflate
2import ZlibF.Spec.Format.Checksum
3
4/-!
5# Format: the zlib and gzip wrappers
6
7RFC 1950 and RFC 1952; the wrapper sections in `docs/spec/format/README.md`.
8Both are exact: the whole `stream` is the wrapper, there are no bytes after the trailer.
9-/
10
11namespace ZlibF.Spec
12
13/-- `F-zlib-header` (RFC 1950, 2.2): the compression method `CM = 8`, the window size field
14`CINFO <= 7`, and `(CMF * 256 + FLG) mod 31 = 0`. -/
15abbrev Zlib.HeaderOK (cmf flg : UInt8) : Prop :=
16  cmf.toNat % 16 = 8 ∧ cmf.toNat / 16 ≤ 7 ∧ (cmf.toNat * 256 + flg.toNat) % 31 = 0
17
18/-- The window size `2^(CINFO + 8)` announced by `CMF` (RFC 1950, 2.2). -/
19def Zlib.windowSize (cmf : UInt8) : Nat := 2 ^ (cmf.toNat / 16 + 8)
20
21/-- A zlib stream (RFC 1950, 2.2) that decodes to `out`, given the dictionary `dict` that the
22caller can supply (`[]` if none):
23`CMF`, `FLG`, the optional `DICTID` (the Adler-32 of the dictionary, big-endian, present iff
24`FDICT` = bit 5 of `FLG`), deflate data, and the big-endian Adler-32 of `out` (`F-zlib-check`).
25When `FDICT` is set, back-references may reach into the dictionary; zlib keeps only the last
26window-size bytes of it, so only those are used. The dictionary is ignored if `FDICT` is clear. -/
27def Zlib.Decodes (dict stream out : List UInt8) : Prop :=
28  ∃ (cmf flg : UInt8) (pre s : List UInt8),
29    stream = cmf :: flg :: (pre ++ s) ∧ Zlib.HeaderOK cmf flg ∧
30    (flg.toNat / 32 % 2 = 0 → pre = [] ∧
31      Deflate.Prefix [] s (be32 (adler32 out).toNat) out) ∧
32    (flg.toNat / 32 % 2 = 1 → pre = be32 (adler32 dict).toNat ∧
33      Deflate.Prefix (dict.drop (dict.length - Zlib.windowSize cmf)) s (be32 (adler32 out).toNat) out)
34
35/-- The gzip header of RFC 1952, 2.3, without the optional header CRC: `ID1 ID2` = 31, 139;
36`CM` = 8; `FLG`; `MTIME` (4 bytes); `XFL`; `OS`; then, in this order, if `FEXTRA` (bit 2): `XLEN`
37(2 bytes, little endian) and that many bytes; if `FNAME` (bit 3): the zero-terminated name; if
38`FCOMMENT` (bit 4): the zero-terminated comment. -/
39def Gzip.header (flg : UInt8) (mtime : List UInt8) (xfl os : UInt8)
40    (extra name comment : List UInt8) : List UInt8 :=
41  [31, 139, 8, flg] ++ mtime ++ [xfl, os] ++
42    (if flg.toNat / 4 % 2 = 1 then le16 extra.length ++ extra else []) ++
43    (if flg.toNat / 8 % 2 = 1 then name ++ [0] else []) ++
44    (if flg.toNat / 16 % 2 = 1 then comment ++ [0] else [])
45
46/-- A gzip member (RFC 1952, 2.3; format.md 4) that decodes to `out`: the header; if `FHCRC`
47(bit 1) the low 16 bits of the CRC-32 of the header bytes before it, little endian; deflate data;
48the little-endian CRC-32 of `out`; the little-endian length of `out` modulo `2^32`
49(`F-gzip-check`). zlib requires the flag bits 5 to 7 to be 0. The values `extra`, `name`,
50`comment` that belong to a flag that is clear are not used. -/
51def Gzip.Decodes (stream out : List UInt8) : Prop :=
52  ∃ (flg : UInt8) (mtime : List UInt8) (xfl os : UInt8) (extra name comment s : List UInt8),
53    flg.toNat < 32 ∧ mtime.length = 4 ∧ extra.length < 2 ^ 16 ∧ 0 ∉ name ∧ 0 ∉ comment ∧
54    stream = Gzip.header flg mtime xfl os extra name comment ++
55        (if flg.toNat / 2 % 2 = 1 then
56          le16 ((crc32 (Gzip.header flg mtime xfl os extra name comment)).toNat % 2 ^ 16) else []) ++ s ∧
57    Deflate.Prefix [] s (le32 (crc32 out).toNat ++ le32 (out.length % 2 ^ 32)) out
58
59/-- `F-deflate-valid` for the zlib layer: `compressed` is a valid zlib stream for `input`
60(given the preset dictionary `dict`, `[]` if none). -/
61def Zlib.ValidWith (dict input compressed : List UInt8) : Prop :=
62  Zlib.Decodes dict compressed input
63
64/-- `F-deflate-valid` for the zlib layer without a dictionary. This is what `deflate` has
65to produce. -/
66def Zlib.Valid (input compressed : List UInt8) : Prop :=
67  Zlib.Decodes [] compressed input
68
69/-- `F-deflate-valid` for the gzip layer. -/
70def Gzip.Valid (input compressed : List UInt8) : Prop :=
71  Gzip.Decodes compressed input
72
73end ZlibF.Spec