theory Invariants_H

lemma typ_at_lift_valid_cap':
  assumes P: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. valid_cap' cap s\<rbrace> f \<lbrace>\<lambda>rv s. valid_cap' cap s\<rbrace>" including no_pre apply (simp add: valid_cap'_def) apply wp apply (case_tac cap;
         simp add: valid_cap'_def P [where P=id, simplified] typ_at_lift_tcb'
                   hoare_vcg_prop typ_at_lift_ep'
                   typ_at_lift_ntfn' typ_at_lift_cte_at'
                   hoare_vcg_conj_lift [OF typ_at_lift_cte_at']) apply (rename_tac zombie_type nat) apply (case_tac zombie_type; simp) apply (wp typ_at_lift_tcb' P hoare_vcg_all_lift typ_at_lift_cte')+ apply (rename_tac arch_capability) apply (case_tac arch_capability,
           simp_all add: P [where P=id, simplified] page_table_at'_def
                         hoare_vcg_prop page_directory_at'_def All_less_Ball
              split del: if_split) apply (wp hoare_vcg_const_Ball_lift P typ_at_lift_valid_untyped'
                 hoare_vcg_all_lift typ_at_lift_cte')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' cap\<rbrace> f \<lbrace>\<lambda>rv. valid_cap' cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' cap\<rbrace> f \<lbrace>\<lambda>rv. valid_cap' cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. capAligned cap \<and> (case cap of capability.ThreadCap r \<Rightarrow> tcb_at' r s | capability.NotificationCap r badge x y \<Rightarrow> ntfn_at' r s | capability.IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | capability.EndpointCap r badge x y z t \<Rightarrow> ep_at' r s | capability.Zombie r b n \<Rightarrow> n \<le> zombieCTEs b \<and> zBits b < word_bits \<and> (case b of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)) | capability.ArchObjectCap (arch_capability.ASIDPoolCap pool asid) \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | capability.ArchObjectCap arch_capability.ASIDControlCap \<Rightarrow> True | capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz mapdata) \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<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 < pptrBase) | capability.ArchObjectCap (arch_capability.PageTableCap ref mapdata) \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | capability.ArchObjectCap (arch_capability.PageDirectoryCap ref mapdata) \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | capability.ReplyCap r m x \<Rightarrow> tcb_at' r s | capability.UntypedCap d r n f \<Rightarrow> valid_untyped' d r n f s \<and> r \<noteq> 0 \<and> minUntypedSizeBits \<le> n \<and> n \<le> maxUntypedSizeBits \<and> f \<le> 2 ^ n \<and> is_aligned (word_of_nat f) minUntypedSizeBits | capability.CNodeCap r bits guard guard_sz \<Rightarrow> bits \<noteq> 0 \<and> bits + guard_sz \<le> word_bits \<and> guard && mask guard_sz = guard \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask bits)) s) | _ \<Rightarrow> True)\<rbrace> f \<lbrace>\<lambda>rv s. capAligned cap \<and> (case cap of capability.ThreadCap r \<Rightarrow> tcb_at' r s | capability.NotificationCap r badge x y \<Rightarrow> ntfn_at' r s | capability.IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | capability.EndpointCap r badge x y z t \<Rightarrow> ep_at' r s | capability.Zombie r b n \<Rightarrow> n \<le> zombieCTEs b \<and> zBits b < word_bits \<and> (case b of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)) | capability.ArchObjectCap (arch_capability.ASIDPoolCap pool asid) \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | capability.ArchObjectCap arch_capability.ASIDControlCap \<Rightarrow> True | capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz mapdata) \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<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 < pptrBase) | capability.ArchObjectCap (arch_capability.PageTableCap ref mapdata) \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | capability.ArchObjectCap (arch_capability.PageDirectoryCap ref mapdata) \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | capability.ReplyCap r m x \<Rightarrow> tcb_at' r s | capability.UntypedCap d r n f \<Rightarrow> valid_untyped' d r n f s \<and> r \<noteq> 0 \<and> minUntypedSizeBits \<le> n \<and> n \<le> maxUntypedSizeBits \<and> f \<le> 2 ^ n \<and> is_aligned (word_of_nat f) minUntypedSizeBits | capability.CNodeCap r bits guard guard_sz \<Rightarrow> bits \<noteq> 0 \<and> bits + guard_sz \<le> word_bits \<and> guard && mask guard_sz = guard \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask bits)) s) | _ \<Rightarrow> True)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case cap of capability.ThreadCap r \<Rightarrow> tcb_at' r s | capability.NotificationCap r badge x y \<Rightarrow> ntfn_at' r s | capability.IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | capability.EndpointCap r badge x y z t \<Rightarrow> ep_at' r s | capability.Zombie r b n \<Rightarrow> n \<le> zombieCTEs b \<and> zBits b < word_bits \<and> (case b of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)) | capability.ArchObjectCap (arch_capability.ASIDPoolCap pool asid) \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | capability.ArchObjectCap arch_capability.ASIDControlCap \<Rightarrow> True | capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz mapdata) \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<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 < pptrBase) | capability.ArchObjectCap (arch_capability.PageTableCap ref mapdata) \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | capability.ArchObjectCap (arch_capability.PageDirectoryCap ref mapdata) \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | capability.ReplyCap r m x \<Rightarrow> tcb_at' r s | capability.UntypedCap d r n f \<Rightarrow> valid_untyped' d r n f s \<and> r \<noteq> 0 \<and> minUntypedSizeBits \<le> n \<and> n \<le> maxUntypedSizeBits \<and> f \<le> 2 ^ n \<and> is_aligned (word_of_nat f) minUntypedSizeBits | capability.CNodeCap r bits guard guard_sz \<Rightarrow> bits \<noteq> 0 \<and> bits + guard_sz \<le> word_bits \<and> guard && mask guard_sz = guard \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask bits)) s) | _ \<Rightarrow> True\<rbrace> f \<lbrace>\<lambda>rv s. case cap of capability.ThreadCap r \<Rightarrow> tcb_at' r s | capability.NotificationCap r badge x y \<Rightarrow> ntfn_at' r s | capability.IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | capability.EndpointCap r badge x y z t \<Rightarrow> ep_at' r s | capability.Zombie r b n \<Rightarrow> n \<le> zombieCTEs b \<and> zBits b < word_bits \<and> (case b of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)) | capability.ArchObjectCap (arch_capability.ASIDPoolCap pool asid) \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | capability.ArchObjectCap arch_capability.ASIDControlCap \<Rightarrow> True | capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz mapdata) \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<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 < pptrBase) | capability.ArchObjectCap (arch_capability.PageTableCap ref mapdata) \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | capability.ArchObjectCap (arch_capability.PageDirectoryCap ref mapdata) \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | capability.ReplyCap r m x \<Rightarrow> tcb_at' r s | capability.UntypedCap d r n f \<Rightarrow> valid_untyped' d r n f s \<and> r \<noteq> 0 \<and> minUntypedSizeBits \<le> n \<and> n \<le> maxUntypedSizeBits \<and> f \<le> 2 ^ n \<and> is_aligned (word_of_nat f) minUntypedSizeBits | capability.CNodeCap r bits guard guard_sz \<Rightarrow> bits \<noteq> 0 \<and> bits + guard_sz \<le> word_bits \<and> guard && mask guard_sz = guard \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask bits)) s) | _ \<Rightarrow> True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x71 x72 x73. cap = capability.Zombie x71 x72 x73 \<Longrightarrow> \<lbrace>\<lambda>s. x73 \<le> zombieCTEs x72 \<and> zBits x72 < word_bits \<and> (case x72 of ZombieTCB \<Rightarrow> tcb_at' x71 s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (x71 + 2 ^ cteSizeBits * (addr && mask n)) s))\<rbrace> f \<lbrace>\<lambda>rv s. x73 \<le> zombieCTEs x72 \<and> zBits x72 < word_bits \<and> (case x72 of ZombieTCB \<Rightarrow> tcb_at' x71 s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (x71 + 2 ^ cteSizeBits * (addr && mask n)) s))\<rbrace>
 2. \<And>x8. cap = capability.ArchObjectCap x8 \<Longrightarrow> \<lbrace>\<lambda>s. case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<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 < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)\<rbrace> f \<lbrace>\<lambda>rv s. case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<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 < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)\<rbrace>
 3. \<And>x101 x102 x103 x104. cap = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<lbrace>\<lambda>s. valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits\<rbrace> f \<lbrace>\<lambda>rv s. valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits\<rbrace>
 4. \<And>x111 x112 x113 x114. cap = capability.CNodeCap x111 x112 x113 x114 \<Longrightarrow> \<lbrace>\<lambda>s. 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s)\<rbrace> f \<lbrace>\<lambda>rv s. 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x71 zombie_type nat. cap = capability.Zombie x71 zombie_type nat \<Longrightarrow> \<lbrace>\<lambda>s. nat \<le> zombieCTEs zombie_type \<and> zBits zombie_type < word_bits \<and> (case zombie_type of ZombieTCB \<Rightarrow> tcb_at' x71 s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (x71 + 2 ^ cteSizeBits * (addr && mask n)) s))\<rbrace> f \<lbrace>\<lambda>rv s. nat \<le> zombieCTEs zombie_type \<and> zBits zombie_type < word_bits \<and> (case zombie_type of ZombieTCB \<Rightarrow> tcb_at' x71 s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (x71 + 2 ^ cteSizeBits * (addr && mask n)) s))\<rbrace>
 2. \<And>x8. cap = capability.ArchObjectCap x8 \<Longrightarrow> \<lbrace>\<lambda>s. case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<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 < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)\<rbrace> f \<lbrace>\<lambda>rv s. case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<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 < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)\<rbrace>
 3. \<And>x101 x102 x103 x104. cap = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<lbrace>\<lambda>s. valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits\<rbrace> f \<lbrace>\<lambda>rv s. valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits\<rbrace>
 4. \<And>x111 x112 x113 x114. cap = capability.CNodeCap x111 x112 x113 x114 \<Longrightarrow> \<lbrace>\<lambda>s. 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s)\<rbrace> f \<lbrace>\<lambda>rv s. 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x71 zombie_type nat. \<lbrakk>cap = capability.Zombie x71 ZombieTCB nat; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. nat \<le> 5 \<and> tcbBlockSizeBits < word_bits \<and> tcb_at' x71 s\<rbrace> f \<lbrace>\<lambda>rv s. nat \<le> 5 \<and> tcbBlockSizeBits < word_bits \<and> tcb_at' x71 s\<rbrace>
 2. \<And>x71 zombie_type nat x2. \<lbrakk>cap = capability.Zombie x71 (ZombieCNode x2) nat; zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. nat \<le> 2 ^ x2 \<and> objBits undefined + x2 < word_bits \<and> 0 < x2 \<and> (\<forall>addr. real_cte_at' (x71 + 2 ^ cteSizeBits * (addr && mask x2)) s)\<rbrace> f \<lbrace>\<lambda>rv s. nat \<le> 2 ^ x2 \<and> objBits undefined + x2 < word_bits \<and> 0 < x2 \<and> (\<forall>addr. real_cte_at' (x71 + 2 ^ cteSizeBits * (addr && mask x2)) s)\<rbrace>
 3. \<And>x8. cap = capability.ArchObjectCap x8 \<Longrightarrow> \<lbrace>\<lambda>s. case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<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 < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)\<rbrace> f \<lbrace>\<lambda>rv s. case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<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 < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)\<rbrace>
 4. \<And>x101 x102 x103 x104. cap = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<lbrace>\<lambda>s. valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits\<rbrace> f \<lbrace>\<lambda>rv s. valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits\<rbrace>
 5. \<And>x111 x112 x113 x114. cap = capability.CNodeCap x111 x112 x113 x114 \<Longrightarrow> \<lbrace>\<lambda>s. 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s)\<rbrace> f \<lbrace>\<lambda>rv s. 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x8. cap = capability.ArchObjectCap x8 \<Longrightarrow> \<lbrace>\<lambda>s. case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<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 < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)\<rbrace> f \<lbrace>\<lambda>rv s. case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<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 < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)\<rbrace>
 2. \<And>x101 x102 x103 x104. cap = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<lbrace>\<lambda>s. valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits\<rbrace> f \<lbrace>\<lambda>rv s. valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits\<rbrace>
 3. \<And>x111 x112 x113 x114. cap = capability.CNodeCap x111 x112 x113 x114 \<Longrightarrow> \<lbrace>\<lambda>s. 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s)\<rbrace> f \<lbrace>\<lambda>rv s. 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>arch_capability. cap = capability.ArchObjectCap arch_capability \<Longrightarrow> \<lbrace>\<lambda>s. case arch_capability of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<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 < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)\<rbrace> f \<lbrace>\<lambda>rv s. case arch_capability of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<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 < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)\<rbrace>
 2. \<And>x101 x102 x103 x104. cap = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<lbrace>\<lambda>s. valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits\<rbrace> f \<lbrace>\<lambda>rv s. valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits\<rbrace>
 3. \<And>x111 x112 x113 x114. cap = capability.CNodeCap x111 x112 x113 x114 \<Longrightarrow> \<lbrace>\<lambda>s. 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s)\<rbrace> f \<lbrace>\<lambda>rv s. 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>arch_capability x11 x12. \<lbrakk>cap = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12); arch_capability = arch_capability.ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. asid_pool_at' x11 s \<and> is_aligned x12 local.asid_low_bits \<and> x12 < 2 ^ local.asid_bits\<rbrace> f \<lbrace>\<lambda>rv s. asid_pool_at' x11 s \<and> is_aligned x12 local.asid_low_bits \<and> x12 < 2 ^ local.asid_bits\<rbrace>
 2. \<And>arch_capability x31 x32 x33 x34 x35. \<lbrakk>cap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35); arch_capability = arch_capability.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. x32 \<noteq> 0 \<and> (\<forall>p\<in>{..<2 ^ (pageBitsForSize x34 - pageBits)}. typ_at' (if x31 then UserDataDeviceT else UserDataT) (x32 + p * 2 ^ pageBits) s) \<and> (case x35 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned' ref x34 \<and> ref < pptrBase)\<rbrace> f \<lbrace>\<lambda>rv s. x32 \<noteq> 0 \<and> (\<forall>p\<in>{..<2 ^ (pageBitsForSize x34 - pageBits)}. typ_at' (if x31 then UserDataDeviceT else UserDataT) (x32 + p * 2 ^ pageBits) s) \<and> (case x35 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned' ref x34 \<and> ref < pptrBase)\<rbrace>
 3. \<And>arch_capability x41 x42. \<lbrakk>cap = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. is_aligned x41 ptBits \<and> (\<forall>y\<in>{..<0x100}. pte_at' (x41 + (y << 2)) s) \<and> (case x42 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase)\<rbrace> f \<lbrace>\<lambda>rv s. is_aligned x41 ptBits \<and> (\<forall>y\<in>{..<0x100}. pte_at' (x41 + (y << 2)) s) \<and> (case x42 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase)\<rbrace>
 4. \<And>arch_capability x51 x52. \<lbrakk>cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. is_aligned x51 pdBits \<and> (\<forall>y\<in>{..<0x1000}. pde_at' (x51 + (y << 2)) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)\<rbrace> f \<lbrace>\<lambda>rv s. is_aligned x51 pdBits \<and> (\<forall>y\<in>{..<0x1000}. pde_at' (x51 + (y << 2)) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)\<rbrace>
 5. \<And>x101 x102 x103 x104. cap = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<lbrace>\<lambda>s. valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits\<rbrace> f \<lbrace>\<lambda>rv s. valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits\<rbrace>
 6. \<And>x111 x112 x113 x114. cap = capability.CNodeCap x111 x112 x113 x114 \<Longrightarrow> \<lbrace>\<lambda>s. 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s)\<rbrace> f \<lbrace>\<lambda>rv s. 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s)\<rbrace> proof (prove)
goal:
No subgoals!