From 72b2edbe209a48353896277c3695fd72e27facac Mon Sep 17 00:00:00 2001
From: james <j@cpl0.zip>
Date: Sun, 13 Sep 2026 12:00:00 +0100
Subject: [PATCH] feat(compiler): prove exact peak stack demand

---
 src/Compiler.thy | 31 +++++++++++++++++++++++++++++++
 src/Examples.thy |  5 +++++
 src/Frontend.thy |  4 ++--
 3 files changed, 38 insertions(+), 2 deletions(-)

diff --git a/src/Compiler.thy b/src/Compiler.thy
index ba6cbb3..d21aa0e 100644
--- a/src/Compiler.thy
+++ b/src/Compiler.thy
@@ -179,6 +179,37 @@ next
   then show ?case by (simp add: check_append list_all_iff)
 qed
 
+theorem compiled_demand:
+  assumes "scoped (length slots) e" "list_all (\<lambda>i. i < n) slots"
+  shows "bounded limit (compile e slots) n \<longleftrightarrow> n + demand e \<le> limit"
+  using assms
+proof (induction e arbitrary: slots n)
+  case (Literal v)
+  then show ?case by auto
+next
+  case (Input i)
+  then show ?case by auto
+next
+  case (Variable i)
+  then show ?case by (auto simp: list_all_length)
+next
+  case (Binary op a b)
+  then show ?case using demand_positive[of a] demand_positive[of b]
+    by (auto simp: bounded_append compiled_height list_all_iff max_def; arith)
+next
+  case (Cond c a b)
+  then show ?case using demand_positive[of c] demand_positive[of a] demand_positive[of b]
+    by (auto simp: bounded_append compiled_height list_all_iff max_def; arith)
+next
+  case (Let a b)
+  then show ?case using demand_positive[of a] demand_positive[of b]
+    by (auto simp: bounded_append compiled_height list_all_iff max_def; arith)
+qed
+
+corollary closed_demand:
+  "scoped 0 e \<Longrightarrow> bounded limit (compile e []) 0 \<longleftrightarrow> demand e \<le> limit"
+  using compiled_demand[where slots="[]" and n=0] by simp
+
 fun snapshots :: "(input \<Rightarrow> pixel) \<Rightarrow> instruction list \<Rightarrow> pixel list \<Rightarrow> (pixel list list) option" where
   "snapshots inputs [] s = Some [s]"
 | "snapshots inputs (i # code) s = Option.bind (step inputs i s)
diff --git a/src/Examples.thy b/src/Examples.thy
index 3b42376..3a9cea3 100644
--- a/src/Examples.thy
+++ b/src/Examples.thy
@@ -51,6 +51,11 @@ lemma equal_branches:
   "optimise (Cond (Input T) (Input X) (Input X)) = Input X"
   by eval
 
+lemma stack_bound_tight:
+  "bounded 2 (compile (Binary Add (Input X) (Input Y)) []) 0 \<and>
+    \<not> bounded 1 (compile (Binary Add (Input X) (Input Y)) []) 0"
+  by eval
+
 lemma literal_code:
   "executable (Literal 42) = [72,184,42,0,0,0,0,0,0,0,80,88,195]"
   by eval
diff --git a/src/Frontend.thy b/src/Frontend.thy
index 274cd77..a404b02 100644
--- a/src/Frontend.thy
+++ b/src/Frontend.thy
@@ -63,7 +63,7 @@ definition prepare :: "string \<Rightarrow> expression option" where
     Option.bind (parse 128 [] (lex s [] [])) (\<lambda>(e,rest).
       if rest = [] \<and> scoped 0 e \<and> nodes e \<le> 4096 then
         let code = compile (optimise e) [] in
-        if check code 0 = Some 1 \<and> bounded 512 code 0 \<and> list_all encodable (native code)
+        if check code 0 = Some 1 \<and> demand (optimise e) \<le> 512 \<and> list_all encodable (native code)
         then Some e else None else None))"
 
 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"
 
 lemma prepare_bounded:
   "prepare s = Some e \<Longrightarrow> bounded 512 (compile (optimise e) []) 0"
-  by (auto simp: prepare_def Let_def split: if_splits bind_splits prod.splits)
+  by (auto simp: prepare_def Let_def closed_demand optimise_scoped split: if_splits bind_splits prod.splits)
 
 lemma prepare_encodable:
   "prepare s = Some e \<Longrightarrow> list_all encodable (native (compile (optimise e) []))"