theory CNodeInv_R

lemma shrink_zombie_invs':
  "\<lbrace>invs' and (K (isZombie cap))
    and cte_wp_at' (\<lambda>cte. cteCap cte = Zombie (capZombiePtr cap) (capZombieType cap) (capZombieNumber cap + 1)) sl
    and cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) (capZombiePtr cap + 2^cteSizeBits * (of_nat (capZombieNumber cap)))\<rbrace>
      updateCap sl cap
   \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (wp make_zombie_invs') apply (clarsimp simp: cte_wp_at_ctes_of isFinal_Zombie isCap_simps final_matters'_def) apply (rule context_conjI) apply (drule ctes_of_valid', clarsimp) apply (clarsimp simp: valid_cap'_def capAligned_def) apply clarsimp apply (rule ccontr, erule notE, rule imageI) apply (drule word_le_minus_one_leq) apply (rule ccontr, simp add: linorder_not_less mult.commute mult.left_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and K (isZombie cap) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.Zombie (capZombiePtr cap) (capZombieType cap) (capZombieNumber cap + 1)) sl and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (capZombiePtr cap + 2 ^ cteSizeBits * word_of_nat (capZombieNumber cap))\<rbrace> updateCap sl cap \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and K (isZombie cap) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.Zombie (capZombiePtr cap) (capZombieType cap) (capZombieNumber cap + 1)) sl and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (capZombiePtr cap + 2 ^ cteSizeBits * word_of_nat (capZombieNumber cap))) s \<Longrightarrow> invs' s \<and> valid_cap' cap s \<and> cte_wp_at' (\<lambda>cte. isFinal (cteCap cte) sl (cteCaps_of s)) sl s \<and> cte_wp_at' (\<lambda>cte. capClass (cteCap cte) = PhysicalClass \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap \<and> capBits (cteCap cte) = capBits cap \<and> (\<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) r s) \<and> (isZombie cap \<or> isThreadCap cap \<or> isCNodeCap cap) \<and> final_matters' (cteCap cte) \<and> (isThreadCap (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isZombie (cteCap cte)) \<and> \<not> isUntypedCap (cteCap cte) \<and> (\<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> bound_tcb_at' ((=) None) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> (\<forall>pr. p \<notin> set (ksReadyQueues s pr)))) sl s proof (prove)
goal (1 subgoal):
 1. \<And>s v0 v1 v2 cte ctea. \<lbrakk>invs' s; cap = capability.Zombie v0 v1 v2; ctes_of s sl = Some cte; cteCap cte = capability.Zombie v0 v1 (Suc v2); ctes_of s (v0 + 2 ^ cteSizeBits * word_of_nat v2) = Some ctea; cteCap ctea = capability.NullCap\<rbrakk> \<Longrightarrow> valid_cap' (capability.Zombie v0 v1 v2) s \<and> (\<forall>r\<in>(\<lambda>x. v0 + x * 2 ^ cteSizeBits) ` {0..<1 + word_of_nat v2} - (\<lambda>x. v0 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat v2}. \<exists>cte. ctes_of s r = Some cte \<and> cteCap cte = capability.NullCap) proof (prove)
goal (2 subgoals):
 1. \<And>s v0 v1 v2 cte ctea. \<lbrakk>invs' s; cap = capability.Zombie v0 v1 v2; ctes_of s sl = Some cte; cteCap cte = capability.Zombie v0 v1 (Suc v2); ctes_of s (v0 + 2 ^ cteSizeBits * word_of_nat v2) = Some ctea; cteCap ctea = capability.NullCap\<rbrakk> \<Longrightarrow> valid_cap' (capability.Zombie v0 v1 v2) s
 2. \<And>s v0 v1 v2 cte ctea. \<lbrakk>invs' s; cap = capability.Zombie v0 v1 v2; ctes_of s sl = Some cte; cteCap cte = capability.Zombie v0 v1 (Suc v2); ctes_of s (v0 + 2 ^ cteSizeBits * word_of_nat v2) = Some ctea; cteCap ctea = capability.NullCap; valid_cap' (capability.Zombie v0 v1 v2) s\<rbrakk> \<Longrightarrow> \<forall>r\<in>(\<lambda>x. v0 + x * 2 ^ cteSizeBits) ` {0..<1 + word_of_nat v2} - (\<lambda>x. v0 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat v2}. \<exists>cte. ctes_of s r = Some cte \<and> cteCap cte = capability.NullCap proof (prove)
goal (2 subgoals):
 1. \<And>s v0 v1 v2 cte ctea. \<lbrakk>invs' s; cap = capability.Zombie v0 v1 v2; cteCap cte = capability.Zombie v0 v1 (Suc v2); ctes_of s (v0 + 2 ^ cteSizeBits * word_of_nat v2) = Some ctea; cteCap ctea = capability.NullCap; valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> valid_cap' (capability.Zombie v0 v1 v2) s
 2. \<And>s v0 v1 v2 cte ctea. \<lbrakk>invs' s; cap = capability.Zombie v0 v1 v2; ctes_of s sl = Some cte; cteCap cte = capability.Zombie v0 v1 (Suc v2); ctes_of s (v0 + 2 ^ cteSizeBits * word_of_nat v2) = Some ctea; cteCap ctea = capability.NullCap; valid_cap' (capability.Zombie v0 v1 v2) s\<rbrakk> \<Longrightarrow> \<forall>r\<in>(\<lambda>x. v0 + x * 2 ^ cteSizeBits) ` {0..<1 + word_of_nat v2} - (\<lambda>x. v0 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat v2}. \<exists>cte. ctes_of s r = Some cte \<and> cteCap cte = capability.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s v0 v1 v2 cte ctea. \<lbrakk>invs' s; cap = capability.Zombie v0 v1 v2; ctes_of s sl = Some cte; cteCap cte = capability.Zombie v0 v1 (Suc v2); ctes_of s (v0 + 2 ^ cteSizeBits * word_of_nat v2) = Some ctea; cteCap ctea = capability.NullCap; valid_cap' (capability.Zombie v0 v1 v2) s\<rbrakk> \<Longrightarrow> \<forall>r\<in>(\<lambda>x. v0 + x * 2 ^ cteSizeBits) ` {0..<1 + word_of_nat v2} - (\<lambda>x. v0 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat v2}. \<exists>cte. ctes_of s r = Some cte \<and> cteCap cte = capability.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s v0 v1 v2 cte ctea x. \<lbrakk>invs' s; cap = capability.Zombie v0 v1 v2; ctes_of s sl = Some cte; cteCap cte = capability.Zombie v0 v1 (Suc v2); ctes_of s (v0 + 2 ^ cteSizeBits * word_of_nat v2) = Some ctea; cteCap ctea = capability.NullCap; valid_cap' (capability.Zombie v0 v1 v2) s; v0 + x * 2 ^ cteSizeBits \<notin> (\<lambda>x. v0 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat v2}; x < 1 + word_of_nat v2\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s (v0 + x * 2 ^ cteSizeBits) = Some cte \<and> cteCap cte = capability.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s v0 v1 v2 cte ctea x. \<lbrakk>invs' s; cap = capability.Zombie v0 v1 v2; ctes_of s sl = Some cte; cteCap cte = capability.Zombie v0 v1 (Suc v2); ctes_of s (v0 + 2 ^ cteSizeBits * word_of_nat v2) = Some ctea; cteCap ctea = capability.NullCap; valid_cap' (capability.Zombie v0 v1 v2) s; x < 1 + word_of_nat v2; \<nexists>cte. ctes_of s (v0 + x * 2 ^ cteSizeBits) = Some cte \<and> cteCap cte = capability.NullCap\<rbrakk> \<Longrightarrow> x \<in> {0..<word_of_nat v2} proof (prove)
goal (1 subgoal):
 1. \<And>s v0 v1 v2 cte ctea x. \<lbrakk>invs' s; cap = capability.Zombie v0 v1 v2; ctes_of s sl = Some cte; cteCap cte = capability.Zombie v0 v1 (Suc v2); ctes_of s (v0 + 2 ^ cteSizeBits * word_of_nat v2) = Some ctea; cteCap ctea = capability.NullCap; valid_cap' (capability.Zombie v0 v1 v2) s; \<nexists>cte. ctes_of s (v0 + x * 2 ^ cteSizeBits) = Some cte \<and> cteCap cte = capability.NullCap; x \<le> 1 + word_of_nat v2 - 1\<rbrakk> \<Longrightarrow> x \<in> {0..<word_of_nat v2} proof (prove)
goal:
No subgoals!