Monad.lean

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

1import ZlibF.Runtime.Schema
2
3/-!
4# Runtime: the monad, faults and loops
5
6Trusted base of every translation; see `docs/trusted-base.md`.
7
8A C computation takes the heap and returns a value and the new heap, or a fault. Every undefined behaviour
9the translation can reach is `Fault.ub`. Unsigned arithmetic wraps and signed arithmetic is checked in the
10translation itself, not here.
11
12The rules at the end (`bind_app`, `OkOn`, the loop rules) are for proofs. They are theorems, not part of the
13trusted definitions.
14-/
15
16namespace C
17
18/-- Why a C computation did not produce a value. -/
19inductive Fault where
20  /-- undefined behaviour, with a short reason -/
21  | ub (what : String)
22  /-- a loop used up its fuel (a termination theorem rules this out) -/
23  | outOfFuel
24  deriving Repr, DecidableEq, Inhabited
25
26/-- A C computation: the heap in, a value and the heap out, or a fault. -/
27def M (α : Type) : Type := Heap → Except Fault (α × Heap)
28
29instance : Monad M where
30  pure a := fun h => .ok (a, h)
31  bind m f := fun h => match m h with
32    | .ok (a, h') => f a h'
33    | .error e => .error e
34
35/-- Undefined behaviour. -/
36def ub {α : Type} (what : String) : M α := fun _ => .error (.ub what)
37
38/-- Run a computation on a heap. -/
39def run {α : Type} (m : M α) (h : Heap) : Except Fault (α × Heap) := m h
40
41/-- Loop fuel. Large enough that no zlib loop over in-memory data can exhaust it. -/
42def fuel : Nat := 2 ^ 64
43
44/-- `while (cond) body` over the loop-carried locals `σ`. The condition may update them (`while (len--)`):
45its update happens on every evaluation, including the last, false one, as in C. -/
46def cwhile {σ : Type} (cond : σ → M (Bool × σ)) (body : σ → M σ) (s : σ) : M σ :=
47  go fuel s
48where
49  go : Nat → σ → M σ
50    | 0, _ => fun _ => .error .outOfFuel
51    | n + 1, s => do
52      let (c, s) ← cond s
53      if c then go n (← body s) else pure s
54
55/-- `do body while (cond)` over the loop-carried locals `σ`. -/
56def cdoWhile {σ : Type} (body : σ → M σ) (cond : σ → M (Bool × σ)) (s : σ) : M σ :=
57  go fuel s
58where
59  go : Nat → σ → M σ
60    | 0, _ => fun _ => .error .outOfFuel
61    | n + 1, s => do
62      let s ← body s
63      let (c, s) ← cond s
64      if c then go n s else pure s
65
66/-! ## Rules for proofs -/
67
68@[simp] theorem bind_app {α β : Type} (m : M α) (f : α → M β) (h : Heap) :
69    (m >>= f) h = match m h with | .ok (a, h') => f a h' | .error e => .error e := rfl
70@[simp] theorem pure_app {α : Type} (a : α) (h : Heap) : (pure a : M α) h = .ok (a, h) := rfl
71
72theorem bind_ok {α β : Type} {m : M α} {f : α → M β} {h h1 : Heap} {a : α} (e : m h = .ok (a, h1)) :
73    (m >>= f) h = f a h1 := by simp [e]
74
75/-- `m` returns `x` on heap `h` and leaves the heap unchanged (read-only code such as checksums). -/
76def OkOn {α : Type} (h : Heap) (m : M α) (x : α) : Prop := m h = .ok (x, h)
77
78theorem OkOn.pure {α : Type} (h : Heap) (x : α) : OkOn h (Pure.pure x : M α) x := rfl
79
80theorem OkOn.bind {α β : Type} {h : Heap} {m : M α} {f : α → M β} {x : α} {y : β}
81    (hm : OkOn h m x) (hf : OkOn h (f x) y) : OkOn h (m >>= f) y := by
82  unfold OkOn at *
83  rw [bind_app, hm]
84  exact hf
85
86theorem OkOn.bind_ex {α β : Type} {h : Heap} {m : M α} {f : α → M β} {R : α → Prop} {T : β → Prop}
87    (hm : ∃ x, OkOn h m x ∧ R x) (hf : ∀ x, R x → ∃ y, OkOn h (f x) y ∧ T y) :
88    ∃ y, OkOn h (m >>= f) y ∧ T y := by
89  obtain ⟨x, hx, hR⟩ := hm
90  obtain ⟨y, hy, hT⟩ := hf x hR
91  exact ⟨y, OkOn.bind hx hy, hT⟩
92
93theorem OkOn.bind_ex_pure {α : Type} {h : Heap} {m : M α} {x : α} (hm : OkOn h m x) :
94    ∃ y, OkOn h m y ∧ y = x := ⟨x, hm, rfl⟩
95
96/-- `while` rule. `P k s`: exactly `k` more iterations remain from state `s`. -/
97theorem cwhile_go_ok {σ : Type} {h : Heap} {cond : σ → M (Bool × σ)} {body : σ → M σ}
98    (P : Nat → σ → Prop) (Q : σ → Prop)
99    (hstep : ∀ k s, P (k + 1) s → ∃ s1 s2, OkOn h (cond s) (true, s1) ∧ OkOn h (body s1) s2 ∧ P k s2)
100    (hstop : ∀ s, P 0 s → ∃ s1, OkOn h (cond s) (false, s1) ∧ Q s1) :
101    ∀ k n s, P k s → k < n → ∃ s', OkOn h (cwhile.go cond body n s) s' ∧ Q s' := by
102  intro k
103  induction k with
104  | zero =>
105    intro n s hP hn
106    obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
107    obtain ⟨s1, hc, hQ⟩ := hstop s hP
108    refine ⟨s1, ?_, hQ⟩
109    unfold OkOn at *
110    simp [cwhile.go, hc]
111  | succ k ih =>
112    intro n s hP hn
113    obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
114    obtain ⟨s1, s2, hc, hb, hP2⟩ := hstep k s hP
115    obtain ⟨s', hgo, hQ⟩ := ih n s2 hP2 (by omega)
116    refine ⟨s', ?_, hQ⟩
117    unfold OkOn at *
118    simp [cwhile.go, hc, hb, hgo]
119
120theorem cwhile_ok {σ : Type} {h : Heap} {cond : σ → M (Bool × σ)} {body : σ → M σ}
121    (P : Nat → σ → Prop) (Q : σ → Prop)
122    (hstep : ∀ k s, P (k + 1) s → ∃ s1 s2, OkOn h (cond s) (true, s1) ∧ OkOn h (body s1) s2 ∧ P k s2)
123    (hstop : ∀ s, P 0 s → ∃ s1, OkOn h (cond s) (false, s1) ∧ Q s1)
124    {k : Nat} {s : σ} (hP : P k s) (hk : k < fuel) :
125    ∃ s', OkOn h (cwhile cond body s) s' ∧ Q s' :=
126  cwhile_go_ok P Q hstep hstop k fuel s hP hk
127
128/-- `do ... while` rule. `P k s`: the body runs exactly `k + 1` more times. -/
129theorem cdoWhile_go_ok {σ : Type} {h : Heap} {body : σ → M σ} {cond : σ → M (Bool × σ)}
130    (P : Nat → σ → Prop) (Q : σ → Prop)
131    (hstep : ∀ k s, P (k + 1) s → ∃ s1 s2, OkOn h (body s) s1 ∧ OkOn h (cond s1) (true, s2) ∧ P k s2)
132    (hlast : ∀ s, P 0 s → ∃ s1 s2, OkOn h (body s) s1 ∧ OkOn h (cond s1) (false, s2) ∧ Q s2) :
133    ∀ k n s, P k s → k < n → ∃ s', OkOn h (cdoWhile.go body cond n s) s' ∧ Q s' := by
134  intro k
135  induction k with
136  | zero =>
137    intro n s hP hn
138    obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
139    obtain ⟨s1, s2, hb, hc, hQ⟩ := hlast s hP
140    refine ⟨s2, ?_, hQ⟩
141    unfold OkOn at *
142    simp [cdoWhile.go, hb, hc]
143  | succ k ih =>
144    intro n s hP hn
145    obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
146    obtain ⟨s1, s2, hb, hc, hP2⟩ := hstep k s hP
147    obtain ⟨s', hgo, hQ⟩ := ih n s2 hP2 (by omega)
148    refine ⟨s', ?_, hQ⟩
149    unfold OkOn at *
150    simp [cdoWhile.go, hb, hc, hgo]
151
152theorem cdoWhile_ok {σ : Type} {h : Heap} {body : σ → M σ} {cond : σ → M (Bool × σ)}
153    (P : Nat → σ → Prop) (Q : σ → Prop)
154    (hstep : ∀ k s, P (k + 1) s → ∃ s1 s2, OkOn h (body s) s1 ∧ OkOn h (cond s1) (true, s2) ∧ P k s2)
155    (hlast : ∀ s, P 0 s → ∃ s1 s2, OkOn h (body s) s1 ∧ OkOn h (cond s1) (false, s2) ∧ Q s2)
156    {k : Nat} {s : σ} (hP : P k s) (hk : k < fuel) :
157    ∃ s', OkOn h (cdoWhile body cond s) s' ∧ Q s' :=
158  cdoWhile_go_ok P Q hstep hlast k fuel s hP hk
159
160/-! ### Loops that change the heap
161
162The rules above are for loops that leave the heap alone. These carry the heap through the invariant:
163`P k s h` says that exactly `k` more iterations remain from the locals `s` on the heap `h`. -/
164
165theorem cwhile_go_run {σ : Type} {cond : σ → M (Bool × σ)} {body : σ → M σ}
166    (P : Nat → σ → Heap → Prop) (Q : σ → Heap → Prop)
167    (hstep : ∀ k s h, P (k + 1) s h → ∃ s1 h1 s2 h2, cond s h = .ok ((true, s1), h1) ∧ body s1 h1 = .ok (s2, h2) ∧
168      P k s2 h2)
169    (hstop : ∀ s h, P 0 s h → ∃ s1 h1, cond s h = .ok ((false, s1), h1) ∧ Q s1 h1) :
170    ∀ k n s h, P k s h → k < n → ∃ s' h', cwhile.go cond body n s h = .ok (s', h') ∧ Q s' h' := by
171  intro k
172  induction k with
173  | zero =>
174    intro n s h hP hn
175    obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
176    obtain ⟨s1, h1, hc, hQ⟩ := hstop s h hP
177    exact ⟨s1, h1, by simp [cwhile.go, hc], hQ⟩
178  | succ k ih =>
179    intro n s h hP hn
180    obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
181    obtain ⟨s1, h1, s2, h2, hc, hb, hP2⟩ := hstep k s h hP
182    obtain ⟨s', h', hgo, hQ⟩ := ih n s2 h2 hP2 (by omega)
183    exact ⟨s', h', by simp [cwhile.go, hc, hb, hgo], hQ⟩
184
185/-- `while` rule for a loop that changes the heap: if `P k s h` holds at the start, with fewer than `fuel` iterations,
186the loop ends in a state that satisfies `Q`. -/
187theorem cwhile_run {σ : Type} {cond : σ → M (Bool × σ)} {body : σ → M σ}
188    (P : Nat → σ → Heap → Prop) (Q : σ → Heap → Prop)
189    (hstep : ∀ k s h, P (k + 1) s h → ∃ s1 h1 s2 h2, cond s h = .ok ((true, s1), h1) ∧ body s1 h1 = .ok (s2, h2) ∧
190      P k s2 h2)
191    (hstop : ∀ s h, P 0 s h → ∃ s1 h1, cond s h = .ok ((false, s1), h1) ∧ Q s1 h1)
192    {k : Nat} {s : σ} {h : Heap} (hP : P k s h) (hk : k < fuel) :
193    ∃ s' h', cwhile cond body s h = .ok (s', h') ∧ Q s' h' :=
194  cwhile_go_run P Q hstep hstop k fuel s h hP hk
195
196theorem cdoWhile_go_run {σ : Type} {body : σ → M σ} {cond : σ → M (Bool × σ)}
197    (P : Nat → σ → Heap → Prop) (Q : σ → Heap → Prop)
198    (hstep : ∀ k s h, P (k + 1) s h → ∃ s1 h1 s2 h2, body s h = .ok (s1, h1) ∧ cond s1 h1 = .ok ((true, s2), h2) ∧
199      P k s2 h2)
200    (hlast : ∀ s h, P 0 s h → ∃ s1 h1 s2 h2, body s h = .ok (s1, h1) ∧ cond s1 h1 = .ok ((false, s2), h2) ∧ Q s2 h2) :
201    ∀ k n s h, P k s h → k < n → ∃ s' h', cdoWhile.go body cond n s h = .ok (s', h') ∧ Q s' h' := by
202  intro k
203  induction k with
204  | zero =>
205    intro n s h hP hn
206    obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
207    obtain ⟨s1, h1, s2, h2, hb, hc, hQ⟩ := hlast s h hP
208    exact ⟨s2, h2, by simp [cdoWhile.go, hb, hc], hQ⟩
209  | succ k ih =>
210    intro n s h hP hn
211    obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
212    obtain ⟨s1, h1, s2, h2, hb, hc, hP2⟩ := hstep k s h hP
213    obtain ⟨s', h', hgo, hQ⟩ := ih n s2 h2 hP2 (by omega)
214    exact ⟨s', h', by simp [cdoWhile.go, hb, hc, hgo], hQ⟩
215
216/-- `do ... while` rule for a loop that changes the heap: `P k s h` says that the body runs exactly `k + 1` more times. -/
217theorem cdoWhile_run {σ : Type} {body : σ → M σ} {cond : σ → M (Bool × σ)}
218    (P : Nat → σ → Heap → Prop) (Q : σ → Heap → Prop)
219    (hstep : ∀ k s h, P (k + 1) s h → ∃ s1 h1 s2 h2, body s h = .ok (s1, h1) ∧ cond s1 h1 = .ok ((true, s2), h2) ∧
220      P k s2 h2)
221    (hlast : ∀ s h, P 0 s h → ∃ s1 h1 s2 h2, body s h = .ok (s1, h1) ∧ cond s1 h1 = .ok ((false, s2), h2) ∧ Q s2 h2)
222    {k : Nat} {s : σ} {h : Heap} (hP : P k s h) (hk : k < fuel) :
223    ∃ s' h', cdoWhile body cond s h = .ok (s', h') ∧ Q s' h' :=
224  cdoWhile_go_run P Q hstep hlast k fuel s h hP hk
225
226end C