begin with value domain

Author: RalfJung

wip/memory-interface.md

@@ -16,6 +16,7 @@ This encodes the fact that in Rust, *operations are typed, but memory is not*---
 
 One key question a memory model has to answer is *what is a pointer*.
 It might seem like the answer is just "an integer of appropriate size", but [that is not the case][pointers-complicated].
+This becomes even more prominent with aliasing models such as [Stacked Borrows].
 So we will leave this question open, and treat `Pointer` as an "associated type" of the memory interface
 
 ## Bytes
@@ -31,7 +32,7 @@ enum Byte<Pointer> {
     /// An uninitialized byte.
     Uninit,
     /// One byte of a pointer.
-    Pointer {
+    PtrFragment {
         /// The pointer of which this is a byte.
         ptr: Pointer,
         /// Which byte of the pointer this is.
@@ -41,6 +42,12 @@ enum Byte<Pointer> {
 }
 ```
 
+The purpose of `PtrFragment` is to be able to have a byte-wise representation of a `Pointer`.
+On a 32-bit system, the sequence of 4 bytes representing `ptr: Pointer` is:
+```
+[PtrFragment { ptr, idx: 0 }, PtrFragment { ptr, idx: 1 }, PtrFragment { ptr, idx: 2 }, PtrFragment { ptr, idx: 3 }]
+```
+
 ## Memory interface
 
 The Rust memory interface is described by the following (not-yet-complete) trait definition:
@@ -51,34 +58,32 @@ The Rust memory interface is described by the following (not-yet-complete) trait
 /// We also let all operations potentially mutated memory. For example, reads
 /// actually do change the current state when considering concurrency or
 /// Stacked Borrows.
+/// And finally, all operations are fallible (they return `Result`); if they
+/// fail, that means the program caused UB.
 trait Memory {
     /// The type of pointer values.
     type Pointer;
 
-    /// The type of memory errors (i.e., ways in which the program can cause UB
-    /// by interacting with memory).
-    type Error;
-
     /// Create a new allocation.
-    fn allocate(&mut self, size: u64, align: u64) -> Result<Self::Pointer, Self::Error>;
+    fn allocate(&mut self, size: u64, align: u64) -> Result<Self::Pointer, Error>;
 
     /// Remove an allocation.
-    fn deallocate(&mut self, ptr: Self::Pointer, size: u64, align: u64) -> Result<(), Self::Error>;
+    fn deallocate(&mut self, ptr: Self::Pointer, size: u64, align: u64) -> Result<(), Error>;
 
     /// Write some bytes to memory.
-    fn write(&mut self, ptr: Self::Pointer, bytes: Vec<Byte<Self::Pointer>>) -> Result<(), Self::Error>;
+    fn write(&mut self, ptr: Self::Pointer, bytes: Vec<Byte<Self::Pointer>>) -> Result<(), Error>;
 
     /// Read some bytes from memory.
-    fn read(&mut self, ptr: Self::Pointer, len: u64) -> Result<Vec<Byte<Self::Pointer>>, Self::Error>;
+    fn read(&mut self, ptr: Self::Pointer, len: u64) -> Result<Vec<Byte<Self::Pointer>>, Error>;
 
     /// Offset the given pointer.
-    fn offset(&mut self, ptr: Self::Pointer, offset: u64, mode: OffsetMode) -> Result<Self::Pointer, Self::Error>;
+    fn offset(&mut self, ptr: Self::Pointer, offset: u64, mode: OffsetMode) -> Result<Self::Pointer, Error>;
 
     /// Cast the given pointer to an integer.
-    fn ptr_to_int(&mut self, ptr: Self::Pointer) -> Result<u64, Self::Error>;
+    fn ptr_to_int(&mut self, ptr: Self::Pointer) -> Result<u64, Error>;
 
     /// Cast the given integer to a pointer.
-    fn int_to_ptr(&mut self, int: u64) -> Result<Self::Pointer, Self::Error>;
+    fn int_to_ptr(&mut self, int: u64) -> Result<Self::Pointer, Error>;
 }
 
 /// The rules applying to this pointer offset operation.

wip/value-domain.md

@@ -0,0 +1,120 @@
+# Rust Value Domain
+
+**Note:** This document is not normative nor endorsed by the UCG WG. Its purpose is to be the basis for discussion and to set down some key terminology.
+
+The purpose of this document is to describe what the set of *all possible values* is in Rust.
+This is an important definition: one key element of a Rust specification will be to define the [representation relation][representation] of every type.
+This relation relates values with lists of bytes, so before we can even start specifying the relation we have to specify the involved domains.
+`Byte` is defined as part of [the memory interface][memory-interface]; this document is about defining `Value`.
+
+[representation]: https://github.com/rust-lang/unsafe-code-guidelines/blob/master/reference/src/glossary.md#representation
+[memory-interface]: memory-interface.md
+
+## Values
+
+The Rust value domain is described by the following (incomplete) type definition (in terms of an arbitrary `Pointer` type instantiated by [the memory interface][memory-interface]):
+
+```rust
+enum Value<Pointer> {
+    /// A mathematical integer.
+    Int(BigInt),
+    /// A Boolean value.
+    Bool(bool),
+    /// A pointer.
+    Ptr(Pointer),
+    /// A zero-sized "unit".
+    Unit,
+    /// An uninitialized value.
+    Uninit,
+    /// An n-tuple.
+    Tuple(Vec<Self>),
+    /// A variant of a sum type.
+    Variant {
+        idx: u64,
+        data: Box<Self>,
+    },
+    /* ... */
+}
+```
+
+As Rust grows, we might expand this definition. That is okay; all previously defined representation relations are still well-defined when the domain grows, the newly added values will just not be valid for old types as one would expect.
+
+## Example value relations
+
+We show some examples for how one might want to use this `Value` domain to define the value relation for a type.
+
+### `bool`
+
+The value relation for `bool` relates `Bool(true)` with `[Raw(0)]` and `Bool(false)` with [`Raw(1)`], and that's it.
+
+### `()`
+
+The value relation for the `()` type relates `Unit` with the empty list `[]`, and that's it.
+
+### `!`
+
+The value relation for the `!` type is empty: nothing is related to anything at this type.
+
+### `#[repr(C)] struct Pair<T, U>(T, U)`
+
+The value relation for `Pair` us based on the value relations for `T` and `U`.
+A value `Tuple([t, u])` (assuming we can use array notation to "match" on `Vec`) is represented by a list of bytes `rt ++ pad1 ++ ru ++ pad2` (using `++` for list concatenation) if:
+
+* `t` is represented by `rt` at type `T`.
+* `u` is represented by `ru` at type `U`.
+* The length of `rt ++ pad1` is equal to the offset of the `U` field.
+* The length of the entire list `rt ++ pad1 ++ ru ++ pad2` is equal to the size of `Pair<T, U>`.
+
+This relation demonstrates that value of type `Pair` are always 2-tuples (aka, pairs).
+It also shows that the actual content of the padding bytes is entirely irrelevant, we only care to have the right number of them to "pad" `ru` to the right place and to "pad" the entire list to have the right length.
+
+### `&T`/`&mut T`
+
+Reference types are tricky.
+But a possible value relation for sized `T` is:
+A value `Ptr(ptr)` is related to `[PtrFragment { ptr, idx: 0 }, ..., PtrFragment { ptr, idx: N-1 }]` where `N == size_of::<usize>()` if `ptr` is non-NULL and aligned to `align_of::<T>()`.
+
+### `u8`
+
+For the value representation of integer types, there are two different reasonable choices.
+Certainly, a value `Int(i)` where `i` in `0..256` is related to `[Raw(i as u8)]`.
+
+And then, maybe, we also want to additionally say that value `Uninit` is related to `[Uninit]`.
+This essentially corresponds to saying that uninitialized memory is a valid representation of a `u8` value (namely, the uninitialized value).
+
+## The role of the value representation in the operational semantics
+
+One key use of the value representation is to define a "typed" interface to memory:
+
+```rust
+trait TypedMemory: Memory {
+    /// Write a value of the given type to memory.
+    fn typed_write(&mut self, ptr: Self::Pointer, val: Value, ty: Type) -> Result<(), Error>;
+
+    /// Read a value of the given type.
+    fn typed_read(&mut self, ptr: Self::Pointer, ty: Type) -> Result<Value, Error>;
+}
+```
+
+here, `Type` is some representation of the Rust type system (akin to [`Ty`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/type.Ty.html) in the compiler).
+We can implement `TypedMemory` for any `Memory` as follows:
+* For `typed_write`, pick any representation of `val` for `ty`, and call `Memory::write`. If no representation exists, we have UB.
+* For `typed_read`, read `ty.size()` many bytes from memory, and then determine which value this list of bytes represents. If it does not represent any value, we have UB.
+
+In particular, this defines the semantics of a "typed copy": when an assignment is executed in Rust (at some type `T`), or when an argument of type `T` is passed to a function or a return value of type `T` returned from a function, this is called a "typed copy".
+Its semantics is basically to do a `typed_read` at `T` followed by a `typed_write` at `T`.
+In particular, this means doing a "typed copy" at `T` of some memory that has no valid representation at `T` is undefined behavior!
+This also means that for types that have padding, the "typed copy" does not preserve the padding bytes.
+
+## Relation to validity invariant
+
+One way we *could* also use the value representation (and the author things this is exceedingly elegant) is to define the validity invariant.
+Certainly, it is the case that if a list of bytes is not related to any value for a given type `T`, then that list of bytes is *invalid* for `T` and it should be UB to produce such a list of bytes at type `T`.
+We could decide that this is an "if and only if", i.e., that the validity invariant for a type is exactly "must be in the value representation".
+For many types this is likely what we will do anyway (e.g., for `bool` and `!` and `()` and integers), but for references, this choice would mean that *validity of the reference cannot depend on what memory looks like*---so "dereferencable" and "points to valid data" cannot be part of the validity invariant for references.
+The reason this is so elegant is that, as we have seen above, a "typed copy" already very naturally is UB when the memory that is copied is not a valid representation of `T`.
+This means we do not even need a special clause in our specification for the validity invariant---in fact, the term does not even have to appear in the specification---as everything juts falls out of how a "typed copy" applies the value representation twice.
+
+Justifying the `dereferencable` LLVM attribute is, in this case, left to the aliasing model (e.g. [Stacked Borrows]), just like that is needed to justify the `noalias` attribute.
+
+[Stacked Borrows]: stacked-borrows.md