theory Orphanage

lemma performASIDControlInvocation_no_orphans [wp]:
  notes blah[simp del] =
  atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
  Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex usableUntypedRange.simps
  shows "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> valid_aci' aci s \<and> ct_active' s \<rbrace>
   performASIDControlInvocation aci
   \<lbrace> \<lambda>reply s. no_orphans s \<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp:valid_aci'_def cte_wp_at_ctes_of
    split:asidcontrol_invocation.splits) apply (rename_tac s ptr_base p cref ptr null_cte ut_cte idx) proof - fix s ptr_base p cref ptr null_cte ut_cte idx assume no_orphans: "no_orphans s"
    and  invs'     : "invs' s"
    and  cte       : "ctes_of s p = Some null_cte" "cteCap null_cte = capability.NullCap"
                     "ctes_of s cref = Some ut_cte" "cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx"
    and  desc      : "descendants_of' cref (ctes_of s) = {}"
    and  misc      : "p \<noteq> cref" "ex_cte_cap_wp_to' (\<lambda>_. True) p s" "sch_act_simple s" "is_aligned ptr asid_low_bits"
                     "(ptr :: word32) < 2 ^ asid_bits" "ct_active' s" have vc:"s \<turnstile>' UntypedCap False ptr_base pageBits idx" using cte misc invs' apply - apply (case_tac ut_cte) apply (rule ctes_of_valid_cap') apply simp apply fastforce done hence cover:
    "range_cover ptr_base pageBits pageBits (Suc 0)" apply - apply (rule range_cover_full) apply (simp add:valid_cap'_def capAligned_def) apply simp done have exclude: "cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1}" apply (rule descendants_range_ex_cte'[where cte = "ut_cte"]) apply (rule empty_descendants_range_in'[OF desc]) apply (rule if_unsafe_then_capD'[where P = "\<lambda>c. c = ut_cte"]) apply (clarsimp simp: cte_wp_at_ctes_of cte) apply (simp add:invs' invs_unsafe_then_cap') apply (simp add:cte invs')+ done show "\<lbrace>(=) s\<rbrace>performASIDControlInvocation (asidcontrol_invocation.MakePool ptr_base p cref ptr)
       \<lbrace>\<lambda>reply. no_orphans\<rbrace>" apply (clarsimp simp: performASIDControlInvocation_def
                  split: asidcontrol_invocation.splits) apply (wp hoare_weak_lift_imp | clarsimp)+ apply (rule_tac Q="\<lambda>rv s. no_orphans s" in hoare_post_imp) apply (clarsimp simp: no_orphans_def all_active_tcb_ptrs_def
                           is_active_tcb_ptr_def all_queued_tcb_ptrs_def) apply (wp | clarsimp simp:placeNewObject_def2)+ apply (wp createObjects'_wp_subst)+ apply (wp hoare_weak_lift_imp updateFreeIndex_pspace_no_overlap'[where sz= pageBits] getSlotCap_wp | simp)+ apply (strengthen invs_pspace_aligned' invs_pspace_distinct' invs_valid_pspace') apply (clarsimp simp:conj_comms) apply (wp deleteObjects_invs'[where idx = idx and d=False]
       hoare_vcg_ex_lift deleteObjects_cte_wp_at'[where idx = idx and d=False] hoare_vcg_const_imp_lift ) using invs' misc cte exclude no_orphans cover apply (clarsimp simp: is_active_thread_state_def makeObject_tcb valid_aci'_def
                        cte_wp_at_ctes_of invs_pspace_aligned' invs_pspace_distinct'
                        projectKO_opt_tcb isRunning_def isRestart_def conj_comms
                        invs_valid_pspace' vc objBits_simps archObjSize_def range_cover.aligned) apply (intro conjI) apply (rule vc) apply (simp add:descendants_range'_def2) apply (rule empty_descendants_range_in'[OF desc]) apply clarsimp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_aci' aci s \<and> ct_active' s\<rbrace> performASIDControlInvocation aci \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. no_orphans s \<and> invs' s \<and> valid_aci' aci s \<and> ct_active' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> performASIDControlInvocation aci \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x3 x4 cte ctea idx. \<lbrakk>aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; no_orphans s; invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some ctea; cteCap ctea = capability.UntypedCap False x1 pageBits idx; x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> performASIDControlInvocation (asidcontrol_invocation.MakePool x1 x2 x3 x4) \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ptr_base p cref ptr null_cte ut_cte idx. \<lbrakk>aci = asidcontrol_invocation.MakePool ptr_base p cref ptr; no_orphans s; invs' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; descendants_of' cref (ctes_of s) = {}; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> performASIDControlInvocation (asidcontrol_invocation.MakePool ptr_base p cref ptr) \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>s ptr_base p cref ptr null_cte ut_cte idx. \<lbrakk>aci = asidcontrol_invocation.MakePool ptr_base p cref ptr; no_orphans s; invs' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; descendants_of' cref (ctes_of s) = {}; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> performASIDControlInvocation (asidcontrol_invocation.MakePool ptr_base p cref ptr) \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>s ptr_base p cref ptr null_cte ut_cte idx. \<lbrakk>aci = asidcontrol_invocation.MakePool ptr_base p cref ptr; no_orphans s; invs' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; descendants_of' cref (ctes_of s) = {}; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> performASIDControlInvocation (asidcontrol_invocation.MakePool ptr_base p cref ptr) \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (state)
this:
no_orphans s
invs' s
ctes_of s p = Some null_cte
cteCap null_cte = capability.NullCap
ctes_of s cref = Some ut_cte
cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx
descendants_of' cref (ctes_of s) = {}
p \<noteq> cref
ex_cte_cap_wp_to' (\<lambda>_. True) p s
sch_act_simple s
is_aligned ptr local.asid_low_bits
ptr < 2 ^ local.asid_bits
ct_active' s

goal (1 subgoal):
 1. \<And>s ptr_base p cref ptr null_cte ut_cte idx. \<lbrakk>aci = asidcontrol_invocation.MakePool ptr_base p cref ptr; no_orphans s; invs' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; descendants_of' cref (ctes_of s) = {}; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> performASIDControlInvocation (asidcontrol_invocation.MakePool ptr_base p cref ptr) \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. valid_cap' (capability.UntypedCap False ptr_base pageBits idx) s proof (prove)
using this:
ctes_of s p = Some null_cte
cteCap null_cte = capability.NullCap
ctes_of s cref = Some ut_cte
cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx
p \<noteq> cref
ex_cte_cap_wp_to' (\<lambda>_. True) p s
sch_act_simple s
is_aligned ptr local.asid_low_bits
ptr < 2 ^ local.asid_bits
ct_active' s
invs' s

goal (1 subgoal):
 1. valid_cap' (capability.UntypedCap False ptr_base pageBits idx) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s; invs' s\<rbrakk> \<Longrightarrow> valid_cap' (capability.UntypedCap False ptr_base pageBits idx) s proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s; invs' s; ut_cte = CTE x1 x2\<rbrakk> \<Longrightarrow> valid_cap' (capability.UntypedCap False ptr_base pageBits idx) s proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s; invs' s; ut_cte = CTE x1 x2\<rbrakk> \<Longrightarrow> ctes_of s (?p12 x1 x2) = Some (CTE (capability.UntypedCap False ptr_base pageBits idx) (?n12 x1 x2))
 2. \<And>x1 x2. \<lbrakk>ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s; invs' s; ut_cte = CTE x1 x2\<rbrakk> \<Longrightarrow> valid_objs' s proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s; invs' s; ut_cte = CTE x1 x2\<rbrakk> \<Longrightarrow> valid_objs' s proof (prove)
goal:
No subgoals! proof (state)
this:
valid_cap' (capability.UntypedCap False ptr_base pageBits idx) s

goal (1 subgoal):
 1. \<And>s ptr_base p cref ptr null_cte ut_cte idx. \<lbrakk>aci = asidcontrol_invocation.MakePool ptr_base p cref ptr; no_orphans s; invs' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; descendants_of' cref (ctes_of s) = {}; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> performASIDControlInvocation (asidcontrol_invocation.MakePool ptr_base p cref ptr) \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
using this:
valid_cap' (capability.UntypedCap False ptr_base pageBits idx) s

goal (1 subgoal):
 1. range_cover ptr_base pageBits pageBits (Suc 0) proof (prove)
goal (1 subgoal):
 1. valid_cap' (capability.UntypedCap False ptr_base pageBits idx) s \<Longrightarrow> range_cover ptr_base pageBits pageBits (Suc 0) proof (prove)
goal (2 subgoals):
 1. valid_cap' (capability.UntypedCap False ptr_base pageBits idx) s \<Longrightarrow> is_aligned ptr_base pageBits
 2. valid_cap' (capability.UntypedCap False ptr_base pageBits idx) s \<Longrightarrow> pageBits < word_bits proof (prove)
goal (1 subgoal):
 1. valid_cap' (capability.UntypedCap False ptr_base pageBits idx) s \<Longrightarrow> pageBits < word_bits proof (prove)
goal:
No subgoals! proof (state)
this:
range_cover ptr_base pageBits pageBits (Suc 0)

goal (1 subgoal):
 1. \<And>s ptr_base p cref ptr null_cte ut_cte idx. \<lbrakk>aci = asidcontrol_invocation.MakePool ptr_base p cref ptr; no_orphans s; invs' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; descendants_of' cref (ctes_of s) = {}; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> performASIDControlInvocation (asidcontrol_invocation.MakePool ptr_base p cref ptr) \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1} proof (prove)
goal (6 subgoals):
 1. descendants_range_in' {ptr_base..ptr_base + 2 ^ pageBits - 1} ?p (ctes_of ?s')
 2. ex_cte_cap_wp_to' ?P cref ?s'
 3. {ptr_base..ptr_base + 2 ^ pageBits - 1} \<subseteq> capRange (cteCap ut_cte)
 4. invs' ?s'
 5. ctes_of ?s' ?p = Some ut_cte
 6. isUntypedCap (cteCap ut_cte) proof (prove)
goal (5 subgoals):
 1. ex_cte_cap_wp_to' ?P cref s
 2. {ptr_base..ptr_base + 2 ^ pageBits - 1} \<subseteq> capRange (cteCap ut_cte)
 3. invs' s
 4. ctes_of s cref = Some ut_cte
 5. isUntypedCap (cteCap ut_cte) proof (prove)
goal (7 subgoals):
 1. cte_wp_at' (\<lambda>c. c = ut_cte) cref s
 2. if_unsafe_then_cap' s
 3. \<And>cte. cte = ut_cte \<Longrightarrow> cteCap cte \<noteq> capability.NullCap
 4. {ptr_base..ptr_base + 2 ^ pageBits - 1} \<subseteq> capRange (cteCap ut_cte)
 5. invs' s
 6. ctes_of s cref = Some ut_cte
 7. isUntypedCap (cteCap ut_cte) proof (prove)
goal (6 subgoals):
 1. if_unsafe_then_cap' s
 2. \<And>cte. cte = ut_cte \<Longrightarrow> cteCap cte \<noteq> capability.NullCap
 3. {ptr_base..ptr_base + 2 ^ pageBits - 1} \<subseteq> capRange (cteCap ut_cte)
 4. invs' s
 5. ctes_of s cref = Some ut_cte
 6. isUntypedCap (cteCap ut_cte) proof (prove)
goal (5 subgoals):
 1. \<And>cte. cte = ut_cte \<Longrightarrow> cteCap cte \<noteq> capability.NullCap
 2. {ptr_base..ptr_base + 2 ^ pageBits - 1} \<subseteq> capRange (cteCap ut_cte)
 3. invs' s
 4. ctes_of s cref = Some ut_cte
 5. isUntypedCap (cteCap ut_cte) proof (prove)
goal:
No subgoals! proof (state)
this:
cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1}

goal (1 subgoal):
 1. \<And>s ptr_base p cref ptr null_cte ut_cte idx. \<lbrakk>aci = asidcontrol_invocation.MakePool ptr_base p cref ptr; no_orphans s; invs' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; descendants_of' cref (ctes_of s) = {}; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> performASIDControlInvocation (asidcontrol_invocation.MakePool ptr_base p cref ptr) \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s\<rbrace> performASIDControlInvocation (asidcontrol_invocation.MakePool ptr_base p cref ptr) \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s\<rbrace> do y <- deleteObjects ptr_base pageBits;
pcap <- getSlotCap cref;
y <- updateFreeIndex cref (max_free_index (capBlockSize pcap));
y <- placeNewObject ptr_base makeObject 0;
y <- cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap ptr_base ptr)) cref p;
y <- assert (ptr && mask local.asid_low_bits = 0);
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of ptr) \<mapsto> ptr_base)) (ksArchState s)\<rparr>)
od \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>pcap. \<lbrace>?P'13 () pcap () ()\<rbrace> cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap ptr_base ptr)) cref p \<lbrace>\<lambda>rv s. no_orphans (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_ a. if a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of ptr) then Some ptr_base else armKSASIDTable (ksArchState s) a) (ksArchState s)\<rparr>)\<rbrace>
 2. \<And>y pcap ya. \<lbrace>?B4 y pcap ya\<rbrace> placeNewObject ptr_base makeObject 0 \<lbrace>\<lambda>yb s. ptr && mask local.asid_low_bits = 0 \<longrightarrow> ?P'13 y pcap ya yb s\<rbrace>
 3. \<And>y pcap. \<lbrace>?B3 y pcap\<rbrace> updateFreeIndex cref (max_free_index (capBlockSize pcap)) \<lbrace>?B4 y pcap\<rbrace>
 4. \<And>y. \<lbrace>?B2 y\<rbrace> getSlotCap cref \<lbrace>?B3 y\<rbrace>
 5. \<lbrace>?Q1\<rbrace> deleteObjects ptr_base pageBits \<lbrace>?B2\<rbrace>
 6. \<And>sa. s = sa \<Longrightarrow> ?Q1 sa proof (prove)
goal (7 subgoals):
 1. \<And>pcap rv s. no_orphans s \<Longrightarrow> no_orphans (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_ a. if a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of ptr) then Some ptr_base else armKSASIDTable (ksArchState s) a) (ksArchState s)\<rparr>)
 2. \<And>pcap. \<lbrace>?P'13 () pcap () ()\<rbrace> cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap ptr_base ptr)) cref p \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>y pcap ya. \<lbrace>?B4 y pcap ya\<rbrace> placeNewObject ptr_base makeObject 0 \<lbrace>\<lambda>yb s. ptr && mask local.asid_low_bits = 0 \<longrightarrow> ?P'13 y pcap ya yb s\<rbrace>
 4. \<And>y pcap. \<lbrace>?B3 y pcap\<rbrace> updateFreeIndex cref (max_free_index (capBlockSize pcap)) \<lbrace>?B4 y pcap\<rbrace>
 5. \<And>y. \<lbrace>?B2 y\<rbrace> getSlotCap cref \<lbrace>?B3 y\<rbrace>
 6. \<lbrace>?Q1\<rbrace> deleteObjects ptr_base pageBits \<lbrace>?B2\<rbrace>
 7. \<And>sa. s = sa \<Longrightarrow> ?Q1 sa proof (prove)
goal (6 subgoals):
 1. \<And>pcap. \<lbrace>?P'13 () pcap () ()\<rbrace> cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap ptr_base ptr)) cref p \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>y pcap ya. \<lbrace>?B4 y pcap ya\<rbrace> placeNewObject ptr_base makeObject 0 \<lbrace>\<lambda>yb s. ptr && mask local.asid_low_bits = 0 \<longrightarrow> ?P'13 y pcap ya yb s\<rbrace>
 3. \<And>y pcap. \<lbrace>?B3 y pcap\<rbrace> updateFreeIndex cref (max_free_index (capBlockSize pcap)) \<lbrace>?B4 y pcap\<rbrace>
 4. \<And>y. \<lbrace>?B2 y\<rbrace> getSlotCap cref \<lbrace>?B3 y\<rbrace>
 5. \<lbrace>?Q1\<rbrace> deleteObjects ptr_base pageBits \<lbrace>?B2\<rbrace>
 6. \<And>sa. s = sa \<Longrightarrow> ?Q1 sa proof (prove)
goal (5 subgoals):
 1. \<And>pcap. \<lbrace>?B4 () pcap ()\<rbrace> createObjects' ptr_base (Suc 0) (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>yb s. ptr && mask local.asid_low_bits = 0 \<longrightarrow> no_orphans s\<rbrace>
 2. \<And>y pcap. \<lbrace>?B3 y pcap\<rbrace> updateFreeIndex cref (max_free_index (capBlockSize pcap)) \<lbrace>?B4 y pcap\<rbrace>
 3. \<And>y. \<lbrace>?B2 y\<rbrace> getSlotCap cref \<lbrace>?B3 y\<rbrace>
 4. \<lbrace>?Q1\<rbrace> deleteObjects ptr_base pageBits \<lbrace>?B2\<rbrace>
 5. \<And>sa. s = sa \<Longrightarrow> ?Q1 sa proof (prove)
goal (5 subgoals):
 1. \<And>pcap. \<lbrace>?B4 () pcap ()\<rbrace> createObjects ptr_base (Suc 0) (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>yb a. ptr && mask local.asid_low_bits = 0 \<longrightarrow> no_orphans a\<rbrace>
 2. \<And>y pcap. \<lbrace>?B3 y pcap\<rbrace> updateFreeIndex cref (max_free_index (capBlockSize pcap)) \<lbrace>?B4 y pcap\<rbrace>
 3. \<And>y. \<lbrace>?B2 y\<rbrace> getSlotCap cref \<lbrace>?B3 y\<rbrace>
 4. \<lbrace>?Q1\<rbrace> deleteObjects ptr_base pageBits \<lbrace>?B2\<rbrace>
 5. \<And>sa. s = sa \<Longrightarrow> ?Q1 sa proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'52\<rbrace> deleteObjects ptr_base pageBits \<lbrace>\<lambda>rv s. (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) cref s) \<and> no_orphans s \<and> pspace_aligned' s \<and> pspace_no_overlap' ptr_base pageBits s \<and> valid_pspace' s \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) cref s \<and> pspace_distinct' s \<and> range_cover ptr_base pageBits (objBitsKO (KOArch (KOASIDPool makeObject))) (Suc 0) \<and> \<not> (case projectKO_opt (KOArch (KOASIDPool makeObject)) of None \<Rightarrow> False | Some x2 \<Rightarrow> is_active_thread_state (tcbState x2))\<rbrace>
 2. \<And>sa. s = sa \<Longrightarrow> ptr && mask local.asid_low_bits = 0 \<longrightarrow> ?P'52 sa proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'52\<rbrace> deleteObjects ptr_base pageBits \<lbrace>\<lambda>r s. (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) cref s) \<and> no_orphans s \<and> invs' s \<and> pspace_no_overlap' ptr_base pageBits s \<and> invs' s \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) cref s \<and> invs' s \<and> range_cover ptr_base pageBits (objBitsKO (KOArch (KOASIDPool makeObject))) (Suc 0) \<and> \<not> (case projectKO_opt (KOArch (KOASIDPool makeObject)) of None \<Rightarrow> False | Some x2 \<Rightarrow> is_active_thread_state (tcbState x2))\<rbrace>
 2. \<And>sa. s = sa \<Longrightarrow> ptr && mask local.asid_low_bits = 0 \<longrightarrow> ?P'52 sa proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'52\<rbrace> deleteObjects ptr_base pageBits \<lbrace>\<lambda>r s. invs' s \<and> no_orphans s \<and> pspace_no_overlap' ptr_base pageBits s \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) cref s \<and> range_cover ptr_base pageBits (objBitsKO (KOArch (KOASIDPool makeObject))) (Suc 0) \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) cref s) \<and> \<not> (case projectKO_opt (KOArch (KOASIDPool makeObject)) of None \<Rightarrow> False | Some x2 \<Rightarrow> is_active_thread_state (tcbState x2))\<rbrace>
 2. \<And>sa. s = sa \<Longrightarrow> ptr && mask local.asid_low_bits = 0 \<longrightarrow> ?P'52 sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. s = sa \<Longrightarrow> ptr && mask local.asid_low_bits = 0 \<longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap False ptr_base pageBits idx) ?p81 and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap False ptr_base pageBits idx) ?p81 (ctes_of s)) and K (pageBits < word_bits \<and> is_aligned ptr_base pageBits)) sa \<and> ((\<lambda>s. no_orphans s \<and> pspace_distinct' s) and K (is_aligned ptr_base pageBits)) sa \<and> (valid_cap' (capability.UntypedCap ?d85 ptr_base pageBits ?idx85) and valid_pspace') sa \<and> (cte_wp_at' (isUntypedCap \<circ> cteCap) cref sa \<and> cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap False ptr_base pageBits idx) sa \<and> valid_pspace' sa) \<and> range_cover ptr_base pageBits (objBitsKO (KOArch (KOASIDPool makeObject))) (Suc 0) \<and> (\<exists>x. cte_wp_at' (\<lambda>c. cteCap c = x) cref sa \<and> cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap False ptr_base pageBits idx) sa \<and> valid_pspace' sa) \<and> \<not> (case projectKO_opt (KOArch (KOASIDPool makeObject)) of None \<Rightarrow> False | Some x2 \<Rightarrow> is_active_thread_state (tcbState x2)) proof (prove)
using this:
invs' s
p \<noteq> cref
ex_cte_cap_wp_to' (\<lambda>_. True) p s
sch_act_simple s
is_aligned ptr local.asid_low_bits
ptr < 2 ^ local.asid_bits
ct_active' s
ctes_of s p = Some null_cte
cteCap null_cte = capability.NullCap
ctes_of s cref = Some ut_cte
cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx
cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1}
no_orphans s
range_cover ptr_base pageBits pageBits (Suc 0)

goal (1 subgoal):
 1. \<And>sa. s = sa \<Longrightarrow> ptr && mask local.asid_low_bits = 0 \<longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap False ptr_base pageBits idx) ?p81 and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap False ptr_base pageBits idx) ?p81 (ctes_of s)) and K (pageBits < word_bits \<and> is_aligned ptr_base pageBits)) sa \<and> ((\<lambda>s. no_orphans s \<and> pspace_distinct' s) and K (is_aligned ptr_base pageBits)) sa \<and> (valid_cap' (capability.UntypedCap ?d85 ptr_base pageBits ?idx85) and valid_pspace') sa \<and> (cte_wp_at' (isUntypedCap \<circ> cteCap) cref sa \<and> cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap False ptr_base pageBits idx) sa \<and> valid_pspace' sa) \<and> range_cover ptr_base pageBits (objBitsKO (KOArch (KOASIDPool makeObject))) (Suc 0) \<and> (\<exists>x. cte_wp_at' (\<lambda>c. cteCap c = x) cref sa \<and> cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap False ptr_base pageBits idx) sa \<and> valid_pspace' sa) \<and> \<not> (case projectKO_opt (KOArch (KOASIDPool makeObject)) of None \<Rightarrow> False | Some x2 \<Rightarrow> is_active_thread_state (tcbState x2)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1}; no_orphans s; range_cover ptr_base pageBits pageBits (Suc 0); ptr && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> valid_cap' (capability.UntypedCap ?d85 ptr_base pageBits ?idx85) s \<and> descendants_range' (capability.UntypedCap False ptr_base pageBits idx) ?p81 (ctes_of s) \<and> (\<exists>cte. ctes_of s ?p81 = Some cte \<and> cteCap cte = capability.UntypedCap False ptr_base pageBits idx) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invs' s; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1}; no_orphans s; range_cover ptr_base pageBits pageBits (Suc 0); ptr && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> valid_cap' (capability.UntypedCap ?d85 ptr_base pageBits ?idx85) s
 2. \<lbrakk>invs' s; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1}; no_orphans s; range_cover ptr_base pageBits pageBits (Suc 0); ptr && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> descendants_range' (capability.UntypedCap False ptr_base pageBits idx) ?p81 (ctes_of s)
 3. \<lbrakk>invs' s; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1}; no_orphans s; range_cover ptr_base pageBits pageBits (Suc 0); ptr && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s ?p81 = Some cte \<and> cteCap cte = capability.UntypedCap False ptr_base pageBits idx proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs' s; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1}; no_orphans s; range_cover ptr_base pageBits pageBits (Suc 0); ptr && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> descendants_range' (capability.UntypedCap False ptr_base pageBits idx) ?p81 (ctes_of s)
 2. \<lbrakk>invs' s; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1}; no_orphans s; range_cover ptr_base pageBits pageBits (Suc 0); ptr && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s ?p81 = Some cte \<and> cteCap cte = capability.UntypedCap False ptr_base pageBits idx proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs' s; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1}; no_orphans s; range_cover ptr_base pageBits pageBits (Suc 0); ptr && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> descendants_range_in' {ptr_base..ptr_base + 2 ^ pageBits - 1} ?p81 (ctes_of s)
 2. \<lbrakk>invs' s; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1}; no_orphans s; range_cover ptr_base pageBits pageBits (Suc 0); ptr && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s ?p81 = Some cte \<and> cteCap cte = capability.UntypedCap False ptr_base pageBits idx proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; p \<noteq> cref; ex_cte_cap_wp_to' (\<lambda>_. True) p s; sch_act_simple s; is_aligned ptr local.asid_low_bits; ptr < 2 ^ local.asid_bits; ct_active' s; ctes_of s p = Some null_cte; cteCap null_cte = capability.NullCap; ctes_of s cref = Some ut_cte; cteCap ut_cte = capability.UntypedCap False ptr_base pageBits idx; cref \<notin> {ptr_base..ptr_base + 2 ^ pageBits - 1}; no_orphans s; range_cover ptr_base pageBits pageBits (Suc 0); ptr && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte = capability.UntypedCap False ptr_base pageBits idx proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>(=) s\<rbrace> performASIDControlInvocation (asidcontrol_invocation.MakePool ptr_base p cref ptr) \<lbrace>\<lambda>reply. no_orphans\<rbrace>

goal:
No subgoals!