theory CSpace_AI

lemma cap_insert_weak_cte_wp_at:
  "\<lbrace>(\<lambda>s. if p = dest then P cap else p \<noteq> src \<and> cte_wp_at P p s)\<rbrace>
   cap_insert cap src dest
   \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace>" unfolding cap_insert_def error_def set_untyped_cap_as_full_def apply (simp add: bind_assoc split del: if_split ) apply (wp set_cap_cte_wp_at hoare_vcg_if_lift hoare_vcg_imp_lift get_cap_wp | simp | intro conjI impI allI)+ apply (auto simp: cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if p = dest then P cap else p \<noteq> src \<and> cte_wp_at P p s\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if p = dest then P cap else p \<noteq> src \<and> cte_wp_at P p s\<rbrace> do src_cap <- get_cap src;
dest_original <- return $ is_cap_revocable cap src_cap;
old_cap <- get_cap dest;
assert (old_cap = NullCap);
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 ();
set_cap cap dest;
is_original <- gets is_original_cap;
src_parent <- return $ should_be_parent_of src_cap (is_original src) cap dest_original;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
update_cdt (\<lambda>cdt. cdt(dest := if src_parent then Some src else cdt src));
do_extended_op (cap_insert_ext src_parent src dest src_p dest_p);
set_original dest dest_original
od \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if p = dest then P cap else p \<noteq> src \<and> cte_wp_at P p s\<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>uu. cte_wp_at P p\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s capa. \<lbrakk>if p = src then P cap else p \<noteq> src \<and> cte_wp_at P p s; dest = src; cte_wp_at ((=) capa) src s; \<exists>cap. cte_wp_at ((=) cap) src s\<rbrakk> \<Longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) src s \<longrightarrow> cap \<noteq> NullCap) \<or> (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 (\<lambda>_. True) src s) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> cte_wp_at (\<lambda>_. True) src s)
 2. \<And>s capa. \<lbrakk>if p = dest then P cap else p \<noteq> src \<and> cte_wp_at P p s; dest \<noteq> src; p = src; cte_wp_at ((=) capa) src s; \<exists>cap. cte_wp_at ((=) cap) dest s\<rbrakk> \<Longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) dest s \<longrightarrow> cap \<noteq> NullCap) \<or> (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> P (max_free_index_update capa) \<and> cte_wp_at (\<lambda>_. True) src s) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> cte_wp_at P src s) \<and> (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 (\<lambda>_. True) dest s \<and> cte_wp_at (\<lambda>_. True) src s) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> cte_wp_at (\<lambda>_. True) dest s)
 3. \<And>s capa. \<lbrakk>if p = dest then P cap else p \<noteq> src \<and> cte_wp_at P p s; dest \<noteq> src; p \<noteq> src; cte_wp_at ((=) capa) src s; \<exists>cap. cte_wp_at ((=) cap) dest s\<rbrakk> \<Longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) dest s \<longrightarrow> cap \<noteq> NullCap) \<or> (p = dest \<or> (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 P p s \<and> cte_wp_at (\<lambda>_. True) src s) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> cte_wp_at P p s)) \<and> (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 (\<lambda>_. True) dest s \<and> cte_wp_at (\<lambda>_. True) src s) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> cte_wp_at (\<lambda>_. True) dest s) proof (prove)
goal:
No subgoals!