theory Detype_R

lemma storePDE_det:
  "ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s
   \<Longrightarrow> storePDE ptr (new_pde::ARM_H.pde) s =
       modify
         (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s" apply (clarsimp simp:ko_wp_at'_def storePDE_def split_def
                       bind_def gets_def return_def
                       get_def setObject_def
                       assert_opt_def split:if_splits) apply (clarsimp simp:lookupAround2_known1 return_def alignCheck_def
                       updateObject_default_def split_def
                       archObjSize_def unless_def projectKO_def
                       projectKO_opt_pde bind_def when_def
                       is_aligned_mask[symmetric] objBits_simps) apply (drule magnitudeCheck_det) apply (simp add:objBits_simps archObjSize_def)+ apply (simp add:simpler_modify_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s \<Longrightarrow> storePDE ptr new_pde s = modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst ((case fst (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> fail | Some v \<Rightarrow> \<lambda>s. ({(v, s)}, False)) s). \<Union>xa\<in>fst (updateObject_default new_pde (snd (fst x)) ptr (fst (fst x)) (snd (lookupAround2 ptr (ksPSpace s))) (snd x)). \<Union>x\<in>fst (modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(fst (fst x) \<mapsto> fst xa))) (snd xa)). {((), snd x)}, (\<exists>x\<in>fst ((case fst (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> fail | Some v \<Rightarrow> \<lambda>s. ({(v, s)}, False)) s). (\<exists>xa\<in>fst (updateObject_default new_pde (snd (fst x)) ptr (fst (fst x)) (snd (lookupAround2 ptr (ksPSpace s))) (snd x)). snd (modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(fst (fst x) \<mapsto> fst xa))) (snd xa))) \<or> snd (updateObject_default new_pde (snd (fst x)) ptr (fst (fst x)) (snd (lookupAround2 ptr (ksPSpace s))) (snd x))) \<or> snd ((case fst (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> fail | Some v \<Rightarrow> \<lambda>s. ({(v, s)}, False)) s)) = modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr pdeBits; ps_clear ptr pdeBits s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) pdeBits s). \<Union>x\<in>fst (modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) (snd x)). {((), snd x)}, (\<exists>y\<in>fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) pdeBits s). snd (modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) (snd y))) \<or> snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) pdeBits s)) = modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr pdeBits; ps_clear ptr pdeBits s\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (KOArch (KOPDE pde)))
 2. \<lbrakk>is_aligned ptr pdeBits; ps_clear ptr pdeBits s\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s
 3. \<lbrakk>is_aligned ptr pdeBits; ps_clear ptr pdeBits s; magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO (KOArch (KOPDE pde))) s = ({((), s)}, False)\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) pdeBits s). \<Union>x\<in>fst (modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) (snd x)). {((), snd x)}, (\<exists>y\<in>fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) pdeBits s). snd (modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) (snd y))) \<or> snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) pdeBits s)) = modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr pdeBits; ps_clear ptr pdeBits s; magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) pdeBits s = ({((), s)}, False)\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s). {((), snd x)}, snd (modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s)) = modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s proof (prove)
goal:
No subgoals!