inflate.c.main.table2.lean

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

1import ZlibF.Proof.«inflate.c.main.table»
2
3/-!
4# inflate.c: `case LENLENS:` -- the code-length code lengths
5
6Pure part: the order of the 19 code-length code lengths, the 3-bit groups of the stream, and the array `lens` after the
7two loops (`lensRead`, `lensZero`). Mode part: the loop body, the two loops, the `inflate_table(CODES, ...)` call.
8-/
9
10namespace Zlib.Inflate.Proofs
11open C Zlib.Inflate Zlib.Inflate.Spec
12
13/-! ## The order of the code-length code lengths -/
14
15/-- `order[i]` as a number. -/
16def orderNat (i : Nat) : Nat := (order[i]!).toNat
17
18theorem order_size : order.size = 19 := rfl
19
20theorem order_lt : ∀ i, i < 19 → orderNat i < 19 := by
21  unfold orderNat order; decide +kernel
22
23theorem order_surj : ∀ k, k < 19 → ∃ i, i < 19 ∧ orderNat i = k := by
24  unfold orderNat order; decide +kernel
25
26theorem orderAt_run (h : Heap) (i : UInt32) (hi : i.toNat < 19) :
27    orderAt i h = .ok (order[i.toNat]!, h) := by
28  have hi' : i.toNat < order.size := by rw [order_size]; exact hi
29  unfold orderAt
30  rw [Array.getElem?_eq_getElem hi']
31  simp [pure_app]
32  exact (getElem!_pos order i.toNat hi').symm
33
34/-! ## The 3-bit groups of a bit stream -/
35
36/-- The number given by the first three bits of `L` (least significant first; missing bits are 0). -/
37def grp0 (L : List Bool) : Nat :=
38  (L.getD 0 false).toNat + 2 * (L.getD 1 false).toNat + 4 * (L.getD 2 false).toNat
39
40/-- The `t`-th 3-bit group of the stream `S`. -/
41def grp (S : List Bool) (t : Nat) : Nat := grp0 (S.drop (3 * t))
42
43theorem grp0_le (L : List Bool) : grp0 L ≤ 7 := by
44  unfold grp0
45  cases L.getD 0 false <;> cases L.getD 1 false <;> cases L.getD 2 false <;> decide
46
47theorem grp_le (S : List Bool) (t : Nat) : grp S t ≤ 7 := grp0_le _
48
49theorem grp0_natBits (k n : Nat) (rest : List Bool) : grp0 (natBits (3 + k) n ++ rest) = n % 8 := by
50  rw [natBits_add]
51  simp only [natBits]
52  simp [grp0]
53  have h0 := Nat.mod_two_eq_zero_or_one n
54  have h1 := Nat.mod_two_eq_zero_or_one (n / 2)
55  have h2 := Nat.mod_two_eq_zero_or_one (n / 2 / 2)
56  rcases h0 with h0 | h0 <;> rcases h1 with h1 | h1 <;> rcases h2 with h2 | h2 <;> simp [h0, h1, h2] <;> omega
57
58/-- Reading from the registers: the group is `hold % 8` once three bits are held. -/
59theorem grp_head (bits hold : Nat) (rest : List Bool) (h3 : 3 ≤ bits) : grp0 (natBits bits hold ++ rest) = hold % 8 := by
60  obtain ⟨k, rfl⟩ : ∃ k, bits = 3 + k := ⟨bits - 3, by omega⟩
61  exact grp0_natBits k hold rest
62
63theorem grp_succ (S : List Bool) (t : Nat) : grp S t = grp (S.drop (3 * t)) 0 := by
64  simp [grp]
65
66/-! ## The array `lens` after the two loops -/
67
68/-- `lens[order[i0 + u]] = grp S u` for `u < t`. -/
69def lensRead (a : Array UInt16) (i0 : Nat) (S : List Bool) : Nat → Array UInt16
70  | 0 => a
71  | t + 1 => (lensRead a i0 S t).set! (orderNat (i0 + t)) (grp S t).toUInt16
72
73/-- `lens[order[i0 + u]] = 0` for `u < t`. -/
74def lensZero (a : Array UInt16) (i0 : Nat) : Nat → Array UInt16
75  | 0 => a
76  | t + 1 => (lensZero a i0 t).set! (orderNat (i0 + t)) 0
77
78theorem lensRead_size (a : Array UInt16) (i0 : Nat) (S : List Bool) : ∀ t, (lensRead a i0 S t).size = a.size
79  | 0 => rfl
80  | t + 1 => by simp [lensRead, lensRead_size a i0 S t]
81
82theorem lensZero_size (a : Array UInt16) (i0 : Nat) : ∀ t, (lensZero a i0 t).size = a.size
83  | 0 => rfl
84  | t + 1 => by simp [lensZero, lensZero_size a i0 t]
85
86/-- The entries `lens[order[i]]`, `i < u`, are 3-bit values. -/
87def Good3 (a : Array UInt16) (u : Nat) : Prop := ∀ i, i < u → (a.getD (orderNat i) 0).toNat ≤ 7
88
89theorem Good3.set {a : Array UInt16} {u : Nat} (H : Good3 a u) (v : UInt16) (hv : v.toNat ≤ 7) (hu : u < 19) :
90    Good3 (a.set! (orderNat u) v) (u + 1) := by
91  intro i hi
92  by_cases he : orderNat i = orderNat u
93  · rw [he]
94    have hlt := order_lt u hu
95    by_cases hsz : orderNat u < a.size
96    · simp [Array.getD_eq_getD_getElem?, Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds, hsz]; exact hv
97    · simp [Array.getD_eq_getD_getElem?, Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds, hsz]
98  · have hne : i < u := by
99      rcases Nat.lt_succ_iff_lt_or_eq.mp hi with h | h
100      · exact h
101      · exact absurd (by rw [h]) he
102    have := H i hne
103    have he' : orderNat u ≠ orderNat i := fun e => he e.symm
104    simpa [Array.getD_eq_getD_getElem?, Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds, he'] using this
105
106theorem lensRead_good {a : Array UInt16} {i0 : Nat} (S : List Bool) (H : Good3 a i0) :
107    ∀ t, i0 + t ≤ 19 → Good3 (lensRead a i0 S t) (i0 + t)
108  | 0, _ => H
109  | t + 1, ht => by
110    have := (lensRead_good S H t (by omega)).set (grp S t).toUInt16 (by
111      have := grp_le S t
112      simp only [Nat.toUInt16_eq, UInt16.toNat_ofNat']; omega) (by omega)
113    rwa [show i0 + (t + 1) = i0 + t + 1 by omega]
114
115theorem lensZero_good {a : Array UInt16} {i0 : Nat} (H : Good3 a i0) :
116    ∀ t, i0 + t ≤ 19 → Good3 (lensZero a i0 t) (i0 + t)
117  | 0, _ => H
118  | t + 1, ht => by
119    have := (lensZero_good H t (by omega)).set 0 (by decide) (by omega)
120    rwa [show i0 + (t + 1) = i0 + t + 1 by omega]
121
122theorem Good3.all {a : Array UInt16} (H : Good3 a 19) : ∀ k, k < 19 → (a.getD k 0).toNat ≤ 7 := by
123  intro k hk
124  obtain ⟨i, hi, he⟩ := order_surj k hk
125  rw [← he]; exact H i hi
126
127/-! ## A mode that never executes `return v` -/
128
129/-- Running `x` never ends in `return v` (`Ex.ret`); the other exits (`goto inf_leave`, a value) are allowed. -/
130def NoRet {α : Type} (x : X α) : Prop :=
131  ∀ l h r l' h', runX x l h = .ok ((r, l'), h') → ∀ v, r ≠ .error (Ex.ret v)
132
133theorem noRet_pure {α : Type} (a : α) : NoRet (pure a : X α) := by
134  intro l h r l' h' e v
135  rw [runX_pure] at e
136  cases e
137  simp
138
139theorem noRet_leave {α : Type} : NoRet (throw Ex.leave : X α) := by
140  intro l h r l' h' e v
141  rw [runX_throw] at e
142  cases e
143  simp
144
145theorem noRet_get : NoRet (get : X IL) := by
146  intro l h r l' h' e v
147  rw [runX_get] at e
148  cases e
149  simp
150
151theorem noRet_set (l0 : IL) : NoRet (set l0 : X PUnit) := by
152  intro l h r l' h' e v
153  rw [runX_set] at e
154  cases e
155  simp
156
157theorem noRet_modify (f : IL → IL) : NoRet (modify f : X PUnit) := by
158  intro l h r l' h' e v
159  rw [runX_modify] at e
160  cases e
161  simp
162
163theorem noRet_lift {α : Type} (m : M α) : NoRet (monadLift m : X α) := by
164  intro l h r l' h' e v
165  rw [runX_lift] at e
166  cases hm : m h with
167  | error f => rw [hm] at e; cases e
168  | ok p =>
169    obtain ⟨a, h1⟩ := p
170    rw [hm] at e
171    cases e
172    simp
173
174theorem noRet_bind {α β : Type} {x : X α} {f : α → X β} (hx : NoRet x) (hf : ∀ a, NoRet (f a)) : NoRet (x >>= f) := by
175  intro l h r l' h' e v
176  rw [runX_bind] at e
177  cases hr : runX x l h with
178  | error f' => rw [hr] at e; cases e
179  | ok p =>
180    obtain ⟨⟨r1, l1⟩, h1⟩ := p
181    rw [hr] at e
182    cases r1 with
183    | ok a => exact hf a l1 h1 r l' h' e v
184    | error ex =>
185      simp only at e
186      cases e
187      intro hh
188      have hex : ex = Ex.ret v := by cases hh; rfl
189      subst hex
190      exact hx l h _ l' h' hr v rfl
191
192theorem noRet_ite {α : Type} {b : Prop} [Decidable b] {x y : X α} (hx : NoRet x) (hy : NoRet y) :
193    NoRet (if b then x else y) := by
194  by_cases hb : b
195  · simpa [hb] using hx
196  · simpa [hb] using hy
197
198theorem go_inv {σ : Type} (P : σ → Prop) (F : σ → M (Bool × σ)) (B : σ → M σ)
199    (hF : ∀ s h c s' h', P s → F s h = .ok ((c, s'), h') → P s')
200    (hB : ∀ s h s' h', P s → B s h = .ok (s', h') → P s') :
201    ∀ n s h s' h', P s → cwhile.go F B n s h = .ok (s', h') → P s' := by
202  intro n
203  induction n with
204  | zero => intro s h s' h' _ e; simp [cwhile.go] at e
205  | succ n ih =>
206    intro s h s' h' hs e
207    simp only [cwhile.go, bind_app] at e
208    cases hf : F s h with
209    | error f => rw [hf] at e; cases e
210    | ok p =>
211      obtain ⟨⟨c, s1⟩, h1⟩ := p
212      rw [hf] at e
213      have hs1 := hF s h c s1 h1 hs hf
214      cases c
215      · simp only [Bool.false_eq_true, ↓reduceIte, pure_app, Except.ok.injEq, Prod.mk.injEq] at e
216        obtain ⟨rfl, _⟩ := e
217        exact hs1
218      · simp only [ite_true, bind_app] at e
219        cases hbb : B s1 h1 with
220        | error f => rw [hbb] at e; cases e
221        | ok q =>
222          obtain ⟨s2, h2⟩ := q
223          rw [hbb] at e
224          exact ih s2 h2 s' h' (hB s1 h1 s2 h2 hs1 hbb) e
225
226/-- `xwhileBrk` over a condition and a body that never `return`: the loop never `return`s. -/
227theorem noRet_xwhileBrk {cond body : X Bool} (hc : NoRet cond) (hb : NoRet body) : NoRet (xwhileBrk cond body) := by
228  intro l0 h0 r l' h' e v
229  unfold runX xwhileBrk at e
230  simp only [ExceptT.run, StateT.run, ExceptT.mk, cwhile, bind_app] at e
231  generalize hg : cwhile.go _ _ fuel (l0, Stop.go) h0 = G at e
232  cases G with
233  | error f => simp at e
234  | ok p =>
235    obtain ⟨⟨l2, s2⟩, h2⟩ := p
236    have hk : (l2, s2).2 ≠ Stop.ex (Ex.ret v) := go_inv (fun s => s.2 ≠ Stop.ex (Ex.ret v)) _ _
237      (by
238        intro s h c s' h' hs hF
239        obtain ⟨l1, st⟩ := s
240        cases st with
241        | go =>
242          simp only [bind_app] at hF
243          cases hcr : cond l1 h with
244          | error f => rw [hcr] at hF; cases hF
245          | ok p =>
246            obtain ⟨⟨rc, lc⟩, hh⟩ := p
247            have hrc := hc l1 h rc lc hh hcr v
248            rw [hcr] at hF
249            cases rc with
250            | error ex =>
251              simp only [pure_app, Except.ok.injEq, Prod.mk.injEq] at hF
252              obtain ⟨⟨_, rfl⟩, _⟩ := hF
253              intro hh2
254              simp only [Stop.ex.injEq] at hh2
255              subst hh2
256              exact hrc rfl
257            | ok b =>
258              simp only [pure_app, Except.ok.injEq, Prod.mk.injEq] at hF
259              obtain ⟨⟨_, rfl⟩, _⟩ := hF
260              simp
261        | brk =>
262          simp only [pure_app, Except.ok.injEq, Prod.mk.injEq] at hF
263          obtain ⟨⟨_, rfl⟩, _⟩ := hF
264          exact hs
265        | ex ex2 =>
266          simp only [pure_app, Except.ok.injEq, Prod.mk.injEq] at hF
267          obtain ⟨⟨_, rfl⟩, _⟩ := hF
268          exact hs)
269      (by
270        intro s h s' h' hs hB
271        obtain ⟨l1, st⟩ := s
272        simp only [bind_app] at hB
273        cases hbr : body l1 h with
274        | error f => rw [hbr] at hB; cases hB
275        | ok p =>
276          obtain ⟨⟨rb, lb⟩, hh⟩ := p
277          have hrb := hb l1 h rb lb hh hbr v
278          rw [hbr] at hB
279          cases rb with
280          | error ex =>
281            simp only [pure_app, Except.ok.injEq, Prod.mk.injEq] at hB
282            obtain ⟨rfl, _⟩ := hB
283            intro hh2
284            simp only [Stop.ex.injEq] at hh2
285            subst hh2
286            exact hrb rfl
287          | ok b =>
288            simp only [pure_app, Except.ok.injEq, Prod.mk.injEq] at hB
289            obtain ⟨rfl, _⟩ := hB
290            cases b <;> simp)
291      fuel (l0, Stop.go) h0 (l2, s2) h2 (by simp) hg
292    simp only at hk
293    cases s2 with
294    | go => simp at e; obtain ⟨⟨rfl, _⟩, _⟩ := e; simp
295    | brk => simp at e; obtain ⟨⟨rfl, _⟩, _⟩ := e; simp
296    | ex ex2 =>
297      simp at e
298      obtain ⟨⟨rfl, _⟩, _⟩ := e
299      intro hh2
300      simp only [Except.error.injEq] at hh2
301      subst hh2
302      exact hk rfl
303
304theorem noRet_xwhile {cond : X Bool} {body : X Unit} (hc : NoRet cond) (hb : NoRet body) : NoRet (xwhile cond body) :=
305  noRet_xwhileBrk hc (noRet_bind hb fun _ => noRet_pure _)
306
307theorem noRet_PULLBYTE : NoRet PULLBYTE := by
308  unfold PULLBYTE
309  refine noRet_bind noRet_get fun l => ?_
310  by_cases h0 : l.have_ == 0
311  · simp only [h0, ite_true]
312    exact noRet_leave
313  · simp only [h0, ite_false]
314    refine noRet_bind (noRet_set _) fun _ => ?_
315    refine noRet_bind (noRet_lift _) fun _ => ?_
316    refine noRet_bind (noRet_lift _) fun _ => ?_
317    refine noRet_bind (noRet_lift _) fun _ => ?_
318    exact noRet_set _
319
320/-- `NEEDBITS(n)` never executes `return v`: it ends with a value or with `goto inf_leave`. -/
321theorem noRet_NEEDBITS (n : UInt32) : NoRet (NEEDBITS n) := by
322  unfold NEEDBITS
323  refine noRet_xwhile (noRet_bind noRet_get fun _ => noRet_pure _) noRet_PULLBYTE
324
325end Zlib.Inflate.Proofs