theory Move_C

lemma asUser_threadGet_tcbFault_comm:
  "empty_fail im \<Longrightarrow>
   do y \<leftarrow> asUser t im;
      x \<leftarrow> threadGet tcbFault t';
      n x y
   od =
   do x \<leftarrow> threadGet tcbFault t';
      asUser t im >>= n x
   od" apply (rule submonad_comm2 [OF tcbFault_submonad_args
                                 threadGet_tcbFault_submonad_fn
                                 submonad_asUser, symmetric]) apply (clarsimp simp: thread_replace_def asUser_replace_def Let_def
                     split: option.split) apply (clarsimp simp: fun_upd_idem fun_upd_twist
                     split: kernel_object.split) apply (rename_tac tcb) apply (case_tac tcb, simp) apply (clarsimp simp: asUser_replace_def Let_def obj_at'_real_def
                           ko_wp_at'_def ps_clear_upd_None ps_clear_upd
                           objBitsKO_def projectKOs
                    split: option.split kernel_object.split) apply (clarsimp simp: thread_replace_def Let_def obj_at'_real_def
                          ko_wp_at'_def ps_clear_upd_None
                          ps_clear_upd objBitsKO_def projectKOs
                   split: option.split kernel_object.split) apply (simp add: get_def empty_fail_def) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail im \<Longrightarrow> do y <- asUser t im;
x <- threadGet tcbFault t';
n x y
od = do x <- threadGet tcbFault t';
asUser t im >>= n x
od proof (prove)
goal (5 subgoals):
 1. \<And>s x x'. empty_fail im \<Longrightarrow> thread_replace tcbFault_update t' x (asUser_replace t x' s) = asUser_replace t x' (thread_replace tcbFault_update t' x s)
 2. \<And>s x. empty_fail im \<Longrightarrow> tcb_at' t' (asUser_replace t x s) = tcb_at' t' s
 3. \<And>s x. empty_fail im \<Longrightarrow> tcb_at' t (thread_replace tcbFault_update t' x s) = tcb_at' t s
 4. empty_fail im \<Longrightarrow> empty_fail get
 5. empty_fail im \<Longrightarrow> empty_fail im proof (prove)
goal (5 subgoals):
 1. \<And>s x x' x2. empty_fail im \<Longrightarrow> ((case x2 of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object)) = None \<longrightarrow> ksPSpace s t' = Some x2 \<longrightarrow> ((case x2 of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbFault_update (\<lambda>_. x) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object)) = None \<longrightarrow> (\<forall>x2. ksPSpace s t = Some x2 \<longrightarrow> t \<noteq> t' \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t := case x2 of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object), t' := None)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t' := None, t := case x2 of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object))\<rparr>)) \<and> (\<forall>x2a. (case x2 of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbFault_update (\<lambda>_. x) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object)) = Some x2a \<longrightarrow> (ksPSpace s t = None \<longrightarrow> t = t' \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t' := None)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t' := case x2a of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object))\<rparr>) \<and> (\<forall>x2. ksPSpace s t = Some x2 \<longrightarrow> (t = t' \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t' := None)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t' := case x2a of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object))\<rparr>) \<and> (t \<noteq> t' \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t := case x2 of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object), t' \<mapsto> x2a)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> x2a, t := case x2 of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object))\<rparr>)))) \<and> (\<forall>x2a. (case x2 of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object)) = Some x2a \<longrightarrow> ksPSpace s t' = Some x2 \<longrightarrow> ((case x2 of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbFault_update (\<lambda>_. x) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object)) = None \<longrightarrow> (ksPSpace s t = None \<longrightarrow> t = t' \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t' := case x2a of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbFault_update (\<lambda>_. x) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t' := None)\<rparr>) \<and> (\<forall>x2. ksPSpace s t = Some x2 \<longrightarrow> (t = t' \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t' := case x2a of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbFault_update (\<lambda>_. x) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t' := None)\<rparr>) \<and> (t \<noteq> t' \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t := case x2 of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object), t' := None)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t' := None, t := case x2 of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object))\<rparr>))) \<and> (\<forall>x2b. (case x2 of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbFault_update (\<lambda>_. x) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object)) = Some x2b \<longrightarrow> (ksPSpace s t = None \<longrightarrow> t = t' \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t' := case x2a of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbFault_update (\<lambda>_. x) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t' := case x2b of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object))\<rparr>) \<and> (\<forall>x2. ksPSpace s t = Some x2 \<longrightarrow> (t = t' \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t' := case x2a of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbFault_update (\<lambda>_. x) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t' := case x2b of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object))\<rparr>) \<and> (t \<noteq> t' \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t := case x2 of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object), t' \<mapsto> x2b)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> x2b, t := case x2 of KOEndpoint endpoint \<Rightarrow> Some (KOEndpoint endpoint) | KONotification notification \<Rightarrow> Some (KONotification notification) | KOKernelData \<Rightarrow> Some KOKernelData | KOUserData \<Rightarrow> Some KOUserData | KOUserDataDevice \<Rightarrow> Some KOUserDataDevice | KOTCB tcb \<Rightarrow> Some (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) tcb)) | KOCTE cte \<Rightarrow> Some (KOCTE cte) | KOArch arch_kernel_object \<Rightarrow> Some (KOArch arch_kernel_object))\<rparr>))))
 2. \<And>s x. empty_fail im \<Longrightarrow> tcb_at' t' (asUser_replace t x s) = tcb_at' t' s
 3. \<And>s x. empty_fail im \<Longrightarrow> tcb_at' t (thread_replace tcbFault_update t' x s) = tcb_at' t s
 4. empty_fail im \<Longrightarrow> empty_fail get
 5. empty_fail im \<Longrightarrow> empty_fail im proof (prove)
goal (5 subgoals):
 1. \<And>s x x' x6. \<lbrakk>empty_fail im; ksPSpace s t' = Some (KOTCB x6); t = t'\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbFault_update (\<lambda>_. x) (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch x6)) x6)))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch x6)) (tcbFault_update (\<lambda>_. x) x6)))\<rparr>
 2. \<And>s x. empty_fail im \<Longrightarrow> tcb_at' t' (asUser_replace t x s) = tcb_at' t' s
 3. \<And>s x. empty_fail im \<Longrightarrow> tcb_at' t (thread_replace tcbFault_update t' x s) = tcb_at' t s
 4. empty_fail im \<Longrightarrow> empty_fail get
 5. empty_fail im \<Longrightarrow> empty_fail im proof (prove)
goal (5 subgoals):
 1. \<And>s x x' tcb. \<lbrakk>empty_fail im; ksPSpace s t' = Some (KOTCB tcb); t = t'\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbFault_update (\<lambda>_. x) (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) tcb)))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x' (tcbArch tcb)) (tcbFault_update (\<lambda>_. x) tcb)))\<rparr>
 2. \<And>s x. empty_fail im \<Longrightarrow> tcb_at' t' (asUser_replace t x s) = tcb_at' t' s
 3. \<And>s x. empty_fail im \<Longrightarrow> tcb_at' t (thread_replace tcbFault_update t' x s) = tcb_at' t s
 4. empty_fail im \<Longrightarrow> empty_fail get
 5. empty_fail im \<Longrightarrow> empty_fail im proof (prove)
goal (4 subgoals):
 1. \<And>s x. empty_fail im \<Longrightarrow> tcb_at' t' (asUser_replace t x s) = tcb_at' t' s
 2. \<And>s x. empty_fail im \<Longrightarrow> tcb_at' t (thread_replace tcbFault_update t' x s) = tcb_at' t s
 3. empty_fail im \<Longrightarrow> empty_fail get
 4. empty_fail im \<Longrightarrow> empty_fail im proof (prove)
goal (3 subgoals):
 1. \<And>s x. empty_fail im \<Longrightarrow> tcb_at' t (thread_replace tcbFault_update t' x s) = tcb_at' t s
 2. empty_fail im \<Longrightarrow> empty_fail get
 3. empty_fail im \<Longrightarrow> empty_fail im proof (prove)
goal (2 subgoals):
 1. empty_fail im \<Longrightarrow> empty_fail get
 2. empty_fail im \<Longrightarrow> empty_fail im proof (prove)
goal (1 subgoal):
 1. empty_fail im \<Longrightarrow> empty_fail im proof (prove)
goal:
No subgoals!