theory VSpace_C

lemma armv_contextSwitch_ccorres:
  "ccorres dc xfdc (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask asid_bits))
                   (UNIV \<inter> {s. cap_pd_' s =  pde_Ptr pd} \<inter> {s. asid_' s = asid} ) []
       (armv_contextSwitch pd asid) (Call armv_contextSwitch_'proc)" apply (cinit lift: cap_pd_' asid_') apply simp apply (ctac(no_vcg) add: getHWASID_ccorres) apply (ctac (no_vcg)add: armv_contextSwitch_HWASID_ccorres) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) (UNIV \<inter> \<lbrace>\<acute>cap_pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>) [] (armv_contextSwitch pd asid) (Call armv_contextSwitch_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>asida cap_pd. \<lbrakk>asida = asid; cap_pd = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q110 asida cap_pd) (?Q'110 asida cap_pd) [SKIP] (do hwasid <- getHWASID asid;
doMachineOp (armv_contextSwitch_HWASID pd hwasid)
od) (\<acute>ret__unsigned_char :== CALL getHWASID_'proc(asida);;
CALL armv_contextSwitch_HWASID_'proc(cap_pd,\<acute>ret__unsigned_char))
 2. \<And>asida cap_pd s s'. \<lbrakk>asida = asid; cap_pd = pde_Ptr pd; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q110 asida cap_pd s \<and> s' \<in> ?Q'110 asida cap_pd proof (prove)
goal (2 subgoals):
 1. \<And>asida cap_pd. \<lbrakk>asida = asid; cap_pd = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q110 asid (pde_Ptr pd)) (?Q'110 asid (pde_Ptr pd)) [SKIP] (do hwasid <- getHWASID asid;
doMachineOp (armv_contextSwitch_HWASID pd hwasid)
od) (\<acute>ret__unsigned_char :== CALL getHWASID_'proc(asid);;
CALL armv_contextSwitch_HWASID_'proc(pde_Ptr pd,\<acute>ret__unsigned_char))
 2. \<And>asida cap_pd s s'. \<lbrakk>asida = asid; cap_pd = pde_Ptr pd; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q110 asida cap_pd s \<and> s' \<in> ?Q'110 asida cap_pd proof (prove)
goal (3 subgoals):
 1. \<And>asida cap_pd rv ret__unsigned_char. \<lbrakk>asida = asid; cap_pd = pde_Ptr pd; rv = ret__unsigned_char\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q121 asida cap_pd rv) (?Q'135 rv ret__unsigned_char) [SKIP] (doMachineOp (armv_contextSwitch_HWASID pd rv)) (CALL armv_contextSwitch_HWASID_'proc(pde_Ptr pd,ret__unsigned_char))
 2. \<And>asida cap_pd. \<lbrakk>asida = asid; cap_pd = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R129 asid (pde_Ptr pd)\<rbrace> getHWASID asid \<lbrace>?Q121 asida cap_pd\<rbrace>
 3. \<And>asida cap_pd s s'. \<lbrakk>asida = asid; cap_pd = pde_Ptr pd; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R129 asida cap_pd) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_char_' t \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_char_' := ret__unsigned_char_' t\<rparr> \<in> ?Q'134 asida cap_pd t rv}
flex-flex pairs:
\<lambda>t rv. ?Q'135 rv (ret__unsigned_char_' t) \<equiv>\<^sup>? ?Q'134 asid (pde_Ptr pd) proof (prove)
goal (2 subgoals):
 1. \<And>asida cap_pd. \<lbrakk>asida = asid; cap_pd = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R129 asid (pde_Ptr pd)\<rbrace> getHWASID asid \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>asida cap_pd s s'. \<lbrakk>asida = asid; cap_pd = pde_Ptr pd; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R129 asida cap_pd) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_char_' t \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_char_' := ret__unsigned_char_' t\<rparr> \<in> {s. hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (cap_pd_'_update (\<lambda>_. cap_pd) s) \<in> UNIV \<inter> \<lbrace>\<acute>cap_pd = cap_pd\<rbrace> \<inter> \<lbrace>\<acute>hw_asid = rv\<rbrace>}} proof (prove)
goal (1 subgoal):
 1. \<And>asida cap_pd s s'. \<lbrakk>asida = asid; cap_pd = pde_Ptr pd; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asida \<le> mask local.asid_bits) and (\<lambda>a. True)) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_char_' t \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_char_' := ret__unsigned_char_' t\<rparr> \<in> {s. hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (cap_pd_'_update (\<lambda>_. cap_pd) s) \<in> UNIV \<inter> \<lbrace>\<acute>cap_pd = cap_pd\<rbrace> \<inter> \<lbrace>\<acute>hw_asid = rv\<rbrace>}} proof (prove)
goal:
No subgoals!