theory Ipc_C

lemma cpspace_relation_ntfn_update_ntfn':
  fixes ntfn :: "Structures_H.notification" and ntfn' :: "Structures_H.notification"
    and ntfnptr :: "word32" and s :: "kernel_state"
  defines "qs \<equiv> if isWaitingNtfn (ntfnObj ntfn') then set (ntfnQueue (ntfnObj ntfn')) else {}"
  defines "s' \<equiv> s\<lparr>ksPSpace := (ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn')\<rparr>"
  assumes koat: "ko_at' ntfn ntfnptr s"
  and       vp: "valid_pspace' s"
  and      cp: "cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) Ptr (cnotification_relation (cslift t))"
  and      srs: "sym_refs (state_refs_of' s')"
  and     rel: "cnotification_relation (cslift t') ntfn' notification"
  and    mpeq: "(cslift t' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (cslift t |` (- (tcb_ptr_to_ctcb_ptr ` qs)))"
  shows "cmap_relation (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn')))
                       ((cslift t)(Ptr ntfnptr \<mapsto> notification))
                       Ptr
                       (cnotification_relation (cslift t'))" proof - from koat have koat': "ko_at' ntfn' ntfnptr s'" by (clarsimp simp: obj_at'_def s'_def objBitsKO_def ps_clear_def projectKOs) have ntfns':
    "\<And>x. x \<noteq> ntfnptr \<Longrightarrow> map_to_ntfns (ksPSpace s) x =
                         map_to_ntfns (ksPSpace s') x" unfolding s'_def by (fastforce intro: ssubst [OF map_comp_update] simp: projectKO_opt_ntfn) from koat have map_to_ko_atI'':
    "\<And>x y. \<lbrakk> x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some y \<rbrakk> \<Longrightarrow> ko_at' y x s'" using vp unfolding s'_def by (simp add: map_to_ko_at_updI' injectKO_ntfn objBitsKO_def) thus ?thesis using vp srs cp rel mpeq unfolding cmap_relation_def apply - apply (elim conjE) apply (clarsimp elim!: obj_atE' simp: map_comp_update projectKO_opts_defs
                   split: if_split) apply (drule (1) bspec [OF _ domI]) apply simp apply (erule(1) cnotification_relation_ntfn_queue [OF _ _ koat']) apply (erule(1) map_to_ko_atI'') apply (fold qs_def, rule mpeq) apply assumption done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmap_relation (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))) ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift t')) proof (state)
goal (1 subgoal):
 1. cmap_relation (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))) ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift t')) proof (chain)
picking this:
ko_at' ntfn ntfnptr s proof (prove)
using this:
ko_at' ntfn ntfnptr s

goal (1 subgoal):
 1. ko_at' ntfn' ntfnptr s' proof (state)
this:
ko_at' ntfn' ntfnptr s'

goal (1 subgoal):
 1. cmap_relation (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))) ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift t')) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<noteq> ntfnptr \<Longrightarrow> map_to_ntfns (ksPSpace s) x = map_to_ntfns (ksPSpace s') x proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<noteq> ntfnptr \<Longrightarrow> map_to_ntfns (ksPSpace s) x = map_to_ntfns (ksPSpace (s\<lparr>ksPSpace := (ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn')\<rparr>)) x proof (state)
this:
?x1 \<noteq> ntfnptr \<Longrightarrow> map_to_ntfns (ksPSpace s) ?x1 = map_to_ntfns (ksPSpace s') ?x1

goal (1 subgoal):
 1. cmap_relation (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))) ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift t')) proof (chain)
picking this:
ko_at' ntfn ntfnptr s proof (prove)
using this:
ko_at' ntfn ntfnptr s

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some y\<rbrakk> \<Longrightarrow> ko_at' y x s' proof (prove)
using this:
ko_at' ntfn ntfnptr s
valid_pspace' s

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some y\<rbrakk> \<Longrightarrow> ko_at' y x s' proof (prove)
using this:
ko_at' ntfn ntfnptr s
valid_pspace' s

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some y\<rbrakk> \<Longrightarrow> ko_at' y x (s\<lparr>ksPSpace := (ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn')\<rparr>) proof (state)
this:
\<lbrakk>?x1 \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) ?x1 = Some ?y1\<rbrakk> \<Longrightarrow> ko_at' ?y1 ?x1 s'

goal (1 subgoal):
 1. cmap_relation (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))) ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift t')) proof (prove)
using this:
\<lbrakk>?x1 \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) ?x1 = Some ?y1\<rbrakk> \<Longrightarrow> ko_at' ?y1 ?x1 s'

goal (1 subgoal):
 1. cmap_relation (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))) ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift t')) proof (prove)
using this:
\<lbrakk>?x1 \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) ?x1 = Some ?y1\<rbrakk> \<Longrightarrow> ko_at' ?y1 ?x1 s'
valid_pspace' s
sym_refs (state_refs_of' s')
cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t))
cnotification_relation (cslift t') ntfn' notification
cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>

goal (1 subgoal):
 1. cmap_relation (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))) ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift t')) proof (prove)
using this:
\<lbrakk>?x1 \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) ?x1 = Some ?y1\<rbrakk> \<Longrightarrow> ko_at' ?y1 ?x1 s'
valid_pspace' s
sym_refs (state_refs_of' s')
ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (cslift t) \<and> (\<forall>x\<in>dom (map_to_ntfns (ksPSpace s)). cnotification_relation (cslift t) (the (map_to_ntfns (ksPSpace s) x)) (the (cslift t (ntfn_Ptr x))))
cnotification_relation (cslift t') ntfn' notification
cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>

goal (1 subgoal):
 1. ntfn_Ptr ` dom (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))) = dom ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) \<and> (\<forall>x\<in>dom (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))). cnotification_relation (cslift t') (the (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn')) x)) (the (((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) (ntfn_Ptr x)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x y. \<lbrakk>x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some y\<rbrakk> \<Longrightarrow> ko_at' y x s'; valid_pspace' s; sym_refs (state_refs_of' s'); ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (cslift t) \<and> (\<forall>x\<in>dom (map_to_ntfns (ksPSpace s)). cnotification_relation (cslift t) (the (map_to_ntfns (ksPSpace s) x)) (the (cslift t (ntfn_Ptr x)))); cnotification_relation (cslift t') ntfn' notification; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>\<rbrakk> \<Longrightarrow> ntfn_Ptr ` dom (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))) = dom ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) \<and> (\<forall>x\<in>dom (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))). cnotification_relation (cslift t') (the (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn')) x)) (the (((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) (ntfn_Ptr x)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x y. \<lbrakk>x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some y\<rbrakk> \<Longrightarrow> ko_at' y x s'; valid_pspace' s; sym_refs (state_refs_of' s'); cnotification_relation (cslift t') ntfn' notification; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (cslift t); \<forall>x\<in>dom (map_to_ntfns (ksPSpace s)). cnotification_relation (cslift t) (the (map_to_ntfns (ksPSpace s) x)) (the (cslift t (ntfn_Ptr x)))\<rbrakk> \<Longrightarrow> ntfn_Ptr ` dom (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))) = dom ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) \<and> (\<forall>x\<in>dom (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))). cnotification_relation (cslift t') (the (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn')) x)) (the (((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) (ntfn_Ptr x)))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<And>x y. \<lbrakk>x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some y\<rbrakk> \<Longrightarrow> ko_at' y x s'; valid_pspace' s; sym_refs (state_refs_of' s'); cnotification_relation (cslift t') ntfn' notification; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (cslift t); \<forall>x\<in>dom (map_to_ntfns (ksPSpace s)). cnotification_relation (cslift t) (the (map_to_ntfns (ksPSpace s) x)) (the (cslift t (ntfn_Ptr x))); map_to_ntfns (ksPSpace s) x = Some y; x \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> cnotification_relation (cslift t') y (the (cslift t (ntfn_Ptr x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<And>x y. \<lbrakk>x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some y\<rbrakk> \<Longrightarrow> ko_at' y x s'; valid_pspace' s; sym_refs (state_refs_of' s'); cnotification_relation (cslift t') ntfn' notification; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (cslift t); map_to_ntfns (ksPSpace s) x = Some y; x \<noteq> ntfnptr; cnotification_relation (cslift t) (the (map_to_ntfns (ksPSpace s) x)) (the (cslift t (ntfn_Ptr x)))\<rbrakk> \<Longrightarrow> cnotification_relation (cslift t') y (the (cslift t (ntfn_Ptr x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<And>x y. \<lbrakk>x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some y\<rbrakk> \<Longrightarrow> ko_at' y x s'; valid_pspace' s; sym_refs (state_refs_of' s'); cnotification_relation (cslift t') ntfn' notification; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (cslift t); map_to_ntfns (ksPSpace s) x = Some y; x \<noteq> ntfnptr; cnotification_relation (cslift t) y (the (cslift t (ntfn_Ptr x)))\<rbrakk> \<Longrightarrow> cnotification_relation (cslift t') y (the (cslift t (ntfn_Ptr x))) proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>\<And>x y. \<lbrakk>x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some y\<rbrakk> \<Longrightarrow> ko_at' y x s'; valid_pspace' s; sym_refs (state_refs_of' s'); cnotification_relation (cslift t') ntfn' notification; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (cslift t); map_to_ntfns (ksPSpace s) x = Some y; x \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> ko_at' y (?ntfnptr'25 x y) s'
 2. \<And>x y. \<lbrakk>\<And>x y. \<lbrakk>x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some y\<rbrakk> \<Longrightarrow> ko_at' y x s'; valid_pspace' s; sym_refs (state_refs_of' s'); cnotification_relation (cslift t') ntfn' notification; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (cslift t); map_to_ntfns (ksPSpace s) x = Some y; x \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn') then set (ntfnQueue (ntfnObj ntfn')) else {}))\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn') then set (ntfnQueue (ntfnObj ntfn')) else {}))\<^esub>
 3. \<And>x y. \<lbrakk>\<And>x y. \<lbrakk>x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some y\<rbrakk> \<Longrightarrow> ko_at' y x s'; valid_pspace' s; sym_refs (state_refs_of' s'); cnotification_relation (cslift t') ntfn' notification; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (cslift t); map_to_ntfns (ksPSpace s) x = Some y; x \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> ?ntfnptr'25 x y \<noteq> ntfnptr proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<And>x y. \<lbrakk>x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some y\<rbrakk> \<Longrightarrow> ko_at' y x s'; valid_pspace' s; sym_refs (state_refs_of' s'); cnotification_relation (cslift t') ntfn' notification; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (cslift t); map_to_ntfns (ksPSpace s) x = Some y; x \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn') then set (ntfnQueue (ntfnObj ntfn')) else {}))\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn') then set (ntfnQueue (ntfnObj ntfn')) else {}))\<^esub>
 2. \<And>x y. \<lbrakk>\<And>x y. \<lbrakk>x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some y\<rbrakk> \<Longrightarrow> ko_at' y x s'; valid_pspace' s; sym_refs (state_refs_of' s'); cnotification_relation (cslift t') ntfn' notification; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (cslift t); map_to_ntfns (ksPSpace s) x = Some y; x \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> x \<noteq> ntfnptr proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<And>x y. \<lbrakk>x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some y\<rbrakk> \<Longrightarrow> ko_at' y x s'; valid_pspace' s; sym_refs (state_refs_of' s'); cnotification_relation (cslift t') ntfn' notification; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (cslift t); map_to_ntfns (ksPSpace s) x = Some y; x \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> x \<noteq> ntfnptr proof (prove)
goal:
No subgoals! proof (state)
this:
cmap_relation (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))) ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift t'))

goal:
No subgoals!