kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_IF

lemma requiv_get_tcb_eq':
  "\<lbrakk> reads_equiv aag s t; aag_can_read aag thread \<rbrakk>
     \<Longrightarrow> get_tcb thread s = get_tcb thread t" by (auto simp: reads_equiv_def2 get_tcb_def
           elim: states_equiv_forE_kheap
          dest!: aag_can_read_self)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s t; aag_can_read aag thread\<rbrakk> \<Longrightarrow> get_tcb thread s = get_tcb thread t
theory Finalise_IF

lemma set_scheduler_action_reads_respects[wp]:
  "reads_respects aag l \<top> (set_scheduler_action action)" by (simp add: set_scheduler_action_def equiv_valid_def2 equiv_valid_2_def modify_def bind_def put_def
                get_def reads_equiv_scheduler_action_update affects_equiv_scheduler_action_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (set_scheduler_action action)
theory Finalise_IF

lemma set_thread_state_ext_owned_reads_respects:
  "reads_respects aag l (\<lambda>s. aag_can_read aag ref) (set_thread_state_ext ref)" apply (simp add: set_thread_state_ext_def when_def get_thread_state_def | wp thread_get_rev)+ apply (simp add: reads_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. aag_can_read aag ref) (set_thread_state_ext ref) proof (prove)
goal (1 subgoal):
 1. aag_can_read aag ref \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t) \<and> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> scheduler_action s = scheduler_action t) proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma set_thread_state_owned_reads_respects:
  "reads_respects aag l (\<lambda>s. aag_can_read aag ref) (set_thread_state ref ts)" apply (simp add: set_thread_state_def) apply (wp set_object_reads_respects gets_the_ev set_thread_state_ext_owned_reads_respects) by (fastforce intro: kheap_get_tcb_eq elim: reads_equivE equiv_forD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. aag_can_read aag ref) (set_thread_state ref ts) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. aag_can_read aag ref) (do tcb <- gets_the (get_tcb ref);
y <- set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext ref
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. aag_can_read aag ref \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb ref s = get_tcb ref t) s \<and> (get_tcb ref s \<noteq> None \<longrightarrow> True \<and> aag_can_read aag ref)
theory Finalise_IF

lemma set_bound_notification_owned_reads_respects:
  "reads_respects aag l (\<lambda>s. is_subject aag ref) (set_bound_notification ref ntfn)" apply (simp add: set_bound_notification_def) apply (wp set_object_reads_respects gets_the_ev) apply (force elim: reads_equivE equiv_forE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. is_subject aag ref) (set_bound_notification ref ntfn) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. is_subject aag ref) (do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. is_subject aag ref \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb ref s = get_tcb ref t) s \<and> (get_tcb ref s \<noteq> None \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma get_thread_state_runnable[wp]:
   "\<lbrace>st_tcb_at runnable ref\<rbrace> get_thread_state ref \<lbrace>\<lambda>rv _. runnable rv\<rbrace>" by (wpsimp wp: gts_st_tcb_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at runnable ref\<rbrace> get_thread_state ref \<lbrace>\<lambda>rv _. runnable rv\<rbrace>
theory Finalise_IF

lemma get_ep_queue_reads_respects:
  "reads_respects aag l \<top> (get_ep_queue ep)" unfolding get_ep_queue_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) (get_ep_queue ep) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (case ep of IdleEP \<Rightarrow> fail | SendEP q \<Rightarrow> return q | RecvEP q \<Rightarrow> return q) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (case ep of IdleEP \<Rightarrow> fail | SendEP q \<Rightarrow> return q | RecvEP q \<Rightarrow> return q)
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> (ep = IdleEP \<longrightarrow> True) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> True) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma get_object_reads_respects:
  "reads_respects aag l (K (aag_can_read aag ptr \<or> (aag_can_affect aag l ptr))) (get_object ptr)" apply (unfold get_object_def fun_app_def) apply (subst gets_apply) apply (wp gets_apply_ev | wp (once) hoare_drop_imps)+ apply (fastforce elim: reads_equivE affects_equivE equiv_forE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag ptr \<or> aag_can_affect aag l ptr)) (get_object ptr) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag ptr \<or> aag_can_affect aag l ptr)) (do kh <- gets kheap;
assert (kh ptr \<noteq> None);
return (the (kh ptr))
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag ptr \<or> aag_can_affect aag l ptr)) (do a <- gets_apply kheap ptr;
assert (a \<noteq> None);
return (the a)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. K (aag_can_read aag ptr \<or> aag_can_affect aag l ptr) s \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> kheap s ptr = kheap t ptr) s \<and> True \<and> (kheap s ptr \<noteq> None \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma get_simple_ko_reads_respects:
  "reads_respects aag l (K (aag_can_read aag ptr \<or> aag_can_affect aag l ptr))
    (get_simple_ko f ptr)" unfolding get_simple_ko_def by (wp get_object_reads_respects | wpc | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag ptr \<or> aag_can_affect aag l ptr)) (get_simple_ko f ptr) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag ptr \<or> aag_can_affect aag l ptr)) (do kobj <- get_object ptr;
assert (is_simple_type kobj);
case partial_inv f kobj of None \<Rightarrow> fail | Some e \<Rightarrow> return e
od)
theory Finalise_IF

lemma get_epq_SendEP_ret:
  "\<lbrace>\<lambda>s. \<forall>x\<in>set list. P x\<rbrace> get_ep_queue (SendEP list) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. P x\<rbrace>" by (wpsimp simp: get_ep_queue_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>set list. P x\<rbrace> get_ep_queue (SendEP list) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. P x\<rbrace>
theory Finalise_IF

lemma get_epq_RecvEP_ret:
  "\<lbrace>\<lambda>s. \<forall>x\<in>set list. P x\<rbrace> get_ep_queue (RecvEP list) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. P x\<rbrace>" by (wpsimp simp: get_ep_queue_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>set list. P x\<rbrace> get_ep_queue (RecvEP list) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. P x\<rbrace>
theory Finalise_IF

lemma obj_eq_st_tcb_at:
  "\<lbrakk> kheap s x = kheap s' x; st_tcb_at P x s' \<rbrakk>
    \<Longrightarrow> st_tcb_at P x s" by (clarsimp simp: st_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = kheap s' x; st_tcb_at P x s'\<rbrakk> \<Longrightarrow> st_tcb_at P x s
theory Finalise_IF

lemma receive_blocked_on_tcb_st_to_auth:
  "receive_blocked_on epptr ts \<Longrightarrow> (epptr, Receive) \<in> tcb_st_to_auth ts" by (case_tac ts, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. receive_blocked_on epptr ts \<Longrightarrow> (epptr, Receive) \<in> tcb_st_to_auth ts
theory Finalise_IF

lemma not_ep_queue_invisible:
  "\<lbrakk> \<not> ep_queue_invisible aag l eplist; eplist = SendEP list \<or> eplist = RecvEP list \<rbrakk>
     \<Longrightarrow> \<exists>t \<in> set list. aag_can_read aag t \<or> aag_can_affect aag l t" by (auto simp: labels_are_invisible_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> ep_queue_invisible aag l eplist; eplist = SendEP list \<or> eplist = RecvEP list\<rbrakk> \<Longrightarrow> \<exists>t\<in>set list. aag_can_read aag t \<or> aag_can_affect aag l t
theory Finalise_IF

lemma get_endpoint_revrv:
  "reads_equiv_valid_rv_inv (affects_equiv aag l) aag
     (\<lambda>ep ep'. (\<not> ep_queue_invisible aag l ep \<or> \<not> ep_queue_invisible aag l ep') \<longrightarrow> ep = ep')
     (pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of
                      and K ((pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag))
     (get_endpoint epptr)" apply (rule equiv_valid_2_rvrel_imp, rule get_simple_ko_revrv) apply (simp add: inj_Endpoint) apply (auto elim: ep_queues_are_invisible_or_eps_are_equal[rule_format]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>ep ep'. \<not> ep_queue_invisible aag l ep \<or> \<not> ep_queue_invisible aag l ep' \<longrightarrow> ep = ep') (pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and K ((pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag)) (get_endpoint epptr) proof (prove)
goal (2 subgoals):
 1. inj Endpoint
 2. \<And>s t. \<exists>sa ta. reads_equiv aag sa ta \<and> affects_equiv aag l sa ta \<and> (pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and K ((pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag)) sa \<and> (pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and K ((pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag)) ta \<and> ko_at (Endpoint s) epptr sa \<and> ko_at (Endpoint t) epptr ta \<Longrightarrow> \<not> ep_queue_invisible aag l s \<or> \<not> ep_queue_invisible aag l t \<longrightarrow> s = t proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<exists>sa ta. reads_equiv aag sa ta \<and> affects_equiv aag l sa ta \<and> (pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and K ((pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag)) sa \<and> (pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and K ((pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag)) ta \<and> ko_at (Endpoint s) epptr sa \<and> ko_at (Endpoint t) epptr ta \<Longrightarrow> \<not> ep_queue_invisible aag l s \<or> \<not> ep_queue_invisible aag l t \<longrightarrow> s = t proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma gen_asm_ev2_r:
  "(P' \<Longrightarrow> equiv_valid_2 I A B R P \<top> f f') \<Longrightarrow> equiv_valid_2 I A B R P (\<lambda>s. P') f f'" by (rule gen_asm_ev2_r')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P' \<Longrightarrow> equiv_valid_2 I A B R P (\<lambda>_. True) f f') \<Longrightarrow> equiv_valid_2 I A B R P (\<lambda>s. P') f f'
theory Finalise_IF

lemma gen_asm_ev2_l:
  "(P \<Longrightarrow> equiv_valid_2 I A B R \<top> P' f f') \<Longrightarrow> equiv_valid_2 I A B R (\<lambda>s. P) P' f f'" by (rule gen_asm_ev2_l')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> equiv_valid_2 I A B R (\<lambda>_. True) P' f f') \<Longrightarrow> equiv_valid_2 I A B R (\<lambda>s. P) P' f f'
theory Finalise_IF

lemma bind_return_unit2:
  "f = return () >>= (\<lambda>_. f)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f = do _ <- return ();
f
od
theory Finalise_IF

lemma ev2_inv:
  assumes inv: "\<And>P. f \<lbrace>P\<rbrace>"
  assumes inv': "\<And>P. g \<lbrace>P\<rbrace>"
  shows "equiv_valid_2 I A A \<top>\<top> \<top> \<top> f g" apply (clarsimp simp: equiv_valid_2_def) apply (drule state_unchanged[OF inv]) apply (drule state_unchanged[OF inv']) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A A (\<lambda>_ _. True) (\<lambda>_. True) (\<lambda>_. True) f g proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); I s t; A s t\<rbrakk> \<Longrightarrow> I b ba \<and> A b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(aa, ba) \<in> fst (g t); I s t; A s t; s = b\<rbrakk> \<Longrightarrow> I b ba \<and> A b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>I s t; A s t; s = b; t = ba\<rbrakk> \<Longrightarrow> I b ba \<and> A b ba
theory Finalise_IF

lemma ev2_sym:
  assumes symI: "\<And>x y. I x y \<Longrightarrow> I y x"
  assumes symA: "\<And>x y. A x y \<Longrightarrow> A y x"
  assumes symB: "\<And>x y. B x y \<Longrightarrow> B y x"
  assumes symR: "\<And>x y. R x y \<Longrightarrow> R y x"
  shows "equiv_valid_2 I A B R P' P f' f \<Longrightarrow>
         equiv_valid_2 I A B R P P' f f'" apply (clarsimp simp: equiv_valid_2_def) apply (blast intro: symA symB symI symR) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A B R P' P f' f \<Longrightarrow> equiv_valid_2 I A B R P P' f f' proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P' s \<and> P t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>x\<in>fst (f' s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> R rva rvb \<and> I s' t' \<and> B s' t'); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); P s; P' t; I s t; A s t\<rbrakk> \<Longrightarrow> R a aa \<and> I b ba \<and> B b ba proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma not_label_is_invisible:
  "(\<not> labels_are_invisible aag l {(pasObjectAbs aag x)}) =
   (aag_can_read aag x \<or> aag_can_affect aag l x)" by (simp add: labels_are_invisible_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> labels_are_invisible aag l {pasObjectAbs aag x}) = (aag_can_read aag x \<or> aag_can_affect aag l x)
theory Finalise_IF

lemma label_is_invisible:
  "(labels_are_invisible aag l {(pasObjectAbs aag x)}) =
   (\<not> (aag_can_read aag x \<or> aag_can_affect aag l x))" by (simp add: labels_are_invisible_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. labels_are_invisible aag l {pasObjectAbs aag x} = (\<not> (aag_can_read aag x \<or> aag_can_affect aag l x))
theory Finalise_IF

lemma op_eq_unit_taut: "(=) = (\<lambda> (_:: unit) _. True)" by (rule ext | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (=) = (\<lambda>_ _. True)
theory Finalise_IF

lemma ev2_symmetric:
  "equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) P P f f'
   \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) P P f' f" apply (clarsimp simp add: equiv_valid_2_def) apply (drule_tac x=t in spec) apply (drule_tac x=s in spec) apply (fastforce elim: affects_equiv_sym reads_equiv_sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) P P f f' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) P P f' f proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f' t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> affects_equiv aag l s' t'); (a, b) \<in> fst (f' s); (aa, ba) \<in> fst (f t); P s; P t; reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f' s); (aa, ba) \<in> fst (f t); P s; P t; reads_equiv aag s t; affects_equiv aag l s t; \<forall>ta. P t \<and> P ta \<and> reads_equiv aag t ta \<and> affects_equiv aag l t ta \<longrightarrow> (\<forall>x\<in>fst (f t). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f' ta). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> affects_equiv aag l s' t')\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f' s); (aa, ba) \<in> fst (f t); P s; P t; reads_equiv aag s t; affects_equiv aag l s t; P t \<and> P s \<and> reads_equiv aag t s \<and> affects_equiv aag l t s \<longrightarrow> (\<forall>x\<in>fst (f t). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f' s). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> affects_equiv aag l s' t')\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma reads_respects_ethread_get:
  "reads_respects aag l (\<lambda>_. is_subject aag thread) (ethread_get f thread)" apply (simp add: ethread_get_def) apply wp apply (drule aag_can_read_self) apply (fastforce simp: reads_equiv_def2 get_etcb_def equiv_for_def states_equiv_for_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. is_subject aag thread) (ethread_get f thread) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. is_subject aag thread) (do tcb <- gets_the (get_etcb thread);
return (f tcb)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. is_subject aag thread \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_etcb thread s = get_etcb thread t) s \<and> (get_etcb thread s \<noteq> None \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s. aag_can_read aag thread \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_etcb thread s = get_etcb thread t) s \<and> (get_etcb thread s \<noteq> None \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma gets_apply_ready_queues_reads_respects:
  "reads_respects aag l (\<lambda>_. pasSubject aag \<in> pasDomainAbs aag d) (gets_apply ready_queues d)" apply (rule gets_apply_ev') apply (force elim: reads_equivE simp: equiv_for_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. pasSubject aag \<in> pasDomainAbs aag d) (gets_apply ready_queues d) proof (prove)
goal (1 subgoal):
 1. \<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<and> pasSubject aag \<in> pasDomainAbs aag d \<and> pasSubject aag \<in> pasDomainAbs aag d \<longrightarrow> ready_queues s d = ready_queues t d proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma equiv_valid_rv_trivial':
  assumes inv: "\<And>P. f \<lbrace>P\<rbrace>"
  shows "equiv_valid_rv_inv I A \<top>\<top> Q f" by (auto simp: equiv_valid_2_def dest: state_unchanged[OF inv])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A (\<lambda>_ _. True) Q f
theory Finalise_IF

lemma gets_cur_domain_ev:
  "reads_equiv_valid_inv A aag \<top> (gets cur_domain)" apply (rule equiv_valid_guard_imp) apply wp apply (simp add: reads_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>_. True) (gets cur_domain) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_inv A aag ?Q (gets cur_domain)
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>s t. reads_equiv aag s t \<and> A s t \<longrightarrow> cur_domain s = cur_domain t proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma set_tcb_queue_modifies_at_most:
  "modifies_at_most aag L (\<lambda>s. pasDomainAbs aag d \<inter> L \<noteq> {}) (set_tcb_queue d prio queue)" apply (rule modifies_at_mostI) apply (simp add: set_tcb_queue_def modify_def, wp) apply (force simp: equiv_but_for_labels_def states_equiv_for_def equiv_for_def equiv_asids_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modifies_at_most aag L (\<lambda>s. pasDomainAbs aag d \<inter> L \<noteq> {}) (set_tcb_queue d prio queue) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrace>(\<lambda>s. pasDomainAbs aag d \<inter> L \<noteq> {}) and equiv_but_for_labels aag L st\<rbrace> set_tcb_queue d prio queue \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>st s. ((\<lambda>s. pasDomainAbs aag d \<inter> L \<noteq> {}) and equiv_but_for_labels aag L st) s \<Longrightarrow> equiv_but_for_labels aag L st (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues s d' p) s) proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma reschedule_required_reads_respects[wp]:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects aag l (pas_refined aag) reschedule_required" apply (simp add: reschedule_required_def | wp tcb_sched_action_reads_respects | wpc)+ apply (simp add: reads_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag) reschedule_required proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<Longrightarrow> \<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> scheduler_action s = scheduler_action t proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma cancel_all_ipc_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs
                                               and valid_arch_state and K (aag_can_read aag epptr))
                        (cancel_all_ipc epptr)" unfolding cancel_all_ipc_def fun_app_def by (wp mapM_x_ev'' tcb_sched_action_reads_respects set_thread_state_runnable_reads_respects
         set_thread_state_pas_refined hoare_vcg_ball_lift
         set_thread_state_runnable_valid_sched_action
         set_simple_ko_reads_respects get_ep_queue_reads_respects get_epq_SendEP_ret
         get_epq_RecvEP_ret get_simple_ko_reads_respects get_simple_ko_wp
      | wpc
      | clarsimp simp: ball_conj_distrib
      | rule subset_refl
      | wp (once) hoare_drop_imps
      | assumption
      | rule hoare_strengthen_post[where Q="\<lambda>_. pas_refined aag and pspace_aligned
                                                                and valid_vspace_objs
                                                                and valid_arch_state", OF mapM_x_wp])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (aag_can_read aag epptr)) (cancel_all_ipc epptr) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (aag_can_read aag epptr)) (do ep <- get_endpoint epptr;
case ep of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue ep;
set_endpoint epptr IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) queue;
do_extended_op reschedule_required
od
od)