theory Retype_R

lemma createObjects_queues':
  assumes no_tcb: "\<And>t. projectKO_opt val \<noteq> Some (t::tcb)"
  shows
  "\<lbrace>\<lambda>s. valid_queues' s \<and>  pspace_aligned' s \<and> pspace_distinct' s \<and>
        pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0\<rbrace>
  createObjects ptr n val gbits
  \<lbrace>\<lambda>rv. valid_queues'\<rbrace>" apply (simp add: createObjects_def) apply (wp valid_queues_lift_asm') apply (wp createObjects_orig_obj_at2') apply clarsimp apply assumption apply wp apply (clarsimp simp: no_tcb split: option.splits) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_queues' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_queues' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n\<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. valid_queues'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>d p t. \<lbrace>\<lambda>s. \<not> obj_at' (inQ d p) t s \<and> ?Q1 d p s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>x a. \<not> obj_at' (inQ d p) t a\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<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. P (ksReadyQueues s)\<rbrace>
 3. \<And>s. valid_queues' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<Longrightarrow> valid_queues' s \<and> (\<forall>d p. ?Q1 d p s) proof (prove)
goal (3 subgoals):
 1. \<And>d p t s. \<not> obj_at' (inQ d p) t s \<and> ?Q1 d p s \<Longrightarrow> n \<noteq> 0 \<and> range_cover ptr (?sz6 d p t) (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> obj_at' (inQ d p) t s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some a \<Rightarrow> inQ d p a) \<and> pspace_no_overlap' ptr (?sz6 d p t) s
 2. \<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<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. P (ksReadyQueues s)\<rbrace>
 3. \<And>s. valid_queues' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<Longrightarrow> valid_queues' s \<and> (\<forall>d p. ?Q1 d p s) proof (prove)
goal (3 subgoals):
 1. \<And>d p t s. \<lbrakk>\<not> obj_at' (inQ d p) t s; ?Q1 d p s\<rbrakk> \<Longrightarrow> 0 < n \<and> range_cover ptr (?sz6 d p t) (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> inQ d p x2) \<and> pspace_no_overlap' ptr (?sz6 d p t) s
 2. \<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<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. P (ksReadyQueues s)\<rbrace>
 3. \<And>s. valid_queues' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<Longrightarrow> valid_queues' s \<and> (\<forall>d p. ?Q1 d p s) proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<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. P (ksReadyQueues s)\<rbrace>
 2. \<And>s. valid_queues' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<Longrightarrow> valid_queues' s \<and> (\<forall>d p. 0 < n \<and> range_cover ptr (?sz13 d p) (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> inQ d p x2) \<and> pspace_no_overlap' ptr (?sz13 d p) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<Longrightarrow> valid_queues' s \<and> (\<forall>d p. 0 < n \<and> range_cover ptr (?sz13 d p) (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> inQ d p x2) \<and> pspace_no_overlap' ptr (?sz13 d p) s) proof (prove)
goal (1 subgoal):
 1. \<And>s d p. \<lbrakk>valid_queues' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; projectKO_opt val = None\<rbrakk> \<Longrightarrow> range_cover ptr (?sz13 d p) (objBitsKO val + gbits) n \<and> pspace_no_overlap' ptr (?sz13 d p) s proof (prove)
goal:
No subgoals!