theory Retype_R

lemma createObjects_idle':
  "\<lbrace>valid_idle' and valid_pspace' and pspace_no_overlap' ptr sz
        and (\<lambda>s. \<not> case_option False (\<lambda>cte. ksIdleThread s \<in> capRange (cteCap cte))
                        (projectKO_opt val)
               \<and> (\<forall>(getF, setF) \<in> ran tcb_cte_cases.
                 \<not> case_option False (\<lambda>tcb. ksIdleThread s \<in> capRange (cteCap (getF tcb)))
                        (projectKO_opt val)))
        and K (range_cover ptr sz (objBitsKO val + gbits) n  \<and> n \<noteq> 0)\<rbrace>
  createObjects' ptr n val gbits
  \<lbrace>\<lambda>rv. valid_idle'\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_pre) apply (clarsimp simp add: valid_idle'_def pred_tcb_at'_def) apply (rule hoare_vcg_conj_lift) apply (rule hoare_as_subst [OF createObjects'_it]) apply (wp createObjects_orig_obj_at'
              createObjects_orig_cte_wp_at2'
              hoare_vcg_all_lift | simp)+ apply (clarsimp simp: valid_idle'_def projectKOs o_def
                        pred_tcb_at'_def valid_pspace'_def
                  cong: option.case_cong) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle' and valid_pspace' and pspace_no_overlap' ptr sz and (\<lambda>s. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some cte \<Rightarrow> ksIdleThread s \<in> capRange (cteCap cte)) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some tcb \<Rightarrow> ksIdleThread s \<in> capRange (cteCap (getF tcb))))) and K (range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0)\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>valid_idle' and valid_pspace' and pspace_no_overlap' ptr sz and (\<lambda>s. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some cte \<Rightarrow> ksIdleThread s \<in> capRange (cteCap cte)) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some tcb \<Rightarrow> ksIdleThread s \<in> capRange (cteCap (getF tcb)))))\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (2 subgoals):
 1. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>?Q2\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv. valid_idle'\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0; (valid_idle' and valid_pspace' and pspace_no_overlap' ptr sz and (\<lambda>s. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some cte \<Rightarrow> ksIdleThread s \<in> capRange (cteCap cte)) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some tcb \<Rightarrow> ksIdleThread s \<in> capRange (cteCap (getF tcb)))))) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv s. obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0; (valid_idle' and valid_pspace' and pspace_no_overlap' ptr sz and (\<lambda>s. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some cte \<Rightarrow> ksIdleThread s \<in> capRange (cteCap cte)) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some tcb \<Rightarrow> ksIdleThread s \<in> capRange (cteCap (getF tcb)))))) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P8\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv s. obj_at' idle_tcb' (ksIdleThread s) s\<rbrace>
 2. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'8\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv s. idle_thread_ptr = ksIdleThread s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0; (valid_idle' and valid_pspace' and pspace_no_overlap' ptr sz and (\<lambda>s. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some cte \<Rightarrow> ksIdleThread s \<in> capRange (cteCap cte)) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some tcb \<Rightarrow> ksIdleThread s \<in> capRange (cteCap (getF tcb)))))) s\<rbrakk> \<Longrightarrow> ?P8 s \<and> ?P'8 s proof (prove)
goal (3 subgoals):
 1. \<And>v. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P11 v\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>a. obj_at' idle_tcb' v\<rbrace>
 2. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'8\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv s. idle_thread_ptr = ksIdleThread s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0; (valid_idle' and valid_pspace' and pspace_no_overlap' ptr sz and (\<lambda>s. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some cte \<Rightarrow> ksIdleThread s \<in> capRange (cteCap cte)) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some tcb \<Rightarrow> ksIdleThread s \<in> capRange (cteCap (getF tcb)))))) s\<rbrakk> \<Longrightarrow> ?P11 (ksIdleThread s) s \<and> ?P'8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n; valid_idle' s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some cte \<Rightarrow> ksIdleThread s \<in> capRange (cteCap cte)) \<and> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some tcb \<Rightarrow> ksIdleThread s \<in> capRange (cteCap (getF tcb))))\<rbrakk> \<Longrightarrow> range_cover ptr (?sz29 (ksIdleThread s)) (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> obj_at' idle_tcb' (ksIdleThread s) s \<and> pspace_no_overlap' ptr (?sz29 (ksIdleThread s)) s \<and> idle_thread_ptr = ksIdleThread s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; pspace_no_overlap' ptr sz s; \<not> (case projectKO_opt val of None \<Rightarrow> False | Some cte \<Rightarrow> idle_thread_ptr \<in> capRange (cteCap cte)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some tcb \<Rightarrow> idle_thread_ptr \<in> capRange (cteCap (getF tcb)))\<rbrakk> \<Longrightarrow> range_cover ptr (?sz29 idle_thread_ptr) (objBitsKO val + gbits) n \<and> pspace_no_overlap' ptr (?sz29 idle_thread_ptr) s proof (prove)
goal:
No subgoals!