commit a68ad347f48eb214044370b3ca67d33d9b3c9a6d Author: james Date: Sat Oct 31 06:50:40 2026 +0000 initial commit diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..78e8a1c --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +/.build/ +__pycache__/ diff --git a/Encoding.thy b/Encoding.thy new file mode 120000 index 0000000..bb9d2ce --- /dev/null +++ b/Encoding.thy @@ -0,0 +1 @@ +src/Encoding.thy \ No newline at end of file diff --git a/Machine.thy b/Machine.thy new file mode 120000 index 0000000..012666a --- /dev/null +++ b/Machine.thy @@ -0,0 +1 @@ +src/Machine.thy \ No newline at end of file diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..eda4323 --- /dev/null +++ b/Makefile @@ -0,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 diff --git a/README.md b/README.md new file mode 100644 index 0000000..7eba9b3 --- /dev/null +++ b/README.md @@ -0,0 +1,15 @@ +# Span + +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.gif)](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) + +![](media/correspondence.svg) + +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 diff --git a/ROOT b/ROOT new file mode 100644 index 0000000..60aa483 --- /dev/null +++ b/ROOT @@ -0,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 diff --git a/Relax.thy b/Relax.thy new file mode 120000 index 0000000..db1f5e3 --- /dev/null +++ b/Relax.thy @@ -0,0 +1 @@ +src/Relax.thy \ No newline at end of file diff --git a/cli/driver.ML b/cli/driver.ML new file mode 100644 index 0000000..8d724a6 --- /dev/null +++ b/cli/driver.ML @@ -0,0 +1,57 @@ +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 stream = if path = "-" then TextIO.stdIn else TextIO.openIn path + val text = TextIO.inputN (stream, 1048577) + val _ = if path = "-" then () else TextIO.closeIn stream + in + if size text > 1048576 then raise Fail "input exceeds 1 MiB" else text + end; + +fun write path text = + let + val stream = BinIO.openOut path + val _ = BinIO.output (stream, Byte.stringToBytes text) + in BinIO.closeOut stream 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 input = chars (read file) + val (ok, bytes) = Span.binary input + in + if ok then + (write destination (text bytes); + output (Span.process [chars "assemble"] input)) + else output (false, bytes) + 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); diff --git a/examples/backward.span b/examples/backward.span new file mode 100644 index 0000000..15fb150 --- /dev/null +++ b/examples/backward.span @@ -0,0 +1,4 @@ +label start +pad 127 +jmp start +halt diff --git a/examples/cascade.span b/examples/cascade.span new file mode 100644 index 0000000..4691e09 --- /dev/null +++ b/examples/cascade.span @@ -0,0 +1,8 @@ +jmp near +jmp far +pad 125 +label near +nop +pad 2 +label far +halt diff --git a/examples/countdown.span b/examples/countdown.span new file mode 100644 index 0000000..3c2ca6d --- /dev/null +++ b/examples/countdown.span @@ -0,0 +1,9 @@ +inc +inc +inc +label loop +dec +jz done +jmp loop +label done +halt diff --git a/examples/overflow.span b/examples/overflow.span new file mode 100644 index 0000000..3027415 --- /dev/null +++ b/examples/overflow.span @@ -0,0 +1,4 @@ +jmp end +pad 32768 +label end +halt diff --git a/media/correspondence.svg b/media/correspondence.svg new file mode 100644 index 0000000..32bd883 --- /dev/null +++ b/media/correspondence.svg @@ -0,0 +1,32 @@ + + Execution correspondence + 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 + + + + + + + + wellformed p · valid p W · i ≤ |p| + + s + RW(s) + Sk(s) + Bk(RW(s)) + + + RW + RW + Sk + Bk + + s = (i, a)    RW(i, a) = (addrW(i), a) + + + + + + + + diff --git a/media/demo.gif b/media/demo.gif new file mode 100644 index 0000000..88c7a91 Binary files /dev/null and b/media/demo.gif differ diff --git a/media/demo.mp4 b/media/demo.mp4 new file mode 100644 index 0000000..7cdd96b Binary files /dev/null and b/media/demo.mp4 differ diff --git a/span b/span new file mode 100755 index 0000000..81c5b03 --- /dev/null +++ b/span @@ -0,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" "$@" diff --git a/src/Encoding.thy b/src/Encoding.thy new file mode 100644 index 0000000..081b918 --- /dev/null +++ b/src/Encoding.thy @@ -0,0 +1,129 @@ +theory Encoding + imports Relax +begin + +datatype operation = Idle | Raise | Lower | Finish | Branch bool bool int + +fun bytesize :: "operation \ nat" where + "bytesize (Branch c wide d) = (if wide then 3 else 2)" +| "bytesize _ = 1" + +fun encodable :: "operation \ bool" where + "encodable (Branch c wide d) = (if wide then -32768 \ d \ d < 32768 else -128 \ d \ d < 128)" +| "encodable _ = True" + +fun encode :: "operation \ 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 \ (operation \ 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 \ b = 17 then + (case bs of [] \ None | x # xs \ + if x < 256 then Some (Branch (b = 17) False (int x - 128), xs) else None) + else if b = 18 \ b = 19 then + (case bs of x # y # xs \ + if x < 256 \ y < 256 then Some (Branch (b = 19) True (int (y * 256 + x) - 32768), xs) else None + | _ \ 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 \ set (encode op) \ {..<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) + +fun lower :: "nat instruction list \ nat set \ nat \ nat instruction \ 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 \ W) (displacement p W i)" +| "lower p W i (Zero t) = Branch True (i \ W) (displacement p W i)" + +definition chunks :: "nat instruction list \ nat set \ nat list list" where + "chunks p W = map (\i. encode (lower p W i (p ! i))) [0.. nat set \ nat list" where + "bytecode p W = concat (chunks p W)" + +lemma chunks_code [code]: + "chunks p W = map (\(i,op). encode (lower p W i op)) (zip [0.. 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 \ i < length p \ 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 \ chunks p W ! i = encode (lower p W i (p ! i))" + by (simp add: chunks_def) + +lemma prefix_length: + "i \ length p \ 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) \ {..<256}" +proof - + have each: "\i. i < length p \ set (encode (lower p W i (p ! i))) \ {..<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 diff --git a/src/Export.thy b/src/Export.thy new file mode 100644 index 0000000..01fd65a --- /dev/null +++ b/src/Export.thy @@ -0,0 +1,11 @@ +theory Export + imports Frontend +begin + +definition ascii :: "integer \ char" where "ascii = char_of" + +definition ordinal :: "char \ integer" where "ordinal = of_char" + +export_code process binary disassemble ascii ordinal in SML module_name Span file_prefix span + +end diff --git a/src/Frontend.thy b/src/Frontend.thy new file mode 100644 index 0000000..c96b2db --- /dev/null +++ b/src/Frontend.thy @@ -0,0 +1,201 @@ +theory Frontend + imports Machine "HOL-Library.Code_Target_Numeral" +begin + +datatype 'a result = Error string | Ok 'a + +fun bind :: "'a result \ ('a \ 'b result) \ 'b result" where + "bind (Error e) f = Error e" +| "bind (Ok x) f = f x" + +function decimal :: "nat \ 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 \ string \ string list" where + "separate c [] = [[]]" +| "separate c (x # xs) = (if x = c then [] # separate c xs else + case separate c xs of [] \ [[x]] | y # ys \ (x # y) # ys)" + +definition words :: "string \ string list" where + "words s = filter (\x. x \ []) (separate CHR '' '' + (map (\c. if c = CHR 0x09 \ c = CHR 0x0D then CHR '' '' else c) s))" + +definition number :: "string \ nat option" where + "number s = (if s \ [] \ list_all (\c. 48 \ nat_of_char c \ nat_of_char c < 58) s then + let n = foldl (\n c. min 65537 (10 * n + nat_of_char c - 48)) 0 s in + if n \ 65536 then Some n else None else None)" + +datatype statement = Label string | Emit "string instruction" | Pad nat + +definition parse_line :: "nat \ string list \ statement list result" where + "parse_line n tokens = (let bad = Error (''invalid instruction at line '' @ decimal n) in + case tokens of [] \ Ok [] + | [a] \ 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] \ 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 \ Error (''invalid padding at line '' @ decimal n) | Some k \ Ok [Pad k]) + else bad + | _ \ bad)" + +fun parse_lines :: "nat \ string list \ statement list result" where + "parse_lines n [] = Ok []" +| "parse_lines n (s # ss) = bind (parse_line n (words s)) (\xs. + bind (parse_lines (Suc n) ss) (\ys. Ok (xs @ ys)))" + +fun count :: "statement \ nat" where + "count (Label l) = 0" +| "count (Emit op) = 1" +| "count (Pad n) = n" + +fun collect :: "statement list \ nat \ (string \ nat) list \ (string \ nat) list result" where + "collect [] pc env = Ok env" +| "collect (Label l # ss) pc env = (if map_of env l \ 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 \ nat) list \ string instruction \ 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 \ Error (''undefined label '' @ l) | Some t \ Ok (Jump t))" +| "resolve env (Zero l) = (case map_of env l of None \ Error (''undefined label '' @ l) | Some t \ Ok (Zero t))" + +fun resolve_all :: "(string \ nat) list \ statement list \ 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) (\x. + bind (resolve_all env ss) (\xs. Ok (x # xs)))" +| "resolve_all env (Pad n # ss) = bind (resolve_all env ss) (\xs. Ok (replicate n Nop @ xs))" + +definition source :: "string \ nat instruction list result" where + "source s = (if \ list_all (\c. let n = nat_of_char c in + n = 9 \ n = 10 \ n = 13 \ (32 \ n \ n < 127)) s + then Error ''source must contain printable ASCII, tabs, or line endings'' else + bind (parse_lines 1 (separate CHR 0x0A s)) (\ss. + if sum_list (map count ss) > 65536 then Error ''program exceeds 65536 instructions'' + else bind (collect ss 0 []) (\env. bind (resolve_all env ss) (\p. + if wellformed p then Ok p else Error ''branch targets a label after the final instruction''))))" + +definition checked :: "nat instruction list \ nat list result" where + "checked p = (if \ 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 \ assemble p = Some code" + by (auto simp: checked_def assemble_def Let_def split: if_splits) + +theorem checked_execution: + "checked p = Ok code \ + 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 \ nat set \ 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 (\(p,W). card (branches p - W))") (auto intro: widen_decreases) + +declare history.simps [simp del] + +lemma history_nonempty: "history p W \ []" + 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 \ string" where + "hexbyte n = [''0123456789abcdef'' ! (n div 16 mod 16), ''0123456789abcdef'' ! (n mod 16)]" + +fun joined :: "string \ string list \ string" where + "joined sep [] = []" +| "joined sep (x # xs) = x @ (if xs = [] then [] else sep @ joined sep xs)" + +definition hex :: "nat list \ string" where + "hex bs = joined '' '' (map hexbyte bs)" + +definition signed :: "int \ string" where + "signed n = (if n < 0 then ''-'' @ decimal (nat (-n)) else ''+'' @ decimal (nat n))" + +fun opname :: "operation \ 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 \ nat set \ nat \ 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 \ nat \ nat set \ string" where + "passline p n W = ''pass '' @ decimal n @ '' '' @ decimal (address p W (length p)) @ + '' bytes widen ['' @ joined '', '' (map decimal (filter (\i. i \ pending p W) [0..i. i \ branches p) [0.. string" where + "trace p = (let hs = history p {} in concat (map (\i. passline p i (hs ! i)) [0.. nat list \ string" where + "summary p bs = decimal (length p) @ '' instructions, '' @ decimal (length bs) @ '' bytes, '' @ + decimal (card (layout p)) @ '' long branches'' @ newline" + +definition compile :: "string \ nat list result" where + "compile s = bind (source s) checked" + +theorem compile_sound: + "compile s = Ok code \ \p. source s = Ok p \ assemble p = Some code" + unfolding compile_def by (cases "source s") (auto simp: checked_assemble) + +theorem checked_failure: + "wellformed p \ checked p = Error e \ \ (\W. valid p W)" + using assembly_complete[of p] + by (auto simp: checked_def assemble_def split: if_splits) + +definition stopped :: "nat list \ nat \ nat \ string" where + "stopped bs s = (case map_option fst (decode (drop (fst s) bs)) of + Some Finish \ ''halted'' | _ \ if machine_step bs s = None then ''fault'' else ''fuel exhausted'')" + +definition runreport :: "nat list \ nat \ 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 \ nat list \ string result" where + "listing pc bs = (if bs = [] then Ok [] else case decode bs of None \ Error (''invalid encoding at byte '' @ decimal pc) + | Some (op,rest) \ if length rest < length bs then + bind (listing (pc + bytesize op) rest) (\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 (\(pc,bs). length bs)") auto + +definition binary :: "string \ bool \ string" where + "binary s = (case compile s of Error e \ (False, e @ newline) | Ok bs \ (True, map char_of_nat bs))" + +definition disassemble :: "string \ bool \ string" where + "disassemble s = (case listing 0 (map nat_of_char s) of Error e \ (False,e @ newline) | Ok text \ (True,text))" + +definition inspect :: "string list \ nat instruction list \ nat list \ bool \ string" where + "inspect args p bs = (let bad = (False, ''usage: span {assemble|trace|list|run} file [fuel]'' @ newline) in + case args of [mode] \ + 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 \ (False,e @ newline) | Ok s \ (True,s)) + else bad + | [mode,n] \ if mode = ''run'' then + (case number n of None \ (False,''fuel must be between 0 and 65536'' @ newline) + | Some fuel \ (True, runreport bs fuel)) else bad + | _ \ bad)" + +definition process :: "string list \ string \ bool \ string" where + "process args s = (case source s of Error e \ (False, e @ newline) | Ok p \ + case checked p of Error e \ (False, (if args = [''trace''] then trace p else []) @ e @ newline) + | Ok bs \ inspect args p bs)" + +end diff --git a/src/Layout.thy b/src/Layout.thy new file mode 100644 index 0000000..266d0b2 --- /dev/null +++ b/src/Layout.thy @@ -0,0 +1,151 @@ +theory Layout + imports Model +begin + +definition width :: "nat instruction list \ nat set \ nat \ nat" where + "width p W i = (if i \ branches p then if i \ W then 3 else 2 else 1)" + +definition address :: "nat instruction list \ nat set \ nat \ nat" where + "address p W i = (\j nat set \ nat \ nat" where + "distance p W i = (let t = destination p i in + if i < t then (\j\{Suc i..j\{t.. nat set \ nat \ nat \ bool" where + "fits p W i bits \ + (if i < destination p i then distance p W i < 2 ^ (bits - 1) + else distance p W i \ 2 ^ (bits - 1))" + +definition displacement :: "nat instruction list \ nat set \ nat \ int" where + "displacement p W i = int (address p W (destination p i)) - int (address p W (Suc i))" + +definition valid :: "nat instruction list \ nat set \ bool" where + "valid p W \ W \ branches p \ + (\i\branches p. fits p W i (if i \ 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 \ target (p ! i) \ None then if i \ W then 3 else 2 else 1)" + by (simp add: width_def branches_def) + +definition sizes :: "nat instruction list \ nat set \ nat list" where + "sizes p W = map (\(i,op). if target op = None then 1 else if i \ W then 3 else 2) + (zip [0.. sizes p W ! i = width p W i" + by (simp add: sizes_def width_def branches_def) + +lemma width_mono: "W \ V \ width p W i \ 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 \ V \ address p W i \ address p V i" + unfolding address_def by (intro sum_mono width_mono) assumption + +lemma distance_mono: + "W \ V \ distance p W i \ 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 \ V \ fits p V i bits \ fits p W i bits" + using distance_mono[of W V p i] unfolding fits_def by auto + +lemma prefix_interval: + fixes f :: "nat \ nat" + assumes "a \ b" + shows "(\jjj\{a.. {a.. {a.. destination p i" by simp + have eq: "int (\jjj\{Suc i.. Suc i" by simp + have eq: "int (\jjj\{destination p i.. + - int (2 ^ (bits - 1)) \ displacement p W i \ + displacement p W i < int (2 ^ (bits - 1))" +proof - + have positive: "(0::int) < int (2 ^ (bits - 1) :: nat)" by simp + have nonnegative: "(0::int) \ int (distance p W i)" by simp + have lower: "- int (2 ^ (bits - 1)) \ 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 < (\k\{i.. nat \ nat \ (nat \ 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 \ a \ 0 then Some (next, a) + else if 0 \ int next + d then Some (nat (int next + d), a) else None)" + +definition machine_step :: "nat list \ nat \ nat \ (nat \ nat) option" where + "machine_step code s = (case map_option fst (decode (drop (fst s) code)) of + None \ None | Some op \ machine_advance op (fst s) (snd s))" + +definition relocate :: "nat instruction list \ nat set \ nat \ nat \ nat \ 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 \ i \ length p \ source_step p (i,a) = Some (j,b) \ j \ 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 \ 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 \ 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 \ nat list option" where + "assemble p = (if wellformed p \ valid p (layout p) then Some (bytecode p (layout p)) else None)" + +theorem assembly_complete: + "assemble p \ None \ wellformed p \ (\W. valid p W)" + by (simp add: assemble_def layout_complete) + +theorem assembly_minimum: + "assemble p = Some code \ valid p V \ length code \ 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 diff --git a/src/Model.thy b/src/Model.thy new file mode 100644 index 0000000..4745c0e --- /dev/null +++ b/src/Model.thy @@ -0,0 +1,46 @@ +theory Model + imports Main +begin + +datatype 'a instruction = Nop | Inc | Dec | Stop | Jump 'a | Zero 'a + +fun target :: "'a instruction \ 'a option" where + "target (Jump t) = Some t" +| "target (Zero t) = Some t" +| "target _ = None" + +definition branches :: "nat instruction list \ nat set" where + "branches p = {i. i < length p \ target (p ! i) \ None}" + +definition destination :: "nat instruction list \ nat \ nat" where + "destination p i = the (target (p ! i))" + +definition wellformed :: "nat instruction list \ bool" where + "wellformed p \ (\i \ branches p. destination p i < length p)" + +lemma finite_branches [simp]: "finite (branches p)" + unfolding branches_def by (rule finite_subset[of _ "{.. branches p \ i < length p" + by (simp add: branches_def) + +lemma branches_code [code]: + "branches p = set (map fst (filter (\(i,op). target op \ None) (zip [0.. nat \ nat \ (nat \ 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 \ nat \ nat \ (nat \ 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 \ 's option) \ nat \ 's \ 's" where + "execute step 0 s = s" +| "execute step (Suc n) s = (case step s of None \ s | Some t \ execute step n t)" + +end diff --git a/src/Relax.thy b/src/Relax.thy new file mode 100644 index 0000000..1daddc7 --- /dev/null +++ b/src/Relax.thy @@ -0,0 +1,144 @@ +theory Relax + imports Layout +begin + +definition pending :: "nat instruction list \ nat set \ nat set" where + "pending p W = {i \ branches p. i \ W \ \ fits p W i 8}" + +definition widen :: "nat instruction list \ nat set \ nat set" where + "widen p W = W \ pending p W" + +lemma widen_extensive: "W \ widen p W" + by (auto simp: widen_def) + +lemma widen_bounded: + "W \ branches p \ widen p W \ branches p" + by (auto simp: widen_def pending_def) + +lemma widen_decreases: + assumes "widen p W \ 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 \ branches p - W" + using assms unfolding widen_def pending_def by auto +qed + +function settle :: "nat instruction list \ nat set \ 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 (\(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 \ 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 \ settle p (widen p W)" using "1.IH" False by simp + then have sub: "W \ 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 \ branches p \ settle p W \ 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 \ branches p" by (rule widen_bounded[OF "1.prems"]) + have rec: "settle p (widen p W) \ 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 \ V" + shows "widen p W \ V" +proof + fix i + assume member: "i \ widen p W" + show "i \ V" + proof (cases "i \ W") + case True + with assms show ?thesis by blast + next + case False + with member have branch: "i \ branches p" and bad: "\ fits p W i 8" + by (auto simp: widen_def pending_def) + show ?thesis + proof (rule ccontr) + assume "i \ 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 \ V" + shows "settle p W \ 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 \ V" by (rule widen_necessary[OF "1.prems"]) + have rec: "settle p (widen p W) \ 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 \ nat set" where + "layout p = settle p {}" + +lemma layout_bounded: "layout p \ branches p" + unfolding layout_def by (rule settle_bounded) simp + +lemma layout_least: "valid p V \ layout p \ V" + unfolding layout_def by (rule settle_least) auto + +lemma layout_short: + "i \ branches p \ i \ layout p \ 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) \ (\V. valid p V)" +proof + assume "valid p (layout p)" + then show "\V. valid p V" by blast +next + assume "\V. valid p V" + then obtain V where v: "valid p V" by blast + have sub: "layout p \ V" by (rule layout_least[OF v]) + have "\i\branches p. fits p (layout p) i (if i \ 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 \ address p (layout p) (length p) \ address p V (length p)" + by (intro address_mono layout_least) + +end diff --git a/tests/Examples.thy b/tests/Examples.thy new file mode 100644 index 0000000..b115372 --- /dev/null +++ b/tests/Examples.thy @@ -0,0 +1,74 @@ +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 \ nat instruction list" where + "forward n = [Jump (Suc n)] @ replicate n Nop @ [Stop]" + +definition backward :: "nat \ nat instruction list" where + "backward n = replicate n Nop @ [Jump 0, Stop]" + +lemma cascade_rounds: + "map (\W. filter (\i. i \ W) [0..= 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") + 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}") + cli("assemble", "examples/countdown.span", "-o", out) + 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") + cli("assemble", "-", "-o", out, text="jmp missing", ok=False) + check(out.read_bytes() == b"preserve", "failed assembly clobbered output") + print(f"{CHECKS} checks passed, including 36 exhaustive layout comparisons") + + +if __name__ == "__main__": + main()