kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_R

lemma setObject_tcb_at':
  "\<lbrace>tcb_at' t'\<rbrace> setObject t (v :: tcb) \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace>" apply (rule obj_at_setObject1) apply (clarsimp simp: updateObject_default_def return_def in_monad) apply (simp add: objBits_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t'\<rbrace> setObject t v \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>v p q n ko s x s''. (x, s'') \<in> fst (updateObject v ko p q n s) \<Longrightarrow> x = injectKO v
 2. \<And>v v'. objBits v = objBits v' proof (prove)
goal (1 subgoal):
 1. \<And>v v'. objBits v = objBits v' proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setObject_sa_unchanged:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setObject t (v :: tcb) \<lbrace>\<lambda>rv s.  P (ksSchedulerAction s)\<rbrace>" apply (simp add: setObject_def split_def) apply (wp | simp add: updateObject_default_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setObject t v \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- updateObject_default v (snd p) t (fst p) (snd (lookupAround2 t ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setObject_queues_unchanged:
  assumes inv: "\<And>P p q n obj. \<lbrace>P\<rbrace> updateObject v obj p q n \<lbrace>\<lambda>r. P\<rbrace>"
  shows "\<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> setObject t v \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace>" apply (simp add: setObject_def split_def) apply (wp inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> setObject t v \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- updateObject v (snd p) t (fst p) (snd (lookupAround2 t ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setObject_queues_unchanged_tcb[wp]:
  "\<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> setObject t (v :: tcb) \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace>" apply (rule setObject_queues_unchanged) apply (wp|simp add: updateObject_default_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> setObject t v \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P p q n obj. \<lbrace>P\<rbrace> updateObject v obj p q n \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setObject_queuesL1_unchanged_tcb[wp]:
  "\<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> setObject t (v :: tcb) \<lbrace>\<lambda>rv s. P (ksReadyQueuesL1Bitmap s)\<rbrace>" by (clarsimp simp: setObject_def split_def)
     (wp | simp add: updateObject_default_def)+

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

lemma setObject_tcb_ctes_of[wp]:
  "\<lbrace>\<lambda>s. P (ctes_of s) \<and>
     obj_at' (\<lambda>t. \<forall>(getF, setF) \<in> ran tcb_cte_cases. getF t = getF v) t s\<rbrace>
     setObject t v
   \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>" apply (rule setObject_ctes_of) apply (clarsimp simp: updateObject_default_def in_monad prod_eq_iff
                         obj_at'_def objBits_simps' in_magnitude_check
                         projectKOs) apply fastforce apply (clarsimp simp: updateObject_default_def in_monad prod_eq_iff
                        obj_at'_def objBits_simps in_magnitude_check
                        projectKOs bind_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ctes_of s) \<and> obj_at' (\<lambda>t. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF t = getF v) t s\<rbrace> setObject t v \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P P' p x n tcb s ta. \<lbrakk>ta \<in> fst (updateObject v (KOTCB tcb) t x n s); obj_at' (\<lambda>t. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF t = getF v) t s; lookupAround2 t (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. ta = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF tcb)
 2. \<And>P P' p x n cte s. fst (updateObject v (KOCTE cte) t x n s) = {} proof (prove)
goal (2 subgoals):
 1. \<And>s obj a b. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF obj = getF v; ps_clear t 9 s; (a, b) \<in> ran tcb_cte_cases\<rbrakk> \<Longrightarrow> a v = a obj
 2. \<And>P P' p x n cte s. fst (updateObject v (KOCTE cte) t x n s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>P P' p x n cte s. fst (updateObject v (KOCTE cte) t x n s) = {} proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setObject_tcb_mdb' [wp]:
  "\<lbrace> valid_mdb' and
     obj_at' (\<lambda>t. \<forall>(getF, setF) \<in> ran tcb_cte_cases. getF t = getF v) t\<rbrace>
  setObject t (v :: tcb)
  \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>" unfolding valid_mdb'_def pred_conj_def by (rule setObject_tcb_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb' and obj_at' (\<lambda>t. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF t = getF v) t\<rbrace> setObject t v \<lbrace>\<lambda>rv. valid_mdb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. valid_mdb_ctes (ctes_of x) \<and> obj_at' (\<lambda>t. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF t = getF v) t x\<rbrace> setObject t v \<lbrace>\<lambda>rv s. valid_mdb_ctes (ctes_of s)\<rbrace>
theory TcbAcc_R

lemma setObject_tcb_state_refs_of'[wp]:
  "\<lbrace>\<lambda>s. P ((state_refs_of' s) (t := tcb_st_refs_of' (tcbState v)
                                  \<union> tcb_bound_refs' (tcbBoundNotification v)))\<rbrace>
     setObject t (v :: tcb) \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" by (wp setObject_state_refs_of',
      simp_all add: objBits_simps' fun_upd_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of' s)(t := tcb_st_refs_of' (tcbState v) \<union> tcb_bound_refs' (tcbBoundNotification v)))\<rbrace> setObject t v \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>
theory TcbAcc_R

lemma setObject_tcb_iflive':
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and>
      (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' t s)
       \<and> obj_at' (\<lambda>t. \<forall>(getF, setF) \<in> ran tcb_cte_cases. getF t = getF v) t s\<rbrace>
     setObject t (v :: tcb)
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" apply (rule setObject_iflive') apply (simp add: objBits_simps')+ apply (clarsimp simp: updateObject_default_def in_monad projectKOs
                         in_magnitude_check objBits_simps' prod_eq_iff
                         obj_at'_def) apply fastforce apply (clarsimp simp: updateObject_default_def bind_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' t s) \<and> obj_at' (\<lambda>t. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF t = getF v) t s\<rbrace> setObject t v \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ko s x y n. updateObject v ko t y n s = updateObject_default v ko t y n s
 2. \<And>x. objBits x = ?n
 3. 1 < 2 ^ ?n
 4. \<And>x n tcb s ta. \<lbrakk>ta \<in> fst (updateObject v (KOTCB tcb) t x n s); obj_at' (\<lambda>t. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF t = getF v) t s; lookupAround2 t (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. ta = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF tcb)
 5. \<And>x n cte s. fst (updateObject v (KOCTE cte) t x n s) = {} proof (prove)
goal (2 subgoals):
 1. \<And>x n tcb s ta. \<lbrakk>ta \<in> fst (updateObject_default v (KOTCB tcb) t x n s); obj_at' (\<lambda>t. \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF t = getF v) t s; lookupAround2 t (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. ta = (KOTCB tcb', s) \<and> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF tcb' = getF tcb)
 2. \<And>x n cte s. fst (updateObject v (KOCTE cte) t x n s) = {} proof (prove)
goal (2 subgoals):
 1. \<And>s obj a b. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF obj = getF v; ps_clear t 9 s; (a, b) \<in> ran tcb_cte_cases\<rbrakk> \<Longrightarrow> a v = a obj
 2. \<And>x n cte s. fst (updateObject v (KOCTE cte) t x n s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x n cte s. fst (updateObject v (KOCTE cte) t x n s) = {} proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setObject_tcb_idle':
  "\<lbrace>\<lambda>s. valid_idle' s \<and>
     (t = ksIdleThread s \<longrightarrow> idle' (tcbState v) \<and> tcbBoundNotification v = None)\<rbrace>
     setObject t (v :: tcb) \<lbrace>\<lambda>rv. valid_idle'\<rbrace>" apply (rule hoare_pre) apply (rule setObject_idle') apply (simp add: objBits_simps')+ apply (simp add: updateObject_default_inv) apply (simp add: projectKOs idle_tcb_ps_def idle_tcb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_idle' s \<and> (t = ksIdleThread s \<longrightarrow> idle' (tcbState v) \<and> tcbBoundNotification v = None)\<rbrace> setObject t v \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setObject t v \<lbrace>\<lambda>rv. valid_idle'\<rbrace>
 2. \<And>s. valid_idle' s \<and> (t = ksIdleThread s \<longrightarrow> idle' (tcbState v) \<and> tcbBoundNotification v = None) \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>ko s x y n. updateObject v ko t y n s = updateObject_default v ko t y n s
 2. \<And>x. objBits x = ?n3
 3. 1 < 2 ^ ?n3
 4. \<And>P p q n ko. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> updateObject v p q n ko \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>
 5. \<And>s. valid_idle' s \<and> (t = ksIdleThread s \<longrightarrow> idle' (tcbState v) \<and> tcbBoundNotification v = None) \<Longrightarrow> valid_idle' s \<and> (t = ksIdleThread s \<longrightarrow> (\<exists>val. idle_tcb_ps val) \<longrightarrow> idle_tcb_ps v) proof (prove)
goal (2 subgoals):
 1. \<And>P p q n ko. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> updateObject_default v p q n ko \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>
 2. \<And>s. valid_idle' s \<and> (t = ksIdleThread s \<longrightarrow> idle' (tcbState v) \<and> tcbBoundNotification v = None) \<Longrightarrow> valid_idle' s \<and> (t = ksIdleThread s \<longrightarrow> (\<exists>val. idle_tcb_ps val) \<longrightarrow> idle_tcb_ps v) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_idle' s \<and> (t = ksIdleThread s \<longrightarrow> idle' (tcbState v) \<and> tcbBoundNotification v = None) \<Longrightarrow> valid_idle' s \<and> (t = ksIdleThread s \<longrightarrow> (\<exists>val. idle_tcb_ps val) \<longrightarrow> idle_tcb_ps v) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setObject_tcb_irq_node'[wp]:
  "\<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> setObject t (v :: tcb) \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace>" apply (simp add: setObject_def split_def) apply (wp updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> setObject t v \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- updateObject_default v (snd p) t (fst p) (snd (lookupAround2 t ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setObject_tcb_ifunsafe':
  "\<lbrace>if_unsafe_then_cap' and obj_at' (\<lambda>t. \<forall>(getF, setF) \<in> ran tcb_cte_cases. getF t = getF v) t\<rbrace>
     setObject t (v :: tcb) \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" unfolding pred_conj_def apply (rule setObject_ifunsafe') apply (clarsimp simp: updateObject_default_def in_monad projectKOs
                          in_magnitude_check objBits_simps' prod_eq_iff
                          obj_at'_def) apply fastforce apply (clarsimp simp: updateObject_default_def bind_def projectKOs) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap' and obj_at' (\<lambda>t. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF t = getF v) t\<rbrace> setObject t v \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. if_unsafe_then_cap' x \<and> obj_at' (\<lambda>t. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF t = getF v) t x\<rbrace> setObject t v \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x n tcb xa ta. \<lbrakk>ta \<in> fst (updateObject v (KOTCB tcb) t x n xa); obj_at' (\<lambda>t. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF t = getF v) t xa; lookupAround2 t (ksPSpace xa) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. ta = (KOTCB tcb', xa) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF tcb)
 2. \<And>x n cte xa. fst (updateObject v (KOCTE cte) t x n xa) = {}
 3. \<And>P. \<lbrace>\<lambda>x. P (irq_node' x)\<rbrace> setObject t v \<lbrace>\<lambda>rv x. P (irq_node' x)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>xa obj a b. \<lbrakk>ksPSpace xa t = Some (KOTCB obj); is_aligned t 9; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF obj = getF v; ps_clear t 9 xa; (a, b) \<in> ran tcb_cte_cases\<rbrakk> \<Longrightarrow> a v = a obj
 2. \<And>x n cte xa. fst (updateObject v (KOCTE cte) t x n xa) = {}
 3. \<And>P. \<lbrace>\<lambda>x. P (irq_node' x)\<rbrace> setObject t v \<lbrace>\<lambda>rv x. P (irq_node' x)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x n cte xa. fst (updateObject v (KOCTE cte) t x n xa) = {}
 2. \<And>P. \<lbrace>\<lambda>x. P (irq_node' x)\<rbrace> setObject t v \<lbrace>\<lambda>rv x. P (irq_node' x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>x. P (irq_node' x)\<rbrace> setObject t v \<lbrace>\<lambda>rv x. P (irq_node' x)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setObject_tcb_arch' [wp]:
  "\<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setObject t (v :: tcb) \<lbrace>\<lambda>rv s. P (ksArchState s)\<rbrace>" apply (simp add: setObject_def split_def updateObject_default_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setObject t v \<lbrace>\<lambda>rv s. P (ksArchState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- do y <- assert (t = fst p);
_ <- projectKO (snd p);
y <- alignCheck t (objBits v);
y <- magnitudeCheck t (snd (lookupAround2 t ps)) (objBits v);
return (KOTCB v)
od;
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksArchState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ksArchState s) \<Longrightarrow> fst (lookupAround2 t (ksPSpace s)) \<noteq> None \<longrightarrow> t = fst (the (fst (lookupAround2 t (ksPSpace s)))) \<longrightarrow> P (ksArchState (s\<lparr>ksPSpace := (ksPSpace s)(fst (the (fst (lookupAround2 t (ksPSpace s)))) \<mapsto> KOTCB v)\<rparr>)) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setObject_tcb_valid_arch' [wp]:
  "\<lbrace>valid_arch_state'\<rbrace> setObject t (v :: tcb) \<lbrace>\<lambda>rv. valid_arch_state'\<rbrace>" by (wp valid_arch_state_lift' setObject_typ_at')

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

lemma setObject_tcb_refs' [wp]:
  "\<lbrace>\<lambda>s. P (global_refs' s)\<rbrace> setObject t (v::tcb) \<lbrace>\<lambda>rv s. P (global_refs' s)\<rbrace>" apply (clarsimp simp: setObject_def split_def updateObject_default_def) apply wp apply (simp add: global_refs'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (global_refs' s)\<rbrace> setObject t v \<lbrace>\<lambda>rv s. P (global_refs' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (global_refs' s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- do y <- assert (t = fst p);
_ <- projectKO (snd p);
y <- alignCheck t (objBits v);
y <- magnitudeCheck t (snd (lookupAround2 t ps)) (objBits v);
return (KOTCB v)
od;
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (global_refs' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (global_refs' s) \<Longrightarrow> fst (lookupAround2 t (ksPSpace s)) \<noteq> None \<longrightarrow> t = fst (the (fst (lookupAround2 t (ksPSpace s)))) \<longrightarrow> P (global_refs' (s\<lparr>ksPSpace := (ksPSpace s)(fst (the (fst (lookupAround2 t (ksPSpace s)))) \<mapsto> KOTCB v)\<rparr>)) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setObject_tcb_irq_states' [wp]:
  "\<lbrace>valid_irq_states'\<rbrace> setObject t (v :: tcb) \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace>" apply (rule hoare_pre) apply (rule hoare_use_eq [where f=ksInterruptState, OF setObject_ksInterrupt]) apply (simp, rule updateObject_default_inv) apply (rule hoare_use_eq [where f=ksMachineState, OF setObject_ksMachine]) apply (simp, rule updateObject_default_inv) apply wp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> setObject t v \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setObject t v \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace>
 2. \<And>s. valid_irq_states' s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>P p q n ko. \<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> updateObject v p q n ko \<lbrace>\<lambda>rv s. P (ksInterruptState s)\<rbrace>
 2. \<And>f. \<lbrace>?P3 f\<rbrace> setObject t v \<lbrace>\<lambda>rv s. valid_irq_masks' (intStateIRQTable f) (irq_masks (ksMachineState s))\<rbrace>
 3. \<And>s. valid_irq_states' s \<Longrightarrow> ?P3 (ksInterruptState s) s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<rbrace> setObject t v \<lbrace>\<lambda>rv s. valid_irq_masks' (intStateIRQTable f) (irq_masks (ksMachineState s))\<rbrace>
 2. \<And>s. valid_irq_states' s \<Longrightarrow> ?P3 (ksInterruptState s) s proof (prove)
goal (3 subgoals):
 1. \<And>f P p q n ko. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> updateObject v p q n ko \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>
 2. \<And>f fa. \<lbrace>?P16 f fa\<rbrace> setObject t v \<lbrace>\<lambda>rv s. valid_irq_masks' (intStateIRQTable f) (irq_masks fa)\<rbrace>
 3. \<And>s. valid_irq_states' s \<Longrightarrow> ?P16 (ksInterruptState s) (ksMachineState s) s proof (prove)
goal (2 subgoals):
 1. \<And>f fa. \<lbrace>?P16 f fa\<rbrace> setObject t v \<lbrace>\<lambda>rv s. valid_irq_masks' (intStateIRQTable f) (irq_masks fa)\<rbrace>
 2. \<And>s. valid_irq_states' s \<Longrightarrow> ?P16 (ksInterruptState s) (ksMachineState s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_states' s \<Longrightarrow> valid_irq_states' s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma getObject_tcb_wp:
  "\<lbrace>\<lambda>s. tcb_at' p s \<longrightarrow> (\<exists>t::tcb. ko_at' t p s \<and> Q t s)\<rbrace> getObject p \<lbrace>Q\<rbrace>" by (clarsimp simp: getObject_def valid_def in_monad
                     split_def objBits_simps' loadObject_default_def
                     projectKOs obj_at'_def in_magnitude_check)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' p s \<longrightarrow> (\<exists>t. ko_at' t p s \<and> Q t s)\<rbrace> getObject p \<lbrace>Q\<rbrace>
theory TcbAcc_R

lemma threadSet_pspace_no_overlap' [wp]:
  "\<lbrace>pspace_no_overlap' w s\<rbrace> threadSet f t \<lbrace>\<lambda>rv. pspace_no_overlap' w s\<rbrace>" apply (simp add: threadSet_def) apply (wp setObject_tcb_pspace_no_overlap' getObject_tcb_wp) apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' w s\<rbrace> threadSet f t \<lbrace>\<lambda>rv. pspace_no_overlap' w s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' w s\<rbrace> do tcb <- getObject t;
setObject t (f tcb)
od \<lbrace>\<lambda>rv. pspace_no_overlap' w s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. pspace_no_overlap' w s sa \<Longrightarrow> tcb_at' t sa \<longrightarrow> (\<exists>ta. ko_at' ta t sa \<and> (pspace_no_overlap' w s and tcb_at' t) sa) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadSet_global_refsT:
  assumes x: "\<forall>tcb. \<forall>(getF, setF) \<in> ran tcb_cte_cases.
                 getF (F tcb) = getF tcb"
  shows "\<lbrace>valid_global_refs'\<rbrace> threadSet F t \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>" apply (simp add: threadSet_def) apply (wp setObject_tcb_valid_globals' getObject_tcb_wp) apply (clarsimp simp: obj_at'_def projectKOs bspec_split [OF spec [OF x]]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs'\<rbrace> threadSet F t \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs'\<rbrace> do tcb <- getObject t;
setObject t (F tcb)
od \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_global_refs' s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (valid_global_refs' and obj_at' (\<lambda>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb = getF (F ta)) t) s) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadSet_ifunsafe'T:
  assumes x: "\<forall>tcb. \<forall>(getF, setF) \<in> ran tcb_cte_cases. getF (F tcb) = getF tcb"
  shows      "\<lbrace>if_unsafe_then_cap'\<rbrace> threadSet F t \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" apply (simp add: threadSet_def) apply (wp setObject_tcb_ifunsafe' getObject_tcb_wp) apply (clarsimp simp: obj_at'_def bspec_split [OF spec [OF x]]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap'\<rbrace> threadSet F t \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap'\<rbrace> do tcb <- getObject t;
setObject t (F tcb)
od \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. if_unsafe_then_cap' s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (if_unsafe_then_cap' and obj_at' (\<lambda>t. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF t = getF (F ta)) t) s) proof (prove)
goal:
No subgoals!