theory VSpace_C

lemma flushPage_ccorres:
  "ccorres dc xfdc (invs' and (\<lambda>s. asid \<le> mask asid_bits \<and> is_aligned vptr pageBits))
      (UNIV \<inter> {s. gen_framesize_to_H (page_size_' s) = sz
                     \<and> page_size_' s < 4}
            \<inter> {s. pd_' s = pde_Ptr pd} \<inter> {s. asid_' s = asid}
            \<inter> {s. vptr_' s = vptr}) []
      (flushPage sz pd asid vptr) (Call flushPage_'proc)" apply (cinit lift: page_size_' pd_' asid_' vptr_') apply (rule ccorres_assert) apply (simp del: Collect_const) apply (ctac(no_vcg) add: setVMRootForFlush_ccorres) apply (ctac(no_vcg) add: loadHWASID_ccorres) apply csymbr apply (simp add: when_def del: Collect_const) apply (rule ccorres_cond2[where R=\<top>]) apply (clarsimp simp: pde_stored_asid_def to_bool_def split: if_split) apply (rule ccorres_Guard_Seq ccorres_rhs_assoc)+ apply csymbr apply csymbr apply (ctac(no_vcg) add: invalidateTranslationSingle_ccorres) apply (rule ccorres_cond2[where R=\<top>]) apply (simp add: from_bool_0 Collect_const_mem) apply (rule ccorres_pre_getCurThread) apply (ctac add: setVMRoot_ccorres) apply (rule ccorres_return_Skip) apply (wp | simp add: cur_tcb'_def[symmetric])+ apply (rule_tac Q="\<lambda>_ s. invs' s \<and> cur_tcb' s" in hoare_post_imp) apply (simp add: invs'_invs_no_cicd) apply (wp | simp add: cur_tcb'_def[symmetric])+ apply (rule ccorres_return_Skip) apply wp apply (simp only: pred_conj_def simp_thms) apply (strengthen invs_valid_pde_mappings') apply (wp hoare_drop_imps setVMRootForFlush_invs') apply (clarsimp simp: Collect_const_mem word_sle_def) apply (rule conjI, clarsimp+) apply (clarsimp simp: pde_stored_asid_def to_bool_def ucast_ucast_mask
                  cong: conj_cong) apply (drule is_aligned_neg_mask_eq) apply (simp add: pde_pde_invalid_lift_def pde_lift_def mask_def[where n=8]
                   word_bw_assocs mask_def[where n=pageBits]) apply (simp add: pageBits_def mask_eq_iff_w2p word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) (UNIV \<inter> \<lbrace>gen_framesize_to_H \<acute>page_size = sz \<and> \<acute>page_size < 4\<rbrace> \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vptr = vptr\<rbrace>) [] (flushPage sz pd asid vptr) (Call flushPage_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1347 vptra asida pda page_size) (?Q'1347 vptra asida pda page_size) [SKIP] (do y <- assert (vptr && mask pageBits = 0);
root_switched <- setVMRootForFlush pd asid;
maybe_hw_asid <- loadHWASID asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid)));
when root_switched (getCurThread >>= setVMRoot)
od)
od) (\<acute>root_switched :== CALL setVMRootForFlush_'proc(pda,asida);;
(\<acute>stored_hw_asid___struct_pde_C :== CALL loadHWASID_'proc(asida);;
(\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_asid_valid_'proc(\<acute>stored_hw_asid___struct_pde_C);;
IF \<acute>ret__unsigned \<noteq> 0 THEN
  \<acute>base_addr :== vptra && 0xFFFFF000;;
\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(\<acute>stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationSingle_'proc(\<acute>base_addr || UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
IF \<acute>root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI
FI)))
 2. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q1347 vptra asida pda page_size s \<and> s' \<in> ?Q'1347 vptra asida pda page_size proof (prove)
goal (2 subgoals):
 1. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1347 vptra asida pda page_size) (?Q'1347 vptra asida pda page_size) [SKIP] (do root_switched <- setVMRootForFlush pd asid;
maybe_hw_asid <- loadHWASID asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid)));
when root_switched (getCurThread >>= setVMRoot)
od)
od) (\<acute>root_switched :== CALL setVMRootForFlush_'proc(pda,asida);;
(\<acute>stored_hw_asid___struct_pde_C :== CALL loadHWASID_'proc(asida);;
(\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_asid_valid_'proc(\<acute>stored_hw_asid___struct_pde_C);;
IF \<acute>ret__unsigned \<noteq> 0 THEN
  \<acute>base_addr :== vptra && 0xFFFFF000;;
\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(\<acute>stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationSingle_'proc(\<acute>base_addr || UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
IF \<acute>root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI
FI)))
 2. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q1347 vptra asida pda page_size s \<and> s' \<in> ?Q'1347 vptra asida pda page_size proof (prove)
goal (2 subgoals):
 1. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1347 vptr asid (pde_Ptr pd) page_size) (?Q'1347 vptr asid (pde_Ptr pd) page_size) [SKIP] (do root_switched <- setVMRootForFlush pd asid;
maybe_hw_asid <- loadHWASID asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid)));
when root_switched (getCurThread >>= setVMRoot)
od)
od) (\<acute>root_switched :== CALL setVMRootForFlush_'proc(pde_Ptr pd,asid);;
(\<acute>stored_hw_asid___struct_pde_C :== CALL loadHWASID_'proc(asid);;
(\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_asid_valid_'proc(\<acute>stored_hw_asid___struct_pde_C);;
IF \<acute>ret__unsigned \<noteq> 0 THEN
  \<acute>base_addr :== vptr && 0xFFFFF000;;
\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(\<acute>stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationSingle_'proc(\<acute>base_addr || \<acute>ret__unsigned);;
IF \<acute>root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI
FI)))
 2. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q1347 vptra asida pda page_size s \<and> s' \<in> ?Q'1347 vptra asida pda page_size proof (prove)
goal (3 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1359 vptra asida pda page_size rv) (?Q'1373 page_size rv root_switched) [SKIP] (do maybe_hw_asid <- loadHWASID asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid)));
when rv (getCurThread >>= setVMRoot)
od)
od) (\<acute>stored_hw_asid___struct_pde_C :== CALL loadHWASID_'proc(asid);;
(\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_asid_valid_'proc(\<acute>stored_hw_asid___struct_pde_C);;
IF \<acute>ret__unsigned \<noteq> 0 THEN
  \<acute>base_addr :== vptr && 0xFFFFF000;;
\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(\<acute>stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationSingle_'proc(\<acute>base_addr || \<acute>ret__unsigned);;
IF root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI
FI))
 2. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>?Q1359 vptra asida pda page_size\<rbrace>
 3. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?Q'1372 vptra asida pda page_size t rv}
flex-flex pairs:
\<lambda>page_size t rv. ?Q'1373 page_size rv (ret__unsigned_long_' t) \<equiv>\<^sup>? ?Q'1372 vptr asid (pde_Ptr pd) proof (prove)
goal (4 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched rva stored_hw_asid___struct_pde_C. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; rva = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1625 vptra asida pda page_size rv root_switched rva) (?Q'1643 page_size rv root_switched rva stored_hw_asid___struct_pde_C) [SKIP] (when (\<exists>y. rva = Some y) (do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the rva)));
when rv (getCurThread >>= setVMRoot)
od)) (\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_asid_valid_'proc(stored_hw_asid___struct_pde_C);;
IF \<acute>ret__unsigned \<noteq> 0 THEN
  \<acute>base_addr :== vptr && 0xFFFFF000;;
\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationSingle_'proc(\<acute>base_addr || \<acute>ret__unsigned);;
IF root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI
FI)
 2. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>?Q1625 vptra asida pda page_size rv root_switched\<rbrace>
 3. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 4. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> ?Q'1644 vptra asida pda page_size t rv ta rva}}
flex-flex pairs:
?Q'1644 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Q'1643 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (4 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1625 vptra asida pda page_size rv root_switched (pde_stored_asid stored_hw_asid___struct_pde_C)) (?G'1870 page_size rv root_switched (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [SKIP] (when (\<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y) (do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C))));
when rv (getCurThread >>= setVMRoot)
od)) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>base_addr :== vptr && 0xFFFFF000;;
\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationSingle_'proc(\<acute>base_addr || \<acute>ret__unsigned);;
IF root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI
FI)
 2. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>?Q1625 vptra asida pda page_size rv root_switched\<rbrace>
 3. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 4. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> ?G'1871 vptra asida pda page_size t rv ta rva v}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?G'1871 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?G'1870 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (4 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1625 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?G'1870 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C))));
if rv then getCurThread >>= setVMRoot else return ()
od else return ()) (IF stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C) \<noteq> 0 THEN
  \<acute>base_addr :== vptr && 0xFFFFF000;;
\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationSingle_'proc(\<acute>base_addr || \<acute>ret__unsigned);;
IF rv THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI
FI)
 2. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>?Q1625 vptra asida pda page_size rv root_switched\<rbrace>
 3. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 4. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> ?G'1871 vptra asida pda page_size t rv ta rva v}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?G'1871 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?G'1870 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (6 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<longrightarrow> (\<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y) = (s' \<in> \<lbrace>stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C) \<noteq> 0\<rbrace>)
 2. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt2010 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rt2004 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C))));
if rv then getCurThread >>= setVMRoot else return ()
od) (\<acute>base_addr :== vptr && 0xFFFFF000;;
\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationSingle_'proc(\<acute>base_addr || \<acute>ret__unsigned);;
IF rv THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI)
 3. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2008 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf2002 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) SKIP
 4. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ?Pt2010 vptra asida pda page_size rv root_switched a s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf2008 vptra asida pda page_size rv root_switched a s)\<rbrace>
 5. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 6. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rt2007 vptra asida pda page_size t rv ta rva v) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf2006 vptra asida pda page_size t rv ta rva v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?Rt2007 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rt2004 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta)
?Rf2006 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2002 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (5 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt2010 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rt2004 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C))));
if rv then getCurThread >>= setVMRoot else return ()
od) (\<acute>base_addr :== vptr && 0xFFFFF000;;
\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationSingle_'proc(\<acute>base_addr || \<acute>ret__unsigned);;
IF rv THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI)
 2. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2008 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf2002 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) SKIP
 3. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ?Pt2010 vptra asida pda page_size rv root_switched a s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf2008 vptra asida pda page_size rv root_switched a s)\<rbrace>
 4. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 5. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rt2007 vptra asida pda page_size t rv ta rva v) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf2006 vptra asida pda page_size t rv ta rva v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?Rt2007 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rt2004 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta)
?Rf2006 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2002 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (5 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt2010 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rt2004 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C))));
if rv then getCurThread >>= setVMRoot else return ()
od) (\<acute>base_addr :== vptr && 0xFFFFF000;;
(\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
(CALL invalidateTranslationSingle_'proc(\<acute>base_addr || \<acute>ret__unsigned);;
IF rv THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI)))
 2. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2008 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf2002 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) SKIP
 3. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ?Pt2010 vptra asida pda page_size rv root_switched a s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf2008 vptra asida pda page_size rv root_switched a s)\<rbrace>
 4. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 5. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rt2007 vptra asida pda page_size t rv ta rva v) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf2006 vptra asida pda page_size t rv ta rva v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?Rt2007 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rt2004 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta)
?Rf2006 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2002 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (5 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt2010 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?G'2036 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C))));
if rv then getCurThread >>= setVMRoot else return ()
od) (\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
(CALL invalidateTranslationSingle_'proc(vptr && 0xFFFFF000 || \<acute>ret__unsigned);;
IF rv THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI))
 2. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2008 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf2002 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) SKIP
 3. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ?Pt2010 vptra asida pda page_size rv root_switched a s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf2008 vptra asida pda page_size rv root_switched a s)\<rbrace>
 4. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 5. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> ?G'2038 vptra asida pda page_size t rv ta rva v}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf2006 vptra asida pda page_size t rv ta rva v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?G'2038 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?G'2036 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta)
?Rf2006 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2002 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (5 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt2010 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?G'2185 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) ret__unsigned) [SKIP] (do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C))));
if rv then getCurThread >>= setVMRoot else return ()
od) (CALL invalidateTranslationSingle_'proc(vptr && 0xFFFFF000 || ret__unsigned);;
IF rv THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI)
 2. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2008 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf2002 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) SKIP
 3. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ?Pt2010 vptra asida pda page_size rv root_switched a s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf2008 vptra asida pda page_size rv root_switched a s)\<rbrace>
 4. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 5. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> ?G'2187 vptra asida pda page_size t rv ta rva v va}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf2006 vptra asida pda page_size t rv ta rva v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?G'2187 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?G'2185 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta)
?Rf2006 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2002 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (6 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva xfdca. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q2298 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva) (?Q'2316 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva xfdca) [SKIP] (if rv then getCurThread >>= setVMRoot else return ()) (IF rv THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI)
 2. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<lbrace>?R2310 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C)))) \<lbrace>?Q2298 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned\<rbrace>
 3. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2008 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf2002 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) SKIP
 4. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and ?R2310 vptra asida pda page_size rv root_switched a) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf2008 vptra asida pda page_size rv root_switched a s)\<rbrace>
 5. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 6. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. vptr_'_update (\<lambda>_. vptra && 0xFFFFF000 || va) s \<in> \<lbrace>\<acute>vptr = vptra || UCAST(8 \<rightarrow> 32) (the rva)\<rbrace>} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> ?Q'2317 vptra asida pda page_size t rv ta rva v va tb rvb}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf2006 vptra asida pda page_size t rv ta rva v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?Q'2317 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Q'2315 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta)
\<lambda>page_size rv stored_hw_asid___struct_pde_C ret__unsigned t rva. ?Q'2316 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva (xfdc t) \<equiv>\<^sup>? \<lambda>page_size rv stored_hw_asid___struct_pde_C. ?Q'2315 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))
?Rf2006 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2002 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (8 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva xfdc. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); dc rva xfdc\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<longrightarrow> rv = (s' \<in> \<lbrace>rv\<rbrace>)
 2. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva xfdca. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt2371 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva) (?Rt2363 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva xfdca) [SKIP] (getCurThread >>= setVMRoot) (CALL setVMRoot_'proc(\<acute>ksCurThread))
 3. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva xfdca. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2369 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva) (?Rf2361 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva xfdca) [SKIP] (return ()) SKIP
 4. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<lbrace>?R2310 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C)))) \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. rv \<longrightarrow> ?Pt2371 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned a s) and (\<lambda>s. \<not> rv \<longrightarrow> ?Pf2369 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned a s)\<rbrace>
 5. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2008 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf2002 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) SKIP
 6. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and ?R2310 vptra asida pda page_size rv root_switched a) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf2008 vptra asida pda page_size rv root_switched a s)\<rbrace>
 7. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 8. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. vptr_'_update (\<lambda>_. vptra && 0xFFFFF000 || va) s \<in> \<lbrace>\<acute>vptr = vptra || UCAST(8 \<rightarrow> 32) (the rva)\<rbrace>} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> ?Rt2367 vptra asida pda page_size t rv ta rva v va tb rvb) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> ?Rf2366 vptra asida pda page_size t rv ta rva v va tb rvb)}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf2006 vptra asida pda page_size t rv ta rva v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?Rt2367 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rt2365 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta)
?Rf2366 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2364 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta)
\<lambda>page_size rv stored_hw_asid___struct_pde_C. ?Rt2365 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) \<equiv>\<^sup>? \<lambda>page_size rv stored_hw_asid___struct_pde_C ret__unsigned t rva. ?Rt2363 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva (xfdc t)
\<lambda>page_size rv stored_hw_asid___struct_pde_C. ?Rf2364 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) \<equiv>\<^sup>? \<lambda>page_size rv stored_hw_asid___struct_pde_C ret__unsigned t rva. ?Rf2361 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva (xfdc t)
?Rf2006 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2002 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (7 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva xfdca. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt2371 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva) (?Rt2363 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva xfdca) [SKIP] (getCurThread >>= setVMRoot) (CALL setVMRoot_'proc(\<acute>ksCurThread))
 2. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva xfdca. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2369 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva) (?Rf2361 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva xfdca) [SKIP] (return ()) SKIP
 3. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<lbrace>?R2310 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C)))) \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. rv \<longrightarrow> ?Pt2371 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned a s) and (\<lambda>s. \<not> rv \<longrightarrow> ?Pf2369 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned a s)\<rbrace>
 4. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2008 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf2002 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) SKIP
 5. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and ?R2310 vptra asida pda page_size rv root_switched a) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf2008 vptra asida pda page_size rv root_switched a s)\<rbrace>
 6. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 7. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. vptr_'_update (\<lambda>_. vptra && 0xFFFFF000 || va) s \<in> \<lbrace>\<acute>vptr = vptra || UCAST(8 \<rightarrow> 32) (the rva)\<rbrace>} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> ?Rt2367 vptra asida pda page_size t rv ta rva v va tb rvb) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> ?Rf2366 vptra asida pda page_size t rv ta rva v va tb rvb)}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf2006 vptra asida pda page_size t rv ta rva v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?Rt2367 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rt2365 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta)
?Rf2366 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2364 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta)
\<lambda>page_size rv stored_hw_asid___struct_pde_C. ?Rt2365 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) \<equiv>\<^sup>? \<lambda>page_size rv stored_hw_asid___struct_pde_C ret__unsigned t rva. ?Rt2363 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva (xfdc t)
\<lambda>page_size rv stored_hw_asid___struct_pde_C. ?Rf2364 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) \<equiv>\<^sup>? \<lambda>page_size rv stored_hw_asid___struct_pde_C ret__unsigned t rva. ?Rf2361 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva (xfdc t)
?Rf2006 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2002 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (7 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva xfdca rvb. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>a. ?P2384 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva a rvb) (?P'2381 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva xfdca rvb) [SKIP] (setVMRoot rvb) (CALL setVMRoot_'proc(\<acute>ksCurThread))
 2. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva xfdca. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2369 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva) (?Rf2361 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva xfdca) [SKIP] (return ()) SKIP
 3. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<lbrace>?R2310 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C)))) \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. rv \<longrightarrow> (\<forall>rva. ksCurThread s = rva \<longrightarrow> ?P2384 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned a s rva)) and (\<lambda>s. \<not> rv \<longrightarrow> ?Pf2369 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned a s)\<rbrace>
 4. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2008 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf2002 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) SKIP
 5. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and ?R2310 vptra asida pda page_size rv root_switched a) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf2008 vptra asida pda page_size rv root_switched a s)\<rbrace>
 6. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 7. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. vptr_'_update (\<lambda>_. vptra && 0xFFFFF000 || va) s \<in> \<lbrace>\<acute>vptr = vptra || UCAST(8 \<rightarrow> 32) (the rva)\<rbrace>} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rvc. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rvc \<longrightarrow> s \<in> ?P'2383 vptra asida pda page_size t rv ta rva v va tb rvb rvc}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> ?Rf2366 vptra asida pda page_size t rv ta rva v va tb rvb)}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf2006 vptra asida pda page_size t rv ta rva v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?P'2383 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?P'2382 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta)
\<lambda>page_size rv stored_hw_asid___struct_pde_C. ?P'2382 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) \<equiv>\<^sup>? \<lambda>page_size rv stored_hw_asid___struct_pde_C ret__unsigned t rva. ?P'2381 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva (xfdc t)
?Rf2366 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2364 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta)
\<lambda>page_size rv stored_hw_asid___struct_pde_C. ?Rf2364 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) \<equiv>\<^sup>? \<lambda>page_size rv stored_hw_asid___struct_pde_C ret__unsigned t rva. ?Rf2361 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva (xfdc t)
?Rf2006 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2002 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (6 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva xfdca. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2369 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva) (?Rf2361 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva xfdca) [SKIP] (return ()) SKIP
 2. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<lbrace>?R2310 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C)))) \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. rv \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' rv) s)) and (\<lambda>s. \<not> rv \<longrightarrow> ?Pf2369 vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned a s)\<rbrace>
 3. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2008 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf2002 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) SKIP
 4. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and ?R2310 vptra asida pda page_size rv root_switched a) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf2008 vptra asida pda page_size rv root_switched a s)\<rbrace>
 5. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 6. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. vptr_'_update (\<lambda>_. vptra && 0xFFFFF000 || va) s \<in> \<lbrace>\<acute>vptr = vptra || UCAST(8 \<rightarrow> 32) (the rva)\<rbrace>} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> ?Rf2366 vptra asida pda page_size t rv ta rva v va tb rvb)}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf2006 vptra asida pda page_size t rv ta rva v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?Rf2366 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2364 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta)
\<lambda>page_size rv stored_hw_asid___struct_pde_C. ?Rf2364 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) \<equiv>\<^sup>? \<lambda>page_size rv stored_hw_asid___struct_pde_C ret__unsigned t rva. ?Rf2361 page_size rv stored_hw_asid___struct_pde_C ret__unsigned rva (xfdc t)
?Rf2006 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2002 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (5 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<lbrace>?R2310 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C)))) \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. rv \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' rv) s)) and (\<lambda>s. \<not> rv \<longrightarrow> True)\<rbrace>
 2. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2008 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf2002 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) SKIP
 3. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and ?R2310 vptra asida pda page_size rv root_switched a) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf2008 vptra asida pda page_size rv root_switched a s)\<rbrace>
 4. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 5. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>v v'. v = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. vptr_'_update (\<lambda>_. vptra && 0xFFFFF000 || v) s \<in> \<lbrace>\<acute>vptr = vptra || UCAST(8 \<rightarrow> 32) (the rva)\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf2006 vptra asida pda page_size t rv ta rva v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?Rf2006 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2002 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (5 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<lbrace>?P'2410 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C)))) \<lbrace>\<lambda>rva s. rv \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s \<and> cur_tcb' s\<rbrace>
 2. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2008 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf2002 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) SKIP
 3. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>b. True \<and> ?P'2410 vptra asida pda page_size rv root_switched a b)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf2008 vptra asida pda page_size rv root_switched a s)\<rbrace>
 4. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 5. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>v v'. v = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. vptr_'_update (\<lambda>_. vptra && 0xFFFFF000 || v) s \<in> \<lbrace>\<acute>vptr = vptra || UCAST(8 \<rightarrow> 32) (the rva)\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf2006 vptra asida pda page_size t rv ta rva v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?Rf2006 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2002 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (6 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned rva s. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); invs' s \<and> cur_tcb' s\<rbrakk> \<Longrightarrow> rv \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s \<and> cur_tcb' s
 2. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<lbrace>?P'2410 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C)))) \<lbrace>\<lambda>_ s. invs' s \<and> cur_tcb' s\<rbrace>
 3. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2008 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf2002 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) SKIP
 4. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>b. True \<and> ?P'2410 vptra asida pda page_size rv root_switched a b)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf2008 vptra asida pda page_size rv root_switched a s)\<rbrace>
 5. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 6. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>v v'. v = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. vptr_'_update (\<lambda>_. vptra && 0xFFFFF000 || v) s \<in> \<lbrace>\<acute>vptr = vptra || UCAST(8 \<rightarrow> 32) (the rva)\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf2006 vptra asida pda page_size t rv ta rva v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?Rf2006 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2002 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (5 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<lbrace>?P'2410 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid stored_hw_asid___struct_pde_C)))) \<lbrace>\<lambda>_ s. invs' s \<and> cur_tcb' s\<rbrace>
 2. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2008 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf2002 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) SKIP
 3. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>b. True \<and> ?P'2410 vptra asida pda page_size rv root_switched a b)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf2008 vptra asida pda page_size rv root_switched a s)\<rbrace>
 4. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 5. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>v v'. v = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. vptr_'_update (\<lambda>_. vptra && 0xFFFFF000 || v) s \<in> \<lbrace>\<acute>vptr = vptra || UCAST(8 \<rightarrow> 32) (the rva)\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf2006 vptra asida pda page_size t rv ta rva v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?Rf2006 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2002 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (4 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf2008 vptr asid (pde_Ptr pd) page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf2002 page_size rv (from_bool rv) (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) SKIP
 2. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> invs' a \<and> cur_tcb' a)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf2008 vptra asida pda page_size rv root_switched a s)\<rbrace>
 3. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 4. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>ta rva. rva = pde_stored_asid (ret__struct_pde_C_' ta) \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals ta, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>v v'. v = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. vptr_'_update (\<lambda>_. vptra && 0xFFFFF000 || v) s \<in> \<lbrace>\<acute>vptr = vptra || UCAST(8 \<rightarrow> 32) (the rva)\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf2006 vptra asida pda page_size t rv ta rva v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' ta) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}}
flex-flex pairs:
?Rf2006 vptr asid (pde_Ptr pd) \<equiv>\<^sup>? \<lambda>page_size t rv ta rva. ?Rf2002 page_size rv (ret__unsigned_long_' t) rva (ret__struct_pde_C_' ta) proof (prove)
goal (3 subgoals):
 1. \<And>vptra asida pda page_size rv root_switched. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1638 vptra asida pda page_size rv\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> invs' a \<and> cur_tcb' a)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> True)\<rbrace>
 2. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R1638 vptra asida pda page_size a\<rbrace>
 3. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rva. rva = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>v v'. v = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. vptr_'_update (\<lambda>_. vptra && 0xFFFFF000 || v) s \<in> \<lbrace>\<acute>vptr = vptra || UCAST(8 \<rightarrow> 32) (the rva)\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (2 subgoals):
 1. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and (\<lambda>a. ((\<lambda>_. True) and (\<lambda>s. (\<exists>y. map_option fst (armKSASIDMap (ksArchState a) asid) = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> invs' a \<and> cur_tcb' a)) s) and (\<lambda>s. (\<nexists>y. map_option fst (armKSASIDMap (ksArchState a) asid) = Some y) \<longrightarrow> True)) a)\<rbrace>
 2. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rva. rva = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>v v'. v = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. vptr_'_update (\<lambda>_. vptra && 0xFFFFF000 || v) s \<in> \<lbrace>\<acute>vptr = vptra || UCAST(8 \<rightarrow> 32) (the rva)\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (2 subgoals):
 1. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>a b. (valid_pde_mappings' b \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>y. map_option fst (armKSASIDMap (ksArchState b) asid) = Some y) \<longrightarrow> invs' b \<and> cur_tcb' b)\<rbrace>
 2. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rva. rva = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>v v'. v = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. vptr_'_update (\<lambda>_. vptra && 0xFFFFF000 || v) s \<in> \<lbrace>\<acute>vptr = vptra || UCAST(8 \<rightarrow> 32) (the rva)\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (2 subgoals):
 1. \<And>vptra asida pda page_size. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; vptr && mask pageBits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1367 vptr asid (pde_Ptr pd) page_size\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>r s. (invs' s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>y. map_option fst (armKSASIDMap (ksArchState s) asid) = Some y) \<longrightarrow> invs' s \<and> cur_tcb' s)\<rbrace>
 2. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R1367 vptra asida pda page_size) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rva. rva = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>v v'. v = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. vptr_'_update (\<lambda>_. vptra && 0xFFFFF000 || v) s \<in> \<lbrace>\<acute>vptr = vptra || UCAST(8 \<rightarrow> 32) (the rva)\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (1 subgoal):
 1. \<And>vptra asida pda page_size s s'. \<lbrakk>vptra = vptr; asida = asid; pda = pde_Ptr pd; gen_framesize_to_H page_size = sz \<and> page_size < 4; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> is_aligned vptr pageBits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. asida \<le> mask local.asid_bits) and (\<lambda>a. invs' a \<and> asida \<le> mask local.asid_bits \<and> invs' a \<and> cur_tcb' a)) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rva. rva = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. base_addr_'_update (\<lambda>_. vptra && 0xFFFFF000) s \<in> {s. \<forall>v v'. v = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. vptr_'_update (\<lambda>_. vptra && 0xFFFFF000 || v) s \<in> \<lbrace>\<acute>vptr = vptra || UCAST(8 \<rightarrow> 32) (the rva)\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (1 subgoal):
 1. \<And>page_size s s'. \<lbrakk>(s, s') \<in> rf_sr; page_size < 4; sz = gen_framesize_to_H page_size; invs' s; asid \<le> mask local.asid_bits; is_aligned vptr pageBits\<rbrakk> \<Longrightarrow> cur_tcb' s \<and> ((\<exists>t rv. ret__unsigned_long_' t = from_bool rv) \<longrightarrow> (\<forall>t. pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> stored_asid_valid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' t)) \<noteq> 0 \<longrightarrow> vptr && 0xFFFFF000 || stored_hw_asid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' t)) = vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid (ret__struct_pde_C_' t))))) proof (prove)
goal (1 subgoal):
 1. \<And>page_size s s' t rv ta. \<lbrakk>(s, s') \<in> rf_sr; page_size < 4; sz = gen_framesize_to_H page_size; invs' s; asid \<le> mask local.asid_bits; is_aligned vptr pageBits; ret__unsigned_long_' t = from_bool rv; pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; stored_asid_valid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' ta)) \<noteq> 0\<rbrakk> \<Longrightarrow> vptr && 0xFFFFF000 || stored_hw_asid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' ta)) = vptr || UCAST(8 \<rightarrow> 32) (the (pde_stored_asid (ret__struct_pde_C_' ta))) proof (prove)
goal (1 subgoal):
 1. \<And>page_size s s' t rv ta. \<lbrakk>(s, s') \<in> rf_sr; page_size < 4; sz = gen_framesize_to_H page_size; invs' s; asid \<le> mask local.asid_bits; is_aligned vptr pageBits; ret__unsigned_long_' t = from_bool rv; pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; stored_asid_valid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' ta)) \<noteq> 0\<rbrakk> \<Longrightarrow> vptr && 0xFFFFF000 || stored_hw_asid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' ta)) = vptr || stored_hw_asid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' ta)) && mask 8 proof (prove)
goal (1 subgoal):
 1. \<And>page_size s s' t rv ta. \<lbrakk>(s, s') \<in> rf_sr; page_size < 4; sz = gen_framesize_to_H page_size; invs' s; asid \<le> mask local.asid_bits; ret__unsigned_long_' t = from_bool rv; pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; stored_asid_valid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' ta)) \<noteq> 0; vptr && ~~ mask pageBits = vptr\<rbrakk> \<Longrightarrow> vptr && 0xFFFFF000 || stored_hw_asid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' ta)) = vptr || stored_hw_asid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' ta)) && mask 8 proof (prove)
goal (1 subgoal):
 1. \<And>page_size s s' t rv ta. \<lbrakk>(s, s') \<in> rf_sr; page_size < 4; sz = gen_framesize_to_H page_size; invs' s; asid \<le> mask local.asid_bits; ret__unsigned_long_' t = from_bool rv; pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; (pde_C.words_C (ret__struct_pde_C_' ta).[0] >> 23) && 1 = 1; vptr && ~~ (2 ^ pageBits - 1) = vptr\<rbrakk> \<Longrightarrow> vptr && 0xFFFFF000 || (pde_C.words_C (ret__struct_pde_C_' ta).[0] >> 24) && 0xFF = vptr || (pde_C.words_C (ret__struct_pde_C_' ta).[0] >> 24) && 0xFF proof (prove)
goal:
No subgoals!