theory Fastpath_C

lemma obj_at_bound_tcb_grandD:
  "\<lbrakk> obj_at' P t s; valid_objs' s; no_0_obj' s; (s, s') \<in> rf_sr \<rbrakk>
    \<Longrightarrow> \<exists>tcb tcb' ntfn ntfn'. ko_at' tcb t s \<and> P tcb
       \<and> cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'
       \<and> ctcb_relation tcb tcb'
       \<and> ((tcbBoundNotification_C tcb' = NULL) = (tcbBoundNotification tcb = None))
       \<and> (tcbBoundNotification tcb \<noteq> None \<longrightarrow> ko_at' ntfn (the (tcbBoundNotification tcb)) s)
       \<and> (tcbBoundNotification tcb \<noteq> None \<longrightarrow> cslift s' (tcbBoundNotification_C tcb') = Some ntfn')
       \<and> (tcbBoundNotification tcb \<noteq> None \<longrightarrow> cnotification_relation (cslift s') ntfn ntfn')" apply (clarsimp simp: pred_tcb_at'_def) apply (drule(1) obj_at_cslift_tcb, clarsimp) apply (rule exI, rule conjI, assumption) apply (clarsimp simp: ctcb_relation_def
                                 option_to_ptr_def option_to_0_def) apply (simp add: return_def split: option.split_asm) apply (drule_tac s="ntfn_Ptr x"for x in sym) apply (drule(1) ko_at_valid_objs', clarsimp simp: projectKOs) apply (clarsimp simp: projectKOs valid_obj'_def valid_tcb'_def) apply (drule obj_at_ko_at', clarsimp) apply (rule conjI, clarsimp) apply (rule cmap_relationE1[OF cmap_relation_ntfn], assumption, erule ko_at_projectKO_opt) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' P t s; valid_objs' s; no_0_obj' s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>tcb tcb' ntfn ntfn'. ko_at' tcb t s \<and> P tcb \<and> cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb' \<and> ctcb_relation tcb tcb' \<and> (tcbBoundNotification_C tcb' = NULL) = (tcbBoundNotification tcb = None) \<and> (tcbBoundNotification tcb \<noteq> None \<longrightarrow> ko_at' ntfn (the (tcbBoundNotification tcb)) s) \<and> (tcbBoundNotification tcb \<noteq> None \<longrightarrow> cslift s' (tcbBoundNotification_C tcb') = Some ntfn') \<and> (tcbBoundNotification tcb \<noteq> None \<longrightarrow> cnotification_relation (cslift s') ntfn ntfn') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' P t s; valid_objs' s; no_0_obj' s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>tcb. ko_at' tcb t s \<and> P tcb \<and> (\<exists>tcb'. cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb' \<and> ctcb_relation tcb tcb' \<and> (tcbBoundNotification_C tcb' = NULL) = (tcbBoundNotification tcb = None) \<and> (\<exists>ntfn. ((\<exists>y. tcbBoundNotification tcb = Some y) \<longrightarrow> ko_at' ntfn (the (tcbBoundNotification tcb)) s) \<and> (\<exists>ntfn'. ((\<exists>y. tcbBoundNotification tcb = Some y) \<longrightarrow> cslift s' (tcbBoundNotification_C tcb') = Some ntfn') \<and> ((\<exists>y. tcbBoundNotification tcb = Some y) \<longrightarrow> cnotification_relation (cslift s') ntfn ntfn')))) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>valid_objs' s; no_0_obj' s; (s, s') \<in> rf_sr; ko_at' ko t s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> \<exists>tcb. ko_at' tcb t s \<and> P tcb \<and> ctcb_relation tcb ko' \<and> (tcbBoundNotification_C ko' = NULL) = (tcbBoundNotification tcb = None) \<and> (\<exists>ntfn. ((\<exists>y. tcbBoundNotification tcb = Some y) \<longrightarrow> ko_at' ntfn (the (tcbBoundNotification tcb)) s) \<and> (\<exists>ntfn'. ((\<exists>y. tcbBoundNotification tcb = Some y) \<longrightarrow> cslift s' (tcbBoundNotification_C ko') = Some ntfn') \<and> ((\<exists>y. tcbBoundNotification tcb = Some y) \<longrightarrow> cnotification_relation (cslift s') ntfn ntfn'))) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>valid_objs' s; no_0_obj' s; (s, s') \<in> rf_sr; ko_at' ko t s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> P ko \<and> ctcb_relation ko ko' \<and> (tcbBoundNotification_C ko' = NULL) = (tcbBoundNotification ko = None) \<and> (\<exists>ntfn. ((\<exists>y. tcbBoundNotification ko = Some y) \<longrightarrow> ko_at' ntfn (the (tcbBoundNotification ko)) s) \<and> (\<exists>ntfn'. ((\<exists>y. tcbBoundNotification ko = Some y) \<longrightarrow> cslift s' (tcbBoundNotification_C ko') = Some ntfn') \<and> ((\<exists>y. tcbBoundNotification ko = Some y) \<longrightarrow> cnotification_relation (cslift s') ntfn ntfn'))) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>valid_objs' s; no_0_obj' s; (s, s') \<in> rf_sr; ko_at' ko t s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some ko'; tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); ntfn_Ptr (case tcbBoundNotification ko of None \<Rightarrow> 0 | Some y \<Rightarrow> y) = tcbBoundNotification_C ko'\<rbrakk> \<Longrightarrow> (tcbBoundNotification_C ko' = NULL) = (tcbBoundNotification ko = None) \<and> (\<exists>ntfn. ((\<exists>y. tcbBoundNotification ko = Some y) \<longrightarrow> ko_at' ntfn (the (tcbBoundNotification ko)) s) \<and> (\<exists>ntfn'. ((\<exists>y. tcbBoundNotification ko = Some y) \<longrightarrow> cslift s' (tcbBoundNotification_C ko') = Some ntfn') \<and> ((\<exists>y. tcbBoundNotification ko = Some y) \<longrightarrow> cnotification_relation (cslift s') ntfn ntfn'))) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko' x2. \<lbrakk>valid_objs' s; no_0_obj' s; (s, s') \<in> rf_sr; ko_at' ko t s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some ko'; tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); tcbBoundNotification ko = Some x2; ntfn_Ptr x2 = tcbBoundNotification_C ko'\<rbrakk> \<Longrightarrow> tcbBoundNotification_C ko' \<noteq> NULL \<and> (\<exists>ntfn. ko_at' ntfn x2 s \<and> (\<exists>ntfn'. cslift s' (tcbBoundNotification_C ko') = Some ntfn' \<and> cnotification_relation (cslift s') ntfn ntfn')) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko' x2. \<lbrakk>valid_objs' s; no_0_obj' s; (s, s') \<in> rf_sr; ko_at' ko t s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some ko'; tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); tcbBoundNotification ko = Some x2; tcbBoundNotification_C ko' = ntfn_Ptr x2\<rbrakk> \<Longrightarrow> tcbBoundNotification_C ko' \<noteq> NULL \<and> (\<exists>ntfn. ko_at' ntfn x2 s \<and> (\<exists>ntfn'. cslift s' (tcbBoundNotification_C ko') = Some ntfn' \<and> cnotification_relation (cslift s') ntfn ntfn')) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko' x2. \<lbrakk>valid_objs' s; no_0_obj' s; (s, s') \<in> rf_sr; P ko; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some ko'; tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); tcbBoundNotification ko = Some x2; tcbBoundNotification_C ko' = ntfn_Ptr x2; valid_obj' (injectKOS ko) s\<rbrakk> \<Longrightarrow> tcbBoundNotification_C ko' \<noteq> NULL \<and> (\<exists>ntfn. ko_at' ntfn x2 s \<and> (\<exists>ntfn'. cslift s' (tcbBoundNotification_C ko') = Some ntfn' \<and> cnotification_relation (cslift s') ntfn ntfn')) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko' x2. \<lbrakk>valid_objs' s; no_0_obj' s; (s, s') \<in> rf_sr; P ko; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some ko'; tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); tcbBoundNotification ko = Some x2; tcbBoundNotification_C ko' = ntfn_Ptr x2; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF ko)) s; valid_tcb_state' (tcbState ko) s; is_aligned (tcbIPCBuffer_C ko') msg_align_bits; ntfn_at' x2 s; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority\<rbrakk> \<Longrightarrow> x2 \<noteq> 0 \<and> (\<exists>ntfn. ko_at' ntfn x2 s \<and> (\<exists>ntfn'. cslift s' (ntfn_Ptr x2) = Some ntfn' \<and> cnotification_relation (cslift s') ntfn ntfn')) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko' x2 koa. \<lbrakk>valid_objs' s; no_0_obj' s; (s, s') \<in> rf_sr; P ko; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some ko'; tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); tcbBoundNotification ko = Some x2; tcbBoundNotification_C ko' = ntfn_Ptr x2; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF ko)) s; valid_tcb_state' (tcbState ko) s; is_aligned (tcbIPCBuffer_C ko') msg_align_bits; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; ko_at' koa x2 s\<rbrakk> \<Longrightarrow> x2 \<noteq> 0 \<and> (\<exists>ntfn. ko_at' ntfn x2 s \<and> (\<exists>ntfn'. cslift s' (ntfn_Ptr x2) = Some ntfn' \<and> cnotification_relation (cslift s') ntfn ntfn')) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko' x2 koa. \<lbrakk>valid_objs' s; no_0_obj' s; (s, s') \<in> rf_sr; P ko; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some ko'; tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); tcbBoundNotification ko = Some x2; tcbBoundNotification_C ko' = ntfn_Ptr x2; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF ko)) s; valid_tcb_state' (tcbState ko) s; is_aligned (tcbIPCBuffer_C ko') msg_align_bits; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; ko_at' koa x2 s\<rbrakk> \<Longrightarrow> \<exists>ntfn. ko_at' ntfn x2 s \<and> (\<exists>ntfn'. cslift s' (ntfn_Ptr x2) = Some ntfn' \<and> cnotification_relation (cslift s') ntfn ntfn') proof (prove)
goal (1 subgoal):
 1. \<And>ko ko' x2 koa y'. \<lbrakk>valid_objs' s; no_0_obj' s; (s, s') \<in> rf_sr; P ko; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some ko'; tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); tcbBoundNotification ko = Some x2; tcbBoundNotification_C ko' = ntfn_Ptr x2; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF ko)) s; valid_tcb_state' (tcbState ko) s; is_aligned (tcbIPCBuffer_C ko') msg_align_bits; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; ko_at' koa x2 s; map_to_ntfns (ksPSpace s) x2 = Some koa; cnotification_relation (cslift s') koa y'; cslift s' (ntfn_Ptr x2) = Some y'\<rbrakk> \<Longrightarrow> \<exists>ntfn. ko_at' ntfn x2 s \<and> (\<exists>ntfn'. cslift s' (ntfn_Ptr x2) = Some ntfn' \<and> cnotification_relation (cslift s') ntfn ntfn') proof (prove)
goal:
No subgoals!