theory CSpaceInv_AI

lemma cap_insert_zombies:
  "\<lbrace>zombies_final and
    (\<lambda>s. (\<forall>r\<in>obj_refs cap. \<forall>p'.
           cte_wp_at (\<lambda>c. r \<in> obj_refs c) p' s
             \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap))\<rbrace>
     cap_insert cap src dest
   \<lbrace>\<lambda>rv. zombies_final\<rbrace>" apply (simp add: cap_insert_def set_untyped_cap_as_full_def) apply (wp| simp split del: if_split)+ apply (wp new_cap_zombies get_cap_wp set_cap_cte_wp_at)+ apply (rule hoare_vcg_conj_lift) apply (clarsimp simp: is_cap_simps) apply (wp set_cap_zombies get_cap_wp set_cap_cte_wp_at hoare_allI)+ apply (clarsimp simp: is_cap_simps free_index_update_def cte_wp_at_caps_of_state | rule conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>p'. cte_wp_at (\<lambda>c. r \<in> obj_refs c) p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. cte_wp_at (\<lambda>c. r \<in> obj_refs c) (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return ();
y <- set_cap cap dest;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
y <- update_cdt (\<lambda>cdt. cdt(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else cdt src));
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap)) src dest src_p dest_p);
set_original dest (is_cap_revocable cap src_cap)
od \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>src_cap x. \<lbrace>?B10 src_cap x () ()\<rbrace> set_cap cap dest \<lbrace>\<lambda>yb. zombies_final\<rbrace>
 2. \<And>src_cap x y. \<lbrace>?B9 src_cap x y\<rbrace> if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return () \<lbrace>?B10 src_cap x y\<rbrace>
 3. \<And>src_cap x. \<lbrace>?B8 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>?B9 src_cap x\<rbrace>
 4. \<And>src_cap. \<lbrace>?B7 src_cap\<rbrace> get_cap dest \<lbrace>?B8 src_cap\<rbrace>
 5. \<lbrace>?Q6\<rbrace> get_cap src \<lbrace>?B7\<rbrace>
 6. \<And>s. (zombies_final and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. cte_wp_at (\<lambda>c. r \<in> obj_refs c) (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>src_cap x y. is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<Longrightarrow> \<lbrace>?P'39 src_cap x y\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. (\<forall>r\<in>obj_refs cap. \<forall>p'. dest \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) \<and> zombies_final s\<rbrace>
 2. \<And>src_cap x y. \<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<Longrightarrow> \<lbrace>?R38 src_cap x y\<rbrace> return () \<lbrace>\<lambda>a b. cte_wp_at ((=) NullCap) dest b \<and> (\<forall>r\<in>obj_refs cap. \<forall>p'. dest \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' b \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' b \<and> \<not> is_zombie cap) \<and> zombies_final b\<rbrace>
 3. \<And>src_cap x. \<lbrace>?B8 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>\<lambda>y s. (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> ((\<lambda>s. if dest = src then NullCap = max_free_index_update src_cap else cte_wp_at ((=) NullCap) dest s) and cte_wp_at (\<lambda>_. True) src) s \<and> ?P'39 src_cap x y s) \<and> (\<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<longrightarrow> ?R38 src_cap x y s)\<rbrace>
 4. \<And>src_cap. \<lbrace>?B7 src_cap\<rbrace> get_cap dest \<lbrace>?B8 src_cap\<rbrace>
 5. \<lbrace>?Q6\<rbrace> get_cap src \<lbrace>?B7\<rbrace>
 6. \<And>s. (zombies_final and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. cte_wp_at (\<lambda>c. r \<in> obj_refs c) (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (7 subgoals):
 1. \<And>src_cap x y. is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<Longrightarrow> \<lbrace>?P42 src_cap x y\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. \<forall>r\<in>obj_refs cap. \<forall>p'. dest \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap\<rbrace>
 2. \<And>src_cap x y. is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<Longrightarrow> \<lbrace>?P'42 src_cap x y\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv. zombies_final\<rbrace>
 3. \<And>src_cap x y. \<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<Longrightarrow> \<lbrace>?R38 src_cap x y\<rbrace> return () \<lbrace>\<lambda>a b. cte_wp_at ((=) NullCap) dest b \<and> (\<forall>r\<in>obj_refs cap. \<forall>p'. dest \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' b \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' b \<and> \<not> is_zombie cap) \<and> zombies_final b\<rbrace>
 4. \<And>src_cap x. \<lbrace>?B8 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>\<lambda>y s. (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> ((\<lambda>s. if dest = src then NullCap = max_free_index_update src_cap else cte_wp_at ((=) NullCap) dest s) and cte_wp_at (\<lambda>_. True) src) s \<and> ?P42 src_cap x y s \<and> ?P'42 src_cap x y s) \<and> (\<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<longrightarrow> ?R38 src_cap x y s)\<rbrace>
 5. \<And>src_cap. \<lbrace>?B7 src_cap\<rbrace> get_cap dest \<lbrace>?B8 src_cap\<rbrace>
 6. \<lbrace>?Q6\<rbrace> get_cap src \<lbrace>?B7\<rbrace>
 7. \<And>s. (zombies_final and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. cte_wp_at (\<lambda>c. r \<in> obj_refs c) (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (7 subgoals):
 1. \<And>x dev f deva ra bitsa fa. cap = UntypedCap deva ra bitsa fa \<Longrightarrow> \<lbrace>?P42 (UntypedCap dev ra bitsa f) x ()\<rbrace> set_cap (free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f)) src \<lbrace>\<lambda>rv s. True\<rbrace>
 2. \<And>src_cap x y. is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<Longrightarrow> \<lbrace>?P'42 src_cap x y\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv. zombies_final\<rbrace>
 3. \<And>src_cap x y. \<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<Longrightarrow> \<lbrace>?R38 src_cap x y\<rbrace> return () \<lbrace>\<lambda>a b. cte_wp_at ((=) NullCap) dest b \<and> (\<forall>r\<in>obj_refs cap. \<forall>p'. dest \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' b \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' b \<and> \<not> is_zombie cap) \<and> zombies_final b\<rbrace>
 4. \<And>src_cap x. \<lbrace>?B8 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>\<lambda>y s. (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> ((\<lambda>s. if dest = src then NullCap = max_free_index_update src_cap else cte_wp_at ((=) NullCap) dest s) and cte_wp_at (\<lambda>_. True) src) s \<and> ?P42 src_cap x y s \<and> ?P'42 src_cap x y s) \<and> (\<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<longrightarrow> ?R38 src_cap x y s)\<rbrace>
 5. \<And>src_cap. \<lbrace>?B7 src_cap\<rbrace> get_cap dest \<lbrace>?B8 src_cap\<rbrace>
 6. \<lbrace>?Q6\<rbrace> get_cap src \<lbrace>?B7\<rbrace>
 7. \<And>s. (zombies_final and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. cte_wp_at (\<lambda>c. r \<in> obj_refs c) (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (zombies_final and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. cte_wp_at (\<lambda>c. r \<in> obj_refs c) (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> (\<forall>capb. cte_wp_at ((=) capb) dest s \<longrightarrow> capb = NullCap \<longrightarrow> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> ((\<lambda>s. if dest = src then NullCap = max_free_index_update capa else cte_wp_at ((=) NullCap) dest s) and cte_wp_at (\<lambda>_. True) src) s \<and> True \<and> zombies_final s \<and> cte_wp_at (\<lambda>cap'. \<forall>r\<in>ex_zombie_refs (max_free_index_update capa, cap'). \<forall>p'. src \<noteq> p' \<and> cte_wp_at (\<lambda>cap''. r \<in> obj_refs cap'') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie (max_free_index_update capa)) src s) \<and> (\<not> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap) \<longrightarrow> cte_wp_at ((=) NullCap) dest s \<and> (\<forall>r\<in>obj_refs cap. \<forall>p'. dest \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) \<and> zombies_final s)) proof (prove)
goal:
No subgoals!