1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191

theory Native
  imports Compiler
begin

datatype register = Rax | Rcx | Rbx | Rdx | R8 | R9

datatype opcode = Immediate pixel | Push register | Pop register | Peek nat
  | Arithmetic operator | Conditional | Move register register

record machine =
  registers :: "register \<Rightarrow> pixel"
  stack :: "pixel list"

fun input_register :: "input \<Rightarrow> register" where
  "input_register X = R8"
| "input_register Y = R9"
| "input_register T = Rdx"

definition inputs :: "machine \<Rightarrow> input \<Rightarrow> pixel" where
  "inputs s i = registers s (input_register i)"

fun exchanges :: "operator \<Rightarrow> bool" where
  "exchanges Sub = True"
| "exchanges Shl = True"
| "exchanges Shr = True"
| "exchanges Less = True"
| "exchanges _ = False"

fun transition :: "opcode \<Rightarrow> machine \<Rightarrow> machine option" where
  "transition (Immediate v) s = Some (s\<lparr>registers := (registers s)(Rax := v)\<rparr>)"
| "transition (Push r) s = Some (s\<lparr>stack := registers s r # stack s\<rparr>)"
| "transition (Pop r) s = (case stack s of [] \<Rightarrow> None | v # vs \<Rightarrow>
    Some (s\<lparr>registers := (registers s)(r := v), stack := vs\<rparr>))"
| "transition (Peek i) s = (if i < length (stack s) then
    Some (s\<lparr>registers := (registers s)(Rax := stack s ! i)\<rparr>) else None)"
| "transition (Arithmetic op) s = Some (s\<lparr>registers :=
    (registers s)(Rcx := if exchanges op then registers s Rax else registers s Rcx,
      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"
| "run (i # code) s = Option.bind (transition i s) (run code)"

lemma run_append:
  "run (a @ b) s = Option.bind (run a s) (run b)"
  by (induction a arbitrary: s) (auto split: option.splits bind_splits)

fun lower :: "instruction \<Rightarrow> opcode list" where
  "lower (Constant v) = [Immediate v, Push Rax]"
| "lower (Fetch i) = [Push (input_register i)]"
| "lower (Pick i) = [Peek i, Push Rax]"
| "lower (Calculate op) = [Pop Rax, Pop Rcx, Arithmetic op, Push Rax]"
| "lower Choose = [Pop Rax, Pop Rcx, Pop Rbx, Conditional, Push Rax]"
| "lower Slide = [Pop Rax, Pop Rcx, Push Rax]"

definition observe :: "machine \<Rightarrow> (input \<Rightarrow> pixel) \<times> pixel list" where
  "observe s = (inputs s, stack s)"

lemma input_scratch [simp]:
  "input_register i \<noteq> Rax"
  "input_register i \<noteq> Rcx"
  "input_register i \<noteq> Rbx"
  by (cases i; simp)+

lemma inputs_update [simp]:
  "inputs (s\<lparr>registers := (registers s)(Rax := a)\<rparr>) = inputs s"
  "inputs (s\<lparr>registers := (registers s)(Rcx := a)\<rparr>) = inputs s"
  "inputs (s\<lparr>registers := (registers s)(Rbx := a)\<rparr>) = inputs s"
  "inputs (s\<lparr>stack := vs\<rparr>) = inputs s"
  by (auto simp: inputs_def fun_eq_iff split: input.splits)

theorem lower_correct:
  "map_option observe (run (lower i) s) =
    map_option (\<lambda>vs. (inputs s, vs)) (step (inputs s) i (stack s))"
proof (cases i)
  case (Constant v)
  then show ?thesis by (simp add: observe_def)
next
  case (Fetch i)
  then show ?thesis by (simp add: observe_def inputs_def)
next
  case (Pick i)
  then show ?thesis by (simp add: observe_def)
next
  case (Calculate op)
  then show ?thesis
    by (cases "stack s"; simp add: observe_def inputs_def fun_eq_iff split: list.splits input.splits)
next
  case Choose
  then show ?thesis
    by (cases "stack s"; simp add: observe_def inputs_def fun_eq_iff split: list.splits input.splits)
next
  case Slide
  then show ?thesis
    by (cases "stack s"; simp add: observe_def inputs_def fun_eq_iff split: list.splits input.splits)
qed

definition native :: "instruction list \<Rightarrow> opcode list" where
  "native code = concat (map lower code)"

theorem native_correct:
  "map_option observe (run (native code) s) =
    map_option (\<lambda>vs. (inputs s, vs)) (execute (inputs s) code (stack s))"
proof (induction code arbitrary: s)
  case Nil
  then show ?case by (simp add: native_def observe_def)
next
  case (Cons i code)
  show ?case
    using Cons.IH lower_correct[of i s]
    by (auto simp: native_def run_append observe_def split: option.splits bind_splits)
qed

corollary native_expression:
  assumes "scoped 0 e"
  shows "map_option observe (run (native (compile (optimise e) [])) s) =
    Some (inputs s, evaluate e [] (inputs s) # stack s)"
proof -
  have code: "execute (inputs s) (compile (optimise e) []) (stack s) =
      Some (evaluate e [] (inputs s) # stack s)"
    using compile_correct[where e="optimise e" and env="[]" and slots="[]" and s="stack s" and inputs="inputs s"]
      assms optimise_scoped
    by (simp add: represents_def optimise_correct)
  show ?thesis using native_correct[of "compile (optimise e) []" s] code by simp
qed

theorem native_return:
  assumes "scoped 0 e"
  shows "\<exists>q. run (native (compile (optimise e) []) @ [Pop Rax]) s = Some q \<and>
    registers q Rax = evaluate e [] (inputs s) \<and> stack q = stack s \<and> inputs q = inputs s"
proof -
  obtain q where run: "run (native (compile (optimise e) [])) s = Some q"
    and ins: "inputs q = inputs s" and stk: "stack q = evaluate e [] (inputs s) # stack s"
    using native_expression[OF assms, of s]
    by (auto simp: observe_def split: option.splits)
  show ?thesis using run ins stk
    by (auto simp: run_append inputs_def fun_eq_iff)
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}"
| "writes _ = {}"

lemma transition_preserves:
  "transition i s = Some t \<Longrightarrow> r \<notin> writes i \<Longrightarrow> registers t r = registers s r"
  by (cases i) (auto split: list.splits if_splits)

theorem run_preserves:
  "run code s = Some t \<Longrightarrow> list_all (\<lambda>i. r \<notin> writes i) code \<Longrightarrow>
    registers t r = registers s r"
  by (induction code arbitrary: s) (auto dest: transition_preserves split: option.splits bind_splits)

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