ainvs: reduce Finalise interface (#179)

* ainvs: reduce Finalise interface

The lemma finalise_cap_replaceable is only used in arch proofs,
so it doesn't need to be in the interface locale to generic proofs.

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

proof/invariant-abstract/ARM/ArchFinalise_AI.thy

@@ -523,7 +523,7 @@ lemma suspend_unlive':
   apply simp
   done
 
-lemma (* finalise_cap_replaceable *) [Finalise_AI_asms]:
+lemma finalise_cap_replaceable [Finalise_AI_asms]:
   "\<lbrace>\<lambda>s. s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s
         \<and> cte_wp_at ((=) cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s)
         \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s)

proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy

@@ -1290,7 +1290,7 @@ lemma arch_finalise_cap_replaceable:
    \<lbrace>\<lambda>rv s. replaceable s sl (fst rv) (cap.ArchObjectCap cap)\<rbrace>"
   by (cases cap; simp add: arch_finalise_cap_vcpu arch_finalise_cap_replaceable1)
 
-lemma (* finalise_cap_replaceable *) [Finalise_AI_asms]:
+lemma finalise_cap_replaceable [Finalise_AI_asms]:
   "\<lbrace>\<lambda>s. s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s
         \<and> cte_wp_at ((=) cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s)
         \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s)

proof/invariant-abstract/Finalise_AI.thy

@@ -119,17 +119,6 @@ locale Finalise_AI_1 =
     \<lbrace>no_cap_to_obj_with_diff_ref cap S :: 'a state \<Rightarrow> bool\<rbrace>
        suspend t
      \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace>"
-  assumes finalise_cap_replaceable:
-    "\<And> cap x sl.
-    \<lbrace>\<lambda>(s :: 'a state). s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s
-          \<and> cte_wp_at ((=) cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s)
-          \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s)
-          \<and> (is_arch_cap cap \<longrightarrow> pspace_aligned s \<and>
-                                 valid_vspace_objs s \<and>
-                                 valid_arch_state s \<and>
-                                 valid_arch_caps s)\<rbrace>
-       finalise_cap cap x
-     \<lbrace>\<lambda>rv s. replaceable s sl (fst rv) cap\<rbrace>"
   assumes deleting_irq_handler_cte_preserved:
   "\<And> P p irq.\<lbrakk> \<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap \<rbrakk>
     \<Longrightarrow> \<lbrace>cte_wp_at P p\<rbrace>

proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy

@@ -895,7 +895,7 @@ lemma prepare_thread_delete_unlive[wp]:
   apply (clarsimp simp: obj_at_def, case_tac ko, simp_all add: is_tcb_def live_def)
   done
 
-lemma (* finalise_cap_replaceable *) [Finalise_AI_asms]:
+lemma finalise_cap_replaceable [Finalise_AI_asms]:
   "\<lbrace>\<lambda>s. s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s
         \<and> cte_wp_at ((=) cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s)
         \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s)

proof/invariant-abstract/X64/ArchFinalise_AI.thy

@@ -531,7 +531,7 @@ lemma (* fpu_thread_delete_no_cap_to_obj_ref *)[wp,Finalise_AI_asms]:
    \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace>"
   by (wpsimp simp: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state)
 
-lemma (* finalise_cap_replaceable *) [Finalise_AI_asms]:
+lemma finalise_cap_replaceable [Finalise_AI_asms]:
   "\<lbrace>\<lambda>s. s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s
         \<and> cte_wp_at ((=) cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s)
         \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s)