Wrapper.lean

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

1import ZlibF.Proof.Format.Deflate
2import ZlibF.Spec.Format.Wrapper
3
4/-!
5# Format meta-theory: the wrappers are parsed in one way
6
7`Zlib.ext`, `Gzip.ext`: if `z` is a complete zlib (gzip) stream and `z ++ t` is one too, then
8`t = []` and the outputs are equal. The gzip header is a prefix-free language (`PU`): fixed length
9fields, a length-prefixed field and zero-terminated fields.
10-/
11
12namespace ZlibF.Spec
13
14namespace Proofs
15
16/-- A set of byte strings is prefix-unique if no two of its members are in a prefix relation unless
17they are equal. -/
18def PU (P : List UInt8 → Prop) : Prop :=
19  ∀ x y a b, P x → P y → x ++ a = y ++ b → x = y
20
21/-- Concatenation of two sets. -/
22def PUapp (P Q : List UInt8 → Prop) : List UInt8 → Prop :=
23  fun l => ∃ x y, P x ∧ Q y ∧ l = x ++ y
24
25/-- A field that is present only if the condition holds. -/
26def Pite (c : Prop) [Decidable c] (P : List UInt8 → Prop) : List UInt8 → Prop :=
27  fun l => if c then P l else l = []
28
29/-- A zero-terminated string without zeros. -/
30def Pterm : List UInt8 → Prop := fun l => ∃ n : List UInt8, (0 : UInt8) ∉ n ∧ l = n ++ [0]
31
32/-- `XLEN` (2 bytes, little endian) and that many bytes. -/
33def Pextra : List UInt8 → Prop :=
34  fun l => ∃ e : List UInt8, e.length < 2 ^ 16 ∧ l = le16 e.length ++ e
35
36theorem PU_len (n : Nat) : PU (fun l => l.length = n) := by
37  intro x y a b hx hy h
38  exact (List.append_inj h (by omega)).1
39
40theorem PU_append {P Q : List UInt8 → Prop} (hP : PU P) (hQ : PU Q) : PU (PUapp P Q) := by
41  rintro _ _ a b ⟨x1, y1, hx1, hy1, rfl⟩ ⟨x2, y2, hx2, hy2, rfl⟩ h
42  have h1 : x1 = x2 := hP x1 x2 (y1 ++ a) (y2 ++ b) hx1 hx2 (by simpa [List.append_assoc] using h)
43  subst h1
44  have h2 : y1 = y2 := hQ y1 y2 a b hy1 hy2 (by simpa [List.append_assoc] using h)
45  rw [h2]
46
47theorem PU_ite (c : Prop) [Decidable c] {P : List UInt8 → Prop} (hP : PU P) : PU (Pite c P) := by
48  intro x y a b hx hy h
49  unfold Pite at hx hy
50  by_cases hc : c
51  · simp only [hc, ↓reduceIte] at hx hy; exact hP x y a b hx hy h
52  · simp only [hc, ↓reduceIte] at hx hy; rw [hx, hy]
53
54theorem PU_term : PU Pterm := by
55  have key : ∀ (n m a b : List UInt8), (0 : UInt8) ∉ n → (0 : UInt8) ∉ m →
56      n ++ 0 :: a = m ++ 0 :: b → n = m := by
57    intro n
58    induction n with
59    | nil =>
60      intro m a b hn hm h
61      cases m with
62      | nil => rfl
63      | cons c m => simp at h; exact absurd (by simp [h.1]) hm
64    | cons c n ih =>
65      intro m a b hn hm h
66      cases m with
67      | nil => simp at h; exact absurd (by simp [h.1]) hn
68      | cons d m =>
69        simp only [List.cons_append, List.cons.injEq] at h
70        obtain ⟨rfl, h2⟩ := h
71        rw [ih m a b (fun hh => hn (List.mem_cons_of_mem _ hh))
72          (fun hh => hm (List.mem_cons_of_mem _ hh)) h2]
73  rintro _ _ a b ⟨n, hn, rfl⟩ ⟨m, hm, rfl⟩ h
74  rw [key n m a b hn hm (by simpa [List.append_assoc] using h)]
75
76theorem PU_extra : PU Pextra := by
77  rintro _ _ a b ⟨e, he, rfl⟩ ⟨e', he', rfl⟩ h
78  have hh : le16 e.length ++ (e ++ a) = le16 e'.length ++ (e' ++ b) := by
79    simpa [List.append_assoc] using h
80  obtain ⟨h1, h2⟩ := List.append_inj hh (by simp [le16])
81  have hl : e.length = e'.length := by
82    simp only [le16, List.cons.injEq, and_true] at h1
83    obtain ⟨h1a, h1b⟩ := h1
84    have a1 := congrArg UInt8.toNat h1a
85    have a2 := congrArg UInt8.toNat h1b
86    simp [Nat.toUInt8] at a1 a2
87    omega
88  have := (List.append_inj h2 hl).1
89  rw [this]
90
91/-- The gzip header with its flags fixed, as a language. -/
92def HdrSet (flg : UInt8) : List UInt8 → Prop :=
93  PUapp (PUapp (PUapp (fun l => l.length = 10) (Pite (flg.toNat / 4 % 2 = 1) Pextra))
94    (Pite (flg.toNat / 8 % 2 = 1) Pterm)) (Pite (flg.toNat / 16 % 2 = 1) Pterm)
95
96theorem PU_HdrSet (flg : UInt8) : PU (HdrSet flg) :=
97  PU_append (PU_append (PU_append (PU_len 10) (PU_ite _ PU_extra)) (PU_ite _ PU_term))
98    (PU_ite _ PU_term)
99
100theorem header_mem (flg : UInt8) (mt : List UInt8) (xfl os : UInt8) (ex nm cm : List UInt8)
101    (hmt : mt.length = 4) (hex : ex.length < 2 ^ 16) (hnm : (0 : UInt8) ∉ nm)
102    (hcm : (0 : UInt8) ∉ cm) : HdrSet flg (Gzip.header flg mt xfl os ex nm cm) := by
103  refine ⟨_, if flg.toNat / 16 % 2 = 1 then cm ++ [0] else [], ⟨_, if flg.toNat / 8 % 2 = 1 then nm ++ [0] else [], ⟨[31, 139, 8, flg] ++ mt ++ [xfl, os], if flg.toNat / 4 % 2 = 1 then le16 ex.length ++ ex else [], by simp [hmt], ?_, rfl⟩, ?_, rfl⟩, ?_, rfl⟩
104  · unfold Pite
105    by_cases h : flg.toNat / 4 % 2 = 1
106    · simp only [h, ↓reduceIte]; exact ⟨ex, hex, rfl⟩
107    · simp only [h, ↓reduceIte]
108  · unfold Pite
109    by_cases h : flg.toNat / 8 % 2 = 1
110    · simp only [h, ↓reduceIte]; exact ⟨nm, hnm, rfl⟩
111    · simp only [h, ↓reduceIte]
112  · unfold Pite
113    by_cases h : flg.toNat / 16 % 2 = 1
114    · simp only [h, ↓reduceIte]; exact ⟨cm, hcm, rfl⟩
115    · simp only [h, ↓reduceIte]
116
117theorem header_eq (flg : UInt8) (mt : List UInt8) (xfl os : UInt8) (ex nm cm : List UInt8) :
118    Gzip.header flg mt xfl os ex nm cm = 31 :: 139 :: 8 :: flg :: (mt ++ [xfl, os] ++
119      (if flg.toNat / 4 % 2 = 1 then le16 ex.length ++ ex else []) ++
120      (if flg.toNat / 8 % 2 = 1 then nm ++ [0] else []) ++
121      (if flg.toNat / 16 % 2 = 1 then cm ++ [0] else [])) := by
122  simp [Gzip.header]
123
124end Proofs
125
126open Proofs
127
128theorem gzip_head {z o : List UInt8} (h : Gzip.Decodes z o) : ∃ r, z = 31 :: r := by
129  obtain ⟨flg, mt, xfl, os, ex, nm, cm, s, -, -, -, -, -, hz, -⟩ := h
130  rw [hz, header_eq]
131  exact ⟨_, rfl⟩
132
133theorem zlib_head {d z o : List UInt8} (h : Zlib.Decodes d z o) :
134    ∃ cmf r, z = cmf :: r ∧ cmf.toNat % 16 = 8 := by
135  obtain ⟨cmf, flg, pre, s, hz, hh, -⟩ := h
136  exact ⟨cmf, _, hz, hh.1⟩
137
138theorem be32_length (n : Nat) : (be32 n).length = 4 := rfl
139theorem le32_length (n : Nat) : (le32 n).length = 4 := rfl
140
141/-- A complete zlib stream has no complete extension, and its output is determined. -/
142theorem Zlib.ext {d z t o1 o2 : List UInt8} (h1 : Zlib.Decodes d z o1)
143    (h2 : Zlib.Decodes d (z ++ t) o2) : t = [] ∧ o1 = o2 := by
144  obtain ⟨cmf, flg, pre, s, hz, hh, hA, hB⟩ := h1
145  obtain ⟨cmf', flg', pre', s', hz', hh', hA', hB'⟩ := h2
146  rw [hz] at hz'
147  simp only [List.cons_append, List.cons.injEq] at hz'
148  obtain ⟨rfl, rfl, hz'⟩ := hz'
149  by_cases hb : flg.toNat / 32 % 2 = 0
150  · obtain ⟨rfl, hp⟩ := hA hb
151    obtain ⟨rfl, hp'⟩ := hA' hb
152    simp only [List.nil_append] at hz'
153    subst hz'
154    obtain ⟨hl, ho⟩ := Prefix.ext hp hp'
155    refine ⟨?_, ho⟩
156    rw [be32_length, be32_length] at hl
157    exact List.eq_nil_of_length_eq_zero (by omega)
158  · have hb1 : flg.toNat / 32 % 2 = 1 := by omega
159    obtain ⟨rfl, hp⟩ := hB hb1
160    obtain ⟨hpre, hp'⟩ := hB' hb1
161    have : s ++ t = s' := by
162      have := hz'
163      rw [← hpre] at this
164      simpa [List.append_assoc] using this
165    subst this
166    obtain ⟨hl, ho⟩ := Prefix.ext hp hp'
167    refine ⟨?_, ho⟩
168    rw [be32_length, be32_length] at hl
169    exact List.eq_nil_of_length_eq_zero (by omega)
170
171/-- A complete gzip member has no complete extension, and its output is determined. -/
172theorem Gzip.ext {z t o1 o2 : List UInt8} (h1 : Gzip.Decodes z o1)
173    (h2 : Gzip.Decodes (z ++ t) o2) : t = [] ∧ o1 = o2 := by
174  obtain ⟨flg, mt, xfl, os, ex, nm, cm, s, hf, hmt, hex, hnm, hcm, hz, hp⟩ := h1
175  obtain ⟨flg', mt', xfl', os', ex', nm', cm', s', hf', hmt', hex', hnm', hcm', hz', hp'⟩ := h2
176  have hflg : flg = flg' := by
177    have e1 : z ++ t = _ := congrArg (· ++ t) hz
178    rw [e1, header_eq, header_eq] at hz'
179    simp only [List.cons_append, List.cons.injEq] at hz'
180    exact hz'.2.2.2.1
181  subst hflg
182  have hmem1 := header_mem flg mt xfl os ex nm cm hmt hex hnm hcm
183  have hmem2 := header_mem flg mt' xfl' os' ex' nm' cm' hmt' hex' hnm' hcm'
184  rw [hz] at hz'
185  have key : ∀ H1 H2 C1 C2 : List UInt8, HdrSet flg H1 → HdrSet flg H2 →
186      (H1 ++ C1 ++ s) ++ t = H2 ++ C2 ++ s' → H1 = H2 := by
187    intro H1 H2 C1 C2 h1 h2 h
188    exact PU_HdrSet flg H1 H2 (C1 ++ (s ++ t)) (C2 ++ s') h1 h2 (by simpa [List.append_assoc] using h)
189  have hHH := key _ _ _ _ hmem1 hmem2 hz'
190  rw [← hHH] at hz'
191  have hs : s ++ t = s' := by
192    have := hz'
193    simp only [List.append_assoc] at this
194    simpa using this
195  subst hs
196  obtain ⟨hl, ho⟩ := Prefix.ext hp hp'
197  refine ⟨?_, ho⟩
198  simp only [List.length_append, le32_length] at hl
199  exact List.eq_nil_of_length_eq_zero (by omega)
200
201end ZlibF.Spec