From de502ca765320a4ac82d4bce88e01936c82bc498 Mon Sep 17 00:00:00 2001
From: james <j@cpl0.zip>
Date: Sat, 31 Oct 2026 11:55:00 +0000
Subject: [PATCH] perf(cli): compile binary output and assembly report once

---
 cli/driver.ML    |  7 +++----
 src/Export.thy   |  2 +-
 src/Frontend.thy | 11 +++++++++++
 tests/cli.py     |  8 ++++++--
 4 files changed, 21 insertions(+), 7 deletions(-)

diff --git a/cli/driver.ML b/cli/driver.ML
index 8d724a6f04f51b9ebbcd1ace039c49d9ea9312dc..414345364e952f16a8598f904aa831d4ff4e51b0 100644
--- a/cli/driver.ML
+++ b/cli/driver.ML
@@ -35,13 +35,12 @@ fun run args =
   | ["disassemble", file] => output (Span.disassemble (chars (read file)))
   | ["assemble", file, "-o", destination] =>
       let
-        val input = chars (read file)
-        val (ok, bytes) = Span.binary input
+        val ((ok, bytes), report) = Span.artifact (chars (read file))
       in
         if ok then
           (write destination (text bytes);
-           output (Span.process [chars "assemble"] input))
-        else output (false, bytes)
+           output (true, report))
+        else output (false, report)
       end
   | ["run", file] => output (Span.process (map chars ["run", "4096"]) (chars (read file)))
   | ["run", file, fuel] => output (Span.process (map chars ["run", fuel]) (chars (read file)))
diff --git a/src/Export.thy b/src/Export.thy
index 01fd65a1cb29dfd426d80fde9865f9fd80475ac5..7d7ffe0d127a4463852b20fec30dab474af922d6 100644
--- a/src/Export.thy
+++ b/src/Export.thy
@@ -6,6 +6,6 @@ definition ascii :: "integer \<Rightarrow> char" where "ascii = char_of"
 
 definition ordinal :: "char \<Rightarrow> integer" where "ordinal = of_char"
 
-export_code process binary disassemble ascii ordinal in SML module_name Span file_prefix span
+export_code process binary artifact disassemble ascii ordinal in SML module_name Span file_prefix span
 
 end
diff --git a/src/Frontend.thy b/src/Frontend.thy
index 7b96a083937eec815d218dec99e57d37994c24aa..4faedf6a5fc7dfb96f7da71b4bb888808b1a9a9e 100644
--- a/src/Frontend.thy
+++ b/src/Frontend.thy
@@ -237,4 +237,15 @@ definition process :: "string list \<Rightarrow> string \<Rightarrow> bool \<tim
     case checked p of Error e \<Rightarrow> (False, (if args = [''trace''] then trace p else []) @ e @ newline)
     | Ok bs \<Rightarrow> inspect args p bs)"
 
+definition artifact :: "string \<Rightarrow> (bool \<times> string) \<times> string" where
+  "artifact s = (case source s of Error e \<Rightarrow> ((False, e @ newline), e @ newline)
+    | Ok p \<Rightarrow> case checked p of Error e \<Rightarrow> ((False, e @ newline), e @ newline)
+    | Ok bs \<Rightarrow> ((True, map char_of_nat bs), summary p bs @ hex bs @ newline))"
+
+theorem artifact_binary: "fst (artifact s) = binary s"
+  by (auto simp: artifact_def binary_def compile_def split: result.splits)
+
+theorem artifact_report: "(fst (fst (artifact s)), snd (artifact s)) = process [''assemble''] s"
+  by (auto simp: artifact_def process_def inspect_def Let_def split: result.splits)
+
 end
diff --git a/tests/cli.py b/tests/cli.py
index 52a758ef4a6bc7748f2ce6956c6c90c7be3e2dd6..01ca990baf701dbd6bf305f936a40236a90e458e 100644
--- a/tests/cli.py
+++ b/tests/cli.py
@@ -148,7 +148,8 @@ def main():
             expected = rows[pc][0] if pc < length else len(out.read_bytes())
             report = cli("run", "-", "256", text=text)
             check(f"pc={expected}  acc={acc}\n" in report, f"execution mismatch in case {case}")
-        cli("assemble", "examples/countdown.span", "-o", out)
+        report = cli("assemble", "examples/countdown.span", "-o", out)
+        check(report == cli("assemble", "examples/countdown.span"), "binary report changed")
         check(out.read_bytes() == bytes([1, 1, 1, 2, 17, 130, 16, 123, 3]), "binary output")
         check("jmp.8 -5" in cli("disassemble", out), "binary disassembly")
         out.write_bytes(bytes([18, 0]))
@@ -156,8 +157,11 @@ def main():
         out.write_bytes(bytes([255]))
         check("invalid encoding" in cli("disassemble", out, ok=False), "unknown opcode accepted")
         out.write_bytes(b"preserve")
-        cli("assemble", "-", "-o", out, text="jmp missing", ok=False)
+        error = cli("assemble", "-", "-o", out, text="jmp missing", ok=False)
+        check(error == cli("assemble", "-", text="jmp missing", ok=False), "binary error changed")
         check(out.read_bytes() == b"preserve", "failed assembly clobbered output")
+        cli("assemble", "-", "-o", out, text="")
+        check(out.read_bytes() == b"", "empty binary output")
     print(f"{CHECKS} checks passed, including 36 exhaustive layout comparisons")