M Makefile => Makefile +5 -1
@@ 1,6 1,6 @@
ISABELLE ?= isabelle
-.PHONY: all check measure payload clean
+.PHONY: all check measure payload guest clean
all: .build/ready
@@ 14,6 14,7 @@ all: .build/ready
check: all
python3 tests/native.py
python3 tests/cli.py
+ python3 tests/live.py
measure: all
python3 tests/measure.py
@@ 23,5 24,8 @@ payload: all
@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
M README.md => README.md +19 -3
@@ 1,4 1,4 @@
-Pixel expressions compile to native x86+64 for TempleOS through a compiler implemented in Isabelle/HOL with proofs of constant folding, lexical slot allocation, bounded stack execution and correspondence with a register and stack model
+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)
@@ 13,7 13,7 @@ It uses:
- Isabelle2026 and its bundled Poly/ML toolchain
- Python
-Copy these files onto `C:/` in TempleOS and run:
+Copy `.build/payload/*` onto `C:/` in TempleOS and run:
```c
#include "C:/Remy.HC";
@@ 33,6 33,22 @@ The byte interpreter follows encoded jumps and consumes a synthetic return addre
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
@@ 49,6 65,6 @@ The [encoder](src/core/Encoding.thy) proves inversion and byte bounds for immedi
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. The HolyC runner masks each result to four bits for the TempleOS palette
+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
M ROOT => ROOT +2 -0
@@ 16,7 16,9 @@ session Remy in src = Remybase +
theories
Allocation
Branches
+ Bounds
X86
Frontend
+ Delivery
Examples
Export
M cli/driver.ML => cli/driver.ML +3 -1
@@ 66,6 66,8 @@ 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] =>
@@ 74,7 76,7 @@ fun main () =
| ["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 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)")
+ | _ => 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 => cli/watch.py +151 -0
@@ 0,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()
M guest/Remy.HC => guest/Remy.HC +221 -13
@@ 18,19 18,171 @@ 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 Verify()
+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,"C:/%s.BIN",names[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,"C:/%s.DAT",names[i]);
+ 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++) {
@@ 48,22 200,38 @@ U0 Verify()
} 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)
{
- dc->color=BLUE;
- GrPrint(dc,80,24,"remy %s",names[selected]);
- dc->color=BLACK;
- GrBlot(dc,80,64,image);
- GrPrint(dc,80,416,"%s",program);
+ 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;
@@ 71,30 239,63 @@ U0 Release(Bool restore)
shader=NULL;
Free(program);
program=NULL;
+ Free(incoming);
+ incoming=NULL;
+ LBtr(&display_lock,0);
}
-U0 Show(I64 which=0)
+U0 Show(I64 which=0,Bool live=FALSE)
{
- I64 x,y,dy,t=0;
+ I64 x,y,dy,t=0,cpu=0,key;
U8 color,path[64];
Bool restore=FALSE;
if (!(0<=which<3)) return;
try {
selected=which;
- StrPrint(path,"C:/%s.BIN",names[which]);
+ live_mode=live;
+ StrPrint(path,"%s%s.BIN",directory,names[which]);
shader=FileRead(path);
if (!shader) throw('Code');
- StrPrint(path,"C:/%s.TXT",names[which]);
+ 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 (!ScanChar) {
+ 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;
@@ 107,8 308,15 @@ U0 Show(I64 which=0)
Sleep(20);
}
} catch {
+ PutExcept;
Release(restore);
+ return;
}
Release(restore);
DocClear;
}
+
+U0 Live(I64 which=0)
+{
+ Show(which,TRUE);
+}
A src/Bounds.thy => src/Bounds.thy +116 -0
@@ 0,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/Delivery.thy => src/Delivery.thy +41 -0
@@ 0,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
M src/Export.thy => src/Export.thy +2 -2
@@ 1,11 1,11 @@
theory Export
- imports Examples
+ 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 ascii ordinal in SML module_name Remy file_prefix remy
+export_code validate disassemble configured artifact baseline vectors reference simulate delivery ascii ordinal in SML module_name Remy file_prefix remy
end
M src/X86.thy => src/X86.thy +1 -1
@@ 1,5 1,5 @@
theory X86
- imports Branches
+ imports Bounds
begin
datatype micro = Imm64 pixel | Imm32 pixel | Copy register register | Save register | Restore register
A tests/guest.py => tests/guest.py +263 -0
@@ 0,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 => tests/live.py +172 -0
@@ 0,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()
M tests/native.py => tests/native.py +1 -1
@@ 178,7 178,7 @@ def main():
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, HOL reference checks and 11 rejection cases passed")
+ print(f"{len(cases)} programs, {comparisons} native comparisons, byte interpreter and HOL reference checks, 11 rejection cases passed")
if __name__ == "__main__":