}
{% endhighlight %}
-Now, `PinBox::deallocate` is pretty artificial, but in fact the [API for stack pinning](https://github.com/rust-lang/rfcs/blob/master/text/2349-pin.md#stack-pinning-api-potential-future-extension) that is drafted in the RFC, together with [`ManuallyDrop`](https://doc.rust-lang.org/beta/std/mem/union.ManuallyDrop.html), make it possible to obtain a `Pin<T>` to a stack-allocated `T` and subsequently pop the stack frame without calling `drop` on the `T`.
+Now, `PinBox::deallocate` is pretty artificial, but in fact the [API for stack pinning](https://github.com/rust-lang/rfcs/blob/master/text/2349-pin.md#stack-pinning-api-potential-future-extension) that is drafted in the RFC, together with [`ManuallyDrop`](https://doc.rust-lang.org/stable/std/mem/struct.ManuallyDrop.html), make it possible to obtain a `Pin<T>` to a stack-allocated `T` and subsequently pop the stack frame without calling `drop` on the `T`.
That has the same effect as `PinBox::deallocate`: It renders our collection interface unsound.
The concern about dropping pinned data is real.
)
```
Notice how we iterate over the elements of the list and make sure that we own whatever memory is to own there.
-(I love how `all` [really exists for iterators](https://doc.rust-lang.org/beta/std/iter/trait.Iterator.html#method.all) so I can express quantification over lists without any hassle. :)
+(I love how `all` [really exists for iterators](https://doc.rust-lang.org/stable/std/iter/trait.Iterator.html#method.all) so I can express quantification over lists without any hassle. :)
This invariant already justifies `print_all`: All the entries we are going to see there are in the list, so we have their `T.pin` at our disposal and are free to call `Debug::fmt`.
It seems perfectly fine to change `insert` to take `&Pin<Entry<T>>`.
I can't come up with any counter-example.
However, the formal model also cannot justify this variant of `insert`: Our model as defind previously defines `Pin<'a, T>.shr` in terms of `T.shr`.
-That made it easy to justify [`Pin::deref`](https://doc.rust-lang.org/nightly/std/mem/struct.Pin.html#method.deref).
+That made it easy to justify `Pin::deref`.
However, as a consequence, `Pin<'a, T>.shr` and `(&'a T).shr` are literally the same invariant, and hence `&Pin<T>` and `&&T` *are the same type*.
We could literally write functions transmuting between the two, and we could justify them in my model.
Clearly, `insert` taking `entry: &&T` would be unsound as nothing stops the entry from being moved later:
Others [have](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-373206171) [argued](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-378555691) for a shared pinned reference after it got removed from the API, and I argued against them as I did not understand how it could be useful.
Thanks for not being convinced by me!
-However, there is one strange aspect to this "shared pinned" typestate: Due to [`Pin::deref`](https://doc.rust-lang.org/beta/std/mem/struct.Pin.html#method.deref), we can turn a "shared pinned" reference into a shared reference.
+However, there is one strange aspect to this "shared pinned" typestate: Due to `Pin::deref`, we can turn a "shared pinned" reference into a shared reference.
We can go from `&Pin<T>` to `&&T`.
In other words, the shared pinned typestate invariant must *imply* the invariant for the (general, unpinned) shared typestate.
The reason for `Pin::deref` to exist is mostly a rustc implementation detail [related to using `Pin<Self>` as the type of `self`](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-372475895), but this detail has some significant consequences: Even with a separate shared pinned typestate, we can still not define `RefCell` in a way that a pinned `RefCell` pins its contents.
projects / web.git / blobdiff