theory ArchVSpaceEntries_AI

lemma set_cap_page_inv_entries_safe:
  "\<lbrace>page_inv_entries_safe x\<rbrace> set_cap y z \<lbrace>\<lambda>_. page_inv_entries_safe x\<rbrace>" apply (simp add:page_inv_entries_safe_def set_cap_def split_def
    get_object_def set_object_def) apply (wp | wpc)+ apply (case_tac x) apply (auto simp:obj_at_def
    Let_def split:if_splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>page_inv_entries_safe x\<rbrace> set_cap y z \<lbrace>\<lambda>_. page_inv_entries_safe x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))\<rbrace> do obj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh (fst z) = Some y);
return (the (kh (fst z)))
od;
obj' <- case obj of CNode sz cn \<Rightarrow> if snd z \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd z \<mapsto> y) else fail | TCB tcb \<Rightarrow> if snd z = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := y\<rparr> else if snd z = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := y\<rparr> else if snd z = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := y\<rparr> else if snd z = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := y\<rparr> else if snd z = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := y\<rparr> else fail | _ \<Rightarrow> fail;
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh (fst z) = Some y);
return (the (kh (fst z)))
od;
y <- assert (a_type kobj = a_type obj');
s <- get;
put (s\<lparr>kheap := (kheap s)(fst z \<mapsto> obj')\<rparr>)
od \<lbrace>\<lambda>_. let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) s \<Longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> (\<forall>xa xb. the (kheap s (fst z)) = CNode xa xb \<longrightarrow> (snd z \<in> dom xb \<and> well_formed_cnode_n xa xb \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (CNode xa $ xb(snd z \<mapsto> y)) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> CNode xa $ xb(snd z \<mapsto> y))\<rparr>)) \<and> (\<not> (snd z \<in> dom xb \<and> well_formed_cnode_n xa xb) \<longrightarrow> True)) \<and> (\<forall>xa. the (kheap s (fst z)) = TCB xa \<longrightarrow> (snd z = tcb_cnode_index 0 \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (TCB $ xa\<lparr>tcb_ctable := y\<rparr>) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> TCB $ xa\<lparr>tcb_ctable := y\<rparr>)\<rparr>)) \<and> (snd z \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd z = tcb_cnode_index 1 \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (TCB $ xa\<lparr>tcb_vtable := y\<rparr>) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> TCB $ xa\<lparr>tcb_vtable := y\<rparr>)\<rparr>)) \<and> (snd z \<noteq> tcb_cnode_index 1 \<longrightarrow> (snd z = tcb_cnode_index 2 \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (TCB $ xa\<lparr>tcb_reply := y\<rparr>) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> TCB $ xa\<lparr>tcb_reply := y\<rparr>)\<rparr>)) \<and> (snd z \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd z = tcb_cnode_index 3 \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (TCB $ xa\<lparr>tcb_caller := y\<rparr>) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> TCB $ xa\<lparr>tcb_caller := y\<rparr>)\<rparr>)) \<and> (snd z \<noteq> tcb_cnode_index 3 \<longrightarrow> (snd z = tcb_cnode_index 4 \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (TCB $ xa\<lparr>tcb_ipcframe := y\<rparr>) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> TCB $ xa\<lparr>tcb_ipcframe := y\<rparr>)\<rparr>)) \<and> (snd z \<noteq> tcb_cnode_index 4 \<longrightarrow> True)))))) \<and> (\<forall>x. the (kheap s (fst z)) = Endpoint x \<longrightarrow> True) \<and> (\<forall>x. the (kheap s (fst z)) = Notification x \<longrightarrow> True) \<and> (\<forall>x. the (kheap s (fst z)) = ArchObj x \<longrightarrow> True) proof (prove)
goal (2 subgoals):
 1. \<And>s a. \<lbrakk>(let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) s; x = Inl a\<rbrakk> \<Longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> (\<forall>xa xb. the (kheap s (fst z)) = CNode xa xb \<longrightarrow> (snd z \<in> dom xb \<and> well_formed_cnode_n xa xb \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (CNode xa $ xb(snd z \<mapsto> y)) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> CNode xa $ xb(snd z \<mapsto> y))\<rparr>)) \<and> (\<not> (snd z \<in> dom xb \<and> well_formed_cnode_n xa xb) \<longrightarrow> True)) \<and> (\<forall>xa. the (kheap s (fst z)) = TCB xa \<longrightarrow> (snd z = tcb_cnode_index 0 \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (TCB $ xa\<lparr>tcb_ctable := y\<rparr>) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> TCB $ xa\<lparr>tcb_ctable := y\<rparr>)\<rparr>)) \<and> (snd z \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd z = tcb_cnode_index 1 \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (TCB $ xa\<lparr>tcb_vtable := y\<rparr>) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> TCB $ xa\<lparr>tcb_vtable := y\<rparr>)\<rparr>)) \<and> (snd z \<noteq> tcb_cnode_index 1 \<longrightarrow> (snd z = tcb_cnode_index 2 \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (TCB $ xa\<lparr>tcb_reply := y\<rparr>) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> TCB $ xa\<lparr>tcb_reply := y\<rparr>)\<rparr>)) \<and> (snd z \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd z = tcb_cnode_index 3 \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (TCB $ xa\<lparr>tcb_caller := y\<rparr>) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> TCB $ xa\<lparr>tcb_caller := y\<rparr>)\<rparr>)) \<and> (snd z \<noteq> tcb_cnode_index 3 \<longrightarrow> (snd z = tcb_cnode_index 4 \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (TCB $ xa\<lparr>tcb_ipcframe := y\<rparr>) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> TCB $ xa\<lparr>tcb_ipcframe := y\<rparr>)\<rparr>)) \<and> (snd z \<noteq> tcb_cnode_index 4 \<longrightarrow> True)))))) \<and> (\<forall>x. the (kheap s (fst z)) = Endpoint x \<longrightarrow> True) \<and> (\<forall>x. the (kheap s (fst z)) = Notification x \<longrightarrow> True) \<and> (\<forall>x. the (kheap s (fst z)) = ArchObj x \<longrightarrow> True)
 2. \<And>s b. \<lbrakk>(let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) s; x = Inr b\<rbrakk> \<Longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> (\<forall>xa xb. the (kheap s (fst z)) = CNode xa xb \<longrightarrow> (snd z \<in> dom xb \<and> well_formed_cnode_n xa xb \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (CNode xa $ xb(snd z \<mapsto> y)) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> CNode xa $ xb(snd z \<mapsto> y))\<rparr>)) \<and> (\<not> (snd z \<in> dom xb \<and> well_formed_cnode_n xa xb) \<longrightarrow> True)) \<and> (\<forall>xa. the (kheap s (fst z)) = TCB xa \<longrightarrow> (snd z = tcb_cnode_index 0 \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (TCB $ xa\<lparr>tcb_ctable := y\<rparr>) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> TCB $ xa\<lparr>tcb_ctable := y\<rparr>)\<rparr>)) \<and> (snd z \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd z = tcb_cnode_index 1 \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (TCB $ xa\<lparr>tcb_vtable := y\<rparr>) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> TCB $ xa\<lparr>tcb_vtable := y\<rparr>)\<rparr>)) \<and> (snd z \<noteq> tcb_cnode_index 1 \<longrightarrow> (snd z = tcb_cnode_index 2 \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (TCB $ xa\<lparr>tcb_reply := y\<rparr>) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> TCB $ xa\<lparr>tcb_reply := y\<rparr>)\<rparr>)) \<and> (snd z \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd z = tcb_cnode_index 3 \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (TCB $ xa\<lparr>tcb_caller := y\<rparr>) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> TCB $ xa\<lparr>tcb_caller := y\<rparr>)\<rparr>)) \<and> (snd z \<noteq> tcb_cnode_index 3 \<longrightarrow> (snd z = tcb_cnode_index 4 \<longrightarrow> (\<exists>y. kheap s (fst z) = Some y) \<longrightarrow> a_type (the (kheap s (fst z))) = a_type (TCB $ xa\<lparr>tcb_ipcframe := y\<rparr>) \<longrightarrow> (let slots = case x of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots in if \<exists>sl. slots = [sl] then case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> pt (UCAST(32 \<rightarrow> 8) (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte \<and> pte_range_sz pte = 0) (hd slots && ~~ mask pt_bits) and K (pte_range_sz pte = 0) | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (head slots && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (hd slots && ~~ mask pd_bits) and K (pde_range_sz pde = 0) else (\<lambda>s. \<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> (case x of Inl (pte, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl slots). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd slots && ~~ mask pt_bits) s | Inr (pde, x) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl slots). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd slots && ~~ mask pd_bits) s))) (s\<lparr>kheap := (kheap s)(fst z \<mapsto> TCB $ xa\<lparr>tcb_ipcframe := y\<rparr>)\<rparr>)) \<and> (snd z \<noteq> tcb_cnode_index 4 \<longrightarrow> True)))))) \<and> (\<forall>x. the (kheap s (fst z)) = Endpoint x \<longrightarrow> True) \<and> (\<forall>x. the (kheap s (fst z)) = Notification x \<longrightarrow> True) \<and> (\<forall>x. the (kheap s (fst z)) = ArchObj x \<longrightarrow> True) proof (prove)
goal:
No subgoals!