theory Ipc_IF

lemma receive_ipc_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects aag (l :: 'a subject_label)
                      (invs and
                         pas_refined aag and pas_cur_domain aag and valid_cap cap
                     and is_subject aag \<circ> cur_thread
                     and K (is_subject aag receiver \<and> pas_cap_cur_auth aag cap
                          \<and> AllowRead \<in> cap_rights cap))
     (receive_ipc receiver cap is_blocking)" apply (rule gen_asm_ev) apply (simp add: receive_ipc_def thread_get_def split: cap.split) apply (clarsimp simp: fail_ev_pre) apply (rename_tac epptr badge rights) apply (wp receive_ipc_base_reads_respects
            complete_signal_reads_respects
            hoare_weak_lift_imp set_simple_ko_reads_respects set_thread_state_reads_respects
            setup_caller_cap_reads_respects
            complete_signal_reads_respects thread_get_reads_respects
            get_thread_state_reads_respects
            possible_switch_to_reads_respects
            gets_cur_thread_ev
            set_thread_state_pas_refined
            do_ipc_transfer_reads_respects do_ipc_transfer_pas_refined
            hoare_vcg_all_lift
            get_bound_notification_reads_respects' gbn_wp
            get_simple_ko_reads_respects get_simple_ko_wp
        | wpc
        | simp)+ by (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def
                dest: bound_tcb_at_implies_receive reads_ep)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap cap and is_subject aag \<circ> cur_thread and K (is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap)) (receive_ipc receiver cap is_blocking) proof (prove)
goal (1 subgoal):
 1. is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap \<Longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap cap and is_subject aag \<circ> cur_thread) (receive_ipc receiver cap is_blocking) proof (prove)
goal (1 subgoal):
 1. is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap \<Longrightarrow> (cap = NullCap \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap NullCap and is_subject aag \<circ> cur_thread) fail) \<and> (\<forall>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap (UntypedCap x21 x22 x23 x24) and is_subject aag \<circ> cur_thread) fail) \<and> (\<forall>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap (EndpointCap x31 x32 x33) and is_subject aag \<circ> cur_thread) (do ep <- get_endpoint x31;
ntfnptr <- get_bound_notification receiver;
ntfn <- case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x;
if (\<exists>y. ntfnptr = Some y) \<and> isActive ntfn then complete_signal (the ntfnptr) receiver else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver
od)) \<and> (\<forall>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap (NotificationCap x41 x42 x43) and is_subject aag \<circ> cur_thread) fail) \<and> (\<forall>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap (ReplyCap x51 x52 x53) and is_subject aag \<circ> cur_thread) fail) \<and> (\<forall>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap (CNodeCap x61 x62 x63) and is_subject aag \<circ> cur_thread) fail) \<and> (\<forall>x7. cap = ThreadCap x7 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap (ThreadCap x7) and is_subject aag \<circ> cur_thread) fail) \<and> (cap = DomainCap \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap DomainCap and is_subject aag \<circ> cur_thread) fail) \<and> (cap = IRQControlCap \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap IRQControlCap and is_subject aag \<circ> cur_thread) fail) \<and> (\<forall>x10. cap = IRQHandlerCap x10 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap (IRQHandlerCap x10) and is_subject aag \<circ> cur_thread) fail) \<and> (\<forall>x111 x112 x113. cap = Zombie x111 x112 x113 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap (Zombie x111 x112 x113) and is_subject aag \<circ> cur_thread) fail) \<and> (\<forall>x12. cap = ArchObjectCap x12 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap (ArchObjectCap x12) and is_subject aag \<circ> cur_thread) fail) proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap (EndpointCap x31 x32 x33) and is_subject aag \<circ> cur_thread) (do ep <- get_endpoint x31;
ntfnptr <- get_bound_notification receiver;
ntfn <- case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x;
if (\<exists>y. ntfnptr = Some y) \<and> isActive ntfn then complete_signal (the ntfnptr) receiver else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver
od) proof (prove)
goal (1 subgoal):
 1. \<And>epptr badge rights. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap epptr badge rights); AllowRead \<in> rights; cap = EndpointCap epptr badge rights\<rbrakk> \<Longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and valid_cap (EndpointCap epptr badge rights) and is_subject aag \<circ> cur_thread) (do ep <- get_endpoint epptr;
ntfnptr <- get_bound_notification receiver;
ntfn <- case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x;
if (\<exists>y. ntfnptr = Some y) \<and> isActive ntfn then complete_signal (the ntfnptr) receiver else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some epptr) (sender_badge data) (sender_can_grant data) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (AllowGrant \<in> rights) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver
od) proof (prove)
goal (1 subgoal):
 1. \<And>epptr badge rights s. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap epptr badge rights); AllowRead \<in> rights; cap = EndpointCap epptr badge rights; invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> s \<turnstile> EndpointCap epptr badge rights \<and> is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l epptr \<and> ((\<exists>ntfn. ko_at (Endpoint ntfn) epptr s) \<longrightarrow> (\<forall>ntfn. bound_tcb_at ((=) ntfn) receiver s \<longrightarrow> (\<forall>x. ntfn = Some x \<longrightarrow> aag_can_read_or_affect aag l x) \<and> (ntfn = None \<longrightarrow> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag)) \<and> (\<forall>x. ntfn = Some x \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> (isActive ntfn \<longrightarrow> aag_can_read_or_affect aag l x) \<and> (\<not> isActive ntfn \<longrightarrow> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag))))))