Define and implement raw pointer difference as address subtraction, not implicit element distance

[ehartford]

Summary

The raw-pointer spec now distinguishes two operations that were previously conflated:

• raw address difference: safe when specified as integer address subtraction;
• allocation-relative element distance: stronger, because it asserts same-allocation/provenance/bounds facts and therefore requires proof or unsafe.

Current behavior accepts p - q in safe code for unrelated raw pointers. The old spec wording said this returns an element count between pointers; the new spec says that meaning is only valid when same-allocation facts are proven.

Repro

fn main:
    var a = 1
    var b = 2
    let p = (&raw mut a) as *mut i32
    let q = (&raw mut b) as *mut i32
    let d = p - q
    let _ = d

Observed with ./out/bin/with check: currently reports ok.

Expected

The language should make the distinction explicit:

• If p - q remains a safe operation, it must mean raw address-value subtraction under the target raw-pointer model, not same-allocation element distance.
• If With wants allocation-relative element distance, that operation must require proven same-allocation facts or unsafe.
• Diagnostics should not imply that arbitrary raw pointer subtraction proves same allocation or element distance.

Root cause / 5 Whys

1. Why does p - q compile safely? Raw pointer subtraction is currently classified with raw pointer arithmetic.
2. Why is that too broad? The old rule treated pointer difference as an element count without separating address arithmetic from allocation-relative distance.
3. Why is element distance stronger? It asserts the pointers are in the same allocation/provenance domain and that an element distance is meaningful.
4. Why is that unsafe for arbitrary raw pointers? Raw pointer values alone do not carry those facts.
5. Root cause: the operator semantics conflate validity-less raw address subtraction with same-allocation element-distance semantics.

Acceptance criteria

• The spec-facing behavior for raw pointer difference is implemented exactly: safe address difference is integer address subtraction.
• Allocation-relative element distance is rejected unless same-allocation facts are proven or the operation is inside unsafe / raw surface.
• Tests cover unrelated raw pointers, same-array/slice proven pointers if supported, and emitted IR/C lowering.
• Backend lowering for address difference does not use C pointer subtraction or any LLVM/C construct that assumes same allocation for arbitrary raw addresses.