theory IsolatedThreadAction

lemma getObject_isolatable:
  "\<lbrakk> \<And>a b c d. (loadObject a b c d :: 'a kernel) = loadObject_default a b c d;
      \<And>tcb. projectKO_opt (KOTCB tcb) = (None :: 'a option) \<rbrakk> \<Longrightarrow>
   thread_actions_isolatable idx (getObject p :: ('a :: pspace_storable) kernel)" apply (clarsimp simp: thread_actions_isolatable_def) apply (simp add: getObject_get_assert split_def
                   isolate_thread_actions_def bind_select_f_bind[symmetric]
                   bind_assoc select_f_asserts select_f_returns) apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def) apply (case_tac "p \<in> range idx") apply clarsimp apply (drule_tac x=x in spec) apply (clarsimp simp: obj_at'_def projectKOs partial_overwrite_def
                         put_tcb_state_regs_def) apply (simp add: obj_at_partial_overwrite_id1) apply (simp add: partial_overwrite_def) apply (rule bind_apply_cong[OF refl]) apply (simp add: exec_modify return_def o_def simpler_gets_def
                   ksPSpace_update_partial_id in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a b c d. loadObject a b c d = loadObject_default a b c d; \<And>tcb. projectKO_opt (KOTCB tcb) = None\<rbrakk> \<Longrightarrow> thread_actions_isolatable idx (getObject p) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a b c d. loadObject a b c d = loadObject_default a b c d; \<And>tcb. projectKO_opt (KOTCB tcb) = None; inj idx\<rbrakk> \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (getObject p) (isolate_thread_actions idx (getObject p) id id) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a b c d. loadObject a b c d = loadObject_default a b c d; \<And>tcb. projectKO_opt (KOTCB tcb) = None; inj idx\<rbrakk> \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (do v <- gets (obj_at' (\<lambda>x. True) p);
y <- assert v;
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) (do s <- gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)));
tcbs <- gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx);
sa <- getSchedulerAction;
y <- assert (obj_at' (\<lambda>x. True) p s);
y <- modify (\<lambda>sb. ksPSpace_update (partial_overwrite idx tcbs) (s\<lparr>ksSchedulerAction := sa\<rparr>));
return (the (projectKO_opt (the (ksPSpace s p))))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>a b c d. loadObject a b c d = loadObject_default a b c d; \<And>tcb. projectKO_opt (KOTCB tcb) = None; inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (do y <- assert (obj_at' (\<lambda>x. True) p s);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) s = (do y <- assert (obj_at' (\<lambda>x. True) p (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s));
y <- modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s);
return (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) p))))
od) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>a b c d. loadObject a b c d = loadObject_default a b c d; \<And>tcb. projectKO_opt (KOTCB tcb) = None; inj idx; \<forall>x. tcb_at' (idx x) s; p \<in> range idx\<rbrakk> \<Longrightarrow> (do y <- assert (obj_at' (\<lambda>x. True) p s);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) s = (do y <- assert (obj_at' (\<lambda>x. True) p (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s));
y <- modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s);
return (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) p))))
od) s
 2. \<And>s. \<lbrakk>\<And>a b c d. loadObject a b c d = loadObject_default a b c d; \<And>tcb. projectKO_opt (KOTCB tcb) = None; inj idx; \<forall>x. tcb_at' (idx x) s; p \<notin> range idx\<rbrakk> \<Longrightarrow> (do y <- assert (obj_at' (\<lambda>x. True) p s);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) s = (do y <- assert (obj_at' (\<lambda>x. True) p (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s));
y <- modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s);
return (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) p))))
od) s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>\<And>a b c d. loadObject a b c d = loadObject_default a b c d; \<And>tcb. projectKO_opt (KOTCB tcb) = None; inj idx; \<forall>x. tcb_at' (idx x) s; p = idx x\<rbrakk> \<Longrightarrow> (do y <- assert (obj_at' (\<lambda>x. True) (idx x) s);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) (idx x) \<circ> ksPSpace)
od) s = (do y <- assert (obj_at' (\<lambda>x. True) (idx x) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s));
y <- modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s);
return (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) (idx x)))))
od) s
 2. \<And>s. \<lbrakk>\<And>a b c d. loadObject a b c d = loadObject_default a b c d; \<And>tcb. projectKO_opt (KOTCB tcb) = None; inj idx; \<forall>x. tcb_at' (idx x) s; p \<notin> range idx\<rbrakk> \<Longrightarrow> (do y <- assert (obj_at' (\<lambda>x. True) p s);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) s = (do y <- assert (obj_at' (\<lambda>x. True) p (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s));
y <- modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s);
return (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) p))))
od) s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>\<And>a b c d. loadObject a b c d = loadObject_default a b c d; \<And>tcb. projectKO_opt (KOTCB tcb) = None; inj idx; p = idx x; tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (do y <- assert (obj_at' (\<lambda>x. True) (idx x) s);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) (idx x) \<circ> ksPSpace)
od) s = (do y <- assert (obj_at' (\<lambda>x. True) (idx x) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s));
y <- modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s);
return (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) (idx x)))))
od) s
 2. \<And>s. \<lbrakk>\<And>a b c d. loadObject a b c d = loadObject_default a b c d; \<And>tcb. projectKO_opt (KOTCB tcb) = None; inj idx; \<forall>x. tcb_at' (idx x) s; p \<notin> range idx\<rbrakk> \<Longrightarrow> (do y <- assert (obj_at' (\<lambda>x. True) p s);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) s = (do y <- assert (obj_at' (\<lambda>x. True) p (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s));
y <- modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s);
return (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) p))))
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>a b c d. loadObject a b c d = loadObject_default a b c d; \<And>tcb. projectKO_opt (KOTCB tcb) = None; inj idx; \<forall>x. tcb_at' (idx x) s; p \<notin> range idx\<rbrakk> \<Longrightarrow> (do y <- assert (obj_at' (\<lambda>x. True) p s);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) s = (do y <- assert (obj_at' (\<lambda>x. True) p (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s));
y <- modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s);
return (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) p))))
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>a b c d. loadObject a b c d = loadObject_default a b c d; \<And>tcb. projectKO_opt (KOTCB tcb) = None; inj idx; \<forall>x. tcb_at' (idx x) s; p \<notin> range idx\<rbrakk> \<Longrightarrow> (do y <- assert (obj_at' (\<lambda>x. True) p s);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) s = (do y <- assert (obj_at' (\<lambda>x. True) p s);
y <- modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s);
return (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) p))))
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>a b c d. loadObject a b c d = loadObject_default a b c d; \<And>tcb. projectKO_opt (KOTCB tcb) = None; inj idx; \<forall>x. tcb_at' (idx x) s; p \<notin> range idx\<rbrakk> \<Longrightarrow> (do y <- assert (obj_at' (\<lambda>x. True) p s);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) s = (do y <- assert (obj_at' (\<lambda>x. True) p s);
y <- modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s);
return (the (projectKO_opt (the (ksPSpace s p))))
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s rv st. \<lbrakk>\<And>a b c d. loadObject a b c d = loadObject_default a b c d; \<And>tcb. projectKO_opt (KOTCB tcb) = None; inj idx; \<forall>x. tcb_at' (idx x) s; p \<notin> range idx; (rv, st) \<in> fst (assert (obj_at' (\<lambda>x. True) p s) s)\<rbrakk> \<Longrightarrow> gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace) st = (do y <- modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s);
return (the (projectKO_opt (the (ksPSpace s p))))
od) st proof (prove)
goal:
No subgoals!