kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchDomainSepInv

lemma perform_asid_control_invocation_domain_sep_inv:
  "perform_asid_control_invocation iv \<lbrace>domain_sep_inv irqs st\<rbrace>" unfolding perform_asid_control_invocation_def apply (rule hoare_pre) apply (wp modify_wp cap_insert_domain_sep_inv' set_cap_domain_sep_inv
            get_cap_domain_sep_inv_cap[where st=st] hoare_weak_lift_imp
         | wpc | simp )+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> perform_asid_control_invocation iv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> case iv of MakePool frame slot parent base \<Rightarrow> do delete_objects frame page_bits;
pcap <- get_cap parent;
set_cap (max_free_index_update pcap) parent;
retype_region frame 1 0 (ArchObject ASIDPoolObj) False;
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot;
assert (base && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of base \<mapsto> frame));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case iv of MakePool frame slot parent base \<Rightarrow> do delete_objects frame page_bits;
pcap <- get_cap parent;
set_cap (max_free_index_update pcap) parent;
retype_region frame 1 0 (ArchObject ASIDPoolObj) False;
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot;
assert (base && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of base \<mapsto> frame));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>s. domain_sep_inv irqs st s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchDomainSepInv

lemma perform_asid_pool_invocation_domain_sep_inv:
  "perform_asid_pool_invocation iv \<lbrace>domain_sep_inv irqs st\<rbrace>" apply (simp add: perform_asid_pool_invocation_def) apply (rule hoare_pre) apply (wp set_cap_domain_sep_inv get_cap_wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> perform_asid_pool_invocation iv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> case iv of Assign asid pool_ptr ct_slot \<Rightarrow> do pd_cap <- get_cap ct_slot;
case pd_cap of ArchObjectCap (PageDirectoryCap pd_base x) \<Rightarrow> do pool <- get_asid_pool pool_ptr;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid \<mapsto> pd_base));
set_cap (ArchObjectCap $ PageDirectoryCap pd_base (Some asid)) ct_slot;
set_asid_pool pool_ptr pool'
od | ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case iv of Assign asid pool_ptr ct_slot \<Rightarrow> do pd_cap <- get_cap ct_slot;
case pd_cap of ArchObjectCap (PageDirectoryCap pd_base x) \<Rightarrow> do pool <- get_asid_pool pool_ptr;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid \<mapsto> pd_base));
set_cap (ArchObjectCap $ PageDirectoryCap pd_base (Some asid)) ct_slot;
set_asid_pool pool_ptr pool'
od | ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>s. domain_sep_inv irqs st s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchDomainSepInv

lemma arch_perform_invocation_domain_sep_inv[DomainSepInv_assms]:
  "\<lbrace>domain_sep_inv irqs st and valid_arch_inv ai\<rbrace>
   arch_perform_invocation ai
   \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" unfolding arch_perform_invocation_def apply (wpsimp wp: perform_page_table_invocation_domain_sep_inv
                    perform_page_directory_invocation_domain_sep_inv
                    perform_page_invocation_domain_sep_inv
                    perform_asid_control_invocation_domain_sep_inv
                    perform_asid_pool_invocation_domain_sep_inv) apply (clarsimp simp: valid_arch_inv_def split: arch_invocation.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and valid_arch_inv ai\<rbrace> arch_perform_invocation ai \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and valid_arch_inv ai\<rbrace> liftE $ case ai of InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | InvokePage oper \<Rightarrow> perform_page_invocation oper | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>domain_sep_inv irqs st s; valid_arch_inv ai s\<rbrakk> \<Longrightarrow> (\<forall>x. ai = InvokePageTable x \<longrightarrow> valid_pti x s) \<and> (\<forall>x. ai = InvokePage x \<longrightarrow> valid_page_inv x s) proof (prove)
goal:
No subgoals!
theory ArchDomainSepInv

lemma arch_invoke_irq_handler_domain_sep_inv[DomainSepInv_assms, wp]:
  "arch_invoke_irq_handler ihi \<lbrace>domain_sep_inv irqs st\<rbrace>" by (cases ihi; wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> arch_invoke_irq_handler ihi \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
theory ArchDomainSepInv

lemma arch_derive_cap_domain_sep_inv[DomainSepInv_assms, wp]:
  "\<lbrace>\<top>\<rbrace> arch_derive_cap acap \<lbrace>\<lambda>rv _. domain_sep_inv_cap irqs rv\<rbrace>,-" unfolding arch_derive_cap_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> arch_derive_cap acap \<lbrace>\<lambda>rv _. domain_sep_inv_cap irqs rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> case acap 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 acap) | PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap acap) | _ \<Rightarrow> returnOk (ArchObjectCap acap) \<lbrace>\<lambda>rv _. domain_sep_inv_cap irqs rv\<rbrace>, -
theory ArchDomainSepInv

lemma arch_post_modify_registers_domain_sep_inv[DomainSepInv_assms, wp]:
  "arch_post_modify_registers cur x31 \<lbrace>domain_sep_inv irqs st\<rbrace>" unfolding arch_post_modify_registers_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> arch_post_modify_registers cur x31 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> return () \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
theory Syscall_AC

lemma ntfn_gives_obj_at:
  "invs s
   \<Longrightarrow> (\<exists>ntfn. ko_at (Notification ntfn) ntfnptr s
             \<and> (\<forall>x\<in>ntfn_q_refs_of (ntfn_obj ntfn).
                  (\<lambda>(t, rt). obj_at (\<lambda>tcb. ko_at tcb t s) t s) x)) = ntfn_at ntfnptr s" apply (rule iffI) apply (clarsimp simp: obj_at_def is_ntfn) apply (clarsimp simp: obj_at_def is_ntfn) apply (drule (1) ntfn_queued_st_tcb_at [where P = \<top>, unfolded obj_at_def, simplified]) apply clarsimp apply clarsimp apply (clarsimp simp: st_tcb_def2 dest!: get_tcb_SomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> (\<exists>ntfn. ko_at (Notification ntfn) ntfnptr s \<and> (\<forall>x\<in>ntfn_q_refs_of (ntfn_obj ntfn). case x of (t, rt) \<Rightarrow> obj_at (\<lambda>tcb. ko_at tcb t s) t s)) = ntfn_at ntfnptr s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; \<exists>ntfn. ko_at (Notification ntfn) ntfnptr s \<and> (\<forall>x\<in>ntfn_q_refs_of (ntfn_obj ntfn). case x of (t, rt) \<Rightarrow> obj_at (\<lambda>tcb. ko_at tcb t s) t s)\<rbrakk> \<Longrightarrow> ntfn_at ntfnptr s
 2. \<lbrakk>invs s; ntfn_at ntfnptr s\<rbrakk> \<Longrightarrow> \<exists>ntfn. ko_at (Notification ntfn) ntfnptr s \<and> (\<forall>x\<in>ntfn_q_refs_of (ntfn_obj ntfn). case x of (t, rt) \<Rightarrow> obj_at (\<lambda>tcb. ko_at tcb t s) t s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; ntfn_at ntfnptr s\<rbrakk> \<Longrightarrow> \<exists>ntfn. ko_at (Notification ntfn) ntfnptr s \<and> (\<forall>x\<in>ntfn_q_refs_of (ntfn_obj ntfn). case x of (t, rt) \<Rightarrow> obj_at (\<lambda>tcb. ko_at tcb t s) t s) proof (prove)
goal (1 subgoal):
 1. \<And>ep a b. \<lbrakk>invs s; kheap s ntfnptr = Some (Notification ep); (a, b) \<in> ntfn_q_refs_of (ntfn_obj ep)\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s a = Some ko proof (prove)
goal (3 subgoals):
 1. \<And>ep a b. \<lbrakk>invs s; (a, b) \<in> ntfn_q_refs_of (ntfn_obj ep)\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>ep a b. \<lbrakk>invs s; (a, b) \<in> ntfn_q_refs_of (ntfn_obj ep)\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 3. \<And>ep a b. \<lbrakk>invs s; (a, b) \<in> ntfn_q_refs_of (ntfn_obj ep); st_tcb_at (\<lambda>_. True) a s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s a = Some ko proof (prove)
goal (2 subgoals):
 1. \<And>ep a b. \<lbrakk>invs s; (a, b) \<in> ntfn_q_refs_of (ntfn_obj ep)\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 2. \<And>ep a b. \<lbrakk>invs s; (a, b) \<in> ntfn_q_refs_of (ntfn_obj ep); st_tcb_at (\<lambda>_. True) a s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s a = Some ko proof (prove)
goal (1 subgoal):
 1. \<And>ep a b. \<lbrakk>invs s; (a, b) \<in> ntfn_q_refs_of (ntfn_obj ep); st_tcb_at (\<lambda>_. True) a s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s a = Some ko proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma in_extended: "(u,a) \<in> fst (do_extended_op f s) \<Longrightarrow> \<exists>e. a = (trans_state (\<lambda>_. e) s)" by (fastforce simp: do_extended_op_def bind_def gets_def return_def get_def
                      mk_ef_def modify_def select_f_def put_def trans_state_update')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (u, a) \<in> fst (do_extended_op f s) \<Longrightarrow> \<exists>e. a = trans_state (\<lambda>_. e) s
theory Syscall_AC

lemma set_scheduler_action_authorised_arch_inv[wp]:
  "set_scheduler_action act \<lbrace>authorised_arch_inv aag i\<rbrace>" unfolding set_scheduler_action_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>authorised_arch_inv aag i\<rbrace> set_scheduler_action act \<lbrace>\<lambda>_. authorised_arch_inv aag i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>authorised_arch_inv aag i\<rbrace> modify (scheduler_action_update (\<lambda>_. act)) \<lbrace>\<lambda>_. authorised_arch_inv aag i\<rbrace>
theory Syscall_AC

lemma sts_first_restart:
  "\<lbrace>(=) st and (\<lambda>s. thread = cur_thread s)\<rbrace>
   set_thread_state thread Structures_A.thread_state.Restart
   \<lbrace>\<lambda>rv s. \<forall>p ko. kheap s p = Some ko \<longrightarrow>
           (is_tcb ko \<longrightarrow> p \<noteq> cur_thread st) \<longrightarrow> kheap st p = Some ko\<rbrace>" unfolding set_thread_state_def by (wpsimp wp: set_object_wp dxo_wp_weak simp: is_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) st and (\<lambda>s. thread = cur_thread s)\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>rv s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> (is_tcb ko \<longrightarrow> p \<noteq> cur_thread st) \<longrightarrow> kheap st p = Some ko\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) st and (\<lambda>s. thread = cur_thread s)\<rbrace> do tcb <- gets_the $ get_tcb thread;
set_object thread (TCB (tcb\<lparr>tcb_state := Restart\<rparr>));
do_extended_op (set_thread_state_ext thread)
od \<lbrace>\<lambda>rv s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> (is_tcb ko \<longrightarrow> p \<noteq> cur_thread st) \<longrightarrow> kheap st p = Some ko\<rbrace>
theory Syscall_AC

lemma lcs_reply_owns:
  "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
   lookup_cap_and_slot thread ptr
   \<lbrace>\<lambda>rv _. \<forall>ep. (\<exists>m R. fst rv = ReplyCap ep m R \<and> AllowGrant \<in> R) \<longrightarrow> is_subject aag ep\<rbrace>, -" apply (rule hoare_post_imp_R) apply (rule hoare_pre) apply (rule hoare_vcg_conj_lift_R [where S = "K (pas_refined aag)"]) apply (rule lookup_cap_and_slot_cur_auth) apply (simp | wp lookup_cap_and_slot_inv)+ apply (force simp: aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
               dest: aag_Control_into_owns) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> lookup_cap_and_slot thread ptr \<lbrace>\<lambda>rv _. \<forall>ep. (\<exists>m R. fst rv = ReplyCap ep m R \<and> AllowGrant \<in> R) \<longrightarrow> is_subject aag ep\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> lookup_cap_and_slot thread ptr \<lbrace>?Q'\<rbrace>, -
 2. \<And>rv s. ?Q' rv s \<Longrightarrow> \<forall>ep. (\<exists>m R. fst rv = ReplyCap ep m R \<and> AllowGrant \<in> R) \<longrightarrow> is_subject aag ep proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'3\<rbrace> lookup_cap_and_slot thread ptr \<lbrace>?Q'\<rbrace>, -
 2. \<And>s. (pas_refined aag and K (is_subject aag thread)) s \<Longrightarrow> ?P'3 s
 3. \<And>rv s. ?Q' rv s \<Longrightarrow> \<forall>ep. (\<exists>m R. fst rv = ReplyCap ep m R \<and> AllowGrant \<in> R) \<longrightarrow> is_subject aag ep proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P6\<rbrace> lookup_cap_and_slot thread ptr \<lbrace>?Q6\<rbrace>, -
 2. \<lbrace>?R6\<rbrace> lookup_cap_and_slot thread ptr \<lbrace>K (pas_refined aag)\<rbrace>, -
 3. \<And>s. (pas_refined aag and K (is_subject aag thread)) s \<Longrightarrow> ?P6 s \<and> ?R6 s
 4. \<And>rv s. ?Q6 rv s \<and> K (pas_refined aag) rv s \<Longrightarrow> \<forall>ep. (\<exists>m R. fst rv = ReplyCap ep m R \<and> AllowGrant \<in> R) \<longrightarrow> is_subject aag ep proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R6\<rbrace> lookup_cap_and_slot thread ptr \<lbrace>K (pas_refined aag)\<rbrace>, -
 2. \<And>s. (pas_refined aag and K (is_subject aag thread)) s \<Longrightarrow> (pas_refined ?aag9 and K (is_subject ?aag9 thread)) s \<and> ?R6 s
 3. \<And>rv s. pas_cap_cur_auth ?aag9 (fst rv) \<and> K (pas_refined aag) rv s \<Longrightarrow> \<forall>ep. (\<exists>m R. fst rv = ReplyCap ep m R \<and> AllowGrant \<in> R) \<longrightarrow> is_subject aag ep proof (prove)
goal (1 subgoal):
 1. \<And>rv s. pas_cap_cur_auth aag (fst rv) \<and> pas_refined aag s \<Longrightarrow> \<forall>ep. (\<exists>m R. fst rv = ReplyCap ep m R \<and> AllowGrant \<in> R) \<longrightarrow> is_subject aag ep proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma lookup_cap_and_slot_valid_fault3:
  "\<lbrace>valid_objs\<rbrace>
   lookup_cap_and_slot thread cptr
   -, \<lbrace>\<lambda>ft _. valid_fault (CapFault (of_bl cptr) rp ft)\<rbrace>" apply (unfold validE_E_def) apply (rule hoare_post_impErr) apply (rule lookup_cap_and_slot_valid_fault) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_cap_and_slot thread cptr -, \<lbrace>\<lambda>ft _. valid_fault (CapFault (of_bl cptr) rp ft)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_cap_and_slot thread cptr \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft _. valid_fault (CapFault (of_bl cptr) rp ft)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>valid_objs\<rbrace> lookup_cap_and_slot thread cptr \<lbrace>?Q\<rbrace>, \<lbrace>?E\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> True
 3. \<And>e s. ?E e s \<Longrightarrow> valid_fault (CapFault (of_bl cptr) rp e) proof (prove)
goal (2 subgoals):
 1. \<And>rv s. valid_objs s \<Longrightarrow> True
 2. \<And>e s. valid_fault (CapFault (of_bl cptr) ?rp4 e) \<Longrightarrow> valid_fault (CapFault (of_bl cptr) rp e) proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma guarded_pas_domain_lift:
  assumes a: "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>"
  assumes b: "\<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> f \<lbrace>\<lambda>r s. P (cur_domain s)\<rbrace>"
  assumes c: "\<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> f \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>"
  shows "\<lbrace>guarded_pas_domain aag\<rbrace> f \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace>" apply (simp add: guarded_pas_domain_def) apply (rule hoare_pre) apply (wps a b c) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>guarded_pas_domain aag\<rbrace> f \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s)\<rbrace> f \<lbrace>\<lambda>_ s. cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>\<lambda>_ s. cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s)\<rbrace>
 2. \<And>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> f \<lbrace>\<lambda>rv s'. cur_thread prev_s \<noteq> idle_thread prev_s \<longrightarrow> pasObjectAbs aag (cur_thread prev_s) \<in> pasDomainAbs aag (cur_domain prev_s)\<rbrace>
 2. \<And>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s) \<Longrightarrow> ?P3 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s) \<Longrightarrow> cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma guarded_to_cur_domain:
  "\<lbrakk> invs s; ct_in_state x s; \<not> x IdleThreadState;
     guarded_pas_domain aag s; is_subject aag (cur_thread s) \<rbrakk>
     \<Longrightarrow> pas_cur_domain aag s" by (auto simp: invs_def valid_state_def valid_idle_def pred_tcb_at_def
                 obj_at_def ct_in_state_def guarded_pas_domain_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; ct_in_state x s; \<not> x IdleThreadState; guarded_pas_domain aag s; is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> pas_cur_domain aag s
theory Syscall_AC

lemma sts_ct_in_state:
  "\<lbrace>\<lambda>s. t = cur_thread s \<and> P ts\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv. ct_in_state P\<rbrace>" unfolding ct_in_state_def apply (rule hoare_pre) apply wps apply (wpsimp wp: sts_st_tcb_at'') apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. t = cur_thread s \<and> P ts\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv. ct_in_state P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. t = cur_thread s \<and> P ts\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv s. st_tcb_at P (cur_thread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv s. st_tcb_at P (cur_thread s) s\<rbrace>
 2. \<And>s. t = cur_thread s \<and> P ts \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv. st_tcb_at P (cur_thread prev_s)\<rbrace>
 2. \<And>s. t = cur_thread s \<and> P ts \<Longrightarrow> ?P3 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. t = cur_thread s \<and> P ts \<Longrightarrow> K (t = cur_thread s \<and> P ts) s proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma handle_reply_pas_refined[wp]:
  "\<lbrace>pas_refined aag and invs and is_subject aag \<circ> cur_thread\<rbrace>
   handle_reply
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" unfolding handle_reply_def apply (rule hoare_pre) apply (wp do_reply_transfer_pas_refined get_cap_auth_wp [where aag = aag]| wpc)+ by (force simp: aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
           intro: aag_Control_into_owns)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and is_subject aag \<circ> cur_thread\<rbrace> handle_reply \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and is_subject aag \<circ> cur_thread\<rbrace> do thread <- gets cur_thread;
caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do thread <- gets cur_thread;
caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. (pas_refined aag and invs and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and invs and is_subject aag \<circ> cur_thread) s \<Longrightarrow> pas_refined aag s \<and> is_subject aag (fst (cur_thread s, tcb_cnode_index 3)) \<and> (\<forall>cap. caps_of_state s (cur_thread s, tcb_cnode_index 3) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> (cap = NullCap \<longrightarrow> pas_refined aag s) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (pas_refined aag and invs and K (is_subject aag (cur_thread s)) and K ((AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> is_subject aag (fst (cur_thread s, tcb_cnode_index 3)))) s)) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> True))
theory Syscall_AC

lemma thread_set_time_slice_pas_refined[wp]:
  "thread_set_time_slice tptr time \<lbrace>pas_refined aag\<rbrace>" by (simp add: thread_set_time_slice_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> thread_set_time_slice tptr time \<lbrace>\<lambda>_. pas_refined aag\<rbrace>