theory Dpolicy

lemma thread_st_auth_transform:
  "\<lbrakk> einvs s; (oref', auth) \<in> thread_st_auth s oref \<rbrakk> \<Longrightarrow>
         (oref, auth, oref') \<in> cdl_state_objs_to_policy (transform s)" apply clarify apply (simp add:thread_st_auth_def tcb_states_of_state_def) apply (cases "get_tcb oref s") apply simp+ apply (frule valid_etcbs_get_tcb_get_etcb[rotated], fastforce) apply clarsimp apply (rule_tac cap="infer_tcb_pending_op oref (tcb_state a)" in csta_caps[where ptr="(oref, 5)"
                          and auth=auth and oref=oref' and s="transform s", simplified]) apply (rule opt_cap_tcb[where sl=5, unfolded tcb_slot_defs, simplified]) apply simp apply simp apply (rule notI, drule invs_valid_idle, simp add:valid_idle_def pred_tcb_def2) apply (simp add:infer_tcb_pending_op_def, case_tac "tcb_state a";
          fastforce split:if_splits) apply (simp add:infer_tcb_pending_op_def cdl_cap_auth_conferred_def, case_tac "tcb_state a";
         fastforce split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (oref, auth, oref') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(oref', auth) \<in> thread_st_auth s oref; valid_sched s; invs s; valid_list s\<rbrakk> \<Longrightarrow> (oref, auth, oref') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(oref', auth) \<in> (case get_tcb oref s of None \<Rightarrow> {} | Some x2 \<Rightarrow> tcb_st_to_auth (tcb_state x2)); valid_sched s; invs s; valid_list s\<rbrakk> \<Longrightarrow> (oref, auth, oref') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(oref', auth) \<in> (case get_tcb oref s of None \<Rightarrow> {} | Some x2 \<Rightarrow> tcb_st_to_auth (tcb_state x2)); valid_sched s; invs s; valid_list s; get_tcb oref s = None\<rbrakk> \<Longrightarrow> (oref, auth, oref') \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>a. \<lbrakk>(oref', auth) \<in> (case get_tcb oref s of None \<Rightarrow> {} | Some x2 \<Rightarrow> tcb_st_to_auth (tcb_state x2)); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a\<rbrakk> \<Longrightarrow> (oref, auth, oref') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a\<rbrakk> \<Longrightarrow> (oref, auth, oref') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; \<exists>etcb. get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> (oref, auth, oref') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> (oref, auth, oref') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> opt_cap (oref, 5) (transform s) = Some (infer_tcb_pending_op oref (tcb_state a))
 2. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> oref' \<in> cdl_obj_refs (infer_tcb_pending_op oref (tcb_state a))
 3. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (infer_tcb_pending_op oref (tcb_state a)) proof (prove)
goal (5 subgoals):
 1. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> get_tcb oref s = Some a
 2. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> \<exists>etcb. get_etcb oref s = Some etcb
 3. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> oref \<noteq> idle_thread s
 4. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> oref' \<in> cdl_obj_refs (infer_tcb_pending_op oref (tcb_state a))
 5. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (infer_tcb_pending_op oref (tcb_state a)) proof (prove)
goal (4 subgoals):
 1. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> \<exists>etcb. get_etcb oref s = Some etcb
 2. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> oref \<noteq> idle_thread s
 3. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> oref' \<in> cdl_obj_refs (infer_tcb_pending_op oref (tcb_state a))
 4. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (infer_tcb_pending_op oref (tcb_state a)) proof (prove)
goal (3 subgoals):
 1. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> oref \<noteq> idle_thread s
 2. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> oref' \<in> cdl_obj_refs (infer_tcb_pending_op oref (tcb_state a))
 3. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (infer_tcb_pending_op oref (tcb_state a)) proof (prove)
goal (2 subgoals):
 1. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> oref' \<in> cdl_obj_refs (infer_tcb_pending_op oref (tcb_state a))
 2. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (infer_tcb_pending_op oref (tcb_state a)) proof (prove)
goal (1 subgoal):
 1. \<And>a etcb. \<lbrakk>(oref', auth) \<in> tcb_st_to_auth (tcb_state a); valid_sched s; invs s; valid_list s; get_tcb oref s = Some a; get_etcb oref s = Some etcb\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (infer_tcb_pending_op oref (tcb_state a)) proof (prove)
goal:
No subgoals!