kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchIpc_IF

lemma set_thread_state_runnable_equiv_but_for_labels[Ipc_IF_assms]:
  "runnable tst
   \<Longrightarrow> \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L)\<rbrace>
       set_thread_state thread tst
       \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" unfolding set_thread_state_def apply (wpsimp wp: set_object_equiv_but_for_labels[THEN hoare_set_object_weaken_pre]
                    set_thread_state_ext_runnable_equiv_but_for_labels) apply (wpsimp wp: set_object_wp)+ apply (fastforce dest: get_tcb_not_asid_pool_at simp: st_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. runnable tst \<Longrightarrow> \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L)\<rbrace> set_thread_state thread tst \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. runnable tst \<Longrightarrow> \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L)\<rbrace> do tcb <- gets_the $ get_tcb thread;
set_object thread (TCB (tcb\<lparr>tcb_state := tst\<rparr>));
do_extended_op (set_thread_state_ext thread)
od \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. runnable tst \<Longrightarrow> \<lbrace>?P'19 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_state := tst\<rparr>)) \<lbrace>\<lambda>rv. st_tcb_at runnable thread\<rbrace>
 2. runnable tst \<Longrightarrow> \<lbrace>?Q1\<rbrace> gets_the $ get_tcb thread \<lbrace>\<lambda>tcb s. (\<forall>ko. ko_at ko thread s \<longrightarrow> a_type (TCB (tcb\<lparr>tcb_state := tst\<rparr>)) = a_type ko \<longrightarrow> (equiv_but_for_labels aag L st and (\<lambda>s. \<not> typ_at (AArch AASIDPool) thread s) and K ((\<forall>asid_pool. TCB (tcb\<lparr>tcb_state := tst\<rparr>) \<noteq> ArchObj (ASIDPool asid_pool)) \<and> pasObjectAbs aag thread \<in> L)) s) \<and> K (pasObjectAbs aag thread \<in> L) s \<and> ?P'19 tcb s\<rbrace>
 3. \<And>s. \<lbrakk>runnable tst; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L)) s\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>runnable tst; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; get_tcb thread s = Some y\<rbrakk> \<Longrightarrow> (\<forall>ko. ko_at ko thread s \<longrightarrow> ATCB = a_type ko \<longrightarrow> \<not> typ_at (AArch AASIDPool) thread s) \<and> st_tcb_at runnable thread (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (y\<lparr>tcb_state := tst\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchIpc_IF

lemma set_endpoint_equiv_but_for_labels[Ipc_IF_assms]:
  "\<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag epptr \<in> L)\<rbrace>
   set_endpoint epptr ep
   \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" unfolding set_simple_ko_def apply (wp set_object_equiv_but_for_labels get_object_wp) apply (clarsimp simp: asid_pool_at_kheap partial_inv_def obj_at_def split: kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag epptr \<in> L)\<rbrace> set_endpoint epptr ep \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag epptr \<in> L)\<rbrace> do obj <- get_object epptr;
assert (is_simple_type obj);
assert (partial_inv Endpoint obj \<noteq> None);
set_object epptr (Endpoint ep)
od \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag epptr \<in> L)) s \<Longrightarrow> \<forall>ko. ko_at ko epptr s \<longrightarrow> is_simple_type ko \<longrightarrow> partial_inv Endpoint ko \<noteq> None \<longrightarrow> (equiv_but_for_labels aag L st and (\<lambda>s. \<not> typ_at (AArch AASIDPool) epptr s) and K ((\<forall>asid_pool. Endpoint ep \<noteq> ArchObj (ASIDPool asid_pool)) \<and> pasObjectAbs aag epptr \<in> L)) s proof (prove)
goal:
No subgoals!
theory ArchIpc_IF

lemma conj_imp:
  "\<lbrakk> Q \<longrightarrow> R; P \<longrightarrow> Q; P' \<longrightarrow> Q \<rbrakk> \<Longrightarrow> (P \<longrightarrow> R) \<and> (P' \<longrightarrow> R)" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Q \<longrightarrow> R; P \<longrightarrow> Q; P' \<longrightarrow> Q\<rbrakk> \<Longrightarrow> (P \<longrightarrow> R) \<and> (P' \<longrightarrow> R)
theory ArchIpc_IF

lemma arch_derive_cap_reads_respects[Ipc_IF_assms]:
  "reads_respects aag l \<top> (arch_derive_cap cap)" unfolding arch_derive_cap_def apply (rule equiv_valid_guard_imp) apply (wp | wpc)+ apply (simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (arch_derive_cap cap) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (case cap of PageCap dev r R pgs x \<Rightarrow> returnOk (ArchObjectCap (PageCap dev r R pgs None)) | PageTableCap xa None \<Rightarrow> throwError IllegalOperation | PageTableCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap cap) | PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap cap) | _ \<Rightarrow> returnOk (ArchObjectCap cap)) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (case cap of PageCap dev r R pgs x \<Rightarrow> returnOk (ArchObjectCap (PageCap dev r R pgs None)) | PageTableCap xa None \<Rightarrow> throwError IllegalOperation | PageTableCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap cap) | PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap cap) | _ \<Rightarrow> returnOk (ArchObjectCap cap))
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> (\<forall>x xa. cap = ASIDPoolCap x xa \<longrightarrow> True) \<and> (cap = ASIDControlCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. cap = PageCap x xa xb xc xd \<longrightarrow> True) \<and> (\<forall>x xa. cap = PageTableCap x xa \<longrightarrow> (xa = None \<longrightarrow> True) \<and> (\<forall>x. xa = Some x \<longrightarrow> True)) \<and> (\<forall>x xa. cap = PageDirectoryCap x xa \<longrightarrow> (xa = None \<longrightarrow> True) \<and> (\<forall>x. xa = Some x \<longrightarrow> True)) proof (prove)
goal:
No subgoals!
theory ArchIpc_IF

lemma arch_derive_cap_rev[Ipc_IF_assms]:
  "reads_equiv_valid_inv aag l \<top> (arch_derive_cap cap)" unfolding arch_derive_cap_def apply (rule equiv_valid_guard_imp) apply (wp | wpc)+ apply (simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv aag l (\<lambda>_. True) (arch_derive_cap cap) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv aag l (\<lambda>_. True) (case cap of PageCap dev r R pgs x \<Rightarrow> returnOk (ArchObjectCap (PageCap dev r R pgs None)) | PageTableCap xa None \<Rightarrow> throwError IllegalOperation | PageTableCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap cap) | PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap cap) | _ \<Rightarrow> returnOk (ArchObjectCap cap)) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_inv aag l ?Q (case cap of PageCap dev r R pgs x \<Rightarrow> returnOk (ArchObjectCap (PageCap dev r R pgs None)) | PageTableCap xa None \<Rightarrow> throwError IllegalOperation | PageTableCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap cap) | PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap cap) | _ \<Rightarrow> returnOk (ArchObjectCap cap))
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> (\<forall>x xa. cap = ASIDPoolCap x xa \<longrightarrow> True) \<and> (cap = ASIDControlCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. cap = PageCap x xa xb xc xd \<longrightarrow> True) \<and> (\<forall>x xa. cap = PageTableCap x xa \<longrightarrow> (xa = None \<longrightarrow> True) \<and> (\<forall>x. xa = Some x \<longrightarrow> True)) \<and> (\<forall>x xa. cap = PageDirectoryCap x xa \<longrightarrow> (xa = None \<longrightarrow> True) \<and> (\<forall>x. xa = Some x \<longrightarrow> True)) proof (prove)
goal:
No subgoals!
theory ArchIpc_IF

lemma complete_signal_reads_respects[Ipc_IF_assms]:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects aag l (K (aag_can_read aag ntfnptr \<or> aag_can_affect aag l ntfnptr))
                        (complete_signal ntfnptr receiver)" unfolding complete_signal_def by (wp set_simple_ko_reads_respects get_simple_ko_reads_respects as_user_set_register_reads_respects'
      | wpc | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read_or_affect aag l ntfnptr)) (complete_signal ntfnptr receiver) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read_or_affect aag l ntfnptr)) (do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of ActiveNtfn badge \<Rightarrow> do as_user receiver $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn
od | _ \<Rightarrow> fail
od)
theory ArchIpc_IF

lemma handle_arch_fault_reply_reads_respects[Ipc_IF_assms, wp]:
  "reads_respects aag l (K (aag_can_read aag thread)) (handle_arch_fault_reply afault thread x y)" by (simp add: handle_arch_fault_reply_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag thread)) (handle_arch_fault_reply afault thread x y)
theory ArchIpc_IF

lemma arch_get_sanitise_register_info_reads_respects[Ipc_IF_assms, wp]:
  "reads_respects aag l \<top> (arch_get_sanitise_register_info t)" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (arch_get_sanitise_register_info t)
theory ArchIpc_IF

lemma lookup_ipc_buffer_aligned'[Ipc_IF_assms]:
  "\<lbrace>valid_objs\<rbrace>
   lookup_ipc_buffer True thread
   \<lbrace>\<lambda>rv s. rv = Some buf' \<longrightarrow> is_aligned buf' msg_align_bits\<rbrace>" apply (insert lookup_ipc_buffer_aligned) apply (fastforce simp: valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_ipc_buffer True thread \<lbrace>\<lambda>rv s. rv = Some buf' \<longrightarrow> is_aligned buf' msg_align_bits\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>thread. \<lbrace>valid_objs\<rbrace> lookup_ipc_buffer True thread \<lbrace>\<lambda>rv _. case rv of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits\<rbrace>) \<Longrightarrow> \<lbrace>valid_objs\<rbrace> lookup_ipc_buffer True thread \<lbrace>\<lambda>rv s. rv = Some buf' \<longrightarrow> is_aligned buf' msg_align_bits\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchIpc_IF

lemma handle_arch_fault_reply_globals_equiv[Ipc_IF_assms]:
  "\<lbrace>globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
   handle_arch_fault_reply vmf thread x y
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" by (wpsimp simp: handle_arch_fault_reply_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> handle_arch_fault_reply vmf thread x y \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory ArchIpc_IF

lemma get_message_info_reads_respects[Ipc_IF_assms]:
  "reads_respects aag (l :: 'a subject_label) (K (aag_can_read_or_affect aag l ptr)) (get_message_info ptr)" apply (simp add: get_message_info_def) apply (wp as_user_reads_respects | clarsimp simp: getRegister_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read_or_affect aag l ptr)) (get_message_info ptr) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. aag_can_read_or_affect aag l ptr) (do x <- as_user ptr (getRegister msg_info_register);
return (data_to_message_info x)
od) proof (prove)
goal:
No subgoals!
theory ArchIpc_IF

lemma make_arch_fault_msg_reads_respects[Ipc_IF_assms]:
  "reads_respects aag (l :: 'a subject_label) (\<lambda>y. aag_can_read_or_affect aag l sender)
                  (make_arch_fault_msg x4 sender)" apply (case_tac x4) apply (wp as_user_reads_respects | simp add: det_getRegister det_getRestartPC)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. aag_can_read_or_affect aag l sender) (make_arch_fault_msg x4 sender) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. x4 = VMFault x1 x2 \<Longrightarrow> reads_respects aag l (\<lambda>y. aag_can_read_or_affect aag l sender) (make_arch_fault_msg x4 sender) proof (prove)
goal:
No subgoals!
theory Decode_IF

lemma ensure_empty_rev:
  "reads_equiv_valid_inv A aag (K (is_subject aag (fst slot))) (ensure_empty slot)" unfolding ensure_empty_def fun_app_def by (wp get_cap_rev | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject aag (fst slot))) (ensure_empty slot) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject aag (fst slot))) (doE cap <- liftE (get_cap slot);
whenE (cap \<noteq> NullCap) (throwError DeleteFirst)
odE)
theory Decode_IF

lemma prop_of_obj_ref_of_cnode_cap:
  "\<lbrakk> is_cnode_cap cap; \<forall>r\<in>obj_refs_ac cap. P r \<rbrakk>
     \<Longrightarrow> P (obj_ref_of cap)" by (case_tac cap, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_cnode_cap cap; \<forall>r\<in>obj_refs_ac cap. P r\<rbrakk> \<Longrightarrow> P (obj_ref_of cap)
theory Decode_IF

lemma get_irq_state_rev:
  "reads_equiv_valid_inv A aag (K (is_subject_irq aag irq)) (get_irq_state irq)" unfolding get_irq_state_def apply (rule equiv_valid_guard_imp[OF gets_ev]) apply (fastforce simp: reads_equiv_def2
                   elim: states_equiv_forE_interrupt_states
                  intro: aag_can_read_irq_self) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject_irq aag irq)) (get_irq_state irq) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject_irq aag irq)) (gets (\<lambda>s. interrupt_states s irq)) proof (prove)
goal (1 subgoal):
 1. \<And>s. K (is_subject_irq aag irq) s \<Longrightarrow> \<forall>s t. reads_equiv aag s t \<and> A s t \<longrightarrow> interrupt_states s irq = interrupt_states t irq proof (prove)
goal:
No subgoals!
theory Decode_IF

lemma is_irq_active_rev:
  "reads_equiv_valid_inv A aag (K (is_subject_irq aag irq)) (is_irq_active irq)" unfolding is_irq_active_def fun_app_def by (wp get_irq_state_rev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject_irq aag irq)) (is_irq_active irq) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject_irq aag irq)) (liftM (\<lambda>st. st \<noteq> IRQInactive) (get_irq_state irq))
theory Decode_IF

lemma if_apply_ev:
  "equiv_valid I A B P (if a then b x  else c x) \<Longrightarrow>
   equiv_valid I A B P ((if a then b else c) x)" by (simp split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P (if a then b x else c x) \<Longrightarrow> equiv_valid I A B P ((if a then b else c) x)
theory Decode_IF

lemma whenE_throwError_bindE_ev:
  assumes ev: "\<not> b \<Longrightarrow> equiv_valid I A A P f"
  shows "equiv_valid I A A P (whenE b (throwError x) >>=E (\<lambda>_. f))" apply (rule_tac Q="\<lambda> rv s. \<not> b \<and> P s" in bindE_ev_pre) using ev apply (fastforce simp: equiv_valid_def2 equiv_valid_2_def) apply (wp whenE_throwError_sp)+ by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P (doE _ <- whenE b (throwError x);
f
odE) proof (prove)
goal (4 subgoals):
 1. \<And>rv. equiv_valid_inv I A (\<lambda>s. \<not> b \<and> P s) f
 2. equiv_valid_inv I A ?P' (whenE b (throwError x))
 3. \<lbrace>?P''\<rbrace> whenE b (throwError x) \<lbrace>\<lambda>rv s. \<not> b \<and> P s\<rbrace>, -
 4. \<And>s. P s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
using this:
\<not> b \<Longrightarrow> equiv_valid_inv I A P f

goal (4 subgoals):
 1. \<And>rv. equiv_valid_inv I A (\<lambda>s. \<not> b \<and> P s) f
 2. equiv_valid_inv I A ?P' (whenE b (throwError x))
 3. \<lbrace>?P''\<rbrace> whenE b (throwError x) \<lbrace>\<lambda>rv s. \<not> b \<and> P s\<rbrace>, -
 4. \<And>s. P s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (3 subgoals):
 1. equiv_valid_inv I A ?P' (whenE b (throwError x))
 2. \<lbrace>?P''\<rbrace> whenE b (throwError x) \<lbrace>\<lambda>rv s. \<not> b \<and> P s\<rbrace>, -
 3. \<And>s. P s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (b \<longrightarrow> True) \<and> P s
theory Decode_IF

lemma expand_len_gr_Suc_0:
  "Suc 0 < length xs = (xs \<noteq> [] \<and> Suc (Suc 0) \<le> length xs)" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Suc 0 < length xs) = (xs \<noteq> [] \<and> Suc (Suc 0) \<le> length xs)
theory Decode_IF

lemma range_check_ev:
  "equiv_valid_inv I A \<top> (range_check v v_min v_max)" unfolding range_check_def fun_app_def unlessE_whenE apply (rule equiv_valid_guard_imp) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>_. True) (range_check v v_min v_max) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>_. True) (whenE (\<not> (v_min \<le> v \<and> v \<le> v_max)) (throwError (RangeError v_min v_max))) proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv I A ?Q (whenE (\<not> (v_min \<le> v \<and> v \<le> v_max)) (throwError (RangeError v_min v_max)))
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<not> (v_min \<le> v \<and> v \<le> v_max) \<longrightarrow> True proof (prove)
goal:
No subgoals!
theory Decode_IF

lemma aag_has_auth_to_obj_refs_of_owned_cap:
  "\<lbrakk> pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s;
     a \<in> cap_auth_conferred cap; x \<in> obj_refs_ac cap \<rbrakk>
     \<Longrightarrow> aag_has_auth_to aag a x" apply (drule sym, erule ssubst) apply (rule_tac s=s in pas_refined_mem) apply (fastforce intro: sta_caps[OF cte_wp_at_caps_of_state']) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; a \<in> cap_auth_conferred cap; x \<in> obj_refs_ac cap\<rbrakk> \<Longrightarrow> (pasSubject aag, a, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; cte_wp_at ((=) cap) slot s; a \<in> cap_auth_conferred cap; x \<in> obj_refs_ac cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst slot), a, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; cte_wp_at ((=) cap) slot s; a \<in> cap_auth_conferred cap; x \<in> obj_refs_ac cap\<rbrakk> \<Longrightarrow> (fst slot, a, x) \<in> state_objs_to_policy s
 2. \<lbrakk>pas_refined aag s; cte_wp_at ((=) cap) slot s; a \<in> cap_auth_conferred cap; x \<in> obj_refs_ac cap\<rbrakk> \<Longrightarrow> pas_refined aag s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; cte_wp_at ((=) cap) slot s; a \<in> cap_auth_conferred cap; x \<in> obj_refs_ac cap\<rbrakk> \<Longrightarrow> pas_refined aag s proof (prove)
goal:
No subgoals!
theory Decode_IF

lemma OR_choice_def2:
  "\<lbrakk> \<And>P. \<lbrace>P\<rbrace> (c :: bool det_ext_monad) \<lbrace>\<lambda>_. P\<rbrace>; empty_fail c \<rbrakk>
     \<Longrightarrow> (OR_choice c f g) = (do b \<leftarrow> c; if b then f else g od)" apply (simp add: OR_choice_def wrap_ext_bool_det_ext_ext_def ef_mk_ef) by (subst no_state_changes[where f=c], simp, fastforce simp: bind_assoc split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> c \<lbrace>\<lambda>_. P\<rbrace>; empty_fail c\<rbrakk> \<Longrightarrow> OR_choice c f g = do b <- c;
if b then f else g
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> c \<lbrace>\<lambda>_. P\<rbrace>; empty_fail c\<rbrakk> \<Longrightarrow> do ex <- get;
(rv, uu_) <- select_f (c ex);
if rv then f else g
od = do b <- c;
if b then f else g
od
theory Decode_IF

lemma check_prio_rev:
  "reads_respects aag l (\<lambda>s. is_subject aag auth) (check_prio prio auth)" by (wpsimp simp: check_prio_def wp: thread_get_reads_respects hoare_drop_imps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. is_subject aag auth) (check_prio prio auth)
theory Decode_IF

lemma decode_set_priority_rev:
  "reads_respects aag l (K (\<forall>x \<in> set excs. pas_cap_cur_auth aag (fst x)) and (pas_refined aag))
                  (decode_set_priority args (ThreadCap t) slot excs)" apply (wpsimp simp: decode_set_priority_def aag_cap_auth_Thread[symmetric]
                wp: check_prio_rev whenE_throwError_wp) apply (case_tac excs; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (\<forall>x\<in>set excs. pas_cap_cur_auth aag (fst x)) and pas_refined aag) (decode_set_priority args (ThreadCap t) slot excs) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>\<forall>x\<in>set excs. pas_cap_cur_auth aag (fst x); pas_refined aag s; args \<noteq> []; excs \<noteq> []; fst (excs ! 0) = ThreadCap x\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag (ThreadCap x) proof (prove)
goal:
No subgoals!
theory Decode_IF

lemma decode_set_mcpriority_rev:
  "reads_respects aag l (K (\<forall>x \<in> set excs. pas_cap_cur_auth aag (fst x)) and (pas_refined aag))
                  (decode_set_mcpriority args cap slot excs)" apply (wpsimp simp: decode_set_mcpriority_def aag_cap_auth_Thread[symmetric]
                  wp: check_prio_rev whenE_throwError_wp) apply (case_tac excs; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (\<forall>x\<in>set excs. pas_cap_cur_auth aag (fst x)) and pas_refined aag) (decode_set_mcpriority args cap slot excs) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>\<forall>x\<in>set excs. pas_cap_cur_auth aag (fst x); pas_refined aag s; args \<noteq> []; excs \<noteq> []; fst (excs ! 0) = ThreadCap x\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag (ThreadCap x) proof (prove)
goal:
No subgoals!
theory Decode_IF

lemma decode_set_sched_params_rev:
  "reads_respects aag l (K (\<forall>x \<in> set excs. pas_cap_cur_auth aag (fst x)) and (pas_refined aag))
                  (decode_set_sched_params args cap slot excs)" apply (wpsimp simp: decode_set_sched_params_def aag_cap_auth_Thread[symmetric]
                  wp: check_prio_rev whenE_throwError_wp) apply (case_tac excs; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (\<forall>x\<in>set excs. pas_cap_cur_auth aag (fst x)) and pas_refined aag) (decode_set_sched_params args cap slot excs) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>\<forall>x\<in>set excs. pas_cap_cur_auth aag (fst x); pas_refined aag s; \<not> length args < 2; excs \<noteq> []; fst (excs ! 0) = ThreadCap x\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag (ThreadCap x) proof (prove)
goal:
No subgoals!
theory Decode_IF

lemma vspace_cap_rights_to_auth_mask_vm_rights:
  "vspace_cap_rights_to_auth (mask_vm_rights R d) \<subseteq> vspace_cap_rights_to_auth R" apply (rule vspace_cap_rights_to_auth_mono) apply (auto simp: mask_vm_rights_def dest: subsetD[OF validate_vm_rights_subseteq]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vspace_cap_rights_to_auth (mask_vm_rights R d) \<subseteq> vspace_cap_rights_to_auth R proof (prove)
goal (1 subgoal):
 1. mask_vm_rights R d \<subseteq> R proof (prove)
goal:
No subgoals!