From 6c2ae29853a0af4a81a7b10663239e844781ff11 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 27 Oct 2023 09:27:31 +1100 Subject: [PATCH 1/2] lib: produce _def and _val thms in value_type Produce a _def theorem for the value type that provides direct symbolic access to the right-hand side of the value_type definition. This avoids having to unfold those terms in subsequent proofs. The numeric value as as term is still available as _val. This restricts value_type to nat/int inputs, i.e. word is no longer accepted on the rhs (so far unused). A manual cast to nat on the rhs will still work. Signed-off-by: Gerwin Klein --- lib/Value_Type.thy | 55 +++++++++++++++++++++++++----------- lib/test/Value_Type_Test.thy | 38 +++++++++++++++++++------ 2 files changed, 69 insertions(+), 24 deletions(-) diff --git a/lib/Value_Type.thy b/lib/Value_Type.thy index e01ec193ff..2c1c4a6a52 100644 --- a/lib/Value_Type.thy +++ b/lib/Value_Type.thy @@ -10,7 +10,7 @@ keywords "value_type" :: thy_decl begin (* - Define a type synonym from a term that evaluates to a numeral. + Define a type synonym from a term of type nat or int that evaluates to a (positive) numeral. Examples: @@ -41,6 +41,8 @@ fun force_nat_numeral (Const (@{const_name numeral}, Type ("fun", [num, _])) $ n | force_nat_numeral (Const (@{const_name "Groups.zero"}, _)) = @{term "0::nat"} | force_nat_numeral t = raise TERM ("force_nat_numeral: number expected", [t]) +fun cast_to_nat t = if type_of t = @{typ int} then @{term nat} $ t else t + fun make_type binding v lthy = let val n = case get_term_numeral v of @@ -51,12 +53,31 @@ fun make_type binding v lthy = lthy |> Typedecl.abbrev (binding, [], Mixfix.NoSyn) typ |> #2 end -fun make_def binding v lthy = +(* Copied from method eval in HOL.thy: *) +fun eval_tac ctxt = + let val conv = Code_Runtime.dynamic_holds_conv + in + CONVERSION (Conv.params_conv ~1 (Conv.concl_conv ~1 o conv) ctxt) THEN' + resolve_tac ctxt [TrueI] + end + +(* This produces two theorems: one symbolic _def theorem and one numeric _val theorem. + The _def theorem is a definition, via Specification.definition. + The _val theorem is proved from that definition using "eval_tac" via the code generator. *) +fun make_defs binding t v lthy = let + val t = cast_to_nat t val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq - val def_t = mk_eq (Free (Binding.name_of binding, @{typ nat}), force_nat_numeral v) + val def_t = mk_eq (Free (Binding.name_of binding, @{typ nat}), t) + val ((_, (_, def_thm)), lthy') = + lthy |> Specification.definition NONE [] [] (Binding.empty_atts, def_t) + val eq_t = mk_eq (t, force_nat_numeral v) + val eq_thm = + Goal.prove lthy' [] [] eq_t (fn {context = ctxt, prems = _} => eval_tac ctxt 1) + val thm = @{thm trans} OF [def_thm, eq_thm] + val val_binding = Binding.map_name (fn n => n ^ "_val") binding |> Binding.reset_pos in - lthy |> Specification.definition NONE [] [] (Binding.empty_atts, def_t) |> #2 + Local_Theory.note ((val_binding, []), [thm]) lthy' |> #2 end in @@ -68,7 +89,7 @@ fun value_type_cmd no_def binding t lthy = in lthy |> make_type binding v - |> (if no_def then I else make_def binding v) + |> (if no_def then I else make_defs binding t' v) end val no_def_option = @@ -86,20 +107,22 @@ end \ (* -Potential extension idea for the future: +Potential extension ideas for the future: -It may be possible to generalise this command to non-numeral types -- as long as the RHS can -be interpreted as some nat n, we can in theory always define a type with n elements, and instantiate -that type into class finite. Might have to present a goal to the user that RHS evaluates > 0 in nat. +* It may be possible to generalise this command to non-numeral types -- as long as the RHS can + be interpreted as some nat n, we can in theory always define a type with n elements, and + instantiate that type into class finite. Might have to present a goal to the user that RHS + evaluates > 0 in nat. -There are a few wrinkles with that, because currently you can use any type on the RHS without -complications. Requiring nat for the RHS term would not be great, because we often have word there. -We could add coercion to nat for word and int, though, that would cover all current use cases. + The benefit of defining a new type instead of a type synonym for a numeral type is that type + checking is now more meaningful and we do get some abstraction over the actual value, which would + help make proofs more generic. -The benefit of defining a new type instead of a type synonym for a numeral type is that type -checking is now more meaningful and we do get some abstraction over the actual value, which would -help make proofs more generic. -*) + The disadvantage of a non-numeral type is that it is not equal to the types that come out of the + C parser. +* We could add more automatic casts from known types to nat (e.g. from word). But it's relatively + low overhead to provide the cast as a user. +*) end diff --git a/lib/test/Value_Type_Test.thy b/lib/test/Value_Type_Test.thy index 36636c97d6..d008226dd7 100644 --- a/lib/test/Value_Type_Test.thy +++ b/lib/test/Value_Type_Test.thy @@ -5,11 +5,13 @@ *) theory Value_Type_Test -imports Lib.Value_Type + imports + Lib.Value_Type + "Word_Lib.WordSetup" begin (* - Define a type synonym from a term that evaluates to a numeral. + Define a type synonym from a term of type nat or int that evaluates to a positive numeral. *) definition num_domains :: int where @@ -18,31 +20,51 @@ definition num_domains :: int where definition num_prio :: int where "num_prio = 256" -text \The RHS does not have to be of type nat, it just has to evaluate to any numeral:\ +text \ + The RHS has to be of type @{typ nat} or @{typ int}. @{typ int} will be automatically cast to + @{term nat}:\ value_type num_queues = "num_prio * num_domains" text \This produces a type of the specified size and a constant of type nat:\ typ num_queues term num_queues -thm num_queues_def -text \You can leave out the constant definition, and just define the type:\ +text \You get a symbolic definition theorem:\ +lemma "num_queues = nat (num_prio * num_domains)" + by (rule num_queues_def) + +text \And a numeric value theorem:\ +lemma "num_queues = 4096" + by (rule num_queues_val) + + +text \You can leave out the constant definitions, and just define the type:\ value_type (no_def) num_something = "10 * num_domains" typ num_something +text \ + If the value on the rhs is not of type @{typ nat}, it can still be cast to @{typ nat} manually:\ +definition some_word :: "8 word" where + "some_word \ 0xFF" + +value_type word_val = "unat (some_word && 0xF0)" + +lemma "word_val = (0xF0::nat)" + by (rule word_val_val) + + text \ @{command value_type} uses @{command value} in the background, so all of this also works in anonymous local contexts, provided they don't have assumptions (so that @{command value} can produce code) - Example: -\ + Example:\ context begin -definition X::int where "X = 10" +definition X::nat where "X = 10" value_type x_t = X From 7a5f2ff62c43d4be2bd2f1b90a10af8c0c309399 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 27 Oct 2023 09:47:57 +1100 Subject: [PATCH 2/2] 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 | 18 +++++++++--------- 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 | 18 +++++++++--------- 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 ++-- spec/abstract/AARCH64/Arch_Structs_A.thy | 2 +- spec/cspec/AARCH64/Kernel_C.thy | 4 ++-- 18 files changed, 63 insertions(+), 63 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..a6d00f17ff 100644 --- a/proof/crefine/AARCH64/Wellformed_C.thy +++ b/proof/crefine/AARCH64/Wellformed_C.thy @@ -94,7 +94,7 @@ abbreviation vcpu_vppi_masked_C_Ptr :: "addr \ (machine_word[1]) ptr" where "vcpu_vppi_masked_C_Ptr \ Ptr" declare seL4_VCPUReg_Num_def[code] -value_type num_vcpu_regs = seL4_VCPUReg_Num +value_type num_vcpu_regs = "unat seL4_VCPUReg_Num" abbreviation vcpuregs_C_Ptr :: "addr \ (machine_word[num_vcpu_regs]) ptr" where "vcpuregs_C_Ptr \ Ptr" @@ -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..d42a1b71e0 100644 --- a/proof/crefine/ARM_HYP/Wellformed_C.thy +++ b/proof/crefine/ARM_HYP/Wellformed_C.thy @@ -44,7 +44,7 @@ abbreviation pd_Ptr :: "32 word \ (pde_C[2048]) ptr" where "pd_Ptr == Ptr" declare seL4_VCPUReg_Num_def[code] -value_type num_vcpu_regs = seL4_VCPUReg_Num +value_type num_vcpu_regs = "unat seL4_VCPUReg_Num" abbreviation regs_C_Ptr :: "addr \ (machine_word[num_vcpu_regs]) ptr" where"regs_C_Ptr \ Ptr" @@ -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/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\