theory Delete_C

lemma capCyclicZombie_spec:
  "\<forall>cap s.  \<Gamma>\<turnstile> \<lbrace>s. ccap_relation cap \<acute>cap \<and> isZombie cap \<and> capAligned cap\<rbrace>
     Call capCyclicZombie_'proc
      {s'. ret__unsigned_long_' s' = from_bool (capCyclicZombie cap (ptr_val (slot_' s)))}" supply if_cong[cong] apply vcg apply (clarsimp simp: from_bool_0) apply (frule(1) cap_get_tag_isCap [THEN iffD2], simp) apply (subst eq_commute, subst from_bool_eq_if) apply (simp add: ccap_zombie_radix_less4) apply (case_tac slot, simp) apply (frule(1) cap_get_tag_to_H) apply (clarsimp simp: capCyclicZombie_def Let_def
                        get_capZombieBits_CL_def get_capZombiePtr_CL_def
                 split: if_split_asm) apply (auto simp: less_mask_eq ccap_zombie_radix_less2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>cap s. \<Gamma>\<turnstile> \<lbrace>s. ccap_relation cap \<acute>cap \<and> isZombie cap \<and> capAligned cap\<rbrace> Call capCyclicZombie_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (capCyclicZombie cap (ptr_val \<^bsup>s\<^esup>slot))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>cap s. \<Gamma>\<turnstile> \<lbrace>s. ccap_relation cap \<acute>cap \<and> isZombie cap \<and> capAligned cap\<rbrace> Call capCyclicZombie_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (capCyclicZombie cap (ptr_val \<^bsup>s\<^esup>slot))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap slot capa. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap\<rbrakk> \<Longrightarrow> \<forall>ret__unsigned. ret__unsigned = cap_get_tag capa \<longrightarrow> ((if cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap then 1 else 0) \<noteq> 0 \<longrightarrow> cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<and> get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1F \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = get_capZombiePtr_CL (cap_zombie_cap_lift capa) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) (if cte_Ptr (get_capZombiePtr_CL (cap_zombie_cap_lift capa)) = slot then 1 else 0) = from_bool (capCyclicZombie cap (ptr_val slot)))) \<and> ((if cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap then 1 else 0) = 0 \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = from_bool (capCyclicZombie cap (ptr_val slot))) proof (prove)
goal (1 subgoal):
 1. \<And>cap slot capa. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap\<rbrakk> \<Longrightarrow> (cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1F \<and> (if cte_Ptr (get_capZombiePtr_CL (cap_zombie_cap_lift capa)) = slot then 1 else 0) = from_bool (capCyclicZombie cap (ptr_val slot))) \<and> (cap_get_tag capa \<noteq> SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> \<not> capCyclicZombie cap (ptr_val slot)) proof (prove)
goal (1 subgoal):
 1. \<And>cap slot capa. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap; cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap\<rbrakk> \<Longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1F \<and> (if cte_Ptr (get_capZombiePtr_CL (cap_zombie_cap_lift capa)) = slot then 1 else 0) = from_bool (capCyclicZombie cap (ptr_val slot)) proof (prove)
goal (1 subgoal):
 1. \<And>cap slot capa. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap; cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap\<rbrakk> \<Longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1F \<and> (cte_Ptr (get_capZombiePtr_CL (cap_zombie_cap_lift capa)) = slot) = capCyclicZombie cap (ptr_val slot) proof (prove)
goal (1 subgoal):
 1. \<And>cap slot capa. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap; cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap\<rbrakk> \<Longrightarrow> (cte_Ptr (get_capZombiePtr_CL (cap_zombie_cap_lift capa)) = slot) = capCyclicZombie cap (ptr_val slot) proof (prove)
goal (1 subgoal):
 1. \<And>cap slot capa x. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap; cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; slot = cte_Ptr x\<rbrakk> \<Longrightarrow> (get_capZombiePtr_CL (cap_zombie_cap_lift capa) = x) = capCyclicZombie cap x proof (prove)
goal (1 subgoal):
 1. \<And>cap slot capa x. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap; cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; slot = cte_Ptr x; cap = (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (radix + 1))))\<rbrakk> \<Longrightarrow> (get_capZombiePtr_CL (cap_zombie_cap_lift capa) = x) = capCyclicZombie cap x proof (prove)
goal (2 subgoals):
 1. \<And>capa x. \<lbrakk>capAligned (capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5))); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)); ccap_relation (capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5))) capa\<rbrakk> \<Longrightarrow> (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5 = x) = (x = capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5)
 2. \<And>capa x. \<lbrakk>capAligned (capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))) (ZombieCNode (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))))); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)); ccap_relation (capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))) (ZombieCNode (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))))) capa\<rbrakk> \<Longrightarrow> (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa) && mask 5))) = x) = (x = capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))) proof (prove)
goal:
No subgoals!