Header.lean

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

1import ZlibF.Spec.Api.Basic
2
3/-!
4# API model: the gzip header record (`gz_header`)
5
6The part of `gz_header` that `deflateSetHeader` writes and `inflateGetHeader` reads
7(`zlib.h`), as plain data. Pointers become `Option (List UInt8)` (`none` is `Z_NULL`).
8-/
9
10namespace ZlibF.Spec.Api
11
12open ZlibF.Spec
13
14/-- `gz_header` as `deflateSetHeader` sees it: `extra`, `name`, `comment` are `none` for a null
15pointer. `name` and `comment` hold no zero byte (they are zero-terminated strings) and `extra`
16has fewer than `2^16` bytes. `xflags` is not used when writing. -/
17structure GzHead where
18  text : Bool
19  time : Nat
20  os : Nat
21  extra : Option (List UInt8)
22  name : Option (List UInt8)
23  comment : Option (List UInt8)
24  hcrc : Bool
25  deriving DecidableEq, Repr
26
27/-- The header record can be written (`deflateSetHeader` precondition of `zlib.h`). -/
28def GzHead.Valid (h : GzHead) : Prop :=
29  (∀ e, h.extra = some e → e.length < 2 ^ 16) ∧ (∀ s, h.name = some s → 0 ∉ s) ∧
30    (∀ s, h.comment = some s → 0 ∉ s)
31
32/-- The `OS_CODE` of the default x86_64 Linux build. -/
33def osCode : Nat := 3
34
35/-- The default header that `deflate` writes without `deflateSetHeader` (`deflate.c`): no flags,
36`MTIME = 0`, `OS = OS_CODE`. -/
37def GzHead.default : GzHead := ⟨false, 0, osCode, none, none, none, false⟩
38
39/-- `XFL` written by `deflate` (`deflate.c`): 2 for level 9, 4 for the fastest algorithms
40(level below 2, or Huffman only or run-length strategy), else 0. -/
41def xflOf (p : DeflParams) : Nat :=
42  if p.level = 9 then 2 else if p.strategy ≥ 2 ∨ p.level < 2 then 4 else 0
43
44/-- The flag byte `FLG` of a header record. -/
45def GzHead.flg (h : GzHead) : Nat :=
46  (if h.text then 1 else 0) + (if h.hcrc then 2 else 0) + (if h.extra.isSome then 4 else 0) +
47    (if h.name.isSome then 8 else 0) + (if h.comment.isSome then 16 else 0)
48
49/-- The header without the optional header CRC, as `Gzip.header` of the format specification. -/
50def GzHead.core (p : DeflParams) (h : GzHead) : List UInt8 :=
51  Gzip.header h.flg.toUInt8 (le32 h.time) (xflOf p).toUInt8 h.os.toUInt8
52    (h.extra.getD []) (h.name.getD []) (h.comment.getD [])
53
54/-- The bytes that `deflate` writes before the deflate data: the header and, if `hcrc`, the low
5516 bits of the CRC-32 of the header (RFC 1952). -/
56def GzHead.bytes (p : DeflParams) (h : GzHead) : List UInt8 :=
57  h.core p ++ (if h.hcrc then le16 ((crc32 (h.core p)).toNat % 2 ^ 16) else [])
58
59/-- A gzip member with the given header bytes, that decodes to `out`: the header bytes, deflate
60data, the little-endian CRC-32 and length of `out` (`Gzip.Decodes` with the header fixed). -/
61def Gzip.DecodesWith (hdr stream out : List UInt8) : Prop :=
62  ∃ s, stream = hdr ++ s ∧ Deflate.Prefix [] s (le32 (crc32 out).toNat ++ le32 (out.length % 2 ^ 32)) out
63
64/-- What `inflateGetHeader` was given: whether `extra`, `name`, `comment` have a buffer and its
65size (`extra_max`, `name_max`, `comm_max`). -/
66structure HdrReq where
67  extraMax : Option Nat
68  nameMax : Option Nat
69  commMax : Option Nat
70  deriving DecidableEq, Repr
71
72/-- The record after `inflate` has read the header (`done = 1`), or `done = -1` for a zlib
73stream. `extraLen` is `extra_len`. -/
74structure GzHdrOut where
75  text : Bool
76  time : Nat
77  xflags : Nat
78  os : Nat
79  extra : Option (List UInt8)
80  extraLen : Nat
81  name : Option (List UInt8)
82  comment : Option (List UInt8)
83  hcrc : Bool
84  done : Int
85  deriving DecidableEq, Repr
86
87/-- What `inflate` stores for a gzip header with the given fields (`A-header-fill`, `inflate.c`
88cases `HEAD` to `HCRC`): `text`, `time`, `xflags`, `os`; `extra` truncated to `extra_max` and
89`extra_len` the full length; the name and the comment including their zero terminator,
90truncated to `name_max` and `comm_max`; a field that is absent in the stream, or that has no
91buffer, is stored as `Z_NULL`; `hcrc` from the flag; `done = 1`. -/
92def fillHeader (req : HdrReq) (flg : Nat) (mtime : Nat) (xfl os : Nat)
93    (extra name comment : List UInt8) : GzHdrOut where
94  text := flg % 2 = 1
95  time := mtime
96  xflags := xfl
97  os := os
98  extra := if flg / 4 % 2 = 1 then req.extraMax.map (fun m => extra.take m) else none
99  extraLen := if flg / 4 % 2 = 1 then extra.length else 0
100  name := if flg / 8 % 2 = 1 then req.nameMax.map (fun m => (name ++ [0]).take m) else none
101  comment := if flg / 16 % 2 = 1 then req.commMax.map (fun m => (comment ++ [0]).take m) else none
102  hcrc := flg / 2 % 2 = 1
103  done := 1
104
105/-- The header record is complete in the bytes `seen`: a valid gzip header (as written by
106`Gzip.header`, with its header CRC if `FHCRC`) starts `seen`, and the record is `fillHeader` of its
107fields. Used by the inflate model; for a zlib stream `done = -1`. -/
108def HeaderRead (req : HdrReq) (seen : List UInt8) (h : GzHdrOut) : Prop :=
109  (∃ (flg : UInt8) (mtime : List UInt8) (xfl os : UInt8) (extra name comment r : List UInt8),
110    flg.toNat < 32 ∧ mtime.length = 4 ∧ extra.length < 2 ^ 16 ∧ 0 ∉ name ∧ 0 ∉ comment ∧
111    seen = Gzip.header flg mtime xfl os extra name comment ++
112        (if flg.toNat / 2 % 2 = 1 then
113          le16 ((crc32 (Gzip.header flg mtime xfl os extra name comment)).toNat % 2 ^ 16) else []) ++ r ∧
114    h = fillHeader req flg.toNat (mtime.foldr (fun b a => a * 256 + b.toNat) 0) xfl.toNat os.toNat
115          extra name comment) ∨
116  (∃ cmf flg r, seen = cmf :: flg :: r ∧ Zlib.HeaderOK cmf flg ∧ h.done = -1)
117
118end ZlibF.Spec.Api