theory ArchArch_AI

lemma max_index_upd_no_cap_to:
  "\<lbrace>\<lambda>s. no_cap_to_obj_with_diff_ref cap {slot} s \<and>
        cte_wp_at ((=) ucap) cref s \<and> is_untyped_cap ucap\<rbrace>
   set_cap (max_free_index_update ucap) cref
   \<lbrace>\<lambda>rv s. no_cap_to_obj_with_diff_ref cap {slot} s \<rbrace>" apply (clarsimp simp:no_cap_to_obj_with_diff_ref_def) apply (wp hoare_vcg_ball_lift set_cap_cte_wp_at_neg) apply (clarsimp simp:cte_wp_at_caps_of_state free_index_update_def is_cap_simps) apply (drule_tac x = cref in bspec) apply clarsimp apply (clarsimp simp:table_cap_ref_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_cap_to_obj_with_diff_ref cap {slot} s \<and> cte_wp_at ((=) ucap) cref s \<and> is_untyped_cap ucap\<rbrace> set_cap (max_free_index_update ucap) cref \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap {slot}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>p\<in>UNIV - {slot}. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) p s) \<and> cte_wp_at ((=) ucap) cref s \<and> is_untyped_cap ucap\<rbrace> set_cap (max_free_index_update ucap) cref \<lbrace>\<lambda>rv s. \<forall>p\<in>UNIV - {slot}. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>p\<in>UNIV - {slot}. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) p s) \<and> cte_wp_at ((=) ucap) cref s \<and> is_untyped_cap ucap \<Longrightarrow> \<forall>x\<in>UNIV - {slot}. cte_wp_at (\<lambda>_. True) cref s \<and> (if x = cref then \<not> (obj_refs (max_free_index_update ucap) = obj_refs cap \<and> table_cap_ref (max_free_index_update ucap) \<noteq> table_cap_ref cap) else \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>\<forall>p\<in>UNIV - {slot}. \<forall>capa. obj_refs capa = {} \<longrightarrow> caps_of_state s p = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap; caps_of_state s cref = Some (UntypedCap dev r bits f); ucap = UntypedCap dev r bits f; cref \<noteq> slot; {} = obj_refs cap\<rbrakk> \<Longrightarrow> table_cap_ref (UntypedCap dev r bits (max_free_index bits)) = table_cap_ref cap proof (prove)
goal (2 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev r bits f); ucap = UntypedCap dev r bits f; cref \<noteq> slot; {} = obj_refs cap\<rbrakk> \<Longrightarrow> cref \<in> UNIV - {slot}
 2. \<And>s dev r bits f. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev r bits f); ucap = UntypedCap dev r bits f; cref \<noteq> slot; {} = obj_refs cap; \<forall>capa. obj_refs capa = {} \<longrightarrow> caps_of_state s cref = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap\<rbrakk> \<Longrightarrow> table_cap_ref (UntypedCap dev r bits (max_free_index bits)) = table_cap_ref cap proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev r bits f); ucap = UntypedCap dev r bits f; cref \<noteq> slot; {} = obj_refs cap; \<forall>capa. obj_refs capa = {} \<longrightarrow> caps_of_state s cref = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap\<rbrakk> \<Longrightarrow> table_cap_ref (UntypedCap dev r bits (max_free_index bits)) = table_cap_ref cap proof (prove)
goal:
No subgoals!