theory Retype_R

lemma retype_region_ext_modify_kheap_futz:
  "(retype_region2_extra_ext ptrs type :: (unit, det_ext) s_monad) >>= (\<lambda>_. modify (kheap_update f))
 = (modify (kheap_update f) >>= (\<lambda>_. retype_region2_extra_ext ptrs type))" apply (clarsimp simp: retype_region_ext_def retype_region2_ext_def retype_region2_extra_ext_def when_def bind_assoc) apply (subst oblivious_modify_swap) defer apply (simp add: bind_assoc) apply (rule oblivious_bind) apply simp apply (rule oblivious_mapM_x) apply (clarsimp simp: ethread_set_def set_eobject_def) apply (rule oblivious_bind) apply (simp add: gets_the_def) apply (rule oblivious_bind) apply (clarsimp simp: get_etcb_def) apply simp apply (simp add: modify_def[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- retype_region2_extra_ext ptrs type;
modify (kheap_update f)
od = do _ <- modify (kheap_update f);
retype_region2_extra_ext ptrs type
od proof (prove)
goal (1 subgoal):
 1. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> do x <- gets cur_domain;
_ <- mapM_x (ethread_set (tcb_domain_update (\<lambda>_. x))) ptrs;
modify (kheap_update f)
od = do _ <- modify (kheap_update f);
cdom <- gets cur_domain;
mapM_x (ethread_set (tcb_domain_update (\<lambda>_. cdom))) ptrs
od proof (prove)
goal (2 subgoals):
 1. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> oblivious (kheap_update f) (do cdom <- gets cur_domain;
mapM_x (ethread_set (tcb_domain_update (\<lambda>_. cdom))) ptrs
od)
 2. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> do x <- gets cur_domain;
_ <- mapM_x (ethread_set (tcb_domain_update (\<lambda>_. x))) ptrs;
modify (kheap_update f)
od = do rv <- do cdom <- gets cur_domain;
mapM_x (ethread_set (tcb_domain_update (\<lambda>_. cdom))) ptrs
od;
modify (kheap_update f)
od proof (prove)
goal (2 subgoals):
 1. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> do x <- gets cur_domain;
_ <- mapM_x (ethread_set (tcb_domain_update (\<lambda>_. x))) ptrs;
modify (kheap_update f)
od = do rv <- do cdom <- gets cur_domain;
mapM_x (ethread_set (tcb_domain_update (\<lambda>_. cdom))) ptrs
od;
modify (kheap_update f)
od
 2. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> oblivious (kheap_update f) (do cdom <- gets cur_domain;
mapM_x (ethread_set (tcb_domain_update (\<lambda>_. cdom))) ptrs
od) proof (prove)
goal (1 subgoal):
 1. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> oblivious (kheap_update f) (do cdom <- gets cur_domain;
mapM_x (ethread_set (tcb_domain_update (\<lambda>_. cdom))) ptrs
od) proof (prove)
goal (2 subgoals):
 1. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> oblivious (kheap_update f) (gets cur_domain)
 2. \<And>rv. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> oblivious (kheap_update f) (mapM_x (ethread_set (tcb_domain_update (\<lambda>_. rv))) ptrs) proof (prove)
goal (1 subgoal):
 1. \<And>rv. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> oblivious (kheap_update f) (mapM_x (ethread_set (tcb_domain_update (\<lambda>_. rv))) ptrs) proof (prove)
goal (1 subgoal):
 1. \<And>rv. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> \<forall>x\<in>set ptrs. oblivious (kheap_update f) (ethread_set (tcb_domain_update (\<lambda>_. rv)) x) proof (prove)
goal (1 subgoal):
 1. \<And>rv x. \<lbrakk>type = Structures_A.apiobject_type.TCBObject; x \<in> set ptrs\<rbrakk> \<Longrightarrow> oblivious (kheap_update f) (do tcb <- gets_the (get_etcb x);
es <- get;
put (ekheap_update (\<lambda>_. (ekheap es)(x \<mapsto> tcb\<lparr>tcb_domain := rv\<rparr>)) es)
od) proof (prove)
goal (2 subgoals):
 1. \<And>rv x. \<lbrakk>type = Structures_A.apiobject_type.TCBObject; x \<in> set ptrs\<rbrakk> \<Longrightarrow> oblivious (kheap_update f) (gets_the (get_etcb x))
 2. \<And>rv x rva. \<lbrakk>type = Structures_A.apiobject_type.TCBObject; x \<in> set ptrs\<rbrakk> \<Longrightarrow> oblivious (kheap_update f) (do es <- get;
put (ekheap_update (\<lambda>_. (ekheap es)(x \<mapsto> rva\<lparr>tcb_domain := rv\<rparr>)) es)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>type = Structures_A.apiobject_type.TCBObject; x \<in> set ptrs\<rbrakk> \<Longrightarrow> oblivious (kheap_update f) (gets (get_etcb x) >>= assert_opt)
 2. \<And>rv x rva. \<lbrakk>type = Structures_A.apiobject_type.TCBObject; x \<in> set ptrs\<rbrakk> \<Longrightarrow> oblivious (kheap_update f) (do es <- get;
put (ekheap_update (\<lambda>_. (ekheap es)(x \<mapsto> rva\<lparr>tcb_domain := rv\<rparr>)) es)
od) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>type = Structures_A.apiobject_type.TCBObject; x \<in> set ptrs\<rbrakk> \<Longrightarrow> oblivious (kheap_update f) (gets (get_etcb x))
 2. \<And>x rv. \<lbrakk>type = Structures_A.apiobject_type.TCBObject; x \<in> set ptrs\<rbrakk> \<Longrightarrow> oblivious (kheap_update f) (assert_opt rv)
 3. \<And>rv x rva. \<lbrakk>type = Structures_A.apiobject_type.TCBObject; x \<in> set ptrs\<rbrakk> \<Longrightarrow> oblivious (kheap_update f) (do es <- get;
put (ekheap_update (\<lambda>_. (ekheap es)(x \<mapsto> rva\<lparr>tcb_domain := rv\<rparr>)) es)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x rv. \<lbrakk>type = Structures_A.apiobject_type.TCBObject; x \<in> set ptrs\<rbrakk> \<Longrightarrow> oblivious (kheap_update f) (assert_opt rv)
 2. \<And>rv x rva. \<lbrakk>type = Structures_A.apiobject_type.TCBObject; x \<in> set ptrs\<rbrakk> \<Longrightarrow> oblivious (kheap_update f) (do es <- get;
put (ekheap_update (\<lambda>_. (ekheap es)(x \<mapsto> rva\<lparr>tcb_domain := rv\<rparr>)) es)
od) proof (prove)
goal (1 subgoal):
 1. \<And>rv x rva. \<lbrakk>type = Structures_A.apiobject_type.TCBObject; x \<in> set ptrs\<rbrakk> \<Longrightarrow> oblivious (kheap_update f) (do es <- get;
put (ekheap_update (\<lambda>_. (ekheap es)(x \<mapsto> rva\<lparr>tcb_domain := rv\<rparr>)) es)
od) proof (prove)
goal:
No subgoals!