From 0ced46820ba266be5f74704fe343b59fb519e8e2 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sat, 30 Apr 2016 14:36:27 +1000 Subject: [PATCH] manual levity into Word_Lemmas --- lib/Word_Lib/Word_Lemmas.thy | 144 ++++++++++++++++++++ proof/invariant-abstract/ARM/ArchAcc_AI.thy | 30 ---- proof/invariant-abstract/LevityCatch_AI.thy | 37 ----- proof/invariant-abstract/Untyped_AI.thy | 85 +----------- 4 files changed, 145 insertions(+), 151 deletions(-) diff --git a/lib/Word_Lib/Word_Lemmas.thy b/lib/Word_Lib/Word_Lemmas.thy index 4dfaea77a..77b671d2b 100644 --- a/lib/Word_Lib/Word_Lemmas.thy +++ b/lib/Word_Lib/Word_Lemmas.thy @@ -5327,6 +5327,150 @@ proof qed qed +lemma alignUp_def2: + "alignUp a sz = a + 2 ^ sz - 1 && ~~ mask sz" + unfolding alignUp_def[unfolded complement_def] + by (simp add:mask_def[symmetric,unfolded shiftl_t2n,simplified]) + + +lemma mask_out_first_mask_some: + "\ x && ~~ mask n = y; n \ m \ \ x && ~~ mask m = y && ~~ mask m" + apply (rule word_eqI, rename_tac n') + apply (drule_tac x=n' in word_eqD) + apply (auto simp: word_ops_nth_size word_size) + done + +lemma gap_between_aligned: + "\a < (b :: 'a ::len word); is_aligned a n; is_aligned b n; n < len_of TYPE('a) \ + \ a + (2^n - 1) < b" + apply (rule ccontr,simp add:not_less) + apply (drule le_shiftr[where n = n]) + apply (simp add: aligned_shift') + apply (case_tac "b >> n = a >> n") + apply (drule arg_cong[where f = "\x. x< alignUp (w + a) us = w + alignUp a us" + apply (clarsimp simp:alignUp_def2 add.assoc) + apply (simp add: mask_out_add_aligned field_simps) + done + +lemma mask_lower_twice: + "n \ m \ (x && ~~ mask n) && ~~ mask m = x && ~~ mask m" + apply (rule word_eqI) + apply (simp add: word_size word_ops_nth_size) + apply safe + apply simp + done + +lemma mask_lower_twice2: + "(a && ~~ mask n) && ~~ mask m = a && ~~ mask (max n m)" + by (rule word_eqI, simp add: neg_mask_bang conj_comms) + +lemma ucast_and_neg_mask: + "ucast (x && ~~ mask n) = ucast x && ~~ mask n" + apply (rule word_eqI) + apply (simp add: word_size neg_mask_bang nth_ucast) + apply (auto simp add: test_bit_bl word_size) + done + +lemma ucast_and_mask: + "ucast (x && mask n) = ucast x && mask n" + apply (rule word_eqI) + apply (simp add: nth_ucast) + apply (auto simp add: test_bit_bl word_size) + done + +lemma ucast_mask_drop: + "len_of TYPE('a :: len) \ n \ (ucast (x && mask n) :: 'a word) = ucast x" + apply (rule word_eqI) + apply (simp add: nth_ucast word_size) + apply safe + apply (simp add: test_bit_bl word_size) + done + +lemma alignUp_distance: + "alignUp (q :: 'a :: len word) sz - q \ mask sz" + apply (case_tac "len_of TYPE('a) \ sz") + apply (simp add:alignUp_def2 mask_def power_overflow) + apply (case_tac "is_aligned q sz") + apply (clarsimp simp:alignUp_def2 p_assoc_help) + apply (subst mask_out_add_aligned[symmetric],simp)+ + apply (simp add:mask_lower_twice word_and_le2) + apply (simp add:and_not_mask) + apply (subst le_mask_iff[THEN iffD1]) + apply (simp add:mask_def) + apply simp + apply (clarsimp simp:alignUp_def3) + apply (subgoal_tac "2 ^ sz - (q - (q - 1 && ~~ mask sz)) \ 2 ^ sz - 1") + apply (simp add:field_simps mask_def) + apply (rule word_sub_mono) + apply simp + apply (rule ccontr) + apply (clarsimp simp:not_le) + apply (drule eq_refl) + apply (drule order_trans[OF _ word_and_le2]) + apply (subgoal_tac "q \ 0") + apply (drule minus_one_helper[rotated]) + apply simp + apply simp + apply (fastforce) + apply (simp add: word_sub_le_iff) + apply (subgoal_tac "q - 1 && ~~ mask sz = (q - 1) - (q - 1 && mask sz)") + apply simp + apply (rule order_trans) + apply (rule word_add_le_mono2) + apply (rule word_and_le1) + apply (subst unat_plus_simple[THEN iffD1,symmetric]) + apply (simp add:not_le mask_def) + apply (rule word_sub_1_le) + apply simp + apply (rule unat_lt2p) + apply (simp add:mask_def) + apply (simp add:mask_out_sub_mask) + apply (rule word_sub_1_le) + apply simp + done + +lemma is_aligned_diff_neg_mask: + "is_aligned p sz \ (p - q && ~~ mask sz) = (p - ((alignUp q sz) && ~~ mask sz))" + apply (clarsimp simp only:word_and_le2 diff_conv_add_uminus) + apply (subst mask_out_add_aligned[symmetric]) + apply simp+ + apply (rule sum_to_zero) + apply (subst add.commute) + apply (subst mask_out_add_aligned) + apply (simp add:is_aligned_neg_mask) + apply simp + apply (subst and_not_mask[where w = "(alignUp q sz && ~~ mask sz) - q "]) + apply (subst le_mask_iff[THEN iffD1]) + apply (simp add:is_aligned_neg_mask_eq) + apply (rule alignUp_distance) + apply simp + done + lemma map_bits_rev_to_bl: "map (op !! x) [0.. x && ~~ mask n = y; n \ m \ \ x && ~~ mask m = y && ~~ mask m" - apply (rule word_eqI, drule_tac x=na in word_eqD) - apply (simp add: word_ops_nth_size word_size) - apply auto - done - - -lemma gap_between_aligned: - "\a < (b :: ('a ::len word)); is_aligned a n; - is_aligned b n;n < len_of TYPE('a) \ \ a + (2^ n - 1) < b" - apply (rule ccontr,simp add:not_less) - apply (drule le_shiftr[where n = n]) - apply (simp add: aligned_shift') - apply (case_tac "b >> n = a >> n") - apply (drule arg_cong[where f = "%x. x< vptr < kernel_base; is_aligned pd pd_bits; (x = 0) @@ -2616,12 +2592,6 @@ lemmas less_kernel_base_mapping_slots = less_kernel_base_mapping_slots_both[where x=0, simplified] -lemma mask_out_add_aligned: - assumes al: "is_aligned p n" - shows "p + (q && ~~ mask n) = (p + q) && ~~ mask n" - using mask_add_aligned [OF al] - by (simp add: mask_out_sub_mask) - lemma is_aligned_lookup_pd_slot: "\is_aligned vptr 24; is_aligned pd 6\ \ is_aligned (lookup_pd_slot pd vptr) 6" diff --git a/proof/invariant-abstract/LevityCatch_AI.thy b/proof/invariant-abstract/LevityCatch_AI.thy index b90c70ee7..38f4c1184 100644 --- a/proof/invariant-abstract/LevityCatch_AI.thy +++ b/proof/invariant-abstract/LevityCatch_AI.thy @@ -46,38 +46,10 @@ lemmas cap_irq_opt_simps[simp] = lemmas cap_irqs_simps[simp] = cap_irqs_def [unfolded cap_irq_opt_def, split_simps cap.split sum.split, simplified option.simps] -(* FIXME: move *) -lemma mask_lower_twice: - "n \ m \ (x && ~~ mask n) && ~~ mask m = x && ~~ mask m" - apply (rule word_eqI) - apply (simp add: word_size word_ops_nth_size) - apply safe - apply simp - done - -(* FIXME: move *) -lemma mask_lower_twice2: - "(a && ~~ mask n) && ~~ mask m = a && ~~ mask (max n m)" - by (rule word_eqI, simp add: neg_mask_bang conj_comms) lemma all_eq_trans: "\ \x. P x = Q x; \x. Q x = R x \ \ \x. P x = R x" by simp -(* FIXME: move *) -lemma ucast_and_neg_mask: - "ucast (x && ~~ mask n) = ucast x && ~~ mask n" - apply (rule word_eqI) - apply (simp add: word_size neg_mask_bang nth_ucast) - apply (auto simp add: test_bit_bl word_size) - done - -(* FIXME: move *) -lemma ucast_and_mask: - "ucast (x && mask n) = ucast x && mask n" - apply (rule word_eqI) - apply (simp add: nth_ucast) - apply (auto simp add: test_bit_bl word_size) - done lemma mask_out_8_le_kernel_base: "(x && ~~ mask 8 \ kernel_base >> 20) = (x \ kernel_base >> 20)" @@ -92,15 +64,6 @@ lemma mask_out_8_less_kernel_base: using mask_out_8_le_kernel_base[where x=x] by (simp add: linorder_not_less[symmetric]) -(* FIXME: move *) -lemma ucast_mask_drop: - "len_of TYPE('a :: len) \ n \ (ucast (x && mask n) :: 'a word) = ucast x" - apply (rule word_eqI) - apply (simp add: nth_ucast word_size) - apply safe - apply (simp add: test_bit_bl word_size) - done - declare liftE_wp[wp] declare case_sum_True[simp] declare select_singleton[simp] diff --git a/proof/invariant-abstract/Untyped_AI.thy b/proof/invariant-abstract/Untyped_AI.thy index 09360cad0..1ce893b5c 100644 --- a/proof/invariant-abstract/Untyped_AI.thy +++ b/proof/invariant-abstract/Untyped_AI.thy @@ -308,12 +308,8 @@ lemma data_to_obj_type_sp: apply clarsimp apply (simp add: arch_data_to_obj_type_def split: split_if_asm) done -end -lemma alignUp_def2: - "alignUp a sz = a + 2 ^ sz - 1 && ~~ mask sz" - unfolding alignUp_def[unfolded complement_def] - by (simp add:mask_def[symmetric,unfolded shiftl_t2n,simplified]) +end lemma is_aligned_triv2: "is_aligned (2^a) a" @@ -322,85 +318,6 @@ lemma is_aligned_triv2: done context begin interpretation Arch . (*FIXME: arch_split*) -lemma alignUp_def3: - "alignUp a sz = 2^ sz + (a - 1 && ~~ mask sz)" (is "?lhs = ?rhs") - apply (simp add:alignUp_def2) - apply (subgoal_tac "2 ^ sz + a - 1 && ~~ mask sz = ?rhs") - apply (clarsimp simp:field_simps) - apply (subst mask_out_add_aligned) - apply (rule is_aligned_triv2) - apply (simp add:field_simps) - done - - -lemma alignUp_plus: - "is_aligned w us \ alignUp (w + a) us = w + alignUp a us" - apply (clarsimp simp:alignUp_def2 add.assoc) - apply (simp add: mask_out_add_aligned field_simps) - done - - -lemma alignUp_distance: - "(alignUp (q :: 'a :: len word) sz) - q \ mask sz" - apply (case_tac "len_of TYPE('a) \ sz") - apply (simp add:alignUp_def2 mask_def power_overflow) - apply (case_tac "is_aligned q sz") - apply (clarsimp simp:alignUp_def2 p_assoc_help) - apply (subst mask_out_add_aligned[symmetric],simp)+ - apply (simp add:mask_lower_twice word_and_le2) - apply (simp add:and_not_mask) - apply (subst le_mask_iff[THEN iffD1]) - apply (simp add:mask_def) - apply simp - apply (clarsimp simp:alignUp_def3) - apply (subgoal_tac "2 ^ sz - (q - (q - 1 && ~~ mask sz)) \ 2 ^ sz - 1") - apply (simp add:field_simps mask_def) - apply (rule word_sub_mono) - apply simp - apply (rule ccontr) - apply (clarsimp simp:not_le) - apply (drule eq_refl) - apply (drule order_trans[OF _ word_and_le2]) - apply (subgoal_tac "q \ 0") - apply (drule minus_one_helper[rotated]) - apply simp - apply simp - apply (fastforce) - apply (simp add: word_sub_le_iff) - apply (subgoal_tac "q - 1 && ~~ mask sz = (q - 1) - (q - 1 && mask sz)") - apply simp - apply (rule order_trans) - apply (rule word_add_le_mono2) - apply (rule word_and_le1) - apply (subst unat_plus_simple[THEN iffD1,symmetric]) - apply (simp add:not_le mask_def) - apply (rule word_sub_1_le) - apply simp - apply (rule unat_lt2p) - apply (simp add:mask_def) - apply (simp add:mask_out_sub_mask) - apply (rule word_sub_1_le) - apply simp - done - - -lemma is_aligned_diff_neg_mask: - "is_aligned p sz \ (p - q && ~~ mask sz) = (p - ((alignUp q sz) && ~~ mask sz))" - apply (clarsimp simp only:word_and_le2 diff_conv_add_uminus) - apply (subst mask_out_add_aligned[symmetric]) - apply simp+ - apply (rule sum_to_zero) - apply (subst add.commute) - apply (subst mask_out_add_aligned) - apply (simp add:is_aligned_neg_mask) - apply simp - apply (subst and_not_mask[where w = "(alignUp q sz && ~~ mask sz) - q "]) - apply (subst le_mask_iff[THEN iffD1]) - apply (simp add:is_aligned_neg_mask_eq) - apply (rule alignUp_distance) - apply simp -done -end lemma strengthen_imp_ex2: "(P \ Q x y) \ (P \ (\x y. Q x y))" by auto