kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchArch_AC

lemma set_asid_pool_respects_clear:
  "\<lbrace>integrity aag X st and (\<lambda>s. \<forall>pool'. ko_at (ArchObj (arch_kernel_obj.ASIDPool pool')) ptr s
                                        \<longrightarrow> asid_pool_integrity {pasSubject aag} aag pool' pool)\<rbrace>
   set_asid_pool ptr pool
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: set_asid_pool_def) apply (wpsimp wp: set_object_wp_strong
              simp: obj_at_def a_type_def
             split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm if_splits) apply (erule integrity_trans) apply (clarsimp simp: integrity_def) apply (rule tro_arch; fastforce simp: arch_integrity_obj_atomic.simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>s. \<forall>pool'. ako_at (ASIDPool pool') ptr s \<longrightarrow> asid_pool_integrity {pasSubject aag} aag pool' pool)\<rbrace> set_asid_pool ptr pool \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>s. \<forall>pool'. ako_at (ASIDPool pool') ptr s \<longrightarrow> asid_pool_integrity {pasSubject aag} aag pool' pool)\<rbrace> set_object ptr (ArchObj (ASIDPool pool)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x1. \<lbrakk>integrity aag X st s; asid_pool_integrity {pasSubject aag} aag x1 pool; kheap s ptr = Some (ArchObj (ASIDPool x1))\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (ASIDPool pool))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x1. \<lbrakk>asid_pool_integrity {pasSubject aag} aag x1 pool; kheap s ptr = Some (ArchObj (ASIDPool x1))\<rbrakk> \<Longrightarrow> integrity aag X s (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (ASIDPool pool))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x1. \<lbrakk>asid_pool_integrity {pasSubject aag} aag x1 pool; kheap s ptr = Some (ArchObj (ASIDPool x1))\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag ptr) (Some (ArchObj (ASIDPool x1))) (Some (ArchObj (ASIDPool pool))) proof (prove)
goal:
No subgoals!
theory ArchArch_AC

lemma delete_asid_respects:
  "\<lbrace>integrity aag X st and pas_refined aag and invs and K (is_subject aag pd)\<rbrace>
   delete_asid asid pd
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" by (wpsimp wp: set_asid_pool_respects_clear hoare_vcg_all_lift
           simp: obj_at_def pas_refined_refl delete_asid_def asid_pool_integrity_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and invs and K (is_subject aag pd)\<rbrace> delete_asid asid pd \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory ArchArch_AC

lemma authorised_arch_inv_sa_update:
  "authorised_arch_inv aag i (scheduler_action_update (\<lambda>_. act) s) =
   authorised_arch_inv aag i s" by (clarsimp simp: authorised_arch_inv_def authorised_page_inv_def authorised_slots_def
              split: arch_invocation.splits page_invocation.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. authorised_arch_inv aag i (scheduler_action_update (\<lambda>_. act) s) = authorised_arch_inv aag i s
theory ArchArch_AC

lemma set_thread_state_authorised_arch_inv[wp]:
  "set_thread_state ref ts \<lbrace>authorised_arch_inv aag i\<rbrace>" unfolding set_thread_state_def apply (wpsimp wp: dxo_wp_weak) apply (clarsimp simp: authorised_arch_inv_def authorised_page_inv_def authorised_slots_def
                    split: arch_invocation.splits page_invocation.splits) apply (wpsimp wp: set_object_wp)+ by (clarsimp simp: authorised_arch_inv_def authorised_page_inv_def authorised_slots_def
              split: arch_invocation.splits page_invocation.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>authorised_arch_inv aag i\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. authorised_arch_inv aag i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>authorised_arch_inv aag i\<rbrace> do tcb <- gets_the $ get_tcb ref;
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
do_extended_op (set_thread_state_ext ref)
od \<lbrace>\<lambda>_. authorised_arch_inv aag i\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s f. authorised_arch_inv aag i (trans_state f s) = authorised_arch_inv aag i s
 2. \<And>tcb. \<lbrace>?B2 tcb\<rbrace> set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>)) \<lbrace>\<lambda>x. authorised_arch_inv aag i\<rbrace>
 3. \<lbrace>?Q1\<rbrace> gets_the $ get_tcb ref \<lbrace>?B2\<rbrace>
 4. \<And>s. authorised_arch_inv aag i s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B2 tcb\<rbrace> set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>)) \<lbrace>\<lambda>x. authorised_arch_inv aag i\<rbrace>
 2. \<lbrace>?Q1\<rbrace> gets_the $ get_tcb ref \<lbrace>?B2\<rbrace>
 3. \<And>s. authorised_arch_inv aag i s \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>authorised_arch_inv aag i s; get_tcb ref s = Some y\<rbrakk> \<Longrightarrow> authorised_arch_inv aag i (s\<lparr>kheap := (kheap s)(ref \<mapsto> TCB (y\<lparr>tcb_state := ts\<rparr>))\<rparr>)
theory Finalise_AC

lemma tcb_sched_action_dequeue_integrity':
  "\<lbrace>integrity aag X st and pas_refined aag and
    (\<lambda>s. pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s thread))))\<rbrace>
   tcb_sched_action tcb_sched_dequeue thread
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (wpsimp simp: tcb_sched_action_def) apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def
                        tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def
                 split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and (\<lambda>s. pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s thread))))\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>integrity aag X st s; pas_refined aag s; pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s thread)))\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. integrity aag X st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) thread s) thread s proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma tcb_sched_action_append_integrity':
  "\<lbrace>integrity aag X st and
    (\<lambda>s. pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s thread))))\<rbrace>
   tcb_sched_action tcb_sched_append thread
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: tcb_sched_action_def) apply wp apply (clarsimp simp: integrity_def integrity_ready_queues_def etcb_at_def
                 split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>s. pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s thread))))\<rbrace> tcb_sched_action tcb_sched_append thread \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>s. pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s thread))))\<rbrace> do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_append thread queue)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and (\<lambda>s. pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s thread))))) s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. integrity aag X st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_append thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) thread s) thread s proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma tcb_sched_action_append_integrity_pasMayEditReadyQueues:
  "\<lbrace>integrity aag X st and pas_refined aag and K (pasMayEditReadyQueues aag)\<rbrace>
   tcb_sched_action tcb_sched_append thread
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: tcb_sched_action_def) apply wp apply (clarsimp simp: integrity_def integrity_ready_queues_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (pasMayEditReadyQueues aag)\<rbrace> tcb_sched_action tcb_sched_append thread \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and (\<lambda>y. pasMayEditReadyQueues aag)\<rbrace> do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_append thread queue)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and pas_refined aag and (\<lambda>y. pasMayEditReadyQueues aag)) s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. integrity aag X st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_append thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) thread s) thread s proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma reschedule_required_integrity[wp]:
  "reschedule_required \<lbrace>integrity aag X st\<rbrace>" apply (simp add: integrity_def reschedule_required_def) apply (wp | wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> reschedule_required \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> do action <- gets scheduler_action;
y <- case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ();
set_scheduler_action choose_new_thread
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. integrity aag X st s \<Longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> integrity aag X st s) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> integrity aag X st s) proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma tcb_sched_action_ekheap[wp]:
  "tcb_sched_action p1 p2 \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>" apply (simp add: tcb_sched_action_def) apply wp apply (simp add: etcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> tcb_sched_action p1 p2 \<lbrace>\<lambda>_ s. P (ekheap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> do d <- ethread_get tcb_domain p2;
prio <- ethread_get tcb_priority p2;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (p1 p2 queue)
od \<lbrace>\<lambda>_ s. P (ekheap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ekheap s) \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. P (ekheap (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then p1 p2 (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s))) p2 s) p2 s proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma scheduler_action_update_pas_refined[simp]:
  "pas_refined aag (scheduler_action_update (\<lambda>_. param_a) s) = pas_refined aag s" by (simp add: pas_refined_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag (scheduler_action_update (\<lambda>_. param_a) s) = pas_refined aag s
theory Finalise_AC

lemma set_bound_notification_ekheap[wp]:
  "set_bound_notification t st \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>" apply (simp add: set_bound_notification_def) apply (wp set_scheduler_action_wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> set_bound_notification t st \<lbrace>\<lambda>_ s. P (ekheap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := st\<rparr>))
od \<lbrace>\<lambda>_ s. P (ekheap s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma sbn_thread_st_auth[wp]:
  "set_bound_notification t ntfn \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace>" apply (simp add: set_bound_notification_def) apply (wpsimp wp: set_object_wp dxo_wp_weak) apply (clarsimp simp: get_tcb_def thread_st_auth_def tcb_states_of_state_def
                 elim!: rsubst[where P=P, OF _ ext]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_ s. P (thread_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>_ s. P (thread_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>P (thread_st_auth s); get_tcb t s = Some y\<rbrakk> \<Longrightarrow> P (thread_st_auth (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)) proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma unbind_maybe_notification_pas_refined[wp]:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
   unbind_maybe_notification nptr \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (clarsimp simp: unbind_maybe_notification_def) apply (wp set_simple_ko_pas_refined hoare_drop_imps | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> unbind_maybe_notification nptr \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> do ntfn <- get_notification nptr;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- set_notification nptr (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma cancel_all_ipc_pas_refined[wp]:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
   cancel_all_ipc epptr
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (clarsimp simp: cancel_all_ipc_def get_ep_queue_def cong: endpoint.case_cong) apply (rule_tac Q="\<lambda>_. pas_refined aag and pspace_aligned
                                         and valid_vspace_objs
                                         and valid_arch_state"
               in hoare_strengthen_post) apply (wpsimp wp: mapM_x_wp_inv set_thread_state_pas_refined get_simple_ko_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> cancel_all_ipc epptr \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> do ep <- get_endpoint epptr;
case ep of IdleEP \<Rightarrow> return () | SendEP list \<Rightarrow> do y <- set_endpoint epptr IdleEP;
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od | RecvEP list \<Rightarrow> do y <- set_endpoint epptr IdleEP;
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> do ep <- get_endpoint epptr;
case ep of IdleEP \<Rightarrow> return () | SendEP list \<Rightarrow> do y <- set_endpoint epptr IdleEP;
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od | RecvEP list \<Rightarrow> do y <- set_endpoint epptr IdleEP;
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od
od \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
 2. \<And>rv s. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s \<Longrightarrow> pas_refined aag s proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma cancel_all_signals_pas_refined[wp]:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and
     valid_arch_state\<rbrace>
   cancel_all_signals ntfnptr
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (clarsimp simp: cancel_all_signals_def cong: ntfn.case_cong) apply (rule_tac Q="\<lambda>_. pas_refined aag and pspace_aligned
                                         and valid_vspace_objs
                                         and valid_arch_state"
               in hoare_strengthen_post) apply (wpsimp wp: mapM_x_wp_inv set_thread_state_pas_refined get_simple_ko_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> cancel_all_signals ntfnptr \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ntfnptr (ntfn_set_obj ntfn IdleNtfn);
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) queue;
reschedule_required
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ntfnptr (ntfn_set_obj ntfn IdleNtfn);
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) queue;
reschedule_required
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
 2. \<And>rv s. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s \<Longrightarrow> pas_refined aag s proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma thread_set_tcb_fault_reset_invs:
  "thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>invs\<rbrace>" by (rule thread_set_invs_trivial) (clarsimp simp: ran_tcb_cap_cases)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs\<rbrace>
theory Finalise_AC

lemma deleting_irq_handler_pas_refined[wp]:
  "\<lbrace>pas_refined aag and invs and K (is_subject_irq aag irq)\<rbrace>
   deleting_irq_handler irq
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: deleting_irq_handler_def get_irq_slot_def) apply wp apply (fastforce simp: pas_refined_def irq_map_wellformed_aux_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and K (is_subject_irq aag irq)\<rbrace> deleting_irq_handler irq \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and (\<lambda>y. is_subject_irq aag irq)\<rbrace> gets (\<lambda>st. (interrupt_irq_node st irq, [])) >>= cap_delete_one \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and invs and (\<lambda>y. is_subject_irq aag irq)) s \<Longrightarrow> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (valid_mdb and K (is_subject aag (fst (interrupt_irq_node s irq, []))))) s proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma bound_tcb_at_thread_bound_ntfns:
  "bound_tcb_at ((=) ntfn) t s \<Longrightarrow> thread_bound_ntfns s t = ntfn" by (clarsimp simp: thread_bound_ntfns_def pred_tcb_at_def obj_at_def get_tcb_def
              split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bound_tcb_at ((=) ntfn) t s \<Longrightarrow> thread_bound_ntfns s t = ntfn
theory Finalise_AC

lemma bound_tcb_at_implies_receive:
  "\<lbrakk> pas_refined aag s; bound_tcb_at ((=) (Some x)) t s \<rbrakk>
     \<Longrightarrow> abs_has_auth_to aag Receive t x" by (fastforce dest!: bound_tcb_at_thread_bound_ntfns sta_bas pas_refined_mem)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; bound_tcb_at ((=) (Some x)) t s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag
theory Finalise_AC

lemma bound_tcb_at_implies_reset:
  "\<lbrakk> pas_refined aag s; bound_tcb_at ((=) (Some x)) t s \<rbrakk>
     \<Longrightarrow> abs_has_auth_to aag Reset t x" by (fastforce dest!: bound_tcb_at_thread_bound_ntfns sta_bas pas_refined_mem)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; bound_tcb_at ((=) (Some x)) t s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag t, Reset, pasObjectAbs aag x) \<in> pasPolicy aag
theory Finalise_AC

lemma cap_delete_one_respects[wp,wp_not_transferable]:
  "\<lbrace>integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))\<rbrace>
   cap_delete_one slot
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: cap_delete_one_def unless_def bind_assoc) apply (wpsimp wp: hoare_drop_imps get_cap_auth_wp [where aag = aag]) apply (fastforce simp: caps_of_state_valid) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and einvs and (\<lambda>y. is_subject aag (fst slot))\<rbrace> do cap <- get_cap slot;
when (cap \<noteq> NullCap) (do final <- is_final_cap cap;
y <- fast_finalise cap final;
empty_slot slot NullCap
od)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>integrity aag X st s; pas_refined aag s; invs s; valid_list s; valid_sched s; is_subject aag (fst slot); cap \<noteq> NullCap; caps_of_state s slot = Some cap; pas_cap_cur_auth aag cap\<rbrakk> \<Longrightarrow> s \<turnstile> cap \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma fast_finalise_is_transferable[wp_transferable]:
  "\<lbrace>P and K (is_transferable (Some cap))\<rbrace>
   fast_finalise cap final
   \<lbrace>\<lambda>_. P\<rbrace>" by (rule hoare_gen_asm) (erule is_transferable.cases; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and K (is_transferable_cap cap)\<rbrace> fast_finalise cap final \<lbrace>\<lambda>_. P\<rbrace>