theory CSpace1_R

lemma no_fail_getCTE [wp]:
  "no_fail (cte_at' p) (getCTE p)" apply (simp add: getCTE_def getObject_def split_def
                   loadObject_cte alignCheck_def unless_def
                   alignError_def is_aligned_mask[symmetric]
             cong: kernel_object.case_cong) apply (rule no_fail_pre, (wp | wpc)+) apply (clarsimp simp: cte_wp_at'_def getObject_def
                        loadObject_cte split_def in_monad
                 dest!: in_singleton
             split del: if_split) apply (clarsimp simp: in_monad typeError_def objBits_simps
                        magnitudeCheck_def
                 split: kernel_object.split_asm if_split_asm option.split_asm
             split del: if_split) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (cte_wp_at' (\<lambda>_. True) p) (getCTE p) proof (prove)
goal (1 subgoal):
 1. no_fail (cte_wp_at' (\<lambda>_. True) p) (do map <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p map));
case snd pa of KOEndpoint endpoint \<Rightarrow> typeError [] (KOEndpoint endpoint) | KONotification notification \<Rightarrow> typeError [] (KONotification notification) | KOKernelData \<Rightarrow> typeError [] KOKernelData | KOUserData \<Rightarrow> typeError [] KOUserData | KOUserDataDevice \<Rightarrow> typeError [] KOUserDataDevice | KOTCB tcb \<Rightarrow> do y <- when (\<not> is_aligned (fst pa) (objBits tcb)) fail;
y <- magnitudeCheck (fst pa) (snd (lookupAround2 p map)) (objBits tcb);
if p - fst pa = tcbVTableSlot << objBits undefined then return (tcbVTable tcb) else if p - fst pa = tcbCTableSlot << objBits undefined then return (tcbCTable tcb) else if p - fst pa = tcbReplySlot << objBits undefined then return (tcbReply tcb) else if p - fst pa = tcbCallerSlot << objBits undefined then return (tcbCaller tcb) else if p - fst pa = tcbIPCBufferSlot << objBits undefined then return (tcbIPCBufferFrame tcb) else fail
od | KOCTE cte \<Rightarrow> do y <- when (p \<noteq> fst pa) fail;
y <- when (\<not> is_aligned p (objBits cte)) fail;
y <- magnitudeCheck p (snd (lookupAround2 p map)) (objBits cte);
return cte
od | KOArch arch_kernel_object \<Rightarrow> typeError [] (KOArch arch_kernel_object)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>_. True) p s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. fst (lookupAround2 p (ksPSpace s)) \<noteq> None) and (\<lambda>sa. fst (lookupAround2 p (ksPSpace s)) \<noteq> None \<longrightarrow> (\<forall>x. snd (the (fst (lookupAround2 p (ksPSpace s)))) = KOEndpoint x \<longrightarrow> False) \<and> (\<forall>x. snd (the (fst (lookupAround2 p (ksPSpace s)))) = KONotification x \<longrightarrow> False) \<and> (snd (the (fst (lookupAround2 p (ksPSpace s)))) = KOKernelData \<longrightarrow> False) \<and> (snd (the (fst (lookupAround2 p (ksPSpace s)))) = KOUserData \<longrightarrow> False) \<and> (snd (the (fst (lookupAround2 p (ksPSpace s)))) = KOUserDataDevice \<longrightarrow> False) \<and> (\<forall>x. snd (the (fst (lookupAround2 p (ksPSpace s)))) = KOTCB x \<longrightarrow> ((if \<not> is_aligned (fst (the (fst (lookupAround2 p (ksPSpace s))))) (objBits x) then \<lambda>_. False else (\<lambda>_. True)) and (\<lambda>sa. (case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x \<le> z - fst (the (fst (lookupAround2 p (ksPSpace s))))) \<and> (if \<not> is_aligned (fst (the (fst (lookupAround2 p (ksPSpace s))))) (objBits x) then \<lambda>_. True else if p - fst (the (fst (lookupAround2 p (ksPSpace s)))) = tcbVTableSlot << objBits undefined then \<lambda>_. True else if p - fst (the (fst (lookupAround2 p (ksPSpace s)))) = tcbCTableSlot << objBits undefined then \<lambda>_. True else if p - fst (the (fst (lookupAround2 p (ksPSpace s)))) = tcbReplySlot << objBits undefined then \<lambda>_. True else if p - fst (the (fst (lookupAround2 p (ksPSpace s)))) = tcbCallerSlot << objBits undefined then \<lambda>_. True else if p - fst (the (fst (lookupAround2 p (ksPSpace s)))) = tcbIPCBufferSlot << objBits undefined then \<lambda>_. True else (\<lambda>_. False)) sa)) sa) \<and> (\<forall>x. snd (the (fst (lookupAround2 p (ksPSpace s)))) = KOCTE x \<longrightarrow> ((if p \<noteq> fst (the (fst (lookupAround2 p (ksPSpace s)))) then \<lambda>_. False else (\<lambda>_. True)) and (if p \<noteq> fst (the (fst (lookupAround2 p (ksPSpace s)))) then \<lambda>_. True else (\<lambda>sa. (if \<not> is_aligned p (objBits x) then \<lambda>_. False else (\<lambda>_. True)) sa \<and> (case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x \<le> z - p) \<and> True))) sa) \<and> (\<forall>x. snd (the (fst (lookupAround2 p (ksPSpace s)))) = KOArch x \<longrightarrow> False))) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte a b. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, b); (cte, s) \<in> fst ((case b of KOTCB tcb \<Rightarrow> do alignCheck (fst (a, b)) (objBits tcb);
magnitudeCheck (fst (a, b)) (snd (lookupAround2 p (ksPSpace s))) (objBits tcb);
if p - fst (a, b) = tcbVTableSlot << objBits undefined then return (tcbVTable tcb) else if p - fst (a, b) = tcbCTableSlot << objBits undefined then return (tcbCTable tcb) else if p - fst (a, b) = tcbReplySlot << objBits undefined then return (tcbReply tcb) else if p - fst (a, b) = tcbCallerSlot << objBits undefined then return (tcbCaller tcb) else if p - fst (a, b) = tcbIPCBufferSlot << objBits undefined then return (tcbIPCBufferFrame tcb) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (a, b)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (a, b))) s)\<rbrakk> \<Longrightarrow> (\<forall>x. b \<noteq> KOEndpoint x) \<and> (\<forall>x. b \<noteq> KONotification x) \<and> b \<noteq> KOKernelData \<and> b \<noteq> KOUserData \<and> b \<noteq> KOUserDataDevice \<and> (\<forall>x. b = KOTCB x \<longrightarrow> (if \<not> is_aligned a (objBits x) then \<lambda>_. False else (\<lambda>_. True)) s \<and> (case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x \<le> z - a) \<and> (if \<not> is_aligned a (objBits x) then \<lambda>_. True else if p - a = tcbVTableSlot << objBits undefined then \<lambda>_. True else if p - a = tcbCTableSlot << objBits undefined then \<lambda>_. True else if p - a = tcbReplySlot << objBits undefined then \<lambda>_. True else if p - a = tcbCallerSlot << objBits undefined then \<lambda>_. True else if p - a = tcbIPCBufferSlot << objBits undefined then \<lambda>_. True else (\<lambda>_. False)) s) \<and> (\<forall>x. b = KOCTE x \<longrightarrow> (if p \<noteq> a then \<lambda>_. False else (\<lambda>_. True)) s \<and> (if p \<noteq> a then \<lambda>_. True else (\<lambda>sa. (if \<not> is_aligned p (objBits x) then \<lambda>_. False else (\<lambda>_. True)) sa \<and> (case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x \<le> z - p))) s) \<and> (\<forall>x. b \<noteq> KOArch x) proof (prove)
goal (6 subgoals):
 1. \<And>s a x6 x2. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); p - a = tcbVTableSlot << cteSizeBits; snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned a tcbBlockSizeBits; \<not> x2 - a < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a
 2. \<And>s a x6 x2. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbCTableSlot << cteSizeBits \<noteq> tcbVTableSlot << cteSizeBits; p - a = tcbCTableSlot << cteSizeBits; snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned a tcbBlockSizeBits; \<not> x2 - a < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a
 3. \<And>s a x6 x2. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbReplySlot << cteSizeBits \<noteq> tcbVTableSlot << cteSizeBits; tcbReplySlot << cteSizeBits \<noteq> tcbCTableSlot << cteSizeBits; p - a = tcbReplySlot << cteSizeBits; snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned a tcbBlockSizeBits; \<not> x2 - a < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a
 4. \<And>s a x6 x2. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbCallerSlot << cteSizeBits \<noteq> tcbVTableSlot << cteSizeBits; tcbCallerSlot << cteSizeBits \<noteq> tcbCTableSlot << cteSizeBits; tcbCallerSlot << cteSizeBits \<noteq> tcbReplySlot << cteSizeBits; p - a = tcbCallerSlot << cteSizeBits; snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned a tcbBlockSizeBits; \<not> x2 - a < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a
 5. \<And>s a x6 x2. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbIPCBufferSlot << cteSizeBits \<noteq> tcbVTableSlot << cteSizeBits; tcbIPCBufferSlot << cteSizeBits \<noteq> tcbCTableSlot << cteSizeBits; tcbIPCBufferSlot << cteSizeBits \<noteq> tcbReplySlot << cteSizeBits; tcbIPCBufferSlot << cteSizeBits \<noteq> tcbCallerSlot << cteSizeBits; p - a = tcbIPCBufferSlot << cteSizeBits; snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned a tcbBlockSizeBits; \<not> x2 - a < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a
 6. \<And>s cte x2. \<lbrakk>ksPSpace s p = Some (KOCTE cte); snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned p cteSizeBits; \<not> x2 - p < 2 ^ cteSizeBits\<rbrakk> \<Longrightarrow> 2 ^ cteSizeBits \<le> x2 - p proof (prove)
goal:
No subgoals!