inflate.c.xloop-rank.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
3namespace Zlib.Inflate.Proofs
4open C Zlib.Inflate
5set_option autoImplicit false
6
7/-- A mode loop may advance a heap-resident counter by several units.
8Only a strict decrease is required. The two extra fuel units cover the
9terminal condition test after break or an exception from the body. -/
10theorem xwhileBrk_rank {cond : X Bool} {body : X Bool}
11    (P : IL → Heap → Prop) (rank : IL → Heap → Nat)
12    (Q : Except Ex Unit → IL → Heap → Prop)
13    (step : ∀ l h, P l h → ∃ test l1 h1,
14      runX cond l h = .ok ((test, l1), h1) ∧
15      (match test with
16       | .error fault => Q (.error fault) l1 h1
17       | .ok false => Q (.ok ()) l1 h1
18       | .ok true => ∃ result l2 h2,
19           runX body l1 h1 = .ok ((result, l2), h2) ∧
20           (match result with
21            | .error fault => Q (.error fault) l2 h2
22            | .ok true => Q (.ok ()) l2 h2
23            | .ok false => P l2 h2 ∧ rank l2 h2 < rank l h)))
24    {l : IL} {h : Heap} (initial : P l h) (budget : rank l h + 2 < fuel) :
25    ∃ result regs after, runX (xwhileBrk cond body) l h = .ok ((result, regs), after) ∧
26      Q result regs after := by
27  let loopCond := fun (locals : IL × Stop) => match locals.2 with
28    | .go => do
29      let (result, regs) ← StateT.run (ExceptT.run cond) locals.1
30      pure (match result with
31        | .ok value => (value, (regs, Stop.go))
32        | .error fault => (false, (regs, Stop.ex fault)))
33    | status => pure (false, (locals.1, status))
34  let loopBody := fun (locals : IL × Stop) => do
35    let (result, regs) ← StateT.run (ExceptT.run body) locals.1
36    pure (match result with
37      | .ok value => (regs, if value then Stop.brk else Stop.go)
38      | .error fault => (regs, Stop.ex fault))
39  have key : ∀ k n current heap, P current heap → rank current heap ≤ k → k + 2 < n →
40      ∃ status regs after,
41        cwhile.go loopCond loopBody n (current, Stop.go) heap = .ok ((regs, status), after) ∧
42        Q (Stop.toE status) regs after := by
43    intro k
44    induction k using Nat.strongRecOn with
45    | _ k ih =>
46      intro n current heap inv bound gas
47      obtain ⟨n, nEq⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
48      subst nEq
49      obtain ⟨test, regs1, heap1, condRun, post⟩ := step current heap inv
50      have condC : (StateT.run (ExceptT.run cond) current) heap = .ok ((test, regs1), heap1) := condRun
51      cases test with
52      | error fault =>
53        exact ⟨.ex fault, regs1, heap1, by simp [cwhile.go, loopCond, condC], post⟩
54      | ok decision =>
55        cases decision with
56        | false =>
57          exact ⟨.go, regs1, heap1, by simp [cwhile.go, loopCond, condC], post⟩
58        | true =>
59          obtain ⟨result, regs2, heap2, bodyRun, bodyPost⟩ := post
60          have bodyC : (StateT.run (ExceptT.run body) regs1) heap1 = .ok ((result, regs2), heap2) := bodyRun
61          cases result with
62          | error fault =>
63            obtain ⟨m, mEq⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
64            subst mEq
65            exact ⟨.ex fault, regs2, heap2,
66              by simp [cwhile.go, loopCond, loopBody, condC, bodyC], bodyPost⟩
67          | ok decision =>
68            cases decision with
69            | false =>
70              obtain ⟨nextInv, decreases⟩ := bodyPost
71              obtain ⟨status, regs, after, run, post⟩ :=
72                ih (rank regs2 heap2) (by omega) n regs2 heap2 nextInv (Nat.le_refl _) (by omega)
73              exact ⟨status, regs, after,
74                by simpa [cwhile.go, loopCond, loopBody, condC, bodyC] using run, post⟩
75            | true =>
76              obtain ⟨m, mEq⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
77              subst mEq
78              exact ⟨.brk, regs2, heap2,
79                by simp [cwhile.go, loopCond, loopBody, condC, bodyC], bodyPost⟩
80  obtain ⟨status, regs, after, run, post⟩ :=
81    key (rank l h) fuel l h initial (Nat.le_refl _) budget
82  refine ⟨Stop.toE status, regs, after, ?_, post⟩
83  unfold xwhileBrk runX
84  simp only [ExceptT.run, StateT.run, ExceptT.mk, cwhile, bind_app]
85  dsimp only [loopCond, loopBody] at run
86  erw [run]
87  cases status <;> rfl
88
89end Zlib.Inflate.Proofs