theory Ipc_R

lemma get_rs_cte_at'[wp]:
  "\<lbrace>\<top>\<rbrace>
   getReceiveSlots receiver recv_buf
   \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s\<rbrace>" apply (cases recv_buf) apply (simp add: getReceiveSlots_def) apply (wp,simp) apply (clarsimp simp add: getReceiveSlots_def
                            split_def whenE_def unlessE_whenE) apply wp apply simp apply (rule getCTE_wp) apply (simp add: cte_wp_at_ctes_of cong: conj_cong) apply wp+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getReceiveSlots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s\<rbrace> proof (prove)
goal (2 subgoals):
 1. recv_buf = None \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> getReceiveSlots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s\<rbrace>
 2. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> getReceiveSlots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s\<rbrace> proof (prove)
goal (2 subgoals):
 1. recv_buf = None \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return [] \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s\<rbrace>
 2. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> getReceiveSlots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> getReceiveSlots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do ct <- loadCapTransfer a;
emptyOnFailure (doE cnode <- unifyFailure (lookupCap receiver (ctReceiveRoot ct));
slot <- unifyFailure (lookupSlotForCNodeOp False cnode (ctReceiveIndex ct) (ctReceiveDepth ct));
cte <- liftE (getCTE slot);
y <- if cteCap cte \<noteq> capability.NullCap then throwError () else returnOk ();
returnOk [slot]
odE)
od \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>a ct cnode slot. recv_buf = Some a \<Longrightarrow> \<lbrace>?B12 a ct cnode slot\<rbrace> getCTE slot \<lbrace>\<lambda>cte s. (cteCap cte \<noteq> capability.NullCap \<longrightarrow> (\<forall>x\<in>set []. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s) \<and> True) \<and> (\<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> (\<forall>x\<in>set [slot]. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s))\<rbrace>
 2. \<And>a ct cnode. recv_buf = Some a \<Longrightarrow> \<lbrace>?B11 a ct cnode\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnode (ctReceiveIndex ct) (ctReceiveDepth ct)) \<lbrace>?B12 a ct cnode\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x\<in>set []. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s\<rbrace>
 3. \<And>a ct. recv_buf = Some a \<Longrightarrow> \<lbrace>?B9 a ct\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot ct)) \<lbrace>?B11 a ct\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x\<in>set []. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s\<rbrace>
 4. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q8 a\<rbrace> loadCapTransfer a \<lbrace>?B9 a\<rbrace>
 5. \<And>a s. \<lbrakk>recv_buf = Some a; True\<rbrakk> \<Longrightarrow> ?Q8 a s proof (prove)
goal (5 subgoals):
 1. \<And>a ct cnode slot. recv_buf = Some a \<Longrightarrow> \<lbrace>?B12 a ct cnode slot\<rbrace> getCTE slot \<lbrace>\<lambda>cte s. cteCap cte = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s\<rbrace>
 2. \<And>a ct cnode. recv_buf = Some a \<Longrightarrow> \<lbrace>?B11 a ct cnode\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnode (ctReceiveIndex ct) (ctReceiveDepth ct)) \<lbrace>?B12 a ct cnode\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x\<in>set []. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s\<rbrace>
 3. \<And>a ct. recv_buf = Some a \<Longrightarrow> \<lbrace>?B9 a ct\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot ct)) \<lbrace>?B11 a ct\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x\<in>set []. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s\<rbrace>
 4. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q8 a\<rbrace> loadCapTransfer a \<lbrace>?B9 a\<rbrace>
 5. \<And>a s. \<lbrakk>recv_buf = Some a; True\<rbrakk> \<Longrightarrow> ?Q8 a s proof (prove)
goal (4 subgoals):
 1. \<And>a ct cnode. recv_buf = Some a \<Longrightarrow> \<lbrace>?B11 a ct cnode\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnode (ctReceiveIndex ct) (ctReceiveDepth ct)) \<lbrace>\<lambda>slot s. cte_wp_at' (\<lambda>_. True) slot s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) slot s \<and> (cteCap cte = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s))\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x\<in>set []. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s\<rbrace>
 2. \<And>a ct. recv_buf = Some a \<Longrightarrow> \<lbrace>?B9 a ct\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot ct)) \<lbrace>?B11 a ct\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x\<in>set []. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s\<rbrace>
 3. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q8 a\<rbrace> loadCapTransfer a \<lbrace>?B9 a\<rbrace>
 4. \<And>a s. \<lbrakk>recv_buf = Some a; True\<rbrakk> \<Longrightarrow> ?Q8 a s proof (prove)
goal (4 subgoals):
 1. \<And>a ct cnode. recv_buf = Some a \<Longrightarrow> \<lbrace>?B11 a ct cnode\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnode (ctReceiveIndex ct) (ctReceiveDepth ct)) \<lbrace>\<lambda>slot s. True\<rbrace>, \<lbrace>\<lambda>rv s. True\<rbrace>
 2. \<And>a ct. recv_buf = Some a \<Longrightarrow> \<lbrace>?B9 a ct\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot ct)) \<lbrace>?B11 a ct\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x\<in>set []. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s\<rbrace>
 3. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q8 a\<rbrace> loadCapTransfer a \<lbrace>?B9 a\<rbrace>
 4. \<And>a s. \<lbrakk>recv_buf = Some a; True\<rbrakk> \<Longrightarrow> ?Q8 a s proof (prove)
goal (1 subgoal):
 1. \<And>a s. \<lbrakk>recv_buf = Some a; True\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set []. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s) \<and> True \<and> True proof (prove)
goal:
No subgoals!