theory CSpace_C

lemma cap_zombie_cap_get_capZombiePtr_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_zombie_cap
                \<and> get_capZombieBits_CL (cap_zombie_cap_lift \<acute>cap) < 0x1F \<rbrace>
       \<acute>ret__unsigned_long :== PROC cap_zombie_cap_get_capZombiePtr(\<acute>cap)
       \<lbrace>\<acute>ret__unsigned_long = get_capZombiePtr_CL (cap_zombie_cap_lift \<^bsup>s\<^esup>cap)\<rbrace>" apply vcg apply (clarsimp simp: get_capZombiePtr_CL_def word_sle_def mask_def
                        isZombieTCB_C_def ZombieTCB_C_def Let_def) apply (intro conjI) apply (simp add: word_add_less_mono1[where k=1 and j="0x1F", simplified]) apply (subst unat_plus_if_size) apply (clarsimp split: if_split) apply (clarsimp simp: get_capZombieBits_CL_def Let_def word_size
                 split: if_split if_split_asm) apply (subgoal_tac "unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5)
                      < unat ((2::word32) ^ 5)") apply (clarsimp simp: shiftl_eq_mult) apply (rule unat_mono) apply (rule and_mask_less_size) apply (clarsimp simp: word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<and> get_capZombieBits_CL (cap_zombie_cap_lift \<acute>cap) < 0x1F\<rbrace> Call cap_zombie_cap_get_capZombiePtr_'proc \<lbrace>\<acute>ret__unsigned_long = get_capZombiePtr_CL (cap_zombie_cap_lift \<^bsup>s\<^esup>cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F\<rbrakk> \<Longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = get_capZombieBits_CL (cap_zombie_cap_lift cap) \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<and> (\<forall>ret__unsigned. ret__unsigned = capZombieID_CL (cap_zombie_cap_lift cap) \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift cap) + SCAST(32 signed \<rightarrow> 32) 1 < SCAST(32 signed \<rightarrow> 32) 0x20 \<and> UCAST(32 \<rightarrow> 32) (capZombieID_CL (cap_zombie_cap_lift cap)) && ~~ ((1 << unat (get_capZombieBits_CL (cap_zombie_cap_lift cap) + SCAST(32 signed \<rightarrow> 32) 1)) - 1) = get_capZombiePtr_CL (cap_zombie_cap_lift cap))) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F\<rbrakk> \<Longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift cap) + 1 < 0x20 \<and> capZombieID_CL (cap_zombie_cap_lift cap) && ~~ (2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift cap) + 1) - 1) = capZombieID_CL (cap_zombie_cap_lift cap) && ~~ ((2 << unat (get_capZombieBits_CL (cap_zombie_cap_lift cap))) - 1) proof (prove)
goal (2 subgoals):
 1. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F\<rbrakk> \<Longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift cap) + 1 < 0x20
 2. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F\<rbrakk> \<Longrightarrow> capZombieID_CL (cap_zombie_cap_lift cap) && ~~ (2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift cap) + 1) - 1) = capZombieID_CL (cap_zombie_cap_lift cap) && ~~ ((2 << unat (get_capZombieBits_CL (cap_zombie_cap_lift cap))) - 1) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F\<rbrakk> \<Longrightarrow> capZombieID_CL (cap_zombie_cap_lift cap) && ~~ (2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift cap) + 1) - 1) = capZombieID_CL (cap_zombie_cap_lift cap) && ~~ ((2 << unat (get_capZombieBits_CL (cap_zombie_cap_lift cap))) - 1) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F\<rbrakk> \<Longrightarrow> capZombieID_CL (cap_zombie_cap_lift cap) && ~~ (2 ^ (if unat (get_capZombieBits_CL (cap_zombie_cap_lift cap)) + unat 1 < 2 ^ size (get_capZombieBits_CL (cap_zombie_cap_lift cap)) then unat (get_capZombieBits_CL (cap_zombie_cap_lift cap)) + unat 1 else unat (get_capZombieBits_CL (cap_zombie_cap_lift cap)) + unat 1 - 2 ^ size (get_capZombieBits_CL (cap_zombie_cap_lift cap))) - 1) = capZombieID_CL (cap_zombie_cap_lift cap) && ~~ ((2 << unat (get_capZombieBits_CL (cap_zombie_cap_lift cap))) - 1) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F\<rbrakk> \<Longrightarrow> (Suc (unat (get_capZombieBits_CL (cap_zombie_cap_lift cap))) < 2 ^ size (get_capZombieBits_CL (cap_zombie_cap_lift cap)) \<longrightarrow> capZombieID_CL (cap_zombie_cap_lift cap) && ~~ (2 * 2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift cap)) - 1) = capZombieID_CL (cap_zombie_cap_lift cap) && ~~ ((2 << unat (get_capZombieBits_CL (cap_zombie_cap_lift cap))) - 1)) \<and> (\<not> Suc (unat (get_capZombieBits_CL (cap_zombie_cap_lift cap))) < 2 ^ size (get_capZombieBits_CL (cap_zombie_cap_lift cap)) \<longrightarrow> capZombieID_CL (cap_zombie_cap_lift cap) && ~~ (2 ^ (Suc (unat (get_capZombieBits_CL (cap_zombie_cap_lift cap))) - 2 ^ size (get_capZombieBits_CL (cap_zombie_cap_lift cap))) - 1) = capZombieID_CL (cap_zombie_cap_lift cap) && ~~ ((2 << unat (get_capZombieBits_CL (cap_zombie_cap_lift cap))) - 1)) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap)); capZombieType_CL (cap_zombie_cap_lift cap) && mask 5 < 0x1F\<rbrakk> \<Longrightarrow> (unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5) < 4294967295 \<longrightarrow> capZombieID_CL (cap_zombie_cap_lift cap) && ~~ (2 * 2 ^ unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5) - 1) = capZombieID_CL (cap_zombie_cap_lift cap) && ~~ ((2 << unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5)) - 1)) \<and> (\<not> unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5) < 4294967295 \<longrightarrow> capZombieID_CL (cap_zombie_cap_lift cap) && ~~ (2 ^ (unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5) - 4294967295) - 1) = capZombieID_CL (cap_zombie_cap_lift cap) && ~~ ((2 << unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5)) - 1)) proof (prove)
goal (2 subgoals):
 1. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap)); capZombieType_CL (cap_zombie_cap_lift cap) && mask 5 < 0x1F; unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5) < unat (2 ^ 5)\<rbrakk> \<Longrightarrow> (unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5) < 4294967295 \<longrightarrow> capZombieID_CL (cap_zombie_cap_lift cap) && ~~ (2 * 2 ^ unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5) - 1) = capZombieID_CL (cap_zombie_cap_lift cap) && ~~ ((2 << unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5)) - 1)) \<and> (\<not> unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5) < 4294967295 \<longrightarrow> capZombieID_CL (cap_zombie_cap_lift cap) && ~~ (2 ^ (unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5) - 4294967295) - 1) = capZombieID_CL (cap_zombie_cap_lift cap) && ~~ ((2 << unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5)) - 1))
 2. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap)); capZombieType_CL (cap_zombie_cap_lift cap) && mask 5 < 0x1F\<rbrakk> \<Longrightarrow> unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5) < unat (2 ^ 5) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap)); capZombieType_CL (cap_zombie_cap_lift cap) && mask 5 < 0x1F\<rbrakk> \<Longrightarrow> unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 5) < unat (2 ^ 5) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap)); capZombieType_CL (cap_zombie_cap_lift cap) && mask 5 < 0x1F\<rbrakk> \<Longrightarrow> capZombieType_CL (cap_zombie_cap_lift cap) && mask 5 < 2 ^ 5 proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap)); capZombieType_CL (cap_zombie_cap_lift cap) && mask 5 < 0x1F\<rbrakk> \<Longrightarrow> 5 < size (capZombieType_CL (cap_zombie_cap_lift cap)) proof (prove)
goal:
No subgoals!