kings-crown/FVELER_Isabelle huggingface dataset:
theory Arch_AC

lemma as_user_state_vrefs:
  "\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace>
   as_user t f
   \<lbrace>\<lambda>_ s :: det_ext state. P (state_vrefs s)\<rbrace>" apply (simp add: as_user_def) apply (wpsimp wp: set_object_wp) apply (clarsimp simp: state_vrefs_tcb_upd obj_at_def is_obj_defs
                 elim!: rsubst[where P=P, OF _ ext]
                 dest!: get_tcb_SomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace> as_user t f \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace> do tcb <- gets_the (get_tcb t);
(a, uc') <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>));
return a
od \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa. \<lbrakk>pspace_aligned s; valid_vspace_objs s; valid_arch_state s; P (state_vrefs s); (x, xa) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); get_tcb t s = Some y\<rbrakk> \<Longrightarrow> P (state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>))\<rparr>)) proof (prove)
goal:
No subgoals!
theory Arch_AC

lemma set_mrs_thread_st_auth[wp]:
  "set_mrs thread buf msgs \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace>" supply if_split[split del] apply (simp add: set_mrs_def split_def set_object_def get_object_def) apply (wpsimp wp: gets_the_wp get_wp put_wp mapM_x_wp'
              simp: zipWithM_x_mapM_x split_def store_word_offs_def) apply (clarsimp simp: fun_upd_def[symmetric] thread_st_auth_preserved) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_ s. P (thread_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_ s. P (thread_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh thread = Some y);
return (the (kh thread))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>))\<rparr>)
od;
case buf of None \<Rightarrow> return (nat_to_len (min (length msg_registers) (length msgs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) (drop (length msg_registers) msgs);
return (nat_to_len (min (length msgs) msg_max_length))
od
od \<lbrace>\<lambda>_ s. P (thread_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>P (thread_st_auth s); get_tcb thread s = Some y; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> P (thread_st_auth (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch y) reg) (tcb_arch y)\<rparr>)) else kheap s a\<rparr>)) proof (prove)
goal:
No subgoals!
theory Arch_AC

lemma set_mrs_thread_bound_ntfns[wp]:
  "set_mrs thread buf msgs \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace>" supply if_split[split del] apply (simp add: set_mrs_def split_def set_object_def get_object_def ) apply (wpsimp wp: gets_the_wp get_wp put_wp mapM_x_wp' dmo_wp
              simp: zipWithM_x_mapM_x split_def store_word_offs_def no_irq_storeWord) apply (clarsimp simp: fun_upd_def[symmetric] thread_bound_ntfns_preserved) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_ s. P (thread_bound_ntfns s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_ s. P (thread_bound_ntfns s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh thread = Some y);
return (the (kh thread))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>))\<rparr>)
od;
case buf of None \<Rightarrow> return (nat_to_len (min (length msg_registers) (length msgs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) (drop (length msg_registers) msgs);
return (nat_to_len (min (length msgs) msg_max_length))
od
od \<lbrace>\<lambda>_ s. P (thread_bound_ntfns s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>P (thread_bound_ntfns s); get_tcb thread s = Some y; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> P (thread_bound_ntfns (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch y) reg) (tcb_arch y)\<rparr>)) else kheap s a\<rparr>)) proof (prove)
goal:
No subgoals!
theory Arch_AC

lemma delete_objects_pspace_no_overlap:
  "\<lbrace>pspace_aligned and valid_objs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s)\<rbrace>
   delete_objects ptr sz
   \<lbrace>\<lambda>_. pspace_no_overlap_range_cover ptr sz\<rbrace>" unfolding delete_objects_def do_machine_op_def apply (wp | simp add: split_def detype_machine_state_update_comm)+ apply (clarsimp) apply (rule pspace_no_overlap_detype) apply (auto dest: cte_wp_at_valid_objs_valid_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_objs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s)\<rbrace> delete_objects ptr sz \<lbrace>\<lambda>_. pspace_no_overlap (up_aligned_area ptr sz)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_objs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s)\<rbrace> do do ms <- gets machine_state;
(r, ms') <- select_f (freeMemory ptr sz ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od;
modify (detype {ptr..ptr + 2 ^ sz - 1})
od \<lbrace>\<lambda>_. pspace_no_overlap (up_aligned_area ptr sz)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned s \<and> valid_objs s \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s) \<Longrightarrow> (\<exists>b. ((), b) \<in> fst (freeMemory ptr sz (machine_state s))) \<longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) (detype {ptr..ptr + 2 ^ sz - 1} s) proof (prove)
goal (1 subgoal):
 1. \<And>s idx b. \<lbrakk>pspace_aligned s; valid_objs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s; ((), b) \<in> fst (freeMemory ptr sz (machine_state s))\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) (detype {ptr..ptr + 2 ^ sz - 1} s) proof (prove)
goal (3 subgoals):
 1. \<And>s idx b. \<lbrakk>pspace_aligned s; valid_objs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s; ((), b) \<in> fst (freeMemory ptr sz (machine_state s))\<rbrakk> \<Longrightarrow> s \<turnstile> UntypedCap (?dev20 s idx b) ptr sz (?idx20 s idx b)
 2. \<And>s idx b. \<lbrakk>pspace_aligned s; valid_objs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s; ((), b) \<in> fst (freeMemory ptr sz (machine_state s))\<rbrakk> \<Longrightarrow> pspace_aligned s
 3. \<And>s idx b. \<lbrakk>pspace_aligned s; valid_objs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s; ((), b) \<in> fst (freeMemory ptr sz (machine_state s))\<rbrakk> \<Longrightarrow> valid_objs s proof (prove)
goal:
No subgoals!
theory Arch_AC

lemma delete_objects_invs_ex:
  "\<lbrace>invs and ct_active and
    (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev ptr bits f)) slot s \<and>
                      descendants_range (UntypedCap dev ptr bits f) slot s)\<rbrace>
   delete_objects ptr bits
   \<lbrace>\<lambda>_. invs\<rbrace>" apply (clarsimp simp: valid_def) apply (erule use_valid) apply wp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev ptr bits f)) slot s \<and> descendants_range (UntypedCap dev ptr bits f) slot s)\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b a ba dev f. \<lbrakk>((), b) \<in> fst (delete_objects ptr bits s); invs s; ct_active s; cte_wp_at ((=) (UntypedCap dev ptr bits f)) (a, ba) s; descendants_range (UntypedCap dev ptr bits f) (a, ba) s\<rbrakk> \<Longrightarrow> invs b proof (prove)
goal (2 subgoals):
 1. \<And>s b a ba dev f. \<lbrakk>invs s; ct_active s; cte_wp_at ((=) (UntypedCap dev ptr bits f)) (a, ba) s; descendants_range (UntypedCap dev ptr bits f) (a, ba) s\<rbrakk> \<Longrightarrow> \<lbrace>?P16 s b a ba dev f\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>a. invs\<rbrace>
 2. \<And>s b a ba dev f. \<lbrakk>invs s; ct_active s; cte_wp_at ((=) (UntypedCap dev ptr bits f)) (a, ba) s; descendants_range (UntypedCap dev ptr bits f) (a, ba) s\<rbrakk> \<Longrightarrow> ?P16 s b a ba dev f s proof (prove)
goal (1 subgoal):
 1. \<And>s b a ba dev f. \<lbrakk>invs s; ct_active s; cte_wp_at ((=) (UntypedCap dev ptr bits f)) (a, ba) s; descendants_range (UntypedCap dev ptr bits f) (a, ba) s\<rbrakk> \<Longrightarrow> ((\<lambda>sa. \<exists>slot. cte_wp_at ((=) (UntypedCap (?dev20 s b a ba dev f) ptr bits (?f20 s b a ba dev f))) slot sa \<and> descendants_range (UntypedCap (?dev20 s b a ba dev f) ptr bits (?f20 s b a ba dev f)) slot sa) and invs and ct_active) s proof (prove)
goal:
No subgoals!
theory Arch_AC

lemma is_subject_asid_into_loas:
  "\<lbrakk> is_subject_asid aag asid; pas_refined aag s \<rbrakk>
     \<Longrightarrow> label_owns_asid_slot aag (pasSubject aag) asid" unfolding label_owns_asid_slot_def by (clarsimp simp: pas_refined_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject_asid aag asid; pas_refined aag s\<rbrakk> \<Longrightarrow> label_owns_asid_slot aag (pasSubject aag) asid proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject_asid aag asid; pas_refined aag s\<rbrakk> \<Longrightarrow> (pasSubject aag, Control, pasASIDAbs aag asid) \<in> pasPolicy aag
theory ArchArch_AC

lemma set_mrs_state_vrefs[Arch_AC_assms, wp]:
  "set_mrs thread buf msgs \<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace>" apply (simp add: set_mrs_def split_def set_object_def get_object_def split del: if_split) apply (wpsimp wp: gets_the_wp get_wp put_wp mapM_x_wp'
              simp: zipWithM_x_mapM_x split_def store_word_offs_def
         split_del: if_split) apply (auto simp: obj_at_def state_vrefs_def get_tcb_ko_at
             elim!: rsubst[where P=P, OF _ ext]
             split: if_split_asm simp: vs_refs_no_global_pts_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh thread = Some y);
return (the (kh thread))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>))\<rparr>)
od;
case buf of None \<Rightarrow> return (word_of_nat (min (length msg_registers) (length msgs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) (drop (length msg_registers) msgs);
return (word_of_nat (min (length msgs) msg_max_length))
od
od \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>P (state_vrefs s); get_tcb thread s = Some y; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> P (state_vrefs (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch y) reg) (tcb_arch y)\<rparr>)) else kheap s a\<rparr>)) proof (prove)
goal:
No subgoals!
theory ArchArch_AC

lemma mul_add_word_size_lt_msg_align_bits_ofnat[Arch_AC_assms]:
  "\<lbrakk> p < 2 ^ (msg_align_bits - word_size_bits); k < word_size \<rbrakk>
     \<Longrightarrow> of_nat p * of_nat word_size + k < (2 :: obj_ref) ^ msg_align_bits" apply (rule is_aligned_add_less_t2n[where n=word_size_bits]) apply (simp_all add: msg_align_bits' word_size_word_size_bits is_aligned_mult_triv2) apply (simp_all add: word_size_def word_size_bits_def) apply (erule word_less_power_trans_ofnat[where k=2 and m=9, simplified], simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < 2 ^ (msg_align_bits - word_size_bits); k < word_size\<rbrakk> \<Longrightarrow> word_of_nat p * word_of_nat word_size + k < 2 ^ msg_align_bits proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p < 2 ^ (msg_align_bits - word_size_bits); k < word_size\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat p * word_of_nat word_size) word_size_bits
 2. \<lbrakk>p < 2 ^ (msg_align_bits - word_size_bits); k < word_size\<rbrakk> \<Longrightarrow> k < 2 ^ word_size_bits
 3. \<lbrakk>p < 2 ^ (msg_align_bits - word_size_bits); k < word_size\<rbrakk> \<Longrightarrow> word_size_bits \<le> msg_align_bits
 4. \<lbrakk>p < 2 ^ (msg_align_bits - word_size_bits); k < word_size\<rbrakk> \<Longrightarrow> word_of_nat p * word_of_nat word_size < 2 ^ msg_align_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < 128; k < 2 ^ word_size_bits\<rbrakk> \<Longrightarrow> word_of_nat p * 2 ^ word_size_bits < 2 ^ (word_size_bits + 7) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < 128; k < 4\<rbrakk> \<Longrightarrow> word_of_nat p * 4 < 0x200 proof (prove)
goal:
No subgoals!
theory ArchArch_AC

lemma zero_less_word_size[Arch_AC_assms, simp]:
    "0 < (word_size :: obj_ref)" by (simp add: word_size_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < word_size
theory ArchArch_AC

lemma store_pte_respects:
  "\<lbrace>integrity aag X st and K (is_subject aag (p && ~~ mask pt_bits))\<rbrace>
   store_pte p pte
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: store_pte_def set_pt_def) apply (wp get_object_wp set_object_integrity_autarch) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag (p && ~~ mask pt_bits))\<rbrace> store_pte p pte \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag (p && ~~ mask pt_bits))\<rbrace> do pt <- get_pt (p && ~~ mask pt_bits);
set_object (p && ~~ mask pt_bits) (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and (\<lambda>y. is_subject aag (p && ~~ mask pt_bits))) s \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> (integrity aag X st and K (is_subject aag (p && ~~ mask pt_bits))) s proof (prove)
goal:
No subgoals!
theory ArchArch_AC

lemma integrity_arch_state [iff]:
  "arm_asid_table v = arm_asid_table (arch_state s)
   \<Longrightarrow> integrity aag X st (s\<lparr>arch_state := v\<rparr>) = integrity aag X st s" unfolding integrity_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_asid_table v = asid_table s \<Longrightarrow> integrity aag X st (s\<lparr>arch_state := v\<rparr>) = integrity aag X st s proof (prove)
goal (1 subgoal):
 1. arm_asid_table v = asid_table s \<Longrightarrow> (integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st (s\<lparr>arch_state := v\<rparr>) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap (s\<lparr>arch_state := v\<rparr>) x)) \<and> integrity_cdt_state aag {pasSubject aag} st (s\<lparr>arch_state := v\<rparr>) \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list (s\<lparr>arch_state := v\<rparr>) x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node (s\<lparr>arch_state := v\<rparr>) x, interrupt_states (s\<lparr>arch_state := v\<rparr>) x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues (s\<lparr>arch_state := v\<rparr>) d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>arch_state := v\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state (s\<lparr>arch_state := v\<rparr>)) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>arch_state := v\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state (s\<lparr>arch_state := v\<rparr>)) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>arch_state := v\<rparr>))) = (integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> integrity_cdt_state aag {pasSubject aag} st s \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list s x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st s))
theory ArchArch_AC

lemma kheap_eq_state_vrefsD:
  "kheap s p = Some ko \<Longrightarrow> state_vrefs s p = vs_refs_no_global_pts ko" by (simp add: state_vrefs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s p = Some ko \<Longrightarrow> state_vrefs s p = vs_refs_no_global_pts ko
theory ArchArch_AC

lemma kheap_eq_state_vrefs_pas_refinedD:
  "\<lbrakk> kheap s p = Some ko; (p', r, t, a) \<in> vs_refs_no_global_pts ko; pas_refined aag s \<rbrakk>
     \<Longrightarrow> abs_has_auth_to aag a p p'" apply (drule kheap_eq_state_vrefsD) apply (erule pas_refined_mem[OF sta_vref, rotated]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some ko; (p', r, t, a) \<in> vs_refs_no_global_pts ko; pas_refined aag s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag p, a, pasObjectAbs aag p') \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(p', r, t, a) \<in> vs_refs_no_global_pts ko; pas_refined aag s; state_vrefs s p = vs_refs_no_global_pts ko\<rbrakk> \<Longrightarrow> (pasObjectAbs aag p, a, pasObjectAbs aag p') \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(p', r, t, a) \<in> vs_refs_no_global_pts ko; state_vrefs s p = vs_refs_no_global_pts ko\<rbrakk> \<Longrightarrow> (p', ?uu3, ?uv3, a) \<in> state_vrefs s p proof (prove)
goal:
No subgoals!
theory ArchArch_AC

lemma find_pd_for_asid_authority2:
  "\<lbrace>\<lambda>s. \<forall>pd. (\<forall>aag. pas_refined aag s
                    \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag pd) \<in> pasPolicy aag) \<and>
             (pspace_aligned s \<and> valid_vspace_objs s \<longrightarrow> is_aligned pd pd_bits) \<and>
             (\<exists>\<rhd> pd) s
             \<longrightarrow> Q pd s\<rbrace>
   find_pd_for_asid asid
   \<lbrace>Q\<rbrace>, -" (is "\<lbrace>?P\<rbrace> ?f \<lbrace>Q\<rbrace>,-") apply (clarsimp simp: validE_R_def validE_def valid_def imp_conjL[symmetric]) apply (frule in_inv_by_hoareD[OF find_pd_for_asid_inv], clarsimp) apply (drule spec, erule mp) apply (simp add: use_validE_R[OF _ find_pd_for_asid_authority1]
                   use_validE_R[OF _ find_pd_for_asid_aligned_pd_bits]
                   use_validE_R[OF _ find_pd_for_asid_lookup]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pd. (\<forall>aag. pas_refined aag s \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag pd) \<in> pasPolicy aag) \<and> (pspace_aligned s \<and> valid_vspace_objs s \<longrightarrow> is_aligned pd pd_bits) \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> Q pd s\<rbrace> find_pd_for_asid asid \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s b r. \<lbrakk>\<forall>pd. (\<forall>aag. pas_refined aag s \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag pd) \<in> pasPolicy aag) \<and> (pspace_aligned s \<and> valid_vspace_objs s \<longrightarrow> is_aligned pd pd_bits) \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> Q pd s; (Inr r, b) \<in> fst (find_pd_for_asid asid s)\<rbrakk> \<Longrightarrow> Q r b proof (prove)
goal (1 subgoal):
 1. \<And>s r. \<lbrakk>\<forall>pd. (\<forall>aag. pas_refined aag s \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag pd) \<in> pasPolicy aag) \<and> (pspace_aligned s \<and> valid_vspace_objs s \<longrightarrow> is_aligned pd pd_bits) \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> Q pd s; (Inr r, s) \<in> fst (find_pd_for_asid asid s)\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>s r. (Inr r, s) \<in> fst (find_pd_for_asid asid s) \<Longrightarrow> (\<forall>aag. pas_refined aag s \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag r) \<in> pasPolicy aag) \<and> (pspace_aligned s \<and> valid_vspace_objs s \<longrightarrow> is_aligned r pd_bits) \<and> (\<exists>ref. (ref \<rhd> r) s) proof (prove)
goal:
No subgoals!