theory Detype_C

lemma valid_untyped_cap_ko_at_disjoint:
  assumes vu: "s \<turnstile>' UntypedCap d ptr bits idx"
  and   koat: "ko_at' ko x s"
  and     pv: "{x .. x + 2 ^ objBits ko - 1} \<inter> {ptr .. ptr + 2 ^ bits - 1} \<noteq> {}"
  shows   "{x .. x + 2 ^ objBits ko - 1} \<subseteq> {ptr .. ptr + 2 ^ bits - 1}" proof - from vu have "is_aligned ptr bits" unfolding valid_cap'_def capAligned_def by simp moreover from koat have "is_aligned x (objBits ko)" by (rule obj_atE') (simp add: projectKOs objBits_def project_inject) ultimately show ?thesis proof (cases rule: aligned_ranges_subset_or_disjointE) case disjoint thus ?thesis using pv by auto next case subset2 thus ?thesis . next case subset1 note blah[simp del] =  atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex have  "\<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko) x s" using vu unfolding valid_cap'_def valid_untyped'_def apply clarsimp apply (drule_tac x = x in spec) apply (clarsimp simp:ko_wp_at'_def) done with koat have "\<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBits ko - 1}" apply - apply (erule obj_atE')+ apply (simp add: ko_wp_at'_def projectKOs obj_range'_def not_less objBits_def project_inject) done thus ?thesis using subset1 by (simp add: psubset_eq del: Icc_eq_Icc) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (state)
goal (1 subgoal):
 1. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} 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 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 proof (state)
this:
is_aligned ptr bits

goal (1 subgoal):
 1. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (state)
this:
is_aligned ptr bits

goal (1 subgoal):
 1. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (chain)
picking this:
ko_at' ko x s proof (prove)
using this:
ko_at' ko x s

goal (1 subgoal):
 1. is_aligned x (objBits ko) proof (state)
this:
is_aligned x (objBits ko)

goal (1 subgoal):
 1. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (chain)
picking this:
is_aligned ptr bits
is_aligned x (objBits ko) proof (prove)
using this:
is_aligned ptr bits
is_aligned x (objBits ko)

goal (1 subgoal):
 1. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (state)
goal (3 subgoals):
 1. {ptr..ptr + 2 ^ bits - 1} \<inter> {x..x + 2 ^ objBits ko - 1} = {} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}
 2. {ptr..ptr + 2 ^ bits - 1} \<subseteq> {x..x + 2 ^ objBits ko - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}
 3. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (state)
this:
{ptr..ptr + 2 ^ bits - 1} \<inter> {x..x + 2 ^ objBits ko - 1} = {}

goal (3 subgoals):
 1. {ptr..ptr + 2 ^ bits - 1} \<inter> {x..x + 2 ^ objBits ko - 1} = {} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}
 2. {ptr..ptr + 2 ^ bits - 1} \<subseteq> {x..x + 2 ^ objBits ko - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}
 3. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (prove)
using this:
{ptr..ptr + 2 ^ bits - 1} \<inter> {x..x + 2 ^ objBits ko - 1} = {}

goal (1 subgoal):
 1. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (prove)
using this:
{ptr..ptr + 2 ^ bits - 1} \<inter> {x..x + 2 ^ objBits ko - 1} = {}
{x..x + 2 ^ objBits ko - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}

goal (1 subgoal):
 1. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (state)
this:
{x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}

goal (2 subgoals):
 1. {ptr..ptr + 2 ^ bits - 1} \<subseteq> {x..x + 2 ^ objBits ko - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}
 2. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (state)
goal (2 subgoals):
 1. {ptr..ptr + 2 ^ bits - 1} \<subseteq> {x..x + 2 ^ objBits ko - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}
 2. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (state)
this:
{x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}

goal (2 subgoals):
 1. {ptr..ptr + 2 ^ bits - 1} \<subseteq> {x..x + 2 ^ objBits ko - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}
 2. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (prove)
using this:
{x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}

goal (1 subgoal):
 1. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (state)
this:
{x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}

goal (1 subgoal):
 1. {ptr..ptr + 2 ^ bits - 1} \<subseteq> {x..x + 2 ^ objBits ko - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (state)
goal (1 subgoal):
 1. {ptr..ptr + 2 ^ bits - 1} \<subseteq> {x..x + 2 ^ objBits ko - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (state)
this:
{ptr..ptr + 2 ^ bits - 1} \<subseteq> {x..x + 2 ^ objBits ko - 1}

goal (1 subgoal):
 1. {ptr..ptr + 2 ^ bits - 1} \<subseteq> {x..x + 2 ^ objBits ko - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (state)
this:
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)
({?a..?b} \<subseteq> {?c..?d}) = (\<not> ?a \<le> ?b \<or> ?c \<le> ?a \<and> ?b \<le> ?d)
(?i \<in> {?l..<?u}) = (?l \<le> ?i \<and> ?i < ?u)
{?a..?b} \<inter> {?c..?d} = {max ?a ?c..min ?b ?d}
({?a..?b} = {}) = (\<not> ?a \<le> ?b)
(\<exists>x. ?P x) = (\<exists>a b. ?P (a, b))

goal (1 subgoal):
 1. {ptr..ptr + 2 ^ bits - 1} \<subseteq> {x..x + 2 ^ objBits ko - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko) x s proof (prove)
using this:
valid_cap' (capability.UntypedCap d ptr bits idx) s

goal (1 subgoal):
 1. \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko) x s proof (prove)
using this:
capAligned (capability.UntypedCap d ptr bits idx) \<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> (\<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {r..r + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d r n f) \<noteq> {}) ptr' 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. \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko) x s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capAligned (capability.UntypedCap d ptr bits idx); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}) ptr' s; 0 < ptr; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; idx \<le> 2 ^ bits; is_aligned (word_of_nat idx) minUntypedSizeBits; ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko) x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capAligned (capability.UntypedCap d ptr bits idx); 0 < ptr; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; idx \<le> 2 ^ bits; is_aligned (word_of_nat idx) minUntypedSizeBits; ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko) x s; \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko \<or> obj_range' x ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}) x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko) x s

goal (1 subgoal):
 1. {ptr..ptr + 2 ^ bits - 1} \<subseteq> {x..x + 2 ^ objBits ko - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (chain)
picking this:
ko_at' ko x s
\<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko) x s proof (prove)
using this:
ko_at' ko x s
\<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko) x s

goal (1 subgoal):
 1. \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBits ko - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ko x s; \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko) x s\<rbrakk> \<Longrightarrow> \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBits ko - 1} proof (prove)
goal (1 subgoal):
 1. \<And>koa obj. \<lbrakk>\<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko) x s; ksPSpace s x = Some koa; is_aligned x (objBitsKO koa); fst (projectKO koa s) = {(obj, s)}; obj = ko; ps_clear x (objBitsKO koa) s\<rbrakk> \<Longrightarrow> \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBits ko - 1} proof (prove)
goal:
No subgoals! proof (state)
this:
\<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBits ko - 1}

goal (1 subgoal):
 1. {ptr..ptr + 2 ^ bits - 1} \<subseteq> {x..x + 2 ^ objBits ko - 1} \<Longrightarrow> {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (prove)
using this:
\<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBits ko - 1}

goal (1 subgoal):
 1. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (prove)
using this:
\<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBits ko - 1}
{ptr..ptr + 2 ^ bits - 1} \<subseteq> {x..x + 2 ^ objBits ko - 1}

goal (1 subgoal):
 1. {x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (state)
this:
{x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}

goal:
No subgoals! proof (state)
this:
{x..x + 2 ^ objBits ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}

goal:
No subgoals!