From dd6b9d1661bbb14e3dfa70ecdba2d25593e72eb8 Mon Sep 17 00:00:00 2001
From: james <j@cpl0.zip>
Date: Sat, 31 Oct 2026 10:55:00 +0000
Subject: [PATCH] perf(frontend): use verified tail recursive parsing and
 resolution

---
 src/Frontend.thy | 39 +++++++++++++++++++++++++++++++++++++++
 tests/cli.py     |  3 +++
 2 files changed, 42 insertions(+)

diff --git a/src/Frontend.thy b/src/Frontend.thy
index c96b2db..7b96a08 100644
--- a/src/Frontend.thy
+++ b/src/Frontend.thy
@@ -8,6 +8,9 @@ fun bind :: "'a result \<Rightarrow> ('a \<Rightarrow> 'b result) \<Rightarrow>
   "bind (Error e) f = Error e"
 | "bind (Ok x) f = f x"
 
+lemma bind_assoc: "bind (bind r f) g = bind r (\<lambda>x. bind (f x) g)"
+  by (cases r) auto
+
 function decimal :: "nat \<Rightarrow> string" where
   "decimal n = (if n < 10 then [char_of_nat (48 + n)] else decimal (n div 10) @ [char_of_nat (48 + n mod 10)])"
   by pat_completeness auto
@@ -47,6 +50,20 @@ fun parse_lines :: "nat \<Rightarrow> string list \<Rightarrow> statement list r
 | "parse_lines n (s # ss) = bind (parse_line n (words s)) (\<lambda>xs.
     bind (parse_lines (Suc n) ss) (\<lambda>ys. Ok (xs @ ys)))"
 
+fun parse_acc :: "nat \<Rightarrow> string list \<Rightarrow> statement list \<Rightarrow> statement list result" where
+  "parse_acc n [] acc = Ok (rev acc)"
+| "parse_acc n (s # ss) acc = (case parse_line n (words s) of Error e \<Rightarrow> Error e
+    | Ok xs \<Rightarrow> parse_acc (Suc n) ss (rev xs @ acc))"
+
+lemma parse_acc_correct:
+  "parse_acc n ss acc = bind (parse_lines n ss) (\<lambda>xs. Ok (rev acc @ xs))"
+  by (induction ss arbitrary: n acc) (auto simp: bind_assoc split: result.splits)
+
+declare parse_lines.simps [code drop]
+
+lemma parse_lines_code [code]: "parse_lines n ss = parse_acc n ss []"
+  by (cases "parse_lines n ss") (simp_all add: parse_acc_correct)
+
 fun count :: "statement \<Rightarrow> nat" where
   "count (Label l) = 0"
 | "count (Emit op) = 1"
@@ -73,6 +90,28 @@ fun resolve_all :: "(string \<times> nat) list \<Rightarrow> statement list \<Ri
     bind (resolve_all env ss) (\<lambda>xs. Ok (x # xs)))"
 | "resolve_all env (Pad n # ss) = bind (resolve_all env ss) (\<lambda>xs. Ok (replicate n Nop @ xs))"
 
+fun resolve_acc :: "(string \<times> nat) list \<Rightarrow> statement list \<Rightarrow> nat instruction list \<Rightarrow> nat instruction list result" where
+  "resolve_acc env [] acc = Ok (rev acc)"
+| "resolve_acc env (Label l # ss) acc = resolve_acc env ss acc"
+| "resolve_acc env (Emit op # ss) acc = (case resolve env op of Error e \<Rightarrow> Error e
+    | Ok x \<Rightarrow> resolve_acc env ss (x # acc))"
+| "resolve_acc env (Pad n # ss) acc = resolve_acc env ss (replicate n Nop @ acc)"
+
+lemma resolve_acc_correct:
+  "resolve_acc env ss acc = bind (resolve_all env ss) (\<lambda>xs. Ok (rev acc @ xs))"
+proof (induction ss arbitrary: acc)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons s ss)
+  then show ?case by (cases s) (auto simp: bind_assoc split: result.splits)
+qed
+
+declare resolve_all.simps [code drop]
+
+lemma resolve_all_code [code]: "resolve_all env ss = resolve_acc env ss []"
+  by (cases "resolve_all env ss") (simp_all add: resolve_acc_correct)
+
 definition source :: "string \<Rightarrow> nat instruction list result" where
   "source s = (if \<not> list_all (\<lambda>c. let n = nat_of_char c in
       n = 9 \<or> n = 10 \<or> n = 13 \<or> (32 \<le> n \<and> n < 127)) s
diff --git a/tests/cli.py b/tests/cli.py
index b20c821..52a758e 100644
--- a/tests/cli.py
+++ b/tests/cli.py
@@ -122,6 +122,9 @@ def main():
     ]:
         check(message in cli("assemble", "-", text=text, ok=False), message)
     check("16-bit range" in cli("assemble", "examples/overflow.span", ok=False), "overflow accepted")
+    check("65536 instructions, 65536 bytes" in cli("assemble", "-", text="nop\n" * 65536), "maximum line count")
+    check("invalid instruction at line 4097" in cli("assemble", "-", text="nop\n" * 4096 + "invalid\npad -1", ok=False), "first parse error changed")
+    check("undefined label first" in cli("assemble", "-", text="pad 3\njmp first\njmp second", ok=False), "first resolution error changed")
     for padding, width in [(127, 2), (128, 3), (32767, 3)]:
         report = cli("assemble", "-", text=f"jmp end\npad {padding}\nlabel end\nhalt")
         check(f"{padding + width + 1} bytes" in report, "forward range boundary")