feat(snapshot): preserve source frames across valid edit traces

ROOT

@@ -5,3 +5,4 @@ session Split = HOL +
     Isolation
     Execution
     Protocol
+    Snapshot

Snapshot.thy

@@ -0,0 +1,73 @@
+theory Snapshot
+  imports Protocol
+begin
+
+definition private_frames :: "nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> bool" where
+  "private_frames pages slots s \<longleftrightarrow> pages \<le> frontier s \<and>
+    (\<forall>k<slots. writable s k \<longrightarrow> pages \<le> ptable s k)"
+
+lemma initial_private: "private_frames pages slots (initial pages contents)"
+  by (simp add: private_frames_def)
+
+lemma prepare_private:
+  "private_frames pages slots s \<Longrightarrow> private_frames pages slots (prepare s k)"
+  by (auto simp: private_frames_def prepare_def split: if_splits)
+
+lemma prepared_frame_private:
+  "private_frames pages slots s \<Longrightarrow> k < slots \<Longrightarrow>
+   pages \<le> ptable (prepare s k) k"
+  by (auto simp: private_frames_def prepare_def)
+
+lemma store_private:
+  "private_frames pages slots s \<Longrightarrow> private_frames pages slots (store s k offset byte)"
+  using prepare_private[of pages slots s k]
+  by (simp add: private_frames_def)
+
+lemma prepare_original:
+  "private_frames pages slots s \<Longrightarrow> f < pages \<Longrightarrow>
+   physical (prepare s k) f = physical s f"
+  by (auto simp: private_frames_def prepare_def detach_def)
+
+theorem store_original:
+  assumes owned: "private_frames pages slots s" and valid: "k < slots" and original: "f < pages"
+  shows "physical (store s k offset byte) f = physical s f"
+proof -
+  have distinct: "f \<noteq> ptable (prepare s k) k"
+    using prepared_frame_private[OF owned valid] original by arith
+  have preserved: "physical (prepare s k) f = physical s f"
+    using prepare_original[OF owned original] .
+  show ?thesis
+    using distinct preserved by (simp add: store_def Let_def)
+qed
+
+lemma advance_private:
+  "private_frames pages slots s \<Longrightarrow> private_frames pages slots (advance s a)"
+  by (cases a; simp add: store_private)
+
+lemma advance_original:
+  "private_frames pages slots s \<Longrightarrow> valid slots bytes a \<Longrightarrow> f < pages \<Longrightarrow>
+   physical (advance s a) f = physical s f"
+  by (cases a; auto intro: store_original)
+
+theorem execute_original:
+  "private_frames pages slots s \<Longrightarrow> list_all (valid slots bytes) actions \<Longrightarrow>
+   f < pages \<Longrightarrow> physical (execute s actions) f = physical s f"
+proof (induction actions arbitrary: s)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons a actions)
+  have state: "private_frames pages slots (advance s a)"
+    using Cons.prems by (simp add: advance_private)
+  have tail: "physical (execute (advance s a) actions) f = physical (advance s a) f"
+    using Cons.IH[OF state] Cons.prems by simp
+  show ?case
+    using tail advance_original Cons.prems by auto
+qed
+
+corollary original_preserved:
+  "list_all (valid slots bytes) actions \<Longrightarrow> f < pages \<Longrightarrow>
+   physical (execute (initial pages contents) actions) f = contents f"
+  using execute_original[OF initial_private] by simp
+
+end