feat(compiler): prove exact peak stack demand
3 files changed, +38 −2
- src/Compiler.thy modified +31 −0
- src/Examples.thy modified +5 −0
- src/Frontend.thy modified +2 −2
src/Compiler.thy modified
| @@ -179,6 +179,37 @@ next | ||
| 179 | 179 | then show ?case by (simp add: check_append list_all_iff) |
| 180 | 180 | qed |
| 181 | 181 | |
| 182 | +theorem compiled_demand: | |
| 183 | + assumes "scoped (length slots) e" "list_all (\<lambda>i. i < n) slots" | |
| 184 | + shows "bounded limit (compile e slots) n \<longleftrightarrow> n + demand e \<le> limit" | |
| 185 | + using assms | |
| 186 | +proof (induction e arbitrary: slots n) | |
| 187 | + case (Literal v) | |
| 188 | + then show ?case by auto | |
| 189 | +next | |
| 190 | + case (Input i) | |
| 191 | + then show ?case by auto | |
| 192 | +next | |
| 193 | + case (Variable i) | |
| 194 | + then show ?case by (auto simp: list_all_length) | |
| 195 | +next | |
| 196 | + case (Binary op a b) | |
| 197 | + then show ?case using demand_positive[of a] demand_positive[of b] | |
| 198 | + by (auto simp: bounded_append compiled_height list_all_iff max_def; arith) | |
| 199 | +next | |
| 200 | + case (Cond c a b) | |
| 201 | + then show ?case using demand_positive[of c] demand_positive[of a] demand_positive[of b] | |
| 202 | + by (auto simp: bounded_append compiled_height list_all_iff max_def; arith) | |
| 203 | +next | |
| 204 | + case (Let a b) | |
| 205 | + then show ?case using demand_positive[of a] demand_positive[of b] | |
| 206 | + by (auto simp: bounded_append compiled_height list_all_iff max_def; arith) | |
| 207 | +qed | |
| 208 | + | |
| 209 | +corollary closed_demand: | |
| 210 | + "scoped 0 e \<Longrightarrow> bounded limit (compile e []) 0 \<longleftrightarrow> demand e \<le> limit" | |
| 211 | + using compiled_demand[where slots="[]" and n=0] by simp | |
| 212 | + | |
| 182 | 213 | fun snapshots :: "(input \<Rightarrow> pixel) \<Rightarrow> instruction list \<Rightarrow> pixel list \<Rightarrow> (pixel list list) option" where |
| 183 | 214 | "snapshots inputs [] s = Some [s]" |
| 184 | 215 | | "snapshots inputs (i # code) s = Option.bind (step inputs i s) |
src/Examples.thy modified
| @@ -51,6 +51,11 @@ lemma equal_branches: | ||
| 51 | 51 | "optimise (Cond (Input T) (Input X) (Input X)) = Input X" |
| 52 | 52 | by eval |
| 53 | 53 | |
| 54 | +lemma stack_bound_tight: | |
| 55 | + "bounded 2 (compile (Binary Add (Input X) (Input Y)) []) 0 \<and> | |
| 56 | + \<not> bounded 1 (compile (Binary Add (Input X) (Input Y)) []) 0" | |
| 57 | + by eval | |
| 58 | + | |
| 54 | 59 | lemma literal_code: |
| 55 | 60 | "executable (Literal 42) = [72,184,42,0,0,0,0,0,0,0,80,88,195]" |
| 56 | 61 | by eval |
src/Frontend.thy modified
| @@ -63,7 +63,7 @@ definition prepare :: "string \<Rightarrow> expression option" where | ||
| 63 | 63 | Option.bind (parse 128 [] (lex s [] [])) (\<lambda>(e,rest). |
| 64 | 64 | if rest = [] \<and> scoped 0 e \<and> nodes e \<le> 4096 then |
| 65 | 65 | let code = compile (optimise e) [] in |
| 66 | - if check code 0 = Some 1 \<and> bounded 512 code 0 \<and> list_all encodable (native code) | |
| 66 | + if check code 0 = Some 1 \<and> demand (optimise e) \<le> 512 \<and> list_all encodable (native code) | |
| 67 | 67 | then Some e else None else None))" |
| 68 | 68 | |
| 69 | 69 | lemma prepare_scoped: "prepare s = Some e \<Longrightarrow> scoped 0 e" |
| @@ -71,7 +71,7 @@ lemma prepare_scoped: "prepare s = Some e \<Longrightarrow> scoped 0 e" | ||
| 71 | 71 | |
| 72 | 72 | lemma prepare_bounded: |
| 73 | 73 | "prepare s = Some e \<Longrightarrow> bounded 512 (compile (optimise e) []) 0" |
| 74 | - by (auto simp: prepare_def Let_def split: if_splits bind_splits prod.splits) | |
| 74 | + by (auto simp: prepare_def Let_def closed_demand optimise_scoped split: if_splits bind_splits prod.splits) | |
| 75 | 75 | |
| 76 | 76 | lemma prepare_encodable: |
| 77 | 77 | "prepare s = Some e \<Longrightarrow> list_all encodable (native (compile (optimise e) []))" |