theory KHeap_DR

lemma fast_finalise_corres:
  "dcorres dc \<top> (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.fast_finalise (transform_cap rv') final)
   (IpcCancel_A.fast_finalise rv' final)" apply (case_tac rv') apply (simp_all add:transform_cap_def) apply (simp_all add:PageTableUnmap_D.fast_finalise_def corres_free_fail) apply (simp_all add:when_def) apply (clarsimp simp:dcorres_cancel_all_ipc) apply clarsimp apply (rule corres_guard_imp) apply (rule corres_split) apply (rule dcorres_unbind_maybe_notification) apply (rule dcorres_cancel_all_signals) apply (wp unbind_notification_valid_etcbs unbind_maybe_notification_valid_etcbs | simp add:  | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.fast_finalise (transform_cap rv') final) (IpcCancel_A.fast_finalise rv' final) proof (prove)
goal (12 subgoals):
 1. rv' = cap.NullCap \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.fast_finalise (transform_cap rv') final) (IpcCancel_A.fast_finalise rv' final)
 2. \<And>x21 x22 x23 x24. rv' = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.fast_finalise (transform_cap rv') final) (IpcCancel_A.fast_finalise rv' final)
 3. \<And>x31 x32 x33. rv' = cap.EndpointCap x31 x32 x33 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.fast_finalise (transform_cap rv') final) (IpcCancel_A.fast_finalise rv' final)
 4. \<And>x41 x42 x43. rv' = cap.NotificationCap x41 x42 x43 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.fast_finalise (transform_cap rv') final) (IpcCancel_A.fast_finalise rv' final)
 5. \<And>x51 x52 x53. rv' = cap.ReplyCap x51 x52 x53 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.fast_finalise (transform_cap rv') final) (IpcCancel_A.fast_finalise rv' final)
 6. \<And>x61 x62 x63. rv' = cap.CNodeCap x61 x62 x63 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.fast_finalise (transform_cap rv') final) (IpcCancel_A.fast_finalise rv' final)
 7. \<And>x7. rv' = ThreadCap x7 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.fast_finalise (transform_cap rv') final) (IpcCancel_A.fast_finalise rv' final)
 8. rv' = cap.DomainCap \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.fast_finalise (transform_cap rv') final) (IpcCancel_A.fast_finalise rv' final)
 9. rv' = IRQControlCap \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.fast_finalise (transform_cap rv') final) (IpcCancel_A.fast_finalise rv' final)
 10. \<And>x10. rv' = IRQHandlerCap x10 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.fast_finalise (transform_cap rv') final) (IpcCancel_A.fast_finalise rv' final)
A total of 12 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>x21 x22 x23 x24. rv' = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) fail fail
 2. \<And>x31 x32 x33. rv' = cap.EndpointCap x31 x32 x33 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (when final (PageTableUnmap_D.cancel_all_ipc x31)) (when final (IpcCancel_A.cancel_all_ipc x31))
 3. \<And>x41 x42 x43. rv' = cap.NotificationCap x41 x42 x43 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (when final (do y <- PageTableUnmap_D.unbind_maybe_notification x41;
PageTableUnmap_D.cancel_all_ipc x41
od)) (when final (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od))
 4. \<And>x61 x62 x63. rv' = cap.CNodeCap x61 x62 x63 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) fail fail
 5. \<And>x7. rv' = ThreadCap x7 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) fail fail
 6. rv' = cap.DomainCap \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (return ()) fail
 7. rv' = IRQControlCap \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) fail fail
 8. \<And>x10. rv' = IRQHandlerCap x10 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) fail fail
 9. \<And>x111 x112 x113. rv' = Zombie x111 x112 x113 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) fail fail
 10. \<And>x12. rv' = ArchObjectCap x12 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.fast_finalise (case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)) final) fail proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33. rv' = cap.EndpointCap x31 x32 x33 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (when final (PageTableUnmap_D.cancel_all_ipc x31)) (when final (IpcCancel_A.cancel_all_ipc x31))
 2. \<And>x41 x42 x43. rv' = cap.NotificationCap x41 x42 x43 \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (when final (do y <- PageTableUnmap_D.unbind_maybe_notification x41;
PageTableUnmap_D.cancel_all_ipc x41
od)) (when final (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od)) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33. rv' = cap.EndpointCap x31 x32 x33 \<Longrightarrow> final \<longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.cancel_all_ipc x31) (IpcCancel_A.cancel_all_ipc x31)
 2. \<And>x41 x42 x43. rv' = cap.NotificationCap x41 x42 x43 \<Longrightarrow> final \<longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (do y <- PageTableUnmap_D.unbind_maybe_notification x41;
PageTableUnmap_D.cancel_all_ipc x41
od) (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od) proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43. rv' = cap.NotificationCap x41 x42 x43 \<Longrightarrow> final \<longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (do y <- PageTableUnmap_D.unbind_maybe_notification x41;
PageTableUnmap_D.cancel_all_ipc x41
od) (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od) proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (do y <- PageTableUnmap_D.unbind_maybe_notification x41;
PageTableUnmap_D.cancel_all_ipc x41
od) (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od) proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42 x43. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final\<rbrakk> \<Longrightarrow> dcorres dc (?Q8 x41 x42 x43) (?Q'8 x41 x42 x43) (do y <- PageTableUnmap_D.unbind_maybe_notification x41;
PageTableUnmap_D.cancel_all_ipc x41
od) (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od)
 2. \<And>x41 x42 x43 s. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final; True\<rbrakk> \<Longrightarrow> ?Q8 x41 x42 x43 s
 3. \<And>x41 x42 x43 s. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final; (valid_state and valid_idle and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'8 x41 x42 x43 s proof (prove)
goal (6 subgoals):
 1. \<And>x41 x42 x43. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final\<rbrakk> \<Longrightarrow> dcorres (?r'12 x41 x42 x43) (?P12 x41 x42 x43) (?P'12 x41 x42 x43) (PageTableUnmap_D.unbind_maybe_notification x41) (IpcCancel_A.unbind_maybe_notification x41)
 2. \<And>x41 x42 x43 y ya. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final; ?r'12 x41 x42 x43 y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R12 x41 x42 x43 y) (?R'12 x41 x42 x43 ya) (PageTableUnmap_D.cancel_all_ipc x41) (cancel_all_signals x41)
 3. \<And>x41 x42 x43. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 x41 x42 x43\<rbrace> PageTableUnmap_D.unbind_maybe_notification x41 \<lbrace>?R12 x41 x42 x43\<rbrace>
 4. \<And>x41 x42 x43. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final\<rbrakk> \<Longrightarrow> \<lbrace>?Q'12 x41 x42 x43\<rbrace> IpcCancel_A.unbind_maybe_notification x41 \<lbrace>?R'12 x41 x42 x43\<rbrace>
 5. \<And>x41 x42 x43 s. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final; True\<rbrakk> \<Longrightarrow> (?P12 x41 x42 x43 and ?Q12 x41 x42 x43) s
 6. \<And>x41 x42 x43 s. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final; (valid_state and valid_idle and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'12 x41 x42 x43 and ?Q'12 x41 x42 x43) s proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 x43 y ya. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R12 x41 x42 x43 y) (?R'12 x41 x42 x43 ya) (PageTableUnmap_D.cancel_all_ipc x41) (cancel_all_signals x41)
 2. \<And>x41 x42 x43. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 x41 x42 x43\<rbrace> PageTableUnmap_D.unbind_maybe_notification x41 \<lbrace>?R12 x41 x42 x43\<rbrace>
 3. \<And>x41 x42 x43. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final\<rbrakk> \<Longrightarrow> \<lbrace>?Q'12 x41 x42 x43\<rbrace> IpcCancel_A.unbind_maybe_notification x41 \<lbrace>?R'12 x41 x42 x43\<rbrace>
 4. \<And>x41 x42 x43 s. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12 x41 x42 x43) s
 5. \<And>x41 x42 x43 s. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final; (valid_state and valid_idle and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_etcbs and valid_idle and valid_state and ?Q'12 x41 x42 x43) s proof (prove)
goal (4 subgoals):
 1. \<And>x41 x42 x43. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 x41 x42 x43\<rbrace> PageTableUnmap_D.unbind_maybe_notification x41 \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>x41 x42 x43. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final\<rbrakk> \<Longrightarrow> \<lbrace>?Q'12 x41 x42 x43\<rbrace> IpcCancel_A.unbind_maybe_notification x41 \<lbrace>\<lambda>ya. valid_state and valid_idle and valid_etcbs\<rbrace>
 3. \<And>x41 x42 x43 s. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12 x41 x42 x43) s
 4. \<And>x41 x42 x43 s. \<lbrakk>rv' = cap.NotificationCap x41 x42 x43; final; (valid_state and valid_idle and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_etcbs and valid_idle and valid_state and ?Q'12 x41 x42 x43) s proof (prove)
goal:
No subgoals!