theory Finalise_DR

lemma dcorres_set_asid_pool:
  "\<lbrakk> pool' = pool (ucast asid := pd); slot = snd (transform_asid asid);
     cap = transform_asid_pool_entry pd \<rbrakk> \<Longrightarrow>
    dcorres dc \<top> (valid_idle and ko_at (ArchObj (arch_kernel_obj.ASIDPool pool)) a)
    (KHeap_D.set_cap (a, slot) cap)
    (set_asid_pool a pool')" apply (simp add:KHeap_D.set_cap_def set_asid_pool_def get_object_def gets_the_def
                  gets_def bind_assoc) apply (rule dcorres_absorb_get_l) apply (clarsimp simp: obj_at_def opt_object_asid_pool assert_opt_def has_slots_def) apply (clarsimp simp: KHeap_D.set_object_def simpler_modify_def put_def bind_def
                       corres_underlying_def update_slots_def return_def object_slots_def) apply (clarsimp simp: KHeap_A.set_object_def get_object_def in_monad get_def
                        put_def bind_def return_def) apply (clarsimp simp: transform_def transform_current_thread_def) apply (drule(1) arch_obj_not_idle) apply (rule ext) apply (clarsimp simp: not_idle_thread_def transform_objects_def restrict_map_def map_add_def) apply (rule transform_asid_pool_contents_upd) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pool' = pool(UCAST(32 \<rightarrow> 10) asid := pd); slot = snd (transform_asid asid); cap = transform_asid_pool_entry pd\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and ako_at (ASIDPool pool) a) (KHeap_D.set_cap (a, slot) cap) (set_asid_pool a pool') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pool' = pool(UCAST(32 \<rightarrow> 10) asid := pd); slot = snd (transform_asid asid); cap = transform_asid_pool_entry pd\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and ako_at (ASIDPool pool) a) (do x <- get;
obj <- assert_opt (cdl_objects x a);
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)) obj of Tcb t \<Rightarrow> if snd (transform_asid asid) = tcb_ipcbuffer_slot \<and> object_slots obj (snd (transform_asid asid)) \<noteq> Some (transform_asid_pool_entry pd) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)) obj)) >>= KHeap_D.set_object a
od) (KHeap_A.set_object a (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := pd))))) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>pool' = pool(UCAST(32 \<rightarrow> 10) asid := pd); slot = snd (transform_asid asid); cap = transform_asid_pool_entry pd; True; (valid_idle and ako_at (ASIDPool pool) a) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do obj <- assert_opt (cdl_objects (transform s') a);
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)) obj of Tcb t \<Rightarrow> if snd (transform_asid asid) = tcb_ipcbuffer_slot \<and> object_slots obj (snd (transform_asid asid)) \<noteq> Some (transform_asid_pool_entry pd) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)) obj)) >>= KHeap_D.set_object a
od) (KHeap_A.set_object a (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := pd))))) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>pool' = pool(UCAST(32 \<rightarrow> 10) asid := pd); slot = snd (transform_asid asid); cap = transform_asid_pool_entry pd; valid_idle s'; kheap s' a = Some (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') ((case update_slots ((object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>))(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)) (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>) of Tcb t \<Rightarrow> if snd (transform_asid asid) = tcb_ipcbuffer_slot \<and> object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>) (snd (transform_asid asid)) \<noteq> Some (transform_asid_pool_entry pd) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>))(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)) (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>)) | _ \<Rightarrow> return (update_slots ((object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>))(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)) (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>))) >>= KHeap_D.set_object a) (KHeap_A.set_object a (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := pd))))) proof (prove)
goal (1 subgoal):
 1. \<And>s' b. \<lbrakk>pool' = pool(UCAST(32 \<rightarrow> 10) asid := pd); slot = snd (transform_asid asid); cap = transform_asid_pool_entry pd; valid_idle s'; kheap s' a = Some (ArchObj (ASIDPool pool)); ((), b) \<in> fst (KHeap_A.set_object a (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := pd)))) s')\<rbrakk> \<Longrightarrow> transform b = dupdate_cdl_object a (AsidPool \<lparr>cdl_asid_pool_caps = (transform_asid_pool_contents pool)(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)\<rparr>) (transform s') proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>pool' = pool(UCAST(32 \<rightarrow> 10) asid := pd); slot = snd (transform_asid asid); cap = transform_asid_pool_entry pd; valid_idle s'; kheap s' a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := pd))))\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s')(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := pd))))) s') = dupdate_cdl_object a (AsidPool \<lparr>cdl_asid_pool_caps = (transform_asid_pool_contents pool)(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)\<rparr>) (transform s') proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>pool' = pool(UCAST(32 \<rightarrow> 10) asid := pd); slot = snd (transform_asid asid); cap = transform_asid_pool_entry pd; valid_idle s'; kheap s' a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := pd))))\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := pd))))) s') = (transform_objects s')(a \<mapsto> AsidPool \<lparr>cdl_asid_pool_caps = (transform_asid_pool_contents pool)(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>pool' = pool(UCAST(32 \<rightarrow> 10) asid := pd); slot = snd (transform_asid asid); cap = transform_asid_pool_entry pd; kheap s' a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := pd)))); not_idle_thread a s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := pd))))) s') = (transform_objects s')(a \<mapsto> AsidPool \<lparr>cdl_asid_pool_caps = (transform_asid_pool_contents pool)(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s' x. \<lbrakk>pool' = pool(UCAST(32 \<rightarrow> 10) asid := pd); slot = snd (transform_asid asid); cap = transform_asid_pool_entry pd; kheap s' a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := pd)))); not_idle_thread a s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := pd))))) s') x = ((transform_objects s')(a \<mapsto> AsidPool \<lparr>cdl_asid_pool_caps = (transform_asid_pool_contents pool)(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)\<rparr>)) x proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>pool' = pool(UCAST(32 \<rightarrow> 10) asid := pd); slot = snd (transform_asid asid); cap = transform_asid_pool_entry pd; kheap s' a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := pd)))); a \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> transform_asid_pool_contents (pool(UCAST(32 \<rightarrow> 10) asid := pd)) = (transform_asid_pool_contents pool)(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd) proof (prove)
goal:
No subgoals!