theory CNodeInv_R

lemma spec_corres_locate_Zombie:
  "\<lbrakk> P s \<Longrightarrow> valid_cap (cap.Zombie ptr bits (Suc n)) s;
      spec_corres s r P P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))) \<rbrakk>
    \<Longrightarrow> spec_corres s r P P' f (locateSlotCap (Zombie ptr (zbits_map bits) (Suc n)) (of_nat n) >>= f')" unfolding spec_corres_def apply (simp add: locateSlot_conv cte_level_bits_def stateAssert_def bind_assoc) apply (rule corres_symb_exec_r[OF _ get_sp]) apply (rule corres_assume_pre, clarsimp) apply (frule cte_at_nat_to_cref_zbits, rule lessI) apply (subst(asm) cte_map_nat_to_cref) apply (drule valid_Zombie_n_less_cte_bits) apply simp apply (clarsimp simp: valid_cap_def cap_aligned_def word_bits_def
                     split: option.split_asm) apply (simp add: mult.commute cte_level_bits_def) apply (clarsimp simp: isCap_simps valid_cap_def) apply (simp only: assert_def, subst if_P) apply (cases bits, simp_all add: zbits_map_def) apply (clarsimp simp: cap_table_at_gsCNodes isCap_simps
                           zbits_map_def) apply (rule word_of_nat_less) apply (simp add: cap_aligned_def) apply (erule corres_guard_imp, simp_all) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); spec_corres s r P P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n)))\<rbrakk> \<Longrightarrow> spec_corres s r P P' f (locateSlotCap (capability.Zombie ptr (zbits_map bits) (Suc n)) (word_of_nat n) >>= f') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n)))\<rbrakk> \<Longrightarrow> corres r (P and (=) s) P' f (locateSlotCap (capability.Zombie ptr (zbits_map bits) (Suc n)) (word_of_nat n) >>= f') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n)))\<rbrakk> \<Longrightarrow> corres r (P and (=) s) P' f (do x <- get;
x <- assert ((isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits \<noteq> ZombieTCB) \<and> (case gsCNodes x ptr of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<and> na = capCNodeBits (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> na = zombieCTEBits (zbits_map bits)) \<and> word_of_nat n < 2 ^ na) \<or> isThreadCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits = ZombieTCB);
f' (ptr + 0x10 * word_of_nat n)
od) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n)))\<rbrakk> \<Longrightarrow> corres r (P and (=) s) (\<lambda>s. s = x \<and> P' s) f (do x <- assert ((isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits \<noteq> ZombieTCB) \<and> (case gsCNodes x ptr of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<and> na = capCNodeBits (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> na = zombieCTEBits (zbits_map bits)) \<and> word_of_nat n < 2 ^ na) \<or> isThreadCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits = ZombieTCB);
f' (ptr + 0x10 * word_of_nat n)
od)
 2. \<And>sa. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P' sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); True\<rbrakk> \<Longrightarrow> no_fail P' get proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P s; P' x; (s, x) \<in> state_relation\<rbrakk> \<Longrightarrow> corres r (P and (=) s) (\<lambda>s. s = x \<and> P' s) f (do x <- assert ((isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits \<noteq> ZombieTCB) \<and> (case gsCNodes x ptr of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<and> na = capCNodeBits (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> na = zombieCTEBits (zbits_map bits)) \<and> word_of_nat n < 2 ^ na) \<or> isThreadCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits = ZombieTCB);
f' (ptr + 0x10 * word_of_nat n)
od)
 2. \<And>sa. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P' sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); True\<rbrakk> \<Longrightarrow> no_fail P' get proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s\<rbrakk> \<Longrightarrow> corres r (P and (=) s) (\<lambda>s. s = x \<and> P' s) f (do x <- assert ((isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits \<noteq> ZombieTCB) \<and> (case gsCNodes x ptr of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<and> na = capCNodeBits (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> na = zombieCTEBits (zbits_map bits)) \<and> word_of_nat n < 2 ^ na) \<or> isThreadCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits = ZombieTCB);
f' (ptr + 0x10 * word_of_nat n)
od)
 2. \<And>sa. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P' sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); True\<rbrakk> \<Longrightarrow> no_fail P' get proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s; s \<turnstile> cap.Zombie ptr bits (Suc n)\<rbrakk> \<Longrightarrow> n < 2 ^ zombie_cte_bits bits
 2. \<And>x. \<lbrakk>P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s; s \<turnstile> cap.Zombie ptr bits (Suc n)\<rbrakk> \<Longrightarrow> zombie_cte_bits bits < word_bits
 3. \<And>x. \<lbrakk>s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (ptr + word_of_nat n * 2 ^ cte_level_bits)); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s\<rbrakk> \<Longrightarrow> corres r (P and (=) s) (\<lambda>s. s = x \<and> P' s) f (do x <- assert ((isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits \<noteq> ZombieTCB) \<and> (case gsCNodes x ptr of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<and> na = capCNodeBits (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> na = zombieCTEBits (zbits_map bits)) \<and> word_of_nat n < 2 ^ na) \<or> isThreadCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits = ZombieTCB);
f' (ptr + 0x10 * word_of_nat n)
od)
 4. \<And>sa. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P' sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); True\<rbrakk> \<Longrightarrow> no_fail P' get proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s; Suc n \<le> 2 ^ zombie_cte_bits bits\<rbrakk> \<Longrightarrow> n < 2 ^ zombie_cte_bits bits
 2. \<And>x. \<lbrakk>P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s; s \<turnstile> cap.Zombie ptr bits (Suc n)\<rbrakk> \<Longrightarrow> zombie_cte_bits bits < word_bits
 3. \<And>x. \<lbrakk>s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (ptr + word_of_nat n * 2 ^ cte_level_bits)); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s\<rbrakk> \<Longrightarrow> corres r (P and (=) s) (\<lambda>s. s = x \<and> P' s) f (do x <- assert ((isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits \<noteq> ZombieTCB) \<and> (case gsCNodes x ptr of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<and> na = capCNodeBits (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> na = zombieCTEBits (zbits_map bits)) \<and> word_of_nat n < 2 ^ na) \<or> isThreadCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits = ZombieTCB);
f' (ptr + 0x10 * word_of_nat n)
od)
 4. \<And>sa. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P' sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); True\<rbrakk> \<Longrightarrow> no_fail P' get proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s; s \<turnstile> cap.Zombie ptr bits (Suc n)\<rbrakk> \<Longrightarrow> zombie_cte_bits bits < word_bits
 2. \<And>x. \<lbrakk>s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (ptr + word_of_nat n * 2 ^ cte_level_bits)); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s\<rbrakk> \<Longrightarrow> corres r (P and (=) s) (\<lambda>s. s = x \<and> P' s) f (do x <- assert ((isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits \<noteq> ZombieTCB) \<and> (case gsCNodes x ptr of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<and> na = capCNodeBits (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> na = zombieCTEBits (zbits_map bits)) \<and> word_of_nat n < 2 ^ na) \<or> isThreadCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits = ZombieTCB);
f' (ptr + 0x10 * word_of_nat n)
od)
 3. \<And>sa. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P' sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); True\<rbrakk> \<Longrightarrow> no_fail P' get proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (ptr + word_of_nat n * 2 ^ cte_level_bits)); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s\<rbrakk> \<Longrightarrow> corres r (P and (=) s) (\<lambda>s. s = x \<and> P' s) f (do x <- assert ((isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits \<noteq> ZombieTCB) \<and> (case gsCNodes x ptr of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<and> na = capCNodeBits (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> na = zombieCTEBits (zbits_map bits)) \<and> word_of_nat n < 2 ^ na) \<or> isThreadCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits = ZombieTCB);
f' (ptr + 0x10 * word_of_nat n)
od)
 2. \<And>sa. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P' sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); True\<rbrakk> \<Longrightarrow> no_fail P' get proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (ptr + word_of_nat n * 0x10)); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s\<rbrakk> \<Longrightarrow> corres r (P and (=) s) (\<lambda>s. s = x \<and> P' s) f (do x <- assert ((isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits \<noteq> ZombieTCB) \<and> (case gsCNodes x ptr of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<and> na = capCNodeBits (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> na = zombieCTEBits (zbits_map bits)) \<and> word_of_nat n < 2 ^ na) \<or> isThreadCap (capability.Zombie ptr (zbits_map bits) (Suc n)) \<or> zbits_map bits = ZombieTCB);
f' (ptr + word_of_nat n * 0x10)
od)
 2. \<And>sa. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P' sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); True\<rbrakk> \<Longrightarrow> no_fail P' get proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>corres r (P and (=) s) P' f (f' (ptr + word_of_nat n * 0x10)); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s; cap_aligned (cap.Zombie ptr bits (Suc n)); case bits of None \<Rightarrow> tcb_at ptr s \<and> n \<le> 4 | Some b \<Rightarrow> cap_table_at b ptr s \<and> Suc n \<le> 2 ^ b \<and> 0 < b\<rbrakk> \<Longrightarrow> corres r (P and (=) s) (\<lambda>s. s = x \<and> P' s) f (do x <- assert (zbits_map bits \<noteq> ZombieTCB \<and> (case gsCNodes x ptr of None \<Rightarrow> False | Some na \<Rightarrow> na = zombieCTEBits (zbits_map bits) \<and> word_of_nat n < 2 ^ na) \<or> zbits_map bits = ZombieTCB);
f' (ptr + word_of_nat n * 0x10)
od)
 2. \<And>sa. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P' sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); True\<rbrakk> \<Longrightarrow> no_fail P' get proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>corres r (P and (=) s) P' f (f' (ptr + word_of_nat n * 0x10)); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s; cap_aligned (cap.Zombie ptr bits (Suc n)); case bits of None \<Rightarrow> tcb_at ptr s \<and> n \<le> 4 | Some b \<Rightarrow> cap_table_at b ptr s \<and> Suc n \<le> 2 ^ b \<and> 0 < b\<rbrakk> \<Longrightarrow> zbits_map bits \<noteq> ZombieTCB \<and> (case gsCNodes x ptr of None \<Rightarrow> False | Some na \<Rightarrow> na = zombieCTEBits (zbits_map bits) \<and> word_of_nat n < 2 ^ na) \<or> zbits_map bits = ZombieTCB
 2. \<And>x. \<lbrakk>corres r (P and (=) s) P' f (f' (ptr + word_of_nat n * 0x10)); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s; cap_aligned (cap.Zombie ptr bits (Suc n)); case bits of None \<Rightarrow> tcb_at ptr s \<and> n \<le> 4 | Some b \<Rightarrow> cap_table_at b ptr s \<and> Suc n \<le> 2 ^ b \<and> 0 < b\<rbrakk> \<Longrightarrow> corres r (P and (=) s) (\<lambda>s. s = x \<and> P' s) f (do x <- return ();
f' (ptr + word_of_nat n * 0x10)
od)
 3. \<And>sa. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P' sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); True\<rbrakk> \<Longrightarrow> no_fail P' get proof (prove)
goal (4 subgoals):
 1. \<And>x a. \<lbrakk>corres r (P and (=) s) P' f (f' (ptr + word_of_nat n * 0x10)); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref a n) s; cap_aligned (cap.Zombie ptr (Some a) (Suc n)); cap_table_at a ptr s \<and> Suc n \<le> 2 ^ a \<and> 0 < a; bits = Some a\<rbrakk> \<Longrightarrow> case gsCNodes x ptr of None \<Rightarrow> False | Some na \<Rightarrow> na = a \<and> word_of_nat n < 2 ^ na
 2. \<And>x. \<lbrakk>corres r (P and (=) s) P' f (f' (ptr + word_of_nat n * 0x10)); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s; cap_aligned (cap.Zombie ptr bits (Suc n)); case bits of None \<Rightarrow> tcb_at ptr s \<and> n \<le> 4 | Some b \<Rightarrow> cap_table_at b ptr s \<and> Suc n \<le> 2 ^ b \<and> 0 < b\<rbrakk> \<Longrightarrow> corres r (P and (=) s) (\<lambda>s. s = x \<and> P' s) f (f' (ptr + word_of_nat n * 0x10))
 3. \<And>sa. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P' sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n)))\<rbrakk> \<Longrightarrow> no_fail P' get proof (prove)
goal (4 subgoals):
 1. \<And>x a. \<lbrakk>corres r (P and (=) s) P' f (f' (ptr + word_of_nat n * 0x10)); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref a n) s; cap_aligned (cap.Zombie ptr (Some a) (Suc n)); bits = Some a; cap_table_at a ptr s; Suc n \<le> 2 ^ a; 0 < a\<rbrakk> \<Longrightarrow> word_of_nat n < 2 ^ a
 2. \<And>x. \<lbrakk>corres r (P and (=) s) P' f (f' (ptr + word_of_nat n * 0x10)); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s; cap_aligned (cap.Zombie ptr bits (Suc n)); case bits of None \<Rightarrow> tcb_at ptr s \<and> n \<le> 4 | Some b \<Rightarrow> cap_table_at b ptr s \<and> Suc n \<le> 2 ^ b \<and> 0 < b\<rbrakk> \<Longrightarrow> corres r (P and (=) s) (\<lambda>s. s = x \<and> P' s) f (f' (ptr + word_of_nat n * 0x10))
 3. \<And>sa. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P' sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n)))\<rbrakk> \<Longrightarrow> no_fail P' get proof (prove)
goal (4 subgoals):
 1. \<And>x a. \<lbrakk>corres r (P and (=) s) P' f (f' (ptr + word_of_nat n * 0x10)); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref a n) s; cap_aligned (cap.Zombie ptr (Some a) (Suc n)); bits = Some a; cap_table_at a ptr s; Suc n \<le> 2 ^ a; 0 < a\<rbrakk> \<Longrightarrow> n < unat (2 ^ a)
 2. \<And>x. \<lbrakk>corres r (P and (=) s) P' f (f' (ptr + word_of_nat n * 0x10)); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s; cap_aligned (cap.Zombie ptr bits (Suc n)); case bits of None \<Rightarrow> tcb_at ptr s \<and> n \<le> 4 | Some b \<Rightarrow> cap_table_at b ptr s \<and> Suc n \<le> 2 ^ b \<and> 0 < b\<rbrakk> \<Longrightarrow> corres r (P and (=) s) (\<lambda>s. s = x \<and> P' s) f (f' (ptr + word_of_nat n * 0x10))
 3. \<And>sa. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P' sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n)))\<rbrakk> \<Longrightarrow> no_fail P' get proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>corres r (P and (=) s) P' f (f' (ptr + word_of_nat n * 0x10)); P s; P' x; (s, x) \<in> state_relation; cte_wp_at (\<lambda>_. True) (ptr, nat_to_cref (zombie_cte_bits bits) n) s; cap_aligned (cap.Zombie ptr bits (Suc n)); case bits of None \<Rightarrow> tcb_at ptr s \<and> n \<le> 4 | Some b \<Rightarrow> cap_table_at b ptr s \<and> Suc n \<le> 2 ^ b \<and> 0 < b\<rbrakk> \<Longrightarrow> corres r (P and (=) s) (\<lambda>s. s = x \<and> P' s) f (f' (ptr + word_of_nat n * 0x10))
 2. \<And>sa. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P' sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n)))\<rbrakk> \<Longrightarrow> no_fail P' get proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n))); P' sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get \<lbrace>\<lambda>r. (=) sa\<rbrace>
 2. \<lbrakk>P s \<Longrightarrow> s \<turnstile> cap.Zombie ptr bits (Suc n); corres r (P and (=) s) P' f (f' (cte_map (ptr, nat_to_cref (zombie_cte_bits bits) n)))\<rbrakk> \<Longrightarrow> no_fail P' get proof (prove)
goal:
No subgoals!