set_next and get_next truncate pointers unsafely on some x86 and ARM configurations

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

lean_object has a clever optimization to mutate into a linked list for handling deletions without stack growth:

https://github.com/leanprover/lean4/blob/e60078db3b4e63ca150573dd94f04862be7187e0/src/include/lean/lean.h#L119-L121

which effectively assumes that a 64-bit pointer can be truncated to 48-bits, and that zero-extending will round-trip, This is implemented here:

https://github.com/leanprover/lean4/blob/e60078db3b4e63ca150573dd94f04862be7187e0/src/runtime/object.cpp#L278-L301

Unfortunately, like many clever optimizations, eventually compilers and hardware adjust such that its assumptions no longer hold.

In particular, the following configurations lead to segfaults due to the top bits of the address space being zeroed out:

• Arm's memory tagging hardware extension (MTE), which uses the top bits to implement address sanitization.
• Arm's large virtual addressing, which extends the virtual address space from 48 bits to 52 bits (i.e. with CONFIG_ARM64_FORCE_52BIT=y)
• Intel's 5-level paging, which extends the virtual address space from 48 bits to 57 bits

Context

Detected in some address-sanitization runs of AlphaProof infrastructure.

Steps to Reproduce

1. Build with some of the suggested flags above

Expected behavior: Lean's tests pass

Actual behavior: Segfault due to invalid addresses, or the lean_assert(get_next(o) == n); firing.

Versions

4.27.0

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the lean_object definition in src/include/lean/lean.h at lines 119-121, then inspect set_next and get_next in src/runtime/object.cpp at lines 278-301. Run the Lean tests with the affected ARM and x86 address-space configurations where possible. Done means the pointer round-trip remains valid and the tests pass without invalid-address faults or the reported assertion.