Static preconditions

[leonardo]

Like D language ( https://dlang.org/spec/contracts.html ) and Ada2012 ( https://en.wikibooks.org/wiki/Ada_Programming/Contract_Based_Programming ) C++20 could add contract-based features: https://herbsutter.com/2018/07/02/trip-report-summer-iso-c-standards-meeting-rapperswil/

In Rust there are some crates that allow some contract-based programming, like: https://crates.io/crates/adhesion

I’ve used contracts often in D language and while I like them, I think they don’t add that much compared to just putting some asserts at the top and end of functions, and calling private invariant() methods of structs/classes, so I think D contracts don’t change significantly the way you write and debug D code (I have not used contracts in C++ yet, I will probably try them later).

(What I think could change the way we think about Rust code is optional full-compile-time (or proof-time) verification of contracts, as in Why3 language: http://why3.lri.fr/ Take a look at its gallery for many nice examples that show both the power and problems of this: http://toccata.lri.fr/gallery/why3.en.html See also this for few examples with explanations: https://hal.inria.fr/hal-00967132/en/ But such stuff is complex and I leave it to future discussions).

So at the moment I am not asking to add regular built-in contract-based features in Rust as the ones of C++20. But there is a smaller related feature that I think could be useful in Rust, and I think it’s future-compatible with both C++20-style contracts and Why3-style proofs.

I can call it Static Preconditions, it’s similar to function pre-conditions used in contract-based programming. It’s a part of function signature (and its code from other crates is handled by the compiler like generics). It’s a pre-condition that runs only when the arguments of a function are statically known (or they are results of const functions), and it runs at compile-time. If later Rust adds C++20-style contracts, static preconditions run before the dynamic pre-conditions (and Why3-style proofs use all kinds of pre-conditions).

Currently code like:

fn main() {
    let a = [10, 20];
    println!("{}", a[2]);
}

Gives:

error: index out of bounds: the len is 2 but the index is 2
 --> test.rs:3:20
  |
3 |     println!("{}", a[2]);
  |                    ^^^^
  |
  = note: #[deny(const_err)] on by default

But equivalent user-defined code doesn’t give that compile-time error:

use std::ops::Index;
struct Foo([u32; 2]);

impl Index<usize> for Foo {
    type Output = u32;

    fn index(&self, i: usize) -> &Self::Output {
        &self.0[i]
    }
}
fn main() {
    let a = Foo([10, 20]);
    println!("{}", a[2]);
}

Static preconditions allow user code to generate that compile-time error (syntax is provisory):

fn index(&self, i: usize) -> &Self::Output {
    const_requires(i < self.0.len(), "Index out of bounds");
    &self.0[i]
}

A purpose of static preconditions is to catch at compile-time some mistakes in Rust code that get caught later in unit testing and when some code is run.

Edit 1: I was forgetting that this feature is also related to the “Static_Predicate” of Ada2012:

http://www.ada-auth.org/standards/12rat/html/Rat12-2-5.html

And the __builtin_constant_p() of GCC:

http://gcc.gnu.org/onlinedocs/gcc/Other-Builtins.html

[Nemo157]

One way to experiment with this outside of the compiler is via custom attributes. You could have something like

#[contract(requires(i < self.0.len(), "Index out of bounds"))]
fn index(&self, i: usize) -> &Self::Output {
    &self.0[i]
}

contract could be a custom proc-macro which would expand to a normal assertion in the body of the function (or maybe a wrapper #[inline(always)] function to push the assertion into the caller could be more optimisable)

fn index(&self, i: usize) -> &Self::Output {
    assert!(i < self.0.len(), "Index out of bounds");
    &self.0[i]
}

Then you could have a custom compiler driver (like clippy) which looks for and registers contract attributes during expansion and emits lints if it can statically verify the contract is violated.

---

This is basically how I remember C#'s code contracts working, but it’s been many years since I’ve looked at them.

[mark-i-m]

Related:

Idea: Static assertions

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 …

Compile time assert

Yes, I know about this trick, there is also static_assertions crate that provides nice wrapper around this or similar trick. But it would be great to have it inside std or compiler.

Quick Thought: const{} blocks

Looking at async fn+async{} and unsafe fn+unsafe{} made me think, what about const{}? As an example, (function-level) static_assert!(N == M) could just be const { assert_eq!(N, M) } (Ref Idea: Static assertions & RFC #2345 Allow panicking in constants) I could also imagine something like match x { 0..N => ..., N..const{2*N} => ..., _ => ... }. You could think of this as const { A } => (const || { A })(), like with async – not that const closures exist today.