From 86650c76e96e3766ec12a32d552f12520965f9c2 Mon Sep 17 00:00:00 2001
From: james <j@cpl0.zip>
Date: Tue, 9 Jun 2026 21:08:00 +0100
Subject: [PATCH] feat(protocol): equate fault resolution and retry with atomic
 stores

---
 Protocol.thy | 118 +++++++++++++++++++++++++++++++++++++++++++++++++++
 ROOT         |   1 +
 2 files changed, 119 insertions(+)
 create mode 100644 Protocol.thy

diff --git a/Protocol.thy b/Protocol.thy
new file mode 100644
index 0000000..1a93ea7
--- /dev/null
+++ b/Protocol.thy
@@ -0,0 +1,118 @@
+theory Protocol
+  imports Execution
+begin
+
+definition commit :: "pager \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager" where
+  "commit s k offset byte =
+    s\<lparr>physical := (physical s)(ptable s k := (view s k)(offset := byte))\<rparr>"
+
+definition attempt :: "pager \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager option" where
+  "attempt s k offset byte = (if writable s k then Some (commit s k offset byte) else None)"
+
+lemma readonly_faults:
+  "\<not> writable s k \<Longrightarrow> attempt s k offset byte = None"
+  by (simp add: attempt_def)
+
+lemma writable_commits:
+  "writable s k \<Longrightarrow> attempt s k offset byte = Some (store s k offset byte)"
+  by (simp add: attempt_def commit_def store_def prepare_def)
+
+lemma resolve_preserves_memory:
+  "invariant n s \<Longrightarrow> j < n \<Longrightarrow> view (detach s k) j = view s j"
+  using detach_view[of n s j k] by (auto simp: invariant_def)
+
+theorem fault_retry:
+  "\<not> writable s k \<Longrightarrow>
+   attempt (detach s k) k offset byte = Some (store s k offset byte)"
+  by (simp add: attempt_def commit_def store_def prepare_def detach_def)
+
+theorem fault_retry_refinement:
+  assumes "invariant n s" "represents n s m" "k < n" "\<not> writable s k"
+  obtains t where "attempt (detach s k) k offset byte = Some t"
+    "invariant n t" "represents n t (reference_write m k offset byte)"
+  using assms fault_retry write_invariant simulation by blast
+
+definition dirty :: "nat \<Rightarrow> pager \<Rightarrow> nat set" where
+  "dirty n s = {k. k < n \<and> writable s k}"
+
+lemma finite_dirty [simp]: "finite (dirty n s)"
+  unfolding dirty_def by (rule finite_subset[of _ "{..<n}"]) auto
+
+lemma dirty_initial [simp]: "dirty n (initial pages contents) = {}"
+  by (auto simp: dirty_def)
+
+lemma dirty_member [simp]: "k \<in> dirty n s \<longleftrightarrow> k < n \<and> writable s k"
+  by (simp add: dirty_def)
+
+lemma dirty_store:
+  "k < n \<Longrightarrow> dirty n (store s k offset byte) = insert k (dirty n s)"
+  by (auto simp: dirty_def prepare_def)
+
+definition accounted :: "nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> bool" where
+  "accounted pages slots s \<longleftrightarrow> frontier s = pages + card (dirty slots s)"
+
+lemma initial_accounted: "accounted pages slots (initial pages contents)"
+  by (simp add: accounted_def)
+
+lemma store_accounted:
+  assumes "accounted pages slots s" "k < slots"
+  shows "accounted pages slots (store s k offset byte)"
+  using assms
+  by (auto simp: accounted_def dirty_store prepare_frontier card_insert_if insert_absorb)
+
+lemma advance_accounted:
+  "accounted pages slots s \<Longrightarrow> valid slots bytes a \<Longrightarrow>
+   accounted pages slots (advance s a)"
+  by (cases a; auto intro: store_accounted)
+
+theorem execute_accounted:
+  "accounted pages slots s \<Longrightarrow> list_all (valid slots bytes) actions \<Longrightarrow>
+   accounted pages slots (execute s actions)"
+  by (induction actions arbitrary: s) (auto intro: advance_accounted)
+
+lemma dirty_card_bound: "card (dirty slots s) \<le> slots"
+proof -
+  have "dirty slots s \<subseteq> {..<slots}" by (auto simp: dirty_def)
+  then have "card (dirty slots s) \<le> card {..<slots}"
+    by (intro card_mono) auto
+  then show ?thesis by simp
+qed
+
+theorem allocation_bound:
+  assumes "list_all (valid slots bytes) actions"
+  shows "frontier (execute (initial pages contents) actions) \<le> pages + slots"
+  using execute_accounted[OF initial_accounted assms] dirty_card_bound
+  unfolding accounted_def by fastforce
+
+fun written :: "action list \<Rightarrow> nat set" where
+  "written [] = {}"
+| "written (Read k offset # actions) = written actions"
+| "written (Write k offset byte # actions) = insert k (written actions)"
+
+lemma writable_advance:
+  "writable (advance s a) k = (writable s k \<or> k \<in> written [a])"
+  by (cases a; auto simp: prepare_def)
+
+theorem written_exactly:
+  "writable (execute s actions) k = (writable s k \<or> k \<in> written actions)"
+proof (induction actions arbitrary: s)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons a actions)
+  show ?case by (cases a) (auto simp: Cons.IH prepare_def)
+qed
+
+theorem copies_exactly:
+  assumes "list_all (valid slots bytes) actions"
+  shows "frontier (execute (initial pages contents) actions) =
+    pages + card ({..<slots} \<inter> written actions)"
+proof -
+  have "dirty slots (execute (initial pages contents) actions) =
+      {..<slots} \<inter> written actions"
+    by (auto simp: dirty_def written_exactly)
+  then show ?thesis
+    using execute_accounted[OF initial_accounted assms] by (simp add: accounted_def)
+qed
+
+end
diff --git a/ROOT b/ROOT
index c146703..487b9fd 100644
--- a/ROOT
+++ b/ROOT
@@ -4,3 +4,4 @@ session Split = HOL +
     Model
     Isolation
     Execution
+    Protocol