author | kleing |
Mon, 20 Nov 2000 16:37:42 +0100 | |
changeset 10496 | f2d304bdf3cc |
parent 10042 | 7164dc0d24d8 |
child 10592 | fc0b575a2cf7 |
permissions | -rw-r--r-- |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
1 |
(* Title: HOL/MicroJava/BV/LBVSpec.thy |
8245 | 2 |
ID: $Id$ |
3 |
Author: Gerwin Klein |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
9054 | 5 |
*) |
8245 | 6 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
7 |
header {* The Lightweight Bytecode Verifier *} |
9054 | 8 |
|
8245 | 9 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
10 |
theory LBVSpec = Step : |
8245 | 11 |
|
12 |
types |
|
13 |
certificate = "state_type option list" |
|
10042 | 14 |
class_certificate = "sig => certificate" |
15 |
prog_certificate = "cname => class_certificate" |
|
8245 | 16 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
17 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
18 |
constdefs |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
19 |
check_cert :: "[instr, jvm_prog, state_type option, certificate, p_count, p_count] |
10042 | 20 |
=> bool" |
21 |
"check_cert i G s cert pc max_pc == \<forall>pc' \<in> set (succs i pc). pc' < max_pc \<and> |
|
22 |
(pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')" |
|
9376 | 23 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
24 |
wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count] |
10042 | 25 |
=> state_type option err" |
26 |
"wtl_inst i G rT s cert max_pc pc == |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
27 |
if app i G rT s \<and> check_cert i G s cert pc max_pc then |
10496 | 28 |
if pc+1 mem (succs i pc) then OK (step i G s) else OK (cert!(pc+1)) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
29 |
else Err"; |
8245 | 30 |
|
31 |
constdefs |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
32 |
wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count] |
10042 | 33 |
=> state_type option err" |
34 |
"wtl_cert i G rT s cert max_pc pc == |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
35 |
case cert!pc of |
10042 | 36 |
None => wtl_inst i G rT s cert max_pc pc |
37 |
| Some s' => if G \<turnstile> s <=' (Some s') then |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
38 |
wtl_inst i G rT (Some s') cert max_pc pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
39 |
else Err" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
40 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
41 |
consts |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
42 |
wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,p_count,p_count, |
10042 | 43 |
state_type option] => state_type option err" |
8245 | 44 |
primrec |
10496 | 45 |
"wtl_inst_list [] G rT cert max_pc pc s = OK s" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
46 |
"wtl_inst_list (i#is) G rT cert max_pc pc s = |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
47 |
(let s' = wtl_cert i G rT s cert max_pc pc in |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
48 |
strict (wtl_inst_list is G rT cert max_pc (pc+1)) s')"; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
49 |
|
8245 | 50 |
|
51 |
constdefs |
|
10042 | 52 |
wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] => bool" |
53 |
"wtl_method G C pTs rT mxl ins cert == |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
54 |
let max_pc = length ins |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
55 |
in |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
56 |
0 < max_pc \<and> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
57 |
wtl_inst_list ins G rT cert max_pc 0 |
10496 | 58 |
(Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) \<noteq> Err" |
8245 | 59 |
|
10042 | 60 |
wtl_jvm_prog :: "[jvm_prog,prog_certificate] => bool" |
61 |
"wtl_jvm_prog G cert == |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
62 |
wf_prog (\<lambda>G C (sig,rT,maxl,b). wtl_method G C (snd sig) rT maxl b (cert C sig)) G" |
9012 | 63 |
|
10042 | 64 |
|
65 |
||
10496 | 66 |
lemma wtl_inst_OK: |
67 |
"(wtl_inst i G rT s cert max_pc pc = OK s') = |
|
10042 | 68 |
(app i G rT s \<and> (\<forall>pc' \<in> set (succs i pc). |
69 |
pc' < max_pc \<and> (pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')) \<and> |
|
70 |
(if pc+1 \<in> set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))" |
|
71 |
by (auto simp add: wtl_inst_def check_cert_def set_mem_eq); |
|
9012 | 72 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
73 |
lemma strict_Some [simp]: |
10496 | 74 |
"(strict f x = OK y) = (\<exists> z. x = OK z \<and> f z = OK y)" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
75 |
by (cases x, auto) |
8245 | 76 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
77 |
lemma wtl_Cons: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
78 |
"wtl_inst_list (i#is) G rT cert max_pc pc s \<noteq> Err = |
10496 | 79 |
(\<exists>s'. wtl_cert i G rT s cert max_pc pc = OK s' \<and> |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
80 |
wtl_inst_list is G rT cert max_pc (pc+1) s' \<noteq> Err)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
81 |
by (auto simp del: split_paired_Ex) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
82 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
83 |
lemma wtl_append: |
10496 | 84 |
"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mpc pc s = OK s') = |
85 |
(\<exists>s''. wtl_inst_list a G rT cert mpc pc s = OK s'' \<and> |
|
86 |
wtl_inst_list b G rT cert mpc (pc+length a) s'' = OK s')" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
87 |
(is "\<forall> s pc. ?C s pc a" is "?P a") |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
88 |
proof (induct ?P a) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
89 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
90 |
show "?P []" by simp |
9012 | 91 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
92 |
fix x xs |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
93 |
assume IH: "?P xs" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
94 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
95 |
show "?P (x#xs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
96 |
proof (intro allI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
97 |
fix s pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
98 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
99 |
show "?C s pc (x#xs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
100 |
proof (cases "wtl_cert x G rT s cert mpc pc") |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
101 |
case Err thus ?thesis by simp |
9183 | 102 |
next |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
103 |
fix s0 |
10496 | 104 |
assume OK: "wtl_cert x G rT s cert mpc pc = OK s0" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
105 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
106 |
with IH |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
107 |
have "?C s0 (Suc pc) xs" by blast |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
108 |
|
10496 | 109 |
with OK |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
110 |
show ?thesis by simp |
9183 | 111 |
qed |
112 |
qed |
|
113 |
qed |
|
9012 | 114 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
115 |
lemma wtl_take: |
10496 | 116 |
"wtl_inst_list is G rT cert mpc pc s = OK s'' ==> |
117 |
\<exists>s'. wtl_inst_list (take pc' is) G rT cert mpc pc s = OK s'" |
|
9183 | 118 |
proof - |
10496 | 119 |
assume "wtl_inst_list is G rT cert mpc pc s = OK s''" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
120 |
|
10496 | 121 |
hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mpc pc s = OK s''" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
122 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
123 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
124 |
thus ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
125 |
by (auto simp add: wtl_append simp del: append_take_drop_id) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
126 |
qed |
9012 | 127 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
128 |
lemma take_Suc: |
10042 | 129 |
"\<forall>n. n < length l --> take (Suc n) l = (take n l)@[l!n]" (is "?P l") |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
130 |
proof (induct l) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
131 |
show "?P []" by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
132 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
133 |
fix x xs |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
134 |
assume IH: "?P xs" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
135 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
136 |
show "?P (x#xs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
137 |
proof (intro strip) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
138 |
fix n |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
139 |
assume "n < length (x#xs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
140 |
with IH |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
141 |
show "take (Suc n) (x # xs) = take n (x # xs) @ [(x # xs) ! n]" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
142 |
by - (cases n, auto) |
9183 | 143 |
qed |
144 |
qed |
|
9012 | 145 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
146 |
lemma wtl_Suc: |
10496 | 147 |
"[| wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'; |
148 |
wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''; |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
149 |
Suc pc < length is |] ==> |
10496 | 150 |
wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = OK s''" |
9183 | 151 |
proof - |
10496 | 152 |
assume wtt: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'" |
153 |
assume wtc: "wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
154 |
assume pc: "Suc pc < length is" |
9012 | 155 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
156 |
hence "take (Suc pc) is = (take pc is)@[is!pc]" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
157 |
by (simp add: take_Suc) |
9012 | 158 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
159 |
with wtt wtc pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
160 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
161 |
by (simp add: wtl_append min_def) |
9183 | 162 |
qed |
9012 | 163 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
164 |
lemma wtl_all: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
165 |
"[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
166 |
pc < length is |] ==> |
10496 | 167 |
\<exists>s' s''. wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s' \<and> |
168 |
wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''" |
|
9183 | 169 |
proof - |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
170 |
assume all: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err" |
9012 | 171 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
172 |
assume pc: "pc < length is" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
173 |
hence "0 < length (drop pc is)" by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
174 |
then |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
175 |
obtain i r where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
176 |
Cons: "drop pc is = i#r" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
177 |
by (auto simp add: neq_Nil_conv simp del: length_drop) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
178 |
hence "i#r = drop pc is" .. |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
179 |
with all |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
180 |
have take: "wtl_inst_list (take pc is@i#r) G rT cert (length is) 0 s \<noteq> Err" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
181 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
182 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
183 |
from pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
184 |
have "is!pc = drop pc is ! 0" by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
185 |
with Cons |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
186 |
have "is!pc = i" by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
187 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
188 |
with take pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
189 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
190 |
by (auto simp add: wtl_append min_def) |
9183 | 191 |
qed |
9012 | 192 |
|
10042 | 193 |
lemma unique_set: |
194 |
"(a,b,c,d)\<in>set l --> unique l --> (a',b',c',d') \<in> set l --> |
|
195 |
a = a' --> b=b' \<and> c=c' \<and> d=d'" |
|
196 |
by (induct "l") auto |
|
197 |
||
198 |
lemma unique_epsilon: |
|
199 |
"(a,b,c,d)\<in>set l --> unique l --> |
|
200 |
(SOME (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)" |
|
201 |
by (auto simp add: unique_set) |
|
202 |
||
9183 | 203 |
end |