kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_AI

lemma weak_derived_reply_equiv:
  "\<lbrakk> weak_derived c c'; is_reply_cap c \<rbrakk> \<Longrightarrow> obj_ref_of c = obj_ref_of c' \<and> is_reply_cap c'"
  "\<lbrakk> weak_derived c c'; is_reply_cap c' \<rbrakk> \<Longrightarrow> obj_ref_of c = obj_ref_of c' \<and> is_reply_cap c" by (auto simp: weak_derived_def copy_of_def
                 same_object_as_def is_cap_simps
          split: if_split_asm cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>weak_derived c c'; is_reply_cap c\<rbrakk> \<Longrightarrow> obj_ref_of c = obj_ref_of c' \<and> is_reply_cap c') &&& (\<lbrakk>weak_derived c c'; is_reply_cap c'\<rbrakk> \<Longrightarrow> obj_ref_of c = obj_ref_of c' \<and> is_reply_cap c)
theory CSpace_AI

lemma reply_mdb:
  assumes r: "reply_mdb m cs"
  assumes s: "cs src = Some src_cap"
  assumes d: "cs dest = Some cap.NullCap"
  assumes c: "weak_derived cap src_cap"
  shows "reply_mdb m' (cs (dest \<mapsto> cap, src \<mapsto> cap.NullCap))" using r c s d unfolding reply_mdb_def by (simp add: reply_caps_mdb reply_masters_mdb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_mdb m' (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) proof (prove)
using this:
reply_mdb m cs
weak_derived cap src_cap
cs src = Some src_cap
cs dest = Some NullCap

goal (1 subgoal):
 1. reply_mdb m' (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) proof (prove)
using this:
reply_caps_mdb m cs \<and> reply_masters_mdb m cs
weak_derived cap src_cap
cs src = Some src_cap
cs dest = Some NullCap

goal (1 subgoal):
 1. reply_caps_mdb m' (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) \<and> reply_masters_mdb m' (cs(dest \<mapsto> cap, src \<mapsto> NullCap))
theory CSpace_AI

lemma mdb_move_abs_gen:
  "\<And>src dest m (s::'state_ext state).
    mdb_move_abs src dest m s \<Longrightarrow> mdb_move_abs_gen src dest m s" apply (unfold_locales) apply (unfold mdb_move_abs_def) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>src dest m s. mdb_move_abs src dest m s \<Longrightarrow> mdb_move_abs_gen src dest m s proof (prove)
goal (4 subgoals):
 1. \<And>src dest m s. mdb_move_abs src dest m s \<Longrightarrow> valid_mdb s
 2. \<And>src dest m s. mdb_move_abs src dest m s \<Longrightarrow> cte_wp_at ((=) NullCap) dest s
 3. \<And>src dest m s. mdb_move_abs src dest m s \<Longrightarrow> m = cdt s
 4. \<And>src dest m s. mdb_move_abs src dest m s \<Longrightarrow> src \<noteq> dest proof (prove)
goal (4 subgoals):
 1. \<And>src dest m s. (valid_mdb s \<and> cte_wp_at ((=) NullCap) dest s) \<and> m = cdt s \<and> src \<noteq> dest \<Longrightarrow> valid_mdb s
 2. \<And>src dest m s. (valid_mdb s \<and> cte_wp_at ((=) NullCap) dest s) \<and> m = cdt s \<and> src \<noteq> dest \<Longrightarrow> cte_wp_at ((=) NullCap) dest s
 3. \<And>src dest m s. (valid_mdb s \<and> cte_wp_at ((=) NullCap) dest s) \<and> m = cdt s \<and> src \<noteq> dest \<Longrightarrow> m = cdt s
 4. \<And>src dest m s. (valid_mdb s \<and> cte_wp_at ((=) NullCap) dest s) \<and> m = cdt s \<and> src \<noteq> dest \<Longrightarrow> src \<noteq> dest
theory CSpace_AI

lemma cap_move_typ_at:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> cap_move cap ptr ptr' \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" apply (simp add: cap_move_def set_cdt_def) apply (wp set_cap_typ_at | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> cap_move cap ptr ptr' \<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 y <- set_cap cap ptr';
y <- set_cap NullCap ptr;
src_p <- gets (\<lambda>s. cdt s ptr);
dest_p <- gets (\<lambda>s. cdt s ptr');
cdt <- gets cdt;
y <- do s <- get;
put (s\<lparr>cdt := \<lambda>r. if (if r = ptr then None else (cdt(ptr' := cdt ptr)) r) = Some ptr then Some ptr' else (cdt(ptr' := cdt ptr, ptr := None)) r\<rparr>)
od;
y <- do_extended_op (cap_move_ext ptr ptr' src_p dest_p);
is_original <- gets is_original_cap;
y <- set_original ptr' (is_original ptr);
set_original ptr False
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma set_cdt_pspace:
  "\<lbrace>valid_pspace\<rbrace> set_cdt m \<lbrace>\<lambda>_. valid_pspace\<rbrace>" apply (simp add: set_cdt_def) apply wp apply (auto intro: valid_pspace_eqI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace\<rbrace> set_cdt m \<lbrace>\<lambda>_. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace\<rbrace> do s <- get;
put (s\<lparr>cdt := m\<rparr>)
od \<lbrace>\<lambda>_. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_pspace s \<Longrightarrow> valid_pspace (s\<lparr>cdt := m\<rparr>) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma set_cdt_cur:
  "\<lbrace>cur_tcb\<rbrace> set_cdt m \<lbrace>\<lambda>_. cur_tcb\<rbrace>" apply (simp add: set_cdt_def) apply wp apply (simp add: cur_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb\<rbrace> set_cdt m \<lbrace>\<lambda>_. cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb\<rbrace> do s <- get;
put (s\<lparr>cdt := m\<rparr>)
od \<lbrace>\<lambda>_. cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cur_tcb s \<Longrightarrow> cur_tcb (s\<lparr>cdt := m\<rparr>) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma set_cdt_cte_at:
  "\<lbrace>cte_at x\<rbrace> set_cdt m \<lbrace>\<lambda>_. cte_at x\<rbrace>" by (simp add: valid_cte_at_typ set_cdt_typ_at [where P="\<lambda>x. x"])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) x\<rbrace> set_cdt m \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) x\<rbrace>
theory CSpace_AI

lemma set_cdt_valid_cap:
  "\<lbrace>valid_cap c\<rbrace> set_cdt m \<lbrace>\<lambda>_. valid_cap c\<rbrace>" by (rule set_cdt_inv) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap c\<rbrace> set_cdt m \<lbrace>\<lambda>_. valid_cap c\<rbrace>
theory CSpace_AI

lemma set_cdt_iflive[wp]:
  "\<lbrace>if_live_then_nonz_cap\<rbrace> set_cdt m \<lbrace>\<lambda>_. if_live_then_nonz_cap\<rbrace>" by (simp add: set_cdt_def, wp, simp add: if_live_then_nonz_cap_def ex_nonz_cap_to_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap\<rbrace> set_cdt m \<lbrace>\<lambda>_. if_live_then_nonz_cap\<rbrace>
theory CSpace_AI

lemma set_untyped_cap_as_full_cap_to:
  shows
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap s \<and> cte_wp_at ((=) src_cap) src s\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>rv s. if_live_then_nonz_cap s\<rbrace>" apply (clarsimp simp:if_live_then_nonz_cap_def set_untyped_cap_as_full_def
             split del: if_split) apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift set_cap_cap_to)+ apply (auto simp add:cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap s \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>ptr. obj_at live ptr s \<longrightarrow> ex_nonz_cap_to ptr s) \<and> cte_wp_at ((=) src_cap) src s\<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>\<lambda>rv s. \<forall>ptr. obj_at live ptr s \<longrightarrow> ex_nonz_cap_to ptr s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>ptr. obj_at live ptr s \<longrightarrow> ex_nonz_cap_to ptr s) \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> \<forall>x. (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> \<not> obj_at live x 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> \<not> obj_at live x s) \<or> (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> cte_wp_at (\<lambda>cap'. x \<notin> zobj_refs cap' - zobj_refs (max_free_index_update src_cap)) src s \<and> ex_nonz_cap_to x 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> ex_nonz_cap_to x s) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma set_untyped_cap_as_full_valid_pspace:
  "\<lbrace>valid_pspace and cte_wp_at ((=) src_cap) src\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>rv s. valid_pspace s \<rbrace>" apply (clarsimp simp:valid_pspace_def) apply (clarsimp | wp set_untyped_cap_full_valid_objs
      set_untyped_cap_as_full_cap_to set_untyped_cap_as_full_cap_zombies_final )+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace and cte_wp_at ((=) src_cap) src\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and cte_wp_at ((=) src_cap) src\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma set_cdt_idle [wp]:
  "\<lbrace>valid_idle\<rbrace> set_cdt m \<lbrace>\<lambda>rv. valid_idle\<rbrace>" by (simp add: set_cdt_def, wp,
      auto simp: valid_idle_def pred_tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> set_cdt m \<lbrace>\<lambda>rv. valid_idle\<rbrace>
theory CSpace_AI

lemma cap_insert_idle [wp]:
  "\<lbrace>valid_idle\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. valid_idle\<rbrace>" by (rule valid_idle_lift; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. valid_idle\<rbrace>
theory CSpace_AI

lemma caps_of_state_cte_wp_at_neq:
  "(caps_of_state s slot \<noteq> Some capa) = (\<not> cte_wp_at ((=) capa) slot s)" by (clarsimp simp:cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (caps_of_state s slot \<noteq> Some capa) = (\<not> cte_wp_at ((=) capa) slot s)
theory CSpace_AI

lemma max_free_index_update_preserve_untyped:
 "is_untyped_cap c \<Longrightarrow> is_untyped_cap ( max_free_index_update c)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_untyped_cap c \<Longrightarrow> is_untyped_cap (max_free_index_update c)
theory CSpace_AI

lemma set_untyped_cap_as_full_valid_global_refs[wp]:
  "\<lbrace>valid_global_refs and cte_wp_at ((=) src_cap) src\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>r. valid_global_refs\<rbrace>" apply (simp add:valid_global_refs_def valid_refs_def) apply (wp hoare_vcg_all_lift set_untyped_cap_as_full_cte_wp_at_neg| wps)+ apply (clarsimp simp:cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs and cte_wp_at ((=) src_cap) src\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>r. valid_global_refs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>a b. \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s) and cte_wp_at ((=) src_cap) src\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>r s. \<forall>a b. \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>a b. \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s) and cte_wp_at ((=) src_cap) src) s \<Longrightarrow> \<forall>x xa. ((x, xa) \<noteq> src \<and> \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (x, xa) s \<or> (x, xa) = src \<and> \<not> cte_wp_at (\<lambda>a. global_refs s \<inter> cap_range (masked_as_full a cap) \<noteq> {}) src s) \<and> cte_wp_at ((=) src_cap) src s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma cap_insert_reply_masters [wp]:
  "\<lbrace>valid_reply_masters and cte_at dest and K (\<not> is_master_reply_cap cap) \<rbrace>
   cap_insert cap src dest \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>" apply (simp add: cap_insert_def update_cdt_def) apply (wp hoare_drop_imp set_untyped_cap_as_full_valid_reply_masters
      set_untyped_cap_as_full_cte_wp_at get_cap_wp
    | simp add: is_cap_simps split del: if_split)+ apply (clarsimp simp:cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters and cte_wp_at (\<lambda>_. True) dest and K (\<not> is_master_reply_cap cap)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. valid_reply_masters\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters and cte_wp_at (\<lambda>_. True) dest and (\<lambda>y. \<not> is_master_reply_cap cap)\<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 <- do t <- gets cdt;
set_cdt (t(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else t src))
od;
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>_. valid_reply_masters\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_reply_masters s \<and> cte_wp_at (\<lambda>_. True) dest s \<and> (\<forall>x R. cap \<noteq> ReplyCap x True R) \<Longrightarrow> (\<exists>cap. cte_wp_at ((=) cap) src s) \<longrightarrow> (\<exists>cap. cte_wp_at ((=) cap) dest s) \<longrightarrow> dest = src \<longrightarrow> cte_wp_at (\<lambda>a. True) src s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma cap_insert_aobj_at:
  "arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>" unfolding cap_insert_def update_cdt_def set_cdt_def set_untyped_cap_as_full_def by (wpsimp wp: set_cap.aobj_at get_cap_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd 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);
do t <- gets cdt;
s <- get;
put $ s\<lparr>cdt := t(dest := if src_parent then Some src else t src)\<rparr>
od;
do_extended_op (cap_insert_ext src_parent src dest src_p dest_p);
set_original dest dest_original
od \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>
theory CSpace_AI

lemma cap_insert_valid_arch [wp]:
  "\<lbrace>valid_arch_state\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" by (rule valid_arch_state_lift_aobj_at; wp cap_insert_aobj_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
theory CSpace_AI

lemma update_cdt_global [wp]:
  "\<lbrace>valid_global_refs\<rbrace> update_cdt m \<lbrace>\<lambda>_. valid_global_refs\<rbrace>" by (rule valid_global_refs_cte_lift; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs\<rbrace> update_cdt m \<lbrace>\<lambda>_. valid_global_refs\<rbrace>
theory CSpace_AI

lemma cap_insert_valid_global_refs[wp]:
  "\<lbrace>valid_global_refs and (\<lambda>s. cte_wp_at (\<lambda>scap. cap_range cap \<subseteq> cap_range scap) src s)\<rbrace>
  cap_insert cap src dest
  \<lbrace>\<lambda>_. valid_global_refs\<rbrace>" apply (simp add: cap_insert_def) apply (wp get_cap_wp|simp split del: if_split)+ apply (clarsimp simp: cte_wp_at_caps_of_state) apply (simp add: valid_global_refs_def valid_refs_def2) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs and cte_wp_at (\<lambda>scap. cap_range cap \<subseteq> cap_range scap) src\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. valid_global_refs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs and cte_wp_at (\<lambda>scap. cap_range cap \<subseteq> cap_range scap) src\<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>\<lambda>_. valid_global_refs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_global_refs s \<and> cte_wp_at (\<lambda>scap. cap_range cap \<subseteq> cap_range scap) src s \<Longrightarrow> (\<exists>cap. cte_wp_at ((=) cap) src s) \<longrightarrow> cte_wp_at ((=) NullCap) dest s \<longrightarrow> global_refs s \<inter> cap_range cap = {} proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_global_refs s; cap_range cap \<subseteq> cap_range capa; caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range cap = {} proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>\<forall>c\<in>ran (caps_of_state s). global_refs s \<inter> cap_range c = {}; cap_range cap \<subseteq> cap_range capa; caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range cap = {} proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma is_derived_obj_refs:
  "is_derived m p cap cap' \<Longrightarrow> obj_refs cap = obj_refs cap'" apply (clarsimp simp: is_derived_def is_cap_simps cap_master_cap_simps
    split: if_split_asm dest!:cap_master_cap_eqDs) apply (clarsimp simp: cap_master_cap_def) apply (auto split: cap.split_asm dest: master_arch_cap_obj_refs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived m p cap cap' \<Longrightarrow> obj_refs cap = obj_refs cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>dev r bits f. cap' \<noteq> UntypedCap dev r bits f; cap \<noteq> NullCap; \<forall>r b n. cap' \<noteq> Zombie r b n; cap \<noteq> IRQControlCap; cap_master_cap cap' = cap_master_cap cap; (cap_badge cap', cap_badge cap) \<in> capBadge_ordering False; (\<exists>x R. cap' = ReplyCap x True R) = (\<exists>x R. cap = ReplyCap x False R); is_derived_arch cap cap'; \<forall>x R. cap' \<noteq> ReplyCap x False R; \<forall>x R. cap \<noteq> ReplyCap x True R\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>dev r bits f. cap' \<noteq> UntypedCap dev r bits f; cap \<noteq> NullCap; \<forall>r b n. cap' \<noteq> Zombie r b n; cap \<noteq> IRQControlCap; (case cap' of UntypedCap dev ref n f \<Rightarrow> UntypedCap dev ref n 0 | EndpointCap ref bdg rghts \<Rightarrow> EndpointCap ref 0 UNIV | NotificationCap ref bdg rghts \<Rightarrow> NotificationCap ref 0 UNIV | ReplyCap ref master rghts \<Rightarrow> ReplyCap ref True UNIV | CNodeCap ref bits gd \<Rightarrow> CNodeCap ref bits [] | ThreadCap ref \<Rightarrow> ThreadCap ref | DomainCap \<Rightarrow> DomainCap | ArchObjectCap acap \<Rightarrow> ArchObjectCap (cap_master_arch_cap acap) | _ \<Rightarrow> cap') = (case cap of UntypedCap dev ref n f \<Rightarrow> UntypedCap dev ref n 0 | EndpointCap ref bdg rghts \<Rightarrow> EndpointCap ref 0 UNIV | NotificationCap ref bdg rghts \<Rightarrow> NotificationCap ref 0 UNIV | ReplyCap ref master rghts \<Rightarrow> ReplyCap ref True UNIV | CNodeCap ref bits gd \<Rightarrow> CNodeCap ref bits [] | ThreadCap ref \<Rightarrow> ThreadCap ref | DomainCap \<Rightarrow> DomainCap | ArchObjectCap acap \<Rightarrow> ArchObjectCap (cap_master_arch_cap acap) | _ \<Rightarrow> cap); (cap_badge cap', cap_badge cap) \<in> capBadge_ordering False; (\<exists>x R. cap' = ReplyCap x True R) = (\<exists>x R. cap = ReplyCap x False R); is_derived_arch cap cap'; \<forall>x R. cap' \<noteq> ReplyCap x False R; \<forall>x R. cap \<noteq> ReplyCap x True R\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs cap' proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma set_untyped_cap_as_full_access[wp]:
  "\<lbrace>(\<lambda>s. P (vs_lookup s))\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>r s. P (vs_lookup s)\<rbrace>" by (clarsimp simp:set_untyped_cap_as_full_def, wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>r s. P (vs_lookup s)\<rbrace>
theory CSpace_AI

lemma set_untyped_cap_as_full_vs_lookup_pages[wp]:
  "\<lbrace>(\<lambda>s. P (vs_lookup_pages s))\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>r s. P (vs_lookup_pages s)\<rbrace>" by (clarsimp simp:set_untyped_cap_as_full_def, wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>r s. P (vs_lookup_pages s)\<rbrace>