theory Finalise_C

lemma unmapPageTable_ccorres:
  "ccorres dc xfdc (invs' and (\<lambda>s. asid \<le> mask asid_bits \<and> vaddr < pptrBase))
      (UNIV \<inter> {s. asid_' s = asid} \<inter> {s. vaddr_' s = vaddr} \<inter> {s. pt_' s = Ptr ptPtr}) []
      (unmapPageTable asid vaddr ptPtr) (Call unmapPageTable_'proc)" apply (rule ccorres_gen_asm) apply (cinit lift: asid_' vaddr_' pt_') apply (ctac(no_vcg) add: pageTableMapped_ccorres) apply wpc apply (simp add: option_to_ptr_def option_to_0_def ccorres_cond_iffs) apply (rule ccorres_return_Skip) apply (simp add: option_to_ptr_def option_to_0_def ccorres_cond_iffs) apply (rule ccorres_rhs_assoc)+ apply csymbr apply (rule ccorres_move_array_assertion_pd) apply csymbr apply csymbr apply (rule ccorres_split_nothrow_novcg_dc) apply (rule storePDE_Basic_ccorres) apply (simp add: cpde_relation_def Let_def pde_lift_pde_invalid) apply csymbr apply (ctac add: cleanByVA_PoU_ccorres) apply (ctac(no_vcg) add:flushTable_ccorres) apply wp apply (vcg exspec=cleanByVA_PoU_modifies) apply wp apply (fastforce simp: guard_is_UNIV_def Collect_const_mem Let_def
      shiftl_t2n field_simps lookup_pd_slot_def) apply (rule_tac Q="\<lambda>rv s. (case rv of Some pd \<Rightarrow> page_directory_at' pd s | _ \<Rightarrow> True) \<and> invs' s"
             in hoare_post_imp) apply (clarsimp simp: lookup_pd_slot_def Let_def
                          mask_add_aligned less_pptrBase_valid_pde_offset''
                          page_directory_at'_def) apply (wp pageTableMapped_pd) apply (clarsimp simp: word_sle_def lookup_pd_slot_def
                        Let_def shiftl_t2n field_simps
                        Collect_const_mem pdBits_def pageBits_def) apply (simp add: unat_shiftr_le_bound unat_eq_0 pdeBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and (\<lambda>s. asid \<le> mask local.asid_bits \<and> vaddr < pptrBase)) (UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>) [] (unmapPageTable asid vaddr ptPtr) (Call unmapPageTable_'proc) proof (prove)
goal (1 subgoal):
 1. asid \<le> mask local.asid_bits \<and> vaddr < pptrBase \<Longrightarrow> ccorres dc xfdc invs' (UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>) [] (unmapPageTable asid vaddr ptPtr) (Call unmapPageTable_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1111 pt vaddra asida) (?Q'1111 pt vaddra asida) [SKIP] (do maybePD <- pageTableMapped asid vaddr ptPtr;
case maybePD of None \<Rightarrow> return () | Some pd \<Rightarrow> do pdSlot <- return (lookupPDSlot pd vaddr);
storePDE pdSlot ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr pdSlot) (addrFromPPtr pdSlot);
flushTable pd asid vaddr
od
od) (\<acute>pd :== CALL pageTableMapped_'proc(asida,vaddra,pt);;
IF \<acute>pd \<noteq> NULL THEN
  \<acute>pdIndex :== vaddra >> 20;;
Guard MemorySafety \<lbrace>\<acute>pdIndex = 0 \<or> array_assertion \<acute>pd (unat \<acute>pdIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>pdSlot :== \<acute>pd +\<^sub>p uint \<acute>pdIndex);;
\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c pdSlot_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>pdSlot \<acute>ret__struct_pde_C)));;
\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) \<acute>pdSlot);;
CALL cleanByVA_PoU_'proc(ptr_val \<acute>pdSlot,\<acute>ret__unsigned_long);;
CALL flushTable_'proc(\<acute>pd,asida,vaddra,pt)
FI)
 2. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q1111 pt vaddra asida s \<and> s' \<in> ?Q'1111 pt vaddra asida proof (prove)
goal (3 subgoals):
 1. \<And>pt vaddra asida rv pd. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; pd = option_to_ptr rv \<and> rv \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1119 pt vaddra asida rv) (?Q'1119 pt vaddra asida rv pd) [SKIP] (case rv of None \<Rightarrow> return () | Some pd \<Rightarrow> do pdSlot <- return (lookupPDSlot pd vaddr);
storePDE pdSlot ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr pdSlot) (addrFromPPtr pdSlot);
flushTable pd asid vaddr
od) (IF pd \<noteq> NULL THEN
  \<acute>pdIndex :== vaddra >> 20;;
Guard MemorySafety \<lbrace>\<acute>pdIndex = 0 \<or> array_assertion pd (unat \<acute>pdIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>pdSlot :== pd +\<^sub>p uint \<acute>pdIndex);;
\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c pdSlot_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>pdSlot \<acute>ret__struct_pde_C)));;
\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) \<acute>pdSlot);;
CALL cleanByVA_PoU_'proc(ptr_val \<acute>pdSlot,\<acute>ret__unsigned_long);;
CALL flushTable_'proc(pd,asida,vaddra,pt)
FI)
 2. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>?Q1119 pt vaddra asida\<rbrace>
 3. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?Q'1119 pt vaddra asida rv (ret__ptr_to_struct_pde_C_' t)} proof (prove)
goal (4 subgoals):
 1. \<And>pt vaddra asida rv pd. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; pd = option_to_ptr rv \<and> rv \<noteq> Some 0; rv = None\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1326 pt vaddra asida rv) (?R''1328 pt vaddra asida rv pd) [SKIP] (return ()) (IF pd \<noteq> NULL THEN
  \<acute>pdIndex :== vaddra >> 20;;
Guard MemorySafety \<lbrace>\<acute>pdIndex = 0 \<or> array_assertion pd (unat \<acute>pdIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>pdSlot :== pd +\<^sub>p uint \<acute>pdIndex);;
\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c pdSlot_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>pdSlot \<acute>ret__struct_pde_C)));;
\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) \<acute>pdSlot);;
CALL cleanByVA_PoU_'proc(ptr_val \<acute>pdSlot,\<acute>ret__unsigned_long);;
CALL flushTable_'proc(pd,asida,vaddra,pt)
FI)
 2. \<And>pt vaddra asida rv pd x2. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; pd = option_to_ptr rv \<and> rv \<noteq> Some 0; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1327 pt vaddra asida rv x2) (?R''1329 pt vaddra asida rv pd x2) [SKIP] (do pdSlot <- return (lookupPDSlot x2 vaddr);
storePDE pdSlot ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr pdSlot) (addrFromPPtr pdSlot);
flushTable x2 asid vaddr
od) (IF pd \<noteq> NULL THEN
  \<acute>pdIndex :== vaddra >> 20;;
Guard MemorySafety \<lbrace>\<acute>pdIndex = 0 \<or> array_assertion pd (unat \<acute>pdIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>pdSlot :== pd +\<^sub>p uint \<acute>pdIndex);;
\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c pdSlot_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>pdSlot \<acute>ret__struct_pde_C)));;
\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) \<acute>pdSlot);;
CALL cleanByVA_PoU_'proc(ptr_val \<acute>pdSlot,\<acute>ret__unsigned_long);;
CALL flushTable_'proc(pd,asida,vaddra,pt)
FI)
 3. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> ?R1326 pt vaddra asida rv s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R1327 pt vaddra asida rv x s)\<rbrace>
 4. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''1328 pt vaddra asida rv (ret__ptr_to_struct_pde_C_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''1329 pt vaddra asida rv (ret__ptr_to_struct_pde_C_' t) x}}} proof (prove)
goal (4 subgoals):
 1. \<And>pt vaddra asida rv pd. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; pd = NULL; rv = None\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1326 (pte_Ptr ptPtr) vaddr asid None) (?R''1328 (pte_Ptr ptPtr) vaddr asid None NULL) [SKIP] (return ()) SKIP
 2. \<And>pt vaddra asida rv pd x2. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; pd = option_to_ptr rv \<and> rv \<noteq> Some 0; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1327 pt vaddra asida rv x2) (?R''1329 pt vaddra asida rv pd x2) [SKIP] (do pdSlot <- return (lookupPDSlot x2 vaddr);
storePDE pdSlot ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr pdSlot) (addrFromPPtr pdSlot);
flushTable x2 asid vaddr
od) (IF pd \<noteq> NULL THEN
  \<acute>pdIndex :== vaddra >> 20;;
Guard MemorySafety \<lbrace>\<acute>pdIndex = 0 \<or> array_assertion pd (unat \<acute>pdIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>pdSlot :== pd +\<^sub>p uint \<acute>pdIndex);;
\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c pdSlot_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>pdSlot \<acute>ret__struct_pde_C)));;
\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) \<acute>pdSlot);;
CALL cleanByVA_PoU_'proc(ptr_val \<acute>pdSlot,\<acute>ret__unsigned_long);;
CALL flushTable_'proc(pd,asida,vaddra,pt)
FI)
 3. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> ?R1326 pt vaddra asida rv s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R1327 pt vaddra asida rv x s)\<rbrace>
 4. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''1328 pt vaddra asida rv (ret__ptr_to_struct_pde_C_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''1329 pt vaddra asida rv (ret__ptr_to_struct_pde_C_' t) x}}} proof (prove)
goal (3 subgoals):
 1. \<And>pt vaddra asida rv pd x2. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; pd = option_to_ptr rv \<and> rv \<noteq> Some 0; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1327 pt vaddra asida rv x2) (?R''1329 pt vaddra asida rv pd x2) [SKIP] (do pdSlot <- return (lookupPDSlot x2 vaddr);
storePDE pdSlot ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr pdSlot) (addrFromPPtr pdSlot);
flushTable x2 asid vaddr
od) (IF pd \<noteq> NULL THEN
  \<acute>pdIndex :== vaddra >> 20;;
Guard MemorySafety \<lbrace>\<acute>pdIndex = 0 \<or> array_assertion pd (unat \<acute>pdIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>pdSlot :== pd +\<^sub>p uint \<acute>pdIndex);;
\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c pdSlot_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>pdSlot \<acute>ret__struct_pde_C)));;
\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) \<acute>pdSlot);;
CALL cleanByVA_PoU_'proc(ptr_val \<acute>pdSlot,\<acute>ret__unsigned_long);;
CALL flushTable_'proc(pd,asida,vaddra,pt)
FI)
 2. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R1327 pt vaddra asida rv x s)\<rbrace>
 3. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''1329 pt vaddra asida rv (ret__ptr_to_struct_pde_C_' t) x}}} proof (prove)
goal (3 subgoals):
 1. \<And>pt vaddra asida rv x2. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1327 (pte_Ptr ptPtr) vaddr asid (Some x2) x2) (?R''1329 (pte_Ptr ptPtr) vaddr asid (Some x2) (pde_Ptr x2) x2) [SKIP] (do y <- storePDE (lookup_pd_slot x2 vaddr) ARM_H.InvalidPDE;
y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot x2 vaddr) (addrFromPPtr (lookup_pd_slot x2 vaddr)));
flushTable x2 asid vaddr
od) (\<acute>pdIndex :== vaddr >> 20;;
Guard MemorySafety \<lbrace>\<acute>pdIndex = 0 \<or> array_assertion (pde_Ptr x2) (unat \<acute>pdIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>pdSlot :== pde_Ptr (x2 + \<acute>pdIndex * 4));;
\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(0,0);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c pdSlot_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>pdSlot \<acute>ret__struct_pde_C)));;
\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) \<acute>pdSlot);;
CALL cleanByVA_PoU_'proc(ptr_val \<acute>pdSlot,\<acute>ret__unsigned_long);;
CALL flushTable_'proc(pde_Ptr x2,asid,vaddr,pte_Ptr ptPtr))
 2. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R1327 pt vaddra asida rv x s)\<rbrace>
 3. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''1329 pt vaddra asida rv (ret__ptr_to_struct_pde_C_' t) x}}} proof (prove)
goal (3 subgoals):
 1. \<And>pt vaddra asida rv x2. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1327 (pte_Ptr ptPtr) vaddr asid (Some x2) x2) (?R''1329 (pte_Ptr ptPtr) vaddr asid (Some x2) (pde_Ptr x2) x2) [SKIP] (do y <- storePDE (lookup_pd_slot x2 vaddr) ARM_H.InvalidPDE;
y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot x2 vaddr) (addrFromPPtr (lookup_pd_slot x2 vaddr)));
flushTable x2 asid vaddr
od) (\<acute>pdIndex :== vaddr >> 20;;
(Guard MemorySafety \<lbrace>\<acute>pdIndex = 0 \<or> array_assertion (pde_Ptr x2) (unat \<acute>pdIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>pdSlot :== pde_Ptr (x2 + \<acute>pdIndex * 4));;
(\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(0,0);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c pdSlot_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>pdSlot \<acute>ret__struct_pde_C)));;
(\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) \<acute>pdSlot);;
(CALL cleanByVA_PoU_'proc(ptr_val \<acute>pdSlot,\<acute>ret__unsigned_long);;
CALL flushTable_'proc(pde_Ptr x2,asid,vaddr,pte_Ptr ptPtr)))))))
 2. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R1327 pt vaddra asida rv x s)\<rbrace>
 3. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''1329 pt vaddra asida rv (ret__ptr_to_struct_pde_C_' t) x}}} proof (prove)
goal (3 subgoals):
 1. \<And>pt vaddra asida rv x2. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1327 (pte_Ptr ptPtr) vaddr asid (Some x2) x2) (?G'1379 (pte_Ptr ptPtr) vaddr asid (Some x2) (pde_Ptr x2) x2) [SKIP] (do y <- storePDE (lookup_pd_slot x2 vaddr) ARM_H.InvalidPDE;
y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot x2 vaddr) (addrFromPPtr (lookup_pd_slot x2 vaddr)));
flushTable x2 asid vaddr
od) (Guard MemorySafety \<lbrace>vaddr >> 20 = 0 \<or> array_assertion (pde_Ptr x2) (unat (vaddr >> 20)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>pdSlot :== pde_Ptr (x2 + (vaddr >> 20) * 4));;
(\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(0,0);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c pdSlot_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>pdSlot \<acute>ret__struct_pde_C)));;
(\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) \<acute>pdSlot);;
(CALL cleanByVA_PoU_'proc(ptr_val \<acute>pdSlot,\<acute>ret__unsigned_long);;
CALL flushTable_'proc(pde_Ptr x2,asid,vaddr,pte_Ptr ptPtr))))))
 2. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R1327 pt vaddra asida rv x s)\<rbrace>
 3. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> ?G'1379 pt vaddra asida rv (ret__ptr_to_struct_pde_C_' t) x}}}} proof (prove)
goal (3 subgoals):
 1. \<And>pt vaddra asida rv x2. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A1551 (pte_Ptr ptPtr) vaddr asid (Some x2) x2) (?C'1548 (pte_Ptr ptPtr) vaddr asid (Some x2) (pde_Ptr x2) x2) [SKIP] (do y <- storePDE (lookup_pd_slot x2 vaddr) ARM_H.InvalidPDE;
y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot x2 vaddr) (addrFromPPtr (lookup_pd_slot x2 vaddr)));
flushTable x2 asid vaddr
od) (\<acute>pdSlot :== pde_Ptr (x2 + (vaddr >> 20) * 4);;
(\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(0,0);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c pdSlot_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>pdSlot \<acute>ret__struct_pde_C)));;
(\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) \<acute>pdSlot);;
(CALL cleanByVA_PoU_'proc(ptr_val \<acute>pdSlot,\<acute>ret__unsigned_long);;
CALL flushTable_'proc(pde_Ptr x2,asid,vaddr,pte_Ptr ptPtr))))))
 2. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> (?A1551 pt vaddra asida rv x and page_directory_at' x) s)\<rbrace>
 3. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> ?C'1548 pt vaddra asida rv (ret__ptr_to_struct_pde_C_' t) x \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (3 subgoals):
 1. \<And>pt vaddra asida rv x2. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A1551 (pte_Ptr ptPtr) vaddr asid (Some x2) x2) (?G'1562 (pte_Ptr ptPtr) vaddr asid (Some x2) (pde_Ptr x2) x2) [SKIP] (do y <- storePDE (lookup_pd_slot x2 vaddr) ARM_H.InvalidPDE;
y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot x2 vaddr) (addrFromPPtr (lookup_pd_slot x2 vaddr)));
flushTable x2 asid vaddr
od) (\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(0,0);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c pde_Ptr (x2 + (vaddr >> 20) * 4)} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr (x2 + (vaddr >> 20) * 4)) \<acute>ret__struct_pde_C)));;
(\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) (pde_Ptr (x2 + (vaddr >> 20) * 4)));;
(CALL cleanByVA_PoU_'proc(ptr_val (pde_Ptr (x2 + (vaddr >> 20) * 4)),\<acute>ret__unsigned_long);;
CALL flushTable_'proc(pde_Ptr x2,asid,vaddr,pte_Ptr ptPtr)))))
 2. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> (?A1551 pt vaddra asida rv x and page_directory_at' x) s)\<rbrace>
 3. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> {s. pdSlot_'_update (\<lambda>_. pde_Ptr (x + (vaddra >> 20) * 4)) s \<in> ?G'1562 pt vaddra asida rv (ret__ptr_to_struct_pde_C_' t) x} \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (3 subgoals):
 1. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A1551 (pte_Ptr ptPtr) vaddr asid (Some x2) x2) (?G'1715 (pte_Ptr ptPtr) vaddr asid (Some x2) (pde_Ptr x2) x2 ret__struct_pde_C) [SKIP] (do y <- storePDE (lookup_pd_slot x2 vaddr) ARM_H.InvalidPDE;
y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot x2 vaddr) (addrFromPPtr (lookup_pd_slot x2 vaddr)));
flushTable x2 asid vaddr
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c pde_Ptr (x2 + (vaddr >> 20) * 4)} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr (x2 + (vaddr >> 20) * 4)) ret__struct_pde_C)));;
(\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) (pde_Ptr (x2 + (vaddr >> 20) * 4)));;
(CALL cleanByVA_PoU_'proc(ptr_val (pde_Ptr (x2 + (vaddr >> 20) * 4)),\<acute>ret__unsigned_long);;
CALL flushTable_'proc(pde_Ptr x2,asid,vaddr,pte_Ptr ptPtr))))
 2. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> (?A1551 pt vaddra asida rv x and page_directory_at' x) s)\<rbrace>
 3. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> {s. pdSlot_'_update (\<lambda>_. pde_Ptr (x + (vaddra >> 20) * 4)) s \<in> {s. \<forall>v. pde_pde_invalid_lift v = \<lparr>stored_hw_asid_CL = stored_hw_asid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 8, stored_asid_valid_CL = stored_asid_valid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 1\<rparr> \<and> pde_get_tag v = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s\<lparr>ret__struct_pde_C_' := v\<rparr> \<in> ?G'1715 pt vaddra asida rv (ret__ptr_to_struct_pde_C_' t) x v}} \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (6 subgoals):
 1. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1841 (pte_Ptr ptPtr) vaddr asid (Some x2) x2) (?G'1715 (pte_Ptr ptPtr) vaddr asid (Some x2) (pde_Ptr x2) x2 ret__struct_pde_C) [] (storePDE (lookup_pd_slot x2 vaddr) ARM_H.InvalidPDE) (Guard C_Guard {s. s \<Turnstile>\<^sub>c pde_Ptr (x2 + (vaddr >> 20) * 4)} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr (x2 + (vaddr >> 20) * 4)) ret__struct_pde_C))))
 2. \<And>pt vaddra asida rv x2 ret__struct_pde_C y rv'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1835 pt vaddra asida rv x2 ret__struct_pde_C y) (?Q'1835 pt vaddra asida rv x2 ret__struct_pde_C y rv') [SKIP] (do y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot x2 vaddr) (addrFromPPtr (lookup_pd_slot x2 vaddr)));
flushTable x2 asid vaddr
od) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) (pde_Ptr (x2 + (vaddr >> 20) * 4)));;
(CALL cleanByVA_PoU_'proc(ptr_val (pde_Ptr (x2 + (vaddr >> 20) * 4)),\<acute>ret__unsigned_long);;
CALL flushTable_'proc(pde_Ptr x2,asid,vaddr,pte_Ptr ptPtr)))
 3. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R1839 (pte_Ptr ptPtr) vaddr asid (Some x2) x2\<rbrace> storePDE (lookup_pd_slot x2 vaddr) ARM_H.InvalidPDE \<lbrace>?Q1835 pt vaddra asida rv x2 ret__struct_pde_C\<rbrace>
 4. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1835 pt vaddra asida rv x2 ret__struct_pde_C)
 5. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> (?P1841 pt vaddra asida rv x and ?R1839 pt vaddra asida rv x and page_directory_at' x) s)\<rbrace>
 6. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> {s. pdSlot_'_update (\<lambda>_. pde_Ptr (x + (vaddra >> 20) * 4)) s \<in> {s. \<forall>v. pde_pde_invalid_lift v = \<lparr>stored_hw_asid_CL = stored_hw_asid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 8, stored_asid_valid_CL = stored_asid_valid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 1\<rparr> \<and> pde_get_tag v = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s\<lparr>ret__struct_pde_C_' := v\<rparr> \<in> ?G'1715 pt vaddra asida rv (ret__ptr_to_struct_pde_C_' t) x v}} \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (6 subgoals):
 1. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> cpde_relation ARM_H.InvalidPDE ret__struct_pde_C
 2. \<And>pt vaddra asida rv x2 ret__struct_pde_C y rv'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1835 pt vaddra asida rv x2 ret__struct_pde_C y) (?Q'1835 pt vaddra asida rv x2 ret__struct_pde_C y rv') [SKIP] (do y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot x2 vaddr) (addrFromPPtr (lookup_pd_slot x2 vaddr)));
flushTable x2 asid vaddr
od) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) (pde_Ptr (x2 + (vaddr >> 20) * 4)));;
(CALL cleanByVA_PoU_'proc(ptr_val (pde_Ptr (x2 + (vaddr >> 20) * 4)),\<acute>ret__unsigned_long);;
CALL flushTable_'proc(pde_Ptr x2,asid,vaddr,pte_Ptr ptPtr)))
 3. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R1839 (pte_Ptr ptPtr) vaddr asid (Some x2) x2\<rbrace> storePDE (lookup_pd_slot x2 vaddr) ARM_H.InvalidPDE \<lbrace>?Q1835 pt vaddra asida rv x2 ret__struct_pde_C\<rbrace>
 4. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1835 pt vaddra asida rv x2 ret__struct_pde_C)
 5. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>a. valid_pde_mapping_offset' (lookup_pd_slot x vaddra && mask pdBits)) and ?R1839 pt vaddra asida rv x and page_directory_at' x) s)\<rbrace>
 6. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> {s. pdSlot_'_update (\<lambda>_. pde_Ptr (x + (vaddra >> 20) * 4)) s \<in> {s. \<forall>v. pde_pde_invalid_lift v = \<lparr>stored_hw_asid_CL = stored_hw_asid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 8, stored_asid_valid_CL = stored_asid_valid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 1\<rparr> \<and> pde_get_tag v = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s\<lparr>ret__struct_pde_C_' := v\<rparr> \<in> \<lbrace>x + (vaddra >> 20) * 4 = lookup_pd_slot x vaddra\<rbrace>}} \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (5 subgoals):
 1. \<And>pt vaddra asida rv x2 ret__struct_pde_C y rv'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1835 pt vaddra asida rv x2 ret__struct_pde_C y) (?Q'1835 pt vaddra asida rv x2 ret__struct_pde_C y rv') [SKIP] (do y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot x2 vaddr) (addrFromPPtr (lookup_pd_slot x2 vaddr)));
flushTable x2 asid vaddr
od) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) (pde_Ptr (x2 + (vaddr >> 20) * 4)));;
(CALL cleanByVA_PoU_'proc(ptr_val (pde_Ptr (x2 + (vaddr >> 20) * 4)),\<acute>ret__unsigned_long);;
CALL flushTable_'proc(pde_Ptr x2,asid,vaddr,pte_Ptr ptPtr)))
 2. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R1839 (pte_Ptr ptPtr) vaddr asid (Some x2) x2\<rbrace> storePDE (lookup_pd_slot x2 vaddr) ARM_H.InvalidPDE \<lbrace>?Q1835 pt vaddra asida rv x2 ret__struct_pde_C\<rbrace>
 3. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1835 pt vaddra asida rv x2 ret__struct_pde_C)
 4. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>a. valid_pde_mapping_offset' (lookup_pd_slot x vaddra && mask pdBits)) and ?R1839 pt vaddra asida rv x and page_directory_at' x) s)\<rbrace>
 5. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> {s. pdSlot_'_update (\<lambda>_. pde_Ptr (x + (vaddra >> 20) * 4)) s \<in> {s. \<forall>v. pde_pde_invalid_lift v = \<lparr>stored_hw_asid_CL = stored_hw_asid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 8, stored_asid_valid_CL = stored_asid_valid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 1\<rparr> \<and> pde_get_tag v = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s\<lparr>ret__struct_pde_C_' := v\<rparr> \<in> \<lbrace>x + (vaddra >> 20) * 4 = lookup_pd_slot x vaddra\<rbrace>}} \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (5 subgoals):
 1. \<And>pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; dc y rv'; ret__unsigned_long = addrFromPPtr (x2 + (vaddr >> 20) * 4)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1835 pt vaddra asida rv x2 ret__struct_pde_C y) (?G'1852 pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long) [SKIP] (do y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot x2 vaddr) (addrFromPPtr (lookup_pd_slot x2 vaddr)));
flushTable x2 asid vaddr
od) (CALL cleanByVA_PoU_'proc(ptr_val (pde_Ptr (x2 + (vaddr >> 20) * 4)),ret__unsigned_long);;
CALL flushTable_'proc(pde_Ptr x2,asid,vaddr,pte_Ptr ptPtr))
 2. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R1839 (pte_Ptr ptPtr) vaddr asid (Some x2) x2\<rbrace> storePDE (lookup_pd_slot x2 vaddr) ARM_H.InvalidPDE \<lbrace>?Q1835 pt vaddra asida rv x2 ret__struct_pde_C\<rbrace>
 3. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. \<forall>v. v = addrFromPPtr (ptr_val (pptr_' (pptr_'_update (\<lambda>_. PTR_COERCE(pde_C \<rightarrow> unit) (pde_Ptr (x2 + (vaddr >> 20) * 4))) s))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := v\<rparr> \<in> ?G'1852 pt vaddra asida rv x2 ret__struct_pde_C y rv' v})
 4. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>a. valid_pde_mapping_offset' (lookup_pd_slot x vaddra && mask pdBits)) and ?R1839 pt vaddra asida rv x and page_directory_at' x) s)\<rbrace>
 5. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> {s. pdSlot_'_update (\<lambda>_. pde_Ptr (x + (vaddra >> 20) * 4)) s \<in> {s. \<forall>v. pde_pde_invalid_lift v = \<lparr>stored_hw_asid_CL = stored_hw_asid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 8, stored_asid_valid_CL = stored_asid_valid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 1\<rparr> \<and> pde_get_tag v = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s\<lparr>ret__struct_pde_C_' := v\<rparr> \<in> \<lbrace>x + (vaddra >> 20) * 4 = lookup_pd_slot x vaddra\<rbrace>}} \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (7 subgoals):
 1. \<And>pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long rva xfdca. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; dc y rv'; ret__unsigned_long = addrFromPPtr (x2 + (vaddr >> 20) * 4); dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1924 pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long rva) (?Q'1924 pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long rva xfdca) [SKIP] (flushTable x2 asid vaddr) (CALL flushTable_'proc(pde_Ptr x2,asid,vaddr,pte_Ptr ptPtr))
 2. \<And>pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; dc y rv'; ret__unsigned_long = addrFromPPtr (x2 + (vaddr >> 20) * 4)\<rbrakk> \<Longrightarrow> \<lbrace>?R1926 pt vaddra asida rv x2 ret__struct_pde_C y\<rbrace> doMachineOp (cleanByVA_PoU (lookup_pd_slot x2 vaddr) (addrFromPPtr (lookup_pd_slot x2 vaddr))) \<lbrace>?Q1924 pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long\<rbrace>
 3. \<And>pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; dc y rv'; ret__unsigned_long = addrFromPPtr (x2 + (vaddr >> 20) * 4)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1924 pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long) CALL cleanByVA_PoU_'proc(ptr_val (pde_Ptr (x2 + (vaddr >> 20) * 4)),ret__unsigned_long) {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> ?Q'1924 pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long rva (xfdc s)}
 4. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R1839 (pte_Ptr ptPtr) vaddr asid (Some x2) x2\<rbrace> storePDE (lookup_pd_slot x2 vaddr) ARM_H.InvalidPDE \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R1926 pt vaddra asida rv x2 ret__struct_pde_C y\<rbrace>
 5. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. \<forall>v. v = addrFromPPtr (ptr_val (pptr_' (pptr_'_update (\<lambda>_. PTR_COERCE(pde_C \<rightarrow> unit) (pde_Ptr (x2 + (vaddr >> 20) * 4))) s))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := v\<rparr> \<in> {s. paddr_'_update (\<lambda>_. v) (vaddr_'_update (\<lambda>_. ptr_val (pde_Ptr (x2 + (vaddr >> 20) * 4))) s) \<in> \<lbrace>\<acute>vaddr = lookup_pd_slot x2 vaddr\<rbrace> \<inter> \<lbrace>\<acute>paddr = addrFromPPtr (lookup_pd_slot x2 vaddr)\<rbrace>} \<inter> ?R'1924 pt vaddra asida rv x2 ret__struct_pde_C y rv' v})
 6. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>a. valid_pde_mapping_offset' (lookup_pd_slot x vaddra && mask pdBits)) and ?R1839 pt vaddra asida rv x and page_directory_at' x) s)\<rbrace>
 7. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> {s. pdSlot_'_update (\<lambda>_. pde_Ptr (x + (vaddra >> 20) * 4)) s \<in> {s. \<forall>v. pde_pde_invalid_lift v = \<lparr>stored_hw_asid_CL = stored_hw_asid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 8, stored_asid_valid_CL = stored_asid_valid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 1\<rparr> \<and> pde_get_tag v = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s\<lparr>ret__struct_pde_C_' := v\<rparr> \<in> \<lbrace>x + (vaddra >> 20) * 4 = lookup_pd_slot x vaddra\<rbrace>}} \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (6 subgoals):
 1. \<And>pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; dc y rv'; ret__unsigned_long = addrFromPPtr (x2 + (vaddr >> 20) * 4)\<rbrakk> \<Longrightarrow> \<lbrace>?R1926 pt vaddra asida rv x2 ret__struct_pde_C y\<rbrace> doMachineOp (cleanByVA_PoU (lookup_pd_slot x2 vaddr) (addrFromPPtr (lookup_pd_slot x2 vaddr))) \<lbrace>\<lambda>rva. invs' and cur_tcb' and (\<lambda>_. asid \<le> mask local.asid_bits)\<rbrace>
 2. \<And>pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; dc y rv'; ret__unsigned_long = addrFromPPtr (x2 + (vaddr >> 20) * 4)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1924 pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long) CALL cleanByVA_PoU_'proc(ptr_val (pde_Ptr (x2 + (vaddr >> 20) * 4)),ret__unsigned_long) {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {sa. pt_'_update (\<lambda>_. pte_Ptr ptPtr) (vptr_'_update (\<lambda>_. vaddr) (asid_'_update (\<lambda>_. asid) (pd_'_update (\<lambda>_. pde_Ptr x2) sa))) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr x2\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vptr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr (?pt1960 pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long rva (xfdc s))\<rbrace>}}
 3. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R1839 (pte_Ptr ptPtr) vaddr asid (Some x2) x2\<rbrace> storePDE (lookup_pd_slot x2 vaddr) ARM_H.InvalidPDE \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R1926 pt vaddra asida rv x2 ret__struct_pde_C y\<rbrace>
 4. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. \<forall>v. v = addrFromPPtr (ptr_val (pptr_' (pptr_'_update (\<lambda>_. PTR_COERCE(pde_C \<rightarrow> unit) (pde_Ptr (x2 + (vaddr >> 20) * 4))) s))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := v\<rparr> \<in> {s. paddr_'_update (\<lambda>_. v) (vaddr_'_update (\<lambda>_. ptr_val (pde_Ptr (x2 + (vaddr >> 20) * 4))) s) \<in> \<lbrace>\<acute>vaddr = lookup_pd_slot x2 vaddr\<rbrace> \<inter> \<lbrace>\<acute>paddr = addrFromPPtr (lookup_pd_slot x2 vaddr)\<rbrace>} \<inter> ?R'1924 pt vaddra asida rv x2 ret__struct_pde_C y rv' v})
 5. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>a. valid_pde_mapping_offset' (lookup_pd_slot x vaddra && mask pdBits)) and ?R1839 pt vaddra asida rv x and page_directory_at' x) s)\<rbrace>
 6. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> {s. pdSlot_'_update (\<lambda>_. pde_Ptr (x + (vaddra >> 20) * 4)) s \<in> {s. \<forall>v. pde_pde_invalid_lift v = \<lparr>stored_hw_asid_CL = stored_hw_asid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 8, stored_asid_valid_CL = stored_asid_valid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 1\<rparr> \<and> pde_get_tag v = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s\<lparr>ret__struct_pde_C_' := v\<rparr> \<in> \<lbrace>x + (vaddra >> 20) * 4 = lookup_pd_slot x vaddra\<rbrace>}} \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (5 subgoals):
 1. \<And>pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; dc y rv'; ret__unsigned_long = addrFromPPtr (x2 + (vaddr >> 20) * 4)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1924 pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long) CALL cleanByVA_PoU_'proc(ptr_val (pde_Ptr (x2 + (vaddr >> 20) * 4)),ret__unsigned_long) {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {sa. pt_'_update (\<lambda>_. pte_Ptr ptPtr) (vptr_'_update (\<lambda>_. vaddr) (asid_'_update (\<lambda>_. asid) (pd_'_update (\<lambda>_. pde_Ptr x2) sa))) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr x2\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vptr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr (?pt1960 pt vaddra asida rv x2 ret__struct_pde_C y rv' ret__unsigned_long rva (xfdc s))\<rbrace>}}
 2. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R1839 (pte_Ptr ptPtr) vaddr asid (Some x2) x2\<rbrace> storePDE (lookup_pd_slot x2 vaddr) ARM_H.InvalidPDE \<lbrace>\<lambda>y. (\<lambda>_. True) and (\<lambda>s. invs' s \<and> cur_tcb' s \<and> asid \<le> mask local.asid_bits)\<rbrace>
 3. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. \<forall>v. v = addrFromPPtr (ptr_val (pptr_' (pptr_'_update (\<lambda>_. PTR_COERCE(pde_C \<rightarrow> unit) (pde_Ptr (x2 + (vaddr >> 20) * 4))) s))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := v\<rparr> \<in> {s. paddr_'_update (\<lambda>_. v) (vaddr_'_update (\<lambda>_. ptr_val (pde_Ptr (x2 + (vaddr >> 20) * 4))) s) \<in> \<lbrace>\<acute>vaddr = lookup_pd_slot x2 vaddr\<rbrace> \<inter> \<lbrace>\<acute>paddr = addrFromPPtr (lookup_pd_slot x2 vaddr)\<rbrace>} \<inter> ?R'1924 pt vaddra asida rv x2 ret__struct_pde_C y rv' v})
 4. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>a. valid_pde_mapping_offset' (lookup_pd_slot x vaddra && mask pdBits)) and ?R1839 pt vaddra asida rv x and page_directory_at' x) s)\<rbrace>
 5. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> {s. pdSlot_'_update (\<lambda>_. pde_Ptr (x + (vaddra >> 20) * 4)) s \<in> {s. \<forall>v. pde_pde_invalid_lift v = \<lparr>stored_hw_asid_CL = stored_hw_asid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 8, stored_asid_valid_CL = stored_asid_valid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 1\<rparr> \<and> pde_get_tag v = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s\<lparr>ret__struct_pde_C_' := v\<rparr> \<in> \<lbrace>x + (vaddra >> 20) * 4 = lookup_pd_slot x vaddra\<rbrace>}} \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (4 subgoals):
 1. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R1839 (pte_Ptr ptPtr) vaddr asid (Some x2) x2\<rbrace> storePDE (lookup_pd_slot x2 vaddr) ARM_H.InvalidPDE \<lbrace>\<lambda>y. (\<lambda>_. True) and (\<lambda>s. invs' s \<and> cur_tcb' s \<and> asid \<le> mask local.asid_bits)\<rbrace>
 2. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. \<forall>v. v = addrFromPPtr (ptr_val (pptr_' (pptr_'_update (\<lambda>_. PTR_COERCE(pde_C \<rightarrow> unit) (pde_Ptr (x2 + (vaddr >> 20) * 4))) s))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := v\<rparr> \<in> {s. paddr_'_update (\<lambda>_. v) (vaddr_'_update (\<lambda>_. ptr_val (pde_Ptr (x2 + (vaddr >> 20) * 4))) s) \<in> \<lbrace>\<acute>vaddr = lookup_pd_slot x2 vaddr\<rbrace> \<inter> \<lbrace>\<acute>paddr = addrFromPPtr (lookup_pd_slot x2 vaddr)\<rbrace>} \<inter> {s. \<forall>t rva. dc rva (xfdc (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<longrightarrow> pte_Ptr ptPtr = pte_Ptr (?pt1960 pt vaddra asida rv x2 ret__struct_pde_C y rv' v rva (xfdc (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)))}})
 3. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>a. valid_pde_mapping_offset' (lookup_pd_slot x vaddra && mask pdBits)) and ?R1839 pt vaddra asida rv x and page_directory_at' x) s)\<rbrace>
 4. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> {s. pdSlot_'_update (\<lambda>_. pde_Ptr (x + (vaddra >> 20) * 4)) s \<in> {s. \<forall>v. pde_pde_invalid_lift v = \<lparr>stored_hw_asid_CL = stored_hw_asid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 8, stored_asid_valid_CL = stored_asid_valid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 1\<rparr> \<and> pde_get_tag v = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s\<lparr>ret__struct_pde_C_' := v\<rparr> \<in> \<lbrace>x + (vaddra >> 20) * 4 = lookup_pd_slot x vaddra\<rbrace>}} \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (3 subgoals):
 1. \<And>pt vaddra asida rv x2 ret__struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; x2 \<noteq> 0; rv = Some x2; pde_pde_invalid_lift ret__struct_pde_C = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = 0\<rparr> \<and> pde_get_tag ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. \<forall>v. v = addrFromPPtr (ptr_val (pptr_' (pptr_'_update (\<lambda>_. PTR_COERCE(pde_C \<rightarrow> unit) (pde_Ptr (x2 + (vaddr >> 20) * 4))) s))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := v\<rparr> \<in> {s. paddr_'_update (\<lambda>_. v) (vaddr_'_update (\<lambda>_. ptr_val (pde_Ptr (x2 + (vaddr >> 20) * 4))) s) \<in> \<lbrace>\<acute>vaddr = lookup_pd_slot x2 vaddr\<rbrace> \<inter> \<lbrace>\<acute>paddr = addrFromPPtr (lookup_pd_slot x2 vaddr)\<rbrace>} \<inter> {s. \<forall>t rva. dc rva (xfdc (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<longrightarrow> pte_Ptr ptPtr = pte_Ptr (?pt1960 pt vaddra asida rv x2 ret__struct_pde_C y rv' v rva (xfdc (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)))}})
 2. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>a. valid_pde_mapping_offset' (lookup_pd_slot x vaddra && mask pdBits)) and (\<lambda>a. True \<and> (invs' and valid_pde' ARM_H.InvalidPDE and (\<lambda>s. valid_pde_mapping' (lookup_pd_slot x vaddra && mask pdBits) ARM_H.InvalidPDE)) a \<and> cur_tcb' a \<and> asida \<le> mask local.asid_bits) and page_directory_at' x) s)\<rbrace>
 3. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> {s. pdSlot_'_update (\<lambda>_. pde_Ptr (x + (vaddra >> 20) * 4)) s \<in> {s. \<forall>v. pde_pde_invalid_lift v = \<lparr>stored_hw_asid_CL = stored_hw_asid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 8, stored_asid_valid_CL = stored_asid_valid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 1\<rparr> \<and> pde_get_tag v = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s\<lparr>ret__struct_pde_C_' := v\<rparr> \<in> \<lbrace>x + (vaddra >> 20) * 4 = lookup_pd_slot x vaddra\<rbrace>}} \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (2 subgoals):
 1. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>a. valid_pde_mapping_offset' (lookup_pd_slot x vaddra && mask pdBits)) and (\<lambda>a. True \<and> (invs' and valid_pde' ARM_H.InvalidPDE and (\<lambda>s. valid_pde_mapping' (lookup_pd_slot x vaddra && mask pdBits) ARM_H.InvalidPDE)) a \<and> cur_tcb' a \<and> asida \<le> mask local.asid_bits) and page_directory_at' x) s)\<rbrace>
 2. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> {s. pdSlot_'_update (\<lambda>_. pde_Ptr (x + (vaddra >> 20) * 4)) s \<in> {s. \<forall>v. pde_pde_invalid_lift v = \<lparr>stored_hw_asid_CL = stored_hw_asid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 8, stored_asid_valid_CL = stored_asid_valid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 1\<rparr> \<and> pde_get_tag v = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s\<lparr>ret__struct_pde_C_' := v\<rparr> \<in> \<lbrace>x + (vaddra >> 20) * 4 = lookup_pd_slot x vaddra\<rbrace>}} \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (3 subgoals):
 1. \<And>pt vaddra asida rv s. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (case rv of None \<Rightarrow> True | Some pd \<Rightarrow> page_directory_at' pd s) \<and> invs' s\<rbrakk> \<Longrightarrow> (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>a. valid_pde_mapping_offset' (lookup_pd_slot x vaddra && mask pdBits)) and (\<lambda>a. True \<and> (invs' and valid_pde' ARM_H.InvalidPDE and (\<lambda>s. valid_pde_mapping' (lookup_pd_slot x vaddra && mask pdBits) ARM_H.InvalidPDE)) a \<and> cur_tcb' a \<and> asida \<le> mask local.asid_bits) and page_directory_at' x) s)
 2. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (case rv of None \<Rightarrow> True | Some pd \<Rightarrow> page_directory_at' pd s) \<and> invs' s\<rbrace>
 3. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> {s. pdSlot_'_update (\<lambda>_. pde_Ptr (x + (vaddra >> 20) * 4)) s \<in> {s. \<forall>v. pde_pde_invalid_lift v = \<lparr>stored_hw_asid_CL = stored_hw_asid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 8, stored_asid_valid_CL = stored_asid_valid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 1\<rparr> \<and> pde_get_tag v = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s\<lparr>ret__struct_pde_C_' := v\<rparr> \<in> \<lbrace>x + (vaddra >> 20) * 4 = lookup_pd_slot x vaddra\<rbrace>}} \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (2 subgoals):
 1. \<And>pt vaddra asida. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R1119 pt vaddra asida\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. (case rv of None \<Rightarrow> True | Some pd \<Rightarrow> page_directory_at' pd s) \<and> invs' s\<rbrace>
 2. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and ?R1119 pt vaddra asida) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> {s. pdSlot_'_update (\<lambda>_. pde_Ptr (x + (vaddra >> 20) * 4)) s \<in> {s. \<forall>v. pde_pde_invalid_lift v = \<lparr>stored_hw_asid_CL = stored_hw_asid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 8, stored_asid_valid_CL = stored_asid_valid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 1\<rparr> \<and> pde_get_tag v = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s\<lparr>ret__struct_pde_C_' := v\<rparr> \<in> \<lbrace>x + (vaddra >> 20) * 4 = lookup_pd_slot x vaddra\<rbrace>}} \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (1 subgoal):
 1. \<And>pt vaddra asida s s'. \<lbrakk>asid \<le> mask local.asid_bits \<and> vaddr < pptrBase; pt = pte_Ptr ptPtr; vaddra = vaddr; asida = asid; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and K (asid \<le> mask local.asid_bits) and (\<lambda>s. True \<and> invs' s)) s \<and> s' \<in> {s. pt_'_update (\<lambda>_. pt) (vaddr_'_update (\<lambda>_. vaddra) (asid_'_update (\<lambda>_. asida) s)) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vaddr = vaddr\<rbrace> \<inter> \<lbrace>\<acute>pt = pte_Ptr ptPtr\<rbrace>} \<inter> {s'. \<forall>t rv. ret__ptr_to_struct_pde_C_' t = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> pd_'_update (\<lambda>_. ret__ptr_to_struct_pde_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. pdIndex_'_update (\<lambda>_. vaddra >> 20) s \<in> {s. pdSlot_'_update (\<lambda>_. pde_Ptr (x + (vaddra >> 20) * 4)) s \<in> {s. \<forall>v. pde_pde_invalid_lift v = \<lparr>stored_hw_asid_CL = stored_hw_asid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 8, stored_asid_valid_CL = stored_asid_valid_' (stored_asid_valid_'_update (\<lambda>_. 0) (stored_hw_asid_'_update (\<lambda>_. 0) s)) && mask 1\<rparr> \<and> pde_get_tag v = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s\<lparr>ret__struct_pde_C_' := v\<rparr> \<in> \<lbrace>x + (vaddra >> 20) * 4 = lookup_pd_slot x vaddra\<rbrace>}} \<inter> \<lbrace>unat (vaddra >> 20) \<le> 2 ^ (pdBits - 2) \<and> (vaddra >> 20 \<noteq> 0 \<longrightarrow> unat (vaddra >> 20) \<noteq> 0)\<rbrace>}}}} proof (prove)
goal (1 subgoal):
 1. \<And>s s' t x. \<lbrakk>(s, s') \<in> rf_sr; invs' s; asid \<le> mask local.asid_bits; vaddr < pptrBase; ret__ptr_to_struct_pde_C_' t = option_to_ptr (Some x); unat (vaddr >> 20) \<le> 2 ^ (pdeBits + 10) \<longrightarrow> vaddr >> 20 \<noteq> 0 \<and> unat (vaddr >> 20) = 0\<rbrakk> \<Longrightarrow> x = 0 proof (prove)
goal:
No subgoals!