theory memory_cover
imports invariant
begin
section ‹partition of memory addresses of a pool›
declare [[smt_timeout = 300]]
text‹
this theory shows that all memory blocks are a COVER of address space of a memory pool.
A COVER means blocks are disjoint and continuous.
It means that for any memory address of a memory pool, the address is in the address range of only one block.
Due to algorithm, address range of each block is implicitly derived.
address range of a block at level $ii$ with block index $jj$ at this level is
{jj * (max\_sz mp div ($4 ^ ii$)) ..< Suc jj * (max\_sz mp div ($4 ^ ii$))}.
›
abbreviation "addr_in_block mp addr ii jj ≡
ii < length (levels mp) ∧ jj < length (bits (levels mp ! ii))
∧ (bits (levels mp ! ii) ! jj = FREE ∨ bits (levels mp ! ii) ! jj = FREEING ∨
bits (levels mp ! ii) ! jj = ALLOCATED ∨ bits (levels mp ! ii) ! jj = ALLOCATING)
∧ addr ∈ {jj * (max_sz mp div (4 ^ ii)) ..< Suc jj * (max_sz mp div (4 ^ ii))}"
abbreviation mem_cover_mp :: "State ⇒ mempool_ref ⇒ bool"
where "mem_cover_mp s p ≡
let mp = mem_pool_info s p in (∀addr < n_max mp * max_sz mp. (∃!(i,j). addr_in_block mp addr i j) )"
definition mem_cover :: "State ⇒ bool"
where "mem_cover s ≡ ∀p∈mem_pools s. mem_cover_mp s p"
lemma split_div_lemma:
assumes "0 < n"
shows "n * q ≤ m ∧ m < n * Suc q ⟷ q = ((m::nat) div n)" (is "?lhs ⟷ ?rhs")
proof
assume ?rhs
with minus_mod_eq_mult_div [symmetric] have nq: "n * q = m - (m mod n)" by simp
then have A: "n * q ≤ m" by simp
have "n - (m mod n) > 0" using mod_less_divisor assms by auto
then have "m < m + (n - (m mod n))" by simp
then have "m < n + (m - (m mod n))" by simp
with nq have "m < n + n * q" by simp
then have B: "m < n * Suc q" by simp
from A B show ?lhs ..
next
assume P: ?lhs
then show ?rhs
using div_nat_eqI by blast
qed
lemma align_up_ge_low:
"sz1 > 0 ⟹ sz2 > sz1 ⟹ sz2 mod sz1 = 0 ⟹ (addr::nat) div sz2 * sz2 + sz2 ≥ addr div sz1 * sz1 + sz1"
apply(subgoal_tac "∃n>0. sz2 = n * sz1") prefer 2 apply auto[1]
apply(rule subst[where s="addr - addr mod sz1" and t="addr div sz1 * sz1"])
using minus_mod_eq_div_mult apply auto[1]
apply(rule subst[where s="addr - addr mod sz2" and t="addr div sz2 * sz2"])
using minus_mod_eq_div_mult apply auto[1]
apply(subgoal_tac "sz1 - addr mod sz1 ≤ sz2 - addr mod sz2")
apply(subgoal_tac "addr mod sz1 < sz1") prefer 2 apply simp
apply(subgoal_tac "addr mod sz2 < sz2") prefer 2 apply simp
apply simp
apply clarsimp
apply(case_tac "addr mod (sz1 * n) ≥ sz1 * (n - 1)")
apply(subgoal_tac "addr mod (sz1 * n) = sz1 * (n - 1) + addr mod sz1")
prefer 2 using Suc_lessD Suc_pred' mod_less_divisor
mult_div_mod_eq nat_0_less_mult_iff mod_mult_self4 split_div_lemma
apply (metis mod_mult2_eq)
apply clarsimp
apply (metis (no_types, lifting) Nat.diff_diff_right One_nat_def Suc_lessD add_diff_cancel_left'
le_add1 less_numeral_extra(3) less_or_eq_imp_le mult.commute mult_eq_if)
by (metis (no_types, lifting) Nat.le_diff_conv2 Suc_lessD add_mono_thms_linordered_semiring(1)
diff_le_self less_numeral_extra(3) mod_le_divisor mult.commute mult_eq_if mult_pos_pos nat_le_linear)
lemma addr_exist_block_h1_1:
"li < ii ⟹ ii < nl ⟹ (4::nat) ^ nl div 4 ^ ii < 4 ^ nl div 4 ^ li"
apply(rule subst[where s="4 ^ (nl - ii)" and t="4 ^ nl div 4 ^ ii"])
apply (simp add: div2_eq_minus)
apply(rule subst[where s="4 ^ (nl - li)" and t="4 ^ nl div 4 ^ li"])
apply (simp add: div2_eq_minus)
apply auto
done
lemma mod_time: "(x::nat) mod m = 0 ⟹ n * x mod (n * m) = 0"
by simp
lemma addr_exist_block_h1:
"li < ii ⟹
∃n>0. msz = (4 * n) * (4 ^ nl) ⟹
ii < nl ⟹
Suc (addr div (msz div 4 ^ ii)) * (msz div 4 ^ ii)
≤ Suc (addr div (msz div 4 ^ ii) div 4 ^ (ii - li)) * (msz div 4 ^ li)"
apply(rule subst[where s="(addr div (msz div 4 ^ ii)) * (msz div 4 ^ ii) + (msz div 4 ^ ii)"
and t="Suc (addr div (msz div 4 ^ ii)) * (msz div 4 ^ ii)"]) apply auto[1]
apply(rule subst[where s="(addr div (msz div 4 ^ ii) div 4 ^ (ii - li)) * (msz div 4 ^ li) + (msz div 4 ^ li)"
and t="Suc (addr div (msz div 4 ^ ii) div 4 ^ (ii - li)) * (msz div 4 ^ li)"]) apply auto[1]
apply(rule subst[where s="addr div (msz div 4 ^ li)" and t="addr div (msz div 4 ^ ii) div 4 ^ (ii - li)"])
apply(rule subst[where s="addr div (msz div 4 ^ ii * 4 ^ (ii - li))" and t="addr div (msz div 4 ^ ii) div 4 ^ (ii - li)"])
using div2_eq_divmul[of addr "msz div 4 ^ ii" "4 ^ (ii - li)"] apply simp
apply(rule subst[where s="msz div 4 ^ li" and t="msz div 4 ^ ii * 4 ^ (ii - li)"])
apply(subgoal_tac "msz mod 4 ^ ii = 0") prefer 2
using ge_pow_mod_0 apply auto[1]
apply (smt add_diff_inverse_nat less_imp_le_nat mod_div_self mult.left_commute
nonzero_mult_div_cancel_left not_less power_add power_not_zero rel_simps(76))
apply fast
apply(rule align_up_ge_low[of "msz div 4 ^ ii" "msz div 4 ^ li" addr])
apply (metis ge_pow_mod_0 mod_div_self nat_0_less_mult_iff zero_less_numeral zero_less_power)
apply clarsimp apply(subgoal_tac "4 ^ nl div 4 ^ ii < 4 ^ nl div 4 ^ li")
prefer 2 using addr_exist_block_h1_1[of li ii nl] apply simp
using m_mod_div pow_mod_0 apply auto[1]
apply clarsimp using mod_time[of "4 ^ nl div 4 ^ li" "4 ^ nl div 4 ^ ii"]
by (smt less_imp_add_positive mod_div_self mod_mult_self1_is_0 mult.left_commute
nonzero_mult_div_cancel_left power_add power_not_zero zero_neq_numeral)
lemma divornoe_imp_div_noe_neigh:
"∀li≤ii. get_bit_s s p li (jj div 4 ^ (ii - li)) = DIVIDED ∨ get_bit_s s p li (jj div 4 ^ (ii - li)) = NOEXIST ⟹
get_bit_s s p NULL (jj div 4 ^ ii) = DIVIDED ⟹
get_bit_s s p ii jj = NOEXIST ⟹
ii > 0 ⟹
∃n. n > 0 ∧ n≤ii ∧ get_bit_s s p (n-1) (jj div 4 ^ (ii - (n-1))) = DIVIDED ∧
get_bit_s s p n (jj div 4 ^ (ii - n)) = NOEXIST"
apply(induction ii arbitrary: jj)
apply simp
apply(case_tac "get_bit_s s p ii (jj div 4) = DIVIDED")
apply auto[1]
apply(subgoal_tac "get_bit_s s p ii (jj div 4) = NOEXIST")
prefer 2
apply (metis One_nat_def Suc_diff_Suc diff_self_eq_0 lessI less_imp_le_nat power_one_right)
apply(case_tac "ii = 0") apply auto[1]
apply(subgoal_tac "∀li≤ii. get_bit_s s p li ((jj div 4) div 4 ^ (ii - li)) = DIVIDED
∨ get_bit_s s p li ((jj div 4) div 4 ^ (ii - li)) = NOEXIST")
prefer 2 apply clarsimp
apply (metis Suc_diff_le div_mult2_eq le_SucI power_Suc)
apply(subgoal_tac "∃n>NULL. n ≤ ii ∧
get_bit_s s p (n - 1) ((jj div 4) div 4 ^ (ii - (n - 1))) = DIVIDED ∧
get_bit_s s p n ((jj div 4) div 4 ^ (ii - n)) = NOEXIST")
prefer 2 apply (simp add: Divides.div_mult2_eq)
proof -
fix iia :: nat and jja :: nat
assume "∃n>NULL. n ≤ iia ∧ get_bit_s s p (n - 1) (jja div 4 div 4 ^ (iia - (n - 1))) = DIVIDED
∧ get_bit_s s p n (jja div 4 div 4 ^ (iia - n)) = NOEXIST"
then obtain nn :: nat where
f1: "NULL < nn ∧ nn ≤ iia ∧ get_bit_s s p nn (jja div 4 div 4 ^ (iia - nn)) = NOEXIST
∧ get_bit_s s p (nn - 1) (jja div 4 div 4 ^ (iia - (nn - 1))) = DIVIDED"
by meson
then have f2: "get_bit_s s p nn (jja div 4 ^ Suc (iia - nn)) = NOEXIST"
by (metis (no_types) div_mult2_eq semiring_normalization_rules(27))
have f3: "get_bit_s s p (nn - 1) (jja div 4 ^ Suc (Suc (iia - nn))) = DIVIDED"
using f1 by (metis (no_types) Suc_diff_eq_diff_pred Suc_diff_le div_mult2_eq semiring_normalization_rules(27))
have "nn ≤ iia ∧ NULL < nn"
using f1 by meson
then show "∃n>NULL. n ≤ Suc iia ∧ get_bit_s s p (n - 1) (jja div 4 ^ (Suc iia - (n - 1))) = DIVIDED
∧ get_bit_s s p n (jja div 4 ^ (Suc iia - n)) = NOEXIST"
using f3 f2 Suc_diff_le le_Suc_eq by auto
qed
lemma addr_exist_block:
assumes
p2: "inv_bitmap0 s" and
p3: "inv_bitmap s" and
p6: "inv_mempool_info s" and
p4: "p ∈ mem_pools s" and
p7: "inv_bitmapn s" and
p5: "addr < n_max (mem_pool_info s p) * max_sz (mem_pool_info s p)"
shows "∃i j. addr_in_block (mem_pool_info s p) addr i j"
proof -
obtain ii where ii: "ii = length (levels (mem_pool_info s p)) - 1" by auto
obtain jj where jj: "jj = addr div (max_sz (mem_pool_info s p) div (4 ^ ii))" by auto
have bits_len_nmax: "∀i<length (levels (mem_pool_info s p)). length (bits (levels (mem_pool_info s p) ! i)) = (n_max (mem_pool_info s p)) * 4 ^ i"
using p6 p4 by(simp add:inv_mempool_info_def Let_def)
have maxsz: "∃n>0. max_sz (mem_pool_info s p) = (4 * n) * (4 ^ n_levels (mem_pool_info s p))"
using p4 p6 apply(simp add:inv_mempool_info_def Let_def) by auto
have nl_eq_len: "n_levels (mem_pool_info s p) = length (levels (mem_pool_info s p))"
using p4 p6 by(simp add:inv_mempool_info_def Let_def)
from ii have ii_len: "ii < length (levels (mem_pool_info s p))"
by (metis diff_less inv_mempool_info_def length_greater_0_conv p4 p6 rel_simps(68))
from ii p6 have blk_ii: "max_sz (mem_pool_info s p) div 4 ^ ii > 0"
by (smt Euclidean_Division.div_eq_0_iff divisors_zero gr0I ii_len less_imp_le_nat
m_mod_div maxsz mod_if nl_eq_len pow_mod_0 power_not_zero zero_neq_numeral)
hence addr_ran: "addr ∈ {jj * (max_sz (mem_pool_info s p) div (4 ^ ii)) ..< Suc jj * (max_sz (mem_pool_info s p) div (4 ^ ii))}"
using jj div_in_suc[of "max_sz (mem_pool_info s p) div 4 ^ ii" jj addr] by blast
have jj_lt_maxdiv4ii: "jj < n_max (mem_pool_info s p) * 4 ^ ii"
apply(rule subst[where s="addr div (max_sz (mem_pool_info s p) div 4 ^ ii)" and t="jj"]) using jj apply fast
apply(rule subst[where s="n_max (mem_pool_info s p) * max_sz (mem_pool_info s p) div (max_sz (mem_pool_info s p) div 4 ^ ii)"
and t="n_max (mem_pool_info s p) * 4 ^ ii"]) using ii_len maxsz
apply (metis (no_types, lifting) blk_ii ge_pow_mod_0 inv_mempool_info_def m_mod_div
mod_div_self mod_mult_self1_is_0 neq0_conv nonzero_mult_div_cancel_left p4 p6)
apply(rule mod_div_gt[of addr "n_max (mem_pool_info s p) * max_sz (mem_pool_info s p)"
"max_sz (mem_pool_info s p) div 4 ^ ii"]) using p5 apply fast
using maxsz nl_eq_len
apply (metis ge_pow_mod_0 ii_len mod_div_self mod_mult_right_eq mod_mult_self1_is_0 mult_0_right)
done
have lvlii_eq_last: "levels (mem_pool_info s p) ! ii = last (levels (mem_pool_info s p))"
apply(subgoal_tac "length (levels (mem_pool_info s p)) > 0")
prefer 2 using p4 p6 ii jj_lt_maxdiv4ii p4 p6 ii_len apply(simp add:inv_mempool_info_def Let_def)
using ii apply clarsimp
by (simp add: last_conv_nth)
have jj_lt_len_lstbits: "jj < length (bits (last (levels (mem_pool_info s p))))"
using ii jj_lt_maxdiv4ii p4 p6 ii_len apply(simp add:inv_mempool_info_def Let_def)
apply(subgoal_tac "length (bits (levels (mem_pool_info s p) ! ii)) = n_max (mem_pool_info s p) * 4 ^ ii")
prefer 2 apply auto[1]
apply(subgoal_tac "levels (mem_pool_info s p) ! ii = last (levels (mem_pool_info s p))")
prefer 2 apply(subgoal_tac "length (levels (mem_pool_info s p)) > 0")
prefer 2 using p4 p6 apply(simp add:inv_mempool_info_def Let_def) apply clarsimp
apply (simp add: last_conv_nth)
by fastforce
have "∃li≤ii. addr_in_block (mem_pool_info s p) addr li (jj div 4 ^ (ii - li))"
proof -
{
assume asm: "¬ (∃li≤ii. addr_in_block (mem_pool_info s p) addr li (jj div 4 ^ (ii - li)))"
from asm have "∀li≤ii. ¬ addr_in_block (mem_pool_info s p) addr li (jj div 4 ^ (ii - li))" by fast
moreover
from ii have ii_len: "ii < length (levels (mem_pool_info s p))"
by (metis diff_less inv_mempool_info_def length_greater_0_conv p4 p6 rel_simps(68))
moreover
have "∀li≤ii. addr ∈ {jj div 4 ^ (ii - li) * (max_sz (mem_pool_info s p) div 4 ^ li)..<
Suc (jj div 4 ^ (ii - li)) * (max_sz (mem_pool_info s p) div 4 ^ li)}"
apply(subgoal_tac "∃n>0. max_sz (mem_pool_info s p) = (4 * n) * (4 ^ n_levels (mem_pool_info s p))")
prefer 2 using p4 p6 apply(simp add:inv_mempool_info_def Let_def) apply auto[1]
apply(subgoal_tac "n_levels (mem_pool_info s p) = length (levels (mem_pool_info s p)) ∧
length (levels (mem_pool_info s p)) > 0")
prefer 2 using p4 p6 apply(simp add:inv_mempool_info_def Let_def) apply auto[1]
apply clarify apply auto
apply(subgoal_tac "jj * (max_sz (mem_pool_info s p) div 4 ^ ii)
≥ jj div 4 ^ (ii - li) * (max_sz (mem_pool_info s p) div 4 ^ li)")
prefer 2 apply(case_tac "li = ii") apply auto[1]
using Divides.div_mult2_eq Groups.mult_ac(2) blk_ii add_diff_inverse_nat calculation(2)
div_mult_self_is_m divisors_zero ge_pow_mod_0 mod_div_self neq0_conv not_less power_add
semiring_normalization_rules(17) split_div_lemma zero_less_numeral zero_less_power
apply (smt div_mult_self1_is_m nat_mult_le_cancel_disj)
using addr_ran apply auto[1]
apply(subgoal_tac "Suc jj * (max_sz (mem_pool_info s p) div (4 ^ ii))
≤ Suc (jj div 4 ^ (ii - li)) * (max_sz (mem_pool_info s p) div 4 ^ li)")
prefer 2 apply(case_tac "li = ii") apply simp
apply(rule subst[where s="addr div (max_sz (mem_pool_info s p) div (4 ^ ii))" and t="jj"]) using jj apply fast
using addr_exist_block_h1[of _ ii "max_sz (mem_pool_info s p)" "n_levels (mem_pool_info s p)" addr]
ii_len nl_eq_len maxsz apply fastforce
using addr_ran ii_len apply auto[1]
done
moreover
have li_len: "∀li≤ii. jj div 4 ^ (ii - li) < length (bits (levels (mem_pool_info s p) ! li))"
apply clarsimp
apply(subgoal_tac "length (bits (levels (mem_pool_info s p) ! li)) = (n_max (mem_pool_info s p)) * 4 ^ li")
prefer 2 using p4 p6 ii_len apply(simp add:inv_mempool_info_def Let_def)
using jj maxsz nl_eq_len jj_lt_maxdiv4ii Divides.div_mult2_eq add_diff_cancel_left' blk_ii div_eq_0_iff gr_implies_not0
le_Suc_ex less_not_refl2 mult.commute mult.left_commute mult_0 mult_is_0 p5 power_add
by (smt not_less)
ultimately have "∀li≤ii. ¬ (get_bit_s s p li (jj div 4 ^ (ii - li)) = FREE ∨
get_bit_s s p li (jj div 4 ^ (ii - li)) = FREEING ∨
get_bit_s s p li (jj div 4 ^ (ii - li)) = ALLOCATED ∨ get_bit_s s p li (jj div 4 ^ (ii - li)) = ALLOCATING)"
by auto
hence all_dv_ne: "∀li≤ii. get_bit_s s p li (jj div 4 ^ (ii - li)) = DIVIDED ∨ get_bit_s s p li (jj div 4 ^ (ii - li)) = NOEXIST"
using BlockState.exhaust by blast
moreover
have bit_lvl0: "get_bit_s s p 0 (jj div 4 ^ ii) = DIVIDED" using all_dv_ne p2 p4 apply(simp add:inv_bitmap0_def Let_def)
using li_len by fastforce
moreover
have bit_lvln: "get_bit_s s p ii jj = NOEXIST"
using all_dv_ne p4 p7 apply(simp add:inv_bitmapn_def inv_bitmap_not4free_def Let_def)
using jj_lt_len_lstbits ii lvlii_eq_last
by (metis One_nat_def diff_self_eq_0 div_by_Suc_0 eq_imp_le power_0)
ultimately have "∃n. n > 0 ∧ n ≤ ii ∧ get_bit_s s p (n-1) (jj div 4 ^ (ii - (n-1))) = DIVIDED ∧
get_bit_s s p n (jj div 4 ^ (ii - n)) = NOEXIST"
using divornoe_imp_div_noe_neigh[of ii s p jj] by fastforce
then obtain n where "n > 0 ∧ n ≤ ii ∧ get_bit_s s p (n-1) (jj div 4 ^ (ii - (n-1))) = DIVIDED ∧
get_bit_s s p n (jj div 4 ^ (ii - n)) = NOEXIST" by auto
moreover
with p3 have "get_bit_s s p (n - Suc NULL) (jj div 4 ^ (ii - (n - Suc NULL))) ≠ DIVIDED"
apply(simp add:inv_bitmap_def Let_def)
using Divides.div_mult2_eq One_nat_def Suc_diff_eq_diff_pred Suc_pred
diff_Suc_eq_diff_pred diff_commute ii less_Suc_eq_le li_len p4 power_minus_mult zero_less_diff
by (smt le_imp_less_Suc zero_le_numeral)
ultimately have False by simp
} thus ?thesis by auto
qed
thus ?thesis by auto
qed
lemma div_imp_up_alldiv:
"∀i1 j1 j2. inv_bitmap s ∧ inv_bitmap0 s ∧
inv_mempool_info s ∧
p ∈ mem_pools s ∧
i1 < length (levels (mem_pool_info s p)) ∧
j1 < length (bits (levels (mem_pool_info s p) ! i1)) ∧
i2 < length (levels (mem_pool_info s p)) ∧
j2 < length (bits (levels (mem_pool_info s p) ! i2)) ∧
get_bit_s s p i2 j2 = DIVIDED ∧
i1 < i2 ∧
j1 = j2 div 4 ^ (i2 - i1) ⟶
get_bit_s s p i1 j1 = DIVIDED"
apply(induct i2)
apply simp
apply clarsimp
apply(case_tac "i1 = i2")
apply clarsimp apply(simp add:inv_bitmap_def Let_def)
apply fastforce
apply(subgoal_tac "i1 < i2") prefer 2 apply simp
apply(subgoal_tac "get_bit_s s p i2 (j2 div 4) = DIVIDED") prefer 2
apply(simp add:inv_bitmap_def Let_def) apply fastforce
apply(subgoal_tac "get_bit_s s p i1 ((j2 div 4) div 4 ^ (i2 - i1)) = DIVIDED") prefer 2
apply(subgoal_tac "(j2 div 4) div 4 ^ (i2 - i1) < length (bits (levels (mem_pool_info s p) ! i1))")
prefer 2 apply (simp add: Divides.div_mult2_eq Suc_diff_le)
apply(subgoal_tac "j2 div 4 < length (bits (levels (mem_pool_info s p) ! i2))")
prefer 2 apply(simp add:inv_mempool_info_def Let_def)
apply fastforce
apply(subgoal_tac "j2 div 4 div 4 ^ (i2 - i1) = j2 div 4 ^ (Suc i2 - i1)")
prefer 2
apply (metis Suc_diff_le div_mult2_eq less_or_eq_imp_le power_Suc)
apply fastforce
done
lemma block_imp_up_alldiv:
"inv_bitmap s ⟹ inv_bitmap0 s ⟹
inv_mempool_info s ⟹
p ∈ mem_pools s ⟹
i1 < length (levels (mem_pool_info s p)) ⟹
j1 < length (bits (levels (mem_pool_info s p) ! i1)) ⟹
i2 < length (levels (mem_pool_info s p)) ⟹
j2 < length (bits (levels (mem_pool_info s p) ! i2)) ⟹
(get_bit_s s p i2 j2 = FREE ∨
get_bit_s s p i2 j2 = FREEING ∨ get_bit_s s p i2 j2 = ALLOCATED ∨ get_bit_s s p i2 j2 = ALLOCATING) ⟹
i1 < i2 ⟹
j1 = j2 div 4 ^ (i2 - i1) ⟹
get_bit_s s p i1 j1 = DIVIDED"
apply(subgoal_tac "get_bit_s s p (i2 - 1) (j2 div 4) = DIVIDED")
prefer 2 apply(simp add:inv_bitmap_def Let_def)
apply (metis neq0_conv not_less_zero)
apply(case_tac "i1 = i2 - 1")
apply simp
apply clarsimp
apply(rule div_imp_up_alldiv[rule_format,of s p i1 "j2 div 4 ^ (i2 - i1)" "i2 - 1" "j2 div 4"])
apply clarsimp
apply(rule conjI) apply simp
apply(rule conjI) apply(simp add:inv_mempool_info_def Let_def)
using One_nat_def div_eq_0_iff gr_implies_not0 nat_0_less_mult_iff
apply (metis (no_types, lifting) less_mult_imp_div_less nat_neq_iff power_minus_mult semiring_normalization_rules(17))
using Divides.div_mult2_eq Suc_diff_Suc Suc_pred linorder_neqE_nat not_less_eq not_less_zero power_Suc
by (metis not_less)
lemma addr_in_same_block:
"inv_bitmap0 s ⟹ inv_bitmap s ⟹ inv_mempool_info s ⟹
p ∈ mem_pools s ⟹ addr < n_max (mem_pool_info s p) * max_sz (mem_pool_info s p) ⟹
addr_in_block (mem_pool_info s p) addr i1 j1 ⟹
addr_in_block (mem_pool_info s p) addr i2 j2 ⟹
i1 = i2 ∧ j1 = j2"
apply(case_tac "i1 = i2")
apply(rule conjI) apply fast
apply clarsimp
apply(case_tac "j1 < j2")
apply (smt Groups.mult_ac(2) mult_Suc_right nat_0_less_mult_iff neq0_conv not_le split_div_lemma)
apply(case_tac "j1 > j2")
apply (smt Groups.mult_ac(2) mult_Suc_right nat_0_less_mult_iff neq0_conv not_le split_div_lemma)
apply simp
apply(subgoal_tac "∃n>0. max_sz (mem_pool_info s p) = (4 * n) * (4 ^ n_levels (mem_pool_info s p))")
prefer 2 apply(simp add:inv_mempool_info_def Let_def) apply metis
apply(subgoal_tac "length (levels (mem_pool_info s p)) = n_levels (mem_pool_info s p)")
prefer 2 apply(simp add:inv_mempool_info_def Let_def)
apply(case_tac "i1 < i2")
apply(subgoal_tac "addr div (max_sz (mem_pool_info s p) div 4 ^ i1) = j1")
prefer 2 using addr_in_div[of addr j1 "max_sz (mem_pool_info s p) div 4 ^ i1"] apply simp
apply(subgoal_tac "addr div (max_sz (mem_pool_info s p) div 4 ^ i2) = j2")
prefer 2 using addr_in_div[of addr j2 "max_sz (mem_pool_info s p) div 4 ^ i2"] apply simp
apply(subgoal_tac "j1 = j2 div (4 ^ (i2 - i1))") prefer 2
apply(rule subst[where s="addr div (max_sz (mem_pool_info s p) div 4 ^ i2) div 4 ^ (i2 - i1)" and t="j2 div 4 ^ (i2 - i1)"])
apply fast
apply(rule subst[where s="addr div ((max_sz (mem_pool_info s p) div 4 ^ i2) * 4 ^ (i2 - i1))"
and t="addr div (max_sz (mem_pool_info s p) div 4 ^ i2) div 4 ^ (i2 - i1)"])
using div2_eq_divmul[of addr "max_sz (mem_pool_info s p) div 4 ^ i2" "4 ^ (i2 - i1)"] apply simp
apply(rule subst[where s="max_sz (mem_pool_info s p) div 4 ^ i1" and
t="max_sz (mem_pool_info s p) div 4 ^ i2 * 4 ^ (i2 - i1)"])
apply(subgoal_tac "max_sz (mem_pool_info s p) mod (4 ^ i1) = 0")
prefer 2 apply (metis ge_pow_mod_0)
apply(subgoal_tac "max_sz (mem_pool_info s p) mod (4 ^ i2) = 0")
prefer 2 apply (metis ge_pow_mod_0)
apply(smt add_diff_inverse_nat div2_eq_minus less_imp_le_nat m_mod_div minus_div_mult_eq_mod
minus_mult_div_eq_mod mod_div_self mod_mult_self2_is_0 not_less power_add zero_neq_numeral)
apply fast
apply(subgoal_tac "get_bit_s s p i1 j1 = DIVIDED")
prefer 2 using block_imp_up_alldiv[of s p i1 j1 i2 j2] apply fast
apply auto[1]
apply(case_tac "i1 > i2")
apply(subgoal_tac "addr div (max_sz (mem_pool_info s p) div 4 ^ i1) = j1")
prefer 2 using addr_in_div[of addr j1 "max_sz (mem_pool_info s p) div 4 ^ i1"] apply simp
apply(subgoal_tac "addr div (max_sz (mem_pool_info s p) div 4 ^ i2) = j2")
prefer 2 using addr_in_div[of addr j2 "max_sz (mem_pool_info s p) div 4 ^ i2"] apply simp
apply(subgoal_tac "j2 = j1 div (4 ^ (i1 - i2))") prefer 2
apply(rule subst[where s="addr div (max_sz (mem_pool_info s p) div 4 ^ i1) div 4 ^ (i1 - i2)" and t="j1 div 4 ^ (i1 - i2)"])
apply fast
apply(rule subst[where s="addr div ((max_sz (mem_pool_info s p) div 4 ^ i1) * 4 ^ (i1 - i2))"
and t="addr div (max_sz (mem_pool_info s p) div 4 ^ i1) div 4 ^ (i1 - i2)"])
using div2_eq_divmul[of addr "max_sz (mem_pool_info s p) div 4 ^ i1" "4 ^ (i1 - i2)"] apply simp
apply(rule subst[where s="max_sz (mem_pool_info s p) div 4 ^ i2" and
t="max_sz (mem_pool_info s p) div 4 ^ i1 * 4 ^ (i1 - i2)"])
apply(subgoal_tac "max_sz (mem_pool_info s p) mod (4 ^ i1) = 0")
prefer 2 apply (metis ge_pow_mod_0)
apply(subgoal_tac "max_sz (mem_pool_info s p) mod (4 ^ i2) = 0")
prefer 2 apply (metis ge_pow_mod_0)
apply(smt add_diff_inverse_nat div2_eq_minus less_imp_le_nat m_mod_div minus_div_mult_eq_mod
minus_mult_div_eq_mod mod_div_self mod_mult_self2_is_0 not_less power_add zero_neq_numeral)
apply fast
apply(subgoal_tac "get_bit_s s p i2 j2 = DIVIDED")
prefer 2 using block_imp_up_alldiv[of s p i2 j2 i1 j1] apply fast
apply auto[1]
apply auto
done
lemma inv_impl_mem_cover':
"inv_mempool_info s ⟹
inv_bitmap0 s ⟹ inv_bitmap s ⟹ inv_bitmapn s ⟹ mem_cover s"
apply(simp add: mem_cover_def Let_def)
apply clarify
apply(rule ex_ex1I)
apply clarsimp using addr_exist_block[of s] apply fastforce
apply clarsimp using addr_in_same_block[of s] apply force
done
lemma inv_impl_mem_cover: "inv s ⟹ mem_cover s"
apply(simp add:inv_def)
using inv_impl_mem_cover' apply fast
done
abbreviation divide_noexist_cont' :: "State ⇒ mempool_ref ⇒ bool"
where "divide_noexist_cont' s p ≡
let mp = mem_pool_info s p in
∀i < length (levels mp).
let bts = bits (levels mp ! i) in
(∀j < length bts. (bts ! j = DIVIDED ⟶ i > 0 ⟶ (bits (levels mp ! (i - 1))) ! (j div 4) = DIVIDED)
∧ (bts ! j = NOEXIST ⟶ i < length (levels mp) - 1 ⟶ noexist_bits mp (i+1) (j*4)) )"
definition divide_noexist_cont :: "State ⇒ bool"
where "divide_noexist_cont s ≡
∀p∈mem_pools s. divide_noexist_cont' s p"
end