kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchArch_AI

lemma valid_asid_map_asid_upd_strg:
  "valid_asid_map s \<and>
   ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and>
   asid_table s asid = None \<longrightarrow>
   valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)" apply clarsimp apply (subgoal_tac "asid_update ap asid s") prefer 2 apply unfold_locales[1] apply assumption+ apply (erule (1) asid_update.valid_asid_map') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_asid_map s \<and> ako_at (ASIDPool (\<lambda>x. None)) ap s \<and> asid_table s asid = None \<longrightarrow> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_asid_map s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_asid_map s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; asid_update ap asid s\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)
 2. \<lbrakk>valid_asid_map s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None\<rbrakk> \<Longrightarrow> asid_update ap asid s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_asid_map s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None\<rbrakk> \<Longrightarrow> asid_update ap asid s
 2. \<lbrakk>valid_asid_map s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; asid_update ap asid s\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_asid_map s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None\<rbrakk> \<Longrightarrow> ako_at (ASIDPool (\<lambda>x. None)) ap s
 2. \<lbrakk>valid_asid_map s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None\<rbrakk> \<Longrightarrow> asid_table s asid = None
 3. \<lbrakk>valid_asid_map s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; asid_update ap asid s\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_asid_map s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; asid_update ap asid s\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma valid_vspace_objs_asid_upd_strg:
  "valid_vspace_objs s \<and>
   ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and>
   asid_table s asid = None \<longrightarrow>
   valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)" apply clarsimp apply (subgoal_tac "asid_update ap asid s") prefer 2 apply unfold_locales[1] apply assumption+ apply (erule (1) asid_update.vspace_objs') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vspace_objs s \<and> ako_at (ASIDPool (\<lambda>x. None)) ap s \<and> asid_table s asid = None \<longrightarrow> valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None\<rbrakk> \<Longrightarrow> valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_vspace_objs s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; asid_update ap asid s\<rbrakk> \<Longrightarrow> valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)
 2. \<lbrakk>valid_vspace_objs s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None\<rbrakk> \<Longrightarrow> asid_update ap asid s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_vspace_objs s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None\<rbrakk> \<Longrightarrow> asid_update ap asid s
 2. \<lbrakk>valid_vspace_objs s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; asid_update ap asid s\<rbrakk> \<Longrightarrow> valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_vspace_objs s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None\<rbrakk> \<Longrightarrow> ako_at (ASIDPool (\<lambda>x. None)) ap s
 2. \<lbrakk>valid_vspace_objs s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None\<rbrakk> \<Longrightarrow> asid_table s asid = None
 3. \<lbrakk>valid_vspace_objs s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; asid_update ap asid s\<rbrakk> \<Longrightarrow> valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; asid_update ap asid s\<rbrakk> \<Longrightarrow> valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma valid_global_objs_asid_upd_strg:
  "valid_global_objs s \<and>
   ko_at (ArchObj (arch_kernel_obj.ASIDPool Map.empty)) ap s \<and>
   asid_table s asid = None \<longrightarrow>
   valid_global_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_objs s \<and> ako_at (ASIDPool (\<lambda>x. None)) ap s \<and> asid_table s asid = None \<longrightarrow> valid_global_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)
theory ArchArch_AI

lemma safe_parent_cap_is_device:
  "safe_parent_for m p cap pcap \<Longrightarrow> cap_is_device cap = cap_is_device pcap" by (simp add: safe_parent_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. safe_parent_for m p cap pcap \<Longrightarrow> cap_is_device cap = cap_is_device pcap
theory ArchArch_AI

lemma perform_asid_control_invocation_st_tcb_at:
  "\<lbrace>st_tcb_at (P and (Not \<circ> inactive) and (Not \<circ> idle)) t
    and ct_active and invs and valid_aci aci\<rbrace>
   perform_asid_control_invocation aci
   \<lbrace>\<lambda>_. st_tcb_at P t\<rbrace>" apply (wpsimp wp: perform_asid_control_invocation_pred_tcb_at) apply (fastforce simp: pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t and ct_active and invs and valid_aci aci\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t s; ct_active s; invs s; valid_aci aci s\<rbrakk> \<Longrightarrow> st_tcb_at P t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma invoke_arch_invs[wp]:
  "\<lbrace>invs and ct_active and valid_arch_inv ai\<rbrace>
   arch_perform_invocation ai
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (cases ai, simp_all add: valid_arch_inv_def arch_perform_invocation_def) apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active and valid_arch_inv ai\<rbrace> arch_perform_invocation ai \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x1. ai = InvokePageTable x1 \<Longrightarrow> \<lbrace>invs and ct_active and valid_pti x1\<rbrace> liftE (do y <- perform_page_table_invocation x1;
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x2. ai = InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs and ct_active and valid_pdi x2\<rbrace> liftE (do y <- perform_page_directory_invocation x2;
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x3. ai = InvokePage x3 \<Longrightarrow> \<lbrace>invs and ct_active and valid_page_inv x3\<rbrace> liftE (perform_page_invocation x3) \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x4. ai = InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs and ct_active and valid_aci x4\<rbrace> liftE (do y <- perform_asid_control_invocation x4;
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs and ct_active and valid_apinv x5\<rbrace> liftE (do y <- perform_asid_pool_invocation x5;
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma sts_empty_pde [wp]:
  "\<lbrace>empty_pde_at p\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. empty_pde_at p\<rbrace>" apply (simp add: empty_pde_at_def) apply (rule hoare_pre) apply (wp hoare_vcg_ex_lift set_thread_state_ko) apply (clarsimp simp: is_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>empty_pde_at p\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. empty_pde_at p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<and> pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. \<exists>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<and> pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. \<exists>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<and> pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE\<rbrace>
 2. \<And>s. \<exists>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<and> pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<and> pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE \<Longrightarrow> \<exists>x. (ako_at (PageDirectory x) (p && ~~ mask pd_bits) and K (\<not> is_tcb (ArchObj (PageDirectory x)))) s \<and> x (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma sts_pd_at_asid [wp]:
  "\<lbrace>vspace_at_asid asid pd\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. vspace_at_asid asid pd\<rbrace>" apply (simp add: vspace_at_asid_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>vspace_at_asid asid pd\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. vspace_at_asid asid pd\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>[VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma sts_same_refs_inv[wp]:
  "\<lbrace>\<lambda>s. same_refs m cap s\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. same_refs m cap s\<rbrace>" by (cases m, (clarsimp simp: same_refs_def, wp)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>same_refs m cap\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. same_refs m cap\<rbrace>
theory ArchArch_AI

lemma sts_valid_slots_inv[wp]:
  "\<lbrace>valid_slots m\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_slots m\<rbrace>" by (cases m, (clarsimp simp: valid_slots_def, wp hoare_vcg_ball_lift sts.vs_lookup sts_typ_ats)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_slots m\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_slots m\<rbrace>
theory ArchArch_AI

lemma sts_valid_page_inv[wp]:
"\<lbrace>valid_page_inv page_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_page_inv page_invocation\<rbrace>" apply (cases page_invocation) by (wpsimp wp: hoare_vcg_ex_lift sts_typ_ats hoare_vcg_disj_lift
           simp: valid_page_inv_def same_refs_def
      | wps)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_page_inv page_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_page_inv page_invocation\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13 x14. page_invocation = PageMap x11 x12 x13 x14 \<Longrightarrow> \<lbrace>valid_page_inv page_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_page_inv page_invocation\<rbrace>
 2. \<And>x21 x22. page_invocation = PageUnmap x21 x22 \<Longrightarrow> \<lbrace>valid_page_inv page_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_page_inv page_invocation\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36. page_invocation = PageFlush x31 x32 x33 x34 x35 x36 \<Longrightarrow> \<lbrace>valid_page_inv page_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_page_inv page_invocation\<rbrace>
 4. \<And>x4. page_invocation = PageGetAddr x4 \<Longrightarrow> \<lbrace>valid_page_inv page_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_page_inv page_invocation\<rbrace>
theory ArchArch_AI

lemma sts_valid_pdi_inv[wp]:
  "\<lbrace>valid_pdi page_directory_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_pdi page_directory_invocation\<rbrace>" apply (cases page_directory_invocation) apply (wp | simp add: valid_pdi_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pdi page_directory_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_pdi page_directory_invocation\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. page_directory_invocation = PageDirectoryFlush x11 x12 x13 x14 x15 x16 \<Longrightarrow> \<lbrace>valid_pdi page_directory_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_pdi page_directory_invocation\<rbrace>
 2. page_directory_invocation = PageDirectoryNothing \<Longrightarrow> \<lbrace>valid_pdi page_directory_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_pdi page_directory_invocation\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma create_mapping_entries_inv [wp]:
  "\<lbrace>P\<rbrace> create_mapping_entries base vptr vmsz R A pd \<lbrace>\<lambda>_. P\<rbrace>" by (induct vmsz; wpsimp wp: lookup_pt_slot_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> create_mapping_entries base vptr vmsz R A pd \<lbrace>\<lambda>_. P\<rbrace>
theory ArchArch_AI

lemma create_mappings_empty [wp]:
  "\<lbrace>\<top>\<rbrace> create_mapping_entries base vptr vmsz R A pd \<lbrace>\<lambda>m s. empty_refs m\<rbrace>, -" by (cases vmsz; wpsimp simp: pde_ref_def empty_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> create_mapping_entries base vptr vmsz R A pd \<lbrace>\<lambda>m s. empty_refs m\<rbrace>, -
theory ArchArch_AI

lemma empty_pde_atI:
  "\<lbrakk> ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s;
     pd (ucast (p && mask pd_bits >> 2)) = InvalidPDE \<rbrakk> \<Longrightarrow>
   empty_pde_at p s" by (fastforce simp add: empty_pde_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s; pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> empty_pde_at p s
theory ArchArch_AI

lemma map_up_enum_0x3C:
  "is_aligned (r::32 word) 6 \<Longrightarrow> map (\<lambda>x. x + r) [0 , 4 .e. 0x3C] = [r, r + 4 .e. r + 0x3C]" apply (simp add: upto_enum_step_def upto_enum_def not_less) apply (drule is_aligned_no_overflow') apply simp apply (erule word_plus_mono_right2) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned r 6 \<Longrightarrow> map (\<lambda>x. x + r) [0 , 4 .e. 0x3C] = [r , r + 4 .e. r + 0x3C] proof (prove)
goal (1 subgoal):
 1. is_aligned r 6 \<Longrightarrow> r \<le> r + 0x3C proof (prove)
goal (1 subgoal):
 1. r \<le> r + (2 ^ 6 - 1) \<Longrightarrow> r \<le> r + 0x3C proof (prove)
goal (1 subgoal):
 1. r \<le> r + 0x3F \<Longrightarrow> r \<le> r + 0x3C proof (prove)
goal (1 subgoal):
 1. 0x3C \<le> 0x3F proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma find_pd_for_asid_shifting_voodoo:
  "\<lbrace>pspace_aligned and valid_vspace_objs\<rbrace>
     find_pd_for_asid asid
   \<lbrace>\<lambda>rv s. v >> 20 = rv + (v >> 20 << 2) && mask pd_bits >> 2\<rbrace>,-" apply (rule hoare_post_imp_R,
         rule find_pd_for_asid_aligned_pd) apply (subst pd_shifting_dual, simp) apply (rule word_eqI) apply (simp add: nth_shiftr nth_shiftl word_size) apply safe apply (drule test_bit_size) apply (simp add: word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s. v >> 20 = rv + (v >> 20 << 2) && mask pd_bits >> 2\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>rv s. is_aligned rv 14 \<Longrightarrow> v >> 20 = rv + (v >> 20 << 2) && mask pd_bits >> 2 proof (prove)
goal (1 subgoal):
 1. \<And>rv s. is_aligned rv 14 \<Longrightarrow> v >> 20 = v >> 20 << 2 >> 2 proof (prove)
goal (1 subgoal):
 1. \<And>rv s n. is_aligned rv 14 \<Longrightarrow> n < size (v >> 20) \<longrightarrow> (v >> 20) !! n = (v >> 20 << 2 >> 2) !! n proof (prove)
goal (1 subgoal):
 1. \<And>rv n. is_aligned rv 14 \<Longrightarrow> n < 32 \<longrightarrow> v !! (20 + n) = (n < 30 \<and> v !! (20 + n)) proof (prove)
goal (1 subgoal):
 1. \<And>rv n. \<lbrakk>is_aligned rv 14; n < 32; v !! (20 + n)\<rbrakk> \<Longrightarrow> n < 30 proof (prove)
goal (1 subgoal):
 1. \<And>rv n. \<lbrakk>is_aligned rv 14; n < 32; 20 + n < size v\<rbrakk> \<Longrightarrow> n < 30 proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma valid_global_ptsD2:
  "\<lbrakk>r \<in> set (arm_global_pts (arch_state s)); valid_global_pts s\<rbrakk>
   \<Longrightarrow> \<exists>pt. ko_at (ArchObj (PageTable pt)) r s" apply (clarsimp simp: valid_global_pts_def) apply (drule (1) bspec) apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> set (arm_global_pts (arch_state s)); valid_global_pts s\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) r s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> set (arm_global_pts (arch_state s)); \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) r s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> set (arm_global_pts (arch_state s)); typ_at (AArch APageTable) r s\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) r s proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma cte_wp_at_page_cap_weaken:
  "cte_wp_at ((=) (ArchObjectCap (PageCap dev word seta vmpage_size None))) slot s \<Longrightarrow>
   cte_wp_at (\<lambda>a. \<exists>dev p R sz m. a = ArchObjectCap (PageCap dev p R sz m)) slot s" by (clarsimp simp: cte_wp_at_def mask_cap_def cap_rights_update_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at ((=) (ArchObjectCap (PageCap dev word seta vmpage_size None))) slot s \<Longrightarrow> cte_wp_at (\<lambda>a. \<exists>dev p R sz m. a = ArchObjectCap (PageCap dev p R sz m)) slot s
theory ArchArch_AI

lemma find_pd_for_asid_lookup_pd_wp:
  "\<lbrace> \<lambda>s. valid_vspace_objs s \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> page_directory_at pd s
    \<and> (\<exists>\<rhd> pd) s \<longrightarrow> Q pd s) \<rbrace> find_pd_for_asid asid \<lbrace> Q \<rbrace>, -" apply (rule hoare_post_imp_R) apply (rule hoare_vcg_conj_lift_R[OF find_pd_for_asid_page_directory]) apply (rule hoare_vcg_conj_lift_R[OF find_pd_for_asid_lookup, simplified]) apply (rule hoare_vcg_conj_lift_R[OF find_pd_for_asid_pd_at_asid, simplified]) apply (wp (once) find_pd_for_asid_inv) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_vspace_objs s \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> Q pd s)\<rbrace> find_pd_for_asid asid \<lbrace>Q\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. valid_vspace_objs s \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> Q pd s)\<rbrace> find_pd_for_asid asid \<lbrace>?Q'\<rbrace>, -
 2. \<And>rv s. ?Q' rv s \<Longrightarrow> Q rv s proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> Q pd s\<rbrace> find_pd_for_asid asid \<lbrace>?S3\<rbrace>, -
 2. \<And>rv s. typ_at (AArch APageDirectory) rv s \<and> ?S3 rv s \<Longrightarrow> Q rv s proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> Q pd s\<rbrace> find_pd_for_asid asid \<lbrace>?S6\<rbrace>, -
 2. \<And>rv s. typ_at (AArch APageDirectory) rv s \<and> (\<exists>ref. (ref \<rhd> rv) s) \<and> ?S6 rv s \<Longrightarrow> Q rv s proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> Q pd s\<rbrace> find_pd_for_asid asid \<lbrace>?S9\<rbrace>, -
 2. \<And>rv s. typ_at (AArch APageDirectory) rv s \<and> (\<exists>ref. (ref \<rhd> rv) s) \<and> vspace_at_asid asid rv s \<and> ?S9 rv s \<Longrightarrow> Q rv s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. typ_at (AArch APageDirectory) rv s \<and> (\<exists>ref. (ref \<rhd> rv) s) \<and> vspace_at_asid asid rv s \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> Q pd s) \<Longrightarrow> Q rv s proof (prove)
goal:
No subgoals!