~james/remy

feat(compiler): add verified pixel compiler and templeos runner

commit
3ac5bae085495f49c3f24dbfb40242ee81069c4f browse tree
author
james <j@cpl0.zip>
signature
Verified ~james signed with a key registered by ~james
date
2026-08-31 11:00 UTC

21 files changed, +1217 −0

.gitignore added

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

Makefile added

@@ -0,0 +1,23 @@
1+ISABELLE ?= isabelle
2+
3+.PHONY: all check payload clean
4+
5+all: .build/ready
6+
7+.build/ready: ROOT $(wildcard src/*.thy) cli/driver.ML Makefile
8+ @test "$$('$(ISABELLE)' version)" = Isabelle2026
9+ "$(ISABELLE)" build -D . -j 1 -o threads=1 -o parallel_proofs=0
10+ "$(ISABELLE)" export -n -d . -O .build -x 'Remy.Export:code/remy.ML' Remy
11+ REMY_ROOT="$(CURDIR)" "$$('$(ISABELLE)' getenv -b POLYML_HOME)/$$('$(ISABELLE)' getenv -b ISABELLE_PLATFORM64)/polyc" -o .build/remy cli/driver.ML
12+ @touch $@
13+
14+check: all
15+ python3 tests/native.py
16+
17+payload: all
18+ @mkdir -p .build/payload
19+ @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
20+ cp guest/Remy.HC .build/payload/Remy.HC
21+
22+clean:
23+ rm -rf .build

README.md added

@@ -0,0 +1,36 @@
1+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
2+
3+[![i like men](media/demo.gif)](media/demo.mp4)
4+
5+## Build
6+
7+```sh
8+make check
9+make payload
10+```
11+
12+It uses:
13+- Isabelle2026 and its bundled Poly/ML toolchain
14+- Python
15+
16+Copy these files onto `C:/` in TempleOS and run:
17+
18+```c
19+#include "C:/Remy.HC";
20+Verify;
21+Show(0);
22+```
23+
24+## Correctness
25+
26+Each `let` pushes a binding onto the evaluation stack. [Compilation](src/Compiler.thy) adjusts variable offsets as intermediate values accumulate above those bindings and proves that execution leaves the result followed by the original stack whereas accepted programs stay within 512 evaluation words at every instruction boundary
27+
28+[Native lowering](src/Native.thy) puts the result in `rax` and preserves `r8`, `r9` and `rdx` which carry `x`, `y` and `t`. The temporary registers are `rax`, `rcx` and `rbx` while the [Encoding](src/Encoding.thy) proves decoder inversion and byte bounds for the emitted blocks including their immediate operands and stack displacements
29+
30+![Source eval](media/correspondence.svg)
31+
32+Arithmetic wraps modulo `2^64` and shifts mask their count to six bits
33+
34+Both branches of a nonconstant conditional run before selection which preserves the result because expressions have no side effects. The HolyC runner masks each pixel result to four bits for the TempleOS palette
35+
36+The execution theorem is relative to the instruction block model. Actual x86 execution + the HolyC calling bridge and the extracted runtime and the OS are outside its scope. Tests compare emitted code against an independent evaluator on Linux and against HOL results inside the recorded TempleOS guest

ROOT added

@@ -0,0 +1,18 @@
1+session Remybase = HOL +
2+ options [document = false]
3+ sessions "HOL-Library"
4+ theories
5+ "HOL-Library.Word"
6+ "HOL-Library.Code_Target_Numeral"
7+
8+session Remy in src = Remybase +
9+ options [document = false]
10+ sessions "HOL-Library"
11+ theories
12+ Model
13+ Compiler
14+ Native
15+ Encoding
16+ Frontend
17+ Examples
18+ Export

cli/driver.ML added

@@ -0,0 +1,40 @@
1+val root = valOf (OS.Process.getEnv "REMY_ROOT");
2+val _ = use (root ^ "/.build/Remy.Export/code/remy.ML");
3+
4+fun chars s = map (Remy.ascii o IntInf.fromInt o Char.ord) (String.explode s);
5+fun text cs = String.implode (map (Char.chr o IntInf.toInt o Remy.ordinal) cs);
6+
7+fun read path =
8+ let
9+ val stream = TextIO.openIn path
10+ val input = TextIO.inputN (stream, 65537)
11+ handle exn => (TextIO.closeIn stream; raise exn)
12+ val _ = TextIO.closeIn stream
13+ in
14+ if size input > 65536 then raise Fail "source exceeds 64 KiB" else chars input
15+ end;
16+
17+fun write path bytes =
18+ let
19+ val stream = BinIO.openOut path
20+ in
21+ (BinIO.output (stream, Byte.stringToBytes (text bytes)); BinIO.closeOut stream)
22+ handle exn => ((BinIO.closeOut stream handle _ => ()); raise exn)
23+ end;
24+
25+fun output (ok, message) =
26+ (TextIO.output (if ok then TextIO.stdOut else TextIO.stdErr, text message);
27+ if ok then () else OS.Process.exit OS.Process.failure);
28+
29+fun main () =
30+ (case CommandLine.arguments () of
31+ ["vectors", source, destination] =>
32+ (case Remy.vectors (read source) of (true, bytes) => write destination bytes | result => output result)
33+ | ["eval", source, x, y, t] => output (Remy.reference (read source) (chars x) (chars y) (chars t))
34+ | [source, destination] =>
35+ let val ((ok, bytes), report) = Remy.artifact (read source)
36+ in if ok then (write destination bytes; output (true,report)) else output (false,report) end
37+ | _ => raise Fail "usage: remy source binary | remy vectors source data | remy eval source x y t")
38+ handle exn =>
39+ (TextIO.output (TextIO.stdErr, "remy: " ^ General.exnMessage exn ^ "\n");
40+ OS.Process.exit OS.Process.failure);

examples/Cells.remy added

@@ -0,0 +1,5 @@
1+(let u (+ x (shr t 2))
2+ (let cell (xor (shr u 4) (shr y 4))
3+ (if (< (and cell 3) 1)
4+ (and (+ (xor u y) t) 15)
5+ (and (shr (+ (* u u) (* y y)) 7) 15))))

examples/Rings.remy added

@@ -0,0 +1,4 @@
1+(let dx (- x 80)
2+ (let dy (- y 56)
3+ (let radius (+ (* dx dx) (* dy dy))
4+ (and (shr (+ radius (* t 32)) 6) 15))))

examples/Weave.remy added

@@ -0,0 +1,3 @@
1+(let drift (+ y (shr t 1))
2+ (let warp (xor (* x drift) (* (+ x t) y))
3+ (and (xor (shr warp 5) (shr (+ x drift) 3)) 15)))

guest/Remy.HC added

@@ -0,0 +1,93 @@
1+asm {
2+_REMY::
3+ PUSH RBP
4+ MOV RBP,RSP
5+ MOV RAX,U64 SF_ARG1[RBP]
6+ MOV R8,U64 SF_ARG2[RBP]
7+ MOV R9,U64 SF_ARG3[RBP]
8+ MOV RDX,U64 SF_ARG4[RBP]
9+ CALL RAX
10+ POP RBP
11+ RET1 32
12+}
13+
14+_extern _REMY U64 Pixel(U8 *code,U64 x,U64 y,U64 t);
15+
16+U8 *names[3]={"Rings","Weave","Cells"};
17+CDC *image=NULL;
18+U8 *shader=NULL;
19+U8 *program=NULL;
20+I64 selected;
21+
22+U0 Verify()
23+{
24+ I64 i,j,size,total=0;
25+ U8 *code,path[64];
26+ U64 *rows;
27+ for (i=0;i<3;i++) {
28+ StrPrint(path,"C:/%s.BIN",names[i]);
29+ code=FileRead(path,&size);
30+ if (!code) throw('Code');
31+ "%-6s %d bytes ",names[i],size;
32+ StrPrint(path,"C:/%s.DAT",names[i]);
33+ rows=FileRead(path,&size);
34+ if (!rows || size!=16384) throw('Vectors');
35+ for (j=0;j<size/32;j++) {
36+ if (Pixel(code,rows[4*j],rows[4*j+1],rows[4*j+2])!=rows[4*j+3]) {
37+ throw('Mismatch');
38+ }
39+ total++;
40+ }
41+ "%d comparisons passed\n",size/32;
42+ Free(rows);
43+ Free(code);
44+ }
45+ "native results match HOL evaluation (%d cases)\n",total;
46+}
47+
48+U0 Draw(CTask *,CDC *dc)
49+{
50+ dc->color=BLUE;
51+ GrPrint(dc,80,24,"remy %s",names[selected]);
52+ dc->color=BLACK;
53+ GrBlot(dc,80,64,image);
54+ GrPrint(dc,80,416,"%s",program);
55+}
56+
57+U0 Show(I64 which=0)
58+{
59+ I64 x,y,dy,t=0;
60+ U8 color,path[64];
61+ if (!(0<=which<3)) return;
62+ selected=which;
63+ StrPrint(path,"C:/%s.BIN",names[which]);
64+ shader=FileRead(path);
65+ if (!shader) throw('Code');
66+ StrPrint(path,"C:/%s.TXT",names[which]);
67+ program=FileRead(path);
68+ if (!program) throw('Source');
69+ image=DCNew(480,336);
70+ SettingsPush;
71+ AutoComplete(OFF);
72+ WinMax;
73+ DocClear;
74+ Fs->draw_it=&Draw;
75+ while (!ScanChar) {
76+ for (y=0;y<112;y++) {
77+ for (x=0;x<160;x++) {
78+ color=Pixel(shader,x,y,t)&15;
79+ for (dy=0;dy<3;dy++)
80+ MemSet(image->body+(3*y+dy)*480+3*x,color,3);
81+ }
82+ }
83+ t+=2;
84+ Refresh;
85+ Sleep(20);
86+ }
87+ Fs->draw_it=NULL;
88+ SettingsPop;
89+ DCDel(image);
90+ Free(shader);
91+ Free(program);
92+ DocClear;
93+}

media/correspondence.svg added

@@ -0,0 +1,17 @@
1+<svg xmlns="http://www.w3.org/2000/svg" width="720" height="208" viewBox="0 0 720 208">
2+ <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>
3+ <rect width="720" height="208" fill="white"/>
4+ <g fill="none" stroke="#555" stroke-width="1.5" marker-end="url(#arrow)">
5+ <path d="M 176 45 H 547"/><path d="M 140 64 V 143"/><path d="M 582 64 V 143"/><path d="M 176 164 H 547"/>
6+ </g>
7+ <g fill="white" stroke="#555">
8+ <rect x="62" y="25" width="114" height="40" rx="3"/><rect x="547" y="25" width="113" height="40" rx="3"/>
9+ <rect x="38" y="144" width="138" height="40" rx="3"/><rect x="547" y="144" width="138" height="40" rx="3"/>
10+ </g>
11+ <g font-family="monospace" font-size="14" fill="#222" text-anchor="middle">
12+ <text x="119" y="50">expression</text><text x="603" y="50">64-bit value</text>
13+ <text x="107" y="169">x86 blocks</text><text x="616" y="169">RAX + stack</text>
14+ <text x="360" y="35">source evaluation</text><text x="360" y="153">native block execution</text>
15+ <text x="360" y="106">optimisation + lexical slots + encoding</text>
16+ </g>
17+</svg>

media/demo.gif added

Binary file.

media/demo.mp4 added

Binary file.

media/poster.png added

Binary file.

src/Compiler.thy added

@@ -0,0 +1,237 @@
1+theory Compiler
2+ imports Model
3+begin
4+
5+datatype instruction = Constant pixel | Fetch input | Pick nat | Calculate operator | Choose | Slide
6+
7+fun step :: "(input \<Rightarrow> pixel) \<Rightarrow> instruction \<Rightarrow> pixel list \<Rightarrow> pixel list option" where
8+ "step inputs (Constant v) s = Some (v # s)"
9+| "step inputs (Fetch i) s = Some (inputs i # s)"
10+| "step inputs (Pick i) s = (if i < length s then Some (s ! i # s) else None)"
11+| "step inputs (Calculate op) (b # a # s) = Some (operate op a b # s)"
12+| "step inputs Choose (b # a # c # s) = Some ((if c = 0 then b else a) # s)"
13+| "step inputs Slide (b # a # s) = Some (b # s)"
14+| "step inputs _ _ = None"
15+
16+fun execute :: "(input \<Rightarrow> pixel) \<Rightarrow> instruction list \<Rightarrow> pixel list \<Rightarrow> pixel list option" where
17+ "execute inputs [] s = Some s"
18+| "execute inputs (i # code) s = (case step inputs i s of None \<Rightarrow> None | Some t \<Rightarrow> execute inputs code t)"
19+
20+lemma execute_append:
21+ "execute inputs (a @ b) s = Option.bind (execute inputs a s) (execute inputs b)"
22+ by (induction a arbitrary: s) (auto split: option.splits bind_splits)
23+
24+fun compile :: "expression \<Rightarrow> nat list \<Rightarrow> instruction list" where
25+ "compile (Literal v) slots = [Constant v]"
26+| "compile (Input i) slots = [Fetch i]"
27+| "compile (Variable i) slots = [Pick (slots ! i)]"
28+| "compile (Binary op a b) slots = compile a slots @ compile b (map Suc slots) @ [Calculate op]"
29+| "compile (Cond c a b) slots = compile c slots @ compile a (map Suc slots) @
30+ compile b (map (\<lambda>i. Suc (Suc i)) slots) @ [Choose]"
31+| "compile (Let a b) slots = compile a slots @ compile b (0 # map Suc slots) @ [Slide]"
32+
33+definition represents :: "nat list \<Rightarrow> pixel list \<Rightarrow> pixel list \<Rightarrow> bool" where
34+ "represents slots s env \<longleftrightarrow> length slots = length env \<and>
35+ (\<forall>i < length env. slots ! i < length s \<and> s ! (slots ! i) = env ! i)"
36+
37+lemma represents_push:
38+ "represents slots s env \<Longrightarrow> represents (map Suc slots) (v # s) env"
39+ by (auto simp: represents_def)
40+
41+lemma represents_push_two:
42+ "represents slots s env \<Longrightarrow> represents (map (\<lambda>i. Suc (Suc i)) slots) (a # b # s) env"
43+ by (auto simp: represents_def)
44+
45+lemma represents_bind:
46+ "represents slots s env \<Longrightarrow> represents (0 # map Suc slots) (v # s) (v # env)"
47+ by (auto simp: represents_def nth_Cons split: nat.splits)
48+
49+theorem compile_correct:
50+ assumes "scoped (length env) e" "represents slots s env"
51+ shows "execute inputs (compile e slots) s = Some (evaluate e env inputs # s)"
52+ using assms
53+proof (induction e arbitrary: slots s env)
54+ case (Literal v)
55+ then show ?case by simp
56+next
57+ case (Input i)
58+ then show ?case by simp
59+next
60+ case (Variable i)
61+ then show ?case by (simp add: represents_def)
62+next
63+ case (Binary op a b)
64+ have a: "execute inputs (compile a slots) s = Some (evaluate a env inputs # s)"
65+ using Binary.IH(1) Binary.prems by simp
66+ have b: "execute inputs (compile b (map Suc slots)) (evaluate a env inputs # s) =
67+ Some (evaluate b env inputs # evaluate a env inputs # s)"
68+ using Binary.IH(2) Binary.prems represents_push by simp
69+ show ?case by (simp add: execute_append a b)
70+next
71+ case (Cond c a b)
72+ have c: "execute inputs (compile c slots) s = Some (evaluate c env inputs # s)"
73+ using Cond.IH(1) Cond.prems by simp
74+ have a: "execute inputs (compile a (map Suc slots)) (evaluate c env inputs # s) =
75+ Some (evaluate a env inputs # evaluate c env inputs # s)"
76+ using Cond.IH(2) Cond.prems represents_push by simp
77+ have b: "execute inputs (compile b (map (\<lambda>i. Suc (Suc i)) slots))
78+ (evaluate a env inputs # evaluate c env inputs # s) =
79+ Some (evaluate b env inputs # evaluate a env inputs # evaluate c env inputs # s)"
80+ using Cond.IH(3) Cond.prems represents_push_two by simp
81+ show ?case by (simp add: execute_append c a b)
82+next
83+ case (Let a b)
84+ have a: "execute inputs (compile a slots) s = Some (evaluate a env inputs # s)"
85+ using Let.IH(1) Let.prems by simp
86+ have b: "execute inputs (compile b (0 # map Suc slots)) (evaluate a env inputs # s) =
87+ Some (evaluate b (evaluate a env inputs # env) inputs # evaluate a env inputs # s)"
88+ using Let.IH(2) Let.prems represents_bind by simp
89+ show ?case by (simp add: execute_append a b)
90+qed
91+
92+corollary compile_closed:
93+ "scoped 0 e \<Longrightarrow> execute inputs (compile (optimise e) []) [] = Some [evaluate e [] inputs]"
94+ using compile_correct[where e="optimise e" and env="[]" and slots="[]" and s="[]" and inputs=inputs]
95+ by (simp add: represents_def optimise_correct optimise_scoped)
96+
97+fun height :: "instruction \<Rightarrow> nat \<Rightarrow> nat option" where
98+ "height (Constant v) n = Some (Suc n)"
99+| "height (Fetch i) n = Some (Suc n)"
100+| "height (Pick i) n = (if i < n then Some (Suc n) else None)"
101+| "height (Calculate op) n = (if 2 \<le> n then Some (n - 1) else None)"
102+| "height Choose n = (if 3 \<le> n then Some (n - 2) else None)"
103+| "height Slide n = (if 2 \<le> n then Some (n - 1) else None)"
104+
105+fun check :: "instruction list \<Rightarrow> nat \<Rightarrow> nat option" where
106+ "check [] n = Some n"
107+| "check (i # code) n = Option.bind (height i n) (check code)"
108+
109+lemma check_append:
110+ "check (a @ b) n = Option.bind (check a n) (check b)"
111+ by (induction a arbitrary: n) (auto split: option.splits bind_splits)
112+
113+lemma step_height:
114+ "height i (length s) = Some n \<Longrightarrow> \<exists>t. step inputs i s = Some t \<and> length t = n"
115+ by (cases i; cases s; simp; rename_tac a xs; case_tac xs; simp;
116+ rename_tac b ys; case_tac ys; auto split: if_splits)
117+
118+theorem check_sound:
119+ "check code (length s) = Some n \<Longrightarrow> \<exists>t. execute inputs code s = Some t \<and> length t = n"
120+proof (induction code arbitrary: s)
121+ case Nil
122+ then show ?case by simp
123+next
124+ case (Cons i code)
125+ then obtain m where h: "height i (length s) = Some m" and c: "check code m = Some n"
126+ by (auto simp: bind_eq_Some_conv)
127+ obtain t where step: "step inputs i s = Some t" and len: "length t = m"
128+ using step_height[OF h] by blast
129+ obtain u where run: "execute inputs code t = Some u" and "length u = n"
130+ using Cons.IH c len by blast
131+ then show ?case using step by simp
132+qed
133+
134+fun demand :: "expression \<Rightarrow> nat" where
135+ "demand (Binary op a b) = max (demand a) (Suc (demand b))"
136+| "demand (Cond c a b) = max (demand c) (max (Suc (demand a)) (2 + demand b))"
137+| "demand (Let a b) = max (demand a) (Suc (demand b))"
138+| "demand _ = 1"
139+
140+lemma demand_positive: "0 < demand e"
141+ by (induction e) auto
142+
143+fun bounded :: "nat \<Rightarrow> instruction list \<Rightarrow> nat \<Rightarrow> bool" where
144+ "bounded limit [] n = (n \<le> limit)"
145+| "bounded limit (i # code) n = (n \<le> limit \<and> (case height i n of None \<Rightarrow> False | Some m \<Rightarrow> bounded limit code m))"
146+
147+lemma bounded_start: "bounded limit code n \<Longrightarrow> n \<le> limit"
148+ by (cases code) auto
149+
150+lemma bounded_append:
151+ "bounded limit (a @ b) n \<longleftrightarrow> bounded limit a n \<and> (\<exists>m. check a n = Some m \<and> bounded limit b m)"
152+ by (induction a arbitrary: n) (auto dest: bounded_start split: option.splits bind_splits)
153+
154+lemma bounded_check:
155+ "bounded limit code n \<Longrightarrow> \<exists>m. check code n = Some m \<and> m \<le> limit"
156+ by (induction code arbitrary: n) (auto split: option.splits bind_splits)
157+
158+theorem compiled_height:
159+ "scoped (length slots) e \<Longrightarrow> list_all (\<lambda>i. i < n) slots \<Longrightarrow>
160+ check (compile e slots) n = Some (Suc n)"
161+proof (induction e arbitrary: slots n)
162+ case (Literal v)
163+ then show ?case by simp
164+next
165+ case (Input i)
166+ then show ?case by simp
167+next
168+ case (Variable i)
169+ then show ?case by (simp add: list_all_length)
170+next
171+ case (Binary op a b)
172+ then show ?case
173+ by (simp add: check_append list_all_iff)
174+next
175+ case (Cond c a b)
176+ then show ?case by (simp add: check_append list_all_iff)
177+next
178+ case (Let a b)
179+ then show ?case by (simp add: check_append list_all_iff)
180+qed
181+
182+fun snapshots :: "(input \<Rightarrow> pixel) \<Rightarrow> instruction list \<Rightarrow> pixel list \<Rightarrow> (pixel list list) option" where
183+ "snapshots inputs [] s = Some [s]"
184+| "snapshots inputs (i # code) s = Option.bind (step inputs i s)
185+ (\<lambda>t. map_option ((#) s) (snapshots inputs code t))"
186+
187+lemma snapshots_nonempty:
188+ "snapshots inputs code s = Some frames \<Longrightarrow> frames \<noteq> []"
189+ by (cases code) (auto split: bind_splits option.splits)
190+
191+theorem snapshots_execute:
192+ "snapshots inputs code s = Some frames \<Longrightarrow> execute inputs code s = Some (last frames)"
193+proof (induction code arbitrary: s frames)
194+ case Nil
195+ then show ?case by auto
196+next
197+ case (Cons i code)
198+ then obtain t rest where step: "step inputs i s = Some t"
199+ and tail: "snapshots inputs code t = Some rest" and frames: "frames = s # rest"
200+ by (auto split: bind_splits option.splits)
201+ have "rest \<noteq> []" using snapshots_nonempty[OF tail] .
202+ then show ?case using Cons.IH[OF tail] step frames by simp
203+qed
204+
205+theorem bounded_execution:
206+ "bounded limit code (length s) \<Longrightarrow>
207+ \<exists>frames. snapshots inputs code s = Some frames \<and> list_all (\<lambda>t. length t \<le> limit) frames"
208+proof (induction code arbitrary: s)
209+ case Nil
210+ then show ?case by simp
211+next
212+ case (Cons i code)
213+ then obtain m where bound: "length s \<le> limit" and h: "height i (length s) = Some m"
214+ and tail: "bounded limit code m"
215+ by (auto split: option.splits)
216+ obtain t where step: "step inputs i s = Some t" and len: "length t = m"
217+ using step_height[OF h] by blast
218+ obtain frames where trace: "snapshots inputs code t = Some frames"
219+ and safe: "list_all (\<lambda>t. length t \<le> limit) frames"
220+ using Cons.IH tail len by blast
221+ show ?case using step trace safe bound by auto
222+qed
223+
224+corollary bounded_result:
225+ "bounded limit code (length s) \<Longrightarrow>
226+ \<exists>t. execute inputs code s = Some t \<and> length t \<le> limit"
227+proof -
228+ assume bound: "bounded limit code (length s)"
229+ obtain frames where trace: "snapshots inputs code s = Some frames"
230+ and safe: "list_all (\<lambda>t. length t \<le> limit) frames"
231+ using bounded_execution[OF bound] by blast
232+ have "frames \<noteq> []" using snapshots_nonempty[OF trace] .
233+ then have "length (last frames) \<le> limit" using safe by (simp add: list_all_iff)
234+ then show ?thesis using snapshots_execute[OF trace] by blast
235+qed
236+
237+end

src/Encoding.thy added

@@ -0,0 +1,158 @@
1+theory Encoding
2+ imports Native
3+begin
4+
5+fun octets :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
6+ "octets 0 n = []"
7+| "octets (Suc k) n = n mod 256 # octets k (n div 256)"
8+
9+fun integer :: "nat list \<Rightarrow> nat" where
10+ "integer [] = 0"
11+| "integer (b # bs) = b + 256 * integer bs"
12+
13+lemma octets_length [simp]: "length (octets k n) = k"
14+ by (induction k arbitrary: n) auto
15+
16+lemma octets_bytes: "set (octets k n) \<subseteq> {..<256}"
17+ by (induction k arbitrary: n) auto
18+
19+lemma integer_octets: "integer (octets k n) = n mod 256 ^ k"
20+ by (induction k arbitrary: n) (simp_all add: power_Suc mod_mult2_eq add.commute)
21+
22+lemma literal_bound: "unat (v :: pixel) < 256 ^ 8"
23+ using unsigned_less[of v, where ?'a=nat] by simp
24+
25+lemma integer_literal [simp]: "word_of_nat (integer (octets 8 (unat v))) = (v :: pixel)"
26+ using literal_bound[of v] by (simp add: integer_octets)
27+
28+fun pushcode :: "register \<Rightarrow> nat list" where
29+ "pushcode Rax = [80]"
30+| "pushcode Rcx = [81]"
31+| "pushcode Rbx = [83]"
32+| "pushcode Rdx = [82]"
33+| "pushcode R8 = [65,80]"
34+| "pushcode R9 = [65,81]"
35+
36+fun popcode :: "register \<Rightarrow> nat list" where
37+ "popcode Rax = [88]"
38+| "popcode Rcx = [89]"
39+| "popcode Rbx = [91]"
40+| "popcode Rdx = [90]"
41+| "popcode R8 = [65,88]"
42+| "popcode R9 = [65,89]"
43+
44+fun arithmetic :: "operator \<Rightarrow> nat list" where
45+ "arithmetic Add = [72,1,200]"
46+| "arithmetic Sub = [72,145,72,41,200]"
47+| "arithmetic Mul = [72,15,175,193]"
48+| "arithmetic And = [72,33,200]"
49+| "arithmetic Or = [72,9,200]"
50+| "arithmetic Xor = [72,49,200]"
51+| "arithmetic Shl = [72,145,72,211,224]"
52+| "arithmetic Shr = [72,145,72,211,232]"
53+| "arithmetic Less = [72,145,72,57,200,15,146,192,72,15,182,192]"
54+
55+fun encode :: "opcode \<Rightarrow> nat list" where
56+ "encode (Immediate v) = [72,184] @ octets 8 (unat v)"
57+| "encode (Push r) = pushcode r"
58+| "encode (Pop r) = popcode r"
59+| "encode (Peek i) = [72,139,132,36] @ octets 4 (8 * i)"
60+| "encode (Arithmetic op) = arithmetic op"
61+| "encode Conditional = [72,133,219,72,15,69,193]"
62+
63+fun encodable :: "opcode \<Rightarrow> bool" where
64+ "encodable (Peek i) = (i < 2 ^ 28)"
65+| "encodable _ = True"
66+
67+definition fixed :: "opcode list" where
68+ "fixed = map Push [Rax,Rcx,Rbx,Rdx,R8,R9] @ map Pop [Rax,Rcx,Rbx,Rdx,R8,R9] @
69+ map Arithmetic [Add,Sub,Mul,And,Or,Xor,Shl,Shr,Less] @ [Conditional]"
70+
71+definition decode :: "nat list \<Rightarrow> (opcode \<times> nat list) option" where
72+ "decode bs = (if take 2 bs = [72,184] then
73+ if 10 \<le> length bs \<and> list_all (\<lambda>b. b < 256) (take 8 (drop 2 bs)) then
74+ Some (Immediate (word_of_nat (integer (take 8 (drop 2 bs)))), drop 10 bs) else None
75+ else if take 4 bs = [72,139,132,36] then
76+ let n = integer (take 4 (drop 4 bs)) in
77+ if 8 \<le> length bs \<and> list_all (\<lambda>b. b < 256) (take 4 (drop 4 bs)) \<and>
78+ n mod 8 = 0 \<and> n div 8 < 2 ^ 28 then Some (Peek (n div 8), drop 8 bs) else None
79+ else map_option (\<lambda>op. (op, drop (length (encode op)) bs))
80+ (List.find (\<lambda>op. take (length (encode op)) bs = encode op) fixed))"
81+
82+lemma octets_all [simp]: "list_all (\<lambda>b. b < 256) (octets k n)"
83+ using octets_bytes[of k n] by (auto simp: list_all_iff)
84+
85+lemma peek_bound:
86+ "(i :: nat) < 2 ^ 28 \<Longrightarrow> 8 * i < 256 ^ 4"
87+ by (simp; linarith)
88+
89+theorem decode_encode:
90+ assumes valid: "encodable op"
91+ shows "decode (encode op @ tail) = Some (op, tail)"
92+proof (cases op)
93+ case (Immediate v)
94+ then show ?thesis
95+ by (simp add: decode_def take_add integer_literal)
96+next
97+ case (Push r)
98+ then show ?thesis by (cases r) (simp_all add: decode_def fixed_def)
99+next
100+ case (Pop r)
101+ then show ?thesis by (cases r) (simp_all add: decode_def fixed_def)
102+next
103+ case (Peek i)
104+ have small: "i < 2 ^ 28" using valid Peek by simp
105+ have bound: "8 * i < 4294967296" using peek_bound[OF small] by simp
106+ show ?thesis using Peek small bound
107+ by (simp add: decode_def integer_octets Let_def)
108+next
109+ case (Arithmetic op)
110+ then show ?thesis by (cases op) (simp_all add: decode_def fixed_def)
111+next
112+ case Conditional
113+ then show ?thesis by (simp add: decode_def fixed_def)
114+qed
115+
116+theorem encode_bytes: "set (encode op) \<subseteq> {..<256}"
117+proof (cases op)
118+ case (Immediate v)
119+ then show ?thesis using octets_bytes by auto
120+next
121+ case (Push r)
122+ then show ?thesis by (cases r) auto
123+next
124+ case (Pop r)
125+ then show ?thesis by (cases r) auto
126+next
127+ case (Peek i)
128+ then show ?thesis using octets_bytes by auto
129+next
130+ case (Arithmetic op)
131+ then show ?thesis by (cases op) auto
132+next
133+ case Conditional
134+ then show ?thesis by simp
135+qed
136+
137+theorem encode_injective:
138+ "encodable a \<Longrightarrow> encodable b \<Longrightarrow> encode a = encode b \<longleftrightarrow> a = b"
139+ using decode_encode[of a "[]"] decode_encode[of b "[]"]
140+ by (metis append_Nil option.inject prod.inject)
141+
142+fun recover :: "nat \<Rightarrow> nat list \<Rightarrow> (opcode list \<times> nat list) option" where
143+ "recover 0 bs = Some ([],bs)"
144+| "recover (Suc n) bs = Option.bind (decode bs) (\<lambda>(op,tail).
145+ map_option (\<lambda>(ops,rest). (op # ops,rest)) (recover n tail))"
146+
147+theorem recover_encode:
148+ "list_all encodable ops \<Longrightarrow>
149+ recover (length ops) (concat (map encode ops) @ tail) = Some (ops,tail)"
150+ by (induction ops) (simp_all add: decode_encode)
151+
152+definition executable :: "expression \<Rightarrow> nat list" where
153+ "executable e = concat (map encode (native (compile (optimise e) []))) @ [88,195]"
154+
155+theorem executable_bytes: "set (executable e) \<subseteq> {..<256}"
156+ unfolding executable_def using encode_bytes by auto
157+
158+end

src/Examples.thy added

@@ -0,0 +1,71 @@
1+theory Examples
2+ imports Frontend
3+begin
4+
5+lemma overflow: "operate Add (-1) 1 = 0"
6+ by eval
7+
8+lemma multiply_overflow: "operate Mul (2 ^ 63) 2 = 0"
9+ by eval
10+
11+lemma shift_mask: "operate Shl 7 64 = 7"
12+ by eval
13+
14+lemma shift_wrap: "operate Shl 7 65 = 14"
15+ by eval
16+
17+lemma logical_shift: "operate Shr (-1) 63 = 1"
18+ by eval
19+
20+lemma unsigned_comparison: "operate Less (-1) 1 = 0"
21+ by eval
22+
23+lemma unsigned_high_bit: "operate Less 1 (2 ^ 63) = 1"
24+ by eval
25+
26+lemma constant_fold:
27+ "optimise (Binary Add (Literal (-1)) (Literal 1)) = Literal 0"
28+ by eval
29+
30+lemma dead_branch:
31+ "optimise (Cond (Literal 0) (Input X) (Input Y)) = Input Y"
32+ by eval
33+
34+lemma literal_code:
35+ "executable (Literal 42) = [72,184,42,0,0,0,0,0,0,0,80,88,195]"
36+ by eval
37+
38+lemma opcode_roundtrip:
39+ "decode [72,145,72,211,232,195] = Some (Arithmetic Shr,[195])"
40+ by eval
41+
42+lemma truncated_literal: "decode [72,184,0,0] = None"
43+ by eval
44+
45+lemma unaligned_slot: "decode [72,139,132,36,1,0,0,0] = None"
46+ by eval
47+
48+lemma negative_slot: "decode [72,139,132,36,0,0,0,128] = None"
49+ by eval
50+
51+lemma lexical_shadow:
52+ "reference ''(let x 7 (let x (+ x 2) (* x x)))'' ''1'' ''2'' ''3'' = (True,''81'' @ newline)"
53+ by eval
54+
55+lemma nested_temporaries:
56+ "reference ''(+ 10 (let a 3 (+ a (let b 4 (* a b)))))'' ''0'' ''0'' ''0'' = (True,''25'' @ newline)"
57+ by eval
58+
59+lemma unbound_rejected: "prepare ''(let a 3 b)'' = None"
60+ by eval
61+
62+lemma trailing_rejected: "prepare ''(+ x y) 1'' = None"
63+ by eval
64+
65+lemma literal_overflow_rejected: "prepare ''18446744073709551616'' = None"
66+ by eval
67+
68+lemma incomplete_rejected: "prepare ''(if x y)'' = None"
69+ by eval
70+
71+end

src/Export.thy added

@@ -0,0 +1,11 @@
1+theory Export
2+ imports Examples
3+begin
4+
5+definition ascii :: "integer \<Rightarrow> char" where "ascii = char_of"
6+
7+definition ordinal :: "char \<Rightarrow> integer" where "ordinal = of_char"
8+
9+export_code artifact vectors reference ascii ordinal in SML module_name Remy file_prefix remy
10+
11+end

src/Frontend.thy added

@@ -0,0 +1,137 @@
1+theory Frontend
2+ imports Encoding
3+begin
4+
5+fun finish :: "string \<Rightarrow> string list \<Rightarrow> string list" where
6+ "finish [] out = out"
7+| "finish word out = rev word # out"
8+
9+fun lex :: "string \<Rightarrow> string \<Rightarrow> string list \<Rightarrow> string list" where
10+ "lex [] word out = rev (finish word out)"
11+| "lex (c # cs) word out = (if c = CHR '' '' \<or> c = CHR 0x09 \<or> c = CHR 0x0A \<or> c = CHR 0x0D
12+ then lex cs [] (finish word out)
13+ else if c = CHR ''('' \<or> c = CHR '')'' then lex cs [] ([c] # finish word out)
14+ else lex cs (c # word) out)"
15+
16+definition number :: "string \<Rightarrow> nat option" where
17+ "number s = (if s = [] \<or> \<not> list_all (\<lambda>c. 48 \<le> nat_of_char c \<and> nat_of_char c < 58) s
18+ then None else let n = foldl (\<lambda>n c. min (2 ^ 64) (10 * n + nat_of_char c - 48)) 0 s in
19+ if n < 2 ^ 64 then Some n else None)"
20+
21+definition valid_name :: "string \<Rightarrow> bool" where
22+ "valid_name s = (s \<noteq> [] \<and> list_all (\<lambda>c. (97 \<le> nat_of_char c \<and> nat_of_char c \<le> 122)) s
23+ \<and> s \<noteq> ''let'' \<and> s \<noteq> ''if'')"
24+
25+fun lookup :: "string \<Rightarrow> string list \<Rightarrow> nat option" where
26+ "lookup name [] = None"
27+| "lookup name (x # xs) = (if name = x then Some 0 else map_option Suc (lookup name xs))"
28+
29+fun operator :: "string \<Rightarrow> operator option" where
30+ "operator s = (if s = ''+'' then Some Add else if s = ''-'' then Some Sub else if s = ''*'' then Some Mul
31+ else if s = ''and'' then Some And else if s = ''or'' then Some Or else if s = ''xor'' then Some Xor
32+ else if s = ''shl'' then Some Shl else if s = ''shr'' then Some Shr else if s = ''<'' then Some Less else None)"
33+
34+definition atom :: "string list \<Rightarrow> string \<Rightarrow> expression option" where
35+ "atom names s = (case lookup s names of Some i \<Rightarrow> Some (Variable i) | None \<Rightarrow>
36+ if s = ''x'' then Some (Input X) else if s = ''y'' then Some (Input Y) else if s = ''t'' then Some (Input T)
37+ else map_option (Literal \<circ> word_of_nat) (number s))"
38+
39+fun close :: "expression \<Rightarrow> string list \<Rightarrow> (expression \<times> string list) option" where
40+ "close e (s # rest) = (if s = '')'' then Some (e,rest) else None)"
41+| "close e [] = None"
42+
43+function parse :: "nat \<Rightarrow> string list \<Rightarrow> string list \<Rightarrow> (expression \<times> string list) option" where
44+ "parse fuel names tokens = (if fuel = 0 then None else case tokens of [] \<Rightarrow> None | s # rest \<Rightarrow>
45+ if s \<noteq> ''('' then map_option (\<lambda>e. (e,rest)) (atom names s)
46+ else case rest of [] \<Rightarrow> None | op # args \<Rightarrow>
47+ if op = ''let'' then (case args of [] \<Rightarrow> None | name # body \<Rightarrow>
48+ if \<not> valid_name name then None else
49+ Option.bind (parse (fuel - 1) names body) (\<lambda>(a,tail).
50+ Option.bind (parse (fuel - 1) (name # names) tail) (\<lambda>(b,tail). close (Let a b) tail)))
51+ else if op = ''if'' then
52+ Option.bind (parse (fuel - 1) names args) (\<lambda>(c,tail).
53+ Option.bind (parse (fuel - 1) names tail) (\<lambda>(a,tail).
54+ Option.bind (parse (fuel - 1) names tail) (\<lambda>(b,tail). close (Cond c a b) tail)))
55+ else Option.bind (operator op) (\<lambda>f.
56+ Option.bind (parse (fuel - 1) names args) (\<lambda>(a,tail).
57+ Option.bind (parse (fuel - 1) names tail) (\<lambda>(b,tail). close (Binary f a b) tail))))"
58+ by pat_completeness auto
59+termination by (relation "measure (\<lambda>(fuel,names,tokens). fuel)") auto
60+
61+definition prepare :: "string \<Rightarrow> expression option" where
62+ "prepare s = (if \<not> list_all (\<lambda>c. nat_of_char c < 128) s then None else
63+ Option.bind (parse 128 [] (lex s [] [])) (\<lambda>(e,rest).
64+ if rest = [] \<and> scoped 0 e \<and> nodes e \<le> 4096 then
65+ let code = compile (optimise e) [] in
66+ if check code 0 = Some 1 \<and> bounded 512 code 0 \<and> list_all encodable (native code)
67+ then Some e else None else None))"
68+
69+lemma prepare_scoped: "prepare s = Some e \<Longrightarrow> scoped 0 e"
70+ by (auto simp: prepare_def Let_def split: if_splits bind_splits prod.splits)
71+
72+lemma prepare_bounded:
73+ "prepare s = Some e \<Longrightarrow> bounded 512 (compile (optimise e) []) 0"
74+ by (auto simp: prepare_def Let_def split: if_splits bind_splits prod.splits)
75+
76+lemma prepare_encodable:
77+ "prepare s = Some e \<Longrightarrow> list_all encodable (native (compile (optimise e) []))"
78+ by (auto simp: prepare_def Let_def split: if_splits bind_splits prod.splits)
79+
80+theorem prepared_correct:
81+ "prepare source = Some e \<Longrightarrow>
82+ execute values (compile (optimise e) []) [] = Some [evaluate e [] values]"
83+ using compile_closed prepare_scoped by blast
84+
85+theorem prepared_native:
86+ "prepare source = Some e \<Longrightarrow>
87+ map_option observe (run (native (compile (optimise e) [])) s) =
88+ Some (inputs s, evaluate e [] (inputs s) # stack s)"
89+ using native_expression prepare_scoped by blast
90+
91+theorem prepared_bytes:
92+ "prepare source = Some e \<Longrightarrow>
93+ recover (length (native (compile (optimise e) []))) (executable e) =
94+ Some (native (compile (optimise e) []), [88,195])"
95+ unfolding executable_def using recover_encode prepare_encodable by blast
96+
97+theorem prepared_stacks:
98+ "prepare source = Some e \<Longrightarrow>
99+ \<exists>frames. snapshots values (compile (optimise e) []) [] = Some frames \<and>
100+ list_all (\<lambda>s. length s \<le> 512) frames"
101+ using bounded_execution[where s="[]" and limit=512] prepare_bounded by auto
102+
103+function decimal :: "nat \<Rightarrow> string" where
104+ "decimal n = (if n < 10 then [char_of_nat (48+n)] else decimal (n div 10) @ [char_of_nat (48+n mod 10)])"
105+ by pat_completeness auto
106+termination by (relation "measure id") (auto simp: div_less_dividend)
107+
108+definition newline :: string where "newline = [CHR 0x0A]"
109+
110+definition artifact :: "string \<Rightarrow> (bool \<times> string) \<times> string" where
111+ "artifact s = (case prepare s of None \<Rightarrow> ((False,[]), ''invalid source or resource limit'' @ newline)
112+ | Some e \<Rightarrow> let opt = optimise e; bytes = executable e in
113+ ((True, map char_of_nat bytes), decimal (nodes e) @ '' nodes -> '' @ decimal (nodes opt) @
114+ '' nodes, '' @ decimal (length bytes) @ '' bytes, '' @ decimal (demand opt) @ '' stack words'' @ newline))"
115+
116+definition boundary :: "nat list" where
117+ "boundary = [0,1,63,64,65,127,255,256,2 ^ 31,2 ^ 32,2 ^ 63,2 ^ 64 - 1]"
118+
119+definition sample :: "nat \<Rightarrow> input \<Rightarrow> pixel" where
120+ "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)
121+ else case v of X \<Rightarrow> (17*i) mod 257 | Y \<Rightarrow> (29*i) mod 131 | T \<Rightarrow> 13*i))"
122+
123+definition row :: "expression \<Rightarrow> nat \<Rightarrow> nat list" where
124+ "row e i = concat (map (\<lambda>v. octets 8 (unat v))
125+ [sample i X, sample i Y, sample i T, evaluate e [] (sample i)])"
126+
127+definition vectors :: "string \<Rightarrow> bool \<times> string" where
128+ "vectors s = (case prepare s of None \<Rightarrow> (False, ''invalid source or resource limit'' @ newline)
129+ | Some e \<Rightarrow> (True, map char_of_nat (concat (map (row e) [0..<512]))))"
130+
131+definition reference :: "string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> bool \<times> string" where
132+ "reference source x y t = (case (prepare source, number x, number y, number t) of
133+ (Some e,Some a,Some b,Some c) \<Rightarrow>
134+ (True, decimal (unat (evaluate e [] (\<lambda>v. word_of_nat (case v of X \<Rightarrow> a | Y \<Rightarrow> b | T \<Rightarrow> c)))) @ newline)
135+ | _ \<Rightarrow> (False,''invalid source or input'' @ newline))"
136+
137+end

src/Model.thy added

@@ -0,0 +1,97 @@
1+theory Model
2+ imports "HOL-Library.Word" "HOL-Library.Code_Target_Numeral"
3+begin
4+
5+unbundle bit_operations_syntax
6+
7+type_synonym pixel = "64 word"
8+
9+datatype input = X | Y | T
10+
11+datatype operator = Add | Sub | Mul | And | Or | Xor | Shl | Shr | Less
12+
13+fun operate :: "operator \<Rightarrow> pixel \<Rightarrow> pixel \<Rightarrow> pixel" where
14+ "operate Add a b = a + b"
15+| "operate Sub a b = a - b"
16+| "operate Mul a b = a * b"
17+| "operate And a b = a AND b"
18+| "operate Or a b = a OR b"
19+| "operate Xor a b = a XOR b"
20+| "operate Shl a b = push_bit (unat b mod 64) a"
21+| "operate Shr a b = drop_bit (unat b mod 64) a"
22+| "operate Less a b = (if a < b then 1 else 0)"
23+
24+datatype expression = Literal pixel | Input input | Variable nat
25+ | Binary operator expression expression
26+ | Cond expression expression expression
27+ | Let expression expression
28+
29+fun evaluate :: "expression \<Rightarrow> pixel list \<Rightarrow> (input \<Rightarrow> pixel) \<Rightarrow> pixel" where
30+ "evaluate (Literal v) env inputs = v"
31+| "evaluate (Input i) env inputs = inputs i"
32+| "evaluate (Variable i) env inputs = env ! i"
33+| "evaluate (Binary op a b) env inputs = operate op (evaluate a env inputs) (evaluate b env inputs)"
34+| "evaluate (Cond c a b) env inputs = (if evaluate c env inputs = 0 then evaluate b env inputs else evaluate a env inputs)"
35+| "evaluate (Let a b) env inputs = evaluate b (evaluate a env inputs # env) inputs"
36+
37+fun scoped :: "nat \<Rightarrow> expression \<Rightarrow> bool" where
38+ "scoped n (Literal v) = True"
39+| "scoped n (Input i) = True"
40+| "scoped n (Variable i) = (i < n)"
41+| "scoped n (Binary op a b) = (scoped n a \<and> scoped n b)"
42+| "scoped n (Cond c a b) = (scoped n c \<and> scoped n a \<and> scoped n b)"
43+| "scoped n (Let a b) = (scoped n a \<and> scoped (Suc n) b)"
44+
45+fun fold_binary :: "operator \<Rightarrow> expression \<Rightarrow> expression \<Rightarrow> expression" where
46+ "fold_binary op (Literal a) (Literal b) = Literal (operate op a b)"
47+| "fold_binary op a b = Binary op a b"
48+
49+fun fold_cond :: "expression \<Rightarrow> expression \<Rightarrow> expression \<Rightarrow> expression" where
50+ "fold_cond (Literal c) a b = (if c = 0 then b else a)"
51+| "fold_cond c a b = Cond c a b"
52+
53+fun optimise :: "expression \<Rightarrow> expression" where
54+ "optimise (Binary op a b) = fold_binary op (optimise a) (optimise b)"
55+| "optimise (Cond c a b) = fold_cond (optimise c) (optimise a) (optimise b)"
56+| "optimise (Let a b) = Let (optimise a) (optimise b)"
57+| "optimise e = e"
58+
59+lemma fold_binary_value:
60+ "evaluate (fold_binary op a b) env inputs = operate op (evaluate a env inputs) (evaluate b env inputs)"
61+ by (cases a; cases b) auto
62+
63+lemma fold_cond_value:
64+ "evaluate (fold_cond c a b) env inputs = (if evaluate c env inputs = 0 then evaluate b env inputs else evaluate a env inputs)"
65+ by (cases c) auto
66+
67+theorem optimise_correct:
68+ "evaluate (optimise e) env inputs = evaluate e env inputs"
69+ by (induction e arbitrary: env) (simp_all add: fold_binary_value fold_cond_value)
70+
71+lemma fold_binary_scoped:
72+ "scoped n a \<Longrightarrow> scoped n b \<Longrightarrow> scoped n (fold_binary op a b)"
73+ by (cases a; cases b) auto
74+
75+lemma fold_cond_scoped:
76+ "scoped n c \<Longrightarrow> scoped n a \<Longrightarrow> scoped n b \<Longrightarrow> scoped n (fold_cond c a b)"
77+ by (cases c) auto
78+
79+theorem optimise_scoped: "scoped n e \<Longrightarrow> scoped n (optimise e)"
80+ by (induction e arbitrary: n) (auto intro: fold_binary_scoped fold_cond_scoped)
81+
82+fun nodes :: "expression \<Rightarrow> nat" where
83+ "nodes (Binary op a b) = Suc (nodes a + nodes b)"
84+| "nodes (Cond c a b) = Suc (nodes c + nodes a + nodes b)"
85+| "nodes (Let a b) = Suc (nodes a + nodes b)"
86+| "nodes _ = 1"
87+
88+lemma fold_binary_nodes: "nodes (fold_binary op a b) \<le> Suc (nodes a + nodes b)"
89+ by (cases a; cases b) auto
90+
91+lemma fold_cond_nodes: "nodes (fold_cond c a b) \<le> Suc (nodes c + nodes a + nodes b)"
92+ by (cases c) auto
93+
94+theorem optimise_size: "nodes (optimise e) \<le> nodes e"
95+ by (induction e) (auto intro: order_trans[OF fold_binary_nodes] order_trans[OF fold_cond_nodes])
96+
97+end

src/Native.thy added

@@ -0,0 +1,163 @@
1+theory Native
2+ imports Compiler
3+begin
4+
5+datatype register = Rax | Rcx | Rbx | Rdx | R8 | R9
6+
7+datatype opcode = Immediate pixel | Push register | Pop register | Peek nat
8+ | Arithmetic operator | Conditional
9+
10+record machine =
11+ registers :: "register \<Rightarrow> pixel"
12+ stack :: "pixel list"
13+
14+fun input_register :: "input \<Rightarrow> register" where
15+ "input_register X = R8"
16+| "input_register Y = R9"
17+| "input_register T = Rdx"
18+
19+definition inputs :: "machine \<Rightarrow> input \<Rightarrow> pixel" where
20+ "inputs s i = registers s (input_register i)"
21+
22+fun exchanges :: "operator \<Rightarrow> bool" where
23+ "exchanges Sub = True"
24+| "exchanges Shl = True"
25+| "exchanges Shr = True"
26+| "exchanges Less = True"
27+| "exchanges _ = False"
28+
29+fun transition :: "opcode \<Rightarrow> machine \<Rightarrow> machine option" where
30+ "transition (Immediate v) s = Some (s\<lparr>registers := (registers s)(Rax := v)\<rparr>)"
31+| "transition (Push r) s = Some (s\<lparr>stack := registers s r # stack s\<rparr>)"
32+| "transition (Pop r) s = (case stack s of [] \<Rightarrow> None | v # vs \<Rightarrow>
33+ Some (s\<lparr>registers := (registers s)(r := v), stack := vs\<rparr>))"
34+| "transition (Peek i) s = (if i < length (stack s) then
35+ Some (s\<lparr>registers := (registers s)(Rax := stack s ! i)\<rparr>) else None)"
36+| "transition (Arithmetic op) s = Some (s\<lparr>registers :=
37+ (registers s)(Rcx := if exchanges op then registers s Rax else registers s Rcx,
38+ Rax := operate op (registers s Rcx) (registers s Rax))\<rparr>)"
39+| "transition Conditional s = Some (s\<lparr>registers :=
40+ (registers s)(Rax := if registers s Rbx = 0 then registers s Rax else registers s Rcx)\<rparr>)"
41+
42+fun run :: "opcode list \<Rightarrow> machine \<Rightarrow> machine option" where
43+ "run [] s = Some s"
44+| "run (i # code) s = Option.bind (transition i s) (run code)"
45+
46+lemma run_append:
47+ "run (a @ b) s = Option.bind (run a s) (run b)"
48+ by (induction a arbitrary: s) (auto split: option.splits bind_splits)
49+
50+fun lower :: "instruction \<Rightarrow> opcode list" where
51+ "lower (Constant v) = [Immediate v, Push Rax]"
52+| "lower (Fetch i) = [Push (input_register i)]"
53+| "lower (Pick i) = [Peek i, Push Rax]"
54+| "lower (Calculate op) = [Pop Rax, Pop Rcx, Arithmetic op, Push Rax]"
55+| "lower Choose = [Pop Rax, Pop Rcx, Pop Rbx, Conditional, Push Rax]"
56+| "lower Slide = [Pop Rax, Pop Rcx, Push Rax]"
57+
58+definition observe :: "machine \<Rightarrow> (input \<Rightarrow> pixel) \<times> pixel list" where
59+ "observe s = (inputs s, stack s)"
60+
61+lemma input_scratch [simp]:
62+ "input_register i \<noteq> Rax"
63+ "input_register i \<noteq> Rcx"
64+ "input_register i \<noteq> Rbx"
65+ by (cases i; simp)+
66+
67+lemma inputs_update [simp]:
68+ "inputs (s\<lparr>registers := (registers s)(Rax := a)\<rparr>) = inputs s"
69+ "inputs (s\<lparr>registers := (registers s)(Rcx := a)\<rparr>) = inputs s"
70+ "inputs (s\<lparr>registers := (registers s)(Rbx := a)\<rparr>) = inputs s"
71+ "inputs (s\<lparr>stack := vs\<rparr>) = inputs s"
72+ by (auto simp: inputs_def fun_eq_iff split: input.splits)
73+
74+theorem lower_correct:
75+ "map_option observe (run (lower i) s) =
76+ map_option (\<lambda>vs. (inputs s, vs)) (step (inputs s) i (stack s))"
77+proof (cases i)
78+ case (Constant v)
79+ then show ?thesis by (simp add: observe_def)
80+next
81+ case (Fetch i)
82+ then show ?thesis by (simp add: observe_def inputs_def)
83+next
84+ case (Pick i)
85+ then show ?thesis by (simp add: observe_def)
86+next
87+ case (Calculate op)
88+ then show ?thesis
89+ by (cases "stack s"; simp add: observe_def inputs_def fun_eq_iff split: list.splits input.splits)
90+next
91+ case Choose
92+ then show ?thesis
93+ by (cases "stack s"; simp add: observe_def inputs_def fun_eq_iff split: list.splits input.splits)
94+next
95+ case Slide
96+ then show ?thesis
97+ by (cases "stack s"; simp add: observe_def inputs_def fun_eq_iff split: list.splits input.splits)
98+qed
99+
100+definition native :: "instruction list \<Rightarrow> opcode list" where
101+ "native code = concat (map lower code)"
102+
103+theorem native_correct:
104+ "map_option observe (run (native code) s) =
105+ map_option (\<lambda>vs. (inputs s, vs)) (execute (inputs s) code (stack s))"
106+proof (induction code arbitrary: s)
107+ case Nil
108+ then show ?case by (simp add: native_def observe_def)
109+next
110+ case (Cons i code)
111+ show ?case
112+ using Cons.IH lower_correct[of i s]
113+ by (auto simp: native_def run_append observe_def split: option.splits bind_splits)
114+qed
115+
116+corollary native_expression:
117+ assumes "scoped 0 e"
118+ shows "map_option observe (run (native (compile (optimise e) [])) s) =
119+ Some (inputs s, evaluate e [] (inputs s) # stack s)"
120+proof -
121+ have code: "execute (inputs s) (compile (optimise e) []) (stack s) =
122+ Some (evaluate e [] (inputs s) # stack s)"
123+ using compile_correct[where e="optimise e" and env="[]" and slots="[]" and s="stack s" and inputs="inputs s"]
124+ assms optimise_scoped
125+ by (simp add: represents_def optimise_correct)
126+ show ?thesis using native_correct[of "compile (optimise e) []" s] code by simp
127+qed
128+
129+theorem native_return:
130+ assumes "scoped 0 e"
131+ shows "\<exists>q. run (native (compile (optimise e) []) @ [Pop Rax]) s = Some q \<and>
132+ registers q Rax = evaluate e [] (inputs s) \<and> stack q = stack s \<and> inputs q = inputs s"
133+proof -
134+ obtain q where run: "run (native (compile (optimise e) [])) s = Some q"
135+ and ins: "inputs q = inputs s" and stk: "stack q = evaluate e [] (inputs s) # stack s"
136+ using native_expression[OF assms, of s]
137+ by (auto simp: observe_def split: option.splits)
138+ show ?thesis using run ins stk
139+ by (auto simp: run_append inputs_def fun_eq_iff)
140+qed
141+
142+fun writes :: "opcode \<Rightarrow> register set" where
143+ "writes (Immediate v) = {Rax}"
144+| "writes (Pop r) = {r}"
145+| "writes (Peek i) = {Rax}"
146+| "writes (Arithmetic op) = {Rax,Rcx}"
147+| "writes Conditional = {Rax}"
148+| "writes _ = {}"
149+
150+lemma transition_preserves:
151+ "transition i s = Some t \<Longrightarrow> r \<notin> writes i \<Longrightarrow> registers t r = registers s r"
152+ by (cases i) (auto split: list.splits if_splits)
153+
154+theorem run_preserves:
155+ "run code s = Some t \<Longrightarrow> list_all (\<lambda>i. r \<notin> writes i) code \<Longrightarrow>
156+ registers t r = registers s r"
157+ by (induction code arbitrary: s) (auto dest: transition_preserves split: option.splits bind_splits)
158+
159+lemma lower_scratch:
160+ "list_all (\<lambda>i. writes i \<subseteq> {Rax,Rcx,Rbx}) (lower op)"
161+ by (cases op) auto
162+
163+end

tests/native.py added

@@ -0,0 +1,102 @@
1+import ctypes
2+import mmap
3+from pathlib import Path
4+import platform
5+import random
6+import struct
7+import subprocess
8+import tempfile
9+
10+
11+ROOT = Path(__file__).resolve().parents[1]
12+MASK = (1 << 64) - 1
13+OPERATORS = ("+", "-", "*", "and", "or", "xor", "shl", "shr", "<")
14+
15+
16+def evaluate(e, env):
17+ if isinstance(e, int):
18+ return e
19+ if isinstance(e, str):
20+ return env[e]
21+ op, *args = e
22+ if op == "let":
23+ name, a, b = args
24+ return evaluate(b, {**env, name: evaluate(a, env)})
25+ if op == "if":
26+ c, a, b = args
27+ return evaluate(a if evaluate(c, env) else b, env)
28+ a, b = (evaluate(x, env) for x in args)
29+ return {"+": lambda: a + b, "-": lambda: a - b, "*": lambda: a * b,
30+ "and": lambda: a & b, "or": lambda: a | b, "xor": lambda: a ^ b,
31+ "shl": lambda: a << (b & 63), "shr": lambda: a >> (b & 63),
32+ "<": lambda: int(a < b)}[op]() & MASK
33+
34+
35+def source(e):
36+ return "(" + " ".join(map(source, e)) + ")" if isinstance(e, tuple) else str(e)
37+
38+
39+def native(code):
40+ image = mmap.mmap(-1, len(code), prot=mmap.PROT_READ | mmap.PROT_WRITE | mmap.PROT_EXEC)
41+ image.write(code)
42+ address = ctypes.addressof(ctypes.c_char.from_buffer(image))
43+ bridge = bytes.fromhex("53 49 89 f8 49 89 f1 48 b8") + struct.pack("<Q", address) + bytes.fromhex("ff d0 5b c3")
44+ thunk = mmap.mmap(-1, len(bridge), prot=mmap.PROT_READ | mmap.PROT_WRITE | mmap.PROT_EXEC)
45+ thunk.write(bridge)
46+ function = ctypes.CFUNCTYPE(ctypes.c_uint64, ctypes.c_uint64, ctypes.c_uint64, ctypes.c_uint64)(
47+ ctypes.addressof(ctypes.c_char.from_buffer(thunk)))
48+ return function, image, thunk
49+
50+
51+def generate(rng, depth, names):
52+ if depth == 0 or rng.randrange(5) == 0:
53+ return rng.choice([0, 1, 63, 64, 65, MASK, 1 << 63, *names])
54+ kind = rng.randrange(5)
55+ if kind == 0:
56+ name = rng.choice(("a", "b", "c", "x"))
57+ return ("let", name, generate(rng, depth - 1, names), generate(rng, depth - 1, [*names, name]))
58+ if kind == 1:
59+ return ("if", *(generate(rng, depth - 1, names) for _ in range(3)))
60+ return (rng.choice(OPERATORS), *(generate(rng, depth - 1, names) for _ in range(2)))
61+
62+
63+def main():
64+ if platform.system() != "Linux" or platform.machine() != "x86_64":
65+ raise RuntimeError("native differential tests require an x86-64 Linux host")
66+ rng = random.Random(0x52454D59)
67+ cases = [(op, "x", "y") for op in OPERATORS]
68+ cases += [("let", "a", ("+", "x", 3), ("+", "y", ("let", "b", "t", ("*", "a", "b")))),
69+ ("let", "x", "y", ("if", "t", ("+", "x", 1), ("-", "x", 1)))]
70+ cases += [generate(rng, 5, ["x", "y", "t"]) for _ in range(117)]
71+ comparisons = 0
72+ with tempfile.TemporaryDirectory() as directory:
73+ path, binary = Path(directory) / "source", Path(directory) / "binary"
74+ for case in cases:
75+ path.write_text(source(case))
76+ result = subprocess.run([ROOT / ".build/remy", path, binary], capture_output=True, text=True, timeout=30)
77+ assert result.returncode == 0, (case, result.stderr)
78+ function, image, thunk = native(binary.read_bytes())
79+ vectors = [(a, b, a ^ b) for a in (0, 1, MASK, 1 << 63) for b in (0, 1, 63, 64, 65, MASK)]
80+ vectors += [tuple(rng.getrandbits(64) for _ in range(3)) for _ in range(24)]
81+ for x, y, t in vectors:
82+ expected = evaluate(case, {"x": x, "y": y, "t": t})
83+ actual = function(x, y, t)
84+ assert actual == expected, (source(case), x, y, t, expected, actual)
85+ comparisons += 1
86+ result = subprocess.run([ROOT / ".build/remy", "eval", path, str(x), str(y), str(t)],
87+ capture_output=True, text=True, timeout=30)
88+ assert result.returncode == 0 and int(result.stdout) == expected, (case, result.stdout, result.stderr)
89+ del function
90+ image.close()
91+ thunk.close()
92+ for bad in ("", "(+ x)", "(+ x y) 1", "(let a 3 b)", "(if 1 2)", "(let if 3 4)",
93+ "18446744073709551616", "(+ x z)", "(div x y)", "é", " " * 65537):
94+ path.write_text(bad)
95+ binary.write_bytes(b"preserve")
96+ result = subprocess.run([ROOT / ".build/remy", path, binary], capture_output=True, timeout=30)
97+ assert result.returncode != 0 and binary.read_bytes() == b"preserve", bad
98+ print(f"{len(cases)} programs, {comparisons} native comparisons, HOL reference checks and 11 rejection cases passed")
99+
100+
101+if __name__ == "__main__":
102+ main()