theory Invariants_H

lemma cte_wp_at'_pspaceI:
  "\<lbrakk>cte_wp_at' P p s; ksPSpace s = ksPSpace s'\<rbrakk> \<Longrightarrow> cte_wp_at' P p s'" supply if_cong[cong] apply (clarsimp simp add: cte_wp_at'_def getObject_def) apply (drule equalityD2) apply (clarsimp simp: in_monad loadObject_cte gets_def
                        get_def bind_def return_def split_def) apply (case_tac b) apply (simp_all add: in_monad typeError_def) prefer 2 apply (simp add: in_monad return_def alignError_def assert_opt_def
                    alignCheck_def magnitudeCheck_def when_def bind_def
             split: if_split_asm option.splits) apply (clarsimp simp: in_monad return_def alignError_def fail_def assert_opt_def
                        alignCheck_def bind_def when_def
                        objBits_cte_conv tcbCTableSlot_def tcbVTableSlot_def
                        tcbReplySlot_def cteSizeBits_def
                 split: if_split_asm
                 dest!: singleton_in_magnitude_check) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' P p s; ksPSpace s = ksPSpace s'\<rbrakk> \<Longrightarrow> cte_wp_at' P p s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' P p s; ksPSpace s = ksPSpace s'\<rbrakk> \<Longrightarrow> cte_wp_at' P p s' proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>ksPSpace s = ksPSpace s'; fst ((do map <- gets ksPSpace;
case lookupAround2 p map of (before, after) \<Rightarrow> do (ptr', y) <- assert_opt before;
loadObject p ptr' after y
od
od) s) = {(cte, s)}; P cte\<rbrakk> \<Longrightarrow> \<exists>cte. fst ((do map <- gets ksPSpace;
case lookupAround2 p map of (before, after) \<Rightarrow> do (ptr', y) <- assert_opt before;
loadObject p ptr' after y
od
od) s') = {(cte, s')} \<and> P cte proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>ksPSpace s = ksPSpace s'; P cte; {(cte, s)} \<subseteq> fst ((do map <- gets ksPSpace;
case lookupAround2 p map of (before, after) \<Rightarrow> do (ptr', y) <- assert_opt before;
loadObject p ptr' after y
od
od) s)\<rbrakk> \<Longrightarrow> \<exists>cte. fst ((do map <- gets ksPSpace;
case lookupAround2 p map of (before, after) \<Rightarrow> do (ptr', y) <- assert_opt before;
loadObject p ptr' after y
od
od) s') = {(cte, s')} \<and> P cte proof (prove)
goal (1 subgoal):
 1. \<And>cte a b. \<lbrakk>ksPSpace s = ksPSpace s'; P cte; fst (lookupAround2 p (ksPSpace s')) = Some (a, b); (cte, s) \<in> fst ((case b of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst ((a, b), s))) (objBits tcb);
magnitudeCheck (fst (fst ((a, b), s))) (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst ((a, b), s)) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst ((a, b), s))) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst ((a, b), s)))) s)\<rbrakk> \<Longrightarrow> \<exists>cte. (\<Union>x\<in>fst (assert_opt (fst (lookupAround2 p (ksPSpace s'))) s'). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(cte, s')} \<and> P cte proof (prove)
goal (8 subgoals):
 1. \<And>cte a b x1. \<lbrakk>ksPSpace s = ksPSpace s'; P cte; fst (lookupAround2 p (ksPSpace s')) = Some (a, b); (cte, s) \<in> fst ((case b of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst ((a, b), s))) (objBits tcb);
magnitudeCheck (fst (fst ((a, b), s))) (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst ((a, b), s)) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst ((a, b), s))) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst ((a, b), s)))) s); b = KOEndpoint x1\<rbrakk> \<Longrightarrow> \<exists>cte. (\<Union>x\<in>fst (assert_opt (fst (lookupAround2 p (ksPSpace s'))) s'). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(cte, s')} \<and> P cte
 2. \<And>cte a b x2. \<lbrakk>ksPSpace s = ksPSpace s'; P cte; fst (lookupAround2 p (ksPSpace s')) = Some (a, b); (cte, s) \<in> fst ((case b of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst ((a, b), s))) (objBits tcb);
magnitudeCheck (fst (fst ((a, b), s))) (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst ((a, b), s)) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst ((a, b), s))) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst ((a, b), s)))) s); b = KONotification x2\<rbrakk> \<Longrightarrow> \<exists>cte. (\<Union>x\<in>fst (assert_opt (fst (lookupAround2 p (ksPSpace s'))) s'). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(cte, s')} \<and> P cte
 3. \<And>cte a b. \<lbrakk>ksPSpace s = ksPSpace s'; P cte; fst (lookupAround2 p (ksPSpace s')) = Some (a, b); (cte, s) \<in> fst ((case b of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst ((a, b), s))) (objBits tcb);
magnitudeCheck (fst (fst ((a, b), s))) (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst ((a, b), s)) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst ((a, b), s))) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst ((a, b), s)))) s); b = KOKernelData\<rbrakk> \<Longrightarrow> \<exists>cte. (\<Union>x\<in>fst (assert_opt (fst (lookupAround2 p (ksPSpace s'))) s'). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(cte, s')} \<and> P cte
 4. \<And>cte a b. \<lbrakk>ksPSpace s = ksPSpace s'; P cte; fst (lookupAround2 p (ksPSpace s')) = Some (a, b); (cte, s) \<in> fst ((case b of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst ((a, b), s))) (objBits tcb);
magnitudeCheck (fst (fst ((a, b), s))) (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst ((a, b), s)) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst ((a, b), s))) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst ((a, b), s)))) s); b = KOUserData\<rbrakk> \<Longrightarrow> \<exists>cte. (\<Union>x\<in>fst (assert_opt (fst (lookupAround2 p (ksPSpace s'))) s'). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(cte, s')} \<and> P cte
 5. \<And>cte a b. \<lbrakk>ksPSpace s = ksPSpace s'; P cte; fst (lookupAround2 p (ksPSpace s')) = Some (a, b); (cte, s) \<in> fst ((case b of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst ((a, b), s))) (objBits tcb);
magnitudeCheck (fst (fst ((a, b), s))) (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst ((a, b), s)) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst ((a, b), s))) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst ((a, b), s)))) s); b = KOUserDataDevice\<rbrakk> \<Longrightarrow> \<exists>cte. (\<Union>x\<in>fst (assert_opt (fst (lookupAround2 p (ksPSpace s'))) s'). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(cte, s')} \<and> P cte
 6. \<And>cte a b x6. \<lbrakk>ksPSpace s = ksPSpace s'; P cte; fst (lookupAround2 p (ksPSpace s')) = Some (a, b); (cte, s) \<in> fst ((case b of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst ((a, b), s))) (objBits tcb);
magnitudeCheck (fst (fst ((a, b), s))) (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst ((a, b), s)) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst ((a, b), s))) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst ((a, b), s)))) s); b = KOTCB x6\<rbrakk> \<Longrightarrow> \<exists>cte. (\<Union>x\<in>fst (assert_opt (fst (lookupAround2 p (ksPSpace s'))) s'). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(cte, s')} \<and> P cte
 7. \<And>cte a b x7. \<lbrakk>ksPSpace s = ksPSpace s'; P cte; fst (lookupAround2 p (ksPSpace s')) = Some (a, b); (cte, s) \<in> fst ((case b of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst ((a, b), s))) (objBits tcb);
magnitudeCheck (fst (fst ((a, b), s))) (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst ((a, b), s)) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst ((a, b), s))) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst ((a, b), s)))) s); b = KOCTE x7\<rbrakk> \<Longrightarrow> \<exists>cte. (\<Union>x\<in>fst (assert_opt (fst (lookupAround2 p (ksPSpace s'))) s'). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(cte, s')} \<and> P cte
 8. \<And>cte a b x8. \<lbrakk>ksPSpace s = ksPSpace s'; P cte; fst (lookupAround2 p (ksPSpace s')) = Some (a, b); (cte, s) \<in> fst ((case b of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst ((a, b), s))) (objBits tcb);
magnitudeCheck (fst (fst ((a, b), s))) (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst ((a, b), s)) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst ((a, b), s)) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst ((a, b), s))) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst ((a, b), s)))) s); b = KOArch x8\<rbrakk> \<Longrightarrow> \<exists>cte. (\<Union>x\<in>fst (assert_opt (fst (lookupAround2 p (ksPSpace s'))) s'). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(cte, s')} \<and> P cte proof (prove)
goal (2 subgoals):
 1. \<And>cte a b x6. \<lbrakk>ksPSpace s = ksPSpace s'; P cte; fst (lookupAround2 p (ksPSpace s')) = Some (a, KOTCB x6); \<exists>s''. ((), s'') \<in> fst (alignCheck a (objBits x6) s) \<and> (\<exists>s''a. ((), s''a) \<in> fst (magnitudeCheck a (snd (lookupAround2 p (ksPSpace s'))) (objBits x6) s'') \<and> (cte, s) \<in> fst ((if p - a = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable x6, s)}, False) else if p - a = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable x6, s)}, False) else if p - a = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply x6, s)}, False) else if p - a = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller x6, s)}, False) else if p - a = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame x6, s)}, False) else fail) s''a)); b = KOTCB x6\<rbrakk> \<Longrightarrow> \<exists>cte. (\<Union>x\<in>fst (return (a, KOTCB x6) s'). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(cte, s')} \<and> P cte
 2. \<And>cte b x7. \<lbrakk>ksPSpace s = ksPSpace s'; P cte; fst (lookupAround2 p (ksPSpace s')) = Some (p, KOCTE x7); \<exists>s''. ((), s'') \<in> fst (alignCheck p (objBits x7) s) \<and> ((), s) \<in> fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s'))) (objBits x7) s'') \<and> cte = x7; b = KOCTE x7\<rbrakk> \<Longrightarrow> \<exists>cte. (\<Union>x\<in>fst (return (p, KOCTE x7) s'). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(cte, s')} \<and> P cte proof (prove)
goal (2 subgoals):
 1. \<And>cte b x7. \<lbrakk>ksPSpace s = ksPSpace s'; P cte; fst (lookupAround2 p (ksPSpace s')) = Some (p, KOCTE x7); \<exists>s''. ((), s'') \<in> fst (alignCheck p (objBits x7) s) \<and> ((), s) \<in> fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s'))) (objBits x7) s'') \<and> cte = x7; b = KOCTE x7\<rbrakk> \<Longrightarrow> \<exists>cte. (\<Union>x\<in>fst (return (p, KOCTE x7) s'). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(cte, s')} \<and> P cte
 2. \<And>cte a b x6. \<lbrakk>ksPSpace s = ksPSpace s'; P cte; fst (lookupAround2 p (ksPSpace s')) = Some (a, KOTCB x6); \<exists>s''. ((), s'') \<in> fst (alignCheck a (objBits x6) s) \<and> (\<exists>s''a. ((), s''a) \<in> fst (magnitudeCheck a (snd (lookupAround2 p (ksPSpace s'))) (objBits x6) s'') \<and> (cte, s) \<in> fst ((if p - a = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable x6, s)}, False) else if p - a = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable x6, s)}, False) else if p - a = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply x6, s)}, False) else if p - a = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller x6, s)}, False) else if p - a = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame x6, s)}, False) else fail) s''a)); b = KOTCB x6\<rbrakk> \<Longrightarrow> \<exists>cte. (\<Union>x\<in>fst (return (a, KOTCB x6) s'). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(cte, s')} \<and> P cte proof (prove)
goal (1 subgoal):
 1. \<And>cte a b x6. \<lbrakk>ksPSpace s = ksPSpace s'; P cte; fst (lookupAround2 p (ksPSpace s')) = Some (a, KOTCB x6); \<exists>s''. ((), s'') \<in> fst (alignCheck a (objBits x6) s) \<and> (\<exists>s''a. ((), s''a) \<in> fst (magnitudeCheck a (snd (lookupAround2 p (ksPSpace s'))) (objBits x6) s'') \<and> (cte, s) \<in> fst ((if p - a = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable x6, s)}, False) else if p - a = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable x6, s)}, False) else if p - a = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply x6, s)}, False) else if p - a = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller x6, s)}, False) else if p - a = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame x6, s)}, False) else fail) s''a)); b = KOTCB x6\<rbrakk> \<Longrightarrow> \<exists>cte. (\<Union>x\<in>fst (return (a, KOTCB x6) s'). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (fst (ksPSpace s', s')))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(cte, s')} \<and> P cte proof (prove)
goal:
No subgoals!