theory CSpace1_R

lemma cte_map_shift:
  assumes bl: "to_bl cref' = zs @ cref"
  assumes pre: "guard \<le> cref"
  assumes len: "cbits + length guard \<le> length cref"
  assumes aligned: "is_aligned ptr (cte_level_bits + cbits)"
  assumes cbits: "cbits \<le> word_bits - cte_level_bits"
  shows
  "ptr + 2^cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) =
   cte_map (ptr, take cbits (drop (length guard) cref))" proof - let ?l = "length cref - (cbits + length guard)" from pre obtain xs where
    xs: "cref = guard @ xs" by (auto simp: prefix_def less_eq_list_def) hence len_c: "length cref = length guard + length xs" by simp with len have len_x: "cbits \<le> length xs" by simp from bl xs have cref': "to_bl cref' = zs @ guard @ xs" by simp hence "length (to_bl cref') = length \<dots>" by simp hence 32: "32 = length zs + length guard + length xs" by simp have len_conv [simp]: "size ptr = word_bits" by (simp add: word_size word_bits_def) have "to_bl ((cref' >> ?l) && mask cbits) = (replicate (32 - cbits) False) @
        drop (32 - cbits) (to_bl (cref' >> ?l))" by (simp add: bl_shiftl word_size bl_and_mask
                  cte_level_bits_def word_bits_def) also from len_c len_x cref' 32 have "\<dots> = (replicate (32 - cbits) False) @ take cbits xs" by (simp add: bl_shiftr word_size add.commute add.left_commute) also from len_x len_c 32 have "\<dots> = to_bl (of_bl (take cbits (drop (length guard) cref)) :: word32)" by (simp add: xs word_rev_tf takefill_alt rev_take rev_drop) finally show ?thesis by (simp add: cte_map_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (state)
goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (state)
goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (chain)
picking this:
guard \<le> cref proof (prove)
using this:
guard \<le> cref

goal (1 subgoal):
 1. (\<And>xs. cref = guard @ xs \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
cref = guard @ xs

goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (prove)
using this:
cref = guard @ xs

goal (1 subgoal):
 1. length cref = length guard + length xs proof (state)
this:
length cref = length guard + length xs

goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (chain)
picking this:
cbits + length guard \<le> length cref
length cref = length guard + length xs proof (prove)
using this:
cbits + length guard \<le> length cref
length cref = length guard + length xs

goal (1 subgoal):
 1. cbits \<le> length xs proof (state)
this:
cbits \<le> length xs

goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (chain)
picking this:
to_bl cref' = zs @ cref
cref = guard @ xs proof (prove)
using this:
to_bl cref' = zs @ cref
cref = guard @ xs

goal (1 subgoal):
 1. to_bl cref' = zs @ guard @ xs proof (state)
this:
to_bl cref' = zs @ guard @ xs

goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (prove)
using this:
to_bl cref' = zs @ guard @ xs

goal (1 subgoal):
 1. length (to_bl cref') = length (zs @ guard @ xs) proof (state)
this:
length (to_bl cref') = length (zs @ guard @ xs)

goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (prove)
using this:
length (to_bl cref') = length (zs @ guard @ xs)

goal (1 subgoal):
 1. 32 = length zs + length guard + length xs proof (state)
this:
32 = length zs + length guard + length xs

goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (prove)
goal (1 subgoal):
 1. size ptr = word_bits proof (state)
this:
size ptr = word_bits

goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (prove)
goal (1 subgoal):
 1. to_bl ((cref' >> length cref - (cbits + length guard)) && mask cbits) = replicate (32 - cbits) False @ drop (32 - cbits) (to_bl (cref' >> length cref - (cbits + length guard))) proof (state)
this:
to_bl ((cref' >> length cref - (cbits + length guard)) && mask cbits) = replicate (32 - cbits) False @ drop (32 - cbits) (to_bl (cref' >> length cref - (cbits + length guard)))

goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (state)
this:
to_bl ((cref' >> length cref - (cbits + length guard)) && mask cbits) = replicate (32 - cbits) False @ drop (32 - cbits) (to_bl (cref' >> length cref - (cbits + length guard)))

goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (chain)
picking this:
length cref = length guard + length xs
cbits \<le> length xs
to_bl cref' = zs @ guard @ xs
32 = length zs + length guard + length xs proof (prove)
using this:
length cref = length guard + length xs
cbits \<le> length xs
to_bl cref' = zs @ guard @ xs
32 = length zs + length guard + length xs

goal (1 subgoal):
 1. replicate (32 - cbits) False @ drop (32 - cbits) (to_bl (cref' >> length cref - (cbits + length guard))) = replicate (32 - cbits) False @ take cbits xs proof (state)
this:
replicate (32 - cbits) False @ drop (32 - cbits) (to_bl (cref' >> length cref - (cbits + length guard))) = replicate (32 - cbits) False @ take cbits xs

goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (state)
this:
replicate (32 - cbits) False @ drop (32 - cbits) (to_bl (cref' >> length cref - (cbits + length guard))) = replicate (32 - cbits) False @ take cbits xs

goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (chain)
picking this:
cbits \<le> length xs
length cref = length guard + length xs
32 = length zs + length guard + length xs proof (prove)
using this:
cbits \<le> length xs
length cref = length guard + length xs
32 = length zs + length guard + length xs

goal (1 subgoal):
 1. replicate (32 - cbits) False @ take cbits xs = to_bl (of_bl (take cbits (drop (length guard) cref))) proof (state)
this:
replicate (32 - cbits) False @ take cbits xs = to_bl (of_bl (take cbits (drop (length guard) cref)))

goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (chain)
picking this:
to_bl ((cref' >> length cref - (cbits + length guard)) && mask cbits) = to_bl (of_bl (take cbits (drop (length guard) cref))) proof (prove)
using this:
to_bl ((cref' >> length cref - (cbits + length guard)) && mask cbits) = to_bl (of_bl (take cbits (drop (length guard) cref)))

goal (1 subgoal):
 1. ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) proof (state)
this:
ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))

goal:
No subgoals!