HeaderRoundtrip.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Proof.Api.GzipRoundtrip
2
3namespace ZlibF.Spec.Api.Proofs
4open ZlibF.Spec ZlibF.Spec.Proofs
5
6/-- Two legal parses of the same gzip header agree on every field the API exposes. -/
7theorem header_fill_unique {flag : UInt8} {mt mt' : List UInt8} {xf xf' os os' : UInt8}
8    {ex ex' nm nm' cm cm' : List UInt8} (req : HdrReq)
9    (hm : mt.length = 4) (hm' : mt'.length = 4)
10    (he : ex.length < 2 ^ 16) (he' : ex'.length < 2 ^ 16)
11    (hn : (0 : UInt8) ∉ nm) (hn' : (0 : UInt8) ∉ nm')
12    (_hc : (0 : UInt8) ∉ cm) (_hc' : (0 : UInt8) ∉ cm')
13    (hh : Gzip.header flag mt xf os ex nm cm = Gzip.header flag mt' xf' os' ex' nm' cm') :
14    fillHeader req flag.toNat (mt.foldr (fun b a => a * 256 + b.toNat) 0) xf.toNat os.toNat ex nm cm =
15    fillHeader req flag.toNat (mt'.foldr (fun b a => a * 256 + b.toNat) 0) xf'.toNat os'.toNat ex' nm' cm' := by
16  rw [header_eq, header_eq] at hh
17  simp only [List.cons.injEq, true_and] at hh
18  simp only [List.append_assoc] at hh
19  have hmt := List.append_inj_left hh (by omega : mt.length = mt'.length)
20  subst mt'
21  have htail := List.append_cancel_left hh
22  simp only [List.cons_append, List.cons.injEq] at htail
23  obtain ⟨rfl, rfl, hbody⟩ := htail
24  have hextra : flag.toNat / 4 % 2 = 1 → ex = ex' := by
25    intro hbit
26    simp only [hbit, ↓reduceIte] at hbody
27    have hpart := PU_extra (le16 ex.length ++ ex) (le16 ex'.length ++ ex') _ _
28      ⟨ex, he, rfl⟩ ⟨ex', he', rfl⟩ (by simpa [List.append_assoc] using hbody)
29    have htail := congrArg (List.drop 2) hpart
30    simpa [le16] using htail
31  have hname : flag.toNat / 8 % 2 = 1 → nm = nm' := by
32    intro hbit
33    by_cases hbitex : flag.toNat / 4 % 2 = 1
34    · have ee := hextra hbitex
35      subst ex'
36      simp only [hbitex, ↓reduceIte, List.append_assoc, List.append_right_inj] at hbody
37      simp only [hbit, ↓reduceIte] at hbody
38      have hpart := PU_term (nm ++ [0]) (nm' ++ [0]) _ _ ⟨nm, hn, rfl⟩ ⟨nm', hn', rfl⟩
39        (by simpa [List.append_assoc] using hbody)
40      exact List.append_cancel_right hpart
41    · simp only [hbitex, ↓reduceIte, List.nil_append, hbit] at hbody
42      have hpart := PU_term (nm ++ [0]) (nm' ++ [0]) _ _ ⟨nm, hn, rfl⟩ ⟨nm', hn', rfl⟩
43        (by simpa [List.append_assoc] using hbody)
44      exact List.append_cancel_right hpart
45  have hcomment : flag.toNat / 16 % 2 = 1 → cm = cm' := by
46    intro hbit
47    by_cases hbex : flag.toNat / 4 % 2 = 1
48    · have ee := hextra hbex
49      subst ex'
50      simp only [hbex, ↓reduceIte, List.append_assoc, List.append_right_inj] at hbody
51      by_cases hbnm : flag.toNat / 8 % 2 = 1
52      · have en := hname hbnm
53        subst nm'
54        simp only [hbnm, ↓reduceIte, List.append_assoc, List.append_right_inj, hbit] at hbody
55        exact List.append_cancel_right hbody
56      · simp only [hbnm, ↓reduceIte, List.nil_append, hbit] at hbody
57        exact List.append_cancel_right hbody
58    · simp only [hbex, ↓reduceIte, List.nil_append] at hbody
59      by_cases hbnm : flag.toNat / 8 % 2 = 1
60      · have en := hname hbnm
61        subst nm'
62        simp only [hbnm, ↓reduceIte, List.append_assoc, List.append_right_inj, hbit] at hbody
63        exact List.append_cancel_right hbody
64      · simp only [hbnm, ↓reduceIte, List.nil_append, hbit] at hbody
65        exact List.append_cancel_right hbody
66  unfold fillHeader
67  by_cases hbex : flag.toNat / 4 % 2 = 1 <;>
68    by_cases hbnm : flag.toNat / 8 % 2 = 1 <;>
69    by_cases hbcm : flag.toNat / 16 % 2 = 1 <;>
70    simp_all
71
72private theorem flag_values (h : GzHead) : h.flg.toUInt8.toNat = h.flg ∧
73    (h.flg.toUInt8.toNat / 2 % 2 = 1 ↔ h.hcrc = true) := by
74  cases h with
75  | mk text time os extra name comment hcrc =>
76    cases text <;> cases hcrc <;> cases extra <;> cases name <;> cases comment <;> simp [GzHead.flg]
77
78private theorem mtime_value (t : Nat) :
79    (le32 t).foldr (fun b a => a * 256 + b.toNat) 0 = t % 2 ^ 32 := by
80  simp [le32, Nat.toUInt8, UInt8.toNat_ofNat']
81  omega
82
83private theorem xfl_value (p : DeflParams) : (xflOf p).toUInt8.toNat = xflOf p := by
84  unfold xflOf
85  split <;> (try rfl)
86  split <;> rfl
87
88/-- The model header reader recovers the fields of the valid header written by deflate. -/
89theorem header_roundtrip : Goal.header_roundtrip := by
90  intro p h x sd req g hc hw hvalid ht hd hp hhead hread
91  have hparam : sd.params = p := by simpa [DeflState.fresh] using deflate_trace_params ht
92  have hheader : sd.header = h := by simp [DeflState.header, hhead]
93  have hv := deflate_valid p x sd hc ht hd hp
94  have hwritten : Gzip.DecodesWith (h.bytes p) sd.produced sd.input := by
95    simpa [DeflState.Valid, hparam, hw, hheader] using hv
96  have hformat := gzip_decode_with_header hvalid hwritten
97  obtain ⟨tail, hstream, _⟩ := hwritten
98  rcases hread with hread | hread
99  · obtain ⟨flag, mt, xf, os, ex, nm, cm, rest, hflag, hmt, hex, hnm, hcm, hparse, rfl⟩ := hread
100    have hcore : sd.produced = Gzip.header h.flg.toUInt8 (le32 h.time) (xflOf p).toUInt8 h.os.toUInt8
101          (h.extra.getD []) (h.name.getD []) (h.comment.getD []) ++
102        (if h.hcrc then le16 ((crc32 (h.core p)).toNat % 2 ^ 16) else []) ++ tail := by
103      simpa [GzHead.bytes, GzHead.core] using hstream
104    have he : h.flg.toUInt8 = flag := by
105      rw [hcore, header_eq, header_eq] at hparse
106      simp only [List.cons_append, List.cons.injEq] at hparse
107      exact hparse.2.2.2.1
108    subst flag
109    have hvalidextra : (h.extra.getD []).length < 2 ^ 16 := by
110      cases he : h.extra with
111      | none => simp
112      | some e => simpa [he] using hvalid.1 e he
113    have hvalidname : (0 : UInt8) ∉ h.name.getD [] := by
114      cases hn : h.name with
115      | none => simp
116      | some name => simpa [hn] using hvalid.2.1 name hn
117    have hvalidcomment : (0 : UInt8) ∉ h.comment.getD [] := by
118      cases hc : h.comment with
119      | none => simp
120      | some comment => simpa [hc] using hvalid.2.2 comment hc
121    have hmem1 := header_mem h.flg.toUInt8 (le32 h.time) (xflOf p).toUInt8 h.os.toUInt8
122      (h.extra.getD []) (h.name.getD []) (h.comment.getD []) (le32_length _) hvalidextra hvalidname hvalidcomment
123    have hmem2 := header_mem h.flg.toUInt8 mt xf os ex nm cm hmt hex hnm hcm
124    have heq := hcore.symm.trans hparse
125    have hheaders := PU_HdrSet h.flg.toUInt8 _ _ _ _ hmem1 hmem2 (by simpa [List.append_assoc] using heq)
126    have hfill := header_fill_unique req (le32_length _) hmt hvalidextra hex hvalidname hnm
127      hvalidcomment hcm hheaders
128    have hvalues := flag_values h
129    have hx : xflOf p % 256 = xflOf p := by
130      simpa [Nat.toUInt8, UInt8.toNat_ofNat'] using xfl_value p
131    simpa [expectedHdr, hvalues.1, mtime_value, Nat.toUInt8, UInt8.toNat_ofNat', hx] using hfill.symm
132  · obtain ⟨cmf, flag, r, hs, hh, _⟩ := hread
133    obtain ⟨rest, hprefix⟩ := ZlibF.Spec.gzip_head hformat
134    rw [hs] at hprefix
135    simp only [List.cons.injEq] at hprefix
136    have he : cmf = 31 := hprefix.1
137    rw [he] at hh
138    exact False.elim ((by decide : ¬ ((31 : UInt8).toNat % 16 = 8)) hh.1)
139
140#print axioms header_roundtrip
141#print axioms header_fill_unique
142end ZlibF.Spec.Api.Proofs