theory Untyped_DR

lemma transform_full_intent_machine_state_eq:
  assumes 3: "tcb_ipcframe tcb =
              cap.ArchObjectCap (arch_cap.PageCap dev buf rights sz opt)"
  assumes 4: "is_aligned buf (pageBitsForSize sz)"
  assumes 1: "is_aligned (tcb_ipc_buffer tcb) msg_align_bits"
  assumes 5: "(\<forall>p. buf = (p && ~~ mask (pageBitsForSize sz)) \<longrightarrow>
                   underlying_memory ms' p = underlying_memory ms p)"
  shows "transform_full_intent ms tref tcb = transform_full_intent ms' tref tcb" proof - have 2: "valid_message_info (get_tcb_message_info tcb)" by (simp add: get_tcb_message_info_def data_to_message_info_valid) let ?p = "%x. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) +
                of_nat x * of_nat word_size" have word_rcat_eq:
    "\<And>x. x<128 \<Longrightarrow>
       word_rcat [underlying_memory ms (?p x + 3),
                  underlying_memory ms (?p x + 2),
                  underlying_memory ms (?p x + 1),
                  underlying_memory ms (?p x)] =
       word_rcat [underlying_memory ms'(?p x + 3),
                  underlying_memory ms'(?p x + 2),
                  underlying_memory ms'(?p x + 1),
                  underlying_memory ms'(?p x)]" proof - fix x :: nat assume x: "x<128" have y: "!!y. y<4 \<Longrightarrow> ?p x + y && ~~ mask (pageBitsForSize sz) = buf" apply (simp add: add.assoc) apply (rule is_aligned_add_helper[OF 4, THEN conjunct2]) apply (rule_tac n=msg_align_bits in is_aligned_add_less_t2n) apply (rule is_aligned_andI1[OF 1]) apply (rule_tac n=2 in is_aligned_add_less_t2n) apply (simp add: word_size_def) apply (rule is_aligned_mult_triv2[where n=2, simplified]) apply simp apply (simp add: msg_align_bits) apply (simp add: word_size_def) apply (rule word_less_power_trans_ofnat[where k=2, simplified],
               simp_all add: x msg_align_bits word_bits_def)[1] apply (case_tac sz, simp_all add: msg_align_bits)[1] apply (rule and_mask_less_size) apply (case_tac sz, simp_all add: word_size)[1] done note 6 = 5[rule_format, OF y[symmetric]] show "?thesis x" apply (rule arg_cong[where f=word_rcat]) using 6[of 3] 6[of 2] 6[of 1] 6[of 0] by simp qed show ?thesis apply (clarsimp simp: transform_full_intent_def Let_def get_tcb_mrs_def
                        get_ipc_buffer_words_def2 3
                        Suc_leI[OF msg_registers_lt_msg_max_length]
                  simp del: upt_Suc
                  split del: if_split) apply (case_tac "AllowRead \<in> rights",
         simp_all del: upt_Suc  split del: if_split) apply (cut_tac y=2 in is_aligned_weaken[OF 1]) apply (simp add: msg_align_bits) apply (cut_tac y=2 in is_aligned_weaken[OF 4]) apply (case_tac sz, simp_all)[1] apply (frule (1) is_aligned_add[of buf 2 "tcb_ipc_buffer tcb"]) apply (simp add: o_def del: upt_Suc) apply (intro conjI) apply (rule arg_cong2[where f=transform_intent, OF refl]) apply (rule arg_cong2[where f="(@)", OF refl]) apply (rule arg_cong2[where f=take, OF refl]) apply (rule map_cong[OF refl]) apply (rule word_rcat_eq) apply (clarsimp simp: atLeastAtMost_upt[symmetric] msg_max_length_def
                    simp del: upt_Suc) apply clarsimp apply (rule word_rcat_eq) using 2 apply (clarsimp simp: buffer_cptr_index_def msg_max_length_def
              valid_message_info_def msg_max_extra_caps_def word_le_nat_alt) apply (rule arg_cong2[where f="case_list None", OF refl]) apply (rule map_cong[OF refl]) apply (rule word_rcat_eq) apply (clarsimp simp: atLeastAtMost_upt[symmetric]  simp del: upt_Suc) apply (simp add: msg_max_length_def msg_max_extra_caps_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_full_intent ms tref tcb = transform_full_intent ms' tref tcb proof (state)
goal (1 subgoal):
 1. transform_full_intent ms tref tcb = transform_full_intent ms' tref tcb proof (prove)
goal (1 subgoal):
 1. valid_message_info (get_tcb_message_info tcb) proof (state)
this:
valid_message_info (get_tcb_message_info tcb)

goal (1 subgoal):
 1. transform_full_intent ms tref tcb = transform_full_intent ms' tref tcb proof (state)
goal (1 subgoal):
 1. transform_full_intent ms tref tcb = transform_full_intent ms' tref tcb proof (prove)
goal (1 subgoal):
 1. \<And>x. x < 128 \<Longrightarrow> word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] proof (state)
goal (1 subgoal):
 1. \<And>x. x < 128 \<Longrightarrow> word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] proof (state)
goal (1 subgoal):
 1. \<And>x. x < 128 \<Longrightarrow> word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] proof (state)
this:
x < 128

goal (1 subgoal):
 1. \<And>x. x < 128 \<Longrightarrow> word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] proof (prove)
goal (1 subgoal):
 1. \<And>y. y < 4 \<Longrightarrow> buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + y && ~~ mask (pageBitsForSize sz) = buf proof (prove)
goal (1 subgoal):
 1. \<And>y. y < 4 \<Longrightarrow> buf + ((tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + (word_of_nat x * word_of_nat word_size + y)) && ~~ mask (pageBitsForSize sz) = buf proof (prove)
goal (1 subgoal):
 1. \<And>y. y < 4 \<Longrightarrow> (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + (word_of_nat x * word_of_nat word_size + y) < 2 ^ pageBitsForSize sz proof (prove)
goal (4 subgoals):
 1. \<And>y. y < 4 \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) msg_align_bits
 2. \<And>y. y < 4 \<Longrightarrow> word_of_nat x * word_of_nat word_size + y < 2 ^ msg_align_bits
 3. \<And>y. y < 4 \<Longrightarrow> msg_align_bits \<le> pageBitsForSize sz
 4. \<And>y. y < 4 \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize sz) < 2 ^ pageBitsForSize sz proof (prove)
goal (3 subgoals):
 1. \<And>y. y < 4 \<Longrightarrow> word_of_nat x * word_of_nat word_size + y < 2 ^ msg_align_bits
 2. \<And>y. y < 4 \<Longrightarrow> msg_align_bits \<le> pageBitsForSize sz
 3. \<And>y. y < 4 \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize sz) < 2 ^ pageBitsForSize sz proof (prove)
goal (6 subgoals):
 1. \<And>y. y < 4 \<Longrightarrow> is_aligned (word_of_nat x * word_of_nat word_size) 2
 2. \<And>y. y < 4 \<Longrightarrow> y < 2\<^sup>2
 3. \<And>y. y < 4 \<Longrightarrow> 2 \<le> msg_align_bits
 4. \<And>y. y < 4 \<Longrightarrow> word_of_nat x * word_of_nat word_size < 2 ^ msg_align_bits
 5. \<And>y. y < 4 \<Longrightarrow> msg_align_bits \<le> pageBitsForSize sz
 6. \<And>y. y < 4 \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize sz) < 2 ^ pageBitsForSize sz proof (prove)
goal (6 subgoals):
 1. \<And>y. y < 4 \<Longrightarrow> is_aligned (word_of_nat x * 4) 2
 2. \<And>y. y < 4 \<Longrightarrow> y < 2\<^sup>2
 3. \<And>y. y < 4 \<Longrightarrow> 2 \<le> msg_align_bits
 4. \<And>y. y < 4 \<Longrightarrow> word_of_nat x * word_of_nat word_size < 2 ^ msg_align_bits
 5. \<And>y. y < 4 \<Longrightarrow> msg_align_bits \<le> pageBitsForSize sz
 6. \<And>y. y < 4 \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize sz) < 2 ^ pageBitsForSize sz proof (prove)
goal (5 subgoals):
 1. \<And>y. y < 4 \<Longrightarrow> y < 2\<^sup>2
 2. \<And>y. y < 4 \<Longrightarrow> 2 \<le> msg_align_bits
 3. \<And>y. y < 4 \<Longrightarrow> word_of_nat x * word_of_nat word_size < 2 ^ msg_align_bits
 4. \<And>y. y < 4 \<Longrightarrow> msg_align_bits \<le> pageBitsForSize sz
 5. \<And>y. y < 4 \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize sz) < 2 ^ pageBitsForSize sz proof (prove)
goal (4 subgoals):
 1. \<And>y. y < 4 \<Longrightarrow> 2 \<le> msg_align_bits
 2. \<And>y. y < 4 \<Longrightarrow> word_of_nat x * word_of_nat word_size < 2 ^ msg_align_bits
 3. \<And>y. y < 4 \<Longrightarrow> msg_align_bits \<le> pageBitsForSize sz
 4. \<And>y. y < 4 \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize sz) < 2 ^ pageBitsForSize sz proof (prove)
goal (3 subgoals):
 1. \<And>y. y < 4 \<Longrightarrow> word_of_nat x * word_of_nat word_size < 2 ^ msg_align_bits
 2. \<And>y. y < 4 \<Longrightarrow> msg_align_bits \<le> pageBitsForSize sz
 3. \<And>y. y < 4 \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize sz) < 2 ^ pageBitsForSize sz proof (prove)
goal (3 subgoals):
 1. \<And>y. y < 4 \<Longrightarrow> word_of_nat x * 4 < 2 ^ msg_align_bits
 2. \<And>y. y < 4 \<Longrightarrow> msg_align_bits \<le> pageBitsForSize sz
 3. \<And>y. y < 4 \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize sz) < 2 ^ pageBitsForSize sz proof (prove)
goal (2 subgoals):
 1. \<And>y. y < 4 \<Longrightarrow> msg_align_bits \<le> pageBitsForSize sz
 2. \<And>y. y < 4 \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize sz) < 2 ^ pageBitsForSize sz proof (prove)
goal (1 subgoal):
 1. \<And>y. y < 4 \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize sz) < 2 ^ pageBitsForSize sz proof (prove)
goal (1 subgoal):
 1. \<And>y. y < 4 \<Longrightarrow> pageBitsForSize sz < size (tcb_ipc_buffer tcb) proof (prove)
goal:
No subgoals! proof (state)
this:
?y < 4 \<Longrightarrow> buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + ?y && ~~ mask (pageBitsForSize sz) = buf

goal (1 subgoal):
 1. \<And>x. x < 128 \<Longrightarrow> word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] proof (state)
this:
?y1 < 4 \<Longrightarrow> underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + ?y1) = underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + ?y1)

goal (1 subgoal):
 1. \<And>x. x < 128 \<Longrightarrow> word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] proof (prove)
goal (1 subgoal):
 1. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] proof (prove)
goal (1 subgoal):
 1. [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] proof (prove)
using this:
3 < 4 \<Longrightarrow> underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3) = underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3)
2 < 4 \<Longrightarrow> underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2) = underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2)
1 < 4 \<Longrightarrow> underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1) = underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1)
0 < 4 \<Longrightarrow> underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 0) = underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 0)

goal (1 subgoal):
 1. [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] proof (state)
this:
word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]

goal:
No subgoals! proof (state)
this:
?x < 128 \<Longrightarrow> word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat ?x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat ?x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat ?x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat ?x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat ?x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat ?x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat ?x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat ?x * word_of_nat word_size)]

goal (1 subgoal):
 1. transform_full_intent ms tref tcb = transform_full_intent ms' tref tcb proof (prove)
goal (1 subgoal):
 1. transform_full_intent ms tref tcb = transform_full_intent ms' tref tcb proof (prove)
goal (1 subgoal):
 1. transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (if AllowRead \<in> rights then if [Suc (length msg_registers)..<Suc msg_max_length] = [] \<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)) [Suc (length msg_registers)..<Suc msg_max_length] else the None else [])) = transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (if AllowRead \<in> rights then if [Suc (length msg_registers)..<Suc msg_max_length] = [] \<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)) [Suc (length msg_registers)..<Suc msg_max_length] else the None else [])) \<and> (if AllowRead \<in> rights then if [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] = [] \<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)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] else the None else []) = (if AllowRead \<in> rights then if [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] = [] \<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)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] else the None else []) \<and> (case if AllowRead \<in> rights then if [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] = [] \<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)) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] else the None else [] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case if AllowRead \<in> rights then if [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] = [] \<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)) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] else the None else [] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. AllowRead \<in> rights \<Longrightarrow> transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (if msg_max_length \<le> length msg_registers \<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)) [Suc (length msg_registers)..<Suc msg_max_length] else the None)) = transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (if msg_max_length \<le> length msg_registers \<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)) [Suc (length msg_registers)..<Suc msg_max_length] else the None)) \<and> (if buffer_cptr_index = 0 \<and> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<or> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<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)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] else the None) = (if buffer_cptr_index = 0 \<and> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<or> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<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)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] else the None) \<and> (case if 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)) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] else the None of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case if 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)) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] else the None of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (2 subgoals):
 1. AllowRead \<in> rights \<Longrightarrow> 2 \<le> msg_align_bits
 2. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (if msg_max_length \<le> length msg_registers \<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)) [Suc (length msg_registers)..<Suc msg_max_length] else the None)) = transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (if msg_max_length \<le> length msg_registers \<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)) [Suc (length msg_registers)..<Suc msg_max_length] else the None)) \<and> (if buffer_cptr_index = 0 \<and> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<or> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<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)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] else the None) = (if buffer_cptr_index = 0 \<and> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<or> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<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)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] else the None) \<and> (case if 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)) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] else the None of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case if 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)) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] else the None of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (if msg_max_length \<le> length msg_registers \<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)) [Suc (length msg_registers)..<Suc msg_max_length] else the None)) = transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (if msg_max_length \<le> length msg_registers \<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)) [Suc (length msg_registers)..<Suc msg_max_length] else the None)) \<and> (if buffer_cptr_index = 0 \<and> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<or> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<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)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] else the None) = (if buffer_cptr_index = 0 \<and> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<or> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<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)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] else the None) \<and> (case if 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)) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] else the None of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case if 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)) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] else the None of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> 2 \<le> pageBitsForSize sz
 2. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2\<rbrakk> \<Longrightarrow> transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (if msg_max_length \<le> length msg_registers \<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)) [Suc (length msg_registers)..<Suc msg_max_length] else the None)) = transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (if msg_max_length \<le> length msg_registers \<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)) [Suc (length msg_registers)..<Suc msg_max_length] else the None)) \<and> (if buffer_cptr_index = 0 \<and> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<or> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<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)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] else the None) = (if buffer_cptr_index = 0 \<and> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<or> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<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)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] else the None) \<and> (case if 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)) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] else the None of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case if 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)) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] else the None of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2\<rbrakk> \<Longrightarrow> transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (if msg_max_length \<le> length msg_registers \<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)) [Suc (length msg_registers)..<Suc msg_max_length] else the None)) = transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (if msg_max_length \<le> length msg_registers \<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)) [Suc (length msg_registers)..<Suc msg_max_length] else the None)) \<and> (if buffer_cptr_index = 0 \<and> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<or> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<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)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] else the None) = (if buffer_cptr_index = 0 \<and> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<or> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<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)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] else the None) \<and> (case if 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)) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] else the None of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case if 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)) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] else the None of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (if msg_max_length \<le> length msg_registers \<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)) [Suc (length msg_registers)..<Suc msg_max_length] else the None)) = transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (if msg_max_length \<le> length msg_registers \<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)) [Suc (length msg_registers)..<Suc msg_max_length] else the None)) \<and> (if buffer_cptr_index = 0 \<and> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<or> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<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)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] else the None) = (if buffer_cptr_index = 0 \<and> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<or> unat (mi_extra_caps (get_tcb_message_info tcb)) = 0 \<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)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] else the None) \<and> (case if 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)) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] else the None of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case if 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)) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<Suc (Suc (msg_max_length + msg_max_extra_caps)) + 3] else the None of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (length msg_registers)..<Suc msg_max_length])) = transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (length msg_registers)..<Suc msg_max_length])) \<and> (\<forall>x\<in>{buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))}. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) \<and> (case map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (length msg_registers)..<Suc msg_max_length])) = transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (length msg_registers)..<Suc msg_max_length]))
 2. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> \<forall>x\<in>{buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))}. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]
 3. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> (case map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (length msg_registers)..<Suc msg_max_length]) = take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (length msg_registers)..<Suc msg_max_length])
 2. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> \<forall>x\<in>{buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))}. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]
 3. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> (case map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (length msg_registers)..<Suc msg_max_length]) = take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (length msg_registers)..<Suc msg_max_length])
 2. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> \<forall>x\<in>{buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))}. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]
 3. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> (case map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (length msg_registers)..<Suc msg_max_length] = map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (length msg_registers)..<Suc msg_max_length]
 2. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> \<forall>x\<in>{buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))}. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]
 3. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> (case map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2; x \<in> set [Suc (length msg_registers)..<Suc msg_max_length]\<rbrakk> \<Longrightarrow> word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]
 2. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> \<forall>x\<in>{buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))}. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]
 3. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> (case map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2; x \<in> set [Suc (length msg_registers)..<Suc msg_max_length]\<rbrakk> \<Longrightarrow> x < 128
 2. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> \<forall>x\<in>{buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))}. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]
 3. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> (case map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> \<forall>x\<in>{buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))}. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]
 2. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> (case map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2; buffer_cptr_index \<le> x; x < buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))\<rbrakk> \<Longrightarrow> word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]
 2. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> (case map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2; buffer_cptr_index \<le> x; x < buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))\<rbrakk> \<Longrightarrow> x < 128
 2. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> (case map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
using this:
valid_message_info (get_tcb_message_info tcb)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2; buffer_cptr_index \<le> x; x < buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))\<rbrakk> \<Longrightarrow> x < 128
 2. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> (case map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> (case map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) = (case map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2\<rbrakk> \<Longrightarrow> map (\<lambda>x. word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] = map (\<lambda>x. word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)]) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2; x \<in> set [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)]\<rbrakk> \<Longrightarrow> word_rcat [underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] = word_rcat [underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 3), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 2), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size + 1), underlying_memory ms' (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size)] proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2; x \<in> set [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)]\<rbrakk> \<Longrightarrow> x < 128 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>AllowRead \<in> rights; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; is_aligned (buf + tcb_ipc_buffer tcb) 2; Suc (Suc (msg_max_length + msg_max_extra_caps)) \<le> x; x < 5 + (msg_max_length + msg_max_extra_caps)\<rbrakk> \<Longrightarrow> x < 128 proof (prove)
goal:
No subgoals! proof (state)
this:
transform_full_intent ms tref tcb = transform_full_intent ms' tref tcb

goal:
No subgoals!