theory Ipc_R

lemma loadCapTransfer_corres:
  "corres ct_relation \<top> (valid_ipc_buffer_ptr' buffer) (load_cap_transfer buffer) (loadCapTransfer buffer)" apply (simp add: load_cap_transfer_def loadCapTransfer_def
                   captransfer_from_words_def
                   capTransferDataSize_def capTransferFromWords_def
                   msgExtraCapBits_def word_size add.commute add.left_commute
                   msg_max_length_def msg_max_extra_caps_def word_size_def
                   msgMaxLength_def msgMaxExtraCaps_def msgLengthBits_def wordSize_def wordBits_def
              del: upt.simps) apply (rule corres_guard_imp) apply (rule corres_split[OF load_word_corres]) apply (rule corres_split[OF load_word_corres]) apply (rule corres_split[OF load_word_corres]) apply (rule_tac P=\<top> and P'=\<top> in corres_inst) apply (clarsimp simp: ct_relation_def) apply (wp no_irq_loadWord)+ apply simp apply (simp add: conj_comms) apply safe apply (erule valid_ipc_buffer_ptr_aligned_2, simp add: is_aligned_def)+ apply (erule valid_ipc_buffer_ptr'D2, simp add: max_ipc_words, simp add: is_aligned_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres ct_relation (\<lambda>_. True) (valid_ipc_buffer_ptr' buffer) (load_cap_transfer buffer) (loadCapTransfer buffer) proof (prove)
goal (1 subgoal):
 1. corres ct_relation (\<lambda>_. True) (valid_ipc_buffer_ptr' buffer) (do w0 <- do_machine_op (loadWord (buffer + 0x1F4));
w1 <- do_machine_op (loadWord (buffer + 0x1F8));
w2 <- do_machine_op (loadWord (buffer + 0x1FC));
return \<lparr>ct_receive_root = to_bl w0, ct_receive_index = to_bl w1, ct_receive_depth = w2\<rparr>
od) (do w0 <- loadWordUser (buffer + 0x1F4);
w1 <- loadWordUser (buffer + 0x1F8);
w2 <- loadWordUser (buffer + 0x1FC);
return (CT w0 w1 (unat w2))
od) proof (prove)
goal (3 subgoals):
 1. corres ct_relation ?Q1 ?Q'1 (do w0 <- do_machine_op (loadWord (buffer + 0x1F4));
w1 <- do_machine_op (loadWord (buffer + 0x1F8));
w2 <- do_machine_op (loadWord (buffer + 0x1FC));
return \<lparr>ct_receive_root = to_bl w0, ct_receive_index = to_bl w1, ct_receive_depth = w2\<rparr>
od) (do w0 <- loadWordUser (buffer + 0x1F4);
w1 <- loadWordUser (buffer + 0x1F8);
w2 <- loadWordUser (buffer + 0x1FC);
return (CT w0 w1 (unat w2))
od)
 2. \<And>s. True \<Longrightarrow> ?Q1 s
 3. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> ?Q'1 s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. rv = rv' \<Longrightarrow> corres ct_relation (?R5 rv) (?R'5 rv') (do w1 <- do_machine_op (loadWord (buffer + 0x1F8));
w2 <- do_machine_op (loadWord (buffer + 0x1FC));
return \<lparr>ct_receive_root = to_bl rv, ct_receive_index = to_bl w1, ct_receive_depth = w2\<rparr>
od) (do w1 <- loadWordUser (buffer + 0x1F8);
w2 <- loadWordUser (buffer + 0x1FC);
return (CT rv' w1 (unat w2))
od)
 2. \<lbrace>?Q5\<rbrace> do_machine_op (loadWord (buffer + 0x1F4)) \<lbrace>?R5\<rbrace>
 3. \<lbrace>?Q'5\<rbrace> loadWordUser (buffer + 0x1F4) \<lbrace>?R'5\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 5. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> (typ_at' UserDataT (buffer + 0x1F4 && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1F4) 2) and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' w1 w1a. \<lbrakk>rv = rv'; w1 = w1a\<rbrakk> \<Longrightarrow> corres ct_relation (?R10 rv rv' w1) (?R'10 rv rv' w1a) (do w2 <- do_machine_op (loadWord (buffer + 0x1FC));
return \<lparr>ct_receive_root = to_bl rv, ct_receive_index = to_bl w1, ct_receive_depth = w2\<rparr>
od) (do w2 <- loadWordUser (buffer + 0x1FC);
return (CT rv' w1a (unat w2))
od)
 2. \<And>rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q12 rv\<rbrace> do_machine_op (loadWord (buffer + 0x1F8)) \<lbrace>?R10 rv rv'\<rbrace>
 3. \<And>rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'15 rv'\<rbrace> loadWordUser (buffer + 0x1F8) \<lbrace>?R'10 rv rv'\<rbrace>
 4. \<lbrace>?Q5\<rbrace> do_machine_op (loadWord (buffer + 0x1F4)) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q12 rv\<rbrace>
 5. \<lbrace>?Q'5\<rbrace> loadWordUser (buffer + 0x1F4) \<lbrace>\<lambda>rv'. typ_at' UserDataT (buffer + 0x1F8 && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1F8) 2) and ?Q'15 rv'\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 7. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> (typ_at' UserDataT (buffer + 0x1F4 && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1F4) 2) and ?Q'5) s proof (prove)
goal (9 subgoals):
 1. \<And>rv rv' w1 w1a w2 w2a. \<lbrakk>rv = rv'; w1 = w1a; w2 = w2a\<rbrakk> \<Longrightarrow> corres ct_relation (?R19 rv rv' w1 w1a w2) (?R'19 rv rv' w1 w1a w2a) (return \<lparr>ct_receive_root = to_bl rv, ct_receive_index = to_bl w1, ct_receive_depth = w2\<rparr>) (return (CT rv' w1a (unat w2a)))
 2. \<And>rv rv' w1 w1a. \<lbrakk>rv = rv'; w1 = w1a\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 rv rv' w1\<rbrace> do_machine_op (loadWord (buffer + 0x1FC)) \<lbrace>?R19 rv rv' w1 w1a\<rbrace>
 3. \<And>rv rv' w1 w1a. \<lbrakk>rv = rv'; w1 = w1a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'24 rv rv' w1a\<rbrace> loadWordUser (buffer + 0x1FC) \<lbrace>?R'19 rv rv' w1 w1a\<rbrace>
 4. \<And>rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q12 rv\<rbrace> do_machine_op (loadWord (buffer + 0x1F8)) \<lbrace>\<lambda>w1. (\<lambda>_. True) and ?Q21 rv rv' w1\<rbrace>
 5. \<And>rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'15 rv'\<rbrace> loadWordUser (buffer + 0x1F8) \<lbrace>\<lambda>w1a. typ_at' UserDataT (buffer + 0x1FC && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1FC) 2) and ?Q'24 rv rv' w1a\<rbrace>
 6. \<lbrace>?Q5\<rbrace> do_machine_op (loadWord (buffer + 0x1F4)) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q12 rv\<rbrace>
 7. \<lbrace>?Q'5\<rbrace> loadWordUser (buffer + 0x1F4) \<lbrace>\<lambda>rv'. typ_at' UserDataT (buffer + 0x1F8 && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1F8) 2) and ?Q'15 rv'\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 9. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> (typ_at' UserDataT (buffer + 0x1F4 && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1F4) 2) and ?Q'5) s proof (prove)
goal (9 subgoals):
 1. \<And>rv rv' w1 w1a w2 w2a. \<lbrakk>rv = rv'; w1 = w1a; w2 = w2a\<rbrakk> \<Longrightarrow> corres ct_relation (\<lambda>_. True) (\<lambda>_. True) (return \<lparr>ct_receive_root = to_bl rv, ct_receive_index = to_bl w1, ct_receive_depth = w2\<rparr>) (return (CT rv' w1a (unat w2a)))
 2. \<And>rv rv' w1 w1a. \<lbrakk>rv = rv'; w1 = w1a\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 rv rv' w1\<rbrace> do_machine_op (loadWord (buffer + 0x1FC)) \<lbrace>\<lambda>w2 _. True\<rbrace>
 3. \<And>rv rv' w1 w1a. \<lbrakk>rv = rv'; w1 = w1a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'24 rv rv' w1a\<rbrace> loadWordUser (buffer + 0x1FC) \<lbrace>\<lambda>w2a _. True\<rbrace>
 4. \<And>rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q12 rv\<rbrace> do_machine_op (loadWord (buffer + 0x1F8)) \<lbrace>\<lambda>w1. (\<lambda>_. True) and ?Q21 rv rv' w1\<rbrace>
 5. \<And>rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'15 rv'\<rbrace> loadWordUser (buffer + 0x1F8) \<lbrace>\<lambda>w1a. typ_at' UserDataT (buffer + 0x1FC && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1FC) 2) and ?Q'24 rv rv' w1a\<rbrace>
 6. \<lbrace>?Q5\<rbrace> do_machine_op (loadWord (buffer + 0x1F4)) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q12 rv\<rbrace>
 7. \<lbrace>?Q'5\<rbrace> loadWordUser (buffer + 0x1F4) \<lbrace>\<lambda>rv'. typ_at' UserDataT (buffer + 0x1F8 && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1F8) 2) and ?Q'15 rv'\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 9. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> (typ_at' UserDataT (buffer + 0x1F4 && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1F4) 2) and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' w1 w1a. \<lbrakk>rv = rv'; w1 = w1a\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 rv rv' w1\<rbrace> do_machine_op (loadWord (buffer + 0x1FC)) \<lbrace>\<lambda>w2 _. True\<rbrace>
 2. \<And>rv rv' w1 w1a. \<lbrakk>rv = rv'; w1 = w1a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'24 rv rv' w1a\<rbrace> loadWordUser (buffer + 0x1FC) \<lbrace>\<lambda>w2a _. True\<rbrace>
 3. \<And>rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q12 rv\<rbrace> do_machine_op (loadWord (buffer + 0x1F8)) \<lbrace>\<lambda>w1. (\<lambda>_. True) and ?Q21 rv rv' w1\<rbrace>
 4. \<And>rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'15 rv'\<rbrace> loadWordUser (buffer + 0x1F8) \<lbrace>\<lambda>w1a. typ_at' UserDataT (buffer + 0x1FC && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1FC) 2) and ?Q'24 rv rv' w1a\<rbrace>
 5. \<lbrace>?Q5\<rbrace> do_machine_op (loadWord (buffer + 0x1F4)) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q12 rv\<rbrace>
 6. \<lbrace>?Q'5\<rbrace> loadWordUser (buffer + 0x1F4) \<lbrace>\<lambda>rv'. typ_at' UserDataT (buffer + 0x1F8 && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1F8) 2) and ?Q'15 rv'\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 8. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> (typ_at' UserDataT (buffer + 0x1F4 && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1F4) 2) and ?Q'5) s proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True)) s
 2. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> (typ_at' UserDataT (buffer + 0x1F4 && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1F4) 2) and (typ_at' UserDataT (buffer + 0x1F8 && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1F8) 2) and (typ_at' UserDataT (buffer + 0x1FC && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1FC) 2) and (\<lambda>_. True)))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> (typ_at' UserDataT (buffer + 0x1F4 && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1F4) 2) and (typ_at' UserDataT (buffer + 0x1F8 && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1F8) 2) and (typ_at' UserDataT (buffer + 0x1FC && ~~ mask pageBits) and (\<lambda>s. is_aligned (buffer + 0x1FC) 2) and (\<lambda>_. True)))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> is_aligned (buffer + 0x1F8) 2 \<and> is_aligned (buffer + 0x1F4) 2 \<and> is_aligned (buffer + 0x1FC) 2 \<and> typ_at' UserDataT (buffer + 0x1F8 && ~~ mask pageBits) s \<and> typ_at' UserDataT (buffer + 0x1F4 && ~~ mask pageBits) s \<and> typ_at' UserDataT (buffer + 0x1FC && ~~ mask pageBits) s proof (prove)
goal (6 subgoals):
 1. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> is_aligned (buffer + 0x1F8) 2
 2. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> is_aligned (buffer + 0x1F4) 2
 3. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> is_aligned (buffer + 0x1FC) 2
 4. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> typ_at' UserDataT (buffer + 0x1F8 && ~~ mask pageBits) s
 5. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> typ_at' UserDataT (buffer + 0x1F4 && ~~ mask pageBits) s
 6. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> typ_at' UserDataT (buffer + 0x1FC && ~~ mask pageBits) s proof (prove)
goal (3 subgoals):
 1. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> typ_at' UserDataT (buffer + 0x1F8 && ~~ mask pageBits) s
 2. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> typ_at' UserDataT (buffer + 0x1F4 && ~~ mask pageBits) s
 3. \<And>s. valid_ipc_buffer_ptr' buffer s \<Longrightarrow> typ_at' UserDataT (buffer + 0x1FC && ~~ mask pageBits) s proof (prove)
goal:
No subgoals!