diff --git a/cranelift/codegen/src/egraph.rs b/cranelift/codegen/src/egraph.rs
index fd89743951b..3f526044356 100644
--- a/cranelift/codegen/src/egraph.rs
+++ b/cranelift/codegen/src/egraph.rs
@@ -347,6 +347,7 @@ where
                     let orig_result = *o.get();
                     // Hit in GVN map -- reuse value.
                     self.value_to_opt_value[result] = orig_result;
+                    self.func.dfg.merge_facts(orig_result, result);
                     self.eclasses.union(orig_result, result);
                     trace!(" -> merges result {} to {}", result, orig_result);
                     true
diff --git a/cranelift/codegen/src/ir/mod.rs b/cranelift/codegen/src/ir/mod.rs
index 396f245a23f..4238abb198b 100644
--- a/cranelift/codegen/src/ir/mod.rs
+++ b/cranelift/codegen/src/ir/mod.rs
@@ -56,7 +56,7 @@ pub use crate::ir::layout::Layout;
 pub use crate::ir::libcall::{get_probestack_funcref, LibCall};
 pub use crate::ir::memflags::{Endianness, MemFlags};
 pub use crate::ir::memtype::{MemoryTypeData, MemoryTypeField};
-pub use crate::ir::pcc::{BaseExpr, Expr, Fact, FactContext, PccError, PccResult};
+pub use crate::ir::pcc::{Expr, Fact, FactContext, PccError, PccResult};
 pub use crate::ir::progpoint::ProgramPoint;
 pub use crate::ir::sourceloc::RelSourceLoc;
 pub use crate::ir::sourceloc::SourceLoc;
diff --git a/cranelift/codegen/src/ir/pcc.rs b/cranelift/codegen/src/ir/pcc.rs
index 33a515cac67..ae30d3e6631 100644
--- a/cranelift/codegen/src/ir/pcc.rs
+++ b/cranelift/codegen/src/ir/pcc.rs
@@ -47,6 +47,10 @@
 //!
 //! TODO:
 //!
+//! Correctness:
+//! - Underflow/overflow: clear min and max respectively on all adds
+//!   and subs
+//!
 //! Deployment:
 //! - Add to fuzzing
 //! - Turn on during wasm spec-tests
@@ -78,6 +82,7 @@ use crate::isa::TargetIsa;
 use crate::machinst::{BlockIndex, LowerBackend, VCode};
 use crate::trace;
 use regalloc2::Function as _;
+use smallvec::{smallvec, SmallVec};
 use std::fmt;
 
 #[cfg(feature = "enable-serde")]
@@ -122,6 +127,44 @@ pub enum PccError {
     InvalidStoredFact,
 }
 
+/// A range in an integer space. This can be used to describe a value
+/// or an offset into a memtype.
+///
+/// The value is described by three lists of symbolic expressions:
+/// lower bounds (inclusive), exact equalities, and upper bounds
+/// (inclusive).
+///
+/// We may need multiple such lower and upper bounds, and may want
+/// bounds even if we have exact equalities, because comparison is a
+/// *partial* relation: we can't say anything about how `v1` and `v2`
+/// are related, so it may be useful to know that `x < v1`, and also
+/// `x < v2`; or, say, that `x == v1` and also `x < v2`.
+///
+/// When producing a new range, we simplify these lists against each
+/// other, so if one lower bound is greater than or equal to another,
+/// or one upper bound is less than or equal to another, it will be
+/// removed.
+#[derive(Clone, Debug, Hash, PartialEq, Eq)]
+#[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
+pub struct ValueRange {
+    /// Lower bounds (inclusive). The list specifies a set of bounds;
+    /// the concrete value is greater than or equal to *all* of these
+    /// bounds. If the list is empty, then there is no lower bound.
+    pub min: SmallVec<[Expr; 1]>,
+    /// Upper bounds (inclusive). The list specifies a set of bounds;
+    /// the concrete value is less than or equal to *all* of these
+    /// bounds. If the list is empty, then there is no upper bound.
+    pub max: SmallVec<[Expr; 1]>,
+    /// Equalties (inclusive). The list specifies a set of values all
+    /// of which are known to be equal to the value described by this
+    /// range. Note that if this is non-empty, the range's "size"
+    /// (cardinality of the set of possible values) is exactly one
+    /// value; but we may not know a concrete constant, and it is
+    /// still useful to carry around the lower/upper bounds to enable
+    /// further comparisons to be resolved.
+    pub equal: SmallVec<[Expr; 1]>,
+}
+
 /// A fact on a value.
 #[derive(Clone, Debug, Hash, PartialEq, Eq)]
 #[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
@@ -136,59 +179,24 @@ pub enum Fact {
     Range {
         /// The bitwidth of bits we care about, from the LSB upward.
         bit_width: u16,
-        /// The minimum value that the bitslice can take
-        /// (inclusive). The range is unsigned: the specified bits of
-        /// the actual value will be greater than or equal to this
-        /// value, as evaluated by an unsigned integer comparison.
-        min: u64,
-        /// The maximum value that the bitslice can take
-        /// (inclusive). The range is unsigned: the specified bits of
-        /// the actual value will be less than or equal to this value,
-        /// as evaluated by an unsigned integer comparison.
-        max: u64,
-    },
-
-    /// A value bounded by a global value.
-    ///
-    /// The range is in `(min_GV + min_offset)..(max_GV +
-    /// max_offset)`, inclusive on the lower and upper bound.
-    DynamicRange {
-        /// The bitwidth of bits we care about, from the LSB upward.
-        bit_width: u16,
-        /// The lower bound, inclusive.
-        min: Expr,
-        /// The upper bound, inclusive.
-        max: Expr,
+        /// The actual range.
+        range: ValueRange,
     },
 
-    /// A pointer to a memory type.
+    /// A pointer to a memory type, with an offset inside the memory
+    /// type specified as a range, and optionally nullable (can take
+    /// on a zero/NULL pointer value) as well.
     Mem {
         /// The memory type.
         ty: ir::MemoryType,
-        /// The minimum offset into the memory type, inclusive.
-        min_offset: u64,
-        /// The maximum offset into the memory type, inclusive.
-        max_offset: u64,
-        /// This pointer can also be null.
-        nullable: bool,
-    },
-
-    /// A pointer to a memory type, dynamically bounded. The pointer
-    /// is within `(GV_min+offset_min)..(GV_max+offset_max)`
-    /// (inclusive on both ends) in the memory type.
-    DynamicMem {
-        /// The memory type.
-        ty: ir::MemoryType,
-        /// The lower bound, inclusive.
-        min: Expr,
-        /// The upper bound, inclusive.
-        max: Expr,
+        /// The range of offsets into this type.
+        range: ValueRange,
         /// This pointer can also be null.
         nullable: bool,
     },
 
     /// A definition of a value to be used as a symbol in
-    /// BaseExprs. There can only be one of these per value number.
+    /// Exprs. There can only be one of these per value number.
     ///
     /// Note that this differs from a `DynamicRange` specifying that
     /// some value in the program is the same as `value`. A `def(v1)`
@@ -224,212 +232,245 @@ pub enum Fact {
 }
 
 /// A bound expression.
-#[derive(Clone, Debug, Hash, PartialEq, Eq)]
-#[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
-pub struct Expr {
-    /// The dynamic (base) part.
-    pub base: BaseExpr,
-    /// The static (offset) part.
-    pub offset: i64,
-}
-
-/// The base part of a bound expression.
-#[derive(Clone, Debug, Hash, PartialEq, Eq)]
+///
+/// An expression consists of an (optional) symbolic base -- an SSA
+/// value or a GlobalValue -- and a static offset.
+///
+/// Note that `Expr` obeys structural equality -- that is, two `Expr`s
+/// represent actually-equal program values if the `Expr`s themselves
+/// are structurally equal, and conversely, if they are not
+/// structurally equal, then we *cannot prove* equality. There is no
+/// such thing as an "unsimplified" form of an expression that is
+/// statically equal but structurally unequal.
+#[derive(Clone, Copy, Debug, Hash, PartialEq, Eq, PartialOrd, Ord)]
 #[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
-pub enum BaseExpr {
-    /// No dynamic part (i.e., zero).
-    None,
-    /// A global value.
-    GlobalValue(ir::GlobalValue),
-    /// An SSA Value as a symbolic value. This can be referenced in
-    /// facts even after we've lowered out of SSA: it becomes simply
-    /// some symbolic value.
-    Value(ir::Value),
+pub enum Expr {
+    /// A concrete static value in the range of a `u64`.
+    Absolute(u64),
+    /// An offset from an SSA value as a symbolic value. This can be
+    /// referenced in facts even after we've lowered out of SSA -- it
+    /// becomes an arbitrary symbolic base. The offset is an `i128`
+    /// because it may be negative, but also must carry teh full range
+    /// of a `u64` (e.g. if we add an `Absolute`).
+    Value(ir::Value, i128),
+    /// An offset from a GlobalValue as a symbolic value, as `Value`
+    /// is for SSA values.
+    GlobalValue(ir::GlobalValue, i128),
     /// Top of the address space. This is "saturating": the offset
     /// doesn't matter.
     Max,
 }
 
-impl BaseExpr {
-    /// Is one base less than or equal to another? (We can't always
-    /// know; in such cases, returns `false`.)
-    fn le(lhs: &BaseExpr, rhs: &BaseExpr) -> bool {
-        // (i) reflexivity; (ii) 0 <= x for all (unsigned) x; (iii) x <= max for all x.
-        lhs == rhs || *lhs == BaseExpr::None || *rhs == BaseExpr::Max
-    }
-
-    /// Compute some BaseExpr that will be less than or equal to both
-    /// inputs. This is a generalization of `min` (but looser).
-    fn min(lhs: &BaseExpr, rhs: &BaseExpr) -> BaseExpr {
-        if lhs == rhs {
-            lhs.clone()
-        } else if *lhs == BaseExpr::Max {
-            rhs.clone()
-        } else if *rhs == BaseExpr::Max {
-            lhs.clone()
-        } else {
-            BaseExpr::None // zero is <= x for all (unsigned) x.
-        }
+impl Expr {
+    /// Constant value.
+    pub const fn constant(value: u64) -> Self {
+        Expr::Absolute(value)
     }
 
-    /// Compute some BaseExpr that will be greater than or equal to
-    /// both inputs.
-    fn max(lhs: &BaseExpr, rhs: &BaseExpr) -> BaseExpr {
-        if lhs == rhs {
-            lhs.clone()
-        } else if *lhs == BaseExpr::None {
-            rhs.clone()
-        } else if *rhs == BaseExpr::None {
-            lhs.clone()
-        } else {
-            BaseExpr::Max
-        }
+    /// Maximum (saturated) value.
+    pub const fn max_value() -> Self {
+        Expr::Max
     }
-}
 
-impl Expr {
-    /// Constant value.
-    pub fn constant(offset: i64) -> Self {
-        Expr {
-            base: BaseExpr::None,
-            offset,
-        }
+    /// The value of an SSA value.
+    pub const fn value(value: ir::Value) -> Self {
+        Expr::Value(value, 0)
     }
 
-    /// The value of an SSA value.
-    pub fn value(value: ir::Value) -> Self {
-        Expr {
-            base: BaseExpr::Value(value),
-            offset: 0,
-        }
+    /// The value of an SSA value plus some offset.
+    pub const fn value_offset(value: ir::Value, offset: i128) -> Self {
+        Expr::Value(value, offset)
     }
 
     /// The value of a global value.
-    pub fn global_value(gv: ir::GlobalValue) -> Self {
-        Expr {
-            base: BaseExpr::GlobalValue(gv),
-            offset: 0,
-        }
+    pub const fn global_value(gv: ir::GlobalValue) -> Self {
+        Expr::GlobalValue(gv, 0)
+    }
+
+    /// The value of a global value plus some offset.
+    pub const fn global_value_offset(gv: ir::GlobalValue, offset: i128) -> Self {
+        Expr::GlobalValue(gv, offset)
     }
 
     /// Is one expression definitely less than or equal to another?
     /// (We can't always know; in such cases, returns `false`.)
     fn le(lhs: &Expr, rhs: &Expr) -> bool {
-        if rhs.base == BaseExpr::Max {
-            true
-        } else {
-            BaseExpr::le(&lhs.base, &rhs.base) && lhs.offset <= rhs.offset
-        }
+        let result = match (lhs, rhs) {
+            (_, Expr::Max) => true,
+            (Expr::Absolute(0), _) => true,
+            (Expr::Absolute(x), Expr::Absolute(y)) => x <= y,
+            (Expr::Value(v1, x), Expr::Value(v2, y)) if v1 == v2 => x <= y,
+            (Expr::GlobalValue(gv1, x), Expr::GlobalValue(gv2, y)) if gv1 == gv2 => x <= y,
+            _ => false,
+        };
+        trace!("Expr::le: {lhs:?} {rhs:?} -> {result}");
+        result
     }
 
-    /// Generalization of `min`: compute some Expr that is less than
-    /// or equal to both inputs.
-    fn min(lhs: &Expr, rhs: &Expr) -> Expr {
-        if lhs.base == BaseExpr::None && lhs.offset == 0 {
-            lhs.clone()
-        } else if rhs.base == BaseExpr::None && rhs.offset == 0 {
-            rhs.clone()
-        } else {
-            Expr {
-                base: BaseExpr::min(&lhs.base, &rhs.base),
-                offset: std::cmp::min(lhs.offset, rhs.offset),
+    /// Add one expression to another.
+    fn add(lhs: &Expr, rhs: &Expr) -> Expr {
+        let result = match (lhs, rhs) {
+            (Expr::Max, _) | (_, Expr::Max) => Expr::Max,
+            (Expr::Absolute(x), Expr::Absolute(y)) => {
+                x.checked_add(*y).map(Expr::Absolute).unwrap_or(Expr::Max)
+            }
+            (Expr::Value(v1, x), Expr::Value(v2, y)) if v1 == v2 => x
+                .checked_add(*y)
+                .map(|sum| Expr::Value(*v1, sum))
+                .unwrap_or(Expr::Max),
+            (Expr::GlobalValue(gv1, x), Expr::GlobalValue(gv2, y)) if gv1 == gv2 => x
+                .checked_add(*y)
+                .map(|sum| Expr::GlobalValue(*gv1, sum))
+                .unwrap_or(Expr::Max),
+            (Expr::Value(v, x), Expr::Absolute(off)) | (Expr::Absolute(off), Expr::Value(v, x)) => {
+                Expr::Value(*v, *x + i128::from(*off))
+            }
+            (Expr::GlobalValue(gv, x), Expr::Absolute(off))
+            | (Expr::Absolute(off), Expr::GlobalValue(gv, x)) => {
+                Expr::GlobalValue(*gv, *x + i128::from(*off))
             }
+            _ => Expr::Max,
+        };
+        trace!("Expr::add: {lhs:?} + {rhs:?} -> {result:?}");
+        result
+    }
+
+    /// Add a static offset to an expression.
+    pub fn offset(lhs: &Expr, rhs: i64) -> Option<Expr> {
+        match lhs {
+            Expr::Absolute(x) => Some(Expr::Absolute(
+                u64::try_from(i128::from(*x) + i128::from(rhs)).ok()?,
+            )),
+            Expr::Value(v, x) => Some(Expr::Value(*v, *x + i128::from(rhs))),
+            Expr::GlobalValue(gv, x) => Some(Expr::GlobalValue(*gv, *x + i128::from(rhs))),
+            Expr::Max => Some(Expr::Max),
         }
     }
 
-    /// Generalization of `max`: compute some Expr that is greater
-    /// than or equal to both inputs.
-    fn max(lhs: &Expr, rhs: &Expr) -> Expr {
-        if lhs.base == BaseExpr::None && lhs.offset == 0 {
-            rhs.clone()
-        } else if rhs.base == BaseExpr::None && rhs.offset == 0 {
-            lhs.clone()
-        } else {
-            Expr {
-                base: BaseExpr::max(&lhs.base, &rhs.base),
-                offset: std::cmp::max(lhs.offset, rhs.offset),
+    /// Determine if we can know the difference between two expressions.
+    pub fn difference(lhs: &Expr, rhs: &Expr) -> Option<i64> {
+        match (lhs, rhs) {
+            (Expr::Max, _) | (_, Expr::Max) => None,
+            (Expr::Absolute(x), Expr::Absolute(y)) => {
+                i64::try_from(*x).ok()?.checked_sub(i64::try_from(*y).ok()?)
             }
+            (Expr::Value(v1, x), Expr::Value(v2, y)) if v1 == v2 => {
+                i64::try_from(x.checked_sub(*y)?).ok()
+            }
+            (Expr::GlobalValue(gv1, x), Expr::GlobalValue(gv2, y)) if gv1 == gv2 => {
+                i64::try_from(x.checked_sub(*y)?).ok()
+            }
+            _ => None,
         }
     }
 
-    /// Add one expression to another.
-    fn add(lhs: &Expr, rhs: &Expr) -> Option<Expr> {
-        if lhs.base == rhs.base {
-            Some(Expr {
-                base: lhs.base.clone(),
-                offset: lhs.offset.checked_add(rhs.offset)?,
-            })
-        } else if lhs.base == BaseExpr::None {
-            Some(Expr {
-                base: rhs.base.clone(),
-                offset: lhs.offset.checked_add(rhs.offset)?,
-            })
-        } else if rhs.base == BaseExpr::None {
-            Some(Expr {
-                base: lhs.base.clone(),
-                offset: lhs.offset.checked_add(rhs.offset)?,
-            })
-        } else {
-            Some(Expr {
-                base: BaseExpr::Max,
-                offset: 0,
-            })
+    /// Multiply an expression by a constant, if possible.
+    fn scale(&self, factor: u32) -> Option<Expr> {
+        match self {
+            Expr::Absolute(x) => Some(Expr::Absolute(x.checked_mul(u64::from(factor))?)),
+            Expr::Max => Some(Expr::Max),
+            _ => None,
         }
     }
 
-    /// Add a static offset to an expression.
-    pub fn offset(lhs: &Expr, rhs: i64) -> Option<Expr> {
-        let offset = lhs.offset.checked_add(rhs)?;
-        Some(Expr {
-            base: lhs.base.clone(),
-            offset,
-        })
+    /// Multiply an expression by a constant, rounding downward if we
+    /// must approximate.
+    ///
+    /// This is necessary to compute new lower bounds when scaling a range.
+    fn scale_downward(&self, factor: u32) -> Expr {
+        self.scale(factor).unwrap_or(Expr::constant(0))
     }
 
-    /// Is this Expr a BaseExpr with no offset? Return it if so.
-    pub fn without_offset(&self) -> Option<&BaseExpr> {
-        if self.offset == 0 {
-            Some(&self.base)
-        } else {
-            None
+    /// Multiply an expression by a constant, rounding upward if we
+    /// must approximate.
+    ///
+    /// This is necessary to compute new upper bounds when scaling a range.
+    fn scale_upward(&self, factor: u32) -> Expr {
+        self.scale(factor).unwrap_or(Expr::max_value())
+    }
+
+    /// Is this Expr an integer constant?
+    fn as_const(&self) -> Option<i128> {
+        match self {
+            Expr::Absolute(x) => Some(i128::from(*x)),
+            _ => None,
         }
     }
 }
 
-impl fmt::Display for BaseExpr {
+impl fmt::Display for Expr {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         match self {
-            BaseExpr::None => Ok(()),
-            BaseExpr::Max => write!(f, "max"),
-            BaseExpr::GlobalValue(gv) => write!(f, "{gv}"),
-            BaseExpr::Value(value) => write!(f, "{value}"),
+            Expr::Absolute(x) => write!(f, "{x:#x}"),
+            Expr::Value(v, off) => {
+                if *off > 0 {
+                    write!(f, "{v}+{off:#x}")
+                } else if *off == 0 {
+                    write!(f, "{v}")
+                } else {
+                    write!(f, "{v}-{neg:#x}", neg = -off)
+                }
+            }
+            Expr::GlobalValue(gv, off) => {
+                if *off >= 0 {
+                    write!(f, "{gv}+{off:#x}")
+                } else if *off == 0 {
+                    write!(f, "{gv}")
+                } else {
+                    write!(f, "{gv}-{neg:#x}", neg = -off)
+                }
+            }
+            Expr::Max => write!(f, "max"),
         }
     }
 }
 
-impl BaseExpr {
-    /// Does this dynamic_expression take an offset?
-    pub fn is_some(&self) -> bool {
-        match self {
-            BaseExpr::None => false,
-            _ => true,
+struct DisplayExprs<'a>(&'a [Expr]);
+
+impl<'a> fmt::Display for DisplayExprs<'a> {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        match self.0.len() {
+            0 => write!(f, "{{}}"),
+            1 => write!(f, "{}", self.0[0]),
+            _ => {
+                write!(f, "{{")?;
+
+                let mut first = true;
+                for expr in self.0 {
+                    if first {
+                        write!(f, " {expr}")?;
+                        first = false;
+                    } else {
+                        write!(f, ", {expr}")?;
+                    }
+                }
+
+                write!(f, " }}")?;
+                Ok(())
+            }
         }
     }
 }
 
-impl fmt::Display for Expr {
+impl fmt::Display for ValueRange {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        write!(f, "{}", self.base)?;
-        match self.offset {
-            offset if offset > 0 && self.base.is_some() => write!(f, "+{offset:#x}"),
-            offset if offset > 0 => write!(f, "{offset:#x}"),
-            offset if offset < 0 => {
-                let negative_offset = -i128::from(offset); // upcast to support i64::MIN.
-                write!(f, "-{negative_offset:#x}")
-            }
-            0 if self.base.is_some() => Ok(()),
-            0 => write!(f, "0"),
-            _ => unreachable!(),
+        if self.equal.is_empty() {
+            write!(
+                f,
+                "{}, {}",
+                DisplayExprs(&self.min[..]),
+                DisplayExprs(&self.max[..])
+            )
+        } else if self.min.is_empty() && self.max.is_empty() {
+            write!(f, "={}", DisplayExprs(&self.equal[..]))
+        } else {
+            write!(
+                f,
+                "{}, ={}, {}",
+                DisplayExprs(&self.min[..]),
+                DisplayExprs(&self.equal[..]),
+                DisplayExprs(&self.max[..])
+            )
         }
     }
 }
@@ -437,38 +478,16 @@ impl fmt::Display for Expr {
 impl fmt::Display for Fact {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         match self {
-            Fact::Range {
-                bit_width,
-                min,
-                max,
-            } => write!(f, "range({bit_width}, {min:#x}, {max:#x})"),
-            Fact::DynamicRange {
-                bit_width,
-                min,
-                max,
-            } => {
-                write!(f, "dynamic_range({bit_width}, {min}, {max})")
+            Fact::Range { bit_width, range } => {
+                write!(f, "range({bit_width}, {range})")
             }
             Fact::Mem {
                 ty,
-                min_offset,
-                max_offset,
-                nullable,
-            } => {
-                let nullable_flag = if *nullable { ", nullable" } else { "" };
-                write!(
-                    f,
-                    "mem({ty}, {min_offset:#x}, {max_offset:#x}{nullable_flag})"
-                )
-            }
-            Fact::DynamicMem {
-                ty,
-                min,
-                max,
+                range,
                 nullable,
             } => {
                 let nullable_flag = if *nullable { ", nullable" } else { "" };
-                write!(f, "dynamic_mem({ty}, {min}, {max}{nullable_flag})")
+                write!(f, "mem({ty}{nullable_flag}, {range})")
             }
             Fact::Def { value } => write!(f, "def({value})"),
             Fact::Compare { kind, lhs, rhs } => {
@@ -479,6 +498,293 @@ impl fmt::Display for Fact {
     }
 }
 
+impl ValueRange {
+    /// Create a range that is exactly one expression.
+    pub fn exact(expr: Expr) -> Self {
+        ValueRange {
+            equal: smallvec![expr],
+            min: smallvec![],
+            max: smallvec![],
+        }
+    }
+
+    /// Create a range that has a min and max.
+    pub fn min_max(min: Expr, max: Expr) -> Self {
+        ValueRange {
+            equal: smallvec![],
+            min: smallvec![min],
+            max: smallvec![max],
+        }
+    }
+
+    /// Create a range that is exactly one expression, with another expression as an upper bound.
+    pub fn exact_with_max(expr: Expr, max: Expr) -> Self {
+        ValueRange {
+            equal: smallvec![expr],
+            min: smallvec![],
+            max: smallvec![max],
+        }
+    }
+
+    /// Is this ValueRange an exact integer constant?
+    pub fn as_const(&self) -> Option<i128> {
+        self.equal.iter().find_map(|&e| e.as_const())
+    }
+
+    /// Is this ValueRange definitely less than or equal to the given expression?
+    pub fn le_expr(&self, expr: &Expr) -> bool {
+        // The range is <= the expr if *any* of its upper bounds are
+        // <= the expr, because each upper bound constrains the whole
+        // range (i.e., the range is the intersection of all
+        // combinations of bounds). Likewise, if any expression that
+        // exactly determines the value less than `expr`, then we can
+        // definitely say the range is less than `expr`.
+        let result = self
+            .equal
+            .iter()
+            .chain(self.max.iter())
+            .any(|e| Expr::le(e, expr));
+        trace!("ValueRange::le_expr: {self:?} {expr:?} -> {result}");
+        result
+    }
+
+    /// Is the expression definitely within the ValueRange?
+    pub fn contains_expr(&self, expr: &Expr) -> bool {
+        let result = ((!self.min.is_empty() || !self.max.is_empty())
+            && self
+                .min
+                .iter()
+                .all(|lower_bound| Expr::le(lower_bound, expr))
+            && self
+                .max
+                .iter()
+                .all(|upper_bound| Expr::le(expr, upper_bound)))
+            || self.equal.iter().any(|equiv| equiv == expr);
+        trace!("ValueRange::contains_expr: {self:?} {expr:?} -> {result}");
+        result
+    }
+
+    /// Simplify a ValueRange by removing redundant bounds. Any lower
+    /// bound greater than another lower bound, or any upper bound
+    /// less than another upper bound, can be removed.
+    pub fn simplify(&mut self) {
+        trace!("simplify: {self:?}");
+
+        // Note an important invariant: syntactic equality of Exprs
+        // implies symbolic equality. This is required to ensure we
+        // don't remove both `x` and `y` if `x <= y` and `y <= x`,
+        // given the logic below.
+        self.equal.sort();
+        self.equal.dedup();
+
+        // A lower bound `e` is not redundant if for all other
+        // lower bounds `other`, we cannot show that `e >=
+        // other`.
+        self.min.sort();
+        self.min.dedup();
+        let min = self
+            .min
+            .iter()
+            .filter(|&e| {
+                self.min
+                    .iter()
+                    .all(|other| e == other || !Expr::le(other, e))
+            })
+            .cloned()
+            .collect::<SmallVec<[Expr; 1]>>();
+        self.min = min;
+
+        // Likewise, an upper bound `e` is not redundant if
+        // for all other upper bounds `other`, we cannot show
+        // that `other >= e`.
+        self.max.sort();
+        self.max.dedup();
+        let max = self
+            .max
+            .iter()
+            .filter(|&e| {
+                self.min
+                    .iter()
+                    .all(|other| e == other || !Expr::le(e, other))
+            })
+            .cloned()
+            .collect::<SmallVec<[Expr; 1]>>();
+        self.max = max;
+
+        trace!("simplify: produced {self:?}");
+    }
+
+    /// Does one ValueRange contain another? Assumes both sides are already simplified.
+    pub fn contains(&self, other: &ValueRange) -> bool {
+        let result = other.equal.iter().any(|e| self.contains_expr(e)) ||
+        // *Some* lower bound and *some* upper bound of the RHS must
+        // be contained in the LHS. Either those lower and upper
+        // bounds are tight, in which case all values between them are
+        // then contained in the LHS; or they are loose, and the true
+        // range is contained within them, which in turn is contained
+        // in the LHS.
+            (other.min
+             .iter()
+             .any(|lower_bound2| self.contains_expr(lower_bound2))
+             || self.contains_expr(&Expr::constant(0)))
+            && (other.max
+                .iter()
+                .any(|upper_bound2| self.contains_expr(upper_bound2))
+                || self.contains_expr(&Expr::max_value()));
+        trace!("ValueRange::contains: {self:?} {other:?} -> {result}");
+        result
+    }
+
+    /// Intersect two ValueRanges.
+    pub fn intersect(lhs: &ValueRange, rhs: &ValueRange) -> ValueRange {
+        let equal = lhs
+            .equal
+            .iter()
+            .cloned()
+            .chain(rhs.equal.iter().cloned())
+            .collect();
+        let min = lhs
+            .min
+            .iter()
+            .cloned()
+            .chain(rhs.min.iter().cloned())
+            .collect();
+        let max = lhs
+            .max
+            .iter()
+            .cloned()
+            .chain(rhs.max.iter().cloned())
+            .collect();
+        let mut result = ValueRange { equal, min, max };
+        result.simplify();
+        result
+    }
+
+    /// Take the union of two ranges.
+    pub fn union(lhs: &ValueRange, rhs: &ValueRange) -> ValueRange {
+        // Take lower bounds from LHS that are less than all
+        // lower bounds on the RHS; and likewise the other
+        // way; and likewise for upper bounds.
+        let min = lhs
+            .min
+            .iter()
+            .filter(|&e| rhs.min.iter().all(|e2| Expr::le(e, e2)))
+            .cloned()
+            .chain(
+                rhs.min
+                    .iter()
+                    .filter(|e| lhs.min.iter().all(|e2| Expr::le(e, e2)))
+                    .cloned(),
+            )
+            .collect();
+        let max = lhs
+            .max
+            .iter()
+            .filter(|&e| rhs.max.iter().all(|e2| Expr::le(e2, e)))
+            .cloned()
+            .chain(
+                rhs.max
+                    .iter()
+                    .filter(|e| lhs.max.iter().all(|e2| Expr::le(e2, e)))
+                    .cloned(),
+            )
+            .collect();
+        let equal = lhs
+            .equal
+            .iter()
+            .filter(|&e| rhs.equal.iter().any(|e2| e == e2))
+            .cloned()
+            .chain(
+                rhs.equal
+                    .iter()
+                    .filter(|&e| lhs.equal.iter().any(|e2| e == e2))
+                    .cloned(),
+            )
+            .collect();
+        let mut result = ValueRange { min, max, equal };
+        result.simplify();
+        result
+    }
+
+    /// Scale a range by a factor.
+    pub fn scale(&self, factor: u32) -> ValueRange {
+        let equal = self.equal.iter().filter_map(|e| e.scale(factor)).collect();
+        let min = self.min.iter().map(|e| e.scale_downward(factor)).collect();
+        let max = self.max.iter().map(|e| e.scale_upward(factor)).collect();
+        let mut result = ValueRange { equal, min, max };
+        result.simplify();
+        result
+    }
+
+    /// Add an offset to the lower and upper bounds of a range.
+    pub fn offset(&self, offset: i64) -> ValueRange {
+        let equal = self
+            .equal
+            .iter()
+            .flat_map(|e| Expr::offset(e, offset))
+            .collect();
+        let min = self
+            .min
+            .iter()
+            .flat_map(|e| Expr::offset(e, offset))
+            .collect();
+        let max = self
+            .max
+            .iter()
+            .flat_map(|e| Expr::offset(e, offset))
+            .collect();
+        let mut result = ValueRange { equal, min, max };
+        result.simplify();
+        result
+    }
+
+    /// Find the range of the sum of two values described by ranges.
+    pub fn add(lhs: &ValueRange, rhs: &ValueRange) -> ValueRange {
+        trace!("ValueRange::add: {lhs:?} + {rhs:?}");
+        let min = lhs
+            .min
+            .iter()
+            .chain(lhs.equal.iter())
+            .flat_map(|m1| {
+                rhs.min
+                    .iter()
+                    .chain(rhs.equal.iter())
+                    .map(|m2| Expr::add(m1, m2))
+            })
+            .collect();
+        let max = lhs
+            .max
+            .iter()
+            .chain(lhs.equal.iter())
+            .flat_map(|m1| {
+                rhs.max
+                    .iter()
+                    .chain(rhs.equal.iter())
+                    .map(|m2| Expr::add(m1, m2))
+            })
+            .collect();
+        let equal = lhs
+            .equal
+            .iter()
+            .flat_map(|m1| rhs.equal.iter().map(|m2| Expr::add(m1, m2)))
+            .collect();
+        let mut result = ValueRange { equal, min, max };
+        trace!(" -> inclusive + inclusive: {result:?}");
+        result.simplify();
+        trace!(" -> {result:?}");
+        result
+    }
+
+    /// Clamp a ValueRange given a bit-width for the result.
+    fn clamp(mut self, width: u16) -> ValueRange {
+        trace!("ValueRange::clamp: {self:?} width {width}");
+        self.max.push(Expr::constant(max_value_for_width(width)));
+        self.simplify();
+        trace!("ValueRange::clamp: -> {self:?}");
+        self
+    }
+}
+
 impl Fact {
     /// Create a range fact that specifies a single known constant value.
     pub fn constant(bit_width: u16, value: u64) -> Self {
@@ -487,17 +793,15 @@ impl Fact {
         // exactly one value.
         Fact::Range {
             bit_width,
-            min: value,
-            max: value,
+            range: ValueRange::exact(Expr::constant(value)),
         }
     }
 
-    /// Create a dynamic range fact that points to the base of a dynamic memory.
+    /// Create a range fact that points to the base of a memory type.
     pub fn dynamic_base_ptr(ty: ir::MemoryType) -> Self {
-        Fact::DynamicMem {
+        Fact::Mem {
             ty,
-            min: Expr::constant(0),
-            max: Expr::constant(0),
+            range: ValueRange::exact(Expr::constant(0)),
             nullable: false,
         }
     }
@@ -510,91 +814,143 @@ impl Fact {
     /// that symbol is. (In other words, the def should be elsewhere,
     /// and we are tying ourselves to it.)
     pub fn value(bit_width: u16, value: ir::Value) -> Self {
-        Fact::DynamicRange {
+        Fact::Range {
             bit_width,
-            min: Expr::value(value),
-            max: Expr::value(value),
+            range: ValueRange::exact_with_max(
+                Expr::value(value),
+                Expr::constant(max_value_for_width(bit_width)),
+            ),
         }
     }
 
     /// Create a fact that specifies the value is exactly an SSA value plus some offset.
     pub fn value_offset(bit_width: u16, value: ir::Value, offset: i64) -> Self {
-        Fact::DynamicRange {
+        Fact::Range {
             bit_width,
-            min: Expr::offset(&Expr::value(value), offset).unwrap(),
-            max: Expr::offset(&Expr::value(value), offset).unwrap(),
+            range: ValueRange::exact_with_max(
+                Expr::value_offset(value, offset.into()),
+                Expr::constant(max_value_for_width(bit_width)),
+            ),
         }
     }
 
     /// Create a fact that specifies the value is exactly the value of a GV.
     pub fn global_value(bit_width: u16, gv: ir::GlobalValue) -> Self {
-        Fact::DynamicRange {
+        Fact::Range {
             bit_width,
-            min: Expr::global_value(gv),
-            max: Expr::global_value(gv),
+            range: ValueRange::exact_with_max(
+                Expr::global_value(gv),
+                Expr::constant(max_value_for_width(bit_width)),
+            ),
         }
     }
 
     /// Create a fact that specifies the value is exactly the value of a GV plus some offset.
     pub fn global_value_offset(bit_width: u16, gv: ir::GlobalValue, offset: i64) -> Self {
-        Fact::DynamicRange {
+        Fact::Range {
             bit_width,
-            min: Expr::offset(&Expr::global_value(gv), offset).unwrap(),
-            max: Expr::offset(&Expr::global_value(gv), offset).unwrap(),
+            range: ValueRange::exact_with_max(
+                Expr::global_value_offset(gv, offset.into()),
+                Expr::constant(max_value_for_width(bit_width)),
+            ),
+        }
+    }
+
+    /// Create a fact that expresses a given static range, from zero
+    /// up to `max` (inclusive).
+    pub fn static_value_range(bit_width: u16, max: u64) -> Self {
+        Fact::Range {
+            bit_width,
+            range: ValueRange::min_max(Expr::constant(0), Expr::constant(max)),
+        }
+    }
+
+    /// Create a fact that expresses a given static range, from `min`
+    /// (inclusive) up to `max` (inclusive).
+    pub fn static_value_two_ended_range(bit_width: u16, min: u64, max: u64) -> Self {
+        if min == max {
+            Fact::constant(bit_width, min)
+        } else {
+            Fact::Range {
+                bit_width,
+                range: ValueRange::min_max(Expr::constant(min), Expr::constant(max)),
+            }
+        }
+    }
+
+    /// Create a fact that expresses a given dynamic range, from zero up to `expr`.
+    pub fn dynamic_value_range(bit_width: u16, max: Expr) -> Self {
+        Fact::Range {
+            bit_width,
+            range: ValueRange::min_max(Expr::constant(0), max),
         }
     }
 
     /// Create a range fact that specifies the maximum range for a
     /// value of the given bit-width.
-    pub const fn max_range_for_width(bit_width: u16) -> Self {
-        match bit_width {
-            bit_width if bit_width < 64 => Fact::Range {
-                bit_width,
-                min: 0,
-                max: (1u64 << bit_width) - 1,
-            },
-            64 => Fact::Range {
-                bit_width: 64,
-                min: 0,
-                max: u64::MAX,
-            },
-            _ => panic!("bit width too large!"),
+    pub fn max_range_for_width(bit_width: u16) -> Self {
+        Fact::Range {
+            bit_width,
+            range: ValueRange::min_max(
+                Expr::constant(0),
+                Expr::constant(max_value_for_width(bit_width)),
+            ),
+        }
+    }
+
+    /// Create a fact that describes the base pointer for a memory
+    /// type.
+    pub fn memory_base(ty: ir::MemoryType) -> Self {
+        Fact::Mem {
+            ty,
+            range: ValueRange::exact(Expr::constant(0)),
+            nullable: false,
         }
     }
 
+    /// Create a fact that describes a pointer to the given memory
+    /// type with an offset described by the given fact.
+    pub fn memory_with_range(
+        ty: ir::MemoryType,
+        offset_fact: Fact,
+        nullable: bool,
+    ) -> Option<Self> {
+        let Fact::Range {
+            bit_width: _,
+            range,
+        } = offset_fact
+        else {
+            return None;
+        };
+        Some(Fact::Mem {
+            ty,
+            range,
+            nullable,
+        })
+    }
+
     /// Create a range fact that specifies the maximum range for a
     /// value of the given bit-width, zero-extended into a wider
     /// width.
-    pub const fn max_range_for_width_extended(from_width: u16, to_width: u16) -> Self {
+    pub fn max_range_for_width_extended(from_width: u16, to_width: u16) -> Self {
         debug_assert!(from_width <= to_width);
-        match from_width {
-            from_width if from_width < 64 => Fact::Range {
-                bit_width: to_width,
-                min: 0,
-                max: (1u64 << from_width) - 1,
-            },
-            64 => Fact::Range {
-                bit_width: to_width,
-                min: 0,
-                max: u64::MAX,
-            },
-            _ => panic!("bit width too large!"),
+        let upper_bound = if from_width <= 64 {
+            Expr::constant(max_value_for_width(from_width))
+        } else {
+            Expr::max_value()
+        };
+        Fact::Range {
+            bit_width: to_width,
+            range: ValueRange::min_max(Expr::constant(0), upper_bound),
         }
     }
 
     /// Try to infer a minimal fact for a value of the given IR type.
-    pub fn infer_from_type(ty: ir::Type) -> Option<&'static Self> {
-        static FACTS: [Fact; 4] = [
-            Fact::max_range_for_width(8),
-            Fact::max_range_for_width(16),
-            Fact::max_range_for_width(32),
-            Fact::max_range_for_width(64),
-        ];
+    pub fn infer_from_type(ty: ir::Type) -> Option<Self> {
         match ty {
-            I8 => Some(&FACTS[0]),
-            I16 => Some(&FACTS[1]),
-            I32 => Some(&FACTS[2]),
-            I64 => Some(&FACTS[3]),
+            I8 | I16 | I32 | I64 => {
+                Some(Self::max_range_for_width(u16::try_from(ty.bits()).unwrap()))
+            }
             _ => None,
         }
     }
@@ -610,129 +966,228 @@ impl Fact {
         }
     }
 
-    /// Is this a constant value of the given bitwidth? Return it as a
-    /// `Some(value)` if so.
-    pub fn as_const(&self, bits: u16) -> Option<u64> {
-        match self {
-            Fact::Range {
-                bit_width,
-                min,
-                max,
-            } if *bit_width == bits && min == max => Some(*min),
-            _ => None,
-        }
-    }
-
-    /// Is this fact a single-value range with a symbolic Expr?
-    pub fn as_symbol(&self) -> Option<&Expr> {
-        match self {
-            Fact::DynamicRange { min, max, .. } if min == max => Some(min),
-            _ => None,
-        }
-    }
-
     /// Merge two facts. We take the *intersection*: that is, we know
     /// both facts to be true, so we can intersect ranges. (This
     /// differs from the usual static analysis approach, where we are
     /// merging multiple possibilities into a generalized / widened
     /// fact. We want to narrow here.)
     pub fn intersect(a: &Fact, b: &Fact) -> Fact {
-        match (a, b) {
+        let result = match (a, b) {
             (
                 Fact::Range {
                     bit_width: bw_lhs,
-                    min: min_lhs,
-                    max: max_lhs,
+                    range: range1,
                 },
                 Fact::Range {
                     bit_width: bw_rhs,
-                    min: min_rhs,
-                    max: max_rhs,
+                    range: range2,
                 },
-            ) if bw_lhs == bw_rhs && max_lhs >= min_rhs && max_rhs >= min_lhs => Fact::Range {
+            ) if bw_lhs == bw_rhs => Fact::Range {
                 bit_width: *bw_lhs,
-                min: std::cmp::max(*min_lhs, *min_rhs),
-                max: std::cmp::min(*max_lhs, *max_rhs),
+                range: ValueRange::intersect(range1, range2),
             },
 
-            (
-                Fact::DynamicRange {
-                    bit_width: bw_lhs,
-                    min: min_lhs,
-                    max: max_lhs,
-                },
-                Fact::DynamicRange {
-                    bit_width: bw_rhs,
-                    min: min_rhs,
-                    max: max_rhs,
-                },
-            ) if bw_lhs == bw_rhs && Expr::le(min_rhs, max_lhs) && Expr::le(min_lhs, max_rhs) => {
-                Fact::DynamicRange {
-                    bit_width: *bw_lhs,
-                    min: Expr::max(min_lhs, min_rhs),
-                    max: Expr::min(max_lhs, max_rhs),
-                }
-            }
-
             (
                 Fact::Mem {
                     ty: ty_lhs,
-                    min_offset: min_offset_lhs,
-                    max_offset: max_offset_lhs,
+                    range: range1,
                     nullable: nullable_lhs,
                 },
                 Fact::Mem {
                     ty: ty_rhs,
-                    min_offset: min_offset_rhs,
-                    max_offset: max_offset_rhs,
+                    range: range2,
                     nullable: nullable_rhs,
                 },
-            ) if ty_lhs == ty_rhs
-                && max_offset_lhs >= min_offset_rhs
-                && max_offset_rhs >= min_offset_lhs =>
-            {
-                Fact::Mem {
-                    ty: *ty_lhs,
-                    min_offset: std::cmp::max(*min_offset_lhs, *min_offset_rhs),
-                    max_offset: std::cmp::min(*max_offset_lhs, *max_offset_rhs),
-                    nullable: *nullable_lhs && *nullable_rhs,
-                }
-            }
+            ) if ty_lhs == ty_rhs => Fact::Mem {
+                ty: *ty_lhs,
+                range: ValueRange::intersect(range1, range2),
+                nullable: *nullable_lhs && *nullable_rhs,
+            },
+
+            (Fact::Def { value: v1 }, Fact::Def { value: v2 }) => Fact::Def {
+                value: std::cmp::min(*v1, *v2),
+            },
 
             (
-                Fact::DynamicMem {
-                    ty: ty_lhs,
-                    min: min_lhs,
-                    max: max_lhs,
-                    nullable: null_lhs,
+                Fact::Compare {
+                    kind: kind1,
+                    lhs: lhs1,
+                    rhs: rhs1,
                 },
-                Fact::DynamicMem {
-                    ty: ty_rhs,
-                    min: min_rhs,
-                    max: max_rhs,
-                    nullable: null_rhs,
+                Fact::Compare {
+                    kind: kind2,
+                    lhs: lhs2,
+                    rhs: rhs2,
                 },
-            ) if ty_lhs == ty_rhs && Expr::le(min_rhs, max_lhs) && Expr::le(min_lhs, max_rhs) => {
-                Fact::DynamicMem {
-                    ty: *ty_lhs,
-                    min: Expr::max(min_lhs, min_rhs),
-                    max: Expr::min(max_lhs, max_rhs),
-                    nullable: *null_lhs && *null_rhs,
+            ) if kind1 == kind2 => {
+                if (lhs1, rhs1) <= (lhs2, rhs2) {
+                    Fact::Compare {
+                        kind: *kind1,
+                        lhs: *lhs1,
+                        rhs: *rhs1,
+                    }
+                } else {
+                    Fact::Compare {
+                        kind: *kind2,
+                        lhs: *lhs2,
+                        rhs: *rhs2,
+                    }
                 }
             }
 
             _ => Fact::Conflict,
-        }
+        };
+        trace!("Fact::intersect: {a:?} {b:?} -> {result:?}");
+        result
     }
-}
 
-macro_rules! ensure {
-    ( $condition:expr, $err:tt $(,)? ) => {
-        if !$condition {
-            return Err(PccError::$err);
-        }
-    };
-}
+    /// Take the union of two facts: produce a fact that applies to a
+    /// value that has either one fact or another (e.g., at a
+    /// control-flow merge point or a conditional-select operator).
+    pub fn union(a: &Fact, b: &Fact) -> Fact {
+        let result = match (a, b) {
+            (
+                Fact::Range {
+                    bit_width: bw_lhs,
+                    range: range1,
+                },
+                Fact::Range {
+                    bit_width: bw_rhs,
+                    range: range2,
+                },
+            ) if bw_lhs == bw_rhs => Fact::Range {
+                bit_width: *bw_lhs,
+                range: ValueRange::union(range1, range2),
+            },
+
+            (
+                Fact::Mem {
+                    ty: ty_lhs,
+                    range: range1,
+                    nullable: nullable_lhs,
+                },
+                Fact::Mem {
+                    ty: ty_rhs,
+                    range: range2,
+                    nullable: nullable_rhs,
+                },
+            ) if ty_lhs == ty_rhs => Fact::Mem {
+                ty: *ty_lhs,
+                range: ValueRange::union(range1, range2),
+                nullable: *nullable_lhs || *nullable_rhs,
+            },
+
+            (
+                Fact::Mem {
+                    ty: ty_mem,
+                    range: range_mem,
+                    nullable: _,
+                },
+                Fact::Range {
+                    bit_width: _,
+                    range: range_offset,
+                },
+            )
+            | (
+                Fact::Range {
+                    bit_width: _,
+                    range: range_offset,
+                },
+                Fact::Mem {
+                    ty: ty_mem,
+                    range: range_mem,
+                    nullable: _,
+                },
+            ) if range_offset.le_expr(&Expr::constant(0)) => Fact::Mem {
+                ty: *ty_mem,
+                range: range_mem.clone(),
+                nullable: true,
+            },
+
+            _ => Fact::Conflict,
+        };
+        trace!("Fact::union: {a:?} {b:?} -> {result:?}");
+        result
+    }
+
+    /// Does this fact describe an exact expression?
+    pub fn as_expr(&self) -> Option<&Expr> {
+        match self {
+            Fact::Range {
+                range: ValueRange { equal, .. },
+                ..
+            } => equal.first(),
+            _ => None,
+        }
+    }
+
+    /// Does this fact describe a constant?
+    pub fn as_const(&self) -> Option<i128> {
+        match self {
+            Fact::Range { range, .. } => range.as_const(),
+            _ => None,
+        }
+    }
+
+    /// Offsets a value with a fact by a known amount.
+    pub fn offset(&self, width: u16, offset: i64) -> Option<Fact> {
+        if offset == 0 {
+            return Some(self.clone());
+        }
+
+        let result = match self {
+            Fact::Range { bit_width, range } if *bit_width == width => Some(Fact::Range {
+                bit_width: *bit_width,
+                range: range.offset(offset.into()).clamp(width),
+            }),
+            Fact::Mem {
+                ty,
+                range,
+                nullable: false,
+            } => Some(Fact::Mem {
+                ty: *ty,
+                range: range.offset(offset.into()).clamp(width),
+                nullable: false,
+            }),
+            _ => None,
+        };
+        trace!("offset: {self:?} + {offset} in width {width} -> {result:?}");
+        result
+    }
+
+    /// Get the range of a fact: either the actual value range, or the
+    /// range of offsets into a memory type.
+    pub fn range(&self) -> Option<&ValueRange> {
+        match self {
+            Fact::Range { range, .. } | Fact::Mem { range, .. } => Some(range),
+            _ => None,
+        }
+    }
+
+    /// Update the range in either a Range or Mem fact.
+    pub fn with_range(&self, range: ValueRange) -> Fact {
+        match self {
+            Fact::Range { bit_width, .. } => Fact::Range {
+                bit_width: *bit_width,
+                range,
+            },
+            Fact::Mem { ty, nullable, .. } => Fact::Mem {
+                ty: *ty,
+                nullable: *nullable,
+                range,
+            },
+            f => f.clone(),
+        }
+    }
+}
+
+macro_rules! ensure {
+    ( $condition:expr, $err:tt $(,)? ) => {
+        if !$condition {
+            return Err(PccError::$err);
+        }
+    };
+}
 
 macro_rules! bail {
     ( $err:tt ) => {{
@@ -769,6 +1224,7 @@ impl<'a> FactContext<'a> {
 
     /// Computes whether `lhs` "subsumes" (implies) `rhs`.
     pub fn subsumes(&self, lhs: &Fact, rhs: &Fact) -> bool {
+        trace!("subsumes {lhs:?} {rhs:?}");
         match (lhs, rhs) {
             // Reflexivity.
             (l, r) if l == r => true,
@@ -776,96 +1232,64 @@ impl<'a> FactContext<'a> {
             (
                 Fact::Range {
                     bit_width: bw_lhs,
-                    min: min_lhs,
-                    max: max_lhs,
+                    range: range_lhs,
                 },
                 Fact::Range {
                     bit_width: bw_rhs,
-                    min: min_rhs,
-                    max: max_rhs,
+                    range: range_rhs,
                 },
-            ) => {
-                // If the bitwidths we're claiming facts about are the
-                // same, or the left-hand-side makes a claim about a
-                // wider bitwidth, and if the right-hand-side range is
-                // larger than the left-hand-side range, than the LHS
-                // subsumes the RHS.
-                //
-                // In other words, we can always expand the claimed
-                // possible value range.
-                bw_lhs >= bw_rhs && max_lhs <= max_rhs && min_lhs >= min_rhs
-            }
+            ) if bw_lhs == bw_rhs => range_rhs.contains(range_lhs),
 
             (
-                Fact::DynamicRange {
+                Fact::Range {
                     bit_width: bw_lhs,
-                    min: min_lhs,
-                    max: max_lhs,
+                    range: range_lhs,
                 },
-                Fact::DynamicRange {
+                Fact::Range {
                     bit_width: bw_rhs,
-                    min: min_rhs,
-                    max: max_rhs,
+                    range: range_rhs,
                 },
-            ) => {
-                // Nearly same as above, but with dynamic-expression
-                // comparisons. Note that we require equal bitwidths
-                // here: unlike in the static case, we don't have
-                // fixed values for min and max, so we can't lean on
-                // the well-formedness requirements of the static
-                // ranges fitting within the bit-width max.
-                bw_lhs == bw_rhs && Expr::le(max_lhs, max_rhs) && Expr::le(min_rhs, min_lhs)
+            ) if bw_lhs > bw_rhs => {
+                // If the LHS makes a claim about a larger bitwidth,
+                // then it can still imply the RHS if the RHS claims
+                // the full range of its width.
+                let rhs_is_trivially_true = range_rhs.contains_expr(&Expr::constant(0))
+                    && range_rhs.contains_expr(&Expr::constant(max_value_for_width(*bw_rhs)));
+                // It can also still imply the RHS if the LHS's range
+                // is within the bitwidth of the RHS and the RHS
+                // otherwise contains the LHS's range, so we don't
+                // have to worry about truncation/aliasing effects.
+                let lhs_is_in_rhs_width_range =
+                    range_lhs.le_expr(&Expr::constant(max_value_for_width(*bw_rhs)));
+
+                rhs_is_trivially_true
+                    || (lhs_is_in_rhs_width_range && range_rhs.contains(range_lhs))
             }
 
             (
                 Fact::Mem {
                     ty: ty_lhs,
-                    min_offset: min_offset_lhs,
-                    max_offset: max_offset_lhs,
+                    range: range_lhs,
                     nullable: nullable_lhs,
                 },
                 Fact::Mem {
                     ty: ty_rhs,
-                    min_offset: min_offset_rhs,
-                    max_offset: max_offset_rhs,
+                    range: range_rhs,
                     nullable: nullable_rhs,
                 },
             ) => {
                 ty_lhs == ty_rhs
-                    && max_offset_lhs <= max_offset_rhs
-                    && min_offset_lhs >= min_offset_rhs
-                    && (*nullable_lhs || !*nullable_rhs)
-            }
-
-            (
-                Fact::DynamicMem {
-                    ty: ty_lhs,
-                    min: min_lhs,
-                    max: max_lhs,
-                    nullable: nullable_lhs,
-                },
-                Fact::DynamicMem {
-                    ty: ty_rhs,
-                    min: min_rhs,
-                    max: max_rhs,
-                    nullable: nullable_rhs,
-                },
-            ) => {
-                ty_lhs == ty_rhs
-                    && Expr::le(max_lhs, max_rhs)
-                    && Expr::le(min_rhs, min_lhs)
+                    && range_rhs.contains(range_lhs)
                     && (*nullable_lhs || !*nullable_rhs)
             }
 
             // Constant zero subsumes nullable DynamicMem pointers.
             (
                 Fact::Range {
-                    bit_width,
-                    min: 0,
-                    max: 0,
+                    bit_width, range, ..
                 },
-                Fact::DynamicMem { nullable: true, .. },
-            ) if *bit_width == self.pointer_width => true,
+                Fact::Mem { nullable: true, .. },
+            ) if *bit_width == self.pointer_width && range.le_expr(&Expr::constant(0)) => true,
 
             // Any fact subsumes a Def, because the Def makes no
             // claims about the actual value (it ties a symbol to that
@@ -899,209 +1323,55 @@ impl<'a> FactContext<'a> {
             (
                 Fact::Range {
                     bit_width: bw_lhs,
-                    min: min_lhs,
-                    max: max_lhs,
+                    range: range_lhs,
                 },
                 Fact::Range {
                     bit_width: bw_rhs,
-                    min: min_rhs,
-                    max: max_rhs,
+                    range: range_rhs,
                 },
-            ) if bw_lhs == bw_rhs && add_width >= *bw_lhs => {
-                let computed_min = min_lhs.checked_add(*min_rhs)?;
-                let computed_max = max_lhs.checked_add(*max_rhs)?;
-                let computed_max = std::cmp::min(max_value_for_width(add_width), computed_max);
-                Some(Fact::Range {
-                    bit_width: *bw_lhs,
-                    min: computed_min,
-                    max: computed_max,
-                })
-            }
+            ) if bw_lhs == bw_rhs && add_width >= *bw_lhs => Some(Fact::Range {
+                bit_width: *bw_lhs,
+                range: ValueRange::add(range_lhs, range_rhs).clamp(add_width),
+            }),
 
             (
                 Fact::Range {
-                    bit_width: bw_max,
-                    min,
-                    max,
+                    bit_width: bw_lhs,
+                    range: range_lhs,
                 },
                 Fact::Mem {
                     ty,
-                    min_offset,
-                    max_offset,
+                    range: range_rhs,
                     nullable,
                 },
             )
             | (
                 Fact::Mem {
                     ty,
-                    min_offset,
-                    max_offset,
+                    range: range_rhs,
                     nullable,
                 },
                 Fact::Range {
-                    bit_width: bw_max,
-                    min,
-                    max,
+                    bit_width: bw_lhs,
+                    range: range_lhs,
                 },
-            ) if *bw_max >= self.pointer_width
-                && add_width >= *bw_max
-                && (!*nullable || *max == 0) =>
+            ) if *bw_lhs >= self.pointer_width
+                && add_width >= *bw_lhs
+                // A null pointer doesn't remain a null pointer unless
+                // the right-hand side is constant zero.
+                && (!*nullable || range_lhs.le_expr(&Expr::constant(0))) =>
             {
-                let min_offset = min_offset.checked_add(*min)?;
-                let max_offset = max_offset.checked_add(*max)?;
                 Some(Fact::Mem {
                     ty: *ty,
-                    min_offset,
-                    max_offset,
-                    nullable: false,
-                })
-            }
-
-            (
-                Fact::Range {
-                    bit_width: bw_static,
-                    min: min_static,
-                    max: max_static,
-                },
-                Fact::DynamicRange {
-                    bit_width: bw_dynamic,
-                    min: ref min_dynamic,
-                    max: ref max_dynamic,
-                },
-            )
-            | (
-                Fact::DynamicRange {
-                    bit_width: bw_dynamic,
-                    min: ref min_dynamic,
-                    max: ref max_dynamic,
-                },
-                Fact::Range {
-                    bit_width: bw_static,
-                    min: min_static,
-                    max: max_static,
-                },
-            ) if bw_static == bw_dynamic => {
-                let min = Expr::offset(min_dynamic, i64::try_from(*min_static).ok()?)?;
-                let max = Expr::offset(max_dynamic, i64::try_from(*max_static).ok()?)?;
-                Some(Fact::DynamicRange {
-                    bit_width: *bw_dynamic,
-                    min,
-                    max,
-                })
-            }
-
-            (
-                Fact::DynamicMem {
-                    ty,
-                    min: min_mem,
-                    max: max_mem,
-                    nullable: false,
-                },
-                Fact::DynamicRange {
-                    bit_width,
-                    min: min_range,
-                    max: max_range,
-                },
-            )
-            | (
-                Fact::DynamicRange {
-                    bit_width,
-                    min: min_range,
-                    max: max_range,
-                },
-                Fact::DynamicMem {
-                    ty,
-                    min: min_mem,
-                    max: max_mem,
-                    nullable: false,
-                },
-            ) if *bit_width == self.pointer_width => {
-                let min = Expr::add(min_mem, min_range)?;
-                let max = Expr::add(max_mem, max_range)?;
-                Some(Fact::DynamicMem {
-                    ty: *ty,
-                    min,
-                    max,
-                    nullable: false,
-                })
-            }
-
-            (
-                Fact::Mem {
-                    ty,
-                    min_offset,
-                    max_offset,
-                    nullable: false,
-                },
-                Fact::DynamicRange {
-                    bit_width,
-                    min: min_range,
-                    max: max_range,
-                },
-            )
-            | (
-                Fact::DynamicRange {
-                    bit_width,
-                    min: min_range,
-                    max: max_range,
-                },
-                Fact::Mem {
-                    ty,
-                    min_offset,
-                    max_offset,
-                    nullable: false,
-                },
-            ) if *bit_width == self.pointer_width => {
-                let min = Expr::offset(min_range, i64::try_from(*min_offset).ok()?)?;
-                let max = Expr::offset(max_range, i64::try_from(*max_offset).ok()?)?;
-                Some(Fact::DynamicMem {
-                    ty: *ty,
-                    min,
-                    max,
-                    nullable: false,
-                })
-            }
-
-            (
-                Fact::Range {
-                    bit_width: bw_static,
-                    min: min_static,
-                    max: max_static,
-                },
-                Fact::DynamicMem {
-                    ty,
-                    min: ref min_dynamic,
-                    max: ref max_dynamic,
-                    nullable,
-                },
-            )
-            | (
-                Fact::DynamicMem {
-                    ty,
-                    min: ref min_dynamic,
-                    max: ref max_dynamic,
-                    nullable,
-                },
-                Fact::Range {
-                    bit_width: bw_static,
-                    min: min_static,
-                    max: max_static,
-                },
-            ) if *bw_static == self.pointer_width && (!*nullable || *max_static == 0) => {
-                let min = Expr::offset(min_dynamic, i64::try_from(*min_static).ok()?)?;
-                let max = Expr::offset(max_dynamic, i64::try_from(*max_static).ok()?)?;
-                Some(Fact::DynamicMem {
-                    ty: *ty,
-                    min,
-                    max,
-                    nullable: false,
+                    range: ValueRange::add(range_lhs, range_rhs).clamp(add_width),
+                    nullable: *nullable,
                 })
             }
 
             _ => None,
         };
 
-        trace!("add: {lhs:?} + {rhs:?} -> {result:?}");
+        trace!("add({add_width}): {lhs:?} + {rhs:?} -> {result:?}");
         result
     }
 
@@ -1112,39 +1382,20 @@ impl<'a> FactContext<'a> {
         }
 
         let result = match fact {
-            // If the claim is already for a same-or-wider value and the min
-            // and max are within range of the narrower value, we can
-            // claim the same range.
-            Fact::Range {
-                bit_width,
-                min,
-                max,
-            } if *bit_width >= from_width
-                && *min <= max_value_for_width(from_width)
-                && *max <= max_value_for_width(from_width) =>
-            {
-                Some(Fact::Range {
-                    bit_width: to_width,
-                    min: *min,
-                    max: *max,
-                })
-            }
-
-            // If the claim is a dynamic range for the from-width, we
-            // can extend to the to-width.
-            Fact::DynamicRange {
-                bit_width,
-                min,
-                max,
-            } if *bit_width == from_width => Some(Fact::DynamicRange {
+            Fact::Range { bit_width, range } if *bit_width == from_width => Some(Fact::Range {
                 bit_width: to_width,
-                min: min.clone(),
-                max: max.clone(),
+                range: range.clone(),
             }),
 
             // If the claim is a definition of a value, we can say
             // that the output has a range of exactly that value.
-            Fact::Def { value } => Some(Fact::value(to_width, *value)),
+            Fact::Def { value } => Some(Fact::Range {
+                bit_width: to_width,
+                range: ValueRange::exact_with_max(
+                    Expr::value(*value),
+                    Expr::constant(max_value_for_width(from_width)),
+                ),
+            }),
 
             // Otherwise, we can at least claim that the value is
             // within the range of `from_width`.
@@ -1158,17 +1409,14 @@ impl<'a> FactContext<'a> {
 
     /// Computes the `sextend` of a value with the given facts.
     pub fn sextend(&self, fact: &Fact, from_width: u16, to_width: u16) -> Option<Fact> {
+        let max_positive_value = 1u64 << (from_width - 1);
         match fact {
             // If we have a defined value in bits 0..bit_width, and
             // the MSB w.r.t. `from_width` is *not* set, then we can
             // do the same as `uextend`.
             Fact::Range {
-                bit_width,
-                // We can ignore `min`: it is always <= max in
-                // unsigned terms, and we check max's LSB below.
-                min: _,
-                max,
-            } if *bit_width == from_width && (*max & (1 << (*bit_width - 1)) == 0) => {
+                bit_width, range, ..
+            } if *bit_width == from_width && range.le_expr(&Expr::constant(max_positive_value)) => {
                 self.uextend(fact, from_width, to_width)
             }
             _ => None,
@@ -1189,24 +1437,15 @@ impl<'a> FactContext<'a> {
         );
 
         match fact {
-            Fact::Range {
-                bit_width,
-                min,
-                max,
-            } if *bit_width == from_width => {
+            Fact::Range { bit_width, range } if *bit_width == from_width => {
                 let max_val = (1u64 << to_width) - 1;
-                if *min <= max_val && *max <= max_val {
+                if range.le_expr(&Expr::constant(max_val)) {
                     Some(Fact::Range {
                         bit_width: to_width,
-                        min: *min,
-                        max: *max,
+                        range: range.clone(),
                     })
                 } else {
-                    Some(Fact::Range {
-                        bit_width: to_width,
-                        min: 0,
-                        max: max_val,
-                    })
+                    Some(Fact::max_range_for_width(to_width))
                 }
             }
             _ => None,
@@ -1217,23 +1456,10 @@ impl<'a> FactContext<'a> {
     pub fn scale(&self, fact: &Fact, width: u16, factor: u32) -> Option<Fact> {
         let result = match fact {
             x if factor == 1 => Some(x.clone()),
-
-            Fact::Range {
-                bit_width,
-                min,
-                max,
-            } if *bit_width == width => {
-                let min = min.checked_mul(u64::from(factor))?;
-                let max = max.checked_mul(u64::from(factor))?;
-                if *bit_width < 64 && max > max_value_for_width(width) {
-                    return None;
-                }
-                Some(Fact::Range {
-                    bit_width: *bit_width,
-                    min,
-                    max,
-                })
-            }
+            Fact::Range { bit_width, range } if *bit_width == width => Some(Fact::Range {
+                bit_width: *bit_width,
+                range: range.scale(factor).clamp(width),
+            }),
             _ => None,
         };
         trace!("scale: {fact:?} * {factor} at width {width} -> {result:?}");
@@ -1249,140 +1475,53 @@ impl<'a> FactContext<'a> {
         self.scale(fact, width, factor)
     }
 
-    /// Offsets a value with a fact by a known amount.
-    pub fn offset(&self, fact: &Fact, width: u16, offset: i64) -> Option<Fact> {
-        if offset == 0 {
-            return Some(fact.clone());
-        }
-
-        let compute_offset = |base: u64| -> Option<u64> {
-            if offset >= 0 {
-                base.checked_add(u64::try_from(offset).unwrap())
-            } else {
-                base.checked_sub(u64::try_from(-offset).unwrap())
-            }
-        };
-
-        let result = match fact {
-            Fact::Range {
-                bit_width,
-                min,
-                max,
-            } if *bit_width == width => {
-                let min = compute_offset(*min)?;
-                let max = compute_offset(*max)?;
-                Some(Fact::Range {
-                    bit_width: *bit_width,
-                    min,
-                    max,
-                })
-            }
-            Fact::DynamicRange {
-                bit_width,
-                min,
-                max,
-            } if *bit_width == width => {
-                let min = Expr::offset(min, offset)?;
-                let max = Expr::offset(max, offset)?;
-                Some(Fact::DynamicRange {
-                    bit_width: *bit_width,
-                    min,
-                    max,
-                })
-            }
-            Fact::Mem {
-                ty,
-                min_offset: mem_min_offset,
-                max_offset: mem_max_offset,
-                nullable: false,
-            } => {
-                let min_offset = compute_offset(*mem_min_offset)?;
-                let max_offset = compute_offset(*mem_max_offset)?;
-                Some(Fact::Mem {
-                    ty: *ty,
-                    min_offset,
-                    max_offset,
-                    nullable: false,
-                })
-            }
-            Fact::DynamicMem {
-                ty,
-                min,
-                max,
-                nullable: false,
-            } => {
-                let min = Expr::offset(min, offset)?;
-                let max = Expr::offset(max, offset)?;
-                Some(Fact::DynamicMem {
-                    ty: *ty,
-                    min,
-                    max,
-                    nullable: false,
-                })
-            }
-            _ => None,
-        };
-        trace!("offset: {fact:?} + {offset} in width {width} -> {result:?}");
-        result
-    }
-
     /// Check that accessing memory via a pointer with this fact, with
     /// a memory access of the given size, is valid.
     ///
     /// If valid, returns the memory type and offset into that type
     /// that this address accesses, if known, or `None` if the range
     /// doesn't constrain the access to exactly one location.
-    fn check_address(&self, fact: &Fact, size: u32) -> PccResult<Option<(ir::MemoryType, u64)>> {
-        trace!("check_address: fact {:?} size {}", fact, size);
+    fn check_address(
+        &self,
+        fact: &Fact,
+        access_size: u32,
+    ) -> PccResult<Option<(ir::MemoryType, u64)>> {
+        trace!("check_address: fact {:?} access_size {}", fact, access_size);
+
         match fact {
             Fact::Mem {
                 ty,
-                min_offset,
-                max_offset,
+                range,
                 nullable: _,
             } => {
-                let end_offset: u64 = max_offset
-                    .checked_add(u64::from(size))
-                    .ok_or(PccError::Overflow)?;
+                trace!(" -> memory type: {}", self.function.memory_types[*ty]);
                 match &self.function.memory_types[*ty] {
                     ir::MemoryTypeData::Struct { size, .. }
                     | ir::MemoryTypeData::Memory { size } => {
-                        ensure!(end_offset <= *size, OutOfBounds)
+                        ensure!(u64::from(access_size) <= *size, OutOfBounds);
+                        let effective_size = *size - u64::from(access_size);
+                        ensure!(range.le_expr(&Expr::constant(effective_size)), OutOfBounds);
+                    }
+                    ir::MemoryTypeData::DynamicMemory {
+                        gv,
+                        size: mem_static_size,
+                    } => {
+                        let effective_size = i128::from(*mem_static_size) - i128::from(access_size);
+                        let end = Expr::global_value_offset(*gv, effective_size);
+                        ensure!(range.le_expr(&end), OutOfBounds)
                     }
-                    ir::MemoryTypeData::DynamicMemory { .. } => bail!(OutOfBounds),
                     ir::MemoryTypeData::Empty => bail!(OutOfBounds),
                 }
-                let specific_ty_and_offset = if min_offset == max_offset {
-                    Some((*ty, *min_offset))
-                } else {
-                    None
-                };
+                let specific_ty_and_offset =
+                    if let Some(constant) = range.as_const().and_then(|i| u64::try_from(i).ok()) {
+                        Some((*ty, constant))
+                    } else {
+                        None
+                    };
+                trace!(" -> specific type and offset: {specific_ty_and_offset:?}");
                 Ok(specific_ty_and_offset)
             }
-            Fact::DynamicMem {
-                ty,
-                min: _,
-                max:
-                    Expr {
-                        base: BaseExpr::GlobalValue(max_gv),
-                        offset: max_offset,
-                    },
-                nullable: _,
-            } => match &self.function.memory_types[*ty] {
-                ir::MemoryTypeData::DynamicMemory {
-                    gv,
-                    size: mem_static_size,
-                } if gv == max_gv => {
-                    let end_offset = max_offset
-                        .checked_add(i64::from(size))
-                        .ok_or(PccError::Overflow)?;
-                    let mem_static_size =
-                        i64::try_from(*mem_static_size).map_err(|_| PccError::Overflow)?;
-                    ensure!(end_offset <= mem_static_size, OutOfBounds);
-                    Ok(None)
-                }
-                _ => bail!(OutOfBounds),
-            },
+
             _ => bail!(OutOfBounds),
         }
     }
@@ -1409,12 +1548,14 @@ impl<'a> FactContext<'a> {
             }
             Ok(Some(field))
         } else {
-            // Access to valid memory, but not a struct: no facts can be attached to the result.
+            // Access to valid memory, but not a struct: no facts can
+            // be attached to the result.
             Ok(None)
         }
     }
 
-    /// Check a load, and determine what fact, if any, the result of the load might have.
+    /// Check a load, and determine what fact, if any, the result of
+    /// the load might have.
     pub fn load<'b>(&'b self, fact: &Fact, access_ty: ir::Type) -> PccResult<Option<&'b Fact>> {
         Ok(self
             .struct_field(fact, access_ty)?
@@ -1433,7 +1574,8 @@ impl<'a> FactContext<'a> {
             if field.readonly {
                 bail!(WriteToReadOnlyField);
             }
-            // Check that the fact on the stored data subsumes the field's fact.
+            // Check that the fact on the stored data subsumes the
+            // field's fact.
             if !self.subsumes_fact_optionals(data_fact, field.fact()) {
                 bail!(InvalidStoredFact);
             }
@@ -1441,10 +1583,11 @@ impl<'a> FactContext<'a> {
         Ok(())
     }
 
-    /// Apply a known inequality to rewrite dynamic bounds using transitivity, if possible.
+    /// Apply a known inequality to rewrite dynamic bounds using
+    /// transitivity, if possible.
     ///
-    /// Given that `lhs >= rhs` (if not `strict`) or `lhs > rhs` (if
-    /// `strict`), update `fact`.
+    /// Given that `lhs >= rhs` (if `kind` is not `strict`) or `lhs >
+    /// rhs` (if `kind` is `strict`), update `fact`.
     pub fn apply_inequality(
         &self,
         fact: &Fact,
@@ -1452,179 +1595,74 @@ impl<'a> FactContext<'a> {
         rhs: &Fact,
         kind: InequalityKind,
     ) -> Fact {
-        let result = match (
-            lhs.as_symbol(),
-            lhs.as_const(self.pointer_width)
-                .and_then(|k| i64::try_from(k).ok()),
-            rhs.as_symbol(),
-            fact,
-        ) {
-            (
-                Some(lhs),
-                None,
-                Some(rhs),
-                Fact::DynamicMem {
-                    ty,
-                    min,
-                    max,
-                    nullable,
-                },
-            ) if rhs.base == max.base => {
-                let strict_offset = match kind {
-                    InequalityKind::Strict => 1,
-                    InequalityKind::Loose => 0,
+        trace!("apply_inequality: fact {fact:?} lhs {lhs:?} rhs {rhs:?} kind {kind:?}");
+
+        // The basic idea is that if `fact` is <= RHS, and RHS <= LHS,
+        // then we know that `fact` is <= LHS as well (transitivity).
+        //
+        // We thus first check if `fact` is indeed <= RHS: are any of
+        // its upper bounds <= any lower or equal bounds on RHS? If
+        // so, what is the minimum headroom (known difference)? E.g.,
+        // if `fact` is known to be `v1`, and RHS is equal to or
+        // greater than `v1 + 4`, then the known difference is at
+        // least 4.
+        //
+        // If such a difference is known, we then take all lower,
+        // equal and upper bounds of LHS, add that offset, and add
+        // these as upper bounds on `fact`. So for example, if we know
+        // that `v1 + 4 <= gv1`, then we can update the fact to be
+        // `range(bit_width, {}, =v1, gv1 - 4)`: it is still equal to
+        // `v1`, but it is also at most `gv1 - 4`.
+
+        let result = if let (Some(fact_range), Some(lhs_range), Some(rhs_range)) =
+            (fact.range(), lhs.range(), rhs.range())
+        {
+            let offset = fact_range
+                .equal
+                .iter()
+                .chain(fact_range.max.iter())
+                .flat_map(|fact_expr| {
+                    rhs_range
+                        .min
+                        .iter()
+                        .chain(rhs_range.equal.iter())
+                        .flat_map(|rhs_expr| Expr::difference(rhs_expr, fact_expr))
+                })
+                .max();
+
+            // Positive offset indicates that RHS is greater than fact by that amount.
+            if let Some(offset) = offset {
+                let offset = match kind {
+                    InequalityKind::Loose => offset,
+                    // If the inequality is strict, we get
+                    // one extra free increment: x < y
+                    // implies x <= y - 1.
+                    InequalityKind::Strict => offset + 1,
                 };
-                if let Some(offset) = max
-                    .offset
-                    .checked_add(lhs.offset)
-                    .and_then(|x| x.checked_sub(rhs.offset))
-                    .and_then(|x| x.checked_sub(strict_offset))
-                {
-                    let new_max = Expr {
-                        base: lhs.base.clone(),
-                        offset,
-                    };
-                    Fact::DynamicMem {
-                        ty: *ty,
-                        min: min.clone(),
-                        max: new_max,
-                        nullable: *nullable,
-                    }
-                } else {
-                    fact.clone()
-                }
-            }
-
-            (
-                None,
-                Some(lhs_const),
-                Some(rhs),
-                Fact::DynamicMem {
-                    ty,
-                    min: _,
+                let new_upper_bounds = lhs_range
+                    .min
+                    .iter()
+                    .chain(lhs_range.equal.iter())
+                    .flat_map(|e| Expr::offset(e, -offset));
+                let max = fact_range
+                    .max
+                    .iter()
+                    .cloned()
+                    .chain(new_upper_bounds)
+                    .collect::<SmallVec<[Expr; 1]>>();
+                fact.with_range(ValueRange {
+                    min: fact_range.min.clone(),
+                    equal: fact_range.equal.clone(),
                     max,
-                    nullable,
-                },
-            ) if rhs.base == max.base => {
-                let strict_offset = match kind {
-                    InequalityKind::Strict => 1,
-                    InequalityKind::Loose => 0,
-                };
-                if let Some(offset) = max
-                    .offset
-                    .checked_add(lhs_const)
-                    .and_then(|x| x.checked_sub(rhs.offset))
-                    .and_then(|x| x.checked_sub(strict_offset))
-                {
-                    Fact::Mem {
-                        ty: *ty,
-                        min_offset: 0,
-                        max_offset: u64::try_from(offset).unwrap_or(0),
-                        nullable: *nullable,
-                    }
-                } else {
-                    fact.clone()
-                }
+                })
+            } else {
+                fact.clone()
             }
-
-            _ => fact.clone(),
+        } else {
+            fact.clone()
         };
-        trace!("apply_inequality({fact:?}, {lhs:?}, {rhs:?}, {kind:?} -> {result:?}");
-        result
-    }
-
-    /// Compute the union of two facts, if possible.
-    pub fn union(&self, lhs: &Fact, rhs: &Fact) -> Option<Fact> {
-        let result = match (lhs, rhs) {
-            (lhs, rhs) if lhs == rhs => Some(lhs.clone()),
-
-            (
-                Fact::DynamicMem {
-                    ty: ty_lhs,
-                    min: min_lhs,
-                    max: max_lhs,
-                    nullable: nullable_lhs,
-                },
-                Fact::DynamicMem {
-                    ty: ty_rhs,
-                    min: min_rhs,
-                    max: max_rhs,
-                    nullable: nullable_rhs,
-                },
-            ) if ty_lhs == ty_rhs => Some(Fact::DynamicMem {
-                ty: *ty_lhs,
-                min: Expr::min(min_lhs, min_rhs),
-                max: Expr::max(max_lhs, max_rhs),
-                nullable: *nullable_lhs || *nullable_rhs,
-            }),
 
-            (
-                Fact::Range {
-                    bit_width: bw_const,
-                    min: 0,
-                    max: 0,
-                },
-                Fact::DynamicMem {
-                    ty,
-                    min,
-                    max,
-                    nullable: _,
-                },
-            )
-            | (
-                Fact::DynamicMem {
-                    ty,
-                    min,
-                    max,
-                    nullable: _,
-                },
-                Fact::Range {
-                    bit_width: bw_const,
-                    min: 0,
-                    max: 0,
-                },
-            ) if *bw_const == self.pointer_width => Some(Fact::DynamicMem {
-                ty: *ty,
-                min: min.clone(),
-                max: max.clone(),
-                nullable: true,
-            }),
-
-            (
-                Fact::Range {
-                    bit_width: bw_const,
-                    min: 0,
-                    max: 0,
-                },
-                Fact::Mem {
-                    ty,
-                    min_offset,
-                    max_offset,
-                    nullable: _,
-                },
-            )
-            | (
-                Fact::Mem {
-                    ty,
-                    min_offset,
-                    max_offset,
-                    nullable: _,
-                },
-                Fact::Range {
-                    bit_width: bw_const,
-                    min: 0,
-                    max: 0,
-                },
-            ) if *bw_const == self.pointer_width => Some(Fact::Mem {
-                ty: *ty,
-                min_offset: *min_offset,
-                max_offset: *max_offset,
-                nullable: true,
-            }),
-
-            _ => None,
-        };
-        trace!("union({lhs:?}, {rhs:?}) -> {result:?}");
+        trace!("apply_inequality({fact:?}, {lhs:?}, {rhs:?}, {kind:?} -> {result:?}");
         result
     }
 }
diff --git a/cranelift/codegen/src/isa/aarch64/pcc.rs b/cranelift/codegen/src/isa/aarch64/pcc.rs
index fe9dc8a4617..e38d8d48635 100644
--- a/cranelift/codegen/src/isa/aarch64/pcc.rs
+++ b/cranelift/codegen/src/isa/aarch64/pcc.rs
@@ -128,7 +128,7 @@ pub(crate) fn check(
                 ctx,
                 64,
                 size.bits().into(),
-                ctx.offset(&rn, size.bits().into(), imm12),
+                rn.offset(size.bits().into(), imm12),
             )
         }),
         Inst::AluRRImm12 {
@@ -143,7 +143,7 @@ pub(crate) fn check(
                 ctx,
                 64,
                 size.bits().into(),
-                ctx.offset(&rn, size.bits().into(), -imm12),
+                rn.offset(size.bits().into(), -imm12),
             )
         }),
         Inst::AluRRR {
@@ -153,12 +153,12 @@ pub(crate) fn check(
             rn,
             rm,
         } => check_binop(ctx, vcode, 64, rd, rn, rm, |rn, rm| {
-            if let Some(k) = rm.as_const(64) {
+            if let Some(k) = rm.as_const() {
                 clamp_range(
                     ctx,
                     64,
                     size.bits().into(),
-                    ctx.offset(rn, size.bits().into(), -(k as i64)),
+                    rn.offset(size.bits().into(), -(i64::try_from(k).unwrap())),
                 )
             } else {
                 clamp_range(ctx, 64, size.bits().into(), None)
@@ -247,6 +247,20 @@ pub(crate) fn check(
             Ok(())
         }
 
+        Inst::AluRRImm12 {
+            alu_op: ALUOp::SubS,
+            size,
+            rd,
+            rn,
+            imm12,
+        } if rd.to_reg() == zero_reg() => {
+            // Compare.
+            let rn = get_fact_or_default(vcode, rn, size.bits().into());
+            let rm = Fact::constant(size.bits().into(), imm12.value().into());
+            state.cmp_flags = Some((rn, rm));
+            Ok(())
+        }
+
         Inst::AluRRImmLogic {
             alu_op: ALUOp::Orr,
             size,
@@ -298,7 +312,8 @@ pub(crate) fn check(
 
         Inst::MovK { rd, rn, imm, .. } => {
             let input = get_fact_or_default(vcode, rn, 64);
-            if let Some(input_constant) = input.as_const(64) {
+            if let Some(input_constant) = input.as_const() {
+                let input_constant = u64::try_from(input_constant).unwrap();
                 let constant = u64::from(imm.bits) << (imm.shift * 16);
                 let constant = input_constant | constant;
                 check_constant(ctx, vcode, rd, 64, constant)
@@ -310,11 +325,18 @@ pub(crate) fn check(
         }
 
         Inst::CSel { rd, cond, rn, rm }
-            if (cond == Cond::Hs || cond == Cond::Hi) && cmp_flags.is_some() =>
+            if (cond == Cond::Hs || cond == Cond::Hi || cond == Cond::Ls || cond == Cond::Lo)
+                && cmp_flags.is_some() =>
         {
             let (cmp_lhs, cmp_rhs) = cmp_flags.unwrap();
             trace!("CSel: cmp {cond:?} ({cmp_lhs:?}, {cmp_rhs:?})");
 
+            let (cmp_lhs, cmp_rhs) = match cond {
+                Cond::Hs | Cond::Hi => (cmp_lhs, cmp_rhs),
+                Cond::Ls | Cond::Lo => (cmp_rhs, cmp_lhs),
+                _ => unreachable!(),
+            };
+
             check_output(ctx, vcode, rd, &[], |vcode| {
                 // We support transitivity-based reasoning. If the
                 // comparison establishes that
@@ -333,22 +355,22 @@ pub(crate) fn check(
                 // True side: lhs >= rhs (Hs) or lhs > rhs (Hi).
                 let rn = get_fact_or_default(vcode, rn, 64);
                 let lhs_kind = match cond {
-                    Cond::Hs => InequalityKind::Loose,
-                    Cond::Hi => InequalityKind::Strict,
+                    Cond::Hs | Cond::Ls => InequalityKind::Loose,
+                    Cond::Hi | Cond::Lo => InequalityKind::Strict,
                     _ => unreachable!(),
                 };
                 let rn = ctx.apply_inequality(&rn, &cmp_lhs, &cmp_rhs, lhs_kind);
                 // false side: rhs < lhs (Hs) or rhs <= lhs (Hi).
                 let rm = get_fact_or_default(vcode, rm, 64);
                 let rhs_kind = match cond {
-                    Cond::Hs => InequalityKind::Strict,
-                    Cond::Hi => InequalityKind::Loose,
+                    Cond::Hs | Cond::Ls => InequalityKind::Strict,
+                    Cond::Hi | Cond::Lo => InequalityKind::Loose,
                     _ => unreachable!(),
                 };
                 let rm = ctx.apply_inequality(&rm, &cmp_rhs, &cmp_lhs, rhs_kind);
-                let union = ctx.union(&rn, &rm);
+                let union = Fact::union(&rn, &rm);
                 // Union the two facts.
-                clamp_range(ctx, 64, 64, union)
+                clamp_range(ctx, 64, 64, Some(union))
             })
         }
 
@@ -475,7 +497,7 @@ fn check_addr<'a>(
         }
         &AMode::Unscaled { rn, simm9 } => {
             let rn = get_fact_or_default(vcode, rn, 64);
-            let sum = fail_if_missing(ctx.offset(&rn, 64, simm9.value.into()))?;
+            let sum = fail_if_missing(rn.offset(64, simm9.value.into()))?;
             check(&sum, ty)
         }
         &AMode::UnsignedOffset { rn, uimm12 } => {
@@ -490,7 +512,7 @@ fn check_addr<'a>(
             // This `unwrap()` will always succeed because the value
             // will always be positive and much smaller than
             // `i64::MAX` (see above).
-            let sum = fail_if_missing(ctx.offset(&rn, 64, i64::try_from(offset).unwrap()))?;
+            let sum = fail_if_missing(rn.offset(64, i64::try_from(offset).unwrap()))?;
             check(&sum, ty)
         }
         &AMode::Label { .. } | &AMode::Const { .. } => {
@@ -500,7 +522,7 @@ fn check_addr<'a>(
         }
         &AMode::RegOffset { rn, off, .. } => {
             let rn = get_fact_or_default(vcode, rn, 64);
-            let sum = fail_if_missing(ctx.offset(&rn, 64, off))?;
+            let sum = fail_if_missing(rn.offset(64, off))?;
             check(&sum, ty)
         }
         &AMode::SPOffset { .. }
diff --git a/cranelift/codegen/src/isa/x64/pcc.rs b/cranelift/codegen/src/isa/x64/pcc.rs
index 6fa8f886e3a..f0fba3c8f2d 100644
--- a/cranelift/codegen/src/isa/x64/pcc.rs
+++ b/cranelift/codegen/src/isa/x64/pcc.rs
@@ -93,7 +93,7 @@ pub(crate) fn check(
                     src1.to_reg(),
                     |src1| {
                         let simm32: i64 = simm32.into();
-                        clamp_range(ctx, 64, bits, ctx.offset(src1, bits, simm32))
+                        clamp_range(ctx, 64, bits, src1.offset(bits, simm32))
                     },
                 )
             }
@@ -124,7 +124,7 @@ pub(crate) fn check(
                     src1.to_reg(),
                     |src1| {
                         let simm32: i64 = simm32.into();
-                        clamp_range(ctx, 64, bits, ctx.offset(src1, bits, -simm32))
+                        clamp_range(ctx, 64, bits, src1.offset(bits, -simm32))
                     },
                 )
             }
@@ -508,8 +508,8 @@ pub(crate) fn check(
                     };
                     let in_false =
                         ctx.apply_inequality(&in_false, &cmp_rhs, &cmp_lhs, in_false_kind);
-                    let union = ctx.union(&in_true, &in_false);
-                    clamp_range(ctx, 64, 64, union)
+                    let union = Fact::union(&in_true, &in_false);
+                    clamp_range(ctx, 64, 64, Some(union))
                 })
             }
             _ => undefined_result(ctx, vcode, dst, 64, 64),
diff --git a/cranelift/codegen/src/machinst/lower.rs b/cranelift/codegen/src/machinst/lower.rs
index 32d841ebb5d..c4d8bea296c 100644
--- a/cranelift/codegen/src/machinst/lower.rs
+++ b/cranelift/codegen/src/machinst/lower.rs
@@ -1432,11 +1432,7 @@ impl<'func, I: VCodeInst> Lower<'func, I> {
         if self.flags.enable_pcc() {
             self.vregs.set_fact_if_missing(
                 reg.to_virtual_reg().unwrap(),
-                Fact::Range {
-                    bit_width,
-                    min,
-                    max,
-                },
+                Fact::static_value_two_ended_range(bit_width, min, max),
             );
         }
     }
diff --git a/cranelift/codegen/src/machinst/pcc.rs b/cranelift/codegen/src/machinst/pcc.rs
index d737d83dacc..17ca08fcdf0 100644
--- a/cranelift/codegen/src/machinst/pcc.rs
+++ b/cranelift/codegen/src/machinst/pcc.rs
@@ -29,11 +29,6 @@ pub(crate) fn clamp_range(
     from_bits: u16,
     fact: Option<Fact>,
 ) -> PccResult<Fact> {
-    let max = if from_bits == 64 {
-        u64::MAX
-    } else {
-        (1u64 << from_bits) - 1
-    };
     trace!(
         "clamp_range: fact {:?} from {} to {}",
         fact,
@@ -43,11 +38,7 @@ pub(crate) fn clamp_range(
     Ok(fact
         .and_then(|f| ctx.uextend(&f, from_bits, to_bits))
         .unwrap_or_else(|| {
-            let result = Fact::Range {
-                bit_width: to_bits,
-                min: 0,
-                max,
-            };
+            let result = Fact::max_range_for_width_extended(from_bits, to_bits);
             trace!(" -> clamping to {:?}", result);
             result
         }))
diff --git a/cranelift/filetests/filetests/pcc/fail/load.clif b/cranelift/filetests/filetests/pcc/fail/load.clif
index c4c086b1f19..4d1c7a9cebc 100644
--- a/cranelift/filetests/filetests/pcc/fail/load.clif
+++ b/cranelift/filetests/filetests/pcc/fail/load.clif
@@ -5,7 +5,7 @@ target x86_64
 
 function %f0(i64, i32) -> i64 {
     mt0 = memory 0x1000
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0x1000): i32):
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(32, 0, 0x1000): i32):
     v2 ! range(64, 0, 0x100) = uextend.i64 v1
     v3 ! mem(mt0, 0, 0x100) = iadd.i64 v0, v2
     v4 = load.i64 checked v3
@@ -15,7 +15,7 @@ block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0x1000): i32):
 ;; Insufficient guard region: the 8-byte load could go off the end.
 function %f1(i64, i32) -> i64 {
     mt0 = memory 0x1_0000_0000
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0xffff_ffff): i32):
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(32, 0, 0xffff_ffff): i32):
     v2 ! range(64, 0, 0xffff_ffff) = uextend.i64 v1
     v3 ! mem(mt0, 0, 0xffff_ffff) = iadd.i64 v0, v2
     v4 = load.i64 checked v3
@@ -35,7 +35,7 @@ block0(v0 ! mem(mt0, 0, 0x1000): i64, v1 ! range(32, 0, 0x1000): i32):
 ;; RegReg mode on aarch64.
 function %f3(i64, i64) -> i8 {
     mt0 = memory 0x100
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(64, 0, 0xfff): i64):
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(64, 0, 0xfff): i64):
     v2 ! mem(mt0, 0, 0xfff) = iadd.i64 v0, v1
     v3 = load.i8 checked v2
     return v3
@@ -44,7 +44,7 @@ block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(64, 0, 0xfff): i64):
 ;; RegScaledExtended mode on aarch64.
 function %f4(i64, i32) -> i64 {
     mt0 = memory 0x7000
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0xfff): i32):
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(32, 0, 0xfff): i32):
     v2 ! range(64, 0, 0xfff) = uextend.i64 v1
     v3 = iconst.i32 3
     v4 ! range(64, 0, 0x7ff8) = ishl.i64 v2, v3
@@ -56,7 +56,7 @@ block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0xfff): i32):
 ;; RegScaled mode on aarch64.
 function %f5(i64, i64) -> i64 {
     mt0 = memory 0x7000
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(64, 0, 0xfff): i64):
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(64, 0, 0xfff): i64):
     v2 = iconst.i32 3
     v3 ! range(64, 0, 0x7ff8) = ishl.i64 v1, v2
     v4 ! mem(mt0, 0, 0x7ff8) = iadd.i64 v0, v3
diff --git a/cranelift/filetests/filetests/pcc/fail/memtypes.clif b/cranelift/filetests/filetests/pcc/fail/memtypes.clif
index 6f5b12a3830..fa576b10d9f 100644
--- a/cranelift/filetests/filetests/pcc/fail/memtypes.clif
+++ b/cranelift/filetests/filetests/pcc/fail/memtypes.clif
@@ -6,7 +6,7 @@ target x86_64
 function %f0(i64) -> i32 {
     mt0 = struct 8 { 4: i32, 0: i32 } ; error: out-of-order
 
-block0(v0 ! mem(mt0, 0, 0): i64):
+block0(v0 ! mem(mt0, =0): i64):
     v1 = load.i32 v0+0
     return v1
 }
@@ -15,7 +15,7 @@ function %f1(i64) -> i32 {
     ;; out-of-bounds field:
     mt0 = struct 8 { 0: i32, 6: i32 } ; error: field at offset 6 of size 4 that overflows
 
-block0(v0 ! mem(mt0, 0, 0): i64):
+block0(v0 ! mem(mt0, =0): i64):
     v1 = load.i32 v0+0
     return v1
 }
@@ -24,7 +24,7 @@ function %f2(i64) -> i32 {
     ;; overflowing offset + field size:
     mt0 = struct 8 { 0: i32, 0xffff_ffff_ffff_ffff: i32 } ; error: field at offset 18446744073709551615 of size 4; offset plus size overflows a u64
 
-block0(v0 ! mem(mt0, 0, 0): i64):
+block0(v0 ! mem(mt0, =0): i64):
     v1 = load.i32 v0+0
     return v1
 }
diff --git a/cranelift/filetests/filetests/pcc/fail/simple.clif b/cranelift/filetests/filetests/pcc/fail/simple.clif
index 45b2e9ab665..35576157b74 100644
--- a/cranelift/filetests/filetests/pcc/fail/simple.clif
+++ b/cranelift/filetests/filetests/pcc/fail/simple.clif
@@ -8,7 +8,7 @@ target x86_64
 
 function %simple1(i64 vmctx, i32) -> i8 {
     mt0 = memory 0x8000_0000
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0xffff_ffff): i32):
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(32, 0, 0xffff_ffff): i32):
     v2 ! range(64, 0, 0xffff_ffff) = uextend.i64 v1
     v3 ! mem(mt0, 0, 0xffff_ffff) = iadd.i64 v0, v2
     v4 = load.i8 checked v3
@@ -19,9 +19,9 @@ block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0xffff_ffff): i32):
 
 function %simple2(i64 vmctx, i32) -> i8 {
     mt0 = memory 0x8000_0000
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0xffff_ffff): i32):
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(32, 0, 0xffff_ffff): i32):
     v2 ! range(64, 0, 0xffff_ffff) = uextend.i64 v1
-    v3 ! mem(mt0, 0, 0) = iadd.i64 v0, v2
+    v3 ! mem(mt0, =0) = iadd.i64 v0, v2
     v4 = load.i8 checked v3
     return v4
 }
diff --git a/cranelift/filetests/filetests/pcc/fail/struct.clif b/cranelift/filetests/filetests/pcc/fail/struct.clif
index 88d905e32e3..def827e40ec 100644
--- a/cranelift/filetests/filetests/pcc/fail/struct.clif
+++ b/cranelift/filetests/filetests/pcc/fail/struct.clif
@@ -4,17 +4,17 @@ target aarch64
 target x86_64
 
 function %f0(i64) -> i64 {
-    mt0 = struct 8 { 0: i64 ! mem(mt1, 0, 0) }
+    mt0 = struct 8 { 0: i64 ! mem(mt1, =0) }
     mt1 = memory 0x1_0000_0000
-block0(v0 ! mem(mt0, 0, 0): i64):
-    v1 ! mem(mt1, 8, 8) = load.i64 checked v0
+block0(v0 ! mem(mt0, =0): i64):
+    v1 ! mem(mt1, 8, 16) = load.i64 checked v0
     return v1
 }
 
 function %f1(i64, i64) {
-    mt0 = struct 8 { 0: i64 ! mem(mt1, 0, 0) }
+    mt0 = struct 8 { 0: i64 ! mem(mt1, =0) }
     mt1 = memory 0x1_0000_0000
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! mem(mt1, 8, 8): i64):
+block0(v0 ! mem(mt0, =0): i64, v1 ! mem(mt1, 8, 8): i64):
     store.i64 checked v1, v0
     return
 }
diff --git a/cranelift/filetests/filetests/pcc/fail/vmctx.clif b/cranelift/filetests/filetests/pcc/fail/vmctx.clif
index 1dc947bf21f..73241667cfd 100644
--- a/cranelift/filetests/filetests/pcc/fail/vmctx.clif
+++ b/cranelift/filetests/filetests/pcc/fail/vmctx.clif
@@ -6,14 +6,14 @@ target x86_64
 ;; Equivalent to a Wasm `i64.load` from a static memory.
 function %f0(i64, i32) -> i64 {
     ;; mock vmctx struct:
-    mt0 = struct 8 { 0: i64 readonly ! mem(mt1, 0, 0) }
+    mt0 = struct 8 { 0: i64 readonly ! mem(mt1, =0) }
     ;; mock static memory: 4GiB range, *but insufficient guard*
     mt1 = memory 0x1_0000_0000
 
-block0(v0 ! mem(mt0, 0, 0): i64, v1: i32):
+block0(v0 ! mem(mt0, =0): i64, v1: i32):
     ;; Compute the address: base + offset. Guard region (2GiB) is
     ;; sufficient for an 8-byte I64 load.
-    v2 ! mem(mt1, 0, 0) = load.i64 checked v0+0    ;; base pointer
+    v2 ! mem(mt1, =0) = load.i64 checked v0+0      ;; base pointer
     v3 ! range(64, 0, 0xffff_ffff) = uextend.i64 v1  ;; offset
     v4 ! mem(mt1, 0, 0xffff_ffff) = iadd.i64 v2, v3
     v5 = load.i64 checked v4
@@ -23,14 +23,14 @@ block0(v0 ! mem(mt0, 0, 0): i64, v1: i32):
 ;; Equivalent to a Wasm `i64.load` from a static memory.
 function %f1(i64, i32) -> i64 {
     ;; mock vmctx struct:
-    mt0 = struct 16 { 0: i64 readonly ! mem(mt1, 0, 0), 8: i64 readonly }
+    mt0 = struct 16 { 0: i64 readonly ! mem(mt1, =0), 8: i64 readonly }
     ;; mock static memory: 4GiB range, *but insufficient guard*
     mt1 = memory 0x1_8000_0000
 
-block0(v0 ! mem(mt0, 0, 0): i64, v1: i32):
+block0(v0 ! mem(mt0, =0): i64, v1: i32):
     ;; Compute the address: base + offset. Guard region (2GiB) is
     ;; sufficient for an 8-byte I64 load.
-    v2 ! mem(mt1, 0, 0) = load.i64 checked v0+8    ;; base pointer, but the wrong one
+    v2 ! mem(mt1, =0) = load.i64 checked v0+8      ;; base pointer, but the wrong one
     v3 ! range(64, 0, 0xffff_ffff) = uextend.i64 v1  ;; offset
     v4 ! mem(mt1, 0, 0xffff_ffff) = iadd.i64 v2, v3
     v5 = load.i64 checked v4
diff --git a/cranelift/filetests/filetests/pcc/succeed/const.clif b/cranelift/filetests/filetests/pcc/succeed/const.clif
index 529c43eaa39..e4c798157e0 100644
--- a/cranelift/filetests/filetests/pcc/succeed/const.clif
+++ b/cranelift/filetests/filetests/pcc/succeed/const.clif
@@ -5,15 +5,15 @@ target x86_64
 
 function %f0() {
 block0:
-    v0 ! range(64, 0, 0) = iconst.i64 0
-    v1 ! range(64, 1, 1) = iconst.i64 1
-    v2 ! range(64, 0xfff, 0xfff) = iconst.i64 0xfff
-    v3 ! range(64, 0x10000, 0x10000) = iconst.i64 0x10000
-    v4 ! range(64, 0xffffc, 0xffffc) = iconst.i64 0xffffc
-    v5 ! range(64, 0x1_0000_0000, 0x1_0000_0000) = iconst.i64 0x1_0000_0000
-    v6 ! range(64, 0x1_0000_0000_0000, 0x1_0000_0000_0000) = iconst.i64 0x1_0000_0000_0000
-    v7 ! range(64, 0xffff_0000_0000_0000, 0xffff_0000_0000_0000) = iconst.i64 0xffff_0000_0000_0000
-    v8 ! range(64, 0xffff_0000_0000_ffff, 0xffff_0000_0000_ffff) = iconst.i64 0xffff_0000_0000_ffff
+    v0 ! range(64, =0) = iconst.i64 0
+    v1 ! range(64, =1) = iconst.i64 1
+    v2 ! range(64, =0xfff) = iconst.i64 0xfff
+    v3 ! range(64, =0x10000) = iconst.i64 0x10000
+    v4 ! range(64, =0xffffc) = iconst.i64 0xffffc
+    v5 ! range(64, =0x1_0000_0000) = iconst.i64 0x1_0000_0000
+    v6 ! range(64, =0x1_0000_0000_0000) = iconst.i64 0x1_0000_0000_0000
+    v7 ! range(64, =0xffff_0000_0000_0000) = iconst.i64 0xffff_0000_0000_0000
+    v8 ! range(64, =0xffff_0000_0000_ffff) = iconst.i64 0xffff_0000_0000_ffff
     return
 }
 
diff --git a/cranelift/filetests/filetests/pcc/succeed/dynamic.clif b/cranelift/filetests/filetests/pcc/succeed/dynamic.clif
index 13f96bc8b3b..e5b381e3efe 100644
--- a/cranelift/filetests/filetests/pcc/succeed/dynamic.clif
+++ b/cranelift/filetests/filetests/pcc/succeed/dynamic.clif
@@ -11,32 +11,32 @@ function %f0(i64 vmctx, i32) -> i64 {
     
     ;; mock vmctx struct:
     mt0 = struct 16 {
-        0: i64 readonly ! dynamic_mem(mt1, 0, 0),
-        8: i64 readonly ! dynamic_range(64, gv2, gv2),
+        0: i64 readonly ! mem(mt1, =0),
+        8: i64 readonly ! range(64, =gv2),
     }
     ;; mock dynamic memory: dynamic range, plus 2GiB guard
     mt1 = dynamic_memory gv2 + 0x8000_0000
 
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! dynamic_range(32, v1, v1): i32):
-    v2 ! dynamic_range(64, v1, v1)            = uextend.i64 v1       ;; extended Wasm offset
-    v3 ! dynamic_mem(mt1, 0, 0)               = global_value.i64 gv1 ;; base
-    v4 ! dynamic_range(64, gv2, gv2)          = global_value.i64 gv2 ;; size
-    v5 ! compare(uge, v1, gv2)                = icmp.i64 uge v2, v4  ;; bounds-check compare of extended Wasm offset to size
-    v6 ! dynamic_mem(mt1, v1, v1)             = iadd.i64 v3, v2      ;; compute access address: memory base plus extended Wasm offset
-    v7 ! dynamic_mem(mt1, 0, 0, nullable)     = iconst.i64 0         ;; null pointer for speculative path
-    v8 ! dynamic_mem(mt1, 0, gv2-1, nullable) = select_spectre_guard v5, v7, v6  ;; if OOB, pick null, otherwise the real address
-    v9                                        = load.i64 checked v8
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(32, =v1): i32):
+    v2 ! range(64, =v1)               = uextend.i64 v1       ;; extended Wasm offset
+    v3 ! mem(mt1, =0)                 = global_value.i64 gv1 ;; base
+    v4 ! range(64, =gv2)              = global_value.i64 gv2 ;; size
+    v5 ! compare(uge, v1, gv2)        = icmp.i64 uge v2, v4  ;; bounds-check compare of extended Wasm offset to size
+    v6 ! mem(mt1, =v1)                = iadd.i64 v3, v2      ;; compute access address: memory base plus extended Wasm offset
+    v7 ! mem(mt1, nullable, =0)       = iconst.i64 0         ;; null pointer for speculative path
+    v8 ! mem(mt1, nullable, 0, gv2-1) = select_spectre_guard v5, v7, v6  ;; if OOB, pick null, otherwise the real address
+    v9                                = load.i64 checked v8
     return v9
 }
 
 ;; select sees:
 ;;  v5 ! compare(uge, v1, gv2)
-;;  v6 ! dynamic_mem(mt1, v1, v1)
-;;  v7 ! dynamic_mem(mt0, 0, 0, nullable)
+;;  v6 ! mem(mt1, =v1)
+;;  v7 ! mem(mt0, nullable, 0)
 ;;
 ;; preprocess:
-;; v6' (assuming compare is false) = dynamic_mem(mt1, 0, gv2-1)
-;; v7' (assuming compare is true)  = dynamic_mem(mt1, 0, 0, nullable)
+;; v6' (assuming compare is false) = mem(mt1, 0, gv2-1)
+;; v7' (assuming compare is true)  = mem(mt1, nullable, 0)
 ;;
 ;; take the union of range and nullability:
-;; dynamic_mem(mt1, 0, gv2-1, nullable)
+;; mem(mt1, nullable, 0, gv2-1)
diff --git a/cranelift/filetests/filetests/pcc/succeed/gv_fact.clif b/cranelift/filetests/filetests/pcc/succeed/gv_fact.clif
index 329b8d444ed..cd963fb4c40 100644
--- a/cranelift/filetests/filetests/pcc/succeed/gv_fact.clif
+++ b/cranelift/filetests/filetests/pcc/succeed/gv_fact.clif
@@ -4,55 +4,55 @@ target aarch64
 target x86_64
 
 function %f0(i64 vmctx) -> i64 {
-    mt0 = struct 16 { 8: i64 ! mem(mt1, 0, 0) }
+    mt0 = struct 16 { 8: i64 ! mem(mt1, =0) }
     mt1 = memory 0x1_0000_0000
-    gv0 ! mem(mt0, 0, 0) = vmctx
-    gv1 ! mem(mt1, 0, 0) = load.i64 notrap aligned checked gv0+8
+    gv0 ! mem(mt0, =0) = vmctx
+    gv1 ! mem(mt1, =0) = load.i64 notrap aligned checked gv0+8
     
-block0(v0 ! mem(mt0, 0, 0): i64):
-    v1 ! mem(mt1, 0, 0) = global_value.i64 gv1
+block0(v0 ! mem(mt0, =0): i64):
+    v1 ! mem(mt1, =0) = global_value.i64 gv1
     return v1
 }
 
 function %f1(i64 vmctx) -> i64 {
-    mt0 = struct 16 { 8: i64 ! mem(mt1, 0, 0) }
-    mt1 = struct 8 { 0: i64 ! mem(mt2, 0, 0) }
+    mt0 = struct 16 { 8: i64 ! mem(mt1, =0) }
+    mt1 = struct 8 { 0: i64 ! mem(mt2, =0) }
     mt2 = memory 0x1_0000_0000
-    gv0 ! mem(mt0, 0, 0) = vmctx
-    gv1 ! mem(mt1, 0, 0) = load.i64 notrap aligned checked gv0+8
-    gv2 ! mem(mt2, 0, 0) = load.i64 notrap aligned checked gv1+0
+    gv0 ! mem(mt0, =0) = vmctx
+    gv1 ! mem(mt1, =0) = load.i64 notrap aligned checked gv0+8
+    gv2 ! mem(mt2, =0) = load.i64 notrap aligned checked gv1+0
     
-block0(v0 ! mem(mt0, 0, 0): i64):
-    v1 ! mem(mt2, 0, 0) = global_value.i64 gv2
+block0(v0 ! mem(mt0, =0): i64):
+    v1 ! mem(mt2, =0) = global_value.i64 gv2
     return v1
 }
 
 function %f2(i64 vmctx) -> i64 {
-    mt0 = struct 16 { 8: i64 ! mem(mt1, 0, 0) }
-    mt1 = struct 8 { 0: i64 ! mem(mt2, 0, 0) }
+    mt0 = struct 16 { 8: i64 ! mem(mt1, =0) }
+    mt1 = struct 8 { 0: i64 ! mem(mt2, =0) }
     mt2 = memory 0x1_0000_0000
-    gv0 ! mem(mt0, 0, 0) = vmctx
-    gv1 ! mem(mt1, 0, 0) = load.i64 notrap aligned checked gv0+8
-    gv2 ! mem(mt2, 0, 0) = load.i64 notrap aligned checked gv1+0
-    gv3 ! mem(mt2, 8, 8) = iadd_imm.i64 gv2, 8
+    gv0 ! mem(mt0, =0) = vmctx
+    gv1 ! mem(mt1, =0) = load.i64 notrap aligned checked gv0+8
+    gv2 ! mem(mt2, =0) = load.i64 notrap aligned checked gv1+0
+    gv3 ! mem(mt2, =8) = iadd_imm.i64 gv2, 8
     
-block0(v0 ! mem(mt0, 0, 0): i64):
-    v1 ! mem(mt2, 8, 8) = global_value.i64 gv3
+block0(v0 ! mem(mt0, =0): i64):
+    v1 ! mem(mt2, =8) = global_value.i64 gv3
     return v1
 }
 
 function %f3(i64 vmctx) -> i64 {
-    mt0 = struct 16 { 8: i64 ! mem(mt1, 0, 0) }
-    mt1 = struct 8 { 0: i64 ! mem(mt2, 0, 0) }
+    mt0 = struct 16 { 8: i64 ! mem(mt1, =0) }
+    mt1 = struct 8 { 0: i64 ! mem(mt2, =0) }
     mt2 = memory 0x1_0000_0000
-    gv0 ! mem(mt0, 0, 0) = vmctx
-    gv1 ! mem(mt1, 0, 0) = load.i64 notrap aligned checked gv0+8
-    gv2 ! mem(mt2, 0, 0) = load.i64 notrap aligned checked gv1+0
-    gv3 ! mem(mt2, 8, 8) = iadd_imm.i64 gv2, 8
+    gv0 ! mem(mt0, =0) = vmctx
+    gv1 ! mem(mt1, =0) = load.i64 notrap aligned checked gv0+8
+    gv2 ! mem(mt2, =0) = load.i64 notrap aligned checked gv1+0
+    gv3 ! mem(mt2, =8) = iadd_imm.i64 gv2, 8
 
     ;; like the above, but with no fact provided on `v0`; it should
     ;; get copied from the GV.
 block0(v0: i64):
-    v1 ! mem(mt2, 8, 8) = global_value.i64 gv3
+    v1 ! mem(mt2, =8) = global_value.i64 gv3
     return v1
 }
diff --git a/cranelift/filetests/filetests/pcc/succeed/load.clif b/cranelift/filetests/filetests/pcc/succeed/load.clif
index 59996ef05fa..09902f9b977 100644
--- a/cranelift/filetests/filetests/pcc/succeed/load.clif
+++ b/cranelift/filetests/filetests/pcc/succeed/load.clif
@@ -5,9 +5,9 @@ target x86_64
 
 function %f0(i64, i32) -> i64 {
     mt0 = memory 0x1_0000_0000
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0x100): i32):
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(32, 0, 0x100): i32):
     v2 ! range(64, 0, 0x100) = uextend.i64 v1
-    v3 ! mem(mt0, 0, 8) = iadd.i64 v0, v2
+    v3 ! mem(mt0, 0, 0x100) = iadd.i64 v0, v2
     v4 = load.i64 checked v3
     return v4
 }
@@ -15,7 +15,7 @@ block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0x100): i32):
 function %f1(i64, i32) -> i64 {
     ;; Note the guard region of 8 bytes -- just enough for the below!
     mt0 = memory 0x1_0000_0008
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0xffff_ffff): i32):
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(32, 0, 0xffff_ffff): i32):
     v2 ! range(64, 0, 0xffff_ffff) = uextend.i64 v1
     v3 ! mem(mt0, 0, 0xffff_ffff) = iadd.i64 v0, v2
     v4 = load.i64 checked v3
@@ -25,7 +25,7 @@ block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0xffff_ffff): i32):
 ;; RegRegExtend mode on aarch64.
 function %f2(i64, i32) -> i8 {
     mt0 = memory 0x1000
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0xfff): i32):
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(32, 0, 0xfff): i32):
     v2 ! range(64, 0, 0xfff) = uextend.i64 v1
     v3 ! mem(mt0, 0, 0xfff) = iadd.i64 v0, v2
     v4 = load.i8 checked v3
@@ -35,7 +35,7 @@ block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0xfff): i32):
 ;; RegReg mode on aarch64.
 function %f3(i64, i64) -> i8 {
     mt0 = memory 0x1000
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(64, 0, 0xfff): i64):
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(64, 0, 0xfff): i64):
     v2 ! mem(mt0, 0, 0xfff) = iadd.i64 v0, v1
     v3 = load.i8 checked v2
     return v3
@@ -44,7 +44,7 @@ block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(64, 0, 0xfff): i64):
 ;; RegScaledExtended mode on aarch64.
 function %f4(i64, i32) -> i64 {
     mt0 = memory 0x8000
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0xfff): i32):
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(32, 0, 0xfff): i32):
     v2 ! range(64, 0, 0xfff) = uextend.i64 v1
     v3 = iconst.i32 3
     v4 ! range(64, 0, 0x7ff8) = ishl.i64 v2, v3
@@ -56,7 +56,7 @@ block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0xfff): i32):
 ;; RegScaled mode on aarch64.
 function %f5(i64, i64) -> i64 {
     mt0 = memory 0x8000
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(64, 0, 0xfff): i64):
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(64, 0, 0xfff): i64):
     v2 = iconst.i32 3
     v3 ! range(64, 0, 0x7ff8) = ishl.i64 v1, v2
     v4 ! mem(mt0, 0, 0x7ff8) = iadd.i64 v0, v3
@@ -67,9 +67,9 @@ block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(64, 0, 0xfff): i64):
 ;; UnsignedOffset mode on aarch64.
 function %f6(i64) -> i64 {
     mt0 = memory 0x8000
-block0(v0 ! mem(mt0, 0, 0): i64):
+block0(v0 ! mem(mt0, =0): i64):
     v2 = iconst.i64 8
-    v3 ! mem(mt0, 8, 8) = iadd.i64 v0, v2
+    v3 ! mem(mt0, =8) = iadd.i64 v0, v2
     v4 = load.i64 checked v3
     return v4
 }
@@ -77,9 +77,9 @@ block0(v0 ! mem(mt0, 0, 0): i64):
 ;; Unscaled mode on aarch64.
 function %f6(i64) -> i64 {
     mt0 = memory 0x8000
-block0(v0 ! mem(mt0, 8, 8): i64):
+block0(v0 ! mem(mt0, =8): i64):
     v2 = iconst.i64 8
-    v3 ! mem(mt0, 0, 0) = isub.i64 v0, v2
+    v3 ! mem(mt0, =0) = isub.i64 v0, v2
     v4 = load.i64 checked v3
     return v4
 }
diff --git a/cranelift/filetests/filetests/pcc/succeed/memtypes.clif b/cranelift/filetests/filetests/pcc/succeed/memtypes.clif
index dc4805c90cc..4d1e0e645b6 100644
--- a/cranelift/filetests/filetests/pcc/succeed/memtypes.clif
+++ b/cranelift/filetests/filetests/pcc/succeed/memtypes.clif
@@ -6,7 +6,7 @@ target x86_64
 function %f0(i64) -> i32 {
     mt0 = struct 8 { 0: i32, 4: i32 readonly }
 
-block0(v0 ! mem(mt0, 0, 0): i64):  ;; v0 points to an instance of mt0, at offset 0
+block0(v0 ! mem(mt0, =0): i64):  ;; v0 points to an instance of mt0, at offset 0
     v1 = load.i32 v0+0
     v2 = load.i32 v0+4
     v3 = iadd.i32 v1, v2
@@ -14,11 +14,11 @@ block0(v0 ! mem(mt0, 0, 0): i64):  ;; v0 points to an instance of mt0, at offset
 }
 
 function %f1(i64) -> i32 {
-    mt0 = struct 8 { 0: i64 readonly ! mem(mt1, 0, 0) }
+    mt0 = struct 8 { 0: i64 readonly ! mem(mt1, =0) }
     mt1 = memory 0x1_0000_0000
 
-block0(v0 ! mem(mt0, 0, 0): i64):
-    v1 ! mem(mt1, 0, 0) = load.i64 v0
+block0(v0 ! mem(mt0, =0): i64):
+    v1 ! mem(mt1, =0) = load.i64 v0
     v2 = load.i32 v1+0x1000
     return v2
 }
diff --git a/cranelift/filetests/filetests/pcc/succeed/opt.clif b/cranelift/filetests/filetests/pcc/succeed/opt.clif
index 8fda923223c..a565a41ba8a 100644
--- a/cranelift/filetests/filetests/pcc/succeed/opt.clif
+++ b/cranelift/filetests/filetests/pcc/succeed/opt.clif
@@ -8,12 +8,12 @@ target x86_64
 ;; redundant stuff that should be optimized away (x+0 -> x).
 function %f0(i64, i32) -> i64 {
     ;; mock vmctx struct:
-    mt0 = struct 8 { 0: i64 readonly ! mem(mt1, 0, 0) }
+    mt0 = struct 8 { 0: i64 readonly ! mem(mt1, =0) }
     ;; mock static memory: 4GiB range, plus 2GiB guard
     mt1 = memory 0x1_8000_0000
 
-block0(v0 ! mem(mt0, 0, 0): i64, v1: i32):
-    v2 ! mem(mt1, 0, 0) = load.i64 checked v0+0
+block0(v0 ! mem(mt0, =0): i64, v1: i32):
+    v2 ! mem(mt1, =0) = load.i64 checked v0+0
     v3 ! range(64, 0, 0xffff_ffff) = uextend.i64 v1
     v4 = iconst.i64 0
     v5 = iadd.i64 v3, v4
@@ -25,12 +25,12 @@ block0(v0 ! mem(mt0, 0, 0): i64, v1: i32):
 ;; GVN opportunity.
 function %f1(i64, i32) -> i64 {
     ;; mock vmctx struct:
-    mt0 = struct 8 { 0: i64 readonly ! mem(mt1, 0, 0) }
+    mt0 = struct 8 { 0: i64 readonly ! mem(mt1, =0) }
     ;; mock static memory: 4GiB range, plus 2GiB guard
     mt1 = memory 0x1_8000_0000
 
-block0(v0 ! mem(mt0, 0, 0): i64, v1: i32):
-    v2 ! mem(mt1, 0, 0) = load.i64 checked notrap readonly v0+0
+block0(v0 ! mem(mt0, =0): i64, v1: i32):
+    v2 ! mem(mt1, =0) = load.i64 checked notrap readonly v0+0
     v3 ! range(64, 0, 0xffff_ffff) = uextend.i64 v1
     v4 = iconst.i64 0
     v5 = iadd.i64 v3, v4
@@ -50,27 +50,27 @@ block0(v0 ! mem(mt0, 0, 0): i64, v1: i32):
 ;; RLE opportunity.
 function %f2(i64, i32) -> i64 {
     ;; mock vmctx struct:
-    mt0 = struct 8 { 0: i64 readonly ! mem(mt1, 0, 0) }
+    mt0 = struct 8 { 0: i64 readonly ! mem(mt1, =0) }
     ;; mock static memory: 4GiB range, plus 2GiB guard
     mt1 = memory 0x1_8000_0000
 
-block0(v0 ! mem(mt0, 0, 0): i64, v1: i32):
-    v2 ! mem(mt1, 0, 0) = load.i64 checked notrap readonly aligned v0+0
+block0(v0 ! mem(mt0, =0): i64, v1: i32):
+    v2 ! mem(mt1, =0) = load.i64 checked notrap readonly aligned v0+0
     brif v1, block1, block2
 
 block1:
-    v3 ! mem(mt1, 0, 0) = load.i64 checked notrap readonly aligned v0+0
+    v3 ! mem(mt1, =0) = load.i64 checked notrap readonly aligned v0+0
     return v3
 
 block2:
-    v4 ! mem(mt1, 0, 0) = load.i64 checked notrap readonly aligned v0+0
+    v4 ! mem(mt1, =0) = load.i64 checked notrap readonly aligned v0+0
     return v4
 }
 
 function %f3(i64, i32) {
     mt0 = struct 4 { 0: i32 ! range(32, 1, 3) }
 
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 1): i32):
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(32, 0, 1): i32):
     v2 ! range(32, 1, 1) = iconst.i32 1
     v3 ! range(32, 1, 2) = iadd.i32 v1, v2
 
diff --git a/cranelift/filetests/filetests/pcc/succeed/simple.clif b/cranelift/filetests/filetests/pcc/succeed/simple.clif
index 80dc769899e..fd864a3f64e 100644
--- a/cranelift/filetests/filetests/pcc/succeed/simple.clif
+++ b/cranelift/filetests/filetests/pcc/succeed/simple.clif
@@ -5,7 +5,7 @@ target x86_64
 
 function %simple1(i64 vmctx, i32) -> i8 {
     mt0 = memory 0x1_0000_0000
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(32, 0, 0xffff_ffff): i32):
+block0(v0 ! mem(mt0, =0): i64, v1 ! range(32, 0, 0xffff_ffff): i32):
     v2 ! range(64, 0, 0xffff_ffff) = uextend.i64 v1
     v3 ! mem(mt0, 0, 0xffff_ffff) = iadd.i64 v0, v2
     v4 = load.i8 checked v3
diff --git a/cranelift/filetests/filetests/pcc/succeed/struct.clif b/cranelift/filetests/filetests/pcc/succeed/struct.clif
index f53bdaff54d..93fb2384b3a 100644
--- a/cranelift/filetests/filetests/pcc/succeed/struct.clif
+++ b/cranelift/filetests/filetests/pcc/succeed/struct.clif
@@ -4,17 +4,17 @@ target aarch64
 target x86_64
 
 function %f0(i64) -> i64 {
-    mt0 = struct 8 { 0: i64 ! mem(mt1, 0, 0) }
+    mt0 = struct 8 { 0: i64 ! mem(mt1, =0) }
     mt1 = memory 0x1_0000_0000
-block0(v0 ! mem(mt0, 0, 0): i64):
-    v1 ! mem(mt1, 0, 0) = load.i64 checked v0
+block0(v0 ! mem(mt0, =0): i64):
+    v1 ! mem(mt1, =0) = load.i64 checked v0
     return v1
 }
 
 function %f1(i64, i64) {
-    mt0 = struct 8 { 0: i64 ! mem(mt1, 0, 0) }
+    mt0 = struct 8 { 0: i64 ! mem(mt1, =0) }
     mt1 = memory 0x1_0000_0000
-block0(v0 ! mem(mt0, 0, 0): i64, v1 ! mem(mt1, 0, 0): i64):
+block0(v0 ! mem(mt0, =0): i64, v1 ! mem(mt1, =0): i64):
     store.i64 checked v1, v0
     return
 }
diff --git a/cranelift/filetests/filetests/pcc/succeed/vmctx.clif b/cranelift/filetests/filetests/pcc/succeed/vmctx.clif
index ec05f22fa6c..4c06af6ad86 100644
--- a/cranelift/filetests/filetests/pcc/succeed/vmctx.clif
+++ b/cranelift/filetests/filetests/pcc/succeed/vmctx.clif
@@ -6,14 +6,14 @@ target x86_64
 ;; Equivalent to a Wasm `i64.load` from a static memory.
 function %f0(i64, i32) -> i64 {
     ;; mock vmctx struct:
-    mt0 = struct 8 { 0: i64 readonly ! mem(mt1, 0, 0) }
+    mt0 = struct 8 { 0: i64 readonly ! mem(mt1, =0) }
     ;; mock static memory: 4GiB range, plus 2GiB guard
     mt1 = memory 0x1_8000_0000
 
-block0(v0 ! mem(mt0, 0, 0): i64, v1: i32):
+block0(v0 ! mem(mt0, =0): i64, v1: i32):
     ;; Compute the address: base + offset. Guard region (2GiB) is
     ;; sufficient for an 8-byte I64 load.
-    v2 ! mem(mt1, 0, 0) = load.i64 checked v0+0    ;; base pointer
+    v2 ! mem(mt1, =0) = load.i64 checked v0+0         ;; base pointer
     v3 ! range(64, 0, 0xffff_ffff) = uextend.i64 v1  ;; offset
     v4 ! mem(mt1, 0, 0xffff_ffff) = iadd.i64 v2, v3
     v5 = load.i64 checked v4
diff --git a/cranelift/reader/src/parser.rs b/cranelift/reader/src/parser.rs
index 0ceb28477d9..228957dfa29 100644
--- a/cranelift/reader/src/parser.rs
+++ b/cranelift/reader/src/parser.rs
@@ -12,7 +12,7 @@ use cranelift_codegen::entity::{EntityRef, PrimaryMap};
 use cranelift_codegen::ir::entities::{AnyEntity, DynamicType, MemoryType};
 use cranelift_codegen::ir::immediates::{Ieee32, Ieee64, Imm64, Offset32, Uimm32, Uimm64};
 use cranelift_codegen::ir::instructions::{InstructionData, InstructionFormat, VariableArgs};
-use cranelift_codegen::ir::pcc::{BaseExpr, Expr, Fact};
+use cranelift_codegen::ir::pcc::{Expr, Fact, ValueRange};
 use cranelift_codegen::ir::types;
 use cranelift_codegen::ir::types::INVALID;
 use cranelift_codegen::ir::types::*;
@@ -27,7 +27,7 @@ use cranelift_codegen::ir::{
 use cranelift_codegen::isa::{self, CallConv};
 use cranelift_codegen::packed_option::ReservedValue;
 use cranelift_codegen::{settings, settings::Configurable, timing};
-use smallvec::SmallVec;
+use smallvec::{smallvec, SmallVec};
 use std::mem;
 use std::str::FromStr;
 use std::{u16, u32};
@@ -2179,16 +2179,10 @@ impl<'a> Parser<'a> {
 
     // Parse a "fact" for proof-carrying code, attached to a value.
     //
-    // fact ::= "range" "(" bit-width "," min-value "," max-value ")"
-    //        | "dynamic_range" "(" bit-width "," expr "," expr ")"
-    //        | "mem" "(" memory-type "," mt-offset "," mt-offset [ "," "nullable" ] ")"
-    //        | "dynamic_mem" "(" memory-type "," expr "," expr [ "," "nullable" ] ")"
+    // fact ::= "range" "(" bit-width "," range ")"
+    //        | "mem" "(" memory-type [ "," "nullable" ] "," range ")"
     //        | "conflict"
     // bit-width ::= uimm64
-    // min-value ::= uimm64
-    // max-value ::= uimm64
-    // valid-range ::= uimm64
-    // mt-offset ::= uimm64
     fn parse_fact(&mut self) -> ParseResult<Fact> {
         match self.token() {
             Some(Token::Identifier("range")) => {
@@ -2198,52 +2192,11 @@ impl<'a> Parser<'a> {
                     .match_uimm64("expected a bit-width value for `range` fact")?
                     .into();
                 self.match_token(Token::Comma, "expected a comma")?;
-                let min: u64 = self
-                    .match_uimm64("expected a min value for `range` fact")?
-                    .into();
-                self.match_token(Token::Comma, "expected a comma")?;
-                let max: u64 = self
-                    .match_uimm64("expected a max value for `range` fact")?
-                    .into();
+                let range = self.parse_range()?;
                 self.match_token(Token::RPar, "`range` fact needs a closing `)`")?;
-                let bit_width_max = match bit_width {
-                    x if x > 64 => {
-                        return Err(self.error("bitwidth must be <= 64 bits on a `range` fact"));
-                    }
-                    64 => u64::MAX,
-                    x => (1u64 << x) - 1,
-                };
-                if min > max {
-                    return Err(self.error(
-                        "min value must be less than or equal to max value on a `range` fact",
-                    ));
-                }
-                if max > bit_width_max {
-                    return Err(
-                        self.error("max value is out of range for bitwidth on a `range` fact")
-                    );
-                }
                 Ok(Fact::Range {
                     bit_width: u16::try_from(bit_width).unwrap(),
-                    min: min.into(),
-                    max: max.into(),
-                })
-            }
-            Some(Token::Identifier("dynamic_range")) => {
-                self.consume();
-                self.match_token(Token::LPar, "`dynamic_range` fact needs an opening `(`")?;
-                let bit_width: u64 = self
-                    .match_uimm64("expected a bit-width value for `dynamic_range` fact")?
-                    .into();
-                self.match_token(Token::Comma, "expected a comma")?;
-                let min = self.parse_expr()?;
-                self.match_token(Token::Comma, "expected a comma")?;
-                let max = self.parse_expr()?;
-                self.match_token(Token::RPar, "`dynamic_range` fact needs a closing `)`")?;
-                Ok(Fact::DynamicRange {
-                    bit_width: u16::try_from(bit_width).unwrap(),
-                    min,
-                    max,
+                    range,
                 })
             }
             Some(Token::Identifier("mem")) => {
@@ -2254,61 +2207,22 @@ impl<'a> Parser<'a> {
                     Token::Comma,
                     "expected a comma after memory type in `mem` fact",
                 )?;
-                let min_offset: u64 = self
-                    .match_uimm64("expected a uimm64 minimum pointer offset for `mem` fact")?
-                    .into();
-                self.match_token(Token::Comma, "expected a comma after offset in `mem` fact")?;
-                let max_offset: u64 = self
-                    .match_uimm64("expected a uimm64 maximum pointer offset for `mem` fact")?
-                    .into();
-                let nullable = if self.token() == Some(Token::Comma) {
+                let nullable = if self.token() == Some(Token::Identifier("nullable")) {
                     self.consume();
                     self.match_token(
-                        Token::Identifier("nullable"),
-                        "expected `nullable` in last optional field of `dynamic_mem`",
+                        Token::Comma,
+                        "expected a comma after `nullable` in `mem` fact",
                     )?;
                     true
                 } else {
                     false
                 };
+                let range = self.parse_range()?;
                 self.match_token(Token::RPar, "expected a `)`")?;
                 Ok(Fact::Mem {
                     ty,
-                    min_offset,
-                    max_offset,
-                    nullable,
-                })
-            }
-            Some(Token::Identifier("dynamic_mem")) => {
-                self.consume();
-                self.match_token(Token::LPar, "expected a `(`")?;
-                let ty = self.match_mt("expected a memory type for `dynamic_mem` fact")?;
-                self.match_token(
-                    Token::Comma,
-                    "expected a comma after memory type in `dynamic_mem` fact",
-                )?;
-                let min = self.parse_expr()?;
-                self.match_token(
-                    Token::Comma,
-                    "expected a comma after offset in `dynamic_mem` fact",
-                )?;
-                let max = self.parse_expr()?;
-                let nullable = if self.token() == Some(Token::Comma) {
-                    self.consume();
-                    self.match_token(
-                        Token::Identifier("nullable"),
-                        "expected `nullable` in last optional field of `dynamic_mem`",
-                    )?;
-                    true
-                } else {
-                    false
-                };
-                self.match_token(Token::RPar, "expected a `)`")?;
-                Ok(Fact::DynamicMem {
-                    ty,
-                    min,
-                    max,
                     nullable,
+                    range,
                 })
             }
             Some(Token::Identifier("def")) => {
@@ -2336,74 +2250,121 @@ impl<'a> Parser<'a> {
                 self.consume();
                 Ok(Fact::Conflict)
             }
-            _ => Err(self.error(
-                "expected a `range`, 'dynamic_range', `mem`, `dynamic_mem`, `def`, `compare` or `conflict` fact",
-            )),
+            _ => Err(self.error("expected a `range`, `mem`, `def`, `compare` or `conflict` fact")),
         }
     }
 
-    // Parse a dynamic expression used in some kinds of PCC facts.
+    // Parse a range with min-, equals-, and max-constraints.
     //
-    // expr ::= base-expr
-    //        | base-expr + uimm64  // but in-range for imm64
-    //        | base-expr - uimm64  // but in-range for imm64
-    //        | imm64
-    fn parse_expr(&mut self) -> ParseResult<Expr> {
-        if let Some(Token::Integer(_)) = self.token() {
-            let offset: i64 = self
-                .match_imm64("expected imm64 for dynamic expression")?
-                .into();
-            Ok(Expr {
-                base: BaseExpr::None,
-                offset,
+    // range ::= "=" exprs                      -- equals
+    //         | exprs "," exprs                -- min, max
+    //         | exprs "," "=" exprs "," exprs  -- min, equals, max
+    fn parse_range(&mut self) -> ParseResult<ValueRange> {
+        if self.token() == Some(Token::Equal) {
+            self.consume();
+            let equal = self.parse_exprs()?;
+            Ok(ValueRange {
+                equal,
+                min: smallvec![],
+                max: smallvec![],
             })
         } else {
-            let base = self.parse_base_expr()?;
-            match self.token() {
-                Some(Token::Plus) => {
+            let min = self.parse_exprs()?;
+            self.match_token(Token::Comma, "expected comma in range after min exprs")?;
+            let equal = if self.token() == Some(Token::Equal) {
+                self.consume();
+                let equal = self.parse_exprs()?;
+                self.match_token(Token::Comma, "expected comma n range after equal exprs")?;
+                equal
+            } else {
+                smallvec![]
+            };
+            let max = self.parse_exprs()?;
+            Ok(ValueRange { equal, min, max })
+        }
+    }
+
+    // Parse a list of expressions, for an equivalent set /
+    // min-boundss set / max-bounds set in a range.
+    //
+    // exprs ::= expr | "{" expr ( "," expr )* "}" | "{" "}"
+    fn parse_exprs(&mut self) -> ParseResult<SmallVec<[Expr; 1]>> {
+        let mut results = smallvec![];
+        if self.token() == Some(Token::LBrace) {
+            self.consume();
+            loop {
+                if self.token() == Some(Token::RBrace) {
                     self.consume();
-                    let offset: u64 = self
-                        .match_uimm64(
-                            "expected uimm64 in imm64 range for offset in dynamic expression",
-                        )?
-                        .into();
-                    let offset: i64 = i64::try_from(offset).map_err(|_| {
-                        self.error("integer offset in dynamic expression is out of range")
-                    })?;
-                    Ok(Expr { base, offset })
+                    break;
                 }
-                Some(Token::Integer(x)) if x.starts_with("-") => {
-                    let offset: i64 = self
-                        .match_imm64("expected an imm64 range for offset in dynamic expression")?
-                        .into();
-                    Ok(Expr { base, offset })
+                results.push(self.parse_expr()?);
+                if self.token() != Some(Token::Comma) {
+                    break;
                 }
-                _ => Ok(Expr { base, offset: 0 }),
+                self.consume();
             }
+        } else {
+            results.push(self.parse_expr()?);
         }
+        Ok(results)
     }
 
-    // Parse the base part of a dynamic expression, used in some PCC facts.
+    // Parse a dynamic expression used in some kinds of PCC facts.
     //
-    // base-expr ::= GlobalValue(base)
-    //             | Value(base)
-    //             | "max"
-    //             | (epsilon)
-    fn parse_base_expr(&mut self) -> ParseResult<BaseExpr> {
+    // expr ::= base-expr
+    //        | base-expr + uimm64
+    //        | base-expr - uimm64
+    //        | uimm64
+    //        | "max"
+    // base-expr ::= GlobalValue(base) | Value(base)
+    fn parse_expr(&mut self) -> ParseResult<Expr> {
         match self.token() {
-            Some(Token::Identifier("max")) => {
-                self.consume();
-                Ok(BaseExpr::Max)
+            Some(Token::Integer(_)) => {
+                let offset: u64 = self
+                    .match_uimm64("expected uimm64 for dynamic expression")?
+                    .into();
+                Ok(Expr::constant(offset))
+            }
+            Some(Token::Value(_)) => {
+                let value = self.match_value("expected value")?;
+                let offset: i128 = self.parse_expr_offset()?;
+                Ok(Expr::value_offset(value, offset))
             }
-            Some(Token::GlobalValue(..)) => {
+            Some(Token::GlobalValue(_)) => {
                 let gv = self.match_gv("expected global value")?;
-                Ok(BaseExpr::GlobalValue(gv))
+                let offset: i128 = self.parse_expr_offset()?;
+                Ok(Expr::global_value_offset(gv, offset.into()))
             }
-            Some(Token::Value(..)) => {
-                let value = self.match_value("expected value")?;
-                Ok(BaseExpr::Value(value))
+            Some(Token::Identifier("max")) => Ok(Expr::max_value()),
+            _ => Err(self.error("unexpected token")),
+        }
+    }
+
+    // Parse the offset part of a dynamic expression, used in some PCC facts.
+    //
+    // expr-offset ::= "+" uimm64 | "-" uimm64 | (epsilon)
+    fn parse_expr_offset(&mut self) -> ParseResult<i128> {
+        match self.token() {
+            Some(Token::Plus) => {
+                self.consume();
+                Ok(i128::from(u64::from(self.match_uimm64(
+                    "expected imm64 for value offset in expression",
+                )?)))
+            }
+            Some(Token::Minus) => {
+                self.consume();
+                Ok(-i128::from(u64::from(self.match_uimm64(
+                    "expected imm64 for value offset in expression",
+                )?)))
+            }
+            Some(Token::Integer(s)) if s.starts_with("+") || s.starts_with("-") => {
+                let value: i128 = s
+                    .parse()
+                    .map_err(|_| self.error("unable to parse integer constant"))?;
+                self.consume();
+                Ok(value)
             }
-            _ => Ok(BaseExpr::None),
+            _ => Ok(0),
         }
     }
 
diff --git a/cranelift/wasm/src/code_translator/bounds_checks.rs b/cranelift/wasm/src/code_translator/bounds_checks.rs
index 9bd0f99f527..0c7291f2a0e 100644
--- a/cranelift/wasm/src/code_translator/bounds_checks.rs
+++ b/cranelift/wasm/src/code_translator/bounds_checks.rs
@@ -86,11 +86,11 @@ where
                 orig_index,
                 lhs_off.unwrap(),
             ));
-            // If the RHS is a symbolic value (v1 or gv1), we can
-            // emit a Compare fact.
+            // If the RHS has an exact expression (v1, gv1, or a
+            // numeric constant), we can emit a Compare fact.
             if let Some(rhs) = builder.func.dfg.facts[rhs]
                 .as_ref()
-                .and_then(|f| f.as_symbol())
+                .and_then(|f| f.as_expr())
             {
                 builder.func.dfg.facts[result] = Some(Fact::Compare {
                     kind: compare_kind,
@@ -98,18 +98,6 @@ where
                     rhs: Expr::offset(rhs, rhs_off.unwrap()).unwrap(),
                 });
             }
-            // Likewise, if the RHS is a constant, we can emit a
-            // Compare fact.
-            if let Some(k) = builder.func.dfg.facts[rhs]
-                .as_ref()
-                .and_then(|f| f.as_const(pointer_bit_width))
-            {
-                builder.func.dfg.facts[result] = Some(Fact::Compare {
-                    kind: compare_kind,
-                    lhs: Expr::offset(&Expr::value(orig_index), lhs_off.unwrap()).unwrap(),
-                    rhs: Expr::constant((k as i64).checked_add(rhs_off.unwrap()).unwrap()),
-                });
-            }
         }
         result
     };
@@ -554,6 +542,7 @@ fn explicit_check_oob_condition_and_compute_addr(
     }
 
     let mut addr = compute_addr(pos, heap, addr_ty, index, offset, pcc);
+    let addr_bits = u16::try_from(addr_ty.bits()).unwrap();
 
     if spectre_mitigations_enabled {
         let null = pos.ins().iconst(addr_ty, 0);
@@ -564,29 +553,27 @@ fn explicit_check_oob_condition_and_compute_addr(
             Some(AddrPcc::Static32(ty, size)) => {
                 pos.func.dfg.facts[null] =
                     Some(Fact::constant(u16::try_from(addr_ty.bits()).unwrap(), 0));
-                pos.func.dfg.facts[addr] = Some(Fact::Mem {
-                    ty,
-                    min_offset: 0,
-                    max_offset: size.checked_sub(u64::from(access_size)).unwrap(),
-                    nullable: true,
-                });
+                let max_static = size.checked_sub(u64::from(access_size)).unwrap();
+                pos.func.dfg.facts[addr] = Some(
+                    Fact::memory_with_range(
+                        ty,
+                        Fact::static_value_range(addr_bits, max_static),
+                        true,
+                    )
+                    .unwrap(),
+                );
             }
             Some(AddrPcc::Dynamic(ty, gv)) => {
                 pos.func.dfg.facts[null] =
                     Some(Fact::constant(u16::try_from(addr_ty.bits()).unwrap(), 0));
-                pos.func.dfg.facts[addr] = Some(Fact::DynamicMem {
-                    ty,
-                    min: Expr::constant(0),
-                    max: Expr::offset(
-                        &Expr::global_value(gv),
-                        i64::try_from(heap.offset_guard_size)
-                            .unwrap()
-                            .checked_sub(i64::from(access_size))
-                            .unwrap(),
-                    )
-                    .unwrap(),
-                    nullable: true,
-                });
+                let bound = Expr::global_value_offset(
+                    gv,
+                    i128::from(heap.offset_guard_size) - i128::from(access_size),
+                );
+                pos.func.dfg.facts[addr] = Some(
+                    Fact::memory_with_range(ty, Fact::dynamic_value_range(addr_bits, bound), true)
+                        .unwrap(),
+                );
             }
         }
     }
@@ -610,17 +597,13 @@ fn compute_addr(
 ) -> ir::Value {
     debug_assert_eq!(pos.func.dfg.value_type(index), addr_ty);
 
+    let addr_bits = u16::try_from(addr_ty.bits()).unwrap();
     let heap_base = pos.ins().global_value(addr_ty, heap.base);
 
     match pcc {
         None => {}
         Some(AddrPcc::Static32(ty, _size)) => {
-            pos.func.dfg.facts[heap_base] = Some(Fact::Mem {
-                ty,
-                min_offset: 0,
-                max_offset: 0,
-                nullable: false,
-            });
+            pos.func.dfg.facts[heap_base] = Some(Fact::memory_base(ty));
         }
         Some(AddrPcc::Dynamic(ty, _limit)) => {
             pos.func.dfg.facts[heap_base] = Some(Fact::dynamic_base_ptr(ty));
@@ -632,24 +615,18 @@ fn compute_addr(
     match pcc {
         None => {}
         Some(AddrPcc::Static32(ty, _) | AddrPcc::Dynamic(ty, _)) => {
-            if let Some(idx) = pos.func.dfg.facts[index]
-                .as_ref()
-                .and_then(|f| f.as_symbol())
-                .cloned()
-            {
-                pos.func.dfg.facts[base_and_index] = Some(Fact::DynamicMem {
-                    ty,
-                    min: idx.clone(),
-                    max: idx,
-                    nullable: false,
-                });
+            if let Some(idx) = pos.func.dfg.facts[index].as_ref() {
+                pos.func.dfg.facts[base_and_index] =
+                    Some(Fact::memory_with_range(ty, idx.clone(), false).unwrap());
             } else {
-                pos.func.dfg.facts[base_and_index] = Some(Fact::Mem {
-                    ty,
-                    min_offset: 0,
-                    max_offset: u64::from(u32::MAX),
-                    nullable: false,
-                });
+                pos.func.dfg.facts[base_and_index] = Some(
+                    Fact::memory_with_range(
+                        ty,
+                        Fact::static_value_range(addr_bits, u64::from(u32::MAX)),
+                        false,
+                    )
+                    .unwrap(),
+                );
             }
         }
     }
@@ -675,30 +652,22 @@ fn compute_addr(
         match pcc {
             None => {}
             Some(AddrPcc::Static32(ty, _) | AddrPcc::Dynamic(ty, _)) => {
-                if let Some(idx) = pos.func.dfg.facts[index]
-                    .as_ref()
-                    .and_then(|f| f.as_symbol())
-                {
-                    pos.func.dfg.facts[result] = Some(Fact::DynamicMem {
-                        ty,
-                        min: idx.clone(),
-                        // Safety: adding an offset to an expression with
-                        // zero offset -- add cannot wrap, so `unwrap()`
-                        // cannot fail.
-                        max: Expr::offset(idx, i64::from(offset)).unwrap(),
-                        nullable: false,
-                    });
+                if let Some(base_and_index_fact) = pos.func.dfg.facts[base_and_index].as_ref() {
+                    pos.func.dfg.facts[result] = Some(
+                        base_and_index_fact
+                            .offset(addr_bits, i64::from(offset))
+                            .unwrap(),
+                    );
                 } else {
-                    pos.func.dfg.facts[result] = Some(Fact::Mem {
-                        ty,
-                        min_offset: u64::from(offset),
-                        // Safety: can't overflow -- two u32s summed in a
-                        // 64-bit add. TODO: when memory64 is supported here,
-                        // `u32::MAX` is no longer true, and we'll need to
-                        // handle overflow here.
-                        max_offset: u64::from(u32::MAX) + u64::from(offset),
-                        nullable: false,
-                    });
+                    let max_static = u64::from(u32::MAX) + u64::from(offset);
+                    pos.func.dfg.facts[result] = Some(
+                        Fact::memory_with_range(
+                            ty,
+                            Fact::static_value_range(addr_bits, max_static),
+                            false,
+                        )
+                        .unwrap(),
+                    );
                 }
             }
         }
diff --git a/crates/cranelift/src/func_environ.rs b/crates/cranelift/src/func_environ.rs
index cb695cdab04..eb87887360a 100644
--- a/crates/cranelift/src/func_environ.rs
+++ b/crates/cranelift/src/func_environ.rs
@@ -228,12 +228,7 @@ impl<'module_environment> FuncEnvironment<'module_environment> {
                 });
 
                 self.pcc_vmctx_memtype = Some(vmctx_memtype);
-                func.global_value_facts[vmctx] = Some(Fact::Mem {
-                    ty: vmctx_memtype,
-                    min_offset: 0,
-                    max_offset: 0,
-                    nullable: false,
-                });
+                func.global_value_facts[vmctx] = Some(Fact::memory_base(vmctx_memtype));
             }
 
             self.vmctx = Some(vmctx);
@@ -1945,12 +1940,7 @@ impl<'module_environment> cranelift_wasm::FuncEnvironment for FuncEnvironment<'m
                                 .expect("Memory plan has overflowing size plus guard"),
                         });
                         // This fact applies to any pointer to the start of the memory.
-                        let base_fact = Fact::Mem {
-                            ty: data_mt,
-                            min_offset: 0,
-                            max_offset: 0,
-                            nullable: false,
-                        };
+                        let base_fact = Fact::memory_base(data_mt);
                         // Create a field in the vmctx for the base pointer.
                         match &mut func.memory_types[ptr_memtype] {
                             ir::MemoryTypeData::Struct { size, fields } => {
diff --git a/tests/pcc_memory.rs b/tests/pcc_memory.rs
index dddff2a5ba9..15f721d939a 100644
--- a/tests/pcc_memory.rs
+++ b/tests/pcc_memory.rs
@@ -8,132 +8,44 @@ mod pcc_memory_tests {
 
     const TESTS: &'static [&'static str] = &[
         r#"
-(module
- (memory 1 1)
- (func (param i32)
   local.get 0
   i32.load8_u
-  drop))
+  drop
     "#,
         r#"
-(module
- (memory 1 1)
- (func (param i32)
   local.get 0
   i32.load8_u offset=0x10000
-  drop))
+  drop
     "#,
         r#"
-(module
- (memory 1 1)
- (func (param i32)
   local.get 0
   i32.load16_u
-  drop))
+  drop
     "#,
         r#"
-(module
- (memory 1 1)
- (func (param i32)
   local.get 0
   i32.load16_u offset=0x10000
-  drop))
+  drop
     "#,
         r#"
-(module
- (memory 1 1)
- (func (param i32)
   local.get 0
   i32.load
-  drop))
+  drop
     "#,
         r#"
-(module
- (memory 1 1)
- (func (param i32)
   local.get 0
   i32.load offset=0x10000
-  drop))
+  drop
     "#,
         r#"
-(module
- (memory 1 1)
- (func (param i32)
   local.get 0
   i64.load
-  drop))
+  drop
     "#,
         r#"
-(module
- (memory 1 1)
- (func (param i32)
   local.get 0
   i64.load offset=0x10000
-  drop))
-    "#,
-        r#"
-(module
- (memory 10 20)
- (func (param i32)
-  local.get 0
-  i32.load8_u
-  drop))
-    "#,
-        r#"
-(module
- (memory 10 20)
- (func (param i32)
-  local.get 0
-  i32.load8_u offset=0x10000
-  drop))
-    "#,
-        r#"
-(module
- (memory 10 20)
- (func (param i32)
-  local.get 0
-  i32.load16_u
-  drop))
-    "#,
-        r#"
-(module
- (memory 10 20)
- (func (param i32)
-  local.get 0
-  i32.load16_u offset=0x10000
-  drop))
-    "#,
-        r#"
-(module
- (memory 10 20)
- (func (param i32)
-  local.get 0
-  i32.load
-  drop))
-    "#,
-        r#"
-(module
- (memory 10 20)
- (func (param i32)
-  local.get 0
-  i32.load offset=0x10000
-  drop))
-    "#,
-        r#"
-(module
- (memory 10 20)
- (func (param i32)
-  local.get 0
-  i64.load
-  drop))
-    "#,
-        r#"
-(module
- (memory 10 20)
- (func (param i32)
-  local.get 0
-  i64.load offset=0x10000
-  drop))
+  drop
     "#,
     ];
 
@@ -145,7 +57,24 @@ mod pcc_memory_tests {
         const MIB: u64 = 1024 * KIB;
         const GIB: u64 = 1024 * MIB;
 
-        for &test in TESTS {
+        let mut bodies = vec![];
+        for (mem_min, mem_max) in [(1, 1), (10, 20)] {
+            for &snippet in TESTS {
+                bodies.push(format!(
+                    "(module (memory {mem_min} {mem_max}) (func (param i32) {snippet}))"
+                ));
+            }
+            let all_snippets = TESTS
+                .iter()
+                .map(|s| s.to_owned())
+                .collect::<Vec<_>>()
+                .join("\n");
+            bodies.push(format!(
+                "(module (memory {mem_min} {mem_max}) (func (param i32) {all_snippets}))"
+            ));
+        }
+
+        for test in &bodies {
             for static_memory_maximum_size in [0, 64 * KIB, 1 * MIB, 4 * GIB, 6 * GIB] {
                 for guard_size in [0, 64 * KIB, 2 * GIB] {
                     for enable_spectre in [true /* not yet supported by PCC: false */] {