theory Finalise_AC

lemma fast_finalise_respects[wp]:
  "\<lbrace>integrity aag X st and invs and pas_refined aag and valid_cap cap
                                and K (pas_cap_cur_auth aag cap)\<rbrace>
   fast_finalise cap fin
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (cases cap; simp) apply (wpsimp wp: unbind_maybe_notification_valid_objs get_simple_ko_wp
                       unbind_maybe_notification_respects
                 simp: cap_auth_conferred_def cap_rights_to_auth_def aag_cap_auth_def when_def
            | fastforce)+ apply (clarsimp simp: obj_at_def valid_cap_def is_ntfn invs_def valid_state_def valid_pspace_def
                  split: option.splits)+ apply (wp, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and invs and pas_refined aag and valid_cap cap and K (pas_cap_cur_auth aag cap)\<rbrace> fast_finalise cap fin \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (4 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>integrity aag X st and invs and pas_refined aag and valid_cap NullCap\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>integrity aag X st and invs and pas_refined aag and valid_cap (EndpointCap x31 x32 x33) and (\<lambda>y. pas_cap_cur_auth aag (EndpointCap x31 x32 x33))\<rbrace> when fin (cancel_all_ipc x31) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>integrity aag X st and invs and pas_refined aag and valid_cap (NotificationCap x41 x42 x43) and (\<lambda>y. pas_cap_cur_auth aag (NotificationCap x41 x42 x43))\<rbrace> when fin (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>integrity aag X st and invs and pas_refined aag and valid_cap (ReplyCap x51 x52 x53) and (\<lambda>y. pas_cap_cur_auth aag (ReplyCap x51 x52 x53))\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 s. \<lbrakk>cap = NotificationCap x41 x42 x43; integrity aag X st s; invs s; pas_refined aag s; s \<turnstile> NotificationCap x41 x42 x43; (pasSubject aag, Reset, pasObjectAbs aag x41) \<in> pasPolicy aag; \<forall>auth\<in>(if AllowRead \<in> x43 then {Receive} else {}) \<union> (if AllowWrite \<in> x43 then {Notify} else {}). (pasSubject aag, auth, pasObjectAbs aag x41) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (NotificationCap x41 x42 x43); cap_links_irq aag (pasSubject aag) (NotificationCap x41 x42 x43); fin\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (case ntfn_bound_tcb ntfn of None \<Rightarrow> True | _ \<Rightarrow> True)) x41 s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_objs s
 2. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>integrity aag X st and invs and pas_refined aag and valid_cap (ReplyCap x51 x52 x53) and (\<lambda>y. pas_cap_cur_auth aag (ReplyCap x51 x52 x53))\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>integrity aag X st and (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 pas_refined aag and valid_cap (ReplyCap x51 x52 x53) and (\<lambda>y. pas_cap_cur_auth aag (ReplyCap x51 x52 x53))\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal:
No subgoals!