theory FinalCaps

lemma set_cap_silc_inv_simple:
  "\<lbrace>silc_inv aag st and cte_wp_at (\<lambda>cp. cap_irqs cp = cap_irqs cap \<and>
                                        obj_refs cp = obj_refs cap) slot
                    and K (is_subject aag (fst slot))\<rbrace>
   set_cap cap slot
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (wp set_cap_silc_inv) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (rule conjI; clarsimp) apply (drule caps_of_state_cteD) apply (frule(1) silc_invD) apply (clarsimp simp: intra_label_cap_def) apply (rule exI, rule conjI, assumption) apply (simp add: cap_points_to_label_def) apply (simp add: slots_holding_overlapping_caps_def) apply (simp add: silc_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and cte_wp_at (\<lambda>cp. cap_irqs cp = cap_irqs cap \<and> obj_refs cp = obj_refs cap) slot and K (is_subject aag (fst slot))\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and cte_wp_at (\<lambda>cp. cap_irqs cp = cap_irqs cap \<and> obj_refs cp = obj_refs cap) slot and K (is_subject aag (fst slot))) s \<Longrightarrow> ((\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; is_subject aag (fst slot); caps_of_state s slot = Some capa; cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag cap (pasSubject aag) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasSubject aag \<noteq> SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; is_subject aag (fst slot); caps_of_state s slot = Some capa; cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; \<not> cap_points_to_label aag cap (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = SilcLabel; caps_of_state s slot = Some capa; cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; pasSubject aag = SilcLabel\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; is_subject aag (fst slot); cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; \<not> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) slot s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = SilcLabel; caps_of_state s slot = Some capa; cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; pasSubject aag = SilcLabel\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; is_subject aag (fst slot); cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; \<not> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) slot s\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag slot s
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; is_subject aag (fst slot); cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; \<not> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) slot s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = SilcLabel; caps_of_state s slot = Some capa; cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; pasSubject aag = SilcLabel\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; is_subject aag (fst slot); cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; \<not> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) slot s\<rbrakk> \<Longrightarrow> \<exists>cap. cte_wp_at ((=) cap) slot s \<and> \<not> cap_points_to_label aag cap (pasSubject aag)
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; is_subject aag (fst slot); cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; \<not> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) slot s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = SilcLabel; caps_of_state s slot = Some capa; cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; pasSubject aag = SilcLabel\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; is_subject aag (fst slot); cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; \<not> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) slot s\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag capa (pasSubject aag)
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; is_subject aag (fst slot); cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; \<not> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) slot s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = SilcLabel; caps_of_state s slot = Some capa; cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; pasSubject aag = SilcLabel\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; is_subject aag (fst slot); cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; \<not> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) slot s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = SilcLabel; caps_of_state s slot = Some capa; cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; pasSubject aag = SilcLabel\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = SilcLabel; caps_of_state s slot = Some capa; cap_irqs capa = cap_irqs cap; obj_refs capa = obj_refs cap; pasSubject aag = SilcLabel\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!