theory Dpolicy

lemma thread_bound_ntfns_transform_rev:
  "\<lbrakk> einvs s; opt_cap ptr (transform s) = Some cap; is_bound_ntfn_cap cap;
     oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; (fst ptr) \<noteq> idle_thread s \<rbrakk> \<Longrightarrow>
     thread_bound_ntfns s (fst ptr) = Some oref" apply (frule thread_bound_ntfn_cap_transform_tcb, simp) apply (case_tac ptr) apply (clarsimp simp:thread_bound_ntfns_def) apply (frule valid_etcbs_get_tcb_get_etcb[rotated], fastforce) apply (frule_tac sl=b in opt_cap_tcb, assumption, simp) apply (clarsimp split:if_split_asm) apply (case_tac "tcb"; simp add:is_thread_state_cap_def is_bound_ntfn_cap_def split:if_split_asm) apply (rename_tac arch_cap) apply (case_tac "arch_cap", simp_all split:if_split_asm) apply (clarsimp simp: infer_tcb_pending_op_def split: Structures_A.thread_state.splits) apply (case_tac "tcb_bound_notification tcb",
         auto simp: infer_tcb_pending_op_def cdl_cap_auth_conferred_def
                    infer_tcb_bound_notification_def
              split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; is_bound_ntfn_cap cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; fst ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> thread_bound_ntfns s (fst ptr) = Some oref proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; is_bound_ntfn_cap cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; fst ptr \<noteq> idle_thread s; \<exists>tcb. get_tcb (fst ptr) s = Some tcb\<rbrakk> \<Longrightarrow> thread_bound_ntfns s (fst ptr) = Some oref proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; is_bound_ntfn_cap cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; fst ptr \<noteq> idle_thread s; \<exists>tcb. get_tcb (fst ptr) s = Some tcb; ptr = (a, b)\<rbrakk> \<Longrightarrow> thread_bound_ntfns s (fst ptr) = Some oref proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; is_bound_ntfn_cap cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; a \<noteq> idle_thread s; ptr = (a, b); get_tcb a s = Some tcb; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> tcb_bound_notification tcb = Some oref proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; is_bound_ntfn_cap cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; a \<noteq> idle_thread s; ptr = (a, b); get_tcb a s = Some tcb; invs s; valid_list s; valid_sched s; \<exists>etcb. get_etcb a s = Some etcb\<rbrakk> \<Longrightarrow> tcb_bound_notification tcb = Some oref proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; is_bound_ntfn_cap cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; a \<noteq> idle_thread s; ptr = (a, b); get_tcb a s = Some tcb; invs s; valid_list s; valid_sched s; \<exists>etcb. get_etcb a s = Some etcb; opt_cap (a, b) (transform s) = (if b \<in> tcb_abstract_slots then map_option (\<lambda>(getF, uu_, uu_). transform_cap (getF tcb)) (tcb_cap_cases (tcb_cnode_index b)) else if b = tcb_pending_op_slot then Some (infer_tcb_pending_op a (tcb_state tcb)) else if b = tcb_boundntfn_slot then Some (infer_tcb_bound_notification (tcb_bound_notification tcb)) else None)\<rbrakk> \<Longrightarrow> tcb_bound_notification tcb = Some oref proof (prove)
goal (2 subgoals):
 1. \<And>a tcb etcb. \<lbrakk>is_bound_ntfn_cap (infer_tcb_pending_op a (tcb_state tcb)); oref \<in> cdl_obj_refs (infer_tcb_pending_op a (tcb_state tcb)); auth \<in> cdl_cap_auth_conferred (infer_tcb_pending_op a (tcb_state tcb)); a \<noteq> idle_thread s; ptr = (a, tcb_pending_op_slot); get_tcb a s = Some tcb; invs s; valid_list s; valid_sched s; opt_cap (a, tcb_pending_op_slot) (transform s) = Some (infer_tcb_pending_op a (tcb_state tcb)); get_etcb a s = Some etcb; tcb_pending_op_slot \<noteq> tcb_caller_slot; tcb_pending_op_slot \<noteq> tcb_cspace_slot; tcb_pending_op_slot \<noteq> tcb_replycap_slot; tcb_pending_op_slot \<noteq> tcb_vspace_slot; cap = infer_tcb_pending_op a (tcb_state tcb)\<rbrakk> \<Longrightarrow> tcb_bound_notification tcb = Some oref
 2. \<And>a tcb etcb. \<lbrakk>is_bound_ntfn_cap (infer_tcb_bound_notification (tcb_bound_notification tcb)); oref \<in> cdl_obj_refs (infer_tcb_bound_notification (tcb_bound_notification tcb)); auth \<in> cdl_cap_auth_conferred (infer_tcb_bound_notification (tcb_bound_notification tcb)); a \<noteq> idle_thread s; ptr = (a, tcb_boundntfn_slot); get_tcb a s = Some tcb; invs s; valid_list s; valid_sched s; opt_cap (a, tcb_boundntfn_slot) (transform s) = Some (infer_tcb_bound_notification (tcb_bound_notification tcb)); get_etcb a s = Some etcb; tcb_boundntfn_slot \<noteq> tcb_pending_op_slot; tcb_boundntfn_slot \<noteq> tcb_caller_slot; tcb_boundntfn_slot \<noteq> tcb_cspace_slot; tcb_boundntfn_slot \<noteq> tcb_ipcbuffer_slot; tcb_boundntfn_slot \<noteq> tcb_replycap_slot; tcb_boundntfn_slot \<noteq> tcb_vspace_slot; cap = infer_tcb_bound_notification (tcb_bound_notification tcb)\<rbrakk> \<Longrightarrow> tcb_bound_notification tcb = Some oref proof (prove)
goal (2 subgoals):
 1. \<And>a tcb etcb tcb_ctable tcb_vtable tcb_reply tcb_caller tcb_ipcframe tcb_state tcb_fault_handler tcb_ipc_buffer tcb_fault tcb_bound_notification tcb_mcpriority tcb_arch. \<lbrakk>case infer_tcb_pending_op a tcb_state of BoundNotificationCap a \<Rightarrow> True | _ \<Rightarrow> False; oref \<in> cdl_obj_refs (infer_tcb_pending_op a tcb_state); auth \<in> cdl_cap_auth_conferred (infer_tcb_pending_op a tcb_state); a \<noteq> idle_thread s; ptr = (a, tcb_pending_op_slot); get_tcb a s = Some \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>; invs s; valid_list s; valid_sched s; opt_cap (a, tcb_pending_op_slot) (transform s) = Some (infer_tcb_pending_op a tcb_state); get_etcb a s = Some etcb; tcb_pending_op_slot \<noteq> tcb_caller_slot; tcb_pending_op_slot \<noteq> tcb_cspace_slot; tcb_pending_op_slot \<noteq> tcb_replycap_slot; tcb_pending_op_slot \<noteq> tcb_vspace_slot; cap = infer_tcb_pending_op a tcb_state; tcb = \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>\<rbrakk> \<Longrightarrow> tcb_bound_notification = Some oref
 2. \<And>a tcb etcb. \<lbrakk>is_bound_ntfn_cap (infer_tcb_bound_notification (tcb_bound_notification tcb)); oref \<in> cdl_obj_refs (infer_tcb_bound_notification (tcb_bound_notification tcb)); auth \<in> cdl_cap_auth_conferred (infer_tcb_bound_notification (tcb_bound_notification tcb)); a \<noteq> idle_thread s; ptr = (a, tcb_boundntfn_slot); get_tcb a s = Some tcb; invs s; valid_list s; valid_sched s; opt_cap (a, tcb_boundntfn_slot) (transform s) = Some (infer_tcb_bound_notification (tcb_bound_notification tcb)); get_etcb a s = Some etcb; tcb_boundntfn_slot \<noteq> tcb_pending_op_slot; tcb_boundntfn_slot \<noteq> tcb_caller_slot; tcb_boundntfn_slot \<noteq> tcb_cspace_slot; tcb_boundntfn_slot \<noteq> tcb_ipcbuffer_slot; tcb_boundntfn_slot \<noteq> tcb_replycap_slot; tcb_boundntfn_slot \<noteq> tcb_vspace_slot; cap = infer_tcb_bound_notification (tcb_bound_notification tcb)\<rbrakk> \<Longrightarrow> tcb_bound_notification tcb = Some oref proof (prove)
goal (2 subgoals):
 1. \<And>a tcb etcb tcb_ctable tcb_vtable tcb_reply tcb_caller tcb_ipcframe tcb_state tcb_fault_handler tcb_ipc_buffer tcb_fault tcb_bound_notification tcb_mcpriority arch_cap. \<lbrakk>case infer_tcb_pending_op a tcb_state of BoundNotificationCap a \<Rightarrow> True | _ \<Rightarrow> False; oref \<in> cdl_obj_refs (infer_tcb_pending_op a tcb_state); auth \<in> cdl_cap_auth_conferred (infer_tcb_pending_op a tcb_state); a \<noteq> idle_thread s; ptr = (a, tcb_pending_op_slot); get_tcb a s = Some \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = arch_cap\<rparr>; invs s; valid_list s; valid_sched s; opt_cap (a, tcb_pending_op_slot) (transform s) = Some (infer_tcb_pending_op a tcb_state); get_etcb a s = Some etcb; tcb_pending_op_slot \<noteq> tcb_caller_slot; tcb_pending_op_slot \<noteq> tcb_cspace_slot; tcb_pending_op_slot \<noteq> tcb_replycap_slot; tcb_pending_op_slot \<noteq> tcb_vspace_slot; cap = infer_tcb_pending_op a tcb_state; tcb = \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = arch_cap\<rparr>\<rbrakk> \<Longrightarrow> tcb_bound_notification = Some oref
 2. \<And>a tcb etcb. \<lbrakk>is_bound_ntfn_cap (infer_tcb_bound_notification (tcb_bound_notification tcb)); oref \<in> cdl_obj_refs (infer_tcb_bound_notification (tcb_bound_notification tcb)); auth \<in> cdl_cap_auth_conferred (infer_tcb_bound_notification (tcb_bound_notification tcb)); a \<noteq> idle_thread s; ptr = (a, tcb_boundntfn_slot); get_tcb a s = Some tcb; invs s; valid_list s; valid_sched s; opt_cap (a, tcb_boundntfn_slot) (transform s) = Some (infer_tcb_bound_notification (tcb_bound_notification tcb)); get_etcb a s = Some etcb; tcb_boundntfn_slot \<noteq> tcb_pending_op_slot; tcb_boundntfn_slot \<noteq> tcb_caller_slot; tcb_boundntfn_slot \<noteq> tcb_cspace_slot; tcb_boundntfn_slot \<noteq> tcb_ipcbuffer_slot; tcb_boundntfn_slot \<noteq> tcb_replycap_slot; tcb_boundntfn_slot \<noteq> tcb_vspace_slot; cap = infer_tcb_bound_notification (tcb_bound_notification tcb)\<rbrakk> \<Longrightarrow> tcb_bound_notification tcb = Some oref proof (prove)
goal (2 subgoals):
 1. \<And>a tcb etcb tcb_ctable tcb_vtable tcb_reply tcb_caller tcb_ipcframe tcb_state tcb_fault_handler tcb_ipc_buffer tcb_fault tcb_bound_notification tcb_mcpriority arch_cap tcb_context. \<lbrakk>case infer_tcb_pending_op a tcb_state of BoundNotificationCap a \<Rightarrow> True | _ \<Rightarrow> False; oref \<in> cdl_obj_refs (infer_tcb_pending_op a tcb_state); auth \<in> cdl_cap_auth_conferred (infer_tcb_pending_op a tcb_state); a \<noteq> idle_thread s; ptr = (a, tcb_pending_op_slot); get_tcb a s = Some \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = \<lparr>tcb_context = tcb_context\<rparr>\<rparr>; invs s; valid_list s; valid_sched s; opt_cap (a, tcb_pending_op_slot) (transform s) = Some (infer_tcb_pending_op a tcb_state); get_etcb a s = Some etcb; tcb_pending_op_slot \<noteq> tcb_caller_slot; tcb_pending_op_slot \<noteq> tcb_cspace_slot; tcb_pending_op_slot \<noteq> tcb_replycap_slot; tcb_pending_op_slot \<noteq> tcb_vspace_slot; cap = infer_tcb_pending_op a tcb_state; tcb = \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = \<lparr>tcb_context = tcb_context\<rparr>\<rparr>; arch_cap = \<lparr>tcb_context = tcb_context\<rparr>\<rbrakk> \<Longrightarrow> tcb_bound_notification = Some oref
 2. \<And>a tcb etcb. \<lbrakk>is_bound_ntfn_cap (infer_tcb_bound_notification (tcb_bound_notification tcb)); oref \<in> cdl_obj_refs (infer_tcb_bound_notification (tcb_bound_notification tcb)); auth \<in> cdl_cap_auth_conferred (infer_tcb_bound_notification (tcb_bound_notification tcb)); a \<noteq> idle_thread s; ptr = (a, tcb_boundntfn_slot); get_tcb a s = Some tcb; invs s; valid_list s; valid_sched s; opt_cap (a, tcb_boundntfn_slot) (transform s) = Some (infer_tcb_bound_notification (tcb_bound_notification tcb)); get_etcb a s = Some etcb; tcb_boundntfn_slot \<noteq> tcb_pending_op_slot; tcb_boundntfn_slot \<noteq> tcb_caller_slot; tcb_boundntfn_slot \<noteq> tcb_cspace_slot; tcb_boundntfn_slot \<noteq> tcb_ipcbuffer_slot; tcb_boundntfn_slot \<noteq> tcb_replycap_slot; tcb_boundntfn_slot \<noteq> tcb_vspace_slot; cap = infer_tcb_bound_notification (tcb_bound_notification tcb)\<rbrakk> \<Longrightarrow> tcb_bound_notification tcb = Some oref proof (prove)
goal (1 subgoal):
 1. \<And>a tcb etcb. \<lbrakk>is_bound_ntfn_cap (infer_tcb_bound_notification (tcb_bound_notification tcb)); oref \<in> cdl_obj_refs (infer_tcb_bound_notification (tcb_bound_notification tcb)); auth \<in> cdl_cap_auth_conferred (infer_tcb_bound_notification (tcb_bound_notification tcb)); a \<noteq> idle_thread s; ptr = (a, tcb_boundntfn_slot); get_tcb a s = Some tcb; invs s; valid_list s; valid_sched s; opt_cap (a, tcb_boundntfn_slot) (transform s) = Some (infer_tcb_bound_notification (tcb_bound_notification tcb)); get_etcb a s = Some etcb; tcb_boundntfn_slot \<noteq> tcb_pending_op_slot; tcb_boundntfn_slot \<noteq> tcb_caller_slot; tcb_boundntfn_slot \<noteq> tcb_cspace_slot; tcb_boundntfn_slot \<noteq> tcb_ipcbuffer_slot; tcb_boundntfn_slot \<noteq> tcb_replycap_slot; tcb_boundntfn_slot \<noteq> tcb_vspace_slot; cap = infer_tcb_bound_notification (tcb_bound_notification tcb)\<rbrakk> \<Longrightarrow> tcb_bound_notification tcb = Some oref proof (prove)
goal:
No subgoals!