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

@eddyb

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.

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

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}]:.

@Evrey

@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)

Implement Condemned for (A, B)

@memoryruins

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.

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

@oli-obk

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

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.

@oli-obk

@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?

@lcnr

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.

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.

@oli-obk

@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

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.

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}]

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.

@oli-obk

@oli-obk, thanks for clarification.

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)

Navigation Menu

Repository navigation

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

51 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

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

Description

Activity

eddyb commented on Feb 3, 2020

Evrey commented on Feb 14, 2020

oli-obk commented on May 31, 2020

51 remaining items

beepster4096 commented on Oct 17, 2020

oli-obk commented on Oct 20, 2020

newpavlov commented on Oct 20, 2020

oli-obk commented on Oct 20, 2020

sighoya commented on Oct 27, 2020

oli-obk commented on Oct 27, 2020

lcnr commented on Oct 27, 2020

oli-obk commented on Oct 27, 2020

sighoya commented on Oct 27, 2020

oli-obk commented on Oct 27, 2020

sighoya commented on Oct 27, 2020

oli-obk commented on Oct 27, 2020

sighoya commented on Oct 29, 2020

JAicewizard commented on Aug 4, 2021

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions