theory Detype_C

lemma cmap_relation_disjoint:
  fixes  rel :: "'a :: pspace_storable \<Rightarrow> 'b :: mem_type \<Rightarrow> bool" and x :: "'b :: mem_type ptr"
  assumes vuc: "s \<turnstile>' UntypedCap d ptr bits idx"
  and   invs: "invs' s"
  and     cm: "cmap_relation (proj \<circ>\<^sub>m (ksPSpace s)) (cslift s') Ptr rel"
  and     ht: "s' \<Turnstile>\<^sub>c x"
  and     tp: "\<And>ko v. proj ko = Some v \<Longrightarrow> koType TYPE('a) = koTypeOf ko"
  and     xv: "x \<notin> Ptr ` {ptr..+2 ^ bits}"
  and    sof: "size_td (typ_info_t TYPE('b)) \<le> 2 ^ objBits (undefined :: 'a)"
  shows  "{ptr_val x..+size_of TYPE('b)} \<inter> {ptr..+2 ^ bits} = {}" proof - from vuc have al: "is_aligned ptr bits"
    and vu: "valid_untyped' d ptr bits idx s" and p0: "ptr \<noteq> 0"
    and wb: "bits < word_bits"
    and [simp]: "(ptr && ~~ mask bits) = ptr" by (auto elim!: valid_untyped_capE) note blah[simp del] =  atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex let ?ran = "{ptr..ptr + 2 ^ bits - 1}" let ?s = "(s\<lparr>ksPSpace := (ksPSpace s) |` (- ?ran)\<rparr>)" from cm ht obtain ko and v :: 'a where ks: "ksPSpace s (ptr_val x) = Some ko" and po: "proj ko = Some v" apply (rule cmap_relation_h_t_valid) apply (clarsimp simp: map_comp_Some_iff) done let ?oran = "{ptr_val x .. ptr_val x + 2 ^ objBitsKO ko - 1}" let ?ran' = "{ptr..+2 ^ bits}" let ?oran' = "{ptr_val x..+2 ^ objBitsKO ko}" have ran' [simp]: "?ran' = ?ran" using al wb upto_intvl_eq by blast have oran' [simp]: "?oran' = ?oran" proof (rule upto_intvl_eq) from invs have "pspace_aligned' s" .. with ks show "is_aligned (ptr_val x) (objBitsKO ko)" .. qed from xv have "ptr_val x \<in> (- ?ran)" apply (simp only: ran' Compl_iff) apply (erule contrapos_nn) apply (erule image_eqI [rotated]) apply simp done hence "ksPSpace ?s (ptr_val x) = Some ko" using ks by auto hence "?oran \<inter> ?ran = {}" proof (rule pspace_no_overlapD'[where p = ptr and bits = bits,simplified]) from invs have "valid_pspace' s" .. with vu al show "pspace_no_overlap' ptr bits ?s" by (rule valid_untyped_no_overlap) qed hence "?oran' \<inter> ?ran' = {}" by simp thus "{ptr_val x..+size_of TYPE('b)} \<inter> ?ran' = {}" proof (rule disjoint_subset [rotated]) have "objBits (undefined :: 'a) = objBitsKO ko" using po apply (simp add: objBits_def) apply (rule objBits_type) apply (subst iffD1 [OF project_koType]) apply (fastforce simp add: project_inject) apply (erule tp) done thus "{ptr_val x..+size_of TYPE('b)} \<subseteq> ?oran'" using sof apply - apply (rule intvl_start_le) apply (simp add: size_of_def) done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (state)
goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ 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 &&& bits < word_bits &&& ptr && ~~ mask bits = ptr proof (state)
this:
is_aligned ptr bits
valid_untyped' d ptr bits idx s
ptr \<noteq> 0
bits < word_bits
ptr && ~~ mask bits = ptr

goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} 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_span x \<inter> {ptr..+2 ^ bits} = {} proof (state)
goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (state)
goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (chain)
picking this:
cmap_relation (proj \<circ>\<^sub>m ksPSpace s) (cslift s') PTR('b) rel
s' \<Turnstile>\<^sub>c x proof (prove)
using this:
cmap_relation (proj \<circ>\<^sub>m ksPSpace s) (cslift s') PTR('b) rel
s' \<Turnstile>\<^sub>c x

goal (1 subgoal):
 1. (\<And>ko v. \<lbrakk>ksPSpace s (ptr_val x) = Some ko; proj ko = Some v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<And>v v' xa. \<lbrakk>\<And>ko v. \<lbrakk>ksPSpace s (ptr_val x) = Some ko; proj ko = Some v\<rbrakk> \<Longrightarrow> thesis; PTR('b) xa = x; (proj \<circ>\<^sub>m ksPSpace s) xa = Some v; cslift s' x = Some v'; rel v v'\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal:
No subgoals! proof (state)
this:
ksPSpace s (ptr_val x) = Some ko
proj ko = Some v

goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (state)
goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (state)
goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (state)
goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. {ptr..+2 ^ bits} = {ptr..ptr + 2 ^ bits - 1} proof (prove)
using this:
is_aligned ptr bits
bits < word_bits
is_aligned ?x ?n \<Longrightarrow> {?x..+2 ^ ?n} = {?x..?x + 2 ^ ?n - 1}

goal (1 subgoal):
 1. {ptr..+2 ^ bits} = {ptr..ptr + 2 ^ bits - 1} proof (state)
this:
{ptr..+2 ^ bits} = {ptr..ptr + 2 ^ bits - 1}

goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. {ptr_val x..+2 ^ objBitsKO ko} = {ptr_val x..ptr_val x + 2 ^ objBitsKO ko - 1} proof (state)
goal (1 subgoal):
 1. is_aligned (ptr_val x) (objBitsKO ko) proof (chain)
picking this:
invs' s proof (prove)
using this:
invs' s

goal (1 subgoal):
 1. pspace_aligned' s proof (state)
this:
pspace_aligned' s

goal (1 subgoal):
 1. is_aligned (ptr_val x) (objBitsKO ko) proof (chain)
picking this:
ksPSpace s (ptr_val x) = Some ko
pspace_aligned' s proof (prove)
using this:
ksPSpace s (ptr_val x) = Some ko
pspace_aligned' s

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

goal:
No subgoals! proof (state)
this:
{ptr_val x..+2 ^ objBitsKO ko} = {ptr_val x..ptr_val x + 2 ^ objBitsKO ko - 1}

goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (chain)
picking this:
x \<notin> PTR('b) ` {ptr..+2 ^ bits} proof (prove)
using this:
x \<notin> PTR('b) ` {ptr..+2 ^ bits}

goal (1 subgoal):
 1. ptr_val x \<in> - {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. x \<notin> PTR('b) ` {ptr..ptr + 2 ^ bits - 1} \<Longrightarrow> ptr_val x \<notin> {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. ptr_val x \<in> {ptr..ptr + 2 ^ bits - 1} \<Longrightarrow> x \<in> PTR('b) ` {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. x = PTR('b) (ptr_val x) proof (prove)
goal:
No subgoals! proof (state)
this:
ptr_val x \<in> - {ptr..ptr + 2 ^ bits - 1}

goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (prove)
using this:
ptr_val x \<in> - {ptr..ptr + 2 ^ bits - 1}

goal (1 subgoal):
 1. ksPSpace (s\<lparr>ksPSpace := ksPSpace s|\<^bsub>(- {ptr..ptr + 2 ^ bits - 1})\<^esub>\<rparr>) (ptr_val x) = Some ko proof (prove)
using this:
ptr_val x \<in> - {ptr..ptr + 2 ^ bits - 1}
ksPSpace s (ptr_val x) = Some ko

goal (1 subgoal):
 1. ksPSpace (s\<lparr>ksPSpace := ksPSpace s|\<^bsub>(- {ptr..ptr + 2 ^ bits - 1})\<^esub>\<rparr>) (ptr_val x) = Some ko proof (state)
this:
ksPSpace (s\<lparr>ksPSpace := ksPSpace s|\<^bsub>(- {ptr..ptr + 2 ^ bits - 1})\<^esub>\<rparr>) (ptr_val x) = Some ko

goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (prove)
using this:
ksPSpace (s\<lparr>ksPSpace := ksPSpace s|\<^bsub>(- {ptr..ptr + 2 ^ bits - 1})\<^esub>\<rparr>) (ptr_val x) = Some ko

goal (1 subgoal):
 1. {ptr_val x..ptr_val x + 2 ^ objBitsKO ko - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} = {} proof (state)
goal (1 subgoal):
 1. pspace_no_overlap' ptr bits (s\<lparr>ksPSpace := ksPSpace s|\<^bsub>(- {ptr..ptr + 2 ^ bits - 1})\<^esub>\<rparr>) proof (chain)
picking this:
invs' s proof (prove)
using this:
invs' s

goal (1 subgoal):
 1. valid_pspace' s proof (state)
this:
valid_pspace' s

goal (1 subgoal):
 1. pspace_no_overlap' ptr bits (s\<lparr>ksPSpace := ksPSpace s|\<^bsub>(- {ptr..ptr + 2 ^ bits - 1})\<^esub>\<rparr>) proof (chain)
picking this:
valid_untyped' d ptr bits idx s
is_aligned ptr bits
valid_pspace' s proof (prove)
using this:
valid_untyped' d ptr bits idx s
is_aligned ptr bits
valid_pspace' s

goal (1 subgoal):
 1. pspace_no_overlap' ptr bits (s\<lparr>ksPSpace := ksPSpace s|\<^bsub>(- {ptr..ptr + 2 ^ bits - 1})\<^esub>\<rparr>) proof (state)
this:
pspace_no_overlap' ptr bits (s\<lparr>ksPSpace := ksPSpace s|\<^bsub>(- {ptr..ptr + 2 ^ bits - 1})\<^esub>\<rparr>)

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

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

goal (1 subgoal):
 1. {ptr_val x..+2 ^ objBitsKO ko} \<inter> {ptr..+2 ^ bits} = {} proof (state)
this:
{ptr_val x..+2 ^ objBitsKO ko} \<inter> {ptr..+2 ^ bits} = {}

goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (prove)
using this:
{ptr_val x..+2 ^ objBitsKO ko} \<inter> {ptr..+2 ^ bits} = {}

goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (state)
goal (1 subgoal):
 1. ptr_span x \<subseteq> {ptr_val x..+2 ^ objBitsKO ko} proof (prove)
goal (1 subgoal):
 1. objBits undefined = objBitsKO ko proof (prove)
using this:
proj ko = Some v

goal (1 subgoal):
 1. objBits undefined = objBitsKO ko proof (prove)
goal (1 subgoal):
 1. proj ko = Some v \<Longrightarrow> objBitsKO (injectKOS undefined) = objBitsKO ko proof (prove)
goal (1 subgoal):
 1. proj ko = Some v \<Longrightarrow> koTypeOf (injectKOS undefined) = koTypeOf ko proof (prove)
goal (2 subgoals):
 1. proj ko = Some v \<Longrightarrow> \<exists>v. projectKO_opt (injectKOS undefined) = Some v
 2. proj ko = Some v \<Longrightarrow> koType TYPE(?'aa3) = koTypeOf ko proof (prove)
goal (1 subgoal):
 1. proj ko = Some v \<Longrightarrow> koType TYPE('a) = koTypeOf ko proof (prove)
goal:
No subgoals! proof (state)
this:
objBits undefined = objBitsKO ko

goal (1 subgoal):
 1. ptr_span x \<subseteq> {ptr_val x..+2 ^ objBitsKO ko} proof (prove)
using this:
objBits undefined = objBitsKO ko

goal (1 subgoal):
 1. ptr_span x \<subseteq> {ptr_val x..+2 ^ objBitsKO ko} proof (prove)
using this:
objBits undefined = objBitsKO ko
size_td (typ_info_t TYPE('b)) \<le> 2 ^ objBits undefined

goal (1 subgoal):
 1. ptr_span x \<subseteq> {ptr_val x..+2 ^ objBitsKO ko} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>objBits undefined = objBitsKO ko; size_td (typ_info_t TYPE('b)) \<le> 2 ^ objBits undefined\<rbrakk> \<Longrightarrow> ptr_span x \<subseteq> {ptr_val x..+2 ^ objBitsKO ko} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>objBits undefined = objBitsKO ko; size_td (typ_info_t TYPE('b)) \<le> 2 ^ objBits undefined\<rbrakk> \<Longrightarrow> size_of TYPE('b) \<le> 2 ^ objBitsKO ko proof (prove)
goal:
No subgoals! proof (state)
this:
ptr_span x \<subseteq> {ptr_val x..+2 ^ objBitsKO ko}

goal:
No subgoals! proof (state)
this:
ptr_span x \<inter> {ptr..+2 ^ bits} = {}

goal:
No subgoals!