kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchFinalise_AI

lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_asms]:
  "\<lbrace>st_tcb_at P t and K (\<forall>st. simple st \<longrightarrow> P st)\<rbrace>
     deleting_irq_handler irq
   \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>" apply (simp add: deleting_irq_handler_def) apply (wp cap_delete_one_st_tcb_at) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t and K (\<forall>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st \<longrightarrow> P st)\<rbrace> deleting_irq_handler irq \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t and (\<lambda>y. \<forall>st. (inactive st \<longrightarrow> P Inactive) \<and> (st = Running \<longrightarrow> P Running) \<and> (st = Restart \<longrightarrow> P Restart) \<and> (idle st \<longrightarrow> P IdleThreadState) \<and> (awaiting_reply st \<longrightarrow> P BlockedOnReply))\<rbrace> get_irq_slot irq >>= cap_delete_one \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (st_tcb_at P t and (\<lambda>y. \<forall>st. (inactive st \<longrightarrow> P Inactive) \<and> (st = Running \<longrightarrow> P Running) \<and> (st = Restart \<longrightarrow> P Restart) \<and> (idle st \<longrightarrow> P IdleThreadState) \<and> (awaiting_reply st \<longrightarrow> P BlockedOnReply))) s \<Longrightarrow> (st_tcb_at P t and K (\<forall>st. active st \<longrightarrow> P st)) s proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma irq_node_global_refs_ARCH [Finalise_AI_asms]:
  "interrupt_irq_node s irq \<in> global_refs s" by (simp add: global_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. interrupt_irq_node s irq \<in> global_refs s
theory ArchFinalise_AI

lemma (* replaceable_or_arch_update_same *) [Finalise_AI_asms]:
  "replaceable_or_arch_update s slot cap cap" by (clarsimp simp: replaceable_or_arch_update_def
                replaceable_def is_arch_update_def is_cap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. replaceable_or_arch_update s slot cap cap
theory ArchFinalise_AI

lemma typ_at_data_at_wp:
  assumes typ_wp: "\<And>a.\<lbrace>typ_at a p \<rbrace> g \<lbrace>\<lambda>s. typ_at a p\<rbrace>"
  shows "\<lbrace>data_at b p\<rbrace> g \<lbrace>\<lambda>s. data_at b p\<rbrace>" apply (simp add: data_at_def) apply (wp typ_wp hoare_vcg_disj_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>data_at b p\<rbrace> g \<lbrace>\<lambda>s. data_at b p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. typ_at (AArch (AUserData b)) p s \<or> typ_at (AArch (ADeviceData b)) p s\<rbrace> g \<lbrace>\<lambda>s sa. typ_at (AArch (AUserData b)) p sa \<or> typ_at (AArch (ADeviceData b)) p sa\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma set_asid_pool_obj_at_ptr:
  "\<lbrace>\<lambda>s. P (ArchObj (arch_kernel_obj.ASIDPool mp))\<rbrace>
     set_asid_pool ptr mp
   \<lbrace>\<lambda>rv s. obj_at P ptr s\<rbrace>" apply (simp add: set_asid_pool_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ArchObj (ASIDPool mp))\<rbrace> set_asid_pool ptr mp \<lbrace>\<lambda>rv. obj_at P ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ArchObj (ASIDPool mp))\<rbrace> do kobj <- get_object ptr;
y <- assert (a_type kobj = a_type (ArchObj (ASIDPool mp)));
s <- get;
put (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (ASIDPool mp))\<rparr>)
od \<lbrace>\<lambda>rv. obj_at P ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ArchObj (ASIDPool mp)) \<Longrightarrow> \<forall>ko. ko_at ko ptr s \<longrightarrow> a_type ko = a_type (ArchObj (ASIDPool mp)) \<longrightarrow> obj_at P ptr (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (ASIDPool mp))\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma valid_arch_state_table_strg:
  "valid_arch_state s \<and> asid_pool_at p s \<and>
   Some p \<notin> arm_asid_table (arch_state s) ` (dom (arm_asid_table (arch_state s)) - {x}) \<longrightarrow>
   valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (arm_asid_table (arch_state s))(x \<mapsto> p)\<rparr>\<rparr>)" apply (clarsimp simp: valid_arch_state_def valid_asid_table_def ran_def) apply (rule conjI, fastforce) apply (erule inj_on_fun_upd_strongerI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_state s \<and> typ_at (AArch AASIDPool) p s \<and> Some p \<notin> asid_table s ` (dom (asid_table s) - {x}) \<longrightarrow> valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); typ_at (AArch AASIDPool) p s; Some p \<notin> asid_table s ` (dom (asid_table s) - {x})\<rbrakk> \<Longrightarrow> (\<forall>pa. (\<exists>a. (a = x \<longrightarrow> p = pa) \<and> (a \<noteq> x \<longrightarrow> asid_table s a = Some pa)) \<longrightarrow> typ_at (AArch AASIDPool) pa s) \<and> inj_on ((asid_table s)(x \<mapsto> p)) (dom (asid_table s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); typ_at (AArch AASIDPool) p s; Some p \<notin> asid_table s ` (dom (asid_table s) - {x})\<rbrakk> \<Longrightarrow> inj_on ((asid_table s)(x \<mapsto> p)) (dom (asid_table s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); typ_at (AArch AASIDPool) p s; Some p \<notin> asid_table s ` (dom (asid_table s) - {x})\<rbrakk> \<Longrightarrow> Some p \<notin> asid_table s ` (dom (asid_table s) - {x}) proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma valid_table_caps_table [simp]:
  "valid_table_caps (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table'\<rparr>\<rparr>) = valid_table_caps s" by (simp add: valid_table_caps_def second_level_tables_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_table_caps (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table'\<rparr>\<rparr>) = valid_table_caps s
theory ArchFinalise_AI

lemma valid_global_objs_table [simp]:
  "valid_global_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table'\<rparr>\<rparr>) = valid_global_objs s" by (simp add: valid_global_objs_def second_level_tables_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table'\<rparr>\<rparr>) = valid_global_objs s
theory ArchFinalise_AI

lemma valid_kernel_mappings [iff]:
  "valid_kernel_mappings (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table'\<rparr>\<rparr>) = valid_kernel_mappings s" by (simp add: valid_kernel_mappings_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_kernel_mappings (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table'\<rparr>\<rparr>) = valid_kernel_mappings s
theory ArchFinalise_AI

lemma vs_asid_refs_updateD:
  "(ref', p') \<in> vs_asid_refs (table (x \<mapsto> p))
  \<Longrightarrow> (ref',p') \<in> vs_asid_refs table \<or> (ref' = [VSRef (ucast x) None] \<and> p' = p)" apply (clarsimp simp: vs_asid_refs_def graph_of_def split: if_split_asm) apply (rule_tac x="(a,p')" in image_eqI) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ref', p') \<in> vs_asid_refs (table(x \<mapsto> p)) \<Longrightarrow> (ref', p') \<in> vs_asid_refs table \<or> ref' = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> p' = p proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>ref' = [VSRef (UCAST(7 \<rightarrow> 32) a) None]; UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) x \<longrightarrow> p' \<noteq> p; a \<noteq> x; table a = Some p'\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) a) None], p') \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], x)) ` {(x, y). table x = Some y} proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>ref' = [VSRef (UCAST(7 \<rightarrow> 32) a) None]; UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) x \<longrightarrow> p' \<noteq> p; a \<noteq> x; table a = Some p'\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) a) None], p') = (case (a, p') of (r, x) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], x))
 2. \<And>a. \<lbrakk>ref' = [VSRef (UCAST(7 \<rightarrow> 32) a) None]; UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) x \<longrightarrow> p' \<noteq> p; a \<noteq> x; table a = Some p'\<rbrakk> \<Longrightarrow> (a, p') \<in> {(x, y). table x = Some y} proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma vs_lookup1_arch [simp]:
  "vs_lookup1 (arch_state_update f s) = vs_lookup1 s" by (simp add: vs_lookup1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup1 (arch_state_update f s) = vs_lookup1 s
theory ArchFinalise_AI

lemma page_table_pte_atE:
  "\<lbrakk> page_table_at p s; x < 2 ^ pt_bits;
             (x >> 2) << 2 = x; pspace_aligned s \<rbrakk>
       \<Longrightarrow> pte_at (p + x) s" apply (drule page_table_pte_atI[where x="x >> 2"], simp_all) apply (subst mask_eq_iff_w2p[symmetric]) apply (simp add: pt_bits_def pageBits_def word_size) apply (rule word_eqI) apply (simp add: nth_shiftr word_size) apply (drule_tac x="Suc (Suc n)" in word_eqD [OF less_mask_eq]) apply (simp add: word_size) apply arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageTable) p s; x < 2 ^ pt_bits; x >> 2 << 2 = x; pspace_aligned s\<rbrakk> \<Longrightarrow> pte_at (p + x) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ pt_bits; x >> 2 << 2 = x; pspace_aligned s\<rbrakk> \<Longrightarrow> x >> 2 < 2 ^ (pt_bits - 2) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < 2 ^ pt_bits; x >> 2 << 2 = x; pspace_aligned s\<rbrakk> \<Longrightarrow> pt_bits - 2 < size (x >> 2)
 2. \<lbrakk>x < 2 ^ pt_bits; x >> 2 << 2 = x; pspace_aligned s\<rbrakk> \<Longrightarrow> (x >> 2) && mask (pt_bits - 2) = x >> 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ pt_bits; x >> 2 << 2 = x; pspace_aligned s\<rbrakk> \<Longrightarrow> (x >> 2) && mask (pt_bits - 2) = x >> 2 proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x < 2 ^ pt_bits; x >> 2 << 2 = x; pspace_aligned s\<rbrakk> \<Longrightarrow> n < size ((x >> 2) && mask (pt_bits - 2)) \<longrightarrow> ((x >> 2) && mask (pt_bits - 2)) !! n = (x >> 2) !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x < 2 ^ pt_bits; x >> 2 << 2 = x; pspace_aligned s\<rbrakk> \<Longrightarrow> n < 32 \<longrightarrow> (x !! Suc (Suc n) \<and> n < pt_bits - 2) = x !! Suc (Suc n) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x >> 2 << 2 = x; pspace_aligned s; (x && mask pt_bits) !! Suc (Suc n) = x !! Suc (Suc n)\<rbrakk> \<Longrightarrow> n < 32 \<longrightarrow> (x !! Suc (Suc n) \<and> n < pt_bits - 2) = x !! Suc (Suc n) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x >> 2 << 2 = x; pspace_aligned s; (x !! Suc (Suc n) \<and> n < 30 \<and> Suc (Suc n) < pt_bits) = x !! Suc (Suc n)\<rbrakk> \<Longrightarrow> n < 32 \<longrightarrow> (x !! Suc (Suc n) \<and> n < pt_bits - 2) = x !! Suc (Suc n) proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma (* zombie_cap_two_nonidles *)[Finalise_AI_asms]:
  "\<lbrakk> caps_of_state s ptr = Some (Zombie ptr' zbits n); invs s \<rbrakk>
       \<Longrightarrow> fst ptr \<noteq> idle_thread s \<and> ptr' \<noteq> idle_thread s" apply (frule valid_global_refsD2, clarsimp+) apply (simp add: cap_range_def global_refs_def) apply (cases ptr, auto dest: valid_idle_has_null_cap_ARCH[rotated -1])[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s ptr = Some (Zombie ptr' zbits n); invs s\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s \<and> ptr' \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s ptr = Some (Zombie ptr' zbits n); invs s; global_refs s \<inter> cap_range (Zombie ptr' zbits n) = {}\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s \<and> ptr' \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s ptr = Some (Zombie ptr' zbits n); invs s; ptr' \<noteq> idle_thread s \<and> ptr' \<noteq> arm_global_pd (arch_state s) \<and> ptr' \<notin> range (interrupt_irq_node s) \<and> ptr' \<notin> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma arch_derive_cap_notzombie[wp]:
  "\<lbrace>\<top>\<rbrace> arch_derive_cap acap \<lbrace>\<lambda>rv s. \<not> is_zombie rv\<rbrace>, -" by (cases acap; wpsimp simp: arch_derive_cap_def is_zombie_def o_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> arch_derive_cap acap \<lbrace>\<lambda>rv s. \<not> is_zombie rv\<rbrace>, -
theory ArchFinalise_AI

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

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

lemma logic_to_conj_thm_workers:
  "A = (A' \<and> A'') \<Longrightarrow> B = (B' \<and> B'')
    \<Longrightarrow> (A \<and> B) = ((A' \<and> B') \<and> (A'' \<and> B''))"
  "B = (B' \<and> B'')
    \<Longrightarrow> (A \<or> B) = ((A \<or> B') \<and> (A \<or> B''))"
  "\<lbrakk> \<And>x. P x = (P' x \<and> P'' x) \<rbrakk>
    \<Longrightarrow> (\<forall>x. P x) = ((\<forall>x. P' x) \<and> (\<forall>x. P'' x))"
  "\<lbrakk> \<And>x. P x = (P' x \<and> P'' x) \<rbrakk>
    \<Longrightarrow> (\<forall>x \<in> S. P x) = ((\<forall>x \<in> S. P' x) \<and> (\<forall>x \<in> S. P'' x))"
  "B = (B' \<and> B'')
    \<Longrightarrow> (A \<longrightarrow> B) = ((A \<longrightarrow> B') \<and> (A \<longrightarrow> B''))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>A = (A' \<and> A''); B = (B' \<and> B'')\<rbrakk> \<Longrightarrow> (A \<and> B) = ((A' \<and> B') \<and> A'' \<and> B'')) &&& (B = (B' \<and> B'') \<Longrightarrow> (A \<or> B) = ((A \<or> B') \<and> (A \<or> B'')))) &&& ((\<And>x. P x = (P' x \<and> P'' x)) \<Longrightarrow> (\<forall>x. P x) = ((\<forall>x. P' x) \<and> (\<forall>x. P'' x))) &&& ((\<And>x. P x = (P' x \<and> P'' x)) \<Longrightarrow> (\<forall>x\<in>S. P x) = ((\<forall>x\<in>S. P' x) \<and> (\<forall>x\<in>S. P'' x))) &&& (B = (B' \<and> B'') \<Longrightarrow> (A \<longrightarrow> B) = ((A \<longrightarrow> B') \<and> (A \<longrightarrow> B'')))
theory WPBang

lemma conj_meta_forward:
  "P \<and> Q \<Longrightarrow> (P \<Longrightarrow> P') \<Longrightarrow> (Q \<Longrightarrow> Q') \<Longrightarrow> P' \<and> Q'" by simp

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

lemma get_mi_inv[wp]: "\<lbrace>I\<rbrace> get_message_info a \<lbrace>\<lambda>x. I\<rbrace>" by (simp add: get_message_info_def user_getreg_inv | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> get_message_info a \<lbrace>\<lambda>x. I\<rbrace>
theory Ipc_AI

lemma lsfco_cte_at:
  "\<lbrace>valid_objs and valid_cap cn\<rbrace>
  lookup_slot_for_cnode_op f cn idx depth
  \<lbrace>\<lambda>rv. cte_at rv\<rbrace>,-" by (rule hoare_post_imp_R, rule lookup_cnode_slot_real_cte, simp add: real_cte_at_cte)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap cn\<rbrace> lookup_slot_for_cnode_op f cn idx depth \<lbrace>cte_wp_at (\<lambda>_. True)\<rbrace>, -
theory Ipc_AI

lemma load_ct_inv[wp]:
  "\<lbrace>P\<rbrace> load_cap_transfer buf \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: load_cap_transfer_def) apply (wp dmo_inv mapM_wp' loadWord_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> load_cap_transfer buf \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> captransfer_from_words (buf + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma get_recv_slot_inv[wp]:
  "\<lbrace> P \<rbrace> get_receive_slots receiver buf \<lbrace>\<lambda>rv. P \<rbrace>" apply (case_tac buf) apply simp apply (simp add: split_def whenE_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_receive_slots receiver buf \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. buf = None \<Longrightarrow> \<lbrace>P\<rbrace> get_receive_slots receiver buf \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>P\<rbrace> get_receive_slots receiver buf \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>P\<rbrace> get_receive_slots receiver buf \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>P\<rbrace> do ct <- load_cap_transfer a;
empty_on_failure (doE cnode <- unify_failure (lookup_cap receiver (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. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma cte_wp_at_eq_simp:
  "cte_wp_at ((=) cap) = cte_wp_at (\<lambda>c. c = cap)" apply (rule arg_cong [where f=cte_wp_at]) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at ((=) cap) = cte_wp_at (\<lambda>c. c = cap) proof (prove)
goal (1 subgoal):
 1. (=) cap = (\<lambda>c. c = cap) proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma get_rs_cte_at[wp]:
  "\<lbrace>\<top>\<rbrace>
  get_receive_slots receiver recv_buf
  \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. cte_wp_at (\<lambda>c. c = cap.NullCap) x s\<rbrace>" apply (cases recv_buf) apply (simp,wp,simp) apply (clarsimp simp add: split_def whenE_def) apply (wp | simp add: cte_wp_at_eq_simp | rule get_cap_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>c. c = NullCap) x s\<rbrace> proof (prove)
goal (2 subgoals):
 1. recv_buf = None \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>c. c = NullCap) x s\<rbrace>
 2. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>c. c = NullCap) x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>c. c = NullCap) x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do ct <- load_cap_transfer a;
empty_on_failure (doE cnode <- unify_failure (lookup_cap receiver (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. cte_wp_at (\<lambda>c. c = NullCap) x s\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma get_rs_cte_at2[wp]:
  "\<lbrace>\<top>\<rbrace>
  get_receive_slots receiver recv_buf
  \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. cte_wp_at ((=) cap.NullCap) x s\<rbrace>" apply (rule hoare_strengthen_post, rule get_rs_cte_at) apply (clarsimp simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>c. c = NullCap) x s \<Longrightarrow> \<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma get_rs_real_cte_at[wp]:
  "\<lbrace>valid_objs\<rbrace>
   get_receive_slots receiver recv_buf
   \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. real_cte_at x s\<rbrace>" apply (cases recv_buf) apply (simp,wp,simp) apply (clarsimp simp add: split_def whenE_def) apply (wp hoare_drop_imps lookup_cnode_slot_real_cte lookup_cap_valid | simp | rule get_cap_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. real_cte_at x s\<rbrace> proof (prove)
goal (2 subgoals):
 1. recv_buf = None \<Longrightarrow> \<lbrace>valid_objs\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. real_cte_at x s\<rbrace>
 2. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>valid_objs\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. real_cte_at x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>valid_objs\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. real_cte_at x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>valid_objs\<rbrace> do ct <- load_cap_transfer a;
empty_on_failure (doE cnode <- unify_failure (lookup_cap receiver (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. real_cte_at x s\<rbrace> proof (prove)
goal:
No subgoals!