squash arm access: more PR feedback

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
seL4 · Feb 10, 2025 · fc3d64b · fc3d64b
1 parent e3797a8
commit fc3d64b
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 13 deletions.
diff --git a/proof/access-control/ARM/ArchAccess.thy b/proof/access-control/ARM/ArchAccess.thy
@@ -143,7 +143,6 @@ abbreviation integrity_asids_aux ::
      pp_opt = pp_opt' \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of asid
                                  \<longrightarrow> pasASIDAbs aag asid' \<in> subjects)"
 
-\<comment> \<open>FIXME: could we define integrity_asids to operate on arch_state only?\<close>
 definition integrity_asids ::
   "'a PAS \<Rightarrow> 'a set \<Rightarrow> obj_ref \<Rightarrow> asid \<Rightarrow> 'y::state_ext state \<Rightarrow> 'z:: state_ext state  \<Rightarrow> bool" where
   "integrity_asids aag subjects x a s s' \<equiv>

diff --git a/proof/access-control/ARM/ArchRetype_AC.thy b/proof/access-control/ARM/ArchRetype_AC.thy
@@ -33,18 +33,6 @@ end
 
 context retype_region_proofs' begin interpretation Arch .
 
-\<comment> \<open>FIXME: move to pas_refined_state_objs_to_policy_subset?\<close>
-lemma pas_refined_subsets_tcb_domain_map_wellformed:
-  "\<lbrakk> pas_refined aag s;
-     state_objs_to_policy s' \<subseteq> state_objs_to_policy s;
-     state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s;
-     state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s;
-     tcb_domain_map_wellformed aag s \<Longrightarrow> tcb_domain_map_wellformed aag s';
-     interrupt_irq_node s' = interrupt_irq_node s \<rbrakk>
-     \<Longrightarrow> pas_refined aag s'"
-  by (simp add: pas_refined_def)
-     (blast dest: auth_graph_map_mono[where G="pasObjectAbs aag"])
-
 lemma pas_refined:
   "\<lbrakk> invs s; pas_refined aag s; pas_cur_domain aag s; \<forall>x\<in> set (retype_addrs ptr ty n us). is_subject aag x \<rbrakk>
    \<Longrightarrow> pas_refined aag s'"

diff --git a/proof/access-control/Access_AC.thy b/proof/access-control/Access_AC.thy
@@ -263,6 +263,17 @@ lemma pas_refined_state_objs_to_policy_subset:
   by (simp add: pas_refined_def)
      (blast dest: tcb_domain_map_wellformed_mono auth_graph_map_mono[where G="pasObjectAbs aag"])
 
+lemma pas_refined_subsets_tcb_domain_map_wellformed:
+  "\<lbrakk> pas_refined aag s;
+     state_objs_to_policy s' \<subseteq> state_objs_to_policy s;
+     state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s;
+     state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s;
+     tcb_domain_map_wellformed aag s \<Longrightarrow> tcb_domain_map_wellformed aag s';
+     interrupt_irq_node s' = interrupt_irq_node s \<rbrakk>
+     \<Longrightarrow> pas_refined aag s'"
+  by (simp add: pas_refined_def)
+     (blast dest: auth_graph_map_mono[where G="pasObjectAbs aag"])
+
 lemma aag_wellformed_all_auth_is_owns':
   "\<lbrakk> Control \<in> S; pas_wellformed aag \<rbrakk>
      \<Longrightarrow> (\<forall>auth \<in> S. aag_has_auth_to aag auth x) = (is_subject aag x)"