theory FinalCaps

lemma create_cap_silc_inv:
  "\<lbrace>silc_inv aag st and K (is_subject aag (fst (fst ref)) \<and>
                           is_subject aag (snd ref) \<and>
                           is_subject aag (fst c))\<rbrace>
   create_cap a b c dev ref
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding create_cap_def apply (rule hoare_gen_asm) apply (wp set_cap_default_cap_silc_inv set_cdt_silc_inv | simp add: split_def)+ apply (subgoal_tac "pasObjectAbs aag (fst c) \<noteq> SilcLabel") apply (drule silc_inv_all_children) apply (simp add: all_children_def del: split_paired_All) apply (clarsimp simp: silc_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (is_subject aag (fst (fst ref)) \<and> is_subject aag (snd ref) \<and> is_subject aag (fst c))\<rbrace> create_cap a b c dev ref \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (is_subject aag (fst (fst ref)) \<and> is_subject aag (snd ref) \<and> is_subject aag (fst c))\<rbrace> case ref of (dest, oref) \<Rightarrow> do dest_p <- gets (\<lambda>s. cdt s dest);
cdt <- gets cdt;
set_cdt (cdt(dest \<mapsto> c));
do_extended_op (create_cap_ext c dest dest_p);
set_original dest True;
set_cap (default_cap a oref b dev) dest
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst (fst ref)) \<and> is_subject aag (snd ref) \<and> is_subject aag (fst c) \<Longrightarrow> \<lbrace>silc_inv aag st\<rbrace> case ref of (dest, oref) \<Rightarrow> do dest_p <- gets (\<lambda>s. cdt s dest);
cdt <- gets cdt;
set_cdt (cdt(dest \<mapsto> c));
do_extended_op (create_cap_ext c dest dest_p);
set_original dest True;
set_cap (default_cap a oref b dev) dest
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst (fst ref)) \<and> is_subject aag (snd ref) \<and> is_subject aag (fst c); silc_inv aag st s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) ((cdt s)(fst ref \<mapsto> c)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag (fst (fst ref)) \<and> is_subject aag (snd ref) \<and> is_subject aag (fst c); silc_inv aag st s; pasObjectAbs aag (fst c) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) ((cdt s)(fst ref \<mapsto> c))
 2. \<And>s. \<lbrakk>is_subject aag (fst (fst ref)) \<and> is_subject aag (snd ref) \<and> is_subject aag (fst c); silc_inv aag st s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst c) \<noteq> SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag (fst (fst ref)) \<and> is_subject aag (snd ref) \<and> is_subject aag (fst c); pasObjectAbs aag (fst c) \<noteq> SilcLabel; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) ((cdt s)(fst ref \<mapsto> c))
 2. \<And>s. \<lbrakk>is_subject aag (fst (fst ref)) \<and> is_subject aag (snd ref) \<and> is_subject aag (fst c); silc_inv aag st s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst c) \<noteq> SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst (fst ref)) \<and> is_subject aag (snd ref) \<and> is_subject aag (fst c); silc_inv aag st s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst c) \<noteq> SilcLabel proof (prove)
goal:
No subgoals!