kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchFinalise_AI

lemma mapM_x_swp_store_empty_table_set:
  "\<lbrace>page_table_at p
    and pspace_aligned
    and K ((UNIV :: word8 set) \<subseteq> (\<lambda>sl. ucast ((sl && mask pt_bits) >> 2)) ` set slots
                       \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p))\<rbrace>
    mapM_x (swp store_pte InvalidPTE) slots
   \<lbrace>\<lambda>rv s. obj_at (empty_table (S s)) p s\<rbrace>" apply (rule hoare_strengthen_post) apply (rule mapM_x_swp_store_empty_table) apply (clarsimp simp: obj_at_def empty_table_def) apply (clarsimp split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>typ_at (AArch APageTable) p and pspace_aligned and K (UNIV \<subseteq> (\<lambda>sl. UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) ` set slots \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p))\<rbrace> mapM_x (swp store_pte InvalidPTE) slots \<lbrace>\<lambda>rv s. obj_at (empty_table (S s)) p s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>typ_at (AArch APageTable) p and pspace_aligned and K (UNIV \<subseteq> (\<lambda>sl. UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) ` set slots \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p))\<rbrace> mapM_x (swp store_pte InvalidPTE) slots \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> obj_at (empty_table (S s)) p s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. obj_at (empty_table {}) p s \<Longrightarrow> obj_at (empty_table (S s)) p s proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>kheap s p = Some ko; case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> {}) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> S s) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma is_final_cap_pt_asid_eq:
  "is_final_cap' (ArchObjectCap (PageTableCap p y)) s \<Longrightarrow>
   is_final_cap' (ArchObjectCap (PageTableCap p x)) s" apply (clarsimp simp: is_final_cap'_def gen_obj_refs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_final_cap' (ArchObjectCap (PageTableCap p y)) s \<Longrightarrow> is_final_cap' (ArchObjectCap (PageTableCap p x)) s proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma cte_wp_at_obj_refs_singleton_page_table:
  "\<lbrakk>cte_wp_at
      (\<lambda>cap'. obj_refs cap' = {p}
            \<and> (\<exists>p asid. cap' = ArchObjectCap (PageTableCap p asid)))
      (a, b) s\<rbrakk> \<Longrightarrow>
   \<exists>asid. cte_wp_at ((=) (ArchObjectCap (PageTableCap p asid))) (a,b) s" apply (clarsimp simp: cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>cap'. obj_refs cap' = {p} \<and> (\<exists>p asid. cap' = ArchObjectCap (PageTableCap p asid))) (a, b) s \<Longrightarrow> \<exists>asid. cte_wp_at ((=) (ArchObjectCap (PageTableCap p asid))) (a, b) s proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma cte_wp_at_obj_refs_singleton_page_directory:
  "\<lbrakk>cte_wp_at
      (\<lambda>cap'. obj_refs cap' = {p}
            \<and> (\<exists>p asid. cap' = ArchObjectCap (PageDirectoryCap p asid)))
      (a, b) s\<rbrakk> \<Longrightarrow>
   \<exists>asid. cte_wp_at
            ((=) (ArchObjectCap (PageDirectoryCap p asid))) (a,b) s" apply (clarsimp simp: cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>cap'. obj_refs cap' = {p} \<and> (\<exists>p asid. cap' = ArchObjectCap (PageDirectoryCap p asid))) (a, b) s \<Longrightarrow> \<exists>asid. cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid))) (a, b) s proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma is_arch_update_reset_page:
  "is_arch_update
     (ArchObjectCap (PageCap dev p r sz m))
     (ArchObjectCap (PageCap dev p r' sz m'))" apply (simp add: is_arch_update_def is_arch_cap_def cap_master_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_arch_update (ArchObjectCap (PageCap dev p r sz m)) (ArchObjectCap (PageCap dev p r' sz m')) proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma store_pde_pde_wp_at:
  "\<lbrace>\<top>\<rbrace>
   store_pde p x
   \<lbrace>\<lambda>_. pde_wp_at
         (\<lambda>pde. pde = x) (p && ~~ mask pd_bits) (ucast (p && mask pd_bits >> 2))\<rbrace>" apply (wp
    | simp add: store_pde_def set_pd_def set_object_def get_object_def
                obj_at_def pde_wp_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> store_pde p x \<lbrace>\<lambda>_. pde_wp_at (\<lambda>pde. pde = x) (p && ~~ mask pd_bits) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma store_pde_pde_wp_at2:
  "\<lbrace>pde_wp_at (\<lambda>pde. pde = pde.InvalidPDE) ptr slot\<rbrace>
   store_pde p' InvalidPDE
   \<lbrace>\<lambda>_. pde_wp_at (\<lambda>pde. pde = InvalidPDE) ptr slot\<rbrace>" apply (wp
    | simp add: store_pde_def set_pd_def set_object_def get_object_def
                obj_at_def pde_wp_at_def
    | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pde_wp_at (\<lambda>pde. pde = InvalidPDE) ptr slot\<rbrace> store_pde p' InvalidPDE \<lbrace>\<lambda>_. pde_wp_at (\<lambda>pde. pde = InvalidPDE) ptr slot\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma pd_shifting_again3:
  "is_aligned pd pd_bits \<Longrightarrow> ((ucast (ae :: 12 word) << 2) + (pd :: word32) && ~~ mask pd_bits) = pd" apply (subst add.commute) apply (rule pd_shifting_again) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> (UCAST(12 \<rightarrow> 32) ae << 2) + pd && ~~ mask pd_bits = pd proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> pd + (UCAST(12 \<rightarrow> 32) ae << 2) && ~~ mask pd_bits = pd proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma pd_shifting_again4: "is_aligned (pd::word32) pd_bits \<Longrightarrow>
  (ucast (ae::12 word) << 2) + pd && mask pd_bits = (ucast ae << 2)" apply (subst add.commute) apply (simp add:shiftl_t2n mask_add_aligned) apply (rule less_mask_eq) apply (rule word_less_power_trans[where k = 2, simplified]) apply (rule less_le_trans[OF ucast_less]) apply (simp add:pd_bits_def pageBits_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> (UCAST(12 \<rightarrow> 32) ae << 2) + pd && mask pd_bits = UCAST(12 \<rightarrow> 32) ae << 2 proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> pd + (UCAST(12 \<rightarrow> 32) ae << 2) && mask pd_bits = UCAST(12 \<rightarrow> 32) ae << 2 proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> 4 * UCAST(12 \<rightarrow> 32) ae && mask pd_bits = 4 * UCAST(12 \<rightarrow> 32) ae proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> 4 * UCAST(12 \<rightarrow> 32) ae < 2 ^ pd_bits proof (prove)
goal (3 subgoals):
 1. is_aligned pd pd_bits \<Longrightarrow> UCAST(12 \<rightarrow> 32) ae < 2 ^ (pd_bits - 2)
 2. is_aligned pd pd_bits \<Longrightarrow> 2 \<le> pd_bits
 3. is_aligned pd pd_bits \<Longrightarrow> pd_bits < LENGTH(32) proof (prove)
goal (4 subgoals):
 1. is_aligned pd pd_bits \<Longrightarrow> LENGTH(12) < LENGTH(32)
 2. is_aligned pd pd_bits \<Longrightarrow> 2 ^ LENGTH(12) \<le> 2 ^ (pd_bits - 2)
 3. is_aligned pd pd_bits \<Longrightarrow> 2 \<le> pd_bits
 4. is_aligned pd pd_bits \<Longrightarrow> pd_bits < LENGTH(32) proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma pd_shifting_global_refs:
  "\<lbrakk>is_aligned pd pd_bits;
    ae \<le> (kernel_base >> 20) - 1; pd \<notin> global_refs s\<rbrakk>
   \<Longrightarrow> ((ae::word32) << 2) + pd && ~~ mask pd_bits \<notin> global_refs s" apply (cut_tac pd="pd" and ae="ucast ae" in pd_shifting_again3) apply simp apply (simp add: ucast_bl word_rep_drop of_drop_to_bl word_size) apply (insert and_mask_eq_iff_le_mask[where n=12 and w=ae, THEN iffD2]) apply (frule_tac z="mask 12" in order_trans) apply (simp add: mask_def kernel_base_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; ae \<le> (kernel_base >> 20) - 1; pd \<notin> global_refs s\<rbrakk> \<Longrightarrow> (ae << 2) + pd && ~~ mask pd_bits \<notin> global_refs s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; ae \<le> (kernel_base >> 20) - 1; pd \<notin> global_refs s\<rbrakk> \<Longrightarrow> is_aligned pd pd_bits
 2. \<lbrakk>is_aligned pd pd_bits; ae \<le> (kernel_base >> 20) - 1; pd \<notin> global_refs s; (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) ae) << 2) + pd && ~~ mask pd_bits = pd\<rbrakk> \<Longrightarrow> (ae << 2) + pd && ~~ mask pd_bits \<notin> global_refs s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; ae \<le> (kernel_base >> 20) - 1; pd \<notin> global_refs s; (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) ae) << 2) + pd && ~~ mask pd_bits = pd\<rbrakk> \<Longrightarrow> (ae << 2) + pd && ~~ mask pd_bits \<notin> global_refs s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; ae \<le> (kernel_base >> 20) - 1; pd \<notin> global_refs s; (ae && mask 12 << 2) + pd && ~~ mask pd_bits = pd\<rbrakk> \<Longrightarrow> (ae << 2) + pd && ~~ mask pd_bits \<notin> global_refs s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; ae \<le> (kernel_base >> 20) - 1; pd \<notin> global_refs s; (ae && mask 12 << 2) + pd && ~~ mask pd_bits = pd; ae \<le> mask 12 \<Longrightarrow> ae && mask 12 = ae\<rbrakk> \<Longrightarrow> (ae << 2) + pd && ~~ mask pd_bits \<notin> global_refs s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; ae \<le> (kernel_base >> 20) - 1; pd \<notin> global_refs s; (ae && mask 12 << 2) + pd && ~~ mask pd_bits = pd; ae \<le> mask 12 \<Longrightarrow> ae && mask 12 = ae\<rbrakk> \<Longrightarrow> (kernel_base >> 20) - 1 \<le> mask 12
 2. \<lbrakk>is_aligned pd pd_bits; ae \<le> (kernel_base >> 20) - 1; pd \<notin> global_refs s; (ae && mask 12 << 2) + pd && ~~ mask pd_bits = pd; ae \<le> mask 12 \<Longrightarrow> ae && mask 12 = ae; ae \<le> mask 12\<rbrakk> \<Longrightarrow> (ae << 2) + pd && ~~ mask pd_bits \<notin> global_refs s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; ae \<le> (kernel_base >> 20) - 1; pd \<notin> global_refs s; (ae && mask 12 << 2) + pd && ~~ mask pd_bits = pd; ae \<le> mask 12 \<Longrightarrow> ae && mask 12 = ae; ae \<le> mask 12\<rbrakk> \<Longrightarrow> (ae << 2) + pd && ~~ mask pd_bits \<notin> global_refs s proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma word_aligned_pt_slots:
  "\<lbrakk>is_aligned word pt_bits;
    x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk>
  \<Longrightarrow> x && ~~ mask pt_bits = word" apply (simp add: pt_bits_def pageBits_def) apply (drule subsetD[OF upto_enum_step_subset]) apply (frule_tac ptr'=x in mask_in_range) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned word pt_bits; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> x && ~~ mask pt_bits = word proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned word 10; x \<in> set [word , word + 4 .e. 0x3FF + word]\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = word proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned word 10; x \<in> {word..0x3FF + word}\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = word proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned word 10; x \<in> {word..0x3FF + word}; (x && ~~ mask 10 = word) = (x \<in> {word..word + 2 ^ 10 - 1})\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = word proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma caps_of_state_aligned_page_table:
  "\<lbrakk>caps_of_state s slot =
  Some (ArchObjectCap (PageTableCap word option));
  invs s\<rbrakk>
  \<Longrightarrow> is_aligned word pt_bits" apply (frule caps_of_state_valid) apply (frule invs_valid_objs, assumption) apply (frule valid_cap_aligned) apply (simp add: cap_aligned_def pt_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s slot = Some (ArchObjectCap (PageTableCap word option)); invs s\<rbrakk> \<Longrightarrow> is_aligned word pt_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s slot = Some (ArchObjectCap (PageTableCap word option)); invs s\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<lbrakk>caps_of_state s slot = Some (ArchObjectCap (PageTableCap word option)); invs s; s \<turnstile> ArchObjectCap (PageTableCap word option)\<rbrakk> \<Longrightarrow> is_aligned word pt_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s slot = Some (ArchObjectCap (PageTableCap word option)); invs s; s \<turnstile> ArchObjectCap (PageTableCap word option)\<rbrakk> \<Longrightarrow> is_aligned word pt_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s slot = Some (ArchObjectCap (PageTableCap word option)); invs s; s \<turnstile> ArchObjectCap (PageTableCap word option); cap_aligned (ArchObjectCap (PageTableCap word option))\<rbrakk> \<Longrightarrow> is_aligned word pt_bits proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma caps_of_state_aligned_page_directory:
  "\<lbrakk>caps_of_state s slot =
  Some (ArchObjectCap (PageDirectoryCap word option));
  invs s\<rbrakk>
  \<Longrightarrow> is_aligned word pd_bits" apply (frule caps_of_state_valid) apply (frule invs_valid_objs, assumption) apply (frule valid_cap_aligned) apply (simp add: cap_aligned_def pd_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s slot = Some (ArchObjectCap (PageDirectoryCap word option)); invs s\<rbrakk> \<Longrightarrow> is_aligned word pd_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s slot = Some (ArchObjectCap (PageDirectoryCap word option)); invs s\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<lbrakk>caps_of_state s slot = Some (ArchObjectCap (PageDirectoryCap word option)); invs s; s \<turnstile> ArchObjectCap (PageDirectoryCap word option)\<rbrakk> \<Longrightarrow> is_aligned word pd_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s slot = Some (ArchObjectCap (PageDirectoryCap word option)); invs s; s \<turnstile> ArchObjectCap (PageDirectoryCap word option)\<rbrakk> \<Longrightarrow> is_aligned word pd_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s slot = Some (ArchObjectCap (PageDirectoryCap word option)); invs s; s \<turnstile> ArchObjectCap (PageDirectoryCap word option); cap_aligned (ArchObjectCap (PageDirectoryCap word option))\<rbrakk> \<Longrightarrow> is_aligned word pd_bits proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma invs_valid_arch_capsI:
  "invs s \<Longrightarrow> valid_arch_caps s" by (simp add: invs_def valid_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> valid_arch_caps s
theory ArchFinalise_AI

lemma do_machine_op_reachable_pg_cap[wp]:
  "\<lbrace>\<lambda>s. P (reachable_pg_cap cap s)\<rbrace>
   do_machine_op mo
   \<lbrace>\<lambda>rv s. P (reachable_pg_cap cap s)\<rbrace>" apply (simp add:reachable_pg_cap_def,wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (reachable_pg_cap cap s)\<rbrace> do_machine_op mo \<lbrace>\<lambda>rv s. P (reachable_pg_cap cap s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma replaceable_or_arch_update_pg:
  " (case (vs_cap_ref (ArchObjectCap (PageCap dev word fun vm_pgsz y))) of None \<Rightarrow> True | Some ref \<Rightarrow> \<not> (ref \<unrhd> word) s)
  \<longrightarrow> replaceable_or_arch_update s slot (ArchObjectCap (PageCap dev word fun vm_pgsz None))
                (ArchObjectCap (PageCap dev word fun vm_pgsz y))" unfolding replaceable_or_arch_update_def apply (auto simp: is_cap_simps is_arch_update_def cap_master_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case vs_cap_ref (ArchObjectCap (PageCap dev word fun vm_pgsz y)) of None \<Rightarrow> True | Some ref \<Rightarrow> (ref, word) \<notin> vs_lookup_pages s) \<longrightarrow> replaceable_or_arch_update s slot (ArchObjectCap (PageCap dev word fun vm_pgsz None)) (ArchObjectCap (PageCap dev word fun vm_pgsz y)) proof (prove)
goal (1 subgoal):
 1. (case vs_cap_ref (ArchObjectCap (PageCap dev word fun vm_pgsz y)) of None \<Rightarrow> True | Some ref \<Rightarrow> (ref, word) \<notin> vs_lookup_pages s) \<longrightarrow> (if is_pg_cap (ArchObjectCap (PageCap dev word fun vm_pgsz None)) then is_arch_update (ArchObjectCap (PageCap dev word fun vm_pgsz None)) (ArchObjectCap (PageCap dev word fun vm_pgsz y)) \<and> (\<forall>vref. vs_cap_ref (ArchObjectCap (PageCap dev word fun vm_pgsz y)) = Some vref \<longrightarrow> vs_cap_ref (ArchObjectCap (PageCap dev word fun vm_pgsz None)) = Some vref \<and> obj_refs (ArchObjectCap (PageCap dev word fun vm_pgsz None)) = obj_refs (ArchObjectCap (PageCap dev word fun vm_pgsz y)) \<or> (\<forall>oref\<in>obj_refs (ArchObjectCap (PageCap dev word fun vm_pgsz y)). (vref, oref) \<notin> vs_lookup_pages s)) else replaceable s slot (ArchObjectCap (PageCap dev word fun vm_pgsz None)) (ArchObjectCap (PageCap dev word fun vm_pgsz y))) proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma store_pde_vspace_objs_invalid:
  "\<lbrace>valid_vspace_objs\<rbrace> store_pde p ARM_A.InvalidPDE \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" apply (wp store_pde_vspace_objs_unmap) apply (simp add: pde_ref_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs\<rbrace> store_pde p InvalidPDE \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_vspace_objs s \<Longrightarrow> (valid_vspace_objs and valid_pde InvalidPDE and K (pde_ref InvalidPDE = None)) s proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma mapM_x_swp_store_invalid_pte_invs:
  "\<lbrace>invs and (\<lambda>s. \<exists>slot. cte_wp_at
             (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs c \<and>
                  is_pt_cap c) slot s)\<rbrace>
  mapM_x (\<lambda>x. store_pte x InvalidPTE) slots \<lbrace>\<lambda>_. invs\<rbrace>" by (simp add:
    mapM_x_swp_store_pte_invs[unfolded swp_def,
      where pte=InvalidPTE, simplified])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs c \<and> is_pt_cap c) slot s)\<rbrace> mapM_x (\<lambda>x. store_pte x InvalidPTE) slots \<lbrace>\<lambda>_. invs\<rbrace>
theory ArchFinalise_AI

lemma mapM_x_swp_store_invalid_pde_invs:
  "\<lbrace>invs and
   (\<lambda>s. \<forall>sl\<in>set slots.
         ucast (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and
   (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s)\<rbrace>
     mapM_x (\<lambda>x. store_pde x InvalidPDE) slots
   \<lbrace>\<lambda>rv. invs \<rbrace>" apply (simp add:mapM_x_mapM) apply (wp mapM_swp_store_pde_invs_unmap[unfolded swp_def,
              where pde=InvalidPDE, simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<forall>sl\<in>set slots. UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s)\<rbrace> mapM_x (\<lambda>x. store_pde x InvalidPDE) slots \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<forall>sl\<in>set slots. UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s)\<rbrace> do x <- mapM (\<lambda>x. store_pde x InvalidPDE) slots;
return ()
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma (* finalise_cap_irq_node *)[Finalise_AI_asms]:
"\<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> finalise_cap a b \<lbrace>\<lambda>_ s. P (interrupt_irq_node s)\<rbrace>" apply (case_tac a,simp_all) apply (wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> finalise_cap a b \<lbrace>\<lambda>_ s. P (interrupt_irq_node s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33. a = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when b (cancel_all_ipc x31)) \<lbrace>\<lambda>_ s. P (interrupt_irq_node s)\<rbrace>
 2. \<And>x41 x42 x43. a = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when b (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od)) \<lbrace>\<lambda>_ s. P (interrupt_irq_node s)\<rbrace>
 3. \<And>x7. a = ThreadCap x7 \<Longrightarrow> b \<longrightarrow> \<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> do y <- unbind_notification x7;
y <- suspend x7;
y <- prepare_thread_delete x7;
return (Zombie x7 None 5, NullCap)
od \<lbrace>\<lambda>_ s. P (interrupt_irq_node s)\<rbrace>
 4. \<And>x10. a = IRQHandlerCap x10 \<Longrightarrow> b \<longrightarrow> \<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od \<lbrace>\<lambda>_ s. P (interrupt_irq_node s)\<rbrace>
 5. \<And>x111 x112 x113. a = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> do y <- assert b;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>_ s. P (interrupt_irq_node s)\<rbrace>
 6. \<And>x12. a = ArchObjectCap x12 \<Longrightarrow> \<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> arch_finalise_cap x12 b \<lbrace>\<lambda>_ s. P (interrupt_irq_node s)\<rbrace> proof (prove)
goal:
No subgoals!