kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchArch_IF

lemma arm_global_pd_arm_asid_map_update[simp]:
  "arm_global_pd (arch_state s\<lparr>arm_asid_map := x\<rparr>) = arm_global_pd (arch_state s)" by (simp add: globals_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_global_pd (arch_state s\<lparr>arm_asid_map := x\<rparr>) = arm_global_pd (arch_state s)
theory ArchArch_IF

lemma arm_global_pd_arm_hwasid_table_update[simp]:
  "arm_global_pd (arch_state s\<lparr>arm_hwasid_table := x\<rparr>) = arm_global_pd (arch_state s)" by (simp add: globals_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_global_pd (arch_state s\<lparr>arm_hwasid_table := x\<rparr>) = arm_global_pd (arch_state s)
theory ArchArch_IF

lemma not_in_global_refs_vs_lookup2:
  "\<lbrakk> valid_vs_lookup s; valid_global_refs s; valid_arch_state s;
     valid_global_objs s; page_directory_at p s; (\<exists>\<rhd> p) s \<rbrakk>
     \<Longrightarrow> p \<notin> global_refs s" apply (insert not_in_global_refs_vs_lookup[where p=p and s=s]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vs_lookup s; valid_global_refs s; valid_arch_state s; valid_global_objs s; typ_at (AArch APageDirectory) p s; \<exists>ref. (ref \<rhd> p) s\<rbrakk> \<Longrightarrow> p \<notin> global_refs s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vs_lookup s; valid_global_refs s; valid_arch_state s; valid_global_objs s; typ_at (AArch APageDirectory) p s; \<exists>ref. (ref \<rhd> p) s; (\<exists>ref. (ref \<rhd> p) s) \<and> valid_vs_lookup s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_global_objs s \<and> typ_at (AArch APageDirectory) p s \<longrightarrow> p \<notin> global_refs s\<rbrakk> \<Longrightarrow> p \<notin> global_refs s proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma mapM_x_swp_store_pte_globals_equiv:
  "\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
   mapM_x (swp store_pte A) slots
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" apply (rule_tac Q="\<lambda>_. globals_equiv s and valid_arch_state" in hoare_strengthen_post) apply (wp mapM_x_wp' store_pte_globals_equiv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> mapM_x (swp store_pte A) slots \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> mapM_x (swp store_pte A) slots \<lbrace>\<lambda>_. globals_equiv s and valid_arch_state\<rbrace>
 2. \<And>rv sa. (globals_equiv s and valid_arch_state) sa \<Longrightarrow> globals_equiv s sa proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma do_flush_globals_equiv:
  "do_machine_op (do_flush typ start end pstart) \<lbrace>globals_equiv st\<rbrace>" apply (cases "typ") by (wp dmo_cacheRangeOp_lift
      | simp add: do_flush_def cache_machine_op_defs do_flush_defs do_machine_op_bind when_def
                  empty_fail_cond
      | clarsimp | rule conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st\<rbrace> do_machine_op (do_flush typ start end pstart) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. typ = Clean \<Longrightarrow> \<lbrace>globals_equiv st\<rbrace> do_machine_op (do_flush typ start end pstart) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. typ = Invalidate \<Longrightarrow> \<lbrace>globals_equiv st\<rbrace> do_machine_op (do_flush typ start end pstart) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. typ = CleanInvalidate \<Longrightarrow> \<lbrace>globals_equiv st\<rbrace> do_machine_op (do_flush typ start end pstart) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. typ = Unify \<Longrightarrow> \<lbrace>globals_equiv st\<rbrace> do_machine_op (do_flush typ start end pstart) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory ArchArch_IF

lemma perform_page_directory_invocation_globals_equiv:
  "perform_page_directory_invocation pdi \<lbrace>globals_equiv st\<rbrace>" unfolding perform_page_directory_invocation_def apply (cases pdi) apply (wp do_flush_globals_equiv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st\<rbrace> perform_page_directory_invocation pdi \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st\<rbrace> case pdi of PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od | PageDirectoryNothing \<Rightarrow> return () \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. pdi = PageDirectoryFlush x11 x12 x13 x14 x15 x16 \<Longrightarrow> \<lbrace>globals_equiv st\<rbrace> case pdi of PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od | PageDirectoryNothing \<Rightarrow> return () \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. pdi = PageDirectoryNothing \<Longrightarrow> \<lbrace>globals_equiv st\<rbrace> case pdi of PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od | PageDirectoryNothing \<Rightarrow> return () \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma flush_page_globals_equiv[wp]:
  "flush_page page_size pd asid vptr \<lbrace>globals_equiv st\<rbrace>" unfolding flush_page_def invalidateLocalTLB_VAASID_def by (wp | simp cong: if_cong split del: if_split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st\<rbrace> flush_page page_size pd asid vptr \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st\<rbrace> do assert (vptr && mask pageBits = 0);
root_switched <- set_vm_root_for_flush pd asid;
maybe_hw_asid <- load_hw_asid asid;
when (maybe_hw_asid \<noteq> None) $ do hw_asid <- return (the maybe_hw_asid);
do_machine_op $ machine_op_lift (invalidateLocalTLB_VAASID_impl (vptr || UCAST(8 \<rightarrow> 32) hw_asid));
when root_switched $ gets cur_thread >>= set_vm_root
od
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory ArchArch_IF

lemma flush_page_arm_global_pd[wp]:
  "flush_page pgsz pd asid vptr \<lbrace>\<lambda>s. P (arm_global_pd (arch_state s))\<rbrace>" unfolding flush_page_def by (wp | simp cong: if_cong split del: if_split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (arm_global_pd (arch_state s))\<rbrace> flush_page pgsz pd asid vptr \<lbrace>\<lambda>_ s. P (arm_global_pd (arch_state s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (arm_global_pd (arch_state s))\<rbrace> do assert (vptr && mask pageBits = 0);
root_switched <- set_vm_root_for_flush pd asid;
maybe_hw_asid <- load_hw_asid asid;
when (maybe_hw_asid \<noteq> None) $ do hw_asid <- return (the maybe_hw_asid);
do_machine_op $ invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) hw_asid);
when root_switched $ gets cur_thread >>= set_vm_root
od
od \<lbrace>\<lambda>_ s. P (arm_global_pd (arch_state s))\<rbrace>
theory ArchArch_IF

lemma mapM_swp_store_pte_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
   mapM (swp store_pte A) slots
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (rule_tac Q="\<lambda> _. globals_equiv st and valid_arch_state"
               in hoare_strengthen_post) apply (wp mapM_wp' store_pte_globals_equiv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> mapM (swp store_pte A) slots \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> mapM (swp store_pte A) slots \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state\<rbrace>
 2. \<And>rv s. (globals_equiv st and valid_arch_state) s \<Longrightarrow> globals_equiv st s proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma mapM_swp_store_pde_globals_equiv:
  "\<lbrace>globals_equiv st and (\<lambda>s. \<forall>x \<in> set slots. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))\<rbrace>
   mapM (swp store_pde A) slots
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (rule_tac Q="\<lambda>_. globals_equiv st and
                         (\<lambda>s. \<forall>x \<in> set slots. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))"
               in hoare_strengthen_post) apply (wp mapM_wp' store_pde_globals_equiv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and (\<lambda>s. \<forall>x\<in>set slots. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))\<rbrace> mapM (swp store_pde A) slots \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>globals_equiv st and (\<lambda>s. \<forall>x\<in>set slots. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))\<rbrace> mapM (swp store_pde A) slots \<lbrace>\<lambda>_. globals_equiv st and (\<lambda>s. \<forall>x\<in>set slots. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))\<rbrace>
 2. \<And>rv s. (globals_equiv st and (\<lambda>s. \<forall>x\<in>set slots. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))) s \<Longrightarrow> globals_equiv st s proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma mapM_swp_store_pte_valid_arch_state[wp]:
  "mapM (swp store_pte A) slots \<lbrace>valid_arch_state\<rbrace>" by (wp mapM_wp' | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> mapM (swp store_pte A) slots \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
theory ArchArch_IF

lemma mapM_x_swp_store_pde_globals_equiv :
  "\<lbrace>globals_equiv st and (\<lambda>s. \<forall>x \<in> set slots. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))\<rbrace>
   mapM_x (swp store_pde A) slots
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (rule_tac Q="\<lambda>_. globals_equiv st and
                         (\<lambda>s. \<forall>x \<in> set slots. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))"
               in hoare_strengthen_post) apply (wp mapM_x_wp' store_pde_globals_equiv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and (\<lambda>s. \<forall>x\<in>set slots. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))\<rbrace> mapM_x (swp store_pde A) slots \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>globals_equiv st and (\<lambda>s. \<forall>x\<in>set slots. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))\<rbrace> mapM_x (swp store_pde A) slots \<lbrace>\<lambda>_. globals_equiv st and (\<lambda>s. \<forall>x\<in>set slots. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))\<rbrace>
 2. \<And>rv s. (globals_equiv st and (\<lambda>s. \<forall>x\<in>set slots. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))) s \<Longrightarrow> globals_equiv st s proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma arm_global_pd_not_tcb:
  "valid_arch_state s \<Longrightarrow> get_tcb (arm_global_pd (arch_state s)) s = None" unfolding valid_arch_state_def apply (case_tac "get_tcb (arm_global_pd (arch_state s)) s") apply (auto simp: get_tcb_ko_at obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_state s \<Longrightarrow> get_tcb (arm_global_pd (arch_state s)) s = None proof (prove)
goal (1 subgoal):
 1. valid_asid_table (asid_table s) s \<and> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s \<and> valid_global_pts s \<and> is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)) \<Longrightarrow> get_tcb (arm_global_pd (arch_state s)) s = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_asid_table (asid_table s) s \<and> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s \<and> valid_global_pts s \<and> is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); get_tcb (arm_global_pd (arch_state s)) s = None\<rbrakk> \<Longrightarrow> get_tcb (arm_global_pd (arch_state s)) s = None
 2. \<And>a. \<lbrakk>valid_asid_table (asid_table s) s \<and> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s \<and> valid_global_pts s \<and> is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); get_tcb (arm_global_pd (arch_state s)) s = Some a\<rbrakk> \<Longrightarrow> get_tcb (arm_global_pd (arch_state s)) s = None proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma length_msg_lt_msg_max:
  "length msg_registers < msg_max_length" by (simp add: msg_registers_def msgRegisters_def upto_enum_def fromEnum_def enum_register msg_max_length_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length msg_registers < msg_max_length
theory ArchArch_IF

lemma retype_region_ASIDPoolObj_globals_equiv:
  "\<lbrace>globals_equiv s and (\<lambda>sa. ptr \<noteq> arm_global_pd (arch_state s)) and (\<lambda>sa. ptr \<noteq> idle_thread sa)\<rbrace>
   retype_region ptr 1 0 (ArchObject ASIDPoolObj) dev
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding retype_region_def apply (wpsimp wp: modify_wp dxo_wp_weak
              simp: trans_state_update[symmetric] simp_del: trans_state_update) apply (fastforce simp: globals_equiv_def idle_equiv_def tcb_at_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and (\<lambda>sa. ptr \<noteq> arm_global_pd (arch_state s)) and (\<lambda>sa. ptr \<noteq> idle_thread sa)\<rbrace> retype_region ptr 1 0 (ArchObject ASIDPoolObj) dev \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and (\<lambda>sa. ptr \<noteq> arm_global_pd (arch_state s)) and (\<lambda>sa. ptr \<noteq> idle_thread sa)\<rbrace> do obj_size <- return $ 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0;
ptrs <- return $ map (\<lambda>p. ptr_add ptr (p * obj_size)) [0..<1];
when (ArchObject ASIDPoolObj \<noteq> Untyped) (do kh <- gets kheap;
kh' <- return $ foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject ASIDPoolObj) dev 0)) ptrs kh;
do_extended_op (retype_region_ext ptrs (ArchObject ASIDPoolObj));
modify $ kheap_update (K kh')
od);
return $ ptrs
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>globals_equiv s sa; ptr \<noteq> arm_global_pd (arch_state s); ptr \<noteq> idle_thread sa\<rbrakk> \<Longrightarrow> globals_equiv s (sa\<lparr>kheap := (kheap sa)(ptr \<mapsto> default_object (ArchObject ASIDPoolObj) dev 0)\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma perform_asid_pool_invocation_globals_equiv:
  "\<lbrace>globals_equiv s and valid_arch_state\<rbrace> perform_asid_pool_invocation api \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding perform_asid_pool_invocation_def apply (rule hoare_weaken_pre) apply (wp modify_wp set_asid_pool_globals_equiv set_cap_globals_equiv''
        get_cap_wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> perform_asid_pool_invocation api \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> case api of Assign asid pool_ptr ct_slot \<Rightarrow> do pd_cap <- get_cap ct_slot;
case pd_cap of ArchObjectCap (PageDirectoryCap pd_base x) \<Rightarrow> do pool <- get_asid_pool pool_ptr;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid \<mapsto> pd_base));
set_cap (ArchObjectCap $ PageDirectoryCap pd_base (Some asid)) ct_slot;
set_asid_pool pool_ptr pool'
od | ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case api of Assign asid pool_ptr ct_slot \<Rightarrow> do pd_cap <- get_cap ct_slot;
case pd_cap of ArchObjectCap (PageDirectoryCap pd_base x) \<Rightarrow> do pool <- get_asid_pool pool_ptr;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid \<mapsto> pd_base));
set_cap (ArchObjectCap $ PageDirectoryCap pd_base (Some asid)) ct_slot;
set_asid_pool pool_ptr pool'
od | ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 2. \<And>sa. (globals_equiv s and valid_arch_state) sa \<Longrightarrow> ?Q sa proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma arch_perform_invocation_globals_equiv:
  "\<lbrace>globals_equiv s and invs and ct_active and valid_arch_inv ai
                    and authorised_for_globals_arch_inv ai\<rbrace>
   arch_perform_invocation ai
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding arch_perform_invocation_def apply (wpsimp wp: perform_page_table_invocation_globals_equiv
                   perform_page_directory_invocation_globals_equiv
                   perform_page_invocation_globals_equiv
                   perform_asid_control_invocation_globals_equiv
                   perform_asid_pool_invocation_globals_equiv)+ apply (auto simp: authorised_for_globals_arch_inv_def
              simp: invs_def valid_state_def valid_arch_inv_def invs_valid_vs_lookup) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and invs and ct_active and valid_arch_inv ai and authorised_for_globals_arch_inv ai\<rbrace> arch_perform_invocation ai \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and invs and ct_active and valid_arch_inv ai and authorised_for_globals_arch_inv ai\<rbrace> liftE $ case ai of InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | InvokePage oper \<Rightarrow> perform_page_invocation oper | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>globals_equiv s sa; invs sa; ct_active sa; valid_arch_inv ai sa; authorised_for_globals_arch_inv ai sa\<rbrakk> \<Longrightarrow> (\<forall>x. ai = InvokePageTable x \<longrightarrow> valid_global_refs sa \<and> valid_global_objs sa \<and> valid_arch_state sa \<and> pspace_aligned sa \<and> valid_vspace_objs sa \<and> valid_vs_lookup sa \<and> valid_kernel_mappings sa \<and> authorised_for_globals_page_table_inv x sa) \<and> (\<forall>x. ai = InvokePage x \<longrightarrow> authorised_for_globals_page_inv x sa \<and> valid_page_inv x sa \<and> valid_arch_state sa \<and> pspace_aligned sa \<and> valid_vspace_objs sa \<and> valid_global_objs sa \<and> valid_vs_lookup sa \<and> valid_global_refs sa \<and> valid_idle sa) \<and> (\<forall>x. ai = InvokeASIDControl x \<longrightarrow> valid_aci x sa) \<and> ((\<exists>x. ai = InvokeASIDPool x) \<longrightarrow> valid_arch_state sa) proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma find_pd_for_asid_authority3:
  "\<lbrace>\<lambda>s. \<forall>pd. (pspace_aligned s \<and> valid_vspace_objs s \<longrightarrow> is_aligned pd pd_bits) \<and> (\<exists>\<rhd> pd) s
             \<longrightarrow> Q pd s\<rbrace>
   find_pd_for_asid asid
   \<lbrace>Q\<rbrace>, -" apply (clarsimp simp: validE_R_def validE_def valid_def imp_conjL[symmetric]) apply (frule in_inv_by_hoareD[OF find_pd_for_asid_inv], clarsimp) apply (drule spec, erule mp) apply (simp add: use_validE_R[OF _ find_pd_for_asid_authority1]
                   use_validE_R[OF _ find_pd_for_asid_aligned_pd_bits]
                   use_validE_R[OF _ find_pd_for_asid_lookup]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pd. (pspace_aligned s \<and> valid_vspace_objs s \<longrightarrow> is_aligned pd pd_bits) \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> Q pd s\<rbrace> find_pd_for_asid asid \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s b r. \<lbrakk>\<forall>pd. (pspace_aligned s \<and> valid_vspace_objs s \<longrightarrow> is_aligned pd pd_bits) \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> Q pd s; (Inr r, b) \<in> fst (find_pd_for_asid asid s)\<rbrakk> \<Longrightarrow> Q r b proof (prove)
goal (1 subgoal):
 1. \<And>s r. \<lbrakk>\<forall>pd. (pspace_aligned s \<and> valid_vspace_objs s \<longrightarrow> is_aligned pd pd_bits) \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> Q pd s; (Inr r, s) \<in> fst (find_pd_for_asid asid s)\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>s r. (Inr r, s) \<in> fst (find_pd_for_asid asid s) \<Longrightarrow> (pspace_aligned s \<and> valid_vspace_objs s \<longrightarrow> is_aligned r pd_bits) \<and> (\<exists>ref. (ref \<rhd> r) s) proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma valid_arch_arm_asid_table_unmap:
  "valid_arch_state s \<and> tab = arm_asid_table (arch_state s)
   \<longrightarrow> valid_arch_state
         (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := tab(asid_high_bits_of base := None)\<rparr>\<rparr>)" by (clarsimp simp: valid_state_def valid_arch_state_unmap_strg)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_state s \<and> tab = asid_table s \<longrightarrow> valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := tab(asid_high_bits_of base := None)\<rparr>\<rparr>)
theory ArchArch_IF

lemma valid_arch_objs_arm_asid_table_unmap:
  "valid_vspace_objs s \<and> tab = arm_asid_table (arch_state s)
   \<longrightarrow> valid_vspace_objs
         (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := tab(asid_high_bits_of base := None)\<rparr>\<rparr>)" by (clarsimp simp: valid_state_def valid_vspace_objs_unmap_strg)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vspace_objs s \<and> tab = asid_table s \<longrightarrow> valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := tab(asid_high_bits_of base := None)\<rparr>\<rparr>)
theory ArchArch_IF

lemma valid_vspace_objs_arm_asid_table_unmap:
  "valid_vspace_objs s \<and> tab = arm_asid_table (arch_state s)
   \<longrightarrow> valid_vspace_objs
         (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := tab(asid_high_bits_of base := None)\<rparr>\<rparr>)" by (clarsimp simp: valid_state_def valid_vspace_objs_unmap_strg)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vspace_objs s \<and> tab = asid_table s \<longrightarrow> valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := tab(asid_high_bits_of base := None)\<rparr>\<rparr>)
theory ArchArch_IF

lemma set_asid_pool_arch_objs_unmap'':
  "\<lbrace>(valid_vspace_objs and ko_at (ArchObj (ASIDPool ap)) p) and K(f = (ap |` S))\<rbrace>
   set_asid_pool p f
   \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" apply (rule hoare_gen_asm) apply simp apply (rule set_asid_pool_vspace_objs_unmap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and ako_at (ASIDPool ap) p and K (f = ap |` S)\<rbrace> set_asid_pool p f \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. f = ap |` S \<Longrightarrow> \<lbrace>valid_vspace_objs and ako_at (ASIDPool ap) p\<rbrace> set_asid_pool p f \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. f = ap |` S \<Longrightarrow> \<lbrace>valid_vspace_objs and ako_at (ASIDPool ap) p\<rbrace> set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal:
No subgoals!