From d5ec9d43bb40f942cd275ec0d52561516d6446ea Mon Sep 17 00:00:00 2001
From: james <j@cpl0.zip>
Date: Wed, 15 Jul 2026 19:52:00 +0100
Subject: [PATCH] feat(export): export checked pager transitions as executable
 ocaml

---
 Export.thy | 16 ++++++++++++++++
 ROOT       |  1 +
 2 files changed, 17 insertions(+)
 create mode 100644 Export.thy

diff --git a/Export.thy b/Export.thy
new file mode 100644
index 0000000000000000000000000000000000000000..49c4abeeb9f8c4a0f992403a7c27e761662304cd
--- /dev/null
+++ b/Export.thy
@@ -0,0 +1,16 @@
+theory Export
+  imports Reuse
+begin
+
+definition seed :: memory where
+  "seed frame offset = (frame * 17 + offset) mod 256"
+
+definition boot :: pager where "boot = initial 4 seed"
+
+definition read_byte :: "pager \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
+  "read_byte s k offset = view s k offset"
+
+export_code boot initial read_byte checked frontier ptable writable prepare reserve reclaim
+  Read Write Suc in OCaml module_name Split file_prefix split
+
+end
diff --git a/ROOT b/ROOT
index 83b28d453f5f9c4e98e510fb3751fe9711e74106..41710389e544d66e21102bb5ad95f05defd708ff 100644
--- a/ROOT
+++ b/ROOT
@@ -7,3 +7,4 @@ session Split = HOL +
     Protocol
     Snapshot
     Reuse
+    Export