A => .gitignore +2 -0
@@ 1,2 @@
+/.build/
+__pycache__/
A => Makefile +31 -0
@@ 1,31 @@
+ISABELLE ?= isabelle
+
+.PHONY: all check measure payload guest clean
+
+all: .build/ready
+
+.build/ready: ROOT $(wildcard src/*.thy src/core/*.thy) cli/driver.ML Makefile
+ @test "$$('$(ISABELLE)' version)" = Isabelle2026
+ "$(ISABELLE)" build -D . -j 1 -o threads=1 -o parallel_proofs=0
+ "$(ISABELLE)" export -n -d . -O .build -x 'Remy.Export:code/remy.ML' Remy
+ REMY_ROOT="$(CURDIR)" "$$('$(ISABELLE)' getenv -b POLYML_HOME)/$$('$(ISABELLE)' getenv -b ISABELLE_PLATFORM64)/polyc" -o .build/remy cli/driver.ML
+ @touch $@
+
+check: all
+ python3 tests/native.py
+ python3 tests/cli.py
+ python3 tests/live.py
+
+measure: all
+ python3 tests/measure.py
+
+payload: all
+ @mkdir -p .build/payload
+ @set -e; for name in Rings Weave Cells; do .build/remy examples/$$name.remy .build/payload/$$name.BIN; .build/remy vectors examples/$$name.remy .build/payload/$$name.DAT; cp examples/$$name.remy .build/payload/$$name.TXT; done
+ cp guest/Remy.HC .build/payload/Remy.HC
+
+guest: payload
+ python3 tests/guest.py "$(TEMPLE_ISO)"
+
+clean:
+ rm -rf .build
A => README.md +70 -0
@@ 1,70 @@
+Pixel expressions compile to native x86-64 for TempleOS through an Isabelle/HOL compiler, with proofs of constant folding, register allocation, bounded branching and instruction-level execution of the emitted bytes
+
+[](media/demo.mp4)
+
+## Build
+
+```sh
+make check
+make payload
+```
+
+It uses:
+- Isabelle2026 and its bundled Poly/ML toolchain
+- Python
+
+Copy `.build/payload/*` onto `C:/` in TempleOS and run:
+
+```c
+#include "C:/Remy.HC";
+Verify;
+Show(0);
+```
+
+## Usage
+
+The byte interpreter follows encoded jumps and consumes a synthetic return address through `ret`. Compare its result with `eval` using the same `x`, `y` and `t` arguments
+
+```sh
+.build/remy examples/Rings.remy /tmp/rings.bin
+.build/remy simulate /tmp/rings.bin 17 23 41
+.build/remy eval examples/Rings.remy 17 23 41
+```
+
+Both evaluations return `3`. `make measure` compares the original stack backend with the current compiler on the three examples and reports bytes, static stack instructions and median host pixel-kernel time
+
+## Live
+
+The HOL packet builder serialises native code, its source snapshot and 512 reference rows for the trusted local compiler. The guest checks lengths, a checksum and every reference result before switching shaders between frames
+
+`make guest` tests a copy of an official TempleOS RedSea ISO and leaves a bootable image that starts `Live(0)` automatically. Start that image with COM1 attached to a Unix socket, then edit the watched source file
+
+```sh
+make guest TEMPLE_ISO=/path/to/TempleOS.ISO
+qemu-system-x86_64 -m 512 -smp 2 -cdrom .build/guest.iso \
+ -chardev socket,id=live,path=/tmp/remy.sock,server=on,wait=off \
+ -serial chardev:live &
+python3 cli/watch.py examples/Rings.remy --socket /tmp/remy.sock
+```
+
+The watcher keeps one transfer in flight and coalesces edits while awaiting its acknowledgement. Syntax errors and rejected packets leave the current shader running, and Escape stops the guest renderer and receiver
+
+## Correctness
+
+Lexical bindings share the evaluation stack with spilled intermediates. The [allocator](src/Allocation.thy) keeps one intermediate in a register and adjusts variable offsets when it must spill, while the [branching compiler](src/Branches.thy) preserves the incoming frame and returns the expression result
+
+The [encoder](src/core/Encoding.thy) proves inversion and byte bounds for immediate operands and stack displacements, while [native lowering](src/core/Native.thy) uses the following register convention to keep pixel inputs available across expression evaluation
+
+| Registers | Role |
+| --- | --- |
+| `r8`, `r9`, `rdx` | Preserved inputs `x`, `y`, `t` |
+| `rax` | Accumulator and result |
+| `rcx`, `rbx` | Scratch |
+
+
+
+Arithmetic wraps modulo `2^64` and shifts mask their count to six bits
+
+Nonconstant conditionals use forward `jz` and `jmp` instructions so only the selected arm runs. The validator checks both arms for matching stack heights and protected input registers, with a proved [512-word bound](src/Bounds.thy) above the caller frame. The HolyC runner masks each result to four bits for the TempleOS palette
+
+The [x86 model](src/X86.thy) follows the [Intel instruction descriptions](https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html) for the emitted subset using a word-addressed stack. The proved function body preserves its incoming stack and pointer, then `ret` removes the return address and advances that pointer by eight bytes. Arithmetic flags that the compiler never reads are abstracted, and hardware faults, the HolyC bridge, extraction and the OS remain outside the proof
A => ROOT +24 -0
@@ 1,24 @@
+session Remybase in "src/core" = HOL +
+ options [document = false]
+ sessions "HOL-Library"
+ theories
+ "HOL-Library.Word"
+ "HOL-Library.Code_Target_Numeral"
+ Model
+ Compiler
+ Native
+ Encoding
+ Checker
+
+session Remy in src = Remybase +
+ options [document = false]
+ sessions "HOL-Library"
+ theories
+ Allocation
+ Branches
+ Bounds
+ X86
+ Frontend
+ Delivery
+ Examples
+ Export
A => cli/driver.ML +82 -0
@@ 1,82 @@
+val root = valOf (OS.Process.getEnv "REMY_ROOT");
+val _ = use (root ^ "/.build/Remy.Export/code/remy.ML");
+
+fun chars s = map (Remy.ascii o IntInf.fromInt o Char.ord) (String.explode s);
+fun text cs = String.implode (map (Char.chr o IntInf.toInt o Remy.ordinal) cs);
+
+fun read path =
+ let
+ val stream = if path = "-" then TextIO.stdIn else TextIO.openIn path
+ fun close () = if path = "-" then () else TextIO.closeIn stream
+ val input = TextIO.inputN (stream, 65537)
+ handle exn => (close (); raise exn)
+ val _ = close ()
+ in
+ if size input > 65536 then raise Fail "source exceeds 64 KiB" else chars input
+ end;
+
+fun write path data =
+ let
+ val bytes = Byte.stringToBytes (text data)
+ val pid = SysWord.toString (Posix.Process.pidToWord (Posix.ProcEnv.getpid ()))
+ val prefix = OS.Path.concat (OS.Path.dir path, "." ^ OS.Path.file path ^ "." ^ pid ^ ".")
+ val defaultMode = Posix.FileSys.S.flags [Posix.FileSys.S.irusr, Posix.FileSys.S.iwusr,
+ Posix.FileSys.S.irgrp, Posix.FileSys.S.iwgrp, Posix.FileSys.S.iroth, Posix.FileSys.S.iwoth]
+ val mode = Posix.FileSys.S.intersect [Posix.FileSys.ST.mode (Posix.FileSys.stat path),
+ Posix.FileSys.S.flags [Posix.FileSys.S.irwxu, Posix.FileSys.S.irwxg, Posix.FileSys.S.irwxo]]
+ handle exn as OS.SysErr (_, SOME error) =>
+ if error = Posix.Error.noent then defaultMode else raise exn
+ fun reserve n =
+ if n = 128 then raise Fail "cannot reserve output file"
+ else
+ let
+ val temporary = prefix ^ Int.toString n
+ in
+ (temporary, Posix.FileSys.createf
+ (temporary, Posix.FileSys.O_WRONLY, Posix.FileSys.O.excl, mode))
+ end handle exn as OS.SysErr (_, SOME error) =>
+ if error = Posix.Error.exist then reserve (n + 1) else raise exn
+ val (temporary, fd) = reserve 0
+ val closed = ref false
+ fun close () = (Posix.IO.close fd; closed := true)
+ fun discard () =
+ ((if !closed then () else close ()) handle _ => ();
+ OS.FileSys.remove temporary handle _ => ())
+ fun loop offset =
+ if offset = Word8Vector.length bytes then ()
+ else
+ let
+ val count = Posix.IO.writeVec (fd, Word8VectorSlice.slice (bytes, offset, NONE))
+ in
+ if count = 0 then raise Fail "output write made no progress" else loop (offset + count)
+ end
+ in
+ (loop 0; close (); OS.FileSys.rename {old = temporary, new = path})
+ handle exn => (discard (); raise exn)
+ end;
+
+fun output (ok, message) =
+ (TextIO.output (if ok then TextIO.stdOut else TextIO.stdErr, text message);
+ if ok then () else OS.Process.exit OS.Process.failure);
+
+fun emit destination ((ok, bytes), report) =
+ if ok then (write destination bytes; output (true,report)) else output (false,report);
+
+fun main () =
+ (case CommandLine.arguments () of
+ ["vectors", source, destination] =>
+ (case Remy.vectors (read source) of (true, bytes) => write destination bytes | result => output result)
+ | ["package", revision, source, destination] =>
+ emit destination (Remy.delivery (chars revision) (read source))
+ | ["eval", source, x, y, t] => output (Remy.reference (read source) (chars x) (chars y) (chars t))
+ | ["simulate", binary, x, y, t] => output (Remy.simulate (read binary) (chars x) (chars y) (chars t))
+ | ["limits", depth, nodes, stack, source, destination] =>
+ emit destination (Remy.configured (chars depth) (chars nodes) (chars stack) (read source))
+ | ["check", binary] => output (Remy.validate (read binary))
+ | ["disassemble", binary] => output (Remy.disassemble (read binary))
+ | ["baseline", source, destination] => emit destination (Remy.baseline (read source))
+ | [source, destination] => emit destination (Remy.artifact (read source))
+ | _ => raise Fail "usage: remy check binary | remy disassemble binary | remy simulate binary x y t | remy package revision source packet | remy baseline source binary | remy limits depth nodes stack source binary | remy source binary | remy vectors source data | remy eval source x y t (source - reads standard input)")
+ handle exn =>
+ (TextIO.output (TextIO.stdErr, "remy: " ^ General.exnMessage exn ^ "\n");
+ OS.Process.exit OS.Process.failure);
A => cli/watch.py +151 -0
@@ 1,151 @@
+import argparse
+import os
+from pathlib import Path
+import secrets
+import socket
+import struct
+import subprocess
+import sys
+import tempfile
+import time
+
+
+ROOT = Path(__file__).resolve().parents[1]
+MAGIC = b'RMA1'
+
+
+def snapshot(path):
+ with path.open('rb') as stream:
+ before = os.fstat(stream.fileno())
+ data = stream.read(65537)
+ after = path.stat()
+ if (before.st_ino, before.st_size, before.st_mtime_ns) != (after.st_ino, after.st_size, after.st_mtime_ns):
+ return None
+ if len(data) > 65536:
+ raise ValueError('source exceeds 64 KiB')
+ return data
+
+
+def compile_packet(compiler, source, revision, directory):
+ path, packet = directory / 'source', directory / 'packet'
+ path.write_bytes(source)
+ with subprocess.Popen([compiler, 'package', str(revision), path, packet],
+ stdout=subprocess.PIPE, stderr=subprocess.PIPE, text=True) as process:
+ try:
+ _, error = process.communicate(timeout=30)
+ except BaseException:
+ process.kill()
+ process.communicate()
+ raise
+ if process.returncode:
+ raise ValueError(error.strip())
+ return packet.read_bytes()
+
+
+def watch(source, endpoint, compiler, interval):
+ previous = None
+ packet = None
+ connection = None
+ flight = None
+ completed = None
+ sent = 0.0
+ revision = secrets.randbelow((1 << 32) - 1) + 1
+ replies = bytearray()
+ next_connection = 0.0
+ source_error = None
+ with tempfile.TemporaryDirectory() as directory:
+ directory = Path(directory)
+ try:
+ while True:
+ try:
+ data = snapshot(source)
+ source_error = None
+ if data is not None and data != previous:
+ previous = data
+ candidate = revision % ((1 << 32) - 1) + 1
+ try:
+ compiled = compile_packet(compiler, data, candidate, directory)
+ packet, revision = compiled, candidate
+ print(f'revision {revision}: compiled', flush=True)
+ except (ValueError, subprocess.TimeoutExpired) as error:
+ print(error, file=sys.stderr, flush=True)
+ except (OSError, ValueError) as error:
+ message = str(error)
+ if message != source_error:
+ print(message, file=sys.stderr, flush=True)
+ source_error = message
+ try:
+ if connection is None:
+ if time.monotonic() < next_connection:
+ time.sleep(interval)
+ continue
+ connection = socket.socket(socket.AF_UNIX, socket.SOCK_STREAM)
+ connection.settimeout(1)
+ connection.connect(str(endpoint))
+ connection.settimeout(interval)
+ flight = None
+ completed = None
+ sent = 0.0
+ replies.clear()
+ if packet is not None and flight is None and revision != completed:
+ connection.settimeout(180)
+ connection.sendall(packet)
+ connection.settimeout(interval)
+ flight = revision
+ sent = time.monotonic()
+ if flight is not None and time.monotonic() - sent > 180:
+ raise TimeoutError('guest acknowledgement timed out')
+ try:
+ chunk = connection.recv(4096)
+ if not chunk:
+ raise ConnectionError('guest disconnected')
+ replies.extend(chunk)
+ except socket.timeout:
+ pass
+ while len(replies) >= 16:
+ if replies[:4] != MAGIC:
+ del replies[0]
+ continue
+ _, received, status, active = struct.unpack('<4sIII', replies[:16])
+ del replies[:16]
+ if received == 0 and status == 0:
+ completed = None
+ flight = None
+ elif received == flight:
+ completed = received
+ flight = None
+ print(f'revision {received}: ' + ('accepted' if status == 1 else f'rejected ({status}); active {active}'),
+ flush=True)
+ except OSError as error:
+ if connection is not None:
+ connection.close()
+ if sent:
+ print(str(error), file=sys.stderr, flush=True)
+ next_connection = time.monotonic() + (6 if sent else interval)
+ connection = None
+ sent = 0.0
+ time.sleep(interval)
+ finally:
+ if connection is not None:
+ connection.close()
+
+
+def main():
+ parser = argparse.ArgumentParser()
+ parser.add_argument('source', type=Path)
+ parser.add_argument('--socket', required=True, type=Path)
+ parser.add_argument('--compiler', type=Path, default=ROOT / '.build/remy')
+ parser.add_argument('--interval', type=float, default=0.25)
+ args = parser.parse_args()
+ if not 0.01 <= args.interval <= 10:
+ parser.error('interval must be between 0.01 and 10 seconds')
+ if not args.compiler.is_file() or not os.access(args.compiler, os.X_OK):
+ parser.error('build an executable compiler with make first')
+ try:
+ watch(args.source, args.socket, args.compiler.resolve(), args.interval)
+ except KeyboardInterrupt:
+ pass
+
+
+if __name__ == '__main__':
+ main()
A => examples/Cells.remy +5 -0
@@ 1,5 @@
+(let u (+ x (shr t 2))
+ (let cell (xor (shr u 4) (shr y 4))
+ (if (< (and cell 3) 1)
+ (and (+ (xor u y) t) 15)
+ (and (shr (+ (* u u) (* y y)) 7) 15))))
A => examples/Rings.remy +4 -0
@@ 1,4 @@
+(let dx (- x 80)
+ (let dy (- y 56)
+ (let radius (+ (* dx dx) (* dy dy))
+ (and (shr (+ radius (* t 32)) 6) 15))))
A => examples/Weave.remy +3 -0
@@ 1,3 @@
+(let drift (+ y (shr t 1))
+ (let warp (xor (* x drift) (* (+ x t) y))
+ (and (xor (shr warp 5) (shr (+ x drift) 3)) 15)))
A => guest/Remy.HC +322 -0
@@ 1,322 @@
+asm {
+_REMY::
+ PUSH RBP
+ MOV RBP,RSP
+ MOV RAX,U64 SF_ARG1[RBP]
+ MOV R8,U64 SF_ARG2[RBP]
+ MOV R9,U64 SF_ARG3[RBP]
+ MOV RDX,U64 SF_ARG4[RBP]
+ CALL RAX
+ POP RBP
+ RET1 32
+}
+
+_extern _REMY U64 Pixel(U8 *code,U64 x,U64 y,U64 t);
+
+U8 *names[3]={"Rings","Weave","Cells"};
+CDC *image=NULL;
+U8 *shader=NULL;
+U8 *program=NULL;
+I64 selected;
+U8 *directory="C:/";
+U8 *incoming=NULL;
+I64 received=0,expected=0;
+U32 synchronise=0,revision=0;
+I64 display_lock=0,reply_lock=0,transfer=0;
+CTask *receiver=NULL;
+Bool live_mode=FALSE;
+F64 last_received;
+
+U0 Reply(U32 sequence,U32 status)
+{
+ U32 words[4];
+ I64 i;
+ F64 until;
+ U8 *bytes=words;
+ while (LBts(&reply_lock,0)) Yield;
+ words[0]=0x31414D52;
+ words[1]=sequence;
+ words[2]=status;
+ words[3]=revision;
+ for (i=0;i<16;i++) {
+ until=tS()+0.1;
+ while (!(InU8(0x3FD)&0x20)) {
+ if (tS()>until) {
+ LBtr(&reply_lock,0);
+ return;
+ }
+ }
+ OutU8(0x3F8,bytes[i]);
+ }
+ LBtr(&reply_lock,0);
+}
+
+U64 Checksum(U8 *bytes,I64 size,U64 value=14695981039346656037)
+{
+ I64 i;
+ for (i=0;i<size;i++) value=(value^bytes[i])*1099511628211;
+ return value;
+}
+
+U0 Accept()
+{
+ U32 *header=incoming;
+ U64 sum,*rows;
+ U8 *next_code=NULL,*next_source=NULL,*old_code,*old_source;
+ I64 i;
+ Bool matches=TRUE;
+ sum=Checksum(incoming,20);
+ sum=Checksum(incoming+28,expected-28,sum);
+ if (sum!=*(incoming+20)(U64 *)) {
+ Reply(header[4],2);
+ return;
+ }
+ if (header[4]==revision) {
+ Reply(header[4],1);
+ return;
+ }
+ try {
+ next_code=MAlloc(header[1]);
+ next_source=CAlloc(header[2]+1);
+ MemCpy(next_code,incoming+28,header[1]);
+ MemCpy(next_source,incoming+28+header[1],header[2]);
+ rows=(incoming+28+header[1]+header[2])(U64 *);
+ for (i=0;i<512;i++) {
+ if (Pixel(next_code,rows[4*i],rows[4*i+1],rows[4*i+2])!=rows[4*i+3]) {
+ matches=FALSE;
+ break;
+ }
+ }
+ if (matches) {
+ while (LBts(&display_lock,0)) Yield;
+ old_code=shader;
+ old_source=program;
+ shader=next_code;
+ program=next_source;
+ next_code=NULL;
+ next_source=NULL;
+ revision=header[4];
+ LBtr(&display_lock,0);
+ Free(old_code);
+ Free(old_source);
+ Reply(header[4],1);
+ } else Reply(header[4],3);
+ Free(next_code);
+ Free(next_source);
+ } catch {
+ Free(next_code);
+ Free(next_source);
+ Reply(header[4],3);
+ }
+}
+
+U0 Poll()
+{
+ I64 i;
+ U64 byte;
+ F64 until;
+ U32 *header=incoming;
+ if (received && tS()-last_received>5) {
+ received=0;
+ expected=0;
+ synchronise=0;
+ }
+ if (!(InU8(0x3FD)&1)) return;
+ until=tS()+0.004;
+ for (i=0;i<8192;) {
+ if (!(InU8(0x3FD)&1)) {
+ if (tS()>=until) break;
+ goto skip;
+ }
+ byte=InU8(0x3F8)&255;
+ i++;
+ last_received=tS();
+ if (received<4) {
+ synchronise=(synchronise>>8)|(byte(U32)<<24);
+ if (synchronise==0x31594D52) {
+ header[0]=synchronise;
+ received=4;
+ }
+ goto skip;
+ }
+ incoming[received++]=byte;
+ if (received==28) {
+ if (!header[1] || header[1]>65536 || !header[2] || header[2]>65536 ||
+ header[3]!=512 || !header[4]) {
+ Reply(header[4],4);
+ received=0;
+ expected=0;
+ synchronise=0;
+ goto skip;
+ }
+ expected=28+header[1]+header[2]+16384;
+ }
+ if (expected && received==expected) {
+ LBts(&transfer,0);
+ break;
+ }
+skip:;
+ }
+}
+
+U0 Receive(U8 *)
+{
+ while (TRUE) {
+ if (Bt(&transfer,0)) Sleep(1);
+ else {
+ Poll();
+ if (!received) Sleep(1);
+ else Yield;
+ }
+ }
+}
+
+Bool Verify()
+{
+ I64 i,j,size,total=0;
+ U8 *code=NULL,path[64];
+ U64 *rows=NULL;
+ try {
+ for (i=0;i<3;i++) {
+ StrPrint(path,"%s%s.BIN",directory,names[i]);
+ code=FileRead(path,&size);
+ if (!code) throw('Code');
+ "%-6s %d bytes ",names[i],size;
+ StrPrint(path,"%s%s.DAT",directory,names[i]);
+ rows=FileRead(path,&size);
+ if (!rows || size!=16384) throw('Vectors');
+ for (j=0;j<size/32;j++) {
+ if (Pixel(code,rows[4*j],rows[4*j+1],rows[4*j+2])!=rows[4*j+3]) {
+ throw('Mismatch');
+ }
+ total++;
+ }
+ "%d comparisons passed\n",size/32;
+ Free(rows);
+ rows=NULL;
+ Free(code);
+ code=NULL;
+ }
+ } catch {
+ Free(rows);
+ Free(code);
+ "verification failed after %d cases\n",total;
+ return FALSE;
+ }
+ "native results match HOL evaluation (%d cases)\n",total;
+ return TRUE;
+}
+
+U0 Draw(CTask *,CDC *dc)
+{
+ U8 *title="live";
+ if (!live_mode) title=names[selected];
+ if (LBts(&display_lock,0)) return;
+ try {
+ dc->color=BLUE;
+ GrPrint(dc,80,24,"remy %s revision %d",title,revision);
+ dc->color=BLACK;
+ GrBlot(dc,80,64,image);
+ GrPrint(dc,80,416,"%s",program);
+ LBtr(&display_lock,0);
+ } catch {
+ LBtr(&display_lock,0);
+ }
+}
+
+U0 Release(Bool restore)
+{
+ Fs->draw_it=NULL;
+ if (receiver) {
+ Kill(receiver);
+ receiver=NULL;
+ }
+ while (LBts(&display_lock,0)) Yield;
+ if (restore) SettingsPop;
+ DCDel(image);
+ image=NULL;
+ Free(shader);
+ shader=NULL;
+ Free(program);
+ program=NULL;
+ Free(incoming);
+ incoming=NULL;
+ LBtr(&display_lock,0);
+}
+
+U0 Show(I64 which=0,Bool live=FALSE)
+{
+ I64 x,y,dy,t=0,cpu=0,key;
+ U8 color,path[64];
+ Bool restore=FALSE;
+ if (!(0<=which<3)) return;
+ try {
+ selected=which;
+ live_mode=live;
+ StrPrint(path,"%s%s.BIN",directory,names[which]);
+ shader=FileRead(path);
+ if (!shader) throw('Code');
+ StrPrint(path,"%s%s.TXT",directory,names[which]);
+ program=FileRead(path);
+ if (!program) throw('Source');
+ image=DCNew(480,336);
+ if (live) {
+ incoming=CAlloc(147484);
+ received=0;
+ expected=0;
+ synchronise=0;
+ revision=0;
+ OutU8(0x3F9,0);
+ OutU8(0x3FB,0x80);
+ OutU8(0x3F8,1);
+ OutU8(0x3F9,0);
+ OutU8(0x3FB,3);
+ OutU8(0x3FA,7);
+ OutU8(0x3FC,3);
+ transfer=0;
+ if (mp_cnt>1) cpu=1;
+ receiver=Spawn(&Receive,NULL,"remy uart",cpu);
+ if (!receiver) throw('Receiver');
+ Reply(0,0);
+ }
+ SettingsPush;
+ restore=TRUE;
+ AutoComplete(OFF);
+ WinMax;
+ DocClear;
+ FlushMsgs;
+ Fs->draw_it=&Draw;
+ while (TRUE) {
+ key=ScanChar();
+ if (key && (!live || key==CH_ESC)) break;
+ if (live && Bt(&transfer,0)) {
+ Accept();
+ received=0;
+ expected=0;
+ synchronise=0;
+ LBtr(&transfer,0);
+ }
+ for (y=0;y<112;y++) {
+ for (x=0;x<160;x++) {
+ color=Pixel(shader,x,y,t)&15;
+ for (dy=0;dy<3;dy++)
+ MemSet(image->body+(3*y+dy)*480+3*x,color,3);
+ }
+ }
+ t+=2;
+ Refresh;
+ Sleep(20);
+ }
+ } catch {
+ PutExcept;
+ Release(restore);
+ return;
+ }
+ Release(restore);
+ DocClear;
+}
+
+U0 Live(I64 which=0)
+{
+ Show(which,TRUE);
+}
A => media/correspondence.svg +19 -0
@@ 1,19 @@
+<svg xmlns="http://www.w3.org/2000/svg" width="720" height="208" viewBox="0 0 720 208" role="img" aria-labelledby="title description">
+ <title id="title">Compiler execution correspondence</title>
+ <desc id="description">Source evaluation agrees with instruction execution of emitted bytes, with RAX containing the result and the caller frame preserved</desc>
+ <defs><marker id="arrow" viewBox="0 0 10 10" refX="9" refY="5" markerWidth="6" markerHeight="6" orient="auto-start-reverse"><path d="M 0 0 L 10 5 L 0 10 z" fill="#555"/></marker></defs>
+ <rect width="720" height="208" fill="white"/>
+ <g fill="none" stroke="#555" stroke-width="1" marker-end="url(#arrow)">
+ <path d="M 176 45 H 547"/><path d="M 140 64 V 143"/><path d="M 582 143 V 64"/><path d="M 176 164 H 547"/>
+ </g>
+ <g fill="white" stroke="#555">
+ <rect x="62" y="25" width="114" height="40" rx="3"/><rect x="547" y="25" width="113" height="40" rx="3"/>
+ <rect x="38" y="144" width="138" height="40" rx="3"/><rect x="547" y="144" width="138" height="40" rx="3"/>
+ </g>
+ <g font-family="STIX Two Text, Libertinus Serif, Georgia, serif" font-size="15" fill="#222" text-anchor="middle">
+ <text x="119" y="50">expression</text><text x="603" y="50">64-bit value</text>
+ <text x="107" y="169">emitted bytes</text><text x="616" y="169">RAX + frame</text>
+ <text x="360" y="35">source evaluation</text><text x="360" y="153">x86 instruction execution</text>
+ <text x="360" y="106">folding · allocation · branches · encoding</text>
+ </g>
+</svg>
A => media/demo.gif +0 -0
A => media/demo.mp4 +0 -0
A => media/poster.png +0 -0
A => src/Allocation.thy +123 -0
@@ 1,123 @@
+theory Allocation
+ imports "Remybase.Checker"
+begin
+
+fun allocate :: "bool \<Rightarrow> expression \<Rightarrow> nat list \<Rightarrow> opcode list" where
+ "allocate free (Literal v) slots = [Immediate v]"
+| "allocate free (Input i) slots = [Move Rax (input_register i)]"
+| "allocate free (Variable i) slots = [Peek (slots ! i)]"
+| "allocate free (Binary op a b) slots = (if free then
+ allocate True a slots @ [Move Rbx Rax] @ allocate False b slots @
+ [Move Rcx Rbx, Arithmetic op]
+ else allocate False a slots @ [Push Rax] @ allocate False b (map Suc slots) @
+ [Pop Rcx, Arithmetic op])"
+| "allocate free (Cond c a b) slots = [Push Rbx] @
+ allocate True c (map Suc slots) @ [Push Rax] @
+ allocate True a (map (\<lambda>i. Suc (Suc i)) slots) @ [Push Rax] @
+ allocate True b (map (\<lambda>i. Suc (Suc (Suc i))) slots) @
+ [Pop Rcx, Pop Rbx, Conditional, Pop Rbx]"
+| "allocate free (Let a b) slots = allocate free a slots @ [Push Rax] @
+ allocate free b (0 # map Suc slots) @ [Pop Rcx]"
+
+definition allocated_result :: "bool \<Rightarrow> expression \<Rightarrow> pixel list \<Rightarrow> machine \<Rightarrow> machine \<Rightarrow> bool" where
+ "allocated_result free e env s q \<longleftrightarrow>
+ registers q Rax = evaluate e env (inputs s) \<and> stack q = stack s \<and>
+ inputs q = inputs s \<and> (\<not> free \<longrightarrow> registers q Rbx = registers s Rbx)"
+
+theorem allocate_correct:
+ assumes "scoped (length env) e" "represents slots (stack s) env"
+ shows "\<exists>q. run (allocate free e slots) s = Some q \<and> allocated_result free e env s q"
+ using assms
+proof (induction e arbitrary: free slots env s)
+ case (Literal v)
+ then show ?case by (auto simp: allocated_result_def)
+next
+ case (Input i)
+ then show ?case by (auto simp: allocated_result_def inputs_def fun_eq_iff)
+next
+ case (Variable i)
+ then show ?case by (auto simp: allocated_result_def represents_def)
+next
+ case (Binary op a b)
+ obtain p where a: "run (allocate free a slots) s = Some p"
+ and p: "allocated_result free a env s p"
+ using Binary.IH(1)[of env slots s free] Binary.prems by auto
+ show ?case
+ proof (cases free)
+ case True
+ let ?p = "p\<lparr>registers := (registers p)(Rbx := registers p Rax)\<rparr>"
+ obtain q where b: "run (allocate False b slots) ?p = Some q"
+ and q: "allocated_result False b env ?p q"
+ using Binary.IH(2)[of env slots ?p False] Binary.prems p
+ by (auto simp: allocated_result_def)
+ show ?thesis using a b p q True
+ by (auto simp: allocated_result_def run_append; auto simp: inputs_def fun_eq_iff)
+ next
+ case False
+ let ?p = "p\<lparr>stack := registers p Rax # stack p\<rparr>"
+ obtain q where b: "run (allocate False b (map Suc slots)) ?p = Some q"
+ and q: "allocated_result False b env ?p q"
+ using Binary.IH(2)[of env "map Suc slots" ?p False] Binary.prems p
+ represents_push[OF Binary.prems(2), of "registers p Rax"]
+ by (auto simp: allocated_result_def)
+ show ?thesis using a b p q False
+ by (auto simp: allocated_result_def run_append; auto simp: inputs_def fun_eq_iff)
+ qed
+next
+ case (Cond c a b)
+ have sc: "scoped (length env) c" and sa: "scoped (length env) a"
+ and sb: "scoped (length env) b" using Cond.prems by auto
+ let ?s = "s\<lparr>stack := registers s Rbx # stack s\<rparr>"
+ have repc: "represents (map Suc slots) (stack ?s) env"
+ using represents_push[OF Cond.prems(2)] by simp
+ obtain p where c: "run (allocate True c (map Suc slots)) ?s = Some p"
+ and p: "allocated_result True c env ?s p"
+ using Cond.IH(1)[of env "map Suc slots" ?s True] sc repc by blast
+ let ?p = "p\<lparr>stack := registers p Rax # stack p\<rparr>"
+ have repa: "represents (map (\<lambda>i. Suc (Suc i)) slots) (stack ?p) env"
+ using Cond.prems(2) p by (auto simp: allocated_result_def represents_def)
+ obtain q where a: "run (allocate True a (map (\<lambda>i. Suc (Suc i)) slots)) ?p = Some q"
+ and q: "allocated_result True a env ?p q"
+ using Cond.IH(2)[of env "map (\<lambda>i. Suc (Suc i)) slots" ?p True] sa repa by blast
+ let ?q = "q\<lparr>stack := registers q Rax # stack q\<rparr>"
+ have repb: "represents (map (\<lambda>i. Suc (Suc (Suc i))) slots) (stack ?q) env"
+ using Cond.prems(2) p q by (auto simp: allocated_result_def represents_def)
+ obtain r where b: "run (allocate True b (map (\<lambda>i. Suc (Suc (Suc i))) slots)) ?q = Some r"
+ and r: "allocated_result True b env ?q r"
+ using Cond.IH(3)[of env "map (\<lambda>i. Suc (Suc (Suc i))) slots" ?q True] sb repb by blast
+ show ?case using c a b p q r
+ by (auto simp: allocated_result_def run_append; auto simp: inputs_def fun_eq_iff)
+next
+ case (Let a b)
+ obtain p where a: "run (allocate free a slots) s = Some p"
+ and p: "allocated_result free a env s p"
+ using Let.IH(1)[of env slots s free] Let.prems by auto
+ let ?p = "p\<lparr>stack := registers p Rax # stack p\<rparr>"
+ obtain q where b: "run (allocate free b (0 # map Suc slots)) ?p = Some q"
+ and q: "allocated_result free b (registers p Rax # env) ?p q"
+ using Let.IH(2)[of "registers p Rax # env" "0 # map Suc slots" ?p free]
+ Let.prems p represents_bind[OF Let.prems(2), of "registers p Rax"]
+ by (auto simp: allocated_result_def)
+ show ?case using a b p q
+ by (auto simp: allocated_result_def run_append; auto simp: inputs_def fun_eq_iff)
+qed
+
+definition allocated :: "expression \<Rightarrow> opcode list" where
+ "allocated e = transfers (allocate True (optimise e) [])"
+
+theorem allocated_return:
+ "scoped 0 e \<Longrightarrow> \<exists>q. run (allocated e) s = Some q \<and>
+ registers q Rax = evaluate e [] (inputs s) \<and> stack q = stack s \<and> inputs q = inputs s"
+ using allocate_correct[where env="[]" and slots="[]" and free=True and e="optimise e"]
+ optimise_scoped
+ by (auto simp: allocated_def transfers_correct allocated_result_def represents_def optimise_correct)
+
+definition allocated_bytes :: "expression \<Rightarrow> nat list" where
+ "allocated_bytes e = concat (map encode (allocated e)) @ [195]"
+
+lemma allocated_add:
+ "allocated (Binary Add (Input X) (Input Y)) =
+ [Move Rax R8, Move Rbx Rax, Move Rax R9, Move Rcx Rbx, Arithmetic Add]"
+ by eval
+
+end
A => src/Bounds.thy +116 -0
@@ 1,116 @@
+theory Bounds
+ imports Branches
+begin
+
+fun guarded_run :: "nat \<Rightarrow> opcode list \<Rightarrow> machine \<Rightarrow> bool" where
+ "guarded_run limit [] s = (length (stack s) \<le> limit)"
+| "guarded_run limit (op # code) s = (length (stack s) \<le> limit \<and>
+ (case transition op s of None \<Rightarrow> False | Some q \<Rightarrow> guarded_run limit code q))"
+
+fun guarded_flow :: "nat \<Rightarrow> flow \<Rightarrow> machine \<Rightarrow> bool" where
+ "guarded_flow limit (Basic code) s = guarded_run limit code s"
+| "guarded_flow limit (Sequence a b) s = (guarded_flow limit a s \<and>
+ (case flowrun a s of None \<Rightarrow> False | Some q \<Rightarrow> guarded_flow limit b q))"
+| "guarded_flow limit (Choice a b) s = guarded_flow limit (if registers s Rax = 0 then b else a) s"
+
+lemma effect_shift:
+ "effect op n = Some m \<Longrightarrow> effect op (n + base) = Some (m + base)"
+ by (cases op; cases n; auto split: if_splits; arith)
+
+lemma effect_frame:
+ "effect op n = Some m \<Longrightarrow> transition op s = Some q \<Longrightarrow>
+ drop m (stack q) = drop n (stack s)"
+ by (cases op; cases n; cases "stack s") (auto simp: effect.simps transition.simps split: if_splits)
+
+lemma audit_limit:
+ "n \<le> 512 \<Longrightarrow> audit code n = Some m \<Longrightarrow> m \<le> 512"
+ by (induction code arbitrary: n) (auto split: if_splits bind_splits)
+
+lemma flowaudit_limit:
+ "n \<le> 512 \<Longrightarrow> flowaudit code n = Some m \<Longrightarrow> m \<le> 512"
+proof (induction code arbitrary: n m)
+ case (Basic code)
+ then show ?case by (auto dest: audit_limit)
+next
+ case (Sequence a b)
+ obtain k where a: "flowaudit a n = Some k" and b: "flowaudit b k = Some m"
+ using Sequence.prems(2) by (auto split: bind_splits)
+ have "k \<le> 512" using Sequence.IH(1)[OF Sequence.prems(1) a] .
+ then show ?case using Sequence.IH(2)[OF _ b] by blast
+next
+ case (Choice a b)
+ have "flowaudit a n = Some m"
+ using Choice.prems(2) by (auto split: option.splits if_splits)
+ then show ?case using Choice.IH(1)[OF Choice.prems(1)] by blast
+qed
+
+theorem audit_window:
+ assumes "length (stack s) = base + n" "n \<le> 512" "audit code n = Some m"
+ shows "\<exists>q. run code s = Some q \<and> length (stack q) = base + m \<and>
+ drop m (stack q) = drop n (stack s) \<and> guarded_run (base + 512) code s"
+ using assms
+proof (induction code arbitrary: s n m)
+ case Nil
+ then show ?case by auto
+next
+ case (Cons op code)
+ obtain k where effect: "effect op n = Some k" and bound: "k \<le> 512"
+ and tail: "audit code k = Some m"
+ using Cons.prems(3) by (auto split: if_splits bind_splits)
+ have shifted: "effect op (length (stack s)) = Some (base + k)"
+ using effect_shift[OF effect, of base] Cons.prems(1) by (simp add: add.commute)
+ obtain p where p: "transition op s = Some p" "length (stack p) = base + k"
+ using effect_sound[OF shifted] by blast
+ obtain q where q: "run code p = Some q" "length (stack q) = base + m"
+ "drop m (stack q) = drop k (stack p)" "guarded_run (base + 512) code p"
+ using Cons.IH[OF p(2) bound tail] by blast
+ have frame: "drop k (stack p) = drop n (stack s)"
+ using effect_frame[OF effect p(1)] .
+ have "length (stack s) \<le> base + 512" using Cons.prems(1,2) by arith
+ then show ?case using p q frame by auto
+qed
+
+theorem flow_window:
+ assumes "length (stack s) = base + n" "n \<le> 512" "flowaudit code n = Some m"
+ shows "\<exists>q. flowrun code s = Some q \<and> length (stack q) = base + m \<and>
+ drop m (stack q) = drop n (stack s) \<and> inputs q = inputs s \<and>
+ guarded_flow (base + 512) code s"
+ using assms
+proof (induction code arbitrary: s n m)
+ case (Basic code)
+ have audit: "audit code n = Some m" using Basic.prems by simp
+ obtain q where q: "run code s = Some q" "length (stack q) = base + m"
+ "drop m (stack q) = drop n (stack s)" "guarded_run (base + 512) code s"
+ using audit_window[OF Basic.prems(1,2) audit] by blast
+ show ?case using q audit_inputs[OF audit q(1)] by auto
+next
+ case (Sequence a b)
+ obtain k where a: "flowaudit a n = Some k" and b: "flowaudit b k = Some m"
+ using Sequence.prems(3) by (auto split: bind_splits)
+ obtain p where p: "flowrun a s = Some p" "length (stack p) = base + k"
+ "drop k (stack p) = drop n (stack s)" "inputs p = inputs s"
+ "guarded_flow (base + 512) a s"
+ using Sequence.IH(1)[OF Sequence.prems(1,2) a] by blast
+ have bound: "k \<le> 512" using flowaudit_limit[OF Sequence.prems(2) a] .
+ obtain q where q: "flowrun b p = Some q" "length (stack q) = base + m"
+ "drop m (stack q) = drop k (stack p)" "inputs q = inputs p"
+ "guarded_flow (base + 512) b p"
+ using Sequence.IH(2)[OF p(2) bound b] by blast
+ show ?case using p q by auto
+next
+ case (Choice a b)
+ have a: "flowaudit a n = Some m" and b: "flowaudit b n = Some m"
+ using Choice.prems(3) by (auto split: option.splits if_splits)
+ show ?case
+ using Choice.IH(1)[OF Choice.prems(1,2) a] Choice.IH(2)[OF Choice.prems(1,2) b]
+ by (cases "registers s Rax = 0") auto
+qed
+
+corollary checked_frame:
+ "flowaudit code 0 = Some 0 \<Longrightarrow> \<exists>q. flowrun code s = Some q \<and>
+ stack q = stack s \<and> inputs q = inputs s \<and>
+ guarded_flow (length (stack s) + 512) code s"
+ using flow_window[where s=s and base="length (stack s)" and n=0 and m=0 and code=code]
+ by auto
+
+end
A => src/Branches.thy +169 -0
@@ 1,169 @@
+theory Branches
+ imports Allocation
+begin
+
+datatype flow = Basic "opcode list" | Sequence flow flow | Choice flow flow
+
+fun flowrun :: "flow \<Rightarrow> machine \<Rightarrow> machine option" where
+ "flowrun (Basic code) s = run code s"
+| "flowrun (Sequence a b) s = Option.bind (flowrun a s) (flowrun b)"
+| "flowrun (Choice a b) s = flowrun (if registers s Rax = 0 then b else a) s"
+
+fun chain :: "flow list \<Rightarrow> flow" where
+ "chain [] = Basic []"
+| "chain (a # code) = Sequence a (chain code)"
+
+fun branch_allocate :: "bool \<Rightarrow> expression \<Rightarrow> nat list \<Rightarrow> flow" where
+ "branch_allocate free (Literal v) slots = Basic [Immediate v]"
+| "branch_allocate free (Input i) slots = Basic [Move Rax (input_register i)]"
+| "branch_allocate free (Variable i) slots = Basic [Peek (slots ! i)]"
+| "branch_allocate free (Binary op a b) slots = (if free then
+ chain [branch_allocate True a slots, Basic [Move Rbx Rax], branch_allocate False b slots,
+ Basic [Move Rcx Rbx, Arithmetic op]]
+ else chain [branch_allocate False a slots, Basic [Push Rax], branch_allocate False b (map Suc slots),
+ Basic [Pop Rcx, Arithmetic op]])"
+| "branch_allocate free (Cond c a b) slots = Sequence (branch_allocate free c slots)
+ (Choice (branch_allocate free a slots) (branch_allocate free b slots))"
+| "branch_allocate free (Let a b) slots = chain [branch_allocate free a slots, Basic [Push Rax],
+ branch_allocate free b (0 # map Suc slots), Basic [Pop Rcx]]"
+
+theorem branch_allocate_correct:
+ assumes "scoped (length env) e" "represents slots (stack s) env"
+ shows "\<exists>q. flowrun (branch_allocate free e slots) s = Some q \<and> allocated_result free e env s q"
+ using assms
+proof (induction e arbitrary: free slots env s)
+ case (Literal v)
+ then show ?case by (auto simp: allocated_result_def chain.simps)
+next
+ case (Input i)
+ then show ?case by (auto simp: allocated_result_def inputs_def fun_eq_iff)
+next
+ case (Variable i)
+ then show ?case by (auto simp: allocated_result_def represents_def)
+next
+ case (Binary op a b)
+ obtain p where a: "flowrun (branch_allocate free a slots) s = Some p"
+ and p: "allocated_result free a env s p"
+ using Binary.IH(1)[of env slots s free] Binary.prems by auto
+ show ?case
+ proof (cases free)
+ case True
+ let ?p = "p\<lparr>registers := (registers p)(Rbx := registers p Rax)\<rparr>"
+ obtain q where b: "flowrun (branch_allocate False b slots) ?p = Some q"
+ and q: "allocated_result False b env ?p q"
+ using Binary.IH(2)[of env slots ?p False] Binary.prems p
+ by (auto simp: allocated_result_def chain.simps)
+ show ?thesis using a b p q True
+ by (auto simp: allocated_result_def run_append flowrun.simps chain.simps; auto simp: inputs_def fun_eq_iff)
+ next
+ case False
+ let ?p = "p\<lparr>stack := registers p Rax # stack p\<rparr>"
+ obtain q where b: "flowrun (branch_allocate False b (map Suc slots)) ?p = Some q"
+ and q: "allocated_result False b env ?p q"
+ using Binary.IH(2)[of env "map Suc slots" ?p False] Binary.prems p
+ represents_push[OF Binary.prems(2), of "registers p Rax"]
+ by (auto simp: allocated_result_def chain.simps)
+ show ?thesis using a b p q False
+ by (auto simp: allocated_result_def run_append flowrun.simps chain.simps; auto simp: inputs_def fun_eq_iff)
+ qed
+next
+ case (Cond c a b)
+ obtain p where c: "flowrun (branch_allocate free c slots) s = Some p"
+ and p: "allocated_result free c env s p"
+ using Cond.IH(1)[of env slots s free] Cond.prems by auto
+ show ?case
+ using Cond.IH(2)[of env slots p free] Cond.IH(3)[of env slots p free]
+ Cond.prems c p
+ by (auto simp: allocated_result_def split: if_splits)
+next
+ case (Let a b)
+ obtain p where a: "flowrun (branch_allocate free a slots) s = Some p"
+ and p: "allocated_result free a env s p"
+ using Let.IH(1)[of env slots s free] Let.prems by auto
+ let ?p = "p\<lparr>stack := registers p Rax # stack p\<rparr>"
+ obtain q where b: "flowrun (branch_allocate free b (0 # map Suc slots)) ?p = Some q"
+ and q: "allocated_result free b (registers p Rax # env) ?p q"
+ using Let.IH(2)[of "registers p Rax # env" "0 # map Suc slots" ?p free]
+ Let.prems p represents_bind[OF Let.prems(2), of "registers p Rax"]
+ by (auto simp: allocated_result_def chain.simps)
+ show ?case using a b p q
+ by (auto simp: allocated_result_def run_append flowrun.simps chain.simps; auto simp: inputs_def fun_eq_iff)
+qed
+
+definition branching :: "expression \<Rightarrow> flow" where
+ "branching e = branch_allocate True (optimise e) []"
+
+theorem branching_return:
+ "scoped 0 e \<Longrightarrow> \<exists>q. flowrun (branching e) s = Some q \<and>
+ registers q Rax = evaluate e [] (inputs s) \<and> stack q = stack s \<and> inputs q = inputs s"
+ using branch_allocate_correct[where env="[]" and slots="[]" and free=True and e="optimise e"]
+ optimise_scoped
+ by (auto simp: branching_def allocated_result_def represents_def optimise_correct)
+
+fun flowaudit :: "flow \<Rightarrow> nat \<Rightarrow> nat option" where
+ "flowaudit (Basic code) n = audit code n"
+| "flowaudit (Sequence a b) n = Option.bind (flowaudit a n) (flowaudit b)"
+| "flowaudit (Choice a b) n = (case (flowaudit a n, flowaudit b n) of
+ (Some x,Some y) \<Rightarrow> if x = y then Some x else None | _ \<Rightarrow> None)"
+
+theorem flowaudit_sound:
+ "flowaudit code (length (stack s)) = Some n \<Longrightarrow>
+ \<exists>q. flowrun code s = Some q \<and> length (stack q) = n \<and> inputs q = inputs s"
+proof (induction code arbitrary: s n)
+ case (Basic code)
+ then show ?case using audit_sound audit_inputs by fastforce
+next
+ case (Sequence a b)
+ then show ?case by (auto split: option.splits bind_splits; fastforce)
+next
+ case (Choice a b)
+ then show ?case by (auto split: option.splits if_splits; fastforce)
+qed
+
+fun flowbytes :: "flow \<Rightarrow> nat list" where
+ "flowbytes (Basic code) = concat (map encode code)"
+| "flowbytes (Sequence a b) = flowbytes a @ flowbytes b"
+| "flowbytes (Choice a b) = [72,133,192,15,132] @ octets 4 (length (flowbytes a) + 5) @
+ flowbytes a @ [233] @ octets 4 (length (flowbytes b)) @ flowbytes b"
+
+fun flowvalid :: "flow \<Rightarrow> bool" where
+ "flowvalid (Basic code) = list_all encodable code"
+| "flowvalid (Sequence a b) = (flowvalid a \<and> flowvalid b)"
+| "flowvalid (Choice a b) = (flowvalid a \<and> flowvalid b \<and>
+ length (flowbytes a) + 5 < 2 ^ 31 \<and> length (flowbytes b) < 2 ^ 31)"
+
+lemma flowbytes_bytes: "set (flowbytes code) \<subseteq> {..<256}"
+ by (induction code) (auto dest: subsetD[OF encode_bytes] subsetD[OF octets_bytes])
+
+function unpack :: "nat \<Rightarrow> nat list \<Rightarrow> flow option" where
+ "unpack 0 bytes = (if bytes = [] then Some (Basic []) else None)"
+| "unpack (Suc fuel) bytes = (if bytes = [] then Some (Basic []) else
+ if take 5 bytes = [72,133,192,15,132] then
+ let offset = integer (take 4 (drop 5 bytes)); pos = 9 + (offset - 5);
+ count = integer (take 4 (drop (Suc pos) bytes)) in
+ if 9 \<le> length bytes \<and> 5 \<le> offset \<and> pos + 5 + count \<le> length bytes \<and>
+ bytes ! pos = 233 then
+ Option.bind (unpack fuel (take (offset - 5) (drop 9 bytes))) (\<lambda>a.
+ Option.bind (unpack fuel (take count (drop (pos + 5) bytes))) (\<lambda>b.
+ map_option (Sequence (Choice a b)) (unpack fuel (drop (pos + 5 + count) bytes))))
+ else None
+ else Option.bind (decode bytes) (\<lambda>(op,rest).
+ map_option (Sequence (Basic [op])) (unpack fuel rest)))"
+ by pat_completeness auto
+termination by (relation "measure (\<lambda>(fuel,bytes). fuel)") auto
+
+declare unpack.simps [simp del]
+
+definition inspect :: "nat list \<Rightarrow> flow option" where
+ "inspect bytes = (if bytes = [] \<or> last bytes \<noteq> 195 \<or> \<not> list_all (\<lambda>b. b < 256) bytes then None else
+ Option.bind (unpack (length bytes) (butlast bytes)) (\<lambda>code.
+ if flowvalid code \<and> flowbytes code = butlast bytes \<and> flowaudit code 0 = Some 0
+ then Some code else None))"
+
+theorem inspected_sound:
+ "inspect bytes = Some code \<Longrightarrow> \<exists>q. flowrun code (s\<lparr>stack := []\<rparr>) = Some q \<and>
+ stack q = [] \<and> inputs q = inputs s"
+ using flowaudit_sound[where s="s\<lparr>stack := []\<rparr>" and n=0]
+ by (auto simp: inspect_def split: if_splits option.splits bind_splits)
+
+end
A => src/Delivery.thy +41 -0
@@ 1,41 @@
+theory Delivery
+ imports Frontend
+begin
+
+definition checksum :: "nat list \<Rightarrow> pixel" where
+ "checksum bytes = foldl (\<lambda>h b. (h XOR word_of_nat b) * 1099511628211) 14695981039346656037 bytes"
+
+definition delivery :: "string \<Rightarrow> string \<Rightarrow> (bool \<times> string) \<times> string" where
+ "delivery sequence source = (case (number sequence,prepare source) of
+ (Some revision,Some e) \<Rightarrow>
+ let emitted = artifact source; code = map nat_of_char (snd (fst emitted));
+ data = code @ map nat_of_char source @ concat (map (row e) [0..<512]);
+ header = [82,77,89,49] @ octets 4 (length code) @ octets 4 (length source) @
+ octets 4 512 @ octets 4 revision in
+ if fst (fst emitted) \<and> revision < 2 ^ 32 \<and> 0 < revision \<and>
+ length code \<le> 65536 \<and> length source \<le> 65536
+ then ((True,map char_of_nat (header @ octets 8 (unat (checksum (header @ data))) @ data)),snd emitted)
+ else ((False,[]),''invalid live payload limits'' @ newline)
+ | (_,None) \<Rightarrow> ((False,[]),source_error source)
+ | _ \<Rightarrow> ((False,[]),''invalid live revision'' @ newline))"
+
+lemma checksum_empty: "checksum [] = 14695981039346656037"
+ by (simp add: checksum_def)
+
+lemma checksum_step:
+ "checksum (bytes @ [b]) = (checksum bytes XOR word_of_nat b) * 1099511628211"
+ by (simp add: checksum_def foldl_append)
+
+
+lemma row_size [simp]: "length (row e i) = 32"
+ by (simp add: row_def)
+
+lemma rows_size [simp]: "length (concat (map (row e) xs)) = 32 * length xs"
+ by (induction xs) auto
+
+theorem delivery_bounds:
+ "delivery sequence source = ((True,packet),report) \<Longrightarrow>
+ 16412 \<le> length packet \<and> length packet \<le> 147484"
+ by (auto simp: delivery_def Let_def split: option.splits if_splits; linarith)
+
+end
A => src/Examples.thy +143 -0
@@ 1,143 @@
+theory Examples
+ imports Frontend
+begin
+
+lemma overflow: "operate Add (-1) 1 = 0"
+ by eval
+
+lemma multiply_overflow: "operate Mul (2 ^ 63) 2 = 0"
+ by eval
+
+lemma shift_mask: "operate Shl 7 64 = 7"
+ by eval
+
+lemma shift_wrap: "operate Shl 7 65 = 14"
+ by eval
+
+lemma logical_shift: "operate Shr (-1) 63 = 1"
+ by eval
+
+lemma unsigned_comparison: "operate Less (-1) 1 = 0"
+ by eval
+
+lemma unsigned_high_bit: "operate Less 1 (2 ^ 63) = 1"
+ by eval
+
+lemma constant_fold:
+ "optimise (Binary Add (Literal (-1)) (Literal 1)) = Literal 0"
+ by eval
+
+lemma neutral_arithmetic:
+ "optimise (Binary Mul (Binary Add (Input X) (Literal 0)) (Literal 1)) = Input X"
+ by eval
+
+lemma neutral_bits:
+ "optimise (Binary And (Binary Xor (Input Y) (Literal 0)) (Literal (-1))) = Input Y"
+ by eval
+
+lemma absorbing_arithmetic:
+ "optimise (Binary Mul (Input X) (Literal 0)) = Literal 0"
+ by eval
+
+lemma absorbing_bits:
+ "optimise (Binary Or (Binary And (Input Y) (Literal 0)) (Literal (-1))) = Literal (-1)"
+ by eval
+
+lemma dead_branch:
+ "optimise (Cond (Literal 0) (Input X) (Input Y)) = Input Y"
+ by eval
+
+lemma equal_branches:
+ "optimise (Cond (Input T) (Input X) (Input X)) = Input X"
+ by eval
+
+lemma stack_bound_tight:
+ "bounded 2 (compile (Binary Add (Input X) (Input Y)) []) 0 \<and>
+ \<not> bounded 1 (compile (Binary Add (Input X) (Input Y)) []) 0"
+ by eval
+
+lemma literal_code:
+ "executable (Literal 42) = [72,199,192,42,0,0,0,195]"
+ by eval
+
+lemma signed_immediates:
+ "encode (Immediate (-1)) = [72,199,192,255,255,255,255] \<and>
+ length (encode (Immediate 2147483647)) = 7 \<and>
+ length (encode (Immediate 2147483648)) = 10 \<and>
+ length (encode (Immediate (-2147483648))) = 7 \<and>
+ length (encode (Immediate (-2147483649))) = 10"
+ by eval
+
+lemma compact_slots:
+ "encode (Peek 15) = [72,139,68,36,120] \<and>
+ length (encode (Peek 16)) = 8 \<and>
+ decode [72,139,68,36,128] = None \<and>
+ decode [72,139,68,36,7] = None"
+ by eval
+
+lemma opcode_roundtrip:
+ "decode [72,145,72,211,232,195] = Some (Arithmetic Shr,[195])"
+ by eval
+
+lemma truncated_literal: "decode [72,184,0,0] = None"
+ by eval
+
+lemma unaligned_slot: "decode [72,139,132,36,1,0,0,0] = None"
+ by eval
+
+lemma negative_slot: "decode [72,139,132,36,0,0,0,128] = None"
+ by eval
+
+lemma lexical_shadow:
+ "reference ''(let x 7 (let x (+ x 2) (* x x)))'' ''1'' ''2'' ''3'' = (True,''81'' @ newline)"
+ by eval
+
+lemma numeric_identifier:
+ "reference ''(let x1 7 (let x1 (+ x1 2) (* x1 x1)))'' ''0'' ''0'' ''0'' = (True,''81'' @ newline)"
+ by eval
+
+lemma numeric_prefix_rejected: "prepare ''(let 1x 3 1x)'' = None"
+ by eval
+
+lemma nested_temporaries:
+ "reference ''(+ 10 (let a 3 (+ a (let b 4 (* a b)))))'' ''0'' ''0'' ''0'' = (True,''25'' @ newline)"
+ by eval
+
+lemma unbound_rejected: "prepare ''(let a 3 b)'' = None"
+ by eval
+
+lemma trailing_rejected: "prepare ''(+ x y) 1'' = None"
+ by eval
+
+lemma literal_overflow_rejected: "prepare ''18446744073709551616'' = None"
+ by eval
+
+lemma hexadecimal_boundaries:
+ "number ''0xffffffffffffffff'' = Some (2 ^ 64 - 1) \<and>
+ number ''0x10000000000000000'' = None"
+ by eval
+
+lemma hexadecimal_execution:
+ "reference ''(+ x 0XfF)'' ''0x1'' ''0'' ''0'' = (True,''256'' @ newline)"
+ by eval
+
+lemma incomplete_rejected: "prepare ''(if x y)'' = None"
+ by eval
+
+lemma comment_tokens:
+ "lex (''(+ x; ignore ) tokens'' @ newline @ ''y) ; end'') [] [] = [''('', ''+'', ''x'', ''y'', '')'']"
+ by eval
+
+lemma missing_operand_offset:
+ "source_error ''(+ x)'' = ''syntax error at token 3'' @ newline"
+ by eval
+
+lemma trailing_token_offset:
+ "source_error ''(+ x y) 1'' = ''syntax error at token 5'' @ newline"
+ by eval
+
+lemma exhausted_parser:
+ "diagnose 0 [] [''1''] 7 = Failed (Exhausted 7)"
+ by (subst diagnose.simps) simp
+
+end
A => src/Export.thy +11 -0
@@ 1,11 @@
+theory Export
+ imports Examples Delivery
+begin
+
+definition ascii :: "integer \<Rightarrow> char" where "ascii = char_of"
+
+definition ordinal :: "char \<Rightarrow> integer" where "ordinal = of_char"
+
+export_code validate disassemble configured artifact baseline vectors reference simulate delivery ascii ordinal in SML module_name Remy file_prefix remy
+
+end
A => src/Frontend.thy +365 -0
@@ 1,365 @@
+theory Frontend
+ imports X86
+begin
+
+fun finish :: "string \<Rightarrow> string list \<Rightarrow> string list" where
+ "finish [] out = out"
+| "finish word out = rev word # out"
+
+fun scan :: "string \<Rightarrow> string \<Rightarrow> string list \<Rightarrow> bool \<Rightarrow> string list" where
+ "scan [] word out comment = rev (finish word out)"
+| "scan (c # cs) word out comment = (if comment then
+ scan cs [] out (c \<noteq> CHR 0x0A \<and> c \<noteq> CHR 0x0D)
+ else if c = CHR '';'' then scan cs [] (finish word out) True
+ else if c = CHR '' '' \<or> c = CHR 0x09 \<or> c = CHR 0x0A \<or> c = CHR 0x0D
+ then scan cs [] (finish word out) False
+ else if c = CHR ''('' \<or> c = CHR '')'' then scan cs [] ([c] # finish word out) False
+ else scan cs (c # word) out False)"
+
+definition lex :: "string \<Rightarrow> string \<Rightarrow> string list \<Rightarrow> string list" where
+ "lex s word out = scan s word out False"
+
+fun digit :: "char \<Rightarrow> nat" where
+ "digit c = (let n = nat_of_char c in
+ if 48 \<le> n \<and> n < 58 then n - 48 else
+ if 65 \<le> n \<and> n < 71 then n - 55 else
+ if 97 \<le> n \<and> n < 103 then n - 87 else 16)"
+
+definition parse_digits :: "nat \<Rightarrow> string \<Rightarrow> nat option" where
+ "parse_digits base s = (if s = [] \<or> \<not> list_all (\<lambda>c. digit c < base) s
+ then None else let n = foldl (\<lambda>n c. min (2 ^ 64) (base * n + digit c)) 0 s in
+ if n < 2 ^ 64 then Some n else None)"
+
+definition number :: "string \<Rightarrow> nat option" where
+ "number s = (case s of a # b # rest \<Rightarrow>
+ if a = CHR ''0'' \<and> (b = CHR ''x'' \<or> b = CHR ''X'') then parse_digits 16 rest
+ else parse_digits 10 s | _ \<Rightarrow> parse_digits 10 s)"
+
+lemma parse_digits_bound: "parse_digits base s = Some n \<Longrightarrow> n < 2 ^ 64"
+ by (auto simp only: parse_digits_def Let_def option.inject option.distinct split: if_splits)
+
+theorem number_bound: "number s = Some n \<Longrightarrow> n < 2 ^ 64"
+ using parse_digits_bound by (auto simp: number_def split: list.splits if_splits)
+
+definition valid_name :: "string \<Rightarrow> bool" where
+ "valid_name s = (case s of [] \<Rightarrow> False | c # cs \<Rightarrow>
+ 97 \<le> nat_of_char c \<and> nat_of_char c \<le> 122 \<and>
+ list_all (\<lambda>d. (97 \<le> nat_of_char d \<and> nat_of_char d \<le> 122) \<or>
+ (48 \<le> nat_of_char d \<and> nat_of_char d < 58)) cs \<and> s \<noteq> ''let'' \<and> s \<noteq> ''if'')"
+
+fun lookup :: "string \<Rightarrow> string list \<Rightarrow> nat option" where
+ "lookup name [] = None"
+| "lookup name (x # xs) = (if name = x then Some 0 else map_option Suc (lookup name xs))"
+
+lemma lookup_bound: "lookup name names = Some i \<Longrightarrow> i < length names"
+ by (induction names arbitrary: i) (auto split: if_splits option.splits)
+
+fun operator :: "string \<Rightarrow> operator option" where
+ "operator s = (if s = ''+'' then Some Add else if s = ''-'' then Some Sub else if s = ''*'' then Some Mul
+ else if s = ''and'' then Some And else if s = ''or'' then Some Or else if s = ''xor'' then Some Xor
+ else if s = ''shl'' then Some Shl else if s = ''shr'' then Some Shr else if s = ''<'' then Some Less else None)"
+
+definition atom :: "string list \<Rightarrow> string \<Rightarrow> expression option" where
+ "atom names s = (case lookup s names of Some i \<Rightarrow> Some (Variable i) | None \<Rightarrow>
+ if s = ''x'' then Some (Input X) else if s = ''y'' then Some (Input Y) else if s = ''t'' then Some (Input T)
+ else map_option (Literal \<circ> word_of_nat) (number s))"
+
+lemma atom_scoped: "atom names s = Some e \<Longrightarrow> scoped (length names) e"
+ by (auto simp: atom_def split: option.splits if_splits dest: lookup_bound)
+
+fun close :: "expression \<Rightarrow> string list \<Rightarrow> (expression \<times> string list) option" where
+ "close e (s # rest) = (if s = '')'' then Some (e,rest) else None)"
+| "close e [] = None"
+
+lemma close_expression: "close e tokens = Some (a,rest) \<Longrightarrow> a = e"
+ by (cases tokens) (auto split: if_splits)
+
+function parse :: "nat \<Rightarrow> string list \<Rightarrow> string list \<Rightarrow> (expression \<times> string list) option" where
+ "parse fuel names tokens = (if fuel = 0 then None else case tokens of [] \<Rightarrow> None | s # rest \<Rightarrow>
+ if s \<noteq> ''('' then map_option (\<lambda>e. (e,rest)) (atom names s)
+ else case rest of [] \<Rightarrow> None | op # args \<Rightarrow>
+ if op = ''let'' then (case args of [] \<Rightarrow> None | name # body \<Rightarrow>
+ if \<not> valid_name name then None else
+ Option.bind (parse (fuel - 1) names body) (\<lambda>(a,tail).
+ Option.bind (parse (fuel - 1) (name # names) tail) (\<lambda>(b,tail). close (Let a b) tail)))
+ else if op = ''if'' then
+ Option.bind (parse (fuel - 1) names args) (\<lambda>(c,tail).
+ Option.bind (parse (fuel - 1) names tail) (\<lambda>(a,tail).
+ Option.bind (parse (fuel - 1) names tail) (\<lambda>(b,tail). close (Cond c a b) tail)))
+ else Option.bind (operator op) (\<lambda>f.
+ Option.bind (parse (fuel - 1) names args) (\<lambda>(a,tail).
+ Option.bind (parse (fuel - 1) names tail) (\<lambda>(b,tail). close (Binary f a b) tail))))"
+ by pat_completeness auto
+termination by (relation "measure (\<lambda>(fuel,names,tokens). fuel)") auto
+
+declare parse.simps [simp del]
+
+theorem parse_scoped:
+ "parse fuel names tokens = Some (e,rest) \<Longrightarrow> scoped (length names) e"
+proof (induction fuel arbitrary: names tokens e rest)
+ case 0
+ then show ?case by (subst (asm) parse.simps) auto
+next
+ case (Suc fuel)
+ from Suc.prems show ?case
+ by (subst (asm) parse.simps)
+ (auto simp del: operator.simps dest: atom_scoped split: list.splits if_splits bind_splits option.splits prod.splits;
+ drule close_expression; auto dest: Suc.IH)
+qed
+
+record limits =
+ depth_budget :: nat
+ node_budget :: nat
+ stack_budget :: nat
+
+definition defaults :: limits where
+ "defaults = \<lparr>depth_budget = 128, node_budget = 4096, stack_budget = 512\<rparr>"
+
+definition valid_limits :: "limits \<Rightarrow> bool" where
+ "valid_limits lim = (depth_budget lim \<le> 128 \<and> node_budget lim \<le> 4096 \<and> stack_budget lim \<le> 512)"
+
+definition prepare_with :: "limits \<Rightarrow> string \<Rightarrow> expression option" where
+ "prepare_with lim s = (if \<not> valid_limits lim \<or> \<not> list_all (\<lambda>c. nat_of_char c < 128) s then None else
+ Option.bind (parse (depth_budget lim) [] (lex s [] [])) (\<lambda>(e,rest).
+ if rest = [] \<and> nodes e \<le> node_budget lim then
+ let code = compile (optimise e) [] in
+ if check code 0 = Some 1 \<and> demand (optimise e) \<le> stack_budget lim \<and> list_all encodable (native code)
+ then Some e else None else None))"
+
+definition prepare :: "string \<Rightarrow> expression option" where
+ "prepare = prepare_with defaults"
+
+lemma prepare_with_scoped: "prepare_with lim s = Some e \<Longrightarrow> scoped 0 e"
+ by (auto simp: prepare_with_def Let_def dest: parse_scoped split: if_splits bind_splits prod.splits)
+
+lemma prepare_with_bounded:
+ "prepare_with lim s = Some e \<Longrightarrow> bounded (stack_budget lim) (compile (optimise e) []) 0"
+ by (auto simp: prepare_with_def Let_def closed_demand optimise_scoped dest: parse_scoped split: if_splits bind_splits prod.splits)
+
+lemma prepare_scoped: "prepare s = Some e \<Longrightarrow> scoped 0 e"
+ unfolding prepare_def using prepare_with_scoped by blast
+
+lemma prepare_bounded:
+ "prepare s = Some e \<Longrightarrow> bounded 512 (compile (optimise e) []) 0"
+ using prepare_with_bounded[where lim=defaults] by (simp add: prepare_def defaults_def)
+
+lemma prepare_encodable:
+ "prepare s = Some e \<Longrightarrow> list_all encodable (native (compile (optimise e) []))"
+ by (auto simp: prepare_def prepare_with_def Let_def split: if_splits bind_splits prod.splits)
+
+lemma prepare_program:
+ "prepare s = Some e \<Longrightarrow> list_all encodable (program e)"
+ unfolding program_def using prepare_encodable
+ by (auto intro: transfers_property)
+
+theorem prepared_correct:
+ "prepare source = Some e \<Longrightarrow>
+ execute values (compile (optimise e) []) [] = Some [evaluate e [] values]"
+ using compile_closed prepare_scoped by blast
+
+theorem prepared_native:
+ "prepare source = Some e \<Longrightarrow>
+ map_option observe (run (native (compile (optimise e) [])) s) =
+ Some (inputs s, evaluate e [] (inputs s) # stack s)"
+ using native_expression prepare_scoped by blast
+
+theorem prepared_bytes:
+ "prepare source = Some e \<Longrightarrow>
+ recover (length (program e)) (executable e) =
+ Some (program e, [195])"
+ unfolding executable_def using recover_encode prepare_program by blast
+
+theorem prepared_stacks:
+ "prepare source = Some e \<Longrightarrow>
+ \<exists>frames. snapshots values (compile (optimise e) []) [] = Some frames \<and>
+ list_all (\<lambda>s. length s \<le> 512) frames"
+ using bounded_execution[where s="[]" and limit=512] prepare_bounded by auto
+
+function decimal :: "nat \<Rightarrow> string" where
+ "decimal n = (if n < 10 then [char_of_nat (48+n)] else decimal (n div 10) @ [char_of_nat (48+n mod 10)])"
+ by pat_completeness auto
+termination by (relation "measure id") (auto simp: div_less_dividend)
+
+definition newline :: string where "newline = [CHR 0x0A]"
+
+fun regname :: "register \<Rightarrow> string" where
+ "regname Rax = ''rax''" | "regname Rcx = ''rcx''" | "regname Rbx = ''rbx''"
+| "regname Rdx = ''rdx''" | "regname R8 = ''r8''" | "regname R9 = ''r9''"
+
+fun opname :: "operator \<Rightarrow> string" where
+ "opname Add = ''add''" | "opname Sub = ''sub''" | "opname Mul = ''mul''"
+| "opname And = ''and''" | "opname Or = ''or''" | "opname Xor = ''xor''"
+| "opname Shl = ''shl''" | "opname Shr = ''shr''" | "opname Less = ''less''"
+
+fun mnemonic :: "opcode \<Rightarrow> string" where
+ "mnemonic (Immediate v) = ''immediate rax '' @ decimal (unat v)"
+| "mnemonic (Push r) = ''push '' @ regname r"
+| "mnemonic (Pop r) = ''pop '' @ regname r"
+| "mnemonic (Move dst src) = ''mov '' @ regname dst @ '' '' @ regname src"
+| "mnemonic (Peek i) = ''peek rax stack['' @ decimal i @ '']''"
+| "mnemonic (Arithmetic op) = ''arithmetic '' @ opname op"
+| "mnemonic Conditional = ''conditional rax rcx rbx''"
+
+fun listing :: "nat \<Rightarrow> (nat list \<times> opcode) list \<Rightarrow> string" where
+ "listing offset [] = decimal offset @ '' ret'' @ newline"
+| "listing offset ((bytes,op) # code) = decimal offset @ '' '' @ mnemonic op @
+ '' ['' @ concat (map (\<lambda>b. decimal b @ '' '') bytes) @ '']'' @ newline @
+ listing (offset + length bytes) code"
+
+fun linear_listing :: "nat \<Rightarrow> opcode list \<Rightarrow> string" where
+ "linear_listing offset [] = []"
+| "linear_listing offset (op # code) = decimal offset @ '' '' @ mnemonic op @ newline @
+ linear_listing (offset + length (encode op)) code"
+
+fun flowlisting :: "nat \<Rightarrow> flow \<Rightarrow> string" where
+ "flowlisting offset (Basic code) = linear_listing offset code"
+| "flowlisting offset (Sequence a b) = flowlisting offset a @
+ flowlisting (offset + length (flowbytes a)) b"
+| "flowlisting offset (Choice a b) = decimal offset @ '' test rax rax'' @ newline @
+ decimal (offset + 3) @ '' jz '' @ decimal (offset + 14 + length (flowbytes a)) @ newline @
+ flowlisting (offset + 9) a @ decimal (offset + 9 + length (flowbytes a)) @ '' jmp '' @
+ decimal (offset + length (flowbytes (Choice a b))) @ newline @
+ flowlisting (offset + 14 + length (flowbytes a)) b"
+
+definition disassemble :: "string \<Rightarrow> bool \<times> string" where
+ "disassemble bytes = (case blocks (map nat_of_char bytes) of
+ None \<Rightarrow> (case inspect (map nat_of_char bytes) of
+ None \<Rightarrow> (False,''invalid native block stream'' @ newline)
+ | Some code \<Rightarrow> (True,flowlisting 0 code @ decimal (length (flowbytes code)) @ '' ret'' @ newline))
+ | Some code \<Rightarrow> (True,listing 0 code))"
+
+definition validate :: "string \<Rightarrow> bool \<times> string" where
+ "validate bytes = (case blocks (map nat_of_char bytes) of
+ None \<Rightarrow> (case inspect (map nat_of_char bytes) of
+ None \<Rightarrow> (False,''invalid native block stream'' @ newline)
+ | Some code \<Rightarrow> (True,''native branch, stack and register effects verified'' @ newline))
+ | Some code \<Rightarrow> if audit (map snd code) 0 = Some 0
+ then (True,''native stack and register effects verified'' @ newline)
+ else (False,''invalid native stack or register effects'' @ newline))"
+
+datatype problem = Unexpected nat | Exhausted nat
+
+datatype 'a outcome = Failed problem | Parsed 'a
+
+fun parsed_bind :: "'a outcome \<Rightarrow> ('a \<Rightarrow> 'b outcome) \<Rightarrow> 'b outcome" where
+ "parsed_bind (Failed p) f = Failed p"
+| "parsed_bind (Parsed x) f = f x"
+
+fun close_at :: "expression \<Rightarrow> string list \<Rightarrow> nat \<Rightarrow> (expression \<times> string list \<times> nat) outcome" where
+ "close_at e [] pos = Failed (Unexpected pos)"
+| "close_at e (s # rest) pos = (if s = '')'' then Parsed (e,rest,Suc pos) else Failed (Unexpected pos))"
+
+lemma close_at_cursor:
+ "close_at e tokens pos = Parsed (a,rest,nextpos) \<Longrightarrow> a = e \<and> nextpos = Suc pos"
+ by (cases tokens) (auto split: if_splits)
+
+function diagnose :: "nat \<Rightarrow> string list \<Rightarrow> string list \<Rightarrow> nat \<Rightarrow>
+ (expression \<times> string list \<times> nat) outcome" where
+ "diagnose fuel names tokens pos = (if fuel = 0 then Failed (Exhausted pos)
+ else case tokens of [] \<Rightarrow> Failed (Unexpected pos) | s # rest \<Rightarrow>
+ if s \<noteq> ''('' then (case atom names s of None \<Rightarrow> Failed (Unexpected pos)
+ | Some e \<Rightarrow> Parsed (e,rest,Suc pos))
+ else case rest of [] \<Rightarrow> Failed (Unexpected (Suc pos)) | op # args \<Rightarrow>
+ if op = ''let'' then (case args of [] \<Rightarrow> Failed (Unexpected (pos + 2)) | name # body \<Rightarrow>
+ if \<not> valid_name name then Failed (Unexpected (pos + 2)) else
+ parsed_bind (diagnose (fuel - 1) names body (pos + 3)) (\<lambda>(a,tail,nextpos).
+ parsed_bind (diagnose (fuel - 1) (name # names) tail nextpos) (\<lambda>(b,tail,lastpos).
+ close_at (Let a b) tail lastpos)))
+ else if op = ''if'' then
+ parsed_bind (diagnose (fuel - 1) names args (pos + 2)) (\<lambda>(c,tail,nextpos).
+ parsed_bind (diagnose (fuel - 1) names tail nextpos) (\<lambda>(a,tail,nextpos).
+ parsed_bind (diagnose (fuel - 1) names tail nextpos) (\<lambda>(b,tail,lastpos).
+ close_at (Cond c a b) tail lastpos)))
+ else case operator op of None \<Rightarrow> Failed (Unexpected (Suc pos)) | Some f \<Rightarrow>
+ parsed_bind (diagnose (fuel - 1) names args (pos + 2)) (\<lambda>(a,tail,nextpos).
+ parsed_bind (diagnose (fuel - 1) names tail nextpos) (\<lambda>(b,tail,lastpos).
+ close_at (Binary f a b) tail lastpos)))"
+ by pat_completeness auto
+termination by (relation "measure (\<lambda>(fuel,names,tokens,pos). fuel)") auto
+
+declare diagnose.simps [simp del]
+
+definition source_error_with :: "limits \<Rightarrow> string \<Rightarrow> string" where
+ "source_error_with lim s = (if \<not> valid_limits lim then ''limits exceed compiler bounds'' @ newline else if \<not> list_all (\<lambda>c. nat_of_char c < 128) s then ''source must contain ASCII'' @ newline else
+ case diagnose (depth_budget lim) [] (lex s [] []) 0 of
+ Failed (Unexpected pos) \<Rightarrow> ''syntax error at token '' @ decimal pos @ newline
+ | Failed (Exhausted pos) \<Rightarrow> ''parse depth limit exceeded at token '' @ decimal pos @ newline
+ | Parsed (e,rest,pos) \<Rightarrow> if rest \<noteq> [] then ''syntax error at token '' @ decimal pos @ newline
+ else if nodes e > node_budget lim then ''program exceeds '' @ decimal (node_budget lim) @ '' nodes'' @ newline
+ else if demand (optimise e) > stack_budget lim then ''evaluation stack exceeds '' @ decimal (stack_budget lim) @ '' words'' @ newline
+ else ''native validation failed'' @ newline)"
+
+definition artifact_with :: "limits \<Rightarrow> string \<Rightarrow> (bool \<times> string) \<times> string" where
+ "artifact_with lim s = (case prepare_with lim s of None \<Rightarrow> ((False,[]), source_error_with lim s)
+ | Some e \<Rightarrow> let opt = optimise e; code = branching e; bytes = flowbytes code @ [195] in
+ if flowaudit code 0 = Some 0 \<and> flowvalid code then
+ ((True, map char_of_nat bytes), decimal (nodes e) @ '' nodes -> '' @ decimal (nodes opt) @
+ '' nodes, '' @ decimal (length bytes) @ '' bytes, '' @ decimal (demand opt) @ '' stack words'' @ newline)
+ else ((False,[]),''allocated code exceeds native limits'' @ newline))"
+
+definition source_error :: "string \<Rightarrow> string" where
+ "source_error = source_error_with defaults"
+
+definition artifact :: "string \<Rightarrow> (bool \<times> string) \<times> string" where
+ "artifact = artifact_with defaults"
+
+theorem artifact_execution:
+ assumes "artifact source = ((True,bytes),report)"
+ shows "\<exists>e d. prepare source = Some e \<and>
+ bytes = map char_of_nat (flowbytes (branching e) @ [195]) \<and>
+ executes64 (flowbytes (branching e)) c d \<and>
+ registers (state64 d) Rax = evaluate e [] (inputs (state64 c)) \<and>
+ stack (state64 d) = stack (state64 c) \<and> inputs (state64 d) = inputs (state64 c)"
+proof -
+ obtain e where e: "prepare source = Some e" "flowvalid (branching e)"
+ "bytes = map char_of_nat (flowbytes (branching e) @ [195])"
+ using assms by (auto simp: artifact_def artifact_with_def prepare_def Let_def split: option.splits if_splits)
+ show ?thesis using compiled_execution[OF prepare_scoped[OF e(1)] e(2), of c] e by blast
+qed
+
+definition baseline :: "string \<Rightarrow> (bool \<times> string) \<times> string" where
+ "baseline s = (case prepare s of None \<Rightarrow> ((False,[]),source_error s)
+ | Some e \<Rightarrow> ((True,map char_of_nat (executable e)),''stack backend'' @ newline))"
+
+definition configured :: "string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> (bool \<times> string) \<times> string" where
+ "configured depth count stacktext source = (case (number depth, number count, number stacktext) of
+ (Some d,Some n,Some k) \<Rightarrow> artifact_with \<lparr>depth_budget=d, node_budget=n, stack_budget=k\<rparr> source
+ | _ \<Rightarrow> ((False,[]),''invalid resource limits'' @ newline))"
+
+definition boundary :: "nat list" where
+ "boundary = [0,1,63,64,65,127,255,256,2 ^ 31,2 ^ 32,2 ^ 63,2 ^ 64 - 1]"
+
+definition sample :: "nat \<Rightarrow> input \<Rightarrow> pixel" where
+ "sample i = (\<lambda>v. word_of_nat (if i < 12 then boundary ! ((i + (case v of X \<Rightarrow> 0 | Y \<Rightarrow> 3 | T \<Rightarrow> 7)) mod 12)
+ else case v of X \<Rightarrow> (17*i) mod 257 | Y \<Rightarrow> (29*i) mod 131 | T \<Rightarrow> 13*i))"
+
+definition row :: "expression \<Rightarrow> nat \<Rightarrow> nat list" where
+ "row e i = concat (map (\<lambda>v. octets 8 (unat v))
+ [sample i X, sample i Y, sample i T, evaluate e [] (sample i)])"
+
+definition vectors :: "string \<Rightarrow> bool \<times> string" where
+ "vectors s = (case prepare s of None \<Rightarrow> (False, source_error s)
+ | Some e \<Rightarrow> (True, map char_of_nat (concat (map (row e) [0..<512]))))"
+
+definition reference :: "string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> bool \<times> string" where
+ "reference source x y t = (case prepare source of None \<Rightarrow> (False,source_error source) | Some e \<Rightarrow>
+ case (number x, number y, number t) of (Some a,Some b,Some c) \<Rightarrow>
+ (True, decimal (unat (evaluate e [] (\<lambda>v. word_of_nat (case v of X \<Rightarrow> a | Y \<Rightarrow> b | T \<Rightarrow> c)))) @ newline)
+ | _ \<Rightarrow> (False,''invalid input'' @ newline))"
+
+definition initial64 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> processor" where
+ "initial64 x y t = \<lparr>state64 = \<lparr>registers = (\<lambda>r. word_of_nat
+ (if r = R8 then x else if r = R9 then y else if r = Rdx then t else 0)), stack = [0]\<rparr>,
+ pointer64 = 65536, zero64 = None, carry64 = None\<rparr>"
+
+definition simulate :: "string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> bool \<times> string" where
+ "simulate code x y t = (if \<not> fst (validate code) then (False,''invalid native image'' @ newline) else
+ case (number x,number y,number t) of (Some a,Some b,Some c) \<Rightarrow>
+ (case simulate64 (Suc (length code)) (map nat_of_char code) (initial64 a b c) of
+ None \<Rightarrow> (False,''unsupported or incomplete x86 execution'' @ newline)
+ | Some q \<Rightarrow> if stack (state64 q) = []
+ then (True,decimal (unat (registers (state64 q) Rax)) @ newline)
+ else (False,''return frame was not consumed'' @ newline))
+ | _ \<Rightarrow> (False,''invalid input'' @ newline))"
+
+end
A => src/X86.thy +345 -0
@@ 1,345 @@
+theory X86
+ imports Bounds
+begin
+
+datatype micro = Imm64 pixel | Imm32 pixel | Copy register register | Save register | Restore register
+ | Load nat | Alu operator | Exchange | Compare | Below | Extend | Test register | Select
+
+record processor =
+ state64 :: machine
+ pointer64 :: pixel
+ zero64 :: "bool option"
+ carry64 :: "bool option"
+
+definition put64 :: "register \<Rightarrow> pixel \<Rightarrow> processor \<Rightarrow> processor" where
+ "put64 r v c = c\<lparr>state64 := (state64 c)\<lparr>registers := (registers (state64 c))(r := v)\<rparr>\<rparr>"
+
+fun microstep :: "micro \<Rightarrow> processor \<Rightarrow> processor option" where
+ "microstep (Imm64 v) c = Some (put64 Rax v c)"
+| "microstep (Imm32 v) c = Some (put64 Rax v c)"
+| "microstep (Copy dst src) c = Some (put64 dst (registers (state64 c) src) c)"
+| "microstep (Save r) c = Some (c\<lparr>state64 := (state64 c)\<lparr>stack := registers (state64 c) r # stack (state64 c)\<rparr>,
+ pointer64 := pointer64 c - 8\<rparr>)"
+| "microstep (Restore r) c = (case stack (state64 c) of [] \<Rightarrow> None | v # vs \<Rightarrow>
+ Some ((put64 r v c)\<lparr>state64 := (state64 (put64 r v c))\<lparr>stack := vs\<rparr>, pointer64 := pointer64 c + 8\<rparr>))"
+| "microstep (Load i) c = (if i < length (stack (state64 c))
+ then Some (put64 Rax (stack (state64 c) ! i) c) else None)"
+| "microstep (Alu op) c = (if op = Less then None else
+ Some ((put64 Rax (operate op (registers (state64 c) Rax) (registers (state64 c) Rcx)) c)
+ \<lparr>zero64 := None, carry64 := None\<rparr>))"
+| "microstep Exchange c = Some (put64 Rcx (registers (state64 c) Rax)
+ (put64 Rax (registers (state64 c) Rcx) c))"
+| "microstep Compare c = Some (c\<lparr>zero64 := Some (registers (state64 c) Rax = registers (state64 c) Rcx),
+ carry64 := Some (registers (state64 c) Rax < registers (state64 c) Rcx)\<rparr>)"
+| "microstep Below c = (case carry64 c of None \<Rightarrow> None | Some flag \<Rightarrow>
+ Some (put64 Rax ((registers (state64 c) Rax AND NOT 255) OR (if flag then 1 else 0)) c))"
+| "microstep Extend c = Some (put64 Rax (registers (state64 c) Rax AND 255) c)"
+| "microstep (Test r) c = Some (c\<lparr>zero64 := Some (registers (state64 c) r = 0), carry64 := Some False\<rparr>)"
+| "microstep Select c = (case zero64 c of None \<Rightarrow> None | Some flag \<Rightarrow>
+ Some (if flag then c else put64 Rax (registers (state64 c) Rcx) c))"
+
+fun microrun :: "micro list \<Rightarrow> processor \<Rightarrow> processor option" where
+ "microrun [] c = Some c"
+| "microrun (i # code) c = Option.bind (microstep i c) (microrun code)"
+
+lemma microrun_append:
+ "microrun (a @ b) c = Option.bind (microrun a c) (microrun b)"
+ by (induction a arbitrary: c) (auto split: option.splits bind_splits)
+
+fun microbytes :: "micro \<Rightarrow> nat list" where
+ "microbytes (Imm64 v) = [72,184] @ octets 8 (unat v)"
+| "microbytes (Imm32 v) = [72,199,192] @ octets 4 (unat v)"
+| "microbytes (Copy dst src) = movecode dst src"
+| "microbytes (Save r) = pushcode r"
+| "microbytes (Restore r) = popcode r"
+| "microbytes (Load i) = (if i < 16 then [72,139,68,36,8*i]
+ else [72,139,132,36] @ octets 4 (8*i))"
+| "microbytes (Alu Add) = [72,1,200]"
+| "microbytes (Alu Sub) = [72,41,200]"
+| "microbytes (Alu Mul) = [72,15,175,193]"
+| "microbytes (Alu And) = [72,33,200]"
+| "microbytes (Alu Or) = [72,9,200]"
+| "microbytes (Alu Xor) = [72,49,200]"
+| "microbytes (Alu Shl) = [72,211,224]"
+| "microbytes (Alu Shr) = [72,211,232]"
+| "microbytes (Alu Less) = []"
+| "microbytes Exchange = [72,145]"
+| "microbytes Compare = [72,57,200]"
+| "microbytes Below = [15,146,192]"
+| "microbytes Extend = [72,15,182,192]"
+| "microbytes (Test r) = [72,133,192 + 9 * regno r]"
+| "microbytes Select = [72,15,69,193]"
+
+fun microvalid :: "micro \<Rightarrow> bool" where
+ "microvalid (Imm32 v) = (extend32 (unat v) = v)"
+| "microvalid (Load i) = (i < 2 ^ 28)"
+| "microvalid (Alu Less) = False"
+| "microvalid (Test r) = (r = Rax \<or> r = Rbx)"
+| "microvalid _ = True"
+
+fun expand :: "opcode \<Rightarrow> micro list" where
+ "expand (Immediate v) = [if extend32 (unat v) = v then Imm32 v else Imm64 v]"
+| "expand (Push r) = [Save r]"
+| "expand (Pop r) = [Restore r]"
+| "expand (Move dst src) = [Copy dst src]"
+| "expand (Peek i) = [Load i]"
+| "expand (Arithmetic op) = (if op = Less then [Exchange,Compare,Below,Extend]
+ else if exchanges op then [Exchange,Alu op] else [Alu op])"
+| "expand Conditional = [Test Rbx,Select]"
+
+lemma byte_register:
+ "((v AND NOT 255) OR (if flag then 1 else 0)) AND 255 = (if flag then 1 else 0 :: pixel)"
+ by (cases flag) (simp_all add: word_ao_dist word_bw_assocs)
+
+theorem expand_state:
+ "map_option state64 (microrun (expand op) c) = transition op (state64 c)"
+proof (cases op)
+ case (Arithmetic f)
+ then show ?thesis
+ by (cases f)
+ (auto simp: put64_def byte_register word_ao_dist2 word_ao_dist word_bw_assocs ac_simps split: option.splits)
+next
+ case (Pop r)
+ then show ?thesis by (cases "stack (state64 c)") (auto simp: put64_def)
+qed (auto simp: put64_def split: if_splits option.splits)
+
+theorem expand_bytes:
+ "concat (map microbytes (expand op)) = encode op"
+proof (cases op)
+ case (Arithmetic f)
+ then show ?thesis by (cases f) auto
+qed auto
+
+lemma expand_valid:
+ "encodable op \<Longrightarrow> list_all microvalid (expand op)"
+proof (cases op)
+ case (Arithmetic f)
+ then show ?thesis by (cases f) auto
+qed auto
+
+theorem expand_run:
+ "map_option state64 (microrun (concat (map expand code)) c) = run code (state64 c)"
+proof (induction code arbitrary: c)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons op code)
+ then show ?case using expand_state[of op c]
+ by (auto simp: microrun_append split: option.splits bind_splits)
+qed
+
+definition top64 :: "processor \<Rightarrow> pixel" where
+ "top64 c = pointer64 c + 8 * of_nat (length (stack (state64 c)))"
+
+lemma microstep_top:
+ "microstep i c = Some d \<Longrightarrow> top64 d = top64 c"
+ by (cases i)
+ (auto simp: top64_def put64_def algebra_simps split: list.splits if_splits option.splits)
+
+definition fixed64 :: "micro list" where
+ "fixed64 = map Save [Rax,Rcx,Rbx,Rdx,R8,R9] @ map Restore [Rax,Rcx,Rbx,Rdx,R8,R9] @
+ concat (map (\<lambda>dst. map (Copy dst) [Rax,Rcx,Rbx,Rdx,R8,R9]) [Rax,Rcx,Rbx,Rdx,R8,R9]) @
+ map Alu [Add,Sub,Mul,And,Or,Xor,Shl,Shr] @ [Exchange,Compare,Below,Extend,Test Rax,Test Rbx,Select]"
+
+definition decode64 :: "nat list \<Rightarrow> (micro \<times> nat list) option" where
+ "decode64 bs = (if take 2 bs = [72,184] then
+ if 10 \<le> length bs then Some (Imm64 (word_of_nat (integer (take 8 (drop 2 bs)))),drop 10 bs) else None
+ else if take 3 bs = [72,199,192] then
+ if 7 \<le> length bs then Some (Imm32 (extend32 (integer (take 4 (drop 3 bs)))),drop 7 bs) else None
+ else if take 4 bs = [72,139,68,36] then
+ let n = integer (take 1 (drop 4 bs)) in
+ if 5 \<le> length bs \<and> n < 128 \<and> n mod 8 = 0 then Some (Load (n div 8),drop 5 bs) else None
+ else if take 4 bs = [72,139,132,36] then
+ let n = integer (take 4 (drop 4 bs)) in
+ if 8 \<le> length bs \<and> n mod 8 = 0 \<and> n div 8 < 2 ^ 28
+ then Some (Load (n div 8),drop 8 bs) else None
+ else map_option (\<lambda>i. (i,drop (length (microbytes i)) bs))
+ (List.find (\<lambda>i. take (length (microbytes i)) bs = microbytes i) fixed64))"
+
+theorem decode64_encode:
+ assumes "microvalid i"
+ shows "decode64 (microbytes i @ tail) = Some (i,tail)"
+proof (cases i)
+ case (Imm64 v)
+ then show ?thesis by (simp add: decode64_def)
+next
+ case (Imm32 v)
+ then show ?thesis using assms by (simp add: decode64_def)
+next
+ case (Copy dst src)
+ then show ?thesis by (cases dst; cases src) (simp_all add: decode64_def fixed64_def movecode_def)
+next
+ case (Save r)
+ then show ?thesis by (cases r) (simp_all add: decode64_def fixed64_def)
+next
+ case (Restore r)
+ then show ?thesis by (cases r) (simp_all add: decode64_def fixed64_def)
+next
+ case (Load n)
+ then show ?thesis using assms peek_bound[of n]
+ by (auto simp: decode64_def integer_octets Let_def)
+next
+ case (Alu op)
+ then show ?thesis using assms by (cases op) (simp_all add: decode64_def fixed64_def movecode_def)
+next
+ case (Test r)
+ then show ?thesis using assms by (cases r) (simp_all add: decode64_def fixed64_def movecode_def)
+qed (simp_all add: decode64_def fixed64_def movecode_def)
+
+inductive executes64 :: "nat list \<Rightarrow> processor \<Rightarrow> processor \<Rightarrow> bool" where
+ empty: "executes64 [] c c"
+| advance: "microvalid i \<Longrightarrow> microstep i c = Some d \<Longrightarrow> executes64 tail d e \<Longrightarrow>
+ executes64 (microbytes i @ tail) c e"
+| jump: "n < 2 ^ 31 \<Longrightarrow> n \<le> length tail \<Longrightarrow> executes64 (drop n tail) c d \<Longrightarrow>
+ executes64 ([233] @ octets 4 n @ tail) c d"
+| zero: "n < 2 ^ 31 \<Longrightarrow> n \<le> length tail \<Longrightarrow> zero64 c = Some True \<Longrightarrow>
+ executes64 (drop n tail) c d \<Longrightarrow> executes64 ([15,132] @ octets 4 n @ tail) c d"
+| nonzero: "n < 2 ^ 31 \<Longrightarrow> zero64 c = Some False \<Longrightarrow> executes64 tail c d \<Longrightarrow>
+ executes64 ([15,132] @ octets 4 n @ tail) c d"
+
+lemma executes64_append:
+ "executes64 a c d \<Longrightarrow> executes64 b d e \<Longrightarrow> executes64 (a @ b) c e"
+ by (induction a c d rule: executes64.induct)
+ (auto simp: drop_append intro: executes64.intros[simplified])
+
+lemma executes64_micro:
+ "list_all microvalid code \<Longrightarrow> microrun code c = Some d \<Longrightarrow>
+ executes64 (concat (map microbytes code)) c d"
+ by (induction code arbitrary: c) (auto split: option.splits bind_splits intro: executes64.intros)
+
+lemma executes64_top:
+ "executes64 code c d \<Longrightarrow> top64 d = top64 c"
+ by (induction rule: executes64.induct) (auto dest: microstep_top)
+
+theorem executes64_native:
+ "list_all encodable code \<Longrightarrow> run code (state64 c) = Some s \<Longrightarrow>
+ \<exists>d. executes64 (concat (map encode code)) c d \<and> state64 d = s"
+proof -
+ assume valid: "list_all encodable code" and ran: "run code (state64 c) = Some s"
+ obtain d where d: "microrun (concat (map expand code)) c = Some d" "state64 d = s"
+ using expand_run[of code c] ran by (auto split: option.splits)
+ have safe: "list_all microvalid (concat (map expand code))"
+ using valid expand_valid by (auto simp: list_all_iff)
+ have bytes: "concat (map microbytes (concat (map expand code))) = concat (map encode code)"
+ using expand_bytes by (induction code) auto
+ show ?thesis using executes64_micro[OF safe d(1)] d(2) bytes by auto
+qed
+
+
+theorem executes64_flow:
+ assumes "flowvalid code" "flowrun code (state64 c) = Some s"
+ shows "\<exists>d. executes64 (flowbytes code) c d \<and> state64 d = s"
+ using assms
+proof (induction code arbitrary: c s)
+ case (Basic code)
+ then show ?case using executes64_native by fastforce
+next
+ case (Sequence a b)
+ obtain m where a: "flowrun a (state64 c) = Some m" and b: "flowrun b m = Some s"
+ using Sequence.prems by (auto split: bind_splits)
+ obtain d where d: "executes64 (flowbytes a) c d" "state64 d = m"
+ using Sequence.IH(1) Sequence.prems a by auto
+ obtain e where e: "executes64 (flowbytes b) d e" "state64 e = s"
+ using Sequence.IH(2) Sequence.prems b d by auto
+ show ?case using executes64_append[OF d(1) e(1)] e(2) by auto
+next
+ case (Choice a b)
+ let ?c = "c\<lparr>zero64 := Some (registers (state64 c) Rax = 0), carry64 := Some False\<rparr>"
+ have test: "microstep (Test Rax) c = Some ?c" by simp
+ have limits: "length (flowbytes a) + 5 < 2 ^ 31" "length (flowbytes b) < 2 ^ 31"
+ using Choice.prems by auto
+ show ?case
+ proof (cases "registers (state64 c) Rax = 0")
+ case True
+ obtain d where d: "executes64 (flowbytes b) ?c d" "state64 d = s"
+ using Choice.IH(2)[of ?c s] Choice.prems True by auto
+ have z: "executes64 ([15,132] @ octets 4 (length (flowbytes a) + 5) @
+ (flowbytes a @ [233] @ octets 4 (length (flowbytes b)) @ flowbytes b)) ?c d"
+ using d(1) limits True by (intro executes64.zero) auto
+ have "executes64 (microbytes (Test Rax) @ ([15,132] @ octets 4 (length (flowbytes a) + 5) @
+ (flowbytes a @ [233] @ octets 4 (length (flowbytes b)) @ flowbytes b))) c d"
+ using test z by (intro executes64.advance) auto
+ then show ?thesis using d(2) by auto
+ next
+ case False
+ obtain d where d: "executes64 (flowbytes a) ?c d" "state64 d = s"
+ using Choice.IH(1)[of ?c s] Choice.prems False by auto
+ have skip: "executes64 ([233] @ octets 4 (length (flowbytes b)) @ flowbytes b) d d"
+ using limits(2) by (intro executes64.jump) (auto intro: executes64.empty)
+ have z: "executes64 ([15,132] @ octets 4 (length (flowbytes a) + 5) @
+ (flowbytes a @ [233] @ octets 4 (length (flowbytes b)) @ flowbytes b)) ?c d"
+ using executes64_append[OF d(1) skip] limits False
+ by (intro executes64.nonzero) auto
+ have "executes64 (microbytes (Test Rax) @ ([15,132] @ octets 4 (length (flowbytes a) + 5) @
+ (flowbytes a @ [233] @ octets 4 (length (flowbytes b)) @ flowbytes b))) c d"
+ using test z by (intro executes64.advance) auto
+ then show ?thesis using d(2) by auto
+ qed
+qed
+
+theorem compiled_execution:
+ assumes "scoped 0 e" "flowvalid (branching e)"
+ shows "\<exists>d. executes64 (flowbytes (branching e)) c d \<and>
+ registers (state64 d) Rax = evaluate e [] (inputs (state64 c)) \<and>
+ stack (state64 d) = stack (state64 c) \<and> inputs (state64 d) = inputs (state64 c) \<and>
+ pointer64 d = pointer64 c"
+proof -
+ obtain s where s: "flowrun (branching e) (state64 c) = Some s"
+ "registers s Rax = evaluate e [] (inputs (state64 c))"
+ "stack s = stack (state64 c)" "inputs s = inputs (state64 c)"
+ using branching_return[OF assms(1), of "state64 c"] by blast
+ obtain d where d: "executes64 (flowbytes (branching e)) c d" "state64 d = s"
+ using executes64_flow[OF assms(2) s(1)] by blast
+ have "pointer64 d = pointer64 c"
+ using executes64_top[OF d(1)] d(2) s(3) by (simp add: top64_def)
+ then show ?thesis using d s by blast
+qed
+
+definition ret64 :: "processor \<Rightarrow> (pixel \<times> processor) option" where
+ "ret64 c = (case stack (state64 c) of [] \<Rightarrow> None | address # rest \<Rightarrow>
+ Some (address,c\<lparr>state64 := (state64 c)\<lparr>stack := rest\<rparr>, pointer64 := pointer64 c + 8\<rparr>))"
+
+definition returns64 :: "nat list \<Rightarrow> processor \<Rightarrow> pixel \<Rightarrow> processor \<Rightarrow> bool" where
+ "returns64 bytes c address d \<longleftrightarrow> (\<exists>body q. bytes = body @ [195] \<and>
+ executes64 body c q \<and> ret64 q = Some (address,d))"
+
+theorem compiled_return:
+ assumes "scoped 0 e" "flowvalid (branching e)" "stack (state64 c) = address # rest"
+ shows "\<exists>d. returns64 (flowbytes (branching e) @ [195]) c address d \<and>
+ registers (state64 d) Rax = evaluate e [] (inputs (state64 c)) \<and>
+ stack (state64 d) = rest \<and> inputs (state64 d) = inputs (state64 c) \<and>
+ pointer64 d = pointer64 c + 8"
+proof -
+ obtain q where q: "executes64 (flowbytes (branching e)) c q"
+ "registers (state64 q) Rax = evaluate e [] (inputs (state64 c))"
+ "stack (state64 q) = stack (state64 c)" "inputs (state64 q) = inputs (state64 c)"
+ "pointer64 q = pointer64 c"
+ using compiled_execution[OF assms(1,2), of c] by blast
+ let ?d = "q\<lparr>state64 := (state64 q)\<lparr>stack := rest\<rparr>, pointer64 := pointer64 q + 8\<rparr>"
+ have ret: "ret64 q = Some (address,?d)"
+ using q(3) assms(3) by (simp add: ret64_def)
+ have "returns64 (flowbytes (branching e) @ [195]) c address ?d"
+ using q(1) ret by (auto simp: returns64_def)
+ then show ?thesis using q by auto
+qed
+
+function simulate64 :: "nat \<Rightarrow> nat list \<Rightarrow> processor \<Rightarrow> processor option" where
+ "simulate64 0 bytes c = None"
+| "simulate64 (Suc fuel) bytes c = (if bytes = [] then None else
+ if bytes = [195] then map_option snd (ret64 c) else
+ if take 1 bytes = [233] then let n = integer (take 4 (drop 1 bytes)) in
+ if 5 \<le> length bytes \<and> n < 2 ^ 31 \<and> n \<le> length bytes - 5
+ then simulate64 fuel (drop (5+n) bytes) c else None
+ else if take 2 bytes = [15,132] then let n = integer (take 4 (drop 2 bytes)) in
+ if 6 \<le> length bytes \<and> n < 2 ^ 31 \<and> n \<le> length bytes - 6 then
+ (case zero64 c of None \<Rightarrow> None | Some flag \<Rightarrow>
+ simulate64 fuel (drop (6 + (if flag then n else 0)) bytes) c)
+ else None
+ else Option.bind (decode64 bytes) (\<lambda>(i,rest).
+ if microvalid i then Option.bind (microstep i c) (simulate64 fuel rest) else None))"
+ by pat_completeness auto
+termination by (relation "measure (\<lambda>(fuel,bytes,c). fuel)") auto
+
+declare simulate64.simps [simp del]
+
+end
A => src/core/Checker.thy +66 -0
@@ 1,66 @@
+theory Checker
+ imports Encoding
+begin
+
+fun effect :: "opcode \<Rightarrow> nat \<Rightarrow> nat option" where
+ "effect (Push r) n = Some (Suc n)"
+| "effect (Pop r) n = (if n = 0 then None else Some (n - 1))"
+| "effect (Peek i) n = (if i < n then Some n else None)"
+| "effect _ n = Some n"
+
+fun audit :: "opcode list \<Rightarrow> nat \<Rightarrow> nat option" where
+ "audit [] n = Some n"
+| "audit (op # code) n = (if writes op \<subseteq> {Rax,Rcx,Rbx} then
+ Option.bind (effect op n) (\<lambda>m. if m \<le> 512 then audit code m else None) else None)"
+
+lemma effect_sound:
+ "effect op (length (stack s)) = Some n \<Longrightarrow>
+ \<exists>t. transition op s = Some t \<and> length (stack t) = n"
+ by (cases op; cases "stack s") (auto split: if_splits)
+
+theorem audit_sound:
+ "audit code (length (stack s)) = Some n \<Longrightarrow>
+ \<exists>t. run code s = Some t \<and> length (stack t) = n"
+proof (induction code arbitrary: s)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons op code)
+ then show ?case
+ by (auto dest!: effect_sound split: if_splits bind_splits; fastforce)
+qed
+
+lemma audit_scratch:
+ "audit code n = Some m \<Longrightarrow> list_all (\<lambda>op. writes op \<subseteq> {Rax,Rcx,Rbx}) code"
+ by (induction code arbitrary: n) (auto split: if_splits bind_splits)
+
+theorem audit_inputs:
+ "audit code n = Some m \<Longrightarrow> run code s = Some t \<Longrightarrow> inputs t = inputs s"
+proof -
+ assume audited: "audit code n = Some m" and ran: "run code s = Some t"
+ have scratch: "list_all (\<lambda>op. writes op \<subseteq> {Rax,Rcx,Rbx}) code"
+ using audit_scratch[OF audited] .
+ show ?thesis
+ proof (rule ext)
+ fix i
+ have keep: "list_all (\<lambda>op. input_register i \<notin> writes op) code"
+ unfolding list_all_iff
+ proof (rule ballI)
+ fix op
+ assume member: "op \<in> set code"
+ have bound: "writes op \<subseteq> {Rax,Rcx,Rbx}"
+ using scratch member by (auto simp: list_all_iff)
+ show "input_register i \<notin> writes op"
+ proof
+ assume written: "input_register i \<in> writes op"
+ have "input_register i \<in> {Rax,Rcx,Rbx}"
+ using subsetD[OF bound written] .
+ then show False by simp
+ qed
+ qed
+ show "inputs t i = inputs s i"
+ unfolding inputs_def using run_preserves[OF ran keep] .
+ qed
+qed
+
+end
A => src/core/Compiler.thy +268 -0
@@ 1,268 @@
+theory Compiler
+ imports Model
+begin
+
+datatype instruction = Constant pixel | Fetch input | Pick nat | Calculate operator | Choose | Slide
+
+fun step :: "(input \<Rightarrow> pixel) \<Rightarrow> instruction \<Rightarrow> pixel list \<Rightarrow> pixel list option" where
+ "step inputs (Constant v) s = Some (v # s)"
+| "step inputs (Fetch i) s = Some (inputs i # s)"
+| "step inputs (Pick i) s = (if i < length s then Some (s ! i # s) else None)"
+| "step inputs (Calculate op) (b # a # s) = Some (operate op a b # s)"
+| "step inputs Choose (b # a # c # s) = Some ((if c = 0 then b else a) # s)"
+| "step inputs Slide (b # a # s) = Some (b # s)"
+| "step inputs _ _ = None"
+
+fun execute :: "(input \<Rightarrow> pixel) \<Rightarrow> instruction list \<Rightarrow> pixel list \<Rightarrow> pixel list option" where
+ "execute inputs [] s = Some s"
+| "execute inputs (i # code) s = (case step inputs i s of None \<Rightarrow> None | Some t \<Rightarrow> execute inputs code t)"
+
+lemma execute_append:
+ "execute inputs (a @ b) s = Option.bind (execute inputs a s) (execute inputs b)"
+ by (induction a arbitrary: s) (auto split: option.splits bind_splits)
+
+fun compile :: "expression \<Rightarrow> nat list \<Rightarrow> instruction list" where
+ "compile (Literal v) slots = [Constant v]"
+| "compile (Input i) slots = [Fetch i]"
+| "compile (Variable i) slots = [Pick (slots ! i)]"
+| "compile (Binary op a b) slots = compile a slots @ compile b (map Suc slots) @ [Calculate op]"
+| "compile (Cond c a b) slots = compile c slots @ compile a (map Suc slots) @
+ compile b (map (\<lambda>i. Suc (Suc i)) slots) @ [Choose]"
+| "compile (Let a b) slots = compile a slots @ compile b (0 # map Suc slots) @ [Slide]"
+
+definition represents :: "nat list \<Rightarrow> pixel list \<Rightarrow> pixel list \<Rightarrow> bool" where
+ "represents slots s env \<longleftrightarrow> length slots = length env \<and>
+ (\<forall>i < length env. slots ! i < length s \<and> s ! (slots ! i) = env ! i)"
+
+lemma represents_push:
+ "represents slots s env \<Longrightarrow> represents (map Suc slots) (v # s) env"
+ by (auto simp: represents_def)
+
+lemma represents_push_two:
+ "represents slots s env \<Longrightarrow> represents (map (\<lambda>i. Suc (Suc i)) slots) (a # b # s) env"
+ by (auto simp: represents_def)
+
+lemma represents_bind:
+ "represents slots s env \<Longrightarrow> represents (0 # map Suc slots) (v # s) (v # env)"
+ by (auto simp: represents_def nth_Cons split: nat.splits)
+
+theorem compile_correct:
+ assumes "scoped (length env) e" "represents slots s env"
+ shows "execute inputs (compile e slots) s = Some (evaluate e env inputs # s)"
+ using assms
+proof (induction e arbitrary: slots s env)
+ case (Literal v)
+ then show ?case by simp
+next
+ case (Input i)
+ then show ?case by simp
+next
+ case (Variable i)
+ then show ?case by (simp add: represents_def)
+next
+ case (Binary op a b)
+ have a: "execute inputs (compile a slots) s = Some (evaluate a env inputs # s)"
+ using Binary.IH(1) Binary.prems by simp
+ have b: "execute inputs (compile b (map Suc slots)) (evaluate a env inputs # s) =
+ Some (evaluate b env inputs # evaluate a env inputs # s)"
+ using Binary.IH(2) Binary.prems represents_push by simp
+ show ?case by (simp add: execute_append a b)
+next
+ case (Cond c a b)
+ have c: "execute inputs (compile c slots) s = Some (evaluate c env inputs # s)"
+ using Cond.IH(1) Cond.prems by simp
+ have a: "execute inputs (compile a (map Suc slots)) (evaluate c env inputs # s) =
+ Some (evaluate a env inputs # evaluate c env inputs # s)"
+ using Cond.IH(2) Cond.prems represents_push by simp
+ have b: "execute inputs (compile b (map (\<lambda>i. Suc (Suc i)) slots))
+ (evaluate a env inputs # evaluate c env inputs # s) =
+ Some (evaluate b env inputs # evaluate a env inputs # evaluate c env inputs # s)"
+ using Cond.IH(3) Cond.prems represents_push_two by simp
+ show ?case by (simp add: execute_append c a b)
+next
+ case (Let a b)
+ have a: "execute inputs (compile a slots) s = Some (evaluate a env inputs # s)"
+ using Let.IH(1) Let.prems by simp
+ have b: "execute inputs (compile b (0 # map Suc slots)) (evaluate a env inputs # s) =
+ Some (evaluate b (evaluate a env inputs # env) inputs # evaluate a env inputs # s)"
+ using Let.IH(2) Let.prems represents_bind by simp
+ show ?case by (simp add: execute_append a b)
+qed
+
+corollary compile_closed:
+ "scoped 0 e \<Longrightarrow> execute inputs (compile (optimise e) []) [] = Some [evaluate e [] inputs]"
+ using compile_correct[where e="optimise e" and env="[]" and slots="[]" and s="[]" and inputs=inputs]
+ by (simp add: represents_def optimise_correct optimise_scoped)
+
+fun height :: "instruction \<Rightarrow> nat \<Rightarrow> nat option" where
+ "height (Constant v) n = Some (Suc n)"
+| "height (Fetch i) n = Some (Suc n)"
+| "height (Pick i) n = (if i < n then Some (Suc n) else None)"
+| "height (Calculate op) n = (if 2 \<le> n then Some (n - 1) else None)"
+| "height Choose n = (if 3 \<le> n then Some (n - 2) else None)"
+| "height Slide n = (if 2 \<le> n then Some (n - 1) else None)"
+
+fun check :: "instruction list \<Rightarrow> nat \<Rightarrow> nat option" where
+ "check [] n = Some n"
+| "check (i # code) n = Option.bind (height i n) (check code)"
+
+lemma check_append:
+ "check (a @ b) n = Option.bind (check a n) (check b)"
+ by (induction a arbitrary: n) (auto split: option.splits bind_splits)
+
+lemma step_height:
+ "height i (length s) = Some n \<Longrightarrow> \<exists>t. step inputs i s = Some t \<and> length t = n"
+ by (cases i; cases s; simp; rename_tac a xs; case_tac xs; simp;
+ rename_tac b ys; case_tac ys; auto split: if_splits)
+
+theorem check_sound:
+ "check code (length s) = Some n \<Longrightarrow> \<exists>t. execute inputs code s = Some t \<and> length t = n"
+proof (induction code arbitrary: s)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons i code)
+ then obtain m where h: "height i (length s) = Some m" and c: "check code m = Some n"
+ by (auto simp: bind_eq_Some_conv)
+ obtain t where step: "step inputs i s = Some t" and len: "length t = m"
+ using step_height[OF h] by blast
+ obtain u where run: "execute inputs code t = Some u" and "length u = n"
+ using Cons.IH c len by blast
+ then show ?case using step by simp
+qed
+
+fun demand :: "expression \<Rightarrow> nat" where
+ "demand (Binary op a b) = max (demand a) (Suc (demand b))"
+| "demand (Cond c a b) = max (demand c) (max (Suc (demand a)) (2 + demand b))"
+| "demand (Let a b) = max (demand a) (Suc (demand b))"
+| "demand _ = 1"
+
+lemma demand_positive: "0 < demand e"
+ by (induction e) auto
+
+fun bounded :: "nat \<Rightarrow> instruction list \<Rightarrow> nat \<Rightarrow> bool" where
+ "bounded limit [] n = (n \<le> limit)"
+| "bounded limit (i # code) n = (n \<le> limit \<and> (case height i n of None \<Rightarrow> False | Some m \<Rightarrow> bounded limit code m))"
+
+lemma bounded_start: "bounded limit code n \<Longrightarrow> n \<le> limit"
+ by (cases code) auto
+
+lemma bounded_append:
+ "bounded limit (a @ b) n \<longleftrightarrow> bounded limit a n \<and> (\<exists>m. check a n = Some m \<and> bounded limit b m)"
+ by (induction a arbitrary: n) (auto dest: bounded_start split: option.splits bind_splits)
+
+lemma bounded_check:
+ "bounded limit code n \<Longrightarrow> \<exists>m. check code n = Some m \<and> m \<le> limit"
+ by (induction code arbitrary: n) (auto split: option.splits bind_splits)
+
+theorem compiled_height:
+ "scoped (length slots) e \<Longrightarrow> list_all (\<lambda>i. i < n) slots \<Longrightarrow>
+ check (compile e slots) n = Some (Suc n)"
+proof (induction e arbitrary: slots n)
+ case (Literal v)
+ then show ?case by simp
+next
+ case (Input i)
+ then show ?case by simp
+next
+ case (Variable i)
+ then show ?case by (simp add: list_all_length)
+next
+ case (Binary op a b)
+ then show ?case
+ by (simp add: check_append list_all_iff)
+next
+ case (Cond c a b)
+ then show ?case by (simp add: check_append list_all_iff)
+next
+ case (Let a b)
+ then show ?case by (simp add: check_append list_all_iff)
+qed
+
+theorem compiled_demand:
+ assumes "scoped (length slots) e" "list_all (\<lambda>i. i < n) slots"
+ shows "bounded limit (compile e slots) n \<longleftrightarrow> n + demand e \<le> limit"
+ using assms
+proof (induction e arbitrary: slots n)
+ case (Literal v)
+ then show ?case by auto
+next
+ case (Input i)
+ then show ?case by auto
+next
+ case (Variable i)
+ then show ?case by (auto simp: list_all_length)
+next
+ case (Binary op a b)
+ then show ?case using demand_positive[of a] demand_positive[of b]
+ by (auto simp: bounded_append compiled_height list_all_iff max_def; arith)
+next
+ case (Cond c a b)
+ then show ?case using demand_positive[of c] demand_positive[of a] demand_positive[of b]
+ by (auto simp: bounded_append compiled_height list_all_iff max_def; arith)
+next
+ case (Let a b)
+ then show ?case using demand_positive[of a] demand_positive[of b]
+ by (auto simp: bounded_append compiled_height list_all_iff max_def; arith)
+qed
+
+corollary closed_demand:
+ "scoped 0 e \<Longrightarrow> bounded limit (compile e []) 0 \<longleftrightarrow> demand e \<le> limit"
+ using compiled_demand[where slots="[]" and n=0] by simp
+
+fun snapshots :: "(input \<Rightarrow> pixel) \<Rightarrow> instruction list \<Rightarrow> pixel list \<Rightarrow> (pixel list list) option" where
+ "snapshots inputs [] s = Some [s]"
+| "snapshots inputs (i # code) s = Option.bind (step inputs i s)
+ (\<lambda>t. map_option ((#) s) (snapshots inputs code t))"
+
+lemma snapshots_nonempty:
+ "snapshots inputs code s = Some frames \<Longrightarrow> frames \<noteq> []"
+ by (cases code) (auto split: bind_splits option.splits)
+
+theorem snapshots_execute:
+ "snapshots inputs code s = Some frames \<Longrightarrow> execute inputs code s = Some (last frames)"
+proof (induction code arbitrary: s frames)
+ case Nil
+ then show ?case by auto
+next
+ case (Cons i code)
+ then obtain t rest where step: "step inputs i s = Some t"
+ and tail: "snapshots inputs code t = Some rest" and frames: "frames = s # rest"
+ by (auto split: bind_splits option.splits)
+ have "rest \<noteq> []" using snapshots_nonempty[OF tail] .
+ then show ?case using Cons.IH[OF tail] step frames by simp
+qed
+
+theorem bounded_execution:
+ "bounded limit code (length s) \<Longrightarrow>
+ \<exists>frames. snapshots inputs code s = Some frames \<and> list_all (\<lambda>t. length t \<le> limit) frames"
+proof (induction code arbitrary: s)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons i code)
+ then obtain m where bound: "length s \<le> limit" and h: "height i (length s) = Some m"
+ and tail: "bounded limit code m"
+ by (auto split: option.splits)
+ obtain t where step: "step inputs i s = Some t" and len: "length t = m"
+ using step_height[OF h] by blast
+ obtain frames where trace: "snapshots inputs code t = Some frames"
+ and safe: "list_all (\<lambda>t. length t \<le> limit) frames"
+ using Cons.IH tail len by blast
+ show ?case using step trace safe bound by auto
+qed
+
+corollary bounded_result:
+ "bounded limit code (length s) \<Longrightarrow>
+ \<exists>t. execute inputs code s = Some t \<and> length t \<le> limit"
+proof -
+ assume bound: "bounded limit code (length s)"
+ obtain frames where trace: "snapshots inputs code s = Some frames"
+ and safe: "list_all (\<lambda>t. length t \<le> limit) frames"
+ using bounded_execution[OF bound] by blast
+ have "frames \<noteq> []" using snapshots_nonempty[OF trace] .
+ then have "length (last frames) \<le> limit" using safe by (simp add: list_all_iff)
+ then show ?thesis using snapshots_execute[OF trace] by blast
+qed
+
+end
A => src/core/Encoding.thy +252 -0
@@ 1,252 @@
+theory Encoding
+ imports Native
+begin
+
+fun octets :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
+ "octets 0 n = []"
+| "octets (Suc k) n = n mod 256 # octets k (n div 256)"
+
+fun integer :: "nat list \<Rightarrow> nat" where
+ "integer [] = 0"
+| "integer (b # bs) = b + 256 * integer bs"
+
+lemma octets_length [simp]: "length (octets k n) = k"
+ by (induction k arbitrary: n) auto
+
+lemma octets_bytes: "set (octets k n) \<subseteq> {..<256}"
+ by (induction k arbitrary: n) auto
+
+lemma integer_octets: "integer (octets k n) = n mod 256 ^ k"
+ by (induction k arbitrary: n) (simp_all add: power_Suc mod_mult2_eq add.commute)
+
+lemma literal_bound: "unat (v :: pixel) < 256 ^ 8"
+ using unsigned_less[of v, where ?'a=nat] by simp
+
+lemma integer_literal [simp]: "word_of_nat (integer (octets 8 (unat v))) = (v :: pixel)"
+ using literal_bound[of v] by (simp add: integer_octets)
+
+fun pushcode :: "register \<Rightarrow> nat list" where
+ "pushcode Rax = [80]"
+| "pushcode Rcx = [81]"
+| "pushcode Rbx = [83]"
+| "pushcode Rdx = [82]"
+| "pushcode R8 = [65,80]"
+| "pushcode R9 = [65,81]"
+
+fun popcode :: "register \<Rightarrow> nat list" where
+ "popcode Rax = [88]"
+| "popcode Rcx = [89]"
+| "popcode Rbx = [91]"
+| "popcode Rdx = [90]"
+| "popcode R8 = [65,88]"
+| "popcode R9 = [65,89]"
+
+fun arithmetic :: "operator \<Rightarrow> nat list" where
+ "arithmetic Add = [72,1,200]"
+| "arithmetic Sub = [72,145,72,41,200]"
+| "arithmetic Mul = [72,15,175,193]"
+| "arithmetic And = [72,33,200]"
+| "arithmetic Or = [72,9,200]"
+| "arithmetic Xor = [72,49,200]"
+| "arithmetic Shl = [72,145,72,211,224]"
+| "arithmetic Shr = [72,145,72,211,232]"
+| "arithmetic Less = [72,145,72,57,200,15,146,192,72,15,182,192]"
+
+fun regno :: "register \<Rightarrow> nat" where
+ "regno Rax = 0" | "regno Rcx = 1" | "regno Rdx = 2"
+| "regno Rbx = 3" | "regno R8 = 8" | "regno R9 = 9"
+
+definition movecode :: "register \<Rightarrow> register \<Rightarrow> nat list" where
+ "movecode dst src = [72 + (if regno src \<ge> 8 then 4 else 0) + (if regno dst \<ge> 8 then 1 else 0),
+ 137, 192 + 8 * (regno src mod 8) + regno dst mod 8]"
+
+definition extend32 :: "nat \<Rightarrow> pixel" where
+ "extend32 n = word_of_int (signed_take_bit 31 (int n))"
+
+lemma extend32_octets [simp]: "extend32 (integer (octets 4 n)) = extend32 n"
+proof -
+ have "signed_take_bit 31 (int (n mod 256 ^ 4)) = signed_take_bit 31 (int n)"
+ by (simp add: signed_take_bit_eq_iff_take_bit_eq take_bit_eq_mod of_nat_mod)
+ then show ?thesis by (simp add: extend32_def integer_octets)
+qed
+
+fun encode :: "opcode \<Rightarrow> nat list" where
+ "encode (Immediate v) = (if extend32 (unat v) = v then [72,199,192] @ octets 4 (unat v)
+ else [72,184] @ octets 8 (unat v))"
+| "encode (Push r) = pushcode r"
+| "encode (Pop r) = popcode r"
+| "encode (Peek i) = (if i < 16 then [72,139,68,36,8 * i]
+ else [72,139,132,36] @ octets 4 (8 * i))"
+| "encode (Arithmetic op) = arithmetic op"
+| "encode Conditional = [72,133,219,72,15,69,193]"
+| "encode (Move dst src) = movecode dst src"
+
+fun encodable :: "opcode \<Rightarrow> bool" where
+ "encodable (Peek i) = (i < 2 ^ 28)"
+| "encodable _ = True"
+
+definition fixed :: "opcode list" where
+ "fixed = map Push [Rax,Rcx,Rbx,Rdx,R8,R9] @ map Pop [Rax,Rcx,Rbx,Rdx,R8,R9] @
+ map Arithmetic [Add,Sub,Mul,And,Or,Xor,Shl,Shr,Less] @ [Conditional] @
+ concat (map (\<lambda>dst. map (Move dst) [Rax,Rcx,Rbx,Rdx,R8,R9]) [Rax,Rcx,Rbx,Rdx,R8,R9])"
+
+definition decode :: "nat list \<Rightarrow> (opcode \<times> nat list) option" where
+ "decode bs = (if take 2 bs = [72,184] then
+ if 10 \<le> length bs \<and> list_all (\<lambda>b. b < 256) (take 8 (drop 2 bs)) then
+ Some (Immediate (word_of_nat (integer (take 8 (drop 2 bs)))), drop 10 bs) else None
+ else if take 3 bs = [72,199,192] then
+ if 7 \<le> length bs \<and> list_all (\<lambda>b. b < 256) (take 4 (drop 3 bs)) then
+ Some (Immediate (extend32 (integer (take 4 (drop 3 bs)))), drop 7 bs) else None
+ else if take 4 bs = [72,139,68,36] then
+ let n = integer (take 1 (drop 4 bs)) in
+ if 5 \<le> length bs \<and> n < 128 \<and> n mod 8 = 0
+ then Some (Peek (n div 8), drop 5 bs) else None
+ else if take 4 bs = [72,139,132,36] then
+ let n = integer (take 4 (drop 4 bs)) in
+ if 8 \<le> length bs \<and> list_all (\<lambda>b. b < 256) (take 4 (drop 4 bs)) \<and>
+ n mod 8 = 0 \<and> n div 8 < 2 ^ 28 then Some (Peek (n div 8), drop 8 bs) else None
+ else map_option (\<lambda>op. (op, drop (length (encode op)) bs))
+ (List.find (\<lambda>op. take (length (encode op)) bs = encode op) fixed))"
+
+lemma octets_all [simp]: "list_all (\<lambda>b. b < 256) (octets k n)"
+ using octets_bytes[of k n] by (auto simp: list_all_iff)
+
+lemma peek_bound:
+ "(i :: nat) < 2 ^ 28 \<Longrightarrow> 8 * i < 256 ^ 4"
+ by (simp; linarith)
+
+theorem decode_encode:
+ assumes valid: "encodable op"
+ shows "decode (encode op @ tail) = Some (op, tail)"
+proof (cases op)
+ case (Immediate v)
+ then show ?thesis
+ by (auto simp: decode_def take_add integer_literal split: if_splits)
+next
+ case (Push r)
+ then show ?thesis by (cases r) (simp_all add: decode_def fixed_def)
+next
+ case (Pop r)
+ then show ?thesis by (cases r) (simp_all add: decode_def fixed_def)
+next
+ case (Peek i)
+ have small: "i < 2 ^ 28" using valid Peek by simp
+ have bound: "8 * i < 4294967296" using peek_bound[OF small] by simp
+ show ?thesis using Peek small bound
+ by (auto simp: decode_def integer_octets Let_def split: if_splits)
+next
+ case (Arithmetic op)
+ then show ?thesis by (cases op) (simp_all add: decode_def fixed_def)
+next
+ case Conditional
+ then show ?thesis by (simp add: decode_def fixed_def)
+next
+ case (Move dst src)
+ then show ?thesis by (cases dst; cases src) (simp_all add: decode_def fixed_def movecode_def)
+
+qed
+
+theorem encode_bytes: "set (encode op) \<subseteq> {..<256}"
+proof (cases op)
+ case (Immediate v)
+ then show ?thesis using octets_bytes by auto
+next
+ case (Push r)
+ then show ?thesis by (cases r) auto
+next
+ case (Pop r)
+ then show ?thesis by (cases r) auto
+next
+ case (Peek i)
+ then show ?thesis using octets_bytes by auto
+next
+ case (Arithmetic op)
+ then show ?thesis by (cases op) auto
+next
+ case Conditional
+ then show ?thesis by simp
+next
+ case (Move dst src)
+ then show ?thesis by (cases dst; cases src) (simp_all add: movecode_def)
+
+qed
+
+theorem encode_injective:
+ "encodable a \<Longrightarrow> encodable b \<Longrightarrow> encode a = encode b \<longleftrightarrow> a = b"
+ using decode_encode[of a "[]"] decode_encode[of b "[]"]
+ by (metis append_Nil option.inject prod.inject)
+
+lemma push_nonempty [simp]: "pushcode r \<noteq> []"
+ by (cases r) auto
+
+lemma pop_nonempty [simp]: "popcode r \<noteq> []"
+ by (cases r) auto
+
+lemma arithmetic_nonempty [simp]: "arithmetic op \<noteq> []"
+ by (cases op) auto
+
+lemma encode_nonempty [simp]: "encode op \<noteq> []"
+ by (cases op) (auto simp: movecode_def)
+
+lemma fixed_decode:
+ "List.find (\<lambda>op. take (length (encode op)) bs = encode op) fixed = Some op \<Longrightarrow>
+ 0 < length (encode op) \<and> length (encode op) \<le> length bs \<and>
+ list_all (\<lambda>b. b < 256) (take (length (encode op)) bs)"
+ using encode_bytes[of op]
+ by (auto simp: find_Some_iff list_all_iff dest: arg_cong[where f=length])
+
+theorem decode_progress:
+ "decode bs = Some (op,rest) \<Longrightarrow> length rest < length bs"
+ unfolding decode_def
+ apply (auto simp: Let_def dest: fixed_decode split: if_splits option.splits)
+ apply (drule fixed_decode)
+ apply auto
+ by (cases bs) auto
+
+theorem decode_consumed:
+ "decode bs = Some (op,rest) \<Longrightarrow> list_all (\<lambda>b. b < 256) bs \<Longrightarrow>
+ \<exists>prefix. bs = prefix @ rest \<and> prefix \<noteq> [] \<and> list_all (\<lambda>b. b < 256) prefix"
+proof -
+ assume decoded: "decode bs = Some (op,rest)"
+ and input: "list_all (\<lambda>b. b < 256) bs"
+ have drop: "rest = drop (length bs - length rest) bs"
+ using decoded unfolding decode_def
+ apply (auto simp: Let_def split: if_splits option.splits)
+ apply (drule fixed_decode)
+ by auto
+ have bytes: "list_all (\<lambda>b. b < 256) (take (length bs - length rest) bs)"
+ using input by (auto simp: list_all_iff dest: in_set_takeD)
+ have decomposition: "bs = take (length bs - length rest) bs @ rest"
+ using drop append_take_drop_id[of "length bs - length rest" bs] by metis
+ show ?thesis
+ using decomposition bytes decode_progress[OF decoded]
+ by (intro exI[where x="take (length bs - length rest) bs"]) auto
+qed
+
+fun recover :: "nat \<Rightarrow> nat list \<Rightarrow> (opcode list \<times> nat list) option" where
+ "recover 0 bs = Some ([],bs)"
+| "recover (Suc n) bs = Option.bind (decode bs) (\<lambda>(op,tail).
+ map_option (\<lambda>(ops,rest). (op # ops,rest)) (recover n tail))"
+
+theorem recover_encode:
+ "list_all encodable ops \<Longrightarrow>
+ recover (length ops) (concat (map encode ops) @ tail) = Some (ops,tail)"
+ by (induction ops) (simp_all add: decode_encode)
+
+function blocks :: "nat list \<Rightarrow> (nat list \<times> opcode) list option" where
+ "blocks bs = (if bs = [195] then Some [] else
+ Option.bind (decode bs) (\<lambda>(op,rest).
+ map_option (\<lambda>code. (take (length bs - length rest) bs,op) # code) (blocks rest)))"
+ by pat_completeness auto
+termination
+ by (relation "measure length") (auto dest: decode_progress)
+
+declare blocks.simps [simp del]
+
+definition executable :: "expression \<Rightarrow> nat list" where
+ "executable e = concat (map encode (program e)) @ [195]"
+
+theorem executable_bytes: "set (executable e) \<subseteq> {..<256}"
+ unfolding executable_def using encode_bytes by auto
+
+end
A => src/core/Model.thy +122 -0
@@ 1,122 @@
+theory Model
+ imports "HOL-Library.Word" "HOL-Library.Code_Target_Numeral"
+begin
+
+unbundle bit_operations_syntax
+
+type_synonym pixel = "64 word"
+
+datatype input = X | Y | T
+
+datatype operator = Add | Sub | Mul | And | Or | Xor | Shl | Shr | Less
+
+fun operate :: "operator \<Rightarrow> pixel \<Rightarrow> pixel \<Rightarrow> pixel" where
+ "operate Add a b = a + b"
+| "operate Sub a b = a - b"
+| "operate Mul a b = a * b"
+| "operate And a b = a AND b"
+| "operate Or a b = a OR b"
+| "operate Xor a b = a XOR b"
+| "operate Shl a b = push_bit (unat b mod 64) a"
+| "operate Shr a b = drop_bit (unat b mod 64) a"
+| "operate Less a b = (if a < b then 1 else 0)"
+
+datatype expression = Literal pixel | Input input | Variable nat
+ | Binary operator expression expression
+ | Cond expression expression expression
+ | Let expression expression
+
+fun evaluate :: "expression \<Rightarrow> pixel list \<Rightarrow> (input \<Rightarrow> pixel) \<Rightarrow> pixel" where
+ "evaluate (Literal v) env inputs = v"
+| "evaluate (Input i) env inputs = inputs i"
+| "evaluate (Variable i) env inputs = env ! i"
+| "evaluate (Binary op a b) env inputs = operate op (evaluate a env inputs) (evaluate b env inputs)"
+| "evaluate (Cond c a b) env inputs = (if evaluate c env inputs = 0 then evaluate b env inputs else evaluate a env inputs)"
+| "evaluate (Let a b) env inputs = evaluate b (evaluate a env inputs # env) inputs"
+
+fun scoped :: "nat \<Rightarrow> expression \<Rightarrow> bool" where
+ "scoped n (Literal v) = True"
+| "scoped n (Input i) = True"
+| "scoped n (Variable i) = (i < n)"
+| "scoped n (Binary op a b) = (scoped n a \<and> scoped n b)"
+| "scoped n (Cond c a b) = (scoped n c \<and> scoped n a \<and> scoped n b)"
+| "scoped n (Let a b) = (scoped n a \<and> scoped (Suc n) b)"
+
+fun fold_binary :: "operator \<Rightarrow> expression \<Rightarrow> expression \<Rightarrow> expression" where
+ "fold_binary op (Literal a) (Literal b) = Literal (operate op a b)"
+| "fold_binary op a b = (if b = Literal 0 \<and> op \<in> {Add,Sub,Or,Xor,Shl,Shr} then a
+ else if a = Literal 0 \<and> op \<in> {Add,Or,Xor} then b
+ else if b = Literal 1 \<and> op = Mul then a
+ else if a = Literal 1 \<and> op = Mul then b
+ else if b = Literal (-1) \<and> op = And then a
+ else if a = Literal (-1) \<and> op = And then b
+ else if b = Literal 0 \<and> op \<in> {Mul,And} then Literal 0
+ else if a = Literal 0 \<and> op \<in> {Mul,And,Shl,Shr} then Literal 0
+ else if b = Literal (-1) \<and> op = Or then Literal (-1)
+ else if a = Literal (-1) \<and> op = Or then Literal (-1) else Binary op a b)"
+
+fun fold_cond :: "expression \<Rightarrow> expression \<Rightarrow> expression \<Rightarrow> expression" where
+ "fold_cond (Literal c) a b = (if c = 0 then b else a)"
+| "fold_cond c a b = (if a = b then a else Cond c a b)"
+
+fun optimise :: "expression \<Rightarrow> expression" where
+ "optimise (Binary op a b) = fold_binary op (optimise a) (optimise b)"
+| "optimise (Cond c a b) = fold_cond (optimise c) (optimise a) (optimise b)"
+| "optimise (Let a b) = Let (optimise a) (optimise b)"
+| "optimise e = e"
+
+lemma fold_binary_value:
+ "evaluate (fold_binary op a b) env inputs = operate op (evaluate a env inputs) (evaluate b env inputs)"
+ by (cases op; cases a; cases b) auto
+
+lemma fold_cond_value:
+ "evaluate (fold_cond c a b) env inputs = (if evaluate c env inputs = 0 then evaluate b env inputs else evaluate a env inputs)"
+ by (cases c) auto
+
+theorem optimise_correct:
+ "evaluate (optimise e) env inputs = evaluate e env inputs"
+ by (induction e arbitrary: env) (simp_all add: fold_binary_value fold_cond_value)
+
+lemma fold_binary_scoped:
+ "scoped n a \<Longrightarrow> scoped n b \<Longrightarrow> scoped n (fold_binary op a b)"
+ by (cases a; cases b) auto
+
+lemma fold_cond_scoped:
+ "scoped n c \<Longrightarrow> scoped n a \<Longrightarrow> scoped n b \<Longrightarrow> scoped n (fold_cond c a b)"
+ by (cases c) auto
+
+theorem optimise_scoped: "scoped n e \<Longrightarrow> scoped n (optimise e)"
+ by (induction e arbitrary: n) (auto intro: fold_binary_scoped fold_cond_scoped)
+
+fun nodes :: "expression \<Rightarrow> nat" where
+ "nodes (Binary op a b) = Suc (nodes a + nodes b)"
+| "nodes (Cond c a b) = Suc (nodes c + nodes a + nodes b)"
+| "nodes (Let a b) = Suc (nodes a + nodes b)"
+| "nodes _ = 1"
+
+lemma fold_binary_nodes: "nodes (fold_binary op a b) \<le> Suc (nodes a + nodes b)"
+ by (cases a; cases b) auto
+
+lemma fold_cond_nodes: "nodes (fold_cond c a b) \<le> Suc (nodes c + nodes a + nodes b)"
+ by (cases c) auto
+
+theorem optimise_size: "nodes (optimise e) \<le> nodes e"
+ by (induction e) (auto intro: order_trans[OF fold_binary_nodes] order_trans[OF fold_cond_nodes])
+
+lemma fold_binary_idempotent:
+ "optimise a = a \<Longrightarrow> optimise b = b \<Longrightarrow>
+ optimise (fold_binary op a b) = fold_binary op a b"
+ by (cases a; cases b) auto
+
+lemma fold_cond_idempotent:
+ "optimise c = c \<Longrightarrow> optimise a = a \<Longrightarrow> optimise b = b \<Longrightarrow>
+ optimise (fold_cond c a b) = fold_cond c a b"
+ by (cases c) auto
+
+theorem optimise_idempotent: "optimise (optimise e) = optimise e"
+ by (induction e) (auto intro: fold_binary_idempotent fold_cond_idempotent)
+
+theorem scoped_weaken: "scoped n e \<Longrightarrow> n \<le> m \<Longrightarrow> scoped m e"
+ by (induction e arbitrary: n m) auto
+
+end
A => src/core/Native.thy +191 -0
@@ 1,191 @@
+theory Native
+ imports Compiler
+begin
+
+datatype register = Rax | Rcx | Rbx | Rdx | R8 | R9
+
+datatype opcode = Immediate pixel | Push register | Pop register | Peek nat
+ | Arithmetic operator | Conditional | Move register register
+
+record machine =
+ registers :: "register \<Rightarrow> pixel"
+ stack :: "pixel list"
+
+fun input_register :: "input \<Rightarrow> register" where
+ "input_register X = R8"
+| "input_register Y = R9"
+| "input_register T = Rdx"
+
+definition inputs :: "machine \<Rightarrow> input \<Rightarrow> pixel" where
+ "inputs s i = registers s (input_register i)"
+
+fun exchanges :: "operator \<Rightarrow> bool" where
+ "exchanges Sub = True"
+| "exchanges Shl = True"
+| "exchanges Shr = True"
+| "exchanges Less = True"
+| "exchanges _ = False"
+
+fun transition :: "opcode \<Rightarrow> machine \<Rightarrow> machine option" where
+ "transition (Immediate v) s = Some (s\<lparr>registers := (registers s)(Rax := v)\<rparr>)"
+| "transition (Push r) s = Some (s\<lparr>stack := registers s r # stack s\<rparr>)"
+| "transition (Pop r) s = (case stack s of [] \<Rightarrow> None | v # vs \<Rightarrow>
+ Some (s\<lparr>registers := (registers s)(r := v), stack := vs\<rparr>))"
+| "transition (Peek i) s = (if i < length (stack s) then
+ Some (s\<lparr>registers := (registers s)(Rax := stack s ! i)\<rparr>) else None)"
+| "transition (Arithmetic op) s = Some (s\<lparr>registers :=
+ (registers s)(Rcx := if exchanges op then registers s Rax else registers s Rcx,
+ Rax := operate op (registers s Rcx) (registers s Rax))\<rparr>)"
+| "transition Conditional s = Some (s\<lparr>registers :=
+ (registers s)(Rax := if registers s Rbx = 0 then registers s Rax else registers s Rcx)\<rparr>)"
+| "transition (Move dst src) s = Some (s\<lparr>registers := (registers s)(dst := registers s src)\<rparr>)"
+
+fun run :: "opcode list \<Rightarrow> machine \<Rightarrow> machine option" where
+ "run [] s = Some s"
+| "run (i # code) s = Option.bind (transition i s) (run code)"
+
+lemma run_append:
+ "run (a @ b) s = Option.bind (run a s) (run b)"
+ by (induction a arbitrary: s) (auto split: option.splits bind_splits)
+
+fun lower :: "instruction \<Rightarrow> opcode list" where
+ "lower (Constant v) = [Immediate v, Push Rax]"
+| "lower (Fetch i) = [Push (input_register i)]"
+| "lower (Pick i) = [Peek i, Push Rax]"
+| "lower (Calculate op) = [Pop Rax, Pop Rcx, Arithmetic op, Push Rax]"
+| "lower Choose = [Pop Rax, Pop Rcx, Pop Rbx, Conditional, Push Rax]"
+| "lower Slide = [Pop Rax, Pop Rcx, Push Rax]"
+
+definition observe :: "machine \<Rightarrow> (input \<Rightarrow> pixel) \<times> pixel list" where
+ "observe s = (inputs s, stack s)"
+
+lemma input_scratch [simp]:
+ "input_register i \<noteq> Rax"
+ "input_register i \<noteq> Rcx"
+ "input_register i \<noteq> Rbx"
+ by (cases i; simp)+
+
+lemma inputs_update [simp]:
+ "inputs (s\<lparr>registers := (registers s)(Rax := a)\<rparr>) = inputs s"
+ "inputs (s\<lparr>registers := (registers s)(Rcx := a)\<rparr>) = inputs s"
+ "inputs (s\<lparr>registers := (registers s)(Rbx := a)\<rparr>) = inputs s"
+ "inputs (s\<lparr>stack := vs\<rparr>) = inputs s"
+ by (auto simp: inputs_def fun_eq_iff split: input.splits)
+
+theorem lower_correct:
+ "map_option observe (run (lower i) s) =
+ map_option (\<lambda>vs. (inputs s, vs)) (step (inputs s) i (stack s))"
+proof (cases i)
+ case (Constant v)
+ then show ?thesis by (simp add: observe_def)
+next
+ case (Fetch i)
+ then show ?thesis by (simp add: observe_def inputs_def)
+next
+ case (Pick i)
+ then show ?thesis by (simp add: observe_def)
+next
+ case (Calculate op)
+ then show ?thesis
+ by (cases "stack s"; simp add: observe_def inputs_def fun_eq_iff split: list.splits input.splits)
+next
+ case Choose
+ then show ?thesis
+ by (cases "stack s"; simp add: observe_def inputs_def fun_eq_iff split: list.splits input.splits)
+next
+ case Slide
+ then show ?thesis
+ by (cases "stack s"; simp add: observe_def inputs_def fun_eq_iff split: list.splits input.splits)
+qed
+
+definition native :: "instruction list \<Rightarrow> opcode list" where
+ "native code = concat (map lower code)"
+
+theorem native_correct:
+ "map_option observe (run (native code) s) =
+ map_option (\<lambda>vs. (inputs s, vs)) (execute (inputs s) code (stack s))"
+proof (induction code arbitrary: s)
+ case Nil
+ then show ?case by (simp add: native_def observe_def)
+next
+ case (Cons i code)
+ show ?case
+ using Cons.IH lower_correct[of i s]
+ by (auto simp: native_def run_append observe_def split: option.splits bind_splits)
+qed
+
+corollary native_expression:
+ assumes "scoped 0 e"
+ shows "map_option observe (run (native (compile (optimise e) [])) s) =
+ Some (inputs s, evaluate e [] (inputs s) # stack s)"
+proof -
+ have code: "execute (inputs s) (compile (optimise e) []) (stack s) =
+ Some (evaluate e [] (inputs s) # stack s)"
+ using compile_correct[where e="optimise e" and env="[]" and slots="[]" and s="stack s" and inputs="inputs s"]
+ assms optimise_scoped
+ by (simp add: represents_def optimise_correct)
+ show ?thesis using native_correct[of "compile (optimise e) []" s] code by simp
+qed
+
+theorem native_return:
+ assumes "scoped 0 e"
+ shows "\<exists>q. run (native (compile (optimise e) []) @ [Pop Rax]) s = Some q \<and>
+ registers q Rax = evaluate e [] (inputs s) \<and> stack q = stack s \<and> inputs q = inputs s"
+proof -
+ obtain q where run: "run (native (compile (optimise e) [])) s = Some q"
+ and ins: "inputs q = inputs s" and stk: "stack q = evaluate e [] (inputs s) # stack s"
+ using native_expression[OF assms, of s]
+ by (auto simp: observe_def split: option.splits)
+ show ?thesis using run ins stk
+ by (auto simp: run_append inputs_def fun_eq_iff)
+qed
+
+fun writes :: "opcode \<Rightarrow> register set" where
+ "writes (Immediate v) = {Rax}"
+| "writes (Pop r) = {r}"
+| "writes (Move dst src) = {dst}"
+| "writes (Peek i) = {Rax}"
+| "writes (Arithmetic op) = {Rax,Rcx}"
+| "writes Conditional = {Rax}"
+| "writes _ = {}"
+
+lemma transition_preserves:
+ "transition i s = Some t \<Longrightarrow> r \<notin> writes i \<Longrightarrow> registers t r = registers s r"
+ by (cases i) (auto split: list.splits if_splits)
+
+theorem run_preserves:
+ "run code s = Some t \<Longrightarrow> list_all (\<lambda>i. r \<notin> writes i) code \<Longrightarrow>
+ registers t r = registers s r"
+ by (induction code arbitrary: s) (auto dest: transition_preserves split: option.splits bind_splits)
+
+lemma lower_scratch:
+ "list_all (\<lambda>i. writes i \<subseteq> {Rax,Rcx,Rbx}) (lower op)"
+ by (cases op) auto
+
+fun transfers :: "opcode list \<Rightarrow> opcode list" where
+ "transfers (Push src # Pop dst # code) =
+ (if src = dst then transfers code else Move dst src # transfers code)"
+| "transfers (op # code) = op # transfers code"
+| "transfers [] = []"
+
+theorem transfers_correct: "run (transfers code) s = run code s"
+ by (induction code arbitrary: s rule: transfers.induct)
+ (auto simp: fun_upd_idem split: if_splits option.splits bind_splits)
+
+lemma transfers_length: "length (transfers code) \<le> length code"
+ by (induction code rule: transfers.induct) auto
+
+lemma transfers_property:
+ "list_all P code \<Longrightarrow> (\<And>a b. P (Push a) \<Longrightarrow> P (Pop b) \<Longrightarrow> P (Move b a)) \<Longrightarrow>
+ list_all P (transfers code)"
+ by (induction code rule: transfers.induct) auto
+
+definition program :: "expression \<Rightarrow> opcode list" where
+ "program e = transfers (native (compile (optimise e) []) @ [Pop Rax])"
+
+theorem program_return:
+ "scoped 0 e \<Longrightarrow> \<exists>q. run (program e) s = Some q \<and>
+ registers q Rax = evaluate e [] (inputs s) \<and> stack q = stack s \<and> inputs q = inputs s"
+ unfolding program_def using native_return transfers_correct by metis
+
+end
A => tests/cli.py +131 -0
@@ 1,131 @@
+from pathlib import Path
+import os
+import resource
+import signal
+import subprocess
+import tempfile
+
+
+ROOT = Path(__file__).resolve().parents[1]
+
+
+def invoke(*args, ok=True, data=None, preexec_fn=None):
+ result = subprocess.run([str(ROOT / '.build/remy'), *map(str, args)], input=data,
+ capture_output=True, text=True, timeout=30, preexec_fn=preexec_fn)
+ assert (result.returncode == 0) == ok, (args, result.stdout, result.stderr)
+ return result.stdout if ok else result.stderr
+
+
+def main():
+ with tempfile.TemporaryDirectory() as directory:
+ source, binary = Path(directory) / 'source', Path(directory) / 'binary'
+ for text, expected in [('0x0',0),('0xff',255),('0X7F',127),('0xffffffffffffffff',(1 << 64)-1),
+ ('(+ 0xffffffffffffffff 1)',0),('(< 0x8000000000000000 0xffffffffffffffff)',1)]:
+ source.write_text(text)
+ assert int(invoke('eval',source,'0','0','0')) == expected, text
+ source.write_text('(+ x y)')
+ assert int(invoke('eval',source,'0xFF','0x1','0x0')) == 256
+ invoke(source,binary)
+ assert int(invoke('simulate',binary,'0xFF','0x1','0x0')) == 256
+ invoke('simulate',binary,'invalid','0','0',ok=False)
+ source.write_text('(let x1 7 (let x1 (+ x1 2) (* x1 x1)))')
+ assert int(invoke('eval',source,'0','0','0')) == 81
+ source.write_text('(let 1x 3 1x)')
+ invoke(source,binary,ok=False)
+ for text in ['(+ x; ignore ) tokens\ny) ; end', '(+ x; comment\r\ny)', '(+ x y);end']:
+ source.write_text(text)
+ assert int(invoke('eval',source,'3','4','0')) == 7, text
+ for text, position in [('(+ x)',3),('(div x y)',1),('(let a 3 b)',4),('(+ x y',4),('(+ x y) 1',5)]:
+ source.write_text(text)
+ assert f'token {position}\n' in invoke(source,binary,ok=False), text
+ source.write_text('(+ 1 ' * 129 + '0' + ')' * 129)
+ assert 'parse depth limit' in invoke(source,binary,ok=False)
+ large = '0'
+ for _ in range(12):
+ large = f'(+ {large} {large})'
+ source.write_text(large)
+ assert '4096 nodes' in invoke(source,binary,ok=False)
+ source.write_text('(+ x y)')
+ invoke('limits',4,3,2,source,binary)
+ for depth, nodes, stack, message in [(4,2,2,'2 nodes'),(4,3,1,'1 words'),
+ (0,3,2,'parse depth'),(129,3,2,'compiler bounds'),('bad',3,2,'invalid resource')]:
+ binary.write_bytes(b'preserve')
+ assert message in invoke('limits',depth,nodes,stack,source,binary,ok=False)
+ assert binary.read_bytes() == b'preserve'
+ source.write_text('(+ x y)')
+ invoke(source,binary)
+ listing = invoke('disassemble',binary)
+ assert 'mov rax r9' in listing and 'arithmetic add' in listing and 'ret' in listing
+ assert 'push' not in listing and 'pop' not in listing
+ source.write_text('(- x (- y (- t x)))')
+ invoke(source,binary)
+ listing = invoke('disassemble',binary)
+ assert 'push rax' in listing and 'pop rcx' in listing
+ source.write_text('(if x (+ y 7) (- t 9))')
+ invoke(source,binary)
+ listing = invoke('disassemble',binary)
+ assert 'jz ' in listing and 'jmp ' in listing and 'conditional ' not in listing
+ invoke('check',binary)
+ original = binary.read_bytes()
+ branch = original.index(bytes.fromhex('48 85 c0 0f 84'))
+ for offset in (0,4,0x7fffffff,0xffffffff):
+ damaged = bytearray(original)
+ damaged[branch+5:branch+9] = offset.to_bytes(4,'little')
+ binary.write_bytes(damaged)
+ invoke('check',binary,ok=False)
+ for cut in range(branch+1,branch+9):
+ binary.write_bytes(original[:cut]+bytes([195]))
+ invoke('check',binary,ok=False)
+ for malformed in [b'',bytes([195,0]),bytes([72,199,192,0]),bytes([80])]:
+ binary.write_bytes(malformed)
+ assert 'invalid native' in invoke('disassemble',binary,ok=False)
+ binary.write_bytes(bytes([72,184,42,0,0,0,0,0,0,0,195]))
+ assert '10 ret' in invoke('disassemble',binary)
+ source.write_text('(+ x y)')
+ invoke(source,binary)
+ assert 'verified' in invoke('check',binary)
+ for code in [[88,195],[80,195],[65,88,195],[73,137,192,195],[72,139,68,36,0,195]]:
+ binary.write_bytes(bytes(code))
+ invoke('check',binary,ok=False)
+ binary.write_bytes(bytes([72,199,192,42,0,0,0,195]))
+ invoke('check',binary)
+ source.write_text('(+ x y)')
+ binary.write_bytes(b'preserve')
+ binary.chmod(0o600)
+ invoke(source,binary,preexec_fn=lambda: os.umask(0))
+ assert binary.stat().st_mode & 0o777 == 0o600
+ def restricted():
+ signal.signal(signal.SIGXFSZ,signal.SIG_IGN)
+ resource.setrlimit(resource.RLIMIT_FSIZE,(1,1))
+ for args in [(source,binary),('vectors',source,binary)]:
+ binary.write_bytes(b'preserve')
+ invoke(*args,ok=False,preexec_fn=restricted)
+ assert binary.read_bytes() == b'preserve'
+ assert not list(binary.parent.glob('.binary.*'))
+ target = Path(directory) / 'folder'
+ target.mkdir()
+ invoke(source,target,ok=False)
+ assert not list(target.parent.glob('.folder.*'))
+ source.write_text('(+ x y)')
+ invoke(source,source)
+ assert source.read_bytes().endswith(bytes([195]))
+ invoke('-',binary,data='(+ x y)')
+ assert int(invoke('eval','-',3,4,0,data='(+ x y)')) == 7
+ invoke('vectors','-',binary,data='(+ x y)')
+ assert binary.stat().st_size == 16384
+ for data in ['(+ x)', ' ' * 65537]:
+ binary.write_bytes(b'preserve')
+ invoke('-',binary,data=data,ok=False)
+ assert binary.read_bytes() == b'preserve'
+ source.write_text('é')
+ assert 'ASCII' in invoke(source,binary,ok=False)
+ for text in ['0x','0x10000000000000000','0xfg','0xffextra','-0x1']:
+ source.write_text(text)
+ binary.write_bytes(b'preserve')
+ invoke(source,binary,ok=False)
+ assert binary.read_bytes() == b'preserve', text
+ print('CLI literal and rejection checks passed')
+
+
+if __name__ == '__main__':
+ main()
A => tests/guest.py +263 -0
@@ 1,263 @@
+import json
+from pathlib import Path
+import re
+import signal
+import socket
+import struct
+import subprocess
+import sys
+import tempfile
+import time
+
+from live import message
+
+
+ROOT = Path(__file__).resolve().parents[1]
+ENTRY = struct.Struct('<H38sqqQ')
+
+
+def image(template, destination):
+ data = bytearray(template.read_bytes())
+ boots = [n for n in range(min(256, len(data) // 512))
+ if data[n*512+3] == 0x88 and data[n*512+510:n*512+512] == b'\x55\xaa']
+ if len(boots) != 1:
+ raise ValueError('expected a TempleOS RedSea ISO')
+ boot = boots[0]
+ offset, sectors, root, bitmap, _ = struct.unpack_from('<5q', data, boot*512+8)
+ if offset != boot or len(data) % 512:
+ raise ValueError('invalid RedSea geometry')
+ entries = []
+ size = ENTRY.unpack_from(data, root*512)[3]
+ for at in range(root*512, root*512+size, ENTRY.size):
+ row = ENTRY.unpack_from(data, at)
+ if row[1][0]:
+ entries.append(row)
+
+ def append(payload):
+ sector = len(data) // 512
+ data.extend(payload)
+ data.extend(bytes((-len(data)) % 512))
+ return sector
+
+ files = {p.name: p.read_bytes() for p in (ROOT / '.build/payload').iterdir()}
+ for name, payload in files.items():
+ if len(name.encode('ascii')) >= 38:
+ raise ValueError('RedSea filename exceeds 37 bytes')
+ entries.append((0x800, name.encode('ascii'), append(payload), len(payload), 0))
+ once = b'Cd("::/");;\n#include "Remy.HC"\ndirectory="::/";\nif (Verify()) Live(0);\n'
+ once_sector = append(once)
+ home = next(row for row in entries if row[1].split(b'\0')[0] == b'Home')
+ home_start, home_size = home[2:4]
+ for at in range(home_start*512, home_start*512+home_size, ENTRY.size):
+ if not data[at+2]:
+ data[at:at+ENTRY.size] = ENTRY.pack(0x800, b'Once.HC', once_sector, len(once), 0)
+ break
+ else:
+ raise ValueError('template Home directory has no spare entry')
+ new_root = len(data) // 512
+ new_size = ((len(entries)*ENTRY.size+511) // 512)*512
+ entries[0] = (entries[0][0], entries[0][1], new_root, new_size, entries[0][4])
+ entries[1] = (entries[1][0], entries[1][1], new_root, 0, entries[1][4])
+ append(b''.join(ENTRY.pack(*row) for row in entries))
+ for row in entries[2:]:
+ if row[0] & 0x10:
+ parent = row[2]*512+ENTRY.size
+ if ENTRY.unpack_from(data, parent)[1].split(b'\0')[0] == b'..':
+ struct.pack_into('<q', data, parent+40, new_root)
+ data.extend(bytes((-len(data)) % 2048))
+ total = len(data) // 512
+ if total - (offset + bitmap) >= bitmap*512*8:
+ raise ValueError('template allocation bitmap is too small')
+ struct.pack_into('<q', data, boot*512+16, total-offset)
+ struct.pack_into('<q', data, boot*512+24, new_root)
+ first = offset + bitmap
+ for sector in range(offset+sectors, total):
+ bit = sector-first
+ data[(offset+1)*512+bit//8] |= 1 << (bit % 8)
+ for sector in (16,18):
+ struct.pack_into('<I', data, sector*2048+80, len(data)//2048)
+ struct.pack_into('>I', data, sector*2048+84, len(data)//2048)
+ struct.pack_into('<I', data, sector*2048+152, new_root)
+ struct.pack_into('>I', data, sector*2048+156, new_root)
+ destination.write_bytes(data)
+
+
+def exact(connection, count):
+ result = bytearray()
+ while len(result) < count:
+ data = connection.recv(count-len(result))
+ if not data:
+ raise ConnectionError('guest serial connection closed')
+ result.extend(data)
+ return bytes(result)
+
+
+def reply(connection):
+ prefix = bytearray(exact(connection, 4))
+ while prefix != b'RMA1':
+ prefix.pop(0)
+ prefix.extend(exact(connection, 1))
+ return struct.unpack('<III', exact(connection, 12))
+
+
+def packet(source, revision, directory):
+ text, binary = directory / 'source', directory / 'packet'
+ text.write_text(source)
+ subprocess.run([ROOT / '.build/remy', 'package', str(revision), text, binary],
+ check=True, capture_output=True, timeout=30)
+ return binary.read_bytes()
+
+
+def checksum(data):
+ value = 14695981039346656037
+ for byte in data:
+ value = ((value ^ byte)*1099511628211) & ((1 << 64)-1)
+ return value
+
+
+def screen(qmp, path):
+ qmp.write(json.dumps({'execute':'screendump','arguments':{'filename':str(path)}}).encode()+b'\n')
+ while True:
+ response = json.loads(qmp.readline())
+ if 'return' in response:
+ break
+ if 'error' in response:
+ raise RuntimeError(response)
+ data = path.read_bytes()
+ header = re.match(rb'P6\s+(\d+)\s+(\d+)\s+255\s', data)
+ if not header:
+ raise ValueError('invalid QEMU PPM screenshot')
+ width, height = map(int, header.groups())
+ assert width >= 560 and height >= 400
+ pixels = data[header.end():]
+ return b''.join(pixels[(y*width+80)*3:(y*width+560)*3] for y in range(64,400))
+
+
+def main():
+ if len(sys.argv) != 2 or not sys.argv[1]:
+ raise SystemExit('usage: python3 tests/guest.py TempleOS.ISO')
+ destination = ROOT / '.build/guest.iso'
+ image(Path(sys.argv[1]), destination)
+ with tempfile.TemporaryDirectory(prefix='remy') as directory:
+ directory = Path(directory)
+ serial, monitor = directory / 'serial', directory / 'qmp'
+ log = (ROOT / '.build/guest.log').open('wb')
+ process = subprocess.Popen(['qemu-system-x86_64','-m','512','-smp','2',
+ '-accel','tcg,thread=multi','-cdrom',destination,'-boot','d','-display','none',
+ '-monitor','none','-no-reboot','-chardev',f'socket,id=live,path={serial},server=on,wait=off',
+ '-serial','chardev:live','-qmp',f'unix:{monitor},server=on,wait=off'],stdout=log,stderr=log)
+ connection = socket.socket(socket.AF_UNIX, socket.SOCK_STREAM)
+ control = socket.socket(socket.AF_UNIX, socket.SOCK_STREAM)
+ qmp = None
+ watcher = None
+ try:
+ until = time.monotonic()+15
+ while not serial.exists() or not monitor.exists():
+ if time.monotonic()>until or process.poll() is not None:
+ raise RuntimeError('QEMU did not start')
+ time.sleep(0.1)
+ connection.connect(str(serial))
+ connection.settimeout(90)
+ control.connect(str(monitor))
+ control.settimeout(5)
+ qmp = control.makefile('rwb',buffering=0)
+ json.loads(qmp.readline())
+ qmp.write(b'{"execute":"qmp_capabilities"}\n')
+ while 'return' not in json.loads(qmp.readline()):
+ pass
+ assert reply(connection) == (0,0,0)
+ print('guest booted and verified all three payloads',flush=True)
+ connection.settimeout(30)
+ connection.sendall(packet('(+ x y)',1,directory))
+ assert reply(connection) == (1,1,1)
+ time.sleep(1)
+ before = screen(qmp,ROOT / '.build/first.ppm')
+ second = packet('(if (< x y) (+ x 3) (- y 9))',2,directory)
+ connection.sendall(second)
+ assert reply(connection) == (2,1,2)
+ time.sleep(1)
+ after = screen(qmp,ROOT / '.build/second.ppm')
+ assert before != after, 'accepted revision did not change rendered pixels'
+ print('guest changed rendered pixels after two verified revisions',flush=True)
+ corrupt = bytearray(packet('(xor x y)',3,directory))
+ corrupt[-1] ^= 1
+ connection.sendall(corrupt)
+ assert reply(connection) == (3,2,2)
+ corrupt = bytearray(packet('(xor x y)',4,directory))
+ corrupt[-1] ^= 1
+ struct.pack_into('<Q',corrupt,20,checksum(corrupt[:20]+corrupt[28:]))
+ connection.sendall(corrupt)
+ assert reply(connection) == (4,3,2)
+ time.sleep(1)
+ assert screen(qmp,ROOT / '.build/rejected.ppm') == after
+ invalid = ((1,0),(1,65537),(1,0xffffffff),(2,0),(2,65537),(3,0),(3,513),(4,0))
+ for sequence,(field,value) in enumerate(invalid,10):
+ header = bytearray(packet('(xor x y)',sequence,directory)[:28])
+ struct.pack_into('<I',header,4*field,value)
+ connection.sendall(header)
+ assert reply(connection) == (0 if field == 4 else sequence,4,2)
+ print('guest rejected checksum, vector and header failures without changing the active shader',flush=True)
+ connection.sendall(second[:12])
+ time.sleep(6)
+ connection.sendall(packet('(xor x y)',0xffffffff,directory))
+ assert reply(connection) == (0xffffffff,1,0xffffffff)
+ print('guest recovered from a partial frame',flush=True)
+ connection.close()
+ source = directory/'watch'
+ source.write_text('(* x y)')
+ watcher = subprocess.Popen(['python3',ROOT/'cli/watch.py',source,'--socket',serial,'--interval','0.1'],
+ stdout=subprocess.PIPE,stderr=subprocess.PIPE)
+ message(watcher.stdout,b'accepted',timeout=90)
+ time.sleep(1)
+ watched = screen(qmp,ROOT / '.build/watched.ppm')
+ source.write_text('(+ x)')
+ message(watcher.stderr,b'syntax error',timeout=30)
+ assert screen(qmp,ROOT / '.build/invalid.ppm') == watched
+ source.write_text('(and x y)')
+ message(watcher.stdout,b'accepted',timeout=90)
+ time.sleep(1)
+ final = screen(qmp,ROOT / '.build/final.ppm')
+ assert final != watched
+ print('watcher edits reached the real guest and an invalid source preserved its frame',flush=True)
+ watcher.send_signal(signal.SIGINT)
+ watcher.wait(timeout=5)
+ assert watcher.returncode == 0
+ qmp.write(b'{"execute":"human-monitor-command","arguments":{"command-line":"sendkey esc"}}\n')
+ while 'return' not in json.loads(qmp.readline()):
+ pass
+ time.sleep(2)
+ assert screen(qmp,ROOT / '.build/stopped.ppm') != final
+ print('guest renderer and receiver stopped through Escape',flush=True)
+ except Exception:
+ if qmp is not None:
+ try:
+ screen(qmp,ROOT / '.build/failure.ppm')
+ except Exception:
+ pass
+ raise
+ finally:
+ if watcher is not None:
+ if watcher.poll() is None:
+ watcher.terminate()
+ try:
+ watcher.wait(timeout=5)
+ except subprocess.TimeoutExpired:
+ watcher.kill()
+ watcher.wait()
+ watcher.stdout.close()
+ watcher.stderr.close()
+ connection.close()
+ if qmp is not None:
+ qmp.close()
+ control.close()
+ process.terminate()
+ try:
+ process.wait(timeout=10)
+ except subprocess.TimeoutExpired:
+ process.kill()
+ process.wait()
+ log.close()
+
+
+if __name__ == '__main__':
+ main()
A => tests/live.py +172 -0
@@ 1,172 @@
+import os
+from pathlib import Path
+import select
+import signal
+import socket
+import struct
+import subprocess
+import tempfile
+import time
+
+
+ROOT = Path(__file__).resolve().parents[1]
+HEADER = struct.Struct('<4sIIIIQ')
+
+
+def checksum(data):
+ value = 14695981039346656037
+ for byte in data:
+ value = ((value ^ byte)*1099511628211) & ((1 << 64)-1)
+ return value
+
+
+def exact(connection, count):
+ data = bytearray()
+ while len(data) < count:
+ chunk = connection.recv(count-len(data))
+ if not chunk:
+ raise ConnectionError('watcher disconnected')
+ data.extend(chunk)
+ return bytes(data)
+
+
+def receive(connection):
+ head = exact(connection, HEADER.size)
+ magic, code, source, rows, revision, digest = HEADER.unpack(head)
+ assert magic == b'RMY1' and rows == 512 and 0 < revision < 1 << 32
+ assert 0 < code <= 65536 and 0 < source <= 65536
+ body = exact(connection, code+source+32*rows)
+ assert digest == checksum(head[:20]+body)
+ return head+body, body[code:code+source], revision
+
+
+def acknowledge(connection, revision):
+ response = struct.pack('<4sIII',b'RMA1',revision,1,revision)
+ connection.sendall(response[:6])
+ time.sleep(0.05)
+ connection.sendall(response[6:])
+
+
+def message(stream, expected, timeout=10):
+ end = time.monotonic()+timeout
+ data = b''
+ while expected not in data:
+ if not select.select([stream],[],[],max(0,end-time.monotonic()))[0]:
+ raise AssertionError((expected,data))
+ chunk = os.read(stream.fileno(),4096)
+ if not chunk:
+ raise AssertionError((expected,data))
+ data += chunk
+
+
+def main():
+ with tempfile.TemporaryDirectory(prefix='remylive') as directory:
+ directory = Path(directory)
+ source, binary = directory/'source',directory/'packet'
+ source.write_text('(+ x y)')
+ subprocess.run([ROOT/'.build/remy','package','1',source,binary],check=True,capture_output=True)
+ first = binary.read_bytes()
+ magic, code, count, rows, revision, digest = HEADER.unpack(first[:28])
+ assert (magic,count,rows,revision) == (b'RMY1',7,512,1)
+ assert len(first) == 28+code+count+rows*32
+ assert digest == checksum(first[:20]+first[28:])
+ native = directory/'native'
+ subprocess.run([ROOT/'.build/remy',source,native],check=True,capture_output=True)
+ assert first[28:28+code] == native.read_bytes()
+ vectors = first[28+code+count:]
+ for at in range(0,len(vectors),32):
+ x,y,t,result = struct.unpack_from('<4Q',vectors,at)
+ assert result == (x+y) & ((1 << 64)-1)
+ source.write_bytes(b'(+ x y);'+b'a'*(65536-8))
+ subprocess.run([ROOT/'.build/remy','package',str((1 << 32)-1),source,binary],
+ check=True,capture_output=True,timeout=30)
+ maximum = binary.read_bytes()
+ fields = HEADER.unpack(maximum[:28])
+ assert fields[2] == 65536 and fields[4] == (1 << 32)-1
+ assert fields[5] == checksum(maximum[:20]+maximum[28:])
+ source.write_text('(+ x y)')
+ for revision in ('0',str(1 << 32),'bad'):
+ binary.write_bytes(b'preserve')
+ result = subprocess.run([ROOT/'.build/remy','package',revision,source,binary],capture_output=True)
+ assert result.returncode and binary.read_bytes() == b'preserve'
+ source.write_text('(+ x)')
+ result = subprocess.run([ROOT/'.build/remy','package','2',source,binary],capture_output=True)
+ assert result.returncode and binary.read_bytes() == b'preserve'
+ source.write_text('(+ x y)')
+ server = socket.socket(socket.AF_UNIX,socket.SOCK_STREAM)
+ endpoint = directory/'serial'
+ server.bind(str(endpoint))
+ server.listen(1)
+ server.settimeout(15)
+ watcher = subprocess.Popen(['python3',ROOT/'cli/watch.py',source,'--socket',endpoint,'--interval','0.05'],
+ stdout=subprocess.PIPE,stderr=subprocess.PIPE)
+ connection = None
+ try:
+ connection,_ = server.accept()
+ connection.settimeout(10)
+ original, text, revision = receive(connection)
+ assert text == b'(+ x y)'
+ acknowledge(connection,revision)
+ message(watcher.stdout,b'accepted')
+ source.write_text('(+ x)')
+ message(watcher.stderr,b'syntax error')
+ connection.settimeout(0.4)
+ try:
+ data = connection.recv(1)
+ except socket.timeout:
+ pass
+ else:
+ raise AssertionError(('invalid source produced output',data))
+ connection.close()
+ connection,_ = server.accept()
+ connection.settimeout(10)
+ resent,text,same = receive(connection)
+ assert resent == original and same == revision
+ acknowledge(connection,same)
+ message(watcher.stdout,b'accepted')
+ temporary = directory/'replacement'
+ temporary.write_text('(- x y)')
+ temporary.replace(source)
+ updated,text,changed = receive(connection)
+ assert text == b'(- x y)' and changed != revision
+ message(watcher.stdout,b'compiled')
+ source.write_text('(* x 3)')
+ message(watcher.stdout,b'compiled')
+ source.write_text('(* x 7)')
+ message(watcher.stdout,b'compiled')
+ connection.settimeout(0.3)
+ try:
+ data = connection.recv(1)
+ except socket.timeout:
+ pass
+ else:
+ raise AssertionError(('unacknowledged transfer was not coalesced',data))
+ acknowledge(connection,changed)
+ message(watcher.stdout,b'accepted')
+ connection.settimeout(10)
+ updated,text,changed = receive(connection)
+ assert text == b'(* x 7)'
+ acknowledge(connection,changed)
+ message(watcher.stdout,b'accepted')
+ connection.sendall(struct.pack('<4sIII',b'RMA1',0,0,0))
+ reset,_,same = receive(connection)
+ assert reset == updated and same == changed
+ acknowledge(connection,same)
+ finally:
+ watcher.send_signal(signal.SIGINT)
+ try:
+ watcher.wait(timeout=5)
+ except subprocess.TimeoutExpired:
+ watcher.kill()
+ watcher.wait()
+ if connection is not None:
+ connection.close()
+ server.close()
+ watcher.stdout.close()
+ watcher.stderr.close()
+ assert watcher.returncode == 0
+ print('live packet bounds, independent vectors, compile rejection, fragmented replies, reconnect, atomic edits and guest restart passed')
+
+
+if __name__ == '__main__':
+ main()
A => tests/measure.c +72 -0
@@ 1,72 @@
+#define _GNU_SOURCE
+#include <inttypes.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <sys/mman.h>
+#include <time.h>
+#include <unistd.h>
+
+static uint64_t ticks(void)
+{
+ struct timespec now;
+ if (clock_gettime(CLOCK_MONOTONIC, &now)) {
+ perror("clock_gettime");
+ exit(1);
+ }
+ return (uint64_t)now.tv_sec * UINT64_C(1000000000) + now.tv_nsec;
+}
+
+int main(int argc, char **argv)
+{
+ if (argc != 2) return 1;
+ FILE *file = fopen(argv[1], "rb");
+ if (!file) return 1;
+ if (fseek(file, 0, SEEK_END)) {
+ fclose(file);
+ return 1;
+ }
+ long size = ftell(file);
+ long page = sysconf(_SC_PAGESIZE);
+ if (size <= 0 || size > 65536 || page <= 0 || fseek(file, 0, SEEK_SET)) {
+ fclose(file);
+ return 1;
+ }
+ size_t offset = ((size_t)size + page - 1) / page * page;
+ size_t capacity = offset + page;
+ unsigned char *image = mmap(NULL, capacity, PROT_READ | PROT_WRITE,
+ MAP_PRIVATE | MAP_ANONYMOUS, -1, 0);
+ if (image == MAP_FAILED) {
+ fclose(file);
+ return 1;
+ }
+ int failed = fread(image, 1, size, file) != (size_t)size;
+ failed |= fclose(file) != 0;
+ if (failed) {
+ munmap(image, capacity);
+ return 1;
+ }
+ unsigned char bridge[] = {0x53,0x49,0x89,0xf8,0x49,0x89,0xf1,0x48,0xb8,
+ 0,0,0,0,0,0,0,0,0xff,0xd0,0x5b,0xc3};
+ uint64_t address = (uintptr_t)image;
+ memcpy(bridge + 9, &address, sizeof(address));
+ memcpy(image + offset, bridge, sizeof(bridge));
+ if (mprotect(image, capacity, PROT_READ | PROT_EXEC)) {
+ munmap(image, capacity);
+ return 1;
+ }
+ uint64_t (*pixel)(uint64_t, uint64_t, uint64_t) = (void *)(image + offset);
+ uint64_t checksum = 0;
+ uint64_t begin = ticks();
+ for (uint64_t t = 0; t < 64; t++) {
+ for (uint64_t y = 0; y < 112; y++) {
+ for (uint64_t x = 0; x < 160; x++) {
+ checksum += pixel(x, y, 2*t) & 15;
+ }
+ }
+ }
+ uint64_t elapsed = ticks() - begin;
+ printf("%" PRIu64 " %" PRIu64 "\n", elapsed / 64, checksum);
+ return munmap(image, capacity) != 0;
+}
A => tests/measure.py +42 -0
@@ 1,42 @@
+from pathlib import Path
+import statistics
+import subprocess
+import tempfile
+
+
+ROOT = Path(__file__).resolve().parents[1]
+
+
+def main():
+ with tempfile.TemporaryDirectory() as directory:
+ directory = Path(directory)
+ runner = directory / 'measure'
+ subprocess.run(['cc', '-std=c11', '-O2', '-Wall', '-Wextra', '-Werror',
+ ROOT / 'tests/measure.c', '-o', runner], check=True)
+ print('example backend bytes stack_instructions median_frame_ns checksum')
+ for source in sorted((ROOT / 'examples').glob('*.remy')):
+ checksums = set()
+ for backend in ('baseline', 'allocated'):
+ binary = directory / backend
+ args = ['baseline'] if backend == 'baseline' else []
+ subprocess.run([ROOT / '.build/remy', *args, source, binary],
+ check=True, capture_output=True)
+ subprocess.run([ROOT / '.build/remy', 'check', binary],
+ check=True, capture_output=True)
+ listing = subprocess.run([ROOT / '.build/remy', 'disassemble', binary],
+ check=True, capture_output=True, text=True).stdout
+ traffic = sum(' push ' in row or ' pop ' in row for row in listing.splitlines())
+ samples = []
+ for _ in range(9):
+ result = subprocess.run([runner, binary], check=True, capture_output=True,
+ text=True, timeout=30)
+ elapsed, checksum = map(int, result.stdout.split())
+ samples.append(elapsed)
+ checksums.add(checksum)
+ print(source.stem, backend, binary.stat().st_size, traffic,
+ int(statistics.median(samples)), checksum)
+ assert len(checksums) == 1, (source, checksums)
+
+
+if __name__ == '__main__':
+ main()
A => tests/native.py +185 -0
@@ 1,185 @@
+import ctypes
+import itertools
+import mmap
+import multiprocessing
+import resource
+from pathlib import Path
+import platform
+import random
+import struct
+import subprocess
+import tempfile
+
+
+ROOT = Path(__file__).resolve().parents[1]
+MASK = (1 << 64) - 1
+OPERATORS = ("+", "-", "*", "and", "or", "xor", "shl", "shr", "<")
+
+
+def evaluate(e, env):
+ if isinstance(e, int):
+ return e
+ if isinstance(e, str):
+ return env[e]
+ op, *args = e
+ if op == "let":
+ name, a, b = args
+ return evaluate(b, {**env, name: evaluate(a, env)})
+ if op == "if":
+ c, a, b = args
+ return evaluate(a if evaluate(c, env) else b, env)
+ a, b = (evaluate(x, env) for x in args)
+ return {"+": lambda: a + b, "-": lambda: a - b, "*": lambda: a * b,
+ "and": lambda: a & b, "or": lambda: a | b, "xor": lambda: a ^ b,
+ "shl": lambda: a << (b & 63), "shr": lambda: a >> (b & 63),
+ "<": lambda: int(a < b)}[op]() & MASK
+
+
+def source(e):
+ return "(" + " ".join(map(source, e)) + ")" if isinstance(e, tuple) else str(e)
+
+
+def native(code):
+ image = mmap.mmap(-1, len(code), prot=mmap.PROT_READ | mmap.PROT_WRITE | mmap.PROT_EXEC)
+ image.write(code)
+ address = ctypes.addressof(ctypes.c_char.from_buffer(image))
+ bridge = bytes.fromhex("53 49 89 f8 49 89 f1 48 b8") + struct.pack("<Q", address) + bytes.fromhex("ff d0 5b c3")
+ thunk = mmap.mmap(-1, len(bridge), prot=mmap.PROT_READ | mmap.PROT_WRITE | mmap.PROT_EXEC)
+ thunk.write(bridge)
+ function = ctypes.CFUNCTYPE(ctypes.c_uint64, ctypes.c_uint64, ctypes.c_uint64, ctypes.c_uint64)(
+ ctypes.addressof(ctypes.c_char.from_buffer(thunk)))
+ return function, image, thunk
+
+
+def worker(connection, code, vectors):
+ resource.setrlimit(resource.RLIMIT_CORE,(0,0))
+ try:
+ function, image, thunk = native(code)
+ results = [function(*vector) for vector in vectors]
+ del function
+ image.close()
+ thunk.close()
+ connection.send((True,results))
+ except BaseException as error:
+ connection.send((False,repr(error)))
+ finally:
+ connection.close()
+
+
+def execute(code, vectors):
+ context = multiprocessing.get_context('fork')
+ reader, writer = context.Pipe(duplex=False)
+ process = context.Process(target=worker,args=(writer,code,vectors))
+ process.start()
+ writer.close()
+ try:
+ if not reader.poll(30):
+ raise RuntimeError('native child exceeded 30 seconds')
+ try:
+ ok, result = reader.recv()
+ except EOFError:
+ process.join(1)
+ raise RuntimeError(f'native child failed with status {process.exitcode}') from None
+ process.join(1)
+ if not ok or process.exitcode != 0:
+ raise RuntimeError(f'native child failed: {result}, status {process.exitcode}')
+ return result
+ finally:
+ reader.close()
+ if process.is_alive():
+ process.terminate()
+ process.join()
+ process.close()
+
+
+def generate(rng, depth, names):
+ if depth == 0 or rng.randrange(5) == 0:
+ return rng.choice([0, 1, 63, 64, 65, MASK, 1 << 63, *names])
+ kind = rng.randrange(5)
+ if kind == 0:
+ name = rng.choice(("a", "b", "c", "x"))
+ return ("let", name, generate(rng, depth - 1, names), generate(rng, depth - 1, [*names, name]))
+ if kind == 1:
+ return ("if", *(generate(rng, depth - 1, names) for _ in range(3)))
+ return (rng.choice(OPERATORS), *(generate(rng, depth - 1, names) for _ in range(2)))
+
+
+def main():
+ if platform.system() != "Linux" or platform.machine() != "x86_64":
+ raise RuntimeError("native differential tests require an x86-64 Linux host")
+ try:
+ execute(bytes.fromhex('0f 0b'),[(0,0,0)])
+ except RuntimeError as error:
+ assert 'status -4' in str(error), error
+ else:
+ raise AssertionError('invalid opcode did not kill the isolated child')
+ rng = random.Random(0x52454D59)
+ cases = [(op, "x", "y") for op in OPERATORS]
+ cases += [(op, "x", 0) for op in ("+", "-", "or", "xor", "shl", "shr")]
+ cases += [("*", "x", 1), ("*", 1, "x"), ("and", "x", MASK)]
+ cases += [("*", "x", 0), ("and", "x", 0), ("shl", 0, "y"), ("shr", 0, "y"), ("or", "x", MASK)]
+ cases += [("if", "x", ("+", "y", "t"), ("+", "y", "t"))]
+ cases += [("let", "x1", ("+", "x", 1), ("*", "x1", "x1"))]
+ cases += [("let", "a", ("+", "x", 3), ("+", "y", ("let", "b", "t", ("*", "a", "b")))),
+ ("let", "x", "y", ("if", "t", ("+", "x", 1), ("-", "x", 1)))]
+ cases += [("-", "x", ("if", "t", ("+", "x", "y"), ("*", "y", "t"))),
+ ("shl", "x", ("let", "a", ("+", "y", "t"), ("-", "a", "x"))),
+ ("let", "a", "x", ("+", ("if", "y", "a", "t"), ("if", "t", "y", "a")))]
+ cases += [generate(rng, 5, ["x", "y", "t"]) for _ in range(117)]
+ atoms = (0,1,MASK,'x','y','t')
+ exhaustive = list(atoms)
+ exhaustive += [(op,a,b) for op in OPERATORS for a,b in itertools.product(atoms,repeat=2)]
+ exhaustive += [('if',c,a,b) for c,a,b in itertools.product(atoms,repeat=3)]
+ exhaustive += [('let','a',value,body) for value in atoms for body in (*atoms,'a')]
+ assert len(exhaustive) == 588
+ cases += exhaustive
+ comparisons = 0
+ with tempfile.TemporaryDirectory() as directory:
+ path, binary = Path(directory) / "source", Path(directory) / "binary"
+ path.write_text('(if x (+ y 7) (- t 9))')
+ subprocess.run([ROOT / '.build/remy',path,binary],check=True,capture_output=True)
+ conditional = binary.read_bytes()
+ start = conditional.index(bytes.fromhex('48 85 c0 0f 84'))
+ otherwise = start + 9 + int.from_bytes(conditional[start+5:start+9],'little')
+ damaged = bytearray(conditional)
+ damaged[otherwise:otherwise+2] = bytes.fromhex('0f 0b')
+ assert execute(bytes(damaged),[(1,3,2)]) == [10]
+ try:
+ execute(bytes(damaged),[(0,3,2)])
+ except RuntimeError as error:
+ assert 'status -4' in str(error), error
+ else:
+ raise AssertionError('selected poisoned branch did not execute')
+ damaged = bytearray(conditional)
+ damaged[start+9:start+11] = bytes.fromhex('0f 0b')
+ assert execute(bytes(damaged),[(0,3,2)]) == [MASK-6]
+ for case in cases:
+ path.write_text(source(case))
+ result = subprocess.run([ROOT / ".build/remy", path, binary], capture_output=True, text=True, timeout=30)
+ assert result.returncode == 0, (case, result.stderr)
+ checked = subprocess.run([ROOT / ".build/remy", "check", binary],capture_output=True,text=True,timeout=30)
+ assert checked.returncode == 0, (case,checked.stderr)
+ vectors = [(a, b, a ^ b) for a in (0, 1, MASK, 1 << 63) for b in (0, 1, 63, 64, 65, MASK)]
+ vectors += [tuple(rng.getrandbits(64) for _ in range(3)) for _ in range(24)]
+ results = execute(binary.read_bytes(),vectors)
+ for (x, y, t), actual in zip(vectors,results,strict=True):
+ expected = evaluate(case, {"x": x, "y": y, "t": t})
+ assert actual == expected, (source(case), x, y, t, expected, actual)
+ comparisons += 1
+ result = subprocess.run([ROOT / ".build/remy", "eval", path, str(x), str(y), str(t)],
+ capture_output=True, text=True, timeout=30)
+ assert result.returncode == 0 and int(result.stdout) == expected, (case, result.stdout, result.stderr)
+ simulated = subprocess.run([ROOT / '.build/remy', 'simulate', binary, str(x), str(y), str(t)],
+ capture_output=True, text=True, timeout=30)
+ assert simulated.returncode == 0 and int(simulated.stdout) == expected, (case, simulated.stdout, simulated.stderr)
+ for bad in ("", "(+ x)", "(+ x y) 1", "(let a 3 b)", "(if 1 2)", "(let if 3 4)",
+ "18446744073709551616", "(+ x z)", "(div x y)", "é", " " * 65537):
+ path.write_text(bad)
+ binary.write_bytes(b"preserve")
+ result = subprocess.run([ROOT / ".build/remy", path, binary], capture_output=True, timeout=30)
+ assert result.returncode != 0 and binary.read_bytes() == b"preserve", bad
+ print(f"{len(cases)} programs, {comparisons} native comparisons, byte interpreter and HOL reference checks, 11 rejection cases passed")
+
+
+if __name__ == "__main__":
+ main()
