theory Retype_R

lemma createNewCaps_valid_queues:
  "\<lbrace>valid_queues and pspace_no_overlap' ptr sz
       and pspace_aligned' and pspace_distinct'
       and K (range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0)\<rbrace>
     createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv. valid_queues\<rbrace>" apply (rule hoare_gen_asm) apply (wp valid_queues_lift_asm createNewCaps_obj_at2[where sz=sz]) apply (clarsimp simp: projectKO_opts_defs) apply (simp add: inQ_def) apply (wp createNewCaps_pred_tcb_at'[where sz=sz] | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and K (range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>Invariants_H.valid_queues and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>da p tcb s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0; (obj_at' (inQ da p) tcb and ?Q3) s\<rbrakk> \<Longrightarrow> obj_at' (inQ da p) tcb s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> ((\<exists>pde_x obj. projectKO_opt (KOArch (KOPDE pde_x)) = Some obj \<and> inQ da p obj) \<longrightarrow> (\<forall>pde_y. \<exists>obj. projectKO_opt (KOArch (KOPDE pde_y)) = Some obj \<and> inQ da p obj)) \<and> (\<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> (\<exists>obj. projectKO_opt (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = Some obj \<and> inQ da p obj) = (\<exists>obj. projectKO_opt (KOTCB tcb_x) = Some obj \<and> inQ da p obj)) \<and> (\<forall>v. makeObjectKO d (Inr ty) = Some v \<longrightarrow> (\<exists>obj. projectKO_opt v = Some obj \<and> inQ da p obj) \<longrightarrow> True)
 2. \<And>tcb. range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>st_tcb_at' runnable' tcb and ?Q3\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. st_tcb_at' runnable' tcb\<rbrace>
 3. \<And>P. range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace>
 4. \<And>P. range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. P (ksReadyQueuesL1Bitmap s)\<rbrace>
 5. \<And>P. range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. P (ksReadyQueuesL2Bitmap s)\<rbrace>
 6. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0; (Invariants_H.valid_queues and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and ?Q3) s proof (prove)
goal (6 subgoals):
 1. \<And>d p tcb s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n; 0 < n; obj_at' (inQ d p) tcb s; ?Q3 s\<rbrakk> \<Longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>da tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> inQ d p (tcbDomain_update (\<lambda>_. da) tcb_x) = inQ d p tcb_x)
 2. \<And>tcb. range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>st_tcb_at' runnable' tcb and ?Q3\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. st_tcb_at' runnable' tcb\<rbrace>
 3. \<And>P. range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace>
 4. \<And>P. range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. P (ksReadyQueuesL1Bitmap s)\<rbrace>
 5. \<And>P. range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. P (ksReadyQueuesL2Bitmap s)\<rbrace>
 6. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0; (Invariants_H.valid_queues and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and ?Q3) s proof (prove)
goal (5 subgoals):
 1. \<And>tcb. range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>st_tcb_at' runnable' tcb and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. st_tcb_at' runnable' tcb\<rbrace>
 2. \<And>P. range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace>
 3. \<And>P. range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. P (ksReadyQueuesL1Bitmap s)\<rbrace>
 4. \<And>P. range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. P (ksReadyQueuesL2Bitmap s)\<rbrace>
 5. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0; (Invariants_H.valid_queues and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s)) s proof (prove)
goal:
No subgoals!