kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpaceInv_AI

lemma set_cap_kernel_window[wp]:
  "set_cap cap p \<lbrace>pspace_in_kernel_window\<rbrace>" apply (simp add: set_cap_def split_def) apply (wp set_object_pspace_in_kernel_window get_object_wp | wpc)+ apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> set_cap cap p \<lbrace>\<lambda>_. pspace_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> do obj <- get_object (fst p);
(case obj of CNode sz cn \<Rightarrow> if snd p \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd p \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd p = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd p = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd p = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd p = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd p = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object (fst p)
od \<lbrace>\<lambda>_. pspace_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_in_kernel_window s \<Longrightarrow> \<forall>ko. ko_at ko (fst p) s \<longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> (snd p \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> pspace_in_kernel_window s) \<and> (\<not> (snd p \<in> dom xa \<and> well_formed_cnode_n x xa) \<longrightarrow> True)) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd p = tcb_cnode_index 0 \<longrightarrow> pspace_in_kernel_window s) \<and> (snd p \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd p = tcb_cnode_index 1 \<longrightarrow> pspace_in_kernel_window s) \<and> (snd p \<noteq> tcb_cnode_index 1 \<longrightarrow> (snd p = tcb_cnode_index 2 \<longrightarrow> pspace_in_kernel_window s) \<and> (snd p \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd p = tcb_cnode_index 3 \<longrightarrow> pspace_in_kernel_window s) \<and> (snd p \<noteq> tcb_cnode_index 3 \<longrightarrow> (snd p = tcb_cnode_index 4 \<longrightarrow> pspace_in_kernel_window s) \<and> (snd p \<noteq> tcb_cnode_index 4 \<longrightarrow> True)))))) \<and> (\<forall>x. ko = Endpoint x \<longrightarrow> True) \<and> (\<forall>x. ko = Notification x \<longrightarrow> True) \<and> (\<forall>x. ko = ArchObj x \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cap_pspace_respects_device[wp]:
  "set_cap cap p \<lbrace>pspace_respects_device_region\<rbrace>" apply (simp add: set_cap_def split_def) apply (wp set_object_pspace_respects_device_region get_object_wp | wpc)+ apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_respects_device_region\<rbrace> set_cap cap p \<lbrace>\<lambda>_. pspace_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_respects_device_region\<rbrace> do obj <- get_object (fst p);
(case obj of CNode sz cn \<Rightarrow> if snd p \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd p \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd p = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd p = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd p = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd p = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd p = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object (fst p)
od \<lbrace>\<lambda>_. pspace_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_respects_device_region s \<Longrightarrow> \<forall>ko. ko_at ko (fst p) s \<longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> (snd p \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> pspace_respects_device_region s) \<and> (\<not> (snd p \<in> dom xa \<and> well_formed_cnode_n x xa) \<longrightarrow> True)) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd p = tcb_cnode_index 0 \<longrightarrow> pspace_respects_device_region s) \<and> (snd p \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd p = tcb_cnode_index 1 \<longrightarrow> pspace_respects_device_region s) \<and> (snd p \<noteq> tcb_cnode_index 1 \<longrightarrow> (snd p = tcb_cnode_index 2 \<longrightarrow> pspace_respects_device_region s) \<and> (snd p \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd p = tcb_cnode_index 3 \<longrightarrow> pspace_respects_device_region s) \<and> (snd p \<noteq> tcb_cnode_index 3 \<longrightarrow> (snd p = tcb_cnode_index 4 \<longrightarrow> pspace_respects_device_region s) \<and> (snd p \<noteq> tcb_cnode_index 4 \<longrightarrow> True)))))) \<and> (\<forall>x. ko = Endpoint x \<longrightarrow> True) \<and> (\<forall>x. ko = Notification x \<longrightarrow> True) \<and> (\<forall>x. ko = ArchObj x \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cap_cap_refs_respects_device_region_spec:
  "\<lbrace>cap_refs_respects_device_region
     and (\<lambda>s. cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c \<and> ((cap_range cap \<noteq> {}) \<longrightarrow> cap_is_device cap = cap_is_device c)) ptr s)\<rbrace>
     set_cap cap p
   \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" apply (wp set_cap_cap_refs_respects_device_region) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region and cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device c)) ptr\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cap_refs_respects_device_region and cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device c)) ptr) s \<Longrightarrow> (cap_refs_respects_device_region and (\<lambda>s. \<exists>ptr. cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device c)) ptr s)) s proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma replaceable_cap_is_device_cap:
 "\<lbrakk>replaceable s p cap c; cap \<noteq> NullCap\<rbrakk>\<Longrightarrow> cap_is_device cap = cap_is_device c" apply (simp add: replaceable_def is_cap_simps is_final_cap'_def) apply (elim disjE,simp_all add: is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>replaceable s p cap c; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_is_device cap = cap_is_device c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = cap \<or> (\<exists>a b. {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> gen_obj_refs c \<inter> gen_obj_refs cap' \<noteq> {}} = {(a, b)}) \<and> (\<forall>p\<in>zobj_refs c - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>a b. (a, b) \<in> cte_refs c (interrupt_irq_node s) \<and> ((a, b) \<in> cte_refs cap (interrupt_irq_node s) \<longrightarrow> (\<exists>cp. appropriate_cte_cap cp c \<and> \<not> appropriate_cte_cap cp cap)) \<longrightarrow> ((a, b) \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) (a, b) s) \<and> (a, b) \<noteq> p) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs c \<and> cap_range cap = cap_range c \<and> (\<forall>x R. c \<noteq> ReplyCap x True R) \<and> (\<forall>x R. c \<noteq> ReplyCap x False R) \<and> ((\<forall>x R. c \<noteq> ReplyCap x True R) \<longrightarrow> tcb_cap_valid c p s \<longrightarrow> tcb_cap_valid cap p s) \<and> (\<forall>dev r bits f. cap \<noteq> UntypedCap dev r bits f) \<and> (\<forall>x R. cap \<noteq> ReplyCap x True R) \<and> (\<forall>x R. cap \<noteq> ReplyCap x False R) \<and> cap \<noteq> IRQControlCap \<and> cap_class cap = cap_class c \<and> cap_is_device cap = cap_is_device c \<and> replaceable_final_arch_cap s p cap c; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_is_device cap = cap_is_device c proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cap_cap_refs_respects_device_region_replaceable:
  "\<lbrace>cap_refs_respects_device_region and (\<lambda>s. cte_wp_at (replaceable s p cap) p s)\<rbrace>
     set_cap cap p
   \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" apply (case_tac "cap = NullCap") apply (wp set_cap_cap_refs_respects_device_region_NullCap | simp)+ apply (wp set_cap_cap_refs_respects_device_region_spec[where ptr = p]) apply clarsimp apply (erule cte_wp_at_weakenE) apply (simp add: replaceable_cap_is_device_cap replaceable_cap_range) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region and (\<lambda>s. cte_wp_at (replaceable s p cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (2 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>cap_refs_respects_device_region and (\<lambda>s. cte_wp_at (replaceable s p cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>
 2. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>cap_refs_respects_device_region and (\<lambda>s. cte_wp_at (replaceable s p cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>cap_refs_respects_device_region and (\<lambda>s. cte_wp_at (replaceable s p cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap \<noteq> NullCap; (cap_refs_respects_device_region and (\<lambda>s. cte_wp_at (replaceable s p cap) p s)) s\<rbrakk> \<Longrightarrow> (cap_refs_respects_device_region and cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device c)) p) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap \<noteq> NullCap; cap_refs_respects_device_region s; cte_wp_at (replaceable s p cap) p s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device c)) p s proof (prove)
goal (1 subgoal):
 1. \<And>s c. \<lbrakk>cap \<noteq> NullCap; cap_refs_respects_device_region s; replaceable s p cap c\<rbrakk> \<Longrightarrow> cap_range cap \<subseteq> cap_range c \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device c) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cdt_cdt_ct_ms_rvk[wp]:
  "\<lbrace>\<lambda>s. P m\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace>"
  "\<lbrace>\<lambda>s. Q (is_original_cap s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. Q (is_original_cap s)\<rbrace>"
  "\<lbrace>\<lambda>s. R (cur_thread s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. R (cur_thread s)\<rbrace>"
  "\<lbrace>\<lambda>s. S (machine_state s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. S (machine_state s)\<rbrace>"
  "\<lbrace>\<lambda>s. T (idle_thread s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. T (idle_thread s)\<rbrace>"
  "\<lbrace>\<lambda>s. U (arch_state s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. U (arch_state s)\<rbrace>" by (simp add: set_cdt_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>\<lambda>s. P m\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace> &&& \<lbrace>\<lambda>s. Q (is_original_cap s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. Q (is_original_cap s)\<rbrace> &&& \<lbrace>\<lambda>s. R (cur_thread s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. R (cur_thread s)\<rbrace>) &&& \<lbrace>\<lambda>s. S (machine_state s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. S (machine_state s)\<rbrace> &&& \<lbrace>\<lambda>s. T (idle_thread s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. T (idle_thread s)\<rbrace> &&& \<lbrace>\<lambda>s. U (arch_state s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. U (arch_state s)\<rbrace>
theory CSpaceInv_AI

lemma set_original_wp[wp]:
  "\<lbrace>\<lambda>s. Q () (s \<lparr> is_original_cap := ((is_original_cap s) (p := v))\<rparr>)\<rbrace>
     set_original p v
   \<lbrace>Q\<rbrace>" by (simp add: set_original_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q () (s\<lparr>is_original_cap := (is_original_cap s)(p := v)\<rparr>)\<rbrace> set_original p v \<lbrace>Q\<rbrace>
theory CSpaceInv_AI

lemma set_cdt_typ_at:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" apply (rule set_cdt_inv) apply (simp add: obj_at_def) done

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

lemma set_untyped_cap_as_full_typ_at[wp]:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace>
   set_untyped_cap_as_full src_cap a b
   \<lbrace>\<lambda>ya s. P (typ_at T p s)\<rbrace>" apply (clarsimp simp: set_untyped_cap_as_full_def) apply (wp set_cap_typ_at hoare_drop_imps | simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_untyped_cap_as_full src_cap a b \<lbrace>\<lambda>ya s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap a; obj_ref_of src_cap = obj_ref_of a; cap_bits_untyped src_cap = cap_bits_untyped a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_cap (max_free_index_update src_cap) b \<lbrace>\<lambda>ya s. P (typ_at T p s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma cap_insert_typ_at [wp]:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> cap_insert a b c \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" apply (simp add: cap_insert_def update_cdt_def) apply (wp set_cap_typ_at set_cdt_typ_at hoare_drop_imps
         |simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> cap_insert a b c \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do src_cap <- get_cap b;
old_cap <- get_cap c;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap a b;
y <- set_cap a c;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s b);
dest_p <- gets (\<lambda>s. cdt s c);
y <- do t <- gets cdt;
set_cdt (t(c := if should_be_parent_of src_cap (is_original b) a (is_cap_revocable a src_cap) then Some b else t b))
od;
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original b) a (is_cap_revocable a src_cap)) b c src_p dest_p);
set_original c (is_cap_revocable a src_cap)
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma cur_mdb [simp]:
  "cur_tcb (cdt_update f s) = cur_tcb s" by (simp add: cur_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cur_tcb (cdt_update f s) = cur_tcb s
theory CSpaceInv_AI

lemma cur_tcb_more_update[iff]:
  "cur_tcb (trans_state f s) = cur_tcb s" by (simp add: cur_tcb_def)

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

lemma update_cdt_ifunsafe[wp]:
  "\<lbrace>if_unsafe_then_cap\<rbrace> update_cdt f \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>" apply (simp add: update_cdt_def set_cdt_def) apply wp apply (clarsimp elim!: ifunsafe_pspaceI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> update_cdt f \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> do t <- gets cdt;
s <- get;
put (s\<lparr>cdt := f t\<rparr>)
od \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. if_unsafe_then_cap s \<Longrightarrow> if_unsafe_then_cap (s\<lparr>cdt := f (cdt s)\<rparr>) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma ex_cap_revokable[simp]:
  "ex_nonz_cap_to p (s\<lparr>is_original_cap := m\<rparr>) = ex_nonz_cap_to p s" by (simp add: ex_nonz_cap_to_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_nonz_cap_to p (s\<lparr>is_original_cap := m\<rparr>) = ex_nonz_cap_to p s
theory CSpaceInv_AI

lemma zombies_final_revokable[simp]:
  "zombies_final (is_original_cap_update f s) = zombies_final s" by (fastforce elim!: zombies_final_pspaceI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zombies_final (is_original_cap_update f s) = zombies_final s
theory CSpaceInv_AI

lemma update_cdt_ex_cap[wp]:
  "\<lbrace>ex_nonz_cap_to p\<rbrace> update_cdt f \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>" apply (simp add: update_cdt_def set_cdt_def) apply wp apply (simp add: ex_nonz_cap_to_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to p\<rbrace> update_cdt f \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to p\<rbrace> do t <- gets cdt;
s <- get;
put (s\<lparr>cdt := f t\<rparr>)
od \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ex_nonz_cap_to p s \<Longrightarrow> ex_nonz_cap_to p (s\<lparr>cdt := f (cdt s)\<rparr>) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma update_cdt_zombies[wp]:
  "\<lbrace>zombies_final\<rbrace> update_cdt m \<lbrace>\<lambda>rv. zombies_final\<rbrace>" apply (simp add: update_cdt_def set_cdt_def) apply wp apply (clarsimp elim!: zombies_final_pspaceI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> update_cdt m \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> do t <- gets cdt;
s <- get;
put (s\<lparr>cdt := m t\<rparr>)
od \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. zombies_final s \<Longrightarrow> zombies_final (s\<lparr>cdt := m (cdt s)\<rparr>) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma valid_cap_free_index_update[simp]:
  "valid_cap cap s \<Longrightarrow> valid_cap (max_free_index_update cap) s" apply (case_tac cap) apply (simp_all add: free_index_update_def split: cap.splits ) apply (clarsimp simp: valid_cap_def cap_aligned_def valid_untyped_def max_free_index_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> cap \<Longrightarrow> s \<turnstile> max_free_index_update cap proof (prove)
goal (12 subgoals):
 1. \<lbrakk>s \<turnstile> cap; cap = NullCap\<rbrakk> \<Longrightarrow> s \<turnstile> max_free_index_update cap
 2. \<And>x21 x22 x23 x24. \<lbrakk>s \<turnstile> cap; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> s \<turnstile> max_free_index_update cap
 3. \<And>x31 x32 x33. \<lbrakk>s \<turnstile> cap; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> s \<turnstile> max_free_index_update cap
 4. \<And>x41 x42 x43. \<lbrakk>s \<turnstile> cap; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> s \<turnstile> max_free_index_update cap
 5. \<And>x51 x52 x53. \<lbrakk>s \<turnstile> cap; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> s \<turnstile> max_free_index_update cap
 6. \<And>x61 x62 x63. \<lbrakk>s \<turnstile> cap; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> s \<turnstile> max_free_index_update cap
 7. \<And>x7. \<lbrakk>s \<turnstile> cap; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> s \<turnstile> max_free_index_update cap
 8. \<lbrakk>s \<turnstile> cap; cap = DomainCap\<rbrakk> \<Longrightarrow> s \<turnstile> max_free_index_update cap
 9. \<lbrakk>s \<turnstile> cap; cap = IRQControlCap\<rbrakk> \<Longrightarrow> s \<turnstile> max_free_index_update cap
 10. \<And>x10. \<lbrakk>s \<turnstile> cap; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> s \<turnstile> max_free_index_update cap
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24. \<lbrakk>s \<turnstile> UntypedCap x21 x22 x23 x24; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> s \<turnstile> UntypedCap x21 x22 x23 (max_free_index x23) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma ex_nonz_cap_to_more_update[iff]:
  "ex_nonz_cap_to w (trans_state f s) = ex_nonz_cap_to w s" by (simp add: ex_nonz_cap_to_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_nonz_cap_to w (trans_state f s) = ex_nonz_cap_to w s
theory CSpaceInv_AI

lemma untyped_cap_update_ex_cte_cap_wp_to:
  "\<lbrakk>if_unsafe_then_cap s; caps_of_state s src = Some src_cap;
    is_untyped_cap src_cap; is_untyped_cap cap\<rbrakk>
   \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) src s" apply (case_tac src) apply (simp add: if_unsafe_then_cap_def) apply (drule spec)+ apply (drule(1) mp)+ apply (clarsimp simp: is_cap_simps) apply (erule ex_cte_cap_wp_to_weakenE) apply (clarsimp simp: appropriate_cte_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>if_unsafe_then_cap s; caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) src s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>if_unsafe_then_cap s; caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap cap; src = (a, b)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) src s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) (a, b) s; caps_of_state s (a, b) = Some src_cap; is_untyped_cap src_cap; is_untyped_cap cap; src = (a, b)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s (a, b) = Some src_cap; is_untyped_cap src_cap; is_untyped_cap cap; src = (a, b); caps_of_state s (?a1 a b, ?b3 a b) = Some (?cap5 a b) \<longrightarrow> ?cap5 a b \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (?cap5 a b)) (?a1 a b, ?b3 a b) s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s (a, b) = Some src_cap; is_untyped_cap src_cap; is_untyped_cap cap; src = (a, b); src_cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap src_cap) (a, b) s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>a b dev deva r ra bits bitsa f fa. \<lbrakk>caps_of_state s (a, b) = Some (UntypedCap dev r bits f); src = (a, b); ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev r bits f)) (a, b) s; src_cap = UntypedCap dev r bits f; cap = UntypedCap deva ra bitsa fa\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap deva ra bitsa fa)) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>a b dev deva r ra bits bitsa f fa cte_cap. \<lbrakk>caps_of_state s (a, b) = Some (UntypedCap dev r bits f); src = (a, b); src_cap = UntypedCap dev r bits f; cap = UntypedCap deva ra bitsa fa; appropriate_cte_cap (UntypedCap dev r bits f) cte_cap; (a, b) \<in> cte_refs cte_cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> appropriate_cte_cap (UntypedCap deva ra bitsa fa) cte_cap proof (prove)
goal:
No subgoals!