theory ArchCNodeInv_AI

lemma cte_at_nat_to_cref_zbits [CNodeInv_AI_assms]:
  "\<lbrakk> s \<turnstile> Zombie oref zb n; m < n \<rbrakk>
     \<Longrightarrow> cte_at (oref, nat_to_cref (zombie_cte_bits zb) m) s" apply (subst(asm) valid_cap_def) apply (cases zb, simp_all add: valid_cap_def) apply (clarsimp simp: obj_at_def is_tcb) apply (drule(1) tcb_cap_cases_lt [OF order_less_le_trans]) apply clarsimp apply (rule cte_wp_at_tcbI, fastforce+) apply (clarsimp elim!: cap_table_at_cte_at simp: cap_aligned_def) apply (simp add: nat_to_cref_def word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> Zombie oref zb n; m < n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, nat_to_cref (zombie_cte_bits zb) m) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_aligned (Zombie oref zb n) \<and> (case Zombie oref zb n of UntypedCap dev p b f \<Rightarrow> valid_untyped (Zombie oref zb n) s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True); m < n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, nat_to_cref (zombie_cte_bits zb) m) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_aligned (Zombie oref None n) \<and> tcb_at oref s \<and> n \<le> 5; m < n; zb = None\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, nat_to_cref 3 m) s
 2. \<And>a. \<lbrakk>cap_aligned (Zombie oref (Some a) n) \<and> cap_table_at a oref s \<and> n \<le> 2 ^ a \<and> 0 < a; m < n; zb = Some a\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, nat_to_cref a m) s proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>m < n; zb = None; cap_aligned (Zombie oref None n); n \<le> 5; kheap s oref = Some (TCB tcb)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, nat_to_cref 3 m) s
 2. \<And>a. \<lbrakk>cap_aligned (Zombie oref (Some a) n) \<and> cap_table_at a oref s \<and> n \<le> 2 ^ a \<and> 0 < a; m < n; zb = Some a\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, nat_to_cref a m) s proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>zb = None; cap_aligned (Zombie oref None n); n \<le> 5; kheap s oref = Some (TCB tcb); tcb_cap_cases (nat_to_cref 3 m) \<noteq> None\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, nat_to_cref 3 m) s
 2. \<And>a. \<lbrakk>cap_aligned (Zombie oref (Some a) n) \<and> cap_table_at a oref s \<and> n \<le> 2 ^ a \<and> 0 < a; m < n; zb = Some a\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, nat_to_cref a m) s proof (prove)
goal (2 subgoals):
 1. \<And>tcb a aa b. \<lbrakk>zb = None; cap_aligned (Zombie oref None n); n \<le> 5; kheap s oref = Some (TCB tcb); tcb_cap_cases (nat_to_cref 3 m) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, nat_to_cref 3 m) s
 2. \<And>a. \<lbrakk>cap_aligned (Zombie oref (Some a) n) \<and> cap_table_at a oref s \<and> n \<le> 2 ^ a \<and> 0 < a; m < n; zb = Some a\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, nat_to_cref a m) s proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>cap_aligned (Zombie oref (Some a) n) \<and> cap_table_at a oref s \<and> n \<le> 2 ^ a \<and> 0 < a; m < n; zb = Some a\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, nat_to_cref a m) s proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>m < n; zb = Some a; is_aligned oref (cte_level_bits + a); cte_level_bits + a < word_bits; n \<le> 2 ^ a; 0 < a\<rbrakk> \<Longrightarrow> length (nat_to_cref a m) = a proof (prove)
goal:
No subgoals!