theory Detype_C

lemma cmap_relation_disjoint_user_data:
  fixes x :: "user_data_C ptr"
  assumes vuc: "s \<turnstile>' UntypedCap d ptr bits idx"
  and    invs: "invs' s"
  and      cm: "cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') Ptr cuser_user_data_relation"
  and      ht: "s' \<Turnstile>\<^sub>c x"
  and      xv: "x \<notin> Ptr ` {ptr..+2 ^ bits}"
  shows  "{ptr_val x..+size_of TYPE(user_data_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 have ks: "ksPSpace s (ptr_val x) = Some KOUserData" apply (rule cmap_relation_h_t_valid) apply (clarsimp simp: map_comp_Some_iff heap_to_user_data_def Let_def projectKO_opts_defs) apply (case_tac k') apply simp_all done let ?oran = "{ptr_val x .. ptr_val x + 2 ^ objBitsKO KOUserData - 1}" let ?ran' = "{ptr..+2 ^ bits}" let ?oran' = "{ptr_val x..+2 ^ objBitsKO KOUserData}" have ran' [simp]: "?ran' = ?ran" using al wb upto_intvl_eq by auto 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 KOUserData)" .. 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 KOUserData" using ks by simp 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(user_data_C)} \<inter> ?ran' = {}" proof (rule disjoint_subset [rotated]) show "{ptr_val x..+size_of TYPE(user_data_C)} \<subseteq> ?oran'" apply - apply (rule intvl_start_le) apply (simp add: size_of_def objBits_simps pageBits_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 (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation
s' \<Turnstile>\<^sub>c x proof (prove)
using this:
cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation
s' \<Turnstile>\<^sub>c x

goal (1 subgoal):
 1. ksPSpace s (ptr_val x) = Some KOUserData proof (prove)
goal (1 subgoal):
 1. \<And>v v' xa. \<lbrakk>PTR(user_data_C) xa = x; heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) xa = Some v; cslift s' x = Some v'; cuser_user_data_relation v v'\<rbrakk> \<Longrightarrow> ksPSpace s (ptr_val x) = Some KOUserData proof (prove)
goal (1 subgoal):
 1. \<And>v' xa z k'. \<lbrakk>cslift s' (PTR(user_data_C) xa) = Some v'; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) xa) v'; x = PTR(user_data_C) xa; ksPSpace s xa = Some k'; (case k' of KOUserData \<Rightarrow> Some UserData | _ \<Rightarrow> None) = Some z\<rbrakk> \<Longrightarrow> k' = KOUserData proof (prove)
goal (8 subgoals):
 1. \<And>v' xa z k' x1. \<lbrakk>cslift s' (PTR(user_data_C) xa) = Some v'; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) xa) v'; x = PTR(user_data_C) xa; ksPSpace s xa = Some k'; (case k' of KOUserData \<Rightarrow> Some UserData | _ \<Rightarrow> None) = Some z; k' = KOEndpoint x1\<rbrakk> \<Longrightarrow> k' = KOUserData
 2. \<And>v' xa z k' x2. \<lbrakk>cslift s' (PTR(user_data_C) xa) = Some v'; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) xa) v'; x = PTR(user_data_C) xa; ksPSpace s xa = Some k'; (case k' of KOUserData \<Rightarrow> Some UserData | _ \<Rightarrow> None) = Some z; k' = KONotification x2\<rbrakk> \<Longrightarrow> k' = KOUserData
 3. \<And>v' xa z k'. \<lbrakk>cslift s' (PTR(user_data_C) xa) = Some v'; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) xa) v'; x = PTR(user_data_C) xa; ksPSpace s xa = Some k'; (case k' of KOUserData \<Rightarrow> Some UserData | _ \<Rightarrow> None) = Some z; k' = KOKernelData\<rbrakk> \<Longrightarrow> k' = KOUserData
 4. \<And>v' xa z k'. \<lbrakk>cslift s' (PTR(user_data_C) xa) = Some v'; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) xa) v'; x = PTR(user_data_C) xa; ksPSpace s xa = Some k'; (case k' of KOUserData \<Rightarrow> Some UserData | _ \<Rightarrow> None) = Some z; k' = KOUserData\<rbrakk> \<Longrightarrow> k' = KOUserData
 5. \<And>v' xa z k'. \<lbrakk>cslift s' (PTR(user_data_C) xa) = Some v'; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) xa) v'; x = PTR(user_data_C) xa; ksPSpace s xa = Some k'; (case k' of KOUserData \<Rightarrow> Some UserData | _ \<Rightarrow> None) = Some z; k' = KOUserDataDevice\<rbrakk> \<Longrightarrow> k' = KOUserData
 6. \<And>v' xa z k' x6. \<lbrakk>cslift s' (PTR(user_data_C) xa) = Some v'; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) xa) v'; x = PTR(user_data_C) xa; ksPSpace s xa = Some k'; (case k' of KOUserData \<Rightarrow> Some UserData | _ \<Rightarrow> None) = Some z; k' = KOTCB x6\<rbrakk> \<Longrightarrow> k' = KOUserData
 7. \<And>v' xa z k' x7. \<lbrakk>cslift s' (PTR(user_data_C) xa) = Some v'; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) xa) v'; x = PTR(user_data_C) xa; ksPSpace s xa = Some k'; (case k' of KOUserData \<Rightarrow> Some UserData | _ \<Rightarrow> None) = Some z; k' = KOCTE x7\<rbrakk> \<Longrightarrow> k' = KOUserData
 8. \<And>v' xa z k' x8. \<lbrakk>cslift s' (PTR(user_data_C) xa) = Some v'; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) xa) v'; x = PTR(user_data_C) xa; ksPSpace s xa = Some k'; (case k' of KOUserData \<Rightarrow> Some UserData | _ \<Rightarrow> None) = Some z; k' = KOArch x8\<rbrakk> \<Longrightarrow> k' = KOUserData proof (prove)
goal:
No subgoals! proof (state)
this:
ksPSpace s (ptr_val x) = Some KOUserData

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

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

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

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

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

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 KOUserData

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

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

goal (1 subgoal):
 1. ptr_span x \<inter> {ptr..+2 ^ bits} = {} proof (prove)
using this:
{ptr_val x..+2 ^ objBitsKO KOUserData} \<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 KOUserData} proof (prove)
goal (1 subgoal):
 1. ptr_span x \<subseteq> {ptr_val x..+2 ^ objBitsKO KOUserData} proof (prove)
goal (1 subgoal):
 1. ptr_span x \<subseteq> {ptr_val x..+2 ^ objBitsKO KOUserData} proof (prove)
goal (1 subgoal):
 1. size_of TYPE(user_data_C) \<le> 2 ^ objBitsKO KOUserData proof (prove)
goal:
No subgoals! proof (state)
this:
ptr_span x \<subseteq> {ptr_val x..+2 ^ objBitsKO KOUserData}

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

goal:
No subgoals!