perf(native): eliminate adjacent stack transfers with verified moves

src/Encoding.thy

@@ -52,6 +52,14 @@ fun arithmetic :: "operator \<Rightarrow> nat list" where
 | "arithmetic Shr = [72,145,72,211,232]"
 | "arithmetic Less = [72,145,72,57,200,15,146,192,72,15,182,192]"
 
+fun regno :: "register \<Rightarrow> nat" where
+  "regno Rax = 0" | "regno Rcx = 1" | "regno Rdx = 2"
+| "regno Rbx = 3" | "regno R8 = 8" | "regno R9 = 9"
+
+definition movecode :: "register \<Rightarrow> register \<Rightarrow> nat list" where
+  "movecode dst src = [72 + (if regno src \<ge> 8 then 4 else 0) + (if regno dst \<ge> 8 then 1 else 0),
+    137, 192 + 8 * (regno src mod 8) + regno dst mod 8]"
+
 fun encode :: "opcode \<Rightarrow> nat list" where
   "encode (Immediate v) = [72,184] @ octets 8 (unat v)"
 | "encode (Push r) = pushcode r"
@@ -59,6 +67,7 @@ fun encode :: "opcode \<Rightarrow> nat list" where
 | "encode (Peek i) = [72,139,132,36] @ octets 4 (8 * i)"
 | "encode (Arithmetic op) = arithmetic op"
 | "encode Conditional = [72,133,219,72,15,69,193]"
+| "encode (Move dst src) = movecode dst src"
 
 fun encodable :: "opcode \<Rightarrow> bool" where
   "encodable (Peek i) = (i < 2 ^ 28)"
@@ -66,7 +75,8 @@ fun encodable :: "opcode \<Rightarrow> bool" where
 
 definition fixed :: "opcode list" where
   "fixed = map Push [Rax,Rcx,Rbx,Rdx,R8,R9] @ map Pop [Rax,Rcx,Rbx,Rdx,R8,R9] @
-    map Arithmetic [Add,Sub,Mul,And,Or,Xor,Shl,Shr,Less] @ [Conditional]"
+    map Arithmetic [Add,Sub,Mul,And,Or,Xor,Shl,Shr,Less] @ [Conditional] @
+    concat (map (\<lambda>dst. map (Move dst) [Rax,Rcx,Rbx,Rdx,R8,R9]) [Rax,Rcx,Rbx,Rdx,R8,R9])"
 
 definition decode :: "nat list \<Rightarrow> (opcode \<times> nat list) option" where
   "decode bs = (if take 2 bs = [72,184] then
@@ -111,6 +121,10 @@ next
 next
   case Conditional
   then show ?thesis by (simp add: decode_def fixed_def)
+next
+  case (Move dst src)
+  then show ?thesis by (cases dst; cases src) (simp_all add: decode_def fixed_def movecode_def)
+
 qed
 
 theorem encode_bytes: "set (encode op) \<subseteq> {..<256}"
@@ -132,6 +146,10 @@ next
 next
   case Conditional
   then show ?thesis by simp
+next
+  case (Move dst src)
+  then show ?thesis by (cases dst; cases src) (simp_all add: movecode_def)
+
 qed
 
 theorem encode_injective:
@@ -150,7 +168,7 @@ theorem recover_encode:
   by (induction ops) (simp_all add: decode_encode)
 
 definition executable :: "expression \<Rightarrow> nat list" where
-  "executable e = concat (map encode (native (compile (optimise e) []))) @ [88,195]"
+  "executable e = concat (map encode (program e)) @ [195]"
 
 theorem executable_bytes: "set (executable e) \<subseteq> {..<256}"
   unfolding executable_def using encode_bytes by auto

src/Examples.thy

@@ -57,7 +57,7 @@ lemma stack_bound_tight:
   by eval
 
 lemma literal_code:
-  "executable (Literal 42) = [72,184,42,0,0,0,0,0,0,0,80,88,195]"
+  "executable (Literal 42) = [72,184,42,0,0,0,0,0,0,0,195]"
   by eval
 
 lemma opcode_roundtrip:

src/Frontend.thy

@@ -144,6 +144,11 @@ lemma prepare_encodable:
   "prepare s = Some e \<Longrightarrow> list_all encodable (native (compile (optimise e) []))"
   by (auto simp: prepare_def prepare_with_def Let_def split: if_splits bind_splits prod.splits)
 
+lemma prepare_program:
+  "prepare s = Some e \<Longrightarrow> list_all encodable (program e)"
+  unfolding program_def using prepare_encodable
+  by (auto intro: transfers_property)
+
 theorem prepared_correct:
   "prepare source = Some e \<Longrightarrow>
     execute values (compile (optimise e) []) [] = Some [evaluate e [] values]"
@@ -157,9 +162,9 @@ theorem prepared_native:
 
 theorem prepared_bytes:
   "prepare source = Some e \<Longrightarrow>
-    recover (length (native (compile (optimise e) []))) (executable e) =
-    Some (native (compile (optimise e) []), [88,195])"
-  unfolding executable_def using recover_encode prepare_encodable by blast
+    recover (length (program e)) (executable e) =
+    Some (program e, [195])"
+  unfolding executable_def using recover_encode prepare_program by blast
 
 theorem prepared_stacks:
   "prepare source = Some e \<Longrightarrow>

src/Native.thy

@@ -5,7 +5,7 @@ begin
 datatype register = Rax | Rcx | Rbx | Rdx | R8 | R9
 
 datatype opcode = Immediate pixel | Push register | Pop register | Peek nat
-  | Arithmetic operator | Conditional
+  | Arithmetic operator | Conditional | Move register register
 
 record machine =
   registers :: "register \<Rightarrow> pixel"
@@ -38,6 +38,7 @@ fun transition :: "opcode \<Rightarrow> machine \<Rightarrow> machine option" wh
       Rax := operate op (registers s Rcx) (registers s Rax))\<rparr>)"
 | "transition Conditional s = Some (s\<lparr>registers :=
     (registers s)(Rax := if registers s Rbx = 0 then registers s Rax else registers s Rcx)\<rparr>)"
+| "transition (Move dst src) s = Some (s\<lparr>registers := (registers s)(dst := registers s src)\<rparr>)"
 
 fun run :: "opcode list \<Rightarrow> machine \<Rightarrow> machine option" where
   "run [] s = Some s"
@@ -142,6 +143,7 @@ qed
 fun writes :: "opcode \<Rightarrow> register set" where
   "writes (Immediate v) = {Rax}"
 | "writes (Pop r) = {r}"
+| "writes (Move dst src) = {dst}"
 | "writes (Peek i) = {Rax}"
 | "writes (Arithmetic op) = {Rax,Rcx}"
 | "writes Conditional = {Rax}"
@@ -160,4 +162,30 @@ lemma lower_scratch:
   "list_all (\<lambda>i. writes i \<subseteq> {Rax,Rcx,Rbx}) (lower op)"
   by (cases op) auto
 
+fun transfers :: "opcode list \<Rightarrow> opcode list" where
+  "transfers (Push src # Pop dst # code) =
+    (if src = dst then transfers code else Move dst src # transfers code)"
+| "transfers (op # code) = op # transfers code"
+| "transfers [] = []"
+
+theorem transfers_correct: "run (transfers code) s = run code s"
+  by (induction code arbitrary: s rule: transfers.induct)
+    (auto simp: fun_upd_idem split: if_splits option.splits bind_splits)
+
+lemma transfers_length: "length (transfers code) \<le> length code"
+  by (induction code rule: transfers.induct) auto
+
+lemma transfers_property:
+  "list_all P code \<Longrightarrow> (\<And>a b. P (Push a) \<Longrightarrow> P (Pop b) \<Longrightarrow> P (Move b a)) \<Longrightarrow>
+    list_all P (transfers code)"
+  by (induction code rule: transfers.induct) auto
+
+definition program :: "expression \<Rightarrow> opcode list" where
+  "program e = transfers (native (compile (optimise e) []) @ [Pop Rax])"
+
+theorem program_return:
+  "scoped 0 e \<Longrightarrow> \<exists>q. run (program e) s = Some q \<and>
+    registers q Rax = evaluate e [] (inputs s) \<and> stack q = stack s \<and> inputs q = inputs s"
+  unfolding program_def using native_return transfers_correct by metis
+
 end