4 files changed, 21 insertions(+), 7 deletions(-)

M cli/driver.ML
M src/Export.thy
M src/Frontend.thy
M tests/cli.py

@@ 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)))

@@ 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

@@ 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

@@ 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")