theory CSpace_R

lemma lookupSlotForCNodeOp_corres:
  "\<lbrakk>cap_relation c c'; ptr = to_bl ptr'\<rbrakk>
  \<Longrightarrow> corres (ser \<oplus> (\<lambda>cref cref'. cref' = cte_map cref))
            (valid_objs and pspace_aligned and valid_cap c)
            (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' c')
            (lookup_slot_for_cnode_op s c ptr depth)
            (lookupSlotForCNodeOp s c' ptr' depth)" apply (simp add: lookup_slot_for_cnode_op_def lookupSlotForCNodeOp_def) apply (clarsimp simp: lookup_failure_map_def split_def word_size) apply (clarsimp simp: rangeCheck_def[unfolded fun_app_def unlessE_def] whenE_def
                        word_bits_def toInteger_nat fromIntegral_def fromInteger_nat) apply (rule corres_lookup_error) apply (rule corres_guard_imp) apply (rule corres_splitEE) apply (rule rab_corres'; simp) apply (rule corres_trivial) apply (clarsimp simp: returnOk_def lookup_failure_map_def
                      split: list.split) apply wp+ apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> (\<lambda>cref cref'. cref' = cte_map cref)) (valid_objs and pspace_aligned and valid_cap c) (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' c') (lookup_slot_for_cnode_op s c ptr depth) (lookupSlotForCNodeOp s c' ptr' depth) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'\<rbrakk> \<Longrightarrow> (is_cnode_cap c \<longrightarrow> corres (ser \<oplus> (\<lambda>cref cref'. cref' = cte_map cref)) (valid_objs and pspace_aligned and valid_cap c) (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' c') (doE y <- whenE (depth = 0 \<or> word_bits < depth) (throwError (ExceptionTypes_A.syscall_error.RangeError 1 (word_of_nat word_bits)));
lookup_error_on_failure s (doE (slot, rem) <- resolve_address_bits (c, drop (32 - depth) (to_bl ptr'));
case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ ExceptionTypes_A.lookup_failure.DepthMismatch (length rem) 0
odE)
odE) (doE y <- rangeCheck depth (Suc 0) (size ptr');
lookupErrorOnFailure s (doE (slot, bitsLeft) <- CSpace_H.resolveAddressBits c' ptr' depth;
if bitsLeft = 0 then returnOk slot else throwError (Fault_H.lookup_failure.DepthMismatch bitsLeft 0)
odE)
odE)) \<and> (\<not> is_cnode_cap c \<longrightarrow> (\<exists>s. valid_objs s \<and> pspace_aligned s \<and> s \<turnstile> c \<and> (\<exists>s'. valid_objs' s' \<and> pspace_aligned' s' \<and> pspace_distinct' s' \<and> valid_cap' c' s' \<and> (s, s') \<in> state_relation)) \<longrightarrow> Fault_H.lookup_failure.InvalidRoot = lookup_failure_map ExceptionTypes_A.lookup_failure.InvalidRoot) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c\<rbrakk> \<Longrightarrow> corres (ser \<oplus> (\<lambda>cref cref'. cref' = cte_map cref)) (valid_objs and pspace_aligned and valid_cap c) (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' c') (doE y <- whenE (depth = 0 \<or> word_bits < depth) (throwError (ExceptionTypes_A.syscall_error.RangeError 1 (word_of_nat word_bits)));
lookup_error_on_failure s (doE p <- resolve_address_bits (c, drop (32 - depth) (to_bl ptr'));
case snd p of [] \<Rightarrow> returnOk (fst p) | a # list \<Rightarrow> throwError $ ExceptionTypes_A.lookup_failure.DepthMismatch (length (snd p)) 0
odE)
odE) (doE y <- rangeCheck depth (Suc 0) 32;
lookupErrorOnFailure s (doE p <- CSpace_H.resolveAddressBits c' ptr' depth;
if snd p = 0 then returnOk (fst p) else throwError (Fault_H.lookup_failure.DepthMismatch (snd p) 0)
odE)
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth\<rbrakk> \<Longrightarrow> corres (ser \<oplus> (\<lambda>cref cref'. cref' = cte_map cref)) (valid_objs and pspace_aligned and valid_cap c) (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' c') (lookup_error_on_failure s (doE p <- resolve_address_bits (c, drop (32 - depth) (to_bl ptr'));
case snd p of [] \<Rightarrow> returnOk (fst p) | a # list \<Rightarrow> throwError $ ExceptionTypes_A.lookup_failure.DepthMismatch (length (snd p)) 0
odE)) (lookupErrorOnFailure s (doE p <- CSpace_H.resolveAddressBits c' ptr' depth;
if snd p = 0 then returnOk (fst p) else throwError (Fault_H.lookup_failure.DepthMismatch (snd p) 0)
odE)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>cref cref'. cref' = cte_map cref)) (valid_objs and pspace_aligned and valid_cap c) (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' c') (doE p <- resolve_address_bits (c, drop (32 - depth) (to_bl ptr'));
case snd p of [] \<Rightarrow> returnOk (fst p) | a # list \<Rightarrow> throwError $ ExceptionTypes_A.lookup_failure.DepthMismatch (length (snd p)) 0
odE) (doE p <- CSpace_H.resolveAddressBits c' ptr' depth;
if snd p = 0 then returnOk (fst p) else throwError (Fault_H.lookup_failure.DepthMismatch (snd p) 0)
odE) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>cref cref'. cref' = cte_map cref)) ?Q27 ?Q'27 (doE p <- resolve_address_bits (c, drop (32 - depth) (to_bl ptr'));
case snd p of [] \<Rightarrow> returnOk (fst p) | a # list \<Rightarrow> throwError $ ExceptionTypes_A.lookup_failure.DepthMismatch (length (snd p)) 0
odE) (doE p <- CSpace_H.resolveAddressBits c' ptr' depth;
if snd p = 0 then returnOk (fst p) else throwError (Fault_H.lookup_failure.DepthMismatch (snd p) 0)
odE)
 2. \<And>s. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; (valid_objs and pspace_aligned and valid_cap c) s\<rbrakk> \<Longrightarrow> ?Q27 s
 3. \<And>s. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' c') s\<rbrakk> \<Longrightarrow> ?Q'27 s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> ?r'31) ?P31 ?P'31 (resolve_address_bits (c, drop (32 - depth) (to_bl ptr'))) (CSpace_H.resolveAddressBits c' ptr' depth)
 2. \<And>p pa. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; ?r'31 p pa\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>cref cref'. cref' = cte_map cref)) (?R31 p) (?R'31 pa) (case snd p of [] \<Rightarrow> returnOk (fst p) | a # list \<Rightarrow> throwError $ ExceptionTypes_A.lookup_failure.DepthMismatch (length (snd p)) 0) (if snd pa = 0 then returnOk (fst pa) else throwError (Fault_H.lookup_failure.DepthMismatch (snd pa) 0))
 3. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth\<rbrakk> \<Longrightarrow> \<lbrace>?Q31\<rbrace> resolve_address_bits (c, drop (32 - depth) (to_bl ptr')) \<lbrace>?R31\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31\<rbrace> CSpace_H.resolveAddressBits c' ptr' depth \<lbrace>?R'31\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; (valid_objs and pspace_aligned and valid_cap c) s\<rbrakk> \<Longrightarrow> (?P31 and ?Q31) s
 6. \<And>s. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' c') s\<rbrakk> \<Longrightarrow> (?P'31 and ?Q'31) s proof (prove)
goal (5 subgoals):
 1. \<And>p pa. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; (case p of (cte, bits) \<Rightarrow> \<lambda>(cte', bits'). cte' = cte_map cte \<and> length bits = bits') pa\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>cref cref'. cref' = cte_map cref)) (?R31 p) (?R'31 pa) (case snd p of [] \<Rightarrow> returnOk (fst p) | a # list \<Rightarrow> throwError $ ExceptionTypes_A.lookup_failure.DepthMismatch (length (snd p)) 0) (if snd pa = 0 then returnOk (fst pa) else throwError (Fault_H.lookup_failure.DepthMismatch (snd pa) 0))
 2. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth\<rbrakk> \<Longrightarrow> \<lbrace>?Q31\<rbrace> resolve_address_bits (c, drop (32 - depth) (to_bl ptr')) \<lbrace>?R31\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31\<rbrace> CSpace_H.resolveAddressBits c' ptr' depth \<lbrace>?R'31\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; (valid_objs and pspace_aligned and valid_cap c) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and valid_cap (fst (c, drop (32 - depth) (to_bl ptr'))) and ?Q31) s
 5. \<And>s. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' c') s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c' and ?Q'31) s proof (prove)
goal (5 subgoals):
 1. \<And>p pa. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; (case p of (cte, bits) \<Rightarrow> \<lambda>(cte', bits'). cte' = cte_map cte \<and> length bits = bits') pa\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>cref cref'. cref' = cte_map cref)) (\<lambda>_. True) (\<lambda>_. True) (case snd p of [] \<Rightarrow> returnOk (fst p) | a # list \<Rightarrow> throwError $ ExceptionTypes_A.lookup_failure.DepthMismatch (length (snd p)) 0) (if snd pa = 0 then returnOk (fst pa) else throwError (Fault_H.lookup_failure.DepthMismatch (snd pa) 0))
 2. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth\<rbrakk> \<Longrightarrow> \<lbrace>?Q31\<rbrace> resolve_address_bits (c, drop (32 - depth) (to_bl ptr')) \<lbrace>\<lambda>p _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31\<rbrace> CSpace_H.resolveAddressBits c' ptr' depth \<lbrace>\<lambda>pa _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; (valid_objs and pspace_aligned and valid_cap c) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and valid_cap (fst (c, drop (32 - depth) (to_bl ptr'))) and ?Q31) s
 5. \<And>s. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' c') s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c' and ?Q'31) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth\<rbrakk> \<Longrightarrow> \<lbrace>?Q31\<rbrace> resolve_address_bits (c, drop (32 - depth) (to_bl ptr')) \<lbrace>\<lambda>p _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31\<rbrace> CSpace_H.resolveAddressBits c' ptr' depth \<lbrace>\<lambda>pa _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; (valid_objs and pspace_aligned and valid_cap c) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and valid_cap (fst (c, drop (32 - depth) (to_bl ptr'))) and ?Q31) s
 4. \<And>s. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' c') s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c' and ?Q'31) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; (valid_objs and pspace_aligned and valid_cap c) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and valid_cap (fst (c, drop (32 - depth) (to_bl ptr'))) and (\<lambda>s. True \<and> True)) s
 2. \<And>s. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' c') s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c' and (\<lambda>s. True \<and> True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap_relation c c'; ptr = to_bl ptr'; is_cnode_cap c; 0 < depth; \<not> 32 < depth; (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' c') s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c' and (\<lambda>s. True \<and> True)) s proof (prove)
goal:
No subgoals!