theory X86
imports Bounds
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 \<Rightarrow> pixel \<Rightarrow> processor \<Rightarrow> processor" where
"put64 r v c = c\<lparr>state64 := (state64 c)\<lparr>registers := (registers (state64 c))(r := v)\<rparr>\<rparr>"
fun microstep :: "micro \<Rightarrow> processor \<Rightarrow> 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\<lparr>state64 := (state64 c)\<lparr>stack := registers (state64 c) r # stack (state64 c)\<rparr>,
pointer64 := pointer64 c - 8\<rparr>)"
| "microstep (Restore r) c = (case stack (state64 c) of [] \<Rightarrow> None | v # vs \<Rightarrow>
Some ((put64 r v c)\<lparr>state64 := (state64 (put64 r v c))\<lparr>stack := vs\<rparr>, pointer64 := pointer64 c + 8\<rparr>))"
| "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)
\<lparr>zero64 := None, carry64 := None\<rparr>))"
| "microstep Exchange c = Some (put64 Rcx (registers (state64 c) Rax)
(put64 Rax (registers (state64 c) Rcx) c))"
| "microstep Compare c = Some (c\<lparr>zero64 := Some (registers (state64 c) Rax = registers (state64 c) Rcx),
carry64 := Some (registers (state64 c) Rax < registers (state64 c) Rcx)\<rparr>)"
| "microstep Below c = (case carry64 c of None \<Rightarrow> None | Some flag \<Rightarrow>
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\<lparr>zero64 := Some (registers (state64 c) r = 0), carry64 := Some False\<rparr>)"
| "microstep Select c = (case zero64 c of None \<Rightarrow> None | Some flag \<Rightarrow>
Some (if flag then c else put64 Rax (registers (state64 c) Rcx) c))"
fun microrun :: "micro list \<Rightarrow> processor \<Rightarrow> 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 \<Rightarrow> 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 \<Rightarrow> bool" where
"microvalid (Imm32 v) = (extend32 (unat v) = v)"
| "microvalid (Load i) = (i < 2 ^ 28)"
| "microvalid (Alu Less) = False"
| "microvalid (Test r) = (r = Rax \<or> r = Rbx)"
| "microvalid _ = True"
fun expand :: "opcode \<Rightarrow> 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 \<Longrightarrow> 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 \<Rightarrow> pixel" where
"top64 c = pointer64 c + 8 * of_nat (length (stack (state64 c)))"
lemma microstep_top:
"microstep i c = Some d \<Longrightarrow> 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 (\<lambda>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 \<Rightarrow> (micro \<times> nat list) option" where
"decode64 bs = (if take 2 bs = [72,184] then
if 10 \<le> 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 \<le> 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 \<le> length bs \<and> n < 128 \<and> 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 \<le> length bs \<and> n mod 8 = 0 \<and> n div 8 < 2 ^ 28
then Some (Load (n div 8),drop 8 bs) else None
else map_option (\<lambda>i. (i,drop (length (microbytes i)) bs))
(List.find (\<lambda>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 \<Rightarrow> processor \<Rightarrow> processor \<Rightarrow> bool" where
empty: "executes64 [] c c"
| advance: "microvalid i \<Longrightarrow> microstep i c = Some d \<Longrightarrow> executes64 tail d e \<Longrightarrow>
executes64 (microbytes i @ tail) c e"
| jump: "n < 2 ^ 31 \<Longrightarrow> n \<le> length tail \<Longrightarrow> executes64 (drop n tail) c d \<Longrightarrow>
executes64 ([233] @ octets 4 n @ tail) c d"
| zero: "n < 2 ^ 31 \<Longrightarrow> n \<le> length tail \<Longrightarrow> zero64 c = Some True \<Longrightarrow>
executes64 (drop n tail) c d \<Longrightarrow> executes64 ([15,132] @ octets 4 n @ tail) c d"
| nonzero: "n < 2 ^ 31 \<Longrightarrow> zero64 c = Some False \<Longrightarrow> executes64 tail c d \<Longrightarrow>
executes64 ([15,132] @ octets 4 n @ tail) c d"
lemma executes64_append:
"executes64 a c d \<Longrightarrow> executes64 b d e \<Longrightarrow> 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 \<Longrightarrow> microrun code c = Some d \<Longrightarrow>
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 \<Longrightarrow> top64 d = top64 c"
by (induction rule: executes64.induct) (auto dest: microstep_top)
theorem executes64_native:
"list_all encodable code \<Longrightarrow> run code (state64 c) = Some s \<Longrightarrow>
\<exists>d. executes64 (concat (map encode code)) c d \<and> 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 "\<exists>d. executes64 (flowbytes code) c d \<and> 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\<lparr>zero64 := Some (registers (state64 c) Rax = 0), carry64 := Some False\<rparr>"
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 "\<exists>d. executes64 (flowbytes (branching e)) c d \<and>
registers (state64 d) Rax = evaluate e [] (inputs (state64 c)) \<and>
stack (state64 d) = stack (state64 c) \<and> inputs (state64 d) = inputs (state64 c) \<and>
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 \<Rightarrow> (pixel \<times> processor) option" where
"ret64 c = (case stack (state64 c) of [] \<Rightarrow> None | address # rest \<Rightarrow>
Some (address,c\<lparr>state64 := (state64 c)\<lparr>stack := rest\<rparr>, pointer64 := pointer64 c + 8\<rparr>))"
definition returns64 :: "nat list \<Rightarrow> processor \<Rightarrow> pixel \<Rightarrow> processor \<Rightarrow> bool" where
"returns64 bytes c address d \<longleftrightarrow> (\<exists>body q. bytes = body @ [195] \<and>
executes64 body c q \<and> ret64 q = Some (address,d))"
theorem compiled_return:
assumes "scoped 0 e" "flowvalid (branching e)" "stack (state64 c) = address # rest"
shows "\<exists>d. returns64 (flowbytes (branching e) @ [195]) c address d \<and>
registers (state64 d) Rax = evaluate e [] (inputs (state64 c)) \<and>
stack (state64 d) = rest \<and> inputs (state64 d) = inputs (state64 c) \<and>
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\<lparr>state64 := (state64 q)\<lparr>stack := rest\<rparr>, pointer64 := pointer64 q + 8\<rparr>"
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 \<Rightarrow> nat list \<Rightarrow> processor \<Rightarrow> 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 \<le> length bytes \<and> n < 2 ^ 31 \<and> n \<le> 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 \<le> length bytes \<and> n < 2 ^ 31 \<and> n \<le> length bytes - 6 then
(case zero64 c of None \<Rightarrow> None | Some flag \<Rightarrow>
simulate64 fuel (drop (6 + (if flag then n else 0)) bytes) c)
else None
else Option.bind (decode64 bytes) (\<lambda>(i,rest).
if microvalid i then Option.bind (microstep i c) (simulate64 fuel rest) else None))"
by pat_completeness auto
termination by (relation "measure (\<lambda>(fuel,bytes,c). fuel)") auto
declare simulate64.simps [simp del]
end