theory TcbAcc_R

lemma valid_ipc_buffer_ptr'D:
  assumes yv: "y < unat max_ipc_words"
  and    buf: "valid_ipc_buffer_ptr' a s"
  shows "pointerInUserData (a + of_nat y * 4) s" using buf unfolding valid_ipc_buffer_ptr'_def pointerInUserData_def apply clarsimp apply (subgoal_tac
         "(a + of_nat y * 4) && ~~ mask pageBits = a  && ~~ mask pageBits") apply simp apply (rule mask_out_first_mask_some [where n = msg_align_bits]) apply (erule is_aligned_add_helper [THEN conjunct2]) apply (rule word_less_power_trans_ofnat [where k = 2, simplified]) apply (rule order_less_le_trans [OF yv]) apply (simp add: msg_align_bits max_ipc_words) apply (simp add: msg_align_bits) apply (simp_all add: msg_align_bits pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pointerInUserData (a + word_of_nat y * 4) s proof (prove)
using this:
valid_ipc_buffer_ptr' a s

goal (1 subgoal):
 1. pointerInUserData (a + word_of_nat y * 4) s proof (prove)
using this:
is_aligned a msg_align_bits \<and> typ_at' UserDataT (a && ~~ mask pageBits) s

goal (1 subgoal):
 1. typ_at' UserDataT (a + word_of_nat y * 4 && ~~ mask pageBits) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> typ_at' UserDataT (a + word_of_nat y * 4 && ~~ mask pageBits) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s; a + word_of_nat y * 4 && ~~ mask pageBits = a && ~~ mask pageBits\<rbrakk> \<Longrightarrow> typ_at' UserDataT (a + word_of_nat y * 4 && ~~ mask pageBits) s
 2. \<lbrakk>is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> a + word_of_nat y * 4 && ~~ mask pageBits = a && ~~ mask pageBits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> a + word_of_nat y * 4 && ~~ mask pageBits = a && ~~ mask pageBits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> a + word_of_nat y * 4 && ~~ mask msg_align_bits = a
 2. \<lbrakk>is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBits proof (prove)
goal (2 subgoals):
 1. typ_at' UserDataT (a && ~~ mask pageBits) s \<Longrightarrow> word_of_nat y * 4 < 2 ^ msg_align_bits
 2. \<lbrakk>is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBits proof (prove)
goal (4 subgoals):
 1. typ_at' UserDataT (a && ~~ mask pageBits) s \<Longrightarrow> y < 2 ^ (msg_align_bits - 2)
 2. typ_at' UserDataT (a && ~~ mask pageBits) s \<Longrightarrow> 2 \<le> msg_align_bits
 3. typ_at' UserDataT (a && ~~ mask pageBits) s \<Longrightarrow> msg_align_bits < LENGTH(32)
 4. \<lbrakk>is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBits proof (prove)
goal (4 subgoals):
 1. typ_at' UserDataT (a && ~~ mask pageBits) s \<Longrightarrow> unat max_ipc_words \<le> 2 ^ (msg_align_bits - 2)
 2. typ_at' UserDataT (a && ~~ mask pageBits) s \<Longrightarrow> 2 \<le> msg_align_bits
 3. typ_at' UserDataT (a && ~~ mask pageBits) s \<Longrightarrow> msg_align_bits < LENGTH(32)
 4. \<lbrakk>is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBits proof (prove)
goal (3 subgoals):
 1. typ_at' UserDataT (a && ~~ mask pageBits) s \<Longrightarrow> 2 \<le> msg_align_bits
 2. typ_at' UserDataT (a && ~~ mask pageBits) s \<Longrightarrow> msg_align_bits < LENGTH(32)
 3. \<lbrakk>is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBits proof (prove)
goal (2 subgoals):
 1. typ_at' UserDataT (a && ~~ mask pageBits) s \<Longrightarrow> msg_align_bits < LENGTH(32)
 2. \<lbrakk>is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBits proof (prove)
goal:
No subgoals!