ainvs: sync ARM/ARM_HYP/X64 with lemmas that are now arch dependent

proof/invariant-abstract/ARM/ArchAcc_AI.thy

@@ -1904,6 +1904,11 @@ lemma valid_pde_typ_at:
    valid_pde pde s = valid_pde pde s'"
   by (case_tac pde, auto simp add: data_at_def)
 
+lemma valid_vspace_obj_same_type:
+  "\<lbrakk>valid_vspace_obj ao s;  kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk>
+  \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> ko')\<rparr>)"
+    apply (rule hoare_to_pure_kheap_upd[OF valid_vspace_obj_typ])
+    by (auto simp: obj_at_def)
 
 lemma set_asid_pool_global_objs [wp]:
   "\<lbrace>valid_global_objs and valid_arch_state\<rbrace>

proof/invariant-abstract/ARM/ArchCSpaceInv_AI.thy

@@ -36,6 +36,22 @@ lemma set_cap_ioports':
   \<lbrace>\<lambda>rv. valid_ioports\<rbrace>"
   by wpsimp
 
+lemma unique_table_refs_no_cap_asidE:
+  "\<lbrakk>caps_of_state s p = Some cap;
+    unique_table_refs (caps_of_state s)\<rbrakk>
+   \<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s"
+  apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def
+                        cte_wp_at_caps_of_state)
+  apply (unfold unique_table_refs_def)
+  apply (drule_tac x=p in spec, drule_tac x="(a,b)" in spec)
+  apply (drule spec)+
+  apply (erule impE, assumption)+
+  apply (clarsimp simp: is_cap_simps)
+  done
+
+lemmas unique_table_refs_no_cap_asidD
+     = unique_table_refs_no_cap_asidE[where S="{}"]
+
 lemma replace_cap_invs:
   "\<lbrace>\<lambda>s. invs s \<and> cte_wp_at (replaceable s p cap) p s
         \<and> cap \<noteq> cap.NullCap

proof/invariant-abstract/ARM/ArchCSpace_AI.thy

@@ -127,6 +127,48 @@ lemma set_free_index_invs [CSpace_AI_assms]:
   apply simp
   done
 
+lemma unique_table_refs_upd_eqD:
+  "\<lbrakk>ms a = Some b; obj_refs b = obj_refs b'; table_cap_ref b = table_cap_ref b'\<rbrakk>
+   \<Longrightarrow> unique_table_refs (ms (a \<mapsto> b')) = unique_table_refs ms"
+  unfolding unique_table_refs_def
+  apply (rule iffI)
+   apply (intro allI impI)
+   apply (case_tac "p=p'")
+    apply simp
+   apply (case_tac "a=p")
+    apply (erule_tac x=p in allE)
+    apply (erule_tac x=p' in allE)
+    apply (erule_tac x=b' in allE)
+    apply simp
+   apply (case_tac "a=p'")
+    apply (erule_tac x=p in allE)
+    apply (erule_tac x=p' in allE)
+    apply (erule_tac x=cap in allE)
+    apply simp
+   apply (erule_tac x=p in allE)
+   apply (erule_tac x=p' in allE)
+   apply (erule_tac x=cap in allE)
+   apply simp
+  apply (intro allI impI)
+  apply (case_tac "p=p'")
+   apply (thin_tac " \<forall>p. P p" for P)
+   apply simp
+  apply (case_tac "a=p")
+   apply (erule_tac x=p in allE)
+   apply (erule_tac x=p' in allE)
+   apply (erule_tac x=b in allE)
+   apply simp
+  apply (case_tac "a=p'")
+   apply (erule_tac x=p in allE)
+   apply (erule_tac x=p' in allE)
+   apply (erule_tac x=cap in allE)
+   apply simp
+  apply (erule_tac x=p in allE)
+  apply (erule_tac x=p' in allE)
+  apply (erule_tac x=cap in allE)
+  apply simp
+  done
+
 lemma set_untyped_cap_as_full_valid_arch_caps [CSpace_AI_assms]:
   "\<lbrace>valid_arch_caps and cte_wp_at ((=) src_cap) src\<rbrace>
    set_untyped_cap_as_full src_cap cap src

proof/invariant-abstract/ARM/ArchDetype_AI.thy

@@ -365,6 +365,14 @@ lemma valid_table_caps:
   apply (metis detype_arch_state no_obj_refs)
   done
 
+lemma unique_table_refs:
+    "\<And>cps P. unique_table_refs cps
+             \<Longrightarrow> unique_table_refs (\<lambda>x. if P x then None else cps x)"
+    apply (simp only: unique_table_refs_def option.simps
+                      simp_thms
+               split: if_split)
+    apply blast
+    done
 
 lemma valid_arch_caps_detype[detype_invs_proofs]: "valid_arch_caps (detype (untyped_range cap) s)"
   using valid_arch_caps  by (simp add: valid_arch_caps_def

proof/invariant-abstract/ARM/ArchVSpace_AI.thy

@@ -5058,5 +5058,12 @@ lemma invs_aligned_pdD:
   apply (simp add: pd_bits_def pageBits_def)
   done
 
+lemma valid_vspace_obj_default:
+  assumes tyunt: "ty \<noteq> Structures_A.apiobject_type.Untyped"
+  shows "ArchObj ao = default_object ty dev us \<Longrightarrow> valid_vspace_obj ao s'"
+  apply (cases ty, simp_all add: default_object_def tyunt)
+  apply (simp add: valid_vspace_obj_default')
+  done
+
 end
 end

proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy

@@ -1943,6 +1943,11 @@ lemma set_asid_pool_vspace_objs_unmap':
   apply fastforce
   done
 
+lemma valid_vspace_obj_same_type:
+  "\<lbrakk>valid_vspace_obj ao s;  kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk>
+  \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> ko')\<rparr>)"
+    apply (rule hoare_to_pure_kheap_upd[OF valid_vspace_obj_typ])
+    by (auto simp: obj_at_def)
 
 lemma set_asid_pool_vspace_objs_unmap:
   "\<lbrace>valid_vspace_objs and ko_at (ArchObj (ASIDPool ap)) p\<rbrace>

proof/invariant-abstract/ARM_HYP/ArchCSpaceInv_AI.thy

@@ -36,6 +36,22 @@ lemma set_cap_ioports':
   \<lbrace>\<lambda>rv. valid_ioports\<rbrace>"
   by wpsimp
 
+lemma unique_table_refs_no_cap_asidE:
+  "\<lbrakk>caps_of_state s p = Some cap;
+    unique_table_refs (caps_of_state s)\<rbrakk>
+   \<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s"
+  apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def
+                        cte_wp_at_caps_of_state)
+  apply (unfold unique_table_refs_def)
+  apply (drule_tac x=p in spec, drule_tac x="(a,b)" in spec)
+  apply (drule spec)+
+  apply (erule impE, assumption)+
+  apply (clarsimp simp: is_cap_simps)
+  done
+
+lemmas unique_table_refs_no_cap_asidD
+     = unique_table_refs_no_cap_asidE[where S="{}"]
+
 lemma replace_cap_invs:
   "\<lbrace>\<lambda>s. invs s \<and> cte_wp_at (replaceable s p cap) p s
         \<and> cap \<noteq> cap.NullCap

proof/invariant-abstract/ARM_HYP/ArchCSpace_AI.thy

@@ -126,6 +126,48 @@ lemma set_free_index_invs [CSpace_AI_assms]:
   apply (simp)
   done
 
+lemma unique_table_refs_upd_eqD:
+  "\<lbrakk>ms a = Some b; obj_refs b = obj_refs b'; table_cap_ref b = table_cap_ref b'\<rbrakk>
+   \<Longrightarrow> unique_table_refs (ms (a \<mapsto> b')) = unique_table_refs ms"
+  unfolding unique_table_refs_def
+  apply (rule iffI)
+   apply (intro allI impI)
+   apply (case_tac "p=p'")
+    apply simp
+   apply (case_tac "a=p")
+    apply (erule_tac x=p in allE)
+    apply (erule_tac x=p' in allE)
+    apply (erule_tac x=b' in allE)
+    apply simp
+   apply (case_tac "a=p'")
+    apply (erule_tac x=p in allE)
+    apply (erule_tac x=p' in allE)
+    apply (erule_tac x=cap in allE)
+    apply simp
+   apply (erule_tac x=p in allE)
+   apply (erule_tac x=p' in allE)
+   apply (erule_tac x=cap in allE)
+   apply simp
+  apply (intro allI impI)
+  apply (case_tac "p=p'")
+   apply (thin_tac " \<forall>p. P p" for P)
+   apply simp
+  apply (case_tac "a=p")
+   apply (erule_tac x=p in allE)
+   apply (erule_tac x=p' in allE)
+   apply (erule_tac x=b in allE)
+   apply simp
+  apply (case_tac "a=p'")
+   apply (erule_tac x=p in allE)
+   apply (erule_tac x=p' in allE)
+   apply (erule_tac x=cap in allE)
+   apply simp
+  apply (erule_tac x=p in allE)
+  apply (erule_tac x=p' in allE)
+  apply (erule_tac x=cap in allE)
+  apply simp
+  done
+
 lemma set_untyped_cap_as_full_valid_arch_caps [CSpace_AI_assms]:
   "\<lbrace>valid_arch_caps and cte_wp_at ((=) src_cap) src\<rbrace>
    set_untyped_cap_as_full src_cap cap src

proof/invariant-abstract/ARM_HYP/ArchDetype_AI.thy

@@ -438,6 +438,14 @@ lemma valid_table_caps:
   apply (metis no_obj_refs)
   done
 
+lemma unique_table_refs:
+    "\<And>cps P. unique_table_refs cps
+             \<Longrightarrow> unique_table_refs (\<lambda>x. if P x then None else cps x)"
+    apply (simp only: unique_table_refs_def option.simps
+                      simp_thms
+               split: if_split)
+    apply blast
+    done
 
 lemma valid_arch_caps_detype[detype_invs_proofs]: "valid_arch_caps (detype (untyped_range cap) s)"
   using valid_arch_caps  by (simp add: valid_arch_caps_def

proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy

@@ -6173,5 +6173,12 @@ lemma perform_asid_pool_invs [wp]:
   apply (clarsimp simp: obj_at_def)
   done
 
+lemma valid_vspace_obj_default:
+  assumes tyunt: "ty \<noteq> Structures_A.apiobject_type.Untyped"
+  shows "ArchObj ao = default_object ty dev us \<Longrightarrow> valid_vspace_obj ao s'"
+  apply (cases ty, simp_all add: default_object_def tyunt)
+  apply (simp add: valid_vspace_obj_default')
+  done
+
 end
 end

proof/invariant-abstract/X64/ArchAcc_AI.thy

@@ -1719,6 +1719,11 @@ lemma vs_lookup_pages_pt_eq:
           split: pml4e.splits pdpte.splits pde.splits pte.splits
            elim: vs_lookup_pdI)
 
+lemma valid_vspace_obj_same_type:
+  "\<lbrakk>valid_vspace_obj ao s;  kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk>
+  \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> ko')\<rparr>)"
+    apply (rule hoare_to_pure_kheap_upd[OF valid_vspace_obj_typ])
+    by (auto simp: obj_at_def)
 
 lemmas invs_ran_asid_table = invs_valid_asid_table[THEN valid_asid_table_ran]
 

proof/invariant-abstract/X64/ArchCSpaceInv_AI.thy

@@ -76,6 +76,22 @@ lemma valid_ioportsD:
   apply (simp add: valid_ioports_def ioports_no_overlap_def)
   by auto
 
+lemma unique_table_refs_no_cap_asidE:
+  "\<lbrakk>caps_of_state s p = Some cap;
+    unique_table_refs (caps_of_state s)\<rbrakk>
+   \<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s"
+  apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def
+                        cte_wp_at_caps_of_state)
+  apply (unfold unique_table_refs_def)
+  apply (drule_tac x=p in spec, drule_tac x="(a,b)" in spec)
+  apply (drule spec)+
+  apply (erule impE, assumption)+
+  apply (clarsimp simp: is_cap_simps)
+  done
+
+lemmas unique_table_refs_no_cap_asidD
+     = unique_table_refs_no_cap_asidE[where S="{}"]
+
 lemma replace_cap_invs:
   "\<lbrace>\<lambda>s. invs s \<and> cte_wp_at (replaceable s p cap) p s
         \<and> cap \<noteq> cap.NullCap

proof/invariant-abstract/X64/ArchCSpace_AI.thy

@@ -129,6 +129,48 @@ lemma set_free_index_invs [CSpace_AI_assms]:
    apply (simp add: cap_range_def)+
   done
 
+lemma unique_table_refs_upd_eqD:
+  "\<lbrakk>ms a = Some b; obj_refs b = obj_refs b'; table_cap_ref b = table_cap_ref b'\<rbrakk>
+   \<Longrightarrow> unique_table_refs (ms (a \<mapsto> b')) = unique_table_refs ms"
+  unfolding unique_table_refs_def
+  apply (rule iffI)
+   apply (intro allI impI)
+   apply (case_tac "p=p'")
+    apply simp
+   apply (case_tac "a=p")
+    apply (erule_tac x=p in allE)
+    apply (erule_tac x=p' in allE)
+    apply (erule_tac x=b' in allE)
+    apply simp
+   apply (case_tac "a=p'")
+    apply (erule_tac x=p in allE)
+    apply (erule_tac x=p' in allE)
+    apply (erule_tac x=cap in allE)
+    apply simp
+   apply (erule_tac x=p in allE)
+   apply (erule_tac x=p' in allE)
+   apply (erule_tac x=cap in allE)
+   apply simp
+  apply (intro allI impI)
+  apply (case_tac "p=p'")
+   apply (thin_tac " \<forall>p. P p" for P)
+   apply simp
+  apply (case_tac "a=p")
+   apply (erule_tac x=p in allE)
+   apply (erule_tac x=p' in allE)
+   apply (erule_tac x=b in allE)
+   apply simp
+  apply (case_tac "a=p'")
+   apply (erule_tac x=p in allE)
+   apply (erule_tac x=p' in allE)
+   apply (erule_tac x=cap in allE)
+   apply simp
+  apply (erule_tac x=p in allE)
+  apply (erule_tac x=p' in allE)
+  apply (erule_tac x=cap in allE)
+  apply simp
+  done
+
 lemma set_untyped_cap_as_full_valid_arch_caps [CSpace_AI_assms]:
   "\<lbrace>valid_arch_caps and cte_wp_at ((=) src_cap) src\<rbrace>
    set_untyped_cap_as_full src_cap cap src

proof/invariant-abstract/X64/ArchDetype_AI.thy

@@ -372,6 +372,14 @@ lemma valid_table_caps:
   apply (metis detype_arch_state no_obj_refs)
   done
 
+lemma unique_table_refs:
+    "\<And>cps P. unique_table_refs cps
+             \<Longrightarrow> unique_table_refs (\<lambda>x. if P x then None else cps x)"
+    apply (simp only: unique_table_refs_def option.simps
+                      simp_thms
+               split: if_split)
+    apply blast
+    done
 
 lemma valid_arch_caps_detype[detype_invs_proofs]: "valid_arch_caps (detype (untyped_range cap) s)"
   using valid_arch_caps  by (simp add: valid_arch_caps_def

proof/invariant-abstract/X64/ArchVSpace_AI.thy

@@ -3960,5 +3960,12 @@ lemmas diminished_table_cap_simps
 
 end
 
+lemma valid_vspace_obj_default:
+  assumes tyunt: "ty \<noteq> Structures_A.apiobject_type.Untyped"
+  shows "ArchObj ao = default_object ty dev us \<Longrightarrow> valid_vspace_obj ao s'"
+  apply (cases ty, simp_all add: default_object_def tyunt)
+  apply (simp add: valid_vspace_obj_default')
+  done
+
 end
 end