theory Detype_C

lemma cmap_relation_disjoint_cte:
  assumes vuc: "s \<turnstile>' UntypedCap d ptr bits idx"
  and   invs: "invs' s"
  and     cm: "cmap_relation (ctes_of s) (cslift s') Ptr ccte_relation"
  and     ht: "s' \<Turnstile>\<^sub>c (x :: cte_C ptr)"
  and     xv: "x \<notin> Ptr ` {ptr..+2 ^ bits}"
  shows  "{ptr_val x..+size_of TYPE(cte_C)} \<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 cte where ks: "ctes_of s (ptr_val x) = Some cte" apply (rule cmap_relation_h_t_valid) apply (clarsimp simp: map_comp_Some_iff) done let ?oran = "{ptr_val x .. ptr_val x + 2 ^ objBits cte - 1}" let ?ran' = "{ptr..+2 ^ bits}" let ?oran' = "{ptr_val x..+2 ^ objBits cte}" have ran' [simp]: "?ran' = ?ran" using al wb upto_intvl_eq by auto have oran' [simp]: "?oran' = ?oran" proof (rule upto_intvl_eq) from ks show "is_aligned (ptr_val x) (objBits cte)" by (rule ctes_of_is_aligned) qed from xv have px: "ptr_val x \<in> (- ?ran)" apply (simp only: ran' Compl_iff) apply (erule contrapos_nn) apply (erule image_eqI [rotated]) apply simp done from ks have "cte_wp_at' ((=) cte) (ptr_val x) s" by (clarsimp simp: cte_wp_at_ctes_of) thus ?thesis proof (cases rule: cte_wp_at_casesE') case (cte cte') hence "ksPSpace ?s (ptr_val x) = Some (injectKOS cte)" using px by simp hence "?oran \<inter> ?ran = {}" unfolding objBits_def 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 ?thesis by (simp add: objBits_simps' size_of_def) next case (tcb n tcb _ _) hence koat: "ko_at' tcb (ptr_val x - n) s" apply - apply (erule obj_atI', simp_all add: objBits_simps' projectKOs) done let ?tran = "{ptr_val x - n .. (ptr_val x - n) + 2 ^ objBits tcb - 1}" have ot: "?oran \<subseteq> ?tran" by (rule tcb_cte_in_range[where p = "ptr_val x - n" and n = "n",
                                simplified diff_add_cancel]) fact+ also from xv have "\<not> \<dots> \<subseteq> ?ran" proof (rule contrapos_nn) assume "?tran \<subseteq> ?ran" with ot have "?oran \<subseteq> ?ran" by (rule order_trans) hence "ptr_val x \<in> ?ran" proof (rule subsetD) from tcb have "is_aligned (ptr_val x) (objBits cte)" apply - apply (drule (1) tcb_cte_cases_aligned) apply simp done hence "ptr_val x \<le> ptr_val x + 2 ^ objBits cte - 1" by (rule is_aligned_no_overflow) thus "ptr_val x \<in> ?oran" by (rule first_in_uptoD) qed thus "x \<in> Ptr ` {ptr..+2 ^ bits}" unfolding ran' by (rule image_eqI [where x = "ptr_val x", rotated]) simp qed hence "?tran \<inter> ?ran' = {}" apply (rule contrapos_np) apply (rule valid_untyped_cap_ko_at_disjoint [OF vuc koat]) apply simp done finally have "{ptr_val x..+2 ^ objBits cte} \<inter> ?ran' = {}" using ot unfolding oran' by blast thus ?thesis by (simp add: objBits_simps' size_of_def) 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 (ctes_of s) (cslift s') cte_Ptr ccte_relation
s' \<Turnstile>\<^sub>c x proof (prove)
using this:
cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation
s' \<Turnstile>\<^sub>c x

goal (1 subgoal):
 1. (\<And>cte. ctes_of s (ptr_val x) = Some cte \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<And>v v' xa. \<lbrakk>\<And>cte. ctes_of s (ptr_val x) = Some cte \<Longrightarrow> thesis; cte_Ptr xa = x; ctes_of s xa = Some v; cslift s' x = Some v'; ccte_relation v v'\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal:
No subgoals! proof (state)
this:
ctes_of s (ptr_val x) = Some cte

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

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

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

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

goal (1 subgoal):
 1. ptr_val x \<in> - {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. x \<notin> cte_Ptr ` {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> cte_Ptr ` {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. x = cte_Ptr (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 (chain)
picking this:
ctes_of s (ptr_val x) = Some cte proof (prove)
using this:
ctes_of s (ptr_val x) = Some cte

goal (1 subgoal):
 1. cte_wp_at' ((=) cte) (ptr_val x) s proof (state)
this:
cte_wp_at' ((=) cte) (ptr_val x) s

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

goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (state)
goal (2 subgoals):
 1. \<And>ctea. \<lbrakk>ksPSpace s (ptr_val x) = Some (KOCTE ctea); is_aligned (ptr_val x) cte_level_bits; cte = ctea; ps_clear (ptr_val x) cteSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {}
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (state)
this:
ksPSpace s (ptr_val x) = Some (KOCTE cte')
is_aligned (ptr_val x) cte_level_bits
cte = cte'
ps_clear (ptr_val x) cteSizeBits s

goal (2 subgoals):
 1. \<And>ctea. \<lbrakk>ksPSpace s (ptr_val x) = Some (KOCTE ctea); is_aligned (ptr_val x) cte_level_bits; cte = ctea; ps_clear (ptr_val x) cteSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {}
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (prove)
using this:
ksPSpace s (ptr_val x) = Some (KOCTE cte')
is_aligned (ptr_val x) cte_level_bits
cte = cte'
ps_clear (ptr_val x) cteSizeBits s

goal (1 subgoal):
 1. ksPSpace (s\<lparr>ksPSpace := ksPSpace s|\<^bsub>(- {ptr..ptr + 2 ^ bits - 1})\<^esub>\<rparr>) (ptr_val x) = Some (injectKOS cte) proof (prove)
using this:
ksPSpace s (ptr_val x) = Some (KOCTE cte')
is_aligned (ptr_val x) cte_level_bits
cte = cte'
ps_clear (ptr_val x) cteSizeBits s
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 (injectKOS cte) proof (state)
this:
ksPSpace (s\<lparr>ksPSpace := ksPSpace s|\<^bsub>(- {ptr..ptr + 2 ^ bits - 1})\<^esub>\<rparr>) (ptr_val x) = Some (injectKOS cte)

goal (2 subgoals):
 1. \<And>ctea. \<lbrakk>ksPSpace s (ptr_val x) = Some (KOCTE ctea); is_aligned (ptr_val x) cte_level_bits; cte = ctea; ps_clear (ptr_val x) cteSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {}
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> 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 (injectKOS cte)

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

goal (1 subgoal):
 1. {ptr_val x..ptr_val x + 2 ^ objBitsKO (injectKOS cte) - 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 ^ objBits cte - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} = {}

goal (2 subgoals):
 1. \<And>ctea. \<lbrakk>ksPSpace s (ptr_val x) = Some (KOCTE ctea); is_aligned (ptr_val x) cte_level_bits; cte = ctea; ps_clear (ptr_val x) cteSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {}
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (prove)
using this:
{ptr_val x..ptr_val x + 2 ^ objBits cte - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} = {}

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

goal (2 subgoals):
 1. \<And>ctea. \<lbrakk>ksPSpace s (ptr_val x) = Some (KOCTE ctea); is_aligned (ptr_val x) cte_level_bits; cte = ctea; ps_clear (ptr_val x) cteSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {}
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (prove)
using this:
{ptr_val x..+2 ^ objBits cte} \<inter> {ptr..+2 ^ bits} = {}

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

goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (state)
goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (state)
this:
ksPSpace s (ptr_val x - n) = Some (KOTCB tcb)
is_aligned (ptr_val x - n) tcbBlockSizeBits
tcb_cte_cases n = Some (getF_, setF_)
cte = getF_ tcb
ps_clear (ptr_val x - n) tcbBlockSizeBits s

goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (prove)
using this:
ksPSpace s (ptr_val x - n) = Some (KOTCB tcb)
is_aligned (ptr_val x - n) tcbBlockSizeBits
tcb_cte_cases n = Some (getF_, setF_)
cte = getF_ tcb
ps_clear (ptr_val x - n) tcbBlockSizeBits s

goal (1 subgoal):
 1. ko_at' tcb (ptr_val x - n) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF_, setF_); cte = getF_ tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ko_at' tcb (ptr_val x - n) s proof (prove)
goal:
No subgoals! proof (state)
this:
ko_at' tcb (ptr_val x - n) s

goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (state)
goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. {ptr_val x..ptr_val x + 2 ^ objBits cte - 1} \<subseteq> {ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1} proof (state)
this:
{ptr_val x..ptr_val x + 2 ^ objBits cte - 1} \<subseteq> {ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1}

goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (state)
this:
{ptr_val x..ptr_val x + 2 ^ objBits cte - 1} \<subseteq> {ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1}

goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (chain)
picking this:
x \<notin> cte_Ptr ` {ptr..+2 ^ bits} proof (prove)
using this:
x \<notin> cte_Ptr ` {ptr..+2 ^ bits}

goal (1 subgoal):
 1. \<not> {ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (state)
goal (1 subgoal):
 1. {ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<Longrightarrow> x \<in> cte_Ptr ` {ptr..+2 ^ bits} proof (state)
this:
{ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}

goal (1 subgoal):
 1. {ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<Longrightarrow> x \<in> cte_Ptr ` {ptr..+2 ^ bits} proof (chain)
picking this:
{ptr_val x..ptr_val x + 2 ^ objBits cte - 1} \<subseteq> {ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1}
{ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (prove)
using this:
{ptr_val x..ptr_val x + 2 ^ objBits cte - 1} \<subseteq> {ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1}
{ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}

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

goal (1 subgoal):
 1. {ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<Longrightarrow> x \<in> cte_Ptr ` {ptr..+2 ^ bits} proof (prove)
using this:
{ptr_val x..ptr_val x + 2 ^ objBits cte - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}

goal (1 subgoal):
 1. ptr_val x \<in> {ptr..ptr + 2 ^ bits - 1} proof (state)
goal (1 subgoal):
 1. ptr_val x \<in> {ptr_val x..ptr_val x + 2 ^ objBits cte - 1} proof (chain)
picking this:
ksPSpace s (ptr_val x - n) = Some (KOTCB tcb)
is_aligned (ptr_val x - n) tcbBlockSizeBits
tcb_cte_cases n = Some (getF_, setF_)
cte = getF_ tcb
ps_clear (ptr_val x - n) tcbBlockSizeBits s proof (prove)
using this:
ksPSpace s (ptr_val x - n) = Some (KOTCB tcb)
is_aligned (ptr_val x - n) tcbBlockSizeBits
tcb_cte_cases n = Some (getF_, setF_)
cte = getF_ tcb
ps_clear (ptr_val x - n) tcbBlockSizeBits s

goal (1 subgoal):
 1. is_aligned (ptr_val x) (objBits cte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF_, setF_); cte = getF_ tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> is_aligned (ptr_val x) (objBits cte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); tcb_cte_cases n = Some (getF_, setF_); cte = getF_ tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s; is_aligned (ptr_val x - n + n) (objBits ?cte5)\<rbrakk> \<Longrightarrow> is_aligned (ptr_val x) (objBits cte) proof (prove)
goal:
No subgoals! proof (state)
this:
is_aligned (ptr_val x) (objBits cte)

goal (1 subgoal):
 1. ptr_val x \<in> {ptr_val x..ptr_val x + 2 ^ objBits cte - 1} proof (prove)
using this:
is_aligned (ptr_val x) (objBits cte)

goal (1 subgoal):
 1. ptr_val x \<le> ptr_val x + 2 ^ objBits cte - 1 proof (state)
this:
ptr_val x \<le> ptr_val x + 2 ^ objBits cte - 1

goal (1 subgoal):
 1. ptr_val x \<in> {ptr_val x..ptr_val x + 2 ^ objBits cte - 1} proof (prove)
using this:
ptr_val x \<le> ptr_val x + 2 ^ objBits cte - 1

goal (1 subgoal):
 1. ptr_val x \<in> {ptr_val x..ptr_val x + 2 ^ objBits cte - 1} proof (state)
this:
ptr_val x \<in> {ptr_val x..ptr_val x + 2 ^ objBits cte - 1}

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

goal (1 subgoal):
 1. {ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<Longrightarrow> x \<in> cte_Ptr ` {ptr..+2 ^ bits} proof (prove)
using this:
ptr_val x \<in> {ptr..ptr + 2 ^ bits - 1}

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

goal (1 subgoal):
 1. x \<in> cte_Ptr ` {ptr..ptr + 2 ^ bits - 1} proof (state)
this:
x \<in> cte_Ptr ` {ptr..+2 ^ bits}

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

goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (prove)
using this:
\<not> {ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}

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

goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (chain)
picking this:
(\<And>x y. x \<subseteq> y \<Longrightarrow> x \<inter> {ptr..+2 ^ bits} \<subseteq> y \<inter> {ptr..+2 ^ bits}) \<Longrightarrow> {ptr_val x..ptr_val x + 2 ^ objBits cte - 1} \<inter> {ptr..+2 ^ bits} \<subseteq> {} proof (prove)
using this:
(\<And>x y. x \<subseteq> y \<Longrightarrow> x \<inter> {ptr..+2 ^ bits} \<subseteq> y \<inter> {ptr..+2 ^ bits}) \<Longrightarrow> {ptr_val x..ptr_val x + 2 ^ objBits cte - 1} \<inter> {ptr..+2 ^ bits} \<subseteq> {}

goal (1 subgoal):
 1. {ptr_val x..+2 ^ objBits cte} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
using this:
(\<And>x y. x \<subseteq> y \<Longrightarrow> x \<inter> {ptr..+2 ^ bits} \<subseteq> y \<inter> {ptr..+2 ^ bits}) \<Longrightarrow> {ptr_val x..ptr_val x + 2 ^ objBits cte - 1} \<inter> {ptr..+2 ^ bits} \<subseteq> {}
{ptr_val x..ptr_val x + 2 ^ objBits cte - 1} \<subseteq> {ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1}

goal (1 subgoal):
 1. {ptr_val x..+2 ^ objBits cte} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
using this:
(\<And>x y. x \<subseteq> y \<Longrightarrow> x \<inter> {ptr..+2 ^ bits} \<subseteq> y \<inter> {ptr..+2 ^ bits}) \<Longrightarrow> {ptr_val x..ptr_val x + 2 ^ objBits cte - 1} \<inter> {ptr..+2 ^ bits} \<subseteq> {}
{ptr_val x..ptr_val x + 2 ^ objBits cte - 1} \<subseteq> {ptr_val x - n..ptr_val x - n + 2 ^ objBits tcb - 1}

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

goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (ptr_val x - n) = Some (KOTCB tcb); is_aligned (ptr_val x - n) tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (ptr_val x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (prove)
using this:
{ptr_val x..+2 ^ objBits cte} \<inter> {ptr..+2 ^ bits} = {}

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

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

goal:
No subgoals!