theory DomainSepInv

lemma receive_ipc_base_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb and
    sym_refs \<circ> state_refs_of and ko_at (Endpoint ep) epptr \<rbrace>
   receive_ipc_base aag receiver ep epptr rights is_blocking
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" apply (clarsimp cong: endpoint.case_cong thread_get_def get_thread_state_def) apply (wp setup_caller_cap_domain_sep_inv dxo_wp_weak | wpc | simp split del: if_split)+ apply (rule_tac Q="\<lambda> r s. domain_sep_inv irqs st s" in hoare_strengthen_post) apply (wp do_ipc_transfer_domain_sep_inv hoare_vcg_all_lift | wpc | simp)+ apply (wpsimp wp: hoare_vcg_imp_lift[OF set_simple_ko_get_tcb, unfolded disj_not1]
                       hoare_vcg_all_lift get_simple_ko_wp
                 simp: a_type_def do_nbrecv_failed_transfer_def)+ apply (fastforce simp: valid_objs_def valid_obj_def obj_at_def
                         ep_redux_simps neq_Nil_conv valid_ep_def
                  split: list.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of and ko_at (Endpoint ep) epptr\<rbrace> 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 data \<Rightarrow> return data | _ \<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 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of and ko_at (Endpoint ep) epptr\<rbrace> 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 y <- assert (q \<noteq> []);
y <- set_endpoint epptr (case tl q of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl q));
tcb <- gets_the (get_tcb (hd q));
data <- case tcb_state tcb of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd q) (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 (hd q) receiver (AllowGrant \<in> rights) else set_thread_state (hd q) Inactive else do y <- set_thread_state (hd q) Running;
possible_switch_to (hd q)
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 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x2 tcb data. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B46 x2 () () tcb data\<rbrace> do_ipc_transfer (hd x2) (Some epptr) (sender_badge data) (sender_can_grant data) receiver \<lbrace>\<lambda>yb s. (sender_is_call data \<longrightarrow> (sender_can_grant data \<longrightarrow> domain_sep_inv irqs st s) \<and> (sender_can_grant_reply data \<longrightarrow> domain_sep_inv irqs st s) \<and> (\<not> sender_can_grant data \<and> \<not> sender_can_grant_reply data \<longrightarrow> domain_sep_inv irqs st s)) \<and> (\<not> sender_is_call data \<longrightarrow> domain_sep_inv irqs st s)\<rbrace>
 2. \<And>x2 y ya tcb. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B45 x2 y ya tcb\<rbrace> case tcb_state tcb of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>?B46 x2 y ya tcb\<rbrace>
 3. \<And>x2 y ya. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B44 x2 y ya\<rbrace> gets_the (get_tcb (hd x2)) \<lbrace>?B45 x2 y ya\<rbrace>
 4. \<And>x2 y. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B43 x2 y\<rbrace> set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>?B44 x2 y\<rbrace>
 5. \<And>x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R21 x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B43 x2\<rbrace>
 6. \<And>x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R22 x3\<rbrace> 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 (x3 @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 7. \<And>s. (domain_sep_inv irqs st and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of and ko_at (Endpoint ep) epptr) s \<Longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> domain_sep_inv irqs st s) \<and> (is_blocking = False \<longrightarrow> domain_sep_inv irqs st s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R21 x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R22 x s) proof (prove)
goal (8 subgoals):
 1. \<And>x2 tcb data. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B46 x2 () () tcb data\<rbrace> do_ipc_transfer (hd x2) (Some epptr) (sender_badge data) (sender_can_grant data) receiver \<lbrace>\<lambda>r. domain_sep_inv irqs st\<rbrace>
 2. \<And>x2 tcb data rv s. \<lbrakk>ep = SendEP x2; domain_sep_inv irqs st s\<rbrakk> \<Longrightarrow> (sender_is_call data \<longrightarrow> (sender_can_grant data \<longrightarrow> domain_sep_inv irqs st s) \<and> (sender_can_grant_reply data \<longrightarrow> domain_sep_inv irqs st s) \<and> (\<not> sender_can_grant data \<and> \<not> sender_can_grant_reply data \<longrightarrow> domain_sep_inv irqs st s)) \<and> (\<not> sender_is_call data \<longrightarrow> domain_sep_inv irqs st s)
 3. \<And>x2 y ya tcb. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B45 x2 y ya tcb\<rbrace> case tcb_state tcb of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>?B46 x2 y ya tcb\<rbrace>
 4. \<And>x2 y ya. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B44 x2 y ya\<rbrace> gets_the (get_tcb (hd x2)) \<lbrace>?B45 x2 y ya\<rbrace>
 5. \<And>x2 y. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B43 x2 y\<rbrace> set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>?B44 x2 y\<rbrace>
 6. \<And>x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R21 x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B43 x2\<rbrace>
 7. \<And>x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R22 x3\<rbrace> 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 (x3 @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 8. \<And>s. (domain_sep_inv irqs st and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of and ko_at (Endpoint ep) epptr) s \<Longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> domain_sep_inv irqs st s) \<and> (is_blocking = False \<longrightarrow> domain_sep_inv irqs st s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R21 x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R22 x s) proof (prove)
goal (4 subgoals):
 1. \<And>x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B43 x2 ()\<rbrace> set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>\<lambda>ya s. (\<exists>y. get_tcb (hd x2) s = Some y) \<longrightarrow> (\<exists>x xa. tcb_state (the (get_tcb (hd x2) s)) = BlockedOnSend x xa) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> valid_mdb s\<rbrace>
 2. \<And>x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R21 x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B43 x2\<rbrace>
 3. \<And>x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R22 x3\<rbrace> 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 (x3 @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>s. (domain_sep_inv irqs st and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of and ko_at (Endpoint ep) epptr) s \<Longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> domain_sep_inv irqs st s) \<and> (is_blocking = False \<longrightarrow> domain_sep_inv irqs st s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R21 x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R22 x s) proof (prove)
goal (1 subgoal):
 1. \<And>s x y xa xb. \<lbrakk>domain_sep_inv irqs st s; valid_objs s; valid_mdb s; sym_refs (state_refs_of s); ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; get_tcb (hd x) s = Some y; tcb_state y = BlockedOnSend xa xb\<rbrakk> \<Longrightarrow> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s proof (prove)
goal:
No subgoals!