restructure pinning post a bit

diff --git a/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md b/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md
index 98b53a18eea36c911f55de6f30f4733c83da360b..989dae55f92f4dcf024385db17daaa6b63209a65 100644 (file)
--- a/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md
+++ b/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md
@@ -4,10 +4,10 @@ categories: research rust
 forum: https://internals.rust-lang.org/t/a-formal-look-at-pinning/7236
 ---
 
 forum: https://internals.rust-lang.org/t/a-formal-look-at-pinning/7236
 ---
 

-Recently, a new API for "pinned references" has [landed as a new unstable feature](https://github.com/rust-lang/rust/pull/49058) in the standard library.
+Recently, a new [API for "pinned references"](https://github.com/rust-lang/rfcs/blob/master/text/2349-pin.md) has [landed as a new unstable feature](https://github.com/rust-lang/rust/pull/49058) in the standard library.

 The purpose of these references is to express that the data at the memory it points to will not, ever, be moved elsewhere.
 The purpose of these references is to express that the data at the memory it points to will not, ever, be moved elsewhere.

-Others have [written](https://boats.gitlab.io/blog/post/2018-03-20-async-vi/) about why this is important in the context of async IO.
-The purpose of this post is to take a closer, more formal look at that API: We are going to take a stab at extending the RustBelt model of types with support for pinning.
+@withoutboats has written about how this [solves](https://boats.gitlab.io/blog/post/2018-03-20-async-vi/) a [problem in the context of async IO](https://boats.gitlab.io/blog/post/2018-01-25-async-i-self-referential-structs/).
+In this post, we take a closer, more formal look at that API: We are going to take a stab at extending the RustBelt model of types with support for pinning.

 
 <!-- MORE -->
 
 
 <!-- MORE -->
 


@@ -121,29 +121,20 @@ forall |'a, ptr|
   borrowed('a, exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes))
   -> T.shr('a, ptr)
 ```
   borrowed('a, exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes))
   -> T.shr('a, ptr)
 ```

-I am using the usual mathematical quantifiers, with a Rust-y syntax (`forall |var| P` and `exists |var| P`), and `->` for implication.
+This is a formal statement that we have to prove whenever we define `T.own` and `T.shr` for our own type `T`.
+It says that for all lifetimes `'a` and pointers `ptr`, if `borrowed('a, ...)` holds, then `T.shr('a, ptr)` holds.
+I am using the usual mathematical quantifiers, with a Rust-y syntax (`forall |var| ...` and `exists |var| ...`), and `->` for implication.

 For disjunction (`||`) and conjunction (`&&`), I follow Rust.
 
 For disjunction (`||`) and conjunction (`&&`), I follow Rust.
 

-We also need some way to talk about ownership and contents of memory:
-I will write `ptr.points_to_owned_bytes(bytes)` (where `ptr: Pointer` and `bytes: List<Byte>`) to express that `ptr` points to `bytes.len()` many bytes of memory containing the given `bytes` of data, and that moreover, we *own* that memory.
-Ownership here means that we are free to read, write and deallocate that memory.
+Because Rust types are a lot about pointers and what they point to, we also need some way to talk about memory:
+`ptr.points_to_owned(bytes)` (where `ptr: Pointer` and `bytes: List<Byte>`) means that `ptr` points to `bytes.len()` many bytes of memory containing the given `bytes` of data, and that moreover, we *own* that memory.
+*Ownership* here means that we are free to read, write and deallocate that memory, and that we are the only party that can do so.

 
 

-Frequently, it is more convenient to not talk about raw lists of bytes but about some higher-level representation of the bytes, and not care about how exactly that data is laid out in memory.
-For example, we might want to say that `ptr` points to `42` of type `i32` by saying `ptr.points_to_owned(42i32)`.
-We can define a suitable `points_to_owned` as
-```
-ptr.points_to_owned(data: U) where List<Bytes>: TryInto<U> :=
-  exists |bytes| bytes.try_into() == Ok(data) && ptr.points_to_owned_bytes(bytes)
-```
-Here, we (ab)use the `TryInto` trait to convert a properly laid out list of bytes into something of type `U`.
-The conversion fails, in particular, if the list does not have exactly the right length.
-If `U == List<Bytes>`, this is just the same as `ptr.points_to_owned_bytes`.
-
-**Update:** In a previous version I called these predicates `mem_own_bytes` and `mem_own`. I decided that `points_to_owned` was actually easier to understand, and it also matches the standard terminology in the literature, so I switched to using that term instead. **/Update**
+**Update:** In a previous version I called this predicate `mem_own`. I decided that `points_to_owned` was actually easier to understand, and it also matches the standard terminology in the literature, so I switched to using that term instead. **/Update**

 
 Finally, `borrowed('a, P)` says that `P` is only temporarily owned, i.e., borrowed, for lifetime `'a`.
 
 Finally, `borrowed('a, P)` says that `P` is only temporarily owned, i.e., borrowed, for lifetime `'a`.

-`P` here is a *proposition* or *assertion*, i.e., a statement about what we expect to own. The axiom above is a proposition, as is `ptr.points_to_owned(42i32)`.
-You can think of propositions as a fancy version of `bool` where we can use things like quantifiers or borrowing, and talk about memory and ownership.
+`P` here is a *proposition* or *assertion*, i.e., a statement about what we expect to own. The axiom above is a proposition, as is `ptr.points_to_owned([0, 0])`.
+You can think of propositions as a fancy version of `bool` where we can use things like quantifiers and borrowing, and talk about memory and ownership.

 
 Let us see how we can define the owned typestate of `Box` and mutable reference using this notation:
 
 
 Let us see how we can define the owned typestate of `Box` and mutable reference using this notation:
 


@@ -161,8 +152,13 @@ Box<T>.own(bytes) := exists |ptr, inner_bytes| bytes.try_into() == Ok(ptr) &&
     exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))
 ```
 
     exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))
 ```
 

-It turns out that using `try_into` like we do above is actually a common pattern.
-We usually do not want to talk directly about the `List<Byte>` but convert them to some higher-level representation first.
+The `:=` means "is defined as"; this is a lot like a function definition in Rust where the part after the `:=` is the function body.
+Notice how we use `try_into` to try to convert a sequence of bytes into a higher-level representation, namely a pointer.
+This relies in `TryInto<U>` being implemented for `List<Byte>`.
+The conversion fails, in particular, if the list of bytes does not have exactly the right length.
+
+It turns out that using `try_into` like we do above is actually a common pattern:
+Often, when we define a predicate on bytes, we do not want to talk directly about the `List<Byte>` but convert them to some higher-level representation first.

 To facilitate this, we will typically define `T.own(data: U)` for some `U` such that `List<Byte>: TryInto<U>`, the idea being that the raw list of bytes is first converted to a `U` and the predicate can then directly access the higher-level data in `U`.
 This could look as follows:
 ```
 To facilitate this, we will typically define `T.own(data: U)` for some `U` such that `List<Byte>: TryInto<U>`, the idea being that the raw list of bytes is first converted to a `U` and the predicate can then directly access the higher-level data in `U`.
 This could look as follows:
 ```


@@ -212,6 +208,17 @@ Moreover, `SelfReferential` also has an owned and a shared typestate, but nothin
 With this choice, it is easy to justify that `read_ref` is safe to execute: When the function begins, we can rely on `SelfReferential.pin(self)`.
 If the closure in `self_ref.map` runs, we are in the `Some` case of the `match` so the deref of the pointer obtained from `self_ref` is fine.
 
 With this choice, it is easy to justify that `read_ref` is safe to execute: When the function begins, we can rely on `SelfReferential.pin(self)`.
 If the closure in `self_ref.map` runs, we are in the `Some` case of the `match` so the deref of the pointer obtained from `self_ref` is fine.
 

+Before we go on, I have to explain what I did with `points_to_owned` above.
+Before I said that this predicate operates on `List<Byte>`, but now I am using it on a pair of an `i32` and an `Option`.
+Again this is an instance of using a higher-level view of memory than a raw list of bytes.
+For example, we might want to say that `ptr` points to `42` of type `i32` by saying `ptr.points_to_owned(42i32)`, without worrying about how to turn that value into a sequence of bytes.
+It turns out that we can define `points_to_owned` in terms of a lower-level `points_to_owned_bytes` that operates on `List<Byte>` as follows:
+```
+ptr.points_to_owned(data: U) where List<Bytes>: TryInto<U> :=
+  exists |bytes| bytes.try_into() == Ok(data) && ptr.points_to_owned_bytes(bytes)
+```
+Just like before, we (ab)use the `TryInto` trait to convert a properly laid out list of bytes into something of type `U`.
+

 ## Verifying the Pin API
 
 With our notion of types extended with a pinned typestate, we can now justify the `Pin` and `PinBox` API.
 ## Verifying the Pin API
 
 With our notion of types extended with a pinned typestate, we can now justify the `Pin` and `PinBox` API.