From d5e6166383cd242ad452a0d76261c8f7cbf663ff Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Tue, 23 Jul 2024 11:33:44 +1000 Subject: [PATCH] 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 --- .../invariant-abstract/AARCH64/ArchCSpaceInvPre_AI.thy | 2 +- proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchCSpaceInvPre_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchInvariants_AI.thy | 2 +- .../invariant-abstract/ARM_HYP/ArchCSpaceInvPre_AI.thy | 2 +- proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy | 2 +- proof/invariant-abstract/CSpaceInv_AI.thy | 10 +++------- proof/invariant-abstract/Invariants_AI.thy | 6 +++--- .../invariant-abstract/RISCV64/ArchCSpaceInvPre_AI.thy | 2 +- proof/invariant-abstract/RISCV64/ArchInvariants_AI.thy | 2 +- proof/invariant-abstract/X64/ArchCSpaceInvPre_AI.thy | 2 +- proof/invariant-abstract/X64/ArchInvariants_AI.thy | 2 +- 12 files changed, 16 insertions(+), 20 deletions(-) diff --git a/proof/invariant-abstract/AARCH64/ArchCSpaceInvPre_AI.thy b/proof/invariant-abstract/AARCH64/ArchCSpaceInvPre_AI.thy index 9be7754f33..44df5b80cd 100644 --- 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 \ 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 index 75d8ba5d37..ee66eb7045 100644 --- 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 \ 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 index a5a4220129..d298ea7f7a 100644 --- 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 \ 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 index d3efceb2c4..c30b47f8d9 100644 --- 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]: "\wellformed_acap cap\ \ 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 index 16024bb9e6..c694bb7881 100644 --- 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 \ 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 index c8b7c5586a..4f23c783f9 100644 --- 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]: "\wellformed_acap cap\ \ 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 index a7145640a6..9d86e52b46 100644 --- 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 index 845908d66b..005db58cf7 100644 --- 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 index 26c89dc4e8..26355d6fb4 100644 --- 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 \ 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 index 44ef380453..b2132a49b9 100644 --- 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 \ 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 index 1f6b81000c..7f7cbfb122 100644 --- 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 \ 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 index 884b521be6..228740a7cf 100644 --- 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]: "\wellformed_acap cap\ \ acap_rights_update (acap_rights cap) cap = cap" unfolding wellformed_acap_def acap_rights_update_def by (auto split: arch_cap.splits)