kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_AI

lemma transfer_caps_loop_aobj_at:
  "arch_obj_pred P' \<Longrightarrow>
  \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>r s::'state_ext state. P (obj_at P' pd s)\<rbrace>" apply (rule hoare_pre) apply (rule transfer_caps_loop_presM[where em=False and ex=False and vo=False, simplified, where P="\<lambda>s. P (obj_at P' pd s)"]) apply (wp cap_insert_aobj_at) apply (wpsimp simp: set_extra_badge_def) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. arch_obj_pred P' \<Longrightarrow> \<lbrace>?Q\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>
 2. \<And>s. \<lbrakk>arch_obj_pred P'; P (obj_at P' pd s)\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>cap src dest. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>
 2. \<And>b n. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_ s. P (obj_at P' pd s)\<rbrace>
 3. \<And>s. \<lbrakk>arch_obj_pred P'; P (obj_at P' pd s)\<rbrakk> \<Longrightarrow> P (obj_at P' pd s) proof (prove)
goal (2 subgoals):
 1. \<And>b n. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_ s. P (obj_at P' pd s)\<rbrace>
 2. \<And>s. \<lbrakk>arch_obj_pred P'; P (obj_at P' pd s)\<rbrakk> \<Longrightarrow> P (obj_at P' pd s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>arch_obj_pred P'; P (obj_at P' pd s)\<rbrakk> \<Longrightarrow> P (obj_at P' pd s) proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma transfer_caps_loop_valid_arch[wp]:
  "\<And>ep buffer n caps slots mi.
    \<lbrace>valid_arch_state::'state_ext state \<Rightarrow> bool\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>" by (rule valid_arch_state_lift_aobj_at; wp transfer_caps_loop_aobj_at)

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

lemma transfer_caps_loop_irq_node[wp]:
  "\<And>P ep buffer n caps slots mi.
    \<lbrace>\<lambda>s::'state_ext state. P (interrupt_irq_node s)\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>rv s. P (interrupt_irq_node 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 (interrupt_irq_node s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv s. P (interrupt_irq_node s)\<rbrace>
theory Ipc_AI

lemma cap_master_cap_irqs:
  "\<And>cap. cap_irqs cap = (case cap_master_cap cap
           of cap.IRQHandlerCap irq \<Rightarrow> {irq}
              | _ \<Rightarrow> {})" by (simp add: cap_master_cap_def split: cap.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>cap. cap_irqs cap = (case cap_master_cap cap of IRQHandlerCap irq \<Rightarrow> {irq} | _ \<Rightarrow> {})
theory Ipc_AI

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

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

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

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

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

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

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

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

lemma transfer_caps_loop_pspace_in_kernel_window[wp]:
  "\<And>ep buffer n caps slots mi.
    \<lbrace>pspace_in_kernel_window :: 'state_ext state \<Rightarrow> bool\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>rv. pspace_in_kernel_window\<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_in_kernel_window\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>
theory Ipc_AI

lemma transfer_caps_loop_valid_ioc[wp]:
  "\<And>ep buffer n caps slots mi.
    \<lbrace>\<lambda>s::'state_ext state. valid_ioc s\<rbrace>
     transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>_. valid_ioc\<rbrace>" by (wp transfer_caps_loop_pres | simp add: set_extra_badge_def)+

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

lemma set_extra_badge_vms[wp]:
  "\<And>buffer b n.
    \<lbrace>valid_machine_state::'state_ext state \<Rightarrow> bool\<rbrace>
      set_extra_badge buffer b n
    \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" by (simp add: set_extra_badge_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>buffer b n. \<lbrace>valid_machine_state\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_. valid_machine_state\<rbrace>
theory Ipc_AI

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

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

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

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

lemma transfer_caps_respects_device_region[wp]:
  "\<lbrace>\<lambda>s::'state_ext state. pspace_respects_device_region s\<rbrace>
    transfer_caps_loop ep buffer n caps slots mi
   \<lbrace>\<lambda>_. pspace_respects_device_region\<rbrace>" apply (wp transfer_caps_loop_pres) done

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

lemma transfer_caps_loop_invs[wp]:
  "\<And>slots.
    \<lbrace>\<lambda>s::'state_ext state. invs s
          \<and> (\<forall>x \<in> set slots. ex_cte_cap_wp_to is_cnode_cap x s) \<and> distinct slots
          \<and> (\<forall>x \<in> set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = cap.NullCap) x s)
          \<and> transfer_caps_srcs caps s\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>rv. invs\<rbrace>" unfolding invs_def valid_state_def valid_pspace_def by (wpsimp wp: valid_irq_node_typ transfer_caps_loop_valid_vspace_objs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>slots. \<lbrace>\<lambda>s. invs s \<and> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s) \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>slots. \<lbrace>\<lambda>s. (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s) \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace>
theory Ipc_AI

lemma zipWith_append2:
  "length ys + 1 < n \<Longrightarrow>
   zipWith f [0 ..< n] (ys @ [y]) = zipWith f [0 ..< n] ys @ [f (length ys) y]" apply (simp add: zipWith_def zip_append2) apply (subst upt_conv_Cons, erule Suc_lessD) apply simp apply (subst zip_take_triv[OF order_refl, symmetric], fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length ys + 1 < n \<Longrightarrow> zipWith f [0..<n] (ys @ [y]) = zipWith f [0..<n] ys @ [f (length ys) y] proof (prove)
goal (1 subgoal):
 1. Suc (length ys) < n \<Longrightarrow> map2 f [0..<length ys] ys = map2 f [0..<n] ys \<and> map2 f [length ys..<n] [y] = [f (length ys) y] proof (prove)
goal (1 subgoal):
 1. Suc (length ys) < n \<Longrightarrow> map2 f [0..<length ys] ys = map2 f [0..<n] ys \<and> map2 f (length ys # [Suc (length ys)..<n]) [y] = [f (length ys) y] proof (prove)
goal (1 subgoal):
 1. Suc (length ys) < n \<Longrightarrow> map2 f [0..<length ys] ys = map2 f [0..<n] ys proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma grs_distinct[wp]:
  "\<lbrace>\<top>\<rbrace> get_receive_slots t buf \<lbrace>\<lambda>rv s. distinct rv\<rbrace>" by (cases buf; wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_receive_slots t buf \<lbrace>\<lambda>rv s. distinct rv\<rbrace>
theory Ipc_AI

lemma transfer_caps_mi_label[wp]:
  "\<lbrace>\<lambda>s. P (mi_label mi)\<rbrace>
     transfer_caps mi caps ep receiver recv_buf
   \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace>" by (wpsimp simp: transfer_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> transfer_caps mi caps ep receiver recv_buf \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace>
theory Ipc_AI

lemma transfer_cap_typ_at[wp]:
  "\<And>P T p mi caps ep receiver recv_buf.
    \<lbrace>\<lambda>s::'state_ext state. P (typ_at T p s)\<rbrace>
      transfer_caps mi caps ep receiver recv_buf
    \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" by (wpsimp wp: cap_insert_typ_at hoare_drop_imps simp: transfer_caps_def)

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

lemma transfer_cap_tcb[wp]:
  "\<And>mi caps ep receiver recv_buf.
    \<lbrace>\<lambda>s::'state_ext state. tcb_at t s\<rbrace>
      transfer_caps mi caps ep receiver recv_buf
    \<lbrace>\<lambda>rv. tcb_at t\<rbrace>" by (simp add: tcb_at_typ, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>mi caps ep receiver recv_buf. \<lbrace>tcb_at t\<rbrace> transfer_caps mi caps ep receiver recv_buf \<lbrace>\<lambda>rv. tcb_at t\<rbrace>
theory Ipc_AI

lemma get_cap_cte_caps_to[wp]:
  "\<lbrace>\<lambda>s. \<forall>cp. P cp = P cp\<rbrace>
     get_cap sl
   \<lbrace>\<lambda>rv s. P rv \<longrightarrow> (\<forall>p\<in>cte_refs rv (interrupt_irq_node s). ex_cte_cap_wp_to P p s)\<rbrace>" apply (wp get_cap_wp) apply (clarsimp simp: ex_cte_cap_wp_to_def) apply (cases sl, fastforce elim!: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>cp. P cp = P cp\<rbrace> get_cap sl \<lbrace>\<lambda>rv s. P rv \<longrightarrow> (\<forall>p\<in>cte_refs rv (interrupt_irq_node s). ex_cte_cap_wp_to P p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>cp. P cp = P cp \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) sl s \<longrightarrow> P cap \<longrightarrow> (\<forall>p\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to P p s) proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b. \<lbrakk>cte_wp_at ((=) cap) sl s; P cap; (a, b) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> \<exists>aa ba. cte_wp_at (\<lambda>c. P c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma is_cnode_cap_mask[simp]:
  "is_cnode_cap (mask_cap rs cap) = is_cnode_cap cap" by (auto simp: mask_cap_def cap_rights_update_def
          split: cap.split bool.splits)

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

lemma get_rs_cap_to[wp]:
  "\<lbrace>\<top>\<rbrace> get_receive_slots rcvr buf
   \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. ex_cte_cap_wp_to is_cnode_cap x s\<rbrace> " apply (cases buf, simp_all add: split_def whenE_def split del: if_split) apply (wp | simp | rule hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_receive_slots rcvr buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. ex_cte_cap_wp_to is_cnode_cap x s\<rbrace> proof (prove)
goal (2 subgoals):
 1. buf = None \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return [] \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. ex_cte_cap_wp_to is_cnode_cap x s\<rbrace>
 2. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do ct <- load_cap_transfer a;
empty_on_failure (doE cnode <- unify_failure (lookup_cap rcvr (ct_receive_root ct));
slot <- unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct)));
cap <- liftE (get_cap slot);
y <- if cap \<noteq> NullCap then throwError () else returnOk ();
returnOk [slot]
odE)
od \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. ex_cte_cap_wp_to is_cnode_cap x s\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma derive_cap_notzombie[wp]:
  "\<lbrace>\<top>\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. \<not> is_zombie rv\<rbrace>,-" apply (cases cap; clarsimp simp: derive_cap_def) by (wpsimp wp: arch_derive_cap_notzombie simp: is_zombie_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. \<not> is_zombie rv\<rbrace>, - proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> returnOk NullCap \<lbrace>\<lambda>rv s. \<not> is_zombie rv\<rbrace>, -
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doE y <- ensure_no_children slot;
returnOk (UntypedCap x21 x22 x23 x24)
odE \<lbrace>\<lambda>rv s. \<not> is_zombie rv\<rbrace>, -
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> returnOk (EndpointCap x31 x32 x33) \<lbrace>\<lambda>rv s. \<not> is_zombie rv\<rbrace>, -
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> returnOk (NotificationCap x41 x42 x43) \<lbrace>\<lambda>rv s. \<not> is_zombie rv\<rbrace>, -
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> returnOk NullCap \<lbrace>\<lambda>rv s. \<not> is_zombie rv\<rbrace>, -
 6. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> returnOk (CNodeCap x61 x62 x63) \<lbrace>\<lambda>rv s. \<not> is_zombie rv\<rbrace>, -
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> returnOk (ThreadCap x7) \<lbrace>\<lambda>rv s. \<not> is_zombie rv\<rbrace>, -
 8. cap = DomainCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> returnOk DomainCap \<lbrace>\<lambda>rv s. \<not> is_zombie rv\<rbrace>, -
 9. cap = IRQControlCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> returnOk NullCap \<lbrace>\<lambda>rv s. \<not> is_zombie rv\<rbrace>, -
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> returnOk (IRQHandlerCap x10) \<lbrace>\<lambda>rv s. \<not> is_zombie rv\<rbrace>, -
A total of 12 subgoals...
theory Ipc_AI

lemma derive_cap_notIRQ[wp]:
  "\<lbrace>\<top>\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. rv \<noteq> cap.IRQControlCap\<rbrace>,-" by (cases cap; wpsimp wp: arch_derive_cap_notIRQ simp: derive_cap_def o_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. rv \<noteq> IRQControlCap\<rbrace>, -
theory Ipc_AI

lemma random_helper[simp]:
  "\<And>ct_send_data ct ms cap.
    is_zombie (case ct_send_data ct of None \<Rightarrow> mask_cap ms cap
                 | Some w \<Rightarrow> update_cap_data P w (mask_cap ms cap))
      = is_zombie cap" by (simp split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ct_send_data ct ms cap. is_zombie (case ct_send_data ct of None \<Rightarrow> mask_cap ms cap | Some w \<Rightarrow> update_cap_data P w (mask_cap ms cap)) = is_zombie cap
theory Ipc_AI

lemma zombies_final_pres:
  assumes x: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
      and y: "\<And>P p. \<lbrace>cte_wp_at P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace>"
  shows      "\<lbrace>zombies_final\<rbrace> f \<lbrace>\<lambda>rv. zombies_final\<rbrace>" apply (simp only: zombies_final_def final_cap_at_eq
                    imp_conv_disj cte_wp_at_neg2[where P=is_zombie]
                    de_Morgan_conj) apply (intro hoare_vcg_disj_lift hoare_vcg_ex_lift hoare_vcg_conj_lift
               y hoare_vcg_all_lift valid_cte_at_neg_typ x) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> f \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. (\<not> cte_wp_at (\<lambda>_. True) p s \<or> cte_wp_at (\<lambda>cap. \<not> is_zombie cap) p s) \<or> (\<exists>cp. cte_wp_at (\<lambda>cap. cap = cp) p s \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<not> cte_wp_at (\<lambda>_. True) p' s \<or> \<not> p' \<noteq> p) \<or> cte_wp_at (\<lambda>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {}) p' s))\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>p. (\<not> cte_wp_at (\<lambda>_. True) p s \<or> cte_wp_at (\<lambda>cap. \<not> is_zombie cap) p s) \<or> (\<exists>cp. cte_wp_at (\<lambda>cap. cap = cp) p s \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<not> cte_wp_at (\<lambda>_. True) p' s \<or> \<not> p' \<noteq> p) \<or> cte_wp_at (\<lambda>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {}) p' s))\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma cte_wp_at_orth:
  "\<lbrakk> cte_wp_at (\<lambda>c. P c) p s; cte_wp_at (\<lambda>c. \<not> P c) p s \<rbrakk> \<Longrightarrow> False" unfolding cte_wp_at_def by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P p s; cte_wp_at (\<lambda>c. \<not> P c) p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>cap. fst (get_cap p s) = {(cap, s)} \<and> P cap; \<exists>cap. fst (get_cap p s) = {(cap, s)} \<and> \<not> P cap\<rbrakk> \<Longrightarrow> False
theory Ipc_AI

lemma no_irq_case_option:
  "\<lbrakk> no_irq f; \<And>x. no_irq (g x) \<rbrakk> \<Longrightarrow> no_irq (case_option f g x)" apply (subst no_irq_def) apply clarsimp apply (rule hoare_pre, wpsimp wp: no_irq) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_irq f; \<And>x. no_irq (g x)\<rbrakk> \<Longrightarrow> no_irq (case x of None \<Rightarrow> f | Some x \<Rightarrow> g x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_irq f; \<And>x. no_irq (g x)\<rbrakk> \<Longrightarrow> \<forall>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> case x of None \<Rightarrow> f | Some x \<Rightarrow> g x \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>no_irq f; \<And>x. no_irq (g x)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> case x of None \<Rightarrow> f | Some x \<Rightarrow> g x \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P s. \<lbrakk>no_irq f; \<And>x. no_irq (g x); P (irq_masks s)\<rbrakk> \<Longrightarrow> P (irq_masks s) proof (prove)
goal:
No subgoals!