From 9e5a7583fccf30eb1df7db042310e2eefff93375 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 18 Feb 2021 10:55:56 +1100 Subject: [PATCH] isabelle-2021: update SysInit Signed-off-by: Gerwin Klein --- sys-init/CreateObjects_SI.thy | 5 ++++- sys-init/InitCSpace_SI.thy | 2 +- sys-init/InitTCB_SI.thy | 2 +- sys-init/InitVSpace_SI.thy | 2 +- sys-init/ObjectInitialised_SI.thy | 2 +- sys-init/Proof_SI.thy | 2 +- sys-init/StartThreads_SI.thy | 2 +- sys-init/WellFormed_SI.thy | 15 +++++++-------- 8 files changed, 17 insertions(+), 15 deletions(-) diff --git a/sys-init/CreateObjects_SI.thy b/sys-init/CreateObjects_SI.thy index a4156c36e..47057c769 100644 --- a/sys-init/CreateObjects_SI.thy +++ b/sys-init/CreateObjects_SI.thy @@ -204,7 +204,8 @@ lemma retype_untyped_wp: (si_cnode_id, unat seL4_CapInitThreadCNode) \c si_cnode_cap \* R\ s \ (\has_children (si_cnode_id,unat untyped_cptr) (kernel_state s) \ cover_ids = available_ids) \ list_all (\index. has_children (si_cnode_id, untyped_slots ! index) (kernel_state s)) indices)\" - (* I would like to remove this later by rewritting seL4_Untyped_Retype_sep *) + including no_take_bit + (* I would like to remove this later by rewriting seL4_Untyped_Retype_sep *) apply (subgoal_tac "si_cspace_cap=si_cnode_cap", simp) apply (unfold retype_untyped_def) apply (rule hoare_chain) @@ -704,6 +705,7 @@ lemma retype_untyped_loop_inv_success: list_all (\index. \has_children (si_cnode_id,untyped_slots!index) (kernel_state s) \ is_full_untyped_cap (untyped_caps!index)) [0 ..< length untyped_slots] \ si_caps = map_of (zip (take obj_id_index obj_ids) free_cptrs))\" + including no_take_bit apply (subst list_all_imp_filter2)+ apply (rule hoare_ex_pre hoare_ex_pre_conj)+ apply (rule hoare_grab_asm2)+ @@ -954,6 +956,7 @@ lemma retype_untyped_loop_inv_fail: list_all (\index. \has_children (si_cnode_id,untyped_slots!index) (kernel_state s) \ is_full_untyped_cap (untyped_caps!index)) [0 ..< length untyped_slots] \ si_caps = map_of (zip (take obj_id_index obj_ids) free_cptrs))\" + including no_take_bit apply (subst list_all_imp_filter2)+ apply (rule valid_imp_ex)+ apply (rule hoare_ex_pre hoare_ex_pre_conj)+ diff --git a/sys-init/InitCSpace_SI.thy b/sys-init/InitCSpace_SI.thy index 3dca6bd84..132d1325d 100644 --- a/sys-init/InitCSpace_SI.thy +++ b/sys-init/InitCSpace_SI.thy @@ -1414,7 +1414,7 @@ lemma seL4_CNode_Mint_object_slot_initialised_sep_helper: cap_badge (default_cap NotificationType {client_object_id} (object_size_bits spec_cap_obj) dev) = 0)") prefer 2 - apply (blast intro: ep_related_capI ep_related_cap_badge_of_default) + apply (blast intro: ep_related_cap_badge_of_default) apply clarsimp apply (intro conjI, simp_all add:has_type_default_not_non ep_related_cap_default_cap diff --git a/sys-init/InitTCB_SI.thy b/sys-init/InitTCB_SI.thy index 55a9f505c..5d480a691 100644 --- a/sys-init/InitTCB_SI.thy +++ b/sys-init/InitTCB_SI.thy @@ -909,7 +909,7 @@ lemma configure_tcb_sep: and root_size = si_cnode_size and tcb_cap = "TcbCap (the (t obj_id))" and tcb = "spec2s t (the (cdl_objects spec obj_id))"] | - simp add: guard_equal_si_cspace_cap' cap_object_simps is_tcb_default_cap)+ + simp add: guard_equal_si_cspace_cap' is_tcb_default_cap)+ apply (subst offset_slot_si_cnode_size', assumption)+ apply clarsimp apply sep_solve diff --git a/sys-init/InitVSpace_SI.thy b/sys-init/InitVSpace_SI.thy index f76aaa48b..4bb2e02cc 100644 --- a/sys-init/InitVSpace_SI.thy +++ b/sys-init/InitVSpace_SI.thy @@ -304,7 +304,7 @@ lemma pd_slot_compute_from_pt[simp]: apply (rule shiftl_less_t2n, simp+) apply (clarsimp simp: shiftr_over_or_dist) apply (subst shiftl_shiftr_id, simp+) - apply (clarsimp simp: limited_and_simps) + apply (clarsimp simp: shiftl_shiftr2) apply (subst le_mask_iff [THEN iffD1]) apply (clarsimp simp: mask_def plus_one_helper) apply clarsimp diff --git a/sys-init/ObjectInitialised_SI.thy b/sys-init/ObjectInitialised_SI.thy index 73705e684..6e9d7bfc4 100644 --- a/sys-init/ObjectInitialised_SI.thy +++ b/sys-init/ObjectInitialised_SI.thy @@ -475,7 +475,7 @@ lemma is_default_cap_cap_transform [simp]: "well_formed_cap cap \ is_default_cap (cap_transform t cap) = is_default_cap cap" apply (clarsimp simp: is_default_cap_def well_formed_cap_def cap_type_def default_cap_def cap_transform_def cap_has_object_def) - apply (cases cap, simp_all add: cap_object_simps update_cap_object_def cnode_cap_size_def) + apply (cases cap, simp_all add: update_cap_object_def cnode_cap_size_def) done lemma default_cap_cap_transform: diff --git a/sys-init/Proof_SI.thy b/sys-init/Proof_SI.thy index d734b7fbb..7ab91e07f 100644 --- a/sys-init/Proof_SI.thy +++ b/sys-init/Proof_SI.thy @@ -143,7 +143,7 @@ lemma le_list_all: apply (clarsimp simp: list_all_iff) apply (subst word_arith_power_alt) apply simp - by (metis (no_types) dual_order.strict_trans2 unat_less_2_si_cnode_size word_of_int_numeral word_of_int_power_hom) + by (metis (no_types) dual_order.strict_trans2 unat_less_2_si_cnode_size) lemma list_all_drop: "list_all P xs \ list_all P (drop n xs)" diff --git a/sys-init/StartThreads_SI.thy b/sys-init/StartThreads_SI.thy index dcadef3a7..e31ecd703 100644 --- a/sys-init/StartThreads_SI.thy +++ b/sys-init/StartThreads_SI.thy @@ -84,7 +84,7 @@ lemma start_thread_sep: and cnode_cap = si_cspace_cap and root_size = si_cnode_size and tcb_cap = "TcbCap (the (t obj_id))"] | - simp add: guard_equal_si_cspace_cap' cap_object_simps is_tcb_default_cap)+ + simp add: guard_equal_si_cspace_cap' is_tcb_default_cap)+ apply (subst offset_slot_si_cnode_size', assumption)+ apply (clarsimp simp: cap_transform_MasterReplyCap) by sep_solve diff --git a/sys-init/WellFormed_SI.thy b/sys-init/WellFormed_SI.thy index b30f1d4e8..9fe97d610 100644 --- a/sys-init/WellFormed_SI.thy +++ b/sys-init/WellFormed_SI.thy @@ -96,7 +96,7 @@ lemma guard_size_shiftl_non_zero: apply (rule of_nat_n_less_equal_power_2) apply (clarsimp simp: guard_bits_def) apply (clarsimp simp: guard_bits_def) - apply (clarsimp simp: of_nat_0) + apply (clarsimp simp: of_nat_0 simp del: word_of_nat_eq_0_iff) apply (drule of_nat_0) apply (erule less_le_trans) apply (clarsimp simp: guard_bits_def word_bits_def) @@ -710,9 +710,8 @@ lemma well_formed_cap_has_object: apply (clarsimp simp: well_formed_caps_def) apply (erule_tac x=slot in allE) apply (clarsimp simp: domI) - apply (clarsimp simp: cap_has_object_def well_formed_cap_def - split: cdl_cap.splits) - done + by (clarsimp simp: cap_has_object_def well_formed_cap_def + split: cdl_cap.splits) lemma well_formed_cap_object: "\well_formed spec; opt_cap (obj_id, slot) spec = Some spec_cap; @@ -1592,10 +1591,9 @@ lemma well_formed_objects_card: apply (frule well_formed_objects_only_real_or_irq) apply (subgoal_tac " card (used_irqs spec) = card (used_irq_nodes spec)", simp) apply (subst card_Un_Int, simp+) - apply (metis Int_commute Nat.add_0_right Un_commute card_empty used_irq_nodes_def) + apply (simp add: Int_commute Un_commute used_irq_nodes_def) by (metis card_image inj_inj_on used_irq_nodes_def) - (**************************************** * Packing data into a well_formed cap. * ****************************************) @@ -1636,7 +1634,7 @@ lemma update_cap_rights_and_data: apply (drule_tac m=8 in word_shift_zero, rule less_imp_le) apply (clarsimp simp: guard_bits_def word_of_nat_less) apply simp - apply (clarsimp simp: of_nat_0 guard_bits_def word_bits_def) + apply (clarsimp simp: of_nat_0 guard_bits_def word_bits_def simp del: word_of_nat_eq_0_iff) apply (clarsimp simp: badge_update_def cap_rights_def cap_data_def guard_update_def guard_as_rawdata_def) apply (cut_tac p="word2 << 8" and d="of_nat nat1 << 3" and n=8 in is_aligned_add_or) @@ -1644,7 +1642,7 @@ lemma update_cap_rights_and_data: apply (rule shiftl_less_t2n) apply (clarsimp simp: guard_bits_def word_of_nat_less) apply simp - apply (simp add: word_ao_dist shiftr_over_or_dist shiftl_shiftr1 word_size shiftl_mask_is_0 + apply (simp add: word_ao_dist shiftr_over_or_dist shiftl_shiftr1 word_size word_bw_assocs mask_and_mask guard_as_rawdata_def guard_update_def) apply (subst le_mask_iff[THEN iffD1]) apply (rule plus_one_helper) @@ -1661,6 +1659,7 @@ lemma update_cap_rights_and_data: apply simp apply (subst less_mask_eq) apply (clarsimp simp: guard_bits_def word_of_nat_less) + including no_take_bit apply (clarsimp simp: guard_bits_def word_of_nat_less word_bits_def unat_of_nat32) done