From 087436dffa8c479396bd36f7908df837ba49f487 Mon Sep 17 00:00:00 2001
From: james <j@cpl0.zip>
Date: Thu, 14 May 2026 20:37:00 +0100
Subject: [PATCH] feat(isolation): refine shared storage to private byte
 memories

---
 Isolation.thy | 89 +++++++++++++++++++++++++++++++++++++++++++++++++++
 ROOT          |  1 +
 2 files changed, 90 insertions(+)
 create mode 100644 Isolation.thy

diff --git a/Isolation.thy b/Isolation.thy
new file mode 100644
index 0000000..d3d7c29
--- /dev/null
+++ b/Isolation.thy
@@ -0,0 +1,89 @@
+theory Isolation
+  imports Model
+begin
+
+lemma write_target:
+  assumes "bounded n s" "k < n"
+  shows "view (store s k offset byte) k = (view s k)(offset := byte)"
+  using prepare_view[OF assms, of k]
+  by (simp add: view_def store_def Let_def)
+
+lemma write_other:
+  assumes inv: "invariant n s" and valid: "k < n" "j < n" and different: "j \<noteq> k"
+  shows "view (store s k offset byte) j = view s j"
+proof -
+  have prepared: "invariant n (prepare s k)"
+    using inv by (rule prepare_invariant)
+  have distinct: "ptable (prepare s k) j \<noteq> ptable (prepare s k) k"
+    using writable_unique[of n "prepare s k" k j] prepared valid different
+    by (auto simp: invariant_def)
+  have preserved: "view (prepare s k) j = view s j"
+    using prepare_view[of n s j k] inv valid by (auto simp: invariant_def)
+  show ?thesis
+    using distinct preserved by (simp add: store_def view_def Let_def)
+qed
+
+theorem write_refinement:
+  assumes "invariant n s" "k < n" "j < n"
+  shows "view (store s k offset byte) j =
+    (if j = k then (view s k)(offset := byte) else view s j)"
+  using assms write_target write_other by (auto simp: invariant_def)
+
+corollary read_after_write:
+  "invariant n s \<Longrightarrow> k < n \<Longrightarrow>
+   view (store s k offset byte) k offset = byte"
+  using write_refinement[of n s k k offset byte] by simp
+
+corollary other_offset:
+  "invariant n s \<Longrightarrow> k < n \<Longrightarrow> address \<noteq> offset \<Longrightarrow>
+   view (store s k offset byte) k address = view s k address"
+  using write_refinement[of n s k k offset byte] by simp
+
+definition reference_write :: "memory \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> memory" where
+  "reference_write m k offset byte = m(k := (m k)(offset := byte))"
+
+definition represents :: "nat \<Rightarrow> pager \<Rightarrow> memory \<Rightarrow> bool" where
+  "represents n s m \<longleftrightarrow> (\<forall>k<n. view s k = m k)"
+
+lemma represents_initial:
+  "represents n (initial pages contents) (\<lambda>k. contents (k mod pages))"
+  by (simp add: represents_def)
+
+theorem simulation:
+  assumes "invariant n s" "represents n s m" "k < n"
+  shows "represents n (store s k offset byte) (reference_write m k offset byte)"
+  using assms write_refinement[of n s k]
+  by (auto simp: represents_def reference_write_def)
+
+lemma prepared_exclusive:
+  "invariant n s \<Longrightarrow> k < n \<Longrightarrow> j < n \<Longrightarrow> j \<noteq> k \<Longrightarrow>
+   ptable (prepare s k) j \<noteq> ptable (prepare s k) k"
+  using prepare_invariant writable_unique prepare_writable
+  unfolding invariant_def by blast
+
+lemma writable_no_copy:
+  "writable s k \<Longrightarrow> frontier (store s k offset byte) = frontier s"
+  by (simp add: prepare_def)
+
+lemma readonly_one_copy:
+  "\<not> writable s k \<Longrightarrow> frontier (store s k offset byte) = Suc (frontier s)"
+  by (simp add: prepare_def)
+
+lemma subsequent_write_no_copy:
+  "frontier (store (store s k a x) k b y) = frontier (store s k a x)"
+  by (rule writable_no_copy) simp
+
+lemma write_writable_target [simp]: "writable (store s k offset byte) k"
+  by simp
+
+lemma write_writable_other:
+  "j \<noteq> k \<Longrightarrow> writable (store s k offset byte) j = writable s j"
+  by (simp add: prepare_def)
+
+lemma write_preserves_unallocated:
+  "f > frontier s \<Longrightarrow> physical (store s k offset byte) f = physical s f"
+  if "bounded n s" "k < n" for f s k n offset byte
+  using that bounded_frame[OF that]
+  by (auto simp: store_def prepare_def detach_def Let_def split: if_splits)
+
+end
diff --git a/ROOT b/ROOT
index 913da45..0ab5054 100644
--- a/ROOT
+++ b/ROOT
@@ -2,3 +2,4 @@ session Split = HOL +
   options [document = false]
   theories
     Model
+    Isolation