I'm currently working on a compiler (written in C++) that intends to implement C++, Rust, and a few other languages. I had a few questions about how lifetimes work with borrow checking, as I will be implementing that at some point. This could also serve as a basis for rigourously specifying the borrow checker. Note that in the below rules, the term "object" is used in the same manner as it is in the C++ Standard ISO 14882, and has the same definition as provided there.
These are the High Level Rules I have interpreted as being applicable:
- A type T is bounded by a lifetime 'a, iff it is a reference type with lifetime 'a, or it contains 1 or more members which are bounded by lifetime 'a
- A type which is not bounded by any lifetime 'a, as defined by rule 1, is said to be bounded by 'static.
- A type T satisfies lifetime 'a, if it is bounded by some lifetime 'b, such that either 'b is exactly the lifetime 'a, or 'b starts before 'a, and ends after 'a. Note -- The lifetime 'static starts before any lifetime other than 'static, and ends after all lifetimes other than 'static -- End Note
- There shall be no reference types to any type T, with lifetime 'a, except where T satisfies 'a
- An object created with the static specifier has lifetime 'static.
- An object created at block scope without the static specifier has a lifetime which starts immediately after its initializer, and ends not later than the end of the block scope it is declared it, before all object's for which the lifetime started before that object. Note -- Such an object has automatic lifetime -- End Note
- A type T has non-trivial destruction if that type implements the Drop trait, or any member of the type has non-trivial destruction. A type T does not have non-trivial destruction has trivial destruction. Note -- An instantiation of the type
core::marker:PhantomData<T>has non-trivial destruction if and only if
Thas non-trivial destruction -- End Note
- The lifetime of an object with a type that has non-trivial destruction, and which is not moved, ends at the end of the block scope it is declared in, as per rule 6. Otherwise the lifetime ends at the last point the object is used or to the end of the lifetime the object is borrowed, whichever is longest.
- The lifetime of a temporary object ends after the full expression which creates it, unless the object is borrowed. The lifetime of a borrowed temporary object is the length of the lifetime it is borrowed for.
- The lifetime of any object ends when the object is moved. Note -- An object of a type T which implements the Copy Trait is never moved -- End Note
- A borrow without an explicit lifetime is for the length of the reference object it creates.
- A non-mutable borrow shall not be created for an object at block scope and automatic lifetime if there exists a mutable borrow of the same object for which the lifetime has started and not yet ended. Note -- An object created in a non-mutable binding can always be borrowed non-mutably -- End note
- A mutable borrow shall not be created for an object at block scope and automatic lifetime if there exists any other borrow of the same object for which the lifetime as started and not yet ended. Note -- This implies there can only be at most one mutable borrow of an object -- End Note
- A mutable reference may be dereferenced, and the result borrowed, which produces a new reference (mutable or non-mutable) to the same object with a smaller lifetime. The original reference may not be accessed for the lifetime of the new reference, except that if the new reference is to a field, the original reference may be accessed to borrow other fields of the same object. Note -- This implies that if a mutable reference is reborrowed as non-mutable, the object cannot be mutated through the mutable reference for the lifetime of the non-mutable reference -- End Note
- A non-mutable reference may be derefereced, and the result borrowed, which produces the same reference, which has a potentially smaller lifetime. Note -- This operation is identical to copying the reference -- End Note
- For the purposes of the above rules, the instantiation of the type
core::marker::PhantomData<T>is considered to have a single field of type
T, except that this field cannot be named and does not affect the size or alignment requirements of the type.
Would the above 15 rules (that's a lot) be sufficient for soundness from a rust compiler?