theory Untyped_R

lemma whenE_reset_resetUntypedCap_invs_etc:
  "\<lbrace>invs' and valid_untyped_inv_wcap' ui
      (Some (UntypedCap dev ptr sz idx))
         and ct_active'
         and K (\<exists>ptr_base ty us slots. ui = Retype slot reset ptr_base ptr' ty us slots dev)\<rbrace>
    whenE reset (resetUntypedCap slot)
  \<lbrace>\<lambda>_. invs' and valid_untyped_inv_wcap' ui (Some (UntypedCap dev ptr sz (if reset then 0 else idx)))
      and ct_active'
      and pspace_no_overlap' (if reset then ptr else ptr') sz\<rbrace>, \<lbrace>\<lambda>_. invs'\<rbrace>" apply (rule hoare_pre) apply (wp whenE_wp resetUntypedCap_invs_etc[where idx=idx,
           simplified pred_conj_def conj_assoc]
       | simp)+ apply (clarsimp simp: cte_wp_at_ctes_of) apply (frule cte_wp_at_valid_objs_valid_cap'[OF ctes_of_cte_wpD], clarsimp+) apply (clarsimp simp: valid_cap_simps' capAligned_def) apply (drule_tac cref=slot in cte_wp_at_pspace_no_overlapI',
    simp add: cte_wp_at_ctes_of, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap dev ptr sz idx)) and ct_active' and K (\<exists>ptr_base ty us slots. ui = Invocations_H.untyped_invocation.Retype slot reset ptr_base ptr' ty us slots dev)\<rbrace> whenE reset (resetUntypedCap slot) \<lbrace>\<lambda>_. invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap dev ptr sz (if reset then 0 else idx))) and ct_active' and pspace_no_overlap' (if reset then ptr else ptr') sz\<rbrace>, \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> whenE reset (resetUntypedCap slot) \<lbrace>\<lambda>_. invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap dev ptr sz (if reset then 0 else idx))) and ct_active' and pspace_no_overlap' (if reset then ptr else ptr') sz\<rbrace>, \<lbrace>\<lambda>_. invs'\<rbrace>
 2. \<And>s. (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap dev ptr sz idx)) and ct_active' and K (\<exists>ptr_base ty us slots. ui = Invocations_H.untyped_invocation.Retype slot reset ptr_base ptr' ty us slots dev)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> valid_untyped_inv_wcap' ui (Some (capability.UntypedCap dev ptr sz idx)) s \<and> ct_active' s \<and> (\<exists>ptr_base ty us slots. ui = Invocations_H.untyped_invocation.Retype slot reset ptr_base ptr' ty us slots dev) \<Longrightarrow> (reset \<longrightarrow> (\<exists>ptr_base ptr' ty us slots. ui = Invocations_H.untyped_invocation.Retype slot True ptr_base ptr' ty us slots dev)) \<and> (\<not> reset \<longrightarrow> pspace_no_overlap' ptr' sz s) proof (prove)
goal (1 subgoal):
 1. \<And>s ty us slots cte. \<lbrakk>invs' s; ct_active' s; ui = Invocations_H.untyped_invocation.Retype slot False (ptr' && ~~ mask sz) ptr' ty us slots dev; range_cover ptr' sz (APIType_capBits ty us) (length slots); ctes_of s slot = Some cte; idx \<le> unat (ptr' && mask sz); cteCap cte = capability.UntypedCap dev (ptr' && ~~ mask sz) sz idx; ptr = ptr' && ~~ mask sz; slot \<notin> set slots; distinct slots; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; \<forall>slot\<in>set slots. \<exists>cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.NullCap; \<forall>slot\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) slot s; sch_act_simple s; slots \<noteq> []; dev \<longrightarrow> ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType ty; APIType_capBits ty us \<le> maxUntypedSizeBits; \<not> reset\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr' sz s proof (prove)
goal (1 subgoal):
 1. \<And>s ty us slots cte. \<lbrakk>invs' s; ct_active' s; ui = Invocations_H.untyped_invocation.Retype slot False (ptr' && ~~ mask sz) ptr' ty us slots dev; range_cover ptr' sz (APIType_capBits ty us) (length slots); ctes_of s slot = Some cte; idx \<le> unat (ptr' && mask sz); cteCap cte = capability.UntypedCap dev (ptr' && ~~ mask sz) sz idx; ptr = ptr' && ~~ mask sz; slot \<notin> set slots; distinct slots; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; \<forall>slot\<in>set slots. \<exists>cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.NullCap; \<forall>slot\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) slot s; sch_act_simple s; slots \<noteq> []; dev \<longrightarrow> ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType ty; APIType_capBits ty us \<le> maxUntypedSizeBits; \<not> reset; valid_cap' (capability.UntypedCap dev (ptr' && ~~ mask sz) sz idx) s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr' sz s proof (prove)
goal (1 subgoal):
 1. \<And>s ty us slots cte. \<lbrakk>invs' s; ct_active' s; ui = Invocations_H.untyped_invocation.Retype slot False (ptr' && ~~ mask sz) ptr' ty us slots dev; range_cover ptr' sz (APIType_capBits ty us) (length slots); ctes_of s slot = Some cte; idx \<le> unat (ptr' && mask sz); cteCap cte = capability.UntypedCap dev (ptr' && ~~ mask sz) sz idx; ptr = ptr' && ~~ mask sz; slot \<notin> set slots; distinct slots; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; \<forall>slot\<in>set slots. \<exists>cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.NullCap; \<forall>slot\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) slot s; sch_act_simple s; slots \<noteq> []; dev \<longrightarrow> ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType ty; APIType_capBits ty us \<le> maxUntypedSizeBits; \<not> reset; sz < word_bits; valid_untyped' dev (ptr' && ~~ mask sz) sz idx s; ptr' && ~~ mask sz \<noteq> 0; minUntypedSizeBits \<le> sz; sz \<le> maxUntypedSizeBits; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) minUntypedSizeBits\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr' sz s proof (prove)
goal:
No subgoals!