theory Ipc_AC

lemma do_normal_transfer_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
                    and valid_objs and valid_mdb
                    and K (grant \<longrightarrow> is_subject aag sender)
                    and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace>
   do_normal_transfer sender sbuf endpoint badge grant receiver rbuf
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" proof(cases grant) case True thus ?thesis apply - apply (rule hoare_gen_asm) apply (simp add: do_normal_transfer_def) by (wpsimp wp: copy_mrs_pas_refined transfer_caps_pas_refined
                   lec_valid_cap' copy_mrs_cte_wp_at hoare_vcg_ball_lift
                   lookup_extra_caps_srcs[simplified ball_conj_distrib,THEN hoare_conjDR1]
                   lookup_extra_caps_srcs[simplified ball_conj_distrib,THEN hoare_conjDR2]
                   lookup_extra_caps_authorised lookup_extra_caps_auth
             simp: ball_conj_distrib) next case False thus ?thesis apply (simp add: do_normal_transfer_def) by (wpsimp wp: copy_mrs_pas_refined copy_mrs_cte_wp_at transfer_caps_empty_inv) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (state)
goal (2 subgoals):
 1. grant \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<not> grant \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (state)
this:
grant

goal (2 subgoals):
 1. grant \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<not> grant \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
using this:
grant

goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. grant \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>grant; grant \<longrightarrow> is_subject aag receiver\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender)\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>grant; is_subject aag receiver\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and (\<lambda>y. is_subject aag sender)\<rbrace> do mi <- get_message_info sender;
caps <- lookup_extra_caps sender sbuf mi <catch> (\<lambda>y. return []);
mrs_transferred <- copy_mrs sender sbuf receiver rbuf (mi_length mi);
mi' <- transfer_caps mi caps endpoint receiver rbuf;
y <- set_message_info receiver (MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (state)
this:
\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. pas_refined aag\<rbrace>

goal (1 subgoal):
 1. \<not> grant \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (state)
goal (1 subgoal):
 1. \<not> grant \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (state)
this:
\<not> grant

goal (1 subgoal):
 1. \<not> grant \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
using this:
\<not> grant

goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> grant \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb\<rbrace> do mi <- get_message_info sender;
mrs_transferred <- copy_mrs sender sbuf receiver rbuf (mi_length mi);
mi' <- transfer_caps mi [] endpoint receiver rbuf;
y <- set_message_info receiver (MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (state)
this:
\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. pas_refined aag\<rbrace>

goal:
No subgoals!