theory Ipc_C

lemma transferCaps_local_slots:
  assumes weak: "\<And>c cap. P (maskedAsFull c cap) = P c"
  shows "\<lbrace> valid_objs' and (Not o real_cte_at' slot) and cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot \<rbrace>
    transferCaps tag caps ep receiver receiveBuffer
   \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace>" apply (simp add: transferCaps_def pred_conj_def) apply (rule hoare_seq_ext[rotated]) apply (rule hoare_vcg_conj_lift) apply (rule get_rs_real_cte_at') apply (rule get_recv_slot_inv') apply (rule hoare_pre) apply (wp transferCapsToSlots_local_slots weak | wpc)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCaps tag caps ep receiver receiveBuffer \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. valid_objs' x \<and> \<not> real_cte_at' slot x \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot x\<rbrace> do destSlots <- getReceiveSlots receiver receiveBuffer;
case receiveBuffer of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag)) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag))
od \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>x. valid_objs' x \<and> \<not> real_cte_at' slot x \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot x\<rbrace> getReceiveSlots receiver receiveBuffer \<lbrace>?B\<rbrace>
 2. \<And>destSlots. \<lbrace>?B destSlots\<rbrace> case receiveBuffer of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag)) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag)) \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>valid_objs'\<rbrace> getReceiveSlots receiver receiveBuffer \<lbrace>?Q3\<rbrace>
 2. \<lbrace>\<lambda>s. \<not> real_cte_at' slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s\<rbrace> getReceiveSlots receiver receiveBuffer \<lbrace>?Q'3\<rbrace>
 3. \<And>destSlots. \<lbrace>\<lambda>s. ?Q3 destSlots s \<and> ?Q'3 destSlots s\<rbrace> case receiveBuffer of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag)) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag)) \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<not> real_cte_at' slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s\<rbrace> getReceiveSlots receiver receiveBuffer \<lbrace>?Q'3\<rbrace>
 2. \<And>destSlots. \<lbrace>\<lambda>s. (\<forall>x\<in>set destSlots. real_cte_at' x s) \<and> ?Q'3 destSlots s\<rbrace> case receiveBuffer of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag)) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag)) \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>destSlots. \<lbrace>\<lambda>s. (\<forall>x\<in>set destSlots. real_cte_at' x s) \<and> \<not> real_cte_at' slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s\<rbrace> case receiveBuffer of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag)) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag)) \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>destSlots. \<lbrace>?Q8 destSlots\<rbrace> case receiveBuffer of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag)) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag)) \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace>
 2. \<And>destSlots s. (\<forall>x\<in>set destSlots. real_cte_at' x s) \<and> \<not> real_cte_at' slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s \<Longrightarrow> ?Q8 destSlots s proof (prove)
goal (1 subgoal):
 1. \<And>destSlots s. (\<forall>x\<in>set destSlots. real_cte_at' x s) \<and> \<not> real_cte_at' slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s \<Longrightarrow> (receiveBuffer = None \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s) \<and> (\<forall>x. receiveBuffer = Some x \<longrightarrow> (cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot and K (slot \<notin> set destSlots)) s) proof (prove)
goal:
No subgoals!