7 files changed, 88 insertions(+), 3 deletions(-)

M ROOT
M cli/driver.ML
A src/Checker.thy
M src/Export.thy
M src/Frontend.thy
M tests/cli.py
M tests/native.py

@@ 13,6 13,7 @@ session Remy in src = Remybase +
     Compiler
     Native
     Encoding
+    Checker
     Frontend
     Examples
     Export

@@ 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);

@@ 0,0 1,66 @@
+theory Checker
+  imports Encoding
+begin
+
+fun effect :: "opcode \<Rightarrow> nat \<Rightarrow> 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 \<Rightarrow> nat \<Rightarrow> nat option" where
+  "audit [] n = Some n"
+| "audit (op # code) n = (if writes op \<subseteq> {Rax,Rcx,Rbx} then
+    Option.bind (effect op n) (\<lambda>m. if m \<le> 512 then audit code m else None) else None)"
+
+lemma effect_sound:
+  "effect op (length (stack s)) = Some n \<Longrightarrow>
+    \<exists>t. transition op s = Some t \<and> length (stack t) = n"
+  by (cases op; cases "stack s") (auto split: if_splits)
+
+theorem audit_sound:
+  "audit code (length (stack s)) = Some n \<Longrightarrow>
+    \<exists>t. run code s = Some t \<and> 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 \<Longrightarrow> list_all (\<lambda>op. writes op \<subseteq> {Rax,Rcx,Rbx}) code"
+  by (induction code arbitrary: n) (auto split: if_splits bind_splits)
+
+theorem audit_inputs:
+  "audit code n = Some m \<Longrightarrow> run code s = Some t \<Longrightarrow> inputs t = inputs s"
+proof -
+  assume audited: "audit code n = Some m" and ran: "run code s = Some t"
+  have scratch: "list_all (\<lambda>op. writes op \<subseteq> {Rax,Rcx,Rbx}) code"
+    using audit_scratch[OF audited] .
+  show ?thesis
+  proof (rule ext)
+    fix i
+    have keep: "list_all (\<lambda>op. input_register i \<notin> writes op) code"
+      unfolding list_all_iff
+    proof (rule ballI)
+      fix op
+      assume member: "op \<in> set code"
+      have bound: "writes op \<subseteq> {Rax,Rcx,Rbx}"
+        using scratch member by (auto simp: list_all_iff)
+      show "input_register i \<notin> writes op"
+      proof
+        assume written: "input_register i \<in> writes op"
+        have "input_register i \<in> {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

@@ 6,6 6,6 @@ definition ascii :: "integer \<Rightarrow> char" where "ascii = char_of"
 
 definition ordinal :: "char \<Rightarrow> 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

@@ 1,5 1,5 @@
 theory Frontend
-  imports Encoding
+  imports Checker
 begin
 
 fun finish :: "string \<Rightarrow> string list \<Rightarrow> string list" where


@@ 208,6 208,13 @@ definition disassemble :: "string \<Rightarrow> bool \<times> string" where
     None \<Rightarrow> (False,''invalid native block stream'' @ newline)
     | Some code \<Rightarrow> (True,listing 0 code))"
 
+definition validate :: "string \<Rightarrow> bool \<times> string" where
+  "validate bytes = (case blocks (map nat_of_char bytes) of
+    None \<Rightarrow> (False,''invalid native block stream'' @ newline)
+    | Some code \<Rightarrow> 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

@@ 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']:

@@ 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)]