author | kleing |
Sun, 07 Jan 2001 18:43:13 +0100 | |
changeset 10812 | ead84e90bfeb |
parent 10638 | 17063aee1d86 |
child 11085 | b830bf10bf71 |
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 |
|
10592 | 24 |
wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,nat,p_count,p_count] |
10042 | 25 |
=> state_type option err" |
10592 | 26 |
"wtl_inst i G rT s cert maxs max_pc pc == |
27 |
if app i G maxs 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)) |
10628 | 29 |
else Err" |
8245 | 30 |
|
31 |
constdefs |
|
10592 | 32 |
wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,nat,p_count,p_count] |
10042 | 33 |
=> state_type option err" |
10592 | 34 |
"wtl_cert i G rT s cert maxs max_pc pc == |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
35 |
case cert!pc of |
10592 | 36 |
None => wtl_inst i G rT s cert maxs max_pc pc |
10042 | 37 |
| Some s' => if G \<turnstile> s <=' (Some s') then |
10592 | 38 |
wtl_inst i G rT (Some s') cert maxs max_pc pc |
9757
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 |
10592 | 42 |
wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,nat,p_count,p_count, |
10042 | 43 |
state_type option] => state_type option err" |
8245 | 44 |
primrec |
10592 | 45 |
"wtl_inst_list [] G rT cert maxs max_pc pc s = OK s" |
46 |
"wtl_inst_list (i#is) G rT cert maxs max_pc pc s = |
|
47 |
(let s' = wtl_cert i G rT s cert maxs max_pc pc in |
|
10628 | 48 |
strict (wtl_inst_list is G rT cert maxs max_pc (pc+1)) s')" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
49 |
|
8245 | 50 |
|
51 |
constdefs |
|
10592 | 52 |
wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,certificate] => bool" |
53 |
"wtl_method G C pTs rT mxs 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> |
10592 | 57 |
wtl_inst_list ins G rT cert mxs 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 == |
|
10592 | 62 |
wf_prog (\<lambda>G C (sig,rT,maxs,maxl,b). wtl_method G C (snd sig) rT maxs maxl b (cert C sig)) G" |
9012 | 63 |
|
10042 | 64 |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10638
diff
changeset
|
65 |
lemmas [iff] = not_Err_eq |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10638
diff
changeset
|
66 |
|
10042 | 67 |
|
10496 | 68 |
lemma wtl_inst_OK: |
10592 | 69 |
"(wtl_inst i G rT s cert maxs max_pc pc = OK s') = |
70 |
(app i G maxs rT s \<and> (\<forall>pc' \<in> set (succs i pc). |
|
71 |
pc' < max_pc \<and> (pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')) \<and> |
|
10042 | 72 |
(if pc+1 \<in> set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))" |
10628 | 73 |
by (auto simp add: wtl_inst_def check_cert_def set_mem_eq) |
9012 | 74 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
75 |
lemma strict_Some [simp]: |
10496 | 76 |
"(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
|
77 |
by (cases x, auto) |
8245 | 78 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
79 |
lemma wtl_Cons: |
10592 | 80 |
"wtl_inst_list (i#is) G rT cert maxs max_pc pc s \<noteq> Err = |
81 |
(\<exists>s'. wtl_cert i G rT s cert maxs max_pc pc = OK s' \<and> |
|
82 |
wtl_inst_list is G rT cert maxs max_pc (pc+1) s' \<noteq> Err)" |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10638
diff
changeset
|
83 |
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
|
84 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
85 |
lemma wtl_append: |
10592 | 86 |
"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mxs mpc pc s = OK s') = |
87 |
(\<exists>s''. wtl_inst_list a G rT cert mxs mpc pc s = OK s'' \<and> |
|
88 |
wtl_inst_list b G rT cert mxs mpc (pc+length a) s'' = OK s')" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
89 |
(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
|
90 |
proof (induct ?P a) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
91 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
92 |
show "?P []" by simp |
9012 | 93 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
94 |
fix x xs |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
95 |
assume IH: "?P xs" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
96 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
97 |
show "?P (x#xs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
98 |
proof (intro allI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
99 |
fix s pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
100 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
101 |
show "?C s pc (x#xs)" |
10592 | 102 |
proof (cases "wtl_cert x G rT s cert mxs mpc pc") |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
103 |
case Err thus ?thesis by simp |
9183 | 104 |
next |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
105 |
fix s0 |
10592 | 106 |
assume OK: "wtl_cert x G rT s cert mxs mpc pc = OK s0" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
107 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
108 |
with IH |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
109 |
have "?C s0 (Suc pc) xs" by blast |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
110 |
|
10496 | 111 |
with OK |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
112 |
show ?thesis by simp |
9183 | 113 |
qed |
114 |
qed |
|
115 |
qed |
|
9012 | 116 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
117 |
lemma wtl_take: |
10592 | 118 |
"wtl_inst_list is G rT cert mxs mpc pc s = OK s'' ==> |
119 |
\<exists>s'. wtl_inst_list (take pc' is) G rT cert mxs mpc pc s = OK s'" |
|
9183 | 120 |
proof - |
10592 | 121 |
assume "wtl_inst_list is G rT cert mxs mpc pc s = OK s''" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
122 |
|
10592 | 123 |
hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mxs mpc pc s = OK s''" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
124 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
125 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
126 |
thus ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
127 |
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
|
128 |
qed |
9012 | 129 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
130 |
lemma take_Suc: |
10042 | 131 |
"\<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
|
132 |
proof (induct l) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
133 |
show "?P []" by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
134 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
135 |
fix x xs |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
136 |
assume IH: "?P xs" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
137 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
138 |
show "?P (x#xs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
139 |
proof (intro strip) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
140 |
fix n |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
141 |
assume "n < length (x#xs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
142 |
with IH |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
143 |
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
|
144 |
by - (cases n, auto) |
9183 | 145 |
qed |
146 |
qed |
|
9012 | 147 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
148 |
lemma wtl_Suc: |
10592 | 149 |
"[| wtl_inst_list (take pc is) G rT cert maxs (length is) 0 s = OK s'; |
150 |
wtl_cert (is!pc) G rT s' cert maxs (length is) pc = OK s''; |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
151 |
Suc pc < length is |] ==> |
10592 | 152 |
wtl_inst_list (take (Suc pc) is) G rT cert maxs (length is) 0 s = OK s''" |
9183 | 153 |
proof - |
10592 | 154 |
assume wtt: "wtl_inst_list (take pc is) G rT cert maxs (length is) 0 s = OK s'" |
155 |
assume wtc: "wtl_cert (is!pc) G rT s' cert maxs (length is) pc = OK s''" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
156 |
assume pc: "Suc pc < length is" |
9012 | 157 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
158 |
hence "take (Suc pc) is = (take pc is)@[is!pc]" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
159 |
by (simp add: take_Suc) |
9012 | 160 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
161 |
with wtt wtc pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
162 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
163 |
by (simp add: wtl_append min_def) |
9183 | 164 |
qed |
9012 | 165 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
166 |
lemma wtl_all: |
10592 | 167 |
"[| wtl_inst_list is G rT cert maxs (length is) 0 s \<noteq> Err; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
168 |
pc < length is |] ==> |
10592 | 169 |
\<exists>s' s''. wtl_inst_list (take pc is) G rT cert maxs (length is) 0 s = OK s' \<and> |
170 |
wtl_cert (is!pc) G rT s' cert maxs (length is) pc = OK s''" |
|
9183 | 171 |
proof - |
10592 | 172 |
assume all: "wtl_inst_list is G rT cert maxs (length is) 0 s \<noteq> Err" |
9012 | 173 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
174 |
assume pc: "pc < length is" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
175 |
hence "0 < length (drop pc is)" by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
176 |
then |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
177 |
obtain i r where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
178 |
Cons: "drop pc is = i#r" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
179 |
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
|
180 |
hence "i#r = drop pc is" .. |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
181 |
with all |
10592 | 182 |
have take: "wtl_inst_list (take pc is@i#r) G rT cert maxs (length is) 0 s \<noteq> Err" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
183 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
184 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
185 |
from pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
186 |
have "is!pc = drop pc is ! 0" by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
187 |
with Cons |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
188 |
have "is!pc = i" by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
189 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
190 |
with take pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
191 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
192 |
by (auto simp add: wtl_append min_def) |
9183 | 193 |
qed |
9012 | 194 |
|
10042 | 195 |
|
9183 | 196 |
end |