more disucssion of retag redundancy check

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

diff --git a/personal/_posts/2018-08-22-two-kinds-of-invariants.md b/personal/_posts/2018-08-22-two-kinds-of-invariants.md
index b403c70b1f58d38eb5cbde43728c310d6a4aa12e..34f33bb9c0a788803459d4be020eb2de79b2050c 100644 (file)
--- a/personal/_posts/2018-08-22-two-kinds-of-invariants.md
+++ b/personal/_posts/2018-08-22-two-kinds-of-invariants.md
@@ -1,5 +1,5 @@
 ---
 ---

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

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


@@ -102,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.


@@ -180,7 +185,7 @@ 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.
 
 
 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.