theory CSpaceInv_AI

lemma cap_insert_cap_wp_to[wp]:
  "\<lbrace> K_bind(\<forall>x. P x = P (x\<lparr>free_index:=y\<rparr>)) and ex_cte_cap_wp_to P p\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace>" apply (simp add: cap_insert_def ex_cte_cap_wp_to_def set_untyped_cap_as_full_def
                   cte_wp_at_caps_of_state update_cdt_def) apply (wp get_cap_wp | simp split del: if_split)+ apply (rule allI) apply (clarsimp, rule conjI) apply (clarsimp simp: is_cap_simps cte_wp_at_caps_of_state) apply (rule_tac x = a in exI) apply (rule_tac x = b in exI) apply (clarsimp simp: cte_wp_at_caps_of_state | rule conjI)+ apply (rule_tac x = a in exI) apply (rule_tac x = b in exI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K_bind (\<forall>x. P x = P (free_index_update (\<lambda>_. y) x)) and ex_cte_cap_wp_to P p\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>ya. \<forall>x. P x = P (free_index_update (\<lambda>_. y) x)) and (\<lambda>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node 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 <- 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>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>x. P x = P (free_index_update (\<lambda>_. y) x)) \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)) \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> cte_wp_at ((=) NullCap) dest s \<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> (\<exists>a b capb. (if (a, b) = dest then Some cap else if (a, b) = src then Some (max_free_index_update capa) else caps_of_state s (a, b)) = Some capb \<and> P capb \<and> p \<in> cte_refs capb (interrupt_irq_node 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> (\<exists>a b capa. (if (a, b) = dest then Some cap else caps_of_state s (a, b)) = Some capa \<and> P capa \<and> p \<in> cte_refs capa (interrupt_irq_node s))) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. (\<forall>x. P x = P (free_index_update (\<lambda>_. y) x)) \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)) \<Longrightarrow> cte_wp_at ((=) capa) src s \<longrightarrow> cte_wp_at ((=) NullCap) dest s \<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> (\<exists>a b capb. (if (a, b) = dest then Some cap else if (a, b) = src then Some (max_free_index_update capa) else caps_of_state s (a, b)) = Some capb \<and> P capb \<and> p \<in> cte_refs capb (interrupt_irq_node 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> (\<exists>a b capa. (if (a, b) = dest then Some cap else caps_of_state s (a, b)) = Some capa \<and> P capa \<and> p \<in> cte_refs capa (interrupt_irq_node s))) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b capaa. \<lbrakk>\<forall>x. P x = P (free_index_update (\<lambda>_. y) x); caps_of_state s (a, b) = Some capaa; P capaa; p \<in> cte_refs capaa (interrupt_irq_node s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s\<rbrakk> \<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> (\<exists>a b. ((a, b) = src \<longrightarrow> (src = dest \<longrightarrow> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)) \<and> (src \<noteq> dest \<longrightarrow> P (max_free_index_update capa) \<and> p \<in> cte_refs (max_free_index_update capa) (interrupt_irq_node s))) \<and> ((a, b) \<noteq> src \<longrightarrow> ((a, b) = dest \<longrightarrow> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)) \<and> ((a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)))))
 2. \<And>s capa a b capaa. \<lbrakk>\<forall>x. P x = P (free_index_update (\<lambda>_. y) x); caps_of_state s (a, b) = Some capaa; P capaa; p \<in> cte_refs capaa (interrupt_irq_node s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> (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> (\<exists>a b. ((a, b) = dest \<longrightarrow> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)) \<and> ((a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s a b capa dev f deva ra bitsa fa. \<lbrakk>\<forall>x. P x = P (free_index_update (\<lambda>_. y) x); caps_of_state s (a, b) = Some capa; P capa; p \<in> cte_refs capa (interrupt_irq_node s); caps_of_state s src = Some (UntypedCap dev ra bitsa f); caps_of_state s dest = Some NullCap; cap = UntypedCap deva ra bitsa fa\<rbrakk> \<Longrightarrow> \<exists>a b. ((a, b) = src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> P (free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f)) \<and> p \<in> cte_refs (free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f)) (interrupt_irq_node s))) \<and> ((a, b) \<noteq> src \<longrightarrow> (a, b) \<noteq> dest \<and> ((a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s))))
 2. \<And>s capa a b capaa. \<lbrakk>\<forall>x. P x = P (free_index_update (\<lambda>_. y) x); caps_of_state s (a, b) = Some capaa; P capaa; p \<in> cte_refs capaa (interrupt_irq_node s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> (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> (\<exists>a b. ((a, b) = dest \<longrightarrow> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)) \<and> ((a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s a b capa dev f deva ra bitsa fa. \<lbrakk>\<forall>x. P x = P (free_index_update (\<lambda>_. y) x); caps_of_state s (a, b) = Some capa; P capa; p \<in> cte_refs capa (interrupt_irq_node s); caps_of_state s src = Some (UntypedCap dev ra bitsa f); caps_of_state s dest = Some NullCap; cap = UntypedCap deva ra bitsa fa\<rbrakk> \<Longrightarrow> \<exists>b. ((a, b) = src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> P (free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f)) \<and> p \<in> cte_refs (free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f)) (interrupt_irq_node s))) \<and> ((a, b) \<noteq> src \<longrightarrow> (a, b) \<noteq> dest \<and> ((a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s))))
 2. \<And>s capa a b capaa. \<lbrakk>\<forall>x. P x = P (free_index_update (\<lambda>_. y) x); caps_of_state s (a, b) = Some capaa; P capaa; p \<in> cte_refs capaa (interrupt_irq_node s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> (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> (\<exists>a b. ((a, b) = dest \<longrightarrow> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)) \<and> ((a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s a b capa dev f deva ra bitsa fa. \<lbrakk>\<forall>x. P x = P (free_index_update (\<lambda>_. y) x); caps_of_state s (a, b) = Some capa; P capa; p \<in> cte_refs capa (interrupt_irq_node s); caps_of_state s src = Some (UntypedCap dev ra bitsa f); caps_of_state s dest = Some NullCap; cap = UntypedCap deva ra bitsa fa\<rbrakk> \<Longrightarrow> ((a, b) = src \<longrightarrow> src \<noteq> dest \<and> (src \<noteq> dest \<longrightarrow> P (free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f)) \<and> p \<in> cte_refs (free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f)) (interrupt_irq_node s))) \<and> ((a, b) \<noteq> src \<longrightarrow> (a, b) \<noteq> dest \<and> ((a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s))))
 2. \<And>s capa a b capaa. \<lbrakk>\<forall>x. P x = P (free_index_update (\<lambda>_. y) x); caps_of_state s (a, b) = Some capaa; P capaa; p \<in> cte_refs capaa (interrupt_irq_node s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> (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> (\<exists>a b. ((a, b) = dest \<longrightarrow> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)) \<and> ((a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa. \<lbrakk>\<forall>x. P x = P (free_index_update (\<lambda>_. y) x); caps_of_state s (a, b) = Some capaa; P capaa; p \<in> cte_refs capaa (interrupt_irq_node s); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; 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\<rbrakk> \<Longrightarrow> \<exists>a b. ((a, b) = dest \<longrightarrow> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)) \<and> ((a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s))) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa. \<lbrakk>\<forall>x. P x = P (free_index_update (\<lambda>_. y) x); caps_of_state s (a, b) = Some capaa; P capaa; p \<in> cte_refs capaa (interrupt_irq_node s); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; 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\<rbrakk> \<Longrightarrow> \<exists>b. ((a, b) = dest \<longrightarrow> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)) \<and> ((a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s))) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa. \<lbrakk>\<forall>x. P x = P (free_index_update (\<lambda>_. y) x); caps_of_state s (a, b) = Some capaa; P capaa; p \<in> cte_refs capaa (interrupt_irq_node s); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; 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\<rbrakk> \<Longrightarrow> ((a, b) = dest \<longrightarrow> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)) \<and> ((a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s))) proof (prove)
goal:
No subgoals!