From b1b249cd6fbbce57ed295d729b9efc69513686bd Mon Sep 17 00:00:00 2001
From: james <j@cpl0.zip>
Date: Thu, 15 Oct 2026 11:24:17 +0100
Subject: [PATCH] feat(core): define typed addresses and captured register
 state

---
 .gitignore      |   4 ++
 dune-project    |   8 ++++
 lib/address.ml  |  33 ++++++++++++++++
 lib/address.mli |  25 ++++++++++++
 lib/dune        |   4 ++
 lib/model.ml    | 101 ++++++++++++++++++++++++++++++++++++++++++++++++
 scope.opam      |  23 +++++++++++
 7 files changed, 198 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 dune-project
 create mode 100644 lib/address.ml
 create mode 100644 lib/address.mli
 create mode 100644 lib/dune
 create mode 100644 lib/model.ml
 create mode 100644 scope.opam

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..f9d3625
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,4 @@
+_build/
+*.install
+guest/build/
+__pycache__/
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000..abd2943
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,8 @@
+(lang dune 3.10)
+(name scope)
+(version 0.1.0)
+(generate_opam_files true)
+(package
+ (name scope)
+ (synopsis "Inspect and replay Xen guest page tables")
+ (depends (ocaml (>= 4.14)) dune))
diff --git a/lib/address.ml b/lib/address.ml
new file mode 100644
index 0000000..8aa0a2b
--- /dev/null
+++ b/lib/address.ml
@@ -0,0 +1,33 @@
+module Virtual = struct
+  type t = int64
+  let of_int64 x = x
+  let to_int64 x = x
+end
+
+module Physical = struct
+  type t = int64
+  let of_int64 x = x
+  let to_int64 x = x
+end
+
+module Machine = struct
+  type t = int64
+  let of_int64 x = x
+  let to_int64 x = x
+end
+
+let compare = Int64.unsigned_compare
+let hex x = Printf.sprintf "0x%016Lx" x
+
+let parse s =
+  if String.length s = 0 || s.[0] = '-' || s.[0] = '+' then
+    invalid_arg ("invalid unsigned address: " ^ s);
+  try Int64.of_string (if String.starts_with ~prefix:"0x" s then s else "0u" ^ s)
+  with Failure _ -> invalid_arg ("invalid unsigned address: " ^ s)
+
+let bit x n = Int64.logand x (Int64.shift_left 1L n) <> 0L
+let mask n = Int64.pred (Int64.shift_left 1L n)
+let align x n = Int64.logand x (Int64.lognot (mask n))
+let canonical x =
+  let high = Int64.shift_right x 47 in
+  high = 0L || high = -1L
diff --git a/lib/address.mli b/lib/address.mli
new file mode 100644
index 0000000..a241a45
--- /dev/null
+++ b/lib/address.mli
@@ -0,0 +1,25 @@
+module Virtual : sig
+  type t
+  val of_int64 : int64 -> t
+  val to_int64 : t -> int64
+end
+
+module Physical : sig
+  type t
+  val of_int64 : int64 -> t
+  val to_int64 : t -> int64
+end
+
+module Machine : sig
+  type t
+  val of_int64 : int64 -> t
+  val to_int64 : t -> int64
+end
+
+val compare : int64 -> int64 -> int
+val hex : int64 -> string
+val parse : string -> int64
+val bit : int64 -> int -> bool
+val mask : int -> int64
+val align : int64 -> int -> int64
+val canonical : int64 -> bool
diff --git a/lib/dune b/lib/dune
new file mode 100644
index 0000000..046a103
--- /dev/null
+++ b/lib/dune
@@ -0,0 +1,4 @@
+(library
+ (name scope)
+ (public_name scope)
+ (libraries unix))
diff --git a/lib/model.ml b/lib/model.ml
new file mode 100644
index 0000000..56c01ed
--- /dev/null
+++ b/lib/model.ml
@@ -0,0 +1,101 @@
+type features = { phys_bits : int; nx : bool; gb_pages : bool }
+
+type registers = {
+  cr0 : int64;
+  cr2 : int64;
+  cr3 : int64;
+  cr4 : int64;
+  efer : int64;
+  rflags : int64;
+  rip : int64;
+}
+
+type context = {
+  registers : registers;
+  root_override : int64 option;
+  features : features;
+  source : string;
+  consistency : string;
+  identity : string;
+  domid : int;
+  vcpu : int;
+}
+
+type permissions = { writable : bool; user : bool; executable : bool }
+type access = Read | Write | Execute
+type privilege = Supervisor | User
+type request = { access : access; privilege : privilege; ac : bool }
+
+type step = {
+  level : int;
+  table : Address.Physical.t;
+  index : int;
+  raw : int64;
+  effective : permissions;
+}
+
+type mapping = {
+  virtual_address : Address.Virtual.t;
+  physical_address : Address.Physical.t;
+  size : int64;
+  permissions : permissions;
+  leaf : int64;
+  trace : step list;
+}
+
+type fault = {
+  vector : int;
+  error_code : int;
+  reason : string;
+  level : int option;
+}
+
+type outcome = Mapped of mapping | Fault of fault | Incomplete of string
+type result = { trace : step list; outcome : outcome }
+type reader = Address.Physical.t -> (string, string) Stdlib.result
+
+exception Limit of string
+
+let unrestricted = { writable = true; user = true; executable = true }
+
+let narrow permissions raw = {
+  writable = permissions.writable && Address.bit raw 1;
+  user = permissions.user && Address.bit raw 2;
+  executable = permissions.executable && not (Address.bit raw 63);
+}
+
+let validate context =
+  let r = context.registers and f = context.features in
+  let require predicate reason = if not predicate then invalid_arg reason in
+  require (Sys.word_size = 64) "scope requires a 64-bit runtime";
+  require (f.phys_bits >= 32 && f.phys_bits <= 52) "physical width must be between 32 and 52";
+  require (Address.bit r.cr0 0 && Address.bit r.cr0 31) "protected paging must be enabled";
+  require (Address.bit r.cr4 5 && Address.bit r.efer 10) "only ia-32e paging is supported";
+  require (not (Address.bit r.cr4 12)) "five-level paging is unsupported";
+  require (not (Address.bit r.cr4 22 || Address.bit r.cr4 24)) "protection keys are unsupported";
+  require (not (Address.bit r.cr4 23)) "cet is unsupported";
+  require (not (Address.bit r.cr4 27)) "linear address space separation is unsupported";
+  require (not (Address.bit r.cr4 28)) "supervisor linear address masking is unsupported";
+  require (not (Address.bit r.efer 11) || f.nx) "nxe requires the guest nx feature";
+  let validate_root root =
+    require (Int64.logand root (Int64.lognot (Address.mask f.phys_bits)) = 0L)
+      "cr3 exceeds the physical width or uses unsupported address masking"
+  in
+  validate_root r.cr3;
+  Option.iter validate_root context.root_override;
+  require (context.domid >= 0 && context.vcpu >= 0) "negative domain or vcpu"
+
+let root context = Address.Physical.of_int64
+  (Address.align (Option.value context.root_override ~default:context.registers.cr3) 12)
+let access_name = function Read -> "read" | Write -> "write" | Execute -> "execute"
+let privilege_name = function Supervisor -> "supervisor" | User -> "user"
+
+let context_changes before after =
+  let a = before.registers and b = after.registers in
+  List.filter_map (fun (changed, field) -> if changed then Some field else None) [
+    (a.cr0 <> b.cr0, "cr0"); (a.cr3 <> b.cr3, "cr3"); (a.cr4 <> b.cr4, "cr4");
+    (root before <> root after, "root");
+    (a.efer <> b.efer, "efer"); (Address.bit a.rflags 18 <> Address.bit b.rflags 18, "ac");
+    (before.features.phys_bits <> after.features.phys_bits, "phys_bits");
+    (before.features.nx <> after.features.nx, "nx");
+    (before.features.gb_pages <> after.features.gb_pages, "gb_pages") ]
diff --git a/scope.opam b/scope.opam
new file mode 100644
index 0000000..ed0c2e8
--- /dev/null
+++ b/scope.opam
@@ -0,0 +1,23 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "0.1.0"
+synopsis: "Inspect and replay Xen guest page tables"
+depends: [
+  "ocaml" {>= "4.14"}
+  "dune" {>= "3.10"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]