theory Ipc_R

lemma lsfco_cte_at':
  "\<lbrace>valid_objs' and valid_cap' cap\<rbrace>
  lookupSlotForCNodeOp f cap idx depth
  \<lbrace>\<lambda>rv. cte_at' rv\<rbrace>, -" apply (simp add: lookupSlotForCNodeOp_def) apply (rule conjI) prefer 2 apply clarsimp apply (wp) apply (clarsimp simp: split_def unlessE_def
             split del: if_split) apply (wp hoare_drop_imps throwE_R) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> lookupSlotForCNodeOp f cap idx depth \<lbrace>cte_wp_at' (\<lambda>_. True)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. (isCNodeCap cap \<longrightarrow> \<lbrace>valid_objs' and valid_cap' cap\<rbrace> doE y <- rangeCheck depth (Suc 0) (size idx);
lookupErrorOnFailure f (doE (slot, bitsLeft) <- CSpace_H.resolveAddressBits cap idx depth;
if bitsLeft = 0 then returnOk slot else throwError (Fault_H.lookup_failure.DepthMismatch bitsLeft 0)
odE)
odE \<lbrace>cte_wp_at' (\<lambda>_. True)\<rbrace>, -) \<and> (\<not> isCNodeCap cap \<longrightarrow> \<lbrace>valid_objs' and valid_cap' cap\<rbrace> throwError (Fault_H.syscall_error.FailedLookup f Fault_H.lookup_failure.InvalidRoot) \<lbrace>cte_wp_at' (\<lambda>_. True)\<rbrace>, -) proof (prove)
goal (2 subgoals):
 1. isCNodeCap cap \<longrightarrow> \<lbrace>valid_objs' and valid_cap' cap\<rbrace> doE y <- rangeCheck depth (Suc 0) (size idx);
lookupErrorOnFailure f (doE (slot, bitsLeft) <- CSpace_H.resolveAddressBits cap idx depth;
if bitsLeft = 0 then returnOk slot else throwError (Fault_H.lookup_failure.DepthMismatch bitsLeft 0)
odE)
odE \<lbrace>cte_wp_at' (\<lambda>_. True)\<rbrace>, -
 2. \<not> isCNodeCap cap \<longrightarrow> \<lbrace>valid_objs' and valid_cap' cap\<rbrace> throwError (Fault_H.syscall_error.FailedLookup f Fault_H.lookup_failure.InvalidRoot) \<lbrace>cte_wp_at' (\<lambda>_. True)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<not> isCNodeCap cap \<longrightarrow> \<lbrace>valid_objs' and valid_cap' cap\<rbrace> throwError (Fault_H.syscall_error.FailedLookup f Fault_H.lookup_failure.InvalidRoot) \<lbrace>cte_wp_at' (\<lambda>_. True)\<rbrace>, -
 2. isCNodeCap cap \<longrightarrow> \<lbrace>valid_objs' and valid_cap' cap\<rbrace> doE y <- rangeCheck depth (Suc 0) (size idx);
lookupErrorOnFailure f (doE (slot, bitsLeft) <- CSpace_H.resolveAddressBits cap idx depth;
if bitsLeft = 0 then returnOk slot else throwError (Fault_H.lookup_failure.DepthMismatch bitsLeft 0)
odE)
odE \<lbrace>cte_wp_at' (\<lambda>_. True)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<not> isCNodeCap cap \<Longrightarrow> \<lbrace>valid_objs' and valid_cap' cap\<rbrace> throwError (Fault_H.syscall_error.FailedLookup f Fault_H.lookup_failure.InvalidRoot) \<lbrace>cte_wp_at' (\<lambda>_. True)\<rbrace>, -
 2. isCNodeCap cap \<longrightarrow> \<lbrace>valid_objs' and valid_cap' cap\<rbrace> doE y <- rangeCheck depth (Suc 0) (size idx);
lookupErrorOnFailure f (doE (slot, bitsLeft) <- CSpace_H.resolveAddressBits cap idx depth;
if bitsLeft = 0 then returnOk slot else throwError (Fault_H.lookup_failure.DepthMismatch bitsLeft 0)
odE)
odE \<lbrace>cte_wp_at' (\<lambda>_. True)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. isCNodeCap cap \<longrightarrow> \<lbrace>valid_objs' and valid_cap' cap\<rbrace> doE y <- rangeCheck depth (Suc 0) (size idx);
lookupErrorOnFailure f (doE (slot, bitsLeft) <- CSpace_H.resolveAddressBits cap idx depth;
if bitsLeft = 0 then returnOk slot else throwError (Fault_H.lookup_failure.DepthMismatch bitsLeft 0)
odE)
odE \<lbrace>cte_wp_at' (\<lambda>_. True)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. isCNodeCap cap \<Longrightarrow> \<lbrace>valid_objs' and valid_cap' cap\<rbrace> doE y <- rangeCheck depth (Suc 0) (size idx);
lookupErrorOnFailure f (doE p <- CSpace_H.resolveAddressBits cap idx depth;
if snd p = 0 then returnOk (fst p) else throwError (Fault_H.lookup_failure.DepthMismatch (snd p) 0)
odE)
odE \<lbrace>cte_wp_at' (\<lambda>_. True)\<rbrace>, - proof (prove)
goal:
No subgoals!