From 76b7f307a15ad03540da2628a3e26ef75bbc1bef Mon Sep 17 00:00:00 2001 From: james Date: Sun, 1 Nov 2026 04:40:42 +0000 Subject: [PATCH] feat(live): validate and swap compiled shaders between guest frames --- Makefile | 6 +- README.md | 22 +++- ROOT | 2 + cli/driver.ML | 4 +- cli/watch.py | 151 +++++++++++++++++++++++++++ guest/Remy.HC | 234 ++++++++++++++++++++++++++++++++++++++--- src/Bounds.thy | 116 +++++++++++++++++++++ src/Delivery.thy | 41 ++++++++ src/Export.thy | 4 +- src/X86.thy | 2 +- tests/guest.py | 263 +++++++++++++++++++++++++++++++++++++++++++++++ tests/live.py | 172 +++++++++++++++++++++++++++++++ tests/native.py | 2 +- 13 files changed, 997 insertions(+), 22 deletions(-) create mode 100644 cli/watch.py create mode 100644 src/Bounds.thy create mode 100644 src/Delivery.thy create mode 100644 tests/guest.py create mode 100644 tests/live.py diff --git a/Makefile b/Makefile index 1e5c4a2fa286df67ab86e8419a1a9d31e9f7c310..084d02d5a981e784e15abf88c57e7c30ad99d2d3 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/README.md b/README.md index c515edd48286b13442473c0607d5e412ae01c633..d369f5230efd9ae6003b75fbec892375293d4b61 100644 --- a/README.md +++ b/README.md @@ -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 [![i like men](media/demo.gif)](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 diff --git a/ROOT b/ROOT index 92a76532e7c711e315e098c7e0f4e58c6f9bd4bf..e4a87d65c9b0a2a648766cbc5a2bd82362d126ad 100644 --- a/ROOT +++ b/ROOT @@ -16,7 +16,9 @@ session Remy in src = Remybase + theories Allocation Branches + Bounds X86 Frontend + Delivery Examples Export diff --git a/cli/driver.ML b/cli/driver.ML index e8be8fd5fa81ef57f04d6170741089525beff158..aa7d7de77c76da9fb6f7e2e5d474c1a86d0df5e6 100644 --- a/cli/driver.ML +++ b/cli/driver.ML @@ -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); diff --git a/cli/watch.py b/cli/watch.py new file mode 100644 index 0000000000000000000000000000000000000000..d96b511af684effd94dea5222186530bbcf71d53 --- /dev/null +++ b/cli/watch.py @@ -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() diff --git a/guest/Remy.HC b/guest/Remy.HC index 3a42bb28b2fa3ce8fa507b9405c74318aace6e22..cb81fd5da69089ed6516657eee5d7a51854420bd 100644 --- a/guest/Remy.HC +++ b/guest/Remy.HC @@ -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;i5) { + 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;jcolor=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); +} diff --git a/src/Bounds.thy b/src/Bounds.thy new file mode 100644 index 0000000000000000000000000000000000000000..0197245db1638883e2c4ee5e9ccbfa4875b264ea --- /dev/null +++ b/src/Bounds.thy @@ -0,0 +1,116 @@ +theory Bounds + imports Branches +begin + +fun guarded_run :: "nat \ opcode list \ machine \ bool" where + "guarded_run limit [] s = (length (stack s) \ limit)" +| "guarded_run limit (op # code) s = (length (stack s) \ limit \ + (case transition op s of None \ False | Some q \ guarded_run limit code q))" + +fun guarded_flow :: "nat \ flow \ machine \ 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 \ + (case flowrun a s of None \ False | Some q \ 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 \ 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 \ transition op s = Some q \ + 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 \ 512 \ audit code n = Some m \ m \ 512" + by (induction code arbitrary: n) (auto split: if_splits bind_splits) + +lemma flowaudit_limit: + "n \ 512 \ flowaudit code n = Some m \ m \ 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 \ 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 \ 512" "audit code n = Some m" + shows "\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 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 \ 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) \ 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 \ 512" "flowaudit code n = Some m" + shows "\q. flowrun code s = Some q \ length (stack q) = base + m \ + drop m (stack q) = drop n (stack s) \ inputs q = inputs s \ + 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 \ 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 \ \q. flowrun code s = Some q \ + stack q = stack s \ inputs q = inputs s \ + 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 diff --git a/src/Delivery.thy b/src/Delivery.thy new file mode 100644 index 0000000000000000000000000000000000000000..737ab545886d2e98aca1cf9d9ad112c6e0d7c781 --- /dev/null +++ b/src/Delivery.thy @@ -0,0 +1,41 @@ +theory Delivery + imports Frontend +begin + +definition checksum :: "nat list \ pixel" where + "checksum bytes = foldl (\h b. (h XOR word_of_nat b) * 1099511628211) 14695981039346656037 bytes" + +definition delivery :: "string \ string \ (bool \ string) \ string" where + "delivery sequence source = (case (number sequence,prepare source) of + (Some revision,Some e) \ + 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) \ revision < 2 ^ 32 \ 0 < revision \ + length code \ 65536 \ length source \ 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) \ ((False,[]),source_error source) + | _ \ ((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) \ + 16412 \ length packet \ length packet \ 147484" + by (auto simp: delivery_def Let_def split: option.splits if_splits; linarith) + +end diff --git a/src/Export.thy b/src/Export.thy index 4b69ac7e259821093b04659c8eb2ccb3131407ac..55ba750741701536270c731b354abea985f0ba75 100644 --- a/src/Export.thy +++ b/src/Export.thy @@ -1,11 +1,11 @@ theory Export - imports Examples + imports Examples Delivery begin definition ascii :: "integer \ char" where "ascii = char_of" definition ordinal :: "char \ 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 diff --git a/src/X86.thy b/src/X86.thy index 454f33e357f4cb0ff93cfd7708ea4af448e342fc..c533e965afef051b0ff709b0b31a4fba3ca7ab1c 100644 --- a/src/X86.thy +++ b/src/X86.thy @@ -1,5 +1,5 @@ theory X86 - imports Branches + imports Bounds begin datatype micro = Imm64 pixel | Imm32 pixel | Copy register register | Save register | Restore register diff --git a/tests/guest.py b/tests/guest.py new file mode 100644 index 0000000000000000000000000000000000000000..e4b4b4316d5f8e34ab4a532bdf3b74ac2db73959 --- /dev/null +++ b/tests/guest.py @@ -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('= 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('= bitmap*512*8: + raise ValueError('template allocation bitmap is too small') + struct.pack_into('I', data, sector*2048+84, len(data)//2048) + 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('= 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('