theory ArchFinalise_AI

lemma finalise_cap_replaceable [Finalise_AI_asms]:
  "\<lbrace>\<lambda>s. s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s
        \<and> cte_wp_at ((=) cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s)
        \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s)
        \<and> (is_arch_cap cap \<longrightarrow> pspace_aligned s \<and>
                               valid_vspace_objs s \<and>
                               valid_arch_state s \<and>
                               valid_arch_caps s)\<rbrace>
     finalise_cap cap x
   \<lbrace>\<lambda>rv s. replaceable s sl (fst rv) cap\<rbrace>" apply (cases "is_arch_cap cap") apply (clarsimp simp: is_cap_simps) apply wp apply (clarsimp simp: replaceable_def reachable_pg_cap_def
                         o_def cap_range_def valid_arch_state_def
                         ran_tcb_cap_cases is_cap_simps
                         gen_obj_refs_subset vs_cap_ref_def) apply ((cases cap;
      simp add: replaceable_def reachable_pg_cap_def
                       split del: if_split;
      rule hoare_pre),

    (wp suspend_unlive'[unfolded o_def]
        suspend_final_cap[where sl=sl]
        unbind_maybe_notification_not_bound
        get_simple_ko_ko_at hoare_vcg_conj_lift
        unbind_notification_valid_objs
      | clarsimp simp: o_def dom_tcb_cap_cases_lt_ARCH
                       ran_tcb_cap_cases is_cap_simps
                       cap_range_def prepare_thread_delete_def
                       can_fast_finalise_def
                       gen_obj_refs_subset
                       vs_cap_ref_def
                       valid_ipc_buffer_cap_def
                dest!: tcb_cap_valid_NullCapD
                split: Structures_A.thread_state.split_asm
      | simp cong: conj_cong
      | simp cong: rev_conj_cong add: no_cap_to_obj_with_diff_ref_Null
      | (strengthen tcb_cap_valid_imp_NullCap tcb_cap_valid_imp', wp)
      | rule conjI
      | erule cte_wp_at_weakenE tcb_cap_valid_imp'[rule_format, rotated -1]
      | erule(1) no_cap_to_obj_with_diff_ref_finalI_ARCH
      | (wp (once) hoare_drop_imps,
          wp (once) cancel_all_ipc_unlive[unfolded o_def]
              cancel_all_signals_unlive[unfolded o_def])
      | ((wp (once) hoare_drop_imps)?,
         (wp (once) hoare_drop_imps)?,
         wp (once) deleting_irq_handler_empty)
      | wpc
      | simp add: valid_cap_simps is_nondevice_page_cap_simps)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s \<and> cte_wp_at ((=) cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap cap \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)\<rbrace> finalise_cap cap x \<lbrace>\<lambda>rv s. replaceable s sl (fst rv) cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_arch_cap cap \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s \<and> cte_wp_at ((=) cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap cap \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)\<rbrace> finalise_cap cap x \<lbrace>\<lambda>rv s. replaceable s sl (fst rv) cap\<rbrace>
 2. \<not> is_arch_cap cap \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s \<and> cte_wp_at ((=) cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap cap \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)\<rbrace> finalise_cap cap x \<lbrace>\<lambda>rv s. replaceable s sl (fst rv) cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a. cap = ArchObjectCap a \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> ArchObjectCap a \<and> x = is_final_cap' (ArchObjectCap a) s \<and> valid_mdb s \<and> cte_wp_at ((=) (ArchObjectCap a)) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s\<rbrace> arch_finalise_cap a x \<lbrace>\<lambda>rv s. replaceable s sl (fst rv) (ArchObjectCap a)\<rbrace>
 2. \<not> is_arch_cap cap \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s \<and> cte_wp_at ((=) cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap cap \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)\<rbrace> finalise_cap cap x \<lbrace>\<lambda>rv s. replaceable s sl (fst rv) cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a s. \<lbrakk>cap = ArchObjectCap a; s \<turnstile> ArchObjectCap a \<and> x = is_final_cap' (ArchObjectCap a) s \<and> valid_mdb s \<and> cte_wp_at ((=) (ArchObjectCap a)) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s\<rbrakk> \<Longrightarrow> s \<turnstile> ArchObjectCap a \<and> x = is_final_cap' (ArchObjectCap a) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_objs s \<and> valid_asid_table (asid_table s) s
 2. \<not> is_arch_cap cap \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s \<and> cte_wp_at ((=) cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap cap \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)\<rbrace> finalise_cap cap x \<lbrace>\<lambda>rv s. replaceable s sl (fst rv) cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> is_arch_cap cap \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s \<and> cte_wp_at ((=) cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap cap \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)\<rbrace> finalise_cap cap x \<lbrace>\<lambda>rv s. replaceable s sl (fst rv) cap\<rbrace> proof (prove)
goal:
No subgoals!