kings-crown/FVELER_Isabelle huggingface dataset:
theory IpcCancel_C

lemma invert_prioToL1Index_c_simp:
  "p \<le> maxPriority
   \<Longrightarrow>
   unat ((of_nat l2BitmapSize :: machine_word) - 1 - (ucast p >> wordRadix))
   = invertL1Index (prioToL1Index p)" unfolding maxPriority_def l2BitmapSize_def' invertL1Index_def prioToL1Index_def
     numPriorities_def by (simp add: unat_sub prio_and_dom_limit_helpers)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<le> maxPriority \<Longrightarrow> unat (word_of_nat l2BitmapSize - 1 - (UCAST(8 \<rightarrow> 32) p >> wordRadix)) = invertL1Index (prioToL1Index p) proof (prove)
goal (1 subgoal):
 1. p \<le> fromIntegral (256 - 1) \<Longrightarrow> unat (word_of_nat 8 - 1 - (UCAST(8 \<rightarrow> 32) p >> wordRadix)) = 8 - 1 - (fromIntegral $ p `~shiftR~` wordRadix)
theory IpcCancel_C

lemma c_invert_assist: "7 - (ucast (p :: priority) >> 5 :: machine_word) < 8" using prio_ucast_shiftr_wordRadix_helper'[simplified wordRadix_def] by - (rule word_less_imp_diff_less, simp_all)

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

goal (1 subgoal):
 1. 7 - (UCAST(8 \<rightarrow> 32) p >> 5) < 8
theory IpcCancel_C

lemma cbitmap_L1_relation_bit_clear:
  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))" unfolding cbitmap_L1_relation_def numPriorities_def wordBits_def word_size l2BitmapSize_def' by (clarsimp simp: word_size prioToL1Index_def wordRadix_def mask_def
                     invertL1Index_def l2BitmapSize_def'
                     le_maxDomain_eq_less_numDomains word_le_nat_alt num_domains_index_updates)

(* 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)
theory IpcCancel_C

lemma cbitmap_L2_relationD:
  "\<lbrakk> cbitmap_L2_relation cbitmap2 abitmap2 ; d \<le> maxDomain ; i < l2BitmapSize \<rbrakk> \<Longrightarrow>
    cbitmap2.[unat d].[i] = abitmap2 (d, i)" unfolding cbitmap_L2_relation_def l2BitmapSize_def' by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cbitmap_L2_relation cbitmap2 abitmap2; d \<le> maxDomain; i < l2BitmapSize\<rbrakk> \<Longrightarrow> cbitmap2.[unat d].[i] = abitmap2 (d, i) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>d i. (d \<le> maxDomain \<and> i < 8 \<longrightarrow> cbitmap2.[unat d].[i] = abitmap2 (d, i)) \<and> (\<not> (d \<le> maxDomain \<and> i < 8) \<longrightarrow> abitmap2 (d, i) = 0); d \<le> maxDomain; i < 8\<rbrakk> \<Longrightarrow> cbitmap2.[unat d].[i] = abitmap2 (d, i)
theory IpcCancel_C

lemma tcb_queue_relation_qend_mems:
  "\<lbrakk> tcb_queue_relation' getNext getPrev mp queue qhead qend;
     \<forall>x \<in> set queue. tcb_at' x s \<rbrakk>
      \<Longrightarrow> (qend = NULL \<longrightarrow> queue = [])
       \<and> (qend \<noteq> NULL \<longrightarrow> ctcb_ptr_to_tcb_ptr qend \<in> set queue)" apply (clarsimp simp: tcb_queue_relation'_def) apply (drule bspec, erule last_in_set) apply (simp add: tcb_at_not_NULL) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation' getNext getPrev mp queue qhead qend; \<forall>x\<in>set queue. tcb_at' x s\<rbrakk> \<Longrightarrow> (qend = NULL \<longrightarrow> queue = []) \<and> (qend \<noteq> NULL \<longrightarrow> ctcb_ptr_to_tcb_ptr qend \<in> set queue) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set queue. tcb_at' x s; qend = NULL; tcb_queue_relation getNext getPrev mp queue NULL qhead; queue \<noteq> []; tcb_ptr_to_ctcb_ptr (last queue) = NULL\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>qend = NULL; tcb_queue_relation getNext getPrev mp queue NULL qhead; queue \<noteq> []; tcb_ptr_to_ctcb_ptr (last queue) = NULL; tcb_at' (last queue) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma isRunnable_spec:
  "\<forall>s. \<Gamma> \<turnstile> ({s} \<inter> {s. cslift s (thread_' s) \<noteq> None}) Call isRunnable_'proc
       {s'. ret__unsigned_long_' s' = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s (thread_' s))))) \<in>
                            { scast ThreadState_Running, scast ThreadState_Restart })}" apply vcg apply (clarsimp simp: typ_heap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. cslift s (thread_' s) \<noteq> None}) Call isRunnable_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s \<^bsup>s\<^esup>thread)))) \<in> {SCAST(32 signed \<rightarrow> 32) ThreadState_Running, SCAST(32 signed \<rightarrow> 32) ThreadState_Restart})\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t_hrs thread. clift t_hrs thread \<noteq> None \<Longrightarrow> hrs_htd t_hrs \<Turnstile>\<^sub>t thread \<and> (\<forall>ret__unsigned. ret__unsigned = tsType_CL (thread_state_lift (h_val (hrs_mem t_hrs) (PTR(thread_state_C) &(thread\<rightarrow>[''tcbState_C''])))) \<longrightarrow> (tsType_CL (thread_state_lift (h_val (hrs_mem t_hrs) (PTR(thread_state_C) &(thread\<rightarrow>[''tcbState_C''])))) \<in> insert (SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (Collect ((=) (SCAST(32 signed \<rightarrow> 32) ThreadState_Running))) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (clift t_hrs thread)))) \<in> insert (SCAST(32 signed \<rightarrow> 32) ThreadState_Running) (Collect ((=) (SCAST(32 signed \<rightarrow> 32) ThreadState_Restart))))) \<and> (tsType_CL (thread_state_lift (h_val (hrs_mem t_hrs) (PTR(thread_state_C) &(thread\<rightarrow>[''tcbState_C''])))) \<notin> insert (SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (Collect ((=) (SCAST(32 signed \<rightarrow> 32) ThreadState_Running))) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) false = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (clift t_hrs thread)))) \<in> insert (SCAST(32 signed \<rightarrow> 32) ThreadState_Running) (Collect ((=) (SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)))))) proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma ccorres_setSchedulerAction:
  "cscheduler_action_relation a p \<Longrightarrow>
  ccorres dc xfdc \<top> UNIV hs
      (setSchedulerAction a)
      (Basic (\<lambda>s. globals_update (ksSchedulerAction_'_update (\<lambda>_. p)) s))" apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: setSchedulerAction_def modify_def get_def put_def bind_def) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def cmachine_state_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cscheduler_action_relation a p \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) UNIV hs (setSchedulerAction a) (\<acute>ksSchedulerAction :== p) proof (prove)
goal (1 subgoal):
 1. cscheduler_action_relation a p \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ksSchedulerAction :== p {s. \<exists>(rv, \<sigma>')\<in>fst (setSchedulerAction a \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. cscheduler_action_relation a p \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setSchedulerAction a \<sigma>). (\<sigma>', globals_update (ksSchedulerAction_'_update (\<lambda>_. p)) s) \<in> rf_sr \<and> dc rv (xfdc (globals_update (ksSchedulerAction_'_update (\<lambda>_. p)) s))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>cscheduler_action_relation a p; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksSchedulerAction := a\<rparr>, globals_update (ksSchedulerAction_'_update (\<lambda>_. p)) x) \<in> rf_sr proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma scheduler_action_case_switch_to_if:
  "(case act of SwitchToThread t \<Rightarrow> f t | _ \<Rightarrow> g)
      = (if \<exists>t. act = SwitchToThread t
            then f (case act of SwitchToThread t \<Rightarrow> t) else g)" by (simp split: scheduler_action.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case act of SwitchToThread t \<Rightarrow> f t | _ \<Rightarrow> g) = (if \<exists>t. act = SwitchToThread t then f (case act of SwitchToThread t \<Rightarrow> t) else g)
theory IpcCancel_C

lemma tcb_at_1:
  "tcb_at' t s \<Longrightarrow> tcb_ptr_to_ctcb_ptr t \<noteq> tcb_Ptr 1" apply (drule is_aligned_tcb_ptr_to_ctcb_ptr) apply (clarsimp simp add: is_aligned_def ctcb_size_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at' t s \<Longrightarrow> tcb_ptr_to_ctcb_ptr t \<noteq> tcb_Ptr 1 proof (prove)
goal (1 subgoal):
 1. is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr t)) ctcb_size_bits \<Longrightarrow> tcb_ptr_to_ctcb_ptr t \<noteq> tcb_Ptr 1 proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma getReadyQueuesL1Bitmap_sp:
  "\<lbrace>\<lambda>s. P s \<and> d \<le> maxDomain \<rbrace>
   getReadyQueuesL1Bitmap d
   \<lbrace>\<lambda>rv s. ksReadyQueuesL1Bitmap s d = rv \<and> d \<le> maxDomain \<and> P s\<rbrace>" unfolding bitmap_fun_defs by wp simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> d \<le> maxDomain\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>rv s. ksReadyQueuesL1Bitmap s d = rv \<and> d \<le> maxDomain \<and> P s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> d \<le> maxDomain\<rbrace> gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d) \<lbrace>\<lambda>rv s. ksReadyQueuesL1Bitmap s d = rv \<and> d \<le> maxDomain \<and> P s\<rbrace>
theory IpcCancel_C

lemma getReadyQueuesL2Bitmap_sp:
  "\<lbrace>\<lambda>s. P s \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<rbrace>
   getReadyQueuesL2Bitmap d i
   \<lbrace>\<lambda>rv s. ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> P s\<rbrace>" unfolding bitmap_fun_defs by wp simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> d \<le> maxDomain \<and> i < l2BitmapSize\<rbrace> getReadyQueuesL2Bitmap d i \<lbrace>\<lambda>rv s. ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> P s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> d \<le> maxDomain \<and> i < l2BitmapSize\<rbrace> gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, i)) \<lbrace>\<lambda>rv s. ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> P s\<rbrace>
theory IpcCancel_C

lemma rf_sr_ksReadyQueuesL1Bitmap_simp:
  "\<lbrakk> (\<sigma>, s') \<in> rf_sr ; d \<le> maxDomain \<rbrakk>
  \<Longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap \<sigma> d" apply (drule rf_sr_cbitmap_L1_relation) apply (simp add: cbitmap_L1_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s') \<in> rf_sr; d \<le> maxDomain\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap \<sigma> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d \<le> maxDomain; cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap \<sigma>)\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap \<sigma> d proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma lookupBitmapPriority_le_maxPriority:
  "\<lbrakk> ksReadyQueuesL1Bitmap s d \<noteq> 0 ; valid_queues s \<rbrakk>
   \<Longrightarrow> lookupBitmapPriority d s \<le> maxPriority" unfolding valid_queues_def valid_queues_no_bitmap_def by (fastforce dest!: bitmapQ_from_bitmap_lookup bitmapQ_ksReadyQueuesI intro: ccontr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksReadyQueuesL1Bitmap s d \<noteq> 0; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> lookupBitmapPriority d s \<le> maxPriority proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksReadyQueuesL1Bitmap s d \<noteq> 0; (\<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 \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])) \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> lookupBitmapPriority d s \<le> maxPriority
theory IpcCancel_C

lemma ksReadyQueuesL1Bitmap_word_log2_max:
    "\<lbrakk>valid_queues s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk>
    \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize" unfolding valid_queues_def by (fastforce dest: word_log2_nth_same bitmapQ_no_L1_orphansD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Invariants_H.valid_queues s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize
theory IpcCancel_C

lemma clzl_spec:
  "\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x___unsigned_long_' s \<noteq> 0} Call clzl_'proc
       \<lbrace>\<acute>ret__long = of_nat (word_clz (x___unsigned_long_' s))\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (rule_tac x="ret__long_'_update f x" for f in exI) apply (simp add: mex_def meq_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. \<^bsup>s\<^esup>x___unsigned_long \<noteq> 0\<rbrace> Call clzl_'proc \<lbrace>\<acute>ret__long = word_of_nat (word_clz \<^bsup>s\<^esup>x___unsigned_long)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. \<^bsup>s\<^esup>x___unsigned_long \<noteq> 0\<rbrace> \<subseteq> {sa. (\<forall>t. (case (sa, t) of (s', t) \<Rightarrow> (\<forall>s. s = s' \<and> x___unsigned_long_' s \<noteq> 0 \<longrightarrow> ret__long_' t = word_of_nat (word_clz (x___unsigned_long_' s))) \<and> (\<exists>s. s = s' \<and> x___unsigned_long_' s \<noteq> 0)) \<and> (case (sa, t) of (s, t) \<Rightarrow> t may_not_modify_globals s) \<longrightarrow> ret__long_' t = word_of_nat (word_clz (x___unsigned_long_' s))) \<and> (\<not> False \<longrightarrow> (\<exists>t. (case (sa, t) of (s', t) \<Rightarrow> (\<forall>s. s = s' \<and> x___unsigned_long_' s \<noteq> 0 \<longrightarrow> ret__long_' t = word_of_nat (word_clz (x___unsigned_long_' s))) \<and> (\<exists>s. s = s' \<and> x___unsigned_long_' s \<noteq> 0)) \<and> (case (sa, t) of (s, t) \<Rightarrow> t may_not_modify_globals s)))} proof (prove)
goal (1 subgoal):
 1. \<And>x. x___unsigned_long_' x \<noteq> 0 \<Longrightarrow> \<exists>t. ret__long_' t = word_of_nat (word_clz (x___unsigned_long_' x)) \<and> t may_not_modify_globals x proof (prove)
goal (1 subgoal):
 1. \<And>x. x___unsigned_long_' x \<noteq> 0 \<Longrightarrow> ret__long_' (ret__long_'_update (?f19 x) x) = word_of_nat (word_clz (x___unsigned_long_' x)) \<and> ret__long_'_update (?f19 x) x may_not_modify_globals x proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma l1index_to_prio_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s} Call l1index_to_prio_'proc
       \<lbrace>\<acute>ret__unsigned_long = l1index_' 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 l1index_to_prio_'proc \<lbrace>\<acute>ret__unsigned_long = \<^bsup>s\<^esup>l1index << wordRadix\<rbrace>
theory IpcCancel_C

lemma ctcb_relation_unat_tcbPriority_C:
  "ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbPriority_C tcb') = unat (tcbPriority tcb)" apply (clarsimp simp: ctcb_relation_def) apply (rule trans, rule arg_cong[where f=unat], erule sym) apply (simp(no_asm)) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbPriority_C tcb') = unat (tcbPriority tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcbFaultHandler tcb = tcbFaultHandler_C tcb'; cthread_state_relation (tcbState tcb) (tcbState_C tcb', tcbFault_C tcb'); tcbIPCBuffer tcb = tcbIPCBuffer_C tcb'; carch_tcb_relation (tcbArch tcb) (tcbArch_C tcb'); tcbQueued tcb = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C tcb'))); UCAST(8 \<rightarrow> 32) (tcbDomain tcb) = tcbDomain_C tcb'; UCAST(8 \<rightarrow> 32) (tcbPriority tcb) = tcbPriority_C tcb'; UCAST(8 \<rightarrow> 32) (tcbMCP tcb) = tcbMCP_C tcb'; tcbTimeSlice tcb = unat (tcbTimeSlice_C tcb'); cfault_rel (tcbFault tcb) (seL4_Fault_lift (tcbFault_C tcb')) (lookup_fault_lift (tcbLookupFailure_C tcb')); option_to_ptr (tcbBoundNotification tcb) = tcbBoundNotification_C tcb'\<rbrakk> \<Longrightarrow> unat (tcbPriority_C tcb') = unat (tcbPriority tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcbFaultHandler tcb = tcbFaultHandler_C tcb'; cthread_state_relation (tcbState tcb) (tcbState_C tcb', tcbFault_C tcb'); tcbIPCBuffer tcb = tcbIPCBuffer_C tcb'; carch_tcb_relation (tcbArch tcb) (tcbArch_C tcb'); tcbQueued tcb = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C tcb'))); UCAST(8 \<rightarrow> 32) (tcbDomain tcb) = tcbDomain_C tcb'; UCAST(8 \<rightarrow> 32) (tcbPriority tcb) = tcbPriority_C tcb'; UCAST(8 \<rightarrow> 32) (tcbMCP tcb) = tcbMCP_C tcb'; tcbTimeSlice tcb = unat (tcbTimeSlice_C tcb'); cfault_rel (tcbFault tcb) (seL4_Fault_lift (tcbFault_C tcb')) (lookup_fault_lift (tcbLookupFailure_C tcb')); option_to_ptr (tcbBoundNotification tcb) = tcbBoundNotification_C tcb'\<rbrakk> \<Longrightarrow> unat (UCAST(8 \<rightarrow> 32) (tcbPriority tcb)) = unat (tcbPriority tcb) proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma ctcb_relation_unat_tcbDomain_C:
  "ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbDomain_C tcb') = unat (tcbDomain tcb)" apply (clarsimp simp: ctcb_relation_def) apply (rule trans, rule arg_cong[where f=unat], erule sym) apply (simp(no_asm)) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbDomain_C tcb') = unat (tcbDomain tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcbFaultHandler tcb = tcbFaultHandler_C tcb'; cthread_state_relation (tcbState tcb) (tcbState_C tcb', tcbFault_C tcb'); tcbIPCBuffer tcb = tcbIPCBuffer_C tcb'; carch_tcb_relation (tcbArch tcb) (tcbArch_C tcb'); tcbQueued tcb = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C tcb'))); UCAST(8 \<rightarrow> 32) (tcbDomain tcb) = tcbDomain_C tcb'; UCAST(8 \<rightarrow> 32) (tcbPriority tcb) = tcbPriority_C tcb'; UCAST(8 \<rightarrow> 32) (tcbMCP tcb) = tcbMCP_C tcb'; tcbTimeSlice tcb = unat (tcbTimeSlice_C tcb'); cfault_rel (tcbFault tcb) (seL4_Fault_lift (tcbFault_C tcb')) (lookup_fault_lift (tcbLookupFailure_C tcb')); option_to_ptr (tcbBoundNotification tcb) = tcbBoundNotification_C tcb'\<rbrakk> \<Longrightarrow> unat (tcbDomain_C tcb') = unat (tcbDomain tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcbFaultHandler tcb = tcbFaultHandler_C tcb'; cthread_state_relation (tcbState tcb) (tcbState_C tcb', tcbFault_C tcb'); tcbIPCBuffer tcb = tcbIPCBuffer_C tcb'; carch_tcb_relation (tcbArch tcb) (tcbArch_C tcb'); tcbQueued tcb = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C tcb'))); UCAST(8 \<rightarrow> 32) (tcbDomain tcb) = tcbDomain_C tcb'; UCAST(8 \<rightarrow> 32) (tcbPriority tcb) = tcbPriority_C tcb'; UCAST(8 \<rightarrow> 32) (tcbMCP tcb) = tcbMCP_C tcb'; tcbTimeSlice tcb = unat (tcbTimeSlice_C tcb'); cfault_rel (tcbFault tcb) (seL4_Fault_lift (tcbFault_C tcb')) (lookup_fault_lift (tcbLookupFailure_C tcb')); option_to_ptr (tcbBoundNotification tcb) = tcbBoundNotification_C tcb'\<rbrakk> \<Longrightarrow> unat (UCAST(8 \<rightarrow> 32) (tcbDomain tcb)) = unat (tcbDomain tcb) proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma getCurDomain_ccorres_dom_':
  "ccorres (\<lambda>rv rv'. rv' = ucast rv) dom_'
       \<top> UNIV hs curDomain (\<acute>dom :== \<acute>ksCurDomain)" apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: curDomain_def simpler_gets_def
                        rf_sr_ksCurDomain) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>_. True) UNIV hs curDomain (\<acute>dom :== \<acute>ksCurDomain) proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>dom :== \<acute>ksCurDomain {s. \<exists>(rv, \<sigma>')\<in>fst (curDomain \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dom_' s = UCAST(8 \<rightarrow> 32) rv} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (curDomain \<sigma>). (\<sigma>', dom_'_update (\<lambda>_. ksCurDomain_' (globals s)) s) \<in> rf_sr \<and> ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv} proof (prove)
goal:
No subgoals!