kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchCNodeInv_AI

lemma weak_derived_mask [CNodeInv_AI_assms]:
  "\<lbrakk> weak_derived c c'; cap_aligned c \<rbrakk> \<Longrightarrow> weak_derived (mask_cap m c) c'" unfolding weak_derived_def apply simp apply (erule disjE) apply simp apply (simp add: mask_cap_def cap_rights_update_def
                   copy_of_def same_object_as_def bits_of_def
                   is_cap_simps acap_rights_update_def
            split: cap.split arch_cap.split)+ apply (clarsimp simp: cap_aligned_def
                        is_aligned_no_overflow) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>weak_derived c c'; cap_aligned c\<rbrakk> \<Longrightarrow> weak_derived (mask_cap m c) c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>copy_of c c' \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = c; cap_aligned c\<rbrakk> \<Longrightarrow> copy_of (mask_cap m c) c' \<and> cap_asid (mask_cap m c) = cap_asid c' \<and> cap_asid_base (mask_cap m c) = cap_asid_base c' \<and> cap_vptr (mask_cap m c) = cap_vptr c' \<or> c' = mask_cap m c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>copy_of c c' \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = c; cap_aligned c\<rbrakk> \<Longrightarrow> copy_of c c' \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = mask_cap m c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_aligned c; copy_of c c' \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c'\<rbrakk> \<Longrightarrow> copy_of c c' \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = mask_cap m c
 2. \<lbrakk>cap_aligned c; c' = c\<rbrakk> \<Longrightarrow> copy_of c c' \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = mask_cap m c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_aligned c; c' = c\<rbrakk> \<Longrightarrow> copy_of c c' \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = mask_cap m c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_aligned c; c' = c\<rbrakk> \<Longrightarrow> \<forall>x31 x32 x33 x34. (\<exists>x35. c = ArchObjectCap (PageCap x31 x32 x33 x34 x35)) \<longrightarrow> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<or> x33 = validate_vm_rights (x33 \<inter> m) proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma vs_cap_ref_update_cap_data[simp, CNodeInv_AI_assms]:
  "vs_cap_ref (update_cap_data P d cap) = vs_cap_ref cap" by (simp add: vs_cap_ref_def update_cap_data_closedform
                arch_update_cap_data_def
         split: cap.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_cap_ref (update_cap_data P d cap) = vs_cap_ref cap
theory ArchCNodeInv_AI

lemma invs_irq_state_independent[intro!, simp, CNodeInv_AI_assms]:
  "invs (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>)
   = invs s" by (clarsimp simp: irq_state_independent_A_def invs_def
      valid_state_def valid_pspace_def valid_mdb_def valid_ioc_def valid_idle_def
      only_idle_def if_unsafe_then_cap_def valid_reply_caps_def
      valid_reply_masters_def valid_global_refs_def valid_arch_state_def
      valid_irq_node_def valid_irq_handlers_def valid_machine_state_def
      valid_arch_caps_def valid_global_objs_def
      valid_kernel_mappings_def equal_kernel_mappings_def
      valid_asid_map_def valid_global_vspace_mappings_def
      pspace_in_kernel_window_def cap_refs_in_kernel_window_def
      cur_tcb_def sym_refs_def state_refs_of_def vspace_at_asid_def
      swp_def valid_irq_states_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = invs s
theory ArchCNodeInv_AI

lemma weak_derived_vs_cap_ref [CNodeInv_AI_assms]:
  "weak_derived c c' \<Longrightarrow> vs_cap_ref c = vs_cap_ref c'" by (auto simp: weak_derived_def copy_of_def
                 same_object_as_def2
          split: if_split_asm elim: vs_cap_ref_master[OF sym])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived c c' \<Longrightarrow> vs_cap_ref c = vs_cap_ref c'
theory ArchCNodeInv_AI

lemma weak_derived_pd_pt_asid:
  "weak_derived c c' \<Longrightarrow> cap_asid c = cap_asid c'
                       \<and> is_pt_cap c = is_pt_cap c'
                       \<and> is_pd_cap c = is_pd_cap c'" by (auto simp: weak_derived_def copy_of_def is_cap_simps
                 same_object_as_def2 is_pt_cap_def
                 cap_master_cap_simps
          split: if_split_asm
          dest!: cap_master_cap_eqDs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived c c' \<Longrightarrow> cap_asid c = cap_asid c' \<and> is_pt_cap c = is_pt_cap c' \<and> is_pd_cap c = is_pd_cap c'
theory ArchCNodeInv_AI

lemma weak_derived_ASIDPool1:
  "weak_derived (cap.ArchObjectCap (ASIDPoolCap ap asid)) cap =
  (cap = cap.ArchObjectCap (ASIDPoolCap ap asid))" apply (rule iffI) prefer 2 apply simp apply (clarsimp simp: weak_derived_def copy_of_def split: if_split_asm) apply (clarsimp simp: same_object_as_def2 cap_master_cap_simps dest!: cap_master_cap_eqDs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived (ArchObjectCap (ASIDPoolCap ap asid)) cap = (cap = ArchObjectCap (ASIDPoolCap ap asid)) proof (prove)
goal (2 subgoals):
 1. weak_derived (ArchObjectCap (ASIDPoolCap ap asid)) cap \<Longrightarrow> cap = ArchObjectCap (ASIDPoolCap ap asid)
 2. cap = ArchObjectCap (ASIDPoolCap ap asid) \<Longrightarrow> weak_derived (ArchObjectCap (ASIDPoolCap ap asid)) cap proof (prove)
goal (2 subgoals):
 1. cap = ArchObjectCap (ASIDPoolCap ap asid) \<Longrightarrow> weak_derived (ArchObjectCap (ASIDPoolCap ap asid)) cap
 2. weak_derived (ArchObjectCap (ASIDPoolCap ap asid)) cap \<Longrightarrow> cap = ArchObjectCap (ASIDPoolCap ap asid) proof (prove)
goal (1 subgoal):
 1. weak_derived (ArchObjectCap (ASIDPoolCap ap asid)) cap \<Longrightarrow> cap = ArchObjectCap (ASIDPoolCap ap asid) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_untyped_cap cap; same_object_as cap (ArchObjectCap (ASIDPoolCap ap asid)); is_reply_cap cap = is_reply_cap (ArchObjectCap (ASIDPoolCap ap asid)); is_master_reply_cap cap = is_master_reply_cap (ArchObjectCap (ASIDPoolCap ap asid)); None = cap_asid cap; Some asid = cap_asid_base cap; None = cap_vptr cap\<rbrakk> \<Longrightarrow> cap = ArchObjectCap (ASIDPoolCap ap asid) proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma weak_derived_ASIDPool2:
  "weak_derived cap (ArchObjectCap (ASIDPoolCap ap asid)) =
  (cap = ArchObjectCap (ASIDPoolCap ap asid))" apply (rule iffI) prefer 2 apply simp apply (clarsimp simp: weak_derived_def copy_of_def split: if_split_asm) apply (auto simp: same_object_as_def2 cap_master_cap_simps dest!: cap_master_cap_eqDs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived cap (ArchObjectCap (ASIDPoolCap ap asid)) = (cap = ArchObjectCap (ASIDPoolCap ap asid)) proof (prove)
goal (2 subgoals):
 1. weak_derived cap (ArchObjectCap (ASIDPoolCap ap asid)) \<Longrightarrow> cap = ArchObjectCap (ASIDPoolCap ap asid)
 2. cap = ArchObjectCap (ASIDPoolCap ap asid) \<Longrightarrow> weak_derived cap (ArchObjectCap (ASIDPoolCap ap asid)) proof (prove)
goal (2 subgoals):
 1. cap = ArchObjectCap (ASIDPoolCap ap asid) \<Longrightarrow> weak_derived cap (ArchObjectCap (ASIDPoolCap ap asid))
 2. weak_derived cap (ArchObjectCap (ASIDPoolCap ap asid)) \<Longrightarrow> cap = ArchObjectCap (ASIDPoolCap ap asid) proof (prove)
goal (1 subgoal):
 1. weak_derived cap (ArchObjectCap (ASIDPoolCap ap asid)) \<Longrightarrow> cap = ArchObjectCap (ASIDPoolCap ap asid) proof (prove)
goal (1 subgoal):
 1. same_object_as (ArchObjectCap (ASIDPoolCap ap asid)) cap \<and> is_reply_cap (ArchObjectCap (ASIDPoolCap ap asid)) = is_reply_cap cap \<and> is_master_reply_cap (ArchObjectCap (ASIDPoolCap ap asid)) = is_master_reply_cap cap \<and> cap_asid cap = None \<and> cap_asid_base cap = Some asid \<and> cap_vptr cap = None \<or> ArchObjectCap (ASIDPoolCap ap asid) = cap \<Longrightarrow> cap = ArchObjectCap (ASIDPoolCap ap asid) proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma cap_swap_cap_refs_in_kernel_window[wp, CNodeInv_AI_assms]:
  "\<lbrace>cap_refs_in_kernel_window and
    cte_wp_at (weak_derived c) a and
    cte_wp_at (weak_derived c') b\<rbrace>
     cap_swap c a c' b \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" apply (simp add: cap_swap_def) apply (rule hoare_pre) apply (wp | simp split del: if_split)+ apply (auto dest!: cap_refs_in_kernel_windowD
               simp: cte_wp_at_caps_of_state weak_derived_cap_range) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace> do y <- set_cap c' a;
y <- set_cap c b;
slot1_p <- gets (\<lambda>s. cdt s a);
slot2_p <- gets (\<lambda>s. cdt s b);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some a then Some b else if cdt n = Some b then Some a else cdt n)(a := if cdt b = Some a then Some b else if cdt b = Some b then Some a else cdt b, b := if cdt a = Some a then Some b else if cdt a = Some b then Some a else cdt a));
y <- do_extended_op (cap_swap_ext a b slot1_p slot2_p);
is_original <- gets is_original_cap;
y <- set_original a (is_original b);
set_original b (is_original a)
od \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do y <- set_cap c' a;
y <- set_cap c b;
slot1_p <- gets (\<lambda>s. cdt s a);
slot2_p <- gets (\<lambda>s. cdt s b);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some a then Some b else if cdt n = Some b then Some a else cdt n)(a := if cdt b = Some a then Some b else if cdt b = Some b then Some a else cdt b, b := if cdt a = Some a then Some b else if cdt a = Some b then Some a else cdt a));
y <- do_extended_op (cap_swap_ext a b slot1_p slot2_p);
is_original <- gets is_original_cap;
y <- set_original a (is_original b);
set_original b (is_original a)
od \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>
 2. \<And>s. (cap_refs_in_kernel_window and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. cap_refs_in_kernel_window s \<and> cte_wp_at (weak_derived c) a s \<and> cte_wp_at (weak_derived c') b s \<Longrightarrow> (\<forall>ref\<in>cap_range c'. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> (\<forall>ref\<in>cap_range c. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma cap_swap_vms[wp, CNodeInv_AI_assms]:
  "\<lbrace>valid_machine_state\<rbrace>  cap_swap c a c' b \<lbrace>\<lambda>rv. valid_machine_state\<rbrace>" apply (simp add: valid_machine_state_def in_user_frame_def) apply (wp cap_swap_typ_at
            hoare_vcg_all_lift hoare_vcg_ex_lift hoare_vcg_disj_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. (\<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s) \<or> underlying_memory (machine_state s) p = 0\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv s. \<forall>p. (\<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s) \<or> underlying_memory (machine_state s) p = 0\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma unat_of_bl_nat_to_cref[CNodeInv_AI_assms]:
  "\<lbrakk> n < 2 ^ len; len < word_bits \<rbrakk>
    \<Longrightarrow> unat (of_bl (nat_to_cref len n) :: word32) = n" apply (simp add: nat_to_cref_def word_bits_conv of_drop_to_bl
                   word_size) apply (subst less_mask_eq) apply (rule order_less_le_trans) apply (erule of_nat_mono_maybe[rotated]) apply (rule power_strict_increasing) apply simp apply simp apply simp apply (rule unat_of_nat32) apply (erule order_less_trans) apply (rule power_strict_increasing) apply (simp add: word_bits_conv) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ len; len < word_bits\<rbrakk> \<Longrightarrow> unat (of_bl (nat_to_cref len n)) = n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> unat (word_of_nat n && mask len) = n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> word_of_nat n < 2 ^ len
 2. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> unat (word_of_nat n) = n proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> word_of_nat n < ?y7
 2. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> ?y7 \<le> 2 ^ len
 3. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> unat (word_of_nat n) = n proof (prove)
goal (3 subgoals):
 1. len < 32 \<Longrightarrow> 2 ^ len < 2 ^ LENGTH(32)
 2. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> word_of_nat (2 ^ len) \<le> 2 ^ len
 3. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> unat (word_of_nat n) = n proof (prove)
goal (4 subgoals):
 1. len < 32 \<Longrightarrow> len < LENGTH(32)
 2. len < 32 \<Longrightarrow> 1 < 2
 3. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> word_of_nat (2 ^ len) \<le> 2 ^ len
 4. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> unat (word_of_nat n) = n proof (prove)
goal (3 subgoals):
 1. len < 32 \<Longrightarrow> 1 < 2
 2. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> word_of_nat (2 ^ len) \<le> 2 ^ len
 3. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> unat (word_of_nat n) = n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> word_of_nat (2 ^ len) \<le> 2 ^ len
 2. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> unat (word_of_nat n) = n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> unat (word_of_nat n) = n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ len; len < 32\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. len < 32 \<Longrightarrow> 2 ^ len < 2 ^ word_bits proof (prove)
goal (2 subgoals):
 1. len < 32 \<Longrightarrow> len < word_bits
 2. len < 32 \<Longrightarrow> 1 < 2 proof (prove)
goal (1 subgoal):
 1. len < 32 \<Longrightarrow> 1 < 2 proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma zombie_is_cap_toE_pre[CNodeInv_AI_assms]:
  "\<lbrakk> s \<turnstile> Zombie ptr zbits n; invs s; m < n \<rbrakk>
     \<Longrightarrow> (ptr, nat_to_cref (zombie_cte_bits zbits) m) \<in> cte_refs (Zombie ptr zbits n) irqn" apply (clarsimp simp add: valid_cap_def cap_aligned_def) apply (clarsimp split: option.split_asm) apply (simp add: unat_of_bl_nat_to_cref) apply (simp add: nat_to_cref_def word_bits_conv) apply (simp add: unat_of_bl_nat_to_cref) apply (simp add: nat_to_cref_def word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> Zombie ptr zbits n; invs s; m < n\<rbrakk> \<Longrightarrow> (ptr, nat_to_cref (zombie_cte_bits zbits) m) \<in> cte_refs (Zombie ptr zbits n) irqn proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; m < n; is_aligned ptr (case zbits of None \<Rightarrow> obj_bits (TCB undefined) | Some x \<Rightarrow> cte_level_bits + x); (case zbits of None \<Rightarrow> obj_bits (TCB undefined) | Some x \<Rightarrow> cte_level_bits + x) < word_bits; case zbits of None \<Rightarrow> tcb_at ptr s \<and> n \<le> 5 | Some b \<Rightarrow> cap_table_at b ptr s \<and> n \<le> 2 ^ b \<and> b \<noteq> 0\<rbrakk> \<Longrightarrow> length (nat_to_cref (zombie_cte_bits zbits) m) = zombie_cte_bits zbits \<and> unat (of_bl (nat_to_cref (zombie_cte_bits zbits) m)) < n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>9 < word_bits; invs s; m < n; zbits = None; is_aligned ptr 9; tcb_at ptr s; n \<le> 5\<rbrakk> \<Longrightarrow> length (nat_to_cref 3 m) = 3 \<and> unat (of_bl (nat_to_cref 3 m)) < n
 2. \<And>x2. \<lbrakk>cte_level_bits + x2 < word_bits; invs s; m < n; zbits = Some x2; is_aligned ptr (cte_level_bits + x2); cap_table_at x2 ptr s; n \<le> 2 ^ x2; 0 < x2\<rbrakk> \<Longrightarrow> length (nat_to_cref x2 m) = x2 \<and> unat (of_bl (nat_to_cref x2 m)) < n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>9 < word_bits; invs s; m < n; zbits = None; is_aligned ptr 9; tcb_at ptr s; n \<le> 5\<rbrakk> \<Longrightarrow> length (nat_to_cref 3 m) = 3
 2. \<And>x2. \<lbrakk>cte_level_bits + x2 < word_bits; invs s; m < n; zbits = Some x2; is_aligned ptr (cte_level_bits + x2); cap_table_at x2 ptr s; n \<le> 2 ^ x2; 0 < x2\<rbrakk> \<Longrightarrow> length (nat_to_cref x2 m) = x2 \<and> unat (of_bl (nat_to_cref x2 m)) < n proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>cte_level_bits + x2 < word_bits; invs s; m < n; zbits = Some x2; is_aligned ptr (cte_level_bits + x2); cap_table_at x2 ptr s; n \<le> 2 ^ x2; 0 < x2\<rbrakk> \<Longrightarrow> length (nat_to_cref x2 m) = x2 \<and> unat (of_bl (nat_to_cref x2 m)) < n proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>cte_level_bits + x2 < word_bits; invs s; m < n; zbits = Some x2; is_aligned ptr (cte_level_bits + x2); cap_table_at x2 ptr s; n \<le> 2 ^ x2; 0 < x2\<rbrakk> \<Longrightarrow> length (nat_to_cref x2 m) = x2 proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma finalise_cap_not_reply_master_unlifted [CNodeInv_AI_assms]:
  "(rv, s') \<in> fst (finalise_cap cap sl s) \<Longrightarrow>
   \<not> is_master_reply_cap (fst rv)" by (case_tac cap, auto simp: is_cap_simps in_monad liftM_def
                               arch_finalise_cap_def
                        split: if_split_asm arch_cap.split_asm bool.split_asm option.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rv, s') \<in> fst (finalise_cap cap sl s) \<Longrightarrow> \<not> is_master_reply_cap (fst rv)
theory ArchCNodeInv_AI

lemma nat_to_cref_0_replicate [CNodeInv_AI_assms]:
  "\<And>n. n < word_bits \<Longrightarrow> nat_to_cref n 0 = replicate n False" apply (subgoal_tac "nat_to_cref n (unat (of_bl (replicate n False))) = replicate n False") apply simp apply (rule nat_to_cref_unat_of_bl') apply (simp add: word_bits_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < word_bits \<Longrightarrow> nat_to_cref n 0 = replicate n False proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>n < word_bits; nat_to_cref n (unat (of_bl (replicate n False))) = replicate n False\<rbrakk> \<Longrightarrow> nat_to_cref n 0 = replicate n False
 2. \<And>n. n < word_bits \<Longrightarrow> nat_to_cref n (unat (of_bl (replicate n False))) = replicate n False proof (prove)
goal (1 subgoal):
 1. \<And>n. n < word_bits \<Longrightarrow> nat_to_cref n (unat (of_bl (replicate n False))) = replicate n False proof (prove)
goal (2 subgoals):
 1. \<And>n. n < word_bits \<Longrightarrow> length (replicate n False) < 32
 2. \<And>n. n < word_bits \<Longrightarrow> n = length (replicate n False) proof (prove)
goal (1 subgoal):
 1. \<And>n. n < word_bits \<Longrightarrow> n = length (replicate n False) proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma prepare_thread_delete_thread_cap [CNodeInv_AI_assms]:
  "\<lbrace>\<lambda>s. caps_of_state s x = Some (cap.ThreadCap p)\<rbrace>
     prepare_thread_delete t
   \<lbrace>\<lambda>rv s. caps_of_state s x = Some (cap.ThreadCap p)\<rbrace>" by (wpsimp simp: prepare_thread_delete_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. caps_of_state s x = Some (ThreadCap p)\<rbrace> prepare_thread_delete t \<lbrace>\<lambda>rv s. caps_of_state s x = Some (ThreadCap p)\<rbrace>
theory ArchCNodeInv_AI

lemma cap_swap_ioports[wp, CNodeInv_AI_assms]:
  "\<lbrace>valid_ioports and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace>
     cap_swap c a c' b
   \<lbrace>\<lambda>rv. valid_ioports\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioports and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv. valid_ioports\<rbrace>
theory ArchCNodeInv_AI

lemma post_cap_delete_pre_is_final_cap':
  "\<And>rv s'' rva s''a s.
       \<lbrakk>valid_ioports s; caps_of_state s slot = Some cap; is_final_cap' cap s; cap_cleanup_opt cap \<noteq> NullCap\<rbrakk>
       \<Longrightarrow> post_cap_delete_pre (cap_cleanup_opt cap) ((caps_of_state s)(slot \<mapsto> NullCap))" apply (clarsimp simp: cap_cleanup_opt_def cte_wp_at_def post_cap_delete_pre_def arch_cap_cleanup_opt_def
                      split: cap.split_asm if_split_asm
                      elim!: ranE dest!: caps_of_state_cteD) 
   (* IRQHandlerCap case *)
    apply (drule(2) final_cap_duplicate_irq) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>rv s'' rva s''a s. \<lbrakk>valid_ioports s; caps_of_state s slot = Some cap; is_final_cap' cap s; cap_cleanup_opt cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> post_cap_delete_pre (cap_cleanup_opt cap) ((caps_of_state s)(slot \<mapsto> NullCap)) proof (prove)
goal (1 subgoal):
 1. \<And>s x10 a b. \<lbrakk>is_final_cap' (IRQHandlerCap x10) s; cap = IRQHandlerCap x10; fst (get_cap slot s) = {(IRQHandlerCap x10, s)}; (a, b) \<noteq> slot; fst (get_cap (a, b) s) = {(IRQHandlerCap x10, s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x10 a b. \<lbrakk>is_final_cap' (IRQHandlerCap x10) s; cap = IRQHandlerCap x10; fst (get_cap slot s) = {(IRQHandlerCap x10, s)}; (a, b) \<noteq> slot; fst (get_cap (a, b) s) = {(IRQHandlerCap x10, s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s x10 a b. \<lbrakk>is_final_cap' (IRQHandlerCap x10) s; cap = IRQHandlerCap x10; (a, b) \<noteq> slot; fst (get_cap (a, b) s) = {(IRQHandlerCap x10, s)}\<rbrakk> \<Longrightarrow> ?x78 s x10 a b \<in> cap_irqs (IRQHandlerCap x10)
 2. \<And>s x10 a b. \<lbrakk>is_final_cap' (IRQHandlerCap x10) s; cap = IRQHandlerCap x10; (a, b) \<noteq> slot; fst (get_cap (a, b) s) = {(IRQHandlerCap x10, s)}\<rbrakk> \<Longrightarrow> slot \<noteq> (a, b)
 3. \<And>s x10 a b. \<lbrakk>is_final_cap' (IRQHandlerCap x10) s; cap = IRQHandlerCap x10; (a, b) \<noteq> slot; fst (get_cap (a, b) s) = {(IRQHandlerCap x10, s)}; ?x78 s x10 a b \<notin> cap_irqs (IRQHandlerCap x10)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!