theory Ipc_R

lemma completeSignal_invs:
  "\<lbrace>invs' and tcb_at' tcb\<rbrace>
     completeSignal ntfnptr tcb
   \<lbrace>\<lambda>_. invs'\<rbrace>" apply (simp add: completeSignal_def) apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) apply (rule hoare_pre) apply (wp set_ntfn_minor_invs' | wpc | simp)+ apply (rule_tac Q="\<lambda>_ s. (state_refs_of' s ntfnptr = ntfn_bound_refs' (ntfnBoundTCB ntfn))
                           \<and> ntfn_at' ntfnptr s
                           \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) s
                           \<and> ((\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' ntfnptr s)
                           \<and> ntfnptr \<noteq> ksIdleThread s"
                          in hoare_strengthen_post) apply ((wp hoare_vcg_ex_lift hoare_weak_lift_imp | wpc | simp add: valid_ntfn'_def)+)[1] apply (clarsimp simp: obj_at'_def state_refs_of'_def typ_at'_def ko_wp_at'_def  projectKOs split: option.splits) apply (blast dest: ntfn_q_refs_no_bound_refs') apply wp apply (subgoal_tac "valid_ntfn' ntfn s") apply (subgoal_tac "ntfnptr \<noteq> ksIdleThread s") apply (fastforce simp: valid_ntfn'_def valid_bound_tcb'_def projectKOs ko_at_state_refs_ofD'
                     elim: obj_at'_weakenE
                           if_live_then_nonz_capD'[OF invs_iflive'
                                                      obj_at'_real_def[THEN meta_eq_to_obj_eq,
                                                                       THEN iffD1]]) apply (fastforce simp: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs
                   dest!: invs_valid_idle') apply (fastforce dest: invs_valid_objs' ko_at_valid_objs'
                   simp: valid_obj'_def projectKOs)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' tcb\<rbrace> completeSignal ntfnptr tcb \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' tcb\<rbrace> do ntfn <- getNotification ntfnptr;
case ntfnObj ntfn of Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser tcb $ setRegister Notification_H.badgeRegister badge;
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn
od | _ \<Rightarrow> haskell_fail []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>invs' and tcb_at' tcb and ko_at' ntfn ntfnptr\<rbrace> case ntfnObj ntfn of Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser tcb $ setRegister Notification_H.badgeRegister badge;
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn
od | _ \<Rightarrow> haskell_fail [] \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. \<lbrace>?Q4 ntfn\<rbrace> case ntfnObj ntfn of Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser tcb $ setRegister Notification_H.badgeRegister badge;
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn
od | _ \<Rightarrow> haskell_fail [] \<lbrace>\<lambda>_. invs'\<rbrace>
 2. \<And>ntfn s. (invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) s \<Longrightarrow> ?Q4 ntfn s proof (prove)
goal (3 subgoals):
 1. \<And>ntfn x2. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>?P'36 ntfn x2\<rbrace> asUser tcb (setRegister Notification_H.badgeRegister x2) \<lbrace>\<lambda>rv s. obj_at' (\<lambda>ntfna. ntfn_q_refs_of' (ntfnObj ntfna) = {} \<and> ntfn_bound_refs' (ntfnBoundTCB ntfna) = ntfn_bound_refs' (ntfnBoundTCB ntfn)) ntfnptr s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) s \<and> ((\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' ntfnptr s) \<and> ntfnptr \<noteq> ksIdleThread s\<rbrace>
 2. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R20 ntfn x3\<rbrace> haskell_fail [] \<lbrace>\<lambda>_. invs'\<rbrace>
 3. \<And>ntfn s. (invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) s \<Longrightarrow> (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> invs' s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> (invs' and tcb_at' tcb) s \<and> ?P'36 ntfn x s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R20 ntfn x s) proof (prove)
goal (4 subgoals):
 1. \<And>ntfn x2. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>?P'36 ntfn x2\<rbrace> asUser tcb (setRegister Notification_H.badgeRegister x2) \<lbrace>\<lambda>_ s. state_refs_of' s ntfnptr = ntfn_bound_refs' (ntfnBoundTCB ntfn) \<and> ntfn_at' ntfnptr s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) s \<and> ((\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' ntfnptr s) \<and> ntfnptr \<noteq> ksIdleThread s\<rbrace>
 2. \<And>ntfn x2 rv s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2; state_refs_of' s ntfnptr = ntfn_bound_refs' (ntfnBoundTCB ntfn) \<and> ntfn_at' ntfnptr s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) s \<and> ((\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' ntfnptr s) \<and> ntfnptr \<noteq> ksIdleThread s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ntfna. ntfn_q_refs_of' (ntfnObj ntfna) = {} \<and> ntfn_bound_refs' (ntfnBoundTCB ntfna) = ntfn_bound_refs' (ntfnBoundTCB ntfn)) ntfnptr s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) s \<and> ((\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' ntfnptr s) \<and> ntfnptr \<noteq> ksIdleThread s
 3. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R20 ntfn x3\<rbrace> haskell_fail [] \<lbrace>\<lambda>_. invs'\<rbrace>
 4. \<And>ntfn s. (invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) s \<Longrightarrow> (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> invs' s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> (invs' and tcb_at' tcb) s \<and> ?P'36 ntfn x s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R20 ntfn x s) proof (prove)
goal (3 subgoals):
 1. \<And>ntfn x2 rv s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2; state_refs_of' s ntfnptr = ntfn_bound_refs' (ntfnBoundTCB ntfn) \<and> ntfn_at' ntfnptr s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) s \<and> ((\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' ntfnptr s) \<and> ntfnptr \<noteq> ksIdleThread s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ntfna. ntfn_q_refs_of' (ntfnObj ntfna) = {} \<and> ntfn_bound_refs' (ntfnBoundTCB ntfna) = ntfn_bound_refs' (ntfnBoundTCB ntfn)) ntfnptr s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) s \<and> ((\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' ntfnptr s) \<and> ntfnptr \<noteq> ksIdleThread s
 2. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R20 ntfn x3\<rbrace> haskell_fail [] \<lbrace>\<lambda>_. invs'\<rbrace>
 3. \<And>ntfn s. (invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) s \<Longrightarrow> (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> invs' s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> (invs' and tcb_at' tcb) s \<and> state_refs_of' s ntfnptr = ntfn_bound_refs' (ntfnBoundTCB ntfn) \<and> ntfn_at' ntfnptr s \<and> valid_bound_tcb' (ntfnBoundTCB ntfn) s \<and> ((\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' ntfnptr s) \<and> ntfnptr \<noteq> ksIdleThread s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R20 ntfn x s) proof (prove)
goal (3 subgoals):
 1. \<And>ntfn x2 s obj. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2; ksPSpace s ntfnptr = Some (KONotification obj); ntfn_q_refs_of' (ntfnObj obj) \<union> ntfn_bound_refs' (ntfnBoundTCB obj) = ntfn_bound_refs' (ntfnBoundTCB ntfn); is_aligned ntfnptr (objBitsKO (KONotification obj)); ps_clear ntfnptr (objBitsKO (KONotification obj)) s; valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) s; (\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' ntfnptr s; ntfnptr \<noteq> ksIdleThread s\<rbrakk> \<Longrightarrow> ntfn_q_refs_of' (ntfnObj obj) = {} \<and> ntfn_bound_refs' (ntfnBoundTCB obj) = ntfn_bound_refs' (ntfnBoundTCB ntfn)
 2. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R20 ntfn x3\<rbrace> haskell_fail [] \<lbrace>\<lambda>_. invs'\<rbrace>
 3. \<And>ntfn s. (invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) s \<Longrightarrow> (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> invs' s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> (invs' and tcb_at' tcb) s \<and> state_refs_of' s ntfnptr = ntfn_bound_refs' (ntfnBoundTCB ntfn) \<and> ntfn_at' ntfnptr s \<and> valid_bound_tcb' (ntfnBoundTCB ntfn) s \<and> ((\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' ntfnptr s) \<and> ntfnptr \<noteq> ksIdleThread s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R20 ntfn x s) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R20 ntfn x3\<rbrace> haskell_fail [] \<lbrace>\<lambda>_. invs'\<rbrace>
 2. \<And>ntfn s. (invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) s \<Longrightarrow> (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> invs' s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> (invs' and tcb_at' tcb) s \<and> state_refs_of' s ntfnptr = ntfn_bound_refs' (ntfnBoundTCB ntfn) \<and> ntfn_at' ntfnptr s \<and> valid_bound_tcb' (ntfnBoundTCB ntfn) s \<and> ((\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' ntfnptr s) \<and> ntfnptr \<noteq> ksIdleThread s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R20 ntfn x s) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. (invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) s \<Longrightarrow> (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> invs' s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> (invs' and tcb_at' tcb) s \<and> state_refs_of' s ntfnptr = ntfn_bound_refs' (ntfnBoundTCB ntfn) \<and> ntfn_at' ntfnptr s \<and> valid_bound_tcb' (ntfnBoundTCB ntfn) s \<and> ((\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' ntfnptr s) \<and> ntfnptr \<noteq> ksIdleThread s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> invs' s) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s. \<lbrakk>(invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) s; valid_ntfn' ntfn s\<rbrakk> \<Longrightarrow> (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> invs' s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> (invs' and tcb_at' tcb) s \<and> state_refs_of' s ntfnptr = ntfn_bound_refs' (ntfnBoundTCB ntfn) \<and> ntfn_at' ntfnptr s \<and> valid_bound_tcb' (ntfnBoundTCB ntfn) s \<and> ((\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' ntfnptr s) \<and> ntfnptr \<noteq> ksIdleThread s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> invs' s)
 2. \<And>ntfn s. (invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) s \<Longrightarrow> valid_ntfn' ntfn s proof (prove)
goal (3 subgoals):
 1. \<And>ntfn s. \<lbrakk>(invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) s; valid_ntfn' ntfn s; ntfnptr \<noteq> ksIdleThread s\<rbrakk> \<Longrightarrow> (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> invs' s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> (invs' and tcb_at' tcb) s \<and> state_refs_of' s ntfnptr = ntfn_bound_refs' (ntfnBoundTCB ntfn) \<and> ntfn_at' ntfnptr s \<and> valid_bound_tcb' (ntfnBoundTCB ntfn) s \<and> ((\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' ntfnptr s) \<and> ntfnptr \<noteq> ksIdleThread s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> invs' s)
 2. \<And>ntfn s. \<lbrakk>(invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) s; valid_ntfn' ntfn s\<rbrakk> \<Longrightarrow> ntfnptr \<noteq> ksIdleThread s
 3. \<And>ntfn s. (invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) s \<Longrightarrow> valid_ntfn' ntfn s proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s. \<lbrakk>(invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) s; valid_ntfn' ntfn s\<rbrakk> \<Longrightarrow> ntfnptr \<noteq> ksIdleThread s
 2. \<And>ntfn s. (invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) s \<Longrightarrow> valid_ntfn' ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. (invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) s \<Longrightarrow> valid_ntfn' ntfn s proof (prove)
goal:
No subgoals!