theory Detype_R

lemma cte_wp_at_top:
  "(cte_wp_at' \<top> src s)
  = (\<exists>a b. ( fst (lookupAround2 src (ksPSpace s)) = Some (a, b) \<and>
  cte_check b src a (snd (lookupAround2 src (ksPSpace s)))))" apply (simp add:cte_wp_at'_def getObject_def gets_def
    get_def bind_def return_def split_def
    assert_opt_def fail_def
    split:option.splits) apply (clarsimp simp:loadObject_cte) apply (case_tac b,simp_all) apply ((simp add: typeError_def fail_def cte_check_def
                  split: Structures_H.kernel_object.splits)+)[5] apply (simp add:loadObject_cte cte_check_def
      tcbIPCBufferSlot_def tcbCallerSlot_def
      tcbReplySlot_def tcbCTableSlot_def
      tcbVTableSlot_def objBits_simps cteSizeBits_def) apply (simp add:alignCheck_def bind_def
      alignError_def fail_def return_def objBits_simps
      magnitudeCheck_def in_monad is_aligned_mask
      when_def unless_def split:option.splits) apply (intro conjI impI allI,simp_all add:not_le) apply (clarsimp simp:cte_check_def) apply (simp add:alignCheck_def bind_def
     alignError_def fail_def return_def objBits_simps
     magnitudeCheck_def in_monad is_aligned_mask
     when_def unless_def split:option.splits) apply (intro conjI impI allI,simp_all add:not_le) apply (simp add:typeError_def fail_def
         cte_check_def split:Structures_H.kernel_object.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (\<lambda>_. True) src s = (\<exists>a b. fst (lookupAround2 src (ksPSpace s)) = Some (a, b) \<and> cte_check b src a (snd (lookupAround2 src (ksPSpace s)))) proof (prove)
goal (1 subgoal):
 1. \<forall>a b. fst (lookupAround2 src (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject src a (snd (lookupAround2 src (ksPSpace s))) b s) = {(cte, s)}) = cte_check b src a (snd (lookupAround2 src (ksPSpace s))) proof (prove)
goal (1 subgoal):
 1. \<And>a b. fst (lookupAround2 src (ksPSpace s)) = Some (a, b) \<Longrightarrow> (\<exists>cte. 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 haskell_fail []
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)}) = cte_check b src a (snd (lookupAround2 src (ksPSpace s))) proof (prove)
goal (8 subgoals):
 1. \<And>a b x1. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOEndpoint x1); b = KOEndpoint x1\<rbrakk> \<Longrightarrow> (\<exists>cte. fst (typeError [] (KOEndpoint x1) s) = {(cte, s)}) = cte_check (KOEndpoint x1) src a (snd (lookupAround2 src (ksPSpace s)))
 2. \<And>a b x2. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KONotification x2); b = KONotification x2\<rbrakk> \<Longrightarrow> (\<exists>cte. fst (typeError [] (KONotification x2) s) = {(cte, s)}) = cte_check (KONotification x2) src a (snd (lookupAround2 src (ksPSpace s)))
 3. \<And>a b. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOKernelData); b = KOKernelData\<rbrakk> \<Longrightarrow> (\<exists>cte. fst (typeError [] KOKernelData s) = {(cte, s)}) = cte_check KOKernelData src a (snd (lookupAround2 src (ksPSpace s)))
 4. \<And>a b. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOUserData); b = KOUserData\<rbrakk> \<Longrightarrow> (\<exists>cte. fst (typeError [] KOUserData s) = {(cte, s)}) = cte_check KOUserData src a (snd (lookupAround2 src (ksPSpace s)))
 5. \<And>a b. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOUserDataDevice); b = KOUserDataDevice\<rbrakk> \<Longrightarrow> (\<exists>cte. fst (typeError [] KOUserDataDevice s) = {(cte, s)}) = cte_check KOUserDataDevice src a (snd (lookupAround2 src (ksPSpace s)))
 6. \<And>a b x6. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOTCB x6); b = KOTCB x6\<rbrakk> \<Longrightarrow> (src - a = tcbIPCBufferSlot << objBits undefined \<longrightarrow> (tcbIPCBufferSlot << objBits undefined = tcbCallerSlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbReplySlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbReply x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCaller x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))))) \<and> (tcbIPCBufferSlot << objBits undefined \<noteq> tcbCallerSlot << objBits undefined \<longrightarrow> (tcbIPCBufferSlot << objBits undefined = tcbReplySlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbReply x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))))) \<and> (tcbIPCBufferSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (tcbIPCBufferSlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (tcbIPCBufferSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbIPCBufferSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbIPCBufferSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbIPCBufferFrame x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))))))) \<and> (src - a \<noteq> tcbIPCBufferSlot << objBits undefined \<longrightarrow> (src - a = tcbCallerSlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbReplySlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbReply x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCaller x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))))) \<and> (src - a \<noteq> tcbCallerSlot << objBits undefined \<longrightarrow> (src - a = tcbReplySlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbReply x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))))) \<and> (src - a \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (src - a = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (src - a \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (src - a = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (src - a \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
fail
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))))))
 7. \<And>a b x7. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOCTE x7); b = KOCTE x7\<rbrakk> \<Longrightarrow> (\<exists>cte. fst ((do y <- unless (src = a) fail;
y <- alignCheck src (objBits x7);
y <- magnitudeCheck src (snd (lookupAround2 src (ksPSpace s))) (objBits x7);
return x7
od) s) = {(cte, s)}) = cte_check (KOCTE x7) src a (snd (lookupAround2 src (ksPSpace s)))
 8. \<And>a b x8. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOArch x8); b = KOArch x8\<rbrakk> \<Longrightarrow> (\<exists>cte. fst (typeError [] (KOArch x8) s) = {(cte, s)}) = cte_check (KOArch x8) src a (snd (lookupAround2 src (ksPSpace s))) proof (prove)
goal (3 subgoals):
 1. \<And>a b x6. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOTCB x6); b = KOTCB x6\<rbrakk> \<Longrightarrow> (src - a = tcbIPCBufferSlot << objBits undefined \<longrightarrow> (tcbIPCBufferSlot << objBits undefined = tcbCallerSlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbReplySlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbReply x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCaller x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))))) \<and> (tcbIPCBufferSlot << objBits undefined \<noteq> tcbCallerSlot << objBits undefined \<longrightarrow> (tcbIPCBufferSlot << objBits undefined = tcbReplySlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbReply x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))))) \<and> (tcbIPCBufferSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (tcbIPCBufferSlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (tcbIPCBufferSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbIPCBufferSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbIPCBufferSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbIPCBufferFrame x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))))))) \<and> (src - a \<noteq> tcbIPCBufferSlot << objBits undefined \<longrightarrow> (src - a = tcbCallerSlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbReplySlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbReply x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCaller x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))))) \<and> (src - a \<noteq> tcbCallerSlot << objBits undefined \<longrightarrow> (src - a = tcbReplySlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbReply x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))))) \<and> (src - a \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (src - a = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbCTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))) \<and> (src - a \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (src - a = tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
return (tcbVTable x6)
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s)))) \<and> (src - a \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) (objBits x6);
fail
od) s) = {(cte, s)}) = cte_check (KOTCB x6) src a (snd (lookupAround2 src (ksPSpace s))))))))
 2. \<And>a b x7. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOCTE x7); b = KOCTE x7\<rbrakk> \<Longrightarrow> (\<exists>cte. fst ((do y <- unless (src = a) fail;
y <- alignCheck src (objBits x7);
y <- magnitudeCheck src (snd (lookupAround2 src (ksPSpace s))) (objBits x7);
return x7
od) s) = {(cte, s)}) = cte_check (KOCTE x7) src a (snd (lookupAround2 src (ksPSpace s)))
 3. \<And>a b x8. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOArch x8); b = KOArch x8\<rbrakk> \<Longrightarrow> (\<exists>cte. fst (typeError [] (KOArch x8) s) = {(cte, s)}) = cte_check (KOArch x8) src a (snd (lookupAround2 src (ksPSpace s))) proof (prove)
goal (3 subgoals):
 1. \<And>a b x6. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOTCB x6); b = KOTCB x6\<rbrakk> \<Longrightarrow> (src - a = 0x40 \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a tcbBlockSizeBits;
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) tcbBlockSizeBits;
return (tcbIPCBufferFrame x6)
od) s) = {(cte, s)}) = (is_aligned a tcbBlockSizeBits \<and> (case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> z - a))) \<and> (src - a \<noteq> 0x40 \<longrightarrow> (src - a = 0x30 \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a tcbBlockSizeBits;
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) tcbBlockSizeBits;
return (tcbCaller x6)
od) s) = {(cte, s)}) = (is_aligned a tcbBlockSizeBits \<and> (case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> z - a))) \<and> (src - a \<noteq> 0x30 \<longrightarrow> (src - a = 0x20 \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a tcbBlockSizeBits;
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) tcbBlockSizeBits;
return (tcbReply x6)
od) s) = {(cte, s)}) = (is_aligned a tcbBlockSizeBits \<and> (case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> z - a))) \<and> (src - a \<noteq> 0x20 \<longrightarrow> (src = a \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a tcbBlockSizeBits;
y <- magnitudeCheck a (snd (lookupAround2 a (ksPSpace s))) tcbBlockSizeBits;
return (tcbCTable x6)
od) s) = {(cte, s)}) = (is_aligned a tcbBlockSizeBits \<and> (case snd (lookupAround2 a (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> z - a))) \<and> (src \<noteq> a \<longrightarrow> (src - a = 0x10 \<longrightarrow> (\<exists>cte. fst ((do y <- alignCheck a tcbBlockSizeBits;
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) tcbBlockSizeBits;
return (tcbVTable x6)
od) s) = {(cte, s)}) = (is_aligned a tcbBlockSizeBits \<and> (case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> z - a))) \<and> (src - a \<noteq> 0x10 \<longrightarrow> (\<forall>cte. fst ((do y <- alignCheck a tcbBlockSizeBits;
y <- magnitudeCheck a (snd (lookupAround2 src (ksPSpace s))) tcbBlockSizeBits;
fail
od) s) \<noteq> {(cte, s)}))))))
 2. \<And>a b x7. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOCTE x7); b = KOCTE x7\<rbrakk> \<Longrightarrow> (\<exists>cte. fst ((do y <- unless (src = a) fail;
y <- alignCheck src (objBits x7);
y <- magnitudeCheck src (snd (lookupAround2 src (ksPSpace s))) (objBits x7);
return x7
od) s) = {(cte, s)}) = cte_check (KOCTE x7) src a (snd (lookupAround2 src (ksPSpace s)))
 3. \<And>a b x8. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOArch x8); b = KOArch x8\<rbrakk> \<Longrightarrow> (\<exists>cte. fst (typeError [] (KOArch x8) s) = {(cte, s)}) = cte_check (KOArch x8) src a (snd (lookupAround2 src (ksPSpace s))) proof (prove)
goal (3 subgoals):
 1. \<And>a b x6. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOTCB x6); b = KOTCB x6\<rbrakk> \<Longrightarrow> (snd (lookupAround2 a (ksPSpace s)) = None \<longrightarrow> (\<forall>x2. (x2 - a < 2 ^ tcbBlockSizeBits \<longrightarrow> snd (lookupAround2 src (ksPSpace s)) = Some x2 \<longrightarrow> a && mask tcbBlockSizeBits = 0 \<longrightarrow> (src - a = 0x40 \<longrightarrow> \<not> 2 ^ tcbBlockSizeBits \<le> x2 - a) \<and> (src - a \<noteq> 0x40 \<longrightarrow> (src - a = 0x30 \<longrightarrow> \<not> 2 ^ tcbBlockSizeBits \<le> x2 - a) \<and> (src - a \<noteq> 0x30 \<longrightarrow> (src - a = 0x20 \<longrightarrow> \<not> 2 ^ tcbBlockSizeBits \<le> x2 - a) \<and> (src - a \<noteq> 0x20 \<longrightarrow> src \<noteq> a \<longrightarrow> src - a = 0x10 \<longrightarrow> \<not> 2 ^ tcbBlockSizeBits \<le> x2 - a)))) \<and> (\<not> x2 - a < 2 ^ tcbBlockSizeBits \<longrightarrow> snd (lookupAround2 src (ksPSpace s)) = Some x2 \<longrightarrow> a && mask tcbBlockSizeBits = 0 \<longrightarrow> (src - a = 0x40 \<longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a) \<and> (src - a \<noteq> 0x40 \<longrightarrow> (src - a = 0x30 \<longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a) \<and> (src - a \<noteq> 0x30 \<longrightarrow> (src - a = 0x20 \<longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a) \<and> (src - a \<noteq> 0x20 \<longrightarrow> src \<noteq> a \<longrightarrow> src - a = 0x10 \<longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a)))))) \<and> (\<forall>x2. (x2 - a < 2 ^ tcbBlockSizeBits \<longrightarrow> snd (lookupAround2 a (ksPSpace s)) = Some x2 \<longrightarrow> (snd (lookupAround2 src (ksPSpace s)) = None \<longrightarrow> a && mask tcbBlockSizeBits = 0 \<longrightarrow> src - a \<noteq> 0x40 \<longrightarrow> src - a \<noteq> 0x30 \<longrightarrow> src - a \<noteq> 0x20 \<longrightarrow> src = a \<longrightarrow> \<not> 2 ^ tcbBlockSizeBits \<le> x2 - a) \<and> (\<forall>x2a. (x2a - a < 2 ^ tcbBlockSizeBits \<longrightarrow> snd (lookupAround2 src (ksPSpace s)) = Some x2a \<longrightarrow> a && mask tcbBlockSizeBits = 0 \<longrightarrow> (src - a = 0x40 \<longrightarrow> \<not> 2 ^ tcbBlockSizeBits \<le> x2a - a) \<and> (src - a \<noteq> 0x40 \<longrightarrow> (src - a = 0x30 \<longrightarrow> \<not> 2 ^ tcbBlockSizeBits \<le> x2a - a) \<and> (src - a \<noteq> 0x30 \<longrightarrow> (src - a = 0x20 \<longrightarrow> \<not> 2 ^ tcbBlockSizeBits \<le> x2a - a) \<and> (src - a \<noteq> 0x20 \<longrightarrow> (src = a \<longrightarrow> \<not> 2 ^ tcbBlockSizeBits \<le> x2 - a) \<and> (src \<noteq> a \<longrightarrow> src - a = 0x10 \<longrightarrow> \<not> 2 ^ tcbBlockSizeBits \<le> x2a - a))))) \<and> (\<not> x2a - a < 2 ^ tcbBlockSizeBits \<longrightarrow> snd (lookupAround2 src (ksPSpace s)) = Some x2a \<longrightarrow> a && mask tcbBlockSizeBits = 0 \<longrightarrow> (src - a = 0x40 \<longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2a - a) \<and> (src - a \<noteq> 0x40 \<longrightarrow> (src - a = 0x30 \<longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2a - a) \<and> (src - a \<noteq> 0x30 \<longrightarrow> (src - a = 0x20 \<longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2a - a) \<and> (src - a \<noteq> 0x20 \<longrightarrow> (src = a \<longrightarrow> \<not> 2 ^ tcbBlockSizeBits \<le> x2 - a) \<and> (src \<noteq> a \<longrightarrow> src - a = 0x10 \<longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2a - a))))))) \<and> (\<not> x2 - a < 2 ^ tcbBlockSizeBits \<longrightarrow> snd (lookupAround2 a (ksPSpace s)) = Some x2 \<longrightarrow> (snd (lookupAround2 src (ksPSpace s)) = None \<longrightarrow> a && mask tcbBlockSizeBits = 0 \<longrightarrow> src - a \<noteq> 0x40 \<longrightarrow> src - a \<noteq> 0x30 \<longrightarrow> src - a \<noteq> 0x20 \<longrightarrow> src = a \<longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a) \<and> (\<forall>x2a. (x2a - a < 2 ^ tcbBlockSizeBits \<longrightarrow> snd (lookupAround2 src (ksPSpace s)) = Some x2a \<longrightarrow> a && mask tcbBlockSizeBits = 0 \<longrightarrow> (src - a = 0x40 \<longrightarrow> \<not> 2 ^ tcbBlockSizeBits \<le> x2a - a) \<and> (src - a \<noteq> 0x40 \<longrightarrow> (src - a = 0x30 \<longrightarrow> \<not> 2 ^ tcbBlockSizeBits \<le> x2a - a) \<and> (src - a \<noteq> 0x30 \<longrightarrow> (src - a = 0x20 \<longrightarrow> \<not> 2 ^ tcbBlockSizeBits \<le> x2a - a) \<and> (src - a \<noteq> 0x20 \<longrightarrow> (src = a \<longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a) \<and> (src \<noteq> a \<longrightarrow> src - a = 0x10 \<longrightarrow> \<not> 2 ^ tcbBlockSizeBits \<le> x2a - a))))) \<and> (\<not> x2a - a < 2 ^ tcbBlockSizeBits \<longrightarrow> snd (lookupAround2 src (ksPSpace s)) = Some x2a \<longrightarrow> a && mask tcbBlockSizeBits = 0 \<longrightarrow> (src - a = 0x40 \<longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2a - a) \<and> (src - a \<noteq> 0x40 \<longrightarrow> (src - a = 0x30 \<longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2a - a) \<and> (src - a \<noteq> 0x30 \<longrightarrow> (src - a = 0x20 \<longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2a - a) \<and> (src - a \<noteq> 0x20 \<longrightarrow> (src = a \<longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a) \<and> (src \<noteq> a \<longrightarrow> src - a = 0x10 \<longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2a - a))))))))
 2. \<And>a b x7. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOCTE x7); b = KOCTE x7\<rbrakk> \<Longrightarrow> (\<exists>cte. fst ((do y <- unless (src = a) fail;
y <- alignCheck src (objBits x7);
y <- magnitudeCheck src (snd (lookupAround2 src (ksPSpace s))) (objBits x7);
return x7
od) s) = {(cte, s)}) = cte_check (KOCTE x7) src a (snd (lookupAround2 src (ksPSpace s)))
 3. \<And>a b x8. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOArch x8); b = KOArch x8\<rbrakk> \<Longrightarrow> (\<exists>cte. fst (typeError [] (KOArch x8) s) = {(cte, s)}) = cte_check (KOArch x8) src a (snd (lookupAround2 src (ksPSpace s))) proof (prove)
goal (2 subgoals):
 1. \<And>a b x7. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOCTE x7); b = KOCTE x7\<rbrakk> \<Longrightarrow> (\<exists>cte. fst ((do y <- unless (src = a) fail;
y <- alignCheck src (objBits x7);
y <- magnitudeCheck src (snd (lookupAround2 src (ksPSpace s))) (objBits x7);
return x7
od) s) = {(cte, s)}) = cte_check (KOCTE x7) src a (snd (lookupAround2 src (ksPSpace s)))
 2. \<And>a b x8. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOArch x8); b = KOArch x8\<rbrakk> \<Longrightarrow> (\<exists>cte. fst (typeError [] (KOArch x8) s) = {(cte, s)}) = cte_check (KOArch x8) src a (snd (lookupAround2 src (ksPSpace s))) proof (prove)
goal (2 subgoals):
 1. \<And>a x7. fst (lookupAround2 src (ksPSpace s)) = Some (a, KOCTE x7) \<Longrightarrow> (\<exists>cte. fst ((do y <- unless (src = a) fail;
y <- alignCheck src (objBits x7);
y <- magnitudeCheck src (snd (lookupAround2 src (ksPSpace s))) (objBits x7);
return x7
od) s) = {(cte, s)}) = (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))
 2. \<And>a b x8. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOArch x8); b = KOArch x8\<rbrakk> \<Longrightarrow> (\<exists>cte. fst (typeError [] (KOArch x8) s) = {(cte, s)}) = cte_check (KOArch x8) src a (snd (lookupAround2 src (ksPSpace s))) proof (prove)
goal (2 subgoals):
 1. \<And>a x7. fst (lookupAround2 src (ksPSpace s)) = Some (a, KOCTE x7) \<Longrightarrow> \<forall>x2. (x2 - a < 2 ^ cteSizeBits \<longrightarrow> snd (lookupAround2 a (ksPSpace s)) = Some x2 \<longrightarrow> a && mask cteSizeBits = 0 \<longrightarrow> src = a \<longrightarrow> \<not> 2 ^ cteSizeBits \<le> x2 - a) \<and> (\<not> x2 - a < 2 ^ cteSizeBits \<longrightarrow> snd (lookupAround2 a (ksPSpace s)) = Some x2 \<longrightarrow> a && mask cteSizeBits = 0 \<longrightarrow> src = a \<longrightarrow> 2 ^ cteSizeBits \<le> x2 - a)
 2. \<And>a b x8. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOArch x8); b = KOArch x8\<rbrakk> \<Longrightarrow> (\<exists>cte. fst (typeError [] (KOArch x8) s) = {(cte, s)}) = cte_check (KOArch x8) src a (snd (lookupAround2 src (ksPSpace s))) proof (prove)
goal (1 subgoal):
 1. \<And>a b x8. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, KOArch x8); b = KOArch x8\<rbrakk> \<Longrightarrow> (\<exists>cte. fst (typeError [] (KOArch x8) s) = {(cte, s)}) = cte_check (KOArch x8) src a (snd (lookupAround2 src (ksPSpace s))) proof (prove)
goal:
No subgoals!