theory Untyped_R

lemma insertNewCap_urz[wp]:
  "\<lbrace>untyped_ranges_zero' and valid_objs' and valid_mdb'\<rbrace>
      insertNewCap parent slot cap \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>" apply (simp add: insertNewCap_def updateNewFreeIndex_def) apply (wp getCTE_cteCap_wp
    | simp add: updateTrackedFreeIndex_def getSlotCap_def case_eq_if_isUntypedCap
               split: option.split split del: if_split
    | wps | wp (once) getCTE_wp')+ apply (clarsimp simp: cte_wp_at_ctes_of fun_upd_def[symmetric]) apply (strengthen untyped_ranges_zero_fun_upd[mk_strg I E]) apply (intro conjI impI; clarsimp simp: isCap_simps) apply (auto simp add: cteCaps_of_def 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> insertNewCap parent slot cap \<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 next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
cap <- getSlotCap slot;
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (capFreeIndex cap) | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. untyped_ranges_zero' s \<and> valid_objs' s \<and> valid_mdb' s \<Longrightarrow> (\<exists>x2. cteCaps_of s parent = Some x2) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) slot s \<longrightarrow> cteCap cte = capability.NullCap \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> mdbPrev (cteMDBNode cte) = nullPointer \<longrightarrow> (\<forall>x2. (untypedZeroRange x2 = None \<longrightarrow> (untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) x2) = None \<longrightarrow> cap = x2 \<longrightarrow> untyped_ranges_zero_inv (\<lambda>a. if a = slot then Some x2 else cteCaps_of s a) (gsUntypedZeroRanges s)) \<and> (\<forall>a b. untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) x2) = Some (a, b) \<longrightarrow> cap = x2 \<longrightarrow> (isUntypedCap x2 \<longrightarrow> untyped_ranges_zero_inv (\<lambda>a. if a = slot then Some x2 else cteCaps_of s a) (insert (a, b) (gsUntypedZeroRanges s))) \<and> (\<not> isUntypedCap x2 \<longrightarrow> untyped_ranges_zero_inv (\<lambda>a. if a = slot then Some x2 else cteCaps_of s a) (gsUntypedZeroRanges s)))) \<and> (\<forall>a b. untypedZeroRange x2 = Some (a, b) \<longrightarrow> (untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) x2) = None \<longrightarrow> cap = x2 \<longrightarrow> (isUntypedCap x2 \<longrightarrow> untyped_ranges_zero_inv (\<lambda>a. if a = slot then Some x2 else cteCaps_of s a) (gsUntypedZeroRanges s - {(a, b)})) \<and> (\<not> isUntypedCap x2 \<longrightarrow> untyped_ranges_zero_inv (\<lambda>a. if a = slot then Some x2 else cteCaps_of s a) (gsUntypedZeroRanges s))) \<and> (\<forall>aa ba. untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) x2) = Some (aa, ba) \<longrightarrow> cap = x2 \<longrightarrow> (isUntypedCap x2 \<longrightarrow> untyped_ranges_zero_inv (\<lambda>a. if a = slot then Some x2 else cteCaps_of s a) (insert (aa, ba) (gsUntypedZeroRanges s - {(a, b)}))) \<and> (\<not> isUntypedCap x2 \<longrightarrow> untyped_ranges_zero_inv (\<lambda>a. if a = slot then Some x2 else cteCaps_of s a) (gsUntypedZeroRanges s)))))) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 cte x2a. \<lbrakk>untyped_ranges_zero' s; valid_objs' s; valid_mdb' s; cteCaps_of s parent = Some x2; ctes_of s slot = Some cte; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (untypedZeroRange x2a = None \<longrightarrow> (untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) x2a) = None \<longrightarrow> cap = x2a \<longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(slot \<mapsto> x2a)) (gsUntypedZeroRanges s)) \<and> (\<forall>a b. untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) x2a) = Some (a, b) \<longrightarrow> cap = x2a \<longrightarrow> (isUntypedCap x2a \<longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(slot \<mapsto> x2a)) (insert (a, b) (gsUntypedZeroRanges s))) \<and> (\<not> isUntypedCap x2a \<longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(slot \<mapsto> x2a)) (gsUntypedZeroRanges s)))) \<and> (\<forall>a b. untypedZeroRange x2a = Some (a, b) \<longrightarrow> (untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) x2a) = None \<longrightarrow> cap = x2a \<longrightarrow> (isUntypedCap x2a \<longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(slot \<mapsto> x2a)) (gsUntypedZeroRanges s - {(a, b)})) \<and> (\<not> isUntypedCap x2a \<longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(slot \<mapsto> x2a)) (gsUntypedZeroRanges s))) \<and> (\<forall>aa ba. untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) x2a) = Some (aa, ba) \<longrightarrow> cap = x2a \<longrightarrow> (isUntypedCap x2a \<longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(slot \<mapsto> x2a)) (insert (aa, ba) (gsUntypedZeroRanges s - {(a, b)}))) \<and> (\<not> isUntypedCap x2a \<longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(slot \<mapsto> x2a)) (gsUntypedZeroRanges s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 cte x2a. \<lbrakk>untyped_ranges_zero' s; valid_objs' s; valid_mdb' s; cteCaps_of s parent = Some x2; ctes_of s slot = Some cte; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (untypedZeroRange x2a = None \<longrightarrow> (untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) x2a) = None \<longrightarrow> cap = x2a \<longrightarrow> (\<forall>p. p \<noteq> slot \<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) slot) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot) \<union> set_option (untypedZeroRange x2a))) \<and> (\<forall>x xa. untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) x2a) = Some (x, xa) \<longrightarrow> cap = x2a \<longrightarrow> (isUntypedCap x2a \<longrightarrow> (\<forall>p. p \<noteq> slot \<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) slot) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> insert (x, xa) (gsUntypedZeroRanges s) = gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot) \<union> set_option (untypedZeroRange x2a))) \<and> (\<not> isUntypedCap x2a \<longrightarrow> (\<forall>p. p \<noteq> slot \<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) slot) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot) \<union> set_option (untypedZeroRange x2a))))) \<and> (\<forall>x xa. untypedZeroRange x2a = Some (x, xa) \<longrightarrow> (untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) x2a) = None \<longrightarrow> cap = x2a \<longrightarrow> (isUntypedCap x2a \<longrightarrow> (\<forall>p. p \<noteq> slot \<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) slot) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s - {(x, xa)} = gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot) \<union> set_option (untypedZeroRange x2a))) \<and> (\<not> isUntypedCap x2a \<longrightarrow> (\<forall>p. p \<noteq> slot \<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) slot) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot) \<union> set_option (untypedZeroRange x2a)))) \<and> (\<forall>xb xc. untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) x2a) = Some (xb, xc) \<longrightarrow> cap = x2a \<longrightarrow> (isUntypedCap x2a \<longrightarrow> (\<forall>p. p \<noteq> slot \<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) slot) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> insert (xb, xc) (gsUntypedZeroRanges s - {(x, xa)}) = gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot) \<union> set_option (untypedZeroRange x2a))) \<and> (\<not> isUntypedCap x2a \<longrightarrow> (\<forall>p. p \<noteq> slot \<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) slot) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot) \<union> set_option (untypedZeroRange x2a))))) proof (prove)
goal (3 subgoals):
 1. \<And>s x2 cte. \<lbrakk>untyped_ranges_zero' s; valid_objs' s; valid_mdb' s; cteCaps_of s parent = Some x2; ctes_of s slot = Some cte; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; untypedZeroRange cap = None; untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) cap) = None; set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot) \<subseteq> gsUntypedZeroRanges s\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot)
 2. \<And>s x2 cte x xa. \<lbrakk>untyped_ranges_zero' s; valid_objs' s; valid_mdb' s; cteCaps_of s parent = Some x2; ctes_of s slot = Some cte; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; untypedZeroRange cap = None; untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) cap) = Some (x, xa)\<rbrakk> \<Longrightarrow> ((\<exists>d v0 v1 f. cap = capability.UntypedCap d v0 v1 f) \<longrightarrow> set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> insert (x, xa) (gsUntypedZeroRanges s) = gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot)) \<and> ((\<forall>d v0 v1 f. cap \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot))
 3. \<And>s x2 cte x2a x xa. \<lbrakk>untyped_ranges_zero' s; valid_objs' s; valid_mdb' s; cteCaps_of s parent = Some x2; ctes_of s slot = Some cte; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; untypedZeroRange x2a = Some (x, xa)\<rbrakk> \<Longrightarrow> (untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) x2a) = None \<longrightarrow> cap = x2a \<longrightarrow> ((\<exists>d v0 v1 f. x2a = capability.UntypedCap d v0 v1 f) \<longrightarrow> set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s - {(x, xa)} = insert (x, xa) (gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot))) \<and> ((\<forall>d v0 v1 f. x2a \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s = insert (x, xa) (gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot)))) \<and> (\<forall>xb xc. untypedZeroRange (capFreeIndex_update (\<lambda>_. capFreeIndex cap) x2a) = Some (xb, xc) \<longrightarrow> cap = x2a \<longrightarrow> ((\<exists>d v0 v1 f. x2a = capability.UntypedCap d v0 v1 f) \<longrightarrow> set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> insert (xb, xc) (gsUntypedZeroRanges s - {(x, xa)}) = insert (x, xa) (gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot))) \<and> ((\<forall>d v0 v1 f. x2a \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s = insert (x, xa) (gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) slot)))) proof (prove)
goal:
No subgoals!