theory ArchVSpaceEntries_AI

lemma set_thread_state_duplicates_valid[wp]:
  "\<lbrace>invocation_duplicates_valid i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. invocation_duplicates_valid i\<rbrace>" apply (simp add: set_thread_state_def set_object_def get_object_def) apply (wp|simp)+ apply (clarsimp simp: invocation_duplicates_valid_def pti_duplicates_valid_def
                        page_inv_duplicates_valid_def page_inv_entries_safe_def
                        Let_def
                 dest!: get_tcb_SomeD
                 split: Invocations_A.invocation.split arch_invocation.split_asm
                        page_table_invocation.split
                        page_invocation.split sum.split
                        ) apply (auto simp add: obj_at_def page_inv_entries_safe_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invocation_duplicates_valid i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. invocation_duplicates_valid i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invocation_duplicates_valid i\<rbrace> do tcb <- gets_the (get_tcb t);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := st\<rparr>))\<rparr>)
od;
do_extended_op (set_thread_state_ext t)
od \<lbrace>\<lambda>rv. invocation_duplicates_valid i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invocation_duplicates_valid i s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> invocation_duplicates_valid i (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_state := st\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s tcb x11 a b x13 x14. \<lbrakk>i = InvokeArchObject (InvokePageTable (PageTableMap x11 (a, b) x13 x14)); kheap s t = Some (TCB tcb); obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (x14 && mask pd_bits >> 2) && ~~ mask 4)) = 0) (x14 && ~~ mask pd_bits) s; pde_range_sz x13 = 0\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (x14 && mask pd_bits >> 2) && ~~ mask 4)) = 0) (x14 && ~~ mask pd_bits) (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_state := st\<rparr>)) else kheap s a\<rparr>)
 2. \<And>s x10 y ya tcb x3. \<lbrakk>i = InvokeArchObject (InvokePage x3); ya = TCB tcb; kheap s t = Some (TCB tcb); y = tcb; x10 = InvokePage x3; (case x3 of PageMap asid cap ct_slot entries \<Rightarrow> page_inv_entries_safe entries | _ \<Rightarrow> \<lambda>_. True) s\<rbrakk> \<Longrightarrow> \<forall>x11 x12 a b x14. (\<forall>aa ba. x14 = Inl (aa, ba) \<longrightarrow> ((\<exists>sl. ba = [sl]) \<longrightarrow> x3 = PageMap x11 x12 (a, b) (Inl (aa, ba)) \<longrightarrow> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (hd ba && mask pt_bits >> 2) && ~~ mask 4)) = 0) (hd ba && ~~ mask pt_bits) (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_state := st\<rparr>)) else kheap s a\<rparr>) \<and> pte_range_sz aa = 0) \<and> ((\<forall>sl. ba \<noteq> [sl]) \<longrightarrow> x3 = PageMap x11 x12 (a, b) (Inl (aa, ba)) \<longrightarrow> (\<exists>p. is_aligned p 6 \<and> ba = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl ba). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd ba && ~~ mask pt_bits) (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_state := st\<rparr>)) else kheap s a\<rparr>)))) \<and> (\<forall>aa ba. x14 = Inr (aa, ba) \<longrightarrow> ((\<exists>sl. ba = [sl]) \<longrightarrow> x3 = PageMap x11 x12 (a, b) (Inr (aa, ba)) \<longrightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (hd ba && mask pd_bits >> 2) && ~~ mask 4)) = 0) (hd ba && ~~ mask pd_bits) (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_state := st\<rparr>)) else kheap s a\<rparr>) \<and> pde_range_sz aa = 0) \<and> ((\<forall>sl. ba \<noteq> [sl]) \<longrightarrow> x3 = PageMap x11 x12 (a, b) (Inr (aa, ba)) \<longrightarrow> (\<exists>p. is_aligned p 6 \<and> ba = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl ba). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd ba && ~~ mask pd_bits) (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_state := st\<rparr>)) else kheap s a\<rparr>)))) proof (prove)
goal:
No subgoals!