kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchFinalise_IF

lemma prepare_thread_delete_reads_respects_f[Finalise_IF_assms]:
  "reads_respects_f aag l \<top> (prepare_thread_delete thread)" unfolding prepare_thread_delete_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (\<lambda>_. True) (prepare_thread_delete thread) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (\<lambda>_. True) (return ())
theory ArchFinalise_IF

lemma maskInterrupt_no_mem:
  "maskInterrupt a b \<lbrace>\<lambda>ms. P (underlying_memory ms)\<rbrace>" by (wpsimp simp: maskInterrupt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. P (underlying_memory ms)\<rbrace> maskInterrupt a b \<lbrace>\<lambda>_ ms. P (underlying_memory ms)\<rbrace>
theory ArchFinalise_IF

lemma maskInterrupt_no_exclusive:
  "maskInterrupt a b \<lbrace>\<lambda>ms. P (exclusive_state ms)\<rbrace>" by (wpsimp simp: maskInterrupt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. P (exclusive_state ms)\<rbrace> maskInterrupt a b \<lbrace>\<lambda>_ ms. P (exclusive_state ms)\<rbrace>
theory ArchFinalise_IF

lemma set_irq_state_valid_global_objs:
  "set_irq_state state irq \<lbrace>valid_global_objs\<rbrace>" apply (simp add: set_irq_state_def) apply (wp modify_wp) apply (fastforce simp: valid_global_objs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs\<rbrace> set_irq_state state irq \<lbrace>\<lambda>_. valid_global_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs\<rbrace> do y <- modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>);
do_machine_op (maskInterrupt (state = IRQInactive) irq)
od \<lbrace>\<lambda>_. valid_global_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_global_objs s \<Longrightarrow> valid_global_objs (s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchFinalise_IF

lemma set_irq_state_globals_equiv[Finalise_IF_assms]:
  "set_irq_state state irq \<lbrace>globals_equiv st\<rbrace>" apply (simp add: set_irq_state_def) apply (wp dmo_no_mem_globals_equiv maskInterrupt_no_mem maskInterrupt_no_exclusive modify_wp) apply (simp add: globals_equiv_interrupt_states_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st\<rbrace> set_irq_state state irq \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st\<rbrace> do y <- modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>);
do_machine_op (maskInterrupt (state = IRQInactive) irq)
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. globals_equiv st s \<Longrightarrow> globals_equiv st (s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchFinalise_IF

lemma set_notification_globals_equiv[Finalise_IF_assms]:
  "\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
   set_notification ptr ntfn
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding set_simple_ko_def apply (wp set_object_globals_equiv get_object_wp) apply (fastforce simp: obj_at_def valid_arch_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> set_notification ptr ntfn \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> do obj <- get_object ptr;
assert (is_simple_type obj);
assert (partial_inv Notification obj \<noteq> None);
set_object ptr (Notification ntfn)
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (globals_equiv st and valid_arch_state) s \<Longrightarrow> \<forall>ko. ko_at ko ptr s \<longrightarrow> is_simple_type ko \<longrightarrow> partial_inv Notification ko \<noteq> None \<longrightarrow> (globals_equiv st and (\<lambda>s. ptr \<noteq> arm_global_pd (arch_state s)) and (\<lambda>t. ptr = idle_thread t \<longrightarrow> (\<forall>tcb. kheap t (idle_thread t) = Some (TCB tcb) \<longrightarrow> (\<exists>tcb'. Notification ntfn = TCB tcb' \<and> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> (\<forall>tcb'. Notification ntfn = TCB tcb' \<longrightarrow> tcb_at (idle_thread t) t))) s proof (prove)
goal:
No subgoals!
theory ArchFinalise_IF

lemma delete_asid_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
   delete_asid asid pd
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding delete_asid_def by (wpsimp wp: set_vm_root_globals_equiv set_asid_pool_globals_equiv
                 invalidate_asid_entry_globals_equiv flush_space_globals_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> delete_asid asid pd \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> do asid_table <- gets (arm_asid_table \<circ> arch_state);
case asid_table (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory ArchFinalise_IF

lemma pagebitsforsize_ge_2[simp]:
  "2 \<le> pageBitsForSize vmpage_size" by (induct vmpage_size; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 \<le> pageBitsForSize vmpage_size
theory ArchFinalise_IF

lemma arch_finalise_cap_globals_equiv[Finalise_IF_assms]:
  "\<lbrace>globals_equiv st and invs and valid_arch_cap cap\<rbrace>
   arch_finalise_cap cap b
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (induct cap; simp add: arch_finalise_cap_def) by (wp delete_asid_pool_globals_equiv case_option_wp unmap_page_globals_equiv
         unmap_page_table_globals_equiv delete_asid_globals_equiv
      | wpc | clarsimp split: bool.splits option.splits | intro impI conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and invs and valid_arch_cap cap\<rbrace> arch_finalise_cap cap b \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2. \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> valid_arch_cap (ASIDPoolCap x1 x2) a\<rbrace> case b of True \<Rightarrow> do delete_asid_pool x2 x1;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> valid_arch_cap ASIDControlCap a\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>x1 x2 x3 x4 x5. \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> valid_arch_cap (PageCap x1 x2 x3 x4 x5) a\<rbrace> case x5 of None \<Rightarrow> return (NullCap, NullCap) | Some (a, v) \<Rightarrow> do y <- unmap_page x4 a v x2;
return (NullCap, NullCap)
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>x1 x2. \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> valid_arch_cap (PageTableCap x1 x2) a\<rbrace> case x2 of None \<Rightarrow> return (NullCap, NullCap) | Some (a, v) \<Rightarrow> case b of True \<Rightarrow> do unmap_page_table a v x1;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<And>x1 x2. \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> valid_arch_cap (PageDirectoryCap x1 x2) a\<rbrace> case x2 of None \<Rightarrow> return (NullCap, NullCap) | Some a \<Rightarrow> case b of True \<Rightarrow> do delete_asid a x1;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory ArchFinalise_IF

lemma set_bound_notification_globals_equiv[Finalise_IF_assms]:
  "\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
   set_bound_notification ref ts
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding set_bound_notification_def apply (wp set_object_globals_equiv dxo_wp_weak |simp)+ apply (intro impI conjI allI) by (clarsimp simp: valid_arch_state_def obj_at_def tcb_at_def2 get_tcb_def is_tcb_def
               dest: get_tcb_SomeD
              split: option.splits kernel_object.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> set_bound_notification ref ts \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> do tcb <- gets_the $ get_tcb ref;
set_object ref (TCB (tcb\<lparr>tcb_bound_notification := ts\<rparr>))
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. globals_equiv s sa \<and> valid_arch_state sa \<Longrightarrow> (\<exists>y. get_tcb ref sa = Some y) \<longrightarrow> ref \<noteq> arm_global_pd (arch_state sa) \<and> (ref = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) = Some (TCB tcb) \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch (the (get_tcb (idle_thread sa) sa)))) \<and> tcb_at (idle_thread sa) sa) proof (prove)
goal (3 subgoals):
 1. \<And>sa. \<lbrakk>globals_equiv s sa \<and> valid_arch_state sa; \<exists>y. get_tcb ref sa = Some y\<rbrakk> \<Longrightarrow> ref \<noteq> arm_global_pd (arch_state sa)
 2. \<And>sa tcb. \<lbrakk>globals_equiv s sa \<and> valid_arch_state sa; \<exists>y. get_tcb ref sa = Some y; ref = idle_thread sa; kheap sa (idle_thread sa) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch (the (get_tcb (idle_thread sa) sa)))
 3. \<And>sa. \<lbrakk>globals_equiv s sa \<and> valid_arch_state sa; \<exists>y. get_tcb ref sa = Some y; ref = idle_thread sa\<rbrakk> \<Longrightarrow> tcb_at (idle_thread sa) sa
theory Tcb_IF

lemma setup_reply_master_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
   setup_reply_master t
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding setup_reply_master_def apply (wp set_cap_globals_equiv'' set_original_globals_equiv get_cap_wp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> setup_reply_master t \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = NullCap) $ do set_original (t, tcb_cnode_index 2) True;
set_cap (ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (globals_equiv st and valid_arch_state) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (if cap = NullCap then \<lambda>s. globals_equiv st s \<and> valid_arch_state s else globals_equiv st) s proof (prove)
goal:
No subgoals!
theory Tcb_IF

lemma restart_globals_equiv[wp]:
  "\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
   restart t
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding restart_def by (wpsimp wp: dxo_wp_weak set_thread_state_globals_equiv setup_reply_master_globals_equiv gts_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> restart t \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> do state <- get_thread_state t;
when (\<not> runnable state \<and> state \<noteq> IdleThreadState) $ do cancel_ipc t;
setup_reply_master t;
set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t);
do_extended_op (possible_switch_to t)
od
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory Tcb_IF

lemma globals_equiv_ioc_update[simp]:
  "globals_equiv st (is_original_cap_update f s) = globals_equiv st s" by (simp add: globals_equiv_def idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_equiv st (is_original_cap_update f s) = globals_equiv st s
theory Tcb_IF

lemma cap_swap_for_delete_globals_equiv[wp]:
  "\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
   cap_swap_for_delete a b
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding cap_swap_for_delete_def cap_swap_def set_original_def by (wp modify_wp set_cdt_globals_equiv set_cap_globals_equiv'' dxo_wp_weak | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> when (a \<noteq> b) $ do cap1 <- get_cap a;
cap2 <- get_cap b;
set_cap cap2 a;
set_cap cap1 b;
slot1_p <- gets (\<lambda>s. cdt s a);
slot2_p <- gets (\<lambda>s. cdt s b);
cdt <- gets cdt;
cdt' <- return (\<lambda>n. if cdt n = Some a then Some b else if cdt n = Some b then Some a else cdt n);
set_cdt (cdt'(a := cdt' b, b := cdt' a));
do_extended_op (cap_swap_ext a b slot1_p slot2_p);
is_original <- gets is_original_cap;
do r <- gets is_original_cap;
modify (is_original_cap_update (\<lambda>_. r(a := is_original b)))
od;
r <- gets is_original_cap;
modify (is_original_cap_update (\<lambda>_. r(b := is_original a)))
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory Tcb_IF

lemma cap_delete_globals_equiv:
  "\<lbrace>globals_equiv st and invs and emptyable a\<rbrace>
   cap_delete a
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding cap_delete_def apply (wp rec_del_globals_equiv) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and invs and emptyable a\<rbrace> cap_delete a \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and invs and emptyable a\<rbrace> doE rec_del (CTEDeleteCall a True);
returnOk ()
odE \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (globals_equiv st and invs and emptyable a) s \<Longrightarrow> (invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall (CTEDeleteCall a True)) s \<and> valid_rec_del_call (CTEDeleteCall a True) s) \<and> invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall (CTEDeleteCall a True)) s \<and> valid_rec_del_call (CTEDeleteCall a True) s proof (prove)
goal:
No subgoals!
theory Tcb_IF

lemma no_cap_to_idle_thread:
   "invs (s :: det_state) \<Longrightarrow> \<not> ex_nonz_cap_to (idle_thread s) s" apply (rule no_cap_to_idle_thread') apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> \<not> ex_nonz_cap_to (idle_thread s) s proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> valid_global_refs s proof (prove)
goal:
No subgoals!
theory Tcb_IF

lemma bind_notification_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
   bind_notification t ntfnptr
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding bind_notification_def by (wp set_bound_notification_globals_equiv set_notification_globals_equiv | wpc | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> bind_notification t ntfnptr \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> do ntfn <- get_notification ntfnptr;
ntfn' <- return $ ntfn_set_bound_tcb ntfn (Some t);
set_notification ntfnptr ntfn';
set_bound_notification t $ Some ntfnptr
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory Tcb_IF

lemma invoke_tcb_NotificationControl_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
   invoke_tcb (NotificationControl t ntfn)
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (case_tac ntfn, simp_all) apply (wp unbind_notification_globals_equiv bind_notification_globals_equiv)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> invoke_tcb (NotificationControl t ntfn) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. ntfn = None \<Longrightarrow> \<lbrace>globals_equiv st and valid_arch_state\<rbrace> liftE (do y <- unbind_notification t;
return []
od) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>a. ntfn = Some a \<Longrightarrow> \<lbrace>globals_equiv st and valid_arch_state\<rbrace> liftE (do y <- bind_notification t a;
return []
od) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_IF

lemma dxo_globals_equiv[wp]:
  "do_extended_op eop \<lbrace>globals_equiv st\<rbrace>" by (simp | wp dxo_wp_weak)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st\<rbrace> do_extended_op eop \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory Tcb_IF

lemma det_zipWithM:
  assumes "\<And>x y. \<lbrakk> x \<in> set xs; y \<in> set ys \<rbrakk> \<Longrightarrow> det (f x y)"
  shows "det (zipWithM f xs ys)" apply (simp add: zipWithM_mapM) apply (rule det_mapM[OF _ subset_refl]) apply (simp add: split_def) apply (case_tac x) apply (clarsimp) apply (erule in_set_zipE) apply (erule (1) assms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det (zipWithM f xs ys) proof (prove)
goal (1 subgoal):
 1. det (mapM (\<lambda>(x, y). f x y) (zip xs ys)) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (zip xs ys) \<Longrightarrow> det (case x of (x, xa) \<Rightarrow> f x xa) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (zip xs ys) \<Longrightarrow> det (f (fst x) (snd x)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>x \<in> set (zip xs ys); x = (a, b)\<rbrakk> \<Longrightarrow> det (f (fst x) (snd x)) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. (aa, ba) \<in> set (zip xs ys) \<Longrightarrow> det (f aa ba) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>aa \<in> set xs; ba \<in> set ys\<rbrakk> \<Longrightarrow> det (f aa ba) proof (prove)
goal:
No subgoals!
theory Tcb_IF

lemma checked_insert_reads_respects:
  "reads_respects aag l
     (K (is_subject aag (fst b) \<and> is_subject aag (fst d) \<and> is_subject aag (fst e)))
     (check_cap_at a b (check_cap_at c d (cap_insert a b e)))" apply (rule equiv_valid_guard_imp) apply (simp add: check_cap_at_def) apply (wp when_ev cap_insert_reads_respects get_cap_wp get_cap_rev | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (fst b) \<and> is_subject aag (fst d) \<and> is_subject aag (fst e))) (check_cap_at a b (check_cap_at c d (cap_insert a b e))) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (check_cap_at a b (check_cap_at c d (cap_insert a b e)))
 2. \<And>s. K (is_subject aag (fst b) \<and> is_subject aag (fst d) \<and> is_subject aag (fst e)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (do cap' <- get_cap b;
when (same_object_as a cap') (do cap' <- get_cap d;
when (same_object_as c cap') (cap_insert a b e)
od)
od)
 2. \<And>s. K (is_subject aag (fst b) \<and> is_subject aag (fst d) \<and> is_subject aag (fst e)) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Tcb_IF

lemma ethread_set_reads_respects:
  "reads_respects aag l \<top> (ethread_set f word)" apply (simp add: ethread_set_def) apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def put_def get_def bind_def set_eobject_def
                        return_def gets_def gets_the_def assert_opt_def get_etcb_def fail_def
                  cong: option.case_cong split: option.splits) apply (fastforce intro: equiv_forI reads_equiv_ekheap_updates affects_equiv_ekheap_update
                    elim: states_equiv_forE_ekheap
                    simp: reads_equiv_def2 affects_equiv_def2 ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (ethread_set f word) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_etcb word);
set_eobject word (f tcb)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 t x2a. \<lbrakk>ekheap s word = Some x2; ekheap t word = Some x2a; reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> reads_equiv aag (ekheap_update (\<lambda>_. (ekheap s)(word \<mapsto> f x2)) s) (ekheap_update (\<lambda>_. (ekheap t)(word \<mapsto> f x2a)) t) \<and> affects_equiv aag l (ekheap_update (\<lambda>_. (ekheap s)(word \<mapsto> f x2)) s) (ekheap_update (\<lambda>_. (ekheap t)(word \<mapsto> f x2a)) t) proof (prove)
goal:
No subgoals!
theory Tcb_IF

lemma set_priority_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects aag (l :: 'a subject_label)
           (pas_refined aag and K (is_subject aag word) and pas_cur_domain aag
                            and (\<lambda>s. is_subject aag (cur_thread s)))
           (set_priority word prio)" apply (simp add: set_priority_def thread_set_priority_def) apply (wp get_thread_state_rev gets_cur_thread_ev gts_wp when_ev
            hoare_vcg_all_lift hoare_vcg_imp_lift'
            ethread_set_reads_respects
            tcb_sched_action_reads_respects
            possible_switch_to_reads_respects
         | simp split del: if_split
         | wp (once) hoare_drop_imps
         | (rule hoare_strengthen_post, rule ethread_set_priority_pas_refined)
         | force)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and K (is_subject aag word) and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) (set_priority word prio) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and (\<lambda>y. is_subject aag word) and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) (do y <- tcb_sched_action tcb_sched_dequeue word;
y <- ethread_set (tcb_priority_update (\<lambda>_. prio)) word;
ts <- get_thread_state word;
when (runnable ts) (do cur <- gets cur_thread;
if word = cur then reschedule_required else possible_switch_to word
od)
od) proof (prove)
goal:
No subgoals!
theory Tcb_IF

lemma set_mcpriority_reads_respects:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "reads_respects aag (l :: 'a subject_label) \<top> (set_mcpriority x y)" unfolding set_mcpriority_def by (rule thread_set_reads_respects[OF domains_distinct])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (set_mcpriority x y) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (thread_set (tcb_mcpriority_update (\<lambda>_. y)) x)
theory Tcb_IF

lemma checked_cap_insert_only_timer_irq_inv:
  "check_cap_at a b (check_cap_at c d (cap_insert a b e)) \<lbrace>only_timer_irq_inv irq (st :: det_state)\<rbrace>" apply (simp add: only_timer_irq_inv_def) apply (wp only_timer_irq_pres checked_cap_insert_domain_sep_inv | clarsimp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st\<rbrace> check_cap_at a b (check_cap_at c d (cap_insert a b e)) \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> check_cap_at a b (check_cap_at c d (cap_insert a b e)) \<lbrace>\<lambda>_. domain_sep_inv False st and only_timer_irq irq\<rbrace> proof (prove)
goal:
No subgoals!