theory IsolatedThreadAction

lemma setObject_modify_assert:
  "\<lbrakk> updateObject v = updateObject_default v \<rbrakk>
    \<Longrightarrow> setObject p v = do f \<leftarrow> gets (obj_at' (\<lambda>v'. v = v' \<or> True) p);
                         assert f; modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKO v))) od" using objBits_2n[where obj=v] apply (simp add: setObject_def split_def updateObject_default_def
                   bind_assoc projectKO_def2 alignCheck_assert) apply (rule ext, simp add: exec_gets) apply (case_tac "obj_at' (\<lambda>v'. v = v' \<or> True) p x") apply (clarsimp simp: obj_at'_def projectKOs lookupAround2_known1
                         assert_opt_def) apply (clarsimp simp: project_inject) apply (simp only: objBits_def objBitsT_koTypeOf[symmetric] koTypeOf_injectKO) apply (simp add: magnitudeCheck_assert2 simpler_modify_def) apply (clarsimp simp: assert_opt_def assert_def magnitudeCheck_assert2
                 split: option.split if_split) apply (clarsimp simp: obj_at'_def projectKOs) apply (clarsimp simp: project_inject) apply (simp only: objBits_def objBitsT_koTypeOf[symmetric]
                    koTypeOf_injectKO simp_thms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. updateObject v = updateObject_default v \<Longrightarrow> setObject p v = do f <- gets (obj_at' (\<lambda>v'. v = v' \<or> True) p);
assert f;
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v)))
od proof (prove)
using this:
1 < 2 ^ objBits v

goal (1 subgoal):
 1. updateObject v = updateObject_default v \<Longrightarrow> setObject p v = do f <- gets (obj_at' (\<lambda>v'. v = v' \<or> True) p);
assert f;
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v)))
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBits v\<rbrakk> \<Longrightarrow> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
y <- assert (p = fst pa);
_ <- assert_opt (projectKO_opt (snd pa));
y <- assert (is_aligned p (objBits v));
y <- magnitudeCheck p (snd (lookupAround2 p ps)) (objBits v);
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> injectKOS v)))
od = do f <- gets (obj_at' (\<lambda>v'. True) p);
y <- assert f;
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v)))
od proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBits v\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
y <- assert (p = fst pa);
_ <- assert_opt (projectKO_opt (snd pa));
y <- assert (is_aligned p (objBits v));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits v);
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> injectKOS v)))
od) x = (do y <- assert (obj_at' (\<lambda>v'. True) p x);
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v)))
od) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBits v; obj_at' (\<lambda>v'. v = v' \<or> True) p x\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
y <- assert (p = fst pa);
_ <- assert_opt (projectKO_opt (snd pa));
y <- assert (is_aligned p (objBits v));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits v);
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> injectKOS v)))
od) x = (do y <- assert (obj_at' (\<lambda>v'. True) p x);
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v)))
od) x
 2. \<And>x. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBits v; \<not> obj_at' (\<lambda>v'. v = v' \<or> True) p x\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
y <- assert (p = fst pa);
_ <- assert_opt (projectKO_opt (snd pa));
y <- assert (is_aligned p (objBits v));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits v);
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> injectKOS v)))
od) x = (do y <- assert (obj_at' (\<lambda>v'. True) p x);
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v)))
od) x proof (prove)
goal (2 subgoals):
 1. \<And>x ko obj. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBits v; ksPSpace x p = Some ko; is_aligned p (objBitsKO ko); ps_clear p (objBitsKO ko) x; projectKO_opt ko = Some obj\<rbrakk> \<Longrightarrow> (do y <- assert (is_aligned p (objBits v));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits v);
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(p \<mapsto> injectKOS v)))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v))) x
 2. \<And>x. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBits v; \<not> obj_at' (\<lambda>v'. v = v' \<or> True) p x\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
y <- assert (p = fst pa);
_ <- assert_opt (projectKO_opt (snd pa));
y <- assert (is_aligned p (objBits v));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits v);
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> injectKOS v)))
od) x = (do y <- assert (obj_at' (\<lambda>v'. True) p x);
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v)))
od) x proof (prove)
goal (2 subgoals):
 1. \<And>x obj. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBits v; ksPSpace x p = Some (injectKOS obj); is_aligned p (objBitsKO (injectKOS obj)); ps_clear p (objBitsKO (injectKOS obj)) x\<rbrakk> \<Longrightarrow> (do y <- assert (is_aligned p (objBits v));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits v);
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(p \<mapsto> injectKOS v)))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v))) x
 2. \<And>x. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBits v; \<not> obj_at' (\<lambda>v'. v = v' \<or> True) p x\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
y <- assert (p = fst pa);
_ <- assert_opt (projectKO_opt (snd pa));
y <- assert (is_aligned p (objBits v));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits v);
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> injectKOS v)))
od) x = (do y <- assert (obj_at' (\<lambda>v'. True) p x);
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v)))
od) x proof (prove)
goal (2 subgoals):
 1. \<And>x obj. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBitsT (koType TYPE('a)); ksPSpace x p = Some (injectKOS obj); is_aligned p (objBitsT (koType TYPE('a))); ps_clear p (objBitsT (koType TYPE('a))) x\<rbrakk> \<Longrightarrow> (do y <- assert True;
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBitsT (koType TYPE('a)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(p \<mapsto> injectKOS v)))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v))) x
 2. \<And>x. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBits v; \<not> obj_at' (\<lambda>v'. v = v' \<or> True) p x\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
y <- assert (p = fst pa);
_ <- assert_opt (projectKO_opt (snd pa));
y <- assert (is_aligned p (objBits v));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits v);
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> injectKOS v)))
od) x = (do y <- assert (obj_at' (\<lambda>v'. True) p x);
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v)))
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBits v; \<not> obj_at' (\<lambda>v'. v = v' \<or> True) p x\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
y <- assert (p = fst pa);
_ <- assert_opt (projectKO_opt (snd pa));
y <- assert (is_aligned p (objBits v));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits v);
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> injectKOS v)))
od) x = (do y <- assert (obj_at' (\<lambda>v'. True) p x);
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v)))
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x b x2. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBits v; \<not> obj_at' (\<lambda>v'. True) p x; ps_clear p (objBits v) x; projectKO_opt b = Some x2; ksPSpace x p = Some b; is_aligned p (objBits v)\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(p \<mapsto> injectKOS v))) x = fail x proof (prove)
goal (1 subgoal):
 1. \<And>x b x2. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBits v; is_aligned p (objBitsKO b) \<longrightarrow> \<not> ps_clear p (objBitsKO b) x; ps_clear p (objBits v) x; projectKO_opt b = Some x2; ksPSpace x p = Some b; is_aligned p (objBits v)\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(p \<mapsto> injectKOS v))) x = fail x proof (prove)
goal (1 subgoal):
 1. \<And>x x2. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBits v; is_aligned p (objBitsKO (injectKOS x2)) \<longrightarrow> \<not> ps_clear p (objBitsKO (injectKOS x2)) x; ps_clear p (objBits v) x; ksPSpace x p = Some (injectKOS x2); is_aligned p (objBits v)\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(p \<mapsto> injectKOS v))) x = fail x proof (prove)
goal:
No subgoals!