# Address Uniqueness

I'm not going to recap the entire problem in this writeup. If anyone has questions about why the more obvious solutions don't work, I'd be happy to answer them on Zulip or Discord.

The short summary is that we need to justify both print statements firing in this example:

#### Example 1 ("stack smashing"):

fn bad(limit: usize) {
    if limit == 0 {
        // We've allocatd `usize::MAX` many `usize`s??
        println!("Bottomed out");
        return;
    }
    let mut x: usize = limit;
    let r = &mut x;
    bad(limit - 1);
    if *r != limit {
        panic!();
    }
    return;
}

fn main() {
    bad(usize::MAX);
    println!("unreachable");
}

#### Example 2:

The solution documented below was initially thought to run into problems with this example, which is why I retain it here. We've since been able to address those concerns though, so this should no longer be relevant.

:::spoiler Not too relevant

let p1 = alloca(8);
let p2 = alloca(8);

if abs_diff(p1.addr(), p2.addr()) < 8 {
    // Dead code but removing it is unsound
    p1.expose_addr();
    p2.expose_addr();
}

if abs_diff(p1.addr(), p2.addr()) < 8 {
    println!("Unreachable")
}

dealloc(p1);
dealloc(p2);

:::

#### Example 3

This example eliminates some alternative solutions:

// May these get overlapping addresses?
let p = alloca(8); *p = 0;
let q = alloca(8); *q = 0;

let a = p.expose_addr();
q.expose_addr();

// If so, how do we ensure this gets a pointer to `p`?
let x = a as *mut usize;
*x = 5;
dbg!(*p);
dbg!(*q);

## Background

We begin with some terminology. Not all of these things are strictly necessary for the remainder of the proposal, but it seems helpful to include some extra information about how this fits into the rest of the AM:

- AM memory looks something like `Map<AllocId, Allocation>`, where each `Allocation` is vaguely:

    struct Allocation {
        base_addr: usize,
        data: Vec<(AmByte, BorrowStack)>
    }

- Pointers are triples of the form `(addr: usize, alloc_id: AllocId, sb_tag: Tag)` where `(alloc_id, sb_tag)` are together the "provenance" and `AllocId` and `Tag` are naturals. It may be the case[^1] that SB allows us to remove the `alloc_id` and have just the `sb_tag`, but it's simpler to keep them separate for now. As a matter of fact, we will actually omit the `sb_tag` throughout the rest of this discussion, because it does not interact with anything else we discuss.

[^1]: Currently, this is true if raw pointers are tagged and false if they are untagged.

Let `p = (p_addr, p_alloc, _)` be a pointer (really a place, but lets ignore that). When we load, store, or do some other operation on `p` that requires accessing its backing memory, we first find the `allocation` that `p` points into via the `p_alloc` allocation id. We then compute the offset `p_addr - allocation.base_addr` and index the allocation's data at that offset to find the appropriate byte. Interestingly, note that none of this requires the base addresses of different allocations to be unique in any way.

## Proposal

The main change of this proposal is to add a `forced: bool`[^2] flag to the `Allocation` definition. We maintain an invariant that all allocations for which the `forced` flag is true have non-overlapping address ranges.

[^2]: Please suggest better names, I'm desperate.

When allocating, the AM non-deterministically chooses between the following options:

1) Fail to allocate and report OOM.
2) Allocate by picking a fresh value for the allocation id, a non-deterministic base address, and setting the forced flag to `false`.
3) Allocate by picking a fresh value for the allocation id, a base address that does not overlap with any other live `forced` allocation but is otherwise non-deterministic, and setting the forced flag to `true`.

Furthermore, we add a new intrinsic operation `fn force_addr((_, alloc_id, _): Ptr)` to pointers. It behaves like this:

let Some(alloc_id) = alloc_id else {
    // This pointer has null provenance
    return;
};
let this_alloc = am_memory.get_alloc(alloc_id);
if !this_alloc.forced {
    non_behavior()
}

In other words, we ensure that the allocation to which the pointer belongs is forced.

`non_behavior` is explained in more detail below, but the tl;dr around it is that it is a state which the AM guarantees will not occur.

Furthermore, we extend `.expose_addr()` and equivalent operations to also invoke `.force_addr()`.

Example 1 continues to be allowed to print "unreachable" because the allocations all succeed and everything Just Works.

The only legal behaviors of Example 3 are OOM or printing `(5, 0)`. The address ranges chosen when the values are allocated may not overlap, because then `non_behavior()` would be invoked in `q.expose_addr()`.

## Non Behavior

The definition of `non_behavior()` (`NB()` from here on out) is obviously imprecise above, so let me give a more precise one. First, terminology:

- An `Execution` of a program is one of possibly many possible results of running that program. It's effectively a `Vec<SideEffect>` that describes the side-effects of this execution.
- The `Outcome` of a program is the `Set<Execution>` of its possible behaviors. When you compile/run a program, its behavior will be that of one of those `Execution`s.

`NB()` is a function that 1) performs `SideEffect::NB`, and 2) terminates the program. Additionally, when we add `NB()` to the language, we promise that the `Execution` that is chosen from the `Outcome` is one that does not contain `SideEffect::NB`. There are two interesting theorems to prove about this.

#### It is possible to compile all programs

We cannot directly expose the ability to invoke `NB()` to users. That is because we might run into a situation in which all possible `Execution`s of a program contain `NB`, and so there is no correct behavior for the compiler.

Instead, we only add `NB()` to the language as a component of the `.force_addr()` intrinsic, and we accompany it with a proof that shows that for all programs the user can write, there is a non-NB execution. This proof is fairly simple: The compiler can ensure at allocation time that all allocations have non-overlapping address ranges. If ever it cannot be sure that this is the case, it OOMs. This guarantees that NB will never be invoked.

#### NB makes sense to optimizations

Although we have shown that it is well-defined, it still remains the case that NB is a slightly weird language feature, and it is important to show that optimizations can deal with it. The important result is this: It is sound for an optimization to treat `NB` as a side-effecting, non-terminating function. The full proof is a little annoying as it requires a lot of definitions, but the gist of the argument is this: If the optimization is sound, then all possible executions of the output must also be possible executions of the input. As such, all non-NB executions of the output must have an equivalent non-NB execution of the input (as NB is a side-effect). Furthermore, the argument above still holds to show that there is a non-NB execution of the output, and so we are happy.

This suffices to show that optimizations *can* handle NB, but "treat it as an opaque function" is also just about the biggest optimization barrier possible. It seems desirable to try and be smarter about handling `.force_addr()`, but I'm not sure how to do it, because of examples like this:

fn foo() {
    let y: u16 = 0;
    (&y as *const _).force_addr();
}

let x: [u8; usize::MAX - 1] = [0; _];
(&x as *const _).force_addr();
// Guaranteed to OOM
foo();