refactor: make CompactedRegion serializable (#13984)

This PR reshapes `CompactedRegion` from a bare `USize` pointer into a
structure whose `filePath`, `size`, `isMemoryMapped`, and `depPaths` are
ordinary Lean values, with the logical base address, a root-relative
buffer offset, and a pointer to the region's root object kept in private
fields. Because the metadata is now plain Lean data and the root pointer
is an ordinary pointer into the region rather than an opaque handle, a
`CompactedRegion` (and thus `Environment`) can be embedded in compacted
data: as long as the region is also supplied in `depRegions`, the object
compactor relocates the pointer like any other cross-region reference
and it is re-resolved against the freshly mapped buffer on load.

The region's buffer is no longer owned by a C++ struct. The former
`compacted_region` becomes `region_reader`, a transient non-owning
read-context that fixes up a just-mapped buffer and is then discarded;
cross-region dependencies are passed as a lightweight `region_view`
value (begin/size/base_addr) rather than a pointer. The Lean
`CompactedRegion` owns the mapping, framed by its whole file (base
address, root-to-base offset, file size), and `CompactedRegion.free`
releases it directly via `munmap`/`free`; `free` first neutralizes the
root pointer so that decrementing any surviving reference to the freed
structure does not dereference released memory. The former
`lean_compacted_region_{size,is_memory_mapped}` accessors become
structure projections, and `read` populates all fields at load time.

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: Kha

src/Lean/CompactedRegion.lean

@@ -16,21 +16,43 @@ A compacted region holds multiple Lean objects in a contiguous memory region, wh
 read/written to/from disk. Objects inside the region do not have reference counters and cannot be
 freed individually. The contents of `.olean` files are compacted regions.
 -/
-@[expose] public def CompactedRegion := USize
-
-@[extern "lean_compacted_region_is_memory_mapped"]
-public opaque CompactedRegion.isMemoryMapped : CompactedRegion → Bool
-
-/-- Size in bytes. -/
-@[extern "lean_compacted_region_size"]
-public opaque CompactedRegion.size : CompactedRegion → USize
-
-/--
-Frees a compacted region and its contents. No live references to the contents may exist at the
-time of invocation.
+/-
+This structure carries the region's loading metadata (`filePath`, `size`, ...) as plain Lean values
+plus a private `root` pointer to the region's root object. Because `root` is an ordinary pointer
+into the buffer rather than an opaque external handle, embedding a `CompactedRegion` in compacted
+data is sound as long as the region is supplied as one of the `depRegions`: the object compactor
+then relocates `root` like any other cross-region pointer, and it is re-resolved against the freshly
+mapped buffer on load.
 -/
-@[extern "lean_compacted_region_free"]
-public unsafe opaque CompactedRegion.free : CompactedRegion → IO Unit
+public structure CompactedRegion where
+  /-- Path the region was loaded from. -/
+  filePath       : System.FilePath
+  /-- Size in bytes of the region's mapping (the backing `.olean` file). -/
+  size           : USize
+  /-- Whether the region's buffer is backed by a memory mapping of its file. -/
+  isMemoryMapped : Bool
+  /--
+  Paths of the dep regions this region depends on, recorded at load time so a consumer can re-open
+  them after a snapshot round-trip.
+  -/
+  depPaths       : Array System.FilePath
+  /--
+  Logical base address the region's mapping is relative to (`olean_header.base_addr`), used to
+  translate cross-region pointers when this region is used as a dependency.
+  -/
+  private baseAddr     : USize
+  /--
+  Byte offset of the region's root object from the start of the mapping; `root - bufferOffset`
+  recovers the mapping base (the address to unmap/free and the start of the dependency range).
+  -/
+  private bufferOffset : USize
+  /--
+  Pointer to the region's root object. A plain pointer into the data buffer (not an external handle),
+  so the object compactor relocates it as a cross-region pointer when the region is embedded in
+  compacted data with itself supplied as a `depRegion`.
+  -/
+  private root         : NonScalar
+  deriving Nonempty
 
 opaque CompactorSpec : NonemptyType.{0}
 /--
@@ -44,6 +66,13 @@ subsequent saves will dereference dangling pointers.
 -/
 public def Compactor := CompactorSpec.type
 
+/--
+Frees a compacted region and its contents. No live references to the contents may exist at the
+time of invocation.
+-/
+@[extern "lean_compacted_region_free"]
+public unsafe opaque CompactedRegion.free (region : CompactedRegion) : IO Unit
+
 /--
 Saves arbitrary data to a compacted region on disk.
 

src/library/module.cpp

@@ -165,7 +165,7 @@ static void ensure_compactor_class() {
     }
 }
 
-static lean_object * mk_compactor(void * base_addr, std::vector<compacted_region *> dep_regions,
+static lean_object * mk_compactor(void * base_addr, std::vector<region_view> dep_regions,
                                   bool allow_closures) {
     ensure_compactor_class();
     return lean_alloc_external(g_compactor_class,
@@ -176,14 +176,32 @@ static object_compactor * to_compactor(lean_object * o) {
     return static_cast<object_compactor *>(lean_get_external_data(o));
 }
 
-// Extract `compacted_region *` pointers from an `Array CompactedRegion`.
-static std::vector<compacted_region *> extract_dep_regions(b_obj_arg odep_regions) {
-    std::vector<compacted_region *> result;
+// Field layout of the Lean `CompactedRegion` structure (see `Lean/CompactedRegion.lean`). A region
+// is identified with its whole mapping: object fields 0 = `filePath`, 1 = `depPaths`, 2 = `root`
+// (a `NonScalar` pointer to the root object); usize slots 3..5 = `size` (mapping size), `baseAddr`
+// (logical mapping base), `bufferOffset` (`root - mappingBase`); a uint8 `isMemoryMapped` at byte
+// offset `sizeof(void*) * 6`.
+static char * region_root(b_obj_arg r)      { return reinterpret_cast<char *>(lean_ctor_get(r, 2)); }
+static size_t region_size(b_obj_arg r)      { return lean_ctor_get_usize(r, 3); }
+static size_t region_base_addr(b_obj_arg r) { return lean_ctor_get_usize(r, 4); }
+// `root` may legitimately sit below the mapping base (its object can be deduplicated into a
+// lower-addressed dep), making `bufferOffset` "negative"; recover the base in integer space so the
+// wrap is defined rather than UB pointer arithmetic.
+static char * region_buffer(b_obj_arg r) {
+    return reinterpret_cast<char *>(reinterpret_cast<uintptr_t>(region_root(r)) - lean_ctor_get_usize(r, 5));
+}
+
+// Extract address-range views from an `Array CompactedRegion` for cross-region pointer relocation.
+// The view spans the whole mapping (`[buffer, buffer + size)` at logical `baseAddr`); since pointers
+// only ever target objects in the data section, the header/trailer slack is harmless.
+static std::vector<region_view> extract_dep_regions(b_obj_arg odep_regions) {
+    std::vector<region_view> result;
     size_t n = lean_array_size(odep_regions);
     result.reserve(n);
     for (size_t i = 0; i < n; i++) {
-        result.push_back(reinterpret_cast<compacted_region *>(
-            lean_unbox_usize(lean_array_get_core(odep_regions, i))));
+        b_obj_arg r = lean_array_get_core(odep_regions, i);
+        result.push_back({ region_buffer(r), region_size(r),
+                           reinterpret_cast<void *>(region_base_addr(r)) });
     }
     return result;
 }
@@ -274,7 +292,7 @@ extern "C" LEAN_EXPORT object * lean_compacted_region_save(b_obj_arg ofname, b_o
         // so reserve a bit of space for them (0x7fff...-0x7f00... = 1TB).
         base_addr = base_addr % 0x7f0000000000;
         base_addr = base_addr & ~(ALIGN - 1);
-        std::vector<compacted_region *> dep_regions = extract_dep_regions(odep_regions);
+        std::vector<region_view> dep_regions = extract_dep_regions(odep_regions);
         cs_obj = object_ref(mk_compactor(reinterpret_cast<void *>(base_addr),
                                          std::move(dep_regions), allow_closures));
     }
@@ -412,6 +430,29 @@ extern "C" LEAN_EXPORT object * lean_compacted_region_save(b_obj_arg ofname, b_o
     return io_result_mk_ok(cs_obj.steal());
 }
 
+static object * mk_compacted_region(b_obj_arg ofname, b_obj_arg odep_regions, object * root,
+                                    char * buffer, size_t base_addr, size_t full_sz, bool is_mmap) {
+    size_t n = lean_array_size(odep_regions);
+    object * dep_paths = lean_alloc_array(n, n);
+    for (size_t i = 0; i < n; i++) {
+        object * dep_file_path = lean_ctor_get(lean_array_get_core(odep_regions, i), 0);
+        lean_inc(dep_file_path);
+        lean_array_set_core(dep_paths, i, dep_file_path);
+    }
+    object * r = lean_alloc_ctor(0, 3, sizeof(size_t) * 3 + 1);
+    lean_inc(ofname);
+    lean_ctor_set(r, 0, ofname);
+    lean_ctor_set(r, 1, dep_paths);
+    lean_ctor_set(r, 2, root);
+    lean_ctor_set_usize(r, 3, full_sz);
+    lean_ctor_set_usize(r, 4, base_addr);
+    // Integer subtraction: `root` may be below `buffer` (see `region_buffer`), and the two can be
+    // unrelated allocations, so a pointer subtraction would be UB.
+    lean_ctor_set_usize(r, 5, reinterpret_cast<uintptr_t>(root) - reinterpret_cast<uintptr_t>(buffer));
+    lean_ctor_set_uint8(r, sizeof(void*) * 6, is_mmap ? 1 : 0);
+    return r;
+}
+
 // Implements `Lean.CompactedRegion.read`. Loads a compacted region from disk. `odep_regions`
 // carries `CompactedRegion`s whose address ranges must be known to resolve cross-region pointers
 // in this file. Returns `(α × CompactedRegion)`, where `α` is the type the Lean caller asks the
@@ -420,8 +461,8 @@ extern "C" LEAN_EXPORT object * lean_compacted_region_save(b_obj_arg ofname, b_o
 // Supports both `v2` and `v3` formats.
 extern "C" LEAN_EXPORT object * lean_compacted_region_read(b_obj_arg ofname, b_obj_arg odep_regions, object *) {
     std::string olean_fn(lean_string_cstr(ofname));
-    std::vector<compacted_region *> dep_regions = extract_dep_regions(odep_regions);
     try {
+        std::vector<region_view> dep_regions = extract_dep_regions(odep_regions);
 #ifdef LEAN_WINDOWS
         HANDLE h_file = CreateFile(olean_fn.c_str(), GENERIC_READ, FILE_SHARE_READ | FILE_SHARE_DELETE, NULL, OPEN_EXISTING, FILE_ATTRIBUTE_NORMAL, NULL);
         if (h_file == INVALID_HANDLE_VALUE) {
@@ -467,9 +508,8 @@ extern "C" LEAN_EXPORT object * lean_compacted_region_read(b_obj_arg ofname, b_o
 
         char * buffer = nullptr;
         bool is_mmap = false;
-        std::function<void()> free_data;
 
-        // Map file COW-writable. The fallback walk in `compacted_region::read()` writes
+        // Map file COW-writable. The fallback walk in `region_reader::read()` writes
         // fixed pointers back into the region's memory when any dep region didn't land at its
         // saved `base_addr`, so the mapping must be writable. `v3` files additionally patch
         // closure fn pointers in place. Unwritten pages remain shared with the page cache under
@@ -485,7 +525,6 @@ extern "C" LEAN_EXPORT object * lean_compacted_region_read(b_obj_arg ofname, b_o
             lean_always_assert(CloseHandle(h_map));
             if (buffer && buffer == base_addr) {
                 is_mmap = true;
-                free_data = [=]() { lean_always_assert(UnmapViewOfFile(base_addr)); };
             } else if (buffer) {
                 lean_always_assert(UnmapViewOfFile(buffer));
                 buffer = nullptr;
@@ -505,7 +544,6 @@ extern "C" LEAN_EXPORT object * lean_compacted_region_read(b_obj_arg ofname, b_o
             mmap_flags, fd.get(), 0));
         if (buffer != MAP_FAILED && buffer == base_addr) {
             is_mmap = true;
-            free_data = [=]() { lean_always_assert(munmap(buffer, size) == 0); };
         } else {
             if (buffer != MAP_FAILED) munmap(buffer, size);
             buffer = nullptr;
@@ -521,9 +559,16 @@ extern "C" LEAN_EXPORT object * lean_compacted_region_read(b_obj_arg ofname, b_o
                 free(buffer);
                 return io_result_mk_error((sstream() << "failed to read file '" << olean_fn << "'").str());
             }
-            char * buf = buffer;
-            size_t sz = size;
-            free_data = [=]() { free_sized(buf, sz); };
+            // The buffer outlives this call (its lifetime is the Lean `CompactedRegion`'s, freed by
+            // `lean_compacted_region_free`). It is only reached through interior pointers (the
+            // region's `root` and the objects read out of it), and a persistent/`leakEnv` region is
+            // never freed at all, so tell LeakSanitizer not to report it. Under `mmap` (the common
+            // path) the buffer is not a heap allocation and needs no such treatment.
+#if defined(__has_feature)
+#if __has_feature(address_sanitizer)
+            __lsan_ignore_object(buffer);
+#endif
+#endif
         }
 
         // v3 format, default data otherwise
@@ -552,24 +597,44 @@ extern "C" LEAN_EXPORT object * lean_compacted_region_read(b_obj_arg ofname, b_o
             }
         }
 
-        compacted_region * region = new compacted_region(
+        region_reader reader(
             data_section_sz, buffer + data_section_off,
-            base_addr + data_section_off, is_mmap, free_data,
+            base_addr + data_section_off,
             std::move(dep_regions),
             std::move(lib_relocs), std::move(closure_offsets));
-#if defined(__has_feature)
-#if __has_feature(address_sanitizer)
-        __lsan_ignore_object(region);
-#endif
-#endif
-        object * mod = region->read();
+        object * mod = reader.read();
         object * pair = alloc_cnstr(0, 2, 0);
         cnstr_set(pair, 0, mod);
-        cnstr_set(pair, 1, box_size_t(reinterpret_cast<size_t>(region)));
+        // The Lean region is framed by its whole mapping (`buffer`, `base_addr` = the mapped-at
+        // logical address, `size` = the file size), not the inner data section.
+        cnstr_set(pair, 1, mk_compacted_region(ofname, odep_regions, mod,
+            buffer, reinterpret_cast<size_t>(base_addr), size, is_mmap));
         return io_result_mk_ok(pair);
     } catch (exception & ex) {
         return io_result_mk_error((sstream() << "failed to read '" << olean_fn << "': " << ex.what()).str());
     }
 }
 
+extern "C" LEAN_EXPORT obj_res lean_compacted_region_free(obj_arg region, object *) {
+    char * buffer = region_buffer(region);
+    size_t full_sz = region_size(region);
+    bool is_mmap = lean_ctor_get_uint8(region, sizeof(void*) * 6) != 0;
+    // `root` points into the buffer we are about to release. Overwrite it with a scalar so that
+    // decrementing this structure now, or any reference to it that outlives the `free` (e.g. one
+    // still sitting in `env.header.regions`), does not dereference freed memory. The old value is a
+    // refcount-free buffer object, so it needs no decrement.
+    lean_ctor_set(region, 2, lean_box(0));
+    lean_dec_ref(region);
+    if (is_mmap) {
+#ifdef LEAN_WINDOWS
+        lean_always_assert(UnmapViewOfFile(buffer));
+#else
+        lean_always_assert(munmap(buffer, full_sz) == 0);
+#endif
+    } else {
+        free_sized(buffer, full_sz);
+    }
+    return lean_io_result_mk_ok(lean_box(0));
+}
+
 }