theory Finalise_DR

lemma dcorres_set_pte_cap:
  "\<lbrakk> (x::word32) = (ptr && mask pt_bits >> 2);pte_cap = transform_pte a_pte\<rbrakk>\<Longrightarrow>
    dcorres dc \<top> (valid_idle and ko_at (ArchObj (arch_kernel_obj.PageTable fun)) a )
    (KHeap_D.set_cap (a, unat (ptr && mask pt_bits >> 2)) pte_cap)
    (KHeap_A.set_object a
      (ArchObj (arch_kernel_obj.PageTable (fun(ucast (ptr && mask pt_bits >> 2) := a_pte)))))" apply (simp add: KHeap_D.set_cap_def KHeap_A.set_object_def get_object_def gets_the_def gets_def bind_assoc) apply (rule dcorres_absorb_get_r) apply (rule dcorres_absorb_get_l) apply (clarsimp simp: obj_at_def opt_object_page_table 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 return_def object_slots_def) apply (rule sym) apply (clarsimp simp: transform_def transform_current_thread_def) apply (rule ext) apply (clarsimp | rule conjI)+ apply (frule page_table_at_rev) apply (frule(1) page_table_not_idle) apply (clarsimp simp: transform_objects_def not_idle_thread_def) apply (rule ext) apply (clarsimp simp: transform_page_table_contents_def transform_pte_def unat_map_def) apply (clarsimp simp: mask_pt_bits_less mask_pt_bits_less') apply (simp only: ucast_nat_def[symmetric]) apply (drule word_of_nat_inj[rotated -1]; clarsimp simp: mask_pt_bits_less) 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 pt_bits >> 2; pte_cap = transform_pte a_pte\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and ako_at (arch_kernel_obj.PageTable fun) a) (KHeap_D.set_cap (a, unat (ptr && mask pt_bits >> 2)) pte_cap) (KHeap_A.set_object a (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and ako_at (arch_kernel_obj.PageTable 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 pt_bits >> 2) \<mapsto> transform_pte a_pte)) obj of Tcb t \<Rightarrow> if unat (ptr && mask pt_bits >> 2) = tcb_ipcbuffer_slot \<and> object_slots obj (unat (ptr && mask pt_bits >> 2)) \<noteq> Some (transform_pte a_pte) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)) obj)) >>= KHeap_D.set_object a
od) (do x <- get;
y <- assert (\<exists>y. kheap x a = Some y);
y <- assert (a_type (the (kheap x a)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte)))));
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; True; (valid_idle and ako_at (arch_kernel_obj.PageTable fun) a) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do x <- get;
obj <- assert_opt (cdl_objects x a);
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)) obj of Tcb t \<Rightarrow> if unat (ptr && mask pt_bits >> 2) = tcb_ipcbuffer_slot \<and> object_slots obj (unat (ptr && mask pt_bits >> 2)) \<noteq> Some (transform_pte a_pte) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)) obj)) >>= KHeap_D.set_object a
od) (do y <- assert (\<exists>y. kheap s' a = Some y);
y <- assert (a_type (the (kheap s' a)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte)))));
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' s'a. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; True; (valid_idle and ako_at (arch_kernel_obj.PageTable fun) a) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do obj <- assert_opt (cdl_objects (transform s'a) a);
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)) obj of Tcb t \<Rightarrow> if unat (ptr && mask pt_bits >> 2) = tcb_ipcbuffer_slot \<and> object_slots obj (unat (ptr && mask pt_bits >> 2)) \<noteq> Some (transform_pte a_pte) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)) obj)) >>= KHeap_D.set_object a
od) (do y <- assert (\<exists>y. kheap s' a = Some y);
y <- assert (a_type (the (kheap s' a)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte)))));
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'a. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case update_slots ((transform_page_table_contents fun)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)) (cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents fun\<rparr>) of Tcb t \<Rightarrow> if unat (ptr && mask pt_bits >> 2) = tcb_ipcbuffer_slot \<and> object_slots (cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents fun\<rparr>) (unat (ptr && mask pt_bits >> 2)) \<noteq> Some (transform_pte a_pte) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots (cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents fun\<rparr>))(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)) (cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents fun\<rparr>)) | _ \<Rightarrow> return (update_slots ((object_slots (cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents fun\<rparr>))(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)) (cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents fun\<rparr>))) >>= KHeap_D.set_object a) (do y <- assert (a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte)))));
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'a. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) = dupdate_cdl_object a (cdl_object.PageTable \<lparr>cdl_page_table_caps = (transform_page_table_contents fun)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)\<rparr>) (transform s'a) proof (prove)
goal (1 subgoal):
 1. \<And>s'a. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))\<rbrakk> \<Longrightarrow> dupdate_cdl_object a (cdl_object.PageTable \<lparr>cdl_page_table_caps = (transform_page_table_contents fun)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)\<rparr>) (transform s'a) = transform (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) proof (prove)
goal (1 subgoal):
 1. \<And>s'a. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))\<rbrakk> \<Longrightarrow> (transform_objects s'a)(a \<mapsto> cdl_object.PageTable \<lparr>cdl_page_table_caps = (transform_page_table_contents fun)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)\<rparr>) = transform_objects (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) proof (prove)
goal (1 subgoal):
 1. \<And>s'a xa. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))\<rbrakk> \<Longrightarrow> ((transform_objects s'a)(a \<mapsto> cdl_object.PageTable \<lparr>cdl_page_table_caps = (transform_page_table_contents fun)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)\<rparr>)) xa = transform_objects (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) xa proof (prove)
goal (2 subgoals):
 1. \<And>s'a. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))\<rbrakk> \<Longrightarrow> Some (cdl_object.PageTable \<lparr>cdl_page_table_caps = (transform_page_table_contents fun)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)\<rparr>) = transform_objects (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) a
 2. \<And>s'a xa. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))\<rbrakk> \<Longrightarrow> xa \<noteq> a \<longrightarrow> transform_objects s'a xa = transform_objects (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) xa proof (prove)
goal (2 subgoals):
 1. \<And>s'a. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte)))); typ_at (AArch APageTable) a s'a\<rbrakk> \<Longrightarrow> Some (cdl_object.PageTable \<lparr>cdl_page_table_caps = (transform_page_table_contents fun)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)\<rparr>) = transform_objects (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) a
 2. \<And>s'a xa. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))\<rbrakk> \<Longrightarrow> xa \<noteq> a \<longrightarrow> transform_objects s'a xa = transform_objects (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) xa proof (prove)
goal (2 subgoals):
 1. \<And>s'a. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte)))); typ_at (AArch APageTable) a s'a; not_idle_thread a s'a\<rbrakk> \<Longrightarrow> Some (cdl_object.PageTable \<lparr>cdl_page_table_caps = (transform_page_table_contents fun)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)\<rparr>) = transform_objects (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) a
 2. \<And>s'a xa. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))\<rbrakk> \<Longrightarrow> xa \<noteq> a \<longrightarrow> transform_objects s'a xa = transform_objects (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) xa proof (prove)
goal (2 subgoals):
 1. \<And>s'a. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte)))); typ_at (AArch APageTable) a s'a; a \<noteq> idle_thread s'a\<rbrakk> \<Longrightarrow> (transform_page_table_contents fun)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte) = transform_page_table_contents (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))
 2. \<And>s'a xa. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))\<rbrakk> \<Longrightarrow> xa \<noteq> a \<longrightarrow> transform_objects s'a xa = transform_objects (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) xa proof (prove)
goal (2 subgoals):
 1. \<And>s'a xa. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte)))); typ_at (AArch APageTable) a s'a; a \<noteq> idle_thread s'a\<rbrakk> \<Longrightarrow> ((transform_page_table_contents fun)(unat (ptr && mask pt_bits >> 2) \<mapsto> transform_pte a_pte)) xa = transform_page_table_contents (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte)) xa
 2. \<And>s'a xa. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))\<rbrakk> \<Longrightarrow> xa \<noteq> a \<longrightarrow> transform_objects s'a xa = transform_objects (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) xa proof (prove)
goal (2 subgoals):
 1. \<And>s'a xa. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = (case a_pte of InvalidPTE \<Rightarrow> cdl_cap.NullCap | LargePagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMLargePage) Fake None | SmallPagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMSmallPage) Fake None); valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte)))); typ_at (AArch APageTable) a s'a; a \<noteq> idle_thread s'a\<rbrakk> \<Longrightarrow> (word_of_nat xa = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<longrightarrow> (xa = unat (ptr && mask pt_bits >> 2) \<longrightarrow> unat (ptr && mask pt_bits >> 2) < 256) \<and> (xa \<noteq> unat (ptr && mask pt_bits >> 2) \<longrightarrow> xa < 256 \<longrightarrow> (case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> cdl_cap.NullCap | LargePagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMLargePage) Fake None | SmallPagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMSmallPage) Fake None) = (case a_pte of InvalidPTE \<Rightarrow> cdl_cap.NullCap | LargePagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMLargePage) Fake None | SmallPagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMSmallPage) Fake None))) \<and> (word_of_nat xa \<noteq> UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<longrightarrow> xa = unat (ptr && mask pt_bits >> 2) \<longrightarrow> unat (ptr && mask pt_bits >> 2) < 256)
 2. \<And>s'a xa. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))\<rbrakk> \<Longrightarrow> xa \<noteq> a \<longrightarrow> transform_objects s'a xa = transform_objects (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) xa proof (prove)
goal (2 subgoals):
 1. \<And>s'a xa. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = (case a_pte of InvalidPTE \<Rightarrow> cdl_cap.NullCap | LargePagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMLargePage) Fake None | SmallPagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMSmallPage) Fake None); valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte)))); typ_at (AArch APageTable) a s'a; a \<noteq> idle_thread s'a; word_of_nat xa = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); xa \<noteq> unat (ptr && mask pt_bits >> 2); xa < 256\<rbrakk> \<Longrightarrow> (case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> cdl_cap.NullCap | LargePagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMLargePage) Fake None | SmallPagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMSmallPage) Fake None) = (case a_pte of InvalidPTE \<Rightarrow> cdl_cap.NullCap | LargePagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMLargePage) Fake None | SmallPagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMSmallPage) Fake None)
 2. \<And>s'a xa. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))\<rbrakk> \<Longrightarrow> xa \<noteq> a \<longrightarrow> transform_objects s'a xa = transform_objects (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) xa proof (prove)
goal (2 subgoals):
 1. \<And>s'a xa. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = (case a_pte of InvalidPTE \<Rightarrow> cdl_cap.NullCap | LargePagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMLargePage) Fake None | SmallPagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMSmallPage) Fake None); valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(word_of_nat (unat (ptr && mask pt_bits >> 2)) := a_pte)))); typ_at (AArch APageTable) a s'a; a \<noteq> idle_thread s'a; word_of_nat xa = word_of_nat (unat (ptr && mask pt_bits >> 2)); xa \<noteq> unat (ptr && mask pt_bits >> 2); xa < 256\<rbrakk> \<Longrightarrow> (case fun (word_of_nat (unat (ptr && mask pt_bits >> 2))) of InvalidPTE \<Rightarrow> cdl_cap.NullCap | LargePagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMLargePage) Fake None | SmallPagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMSmallPage) Fake None) = (case a_pte of InvalidPTE \<Rightarrow> cdl_cap.NullCap | LargePagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMLargePage) Fake None | SmallPagePTE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMSmallPage) Fake None)
 2. \<And>s'a xa. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))\<rbrakk> \<Longrightarrow> xa \<noteq> a \<longrightarrow> transform_objects s'a xa = transform_objects (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) xa proof (prove)
goal (1 subgoal):
 1. \<And>s'a xa. \<lbrakk>x = ptr && mask pt_bits >> 2; pte_cap = transform_pte a_pte; valid_idle s'a; kheap s'a a = Some (ArchObj (arch_kernel_obj.PageTable fun)); a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))\<rbrakk> \<Longrightarrow> xa \<noteq> a \<longrightarrow> transform_objects s'a xa = transform_objects (update_kheap ((kheap s'a)(a \<mapsto> ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := a_pte))))) s'a) xa proof (prove)
goal:
No subgoals!