notes on dynamic checks

Author: RalfJung

const.md

@@ -54,6 +54,11 @@ at type `&Option<Cell<i32>>` would be rejected by the naive analysis above, but
 is actually accepted by the compiler because we know that there is no
 `UnsafeCell` here that would permit interior mutability.
 
+*Dynamic check.* The Miri engine could check this dynamically by ensuring that
+the new data that is interned for a constant is all marked as
+immutable. (Constants referring to already existing mutable data are not
+inherently problematic.)
+
 ### 3. `Sync`
 
 Finally, the same constant reference is actually shared across threads.  This is
@@ -66,6 +71,8 @@ ecosystem that would break if we just started enforcing this now. See
 [this issue](https://github.com/rust-lang/rust/issues/49206) and the
 [PR attempting to fix this](https://github.com/rust-lang/rust/pull/54424/).
 
+*Dynamic check.* It is unclear how the Miri engine could dynamically check this.
+
 ### 4. Drop
 
 `Drop` is actually not an issue, at least not more so than for statics:
@@ -97,3 +104,6 @@ This is distinct to the concern about interior mutability above: That concern
 was about first computing a `&Cell<i32>` and then using it at run-time (and
 observing the fact that it has been "deduplicated"), this here is about using
 such a value at compile-time even though it might be changed at run-time.
+
+*Dynamic check.* The Miri engine could check this dynamically by refusing to
+access mutable global memory when computing a const.

promotion.md

@@ -51,6 +51,9 @@ earlier version of miri used to panic on arithmetic overflow even in release
 mode.  This breaks promotion, because now promoting code that would work (and
 could not panic!) at run-time leads to a compile-time CTFE error.
 
+*Dynamic check.* The Miri engine already dynamically detects panics, but the
+main point of promoteds is ruling them out statically.
+
 ### 2. Const safety
 
 We have explained what happens when evaluating a promoted panics, but what about
@@ -94,6 +97,9 @@ but to abort compilation of a program that would have compiled fine if we would
 not have decided to promote.  It is the responsibility of `foo` to not fail this
 way when working with const-safe arguments.
 
+*Dynamic check.* The Miri engine already dynamically detects const safety
+violations, but the main point of promoteds is ruling them out statically.
+
 ### 3. Drop
 
 Expressions returning "needs drop" types can never be promoted. If such an
@@ -110,6 +116,9 @@ it is unlikely to be the desired behavior in most cases and very likey to be con
 to the user. If such behavior is desired, the user can still use an explicit `static`
 or `const` item and refer to that.
 
+*Dynamic check.* The Miri engine could dynamically check this by ensuring that
+ the result of computing a promoted is a value that does not need dropping.
+
 ## `&` in `const` and `static`
 
 Promotion is also responsible for making code like this work:

static.md

@@ -30,3 +30,6 @@ static FOOO: Foo = Foo; // Ok, drop is never run
 // Not ok, cannot run `Foo::drop` because it's not a const fn
 static BAR: i32 = (Foo, 42).1;
 ```
+
+*Dynamic check.* The Miri engine dynamically checks that this is done correctly
+by not permitting calls of non-`const` functions.