kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_AI

lemma sts_Restart_invs[wp]:
  "\<lbrace>st_tcb_at active t and invs and ex_nonz_cap_to t\<rbrace>
     set_thread_state t Structures_A.Restart
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (wp sts_invs_minor2) apply (auto elim!: pred_tcb_weakenE
           notE [rotated, OF _ idle_no_ex_cap]
           simp: invs_def valid_state_def valid_pspace_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at active t and invs and ex_nonz_cap_to t\<rbrace> set_thread_state t Restart \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (st_tcb_at active t and invs and ex_nonz_cap_to t) s \<Longrightarrow> (st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of Restart \<and> st' \<noteq> BlockedOnReply) t and invs and ex_nonz_cap_to t and (\<lambda>s. t \<noteq> idle_thread s) and K (Restart \<noteq> BlockedOnReply \<and> Restart \<noteq> IdleThreadState) and (\<lambda>s. \<forall>a data. Restart = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s) and (\<lambda>s. st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted Restart \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s)) s proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma invoke_tcb_tcb[wp]:
  "\<lbrace>tcb_at tptr\<rbrace> invoke_tcb i \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>" by (simp add: tcb_at_typ invoke_tcb_typ_at [where P=id, simplified])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at tptr\<rbrace> invoke_tcb i \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>
theory Syscall_AI

lemma invoke_domain_tcb[wp]:
  "\<lbrace>tcb_at tptr\<rbrace> invoke_domain thread domain \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>" by (simp add: tcb_at_typ invoke_domain_typ_at [where P=id, simplified])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at tptr\<rbrace> invoke_domain thread domain \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>
theory Syscall_AI

lemma simple_from_active:
  "st_tcb_at active t s \<Longrightarrow> st_tcb_at simple t s" by (fastforce elim!: pred_tcb_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at active t s \<Longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t s
theory Syscall_AI

lemma simple_from_running:
  "ct_running s \<Longrightarrow> st_tcb_at simple (cur_thread s) s" by (fastforce simp: ct_in_state_def
               elim!: pred_tcb_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_running s \<Longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) (cur_thread s) s
theory Syscall_AI

lemma st_tcb_at_eq:
  "\<lbrakk> st_tcb_at (\<lambda>s. s = st) t s; st_tcb_at (\<lambda>s. s = st') t s \<rbrakk> \<Longrightarrow> st = st'" by (clarsimp simp add: pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at (\<lambda>s. s = st) t s; st_tcb_at (\<lambda>s. s = st') t s\<rbrakk> \<Longrightarrow> st = st'
theory Syscall_AI

lemma do_ipc_transfer_tcb_at [wp]:
  "\<lbrace>\<lambda>s. P (tcb_at t s)\<rbrace> do_ipc_transfer s ep bg grt r \<lbrace>\<lambda>rv s. P (tcb_at t s)\<rbrace>" by (simp add: tcb_at_typ) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (tcb_at t s)\<rbrace> do_ipc_transfer s ep bg grt r \<lbrace>\<lambda>rv s. P (tcb_at t s)\<rbrace>
theory Syscall_AI

lemma do_ipc_transfer_emptyable[wp]:
  "\<lbrace>emptyable sl\<rbrace> do_ipc_transfer sender ep badge grant receiver \<lbrace>\<lambda>_. emptyable sl\<rbrace>" apply (clarsimp simp add: emptyable_def) apply (wp hoare_convert_imp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>emptyable sl\<rbrace> do_ipc_transfer sender ep badge grant receiver \<lbrace>\<lambda>_. emptyable sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at (fst sl) s \<and> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s\<rbrace> do_ipc_transfer sender ep badge grant receiver \<lbrace>\<lambda>_ s. tcb_at (fst sl) s \<and> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma thread_set_has_no_reply_cap:
  "(\<And>tcb. \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (f tcb) = getF tcb)
  \<Longrightarrow> \<lbrace>\<lambda>s. \<not>has_reply_cap tt s\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. \<not>has_reply_cap tt s\<rbrace>" apply (clarsimp simp add: has_reply_cap_def) apply (wpsimp wp: hoare_vcg_all_lift thread_set_cte_wp_at_trivial
    | fast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (f tcb) = getF tcb) \<Longrightarrow> \<lbrace>\<lambda>s. \<not> has_reply_cap tt s\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. \<not> has_reply_cap tt s\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. \<forall>x\<in>ran tcb_cap_cases. case x of (getF, v) \<Rightarrow> getF (f tcb) = getF tcb) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>a b. \<not> cte_wp_at (is_reply_cap_to tt) (a, b) s\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. \<forall>a b. \<not> cte_wp_at (is_reply_cap_to tt) (a, b) s\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma (in Systemcall_AI_Pre) handle_fault_reply_has_no_reply_cap:
  "\<lbrace>\<lambda>s :: 'state_ext state. \<not>has_reply_cap t s\<rbrace> handle_fault_reply f t d dl \<lbrace>\<lambda>_ s. \<not>has_reply_cap t s\<rbrace>" apply (clarsimp simp add: has_reply_cap_def) apply (wpsimp wp: hoare_vcg_all_lift handle_fault_reply_cte_wp_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> has_reply_cap t s\<rbrace> handle_fault_reply f t d dl \<lbrace>\<lambda>_ s. \<not> has_reply_cap t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>a b. \<not> cte_wp_at (is_reply_cap_to t) (a, b) s\<rbrace> handle_fault_reply f t d dl \<lbrace>\<lambda>_ s. \<forall>a b. \<not> cte_wp_at (is_reply_cap_to t) (a, b) s\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma (in Systemcall_AI_Pre2) pinv_invs[wp]:
  "\<lbrace>invs and ct_active and valid_invocation i\<rbrace>
    perform_invocation blocking call i \<lbrace>\<lambda>rv. invs :: 'state_ext state \<Rightarrow> _\<rbrace>" apply (case_tac i, simp_all) apply (wp tcbinv_invs send_signal_interrupt_states invoke_domain_invs
         | clarsimp simp:ct_in_state_def is_reply_cap_to_def
         | erule st_tcb_ex_cap
         | fastforce simp:ct_in_state_def is_reply_cap_to_def | rule conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active and valid_invocation i\<rbrace> perform_invocation blocking call i \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>x1. i = InvokeUntyped x1 \<Longrightarrow> \<lbrace>invs and ct_active and valid_untyped_inv x1\<rbrace> doE y <- invoke_untyped x1;
returnOk []
odE \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x21 x22 x23 x24. i = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> \<lbrace>invs and ct_active and (ep_at x21 and ex_nonz_cap_to x21)\<rbrace> liftE (do thread <- gets cur_thread;
y <- send_ipc blocking call x22 x23 x24 thread x21;
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x31 x32. i = InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>invs and ct_active and (ntfn_at x31 and ex_nonz_cap_to x31)\<rbrace> doE y <- liftE (send_signal x31 x32);
returnOk []
odE \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x41 x42 x43. i = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>invs and ct_active and (tcb_at x41 and cte_wp_at (\<lambda>cap. \<exists>R. cap = ReplyCap x41 False R) x42)\<rbrace> liftE (do sender <- gets cur_thread;
y <- do_reply_transfer sender x41 x42 x43;
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x5. i = InvokeTCB x5 \<Longrightarrow> \<lbrace>invs and ct_active and tcb_inv_wf x5\<rbrace> invoke_tcb x5 \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x61 x62. i = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>invs and ct_active and (tcb_at x61 and (\<lambda>s. x61 \<noteq> idle_thread s))\<rbrace> invoke_domain x61 x62 \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x7. i = InvokeCNode x7 \<Longrightarrow> \<lbrace>invs and ct_active and valid_cnode_inv x7\<rbrace> doE y <- invoke_cnode x7;
returnOk []
odE \<lbrace>\<lambda>rv. invs\<rbrace>
 8. \<And>x8. i = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>invs and ct_active and irq_control_inv_valid x8\<rbrace> doE y <- invoke_irq_control x8;
returnOk []
odE \<lbrace>\<lambda>rv. invs\<rbrace>
 9. \<And>x9. i = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>invs and ct_active and irq_handler_inv_valid x9\<rbrace> doE y <- liftE (invoke_irq_handler x9);
returnOk []
odE \<lbrace>\<lambda>rv. invs\<rbrace>
 10. \<And>x10. i = InvokeArchObject x10 \<Longrightarrow> \<lbrace>invs and ct_active and valid_arch_inv x10\<rbrace> arch_perform_invocation x10 \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma pinv_tcb[wp]:
  "\<And>tptr blocking call i.
    \<lbrace>invs and st_tcb_at active tptr and ct_active and valid_invocation i\<rbrace>
      perform_invocation blocking call i
    \<lbrace>\<lambda>rv. tcb_at tptr :: 'state_ext state \<Rightarrow> bool\<rbrace>" apply (case_tac i, simp_all split:option.splits,
    (wp invoke_arch_tcb
              | simp | clarsimp elim!: st_tcb_at_tcb_at
              | wp (once) tcb_at_typ_at)+
    ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>tptr blocking call i. \<lbrace>invs and st_tcb_at active tptr and ct_active and valid_invocation i\<rbrace> perform_invocation blocking call i \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma cte_wp_cdt_lift:
  assumes c: "\<And>P. \<lbrace>cte_wp_at P p\<rbrace> f \<lbrace>\<lambda>r. cte_wp_at P p\<rbrace>"
  assumes m: "\<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> f \<lbrace>\<lambda>r s. P (cdt s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. cte_wp_at (P (cdt s)) p s\<rbrace> f \<lbrace>\<lambda>r s. cte_wp_at (P (cdt s)) p s\<rbrace>" apply (clarsimp simp add: valid_def) apply (frule_tac P1="(=) (cdt s)" in use_valid [OF _  m], rule refl) apply simp apply (erule use_valid [OF _ c]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (P (cdt s)) p s\<rbrace> f \<lbrace>\<lambda>r s. cte_wp_at (P (cdt s)) p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>cte_wp_at (P (cdt s)) p s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> cte_wp_at (P (cdt b)) p b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>cte_wp_at (P (cdt s)) p s; (a, b) \<in> fst (f s); cdt s = cdt b\<rbrakk> \<Longrightarrow> cte_wp_at (P (cdt b)) p b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>cte_wp_at (P (cdt b)) p s; (a, b) \<in> fst (f s); cdt s = cdt b\<rbrakk> \<Longrightarrow> cte_wp_at (P (cdt b)) p b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>cte_wp_at (P (cdt b)) p s; cdt s = cdt b\<rbrakk> \<Longrightarrow> cte_wp_at (P (cdt b)) p s proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma sts_cte_wp_cdt [wp]:
  "\<lbrace>\<lambda>s. cte_wp_at (P (cdt s)) p s\<rbrace>
  set_thread_state t st
  \<lbrace>\<lambda>rv s. cte_wp_at (P (cdt s)) p s\<rbrace>" by (rule cte_wp_cdt_lift; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (P (cdt s)) p s\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. cte_wp_at (P (cdt s)) p s\<rbrace>
theory Syscall_AI

lemma sts_nasty_bit:
  shows
  "\<lbrace>\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. ptr' \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s
              \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap\<rbrace>
     set_thread_state t st
   \<lbrace>\<lambda>rv s. \<forall>r\<in>obj_refs cap. \<forall>a b. ptr' \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s
              \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap\<rbrace>" apply (intro hoare_vcg_const_Ball_lift hoare_vcg_all_lift) apply (wpsimp wp: hoare_vcg_const_Ball_lift hoare_vcg_all_lift
            hoare_vcg_imp_lift hoare_vcg_disj_lift valid_cte_at_neg_typ
          | simp add: cte_wp_at_neg2[where P="\<lambda>c. x \<in> obj_refs c" for x])+ apply (clarsimp simp: o_def cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. ptr' \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. \<forall>r\<in>obj_refs cap. \<forall>a b. ptr' \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>r a b. r \<in> obj_refs cap \<Longrightarrow> \<lbrace>\<lambda>s. ptr' \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. ptr' \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>r a b s. \<lbrakk>r \<in> obj_refs cap; cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap; cte_wp_at (\<lambda>_. True) (a, b) s; ptr' \<noteq> (a, b); cte_wp_at (\<lambda>a. \<not> is_zombie a) (a, b) s \<longrightarrow> is_zombie cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>a. r \<notin> obj_refs a) (a, b) s proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma sts_no_cap_asid[wp]:
  "\<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace>
     set_thread_state t st
   \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace>" by (simp add: no_cap_to_obj_with_diff_ref_def
                cte_wp_at_caps_of_state, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace>
theory Syscall_AI

lemma sts_mcpriority_tcb_at[wp]:
  "\<lbrace>mcpriority_tcb_at P t\<rbrace> set_thread_state p ts \<lbrace>\<lambda>rv. mcpriority_tcb_at P t\<rbrace>" apply (simp add: set_thread_state_def set_object_def get_object_def) apply (wp | simp)+ apply (clarsimp simp: pred_tcb_at_def obj_at_def) apply (drule get_tcb_SomeD) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>mcpriority_tcb_at P t\<rbrace> set_thread_state p ts \<lbrace>\<lambda>rv. mcpriority_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>mcpriority_tcb_at P t\<rbrace> do tcb <- gets_the (get_tcb p);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>)
od;
do_extended_op (set_thread_state_ext p)
od \<lbrace>\<lambda>rv. mcpriority_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. mcpriority_tcb_at P t s \<Longrightarrow> (\<exists>y. get_tcb p s = Some y) \<longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> a_type (the (kheap s p)) = ATCB \<longrightarrow> mcpriority_tcb_at P t (s\<lparr>kheap := \<lambda>a. if a = p then Some (TCB (the (get_tcb p s)\<lparr>tcb_state := ts\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcba. \<lbrakk>P (tcb_mcpriority tcba); t = p; get_tcb p s = Some y; kheap s p = Some (TCB tcba)\<rbrakk> \<Longrightarrow> P (tcb_mcpriority y) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcba. \<lbrakk>P (tcb_mcpriority tcba); t = p; kheap s p = Some (TCB tcba); kheap s p = Some (TCB y)\<rbrakk> \<Longrightarrow> P (tcb_mcpriority y) proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma sts_mcpriority_tcb_at_ct[wp]:
  "\<lbrace>\<lambda>s. mcpriority_tcb_at P (cur_thread s) s\<rbrace> set_thread_state p ts \<lbrace>\<lambda>rv s. mcpriority_tcb_at P (cur_thread s) s\<rbrace>" apply (simp add: set_thread_state_def set_object_def get_object_def) apply (wp | simp)+ apply (clarsimp simp: pred_tcb_at_def obj_at_def) apply (drule get_tcb_SomeD) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. mcpriority_tcb_at P (cur_thread s) s\<rbrace> set_thread_state p ts \<lbrace>\<lambda>rv s. mcpriority_tcb_at P (cur_thread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. mcpriority_tcb_at P (cur_thread s) s\<rbrace> do tcb <- gets_the (get_tcb p);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>)
od;
do_extended_op (set_thread_state_ext p)
od \<lbrace>\<lambda>rv s. mcpriority_tcb_at P (cur_thread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. mcpriority_tcb_at P (cur_thread s) s \<Longrightarrow> (\<exists>y. get_tcb p s = Some y) \<longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> a_type (the (kheap s p)) = ATCB \<longrightarrow> mcpriority_tcb_at P (cur_thread s) (s\<lparr>kheap := \<lambda>a. if a = p then Some (TCB (the (get_tcb p s)\<lparr>tcb_state := ts\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcba. \<lbrakk>P (tcb_mcpriority tcba); p = cur_thread s; get_tcb (cur_thread s) s = Some y; kheap s (cur_thread s) = Some (TCB tcba)\<rbrakk> \<Longrightarrow> P (tcb_mcpriority y) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcba. \<lbrakk>P (tcb_mcpriority tcba); p = cur_thread s; kheap s (cur_thread s) = Some (TCB tcba); kheap s (cur_thread s) = Some (TCB y)\<rbrakk> \<Longrightarrow> P (tcb_mcpriority y) proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma sts_tcb_inv_wf [wp]:
  "\<lbrace>tcb_inv_wf i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. tcb_inv_wf i\<rbrace>" apply (case_tac i) by (wp set_thread_state_valid_cap hoare_vcg_all_lift hoare_vcg_const_imp_lift
         | simp add: tcb_at_typ split: option.split
         | safe
         | wp sts_obj_at_impossible)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_inv_wf i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. tcb_inv_wf i\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14. i = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> \<lbrace>tcb_inv_wf i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. tcb_inv_wf i\<rbrace>
 2. \<And>x21 x22 x23 x24. i = ReadRegisters x21 x22 x23 x24 \<Longrightarrow> \<lbrace>tcb_inv_wf i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. tcb_inv_wf i\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37. i = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> \<lbrace>tcb_inv_wf i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. tcb_inv_wf i\<rbrace>
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48. i = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>tcb_inv_wf i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. tcb_inv_wf i\<rbrace>
 5. \<And>x5. i = Suspend x5 \<Longrightarrow> \<lbrace>tcb_inv_wf i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. tcb_inv_wf i\<rbrace>
 6. \<And>x6. i = Resume x6 \<Longrightarrow> \<lbrace>tcb_inv_wf i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. tcb_inv_wf i\<rbrace>
 7. \<And>x71 x72. i = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>tcb_inv_wf i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. tcb_inv_wf i\<rbrace>
 8. \<And>x81 x82. i = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>tcb_inv_wf i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. tcb_inv_wf i\<rbrace>
theory Syscall_AI

lemma sts_valid_inv[wp]:
  "\<lbrace>valid_invocation i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_invocation i\<rbrace>" by (cases i; wpsimp simp: sts_valid_untyped_inv sts_valid_arch_inv;
      rename_tac i'; case_tac i'; simp;
      wpsimp wp: set_thread_state_valid_cap sts_nasty_bit
                 sts_nasty_bit[where ptr'="(p_a, p_b)" for p_a p_b, simplified]
                 hoare_vcg_const_imp_lift hoare_vcg_ex_lift;
      auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_invocation i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_invocation i\<rbrace>
theory Syscall_AI

lemma sts_Restart_stay_simple:
  "\<lbrace>st_tcb_at simple t\<rbrace>
     set_thread_state t' Structures_A.Restart
   \<lbrace>\<lambda>rv. st_tcb_at simple t\<rbrace>" apply (rule hoare_pre) apply (wp sts_st_tcb_at_cases) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> set_thread_state t' Restart \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_thread_state t' Restart \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace>
 2. \<And>s. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t s \<Longrightarrow> (t' = t \<longrightarrow> inactive Restart \<or> Restart = Running \<or> Restart = Restart \<or> idle Restart \<or> awaiting_reply Restart) \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t s) proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma decode_inv_inv[wp]:
  notes if_split [split del]
  shows
  "\<lbrace>P\<rbrace> decode_invocation label args cap_index slot cap excaps \<lbrace>\<lambda>rv. P\<rbrace>" apply (case_tac cap, simp_all add: decode_invocation_def,
    (wpsimp wp: decode_tcb_inv_inv decode_domain_inv_inv)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_invocation label args cap_index slot cap excaps \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma cnode_eq_strg:
  "(\<exists>ptr. cte_wp_at ((=) cap) ptr s)
    \<longrightarrow> (is_cnode_cap cap \<longrightarrow> (\<forall>ref \<in> cte_refs cap (interrupt_irq_node s).
                                    ex_cte_cap_wp_to is_cnode_cap ref s))" apply (clarsimp simp: ex_cte_cap_wp_to_def) by (intro exI, erule cte_wp_at_weakenE, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>ptr. cte_wp_at ((=) cap) ptr s) \<longrightarrow> is_cnode_cap cap \<longrightarrow> (\<forall>ref\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap ref s) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at ((=) cap) (a, b) s; is_cnode_cap cap; (aa, ba) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>c. is_cnode_cap c \<and> (aa, ba) \<in> cte_refs c (interrupt_irq_node s)) (a, b) s