diff --git a/proof/crefine/AARCH64/CSpace_C.thy b/proof/crefine/AARCH64/CSpace_C.thy index 71c3aa0608..f3cc296f8e 100644 --- a/proof/crefine/AARCH64/CSpace_C.thy +++ b/proof/crefine/AARCH64/CSpace_C.thy @@ -2533,7 +2533,7 @@ lemma cap_get_capSizeBits_spec: cap_lift_domain_cap cap_get_tag_scast objBits_defs wordRadix_def c_valid_cap_def cl_valid_cap_def pageBits_def asidPoolBits_def - Kernel_Config.config_ARM_PA_SIZE_BITS_40_def (* FIXME AARCH64: #define in C, so no other option for now *) + Kernel_Config.config_ARM_PA_SIZE_BITS_40_def (* #define in C, so no other option for now *) cong: option.case_cong dest!: sym [where t = "ucast (cap_get_tag cap)" for cap]) apply (clarsimp split: option.splits cap_CL.splits dest!: cap_lift_Some_CapD) diff --git a/proof/crefine/AARCH64/Finalise_C.thy b/proof/crefine/AARCH64/Finalise_C.thy index 8ce409abb9..d051c64bb2 100644 --- a/proof/crefine/AARCH64/Finalise_C.thy +++ b/proof/crefine/AARCH64/Finalise_C.thy @@ -1570,7 +1570,7 @@ next have level: "level < maxPTLevel" by simp then have [simp]: "word_of_nat maxPTLevel - (1 + of_nat level) < maxPT" (is "?i < maxPT") - by (cases "config_ARM_PA_SIZE_BITS_40"; + by (cases config_ARM_PA_SIZE_BITS_40; simp add: maxPTLevel_def maxPT_def unat_arith_simps unat_of_nat) from level diff --git a/proof/crefine/AARCH64/Invoke_C.thy b/proof/crefine/AARCH64/Invoke_C.thy index 9a70b33346..d9d8932a09 100644 --- a/proof/crefine/AARCH64/Invoke_C.thy +++ b/proof/crefine/AARCH64/Invoke_C.thy @@ -1463,9 +1463,9 @@ lemma getObjectSize_spec: bit_simps objBits_simps' framesize_to_H_def pageBitsForSize_def object_type_to_H_def Kernel_C_defs APIType_capBits_def) apply (simp add:nAPIObjects_def) - (* FIXME AARCH64 abstraction violation, looks to be not true when config_ARM_PA_SIZE_BITS_40 *) - apply (simp add:enum_object_type enum_apiobject_type frameSizeConstants_defs - Kernel_Config.config_ARM_PA_SIZE_BITS_40_def + (* True for both cases of config_ARM_PA_SIZE_BITS_40 with corresponding max vm level change *) + apply (simp add: enum_object_type enum_apiobject_type frameSizeConstants_defs + Kernel_Config.config_ARM_PA_SIZE_BITS_40_def split: if_split) apply unat_arith done diff --git a/proof/crefine/AARCH64/Retype_C.thy b/proof/crefine/AARCH64/Retype_C.thy index c87b58ccef..7e1e692851 100644 --- a/proof/crefine/AARCH64/Retype_C.thy +++ b/proof/crefine/AARCH64/Retype_C.thy @@ -2142,7 +2142,7 @@ proof (intro impI allI) and cover: "range_cover ptr sz (ptBits pt_t) 1" and al: "is_aligned ptr (ptBits pt_t)" and ptr0: "ptr \ 0" - and sz: "(ptBits pt_t) \ sz" + and sz: "ptBits pt_t \ sz" and szb: "sz < word_bits" and pal: "pspace_aligned' \" and pdst: "pspace_distinct' \" @@ -2215,7 +2215,9 @@ proof (intro impI allI) using al[simplified bit_simps] apply - apply (rule is_aligned_c_guard[where n="ptBits pt_t" and m=3]) - apply (simp_all add: align_td_array align_of_def bit_simps ptr0 split: if_split) + apply (simp_all add: align_td_array align_of_def bit_simps ptr0 pt_t_def + Kernel_Config.config_ARM_PA_SIZE_BITS_40_def + split: if_splits) done have guard'[unfolded array_len_def]: "\n < array_len. c_guard (pte_Ptr ptr +\<^sub>p int n)" @@ -2266,7 +2268,7 @@ proof (intro impI allI) pt_bits_def table_size_def power_add pte_bits_def word_size_bits_def hrs_htd_update ht_rl foldr_upd_app_if [folded data_map_insert_def] rl cvariable_array_ptr_retyps[OF szo] - zero_ranges_ptr_retyps[where p="pt_Ptr ptr", simplified szo]) + zero_ranges_ptr_retyps[where p="vs_Ptr ptr", simplified szo]) apply (subst h_t_valid_ptr_retyps_gen_disjoint, assumption) apply (simp add:szo cte_C_size cte_level_bits_def) apply (erule disjoint_subset) @@ -4378,7 +4380,7 @@ lemma getObjectSize_symb: APIType_capBits_def objBits_simps' bit_simps split: if_split) apply unat_arith - (* FIXME AARCH64 abstraction violation *) + (* True in either config with corresponding max vm level change *) apply (simp add: Kernel_Config.config_ARM_PA_SIZE_BITS_40_def) done @@ -5923,7 +5925,7 @@ subgoal apply (rule is_aligned_c_guard[where m=pte_bits], simp, simp) apply (simp add: align_of_array) apply (simp add: align_of_def bit_simps) - apply (simp add: bit_simps split: if_split) + apply (solves \simp add: bit_simps Kernel_Config.config_ARM_PA_SIZE_BITS_40_def split: if_split\) apply (simp add: bit_simps) apply (drule_tac p="vs_Ptr regionBase" and d="hrs_htd (t_hrs_' (globals s'))" and @@ -7162,7 +7164,7 @@ lemma ccorres_typ_region_bytes_dummy: cnodes_retype_have_size_mono[where T=S] tcb_ctes_typ_region_bytes[OF _ _ invs_pspace_aligned'] pte_typ_region_bytes o_def) - (* FIXME AARCH64 abstraction violation, need to know config_ARM_PA_SIZE_BITS_40 is False *) + (* True for either version of config_ARM_PA_SIZE_BITS_40 with corresponding max vm level change *) apply (simp add: cmap_array_typ_region_bytes_triv invs_pspace_aligned' bit_simps objBitsT_simps word_bits_def zero_ranges_are_zero_typ_region_bytes Kernel_Config.config_ARM_PA_SIZE_BITS_40_def @@ -8660,7 +8662,6 @@ shows "ccorres dc xfdc subgoal premises prems using prems by (clarsimp simp: objBits_simps' unat_eq_def word_unat.Rep_inverse' word_less_nat_alt)+ - (* FIXME AARCH64 abstraction violation: for some of these we need to know config_ARM_PA_SIZE_BITS_40_def *) by (clarsimp simp: bit_simps pageBitsForSize_def framesize_to_H_def frameSizeConstants_defs Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)+ diff --git a/proof/crefine/AARCH64/SR_lemmas_C.thy b/proof/crefine/AARCH64/SR_lemmas_C.thy index 6dabdabd1a..b8bb8899fe 100644 --- a/proof/crefine/AARCH64/SR_lemmas_C.thy +++ b/proof/crefine/AARCH64/SR_lemmas_C.thy @@ -2200,7 +2200,7 @@ lemma vspace_at_rf_sr: apply (simp add: align_of_def typ_info_array array_tag_def align_td_array_tag) apply clarsimp apply (drule aligned_intvl_0, simp) - apply (clarsimp simp: bit_simps Kernel_Config.config_ARM_PA_SIZE_BITS_40_def intvl_self) + apply (solves \clarsimp simp: bit_simps Kernel_Config.config_ARM_PA_SIZE_BITS_40_def intvl_self\) apply simp done diff --git a/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy b/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy index e42dd1b32e..a9f92a1061 100644 --- a/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy @@ -840,7 +840,7 @@ proof - have m1: "(-1::vm_level) = (if config_ARM_PA_SIZE_BITS_40 then 3 else 4)" by (simp add: Kernel_Config.config_ARM_PA_SIZE_BITS_40_def) show ?thesis unfolding asid_pool_level_def - by (simp add: m1) + by (simp add: m1 Kernel_Config.config_ARM_PA_SIZE_BITS_40_def) qed lemma asid_pool_level_not_0[simp]: @@ -864,7 +864,8 @@ next note maxBound_minus_one_bit[simp del] assume "x \ max_pt_level" thus "x \ asid_pool_level" - unfolding level_defs by (auto simp: maxBound_size_bit split: if_splits) + unfolding level_defs + by (auto simp: maxBound_size_bit Kernel_Config.config_ARM_PA_SIZE_BITS_40_def split: if_splits) qed lemma asid_pool_level_eq: @@ -891,7 +892,9 @@ lemma vm_level_less_max_pt_level: lemma vm_level_less_le_1: "\ (level' :: vm_level) < level \ \ level' \ level' + 1" - by (fastforce dest: max_pt_level_enum vm_level_less_max_pt_level split: if_split_asm) + by (fastforce dest: max_pt_level_enum vm_level_less_max_pt_level + simp: Kernel_Config.config_ARM_PA_SIZE_BITS_40_def + split: if_split_asm) lemma asid_pool_level_leq_conv[iff]: "(asid_pool_level \ level) = (level = asid_pool_level)" @@ -905,7 +908,7 @@ lemma max_pt_level_not_asid_pool_level[simp]: "max_pt_level \ asid_pool_level" "asid_pool_level \ max_pt_level" by (simp add: asid_pool_level_def) - (simp add: level_defs) + (simp add: level_defs Kernel_Config.config_ARM_PA_SIZE_BITS_40_def) lemma asid_pool_level_minus: "asid_pool_level = -1" diff --git a/proof/refine/AARCH64/ArchAcc_R.thy b/proof/refine/AARCH64/ArchAcc_R.thy index c21322d823..dc16debeb1 100644 --- a/proof/refine/AARCH64/ArchAcc_R.thy +++ b/proof/refine/AARCH64/ArchAcc_R.thy @@ -603,6 +603,8 @@ lemma user_region_or: "\ vref \ user_region; vref' \ user_region \ \ vref || vref' \ user_region" by (simp add: user_region_def canonical_user_def le_mask_high_bits word_size) +lemmas bit_pred = bit0.pred bit1.pred + lemma lookupPTSlotFromLevel_corres: "\ level' = size level; pt' = pt; level \ max_pt_level \ \ corres (\(level, p) (bits, p'). bits = pt_bits_left level \ p' = p) @@ -619,7 +621,7 @@ next from `0 < level` obtain nlevel where nlevel: "level = nlevel + 1" by (auto intro: that[of "level-1"]) with `0 < level` - have nlevel1: "nlevel < nlevel + 1" using bit1.pred by fastforce + have nlevel1: "nlevel < nlevel + 1" using bit_pred by fastforce with nlevel have level: "size level = Suc (size nlevel)" by simp @@ -672,7 +674,7 @@ next apply (simp add: plus_one_eq_asid_pool vref_for_level_def pt_bits_left_def) apply (rule conjI, simp add: max_pt_level_def) apply (clarsimp simp: level_defs bit_simps maxPTLevel_def) - apply word_eqI_solve + apply (solves \cases config_ARM_PA_SIZE_BITS_40; clarsimp?; word_eqI_solve\) apply (clarsimp simp: vref_for_level_def pt_bits_left_def) apply (rule conjI; clarsimp) apply (subgoal_tac "nlevel = max_pt_level - 1") @@ -684,11 +686,13 @@ next apply (simp add: pt_bits_def) apply (prop_tac "level_type (nlevel + 1) = NormalPT_T") apply (drule max_pt_level_enum) - apply (auto simp: level_defs split: if_split_asm)[1] + (* Unfolding config_ARM_PA_SIZE_BITS_40_def here, because the level_enum only produces a + contradiction in one of the branches when PA_40 is set. *) + apply (solves \auto simp: level_defs Kernel_Config.config_ARM_PA_SIZE_BITS_40_def\)[1] apply (simp add: bit_simps) apply word_eqI apply (drule max_pt_level_enum) - by (auto split: if_split_asm) + by (cases config_ARM_PA_SIZE_BITS_40, auto simp: max_pt_level_def2) from `0 < level` `level' = size level` `pt' = pt` level `level \ max_pt_level` level_m1 show ?case @@ -828,7 +832,7 @@ next apply (simp add: plus_one_eq_asid_pool vref_for_level_def pt_bits_left_def) apply (rule conjI, simp add: max_pt_level_def) apply (clarsimp simp: level_defs bit_simps maxPTLevel_def) - apply word_eqI_solve + apply (solves \cases config_ARM_PA_SIZE_BITS_40; clarsimp?; word_eqI_solve\) apply (clarsimp simp: vref_for_level_def pt_bits_left_def) apply (rule conjI; clarsimp) apply (subgoal_tac "nlevel = max_pt_level - 1") @@ -840,11 +844,13 @@ next apply (simp add: pt_bits_def) apply (prop_tac "level_type (nlevel + 1) = NormalPT_T") apply (drule max_pt_level_enum) - apply (auto simp: level_defs split: if_split_asm)[1] + (* Unfolding config_ARM_PA_SIZE_BITS_40_def here, because the level_enum only produces a + contradiction in one of the branches when PA_40 is set. *) + apply (solves \auto simp: level_defs Kernel_Config.config_ARM_PA_SIZE_BITS_40_def split: if_split_asm\)[1] apply (simp add: bit_simps) apply word_eqI apply (drule max_pt_level_enum) - by (auto split: if_split_asm) + by (cases config_ARM_PA_SIZE_BITS_40, auto simp: max_pt_level_def2) note vm_level.size_minus_one[simp] from minus.prems