theory Orphanage

lemma invokeUntyped_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> valid_untyped_inv' ui s \<and> ct_active' s \<rbrace>
   invokeUntyped ui
   \<lbrace> \<lambda>reply s. no_orphans s \<rbrace>" apply (rule hoare_pre, rule hoare_strengthen_post) apply (rule invokeUntyped_invs''[where Q=no_orphans]) apply (wp createNewCaps_no_orphans)+ apply (clarsimp simp: valid_pspace'_def) apply (intro conjI, simp_all)[1] apply (wp | simp)+ apply (cases ui, auto simp: cte_wp_at_ctes_of)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_untyped_inv' ui s \<and> ct_active' s\<rbrace> invokeUntyped ui \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> invokeUntyped ui \<lbrace>?Q3\<rbrace>
 2. \<And>rv s. ?Q3 rv s \<Longrightarrow> no_orphans s
 3. \<And>s. no_orphans s \<and> invs' s \<and> valid_untyped_inv' ui s \<and> ct_active' s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>p cref cap. \<lbrace>no_orphans\<rbrace> insertNewCap p cref cap \<lbrace>\<lambda>_. no_orphans\<rbrace>
 2. \<And>tp ptr n us sz dev. \<lbrace>\<lambda>s. no_orphans s \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> 0 < n \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s\<rbrace> createNewCaps tp ptr n us dev \<lbrace>\<lambda>_. no_orphans\<rbrace>
 3. \<And>slot idx. \<lbrace>invs' and no_orphans\<rbrace> updateFreeIndex slot idx \<lbrace>\<lambda>_. no_orphans\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> resetUntypedCap (case ui of Invocations_H.untyped_invocation.Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. no_orphans\<rbrace>
 5. \<And>rv s. (invs' and no_orphans) s \<Longrightarrow> no_orphans s
 6. \<And>s. no_orphans s \<and> invs' s \<and> valid_untyped_inv' ui s \<and> ct_active' s \<Longrightarrow> (invs' and valid_untyped_inv' ui and (\<lambda>s. (case ui of Invocations_H.untyped_invocation.Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'6 s) and no_orphans and ct_active') s proof (prove)
goal (5 subgoals):
 1. \<And>tp ptr n us sz dev s. no_orphans s \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> 0 < n \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ((\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz17 tp ptr n us sz dev) s \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)) and K (range_cover ptr (?sz17 tp ptr n us sz dev) (APIType_capBits tp us) n \<and> 0 < n)) s
 2. \<And>slot idx. \<lbrace>invs' and no_orphans\<rbrace> updateFreeIndex slot idx \<lbrace>\<lambda>_. no_orphans\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> resetUntypedCap (case ui of Invocations_H.untyped_invocation.Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. no_orphans\<rbrace>
 4. \<And>rv s. (invs' and no_orphans) s \<Longrightarrow> no_orphans s
 5. \<And>s. no_orphans s \<and> invs' s \<and> valid_untyped_inv' ui s \<and> ct_active' s \<Longrightarrow> (invs' and valid_untyped_inv' ui and (\<lambda>s. (case ui of Invocations_H.untyped_invocation.Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'6 s) and no_orphans and ct_active') s proof (prove)
goal (5 subgoals):
 1. \<And>tp ptr n us sz dev s. \<lbrakk>no_orphans s; range_cover ptr sz (APIType_capBits tp us) n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; 0 < n; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (?sz17 tp ptr n us sz dev) s \<and> range_cover ptr (?sz17 tp ptr n us sz dev) (APIType_capBits tp us) n
 2. \<And>slot idx. \<lbrace>invs' and no_orphans\<rbrace> updateFreeIndex slot idx \<lbrace>\<lambda>_. no_orphans\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> resetUntypedCap (case ui of Invocations_H.untyped_invocation.Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. no_orphans\<rbrace>
 4. \<And>rv s. (invs' and no_orphans) s \<Longrightarrow> no_orphans s
 5. \<And>s. no_orphans s \<and> invs' s \<and> valid_untyped_inv' ui s \<and> ct_active' s \<Longrightarrow> (invs' and valid_untyped_inv' ui and (\<lambda>s. (case ui of Invocations_H.untyped_invocation.Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'6 s) and no_orphans and ct_active') s proof (prove)
goal (4 subgoals):
 1. \<And>slot idx. \<lbrace>invs' and no_orphans\<rbrace> updateFreeIndex slot idx \<lbrace>\<lambda>_. no_orphans\<rbrace>
 2. \<lbrace>?Q'6\<rbrace> resetUntypedCap (case ui of Invocations_H.untyped_invocation.Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. no_orphans\<rbrace>
 3. \<And>rv s. (invs' and no_orphans) s \<Longrightarrow> no_orphans s
 4. \<And>s. no_orphans s \<and> invs' s \<and> valid_untyped_inv' ui s \<and> ct_active' s \<Longrightarrow> (invs' and valid_untyped_inv' ui and (\<lambda>s. (case ui of Invocations_H.untyped_invocation.Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'6 s) and no_orphans and ct_active') s proof (prove)
goal (1 subgoal):
 1. \<And>s. no_orphans s \<and> invs' s \<and> valid_untyped_inv' ui s \<and> ct_active' s \<Longrightarrow> (case ui of Invocations_H.untyped_invocation.Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> pspace_distinct' s \<and> valid_objs' s \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) (case ui of Invocations_H.untyped_invocation.Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) s proof (prove)
goal:
No subgoals!