theory Detype_C

lemma cnotification_relation_restrict:
  assumes vuc: "s \<turnstile>' capability.UntypedCap d ptr bits idx"
  and    invs: "invs' s"
  and      rl: "\<forall>(p :: word32) P. ko_wp_at' P p s \<and> (\<forall>ko. P ko \<longrightarrow> live' ko) \<longrightarrow> p \<notin> {ptr..ptr + 2 ^ bits - 1}"
  and    meps: "map_to_ntfns (ksPSpace s) p = Some ntfn"
  shows "cnotification_relation (cslift s' |` (- Ptr ` {ptr..+2 ^ bits})) ntfn b = cnotification_relation (cslift s') ntfn b" proof - from invs have "valid_objs' s" .. with meps have vep: "valid_ntfn' ntfn s" apply - apply (clarsimp simp add: map_comp_Some_iff projectKOs) apply (erule (1) valid_objsE') apply (simp add: valid_obj'_def) done from meps have koat: "ko_at' ntfn p s" by (rule map_to_ko_atI') fact+ show ?thesis proof (cases "ntfnObj ntfn") case (WaitingNtfn ts) with vep have tats: "\<forall>t \<in> set ts. tcb_at' t s" by (simp add: valid_ntfn'_def) have tlive: "\<forall>t\<in>set ts. ko_wp_at' live' t s" using WaitingNtfn invs koat apply - apply (drule (1) ntfn_queue_live) apply simp done show ?thesis using WaitingNtfn unfolding cnotification_relation_def Let_def by (simp add: tcb_queue_relation_live_restrict [OF vuc tats tlive rl]) qed (simp_all add: cnotification_relation_def Let_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b proof (state)
goal (1 subgoal):
 1. cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b proof (chain)
picking this:
invs' s proof (prove)
using this:
invs' s

goal (1 subgoal):
 1. valid_objs' s proof (state)
this:
valid_objs' s

goal (1 subgoal):
 1. cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b proof (chain)
picking this:
map_to_ntfns (ksPSpace s) p = Some ntfn
valid_objs' s proof (prove)
using this:
map_to_ntfns (ksPSpace s) p = Some ntfn
valid_objs' s

goal (1 subgoal):
 1. valid_ntfn' ntfn s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map_to_ntfns (ksPSpace s) p = Some ntfn; valid_objs' s\<rbrakk> \<Longrightarrow> valid_ntfn' ntfn s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some (KONotification ntfn); valid_objs' s\<rbrakk> \<Longrightarrow> valid_ntfn' ntfn s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some (KONotification ntfn); valid_obj' (KONotification ntfn) s\<rbrakk> \<Longrightarrow> valid_ntfn' ntfn s proof (prove)
goal:
No subgoals! proof (state)
this:
valid_ntfn' ntfn s

goal (1 subgoal):
 1. cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b proof (chain)
picking this:
map_to_ntfns (ksPSpace s) p = Some ntfn proof (prove)
using this:
map_to_ntfns (ksPSpace s) p = Some ntfn

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

goal (1 subgoal):
 1. cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b proof (prove)
goal (1 subgoal):
 1. cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b proof (state)
goal (3 subgoals):
 1. ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<Longrightarrow> cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b
 2. \<And>x2. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b
 3. \<And>x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b proof (state)
this:
ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts

goal (3 subgoals):
 1. ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<Longrightarrow> cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b
 2. \<And>x2. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b
 3. \<And>x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b proof (chain)
picking this:
valid_ntfn' ntfn s
ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts proof (prove)
using this:
valid_ntfn' ntfn s
ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts

goal (1 subgoal):
 1. \<forall>t\<in>set ts. tcb_at' t s proof (state)
this:
\<forall>t\<in>set ts. tcb_at' t s

goal (3 subgoals):
 1. ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<Longrightarrow> cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b
 2. \<And>x2. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b
 3. \<And>x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>set ts. ko_wp_at' live' t s proof (prove)
using this:
ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts
invs' s
ko_at' ntfn p s

goal (1 subgoal):
 1. \<forall>t\<in>set ts. ko_wp_at' live' t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts; invs' s; ko_at' ntfn p s\<rbrakk> \<Longrightarrow> \<forall>t\<in>set ts. ko_wp_at' live' t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts; ko_at' ntfn p s; \<forall>t\<in>set (ntfnQ (ntfnObj ntfn)). ko_wp_at' live' t s\<rbrakk> \<Longrightarrow> \<forall>t\<in>set ts. ko_wp_at' live' t s proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>t\<in>set ts. ko_wp_at' live' t s

goal (3 subgoals):
 1. ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<Longrightarrow> cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b
 2. \<And>x2. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b
 3. \<And>x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b proof (prove)
goal (1 subgoal):
 1. cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b proof (prove)
using this:
ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts

goal (1 subgoal):
 1. cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b proof (prove)
using this:
ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts

goal (1 subgoal):
 1. ((case ntfnObj ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) [] ((tcb_Ptr \<circ> ntfnQueue_head_CL) (notification_lift b)) ((tcb_Ptr \<circ> ntfnQueue_tail_CL) (notification_lift b)) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) [] ((tcb_Ptr \<circ> ntfnQueue_head_CL) (notification_lift b)) ((tcb_Ptr \<circ> ntfnQueue_tail_CL) (notification_lift b)) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) q ((tcb_Ptr \<circ> ntfnQueue_head_CL) (notification_lift b)) ((tcb_Ptr \<circ> ntfnQueue_tail_CL) (notification_lift b))) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn) = (tcb_Ptr \<circ> ntfnBoundTCB_CL) (notification_lift b)) = ((case ntfnObj ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift s') [] ((tcb_Ptr \<circ> ntfnQueue_head_CL) (notification_lift b)) ((tcb_Ptr \<circ> ntfnQueue_tail_CL) (notification_lift b)) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift s') [] ((tcb_Ptr \<circ> ntfnQueue_head_CL) (notification_lift b)) ((tcb_Ptr \<circ> ntfnQueue_tail_CL) (notification_lift b)) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift s') q ((tcb_Ptr \<circ> ntfnQueue_head_CL) (notification_lift b)) ((tcb_Ptr \<circ> ntfnQueue_tail_CL) (notification_lift b))) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn) = (tcb_Ptr \<circ> ntfnBoundTCB_CL) (notification_lift b)) proof (state)
this:
cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b

goal (2 subgoals):
 1. ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<Longrightarrow> cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b
 2. \<And>x2. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b proof (state)
this:
cnotification_relation (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) ntfn b = cnotification_relation (cslift s') ntfn b

goal:
No subgoals!