theory Detype_R

lemma threadSet_det:
  "tcb_at' ptr s
  \<Longrightarrow> threadSet f ptr s =
  modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto>
    (\<lambda>t. case t of Some (KOTCB tcb) \<Rightarrow> KOTCB (f tcb)) (ps ptr)))) s" apply (clarsimp simp add:threadSet_def bind_def obj_at'_def) apply (clarsimp simp:projectKO_eq projectKO_opt_tcb
    split: Structures_H.kernel_object.splits) apply (subst getTCB_det,simp add:ko_wp_at'_def)+ apply (clarsimp simp:setObject_def gets_def get_def) apply (subst bind_def) apply (clarsimp simp:split_def) apply (simp add:lookupAround2_known1 bind_assoc projectKO_def
    assert_opt_def updateObject_default_def projectKO_opt_tcb) apply (clarsimp simp add:
    alignCheck_def unless_def when_def
    is_aligned_mask objBits_simps) apply (clarsimp simp:magnitudeCheck_det bind_def) apply (cut_tac ko = "KOTCB obj" in magnitudeCheck_det) apply (simp add:objBits_simps is_aligned_mask)+ apply (clarsimp simp:modify_def get_def put_def bind_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at' ptr s \<Longrightarrow> threadSet f ptr s = modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (f tcb)))) s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (getObject ptr s). fst (case a of (tcb, x) \<Rightarrow> setObject ptr (f tcb) x), (\<exists>x\<in>fst (getObject ptr s). snd (case x of (tcb, x) \<Rightarrow> setObject ptr (f tcb) x)) \<or> snd (getObject ptr s)) = modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (f tcb)))) s proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (getObject ptr s). fst (case a of (tcb, x) \<Rightarrow> setObject ptr (f tcb) x), (\<exists>x\<in>fst (getObject ptr s). snd (case x of (tcb, x) \<Rightarrow> setObject ptr (f tcb) x)) \<or> snd (getObject ptr s)) = modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (f tcb)))) s proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst ({(obj, s)}, False). fst (case a of (tcb, x) \<Rightarrow> setObject ptr (f tcb) x), (\<exists>x\<in>fst ({(obj, s)}, False). snd (case x of (tcb, x) \<Rightarrow> setObject ptr (f tcb) x)) \<or> snd ({(obj, s)}, False)) = modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (f tcb)))) s proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> (do s <- \<lambda>s. ({(s, s)}, False);
case lookupAround2 ptr (ksPSpace s) of (before, after) \<Rightarrow> do (ptr', obja) <- assert_opt before;
obj' <- updateObject_default (f obj) obja ptr ptr' after;
modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr' \<mapsto> obj')))
od
od) s = modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (f tcb)))) s proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> (\<Union> (fst ` (\<lambda>(s, y). (case lookupAround2 ptr (ksPSpace s) of (before, after) \<Rightarrow> do (ptr', obja) <- assert_opt before;
obj' <- updateObject_default (f obj) obja ptr ptr' after;
modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr' \<mapsto> obj')))
od) y) ` fst ({(s, s)}, False)), True \<in> snd ` (\<lambda>(s, y). (case lookupAround2 ptr (ksPSpace s) of (before, after) \<Rightarrow> do (ptr', obja) <- assert_opt before;
obj' <- updateObject_default (f obj) obja ptr ptr' after;
modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr' \<mapsto> obj')))
od) y) ` fst ({(s, s)}, False) \<or> snd ({(s, s)}, False)) = modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (f tcb)))) s proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> (do p <- assert_opt (fst (lookupAround2 ptr (ksPSpace s)));
obj' <- updateObject_default (f obj) (snd p) ptr (fst p) (snd (lookupAround2 ptr (ksPSpace s)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(fst p \<mapsto> obj')))
od) s = modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (f tcb)))) s proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> (do x <- alignCheck ptr (objBits (f obj));
y <- magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBits (f obj));
modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOTCB (f obj))))
od) s = modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (f tcb)))) s proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s ptr = Some (KOTCB obj); ptr && mask tcbBlockSizeBits = 0; ps_clear ptr tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (do y <- magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) tcbBlockSizeBits;
modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOTCB (f obj))))
od) s = modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (f tcb)))) s proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s ptr = Some (KOTCB obj); ptr && mask tcbBlockSizeBits = 0; ps_clear ptr tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) tcbBlockSizeBits s). fst (case a of (y, x) \<Rightarrow> modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOTCB (f obj)))) x), (\<exists>x\<in>fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) tcbBlockSizeBits s). snd (case x of (y, x) \<Rightarrow> modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOTCB (f obj)))) x)) \<or> snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) tcbBlockSizeBits s)) = modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (f tcb)))) s proof (prove)
goal (4 subgoals):
 1. \<And>obj. \<lbrakk>ksPSpace s ptr = Some (KOTCB obj); ptr && mask tcbBlockSizeBits = 0; ps_clear ptr tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ksPSpace (?s59 obj) (?ptr59 obj) = Some (KOTCB obj)
 2. \<And>obj. \<lbrakk>ksPSpace s ptr = Some (KOTCB obj); ptr && mask tcbBlockSizeBits = 0; ps_clear ptr tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> is_aligned (?ptr59 obj) (objBitsKO (KOTCB obj))
 3. \<And>obj. \<lbrakk>ksPSpace s ptr = Some (KOTCB obj); ptr && mask tcbBlockSizeBits = 0; ps_clear ptr tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ps_clear (?ptr59 obj) (objBitsKO (KOTCB obj)) (?s59 obj)
 4. \<And>obj. \<lbrakk>ksPSpace s ptr = Some (KOTCB obj); ptr && mask tcbBlockSizeBits = 0; ps_clear ptr tcbBlockSizeBits s; magnitudeCheck (?ptr59 obj) (snd (lookupAround2 (?ptr59 obj) (ksPSpace (?s59 obj)))) (objBitsKO (KOTCB obj)) (?s59 obj) = ({((), ?s59 obj)}, False)\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) tcbBlockSizeBits s). fst (case a of (y, x) \<Rightarrow> modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOTCB (f obj)))) x), (\<exists>x\<in>fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) tcbBlockSizeBits s). snd (case x of (y, x) \<Rightarrow> modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOTCB (f obj)))) x)) \<or> snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) tcbBlockSizeBits s)) = modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (f tcb)))) s proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s ptr = Some (KOTCB obj); ptr && mask tcbBlockSizeBits = 0; ps_clear ptr tcbBlockSizeBits s; magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) tcbBlockSizeBits s = ({((), s)}, False)\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOTCB (f obj)))) s = modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (f tcb)))) s proof (prove)
goal:
No subgoals!