~james/remy

feat(x86): prove emitted instruction execution and return-frame consumption

commit
7cb596d931d773db10cc8df8c329cd8b881a8826 browse tree
parent
b58768f9b4b75a882c2394ff6c2135d32062939d
author
james <j@cpl0.zip>
signature
Verified ~james signed with a key registered by ~james
date
2026-11-01 03:54 UTC

9 files changed, +415 −13

README.md modified

@@ -21,11 +21,29 @@ Verify;
2121 Show(0);
2222 ```
2323
24+## Usage
25+
26+The byte interpreter follows encoded jumps and consumes a synthetic return address through `ret`. Compare its result with `eval` using the same `x`, `y` and `t` arguments
27+
28+```sh
29+.build/remy examples/Rings.remy /tmp/rings.bin
30+.build/remy simulate /tmp/rings.bin 17 23 41
31+.build/remy eval examples/Rings.remy 17 23 41
32+```
33+
34+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
35+
2436 ## Correctness
2537
26-Each `let` pushes a binding onto the evaluation stack. [Compilation](src/core/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
38+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
39+
40+The [encoder](src/core/Encoding.thy) proves inversion and byte bounds for immediate operands and stack displacements, while [native lowering](src/core/Native.thy) uses the following register convention to keep pixel inputs available across expression evaluation
2741
28-[Native lowering](src/core/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/core/Encoding.thy) proves decoder inversion and byte bounds for the emitted blocks including their immediate operands and stack displacements
42+| Registers | Role |
43+| --- | --- |
44+| `r8`, `r9`, `rdx` | Preserved inputs `x`, `y`, `t` |
45+| `rax` | Accumulator and result |
46+| `rcx`, `rbx` | Scratch |
2947
3048 ![Source eval](media/correspondence.svg)
3149
@@ -33,4 +51,4 @@ Arithmetic wraps modulo `2^64` and shifts mask their count to six bits
3351
3452 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
3553
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
54+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

ROOT modified

@@ -16,6 +16,7 @@ session Remy in src = Remybase +
1616 theories
1717 Allocation
1818 Branches
19+ X86
1920 Frontend
2021 Examples
2122 Export

cli/driver.ML modified

@@ -67,13 +67,14 @@ fun main () =
6767 ["vectors", source, destination] =>
6868 (case Remy.vectors (read source) of (true, bytes) => write destination bytes | result => output result)
6969 | ["eval", source, x, y, t] => output (Remy.reference (read source) (chars x) (chars y) (chars t))
70+ | ["simulate", binary, x, y, t] => output (Remy.simulate (read binary) (chars x) (chars y) (chars t))
7071 | ["limits", depth, nodes, stack, source, destination] =>
7172 emit destination (Remy.configured (chars depth) (chars nodes) (chars stack) (read source))
7273 | ["check", binary] => output (Remy.validate (read binary))
7374 | ["disassemble", binary] => output (Remy.disassemble (read binary))
7475 | ["baseline", source, destination] => emit destination (Remy.baseline (read source))
7576 | [source, destination] => emit destination (Remy.artifact (read source))
76- | _ => raise Fail "usage: remy check binary | remy disassemble binary | 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)")
77+ | _ => 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)")
7778 handle exn =>
7879 (TextIO.output (TextIO.stdErr, "remy: " ^ General.exnMessage exn ^ "\n");
7980 OS.Process.exit OS.Process.failure);

media/correspondence.svg modified

@@ -1,17 +1,19 @@
1-<svg xmlns="http://www.w3.org/2000/svg" width="720" height="208" viewBox="0 0 720 208">
1+<svg xmlns="http://www.w3.org/2000/svg" width="720" height="208" viewBox="0 0 720 208" role="img" aria-labelledby="title description">
2+ <title id="title">Compiler execution correspondence</title>
3+ <desc id="description">Source evaluation agrees with instruction execution of emitted bytes, with RAX containing the result and the caller frame preserved</desc>
24 <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>
35 <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 fill="none" stroke="#555" stroke-width="1" marker-end="url(#arrow)">
7+ <path d="M 176 45 H 547"/><path d="M 140 64 V 143"/><path d="M 582 143 V 64"/><path d="M 176 164 H 547"/>
68 </g>
79 <g fill="white" stroke="#555">
810 <rect x="62" y="25" width="114" height="40" rx="3"/><rect x="547" y="25" width="113" height="40" rx="3"/>
911 <rect x="38" y="144" width="138" height="40" rx="3"/><rect x="547" y="144" width="138" height="40" rx="3"/>
1012 </g>
11- <g font-family="monospace" font-size="14" fill="#222" text-anchor="middle">
13+ <g font-family="STIX Two Text, Libertinus Serif, Georgia, serif" font-size="15" fill="#222" text-anchor="middle">
1214 <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>
15+ <text x="107" y="169">emitted bytes</text><text x="616" y="169">RAX + frame</text>
16+ <text x="360" y="35">source evaluation</text><text x="360" y="153">x86 instruction execution</text>
17+ <text x="360" y="106">folding · allocation · branches · encoding</text>
1618 </g>
1719 </svg>

src/Export.thy modified

@@ -6,6 +6,6 @@ definition ascii :: "integer \<Rightarrow> char" where "ascii = char_of"
66
77 definition ordinal :: "char \<Rightarrow> integer" where "ordinal = of_char"
88
9-export_code validate disassemble configured artifact baseline vectors reference ascii ordinal in SML module_name Remy file_prefix remy
9+export_code validate disassemble configured artifact baseline vectors reference simulate ascii ordinal in SML module_name Remy file_prefix remy
1010
1111 end

src/Frontend.thy modified

@@ -1,5 +1,5 @@
11 theory Frontend
2- imports Branches
2+ imports X86
33 begin
44
55 fun finish :: "string \<Rightarrow> string list \<Rightarrow> string list" where
@@ -303,6 +303,20 @@ definition source_error :: "string \<Rightarrow> string" where
303303 definition artifact :: "string \<Rightarrow> (bool \<times> string) \<times> string" where
304304 "artifact = artifact_with defaults"
305305
306+theorem artifact_execution:
307+ assumes "artifact source = ((True,bytes),report)"
308+ shows "\<exists>e d. prepare source = Some e \<and>
309+ bytes = map char_of_nat (flowbytes (branching e) @ [195]) \<and>
310+ executes64 (flowbytes (branching e)) c d \<and>
311+ registers (state64 d) Rax = evaluate e [] (inputs (state64 c)) \<and>
312+ stack (state64 d) = stack (state64 c) \<and> inputs (state64 d) = inputs (state64 c)"
313+proof -
314+ obtain e where e: "prepare source = Some e" "flowvalid (branching e)"
315+ "bytes = map char_of_nat (flowbytes (branching e) @ [195])"
316+ using assms by (auto simp: artifact_def artifact_with_def prepare_def Let_def split: option.splits if_splits)
317+ show ?thesis using compiled_execution[OF prepare_scoped[OF e(1)] e(2), of c] e by blast
318+qed
319+
306320 definition baseline :: "string \<Rightarrow> (bool \<times> string) \<times> string" where
307321 "baseline s = (case prepare s of None \<Rightarrow> ((False,[]),source_error s)
308322 | Some e \<Rightarrow> ((True,map char_of_nat (executable e)),''stack backend'' @ newline))"
@@ -333,4 +347,19 @@ definition reference :: "string \<Rightarrow> string \<Rightarrow> string \<Righ
333347 (True, decimal (unat (evaluate e [] (\<lambda>v. word_of_nat (case v of X \<Rightarrow> a | Y \<Rightarrow> b | T \<Rightarrow> c)))) @ newline)
334348 | _ \<Rightarrow> (False,''invalid input'' @ newline))"
335349
350+definition initial64 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> processor" where
351+ "initial64 x y t = \<lparr>state64 = \<lparr>registers = (\<lambda>r. word_of_nat
352+ (if r = R8 then x else if r = R9 then y else if r = Rdx then t else 0)), stack = [0]\<rparr>,
353+ pointer64 = 65536, zero64 = None, carry64 = None\<rparr>"
354+
355+definition simulate :: "string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> bool \<times> string" where
356+ "simulate code x y t = (if \<not> fst (validate code) then (False,''invalid native image'' @ newline) else
357+ case (number x,number y,number t) of (Some a,Some b,Some c) \<Rightarrow>
358+ (case simulate64 (Suc (length code)) (map nat_of_char code) (initial64 a b c) of
359+ None \<Rightarrow> (False,''unsupported or incomplete x86 execution'' @ newline)
360+ | Some q \<Rightarrow> if stack (state64 q) = []
361+ then (True,decimal (unat (registers (state64 q) Rax)) @ newline)
362+ else (False,''return frame was not consumed'' @ newline))
363+ | _ \<Rightarrow> (False,''invalid input'' @ newline))"
364+
336365 end

src/X86.thy added

@@ -0,0 +1,345 @@
1+theory X86
2+ imports Branches
3+begin
4+
5+datatype micro = Imm64 pixel | Imm32 pixel | Copy register register | Save register | Restore register
6+ | Load nat | Alu operator | Exchange | Compare | Below | Extend | Test register | Select
7+
8+record processor =
9+ state64 :: machine
10+ pointer64 :: pixel
11+ zero64 :: "bool option"
12+ carry64 :: "bool option"
13+
14+definition put64 :: "register \<Rightarrow> pixel \<Rightarrow> processor \<Rightarrow> processor" where
15+ "put64 r v c = c\<lparr>state64 := (state64 c)\<lparr>registers := (registers (state64 c))(r := v)\<rparr>\<rparr>"
16+
17+fun microstep :: "micro \<Rightarrow> processor \<Rightarrow> processor option" where
18+ "microstep (Imm64 v) c = Some (put64 Rax v c)"
19+| "microstep (Imm32 v) c = Some (put64 Rax v c)"
20+| "microstep (Copy dst src) c = Some (put64 dst (registers (state64 c) src) c)"
21+| "microstep (Save r) c = Some (c\<lparr>state64 := (state64 c)\<lparr>stack := registers (state64 c) r # stack (state64 c)\<rparr>,
22+ pointer64 := pointer64 c - 8\<rparr>)"
23+| "microstep (Restore r) c = (case stack (state64 c) of [] \<Rightarrow> None | v # vs \<Rightarrow>
24+ Some ((put64 r v c)\<lparr>state64 := (state64 (put64 r v c))\<lparr>stack := vs\<rparr>, pointer64 := pointer64 c + 8\<rparr>))"
25+| "microstep (Load i) c = (if i < length (stack (state64 c))
26+ then Some (put64 Rax (stack (state64 c) ! i) c) else None)"
27+| "microstep (Alu op) c = (if op = Less then None else
28+ Some ((put64 Rax (operate op (registers (state64 c) Rax) (registers (state64 c) Rcx)) c)
29+ \<lparr>zero64 := None, carry64 := None\<rparr>))"
30+| "microstep Exchange c = Some (put64 Rcx (registers (state64 c) Rax)
31+ (put64 Rax (registers (state64 c) Rcx) c))"
32+| "microstep Compare c = Some (c\<lparr>zero64 := Some (registers (state64 c) Rax = registers (state64 c) Rcx),
33+ carry64 := Some (registers (state64 c) Rax < registers (state64 c) Rcx)\<rparr>)"
34+| "microstep Below c = (case carry64 c of None \<Rightarrow> None | Some flag \<Rightarrow>
35+ Some (put64 Rax ((registers (state64 c) Rax AND NOT 255) OR (if flag then 1 else 0)) c))"
36+| "microstep Extend c = Some (put64 Rax (registers (state64 c) Rax AND 255) c)"
37+| "microstep (Test r) c = Some (c\<lparr>zero64 := Some (registers (state64 c) r = 0), carry64 := Some False\<rparr>)"
38+| "microstep Select c = (case zero64 c of None \<Rightarrow> None | Some flag \<Rightarrow>
39+ Some (if flag then c else put64 Rax (registers (state64 c) Rcx) c))"
40+
41+fun microrun :: "micro list \<Rightarrow> processor \<Rightarrow> processor option" where
42+ "microrun [] c = Some c"
43+| "microrun (i # code) c = Option.bind (microstep i c) (microrun code)"
44+
45+lemma microrun_append:
46+ "microrun (a @ b) c = Option.bind (microrun a c) (microrun b)"
47+ by (induction a arbitrary: c) (auto split: option.splits bind_splits)
48+
49+fun microbytes :: "micro \<Rightarrow> nat list" where
50+ "microbytes (Imm64 v) = [72,184] @ octets 8 (unat v)"
51+| "microbytes (Imm32 v) = [72,199,192] @ octets 4 (unat v)"
52+| "microbytes (Copy dst src) = movecode dst src"
53+| "microbytes (Save r) = pushcode r"
54+| "microbytes (Restore r) = popcode r"
55+| "microbytes (Load i) = (if i < 16 then [72,139,68,36,8*i]
56+ else [72,139,132,36] @ octets 4 (8*i))"
57+| "microbytes (Alu Add) = [72,1,200]"
58+| "microbytes (Alu Sub) = [72,41,200]"
59+| "microbytes (Alu Mul) = [72,15,175,193]"
60+| "microbytes (Alu And) = [72,33,200]"
61+| "microbytes (Alu Or) = [72,9,200]"
62+| "microbytes (Alu Xor) = [72,49,200]"
63+| "microbytes (Alu Shl) = [72,211,224]"
64+| "microbytes (Alu Shr) = [72,211,232]"
65+| "microbytes (Alu Less) = []"
66+| "microbytes Exchange = [72,145]"
67+| "microbytes Compare = [72,57,200]"
68+| "microbytes Below = [15,146,192]"
69+| "microbytes Extend = [72,15,182,192]"
70+| "microbytes (Test r) = [72,133,192 + 9 * regno r]"
71+| "microbytes Select = [72,15,69,193]"
72+
73+fun microvalid :: "micro \<Rightarrow> bool" where
74+ "microvalid (Imm32 v) = (extend32 (unat v) = v)"
75+| "microvalid (Load i) = (i < 2 ^ 28)"
76+| "microvalid (Alu Less) = False"
77+| "microvalid (Test r) = (r = Rax \<or> r = Rbx)"
78+| "microvalid _ = True"
79+
80+fun expand :: "opcode \<Rightarrow> micro list" where
81+ "expand (Immediate v) = [if extend32 (unat v) = v then Imm32 v else Imm64 v]"
82+| "expand (Push r) = [Save r]"
83+| "expand (Pop r) = [Restore r]"
84+| "expand (Move dst src) = [Copy dst src]"
85+| "expand (Peek i) = [Load i]"
86+| "expand (Arithmetic op) = (if op = Less then [Exchange,Compare,Below,Extend]
87+ else if exchanges op then [Exchange,Alu op] else [Alu op])"
88+| "expand Conditional = [Test Rbx,Select]"
89+
90+lemma byte_register:
91+ "((v AND NOT 255) OR (if flag then 1 else 0)) AND 255 = (if flag then 1 else 0 :: pixel)"
92+ by (cases flag) (simp_all add: word_ao_dist word_bw_assocs)
93+
94+theorem expand_state:
95+ "map_option state64 (microrun (expand op) c) = transition op (state64 c)"
96+proof (cases op)
97+ case (Arithmetic f)
98+ then show ?thesis
99+ by (cases f)
100+ (auto simp: put64_def byte_register word_ao_dist2 word_ao_dist word_bw_assocs ac_simps split: option.splits)
101+next
102+ case (Pop r)
103+ then show ?thesis by (cases "stack (state64 c)") (auto simp: put64_def)
104+qed (auto simp: put64_def split: if_splits option.splits)
105+
106+theorem expand_bytes:
107+ "concat (map microbytes (expand op)) = encode op"
108+proof (cases op)
109+ case (Arithmetic f)
110+ then show ?thesis by (cases f) auto
111+qed auto
112+
113+lemma expand_valid:
114+ "encodable op \<Longrightarrow> list_all microvalid (expand op)"
115+proof (cases op)
116+ case (Arithmetic f)
117+ then show ?thesis by (cases f) auto
118+qed auto
119+
120+theorem expand_run:
121+ "map_option state64 (microrun (concat (map expand code)) c) = run code (state64 c)"
122+proof (induction code arbitrary: c)
123+ case Nil
124+ then show ?case by simp
125+next
126+ case (Cons op code)
127+ then show ?case using expand_state[of op c]
128+ by (auto simp: microrun_append split: option.splits bind_splits)
129+qed
130+
131+definition top64 :: "processor \<Rightarrow> pixel" where
132+ "top64 c = pointer64 c + 8 * of_nat (length (stack (state64 c)))"
133+
134+lemma microstep_top:
135+ "microstep i c = Some d \<Longrightarrow> top64 d = top64 c"
136+ by (cases i)
137+ (auto simp: top64_def put64_def algebra_simps split: list.splits if_splits option.splits)
138+
139+definition fixed64 :: "micro list" where
140+ "fixed64 = map Save [Rax,Rcx,Rbx,Rdx,R8,R9] @ map Restore [Rax,Rcx,Rbx,Rdx,R8,R9] @
141+ concat (map (\<lambda>dst. map (Copy dst) [Rax,Rcx,Rbx,Rdx,R8,R9]) [Rax,Rcx,Rbx,Rdx,R8,R9]) @
142+ map Alu [Add,Sub,Mul,And,Or,Xor,Shl,Shr] @ [Exchange,Compare,Below,Extend,Test Rax,Test Rbx,Select]"
143+
144+definition decode64 :: "nat list \<Rightarrow> (micro \<times> nat list) option" where
145+ "decode64 bs = (if take 2 bs = [72,184] then
146+ if 10 \<le> length bs then Some (Imm64 (word_of_nat (integer (take 8 (drop 2 bs)))),drop 10 bs) else None
147+ else if take 3 bs = [72,199,192] then
148+ if 7 \<le> length bs then Some (Imm32 (extend32 (integer (take 4 (drop 3 bs)))),drop 7 bs) else None
149+ else if take 4 bs = [72,139,68,36] then
150+ let n = integer (take 1 (drop 4 bs)) in
151+ if 5 \<le> length bs \<and> n < 128 \<and> n mod 8 = 0 then Some (Load (n div 8),drop 5 bs) else None
152+ else if take 4 bs = [72,139,132,36] then
153+ let n = integer (take 4 (drop 4 bs)) in
154+ if 8 \<le> length bs \<and> n mod 8 = 0 \<and> n div 8 < 2 ^ 28
155+ then Some (Load (n div 8),drop 8 bs) else None
156+ else map_option (\<lambda>i. (i,drop (length (microbytes i)) bs))
157+ (List.find (\<lambda>i. take (length (microbytes i)) bs = microbytes i) fixed64))"
158+
159+theorem decode64_encode:
160+ assumes "microvalid i"
161+ shows "decode64 (microbytes i @ tail) = Some (i,tail)"
162+proof (cases i)
163+ case (Imm64 v)
164+ then show ?thesis by (simp add: decode64_def)
165+next
166+ case (Imm32 v)
167+ then show ?thesis using assms by (simp add: decode64_def)
168+next
169+ case (Copy dst src)
170+ then show ?thesis by (cases dst; cases src) (simp_all add: decode64_def fixed64_def movecode_def)
171+next
172+ case (Save r)
173+ then show ?thesis by (cases r) (simp_all add: decode64_def fixed64_def)
174+next
175+ case (Restore r)
176+ then show ?thesis by (cases r) (simp_all add: decode64_def fixed64_def)
177+next
178+ case (Load n)
179+ then show ?thesis using assms peek_bound[of n]
180+ by (auto simp: decode64_def integer_octets Let_def)
181+next
182+ case (Alu op)
183+ then show ?thesis using assms by (cases op) (simp_all add: decode64_def fixed64_def movecode_def)
184+next
185+ case (Test r)
186+ then show ?thesis using assms by (cases r) (simp_all add: decode64_def fixed64_def movecode_def)
187+qed (simp_all add: decode64_def fixed64_def movecode_def)
188+
189+inductive executes64 :: "nat list \<Rightarrow> processor \<Rightarrow> processor \<Rightarrow> bool" where
190+ empty: "executes64 [] c c"
191+| advance: "microvalid i \<Longrightarrow> microstep i c = Some d \<Longrightarrow> executes64 tail d e \<Longrightarrow>
192+ executes64 (microbytes i @ tail) c e"
193+| jump: "n < 2 ^ 31 \<Longrightarrow> n \<le> length tail \<Longrightarrow> executes64 (drop n tail) c d \<Longrightarrow>
194+ executes64 ([233] @ octets 4 n @ tail) c d"
195+| zero: "n < 2 ^ 31 \<Longrightarrow> n \<le> length tail \<Longrightarrow> zero64 c = Some True \<Longrightarrow>
196+ executes64 (drop n tail) c d \<Longrightarrow> executes64 ([15,132] @ octets 4 n @ tail) c d"
197+| nonzero: "n < 2 ^ 31 \<Longrightarrow> zero64 c = Some False \<Longrightarrow> executes64 tail c d \<Longrightarrow>
198+ executes64 ([15,132] @ octets 4 n @ tail) c d"
199+
200+lemma executes64_append:
201+ "executes64 a c d \<Longrightarrow> executes64 b d e \<Longrightarrow> executes64 (a @ b) c e"
202+ by (induction a c d rule: executes64.induct)
203+ (auto simp: drop_append intro: executes64.intros[simplified])
204+
205+lemma executes64_micro:
206+ "list_all microvalid code \<Longrightarrow> microrun code c = Some d \<Longrightarrow>
207+ executes64 (concat (map microbytes code)) c d"
208+ by (induction code arbitrary: c) (auto split: option.splits bind_splits intro: executes64.intros)
209+
210+lemma executes64_top:
211+ "executes64 code c d \<Longrightarrow> top64 d = top64 c"
212+ by (induction rule: executes64.induct) (auto dest: microstep_top)
213+
214+theorem executes64_native:
215+ "list_all encodable code \<Longrightarrow> run code (state64 c) = Some s \<Longrightarrow>
216+ \<exists>d. executes64 (concat (map encode code)) c d \<and> state64 d = s"
217+proof -
218+ assume valid: "list_all encodable code" and ran: "run code (state64 c) = Some s"
219+ obtain d where d: "microrun (concat (map expand code)) c = Some d" "state64 d = s"
220+ using expand_run[of code c] ran by (auto split: option.splits)
221+ have safe: "list_all microvalid (concat (map expand code))"
222+ using valid expand_valid by (auto simp: list_all_iff)
223+ have bytes: "concat (map microbytes (concat (map expand code))) = concat (map encode code)"
224+ using expand_bytes by (induction code) auto
225+ show ?thesis using executes64_micro[OF safe d(1)] d(2) bytes by auto
226+qed
227+
228+
229+theorem executes64_flow:
230+ assumes "flowvalid code" "flowrun code (state64 c) = Some s"
231+ shows "\<exists>d. executes64 (flowbytes code) c d \<and> state64 d = s"
232+ using assms
233+proof (induction code arbitrary: c s)
234+ case (Basic code)
235+ then show ?case using executes64_native by fastforce
236+next
237+ case (Sequence a b)
238+ obtain m where a: "flowrun a (state64 c) = Some m" and b: "flowrun b m = Some s"
239+ using Sequence.prems by (auto split: bind_splits)
240+ obtain d where d: "executes64 (flowbytes a) c d" "state64 d = m"
241+ using Sequence.IH(1) Sequence.prems a by auto
242+ obtain e where e: "executes64 (flowbytes b) d e" "state64 e = s"
243+ using Sequence.IH(2) Sequence.prems b d by auto
244+ show ?case using executes64_append[OF d(1) e(1)] e(2) by auto
245+next
246+ case (Choice a b)
247+ let ?c = "c\<lparr>zero64 := Some (registers (state64 c) Rax = 0), carry64 := Some False\<rparr>"
248+ have test: "microstep (Test Rax) c = Some ?c" by simp
249+ have limits: "length (flowbytes a) + 5 < 2 ^ 31" "length (flowbytes b) < 2 ^ 31"
250+ using Choice.prems by auto
251+ show ?case
252+ proof (cases "registers (state64 c) Rax = 0")
253+ case True
254+ obtain d where d: "executes64 (flowbytes b) ?c d" "state64 d = s"
255+ using Choice.IH(2)[of ?c s] Choice.prems True by auto
256+ have z: "executes64 ([15,132] @ octets 4 (length (flowbytes a) + 5) @
257+ (flowbytes a @ [233] @ octets 4 (length (flowbytes b)) @ flowbytes b)) ?c d"
258+ using d(1) limits True by (intro executes64.zero) auto
259+ have "executes64 (microbytes (Test Rax) @ ([15,132] @ octets 4 (length (flowbytes a) + 5) @
260+ (flowbytes a @ [233] @ octets 4 (length (flowbytes b)) @ flowbytes b))) c d"
261+ using test z by (intro executes64.advance) auto
262+ then show ?thesis using d(2) by auto
263+ next
264+ case False
265+ obtain d where d: "executes64 (flowbytes a) ?c d" "state64 d = s"
266+ using Choice.IH(1)[of ?c s] Choice.prems False by auto
267+ have skip: "executes64 ([233] @ octets 4 (length (flowbytes b)) @ flowbytes b) d d"
268+ using limits(2) by (intro executes64.jump) (auto intro: executes64.empty)
269+ have z: "executes64 ([15,132] @ octets 4 (length (flowbytes a) + 5) @
270+ (flowbytes a @ [233] @ octets 4 (length (flowbytes b)) @ flowbytes b)) ?c d"
271+ using executes64_append[OF d(1) skip] limits False
272+ by (intro executes64.nonzero) auto
273+ have "executes64 (microbytes (Test Rax) @ ([15,132] @ octets 4 (length (flowbytes a) + 5) @
274+ (flowbytes a @ [233] @ octets 4 (length (flowbytes b)) @ flowbytes b))) c d"
275+ using test z by (intro executes64.advance) auto
276+ then show ?thesis using d(2) by auto
277+ qed
278+qed
279+
280+theorem compiled_execution:
281+ assumes "scoped 0 e" "flowvalid (branching e)"
282+ shows "\<exists>d. executes64 (flowbytes (branching e)) c d \<and>
283+ registers (state64 d) Rax = evaluate e [] (inputs (state64 c)) \<and>
284+ stack (state64 d) = stack (state64 c) \<and> inputs (state64 d) = inputs (state64 c) \<and>
285+ pointer64 d = pointer64 c"
286+proof -
287+ obtain s where s: "flowrun (branching e) (state64 c) = Some s"
288+ "registers s Rax = evaluate e [] (inputs (state64 c))"
289+ "stack s = stack (state64 c)" "inputs s = inputs (state64 c)"
290+ using branching_return[OF assms(1), of "state64 c"] by blast
291+ obtain d where d: "executes64 (flowbytes (branching e)) c d" "state64 d = s"
292+ using executes64_flow[OF assms(2) s(1)] by blast
293+ have "pointer64 d = pointer64 c"
294+ using executes64_top[OF d(1)] d(2) s(3) by (simp add: top64_def)
295+ then show ?thesis using d s by blast
296+qed
297+
298+definition ret64 :: "processor \<Rightarrow> (pixel \<times> processor) option" where
299+ "ret64 c = (case stack (state64 c) of [] \<Rightarrow> None | address # rest \<Rightarrow>
300+ Some (address,c\<lparr>state64 := (state64 c)\<lparr>stack := rest\<rparr>, pointer64 := pointer64 c + 8\<rparr>))"
301+
302+definition returns64 :: "nat list \<Rightarrow> processor \<Rightarrow> pixel \<Rightarrow> processor \<Rightarrow> bool" where
303+ "returns64 bytes c address d \<longleftrightarrow> (\<exists>body q. bytes = body @ [195] \<and>
304+ executes64 body c q \<and> ret64 q = Some (address,d))"
305+
306+theorem compiled_return:
307+ assumes "scoped 0 e" "flowvalid (branching e)" "stack (state64 c) = address # rest"
308+ shows "\<exists>d. returns64 (flowbytes (branching e) @ [195]) c address d \<and>
309+ registers (state64 d) Rax = evaluate e [] (inputs (state64 c)) \<and>
310+ stack (state64 d) = rest \<and> inputs (state64 d) = inputs (state64 c) \<and>
311+ pointer64 d = pointer64 c + 8"
312+proof -
313+ obtain q where q: "executes64 (flowbytes (branching e)) c q"
314+ "registers (state64 q) Rax = evaluate e [] (inputs (state64 c))"
315+ "stack (state64 q) = stack (state64 c)" "inputs (state64 q) = inputs (state64 c)"
316+ "pointer64 q = pointer64 c"
317+ using compiled_execution[OF assms(1,2), of c] by blast
318+ let ?d = "q\<lparr>state64 := (state64 q)\<lparr>stack := rest\<rparr>, pointer64 := pointer64 q + 8\<rparr>"
319+ have ret: "ret64 q = Some (address,?d)"
320+ using q(3) assms(3) by (simp add: ret64_def)
321+ have "returns64 (flowbytes (branching e) @ [195]) c address ?d"
322+ using q(1) ret by (auto simp: returns64_def)
323+ then show ?thesis using q by auto
324+qed
325+
326+function simulate64 :: "nat \<Rightarrow> nat list \<Rightarrow> processor \<Rightarrow> processor option" where
327+ "simulate64 0 bytes c = None"
328+| "simulate64 (Suc fuel) bytes c = (if bytes = [] then None else
329+ if bytes = [195] then map_option snd (ret64 c) else
330+ if take 1 bytes = [233] then let n = integer (take 4 (drop 1 bytes)) in
331+ if 5 \<le> length bytes \<and> n < 2 ^ 31 \<and> n \<le> length bytes - 5
332+ then simulate64 fuel (drop (5+n) bytes) c else None
333+ else if take 2 bytes = [15,132] then let n = integer (take 4 (drop 2 bytes)) in
334+ if 6 \<le> length bytes \<and> n < 2 ^ 31 \<and> n \<le> length bytes - 6 then
335+ (case zero64 c of None \<Rightarrow> None | Some flag \<Rightarrow>
336+ simulate64 fuel (drop (6 + (if flag then n else 0)) bytes) c)
337+ else None
338+ else Option.bind (decode64 bytes) (\<lambda>(i,rest).
339+ if microvalid i then Option.bind (microstep i c) (simulate64 fuel rest) else None))"
340+ by pat_completeness auto
341+termination by (relation "measure (\<lambda>(fuel,bytes,c). fuel)") auto
342+
343+declare simulate64.simps [simp del]
344+
345+end

tests/cli.py modified

@@ -25,6 +25,9 @@ def main():
2525 assert int(invoke('eval',source,'0','0','0')) == expected, text
2626 source.write_text('(+ x y)')
2727 assert int(invoke('eval',source,'0xFF','0x1','0x0')) == 256
28+ invoke(source,binary)
29+ assert int(invoke('simulate',binary,'0xFF','0x1','0x0')) == 256
30+ invoke('simulate',binary,'invalid','0','0',ok=False)
2831 source.write_text('(let x1 7 (let x1 (+ x1 2) (* x1 x1)))')
2932 assert int(invoke('eval',source,'0','0','0')) == 81
3033 source.write_text('(let 1x 3 1x)')

tests/native.py modified

@@ -169,6 +169,9 @@ def main():
169169 result = subprocess.run([ROOT / ".build/remy", "eval", path, str(x), str(y), str(t)],
170170 capture_output=True, text=True, timeout=30)
171171 assert result.returncode == 0 and int(result.stdout) == expected, (case, result.stdout, result.stderr)
172+ simulated = subprocess.run([ROOT / '.build/remy', 'simulate', binary, str(x), str(y), str(t)],
173+ capture_output=True, text=True, timeout=30)
174+ assert simulated.returncode == 0 and int(simulated.stdout) == expected, (case, simulated.stdout, simulated.stderr)
172175 for bad in ("", "(+ x)", "(+ x y) 1", "(let a 3 b)", "(if 1 2)", "(let if 3 4)",
173176 "18446744073709551616", "(+ x z)", "(div x y)", "é", " " * 65537):
174177 path.write_text(bad)