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
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
|
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
|