Examples.lean

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

1import ZlibF.Spec.Format.Wrapper
2
3/-!
4# Format: sanity examples
5
6These `example`s are the tests of the specification (there is no other check that the
7definitions say what the RFCs say). Every rule of `docs/spec/format/README.md` has a positive
8and a negative example. Facts about a definition are proved by `decide` (kernel
9evaluation, no extra axiom); a derivation of a relation is built from its constructors, with
10`rfl` filling in the symbols and the bits that are left. All evaluation is kernel checked.
11
12Byte lists were produced by zlib itself (raw deflate, `Z_FIXED`), except the dynamic block
13and the invalid streams, which were written by hand and checked against zlib.
14-/
15
16namespace ZlibF.Spec
17
18set_option maxRecDepth 100000
19
20/-- Kernel evaluation of a decidable proposition. -/
21local macro "dk" : term => `(by decide +kernel)
22
23/-- Evaluate a reader hypothesis `readBits .. = some (..)` or `decodeSym .. = some (..)` of a
24concrete input, and split the equation. Used to invert derivations in the negative examples. -/
25local macro "ev " h:ident : tactic =>
26  `(tactic| (change some (_, _) = some (_, _) at $h:ident
27             simp only [Option.some.injEq, Prod.mk.injEq] at $h:ident))
28
29/-! ## Checksums (`F-adler-incremental`, `F-crc-incremental`) -/
30
31/-- "Wikipedia" (RFC 1950 example, Wikipedia article). -/
32example : adler32 [0x57, 0x69, 0x6B, 0x69, 0x70, 0x65, 0x64, 0x69, 0x61] = 0x11E60398 := by decide
33example : adler32 [] = 1 := by decide
34/-- "123456789", the standard CRC-32 check value. -/
35example : crc32 [0x31, 0x32, 0x33, 0x34, 0x35, 0x36, 0x37, 0x38, 0x39] = 0xCBF43926 := by decide
36example : crc32 [] = 0 := by decide
37/-- Incremental: "1234" then "56789". -/
38example : crc32Update (crc32 [0x31, 0x32, 0x33, 0x34]) [0x35, 0x36, 0x37, 0x38, 0x39] = 0xCBF43926 := by
39  decide
40example : adler32Update (adler32 [0x57, 0x69, 0x6B, 0x69]) [0x70, 0x65, 0x64, 0x69, 0x61] = 0x11E60398 := by
41  decide
42/-- Negative: a different input gives a different value. -/
43example : adler32 [0x57, 0x69, 0x6B, 0x69, 0x70, 0x65, 0x64, 0x69, 0x62] ≠ 0x11E60398 := by decide
44example : crc32 [0x31, 0x32, 0x33, 0x34, 0x35, 0x36, 0x37, 0x38, 0x38] ≠ 0xCBF43926 := by decide
45
46/-! ## Bit order (`F-bit-order`) -/
47
48/-- Data in least significant bit first: 0x05 = 1,0,1,0,0,0,0,0. -/
49example : byteBits 0x05 = [true, false, true, false, false, false, false, false] := by decide
50/-- A number is read least significant bit first: bits 1,0,1 are 5. -/
51example : readBits 3 [true, false, true, false] = some (5, [false]) := by decide
52/-- A Huffman code is written most significant bit first: 5 in 4 bits is 0,1,0,1. -/
53example : natToBitsMSB 4 5 = [false, true, false, true] := by decide
54/-- Negative: too few bits. -/
55example : readBits 3 [true, false] = none := by decide
56
57/-! ## Canonical codes (`F-code-fits`, `F-code-complete`, `F-fixed-lengths`) -/
58
59/-- The example of RFC 1951, 3.2.2: lengths (3,3,3,3,3,2,4,4) for A..H give
60F=00, A=010, B=011, C=100, D=101, E=110, G=1110, H=1111. -/
61example : (List.range 8).map (codeOf [3, 3, 3, 3, 3, 2, 4, 4]) =
62    [[false, true, false], [false, true, true], [true, false, false], [true, false, true],
63     [true, true, false], [false, false], [true, true, true, false], [true, true, true, true]] := by
64  decide
65example : Fits [3, 3, 3, 3, 3, 2, 4, 4] ∧ Complete [3, 3, 3, 3, 3, 2, 4, 4] := by decide
66/-- The fixed codes (RFC 1951, 3.2.6): symbol 0 is 00110000, 143 is 10111111, 144 is
67110010000, 256 is 0000000 (7 bits), 280 is 11000000; distance 3 is 00011. -/
68example : codeOf fixedLitLens 0 = natToBitsMSB 8 0x30 := by decide
69example : codeOf fixedLitLens 143 = natToBitsMSB 8 0xBF := by decide
70example : codeOf fixedLitLens 144 = natToBitsMSB 9 0x190 := by decide
71example : codeOf fixedLitLens 256 = natToBitsMSB 7 0 := by decide
72example : codeOf fixedLitLens 280 = natToBitsMSB 8 0xC0 := by decide
73example : codeOf fixedDistLens 3 = natToBitsMSB 5 3 := by decide
74example : Acceptable .litLen fixedLitLens ∧ Complete fixedLitLens := by decide
75example : Acceptable .dist fixedDistLens ∧ Complete fixedDistLens := by decide
76example : fixedLitLens.length = 288 ∧ fixedDistLens.length = 32 := by decide
77/-- Negative (`F-fixed-lengths`): the fixed literal code is not the all-8 code. -/
78example : codeOf fixedLitLens 256 ≠ natToBitsMSB 8 0 := by decide
79/-- Negative (`F-code-fits`): an over-subscribed set (three codes of length 1). -/
80example : ¬ Fits [1, 1, 1] := by decide
81example : ¬ Acceptable .litLen [1, 1, 1] := by decide
82/-- Negative (`F-code-fits`): over-subscribed at a longer length (1/2 + 1/4 + 1/4 + 1/8 > 1). -/
83example : ¬ Acceptable .dist [1, 2, 2, 3] := by decide
84/-- Negative (`F-code-complete`): an incomplete set with two symbols is rejected. -/
85example : ¬ Acceptable .litLen [2, 2] := by decide
86example : ¬ Acceptable .dist [2, 2, 0, 0] := by decide
87/-- Negative: a length above 15 is rejected. -/
88example : ¬ Acceptable .litLen [16, 16] := by decide
89/-- The single-symbol exception (format.md 2.4): one symbol of length 1 is accepted for the
90literal/length and distance codes, but not for the code-length code. -/
91example : Acceptable .dist [0, 1] ∧ Acceptable .litLen [1] := by decide
92example : ¬ Acceptable .codeLength [0, 1] := by decide
93/-- Negative: a single symbol of length 2 is not the exception. -/
94example : ¬ Acceptable .dist [0, 2] := by decide
95/-- No symbol at all is accepted (format.md 2.4); every decode attempt then fails. -/
96example : Acceptable .dist [0, 0, 0] := by decide
97example : decodeSym [0, 0, 0] [true, false] = none := by decide
98/-- Decoding by prefix: with lengths (1,2,2), "1" then "0 1" then "0 0". -/
99example : decodeSym [1, 2, 2] [true, false, true] = some (1, [true]) := by decide
100example : decodeSym [1, 2, 2] [false, false] = some (0, [false]) := by decide
101/-- Negative: with one symbol of length 1 (code "0"), the bit "1" is not a code. -/
102example : decodeSym [0, 1] [true] = none := by decide
103/-- `F-dynamic-eob`: symbol 256 must have a length. -/
104example : HasEndOfBlock (List.replicate 256 0 ++ [1]) := by decide
105example : ¬ HasEndOfBlock (List.replicate 256 0) := by decide
106example : ¬ HasEndOfBlock (List.replicate 256 0 ++ [0, 1]) := by decide
107/-- `F-dynamic-limits`: at most 286 literal/length and 30 distance codes. -/
108example : DynamicCountsOK 29 29 := by decide
109example : ¬ DynamicCountsOK 30 0 := by decide
110example : ¬ DynamicCountsOK 0 30 := by decide
111
112/-! ## Tables (`F-length-table`, `F-distance-table`) -/
113
114example : lengthBases.length = 29 ∧ lengthExtras.length = 29 := by decide
115example : distBases.length = 30 ∧ distExtras.length = 30 := by decide
116/-- Each distance row starts where the previous one ends, and the last one ends at 32768. -/
117example : (List.range 29).all (fun i => distBases.getD i 0 + 2 ^ distExtras.getD i 0 == distBases.getD (i + 1) 0)
118    = true := by decide
119example : distBases.getD 29 0 + 2 ^ distExtras.getD 29 0 - 1 = 32768 := by decide
120/-- The same for lengths 3..257 (symbols 257..284). Symbol 285 is the single length 258. -/
121example : (List.range 27).all (fun i => lengthBases.getD i 0 + 2 ^ lengthExtras.getD i 0 == lengthBases.getD (i + 1) 0)
122    = true := by decide
123example : lengthBases.getD 28 0 = 258 ∧ lengthExtras.getD 28 0 = 0 := by decide
124/-- Negative: distance 5 is not in the first row, it is symbol 4 with 0 extra bits. -/
125example : distBases.getD 4 0 = 5 ∧ distExtras.getD 4 0 = 1 := by decide
126
127/-! ## Copying (`F-match-copy`) -/
128
129/-- Distance 1 repeats one byte. -/
130example : copyBack [] 1 4 [0x61] = [0x61, 0x61, 0x61, 0x61, 0x61] := by decide
131/-- Overlap: distance 2, length 5 over "ab" gives "abababa". -/
132example : copyBack [] 2 5 [0x61, 0x62] = [0x61, 0x62, 0x61, 0x62, 0x61, 0x62, 0x61] := by decide
133/-- The dictionary is before the output. -/
134example : copyBack [0x61, 0x62] 2 3 [] = [0x61, 0x62, 0x61] := by decide
135
136/-! ## Deflate: stored blocks (`F-stored-complement`, `F-block-type-3`) -/
137
138/-- A final stored block "abc": header byte 0x01, LEN = 3, NLEN = 0xFFFC. -/
139example : Deflate.Decodes [] [0x01, 0x03, 0x00, 0xFC, 0xFF, 0x61, 0x62, 0x63] [0x61, 0x62, 0x63] :=
140  ⟨_, .last rfl rfl (.stored rfl rfl rfl rfl), dk⟩
141/-- An empty stored block. -/
142example : Deflate.Decodes [] [0x01, 0x00, 0x00, 0xFF, 0xFF] [] :=
143  ⟨_, .last rfl rfl (.stored rfl rfl rfl rfl), dk⟩
144/-- The padding bits after the 3 header bits are skipped, whatever they are (here 1s). -/
145example : Deflate.Decodes [] [0xF9, 0x01, 0x00, 0xFE, 0xFF, 0x61] [0x61] :=
146  ⟨_, .last rfl rfl (.stored rfl rfl rfl rfl), dk⟩
147/-- Negative (`F-stored-complement`): `NLEN` is not the complement of `LEN`. -/
148example : ∀ out, ¬ Deflate.Decodes [] [0x01, 0x03, 0x00, 0xFC, 0xFE, 0x61, 0x62, 0x63] out := by
149  rintro out ⟨rest, hb, -⟩
150  cases hb with
151  | more h1 => ev h1; exact absurd h1.1 (by decide)
152  | last h1 h2 hbody =>
153    ev h1; obtain ⟨-, rfl⟩ := h1
154    ev h2; obtain ⟨rfl, rfl⟩ := h2
155    cases hbody with
156    | stored a b c d =>
157      ev a; obtain ⟨rfl, rfl⟩ := a
158      ev b; obtain ⟨rfl, rfl⟩ := b
159      exact absurd c (by decide)
160/-- Negative (`F-block-type-3`): `BTYPE = 3` has no meaning. -/
161example : ∀ out, ¬ Deflate.Decodes [] [0x07, 0x00, 0x00] out := by
162  rintro out ⟨rest, hb, -⟩
163  cases hb with
164  | more h1 => ev h1; exact absurd h1.1 (by decide)
165  | last h1 h2 hbody =>
166    ev h1; obtain ⟨-, rfl⟩ := h1
167    ev h2; obtain ⟨rfl, rfl⟩ := h2
168    cases hbody
169
170/-! ## Deflate: fixed Huffman blocks (`F-fixed-lengths`, `F-match-copy`, `F-distance-bound`) -/
171
172/-- The stream of "a" (zlib raw deflate, fixed block): header 1,1,0; literal 0x61; end of block. -/
173example : Deflate.Decodes [] [0x4b, 0x04, 0x00] [0x61] :=
174  ⟨_, .last rfl rfl (.fixed (.lit (s := 97) rfl dk (.eob rfl))), dk⟩
175/-- "aaaaaaaaaa": literals "aa", then a match of length 8 at distance 1 (it overlaps itself). -/
176example : Deflate.Decodes [] [0x4b, 0x4c, 0x84, 0x01, 0x00] (List.replicate 10 0x61) :=
177  ⟨_, .last rfl rfl (.fixed (.lit (s := 97) rfl dk (.lit (s := 97) rfl dk
178    (.copy (s := 262) (d := 0) (xl := 0) (xd := 0) rfl dk dk rfl rfl dk rfl dk (.eob rfl))))), dk⟩
179/-- "abcabcabcabc": literals "abca", then length 8 at distance 3. -/
180example : Deflate.Decodes [] [0x4b, 0x4c, 0x4a, 0x4e, 0x84, 0x21, 0x00]
181    [0x61, 0x62, 0x63, 0x61, 0x62, 0x63, 0x61, 0x62, 0x63, 0x61, 0x62, 0x63] :=
182  ⟨_, .last rfl rfl (.fixed (.lit (s := 97) rfl dk (.lit (s := 98) rfl dk (.lit (s := 99) rfl dk
183    (.lit (s := 97) rfl dk
184    (.copy (s := 262) (d := 2) (xl := 0) (xd := 0) rfl dk dk rfl rfl dk rfl dk (.eob rfl))))))), dk⟩
185/-- Two blocks: a stored block that is not final ("ab"), then a final fixed block that copies
186from the first (length 3, distance 2). Back-references reach across blocks. -/
187example : Deflate.Decodes [] [0x00, 0x02, 0x00, 0xFD, 0xFF, 0x61, 0x62, 0x03, 0x42, 0x00]
188    [0x61, 0x62, 0x61, 0x62, 0x61] :=
189  ⟨_, .more rfl rfl (.stored rfl rfl rfl rfl) (.last rfl rfl (.fixed
190    (.copy (s := 257) (d := 1) (xl := 0) (xd := 0) rfl dk dk rfl rfl dk rfl dk (.eob rfl)))), dk⟩
191/-- With a preset dictionary "ab", a block that begins with a match is valid. -/
192example : Deflate.Decodes [0x61, 0x62] [0x03, 0x42, 0x00] [0x61, 0x62, 0x61] :=
193  ⟨_, .last rfl rfl (.fixed
194    (.copy (s := 257) (d := 1) (xl := 0) (xd := 0) rfl dk dk rfl rfl dk rfl dk (.eob rfl))), dk⟩
195/-- Bytes after the deflate data are the tail: `Prefix` splits them off. -/
196example : Deflate.Prefix [] [0x4b, 0x04, 0x00, 0xAA, 0xBB] [0xAA, 0xBB] [0x61] :=
197  ⟨_, .last rfl rfl (.fixed (.lit (s := 97) rfl dk (.eob rfl))), dk⟩
198
199/-- Negative (`F-distance-bound`): the match has distance 2 but only 1 byte was produced. -/
200example : ∀ out, ¬ Deflate.Decodes [] [0x4b, 0x04, 0x42, 0x00] out := by
201  rintro out ⟨rest, hb, -⟩
202  cases hb with
203  | more h1 => ev h1; exact absurd h1.1 (by decide)
204  | last h1 h2 hbody =>
205    ev h1; obtain ⟨-, rfl⟩ := h1
206    ev h2; obtain ⟨rfl, rfl⟩ := h2
207    cases hbody with
208    | fixed hs =>
209      cases hs with
210      | eob h => ev h; exact absurd h.1 (by decide)
211      | copy h h2 => ev h; obtain ⟨rfl, rfl⟩ := h; exact absurd h2 (by decide)
212      | lit h _ hs =>
213        ev h; obtain ⟨rfl, rfl⟩ := h
214        cases hs with
215        | eob h => ev h; exact absurd h.1 (by decide)
216        | lit h hlt => ev h; obtain ⟨rfl, rfl⟩ := h; exact absurd hlt (by decide)
217        | copy h _ _ hl hd _ hx hdist =>
218          ev h; obtain ⟨rfl, rfl⟩ := h
219          ev hl; obtain ⟨rfl, rfl⟩ := hl
220          ev hd; obtain ⟨rfl, rfl⟩ := hd
221          ev hx; obtain ⟨rfl, rfl⟩ := hx
222          exact absurd hdist (by decide)
223/-- The same stream is valid with a preset dictionary of one byte (distance 2 then reaches it):
224the distance bound counts the dictionary. -/
225example : Deflate.Decodes [0x62] [0x4b, 0x04, 0x42, 0x00] [0x61, 0x62, 0x61, 0x62] :=
226  ⟨_, .last rfl rfl (.fixed (.lit (s := 97) rfl dk
227    (.copy (s := 257) (d := 1) (xl := 0) (xd := 0) rfl dk dk rfl rfl dk rfl dk (.eob rfl)))), dk⟩
228
229
230/-- Negative (`F-fixed-lengths`): in a fixed block, distance symbol 30 is invalid. -/
231example : ∀ out, ¬ Deflate.Decodes [] [0x4b, 0x04, 0x3e, 0x00] out := by
232  rintro out ⟨rest, hb, -⟩
233  cases hb with
234  | more h1 => ev h1; exact absurd h1.1 (by decide)
235  | last h1 h2 hbody =>
236    ev h1; obtain ⟨-, rfl⟩ := h1
237    ev h2; obtain ⟨rfl, rfl⟩ := h2
238    cases hbody with
239    | fixed hs =>
240      cases hs with
241      | eob h => ev h; exact absurd h.1 (by decide)
242      | copy h h2 => ev h; obtain ⟨rfl, rfl⟩ := h; exact absurd h2 (by decide)
243      | lit h _ hs =>
244        ev h; obtain ⟨rfl, rfl⟩ := h
245        cases hs with
246        | eob h => ev h; exact absurd h.1 (by decide)
247        | lit h hlt => ev h; obtain ⟨rfl, rfl⟩ := h; exact absurd hlt (by decide)
248        | copy h _ _ hl hd hd29 =>
249          ev h; obtain ⟨rfl, rfl⟩ := h
250          ev hl; obtain ⟨rfl, rfl⟩ := hl
251          ev hd; obtain ⟨rfl, rfl⟩ := hd
252          exact absurd hd29 (by decide)
253/-- Negative (`F-fixed-lengths`): in a fixed block, literal/length symbol 286 is invalid. -/
254example : ∀ out, ¬ Deflate.Decodes [] [0x4b, 0x1c, 0x03, 0x00] out := by
255  rintro out ⟨rest, hb, -⟩
256  cases hb with
257  | more h1 => ev h1; exact absurd h1.1 (by decide)
258  | last h1 h2 hbody =>
259    ev h1; obtain ⟨-, rfl⟩ := h1
260    ev h2; obtain ⟨rfl, rfl⟩ := h2
261    cases hbody with
262    | fixed hs =>
263      cases hs with
264      | eob h => ev h; exact absurd h.1 (by decide)
265      | copy h h2 => ev h; obtain ⟨rfl, rfl⟩ := h; exact absurd h2 (by decide)
266      | lit h _ hs =>
267        ev h; obtain ⟨rfl, rfl⟩ := h
268        cases hs with
269        | eob h => ev h; exact absurd h.1 (by decide)
270        | lit h hlt => ev h; obtain ⟨rfl, rfl⟩ := h; exact absurd hlt (by decide)
271        | copy h _ h285 => ev h; obtain ⟨rfl, rfl⟩ := h; exact absurd h285 (by decide)
272
273/-! ## Deflate: dynamic blocks (`F-dynamic-limits`, `F-dynamic-repeat`, `F-dynamic-eob`, `F-dynamic-valid`) -/
274
275/-- A dynamic block written by hand (and accepted by zlib): `HLIT = 2`, `HDIST = 1`, `HCLEN = 14`;
276a code-length code with the four symbols 0, 1, 2, 18 (all of length 2); literal/length lengths
277`a`:2, `b`:2, 256:2, 258:2; distance lengths `[0, 1]`, so the distance code has one symbol of
278length 1 (the single-symbol exception). The data is "a", "b", a match of length 4 at distance 2,
279and the end of block: "ababab". -/
280example : Deflate.Decodes []
281    [21, 193, 1, 9, 0, 0, 0, 128, 160, 173, 245, 127, 68, 132, 184, 0]
282    [0x61, 0x62, 0x61, 0x62, 0x61, 0x62] :=
283  ⟨_, .last rfl rfl (.dynamic rfl rfl rfl dk rfl dk
284    (.rep18 dk rfl rfl dk (.len dk rfl dk (.len dk rfl dk (.rep18 dk rfl rfl dk (.rep18 dk rfl rfl dk
285      (.len dk rfl dk (.len dk rfl dk (.len dk rfl dk (.len dk rfl dk (.len dk rfl dk
286        (.done dk))))))))))) dk dk dk
287    (.lit (s := 97) rfl dk (.lit (s := 98) rfl dk
288      (.copy (s := 258) (d := 1) (xl := 0) (xd := 0) rfl dk dk rfl rfl dk rfl dk (.eob rfl))))), dk⟩
289/-- Negative (`F-dynamic-limits`): `HLIT = 30`, that is 287 literal/length codes. -/
290example : ∀ out, ¬ Deflate.Decodes [] [0xF5, 0x00, 0x00, 0x00] out := by
291  rintro out ⟨rest, hb, -⟩
292  cases hb with
293  | more h1 => ev h1; exact absurd h1.1 (by decide)
294  | last h1 h2 hbody =>
295    ev h1; obtain ⟨-, rfl⟩ := h1
296    ev h2; obtain ⟨rfl, rfl⟩ := h2
297    cases hbody with
298    | dynamic a b _ hcnt =>
299      ev a; obtain ⟨rfl, rfl⟩ := a
300      ev b; obtain ⟨rfl, rfl⟩ := b
301      exact absurd hcnt (by decide)
302/-- Negative (`F-dynamic-repeat`): the first code length is symbol 16 (repeat the previous
303length), but there is no previous length. The code-length code is 16 and 1 with length 1. -/
304example : ∀ out, ¬ Deflate.Decodes [] [5, 192, 3, 0, 0, 0, 0, 0, 144, 0, 0] out := by
305  rintro out ⟨rest, hb, -⟩
306  cases hb with
307  | more h1 => ev h1; exact absurd h1.1 (by decide)
308  | last h1 h2 hbody =>
309    ev h1; obtain ⟨-, rfl⟩ := h1
310    ev h2; obtain ⟨rfl, rfl⟩ := h2
311    cases hbody with
312    | dynamic a b c hcnt e _ g =>
313      ev a; obtain ⟨rfl, rfl⟩ := a
314      ev b; obtain ⟨rfl, rfl⟩ := b
315      ev c; obtain ⟨rfl, rfl⟩ := c
316      ev e; obtain ⟨rfl, rfl⟩ := e
317      cases g with
318      | done h => exact absurd h (by decide)
319      | len _ h hs => ev h; obtain ⟨rfl, rfl⟩ := h; exact absurd hs (by decide)
320      | rep16 _ _ hne => exact absurd rfl hne
321      | rep17 _ h => ev h; exact absurd h.1 (by decide)
322      | rep18 _ h => ev h; exact absurd h.1 (by decide)
323
324/-! ## Helper lemmas for the negative examples of the wrappers -/
325
326theorem bytesToBits_length (t : List UInt8) : (bytesToBits t).length = 8 * t.length := by
327  induction t with
328  | nil => rfl
329  | cons b t ih => simp [bytesToBits, byteBits] at *; omega
330
331theorem drop_pad (X B : List Bool) (n k : Nat) (hX : X.length = n + k) (hk : k < 8)
332    (hB : B.length % 8 = 0) :
333    List.drop (n + (List.drop n (X ++ B)).length % 8) (X ++ B) = B := by
334  have h : (List.drop n (X ++ B)).length % 8 = k := by simp [List.length_drop, hX]; omega
335  rw [h, ← hX]
336  exact List.drop_left
337
338set_option maxHeartbeats 2000000 in
339/-- Inversion of the stream of "a" (`4B 04 00`) followed by any bytes `t`: the output is "a" and
340the bytes left after the data are `t`. -/
341theorem a_stream_inv {t : List UInt8} {rest : List Bool} {out : List UInt8}
342    (hb : Blocks [] [] (bytesToBits (0x4b :: 0x04 :: 0x00 :: t)) rest out) :
343    out = [0x61] ∧ rest.drop (rest.length % 8) = bytesToBits t := by
344  have e : bytesToBits (0x4b :: 0x04 :: 0x00 :: t) =
345      [true,true,false,true,false,false,true,false, false,false,true,false,false,false,false,false,
346       false,false,false,false,false,false,false,false] ++ bytesToBits t := by
347    show byteBits 0x4b ++ (byteBits 0x04 ++ (byteBits 0x00 ++ bytesToBits t)) = _
348    rw [show byteBits 0x4b = [true,true,false,true,false,false,true,false] from by decide,
349        show byteBits 0x04 = [false,false,true,false,false,false,false,false] from by decide,
350        show byteBits 0x00 = [false,false,false,false,false,false,false,false] from by decide]
351    rfl
352  rw [e] at hb
353  cases hb with
354  | more h1 => ev h1; exact absurd h1.1 (by decide)
355  | last h1 h2 hbody =>
356    ev h1; obtain ⟨-, rfl⟩ := h1
357    ev h2; obtain ⟨rfl, rfl⟩ := h2
358    cases hbody with
359    | fixed hs =>
360      cases hs with
361      | eob h => ev h; exact absurd h.1 (by decide)
362      | copy h h2 => ev h; obtain ⟨rfl, rfl⟩ := h; exact absurd h2 (by decide)
363      | lit h _ hs =>
364        ev h; obtain ⟨rfl, rfl⟩ := h
365        cases hs with
366        | eob h =>
367          ev h; obtain ⟨-, rfl⟩ := h
368          refine ⟨rfl, ?_⟩
369          have h97 : fixedLitLens.getD 97 0 = 8 := by decide
370          have h256 : fixedLitLens.getD 256 0 = 7 := by decide
371          rw [h97, h256]
372          simp only [List.drop_drop, List.append_eq]
373          exact drop_pad _ _ 15 6 (by simp) (by decide) (by rw [bytesToBits_length]; omega)
374        | lit h hlt => ev h; obtain ⟨rfl, rfl⟩ := h; exact absurd hlt (by decide)
375        | copy h h2 => ev h; obtain ⟨rfl, rfl⟩ := h; exact absurd h2 (by decide)
376
377/-! ## The zlib wrapper (`F-zlib-header`, `F-zlib-check`) -/
378
379/-- zlib's own stream for "a": header 78 9C, the fixed block, Adler-32 `00 62 00 62`. -/
380example : Zlib.Decodes [] [0x78, 0x9C, 0x4b, 0x04, 0x00, 0x00, 0x62, 0x00, 0x62] [0x61] :=
381  ⟨0x78, 0x9C, [], _, rfl, dk, fun _ => ⟨rfl, _, .last rfl rfl (.fixed (.lit (s := 97) rfl dk (.eob rfl))), dk⟩,
382    fun h => absurd h dk⟩
383example : Zlib.Valid [0x61] [0x78, 0x9C, 0x4b, 0x04, 0x00, 0x00, 0x62, 0x00, 0x62] :=
384  ⟨0x78, 0x9C, [], _, rfl, dk, fun _ => ⟨rfl, _, .last rfl rfl (.fixed (.lit (s := 97) rfl dk (.eob rfl))), dk⟩,
385    fun h => absurd h dk⟩
386/-- With `FDICT`: header 78 20, `DICTID` = Adler-32 of "ab" = 01 26 00 C4, a block that is only a
387match of length 3 at distance 2 (it needs the dictionary), Adler-32 of "aba" = 02 4B 01 25. -/
388example : Zlib.Decodes [0x61, 0x62]
389    [0x78, 0x20, 0x01, 0x26, 0x00, 0xC4, 0x03, 0x42, 0x00, 0x02, 0x4B, 0x01, 0x25] [0x61, 0x62, 0x61] :=
390  ⟨0x78, 0x20, [0x01, 0x26, 0x00, 0xC4], _, rfl, dk, fun h => absurd h dk,
391    fun _ => ⟨dk, _, .last rfl rfl (.fixed
392      (.copy (s := 257) (d := 1) (xl := 0) (xd := 0) rfl dk dk rfl rfl dk rfl dk (.eob rfl))), dk⟩⟩
393/-- Negative: the same stream with no dictionary (zlib returns `Z_NEED_DICT`; here the dictionary id
394does not match the Adler-32 of the empty dictionary). -/
395example : ∀ out, ¬ Zlib.Decodes []
396    [0x78, 0x20, 0x01, 0x26, 0x00, 0xC4, 0x03, 0x42, 0x00, 0x02, 0x4B, 0x01, 0x25] out := by
397  rintro out ⟨cmf, flg, pre, s, hs, hh, h0, h1⟩
398  simp only [List.cons.injEq] at hs
399  obtain ⟨rfl, rfl, hs⟩ := hs
400  obtain ⟨rfl, -⟩ := h1 (by decide)
401  rw [show be32 (adler32 []).toNat = [0, 0, 0, 1] from by decide] at hs
402  simp at hs
403/-- Negative: the same stream with the wrong dictionary "ac". -/
404example : ∀ out, ¬ Zlib.Decodes [0x61, 0x63]
405    [0x78, 0x20, 0x01, 0x26, 0x00, 0xC4, 0x03, 0x42, 0x00, 0x02, 0x4B, 0x01, 0x25] out := by
406  rintro out ⟨cmf, flg, pre, s, hs, hh, h0, h1⟩
407  simp only [List.cons.injEq] at hs
408  obtain ⟨rfl, rfl, hs⟩ := hs
409  obtain ⟨rfl, -⟩ := h1 (by decide)
410  rw [show be32 (adler32 [0x61, 0x63]).toNat = [1, 0x27, 0, 0xC5] from by decide] at hs
411  simp at hs
412/-- Negative (`F-zlib-header`): the header check fails, 0x789D is not a multiple of 31. -/
413example : ∀ out, ¬ Zlib.Decodes [] [0x78, 0x9D, 0x4b, 0x04, 0x00, 0x00, 0x62, 0x00, 0x62] out := by
414  rintro out ⟨cmf, flg, pre, s, hs, hh, -⟩
415  simp only [List.cons.injEq] at hs
416  obtain ⟨rfl, rfl, -⟩ := hs
417  exact absurd hh (by decide)
418/-- Negative (`F-zlib-header`): compression method 9 (the check bits are right). -/
419example : ∀ out, ¬ Zlib.Decodes [] [0x79, 0x18, 0x4b, 0x04, 0x00, 0x00, 0x62, 0x00, 0x62] out := by
420  rintro out ⟨cmf, flg, pre, s, hs, hh, -⟩
421  simp only [List.cons.injEq] at hs
422  obtain ⟨rfl, rfl, -⟩ := hs
423  exact absurd hh (by decide)
424/-- Negative (`F-zlib-header`): window size field `CINFO = 8` (the check bits are right). -/
425example : ∀ out, ¬ Zlib.Decodes [] [0x88, 0x1C, 0x4b, 0x04, 0x00, 0x00, 0x62, 0x00, 0x62] out := by
426  rintro out ⟨cmf, flg, pre, s, hs, hh, -⟩
427  simp only [List.cons.injEq] at hs
428  obtain ⟨rfl, rfl, -⟩ := hs
429  exact absurd hh (by decide)
430/-- Negative (`F-zlib-check`): the Adler-32 is wrong (last byte 0x63 instead of 0x62). -/
431example : ∀ out, ¬ Zlib.Decodes [] [0x78, 0x9C, 0x4b, 0x04, 0x00, 0x00, 0x62, 0x00, 0x63] out := by
432  rintro out ⟨cmf, flg, pre, s, hs, hh, h0, h1⟩
433  simp only [List.cons.injEq] at hs
434  obtain ⟨rfl, rfl, hs⟩ := hs
435  obtain ⟨rfl, ⟨rest, hb, ht⟩⟩ := h0 (by decide)
436  simp only [List.nil_append] at hs
437  subst hs
438  obtain ⟨rfl, hr⟩ := a_stream_inv (t := [0x00, 0x62, 0x00, 0x63]) hb
439  rw [hr] at ht
440  exact absurd ht (by decide)
441/-- Negative: a stream that is too short (no trailer). -/
442example : ∀ out, ¬ Zlib.Decodes [] [0x78, 0x9C, 0x4b, 0x04, 0x00] out := by
443  rintro out ⟨cmf, flg, pre, s, hs, hh, h0, h1⟩
444  simp only [List.cons.injEq] at hs
445  obtain ⟨rfl, rfl, hs⟩ := hs
446  obtain ⟨rfl, ⟨rest, hb, ht⟩⟩ := h0 (by decide)
447  simp only [List.nil_append] at hs
448  subst hs
449  obtain ⟨rfl, hr⟩ := a_stream_inv (t := []) hb
450  rw [hr] at ht
451  exact absurd ht (by decide)
452
453/-! ## The gzip wrapper (format.md section 4, `F-gzip-check`) -/
454
455/-- zlib's own gzip stream for "a" (no optional fields): header 1F 8B 08 00 + MTIME 0 + XFL 2 + OS 19,
456the fixed block, CRC-32 `E8B7BE43` and length 1, both little endian. -/
457example : Gzip.Decodes
458    [31, 139, 8, 0, 0, 0, 0, 0, 2, 19, 75, 4, 0, 67, 190, 183, 232, 1, 0, 0, 0] [0x61] :=
459  ⟨0, [0, 0, 0, 0], 2, 19, [], [], [], [75, 4, 0, 67, 190, 183, 232, 1, 0, 0, 0], dk, dk, dk, dk, dk, dk,
460    _, .last rfl rfl (.fixed (.lit (s := 97) rfl dk (.eob rfl))), dk⟩
461/-- A header with `FHCRC` and `FNAME` (flags 10): name "a.txt", MTIME 01 02 03 04, then the
46216-bit header CRC D3 C6 (the low 16 bits of the CRC-32 of the 16 header bytes before it). -/
463example : Gzip.Decodes
464    [31, 139, 8, 10, 1, 2, 3, 4, 0, 3, 97, 46, 116, 120, 116, 0, 211, 198,
465     75, 4, 0, 67, 190, 183, 232, 1, 0, 0, 0] [0x61] :=
466  ⟨10, [1, 2, 3, 4], 0, 3, [], [97, 46, 116, 120, 116], [], [75, 4, 0, 67, 190, 183, 232, 1, 0, 0, 0], dk, dk, dk, dk, dk, dk,
467    _, .last rfl rfl (.fixed (.lit (s := 97) rfl dk (.eob rfl))), dk⟩
468/-- `FEXTRA` (flags 4): `XLEN = 2` and two extra bytes. -/
469example : Gzip.Decodes
470    [31, 139, 8, 4, 0, 0, 0, 0, 0, 3, 2, 0, 7, 7, 75, 4, 0, 67, 190, 183, 232, 1, 0, 0, 0] [0x61] :=
471  ⟨4, [0, 0, 0, 0], 0, 3, [7, 7], [], [], [75, 4, 0, 67, 190, 183, 232, 1, 0, 0, 0], dk, dk, dk, dk, dk, dk,
472    _, .last rfl rfl (.fixed (.lit (s := 97) rfl dk (.eob rfl))), dk⟩
473/-- Negative: the wrong magic number (ID2 = 138). -/
474example : ∀ out, ¬ Gzip.Decodes
475    [31, 138, 8, 0, 0, 0, 0, 0, 2, 19, 75, 4, 0, 67, 190, 183, 232, 1, 0, 0, 0] out := by
476  rintro out ⟨flg, mtime, xfl, os, extra, name, comment, s, -, -, -, -, -, hs, -⟩
477  simp only [Gzip.header, List.cons_append, List.cons.injEq] at hs
478  exact absurd hs.2.1 (by decide)
479/-- Negative: the reserved flag bit 5 is set (zlib: `unknown header flags set`). -/
480example : ∀ out, ¬ Gzip.Decodes
481    [31, 139, 8, 32, 0, 0, 0, 0, 2, 19, 75, 4, 0, 67, 190, 183, 232, 1, 0, 0, 0] out := by
482  rintro out ⟨flg, mtime, xfl, os, extra, name, comment, s, hf, -, -, -, -, hs, -⟩
483  simp only [Gzip.header, List.cons_append, List.cons.injEq] at hs
484  obtain ⟨-, -, -, rfl, -⟩ := hs
485  exact absurd hf (by decide)
486/-- Negative (`F-gzip-check`): the CRC-32 is wrong (first CRC byte 67 changed to 68). -/
487example : ∀ out, ¬ Gzip.Decodes
488    [31, 139, 8, 0, 0, 0, 0, 0, 2, 19, 75, 4, 0, 68, 190, 183, 232, 1, 0, 0, 0] out := by
489  rintro out ⟨flg, mtime, xfl, os, extra, name, comment, s, hf, hm, he, hn, hc, hs, rest, hb, ht⟩
490  obtain ⟨a, b, c, d, rfl⟩ : ∃ a b c d, mtime = [a, b, c, d] := by
491    match mtime, hm with
492    | [a, b, c, d], _ => exact ⟨a, b, c, d, rfl⟩
493  simp [Gzip.header] at hs
494  obtain ⟨rfl, -, -, -, -, rfl, rfl, hs⟩ := hs
495  simp at hs
496  subst hs
497  obtain ⟨rfl, hr⟩ := a_stream_inv (t := [68, 190, 183, 232, 1, 0, 0, 0]) hb
498  rw [hr] at ht
499  exact absurd ht (by decide)
500
501/-- Negative (`F-gzip-check`): the length is wrong (`ISIZE` = 2 for one byte of data). -/
502example : ∀ out, ¬ Gzip.Decodes
503    [31, 139, 8, 0, 0, 0, 0, 0, 2, 19, 75, 4, 0, 67, 190, 183, 232, 2, 0, 0, 0] out := by
504  rintro out ⟨flg, mtime, xfl, os, extra, name, comment, s, hf, hm, he, hn, hc, hs, rest, hb, ht⟩
505  obtain ⟨a, b, c, d, rfl⟩ : ∃ a b c d, mtime = [a, b, c, d] := by
506    match mtime, hm with
507    | [a, b, c, d], _ => exact ⟨a, b, c, d, rfl⟩
508  simp [Gzip.header] at hs
509  obtain ⟨rfl, -, -, -, -, rfl, rfl, hs⟩ := hs
510  simp at hs
511  subst hs
512  obtain ⟨rfl, hr⟩ := a_stream_inv (t := [67, 190, 183, 232, 2, 0, 0, 0]) hb
513  rw [hr] at ht
514  exact absurd ht (by decide)
515
516end ZlibF.Spec