Quelle  EConform.thy

(*  Title:      JinjaDCI/J/EConform.thy
    Author:     Susannah Mansky
    2019-20 UIUC
*)

section ‹ Expression conformance properties ›

theory EConform
imports SmallStep BigStep
begin

lemma cons_to_append: "list ≠ [] ⟶ (∃ls. a # list = ls @ [last list])"
 by (metis append_butlast_last_id last_ConsR list.simps(3))

subsection "Initialization conformance"

― ‹ returns class that can be initialized (if any) by top-level expression ›
fun init_class :: "'m prog ==> 'a exp ==> cname option" where
"init_class P (new C) = Some C" |
"init_class P (C∙_sF{D}) = Some D" |
"init_class P (C∙_sF{D}:=e₂) = Some D" |
"init_class P (C∙_sM(es)) = seeing_class P C M" |
"init_class _ _ = None"

lemma icheck_init_class: "icheck P C e ==> init_class P e = ⌊C⌋"
proof(induct e)
  case (SFAss x1 x2 x3 e')
  then show ?case by(case_tac e') auto
qed auto

― ‹ exp to take next small step (in particular, subexp that may contain initialization) ›
fun ss_exp :: "'a exp ==> 'a exp" and ss_exps :: "'a exp list ==> 'a exp option" where
  "ss_exp (new C) = new C"
| "ss_exp (Cast C e) = (case val_of e of Some v ==> Cast C e | _ ==> ss_exp e)"
| "ss_exp (Val v) = Val v"
| "ss_exp (e₁ «bop¬ e₂) = (case val_of e₁ of Some v ==> (case val_of e₂ of Some v ==> e₁ «bop¬ e₂ | _ ==> ss_exp e₂)
                                    | _ ==> ss_exp e₁)"
| "ss_exp (Var V) = Var V"
| "ss_exp (LAss V e) = (case val_of e of Some v ==> LAss V e | _ ==> ss_exp e)"
| "ss_exp (e∙F{D}) = (case val_of e of Some v ==> e∙F{D} | _ ==> ss_exp e)"
| "ss_exp (C∙_sF{D}) = C∙_sF{D}"
| "ss_exp (e₁∙F{D}:=e₂) = (case val_of e₁ of Some v ==> (case val_of e₂ of Some v ==> e₁∙F{D}:=e₂ | _ ==> ss_exp e₂)
                                    | _ ==> ss_exp e₁)"
| "ss_exp (C∙_sF{D}:=e₂) = (case val_of e₂ of Some v ==> C∙_sF{D}:=e₂ | _ ==> ss_exp e₂)"
| "ss_exp (e∙M(es)) = (case val_of e of Some v ==> (case map_vals_of es of Some t ==> e∙M(es) | _ ==> the(ss_exps es))
                                    | _ ==> ss_exp e)"
| "ss_exp (C∙_sM(es)) = (case map_vals_of es of Some t ==> C∙_sM(es) | _ ==> the(ss_exps es))"
| "ss_exp ({V:T; e}) = ss_exp e"
| "ss_exp (e₁;;e₂) = (case val_of e₁ of Some v ==> ss_exp e₂
           | None ==> (case lass_val_of e₁ of Some p ==> ss_exp e₂
                                           | None ==> ss_exp e₁))"
| "ss_exp (if (b) e₁ else e₂) = (case bool_of b of Some True ==> if (b) e₁ else e₂
                                        | Some False ==> if (b) e₁ else e₂
                                        | _ ==> ss_exp b)"
| "ss_exp (while (b) e) = while (b) e"
| "ss_exp (throw e) = (case val_of e of Some v ==> throw e | _ ==> ss_exp e)"
| "ss_exp (try e₁ catch(C V) e₂) = (case val_of e₁ of Some v ==> try e₁ catch(C V) e₂
                                            | _ ==> ss_exp e₁)"
| "ss_exp (INIT C (Cs,b) ← e) = INIT C (Cs,b) ← e"
| "ss_exp (RI (C,e);Cs ← e') = (case val_of e of Some v ==> RI (C,e);Cs ← e | _ ==> ss_exp e)"
| "ss_exps([]) = None"
| "ss_exps(e#es) = (case val_of e of Some v ==> ss_exps es | _ ==> Some (ss_exp e))"

(*<*)
lemmas ss_exp_ss_exps_induct = ss_exp_ss_exps.induct
 [ case_names New Cast Val BinOp Var LAss FAcc SFAcc FAss SFAss Call SCall
  Block Seq Cond While Throw Try Init RI Nil Cons ]
(*>*)

lemma icheck_ss_exp:
assumes "icheck P C e" shows "ss_exp e = e"
using assms
proof(cases e)
  case (SFAss C F D e) then show ?thesis using assms
  proof(cases e)qed(auto)
qed(auto)

lemma ss_exps_Vals_None[simp]:
 "ss_exps (map Val vs) = None"
 by(induct vs) (auto)

lemma ss_exps_Vals_NoneI:
 "ss_exps es = None ==> ∃vs. es = map Val vs"
using val_of_spec by(induct es) (auto)

lemma ss_exps_throw_nVal:
 "[ val_of e = None; ss_exps (map Val vs @ throw e # es') = ⌊e'⌋ ]
   ==> e' = ss_exp e"
 by(induct vs) (auto)

lemma ss_exps_throw_Val:
 "[ val_of e = ⌊a⌋; ss_exps (map Val vs @ throw e # es') = ⌊e'⌋ ]
   ==> e' = throw e"
 by(induct vs) (auto)


abbreviation curr_init :: "'m prog ==> 'a exp ==> cname option" where
"curr_init P e ≡ init_class P (ss_exp e)"
abbreviation curr_inits :: "'m prog ==> 'a exp list ==> cname option" where
"curr_inits P es ≡ case ss_exps es of Some e ==> init_class P e | _ ==> None"

lemma icheck_curr_init': "∧e'. ss_exp e = e' ==> icheck P C e' ==> curr_init P e = ⌊C⌋"
 and icheck_curr_inits': "∧e. ss_exps es = ⌊e⌋ ==> icheck P C e ==> curr_inits P es = ⌊C⌋"
proof(induct rule: ss_exp_ss_exps_induct)
qed(simp_all add: icheck_init_class)

lemma icheck_curr_init: "icheck P C e' ==> ss_exp e = e' ==> curr_init P e = ⌊C⌋"
 by(rule icheck_curr_init')

lemma icheck_curr_inits: "icheck P C e ==> ss_exps es = ⌊e⌋ ==> curr_inits P es = ⌊C⌋"
 by(rule icheck_curr_inits')

definition initPD :: "sheap ==> cname ==> bool" where
"initPD sh C ≡ ∃sfs i. sh C = Some (sfs, i) ∧ (i = Done ∨ i = Processing)"

― ‹ checks that @{text INIT} and @{text RI} conform and are only in the main computation ›
fun iconf :: "sheap ==> 'a exp ==> bool" and iconfs :: " sheap ==> 'a exp list ==> bool" where
  "iconf sh (new C) = True"
| "iconf sh (Cast C e) = iconf sh e"
| "iconf sh (Val v) = True"
| "iconf sh (e₁ «bop¬ e₂) = (case val_of e₁ of Some v ==> iconf sh e₂ | _ ==> iconf sh e₁ ∧ ¬sub_RI e₂)"
| "iconf sh (Var V) = True"
| "iconf sh (LAss V e) = iconf sh e"
| "iconf sh (e∙F{D}) = iconf sh e"
| "iconf sh (C∙_sF{D}) = True"
| "iconf sh (e₁∙F{D}:=e₂) = (case val_of e₁ of Some v ==> iconf sh e₂ | _ ==> iconf sh e₁ ∧ ¬sub_RI e₂)"
| "iconf sh (C∙_sF{D}:=e₂) = iconf sh e₂"
| "iconf sh (e∙M(es)) = (case val_of e of Some v ==> iconfs sh es | _ ==> iconf sh e ∧ ¬sub_RIs es)"
| "iconf sh (C∙_sM(es)) = iconfs sh es"
| "iconf sh ({V:T; e}) = iconf sh e"
| "iconf sh (e₁;;e₂) = (case val_of e₁ of Some v ==> iconf sh e₂
           | None ==> (case lass_val_of e₁ of Some p ==> iconf sh e₂
                                           | None ==> iconf sh e₁ ∧ ¬sub_RI e₂))"
| "iconf sh (if (b) e₁ else e₂) = (iconf sh b ∧ ¬sub_RI e₁ ∧ ¬sub_RI e₂)"
| "iconf sh (while (b) e) = (¬sub_RI b ∧ ¬sub_RI e)"
| "iconf sh (throw e) = iconf sh e"
| "iconf sh (try e₁ catch(C V) e₂) = (iconf sh e₁ ∧ ¬sub_RI e₂)"
| "iconf sh (INIT C (Cs,b) ← e) = ((case Cs of Nil ==> initPD sh C | C'#Cs' ==> last Cs = C) ∧ ¬sub_RI e)"
| "iconf sh (RI (C,e);Cs ← e') = (iconf sh e ∧ ¬sub_RI e')"
| "iconfs sh ([]) = True"
| "iconfs sh (e#es) = (case val_of e of Some v ==> iconfs sh es | _ ==> iconf sh e ∧ ¬sub_RIs es)"

lemma iconfs_map_throw: "iconfs sh (map Val vs @ throw e # es') ==> iconf sh e"
 by(induct vs,auto)

lemma nsub_RI_iconf_aux:
 "(¬sub_RI (e::'a exp) ⟶ (∀e'. e' ∈ subexp e ⟶ ¬sub_RI e' ⟶ iconf sh e') ⟶ iconf sh e)
 ∧ (¬sub_RIs (es::'a exp list) ⟶ (∀e'. e' ∈ subexps es ⟶ ¬sub_RI e' ⟶ iconf sh e') ⟶ iconfs sh es)"
proof(induct rule: sub_RI_sub_RIs.induct) qed(auto)

lemma nsub_RI_iconf_aux':
 "(∧e'. subexp_of e' e ==> ¬sub_RI e' ⟶ iconf sh e') ==> (¬sub_RI e ==> iconf sh e)"
 by(simp add: nsub_RI_iconf_aux)

lemma nsub_RI_iconf: "¬sub_RI e ==> iconf sh e"
  and nsub_RIs_iconfs: "¬sub_RIs es ==> iconfs sh es"
proof -
  let ?R = "λe. ¬sub_RI e ⟶ iconf sh e"
  let ?Rs = "λes. ¬sub_RIs es ⟶ iconfs sh es"
  have "(∀e'. subexp_of e' e ⟶ ?R e') ∧ ?R e"
    by(rule subexp_induct[where ?Rs = ?Rs]; clarsimp simp: nsub_RI_iconf_aux)
  moreover have "(∀e'. e' ∈ subexps es ⟶ ?R e') ∧ ?Rs es"
    by(rule subexps_induct; clarsimp simp: nsub_RI_iconf_aux)
  ultimately show "¬sub_RI e ==> iconf sh e"
              and "¬sub_RIs es ==> iconfs sh es" by simp+
qed

lemma lass_val_of_iconf: "lass_val_of e = ⌊a⌋ ==> iconf sh e"
 by(drule lass_val_of_nsub_RI, erule nsub_RI_iconf)

lemma icheck_iconf:
assumes "icheck P C e" shows "iconf sh e"
using assms
proof(cases e)
  case (SFAss C F D e) then show ?thesis using assms
  proof(cases e)qed(auto)
next
  case (SCall C M es) then show ?thesis using assms
    by (auto simp: nsub_RIs_iconfs)
next
qed(auto)


subsection "Indicator boolean conformance"

― ‹ checks that the given expression, indicator boolean pair is allowed in small-step
 (i.e., if @{term b} is True, then @{term e} is an initialization-calling expression to
 a class that is marked either @{term Processing} or @{term Done}) ›
definition bconf :: "'m prog ==> sheap ==> 'a exp ==> bool ==> bool"  (‹_,_ ⊨_b '(_,_') √› [51,51,0,0] 50)
where
  "P,sh ⊨_b (e,b) √ ≡ b ⟶ (∃C. icheck P C (ss_exp e) ∧ initPD sh C)"

definition bconfs :: "'m prog ==> sheap ==> 'a exp list ==> bool ==> bool"  (‹_,_ ⊨_b '(_,_') √› [51,51,0,0] 50)
where
  "P,sh ⊨_b (es,b) √ ≡ b ⟶ (∃C. (icheck P C (the(ss_exps es))
                           ∧ (curr_inits P es = Some C) ∧ initPD sh C))"


― ‹ bconf helper lemmas ›

lemma bconf_nonVal[simp]:
 "P,sh ⊨_b (e,True) √ ==> val_of e = None"
 by(cases e) (auto simp: bconf_def)

lemma bconfs_nonVals[simp]:
 "P,sh ⊨_b (es,True) √ ==> map_vals_of es = None"
 by(induct es) (auto simp: bconfs_def)

lemma bconf_Cast[iff]:
 "P,sh ⊨_b (Cast C e,b) √ ⟷ P,sh ⊨_b (e,b) √"
 by(cases b) (auto simp: bconf_def dest: val_of_spec)

lemma bconf_BinOp[iff]:
 "P,sh ⊨_b (e1 «bop¬ e2,b) √
   ⟷ (case val_of e1 of Some v ==> P,sh ⊨_b (e2,b) √ | _ ==> P,sh ⊨_b (e1,b) √)"
 by(cases b) (auto simp: bconf_def dest: val_of_spec)

lemma bconf_LAss[iff]:
 "P,sh ⊨_b (LAss V e,b) √ ⟷ P,sh ⊨_b (e,b) √"
 by(cases b) (auto simp: bconf_def dest: val_of_spec)

lemma bconf_FAcc[iff]:
 "P,sh ⊨_b (e∙F{D},b) √ ⟷ P,sh ⊨_b (e,b) √"
 by(cases b) (auto simp: bconf_def dest: val_of_spec)

lemma bconf_FAss[iff]:
 "P,sh ⊨_b (FAss e1 F D e2,b) √
   ⟷ (case val_of e1 of Some v ==> P,sh ⊨_b (e2,b) √ | _ ==> P,sh ⊨_b (e1,b) √)"
 by(cases b) (auto simp: bconf_def dest: val_of_spec)

lemma bconf_SFAss[iff]:
"val_of e2 = None ==> P,sh ⊨_b (SFAss C F D e2,b) √ ⟷ P,sh ⊨_b (e2,b) √"
 by(cases b) (auto simp: bconf_def)

lemma bconfs_Vals[iff]:
 "P,sh ⊨_b (map Val vs, b) √ ⟷ ¬ b"
 by(unfold bconfs_def) simp

lemma bconf_Call[iff]:
 "P,sh ⊨_b (e∙M(es),b) √
   ⟷ (case val_of e of Some v ==> P,sh ⊨_b (es,b) √ | _ ==> P,sh ⊨_b (e,b) √)"
proof(cases b)
  case True
  then show ?thesis
  proof(cases "ss_exps es")
    case None
    then obtain vs where "es = map Val vs" using ss_exps_Vals_NoneI by auto
    then have mv: "map_vals_of es = ⌊vs⌋" by simp
    then show ?thesis by(auto simp: bconf_def) (simp add: bconfs_def)
  next
    case (Some a)
    then show ?thesis by(auto simp: bconf_def) (auto simp: bconfs_def icheck_init_class)
  qed
qed(simp add: bconf_def bconfs_def)

lemma bconf_SCall[iff]:
assumes mvn: "map_vals_of es = None"
shows "P,sh ⊨_b (C∙_sM(es),b) √ ⟷ P,sh ⊨_b (es,b) √"
proof(cases b)
  case True
  then show ?thesis
  proof(cases "ss_exps es")
    case None
      then have "∃vs. es = map Val vs" using ss_exps_Vals_NoneI by auto
      then show ?thesis using mvn finals_def by clarsimp
    next
    case (Some a)
      then show ?thesis by(auto simp: bconf_def) (auto simp: bconfs_def icheck_init_class)
    qed
qed(simp add: bconf_def bconfs_def)

lemma bconf_Cons[iff]:
 "P,sh ⊨_b (e#es,b) √
   ⟷ (case val_of e of Some v ==> P,sh ⊨_b (es,b) √ | _ ==> P,sh ⊨_b (e,b) √)"
proof(cases b)
  case True
  then show ?thesis
  proof(cases "ss_exps es")
    case None
      then have "∃vs. es = map Val vs" using ss_exps_Vals_NoneI by auto
      then show ?thesis using None by(auto simp: bconf_def bconfs_def icheck_init_class)
    next
    case (Some a)
      then show ?thesis by(auto simp: bconf_def bconfs_def icheck_init_class)
    qed
qed(simp add: bconf_def bconfs_def)

lemma bconf_InitBlock[iff]:
 "P,sh ⊨_b ({V:T; V:=Val v;; e₂},b) √ ⟷ P,sh ⊨_b (e₂,b) √"
 by(cases b) (auto simp: bconf_def assigned_def)

lemma bconf_Block[iff]:
 "P,sh ⊨_b ({V:T; e},b) √ ⟷ P,sh ⊨_b (e,b) √"
 by(cases b) (auto simp: bconf_def)

lemma bconf_Seq[iff]:
 "P,sh ⊨_b (e1;;e2,b) √
   ⟷ (case val_of e1 of Some v ==> P,sh ⊨_b (e2,b) √
                             | _ ==> (case lass_val_of e1 of Some p ==> P,sh ⊨_b (e2,b) √
                                                          | None ==> P,sh ⊨_b (e1,b) √))"
 by(cases b) (auto simp: bconf_def dest: val_of_spec lass_val_of_spec)

lemma bconf_Cond[iff]:
 "P,sh ⊨_b (if (b) e₁ else e₂,b') √ ⟷ P,sh ⊨_b (b,b') √"
proof(cases "bool_of b")
  case None
  then show ?thesis by(auto simp: bconf_def)
next
  case (Some a)
  then show ?thesis by(case_tac a) (auto simp: bconf_def dest: bool_of_specT bool_of_specF)
qed

lemma bconf_While[iff]:
 "P,sh ⊨_b (while (b) e,b') √ ⟷ ¬b'"
 by(cases b) (auto simp: bconf_def)

lemma bconf_Throw[iff]:
 "P,sh ⊨_b (throw e,b) √ ⟷ P,sh ⊨_b (e,b) √"
 by(cases b) (auto simp: bconf_def dest: val_of_spec)

lemma bconf_Try[iff]:
 "P,sh ⊨_b (try e₁ catch(C V) e₂,b) √ ⟷ P,sh ⊨_b (e₁,b) √"
 by(cases b) (auto simp: bconf_def dest: val_of_spec)

lemma bconf_INIT[iff]:
 "P,sh ⊨_b (INIT C (Cs,b') ← e,b) √ ⟷ ¬b"
 by(cases b) (auto simp: bconf_def)

lemma bconf_RI[iff]:
 "P,sh ⊨_b (RI(C,e);Cs ← e',b) √ ⟷ P,sh ⊨_b (e,b) √"
 by(cases b) (auto simp: bconf_def dest: val_of_spec)

lemma bconfs_map_throw[iff]:
 "P,sh ⊨_b (map Val vs @ throw e # es',b) √ ⟷ P,sh ⊨_b (e,b) √"
 by(induct vs) auto

end