theory Tcb_AI

lemma (in Tcb_AI_1) checked_insert_no_cap_to:
  "\<lbrace>no_cap_to_obj_with_diff_ref c' {} and
        no_cap_to_obj_with_diff_ref a {}\<rbrace>
     check_cap_at a b (check_cap_at c d (cap_insert a b e))
   \<lbrace>\<lambda>r. no_cap_to_obj_with_diff_ref c' {}\<rbrace>" apply (simp add: check_cap_at_def cap_insert_def
                   cte_wp_at_caps_of_state set_untyped_cap_as_full_def
                   no_cap_to_obj_with_diff_ref_def) apply (wp get_cap_wp
               | simp split del: if_split)+ apply (clarsimp simp: cte_wp_at_caps_of_state) apply (clarsimp dest!: same_object_obj_refs) apply (cases b, cases d, clarsimp) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_cap_to_obj_dr_emp c' and no_cap_to_obj_dr_emp a\<rbrace> check_cap_at a b (check_cap_at c d (cap_insert a b e)) \<lbrace>\<lambda>r. no_cap_to_obj_dr_emp c'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>a b cap. obj_refs cap = obj_refs c' \<longrightarrow> caps_of_state s (a, b) = Some cap \<longrightarrow> table_cap_ref cap = table_cap_ref c') and (\<lambda>s. \<forall>aa b cap. obj_refs cap = obj_refs a \<longrightarrow> caps_of_state s (aa, b) = Some cap \<longrightarrow> table_cap_ref cap = table_cap_ref a)\<rbrace> do cap' <- get_cap b;
when (same_object_as a cap') (do cap' <- get_cap d;
when (same_object_as c cap') (do src_cap <- get_cap b;
old_cap <- get_cap e;
y <- assert (old_cap = NullCap);
y <- if is_untyped_cap src_cap \<and> is_untyped_cap a \<and> obj_ref_of src_cap = obj_ref_of a \<and> cap_bits_untyped src_cap = cap_bits_untyped a then set_cap (max_free_index_update src_cap) b else return ();
y <- set_cap a e;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s b);
dest_p <- gets (\<lambda>s. cdt s e);
y <- update_cdt (\<lambda>cdt. cdt(e := if should_be_parent_of src_cap (is_original b) a (is_cap_revocable a src_cap) then Some b else cdt b));
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original b) a (is_cap_revocable a src_cap)) b e src_p dest_p);
set_original e (is_cap_revocable a src_cap)
od)
od)
od \<lbrace>\<lambda>r s. \<forall>a b cap. obj_refs cap = obj_refs c' \<longrightarrow> caps_of_state s (a, b) = Some cap \<longrightarrow> table_cap_ref cap = table_cap_ref c'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>a b cap. obj_refs cap = obj_refs c' \<longrightarrow> caps_of_state s (a, b) = Some cap \<longrightarrow> table_cap_ref cap = table_cap_ref c') \<and> (\<forall>aa b cap. obj_refs cap = obj_refs a \<longrightarrow> caps_of_state s (aa, b) = Some cap \<longrightarrow> table_cap_ref cap = table_cap_ref a) \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) b s \<longrightarrow> (if same_object_as a cap then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) d s \<longrightarrow> (if same_object_as c cap then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) b s \<longrightarrow> cte_wp_at ((=) NullCap) e s \<longrightarrow> (is_untyped_cap cap \<and> is_untyped_cap a \<and> obj_ref_of cap = obj_ref_of a \<and> cap_bits_untyped cap = cap_bits_untyped a \<longrightarrow> (\<forall>aa ba capa. obj_refs capa = obj_refs c' \<longrightarrow> (if (aa, ba) = e then Some a else if (aa, ba) = b then Some (max_free_index_update cap) else caps_of_state s (aa, ba)) = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref c')) \<and> ((obj_ref_of cap = obj_ref_of a \<longrightarrow> is_untyped_cap a \<longrightarrow> is_untyped_cap cap \<longrightarrow> cap_bits_untyped cap \<noteq> cap_bits_untyped a) \<longrightarrow> (\<forall>aa b cap. obj_refs cap = obj_refs c' \<longrightarrow> (if (aa, b) = e then Some a else caps_of_state s (aa, b)) = Some cap \<longrightarrow> table_cap_ref cap = table_cap_ref c')) else (\<lambda>s. \<forall>a b cap. obj_refs cap = obj_refs c' \<longrightarrow> caps_of_state s (a, b) = Some cap \<longrightarrow> table_cap_ref cap = table_cap_ref c')) s else (\<lambda>s. \<forall>a b cap. obj_refs cap = obj_refs c' \<longrightarrow> caps_of_state s (a, b) = Some cap \<longrightarrow> table_cap_ref cap = table_cap_ref c')) s proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>\<forall>a b cap. obj_refs cap = obj_refs c' \<longrightarrow> caps_of_state s (a, b) = Some cap \<longrightarrow> table_cap_ref cap = table_cap_ref c'; \<forall>aa b cap. obj_refs cap = obj_refs a \<longrightarrow> caps_of_state s (aa, b) = Some cap \<longrightarrow> table_cap_ref cap = table_cap_ref a; same_object_as a cap; caps_of_state s b = Some cap; same_object_as c capa; caps_of_state s d = Some capa; caps_of_state s e = Some NullCap\<rbrakk> \<Longrightarrow> (is_untyped_cap cap \<and> is_untyped_cap a \<and> obj_ref_of cap = obj_ref_of a \<and> cap_bits_untyped cap = cap_bits_untyped a \<longrightarrow> (\<forall>aa ba. ((aa, ba) = b \<longrightarrow> (b = e \<longrightarrow> obj_refs a = obj_refs c' \<longrightarrow> table_cap_ref a = table_cap_ref c') \<and> (b \<noteq> e \<longrightarrow> obj_refs cap = obj_refs c' \<longrightarrow> table_cap_ref cap = table_cap_ref c')) \<and> ((aa, ba) \<noteq> b \<longrightarrow> (aa, ba) = e \<longrightarrow> obj_refs a = obj_refs c' \<longrightarrow> table_cap_ref a = table_cap_ref c'))) \<and> ((obj_ref_of cap = obj_ref_of a \<longrightarrow> is_untyped_cap a \<longrightarrow> is_untyped_cap cap \<longrightarrow> cap_bits_untyped cap \<noteq> cap_bits_untyped a) \<longrightarrow> (\<exists>a b. (a, b) = e) \<longrightarrow> obj_refs a = obj_refs c' \<longrightarrow> table_cap_ref a = table_cap_ref c') proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>\<forall>a b cap. obj_refs cap = obj_refs c' \<longrightarrow> caps_of_state s (a, b) = Some cap \<longrightarrow> table_cap_ref cap = table_cap_ref c'; \<forall>aa b capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s (aa, b) = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref a; caps_of_state s b = Some cap; caps_of_state s d = Some capa; caps_of_state s e = Some NullCap; obj_refs a = obj_refs cap; obj_refs c = obj_refs capa\<rbrakk> \<Longrightarrow> (is_untyped_cap cap \<and> is_untyped_cap a \<and> obj_ref_of cap = obj_ref_of a \<and> cap_bits_untyped cap = cap_bits_untyped a \<longrightarrow> (\<forall>aa ba. ((aa, ba) = b \<longrightarrow> (b = e \<longrightarrow> obj_refs cap = obj_refs c' \<longrightarrow> table_cap_ref a = table_cap_ref c') \<and> (b \<noteq> e \<longrightarrow> obj_refs cap = obj_refs c' \<longrightarrow> table_cap_ref cap = table_cap_ref c')) \<and> ((aa, ba) \<noteq> b \<longrightarrow> (aa, ba) = e \<longrightarrow> obj_refs cap = obj_refs c' \<longrightarrow> table_cap_ref a = table_cap_ref c'))) \<and> ((obj_ref_of cap = obj_ref_of a \<longrightarrow> is_untyped_cap a \<longrightarrow> is_untyped_cap cap \<longrightarrow> cap_bits_untyped cap \<noteq> cap_bits_untyped a) \<longrightarrow> (\<exists>a b. (a, b) = e) \<longrightarrow> obj_refs cap = obj_refs c' \<longrightarrow> table_cap_ref a = table_cap_ref c') proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa aa ba aaa baa. \<lbrakk>\<forall>a b cap. obj_refs cap = obj_refs c' \<longrightarrow> caps_of_state s (a, b) = Some cap \<longrightarrow> table_cap_ref cap = table_cap_ref c'; \<forall>aa b capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s (aa, b) = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref a; caps_of_state s (aa, ba) = Some cap; caps_of_state s (aaa, baa) = Some capa; caps_of_state s e = Some NullCap; obj_refs a = obj_refs cap; obj_refs c = obj_refs capa; b = (aa, ba); d = (aaa, baa)\<rbrakk> \<Longrightarrow> (is_untyped_cap cap \<and> is_untyped_cap a \<and> obj_ref_of cap = obj_ref_of a \<and> cap_bits_untyped cap = cap_bits_untyped a \<longrightarrow> (\<forall>ab b. (ab = aa \<and> b = ba \<longrightarrow> (aa, ba) = e \<longrightarrow> obj_refs cap = obj_refs c' \<longrightarrow> table_cap_ref a = table_cap_ref c') \<and> ((ab = aa \<longrightarrow> b \<noteq> ba) \<longrightarrow> (ab, b) = e \<longrightarrow> obj_refs cap = obj_refs c' \<longrightarrow> table_cap_ref a = table_cap_ref c'))) \<and> ((obj_ref_of cap = obj_ref_of a \<longrightarrow> is_untyped_cap a \<longrightarrow> is_untyped_cap cap \<longrightarrow> cap_bits_untyped cap \<noteq> cap_bits_untyped a) \<longrightarrow> (\<exists>a b. (a, b) = e) \<longrightarrow> obj_refs cap = obj_refs c' \<longrightarrow> table_cap_ref a = table_cap_ref c') proof (prove)
goal:
No subgoals!