theory CNodeInv_R

lemma zombie_alignment_oddity:
  "\<lbrakk> cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s;
     invs s \<rbrakk> \<Longrightarrow> (cte_map slot, replicate (zombie_cte_bits zb) False) = slot" apply (frule cte_wp_at_valid_objs_valid_cap, clarsimp+) apply (rule cte_map_inj_eq) apply (simp only: cte_map_replicate) apply (erule cte_at_replicate_zbits) apply (erule cte_wp_at_weakenE, simp) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s\<rbrakk> \<Longrightarrow> (cte_map slot, replicate (zombie_cte_bits zb) False) = slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> (cte_map slot, replicate (zombie_cte_bits zb) False) = slot proof (prove)
goal (6 subgoals):
 1. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> cte_map (cte_map slot, replicate (zombie_cte_bits zb) False) = cte_map slot
 2. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (cte_map slot, replicate (zombie_cte_bits zb) False) ?s6
 3. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot ?s6
 4. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> valid_objs ?s6
 5. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> pspace_aligned ?s6
 6. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> pspace_distinct ?s6 proof (prove)
goal (5 subgoals):
 1. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (cte_map slot, replicate (zombie_cte_bits zb) False) ?s6
 2. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot ?s6
 3. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> valid_objs ?s6
 4. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> pspace_aligned ?s6
 5. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> pspace_distinct ?s6 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 2. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> pspace_aligned s
 4. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> pspace_distinct s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> pspace_aligned s
 3. \<lbrakk>cte_wp_at (\<lambda>c. c = cap.Zombie (cte_map slot) zb n) slot s; invs s; s \<turnstile> cap.Zombie (cte_map slot) zb n\<rbrakk> \<Longrightarrow> pspace_distinct s proof (prove)
goal:
No subgoals!