ainvs: disambiguate acap_rights_update_id

Rename the wellformed_acap version to wf_acap_rights_update_id, and the valid_arch_cap version to valid_acap_rights_update_id. Signed-off-by: Rafal Kolanski <[email protected]>
seL4 · Jul 23, 2024 · d5e6166 · d5e6166
1 parent a585ab0
commit d5e6166
Show file tree

Hide file tree

Showing 12 changed files with 16 additions and 20 deletions.
diff --git a/proof/invariant-abstract/AARCH64/ArchCSpaceInvPre_AI.thy b/proof/invariant-abstract/AARCH64/ArchCSpaceInvPre_AI.thy
@@ -363,7 +363,7 @@ lemma cap_master_arch_cap_rights [simp]:
   by (simp add: cap_master_arch_cap_def acap_rights_update_def
            split: arch_cap.splits)
 
-lemma acap_rights_update_id [intro!, simp]:
+lemma valid_acap_rights_update_id [intro!, simp]:
   "valid_arch_cap ac s \<Longrightarrow> acap_rights_update (acap_rights ac) ac = ac"
   unfolding acap_rights_update_def acap_rights_def valid_arch_cap_def
   by (cases ac; simp)

diff --git a/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy b/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy
@@ -1272,7 +1272,7 @@ lemma aobj_at_default_arch_cap_valid:
 
 lemmas aobj_ref_default = aobj_ref_arch_cap
 
-lemma acap_rights_update_id [intro!, simp]:
+lemma wf_acap_rights_update_id [intro!, simp]:
   "wellformed_acap cap \<Longrightarrow> acap_rights_update (acap_rights cap) cap = cap"
   unfolding acap_rights_update_def
   by (auto split: arch_cap.splits option.splits)

diff --git a/proof/invariant-abstract/ARM/ArchCSpaceInvPre_AI.thy b/proof/invariant-abstract/ARM/ArchCSpaceInvPre_AI.thy
@@ -293,7 +293,7 @@ lemma cap_master_arch_cap_rights [simp]:
   by (simp add: cap_master_arch_cap_def acap_rights_update_def
            split: arch_cap.splits)
 
-lemma acap_rights_update_id [intro!, simp]:
+lemma valid_acap_rights_update_id [intro!, simp]:
   "valid_arch_cap ac s \<Longrightarrow> acap_rights_update (acap_rights ac) ac = ac"
   unfolding acap_rights_update_def acap_rights_def valid_arch_cap_def
   by (cases ac; simp)

diff --git a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy
@@ -2153,7 +2153,7 @@ lemma vs_cap_ref_eq_imp_table_cap_ref_eq:
                   arch_cap_fun_lift_def
           split: cap.splits arch_cap.splits vmpage_size.splits option.splits)
 
-lemma acap_rights_update_id [intro!, simp]:
+lemma wf_acap_rights_update_id [intro!, simp]:
   "\<lbrakk>wellformed_acap cap\<rbrakk> \<Longrightarrow> acap_rights_update (acap_rights cap) cap = cap"
   unfolding wellformed_acap_def acap_rights_update_def
   by (auto split: arch_cap.splits)

diff --git a/proof/invariant-abstract/ARM_HYP/ArchCSpaceInvPre_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchCSpaceInvPre_AI.thy
@@ -293,7 +293,7 @@ lemma cap_master_arch_cap_rights [simp]:
   by (simp add: cap_master_arch_cap_def acap_rights_update_def
            split: arch_cap.splits)
 
-lemma acap_rights_update_id [intro!, simp]:
+lemma valid_acap_rights_update_id [intro!, simp]:
   "valid_arch_cap ac s \<Longrightarrow> acap_rights_update (acap_rights ac) ac = ac"
   unfolding acap_rights_update_def acap_rights_def valid_arch_cap_def
   by (cases ac; simp)

diff --git a/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy
@@ -2162,7 +2162,7 @@ lemma valid_vspace_objs_lift:
   apply (rule valid_vspace_obj_typ [OF z], auto)
   done
 
-lemma acap_rights_update_id [intro!, simp]:
+lemma wf_acap_rights_update_id [intro!, simp]:
   "\<lbrakk>wellformed_acap cap\<rbrakk> \<Longrightarrow> acap_rights_update (acap_rights cap) cap = cap"
   unfolding wellformed_acap_def acap_rights_update_def
   by (auto split: arch_cap.splits)

diff --git a/proof/invariant-abstract/CSpaceInv_AI.thy b/proof/invariant-abstract/CSpaceInv_AI.thy
@@ -18,11 +18,6 @@ arch_requalify_consts
   replaceable_non_final_arch_cap
   unique_table_refs
 
-(* There are multiple arch-dependent acap_rights_update_id, one for wellformed_acap,
-   one for valid_arch_cap. Prefer the latter. *)
-arch_requalify_facts (aliasing)
-  acap_rights_update_id
-
 arch_requalify_facts
   aobj_ref_acap_rights_update
   arch_obj_size_acap_rights_update
@@ -31,6 +26,7 @@ arch_requalify_facts
   unique_table_refs_def
   valid_ipc_buffer_cap_def
   acap_rights_update_idem
+  valid_acap_rights_update_id
   cap_master_arch_cap_rights
   is_nondevice_page_cap_simps
   set_cap_hyp_refs_of
@@ -52,10 +48,10 @@ lemma is_valid_vtable_root_simps[simp]:
 
 lemmas [simp] = aobj_ref_acap_rights_update arch_obj_size_acap_rights_update
   valid_validate_vm_rights cap_master_arch_inv acap_rights_update_idem
-  cap_master_arch_cap_rights acap_rights_update_id state_hyp_refs_of_revokable
+  cap_master_arch_cap_rights valid_acap_rights_update_id state_hyp_refs_of_revokable
 
 lemmas [intro] = valid_arch_cap_acap_rights_update
-lemmas [intro!] = acap_rights_update_id
+lemmas [intro!] = valid_acap_rights_update_id
 lemmas [wp] = set_cap_hyp_refs_of
 
 lemma remove_rights_cap_valid[simp]:

diff --git a/proof/invariant-abstract/Invariants_AI.thy b/proof/invariant-abstract/Invariants_AI.thy
@@ -78,7 +78,7 @@ arch_requalify_facts
   valid_arch_state_lift
   aobj_at_default_arch_cap_valid
   aobj_ref_default
-  acap_rights_update_id
+  wf_acap_rights_update_id
   physical_arch_cap_has_ref
   wellformed_arch_default
   valid_vspace_obj_default'
@@ -114,9 +114,9 @@ lemmas [simp] =
   iarch_tcb_context_set
   iarch_tcb_set_registers
 
-lemmas [intro!] = idle_global acap_rights_update_id
+lemmas [intro!] = idle_global wf_acap_rights_update_id
 
-lemmas [simp] = acap_rights_update_id state_hyp_refs_update
+lemmas [simp] = wf_acap_rights_update_id state_hyp_refs_update
                 tcb_arch_ref_simps hyp_live_tcb_simps hyp_refs_of_simps
 
 

diff --git a/proof/invariant-abstract/RISCV64/ArchCSpaceInvPre_AI.thy b/proof/invariant-abstract/RISCV64/ArchCSpaceInvPre_AI.thy
@@ -368,7 +368,7 @@ lemma cap_master_arch_cap_rights [simp]:
   by (simp add: cap_master_arch_cap_def acap_rights_update_def
            split: arch_cap.splits)
 
-lemma acap_rights_update_id [intro!, simp]:
+lemma valid_acap_rights_update_id [intro!, simp]:
   "valid_arch_cap ac s \<Longrightarrow> acap_rights_update (acap_rights ac) ac = ac"
   unfolding acap_rights_update_def acap_rights_def valid_arch_cap_def
   by (cases ac; simp)

diff --git a/proof/invariant-abstract/RISCV64/ArchInvariants_AI.thy b/proof/invariant-abstract/RISCV64/ArchInvariants_AI.thy
@@ -1082,7 +1082,7 @@ lemma aobj_at_default_arch_cap_valid:
 
 lemmas aobj_ref_default = aobj_ref_arch_cap
 
-lemma acap_rights_update_id [intro!, simp]:
+lemma wf_acap_rights_update_id [intro!, simp]:
   "wellformed_acap cap \<Longrightarrow> acap_rights_update (acap_rights cap) cap = cap"
   unfolding acap_rights_update_def
   by (auto split: arch_cap.splits option.splits)

diff --git a/proof/invariant-abstract/X64/ArchCSpaceInvPre_AI.thy b/proof/invariant-abstract/X64/ArchCSpaceInvPre_AI.thy
@@ -320,7 +320,7 @@ lemma cap_master_arch_cap_rights [simp]:
   by (simp add: cap_master_arch_cap_def acap_rights_update_def
            split: arch_cap.splits)
 
-lemma acap_rights_update_id [intro!, simp]:
+lemma valid_acap_rights_update_id [intro!, simp]:
   "valid_arch_cap ac s \<Longrightarrow> acap_rights_update (acap_rights ac) ac = ac"
   unfolding acap_rights_update_def acap_rights_def valid_arch_cap_def
   by (cases ac; simp)

diff --git a/proof/invariant-abstract/X64/ArchInvariants_AI.thy b/proof/invariant-abstract/X64/ArchInvariants_AI.thy
@@ -3030,7 +3030,7 @@ lemma vs_cap_ref_eq_imp_table_cap_ref_eq:
                   arch_cap_fun_lift_def
           split: cap.splits arch_cap.splits vmpage_size.splits option.splits)
 
-lemma acap_rights_update_id [intro!, simp]:
+lemma wf_acap_rights_update_id [intro!, simp]:
   "\<lbrakk>wellformed_acap cap\<rbrakk> \<Longrightarrow> acap_rights_update (acap_rights cap) cap = cap"
   unfolding wellformed_acap_def acap_rights_update_def
   by (auto split: arch_cap.splits)