theory Refine_C

lemma ccorres_get_registers:
  "\<lbrakk> \<And>cptr msgInfo. ccorres dc xfdc
     ((\<lambda>s. P s \<and> Q s \<and>
           obj_at' (\<lambda>tcb. (atcbContextGet o tcbArch) tcb ARM_H.capRegister = cptr
                      \<and>   (atcbContextGet o tcbArch) tcb ARM_H.msgInfoRegister = msgInfo)
             (ksCurThread s) s) and R)
     (UNIV \<inter> \<lbrace>\<acute>cptr = cptr\<rbrace> \<inter> \<lbrace>\<acute>msgInfo = msgInfo\<rbrace>) [] m c \<rbrakk>
      \<Longrightarrow>
   ccorres dc xfdc
     (P and Q and ct_in_state' \<top> and R)
     {s. \<exists>v. cslift s (ksCurThread_' (globals s)) = Some v
              \<and> cptr_' s = index (registers_C (tcbContext_C (tcbArch_C v))) (unat Kernel_C.capRegister)
              \<and> msgInfo_' s = index (registers_C (tcbContext_C (tcbArch_C v))) (unat Kernel_C.msgInfoRegister)} []
     m c" apply (rule ccorres_assume_pre) apply (clarsimp simp: ct_in_state'_def st_tcb_at'_def) apply (drule obj_at_ko_at', clarsimp) apply (erule_tac x="(atcbContextGet o tcbArch) ko ARM_H.capRegister" in meta_allE) apply (erule_tac x="(atcbContextGet o tcbArch) ko ARM_H.msgInfoRegister" in meta_allE) apply (erule ccorres_guard_imp2) apply (clarsimp simp: rf_sr_ksCurThread) apply (drule(1) obj_at_cslift_tcb, clarsimp simp: obj_at'_def projectKOs) apply (clarsimp simp: ctcb_relation_def ccontext_relation_def
                        ARM_H.msgInfoRegister_def ARM_H.capRegister_def
                        ARM.msgInfoRegister_def ARM.capRegister_def
                        carch_tcb_relation_def
                        "StrictC'_register_defs") done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>cptr msgInfo. ccorres dc xfdc ((\<lambda>s. P s \<and> Q s \<and> obj_at' (\<lambda>tcb. (atcbContextGet \<circ> tcbArch) tcb Thread_H.capRegister = cptr \<and> (atcbContextGet \<circ> tcbArch) tcb TCB_H.msgInfoRegister = msgInfo) (ksCurThread s) s) and R) (UNIV \<inter> \<lbrace>\<acute>cptr = cptr\<rbrace> \<inter> \<lbrace>\<acute>msgInfo = msgInfo\<rbrace>) [] m c) \<Longrightarrow> ccorres dc xfdc (P and Q and ct_in_state' (\<lambda>_. True) and R) {s. \<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> msgInfo_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]} [] m c proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>cptr msgInfo. ccorres dc xfdc ((\<lambda>s. P s \<and> Q s \<and> obj_at' (\<lambda>tcb. (atcbContextGet \<circ> tcbArch) tcb Thread_H.capRegister = cptr \<and> (atcbContextGet \<circ> tcbArch) tcb TCB_H.msgInfoRegister = msgInfo) (ksCurThread s) s) and R) (UNIV \<inter> \<lbrace>\<acute>cptr = cptr\<rbrace> \<inter> \<lbrace>\<acute>msgInfo = msgInfo\<rbrace>) [] m c; (P and Q and ct_in_state' (\<lambda>_. True) and R) s\<rbrakk> \<Longrightarrow> ccorres dc xfdc (P and Q and ct_in_state' (\<lambda>_. True) and R and (\<lambda>s'. s' = s)) {s. \<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> msgInfo_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]} [] m c proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>cptr msgInfo. ccorres dc xfdc ((\<lambda>s. P s \<and> Q s \<and> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) Thread_H.capRegister = cptr \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) (ksCurThread s) s) and R) (\<lbrace>\<acute>cptr = cptr\<rbrace> \<inter> \<lbrace>\<acute>msgInfo = msgInfo\<rbrace>) [] m c; P s; Q s; tcb_at' (ksCurThread s) s; R s\<rbrakk> \<Longrightarrow> ccorres dc xfdc (P and Q and (\<lambda>s. tcb_at' (ksCurThread s) s) and R and (\<lambda>s'. s' = s)) {s. \<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> msgInfo_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]} [] m c proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>\<And>cptr msgInfo. ccorres dc xfdc ((\<lambda>s. P s \<and> Q s \<and> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) Thread_H.capRegister = cptr \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) (ksCurThread s) s) and R) (\<lbrace>\<acute>cptr = cptr\<rbrace> \<inter> \<lbrace>\<acute>msgInfo = msgInfo\<rbrace>) [] m c; P s; Q s; R s; ko_at' ko (ksCurThread s) s\<rbrakk> \<Longrightarrow> ccorres dc xfdc (P and Q and (\<lambda>s. tcb_at' (ksCurThread s) s) and R and (\<lambda>s'. s' = s)) {s. \<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> msgInfo_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]} [] m c proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>P s; Q s; R s; ko_at' ko (ksCurThread s) s; \<And>msgInfo. ccorres dc xfdc ((\<lambda>s. P s \<and> Q s \<and> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) Thread_H.capRegister = (atcbContextGet \<circ> tcbArch) ko Thread_H.capRegister \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) (ksCurThread s) s) and R) (\<lbrace>\<acute>cptr = (atcbContextGet \<circ> tcbArch) ko Thread_H.capRegister\<rbrace> \<inter> \<lbrace>\<acute>msgInfo = msgInfo\<rbrace>) [] m c\<rbrakk> \<Longrightarrow> ccorres dc xfdc (P and Q and (\<lambda>s. tcb_at' (ksCurThread s) s) and R and (\<lambda>s'. s' = s)) {s. \<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> msgInfo_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]} [] m c proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>P s; Q s; R s; ko_at' ko (ksCurThread s) s; ccorres dc xfdc ((\<lambda>s. P s \<and> Q s \<and> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) Thread_H.capRegister = (atcbContextGet \<circ> tcbArch) ko Thread_H.capRegister \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = (atcbContextGet \<circ> tcbArch) ko TCB_H.msgInfoRegister) (ksCurThread s) s) and R) (\<lbrace>\<acute>cptr = (atcbContextGet \<circ> tcbArch) ko Thread_H.capRegister\<rbrace> \<inter> \<lbrace>\<acute>msgInfo = (atcbContextGet \<circ> tcbArch) ko TCB_H.msgInfoRegister\<rbrace>) [] m c\<rbrakk> \<Longrightarrow> ccorres dc xfdc (P and Q and (\<lambda>s. tcb_at' (ksCurThread s) s) and R and (\<lambda>s'. s' = s)) {s. \<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> msgInfo_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]} [] m c proof (prove)
goal (1 subgoal):
 1. \<And>s ko sa s'. \<lbrakk>P s; Q s; R s; ko_at' ko (ksCurThread s) s; (sa, s') \<in> rf_sr; (P and Q and (\<lambda>s. tcb_at' (ksCurThread s) s) and R and (\<lambda>s'. s' = s)) sa; s' \<in> {s. \<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> msgInfo_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]}\<rbrakk> \<Longrightarrow> ((\<lambda>s. P s \<and> Q s \<and> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) Thread_H.capRegister = (atcbContextGet \<circ> tcbArch) ko Thread_H.capRegister \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = (atcbContextGet \<circ> tcbArch) ko TCB_H.msgInfoRegister) (ksCurThread s) s) and R) sa \<and> s' \<in> \<lbrace>\<acute>cptr = (atcbContextGet \<circ> tcbArch) ko Thread_H.capRegister\<rbrace> \<inter> \<lbrace>\<acute>msgInfo = (atcbContextGet \<circ> tcbArch) ko TCB_H.msgInfoRegister\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko s' v. \<lbrakk>P s; Q s; R s; ko_at' ko (ksCurThread s) s; (s, s') \<in> rf_sr; tcb_at' (ksCurThread s) s; cslift s' (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some v; cptr_' s' = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister]; msgInfo_' s' = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) Thread_H.capRegister = atcbContextGet (tcbArch ko) Thread_H.capRegister \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = atcbContextGet (tcbArch ko) TCB_H.msgInfoRegister) (ksCurThread s) s \<and> registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] = atcbContextGet (tcbArch ko) Thread_H.capRegister \<and> registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister] = atcbContextGet (tcbArch ko) TCB_H.msgInfoRegister proof (prove)
goal (1 subgoal):
 1. \<And>s ko s' v. \<lbrakk>P s; Q s; R s; (s, s') \<in> rf_sr; cslift s' (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some v; cptr_' s' = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister]; msgInfo_' s' = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]; ksPSpace s (ksCurThread s) = Some (KOTCB ko); is_aligned (ksCurThread s) (objBitsKO (KOTCB ko)); ps_clear (ksCurThread s) (objBitsKO (KOTCB ko)) s; ctcb_relation ko v\<rbrakk> \<Longrightarrow> registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] = atcbContextGet (tcbArch ko) Thread_H.capRegister \<and> registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister] = atcbContextGet (tcbArch ko) TCB_H.msgInfoRegister proof (prove)
goal:
No subgoals!