theory Detype_C

lemma valid_untyped_capE:
  assumes vuc: "s \<turnstile>' UntypedCap d ptr bits idx"
  and rl: "\<lbrakk>is_aligned ptr bits; valid_untyped' d ptr bits idx s; ptr \<noteq> 0; bits < word_bits \<rbrakk> \<Longrightarrow> P"
  shows P proof (rule rl) from vuc show al: "is_aligned ptr bits" and vu: "valid_untyped' d ptr bits idx s" and p0: "ptr \<noteq> 0" unfolding valid_cap'_def capAligned_def by auto from al p0 show wb: "bits < word_bits" by (clarsimp elim!: is_aligned_get_word_bits[where 'a=32, folded word_bits_def]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P proof (state)
goal (4 subgoals):
 1. is_aligned ptr bits
 2. valid_untyped' d ptr bits idx s
 3. ptr \<noteq> 0
 4. bits < word_bits proof (chain)
picking this:
valid_cap' (capability.UntypedCap d ptr bits idx) s proof (prove)
using this:
valid_cap' (capability.UntypedCap d ptr bits idx) s

goal (1 subgoal):
 1. is_aligned ptr bits &&& valid_untyped' d ptr bits idx s &&& ptr \<noteq> 0 proof (prove)
using this:
(is_aligned (global.capUntypedPtr (capability.UntypedCap d ptr bits idx)) (capBits (capability.UntypedCap d ptr bits idx)) \<and> capBits (capability.UntypedCap d ptr bits idx) < word_bits) \<and> (case capability.UntypedCap d ptr bits idx 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> local.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)

goal (1 subgoal):
 1. is_aligned ptr bits &&& valid_untyped' d ptr bits idx s &&& ptr \<noteq> 0 proof (state)
this:
is_aligned ptr bits
valid_untyped' d ptr bits idx s
ptr \<noteq> 0

goal (1 subgoal):
 1. bits < word_bits proof (chain)
picking this:
is_aligned ptr bits
ptr \<noteq> 0 proof (prove)
using this:
is_aligned ptr bits
ptr \<noteq> 0

goal (1 subgoal):
 1. bits < word_bits proof (state)
this:
bits < word_bits

goal:
No subgoals!