diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs
index 8d7192c1b0fd1..f87b6bbfcfb26 100644
--- a/library/core/src/ptr/mod.rs
+++ b/library/core/src/ptr/mod.rs
@@ -63,11 +63,39 @@
 //!
 //! ## Allocated object
 //!
-//! For several operations, such as [`offset`] or field projections (`expr.field`), the notion of an
-//! "allocated object" becomes relevant. An allocated object is a contiguous region of memory.
-//! Common examples of allocated objects include stack-allocated variables (each variable is a
-//! separate allocated object), heap allocations (each allocation created by the global allocator is
-//! a separate allocated object), and `static` variables.
+//! An *allocated object* is a subset of program memory which is addressable
+//! from Rust, and within which pointer arithmetic is possible. Examples of
+//! allocated objects include heap allocations, stack-allocated variables,
+//! statics, and consts. The safety preconditions of some Rust operations -
+//! such as `offset` and field projections (`expr.field`) - are defined in
+//! terms of the allocated objects on which they operate.
+//!
+//! An allocated object has a base address, a size, and a set of memory
+//! addresses. It is possible for an allocated object to have zero size, but
+//! such an allocated object will still have a base address. The base address
+//! of an allocated object is not necessarily unique. While it is currently the
+//! case that an allocated object always has a set of memory addresses which is
+//! fully contiguous (i.e., has no "holes"), there is no guarantee that this
+//! will not change in the future.
+//!
+//! For any allocated object with `base` address, `size`, and a set of
+//! `addresses`, the following are guaranteed:
+//! - For all addresses `a` in `addresses`, `a` is in the range `base .. (base +
+//!   size)` (note that this requires `a < base + size`, not `a <= base + size`)
+//! - `base` is not equal to [`null()`] (i.e., the address with the numerical
+//!   value 0)
+//! - `base + size <= usize::MAX`
+//! - `size <= isize::MAX`
+//!
+//! As a consequence of these guarantees, given any address `a` within the set
+//! of addresses of an allocated object:
+//! - It is guaranteed that `a - base` does not overflow `isize`
+//! - It is guaranteed that `a - base` is non-negative
+//! - It is guaranteed that, given `o = a - base` (i.e., the offset of `a` within
+//!   the allocated object), `base + o` will not wrap around the address space (in
+//!   other words, will not overflow `usize`)
+//!
+//! [`null()`]: null
 //!
 //! # Strict Provenance
 //!