kings-crown/FVELER_Isabelle huggingface dataset:
theory Tcb_AI

lemma out_valid_objs:
  "\<lbrace>valid_objs and K (\<forall>p (s::'z::state_ext state) t x. valid_tcb p t s \<longrightarrow> valid_tcb p (f x t) s)\<rbrace>
  (option_update_thread a f t :: (unit,'z) s_monad)
  \<lbrace>\<lambda>rv. valid_objs\<rbrace>" apply (cases t) apply (simp add: option_update_thread_def) apply wp apply simp apply (simp add: option_update_thread_def) apply (wp thread_set_valid_objs) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and K (\<forall>p s t x. valid_tcb p t s \<longrightarrow> valid_tcb p (f x t) s)\<rbrace> option_update_thread a f t \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. t = None \<Longrightarrow> \<lbrace>valid_objs and K (\<forall>p s t x. valid_tcb p t s \<longrightarrow> valid_tcb p (f x t) s)\<rbrace> option_update_thread a f t \<lbrace>\<lambda>rv. valid_objs\<rbrace>
 2. \<And>aa. t = Some aa \<Longrightarrow> \<lbrace>valid_objs and K (\<forall>p s t x. valid_tcb p t s \<longrightarrow> valid_tcb p (f x t) s)\<rbrace> option_update_thread a f t \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. t = None \<Longrightarrow> \<lbrace>valid_objs and (\<lambda>y. \<forall>p s t. valid_tcb p t s \<longrightarrow> (\<forall>x. valid_tcb p (f x t) s))\<rbrace> return () \<lbrace>\<lambda>rv. valid_objs\<rbrace>
 2. \<And>aa. t = Some aa \<Longrightarrow> \<lbrace>valid_objs and K (\<forall>p s t x. valid_tcb p t s \<longrightarrow> valid_tcb p (f x t) s)\<rbrace> option_update_thread a f t \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>t = None; (valid_objs and (\<lambda>y. \<forall>p s t. valid_tcb p t s \<longrightarrow> (\<forall>x. valid_tcb p (f x t) s))) s\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>aa. t = Some aa \<Longrightarrow> \<lbrace>valid_objs and K (\<forall>p s t x. valid_tcb p t s \<longrightarrow> valid_tcb p (f x t) s)\<rbrace> option_update_thread a f t \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>aa. t = Some aa \<Longrightarrow> \<lbrace>valid_objs and K (\<forall>p s t x. valid_tcb p t s \<longrightarrow> valid_tcb p (f x t) s)\<rbrace> option_update_thread a f t \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>aa. t = Some aa \<Longrightarrow> \<lbrace>valid_objs and (\<lambda>y. \<forall>p s t. valid_tcb p t s \<longrightarrow> (\<forall>x. valid_tcb p (f x t) s))\<rbrace> thread_set (f aa) a \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a s. \<lbrakk>t = Some a; (valid_objs and (\<lambda>y. \<forall>p s t. valid_tcb p t s \<longrightarrow> (\<forall>x. valid_tcb p (f x t) s))) s\<rbrakk> \<Longrightarrow> (valid_objs and K (\<forall>p s t. valid_tcb p t s \<longrightarrow> valid_tcb p (f a t) s)) s proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma out_cte_wp_at_trivialT:
  "(\<And>tcb v. \<forall>(getF, x)\<in>ran tcb_cap_cases. getF (f v tcb) = getF tcb)
   \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace>
  option_update_thread a f t
  \<lbrace>\<lambda>rv s. P (cte_wp_at P' p s)\<rbrace>" apply (simp add: option_update_thread_def cte_wp_at_caps_of_state) apply (rule hoare_pre) apply (wp thread_set_caps_of_state_trivial | simp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb v. \<forall>(getF, x)\<in>ran tcb_cap_cases. getF (f v tcb) = getF tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> option_update_thread a f t \<lbrace>\<lambda>rv s. P (cte_wp_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb v. \<forall>x\<in>ran tcb_cap_cases. case x of (getF, x) \<Rightarrow> getF (f v tcb) = getF tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (\<exists>cap. caps_of_state s p = Some cap \<and> P' cap)\<rbrace> case t of None \<Rightarrow> return () | Some v \<Rightarrow> thread_set (f v) a \<lbrace>\<lambda>rv s. P (\<exists>cap. caps_of_state s p = Some cap \<and> P' cap)\<rbrace> proof (prove)
goal (2 subgoals):
 1. (\<And>tcb v. \<forall>x\<in>ran tcb_cap_cases. case x of (getF, x) \<Rightarrow> getF (f v tcb) = getF tcb) \<Longrightarrow> \<lbrace>?Q4\<rbrace> case t of None \<Rightarrow> return () | Some v \<Rightarrow> thread_set (f v) a \<lbrace>\<lambda>rv s. P (\<exists>cap. caps_of_state s p = Some cap \<and> P' cap)\<rbrace>
 2. \<And>s. \<lbrakk>\<And>tcb v. \<forall>x\<in>ran tcb_cap_cases. case x of (getF, x) \<Rightarrow> getF (f v tcb) = getF tcb; P (\<exists>cap. caps_of_state s p = Some cap \<and> P' cap)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma same_object_as_cte_refs:
  "\<lbrakk> same_object_as cap cap' \<rbrakk> \<Longrightarrow>
     cte_refs cap' = cte_refs cap" apply (rule ext, cases cap, simp_all add: same_object_as_def) apply (clarsimp simp: is_cap_simps bits_of_def
                      split: cap.split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. same_object_as cap cap' \<Longrightarrow> cte_refs cap' = cte_refs cap proof (prove)
goal (7 subgoals):
 1. \<And>x x32 x33. \<lbrakk>is_ep_cap cap'; cap = EndpointCap (obj_ref_of cap') x32 x33\<rbrakk> \<Longrightarrow> cte_refs cap' x = {}
 2. \<And>x x42 x43. \<lbrakk>is_ntfn_cap cap'; cap = NotificationCap (obj_ref_of cap') x42 x43\<rbrakk> \<Longrightarrow> cte_refs cap' x = {}
 3. \<And>x x51 x52 x53. \<lbrakk>\<exists>m' cr. cap' = ReplyCap x51 m' cr; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> cte_refs cap' x = {}
 4. \<And>x x63. \<lbrakk>is_cnode_cap cap'; cap = CNodeCap (obj_ref_of cap') (bits_of cap') x63\<rbrakk> \<Longrightarrow> cte_refs cap' x = {obj_ref_of cap'} \<times> {xs. length xs = bits_of cap'}
 5. \<And>x. \<lbrakk>is_thread_cap cap'; cap = ThreadCap (obj_ref_of cap')\<rbrakk> \<Longrightarrow> cte_refs cap' x = {obj_ref_of cap'} \<times> dom tcb_cap_cases
 6. \<And>x. \<lbrakk>case cap' of IRQHandlerCap n \<Rightarrow> False | _ \<Rightarrow> same_region_as IRQControlCap cap'; cap = IRQControlCap\<rbrakk> \<Longrightarrow> cte_refs cap' x = {}
 7. \<And>x x12. \<lbrakk>case cap' of ArchObjectCap x \<Rightarrow> same_aobject_as x12 x | _ \<Rightarrow> same_region_as (ArchObjectCap x12) cap'; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> cte_refs cap' x = {} proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma same_object_untyped_range:
  "\<lbrakk> same_object_as cap cap' \<rbrakk>
     \<Longrightarrow> untyped_range cap = {}" by (cases cap, (clarsimp simp: same_object_as_def is_cap_simps)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. same_object_as cap cap' \<Longrightarrow> untyped_range cap = {}
theory Tcb_AI

lemma same_object_zombies:
  "\<lbrakk> same_object_as cap cap' \<rbrakk>
     \<Longrightarrow> is_zombie cap = is_zombie cap'" by (cases cap, (clarsimp simp: same_object_as_def is_cap_simps
                          split: cap.split_asm)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. same_object_as cap cap' \<Longrightarrow> is_zombie cap = is_zombie cap'
theory Tcb_AI

lemma zombies_final_helperE:
  "\<lbrakk> caps_of_state s p = Some cap; r \<in> obj_refs cap; \<not> is_zombie cap;
     zombies_final s; caps_of_state s p' = Some cap'; r \<in> obj_refs cap' \<rbrakk>
     \<Longrightarrow> \<not> is_zombie cap'" apply (cases p', drule caps_of_state_cteD[simplified cte_wp_at_eq_simp],
         drule(2) zombies_final_helper) apply (fastforce simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; \<not> is_zombie cap; zombies_final s; caps_of_state s p' = Some cap'; r \<in> obj_refs cap'\<rbrakk> \<Longrightarrow> \<not> is_zombie cap' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>r \<in> obj_refs cap; \<not> is_zombie cap; zombies_final s; caps_of_state s p' = Some cap'; r \<in> obj_refs cap'; p' = (a, b); \<forall>r\<in>obj_refs cap. \<forall>a b. cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s\<rbrakk> \<Longrightarrow> \<not> is_zombie cap' proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma cap_badge_none_master:
  "(cap_badge (cap_master_cap cap) = None)
     = (cap_badge cap = None)" by (simp add: cap_master_cap_def split: cap.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap_badge (cap_master_cap cap) = None) = (cap_badge cap = None)
theory Tcb_AI

lemma cap_master_eq_badge_none:
  "\<lbrakk> cap_master_cap cap = cap_master_cap cap' \<rbrakk>
        \<Longrightarrow> (cap_badge cap = None) = (cap_badge cap' = None)" apply (subst cap_badge_none_master[symmetric], simp) apply (simp add: cap_badge_none_master) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap cap = cap_master_cap cap' \<Longrightarrow> (cap_badge cap = None) = (cap_badge cap' = None) proof (prove)
goal (1 subgoal):
 1. cap_master_cap cap = cap_master_cap cap' \<Longrightarrow> (cap_badge (cap_master_cap cap') = None) = (cap_badge cap' = None) proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma check_cap_inv2:
  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
  shows      "\<lbrace>P and Q ()\<rbrace> check_cap_at cap slot f \<lbrace>Q\<rbrace>" unfolding check_cap_at_def by (wp x get_cap_wp, clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and Q ()\<rbrace> check_cap_at cap slot f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and Q ()\<rbrace> do cap' <- get_cap slot;
when (same_object_as cap cap') f
od \<lbrace>Q\<rbrace>
theory Tcb_AI

lemma tcb_cap_always_valid_strg:
  "(case tcb_cap_cases p of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> \<forall>st. restr t st cap)
      \<and> (p = tcb_cnode_index 4 \<longrightarrow> (\<forall>ptr. valid_ipc_buffer_cap cap ptr))
         \<longrightarrow> tcb_cap_valid cap (t, p) s" by (clarsimp simp: tcb_cap_valid_def st_tcb_def2 tcb_at_def
              split: option.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case tcb_cap_cases p of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> \<forall>st. restr t st cap) \<and> (p = tcb_cnode_index 4 \<longrightarrow> (\<forall>ptr. valid_ipc_buffer_cap cap ptr)) \<longrightarrow> tcb_cap_valid cap (t, p) s
theory Tcb_AI

lemma no_cap_to_obj_with_diff_ref_ran_caps_form:
  "no_cap_to_obj_dr_emp cap
     = (\<lambda>s. \<forall>cp \<in> ran (caps_of_state s).
              obj_refs cp = obj_refs cap \<longrightarrow> table_cap_ref cp = table_cap_ref cap)" apply (rule ext, simp add: no_cap_to_obj_with_diff_ref_def) apply (simp add: ball_ran_eq cte_wp_at_caps_of_state) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_cap_to_obj_dr_emp cap = (\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). obj_refs cp = obj_refs cap \<longrightarrow> table_cap_ref cp = table_cap_ref cap) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) = (\<forall>cp\<in>ran (caps_of_state s). obj_refs cp = obj_refs cap \<longrightarrow> table_cap_ref cp = table_cap_ref cap) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>a b capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s (a, b) = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap) = (\<forall>a b cp. caps_of_state s (a, b) = Some cp \<longrightarrow> obj_refs cp = obj_refs cap \<longrightarrow> table_cap_ref cp = table_cap_ref cap) proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma thread_set_valid_objs'':
  "\<lbrace>valid_objs and (\<lambda>s. \<forall>tcb. get_tcb t s = Some tcb
        \<longrightarrow> valid_tcb t tcb s \<longrightarrow> valid_tcb t (f tcb) s)\<rbrace>
     thread_set f t
   \<lbrace>\<lambda>rv. valid_objs\<rbrace>" apply (simp add: thread_set_def set_object_def get_object_def) apply wp apply (clarsimp simp: fun_upd_def[symmetric]) apply (frule(1) valid_tcb_objs) apply (rule valid_objs_tcb_update, simp_all add: tcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and (\<lambda>s. \<forall>tcb. get_tcb t s = Some tcb \<longrightarrow> valid_tcb t tcb s \<longrightarrow> valid_tcb t (f tcb) 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>tcb. get_tcb t s = Some tcb \<longrightarrow> valid_tcb t tcb s \<longrightarrow> valid_tcb t (f tcb) s)\<rbrace> do tcb <- gets_the (get_tcb t);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and (\<lambda>s. \<forall>tcb. get_tcb t s = Some tcb \<longrightarrow> valid_tcb t tcb s \<longrightarrow> valid_tcb t (f tcb) s)) s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> valid_objs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f (the (get_tcb t s))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>valid_objs s; valid_tcb t y s \<longrightarrow> valid_tcb t (f y) s; get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> valid_objs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f y))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>valid_objs s; valid_tcb t y s \<longrightarrow> valid_tcb t (f y) s; get_tcb t s = Some y; kheap s t = Some (TCB tcb); valid_tcb t y s\<rbrakk> \<Longrightarrow> valid_objs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f y))\<rparr>) proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma out_tcb_valid:
  assumes x: "\<And>tcb v. tcb_state  (fn v tcb) = tcb_state  tcb"
  assumes w: "\<And>tcb v. tcb_ipc_buffer (fn v tcb) = tcb_ipc_buffer tcb
                          \<or> tcb_ipc_buffer (fn v tcb) = 0"
  shows      "\<lbrace>tcb_cap_valid c p\<rbrace> option_update_thread t fn v
              \<lbrace>\<lambda>rv. tcb_cap_valid c p\<rbrace>" apply (case_tac v, simp_all add: option_update_thread_def) apply (rule thread_set_tcb_valid [OF x w]) done

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

lemma update_mcpriority_valid_tcb[simp]:
  "valid_tcb p t s \<Longrightarrow> valid_tcb p (t\<lparr>tcb_mcpriority := x\<rparr>) s" by (simp add: valid_tcb_def ran_tcb_cap_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_tcb p t s \<Longrightarrow> valid_tcb p (t\<lparr>tcb_mcpriority := x\<rparr>) s
theory Tcb_AI

lemma set_mcpriority_valid_objs[wp]:
  "\<lbrace>invs\<rbrace> set_mcpriority t x \<lbrace>\<lambda>rv. valid_objs\<rbrace>" unfolding set_mcpriority_def apply (wp thread_set_cte_at thread_set_valid_objs') apply (simp add: Invariants_AI.invs_valid_objs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> set_mcpriority t x \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> thread_set (tcb_mcpriority_update (\<lambda>_. x)) t \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> (valid_objs and (\<lambda>s. \<forall>p t. valid_tcb p t s \<longrightarrow> valid_tcb p (t\<lparr>tcb_mcpriority := x\<rparr>) s)) s proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma set_mcpriority_invs[wp]:
  "\<lbrace>invs and tcb_at t\<rbrace> set_mcpriority t x \<lbrace>\<lambda>rv. invs\<rbrace>" unfolding set_mcpriority_def by (wp thread_set_valid_objs''
             thread_set_refs_trivial
             thread_set_hyp_refs_trivial
             thread_set_iflive_trivial
             thread_set_mdb
             thread_set_ifunsafe_trivial
             thread_set_cur_tcb
             thread_set_zombies_trivial
             thread_set_valid_idle_trivial
             thread_set_global_refs_triv
             thread_set_valid_reply_caps_trivial
             thread_set_valid_reply_masters_trivial
             valid_irq_node_typ valid_irq_handlers_lift
             thread_set_caps_of_state_trivial
             thread_set_arch_caps_trivial
             thread_set_only_idle
             thread_set_cap_refs_in_kernel_window
             thread_set_valid_ioc_trivial valid_ioports_lift
             thread_set_cap_refs_respects_device_region
              | simp add: ran_tcb_cap_cases invs_def valid_state_def valid_pspace_def
              | rule conjI | erule disjE)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t\<rbrace> set_mcpriority t x \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t\<rbrace> thread_set (tcb_mcpriority_update (\<lambda>_. x)) t \<lbrace>\<lambda>rv. invs\<rbrace>
theory Tcb_AI

lemma sbn_has_reply[wp]:
  "\<lbrace>\<lambda>s. P (has_reply_cap t s)\<rbrace> set_bound_notification tcb ntfnptr \<lbrace>\<lambda>rv s. P (has_reply_cap t s)\<rbrace>" apply (simp add: has_reply_cap_def cte_wp_at_caps_of_state) apply (wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (has_reply_cap t s)\<rbrace> set_bound_notification tcb ntfnptr \<lbrace>\<lambda>rv s. P (has_reply_cap t s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_reply_cap_to t cap)\<rbrace> set_bound_notification tcb ntfnptr \<lbrace>\<lambda>rv s. P (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_reply_cap_to t cap)\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma set_set_simple_ko_has_reply[wp]:
  "\<lbrace>\<lambda>s. P (has_reply_cap t s)\<rbrace> set_simple_ko f ntfnptr ntfn \<lbrace>\<lambda>rv s. P (has_reply_cap t s)\<rbrace>" by (simp add: has_reply_cap_def cte_wp_at_caps_of_state, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (has_reply_cap t s)\<rbrace> set_simple_ko f ntfnptr ntfn \<lbrace>\<lambda>rv s. P (has_reply_cap t s)\<rbrace>
theory Tcb_AI

lemma unbind_notification_has_reply[wp]:
  "\<lbrace>\<lambda>s. P (has_reply_cap t s)\<rbrace> unbind_notification t' \<lbrace>\<lambda>rv s. P (has_reply_cap t s)\<rbrace>" apply (simp add: unbind_notification_def has_reply_cap_def cte_wp_at_caps_of_state) apply (rule hoare_seq_ext[OF _ gbn_sp]) apply (case_tac ntfnptr, simp, wp, simp) apply (clarsimp) apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (wp, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (has_reply_cap t s)\<rbrace> unbind_notification t' \<lbrace>\<lambda>rv s. P (has_reply_cap t s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_reply_cap_to t cap)\<rbrace> do ntfnptr <- get_bound_notification t';
case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn t'
od
od \<lbrace>\<lambda>rv s. P (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_reply_cap_to t cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr. \<lbrace>bound_tcb_at ((=) ntfnptr) t' and (\<lambda>s. P (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_reply_cap_to t cap))\<rbrace> case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn t'
od \<lbrace>\<lambda>rv s. P (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_reply_cap_to t cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr a. ntfnptr = Some a \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t' and (\<lambda>s. P (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_reply_cap_to t cap))\<rbrace> case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn t'
od \<lbrace>\<lambda>rv s. P (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_reply_cap_to t cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrace>bound_tcb_at ((=) (Some a)) t' and (\<lambda>s. P (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_reply_cap_to t cap))\<rbrace> do ntfn <- get_notification a;
y <- set_notification a (ntfn_set_bound_tcb ntfn None);
set_bound_notification t' None
od \<lbrace>\<lambda>rv s. P (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_reply_cap_to t cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn. \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) t' and (\<lambda>s. P (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_reply_cap_to t cap)))\<rbrace> do y <- set_notification a (ntfn_set_bound_tcb ntfn None);
set_bound_notification t' None
od \<lbrace>\<lambda>rv s. P (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_reply_cap_to t cap)\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma range_check_inv[wp]:
  "\<lbrace>P\<rbrace> range_check a b c \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: range_check_def) apply (rule hoare_pre, wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> range_check a b c \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> unlessE (b \<le> a \<and> a \<le> c) (throwError (RangeError b c)) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (if b \<le> a \<and> a \<le> c then P else (\<lambda>s. P s \<and> True)) s proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma decode_readreg_inv:
  "\<lbrace>P\<rbrace> decode_read_registers args (cap.ThreadCap t) \<lbrace>\<lambda>rv. P\<rbrace>" apply (rule hoare_pre) apply (simp add: decode_read_registers_def whenE_def | rule conjI | clarsimp
          | wp (once) | wpcw)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_read_registers args (ThreadCap t) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> decode_read_registers args (ThreadCap t) \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma decode_copyreg_inv:
  "\<lbrace>P\<rbrace> decode_copy_registers args (cap.ThreadCap t) extras \<lbrace>\<lambda>rv. P\<rbrace>" apply (rule hoare_pre) apply (simp   add: decode_copy_registers_def whenE_def
           split del: if_split
          | wp (once) | wpcw)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_copy_registers args (ThreadCap t) extras \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> decode_copy_registers args (ThreadCap t) extras \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma decode_set_tls_base_inv:
  "\<lbrace>P\<rbrace> decode_set_tls_base args (cap.ThreadCap t) \<lbrace>\<lambda>rv. P\<rbrace>" apply (rule hoare_pre) apply (simp   add: decode_set_tls_base_def whenE_def
           split del: if_split
          | wp (once) | wpcw)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_set_tls_base args (ThreadCap t) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> decode_set_tls_base args (ThreadCap t) \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!