theory ArchADT_AI

lemma get_pd_of_thread_vs_lookup:
  "get_pd_of_thread (kheap s) (arch_state s) tcb_ref =
   (case kheap s tcb_ref of
      Some (TCB tcb) \<Rightarrow>
        (case tcb_vtable tcb of
           ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow>
             if (the (vs_cap_ref (tcb_vtable tcb)) \<rhd> pd_ref) s then pd_ref
             else arm_global_pd (arch_state s)
         | _ \<Rightarrow> arm_global_pd (arch_state s))
    | _ \<Rightarrow> arm_global_pd (arch_state s))" apply (clarsimp simp: get_pd_of_thread_def split: option.splits) apply (case_tac "the (kheap s tcb_ref)", simp_all, clarsimp) apply (rename_tac tcb) apply (case_tac "\<not> is_pd_cap (tcb_vtable tcb)") apply (clarsimp simp: is_pd_cap_def split: cap.split arch_cap.split) apply (clarsimp simp: is_pd_cap_def vs_cap_ref_def) apply (case_tac asid, simp_all, clarsimp) apply (intro conjI impI) apply (erule vs_lookupE) apply (clarsimp simp: vs_asid_refs_def split_def image_def graph_of_def) apply (erule rtranclE, simp) apply (clarsimp dest!: vs_lookup1D) apply (clarsimp simp: vs_refs_def vs_refs_arch_def graph_of_def
                  split: kernel_object.split_asm arch_kernel_obj.split_asm) apply (erule rtranclE) apply (clarsimp simp: up_ucast_inj_eq obj_at_def vs_refs_def vs_refs_arch_def graph_of_def
                          image_def
                   split: arch_kernel_obj.split_asm) apply (clarsimp dest!: vs_lookup1D) apply (clarsimp simp: vs_refs_def vs_refs_arch_def graph_of_def
                   split: kernel_object.split_asm arch_kernel_obj.split_asm) apply (erule swap) apply (clarsimp split: kernel_object.split_asm arch_kernel_obj.split_asm
                         option.split_asm if_split_asm) apply (rule vs_lookupI) apply (fastforce simp: vs_asid_refs_def image_def graph_of_def) apply (rule rtrancl_into_rtrancl) apply (rule rtrancl_refl) apply (rule vs_lookup1I, (simp add: obj_at_def vs_refs_def vs_refs_arch_def)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_pd_of_thread (kheap s) (arch_state s) tcb_ref = (case kheap s tcb_ref of None \<Rightarrow> arm_global_pd (arch_state s) | Some (TCB tcb) \<Rightarrow> case tcb_vtable tcb of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> if (the (vs_cap_ref (tcb_vtable tcb)) \<rhd> pd_ref) s then pd_ref else arm_global_pd (arch_state s) | ArchObjectCap _ \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>x2. kheap s tcb_ref = Some x2 \<Longrightarrow> (case x2 of TCB tcb \<Rightarrow> case tcb_vtable tcb of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> case asid_table s (asid_high_bits_of asid) of None \<Rightarrow> arm_global_pd (arch_state s) | Some p \<Rightarrow> case kheap s p of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd_ref) \<in> vs_refs_arch ako then pd_ref else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap _ \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s)) = (case x2 of TCB tcb \<Rightarrow> case tcb_vtable tcb of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> if (the (vs_cap_ref (tcb_vtable tcb)) \<rhd> pd_ref) s then pd_ref else arm_global_pd (arch_state s) | ArchObjectCap _ \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>x2a. kheap s tcb_ref = Some (TCB x2a) \<Longrightarrow> (case tcb_vtable x2a of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> case asid_table s (asid_high_bits_of asid) of None \<Rightarrow> arm_global_pd (arch_state s) | Some p \<Rightarrow> case kheap s p of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd_ref) \<in> vs_refs_arch ako then pd_ref else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap _ \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s)) = (case tcb_vtable x2a of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> if (the (vs_cap_ref (tcb_vtable x2a)) \<rhd> pd_ref) s then pd_ref else arm_global_pd (arch_state s) | ArchObjectCap _ \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. kheap s tcb_ref = Some (TCB tcb) \<Longrightarrow> (case tcb_vtable tcb of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> case asid_table s (asid_high_bits_of asid) of None \<Rightarrow> arm_global_pd (arch_state s) | Some p \<Rightarrow> case kheap s p of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd_ref) \<in> vs_refs_arch ako then pd_ref else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap _ \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s)) = (case tcb_vtable tcb of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> if (the (vs_cap_ref (tcb_vtable tcb)) \<rhd> pd_ref) s then pd_ref else arm_global_pd (arch_state s) | ArchObjectCap _ \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); \<not> is_pd_cap (tcb_vtable tcb)\<rbrakk> \<Longrightarrow> (case tcb_vtable tcb of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> case asid_table s (asid_high_bits_of asid) of None \<Rightarrow> arm_global_pd (arch_state s) | Some p \<Rightarrow> case kheap s p of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd_ref) \<in> vs_refs_arch ako then pd_ref else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap _ \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s)) = (case tcb_vtable tcb of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> if (the (vs_cap_ref (tcb_vtable tcb)) \<rhd> pd_ref) s then pd_ref else arm_global_pd (arch_state s) | ArchObjectCap _ \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s))
 2. \<And>tcb. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); \<not> \<not> is_pd_cap (tcb_vtable tcb)\<rbrakk> \<Longrightarrow> (case tcb_vtable tcb of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> case asid_table s (asid_high_bits_of asid) of None \<Rightarrow> arm_global_pd (arch_state s) | Some p \<Rightarrow> case kheap s p of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd_ref) \<in> vs_refs_arch ako then pd_ref else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap _ \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s)) = (case tcb_vtable tcb of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> if (the (vs_cap_ref (tcb_vtable tcb)) \<rhd> pd_ref) s then pd_ref else arm_global_pd (arch_state s) | ArchObjectCap _ \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); \<not> \<not> is_pd_cap (tcb_vtable tcb)\<rbrakk> \<Longrightarrow> (case tcb_vtable tcb of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> case asid_table s (asid_high_bits_of asid) of None \<Rightarrow> arm_global_pd (arch_state s) | Some p \<Rightarrow> case kheap s p of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd_ref) \<in> vs_refs_arch ako then pd_ref else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap _ \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s)) = (case tcb_vtable tcb of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd (arch_state s) | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> if (the (vs_cap_ref (tcb_vtable tcb)) \<rhd> pd_ref) s then pd_ref else arm_global_pd (arch_state s) | ArchObjectCap _ \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb p asid. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p asid)\<rbrakk> \<Longrightarrow> ((the (case asid of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<rhd> p) s \<longrightarrow> (case asid of None \<Rightarrow> arm_global_pd (arch_state s) | Some asid \<Rightarrow> case asid_table s (asid_high_bits_of asid) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = (case asid of None \<Rightarrow> arm_global_pd (arch_state s) | Some asid \<Rightarrow> p)) \<and> ((the (case asid of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]), p) \<notin> vs_lookup s \<longrightarrow> (case asid of None \<Rightarrow> arm_global_pd (arch_state s) | Some asid \<Rightarrow> case asid_table s (asid_high_bits_of asid) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = (case asid of None \<Rightarrow> arm_global_pd (arch_state s) | _ \<Rightarrow> arm_global_pd (arch_state s))) proof (prove)
goal (1 subgoal):
 1. \<And>tcb p a. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a))\<rbrakk> \<Longrightarrow> (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> p) s \<longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = p) \<and> (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<notin> vs_lookup s \<longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = arm_global_pd (arch_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>tcb p a. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> p) s\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = p
 2. \<And>tcb p a. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = arm_global_pd (arch_state s) proof (prove)
goal (2 subgoals):
 1. \<And>tcb p a ref' p'. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); (ref', p') \<in> vs_asid_refs (asid_table s); ((ref', p'), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = p
 2. \<And>tcb p a. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = arm_global_pd (arch_state s) proof (prove)
goal (2 subgoals):
 1. \<And>tcb p a p' aa. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], p'), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<in> (vs_lookup1 s)\<^sup>*; asid_table s aa = Some p'\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = p
 2. \<And>tcb p a. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = arm_global_pd (arch_state s) proof (prove)
goal (2 subgoals):
 1. \<And>tcb p a p' aa y. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); asid_table s aa = Some p'; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], p'), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = p
 2. \<And>tcb p a. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = arm_global_pd (arch_state s) proof (prove)
goal (2 subgoals):
 1. \<And>tcb a p' aa pa p'a ko. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p'a (Some a)); asid_table s aa = Some p'; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], p'), [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], pa) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some p \<Rightarrow> case kheap s p of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs_arch ako then p'a else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = p'a
 2. \<And>tcb p a. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = arm_global_pd (arch_state s) proof (prove)
goal (2 subgoals):
 1. \<And>tcb a p' aa pa x1 ab b. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap b (Some a)); asid_table s aa = Some p'; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], p'), [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], pa) \<in> (vs_lookup1 s)\<^sup>*; ako_at (ASIDPool x1) pa s; x1 ab = Some b; a && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some p \<Rightarrow> case kheap s p of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs_arch ako then b else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = b
 2. \<And>tcb p a. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = arm_global_pd (arch_state s) proof (prove)
goal (3 subgoals):
 1. \<And>tcb a p' aa pa x1 ab b. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap b (Some a)); asid_table s aa = Some p'; ako_at (ASIDPool x1) pa s; x1 ab = Some b; a && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], p') = ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], pa)\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some p \<Rightarrow> case kheap s p of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs_arch ako then b else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = b
 2. \<And>tcb a p' aa pa x1 ab b y. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap b (Some a)); asid_table s aa = Some p'; ako_at (ASIDPool x1) pa s; x1 ab = Some b; a && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], p'), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], pa) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some p \<Rightarrow> case kheap s p of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs_arch ako then b else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = b
 3. \<And>tcb p a. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = arm_global_pd (arch_state s) proof (prove)
goal (2 subgoals):
 1. \<And>tcb a p' aa pa x1 ab b y. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap b (Some a)); asid_table s aa = Some p'; ako_at (ASIDPool x1) pa s; x1 ab = Some b; a && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], p'), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], pa) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some p \<Rightarrow> case kheap s p of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs_arch ako then b else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = b
 2. \<And>tcb p a. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = arm_global_pd (arch_state s) proof (prove)
goal (2 subgoals):
 1. \<And>tcb a p' aa x1 ab b p p'a ko. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap b (Some a)); asid_table s aa = Some p'; ako_at (ASIDPool x1) p'a s; x1 ab = Some b; a && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], p'), [], p) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko p s; (VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None, p'a) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some p \<Rightarrow> case kheap s p of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs_arch ako then b else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = b
 2. \<And>tcb p a. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<And>tcb p a. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) = arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<And>tcb p a. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); (case asid_table s (asid_high_bits_of a) of None \<Rightarrow> arm_global_pd (arch_state s) | Some pa \<Rightarrow> case kheap s pa of None \<Rightarrow> arm_global_pd (arch_state s) | Some (ArchObj ako) \<Rightarrow> if (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch ako then p else arm_global_pd (arch_state s) | Some _ \<Rightarrow> arm_global_pd (arch_state s)) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> p) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb p a x2 x5. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); asid_table s (asid_high_bits_of a) = Some x2; kheap s x2 = Some (ArchObj x5); (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch x5; p \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> p) s proof (prove)
goal (2 subgoals):
 1. \<And>tcb p a x2 x5. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); asid_table s (asid_high_bits_of a) = Some x2; kheap s x2 = Some (ArchObj x5); (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch x5; p \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ?ref'297 tcb p a x2 x5 \<in> vs_asid_refs (asid_table s)
 2. \<And>tcb p a x2 x5. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); asid_table s (asid_high_bits_of a) = Some x2; kheap s x2 = Some (ArchObj x5); (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch x5; p \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> (?ref'297 tcb p a x2 x5, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>tcb p a x2 x5. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); asid_table s (asid_high_bits_of a) = Some x2; kheap s x2 = Some (ArchObj x5); (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch x5; p \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], x2), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>tcb p a x2 x5. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); asid_table s (asid_high_bits_of a) = Some x2; kheap s x2 = Some (ArchObj x5); (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch x5; p \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], x2), ?b309 tcb p a x2 x5) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>tcb p a x2 x5. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); asid_table s (asid_high_bits_of a) = Some x2; kheap s x2 = Some (ArchObj x5); (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch x5; p \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> (?b309 tcb p a x2 x5, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<in> vs_lookup1 s proof (prove)
goal (1 subgoal):
 1. \<And>tcb p a x2 x5. \<lbrakk>kheap s tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap (PageDirectoryCap p (Some a)); asid_table s (asid_high_bits_of a) = Some x2; kheap s x2 = Some (ArchObj x5); (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p) \<in> vs_refs_arch x5; p \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], x2), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p) \<in> vs_lookup1 s proof (prove)
goal:
No subgoals!