A => .gitignore +2 -0
@@ 1,2 @@
+/.build/
+__pycache__/
A => Encoding.thy +1 -0
@@ 1,1 @@
+src/Encoding.thy<
\ No newline at end of file
A => Machine.thy +1 -0
@@ 1,1 @@
+src/Machine.thy<
\ No newline at end of file
A => Makefile +18 -0
@@ 1,18 @@
+ISABELLE ?= isabelle
+
+.PHONY: all check clean
+
+all: .build/ready
+
+.build/ready: ROOT $(wildcard src/*.thy tests/*.thy) cli/driver.ML Makefile
+ @test "$$('$(ISABELLE)' version)" = Isabelle2026 || { printf '%s\n' 'span requires Isabelle2026' >&2; exit 1; }
+ "$(ISABELLE)" build -D . -j 1 -o threads=1 -o parallel_proofs=0
+ "$(ISABELLE)" export -n -d . -O .build -x 'Span.Export:code/span.ML' Span
+ SPAN_ROOT="$(CURDIR)" "$$('$(ISABELLE)' getenv -b POLYML_HOME)/$$('$(ISABELLE)' getenv -b ISABELLE_PLATFORM64)/polyc" -o .build/span cli/driver.ML
+ @touch $@
+
+check: all
+ python3 tests/cli.py
+
+clean:
+ rm -rf .build
A => README.md +13 -0
@@ 1,13 @@
+Span implements a branch relaxing assembler in Isabelle/HOL, with proofs of termination, minimum layout size and execution correspondence for a bytecode machine with signed 8-bit and 16-bit relative branches
+
+[](media/demo.mp4)
+
+## Correctness
+
+An overflowing short branch must be wide in every valid assignment. [Relaxation](Relax.thy) computes the least widening set terminating on the number of remaining short branches. A final range check decides whether any valid layout exists
+
+[Encoding](Encoding.thy) proves byte bounds and decoder inversion and [Execution correspondence](Machine.thy) relates source execution `S` and bytecode execution `B` through relocation `R` for every fuel bound (including suspended states)
+
+
+
+Minimality assumes fixed instruction order and excludes alignment directives while the machine uses a natural valued accumulator and biased little endian branch payloads. The execution theorem starts from resolved instructions and excludes the SML compiler, runtime and OS I/O
A => ROOT +15 -0
@@ 1,15 @@
+session Span in src = HOL +
+ options [document = false]
+ sessions
+ "HOL-Library"
+ directories
+ "../tests"
+ theories
+ Model
+ Layout
+ Relax
+ Encoding
+ Machine
+ Frontend
+ Examples
+ Export
A => Relax.thy +1 -0
@@ 1,1 @@
+src/Relax.thy<
\ No newline at end of file
A => cli/driver.ML +101 -0
@@ 1,101 @@
+val root = valOf (OS.Process.getEnv "SPAN_ROOT");
+val _ = use (root ^ "/.build/Span.Export/code/span.ML");
+
+fun chars s = map (Span.ascii o IntInf.fromInt o Char.ord) (String.explode s);
+fun text cs = String.implode (map (Char.chr o IntInf.toInt o Span.ordinal) cs);
+
+fun read path =
+ let
+ val fd = if path = "-" then Posix.FileSys.stdin
+ else Posix.FileSys.openf (path, Posix.FileSys.O_RDONLY, Posix.FileSys.O.flags [])
+ fun close () = if path = "-" then () else Posix.IO.close fd
+ fun loop total chunks =
+ let
+ val bytes = Posix.IO.readVec (fd, Int.min (65536, 1048577 - total))
+ val count = Word8Vector.length bytes
+ in
+ if count = 0 then String.concat (List.rev chunks)
+ else if total + count > 1048576 then raise Fail "input exceeds 1 MiB"
+ else loop (total + count) (Byte.bytesToString bytes :: chunks)
+ end
+ val input = loop 0 [] handle exn => ((close () handle _ => ()); raise exn)
+ val _ = close ()
+ in
+ input
+ end;
+
+fun write path text =
+ let
+ val bytes = Byte.stringToBytes text
+ val pid = SysWord.toString (Posix.Process.pidToWord (Posix.ProcEnv.getpid ()))
+ val prefix = OS.Path.concat (OS.Path.dir path, "." ^ OS.Path.file path ^ "." ^ pid ^ ".")
+ val defaultMode = Posix.FileSys.S.flags [Posix.FileSys.S.irusr, Posix.FileSys.S.iwusr,
+ Posix.FileSys.S.irgrp, Posix.FileSys.S.iwgrp, Posix.FileSys.S.iroth, Posix.FileSys.S.iwoth]
+ val mode = Posix.FileSys.S.intersect [Posix.FileSys.ST.mode (Posix.FileSys.stat path),
+ Posix.FileSys.S.flags [Posix.FileSys.S.irwxu, Posix.FileSys.S.irwxg, Posix.FileSys.S.irwxo]]
+ handle exn as OS.SysErr (_, SOME error) =>
+ if error = Posix.Error.noent then defaultMode else raise exn
+ fun reserve n =
+ if n = 128 then raise Fail "cannot reserve output file"
+ else
+ let
+ val temporary = prefix ^ Int.toString n
+ in
+ (temporary, Posix.FileSys.createf
+ (temporary, Posix.FileSys.O_WRONLY, Posix.FileSys.O.excl, mode))
+ end handle exn as OS.SysErr (_, SOME error) =>
+ if error = Posix.Error.exist then reserve (n + 1) else raise exn
+ val (temporary, fd) = reserve 0
+ val closed = ref false
+ fun close () = (Posix.IO.close fd; closed := true)
+ fun discard () =
+ ((if !closed then () else close ()) handle _ => ();
+ OS.FileSys.remove temporary handle _ => ())
+ fun loop offset =
+ if offset = Word8Vector.length bytes then ()
+ else
+ let
+ val count = Posix.IO.writeVec (fd, Word8VectorSlice.slice (bytes, offset, NONE))
+ in
+ if count = 0 then raise Fail "output write made no progress" else loop (offset + count)
+ end
+ in
+ (loop 0; close (); OS.FileSys.rename {old = temporary, new = path})
+ handle exn => (discard (); raise exn)
+ end;
+
+fun output (ok, message) =
+ (TextIO.output (if ok then TextIO.stdOut else TextIO.stdErr, text message);
+ OS.Process.exit (if ok then OS.Process.success else OS.Process.failure));
+
+fun usage () =
+ (TextIO.output (TextIO.stdOut,
+ "usage: span assemble file [-o binary]\n span trace file\n span list file\n span run file [fuel]\n span disassemble binary\n\nuse - to read standard input\n");
+ OS.Process.exit OS.Process.success);
+
+fun run args =
+ case args of
+ [] => usage ()
+ | ["--help"] => usage ()
+ | ["disassemble", file] => output (Span.disassemble (chars (read file)))
+ | ["assemble", file, "-o", destination] =>
+ let
+ val ((ok, bytes), report) = Span.artifact (chars (read file))
+ in
+ if ok then
+ (write destination (text 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)))
+ | [mode, file] =>
+ if List.exists (fn x => x = mode) ["assemble", "trace", "list"] then
+ output (Span.process [chars mode] (chars (read file)))
+ else raise Fail "unknown command, use span --help"
+ | _ => raise Fail "invalid arguments, use span --help";
+
+fun main () = run (CommandLine.arguments ())
+ handle exn =>
+ (TextIO.output (TextIO.stdErr, "span: " ^ General.exnMessage exn ^ "\n");
+ OS.Process.exit OS.Process.failure);
A => examples/backward.span +4 -0
@@ 1,4 @@
+label start
+pad 127
+jmp start
+halt
A => examples/cascade.span +8 -0
@@ 1,8 @@
+jmp near
+jmp far
+pad 125
+label near
+nop
+pad 2
+label far
+halt
A => examples/countdown.span +9 -0
@@ 1,9 @@
+inc
+inc
+inc
+label loop
+dec
+jz done
+jmp loop
+label done
+halt
A => examples/overflow.span +4 -0
@@ 1,4 @@
+jmp end
+pad 32768
+label end
+halt
A => media/correspondence.svg +32 -0
@@ 1,32 @@
+<svg xmlns="http://www.w3.org/2000/svg" width="860" height="258" viewBox="0 0 860 258" role="img" aria-labelledby="title description">
+ <title id="title">Execution correspondence</title>
+ <desc id="description">For a well-formed program, valid layout W and source index i at most the program length, relocation commutes with fuel-bounded execution. S and B denote source and bytecode execution. R maps the source index to its byte address and preserves the accumulator</desc>
+ <defs>
+ <marker id="arrow" viewBox="0 0 8 8" refX="7" refY="4" markerWidth="7" markerHeight="7" orient="auto-start-reverse">
+ <path d="M1 1 L7 4 L1 7" fill="none" stroke="#292929" stroke-width="0.8"/>
+ </marker>
+ </defs>
+ <rect width="860" height="258" fill="#fff"/>
+ <g fill="#202020" font-family="Latin Modern Roman, STIX Two Text, Times New Roman, serif" text-anchor="middle">
+ <text x="430" y="25" font-size="16">wellformed p · valid p W · i ≤ |p|</text>
+ <g font-size="23" font-style="italic">
+ <text x="195" y="75">s</text>
+ <text x="645" y="75">R<tspan baseline-shift="sub" font-size="15">W</tspan>(s)</text>
+ <text x="195" y="197">S<tspan baseline-shift="super" font-size="15">k</tspan>(s)</text>
+ <text x="645" y="197">B<tspan baseline-shift="super" font-size="15">k</tspan>(R<tspan baseline-shift="sub" font-size="15">W</tspan>(s))</text>
+ </g>
+ <g font-size="20" font-style="italic">
+ <text x="420" y="57">R<tspan baseline-shift="sub" font-size="13">W</tspan></text>
+ <text x="420" y="178">R<tspan baseline-shift="sub" font-size="13">W</tspan></text>
+ <text x="168" y="139">S<tspan baseline-shift="super" font-size="13">k</tspan></text>
+ <text x="675" y="139">B<tspan baseline-shift="super" font-size="13">k</tspan></text>
+ </g>
+ <text x="430" y="242" font-size="18" font-style="italic">s = (i, a)    R<tspan baseline-shift="sub" font-size="12">W</tspan>(i, a) = (addr<tspan baseline-shift="sub" font-size="12">W</tspan>(i), a)</text>
+ </g>
+ <g fill="none" stroke="#292929" stroke-width="0.8" marker-end="url(#arrow)">
+ <path d="M246 68 H568"/>
+ <path d="M274 190 H538"/>
+ <path d="M195 93 V165"/>
+ <path d="M645 93 V165"/>
+ </g>
+</svg>
A => media/demo.gif +0 -0
A => media/demo.mp4 +0 -0
A => span +8 -0
@@ 1,8 @@
+#!/usr/bin/env bash
+set -euo pipefail
+span_root=$(CDPATH= cd -- "$(dirname -- "$0")" && pwd)
+if [[ ! -x "$span_root/.build/span" ]]; then
+ printf '%s\n' 'build span first with make' >&2
+ exit 1
+fi
+exec "$span_root/.build/span" "$@"
A => src/Encoding.thy +146 -0
@@ 1,146 @@
+theory Encoding
+ imports Relax
+begin
+
+datatype operation = Idle | Raise | Lower | Finish | Branch bool bool int
+
+fun bytesize :: "operation \<Rightarrow> nat" where
+ "bytesize (Branch c wide d) = (if wide then 3 else 2)"
+| "bytesize _ = 1"
+
+fun encodable :: "operation \<Rightarrow> bool" where
+ "encodable (Branch c wide d) = (if wide then -32768 \<le> d \<and> d < 32768 else -128 \<le> d \<and> d < 128)"
+| "encodable _ = True"
+
+fun encode :: "operation \<Rightarrow> nat list" where
+ "encode Idle = [0]"
+| "encode Raise = [1]"
+| "encode Lower = [2]"
+| "encode Finish = [3]"
+| "encode (Branch c False d) = [if c then 17 else 16, nat (d + 128)]"
+| "encode (Branch c True d) = [if c then 19 else 18, nat (d + 32768) mod 256, nat (d + 32768) div 256]"
+
+fun decode :: "nat list \<Rightarrow> (operation \<times> nat list) option" where
+ "decode [] = None"
+| "decode (b # bs) =
+ (if b = 0 then Some (Idle, bs)
+ else if b = 1 then Some (Raise, bs)
+ else if b = 2 then Some (Lower, bs)
+ else if b = 3 then Some (Finish, bs)
+ else if b = 16 \<or> b = 17 then
+ (case bs of [] \<Rightarrow> None | x # xs \<Rightarrow>
+ if x < 256 then Some (Branch (b = 17) False (int x - 128), xs) else None)
+ else if b = 18 \<or> b = 19 then
+ (case bs of x # y # xs \<Rightarrow>
+ if x < 256 \<and> y < 256 then Some (Branch (b = 19) True (int (y * 256 + x) - 32768), xs) else None
+ | _ \<Rightarrow> None)
+ else None)"
+
+lemma encode_length [simp]: "length (encode op) = bytesize op"
+ by (cases op) (auto split: bool.splits)
+
+lemma byte_join: "n div 256 * 256 + n mod 256 = (n :: nat)"
+ by (simp add: div_mult_mod_eq)
+
+lemma encode_bytes:
+ "encodable op \<Longrightarrow> set (encode op) \<subseteq> {..<256}"
+ by (cases op) (auto simp: nat_less_iff div_less_iff_less_mult split: bool.splits if_splits)
+
+theorem decode_encode:
+ assumes "encodable op"
+ shows "decode (encode op @ tail) = Some (op, tail)"
+ using assms
+ by (cases op)
+ (auto simp: byte_join nat_less_iff div_less_iff_less_mult split: bool.splits if_splits)
+
+theorem decode_canonical:
+ "decode bs = Some (op, rest) \<Longrightarrow> encodable op \<and> bs = encode op @ rest"
+ by (cases bs)
+ (auto simp: nat_less_iff div_less_iff_less_mult mod_less div_eq_0_iff
+ nat_add_distrib nat_mult_distrib
+ split: if_splits list.splits)
+
+corollary decode_progress:
+ "decode bs = Some (op, rest) \<Longrightarrow> length rest < length bs"
+ using decode_canonical[of bs op rest]
+ by (cases op) (auto split: bool.splits)
+
+theorem encode_injective:
+ "encodable a \<Longrightarrow> encodable b \<Longrightarrow> encode a = encode b \<longleftrightarrow> a = b"
+ using decode_encode[of a "[]"] decode_encode[of b "[]"]
+ by (metis append_Nil option.inject prod.inject)
+
+fun lower :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> nat instruction \<Rightarrow> operation" where
+ "lower p W i Nop = Idle"
+| "lower p W i Inc = Raise"
+| "lower p W i Dec = Lower"
+| "lower p W i Stop = Finish"
+| "lower p W i (Jump t) = Branch False (i \<in> W) (displacement p W i)"
+| "lower p W i (Zero t) = Branch True (i \<in> W) (displacement p W i)"
+
+definition chunks :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat list list" where
+ "chunks p W = map (\<lambda>i. encode (lower p W i (p ! i))) [0..<length p]"
+
+definition bytecode :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat list" where
+ "bytecode p W = concat (chunks p W)"
+
+lemma chunks_code [code]:
+ "chunks p W = map (\<lambda>(i,op). encode (lower p W i op)) (zip [0..<length p] p)"
+ unfolding chunks_def by (rule nth_equalityI) auto
+
+lemma lower_size:
+ "i < length p \<Longrightarrow> bytesize (lower p W i (p ! i)) = width p W i"
+ unfolding width_def branches_def by (cases "p ! i") auto
+
+lemma lower_encodable:
+ "valid p W \<Longrightarrow> i < length p \<Longrightarrow> encodable (lower p W i (p ! i))"
+ unfolding valid_def fits_signed branches_def
+ by (cases "p ! i") (auto split: if_splits)
+
+lemma chunks_length [simp]: "length (chunks p W) = length p"
+ by (simp add: chunks_def)
+
+lemma chunks_nth:
+ "i < length p \<Longrightarrow> chunks p W ! i = encode (lower p W i (p ! i))"
+ by (simp add: chunks_def)
+
+lemma prefix_length:
+ "i \<le> length p \<Longrightarrow> length (concat (take i (chunks p W))) = address p W i"
+proof (induction i)
+ case 0
+ then show ?case by simp
+next
+ case (Suc i)
+ then have idx: "i < length p" by simp
+ show ?case using Suc.IH Suc.prems
+ by (simp add: take_Suc_conv_app_nth chunks_nth[OF idx] lower_size[OF idx])
+qed
+
+lemma bytecode_length: "length (bytecode p W) = address p W (length p)"
+ using prefix_length[of "length p" p W] by (simp add: bytecode_def)
+
+lemma bytecode_bytes:
+ assumes valid: "valid p W"
+ shows "set (bytecode p W) \<subseteq> {..<256}"
+proof -
+ have each: "\<And>i. i < length p \<Longrightarrow> set (encode (lower p W i (p ! i))) \<subseteq> {..<256}"
+ by (rule encode_bytes, rule lower_encodable[OF valid]) assumption
+ show ?thesis unfolding bytecode_def chunks_def
+ by (auto dest: each[THEN subsetD])
+qed
+
+lemma fetch_instruction:
+ assumes "valid p W" "i < length p"
+ shows "map_option fst (decode (drop (address p W i) (bytecode p W))) = Some (lower p W i (p ! i))"
+proof -
+ have prefix: "bytecode p W = concat (take i (chunks p W)) @ concat (drop i (chunks p W))"
+ by (simp add: bytecode_def flip: concat_append)
+ have suffix: "drop i (chunks p W) = chunks p W ! i # drop (Suc i) (chunks p W)"
+ using assms(2) by (simp add: Cons_nth_drop_Suc)
+ show ?thesis
+ using prefix_length[OF less_imp_le[OF assms(2)], of W]
+ by (subst prefix, subst suffix)
+ (simp add: chunks_nth[OF assms(2)] decode_encode[OF lower_encodable[OF assms]])
+qed
+
+end
A => src/Export.thy +11 -0
@@ 1,11 @@
+theory Export
+ imports Frontend
+begin
+
+definition ascii :: "integer \<Rightarrow> char" where "ascii = char_of"
+
+definition ordinal :: "char \<Rightarrow> integer" where "ordinal = of_char"
+
+export_code process binary artifact disassemble ascii ordinal in SML module_name Span file_prefix span
+
+end
A => src/Frontend.thy +251 -0
@@ 1,251 @@
+theory Frontend
+ imports Machine "HOL-Library.Code_Target_Numeral"
+begin
+
+datatype 'a result = Error string | Ok 'a
+
+fun bind :: "'a result \<Rightarrow> ('a \<Rightarrow> 'b result) \<Rightarrow> 'b result" where
+ "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
+termination by (relation "measure id") (auto simp: div_less_dividend)
+
+definition newline :: string where "newline = [CHR 0x0A]"
+
+fun separate :: "char \<Rightarrow> string \<Rightarrow> string list" where
+ "separate c [] = [[]]"
+| "separate c (x # xs) = (if x = c then [] # separate c xs else
+ case separate c xs of [] \<Rightarrow> [[x]] | y # ys \<Rightarrow> (x # y) # ys)"
+
+definition words :: "string \<Rightarrow> string list" where
+ "words s = filter (\<lambda>x. x \<noteq> []) (separate CHR '' ''
+ (map (\<lambda>c. if c = CHR 0x09 \<or> c = CHR 0x0D then CHR '' '' else c) s))"
+
+definition number :: "string \<Rightarrow> nat option" where
+ "number s = (if s \<noteq> [] \<and> list_all (\<lambda>c. 48 \<le> nat_of_char c \<and> nat_of_char c < 58) s then
+ let n = foldl (\<lambda>n c. min 65537 (10 * n + nat_of_char c - 48)) 0 s in
+ if n \<le> 65536 then Some n else None else None)"
+
+datatype statement = Label string | Emit "string instruction" | Pad nat
+
+definition parse_line :: "nat \<Rightarrow> string list \<Rightarrow> statement list result" where
+ "parse_line n tokens = (let bad = Error (''invalid instruction at line '' @ decimal n) in
+ case tokens of [] \<Rightarrow> Ok []
+ | [a] \<Rightarrow> if a = ''nop'' then Ok [Emit Nop] else if a = ''inc'' then Ok [Emit Inc]
+ else if a = ''dec'' then Ok [Emit Dec] else if a = ''halt'' then Ok [Emit Stop] else bad
+ | [a,b] \<Rightarrow> if a = ''label'' then Ok [Label b] else if a = ''jmp'' then Ok [Emit (Jump b)]
+ else if a = ''jz'' then Ok [Emit (Zero b)] else if a = ''pad'' then
+ (case number b of None \<Rightarrow> Error (''invalid padding at line '' @ decimal n) | Some k \<Rightarrow> Ok [Pad k])
+ else bad
+ | _ \<Rightarrow> bad)"
+
+fun parse_lines :: "nat \<Rightarrow> string list \<Rightarrow> statement list result" where
+ "parse_lines n [] = Ok []"
+| "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"
+| "count (Pad n) = n"
+
+fun collect :: "statement list \<Rightarrow> nat \<Rightarrow> (string \<times> nat) list \<Rightarrow> (string \<times> nat) list result" where
+ "collect [] pc env = Ok env"
+| "collect (Label l # ss) pc env = (if map_of env l \<noteq> None then Error (''duplicate label '' @ l)
+ else collect ss pc ((l,pc) # env))"
+| "collect (s # ss) pc env = collect ss (pc + count s) env"
+
+fun resolve :: "(string \<times> nat) list \<Rightarrow> string instruction \<Rightarrow> nat instruction result" where
+ "resolve env Nop = Ok Nop"
+| "resolve env Inc = Ok Inc"
+| "resolve env Dec = Ok Dec"
+| "resolve env Stop = Ok Stop"
+| "resolve env (Jump l) = (case map_of env l of None \<Rightarrow> Error (''undefined label '' @ l) | Some t \<Rightarrow> Ok (Jump t))"
+| "resolve env (Zero l) = (case map_of env l of None \<Rightarrow> Error (''undefined label '' @ l) | Some t \<Rightarrow> Ok (Zero t))"
+
+fun resolve_all :: "(string \<times> nat) list \<Rightarrow> statement list \<Rightarrow> nat instruction list result" where
+ "resolve_all env [] = Ok []"
+| "resolve_all env (Label l # ss) = resolve_all env ss"
+| "resolve_all env (Emit op # ss) = bind (resolve env op) (\<lambda>x.
+ 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
+ then Error ''source must contain printable ASCII, tabs, or line endings'' else
+ bind (parse_lines 1 (separate CHR 0x0A s)) (\<lambda>ss.
+ if sum_list (map count ss) > 65536 then Error ''program exceeds 65536 instructions''
+ else bind (collect ss 0 []) (\<lambda>env. bind (resolve_all env ss) (\<lambda>p.
+ if wellformed p then Ok p else Error ''branch targets a label after the final instruction''))))"
+
+definition checked :: "nat instruction list \<Rightarrow> nat list result" where
+ "checked p = (if \<not> wellformed p then Error ''invalid branch target'' else
+ let W = layout p in if valid p W then Ok (bytecode p W)
+ else Error ''branch displacement exceeds the signed 16-bit range'')"
+
+lemma checked_assemble:
+ "checked p = Ok code \<longleftrightarrow> assemble p = Some code"
+ by (auto simp: checked_def assemble_def Let_def split: if_splits)
+
+theorem checked_execution:
+ "checked p = Ok code \<Longrightarrow>
+ execute (machine_step code) fuel (0,a) = relocate p (layout p) (execute (source_step p) fuel (0,a))"
+ by (simp add: checked_assemble assembly_execution)
+
+function history :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat set list" where
+ "history p W = (if widen p W = W then [W] else W # history p (widen p W))"
+ by pat_completeness auto
+termination
+ by (relation "measure (\<lambda>(p,W). card (branches p - W))") (auto intro: widen_decreases)
+
+declare history.simps [simp del]
+
+lemma history_nonempty: "history p W \<noteq> []"
+ by (subst history.simps) auto
+
+lemma history_last: "last (history p W) = settle p W"
+ by (induction p W rule: history.induct)
+ (subst history.simps, subst settle.simps, auto simp: history_nonempty)
+
+definition hexbyte :: "nat \<Rightarrow> string" where
+ "hexbyte n = [''0123456789abcdef'' ! (n div 16 mod 16), ''0123456789abcdef'' ! (n mod 16)]"
+
+fun joined :: "string \<Rightarrow> string list \<Rightarrow> string" where
+ "joined sep [] = []"
+| "joined sep (x # xs) = x @ (if xs = [] then [] else sep @ joined sep xs)"
+
+definition hex :: "nat list \<Rightarrow> string" where
+ "hex bs = joined '' '' (map hexbyte bs)"
+
+definition signed :: "int \<Rightarrow> string" where
+ "signed n = (if n < 0 then ''-'' @ decimal (nat (-n)) else ''+'' @ decimal (nat n))"
+
+fun opname :: "operation \<Rightarrow> string" where
+ "opname Idle = ''nop''"
+| "opname Raise = ''inc''"
+| "opname Lower = ''dec''"
+| "opname Finish = ''halt''"
+| "opname (Branch c wide d) = (if c then ''jz.'' else ''jmp.'') @ (if wide then ''16 '' else ''8 '') @ signed d"
+
+definition branchline :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> string" where
+ "branchline p W i = '' #'' @ decimal i @ '' @'' @ decimal (address p W i) @ '' '' @
+ opname (lower p W i (p ! i)) @ '' -> @'' @ decimal (address p W (destination p i)) @ newline"
+
+definition passline :: "nat instruction list \<Rightarrow> nat \<Rightarrow> nat set \<Rightarrow> string" where
+ "passline p n W = ''pass '' @ decimal n @ '' '' @ decimal (address p W (length p)) @
+ '' bytes widen ['' @ joined '', '' (map decimal (filter (\<lambda>i. i \<in> pending p W) [0..<length p])) @ '']'' @ newline @
+ concat (map (branchline p W) (filter (\<lambda>i. i \<in> branches p) [0..<length p]))"
+
+definition trace :: "nat instruction list \<Rightarrow> string" where
+ "trace p = (let hs = history p {} in concat (map (\<lambda>i. passline p i (hs ! i)) [0..<length hs]))"
+
+definition summary :: "nat instruction list \<Rightarrow> nat list \<Rightarrow> string" where
+ "summary p bs = decimal (length p) @ '' instructions, '' @ decimal (length bs) @ '' bytes, '' @
+ decimal (card (layout p)) @ '' long branches'' @ newline"
+
+definition compile :: "string \<Rightarrow> nat list result" where
+ "compile s = bind (source s) checked"
+
+theorem compile_sound:
+ "compile s = Ok code \<Longrightarrow> \<exists>p. source s = Ok p \<and> assemble p = Some code"
+ unfolding compile_def by (cases "source s") (auto simp: checked_assemble)
+
+theorem checked_failure:
+ "wellformed p \<Longrightarrow> checked p = Error e \<Longrightarrow> \<not> (\<exists>W. valid p W)"
+ using assembly_complete[of p]
+ by (auto simp: checked_def assemble_def split: if_splits)
+
+definition stopped :: "nat list \<Rightarrow> nat \<times> nat \<Rightarrow> string" where
+ "stopped bs s = (case map_option fst (decode (drop (fst s) bs)) of
+ Some Finish \<Rightarrow> ''halted'' | _ \<Rightarrow> if machine_step bs s = None then ''fault'' else ''fuel exhausted'')"
+
+definition runreport :: "nat list \<Rightarrow> nat \<Rightarrow> string" where
+ "runreport bs fuel = (let s = execute (machine_step bs) fuel (0,0) in
+ stopped bs s @ '' pc='' @ decimal (fst s) @ '' acc='' @ decimal (snd s) @ newline)"
+
+function listing :: "nat \<Rightarrow> nat list \<Rightarrow> string result" where
+ "listing pc bs = (if bs = [] then Ok [] else case decode bs of None \<Rightarrow> Error (''invalid encoding at byte '' @ decimal pc)
+ | Some (op,rest) \<Rightarrow> if length rest < length bs then
+ bind (listing (pc + bytesize op) rest) (\<lambda>s. Ok (decimal pc @ '' '' @
+ hex (take (bytesize op) bs) @ '' '' @ opname op @ newline @ s)) else Error ''invalid decoder progress'')"
+ by pat_completeness auto
+termination by (relation "measure (\<lambda>(pc,bs). length bs)") auto
+
+definition binary :: "string \<Rightarrow> bool \<times> string" where
+ "binary s = (case compile s of Error e \<Rightarrow> (False, e @ newline) | Ok bs \<Rightarrow> (True, map char_of_nat bs))"
+
+definition disassemble :: "string \<Rightarrow> bool \<times> string" where
+ "disassemble s = (case listing 0 (map nat_of_char s) of Error e \<Rightarrow> (False,e @ newline) | Ok text \<Rightarrow> (True,text))"
+
+definition inspect :: "string list \<Rightarrow> nat instruction list \<Rightarrow> nat list \<Rightarrow> bool \<times> string" where
+ "inspect args p bs = (let bad = (False, ''usage: span {assemble|trace|list|run} file [fuel]'' @ newline) in
+ case args of [mode] \<Rightarrow>
+ if mode = ''assemble'' then (True, summary p bs @ hex bs @ newline)
+ else if mode = ''trace'' then (True, trace p @ summary p bs)
+ else if mode = ''list'' then (case listing 0 bs of Error e \<Rightarrow> (False,e @ newline) | Ok s \<Rightarrow> (True,s))
+ else bad
+ | [mode,n] \<Rightarrow> if mode = ''run'' then
+ (case number n of None \<Rightarrow> (False,''fuel must be between 0 and 65536'' @ newline)
+ | Some fuel \<Rightarrow> (True, runreport bs fuel)) else bad
+ | _ \<Rightarrow> bad)"
+
+definition process :: "string list \<Rightarrow> string \<Rightarrow> bool \<times> string" where
+ "process args s = (case source s of Error e \<Rightarrow> (False, e @ newline) | Ok p \<Rightarrow>
+ 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
A => src/Layout.thy +151 -0
@@ 1,151 @@
+theory Layout
+ imports Model
+begin
+
+definition width :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> nat" where
+ "width p W i = (if i \<in> branches p then if i \<in> W then 3 else 2 else 1)"
+
+definition address :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> nat" where
+ "address p W i = (\<Sum>j<i. width p W j)"
+
+definition distance :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> nat" where
+ "distance p W i = (let t = destination p i in
+ if i < t then (\<Sum>j\<in>{Suc i..<t}. width p W j)
+ else (\<Sum>j\<in>{t..<Suc i}. width p W j))"
+
+definition fits :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
+ "fits p W i bits \<longleftrightarrow>
+ (if i < destination p i then distance p W i < 2 ^ (bits - 1)
+ else distance p W i \<le> 2 ^ (bits - 1))"
+
+definition displacement :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> int" where
+ "displacement p W i = int (address p W (destination p i)) - int (address p W (Suc i))"
+
+definition valid :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> bool" where
+ "valid p W \<longleftrightarrow> W \<subseteq> branches p \<and>
+ (\<forall>i\<in>branches p. fits p W i (if i \<in> W then 16 else 8))"
+
+lemma width_positive: "0 < width p W i"
+ by (simp add: width_def)
+
+lemma width_code [code]:
+ "width p W i = (if i < length p \<and> target (p ! i) \<noteq> None then if i \<in> W then 3 else 2 else 1)"
+ by (simp add: width_def branches_def)
+
+definition sizes :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat list" where
+ "sizes p W = map (\<lambda>(i,op). if target op = None then 1 else if i \<in> W then 3 else 2)
+ (zip [0..<length p] p)"
+
+lemma sizes_length [simp]: "length (sizes p W) = length p"
+ by (simp add: sizes_def)
+
+lemma sizes_nth:
+ "i < length p \<Longrightarrow> sizes p W ! i = width p W i"
+ by (simp add: sizes_def width_def branches_def)
+
+lemma width_mono: "W \<subseteq> V \<Longrightarrow> width p W i \<le> width p V i"
+ by (auto simp: width_def)
+
+lemma address_zero [simp]: "address p W 0 = 0"
+ by (simp add: address_def)
+
+lemma address_suc [simp]: "address p W (Suc i) = address p W i + width p W i"
+ by (simp add: address_def)
+
+lemma address_code [code]:
+ "address p W i = sum_list (take i (sizes p W)) + (i - length p)"
+proof (induction i)
+ case 0
+ then show ?case by simp
+next
+ case (Suc i)
+ show ?case
+ proof (cases "i < length p")
+ case True
+ with Suc show ?thesis by (simp add: take_Suc_conv_app_nth sizes_nth)
+ next
+ case False
+ with Suc show ?thesis by (simp add: width_def branches_def Suc_diff_le)
+ qed
+qed
+
+lemma address_mono:
+ "W \<subseteq> V \<Longrightarrow> address p W i \<le> address p V i"
+ unfolding address_def by (intro sum_mono width_mono) assumption
+
+lemma distance_mono:
+ "W \<subseteq> V \<Longrightarrow> distance p W i \<le> distance p V i"
+ unfolding distance_def Let_def
+ by (auto simp only: if_True if_False intro!: sum_mono width_mono split: if_splits)
+
+lemma fits_downward:
+ "W \<subseteq> V \<Longrightarrow> fits p V i bits \<Longrightarrow> fits p W i bits"
+ using distance_mono[of W V p i] unfolding fits_def by auto
+
+lemma prefix_interval:
+ fixes f :: "nat \<Rightarrow> nat"
+ assumes "a \<le> b"
+ shows "(\<Sum>j<b. f j) = (\<Sum>j<a. f j) + (\<Sum>j\<in>{a..<b}. f j)"
+proof -
+ have disjoint: "{..<a} \<inter> {a..<b} = {}" by auto
+ have "{..<b} = {..<a} \<union> {a..<b}" using assms by auto
+ then show ?thesis by (simp add: sum.union_disjoint disjoint)
+qed
+
+lemma displacement_distance:
+ "displacement p W i = (if i < destination p i then int (distance p W i) else - int (distance p W i))"
+proof (cases "i < destination p i")
+ case True
+ then have le: "Suc i \<le> destination p i" by simp
+ have eq: "int (\<Sum>j<destination p i. width p W j) =
+ int (\<Sum>j<Suc i. width p W j) + int (\<Sum>j\<in>{Suc i..<destination p i}. width p W j)"
+ using arg_cong[OF prefix_interval[OF le, of "width p W"], where f=int]
+ by (simp only: of_nat_add)
+ show ?thesis using eq
+ by (simp only: displacement_def distance_def address_def Let_def True if_True; linarith)
+next
+ case False
+ then have le: "destination p i \<le> Suc i" by simp
+ have eq: "int (\<Sum>j<Suc i. width p W j) =
+ int (\<Sum>j<destination p i. width p W j) + int (\<Sum>j\<in>{destination p i..<Suc i}. width p W j)"
+ using arg_cong[OF prefix_interval[OF le, of "width p W"], where f=int]
+ by (simp only: of_nat_add)
+ show ?thesis using eq
+ by (simp only: displacement_def distance_def address_def Let_def False if_False; linarith)
+qed
+
+lemma distance_code [code]:
+ "distance p W i = (if i < destination p i
+ then address p W (destination p i) - address p W (Suc i)
+ else address p W (Suc i) - address p W (destination p i))"
+ using displacement_distance[of p W i]
+ unfolding displacement_def by (auto simp: of_nat_diff split: if_splits)
+
+lemma fits_signed:
+ "fits p W i bits \<longleftrightarrow>
+ - int (2 ^ (bits - 1)) \<le> displacement p W i \<and>
+ displacement p W i < int (2 ^ (bits - 1))"
+proof -
+ have positive: "(0::int) < int (2 ^ (bits - 1) :: nat)" by simp
+ have nonnegative: "(0::int) \<le> int (distance p W i)" by simp
+ have lower: "- int (2 ^ (bits - 1)) \<le> int (distance p W i)"
+ using positive nonnegative by linarith
+ have upper: "- int (distance p W i) < int (2 ^ (bits - 1))"
+ using positive nonnegative by linarith
+ show ?thesis
+ by (cases "i < destination p i")
+ (simp_all only: fits_def displacement_distance if_True if_False lower upper
+ of_nat_less_iff of_nat_le_iff neg_le_iff_le simp_thms)
+qed
+
+lemma address_strict:
+ assumes "i < j"
+ shows "address p W i < address p W j"
+proof -
+ have pos: "0 < (\<Sum>k\<in>{i..<j}. width p W k)"
+ using assms by (intro sum_pos2[where i=i]) (auto simp: width_positive)
+ show ?thesis using prefix_interval[OF less_imp_le[OF assms], of "width p W"] pos
+ by (simp add: address_def)
+qed
+
+end
A => src/Machine.thy +84 -0
@@ 1,84 @@
+theory Machine
+ imports Encoding
+begin
+
+fun machine_advance :: "operation \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) option" where
+ "machine_advance Idle pc a = Some (Suc pc, a)"
+| "machine_advance Raise pc a = Some (Suc pc, Suc a)"
+| "machine_advance Lower pc a = Some (Suc pc, a - 1)"
+| "machine_advance Finish pc a = None"
+| "machine_advance (Branch c wide d) pc a =
+ (let next = pc + (if wide then 3 else 2) in
+ if c \<and> a \<noteq> 0 then Some (next, a)
+ else if 0 \<le> int next + d then Some (nat (int next + d), a) else None)"
+
+definition machine_step :: "nat list \<Rightarrow> nat \<times> nat \<Rightarrow> (nat \<times> nat) option" where
+ "machine_step code s = (case map_option fst (decode (drop (fst s) code)) of
+ None \<Rightarrow> None | Some op \<Rightarrow> machine_advance op (fst s) (snd s))"
+
+definition relocate :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat" where
+ "relocate p W s = (address p W (fst s), snd s)"
+
+lemma lower_advance:
+ assumes "i < length p"
+ shows "machine_advance (lower p W i (p ! i)) (address p W i) a =
+ map_option (relocate p W) (advance (p ! i) i a)"
+ using assms unfolding relocate_def
+ by (cases "p ! i")
+ (auto simp: displacement_def destination_def width_def branches_def Let_def of_nat_add)
+
+lemma source_closed:
+ "wellformed p \<Longrightarrow> i \<le> length p \<Longrightarrow> source_step p (i,a) = Some (j,b) \<Longrightarrow> j \<le> length p"
+ unfolding wellformed_def source_step_def branches_def destination_def
+ by (cases "p ! i") (auto split: if_splits)
+
+theorem step_correspondence:
+ assumes "valid p W" "i \<le> length p"
+ shows "machine_step (bytecode p W) (relocate p W (i,a)) =
+ map_option (relocate p W) (source_step p (i,a))"
+proof (cases "i < length p")
+ case True
+ show ?thesis using fetch_instruction[OF assms(1) True] lower_advance[OF True, of W a] True
+ by (auto simp: machine_step_def source_step_def relocate_def split: option.splits prod.splits)
+next
+ case False
+ with assms have "i = length p" by simp
+ then show ?thesis
+ by (simp add: machine_step_def source_step_def relocate_def bytecode_length[symmetric])
+qed
+
+theorem execution_correspondence:
+ assumes "wellformed p" "valid p W" "i \<le> length p"
+ shows "execute (machine_step (bytecode p W)) fuel (relocate p W (i,a)) =
+ relocate p W (execute (source_step p) fuel (i,a))"
+ using assms(3)
+proof (induction fuel arbitrary: i a)
+ case 0
+ then show ?case by simp
+next
+ case (Suc fuel)
+ show ?case
+ using Suc.IH source_closed[OF assms(1) Suc.prems]
+ step_correspondence[OF assms(2) Suc.prems, of a]
+ by (cases "source_step p (i,a)") (auto split: prod.splits)
+qed
+
+definition assemble :: "nat instruction list \<Rightarrow> nat list option" where
+ "assemble p = (if wellformed p \<and> valid p (layout p) then Some (bytecode p (layout p)) else None)"
+
+theorem assembly_complete:
+ "assemble p \<noteq> None \<longleftrightarrow> wellformed p \<and> (\<exists>W. valid p W)"
+ by (simp add: assemble_def layout_complete)
+
+theorem assembly_minimum:
+ "assemble p = Some code \<Longrightarrow> valid p V \<Longrightarrow> length code \<le> address p V (length p)"
+ using layout_minimum[of p V] by (auto simp: assemble_def bytecode_length split: if_splits)
+
+theorem assembly_execution:
+ assumes "assemble p = Some code"
+ shows "execute (machine_step code) fuel (0,a) =
+ relocate p (layout p) (execute (source_step p) fuel (0,a))"
+ using assms execution_correspondence[of p "layout p" 0 fuel a]
+ by (auto simp: assemble_def relocate_def split: if_splits)
+
+end
A => src/Model.thy +46 -0
@@ 1,46 @@
+theory Model
+ imports Main
+begin
+
+datatype 'a instruction = Nop | Inc | Dec | Stop | Jump 'a | Zero 'a
+
+fun target :: "'a instruction \<Rightarrow> 'a option" where
+ "target (Jump t) = Some t"
+| "target (Zero t) = Some t"
+| "target _ = None"
+
+definition branches :: "nat instruction list \<Rightarrow> nat set" where
+ "branches p = {i. i < length p \<and> target (p ! i) \<noteq> None}"
+
+definition destination :: "nat instruction list \<Rightarrow> nat \<Rightarrow> nat" where
+ "destination p i = the (target (p ! i))"
+
+definition wellformed :: "nat instruction list \<Rightarrow> bool" where
+ "wellformed p \<longleftrightarrow> (\<forall>i \<in> branches p. destination p i < length p)"
+
+lemma finite_branches [simp]: "finite (branches p)"
+ unfolding branches_def by (rule finite_subset[of _ "{..<length p}"]) auto
+
+lemma branch_index: "i \<in> branches p \<Longrightarrow> i < length p"
+ by (simp add: branches_def)
+
+lemma branches_code [code]:
+ "branches p = set (map fst (filter (\<lambda>(i,op). target op \<noteq> None) (zip [0..<length p] p)))"
+ by (auto simp: branches_def set_zip image_iff; force)
+
+fun advance :: "nat instruction \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) option" where
+ "advance Nop i a = Some (Suc i, a)"
+| "advance Inc i a = Some (Suc i, Suc a)"
+| "advance Dec i a = Some (Suc i, a - 1)"
+| "advance Stop i a = None"
+| "advance (Jump t) i a = Some (t, a)"
+| "advance (Zero t) i a = Some (if a = 0 then t else Suc i, a)"
+
+definition source_step :: "nat instruction list \<Rightarrow> nat \<times> nat \<Rightarrow> (nat \<times> nat) option" where
+ "source_step p s = (if fst s < length p then advance (p ! fst s) (fst s) (snd s) else None)"
+
+fun execute :: "('s \<Rightarrow> 's option) \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's" where
+ "execute step 0 s = s"
+| "execute step (Suc n) s = (case step s of None \<Rightarrow> s | Some t \<Rightarrow> execute step n t)"
+
+end
A => src/Relax.thy +144 -0
@@ 1,144 @@
+theory Relax
+ imports Layout
+begin
+
+definition pending :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat set" where
+ "pending p W = {i \<in> branches p. i \<notin> W \<and> \<not> fits p W i 8}"
+
+definition widen :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat set" where
+ "widen p W = W \<union> pending p W"
+
+lemma widen_extensive: "W \<subseteq> widen p W"
+ by (auto simp: widen_def)
+
+lemma widen_bounded:
+ "W \<subseteq> branches p \<Longrightarrow> widen p W \<subseteq> branches p"
+ by (auto simp: widen_def pending_def)
+
+lemma widen_decreases:
+ assumes "widen p W \<noteq> W"
+ shows "card (branches p - widen p W) < card (branches p - W)"
+proof (rule psubset_card_mono)
+ show "finite (branches p - W)" by simp
+ show "branches p - widen p W \<subset> branches p - W"
+ using assms unfolding widen_def pending_def by auto
+qed
+
+function settle :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat set" where
+ "settle p W = (if widen p W = W then W else settle p (widen p W))"
+ by pat_completeness auto
+termination
+ by (relation "measure (\<lambda>(p,W). card (branches p - W))")
+ (auto intro: widen_decreases)
+
+declare settle.simps [simp del]
+
+lemma settle_fixed: "widen p (settle p W) = settle p W"
+ by (induction p W rule: settle.induct) (subst (1 2) settle.simps, auto)
+
+lemma settle_extensive: "W \<subseteq> settle p W"
+proof (induction p W rule: settle.induct)
+ case (1 p W)
+ show ?case
+ proof (cases "widen p W = W")
+ case True
+ show ?thesis by (subst settle.simps) (simp add: True)
+ next
+ case False
+ have "widen p W \<subseteq> settle p (widen p W)" using "1.IH" False by simp
+ then have sub: "W \<subseteq> settle p (widen p W)" using widen_extensive[of W p] by blast
+ show ?thesis by (subst settle.simps) (simp add: False sub)
+ qed
+qed
+
+lemma settle_bounded:
+ "W \<subseteq> branches p \<Longrightarrow> settle p W \<subseteq> branches p"
+proof (induction p W rule: settle.induct)
+ case (1 p W)
+ show ?case
+ proof (cases "widen p W = W")
+ case True
+ show ?thesis by (subst settle.simps) (simp add: True "1.prems")
+ next
+ case False
+ have bounded: "widen p W \<subseteq> branches p" by (rule widen_bounded[OF "1.prems"])
+ have rec: "settle p (widen p W) \<subseteq> branches p" by (rule "1.IH"[OF False bounded])
+ show ?thesis by (subst settle.simps) (simp add: False rec)
+ qed
+qed
+
+lemma widen_necessary:
+ assumes "valid p V" "W \<subseteq> V"
+ shows "widen p W \<subseteq> V"
+proof
+ fix i
+ assume member: "i \<in> widen p W"
+ show "i \<in> V"
+ proof (cases "i \<in> W")
+ case True
+ with assms show ?thesis by blast
+ next
+ case False
+ with member have branch: "i \<in> branches p" and bad: "\<not> fits p W i 8"
+ by (auto simp: widen_def pending_def)
+ show ?thesis
+ proof (rule ccontr)
+ assume "i \<notin> V"
+ with assms(1) branch have "fits p V i 8" by (auto simp: valid_def)
+ then have "fits p W i 8" by (rule fits_downward[OF assms(2)])
+ with bad show False by contradiction
+ qed
+ qed
+qed
+
+lemma settle_least:
+ assumes "valid p V" "W \<subseteq> V"
+ shows "settle p W \<subseteq> V"
+ using assms
+proof (induction p W rule: settle.induct)
+ case (1 p W)
+ show ?case
+ proof (cases "widen p W = W")
+ case True
+ show ?thesis by (subst settle.simps) (simp add: True "1.prems")
+ next
+ case False
+ have necessary: "widen p W \<subseteq> V" by (rule widen_necessary[OF "1.prems"])
+ have rec: "settle p (widen p W) \<subseteq> V" by (rule "1.IH"[OF False "1.prems"(1) necessary])
+ show ?thesis by (subst settle.simps) (simp add: False rec)
+ qed
+qed
+
+definition layout :: "nat instruction list \<Rightarrow> nat set" where
+ "layout p = settle p {}"
+
+lemma layout_bounded: "layout p \<subseteq> branches p"
+ unfolding layout_def by (rule settle_bounded) simp
+
+lemma layout_least: "valid p V \<Longrightarrow> layout p \<subseteq> V"
+ unfolding layout_def by (rule settle_least) auto
+
+lemma layout_short:
+ "i \<in> branches p \<Longrightarrow> i \<notin> layout p \<Longrightarrow> fits p (layout p) i 8"
+ using settle_fixed[of p "{}"] unfolding layout_def widen_def pending_def by auto
+
+theorem layout_complete:
+ "valid p (layout p) \<longleftrightarrow> (\<exists>V. valid p V)"
+proof
+ assume "valid p (layout p)"
+ then show "\<exists>V. valid p V" by blast
+next
+ assume "\<exists>V. valid p V"
+ then obtain V where v: "valid p V" by blast
+ have sub: "layout p \<subseteq> V" by (rule layout_least[OF v])
+ have "\<forall>i\<in>branches p. fits p (layout p) i (if i \<in> layout p then 16 else 8)"
+ using v sub layout_short fits_downward[OF sub]
+ unfolding valid_def by (auto split: if_splits)
+ with layout_bounded show "valid p (layout p)" by (simp add: valid_def)
+qed
+
+theorem layout_minimum:
+ "valid p V \<Longrightarrow> address p (layout p) (length p) \<le> address p V (length p)"
+ by (intro address_mono layout_least)
+
+end
A => tests/Examples.thy +84 -0
@@ 1,84 @@
+theory Examples
+ imports "../src/Frontend"
+begin
+
+definition cascade :: "nat instruction list" where
+ "cascade = [Jump 127, Jump 130] @ replicate 128 Nop @ [Stop]"
+
+definition countdown :: "nat instruction list" where
+ "countdown = [Inc, Inc, Inc, Dec, Zero 6, Jump 3, Stop]"
+
+definition forward :: "nat \<Rightarrow> nat instruction list" where
+ "forward n = [Jump (Suc n)] @ replicate n Nop @ [Stop]"
+
+definition backward :: "nat \<Rightarrow> nat instruction list" where
+ "backward n = replicate n Nop @ [Jump 0, Stop]"
+
+lemma cascade_rounds:
+ "map (\<lambda>W. filter (\<lambda>i. i \<in> W) [0..<length cascade]) (history cascade {}) = [[], [1], [0,1]]"
+ by eval
+
+lemma cascade_size: "map_option length (assemble cascade) = Some 135"
+ by eval
+
+lemma forward_short: "layout (forward 127) = {}"
+ by eval
+
+lemma forward_long: "layout (forward 128) = {0}"
+ by eval
+
+lemma backward_short: "layout (backward 126) = {}"
+ by eval
+
+lemma backward_long: "layout (backward 127) = {127}"
+ by eval
+
+lemma countdown_execution:
+ "execute (source_step countdown) 32 (0,0) = (6,0)"
+ by eval
+
+lemma countdown_bytes:
+ "assemble countdown = Some [1,1,1,2,17,130,16,123,3]"
+ by eval
+
+lemma short_negative_boundary:
+ "decode [16,0] = Some (Branch False False (-128), [])"
+ by eval
+
+lemma long_negative_boundary:
+ "decode [18,0,0] = Some (Branch False True (-32768), [])"
+ by eval
+
+lemma long_positive_boundary:
+ "decode [18,255,255] = Some (Branch False True 32767, [])"
+ by eval
+
+lemma truncated_rejected: "decode [18,1] = None"
+ by eval
+
+lemma unknown_rejected: "decode [255] = None"
+ by eval
+
+lemma short_payload_rejected: "decode [16,256] = None"
+ by eval
+
+lemma long_payload_rejected: "decode [19,0,256] = None"
+ by eval
+
+lemma decoder_preserves_tail:
+ "decode [19,255,255,3,255] = Some (Branch True True 32767, [3,255])"
+ by eval
+
+lemma undefined_rejected:
+ "compile ''jmp missing'' = Error ''undefined label missing''"
+ by eval
+
+lemma duplicate_rejected:
+ "compile (''label a'' @ newline @ ''label a'') = Error ''duplicate label a''"
+ by eval
+
+lemma final_label_rejected:
+ "compile (''jmp end'' @ newline @ ''label end'') = Error ''branch targets a label after the final instruction''"
+ by eval
+
+end
A => tests/cli.py +224 -0
@@ 1,224 @@
+import itertools
+import os
+from pathlib import Path
+import random
+import resource
+import signal
+import stat
+import subprocess
+import tempfile
+
+
+ROOT = Path(__file__).resolve().parents[1]
+CHECKS = 0
+
+
+def check(condition, message):
+ global CHECKS
+ if not condition:
+ raise AssertionError(message)
+ CHECKS += 1
+
+
+def cli(*args, text=None, ok=True, preexec_fn=None):
+ result = subprocess.run(
+ [str(ROOT / "span"), *map(str, args)],
+ input=text,
+ text=True,
+ capture_output=True,
+ timeout=90,
+ cwd=ROOT,
+ preexec_fn=preexec_fn,
+ )
+ check((result.returncode == 0) == ok, (args, result.stdout, result.stderr))
+ return result.stdout if ok else result.stderr
+
+
+def restrict_output():
+ signal.signal(signal.SIGXFSZ, signal.SIG_IGN)
+ resource.setrlimit(resource.RLIMIT_FSIZE, (1, 1))
+
+
+def source(program):
+ lines = []
+ for i, (op, target) in enumerate(program):
+ lines.append(f"label b{i}")
+ lines.append(f"{op} b{target}" if op in ("jmp", "jz") else op)
+ return "\n".join(lines) + "\n"
+
+
+def layouts(program):
+ branches = [i for i, (op, _) in enumerate(program) if op in ("jmp", "jz")]
+ for flags in itertools.product((False, True), repeat=len(branches)):
+ wide = dict(zip(branches, flags))
+ positions = [0]
+ for i in range(len(program)):
+ positions.append(positions[-1] + (3 if wide.get(i) else 2 if i in wide else 1))
+ if all(
+ -(32768 if wide[i] else 128)
+ <= positions[program[i][1]] - positions[i + 1]
+ < (32768 if wide[i] else 128)
+ for i in branches
+ ):
+ yield positions[-1]
+
+
+def interpret(program, fuel):
+ pc, acc = 0, 0
+ for _ in range(fuel):
+ if pc >= len(program) or program[pc][0] == "halt":
+ break
+ op, target = program[pc]
+ if op == "inc":
+ acc += 1
+ elif op == "dec":
+ acc = max(0, acc - 1)
+ if op == "jmp" or op == "jz" and acc == 0:
+ pc = target
+ else:
+ pc += 1
+ return pc, acc
+
+
+def decode(data):
+ rows, at = [], 0
+ while at < len(data):
+ start, op = at, data[at]
+ at += 1
+ if op in (16, 17, 18, 19):
+ length = 2 if op < 18 else 3
+ payload = int.from_bytes(data[at : at + length - 1], "little")
+ at += length - 1
+ rows.append((start, at, op, payload - (128 if length == 2 else 32768)))
+ else:
+ check(op in (0, 1, 2, 3), "invalid opcode")
+ rows.append((start, at, op, None))
+ return rows
+
+
+def verify(program, data):
+ rows = decode(data)
+ check(len(rows) == len(program), "instruction count changed")
+ for (op, target), (_, end, opcode, displacement) in zip(program, rows):
+ if op in ("jmp", "jz"):
+ check(opcode in ((16, 18) if op == "jmp" else (17, 19)), "branch kind changed")
+ check(end + displacement == rows[target][0], "branch destination changed")
+ else:
+ check(opcode == {"nop": 0, "inc": 1, "dec": 2, "halt": 3}[op], "opcode changed")
+ check(len(data) == min(layouts(program)), "layout is not minimum")
+ return rows
+
+
+def main():
+ check("usage:" in cli("--help"), "help missing")
+ check("135 bytes" in cli("assemble", "examples/cascade.span"), "cascade size")
+ trace = cli("trace", "examples/cascade.span")
+ check("pass 0 133 bytes widen [1]" in trace, "first cascade pass")
+ check("pass 1 134 bytes widen [0]" in trace, "second cascade pass")
+ check("pass 2 135 bytes widen []" in trace, "fixed point missing")
+ check("halted pc=8 acc=0" in cli("run", "examples/countdown.span"), "countdown execution")
+ check("fuel exhausted" in cli("run", "examples/countdown.span", "1"), "fuel limit")
+ check("fuel exhausted pc=0 acc=0" in cli("run", "-", "5", text="label loop\njmp loop"), "self branch")
+ for text, message in [
+ ("jmp nowhere", "undefined label"),
+ ("label a\nlabel a", "duplicate label"),
+ ("jmp end\nlabel end", "after the final instruction"),
+ ("pad -1", "invalid padding"),
+ ("pad 65537", "invalid padding"),
+ ("pad 65536\nnop", "exceeds 65536"),
+ ("jmp", "invalid instruction"),
+ ("halt extra", "invalid instruction"),
+ ("label \x1b[31m", "printable ASCII"),
+ ]:
+ 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")
+ for padding, width in [(126, 2), (127, 3), (32765, 3)]:
+ report = cli("assemble", "-", text=f"label start\npad {padding}\njmp start\nhalt")
+ check(f"{padding + width + 1} bytes" in report, "backward range boundary")
+ check("16-bit range" in cli("assemble", "-", text="label start\npad 32766\njmp start\nhalt", ok=False), "negative overflow accepted")
+ rng = random.Random(0x5350414E)
+ with tempfile.TemporaryDirectory() as directory:
+ out = Path(directory) / "program.bin"
+ for case in range(36):
+ length = rng.randrange(8, 180)
+ program = [(rng.choice(("nop", "inc", "dec")), None) for _ in range(length)]
+ for i in rng.sample(range(length - 1), rng.randrange(1, 7)):
+ program[i] = (rng.choice(("jmp", "jz")), rng.randrange(length))
+ program[-1] = ("halt", None)
+ text = source(program)
+ cli("assemble", "-", "-o", out, text=text)
+ rows = verify(program, out.read_bytes())
+ pc, acc = interpret(program, 256)
+ 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}")
+ 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]))
+ check("invalid encoding" in cli("disassemble", out, ok=False), "truncated encoding accepted")
+ out.write_bytes(bytes([255]))
+ check("invalid encoding" in cli("disassemble", out, ok=False), "unknown opcode accepted")
+ out.write_bytes(b"preserve")
+ 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")
+ out.write_bytes(b"preserve")
+ before = set(Path(directory).iterdir())
+ cli("assemble", "examples/countdown.span", "-o", out, ok=False, preexec_fn=restrict_output)
+ check(out.read_bytes() == b"preserve", "failed write clobbered output")
+ check(set(Path(directory).iterdir()) == before, "failed write leaked temporary file")
+ destination = Path(directory) / "destination"
+ destination.mkdir()
+ before = set(Path(directory).iterdir())
+ cli("assemble", "examples/countdown.span", "-o", destination, ok=False)
+ check(destination.is_dir(), "failed rename replaced directory")
+ check(set(Path(directory).iterdir()) == before, "failed rename leaked temporary file")
+ same = Path(directory) / "source"
+ same.write_text("inc\nhalt\n")
+ cli("assemble", same, "-o", same)
+ check(same.read_bytes() == bytes([1, 3]), "assembly cannot replace its source")
+ link = Path(directory) / "link"
+ link.symlink_to(out)
+ cli("assemble", "-", "-o", link, text="halt")
+ check(out.read_bytes() == b"preserve", "output followed destination symlink")
+ check(not link.is_symlink() and link.read_bytes() == bytes([3]), "symlink not atomically replaced")
+ out.write_bytes(b"".join(bytes([18, n, 255 - n]) for n in range(256)) + bytes([3]))
+ listing = cli("disassemble", out)
+ raw = subprocess.run(
+ [str(ROOT / "span"), "disassemble", "-"],
+ input=out.read_bytes(), capture_output=True, timeout=90, cwd=ROOT,
+ )
+ check(raw.returncode == 0 and raw.stdout == listing.encode("ascii"), "binary stdin changed bytes")
+ check(len(listing.splitlines()) == 257, "binary file changed bytes")
+ out.write_bytes(bytes(1048577))
+ check("input exceeds 1 MiB" in cli("disassemble", out, ok=False), "binary size limit missing")
+ check("input exceeds 1 MiB" in cli("assemble", "-", text=" " * 1048577, ok=False), "stdin size limit missing")
+ out.chmod(0o600)
+ cli("assemble", "-", "-o", out, text="halt", preexec_fn=lambda: os.umask(0))
+ check(stat.S_IMODE(out.stat().st_mode) == 0o600, "replacement widened output permissions")
+ protected = Path(directory) / "protected"
+ protected.write_bytes(b"preserve")
+
+ def collide_output():
+ out.with_name(f".{out.name}.{os.getpid():X}.0").symlink_to(protected)
+
+ cli("assemble", "-", "-o", out, text="inc\nhalt", preexec_fn=collide_output)
+ check(out.read_bytes() == bytes([1, 3]), "temporary collision prevented output")
+ check(protected.read_bytes() == b"preserve", "temporary collision followed symlink")
+ collisions = list(Path(directory).glob(f".{out.name}.*"))
+ check(len(collisions) == 1 and collisions[0].is_symlink(), "temporary collision was removed or output leaked")
+ print(f"{CHECKS} checks passed, including 36 exhaustive layout comparisons")
+
+
+if __name__ == "__main__":
+ main()
