kings-crown/FVELER_Isabelle huggingface dataset:
theory CNode_AC

lemma integrity_cdt_list_as_list_integ:
  "cdt_list_integrity_state aag st s =
   list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st s" by (fastforce elim: integrity_cdt_listE list_integE intro: list_integI integrity_cdt_list_intros)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list s x)) = list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st s
theory CNode_AC

lemma set_original_integrity_autarch:
  "\<lbrace>integrity aag X st and K (is_subject aag (fst slot))\<rbrace>
   set_original slot orig
   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" apply (wpsimp simp: set_original_def) apply (clarsimp simp: integrity_def intro!: integrity_cdt_direct) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag (fst slot))\<rbrace> set_original slot orig \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>integrity aag X st s; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>is_original_cap := (is_original_cap s)(slot := orig)\<rparr>) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma set_original_integrity:
  "\<lbrace>integrity aag X st and cdt_change_allowed' aag slot\<rbrace>
   set_original slot orig
   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" apply integrity_trans_start apply (wpsimp simp: set_original_def integrity_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and cdt_change_allowed' aag slot\<rbrace> set_original slot orig \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdt_change_allowed' aag slot s \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_original slot orig \<lbrace>\<lambda>rv. integrity aag X s\<rbrace> proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma update_cdt_fun_upd_integrity_autarch:
  "\<lbrace>integrity aag X st and K (is_subject aag (fst slot))\<rbrace>
   update_cdt (\<lambda>cdt. cdt (slot := v cdt))
   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" apply (wpsimp simp: update_cdt_def set_cdt_def) apply (clarsimp simp: integrity_def intro!: integrity_cdt_direct) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag (fst slot))\<rbrace> update_cdt (\<lambda>cdt. cdt(slot := v cdt)) \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>integrity aag X st s; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>cdt := \<lambda>a. if a = slot then v (cdt s) else cdt s a\<rparr>) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma cap_insert_integrity_autarch:
  "\<lbrace>integrity aag X st and K (is_subject aag (fst src_slot) \<and> is_subject aag (fst dest_slot))\<rbrace>
   cap_insert cap src_slot dest_slot
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: cap_insert_def) apply (wp set_original_integrity_autarch cap_insert_ext_extended_list_integ_lift
            cap_insert_list_integrity update_cdt_fun_upd_integrity_autarch gets_inv
            set_cap_integrity_autarch set_untyped_cap_as_full_integrity_autarch assert_inv) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag (fst src_slot) \<and> is_subject aag (fst dest_slot))\<rbrace> cap_insert cap src_slot dest_slot \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag (fst src_slot) \<and> is_subject aag (fst dest_slot))\<rbrace> do src_cap <- get_cap src_slot;
old_cap <- get_cap dest_slot;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap cap src_slot;
y <- set_cap cap dest_slot;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
y <- update_cdt (\<lambda>cdt. cdt(dest_slot := if should_be_parent_of src_cap (is_original src_slot) cap (is_cap_revocable cap src_cap) then Some src_slot else cdt src_slot));
y <- cap_insert_ext (should_be_parent_of src_cap (is_original src_slot) cap (is_cap_revocable cap src_cap)) src_slot dest_slot src_p dest_p;
set_original dest_slot (is_cap_revocable cap src_cap)
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 (fst src_slot) \<and> is_subject aag (fst dest_slot))) s \<Longrightarrow> (integrity aag X st and K (is_subject aag (fst src_slot))) s \<and> K (is_subject aag (fst dest_slot)) s \<and> K (is_subject aag (fst dest_slot)) s \<and> K (cdt_change_allowed' aag dest_slot st) s \<and> K (is_subject aag (fst dest_slot)) s proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma resolve_address_bits_authorised[wp]:
  "\<lbrace>pas_refined aag and K (is_cnode_cap cap \<longrightarrow> (\<forall>x \<in> obj_refs_ac cap. is_subject aag x))\<rbrace>
   resolve_address_bits (cap, cref)
   \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, -" apply (unfold validE_R_def) apply (rule hoare_pre) apply (rule use_spec(2)[OF resolve_address_bits_authorised_aux]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))\<rbrace> resolve_address_bits (cap, cref) \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))\<rbrace> resolve_address_bits (cap, cref) \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> resolve_address_bits (cap, cref) \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. (pas_refined aag and K (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and K (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))) s \<Longrightarrow> (pas_refined aag and K (is_cnode_cap (fst (cap, cref)) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (fst (cap, cref)). is_subject aag x))) s proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma lookup_slot_for_cnode_op_authorised[wp]:
  "\<lbrace>pas_refined aag and K (is_cnode_cap croot \<longrightarrow> (\<forall>x \<in> obj_refs_ac croot. is_subject aag x))\<rbrace>
   lookup_slot_for_cnode_op is_source croot ptr depth
   \<lbrace>\<lambda>rv s. is_subject aag (fst rv)\<rbrace>, -" apply (simp add: lookup_slot_for_cnode_op_def split del: if_split) apply (wp whenE_throwError_wp hoare_drop_imps
            resolve_address_bits_authorised
              [THEN hoare_post_imp_R[where Q'="\<lambda>x s. is_subject aag (fst (fst x))"]]
         | wpc | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_cnode_cap croot \<longrightarrow> (\<forall>x\<in>obj_refs_ac croot. is_subject aag x))\<rbrace> lookup_slot_for_cnode_op is_source croot ptr depth \<lbrace>\<lambda>rv s. is_subject aag (fst rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and (\<lambda>y. is_cnode_cap croot \<longrightarrow> (\<forall>x\<in>obj_refs_ac croot. is_subject aag x))\<rbrace> if is_cnode_cap croot then doE y <- whenE (depth = 0 \<or> word_bits < depth) (throwError (RangeError 1 (word_of_nat word_bits)));
lookup_error_on_failure is_source (doE (slot, rem) <- resolve_address_bits (croot, drop (length ptr - depth) ptr);
case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0
odE)
odE else throwError (FailedLookup is_source InvalidRoot) \<lbrace>\<lambda>rv s. is_subject aag (fst rv)\<rbrace>, - proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma is_cnode_into_is_subject:
  "\<lbrakk> pas_cap_cur_auth aag cap; pas_refined aag s; is_cnode_cap cap \<rbrakk>
     \<Longrightarrow> \<forall>x\<in>obj_refs_ac cap. is_subject aag x" by (clarsimp simp: is_cap_simps cap_auth_conferred_def
                     pas_refined_all_auth_is_owns aag_cap_auth_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cap_cur_auth aag cap; pas_refined aag s; is_cnode_cap cap\<rbrakk> \<Longrightarrow> \<forall>x\<in>obj_refs_ac cap. is_subject aag x
theory CNode_AC

lemma get_cap_prop_imp:
  "\<lbrace>cte_wp_at (\<lambda>cap. P cap \<longrightarrow> Q cap) slot\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. P rv \<longrightarrow> cte_wp_at Q slot s\<rbrace>" by (wpsimp wp: get_cap_wp simp: cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>cap. P cap \<longrightarrow> Q cap) slot\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. P rv \<longrightarrow> cte_wp_at Q slot s\<rbrace>
theory CNode_AC

lemma get_cap_cur_auth:
  "\<lbrace>pas_refined aag and cte_wp_at (\<lambda>_. True) slot and K (is_subject aag (fst slot))\<rbrace>
   get_cap slot
   \<lbrace>\<lambda>rv s. pas_cap_cur_auth aag rv\<rbrace>" apply (wp get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state cap_cur_auth_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and cte_wp_at (\<lambda>_. True) slot and K (is_subject aag (fst slot))\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. pas_cap_cur_auth aag rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and cte_wp_at (\<lambda>_. True) slot and K (is_subject aag (fst slot))) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> pas_cap_cur_auth aag cap proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma set_cap_thread_st_auth[wp]:
  "set_cap cap ptr \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace>" apply (wpsimp wp: get_object_wp simp: set_cap_def split_def set_object_def) apply (fastforce simp: obj_at_def get_tcb_def tcb_states_of_state_def
                         thread_st_auth_def rsubst[where P=P, OF _ ext]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace> set_cap cap ptr \<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 (fst ptr) s\<rbrakk> \<Longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = a_type (CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) \<longrightarrow> P (thread_st_auth (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) else kheap s a\<rparr>)))) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (thread_st_auth (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ctable := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (thread_st_auth (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_vtable := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (thread_st_auth (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_reply := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (thread_st_auth (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_caller := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (thread_st_auth (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)) else kheap s a\<rparr>)))))))) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma set_cap_thread_bound_ntfns[wp]:
  "set_cap cap ptr \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace>" apply (wpsimp wp: get_object_wp simp: set_cap_def split_def set_object_def) apply (fastforce simp: obj_at_def get_tcb_def thread_bound_ntfns_def rsubst[where P=P, OF _ ext]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> set_cap cap ptr \<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 (fst ptr) s\<rbrakk> \<Longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = a_type (CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) \<longrightarrow> P (thread_bound_ntfns (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) else kheap s a\<rparr>)))) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (thread_bound_ntfns (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ctable := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (thread_bound_ntfns (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_vtable := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (thread_bound_ntfns (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_reply := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (thread_bound_ntfns (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_caller := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (thread_bound_ntfns (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)) else kheap s a\<rparr>)))))))) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma sita_caps_update:
  "\<lbrakk> pas_wellformed aag; state_irqs_to_policy_aux aag caps \<subseteq> pasPolicy aag;
     cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap \<rbrakk>
     \<Longrightarrow> state_irqs_to_policy_aux aag (caps(ptr \<mapsto> cap)) \<subseteq> pasPolicy aag" by (fastforce intro: state_irqs_to_policy_aux.intros
                 elim: state_irqs_to_policy_aux.cases
                 simp: cap_links_irq_def split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_wellformed aag; state_irqs_to_policy_aux aag caps \<subseteq> pasPolicy aag; cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap\<rbrakk> \<Longrightarrow> state_irqs_to_policy_aux aag (caps(ptr \<mapsto> cap)) \<subseteq> pasPolicy aag
theory CNode_AC

lemma sita_caps_update2:
  "\<lbrakk> pas_wellformed aag; state_irqs_to_policy_aux aag caps \<subseteq> pasPolicy aag;
     cap_links_irq aag (pasObjectAbs aag (fst ptr')) cap';
     cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap \<rbrakk>
     \<Longrightarrow> state_irqs_to_policy_aux aag (caps(ptr \<mapsto> cap, ptr' \<mapsto> cap')) \<subseteq> pasPolicy aag" by (fastforce intro: state_irqs_to_policy_aux.intros
                 elim: state_irqs_to_policy_aux.cases
                 simp: cap_links_irq_def split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_wellformed aag; state_irqs_to_policy_aux aag caps \<subseteq> pasPolicy aag; cap_links_irq aag (pasObjectAbs aag (fst ptr')) cap'; cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap\<rbrakk> \<Longrightarrow> state_irqs_to_policy_aux aag (caps(ptr \<mapsto> cap, ptr' \<mapsto> cap')) \<subseteq> pasPolicy aag
theory CNode_AC

lemma set_cap_pas_refined_not_transferable:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
                    and cte_wp_at (\<lambda>c. \<not>is_transferable (Some c)) ptr
                    and K (aag_cap_auth aag (pasObjectAbs aag (fst ptr)) cap)\<rbrace>
   set_cap cap ptr
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" by (wpsimp wp: set_cap_pas_refined simp: cte_wp_at_caps_of_state)

(* 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 cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) ptr and K (aag_cap_auth aag (pasObjectAbs aag (fst ptr)) cap)\<rbrace> set_cap cap ptr \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory CNode_AC

lemma parent_ofI[intro!]: "m x = Some src \<Longrightarrow> m \<Turnstile> src \<leadsto> x" by (simp add: cdt_parent_rel_def is_cdt_parent_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m x = Some src \<Longrightarrow> m \<Turnstile> src \<leadsto> x
theory CNode_AC

lemma cap_swap_for_delete_respects[wp]:
  "\<lbrace>integrity aag X st and pas_refined aag
                       and K (is_subject aag (fst slot) \<and> is_subject aag (fst slot'))\<rbrace>
   cap_swap_for_delete slot slot'
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" by (wpsimp simp: cap_swap_for_delete_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (is_subject aag (fst slot) \<and> is_subject aag (fst slot'))\<rbrace> cap_swap_for_delete slot slot' \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory CNode_AC

lemma set_irq_state_respects[wp]:
  "\<lbrace>integrity aag X st and K (is_subject_irq aag irq)\<rbrace>
   set_irq_state irqst irq
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" unfolding set_irq_state_def by (wpsimp wp: dmo_no_mem_respects simp: integrity_subjects_def integrity_interrupts_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject_irq aag irq)\<rbrace> set_irq_state irqst irq \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject_irq aag irq)\<rbrace> do modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := irqst)\<rparr>);
do_machine_op $ maskInterrupt (irqst = IRQInactive) irq
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory CNode_AC

lemma dmo_wp:
  assumes mopv: "\<And>s. \<lbrace>P s\<rbrace> mop \<lbrace>\<lambda>a b. R a (s\<lparr>machine_state := b\<rparr>)\<rbrace>"
  shows "\<lbrace>\<lambda>s. P s (machine_state s)\<rbrace> do_machine_op mop \<lbrace>R\<rbrace>" by (wpsimp simp: do_machine_op_def use_valid[OF _ mopv])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s (machine_state s)\<rbrace> do_machine_op mop \<lbrace>R\<rbrace>
theory CNode_AC

lemma cdt_change_allowed_all_children:
  "all_children (cdt_change_allowed aag subject (cdt s) (tcb_states_of_state s)) (cdt s)" by (rule all_childrenI) (erule cdt_change_allowed_to_child)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_children (cdt_change_allowed aag subject (cdt s) (tcb_states_of_state s)) (cdt s)
theory CNode_AC

lemma post_cap_deletion_integrity[wp]:
 "\<lbrace>integrity aag X s and K (cleanup_info_wf cleanup_info aag)\<rbrace>
  post_cap_deletion cleanup_info
  \<lbrace>\<lambda>_. integrity aag X s\<rbrace>" by (wpsimp simp: post_cap_deletion_def is_cap_simps wp: arch_post_cap_deletion_integrity)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X s and K (cleanup_info_wf cleanup_info aag)\<rbrace> post_cap_deletion cleanup_info \<lbrace>\<lambda>_. integrity aag X s\<rbrace>
theory CNode_AC

lemma empty_slot_integrity_spec:
  notes split_paired_All[simp del]
  shows
  "s \<turnstile> \<lbrace>valid_list and valid_mdb and valid_objs and pas_refined aag
                   and K (is_subject aag (fst slot) \<and> cleanup_info_wf cleanup_info aag)\<rbrace>
       empty_slot slot cleanup_info
       \<lbrace>\<lambda>_. integrity aag X s\<rbrace>" apply (simp add: spec_valid_def) apply (simp add: empty_slot_def) apply (wp add: get_cap_wp set_cap_integrity_autarch set_original_integrity_autarch
                 empty_slot_extended_list_integ_lift empty_slot_list_integrity[where m="cdt s"]
         | simp add: set_cdt_def | wpc)+ apply (safe; \<comment> \<open>for speedup\<close>
         (clarsimp simp add: integrity_def)?,
         blast intro: cca_owned cdt_change_allowed_all_children) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>valid_list and valid_mdb and valid_objs and pas_refined aag and K (is_subject aag (fst slot) \<and> cleanup_info_wf cleanup_info aag)\<rbrace> empty_slot slot cleanup_info \<lbrace>\<lambda>_. integrity aag X s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>sa. sa = s \<and> valid_list sa \<and> valid_mdb sa \<and> valid_objs sa \<and> pas_refined aag sa \<and> is_subject aag (fst slot) \<and> cleanup_info_wf cleanup_info aag\<rbrace> empty_slot slot cleanup_info \<lbrace>\<lambda>_. integrity aag X s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>sa. sa = s \<and> valid_list sa \<and> valid_mdb sa \<and> valid_objs sa \<and> pas_refined aag sa \<and> is_subject aag (fst slot) \<and> cleanup_info_wf cleanup_info aag\<rbrace> do cap <- get_cap slot;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None));
y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
y <- set_cap NullCap slot;
post_cap_deletion cleanup_info
od
od \<lbrace>\<lambda>_. integrity aag X s\<rbrace> proof (prove)
goal (1 subgoal):
 1. valid_list s \<and> valid_mdb s \<and> valid_objs s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<and> cleanup_info_wf cleanup_info aag \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> integrity aag X s (s\<lparr>cdt := \<lambda>a. if a = slot then None else if cdt s a = Some slot then cdt s slot else cdt s a\<rparr>) \<and> cdt_change_allowed' aag slot s \<and> all_children (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt s) proof (prove)
goal:
No subgoals!