theory Retype_C

lemma createObject_ex_cte_cap_wp_to:
  "\<lbrace>\<lambda>s. ex_cte_cap_wp_to' P p s \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_aligned' s
    \<and> pspace_distinct' s \<and> (APIType_capBits ty us) < word_bits  \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<rbrace>
    createObject ty ptr us dev
   \<lbrace>\<lambda>rv s. ex_cte_cap_wp_to' P p s \<rbrace>" apply (clarsimp simp:ex_cte_cap_wp_to'_def createObject_def3) apply (rule hoare_pre) apply (wp hoare_vcg_ex_lift) apply wps apply (wp createNewCaps_cte_wp_at') apply clarsimp apply (intro exI conjI) apply assumption apply (rule range_cover_full) apply (clarsimp simp:cte_wp_at_ctes_of) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ex_cte_cap_wp_to' P p s \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> APIType_capBits ty us < word_bits \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> APIType_capBits ty us < word_bits \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrace> do m <- createNewCaps ty ptr (Suc 0) us dev;
return (hd m)
od \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> do m <- createNewCaps ty ptr (Suc 0) us dev;
return (hd m)
od \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace>
 2. \<And>s. (\<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> APIType_capBits ty us < word_bits \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<And>cref. \<lbrace>?P5 cref\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>m a. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' a)) cref a\<rbrace>
 2. \<And>s. (\<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> APIType_capBits ty us < word_bits \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<Longrightarrow> \<exists>x. ?P5 x s proof (prove)
goal (2 subgoals):
 1. \<And>cref prev_s. \<lbrace>?P9 cref prev_s\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' prev_s)) cref\<rbrace>
 2. \<And>s. (\<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> APIType_capBits ty us < word_bits \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<Longrightarrow> \<exists>x. ?P9 x s s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> APIType_capBits ty us < word_bits \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<Longrightarrow> \<exists>x. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) x s \<and> range_cover ptr (?sz16 x s) (APIType_capBits ty us) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz16 x s) s proof (prove)
goal (1 subgoal):
 1. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; pspace_distinct' s; APIType_capBits ty us < word_bits; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> \<exists>x. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) x s \<and> range_cover ptr (?sz16 x s) (APIType_capBits ty us) (Suc 0) \<and> pspace_no_overlap' ptr (?sz16 x s) s proof (prove)
goal (3 subgoals):
 1. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; pspace_distinct' s; APIType_capBits ty us < word_bits; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) (?x24 s cref) s
 2. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; pspace_distinct' s; APIType_capBits ty us < word_bits; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz16 (?x24 s cref) s) (APIType_capBits ty us) (Suc 0)
 3. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; pspace_distinct' s; APIType_capBits ty us < word_bits; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (?sz16 (?x24 s cref) s) s proof (prove)
goal (2 subgoals):
 1. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; pspace_distinct' s; APIType_capBits ty us < word_bits; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz16 cref s) (APIType_capBits ty us) (Suc 0)
 2. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; pspace_distinct' s; APIType_capBits ty us < word_bits; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (?sz16 cref s) s proof (prove)
goal (3 subgoals):
 1. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; pspace_distinct' s; APIType_capBits ty us < word_bits; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> is_aligned ptr (APIType_capBits ty us)
 2. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; pspace_distinct' s; APIType_capBits ty us < word_bits; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> APIType_capBits ty us < word_bits
 3. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; pspace_distinct' s; APIType_capBits ty us < word_bits; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (APIType_capBits ty us) s proof (prove)
goal (2 subgoals):
 1. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; pspace_distinct' s; APIType_capBits ty us < word_bits; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> APIType_capBits ty us < word_bits
 2. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; pspace_distinct' s; APIType_capBits ty us < word_bits; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (APIType_capBits ty us) s proof (prove)
goal (1 subgoal):
 1. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; pspace_distinct' s; APIType_capBits ty us < word_bits; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (APIType_capBits ty us) s proof (prove)
goal:
No subgoals!