kings-crown/FVELER_Isabelle huggingface dataset:
theory Tcb_AI

lemma (in Tcb_AI) decode_writereg_wf:
  "\<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace>
     decode_write_registers args (cap.ThreadCap t)
   \<lbrace>tcb_inv_wf\<rbrace>,-" apply (simp add: decode_write_registers_def whenE_def
             cong: list.case_cong) apply (rule hoare_pre) apply (wp | wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace> decode_write_registers args (ThreadCap t) \<lbrace>tcb_inv_wf\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace> case args of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # values \<Rightarrow> doE y <- if length values < unat n then throwError TruncatedMessage else returnOk ();
self <- liftE (gets cur_thread);
y <- if t = self then throwError IllegalOperation else returnOk ();
returnOk (WriteRegisters t (flags !! 0) (take (unat n) values) ArchDefaultExtraRegisters)
odE \<lbrace>tcb_inv_wf\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'6\<rbrace> case args of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # values \<Rightarrow> doE y <- if length values < unat n then throwError TruncatedMessage else returnOk ();
self <- liftE (gets cur_thread);
y <- if t = self then throwError IllegalOperation else returnOk ();
returnOk (WriteRegisters t (flags !! 0) (take (unat n) values) ArchDefaultExtraRegisters)
odE \<lbrace>tcb_inv_wf\<rbrace>, -
 2. \<And>s. (invs and tcb_at t and ex_nonz_cap_to t) s \<Longrightarrow> ?P'6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and tcb_at t and ex_nonz_cap_to t) s \<Longrightarrow> (args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (xa = [] \<longrightarrow> True) \<and> (\<forall>xb xc. xa = xb # xc \<longrightarrow> True \<and> True \<and> True \<and> (length xc < unat xb \<longrightarrow> True) \<and> (\<not> length xc < unat xb \<longrightarrow> (t = cur_thread s \<longrightarrow> True) \<and> (t \<noteq> cur_thread s \<longrightarrow> tcb_inv_wf (WriteRegisters t (x !! 0) (take (unat xb) xc) ArchDefaultExtraRegisters) s)))) proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma (in Tcb_AI) decode_set_tls_base_wf:
  "\<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace>
     decode_set_tls_base args (cap.ThreadCap t)
   \<lbrace>tcb_inv_wf\<rbrace>,-" apply (simp add: decode_set_tls_base_def whenE_def
             cong: list.case_cong split del: if_split) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace> decode_set_tls_base args (ThreadCap t) \<lbrace>tcb_inv_wf\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace> doE y <- if args = [] then throwError TruncatedMessage else returnOk ();
returnOk (SetTLSBase t (args ! 0))
odE \<lbrace>tcb_inv_wf\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma OR_choice_E_weak_wp: "\<lbrace>P\<rbrace> f \<sqinter> g \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> OR_choice b f g \<lbrace>Q\<rbrace>,-" apply (simp add: validE_R_def validE_def OR_choice_weak_wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<sqinter> g \<lbrace>Q\<rbrace>, - \<Longrightarrow> \<lbrace>P\<rbrace> OR_choice b f g \<lbrace>Q\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma OR_choiceE_E_weak_wp: "\<lbrace>P\<rbrace> f \<sqinter> g \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> OR_choiceE b f g \<lbrace>Q\<rbrace>,-" apply (simp add: validE_R_def validE_def OR_choiceE_weak_wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<sqinter> g \<lbrace>Q\<rbrace>, - \<Longrightarrow> \<lbrace>P\<rbrace> OR_choiceE b f g \<lbrace>Q\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma thread_get_pred_tcb_at_wp:
  "\<lbrace>\<lambda>s. \<forall>f. pred_tcb_at proj ((=) f) t s \<longrightarrow> P f s \<rbrace> thread_get (proj \<circ> tcb_to_itcb) t \<lbrace>P\<rbrace>" apply (wp thread_get_wp') apply clarsimp apply (drule spec, erule mp) by (simp add: pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>f. pred_tcb_at proj ((=) f) t s \<longrightarrow> P f s\<rbrace> thread_get (proj \<circ> tcb_to_itcb) t \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>f. pred_tcb_at proj ((=) f) t s \<longrightarrow> P f s \<Longrightarrow> \<forall>tcb. ko_at (TCB tcb) t s \<longrightarrow> P ((proj \<circ> tcb_to_itcb) tcb) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>\<forall>f. pred_tcb_at proj ((=) f) t s \<longrightarrow> P f s; ko_at (TCB tcb) t s\<rbrakk> \<Longrightarrow> P (proj (tcb_to_itcb tcb)) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. ko_at (TCB tcb) t s \<Longrightarrow> pred_tcb_at proj ((=) (proj (tcb_to_itcb tcb))) t s
theory Tcb_AI

lemma thread_get_ret:
  "\<lbrace>\<top>\<rbrace> thread_get (proj \<circ> tcb_to_itcb) t \<lbrace>\<lambda>rv. pred_tcb_at proj ((=) rv) t\<rbrace>" apply (simp add: thread_get_def) apply wp by (clarsimp simp: pred_tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> thread_get (proj \<circ> tcb_to_itcb) t \<lbrace>\<lambda>rv. pred_tcb_at proj ((=) rv) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do tcb <- gets_the (get_tcb t);
return (proj (tcb_to_itcb tcb))
od \<lbrace>\<lambda>rv. pred_tcb_at proj ((=) rv) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> pred_tcb_at proj ((=) (proj (tcb_to_itcb (the (get_tcb t s))))) t s
theory Tcb_AI

lemma check_prio_wp:
  "\<lbrace>\<lambda>s. mcpriority_tcb_at (\<lambda>mcp. prio \<le> ucast mcp) auth s \<longrightarrow> Q s\<rbrace> check_prio prio auth \<lbrace>\<lambda>_. Q\<rbrace>, -" apply (clarsimp simp: check_prio_def) apply (wp get_mcpriority_wp whenE_throwError_wp) apply (intro allI impI, elim mp pred_tcb_weakenE) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. mcpriority_tcb_at (\<lambda>mcp. prio \<le> UCAST(8 \<rightarrow> 32) mcp) auth s \<longrightarrow> Q s\<rbrace> check_prio prio auth \<lbrace>\<lambda>_. Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. mcpriority_tcb_at (\<lambda>mcp. prio \<le> UCAST(8 \<rightarrow> 32) mcp) auth s \<longrightarrow> Q s\<rbrace> doE mcp <- liftE (thread_get tcb_mcpriority auth);
whenE (UCAST(8 \<rightarrow> 32) mcp < prio) (throwError (RangeError 0 (UCAST(8 \<rightarrow> 32) mcp)))
odE \<lbrace>\<lambda>_. Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. mcpriority_tcb_at (\<lambda>mcp. prio \<le> UCAST(8 \<rightarrow> 32) mcp) auth s \<longrightarrow> Q s \<Longrightarrow> \<forall>f. mcpriority_tcb_at ((=) f) auth s \<longrightarrow> \<not> UCAST(8 \<rightarrow> 32) f < prio \<longrightarrow> Q s proof (prove)
goal (1 subgoal):
 1. \<And>s f tcb. \<lbrakk>\<not> UCAST(8 \<rightarrow> 32) f < prio; f = itcb_mcpriority tcb\<rbrakk> \<Longrightarrow> prio \<le> UCAST(8 \<rightarrow> 32) (itcb_mcpriority tcb) proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma check_prio_wp_weak:
  "\<lbrace>\<lambda>s. mcpriority_tcb_at (\<lambda>mcp. ucast prio \<le> mcp) auth s \<longrightarrow> Q s\<rbrace> check_prio prio auth \<lbrace>\<lambda>_. Q\<rbrace>, -" apply (wp check_prio_wp) apply (intro allI impI, elim mp pred_tcb_weakenE) apply (simp add: le_ucast_ucast_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. mcpriority_tcb_at ((\<le>) (UCAST(32 \<rightarrow> 8) prio)) auth s \<longrightarrow> Q s\<rbrace> check_prio prio auth \<lbrace>\<lambda>_. Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. mcpriority_tcb_at ((\<le>) (UCAST(32 \<rightarrow> 8) prio)) auth s \<longrightarrow> Q s \<Longrightarrow> mcpriority_tcb_at (\<lambda>mcp. prio \<le> UCAST(8 \<rightarrow> 32) mcp) auth s \<longrightarrow> Q s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. prio \<le> UCAST(8 \<rightarrow> 32) (itcb_mcpriority tcb) \<Longrightarrow> UCAST(32 \<rightarrow> 8) prio \<le> itcb_mcpriority tcb proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma check_prio_lt_ct:
  "\<lbrace>\<top>\<rbrace> check_prio prio auth \<lbrace>\<lambda>rv s. mcpriority_tcb_at (\<lambda>mcp. prio \<le> ucast mcp) auth s\<rbrace>, -" by (wpsimp wp: check_prio_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> check_prio prio auth \<lbrace>\<lambda>rv. mcpriority_tcb_at (\<lambda>mcp. prio \<le> UCAST(8 \<rightarrow> 32) mcp) auth\<rbrace>, -
theory Tcb_AI

lemma check_prio_lt_ct_weak:
  "\<lbrace>\<top>\<rbrace> check_prio prio auth \<lbrace>\<lambda>rv s. mcpriority_tcb_at (\<lambda>mcp. ucast prio \<le> mcp) auth s\<rbrace>, -" by (wpsimp wp: check_prio_wp_weak)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> check_prio prio auth \<lbrace>\<lambda>rv. mcpriority_tcb_at ((\<le>) (UCAST(32 \<rightarrow> 8) prio)) auth\<rbrace>, -
theory Tcb_AI

lemma (in Tcb_AI) decode_set_priority_wf[wp]:
  "\<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace>
        decode_set_priority args (ThreadCap t) slot excs \<lbrace>tcb_inv_wf\<rbrace>, -" by (wpsimp simp: decode_set_priority_def wp: check_prio_wp_weak whenE_throwError_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace> decode_set_priority args (ThreadCap t) slot excs \<lbrace>tcb_inv_wf\<rbrace>, -
theory Tcb_AI

lemma (in Tcb_AI) decode_set_mcpriority_wf[wp]:
  "\<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace>
        decode_set_mcpriority args (ThreadCap t) slot excs \<lbrace>tcb_inv_wf\<rbrace>, -" by (wpsimp simp: decode_set_mcpriority_def wp: check_prio_wp_weak whenE_throwError_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace> decode_set_mcpriority args (ThreadCap t) slot excs \<lbrace>tcb_inv_wf\<rbrace>, -
theory Tcb_AI

lemma (in Tcb_AI) decode_set_sched_params_wf[wp]:
  "\<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace>
        decode_set_sched_params args (ThreadCap t) slot excs \<lbrace>tcb_inv_wf\<rbrace>, -" by (wpsimp simp: decode_set_sched_params_def wp: check_prio_wp_weak whenE_throwError_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace> decode_set_sched_params args (ThreadCap t) slot excs \<lbrace>tcb_inv_wf\<rbrace>, -
theory Tcb_AI

lemma decode_set_priority_is_tc[wp]:
  "\<lbrace>\<top>\<rbrace> decode_set_priority args cap slot excs \<lbrace>\<lambda>rv s. is_ThreadControl rv\<rbrace>,-" by (wpsimp simp: decode_set_priority_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> decode_set_priority args cap slot excs \<lbrace>\<lambda>rv s. is_ThreadControl rv\<rbrace>, -
theory Tcb_AI

lemma decode_set_priority_inv[wp]:
  "\<lbrace>P\<rbrace> decode_set_priority args cap slot excs \<lbrace>\<lambda>rv. P\<rbrace>" by (wpsimp simp: decode_set_priority_def wp: check_prio_inv whenE_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_set_priority args cap slot excs \<lbrace>\<lambda>rv. P\<rbrace>
theory Tcb_AI

lemma decode_set_mcpriority_inv[wp]:
  "\<lbrace>P\<rbrace> decode_set_mcpriority args cap slot excs \<lbrace>\<lambda>rv. P\<rbrace>" by (wpsimp simp: decode_set_mcpriority_def wp: check_prio_inv whenE_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_set_mcpriority args cap slot excs \<lbrace>\<lambda>rv. P\<rbrace>
theory Tcb_AI

lemma decode_set_sched_params_inv[wp]:
  "\<lbrace>P\<rbrace> decode_set_sched_params args cap slot excs \<lbrace>\<lambda>rv. P\<rbrace>" by (wpsimp simp: decode_set_sched_params_def wp: check_prio_inv whenE_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_set_sched_params args cap slot excs \<lbrace>\<lambda>rv. P\<rbrace>
theory Tcb_AI

lemma decode_set_ipc_is_tc[wp]:
  "\<lbrace>\<top>\<rbrace> decode_set_ipc_buffer args cap slot excaps \<lbrace>\<lambda>rv s. is_ThreadControl rv\<rbrace>,-" apply (rule hoare_pre) apply (simp    add: decode_set_ipc_buffer_def split_def
           split del: if_split
            | wp)+ apply fastforce? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> decode_set_ipc_buffer args cap slot excaps \<lbrace>\<lambda>rv s. is_ThreadControl rv\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> decode_set_ipc_buffer args cap slot excaps \<lbrace>\<lambda>rv s. is_ThreadControl rv\<rbrace>, -
 2. \<And>s. True \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma slot_long_running_inv[wp]:
  "\<lbrace>P\<rbrace> slot_cap_long_running_delete ptr \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: slot_cap_long_running_delete_def) apply (wp | wpcw | simp add: is_final_cap_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> slot_cap_long_running_delete ptr \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do cap <- get_cap ptr;
case cap of NullCap \<Rightarrow> return False | _ \<Rightarrow> do final <- is_final_cap cap;
return (final \<and> long_running_delete cap)
od
od \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma val_le_length_Cons:
  "n \<noteq> 0 \<Longrightarrow> (n \<le> length xs) = (\<exists>y ys. xs = y # ys \<and> (n - 1) \<le> length ys)" apply (cases xs, simp_all) apply (cases n, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> (n \<le> length xs) = (\<exists>y ys. xs = y # ys \<and> n - 1 \<le> length ys) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>0 < n; xs = a # list\<rbrakk> \<Longrightarrow> (n \<le> Suc (length list)) = (n - Suc 0 \<le> length list) proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma decode_set_space_inv[wp]:
  "\<lbrace>P\<rbrace> decode_set_space args cap slot extras \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp   add: decode_set_space_def whenE_def unlessE_def
          split del: if_split) apply (rule hoare_pre) apply (wp hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_set_space args cap slot extras \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE y <- if length args < 3 \<or> length extras < 2 then throwError TruncatedMessage else returnOk ();
can_chg_cr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_ctable_ptr (obj_ref_of cap))));
can_chg_vr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_vtable_ptr (obj_ref_of cap))));
y <- if can_chg_cr \<and> can_chg_vr then returnOk () else throwError IllegalOperation;
croot_cap' <- derive_cap (snd (extras ! 0)) ((if args ! Suc 0 = 0 then id else update_cap_data False (args ! Suc 0)) (fst (extras ! 0)));
y <- if is_cnode_cap croot_cap' then returnOk () else throwError IllegalOperation;
vroot_cap' <- derive_cap (snd (extras ! Suc 0)) ((if args ! 2 = 0 then id else update_cap_data False (args ! 2)) (fst (extras ! Suc 0)));
y <- if is_valid_vtable_root vroot_cap' then returnOk () else throwError IllegalOperation;
returnOk (ThreadControl (obj_ref_of cap) slot (Some (to_bl (args ! 0))) None None (Some (croot_cap', snd (extras ! 0))) (Some (vroot_cap', snd (extras ! Suc 0))) None)
odE \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> doE y <- if length args < 3 \<or> length extras < 2 then throwError TruncatedMessage else returnOk ();
can_chg_cr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_ctable_ptr (obj_ref_of cap))));
can_chg_vr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_vtable_ptr (obj_ref_of cap))));
y <- if can_chg_cr \<and> can_chg_vr then returnOk () else throwError IllegalOperation;
croot_cap' <- derive_cap (snd (extras ! 0)) ((if args ! Suc 0 = 0 then id else update_cap_data False (args ! Suc 0)) (fst (extras ! 0)));
y <- if is_cnode_cap croot_cap' then returnOk () else throwError IllegalOperation;
vroot_cap' <- derive_cap (snd (extras ! Suc 0)) ((if args ! 2 = 0 then id else update_cap_data False (args ! 2)) (fst (extras ! Suc 0)));
y <- if is_valid_vtable_root vroot_cap' then returnOk () else throwError IllegalOperation;
returnOk (ThreadControl (obj_ref_of cap) slot (Some (to_bl (args ! 0))) None None (Some (croot_cap', snd (extras ! 0))) (Some (vroot_cap', snd (extras ! Suc 0))) None)
odE \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q1 s proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma decode_set_space_is_tc[wp]:
  "\<lbrace>\<top>\<rbrace> decode_set_space args cap slot extras \<lbrace>\<lambda>rv s. is_ThreadControl rv\<rbrace>,-" apply (rule hoare_pre) apply (simp   add: decode_set_space_def whenE_def unlessE_def
           split del: if_split) apply (wp | simp only: tcb_invocation.disc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> decode_set_space args cap slot extras \<lbrace>\<lambda>rv s. is_ThreadControl rv\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> decode_set_space args cap slot extras \<lbrace>\<lambda>rv s. is_ThreadControl rv\<rbrace>, -
 2. \<And>s. True \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE y <- if length args < 3 \<or> length extras < 2 then throwError TruncatedMessage else returnOk ();
can_chg_cr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_ctable_ptr (obj_ref_of cap))));
can_chg_vr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_vtable_ptr (obj_ref_of cap))));
y <- if can_chg_cr \<and> can_chg_vr then returnOk () else throwError IllegalOperation;
croot_cap' <- derive_cap (snd (extras ! 0)) ((if args ! Suc 0 = 0 then id else update_cap_data False (args ! Suc 0)) (fst (extras ! 0)));
y <- if is_cnode_cap croot_cap' then returnOk () else throwError IllegalOperation;
vroot_cap' <- derive_cap (snd (extras ! Suc 0)) ((if args ! 2 = 0 then id else update_cap_data False (args ! 2)) (fst (extras ! Suc 0)));
y <- if is_valid_vtable_root vroot_cap' then returnOk () else throwError IllegalOperation;
returnOk (ThreadControl (obj_ref_of cap) slot (Some (to_bl (args ! 0))) None None (Some (croot_cap', snd (extras ! 0))) (Some (vroot_cap', snd (extras ! Suc 0))) None)
odE \<lbrace>\<lambda>rv s. is_ThreadControl rv\<rbrace>, -
 2. \<And>s. True \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma decode_set_mcpriority_is_tc[wp]:
  "\<lbrace>\<top>\<rbrace> decode_set_mcpriority args cap slot excs \<lbrace>\<lambda>rv s. is_ThreadControl rv\<rbrace>,-" by (wpsimp simp: decode_set_mcpriority_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> decode_set_mcpriority args cap slot excs \<lbrace>\<lambda>rv s. is_ThreadControl rv\<rbrace>, -
theory Tcb_AI

lemma decode_set_space_target[wp]:
  "\<lbrace>\<lambda>s. P (obj_ref_of cap)\<rbrace>
   decode_set_space args cap slot extras
   \<lbrace>\<lambda>rv s. P (tc_target rv)\<rbrace>,-" unfolding decode_set_space_def by (wpsimp split_del: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_ref_of cap)\<rbrace> decode_set_space args cap slot extras \<lbrace>\<lambda>rv s. P (tc_target rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_ref_of cap)\<rbrace> doE whenE (length args < 3 \<or> length extras < 2) $ throwError TruncatedMessage;
fault_ep <- returnOk $ args ! 0;
croot_data <- returnOk $ args ! 1;
vroot_data <- returnOk $ args ! 2;
croot_arg <- returnOk $ extras ! 0;
vroot_arg <- returnOk $ extras ! 1;
can_chg_cr <- liftE $ liftM Not $ slot_cap_long_running_delete $ get_tcb_ctable_ptr $ obj_ref_of cap;
can_chg_vr <- liftE $ liftM Not $ slot_cap_long_running_delete $ get_tcb_vtable_ptr $ obj_ref_of cap;
unlessE (can_chg_cr \<and> can_chg_vr) $ throwError IllegalOperation;
croot_cap <- returnOk $ fst croot_arg;
croot_slot <- returnOk $ snd croot_arg;
croot_cap' <- derive_cap croot_slot $ (if croot_data = 0 then id else update_cap_data False croot_data) croot_cap;
unlessE (is_cnode_cap croot_cap') $ throwError IllegalOperation;
croot <- returnOk (croot_cap', croot_slot);
vroot_cap <- returnOk $ fst vroot_arg;
vroot_slot <- returnOk $ snd vroot_arg;
vroot_cap' <- derive_cap vroot_slot $ (if vroot_data = 0 then id else update_cap_data False vroot_data) vroot_cap;
unlessE (is_valid_vtable_root vroot_cap') $ throwError IllegalOperation;
vroot <- returnOk (vroot_cap', vroot_slot);
returnOk $ ThreadControl (obj_ref_of cap) slot (Some (to_bl fault_ep)) None None (Some croot) (Some vroot) None
odE \<lbrace>\<lambda>rv s. P (tc_target rv)\<rbrace>, -
theory Tcb_AI

lemma boring_simp[simp]:
  "(if x then True else False) = x" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if x then True else False) = x
theory Tcb_AI

lemma (in Tcb_AI) decode_tcb_conf_inv[wp]:
  "\<lbrace>P::'state_ext state \<Rightarrow> bool\<rbrace> decode_tcb_configure args cap slot extras \<lbrace>\<lambda>rv. P\<rbrace>" apply (clarsimp simp add: decode_tcb_configure_def Let_def whenE_def
                 split del: if_split) apply (rule hoare_pre, wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_tcb_configure args cap slot extras \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE y <- if length args < 4 then throwError TruncatedMessage else returnOk ();
y <- if length extras < 3 then throwError TruncatedMessage else returnOk ();
set_params <- decode_set_ipc_buffer [args ! 3] cap slot [extras ! 2];
set_space <- decode_set_space [args ! 0, args ! Suc 0, args ! 2] cap slot (take 2 extras);
returnOk (ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))
odE \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (length args < 4 \<longrightarrow> P s \<and> True) \<and> (\<not> length args < 4 \<longrightarrow> (length extras < 3 \<longrightarrow> P s \<and> True) \<and> (\<not> length extras < 3 \<longrightarrow> P s \<and> P s \<and> P s)) proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma decode_bind_notification_inv[wp]:
  "\<lbrace>P\<rbrace> decode_bind_notification cap excaps \<lbrace>\<lambda>_. P\<rbrace>" unfolding decode_bind_notification_def by (wpsimp wp: get_simple_ko_wp gbn_wp
             simp: whenE_def if_apply_def2
             split_del: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_bind_notification cap excaps \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> case cap of ThreadCap tcb \<Rightarrow> doE whenE (length excaps = 0) $ throwError TruncatedMessage;
nTFN <- liftE $ get_bound_notification tcb;
case nTFN of None \<Rightarrow> returnOk () | Some x \<Rightarrow> throwError IllegalOperation;
(ntfnptr, rights) <- case fst (hd excaps) of NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError IllegalOperation;
whenE (AllowRecv \<notin> rights) $ throwError IllegalOperation;
ntfn <- liftE $ get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (WaitingNtfn list, b) \<Rightarrow> throwError IllegalOperation | (_, None) \<Rightarrow> returnOk () | (_, Some a) \<Rightarrow> throwError IllegalOperation;
returnOk $ NotificationControl tcb (Some ntfnptr)
odE | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>_. P\<rbrace>