kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchVSpace_AI

lemma cacheRangeOp_respects_device_region[wp]:
  assumes valid_f: "\<And>a b P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> f a b \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>"
  shows "\<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> cacheRangeOp f a b c\<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>" apply (clarsimp simp: do_flush_def cacheRangeOp_def) apply (rule hoare_pre) apply (wp mapM_x_wp valid_f |  wpc | clarsimp | assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> cacheRangeOp f a b c \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> mapM_x (\<lambda>(x, y). f x y) (zip [lineStart a , lineStart a + word_of_nat cacheLine .e. lineStart b] [lineStart c , lineStart c + word_of_nat cacheLine .e. lineStart (c + (b - a))]) \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> mapM_x (\<lambda>(x, y). f x y) (zip [lineStart a , lineStart a + word_of_nat cacheLine .e. lineStart b] [lineStart c , lineStart c + word_of_nat cacheLine .e. lineStart (c + (b - a))]) \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>
 2. \<And>s. P (device_state s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma dmo_invs_lift:
  assumes dev: "\<And>P. f \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace>"
  assumes mem: "\<And>P. f \<lbrace>\<lambda>ms. P (underlying_memory ms)\<rbrace>"
  assumes irq: "\<And>P. f \<lbrace>\<lambda>ms. P (irq_masks ms)\<rbrace>"
  shows "do_machine_op f \<lbrace>invs\<rbrace>" unfolding invs_def valid_state_def valid_pspace_def valid_irq_states_def valid_machine_state_def by (wpsimp wp: dev hoare_vcg_all_lift hoare_vcg_disj_lift
                 dmo_inv_prop_lift[where g=underlying_memory, OF mem]
                 pspace_respects_device_region_dmo
                 cap_refs_respects_device_region_dmo
     | wps dmo_inv_prop_lift[where g=irq_masks, OF irq])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op f \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and (\<lambda>s. valid_irq_masks (interrupt_states s) (irq_masks (machine_state s))) and valid_ioports and (\<lambda>s. \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0) and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace> do_machine_op f \<lbrace>\<lambda>_. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and (\<lambda>s. valid_irq_masks (interrupt_states s) (irq_masks (machine_state s))) and valid_ioports and (\<lambda>s. \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0) and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace>
theory ArchVSpace_AI

lemma perform_page_directory_invocation_invs[wp]:
  "\<lbrace>invs and valid_pdi pdi\<rbrace>
     perform_page_directory_invocation pdi
   \<lbrace>\<lambda>_. invs\<rbrace>" apply (cases pdi) apply (clarsimp simp: perform_page_directory_invocation_def) apply (wpsimp wp: dmo_invs_lift set_vm_root_for_flush_invs
                     hoare_vcg_const_imp_lift hoare_vcg_all_lift) apply (simp add: valid_pdi_def) apply (clarsimp simp: perform_page_directory_invocation_def valid_pdi_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_pdi pdi\<rbrace> perform_page_directory_invocation pdi \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. pdi = PageDirectoryFlush x11 x12 x13 x14 x15 x16 \<Longrightarrow> \<lbrace>invs and valid_pdi pdi\<rbrace> perform_page_directory_invocation pdi \<lbrace>\<lambda>_. invs\<rbrace>
 2. pdi = PageDirectoryNothing \<Longrightarrow> \<lbrace>invs and valid_pdi pdi\<rbrace> perform_page_directory_invocation pdi \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. pdi = PageDirectoryFlush x11 x12 x13 x14 x15 x16 \<Longrightarrow> \<lbrace>invs and valid_pdi (PageDirectoryFlush x11 x12 x13 x14 x15 x16)\<rbrace> when (x12 < x13) (do root_switched <- set_vm_root_for_flush x15 x16;
y <- do_machine_op (do_flush x11 x12 x13 x14);
when root_switched (gets cur_thread >>= set_vm_root)
od) \<lbrace>\<lambda>_. invs\<rbrace>
 2. pdi = PageDirectoryNothing \<Longrightarrow> \<lbrace>invs and valid_pdi pdi\<rbrace> perform_page_directory_invocation pdi \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 s. \<lbrakk>pdi = PageDirectoryFlush x11 x12 x13 x14 x15 x16; invs s; valid_pdi (PageDirectoryFlush x11 x12 x13 x14 x15 x16) s; x12 < x13\<rbrakk> \<Longrightarrow> x16 \<le> mask local.asid_bits
 2. pdi = PageDirectoryNothing \<Longrightarrow> \<lbrace>invs and valid_pdi pdi\<rbrace> perform_page_directory_invocation pdi \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. pdi = PageDirectoryNothing \<Longrightarrow> \<lbrace>invs and valid_pdi pdi\<rbrace> perform_page_directory_invocation pdi \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma flush_page_invs:
  "\<lbrace>invs and K (asid \<le> mask asid_bits)\<rbrace>
   flush_page sz pd asid vptr
   \<lbrace>\<lambda>_. invs\<rbrace>" unfolding flush_page_def by (wpsimp wp: dmo_invs_lift set_vm_root_for_flush_invs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (asid \<le> mask local.asid_bits)\<rbrace> flush_page sz pd asid vptr \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (asid \<le> mask local.asid_bits)\<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>_. invs\<rbrace>
theory ArchVSpace_AI

lemma find_pd_for_asid_lookup_slot [wp]:
  "\<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> find_pd_for_asid asid
  \<lbrace>\<lambda>rv. \<exists>\<rhd> (lookup_pd_slot rv vptr && ~~ mask pd_bits)\<rbrace>, -" apply (rule hoare_pre) apply (rule hoare_post_imp_R) apply (rule hoare_vcg_R_conj) apply (rule find_pd_for_asid_lookup) apply (rule find_pd_for_asid_aligned_pd) apply (simp add: pd_shifting lookup_pd_slot_def Let_def) apply simp 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. \<exists>ref. (ref \<rhd> (lookup_pd_slot rv vptr && ~~ mask pd_bits)) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s. \<exists>ref. (ref \<rhd> (lookup_pd_slot rv vptr && ~~ mask pd_bits)) s\<rbrace>, -
 2. \<And>s. (pspace_aligned and valid_vspace_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'\<rbrace> find_pd_for_asid asid \<lbrace>?Q'3\<rbrace>, -
 2. \<And>rv s. ?Q'3 rv s \<Longrightarrow> \<exists>ref. (ref \<rhd> (lookup_pd_slot rv vptr && ~~ mask pd_bits)) s
 3. \<And>s. (pspace_aligned and valid_vspace_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P6\<rbrace> find_pd_for_asid asid \<lbrace>?Q6\<rbrace>, -
 2. \<lbrace>?P'6\<rbrace> find_pd_for_asid asid \<lbrace>?Q'6\<rbrace>, -
 3. \<And>rv s. ?Q6 rv s \<and> ?Q'6 rv s \<Longrightarrow> \<exists>ref. (ref \<rhd> (lookup_pd_slot rv vptr && ~~ mask pd_bits)) s
 4. \<And>s. (pspace_aligned and valid_vspace_objs) s \<Longrightarrow> ?P6 s \<and> ?P'6 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'6\<rbrace> find_pd_for_asid asid \<lbrace>?Q'6\<rbrace>, -
 2. \<And>rv s. (\<exists>ref. (ref \<rhd> rv) s) \<and> ?Q'6 rv s \<Longrightarrow> \<exists>ref. (ref \<rhd> (lookup_pd_slot rv vptr && ~~ mask pd_bits)) s
 3. \<And>s. (pspace_aligned and valid_vspace_objs) s \<Longrightarrow> True \<and> ?P'6 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (\<exists>ref. (ref \<rhd> rv) s) \<and> is_aligned rv 14 \<Longrightarrow> \<exists>ref. (ref \<rhd> (lookup_pd_slot rv vptr && ~~ mask pd_bits)) s
 2. \<And>s. (pspace_aligned and valid_vspace_objs) s \<Longrightarrow> True \<and> (pspace_aligned and valid_vspace_objs) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned and valid_vspace_objs) s \<Longrightarrow> True \<and> (pspace_aligned and valid_vspace_objs) s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma find_pd_for_asid_pde_at_add [wp]:
 "\<lbrace>K (x \<in> set [0,4 .e. 0x3C] \<and> is_aligned vptr 24) and pspace_aligned and valid_vspace_objs\<rbrace>
  find_pd_for_asid asid \<lbrace>\<lambda>rv. pde_at (x + lookup_pd_slot rv vptr)\<rbrace>, -" apply (rule hoare_pre) apply (rule hoare_post_imp_R) apply (rule hoare_vcg_R_conj) apply (rule find_pd_for_asid_inv [where P=
                 "K (x \<in> set [0, 4 .e. 0x3C] \<and> is_aligned vptr 24) and pspace_aligned", THEN valid_validE_R]) apply (rule find_pd_for_asid_page_directory) apply (auto intro!: pde_at_aligned_vptr) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) and pspace_aligned and valid_vspace_objs\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv. pde_at (x + lookup_pd_slot rv vptr)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv. pde_at (x + lookup_pd_slot rv vptr)\<rbrace>, -
 2. \<And>s. (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) and pspace_aligned and valid_vspace_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'\<rbrace> find_pd_for_asid asid \<lbrace>?Q'3\<rbrace>, -
 2. \<And>rv s. ?Q'3 rv s \<Longrightarrow> pde_at (x + lookup_pd_slot rv vptr) s
 3. \<And>s. (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) and pspace_aligned and valid_vspace_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P6\<rbrace> find_pd_for_asid asid \<lbrace>?Q6\<rbrace>, -
 2. \<lbrace>?P'6\<rbrace> find_pd_for_asid asid \<lbrace>?Q'6\<rbrace>, -
 3. \<And>rv s. ?Q6 rv s \<and> ?Q'6 rv s \<Longrightarrow> pde_at (x + lookup_pd_slot rv vptr) s
 4. \<And>s. (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) and pspace_aligned and valid_vspace_objs) s \<Longrightarrow> ?P6 s \<and> ?P'6 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'6\<rbrace> find_pd_for_asid asid \<lbrace>?Q'6\<rbrace>, -
 2. \<And>rv s. (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) and pspace_aligned) s \<and> ?Q'6 rv s \<Longrightarrow> pde_at (x + lookup_pd_slot rv vptr) s
 3. \<And>s. (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) and pspace_aligned and valid_vspace_objs) s \<Longrightarrow> (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) and pspace_aligned) s \<and> ?P'6 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) and pspace_aligned) s \<and> typ_at (AArch APageDirectory) rv s \<Longrightarrow> pde_at (x + lookup_pd_slot rv vptr) s
 2. \<And>s. (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) and pspace_aligned and valid_vspace_objs) s \<Longrightarrow> (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) and pspace_aligned) s \<and> valid_vspace_objs s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma valid_kernel_mappingsD:
  "\<lbrakk> kheap s pdptr = Some (ArchObj (PageDirectory pd));
     valid_kernel_mappings s \<rbrakk>
      \<Longrightarrow> \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow>
                  (r \<in> set (arm_global_pts (arch_state s)))
                       = (ucast (kernel_base >> 20) \<le> x)" apply (simp add: valid_kernel_mappings_def) apply (drule bspec, erule ranI) apply (simp add: valid_kernel_mappings_if_pd_def
                   kernel_mapping_slots_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s pdptr = Some (ArchObj (PageDirectory pd)); valid_kernel_mappings s\<rbrakk> \<Longrightarrow> \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s pdptr = Some (ArchObj (PageDirectory pd)); \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x\<rbrakk> \<Longrightarrow> \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s pdptr = Some (ArchObj (PageDirectory pd)); valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma lookup_pt_slot_cap_to1[wp]:
  "\<lbrace>invs and \<exists>\<rhd>pd and K (is_aligned pd pd_bits)
                  and K (vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr
   \<lbrace>\<lambda>rv s.  \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap\<rbrace>,-" apply (rule hoare_post_imp_R) apply (rule lookup_pt_slot_cap_to) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr \<lbrace>?Q'\<rbrace>, -
 2. \<And>rv s. ?Q' rv s \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> cap_asid cap \<noteq> None \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6) \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma lookup_pt_slot_cap_to_multiple[wp]:
  "\<lbrace>invs and \<exists>\<rhd>pd and K (is_aligned pd pd_bits)
                  and K (vptr < kernel_base)
                  and K (is_aligned vptr 16)\<rbrace>
     lookup_pt_slot pd vptr
   \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` (\<lambda>x. x + rv) ` set [0 , 4 .e. 0x3C] \<subseteq> obj_refs c) (a, b) s\<rbrace>, -" apply (rule hoare_post_imp_R, rule lookup_pt_slot_cap_to_multiple1) apply (elim conjE exEI cte_wp_at_weakenE) apply (simp add: subset_eq p_0x3C_shift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base) and K (is_aligned vptr 16)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` (\<lambda>x. x + rv) ` set [0 , 4 .e. 0x3C] \<subseteq> obj_refs c) (a, b) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>rv s. is_aligned rv 6 \<and> (\<exists>a b. cte_wp_at (\<lambda>c. is_pt_cap c \<and> cap_asid c \<noteq> None \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [rv , rv + 4 .e. rv + 0x3C] \<subseteq> obj_refs c) (a, b) s) \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` (\<lambda>x. x + rv) ` set [0 , 4 .e. 0x3C] \<subseteq> obj_refs c) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s x xa c. \<lbrakk>is_aligned rv 6; is_pt_cap c; cap_asid c \<noteq> None; (\<lambda>x. x && ~~ mask pt_bits) ` set [rv , rv + 4 .e. rv + 0x3C] \<subseteq> obj_refs c\<rbrakk> \<Longrightarrow> (\<lambda>x. x && ~~ mask pt_bits) ` (\<lambda>x. x + rv) ` set [0 , 4 .e. 0x3C] \<subseteq> obj_refs c proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma find_pd_for_asid_cap_to1[wp]:
  "\<lbrace>invs\<rbrace> find_pd_for_asid asid
   \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> lookup_pd_slot rv vptr && ~~ mask pd_bits \<in> obj_refs cap\<rbrace>, -" apply (rule hoare_post_imp_R, rule find_pd_for_asid_cap_to) apply (clarsimp simp: lookup_pd_slot_pd) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> lookup_pd_slot rv vptr && ~~ mask pd_bits \<in> obj_refs cap\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> rv \<in> obj_refs cap \<and> is_pd_cap cap \<and> s \<turnstile> cap \<and> is_aligned rv pd_bits \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> lookup_pd_slot rv vptr && ~~ mask pd_bits \<in> obj_refs cap proof (prove)
goal (1 subgoal):
 1. \<And>rv s a b cap. \<lbrakk>caps_of_state s (a, b) = Some cap; rv \<in> obj_refs cap; is_pd_cap cap; s \<turnstile> cap; is_aligned rv pd_bits\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> rv \<in> obj_refs cap proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma find_pd_for_asid_cap_to2[wp]:
  "\<lbrace>invs\<rbrace> find_pd_for_asid asid
   \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at
            (\<lambda>cp. lookup_pd_slot rv vptr && ~~ mask pd_bits \<in> obj_refs cp \<and> is_pd_cap cp)
                  (a, b) s\<rbrace>, -" apply (rule hoare_post_imp_R, rule find_pd_for_asid_cap_to) apply (clarsimp simp: lookup_pd_slot_pd cte_wp_at_caps_of_state) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (\<lambda>cp. lookup_pd_slot rv vptr && ~~ mask pd_bits \<in> obj_refs cp \<and> is_pd_cap cp) (a, b) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> rv \<in> obj_refs cap \<and> is_pd_cap cap \<and> s \<turnstile> cap \<and> is_aligned rv pd_bits \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>cp. lookup_pd_slot rv vptr && ~~ mask pd_bits \<in> obj_refs cp \<and> is_pd_cap cp) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s a b cap. \<lbrakk>caps_of_state s (a, b) = Some cap; rv \<in> obj_refs cap; is_pd_cap cap; s \<turnstile> cap; is_aligned rv pd_bits\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> rv \<in> obj_refs cap \<and> is_pd_cap cap proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma find_pd_for_asid_cap_to_multiple[wp]:
  "\<lbrace>invs and K (is_aligned vptr 24)\<rbrace> find_pd_for_asid asid
   \<lbrace>\<lambda>rv s. \<exists>x xa. cte_wp_at (\<lambda>a. (\<lambda>x. x && ~~ mask pd_bits) ` (\<lambda>x. x + lookup_pd_slot rv vptr) ` set [0 , 4 .e. 0x3C] \<subseteq> obj_refs a) (x, xa) s\<rbrace>, -" apply (rule hoare_gen_asmE, rule hoare_post_imp_R, rule find_pd_for_asid_cap_to) apply (elim exEI, clarsimp simp: cte_wp_at_caps_of_state) apply (simp add: lookup_pd_slot_add_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (is_aligned vptr 24)\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s. \<exists>x xa. cte_wp_at (\<lambda>a. (\<lambda>x. x && ~~ mask pd_bits) ` (\<lambda>x. x + lookup_pd_slot rv vptr) ` set [0 , 4 .e. 0x3C] \<subseteq> obj_refs a) (x, xa) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>is_aligned vptr 24; \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> rv \<in> obj_refs cap \<and> is_pd_cap cap \<and> s \<turnstile> cap \<and> is_aligned rv pd_bits\<rbrakk> \<Longrightarrow> \<exists>x xa. cte_wp_at (\<lambda>a. (\<lambda>x. x && ~~ mask pd_bits) ` (\<lambda>x. x + lookup_pd_slot rv vptr) ` set [0 , 4 .e. 0x3C] \<subseteq> obj_refs a) (x, xa) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s x xa cap xd. \<lbrakk>is_aligned vptr 24; caps_of_state s (x, xa) = Some cap; rv \<in> obj_refs cap; is_pd_cap cap; s \<turnstile> cap; is_aligned rv pd_bits; xd \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> xd + lookup_pd_slot rv vptr && ~~ mask pd_bits \<in> obj_refs cap proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma find_pd_for_asid_cap_to_multiple2[wp]:
  "\<lbrace>invs and K (is_aligned vptr 24)\<rbrace>
     find_pd_for_asid asid
   \<lbrace>\<lambda>rv s. \<forall>x\<in>set [0 , 4 .e. 0x3C]. \<exists>a b.
             cte_wp_at (\<lambda>cp. x + lookup_pd_slot rv vptr && ~~ mask pd_bits
                             \<in> obj_refs cp \<and> is_pd_cap cp) (a, b) s\<rbrace>, -" apply (rule hoare_gen_asmE, rule hoare_post_imp_R,
         rule find_pd_for_asid_cap_to) apply (intro ballI, elim exEI,
         clarsimp simp: cte_wp_at_caps_of_state) apply (simp add: lookup_pd_slot_add_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (is_aligned vptr 24)\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s. \<forall>x\<in>set [0 , 4 .e. 0x3C]. \<exists>a b. cte_wp_at (\<lambda>cp. x + lookup_pd_slot rv vptr && ~~ mask pd_bits \<in> obj_refs cp \<and> is_pd_cap cp) (a, b) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>is_aligned vptr 24; \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> rv \<in> obj_refs cap \<and> is_pd_cap cap \<and> s \<turnstile> cap \<and> is_aligned rv pd_bits\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [0 , 4 .e. 0x3C]. \<exists>a b. cte_wp_at (\<lambda>cp. x + lookup_pd_slot rv vptr && ~~ mask pd_bits \<in> obj_refs cp \<and> is_pd_cap cp) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s x xa xb cap. \<lbrakk>is_aligned vptr 24; x \<in> set [0 , 4 .e. 0x3C]; caps_of_state s (xa, xb) = Some cap; rv \<in> obj_refs cap; is_pd_cap cap; s \<turnstile> cap; is_aligned rv pd_bits\<rbrakk> \<Longrightarrow> x + lookup_pd_slot rv vptr && ~~ mask pd_bits \<in> obj_refs cap proof (prove)
goal:
No subgoals!