Show first example in annotated form early

[web.git] / ralf / _posts / 2018-08-22-two-kinds-of-invariants.md

diff --git a/ralf/_posts/2018-08-22-two-kinds-of-invariants.md b/ralf/_posts/2018-08-22-two-kinds-of-invariants.md
index e87202f376c6b1f741f5d1151a35261ee57ba129..34f33bb9c0a788803459d4be020eb2de79b2050c 100644 (file)
--- a/ralf/_posts/2018-08-22-two-kinds-of-invariants.md
+++ b/ralf/_posts/2018-08-22-two-kinds-of-invariants.md
@@ -1,6 +1,7 @@
 ---
 ---

-title: "Two Kinds of Invariants"
+title: "Two Kinds of Invariants: Safety and Validity"

 categories: internship rust
 categories: internship rust

+forum: https://internals.rust-lang.org/t/two-kinds-of-invariants/8264

 ---
 
 When talking about the Rust type system in the context of unsafe code, the discussion often revolves around *invariants*:
 ---
 
 When talking about the Rust type system in the context of unsafe code, the discussion often revolves around *invariants*:


@@ -28,7 +29,8 @@ In fact, this is the main point of the safety invariant:
 Based on that, it should not be hard to fill in the invariant for some more types.
 For example, `&bool` is an aligned, non-NULL reference to allocated read-only memory (because safe code can dereference) such that the data stored in that memory is safe at `bool` (because safe code can work on that `bool` after dereferencing).
 This kind of "structural recursion" is happening everywhere for safety invariants: `x` is safe for `(T, U)` if `x.0` is safe for `T` and `x.1` is safe for `U`.
 Based on that, it should not be hard to fill in the invariant for some more types.
 For example, `&bool` is an aligned, non-NULL reference to allocated read-only memory (because safe code can dereference) such that the data stored in that memory is safe at `bool` (because safe code can work on that `bool` after dereferencing).
 This kind of "structural recursion" is happening everywhere for safety invariants: `x` is safe for `(T, U)` if `x.0` is safe for `T` and `x.1` is safe for `U`.

-`x` is safe for `Option<T>` if either the discriminant is `None`, or it is `Some` and the data is safe for `T`.
+As far as enums is concerned, for example `x` is safe for `Option<T>` if either the discriminant is `None`, or it is `Some` and the data is safe for `T`.
+Similarly, `x` is never safe for `!` -- there just is no valid discriminant that `x` could have.

 
 When we talk about integer types like `i32`, it is tempting to say that *all* data is safe at `i32`.
 However, that does not actually work: As [I discussed in a previous post]({% post_url 2018-07-24-pointers-and-bytes %}), the "bytes" that make up data have more possible states than just `0..256`.
 
 When we talk about integer types like `i32`, it is tempting to say that *all* data is safe at `i32`.
 However, that does not actually work: As [I discussed in a previous post]({% post_url 2018-07-24-pointers-and-bytes %}), the "bytes" that make up data have more possible states than just `0..256`.


@@ -37,6 +39,7 @@ Some operations like `if x != 0 { ... }` are undefined behavior if `x` is uninit
 
 For reference types, some of the details are [harder to define]({% post_url 2018-04-05-a-formal-look-at-pinning %}), but we can still roughly say that a pointer is safe for `&'a mut T` if it is aligned, non-NULL and points to allocated memory that, for lifetime `'a`, no other pointer accesses, and such that the data stored in memory at that location is safe for `T`.
 Similarly (and [ignoring interior mutability]({% post_url 2018-01-31-sharing-for-a-lifetime %})), a pointer is safe for `&'a T` if it is aligned, non-NULL and points to allocated memory that is not mutated for lifetime `'a` and such that the data stored in memory is safe for `T`. The safety of `&bool` that we discussed above is just an instance of this general definition.
 
 For reference types, some of the details are [harder to define]({% post_url 2018-04-05-a-formal-look-at-pinning %}), but we can still roughly say that a pointer is safe for `&'a mut T` if it is aligned, non-NULL and points to allocated memory that, for lifetime `'a`, no other pointer accesses, and such that the data stored in memory at that location is safe for `T`.
 Similarly (and [ignoring interior mutability]({% post_url 2018-01-31-sharing-for-a-lifetime %})), a pointer is safe for `&'a T` if it is aligned, non-NULL and points to allocated memory that is not mutated for lifetime `'a` and such that the data stored in memory is safe for `T`. The safety of `&bool` that we discussed above is just an instance of this general definition.

+In particular, it is impossible to have a safe `&!` because it would have to point to a safe `!`, which does not exist.

 
 The safety invariant gets particularly interesting for higher-order data like function pointers or trait objects.
 For example, when is `f` safe at type `fn(bool) -> i32`?
 
 The safety invariant gets particularly interesting for higher-order data like function pointers or trait objects.
 For example, when is `f` safe at type `fn(bool) -> i32`?


@@ -99,12 +102,17 @@ But that's okay, because this is carefully controlled unsafe code -- and by the
 
 > *Unsafe code only has to uphold safety invariants at the boundaries to safe code.*
 
 
 > *Unsafe code only has to uphold safety invariants at the boundaries to safe code.*
 

+Notice that the "boundary" is not necessarily where the `unsafe` block ends.
+The boundary occurs where the unsafe code provides a public API that safe code is intended to use -- that might be at the module boundary, or it might even be at the crate level.
+That is where safe code should be able to rely on safety, so that it can interact with the unsafe code without triggering undefined behavior, and hence that is where the safety invariants come into play.
+

 This is in strong contrast to validity, which must *always* hold.
 Layout optimizations and LLVM's attributes are in effect throughout unsafe code, so it is never okay to ever have invalid data.
 This is in strong contrast to validity, which must *always* hold.
 Layout optimizations and LLVM's attributes are in effect throughout unsafe code, so it is never okay to ever have invalid data.

+(With the sole restriction of data which *the compiler statically knows is not initialized*: If you write `let b: bool;`, that data in `b` is kept inaccessible *even to unsafe code*, and it does not have to satisfy any invariant. This works because the compiler knows about `b` not being initialized.)

 
 > *Unsafe code must always uphold validity invariants.*
 
 
 > *Unsafe code must always uphold validity invariants.*
 

-So we clearly cannot just pick the same invariant for both.
+So we clearly cannot just pick the same invariant for both, or else it would be impossible to write `Vec`.

 We *might* want to just ignore user-defined invariants when it comes to validity, but I think that would be ill-advised.
 
 First of all, validity is part of the definition of undefined behavior.
 We *might* want to just ignore user-defined invariants when it comes to validity, but I think that would be ill-advised.
 
 First of all, validity is part of the definition of undefined behavior.


@@ -138,6 +146,7 @@ And finally, all safe data must also be valid, so the safety invariant also impo
 For `bool`, we stick to the same invariant as for safety: It must be `true` or `false`.
 This invariant is already exploited by enum layout optimizations, so violating it *at any time* can break your code.
 More generally speaking, validity requires correct enum discriminants.
 For `bool`, we stick to the same invariant as for safety: It must be `true` or `false`.
 This invariant is already exploited by enum layout optimizations, so violating it *at any time* can break your code.
 More generally speaking, validity requires correct enum discriminants.

+One consequence of this is that no data is valid at `!`.

 
 Similar to safety, validity is structural -- so validity for `(T, U)` requires that the first field is valid at `T`, and the second field is valid at `U`.
 
 
 Similar to safety, validity is structural -- so validity for `(T, U)` requires that the first field is valid at `T`, and the second field is valid at `U`.
 


@@ -150,6 +159,9 @@ It is often useful to be able to call a method that takes `&mut` on a partially
 Doing all that with raw pointers is much less ergonomic, and making people write less ergonomic code will inadvertently lead to more bugs.
 Moreover, the *benefits* of making this validity for reference structural (i.e., `&T` is valid only if it points to a valid `T`) seem slim (though @comex [came up with an optimization that would require this](https://internals.rust-lang.org/t/stacked-borrows-an-aliasing-model-for-rust/8153/25?u=ralfjung)).
 
 Doing all that with raw pointers is much less ergonomic, and making people write less ergonomic code will inadvertently lead to more bugs.
 Moreover, the *benefits* of making this validity for reference structural (i.e., `&T` is valid only if it points to a valid `T`) seem slim (though @comex [came up with an optimization that would require this](https://internals.rust-lang.org/t/stacked-borrows-an-aliasing-model-for-rust/8153/25?u=ralfjung)).
 

+A consequence of this is would be that while `&!` does not have a safe inhabitant, it *is* possible to have data that is valid for `&!`.
+After all, it does not have to point to a valid `!` (which would be impossible).
+

 One point that we *already* assume, however, is that references are dereferencable.
 We even tell LLVM that this is the case.
 It seems natural to make that part of validity.
 One point that we *already* assume, however, is that references are dereferencable.
 We even tell LLVM that this is the case.
 It seems natural to make that part of validity.


@@ -173,11 +185,11 @@ My gut feeling is that it should not be (i.e., validity should require that `i32
 I have talked about two kinds of invariants that come with every type, the safety invariant and the validity invariant.
 For unsafe code authors, the slogan summarizing this post is:
 
 I have talked about two kinds of invariants that come with every type, the safety invariant and the validity invariant.
 For unsafe code authors, the slogan summarizing this post is:
 

-> *You must always be valid, but you must not always be safe.*
+> *You must always be valid, but you only must be safe in safe code.*

 
 I think we have enough experience writing unsafe code at this point that we can reasonably discuss which validity invariants make sense and which do not -- and I think that it is high time that we do so, because many unsafe code authors are wondering about these exact things all the time.
 
 The plan is to open issues in the [UCG RFCs repo](https://github.com/rust-rfcs/unsafe-code-guidelines/) soon-ish, one issue for each type family that we need to make decisions on wrt. validity.
 
 I think we have enough experience writing unsafe code at this point that we can reasonably discuss which validity invariants make sense and which do not -- and I think that it is high time that we do so, because many unsafe code authors are wondering about these exact things all the time.
 
 The plan is to open issues in the [UCG RFCs repo](https://github.com/rust-rfcs/unsafe-code-guidelines/) soon-ish, one issue for each type family that we need to make decisions on wrt. validity.

-<!-- Meanwhile, if you have any comments or questions, feel free to join us in the forum! -->
+Meanwhile, if you have any comments or questions, feel free to join us in the [forum](https://internals.rust-lang.org/t/two-kinds-of-invariants/8264)!

 
 #### Footnotes
 
 #### Footnotes