theory Detype_R

lemma locateCTE_cte_no_fail:
 "no_fail (cte_at' src) (locateCTE src)" apply (clarsimp simp:no_fail_def cte_wp_at'_def getObject_def
     locateCTE_def return_def gets_def get_def bind_def split_def
     assert_opt_def assert_def in_fail fail_set split:option.splits) apply (clarsimp simp:cte_check_def ObjectInstances_H.loadObject_cte) apply (drule in_singleton) by (auto simp: objBits_simps cteSizeBits_def alignError_def
    alignCheck_def in_monad is_aligned_mask magnitudeCheck_def
    typeError_def
    cong: if_cong split: if_splits option.splits kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (cte_wp_at' (\<lambda>_. True) src) (locateCTE src) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cte. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, b); fst (loadObject src a (snd (lookupAround2 src (ksPSpace s))) b s) = {(cte, s)}\<rbrakk> \<Longrightarrow> cte_check b src a (snd (lookupAround2 src (ksPSpace s))) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cte. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, b); fst ((case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits tcb);
if src - a = tcbVTableSlot << objBits undefined then return $ tcbVTable tcb else if src - a = tcbCTableSlot << objBits undefined then return $ tcbCTable tcb else if src - a = tcbReplySlot << objBits undefined then return $ tcbReply tcb else if src - a = tcbCallerSlot << objBits undefined then return $ tcbCaller tcb else if src - a = tcbIPCBufferSlot << objBits undefined then return $ tcbIPCBufferFrame tcb else if True then haskell_fail [] else undefined
od | KOCTE cte \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src (snd (lookupAround2 src (ksPSpace s))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] b) s) = {(cte, s)}\<rbrakk> \<Longrightarrow> case b of KOTCB tcb \<Rightarrow> (is_aligned a (objBits tcb) \<and> (case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits tcb \<le> z - a)) \<and> (src - a = tcbVTableSlot << cteSizeBits \<or> src - a = tcbCTableSlot << cteSizeBits \<or> src - a = tcbReplySlot << cteSizeBits \<or> src - a = tcbCallerSlot << cteSizeBits \<or> src - a = tcbIPCBufferSlot << cteSizeBits) | KOCTE v1 \<Rightarrow> src = a \<and> is_aligned a (objBits makeObject) \<and> (case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits makeObject \<le> z - a) | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b cte. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, b); (cte, s) \<in> fst ((case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits tcb);
if src - a = tcbVTableSlot << objBits undefined then return $ tcbVTable tcb else if src - a = tcbCTableSlot << objBits undefined then return $ tcbCTable tcb else if src - a = tcbReplySlot << objBits undefined then return $ tcbReply tcb else if src - a = tcbCallerSlot << objBits undefined then return $ tcbCaller tcb else if src - a = tcbIPCBufferSlot << objBits undefined then return $ tcbIPCBufferFrame tcb else if True then haskell_fail [] else undefined
od | KOCTE cte \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src (snd (lookupAround2 src (ksPSpace s))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] b) s)\<rbrakk> \<Longrightarrow> case b of KOTCB tcb \<Rightarrow> (is_aligned a (objBits tcb) \<and> (case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits tcb \<le> z - a)) \<and> (src - a = tcbVTableSlot << cteSizeBits \<or> src - a = tcbCTableSlot << cteSizeBits \<or> src - a = tcbReplySlot << cteSizeBits \<or> src - a = tcbCallerSlot << cteSizeBits \<or> src - a = tcbIPCBufferSlot << cteSizeBits) | KOCTE v1 \<Rightarrow> src = a \<and> is_aligned a (objBits makeObject) \<and> (case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits makeObject \<le> z - a) | _ \<Rightarrow> False