theory CNodeInv_R

lemma valid_Zombie_cte_at':
  "\<lbrakk> s \<turnstile>' Zombie p zt m; n < zombieCTEs zt \<rbrakk> \<Longrightarrow> cte_at' (p + (of_nat n * 2^cteSizeBits)) s" apply (clarsimp simp: valid_cap'_def split: zombie_type.split_asm) apply (clarsimp simp: obj_at'_def projectKOs objBits_simps) apply (subgoal_tac "tcb_cte_cases (of_nat n * 2^cteSizeBits) \<noteq> None") apply clarsimp apply (erule(2) cte_wp_at_tcbI') apply fastforce apply simp apply (thin_tac "a < word_bits" for a) apply ((clarsimp | erule less_handy_casesE | fastforce simp: objBits_defs)+)[1] apply (drule spec[where x="of_nat n"]) apply (subst(asm) less_mask_eq) apply (rule order_less_le_trans) apply (erule of_nat_mono_maybe [rotated]) apply (rule power_strict_increasing) apply (simp add: word_bits_def) apply simp apply simp apply (clarsimp simp: mult.commute mult.left_commute real_cte_at') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' (capability.Zombie p zt m) s; n < zombieCTEs zt\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 5; zt = ZombieTCB; capAligned (capability.Zombie p ZombieTCB m); m \<le> 5; tcbBlockSizeBits < word_bits; tcb_at' p s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s
 2. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; \<forall>addr. real_cte_at' (p + 2 ^ cteSizeBits * (addr && mask x2)) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (2 subgoals):
 1. \<And>obj. \<lbrakk>n < 5; zt = ZombieTCB; capAligned (capability.Zombie p ZombieTCB m); m \<le> 5; tcbBlockSizeBits < word_bits; ksPSpace s p = Some (KOTCB obj); is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s
 2. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; \<forall>addr. real_cte_at' (p + 2 ^ cteSizeBits * (addr && mask x2)) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (3 subgoals):
 1. \<And>obj. \<lbrakk>n < 5; zt = ZombieTCB; capAligned (capability.Zombie p ZombieTCB m); m \<le> 5; tcbBlockSizeBits < word_bits; ksPSpace s p = Some (KOTCB obj); is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; tcb_cte_cases (word_of_nat n * 2 ^ cteSizeBits) \<noteq> None\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s
 2. \<And>obj. \<lbrakk>n < 5; zt = ZombieTCB; capAligned (capability.Zombie p ZombieTCB m); m \<le> 5; tcbBlockSizeBits < word_bits; ksPSpace s p = Some (KOTCB obj); is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> tcb_cte_cases (word_of_nat n * 2 ^ cteSizeBits) \<noteq> None
 3. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; \<forall>addr. real_cte_at' (p + 2 ^ cteSizeBits * (addr && mask x2)) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (3 subgoals):
 1. \<And>obj a b. \<lbrakk>n < 5; zt = ZombieTCB; capAligned (capability.Zombie p ZombieTCB m); m \<le> 5; tcbBlockSizeBits < word_bits; ksPSpace s p = Some (KOTCB obj); is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; tcb_cte_cases (word_of_nat n * 2 ^ cteSizeBits) = Some (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s
 2. \<And>obj. \<lbrakk>n < 5; zt = ZombieTCB; capAligned (capability.Zombie p ZombieTCB m); m \<le> 5; tcbBlockSizeBits < word_bits; ksPSpace s p = Some (KOTCB obj); is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> tcb_cte_cases (word_of_nat n * 2 ^ cteSizeBits) \<noteq> None
 3. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; \<forall>addr. real_cte_at' (p + 2 ^ cteSizeBits * (addr && mask x2)) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (4 subgoals):
 1. \<And>obj a b. \<lbrakk>n < 5; zt = ZombieTCB; capAligned (capability.Zombie p ZombieTCB m); m \<le> 5; tcbBlockSizeBits < word_bits; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; tcb_cte_cases (word_of_nat n * 2 ^ cteSizeBits) = Some (a, b)\<rbrakk> \<Longrightarrow> tcb_cte_cases (p + word_of_nat n * 2 ^ cteSizeBits - p) = Some (?getF36 obj a b, ?setF36 obj a b)
 2. \<And>obj a b. \<lbrakk>n < 5; zt = ZombieTCB; capAligned (capability.Zombie p ZombieTCB m); m \<le> 5; tcbBlockSizeBits < word_bits; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; tcb_cte_cases (word_of_nat n * 2 ^ cteSizeBits) = Some (a, b)\<rbrakk> \<Longrightarrow> True
 3. \<And>obj. \<lbrakk>n < 5; zt = ZombieTCB; capAligned (capability.Zombie p ZombieTCB m); m \<le> 5; tcbBlockSizeBits < word_bits; ksPSpace s p = Some (KOTCB obj); is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> tcb_cte_cases (word_of_nat n * 2 ^ cteSizeBits) \<noteq> None
 4. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; \<forall>addr. real_cte_at' (p + 2 ^ cteSizeBits * (addr && mask x2)) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (3 subgoals):
 1. \<And>obj a b. \<lbrakk>n < 5; zt = ZombieTCB; capAligned (capability.Zombie p ZombieTCB m); m \<le> 5; tcbBlockSizeBits < word_bits; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; tcb_cte_cases (word_of_nat n * 2 ^ cteSizeBits) = Some (a, b)\<rbrakk> \<Longrightarrow> True
 2. \<And>obj. \<lbrakk>n < 5; zt = ZombieTCB; capAligned (capability.Zombie p ZombieTCB m); m \<le> 5; tcbBlockSizeBits < word_bits; ksPSpace s p = Some (KOTCB obj); is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> tcb_cte_cases (word_of_nat n * 2 ^ cteSizeBits) \<noteq> None
 3. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; \<forall>addr. real_cte_at' (p + 2 ^ cteSizeBits * (addr && mask x2)) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (2 subgoals):
 1. \<And>obj. \<lbrakk>n < 5; zt = ZombieTCB; capAligned (capability.Zombie p ZombieTCB m); m \<le> 5; tcbBlockSizeBits < word_bits; ksPSpace s p = Some (KOTCB obj); is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> tcb_cte_cases (word_of_nat n * 2 ^ cteSizeBits) \<noteq> None
 2. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; \<forall>addr. real_cte_at' (p + 2 ^ cteSizeBits * (addr && mask x2)) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (2 subgoals):
 1. \<And>obj. \<lbrakk>n < 5; zt = ZombieTCB; capAligned (capability.Zombie p ZombieTCB m); m \<le> 5; ksPSpace s p = Some (KOTCB obj); is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> tcb_cte_cases (word_of_nat n * 2 ^ cteSizeBits) \<noteq> None
 2. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; \<forall>addr. real_cte_at' (p + 2 ^ cteSizeBits * (addr && mask x2)) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; \<forall>addr. real_cte_at' (p + 2 ^ cteSizeBits * (addr && mask x2)) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; real_cte_at' (p + 2 ^ cteSizeBits * (word_of_nat n && mask x2)) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2\<rbrakk> \<Longrightarrow> word_of_nat n < 2 ^ x2
 2. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; real_cte_at' (p + 2 ^ cteSizeBits * word_of_nat n) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2\<rbrakk> \<Longrightarrow> word_of_nat n < ?y91 x2
 2. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2\<rbrakk> \<Longrightarrow> ?y91 x2 \<le> 2 ^ x2
 3. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; real_cte_at' (p + 2 ^ cteSizeBits * word_of_nat n) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2\<rbrakk> \<Longrightarrow> 2 ^ x2 < 2 ^ LENGTH(32)
 2. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2\<rbrakk> \<Longrightarrow> word_of_nat (2 ^ x2) \<le> 2 ^ x2
 3. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; real_cte_at' (p + 2 ^ cteSizeBits * word_of_nat n) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2\<rbrakk> \<Longrightarrow> x2 < LENGTH(32)
 2. \<And>x2. \<lbrakk>zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2\<rbrakk> \<Longrightarrow> 1 < 2
 3. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2\<rbrakk> \<Longrightarrow> word_of_nat (2 ^ x2) \<le> 2 ^ x2
 4. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; real_cte_at' (p + 2 ^ cteSizeBits * word_of_nat n) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2\<rbrakk> \<Longrightarrow> 1 < 2
 2. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2\<rbrakk> \<Longrightarrow> word_of_nat (2 ^ x2) \<le> 2 ^ x2
 3. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; real_cte_at' (p + 2 ^ cteSizeBits * word_of_nat n) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2\<rbrakk> \<Longrightarrow> word_of_nat (2 ^ x2) \<le> 2 ^ x2
 2. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; real_cte_at' (p + 2 ^ cteSizeBits * word_of_nat n) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>n < 2 ^ x2; zt = ZombieCNode x2; capAligned (capability.Zombie p (ZombieCNode x2) m); m \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; real_cte_at' (p + 2 ^ cteSizeBits * word_of_nat n) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (p + word_of_nat n * 2 ^ cteSizeBits) s proof (prove)
goal:
No subgoals!