theory Retype_R

lemma createNewCaps_ifunsafe':
  "\<lbrace>\<lambda>s. valid_pspace' s \<and>
        pspace_no_overlap' ptr sz s \<and>
        range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and>
        if_unsafe_then_cap' s\<rbrace>
      createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv s. if_unsafe_then_cap' s\<rbrace>" apply (simp only: if_unsafe_then_cap'_def ex_cte_cap_to'_def
                    imp_conv_disj) apply (rule hoare_pre) apply (rule hoare_use_eq_irq_node' [OF createNewCaps_ksInterrupt]) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift
             createNewCaps_cte_wp_at2 hoare_vcg_ex_lift) apply (simp add: makeObject_cte pspace_no_overlap'_def
                   valid_pspace'_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> if_unsafe_then_cap' s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> (\<forall>cref. \<not> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<or> (\<exists>crefa. cte_wp_at' (\<lambda>c. True \<and> cref \<in> cte_refs' (cteCap c) (irq_node' s)) crefa s))\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<forall>cref. \<not> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<or> (\<exists>crefa. cte_wp_at' (\<lambda>c. True \<and> cref \<in> cte_refs' (cteCap c) (irq_node' s)) crefa s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<forall>cref. \<not> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<or> (\<exists>crefa. cte_wp_at' (\<lambda>c. True \<and> cref \<in> cte_refs' (cteCap c) (irq_node' s)) crefa s)\<rbrace>
 2. \<And>s. valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> (\<forall>cref. \<not> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<or> (\<exists>crefa. cte_wp_at' (\<lambda>c. True \<and> cref \<in> cte_refs' (cteCap c) (irq_node' s)) crefa s)) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<forall>cref. \<not> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<or> (\<exists>crefa. cte_wp_at' (\<lambda>c. True \<and> cref \<in> cte_refs' (cteCap c) f) crefa s)\<rbrace>
 2. \<And>s. valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> (\<forall>cref. \<not> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<or> (\<exists>crefa. cte_wp_at' (\<lambda>c. True \<and> cref \<in> cte_refs' (cteCap c) (irq_node' s)) crefa s)) \<Longrightarrow> ?P3 (irq_node' s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> (\<forall>cref. \<not> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<or> (\<exists>crefa. cte_wp_at' (\<lambda>c. True \<and> cref \<in> cte_refs' (cteCap c) (irq_node' s)) crefa s)) \<Longrightarrow> \<forall>x. \<not> cte_wp_at' (\<lambda>a. cteCap a \<noteq> capability.NullCap) x s \<and> \<not> cteCap makeObject \<noteq> capability.NullCap \<and> n \<noteq> 0 \<and> range_cover ptr (?sz25 (irq_node' s) x) (APIType_capBits ty us) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz25 (irq_node' s) x) s \<or> (\<exists>xa. cte_wp_at' (\<lambda>a. True \<and> x \<in> cte_refs' (cteCap a) (irq_node' s)) xa s \<and> \<not> (True \<and> x \<in> cte_refs' (cteCap makeObject) (irq_node' s)) \<and> n \<noteq> 0 \<and> range_cover ptr (?sz27 (irq_node' s) x xa) (APIType_capBits ty us) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz27 (irq_node' s) x xa) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> (\<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> x \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) \<longrightarrow> ptr \<le> x + 2 ^ objBitsKO ko - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO ko - 1 \<longrightarrow> \<not> ptr \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)) \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> (\<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> (\<exists>crefa. cte_wp_at' (\<lambda>c. cref \<in> cte_refs' (cteCap c) (irq_node' s)) crefa s)) \<Longrightarrow> \<forall>x. \<not> cte_wp_at' (\<lambda>a. cteCap a \<noteq> capability.NullCap) x s \<and> range_cover ptr (?sz25 (irq_node' s) x) (APIType_capBits ty us) n \<and> (\<forall>xa ko. ksPSpace s xa = Some ko \<longrightarrow> xa \<le> (ptr && ~~ mask (?sz25 (irq_node' s) x)) + (2 ^ ?sz25 (irq_node' s) x - 1) \<longrightarrow> ptr \<le> xa + 2 ^ objBitsKO ko - 1 \<longrightarrow> xa \<le> xa + 2 ^ objBitsKO ko - 1 \<longrightarrow> \<not> ptr \<le> (ptr && ~~ mask (?sz25 (irq_node' s) x)) + (2 ^ ?sz25 (irq_node' s) x - 1)) \<or> (\<exists>xa. cte_wp_at' (\<lambda>a. x \<in> cte_refs' (cteCap a) (irq_node' s)) xa s \<and> range_cover ptr (?sz27 (irq_node' s) x xa) (APIType_capBits ty us) n \<and> (\<forall>xb ko. ksPSpace s xb = Some ko \<longrightarrow> xb \<le> (ptr && ~~ mask (?sz27 (irq_node' s) x xa)) + (2 ^ ?sz27 (irq_node' s) x xa - 1) \<longrightarrow> ptr \<le> xb + 2 ^ objBitsKO ko - 1 \<longrightarrow> xb \<le> xb + 2 ^ objBitsKO ko - 1 \<longrightarrow> \<not> ptr \<le> (ptr && ~~ mask (?sz27 (irq_node' s) x xa)) + (2 ^ ?sz27 (irq_node' s) x xa - 1))) proof (prove)
goal:
No subgoals!