kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchIpc_AI

lemma do_ipc_transfer_tcb_caps [Ipc_AI_assms]:
  assumes imp: "\<And>c. P c \<Longrightarrow> \<not> is_untyped_cap c"
  shows
  "\<lbrace>valid_objs and cte_wp_at P (t, ref) and tcb_at t\<rbrace>
   do_ipc_transfer st ep b gr rt
   \<lbrace>\<lambda>rv. cte_wp_at P (t, ref)\<rbrace>" apply (simp add: do_ipc_transfer_def) apply (rule hoare_pre) apply (wp do_normal_transfer_tcb_caps hoare_drop_imps
       | wpc | simp add:imp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at P (t, ref) and tcb_at t\<rbrace> do_ipc_transfer st ep b gr rt \<lbrace>\<lambda>rv. cte_wp_at P (t, ref)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at P (t, ref) and tcb_at t\<rbrace> do recv_buffer <- lookup_ipc_buffer True rt;
fault <- thread_get tcb_fault st;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False st;
do_normal_transfer st send_buffer ep b gr rt recv_buffer
od | Some f \<Rightarrow> do_fault_transfer b st rt recv_buffer
od \<lbrace>\<lambda>rv. cte_wp_at P (t, ref)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do recv_buffer <- lookup_ipc_buffer True rt;
fault <- thread_get tcb_fault st;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False st;
do_normal_transfer st send_buffer ep b gr rt recv_buffer
od | Some f \<Rightarrow> do_fault_transfer b st rt recv_buffer
od \<lbrace>\<lambda>rv. cte_wp_at P (t, ref)\<rbrace>
 2. \<And>s. (valid_objs and cte_wp_at P (t, ref) and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchIpc_AI

lemma set_thread_state_valid_vso_at[wp]:
  "\<lbrace>valid_vso_at a\<rbrace> set_thread_state s st \<lbrace>\<lambda>rv. valid_vso_at a\<rbrace>" apply (clarsimp simp: valid_vso_at_def) by (wpsimp wp: sts_obj_at_impossible sts_typ_ats hoare_vcg_ex_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vso_at a\<rbrace> set_thread_state s st \<lbrace>\<lambda>rv. valid_vso_at a\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>ao. ako_at ao a s \<and> valid_vspace_obj ao s\<rbrace> set_thread_state s st \<lbrace>\<lambda>rv s. \<exists>ao. ako_at ao a s \<and> valid_vspace_obj ao s\<rbrace>
theory ArchIpc_AI

lemma cap_insert_valid_vso_at[wp]:
  "\<lbrace>valid_vso_at a\<rbrace> cap_insert c sl sl' \<lbrace>\<lambda>rv. valid_vso_at a\<rbrace>" apply (clarsimp simp: valid_vso_at_def) by (wpsimp wp: sts_obj_at_impossible sts_typ_ats hoare_vcg_ex_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vso_at a\<rbrace> cap_insert c sl sl' \<lbrace>\<lambda>rv. valid_vso_at a\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>ao. ako_at ao a s \<and> valid_vspace_obj ao s\<rbrace> cap_insert c sl sl' \<lbrace>\<lambda>rv s. \<exists>ao. ako_at ao a s \<and> valid_vspace_obj ao s\<rbrace>
theory ArchIpc_AI

lemma setup_caller_cap_valid_global_objs[wp, Ipc_AI_assms]:
  "\<lbrace>valid_global_objs\<rbrace> setup_caller_cap send recv grant \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>" apply (wp valid_global_objs_lift valid_ao_at_lift) unfolding setup_caller_cap_def apply (wp sts_obj_at_impossible | simp add: tcb_not_empty_table)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs\<rbrace> setup_caller_cap send recv grant \<lbrace>\<lambda>rv. valid_global_objs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>p. \<lbrace>valid_vso_at p\<rbrace> setup_caller_cap send recv grant \<lbrace>\<lambda>rv. valid_vso_at p\<rbrace>
 2. \<And>ako p. \<lbrace>ako_at ako p\<rbrace> setup_caller_cap send recv grant \<lbrace>\<lambda>_. ako_at ako p\<rbrace>
 3. \<And>pd S. \<lbrace>obj_at (empty_table S) pd\<rbrace> setup_caller_cap send recv grant \<lbrace>\<lambda>rv. obj_at (empty_table S) pd\<rbrace>
 4. \<And>s. valid_global_objs s \<Longrightarrow> valid_global_objs s proof (prove)
goal (4 subgoals):
 1. \<And>p. \<lbrace>valid_vso_at p\<rbrace> do set_thread_state send BlockedOnReply;
cap_insert (ReplyCap send False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (send, tcb_cnode_index 2) (recv, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_vso_at p\<rbrace>
 2. \<And>ako p. \<lbrace>ako_at ako p\<rbrace> do set_thread_state send BlockedOnReply;
cap_insert (ReplyCap send False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (send, tcb_cnode_index 2) (recv, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. ako_at ako p\<rbrace>
 3. \<And>pd S. \<lbrace>obj_at (empty_table S) pd\<rbrace> do set_thread_state send BlockedOnReply;
cap_insert (ReplyCap send False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (send, tcb_cnode_index 2) (recv, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. obj_at (empty_table S) pd\<rbrace>
 4. \<And>s. valid_global_objs s \<Longrightarrow> valid_global_objs s proof (prove)
goal:
No subgoals!
theory ArchIpc_AI

lemma set_mrs_state_hyp_refs_of[wp]:
  "\<lbrace>\<lambda> s. P (state_hyp_refs_of s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace>" by (wp set_mrs_thread_set_dmo thread_set_hyp_refs_trivial | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace>
theory ArchIpc_AI

lemma arch_derive_cap_untyped:
  "\<lbrace>\<lambda>s. P (untyped_range (ArchObjectCap cap))\<rbrace> arch_derive_cap cap \<lbrace>\<lambda>rv s. rv \<noteq> cap.NullCap \<longrightarrow> P (untyped_range rv)\<rbrace>,-" by (wpsimp simp: arch_derive_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (untyped_range (ArchObjectCap cap))\<rbrace> arch_derive_cap cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (untyped_range rv)\<rbrace>, -
theory ArchIpc_AI

lemma valid_arch_mdb_cap_swap:
  "\<And>s cap capb.
       \<lbrakk>valid_arch_mdb (is_original_cap s) (caps_of_state s);
        weak_derived c cap; caps_of_state s a = Some cap;
        is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b;
        weak_derived c' capb; caps_of_state s b = Some capb\<rbrakk>
       \<Longrightarrow> valid_arch_mdb
            ((is_original_cap s)
             (a := is_original_cap s b, b := is_original_cap s a))
            ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s cap capb. \<lbrakk>valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c))
theory CNodeInv_AI

lemma mask_cap_all:
  "mask_cap (all_rights \<inter> r) c = mask_cap r c" unfolding all_rights_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mask_cap (all_rights \<inter> r) c = mask_cap r c proof (prove)
goal (1 subgoal):
 1. mask_cap (UNIV \<inter> r) c = mask_cap r c
theory CNodeInv_AI

lemma Suc_length_not_empty:
  "length xs = length xs' \<Longrightarrow> Suc 0 \<le> length xs' = (xs \<noteq> [])" by (fastforce simp: le_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = length xs' \<Longrightarrow> (Suc 0 \<le> length xs') = (xs \<noteq> [])
theory CNodeInv_AI

lemma update_cap_hoare_helper:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. valid_cap (C rv s) s\<rbrace> \<Longrightarrow>
   \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. valid_cap (update_cap_data prs n (C rv s)) s\<rbrace>" apply (erule hoare_strengthen_post) apply (erule update_cap_data_validI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. s \<turnstile> C rv s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. s \<turnstile> update_cap_data prs n (C rv s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. s \<turnstile> C rv s \<Longrightarrow> s \<turnstile> update_cap_data prs n (C rv s) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma mask_cap_hoare_helper:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. valid_cap (C rv s) s\<rbrace> \<Longrightarrow>
   \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. valid_cap (mask_cap (M rv s) (C rv s)) s\<rbrace>" by (fastforce simp add: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. s \<turnstile> C rv s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. s \<turnstile> mask_cap (M rv s) (C rv s)\<rbrace>
theory CNodeInv_AI

lemma derive_cap_untyped:
  "\<lbrace>\<lambda>s. P (untyped_range cap)\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. rv \<noteq> cap.NullCap \<longrightarrow> P (untyped_range rv)\<rbrace>,-" unfolding derive_cap_def is_zombie_def by (cases cap; (wp ensure_no_children_inv arch_derive_cap_untyped | simp add: o_def)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (untyped_range cap)\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (untyped_range rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (untyped_range cap)\<rbrace> case cap of UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk cap
odE | ReplyCap ptr m cr \<Rightarrow> returnOk NullCap | IRQControlCap \<Rightarrow> returnOk NullCap | Zombie ptr n sz \<Rightarrow> returnOk NullCap | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (untyped_range rv)\<rbrace>, -
theory CNodeInv_AI

lemma cap_asid_mask[simp]:
  "cap_asid (mask_cap m c) = cap_asid c" by (simp add: mask_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_asid (mask_cap m c) = cap_asid c
theory CNodeInv_AI

lemma cap_master_mask[simp]:
  "cap_master_cap (mask_cap rs cap) = cap_master_cap cap" by (simp add: mask_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap (mask_cap rs cap) = cap_master_cap cap
theory CNodeInv_AI

lemma cap_badge_mask[simp]:
  "cap_badge (mask_cap rs cap) = cap_badge cap" by (simp add: mask_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_badge (mask_cap rs cap) = cap_badge cap
theory CNodeInv_AI

lemma ensure_empty_cte_wp_at:
  "\<lbrace>\<top>\<rbrace> ensure_empty c \<lbrace>\<lambda>rv s. cte_wp_at ((=) cap.NullCap) c s\<rbrace>, -" unfolding ensure_empty_def apply (wp whenE_throwError_wp get_cap_wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> ensure_empty c \<lbrace>\<lambda>rv. cte_wp_at ((=) NullCap) c\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> doE cap <- liftE $ get_cap c;
whenE (cap \<noteq> NullCap) (throwError DeleteFirst)
odE \<lbrace>\<lambda>rv. cte_wp_at ((=) NullCap) c\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) c s \<longrightarrow> \<not> cap \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) NullCap) c s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma lookup_cap_ex[wp]:
  "\<lbrace>\<top>\<rbrace> lookup_cap t c \<lbrace>\<lambda>rv s. \<forall>r\<in>cte_refs rv (interrupt_irq_node s). ex_cte_cap_to r s\<rbrace>, -" by (simp add: split_def lookup_cap_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> lookup_cap t c \<lbrace>\<lambda>rv s. \<forall>r\<in>cte_refs rv (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s\<rbrace>, -
theory CNodeInv_AI

lemma has_cancel_send_rights_ep_cap:
  "has_cancel_send_rights cap \<Longrightarrow> is_ep_cap cap" by (clarsimp simp: has_cancel_send_rights_def split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. has_cancel_send_rights cap \<Longrightarrow> is_ep_cap cap
theory CNodeInv_AI

lemma fixed_length_finite:
  "finite (UNIV :: 'a set) \<Longrightarrow> finite {x :: 'a list. length x = n}" apply (induct n) apply simp apply (subgoal_tac "{x :: 'a list. length x = Suc n} = image (split Cons) (UNIV \<times> {x. length x = n})") apply clarsimp apply safe apply (case_tac x, simp_all add: image_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite UNIV \<Longrightarrow> finite {x. length x = n} proof (prove)
goal (2 subgoals):
 1. finite UNIV \<Longrightarrow> finite {x. length x = 0}
 2. \<And>n. \<lbrakk>finite UNIV \<Longrightarrow> finite {x. length x = n}; finite UNIV\<rbrakk> \<Longrightarrow> finite {x. length x = Suc n} proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>finite UNIV \<Longrightarrow> finite {x. length x = n}; finite UNIV\<rbrakk> \<Longrightarrow> finite {x. length x = Suc n} proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>finite UNIV \<Longrightarrow> finite {x. length x = n}; finite UNIV; {x. length x = Suc n} = (\<lambda>(x, y). x # y) ` (UNIV \<times> {x. length x = n})\<rbrakk> \<Longrightarrow> finite {x. length x = Suc n}
 2. \<And>n. \<lbrakk>finite UNIV \<Longrightarrow> finite {x. length x = n}; finite UNIV\<rbrakk> \<Longrightarrow> {x. length x = Suc n} = (\<lambda>(x, y). x # y) ` (UNIV \<times> {x. length x = n}) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>finite UNIV \<Longrightarrow> finite {x. length x = n}; finite UNIV\<rbrakk> \<Longrightarrow> {x. length x = Suc n} = (\<lambda>(x, y). x # y) ` (UNIV \<times> {x. length x = n}) proof (prove)
goal (2 subgoals):
 1. \<And>n x. \<lbrakk>finite UNIV \<Longrightarrow> finite {x. length x = n}; finite UNIV; length x = Suc n\<rbrakk> \<Longrightarrow> x \<in> (\<lambda>(x, y). x # y) ` (UNIV \<times> {x. length x = n})
 2. \<And>n x a b. \<lbrakk>finite UNIV \<Longrightarrow> finite {x. length x = length b}; finite UNIV; a \<in> UNIV\<rbrakk> \<Longrightarrow> length (a # b) = Suc (length b) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma state_cte_ptrs_finite:
  "finite (state_cte_ptrs s)" apply (clarsimp simp add: state_cte_ptrs_def cte_at_cases Collect_disj_eq
                            Collect_conj_eq set_pair_UN tcb_cap_cases_def) apply (clarsimp simp: well_formed_cnode_n_def fixed_length_finite) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite (state_cte_ptrs s) proof (prove)
goal (1 subgoal):
 1. \<And>x xb sz fun y. \<lbrakk>kheap s x = Some (CNode sz fun); well_formed_cnode_n sz fun; fun xb = Some y\<rbrakk> \<Longrightarrow> finite ({x} \<times> dom fun) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cte_wp_at_set_finite:
  "finite {p. cte_wp_at (P p) p s}" apply (rule finite_subset [OF _ state_cte_ptrs_finite[where s=s]]) apply (clarsimp simp: state_cte_ptrs_def elim!: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite {p. cte_wp_at (P p) p s} proof (prove)
goal (1 subgoal):
 1. {p. cte_wp_at (P p) p s} \<subseteq> state_cte_ptrs s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma not_recursive_cspaces_finite:
  "finite (not_recursive_cspaces s)" unfolding not_recursive_cspaces_def by (rule cte_wp_at_set_finite)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite (not_recursive_cspaces s) proof (prove)
goal (1 subgoal):
 1. finite {ptr. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s}
theory CNodeInv_AI

lemma set_cdt_not_recursive[wp]:
  "\<lbrace>\<lambda>s. P (not_recursive_cspaces s)\<rbrace> set_cdt f \<lbrace>\<lambda>rv s. P (not_recursive_cspaces s)\<rbrace>" apply (simp add: set_cdt_def, wp) apply (simp add: not_recursive_cspaces_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (not_recursive_cspaces s)\<rbrace> set_cdt f \<lbrace>\<lambda>rv s. P (not_recursive_cspaces s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (not_recursive_cspaces s) \<Longrightarrow> P (not_recursive_cspaces (s\<lparr>cdt := f\<rparr>)) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma set_cap_no_new_recursive:
  "\<lbrace>\<lambda>s. x \<notin> not_recursive_cspaces s
      \<and> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s\<rbrace>
     set_cap cap ptr
   \<lbrace>\<lambda>rv s. x \<notin> not_recursive_cspaces s\<rbrace>" apply (simp add: not_recursive_cspaces_def) apply (wp set_cap_cte_wp_at_neg) apply (clarsimp simp: cte_wp_at_neg split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. x \<notin> not_recursive_cspaces s \<and> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. x \<notin> not_recursive_cspaces s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at (\<lambda>cap. x \<notin> fst_cte_ptrs cap) x s \<and> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. \<not> cte_wp_at (\<lambda>cap. x \<notin> fst_cte_ptrs cap) x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> cte_wp_at (\<lambda>cap. x \<notin> fst_cte_ptrs cap) x s \<and> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<Longrightarrow> cte_wp_at (\<lambda>_. True) ptr s \<and> (if x = ptr then \<not> x \<notin> fst_cte_ptrs cap else \<not> cte_wp_at (\<lambda>cap. x \<notin> fst_cte_ptrs cap) x s) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma not_recursive_set_cap_doesn't_grow:
  "\<lbrace>\<lambda>s. card (not_recursive_cspaces s) < n
      \<and> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s\<rbrace>
     set_cap cap ptr
   \<lbrace>\<lambda>rv s. card (not_recursive_cspaces s) < n\<rbrace>" apply (rule doesn't_grow_proof) apply (rule not_recursive_cspaces_finite) apply (rule set_cap_no_new_recursive) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. card (not_recursive_cspaces s) < n \<and> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. card (not_recursive_cspaces s) < n\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. finite (not_recursive_cspaces s)
 2. \<And>x. \<lbrace>\<lambda>s. x \<notin> not_recursive_cspaces s \<and> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. x \<notin> not_recursive_cspaces s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. x \<notin> not_recursive_cspaces s \<and> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. x \<notin> not_recursive_cspaces s\<rbrace> proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma fst_cte_ptrs_link_obj_refs:
  "x \<in> fst_cte_ptrs cap \<Longrightarrow> fst x \<in> obj_refs cap" by (case_tac cap, simp_all add: fst_cte_ptrs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> fst_cte_ptrs cap \<Longrightarrow> fst x \<in> obj_refs cap
theory CNodeInv_AI

lemma final_cap_duplicate_cte_ptr:
  "\<lbrakk> fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)}; is_final_cap' cap s;
     x \<in> fst_cte_ptrs cap; p \<noteq> p' \<rbrakk> \<Longrightarrow> x \<notin> fst_cte_ptrs cap'" apply (drule(2) final_cap_duplicate_obj_ref) apply (erule fst_cte_ptrs_link_obj_refs) apply assumption apply (clarsimp simp: fst_cte_ptrs_link_obj_refs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)}; is_final_cap' cap s; x \<in> fst_cte_ptrs cap; p \<noteq> p'\<rbrakk> \<Longrightarrow> x \<notin> fst_cte_ptrs cap' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>fst (get_cap p' s) = {(cap', s)}; is_final_cap' cap s; x \<in> fst_cte_ptrs cap; p \<noteq> p'\<rbrakk> \<Longrightarrow> ?x \<in> obj_refs cap
 2. \<lbrakk>fst (get_cap p' s) = {(cap', s)}; is_final_cap' cap s; x \<in> fst_cte_ptrs cap; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<noteq> p'
 3. \<lbrakk>fst (get_cap p' s) = {(cap', s)}; is_final_cap' cap s; x \<in> fst_cte_ptrs cap; p \<noteq> p'; ?x \<notin> obj_refs cap'\<rbrakk> \<Longrightarrow> x \<notin> fst_cte_ptrs cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fst (get_cap p' s) = {(cap', s)}; is_final_cap' cap s; x \<in> fst_cte_ptrs cap; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<noteq> p'
 2. \<lbrakk>fst (get_cap p' s) = {(cap', s)}; is_final_cap' cap s; x \<in> fst_cte_ptrs cap; p \<noteq> p'; fst x \<notin> obj_refs cap'\<rbrakk> \<Longrightarrow> x \<notin> fst_cte_ptrs cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (get_cap p' s) = {(cap', s)}; is_final_cap' cap s; x \<in> fst_cte_ptrs cap; p \<noteq> p'; fst x \<notin> obj_refs cap'\<rbrakk> \<Longrightarrow> x \<notin> fst_cte_ptrs cap' proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma not_recursive_cspaces_more_update[iff]:
  "not_recursive_cspaces (trans_state f s) = not_recursive_cspaces s" by (simp add: not_recursive_cspaces_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_recursive_cspaces (trans_state f s) = not_recursive_cspaces s
theory CNodeInv_AI

lemma cap_swap_fd_not_recursive:
  "\<lbrace>\<lambda>s. card (not_recursive_cspaces s) \<le> n
     \<and> cte_wp_at (\<lambda>cap. is_final_cap' cap s
                      \<and> p1 \<in> fst_cte_ptrs cap) p2 s
     \<and> p1 \<noteq> p2\<rbrace>
     cap_swap_for_delete p1 p2
   \<lbrace>\<lambda>rv s. card (not_recursive_cspaces s) < n\<rbrace>" unfolding cap_swap_for_delete_def by (wpsimp wp: cap_swap_not_recursive get_cap_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. card (not_recursive_cspaces s) \<le> n \<and> cte_wp_at (\<lambda>cap. is_final_cap' cap s \<and> p1 \<in> fst_cte_ptrs cap) p2 s \<and> p1 \<noteq> p2\<rbrace> cap_swap_for_delete p1 p2 \<lbrace>\<lambda>rv s. card (not_recursive_cspaces s) < n\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. card (not_recursive_cspaces s) \<le> n \<and> cte_wp_at (\<lambda>cap. is_final_cap' cap s \<and> p1 \<in> fst_cte_ptrs cap) p2 s \<and> p1 \<noteq> p2\<rbrace> when (p1 \<noteq> p2) $ do cap1 <- get_cap p1;
cap2 <- get_cap p2;
cap_swap cap1 p1 cap2 p2
od \<lbrace>\<lambda>rv s. card (not_recursive_cspaces s) < n\<rbrace>
theory CNodeInv_AI

lemma cte_wp_and:
  "cte_wp_at (P and Q) c s = (cte_wp_at P c s \<and> cte_wp_at Q c s)" by (auto simp: cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (P and Q) c s = (cte_wp_at P c s \<and> cte_wp_at Q c s)
theory CNodeInv_AI

lemma in_pspace_typ_at:
  "r \<notin> dom (kheap s) = (\<forall>T. \<not> typ_at T r s)" apply (simp add: dom_def) apply (subst simp_thms(2)[symmetric]) apply (fastforce simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (r \<notin> dom (kheap s)) = (\<forall>T. \<not> typ_at T r s) proof (prove)
goal (1 subgoal):
 1. (kheap s r = None) = (\<forall>T. \<not> typ_at T r s) proof (prove)
goal (1 subgoal):
 1. (kheap s r \<noteq> None) = (\<not> (\<forall>T. \<not> typ_at T r s)) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma prepare_thread_delete_not_recursive:
  "\<lbrace>\<lambda>s. P (not_recursive_cspaces s)\<rbrace>
     prepare_thread_delete t
   \<lbrace>\<lambda>rv s. P (not_recursive_cspaces s)\<rbrace>" apply (simp add: not_recursive_cspaces_def cte_wp_at_caps_of_state) apply (wp prepare_thread_delete_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (not_recursive_cspaces s)\<rbrace> prepare_thread_delete t \<lbrace>\<lambda>rv s. P (not_recursive_cspaces s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P {ptr. \<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap}\<rbrace> prepare_thread_delete t \<lbrace>\<lambda>rv s. P {ptr. \<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap}\<rbrace> proof (prove)
goal:
No subgoals!