just assume a memory model is in scope

Author: RalfJung

wip/memory-interface.md

@@ -28,7 +28,7 @@ Practically speaking, `Pointer` will be some representation of an "address", plu
 
 The unit of communication between the memory model and the rest of the program is a *byte*.
 Again, the question of "what is a byte" is not as trivial as it might seem; beyond `u8` values we have to represent `Pointer`s and [uninitialized memory][uninit].
-We define the `Byte` type (in terms of an arbitrary `Pointer` type) as follows:
+We define the `Byte` type as follows, where `Pointer` will later be instantiated with the `Memory::Pointer` associated type.
 
 ```rust
 enum Byte<Pointer> {
@@ -137,6 +137,9 @@ enum OffsetMode {
 }
 ```
 
+We will generally assume we have a particular memory model in scope, and freely refer to its `PTR_SIZE` and `Pointer` items.
+We will also write `Byte` for `Byte<Pointer>`.
+
 This is a very basic memory interface that is incomplete in at least the following ways:
 
 * To implement rules like "dereferencing a null, unaligned, or dangling raw pointer is UB" (even if no memory access happens), there needs to be a way to do an "alignment, bounds and null-check".

wip/value-domain.md

@@ -13,10 +13,10 @@ However, before we can even start specifying the relation, we have to specify th
 
 ## 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]):
+The Rust value domain is described by the following (incomplete) type definition (using the `Pointer` type defined by [the memory interface][memory-interface]):
 
 ```rust
-enum Value<Pointer> {
+enum Value {
     /// A mathematical integer, used for `i*`/`u*` types.
     Int(BigInt),
     /// A Boolean value, used for `bool`.
@@ -33,7 +33,7 @@ enum Value<Pointer> {
         data: Box<Self>,
     },
     /// A "bag of raw bytes", used for unions.
-    RawBag(Vec<Byte<Pointer>>),
+    RawBag(Vec<Byte>),
     /* ... */
 }
 ```