theory Retype_R

lemma createNewCaps_obj_at'':
  "\<lbrace>\<lambda>s. obj_at' (P :: ('a :: pspace_storable) \<Rightarrow> bool) p s
       \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0
       \<and> pspace_aligned' s \<and> pspace_distinct' s
       \<and> pspace_no_overlap' ptr sz s
       \<and> (koType(TYPE('a)) = koType(TYPE(pde))
               \<longrightarrow> (\<forall>x. P x)
                \<and> (\<forall>pde :: pde. \<exists>x :: 'a. injectKO x = injectKO pde))
       \<and> (\<forall>tcb d. \<not>tcbQueued tcb \<and> tcbState tcb = Inactive \<longrightarrow> ((\<exists>obj :: 'a. injectKOS obj = KOTCB (tcb\<lparr>tcbDomain := d\<rparr>) \<and> P obj) \<longleftrightarrow> (\<exists>obj :: 'a. injectKOS obj = KOTCB tcb \<and> P obj)))\<rbrace>
     createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv s. obj_at' P p s\<rbrace>" apply (simp add: obj_at'_real_def) apply (wp createNewCaps_ko_wp_at') apply clarsimp apply (intro conjI impI) apply simp+ apply clarsimp apply (clarsimp simp: projectKOs dest!: iffD1 [OF project_koType, OF exI]) apply (clarsimp simp:project_inject)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' P p s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (koType TYPE('a) = koType TYPE(ARM_H.pde) \<longrightarrow> (\<forall>x. P x) \<and> (\<forall>pde. \<exists>x. injectKOS x = injectKOS pde)) \<and> (\<forall>tcb d. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> P obj) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> P obj))\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. obj_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p 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> (koType TYPE('a) = ArchT PDET \<longrightarrow> (\<forall>x. P x) \<and> (\<forall>pde. \<exists>x. injectKOS x = KOArch (KOPDE pde))) \<and> (\<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> P obj) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> P obj)))\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p 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> (koType TYPE('a) = ArchT PDET \<longrightarrow> (\<forall>x. P x) \<and> (\<forall>pde. \<exists>x. injectKOS x = KOArch (KOPDE pde))) \<and> (\<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> P obj) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> P obj))) \<Longrightarrow> ((\<lambda>s. ko_wp_at' (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> P obj) p s \<and> range_cover ptr ?sz4 (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz4 s) and K ((\<exists>pde_x obj. projectKO_opt (KOArch (KOPDE pde_x)) = Some obj \<and> P obj) \<longrightarrow> (\<forall>pde_y. \<exists>obj. projectKO_opt (KOArch (KOPDE pde_y)) = Some obj \<and> P obj)) and K (\<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> P obj) = (\<exists>obj. projectKO_opt (KOTCB tcb_x) = Some obj \<and> P obj)) and K (\<forall>v. makeObjectKO d (Inr ty) = Some v \<longrightarrow> (\<exists>obj. projectKO_opt v = Some obj \<and> P obj) \<longrightarrow> True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; koType TYPE('a) = ArchT PDET \<longrightarrow> (\<forall>x. P x) \<and> (\<forall>pde. \<exists>x. injectKOS x = KOArch (KOPDE pde)); \<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> P obj) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> P obj))\<rbrakk> \<Longrightarrow> range_cover ptr ?sz4 (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr ?sz4 s \<and> ((\<exists>pde_x obj. projectKO_opt (KOArch (KOPDE pde_x)) = Some obj \<and> P obj) \<longrightarrow> (\<forall>pde_y. \<exists>obj. projectKO_opt (KOArch (KOPDE pde_y)) = Some obj \<and> 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> P obj) = (\<exists>obj. projectKO_opt (KOTCB tcb_x) = Some obj \<and> P obj)) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; koType TYPE('a) = ArchT PDET \<longrightarrow> (\<forall>x. P x) \<and> (\<forall>pde. \<exists>x. injectKOS x = KOArch (KOPDE pde)); \<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> P obj) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> P obj))\<rbrakk> \<Longrightarrow> range_cover ptr ?sz4 (APIType_capBits ty us) n
 2. \<And>s. \<lbrakk>ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; koType TYPE('a) = ArchT PDET \<longrightarrow> (\<forall>x. P x) \<and> (\<forall>pde. \<exists>x. injectKOS x = KOArch (KOPDE pde)); \<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> P obj) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> P obj))\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr ?sz4 s
 3. \<And>s. \<lbrakk>ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; koType TYPE('a) = ArchT PDET \<longrightarrow> (\<forall>x. P x) \<and> (\<forall>pde. \<exists>x. injectKOS x = KOArch (KOPDE pde)); \<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> P obj) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> P obj)); \<exists>pde_x obj. projectKO_opt (KOArch (KOPDE pde_x)) = Some obj \<and> P obj\<rbrakk> \<Longrightarrow> \<forall>pde_y. \<exists>obj. projectKO_opt (KOArch (KOPDE pde_y)) = Some obj \<and> P obj
 4. \<And>s. \<lbrakk>ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; koType TYPE('a) = ArchT PDET \<longrightarrow> (\<forall>x. P x) \<and> (\<forall>pde. \<exists>x. injectKOS x = KOArch (KOPDE pde)); \<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> P obj) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> P obj))\<rbrakk> \<Longrightarrow> \<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> P obj) = (\<exists>obj. projectKO_opt (KOTCB tcb_x) = Some obj \<and> P obj) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; koType TYPE('a) = ArchT PDET \<longrightarrow> (\<forall>x. P x) \<and> (\<forall>pde. \<exists>x. injectKOS x = KOArch (KOPDE pde)); \<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> P obj) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> P obj)); \<exists>pde_x obj. projectKO_opt (KOArch (KOPDE pde_x)) = Some obj \<and> P obj\<rbrakk> \<Longrightarrow> \<forall>pde_y. \<exists>obj. projectKO_opt (KOArch (KOPDE pde_y)) = Some obj \<and> P obj
 2. \<And>s. \<lbrakk>ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; koType TYPE('a) = ArchT PDET \<longrightarrow> (\<forall>x. P x) \<and> (\<forall>pde. \<exists>x. injectKOS x = KOArch (KOPDE pde)); \<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> P obj) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> P obj))\<rbrakk> \<Longrightarrow> \<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> P obj) = (\<exists>obj. projectKO_opt (KOTCB tcb_x) = Some obj \<and> P obj) proof (prove)
goal (2 subgoals):
 1. \<And>s pde_x obj pde_y. \<lbrakk>ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; koType TYPE('a) = ArchT PDET \<longrightarrow> (\<forall>x. P x) \<and> (\<forall>pde. \<exists>x. injectKOS x = KOArch (KOPDE pde)); \<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> P obj) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> P obj)); projectKO_opt (KOArch (KOPDE pde_x)) = Some obj; P obj\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt (KOArch (KOPDE pde_y)) = Some obj \<and> P obj
 2. \<And>s. \<lbrakk>ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; koType TYPE('a) = ArchT PDET \<longrightarrow> (\<forall>x. P x) \<and> (\<forall>pde. \<exists>x. injectKOS x = KOArch (KOPDE pde)); \<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> P obj) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> P obj))\<rbrakk> \<Longrightarrow> \<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> P obj) = (\<exists>obj. projectKO_opt (KOTCB tcb_x) = Some obj \<and> P obj) proof (prove)
goal (2 subgoals):
 1. \<And>s pde_y. \<lbrakk>ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) p s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; \<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb)) = (\<exists>obj. injectKOS obj = KOTCB tcb)); ArchT PDET = koType TYPE('a); All P; \<forall>pde. \<exists>x. injectKOS x = KOArch (KOPDE pde)\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt (KOArch (KOPDE pde_y)) = Some obj
 2. \<And>s. \<lbrakk>ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; koType TYPE('a) = ArchT PDET \<longrightarrow> (\<forall>x. P x) \<and> (\<forall>pde. \<exists>x. injectKOS x = KOArch (KOPDE pde)); \<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> P obj) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> P obj))\<rbrakk> \<Longrightarrow> \<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> P obj) = (\<exists>obj. projectKO_opt (KOTCB tcb_x) = Some obj \<and> P obj) proof (prove)
goal:
No subgoals!