Quelle  BVExample.thy

(*  Title:      Jinja/BV/BVExample.thy

    Author:     Gerwin Klein
*)

section ‹Example Welltypings \label{sec:BVExample}›

theory BVExample
imports "../JVM/JVMListExample" BVSpecTypeSafe BVExec
  "HOL-Library.Code_Target_Numeral"
begin

text ‹
 This theory shows type correctness of the example program in section
 \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by
 explicitly providing a welltyping. It also shows that the start
 state of the program conforms to the welltyping; hence type safe
 execution is guaranteed.
 ›

subsection "Setup"

lemma distinct_classes':
  "list_name ≠ test_name"
  "list_name ≠ Object"
  "list_name ≠ ClassCast"
  "list_name ≠ OutOfMemory"
  "list_name ≠ NullPointer"
  "test_name ≠ Object"
  "test_name ≠ OutOfMemory"
  "test_name ≠ ClassCast"
  "test_name ≠ NullPointer"
  "ClassCast ≠ NullPointer"
  "ClassCast ≠ Object"
  "NullPointer ≠ Object"
  "OutOfMemory ≠ ClassCast"
  "OutOfMemory ≠ NullPointer"
  "OutOfMemory ≠ Object"
  by (simp_all add: list_name_def test_name_def Object_def NullPointer_def
    OutOfMemory_def ClassCast_def)

lemmas distinct_classes = distinct_classes' distinct_classes' [symmetric]

lemma distinct_fields:
  "val_name ≠ next_name"
  "next_name ≠ val_name"
  by (simp_all add: val_name_def next_name_def)

text ‹Abbreviations for definitions we will have to use often in the
  below:›
lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def 
                     OutOfMemoryC_def ClassCastC_def
lemmas class_defs  = list_class_def test_class_def

text ‹These auxiliary proofs are for efficiency: class lookup,
  relation, method and field lookup are computed only once:
 ›
lemma class_Object [simp]:
  "class E Object = Some (undefined, [],[])"
  by (simp add: class_def system_defs E_def)

lemma class_NullPointer [simp]:
  "class E NullPointer = Some (Object, [], [])"
  by (simp add: class_def system_defs E_def distinct_classes)

lemma class_OutOfMemory [simp]:
  "class E OutOfMemory = Some (Object, [], [])"
  by (simp add: class_def system_defs E_def distinct_classes)

lemma class_ClassCast [simp]:
  "class E ClassCast = Some (Object, [], [])"
  by (simp add: class_def system_defs E_def distinct_classes)

lemma class_list [simp]:
  "class E list_name = Some list_class"
  by (simp add: class_def system_defs E_def distinct_classes)
 
lemma class_test [simp]:
  "class E test_name = Some test_class"
  by (simp add: class_def system_defs E_def distinct_classes)

lemma E_classes [simp]:
  "{C. is_class E C} = {list_name, test_name, NullPointer,
                        ClassCast, OutOfMemory, Object}"
  by (auto simp add: is_class_def class_def system_defs E_def class_defs)

text ‹The subclass releation spelled out:›
lemma subcls1:
  "subcls1 E = {(list_name,Object), (test_name,Object), (NullPointer, Object),
                (ClassCast, Object), (OutOfMemory, Object)}"
(*<*)
  apply (simp add: subcls1_def2)
  apply (simp add: class_defs system_defs E_def class_def)
  (* FIXME: cannot simply expand class names, since
     inequality proofs on strings are too inefficient *)
  apply (auto simp: distinct_classes split!: if_splits)
  done
(*>*)

text ‹The subclass relation is acyclic; hence its converse is well founded:›
lemma notin_rtrancl:
  "(a,b) ∈ r^* ==> a ≠ b ==> (∧y. (a,y) ∉ r) ==> False"
  by (auto elim: converse_rtranclE)

lemma acyclic_subcls1_E: "acyclic (subcls1 E)"
(*<*)
  apply (rule acyclicI)
  apply (simp add: subcls1)
  apply (auto dest!: tranclD)
  apply (auto elim!: notin_rtrancl simp add: distinct_classes)
  done
(*>*)

lemma wf_subcls1_E: "wf ((subcls1 E)^-1)"
(*<*)
  apply (rule finite_acyclic_wf_converse)
  apply (simp add: subcls1)
  apply (rule acyclic_subcls1_E)
  done  
(*>*)

text ‹Method and field lookup:›

lemma method_append [simp]:
  "method E list_name append_name =
  (list_name, [Class list_name], Void, 3, 0, append_ins, [(1, 2, NullPointer, 7, 0)])"
(*<*)
  apply (insert class_list)
  apply (unfold list_class_def)
  apply (fastforce simp add: Method_def distinct_classes intro: method_def2 Methods.intros)
  done
(*>*)

lemma method_makelist [simp]:
  "method E test_name makelist_name =
  (test_name, [], Void, 3, 2, make_list_ins, [])"
(*<*)
  apply (insert class_test)
  apply (unfold test_class_def)
  apply (fastforce simp add: Method_def distinct_classes intro: method_def2 Methods.intros)
  done
(*>*)

lemma field_val [simp]:
  "field E list_name val_name = (list_name, Integer)"
(*<*)
  apply (insert class_list)
  apply (unfold list_class_def)
  apply (fastforce simp add: sees_field_def distinct_classes intro: field_def2 Fields.intros)
  done
(*>*)

lemma field_next [simp]:
  "field E list_name next_name = (list_name, Class list_name)"
(*<*)
  apply (insert class_list)
  apply (unfold list_class_def)
  apply (fastforce simp add: distinct_fields sees_field_def distinct_classes intro: field_def2 Fields.intros)
  done
(*>*)

lemma [simp]: "fields E Object = []"
  by (fastforce intro: fields_def2 Fields.intros)
 
lemma [simp]: "fields E NullPointer = []"
  by (fastforce simp add: distinct_classes intro: fields_def2 Fields.intros)

lemma [simp]: "fields E ClassCast = []"
  by (fastforce simp add: distinct_classes intro: fields_def2 Fields.intros)

lemma [simp]: "fields E OutOfMemory = []"
  by (fastforce simp add: distinct_classes intro: fields_def2 Fields.intros)

lemma [simp]: "fields E test_name = []"
(*<*)
  apply (insert class_test)
  apply (unfold test_class_def)
  apply (fastforce simp add: distinct_classes intro: fields_def2 Fields.intros)
  done
(*>*)

lemmas [simp] = is_class_def


subsection "Program structure"

text ‹
 The program is structurally wellformed:
 ›
lemma wf_struct:
  "wf_prog (λG C mb. True) E" (is "wf_prog ?mb E")
(*<*)
proof -
  have "distinct_fst E" 
    by (simp add: system_defs E_def class_defs distinct_classes)
  moreover
  have "set SystemClasses ⊆ set E" by (simp add: system_defs E_def)
  hence "wf_syscls E" by (rule wf_syscls)
  moreover
  have "wf_cdecl ?mb E ObjectC" by (simp add: wf_cdecl_def ObjectC_def)
  moreover
  have "wf_cdecl ?mb E NullPointerC" 
    by (auto elim: notin_rtrancl 
            simp add: wf_cdecl_def distinct_classes NullPointerC_def subcls1)
  moreover
  have "wf_cdecl ?mb E ClassCastC" 
    by (auto elim: notin_rtrancl 
            simp add: wf_cdecl_def distinct_classes ClassCastC_def subcls1)
  moreover
  have "wf_cdecl ?mb E OutOfMemoryC" 
    by (auto elim: notin_rtrancl 
            simp add: wf_cdecl_def distinct_classes OutOfMemoryC_def subcls1)
  moreover
  have "wf_cdecl ?mb E (list_name, list_class)"
    apply (auto elim!: notin_rtrancl 
            simp add: wf_cdecl_def wf_fdecl_def list_class_def 
                      wf_mdecl_def subcls1)
    apply (auto simp add: distinct_classes distinct_fields Method_def elim: Methods.cases)
    done    
  moreover
  have "wf_cdecl ?mb E (test_name, test_class)" 
    apply (auto elim!: notin_rtrancl 
            simp add: wf_cdecl_def wf_fdecl_def test_class_def 
                      wf_mdecl_def subcls1)
    apply (auto simp add: distinct_classes distinct_fields Method_def elim: Methods.cases)
    done       
  ultimately
  show ?thesis by (simp add: wf_prog_def E_def SystemClasses_def)
qed
(*>*)

subsection "Welltypings"
text ‹
 We show welltypings of the methods @{term append_name} in class @{term list_name},
 and @{term makelist_name} in class @{term test_name}:
 ›
lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def
(*declare app'Invoke [simp del]*)

definition phi_append :: ty_m (‹φ_a›)
where
  "φ_a ≡ map (λ(x,y). Some (x, map OK y)) [
   ( [], [Class list_name, Class list_name]),
   ( [Class list_name], [Class list_name, Class list_name]),
   ( [Class list_name], [Class list_name, Class list_name]),
   ( [Class list_name, Class list_name], [Class list_name, Class list_name]),
   ( [Class list_name, Class list_name], [Class list_name, Class list_name]),
   ([NT, Class list_name, Class list_name], [Class list_name, Class list_name]),
   ( [Boolean, Class list_name], [Class list_name, Class list_name]),

   ( [Class Object], [Class list_name, Class list_name]),
   ( [], [Class list_name, Class list_name]),
   ( [Class list_name], [Class list_name, Class list_name]),
   ( [Class list_name, Class list_name], [Class list_name, Class list_name]),
   ( [], [Class list_name, Class list_name]),
   ( [Void], [Class list_name, Class list_name]),

   ( [Class list_name], [Class list_name, Class list_name]),
   ( [Class list_name, Class list_name], [Class list_name, Class list_name]),
   ( [Void], [Class list_name, Class list_name])]"

text ‹
 The next definition and three proof rules implement an algorithm to
 enumarate natural numbers. The command ‹apply (elim pc_end pc_next pc_0›
 transforms a goal of the form
 @{prop [display] "pc < n ==> P pc"}
 into a series of goals
 @{prop [display] "P 0"}
 @{prop [display] "P (Suc 0)"}

 ‹…›

 @{prop [display] "P n"}
 ›
definition intervall :: "nat ==> nat ==> nat ==> bool" (‹_ ∈ [_, _')›)
where
  "x ∈ [a, b) ≡ a ≤ x ∧ x < b"

lemma pc_0: "x < n ==> (x ∈ [0, n) ==> P x) ==> P x"
  by (simp add: intervall_def)

lemma pc_next: "x ∈ [n0, n) ==> P n0 ==> (x ∈ [Suc n0, n) ==> P x) ==> P x"
(*<*)
  apply (cases "x=n0")
  apply (auto simp add: intervall_def)
  done
(*>*)

lemma pc_end: "x ∈ [n,n) ==> P x" 
  by (unfold intervall_def) arith


lemma types_append [simp]: "check_types E 3 (Suc (Suc 0)) (map OK φ_a)"
(*<*)
  by (auto simp add: check_types_def phi_append_def JVM_states_unfold)
(*>*)

lemma wt_append [simp]:
  "wt_method E list_name [Class list_name] Void 3 0 append_ins
             [(Suc 0, 2, NullPointer, 7, 0)] φ_a"
(*<*)
  apply (simp add: wt_method_def wt_start_def wt_instr_def)
  apply (simp add: append_ins_def phi_append_def)
  apply clarify
  apply (drule sym)
  apply (erule_tac P="x = y" for x y in rev_mp)
  apply (elim pc_end pc_next pc_0)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (fastforce simp add: matches_ex_entry_def subcls1
    relevant_entries_def is_relevant_entry_def sees_field_def list_class_def
    distinct_classes distinct_fields intro: Fields.intros)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (fastforce simp add:
    relevant_entries_def is_relevant_entry_def sees_field_def list_class_def
    distinct_classes distinct_fields intro: Fields.intros)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (fastforce simp add: relevant_entries_def is_relevant_entry_def subcls1)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (fastforce simp add:
    relevant_entries_def is_relevant_entry_def sees_field_def list_class_def
    distinct_classes distinct_fields intro: Fields.intros)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (fastforce simp add:
    relevant_entries_def is_relevant_entry_def list_class_def
    distinct_classes Method_def intro: Methods.intros)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  done
(*>*)

text ‹Some abbreviations for readability›
abbreviation "Clist == Class list_name"
abbreviation "Ctest == Class test_name"

definition phi_makelist :: ty_m (‹φ_m›)
where
  "φ_m ≡ map (λ(x,y). Some (x, y)) [
    ( [], [OK Ctest, Err , Err ]),
    ( [Clist], [OK Ctest, Err , Err ]),
    ( [], [OK Clist, Err , Err ]),
    ( [Clist], [OK Clist, Err , Err ]),
    ( [Integer, Clist], [OK Clist, Err , Err ]),

    ( [], [OK Clist, Err , Err ]),
    ( [Clist], [OK Clist, Err , Err ]),
    ( [], [OK Clist, OK Clist, Err ]),
    ( [Clist], [OK Clist, OK Clist, Err ]),
    ( [Integer, Clist], [OK Clist, OK Clist, Err ]),

    ( [], [OK Clist, OK Clist, Err ]),
    ( [Clist], [OK Clist, OK Clist, Err ]),
    ( [], [OK Clist, OK Clist, OK Clist]),
    ( [Clist], [OK Clist, OK Clist, OK Clist]),
    ( [Integer, Clist], [OK Clist, OK Clist, OK Clist]),

    ( [], [OK Clist, OK Clist, OK Clist]),
    ( [Clist], [OK Clist, OK Clist, OK Clist]),
    ( [Clist, Clist], [OK Clist, OK Clist, OK Clist]),
    ( [Void], [OK Clist, OK Clist, OK Clist]),
    ( [], [OK Clist, OK Clist, OK Clist]),
    ( [Clist], [OK Clist, OK Clist, OK Clist]),
    ( [Clist, Clist], [OK Clist, OK Clist, OK Clist]),
    ( [Void], [OK Clist, OK Clist, OK Clist])]"

lemma types_makelist [simp]: "check_types E 3 (Suc (Suc (Suc 0))) (map OK φ_m)"
(*<*)
  by (auto simp add: check_types_def phi_makelist_def JVM_states_unfold)
(*>*)

lemma wt_makelist [simp]:
  "wt_method E test_name [] Void 3 2 make_list_ins [] φ_m"
(*<*)
  apply (simp add: wt_method_def)
  apply (unfold make_list_ins_def phi_makelist_def)
  apply (simp add: wt_start_def eval_nat_numeral)
  apply (simp add: wt_instr_def)
  apply clarify
  apply (drule sym)
  apply (erule_tac P="x = y" for x y in rev_mp)
  apply (elim pc_end pc_next pc_0)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (fastforce simp add:
    relevant_entries_def is_relevant_entry_def sees_field_def list_class_def
    distinct_classes intro: Fields.intros)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (fastforce simp add:
    relevant_entries_def is_relevant_entry_def sees_field_def list_class_def
    distinct_classes intro: Fields.intros)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (fastforce simp add:
    relevant_entries_def is_relevant_entry_def sees_field_def list_class_def
    distinct_classes intro: Fields.intros)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (fastforce simp add:
    relevant_entries_def is_relevant_entry_def list_class_def
    distinct_classes Method_def intro: Methods.intros)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  apply (fastforce simp add:
    relevant_entries_def is_relevant_entry_def list_class_def
    distinct_classes Method_def intro: Methods.intros)
  apply (simp add: relevant_entries_def is_relevant_entry_def)
  done
(*>*)

lemma wf_md'E:
  "[ wf_prog wf_md P;
     ∧C S fs ms m.[(C,S,fs,ms) ∈ set P; m ∈ set ms] ==> wf_md' P C m ]
  ==> wf_prog wf_md' P"
(*<*)
  apply (simp add: wf_prog_def)
  apply auto
  apply (simp add: wf_cdecl_def wf_mdecl_def)
  apply fastforce
  done
(*>*)

text ‹The whole program is welltyped:›
definition Phi :: ty_P (‹Φ›)
where
  "Φ C mn ≡ if C = test_name ∧ mn = makelist_name then φ_m else
             if C = list_name ∧ mn = append_name then φ_a else []"

lemma wf_prog:
  "wf_jvm_prog_<Phi> E" 
(*<*)
  apply (unfold wf_jvm_prog_phi_def)
  apply (rule wf_md'E [OF wf_struct])
  apply (simp add: E_def)
  apply clarify
  apply (fold E_def)
  apply (simp add: system_defs class_defs Phi_def)
  apply auto
  apply (simp add: distinct_classes)
  done 
(*>*)


subsection "Conformance"
text ‹Execution of the program will be typesafe, because its
 start state conforms to the welltyping:›

lemma "E,Φ ⊨ start_state E test_name makelist_name √"
(*<*)
  apply (rule BV_correct_initial)
    apply (rule wf_prog)
  apply (fastforce simp add: test_class_def distinct_classes Method_def intro: Methods.intros)
  done
(*>*)


subsection "Example for code generation: inferring method types"

definition test_kil :: "jvm_prog ==> cname ==> ty list ==> ty ==> nat ==> nat ==>
             ex_table ==> instr list ==> ty_i' err list"
where
  "test_kil G C pTs rT mxs mxl et instr ≡
   (let first = Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err));
        start = OK first#(replicate (size instr - 1) (OK None))
    in kiljvm G mxs (1+size pTs+mxl) rT instr et start)"


lemma [code]:
  "unstables r step ss =
   fold (λp A. if ¬stable r step ss p then insert p A else A) [0..<size ss] {}"
proof -
  have "unstables r step ss = (UN p:{..<size ss}. if ¬stable r step ss p then {p} else {})"
    by (auto simp: unstables_def)
  also have "∧f. (UN p:{..<size ss}. f p) = Union (set (map f [0..<size ss]))" by auto
  also note Sup_set_fold also note fold_map
  also have "(∪) ∘ (λp. if ¬ stable r step ss p then {p} else {}) =
            (λp A. if ¬stable r step ss p then insert p A else A)"
    by(auto simp add: fun_eq_iff)
  finally show ?thesis .
qed

declare some_elem_def [code del]
code_printing
  constant some_elem ⇀ (SML) "(case/ _ of/ Set/ xs/ =>/ hd/ xs)"

text ‹This code setup is just a demonstration and \emph{not} sound!›
notepad begin
  have "some_elem (set [False, True]) = False" by eval
  moreover have "some_elem (set [True, False]) = True" by eval
  ultimately have False by (simp add: some_elem_def)
end

lemma [code]:
  "iter f step ss w = while (λ(ss, w). ¬ Set.is_empty w)
    (λ(ss, w).
        let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
    (ss, w)"
  by (simp add: iter_def)

lemma JVM_sup_unfold [code]:
 "JVM_SemiType.sup S m n = lift2 (Opt.sup
       (Product.sup (Listn.sup (SemiType.sup S))
         (λx y. OK (map2 (lift2 (SemiType.sup S)) x y))))" 
  by (auto simp: JVM_SemiType.sup_def JVM_SemiType.sl_def Opt.esl_def Err.sl_def
         stk_esl_def loc_sl_def Product.esl_def  
         Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def)

lemmas [code] = SemiType.sup_def [unfolded exec_lub_def] JVM_le_unfold

lemmas [code] = lesub_def plussub_def

lemma [code]:
  "is_refT T = (case T of NT ==> True | Class C ==> True | _ ==> False)"
  by (simp add: is_refT_def split: ty.split)

declare
  app_{i_Load} [code]
  app_{i_Store} [code]
  app_{i_Push} [code]

lemma [code]:
  "app_i (Getfield F C, P, pc, mxs, T_r, (T#ST, LT)) =
    Predicate.holds (Predicate.bind (sees_field_i_i_i_o_i P C F C) (λT_f. if P ⊨ T ≤ Class C then Predicate.single () else bot))"
  by (auto simp add: Predicate.holds_eq intro: sees_field_i_i_i_o_iI elim: sees_field_i_i_i_o_iE)

lemma [code]:
  "app_i (Putfield F C, P, pc, mxs, T_r, (T₁#T₂#ST, LT)) =
     Predicate.holds (Predicate.bind (sees_field_i_i_i_o_i P C F C) (λT_f. if P ⊨ T₂ ≤ (Class C) ∧ P ⊨ T₁ ≤ T_f then Predicate.single () else bot))"
  by (auto simp add: Predicate.holds_eq simp del: eval_bind split: if_split_asm elim!: sees_field_i_i_i_o_iE Predicate.bindE intro: Predicate.bindI sees_field_i_i_i_o_iI)

declare
  app_{i_New} [code]
  app_{i_Checkcast} [code]
  app_{i_Pop} [code]
  app_{i_IAdd} [code]
  app_{i_CmpEq} [code]
  app_{i_IfFalse} [code]
  app_{i_Goto} [code]
  app_{i_Return} [code]
  app_{i_Throw} [code]

lemma [code]:
  "app_i (Invoke M n, P, pc, mxs, T_r, (ST,LT)) =
    (n < length ST ∧
    (ST!n ≠ NT ⟶
      (case ST!n of
         Class C ==> Predicate.holds (Predicate.bind (Method_i_i_i_o_o_o_o P C M) (λ(Ts, T, m, D). if P ⊨ rev (take n ST) [≤] Ts then Predicate.single () else bot))
       | _ ==> False)))"
  by (fastforce simp add: Predicate.holds_eq simp del: eval_bind split: ty.split_asm if_split_asm intro: bindI Method_i_i_i_o_o_o_oI elim!: bindE Method_i_i_i_o_o_o_oE)

declare
  app_{i_default} [code]

lemmas [code] =
  widen.equation
  is_relevant_class.simps

definition test1 where
  "test1 = test_kil E list_name [Class list_name] Void 3 0
    [(Suc 0, 2, NullPointer, 7, 0)] append_ins"
definition test2 where
  "test2 = test_kil E test_name [] Void 3 2 [] make_list_ins"
definition test3 where "test3 = φ_a"
definition test4 where "test4 = φ_m"

ML_val ‹
 if @{code test1} = @{code map} @{code OK} @{code test3} then () else error "wrong result";
 if @{code test2} = @{code map} @{code OK} @{code test4} then () else error "wrong result"
 ›

end