theory VSpacePre_AI

lemma arch_update_cap_pspace:
  "\<lbrace>cte_wp_at (is_arch_update cap and
               (\<lambda>c. is_valid_vtable_root c \<longrightarrow> is_valid_vtable_root cap)) p
    and valid_pspace and valid_cap cap\<rbrace>
     set_cap cap p
  \<lbrace>\<lambda>rv. valid_pspace\<rbrace>" apply (simp add: valid_pspace_def) apply (rule hoare_pre) apply (wp set_cap_valid_objs update_cap_iflive arch_update_cap_zombies) apply clarsimp apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_update_def) apply (frule cap_master_cap_zobj_refs) apply clarsimp apply (drule caps_of_state_cteD) apply (drule (1) cte_wp_tcb_cap_valid) apply (clarsimp simp: cap_master_cap_tcb_cap_valid_arch) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (is_arch_update cap and (\<lambda>c. is_valid_vtable_root c \<longrightarrow> is_valid_vtable_root cap)) p and valid_pspace and valid_cap cap\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (is_arch_update cap and (\<lambda>c. is_valid_vtable_root c \<longrightarrow> is_valid_vtable_root cap)) p and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s))) and valid_cap cap\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s))\<rbrace>
 2. \<And>s. (cte_wp_at (is_arch_update cap and (\<lambda>c. is_valid_vtable_root c \<longrightarrow> is_valid_vtable_root cap)) p and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s))) and valid_cap cap) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at (is_arch_update cap and (\<lambda>c. is_valid_vtable_root c \<longrightarrow> is_valid_vtable_root cap)) p and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s))) and valid_cap cap) s \<Longrightarrow> (valid_objs and valid_cap cap and tcb_cap_valid cap p) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (cte_wp_at (\<lambda>cap'. zobj_refs cap' = zobj_refs cap) p and if_live_then_nonz_cap) s \<and> (cte_wp_at (is_arch_update cap) p s \<and> zombies_final s) \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cte_wp_at (is_arch_update cap and (\<lambda>c. is_valid_vtable_root c \<longrightarrow> is_valid_vtable_root cap)) p s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); s \<turnstile> cap\<rbrakk> \<Longrightarrow> tcb_cap_valid cap p s \<and> cte_wp_at (\<lambda>cap'. zobj_refs cap' = zobj_refs cap) p s \<and> cte_wp_at (is_arch_update cap) p s proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); s \<turnstile> cap; caps_of_state s p = Some capa; is_arch_cap cap; cap_master_cap cap = cap_master_cap capa; is_valid_vtable_root capa \<longrightarrow> is_valid_vtable_root cap\<rbrakk> \<Longrightarrow> tcb_cap_valid cap p s \<and> zobj_refs capa = zobj_refs cap proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); s \<turnstile> cap; caps_of_state s p = Some capa; is_arch_cap cap; cap_master_cap cap = cap_master_cap capa; is_valid_vtable_root capa \<longrightarrow> is_valid_vtable_root cap; zobj_refs cap = zobj_refs capa\<rbrakk> \<Longrightarrow> tcb_cap_valid cap p s \<and> zobj_refs capa = zobj_refs cap proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); s \<turnstile> cap; caps_of_state s p = Some capa; is_arch_cap cap; cap_master_cap cap = cap_master_cap capa; is_valid_vtable_root capa \<longrightarrow> is_valid_vtable_root cap; zobj_refs cap = zobj_refs capa\<rbrakk> \<Longrightarrow> tcb_cap_valid cap p s proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); s \<turnstile> cap; is_arch_cap cap; cap_master_cap cap = cap_master_cap capa; is_valid_vtable_root capa \<longrightarrow> is_valid_vtable_root cap; zobj_refs cap = zobj_refs capa; cte_wp_at ((=) capa) p s\<rbrakk> \<Longrightarrow> tcb_cap_valid cap p s proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); s \<turnstile> cap; is_arch_cap cap; cap_master_cap cap = cap_master_cap capa; is_valid_vtable_root capa \<longrightarrow> is_valid_vtable_root cap; zobj_refs cap = zobj_refs capa; tcb_cap_valid capa p s\<rbrakk> \<Longrightarrow> tcb_cap_valid cap p s proof (prove)
goal:
No subgoals!