theory ArchFinalCaps

lemma perform_asid_pool_invocation_silc_inv:
  "\<lbrace>silc_inv aag st and K (authorised_asid_pool_inv aag blah)\<rbrace>
   perform_asid_pool_invocation blah
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (rule hoare_gen_asm) unfolding perform_asid_pool_invocation_def apply (rule hoare_pre) apply (wp set_cap_silc_inv get_cap_wp | wpc)+ apply clarsimp apply (rule conjI, intro impI) apply (drule silc_invD) apply assumption apply (fastforce simp: intra_label_cap_def simp: cap_points_to_label_def) apply (clarsimp simp: slots_holding_overlapping_caps_def) apply (fastforce simp: authorised_asid_pool_inv_def silc_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (authorised_asid_pool_inv aag blah)\<rbrace> perform_asid_pool_invocation blah \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. authorised_asid_pool_inv aag blah \<Longrightarrow> \<lbrace>silc_inv aag st\<rbrace> perform_asid_pool_invocation blah \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. authorised_asid_pool_inv aag blah \<Longrightarrow> \<lbrace>silc_inv aag st\<rbrace> case blah of Assign asid pool_ptr ct_slot \<Rightarrow> do pd_cap <- get_cap ct_slot;
case pd_cap of ArchObjectCap (PageDirectoryCap pd_base x) \<Rightarrow> do pool <- get_asid_pool pool_ptr;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid \<mapsto> pd_base));
set_cap (ArchObjectCap $ PageDirectoryCap pd_base (Some asid)) ct_slot;
set_asid_pool pool_ptr pool'
od | ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. authorised_asid_pool_inv aag blah \<Longrightarrow> \<lbrace>?Q2\<rbrace> case blah of Assign asid pool_ptr ct_slot \<Rightarrow> do pd_cap <- get_cap ct_slot;
case pd_cap of ArchObjectCap (PageDirectoryCap pd_base x) \<Rightarrow> do pool <- get_asid_pool pool_ptr;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid \<mapsto> pd_base));
set_cap (ArchObjectCap $ PageDirectoryCap pd_base (Some asid)) ct_slot;
set_asid_pool pool_ptr pool'
od | ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s. \<lbrakk>authorised_asid_pool_inv aag blah; silc_inv aag st s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>authorised_asid_pool_inv aag blah; silc_inv aag st s\<rbrakk> \<Longrightarrow> \<forall>x xa xb. blah = Assign x xa xb \<longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) xb s \<longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>xc. cap = ArchObjectCap xc \<longrightarrow> (\<forall>x xa. xc = ASIDPoolCap x xa \<longrightarrow> True) \<and> (xc = ASIDControlCap \<longrightarrow> True) \<and> (\<forall>x xa xb xd xe. xc = PageCap x xa xb xd xe \<longrightarrow> True) \<and> (\<forall>x xa. xc = PageTableCap x xa \<longrightarrow> True) \<and> (\<forall>xd xe. xc = PageDirectoryCap xd xe \<longrightarrow> (\<forall>pool. ako_at (ASIDPool pool) xa s \<longrightarrow> ((\<lambda>s. \<not> cap_points_to_label aag (ArchObjectCap $ PageDirectoryCap xd (Some x)) (pasObjectAbs aag (fst xb)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps (ArchObjectCap $ PageDirectoryCap xd (Some x)) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and silc_inv aag st and K (pasObjectAbs aag (fst xb) \<noteq> SilcLabel)) s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa a b xc xd pool. \<lbrakk>authorised_asid_pool_inv aag (Assign x xa (a, b)); silc_inv aag st s; blah = Assign x xa (a, b); cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap xc xd))) (a, b) s; ako_at (ASIDPool pool) xa s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag (ArchObjectCap (PageDirectoryCap xc (Some x))) (pasObjectAbs aag a) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageDirectoryCap xc (Some x))) s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasObjectAbs aag a \<noteq> SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s x xa a b xc xd pool. \<lbrakk>authorised_asid_pool_inv aag (Assign x xa (a, b)); silc_inv aag st s; blah = Assign x xa (a, b); cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap xc xd))) (a, b) s; ako_at (ASIDPool pool) xa s; \<not> cap_points_to_label aag (ArchObjectCap (PageDirectoryCap xc (Some x))) (pasObjectAbs aag a)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageDirectoryCap xc (Some x))) s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s x xa a b xc xd pool. \<lbrakk>authorised_asid_pool_inv aag (Assign x xa (a, b)); silc_inv aag st s; blah = Assign x xa (a, b); cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap xc xd))) (a, b) s; ako_at (ASIDPool pool) xa s\<rbrakk> \<Longrightarrow> pasObjectAbs aag a \<noteq> SilcLabel proof (prove)
goal (4 subgoals):
 1. \<And>s x xa a b xc xd pool. \<lbrakk>authorised_asid_pool_inv aag (Assign x xa (a, b)); blah = Assign x xa (a, b); cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap xc xd))) (a, b) s; ako_at (ASIDPool pool) xa s; \<not> cap_points_to_label aag (ArchObjectCap (PageDirectoryCap xc (Some x))) (pasObjectAbs aag a)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap203 s x xa a b xc xd pool)) (?slot203 s x xa a b xc xd pool) s
 2. \<And>s x xa a b xc xd pool. \<lbrakk>authorised_asid_pool_inv aag (Assign x xa (a, b)); blah = Assign x xa (a, b); cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap xc xd))) (a, b) s; ako_at (ASIDPool pool) xa s; \<not> cap_points_to_label aag (ArchObjectCap (PageDirectoryCap xc (Some x))) (pasObjectAbs aag a)\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (?slot203 s x xa a b xc xd pool) s
 3. \<And>s x xa a b xc xd pool. \<lbrakk>authorised_asid_pool_inv aag (Assign x xa (a, b)); blah = Assign x xa (a, b); cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap xc xd))) (a, b) s; ako_at (ASIDPool pool) xa s; \<not> cap_points_to_label aag (ArchObjectCap (PageDirectoryCap xc (Some x))) (pasObjectAbs aag a); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (?cap203 s x xa a b xc xd pool) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageDirectoryCap xc (Some x))) s) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s x xa a b xc xd pool. \<lbrakk>authorised_asid_pool_inv aag (Assign x xa (a, b)); silc_inv aag st s; blah = Assign x xa (a, b); cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap xc xd))) (a, b) s; ako_at (ASIDPool pool) xa s\<rbrakk> \<Longrightarrow> pasObjectAbs aag a \<noteq> SilcLabel proof (prove)
goal (3 subgoals):
 1. \<And>s x xa a b xc xd pool. \<lbrakk>authorised_asid_pool_inv aag (Assign x xa (a, b)); blah = Assign x xa (a, b); cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap xc xd))) (a, b) s; ako_at (ASIDPool pool) xa s; \<not> cap_points_to_label aag (ArchObjectCap (PageDirectoryCap xc (Some x))) (pasObjectAbs aag a)\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (a, b) s
 2. \<And>s x xa a b xc xd pool. \<lbrakk>authorised_asid_pool_inv aag (Assign x xa (a, b)); blah = Assign x xa (a, b); cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap xc xd))) (a, b) s; ako_at (ASIDPool pool) xa s; \<not> cap_points_to_label aag (ArchObjectCap (PageDirectoryCap xc (Some x))) (pasObjectAbs aag a); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (ArchObjectCap (PageDirectoryCap xc xd)) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageDirectoryCap xc (Some x))) s) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s x xa a b xc xd pool. \<lbrakk>authorised_asid_pool_inv aag (Assign x xa (a, b)); silc_inv aag st s; blah = Assign x xa (a, b); cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap xc xd))) (a, b) s; ako_at (ASIDPool pool) xa s\<rbrakk> \<Longrightarrow> pasObjectAbs aag a \<noteq> SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s x xa a b xc xd pool. \<lbrakk>authorised_asid_pool_inv aag (Assign x xa (a, b)); blah = Assign x xa (a, b); cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap xc xd))) (a, b) s; ako_at (ASIDPool pool) xa s; \<not> cap_points_to_label aag (ArchObjectCap (PageDirectoryCap xc (Some x))) (pasObjectAbs aag a); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (ArchObjectCap (PageDirectoryCap xc xd)) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageDirectoryCap xc (Some x))) s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s x xa a b xc xd pool. \<lbrakk>authorised_asid_pool_inv aag (Assign x xa (a, b)); silc_inv aag st s; blah = Assign x xa (a, b); cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap xc xd))) (a, b) s; ako_at (ASIDPool pool) xa s\<rbrakk> \<Longrightarrow> pasObjectAbs aag a \<noteq> SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s x xa a b xc xd pool. \<lbrakk>authorised_asid_pool_inv aag (Assign x xa (a, b)); silc_inv aag st s; blah = Assign x xa (a, b); cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap xc xd))) (a, b) s; ako_at (ASIDPool pool) xa s\<rbrakk> \<Longrightarrow> pasObjectAbs aag a \<noteq> SilcLabel proof (prove)
goal:
No subgoals!