kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchCNode_AC

lemma set_asid_pool_thread_st_auth[wp]:
  "set_asid_pool p pool \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace>" apply (simp add: set_asid_pool_def) apply (wpsimp wp: set_object_wp_strong) apply (clarsimp simp: thread_st_auth_def obj_at_def get_tcb_def tcb_states_of_state_def
                 elim!: rsubst[where P=P, OF _ ext]
                 split: kernel_object.split_asm option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace> set_asid_pool p pool \<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_object p (ArchObj (ASIDPool pool)) \<lbrace>\<lambda>_ s. P (thread_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>P (thread_st_auth s); ko_at ko p s; a_type (ArchObj (ASIDPool pool)) = a_type ko\<rbrakk> \<Longrightarrow> P (thread_st_auth (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool pool))\<rparr>)) proof (prove)
goal:
No subgoals!
theory ArchCNode_AC

lemma set_asid_pool_thread_bound_ntfns[wp]:
  "set_asid_pool p pool \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace>" apply (simp add: set_asid_pool_def) apply (wpsimp wp: set_object_wp_strong) apply (clarsimp simp: thread_bound_ntfns_def obj_at_def get_tcb_def tcb_states_of_state_def
                 elim!: rsubst[where P=P, OF _ ext]
                 split: kernel_object.split_asm option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> set_asid_pool p pool \<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_object p (ArchObj (ASIDPool pool)) \<lbrace>\<lambda>_ s. P (thread_bound_ntfns s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>P (thread_bound_ntfns s); ko_at ko p s; a_type (ArchObj (ASIDPool pool)) = a_type ko\<rbrakk> \<Longrightarrow> P (thread_bound_ntfns (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool pool))\<rparr>)) proof (prove)
goal:
No subgoals!
theory ArchCNode_AC

lemma set_asid_pool_ekheap[wp]:
  "set_asid_pool p pool \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>" apply (simp add: set_asid_pool_def) apply (wp get_object_wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> set_asid_pool p pool \<lbrace>\<lambda>_ s. P (ekheap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> set_object p (ArchObj (ASIDPool pool)) \<lbrace>\<lambda>_ s. P (ekheap s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchCNode_AC

lemma pas_refined_clear_asid:
  "pas_refined aag s
   \<Longrightarrow> pas_refined aag (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid then None
                                                                           else asid_table s a\<rparr>\<rparr>)" by (fastforce simp: pas_refined_def state_objs_to_policy_def
               intro: state_asids_to_policy_aux.intros
               elim!: state_asids_to_policy_aux.cases
               split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag s \<Longrightarrow> pas_refined aag (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid then None else asid_table s a\<rparr>\<rparr>)
theory Retype_AC

lemma ptr_range_memI:
  "is_aligned p n \<Longrightarrow> p \<in> ptr_range p n" unfolding ptr_range_def apply (erule is_aligned_get_word_bits) apply (drule (1) base_member_set) apply (simp add: field_simps) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p n \<Longrightarrow> p \<in> ptr_range p n proof (prove)
goal (1 subgoal):
 1. is_aligned p n \<Longrightarrow> p \<in> {p..p + 2 ^ n - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> p \<in> {p..p + 2 ^ n - 1}
 2. \<lbrakk>p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p \<in> {p..p + 2 ^ n - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); p \<in> {p..p + (2 ^ n - 1)}\<rbrakk> \<Longrightarrow> p \<in> {p..p + 2 ^ n - 1}
 2. \<lbrakk>p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p \<in> {p..p + 2 ^ n - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p \<in> {p..p + 2 ^ n - 1} proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma ptr_range_add_memI:
  "\<lbrakk> is_aligned (p :: 'a :: len word) n; k < 2 ^ n \<rbrakk> \<Longrightarrow> (p + k) \<in> ptr_range p n" unfolding ptr_range_def apply (erule is_aligned_get_word_bits) apply clarsimp apply (rule conjI) apply (erule (1) is_aligned_no_wrap') apply (subst p_assoc_help, rule word_plus_mono_right) apply simp apply (erule is_aligned_no_overflow') apply (subgoal_tac "2 ^ n = (0 :: 'a word)") apply simp apply (simp add: word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; k < 2 ^ n\<rbrakk> \<Longrightarrow> p + k \<in> ptr_range p n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; k < 2 ^ n\<rbrakk> \<Longrightarrow> p + k \<in> {p..p + 2 ^ n - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>k < 2 ^ n; is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> p + k \<in> {p..p + 2 ^ n - 1}
 2. \<lbrakk>k < 2 ^ n; p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p + k \<in> {p..p + 2 ^ n - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>k < 2 ^ n; is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> p \<le> p + k \<and> p + k \<le> p + 2 ^ n - 1
 2. \<lbrakk>k < 2 ^ n; p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p + k \<in> {p..p + 2 ^ n - 1} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>k < 2 ^ n; is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> p \<le> p + k
 2. \<lbrakk>k < 2 ^ n; is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> p + k \<le> p + 2 ^ n - 1
 3. \<lbrakk>k < 2 ^ n; p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p + k \<in> {p..p + 2 ^ n - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>k < 2 ^ n; is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> p + k \<le> p + 2 ^ n - 1
 2. \<lbrakk>k < 2 ^ n; p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p + k \<in> {p..p + 2 ^ n - 1} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>k < 2 ^ n; is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> k \<le> 2 ^ n - 1
 2. \<lbrakk>k < 2 ^ n; is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> p \<le> p + (2 ^ n - 1)
 3. \<lbrakk>k < 2 ^ n; p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p + k \<in> {p..p + 2 ^ n - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>k < 2 ^ n; is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> p \<le> p + (2 ^ n - 1)
 2. \<lbrakk>k < 2 ^ n; p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p + k \<in> {p..p + 2 ^ n - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k < 2 ^ n; p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p + k \<in> {p..p + 2 ^ n - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>k < 2 ^ n; p = 0; LENGTH('a) \<le> n; 2 ^ n = 0\<rbrakk> \<Longrightarrow> p + k \<in> {p..p + 2 ^ n - 1}
 2. \<lbrakk>k < 2 ^ n; p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> 2 ^ n = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k < 2 ^ n; p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> 2 ^ n = 0 proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma mol_respects:
  "machine_op_lift mop \<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace>" unfolding machine_op_lift_def apply (simp add: machine_rest_lift_def split_def) apply wp apply (clarsimp simp: integrity_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> machine_op_lift mop \<lbrace>\<lambda>_ ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> (machine_rest_lift \<circ> ignore_failure) mop \<lbrace>\<lambda>_ ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> do mr <- gets machine_state_rest;
p <- select_f (ignore_failure mop mr);
modify (machine_state_rest_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>_ ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. integrity aag X st (s\<lparr>machine_state := sa\<rparr>) \<Longrightarrow> \<forall>x\<in>fst (ignore_failure mop (machine_state_rest sa)). integrity aag X st (s\<lparr>machine_state := sa\<lparr>machine_state_rest := snd x\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma dmo_mol_respects[wp]:
  "do_machine_op (machine_op_lift mop) \<lbrace>integrity aag X st\<rbrace>" unfolding do_machine_op_def apply wpsimp apply (erule use_valid) apply (wp mol_respects) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> do_machine_op (machine_op_lift mop) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (machine_op_lift mop ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>integrity aag X st s; ((), x) \<in> fst (machine_op_lift mop (machine_state s))\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x. integrity aag X st s \<Longrightarrow> \<lbrace>?P32 s x\<rbrace> machine_op_lift mop \<lbrace>\<lambda>a b. integrity aag X st (s\<lparr>machine_state := b\<rparr>)\<rbrace>
 2. \<And>s x. integrity aag X st s \<Longrightarrow> ?P32 s x (machine_state s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. integrity aag X st s \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<rparr>) proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma dmo_bind_valid:
  "\<lbrace>P\<rbrace> do_machine_op (a >>= b) \<lbrace>Q\<rbrace> =
   \<lbrace>P\<rbrace> do_machine_op a >>= (\<lambda>rv. do_machine_op (b rv)) \<lbrace>Q\<rbrace>" by (fastforce simp: do_machine_op_def gets_def get_def select_f_def
                      modify_def put_def return_def bind_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do_machine_op (a >>= b) \<lbrace>Q\<rbrace> = \<lbrace>P\<rbrace> do rv <- do_machine_op a;
do_machine_op (b rv)
od \<lbrace>Q\<rbrace>
theory Retype_AC

lemma dmo_bind_valid':
  "\<lbrace>P\<rbrace> a >>= (\<lambda>rv. do_machine_op (b rv >>= c rv)) \<lbrace>Q\<rbrace> =
   \<lbrace>P\<rbrace> a >>= (\<lambda>rv. do_machine_op (b rv) >>= (\<lambda>rv'. do_machine_op (c rv rv'))) \<lbrace>Q\<rbrace>" by (fastforce simp: do_machine_op_def gets_def get_def select_f_def
                      modify_def put_def return_def bind_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do rv <- a;
do_machine_op (b rv >>= c rv)
od \<lbrace>Q\<rbrace> = \<lbrace>P\<rbrace> do rv <- a;
rv' <- do_machine_op (b rv);
do_machine_op (c rv rv')
od \<lbrace>Q\<rbrace>
theory Retype_AC

lemma dmo_mapM_wp:
  assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (f x) \<lbrace>\<lambda>rv. P\<rbrace>"
  shows "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (mapM f xs) \<lbrace>\<lambda>rv. P\<rbrace>" apply (induct xs) apply (simp add: mapM_def sequence_def) apply (simp add: mapM_Cons dmo_bind_valid dmo_bind_valid') apply (wpsimp | rule x)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (mapM f xs) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. set [] \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (mapM f []) \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>a xs. \<lbrakk>set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (mapM f xs) \<lbrace>\<lambda>rv. P\<rbrace>; set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (mapM f (a # xs)) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (mapM f xs) \<lbrace>\<lambda>rv. P\<rbrace>; set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (mapM f (a # xs)) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrace>P\<rbrace> do_machine_op (mapM f xs) \<lbrace>\<lambda>rv. P\<rbrace>; a \<in> S \<and> set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> do rv <- do_machine_op (f a);
rv' <- do_machine_op (mapM f xs);
return (rv # rv')
od \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma dmo_mapM_x_wp:
  assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (f x) \<lbrace>\<lambda>rv. P\<rbrace>"
  shows "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (mapM_x f xs) \<lbrace>\<lambda>rv. P\<rbrace>" apply (subst mapM_x_mapM) apply (simp add: do_machine_op_return_foo) apply wp apply (rule dmo_mapM_wp) apply (rule x) apply assumption+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (mapM_x f xs) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (do x <- mapM f xs;
return ()
od) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> do y <- do_machine_op (mapM f xs);
return ()
od \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. set xs \<subseteq> S \<Longrightarrow> \<lbrace>?Q\<rbrace> do_machine_op (mapM f xs) \<lbrace>\<lambda>y. P\<rbrace>
 2. \<And>s. \<lbrakk>set xs \<subseteq> S; P s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>set xs \<subseteq> S; x \<in> ?S3\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (f x) \<lbrace>\<lambda>y. P\<rbrace>
 2. set xs \<subseteq> S \<Longrightarrow> set xs \<subseteq> ?S3
 3. \<And>s. \<lbrakk>set xs \<subseteq> S; P s\<rbrakk> \<Longrightarrow> P s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>set xs \<subseteq> S; x \<in> ?S3\<rbrakk> \<Longrightarrow> x \<in> S
 2. set xs \<subseteq> S \<Longrightarrow> set xs \<subseteq> ?S3
 3. \<And>s. \<lbrakk>set xs \<subseteq> S; P s\<rbrakk> \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma foldr_upd_app_if':
  "foldr (\<lambda>p ps. ps(p := f p)) as g = (\<lambda>x. if x \<in> set as then (f x) else g x)" apply (induct as) apply simp apply simp apply (rule ext) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>p ps. ps(p := f p)) as g = (\<lambda>x. if x \<in> set as then f x else g x) proof (prove)
goal (2 subgoals):
 1. foldr (\<lambda>p ps. ps(p := f p)) [] g = (\<lambda>x. if x \<in> set [] then f x else g x)
 2. \<And>a as. foldr (\<lambda>p ps. ps(p := f p)) as g = (\<lambda>x. if x \<in> set as then f x else g x) \<Longrightarrow> foldr (\<lambda>p ps. ps(p := f p)) (a # as) g = (\<lambda>x. if x \<in> set (a # as) then f x else g x) proof (prove)
goal (1 subgoal):
 1. \<And>a as. foldr (\<lambda>p ps. ps(p := f p)) as g = (\<lambda>x. if x \<in> set as then f x else g x) \<Longrightarrow> foldr (\<lambda>p ps. ps(p := f p)) (a # as) g = (\<lambda>x. if x \<in> set (a # as) then f x else g x) proof (prove)
goal (1 subgoal):
 1. \<And>a as. foldr (\<lambda>p ps a. if a = p then f p else ps a) as g = (\<lambda>x. if x \<in> set as then f x else g x) \<Longrightarrow> (\<lambda>b. if b = a then f a else if b \<in> set as then f b else g b) = (\<lambda>x. if x = a \<or> x \<in> set as then f x else g x) proof (prove)
goal (1 subgoal):
 1. \<And>a as x. foldr (\<lambda>p ps a. if a = p then f p else ps a) as g = (\<lambda>x. if x \<in> set as then f x else g x) \<Longrightarrow> (if x = a then f a else if x \<in> set as then f x else g x) = (if x = a \<or> x \<in> set as then f x else g x) proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma thread_st_auth_detype[simp]:
  "thread_st_auth (detype S s) = (\<lambda>x. if x \<in> S then {} else thread_st_auth s x)" by (rule ext, simp add: thread_st_auth_def get_tcb_def detype_def tcb_states_of_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_st_auth (detype S s) = (\<lambda>x. if x \<in> S then {} else thread_st_auth s x)
theory Retype_AC

lemma thread_bound_ntfns_detype[simp]:
  "thread_bound_ntfns (detype S s) = (\<lambda>x. if x \<in> S then None else thread_bound_ntfns s x)" by (rule ext, simp add: thread_bound_ntfns_def get_tcb_def detype_def tcb_states_of_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_bound_ntfns (detype S s) = (\<lambda>x. if x \<in> S then None else thread_bound_ntfns s x)
theory Retype_AC

lemma sita_detype:
  "state_irqs_to_policy aag (detype R s) \<subseteq> state_irqs_to_policy aag s" apply (clarsimp) apply (erule state_irqs_to_policy_aux.induct) apply (auto simp: detype_def  intro: state_irqs_to_policy_aux.intros split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_irqs_to_policy aag (detype R s) \<subseteq> state_irqs_to_policy aag s proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. (a, aa, b) \<in> state_irqs_to_policy_aux aag (\<lambda>p. if fst p \<in> R then None else caps_of_state s p) \<Longrightarrow> (a, aa, b) \<in> state_irqs_to_policy aag s proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ptr cap irq. \<lbrakk>(if fst ptr \<in> R then None else caps_of_state s ptr) = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma dtsa_detype: "domains_of_state (detype R s) \<subseteq> domains_of_state s" by (auto simp: detype_def detype_ext_def
          intro: domtcbs
          elim!: domains_of_state_aux.cases
          split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domains_of_state (detype R s) \<subseteq> domains_of_state s
theory Retype_AC

lemma detype_integrity:
  "\<lbrakk> integrity aag X st s; \<forall>r\<in>refs. is_subject aag r \<rbrakk>
     \<Longrightarrow> integrity aag X st (detype refs s)" apply (erule integrity_trans) apply (clarsimp simp: integrity_def integrity_asids_detype) apply (clarsimp simp: detype_def detype_ext_def integrity_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity aag X st s; \<forall>r\<in>refs. is_subject aag r\<rbrakk> \<Longrightarrow> integrity aag X st (detype refs s) proof (prove)
goal (1 subgoal):
 1. \<forall>r\<in>refs. is_subject aag r \<Longrightarrow> integrity aag X s (detype refs s) proof (prove)
goal (1 subgoal):
 1. \<forall>r\<in>refs. is_subject aag r \<Longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (detype refs s) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap s x) (ekheap (detype refs s) x)) \<and> (\<forall>a b. cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (cdt s (a, b), is_original_cap s (a, b)) (cdt s (a, b), is_original_cap (detype refs s) (a, b))) \<and> (\<forall>a b. cdt_list_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (cdt_list s (a, b)) (cdt_list (detype refs s) (a, b))) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s x, interrupt_states (detype refs s) x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues s d p) (ready_queues (detype refs s) d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state s) (tcb_states_of_state (detype refs s)) (auth_ipc_buffers s) (underlying_memory (machine_state s) x) (underlying_memory (machine_state (detype refs s)) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state s) (tcb_states_of_state (detype refs s)) (device_state (machine_state s) x) (device_state (machine_state (detype refs s)) x)) proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma sta_detype:
  "state_objs_to_policy (detype R s) \<subseteq> state_objs_to_policy s" apply (clarsimp simp add: state_objs_to_policy_def state_refs_of_detype) apply (erule state_bits_to_policy.induct) apply (auto intro: state_bits_to_policy.intros dest: state_vrefs_detype
                     simp: state_objs_to_policy_def split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_objs_to_policy (detype R s) \<subseteq> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. (a, aa, b) \<in> state_bits_to_policy (\<lambda>p. if fst p \<in> R then None else caps_of_state s p) (\<lambda>x. if x \<in> R then {} else thread_st_auth s x) (\<lambda>x. if x \<in> R then None else thread_bound_ntfns s x) (cdt s) (state_vrefs (detype R s)) \<Longrightarrow> (a, aa, b) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s) proof (prove)
goal (7 subgoals):
 1. \<And>a aa b ptr cap oref auth. \<lbrakk>(if fst ptr \<in> R then None else caps_of_state s ptr) = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 2. \<And>a aa b ptr cap oref. \<lbrakk>(if fst ptr \<in> R then None else caps_of_state s ptr) = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (fst ptr, Control, oref) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 3. \<And>a aa b oref' auth oref. (oref', auth) \<in> (if oref \<in> R then {} else thread_st_auth s oref) \<Longrightarrow> (oref, auth, oref') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 4. \<And>a aa b oref oref' auth. \<lbrakk>(if oref \<in> R then None else thread_bound_ntfns s oref) = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (oref, auth, oref') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 5. \<And>a aa b slot' slot. \<lbrakk>cdt s slot' = Some slot; \<not> is_transferable (if fst slot' \<in> R then None else caps_of_state s slot')\<rbrakk> \<Longrightarrow> (fst slot, Control, fst slot') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 6. \<And>a aa b slot' slot. cdt s slot' = Some slot \<Longrightarrow> (fst slot, DeleteDerived, fst slot') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 7. \<And>a aa b ptr' uu_ uv_ auth ptr. (ptr', uu_, uv_, auth) \<in> state_vrefs (detype R s) ptr \<Longrightarrow> (ptr, auth, ptr') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s) proof (prove)
goal:
No subgoals!