theory Ipc_DR

lemma load_cap_transfer_def':
  "load_cap_transfer (buf) = (do
    xs \<leftarrow> mapM (load_word_offs buf) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)];
    return \<lparr>ct_receive_root = data_to_cptr (head xs), ct_receive_index = data_to_cptr ((head \<circ> tail) xs), ct_receive_depth = ((head\<circ> tail\<circ> tail) xs)\<rparr>
    od)" apply (clarsimp simp:load_cap_transfer_def ) apply (clarsimp simp:captransfer_from_words_def) apply (simp add:msg_max_length_def msg_max_extra_caps_def cong: if_weak_cong) apply (clarsimp simp:load_word_offs_def mapM_def sequence_def bind_assoc) apply (simp add:word_size_def add.commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. load_cap_transfer buf = do xs <- mapM (load_word_offs buf) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)];
return \<lparr>ct_receive_root = data_to_cptr (head xs), ct_receive_index = data_to_cptr ((head \<circ> tail) xs), ct_receive_depth = (head \<circ> tail \<circ> tail) xs\<rparr>
od proof (prove)
goal (1 subgoal):
 1. captransfer_from_words (buf + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size) = do xs <- mapM (load_word_offs buf) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)];
return \<lparr>ct_receive_root = to_bl (hd xs), ct_receive_index = to_bl (hd (tl xs)), ct_receive_depth = hd (tl (tl xs))\<rparr>
od proof (prove)
goal (1 subgoal):
 1. do w0 <- do_machine_op (loadWord (buf + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size));
w1 <- do_machine_op (loadWord (buf + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + word_size));
w2 <- do_machine_op (loadWord (buf + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + 2 * word_size));
return \<lparr>ct_receive_root = to_bl w0, ct_receive_index = to_bl w1, ct_receive_depth = w2\<rparr>
od = do xs <- mapM (load_word_offs buf) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)];
return \<lparr>ct_receive_root = to_bl (hd xs), ct_receive_index = to_bl (hd (tl xs)), ct_receive_depth = hd (tl (tl xs))\<rparr>
od proof (prove)
goal (1 subgoal):
 1. do w0 <- do_machine_op (loadWord (buf + 0x7D * word_size));
w1 <- do_machine_op (loadWord (0x7E * word_size + buf));
w2 <- do_machine_op (loadWord (0x7F * word_size + buf));
return \<lparr>ct_receive_root = to_bl w0, ct_receive_index = to_bl w1, ct_receive_depth = w2\<rparr>
od = do xs <- mapM (load_word_offs buf) [125, 126, 127];
return \<lparr>ct_receive_root = to_bl (hd xs), ct_receive_index = to_bl (hd (tl xs)), ct_receive_depth = hd (tl (tl xs))\<rparr>
od proof (prove)
goal (1 subgoal):
 1. do w0 <- do_machine_op (loadWord (buf + 0x7D * word_size));
w1 <- do_machine_op (loadWord (0x7E * word_size + buf));
w2 <- do_machine_op (loadWord (0x7F * word_size + buf));
return \<lparr>ct_receive_root = to_bl w0, ct_receive_index = to_bl w1, ct_receive_depth = w2\<rparr>
od = do x <- do_machine_op (loadWord (buf + 0x7D * word_of_nat word_size));
xa <- do_machine_op (loadWord (buf + 0x7E * word_of_nat word_size));
xb <- do_machine_op (loadWord (buf + 0x7F * word_of_nat word_size));
return \<lparr>ct_receive_root = to_bl x, ct_receive_index = to_bl xa, ct_receive_depth = xb\<rparr>
od proof (prove)
goal:
No subgoals!