theory Finalise_R

lemma emptySlot_untyped_ranges[wp]:
  "\<lbrace>untyped_ranges_zero' and valid_objs' and valid_mdb'\<rbrace>
     emptySlot sl opt \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>" apply (simp add: emptySlot_def case_Null_If) apply (rule hoare_pre) apply (rule hoare_seq_ext) apply (rule untyped_ranges_zero_lift) apply (wp getCTE_cteCap_wp clearUntypedFreeIndex_cteCaps_of
       | wpc | simp add: clearUntypedFreeIndex_def updateTrackedFreeIndex_def
                         getSlotCap_def
                  split: option.split)+ apply (clarsimp simp: modify_map_comp[symmetric] modify_map_same) apply (case_tac "\<not> isUntypedCap (the (cteCaps_of s sl))") apply (case_tac "the (cteCaps_of s sl)",
     simp_all add: untyped_ranges_zero_inv_def
                   untypedZeroRange_modify_map_isUntypedCap isCap_simps)[1] apply (clarsimp simp: isCap_simps untypedZeroRange_def modify_map_def) apply (strengthen untyped_ranges_zero_fun_upd[mk_strg I E]) apply simp apply (simp add: untypedZeroRange_def isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_ranges_zero' and valid_objs' and valid_mdb'\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_ranges_zero' and valid_objs' and valid_mdb'\<rbrace> do y <- clearUntypedFreeIndex sl;
newCTE <- getCTE sl;
if cteCap newCTE = capability.NullCap then return () else do y <- updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
y <- updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
y <- updateCap sl capability.NullCap;
y <- updateMDB sl (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> do y <- clearUntypedFreeIndex sl;
newCTE <- getCTE sl;
if cteCap newCTE = capability.NullCap then return () else do y <- updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
y <- updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
y <- updateCap sl capability.NullCap;
y <- updateMDB sl (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>
 2. \<And>s. (untyped_ranges_zero' and valid_objs' and valid_mdb') s \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>?B7 y\<rbrace> do newCTE <- getCTE sl;
if cteCap newCTE = capability.NullCap then return () else do y <- updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
y <- updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
y <- updateCap sl capability.NullCap;
y <- updateMDB sl (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>
 2. \<lbrace>?Q4\<rbrace> clearUntypedFreeIndex sl \<lbrace>?B7\<rbrace>
 3. \<And>s. (untyped_ranges_zero' and valid_objs' and valid_mdb') s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>y P. \<lbrace>\<lambda>s. P (gsUntypedZeroRanges s)\<rbrace> do newCTE <- getCTE sl;
if cteCap newCTE = capability.NullCap then return () else do y <- updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
y <- updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
y <- updateCap sl capability.NullCap;
y <- updateMDB sl (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>rv s. P (gsUntypedZeroRanges s)\<rbrace>
 2. \<And>y f. \<lbrace>?P10 y f\<rbrace> do newCTE <- getCTE sl;
if cteCap newCTE = capability.NullCap then return () else do y <- updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
y <- updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
y <- updateCap sl capability.NullCap;
y <- updateMDB sl (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>rv s. untyped_ranges_zero_inv (cteCaps_of s) f\<rbrace>
 3. \<lbrace>?Q4\<rbrace> clearUntypedFreeIndex sl \<lbrace>\<lambda>y s. ?P10 y (gsUntypedZeroRanges s) s\<rbrace>
 4. \<And>s. (untyped_ranges_zero' and valid_objs' and valid_mdb') s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. untyped_ranges_zero' s \<and> valid_objs' s \<and> valid_mdb' s \<Longrightarrow> \<forall>x2. cteCaps_of s sl = Some x2 \<longrightarrow> ((\<exists>x. x2 = capability.ThreadCap x) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb xc. x2 = capability.NotificationCap x xa xb xc) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x. x2 = capability.IRQHandlerCap x) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb xc xd xe. x2 = capability.EndpointCap x xa xb xc xd xe) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (x2 = capability.DomainCap \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb. x2 = capability.Zombie x xa xb) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x. x2 = capability.ArchObjectCap x) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb. x2 = capability.ReplyCap x xa xb) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (\<forall>x xa xb xc. (untypedZeroRange (capability.UntypedCap x xa xb xc) = None \<longrightarrow> (untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = None \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (\<forall>a b. untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = Some (a, b) \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (insert (a, b) (gsUntypedZeroRanges s)))) \<and> (\<forall>a b. untypedZeroRange (capability.UntypedCap x xa xb xc) = Some (a, b) \<longrightarrow> (untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = None \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s - {(a, b)})) \<and> (\<forall>aa ba. untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = Some (aa, ba) \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (insert (aa, ba) (gsUntypedZeroRanges s - {(a, b)}))))) \<and> ((\<exists>x xa xb xc. x2 = capability.CNodeCap x xa xb xc) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (x2 = capability.IRQControlCap \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>untyped_ranges_zero' s; valid_objs' s; valid_mdb' s; cteCaps_of s sl = Some x2\<rbrakk> \<Longrightarrow> ((\<exists>x. x2 = capability.ThreadCap x) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb xc. x2 = capability.NotificationCap x xa xb xc) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x. x2 = capability.IRQHandlerCap x) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb xc xd xe. x2 = capability.EndpointCap x xa xb xc xd xe) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (x2 = capability.DomainCap \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb. x2 = capability.Zombie x xa xb) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x. x2 = capability.ArchObjectCap x) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb. x2 = capability.ReplyCap x xa xb) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (\<forall>x xa xb xc. (untypedZeroRange (capability.UntypedCap x xa xb xc) = None \<longrightarrow> (untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = None \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (\<forall>a b. untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = Some (a, b) \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (insert (a, b) (gsUntypedZeroRanges s)))) \<and> (\<forall>a b. untypedZeroRange (capability.UntypedCap x xa xb xc) = Some (a, b) \<longrightarrow> (untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = None \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s - {(a, b)})) \<and> (\<forall>aa ba. untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = Some (aa, ba) \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (insert (aa, ba) (gsUntypedZeroRanges s - {(a, b)}))))) \<and> ((\<exists>x xa xb xc. x2 = capability.CNodeCap x xa xb xc) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (x2 = capability.IRQControlCap \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<lbrakk>untyped_ranges_zero' s; valid_objs' s; valid_mdb' s; cteCaps_of s sl = Some x2; \<not> isUntypedCap (the (cteCaps_of s sl))\<rbrakk> \<Longrightarrow> ((\<exists>x. x2 = capability.ThreadCap x) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb xc. x2 = capability.NotificationCap x xa xb xc) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x. x2 = capability.IRQHandlerCap x) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb xc xd xe. x2 = capability.EndpointCap x xa xb xc xd xe) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (x2 = capability.DomainCap \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb. x2 = capability.Zombie x xa xb) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x. x2 = capability.ArchObjectCap x) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb. x2 = capability.ReplyCap x xa xb) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (\<forall>x xa xb xc. (untypedZeroRange (capability.UntypedCap x xa xb xc) = None \<longrightarrow> (untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = None \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (\<forall>a b. untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = Some (a, b) \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (insert (a, b) (gsUntypedZeroRanges s)))) \<and> (\<forall>a b. untypedZeroRange (capability.UntypedCap x xa xb xc) = Some (a, b) \<longrightarrow> (untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = None \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s - {(a, b)})) \<and> (\<forall>aa ba. untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = Some (aa, ba) \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (insert (aa, ba) (gsUntypedZeroRanges s - {(a, b)}))))) \<and> ((\<exists>x xa xb xc. x2 = capability.CNodeCap x xa xb xc) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (x2 = capability.IRQControlCap \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s))
 2. \<And>s x2. \<lbrakk>untyped_ranges_zero' s; valid_objs' s; valid_mdb' s; cteCaps_of s sl = Some x2; \<not> \<not> isUntypedCap (the (cteCaps_of s sl))\<rbrakk> \<Longrightarrow> ((\<exists>x. x2 = capability.ThreadCap x) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb xc. x2 = capability.NotificationCap x xa xb xc) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x. x2 = capability.IRQHandlerCap x) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb xc xd xe. x2 = capability.EndpointCap x xa xb xc xd xe) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (x2 = capability.DomainCap \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb. x2 = capability.Zombie x xa xb) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x. x2 = capability.ArchObjectCap x) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb. x2 = capability.ReplyCap x xa xb) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (\<forall>x xa xb xc. (untypedZeroRange (capability.UntypedCap x xa xb xc) = None \<longrightarrow> (untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = None \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (\<forall>a b. untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = Some (a, b) \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (insert (a, b) (gsUntypedZeroRanges s)))) \<and> (\<forall>a b. untypedZeroRange (capability.UntypedCap x xa xb xc) = Some (a, b) \<longrightarrow> (untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = None \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s - {(a, b)})) \<and> (\<forall>aa ba. untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = Some (aa, ba) \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (insert (aa, ba) (gsUntypedZeroRanges s - {(a, b)}))))) \<and> ((\<exists>x xa xb xc. x2 = capability.CNodeCap x xa xb xc) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (x2 = capability.IRQControlCap \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>untyped_ranges_zero' s; valid_objs' s; valid_mdb' s; cteCaps_of s sl = Some x2; \<not> \<not> isUntypedCap (the (cteCaps_of s sl))\<rbrakk> \<Longrightarrow> ((\<exists>x. x2 = capability.ThreadCap x) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb xc. x2 = capability.NotificationCap x xa xb xc) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x. x2 = capability.IRQHandlerCap x) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb xc xd xe. x2 = capability.EndpointCap x xa xb xc xd xe) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (x2 = capability.DomainCap \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb. x2 = capability.Zombie x xa xb) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x. x2 = capability.ArchObjectCap x) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> ((\<exists>x xa xb. x2 = capability.ReplyCap x xa xb) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (\<forall>x xa xb xc. (untypedZeroRange (capability.UntypedCap x xa xb xc) = None \<longrightarrow> (untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = None \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (\<forall>a b. untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = Some (a, b) \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (insert (a, b) (gsUntypedZeroRanges s)))) \<and> (\<forall>a b. untypedZeroRange (capability.UntypedCap x xa xb xc) = Some (a, b) \<longrightarrow> (untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = None \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s - {(a, b)})) \<and> (\<forall>aa ba. untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb)) = Some (aa, ba) \<longrightarrow> x2 = capability.UntypedCap x xa xb xc \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (insert (aa, ba) (gsUntypedZeroRanges s - {(a, b)}))))) \<and> ((\<exists>x xa xb xc. x2 = capability.CNodeCap x xa xb xc) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (x2 = capability.IRQControlCap \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s)) proof (prove)
goal (1 subgoal):
 1. \<And>s d v0 v1 f x xa xb xc. \<lbrakk>untyped_ranges_zero' s; valid_objs' s; valid_mdb' s; cteCaps_of s sl = Some (capability.UntypedCap d v0 v1 f)\<rbrakk> \<Longrightarrow> (xc = max_free_index xb \<longrightarrow> d = x \<and> v0 = xa \<and> v1 = xb \<and> f = max_free_index xb \<longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(sl \<mapsto> capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (x \<longrightarrow> d \<and> v0 = xa \<and> v1 = xb \<and> f = xc \<longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(sl \<mapsto> capability.NullCap)) (gsUntypedZeroRanges s)) \<and> (xc \<noteq> max_free_index xb \<and> \<not> x \<longrightarrow> \<not> d \<and> v0 = xa \<and> v1 = xb \<and> f = xc \<longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(sl \<mapsto> capability.NullCap)) (gsUntypedZeroRanges s - {(getFreeRef xa xc, xa + 2 ^ xb - 1)})) proof (prove)
goal (1 subgoal):
 1. \<And>s d v0 v1 f x xa xb xc. \<lbrakk>untyped_ranges_zero' s; valid_objs' s; valid_mdb' s; cteCaps_of s sl = Some (capability.UntypedCap d v0 v1 f)\<rbrakk> \<Longrightarrow> (xc = max_free_index xb \<longrightarrow> d = x \<and> v0 = xa \<and> v1 = xb \<and> f = max_free_index xb \<longrightarrow> (\<forall>p. p \<noteq> sl \<longrightarrow> cteCaps_of s p = cteCaps_of s p) \<and> valid_mdb' s \<and> valid_objs' s \<and> (set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) sl) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) sl) \<union> set_option (untypedZeroRange capability.NullCap))) \<and> (x \<longrightarrow> d \<and> v0 = xa \<and> v1 = xb \<and> f = xc \<longrightarrow> (\<forall>p. p \<noteq> sl \<longrightarrow> cteCaps_of s p = cteCaps_of s p) \<and> valid_mdb' s \<and> valid_objs' s \<and> (set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) sl) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) sl) \<union> set_option (untypedZeroRange capability.NullCap))) \<and> (xc \<noteq> max_free_index xb \<and> \<not> x \<longrightarrow> \<not> d \<and> v0 = xa \<and> v1 = xb \<and> f = xc \<longrightarrow> (\<forall>p. p \<noteq> sl \<longrightarrow> cteCaps_of s p = cteCaps_of s p) \<and> valid_mdb' s \<and> valid_objs' s \<and> (set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) sl) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s - {(getFreeRef xa xc, xa + 2 ^ xb - 1)} = gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) sl) \<union> set_option (untypedZeroRange capability.NullCap))) proof (prove)
goal (1 subgoal):
 1. \<And>s d v0 v1 f x xa xb xc. \<lbrakk>untyped_ranges_zero' s; valid_objs' s; valid_mdb' s; cteCaps_of s sl = Some (capability.UntypedCap d v0 v1 f)\<rbrakk> \<Longrightarrow> (xc = max_free_index xb \<longrightarrow> d = x \<and> v0 = xa \<and> v1 = xb \<and> f = max_free_index xb \<longrightarrow> set_option (untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb))) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - set_option (untypedZeroRange (capability.UntypedCap x xa xb (max_free_index xb))) \<union> set_option (untypedZeroRange capability.NullCap)) \<and> (x \<longrightarrow> d \<and> v0 = xa \<and> v1 = xb \<and> f = xc \<longrightarrow> set_option (untypedZeroRange (capability.UntypedCap True xa xb xc)) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - set_option (untypedZeroRange (capability.UntypedCap True xa xb xc)) \<union> set_option (untypedZeroRange capability.NullCap)) \<and> (xc \<noteq> max_free_index xb \<and> \<not> x \<longrightarrow> \<not> d \<and> v0 = xa \<and> v1 = xb \<and> f = xc \<longrightarrow> set_option (untypedZeroRange (capability.UntypedCap False xa xb xc)) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s - {(getFreeRef xa xc, xa + 2 ^ xb - 1)} = gsUntypedZeroRanges s - set_option (untypedZeroRange (capability.UntypedCap False xa xb xc)) \<union> set_option (untypedZeroRange capability.NullCap)) proof (prove)
goal:
No subgoals!