theory IsolatedThreadAction

lemma getObject_get_assert:
  assumes deflt: "\<And>a b c d. (loadObject a b c d :: ('a :: pspace_storable) kernel)
                          = loadObject_default a b c d"
  shows
  "(getObject p :: ('a :: pspace_storable) kernel)
   = do v \<leftarrow> gets (obj_at' (\<lambda>x :: 'a. True) p);
        assert v;
        gets (the o projectKO_opt o the o swp fun_app p o ksPSpace)
     od" apply (rule ext) apply (simp add: exec_get getObject_def split_def exec_gets
                   deflt loadObject_default_def projectKO_def2
                   alignCheck_assert) apply (case_tac "ksPSpace x p") apply (simp add: obj_at'_def assert_opt_def assert_def
             split: option.split if_split) apply (simp add: lookupAround2_known1 assert_opt_def
                   obj_at'_def projectKO_def2
            split: option.split) apply (rule conjI) apply (clarsimp simp: fail_def fst_return conj_comms project_inject
                         objBits_def bind_def simpler_gets_def) apply (clarsimp simp: fail_def fst_return conj_comms project_inject
                        objBits_def) apply (simp only: assert2[symmetric],
         rule bind_apply_cong[OF refl]) apply (clarsimp simp: in_monad) apply (fold objBits_def) apply (simp add: magnitudeCheck_assert2[OF _ objBits_2n]) apply (rule bind_apply_cong[OF refl]) apply (clarsimp simp: in_monad return_def simpler_gets_def) apply (simp add: iffD2[OF project_inject refl]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. getObject p = do v <- gets (obj_at' (\<lambda>x. True) p);
assert v;
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od proof (prove)
goal (1 subgoal):
 1. \<And>x. getObject p x = (do v <- gets (obj_at' (\<lambda>x. True) p);
assert v;
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
y <- assert (p = fst pa);
val <- assert_opt (projectKO_opt (snd pa));
y <- assert (is_aligned p (objBits val));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits val);
return val
od) x = (do y <- assert (obj_at' (\<lambda>x. True) p x);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) x proof (prove)
goal (2 subgoals):
 1. \<And>x. ksPSpace x p = None \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
y <- assert (p = fst pa);
val <- assert_opt (projectKO_opt (snd pa));
y <- assert (is_aligned p (objBits val));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits val);
return val
od) x = (do y <- assert (obj_at' (\<lambda>x. True) p x);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) x
 2. \<And>x a. ksPSpace x p = Some a \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
y <- assert (p = fst pa);
val <- assert_opt (projectKO_opt (snd pa));
y <- assert (is_aligned p (objBits val));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits val);
return val
od) x = (do y <- assert (obj_at' (\<lambda>x. True) p x);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x a. ksPSpace x p = Some a \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
y <- assert (p = fst pa);
val <- assert_opt (projectKO_opt (snd pa));
y <- assert (is_aligned p (objBits val));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits val);
return val
od) x = (do y <- assert (obj_at' (\<lambda>x. True) p x);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x a. ksPSpace x p = Some a \<Longrightarrow> (projectKO_opt a = None \<longrightarrow> fail x = (do y <- assert (is_aligned p (objBitsKO a) \<and> (\<exists>obj. fst (fail x) = {(obj, x)}) \<and> ps_clear p (objBitsKO a) x);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) x) \<and> (\<forall>x2. projectKO_opt a = Some x2 \<longrightarrow> (do y <- assert (is_aligned p (objBits x2));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits x2);
return x2
od) x = (do y <- assert (is_aligned p (objBitsKO a) \<and> (\<exists>obj. fst (return x2 x) = {(obj, x)}) \<and> ps_clear p (objBitsKO a) x);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) x) proof (prove)
goal (2 subgoals):
 1. \<And>x a. ksPSpace x p = Some a \<Longrightarrow> projectKO_opt a = None \<longrightarrow> fail x = (do y <- assert (is_aligned p (objBitsKO a) \<and> (\<exists>obj. fst (fail x) = {(obj, x)}) \<and> ps_clear p (objBitsKO a) x);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) x
 2. \<And>x a. ksPSpace x p = Some a \<Longrightarrow> \<forall>x2. projectKO_opt a = Some x2 \<longrightarrow> (do y <- assert (is_aligned p (objBits x2));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits x2);
return x2
od) x = (do y <- assert (is_aligned p (objBitsKO a) \<and> (\<exists>obj. fst (return x2 x) = {(obj, x)}) \<and> ps_clear p (objBitsKO a) x);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x a. ksPSpace x p = Some a \<Longrightarrow> \<forall>x2. projectKO_opt a = Some x2 \<longrightarrow> (do y <- assert (is_aligned p (objBits x2));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits x2);
return x2
od) x = (do y <- assert (is_aligned p (objBitsKO a) \<and> (\<exists>obj. fst (return x2 x) = {(obj, x)}) \<and> ps_clear p (objBitsKO a) x);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x x2. ksPSpace x p = Some (injectKOS x2) \<Longrightarrow> (do y <- assert (is_aligned p (objBitsKO (injectKOS x2)));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBitsKO (injectKOS x2));
return x2
od) x = (do y <- assert (is_aligned p (objBitsKO (injectKOS x2)) \<and> ps_clear p (objBitsKO (injectKOS x2)) x);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x x2 rv st. \<lbrakk>ksPSpace x p = Some (injectKOS x2); (rv, st) \<in> fst (assert (is_aligned p (objBitsKO (injectKOS x2))) x)\<rbrakk> \<Longrightarrow> (do y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBitsKO (injectKOS x2));
return x2
od) st = (do v2 <- assert (ps_clear p (objBitsKO (injectKOS x2)) x);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) st proof (prove)
goal (1 subgoal):
 1. \<And>x x2. \<lbrakk>ksPSpace x p = Some (injectKOS x2); is_aligned p (objBitsKO (injectKOS x2))\<rbrakk> \<Longrightarrow> (do y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBitsKO (injectKOS x2));
return x2
od) x = (do v2 <- assert (ps_clear p (objBitsKO (injectKOS x2)) x);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x x2. \<lbrakk>ksPSpace x p = Some (injectKOS x2); is_aligned p (objBits x2)\<rbrakk> \<Longrightarrow> (do y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits x2);
return x2
od) x = (do v2 <- assert (ps_clear p (objBits x2) x);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x x2. \<lbrakk>ksPSpace x p = Some (injectKOS x2); is_aligned p (objBits x2)\<rbrakk> \<Longrightarrow> (do y <- assert (ps_clear p (objBits x2) x);
return x2
od) x = (do v2 <- assert (ps_clear p (objBits x2) x);
gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x x2 rv st. \<lbrakk>ksPSpace x p = Some (injectKOS x2); is_aligned p (objBits x2); (rv, st) \<in> fst (assert (ps_clear p (objBits x2) x) x)\<rbrakk> \<Longrightarrow> return x2 st = gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) p \<circ> ksPSpace) st proof (prove)
goal (1 subgoal):
 1. \<And>x x2. \<lbrakk>ksPSpace x p = Some (injectKOS x2); is_aligned p (objBits x2); ps_clear p (objBits x2) x\<rbrakk> \<Longrightarrow> x2 = the (projectKO_opt (injectKOS x2)) proof (prove)
goal:
No subgoals!