theory Syscall_C

lemma performInvocation_Notification_ccorres:
  "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s))
       (UNIV \<inter> {s. ntfn_' s = ntfn_Ptr ntfnptr}
             \<inter> {s. badge_' s = badge}
             \<inter> {s. message_' s = message}) []
     (liftE (sendSignal ntfnptr badge))
     (Call performInvocation_Notification_'proc)" apply cinit apply (ctac add: sendSignal_ccorres) apply (simp add: return_returnOk) apply (rule ccorres_return_CE, simp+)[1] apply wp apply simp apply (vcg exspec=sendSignal_modifies) apply simp 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) (UNIV \<inter> \<lbrace>\<acute>ntfn = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> {s. message_' s = message}) [] (liftE (sendSignal ntfnptr badge)) (Call performInvocation_Notification_'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 <- sendSignal ntfnptr badge;
return (Inr ())
od) (CALL sendSignal_'proc(\<acute>ntfn,\<acute>badge);;
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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> \<lbrace>\<acute>ntfn = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> {s. message_' s = message}\<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> sendSignal ntfnptr badge \<lbrace>?Q18\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'18 CALL sendSignal_'proc(\<acute>ntfn,\<acute>badge) {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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> \<lbrace>\<acute>ntfn = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> {s. message_' s = message}\<rbrakk> \<Longrightarrow> (invs' and ?R18) s \<and> s' \<in> {s. badge_'_update (\<lambda>_. badge_' s) (ntfnPtr_'_update (\<lambda>_. ntfn_' s) s) \<in> UNIV \<inter> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = 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> sendSignal ntfnptr badge \<lbrace>?Q18\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'18 CALL sendSignal_'proc(\<acute>ntfn,\<acute>badge) {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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> \<lbrace>\<acute>ntfn = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> {s. message_' s = message}\<rbrakk> \<Longrightarrow> (invs' and ?R18) s \<and> s' \<in> {s. badge_'_update (\<lambda>_. badge_' s) (ntfnPtr_'_update (\<lambda>_. ntfn_' s) s) \<in> UNIV \<inter> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace>} \<inter> ?R'18 proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R18\<rbrace> sendSignal ntfnptr badge \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'18 CALL sendSignal_'proc(\<acute>ntfn,\<acute>badge) {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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> \<lbrace>\<acute>ntfn = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> {s. message_' s = message}\<rbrakk> \<Longrightarrow> (invs' and ?R18) s \<and> s' \<in> {s. badge_'_update (\<lambda>_. badge_' s) (ntfnPtr_'_update (\<lambda>_. ntfn_' s) s) \<in> UNIV \<inter> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace>} \<inter> ?R'18 proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'18 CALL sendSignal_'proc(\<acute>ntfn,\<acute>badge) {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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> \<lbrace>\<acute>ntfn = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> {s. message_' s = message}\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. True)) s \<and> s' \<in> {s. badge_'_update (\<lambda>_. badge_' s) (ntfnPtr_'_update (\<lambda>_. ntfn_' s) s) \<in> UNIV \<inter> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace>} \<inter> ?R'18 proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'18 CALL sendSignal_'proc(\<acute>ntfn) UNIV
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> \<lbrace>\<acute>ntfn = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> {s. message_' s = message}\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. True)) s \<and> s' \<in> {s. badge_'_update (\<lambda>_. badge_' s) (ntfnPtr_'_update (\<lambda>_. ntfn_' s) s) \<in> UNIV \<inter> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace>} \<inter> ?R'18 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> \<lbrace>\<acute>ntfn = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> {s. message_' s = message}\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. True)) s \<and> s' \<in> {s. badge_'_update (\<lambda>_. badge_' s) (ntfnPtr_'_update (\<lambda>_. ntfn_' s) s) \<in> UNIV \<inter> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace>} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal:
No subgoals!