From f044a95a6ba71c8d90a5222c81c63ce5da190372 Mon Sep 17 00:00:00 2001 From: james Date: Mon, 2 Nov 2026 02:49:18 +0000 Subject: [PATCH] feat(snapshot): prove promotion preserves unselected snapshot contents --- README.md | 4 +- proof/Snapshot.thy | 113 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 116 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 099edb7..635c090 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,5 @@ 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 + diff --git a/proof/Snapshot.thy b/proof/Snapshot.thy index aaf760f..057b2df 100644 --- a/proof/Snapshot.thy +++ b/proof/Snapshot.thy @@ -70,4 +70,117 @@ corollary original_preserved: physical (execute (initial pages contents) actions) f = contents f" using execute_original[OF initial_private] by simp +definition promote :: "nat \ nat \ nat \ pager \ pager" where + "promote pages slots source s = + s\ptable := (\k. if slots \ k \ k < slots + pages + then ptable s (source + (k - slots)) else ptable s k), + writable := (\k. writable s k \ \ (source \ k \ k < source + pages) + \ \ (slots \ k \ k < slots + pages))\" + +lemma promotion_live_view: + "k < slots \ view (promote pages slots source s) k = view s k" + by (simp add: promote_def view_def) + +lemma promotion_baseline_view: + "p < pages \ + 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 \ \ writable (promote pages slots source s) (slots + p)" + by (simp add: promote_def) + +lemma promotion_source_readonly: + "p < pages \ \ 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 \ 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 \ 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 \ 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: "\ (source \ k \ 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 \ j") + case True + have selected: "source + (j - slots) < slots + pages" + and inside: "source \ source + (j - slots) \ 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 \ source + pages \ slots \ + 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 \ source + pages \ k" + shows "view (promote pages slots source s) k = view s k \ + 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 \ slots" + and page: "p < pages" and live: "k < slots" + and unselected: "k < source \ source + pages \ 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 \ 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 \ 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 \ 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