inflate.c.main.xloop.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.bits»
2
3/-!
4# inflate.c: running the modes' monad `X`
5
6`runX x l h` runs a mode body `x : X α` from registers `l` on heap `h`. `xwhileBrk_run` is the proof rule for the loops of the
7modes (`while`, `for (;;)`, with `break`, `goto inf_leave` and `return` as exceptions).
8-/
9
10namespace Zlib.Inflate.Proofs
11open C Zlib.Inflate
12
13/-- Run a mode body: the outcome (a value or the way out) with the registers, and the heap. -/
14def runX {α : Type} (x : X α) (l : IL) : M (Except Ex α × IL) := StateT.run (ExceptT.run x) l
15
16theorem runX_pure {α : Type} (a : α) (l : IL) (h : Heap) : runX (pure a : X α) l h = .ok ((.ok a, l), h) := rfl
17
18theorem runX_bind {α β : Type} (x : X α) (f : α → X β) (l : IL) (h : Heap) :
19    runX (x >>= f) l h = match runX x l h with
20      | .ok ((.ok a, l1), h1) => runX (f a) l1 h1
21      | .ok ((.error e, l1), h1) => .ok ((.error e, l1), h1)
22      | .error e => .error e := by
23  unfold runX
24  simp only [ExceptT.run, StateT.run, bind, ExceptT.bind, ExceptT.mk, StateT.bind, ExceptT.bindCont]
25  generalize x l h = r
26  rcases r with e | ⟨⟨r, l1⟩, h1⟩
27  · rfl
28  · cases r <;> rfl
29
30/-- The way out of a loop. -/
31def Stop.toE : Stop → Except Ex Unit
32  | .ex e => .error e
33  | _ => .ok ()
34
35/-- The loop rule. `P k l h`: exactly `k` more iterations remain; `Q` is the way out. -/
36theorem xwhileBrk_run {cond : X Bool} {body : X Bool}
37    (P : Nat → IL → Heap → Prop) (Q : Except Ex Unit → IL → Heap → Prop)
38    (hstep : ∀ k l h, P (k + 1) l h → ∃ l1 h1, runX cond l h = .ok ((.ok true, l1), h1) ∧
39      ∃ r l2 h2, runX body l1 h1 = .ok ((r, l2), h2) ∧
40        (match r with
41          | .ok true => Q (.ok ()) l2 h2
42          | .ok false => P k l2 h2
43          | .error e => Q (.error e) l2 h2))
44    (hstop : ∀ l h, P 0 l h → ∃ l1 h1, runX cond l h = .ok ((.ok false, l1), h1) ∧ Q (.ok ()) l1 h1)
45    {k : Nat} {l : IL} {h : Heap} (hP : P k l h) (hk : k < fuel) :
46    ∃ r l' h', runX (xwhileBrk cond body) l h = .ok ((r, l'), h') ∧ Q r l' h' := by
47  have key : ∀ k n l h, P k l h → k < n →
48      ∃ r l' h', (cwhile.go (σ := IL × Stop)
49        (fun (l, s) => match s with
50          | .go => do
51            let (r, l') ← StateT.run (ExceptT.run cond) l
52            pure (match r with
53              | .ok b => (b, (l', Stop.go))
54              | .error e => (false, (l', Stop.ex e)))
55          | s => pure (false, (l, s)))
56        (fun (l, _) => do
57          let (r, l') ← StateT.run (ExceptT.run body) l
58          pure (match r with
59            | .ok b => (l', if b then Stop.brk else Stop.go)
60            | .error e => (l', Stop.ex e))) n (l, Stop.go)) h = .ok ((l', r), h') ∧
61        (match r with
62         | .ex e => Q (.error e) l' h'
63         | _ => Q (.ok ()) l' h') := by
64    intro k
65    induction k with
66    | zero =>
67      intro n l h hP hn
68      obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
69      obtain ⟨l1, h1, hc, hQ⟩ := hstop l h hP
70      refine ⟨.go, l1, h1, ?_, hQ⟩
71      have hc' : (StateT.run (ExceptT.run cond) l) h = .ok ((.ok false, l1), h1) := hc
72      simp [cwhile.go, hc']
73    | succ k ih =>
74      intro n l h hP hn
75      obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
76      obtain ⟨l1, h1, hc, r, l2, h2, hb, hQ⟩ := hstep k l h hP
77      have hc' : (StateT.run (ExceptT.run cond) l) h = .ok ((.ok true, l1), h1) := hc
78      have hb' : (StateT.run (ExceptT.run body) l1) h1 = .ok ((r, l2), h2) := hb
79      rcases r with e | b
80      · refine ⟨.ex e, l2, h2, ?_, hQ⟩
81        obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
82        simp [cwhile.go, hc', hb']
83      · cases b
84        · obtain ⟨r', l', h', hr, hq⟩ := ih n l2 h2 hQ (by omega)
85          exact ⟨r', l', h', by simp [cwhile.go, hc', hb', hr], hq⟩
86        · refine ⟨.brk, l2, h2, ?_, hQ⟩
87          obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
88          simp [cwhile.go, hc', hb']
89  obtain ⟨r, l', h', hr, hq⟩ := key k fuel l h hP hk
90  have hrun : runX (xwhileBrk cond body) l h =
91      .ok ((Stop.toE r, l'), h') := by
92    unfold xwhileBrk runX
93    simp only [ExceptT.run, StateT.run, ExceptT.mk, cwhile, bind_app] at hr ⊢
94    erw [hr]
95    cases r <;> rfl
96  rcases r with _ | _ | e
97  · exact ⟨_, l', h', hrun, hq⟩
98  · exact ⟨_, l', h', hrun, hq⟩
99  · exact ⟨_, l', h', hrun, hq⟩
100
101end Zlib.Inflate.Proofs