theory Finalise_AC

lemma finalise_cap_auth:
  "\<lbrace>(\<lambda>s. final \<longrightarrow> is_final_cap' cap s \<and> cte_wp_at ((=) cap) slot s) and K (pas_cap_cur_auth aag cap)\<rbrace>
   finalise_cap cap final
   \<lbrace>\<lambda>rv _. \<forall>x \<in> obj_refs_ac (fst rv). \<forall>a \<in> cap_auth_conferred (fst rv). aag_has_auth_to aag a x\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_strengthen_post, rule finalise_cap_cases) apply (elim disjE, clarsimp+) apply (clarsimp simp: is_cap_simps cap_auth_conferred_def aag_cap_auth_def) apply (simp add: fst_cte_ptrs_def split: cap.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. final \<longrightarrow> is_final_cap' cap s \<and> cte_wp_at ((=) cap) slot s) and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>rv _. \<forall>x\<in>obj_refs_ac (fst rv). \<forall>a\<in>cap_auth_conferred (fst rv). (pasSubject aag, a, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. pas_cap_cur_auth aag cap \<Longrightarrow> \<lbrace>\<lambda>s. final \<longrightarrow> is_final_cap' cap s \<and> cte_wp_at ((=) cap) slot s\<rbrace> finalise_cap cap final \<lbrace>\<lambda>rv _. \<forall>x\<in>obj_refs_ac (fst rv). \<forall>a\<in>cap_auth_conferred (fst rv). (pasSubject aag, a, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>pas_cap_cur_auth aag cap; fst rv = NullCap \<and> snd rv = (if final then cap_cleanup_opt cap else NullCap) \<and> (snd rv \<noteq> NullCap \<longrightarrow> is_final_cap' cap s) \<or> is_zombie (fst rv) \<and> is_final_cap' cap s \<and> is_final_cap' (fst rv) s \<and> snd rv = NullCap \<and> appropriate_cte_cap (fst rv) = appropriate_cte_cap cap \<and> cte_refs (fst rv) = cte_refs cap \<and> gen_obj_refs (fst rv) = gen_obj_refs cap \<and> obj_size (fst rv) = obj_size cap \<and> fst_cte_ptrs (fst rv) = fst_cte_ptrs cap \<and> vs_cap_ref cap = None\<rbrakk> \<Longrightarrow> \<forall>x\<in>obj_refs_ac (fst rv). \<forall>a\<in>cap_auth_conferred (fst rv). (pasSubject aag, a, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>a s x aa. \<lbrakk>pas_cap_cur_auth aag cap; x \<in> obj_refs_ac a; aa \<in> cap_auth_conferred a; is_zombie a; is_final_cap' cap s; is_final_cap' a s; appropriate_cte_cap a = appropriate_cte_cap cap; cte_refs a = cte_refs cap; gen_obj_refs a = gen_obj_refs cap; obj_size a = obj_size cap; fst_cte_ptrs a = fst_cte_ptrs cap; vs_cap_ref cap = None\<rbrakk> \<Longrightarrow> (pasSubject aag, aa, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s r b n. \<lbrakk>is_final_cap' cap s; is_final_cap' (Zombie r b n) s; appropriate_cte_cap (Zombie r b n) = appropriate_cte_cap cap; cte_refs (Zombie r b n) = cte_refs cap; gen_obj_refs (Zombie r b n) = gen_obj_refs cap; (case b of None \<Rightarrow> 0x200 | Some n \<Rightarrow> 2 ^ (cte_level_bits + n)) = obj_size cap; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs cap; vs_cap_ref cap = None; \<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>case cap of NullCap \<Rightarrow> {} | EndpointCap oref badge r \<Rightarrow> cap_rights_to_auth r True | NotificationCap oref badge r \<Rightarrow> cap_rights_to_auth (r - {AllowGrant, AllowGrantReply}) False | ReplyCap oref x xa \<Rightarrow> reply_cap_rights_to_auth x xa | ArchObjectCap x \<Rightarrow> arch_cap_auth_conferred x | _ \<Rightarrow> {Control}. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>x\<in>untyped_range cap. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) cap; cap_links_irq aag (pasSubject aag) cap\<rbrakk> \<Longrightarrow> (pasSubject aag, Control, pasObjectAbs aag r) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!