Pinning chapter should define the Pin contract

[glyn]

The pinning chapter refers to "the Pin contract" three times:

It's important to note that stack pinning will always rely on guarantees you give when writing unsafe. While we know that the pointee of &'a mut T is pinned for the lifetime of 'a we can't know if the data &'a mut T points to isn't moved after 'a ends. If it does it will violate the Pin contract.

A mistake that is easy to make is forgetting to shadow the original variable since you could drop the Pin and move the data after &'a mut T like shown below (which violates the Pin contract):

For pinned data where T: !Unpin you have to maintain the invariant that its memory will not get invalidated or repurposed from the moment it gets pinned until when drop is called. This is an important part of the pin contract.

but there is no definition of what the Pin contract really is.

In the first reference:

It's important to note that stack pinning will always rely on guarantees you give when writing unsafe. While we know that the pointee of &'a mut T is pinned for the lifetime of 'a we can't know if the data &'a mut T points to isn't moved after 'a ends. If it does it will violate the Pin contract.

it is not clear that pinning (in the sense of this chapter: a pointer type being wrapped in the Pin type to guarantee that the referent won't be moved to a distinct address unless the type of the referent implements the Unpin trait) is necessarily being described here. If pinning in the sense of this chapter is not being described, then there is no implication for the Pin contract.

Similarly, it is not clear that the second reference is actually an example of the Pin contract being broken.

The third reference alludes to "an important part of the pin [sic] contract" as if there is another part of parts of the contract.

The pin module documentation doesn't define the Pin contract either.