kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_AI

lemma cap_derive_not_null_helper:
  "\<lbrace>P\<rbrace> derive_cap slot cap \<lbrace>Q\<rbrace>,- \<Longrightarrow>
   \<lbrace>\<lambda>s. cap \<noteq> cap.NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> cap.IRQControlCap \<longrightarrow> P s\<rbrace>
     derive_cap slot
       cap
   \<lbrace>\<lambda>rv s. rv \<noteq> cap.NullCap \<longrightarrow> Q rv s\<rbrace>,-" apply (case_tac cap,
         simp_all add: is_zombie_def,
         safe elim!: hoare_post_imp_R) apply (wp | simp add: derive_cap_def is_zombie_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> derive_cap slot cap \<lbrace>Q\<rbrace>, - \<Longrightarrow> \<lbrace>\<lambda>s. cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap \<longrightarrow> P s\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> Q rv s\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<lbrace>P\<rbrace> derive_cap slot NullCap \<lbrace>Q\<rbrace>, -; cap = NullCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> derive_cap slot NullCap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> Q rv s\<rbrace>, -
 2. \<lbrakk>\<lbrace>P\<rbrace> derive_cap slot IRQControlCap \<lbrace>Q\<rbrace>, -; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> derive_cap slot IRQControlCap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> Q rv s\<rbrace>, -
 3. \<And>x111 x112 x113. \<lbrakk>\<lbrace>P\<rbrace> derive_cap slot (Zombie x111 x112 x113) \<lbrace>Q\<rbrace>, -; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> derive_cap slot (Zombie x111 x112 x113) \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> Q rv s\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma mask_cap_Null [simp]:
  "(mask_cap R c = cap.NullCap) = (c = cap.NullCap)" by (cases c) (auto simp: mask_cap_def cap_rights_update_def split: bool.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (mask_cap R c = NullCap) = (c = NullCap)
theory Ipc_AI

lemma ensure_no_children_wp:
  "\<lbrace>\<lambda>s. descendants_of p (cdt s) = {} \<longrightarrow> P s\<rbrace> ensure_no_children p \<lbrace>\<lambda>_. P\<rbrace>, -" apply (simp add: ensure_no_children_descendants valid_def validE_R_def validE_def) apply (auto simp: in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. descendants_of p (cdt s) = {} \<longrightarrow> P s\<rbrace> ensure_no_children p \<lbrace>\<lambda>_. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<forall>s. (descendants_of p (cdt s) = {} \<longrightarrow> P s \<longrightarrow> (\<forall>x\<in>fst (returnOk () s). case x of (r, s') \<Rightarrow> r = Inr () \<longrightarrow> P s')) \<and> (descendants_of p (cdt s) \<noteq> {} \<longrightarrow> (\<forall>(r, s')\<in>fst (throwError RevokeFirst s). r = Inr () \<longrightarrow> P s')) proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma update_cap_data_closedform:
  "update_cap_data pres w cap =
   (case cap of
      EndpointCap r badge rights \<Rightarrow>
        if badge = 0 \<and> \<not> pres then (EndpointCap r (w && mask badge_bits) rights) else NullCap
    | NotificationCap r badge rights \<Rightarrow>
        if badge = 0 \<and> \<not> pres then (NotificationCap r (w && mask badge_bits) rights) else NullCap
    | CNodeCap r bits guard \<Rightarrow>
        if word_bits < fst (update_cnode_cap_data w) + bits
        then NullCap
        else CNodeCap r bits ((\<lambda>g''. drop (size g'' - fst (update_cnode_cap_data w)) (to_bl g''))
                             (snd (update_cnode_cap_data w)))
    | ThreadCap r \<Rightarrow> ThreadCap r
    | DomainCap \<Rightarrow> DomainCap
    | UntypedCap d p n idx \<Rightarrow> UntypedCap d p n idx
    | NullCap \<Rightarrow> NullCap
    | ReplyCap t m rights \<Rightarrow> ReplyCap t m rights
    | IRQControlCap \<Rightarrow> IRQControlCap
    | IRQHandlerCap irq \<Rightarrow> IRQHandlerCap irq
    | Zombie r b n \<Rightarrow> Zombie r b n
    | ArchObjectCap cap \<Rightarrow> arch_update_cap_data pres w cap)" by (cases cap,
         simp_all only: cap.simps update_cap_data_def is_ep_cap.simps if_False if_True
                        is_ntfn_cap.simps is_cnode_cap.simps is_arch_cap_def word_size
                        cap_ep_badge.simps badge_update_def o_def cap_rights_update_def
                        simp_thms cap_rights.simps Let_def split_def
                        the_cnode_cap_def fst_conv snd_conv fun_app_def the_arch_cap_def
                  cong: if_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_cap_data pres w cap = (case cap of NullCap \<Rightarrow> NullCap | UntypedCap d p n idx \<Rightarrow> UntypedCap d p n idx | EndpointCap r badge rights \<Rightarrow> if badge = 0 \<and> \<not> pres then EndpointCap r (w && mask badge_bits) rights else NullCap | NotificationCap r badge rights \<Rightarrow> if badge = 0 \<and> \<not> pres then NotificationCap r (w && mask badge_bits) rights else NullCap | ReplyCap t m rights \<Rightarrow> ReplyCap t m rights | CNodeCap r bits guard \<Rightarrow> if word_bits < fst (update_cnode_cap_data w) + bits then NullCap else CNodeCap r bits (drop (size (snd (update_cnode_cap_data w)) - fst (update_cnode_cap_data w)) (to_bl (snd (update_cnode_cap_data w)))) | ThreadCap r \<Rightarrow> ThreadCap r | DomainCap \<Rightarrow> DomainCap | IRQControlCap \<Rightarrow> IRQControlCap | IRQHandlerCap irq \<Rightarrow> IRQHandlerCap irq | Zombie r b n \<Rightarrow> Zombie r b n | ArchObjectCap cap \<Rightarrow> arch_update_cap_data pres w cap)
theory Ipc_AI

lemma is_derived_mask [simp]:
  "is_derived m p (mask_cap R c) = is_derived m p c" by (simp add: mask_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived m p (mask_cap R c) = is_derived m p c
theory Ipc_AI

lemma get_mi_valid[wp]:
  "\<lbrace>valid_mdb\<rbrace> get_message_info a \<lbrace>\<lambda>rv s. valid_message_info rv\<rbrace>" apply (simp add: get_message_info_def) apply (wp | simp add: data_to_message_info_valid)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> get_message_info a \<lbrace>\<lambda>rv s. valid_message_info rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> do x <- as_user a (getRegister msg_info_register);
return (data_to_message_info x)
od \<lbrace>\<lambda>rv s. valid_message_info rv\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma get_extra_cptrs_inv[wp]:
  "\<lbrace>P\<rbrace> get_extra_cptrs buf mi \<lbrace>\<lambda>rv. P\<rbrace>" apply (cases buf, simp_all del: upt.simps) apply (wp mapM_wp' dmo_inv loadWord_inv
             | simp add: load_word_offs_def del: upt.simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_extra_cptrs buf mi \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>P\<rbrace> liftM (map data_to_cptr) (mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma mapM_length[wp]:
  "\<lbrace>\<lambda>s. P (length xs)\<rbrace> mapM f xs \<lbrace>\<lambda>rv s. P (length rv)\<rbrace>" by (induct xs arbitrary: P) (wpsimp simp: mapM_Cons mapM_def sequence_def|assumption)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (length xs)\<rbrace> mapM f xs \<lbrace>\<lambda>rv s. P (length rv)\<rbrace>
theory Ipc_AI

lemma cap_badge_rights_update[simp]:
  "cap_badge (cap_rights_update rights cap) = cap_badge cap" by (auto simp: cap_rights_update_def split: cap.split bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_badge (cap_rights_update rights cap) = cap_badge cap
theory Ipc_AI

lemma get_cap_cte_wp_at_rv:
  "\<lbrace>cte_wp_at (\<lambda>cap. P cap cap) p\<rbrace> get_cap p \<lbrace>\<lambda>rv. cte_wp_at (P rv) p\<rbrace>" 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>cte_wp_at (\<lambda>cap. P cap cap) p\<rbrace> get_cap p \<lbrace>\<lambda>rv. cte_wp_at (P rv) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at (\<lambda>cap. P cap cap) p s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) p s \<longrightarrow> cte_wp_at (P cap) p s proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma lsfco_cte_wp_at_univ:
  "\<lbrace>valid_objs and valid_cap croot and K (\<forall>cap rv. P cap rv)\<rbrace>
      lookup_slot_for_cnode_op f croot idx depth
   \<lbrace>\<lambda>rv. cte_wp_at (P rv) rv\<rbrace>, -" apply (rule hoare_gen_asmE) apply (rule hoare_post_imp_R) apply (rule lsfco_cte_at) apply (clarsimp simp: cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap croot and K (\<forall>cap rv. P cap rv)\<rbrace> lookup_slot_for_cnode_op f croot idx depth \<lbrace>\<lambda>rv. cte_wp_at (P rv) rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<forall>cap rv. P cap rv \<Longrightarrow> \<lbrace>valid_objs and valid_cap croot\<rbrace> lookup_slot_for_cnode_op f croot idx depth \<lbrace>\<lambda>rv. cte_wp_at (P rv) rv\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<forall>cap rv. P cap rv \<Longrightarrow> \<lbrace>valid_objs and valid_cap croot\<rbrace> lookup_slot_for_cnode_op f croot idx depth \<lbrace>?Q'2\<rbrace>, -
 2. \<And>rv s. \<lbrakk>\<forall>cap rv. P cap rv; ?Q'2 rv s\<rbrakk> \<Longrightarrow> cte_wp_at (P rv) rv s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>\<forall>cap rv. P cap rv; cte_wp_at (\<lambda>_. True) rv s\<rbrakk> \<Longrightarrow> cte_wp_at (P rv) rv s proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma bits_low_high_eq:
  assumes low: "x && mask bits = y && mask bits"
  and    high: "x >> bits = y >> bits"
  shows        "x = y" apply (rule word_eqI[rule_format]) apply (case_tac "n < bits") apply (cut_tac x=n in word_eqD[OF low]) apply (simp add: word_size) apply (cut_tac x="n - bits" in word_eqD[OF high]) apply (simp add: nth_shiftr) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = y proof (prove)
goal (1 subgoal):
 1. \<And>n. n < size x \<Longrightarrow> x !! n = y !! n proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>n < size x; n < bits\<rbrakk> \<Longrightarrow> x !! n = y !! n
 2. \<And>n. \<lbrakk>n < size x; \<not> n < bits\<rbrakk> \<Longrightarrow> x !! n = y !! n proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>n < size x; n < bits; (x && mask bits) !! n = (y && mask bits) !! n\<rbrakk> \<Longrightarrow> x !! n = y !! n
 2. \<And>n. \<lbrakk>n < size x; \<not> n < bits\<rbrakk> \<Longrightarrow> x !! n = y !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < size x; \<not> n < bits\<rbrakk> \<Longrightarrow> x !! n = y !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < size x; \<not> n < bits; (x >> bits) !! (n - bits) = (y >> bits) !! (n - bits)\<rbrakk> \<Longrightarrow> x !! n = y !! n proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma mask_cap_vs_cap_ref[simp]:
  "vs_cap_ref (mask_cap msk cap) = vs_cap_ref cap" by (simp add: mask_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_cap_ref (mask_cap msk cap) = vs_cap_ref cap
theory Ipc_AI

lemma set_extra_badge_typ_at[wp]:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>" by (simp add: set_extra_badge_def store_word_offs_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>
theory Ipc_AI

lemma impEM:
  "\<lbrakk>P \<longrightarrow> Q; P; \<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<longrightarrow> Q; P; \<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Ipc_AI

lemma cap_rights_update_NullCap[simp]:
  "(cap_rights_update rs cap = cap.NullCap) = (cap = cap.NullCap)" by (auto simp: cap_rights_update_def split: cap.split bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap_rights_update rs cap = NullCap) = (cap = NullCap)
theory Ipc_AI

lemma cap_insert_weak_cte_wp_at2:
  assumes imp: "\<And>c. P c \<Longrightarrow> \<not>is_untyped_cap c"
  shows
  "\<lbrace>\<lambda>s. if p = dest then P cap else cte_wp_at P p s\<rbrace>
   cap_insert cap src dest
   \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace>" unfolding cap_insert_def by (wp set_cap_cte_wp_at get_cap_wp hoare_weak_lift_imp
      | simp add: cap_insert_def
      | unfold set_untyped_cap_as_full_def
      | auto simp: cte_wp_at_def dest!:imp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if p = dest then P cap else cte_wp_at P p s\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if p = dest then P cap else cte_wp_at P p s\<rbrace> do src_cap <- get_cap src;
dest_original <- return $ is_cap_revocable cap src_cap;
old_cap <- get_cap dest;
assert (old_cap = NullCap);
set_untyped_cap_as_full src_cap cap src;
set_cap cap dest;
is_original <- gets is_original_cap;
src_parent <- return $ should_be_parent_of src_cap (is_original src) cap dest_original;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
update_cdt (\<lambda>cdt. cdt(dest := if src_parent then Some src else cdt src));
do_extended_op (cap_insert_ext src_parent src dest src_p dest_p);
set_original dest dest_original
od \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace>
theory Ipc_AI

lemma descendants_insert_update:
  "\<lbrakk>m dest = None; p \<in> descendants_of a m\<rbrakk>
   \<Longrightarrow> p \<in> descendants_of a (\<lambda>x. if x = dest then y else m x)" apply (clarsimp simp:descendants_of_empty descendants_of_def) apply (simp add:cdt_parent_rel_def) apply (erule trancl_mono) apply (clarsimp simp:is_cdt_parent_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m dest = None; p \<in> descendants_of a m\<rbrakk> \<Longrightarrow> p \<in> descendants_of a (\<lambda>x. if x = dest then y else m x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m dest = None; m \<Turnstile> a \<rightarrow> p\<rbrakk> \<Longrightarrow> (\<lambda>x. if x = dest then y else m x) \<Turnstile> a \<rightarrow> p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m dest = None; (a, p) \<in> {(p, c). is_cdt_parent m p c}\<^sup>+\<rbrakk> \<Longrightarrow> (a, p) \<in> {(p, c). is_cdt_parent (\<lambda>x. if x = dest then y else m x) p c}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. m dest = None \<Longrightarrow> {(p, c). is_cdt_parent m p c} \<subseteq> {(p, c). is_cdt_parent (\<lambda>x. if x = dest then y else m x) p c} proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma masked_as_full_null_cap[simp]:
  "(masked_as_full x x = cap.NullCap) = (x = cap.NullCap)"
  "(cap.NullCap  = masked_as_full x x) = (x = cap.NullCap)" by (case_tac x,simp_all add:masked_as_full_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (masked_as_full x x = NullCap) = (x = NullCap) &&& (NullCap = masked_as_full x x) = (x = NullCap)
theory Ipc_AI

lemma valid_remove_rights_If[simp]:
  "valid_cap cap s \<Longrightarrow> valid_cap (if P then remove_rights rs cap else cap) s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> cap \<Longrightarrow> s \<turnstile> (if P then remove_rights rs cap else cap)
theory Ipc_AI

lemma transfer_caps_loop_typ_at[wp]:
   "\<And>P T p ep buffer n caps slots mi.
      \<lbrace>\<lambda>s::'state_ext state. P (typ_at T p s)\<rbrace>
        transfer_caps_loop ep buffer n caps slots mi
      \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" by (wp transfer_caps_loop_pres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P T p ep buffer n caps slots mi. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>
theory Ipc_AI

lemma transfer_loop_aligned[wp]:
  "\<And>ep buffer n caps slots mi.
    \<lbrace>pspace_aligned :: 'state_ext state \<Rightarrow> bool\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
     \<lbrace>\<lambda>rv. pspace_aligned\<rbrace>" by (wp transfer_caps_loop_pres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ep buffer n caps slots mi. \<lbrace>pspace_aligned\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. pspace_aligned\<rbrace>
theory Ipc_AI

lemma transfer_loop_distinct[wp]:
  "\<And>ep buffer n caps slots mi.
    \<lbrace>pspace_distinct :: 'state_ext state \<Rightarrow> bool\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>rv. pspace_distinct\<rbrace>" by (wp transfer_caps_loop_pres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ep buffer n caps slots mi. \<lbrace>pspace_distinct\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. pspace_distinct\<rbrace>
theory Ipc_AI

lemma invs_valid_objs2:
  "\<And>s. invs s \<longrightarrow> valid_objs s" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<longrightarrow> valid_objs s
theory Ipc_AI

lemma tcl_state_refs_of[wp]:
  "\<And>P ep buffer n caps slots mi.
    \<lbrace>\<lambda>s::'state_ext state. P (state_refs_of s)\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>" by (wp transfer_caps_loop_pres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P ep buffer n caps slots mi. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>
theory Ipc_AI

lemma tcl_iflive[wp]:
  "\<And>ep buffer n caps slots mi.
    \<lbrace>if_live_then_nonz_cap :: 'state_ext state \<Rightarrow> bool\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>" by (wp transfer_caps_loop_pres cap_insert_iflive)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ep buffer n caps slots mi. \<lbrace>if_live_then_nonz_cap\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>
theory Ipc_AI

lemma tcl_ifunsafe[wp]:
  "\<And>slots ep buffer n caps mi.
    \<lbrace>\<lambda>s::'state_ext state. if_unsafe_then_cap s
                             \<and> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>" by (wp transfer_caps_loop_presM[where vo=False and em=False and ex=True, simplified]
            cap_insert_ifunsafe | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>slots ep buffer n caps mi. \<lbrace>\<lambda>s. if_unsafe_then_cap s \<and> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>
theory Ipc_AI

lemma get_cap_global_refs[wp]:
  "\<lbrace>valid_global_refs\<rbrace> get_cap p \<lbrace>\<lambda>c s. global_refs s \<inter> cap_range c = {}\<rbrace>" apply (rule hoare_pre) apply (rule get_cap_wp) apply (clarsimp simp: valid_refs_def2 valid_global_refs_def cte_wp_at_caps_of_state) by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs\<rbrace> get_cap p \<lbrace>\<lambda>c s. global_refs s \<inter> cap_range c = {}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_cap p \<lbrace>\<lambda>c s. global_refs s \<inter> cap_range c = {}\<rbrace>
 2. \<And>s. valid_global_refs s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_global_refs s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) p s \<longrightarrow> global_refs s \<inter> cap_range cap = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>\<forall>c\<in>ran (caps_of_state s). global_refs s \<inter> cap_range c = {}; caps_of_state s p = Some cap\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range cap = {}
theory Ipc_AI

lemma (in Ipc_AI) tcl_idle[wp]:
  "\<And>ep buffer n caps slots mi.
    \<lbrace>valid_idle::'state_ext state \<Rightarrow> bool\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>_. valid_idle\<rbrace>" by (wp transfer_caps_loop_pres cap_insert_idle valid_idle_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ep buffer n caps slots mi. \<lbrace>valid_idle\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>_. valid_idle\<rbrace>
theory Ipc_AI

lemma (in Ipc_AI) tcl_ct[wp]:
  "\<And>ep buffer n caps slots mi.
    \<lbrace>cur_tcb::'state_ext state \<Rightarrow> bool\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>rv. cur_tcb\<rbrace>" by (wp transfer_caps_loop_pres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ep buffer n caps slots mi. \<lbrace>cur_tcb\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cur_tcb\<rbrace>
theory Ipc_AI

lemma (in Ipc_AI) tcl_it[wp]:
  "\<And>P ep buffer n caps slots mi.
    \<lbrace>\<lambda>s::'state_ext state. P (idle_thread s)\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>rv s. P (idle_thread s)\<rbrace>" by (wp transfer_caps_loop_pres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P ep buffer n caps slots mi. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv s. P (idle_thread s)\<rbrace>
theory Ipc_AI

lemma set_extra_badge_zombies_final[wp]:
  "\<lbrace>zombies_final\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_. zombies_final\<rbrace>" apply (simp add: zombies_final_def cte_wp_at_caps_of_state is_final_cap'_def2) apply (wp hoare_vcg_all_lift final_cap_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> is_zombie cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>a b. \<forall>aa ba. (\<exists>capa. caps_of_state s (aa, ba) = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) = (aa = a \<and> ba = b)))\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_ s. \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> is_zombie cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>a b. \<forall>aa ba. (\<exists>capa. caps_of_state s (aa, ba) = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) = (aa = a \<and> ba = b)))\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma transfer_caps_loop_arch[wp]:
  "\<And>P ep buffer n caps slots mi.
    \<lbrace>\<lambda>s::'state_ext state. P (arch_state s)\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>rv s. P (arch_state s)\<rbrace>" by (rule transfer_caps_loop_pres) wp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P ep buffer n caps slots mi. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv s. P (arch_state s)\<rbrace>