theory Dpolicy

lemma thread_st_auth_transform_rev:
  "\<lbrakk> einvs s; opt_cap ptr (transform s) = Some cap; is_thread_state_cap cap;
     oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; (fst ptr) \<noteq> idle_thread s \<rbrakk> \<Longrightarrow>
     (oref, auth) \<in> thread_st_auth s (fst ptr)" apply (frule thread_state_cap_transform_tcb, simp) apply (case_tac ptr) apply (clarsimp simp:thread_st_auth_def tcb_states_of_state_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 "aa tcb"; simp add:is_thread_state_cap_def split:if_split_asm) apply (rename_tac arch_cap) apply (case_tac "arch_cap"; simp split:if_split_asm) apply (case_tac "tcb_state tcb";
          fastforce simp:cdl_cap_auth_conferred_def split:option.splits if_splits) apply (fastforce simp:is_thread_state_cap_def infer_tcb_pending_op_def
                        infer_tcb_bound_notification_def
                   split:option.splits if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; is_thread_state_cap cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; fst ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (oref, auth) \<in> thread_st_auth s (fst ptr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; is_thread_state_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> (oref, auth) \<in> thread_st_auth s (fst ptr) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; is_thread_state_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> (oref, auth) \<in> thread_st_auth s (fst ptr) proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; is_thread_state_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> (oref, auth) \<in> tcb_st_to_auth (tcb_state tcb) proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; is_thread_state_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> (oref, auth) \<in> tcb_st_to_auth (tcb_state tcb) proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; is_thread_state_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> (oref, auth) \<in> tcb_st_to_auth (tcb_state tcb) proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb etcb aa ab ba. \<lbrakk>is_thread_state_cap (transform_cap (aa tcb)); oref \<in> cdl_obj_refs (transform_cap (aa tcb)); auth \<in> cdl_cap_auth_conferred (transform_cap (aa tcb)); a \<noteq> idle_thread s; ptr = (a, b); get_tcb a s = Some tcb; invs s; valid_list s; valid_sched s; opt_cap (a, b) (transform s) = Some (transform_cap (aa tcb)); b = tcb_caller_slot \<or> b = tcb_cspace_slot \<or> b = tcb_ipcbuffer_slot \<or> b = tcb_replycap_slot \<or> b = tcb_vspace_slot; get_etcb a s = Some etcb; cap = transform_cap (aa tcb); tcb_cap_cases (tcb_cnode_index b) = Some (aa, ab, ba)\<rbrakk> \<Longrightarrow> (oref, auth) \<in> tcb_st_to_auth (tcb_state tcb)
 2. \<And>a tcb etcb. \<lbrakk>is_thread_state_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> (oref, auth) \<in> tcb_st_to_auth (tcb_state tcb)
 3. \<And>a tcb etcb. \<lbrakk>is_thread_state_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> (oref, auth) \<in> tcb_st_to_auth (tcb_state tcb) proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb etcb aa ab ba x12. \<lbrakk>case transform_cap (ArchObjectCap x12) of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; oref \<in> cdl_obj_refs (transform_cap (ArchObjectCap x12)); auth \<in> cdl_cap_auth_conferred (transform_cap (ArchObjectCap x12)); a \<noteq> idle_thread s; ptr = (a, b); get_tcb a s = Some tcb; invs s; valid_list s; valid_sched s; opt_cap (a, b) (transform s) = Some (transform_cap (ArchObjectCap x12)); b = tcb_caller_slot \<or> b = tcb_cspace_slot \<or> b = tcb_ipcbuffer_slot \<or> b = tcb_replycap_slot \<or> b = tcb_vspace_slot; get_etcb a s = Some etcb; cap = transform_cap (ArchObjectCap x12); tcb_cap_cases (tcb_cnode_index b) = Some (aa, ab, ba); aa tcb = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (oref, auth) \<in> tcb_st_to_auth (tcb_state tcb)
 2. \<And>a tcb etcb. \<lbrakk>is_thread_state_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> (oref, auth) \<in> tcb_st_to_auth (tcb_state tcb)
 3. \<And>a tcb etcb. \<lbrakk>is_thread_state_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> (oref, auth) \<in> tcb_st_to_auth (tcb_state tcb) proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb etcb aa ab ba arch_cap. \<lbrakk>case transform_cap (ArchObjectCap arch_cap) of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; oref \<in> cdl_obj_refs (transform_cap (ArchObjectCap arch_cap)); auth \<in> cdl_cap_auth_conferred (transform_cap (ArchObjectCap arch_cap)); a \<noteq> idle_thread s; ptr = (a, b); get_tcb a s = Some tcb; invs s; valid_list s; valid_sched s; opt_cap (a, b) (transform s) = Some (transform_cap (ArchObjectCap arch_cap)); b = tcb_caller_slot \<or> b = tcb_cspace_slot \<or> b = tcb_ipcbuffer_slot \<or> b = tcb_replycap_slot \<or> b = tcb_vspace_slot; get_etcb a s = Some etcb; cap = transform_cap (ArchObjectCap arch_cap); tcb_cap_cases (tcb_cnode_index b) = Some (aa, ab, ba); aa tcb = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> (oref, auth) \<in> tcb_st_to_auth (tcb_state tcb)
 2. \<And>a tcb etcb. \<lbrakk>is_thread_state_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> (oref, auth) \<in> tcb_st_to_auth (tcb_state tcb)
 3. \<And>a tcb etcb. \<lbrakk>is_thread_state_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> (oref, auth) \<in> tcb_st_to_auth (tcb_state tcb) proof (prove)
goal (2 subgoals):
 1. \<And>a tcb etcb. \<lbrakk>is_thread_state_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> (oref, auth) \<in> tcb_st_to_auth (tcb_state tcb)
 2. \<And>a tcb etcb. \<lbrakk>is_thread_state_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> (oref, auth) \<in> tcb_st_to_auth (tcb_state tcb) proof (prove)
goal (1 subgoal):
 1. \<And>a tcb etcb. \<lbrakk>is_thread_state_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> (oref, auth) \<in> tcb_st_to_auth (tcb_state tcb) proof (prove)
goal:
No subgoals!