theory CSpaceInv_AI

lemma cap_insert_ifunsafe:
  "\<lbrace>if_unsafe_then_cap and
    ex_cte_cap_wp_to (appropriate_cte_cap cap) dest\<rbrace>
     cap_insert cap src dest
   \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>" apply (simp add: cap_insert_def) apply (wp get_cap_wp | simp split del: if_split)+ apply (rule new_cap_ifunsafe) apply (simp add: set_untyped_cap_as_full_def split del: if_split) apply (wp set_cap_cte_wp_at set_cap_ifunsafe set_cap_cte_cap_wp_to get_cap_wp)+ apply (clarsimp simp: is_cap_simps cte_wp_at_caps_of_state) apply (rule untyped_cap_update_ex_cte_cap_wp_to) apply (simp add: free_index_update_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest\<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>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>src_cap x. \<lbrace>?B4 src_cap x () ()\<rbrace> set_cap cap dest \<lbrace>\<lambda>yb. if_unsafe_then_cap\<rbrace>
 2. \<And>src_cap x y. \<lbrace>?B3 src_cap x y\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>?B4 src_cap x y\<rbrace>
 3. \<And>src_cap x. \<lbrace>?B2 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>?B3 src_cap x\<rbrace>
 4. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 6. \<And>s. (if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>src_cap x y. \<lbrace>?B3 src_cap x y\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>a. cte_wp_at ((=) NullCap) dest and if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest\<rbrace>
 2. \<And>src_cap x. \<lbrace>?B2 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>?B3 src_cap x\<rbrace>
 3. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 5. \<And>s. (if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>src_cap x. \<lbrace>?B3 src_cap x ()\<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>a b. cte_wp_at ((=) NullCap) dest b \<and> if_unsafe_then_cap b \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) dest b\<rbrace>
 2. \<And>src_cap x. \<lbrace>?B2 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>?B3 src_cap x\<rbrace>
 3. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 5. \<And>s. (if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest) s \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> (\<forall>capb. cte_wp_at ((=) capb) dest s \<longrightarrow> capb = NullCap \<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> ((\<lambda>s. if dest = src then NullCap = max_free_index_update capa else cte_wp_at ((=) NullCap) dest s) and cte_wp_at (\<lambda>_. True) src) s \<and> (cte_wp_at (\<lambda>cap'. \<forall>p'. p' \<in> cte_refs cap' (interrupt_irq_node s) \<and> (p' \<notin> cte_refs (max_free_index_update capa) (interrupt_irq_node s) \<or> (\<exists>cp. appropriate_cte_cap cp cap' \<and> \<not> appropriate_cte_cap cp (max_free_index_update capa))) \<longrightarrow> (p' \<noteq> src \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = src \<longrightarrow> max_free_index_update capa = NullCap)) src s \<and> if_unsafe_then_cap s \<and> (max_free_index_update capa \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (max_free_index_update capa)) src s)) \<and> cte_wp_at (\<lambda>cap'. dest \<in> cte_refs cap' (interrupt_irq_node s) \<and> appropriate_cte_cap cap cap' \<longrightarrow> dest \<in> cte_refs (max_free_index_update capa) (interrupt_irq_node s) \<and> appropriate_cte_cap cap (max_free_index_update capa)) src s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s) \<and> (\<not> (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> cte_wp_at ((=) NullCap) dest s \<and> if_unsafe_then_cap s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev f deva ra bitsa fa. \<lbrakk>if_unsafe_then_cap s; ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap deva ra bitsa fa)) dest s; dest \<noteq> src; caps_of_state s src = Some (UntypedCap dev ra bitsa f); caps_of_state s dest = Some NullCap; cap = UntypedCap deva ra bitsa fa; free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f) \<noteq> NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f))) src s proof (prove)
goal (4 subgoals):
 1. \<And>s dev f deva ra bitsa fa. \<lbrakk>if_unsafe_then_cap s; ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap deva ra bitsa fa)) dest s; dest \<noteq> src; caps_of_state s src = Some (UntypedCap dev ra bitsa f); caps_of_state s dest = Some NullCap; cap = UntypedCap deva ra bitsa fa; free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f) \<noteq> NullCap\<rbrakk> \<Longrightarrow> if_unsafe_then_cap s
 2. \<And>s dev f deva ra bitsa fa. \<lbrakk>if_unsafe_then_cap s; ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap deva ra bitsa fa)) dest s; dest \<noteq> src; caps_of_state s src = Some (UntypedCap dev ra bitsa f); caps_of_state s dest = Some NullCap; cap = UntypedCap deva ra bitsa fa; free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f) \<noteq> NullCap\<rbrakk> \<Longrightarrow> caps_of_state s src = Some (?src_cap83 s dev f deva ra bitsa fa)
 3. \<And>s dev f deva ra bitsa fa. \<lbrakk>if_unsafe_then_cap s; ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap deva ra bitsa fa)) dest s; dest \<noteq> src; caps_of_state s src = Some (UntypedCap dev ra bitsa f); caps_of_state s dest = Some NullCap; cap = UntypedCap deva ra bitsa fa; free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f) \<noteq> NullCap\<rbrakk> \<Longrightarrow> is_untyped_cap (?src_cap83 s dev f deva ra bitsa fa)
 4. \<And>s dev f deva ra bitsa fa. \<lbrakk>if_unsafe_then_cap s; ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap deva ra bitsa fa)) dest s; dest \<noteq> src; caps_of_state s src = Some (UntypedCap dev ra bitsa f); caps_of_state s dest = Some NullCap; cap = UntypedCap deva ra bitsa fa; free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f) \<noteq> NullCap\<rbrakk> \<Longrightarrow> is_untyped_cap (free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f)) proof (prove)
goal:
No subgoals!