kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_R

lemma prioToL1Index_l1IndexToPrio_or_id:
  "\<lbrakk> unat (w'::priority) < 2 ^ wordRadix ; w < size w' \<rbrakk>
   \<Longrightarrow> prioToL1Index ((l1IndexToPrio w) || w') = w" unfolding l1IndexToPrio_def prioToL1Index_def apply (simp add: shiftr_over_or_dist shiftr_le_0 wordRadix_def') apply (subst shiftl_shiftr_id, simp, simp add: word_size) apply (rule word_of_nat_less) apply simp apply (subst unat_of_nat_eq, simp_all add: word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat w' < 2 ^ wordRadix; w < size w'\<rbrakk> \<Longrightarrow> prioToL1Index (l1IndexToPrio w || w') = w proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat w' < 2 ^ wordRadix; w < size w'\<rbrakk> \<Longrightarrow> (fromIntegral $ (fromIntegral w `~shiftL~` wordRadix || w') `~shiftR~` wordRadix) = w proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat w' < 32; w < size w'\<rbrakk> \<Longrightarrow> unat (word_of_nat w << 5 >> 5) = w proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat w' < 32; w < 8\<rbrakk> \<Longrightarrow> word_of_nat w < 8
 2. \<lbrakk>unat w' < 32; w < size w'\<rbrakk> \<Longrightarrow> unat (word_of_nat w) = w proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat w' < 32; w < 8\<rbrakk> \<Longrightarrow> w < unat 8
 2. \<lbrakk>unat w' < 32; w < size w'\<rbrakk> \<Longrightarrow> unat (word_of_nat w) = w proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat w' < 32; w < size w'\<rbrakk> \<Longrightarrow> unat (word_of_nat w) = w proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma bitmapQ_no_L1_orphansD:
  "\<lbrakk> bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d !! i \<rbrakk>
  \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize" unfolding bitmapQ_no_L1_orphans_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d !! i\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize; ksReadyQueuesL1Bitmap s d !! i\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize
theory TcbAcc_R

lemma l1IndexToPrio_wordRadix_mask[simp]:
  "l1IndexToPrio i && mask wordRadix = 0" unfolding l1IndexToPrio_def by (simp add: wordRadix_def')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. l1IndexToPrio i && mask wordRadix = 0 proof (prove)
goal (1 subgoal):
 1. fromIntegral i `~shiftL~` wordRadix && mask wordRadix = 0
theory TcbAcc_R

lemma valid_queues_no_bitmap_exceptI[intro]:
  "valid_queues_no_bitmap s \<Longrightarrow> valid_queues_no_bitmap_except t s" unfolding valid_queues_no_bitmap_except_def valid_queues_no_bitmap_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_queues_no_bitmap s \<Longrightarrow> valid_queues_no_bitmap_except t s proof (prove)
goal (1 subgoal):
 1. \<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) = []) \<Longrightarrow> \<forall>d p. (\<forall>ta\<in>set (ksReadyQueues s (d, p)). ta \<noteq> t \<longrightarrow> obj_at' (inQ d p and runnable' \<circ> tcbState) ta s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])
theory TcbAcc_R

lemma valid_objs_valid_tcbE: "\<And>s t.\<lbrakk> valid_objs' s; tcb_at' t s; \<And>tcb. valid_tcb' tcb s \<Longrightarrow> R s tcb \<rbrakk> \<Longrightarrow> obj_at' (R s) t s" apply (clarsimp simp add: projectKOs valid_objs'_def ran_def typ_at'_def
                            ko_wp_at'_def valid_obj'_def valid_tcb'_def obj_at'_def) apply (fastforce simp: projectKO_def projectKO_opt_tcb return_def valid_tcb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>valid_objs' s; tcb_at' t s; \<And>tcb. valid_tcb' tcb s \<Longrightarrow> R s tcb\<rbrakk> \<Longrightarrow> obj_at' (R s) t s proof (prove)
goal (1 subgoal):
 1. \<And>s t obj. \<lbrakk>\<forall>x. (\<exists>a. ksPSpace s a = Some x) \<longrightarrow> (case x of KOEndpoint endpoint \<Rightarrow> valid_ep' endpoint s | KONotification notification \<Rightarrow> valid_ntfn' notification s | KOKernelData \<Rightarrow> False | KOTCB tcb \<Rightarrow> valid_tcb' tcb s | KOCTE cte \<Rightarrow> valid_cte' cte s | KOArch arch_kernel_object \<Rightarrow> valid_arch_obj' arch_kernel_object s | _ \<Rightarrow> True); \<And>tcb. (\<forall>a. (\<exists>b aa. tcb_cte_cases aa = Some (a, b)) \<longrightarrow> valid_cap' (cteCap (a tcb)) s) \<and> valid_tcb_state' (tcbState tcb) s \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> valid_bound_ntfn' (tcbBoundNotification tcb) s \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority \<Longrightarrow> R s tcb; ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> R s obj proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma valid_objs'_maxDomain:
  "\<And>s t. \<lbrakk> valid_objs' s; tcb_at' t s \<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t s" apply (erule (1) valid_objs_valid_tcbE) apply (clarsimp simp: valid_tcb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>valid_objs' s; tcb_at' t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t s proof (prove)
goal (1 subgoal):
 1. \<And>s t tcb. \<lbrakk>tcb_at' t s; valid_tcb' tcb s\<rbrakk> \<Longrightarrow> tcbDomain tcb \<le> maxDomain proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma valid_objs'_maxPriority:
  "\<And>s t. \<lbrakk> valid_objs' s; tcb_at' t s \<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t s" apply (erule (1) valid_objs_valid_tcbE) apply (clarsimp simp: valid_tcb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>valid_objs' s; tcb_at' t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t s proof (prove)
goal (1 subgoal):
 1. \<And>s t tcb. \<lbrakk>tcb_at' t s; valid_tcb' tcb s\<rbrakk> \<Longrightarrow> tcbPriority tcb \<le> maxPriority proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma doMachineOp_irq_states':
  assumes masks: "\<And>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> f \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace>"
  shows "\<lbrace>valid_irq_states'\<rbrace> doMachineOp f \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace>" apply (simp add: doMachineOp_def split_def) apply wp apply clarsimp apply (drule use_valid) apply (rule_tac P="\<lambda>m. m = irq_masks (ksMachineState s)" in masks) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> doMachineOp f \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> do ms <- gets ksMachineState;
p <- select_f (f ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_states' s \<Longrightarrow> \<forall>x\<in>fst (f (ksMachineState s)). valid_irq_states' (s\<lparr>ksMachineState := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>valid_irq_states' s; (a, b) \<in> fst (f (ksMachineState s))\<rbrakk> \<Longrightarrow> valid_irq_masks' (intStateIRQTable (ksInterruptState s)) (irq_masks b) proof (prove)
goal (3 subgoals):
 1. \<And>s a b. valid_irq_states' s \<Longrightarrow> \<lbrace>?P9 s a b\<rbrace> f \<lbrace>?Q9 s a b\<rbrace>
 2. \<And>s a b. valid_irq_states' s \<Longrightarrow> ?P9 s a b (ksMachineState s)
 3. \<And>s a b. \<lbrakk>valid_irq_states' s; ?Q9 s a b a b\<rbrakk> \<Longrightarrow> valid_irq_masks' (intStateIRQTable (ksInterruptState s)) (irq_masks b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. valid_irq_states' s \<Longrightarrow> irq_masks (ksMachineState s) = irq_masks (ksMachineState s)
 2. \<And>s a b. \<lbrakk>valid_irq_states' s; irq_masks b = irq_masks (ksMachineState s)\<rbrakk> \<Longrightarrow> valid_irq_masks' (intStateIRQTable (ksInterruptState s)) (irq_masks b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>valid_irq_states' s; irq_masks b = irq_masks (ksMachineState s)\<rbrakk> \<Longrightarrow> valid_irq_masks' (intStateIRQTable (ksInterruptState s)) (irq_masks b) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma dmo_lift':
  assumes f: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
  shows "\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> doMachineOp f
         \<lbrace>\<lambda>rv s. Q rv (ksMachineState s)\<rbrace>" apply (simp add: doMachineOp_def split_def) apply wp apply clarsimp apply (erule (1) use_valid [OF _ f]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> doMachineOp f \<lbrace>\<lambda>rv s. Q rv (ksMachineState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ms <- gets ksMachineState;
p <- select_f (f ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>rv s. Q rv (ksMachineState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ksMachineState s) \<Longrightarrow> \<forall>x\<in>fst (f (ksMachineState s)). Q (fst x) (ksMachineState (s\<lparr>ksMachineState := snd x\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P (ksMachineState s); (a, b) \<in> fst (f (ksMachineState s))\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma doMachineOp_getActiveIRQ_IRQ_active:
  "\<lbrace>valid_irq_states'\<rbrace>
     doMachineOp (getActiveIRQ in_kernel)
   \<lbrace>\<lambda>rv s. \<forall>irq. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> IRQInactive\<rbrace>" apply (rule hoare_lift_Pf3 [where f="ksInterruptState"]) prefer 2 apply wp apply (simp add: irq_state_independent_H_def) apply assumption apply (rule dmo_lift') apply (rule getActiveIRQ_masked) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv s. \<forall>irq. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. valid_irq_masks' (intStateIRQTable x) (irq_masks (ksMachineState s))\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>a b. \<forall>irq. a = Some irq \<longrightarrow> intStateIRQTable x irq \<noteq> irqstate.IRQInactive\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>_ s. P (ksInterruptState s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>_ s. P (ksInterruptState s)\<rbrace>
 2. \<And>x. \<lbrace>\<lambda>s. valid_irq_masks' (intStateIRQTable x) (irq_masks (ksMachineState s))\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>a b. \<forall>irq. a = Some irq \<longrightarrow> intStateIRQTable x irq \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P. irq_state_independent_H (\<lambda>s. P (ksInterruptState s))
 2. \<And>P s. P (ksInterruptState s) \<Longrightarrow> P (ksInterruptState s)
 3. \<And>x. \<lbrace>\<lambda>s. valid_irq_masks' (intStateIRQTable x) (irq_masks (ksMachineState s))\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>a b. \<forall>irq. a = Some irq \<longrightarrow> intStateIRQTable x irq \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P s. P (ksInterruptState s) \<Longrightarrow> P (ksInterruptState s)
 2. \<And>x. \<lbrace>\<lambda>s. valid_irq_masks' (intStateIRQTable x) (irq_masks (ksMachineState s))\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>a b. \<forall>irq. a = Some irq \<longrightarrow> intStateIRQTable x irq \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. valid_irq_masks' (intStateIRQTable x) (irq_masks (ksMachineState s))\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>a b. \<forall>irq. a = Some irq \<longrightarrow> intStateIRQTable x irq \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>a. valid_irq_masks' (intStateIRQTable x) (irq_masks a)\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>a b. \<forall>irq. a = Some irq \<longrightarrow> intStateIRQTable x irq \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma doMachineOp_getActiveIRQ_IRQ_active':
  "\<lbrace>valid_irq_states'\<rbrace>
     doMachineOp (getActiveIRQ in_kernel)
   \<lbrace>\<lambda>rv s. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> IRQInactive\<rbrace>" apply (rule hoare_post_imp) prefer 2 apply (rule doMachineOp_getActiveIRQ_IRQ_active) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv s. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. ?Q rv s \<Longrightarrow> rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive
 2. \<lbrace>valid_irq_states'\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>valid_irq_states'\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<forall>irq. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive \<Longrightarrow> rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma updateObject_tcb_inv:
  "\<lbrace>P\<rbrace> updateObject (obj::tcb) ko p q n \<lbrace>\<lambda>rv. P\<rbrace>" by simp (rule updateObject_default_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> updateObject obj ko p q n \<lbrace>\<lambda>rv. P\<rbrace>
theory TcbAcc_R

lemma getObject_TCB_corres:
  "corres tcb_relation (tcb_at t) (tcb_at' t)
          (gets_the (get_tcb t)) (getObject t)" apply (rule corres_guard_imp) apply (rule corres_gets_the) apply (rule corres_get_tcb) apply (simp add: tcb_at_def) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres tcb_relation (tcb_at t) (tcb_at' t) (gets_the (get_tcb t)) (getObject t) proof (prove)
goal (3 subgoals):
 1. corres tcb_relation ?Q ?Q' (gets_the (get_tcb t)) (getObject t)
 2. \<And>s. tcb_at t s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres (tcb_relation \<circ> the) ?P4 ?Q' (gets (get_tcb t)) (getObject t)
 2. \<And>s. tcb_at t s \<Longrightarrow> (?P4 and (\<lambda>s. get_tcb t s \<noteq> None)) s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (2 subgoals):
 1. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and (\<lambda>s. get_tcb t s \<noteq> None)) s
 2. \<And>s. tcb_at' t s \<Longrightarrow> tcb_at' t s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<Longrightarrow> tcb_at' t s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadGet_corres:
  assumes x: "\<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow> r (f tcb) (f' tcb')"
  shows      "corres r (tcb_at t) (tcb_at' t) (thread_get f t) (threadGet f' t)" apply (simp add: thread_get_def threadGet_def) apply (fold liftM_def) apply simp apply (rule corres_rel_imp) apply (rule getObject_TCB_corres) apply (simp add: x) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r (tcb_at t) (tcb_at' t) (thread_get f t) (threadGet f' t) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>x. r x \<circ> f') (tcb_at t) (tcb_at' t) (do tcb <- gets_the (get_tcb t);
return (f tcb)
od) (getObject t) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>x. r x \<circ> f') (tcb_at t) (tcb_at' t) (liftM f (gets_the (get_tcb t))) (getObject t) proof (prove)
goal (1 subgoal):
 1. corres ((\<lambda>x. r x \<circ> f') \<circ> f) (tcb_at t) (tcb_at' t) (gets_the (get_tcb t)) (getObject t) proof (prove)
goal (2 subgoals):
 1. corres ?r' (tcb_at t) (tcb_at' t) (gets_the (get_tcb t)) (getObject t)
 2. \<And>x y. ?r' x y \<Longrightarrow> ((\<lambda>x. r x \<circ> f') \<circ> f) x y proof (prove)
goal (1 subgoal):
 1. \<And>x y. tcb_relation x y \<Longrightarrow> ((\<lambda>x. r x \<circ> f') \<circ> f) x y proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadGet_inv [wp]: "\<lbrace>P\<rbrace> threadGet f t \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: threadGet_def getObject_inv_tcb | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> threadGet f t \<lbrace>\<lambda>rv. P\<rbrace>
theory TcbAcc_R

lemma ball_tcb_cte_casesI:
  "\<lbrakk> P (tcbCTable, tcbCTable_update);
     P (tcbVTable, tcbVTable_update);
     P (tcbReply, tcbReply_update);
     P (tcbCaller, tcbCaller_update);
     P (tcbIPCBufferFrame, tcbIPCBufferFrame_update) \<rbrakk>
    \<Longrightarrow> \<forall>x \<in> ran tcb_cte_cases. P x" by (simp add: tcb_cte_cases_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (tcbCTable, tcbCTable_update); P (tcbVTable, tcbVTable_update); P (tcbReply, tcbReply_update); P (tcbCaller, tcbCaller_update); P (tcbIPCBufferFrame, tcbIPCBufferFrame_update)\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. P x
theory TcbAcc_R

lemma all_tcbI:
  "\<lbrakk> \<And>a b c d e f g h i j k l m n p q. P (Thread a b c d e f g h i j k l m n p q) \<rbrakk> \<Longrightarrow> \<forall>tcb. P tcb" by (rule allI, case_tac tcb, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c d e f g h i j k l m n p q. P (Thread a b c d e f g h i j k l m n p q)) \<Longrightarrow> \<forall>tcb. P tcb
theory TcbAcc_R

lemma pspace_relation_tcb_at:
  assumes p: "pspace_relation (kheap a) (ksPSpace c)"
  assumes t: "tcb_at' t c"
  shows "tcb_at t a" using assms apply (clarsimp simp: obj_at'_def projectKOs) apply (erule(1) pspace_dom_relatedE) apply (erule(1) obj_relation_cutsE) apply (clarsimp simp: other_obj_relation_def is_tcb obj_at_def
                 split: Structures_A.kernel_object.split_asm if_split_asm
                        ARM_A.arch_kernel_obj.split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at t a proof (prove)
using this:
pspace_relation (kheap a) (ksPSpace c)
tcb_at' t c

goal (1 subgoal):
 1. tcb_at t a proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); ksPSpace c t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) c\<rbrakk> \<Longrightarrow> tcb_at t a proof (prove)
goal (1 subgoal):
 1. \<And>obj y ko P. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) c; kheap a y = Some ko; (t, P) \<in> obj_relation_cuts ko y; P ko (KOTCB obj)\<rbrakk> \<Longrightarrow> tcb_at t a proof (prove)
goal (5 subgoals):
 1. \<And>obj y ko P sz cs z cap cte. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) c; kheap a y = Some ko; P ko (KOTCB obj); ko = CNode sz cs; well_formed_cnode_n sz cs; t = cte_map (y, z); KOTCB obj = KOCTE cte; cs z = Some cap; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> tcb_at t a
 2. \<And>obj y ko P pt z pte'. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) c; kheap a y = Some ko; P ko (KOTCB obj); ko = ArchObj (PageTable pt); t = y + (UCAST(8 \<rightarrow> 32) z << 2); KOTCB obj = KOArch (KOPTE pte'); pte_relation_aligned z (pt z) pte'\<rbrakk> \<Longrightarrow> tcb_at t a
 3. \<And>obj y ko P pd z pde'. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) c; kheap a y = Some ko; P ko (KOTCB obj); ko = ArchObj (PageDirectory pd); t = y + (UCAST(12 \<rightarrow> 32) z << 2); KOTCB obj = KOArch (KOPDE pde'); pde_relation_aligned z (pd z) pde'\<rbrakk> \<Longrightarrow> tcb_at t a
 4. \<And>obj y ko P sz dev n. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) c; kheap a y = Some ko; P ko (KOTCB obj); ko = ArchObj (DataPage dev sz); KOTCB obj = (if dev then KOUserDataDevice else KOUserData); t = y + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize sz - pageBits)\<rbrakk> \<Longrightarrow> tcb_at t a
 5. \<And>obj y ko P. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) c; kheap a y = Some ko; P ko (KOTCB obj); t = y; other_obj_relation ko (KOTCB obj); is_other_obj_relation_type (a_type ko)\<rbrakk> \<Longrightarrow> tcb_at t a proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadSet_tcb' [wp]:
  "\<lbrace>tcb_at' t\<rbrace> threadSet f t' \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>" by (simp add: threadSet_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> threadSet f t' \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
theory TcbAcc_R

lemma threadSet_nosch[wp]:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" unfolding threadSet_def by (simp add: updateObject_default_def | wp setObject_nosch)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> do tcb <- getObject t;
setObject t $ f tcb
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>
theory TcbAcc_R

lemma setObject_tcb_valid_objs:
  "\<lbrace>valid_objs' and (tcb_at' t and valid_obj' (injectKO v))\<rbrace> setObject t (v :: tcb) \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" apply (rule setObject_valid_objs') apply (clarsimp simp: updateObject_default_def in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and (tcb_at' t and valid_obj' (injectKO v))\<rbrace> setObject t v \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x n ko s ko' s'. \<lbrakk>(ko', s') \<in> fst (updateObject v ko t x n s); (tcb_at' t and valid_obj' (injectKO v)) s; valid_obj' ko s; lookupAround2 t (ksPSpace s) = (Some (x, ko), n)\<rbrakk> \<Longrightarrow> valid_obj' ko' s proof (prove)
goal:
No subgoals!