There's currently no way to specify bounds requiring constants in types to be well-formed

[varkor]

When we have a const expression with a generic parameter in it, we cannot be sure that the const expression is valid for all the values that the generic parameter might take.

fn foo<const N: usize>() {
	let _: [u8; { /* some expression involving N */ }] = ...;
	// ^ this type may not be well-formed, because the length may result in an error
}

If we do not force the caller of the function to specify that the expression must be well-formed, we may get post-monomorphisation errors, as we can only determine that the expression is well-formed after substituting the concrete values for the generic parameters. We therefore need some way to specify such a bound. This is currently not possible.

This was discussed in #66962 (comment), #66962 (comment), #68388 (comment).

@eddyb suggested the syntax where [u8; { /* some expression involving N */ }]:, though it is not clear whether this would be appropriate. This needs some discussion and careful consideration of the WF implications.

[eddyb]

Note that the syntax where SomeType:, is already supported (empty bound list), and has been checked for WF-ness for a while now (e.g. where Vec<str>:, errors instead of being ignored).

However, where [(); N+N]:, currently tries to prove N+N can be evaluated the same way writing [(); N+N] in the body does, instead of requiring it of the caller of the function (which would be the useful behavior here).

I'm worried that while this may be a pragmatic way to write "this must const-eval successfully" bounds, it would go against WF principles to use it as such.

cc @rust-lang/wg-traits

[Evrey]

Suggesting new syntax, how about just adding this to the language?

where (bool_expr)

// E.g.:
struct Arr<T, const N: usize>
where T: Sized,
      (N <= (usize::max_value() / size_of::<T>())),
{
    data: [T; N],
}

Being mandatorily wrapped in brackets should be good enough to not need any special restrictions around the syntax for expressions evaluating to bool.

we may get post-monomorphisation errors

As long as ill-formed types error out, that's pretty much Good Enough™. Sure, proper bounds to error out early are much nicer, though. Note that this does require the compiler to check whether or not the bounds make sense at all. I.e. this should not compile, even if you don't use the type:

struct Arr<T, const N: usize>
where T: Sized,
      (N == 0),
{
    data: [T; {32 / N}], // D:
}

Edit: To clarify, in case someone fears O(scary) bool exprs… You are able to do just as scary things with where [T; {usize_expr}]:.

[oli-obk]

@Evrey what you're asking for is already possible:

struct Arr<T, const N: usize>
where T: Sized,
      Assert::<{N <= (usize::max_value() / std::mem::size_of::<T>())}>: IsTrue,
{
    data: [T; N],
}

enum Assert<const COND: bool> {}

trait IsTrue {}

impl IsTrue for Assert<true> {}

The problem lies elsewhere. It's that failure to evaluate the constant expression won't be linked to the fact that the user messed up the generic parameters:

#![feature(const_generics)]
#![allow(incomplete_features)]
struct Arr<const N: usize>
where Assert::<{N + N}>: IsValid,
{
}

enum Assert<const CHECK: usize> {}

trait IsValid {}

impl<const CHECK: usize> IsValid for Assert<CHECK> {}

fn main() {
    let x: Arr<{usize::max_value()}> = Arr {};
}

What we want to be able to avoid is having to work around this by writing

#![feature(const_generics)]
#![allow(incomplete_features)]
struct Arr<const N: usize>
where Assert::<{N < usize::max_value() / 2}>: IsTrue,
{
}

enum Assert<const CHECK: bool> {}

trait IsTrue {}

impl IsTrue for Assert<true> {}

fn main() {
    let x: Arr<{usize::max_value()}> = Arr {};
}

(which ICEs the compiler right now, I'm opening an issue for that)

[newpavlov]

I wonder how:

fn foo<const N: usize>() {
    let _: [u8; { 2*N }] = ...;
}

is fundamentally different from:

const fn double(n: usize) -> usize { 2*n }
fn foo<const N: usize>() {
    let _: [u8; { double(N) }] = ...;
}

Moreover, today we already can write const FOO: usize = double(usize::MAX); and it will fail with "any use of this value will cause an error" compile-time error (which is essentially a monomorphization-time error). And this error can be even turned off by #![allow(const_err)].

So arguably for consistency sake we should use the same behavior for inline expressions as well, maybe with some additional warnings asking to add bounds for trivial cases. In general case compiler would have to prove (or disprove) that provided bounds are sufficient to guarantee lack of overflow/underflow errors, which is far from trivial.

[lcnr]

@newpavlov they are not different (at least for const wf), we probably just missed one of these cases before #70107.

const fn double(v: usize) -> usize {
    v * 2
}

pub const FOO: usize = double(usize::MAX);

Is not a monomorphization error, at least not in the sense which is relevant here.
There are two problems which are somewhat unique to monomorphization errors.

They may not get detected when running cargo check, as they only happen during codegen.

They also require global reasoning, which is kind of bad when writing complex software :)

fn a<const N: usize>() {
    let _: [u8; N + 10];
}

fn foo<const N: usize>() {
    a::<{N * 2>()
}

fn main() {
    foo::<{usize::MAX / 2}>()
}

This causes a monomorphization error in fn a while computing the array length. But users of both foo and a don't
actually know this requirement without looking into a, so we get both a kind of unhelpful error (consider what happens if a is
in an extern crate), and can't very easily reason about what we need to do to prevent that error.

[newpavlov]

@lcnr
I agree that relying on global reasoning is far from ideal, but I just don't see a practical way to solve it in this case. Guaranteeing that a given const computation completes without errors for any possible input constrained by types and bounds is a realm of formal verification, which, unfortunately, is really impractical for general software (and some argue that there are fundamental reasons for that).

And let's not forget that underflow/overflow errors is just one class of errors, which could happen at "const runtime". What are fundamental reasons for special-casing them?

[lcnr]

Guaranteeing that a given const computation completes without errors for any possible input constrained by types and bounds is a realm of formally provable software, which, unfortunately, is really impractical for general software

Well, other people working on this might give you a more elaborate (correct) answer here, but we have to require this
(at least once trait bounds are involved)

trait A {
    fn foo();
}

impl<const N: usize> A for Const<N> {
    fn foo() {
        let _: [u8; N + 1];
    }
}

fn test<const N: usize>() where Const<N>: A {
    // ...
} 

I can think of some ways to keep this sound, but we have to prove that the const evaluation is successful
in the more general case (you can even consider GATs here).

[felix91gr]

Okay so probably this is overkill BUT.

I had this idea the other day that maybe one could put trait-like restrictions/predicates on const type parameters, e.g:

struct ModPNumber<p: const usize> where p: IsPrime {
...
}

The predicates for this case would be of type const fn (usize) -> bool (in this case anyway because usize isn't the only type that's valid in const contexts, but yoy get the idea).

If such a feature was to be implemented, the same predicate checker could be used at a lower level to check for well-formedness of the const parameters, right?

You couldn't write that restriction of well-formedness in the code being compiled, but I'm guessing that the same engine could be used internally to check for that property.

Maybe I'm missing an obvious edge case, though. Take this with a grain of salt. :3

[oli-obk]

While is_prime(p) bounds would work for concrete p, it seems quite hard to satisfy such a bound in a generic context where your p is actually some_const_fn(some_generic_parameter).

[felix91gr]

I don't understand. Why would it be hard? Maybe we're talking about different things. I'm imagining this:

• You have a const fn that you want to use as your bound. It receives a C (the type of your const type parameter) and returns a bool. For example, with C being a usize, it could be is_prime. It could also be is_odd, is_power_of_10, whatever fits in a const fn from C to bool.
• If p : C is the const type parameter to bind, it will eventually be computed, right? If so, it could be checked on all the const fn predicates.

On the other hand, I just realized something. You cannot compute something before checking if it is well-formed. Right? If so, I think my approach would not work... unless you had other machinery that checked well-formedness before each operation, or something like that. And that would work but would also be very costly on degenerate cases (eg computing 1000 by doing 1 + 1 + 1 + 1 + 1 .... + 1). Hmm.

[beepster4096]

#![feature(const_generics, const_evaluatable_checked)]

struct ArrayWrapper<T, const N: usize>([T; N]);

impl<T: Default, const N: usize> Default for ArrayWrapper<T, N> where [T; {N-1}]: {
    fn default() -> Self {
        Self([Default::default(); N])
    }
}

impl<T> Default for ArrayWrapper<T, 0> {
    fn default() -> Self {
        Self([])
    }
}

Currently, this code fails to compile because N-1 underflows. It would make more sense, in my opinion, if the underflow caused the impl to not apply to ArrayWrapper<T, 0>, as 0-1 not being valid would make 0 not satisfy the where clause.

[beepster4096]

Actually, it seems that this is the behavior when the default impl for ArrayWrapper<T, 0> is removed. I think this is a bug.

[lcnr]

@drmeepster this is a bug, and one of the most difficult ones we will have to face for this feature.

fixing that one will be a quite invasive change so we probably don't even want to fix it until we fixed most of the remaining issues here.

[beepster4096]

despite this, this feature is still advanced enough to reimplement transmute in pure rust:

#![feature(const_panic, const_generics, const_evaluatable_checked, untagged_unions)]

use std::mem::{ManuallyDrop, self};

struct ConstAssert<const Assert: ()>;

union TransmuteImpl<T, U>{
  t: ManuallyDrop<T>,
  u: ManuallyDrop<U>
}

const fn const_assert<T: Sized, U: Sized>(){
    assert!(mem::size_of::<T>() == mem::size_of::<U>(), "T and U must have same size");
    assert!(mem::align_of::<T>() == mem::align_of::<U>(), "T and U must have same alignment");
}

pub unsafe fn transmute<T: Sized, U: Sized>(t: T) -> U
where ConstAssert<{const_assert::<T, U>()}>: {
    ManuallyDrop::into_inner(TransmuteImpl{t: ManuallyDrop::new(t)}.u)
}

fn main(){
    unsafe{
        println!("{:?}", transmute::<u8, i8>(255))
    }
}

[oli-obk]

Nice! Although the const eval diagnostic is quite uninformative. Maybe we should report generic parameters in const eval errors, then at least we'd get enough details to track down potential call sites.

[newpavlov]

I would like to bring attention to the following application case. I am working on generic implementation of Weierstrass curve arithmetic and my code is littered with bounds like this

where
    C: WeirstrassCurve,
    WordsLen<C>: ArrayLength<Word> + Add<U1>,
    WideWordsLen<C>: ArrayLength<Word>,
    WordsP1Len<C>: ArrayLength<Word>,
    WordsBytesLen<C>: ArrayLength<u8>,
    DoubleWordsBytesLen<C>: ArrayLength<u8>,
    Words<C>: Copy,

These bounds straightforwardly translate to the "explicit dumb bounds" (proposal 2). Using type aliases I made it a bit nicer, but overall I have to explicitly specify that for a type containing constant BITS: usize, the following arrays are valid: [u8; BITS/8], [u8; BITS/4], [Word; BITS/WORD_SIZE], [Word; BITS/WORD_SIZE + 1], [Word; 2*BITS/WORD_SIZE]. Considering that reasonable curve sizes lie between 256 and 512 bits, those bounds do not improve code reliability in any way and effectively just add noise to the code.

BTW I think that the linked code is a good case for measuring advancement of const generics and const eval. Most constants in the WeirstrassCurve can be computed from others, but current version of const eval is not powerful enough (the main blocker is loops, but there are others, such as const trait methods and panics).

[memoryruins]

For an example where a reimplemented transmute helped, @Nemo157 and I used the feature for a proof of concept to restrict trait implementers to a word size in #74304 (comment) ( playground ). Since core::mem::transmute wasn't aware of the checks and would error, nemo used const_transmute to get around the error.

[memoryruins]

@oli-obk

Nice! Although the const eval diagnostic is quite uninformative. Maybe we should report generic parameters in const eval errors, then at least we'd get enough details to track down potential call sites.

It would definitely help to have a better idea of where the failed assert!s are coming from ^^

In the meantime, the following method yields more informative messages
(though the errors read like the "expected" is flipped)

#![feature(const_generics, const_evaluatable_checked)]

const fn eq_size<T, U>() -> bool {
    use core::mem::size_of;
    size_of::<T>() == size_of::<U>()
}

struct Assert<const EXPR: bool>;
trait True {}
impl True for Assert<true> {}

trait WordSized: Sized
where
    Assert<{ eq_size::<Self, *const ()>() }>: True, {}

impl WordSized for u32 {}
impl WordSized for u64 {}

error[E0308]: mismatched types
  --> src/lib.rs:17:6
   |
17 | impl WordSized for u32 {}
   |      ^^^^^^^^^ expected `false`, found `true`
   |
   = note: expected type `false`
              found type `true`

Trying something similar on @drmeepster's example -- while not a great message at least it shows the call site.

unsafe fn transmute<T: Sized, U: Sized>(t: T) -> U
where
    Assert<{ eq_size::<T, U>() }>: True,

error[E0308]: mismatched types
  --> src/main.rs:37:31
   |
37 |     unsafe { println!("{:?}", transmute::<u8, u16>(255)) }
   |                               ^^^^^^^^^^^^^^^^^^^^ expected `false`, found `true`
   |
   = note: expected type `false`
              found type `true`

[beepster4096]

Combing my method and @memoryruins's method leads to a more informative error, showing the call site but also showing an informative error message.

#![feature(const_panic, const_generics, const_evaluatable_checked, untagged_unions)]

use std::mem::{ManuallyDrop, self};

pub struct ConstAssert<const ASSERT: ()>;

union TransmuteImpl<T, U>{
  t: ManuallyDrop<T>,
  u: ManuallyDrop<U>
}

pub struct ConstCheck<const CHECK: bool>;

pub trait True{}

impl True for ConstCheck<true>{}

pub const fn transmute_check<T: Sized, U: Sized>() -> bool {
    mem::size_of::<T>() == mem::size_of::<U>() && mem::align_of::<T>() == mem::align_of::<U>()
}

pub const fn transmute_assert<T: Sized, U: Sized>(){
    assert!(mem::size_of::<T>() == mem::size_of::<U>(), "T and U must have same size");
    assert!(mem::align_of::<T>() == mem::align_of::<U>(), "T and U must have same alignment");
}

pub unsafe fn transmute<T: Sized, U: Sized>(t: T) -> U
where ConstCheck<{transmute_check::<T,U>()}>: True, ConstAssert<{transmute_assert::<T, U>()}>: {
    ManuallyDrop::into_inner(TransmuteImpl{t: ManuallyDrop::new(t)}.u)
}

fn main(){
    let i: u32 = unsafe{transmute([0u8; 4])};
}

errors with:

error[E0080]: evaluation of constant value failed
  --> src/main.rs:24:5
   |
24 |     assert!(mem::align_of::<T>() == mem::align_of::<U>(), "T and U must have same alignment");
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the evaluated program panicked at 'T and U must have same alignment', src/main.rs:24:5
   |
   = note: this error originates in a macro (in Nightly builds, run with -Z macro-backtrace for more info)

error[E0080]: evaluation of constant value failed
  --> src/main.rs:28:66
   |
28 | where ConstCheck<{transmute_check::<T,U>()}>: True, ConstAssert<{transmute_assert::<T, U>()}>: {
   |                                                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^ referenced constant has errors

error[E0308]: mismatched types
  --> src/main.rs:33:25
   |
33 |     let i: u32 = unsafe{transmute([0u8; 4])};
   |                         ^^^^^^^^^ expected `false`, found `true`
   |
   = note: expected type `false`
              found type `true`

While still being quite ugly, these errors tell both the call site and the panic message.

[oli-obk]

those bounds do not improve code reliability in any way and effectively just add noise to the code.

I do consider 2 * BITS / WORD_SIZE to be more readable than Quot<Prod<TWO, BITS>, WORD_SIZE>, but I get your point, there is some repetition here that we could eliminate. Basically we have

• BITS / 8,
• BITS / 4,
• BITS / WORD_SIZE,
• BITS / WORD_SIZE + 1
• 2 * BITS / WORD_SIZE.

The last three share BITS / WORD_SIZE, and I think a reasonable extension to the current exact matching scheme could be to handle sub-expressions, so we not need the BITS / WORD_SIZE bound, as it is already covered by the last two (or at least the second to last, since the 2 * BITS happens first).

Considering that reasonable curve sizes lie between 256 and 512 bits,

A further reasonable extension could be to ensure that we don't need to specify bounds that cannot possibly fail. So

• BITS / 8,
• BITS / 4,

are fine for any integer, as division by a positive nonzero integer can't ever be problematic

Another reasonable (albeit more complex) extension is that we could make

(BITS / WORD_SIZE) as usize + 1 not require a bound beyond BITS/WORD_SIZE if these two constants are of u8 type, just like we have infallibe usize: From<u8>

But any such comfort improvements should imo be a separate feature gate that will get stabilized after plain wf bounds, as the ability to do something at all is more important than the ability to do something conveniently

[newpavlov]

@oli-obk
You effectively describe path of special case handling of selected operators and types, which I've mentioned here. I don't think it's a sustainable approach in the long run. My point is that the "dumb bounds" do not in practice improve reliability of code compared to overhead and churn associated with them. Yes, they are good for diagnostics, but I think such bounds can be automatically tracked by compiler without making them explicit in code.

[oli-obk]

We can always be more permissive in the future, but I think we should treat const generics like type generics, so i do expect that you will have to write almost all the same bounds as those that you write with the typenum crate. Any modification to const generics bounds should go in hand with the same changes to type generics. There is still lots of design space in adding inferred bounds (like knowing that a const generic is smaller than a specific value, and thus being able to infer all kinds of things) that have equal things in type generics.

I do think that for the initial implementation we should focus on shipping a feature in a way that we already know works in practice instead of going for the full shebang in one go. Like with all complex features, if we go with the full thing, we'll just end up splitting it into a min_* feature before stabilization, so there's no loss if we go with the min_* feature from the start and design and develop the "unknown territories" under a separate feature.

[sighoya]

@oli-obk wrote:

pub struct GostCfb<C, const M: u8>
where
   C: BlockCipher + NewBlockCipher,
   // C::BlockSize: IsLessOrEqual<U255>,
   // above bound not needed anymore, using correct type (u8) now
   // M: Unsigned + ArrayLength<u8> + IsGreaterOrEqual<C::BlockSize> + Sub<C::BlockSize>,
   // above bound not needed anymore
   // * M >= C::BlockSize are covered by subtraction not hitting overflow check below
   // * Sub is covered by subtraction below
   // * ArrayLength is covered by cast below
   // Diff<M, C::BlockSize>: ArrayLength<u8>,
   (M as usize - C::BlockSize), // above bound translated to proposal 2
{
   cipher: C,
   block: Block<C>,
   tail: [u8; {M as usize - C::BlockSize}], // note: moved away from GenericArray
   pos: u8,
   s: u8,
}

Can you explain why it works?

You said nothing have to be proved but what is the case for overloading and specialization?
Regarding semantic (expressed by HOL), it requires equality and ordering to determine the more specialized trait method. But equality and ordering is undecidable in general.
Would it instead be more preferable to dispatch trait methods propositionally instead of semantically like in D.
The latter would treat where x<4, x<3 more specialized than where x<3 even they share the same semantic.

The other way around, can we always assume that the relation < follows transitivity, anti-symmetry and anti-reflexivity in every case, what is if < is overloaded?
Did the user need to prove these properties?
Can we expect the user to read proofs?

[oli-obk]

Can you explain why it works?

We compare the MIR (or to be precise, a datastructure that is created by processing MIR) of the array length and check if an equal constant exists in the where bounds.

You said nothing have to be proved but what is the case for overloading and specialization?

well, equality has to be proven, but that's similar to how you have to prove two variables have the same type in order to be able to assign one variable to the other.

I'm not sure what you mean with overloading and specialization. Rust doesn't actually have overloading. Specialization of functions with such bounds I have not thought about yet, but we can also punt on that question until it becomes a problem (and start out by requiring all bounds on all specializations to be equal and then think about relaxing that).

Regarding semantic (expressed by HOL), it requires equality and ordering to determine the more specialized trait method. But equality and ordering is undecidable in general.

I'm afraid I have no idea what you are talking about. Can you break it down into examples? I also don't know what HOL is and what you mean by semantic.

Would it instead be more preferable to dispatch trait methods propositionally instead of semantically like in D.

Is this a question? I don't know how D does it or how trait dispatch relates to this issue

The latter would treat where x<4, x<3 more specialized than where x<3 even they share the same semantic.

Sure, such bounds are extensions we can think about in the future, but I still believe starting out with the minimal feature (that mirrors what typenum does) is the best way forward. We don't have to worry about any higher effects on the type system, since for everything we're implementing there already exists a type level equivalent.

The other way around, can we always assume that the relation < follows transitivity, anti-symmetry and anti-reflexivity in every case, what is if < is overloaded?
Did the user need to prove these properties?
Can we expect the user to read proofs?

We cannot assume anything about the PartialEq impl unless it's one in core/std. So trusting such an impl for these bounds is likely not possible. On the other hand, this feels a lot like range patterns in pattern matching, where we also don't allow anything but plain integers for which we know their behaviour, so maybe what we want instead is where bounds on ranges instead of on comparisons? This way we can unify any such logic with the pattern matching logic.

cc @lcnr I think we should create a tracking issue that just tracks const_evaluatable_unchecked (so the constants-must-be-equal minimal version of this issue, in order to separate concerns and discussions of that with the more advanced features talked about here)

[lcnr]

cc @lcnr I think we should create a tracking issue that just tracks const_evaluatable_unchecked (so the constants-must-be-equal minimal version of this issue, in order to separate concerns and discussions of that with the more advanced features talked about here)

const_evaluatable_unchecked is the future compat lint for [0; std::mem::size_of::<*mut T>()] being allowed on stable, do you mean a tracking issue for const_evaluatable_checked which is #76560? I personally am not too interested in discussions about how to extend that feature until we get it far enough to be usable and are able to point to examples of actual pain points.

[oli-obk]

const_evaluatable_checked

yea I meant that. Thanks. I didn't realize I was entering unchecked in the search box when I was looking for checked. Ok, so we can close this issue.

For extensions beyond exact matching constants (proposal 2), please open issues on the RFC repository or even better, discussions in the internals forums.

[sighoya]

@oli-obk wrote:

We compare the MIR (or to be precise, a datastructure that is created by processing MIR) of the array length and check if an equal constant exists in the where bounds.

Okay, I may formulated my question a bit too imprecise. Why you can leave out all commented constraints in proposal 2 over proposal 1 or 3, I'm a bit out of look here.

For those who are interested, I've formulated my concerns above in Future Direction: Const Generics and Dispatching

[oli-obk]

You can leave out all the bounds, because you are enforcing that the constant mentioned must compile successfully, and the caller of that function must prove that either by bubbling the constraint to its callers or by inserting enough concrete values and types to make the expression evaluable.

[sighoya]

But that's not the answer to my question because how does the caller know which constraint have to be bubbled up (uppropagated?) when you left out some necessary constraints in your example.
I don't see the case that you proved C::BlockSize: IsLessOrEqual<U255> or could we infer that implicitly from tail: [u8; {M as usize - C::BlockSize}]

[oli-obk]

from C::BlockSize being of type u8 we can infer that all its values must be in the range 0..=255.

The other bounds are M: IsGreaterOrEqual<C::BlockSize> and M: Sub<C::BlockSize>, which are actually the same thing, since unsigned subtraction requires that no overflow happens. So just the fact that there's a subtraction here adds that requirement.

But that's not the answer to my question because how does the caller know which constraint have to be bubbled up (uppropagated?)

The constraint is that M as usize - C::BlockSize compiles successfully. The way to bubble that up is to add the where [(); M as usize - C::BlockSize] bound to the caller's signature. This is no different from bubbling up a T: Add. You either specify a concrete T like i32 which satisfies the bound, or you bubble up the T: Add.

[sighoya]

@oli-obk, thanks for clarification.

[JAicewizard]

I am still not able to use associated consts in, for example, array sizes. Are there any plans to implement this?

(I have enabled #![feature(const_generics, const_evaluatable_checked)] as suggested by rustc)