infback.c.wf.lean

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

1import ZlibF.Proof.«inflate.c.main.xloop»
2
3/-!
4# A loop rule with a measure
5
6`xwhileBrk_run` needs the exact number of iterations. Loops whose trip count is only bounded (the copy loop of a stored block,
7the dispatch loop) use this rule instead: an invariant, a measure that falls on every trip that continues, and the way out.
8-/
9
10namespace Zlib.Infback.Proofs
11open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs
12
13/-- **Loop rule with a measure.** `Inv` holds at the start. In every state satisfying `Inv`, the condition runs and gives `b`;
14if `b` the body runs and either leaves with `Q`, or breaks with `Q (ok ())`, or ends with `Inv` and a smaller measure;
15if not `b` then `Q (ok ())` holds. The measure at the start is below the fuel (less one). -/
16theorem xwhileBrk_wf {cond : X Bool} {body : X Bool} (Inv : IL → Heap → Prop) (Q : Except Ex Unit → IL → Heap → Prop)
17    (μ : IL → Heap → Nat)
18    (hstep : ∀ l h, Inv l h → ∃ l1 h1 b, runX cond l h = .ok ((.ok b, l1), h1) ∧
19      (b = true → ∃ r l2 h2, runX body l1 h1 = .ok ((r, l2), h2) ∧
20        (match r with
21          | .ok true => Q (.ok ()) l2 h2
22          | .ok false => Inv l2 h2 ∧ μ l2 h2 < μ l h
23          | .error e => Q (.error e) l2 h2)) ∧
24      (b = false → Q (.ok ()) l1 h1))
25    {l : IL} {h : Heap} (hI : Inv l h) (hμ : μ l h + 1 < fuel) :
26    ∃ r l' h', runX (xwhileBrk cond body) l h = .ok ((r, l'), h') ∧ Q r l' h' := by
27  have key : ∀ m n (l : IL) (h : Heap), Inv l h → μ l h ≤ m → m + 1 < n →
28      ∃ r l' h', (cwhile.go (σ := IL × Stop)
29        (fun (l, s) => match s with
30          | .go => do
31            let (r, l') ← StateT.run (ExceptT.run cond) l
32            pure (match r with
33              | .ok b => (b, (l', Stop.go))
34              | .error e => (false, (l', Stop.ex e)))
35          | s => pure (false, (l, s)))
36        (fun (l, _) => do
37          let (r, l') ← StateT.run (ExceptT.run body) l
38          pure (match r with
39            | .ok b => (l', if b then Stop.brk else Stop.go)
40            | .error e => (l', Stop.ex e))) n (l, Stop.go)) h = .ok ((l', r), h') ∧
41        (match r with
42         | .ex e => Q (.error e) l' h'
43         | _ => Q (.ok ()) l' h') := by
44    intro m
45    induction m with
46    | zero =>
47      intro n l h hI hm hn
48      obtain ⟨n, rfl⟩ : ∃ k, n = k + 1 := ⟨n - 1, by omega⟩
49      obtain ⟨l1, h1, b, hc, hT, hF⟩ := hstep l h hI
50      have hc' : (StateT.run (ExceptT.run cond) l) h = .ok ((.ok b, l1), h1) := hc
51      cases b
52      · exact ⟨.go, l1, h1, by simp [cwhile.go, hc'], hF rfl⟩
53      · obtain ⟨r, l2, h2, hb, hQ⟩ := hT rfl
54        have hb' : (StateT.run (ExceptT.run body) l1) h1 = .ok ((r, l2), h2) := hb
55        rcases r with e | b2
56        · obtain ⟨k, rfl⟩ : ∃ k, n = k + 1 := ⟨n - 1, by omega⟩
57          exact ⟨.ex e, l2, h2, by simp [cwhile.go, hc', hb'], hQ⟩
58        · cases b2
59          · exact absurd hQ.2 (by omega)
60          · obtain ⟨k, rfl⟩ : ∃ k, n = k + 1 := ⟨n - 1, by omega⟩
61            exact ⟨.brk, l2, h2, by simp [cwhile.go, hc', hb'], hQ⟩
62    | succ m ih =>
63      intro n l h hI hm hn
64      obtain ⟨n, rfl⟩ : ∃ k, n = k + 1 := ⟨n - 1, by omega⟩
65      obtain ⟨l1, h1, b, hc, hT, hF⟩ := hstep l h hI
66      have hc' : (StateT.run (ExceptT.run cond) l) h = .ok ((.ok b, l1), h1) := hc
67      cases b
68      · exact ⟨.go, l1, h1, by simp [cwhile.go, hc'], hF rfl⟩
69      · obtain ⟨r, l2, h2, hb, hQ⟩ := hT rfl
70        have hb' : (StateT.run (ExceptT.run body) l1) h1 = .ok ((r, l2), h2) := hb
71        rcases r with e | b2
72        · obtain ⟨k, rfl⟩ : ∃ k, n = k + 1 := ⟨n - 1, by omega⟩
73          exact ⟨.ex e, l2, h2, by simp [cwhile.go, hc', hb'], hQ⟩
74        · cases b2
75          · obtain ⟨r', l', h', hr, hq⟩ := ih n l2 h2 hQ.1 (by have := hQ.2; omega) (by omega)
76            exact ⟨r', l', h', by simp [cwhile.go, hc', hb', hr], hq⟩
77          · obtain ⟨k, rfl⟩ : ∃ k, n = k + 1 := ⟨n - 1, by omega⟩
78            exact ⟨.brk, l2, h2, by simp [cwhile.go, hc', hb'], hQ⟩
79  obtain ⟨r, l', h', hr, hq⟩ := key (μ l h) fuel l h hI (Nat.le_refl _) hμ
80  have hrun : runX (xwhileBrk cond body) l h = .ok ((Stop.toE r, l'), h') := by
81    unfold xwhileBrk runX
82    simp only [ExceptT.run, StateT.run, ExceptT.mk, cwhile, bind_app] at hr ⊢
83    erw [hr]
84    cases r <;> rfl
85  rcases r with _ | _ | e
86  · exact ⟨_, l', h', hrun, hq⟩
87  · exact ⟨_, l', h', hrun, hq⟩
88  · exact ⟨_, l', h', hrun, hq⟩
89
90end Zlib.Infback.Proofs