theory Delete_C

lemma zombie_rf_sr_helperE:
  "\<lbrakk> cte_wp_at' P p s; (s, s') \<in> rf_sr; invs' s;
      \<And>cte. P cte \<Longrightarrow> isZombie (cteCap cte);
      \<And>cap ccap cte. \<lbrakk> cap = cteCap cte; ccap = h_val
                        (hrs_mem (t_hrs_' (globals s')))
                        (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C'']));
                    P cte; ccap_relation cap ccap; capAligned cap;
                    cap_get_tag ccap = scast cap_zombie_cap;
                    get_capZombiePtr_CL (cap_zombie_cap_lift ccap)
                            = capZombiePtr cap;
                    capZombieType_CL (cap_zombie_cap_lift ccap)
                            = (case_zombie_type ZombieTCB_C of_nat (capZombieType cap)) \<rbrakk>
               \<Longrightarrow> Q \<rbrakk>
     \<Longrightarrow> Q" apply (clarsimp simp: cte_wp_at_ctes_of) apply (frule ctes_of_valid', clarsimp) apply (erule(1) cmap_relationE1 [OF cmap_relation_cte]) apply atomize apply (simp add: typ_heap_simps) apply (drule spec, drule(1) mp)+ apply (clarsimp simp: cap_get_tag_isCap
                 dest!: ccte_relation_ccap_relation
                        valid_capAligned) apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap[THEN iffD2]) apply (clarsimp simp: get_capZombiePtr_CL_def Let_def
                        get_capZombieBits_CL_def
                        isZombieTCB_C_def
                 split: if_split_asm) apply (simp add: less_mask_eq ccap_zombie_radix_less2
                   isZombieTCB_C_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' P p s; (s, s') \<in> rf_sr; invs' s; \<And>cte. P cte \<Longrightarrow> isZombie (cteCap cte); \<And>cap ccap cte. \<lbrakk>cap = cteCap cte; ccap = h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C''])); P cte; ccap_relation cap ccap; capAligned cap; cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; get_capZombiePtr_CL (cap_zombie_cap_lift ccap) = capZombiePtr cap; capZombieType_CL (cap_zombie_cap_lift ccap) = (case capZombieType cap of ZombieTCB \<Rightarrow> ZombieTCB_C | ZombieCNode x \<Rightarrow> word_of_nat x)\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>(s, s') \<in> rf_sr; invs' s; \<And>cte. P cte \<Longrightarrow> isZombie (cteCap cte); \<And>cap ccap cte. \<lbrakk>cap = cteCap cte; ccap = h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C''])); P cte; ccap_relation (cteCap cte) (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C'']))); capAligned (cteCap cte); cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; get_capZombiePtr_CL (cap_zombie_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C''])))) = capZombiePtr (cteCap cte); capZombieType_CL (cap_zombie_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C''])))) = (case capZombieType (cteCap cte) of ZombieTCB \<Rightarrow> ZombieTCB_C | ZombieCNode x \<Rightarrow> word_of_nat x)\<rbrakk> \<Longrightarrow> Q; ctes_of s p = Some cte; P cte\<rbrakk> \<Longrightarrow> Q proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>(s, s') \<in> rf_sr; invs' s; \<And>cte. P cte \<Longrightarrow> isZombie (cteCap cte); \<And>cap ccap cte. \<lbrakk>cap = cteCap cte; ccap = h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C''])); P cte; ccap_relation (cteCap cte) (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C'']))); capAligned (cteCap cte); cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; get_capZombiePtr_CL (cap_zombie_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C''])))) = capZombiePtr (cteCap cte); capZombieType_CL (cap_zombie_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C''])))) = (case capZombieType (cteCap cte) of ZombieTCB \<Rightarrow> ZombieTCB_C | ZombieCNode x \<Rightarrow> word_of_nat x)\<rbrakk> \<Longrightarrow> Q; ctes_of s p = Some cte; P cte; valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> Q proof (prove)
goal (1 subgoal):
 1. \<And>cte y'. \<lbrakk>invs' s; \<And>cte. P cte \<Longrightarrow> isZombie (cteCap cte); \<And>cap ccap cte. \<lbrakk>cap = cteCap cte; ccap = h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C''])); P cte; ccap_relation (cteCap cte) (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C'']))); capAligned (cteCap cte); cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; get_capZombiePtr_CL (cap_zombie_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C''])))) = capZombiePtr (cteCap cte); capZombieType_CL (cap_zombie_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C''])))) = (case capZombieType (cteCap cte) of ZombieTCB \<Rightarrow> ZombieTCB_C | ZombieCNode x \<Rightarrow> word_of_nat x)\<rbrakk> \<Longrightarrow> Q; ctes_of s p = Some cte; P cte; valid_cap' (cteCap cte) s; ctes_of s p = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr p) = Some y'\<rbrakk> \<Longrightarrow> Q proof (prove)
goal (1 subgoal):
 1. \<And>cte y'. \<lbrakk>invs' s; \<forall>cte. P cte \<longrightarrow> isZombie (cteCap cte); \<forall>cap ccap cte. cap = cteCap cte \<longrightarrow> ccap = h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C''])) \<longrightarrow> P cte \<longrightarrow> ccap_relation (cteCap cte) (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C'']))) \<longrightarrow> capAligned (cteCap cte) \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombiePtr_CL (cap_zombie_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C''])))) = capZombiePtr (cteCap cte) \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C''])))) = (case capZombieType (cteCap cte) of ZombieTCB \<Rightarrow> ZombieTCB_C | ZombieCNode x \<Rightarrow> word_of_nat x) \<longrightarrow> Q; ctes_of s p = Some cte; P cte; valid_cap' (cteCap cte) s; ctes_of s p = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr p) = Some y'\<rbrakk> \<Longrightarrow> Q proof (prove)
goal (1 subgoal):
 1. \<And>cte y'. \<lbrakk>invs' s; \<forall>cte. P cte \<longrightarrow> isZombie (cteCap cte); \<forall>cte. P cte \<longrightarrow> ccap_relation (cteCap cte) (cte_C.cap_C y') \<longrightarrow> capAligned (cteCap cte) \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombiePtr_CL (cap_zombie_cap_lift (cte_C.cap_C y')) = capZombiePtr (cteCap cte) \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y')) = (case capZombieType (cteCap cte) of ZombieTCB \<Rightarrow> ZombieTCB_C | ZombieCNode x \<Rightarrow> word_of_nat x) \<longrightarrow> Q; P cte; valid_cap' (cteCap cte) s; ctes_of s p = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr p) = Some y'\<rbrakk> \<Longrightarrow> Q proof (prove)
goal (1 subgoal):
 1. \<And>cte y'. \<lbrakk>invs' s; P cte; valid_cap' (cteCap cte) s; ctes_of s p = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr p) = Some y'; isZombie (cteCap cte); ccap_relation (cteCap cte) (cte_C.cap_C y') \<longrightarrow> capAligned (cteCap cte) \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombiePtr_CL (cap_zombie_cap_lift (cte_C.cap_C y')) = capZombiePtr (cteCap cte) \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y')) = (case capZombieType (cteCap cte) of ZombieTCB \<Rightarrow> ZombieTCB_C | ZombieCNode x \<Rightarrow> word_of_nat x) \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q proof (prove)
goal (1 subgoal):
 1. \<And>cte y'. \<lbrakk>invs' s; P cte; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some y'; isZombie (cteCap cte); capAligned (cteCap cte); ccap_relation (cteCap cte) (cte_C.cap_C y'); get_capZombiePtr_CL (cap_zombie_cap_lift (cte_C.cap_C y')) = capZombiePtr (cteCap cte) \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y')) = (case capZombieType (cteCap cte) of ZombieTCB \<Rightarrow> ZombieTCB_C | ZombieCNode x \<Rightarrow> word_of_nat x) \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q proof (prove)
goal (1 subgoal):
 1. \<And>cte y'. \<lbrakk>invs' s; P cte; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some y'; isZombie (cteCap cte); capAligned (cteCap cte); ccap_relation (cteCap cte) (cte_C.cap_C y'); get_capZombiePtr_CL (cap_zombie_cap_lift (cte_C.cap_C y')) = capZombiePtr (cteCap cte) \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y')) = (case capZombieType (cteCap cte) of ZombieTCB \<Rightarrow> ZombieTCB_C | ZombieCNode x \<Rightarrow> word_of_nat x) \<longrightarrow> Q; cteCap cte = (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y'))) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift (cte_C.cap_C y')) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift (cte_C.cap_C y')) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y'))) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift (cte_C.cap_C y')) && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift (cte_C.cap_C y')) && mask (radix + 1))))\<rbrakk> \<Longrightarrow> Q proof (prove)
goal (1 subgoal):
 1. \<And>cte y'. \<lbrakk>capAligned (capability.Zombie (capZombieID_CL (cap_zombie_cap_lift (cte_C.cap_C y')) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y')))))) (ZombieCNode (unat (capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y'))))) (unat (capZombieID_CL (cap_zombie_cap_lift (cte_C.cap_C y')) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y')))))))); ccap_relation (capability.Zombie (capZombieID_CL (cap_zombie_cap_lift (cte_C.cap_C y')) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y')))))) (ZombieCNode (unat (capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y'))))) (unat (capZombieID_CL (cap_zombie_cap_lift (cte_C.cap_C y')) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y')))))))) (cte_C.cap_C y'); cteCap cte = capability.Zombie (capZombieID_CL (cap_zombie_cap_lift (cte_C.cap_C y')) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y')))))) (ZombieCNode (unat (capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y'))))) (unat (capZombieID_CL (cap_zombie_cap_lift (cte_C.cap_C y')) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y'))))))); invs' s; P cte; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some y'; capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y')) \<noteq> ZombieTCB_C; capZombieID_CL (cap_zombie_cap_lift (cte_C.cap_C y')) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y')) && mask 5))) \<noteq> capZombieID_CL (cap_zombie_cap_lift (cte_C.cap_C y')) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift (cte_C.cap_C y')))))\<rbrakk> \<Longrightarrow> Q proof (prove)
goal:
No subgoals!