theory KHeap_R

lemma getNotification_corres:
  "corres ntfn_relation (ntfn_at ptr) (ntfn_at' ptr)
     (get_notification ptr) (getNotification ptr)" apply (rule corres_no_failI) apply wp apply (simp add: get_simple_ko_def getNotification_def get_object_def
                   getObject_def bind_assoc) apply (clarsimp simp: in_monad split_def bind_def gets_def get_def return_def) apply (clarsimp simp: assert_def fail_def obj_at_def return_def is_ntfn partial_inv_def) apply (clarsimp simp: loadObject_default_def in_monad projectKOs
                        in_magnitude_check objBits_simps') apply (clarsimp simp add: state_relation_def pspace_relation_def) apply (drule bspec) apply blast apply (simp add: other_obj_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres ntfn_relation (ntfn_at ptr) (ntfn_at' ptr) (get_notification ptr) (getNotification ptr) proof (prove)
goal (2 subgoals):
 1. True \<Longrightarrow> no_fail (ntfn_at' ptr) (getNotification ptr)
 2. \<forall>(s, s')\<in>state_relation. ntfn_at ptr s \<and> ntfn_at' ptr s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getNotification ptr s'). \<exists>(r, t)\<in>fst (get_notification ptr s). (t, t') \<in> state_relation \<and> ntfn_relation r r') proof (prove)
goal (1 subgoal):
 1. \<forall>(s, s')\<in>state_relation. ntfn_at ptr s \<and> ntfn_at' ptr s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getNotification ptr s'). \<exists>(r, t)\<in>fst (get_notification ptr s). (t, t') \<in> state_relation \<and> ntfn_relation r r') proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> ntfn_at ptr s \<and> ntfn_at' ptr s' \<longrightarrow> (\<forall>x\<in>fst ((do map <- gets ksPSpace;
case lookupAround2 ptr map of (before, after) \<Rightarrow> do (ptr', y) <- assert_opt before;
loadObject_default ptr ptr' after y
od
od) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((do x <- gets kheap;
y <- assert (\<exists>y. x ptr = Some y);
y <- assert (a_type (the (x ptr)) = AEndpoint \<or> a_type (the (x ptr)) = ANTFN);
case partial_inv Notification (the (x ptr)) of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2
od) s). case x of (r, t) \<Rightarrow> (t, t') \<in> state_relation \<and> ntfn_relation r r') proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bc. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 ptr (ksPSpace b)) = Some (aa, ba); (ab, bc) \<in> fst (loadObject_default ptr aa (snd (lookupAround2 ptr (ksPSpace b))) ba b); ntfn_at ptr a; ntfn_at' ptr b\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (assert (\<exists>y. kheap a ptr = Some y) a). \<exists>y\<in>fst (assert (a_type (the (kheap a ptr)) = AEndpoint \<or> a_type (the (kheap a ptr)) = ANTFN) (snd y)). \<exists>x\<in>fst ((case partial_inv Notification (the (kheap a ptr)) of None \<Rightarrow> fail | Some x2 \<Rightarrow> \<lambda>s. ({(x2, s)}, False)) (snd y)). (snd x, bc) \<in> state_relation \<and> ntfn_relation (fst x) ab proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bc ep. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 ptr (ksPSpace b)) = Some (aa, ba); (ab, bc) \<in> fst (loadObject_default ptr aa (snd (lookupAround2 ptr (ksPSpace b))) ba b); ntfn_at' ptr b; kheap a ptr = Some (Notification ep)\<rbrakk> \<Longrightarrow> (a, bc) \<in> state_relation \<and> ntfn_relation ep ab proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ep. \<lbrakk>(a, b) \<in> state_relation; ksPSpace b ptr = Some (KONotification ab); ntfn_at' ptr b; kheap a ptr = Some (Notification ep); is_aligned ptr 4; ps_clear ptr 4 b\<rbrakk> \<Longrightarrow> ntfn_relation ep ab proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ep. \<lbrakk>ksPSpace b ptr = Some (KONotification ab); ntfn_at' ptr b; kheap a ptr = Some (Notification ep); is_aligned ptr 4; ps_clear ptr 4 b; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>xa\<in>obj_relation_cuts (the (kheap a x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap a x)) (the (ksPSpace b y)); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b\<rbrakk> \<Longrightarrow> ntfn_relation ep ab proof (prove)
goal (2 subgoals):
 1. \<And>a b ab ep. \<lbrakk>ksPSpace b ptr = Some (KONotification ab); ntfn_at' ptr b; kheap a ptr = Some (Notification ep); is_aligned ptr 4; ps_clear ptr 4 b; pspace_dom (kheap a) = dom (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b\<rbrakk> \<Longrightarrow> ?x96 a b ab ep \<in> dom (kheap a)
 2. \<And>a b ab ep. \<lbrakk>ksPSpace b ptr = Some (KONotification ab); ntfn_at' ptr b; kheap a ptr = Some (Notification ep); is_aligned ptr 4; ps_clear ptr 4 b; pspace_dom (kheap a) = dom (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<forall>x\<in>obj_relation_cuts (the (kheap a (?x96 a b ab ep))) (?x96 a b ab ep). case x of (y, P) \<Rightarrow> P (the (kheap a (?x96 a b ab ep))) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> ntfn_relation ep ab proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ep. \<lbrakk>ksPSpace b ptr = Some (KONotification ab); ntfn_at' ptr b; kheap a ptr = Some (Notification ep); is_aligned ptr 4; ps_clear ptr 4 b; pspace_dom (kheap a) = dom (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<forall>x\<in>obj_relation_cuts (the (kheap a ptr)) ptr. case x of (y, P) \<Rightarrow> P (the (kheap a ptr)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> ntfn_relation ep ab proof (prove)
goal:
No subgoals!