kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchCNodeInv_AI

lemma finalise_cap_rvk_prog [CNodeInv_AI_assms]:
   "\<lbrace>\<lambda>s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace>
   finalise_cap a b
   \<lbrace>\<lambda>_ s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace>" apply (case_tac a,simp_all add:liftM_def) apply (wp suspend_rvk_prog deleting_irq_handler_rvk_prog
      | clarsimp simp:is_final_cap_def comp_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace> finalise_cap a b \<lbrace>\<lambda>_ s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33. a = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace> do x <- when b (cancel_all_ipc x31);
return (NullCap, NullCap)
od \<lbrace>\<lambda>_ s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace>
 2. \<And>x41 x42 x43. a = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace> do x <- when b (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od);
return (NullCap, NullCap)
od \<lbrace>\<lambda>_ s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace>
 3. \<And>x7. a = ThreadCap x7 \<Longrightarrow> b \<longrightarrow> \<lbrace>\<lambda>s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace> do y <- unbind_notification x7;
y <- suspend x7;
y <- prepare_thread_delete x7;
return (Zombie x7 None 5, NullCap)
od \<lbrace>\<lambda>_ s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace>
 4. \<And>x10. a = IRQHandlerCap x10 \<Longrightarrow> b \<longrightarrow> \<lbrace>\<lambda>s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace> do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od \<lbrace>\<lambda>_ s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace>
 5. \<And>x111 x112 x113. a = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>\<lambda>s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace> do y <- assert b;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>_ s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace>
 6. \<And>x12. a = ArchObjectCap x12 \<Longrightarrow> \<lbrace>\<lambda>s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace> arch_finalise_cap x12 b \<lbrace>\<lambda>_ s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma weak_derived_appropriate [CNodeInv_AI_assms]:
  "weak_derived cap cap' \<Longrightarrow> appropriate_cte_cap cap = appropriate_cte_cap cap'" by (auto simp: weak_derived_def copy_of_def same_object_as_def2
                 appropriate_cte_master
          split: if_split_asm
          dest!: arg_cong[where f=appropriate_cte_cap])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived cap cap' \<Longrightarrow> appropriate_cte_cap cap = appropriate_cte_cap cap'
theory ArchCNodeInv_AI

lemma arch_derive_is_arch:
  "\<lbrace>\<top>\<rbrace> arch_derive_cap c \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> is_arch_cap rv\<rbrace>,-" by (wpsimp simp: is_arch_cap_def arch_derive_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> arch_derive_cap c \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> is_arch_cap rv\<rbrace>, -
theory Tcb_AI

lemma ct_in_state_weaken:
  "\<lbrakk> ct_in_state Q s; \<And>st. Q st \<Longrightarrow> P st \<rbrakk> \<Longrightarrow> ct_in_state P s" by (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_in_state Q s; \<And>st. Q st \<Longrightarrow> P st\<rbrakk> \<Longrightarrow> ct_in_state P s
theory Tcb_AI

lemma ct_in_state_exst_update[simp]: "ct_in_state P (trans_state f s) = ct_in_state P s" by (simp add: ct_in_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_in_state P (trans_state f s) = ct_in_state P s
theory Tcb_AI

lemma setup_reply_master_reply_master[wp]:
  "\<lbrace>valid_objs and tcb_at t\<rbrace> setup_reply_master t
   \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2)\<rbrace>" apply (simp add: setup_reply_master_def) apply (wp set_cap_cte_wp_at' get_cap_wp) apply (auto simp: tcb_cap_valid_def st_tcb_def2 cte_wp_at_caps_of_state is_cap_simps
              dest: tcb_cap_valid_caps_of_stateD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and tcb_at t\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and tcb_at t\<rbrace> do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and tcb_at t) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (if cap = NullCap then \<lambda>s. if (t, tcb_cnode_index 2) = (t, tcb_cnode_index 2) then (is_master_reply_cap (ReplyCap t True {AllowGrant, AllowWrite}) \<and> obj_ref_of (ReplyCap t True {AllowGrant, AllowWrite}) = t) \<and> cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) else cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) else cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2)) s proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma setup_reply_master_nonz_cap[wp]:
  "\<lbrace>ex_nonz_cap_to p\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>" apply (simp add: setup_reply_master_def ex_nonz_cap_to_def cte_wp_at_caps_of_state) apply (wp get_cap_wp) apply (simp add: cte_wp_at_caps_of_state) apply (rule impI, elim exEI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to p\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> zobj_refs cap\<rbrace> do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> zobj_refs cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> zobj_refs cap \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (if cap = NullCap then \<lambda>s. \<exists>a b cap. ((caps_of_state (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>))((t, tcb_cnode_index 2) \<mapsto> ReplyCap t True {AllowGrant, AllowWrite})) (a, b) = Some cap \<and> p \<in> zobj_refs cap else (\<lambda>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> zobj_refs cap)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> zobj_refs cap \<Longrightarrow> caps_of_state s (t, tcb_cnode_index 2) = Some NullCap \<longrightarrow> (\<exists>a b. (a = t \<longrightarrow> b \<noteq> tcb_cnode_index 2) \<and> ((a = t \<longrightarrow> b \<noteq> tcb_cnode_index 2) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> p \<in> zobj_refs cap))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>caps_of_state s (t, tcb_cnode_index 2) = Some NullCap; \<exists>cap. caps_of_state s (x, xa) = Some cap \<and> p \<in> zobj_refs cap\<rbrakk> \<Longrightarrow> (x = t \<longrightarrow> xa \<noteq> tcb_cnode_index 2) \<and> ((x = t \<longrightarrow> xa \<noteq> tcb_cnode_index 2) \<longrightarrow> (\<exists>cap. caps_of_state s (x, xa) = Some cap \<and> p \<in> zobj_refs cap)) proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma restart_invs[wp]:
  "\<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace> restart t \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: restart_def) apply (rule hoare_seq_ext [OF _ gts_sp]) apply (wp sts_invs_minor cancel_ipc_ex_nonz_cap_to_tcb
            hoare_vcg_disj_lift cancel_ipc_simple2
       | simp add: if_apply_def2
       | strengthen invs_valid_objs2)+ apply (auto dest!: idle_no_ex_cap simp: invs_def valid_state_def valid_pspace_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace> restart t \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace> do state <- get_thread_state t;
when (\<not> runnable state \<and> state \<noteq> IdleThreadState) (do y <- cancel_ipc t;
y <- setup_reply_master t;
y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action tcb_sched_enqueue t);
do_extended_op (possible_switch_to t)
od)
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state. \<lbrace>st_tcb_at ((=) state) t and (invs and tcb_at t and ex_nonz_cap_to t)\<rbrace> when (\<not> runnable state \<and> state \<noteq> IdleThreadState) (do y <- cancel_ipc t;
y <- setup_reply_master t;
y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action tcb_sched_enqueue t);
do_extended_op (possible_switch_to t)
od) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state s. st_tcb_at ((=) state) t s \<and> invs s \<and> tcb_at t s \<and> ex_nonz_cap_to t s \<Longrightarrow> \<not> runnable state \<and> state \<noteq> IdleThreadState \<longrightarrow> t \<noteq> idle_thread s proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma restart_typ_at[wp]:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> Tcb_A.restart t \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" by (wpsimp simp: Tcb_A.restart_def wp: cancel_ipc_typ_at)

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

lemma restart_tcb[wp]:
  "\<lbrace>tcb_at t'\<rbrace> Tcb_A.restart t \<lbrace>\<lambda>rv. tcb_at t'\<rbrace>" by (wpsimp simp: tcb_at_typ wp: restart_typ_at)

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

lemma suspend_nonz_cap_to_tcb[wp]:
  "\<lbrace>\<lambda>s. ex_nonz_cap_to t s \<and> tcb_at t s \<and> valid_objs s\<rbrace>
     suspend t'
   \<lbrace>\<lambda>rv s. ex_nonz_cap_to t s\<rbrace>" by (wp cancel_ipc_ex_nonz_cap_to_tcb | simp add: suspend_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ex_nonz_cap_to t s \<and> tcb_at t s \<and> valid_objs s\<rbrace> suspend t' \<lbrace>\<lambda>rv. ex_nonz_cap_to t\<rbrace>
theory Tcb_AI

lemma readreg_invs:
  "\<lbrace>invs and tcb_at src and ex_nonz_cap_to src\<rbrace>
     invoke_tcb (tcb_invocation.ReadRegisters src susp n arch)
   \<lbrace>\<lambda>rv. invs\<rbrace>" by (simp | wp)+
     (clarsimp simp: invs_def valid_state_def valid_pspace_def
              dest!: idle_no_ex_cap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at src and ex_nonz_cap_to src\<rbrace> invoke_tcb (ReadRegisters src susp n arch) \<lbrace>\<lambda>rv. invs\<rbrace>
theory Tcb_AI

lemma (in Tcb_AI_1) copyreg_invs:
  "\<lbrace>(invs::'state_ext::state_ext state \<Rightarrow> bool) and tcb_at src and tcb_at dest and ex_nonz_cap_to dest and
    ex_nonz_cap_to src\<rbrace>
     invoke_tcb (tcb_invocation.CopyRegisters dest src susp resume frames ints arch)
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (wpsimp simp: if_apply_def2
                  wp: mapM_x_wp' suspend_nonz_cap_to_tcb hoare_weak_lift_imp) apply (clarsimp simp: invs_def valid_state_def valid_pspace_def suspend_def
                 dest!: idle_no_ex_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at src and tcb_at dest and ex_nonz_cap_to dest and ex_nonz_cap_to src\<rbrace> invoke_tcb (CopyRegisters dest src susp resume frames ints arch) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; tcb_at src s; tcb_at dest s; ex_nonz_cap_to dest s; ex_nonz_cap_to src s; susp\<rbrakk> \<Longrightarrow> (resume \<longrightarrow> src \<noteq> idle_thread s \<and> valid_objs s) \<and> (\<not> resume \<longrightarrow> src \<noteq> idle_thread s) proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma out_invs_trivialT:
  assumes x: "\<And>tcb v. \<forall>(getF, setF)\<in>ran tcb_cap_cases. getF (fn v tcb) = getF tcb"
  assumes r:  "\<And>tcb v. tcb_arch_ref (fn v tcb) = tcb_arch_ref tcb" (* ARMHYP *)
  assumes z: "\<And>tcb v. tcb_state  (fn v tcb) = tcb_state  tcb"
  assumes z': "\<And>tcb v. tcb_bound_notification (fn v tcb) = tcb_bound_notification tcb"
  assumes z'': "\<And>tcb v. tcb_iarch (fn v tcb) = tcb_iarch tcb"
  assumes w: "\<And>tcb v. tcb_ipc_buffer (fn v tcb) = tcb_ipc_buffer tcb
                          \<or> tcb_ipc_buffer (fn v tcb) = 0"
  assumes y: "\<And>tcb v'. v = Some v' \<Longrightarrow> tcb_fault_handler (fn v' tcb) \<noteq> tcb_fault_handler tcb
                       \<longrightarrow> length (tcb_fault_handler (fn v' tcb)) = word_bits"
  assumes a: "\<And>tcb v. tcb_fault (fn v tcb) \<noteq> tcb_fault tcb
                       \<longrightarrow> (case tcb_fault (fn v tcb) of None \<Rightarrow> True
                                                   | Some f \<Rightarrow> valid_fault f)"
  shows      "\<lbrace>invs\<rbrace> option_update_thread t fn v \<lbrace>\<lambda>rv. invs\<rbrace>" apply (case_tac v, simp_all add: option_update_thread_def) apply (rule thread_set_invs_trivial [OF x z z' z'' w y a r]) apply (auto intro: r) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> option_update_thread t fn v \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. v = Some a \<Longrightarrow> \<lbrace>invs\<rbrace> thread_set (fn a) t \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a tcb. v = Some a \<Longrightarrow> v = Some a proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma out_typ_at:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> option_update_thread t fn v \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" apply (case_tac v, simp_all add: option_update_thread_def) apply (rule thread_set_typ_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> option_update_thread t fn v \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. v = Some a \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> thread_set (fn a) t \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma out_valid_cap:
  "\<lbrace>valid_cap c\<rbrace> option_update_thread t fn v \<lbrace>\<lambda>rv. valid_cap c\<rbrace>" by (wp out_typ_at valid_cap_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap c\<rbrace> option_update_thread t fn v \<lbrace>\<lambda>rv. valid_cap c\<rbrace>
theory Tcb_AI

lemma out_cte_at:
  "\<lbrace>cte_at c\<rbrace> option_update_thread t fn v \<lbrace>\<lambda>rv. cte_at c\<rbrace>" by (wp out_typ_at valid_cte_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) c\<rbrace> option_update_thread t fn v \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>_. True) c\<rbrace>
theory Tcb_AI

lemma out_st_tcb:
  assumes x: "\<And>tcb v. tcb_state  (fn v tcb) = tcb_state  tcb"
  shows      "\<lbrace>st_tcb_at P t\<rbrace> option_update_thread t' fn v \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>" apply (case_tac v, simp_all add: option_update_thread_def) apply (rule thread_set_no_change_tcb_state, rule x) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t\<rbrace> option_update_thread t' fn v \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. v = Some a \<Longrightarrow> \<lbrace>st_tcb_at P t\<rbrace> thread_set (fn a) t' \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma out_emptyable:
  assumes x: "\<And>tcb v. tcb_state  (fn v tcb) = tcb_state  tcb"
  shows      "\<lbrace>emptyable sl\<rbrace> option_update_thread t fn v
              \<lbrace>\<lambda>rv. emptyable sl\<rbrace>" by (wp emptyable_lift out_typ_at out_st_tcb x)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>emptyable sl\<rbrace> option_update_thread t fn v \<lbrace>\<lambda>rv. emptyable sl\<rbrace>
theory Tcb_AI

lemma set_simple_ko_valid_cap:
  "\<lbrace>valid_cap c\<rbrace> set_simple_ko f e ep \<lbrace>\<lambda>_. valid_cap c\<rbrace>" by (wp valid_cap_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap c\<rbrace> set_simple_ko f e ep \<lbrace>\<lambda>_. valid_cap c\<rbrace>
theory Tcb_AI

lemma sts_cte_at[wp]:
  "\<lbrace>\<lambda>s. cte_at p s\<rbrace> set_thread_state t st \<lbrace>\<lambda>_ s. cte_at p s\<rbrace>" by (wp valid_cte_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) p\<rbrace> set_thread_state t st \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) p\<rbrace>
theory Tcb_AI

lemma as_user_cte_at[wp]:
  "\<lbrace>\<lambda>s. cte_at p s\<rbrace> as_user t m \<lbrace>\<lambda>_ s. cte_at p s\<rbrace>" by (wp valid_cte_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) p\<rbrace> as_user t m \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) p\<rbrace>
theory Tcb_AI

lemma cap_insert_cte_at:
  "\<lbrace>cte_at p\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. cte_at p\<rbrace>" by (wp valid_cte_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) p\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) p\<rbrace>
theory Tcb_AI

lemma smrs_cte_at[wp]:
  "\<lbrace>cte_at p\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_. cte_at p\<rbrace>" by (wp valid_cte_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) p\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) p\<rbrace>
theory Tcb_AI

lemma si_cte_at[wp]:
  "\<lbrace>cte_at p\<rbrace> send_ipc bl c ba cg cgr t ep \<lbrace>\<lambda>_. cte_at p\<rbrace>" by (wp valid_cte_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) p\<rbrace> send_ipc bl c ba cg cgr t ep \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) p\<rbrace>
theory Tcb_AI

lemma rai_cte_at[wp]:
  "\<lbrace>cte_at p\<rbrace> receive_signal t cap is_blocking \<lbrace>\<lambda>_. cte_at p\<rbrace>" by (wp valid_cte_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) p\<rbrace> receive_signal t cap is_blocking \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) p\<rbrace>
theory Tcb_AI

lemma hf_cte_at[wp]:
  "\<lbrace>cte_at p\<rbrace> handle_fault t ft \<lbrace>\<lambda>_. cte_at p\<rbrace>" by (wp valid_cte_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) p\<rbrace> handle_fault t ft \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) p\<rbrace>
theory Tcb_AI

lemma cancel_all_ipc_tcb:
  "\<lbrace>tcb_at t\<rbrace> cancel_all_ipc ptr \<lbrace>\<lambda>_. tcb_at t\<rbrace>" by (simp add: tcb_at_typ, wp cancel_all_ipc_typ_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t\<rbrace> cancel_all_ipc ptr \<lbrace>\<lambda>_. tcb_at t\<rbrace>
theory Tcb_AI

lemma thread_set_valid_objs':
  "\<lbrace>valid_objs and (\<lambda>s. \<forall>p t. valid_tcb p t s \<longrightarrow> valid_tcb p (f t) s)\<rbrace>
  thread_set f t
  \<lbrace>\<lambda>rv. valid_objs\<rbrace>" apply (simp add: thread_set_def) apply wp apply clarsimp apply (clarsimp dest!: get_tcb_SomeD simp: obj_at_def) apply (erule (1) pspace_valid_objsE) apply (simp add: valid_obj_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and (\<lambda>s. \<forall>p t. valid_tcb p t s \<longrightarrow> valid_tcb p (f t) s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and (\<lambda>s. \<forall>p t. valid_tcb p t s \<longrightarrow> valid_tcb p (f t) s)\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and (\<lambda>s. \<forall>p t. valid_tcb p t s \<longrightarrow> valid_tcb p (f t) s)) s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (valid_objs and valid_obj t (TCB (f (the (get_tcb t s))))) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_objs s; \<forall>p t. valid_tcb p t s \<longrightarrow> valid_tcb p (f t) s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> valid_obj t (TCB (f y)) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_objs s; \<forall>p t. valid_tcb p t s \<longrightarrow> valid_tcb p (f t) s; kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> valid_obj t (TCB (f y)) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_objs s; \<forall>p t. valid_tcb p t s \<longrightarrow> valid_tcb p (f t) s; kheap s t = Some (TCB y); valid_obj t (TCB y) s\<rbrakk> \<Longrightarrow> valid_obj t (TCB (f y)) s proof (prove)
goal:
No subgoals!