theory Retype_R

lemma createObjects_queues:
  "\<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 (wp valid_queues_lift_asm [unfolded pred_conj_def, OF createObjects_orig_obj_at3]
            createObjects_pred_tcb_at' [unfolded pred_conj_def]) apply fastforce apply wp+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Invariants_H.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. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>tcb s. st_tcb_at' runnable' tcb s \<and> range_cover ptr ?sz10 (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz10 s \<Longrightarrow> (((st_tcb_at' runnable' tcb s \<and> K (range_cover ptr (?sz16 tcb) (objBitsKO val + gbits) n \<and> n \<noteq> 0) s) \<and> pspace_aligned' s) \<and> pspace_distinct' s) \<and> pspace_no_overlap' ptr (?sz16 tcb) s
 2. \<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. P (ksReadyQueuesL1Bitmap s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. P (ksReadyQueuesL2Bitmap s)\<rbrace>
 5. \<And>s. Invariants_H.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 \<Longrightarrow> Invariants_H.valid_queues s \<and> range_cover ptr ?sz10 (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz10 s proof (prove)
goal (4 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. P (ksReadyQueuesL1Bitmap s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. P (ksReadyQueuesL2Bitmap s)\<rbrace>
 4. \<And>s. Invariants_H.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 \<Longrightarrow> Invariants_H.valid_queues s \<and> range_cover ptr ?sz10 (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz10 s proof (prove)
goal (1 subgoal):
 1. \<And>s. Invariants_H.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 \<Longrightarrow> Invariants_H.valid_queues s \<and> range_cover ptr ?sz10 (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz10 s proof (prove)
goal:
No subgoals!