kings-crown/FVELER_Isabelle huggingface dataset:
theory Tcb_AC

lemma map_le_to_cca:
  "m \<subseteq>\<^sub>m m' \<Longrightarrow> cdt_change_allowed aag subjects m tcbsts ptr
   \<Longrightarrow> cdt_change_allowed aag subjects m' tcbsts ptr" apply (elim cdt_change_allowedE cdt_change_allowedI[rotated]) by (rule map_le_to_rtrancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<subseteq>\<^sub>m m'; cdt_change_allowed aag subjects m tcbsts ptr\<rbrakk> \<Longrightarrow> cdt_change_allowed aag subjects m' tcbsts ptr proof (prove)
goal (1 subgoal):
 1. \<And>pptr. \<lbrakk>m \<subseteq>\<^sub>m m'; m \<Turnstile> pptr \<rightarrow>* ptr\<rbrakk> \<Longrightarrow> m' \<Turnstile> pptr \<rightarrow>* ptr
theory Tcb_AC

lemma sbn_bind_respects:
  "\<lbrace>integrity aag X st and bound_tcb_at ((=) None) t and
    K (aag_has_auth_to aag Receive ntfn \<and> is_subject aag t)\<rbrace>
   set_bound_notification t (Some ntfn)
   \<lbrace>\<lambda>_. integrity aag X st \<rbrace>" apply (simp add: set_bound_notification_def) apply (wpsimp wp: set_object_wp) apply (erule integrity_trans) apply (clarsimp simp: integrity_def obj_at_def pred_tcb_at_def integrity_asids_kh_upds) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and bound_tcb_at ((=) None) t and K ((pasSubject aag, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> is_subject aag t)\<rbrace> set_bound_notification t (Some ntfn) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and bound_tcb_at ((=) None) t and (\<lambda>y. (pasSubject aag, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> is_subject aag t)\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := Some ntfn\<rparr>))
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>integrity aag X st s; bound_tcb_at ((=) None) t s; (pasSubject aag, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag; is_subject aag t; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_bound_notification := Some ntfn\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>bound_tcb_at ((=) None) t s; (pasSubject aag, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag; is_subject aag t; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> integrity aag X s (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_bound_notification := Some ntfn\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!
theory Tcb_AC

lemma bind_notification_respects:
  "\<lbrace>integrity aag X st and pas_refined aag and bound_tcb_at ((=) None) t
                       and K (aag_has_auth_to aag Receive ntfn \<and> is_subject aag t)\<rbrace>
   bind_notification t ntfn
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (clarsimp simp: bind_notification_def) apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (wp set_ntfn_respects hoare_vcg_imp_lift sbn_bind_respects | wpc | clarsimp)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and bound_tcb_at ((=) None) t and K ((pasSubject aag, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> is_subject aag t)\<rbrace> bind_notification t ntfn \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. (pasSubject aag, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> is_subject aag t \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and bound_tcb_at ((=) None) t\<rbrace> bind_notification t ntfn \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag; is_subject aag t\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and bound_tcb_at ((=) None) t\<rbrace> do ntfna <- get_notification ntfn;
y <- set_notification ntfn (ntfn_set_bound_tcb ntfna (Some t));
set_bound_notification t (Some ntfn)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfna. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag; is_subject aag t\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (integrity aag X st and pas_refined aag and bound_tcb_at ((=) None) t)\<rbrace> do y <- set_notification ntfn (ntfn_set_bound_tcb ntfna (Some t));
set_bound_notification t (Some ntfn)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfna s. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag; is_subject aag t; ko_at (Notification ntfna) ntfn s; integrity aag X st s; pas_refined aag s; bound_tcb_at ((=) None) t s\<rbrakk> \<Longrightarrow> \<exists>auth. (pasSubject aag, auth, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify \<or> auth = Reset) proof (prove)
goal:
No subgoals!
theory Tcb_AC

lemma invoke_tcb_bind_notification_respects:
  "\<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action
                       and tcb_inv_wf (NotificationControl t (Some ntfn))
                       and K (authorised_tcb_inv aag (NotificationControl t (Some ntfn)))\<rbrace>
   invoke_tcb (NotificationControl t (Some ntfn))
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (clarsimp) apply (wp bind_notification_respects) apply (clarsimp simp: authorised_tcb_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (NotificationControl t (Some ntfn)) and K (authorised_tcb_inv aag (NotificationControl t (Some ntfn)))\<rbrace> invoke_tcb (NotificationControl t (Some ntfn)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. authorised_tcb_inv aag (NotificationControl t (Some ntfn)) \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (NotificationControl t (Some ntfn))\<rbrace> invoke_tcb (NotificationControl t (Some ntfn)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. authorised_tcb_inv aag (NotificationControl t (Some ntfn)) \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and (tcb_at t and ex_nonz_cap_to t and (obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) ntfn and ex_nonz_cap_to ntfn and bound_tcb_at ((=) None) t))\<rbrace> liftE (do y <- bind_notification t ntfn;
return []
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>authorised_tcb_inv aag (NotificationControl t (Some ntfn)); (integrity aag X st and pas_refined aag and einvs and simple_sched_action and (tcb_at t and ex_nonz_cap_to t and (obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) ntfn and ex_nonz_cap_to ntfn and bound_tcb_at ((=) None) t))) s\<rbrakk> \<Longrightarrow> (integrity aag X st and pas_refined aag and bound_tcb_at ((=) None) t and K ((pasSubject aag, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> is_subject aag t)) s proof (prove)
goal:
No subgoals!
theory Tcb_AC

lemma invoke_tcb_ntfn_control_respects[wp]:
  "\<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action
                       and tcb_inv_wf (NotificationControl t ntfn)
                       and K (authorised_tcb_inv aag (NotificationControl t ntfn))\<rbrace>
   invoke_tcb (NotificationControl t ntfn)
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (case_tac ntfn, simp_all del: invoke_tcb.simps Tcb_AI.tcb_inv_wf.simps K_def) apply (wp invoke_tcb_bind_notification_respects invoke_tcb_unbind_notification_respects | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (NotificationControl t ntfn) and K (authorised_tcb_inv aag (NotificationControl t ntfn))\<rbrace> invoke_tcb (NotificationControl t ntfn) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. ntfn = None \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (NotificationControl t None) and K (authorised_tcb_inv aag (NotificationControl t None))\<rbrace> invoke_tcb (NotificationControl t None) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>a. ntfn = Some a \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (NotificationControl t (Some a)) and K (authorised_tcb_inv aag (NotificationControl t (Some a)))\<rbrace> invoke_tcb (NotificationControl t (Some a)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_AC

lemma hoare_st_refl:
  "\<lbrakk> \<And>st. \<lbrace>P st\<rbrace> f \<lbrace>Q st\<rbrace>; \<And>r s st. Q st r s \<Longrightarrow> Q' r s \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s s\<rbrace> f \<lbrace>Q'\<rbrace>" apply (clarsimp simp add: valid_def) apply (drule_tac x=s in meta_spec) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>st. \<lbrace>P st\<rbrace> f \<lbrace>Q st\<rbrace>; \<And>r s st. Q st r s \<Longrightarrow> Q' r s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s s\<rbrace> f \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>st. \<forall>s. P st s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (x, xa) \<Rightarrow> Q st x xa); \<And>r s st. Q st r s \<Longrightarrow> Q' r s; P s s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> Q' a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>r s st. Q st r s \<Longrightarrow> Q' r s; P s s; (a, b) \<in> fst (f s); \<forall>sa. P s sa \<longrightarrow> (\<forall>x\<in>fst (f sa). case x of (x, xa) \<Rightarrow> Q s x xa)\<rbrakk> \<Longrightarrow> Q' a b proof (prove)
goal:
No subgoals!
theory Tcb_AC

lemma decode_tcb_configure_authorised:
  "\<lbrace>K (is_subject aag t \<and> (\<forall>x \<in> set excaps. is_subject aag (fst (snd x)))
                        \<and> (\<forall>x \<in> set excaps. pas_cap_cur_auth aag (fst x)))\<rbrace>
   decode_tcb_configure msg (ThreadCap t) slot excaps
   \<lbrace>\<lambda>rv _ :: det_ext state. authorised_tcb_inv aag rv\<rbrace>, -" apply (wpsimp simp: decode_tcb_configure_def
                wp: whenE_throwError_wp decode_tcb_configure_authorised_helper
                    decode_set_ipc_buffer_authorised) apply (auto dest: in_set_takeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)))\<rbrace> decode_tcb_configure msg (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag t; \<forall>x\<in>set excaps. is_subject aag (fst (snd x)); \<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x); \<not> length msg < 4; \<not> length excaps < 3\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (take 2 excaps). is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set (take 2 excaps). pas_cap_cur_auth aag (fst x)) proof (prove)
goal:
No subgoals!
theory Tcb_AC

lemma decode_set_priority_authorised:
  "\<lbrace>K (is_subject aag t)\<rbrace>
   decode_set_priority msg (ThreadCap t) slot excs
   \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -" by (wpsimp simp: decode_set_priority_def check_prio_def authorised_tcb_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_subject aag t)\<rbrace> decode_set_priority msg (ThreadCap t) slot excs \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -
theory Tcb_AC

lemma decode_set_mcpriority_authorised:
  "\<lbrace>K (is_subject aag t)\<rbrace>
   decode_set_mcpriority msg (ThreadCap t) slot excs
   \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -" by (wpsimp simp: decode_set_mcpriority_def check_prio_def authorised_tcb_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_subject aag t)\<rbrace> decode_set_mcpriority msg (ThreadCap t) slot excs \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -
theory Tcb_AC

lemma decode_set_sched_params_authorised:
  "\<lbrace>K (is_subject aag t)\<rbrace>
   decode_set_sched_params msg (ThreadCap t) slot excs
   \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -" by (wpsimp simp: decode_set_sched_params_def check_prio_def authorised_tcb_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_subject aag t)\<rbrace> decode_set_sched_params msg (ThreadCap t) slot excs \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -
theory Tcb_AC

lemma decode_unbind_notification_authorised:
  "\<lbrace>K (is_subject aag t)\<rbrace>
   decode_unbind_notification (ThreadCap t)
   \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -" unfolding decode_unbind_notification_def authorised_tcb_inv_def apply clarsimp apply (wp gbn_wp, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_subject aag t)\<rbrace> decode_unbind_notification (ThreadCap t) \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_subject aag t)\<rbrace> case ThreadCap t of ThreadCap tcb \<Rightarrow> doE nTFN <- liftE $ get_bound_notification tcb;
case nTFN of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk ();
returnOk $ NotificationControl tcb None
odE | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>rv _. case rv of WriteRegisters dest res values arch \<Rightarrow> is_subject aag dest | ReadRegisters src susp n arch \<Rightarrow> is_subject aag src | CopyRegisters dest src susp res frame int_regs arch \<Rightarrow> is_subject aag src \<and> is_subject aag dest | ThreadControl t sl ep mcp priority croot vroot buf \<Rightarrow> is_subject aag t \<and> (\<forall>(cap, slot)\<in>set_option croot \<union> set_option vroot \<union> (case buf of None \<Rightarrow> {} | Some x \<Rightarrow> (set_option \<circ> snd) x). pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)) | Suspend t \<Rightarrow> is_subject aag t | Resume t \<Rightarrow> is_subject aag t | NotificationControl t ntfn \<Rightarrow> is_subject aag t \<and> (case ntfn of None \<Rightarrow> True | Some a \<Rightarrow> \<forall>auth\<in>{Receive, Reset}. (pasSubject aag, auth, pasObjectAbs aag a) \<in> pasPolicy aag) | SetTLSBase tcb tls_base \<Rightarrow> is_subject aag tcb\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>y. is_subject aag t\<rbrace> doE nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk ();
returnOk (NotificationControl t None)
odE \<lbrace>\<lambda>rv _. case rv of WriteRegisters dest res values arch \<Rightarrow> is_subject aag dest | ReadRegisters src susp n arch \<Rightarrow> is_subject aag src | CopyRegisters dest src susp res frame int_regs arch \<Rightarrow> is_subject aag src \<and> is_subject aag dest | ThreadControl t sl ep mcp priority croot vroot buf \<Rightarrow> is_subject aag t \<and> (\<forall>(cap, slot)\<in>set_option croot \<union> set_option vroot \<union> (case buf of None \<Rightarrow> {} | Some x \<Rightarrow> (set_option \<circ> snd) x). pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)) | Suspend t \<Rightarrow> is_subject aag t | Resume t \<Rightarrow> is_subject aag t | NotificationControl t ntfn \<Rightarrow> is_subject aag t \<and> (case ntfn of None \<Rightarrow> True | Some a \<Rightarrow> \<forall>auth\<in>{Receive, Reset}. (pasSubject aag, auth, pasObjectAbs aag a) \<in> pasPolicy aag) | SetTLSBase tcb tls_base \<Rightarrow> is_subject aag tcb\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Tcb_AC

lemma decode_set_tls_base_authorised:
  "\<lbrace>K (is_subject aag t)\<rbrace>
   decode_set_tls_base msg (ThreadCap t)
   \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -" unfolding decode_set_tls_base_def authorised_tcb_inv_def apply clarsimp apply (wpsimp wp: gbn_wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_subject aag t)\<rbrace> decode_set_tls_base msg (ThreadCap t) \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_subject aag t)\<rbrace> doE whenE (length msg = 0) $ throwError TruncatedMessage;
returnOk (SetTLSBase (obj_ref_of (ThreadCap t)) (UCAST(32 \<rightarrow> 32) (msg ! 0)))
odE \<lbrace>\<lambda>rv _. case rv of WriteRegisters dest res values arch \<Rightarrow> is_subject aag dest | ReadRegisters src susp n arch \<Rightarrow> is_subject aag src | CopyRegisters dest src susp res frame int_regs arch \<Rightarrow> is_subject aag src \<and> is_subject aag dest | ThreadControl t sl ep mcp priority croot vroot buf \<Rightarrow> is_subject aag t \<and> (\<forall>(cap, slot)\<in>set_option croot \<union> set_option vroot \<union> (case buf of None \<Rightarrow> {} | Some x \<Rightarrow> (set_option \<circ> snd) x). pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)) | Suspend t \<Rightarrow> is_subject aag t | Resume t \<Rightarrow> is_subject aag t | NotificationControl t ntfn \<Rightarrow> is_subject aag t \<and> (case ntfn of None \<Rightarrow> True | Some a \<Rightarrow> \<forall>auth\<in>{Receive, Reset}. (pasSubject aag, auth, pasObjectAbs aag a) \<in> pasPolicy aag) | SetTLSBase tcb tls_base \<Rightarrow> is_subject aag tcb\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>y. is_subject aag t\<rbrace> doE y <- whenE (msg = []) (throwError TruncatedMessage);
returnOk (SetTLSBase t (msg ! 0))
odE \<lbrace>\<lambda>rv _. case rv of WriteRegisters dest res values arch \<Rightarrow> is_subject aag dest | ReadRegisters src susp n arch \<Rightarrow> is_subject aag src | CopyRegisters dest src susp res frame int_regs arch \<Rightarrow> is_subject aag src \<and> is_subject aag dest | ThreadControl t sl ep mcp priority croot vroot buf \<Rightarrow> is_subject aag t \<and> (\<forall>(cap, slot)\<in>set_option croot \<union> set_option vroot \<union> (case buf of None \<Rightarrow> {} | Some x \<Rightarrow> (set_option \<circ> snd) x). pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)) | Suspend t \<Rightarrow> is_subject aag t | Resume t \<Rightarrow> is_subject aag t | NotificationControl t ntfn \<Rightarrow> is_subject aag t \<and> (case ntfn of None \<Rightarrow> True | Some a \<Rightarrow> \<forall>auth\<in>{Receive, Reset}. (pasSubject aag, auth, pasObjectAbs aag a) \<in> pasPolicy aag) | SetTLSBase tcb tls_base \<Rightarrow> is_subject aag tcb\<rbrace>, - proof (prove)
goal:
No subgoals!
theory ArchTcb_AC

lemma arch_post_modify_registers_respects[Tcb_AC_assms]:
  "\<lbrace>integrity aag X st and K (is_subject aag t)\<rbrace>
   arch_post_modify_registers cur t
   \<lbrace>\<lambda>_ s. integrity aag X st s\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag t)\<rbrace> arch_post_modify_registers cur t \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory Interrupt_AC

lemma emptyable_irq_node:
  "emptyable (interrupt_irq_node s x21, []) s" by (simp add:emptyable_def tcb_cnode_index_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. emptyable (interrupt_irq_node s x21, []) s
theory Interrupt_AC

lemma pas_refined_is_subject_irqD:
  "\<lbrakk> is_subject_irq aag irq; pas_refined aag s \<rbrakk> \<Longrightarrow> is_subject aag (interrupt_irq_node s irq)" by (simp add:pas_refined_def irq_map_wellformed_aux_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject_irq aag irq; pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject aag (interrupt_irq_node s irq)
theory Interrupt_AC

lemma invoke_irq_handler_respects:
  "\<lbrace>integrity (aag :: 'a PAS) X st and pas_refined aag and einvs
                                   and K (authorised_irq_hdl_inv aag irq_inv)\<rbrace>
   invoke_irq_handler irq_inv
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (cases irq_inv, simp_all add: authorised_irq_hdl_inv_def) by (wpsimp wp: arch_invoke_irq_handler_respects cap_insert_integrity_autarch)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and einvs and K (authorised_irq_hdl_inv aag irq_inv)\<rbrace> invoke_irq_handler irq_inv \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x1. irq_inv = ACKIrq x1 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs\<rbrace> arch_invoke_irq_handler (ACKIrq x1) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>x21 x22 x23. irq_inv = SetIRQHandler x21 x22 x23 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and (\<lambda>y. is_subject aag (fst x23) \<and> pas_cap_cur_auth aag x22 \<and> is_subject_irq aag x21)\<rbrace> do irq_slot <- get_irq_slot x21;
y <- cap_delete_one irq_slot;
cap_insert x22 x23 irq_slot
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and (\<lambda>y. is_subject_irq aag x3)\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory ArchInterrupt_AC

lemma arch_invoke_irq_control_pas_refined[Interrupt_AC_assms]:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
                    and valid_mdb and arch_irq_control_inv_valid irq_ctl_inv
                    and K (arch_authorised_irq_ctl_inv aag irq_ctl_inv)\<rbrace>
   arch_invoke_irq_control irq_ctl_inv
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (cases irq_ctl_inv; simp) apply (wpsimp wp: cap_insert_pas_refined_not_transferable) apply (clarsimp simp: cte_wp_at_caps_of_state clas_no_asid cap_links_irq_def
                        arch_authorised_irq_ctl_inv_def aag_cap_auth_def
                        arch_irq_control_inv_valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and arch_irq_control_inv_valid irq_ctl_inv and K (arch_authorised_irq_ctl_inv aag irq_ctl_inv)\<rbrace> arch_invoke_irq_control irq_ctl_inv \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. irq_ctl_inv = ArchIRQControlIssue x1 x2 x3 x4 \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and arch_irq_control_inv_valid (ArchIRQControlIssue x1 x2 x3 x4) and (\<lambda>y. arch_authorised_irq_ctl_inv aag (ArchIRQControlIssue x1 x2 x3 x4))\<rbrace> liftE (do y <- do_machine_op (setIRQTrigger x1 x4);
y <- set_irq_state IRQSignal x1;
cap_insert (IRQHandlerCap x1) x3 x2
od) \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4 s. \<lbrakk>irq_ctl_inv = ArchIRQControlIssue x1 (a, b) (aa, ba) x4; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; arch_irq_control_inv_valid (ArchIRQControlIssue x1 (a, b) (aa, ba) x4) s; arch_authorised_irq_ctl_inv aag (ArchIRQControlIssue x1 (a, b) (aa, ba) x4)\<rbrakk> \<Longrightarrow> \<not> cte_wp_at is_transferable_cap (aa, ba) s \<and> is_subject aag a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag (IRQHandlerCap x1) proof (prove)
goal:
No subgoals!