theory Ipc_R

lemma get_rs_real_cte_at'[wp]:
  "\<lbrace>valid_objs'\<rbrace>
   getReceiveSlots receiver recv_buf
   \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. real_cte_at' 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 (wp hoare_drop_imps)[1] apply simp apply (wp lookup_cap_valid')+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> getReceiveSlots 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> getReceiveSlots 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> getReceiveSlots 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> return [] \<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> getReceiveSlots 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> getReceiveSlots 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 <- 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. real_cte_at' 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 []. real_cte_at' x s) \<and> True) \<and> (\<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> (\<forall>x\<in>set [slot]. real_cte_at' 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 []. real_cte_at' 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 []. real_cte_at' 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; valid_objs' s\<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> real_cte_at' 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 []. real_cte_at' 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 []. real_cte_at' 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; valid_objs' s\<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>real_cte_at'\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x\<in>set []. real_cte_at' 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 []. real_cte_at' 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; valid_objs' s\<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>real_cte_at'\<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 []. real_cte_at' 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; valid_objs' s\<rbrakk> \<Longrightarrow> ?Q8 a s proof (prove)
goal (1 subgoal):
 1. \<And>a s. \<lbrakk>recv_buf = Some a; valid_objs' s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set []. real_cte_at' x s) \<and> True \<and> True \<and> True \<and> valid_objs' s \<and> valid_objs' s proof (prove)
goal:
No subgoals!