theory Ipc_DR

lemma cap_insert_cte_wp_at_masked_as_full:
  assumes "\<And>c. P c \<Longrightarrow> P (masked_as_full c cap)"
  shows "\<lbrace>\<lambda>s. if slot = dest then P cap else cte_wp_at P slot s\<rbrace>
   cap_insert cap src dest \<lbrace>\<lambda>uu. cte_wp_at P slot\<rbrace>" apply (simp add:cap_insert_def set_untyped_cap_as_full_def) apply (wp set_cap_cte_wp_at hoare_vcg_if_lift get_cap_wp hoare_weak_lift_imp dxo_wp_weak
       | simp split del:if_split)+ apply (intro conjI impI allI |
    clarsimp simp:cte_wp_at_caps_of_state)+ apply (drule assms) apply (clarsimp simp:masked_as_full_def) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (clarsimp simp:cte_wp_at_caps_of_state)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if slot = dest then P cap else cte_wp_at P slot s\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>uu. cte_wp_at P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s)\<rbrace> do src_cap <- CSpaceAcc_A.get_cap src;
old_cap <- CSpaceAcc_A.get_cap dest;
y <- assert (old_cap = cap.NullCap);
y <- if Structures_A.is_untyped_cap src_cap \<and> Structures_A.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 CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ();
y <- CSpaceAcc_A.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 slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s) \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> cte_wp_at ((=) cap.NullCap) dest s \<longrightarrow> (slot \<noteq> dest \<longrightarrow> Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> (if slot = src then P (max_free_index_update capa) else cte_wp_at P slot s) \<and> cte_wp_at (\<lambda>_. True) src s) \<and> (Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> (if dest = src then True else 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> Structures_A.is_untyped_cap cap \<longrightarrow> Structures_A.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 (5 subgoals):
 1. \<And>s capa. \<lbrakk>caps_of_state s dest = Some cap.NullCap; src \<noteq> dest; Structures_A.is_untyped_cap capa; caps_of_state s src = Some capa; P capa; Structures_A.is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; slot = src\<rbrakk> \<Longrightarrow> P (max_free_index_update capa)
 2. \<And>s capa. \<lbrakk>(slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) cap.NullCap) dest s; slot \<noteq> dest; Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) src s
 3. \<And>s capa. \<lbrakk>(slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) cap.NullCap) dest s; Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> if dest = src then True else cte_wp_at (\<lambda>_. True) dest s
 4. \<And>s capa. \<lbrakk>(slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) cap.NullCap) dest s; Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) src s
 5. \<And>s capa. \<lbrakk>(slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) cap.NullCap) dest s; obj_ref_of capa = obj_ref_of cap \<longrightarrow> Structures_A.is_untyped_cap cap \<longrightarrow> Structures_A.is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) dest s proof (prove)
goal (5 subgoals):
 1. \<And>s capa. \<lbrakk>caps_of_state s dest = Some cap.NullCap; src \<noteq> dest; Structures_A.is_untyped_cap capa; caps_of_state s src = Some capa; Structures_A.is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; slot = src; P (masked_as_full capa cap)\<rbrakk> \<Longrightarrow> P (max_free_index_update capa)
 2. \<And>s capa. \<lbrakk>(slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) cap.NullCap) dest s; slot \<noteq> dest; Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) src s
 3. \<And>s capa. \<lbrakk>(slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) cap.NullCap) dest s; Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> if dest = src then True else cte_wp_at (\<lambda>_. True) dest s
 4. \<And>s capa. \<lbrakk>(slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) cap.NullCap) dest s; Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) src s
 5. \<And>s capa. \<lbrakk>(slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) cap.NullCap) dest s; obj_ref_of capa = obj_ref_of cap \<longrightarrow> Structures_A.is_untyped_cap cap \<longrightarrow> Structures_A.is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) dest s proof (prove)
goal (4 subgoals):
 1. \<And>s capa. \<lbrakk>(slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) cap.NullCap) dest s; slot \<noteq> dest; Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) src s
 2. \<And>s capa. \<lbrakk>(slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) cap.NullCap) dest s; Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> if dest = src then True else cte_wp_at (\<lambda>_. True) dest s
 3. \<And>s capa. \<lbrakk>(slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) cap.NullCap) dest s; Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) src s
 4. \<And>s capa. \<lbrakk>(slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) cap.NullCap) dest s; obj_ref_of capa = obj_ref_of cap \<longrightarrow> Structures_A.is_untyped_cap cap \<longrightarrow> Structures_A.is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) dest s proof (prove)
goal (3 subgoals):
 1. \<And>s capa. \<lbrakk>(slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) cap.NullCap) dest s; Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> if dest = src then True else cte_wp_at (\<lambda>_. True) dest s
 2. \<And>s capa. \<lbrakk>(slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) cap.NullCap) dest s; Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) src s
 3. \<And>s capa. \<lbrakk>(slot = dest \<longrightarrow> P cap) \<and> (slot \<noteq> dest \<longrightarrow> cte_wp_at P slot s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) cap.NullCap) dest s; obj_ref_of capa = obj_ref_of cap \<longrightarrow> Structures_A.is_untyped_cap cap \<longrightarrow> Structures_A.is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) dest s proof (prove)
goal:
No subgoals!