feat(snapshot): prove promotion preserves unselected snapshot contents

Split gives two seL4 workers private configuration snapshots through a userspace pager that copies shared pages on first write and scrubs discarded frames before reuse, with an Isabelle model exported to OCaml for checking guest memory operations.

https://github.com/user-attachments/assets/7301c6cf-f13c-49f5-9c92-14049c07c3ef

<video controls src="https://codesperg.org/wmxiel/split/raw/branch/main/media/split.mp4">

  <a href="media/split.mp4">Watch the demonstration</a>

</video>

   physical (execute (initial pages contents) actions) f = contents f"

  using execute_original[OF initial_private] by simp

definition promote :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> pager" where

  "promote pages slots source s =

    s\<lparr>ptable := (\<lambda>k. if slots \<le> k \<and> k < slots + pages

      then ptable s (source + (k - slots)) else ptable s k),

      writable := (\<lambda>k. writable s k \<and> \<not> (source \<le> k \<and> k < source + pages)

        \<and> \<not> (slots \<le> k \<and> k < slots + pages))\<rparr>"

lemma promotion_live_view:

  "k < slots \<Longrightarrow> view (promote pages slots source s) k = view s k"

  by (simp add: promote_def view_def)

lemma promotion_baseline_view:

  "p < pages \<Longrightarrow>

   view (promote pages slots source s) (slots + p) = view s (source + p)"

  by (simp add: promote_def view_def)

lemma promotion_baseline_readonly:

  "p < pages \<Longrightarrow> \<not> writable (promote pages slots source s) (slots + p)"

  by (simp add: promote_def)

lemma promotion_source_readonly:

  "p < pages \<Longrightarrow> \<not> writable (promote pages slots source s) (source + p)"

  by (simp add: promote_def)

lemma promotion_bounded:

  assumes bounds: "bounded (slots + pages) s" and source: "source + pages \<le> slots"

  shows "bounded (slots + pages) (promote pages slots source s)"

proof (unfold bounded_def, intro allI impI)

  fix k

  assume live: "k < slots + pages"

  show "ptable (promote pages slots source s) k < frontier (promote pages slots source s)"

  proof (cases "slots \<le> k")

    case True

    have selected: "source + (k - slots) < slots + pages"

      using source live True by arith

    show ?thesis

      using bounded_frame[OF bounds selected] live True by (simp add: promote_def)

  next

    case False

    show ?thesis

      using bounded_frame[OF bounds live] False by (simp add: promote_def)

  qed

qed

lemma promotion_exclusive:

  assumes owned: "exclusive (slots + pages) s" and source: "source + pages \<le> slots"

  shows "exclusive (slots + pages) (promote pages slots source s)"

proof (unfold exclusive_def, intro allI impI)

  fix k j

  assume live: "k < slots + pages" "j < slots + pages"

    and access: "writable (promote pages slots source s) k"

    and sharing: "ptable (promote pages slots source s) j = ptable (promote pages slots source s) k"

  have writable: "writable s k" and outside: "\<not> (source \<le> k \<and> k < source + pages)"

    and old: "ptable (promote pages slots source s) k = ptable s k"

    using access by (auto simp: promote_def)

  show "j = k"

  proof (cases "slots \<le> j")

    case True

    have selected: "source + (j - slots) < slots + pages"

      and inside: "source \<le> source + (j - slots) \<and> source + (j - slots) < source + pages"

      using source live True by arith+

    have frame: "ptable s (source + (j - slots)) = ptable s k"

      using sharing old live True by (simp add: promote_def)

    have "source + (j - slots) = k"

      using writable_unique[OF owned live(1) selected writable frame] .

    then show ?thesis using inside outside by simp

  next

    case False

    have "ptable s j = ptable s k"

      using sharing old False by (simp add: promote_def)

    then show ?thesis

      using writable_unique[OF owned live writable] by simp

  qed

qed

theorem promotion_invariant:

  "invariant (slots + pages) s \<Longrightarrow> source + pages \<le> slots \<Longrightarrow>

   invariant (slots + pages) (promote pages slots source s)"

  by (simp add: invariant_def promotion_bounded promotion_exclusive)

theorem promotion_preserves_unselected:

  assumes "k < slots" "k < source \<or> source + pages \<le> k"

  shows "view (promote pages slots source s) k = view s k \<and>

    writable (promote pages slots source s) k = writable s k"

  using assms by (auto simp: promote_def view_def)

theorem promotion_store_preserves_unselected:

  assumes inv: "invariant (slots + pages) s" and source: "source + pages \<le> slots"

    and page: "p < pages" and live: "k < slots"

    and unselected: "k < source \<or> source + pages \<le> k"

  shows "view (store (promote pages slots source s) (source + p) offset byte) k = view s k"

proof -

  have selected: "source + p < slots + pages" and other: "k \<noteq> source + p"

    using source page live unselected by arith+

  show ?thesis

    using write_other[OF promotion_invariant[OF inv source] selected _ other] live

    by (simp add: promotion_live_view)

qed

theorem promotion_store_preserves_baseline:

  assumes inv: "invariant (slots + pages) s" and source: "source + pages \<le> slots"

    and pages: "p < pages" "q < pages"

  shows "view (store (promote pages slots source s) (source + p) offset byte) (slots + q) =

    view s (source + q)"

proof -

  have selected: "source + p < slots + pages" and baseline: "slots + q < slots + pages"

    and other: "slots + q \<noteq> source + p"

    using source pages by arith+

  show ?thesis

    using write_other[OF promotion_invariant[OF inv source] selected baseline other]

    by (simp add: promotion_baseline_view pages)

qed

end