theory Untyped_DR

lemma get_ipc_buffer_words_def2:
  "get_ipc_buffer_words ms tcb ns \<equiv>
   (case tcb_ipcframe tcb of
      cap.ArchObjectCap (arch_cap.PageCap dev buf rights sz mapdata) \<Rightarrow>
        if AllowRead \<in> rights then
          (if ns = Nil \<or> is_aligned (buf + tcb_ipc_buffer tcb) 2 then
            map ((\<lambda>x. word_rcat [underlying_memory ms (x + 3),
                                 underlying_memory ms (x + 2),
                                 underlying_memory ms (x + 1),
                                 underlying_memory ms x]) \<circ>
                 (\<lambda>n. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) +
                      of_nat n * of_nat word_size))
              ns
          else the None)
        else []
    | _ \<Rightarrow> [])" proof - 

  (* FIXME: extract *)
   have mask_eq:
    "\<And>p q m n. m\<ge>n \<Longrightarrow> p + (q && mask m) && mask n = p + q && mask n" by (subst mask_eqs(2)[of p "q && mask m" for p q m, symmetric])
       (simp add: mask_twice min_def mask_eqs) have eq: "\<And>x p b sz. is_aligned (p + (b && mask (pageBitsForSize sz)) +
                                    of_nat x * of_nat word_size) 2
                \<longleftrightarrow> is_aligned (p + b) 2" apply (rule iffI) apply (drule is_aligned_addD2) apply (simp add: word_size_def is_aligned_mult_triv2[where n=2,
                                      simplified word_bits_def, simplified]) apply (simp add: is_aligned_mask mask_eq) apply (rule is_aligned_add) apply (simp add: is_aligned_mask mask_eq) apply (simp add: word_size_def is_aligned_mult_triv2[where n=2,
                                     simplified word_bits_def, simplified]) done show "PROP ?thesis" apply (rule eq_reflection) apply (auto simp: get_ipc_buffer_words_def evalMonad_loadWords eq
               split: cap.splits arch_cap.splits) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_ipc_buffer_words ms tcb ns \<equiv> case tcb_ipcframe tcb of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then if ns = [] \<or> is_aligned (buf + tcb_ipc_buffer tcb) 2 then map ((\<lambda>x. word_rcat [underlying_memory ms (x + 3), underlying_memory ms (x + 2), underlying_memory ms (x + 1), underlying_memory ms x]) \<circ> (\<lambda>n. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) ns else the None else [] | ArchObjectCap _ \<Rightarrow> [] | _ \<Rightarrow> [] proof (state)
goal (1 subgoal):
 1. get_ipc_buffer_words ms tcb ns \<equiv> case tcb_ipcframe tcb of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then if ns = [] \<or> is_aligned (buf + tcb_ipc_buffer tcb) 2 then map ((\<lambda>x. word_rcat [underlying_memory ms (x + 3), underlying_memory ms (x + 2), underlying_memory ms (x + 1), underlying_memory ms x]) \<circ> (\<lambda>n. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) ns else the None else [] | ArchObjectCap _ \<Rightarrow> [] | _ \<Rightarrow> [] proof (state)
goal (1 subgoal):
 1. get_ipc_buffer_words ms tcb ns \<equiv> case tcb_ipcframe tcb of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then if ns = [] \<or> is_aligned (buf + tcb_ipc_buffer tcb) 2 then map ((\<lambda>x. word_rcat [underlying_memory ms (x + 3), underlying_memory ms (x + 2), underlying_memory ms (x + 1), underlying_memory ms x]) \<circ> (\<lambda>n. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) ns else the None else [] | ArchObjectCap _ \<Rightarrow> [] | _ \<Rightarrow> [] proof (prove)
goal (1 subgoal):
 1. \<And>p q m n. n \<le> m \<Longrightarrow> p + (q && mask m) && mask n = p + q && mask n proof (state)
this:
?n \<le> ?m \<Longrightarrow> ?p + (?q && mask ?m) && mask ?n = ?p + ?q && mask ?n

goal (1 subgoal):
 1. get_ipc_buffer_words ms tcb ns \<equiv> case tcb_ipcframe tcb of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then if ns = [] \<or> is_aligned (buf + tcb_ipc_buffer tcb) 2 then map ((\<lambda>x. word_rcat [underlying_memory ms (x + 3), underlying_memory ms (x + 2), underlying_memory ms (x + 1), underlying_memory ms x]) \<circ> (\<lambda>n. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) ns else the None else [] | ArchObjectCap _ \<Rightarrow> [] | _ \<Rightarrow> [] proof (prove)
goal (1 subgoal):
 1. \<And>x p b sz. is_aligned (p + (b && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size) 2 = is_aligned (p + b) 2 proof (prove)
goal (2 subgoals):
 1. \<And>x p b sz. is_aligned (p + (b && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size) 2 \<Longrightarrow> is_aligned (p + b) 2
 2. \<And>x p b sz. is_aligned (p + b) 2 \<Longrightarrow> is_aligned (p + (b && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size) 2 proof (prove)
goal (3 subgoals):
 1. \<And>x p b sz. is_aligned (word_of_nat x * word_of_nat word_size) 2
 2. \<And>x p b sz. is_aligned (p + (b && mask (pageBitsForSize sz))) 2 \<Longrightarrow> is_aligned (p + b) 2
 3. \<And>x p b sz. is_aligned (p + b) 2 \<Longrightarrow> is_aligned (p + (b && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size) 2 proof (prove)
goal (2 subgoals):
 1. \<And>x p b sz. is_aligned (p + (b && mask (pageBitsForSize sz))) 2 \<Longrightarrow> is_aligned (p + b) 2
 2. \<And>x p b sz. is_aligned (p + b) 2 \<Longrightarrow> is_aligned (p + (b && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size) 2 proof (prove)
goal (1 subgoal):
 1. \<And>x p b sz. is_aligned (p + b) 2 \<Longrightarrow> is_aligned (p + (b && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size) 2 proof (prove)
goal (2 subgoals):
 1. \<And>x p b sz. is_aligned (p + b) 2 \<Longrightarrow> is_aligned (p + (b && mask (pageBitsForSize sz))) 2
 2. \<And>x p b sz. is_aligned (p + b) 2 \<Longrightarrow> is_aligned (word_of_nat x * word_of_nat word_size) 2 proof (prove)
goal (1 subgoal):
 1. \<And>x p b sz. is_aligned (p + b) 2 \<Longrightarrow> is_aligned (word_of_nat x * word_of_nat word_size) 2 proof (prove)
goal:
No subgoals! proof (state)
this:
is_aligned (?p1 + (?b1 && mask (pageBitsForSize ?sz1)) + word_of_nat ?x1 * word_of_nat word_size) 2 = is_aligned (?p1 + ?b1) 2

goal (1 subgoal):
 1. get_ipc_buffer_words ms tcb ns \<equiv> case tcb_ipcframe tcb of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then if ns = [] \<or> is_aligned (buf + tcb_ipc_buffer tcb) 2 then map ((\<lambda>x. word_rcat [underlying_memory ms (x + 3), underlying_memory ms (x + 2), underlying_memory ms (x + 1), underlying_memory ms x]) \<circ> (\<lambda>n. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) ns else the None else [] | ArchObjectCap _ \<Rightarrow> [] | _ \<Rightarrow> [] proof (prove)
goal (1 subgoal):
 1. get_ipc_buffer_words ms tcb ns \<equiv> case tcb_ipcframe tcb of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then if ns = [] \<or> is_aligned (buf + tcb_ipc_buffer tcb) 2 then map ((\<lambda>x. word_rcat [underlying_memory ms (x + 3), underlying_memory ms (x + 2), underlying_memory ms (x + 1), underlying_memory ms x]) \<circ> (\<lambda>n. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) ns else the None else [] | ArchObjectCap _ \<Rightarrow> [] | _ \<Rightarrow> [] proof (prove)
goal (1 subgoal):
 1. get_ipc_buffer_words ms tcb ns = (case tcb_ipcframe tcb of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then if ns = [] \<or> is_aligned (buf + tcb_ipc_buffer tcb) 2 then map ((\<lambda>x. word_rcat [underlying_memory ms (x + 3), underlying_memory ms (x + 2), underlying_memory ms (x + 1), underlying_memory ms x]) \<circ> (\<lambda>n. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) ns else the None else [] | ArchObjectCap _ \<Rightarrow> [] | _ \<Rightarrow> []) proof (prove)
goal:
No subgoals! proof (state)
this:
get_ipc_buffer_words ms tcb ns \<equiv> case tcb_ipcframe tcb of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then if ns = [] \<or> is_aligned (buf + tcb_ipc_buffer tcb) 2 then map ((\<lambda>x. word_rcat [underlying_memory ms (x + 3), underlying_memory ms (x + 2), underlying_memory ms (x + 1), underlying_memory ms x]) \<circ> (\<lambda>n. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) ns else the None else [] | ArchObjectCap _ \<Rightarrow> [] | _ \<Rightarrow> []

goal:
No subgoals!