theory Detype_C

lemma cmap_relation_disjoint_tcb:
  fixes x :: "tcb_C ptr"
  assumes vuc: "s \<turnstile>' UntypedCap d ptr bits idx"
  and    invs: "invs' s"
  and      cm: "cmap_relation (projectKO_opt \<circ>\<^sub>m (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation"
  and      ht: "s' \<Turnstile>\<^sub>c x"
  and      xv: "x \<notin> Ptr ` {ptr..+2 ^ bits}"
  shows  "{ptr_val x..+size_of TYPE(tcb_C)} \<inter> {ptr..+2 ^ bits} = {}" proof - let ?ran = "{ptr..ptr + 2 ^ bits - 1}" let ?s = "(s\<lparr>ksPSpace := (ksPSpace s) |` (- ?ran)\<rparr>)" from cm ht invs obtain tcb :: tcb where koat: "ko_at' tcb  (ctcb_ptr_to_tcb_ptr x) s" apply - apply (erule (1) cmap_relation_h_t_valid) apply (drule (1) map_to_ko_atI') apply clarsimp done let ?oran = "{ctcb_ptr_to_tcb_ptr x .. ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1}" let ?ran' = "{ptr..+2 ^ bits}" let ?oran' = "{ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb}" 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" by (auto elim!: valid_untyped_capE) have ran' [simp]: "?ran' = ?ran" using al wb upto_intvl_eq by blast have oran' [simp]: "?oran' = ?oran" proof (rule upto_intvl_eq) from koat show "is_aligned (ctcb_ptr_to_tcb_ptr x) (objBits tcb)" .. qed show ?thesis proof (rule disjoint_subset) from xv koat have "\<not> ?oran \<subseteq> ?ran" apply - apply (erule contrapos_nn) apply (drule tcb_ptr_to_ctcb_ptr_in_range) apply (rule image_eqI [where x = "ptr_val x"]) apply simp apply (drule (1) subsetD) apply simp done thus "{ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} \<inter> {ptr..+2 ^ bits} = {}" apply (rule contrapos_np) apply (rule valid_untyped_cap_ko_at_disjoint [OF vuc koat]) apply simp done from koat show "{ptr_val x..+size_of TYPE(tcb_C)} \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb}" by (metis tcb_ptr_to_ctcb_ptr_in_range' tcb_aligned' obj_at'_weakenE) 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 (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 (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation
s' \<Turnstile>\<^sub>c x
invs' s proof (prove)
using this:
cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation
s' \<Turnstile>\<^sub>c x
invs' s

goal (1 subgoal):
 1. (\<And>tcb. ko_at' tcb (ctcb_ptr_to_tcb_ptr x) s \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>tcb. ko_at' tcb (ctcb_ptr_to_tcb_ptr x) s \<Longrightarrow> thesis; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; s' \<Turnstile>\<^sub>c x; invs' s\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<And>v v' xa. \<lbrakk>\<And>tcb. ko_at' tcb (ctcb_ptr_to_tcb_ptr x) s \<Longrightarrow> thesis; s' \<Turnstile>\<^sub>c x; invs' s; tcb_ptr_to_ctcb_ptr xa = x; map_to_tcbs (ksPSpace s) xa = Some v; cslift s' x = Some v'; ctcb_relation v v'\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<And>v v' xa. \<lbrakk>\<And>tcb. ko_at' tcb (ctcb_ptr_to_tcb_ptr x) s \<Longrightarrow> thesis; s' \<Turnstile>\<^sub>c x; invs' s; tcb_ptr_to_ctcb_ptr xa = x; cslift s' x = Some v'; ctcb_relation v v'; ko_at' v xa s\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal:
No subgoals! proof (state)
this:
ko_at' tcb (ctcb_ptr_to_tcb_ptr x) s

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 (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 proof (state)
this:
is_aligned ptr bits
valid_untyped' d ptr bits idx s
ptr \<noteq> 0
bits < word_bits

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. {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} = {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1} proof (state)
goal (1 subgoal):
 1. is_aligned (ctcb_ptr_to_tcb_ptr x) (objBits tcb) proof (chain)
picking this:
ko_at' tcb (ctcb_ptr_to_tcb_ptr x) s proof (prove)
using this:
ko_at' tcb (ctcb_ptr_to_tcb_ptr x) s

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

goal:
No subgoals! proof (state)
this:
{ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} = {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1}

goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (state)
goal (2 subgoals):
 1. ptr_span x \<subseteq> ?A
 2. ?A \<inter> {ptr..+2 ^ bits} = {} proof (chain)
picking this:
x \<notin> tcb_Ptr ` {ptr..+2 ^ bits}
ko_at' tcb (ctcb_ptr_to_tcb_ptr x) s proof (prove)
using this:
x \<notin> tcb_Ptr ` {ptr..+2 ^ bits}
ko_at' tcb (ctcb_ptr_to_tcb_ptr x) s

goal (1 subgoal):
 1. \<not> {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> tcb_Ptr ` {ptr..+2 ^ bits}; ko_at' tcb (ctcb_ptr_to_tcb_ptr x) s\<rbrakk> \<Longrightarrow> \<not> {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' tcb (ctcb_ptr_to_tcb_ptr x) s; {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> x \<in> tcb_Ptr ` {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}; ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr x)) \<in> {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1}\<rbrakk> \<Longrightarrow> x \<in> tcb_Ptr ` {ptr..+2 ^ bits} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>{ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}; ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr x)) \<in> {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1}\<rbrakk> \<Longrightarrow> x = tcb_Ptr (ptr_val x)
 2. \<lbrakk>{ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}; ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr x)) \<in> {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1}\<rbrakk> \<Longrightarrow> ptr_val x \<in> {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}; ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr x)) \<in> {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1}\<rbrakk> \<Longrightarrow> ptr_val x \<in> {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr x)) \<in> {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1}; ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr x)) \<in> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> ptr_val x \<in> {ptr..+2 ^ bits} proof (prove)
goal:
No subgoals! proof (state)
this:
\<not> {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}

goal (2 subgoals):
 1. ptr_span x \<subseteq> ?A
 2. ?A \<inter> {ptr..+2 ^ bits} = {} proof (prove)
using this:
\<not> {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}

goal (1 subgoal):
 1. {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} \<inter> {ptr..+2 ^ bits} \<noteq> {} \<Longrightarrow> {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} \<inter> {ptr..+2 ^ bits} \<noteq> {} \<Longrightarrow> {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} proof (prove)
goal:
No subgoals! proof (state)
this:
{ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} \<inter> {ptr..+2 ^ bits} = {}

goal (1 subgoal):
 1. ptr_span x \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} proof (chain)
picking this:
ko_at' tcb (ctcb_ptr_to_tcb_ptr x) s proof (prove)
using this:
ko_at' tcb (ctcb_ptr_to_tcb_ptr x) s

goal (1 subgoal):
 1. ptr_span x \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} proof (state)
this:
ptr_span x \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb}

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

goal:
No subgoals!