theory Access_AC

lemma trm_ipc':
  "\<lbrakk> pas_refined aag s; valid_objs s; case_option False can_receive_ipc (tcb_states_of_state s p');
     (tcb_states_of_state s' p') = Some Structures_A.Running; p \<in> auth_ipc_buffers s p' \<rbrakk>
     \<Longrightarrow> integrity_mem aag subjects p (tcb_states_of_state s) (tcb_states_of_state s')
                      (auth_ipc_buffers s) X
                      (underlying_memory (machine_state s) p)
                      (underlying_memory (machine_state s') p)" apply (cases "pasObjectAbs aag p' \<in> subjects") apply (rule trm_write) apply (clarsimp simp: ) apply (frule pas_refined_mem[rotated]) prefer 3 apply (rule trm_ipc; fastforce) prefer 2 apply (rule bexI) apply assumption apply assumption apply (drule (1) auth_ipc_buffers_member) apply clarsimp apply (drule (1) sta_caps[where cap="ArchObjectCap acap" for acap, simplified]) apply (auto simp: cap_auth_conferred_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'\<rbrakk> \<Longrightarrow> integrity_mem aag subjects p (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) p) (underlying_memory (machine_state s') p) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects p (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) p) (underlying_memory (machine_state s') p)
 2. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects p (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) p) (underlying_memory (machine_state s') p) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to subjects aag Write p
 2. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects p (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) p) (underlying_memory (machine_state s') p) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to subjects aag Write p
 2. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects p (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) p) (underlying_memory (machine_state s') p) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects\<rbrakk> \<Longrightarrow> (?x6, ?auth6, ?y6) \<in> state_objs_to_policy s
 2. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects; (pasObjectAbs aag ?x6, ?auth6, pasObjectAbs aag ?y6) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to subjects aag Write p
 3. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects p (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) p) (underlying_memory (machine_state s') p) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects p (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) p) (underlying_memory (machine_state s') p)
 2. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects\<rbrakk> \<Longrightarrow> (?x6, ?auth6, ?y6) \<in> state_objs_to_policy s
 3. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects; (pasObjectAbs aag ?x6, ?auth6, pasObjectAbs aag ?y6) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to subjects aag Write p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects\<rbrakk> \<Longrightarrow> (?x6, ?auth6, ?y6) \<in> state_objs_to_policy s
 2. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects; (pasObjectAbs aag ?x6, ?auth6, pasObjectAbs aag ?y6) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to subjects aag Write p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects; (pasObjectAbs aag ?x6, ?auth6, pasObjectAbs aag ?y6) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to subjects aag Write p
 2. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects\<rbrakk> \<Longrightarrow> (?x6, ?auth6, ?y6) \<in> state_objs_to_policy s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects; (pasObjectAbs aag ?x6, ?auth6, pasObjectAbs aag ?y6) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (?s26, Write, pasObjectAbs aag p) \<in> pasPolicy aag
 2. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects; (pasObjectAbs aag ?x6, ?auth6, pasObjectAbs aag ?y6) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> ?s26 \<in> subjects
 3. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects\<rbrakk> \<Longrightarrow> (?x6, ?auth6, ?y6) \<in> state_objs_to_policy s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects; (pasObjectAbs aag ?x6, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pasObjectAbs aag ?x6 \<in> subjects
 2. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects\<rbrakk> \<Longrightarrow> (?x6, Write, p) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; p \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<in> subjects\<rbrakk> \<Longrightarrow> (p', Write, p) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; pasObjectAbs aag p' \<in> subjects; \<exists>tcb acap. get_tcb p' s = Some tcb \<and> tcb_ipcframe tcb = ArchObjectCap acap \<and> caps_of_state s (p', tcb_cnode_index 4) = Some (ArchObjectCap acap) \<and> Write \<in> arch_cap_auth_conferred acap \<and> p \<in> aobj_ref' acap\<rbrakk> \<Longrightarrow> (p', Write, p) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<And>tcb acap. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; pasObjectAbs aag p' \<in> subjects; get_tcb p' s = Some tcb; tcb_ipcframe tcb = ArchObjectCap acap; caps_of_state s (p', tcb_cnode_index 4) = Some (ArchObjectCap acap); Write \<in> arch_cap_auth_conferred acap; p \<in> aobj_ref' acap\<rbrakk> \<Longrightarrow> (p', Write, p) \<in> state_objs_to_policy s proof (prove)
goal (2 subgoals):
 1. \<And>tcb acap. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; pasObjectAbs aag p' \<in> subjects; get_tcb p' s = Some tcb; tcb_ipcframe tcb = ArchObjectCap acap; Write \<in> arch_cap_auth_conferred acap; p \<in> aobj_ref' acap\<rbrakk> \<Longrightarrow> ?auth38 tcb acap \<in> cap_auth_conferred (ArchObjectCap acap)
 2. \<And>tcb acap. \<lbrakk>pas_refined aag s; valid_objs s; case tcb_states_of_state s p' of None \<Rightarrow> False | Some x2 \<Rightarrow> can_receive_ipc x2; tcb_states_of_state s' p' = Some Running; pasObjectAbs aag p' \<in> subjects; get_tcb p' s = Some tcb; tcb_ipcframe tcb = ArchObjectCap acap; Write \<in> arch_cap_auth_conferred acap; p \<in> aobj_ref' acap; (fst (p', tcb_cnode_index 4), ?auth38 tcb acap, p) \<in> state_objs_to_policy s\<rbrakk> \<Longrightarrow> (p', Write, p) \<in> state_objs_to_policy s proof (prove)
goal:
No subgoals!