kings-crown/FVELER_Isabelle huggingface dataset:
theory CNodeInv_AI

lemma cap_swap_fd_ifunsafe[wp]:
  "\<lbrace>if_unsafe_then_cap
         and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) a
         and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) b\<rbrace>
     cap_swap_for_delete a b
   \<lbrace>\<lambda>rv s. if_unsafe_then_cap s\<rbrace>" apply (simp add: cap_swap_for_delete_def) apply (wp get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state
           | strengthen cap_irqs_appropriate_strengthen)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) a and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) b\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) a and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) b\<rbrace> when (a \<noteq> b) (do cap1 <- get_cap a;
cap2 <- get_cap b;
cap_swap cap1 a cap2 b
od) \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (if_unsafe_then_cap and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) a and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) b) s \<Longrightarrow> (if a \<noteq> b then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) a s \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) b s \<longrightarrow> (if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap capa) a and ex_cte_cap_wp_to (appropriate_cte_cap cap) b and cte_wp_at (\<lambda>x. cte_refs x = cte_refs cap \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> cap_irqs x = cap_irqs cap)) a and cte_wp_at (\<lambda>x. cte_refs x = cte_refs capa \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> cap_irqs x = cap_irqs capa)) b) s) else if_unsafe_then_cap) s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_swap_fd_zombies[wp]:
  "\<lbrace>zombies_final\<rbrace>
     cap_swap_for_delete p p'
   \<lbrace>\<lambda>rv. zombies_final\<rbrace>" apply (simp add: cap_swap_for_delete_def) apply (wp get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> cap_swap_for_delete p p' \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> when (p \<noteq> p') (do cap1 <- get_cap p;
cap2 <- get_cap p';
cap_swap cap1 p cap2 p'
od) \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. zombies_final s \<Longrightarrow> (if p \<noteq> p' then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) p s \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) p' s \<longrightarrow> (zombies_final and cte_wp_at (\<lambda>x. is_zombie x = is_zombie cap \<and> gen_obj_refs x = gen_obj_refs cap) p and cte_wp_at (\<lambda>x. is_zombie x = is_zombie capa \<and> gen_obj_refs x = gen_obj_refs capa) p') s) else zombies_final) s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_swap_pred_tcb_at[wp]:
  "\<lbrace>pred_tcb_at proj P t\<rbrace> cap_swap c sl c' sl' \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>" unfolding cap_swap_def by (wp | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> cap_swap c sl c' sl' \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> do set_cap c' sl;
set_cap c sl';
slot1_p <- gets (\<lambda>s. cdt s sl);
slot2_p <- gets (\<lambda>s. cdt s sl');
cdt <- gets cdt;
cdt' <- return (\<lambda>n. if cdt n = Some sl then Some sl' else if cdt n = Some sl' then Some sl else cdt n);
set_cdt (cdt'(sl := cdt' sl', sl' := cdt' sl));
do_extended_op (cap_swap_ext sl sl' slot1_p slot2_p);
is_original <- gets is_original_cap;
set_original sl (is_original sl');
set_original sl' (is_original sl)
od \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>
theory CNodeInv_AI

lemma cap_swap_replies:
  "\<lbrace>\<lambda>s. valid_reply_caps s
       \<and> cte_wp_at (weak_derived c) p s
       \<and> cte_wp_at (weak_derived c') p' s
       \<and> p \<noteq> p'\<rbrace>
     cap_swap c p c' p'
   \<lbrace>\<lambda>rv s. valid_reply_caps s\<rbrace>" apply (simp add: valid_reply_caps_def) apply (rule hoare_pre) apply (simp only: imp_conv_disj) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift cap_swap_has_reply_cap_neg) apply (clarsimp simp: fun_upd_def cte_wp_at_caps_of_state
                        unique_reply_caps_cap_swap [simplified fun_upd_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_reply_caps s \<and> cte_wp_at (weak_derived c) p s \<and> cte_wp_at (weak_derived c') p' s \<and> p \<noteq> p'\<rbrace> cap_swap c p c' p' \<lbrace>\<lambda>rv. valid_reply_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s) \<and> cte_wp_at (weak_derived c) p s \<and> cte_wp_at (weak_derived c') p' s \<and> p \<noteq> p'\<rbrace> cap_swap c p c' p' \<lbrace>\<lambda>rv s. (\<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cap_swap c p c' p' \<lbrace>\<lambda>rv s. (\<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)\<rbrace>
 2. \<And>s. (\<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s) \<and> cte_wp_at (weak_derived c) p s \<and> cte_wp_at (weak_derived c') p' s \<and> p \<noteq> p' \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cap_swap c p c' p' \<lbrace>\<lambda>rv s. (\<forall>t. \<not> has_reply_cap t s \<or> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)\<rbrace>
 2. \<And>s. (\<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s) \<and> cte_wp_at (weak_derived c) p s \<and> cte_wp_at (weak_derived c') p' s \<and> p \<noteq> p' \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s) \<and> cte_wp_at (weak_derived c) p s \<and> cte_wp_at (weak_derived c') p' s \<and> p \<noteq> p' \<Longrightarrow> (\<forall>x. \<not> has_reply_cap x s \<and> cte_wp_at (weak_derived c) p s \<and> cte_wp_at (weak_derived c') p' s \<and> p \<noteq> p' \<or> st_tcb_at awaiting_reply x s) \<and> unique_reply_caps ((caps_of_state s)(p \<mapsto> c', p' \<mapsto> c)) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_swap_fd_replies[wp]:
  "\<lbrace>\<lambda>s. valid_reply_caps s\<rbrace>
     cap_swap_for_delete p p'
   \<lbrace>\<lambda>rv s. valid_reply_caps s\<rbrace>" apply (simp add: cap_swap_for_delete_def) apply (wp cap_swap_replies get_cap_wp) apply (fastforce elim: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps\<rbrace> cap_swap_for_delete p p' \<lbrace>\<lambda>rv. valid_reply_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps\<rbrace> when (p \<noteq> p') (do cap1 <- get_cap p;
cap2 <- get_cap p';
cap_swap cap1 p cap2 p'
od) \<lbrace>\<lambda>rv. valid_reply_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_reply_caps s \<Longrightarrow> (if p \<noteq> p' then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) p s \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) p' s \<longrightarrow> valid_reply_caps s \<and> cte_wp_at (weak_derived cap) p s \<and> cte_wp_at (weak_derived capa) p' s \<and> p \<noteq> p') else valid_reply_caps) s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_swap_fd_reply_masters[wp]:
  "\<lbrace>valid_reply_masters and
        cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) p and
        cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) p'\<rbrace>
     cap_swap_for_delete p p'
   \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace>" apply (simp add: cap_swap_for_delete_def) apply (wp cap_swap_reply_masters get_cap_wp) apply (clarsimp simp: cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters and cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) p and cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) p'\<rbrace> cap_swap_for_delete p p' \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters and cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) p and cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) p'\<rbrace> when (p \<noteq> p') (do cap1 <- get_cap p;
cap2 <- get_cap p';
cap_swap cap1 p cap2 p'
od) \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_reply_masters and cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) p and cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) p') s \<Longrightarrow> (if p \<noteq> p' then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) p s \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) p' s \<longrightarrow> (valid_reply_masters and K (\<not> is_master_reply_cap cap \<and> \<not> is_master_reply_cap capa)) s) else valid_reply_masters) s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma copy_of_cte_refs:
  "copy_of cap cap' \<Longrightarrow> cte_refs cap = cte_refs cap'" apply (rule ext, clarsimp simp: copy_of_def split: if_split_asm) apply (cases cap', simp_all add: same_object_as_def) apply (clarsimp simp: is_cap_simps bits_of_def
                      split: cap.split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. copy_of cap cap' \<Longrightarrow> cte_refs cap = cte_refs cap' proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<not> is_untyped_cap cap'; same_object_as cap' cap; is_reply_cap cap' = is_reply_cap cap; is_master_reply_cap cap' = is_master_reply_cap cap\<rbrakk> \<Longrightarrow> cte_refs cap x = cte_refs cap' x proof (prove)
goal (7 subgoals):
 1. \<And>x x32 x33. \<lbrakk>is_ep_cap cap; is_reply_cap (EndpointCap (obj_ref_of cap) x32 x33) = is_reply_cap cap; is_master_reply_cap (EndpointCap (obj_ref_of cap) x32 x33) = is_master_reply_cap cap; cap' = EndpointCap (obj_ref_of cap) x32 x33\<rbrakk> \<Longrightarrow> cte_refs cap x = {}
 2. \<And>x x42 x43. \<lbrakk>is_ntfn_cap cap; is_reply_cap (NotificationCap (obj_ref_of cap) x42 x43) = is_reply_cap cap; is_master_reply_cap (NotificationCap (obj_ref_of cap) x42 x43) = is_master_reply_cap cap; cap' = NotificationCap (obj_ref_of cap) x42 x43\<rbrakk> \<Longrightarrow> cte_refs cap x = {}
 3. \<And>x x51 x52 x53. \<lbrakk>\<exists>m' cr. cap = ReplyCap x51 m' cr; is_reply_cap (ReplyCap x51 x52 x53) = is_reply_cap cap; is_master_reply_cap (ReplyCap x51 x52 x53) = is_master_reply_cap cap; cap' = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> cte_refs cap x = {}
 4. \<And>x x63. \<lbrakk>is_cnode_cap cap; is_reply_cap (CNodeCap (obj_ref_of cap) (bits_of cap) x63) = is_reply_cap cap; is_master_reply_cap (CNodeCap (obj_ref_of cap) (bits_of cap) x63) = is_master_reply_cap cap; cap' = CNodeCap (obj_ref_of cap) (bits_of cap) x63\<rbrakk> \<Longrightarrow> cte_refs cap x = {obj_ref_of cap} \<times> {xs. length xs = bits_of cap}
 5. \<And>x. \<lbrakk>is_thread_cap cap; is_reply_cap (ThreadCap (obj_ref_of cap)) = is_reply_cap cap; is_master_reply_cap (ThreadCap (obj_ref_of cap)) = is_master_reply_cap cap; cap' = ThreadCap (obj_ref_of cap)\<rbrakk> \<Longrightarrow> cte_refs cap x = {obj_ref_of cap} \<times> dom tcb_cap_cases
 6. \<And>x. \<lbrakk>case cap of IRQHandlerCap n \<Rightarrow> False | _ \<Rightarrow> same_region_as IRQControlCap cap; is_reply_cap IRQControlCap = is_reply_cap cap; is_master_reply_cap IRQControlCap = is_master_reply_cap cap; cap' = IRQControlCap\<rbrakk> \<Longrightarrow> cte_refs cap x = {}
 7. \<And>x x12. \<lbrakk>case cap of ArchObjectCap x \<Rightarrow> same_aobject_as x12 x | _ \<Rightarrow> same_region_as (ArchObjectCap x12) cap; is_reply_cap (ArchObjectCap x12) = is_reply_cap cap; is_master_reply_cap (ArchObjectCap x12) = is_master_reply_cap cap; cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> cte_refs cap x = {} proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma copy_of_is_zombie:
  "copy_of cap cap' \<Longrightarrow> is_zombie cap = is_zombie cap'" apply (clarsimp simp: copy_of_def split: if_split_asm) apply (cases cap', simp_all add: same_object_as_def) apply (clarsimp simp: is_cap_simps bits_of_def
                      split: cap.split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. copy_of cap cap' \<Longrightarrow> is_zombie cap = is_zombie cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_untyped_cap cap'; same_object_as cap' cap; is_reply_cap cap' = is_reply_cap cap; is_master_reply_cap cap' = is_master_reply_cap cap\<rbrakk> \<Longrightarrow> is_zombie cap = is_zombie cap' proof (prove)
goal (7 subgoals):
 1. \<And>x32 x33. \<lbrakk>is_ep_cap cap; is_reply_cap (EndpointCap (obj_ref_of cap) x32 x33) = is_reply_cap cap; is_master_reply_cap (EndpointCap (obj_ref_of cap) x32 x33) = is_master_reply_cap cap; cap' = EndpointCap (obj_ref_of cap) x32 x33\<rbrakk> \<Longrightarrow> is_zombie cap = is_zombie (EndpointCap (obj_ref_of cap) x32 x33)
 2. \<And>x42 x43. \<lbrakk>is_ntfn_cap cap; is_reply_cap (NotificationCap (obj_ref_of cap) x42 x43) = is_reply_cap cap; is_master_reply_cap (NotificationCap (obj_ref_of cap) x42 x43) = is_master_reply_cap cap; cap' = NotificationCap (obj_ref_of cap) x42 x43\<rbrakk> \<Longrightarrow> is_zombie cap = is_zombie (NotificationCap (obj_ref_of cap) x42 x43)
 3. \<And>x51 x52 x53. \<lbrakk>\<exists>m' cr. cap = ReplyCap x51 m' cr; is_reply_cap (ReplyCap x51 x52 x53) = is_reply_cap cap; is_master_reply_cap (ReplyCap x51 x52 x53) = is_master_reply_cap cap; cap' = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> is_zombie cap = is_zombie (ReplyCap x51 x52 x53)
 4. \<And>x63. \<lbrakk>is_cnode_cap cap; is_reply_cap (CNodeCap (obj_ref_of cap) (bits_of cap) x63) = is_reply_cap cap; is_master_reply_cap (CNodeCap (obj_ref_of cap) (bits_of cap) x63) = is_master_reply_cap cap; cap' = CNodeCap (obj_ref_of cap) (bits_of cap) x63\<rbrakk> \<Longrightarrow> is_zombie cap = is_zombie (CNodeCap (obj_ref_of cap) (bits_of cap) x63)
 5. \<lbrakk>is_thread_cap cap; is_reply_cap (ThreadCap (obj_ref_of cap)) = is_reply_cap cap; is_master_reply_cap (ThreadCap (obj_ref_of cap)) = is_master_reply_cap cap; cap' = ThreadCap (obj_ref_of cap)\<rbrakk> \<Longrightarrow> is_zombie cap = is_zombie (ThreadCap (obj_ref_of cap))
 6. \<lbrakk>case cap of IRQHandlerCap n \<Rightarrow> False | _ \<Rightarrow> same_region_as IRQControlCap cap; is_reply_cap IRQControlCap = is_reply_cap cap; is_master_reply_cap IRQControlCap = is_master_reply_cap cap; cap' = IRQControlCap\<rbrakk> \<Longrightarrow> is_zombie cap = is_zombie IRQControlCap
 7. \<And>x12. \<lbrakk>case cap of ArchObjectCap x \<Rightarrow> same_aobject_as x12 x | _ \<Rightarrow> same_region_as (ArchObjectCap x12) cap; is_reply_cap (ArchObjectCap x12) = is_reply_cap cap; is_master_reply_cap (ArchObjectCap x12) = is_master_reply_cap cap; cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> is_zombie cap = is_zombie (ArchObjectCap x12) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma copy_of_reply_cap:
  "copy_of (ReplyCap t False R) cap \<Longrightarrow> \<exists> R'. cap = ReplyCap t False R'" apply (clarsimp simp: copy_of_def is_cap_simps) by (cases cap, simp_all add: same_object_as_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. copy_of (ReplyCap t False R) cap \<Longrightarrow> \<exists>R'. cap = ReplyCap t False R' proof (prove)
goal (1 subgoal):
 1. if \<exists>dev r bits f. cap = UntypedCap dev r bits f then cap = ReplyCap t False R else same_object_as cap (ReplyCap t False R) \<and> (\<exists>x R. cap = ReplyCap x False R) \<and> (\<forall>x R. cap \<noteq> ReplyCap x True R) \<Longrightarrow> \<exists>R'. cap = ReplyCap t False R'
theory CNodeInv_AI

lemma copy_of_cap_irqs:
  "copy_of cap cap' \<Longrightarrow> cap_irqs cap = cap_irqs cap'" apply (clarsimp simp: copy_of_def cap_irqs_def split: if_split_asm) apply (cases cap', simp_all add: same_object_as_def) by (clarsimp simp: is_cap_simps bits_of_def cap_range_def
                      split: cap.split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. copy_of cap cap' \<Longrightarrow> cap_irqs cap = cap_irqs cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_untyped_cap cap'; same_object_as cap' cap; is_reply_cap cap' = is_reply_cap cap; is_master_reply_cap cap' = is_master_reply_cap cap\<rbrakk> \<Longrightarrow> set_option (cap_irq_opt cap) = set_option (cap_irq_opt cap') proof (prove)
goal (7 subgoals):
 1. \<And>x32 x33. \<lbrakk>is_ep_cap cap; is_reply_cap (EndpointCap (obj_ref_of cap) x32 x33) = is_reply_cap cap; is_master_reply_cap (EndpointCap (obj_ref_of cap) x32 x33) = is_master_reply_cap cap; cap' = EndpointCap (obj_ref_of cap) x32 x33\<rbrakk> \<Longrightarrow> cap_irq_opt cap = None
 2. \<And>x42 x43. \<lbrakk>is_ntfn_cap cap; is_reply_cap (NotificationCap (obj_ref_of cap) x42 x43) = is_reply_cap cap; is_master_reply_cap (NotificationCap (obj_ref_of cap) x42 x43) = is_master_reply_cap cap; cap' = NotificationCap (obj_ref_of cap) x42 x43\<rbrakk> \<Longrightarrow> cap_irq_opt cap = None
 3. \<And>x51 x52 x53. \<lbrakk>\<exists>m' cr. cap = ReplyCap x51 m' cr; is_reply_cap (ReplyCap x51 x52 x53) = is_reply_cap cap; is_master_reply_cap (ReplyCap x51 x52 x53) = is_master_reply_cap cap; cap' = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> cap_irq_opt cap = None
 4. \<And>x63. \<lbrakk>is_cnode_cap cap; is_reply_cap (CNodeCap (obj_ref_of cap) (bits_of cap) x63) = is_reply_cap cap; is_master_reply_cap (CNodeCap (obj_ref_of cap) (bits_of cap) x63) = is_master_reply_cap cap; cap' = CNodeCap (obj_ref_of cap) (bits_of cap) x63\<rbrakk> \<Longrightarrow> cap_irq_opt cap = None
 5. \<lbrakk>is_thread_cap cap; is_reply_cap (ThreadCap (obj_ref_of cap)) = is_reply_cap cap; is_master_reply_cap (ThreadCap (obj_ref_of cap)) = is_master_reply_cap cap; cap' = ThreadCap (obj_ref_of cap)\<rbrakk> \<Longrightarrow> cap_irq_opt cap = None
 6. \<lbrakk>case cap of IRQHandlerCap n \<Rightarrow> False | _ \<Rightarrow> same_region_as IRQControlCap cap; is_reply_cap IRQControlCap = is_reply_cap cap; is_master_reply_cap IRQControlCap = is_master_reply_cap cap; cap' = IRQControlCap\<rbrakk> \<Longrightarrow> cap_irq_opt cap = None
 7. \<And>x12. \<lbrakk>case cap of ArchObjectCap x \<Rightarrow> same_aobject_as x12 x | _ \<Rightarrow> same_region_as (ArchObjectCap x12) cap; is_reply_cap (ArchObjectCap x12) = is_reply_cap cap; is_master_reply_cap (ArchObjectCap x12) = is_master_reply_cap cap; cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> cap_irq_opt cap = None
theory CNodeInv_AI

lemma copy_of_arch_gen_obj_refs:
  "copy_of cap cap' \<Longrightarrow> arch_gen_refs cap = arch_gen_refs cap'" apply (clarsimp simp: copy_of_def split: if_split_asm) by (cases cap'; clarsimp simp: same_object_as_def is_cap_simps same_aobject_same_arch_gen_refs
                          split: cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. copy_of cap cap' \<Longrightarrow> arch_gen_refs cap = arch_gen_refs cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_untyped_cap cap'; same_object_as cap' cap; is_reply_cap cap' = is_reply_cap cap; is_master_reply_cap cap' = is_master_reply_cap cap\<rbrakk> \<Longrightarrow> arch_gen_refs cap = arch_gen_refs cap'
theory CNodeInv_AI

lemma cap_swap_global_refs[wp]:
  "\<lbrace>valid_global_refs and
      (\<lambda>s. global_refs s \<inter> cap_range c = {}) and
      (\<lambda>s. global_refs s \<inter> cap_range c' = {})\<rbrace>
    cap_swap c a c' b \<lbrace>\<lambda>_. valid_global_refs\<rbrace>" apply (simp add: cap_swap_def set_cdt_def) apply (wp set_cap_globals | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range c = {}) and (\<lambda>s. global_refs s \<inter> cap_range c' = {})\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>_. valid_global_refs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range c = {}) and (\<lambda>s. global_refs s \<inter> cap_range c' = {})\<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 <- do s <- get;
put (s\<lparr>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)\<rparr>)
od;
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>_. valid_global_refs\<rbrace> proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma valid_reply_caps_of_stateD:
  "\<And>p t s R. \<lbrakk> valid_reply_caps s; caps_of_state s p = Some (cap.ReplyCap t False R) \<rbrakk>
   \<Longrightarrow> st_tcb_at awaiting_reply t s" by (fastforce simp: valid_reply_caps_def has_reply_cap_def
                      is_reply_cap_to_def cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>p t s R. \<lbrakk>valid_reply_caps s; caps_of_state s p = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> st_tcb_at awaiting_reply t s
theory CNodeInv_AI

lemma valid_reply_caps_of_stateD':
  "\<And>p t s R. \<lbrakk> valid_reply_caps s; cte_wp_at (is_reply_cap_to t) p s \<rbrakk>
   \<Longrightarrow> st_tcb_at awaiting_reply t s" by (fastforce simp: valid_reply_caps_def has_reply_cap_def
                      is_reply_cap_to_def cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>p t s R. \<lbrakk>valid_reply_caps s; cte_wp_at (is_reply_cap_to t) p s\<rbrakk> \<Longrightarrow> st_tcb_at awaiting_reply t s
theory CNodeInv_AI

lemma weak_derived_cap_irqs:
  "weak_derived c c' \<Longrightarrow> cap_irqs c = cap_irqs c'" by (auto simp add: weak_derived_def copy_of_cap_irqs)

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