From 7cb596d931d773db10cc8df8c329cd8b881a8826 Mon Sep 17 00:00:00 2001 From: james Date: Sun, 1 Nov 2026 03:54:53 +0000 Subject: [PATCH] feat(x86): prove emitted instruction execution and return-frame consumption --- README.md | 24 ++- ROOT | 1 + cli/driver.ML | 3 +- media/correspondence.svg | 16 +- src/Export.thy | 2 +- src/Frontend.thy | 31 +++- src/X86.thy | 345 +++++++++++++++++++++++++++++++++++++++ tests/cli.py | 3 + tests/native.py | 3 + 9 files changed, 415 insertions(+), 13 deletions(-) create mode 100644 src/X86.thy diff --git a/README.md b/README.md index 188efcb5b4663de15f04e37678de85c556895362..c515edd48286b13442473c0607d5e412ae01c633 100644 --- a/README.md +++ b/README.md @@ -21,11 +21,29 @@ Verify; Show(0); ``` +## Usage + +The byte interpreter follows encoded jumps and consumes a synthetic return address through `ret`. Compare its result with `eval` using the same `x`, `y` and `t` arguments + +```sh +.build/remy examples/Rings.remy /tmp/rings.bin +.build/remy simulate /tmp/rings.bin 17 23 41 +.build/remy eval examples/Rings.remy 17 23 41 +``` + +Both evaluations return `3`. `make measure` compares the original stack backend with the current compiler on the three examples and reports bytes, static stack instructions and median host pixel-kernel time + ## Correctness -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 +Lexical bindings share the evaluation stack with spilled intermediates. The [allocator](src/Allocation.thy) keeps one intermediate in a register and adjusts variable offsets when it must spill, while the [branching compiler](src/Branches.thy) preserves the incoming frame and returns the expression result + +The [encoder](src/core/Encoding.thy) proves inversion and byte bounds for immediate operands and stack displacements, while [native lowering](src/core/Native.thy) uses the following register convention to keep pixel inputs available across expression evaluation -[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 +| Registers | Role | +| --- | --- | +| `r8`, `r9`, `rdx` | Preserved inputs `x`, `y`, `t` | +| `rax` | Accumulator and result | +| `rcx`, `rbx` | Scratch | ![Source eval](media/correspondence.svg) @@ -33,4 +51,4 @@ 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 -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 +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 0e36e1419179a51b3d2f269411465f31a7aabe4d..92a76532e7c711e315e098c7e0f4e58c6f9bd4bf 100644 --- a/ROOT +++ b/ROOT @@ -16,6 +16,7 @@ session Remy in src = Remybase + theories Allocation Branches + X86 Frontend Examples Export diff --git a/cli/driver.ML b/cli/driver.ML index a6fdd8790a436ed4f8ec9eef28e19ca34e1201a7..e8be8fd5fa81ef57f04d6170741089525beff158 100644 --- a/cli/driver.ML +++ b/cli/driver.ML @@ -67,13 +67,14 @@ fun main () = ["vectors", source, destination] => (case Remy.vectors (read source) of (true, bytes) => write destination bytes | result => output result) | ["eval", source, x, y, t] => output (Remy.reference (read source) (chars x) (chars y) (chars t)) + | ["simulate", binary, x, y, t] => output (Remy.simulate (read binary) (chars x) (chars y) (chars t)) | ["limits", depth, nodes, stack, source, destination] => emit destination (Remy.configured (chars depth) (chars nodes) (chars stack) (read source)) | ["check", binary] => output (Remy.validate (read binary)) | ["disassemble", binary] => output (Remy.disassemble (read binary)) | ["baseline", source, destination] => emit destination (Remy.baseline (read source)) | [source, destination] => emit destination (Remy.artifact (read source)) - | _ => raise Fail "usage: remy check binary | remy disassemble binary | remy 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 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/media/correspondence.svg b/media/correspondence.svg index 1357050668b8807494654cf280bb86a60fe2bb36..89ae8eb1c83340be4f2d1ffe567ad9fcf33896fb 100644 --- a/media/correspondence.svg +++ b/media/correspondence.svg @@ -1,17 +1,19 @@ - + + Compiler execution correspondence + Source evaluation agrees with instruction execution of emitted bytes, with RAX containing the result and the caller frame preserved - - + + - + expression64-bit value - x86 blocksRAX + stack - source evaluationnative block execution - optimisation + lexical slots + encoding + emitted bytesRAX + frame + source evaluationx86 instruction execution + folding · allocation · branches · encoding diff --git a/src/Export.thy b/src/Export.thy index fc998bf86c76156cb000a945530ba76398fa910a..4b69ac7e259821093b04659c8eb2ccb3131407ac 100644 --- a/src/Export.thy +++ b/src/Export.thy @@ -6,6 +6,6 @@ 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 ascii ordinal in SML module_name Remy file_prefix remy +export_code validate disassemble configured artifact baseline vectors reference simulate ascii ordinal in SML module_name Remy file_prefix remy end diff --git a/src/Frontend.thy b/src/Frontend.thy index fd912c04c4f8f479eedf8bcb53bbaa009eafe5f6..85a45e29905dfe59afc39c276d0f0ab732b88771 100644 --- a/src/Frontend.thy +++ b/src/Frontend.thy @@ -1,5 +1,5 @@ theory Frontend - imports Branches + imports X86 begin fun finish :: "string \ string list \ string list" where @@ -303,6 +303,20 @@ definition source_error :: "string \ string" where definition artifact :: "string \ (bool \ string) \ string" where "artifact = artifact_with defaults" +theorem artifact_execution: + assumes "artifact source = ((True,bytes),report)" + shows "\e d. prepare source = Some e \ + bytes = map char_of_nat (flowbytes (branching e) @ [195]) \ + executes64 (flowbytes (branching e)) c d \ + registers (state64 d) Rax = evaluate e [] (inputs (state64 c)) \ + stack (state64 d) = stack (state64 c) \ inputs (state64 d) = inputs (state64 c)" +proof - + obtain e where e: "prepare source = Some e" "flowvalid (branching e)" + "bytes = map char_of_nat (flowbytes (branching e) @ [195])" + using assms by (auto simp: artifact_def artifact_with_def prepare_def Let_def split: option.splits if_splits) + show ?thesis using compiled_execution[OF prepare_scoped[OF e(1)] e(2), of c] e by blast +qed + definition baseline :: "string \ (bool \ string) \ string" where "baseline s = (case prepare s of None \ ((False,[]),source_error s) | Some e \ ((True,map char_of_nat (executable e)),''stack backend'' @ newline))" @@ -333,4 +347,19 @@ definition reference :: "string \ string \ string \v. word_of_nat (case v of X \ a | Y \ b | T \ c)))) @ newline) | _ \ (False,''invalid input'' @ newline))" +definition initial64 :: "nat \ nat \ nat \ processor" where + "initial64 x y t = \state64 = \registers = (\r. word_of_nat + (if r = R8 then x else if r = R9 then y else if r = Rdx then t else 0)), stack = [0]\, + pointer64 = 65536, zero64 = None, carry64 = None\" + +definition simulate :: "string \ string \ string \ string \ bool \ string" where + "simulate code x y t = (if \ fst (validate code) then (False,''invalid native image'' @ newline) else + case (number x,number y,number t) of (Some a,Some b,Some c) \ + (case simulate64 (Suc (length code)) (map nat_of_char code) (initial64 a b c) of + None \ (False,''unsupported or incomplete x86 execution'' @ newline) + | Some q \ if stack (state64 q) = [] + then (True,decimal (unat (registers (state64 q) Rax)) @ newline) + else (False,''return frame was not consumed'' @ newline)) + | _ \ (False,''invalid input'' @ newline))" + end diff --git a/src/X86.thy b/src/X86.thy new file mode 100644 index 0000000000000000000000000000000000000000..454f33e357f4cb0ff93cfd7708ea4af448e342fc --- /dev/null +++ b/src/X86.thy @@ -0,0 +1,345 @@ +theory X86 + imports Branches +begin + +datatype micro = Imm64 pixel | Imm32 pixel | Copy register register | Save register | Restore register + | Load nat | Alu operator | Exchange | Compare | Below | Extend | Test register | Select + +record processor = + state64 :: machine + pointer64 :: pixel + zero64 :: "bool option" + carry64 :: "bool option" + +definition put64 :: "register \ pixel \ processor \ processor" where + "put64 r v c = c\state64 := (state64 c)\registers := (registers (state64 c))(r := v)\\" + +fun microstep :: "micro \ processor \ processor option" where + "microstep (Imm64 v) c = Some (put64 Rax v c)" +| "microstep (Imm32 v) c = Some (put64 Rax v c)" +| "microstep (Copy dst src) c = Some (put64 dst (registers (state64 c) src) c)" +| "microstep (Save r) c = Some (c\state64 := (state64 c)\stack := registers (state64 c) r # stack (state64 c)\, + pointer64 := pointer64 c - 8\)" +| "microstep (Restore r) c = (case stack (state64 c) of [] \ None | v # vs \ + Some ((put64 r v c)\state64 := (state64 (put64 r v c))\stack := vs\, pointer64 := pointer64 c + 8\))" +| "microstep (Load i) c = (if i < length (stack (state64 c)) + then Some (put64 Rax (stack (state64 c) ! i) c) else None)" +| "microstep (Alu op) c = (if op = Less then None else + Some ((put64 Rax (operate op (registers (state64 c) Rax) (registers (state64 c) Rcx)) c) + \zero64 := None, carry64 := None\))" +| "microstep Exchange c = Some (put64 Rcx (registers (state64 c) Rax) + (put64 Rax (registers (state64 c) Rcx) c))" +| "microstep Compare c = Some (c\zero64 := Some (registers (state64 c) Rax = registers (state64 c) Rcx), + carry64 := Some (registers (state64 c) Rax < registers (state64 c) Rcx)\)" +| "microstep Below c = (case carry64 c of None \ None | Some flag \ + Some (put64 Rax ((registers (state64 c) Rax AND NOT 255) OR (if flag then 1 else 0)) c))" +| "microstep Extend c = Some (put64 Rax (registers (state64 c) Rax AND 255) c)" +| "microstep (Test r) c = Some (c\zero64 := Some (registers (state64 c) r = 0), carry64 := Some False\)" +| "microstep Select c = (case zero64 c of None \ None | Some flag \ + Some (if flag then c else put64 Rax (registers (state64 c) Rcx) c))" + +fun microrun :: "micro list \ processor \ processor option" where + "microrun [] c = Some c" +| "microrun (i # code) c = Option.bind (microstep i c) (microrun code)" + +lemma microrun_append: + "microrun (a @ b) c = Option.bind (microrun a c) (microrun b)" + by (induction a arbitrary: c) (auto split: option.splits bind_splits) + +fun microbytes :: "micro \ nat list" where + "microbytes (Imm64 v) = [72,184] @ octets 8 (unat v)" +| "microbytes (Imm32 v) = [72,199,192] @ octets 4 (unat v)" +| "microbytes (Copy dst src) = movecode dst src" +| "microbytes (Save r) = pushcode r" +| "microbytes (Restore r) = popcode r" +| "microbytes (Load i) = (if i < 16 then [72,139,68,36,8*i] + else [72,139,132,36] @ octets 4 (8*i))" +| "microbytes (Alu Add) = [72,1,200]" +| "microbytes (Alu Sub) = [72,41,200]" +| "microbytes (Alu Mul) = [72,15,175,193]" +| "microbytes (Alu And) = [72,33,200]" +| "microbytes (Alu Or) = [72,9,200]" +| "microbytes (Alu Xor) = [72,49,200]" +| "microbytes (Alu Shl) = [72,211,224]" +| "microbytes (Alu Shr) = [72,211,232]" +| "microbytes (Alu Less) = []" +| "microbytes Exchange = [72,145]" +| "microbytes Compare = [72,57,200]" +| "microbytes Below = [15,146,192]" +| "microbytes Extend = [72,15,182,192]" +| "microbytes (Test r) = [72,133,192 + 9 * regno r]" +| "microbytes Select = [72,15,69,193]" + +fun microvalid :: "micro \ bool" where + "microvalid (Imm32 v) = (extend32 (unat v) = v)" +| "microvalid (Load i) = (i < 2 ^ 28)" +| "microvalid (Alu Less) = False" +| "microvalid (Test r) = (r = Rax \ r = Rbx)" +| "microvalid _ = True" + +fun expand :: "opcode \ micro list" where + "expand (Immediate v) = [if extend32 (unat v) = v then Imm32 v else Imm64 v]" +| "expand (Push r) = [Save r]" +| "expand (Pop r) = [Restore r]" +| "expand (Move dst src) = [Copy dst src]" +| "expand (Peek i) = [Load i]" +| "expand (Arithmetic op) = (if op = Less then [Exchange,Compare,Below,Extend] + else if exchanges op then [Exchange,Alu op] else [Alu op])" +| "expand Conditional = [Test Rbx,Select]" + +lemma byte_register: + "((v AND NOT 255) OR (if flag then 1 else 0)) AND 255 = (if flag then 1 else 0 :: pixel)" + by (cases flag) (simp_all add: word_ao_dist word_bw_assocs) + +theorem expand_state: + "map_option state64 (microrun (expand op) c) = transition op (state64 c)" +proof (cases op) + case (Arithmetic f) + then show ?thesis + by (cases f) + (auto simp: put64_def byte_register word_ao_dist2 word_ao_dist word_bw_assocs ac_simps split: option.splits) +next + case (Pop r) + then show ?thesis by (cases "stack (state64 c)") (auto simp: put64_def) +qed (auto simp: put64_def split: if_splits option.splits) + +theorem expand_bytes: + "concat (map microbytes (expand op)) = encode op" +proof (cases op) + case (Arithmetic f) + then show ?thesis by (cases f) auto +qed auto + +lemma expand_valid: + "encodable op \ list_all microvalid (expand op)" +proof (cases op) + case (Arithmetic f) + then show ?thesis by (cases f) auto +qed auto + +theorem expand_run: + "map_option state64 (microrun (concat (map expand code)) c) = run code (state64 c)" +proof (induction code arbitrary: c) + case Nil + then show ?case by simp +next + case (Cons op code) + then show ?case using expand_state[of op c] + by (auto simp: microrun_append split: option.splits bind_splits) +qed + +definition top64 :: "processor \ pixel" where + "top64 c = pointer64 c + 8 * of_nat (length (stack (state64 c)))" + +lemma microstep_top: + "microstep i c = Some d \ top64 d = top64 c" + by (cases i) + (auto simp: top64_def put64_def algebra_simps split: list.splits if_splits option.splits) + +definition fixed64 :: "micro list" where + "fixed64 = map Save [Rax,Rcx,Rbx,Rdx,R8,R9] @ map Restore [Rax,Rcx,Rbx,Rdx,R8,R9] @ + concat (map (\dst. map (Copy dst) [Rax,Rcx,Rbx,Rdx,R8,R9]) [Rax,Rcx,Rbx,Rdx,R8,R9]) @ + map Alu [Add,Sub,Mul,And,Or,Xor,Shl,Shr] @ [Exchange,Compare,Below,Extend,Test Rax,Test Rbx,Select]" + +definition decode64 :: "nat list \ (micro \ nat list) option" where + "decode64 bs = (if take 2 bs = [72,184] then + if 10 \ length bs then Some (Imm64 (word_of_nat (integer (take 8 (drop 2 bs)))),drop 10 bs) else None + else if take 3 bs = [72,199,192] then + if 7 \ length bs then Some (Imm32 (extend32 (integer (take 4 (drop 3 bs)))),drop 7 bs) else None + else if take 4 bs = [72,139,68,36] then + let n = integer (take 1 (drop 4 bs)) in + if 5 \ length bs \ n < 128 \ n mod 8 = 0 then Some (Load (n div 8),drop 5 bs) else None + else if take 4 bs = [72,139,132,36] then + let n = integer (take 4 (drop 4 bs)) in + if 8 \ length bs \ n mod 8 = 0 \ n div 8 < 2 ^ 28 + then Some (Load (n div 8),drop 8 bs) else None + else map_option (\i. (i,drop (length (microbytes i)) bs)) + (List.find (\i. take (length (microbytes i)) bs = microbytes i) fixed64))" + +theorem decode64_encode: + assumes "microvalid i" + shows "decode64 (microbytes i @ tail) = Some (i,tail)" +proof (cases i) + case (Imm64 v) + then show ?thesis by (simp add: decode64_def) +next + case (Imm32 v) + then show ?thesis using assms by (simp add: decode64_def) +next + case (Copy dst src) + then show ?thesis by (cases dst; cases src) (simp_all add: decode64_def fixed64_def movecode_def) +next + case (Save r) + then show ?thesis by (cases r) (simp_all add: decode64_def fixed64_def) +next + case (Restore r) + then show ?thesis by (cases r) (simp_all add: decode64_def fixed64_def) +next + case (Load n) + then show ?thesis using assms peek_bound[of n] + by (auto simp: decode64_def integer_octets Let_def) +next + case (Alu op) + then show ?thesis using assms by (cases op) (simp_all add: decode64_def fixed64_def movecode_def) +next + case (Test r) + then show ?thesis using assms by (cases r) (simp_all add: decode64_def fixed64_def movecode_def) +qed (simp_all add: decode64_def fixed64_def movecode_def) + +inductive executes64 :: "nat list \ processor \ processor \ bool" where + empty: "executes64 [] c c" +| advance: "microvalid i \ microstep i c = Some d \ executes64 tail d e \ + executes64 (microbytes i @ tail) c e" +| jump: "n < 2 ^ 31 \ n \ length tail \ executes64 (drop n tail) c d \ + executes64 ([233] @ octets 4 n @ tail) c d" +| zero: "n < 2 ^ 31 \ n \ length tail \ zero64 c = Some True \ + executes64 (drop n tail) c d \ executes64 ([15,132] @ octets 4 n @ tail) c d" +| nonzero: "n < 2 ^ 31 \ zero64 c = Some False \ executes64 tail c d \ + executes64 ([15,132] @ octets 4 n @ tail) c d" + +lemma executes64_append: + "executes64 a c d \ executes64 b d e \ executes64 (a @ b) c e" + by (induction a c d rule: executes64.induct) + (auto simp: drop_append intro: executes64.intros[simplified]) + +lemma executes64_micro: + "list_all microvalid code \ microrun code c = Some d \ + executes64 (concat (map microbytes code)) c d" + by (induction code arbitrary: c) (auto split: option.splits bind_splits intro: executes64.intros) + +lemma executes64_top: + "executes64 code c d \ top64 d = top64 c" + by (induction rule: executes64.induct) (auto dest: microstep_top) + +theorem executes64_native: + "list_all encodable code \ run code (state64 c) = Some s \ + \d. executes64 (concat (map encode code)) c d \ state64 d = s" +proof - + assume valid: "list_all encodable code" and ran: "run code (state64 c) = Some s" + obtain d where d: "microrun (concat (map expand code)) c = Some d" "state64 d = s" + using expand_run[of code c] ran by (auto split: option.splits) + have safe: "list_all microvalid (concat (map expand code))" + using valid expand_valid by (auto simp: list_all_iff) + have bytes: "concat (map microbytes (concat (map expand code))) = concat (map encode code)" + using expand_bytes by (induction code) auto + show ?thesis using executes64_micro[OF safe d(1)] d(2) bytes by auto +qed + + +theorem executes64_flow: + assumes "flowvalid code" "flowrun code (state64 c) = Some s" + shows "\d. executes64 (flowbytes code) c d \ state64 d = s" + using assms +proof (induction code arbitrary: c s) + case (Basic code) + then show ?case using executes64_native by fastforce +next + case (Sequence a b) + obtain m where a: "flowrun a (state64 c) = Some m" and b: "flowrun b m = Some s" + using Sequence.prems by (auto split: bind_splits) + obtain d where d: "executes64 (flowbytes a) c d" "state64 d = m" + using Sequence.IH(1) Sequence.prems a by auto + obtain e where e: "executes64 (flowbytes b) d e" "state64 e = s" + using Sequence.IH(2) Sequence.prems b d by auto + show ?case using executes64_append[OF d(1) e(1)] e(2) by auto +next + case (Choice a b) + let ?c = "c\zero64 := Some (registers (state64 c) Rax = 0), carry64 := Some False\" + have test: "microstep (Test Rax) c = Some ?c" by simp + have limits: "length (flowbytes a) + 5 < 2 ^ 31" "length (flowbytes b) < 2 ^ 31" + using Choice.prems by auto + show ?case + proof (cases "registers (state64 c) Rax = 0") + case True + obtain d where d: "executes64 (flowbytes b) ?c d" "state64 d = s" + using Choice.IH(2)[of ?c s] Choice.prems True by auto + have z: "executes64 ([15,132] @ octets 4 (length (flowbytes a) + 5) @ + (flowbytes a @ [233] @ octets 4 (length (flowbytes b)) @ flowbytes b)) ?c d" + using d(1) limits True by (intro executes64.zero) auto + have "executes64 (microbytes (Test Rax) @ ([15,132] @ octets 4 (length (flowbytes a) + 5) @ + (flowbytes a @ [233] @ octets 4 (length (flowbytes b)) @ flowbytes b))) c d" + using test z by (intro executes64.advance) auto + then show ?thesis using d(2) by auto + next + case False + obtain d where d: "executes64 (flowbytes a) ?c d" "state64 d = s" + using Choice.IH(1)[of ?c s] Choice.prems False by auto + have skip: "executes64 ([233] @ octets 4 (length (flowbytes b)) @ flowbytes b) d d" + using limits(2) by (intro executes64.jump) (auto intro: executes64.empty) + have z: "executes64 ([15,132] @ octets 4 (length (flowbytes a) + 5) @ + (flowbytes a @ [233] @ octets 4 (length (flowbytes b)) @ flowbytes b)) ?c d" + using executes64_append[OF d(1) skip] limits False + by (intro executes64.nonzero) auto + have "executes64 (microbytes (Test Rax) @ ([15,132] @ octets 4 (length (flowbytes a) + 5) @ + (flowbytes a @ [233] @ octets 4 (length (flowbytes b)) @ flowbytes b))) c d" + using test z by (intro executes64.advance) auto + then show ?thesis using d(2) by auto + qed +qed + +theorem compiled_execution: + assumes "scoped 0 e" "flowvalid (branching e)" + shows "\d. executes64 (flowbytes (branching e)) c d \ + registers (state64 d) Rax = evaluate e [] (inputs (state64 c)) \ + stack (state64 d) = stack (state64 c) \ inputs (state64 d) = inputs (state64 c) \ + pointer64 d = pointer64 c" +proof - + obtain s where s: "flowrun (branching e) (state64 c) = Some s" + "registers s Rax = evaluate e [] (inputs (state64 c))" + "stack s = stack (state64 c)" "inputs s = inputs (state64 c)" + using branching_return[OF assms(1), of "state64 c"] by blast + obtain d where d: "executes64 (flowbytes (branching e)) c d" "state64 d = s" + using executes64_flow[OF assms(2) s(1)] by blast + have "pointer64 d = pointer64 c" + using executes64_top[OF d(1)] d(2) s(3) by (simp add: top64_def) + then show ?thesis using d s by blast +qed + +definition ret64 :: "processor \ (pixel \ processor) option" where + "ret64 c = (case stack (state64 c) of [] \ None | address # rest \ + Some (address,c\state64 := (state64 c)\stack := rest\, pointer64 := pointer64 c + 8\))" + +definition returns64 :: "nat list \ processor \ pixel \ processor \ bool" where + "returns64 bytes c address d \ (\body q. bytes = body @ [195] \ + executes64 body c q \ ret64 q = Some (address,d))" + +theorem compiled_return: + assumes "scoped 0 e" "flowvalid (branching e)" "stack (state64 c) = address # rest" + shows "\d. returns64 (flowbytes (branching e) @ [195]) c address d \ + registers (state64 d) Rax = evaluate e [] (inputs (state64 c)) \ + stack (state64 d) = rest \ inputs (state64 d) = inputs (state64 c) \ + pointer64 d = pointer64 c + 8" +proof - + obtain q where q: "executes64 (flowbytes (branching e)) c q" + "registers (state64 q) Rax = evaluate e [] (inputs (state64 c))" + "stack (state64 q) = stack (state64 c)" "inputs (state64 q) = inputs (state64 c)" + "pointer64 q = pointer64 c" + using compiled_execution[OF assms(1,2), of c] by blast + let ?d = "q\state64 := (state64 q)\stack := rest\, pointer64 := pointer64 q + 8\" + have ret: "ret64 q = Some (address,?d)" + using q(3) assms(3) by (simp add: ret64_def) + have "returns64 (flowbytes (branching e) @ [195]) c address ?d" + using q(1) ret by (auto simp: returns64_def) + then show ?thesis using q by auto +qed + +function simulate64 :: "nat \ nat list \ processor \ processor option" where + "simulate64 0 bytes c = None" +| "simulate64 (Suc fuel) bytes c = (if bytes = [] then None else + if bytes = [195] then map_option snd (ret64 c) else + if take 1 bytes = [233] then let n = integer (take 4 (drop 1 bytes)) in + if 5 \ length bytes \ n < 2 ^ 31 \ n \ length bytes - 5 + then simulate64 fuel (drop (5+n) bytes) c else None + else if take 2 bytes = [15,132] then let n = integer (take 4 (drop 2 bytes)) in + if 6 \ length bytes \ n < 2 ^ 31 \ n \ length bytes - 6 then + (case zero64 c of None \ None | Some flag \ + simulate64 fuel (drop (6 + (if flag then n else 0)) bytes) c) + else None + else Option.bind (decode64 bytes) (\(i,rest). + if microvalid i then Option.bind (microstep i c) (simulate64 fuel rest) else None))" + by pat_completeness auto +termination by (relation "measure (\(fuel,bytes,c). fuel)") auto + +declare simulate64.simps [simp del] + +end diff --git a/tests/cli.py b/tests/cli.py index 99ba91418644bcf23635c410a1cb4ff1a794f46a..9541bb31e71d9c7372c88a7bc4159482dd126f84 100644 --- a/tests/cli.py +++ b/tests/cli.py @@ -25,6 +25,9 @@ def main(): assert int(invoke('eval',source,'0','0','0')) == expected, text source.write_text('(+ x y)') assert int(invoke('eval',source,'0xFF','0x1','0x0')) == 256 + invoke(source,binary) + assert int(invoke('simulate',binary,'0xFF','0x1','0x0')) == 256 + invoke('simulate',binary,'invalid','0','0',ok=False) source.write_text('(let x1 7 (let x1 (+ x1 2) (* x1 x1)))') assert int(invoke('eval',source,'0','0','0')) == 81 source.write_text('(let 1x 3 1x)') diff --git a/tests/native.py b/tests/native.py index 1582bb182fecd133204321393c2f3d994f36dfb5..5ec3fe86770c2c9751d7012f774d43bc552d778a 100644 --- a/tests/native.py +++ b/tests/native.py @@ -169,6 +169,9 @@ def main(): result = subprocess.run([ROOT / ".build/remy", "eval", path, str(x), str(y), str(t)], capture_output=True, text=True, timeout=30) assert result.returncode == 0 and int(result.stdout) == expected, (case, result.stdout, result.stderr) + simulated = subprocess.run([ROOT / '.build/remy', 'simulate', binary, str(x), str(y), str(t)], + capture_output=True, text=True, timeout=30) + assert simulated.returncode == 0 and int(simulated.stdout) == expected, (case, simulated.stdout, simulated.stderr) for bad in ("", "(+ x)", "(+ x y) 1", "(let a 3 b)", "(if 1 2)", "(let if 3 4)", "18446744073709551616", "(+ x z)", "(div x y)", "é", " " * 65537): path.write_text(bad)