theory Detype_R

lemma simpler_updateObject_def:
  "updateObject (cte::cte) b src a next =
   (\<lambda>s. (if (cte_check b src a next) then ({(cte_update cte b src a,s)}, False)
         else fail s))" apply (rule ext) apply (clarsimp simp:ObjectInstances_H.updateObject_cte objBits_simps) apply (case_tac b) apply (simp_all add:cte_check_def typeError_def fail_def
          tcbIPCBufferSlot_def
          tcbCallerSlot_def tcbReplySlot_def
          tcbCTableSlot_def tcbVTableSlot_def) by (intro conjI impI;
        clarsimp simp:alignCheck_def unless_def when_def not_less[symmetric]
         alignError_def is_aligned_mask magnitudeCheck_def
         cte_update_def return_def tcbIPCBufferSlot_def
         tcbCallerSlot_def tcbReplySlot_def
         tcbCTableSlot_def tcbVTableSlot_def objBits_simps
         cteSizeBits_def split:option.splits;
          fastforce simp:return_def fail_def bind_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. updateObject cte b src a next = (\<lambda>s. if cte_check b src a next then ({(cte_update cte b src a, s)}, False) else fail s) proof (prove)
goal (1 subgoal):
 1. \<And>s. updateObject cte b src a next s = (if cte_check b src a next then ({(cte_update cte b src a, s)}, False) else fail s) proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = ({(cte_update cte b src a, s)}, False)) \<and> (\<not> cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = fail s) proof (prove)
goal (8 subgoals):
 1. \<And>s x1. b = KOEndpoint x1 \<Longrightarrow> (cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = ({(cte_update cte b src a, s)}, False)) \<and> (\<not> cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = fail s)
 2. \<And>s x2. b = KONotification x2 \<Longrightarrow> (cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = ({(cte_update cte b src a, s)}, False)) \<and> (\<not> cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = fail s)
 3. \<And>s. b = KOKernelData \<Longrightarrow> (cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = ({(cte_update cte b src a, s)}, False)) \<and> (\<not> cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = fail s)
 4. \<And>s. b = KOUserData \<Longrightarrow> (cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = ({(cte_update cte b src a, s)}, False)) \<and> (\<not> cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = fail s)
 5. \<And>s. b = KOUserDataDevice \<Longrightarrow> (cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = ({(cte_update cte b src a, s)}, False)) \<and> (\<not> cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = fail s)
 6. \<And>s x6. b = KOTCB x6 \<Longrightarrow> (cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = ({(cte_update cte b src a, s)}, False)) \<and> (\<not> cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = fail s)
 7. \<And>s x7. b = KOCTE x7 \<Longrightarrow> (cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = ({(cte_update cte b src a, s)}, False)) \<and> (\<not> cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = fail s)
 8. \<And>s x8. b = KOArch x8 \<Longrightarrow> (cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = ({(cte_update cte b src a, s)}, False)) \<and> (\<not> cte_check b src a next \<longrightarrow> (case b of KOTCB tcb \<Rightarrow> do alignCheck a (objBits tcb);
magnitudeCheck a next (objBits tcb);
if src - a = tcbVTableSlot << cteSizeBits then return $ KOTCB (tcbVTable_update (\<lambda>_. cte) tcb) else if src - a = tcbCTableSlot << cteSizeBits then return $ KOTCB (tcbCTable_update (\<lambda>_. cte) tcb) else if src - a = tcbReplySlot << cteSizeBits then return $ KOTCB (tcbReply_update (\<lambda>_. cte) tcb) else if src - a = tcbCallerSlot << cteSizeBits then return $ KOTCB (tcbCaller_update (\<lambda>_. cte) tcb) else if src - a = tcbIPCBufferSlot << cteSizeBits then return $ KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb) else haskell_fail []
od | KOCTE v3 \<Rightarrow> do unless (src = a) $ haskell_fail [];
alignCheck src (objBits cte);
magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] b) s = fail s) proof (prove)
goal (2 subgoals):
 1. \<And>s x6. b = KOTCB x6 \<Longrightarrow> (src - a = 4 << cteSizeBits \<longrightarrow> (4 << cteSizeBits = 3 << cteSizeBits \<longrightarrow> (3 << cteSizeBits = 2 << cteSizeBits \<longrightarrow> (src = a \<longrightarrow> (32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (\<not> 32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({}, True)))) \<and> (src \<noteq> a \<longrightarrow> (2 << cteSizeBits = 2 ^ cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) src a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (2 << cteSizeBits \<noteq> 2 ^ cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbReply_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) src a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbReply_update (\<lambda>_. cte) x6))
od) s = ({}, True))))) \<and> (3 << cteSizeBits \<noteq> 2 << cteSizeBits \<longrightarrow> (src = a \<longrightarrow> (32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (\<not> 32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({}, True)))) \<and> (src \<noteq> a \<longrightarrow> (3 << cteSizeBits = 2 ^ cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) src a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (3 << cteSizeBits \<noteq> 2 ^ cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCaller_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) src a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCaller_update (\<lambda>_. cte) x6))
od) s = ({}, True)))))) \<and> (4 << cteSizeBits \<noteq> 3 << cteSizeBits \<longrightarrow> (4 << cteSizeBits = 2 << cteSizeBits \<longrightarrow> (src = a \<longrightarrow> (32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (\<not> 32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({}, True)))) \<and> (src \<noteq> a \<longrightarrow> (2 << cteSizeBits = 2 ^ cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) src a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (2 << cteSizeBits \<noteq> 2 ^ cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbReply_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) src a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbReply_update (\<lambda>_. cte) x6))
od) s = ({}, True))))) \<and> (4 << cteSizeBits \<noteq> 2 << cteSizeBits \<longrightarrow> (src = a \<longrightarrow> (32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (\<not> 32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({}, True)))) \<and> (src \<noteq> a \<longrightarrow> (4 << cteSizeBits = 2 ^ cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) src a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (4 << cteSizeBits \<noteq> 2 ^ cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) src a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) x6))
od) s = ({}, True))))))) \<and> (src - a \<noteq> 4 << cteSizeBits \<longrightarrow> (src - a = 3 << cteSizeBits \<longrightarrow> (3 << cteSizeBits = 2 << cteSizeBits \<longrightarrow> (src = a \<longrightarrow> (32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (\<not> 32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({}, True)))) \<and> (src \<noteq> a \<longrightarrow> (2 << cteSizeBits = 2 ^ cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) src a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (2 << cteSizeBits \<noteq> 2 ^ cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbReply_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) src a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbReply_update (\<lambda>_. cte) x6))
od) s = ({}, True))))) \<and> (3 << cteSizeBits \<noteq> 2 << cteSizeBits \<longrightarrow> (src = a \<longrightarrow> (32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (\<not> 32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({}, True)))) \<and> (src \<noteq> a \<longrightarrow> (3 << cteSizeBits = 2 ^ cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) src a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (3 << cteSizeBits \<noteq> 2 ^ cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCaller_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) src a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCaller_update (\<lambda>_. cte) x6))
od) s = ({}, True)))))) \<and> (src - a \<noteq> 3 << cteSizeBits \<longrightarrow> (src - a = 2 << cteSizeBits \<longrightarrow> (src = a \<longrightarrow> (32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (\<not> 32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({}, True)))) \<and> (src \<noteq> a \<longrightarrow> (2 << cteSizeBits = 2 ^ cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) src a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (2 << cteSizeBits \<noteq> 2 ^ cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbReply_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) src a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbReply_update (\<lambda>_. cte) x6))
od) s = ({}, True))))) \<and> (src - a \<noteq> 2 << cteSizeBits \<longrightarrow> (src = a \<longrightarrow> (32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (\<not> 32 \<le> cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) a a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6))
od) s = ({}, True)))) \<and> (src \<noteq> a \<longrightarrow> (src - a = 2 ^ cteSizeBits \<longrightarrow> (is_aligned a (objBits x6) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({(cte_update cte (KOTCB x6) src a, s)}, False)) \<and> (((case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - a) \<longrightarrow> \<not> is_aligned a (objBits x6)) \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6))
od) s = ({}, True))) \<and> (src - a \<noteq> 2 ^ cteSizeBits \<longrightarrow> (do y <- alignCheck a (objBits x6);
y <- magnitudeCheck a next (objBits x6);
\<lambda>s. ({}, True)
od) s = ({}, True))))))
 2. \<And>s x7. b = KOCTE x7 \<Longrightarrow> (src = a \<and> is_aligned a (objBits makeObject) \<and> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits makeObject \<le> z - a) \<longrightarrow> (do y <- alignCheck a (objBits cte);
y <- magnitudeCheck a next (objBits cte);
return (KOCTE cte)
od) s = ({(cte_update cte (KOCTE x7) a a, s)}, False)) \<and> ((is_aligned a (objBits makeObject) \<longrightarrow> src = a \<longrightarrow> \<not> (case next of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits makeObject \<le> z - a)) \<longrightarrow> (do y <- unless (src = a) (\<lambda>s. ({}, True));
y <- alignCheck src (objBits cte);
y <- magnitudeCheck src next (objBits cte);
return (KOCTE cte)
od) s = ({}, True))