theory Retype_R

lemma createObjects_no_cte_ifunsafe':
  assumes no_cte: "\<And>c. projectKO_opt val \<noteq> Some (c::cte)"
  assumes no_tcb: "\<And>t. projectKO_opt val \<noteq> Some (t::tcb)"
  shows
  "\<lbrace>\<lambda>s. valid_pspace' s \<and>
       pspace_no_overlap' ptr sz s \<and>
       range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and>
       if_unsafe_then_cap' s\<rbrace>
      createObjects ptr n val gbits
   \<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 createObjects_ksInterrupt]) apply (simp add: createObjects_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift hoare_vcg_imp_lift
             createObjects_orig_cte_wp_at2' hoare_vcg_ex_lift) apply (simp add: valid_pspace'_def disj_imp) apply (simp add: split_def no_cte no_tcb split: option.splits) 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 (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> if_unsafe_then_cap' s\<rbrace> createObjects ptr n val gbits \<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 (objBitsKO val + gbits) 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> createObjects ptr n val gbits \<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> createObjects ptr n val gbits \<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 (objBitsKO val + gbits) 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> createObjects ptr n val gbits \<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 (objBitsKO val + gbits) 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 (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<rbrace> do y <- createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>rv s. \<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) f) crefa s)\<rbrace>
 2. \<And>s. valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) 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 (objBitsKO val + gbits) 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> n \<noteq> 0 \<and> range_cover ptr (?sz24 (irq_node' s) x) (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some a \<Rightarrow> cteCap a \<noteq> capability.NullCap) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x \<Rightarrow> ((\<lambda>a. cteCap a \<noteq> capability.NullCap) \<circ> getF) x)) \<and> pspace_no_overlap' ptr (?sz24 (irq_node' s) x) s \<or> (\<exists>xa. cte_wp_at' (\<lambda>a. x \<in> cte_refs' (cteCap a) (irq_node' s)) xa s \<and> n \<noteq> 0 \<and> range_cover ptr (?sz28 (irq_node' s) x xa) (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some a \<Rightarrow> x \<in> cte_refs' (cteCap a) (irq_node' s)) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some xa \<Rightarrow> ((\<lambda>a. x \<in> cte_refs' (cteCap a) (irq_node' s)) \<circ> getF) xa)) \<and> pspace_no_overlap' ptr (?sz28 (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> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) 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 \<longrightarrow> range_cover ptr (?sz24 (irq_node' s) x) (objBitsKO val + gbits) n \<longrightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some a \<Rightarrow> cteCap a \<noteq> capability.NullCap) \<longrightarrow> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> cteCap (getF x2) \<noteq> capability.NullCap)) \<longrightarrow> \<not> pspace_no_overlap' ptr (?sz24 (irq_node' s) x) s) \<longrightarrow> (\<exists>xa. cte_wp_at' (\<lambda>a. x \<in> cte_refs' (cteCap a) (irq_node' s)) xa s \<and> range_cover ptr (?sz28 (irq_node' s) x xa) (objBitsKO val + gbits) n \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some a \<Rightarrow> x \<in> cte_refs' (cteCap a) (irq_node' s)) \<and> (\<forall>xa\<in>ran tcb_cte_cases. case xa of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> x \<in> cte_refs' (cteCap (getF x2)) (irq_node' s))) \<and> pspace_no_overlap' ptr (?sz28 (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> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) 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> projectKO_opt val = None \<longrightarrow> (\<forall>x. (\<not> cte_wp_at' (\<lambda>a. cteCap a \<noteq> capability.NullCap) x s \<longrightarrow> range_cover ptr (?sz24 (irq_node' s) x) (objBitsKO val + gbits) n \<longrightarrow> \<not> pspace_no_overlap' ptr (?sz24 (irq_node' s) x) s) \<longrightarrow> (\<exists>xa. cte_wp_at' (\<lambda>a. x \<in> cte_refs' (cteCap a) (irq_node' s)) xa s \<and> range_cover ptr (?sz28 (irq_node' s) x xa) (objBitsKO val + gbits) n \<and> pspace_no_overlap' ptr (?sz28 (irq_node' s) x xa) s)) proof (prove)
goal:
No subgoals!