From 31d281ada88d2822fbbece49ea5e511b0ad3ada3 Mon Sep 17 00:00:00 2001 From: james Date: Wed, 21 Oct 2026 12:00:00 +0100 Subject: [PATCH] feat(checker): validate native stack and register effects --- ROOT | 1 + cli/driver.ML | 3 ++- src/Checker.thy | 66 ++++++++++++++++++++++++++++++++++++++++++++++++ src/Export.thy | 2 +- src/Frontend.thy | 9 ++++++- tests/cli.py | 8 ++++++ tests/native.py | 2 ++ 7 files changed, 88 insertions(+), 3 deletions(-) create mode 100644 src/Checker.thy diff --git a/ROOT b/ROOT index a98b048..8c8ff30 100644 --- a/ROOT +++ b/ROOT @@ -13,6 +13,7 @@ session Remy in src = Remybase + Compiler Native Encoding + Checker Frontend Examples Export diff --git a/cli/driver.ML b/cli/driver.ML index 2f10cbf..3268121 100644 --- a/cli/driver.ML +++ b/cli/driver.ML @@ -36,9 +36,10 @@ fun main () = | ["eval", source, x, y, t] => output (Remy.reference (read source) (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)) | [source, destination] => emit destination (Remy.artifact (read source)) - | _ => raise Fail "usage: remy disassemble binary | remy limits depth nodes stack source binary | remy source binary | remy vectors source data | remy eval source x y t") + | _ => raise Fail "usage: remy check binary | remy disassemble binary | remy limits depth nodes stack source binary | remy source binary | remy vectors source data | remy eval source x y t") handle exn => (TextIO.output (TextIO.stdErr, "remy: " ^ General.exnMessage exn ^ "\n"); OS.Process.exit OS.Process.failure); diff --git a/src/Checker.thy b/src/Checker.thy new file mode 100644 index 0000000..6393f0d --- /dev/null +++ b/src/Checker.thy @@ -0,0 +1,66 @@ +theory Checker + imports Encoding +begin + +fun effect :: "opcode \ nat \ nat option" where + "effect (Push r) n = Some (Suc n)" +| "effect (Pop r) n = (if n = 0 then None else Some (n - 1))" +| "effect (Peek i) n = (if i < n then Some n else None)" +| "effect _ n = Some n" + +fun audit :: "opcode list \ nat \ nat option" where + "audit [] n = Some n" +| "audit (op # code) n = (if writes op \ {Rax,Rcx,Rbx} then + Option.bind (effect op n) (\m. if m \ 512 then audit code m else None) else None)" + +lemma effect_sound: + "effect op (length (stack s)) = Some n \ + \t. transition op s = Some t \ length (stack t) = n" + by (cases op; cases "stack s") (auto split: if_splits) + +theorem audit_sound: + "audit code (length (stack s)) = Some n \ + \t. run code s = Some t \ length (stack t) = n" +proof (induction code arbitrary: s) + case Nil + then show ?case by simp +next + case (Cons op code) + then show ?case + by (auto dest!: effect_sound split: if_splits bind_splits; fastforce) +qed + +lemma audit_scratch: + "audit code n = Some m \ list_all (\op. writes op \ {Rax,Rcx,Rbx}) code" + by (induction code arbitrary: n) (auto split: if_splits bind_splits) + +theorem audit_inputs: + "audit code n = Some m \ run code s = Some t \ inputs t = inputs s" +proof - + assume audited: "audit code n = Some m" and ran: "run code s = Some t" + have scratch: "list_all (\op. writes op \ {Rax,Rcx,Rbx}) code" + using audit_scratch[OF audited] . + show ?thesis + proof (rule ext) + fix i + have keep: "list_all (\op. input_register i \ writes op) code" + unfolding list_all_iff + proof (rule ballI) + fix op + assume member: "op \ set code" + have bound: "writes op \ {Rax,Rcx,Rbx}" + using scratch member by (auto simp: list_all_iff) + show "input_register i \ writes op" + proof + assume written: "input_register i \ writes op" + have "input_register i \ {Rax,Rcx,Rbx}" + using subsetD[OF bound written] . + then show False by simp + qed + qed + show "inputs t i = inputs s i" + unfolding inputs_def using run_preserves[OF ran keep] . + qed +qed + +end diff --git a/src/Export.thy b/src/Export.thy index fd1a9cf..59645e5 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 disassemble configured artifact vectors reference ascii ordinal in SML module_name Remy file_prefix remy +export_code validate disassemble configured artifact vectors reference ascii ordinal in SML module_name Remy file_prefix remy end diff --git a/src/Frontend.thy b/src/Frontend.thy index a535f2e..6736bff 100644 --- a/src/Frontend.thy +++ b/src/Frontend.thy @@ -1,5 +1,5 @@ theory Frontend - imports Encoding + imports Checker begin fun finish :: "string \ string list \ string list" where @@ -208,6 +208,13 @@ definition disassemble :: "string \ bool \ string" where None \ (False,''invalid native block stream'' @ newline) | Some code \ (True,listing 0 code))" +definition validate :: "string \ bool \ string" where + "validate bytes = (case blocks (map nat_of_char bytes) of + None \ (False,''invalid native block stream'' @ newline) + | Some code \ if audit (map snd code) 0 = Some 0 + then (True,''native stack and register effects verified'' @ newline) + else (False,''invalid native stack or register effects'' @ newline))" + datatype problem = Unexpected nat | Exhausted nat datatype 'a outcome = Failed problem | Parsed 'a diff --git a/tests/cli.py b/tests/cli.py index fc34f66..4aa2a9a 100644 --- a/tests/cli.py +++ b/tests/cli.py @@ -55,6 +55,14 @@ def main(): assert 'invalid native' in invoke('disassemble',binary,ok=False) binary.write_bytes(bytes([72,184,42,0,0,0,0,0,0,0,195])) assert '10 ret' in invoke('disassemble',binary) + source.write_text('(+ x y)') + invoke(source,binary) + assert 'verified' in invoke('check',binary) + for code in [[88,195],[80,195],[65,88,195],[73,137,192,195],[72,139,68,36,0,195]]: + binary.write_bytes(bytes(code)) + invoke('check',binary,ok=False) + binary.write_bytes(bytes([72,199,192,42,0,0,0,195])) + invoke('check',binary) source.write_text('é') assert 'ASCII' in invoke(source,binary,ok=False) for text in ['0x','0x10000000000000000','0xfg','0xffextra','-0x1']: diff --git a/tests/native.py b/tests/native.py index c1d9b81..d58553a 100644 --- a/tests/native.py +++ b/tests/native.py @@ -80,6 +80,8 @@ def main(): path.write_text(source(case)) result = subprocess.run([ROOT / ".build/remy", path, binary], capture_output=True, text=True, timeout=30) assert result.returncode == 0, (case, result.stderr) + checked = subprocess.run([ROOT / ".build/remy", "check", binary],capture_output=True,text=True,timeout=30) + assert checked.returncode == 0, (case,checked.stderr) function, image, thunk = native(binary.read_bytes()) vectors = [(a, b, a ^ b) for a in (0, 1, MASK, 1 << 63) for b in (0, 1, 63, 64, 65, MASK)] vectors += [tuple(rng.getrandbits(64) for _ in range(3)) for _ in range(24)]