Idea: Static assertions

language design
1

Idea

(Apologies in advance for the hand-wavy-ness)

Introduce the compile-time assertions based on supported const eval.

For example,

const BUF_SIZE: usize = 500;
const MAX_BUF_SIZE: usize = 1000;

static_assert(BUF_SIZE <= MAX_BUF_SIZE) // static assert
static_assert(10000000 < MAX_BUF_SIZE) // compile error: assertion failed...

Inside the static_assert can be any const expression of type bool that is accepted by the compiler.

Motivation

Often, it can be helpful to assert the truthiness of some invariants about constants at compile time. That is, if the assertion is false, the program fails to compile. This is already a well-known and commonly-used technique in the C/C++ world, where it is often used to avoid buffer overflows on staticly-defined buffers.

This proposal suggests that static asserts may significantly improve safety and correctness of programs. Moreover, when const generics are implemented, this provides a powerful way of placing constraints on them. For example:

fn foo<const N: usize, const M: usize>(buf: [u8; N]) -> [u64; M] {
    static_assert(N == M * 8);
    ...
}

Prior Art

  • Perhaps a bit of a stretch, but C++ concepts (http://en.cppreference.com/w/cpp/language/constraints) seem similar in usage, but I am not sure if they are compile-time enforced.

  • Languages with full dependent types can do this in the type system.

  • C/C++ libraries often have a static assert of some sort.

9 Likes
2

Do want! I definitely made use of it in C++11, though where clauses will make it slightly less applicable in Rust. Maybe a macro, with an optional message afterwards?

More prior art: https://crates.io/crates/static_assertions

3

There was an idea not long ago (IDK about status) for compile-time panics (having the compiler display panics in const-context as hard compilation errors) hand have static assertions implemented using them.

edit: can’t find it rn

edit 2: found irc logs:

https://botbot.me/mozilla/rust-internals/2018-02-23/?tz=America%2FLos_Angeles&page=1

4

I like it, though from consistency viewpoint I’d expect static_assert to be a macro like debug_assert!.

5

One of the issues is that static asserts in generic contexts can't be checked until monomorphisation time. Extending the example from the first post

// crate_1
fn foo<const N: usize, const M: usize>(buf: [u8; N]) -> [u64; M] {
    static_assert(N == M * 8);
    ...
}

// crate_2
fn bar<T>(t: T) {
    let foo: [u64; 5] = crate_1::foo([0; 2])
    ...
}

// crate_3
fn baz() {
    bar(());
}

Would it be possible to receive an error when compiling crate_2 since it's guaranteed to happen, or would it only be crate_3 that would actually cause the error to be emitted.

I agree with what I think @scottmcm was referring to, that extending where clauses to support something like const boolean predicates would subsume most usage of this though, e.g.

fn foo<const N: usize, const M: usize>(buf: [u8; N]) -> [u64; M]
    where (N == M * 8)

// and the one I really want
fn foo<T>(t: T) where (mem::size_of<T>() == 0)

Whether or not that ever happens I think there would still be some places where simple static assertions would be useful, so I'm in favour of getting a simple macro into the standard library.

I agree

1 Like
6

I think a valuable goal is the possibility of declaring all of the contract outside of the fn body:

fn foo<const N: usize, const M: usize>() -> usize
  where predicate(N, M) {
    ...
}

Even for run-time values:

fn foo(n: usize, m: usize) -> usize
  where predicate(n, m) {
    ...
}

If the predicate of some run-time values cannot be determined at compile time then a run-time assertion would have to be generated by the compiler. However, if the predicate can be proved at compile time then the run-time check is unnecessary and is eliminated.

3 Likes
7

Yes, nice! And this could eventually lead to supporting something like this: [Pre-RFC] Another take at clarifying `unsafe` semantics - #31 by gbutler

8

In the PLT literature this is called (proof) erasure. In the talk "Type inference needs a revolution" Conor McBride talks about that and Milner's coincidence. More: http://staff.computing.dundee.ac.uk/frantisekfarka/tiap/#conor. There's also a paper on erasure in Idris, which tries to erase proofs quite agressively, that might interest you: Practical Erasure in Dependently Typed Languages.

We can reinterpret (for the purposes of understanding the mechanics, not how you write it down syntactically):

fn foo(n: usize, m: usize) -> usize
where predicate(n, m) {
    ...
}

as the following:

fn foo<proof: predicate(n, m) == true>(n: usize, m: usize) -> usize {
    ...
}

In other words, there is a sort of implicit argument of type predicate(n, m) == true where == is the type constructor for propositional equality which is inhabited if and only if a and b are the same type. The compiler will try to construct a proof of this fact for you automatically when you try to call foo(x, y). In many ways, this is similar to what the compiler does for traits and their implementations.

I should note however that this is not an easy problem, and significant thinking / research will be needed to make this happen proficiently. But if it can be done well in Rust, it would be quite wonderful. It should also be noted that unlike Idris, Agda, etc. which are based on Intuitionistic logic, Rust is not. The affine nature (or to simplify a lot: linear nature) of Rust's type system makes it difficult for dependent types. Neel Krishnaswami talks about this in a lecture series on Linear and Dependent types and McBride talks about it in a talk about "Worldly type systems + Linear dependent types".

In Idris, we can encode foo by writing:

// Propositional equality, poly kinded:
data (=) : a -> b -> Type where
   Refl : x = x

foo : {auto proof : Predicate(n, m) = True}
   -> (n : Nat) -> (m : Nat) -> Nat
foo n m = the_body_of_foo

The thing inside { .. } is an implicit argument, which means that if the compiler can infer it from the surrounding context, we don't have to specify it. For example take:

data Vec : (len : Nat) -> (elem : Type) -> Type where
  Nil  : Vec Z elem
  (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem

// which is really:

data Vec : (len : Nat) -> (elem : Type) -> Type where
  Nil  : {elem : Type} -> Vec Z elem
  (::) : {elem : Type} -> {len : Nat}
      -> (x : elem) -> (xs : Vec len elem) -> Vec (S len) elem

// Adding two vectors together, we know their lengths from the vectors themselves, so they can be implicit:

add : {n : Nat} -> {m : Nat} -> Vec n Color -> Vec m Color -> Vec (n + m) Color
add vec_a vec_b = ...

// or just:

add : Vec n Color -> Vec m Color -> Vec (n + m) Color
add vec_a vec_b = ...

The auto keyword will tell Idris to try and construct the proof for us automatically.

3 Likes
9

How about calling it const_assert? It’s for const expressions after all.

7 Likes
10

So, would it make sense to add the ability to syntactically add pre/post predicates to function/method declarations and then the compiler would insert them as asserts before/after the call to the function (with a compiler option to elide them in Release mode if desired)? Then, the compiler could gradually grow to support more and more ability to statically verify the pre/post predicates and automatically elide them when it can? Meanwhile, people can start adding pre/post predicates to their functions with the knowledge that they will become run-time assertions that eventually may be elided by the compiler should its ability to statically solve the predicates grows to support their particular predicates.

1 Like
11

I believe this is very similar to the proposed C++20 contracts do. Note that this is not the same as a static assert which is evaluated at compile time and has no runtime effects.

Generally, thanks for the feedback all!

I definitely agree with the sentiment of using where or something similar for checking const generic values, but I thought I would throw the idea of using static assert for that out there.

Do people feel there would be enough support for an RFC for const_assert!($const_bool_expr, "message") at the item level only without anything that would require monomorphization?

12

I do feel this is needed. Sometimes I just want some kind of sanity that will block code compilation, not necessarily as part of an API.

13

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.