theory Finalise_DR

lemma dcorres_set_pde_cap:
  "\<lbrakk> (x::word32) = (ptr && mask pd_bits >> 2);pde_cap = transform_pde a_pde; ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk>\<Longrightarrow>
    dcorres dc \<top> (valid_idle and ko_at (ArchObj (arch_kernel_obj.PageDirectory fun)) a )
      (KHeap_D.set_cap (a, unat x) pde_cap)
      (KHeap_A.set_object a (ArchObj
                 (arch_kernel_obj.PageDirectory (fun(ucast x := a_pde)))))" apply (simp add: KHeap_D.set_cap_def KHeap_A.set_object_def gets_the_def gets_def bind_assoc) apply (rule dcorres_absorb_get_l) apply (clarsimp simp: obj_at_def opt_object_page_directory assert_opt_def has_slots_def object_slots_def) apply (clarsimp simp: KHeap_D.set_object_def get_object_def in_monad simpler_modify_def put_def
                        bind_def corres_underlying_def update_slots_def object_slots_def return_def) apply (clarsimp simp: transform_def transform_current_thread_def) apply (rule ext) apply (clarsimp | rule conjI)+ apply (frule page_directory_at_rev) apply (frule(1) page_directory_not_idle) apply (clarsimp simp: transform_objects_def not_idle_thread_def) apply (rule sym) apply (erule transform_page_directory_contents_upd) apply (clarsimp simp: transform_objects_def restrict_map_def map_add_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and ako_at (arch_kernel_obj.PageDirectory fun) a) (KHeap_D.set_cap (a, unat x) pde_cap) (KHeap_A.set_object a (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) x := a_pde))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and ako_at (arch_kernel_obj.PageDirectory fun) a) (do x <- get;
obj <- assert_opt (cdl_objects x a);
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)) obj of Tcb t \<Rightarrow> if unat (ptr && mask pd_bits >> 2) = tcb_ipcbuffer_slot \<and> object_slots obj (unat (ptr && mask pd_bits >> 2)) \<noteq> Some (transform_pde a_pde) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)) obj)) >>= KHeap_D.set_object a
od) (do kobj <- KHeap_A.get_object a;
y <- assert (a_type kobj = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde)))));
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; True; (valid_idle and ako_at (arch_kernel_obj.PageDirectory fun) 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)(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)) obj of Tcb t \<Rightarrow> if unat (ptr && mask pd_bits >> 2) = tcb_ipcbuffer_slot \<and> object_slots obj (unat (ptr && mask pd_bits >> 2)) \<noteq> Some (transform_pde a_pde) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)) obj)) >>= KHeap_D.set_object a
od) (do kobj <- KHeap_A.get_object a;
y <- assert (a_type kobj = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde)))));
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' a = Some (ArchObj (arch_kernel_obj.PageDirectory fun))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') ((case update_slots ((transform_page_directory_contents fun)(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)) (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents fun\<rparr>) of Tcb t \<Rightarrow> if unat (ptr && mask pd_bits >> 2) = tcb_ipcbuffer_slot \<and> object_slots (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents fun\<rparr>) (unat (ptr && mask pd_bits >> 2)) \<noteq> Some (transform_pde a_pde) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents fun\<rparr>))(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)) (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents fun\<rparr>)) | _ \<Rightarrow> return (update_slots ((object_slots (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents fun\<rparr>))(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)) (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents fun\<rparr>))) >>= KHeap_D.set_object a) (do kobj <- KHeap_A.get_object a;
y <- assert (a_type kobj = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde)))));
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s')(a \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))) s') = dupdate_cdl_object a (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = (transform_page_directory_contents fun)(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)\<rparr>) (transform s') proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(a \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))) s') = (transform_objects s')(a \<mapsto> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = (transform_page_directory_contents fun)(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s' xa. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(a \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))) s') xa = ((transform_objects s')(a \<mapsto> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = (transform_page_directory_contents fun)(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)\<rparr>)) xa proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(a \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))) s') a = Some (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = (transform_page_directory_contents fun)(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)\<rparr>)
 2. \<And>s' xa. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))\<rbrakk> \<Longrightarrow> xa \<noteq> a \<longrightarrow> transform_objects (update_kheap ((kheap s')(a \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))) s') xa = transform_objects s' xa proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde)))); typ_at (AArch APageDirectory) a s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(a \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))) s') a = Some (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = (transform_page_directory_contents fun)(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)\<rparr>)
 2. \<And>s' xa. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))\<rbrakk> \<Longrightarrow> xa \<noteq> a \<longrightarrow> transform_objects (update_kheap ((kheap s')(a \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))) s') xa = transform_objects s' xa proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde)))); typ_at (AArch APageDirectory) a s'; not_idle_thread a s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(a \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))) s') a = Some (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = (transform_page_directory_contents fun)(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)\<rparr>)
 2. \<And>s' xa. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))\<rbrakk> \<Longrightarrow> xa \<noteq> a \<longrightarrow> transform_objects (update_kheap ((kheap s')(a \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))) s') xa = transform_objects s' xa proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde)))); typ_at (AArch APageDirectory) a s'; a \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> transform_page_directory_contents (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde)) = (transform_page_directory_contents fun)(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)
 2. \<And>s' xa. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))\<rbrakk> \<Longrightarrow> xa \<noteq> a \<longrightarrow> transform_objects (update_kheap ((kheap s')(a \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))) s') xa = transform_objects s' xa proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde)))); typ_at (AArch APageDirectory) a s'; a \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> (transform_page_directory_contents fun)(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde) = transform_page_directory_contents (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))
 2. \<And>s' xa. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))\<rbrakk> \<Longrightarrow> xa \<noteq> a \<longrightarrow> transform_objects (update_kheap ((kheap s')(a \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))) s') xa = transform_objects s' xa proof (prove)
goal (1 subgoal):
 1. \<And>s' xa. \<lbrakk>x = ptr && mask pd_bits >> 2; pde_cap = transform_pde a_pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))\<rbrakk> \<Longrightarrow> xa \<noteq> a \<longrightarrow> transform_objects (update_kheap ((kheap s')(a \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := a_pde))))) s') xa = transform_objects s' xa proof (prove)
goal:
No subgoals!