theory Delete_C

lemma capRemovable_spec:
  "\<forall>cap s.  \<Gamma>\<turnstile> \<lbrace>s. ccap_relation cap \<acute>cap \<and> (isZombie cap \<or> cap = NullCap) \<and> capAligned cap\<rbrace>
     Call capRemovable_'proc
      {s'. ret__unsigned_long_' s' = from_bool (capRemovable cap (ptr_val (slot_' s)))}" supply if_cong[cong] apply vcg apply (clarsimp simp: cap_get_tag_isCap(1-8)[THEN trans[OF eq_commute]]) apply (simp add: capRemovable_def) apply (clarsimp simp: ccap_zombie_radix_less4) apply (subst eq_commute, subst from_bool_eq_if) apply (rule exI, rule conjI, assumption) apply clarsimp apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap[THEN iffD2]) apply (case_tac slot) apply (clarsimp simp: get_capZombiePtr_CL_def Let_def get_capZombieBits_CL_def
                        isCap_simps unat_eq_1 unat_eq_0
                        less_mask_eq ccap_zombie_radix_less2
             split: if_split_asm) 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 \<or> cap = capability.NullCap) \<and> capAligned cap\<rbrace> Call capRemovable_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (capRemovable 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 \<or> cap = capability.NullCap) \<and> capAligned cap\<rbrace> Call capRemovable_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (capRemovable 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 \<or> cap = capability.NullCap; capAligned cap\<rbrakk> \<Longrightarrow> \<forall>ret__unsigned. ret__unsigned = cap_get_tag capa \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) cap_null_cap = cap_get_tag capa \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (capRemovable cap (ptr_val slot))) \<and> (SCAST(32 signed \<rightarrow> 32) cap_null_cap \<noteq> cap_get_tag capa \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) cap_zombie_cap = cap_get_tag capa \<longrightarrow> (\<exists>capb. ccap_relation capb capa \<and> isZombie capb \<and> capAligned capb \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = word_of_nat (capZombieNumber capb) \<longrightarrow> 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 word_of_nat (capZombieNumber capb) = SCAST(32 signed \<rightarrow> 32) 0 \<or> word_of_nat (capZombieNumber capb) = SCAST(32 signed \<rightarrow> 32) 1 \<and> slot = cte_Ptr (get_capZombiePtr_CL (cap_zombie_cap_lift capa)) then 1 else 0) = from_bool (capRemovable cap (ptr_val slot)))))) \<and> SCAST(32 signed \<rightarrow> 32) cap_zombie_cap = cap_get_tag capa) proof (prove)
goal (1 subgoal):
 1. \<And>cap slot capa. \<lbrakk>ccap_relation cap capa; isZombie cap \<or> cap = capability.NullCap; capAligned cap\<rbrakk> \<Longrightarrow> (cap = capability.NullCap \<longrightarrow> capRemovable capability.NullCap (ptr_val slot)) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (isZombie cap \<longrightarrow> (\<exists>capb. ccap_relation capb capa \<and> isZombie capb \<and> capAligned capb \<and> get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1F \<and> (if word_of_nat (capZombieNumber capb) = 0 \<or> word_of_nat (capZombieNumber capb) = 1 \<and> slot = cte_Ptr (get_capZombiePtr_CL (cap_zombie_cap_lift capa)) then 1 else 0) = from_bool (capRemovable cap (ptr_val slot)))) \<and> isZombie cap) proof (prove)
goal (1 subgoal):
 1. \<And>cap slot capa. \<lbrakk>ccap_relation cap capa; isZombie cap \<or> cap = capability.NullCap; capAligned cap\<rbrakk> \<Longrightarrow> cap \<noteq> capability.NullCap \<longrightarrow> (isZombie cap \<longrightarrow> (\<exists>capb. ccap_relation capb capa \<and> isZombie capb \<and> capAligned capb \<and> get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1F \<and> (if word_of_nat (capZombieNumber capb) = 0 \<or> word_of_nat (capZombieNumber capb) = 1 \<and> slot = cte_Ptr (get_capZombiePtr_CL (cap_zombie_cap_lift capa)) then 1 else 0) = from_bool (case cap of capability.NullCap \<Rightarrow> True | capability.Zombie slot' x n \<Rightarrow> n = 0 \<or> n = 1 \<and> ptr_val slot = slot' | _ \<Rightarrow> error []))) \<and> isZombie cap proof (prove)
goal (1 subgoal):
 1. \<And>cap slot capa. \<lbrakk>ccap_relation cap capa; capAligned cap; cap \<noteq> capability.NullCap; isZombie cap\<rbrakk> \<Longrightarrow> \<exists>capb. ccap_relation capb capa \<and> isZombie capb \<and> capAligned capb \<and> (if word_of_nat (capZombieNumber capb) = 0 \<or> word_of_nat (capZombieNumber capb) = 1 \<and> slot = cte_Ptr (get_capZombiePtr_CL (cap_zombie_cap_lift capa)) then 1 else 0) = from_bool (case cap of capability.NullCap \<Rightarrow> True | capability.Zombie slot' x n \<Rightarrow> n = 0 \<or> n = 1 \<and> ptr_val slot = slot' | _ \<Rightarrow> error []) proof (prove)
goal (1 subgoal):
 1. \<And>cap slot capa. \<lbrakk>ccap_relation cap capa; capAligned cap; cap \<noteq> capability.NullCap; isZombie cap\<rbrakk> \<Longrightarrow> \<exists>capb. ccap_relation capb capa \<and> isZombie capb \<and> capAligned capb \<and> (word_of_nat (capZombieNumber capb) = 0 \<or> word_of_nat (capZombieNumber capb) = 1 \<and> slot = cte_Ptr (get_capZombiePtr_CL (cap_zombie_cap_lift capa))) = (case cap of capability.NullCap \<Rightarrow> True | capability.Zombie slot' x n \<Rightarrow> n = 0 \<or> n = 1 \<and> ptr_val slot = slot' | _ \<Rightarrow> error []) proof (prove)
goal (1 subgoal):
 1. \<And>cap slot capa. \<lbrakk>ccap_relation cap capa; capAligned cap; cap \<noteq> capability.NullCap; isZombie cap\<rbrakk> \<Longrightarrow> isZombie cap \<and> capAligned cap \<and> (word_of_nat (capZombieNumber cap) = 0 \<or> word_of_nat (capZombieNumber cap) = 1 \<and> slot = cte_Ptr (get_capZombiePtr_CL (cap_zombie_cap_lift capa))) = (case cap of capability.NullCap \<Rightarrow> True | capability.Zombie slot' x n \<Rightarrow> n = 0 \<or> n = 1 \<and> ptr_val slot = slot' | _ \<Rightarrow> error []) proof (prove)
goal (1 subgoal):
 1. \<And>cap slot capa. \<lbrakk>ccap_relation cap capa; capAligned cap; cap \<noteq> capability.NullCap; isZombie cap\<rbrakk> \<Longrightarrow> (word_of_nat (capZombieNumber cap) = 0 \<or> word_of_nat (capZombieNumber cap) = 1 \<and> slot = cte_Ptr (get_capZombiePtr_CL (cap_zombie_cap_lift capa))) = (case cap of capability.NullCap \<Rightarrow> True | capability.Zombie slot' x n \<Rightarrow> n = 0 \<or> n = 1 \<and> ptr_val slot = slot' | _ \<Rightarrow> error []) proof (prove)
goal (1 subgoal):
 1. \<And>cap slot capa. \<lbrakk>ccap_relation cap capa; capAligned cap; cap \<noteq> capability.NullCap; isZombie cap; 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> (word_of_nat (capZombieNumber cap) = 0 \<or> word_of_nat (capZombieNumber cap) = 1 \<and> slot = cte_Ptr (get_capZombiePtr_CL (cap_zombie_cap_lift capa))) = (case cap of capability.NullCap \<Rightarrow> True | capability.Zombie slot' x n \<Rightarrow> n = 0 \<or> n = 1 \<and> ptr_val slot = slot' | _ \<Rightarrow> error []) proof (prove)
goal (1 subgoal):
 1. \<And>cap slot capa x. \<lbrakk>ccap_relation cap capa; capAligned cap; cap \<noteq> capability.NullCap; isZombie cap; 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)))); slot = cte_Ptr x\<rbrakk> \<Longrightarrow> (word_of_nat (capZombieNumber cap) = 0 \<or> word_of_nat (capZombieNumber cap) = 1 \<and> slot = cte_Ptr (get_capZombiePtr_CL (cap_zombie_cap_lift capa))) = (case cap of capability.NullCap \<Rightarrow> True | capability.Zombie slot' x n \<Rightarrow> n = 0 \<or> n = 1 \<and> ptr_val slot = slot' | _ \<Rightarrow> error []) proof (prove)
goal:
No subgoals!