theory FinalCaps

lemma do_normal_transfer_silc_inv:
  "\<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state
                    and valid_objs and valid_mdb and pas_refined aag
                    and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrace>
   do_normal_transfer sender send_buffer ep badge grant receiver recv_buffer
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding do_normal_transfer_def apply (case_tac grant) apply ((wp transfer_caps_silc_inv copy_mrs_cte_wp_at hoare_vcg_ball_lift lec_valid_cap'
              lookup_extra_caps_authorised copy_mrs_pas_refined
           | simp)+)[1] apply simp apply (wp transfer_caps_empty_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrace> do_normal_transfer sender send_buffer ep badge grant receiver recv_buffer \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrace> do mi <- get_message_info sender;
caps <- if grant then lookup_extra_caps sender send_buffer mi <catch> K (return []) else return [];
mrs_transferred <- copy_mrs sender send_buffer receiver recv_buffer (mi_length mi);
mi' <- transfer_caps mi caps ep receiver recv_buffer;
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>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. grant \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrace> do mi <- get_message_info sender;
caps <- if grant then lookup_extra_caps sender send_buffer mi <catch> K (return []) else return [];
mrs_transferred <- copy_mrs sender send_buffer receiver recv_buffer (mi_length mi);
mi' <- transfer_caps mi caps ep receiver recv_buffer;
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>_. silc_inv aag st\<rbrace>
 2. \<not> grant \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrace> do mi <- get_message_info sender;
caps <- if grant then lookup_extra_caps sender send_buffer mi <catch> K (return []) else return [];
mrs_transferred <- copy_mrs sender send_buffer receiver recv_buffer (mi_length mi);
mi' <- transfer_caps mi caps ep receiver recv_buffer;
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>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> grant \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrace> do mi <- get_message_info sender;
caps <- if grant then lookup_extra_caps sender send_buffer mi <catch> K (return []) else return [];
mrs_transferred <- copy_mrs sender send_buffer receiver recv_buffer (mi_length mi);
mi' <- transfer_caps mi caps ep receiver recv_buffer;
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>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> grant \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag\<rbrace> do mi <- get_message_info sender;
mrs_transferred <- copy_mrs sender send_buffer receiver recv_buffer (mi_length mi);
mi' <- transfer_caps mi [] ep receiver recv_buffer;
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>_. silc_inv aag st\<rbrace> proof (prove)
goal:
No subgoals!