theory Finalise_AC

lemma finalise_cap_respects[wp]:
  "\<lbrace>integrity aag X st and pas_refined aag and einvs and valid_cap cap
                                           and K (pas_cap_cur_auth aag cap)\<rbrace>
   finalise_cap cap final
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (cases cap; simp; safe?;
         (solves \<open>(wp | simp add: if_apply_def2 split del: if_split
                      | clarsimp simp: cap_auth_conferred_def cap_rights_to_auth_def is_cap_simps
                                       pas_refined_all_auth_is_owns aag_cap_auth_def
                                       deleting_irq_handler_def cap_links_irq_def invs_valid_objs
                            split del: if_split
                                elim!: pas_refined_Control [symmetric])+\<close>)?) 
   (*NTFN Cap*)
    apply ((wp unbind_maybe_notification_valid_objs get_simple_ko_wp
              unbind_maybe_notification_respects
           | wpc
           | simp add: cap_auth_conferred_def cap_rights_to_auth_def aag_cap_auth_def
                split: if_split_asm
           | fastforce)+;
          clarsimp simp: obj_at_def valid_cap_def is_ntfn invs_def
                         valid_state_def valid_pspace_def
                  split: option.splits) 
  (* tcb cap *)
   apply (wp unbind_notification_respects unbind_notification_invs
         | clarsimp simp: cap_auth_conferred_def cap_rights_to_auth_def aag_cap_auth_def
                          unbind_maybe_notification_def
                   elim!: pas_refined_Control[symmetric]
         | simp add: if_apply_def2 split del: if_split )+ apply (clarsimp simp: valid_cap_def pred_tcb_at_def obj_at_def is_tcb
                 dest!: tcb_at_ko_at) apply (clarsimp split: option.splits elim!: pas_refined_Control[symmetric]) apply (frule pas_refined_Control, simp+) apply (fastforce dest: bound_tcb_at_implies_reset
               simp add: pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and einvs and valid_cap cap and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and valid_cap (NotificationCap x41 x42 x43) and (\<lambda>y. pas_cap_cur_auth aag (NotificationCap x41 x42 x43))\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when final (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>x7. \<lbrakk>cap = ThreadCap x7; final\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and valid_cap (ThreadCap x7) and (\<lambda>y. pas_cap_cur_auth aag (ThreadCap x7))\<rbrace> do y <- unbind_notification x7;
y <- suspend x7;
y <- prepare_thread_delete x7;
return (Zombie x7 None 5, NullCap)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and valid_cap (NotificationCap x41 x42 x43) and (\<lambda>y. pas_cap_cur_auth aag (NotificationCap x41 x42 x43))\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when final (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>x7. \<lbrakk>cap = ThreadCap x7; final\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and valid_cap (ThreadCap x7) and (\<lambda>y. pas_cap_cur_auth aag (ThreadCap x7))\<rbrace> do y <- unbind_notification x7;
y <- suspend x7;
y <- prepare_thread_delete x7;
return (Zombie x7 None 5, NullCap)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x7. \<lbrakk>cap = ThreadCap x7; final\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and valid_cap (ThreadCap x7) and (\<lambda>y. pas_cap_cur_auth aag (ThreadCap x7))\<rbrace> do y <- unbind_notification x7;
y <- suspend x7;
y <- prepare_thread_delete x7;
return (Zombie x7 None 5, NullCap)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x7. \<lbrakk>cap = ThreadCap x7; final\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and valid_cap (ThreadCap x7) and (\<lambda>y. pas_cap_cur_auth aag (ThreadCap x7))\<rbrace> do y <- unbind_notification x7;
y <- suspend x7;
y <- prepare_thread_delete x7;
return (Zombie x7 None 5, NullCap)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x7 s. \<lbrakk>cap = ThreadCap x7; final; integrity aag X st s; pas_refined aag s; invs s; valid_list s; valid_sched s; s \<turnstile> ThreadCap x7; (pasSubject aag, Control, pasObjectAbs aag x7) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7)\<rbrakk> \<Longrightarrow> bound_tcb_at (case_option True (\<lambda>ntfn. (pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag)) x7 s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> tcb_at x7 s \<and> is_subject aag x7 proof (prove)
goal (1 subgoal):
 1. \<And>x7 s tcb. \<lbrakk>cap = ThreadCap x7; final; integrity aag X st s; pas_refined aag s; invs s; valid_list s; valid_sched s; (pasSubject aag, Control, pasObjectAbs aag x7) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7); cap_aligned (ThreadCap x7); kheap s x7 = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (case tcb_bound_notification tcb of None \<Rightarrow> True | Some ntfn \<Rightarrow> (pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag x7 proof (prove)
goal (1 subgoal):
 1. \<And>x7 s tcb. \<lbrakk>cap = ThreadCap x7; final; integrity aag X st s; pas_refined aag s; invs s; valid_list s; valid_sched s; (pasSubject aag, Control, pasObjectAbs aag x7) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7); cap_aligned (ThreadCap x7); kheap s x7 = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (tcb_bound_notification tcb = None \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag x7) \<and> (\<forall>x2. tcb_bound_notification tcb = Some x2 \<longrightarrow> (pasSubject aag, Reset, pasObjectAbs aag x2) \<in> pasPolicy aag \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag x7) proof (prove)
goal (1 subgoal):
 1. \<And>x7 s tcb. \<lbrakk>cap = ThreadCap x7; final; integrity_subjects {pasObjectAbs aag x7} aag (pasMayActivate aag) X st s; pas_refined aag s; invs s; valid_list s; valid_sched s; (pasObjectAbs aag x7, Control, pasObjectAbs aag x7) \<in> pasPolicy aag; cap_links_asid_slot aag (pasObjectAbs aag x7) (ThreadCap x7); cap_links_irq aag (pasObjectAbs aag x7) (ThreadCap x7); cap_aligned (ThreadCap x7); kheap s x7 = Some (TCB tcb); pasSubject aag = pasObjectAbs aag x7\<rbrakk> \<Longrightarrow> (tcb_bound_notification tcb = None \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x2. tcb_bound_notification tcb = Some x2 \<longrightarrow> (pasObjectAbs aag x7, Reset, pasObjectAbs aag x2) \<in> pasPolicy aag \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) proof (prove)
goal:
No subgoals!