theory CNodeInv_R

lemma valid_cap'_handy_bits:
  "s \<turnstile>' Zombie r zb n \<Longrightarrow> n \<le> 2 ^ (zBits zb)"
  "s \<turnstile>' Zombie r zb n \<Longrightarrow> n < 2 ^ word_bits"
  "\<lbrakk> s \<turnstile>' Zombie r zb n; n \<noteq> 0 \<rbrakk> \<Longrightarrow> of_nat n - 1 < (2 ^ (zBits zb) :: word32)"
  "s \<turnstile>' Zombie r zb n \<Longrightarrow> zBits zb < word_bits" apply (insert zombieCTEs_le[where zb=zb],
         simp_all add: valid_cap'_def) apply (clarsimp elim!: order_le_less_trans) apply (clarsimp simp: word_less_nat_alt) apply (subgoal_tac "n \<in> unats (len_of TYPE (32))") apply (subst unat_minus_one) apply (drule of_nat_mono_maybe[rotated, where 'a=32]) apply (simp add: unats_def) apply simp apply (simp add: word_unat.Abs_inverse) apply (simp only: unats_def mem_simps) apply (erule order_le_less_trans) apply (erule order_le_less_trans) apply (rule power_strict_increasing) apply (simp only: word_bits_len_of) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((valid_cap' (capability.Zombie r zb n) s \<Longrightarrow> n \<le> 2 ^ zBits zb) &&& (valid_cap' (capability.Zombie r zb n) s \<Longrightarrow> n < 2 ^ word_bits)) &&& (\<lbrakk>valid_cap' (capability.Zombie r zb n) s; n \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat n - 1 < 2 ^ zBits zb) &&& (valid_cap' (capability.Zombie r zb n) s \<Longrightarrow> zBits zb < word_bits) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>capAligned (capability.Zombie r zb n) \<and> n \<le> zombieCTEs zb \<and> zBits zb < word_bits \<and> (case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)); zombieCTEs zb \<le> 2 ^ zBits zb\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 2. \<lbrakk>capAligned (capability.Zombie r zb n) \<and> n \<le> zombieCTEs zb \<and> zBits zb < word_bits \<and> (case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)); 0 < n; zombieCTEs zb \<le> 2 ^ zBits zb\<rbrakk> \<Longrightarrow> word_of_nat n - 1 < 2 ^ zBits zb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capAligned (capability.Zombie r zb n) \<and> n \<le> zombieCTEs zb \<and> zBits zb < word_bits \<and> (case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)); 0 < n; zombieCTEs zb \<le> 2 ^ zBits zb\<rbrakk> \<Longrightarrow> word_of_nat n - 1 < 2 ^ zBits zb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) < 2 ^ zBits zb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s); n \<in> unats LENGTH(32)\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) < 2 ^ zBits zb
 2. \<lbrakk>0 < n; zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> n \<in> unats LENGTH(32) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s); n \<in> unats LENGTH(32)\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0
 2. \<lbrakk>0 < n; zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s); n \<in> unats LENGTH(32)\<rbrakk> \<Longrightarrow> unat (word_of_nat n) - 1 < 2 ^ zBits zb
 3. \<lbrakk>0 < n; zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> n \<in> unats LENGTH(32) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s); n \<in> unats LENGTH(32)\<rbrakk> \<Longrightarrow> n < 2 ^ LENGTH(32)
 2. \<lbrakk>zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s); n \<in> unats LENGTH(32); word_of_nat 0 < word_of_nat n\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0
 3. \<lbrakk>0 < n; zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s); n \<in> unats LENGTH(32)\<rbrakk> \<Longrightarrow> unat (word_of_nat n) - 1 < 2 ^ zBits zb
 4. \<lbrakk>0 < n; zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> n \<in> unats LENGTH(32) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s); n \<in> unats LENGTH(32); word_of_nat 0 < word_of_nat n\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0
 2. \<lbrakk>0 < n; zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s); n \<in> unats LENGTH(32)\<rbrakk> \<Longrightarrow> unat (word_of_nat n) - 1 < 2 ^ zBits zb
 3. \<lbrakk>0 < n; zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> n \<in> unats LENGTH(32) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s); n \<in> unats LENGTH(32)\<rbrakk> \<Longrightarrow> unat (word_of_nat n) - 1 < 2 ^ zBits zb
 2. \<lbrakk>0 < n; zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> n \<in> unats LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> n \<in> unats LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); n \<le> zombieCTEs zb; zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> n < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; zombieCTEs zb \<le> 2 ^ zBits zb; capAligned (capability.Zombie r zb n); zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> zombieCTEs zb < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; capAligned (capability.Zombie r zb n); zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> 2 ^ zBits zb < 2 ^ LENGTH(32) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; capAligned (capability.Zombie r zb n); zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> zBits zb < LENGTH(32)
 2. \<lbrakk>0 < n; capAligned (capability.Zombie r zb n); zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> 1 < 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; capAligned (capability.Zombie r zb n); zBits zb < word_bits; case zb of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> 1 < 2 proof (prove)
goal:
No subgoals!