theory ArchFinalise_AI

lemma set_asid_pool_empty_table_lookup:
  "\<lbrace>valid_vs_lookup and asid_pool_at p and
    (\<lambda>s. \<exists>p'. caps_of_state s p' = Some (ArchObjectCap (ASIDPoolCap p base)))\<rbrace>
  set_asid_pool p Map.empty
   \<lbrace>\<lambda>rv s. valid_vs_lookup
             (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table :=
                (arm_asid_table (arch_state s))(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>" apply (simp add: set_asid_pool_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def valid_vs_lookup_def
                  simp del: fun_upd_apply) apply (drule vs_lookup_pages_empty_table) apply (erule disjE) apply (fastforce simp: caps_of_state_after_update[folded fun_upd_apply]
                         obj_at_def) apply clarsimp apply (rule_tac x=a in exI) apply (rule_tac x=b in exI) apply (simp add: caps_of_state_after_update [folded fun_upd_apply] obj_at_def) apply (simp add: vs_cap_ref_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup and typ_at (AArch AASIDPool) p and (\<lambda>s. \<exists>p'. caps_of_state s p' = Some (ArchObjectCap (ASIDPoolCap p base)))\<rbrace> set_asid_pool p (\<lambda>x. None) \<lbrace>\<lambda>rv s. valid_vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup and typ_at (AArch AASIDPool) p and (\<lambda>s. \<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)))\<rbrace> do kobj <- get_object p;
y <- assert (a_type kobj = a_type (ArchObj (ASIDPool (\<lambda>x. None))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>)
od \<lbrace>\<lambda>rv s. valid_vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_vs_lookup and typ_at (AArch AASIDPool) p and (\<lambda>s. \<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)))) s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))) \<longrightarrow> valid_vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>)\<lparr>arm_asid_table := (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a b ap pa ref. \<lbrakk>\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (\<lambda>x. None))); (ref \<unrhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrakk> \<Longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>) (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref) proof (prove)
goal (1 subgoal):
 1. \<And>s a b ap pa ref. \<lbrakk>\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (\<lambda>x. None))); (ref \<unrhd> pa) s \<or> ref = [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<and> pa = p\<rbrakk> \<Longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>) (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref) proof (prove)
goal (2 subgoals):
 1. \<And>s a b ap pa ref. \<lbrakk>\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (\<lambda>x. None))); (ref \<unrhd> pa) s\<rbrakk> \<Longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>) (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)
 2. \<And>s a b ap pa ref. \<lbrakk>\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (\<lambda>x. None))); ref = [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<and> pa = p\<rbrakk> \<Longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>) (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref) proof (prove)
goal (1 subgoal):
 1. \<And>s a b ap pa ref. \<lbrakk>\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (\<lambda>x. None))); ref = [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<and> pa = p\<rbrakk> \<Longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>) (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref) proof (prove)
goal (1 subgoal):
 1. \<And>s a b ap. \<lbrakk>\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (\<lambda>x. None)))\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>) (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] proof (prove)
goal (1 subgoal):
 1. \<And>s a b ap. \<lbrakk>\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (\<lambda>x. None)))\<rbrakk> \<Longrightarrow> \<exists>b cap. caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>) (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] proof (prove)
goal (1 subgoal):
 1. \<And>s a b ap. \<lbrakk>\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (\<lambda>x. None)))\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>) (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] proof (prove)
goal (1 subgoal):
 1. \<And>s a b ap. \<lbrakk>\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (\<lambda>x. None)))\<rbrakk> \<Longrightarrow> vs_cap_ref (ArchObjectCap (ASIDPoolCap p base)) = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] proof (prove)
goal:
No subgoals!