~james/span

initial commit

commit
a68ad347f48eb214044370b3ca67d33d9b3c9a6d browse tree
author
james <j@cpl0.zip>
signature
Verified ~james signed with a key registered by ~james
date
2026-10-31 06:50 UTC

25 files changed, +1177 −0

.gitignore added

@@ -0,0 +1,2 @@
1+/.build/
2+__pycache__/

Encoding.thy added

@@ -0,0 +1 @@
1+src/Encoding.thy
\ No newline at end of file

Machine.thy added

@@ -0,0 +1 @@
1+src/Machine.thy
\ No newline at end of file

Makefile added

@@ -0,0 +1,18 @@
1+ISABELLE ?= isabelle
2+
3+.PHONY: all check clean
4+
5+all: .build/ready
6+
7+.build/ready: ROOT $(wildcard src/*.thy tests/*.thy) cli/driver.ML Makefile
8+ @test "$$('$(ISABELLE)' version)" = Isabelle2026 || { printf '%s\n' 'span requires Isabelle2026' >&2; exit 1; }
9+ "$(ISABELLE)" build -D . -j 1 -o threads=1 -o parallel_proofs=0
10+ "$(ISABELLE)" export -n -d . -O .build -x 'Span.Export:code/span.ML' Span
11+ SPAN_ROOT="$(CURDIR)" "$$('$(ISABELLE)' getenv -b POLYML_HOME)/$$('$(ISABELLE)' getenv -b ISABELLE_PLATFORM64)/polyc" -o .build/span cli/driver.ML
12+ @touch $@
13+
14+check: all
15+ python3 tests/cli.py
16+
17+clean:
18+ rm -rf .build

README.md added

@@ -0,0 +1,15 @@
1+# Span
2+
3+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
4+
5+[![](media/demo.gif)](media/demo.mp4)
6+
7+## Correctness
8+
9+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
10+
11+[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)
12+
13+![](media/correspondence.svg)
14+
15+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

ROOT added

@@ -0,0 +1,15 @@
1+session Span in src = HOL +
2+ options [document = false]
3+ sessions
4+ "HOL-Library"
5+ directories
6+ "../tests"
7+ theories
8+ Model
9+ Layout
10+ Relax
11+ Encoding
12+ Machine
13+ Frontend
14+ Examples
15+ Export

Relax.thy added

@@ -0,0 +1 @@
1+src/Relax.thy
\ No newline at end of file

cli/driver.ML added

@@ -0,0 +1,57 @@
1+val root = valOf (OS.Process.getEnv "SPAN_ROOT");
2+val _ = use (root ^ "/.build/Span.Export/code/span.ML");
3+
4+fun chars s = map (Span.ascii o IntInf.fromInt o Char.ord) (String.explode s);
5+fun text cs = String.implode (map (Char.chr o IntInf.toInt o Span.ordinal) cs);
6+
7+fun read path =
8+ let
9+ val stream = if path = "-" then TextIO.stdIn else TextIO.openIn path
10+ val text = TextIO.inputN (stream, 1048577)
11+ val _ = if path = "-" then () else TextIO.closeIn stream
12+ in
13+ if size text > 1048576 then raise Fail "input exceeds 1 MiB" else text
14+ end;
15+
16+fun write path text =
17+ let
18+ val stream = BinIO.openOut path
19+ val _ = BinIO.output (stream, Byte.stringToBytes text)
20+ in BinIO.closeOut stream end;
21+
22+fun output (ok, message) =
23+ (TextIO.output (if ok then TextIO.stdOut else TextIO.stdErr, text message);
24+ OS.Process.exit (if ok then OS.Process.success else OS.Process.failure));
25+
26+fun usage () =
27+ (TextIO.output (TextIO.stdOut,
28+ "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");
29+ OS.Process.exit OS.Process.success);
30+
31+fun run args =
32+ case args of
33+ [] => usage ()
34+ | ["--help"] => usage ()
35+ | ["disassemble", file] => output (Span.disassemble (chars (read file)))
36+ | ["assemble", file, "-o", destination] =>
37+ let
38+ val input = chars (read file)
39+ val (ok, bytes) = Span.binary input
40+ in
41+ if ok then
42+ (write destination (text bytes);
43+ output (Span.process [chars "assemble"] input))
44+ else output (false, bytes)
45+ end
46+ | ["run", file] => output (Span.process (map chars ["run", "4096"]) (chars (read file)))
47+ | ["run", file, fuel] => output (Span.process (map chars ["run", fuel]) (chars (read file)))
48+ | [mode, file] =>
49+ if List.exists (fn x => x = mode) ["assemble", "trace", "list"] then
50+ output (Span.process [chars mode] (chars (read file)))
51+ else raise Fail "unknown command, use span --help"
52+ | _ => raise Fail "invalid arguments, use span --help";
53+
54+fun main () = run (CommandLine.arguments ())
55+ handle exn =>
56+ (TextIO.output (TextIO.stdErr, "span: " ^ General.exnMessage exn ^ "\n");
57+ OS.Process.exit OS.Process.failure);

examples/backward.span added

@@ -0,0 +1,4 @@
1+label start
2+pad 127
3+jmp start
4+halt

examples/cascade.span added

@@ -0,0 +1,8 @@
1+jmp near
2+jmp far
3+pad 125
4+label near
5+nop
6+pad 2
7+label far
8+halt

examples/countdown.span added

@@ -0,0 +1,9 @@
1+inc
2+inc
3+inc
4+label loop
5+dec
6+jz done
7+jmp loop
8+label done
9+halt

examples/overflow.span added

@@ -0,0 +1,4 @@
1+jmp end
2+pad 32768
3+label end
4+halt

media/correspondence.svg added

@@ -0,0 +1,32 @@
1+<svg xmlns="http://www.w3.org/2000/svg" width="860" height="258" viewBox="0 0 860 258" role="img" aria-labelledby="title description">
2+ <title id="title">Execution correspondence</title>
3+ <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>
4+ <defs>
5+ <marker id="arrow" viewBox="0 0 8 8" refX="7" refY="4" markerWidth="7" markerHeight="7" orient="auto-start-reverse">
6+ <path d="M1 1 L7 4 L1 7" fill="none" stroke="#292929" stroke-width="0.8"/>
7+ </marker>
8+ </defs>
9+ <rect width="860" height="258" fill="#fff"/>
10+ <g fill="#202020" font-family="Latin Modern Roman, STIX Two Text, Times New Roman, serif" text-anchor="middle">
11+ <text x="430" y="25" font-size="16">wellformed p &#183; valid p W &#183; i &#8804; |p|</text>
12+ <g font-size="23" font-style="italic">
13+ <text x="195" y="75">s</text>
14+ <text x="645" y="75">R<tspan baseline-shift="sub" font-size="15">W</tspan>(s)</text>
15+ <text x="195" y="197">S<tspan baseline-shift="super" font-size="15">k</tspan>(s)</text>
16+ <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>
17+ </g>
18+ <g font-size="20" font-style="italic">
19+ <text x="420" y="57">R<tspan baseline-shift="sub" font-size="13">W</tspan></text>
20+ <text x="420" y="178">R<tspan baseline-shift="sub" font-size="13">W</tspan></text>
21+ <text x="168" y="139">S<tspan baseline-shift="super" font-size="13">k</tspan></text>
22+ <text x="675" y="139">B<tspan baseline-shift="super" font-size="13">k</tspan></text>
23+ </g>
24+ <text x="430" y="242" font-size="18" font-style="italic">s = (i, a) &#160;&#160; 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>
25+ </g>
26+ <g fill="none" stroke="#292929" stroke-width="0.8" marker-end="url(#arrow)">
27+ <path d="M246 68 H568"/>
28+ <path d="M274 190 H538"/>
29+ <path d="M195 93 V165"/>
30+ <path d="M645 93 V165"/>
31+ </g>
32+</svg>

media/demo.gif added

Binary file.

media/demo.mp4 added

Binary file.

span added

@@ -0,0 +1,8 @@
1+#!/usr/bin/env bash
2+set -euo pipefail
3+span_root=$(CDPATH= cd -- "$(dirname -- "$0")" && pwd)
4+if [[ ! -x "$span_root/.build/span" ]]; then
5+ printf '%s\n' 'build span first with make' >&2
6+ exit 1
7+fi
8+exec "$span_root/.build/span" "$@"

src/Encoding.thy added

@@ -0,0 +1,129 @@
1+theory Encoding
2+ imports Relax
3+begin
4+
5+datatype operation = Idle | Raise | Lower | Finish | Branch bool bool int
6+
7+fun bytesize :: "operation \<Rightarrow> nat" where
8+ "bytesize (Branch c wide d) = (if wide then 3 else 2)"
9+| "bytesize _ = 1"
10+
11+fun encodable :: "operation \<Rightarrow> bool" where
12+ "encodable (Branch c wide d) = (if wide then -32768 \<le> d \<and> d < 32768 else -128 \<le> d \<and> d < 128)"
13+| "encodable _ = True"
14+
15+fun encode :: "operation \<Rightarrow> nat list" where
16+ "encode Idle = [0]"
17+| "encode Raise = [1]"
18+| "encode Lower = [2]"
19+| "encode Finish = [3]"
20+| "encode (Branch c False d) = [if c then 17 else 16, nat (d + 128)]"
21+| "encode (Branch c True d) = [if c then 19 else 18, nat (d + 32768) mod 256, nat (d + 32768) div 256]"
22+
23+fun decode :: "nat list \<Rightarrow> (operation \<times> nat list) option" where
24+ "decode [] = None"
25+| "decode (b # bs) =
26+ (if b = 0 then Some (Idle, bs)
27+ else if b = 1 then Some (Raise, bs)
28+ else if b = 2 then Some (Lower, bs)
29+ else if b = 3 then Some (Finish, bs)
30+ else if b = 16 \<or> b = 17 then
31+ (case bs of [] \<Rightarrow> None | x # xs \<Rightarrow>
32+ if x < 256 then Some (Branch (b = 17) False (int x - 128), xs) else None)
33+ else if b = 18 \<or> b = 19 then
34+ (case bs of x # y # xs \<Rightarrow>
35+ if x < 256 \<and> y < 256 then Some (Branch (b = 19) True (int (y * 256 + x) - 32768), xs) else None
36+ | _ \<Rightarrow> None)
37+ else None)"
38+
39+lemma encode_length [simp]: "length (encode op) = bytesize op"
40+ by (cases op) (auto split: bool.splits)
41+
42+lemma byte_join: "n div 256 * 256 + n mod 256 = (n :: nat)"
43+ by (simp add: div_mult_mod_eq)
44+
45+lemma encode_bytes:
46+ "encodable op \<Longrightarrow> set (encode op) \<subseteq> {..<256}"
47+ by (cases op) (auto simp: nat_less_iff div_less_iff_less_mult split: bool.splits if_splits)
48+
49+theorem decode_encode:
50+ assumes "encodable op"
51+ shows "decode (encode op @ tail) = Some (op, tail)"
52+ using assms
53+ by (cases op)
54+ (auto simp: byte_join nat_less_iff div_less_iff_less_mult split: bool.splits if_splits)
55+
56+fun lower :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> nat instruction \<Rightarrow> operation" where
57+ "lower p W i Nop = Idle"
58+| "lower p W i Inc = Raise"
59+| "lower p W i Dec = Lower"
60+| "lower p W i Stop = Finish"
61+| "lower p W i (Jump t) = Branch False (i \<in> W) (displacement p W i)"
62+| "lower p W i (Zero t) = Branch True (i \<in> W) (displacement p W i)"
63+
64+definition chunks :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat list list" where
65+ "chunks p W = map (\<lambda>i. encode (lower p W i (p ! i))) [0..<length p]"
66+
67+definition bytecode :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat list" where
68+ "bytecode p W = concat (chunks p W)"
69+
70+lemma chunks_code [code]:
71+ "chunks p W = map (\<lambda>(i,op). encode (lower p W i op)) (zip [0..<length p] p)"
72+ unfolding chunks_def by (rule nth_equalityI) auto
73+
74+lemma lower_size:
75+ "i < length p \<Longrightarrow> bytesize (lower p W i (p ! i)) = width p W i"
76+ unfolding width_def branches_def by (cases "p ! i") auto
77+
78+lemma lower_encodable:
79+ "valid p W \<Longrightarrow> i < length p \<Longrightarrow> encodable (lower p W i (p ! i))"
80+ unfolding valid_def fits_signed branches_def
81+ by (cases "p ! i") (auto split: if_splits)
82+
83+lemma chunks_length [simp]: "length (chunks p W) = length p"
84+ by (simp add: chunks_def)
85+
86+lemma chunks_nth:
87+ "i < length p \<Longrightarrow> chunks p W ! i = encode (lower p W i (p ! i))"
88+ by (simp add: chunks_def)
89+
90+lemma prefix_length:
91+ "i \<le> length p \<Longrightarrow> length (concat (take i (chunks p W))) = address p W i"
92+proof (induction i)
93+ case 0
94+ then show ?case by simp
95+next
96+ case (Suc i)
97+ then have idx: "i < length p" by simp
98+ show ?case using Suc.IH Suc.prems
99+ by (simp add: take_Suc_conv_app_nth chunks_nth[OF idx] lower_size[OF idx])
100+qed
101+
102+lemma bytecode_length: "length (bytecode p W) = address p W (length p)"
103+ using prefix_length[of "length p" p W] by (simp add: bytecode_def)
104+
105+lemma bytecode_bytes:
106+ assumes valid: "valid p W"
107+ shows "set (bytecode p W) \<subseteq> {..<256}"
108+proof -
109+ have each: "\<And>i. i < length p \<Longrightarrow> set (encode (lower p W i (p ! i))) \<subseteq> {..<256}"
110+ by (rule encode_bytes, rule lower_encodable[OF valid]) assumption
111+ show ?thesis unfolding bytecode_def chunks_def
112+ by (auto dest: each[THEN subsetD])
113+qed
114+
115+lemma fetch_instruction:
116+ assumes "valid p W" "i < length p"
117+ shows "map_option fst (decode (drop (address p W i) (bytecode p W))) = Some (lower p W i (p ! i))"
118+proof -
119+ have prefix: "bytecode p W = concat (take i (chunks p W)) @ concat (drop i (chunks p W))"
120+ by (simp add: bytecode_def flip: concat_append)
121+ have suffix: "drop i (chunks p W) = chunks p W ! i # drop (Suc i) (chunks p W)"
122+ using assms(2) by (simp add: Cons_nth_drop_Suc)
123+ show ?thesis
124+ using prefix_length[OF less_imp_le[OF assms(2)], of W]
125+ by (subst prefix, subst suffix)
126+ (simp add: chunks_nth[OF assms(2)] decode_encode[OF lower_encodable[OF assms]])
127+qed
128+
129+end

src/Export.thy added

@@ -0,0 +1,11 @@
1+theory Export
2+ imports Frontend
3+begin
4+
5+definition ascii :: "integer \<Rightarrow> char" where "ascii = char_of"
6+
7+definition ordinal :: "char \<Rightarrow> integer" where "ordinal = of_char"
8+
9+export_code process binary disassemble ascii ordinal in SML module_name Span file_prefix span
10+
11+end

src/Frontend.thy added

@@ -0,0 +1,201 @@
1+theory Frontend
2+ imports Machine "HOL-Library.Code_Target_Numeral"
3+begin
4+
5+datatype 'a result = Error string | Ok 'a
6+
7+fun bind :: "'a result \<Rightarrow> ('a \<Rightarrow> 'b result) \<Rightarrow> 'b result" where
8+ "bind (Error e) f = Error e"
9+| "bind (Ok x) f = f x"
10+
11+function decimal :: "nat \<Rightarrow> string" where
12+ "decimal n = (if n < 10 then [char_of_nat (48 + n)] else decimal (n div 10) @ [char_of_nat (48 + n mod 10)])"
13+ by pat_completeness auto
14+termination by (relation "measure id") (auto simp: div_less_dividend)
15+
16+definition newline :: string where "newline = [CHR 0x0A]"
17+
18+fun separate :: "char \<Rightarrow> string \<Rightarrow> string list" where
19+ "separate c [] = [[]]"
20+| "separate c (x # xs) = (if x = c then [] # separate c xs else
21+ case separate c xs of [] \<Rightarrow> [[x]] | y # ys \<Rightarrow> (x # y) # ys)"
22+
23+definition words :: "string \<Rightarrow> string list" where
24+ "words s = filter (\<lambda>x. x \<noteq> []) (separate CHR '' ''
25+ (map (\<lambda>c. if c = CHR 0x09 \<or> c = CHR 0x0D then CHR '' '' else c) s))"
26+
27+definition number :: "string \<Rightarrow> nat option" where
28+ "number s = (if s \<noteq> [] \<and> list_all (\<lambda>c. 48 \<le> nat_of_char c \<and> nat_of_char c < 58) s then
29+ let n = foldl (\<lambda>n c. min 65537 (10 * n + nat_of_char c - 48)) 0 s in
30+ if n \<le> 65536 then Some n else None else None)"
31+
32+datatype statement = Label string | Emit "string instruction" | Pad nat
33+
34+definition parse_line :: "nat \<Rightarrow> string list \<Rightarrow> statement list result" where
35+ "parse_line n tokens = (let bad = Error (''invalid instruction at line '' @ decimal n) in
36+ case tokens of [] \<Rightarrow> Ok []
37+ | [a] \<Rightarrow> if a = ''nop'' then Ok [Emit Nop] else if a = ''inc'' then Ok [Emit Inc]
38+ else if a = ''dec'' then Ok [Emit Dec] else if a = ''halt'' then Ok [Emit Stop] else bad
39+ | [a,b] \<Rightarrow> if a = ''label'' then Ok [Label b] else if a = ''jmp'' then Ok [Emit (Jump b)]
40+ else if a = ''jz'' then Ok [Emit (Zero b)] else if a = ''pad'' then
41+ (case number b of None \<Rightarrow> Error (''invalid padding at line '' @ decimal n) | Some k \<Rightarrow> Ok [Pad k])
42+ else bad
43+ | _ \<Rightarrow> bad)"
44+
45+fun parse_lines :: "nat \<Rightarrow> string list \<Rightarrow> statement list result" where
46+ "parse_lines n [] = Ok []"
47+| "parse_lines n (s # ss) = bind (parse_line n (words s)) (\<lambda>xs.
48+ bind (parse_lines (Suc n) ss) (\<lambda>ys. Ok (xs @ ys)))"
49+
50+fun count :: "statement \<Rightarrow> nat" where
51+ "count (Label l) = 0"
52+| "count (Emit op) = 1"
53+| "count (Pad n) = n"
54+
55+fun collect :: "statement list \<Rightarrow> nat \<Rightarrow> (string \<times> nat) list \<Rightarrow> (string \<times> nat) list result" where
56+ "collect [] pc env = Ok env"
57+| "collect (Label l # ss) pc env = (if map_of env l \<noteq> None then Error (''duplicate label '' @ l)
58+ else collect ss pc ((l,pc) # env))"
59+| "collect (s # ss) pc env = collect ss (pc + count s) env"
60+
61+fun resolve :: "(string \<times> nat) list \<Rightarrow> string instruction \<Rightarrow> nat instruction result" where
62+ "resolve env Nop = Ok Nop"
63+| "resolve env Inc = Ok Inc"
64+| "resolve env Dec = Ok Dec"
65+| "resolve env Stop = Ok Stop"
66+| "resolve env (Jump l) = (case map_of env l of None \<Rightarrow> Error (''undefined label '' @ l) | Some t \<Rightarrow> Ok (Jump t))"
67+| "resolve env (Zero l) = (case map_of env l of None \<Rightarrow> Error (''undefined label '' @ l) | Some t \<Rightarrow> Ok (Zero t))"
68+
69+fun resolve_all :: "(string \<times> nat) list \<Rightarrow> statement list \<Rightarrow> nat instruction list result" where
70+ "resolve_all env [] = Ok []"
71+| "resolve_all env (Label l # ss) = resolve_all env ss"
72+| "resolve_all env (Emit op # ss) = bind (resolve env op) (\<lambda>x.
73+ bind (resolve_all env ss) (\<lambda>xs. Ok (x # xs)))"
74+| "resolve_all env (Pad n # ss) = bind (resolve_all env ss) (\<lambda>xs. Ok (replicate n Nop @ xs))"
75+
76+definition source :: "string \<Rightarrow> nat instruction list result" where
77+ "source s = (if \<not> list_all (\<lambda>c. let n = nat_of_char c in
78+ n = 9 \<or> n = 10 \<or> n = 13 \<or> (32 \<le> n \<and> n < 127)) s
79+ then Error ''source must contain printable ASCII, tabs, or line endings'' else
80+ bind (parse_lines 1 (separate CHR 0x0A s)) (\<lambda>ss.
81+ if sum_list (map count ss) > 65536 then Error ''program exceeds 65536 instructions''
82+ else bind (collect ss 0 []) (\<lambda>env. bind (resolve_all env ss) (\<lambda>p.
83+ if wellformed p then Ok p else Error ''branch targets a label after the final instruction''))))"
84+
85+definition checked :: "nat instruction list \<Rightarrow> nat list result" where
86+ "checked p = (if \<not> wellformed p then Error ''invalid branch target'' else
87+ let W = layout p in if valid p W then Ok (bytecode p W)
88+ else Error ''branch displacement exceeds the signed 16-bit range'')"
89+
90+lemma checked_assemble:
91+ "checked p = Ok code \<longleftrightarrow> assemble p = Some code"
92+ by (auto simp: checked_def assemble_def Let_def split: if_splits)
93+
94+theorem checked_execution:
95+ "checked p = Ok code \<Longrightarrow>
96+ execute (machine_step code) fuel (0,a) = relocate p (layout p) (execute (source_step p) fuel (0,a))"
97+ by (simp add: checked_assemble assembly_execution)
98+
99+function history :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat set list" where
100+ "history p W = (if widen p W = W then [W] else W # history p (widen p W))"
101+ by pat_completeness auto
102+termination
103+ by (relation "measure (\<lambda>(p,W). card (branches p - W))") (auto intro: widen_decreases)
104+
105+declare history.simps [simp del]
106+
107+lemma history_nonempty: "history p W \<noteq> []"
108+ by (subst history.simps) auto
109+
110+lemma history_last: "last (history p W) = settle p W"
111+ by (induction p W rule: history.induct)
112+ (subst history.simps, subst settle.simps, auto simp: history_nonempty)
113+
114+definition hexbyte :: "nat \<Rightarrow> string" where
115+ "hexbyte n = [''0123456789abcdef'' ! (n div 16 mod 16), ''0123456789abcdef'' ! (n mod 16)]"
116+
117+fun joined :: "string \<Rightarrow> string list \<Rightarrow> string" where
118+ "joined sep [] = []"
119+| "joined sep (x # xs) = x @ (if xs = [] then [] else sep @ joined sep xs)"
120+
121+definition hex :: "nat list \<Rightarrow> string" where
122+ "hex bs = joined '' '' (map hexbyte bs)"
123+
124+definition signed :: "int \<Rightarrow> string" where
125+ "signed n = (if n < 0 then ''-'' @ decimal (nat (-n)) else ''+'' @ decimal (nat n))"
126+
127+fun opname :: "operation \<Rightarrow> string" where
128+ "opname Idle = ''nop''"
129+| "opname Raise = ''inc''"
130+| "opname Lower = ''dec''"
131+| "opname Finish = ''halt''"
132+| "opname (Branch c wide d) = (if c then ''jz.'' else ''jmp.'') @ (if wide then ''16 '' else ''8 '') @ signed d"
133+
134+definition branchline :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> string" where
135+ "branchline p W i = '' #'' @ decimal i @ '' @'' @ decimal (address p W i) @ '' '' @
136+ opname (lower p W i (p ! i)) @ '' -> @'' @ decimal (address p W (destination p i)) @ newline"
137+
138+definition passline :: "nat instruction list \<Rightarrow> nat \<Rightarrow> nat set \<Rightarrow> string" where
139+ "passline p n W = ''pass '' @ decimal n @ '' '' @ decimal (address p W (length p)) @
140+ '' bytes widen ['' @ joined '', '' (map decimal (filter (\<lambda>i. i \<in> pending p W) [0..<length p])) @ '']'' @ newline @
141+ concat (map (branchline p W) (filter (\<lambda>i. i \<in> branches p) [0..<length p]))"
142+
143+definition trace :: "nat instruction list \<Rightarrow> string" where
144+ "trace p = (let hs = history p {} in concat (map (\<lambda>i. passline p i (hs ! i)) [0..<length hs]))"
145+
146+definition summary :: "nat instruction list \<Rightarrow> nat list \<Rightarrow> string" where
147+ "summary p bs = decimal (length p) @ '' instructions, '' @ decimal (length bs) @ '' bytes, '' @
148+ decimal (card (layout p)) @ '' long branches'' @ newline"
149+
150+definition compile :: "string \<Rightarrow> nat list result" where
151+ "compile s = bind (source s) checked"
152+
153+theorem compile_sound:
154+ "compile s = Ok code \<Longrightarrow> \<exists>p. source s = Ok p \<and> assemble p = Some code"
155+ unfolding compile_def by (cases "source s") (auto simp: checked_assemble)
156+
157+theorem checked_failure:
158+ "wellformed p \<Longrightarrow> checked p = Error e \<Longrightarrow> \<not> (\<exists>W. valid p W)"
159+ using assembly_complete[of p]
160+ by (auto simp: checked_def assemble_def split: if_splits)
161+
162+definition stopped :: "nat list \<Rightarrow> nat \<times> nat \<Rightarrow> string" where
163+ "stopped bs s = (case map_option fst (decode (drop (fst s) bs)) of
164+ Some Finish \<Rightarrow> ''halted'' | _ \<Rightarrow> if machine_step bs s = None then ''fault'' else ''fuel exhausted'')"
165+
166+definition runreport :: "nat list \<Rightarrow> nat \<Rightarrow> string" where
167+ "runreport bs fuel = (let s = execute (machine_step bs) fuel (0,0) in
168+ stopped bs s @ '' pc='' @ decimal (fst s) @ '' acc='' @ decimal (snd s) @ newline)"
169+
170+function listing :: "nat \<Rightarrow> nat list \<Rightarrow> string result" where
171+ "listing pc bs = (if bs = [] then Ok [] else case decode bs of None \<Rightarrow> Error (''invalid encoding at byte '' @ decimal pc)
172+ | Some (op,rest) \<Rightarrow> if length rest < length bs then
173+ bind (listing (pc + bytesize op) rest) (\<lambda>s. Ok (decimal pc @ '' '' @
174+ hex (take (bytesize op) bs) @ '' '' @ opname op @ newline @ s)) else Error ''invalid decoder progress'')"
175+ by pat_completeness auto
176+termination by (relation "measure (\<lambda>(pc,bs). length bs)") auto
177+
178+definition binary :: "string \<Rightarrow> bool \<times> string" where
179+ "binary s = (case compile s of Error e \<Rightarrow> (False, e @ newline) | Ok bs \<Rightarrow> (True, map char_of_nat bs))"
180+
181+definition disassemble :: "string \<Rightarrow> bool \<times> string" where
182+ "disassemble s = (case listing 0 (map nat_of_char s) of Error e \<Rightarrow> (False,e @ newline) | Ok text \<Rightarrow> (True,text))"
183+
184+definition inspect :: "string list \<Rightarrow> nat instruction list \<Rightarrow> nat list \<Rightarrow> bool \<times> string" where
185+ "inspect args p bs = (let bad = (False, ''usage: span {assemble|trace|list|run} file [fuel]'' @ newline) in
186+ case args of [mode] \<Rightarrow>
187+ if mode = ''assemble'' then (True, summary p bs @ hex bs @ newline)
188+ else if mode = ''trace'' then (True, trace p @ summary p bs)
189+ else if mode = ''list'' then (case listing 0 bs of Error e \<Rightarrow> (False,e @ newline) | Ok s \<Rightarrow> (True,s))
190+ else bad
191+ | [mode,n] \<Rightarrow> if mode = ''run'' then
192+ (case number n of None \<Rightarrow> (False,''fuel must be between 0 and 65536'' @ newline)
193+ | Some fuel \<Rightarrow> (True, runreport bs fuel)) else bad
194+ | _ \<Rightarrow> bad)"
195+
196+definition process :: "string list \<Rightarrow> string \<Rightarrow> bool \<times> string" where
197+ "process args s = (case source s of Error e \<Rightarrow> (False, e @ newline) | Ok p \<Rightarrow>
198+ case checked p of Error e \<Rightarrow> (False, (if args = [''trace''] then trace p else []) @ e @ newline)
199+ | Ok bs \<Rightarrow> inspect args p bs)"
200+
201+end

src/Layout.thy added

@@ -0,0 +1,151 @@
1+theory Layout
2+ imports Model
3+begin
4+
5+definition width :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> nat" where
6+ "width p W i = (if i \<in> branches p then if i \<in> W then 3 else 2 else 1)"
7+
8+definition address :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> nat" where
9+ "address p W i = (\<Sum>j<i. width p W j)"
10+
11+definition distance :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> nat" where
12+ "distance p W i = (let t = destination p i in
13+ if i < t then (\<Sum>j\<in>{Suc i..<t}. width p W j)
14+ else (\<Sum>j\<in>{t..<Suc i}. width p W j))"
15+
16+definition fits :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
17+ "fits p W i bits \<longleftrightarrow>
18+ (if i < destination p i then distance p W i < 2 ^ (bits - 1)
19+ else distance p W i \<le> 2 ^ (bits - 1))"
20+
21+definition displacement :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> int" where
22+ "displacement p W i = int (address p W (destination p i)) - int (address p W (Suc i))"
23+
24+definition valid :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> bool" where
25+ "valid p W \<longleftrightarrow> W \<subseteq> branches p \<and>
26+ (\<forall>i\<in>branches p. fits p W i (if i \<in> W then 16 else 8))"
27+
28+lemma width_positive: "0 < width p W i"
29+ by (simp add: width_def)
30+
31+lemma width_code [code]:
32+ "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)"
33+ by (simp add: width_def branches_def)
34+
35+definition sizes :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat list" where
36+ "sizes p W = map (\<lambda>(i,op). if target op = None then 1 else if i \<in> W then 3 else 2)
37+ (zip [0..<length p] p)"
38+
39+lemma sizes_length [simp]: "length (sizes p W) = length p"
40+ by (simp add: sizes_def)
41+
42+lemma sizes_nth:
43+ "i < length p \<Longrightarrow> sizes p W ! i = width p W i"
44+ by (simp add: sizes_def width_def branches_def)
45+
46+lemma width_mono: "W \<subseteq> V \<Longrightarrow> width p W i \<le> width p V i"
47+ by (auto simp: width_def)
48+
49+lemma address_zero [simp]: "address p W 0 = 0"
50+ by (simp add: address_def)
51+
52+lemma address_suc [simp]: "address p W (Suc i) = address p W i + width p W i"
53+ by (simp add: address_def)
54+
55+lemma address_code [code]:
56+ "address p W i = sum_list (take i (sizes p W)) + (i - length p)"
57+proof (induction i)
58+ case 0
59+ then show ?case by simp
60+next
61+ case (Suc i)
62+ show ?case
63+ proof (cases "i < length p")
64+ case True
65+ with Suc show ?thesis by (simp add: take_Suc_conv_app_nth sizes_nth)
66+ next
67+ case False
68+ with Suc show ?thesis by (simp add: width_def branches_def Suc_diff_le)
69+ qed
70+qed
71+
72+lemma address_mono:
73+ "W \<subseteq> V \<Longrightarrow> address p W i \<le> address p V i"
74+ unfolding address_def by (intro sum_mono width_mono) assumption
75+
76+lemma distance_mono:
77+ "W \<subseteq> V \<Longrightarrow> distance p W i \<le> distance p V i"
78+ unfolding distance_def Let_def
79+ by (auto simp only: if_True if_False intro!: sum_mono width_mono split: if_splits)
80+
81+lemma fits_downward:
82+ "W \<subseteq> V \<Longrightarrow> fits p V i bits \<Longrightarrow> fits p W i bits"
83+ using distance_mono[of W V p i] unfolding fits_def by auto
84+
85+lemma prefix_interval:
86+ fixes f :: "nat \<Rightarrow> nat"
87+ assumes "a \<le> b"
88+ shows "(\<Sum>j<b. f j) = (\<Sum>j<a. f j) + (\<Sum>j\<in>{a..<b}. f j)"
89+proof -
90+ have disjoint: "{..<a} \<inter> {a..<b} = {}" by auto
91+ have "{..<b} = {..<a} \<union> {a..<b}" using assms by auto
92+ then show ?thesis by (simp add: sum.union_disjoint disjoint)
93+qed
94+
95+lemma displacement_distance:
96+ "displacement p W i = (if i < destination p i then int (distance p W i) else - int (distance p W i))"
97+proof (cases "i < destination p i")
98+ case True
99+ then have le: "Suc i \<le> destination p i" by simp
100+ have eq: "int (\<Sum>j<destination p i. width p W j) =
101+ int (\<Sum>j<Suc i. width p W j) + int (\<Sum>j\<in>{Suc i..<destination p i}. width p W j)"
102+ using arg_cong[OF prefix_interval[OF le, of "width p W"], where f=int]
103+ by (simp only: of_nat_add)
104+ show ?thesis using eq
105+ by (simp only: displacement_def distance_def address_def Let_def True if_True; linarith)
106+next
107+ case False
108+ then have le: "destination p i \<le> Suc i" by simp
109+ have eq: "int (\<Sum>j<Suc i. width p W j) =
110+ int (\<Sum>j<destination p i. width p W j) + int (\<Sum>j\<in>{destination p i..<Suc i}. width p W j)"
111+ using arg_cong[OF prefix_interval[OF le, of "width p W"], where f=int]
112+ by (simp only: of_nat_add)
113+ show ?thesis using eq
114+ by (simp only: displacement_def distance_def address_def Let_def False if_False; linarith)
115+qed
116+
117+lemma distance_code [code]:
118+ "distance p W i = (if i < destination p i
119+ then address p W (destination p i) - address p W (Suc i)
120+ else address p W (Suc i) - address p W (destination p i))"
121+ using displacement_distance[of p W i]
122+ unfolding displacement_def by (auto simp: of_nat_diff split: if_splits)
123+
124+lemma fits_signed:
125+ "fits p W i bits \<longleftrightarrow>
126+ - int (2 ^ (bits - 1)) \<le> displacement p W i \<and>
127+ displacement p W i < int (2 ^ (bits - 1))"
128+proof -
129+ have positive: "(0::int) < int (2 ^ (bits - 1) :: nat)" by simp
130+ have nonnegative: "(0::int) \<le> int (distance p W i)" by simp
131+ have lower: "- int (2 ^ (bits - 1)) \<le> int (distance p W i)"
132+ using positive nonnegative by linarith
133+ have upper: "- int (distance p W i) < int (2 ^ (bits - 1))"
134+ using positive nonnegative by linarith
135+ show ?thesis
136+ by (cases "i < destination p i")
137+ (simp_all only: fits_def displacement_distance if_True if_False lower upper
138+ of_nat_less_iff of_nat_le_iff neg_le_iff_le simp_thms)
139+qed
140+
141+lemma address_strict:
142+ assumes "i < j"
143+ shows "address p W i < address p W j"
144+proof -
145+ have pos: "0 < (\<Sum>k\<in>{i..<j}. width p W k)"
146+ using assms by (intro sum_pos2[where i=i]) (auto simp: width_positive)
147+ show ?thesis using prefix_interval[OF less_imp_le[OF assms], of "width p W"] pos
148+ by (simp add: address_def)
149+qed
150+
151+end

src/Machine.thy added

@@ -0,0 +1,84 @@
1+theory Machine
2+ imports Encoding
3+begin
4+
5+fun machine_advance :: "operation \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) option" where
6+ "machine_advance Idle pc a = Some (Suc pc, a)"
7+| "machine_advance Raise pc a = Some (Suc pc, Suc a)"
8+| "machine_advance Lower pc a = Some (Suc pc, a - 1)"
9+| "machine_advance Finish pc a = None"
10+| "machine_advance (Branch c wide d) pc a =
11+ (let next = pc + (if wide then 3 else 2) in
12+ if c \<and> a \<noteq> 0 then Some (next, a)
13+ else if 0 \<le> int next + d then Some (nat (int next + d), a) else None)"
14+
15+definition machine_step :: "nat list \<Rightarrow> nat \<times> nat \<Rightarrow> (nat \<times> nat) option" where
16+ "machine_step code s = (case map_option fst (decode (drop (fst s) code)) of
17+ None \<Rightarrow> None | Some op \<Rightarrow> machine_advance op (fst s) (snd s))"
18+
19+definition relocate :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat" where
20+ "relocate p W s = (address p W (fst s), snd s)"
21+
22+lemma lower_advance:
23+ assumes "i < length p"
24+ shows "machine_advance (lower p W i (p ! i)) (address p W i) a =
25+ map_option (relocate p W) (advance (p ! i) i a)"
26+ using assms unfolding relocate_def
27+ by (cases "p ! i")
28+ (auto simp: displacement_def destination_def width_def branches_def Let_def of_nat_add)
29+
30+lemma source_closed:
31+ "wellformed p \<Longrightarrow> i \<le> length p \<Longrightarrow> source_step p (i,a) = Some (j,b) \<Longrightarrow> j \<le> length p"
32+ unfolding wellformed_def source_step_def branches_def destination_def
33+ by (cases "p ! i") (auto split: if_splits)
34+
35+theorem step_correspondence:
36+ assumes "valid p W" "i \<le> length p"
37+ shows "machine_step (bytecode p W) (relocate p W (i,a)) =
38+ map_option (relocate p W) (source_step p (i,a))"
39+proof (cases "i < length p")
40+ case True
41+ show ?thesis using fetch_instruction[OF assms(1) True] lower_advance[OF True, of W a] True
42+ by (auto simp: machine_step_def source_step_def relocate_def split: option.splits prod.splits)
43+next
44+ case False
45+ with assms have "i = length p" by simp
46+ then show ?thesis
47+ by (simp add: machine_step_def source_step_def relocate_def bytecode_length[symmetric])
48+qed
49+
50+theorem execution_correspondence:
51+ assumes "wellformed p" "valid p W" "i \<le> length p"
52+ shows "execute (machine_step (bytecode p W)) fuel (relocate p W (i,a)) =
53+ relocate p W (execute (source_step p) fuel (i,a))"
54+ using assms(3)
55+proof (induction fuel arbitrary: i a)
56+ case 0
57+ then show ?case by simp
58+next
59+ case (Suc fuel)
60+ show ?case
61+ using Suc.IH source_closed[OF assms(1) Suc.prems]
62+ step_correspondence[OF assms(2) Suc.prems, of a]
63+ by (cases "source_step p (i,a)") (auto split: prod.splits)
64+qed
65+
66+definition assemble :: "nat instruction list \<Rightarrow> nat list option" where
67+ "assemble p = (if wellformed p \<and> valid p (layout p) then Some (bytecode p (layout p)) else None)"
68+
69+theorem assembly_complete:
70+ "assemble p \<noteq> None \<longleftrightarrow> wellformed p \<and> (\<exists>W. valid p W)"
71+ by (simp add: assemble_def layout_complete)
72+
73+theorem assembly_minimum:
74+ "assemble p = Some code \<Longrightarrow> valid p V \<Longrightarrow> length code \<le> address p V (length p)"
75+ using layout_minimum[of p V] by (auto simp: assemble_def bytecode_length split: if_splits)
76+
77+theorem assembly_execution:
78+ assumes "assemble p = Some code"
79+ shows "execute (machine_step code) fuel (0,a) =
80+ relocate p (layout p) (execute (source_step p) fuel (0,a))"
81+ using assms execution_correspondence[of p "layout p" 0 fuel a]
82+ by (auto simp: assemble_def relocate_def split: if_splits)
83+
84+end

src/Model.thy added

@@ -0,0 +1,46 @@
1+theory Model
2+ imports Main
3+begin
4+
5+datatype 'a instruction = Nop | Inc | Dec | Stop | Jump 'a | Zero 'a
6+
7+fun target :: "'a instruction \<Rightarrow> 'a option" where
8+ "target (Jump t) = Some t"
9+| "target (Zero t) = Some t"
10+| "target _ = None"
11+
12+definition branches :: "nat instruction list \<Rightarrow> nat set" where
13+ "branches p = {i. i < length p \<and> target (p ! i) \<noteq> None}"
14+
15+definition destination :: "nat instruction list \<Rightarrow> nat \<Rightarrow> nat" where
16+ "destination p i = the (target (p ! i))"
17+
18+definition wellformed :: "nat instruction list \<Rightarrow> bool" where
19+ "wellformed p \<longleftrightarrow> (\<forall>i \<in> branches p. destination p i < length p)"
20+
21+lemma finite_branches [simp]: "finite (branches p)"
22+ unfolding branches_def by (rule finite_subset[of _ "{..<length p}"]) auto
23+
24+lemma branch_index: "i \<in> branches p \<Longrightarrow> i < length p"
25+ by (simp add: branches_def)
26+
27+lemma branches_code [code]:
28+ "branches p = set (map fst (filter (\<lambda>(i,op). target op \<noteq> None) (zip [0..<length p] p)))"
29+ by (auto simp: branches_def set_zip image_iff; force)
30+
31+fun advance :: "nat instruction \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) option" where
32+ "advance Nop i a = Some (Suc i, a)"
33+| "advance Inc i a = Some (Suc i, Suc a)"
34+| "advance Dec i a = Some (Suc i, a - 1)"
35+| "advance Stop i a = None"
36+| "advance (Jump t) i a = Some (t, a)"
37+| "advance (Zero t) i a = Some (if a = 0 then t else Suc i, a)"
38+
39+definition source_step :: "nat instruction list \<Rightarrow> nat \<times> nat \<Rightarrow> (nat \<times> nat) option" where
40+ "source_step p s = (if fst s < length p then advance (p ! fst s) (fst s) (snd s) else None)"
41+
42+fun execute :: "('s \<Rightarrow> 's option) \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's" where
43+ "execute step 0 s = s"
44+| "execute step (Suc n) s = (case step s of None \<Rightarrow> s | Some t \<Rightarrow> execute step n t)"
45+
46+end

src/Relax.thy added

@@ -0,0 +1,144 @@
1+theory Relax
2+ imports Layout
3+begin
4+
5+definition pending :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat set" where
6+ "pending p W = {i \<in> branches p. i \<notin> W \<and> \<not> fits p W i 8}"
7+
8+definition widen :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat set" where
9+ "widen p W = W \<union> pending p W"
10+
11+lemma widen_extensive: "W \<subseteq> widen p W"
12+ by (auto simp: widen_def)
13+
14+lemma widen_bounded:
15+ "W \<subseteq> branches p \<Longrightarrow> widen p W \<subseteq> branches p"
16+ by (auto simp: widen_def pending_def)
17+
18+lemma widen_decreases:
19+ assumes "widen p W \<noteq> W"
20+ shows "card (branches p - widen p W) < card (branches p - W)"
21+proof (rule psubset_card_mono)
22+ show "finite (branches p - W)" by simp
23+ show "branches p - widen p W \<subset> branches p - W"
24+ using assms unfolding widen_def pending_def by auto
25+qed
26+
27+function settle :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat set" where
28+ "settle p W = (if widen p W = W then W else settle p (widen p W))"
29+ by pat_completeness auto
30+termination
31+ by (relation "measure (\<lambda>(p,W). card (branches p - W))")
32+ (auto intro: widen_decreases)
33+
34+declare settle.simps [simp del]
35+
36+lemma settle_fixed: "widen p (settle p W) = settle p W"
37+ by (induction p W rule: settle.induct) (subst (1 2) settle.simps, auto)
38+
39+lemma settle_extensive: "W \<subseteq> settle p W"
40+proof (induction p W rule: settle.induct)
41+ case (1 p W)
42+ show ?case
43+ proof (cases "widen p W = W")
44+ case True
45+ show ?thesis by (subst settle.simps) (simp add: True)
46+ next
47+ case False
48+ have "widen p W \<subseteq> settle p (widen p W)" using "1.IH" False by simp
49+ then have sub: "W \<subseteq> settle p (widen p W)" using widen_extensive[of W p] by blast
50+ show ?thesis by (subst settle.simps) (simp add: False sub)
51+ qed
52+qed
53+
54+lemma settle_bounded:
55+ "W \<subseteq> branches p \<Longrightarrow> settle p W \<subseteq> branches p"
56+proof (induction p W rule: settle.induct)
57+ case (1 p W)
58+ show ?case
59+ proof (cases "widen p W = W")
60+ case True
61+ show ?thesis by (subst settle.simps) (simp add: True "1.prems")
62+ next
63+ case False
64+ have bounded: "widen p W \<subseteq> branches p" by (rule widen_bounded[OF "1.prems"])
65+ have rec: "settle p (widen p W) \<subseteq> branches p" by (rule "1.IH"[OF False bounded])
66+ show ?thesis by (subst settle.simps) (simp add: False rec)
67+ qed
68+qed
69+
70+lemma widen_necessary:
71+ assumes "valid p V" "W \<subseteq> V"
72+ shows "widen p W \<subseteq> V"
73+proof
74+ fix i
75+ assume member: "i \<in> widen p W"
76+ show "i \<in> V"
77+ proof (cases "i \<in> W")
78+ case True
79+ with assms show ?thesis by blast
80+ next
81+ case False
82+ with member have branch: "i \<in> branches p" and bad: "\<not> fits p W i 8"
83+ by (auto simp: widen_def pending_def)
84+ show ?thesis
85+ proof (rule ccontr)
86+ assume "i \<notin> V"
87+ with assms(1) branch have "fits p V i 8" by (auto simp: valid_def)
88+ then have "fits p W i 8" by (rule fits_downward[OF assms(2)])
89+ with bad show False by contradiction
90+ qed
91+ qed
92+qed
93+
94+lemma settle_least:
95+ assumes "valid p V" "W \<subseteq> V"
96+ shows "settle p W \<subseteq> V"
97+ using assms
98+proof (induction p W rule: settle.induct)
99+ case (1 p W)
100+ show ?case
101+ proof (cases "widen p W = W")
102+ case True
103+ show ?thesis by (subst settle.simps) (simp add: True "1.prems")
104+ next
105+ case False
106+ have necessary: "widen p W \<subseteq> V" by (rule widen_necessary[OF "1.prems"])
107+ have rec: "settle p (widen p W) \<subseteq> V" by (rule "1.IH"[OF False "1.prems"(1) necessary])
108+ show ?thesis by (subst settle.simps) (simp add: False rec)
109+ qed
110+qed
111+
112+definition layout :: "nat instruction list \<Rightarrow> nat set" where
113+ "layout p = settle p {}"
114+
115+lemma layout_bounded: "layout p \<subseteq> branches p"
116+ unfolding layout_def by (rule settle_bounded) simp
117+
118+lemma layout_least: "valid p V \<Longrightarrow> layout p \<subseteq> V"
119+ unfolding layout_def by (rule settle_least) auto
120+
121+lemma layout_short:
122+ "i \<in> branches p \<Longrightarrow> i \<notin> layout p \<Longrightarrow> fits p (layout p) i 8"
123+ using settle_fixed[of p "{}"] unfolding layout_def widen_def pending_def by auto
124+
125+theorem layout_complete:
126+ "valid p (layout p) \<longleftrightarrow> (\<exists>V. valid p V)"
127+proof
128+ assume "valid p (layout p)"
129+ then show "\<exists>V. valid p V" by blast
130+next
131+ assume "\<exists>V. valid p V"
132+ then obtain V where v: "valid p V" by blast
133+ have sub: "layout p \<subseteq> V" by (rule layout_least[OF v])
134+ have "\<forall>i\<in>branches p. fits p (layout p) i (if i \<in> layout p then 16 else 8)"
135+ using v sub layout_short fits_downward[OF sub]
136+ unfolding valid_def by (auto split: if_splits)
137+ with layout_bounded show "valid p (layout p)" by (simp add: valid_def)
138+qed
139+
140+theorem layout_minimum:
141+ "valid p V \<Longrightarrow> address p (layout p) (length p) \<le> address p V (length p)"
142+ by (intro address_mono layout_least)
143+
144+end

tests/Examples.thy added

@@ -0,0 +1,74 @@
1+theory Examples
2+ imports "../src/Frontend"
3+begin
4+
5+definition cascade :: "nat instruction list" where
6+ "cascade = [Jump 127, Jump 130] @ replicate 128 Nop @ [Stop]"
7+
8+definition countdown :: "nat instruction list" where
9+ "countdown = [Inc, Inc, Inc, Dec, Zero 6, Jump 3, Stop]"
10+
11+definition forward :: "nat \<Rightarrow> nat instruction list" where
12+ "forward n = [Jump (Suc n)] @ replicate n Nop @ [Stop]"
13+
14+definition backward :: "nat \<Rightarrow> nat instruction list" where
15+ "backward n = replicate n Nop @ [Jump 0, Stop]"
16+
17+lemma cascade_rounds:
18+ "map (\<lambda>W. filter (\<lambda>i. i \<in> W) [0..<length cascade]) (history cascade {}) = [[], [1], [0,1]]"
19+ by eval
20+
21+lemma cascade_size: "map_option length (assemble cascade) = Some 135"
22+ by eval
23+
24+lemma forward_short: "layout (forward 127) = {}"
25+ by eval
26+
27+lemma forward_long: "layout (forward 128) = {0}"
28+ by eval
29+
30+lemma backward_short: "layout (backward 126) = {}"
31+ by eval
32+
33+lemma backward_long: "layout (backward 127) = {127}"
34+ by eval
35+
36+lemma countdown_execution:
37+ "execute (source_step countdown) 32 (0,0) = (6,0)"
38+ by eval
39+
40+lemma countdown_bytes:
41+ "assemble countdown = Some [1,1,1,2,17,130,16,123,3]"
42+ by eval
43+
44+lemma short_negative_boundary:
45+ "decode [16,0] = Some (Branch False False (-128), [])"
46+ by eval
47+
48+lemma long_negative_boundary:
49+ "decode [18,0,0] = Some (Branch False True (-32768), [])"
50+ by eval
51+
52+lemma long_positive_boundary:
53+ "decode [18,255,255] = Some (Branch False True 32767, [])"
54+ by eval
55+
56+lemma truncated_rejected: "decode [18,1] = None"
57+ by eval
58+
59+lemma unknown_rejected: "decode [255] = None"
60+ by eval
61+
62+lemma undefined_rejected:
63+ "compile ''jmp missing'' = Error ''undefined label missing''"
64+ by eval
65+
66+lemma duplicate_rejected:
67+ "compile (''label a'' @ newline @ ''label a'') = Error ''duplicate label a''"
68+ by eval
69+
70+lemma final_label_rejected:
71+ "compile (''jmp end'' @ newline @ ''label end'') = Error ''branch targets a label after the final instruction''"
72+ by eval
73+
74+end

tests/cli.py added

@@ -0,0 +1,162 @@
1+import itertools
2+from pathlib import Path
3+import random
4+import subprocess
5+import tempfile
6+
7+
8+ROOT = Path(__file__).resolve().parents[1]
9+CHECKS = 0
10+
11+
12+def check(condition, message):
13+ global CHECKS
14+ if not condition:
15+ raise AssertionError(message)
16+ CHECKS += 1
17+
18+
19+def cli(*args, text=None, ok=True):
20+ result = subprocess.run(
21+ [str(ROOT / "span"), *map(str, args)],
22+ input=text,
23+ text=True,
24+ capture_output=True,
25+ timeout=90,
26+ cwd=ROOT,
27+ )
28+ check((result.returncode == 0) == ok, (args, result.stdout, result.stderr))
29+ return result.stdout if ok else result.stderr
30+
31+
32+def source(program):
33+ lines = []
34+ for i, (op, target) in enumerate(program):
35+ lines.append(f"label b{i}")
36+ lines.append(f"{op} b{target}" if op in ("jmp", "jz") else op)
37+ return "\n".join(lines) + "\n"
38+
39+
40+def layouts(program):
41+ branches = [i for i, (op, _) in enumerate(program) if op in ("jmp", "jz")]
42+ for flags in itertools.product((False, True), repeat=len(branches)):
43+ wide = dict(zip(branches, flags))
44+ positions = [0]
45+ for i in range(len(program)):
46+ positions.append(positions[-1] + (3 if wide.get(i) else 2 if i in wide else 1))
47+ if all(
48+ -(32768 if wide[i] else 128)
49+ <= positions[program[i][1]] - positions[i + 1]
50+ < (32768 if wide[i] else 128)
51+ for i in branches
52+ ):
53+ yield positions[-1]
54+
55+
56+def interpret(program, fuel):
57+ pc, acc = 0, 0
58+ for _ in range(fuel):
59+ if pc >= len(program) or program[pc][0] == "halt":
60+ break
61+ op, target = program[pc]
62+ if op == "inc":
63+ acc += 1
64+ elif op == "dec":
65+ acc = max(0, acc - 1)
66+ if op == "jmp" or op == "jz" and acc == 0:
67+ pc = target
68+ else:
69+ pc += 1
70+ return pc, acc
71+
72+
73+def decode(data):
74+ rows, at = [], 0
75+ while at < len(data):
76+ start, op = at, data[at]
77+ at += 1
78+ if op in (16, 17, 18, 19):
79+ length = 2 if op < 18 else 3
80+ payload = int.from_bytes(data[at : at + length - 1], "little")
81+ at += length - 1
82+ rows.append((start, at, op, payload - (128 if length == 2 else 32768)))
83+ else:
84+ check(op in (0, 1, 2, 3), "invalid opcode")
85+ rows.append((start, at, op, None))
86+ return rows
87+
88+
89+def verify(program, data):
90+ rows = decode(data)
91+ check(len(rows) == len(program), "instruction count changed")
92+ for (op, target), (_, end, opcode, displacement) in zip(program, rows):
93+ if op in ("jmp", "jz"):
94+ check(opcode in ((16, 18) if op == "jmp" else (17, 19)), "branch kind changed")
95+ check(end + displacement == rows[target][0], "branch destination changed")
96+ else:
97+ check(opcode == {"nop": 0, "inc": 1, "dec": 2, "halt": 3}[op], "opcode changed")
98+ check(len(data) == min(layouts(program)), "layout is not minimum")
99+ return rows
100+
101+
102+def main():
103+ check("usage:" in cli("--help"), "help missing")
104+ check("135 bytes" in cli("assemble", "examples/cascade.span"), "cascade size")
105+ trace = cli("trace", "examples/cascade.span")
106+ check("pass 0 133 bytes widen [1]" in trace, "first cascade pass")
107+ check("pass 1 134 bytes widen [0]" in trace, "second cascade pass")
108+ check("pass 2 135 bytes widen []" in trace, "fixed point missing")
109+ check("halted pc=8 acc=0" in cli("run", "examples/countdown.span"), "countdown execution")
110+ check("fuel exhausted" in cli("run", "examples/countdown.span", "1"), "fuel limit")
111+ check("fuel exhausted pc=0 acc=0" in cli("run", "-", "5", text="label loop\njmp loop"), "self branch")
112+ for text, message in [
113+ ("jmp nowhere", "undefined label"),
114+ ("label a\nlabel a", "duplicate label"),
115+ ("jmp end\nlabel end", "after the final instruction"),
116+ ("pad -1", "invalid padding"),
117+ ("pad 65537", "invalid padding"),
118+ ("pad 65536\nnop", "exceeds 65536"),
119+ ("jmp", "invalid instruction"),
120+ ("halt extra", "invalid instruction"),
121+ ("label \x1b[31m", "printable ASCII"),
122+ ]:
123+ check(message in cli("assemble", "-", text=text, ok=False), message)
124+ check("16-bit range" in cli("assemble", "examples/overflow.span", ok=False), "overflow accepted")
125+ for padding, width in [(127, 2), (128, 3), (32767, 3)]:
126+ report = cli("assemble", "-", text=f"jmp end\npad {padding}\nlabel end\nhalt")
127+ check(f"{padding + width + 1} bytes" in report, "forward range boundary")
128+ for padding, width in [(126, 2), (127, 3), (32765, 3)]:
129+ report = cli("assemble", "-", text=f"label start\npad {padding}\njmp start\nhalt")
130+ check(f"{padding + width + 1} bytes" in report, "backward range boundary")
131+ check("16-bit range" in cli("assemble", "-", text="label start\npad 32766\njmp start\nhalt", ok=False), "negative overflow accepted")
132+ rng = random.Random(0x5350414E)
133+ with tempfile.TemporaryDirectory() as directory:
134+ out = Path(directory) / "program.bin"
135+ for case in range(36):
136+ length = rng.randrange(8, 180)
137+ program = [(rng.choice(("nop", "inc", "dec")), None) for _ in range(length)]
138+ for i in rng.sample(range(length - 1), rng.randrange(1, 7)):
139+ program[i] = (rng.choice(("jmp", "jz")), rng.randrange(length))
140+ program[-1] = ("halt", None)
141+ text = source(program)
142+ cli("assemble", "-", "-o", out, text=text)
143+ rows = verify(program, out.read_bytes())
144+ pc, acc = interpret(program, 256)
145+ expected = rows[pc][0] if pc < length else len(out.read_bytes())
146+ report = cli("run", "-", "256", text=text)
147+ check(f"pc={expected} acc={acc}\n" in report, f"execution mismatch in case {case}")
148+ cli("assemble", "examples/countdown.span", "-o", out)
149+ check(out.read_bytes() == bytes([1, 1, 1, 2, 17, 130, 16, 123, 3]), "binary output")
150+ check("jmp.8 -5" in cli("disassemble", out), "binary disassembly")
151+ out.write_bytes(bytes([18, 0]))
152+ check("invalid encoding" in cli("disassemble", out, ok=False), "truncated encoding accepted")
153+ out.write_bytes(bytes([255]))
154+ check("invalid encoding" in cli("disassemble", out, ok=False), "unknown opcode accepted")
155+ out.write_bytes(b"preserve")
156+ cli("assemble", "-", "-o", out, text="jmp missing", ok=False)
157+ check(out.read_bytes() == b"preserve", "failed assembly clobbered output")
158+ print(f"{CHECKS} checks passed, including 36 exhaustive layout comparisons")
159+
160+
161+if __name__ == "__main__":
162+ main()