From 05fabf2a48988a3a2f560eca830e6f82862a084a Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 27 Oct 2023 09:47:57 +1100 Subject: [PATCH] proof: updates for value_type _def -> _val Rename occurrences of _def to _val for value_type-generated names. Does not make full use of value_type _def theorems yet. Signed-off-by: Gerwin Klein --- proof/crefine/AARCH64/ADT_C.thy | 2 +- proof/crefine/AARCH64/ArchMove_C.thy | 2 +- proof/crefine/AARCH64/IpcCancel_C.thy | 2 +- proof/crefine/AARCH64/Retype_C.thy | 4 ++-- proof/crefine/AARCH64/VSpace_C.thy | 10 +++++----- proof/crefine/AARCH64/Wellformed_C.thy | 16 ++++++++-------- proof/crefine/ARM/IpcCancel_C.thy | 2 +- proof/crefine/ARM/Wellformed_C.thy | 16 ++++++++-------- proof/crefine/ARM_HYP/IpcCancel_C.thy | 2 +- proof/crefine/ARM_HYP/Wellformed_C.thy | 16 ++++++++-------- proof/crefine/RISCV64/IpcCancel_C.thy | 2 +- proof/crefine/RISCV64/Wellformed_C.thy | 16 ++++++++-------- proof/crefine/X64/IpcCancel_C.thy | 2 +- proof/crefine/X64/Wellformed_C.thy | 16 ++++++++-------- .../AARCH64/ArchInvariants_AI.thy | 4 ++-- proof/refine/AARCH64/ADT_H.thy | 4 ++-- proof/refine/RISCV64/ADT_H.thy | 2 +- spec/abstract/AARCH64/Arch_Structs_A.thy | 2 +- spec/cspec/AARCH64/Kernel_C.thy | 4 ++-- 19 files changed, 62 insertions(+), 62 deletions(-) diff --git a/proof/crefine/AARCH64/ADT_C.thy b/proof/crefine/AARCH64/ADT_C.thy index 289b4c474a..11928fde85 100644 --- a/proof/crefine/AARCH64/ADT_C.thy +++ b/proof/crefine/AARCH64/ADT_C.thy @@ -613,7 +613,7 @@ lemma carch_state_to_H_correct: using valid apply (simp add: valid_arch_state'_def) apply fastforce - apply (clarsimp simp: mask_def vmid_bits_def) + apply (clarsimp simp: mask_def vmid_bits_val) apply (rule conjI) using valid rel apply (simp add: ccur_vcpu_to_H_correct) diff --git a/proof/crefine/AARCH64/ArchMove_C.thy b/proof/crefine/AARCH64/ArchMove_C.thy index 5cb7d5ca0e..805de5eb17 100644 --- a/proof/crefine/AARCH64/ArchMove_C.thy +++ b/proof/crefine/AARCH64/ArchMove_C.thy @@ -715,7 +715,7 @@ lemma asid_pool_at_ko': apply (case_tac asidpool, auto)[1] done -(* FIXME AARCH64: move; also add vmid_bits_def to relevant bit defs *) +(* FIXME AARCH64: move; also add vmid_bits_val to relevant bit defs *) value_type vmid_bits = "size (0::vmid)" (* end of move to Refine/AInvs *) diff --git a/proof/crefine/AARCH64/IpcCancel_C.thy b/proof/crefine/AARCH64/IpcCancel_C.thy index 4513f68ca0..776b195c9c 100644 --- a/proof/crefine/AARCH64/IpcCancel_C.thy +++ b/proof/crefine/AARCH64/IpcCancel_C.thy @@ -29,7 +29,7 @@ proof - qed lemmas cready_queues_index_to_C_in_range = - cready_queues_index_to_C_in_range'[simplified num_tcb_queues_def] + cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val] lemma cready_queues_index_to_C_inj: "\ cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio'; diff --git a/proof/crefine/AARCH64/Retype_C.thy b/proof/crefine/AARCH64/Retype_C.thy index b3935e6c9b..3517b0d809 100644 --- a/proof/crefine/AARCH64/Retype_C.thy +++ b/proof/crefine/AARCH64/Retype_C.thy @@ -1961,7 +1961,7 @@ lemma createObjects_ccorres_pte_pt: (\\ksPSpace := ?ks \\, x\globals := globals x\t_hrs_' := ?ks' x\\) \ rf_sr") proof (intro impI allI) define array_len where "array_len \ pt_array_len" - note array_len_def = pt_array_len_def array_len_def + note array_len_def = pt_array_len_val array_len_def fix \ x let ?thesis = "(\\ksPSpace := ?ks \\, x\globals := globals x\t_hrs_' := ?ks' x\\) \ rf_sr" @@ -2130,7 +2130,7 @@ lemma createObjects_ccorres_pte_vs: (\\ksPSpace := ?ks \\, x\globals := globals x\t_hrs_' := ?ks' x\\) \ rf_sr") proof (intro impI allI) define array_len where "array_len \ vs_array_len" - note array_len_def = vs_array_len_def array_len_def + note array_len_def = vs_array_len_val array_len_def fix \ x let ?thesis = "(\\ksPSpace := ?ks \\, x\globals := globals x\t_hrs_' := ?ks' x\\) \ rf_sr" diff --git a/proof/crefine/AARCH64/VSpace_C.thy b/proof/crefine/AARCH64/VSpace_C.thy index 745f91e322..f92f95ba21 100644 --- a/proof/crefine/AARCH64/VSpace_C.thy +++ b/proof/crefine/AARCH64/VSpace_C.thy @@ -1155,7 +1155,7 @@ lemma invalidateASIDEntry_ccorres: apply (erule array_relation_update) apply word_eqI_solve apply (clarsimp simp: asidInvalid_def) - apply (simp add: mask_def vmid_bits_def unat_max_word) + apply (simp add: mask_def vmid_bits_val unat_max_word) apply (rule ccorres_return_Skip) apply ceqv apply (ctac add: invalidateASID_ccorres) @@ -1185,7 +1185,7 @@ lemma invalidateVMIDEntry_ccorres: apply (simp flip: fun_upd_apply) apply (erule array_relation_update, rule refl) apply (simp (no_asm) add: asidInvalid_def) - apply (simp (no_asm) add: mask_def vmid_bits_def unat_max_word) + apply (simp (no_asm) add: mask_def vmid_bits_val unat_max_word) done crunches invalidateVMIDEntry, invalidateASID @@ -1233,7 +1233,7 @@ lemma findFreeHWASID_ccorres: apply (simp add: throwError_def return_def split: if_split) apply (clarsimp simp: returnOk_def return_def inr_rrel_def rf_sr_armKSNextVMID) apply (drule rf_sr_armKSVMIDTable_rel') - apply (clarsimp simp: array_relation_def vmid_bits_def mask_def) + apply (clarsimp simp: array_relation_def vmid_bits_val mask_def) apply (erule_tac x="armKSNextASID_' (globals s) + word_of_nat (length ys)" in allE) apply (clarsimp simp: valid_arch_state'_def ran_def) apply ((rule conjI, uint_arith, simp add: take_bit_nat_def unsigned_of_nat, clarsimp)+)[1] @@ -1316,7 +1316,7 @@ lemma findFreeHWASID_ccorres: apply (drule rf_sr_armKSVMIDTable_rel') apply (clarsimp simp: array_relation_def) apply (erule_tac x="armKSNextASID_' (globals s')" in allE, erule impE) - apply (simp add: vmid_bits_def mask_def) + apply (simp add: vmid_bits_val mask_def) apply simp apply (fold mapME_def) apply (wp mapME_wp') @@ -1357,7 +1357,7 @@ lemma storeHWASID_ccorres: cmachine_state_relation_def carch_state_relation_def carch_globals_def simp del: fun_upd_apply) apply (erule array_relation_update, rule refl, simp) - apply (simp add: mask_def vmid_bits_def unat_max_word) + apply (simp add: mask_def vmid_bits_val unat_max_word) apply wp apply (clarsimp simp: guard_is_UNIV_def split: if_splits) apply (clarsimp simp: zero_sle_ucast_up is_down word_sless_alt sint_ucast_eq_uint) diff --git a/proof/crefine/AARCH64/Wellformed_C.thy b/proof/crefine/AARCH64/Wellformed_C.thy index 8847b542c0..7543567f6a 100644 --- a/proof/crefine/AARCH64/Wellformed_C.thy +++ b/proof/crefine/AARCH64/Wellformed_C.thy @@ -497,31 +497,31 @@ lemma maxDom_sgt_0_maxDomain: lemma num_domains_calculation: "num_domains = numDomains" - unfolding num_domains_def by eval + unfolding num_domains_val by eval private lemma num_domains_card_explicit: "num_domains = CARD(num_domains)" - by (simp add: num_domains_def) + by (simp add: num_domains_val) lemmas num_domains_index_updates = - index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] - index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] (* C ArrayGuards will throw these at us and there is no way to avoid a proof of being less than a specific number expressed as a word, so we must introduce these. However, being explicit means lack of discipline can lead to a violation. *) -lemma numDomains_less_numeric_explicit[simplified num_domains_def One_nat_def]: +lemma numDomains_less_numeric_explicit[simplified num_domains_val One_nat_def]: "x < Kernel_Config.numDomains \ x < num_domains" by (simp add: num_domains_calculation) -lemma numDomains_less_unat_ucast_explicit[simplified num_domains_def]: +lemma numDomains_less_unat_ucast_explicit[simplified num_domains_val]: "unat x < Kernel_Config.numDomains \ (ucast (x::domain) :: machine_word) < of_nat num_domains" apply (rule word_less_nat_alt[THEN iffD2]) apply transfer apply simp - apply (drule numDomains_less_numeric_explicit, simp add: num_domains_def) + apply (drule numDomains_less_numeric_explicit, simp add: num_domains_val) done lemmas maxDomain_le_unat_ucast_explicit = @@ -546,7 +546,7 @@ value_type num_tcb_queues = "numDomains * numPriorities" lemma num_tcb_queues_calculation: "num_tcb_queues = numDomains * numPriorities" - unfolding num_tcb_queues_def by eval + unfolding num_tcb_queues_val by eval (* Input abbreviations for API object types *) diff --git a/proof/crefine/ARM/IpcCancel_C.thy b/proof/crefine/ARM/IpcCancel_C.thy index 5a7a7e1216..0f79e156a5 100644 --- a/proof/crefine/ARM/IpcCancel_C.thy +++ b/proof/crefine/ARM/IpcCancel_C.thy @@ -30,7 +30,7 @@ proof - qed lemmas cready_queues_index_to_C_in_range = - cready_queues_index_to_C_in_range'[simplified num_tcb_queues_def] + cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val] lemma cready_queues_index_to_C_inj: "\ cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio'; diff --git a/proof/crefine/ARM/Wellformed_C.thy b/proof/crefine/ARM/Wellformed_C.thy index 938283c309..4e964d3559 100644 --- a/proof/crefine/ARM/Wellformed_C.thy +++ b/proof/crefine/ARM/Wellformed_C.thy @@ -426,31 +426,31 @@ lemma maxDom_sgt_0_maxDomain: lemma num_domains_calculation: "num_domains = numDomains" - unfolding num_domains_def by eval + unfolding num_domains_val by eval private lemma num_domains_card_explicit: "num_domains = CARD(num_domains)" - by (simp add: num_domains_def) + by (simp add: num_domains_val) lemmas num_domains_index_updates = - index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] - index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] (* C ArrayGuards will throw these at us and there is no way to avoid a proof of being less than a specific number expressed as a word, so we must introduce these. However, being explicit means lack of discipline can lead to a violation. *) -lemma numDomains_less_numeric_explicit[simplified num_domains_def One_nat_def]: +lemma numDomains_less_numeric_explicit[simplified num_domains_val One_nat_def]: "x < Kernel_Config.numDomains \ x < num_domains" by (simp add: num_domains_calculation) -lemma numDomains_less_unat_ucast_explicit[simplified num_domains_def]: +lemma numDomains_less_unat_ucast_explicit[simplified num_domains_val]: "unat x < Kernel_Config.numDomains \ (ucast (x::domain) :: machine_word) < of_nat num_domains" apply (rule word_less_nat_alt[THEN iffD2]) apply transfer apply simp - apply (drule numDomains_less_numeric_explicit, simp add: num_domains_def) + apply (drule numDomains_less_numeric_explicit, simp add: num_domains_val) done lemmas maxDomain_le_unat_ucast_explicit = @@ -475,7 +475,7 @@ value_type num_tcb_queues = "numDomains * numPriorities" lemma num_tcb_queues_calculation: "num_tcb_queues = numDomains * numPriorities" - unfolding num_tcb_queues_def by eval + unfolding num_tcb_queues_val by eval abbreviation(input) diff --git a/proof/crefine/ARM_HYP/IpcCancel_C.thy b/proof/crefine/ARM_HYP/IpcCancel_C.thy index ba7082881e..b307286b81 100644 --- a/proof/crefine/ARM_HYP/IpcCancel_C.thy +++ b/proof/crefine/ARM_HYP/IpcCancel_C.thy @@ -30,7 +30,7 @@ proof - qed lemmas cready_queues_index_to_C_in_range = - cready_queues_index_to_C_in_range'[simplified num_tcb_queues_def] + cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val] lemma cready_queues_index_to_C_inj: "\ cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio'; diff --git a/proof/crefine/ARM_HYP/Wellformed_C.thy b/proof/crefine/ARM_HYP/Wellformed_C.thy index a09d0de707..de88d5844b 100644 --- a/proof/crefine/ARM_HYP/Wellformed_C.thy +++ b/proof/crefine/ARM_HYP/Wellformed_C.thy @@ -461,31 +461,31 @@ lemma maxDom_sgt_0_maxDomain: lemma num_domains_calculation: "num_domains = numDomains" - unfolding num_domains_def by eval + unfolding num_domains_val by eval private lemma num_domains_card_explicit: "num_domains = CARD(num_domains)" - by (simp add: num_domains_def) + by (simp add: num_domains_val) lemmas num_domains_index_updates = - index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] - index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] (* C ArrayGuards will throw these at us and there is no way to avoid a proof of being less than a specific number expressed as a word, so we must introduce these. However, being explicit means lack of discipline can lead to a violation. *) -lemma numDomains_less_numeric_explicit[simplified num_domains_def One_nat_def]: +lemma numDomains_less_numeric_explicit[simplified num_domains_val One_nat_def]: "x < Kernel_Config.numDomains \ x < num_domains" by (simp add: num_domains_calculation) -lemma numDomains_less_unat_ucast_explicit[simplified num_domains_def]: +lemma numDomains_less_unat_ucast_explicit[simplified num_domains_val]: "unat x < Kernel_Config.numDomains \ (ucast (x::domain) :: machine_word) < of_nat num_domains" apply (rule word_less_nat_alt[THEN iffD2]) apply transfer apply simp - apply (drule numDomains_less_numeric_explicit, simp add: num_domains_def) + apply (drule numDomains_less_numeric_explicit, simp add: num_domains_val) done lemmas maxDomain_le_unat_ucast_explicit = @@ -510,7 +510,7 @@ value_type num_tcb_queues = "numDomains * numPriorities" lemma num_tcb_queues_calculation: "num_tcb_queues = numDomains * numPriorities" - unfolding num_tcb_queues_def by eval + unfolding num_tcb_queues_val by eval (* Input abbreviations for API object types *) diff --git a/proof/crefine/RISCV64/IpcCancel_C.thy b/proof/crefine/RISCV64/IpcCancel_C.thy index f06b9d102c..fc510629a6 100644 --- a/proof/crefine/RISCV64/IpcCancel_C.thy +++ b/proof/crefine/RISCV64/IpcCancel_C.thy @@ -29,7 +29,7 @@ proof - qed lemmas cready_queues_index_to_C_in_range = - cready_queues_index_to_C_in_range'[simplified num_tcb_queues_def] + cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val] lemma cready_queues_index_to_C_inj: "\ cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio'; diff --git a/proof/crefine/RISCV64/Wellformed_C.thy b/proof/crefine/RISCV64/Wellformed_C.thy index f3c815622b..f28a56f303 100644 --- a/proof/crefine/RISCV64/Wellformed_C.thy +++ b/proof/crefine/RISCV64/Wellformed_C.thy @@ -429,31 +429,31 @@ lemma maxDom_sgt_0_maxDomain: lemma num_domains_calculation: "num_domains = numDomains" - unfolding num_domains_def by eval + unfolding num_domains_val by eval private lemma num_domains_card_explicit: "num_domains = CARD(num_domains)" - by (simp add: num_domains_def) + by (simp add: num_domains_val) lemmas num_domains_index_updates = - index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] - index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] (* C ArrayGuards will throw these at us and there is no way to avoid a proof of being less than a specific number expressed as a word, so we must introduce these. However, being explicit means lack of discipline can lead to a violation. *) -lemma numDomains_less_numeric_explicit[simplified num_domains_def One_nat_def]: +lemma numDomains_less_numeric_explicit[simplified num_domains_val One_nat_def]: "x < Kernel_Config.numDomains \ x < num_domains" by (simp add: num_domains_calculation) -lemma numDomains_less_unat_ucast_explicit[simplified num_domains_def]: +lemma numDomains_less_unat_ucast_explicit[simplified num_domains_val]: "unat x < Kernel_Config.numDomains \ (ucast (x::domain) :: machine_word) < of_nat num_domains" apply (rule word_less_nat_alt[THEN iffD2]) apply transfer apply simp - apply (drule numDomains_less_numeric_explicit, simp add: num_domains_def) + apply (drule numDomains_less_numeric_explicit, simp add: num_domains_val) done lemmas maxDomain_le_unat_ucast_explicit = @@ -478,7 +478,7 @@ value_type num_tcb_queues = "numDomains * numPriorities" lemma num_tcb_queues_calculation: "num_tcb_queues = numDomains * numPriorities" - unfolding num_tcb_queues_def by eval + unfolding num_tcb_queues_val by eval (* Input abbreviations for API object types *) diff --git a/proof/crefine/X64/IpcCancel_C.thy b/proof/crefine/X64/IpcCancel_C.thy index cca60bcadd..b8a475cf6d 100644 --- a/proof/crefine/X64/IpcCancel_C.thy +++ b/proof/crefine/X64/IpcCancel_C.thy @@ -28,7 +28,7 @@ proof - qed lemmas cready_queues_index_to_C_in_range = - cready_queues_index_to_C_in_range'[simplified num_tcb_queues_def] + cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val] lemma cready_queues_index_to_C_inj: "\ cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio'; diff --git a/proof/crefine/X64/Wellformed_C.thy b/proof/crefine/X64/Wellformed_C.thy index f3b4521ceb..ed017823e2 100644 --- a/proof/crefine/X64/Wellformed_C.thy +++ b/proof/crefine/X64/Wellformed_C.thy @@ -472,31 +472,31 @@ lemma maxDom_sgt_0_maxDomain: lemma num_domains_calculation: "num_domains = numDomains" - unfolding num_domains_def by eval + unfolding num_domains_val by eval private lemma num_domains_card_explicit: "num_domains = CARD(num_domains)" - by (simp add: num_domains_def) + by (simp add: num_domains_val) lemmas num_domains_index_updates = - index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] - index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] (* C ArrayGuards will throw these at us and there is no way to avoid a proof of being less than a specific number expressed as a word, so we must introduce these. However, being explicit means lack of discipline can lead to a violation. *) -lemma numDomains_less_numeric_explicit[simplified num_domains_def One_nat_def]: +lemma numDomains_less_numeric_explicit[simplified num_domains_val One_nat_def]: "x < Kernel_Config.numDomains \ x < num_domains" by (simp add: num_domains_calculation) -lemma numDomains_less_unat_ucast_explicit[simplified num_domains_def]: +lemma numDomains_less_unat_ucast_explicit[simplified num_domains_val]: "unat x < Kernel_Config.numDomains \ (ucast (x::domain) :: machine_word) < of_nat num_domains" apply (rule word_less_nat_alt[THEN iffD2]) apply transfer apply simp - apply (drule numDomains_less_numeric_explicit, simp add: num_domains_def) + apply (drule numDomains_less_numeric_explicit, simp add: num_domains_val) done lemmas maxDomain_le_unat_ucast_explicit = @@ -521,7 +521,7 @@ value_type num_tcb_queues = "numDomains * numPriorities" lemma num_tcb_queues_calculation: "num_tcb_queues = numDomains * numPriorities" - unfolding num_tcb_queues_def by eval + unfolding num_tcb_queues_val by eval (* Input abbreviations for API object types *) diff --git a/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy b/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy index 9180267283..e42dd1b32e 100644 --- a/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy @@ -2403,7 +2403,7 @@ lemma pptrTop_ucast_ppn: ucast (ucast (p >> pageBits)::ppn) = p >> pageBits" apply (drule below_pptrTop_ipa_size) apply word_eqI - using ppn_len_def'[unfolded ppn_len_def] + using ppn_len_def'[unfolded ppn_len_val] by (fastforce dest: bit_imp_le_length) lemma kernel_window_range_addrFromPPtr: @@ -2470,7 +2470,7 @@ lemma pt_slot_offset_pt_range: lemma ucast_ucast_ppn: "ucast (ucast ptr::ppn) = ptr && mask ppn_len" for ptr::obj_ref - by (simp add: ucast_ucast_mask ppn_len_def) + by (simp add: ucast_ucast_mask ppn_len_val) lemma pte_base_addr_PageTablePTE[simp]: "pte_base_addr (PageTablePTE ppn) = paddr_from_ppn ppn" diff --git a/proof/refine/AARCH64/ADT_H.thy b/proof/refine/AARCH64/ADT_H.thy index 4f93f4044c..d509b4b577 100644 --- a/proof/refine/AARCH64/ADT_H.thy +++ b/proof/refine/AARCH64/ADT_H.thy @@ -745,7 +745,7 @@ proof - apply (rule ucast_leq_mask) apply (clarsimp simp: bit_simps) apply (clarsimp simp: pte_relation_def ucast_ucast_mask ge_mask_eq vs_index_bits_def) - apply (case_tac "vs off"; simp add: ucast_leq_mask ppn_len_def) + apply (case_tac "vs off"; simp add: ucast_leq_mask ppn_len_val) (* NormalPT_T is an exact duplicate of the VSRootPT_T case, but I don't see any good way to factor out the commonality *) @@ -815,7 +815,7 @@ proof - apply (rule ucast_leq_mask) apply (clarsimp simp: bit_simps) apply (clarsimp simp: pte_relation_def ucast_ucast_mask ge_mask_eq vs_index_bits_def) - apply (case_tac "vs off"; simp add: ucast_leq_mask ppn_len_def) + apply (case_tac "vs off"; simp add: ucast_leq_mask ppn_len_val) apply (in_case "DataPage ?p ?sz") apply (clarsimp split: if_splits) diff --git a/proof/refine/RISCV64/ADT_H.thy b/proof/refine/RISCV64/ADT_H.thy index 12353508da..57a27bca6b 100644 --- a/proof/refine/RISCV64/ADT_H.thy +++ b/proof/refine/RISCV64/ADT_H.thy @@ -671,7 +671,7 @@ proof - apply (drule (2) distinct_word_add_inj_ptes[unfolded bit_simps]) apply clarsimp apply (rename_tac pt) - apply (case_tac "pt off"; simp add: ppn_len_def ucast_leq_mask) + apply (case_tac "pt off"; simp add: ppn_len_val ucast_leq_mask) using pspace_aligned[simplified pspace_aligned_def Ball_def dom_def] apply (erule_tac x=y in allE) apply clarsimp diff --git a/spec/abstract/AARCH64/Arch_Structs_A.thy b/spec/abstract/AARCH64/Arch_Structs_A.thy index 32aaf0bb6e..23df8699bb 100644 --- a/spec/abstract/AARCH64/Arch_Structs_A.thy +++ b/spec/abstract/AARCH64/Arch_Structs_A.thy @@ -91,7 +91,7 @@ type_synonym ppn = "ppn_len word" text \This lemma encodes @{typ ppn_len} value above as a term, so we can use it generically:\ lemma ppn_len_def': "ppn_len = ipa_size - pageBits" - by (simp add: ppn_len_def pageBits_def ipa_size_def Kernel_Config.config_ARM_PA_SIZE_BITS_40_def) + by (simp add: ppn_len_val pageBits_def ipa_size_def Kernel_Config.config_ARM_PA_SIZE_BITS_40_def) datatype pte = InvalidPTE diff --git a/spec/cspec/AARCH64/Kernel_C.thy b/spec/cspec/AARCH64/Kernel_C.thy index 254e030c7f..d5ef766e74 100644 --- a/spec/cspec/AARCH64/Kernel_C.thy +++ b/spec/cspec/AARCH64/Kernel_C.thy @@ -36,10 +36,10 @@ lemma ptTranslationBits_vs_index_bits: is unfolded. It'd be nicer if we could also get something symbolic out of value_type, though *) lemma ptTranslationBits_vs_array_len': "2 ^ ptTranslationBits VSRootPT_T = vs_array_len" - by (simp add: vs_array_len_def ptTranslationBits_vs_index_bits vs_index_bits_def + by (simp add: vs_array_len_val ptTranslationBits_vs_index_bits vs_index_bits_def Kernel_Config.config_ARM_PA_SIZE_BITS_40_def) -lemmas ptTranslationBits_vs_array_len = ptTranslationBits_vs_array_len'[unfolded vs_array_len_def] +lemmas ptTranslationBits_vs_array_len = ptTranslationBits_vs_array_len'[unfolded vs_array_len_val] type_synonym cghost_state = "(machine_word \ vmpage_size) \ \ \Frame sizes\