theory ArchAcc_AI

lemma set_pt_vs_lookup [wp]:
  "\<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> set_pt p pt \<lbrace>\<lambda>x s. P (vs_lookup s)\<rbrace>" unfolding set_pt_def including unfold_objects apply (wpsimp wp: set_object_wp_strong simp: a_type_def) apply (erule rsubst [where P=P]) apply (rule order_antisym) apply (rule vs_lookup_sub) apply (clarsimp simp: vs_refs_def) prefer 3 apply (rule vs_lookup_sub) apply (clarsimp simp: vs_refs_def split: if_split_asm) apply blast+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> set_pt p pt \<lbrace>\<lambda>x s. P (vs_lookup s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>x s. P (vs_lookup s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>x s. P (vs_lookup s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>P (vs_lookup s); kheap s p = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> P (vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> vs_lookup s = vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> vs_lookup s \<subseteq> vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)
 2. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) \<subseteq> vs_lookup s proof (prove)
goal (3 subgoals):
 1. \<And>s x2 ko pa. \<lbrakk>kheap s p = Some (ArchObj (PageTable x2)); ko_at ko pa s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)
 2. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> graph_of (asid_table s) \<subseteq> graph_of (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>))
 3. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) \<subseteq> vs_lookup s proof (prove)
goal (3 subgoals):
 1. \<And>s x2 ko pa x5. \<lbrakk>kheap s p = Some (ArchObj (PageTable x2)); kheap s pa = Some ko\<rbrakk> \<Longrightarrow> (\<forall>x1. x5 = ASIDPool x1 \<longrightarrow> ko = ArchObj (ASIDPool x1) \<longrightarrow> pa = p \<longrightarrow> graph_of x1 = {}) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> ko = ArchObj (PageDirectory x3) \<longrightarrow> pa = p \<longrightarrow> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x)) = {})
 2. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> graph_of (asid_table s) \<subseteq> graph_of (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>))
 3. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) \<subseteq> vs_lookup s proof (prove)
goal (3 subgoals):
 1. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) \<subseteq> vs_lookup s
 2. \<And>s x2 ko pa x5. \<lbrakk>kheap s p = Some (ArchObj (PageTable x2)); kheap s pa = Some ko\<rbrakk> \<Longrightarrow> (\<forall>x1. x5 = ASIDPool x1 \<longrightarrow> ko = ArchObj (ASIDPool x1) \<longrightarrow> pa = p \<longrightarrow> graph_of x1 = {}) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> ko = ArchObj (PageDirectory x3) \<longrightarrow> pa = p \<longrightarrow> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x)) = {})
 3. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> graph_of (asid_table s) \<subseteq> graph_of (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)) proof (prove)
goal (4 subgoals):
 1. \<And>s x2 ko pa. \<lbrakk>kheap s p = Some (ArchObj (PageTable x2)); ko_at ko pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') pa s
 2. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> graph_of (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)) \<subseteq> graph_of (asid_table s)
 3. \<And>s x2 ko pa x5. \<lbrakk>kheap s p = Some (ArchObj (PageTable x2)); kheap s pa = Some ko\<rbrakk> \<Longrightarrow> (\<forall>x1. x5 = ASIDPool x1 \<longrightarrow> ko = ArchObj (ASIDPool x1) \<longrightarrow> pa = p \<longrightarrow> graph_of x1 = {}) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> ko = ArchObj (PageDirectory x3) \<longrightarrow> pa = p \<longrightarrow> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x)) = {})
 4. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> graph_of (asid_table s) \<subseteq> graph_of (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)) proof (prove)
goal (5 subgoals):
 1. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> \<exists>ko. (\<forall>x11 x12. ko \<noteq> CNode x11 x12) \<and> (\<forall>x2. ko \<noteq> TCB x2) \<and> (\<forall>x3. ko \<noteq> Endpoint x3) \<and> (\<forall>x4. ko \<noteq> Notification x4) \<and> (\<forall>x5. ko = ArchObj x5 \<longrightarrow> PageTable x2 = x5)
 2. \<And>s x2 ko pa x5. \<lbrakk>kheap s p = Some (ArchObj (PageTable x2)); pa \<noteq> p; kheap s pa = Some ko\<rbrakk> \<Longrightarrow> (\<forall>x1. x5 = ASIDPool x1 \<longrightarrow> ko = ArchObj (ASIDPool x1) \<longrightarrow> (\<exists>ko. (\<forall>x11 x12. ko \<noteq> CNode x11 x12) \<and> (\<forall>x2. ko \<noteq> TCB x2) \<and> (\<forall>x3. ko \<noteq> Endpoint x3) \<and> (\<forall>x4. ko \<noteq> Notification x4) \<and> (\<forall>x5. (\<forall>x1a. x5 = ASIDPool x1a \<longrightarrow> ko = ArchObj (ASIDPool x1a) \<longrightarrow> x1 = x1a \<and> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` graph_of x1 \<subseteq> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` graph_of x1a) \<and> (\<forall>x2. x5 = PageTable x2 \<longrightarrow> ko \<noteq> ArchObj (PageTable x2)) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> ko \<noteq> ArchObj (PageDirectory x3)) \<and> (\<forall>x41 x42. x5 = DataPage x41 x42 \<longrightarrow> ko \<noteq> ArchObj (DataPage x41 x42))))) \<and> (\<forall>x2. x5 = PageTable x2 \<longrightarrow> ko = ArchObj (PageTable x2) \<longrightarrow> (\<exists>ko. (\<forall>x11 x12. ko \<noteq> CNode x11 x12) \<and> (\<forall>x2. ko \<noteq> TCB x2) \<and> (\<forall>x3. ko \<noteq> Endpoint x3) \<and> (\<forall>x4. ko \<noteq> Notification x4) \<and> (\<forall>x5. ko = ArchObj x5 \<longrightarrow> PageTable x2 = x5))) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> ko = ArchObj (PageDirectory x3) \<longrightarrow> (\<exists>ko. (\<forall>x11 x12. ko \<noteq> CNode x11 x12) \<and> (\<forall>x2. ko \<noteq> TCB x2) \<and> (\<forall>x3. ko \<noteq> Endpoint x3) \<and> (\<forall>x4. ko \<noteq> Notification x4) \<and> (\<forall>x5. (\<forall>x1. x5 = ASIDPool x1 \<longrightarrow> ko \<noteq> ArchObj (ASIDPool x1)) \<and> (\<forall>x2. x5 = PageTable x2 \<longrightarrow> ko \<noteq> ArchObj (PageTable x2)) \<and> (\<forall>x3a. x5 = PageDirectory x3a \<longrightarrow> ko = ArchObj (PageDirectory x3a) \<longrightarrow> x3 = x3a \<and> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x)) \<subseteq> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3a x))) \<and> (\<forall>x41 x42. x5 = DataPage x41 x42 \<longrightarrow> ko \<noteq> ArchObj (DataPage x41 x42))))) \<and> (\<forall>x41 x42. x5 = DataPage x41 x42 \<longrightarrow> ko = ArchObj (DataPage x41 x42) \<longrightarrow> (\<exists>ko. (\<forall>x11 x12. ko \<noteq> CNode x11 x12) \<and> (\<forall>x2. ko \<noteq> TCB x2) \<and> (\<forall>x3. ko \<noteq> Endpoint x3) \<and> (\<forall>x4. ko \<noteq> Notification x4) \<and> (\<forall>x5. ko = ArchObj x5 \<longrightarrow> DataPage x41 x42 = x5)))
 3. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> graph_of (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)) \<subseteq> graph_of (asid_table s)
 4. \<And>s x2 ko pa x5. \<lbrakk>kheap s p = Some (ArchObj (PageTable x2)); kheap s pa = Some ko\<rbrakk> \<Longrightarrow> (\<forall>x1. x5 = ASIDPool x1 \<longrightarrow> ko = ArchObj (ASIDPool x1) \<longrightarrow> pa = p \<longrightarrow> graph_of x1 = {}) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> ko = ArchObj (PageDirectory x3) \<longrightarrow> pa = p \<longrightarrow> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x)) = {})
 5. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> graph_of (asid_table s) \<subseteq> graph_of (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)) proof (prove)
goal (3 subgoals):
 1. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> graph_of (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)) \<subseteq> graph_of (asid_table s)
 2. \<And>s x2 ko pa x5. \<lbrakk>kheap s p = Some (ArchObj (PageTable x2)); kheap s pa = Some ko\<rbrakk> \<Longrightarrow> (\<forall>x1. x5 = ASIDPool x1 \<longrightarrow> ko = ArchObj (ASIDPool x1) \<longrightarrow> pa = p \<longrightarrow> graph_of x1 = {}) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> ko = ArchObj (PageDirectory x3) \<longrightarrow> pa = p \<longrightarrow> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x)) = {})
 3. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> graph_of (asid_table s) \<subseteq> graph_of (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)) proof (prove)
goal:
No subgoals!