theory Syscall_C

lemma performInvocation_Endpoint_ccorres:
  "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and st_tcb_at' simple' thread and ep_at' epptr
              and sch_act_sane and (\<lambda>s. thread = ksCurThread s
              \<and> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))))
       (UNIV \<inter> {s. block_' s = from_bool blocking}
             \<inter> {s. call_' s = from_bool do_call}
             \<inter> {s. badge_' s = badge}
             \<inter> {s. canGrant_' s = from_bool canGrant}
             \<inter> {s. canGrantReply_' s = from_bool canGrantReply}
             \<inter> {s. ep_' s = ep_Ptr epptr}
             \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>) []
     (liftE (sendIPC blocking do_call badge canGrant canGrantReply thread epptr))
     (Call performInvocation_Endpoint_'proc)" apply cinit apply (ctac add: sendIPC_ccorres) apply (simp add: return_returnOk) apply (rule ccorres_return_CE, simp+)[1] apply wp apply simp apply (vcg exspec=sendIPC_modifies) apply (clarsimp simp add: rf_sr_ksCurThread sch_act_sane_not) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (K (K (\<lambda>_. False)) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and st_tcb_at' simple' thread and ep_at' epptr and sch_act_sane and (\<lambda>s. thread = ksCurThread s \<and> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)))) (UNIV \<inter> \<lbrace>\<acute>block = from_bool blocking\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool do_call\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool canGrant\<rbrace> \<inter> \<lbrace>\<acute>canGrantReply = from_bool canGrantReply\<rbrace> \<inter> \<lbrace>\<acute>ep = ep_Ptr epptr\<rbrace> \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>) [] (liftE (sendIPC blocking do_call badge canGrant canGrantReply thread epptr)) (Call performInvocation_Endpoint_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres (K (K (\<lambda>_. False)) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') ?Q10 ?Q'10 [SKIP] (do r <- sendIPC blocking do_call badge canGrant canGrantReply thread epptr;
return (Inr ())
od) (CALL sendIPC_'proc(\<acute>block,\<acute>call,\<acute>badge,\<acute>canGrant,\<acute>canGrantReply,\<acute>ksCurThread,\<acute>ep);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' thread and ep_at' epptr and sch_act_sane and (\<lambda>s. thread = ksCurThread s \<and> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))))) s; s' \<in> \<lbrace>\<acute>block = from_bool blocking\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool do_call\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool canGrant\<rbrace> \<inter> \<lbrace>\<acute>canGrantReply = from_bool canGrantReply\<rbrace> \<inter> \<lbrace>\<acute>ep = ep_Ptr epptr\<rbrace> \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>\<rbrakk> \<Longrightarrow> ?Q10 s \<and> s' \<in> ?Q'10 proof (prove)
goal (4 subgoals):
 1. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q18 rv) (?Q'18 rv xfdc) [SKIP] (return (Inr ())) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R18\<rbrace> sendIPC blocking do_call badge canGrant canGrantReply thread epptr \<lbrace>?Q18\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'18 CALL sendIPC_'proc(\<acute>block,\<acute>call,\<acute>badge,\<acute>canGrant,\<acute>canGrantReply,\<acute>ksCurThread,\<acute>ep) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'18 rv (xfdc s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' thread and ep_at' epptr and sch_act_sane and (\<lambda>s. thread = ksCurThread s \<and> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))))) s; s' \<in> \<lbrace>\<acute>block = from_bool blocking\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool do_call\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool canGrant\<rbrace> \<inter> \<lbrace>\<acute>canGrantReply = from_bool canGrantReply\<rbrace> \<inter> \<lbrace>\<acute>ep = ep_Ptr epptr\<rbrace> \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' thread and sch_act_not thread and ep_at' epptr and (\<lambda>s. \<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))) and ?R18) s \<and> s' \<in> {s. epptr_'_update (\<lambda>_. ep_' s) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) (canGrantReply_'_update (\<lambda>_. canGrantReply_' s) (canGrant_'_update (\<lambda>_. canGrant_' s) (badge_'_update (\<lambda>_. badge_' s) (do_call_'_update (\<lambda>_. call_' s) (blocking_'_update (\<lambda>_. block_' s) s)))))) \<in> UNIV \<inter> \<lbrace>\<acute>blocking = from_bool blocking\<rbrace> \<inter> \<lbrace>\<acute>do_call = from_bool do_call\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool canGrant\<rbrace> \<inter> \<lbrace>\<acute>canGrantReply = from_bool canGrantReply\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>epptr = ep_Ptr epptr\<rbrace> \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>} \<inter> ?R'18 proof (prove)
goal (4 subgoals):
 1. \<And>xfdc. ccorres (K (K (\<lambda>_. False)) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q18 ()) (?Q'18 () xfdc) [SKIP] (returnOk ()) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R18\<rbrace> sendIPC blocking do_call badge canGrant canGrantReply thread epptr \<lbrace>?Q18\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'18 CALL sendIPC_'proc(\<acute>block,\<acute>call,\<acute>badge,\<acute>canGrant,\<acute>canGrantReply,\<acute>ksCurThread,\<acute>ep) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'18 rv (xfdc s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' thread and ep_at' epptr and sch_act_sane and (\<lambda>s. thread = ksCurThread s \<and> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))))) s; s' \<in> \<lbrace>\<acute>block = from_bool blocking\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool do_call\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool canGrant\<rbrace> \<inter> \<lbrace>\<acute>canGrantReply = from_bool canGrantReply\<rbrace> \<inter> \<lbrace>\<acute>ep = ep_Ptr epptr\<rbrace> \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' thread and sch_act_not thread and ep_at' epptr and (\<lambda>s. \<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))) and ?R18) s \<and> s' \<in> {s. epptr_'_update (\<lambda>_. ep_' s) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) (canGrantReply_'_update (\<lambda>_. canGrantReply_' s) (canGrant_'_update (\<lambda>_. canGrant_' s) (badge_'_update (\<lambda>_. badge_' s) (do_call_'_update (\<lambda>_. call_' s) (blocking_'_update (\<lambda>_. block_' s) s)))))) \<in> UNIV \<inter> \<lbrace>\<acute>blocking = from_bool blocking\<rbrace> \<inter> \<lbrace>\<acute>do_call = from_bool do_call\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool canGrant\<rbrace> \<inter> \<lbrace>\<acute>canGrantReply = from_bool canGrantReply\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>epptr = ep_Ptr epptr\<rbrace> \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>} \<inter> ?R'18 proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R18\<rbrace> sendIPC blocking do_call badge canGrant canGrantReply thread epptr \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'18 CALL sendIPC_'proc(\<acute>block,\<acute>call,\<acute>badge,\<acute>canGrant,\<acute>canGrantReply,\<acute>ksCurThread,\<acute>ep) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> dc rv (K rv (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))\<rbrace>}
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' thread and ep_at' epptr and sch_act_sane and (\<lambda>s. thread = ksCurThread s \<and> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))))) s; s' \<in> \<lbrace>\<acute>block = from_bool blocking\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool do_call\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool canGrant\<rbrace> \<inter> \<lbrace>\<acute>canGrantReply = from_bool canGrantReply\<rbrace> \<inter> \<lbrace>\<acute>ep = ep_Ptr epptr\<rbrace> \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' thread and sch_act_not thread and ep_at' epptr and (\<lambda>s. \<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))) and ?R18) s \<and> s' \<in> {s. epptr_'_update (\<lambda>_. ep_' s) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) (canGrantReply_'_update (\<lambda>_. canGrantReply_' s) (canGrant_'_update (\<lambda>_. canGrant_' s) (badge_'_update (\<lambda>_. badge_' s) (do_call_'_update (\<lambda>_. call_' s) (blocking_'_update (\<lambda>_. block_' s) s)))))) \<in> UNIV \<inter> \<lbrace>\<acute>blocking = from_bool blocking\<rbrace> \<inter> \<lbrace>\<acute>do_call = from_bool do_call\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool canGrant\<rbrace> \<inter> \<lbrace>\<acute>canGrantReply = from_bool canGrantReply\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>epptr = ep_Ptr epptr\<rbrace> \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>} \<inter> ?R'18 proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'18 CALL sendIPC_'proc(\<acute>block,\<acute>call,\<acute>badge,\<acute>canGrant,\<acute>canGrantReply,\<acute>ksCurThread,\<acute>ep) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> dc rv (K rv (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))\<rbrace>}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' thread and ep_at' epptr and sch_act_sane and (\<lambda>s. thread = ksCurThread s \<and> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))))) s; s' \<in> \<lbrace>\<acute>block = from_bool blocking\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool do_call\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool canGrant\<rbrace> \<inter> \<lbrace>\<acute>canGrantReply = from_bool canGrantReply\<rbrace> \<inter> \<lbrace>\<acute>ep = ep_Ptr epptr\<rbrace> \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' thread and sch_act_not thread and ep_at' epptr and (\<lambda>s. \<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. True)) s \<and> s' \<in> {s. epptr_'_update (\<lambda>_. ep_' s) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) (canGrantReply_'_update (\<lambda>_. canGrantReply_' s) (canGrant_'_update (\<lambda>_. canGrant_' s) (badge_'_update (\<lambda>_. badge_' s) (do_call_'_update (\<lambda>_. call_' s) (blocking_'_update (\<lambda>_. block_' s) s)))))) \<in> UNIV \<inter> \<lbrace>\<acute>blocking = from_bool blocking\<rbrace> \<inter> \<lbrace>\<acute>do_call = from_bool do_call\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool canGrant\<rbrace> \<inter> \<lbrace>\<acute>canGrantReply = from_bool canGrantReply\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>epptr = ep_Ptr epptr\<rbrace> \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>} \<inter> ?R'18 proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'18 CALL sendIPC_'proc(\<acute>block,\<acute>call,\<acute>ksCurThread,\<acute>ep) UNIV
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' thread and ep_at' epptr and sch_act_sane and (\<lambda>s. thread = ksCurThread s \<and> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))))) s; s' \<in> \<lbrace>\<acute>block = from_bool blocking\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool do_call\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool canGrant\<rbrace> \<inter> \<lbrace>\<acute>canGrantReply = from_bool canGrantReply\<rbrace> \<inter> \<lbrace>\<acute>ep = ep_Ptr epptr\<rbrace> \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' thread and sch_act_not thread and ep_at' epptr and (\<lambda>s. \<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. True)) s \<and> s' \<in> {s. epptr_'_update (\<lambda>_. ep_' s) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) (canGrantReply_'_update (\<lambda>_. canGrantReply_' s) (canGrant_'_update (\<lambda>_. canGrant_' s) (badge_'_update (\<lambda>_. badge_' s) (do_call_'_update (\<lambda>_. call_' s) (blocking_'_update (\<lambda>_. block_' s) s)))))) \<in> UNIV \<inter> \<lbrace>\<acute>blocking = from_bool blocking\<rbrace> \<inter> \<lbrace>\<acute>do_call = from_bool do_call\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool canGrant\<rbrace> \<inter> \<lbrace>\<acute>canGrantReply = from_bool canGrantReply\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>epptr = ep_Ptr epptr\<rbrace> \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>} \<inter> ?R'18 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' thread and ep_at' epptr and sch_act_sane and (\<lambda>s. thread = ksCurThread s \<and> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))))) s; s' \<in> \<lbrace>\<acute>block = from_bool blocking\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool do_call\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool canGrant\<rbrace> \<inter> \<lbrace>\<acute>canGrantReply = from_bool canGrantReply\<rbrace> \<inter> \<lbrace>\<acute>ep = ep_Ptr epptr\<rbrace> \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' thread and sch_act_not thread and ep_at' epptr and (\<lambda>s. \<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. True)) s \<and> s' \<in> {s. epptr_'_update (\<lambda>_. ep_' s) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) (canGrantReply_'_update (\<lambda>_. canGrantReply_' s) (canGrant_'_update (\<lambda>_. canGrant_' s) (badge_'_update (\<lambda>_. badge_' s) (do_call_'_update (\<lambda>_. call_' s) (blocking_'_update (\<lambda>_. block_' s) s)))))) \<in> UNIV \<inter> \<lbrace>\<acute>blocking = from_bool blocking\<rbrace> \<inter> \<lbrace>\<acute>do_call = from_bool do_call\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool canGrant\<rbrace> \<inter> \<lbrace>\<acute>canGrantReply = from_bool canGrantReply\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>epptr = ep_Ptr epptr\<rbrace> \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal:
No subgoals!