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 (wp valid_queues_lift_asm' [OF createNewCaps_obj_at2]) apply (clarsimp simp: projectKOs) apply (simp add: makeObjectKO_def
            split: object_type.split_asm
                   apiobject_type.split_asm) apply (clarsimp simp: inQ_def) apply (auto simp: makeObject_tcb
             split: object_type.splits apiobject_type.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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> proof (prove)
goal (1 subgoal):
 1. \<And>s. (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)) s \<Longrightarrow> valid_queues' s \<and> (\<forall>da p. range_cover ptr (?sz37 da p) (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz37 da p) 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> \<not> True)) proof (prove)
goal (1 subgoal):
 1. \<And>s da p. \<lbrakk>valid_queues' s; pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n\<rbrakk> \<Longrightarrow> range_cover ptr (?sz37 da p) (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr (?sz37 da p) s \<and> (\<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> inQ da p (tcbDomain_update (\<lambda>_. d) tcb_x) = inQ da p tcb_x) \<and> (\<forall>v. makeObjectKO d (Inr ty) = Some v \<longrightarrow> (\<forall>obj. v = KOTCB obj \<longrightarrow> \<not> inQ da p obj)) proof (prove)
goal (1 subgoal):
 1. \<And>s da p. \<lbrakk>valid_queues' s; pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n\<rbrakk> \<Longrightarrow> (d \<longrightarrow> range_cover ptr (?sz37 da p) (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr (?sz37 da p) s \<and> (\<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> inQ da p (tcbDomain_update (\<lambda>_. d) tcb_x) = inQ da p tcb_x) \<and> (\<forall>v. (case ty of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> None | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Some (KOTCB makeObject) | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Some (KOEndpoint makeObject) | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Some (KONotification makeObject) | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Some (KOCTE makeObject) | PageTableObject \<Rightarrow> Some (KOArch (KOPTE makeObject)) | PageDirectoryObject \<Rightarrow> Some (KOArch (KOPDE makeObject)) | _ \<Rightarrow> Some KOUserDataDevice) = Some v \<longrightarrow> (\<forall>obj. v = KOTCB obj \<longrightarrow> \<not> inQ da p obj))) \<and> (\<not> d \<longrightarrow> range_cover ptr (?sz37 da p) (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr (?sz37 da p) s \<and> (\<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> inQ da p (tcbDomain_update (\<lambda>_. d) tcb_x) = inQ da p tcb_x) \<and> (\<forall>v. (case ty of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> None | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Some (KOTCB makeObject) | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Some (KOEndpoint makeObject) | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Some (KONotification makeObject) | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Some (KOCTE makeObject) | PageTableObject \<Rightarrow> Some (KOArch (KOPTE makeObject)) | PageDirectoryObject \<Rightarrow> Some (KOArch (KOPDE makeObject)) | _ \<Rightarrow> Some KOUserData) = Some v \<longrightarrow> (\<forall>obj. v = KOTCB obj \<longrightarrow> \<not> inQ da p obj))) proof (prove)
goal (1 subgoal):
 1. \<And>s da p. \<lbrakk>valid_queues' s; pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n\<rbrakk> \<Longrightarrow> (d \<longrightarrow> range_cover ptr (?sz37 da p) (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr (?sz37 da p) s \<and> (\<forall>v. (case ty of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> None | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Some (KOTCB makeObject) | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Some (KOEndpoint makeObject) | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Some (KONotification makeObject) | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Some (KOCTE makeObject) | PageTableObject \<Rightarrow> Some (KOArch (KOPTE makeObject)) | PageDirectoryObject \<Rightarrow> Some (KOArch (KOPDE makeObject)) | _ \<Rightarrow> Some KOUserDataDevice) = Some v \<longrightarrow> (\<forall>obj. v = KOTCB obj \<longrightarrow> tcbPriority obj = p \<longrightarrow> tcbQueued obj \<longrightarrow> tcbDomain obj \<noteq> da))) \<and> (\<not> d \<longrightarrow> range_cover ptr (?sz37 da p) (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr (?sz37 da p) s \<and> (\<forall>v. (case ty of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> None | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> Some (KOTCB makeObject) | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> Some (KOEndpoint makeObject) | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> Some (KONotification makeObject) | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> Some (KOCTE makeObject) | PageTableObject \<Rightarrow> Some (KOArch (KOPTE makeObject)) | PageDirectoryObject \<Rightarrow> Some (KOArch (KOPDE makeObject)) | _ \<Rightarrow> Some KOUserData) = Some v \<longrightarrow> (\<forall>obj. v = KOTCB obj \<longrightarrow> tcbPriority obj = p \<longrightarrow> tcbQueued obj \<longrightarrow> tcbDomain obj \<noteq> da))) proof (prove)
goal:
No subgoals!