kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_R

lemma threadSet_ct_idle_or_in_cur_domain':
  "(\<And>tcb. tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow> \<lbrace>ct_idle_or_in_cur_domain'\<rbrace> threadSet F t \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>" apply (rule ct_idle_or_in_cur_domain'_lift) apply (wp hoare_vcg_disj_lift| simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow> \<lbrace>ct_idle_or_in_cur_domain'\<rbrace> threadSet F t \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>P. (\<And>tcb. tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 2. \<And>P. (\<And>tcb. tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 3. \<And>P. (\<And>tcb. tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 4. \<And>P. (\<And>tcb. tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 5. \<And>d a ta t'. (\<And>tcb. tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow> \<lbrace>\<lambda>s. ta = t' \<or> obj_at' (\<lambda>tcb. d = tcbDomain tcb) ta s\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. ta = t' \<or> obj_at' (\<lambda>tcb. d = tcbDomain tcb) ta s\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setObject_tcb_ksDomScheduleIdx [wp]:
  "\<lbrace>\<lambda>s. P (ksDomScheduleIdx s) \<rbrace> setObject t (v::tcb) \<lbrace>\<lambda>_ s. P (ksDomScheduleIdx s)\<rbrace>" apply (simp add:setObject_def) apply (simp add: updateObject_default_def in_monad) apply (wp|wpc)+ apply (simp add: projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> setObject t v \<lbrace>\<lambda>_ s. P (ksDomScheduleIdx s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> do ps <- gets ksPSpace;
case lookupAround2 t ps of (before, after) \<Rightarrow> do (ptr', obj) <- assert_opt before;
obj' <- updateObject_default v obj t ptr' after;
modify (ksPSpace_update (\<lambda>_. ps(ptr' \<mapsto> obj')))
od
od \<lbrace>\<lambda>_ s. P (ksDomScheduleIdx s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> do ps <- gets ksPSpace;
case lookupAround2 t ps of (before, after) \<Rightarrow> do (ptr', obj) <- assert_opt before;
obj' <- do y <- assert (t = ptr');
_ <- projectKO obj;
y <- alignCheck t (objBits v);
y <- magnitudeCheck t after (objBits v);
return (KOTCB v)
od;
modify (ksPSpace_update (\<lambda>_. ps(ptr' \<mapsto> obj')))
od
od \<lbrace>\<lambda>_ s. P (ksDomScheduleIdx s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ksDomScheduleIdx s) \<Longrightarrow> \<forall>x xa. lookupAround2 t (ksPSpace s) = (x, xa) \<longrightarrow> x \<noteq> None \<longrightarrow> (\<forall>xa xb. the x = (xa, xb) \<longrightarrow> t = xa \<longrightarrow> P (ksDomScheduleIdx (s\<lparr>ksPSpace := (ksPSpace s)(xa \<mapsto> KOTCB v)\<rparr>))) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadSet_valid_dom_schedule':
  "\<lbrace> valid_dom_schedule'\<rbrace> threadSet F t \<lbrace>\<lambda>_. valid_dom_schedule'\<rbrace>" unfolding threadSet_def by (wp setObject_ksDomSchedule_inv hoare_Ball_helper)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_dom_schedule'\<rbrace> threadSet F t \<lbrace>\<lambda>_. valid_dom_schedule'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_dom_schedule'\<rbrace> do tcb <- getObject t;
setObject t $ F tcb
od \<lbrace>\<lambda>_. valid_dom_schedule'\<rbrace>
theory TcbAcc_R

lemma zobj_refs'_capRange:
  "s \<turnstile>' cap \<Longrightarrow> zobj_refs' cap \<subseteq> capRange cap" by (cases cap; simp add: valid_cap'_def capAligned_def capRange_def is_aligned_no_overflow)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cap' cap s \<Longrightarrow> zobj_refs' cap \<subseteq> capRange cap
theory TcbAcc_R

lemma global'_no_ex_cap:
  "\<lbrakk>valid_global_refs' s; valid_pspace' s\<rbrakk> \<Longrightarrow> \<not> ex_nonz_cap_to' (ksIdleThread s) s" apply (clarsimp simp: ex_nonz_cap_to'_def valid_global_refs'_def valid_refs'_def2 valid_pspace'_def) apply (drule cte_wp_at_norm', clarsimp) apply (frule(1) cte_wp_at_valid_objs_valid_cap', clarsimp) apply (clarsimp simp: cte_wp_at'_def dest!: zobj_refs'_capRange, blast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_global_refs' s; valid_pspace' s\<rbrakk> \<Longrightarrow> \<not> ex_nonz_cap_to' (ksIdleThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>cref. \<lbrakk>\<forall>cref. \<not> cte_wp_at' (\<lambda>c. kernel_data_refs \<inter> capRange (cteCap c) \<noteq> {}) cref s; valid_objs' s; global_refs' s \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; cte_wp_at' (\<lambda>c. ksIdleThread s \<in> zobj_refs' (cteCap c)) cref s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref cte. \<lbrakk>\<forall>cref. \<not> cte_wp_at' (\<lambda>c. kernel_data_refs \<inter> capRange (cteCap c) \<noteq> {}) cref s; valid_objs' s; global_refs' s \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; cte_wp_at' ((=) cte) cref s; ksIdleThread s \<in> zobj_refs' (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref cte. \<lbrakk>\<forall>cref. \<not> cte_wp_at' (\<lambda>c. kernel_data_refs \<inter> capRange (cteCap c) \<noteq> {}) cref s; valid_objs' s; global_refs' s \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; cte_wp_at' ((=) cte) cref s; ksIdleThread s \<in> zobj_refs' (cteCap cte); valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma getObject_tcb_sp:
  "\<lbrace>P\<rbrace> getObject r \<lbrace>\<lambda>t::tcb. P and ko_at' t r\<rbrace>" by (wp getObject_obj_at'; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getObject r \<lbrace>\<lambda>t. P and ko_at' t r\<rbrace>
theory TcbAcc_R

lemma asUser_corres:
  assumes y: "corres_underlying Id False True r \<top> \<top> f g"
  shows      "corres r (tcb_at t and invs) (tcb_at' t and invs') (as_user t f) (asUser t g)" apply (rule corres_guard_imp) apply (rule asUser_corres' [OF y]) apply (simp add: invs_def valid_state_def valid_pspace_def) apply (simp add: invs'_def valid_state'_def valid_pspace'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r (tcb_at t and invs) (tcb_at' t and invs') (as_user t f) (asUser t g) proof (prove)
goal (3 subgoals):
 1. corres r ?Q ?Q' (as_user t f) (asUser t g)
 2. \<And>s. (tcb_at t and invs) s \<Longrightarrow> ?Q s
 3. \<And>s. (tcb_at' t and invs') s \<Longrightarrow> ?Q' s proof (prove)
goal (2 subgoals):
 1. \<And>s. (tcb_at t and invs) s \<Longrightarrow> tcb_at t s
 2. \<And>s. (tcb_at' t and invs') s \<Longrightarrow> tcb_at' t s proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_at' t and invs') s \<Longrightarrow> tcb_at' t s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_inv:
  assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>x. P\<rbrace>"
  shows      "\<lbrace>P\<rbrace> asUser t f \<lbrace>\<lambda>x. P\<rbrace>" proof - have P: "\<And>a b input. (a, b) \<in> fst (f input) \<Longrightarrow> b = input" by (rule use_valid [OF _ x], assumption, rule refl) have R: "\<And>x. tcbArch_update (\<lambda>_. tcbArch x) x = x" by (case_tac x, simp) show ?thesis apply (simp add: asUser_def split_def threadGet_def threadSet_def
                     liftM_def bind_assoc) apply (clarsimp simp: valid_def in_monad getObject_def setObject_def
                          loadObject_default_def projectKOs objBits_simps'
                          modify_def split_def updateObject_default_def
                          in_magnitude_check select_f_def
                   dest!: P) apply (simp add: R map_upd_triv) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> asUser t f \<lbrace>\<lambda>x. P\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> asUser t f \<lbrace>\<lambda>x. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b input. (a, b) \<in> fst (f input) \<Longrightarrow> b = input proof (state)
this:
(?a, ?b) \<in> fst (f ?input) \<Longrightarrow> ?b = ?input

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> asUser t f \<lbrace>\<lambda>x. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. tcbArch_update (\<lambda>_. tcbArch x) x = x proof (state)
this:
tcbArch_update (\<lambda>_. tcbArch ?x) ?x = ?x

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> asUser t f \<lbrace>\<lambda>x. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> asUser t f \<lbrace>\<lambda>x. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do x <- getObject t;
p <- select_f (f (atcbContextGet (tcbArch x)));
x <- getObject t;
y <- setObject t (tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch x)) x);
return (fst p)
od \<lbrace>\<lambda>x. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s uu_. \<lbrakk>P s; ksPSpace s t = Some (KOTCB uu_); ps_clear t 9 s; is_aligned t 9\<rbrakk> \<Longrightarrow> P (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch uu_) uu_))\<rparr>) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>P\<rbrace> asUser t f \<lbrace>\<lambda>x. P\<rbrace>

goal:
No subgoals!
theory TcbAcc_R

lemma asUser_getRegister_corres:
 "corres (=) (tcb_at t) (tcb_at' t)
        (as_user t (getRegister r)) (asUser t (getRegister r))" apply (rule asUser_corres') apply (clarsimp simp: getRegister_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t) (tcb_at' t) (as_user t (getRegister r)) (asUser t (getRegister r)) proof (prove)
goal (1 subgoal):
 1. corres_underlying Id False True (=) (\<lambda>_. True) (\<lambda>_. True) (getRegister r) (getRegister r) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma user_getreg_inv'[wp]:
  "\<lbrace>P\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>x. P\<rbrace>" by (wp asUser_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>x. P\<rbrace>
theory TcbAcc_R

lemma asUser_typ_at' [wp]:
  "\<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> asUser t' f \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>" by (simp add: asUser_def bind_assoc split_def, wp select_f_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> asUser t' f \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>
theory TcbAcc_R

lemma asUser_invs[wp]:
  "\<lbrace>invs' and tcb_at' t\<rbrace> asUser t m \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: asUser_def split_def) apply (wp hoare_drop_imps | simp)+ apply (wp threadSet_invs_trivial hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t\<rbrace> asUser t m \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>uc p. \<lbrace>?B2 uc p\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t \<lbrace>\<lambda>y. invs'\<rbrace>
 2. \<And>uc. \<lbrace>?B1 uc\<rbrace> select_f (m uc) \<lbrace>?B2 uc\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>?B1\<rbrace>
 4. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_nosch[wp]:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> asUser t m \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" apply (simp add: asUser_def split_def) apply (wp hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> asUser t m \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_valid_objs [wp]:
  "\<lbrace>valid_objs'\<rbrace> asUser t f \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" apply (simp add: asUser_def split_def) apply (wp threadSet_valid_objs' hoare_drop_imps
             | simp add: valid_tcb'_def tcb_cte_cases_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> asUser t f \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (f uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_valid_pspace'[wp]:
  "\<lbrace>valid_pspace'\<rbrace> asUser t m \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>" apply (simp add: asUser_def split_def) apply (wp threadSet_valid_pspace' hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace'\<rbrace> asUser t m \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace'\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_valid_queues[wp]:
  "\<lbrace>Invariants_H.valid_queues\<rbrace> asUser t m \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" apply (simp add: asUser_def split_def) apply (wp hoare_drop_imps | simp)+ apply (wp threadSet_valid_queues hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues\<rbrace> asUser t m \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>uc p. \<lbrace>?B2 uc p\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t \<lbrace>\<lambda>y. Invariants_H.valid_queues\<rbrace>
 2. \<And>uc. \<lbrace>?B1 uc\<rbrace> select_f (m uc) \<lbrace>?B2 uc\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>?B1\<rbrace>
 4. \<And>s. Invariants_H.valid_queues s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_ifunsafe'[wp]:
  "\<lbrace>if_unsafe_then_cap'\<rbrace> asUser t m \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" apply (simp add: asUser_def split_def) apply (wp threadSet_ifunsafe' hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap'\<rbrace> asUser t m \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap'\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_st_refs_of'[wp]:
  "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace>
     asUser t m
   \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" apply (simp add: asUser_def split_def) apply (wp threadSet_state_refs_of' hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> asUser t m \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_iflive'[wp]:
  "\<lbrace>if_live_then_nonz_cap'\<rbrace> asUser t m \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" apply (simp add: asUser_def split_def) apply (wp threadSet_iflive' hoare_drop_imps | clarsimp | auto)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap'\<rbrace> asUser t m \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap'\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_cur_tcb[wp]:
  "\<lbrace>cur_tcb'\<rbrace> asUser t m \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>" apply (simp add: asUser_def split_def) apply (wp threadSet_cur hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> asUser t m \<lbrace>\<lambda>rv. cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv. cur_tcb'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_cap_to'[wp]:
  "\<lbrace>ex_nonz_cap_to' p\<rbrace> asUser t m \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>" by (wp ex_nonz_cap_to_pres')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p\<rbrace> asUser t m \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>
theory TcbAcc_R

lemma asUser_pred_tcb_at' [wp]:
  "\<lbrace>pred_tcb_at' proj P t\<rbrace> asUser t' f \<lbrace>\<lambda>_. pred_tcb_at' proj P t\<rbrace>" apply (simp add: asUser_def split_def) apply (wp threadSet_pred_tcb_no_state) apply (case_tac tcb) apply (simp add: tcb_to_itcb'_def) apply (wpsimp wp: select_f_inv)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t\<rbrace> asUser t' f \<lbrace>\<lambda>_. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t';
p <- select_f (f uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t';
return (fst p)
od \<lbrace>\<lambda>_. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>uc p tcb. proj (tcb_to_itcb' (tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb)) = proj (tcb_to_itcb' tcb)
 2. \<And>uc. \<lbrace>?B1 uc\<rbrace> select_f (f uc) \<lbrace>\<lambda>p. pred_tcb_at' proj P t\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t' \<lbrace>?B1\<rbrace>
 4. \<And>s. pred_tcb_at' proj P t s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>uc p tcb x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. tcb = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 \<Longrightarrow> proj (tcb_to_itcb' (tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb)) = proj (tcb_to_itcb' tcb)
 2. \<And>uc. \<lbrace>?B1 uc\<rbrace> select_f (f uc) \<lbrace>\<lambda>p. pred_tcb_at' proj P t\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t' \<lbrace>?B1\<rbrace>
 4. \<And>s. pred_tcb_at' proj P t s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>uc. \<lbrace>?B1 uc\<rbrace> select_f (f uc) \<lbrace>\<lambda>p. pred_tcb_at' proj P t\<rbrace>
 2. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t' \<lbrace>?B1\<rbrace>
 3. \<And>s. pred_tcb_at' proj P t s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!