| (* |
| * Copyright 2016, NICTA |
| * |
| * This software may be distributed and modified according to the terms of |
| * the GNU General Public License version 2. Note that NO WARRANTY is provided. |
| * See "LICENSE_GPLv2.txt" for details. |
| * |
| * @TAG(NICTA_GPL) |
| *) |
| |
| theory FunBucket |
| imports |
| TypBucket |
| L4vBucket |
| begin |
| |
| definition count :: "'a list \<Rightarrow> ('b::len) word" |
| where |
| "count xs \<equiv> of_nat (length xs) :: 'b word" |
| |
| definition is_pow_of_2 :: "U32 \<Rightarrow> bool" |
| where |
| "is_pow_of_2 x \<equiv> \<exists>k. x = 1 << k \<and> k < 32" |
| |
| declare fun_app_def [iff] |
| |
| text {* slice: Return a slice of a list, frm and to are offset from the |
| beginning of the list *} |
| definition |
| slice :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
| where |
| "slice frm to xs \<equiv> drop frm $ take to xs" |
| |
| lemma length_slice: |
| "length (slice f t xs) = min (length xs) t - f" |
| by (simp add: slice_def) |
| |
| lemma slice_n_n: |
| "slice n n xs = []" |
| by (simp add: slice_def) |
| |
| lemma slice_append: "slice f t (xs @ ys) = slice f t xs @ slice (f - min (length xs) t) (t - length xs) ys" |
| by (simp add: slice_def) |
| |
| lemmas slice_simps = length_slice slice_n_n slice_append slice_def |
| |
| lemma sub_mod_mask: |
| "\<lbrakk>k < 32 \<rbrakk> \<Longrightarrow> (x::32 word) - x mod 2^k = x && ~~ mask k" |
| apply (simp add: word_mod_2p_is_mask p2_gt_0 mask_out_sub_mask) |
| done |
| |
| lemma alignUp_not_aligned_eq2: |
| " \<not> is_aligned a n \<Longrightarrow> Word_Lib.alignUp a n = ((a >> n) + 1) << n" |
| apply (cases "n < size a") |
| apply (subst alignUp_not_aligned_eq, assumption) |
| apply (simp add: word_size) |
| apply (simp add: shiftr_div_2n_w shiftl_t2n) |
| apply (simp add: Word_Lib.alignUp_def power_overflow |
| word_size complement_def shiftl_zero_size) |
| done |
| |
| lemma alignUp_not_aligned_eq3: |
| "\<not> is_aligned a n \<Longrightarrow> Word_Lib.alignUp a n = (a && ~~ mask n) + (1 << n)" |
| by (simp add: alignUp_not_aligned_eq2 word_shiftl_add_distrib and_not_mask) |
| |
| 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 align32_alignUp: |
| "\<lbrakk>y = 1 << k; k < 32\<rbrakk> \<Longrightarrow> align32(x,y) = alignUp x k" |
| apply (clarsimp simp: align32_def) |
| apply (fold mask_def[simplified]) |
| apply (subst mask_def, simp) |
| apply (subst add_diff_eq) |
| apply (subst alignUp_def2[symmetric]) |
| by simp |
| |
| lemma align32_eq: |
| "\<lbrakk>y=1<<k; k < 32\<rbrakk> \<Longrightarrow> align32(x,y) = (if y udvd x then x else x + y - (x mod y))" |
| apply (simp add: align32_alignUp) |
| apply safe |
| apply (simp add: udvd_iff_dvd) |
| apply (simp add: and_mask_dvd_nat) |
| apply (simp only: is_aligned_mask[symmetric]) |
| apply (simp add: alignUp_idem) |
| apply (subst diff_add_eq[symmetric]) |
| apply (subst sub_mod_mask, assumption) |
| apply (subst alignUp_not_aligned_eq3) |
| apply (clarsimp simp: is_aligned_def udvd_iff_dvd) |
| apply clarsimp |
| done |
| |
| lemma align32_unchanged: |
| "\<lbrakk>is_pow_of_2 a; a udvd x\<rbrakk> \<Longrightarrow> align32 (x,a) = x" |
| by (clarsimp simp: is_pow_of_2_def align32_eq) |
| |
| lemma alignUp_not_aligned_eq': "\<not> is_aligned x k |
| \<Longrightarrow> alignUp x k = x + (2 ^ k - (x && mask k))" |
| apply (subst alignUp_not_aligned_eq3, assumption) |
| apply (subst mask_out_sub_mask) |
| apply simp |
| done |
| |
| lemma al_dvd_align32: |
| "\<lbrakk>is_pow_of_2 al; v < v + al\<rbrakk> \<Longrightarrow> al udvd align32 (v, al)" |
| by (clarsimp simp: is_pow_of_2_def align32_alignUp |
| udvd_iff_dvd is_aligned_def[symmetric]) |
| |
| lemma align32_le: |
| "\<lbrakk>is_pow_of_2 al; v < v + al\<rbrakk> \<Longrightarrow> v \<le> align32 (v, al)" |
| apply (case_tac "v=0", clarsimp simp: align32_alignUp) |
| apply (clarsimp simp: align32_alignUp is_pow_of_2_def) |
| apply (case_tac "is_aligned v k") |
| apply (rule alignUp_ge, simp) |
| apply (rule_tac x=v in alignUp_is_aligned_nz) |
| apply simp |
| apply simp |
| apply simp |
| apply simp |
| apply (simp add: alignUp_not_aligned_eq') |
| apply (drule word_less_sub_1) |
| apply (rule word_plus_mono_right2) |
| apply (subst(asm) field_simps[symmetric], assumption) |
| apply (rule word_le_minus_mono_right) |
| apply (clarsimp simp: lt1_neq0 is_aligned_mask) |
| apply (rule order_trans, rule word_and_le1) |
| apply (rule order_less_imp_le) |
| apply (simp add: mask_lt_2pn) |
| apply (simp add: word_1_le_power) |
| done |
| |
| lemma align32_ge: |
| "\<lbrakk>is_pow_of_2 al; v < v + al\<rbrakk> \<Longrightarrow> align32 (v, al) \<ge> v" |
| by (auto simp:align32_le) |
| |
| lemma alignUp_greater: |
| "\<lbrakk>(v::32 word) < 2^n; v \<noteq> 0\<rbrakk> \<Longrightarrow> alignUp v n = 2^n" |
| apply (subst alignUp_not_aligned_eq') |
| apply (clarsimp simp: aligned_small_is_0) |
| apply (simp add: less_mask_eq) |
| done |
| |
| 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_triv2: |
| "is_aligned (2^a) a" |
| apply (case_tac "word_bits\<le> a") |
| apply (simp add:is_aligned_triv)+ |
| done |
| |
| 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 mask_lower_twice: |
| "n \<le> m \<Longrightarrow> (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 alignUp_distance: |
| "(alignUp (q :: 'a :: len word) sz) - q \<le> mask sz" |
| apply (case_tac "len_of TYPE('a) \<le> 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)) \<le> 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 \<noteq> 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 alignUp_nz: |
| "\<lbrakk>(v :: 32 word) \<noteq> 0; v < v + 2^k; k < 32\<rbrakk> \<Longrightarrow> alignUp v k \<noteq> 0" |
| apply (cut_tac v=v and al="2^k" in align32_le, simp add: is_pow_of_2_def) |
| apply (rule_tac x=k in exI, simp+) |
| apply (subst (asm) align32_alignUp[simplified], simp+) |
| apply auto |
| done |
| |
| lemma aligned_neq_into_ineq: |
| fixes x :: "'a::len word" |
| assumes neq: "x \<noteq> y" |
| and alx: "is_aligned x sz" |
| and aly: "is_aligned y sz" |
| shows "x + 2 ^ sz - 1 < y \<or> y + 2 ^ sz - 1 < x" |
| proof - |
| note no_ov = aligned_neq_into_no_overlap [OF neq alx aly] |
| note x = eqset_imp_iff[OF no_ov, where x=x] |
| note y = eqset_imp_iff[OF no_ov, where x=y] |
| from x y show ?thesis |
| apply (simp add: is_aligned_no_overflow' alx aly) |
| apply (auto simp: field_simps) |
| done |
| qed |
| |
| lemma align32_upper_bound: |
| "\<lbrakk>v \<le> bound; is_pow_of_2 al; al udvd bound; v < v + al\<rbrakk> \<Longrightarrow> |
| align32 (v, al) \<le> bound" |
| apply (case_tac "v=0") |
| apply (clarsimp simp: align32_alignUp is_pow_of_2_def alignUp_def2 mask_def) |
| apply (clarsimp simp: is_pow_of_2_def) |
| apply (subst (asm) udvd_iff_dvd) |
| apply simp |
| apply (fold is_aligned_def) |
| apply (subst align32_alignUp, simp+) |
| apply (case_tac "is_aligned v k") |
| apply (simp add: alignUp_idem) |
| apply (case_tac "al > v") |
| apply (subst alignUp_greater, simp+) |
| apply (drule_tac a=bound in is_aligned_less_sz) |
| apply clarsimp |
| apply (simp add: le_def[symmetric]) |
| apply (simp add: le_def[symmetric]) |
| apply (cut_tac p=v and n=k in is_aligned_alignUp) |
| apply (cut_tac q=v and sz=k in alignUp_distance) |
| apply (drule word_diff_ls'(3)) |
| apply (drule word_less_sub_1) |
| apply (simp add: mask_def word_less_sub_1) |
| apply (subst diff_add_eq) |
| apply (simp add: add.commute) |
| apply (case_tac "v + 2^k \<le> bound") |
| apply (simp add: mask_def) |
| apply (cut_tac v=v and k=k in alignUp_nz, simp+) |
| apply (metis (erased, hide_lams) add.commute add_diff_eq |
| not_less order_trans word_le_less_eq word_less_1 word_sub_le) |
| apply (subst (asm) word_not_le) |
| apply (case_tac "bound = alignUp v k") |
| apply simp |
| apply (frule_tac x=bound and y="alignUp v k" and sz=k |
| in aligned_neq_into_ineq, assumption+) |
| apply (simp add: mask_def) |
| apply safe |
| apply (simp add: L4vBucket.alignUp_le_greater_al) |
| apply (simp add: L4vBucket.alignUp_le_greater_al) |
| done |
| |
| lemma align32_idempotence: |
| "is_pow_of_2 y \<Longrightarrow> x < x + y \<Longrightarrow> |
| align32 (align32 (x, y), y) = align32 (x, y)" |
| apply (frule (1) al_dvd_align32) |
| apply (erule (1) align32_unchanged) |
| done |
| |
| |
| end |
