theory CNodeInv_AI

lemma cap_swap_invs[wp]:
  "\<And>c' a c b.
  \<lbrace>invs and ex_cte_cap_wp_to (appropriate_cte_cap c') a
         and ex_cte_cap_wp_to (appropriate_cte_cap c) b and
    valid_cap c and valid_cap c' and
    tcb_cap_valid c b and tcb_cap_valid c' a and
    cte_wp_at (weak_derived c) a and
    cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c) a and
    cte_wp_at (weak_derived c') b and
    cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c') b and
    K (a \<noteq> b \<and> \<not> is_master_reply_cap c \<and> \<not> is_master_reply_cap c')\<rbrace>
   cap_swap c a c' b \<lbrace>\<lambda>rv. invs :: 'state_ext state \<Rightarrow> bool\<rbrace>" unfolding invs_def valid_state_def valid_pspace_def apply (wp cap_swap_replies cap_swap_reply_masters valid_arch_state_lift_aobj_at
            cap_swap_typ_at valid_irq_node_typ cap_swap_aobj_at
         | simp
         | erule disjE
         | clarsimp simp: cte_wp_at_caps_of_state copy_of_cte_refs weak_derived_def
                          copy_obj_refs copy_of_zobj_refs copy_of_is_zombie
                          copy_of_cap_irqs gen_obj_refs_eq copy_of_arch_gen_obj_refs
         | clarsimp simp: valid_global_refs_def valid_refs_def copy_of_cap_range
                          cte_wp_at_caps_of_state
                simp del: split_paired_Ex split_paired_All
         | rule conjI
         | clarsimp dest!: valid_reply_caps_of_stateD)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>c' a c b. \<lbrace>invs and ex_cte_cap_wp_to (appropriate_cte_cap c') a and ex_cte_cap_wp_to (appropriate_cte_cap c) b and valid_cap c and valid_cap c' and tcb_cap_valid c b and tcb_cap_valid c' a and cte_wp_at (weak_derived c) a and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c) a and cte_wp_at (weak_derived c') b and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c') b and K (a \<noteq> b \<and> \<not> is_master_reply_cap c \<and> \<not> is_master_reply_cap c')\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>c' a c b. \<lbrace>valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and ex_cte_cap_wp_to (appropriate_cte_cap c') a and ex_cte_cap_wp_to (appropriate_cte_cap c) b and valid_cap c and valid_cap c' and tcb_cap_valid c b and tcb_cap_valid c' a and cte_wp_at (weak_derived c) a and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c) a and cte_wp_at (weak_derived c') b and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c') b and K (a \<noteq> b \<and> \<not> is_master_reply_cap c \<and> \<not> is_master_reply_cap c')\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace> proof (prove)
goal:
No subgoals!