Up to index of Isabelle/Bali4
theory TypeSafe = Eval + WellForm + Conform(* Title: isabelle/Bali/TypeSafe.thy
ID: $Id: TypeSafe.thy,v 1.19 2000/06/26 08:52:28 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
The type soundness proof for Java
*)
TypeSafe = Eval + WellForm + Conform
theorem conf_fits:
G,s\<turnstile>v\<Colon>\<preceq>T ==> G,s\<turnstile>v fits T
theorem fits_conf:
[| G,s\<turnstile>v\<Colon>\<preceq>T; G|-T<=:? T'; G,s\<turnstile>v fits T';
ws_prog G |]
==> G,s\<turnstile>v\<Colon>\<preceq>T'
theorem fits_Array:
[| G,s\<turnstile>v\<Colon>\<preceq>T; G|-T'.[]<=:T.[];
G,s\<turnstile>v fits T'; ws_prog G |]
==> G,s\<turnstile>v\<Colon>\<preceq>T'
theorem halloc_gext:
G|-s1 -halloc oi>a-> s2 ==> snd s1\<le>|snd s2
theorem sxalloc_gext:
G|-s1 -sxalloc-> s2 ==> snd s1\<le>|snd s2
theorem eval_gext_lemma:
(s, t, w, s') : eval G
==> snd s\<le>|snd s' &
(case w of In1 v => ALL C. t = In1r (init C) --> normal s --> initd C s'
| In2 vf => normal s --> (ALL v x s. s\<le>|snd (assign (snd vf) v (x, s)))
| In3 vs => True)
[!]
theorem evar_gext_f:
(Norm s1, In2 e, In2 vf, s2) : eval G ==> s\<le>|snd (assign (snd vf) v (x, s))
[!]
theorem eval_gext':
((x1, s1), t, w, x2, s2) : eval G ==> s1\<le>|s2 [!]
theorem init_yields_initd:
(Norm s1, In1r (init C), In1 Unit, s2) : eval G ==> initd C s2 [!]
theorem wt_init_comp_ty:
is_type G T ==> (G, L)|-init_comp_ty T:<> [!]
theorem oconf_init_obj:
[| wf_prog G;
case r of Inl a => is_type G (obj_ty (oi, fs)) | Inr C => is_class G C |]
==> G,s\<turnstile>(oi, init_vals (var_tys G oi r))\<Colon>\<preceq>\<surd>r
theorem conforms_newG:
[| globs s oref = None; (x, s)\<Colon>\<preceq>(G, L); wf_prog G;
case oref of Inl a => is_type G (obj_ty (oi, fs)) | Inr C => is_class G C |]
==> (x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)
theorem conforms_init_class_obj:
[| (x, s)\<Colon>\<preceq>(G, L); wf_prog G; class G C = Some y;
¬ inited C (globs s) |]
==> (x, (init_class_obj G C) s)\<Colon>\<preceq>(G, L)
theorem fst_init_lvars:
fst (init_lvars G C sig (invmode m e) a' pvs (x, s)) = (if m then x else (np a') x)
theorem halloc_conforms:
[| G|-s1 -halloc oi>a-> s2; wf_prog G; s1\<Colon>\<preceq>(G, L);
is_type G (obj_ty (oi, fs)) |]
==> s2\<Colon>\<preceq>(G, L)
[!]
theorem halloc_type_sound:
[| G|-s1 -halloc oi>a-> s2; wf_prog G; s1\<Colon>\<preceq>(G, L);
T = obj_ty (oi, fs); is_type G T |]
==> s2\<Colon>\<preceq>(G, L) &
(%(x', s'). x' = None --> G,s'\<turnstile>Addr a\<Colon>\<preceq>T) s2
[!]
theorem sxalloc_type_sound:
[| G|-s1 -sxalloc-> s2; wf_prog G |]
==> case fst s1 of None => s2 = s1
| Some x =>
EX a. fst s2 = Some (XcptLoc a) &
(ALL L. s1\<Colon>\<preceq>(G, L) --> s2\<Colon>\<preceq>(G, L))
[!]
theorem DynT_propI:
[| (x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>a'\<Colon>\<preceq>RefT t;
wf_prog G; mode = IntVir --> a' ~= Null |]
==> G\<turnstile>mode\<rightarrow>target mode s a' cT\<preceq>t
theorem DynT_mheadsD:
[| the (cmethd G dynT sig) = (md, (m', pns, rT), lvars, bdy);
G\<turnstile>invmode m e\<rightarrow>dynT\<preceq>t; wf_prog G;
(G, L)|-e:-RefT t; (cT, m, pnsa, T) : mheads G t sig;
target (invmode m e) s2 a' cT = dynT |]
==> cmethd G dynT sig = Some (md, (m, pns, rT), lvars, bdy) &
G|-rT<=:T &
m' = m &
wf_mdecl G md (sig, (m, pns, rT), lvars, bdy) &
is_class G dynT &
G|-dynT<=:C md &
is_class G md &
(invmode m e ~= IntVir -->
(EX C. t = ClassT C & G|-C<=:C md) & cT = ClassT md)
[!]
theorem DynT_conf:
[| G|-target mode s2 a' cT<=:C md; wf_prog G;
G,s2\<turnstile>a'\<Colon>\<preceq>RefT t; mode = IntVir --> a' ~= Null;
mode ~= IntVir --> (EX C. t = ClassT C & G|-C<=:C md) & cT = ClassT md |]
==> G,s2\<turnstile>a'\<Colon>\<preceq>Class md
theorem Ass_lemma:
[| (Norm s0, In2 va, In2 (w, f), Norm s1) : eval G;
(Norm s1, In1l e, In1 v, Norm s2) : eval G;
G,s2\<turnstile>v\<Colon>\<preceq>T';
s1\<le>|s2 --> assign f v (Norm s2)\<Colon>\<preceq>(G, L) |]
==> assign f v (Norm s2)\<Colon>\<preceq>(G, L) &
(%(x', s'). x' = None --> G,s'\<turnstile>v\<Colon>\<preceq>T')
(assign f v (Norm s2))
[!]
theorem Throw_lemma:
[| G|-tn<=:C SXcpt Throwable; wf_prog G; (x1, s1)\<Colon>\<preceq>(G, L);
x1 = None --> G,s1\<turnstile>a'\<Colon>\<preceq>Class tn |]
==> xupd (throw a') (x1, s1)\<Colon>\<preceq>(G, L)
theorem Try_lemma:
[| G|-obj_ty (the (globs s1' (Inl a)))<=:Class tn;
(Some (XcptLoc a), s1')\<Colon>\<preceq>(G, L); wf_prog G |]
==> Norm (lupd(vn\<mapsto>Addr a) s1')\<Colon>\<preceq>(G, L(vn|->Class tn))
theorem Fin_lemma:
[| (Norm s1, In1r c2, In1 Unit, s2) : eval G; wf_prog G;
(x1, s1)\<Colon>\<preceq>(G, L); s2\<Colon>\<preceq>(G, L) |]
==> xupd (xcpt_if (EX y. x1 = Some y) x1) s2\<Colon>\<preceq>(G, L)
[!]
theorem FVar_lemma1:
[| table_of (fields G Ca) (fn, C) = Some (stat, fT);
x2 = None --> G,s2\<turnstile>a\<Colon>\<preceq>Class Ca; wf_prog G;
class G Ca = Some y; G|-Ca<=:C C; C ~= Object; class G C = Some ya;
(x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; inited C (globs s1);
(if stat then id else np a) x2 = None |]
==> EX oi fs.
globs s2 (if stat then Inr C else Inl (the_Addr a)) = Some (oi, fs) &
var_tys G oi (if stat then Inr C else Inl (the_Addr a)) (Inl (fn, C)) =
Some fT
theorem FVar_lemma:
[| (v, Norm s2') = fvar C stat fn a (x2, s2); class G Ca = Some y; G|-Ca<=:C C;
table_of (fields G Ca) (fn, C) = Some (stat, fT); wf_prog G;
x2 = None --> G,s2\<turnstile>a\<Colon>\<preceq>Class Ca; C ~= Object;
class G C = Some ya; (x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2;
inited C (globs s1) |]
==> G,s2'\<turnstile>fst v\<Colon>\<preceq>fT &
(ALL s'.
Norm s'\<Colon>\<preceq>(G, L) -->
(ALL w. G,s'\<turnstile>w\<Colon>\<preceq>fT -->
s2'\<le>|s' -->
assign (snd v) w (Norm s')\<Colon>\<preceq>(G, L)))
theorem AVar_lemma1:
[| globs s2 (Inl a) = Some (Arr ty i, vs); #0 <= the_Intg i'; the_Intg i' < i;
wf_prog G; G|-ty.[]<=:Tb.[]; Norm s2\<Colon>\<preceq>(G, L) |]
==> G,s2\<turnstile>the (vs (Inr (the_Intg i')))\<Colon>\<preceq>Tb
theorem AVar_lemma:
[| wf_prog G; ((x1, s1), In1l e2, In1 i, x2, s2) : eval G;
(v, Norm s2') = avar G i a (x2, s2);
x1 = None --> G,s1\<turnstile>a\<Colon>\<preceq>Ta.[];
(x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2 |]
==> G,s2'\<turnstile>fst v\<Colon>\<preceq>Ta &
(ALL s'.
Norm s'\<Colon>\<preceq>(G, L) -->
(ALL w. G,s'\<turnstile>w\<Colon>\<preceq>Ta -->
s2'\<le>|s' -->
assign (snd v) w (Norm s')\<Colon>\<preceq>(G, L)))
theorem conforms_init_lvars_lemma:
[| wf_prog G; wf_mhead G (mn, pTs) (m, pns, rT);
Ball (set lvars) (split (%vn. is_type G)); list_all2 (conf G s2) pvs pTsa;
G\<turnstile>pTsa[\<preceq>]pTs |]
==> G,s2\<turnstile>init_vals (table_of lvars)(pns[|->]pvs
)[\<Colon>\<preceq>]table_of lvars(pns[|->]pTs)
theorem conforms_init_lvars:
[| wf_mhead G (mn, pTs) (m, pns', rT'); wf_prog G;
Ball (set lvars) (split (%vn. is_type G)); list_all2 (conf G s2) pvs pTsa;
G\<turnstile>pTsa[\<preceq>]pTs; (x2, s2)\<Colon>\<preceq>(G, L);
cmethd G (target (invmode m e) s2 a' cT) (mn, pTs) =
Some (md, (ma, pns', rT'), lvars, blk, res);
G|-target (invmode m e) s2 a' cT<=:C md;
G,s2\<turnstile>a'\<Colon>\<preceq>RefT t;
invmode m e = IntVir --> a' ~= Null;
invmode m e ~= IntVir -->
(EX C. t = ClassT C & G|-C<=:C md) & cT = ClassT md |]
==> init_lvars G (target (invmode m e) s2 a' cT) (mn, pTs) (invmode m e) a' pvs
(x2, s2)\<Colon>\<preceq>(G, table_of lvars(pns'[|->]pTs
) (+)¬m ?\<mapsto>Class md)
theorem Call_type_sound:
[| wf_prog G; ((x1, s1), In3 ps, In3 pvs, x2, s2) : eval G;
C = target (invmode m e) s2 a' cT;
s2' = init_lvars G C (mn, pTs) (invmode m e) a' pvs (x2, s2);
(s2', In1l (Methd C (mn, pTs)), In1 v, x3, s3) : eval G;
ALL L. s2'\<Colon>\<preceq>(G, L) -->
(ALL T. (G, L)|-Methd C (mn, pTs):-T -->
(x3, s3)\<Colon>\<preceq>(G, L) &
(x3 = None --> G,s3\<turnstile>v\<Colon>\<preceq>T));
Norm s0\<Colon>\<preceq>(G, L); (G, L)|-e:-RefT t; (G, L)|-ps:#pTsa;
max_spec G t (mn, pTsa) = {((cT, m, pns, rT), pTs)};
(x1, s1)\<Colon>\<preceq>(G, L);
x1 = None --> G,s1\<turnstile>a'\<Colon>\<preceq>RefT t;
(x2, s2)\<Colon>\<preceq>(G, L);
x2 = None --> list_all2 (conf G s2) pvs pTsa |]
==> (x3, set_locals (locals s2) s3)\<Colon>\<preceq>(G, L) &
(x3 = None --> G,s3\<turnstile>v\<Colon>\<preceq>rT)
[!]
theorem eval_type_sound:
[| wf_prog G; (s0, t, v, s1) : eval G; s0\<Colon>\<preceq>(G, L);
(G, L)|-t::T |]
==> s1\<Colon>\<preceq>(G, L) &
(let (x, s) = s1
in x = None -->
((%T. if EX vf. t = In2 vf
then G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T &
(ALL s' w.
Norm s'\<Colon>\<preceq>(G, L) -->
G,s'\<turnstile>w\<Colon>\<preceq>T -->
s\<le>|s' -->
assign (snd (the_In2 v)) w
(Norm s')\<Colon>\<preceq>(G, L))
else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T) (+)
list_all2 (conf G s) (the_In3 v))
T)
[!]
theorem eval_ts:
[| (s, In1l e, In1 v, x', s') : eval G; wf_prog G; s\<Colon>\<preceq>(G, L);
(G, L)|-e:-T |]
==> (x', s')\<Colon>\<preceq>(G, L) &
(x' = None --> G,s'\<turnstile>v\<Colon>\<preceq>T)
[!]
theorem evals_ts:
[| (s, In3 es, In3 vs, x', s') : eval G; wf_prog G; s\<Colon>\<preceq>(G, L);
(G, L)|-es:#Ts |]
==> (x', s')\<Colon>\<preceq>(G, L) &
(x' = None --> list_all2 (conf G s') vs Ts)
[!]
theorem evar_ts:
[| (s, In2 v, In2 (w, f), x', s') : eval G; wf_prog G; s\<Colon>\<preceq>(G, L);
(G, L)|-v:=T |]
==> (x', s')\<Colon>\<preceq>(G, L) &
(x' = None -->
G,s'\<turnstile>w\<Colon>\<preceq>T &
(ALL s'' w'.
Norm s''\<Colon>\<preceq>(G, L) -->
G,s''\<turnstile>w'\<Colon>\<preceq>T -->
s'\<le>|s'' --> assign f w' (Norm s'')\<Colon>\<preceq>(G, L)))
[!]
theorem exec_ts:
[| (s, In1r s0, In1 Unit, s') : eval G; wf_prog G; s\<Colon>\<preceq>(G, L);
(G, L)|-s0:<> |]
==> s'\<Colon>\<preceq>(G, L)
[!]
theorem all_methods_understood:
[| wf_prog G; (G, L)|-{t,md,mode}e..mn( {pTs'}ps):-rT; s\<Colon>\<preceq>(G, L);
(s, In1l e, In1 a', Norm s') : eval G; mode = IntVir --> a' ~= Null |]
==> cmethd G (target mode s' a' md) (mn, pTs') ~= None
[!]