Proof.thy

Back to the index of BV_ASCII 
Proof = Correct

Theorems proved in Proof.ML:

correct_state_imp_wt_class 
[| correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # fs); wt_classfiles CFS phi |]
==> wt_class CFS cn (phi cn)

get_methods_imp_wt_instr 
[| wt_classfiles CFS phi; pc < length ins; is_class CFS cn; get_methods CFS !! cn ml = Some (rd, ins) |]
==> wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc

get_methods_imp_wt_start 
[| wt_classfiles CFS phi; is_class CFS cn; get_methods CFS !! cn ml = Some (rd, ins) |]
==> 0 < length ins & wt_start CFS cn (snd ml) (phi cn ml)

IAload_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = LAS (X load idx);
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

IAstore_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = LAS (X store idx);
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

Bipush_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = LAS (Bipush i);
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

Aconst_null_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = LAS Aconst_null;
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

LAS_correct 
[| wf_classfiles CFS; get_code CFS cn ml ! pc = LAS las_com; wt_class CFS cn (phi cn);
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

IAaload_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = MA (X aload);
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

IAastore_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = MA (X astore);
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

MA_correct 
[| wf_classfiles CFS; get_code CFS cn ml ! pc = MA ma_com; wt_class CFS cn (phi cn);
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

Checkcast_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = CH (Checkcast idx);
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

CH_correct 
[| wf_classfiles CFS; get_code CFS cn ml ! pc = CH ch_com; wt_class CFS cn (phi cn);
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

Getfield_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = MO (Getfield idx);
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

Putfield_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = MO (Putfield idx);
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

MO_correct 
[| wf_classfiles CFS; get_code CFS cn ml ! pc = MO mo_com; wt_class CFS cn (phi cn);
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

New_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = CO (New cl_idx);
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

IAnewarray_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = CO (IAnewarray atd);
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

CO_correct 
[| wf_classfiles CFS; get_code CFS cn ml ! pc = CO co_com; wt_class CFS cn (phi cn);
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

MI_correct 
[| wf_classfiles CFS; wt_classfiles CFS phi; get_code CFS cn ml ! pc = MI inv_com;
   Some (xp', hp, frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp, frs')

IAreturn_correct 
[| wf_classfiles CFS; wt_classfiles CFS phi; get_code CFS cn ml ! pc = MR (X return);
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

Return_correct 
[| wf_classfiles CFS; wt_classfiles CFS phi; get_code CFS cn ml ! pc = MR Return;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

MR_correct 
[| wf_classfiles CFS; get_code CFS cn ml ! pc = MR mr_com; wt_classfiles CFS phi;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

Goto_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = UB (Goto branch);
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

UB_correct 
[| wf_classfiles CFS; get_code CFS cn ml ! pc = UB ub_com; wt_class CFS cn (phi cn);
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

If_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = CB (If_ bop branch);
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

Ifnull_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = CB (Ifnull branch);
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

Ifiacmpeq_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = CB (X Ifiacmpeq branch);
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

CB_correct 
[| wf_classfiles CFS; get_code CFS cn ml ! pc = CB cb_com; wt_class CFS cn (phi cn);
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

Pop_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = OS Pop;
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

Dup_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = OS Dup;
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

Swap_correct 
[| wf_classfiles CFS; get_methods CFS !! cn ml = Some (rd, ins); ins ! pc = OS Swap;
   wt_instr (ins ! pc) CFS rd (get_cpool CFS !! cn) (phi cn ml) (length ins) pc;
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

OS_correct 
[| wf_classfiles CFS; get_code CFS cn ml ! pc = OS os_com; wt_class CFS cn (phi cn);
   Some (xp', hp', frs') = exec (CFS, None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # frs) |]
==> correct_state CFS phi (xp', hp', frs')

BV_correct_1 
[| wf_classfiles CFS; wt_classfiles CFS phi; correct_state CFS phi (xp, hp, frs);
   exec (CFS, xp, hp, frs) = Some (xp', hp', frs') |]
==> correct_state CFS phi (xp', hp', frs')

exec_lemma 
[| xp = None; frs ~= [] |] ==> ? xp' hp' frs'. exec (CFS, xp, hp, frs) = Some (xp', hp', frs')

L1 
[| wf_classfiles CFS; wt_classfiles CFS phi; correct_state CFS phi (xp, hp, frs); xp = None; frs ~= [] |]
==> ? xp' hp' frs'.
       exec (CFS, xp, hp, frs) = Some (xp', hp', frs') & correct_state CFS phi (xp', hp', frs')

BV_correct 
[| wf_classfiles CFS; CFS |- s -jvm-> t; wt_classfiles CFS phi; correct_state CFS phi s |]
==> correct_state CFS phi t

BV_correct_initial 
[| wf_classfiles CFS; wt_classfiles CFS phi; CFS |- s0 -jvm-> (None, hp, (stk, loc, cn, ml, pc) # frs);
   correct_state CFS phi s0 |]
==> approx_stk CFS hp stk (fst (phi cn ml ! pc)) & approx_loc CFS hp loc (snd (phi cn ml ! pc))