kings-crown/FVELER_Isabelle huggingface dataset:
theory IpcCancel_C

lemma ntfn_ptr_get_queue_spec:
  "\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> \<sigma> \<Turnstile>\<^sub>c \<^bsup>\<sigma>\<^esup>ntfnPtr} \<acute>ret__struct_tcb_queue_C :== PROC ntfn_ptr_get_queue(\<acute>ntfnPtr)
       \<lbrace>head_C \<acute>ret__struct_tcb_queue_C = Ptr (ntfnQueue_head_CL (notification_lift (the (cslift s \<^bsup>s\<^esup>ntfnPtr)))) \<and>
        end_C \<acute>ret__struct_tcb_queue_C = Ptr (ntfnQueue_tail_CL (notification_lift (the (cslift s \<^bsup>s\<^esup>ntfnPtr))))\<rbrace>" apply vcg apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {\<sigma>. s = \<sigma> \<and> \<sigma> \<Turnstile>\<^sub>c ntfnPtr_' \<sigma>} Call ntfn_ptr_get_queue_'proc \<lbrace>head_C \<acute>ret__struct_tcb_queue_C = tcb_Ptr (ntfnQueue_head_CL (notification_lift (the (cslift s \<^bsup>s\<^esup>ntfnPtr)))) \<and> StateRelation_C.end_C \<acute>ret__struct_tcb_queue_C = tcb_Ptr (ntfnQueue_tail_CL (notification_lift (the (cslift s \<^bsup>s\<^esup>ntfnPtr))))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t_hrs ntfnPtr. hrs_htd t_hrs \<Turnstile>\<^sub>t ntfnPtr \<Longrightarrow> \<forall>v. hrs_htd t_hrs \<Turnstile>\<^sub>t ntfnPtr \<and> (\<forall>ret__unsigned. ret__unsigned = ntfnQueue_head_CL (notification_lift (the (clift t_hrs ntfnPtr))) \<longrightarrow> hrs_htd t_hrs \<Turnstile>\<^sub>t ntfnPtr \<and> (\<forall>ret__unsigned. ret__unsigned = ntfnQueue_tail_CL (notification_lift (the (clift t_hrs ntfnPtr))) \<longrightarrow> head_C (tcb_queue_C.end_C_update (\<lambda>_. tcb_Ptr (UCAST(32 \<rightarrow> 32) (ntfnQueue_tail_CL (notification_lift (the (clift t_hrs ntfnPtr)))))) (head_C_update (\<lambda>_. tcb_Ptr (UCAST(32 \<rightarrow> 32) (ntfnQueue_head_CL (notification_lift (the (clift t_hrs ntfnPtr)))))) v)) = tcb_Ptr (ntfnQueue_head_CL (notification_lift (the (clift t_hrs ntfnPtr)))) \<and> StateRelation_C.end_C (tcb_queue_C.end_C_update (\<lambda>_. tcb_Ptr (UCAST(32 \<rightarrow> 32) (ntfnQueue_tail_CL (notification_lift (the (clift t_hrs ntfnPtr)))))) (head_C_update (\<lambda>_. tcb_Ptr (UCAST(32 \<rightarrow> 32) (ntfnQueue_head_CL (notification_lift (the (clift t_hrs ntfnPtr)))))) v)) = tcb_Ptr (ntfnQueue_tail_CL (notification_lift (the (clift t_hrs ntfnPtr)))))) proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma ntfn_ptr_set_queue_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>ntfnPtr\<rbrace> Call ntfn_ptr_set_queue_'proc
           {t. (\<exists>ntfn'. notification_lift ntfn' =
  (notification_lift (the (cslift s (\<^bsup>s\<^esup>ntfnPtr))))\<lparr> ntfnQueue_head_CL := ptr_val (head_C \<^bsup>s\<^esup>ntfn_queue) && ~~ mask 4,
                                                      ntfnQueue_tail_CL := ptr_val (end_C \<^bsup>s\<^esup>ntfn_queue) && ~~ mask 4 \<rparr>
            \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (\<^bsup>s\<^esup>ntfnPtr) ntfn')
                (t_hrs_' (globals s)))}" apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: packed_heap_update_collapse_hrs typ_heap_simps') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>ntfnPtr\<rbrace> Call ntfn_ptr_set_queue_'proc \<lbrace>\<exists>ntfn'. notification_lift ntfn' = notification_lift (the (cslift s \<^bsup>s\<^esup>ntfnPtr))\<lparr>ntfnQueue_head_CL := ptr_val (head_C \<^bsup>s\<^esup>ntfn_queue) && ~~ mask 4, ntfnQueue_tail_CL := ptr_val (StateRelation_C.end_C \<^bsup>s\<^esup>ntfn_queue) && ~~ mask 4\<rparr> \<and> \<acute>t_hrs = hrs_mem_update (heap_update \<^bsup>s\<^esup>ntfnPtr ntfn') \<^bsup>s\<^esup>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>ntfnPtr\<rbrace> \<subseteq> {sa. sa \<Turnstile>\<^sub>c ntfnPtr_' sa \<and> (\<forall>t. (\<exists>notification. notification_lift notification = notification_lift (the (cslift sa (ntfnPtr_' sa)))\<lparr>ntfnQueue_head_CL := UCAST(32 \<rightarrow> 32) (ptr_val (head_C (ntfn_queue_' sa))) && ~~ mask 4\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfnPtr_' sa) notification) (t_hrs_' (globals sa))) \<longrightarrow> t \<Turnstile>\<^sub>c ntfnPtr_' sa \<and> (\<forall>ta. (\<exists>notification. notification_lift notification = notification_lift (the (cslift t (ntfnPtr_' sa)))\<lparr>ntfnQueue_tail_CL := UCAST(32 \<rightarrow> 32) (ptr_val (StateRelation_C.end_C (ntfn_queue_' sa))) && ~~ mask 4\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfnPtr_' sa) notification) (t_hrs_' (globals t))) \<longrightarrow> (\<exists>ntfn'. notification_lift ntfn' = notification_lift (the (cslift s (ntfnPtr_' s)))\<lparr>ntfnQueue_head_CL := ptr_val (head_C (ntfn_queue_' s)) && ~~ mask 4, ntfnQueue_tail_CL := ptr_val (StateRelation_C.end_C (ntfn_queue_' s)) && ~~ mask 4\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfnPtr_' s) ntfn') (t_hrs_' (globals s)))))} proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma ko_at_obj_congD':
  "\<lbrakk>ko_at' k p s; ko_at' k' p s\<rbrakk> \<Longrightarrow> k = k'" apply (erule obj_atE')+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' k p s; ko_at' k' p s\<rbrakk> \<Longrightarrow> k = k' proof (prove)
goal (1 subgoal):
 1. \<And>ko obj koa obja. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; obj = k; ps_clear p (objBitsKO ko) s; ksPSpace s p = Some koa; is_aligned p (objBitsKO koa); fst (projectKO koa s) = {(obja, s)}; obja = k'; ps_clear p (objBitsKO koa) s\<rbrakk> \<Longrightarrow> k = k' proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma ctcb_ptr_to_tcb_ptr_imageI:
  "ctcb_ptr_to_tcb_ptr x \<in> S \<Longrightarrow> x \<in> tcb_ptr_to_ctcb_ptr ` S" apply (drule imageI [where f = tcb_ptr_to_ctcb_ptr]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctcb_ptr_to_tcb_ptr x \<in> S \<Longrightarrow> x \<in> tcb_ptr_to_ctcb_ptr ` S proof (prove)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr x) \<in> tcb_ptr_to_ctcb_ptr ` S \<Longrightarrow> x \<in> tcb_ptr_to_ctcb_ptr ` S proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma tcb_queue'_head_end_NULL:
  assumes qr: "tcb_queue_relation' getNext getPrev mp queue qhead qend"
  and   tat: "\<forall>t\<in>set queue. tcb_at' t s"
  shows "(qend = NULL) = (qhead = NULL)" using qr tat apply - apply (erule tcb_queue_relationE') apply (simp add: tcb_queue_head_empty_iff) apply (rule impI) apply (rule tcb_at_not_NULL) apply (erule bspec) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (qend = NULL) = (qhead = NULL) proof (prove)
using this:
tcb_queue_relation' getNext getPrev mp queue qhead qend
\<forall>t\<in>set queue. tcb_at' t s

goal (1 subgoal):
 1. (qend = NULL) = (qhead = NULL) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation' getNext getPrev mp queue qhead qend; \<forall>t\<in>set queue. tcb_at' t s\<rbrakk> \<Longrightarrow> (qend = NULL) = (qhead = NULL) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t\<in>set queue. tcb_at' t s; tcb_queue_relation getNext getPrev mp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> (qend = NULL) = (qhead = NULL) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t\<in>set queue. tcb_at' t s; tcb_queue_relation getNext getPrev mp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> queue \<noteq> [] \<longrightarrow> tcb_ptr_to_ctcb_ptr (last queue) \<noteq> NULL proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t\<in>set queue. tcb_at' t s; tcb_queue_relation getNext getPrev mp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue)); queue \<noteq> []\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr (last queue) \<noteq> NULL proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t\<in>set queue. tcb_at' t s; tcb_queue_relation getNext getPrev mp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue)); queue \<noteq> []\<rbrakk> \<Longrightarrow> tcb_at' (last queue) ?s10 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue)); queue \<noteq> []\<rbrakk> \<Longrightarrow> last queue \<in> set queue proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma tcb_queue_relation_qhead_mem:
  "\<lbrakk> tcb_queue_relation getNext getPrev mp queue NULL qhead;
  (\<forall>tcb\<in>set queue. tcb_at' tcb t) \<rbrakk>
  \<Longrightarrow> qhead \<noteq> NULL \<longrightarrow> ctcb_ptr_to_tcb_ptr qhead \<in> set queue" by (clarsimp simp: tcb_queue_head_empty_iff tcb_queue_relation_head_hd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; \<forall>tcb\<in>set queue. tcb_at' tcb t\<rbrakk> \<Longrightarrow> qhead \<noteq> NULL \<longrightarrow> ctcb_ptr_to_tcb_ptr qhead \<in> set queue
theory IpcCancel_C

lemma tcb_queue_relation_qhead_valid:
  "\<lbrakk> tcb_queue_relation getNext getPrev (cslift s') queue NULL qhead;
  (s, s') \<in> rf_sr; (\<forall>tcb\<in>set queue. tcb_at' tcb s) \<rbrakk>
  \<Longrightarrow> qhead \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c qhead" apply (frule (1) tcb_queue_relation_qhead_mem) apply clarsimp apply(drule (3) tcb_queue_memberD) apply (simp add: h_t_valid_clift_Some_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev (cslift s') queue NULL qhead; (s, s') \<in> rf_sr; \<forall>tcb\<in>set queue. tcb_at' tcb s\<rbrakk> \<Longrightarrow> qhead \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c qhead proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev (cslift s') queue NULL qhead; (s, s') \<in> rf_sr; \<forall>tcb\<in>set queue. tcb_at' tcb s; qhead \<noteq> NULL \<longrightarrow> ctcb_ptr_to_tcb_ptr qhead \<in> set queue\<rbrakk> \<Longrightarrow> qhead \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c qhead proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev (cslift s') queue NULL qhead; (s, s') \<in> rf_sr; \<forall>tcb\<in>set queue. tcb_at' tcb s; qhead \<noteq> NULL; ctcb_ptr_to_tcb_ptr qhead \<in> set queue\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c qhead proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; \<forall>tcb\<in>set queue. tcb_at' tcb s; qhead \<noteq> NULL; ctcb_ptr_to_tcb_ptr qhead \<in> set queue; \<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr qhead)) = Some tcb\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c qhead proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma valid_queues_valid_q:
  "valid_queues s \<Longrightarrow> (\<forall>tcb\<in>set (ksReadyQueues s (qdom, prio)). tcb_at' tcb s) \<and> distinct (ksReadyQueues s (qdom, prio))" apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def) apply (drule spec [where x = qdom]) apply (drule spec [where x = prio]) apply clarsimp apply (drule (1) bspec, erule obj_at'_weakenE) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Invariants_H.valid_queues s \<Longrightarrow> (\<forall>tcb\<in>set (ksReadyQueues s (qdom, prio)). tcb_at' tcb s) \<and> distinct (ksReadyQueues s (qdom, prio)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>tcb \<in> set (ksReadyQueues s (qdom, prio)); \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> tcb_at' tcb s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>tcb \<in> set (ksReadyQueues s (qdom, prio)); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; \<forall>p. (\<forall>t\<in>set (ksReadyQueues s (qdom, p)). obj_at' (inQ qdom p and runnable' \<circ> tcbState) t s) \<and> distinct (ksReadyQueues s (qdom, p)) \<and> (maxDomain < qdom \<longrightarrow> ksReadyQueues s (qdom, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (qdom, p) = [])\<rbrakk> \<Longrightarrow> tcb_at' tcb s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>tcb \<in> set (ksReadyQueues s (qdom, prio)); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; (\<forall>t\<in>set (ksReadyQueues s (qdom, prio)). obj_at' (inQ qdom prio and runnable' \<circ> tcbState) t s) \<and> distinct (ksReadyQueues s (qdom, prio)) \<and> (maxDomain < qdom \<longrightarrow> ksReadyQueues s (qdom, prio) = []) \<and> (maxPriority < prio \<longrightarrow> ksReadyQueues s (qdom, prio) = [])\<rbrakk> \<Longrightarrow> tcb_at' tcb s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>tcb \<in> set (ksReadyQueues s (qdom, prio)); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; \<forall>t\<in>set (ksReadyQueues s (qdom, prio)). obj_at' (inQ qdom prio and runnable' \<circ> tcbState) t s; distinct (ksReadyQueues s (qdom, prio)); maxDomain < qdom \<longrightarrow> ksReadyQueues s (qdom, prio) = []; maxPriority < prio \<longrightarrow> ksReadyQueues s (qdom, prio) = []\<rbrakk> \<Longrightarrow> tcb_at' tcb s proof (prove)
goal (1 subgoal):
 1. \<And>tcb k. \<lbrakk>tcb \<in> set (ksReadyQueues s (qdom, prio)); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; distinct (ksReadyQueues s (qdom, prio)); maxDomain < qdom \<longrightarrow> ksReadyQueues s (qdom, prio) = []; maxPriority < prio \<longrightarrow> ksReadyQueues s (qdom, prio) = []; (inQ qdom prio and runnable' \<circ> tcbState) k\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma prio_to_l1index_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s} Call prio_to_l1index_'proc
       \<lbrace>\<acute>ret__unsigned_long = prio_' s >> wordRadix \<rbrace>" by vcg (simp add: word_sle_def wordRadix_def')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call prio_to_l1index_'proc \<lbrace>\<acute>ret__unsigned_long = \<^bsup>s\<^esup>prio >> wordRadix\<rbrace>
theory IpcCancel_C

lemma invert_l1index_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s} Call invert_l1index_'proc
       \<lbrace>\<acute>ret__unsigned_long = of_nat l2BitmapSize - 1 - l1index_' s \<rbrace>" unfolding l2BitmapSize_def' by vcg
     (simp add: word_sle_def sdiv_int_def sdiv_word_def smod_word_def smod_int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call invert_l1index_'proc \<lbrace>\<acute>ret__unsigned_long = word_of_nat l2BitmapSize - 1 - \<^bsup>s\<^esup>l1index\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call invert_l1index_'proc \<lbrace>\<acute>ret__unsigned_long = word_of_nat 8 - 1 - \<^bsup>s\<^esup>l1index\<rbrace>
theory IpcCancel_C

lemma unat_ucast_prio_L1_cmask_simp:
  "unat (ucast (p::priority) && 0x1F :: machine_word) = unat (p && 0x1F)" using unat_ucast_prio_mask_simp[where m=5] by (simp add: mask_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (UCAST(8 \<rightarrow> 32) p && 0x1F) = unat (p && 0x1F) proof (prove)
using this:
unat (UCAST(8 \<rightarrow> 32) ?p && mask 5) = unat (?p && mask 5)

goal (1 subgoal):
 1. unat (UCAST(8 \<rightarrow> 32) p && 0x1F) = unat (p && 0x1F)
theory IpcCancel_C

lemma machine_word_and_1F_less_20:
  "(w :: machine_word) && 0x1F < 0x20" by (rule word_and_less', simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w && 0x1F < 0x20
theory IpcCancel_C

lemma prio_ucast_shiftr_wordRadix_helper: (* FIXME generalise *)
  "(ucast (p::priority) >> wordRadix :: machine_word) < 8" unfolding maxPriority_def numPriorities_def wordRadix_def using unat_lt2p[where x=p] apply (clarsimp simp add: word_less_nat_alt shiftr_div_2n' unat_ucast_upcast is_up word_le_nat_alt) apply arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 32) p >> wordRadix < 8 proof (prove)
goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 32) p >> State_H.wordSizeCase 5 6 < 8 proof (prove)
using this:
unat p < 2 ^ LENGTH(8)

goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 32) p >> State_H.wordSizeCase 5 6 < 8 proof (prove)
goal (1 subgoal):
 1. unat p < 256 \<Longrightarrow> unat p div 32 < 8 proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma prio_ucast_shiftr_wordRadix_helper': (* FIXME generalise *)
  "(ucast (p::priority) >> wordRadix :: machine_word) \<le> 7" unfolding maxPriority_def numPriorities_def wordRadix_def using unat_lt2p[where x=p] apply (clarsimp simp add: word_less_nat_alt shiftr_div_2n' unat_ucast_upcast is_up word_le_nat_alt) apply arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 32) p >> wordRadix \<le> 7 proof (prove)
goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 32) p >> State_H.wordSizeCase 5 6 \<le> 7 proof (prove)
using this:
unat p < 2 ^ LENGTH(8)

goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 32) p >> State_H.wordSizeCase 5 6 \<le> 7 proof (prove)
goal (1 subgoal):
 1. unat p < 256 \<Longrightarrow> unat p div 32 \<le> 7 proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma prio_unat_shiftr_wordRadix_helper': (* FIXME generalise *)
  "unat ((p::priority) >> wordRadix) \<le> 7" unfolding maxPriority_def numPriorities_def wordRadix_def using unat_lt2p[where x=p] apply (clarsimp simp add: word_less_nat_alt shiftr_div_2n' unat_ucast_upcast is_up word_le_nat_alt) apply arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (p >> wordRadix) \<le> 7 proof (prove)
goal (1 subgoal):
 1. unat (p >> State_H.wordSizeCase 5 6) \<le> 7 proof (prove)
using this:
unat p < 2 ^ LENGTH(8)

goal (1 subgoal):
 1. unat (p >> State_H.wordSizeCase 5 6) \<le> 7 proof (prove)
goal (1 subgoal):
 1. unat p < 256 \<Longrightarrow> unat p div 32 \<le> 7 proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma prio_ucast_shiftr_wordRadix_helper2:
  "(ucast (p::priority) >> wordRadix :: machine_word) < 0x20" by (rule order_less_trans[OF prio_ucast_shiftr_wordRadix_helper]; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 32) p >> wordRadix < 0x20
theory IpcCancel_C

lemma cready_queues_index_to_C_ucast_helper:
  fixes p :: priority
  fixes d :: domain
  shows "unat (ucast d * 0x100 + ucast p :: machine_word) = unat d * 256 + unat p" unfolding tcb_queue_relation'_def maxPriority_def numPriorities_def using unat_lt2p[where x=p] unat_lt2p[where x=d] by (clarsimp simp: cready_queues_index_to_C_def word_le_nat_alt unat_word_ariths)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (UCAST(8 \<rightarrow> 32) d * 0x100 + UCAST(8 \<rightarrow> 32) p) = unat d * 256 + unat p proof (prove)
goal (1 subgoal):
 1. unat (UCAST(8 \<rightarrow> 32) d * 0x100 + UCAST(8 \<rightarrow> 32) p) = unat d * 256 + unat p proof (prove)
using this:
unat p < 2 ^ LENGTH(8)
unat d < 2 ^ LENGTH(8)

goal (1 subgoal):
 1. unat (UCAST(8 \<rightarrow> 32) d * 0x100 + UCAST(8 \<rightarrow> 32) p) = unat d * 256 + unat p
theory IpcCancel_C

lemma rf_sr_cbitmap_L1_relation[intro]:
  "(\<sigma>, x) \<in> rf_sr \<Longrightarrow> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>)" by (clarsimp simp: rf_sr_def cstate_relation_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, x) \<in> rf_sr \<Longrightarrow> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>)
theory IpcCancel_C

lemma rf_sr_cbitmap_L2_relation[intro]:
  "(\<sigma>, x) \<in> rf_sr \<Longrightarrow> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>)" by (clarsimp simp: rf_sr_def cstate_relation_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, x) \<in> rf_sr \<Longrightarrow> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>)
theory IpcCancel_C

lemma cbitmap_L1_relation_bit_set:
  fixes p :: priority
  shows
  "\<lbrakk> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>) ;
     d \<le> maxDomain \<rbrakk> \<Longrightarrow>
   cbitmap_L1_relation
           (Arrays.update (ksReadyQueuesL1Bitmap_' (globals x)) (unat d)
             (ksReadyQueuesL1Bitmap_' (globals x).[unat d] || 2 ^ unat (p >> wordRadix)))
           ((ksReadyQueuesL1Bitmap \<sigma>)(d := ksReadyQueuesL1Bitmap \<sigma> d || 2 ^ prioToL1Index p))" apply (unfold cbitmap_L1_relation_def) apply (clarsimp simp: le_maxDomain_eq_less_numDomains word_le_nat_alt prioToL1Index_def
                        num_domains_index_updates) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); d \<le> maxDomain\<rbrakk> \<Longrightarrow> cbitmap_L1_relation (Arrays.update (ksReadyQueuesL1Bitmap_' (globals x)) (unat d) (ksReadyQueuesL1Bitmap_' (globals x).[unat d] || 2 ^ unat (p >> wordRadix))) ((ksReadyQueuesL1Bitmap \<sigma>)(d := ksReadyQueuesL1Bitmap \<sigma> d || 2 ^ prioToL1Index p)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>d. (d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap_' (globals x).[unat d] = ksReadyQueuesL1Bitmap \<sigma> d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap \<sigma> d = 0); d \<le> maxDomain\<rbrakk> \<Longrightarrow> \<forall>da. (da \<le> maxDomain \<longrightarrow> Arrays.update (ksReadyQueuesL1Bitmap_' (globals x)) (unat d) (ksReadyQueuesL1Bitmap_' (globals x).[unat d] || 2 ^ unat (p >> wordRadix)).[unat da] = ((ksReadyQueuesL1Bitmap \<sigma>)(d := ksReadyQueuesL1Bitmap \<sigma> d || 2 ^ prioToL1Index p)) da) \<and> (\<not> da \<le> maxDomain \<longrightarrow> ((ksReadyQueuesL1Bitmap \<sigma>)(d := ksReadyQueuesL1Bitmap \<sigma> d || 2 ^ prioToL1Index p)) da = 0) proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma t_hrs_ksReadyQueues_upd_absorb:
  "t_hrs_'_update f (g s) \<lparr>ksReadyQueues_' := rqupd \<rparr> =
   t_hrs_'_update f (g s \<lparr>ksReadyQueues_' := rqupd\<rparr>)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t_hrs_'_update f (g s)\<lparr>ksReadyQueues_' := rqupd\<rparr> = t_hrs_'_update f (g s\<lparr>ksReadyQueues_' := rqupd\<rparr>)
theory IpcCancel_C

lemma tcb_queue_relation'_empty_ksReadyQueues:
  "\<lbrakk> sched_queue_relation' (cslift x) (q s) NULL NULL ; \<forall>t\<in> set (q s). tcb_at' t s  \<rbrakk> \<Longrightarrow> q s = []" apply (clarsimp simp add: tcb_queue_relation'_def) apply (subst (asm) eq_commute) apply (cases "q s" rule: rev_cases, simp) apply (clarsimp simp: tcb_at_not_NULL) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sched_queue_relation' (cslift x) (q s) NULL NULL; \<forall>t\<in>set (q s). tcb_at' t s\<rbrakk> \<Longrightarrow> q s = [] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t\<in>set (q s). tcb_at' t s; NULL = (if q s = [] then NULL else tcb_ptr_to_ctcb_ptr (last (q s))); sched_queue_relation (cslift x) (q s) NULL NULL\<rbrakk> \<Longrightarrow> q s = [] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t\<in>set (q s). tcb_at' t s; (if q s = [] then NULL else tcb_ptr_to_ctcb_ptr (last (q s))) = NULL; sched_queue_relation (cslift x) (q s) NULL NULL\<rbrakk> \<Longrightarrow> q s = [] proof (prove)
goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>\<forall>t\<in>set (q s). tcb_at' t s; (if q s = [] then NULL else tcb_ptr_to_ctcb_ptr (last (q s))) = NULL; sched_queue_relation (cslift x) (q s) NULL NULL; q s = ys @ [y]\<rbrakk> \<Longrightarrow> q s = [] proof (prove)
goal:
No subgoals!