theory Ipc_IF

lemma load_cap_transfer_rev:
  "reads_equiv_valid_inv A aag (K (ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer)))
     (load_cap_transfer buffer)" unfolding load_cap_transfer_def fun_app_def captransfer_from_words_def apply (wp dmo_loadWord_rev | simp)+ apply safe apply (erule aag_has_auth_to_read_captransfer[where x=0, simplified]) apply (erule aag_has_auth_to_read_captransfer[where x=1, simplified]) apply (erule aag_has_auth_to_read_captransfer[where x=2, simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer))) (load_cap_transfer buffer) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer))) (do offset <- return (msg_max_length + msg_max_extra_caps + 2);
w0 <- do_machine_op (loadWord (buffer + word_of_nat offset * word_size));
w1 <- do_machine_op (loadWord (buffer + word_of_nat offset * word_size + word_size));
w2 <- do_machine_op (loadWord (buffer + word_of_nat offset * word_size + 2 * word_size));
return \<lparr>ct_receive_root = data_to_cptr w0, ct_receive_index = data_to_cptr w1, ct_receive_depth = w2\<rparr>
od) proof (prove)
goal (1 subgoal):
 1. ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer) \<Longrightarrow> for_each_byte_of_word (aag_can_read aag) (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size) \<and> for_each_byte_of_word (aag_can_read aag) (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + word_size) \<and> for_each_byte_of_word (aag_can_read aag) (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + 2 * word_size) proof (prove)
goal (3 subgoals):
 1. ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer) \<Longrightarrow> for_each_byte_of_word (aag_can_read aag) (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size)
 2. ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer) \<Longrightarrow> for_each_byte_of_word (aag_can_read aag) (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + word_size)
 3. ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer) \<Longrightarrow> for_each_byte_of_word (aag_can_read aag) (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + 2 * word_size) proof (prove)
goal (2 subgoals):
 1. ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer) \<Longrightarrow> for_each_byte_of_word (aag_can_read aag) (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + word_size)
 2. ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer) \<Longrightarrow> for_each_byte_of_word (aag_can_read aag) (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + 2 * word_size) proof (prove)
goal (1 subgoal):
 1. ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer) \<Longrightarrow> for_each_byte_of_word (aag_can_read aag) (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + 2 * word_size) proof (prove)
goal:
No subgoals!