This is an invariant that all the unsafe code implementing `Vec` maintains, and it is the invariant that the safe API surface of `Vec` expects the outside world to uphold.
The reason this works is that the fields mentioned in this invariant are all private, so safe code cannot break the invariant and use that broken invariant to cause havoc.
Again, the safety invariant is about ensuring safe execution of safe code.
This is an invariant that all the unsafe code implementing `Vec` maintains, and it is the invariant that the safe API surface of `Vec` expects the outside world to uphold.
The reason this works is that the fields mentioned in this invariant are all private, so safe code cannot break the invariant and use that broken invariant to cause havoc.
Again, the safety invariant is about ensuring safe execution of safe code.