theory IpcCancel_C

lemma ccorres_pre_getQueue:
  assumes cc: "\<And>queue. ccorres r xf (P queue) (P' queue) hs (f queue) c"
  shows   "ccorres r xf (\<lambda>s. P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority)
                        {s'. \<forall>queue. (let cqueue = index (ksReadyQueues_' (globals s'))
                                                         (cready_queues_index_to_C d p) in
                                      sched_queue_relation' (cslift s') queue (head_C cqueue) (end_C cqueue)) \<longrightarrow> s' \<in> P' queue}
           hs (getQueue d p >>= (\<lambda>queue. f queue)) c" apply (rule ccorres_guard_imp2) apply (rule ccorres_symb_exec_l2) defer defer apply (rule gq_sp) defer apply (rule ccorres_guard_imp) apply (rule cc) apply clarsimp apply assumption apply assumption apply (clarsimp simp: getQueue_def gets_exs_valid) apply clarsimp apply (drule spec, erule mp) apply (simp add: Let_def) apply (erule rf_sr_sched_queue_relation) apply (simp add: maxDom_to_H maxPrio_to_H)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (\<lambda>s. P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority) {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C d p] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> P' queue} hs (getQueue d p >>= f) c proof (prove)
goal (2 subgoals):
 1. ccorres r xf ?Q ?Q' hs (getQueue d p >>= f) c
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority; s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C d p] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> P' queue}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (4 subgoals):
 1. \<And>queue. ccorres r xf (?Q3 queue) (?Q'3 queue) hs (f queue) c
 2. \<And>s. ?Q s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getQueue d p \<lbrace>?Q3\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority; s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C d p] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> P' queue}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q3 rv s \<longrightarrow> s' \<in> ?Q'3 rv} proof (prove)
goal (4 subgoals):
 1. \<And>s. ?Q s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrace>?Q\<rbrace> getQueue d p \<lbrace>?Q3\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority; s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C d p] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> P' queue}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q3 rv s \<longrightarrow> s' \<in> ?Q'3 rv}
 4. \<And>queue. ccorres r xf (?Q3 queue) (?Q'3 queue) hs (f queue) c proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q\<rbrace> getQueue d p \<lbrace>?Q3\<rbrace>
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority; s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C d p] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> P' queue}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q3 rv s \<longrightarrow> s' \<in> ?Q'3 rv}
 3. \<And>queue. ccorres r xf (?Q3 queue) (?Q'3 queue) hs (f queue) c
 4. \<And>s. ?Q s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority; s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C d p] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> P' queue}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?Q and (\<lambda>s. ksReadyQueues s (d, p) = rv)) s \<longrightarrow> s' \<in> ?Q'3 rv}
 2. \<And>queue. ccorres r xf (?Q and (\<lambda>s. ksReadyQueues s (d, p) = queue)) (?Q'3 queue) hs (f queue) c
 3. \<And>s. ?Q s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>queue. ccorres r xf (?Q and (\<lambda>s. ksReadyQueues s (d, p) = queue)) (?Q'3 queue) hs (f queue) c
 2. \<And>s. ?Q s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority; s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C d p] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> P' queue}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?Q and (\<lambda>s. ksReadyQueues s (d, p) = rv)) s \<longrightarrow> s' \<in> ?Q'3 rv} proof (prove)
goal (5 subgoals):
 1. \<And>queue. ccorres r xf (?Q8 queue) (?Q'8 queue) hs (f queue) c
 2. \<And>queue s. (?Q and (\<lambda>s. ksReadyQueues s (d, p) = queue)) s \<Longrightarrow> ?Q8 queue s
 3. \<And>queue s. s \<in> ?Q'3 queue \<Longrightarrow> s \<in> ?Q'8 queue
 4. \<And>s. ?Q s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority; s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C d p] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> P' queue}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?Q and (\<lambda>s. ksReadyQueues s (d, p) = rv)) s \<longrightarrow> s' \<in> ?Q'3 rv} proof (prove)
goal (4 subgoals):
 1. \<And>queue s. (?Q and (\<lambda>s. ksReadyQueues s (d, p) = queue)) s \<Longrightarrow> P queue s
 2. \<And>queue s. s \<in> ?Q'3 queue \<Longrightarrow> s \<in> P' queue
 3. \<And>s. ?Q s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority; s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C d p] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> P' queue}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?Q and (\<lambda>s. ksReadyQueues s (d, p) = rv)) s \<longrightarrow> s' \<in> ?Q'3 rv} proof (prove)
goal (4 subgoals):
 1. \<And>s. ?Q s \<Longrightarrow> P (ksReadyQueues s (d, p)) s
 2. \<And>queue s. s \<in> ?Q'3 queue \<Longrightarrow> s \<in> P' queue
 3. \<And>s. ?Q s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority; s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C d p] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> P' queue}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?Q and (\<lambda>s. ksReadyQueues s (d, p) = rv)) s \<longrightarrow> s' \<in> ?Q'3 rv} proof (prove)
goal (3 subgoals):
 1. \<And>queue s. s \<in> ?Q'3 queue \<Longrightarrow> s \<in> P' queue
 2. \<And>s. P (ksReadyQueues s (d, p)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority; s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C d p] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> P' queue}\<rbrakk> \<Longrightarrow> P (ksReadyQueues s (d, p)) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. P (ksReadyQueues s (d, p)) s) and (\<lambda>s. ksReadyQueues s (d, p) = rv)) s \<longrightarrow> s' \<in> ?Q'3 rv} proof (prove)
goal (2 subgoals):
 1. \<And>s. P (ksReadyQueues s (d, p)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority; s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C d p] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> P' queue}\<rbrakk> \<Longrightarrow> P (ksReadyQueues s (d, p)) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. P (ksReadyQueues s (d, p)) s) and (\<lambda>s. ksReadyQueues s (d, p) = rv)) s \<longrightarrow> s' \<in> P' rv} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority; s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C d p] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> P' queue}\<rbrakk> \<Longrightarrow> P (ksReadyQueues s (d, p)) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. P (ksReadyQueues s (d, p)) s) and (\<lambda>s. ksReadyQueues s (d, p) = rv)) s \<longrightarrow> s' \<in> P' rv} proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa. \<lbrakk>(s, s') \<in> rf_sr; \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C d p] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> P' queue; P (ksReadyQueues s (d, p)) s; d \<le> maxDomain; p \<le> maxPriority; (sa, s') \<in> rf_sr; P (ksReadyQueues sa (d, p)) sa\<rbrakk> \<Longrightarrow> s' \<in> P' (ksReadyQueues sa (d, p)) proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s; d \<le> maxDomain; p \<le> maxPriority; (sa, s') \<in> rf_sr; P (ksReadyQueues sa (d, p)) sa\<rbrakk> \<Longrightarrow> let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C d p] in sched_queue_relation' (cslift s') (ksReadyQueues sa (d, p)) (head_C cqueue) (StateRelation_C.end_C cqueue) proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s; d \<le> maxDomain; p \<le> maxPriority; (sa, s') \<in> rf_sr; P (ksReadyQueues sa (d, p)) sa\<rbrakk> \<Longrightarrow> sched_queue_relation' (cslift s') (ksReadyQueues sa (d, p)) (head_C (ksReadyQueues_' (globals s').[cready_queues_index_to_C d p])) (StateRelation_C.end_C (ksReadyQueues_' (globals s').[cready_queues_index_to_C d p])) proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s; d \<le> maxDomain; p \<le> maxPriority; P (ksReadyQueues sa (d, p)) sa\<rbrakk> \<Longrightarrow> d \<le> UCAST(32 signed \<rightarrow> 8) maxDom
 2. \<And>s s' sa. \<lbrakk>(s, s') \<in> rf_sr; P (ksReadyQueues s (d, p)) s; d \<le> maxDomain; p \<le> maxPriority; P (ksReadyQueues sa (d, p)) sa\<rbrakk> \<Longrightarrow> p \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio proof (prove)
goal:
No subgoals!