theory Ipc_R

lemma replyFromKernel_corres:
  "corres dc (tcb_at t and invs) (tcb_at' t and invs')
             (reply_from_kernel t r) (replyFromKernel t r)" apply (case_tac r) apply (clarsimp simp: replyFromKernel_def reply_from_kernel_def
                        badge_register_def badgeRegister_def) apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF lookupIPCBuffer_corres]) apply (rule corres_split[OF asUser_setRegister_corres]) apply (rule corres_split_eqr[OF setMRs_corres]) apply simp apply (rule setMessageInfo_corres) apply (wp hoare_case_option_wp hoare_valid_ipc_buffer_ptr_typ_at'
                 | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t and invs) (tcb_at' t and invs') (reply_from_kernel t r) (replyFromKernel t r) proof (prove)
goal (1 subgoal):
 1. \<And>a b. r = (a, b) \<Longrightarrow> corres dc (tcb_at t and invs) (tcb_at' t and invs') (reply_from_kernel t r) (replyFromKernel t r) proof (prove)
goal (1 subgoal):
 1. \<And>a b. r = (a, b) \<Longrightarrow> corres dc (tcb_at t and invs) (tcb_at' t and invs') (do buf <- lookup_ipc_buffer True t;
y <- as_user t (setRegister ARM.badgeRegister 0);
len <- set_mrs t buf b;
set_message_info t (Structures_A.message_info.MI len 0 0 a)
od) (do destIPCBuffer <- lookupIPCBuffer True t;
y <- asUser t (setRegister ARM.badgeRegister 0);
len <- setMRs t destIPCBuffer b;
setMessageInfo t (Types_H.message_info.MI len 0 0 a)
od) proof (prove)
goal (3 subgoals):
 1. \<And>a b. r = (a, b) \<Longrightarrow> corres dc (?Q1 a b) (?Q'1 a b) (do buf <- lookup_ipc_buffer True t;
y <- as_user t (setRegister ARM.badgeRegister 0);
len <- set_mrs t buf b;
set_message_info t (Structures_A.message_info.MI len 0 0 a)
od) (do destIPCBuffer <- lookupIPCBuffer True t;
y <- asUser t (setRegister ARM.badgeRegister 0);
len <- setMRs t destIPCBuffer b;
setMessageInfo t (Types_H.message_info.MI len 0 0 a)
od)
 2. \<And>a b s. \<lbrakk>r = (a, b); (tcb_at t and invs) s\<rbrakk> \<Longrightarrow> ?Q1 a b s
 3. \<And>a b s. \<lbrakk>r = (a, b); (tcb_at' t and invs') s\<rbrakk> \<Longrightarrow> ?Q'1 a b s proof (prove)
goal (5 subgoals):
 1. \<And>a b rv. r = (a, b) \<Longrightarrow> corres dc (?R5 a b rv) (?R'5 a b rv) (do y <- as_user t (setRegister ARM.badgeRegister 0);
len <- set_mrs t rv b;
set_message_info t (Structures_A.message_info.MI len 0 0 a)
od) (do y <- asUser t (setRegister ARM.badgeRegister 0);
len <- setMRs t rv b;
setMessageInfo t (Types_H.message_info.MI len 0 0 a)
od)
 2. \<And>a b. r = (a, b) \<Longrightarrow> \<lbrace>?Q5 a b\<rbrace> lookup_ipc_buffer True t \<lbrace>?R5 a b\<rbrace>
 3. \<And>a b. r = (a, b) \<Longrightarrow> \<lbrace>?Q'5 a b\<rbrace> lookupIPCBuffer True t \<lbrace>?R'5 a b\<rbrace>
 4. \<And>a b s. \<lbrakk>r = (a, b); (tcb_at t and invs) s\<rbrakk> \<Longrightarrow> (tcb_at t and invs and ?Q5 a b) s
 5. \<And>a b s. \<lbrakk>r = (a, b); (tcb_at' t and invs') s\<rbrakk> \<Longrightarrow> (tcb_at' t and invs' and ?Q'5 a b) s proof (prove)
goal (7 subgoals):
 1. \<And>a b rv y ya. \<lbrakk>r = (a, b); dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R10 a b rv y) (?R'10 a b rv ya) (do len <- set_mrs t rv b;
set_message_info t (Structures_A.message_info.MI len 0 0 a)
od) (do len <- setMRs t rv b;
setMessageInfo t (Types_H.message_info.MI len 0 0 a)
od)
 2. \<And>a b rv. r = (a, b) \<Longrightarrow> \<lbrace>?Q10 a b rv\<rbrace> as_user t (setRegister ARM.badgeRegister 0) \<lbrace>?R10 a b rv\<rbrace>
 3. \<And>a b rv. r = (a, b) \<Longrightarrow> \<lbrace>?Q'10 a b rv\<rbrace> asUser t (setRegister ARM.badgeRegister 0) \<lbrace>?R'10 a b rv\<rbrace>
 4. \<And>a b. r = (a, b) \<Longrightarrow> \<lbrace>?Q5 a b\<rbrace> lookup_ipc_buffer True t \<lbrace>\<lambda>rv. tcb_at t and ?Q10 a b rv\<rbrace>
 5. \<And>a b. r = (a, b) \<Longrightarrow> \<lbrace>?Q'5 a b\<rbrace> lookupIPCBuffer True t \<lbrace>\<lambda>rv. tcb_at' t and ?Q'10 a b rv\<rbrace>
 6. \<And>a b s. \<lbrakk>r = (a, b); (tcb_at t and invs) s\<rbrakk> \<Longrightarrow> (tcb_at t and invs and ?Q5 a b) s
 7. \<And>a b s. \<lbrakk>r = (a, b); (tcb_at' t and invs') s\<rbrakk> \<Longrightarrow> (tcb_at' t and invs' and ?Q'5 a b) s proof (prove)
goal (10 subgoals):
 1. \<And>a b rv y ya. \<lbrakk>r = (a, b); dc y ya\<rbrakk> \<Longrightarrow> b = b
 2. \<And>a b rv y ya len. \<lbrakk>r = (a, b); dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 a b rv y ya len) (?R'15 a b rv y ya len) (set_message_info t (Structures_A.message_info.MI len 0 0 a)) (setMessageInfo t (Types_H.message_info.MI len 0 0 a))
 3. \<And>a b rv y ya. \<lbrakk>r = (a, b); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a b rv y\<rbrace> set_mrs t rv b \<lbrace>?R15 a b rv y ya\<rbrace>
 4. \<And>a b rv y ya. \<lbrakk>r = (a, b); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 a b rv ya\<rbrace> setMRs t rv b \<lbrace>?R'15 a b rv y ya\<rbrace>
 5. \<And>a b rv. r = (a, b) \<Longrightarrow> \<lbrace>?Q10 a b rv\<rbrace> as_user t (setRegister ARM.badgeRegister 0) \<lbrace>\<lambda>y. tcb_at t and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and ?Q19 a b rv y\<rbrace>
 6. \<And>a b rv. r = (a, b) \<Longrightarrow> \<lbrace>?Q'10 a b rv\<rbrace> asUser t (setRegister ARM.badgeRegister 0) \<lbrace>\<lambda>ya. tcb_at' t and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'22 a b rv ya\<rbrace>
 7. \<And>a b. r = (a, b) \<Longrightarrow> \<lbrace>?Q5 a b\<rbrace> lookup_ipc_buffer True t \<lbrace>\<lambda>rv. tcb_at t and ?Q10 a b rv\<rbrace>
 8. \<And>a b. r = (a, b) \<Longrightarrow> \<lbrace>?Q'5 a b\<rbrace> lookupIPCBuffer True t \<lbrace>\<lambda>rv. tcb_at' t and ?Q'10 a b rv\<rbrace>
 9. \<And>a b s. \<lbrakk>r = (a, b); (tcb_at t and invs) s\<rbrakk> \<Longrightarrow> (tcb_at t and invs and ?Q5 a b) s
 10. \<And>a b s. \<lbrakk>r = (a, b); (tcb_at' t and invs') s\<rbrakk> \<Longrightarrow> (tcb_at' t and invs' and ?Q'5 a b) s proof (prove)
goal (9 subgoals):
 1. \<And>a b rv y ya len. \<lbrakk>r = (a, b); dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 a b rv y ya len) (?R'15 a b rv y ya len) (set_message_info t (Structures_A.message_info.MI len 0 0 a)) (setMessageInfo t (Types_H.message_info.MI len 0 0 a))
 2. \<And>a b rv y ya. \<lbrakk>r = (a, b); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a b rv y\<rbrace> set_mrs t rv b \<lbrace>?R15 a b rv y ya\<rbrace>
 3. \<And>a b rv y ya. \<lbrakk>r = (a, b); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 a b rv ya\<rbrace> setMRs t rv b \<lbrace>?R'15 a b rv y ya\<rbrace>
 4. \<And>a b rv. r = (a, b) \<Longrightarrow> \<lbrace>?Q10 a b rv\<rbrace> as_user t (setRegister ARM.badgeRegister 0) \<lbrace>\<lambda>y. tcb_at t and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and ?Q19 a b rv y\<rbrace>
 5. \<And>a b rv. r = (a, b) \<Longrightarrow> \<lbrace>?Q'10 a b rv\<rbrace> asUser t (setRegister ARM.badgeRegister 0) \<lbrace>\<lambda>ya. tcb_at' t and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'22 a b rv ya\<rbrace>
 6. \<And>a b. r = (a, b) \<Longrightarrow> \<lbrace>?Q5 a b\<rbrace> lookup_ipc_buffer True t \<lbrace>\<lambda>rv. tcb_at t and ?Q10 a b rv\<rbrace>
 7. \<And>a b. r = (a, b) \<Longrightarrow> \<lbrace>?Q'5 a b\<rbrace> lookupIPCBuffer True t \<lbrace>\<lambda>rv. tcb_at' t and ?Q'10 a b rv\<rbrace>
 8. \<And>a b s. \<lbrakk>r = (a, b); (tcb_at t and invs) s\<rbrakk> \<Longrightarrow> (tcb_at t and invs and ?Q5 a b) s
 9. \<And>a b s. \<lbrakk>r = (a, b); (tcb_at' t and invs') s\<rbrakk> \<Longrightarrow> (tcb_at' t and invs' and ?Q'5 a b) s proof (prove)
goal (9 subgoals):
 1. \<And>a b rv y ya len. \<lbrakk>r = (a, b); dc y ya\<rbrakk> \<Longrightarrow> Types_H.message_info.MI len 0 0 a = message_info_map (Structures_A.message_info.MI len 0 0 a)
 2. \<And>a b rv y ya. \<lbrakk>r = (a, b); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a b rv y\<rbrace> set_mrs t rv b \<lbrace>\<lambda>len. tcb_at t\<rbrace>
 3. \<And>a b rv y ya. \<lbrakk>r = (a, b); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 a b rv ya\<rbrace> setMRs t rv b \<lbrace>\<lambda>len. tcb_at' t\<rbrace>
 4. \<And>a b rv. r = (a, b) \<Longrightarrow> \<lbrace>?Q10 a b rv\<rbrace> as_user t (setRegister ARM.badgeRegister 0) \<lbrace>\<lambda>y. tcb_at t and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and ?Q19 a b rv y\<rbrace>
 5. \<And>a b rv. r = (a, b) \<Longrightarrow> \<lbrace>?Q'10 a b rv\<rbrace> asUser t (setRegister ARM.badgeRegister 0) \<lbrace>\<lambda>ya. tcb_at' t and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'22 a b rv ya\<rbrace>
 6. \<And>a b. r = (a, b) \<Longrightarrow> \<lbrace>?Q5 a b\<rbrace> lookup_ipc_buffer True t \<lbrace>\<lambda>rv. tcb_at t and ?Q10 a b rv\<rbrace>
 7. \<And>a b. r = (a, b) \<Longrightarrow> \<lbrace>?Q'5 a b\<rbrace> lookupIPCBuffer True t \<lbrace>\<lambda>rv. tcb_at' t and ?Q'10 a b rv\<rbrace>
 8. \<And>a b s. \<lbrakk>r = (a, b); (tcb_at t and invs) s\<rbrakk> \<Longrightarrow> (tcb_at t and invs and ?Q5 a b) s
 9. \<And>a b s. \<lbrakk>r = (a, b); (tcb_at' t and invs') s\<rbrakk> \<Longrightarrow> (tcb_at' t and invs' and ?Q'5 a b) s proof (prove)
goal:
No subgoals!