Theory EConform

(*  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⇩2) = 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⇩1 «bop» e⇩2) = (case val_of e⇩1 of Some v ⇒ (case val_of e⇩2 of Some v ⇒ e⇩1 «bop» e⇩2 | _ ⇒ ss_exp e⇩2)
                                    | _ ⇒ ss_exp e⇩1)"
| "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⇩1∙F{D}:=e⇩2) = (case val_of e⇩1 of Some v ⇒ (case val_of e⇩2 of Some v ⇒ e⇩1∙F{D}:=e⇩2 | _ ⇒ ss_exp e⇩2)
                                    | _ ⇒ ss_exp e⇩1)"
| "ss_exp (C∙⇩sF{D}:=e⇩2) = (case val_of e⇩2 of Some v ⇒ C∙⇩sF{D}:=e⇩2 | _ ⇒ ss_exp e⇩2)"
| "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⇩1;;e⇩2) = (case val_of e⇩1 of Some v ⇒ ss_exp e⇩2
           | None ⇒ (case lass_val_of e⇩1 of Some p ⇒ ss_exp e⇩2
                                           | None ⇒ ss_exp e⇩1))"
| "ss_exp (if (b) e⇩1 else e⇩2) = (case bool_of b of Some True ⇒ if (b) e⇩1 else e⇩2
                                        | Some False ⇒ if (b) e⇩1 else e⇩2
                                        | _ ⇒ 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⇩1 catch(C V) e⇩2) = (case val_of e⇩1 of Some v ⇒ try e⇩1 catch(C V) e⇩2
                                            | _ ⇒ ss_exp e⇩1)"
| "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⇩1 «bop» e⇩2) = (case val_of e⇩1 of Some v ⇒ iconf sh e⇩2 | _ ⇒ iconf sh e⇩1 ∧ ¬sub_RI e⇩2)"
| "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⇩1∙F{D}:=e⇩2) = (case val_of e⇩1 of Some v ⇒ iconf sh e⇩2 | _ ⇒ iconf sh e⇩1 ∧ ¬sub_RI e⇩2)"
| "iconf sh (C∙⇩sF{D}:=e⇩2) = iconf sh e⇩2"
| "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⇩1;;e⇩2) = (case val_of e⇩1 of Some v ⇒ iconf sh e⇩2
           | None ⇒ (case lass_val_of e⇩1 of Some p ⇒ iconf sh e⇩2
                                           | None ⇒ iconf sh e⇩1 ∧ ¬sub_RI e⇩2))"
| "iconf sh (if (b) e⇩1 else e⇩2) = (iconf sh b ∧ ¬sub_RI e⇩1 ∧ ¬sub_RI e⇩2)"
| "iconf sh (while (b) e) = (¬sub_RI b ∧ ¬sub_RI e)"
| "iconf sh (throw e) = iconf sh e"
| "iconf sh (try e⇩1 catch(C V) e⇩2) = (iconf sh e⇩1 ∧ ¬sub_RI e⇩2)"
| "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⇩2},b) √ ⟷ P,sh ⊢⇩b (e⇩2,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⇩1 else e⇩2,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⇩1 catch(C V) e⇩2,b) √ ⟷ P,sh ⊢⇩b (e⇩1,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