Define "allocation"

[gnzlbg]

We use the word "allocation" in the abstract machine, e.g., when talking about provenance, or when saying that each stack variable lives on its own "allocation". And we might start using it when talking about the guarantees of Rc (see rust-lang/rust#64484). So I think we should define this word in the glossary for now.

While it is possible to write Rust programs that have multiple address spaces, I think it would be reasonable to just start by assuming that there is only just one address space.

[Lokathor]

I think that we should be careful about such a simplification. Usually it's easier to ignore complications than to stick them into the design later.

[gnzlbg]

Note that two allocations with the same address but in distinct address spaces are already distinct allocations, so one can think of the address space a pointer refers to as being part of its provenance.

[RalfJung]

IMO the only satisfying definition of allocation is to actually give a (preliminary) instance of the Rust memory interface. Everything else is going to be imprecise and not very useful IMO.