theory Ipc_AI

lemma cap_insert_assume_null:
  "\<lbrace>P\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace> \<Longrightarrow>
   \<lbrace>\<lambda>s. cte_wp_at ((=) cap.NullCap) dest s \<longrightarrow> P s\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace>" apply (rule hoare_name_pre_state) apply (erule impCE) apply (simp add: cap_insert_def) apply (rule hoare_seq_ext[OF _ get_cap_sp])+ apply (clarsimp simp: valid_def cte_wp_at_caps_of_state in_monad
              split del: if_split) apply (erule hoare_pre(1)) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at ((=) NullCap) dest s \<longrightarrow> P s\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace>; cte_wp_at ((=) NullCap) dest s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace>; \<not> cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap cap src;
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>Q\<rbrace>; \<not> cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap cap src;
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>Q\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s src_cap x. \<lbrakk>\<lbrace>P\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap cap src;
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>Q\<rbrace>; \<not> cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s and cte_wp_at (\<lambda>c. c = src_cap) src and cte_wp_at (\<lambda>c. c = x) dest\<rbrace> do y <- assert (x = NullCap);
y <- set_untyped_cap_as_full src_cap cap src;
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>Q\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>P s; s = sa\<rbrakk> \<Longrightarrow> P sa proof (prove)
goal:
No subgoals!