When exactly is a constant well formed?

[lcnr]

So my current understanding is that all constants used in types must be well formed.

I wasn't able to find any discussion on what exactly that means though 😅

I think that for concrete constants the following must hold:

Constants evaluate successfully

This means that all of 1usize - 2, panic!(), loop {} and [1, 2, 3][3] are not well formed as constants.

An evaluated constant must satisfy all lang invariants of its type

So something like unsafe { std::mem::transmute::<u8, bool>(2) } is not wf.
I do think that the following would be well formed though, as it only breaks library invariants:

const V: &'static str = unsafe { std::mem::transmute::<&[u8], &str>(&[0xff, 0xff, 0xff, 0xff]) };

---

The more interesting case are polymorphic constants as we can't just evaluate them.
For these I think the following rule is appropriate

A polymorphic constant is well formed, iff all possible concrete instances are well formed

Some examples:

use std::mem::size_of;

fn foo<T>() -> [u8; size_of::<T>()] {}
// well formed, as `size_of::<T>()` returns a wf constant no matter the type of `T`.

fn bar<T>() -> [u8; 64 / size_of::<T>()] {}
// not well formed, as `64 / size_of::<()>()` does not evaluate successfully and is therefore not wf.

struct Baz<const V: bool>;
fn baz<T>() -> Baz<{ unsafe { std::mem::transmute::<u8, bool>(size_of::<T>() as u8) }> {}
// not well formed, for any `T` with `size_of::<T>() > 3` the final value is not a valid bool. 

Does this definition make sense?

[lcnr]

cc @oli-obk @RalfJung @eddyb

[oli-obk]

Nit:

fn baz<T>() -> [u8; unsafe { std::mem::transmute<u8, bool>(size_of::<T>()) }]
// not well formed, for any `T` with `size_of::<T>() > 3` the final value is not a valid bool. 

needs to be

fn baz<T>() -> [u8; unsafe { std::mem::transmute<u8, bool>(size_of::<T>() as u8) as usize }]
// not well formed, for any `T` with `size_of::<T>() > 3` the final value is not a valid bool. 

We currently do not detect this case because of performance reasons. It is trivial (a single flag) to turn on that locals are checked for validty after each modifiction

[lcnr]

We detect it in the final value of a constant afaict. So const N: bool = unsafe { std::mem::transmute::<u8, bool>(2) }; already causes a compile time error.

error[E0080]: it is undefined behavior to use this value
 --> src/lib.rs:1:1
  |
1 | const N: bool = unsafe { std::mem::transmute::<u8, bool>(2) };
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ type validation failed: encountered 0x02, but expected a boolean
  |
  = note: The rules on what exactly is undefined behavior aren't clear, so this check might be overzealous. Please open an issue on the rustc repository if you believe it should not be considered undefined behavior.

[oli-obk]

Yes, but we don't detect it in intermediate computations like when it's stored in a local variable but never returned.

[programmerjake]

This means that all of 1 - 2, panic!(), loop {} and [1, 2, 3][3] are not well formed as constants.

1 - 2 evaluates successfully for signed types. maybe you meant something like: 1 - 2usize?

[RalfJung]

A polymorphic constant is well formed, iff all possible concrete instances are well formed

The problem with this definition is that it is uncheckable (except with major effort).

I thought the point of well-formedness is for the compiler to check it? Similar to how it checks that e.g. lifetimes appropriately outlive each other? If that is the case, we need a notion of well-formedness that is efficiently decidable -- which the one I quoted above is not.

[oli-obk]

The problem with this definition is that it is uncheckable (except with major effort).

The way that it is proposed to check this is very cheap: If it is still generic, you need a 1:1 copy of the constant in a where bound (so exposing the fact that you need this constant to be evaluable to the caller), and then the caller either does the same, or (if it's monomorphic now), evaluates it. If it evaluates successfully, the bound is satisfied and the constant is well formed.

[RalfJung]

So basically this system punts the question of polymorphic constants? We don't even define what well-formedness means for them, but we ensure that the context always assumes well-formedness?

I'm somewhat surprised this works, and it also seems very restrictive, but -- yeah, sounds plausible. I'd change the text then and not say things like "polymorphic constants are well-formed if all instances are well-formed". Such a statement says that e.g. this is well-formed:

fn bar<T>() -> [u8; 64 + align_of::<T>() * 0] {}

Or this:

fn bar<T>() -> [u8; 64 / std::min(size_of::<T>(), 1)] {}

But it's not well-formed, due to a lack of where clause. There is simply no rule one can use to prove a polymorphic const well-formed, which makes "forward assumption to caller" the only option.

[lcnr]

I don't see why "The problem with this definition is that it is uncheckable" is a problem in practice.

Just like the borrow checker prevents programs which are theoretically correct, so too can our const well formed check forbid theoretically correct problems.

So at least with how I understand this, both 64 + align_of::<T>() * 0 and 64 / std::min(size_of::<T>(), 1) are well formed, we just aren't currently able to prove this.

So we could theoretically add a potentially unsafe function fn std::constant::evaluatable_unchecked<T>(v: T) -> T { v } in the future, which allows the user to write const expressions we assume to be wf without checking it

[oli-obk]

So basically this system punts the question of polymorphic constants?

yes

We don't even define what well-formedness means for them, but we ensure that the context always assumes well-formedness?

yes

I'm somewhat surprised this works, and it also seems very restrictive, but -- yeah, sounds plausible

it is very restrictive, but it's not actually worse than the status quo (typenum's trait bounds work exactly the same way). We can in the future add more general WF restrictions like X > 10 or sth, which will stop requiring WF bounds for X - 10, X - 9, ... but still require them for X - 11, but any such improvements can be added in a nonbreaking way later.

[RalfJung]

So at least with how I understand this, both 64 + align_of::() * 0 and 64 / std::min(size_of::(), 1) are well formed, we just aren't currently able to prove this.

But then we need a different name for "the thing the compiler checks". So far, "well-formedness" was the thing that the compiler checked, not a more relaxed thing that we could theoretically also allow. This RFC does a good job of describing that thing (though it may be outdated). In the syntax of that RFC, there would simply be no rule that says when polymorphic consts are well-formed, which implicitly makes forwarding the requirement the only way.

If you suddenly use the term "well-formed" for something that is not what the compiler actually checks, that is going to be very confusing. Please don't change the meaning of established terms like that.

---

I thus propose that we say something like:

• All constants are considered well-formed if they also appear in a where clause, thus forwarding the well-formedness requirements to the caller. (This is not specific to consts, it applies to all forms of well-formedness. We just repeat it here for clarity.)
• Additionally, monorphic consts are well-formed if ...

---

Regarding the monomorphic case, shouldn't it also require that the constant must be convertible to a value tree?

[RalfJung]

So we could theoretically add a potentially unsafe function fn std::constant::evaluatable_unchecked(v: T) -> T { v } in the future, which allows the user to write const expressions we assume to be wf without checking it

I doubt we can do that, actually. Much of the compiler relies on well-formedness as an invariant, as far as I know. Such a method would likely trigger ICEs all over the place.

I don't think the theoretical possibility of re-architecting everything to allow such a method justifies what I consider to be a change in the meaning of the pre-existing term "well-formedness".

[lcnr]

Such a method would likely trigger ICEs all over the place.

Then it has to be unsafe, because it can trigger undefined behavior.

It seems like I also have to look at the currently used definitions for well-formed because it seems like we currently assign it a slightly different meaning.

[RalfJung]

Then it has to be unsafe, because it can trigger undefined behavior.

ICEs have nothing to do with UB. In other words, even unsafe code must not be able to trigger ICEs during compilation.

[lcnr]

ICEs have nothing to do with UB. In other words, even unsafe code must not be able to trigger ICEs during compilation.

This seems like a weird restriction on what UB may do. I strongly disagree here.