author | kleing |
Fri, 17 Jun 2011 20:38:43 +0200 | |
changeset 43438 | a666b8d11252 |
parent 43158 | 686fa0a0696e |
child 44000 | ab4d8499815c |
permissions | -rw-r--r-- |
43141 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
header "A Compiler for IMP" |
|
10343 | 4 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
5 |
theory Compiler imports Big_Step |
43141 | 6 |
begin |
12429 | 7 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
8 |
subsection "List setup" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
9 |
|
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
10 |
text {* |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
11 |
We are going to define a small machine language where programs are |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
12 |
lists of instructions. For nicer algebraic properties in our lemmas |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
13 |
later, we prefer @{typ int} to @{term nat} as program counter. |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
14 |
|
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
15 |
Therefore, we define notation for size and indexing for lists |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
16 |
on @{typ int}: |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
17 |
*} |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
18 |
abbreviation "isize xs == int (length xs)" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
19 |
|
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
20 |
primrec |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
21 |
inth :: "'a list => int => 'a" (infixl "!!" 100) where |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
22 |
inth_Cons: "(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
23 |
|
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
24 |
text {* |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
25 |
The only additional lemma we need is indexing over append: |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
26 |
*} |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
27 |
lemma inth_append [simp]: |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
28 |
"0 \<le> n \<Longrightarrow> |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
29 |
(xs @ ys) !! n = (if n < isize xs then xs !! n else ys !! (n - isize xs))" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
30 |
by (induct xs arbitrary: n) (auto simp: algebra_simps) |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
31 |
|
43141 | 32 |
subsection "Instructions and Stack Machine" |
10342 | 33 |
|
43141 | 34 |
datatype instr = |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
35 |
LOADI int | |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
36 |
LOAD string | |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
37 |
ADD | |
43141 | 38 |
STORE string | |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
39 |
JMP int | |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
40 |
JMPFLESS int | |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
41 |
JMPFGE int |
10342 | 42 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
43 |
(* reads slightly nicer *) |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
44 |
abbreviation |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
45 |
"JMPB i == JMP (-i)" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
46 |
|
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
47 |
type_synonym stack = "val list" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
48 |
type_synonym config = "int\<times>state\<times>stack" |
43141 | 49 |
|
50 |
abbreviation "hd2 xs == hd(tl xs)" |
|
51 |
abbreviation "tl2 xs == tl(tl xs)" |
|
11275 | 52 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
53 |
inductive iexec1 :: "instr \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
54 |
("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [50,0,0] 50) |
43141 | 55 |
where |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
56 |
"LOADI n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, n#stk)" | |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
57 |
"LOAD x \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" | |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
58 |
"ADD \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" | |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
59 |
"STORE n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" | |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
60 |
"JMP n \<turnstile>i (i,s,stk) \<rightarrow> (i+1+n,s,stk)" | |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
61 |
"JMPFLESS n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" | |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
62 |
"JMPFGE n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
63 |
|
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
64 |
code_pred iexec1 . |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
65 |
|
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
66 |
declare iexec1.intros |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
67 |
|
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
68 |
(* FIXME: why does code gen not work with fun? *) |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
69 |
inductive |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
70 |
exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
71 |
("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50) where |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
72 |
"\<lbrakk> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'; 0 \<le> i; i < isize P \<rbrakk> \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'" |
43141 | 73 |
|
74 |
code_pred exec1 . |
|
75 |
||
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
76 |
declare exec1.intros [intro!] |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
77 |
|
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
78 |
inductive_cases exec1_elim [elim!]: "P \<turnstile> c \<rightarrow> c'" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
79 |
|
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
80 |
lemma exec1_simp [simp]: |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
81 |
"P \<turnstile> c \<rightarrow> c' = |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
82 |
(\<exists>i s stk. c = (i,s,stk) \<and> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c' \<and> 0 \<le> i \<and> i < isize P)" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
83 |
by auto |
43141 | 84 |
|
85 |
inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50) |
|
86 |
where |
|
87 |
refl: "P \<turnstile> c \<rightarrow>* c" | |
|
88 |
step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''" |
|
89 |
||
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
90 |
declare refl[intro] step[intro] |
43141 | 91 |
|
92 |
lemmas exec_induct = exec.induct[split_format(complete)] |
|
93 |
||
94 |
code_pred exec . |
|
95 |
||
96 |
values |
|
97 |
"{(i,map t [''x'',''y''],stk) | i t stk. |
|
98 |
[LOAD ''y'', STORE ''x''] \<turnstile> |
|
43158 | 99 |
(0, [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 4], []) \<rightarrow>* (i,t,stk)}" |
43141 | 100 |
|
101 |
||
102 |
subsection{* Verification infrastructure *} |
|
103 |
||
104 |
lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''" |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
105 |
by (induct rule: exec.induct) fastsimp+ |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
106 |
|
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
107 |
inductive_cases iexec1_cases [elim!]: |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
108 |
"LOADI n \<turnstile>i c \<rightarrow> c'" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
109 |
"LOAD x \<turnstile>i c \<rightarrow> c'" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
110 |
"ADD \<turnstile>i c \<rightarrow> c'" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
111 |
"STORE n \<turnstile>i c \<rightarrow> c'" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
112 |
"JMP n \<turnstile>i c \<rightarrow> c'" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
113 |
"JMPFLESS n \<turnstile>i c \<rightarrow> c'" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
114 |
"JMPFGE n \<turnstile>i c \<rightarrow> c'" |
43141 | 115 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
116 |
text {* Simplification rules for @{const iexec1}. *} |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
117 |
lemma iexec1_simps [simp]: |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
118 |
"LOADI n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, n # stk))" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
119 |
"LOAD x \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, s x # stk))" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
120 |
"ADD \<turnstile>i c \<rightarrow> c' = |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
121 |
(\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, (hd2 stk + hd stk) # tl2 stk))" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
122 |
"STORE x \<turnstile>i c \<rightarrow> c' = |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
123 |
(\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x \<rightarrow> hd stk), tl stk))" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
124 |
"JMP n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1 + n, s, stk))" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
125 |
"JMPFLESS n \<turnstile>i c \<rightarrow> c' = |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
126 |
(\<exists>i s stk. c = (i, s, stk) \<and> |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
127 |
c' = (if hd2 stk < hd stk then i + 1 + n else i + 1, s, tl2 stk))" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
128 |
"JMPFGE n \<turnstile>i c \<rightarrow> c' = |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
129 |
(\<exists>i s stk. c = (i, s, stk) \<and> |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
130 |
c' = (if hd stk \<le> hd2 stk then i + 1 + n else i + 1, s, tl2 stk))" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
131 |
by (auto split del: split_if intro!: iexec1.intros) |
43141 | 132 |
|
133 |
||
134 |
text{* Below we need to argue about the execution of code that is embedded in |
|
135 |
larger programs. For this purpose we show that execution is preserved by |
|
136 |
appending code to the left or right of a program. *} |
|
137 |
||
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
138 |
lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
139 |
by auto |
11275 | 140 |
|
43141 | 141 |
lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'" |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
142 |
by (induct rule: exec.induct) (fastsimp intro: exec1_appendR)+ |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
143 |
|
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
144 |
lemma iexec1_shiftI: |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
145 |
assumes "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
146 |
shows "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
147 |
using assms by cases auto |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
148 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
149 |
lemma iexec1_shiftD: |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
150 |
assumes "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
151 |
shows "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
152 |
using assms by cases auto |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
153 |
|
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
154 |
lemma iexec_shift [simp]: |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
155 |
"(X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')) = (X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk'))" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
156 |
by (blast intro: iexec1_shiftI dest: iexec1_shiftD) |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
157 |
|
43141 | 158 |
lemma exec1_appendL: |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
159 |
"P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow> |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
160 |
P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow> (isize(P')+i',s',stk')" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
161 |
by simp |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
162 |
|
43141 | 163 |
lemma exec_appendL: |
164 |
"P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow> |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
165 |
P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow>* (isize(P')+i',s',stk')" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
166 |
by (induct rule: exec_induct) (blast intro!: exec1_appendL)+ |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
167 |
|
43141 | 168 |
text{* Now we specialise the above lemmas to enable automatic proofs of |
169 |
@{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and |
|
170 |
pieces of code that we already know how they execute (by induction), combined |
|
171 |
by @{text "@"} and @{text "#"}. Backward jumps are not supported. |
|
172 |
The details should be skipped on a first reading. |
|
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
173 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
174 |
If we have just executed the first instruction of the program, drop it: *} |
43141 | 175 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
176 |
lemma exec_Cons_1 [intro]: |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
177 |
"P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow> |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
178 |
instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
179 |
by (drule exec_appendL[where P'="[instr]"]) simp |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
180 |
|
43141 | 181 |
lemma exec_appendL_if[intro]: |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
182 |
"isize P' <= i |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
183 |
\<Longrightarrow> P \<turnstile> (i - isize P',s,stk) \<rightarrow>* (i',s',stk') |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
184 |
\<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (isize P' + i',s',stk')" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
185 |
by (drule exec_appendL[where P'=P']) simp |
10342 | 186 |
|
43141 | 187 |
text{* Split the execution of a compound program up into the excution of its |
188 |
parts: *} |
|
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
189 |
|
43141 | 190 |
lemma exec_append_trans[intro]: |
191 |
"P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow> |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
192 |
isize P \<le> i' \<Longrightarrow> |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
193 |
P' \<turnstile> (i' - isize P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow> |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
194 |
j'' = isize P + i'' |
43141 | 195 |
\<Longrightarrow> |
196 |
P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')" |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
197 |
by(metis exec_trans[OF exec_appendR exec_appendL_if]) |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
198 |
|
43141 | 199 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
200 |
declare Let_def[simp] |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
201 |
|
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
202 |
|
43141 | 203 |
subsection "Compilation" |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
204 |
|
43141 | 205 |
fun acomp :: "aexp \<Rightarrow> instr list" where |
206 |
"acomp (N n) = [LOADI n]" | |
|
207 |
"acomp (V x) = [LOAD x]" | |
|
208 |
"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]" |
|
209 |
||
210 |
lemma acomp_correct[intro]: |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
211 |
"acomp a \<turnstile> (0,s,stk) \<rightarrow>* (isize(acomp a),s,aval a s#stk)" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
212 |
by (induct a arbitrary: stk) fastsimp+ |
10342 | 213 |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
214 |
fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
215 |
"bcomp (B bv) c n = (if bv=c then [JMP n] else [])" | |
43141 | 216 |
"bcomp (Not b) c n = bcomp b (\<not>c) n" | |
217 |
"bcomp (And b1 b2) c n = |
|
218 |
(let cb2 = bcomp b2 c n; |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
219 |
m = (if c then isize cb2 else isize cb2+n); |
43141 | 220 |
cb1 = bcomp b1 False m |
221 |
in cb1 @ cb2)" | |
|
222 |
"bcomp (Less a1 a2) c n = |
|
223 |
acomp a1 @ acomp a2 @ (if c then [JMPFLESS n] else [JMPFGE n])" |
|
224 |
||
225 |
value |
|
226 |
"bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v'')))) |
|
227 |
False 3" |
|
228 |
||
229 |
lemma bcomp_correct[intro]: |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
230 |
"0 \<le> n \<Longrightarrow> |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
231 |
bcomp b c n \<turnstile> |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
232 |
(0,s,stk) \<rightarrow>* (isize(bcomp b c n) + (if c = bval b s then n else 0),s,stk)" |
43141 | 233 |
proof(induct b arbitrary: c n m) |
234 |
case Not |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
235 |
from Not(1)[where c="~c"] Not(2) show ?case by fastsimp |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
236 |
next |
43141 | 237 |
case (And b1 b2) |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
238 |
from And(1)[of "if c then isize (bcomp b2 c n) else isize (bcomp b2 c n) + n" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
239 |
"False"] |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
240 |
And(2)[of n "c"] And(3) |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
241 |
show ?case by fastsimp |
43141 | 242 |
qed fastsimp+ |
243 |
||
244 |
fun ccomp :: "com \<Rightarrow> instr list" where |
|
245 |
"ccomp SKIP = []" | |
|
246 |
"ccomp (x ::= a) = acomp a @ [STORE x]" | |
|
247 |
"ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" | |
|
248 |
"ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
249 |
(let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (isize cc\<^isub>1 + 1) |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
250 |
in cb @ cc\<^isub>1 @ JMP (isize cc\<^isub>2) # cc\<^isub>2)" | |
43141 | 251 |
"ccomp (WHILE b DO c) = |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
252 |
(let cc = ccomp c; cb = bcomp b False (isize cc + 1) |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
253 |
in cb @ cc @ [JMPB (isize cb + isize cc + 1)])" |
43141 | 254 |
|
255 |
value "ccomp |
|
256 |
(IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1) |
|
257 |
ELSE ''v'' ::= V ''u'')" |
|
258 |
||
259 |
value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))" |
|
260 |
||
261 |
||
262 |
subsection "Preservation of sematics" |
|
263 |
||
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
264 |
lemma ccomp_bigstep: |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
265 |
"(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk)" |
43141 | 266 |
proof(induct arbitrary: stk rule: big_step_induct) |
267 |
case (Assign x a s) |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
268 |
show ?case by (fastsimp simp:fun_upd_def cong: if_cong) |
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
269 |
next |
43141 | 270 |
case (Semi c1 s1 s2 c2 s3) |
271 |
let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2" |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
272 |
have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
273 |
using Semi.hyps(2) by fastsimp |
43141 | 274 |
moreover |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
275 |
have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
276 |
using Semi.hyps(4) by fastsimp |
43141 | 277 |
ultimately show ?case by simp (blast intro: exec_trans) |
278 |
next |
|
279 |
case (WhileTrue b s1 c s2 s3) |
|
280 |
let ?cc = "ccomp c" |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
281 |
let ?cb = "bcomp b False (isize ?cc + 1)" |
43141 | 282 |
let ?cw = "ccomp(WHILE b DO c)" |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
283 |
have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)" |
43141 | 284 |
using WhileTrue(1,3) by fastsimp |
285 |
moreover |
|
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
286 |
have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)" |
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
287 |
by fastsimp |
43141 | 288 |
moreover |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
289 |
have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue(5)) |
43141 | 290 |
ultimately show ?case by(blast intro: exec_trans) |
291 |
qed fastsimp+ |
|
13095
8ed413a57bdc
New machine architecture and other direction of compiler proof.
nipkow
parents:
12566
diff
changeset
|
292 |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
16417
diff
changeset
|
293 |
end |