theory CSpace_R

lemma setCTE_ksMachine[wp]:
  "\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> setCTE x y \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>" apply (clarsimp simp: setCTE_def) apply (wp setObject_ksMachine) apply (clarsimp simp: updateObject_cte
                 split: Structures_H.kernel_object.splits) apply (safe, (wp unless_wp | simp)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> setCTE x y \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> setObject x y \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>p q n ko. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> updateObject y p q n ko \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>
 2. \<And>s. P (ksMachineState s) \<Longrightarrow> P (ksMachineState s) proof (prove)
goal (2 subgoals):
 1. \<And>p q n ko. (\<forall>x1. p = KOEndpoint x1 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> typeError [] (KOEndpoint x1) \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (\<forall>x2. p = KONotification x2 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> typeError [] (KONotification x2) \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (p = KOKernelData \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> typeError [] KOKernelData \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (p = KOUserData \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> typeError [] KOUserData \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (p = KOUserDataDevice \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> typeError [] KOUserDataDevice \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (\<forall>x6. (q - n = 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> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>)) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbReply_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>)) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbCaller_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>)))) \<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> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>)) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbReply_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>))) \<and> (tcbIPCBufferSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (tcbIPCBufferSlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>)) \<and> (tcbIPCBufferSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbIPCBufferSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (tcbIPCBufferSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>))))) \<and> (q - n \<noteq> tcbIPCBufferSlot << objBits undefined \<longrightarrow> (q - n = 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> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>)) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbReply_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>)) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbCaller_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>)))) \<and> (q - n \<noteq> tcbCallerSlot << objBits undefined \<longrightarrow> (q - n = tcbReplySlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>)) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbReply_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>))) \<and> (q - n \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (q - n = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbCTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>)) \<and> (q - n \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (q - n = tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- alignCheck n (objBits x6);
ya <- magnitudeCheck n ko (objBits x6);
return (KOTCB (tcbVTable_update (\<lambda>_. y) x6))
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (q - n \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> p = KOTCB x6 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do y <- alignCheck n (objBits x6);
y <- magnitudeCheck n ko (objBits x6);
fail
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>)))))) \<and> ((\<exists>x7. p = KOCTE x7) \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ya <- unless (q = n) fail;
ya <- alignCheck q (objBits y);
ya <- magnitudeCheck q ko (objBits y);
return (KOCTE y)
od \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>) \<and> (\<forall>x8. p = KOArch x8 \<longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> typeError [] (KOArch x8) \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>)
 2. \<And>s. P (ksMachineState s) \<Longrightarrow> P (ksMachineState s) proof (prove)
goal:
No subgoals!