#[invariant]?

language design
1

I suggest a new tag, #[invariant] that can be put on types to assert any invariant called for by the type.

#[invariant(condition)] // This condition will be `assert`ed every time a function taking mutable references of the struct is called.
struct InvariantType;

This will provide users with strict enforcement of invariants to ensure that at any time a function is called, the invariant will be upheld. Something similar to:

invarianted_variable.modify();
// assert(invariant) automatically called

Perhaps this could be made const? I'd love to hear feedback!

1 Like
2

D has a similar feature where a type can have an invariant {} block in its definition. Every method then runs through the block to ensure it is valid. Not sure if it depends on configuration or not.

Anyways, RFC-like things really benefit from the RFC template so everyone has a better idea of what is actually being proposed. For example, what is the inv name and where else does it appear? Is it user-controlled? A method? Can it be private? And so on.

1 Like
3

Sorry, I didn't make it clear that this is a very nebulous idea. Also, the inv is just a generic name for a condition. Edited my post to make it clear.

Having a look at the documentation, it seems that this is very clear prior art. This could theoretically be restructured, but I believe for our purposes the #[invariant] tag is better syntax due to how Rust is structured.

Additionally bringing to note that Ada and Eiffel have similar features of invariants. contracts - Rust also brings in similar features to the table. This is also one of Rust's project goals.

4

It seems like it would be possible to implement this as a proc-macro on impl blocks. The biggest downside to that approach being duplication on trait impls and not being able to derive.

5

I was thinking more like putting it in struct, enum, and typedef definitions. That way, we can have types with additional invariants be defined as typedefs and we would put the proc macro right at the source.

There is a crate that does this but with rust's project goals, I suggest implementing it natively as a better option.

I would prefer it be implemented like D - with the invariants being checked at the constructor and every function calling a mutable reference to the type.

6

I don't understand how this attribute would encode an arbitrary invariant.

E.g.

#[invariant]
struct MyVec<T> {
    ptr: *mut T,
    size: usize,
    capacity: usize,
}

How does the compiler know, that I, the programmer want the invariants, that

  1. ptr always points to contiguous memory of size items of type T.
  2. size <= capacity.

How could this be const-asserted if the struct's content, i.e. size, allocated memory, etc. can change during runtime?

1 Like
7

Sorry, I made a mistake.

What I meant was more like D's invariant blocks, which track data at runtime.

8

I fail to see how this is better than just private fields with a constructor that enforces the invariant

struct NonEmptyVec<T>(
    /// # Invariant: Must not be empty
    Vec<T>,
);

impl<T> NonEmptyVec<T> {
    fn new(t: T) -> Self {
        unsafe { Self::from_vec_unchecked(vec![t]) }
    }
    unsafe fn from_vec_unchecked(vec: Vec<T>) -> Self {
        Self(vec)
    }
    fn first(&self) -> &T {
        self.0.first().unwrap_or_else(|| unsafe { hint::unreachable_unchecked() }) 
    }
    fn from_vec(vec: Vec<T>) -> Option<Self> {
        if vec.is_empty() {
            None
        } else {
            Some(unsafe { Self::from_vec_unchecked(vect) })
        }
    }
}

This way you only pay the validation cost once

9

In D, at least, the invariant block is automatically called at the end of every method (could probably be limited to methods which accept &mut, but interior mutability also exists…). As I said above, that may depend on build configuration; I don't think I've ever done non-debug builds in D (while developing).

1 Like
10

So meant for ensuring that your implementation upholds and invariant you have decided? I'd think its very uncommon for a type to be complicated enough that your implementation would benefit from automatic invariant checks, while also having an invariant that can be checked trivialy. (I at least cannot come up with an example that would benefit enough from this)

11

It seems extremely difficult to impossible to implement consistently in general.

For instance, let's say you want to put an invariant check on a String that says the bytes are a valid UTF-8 encoding. Now somebody does:

let bytes = unsafe { s.as_bytes_mut() };

Does the invariant get checked when the reference gets dropped, which could happen far away in the program or even in some other crate?

12

No. It would be checked whenever the reference is used or mutated.

13

My main intention was to focus on issues like this.

struct Term {
    // ...
}

#[invariant(self.degree == 1 || self.degree == 0)]
type LinearTerm = Term;

where you wouldn't get the chance to add the additional methods.

14

Is there a reason this would need to be a language builtin/in the stdlib? The contract crate seems just fine to me. I don't think it lets you annotate a type and have it checked everywhere, but you could define an is_valid method and ensures it everywhere you need. In fact, that method seems better, since:

  • It allows internal methods to operate on values that don't uphold the invariant
  • It allows the same level of validation on free functions as methods
  • It avoids checking and rechecking the invariants of the same data (.len() probably doesn't need to check every time that it's greater than .cap())
15

Note that type does not really define a new type (to which you can attach invariants) but instead it's simply an alias for an existing one. Making this work as you expect would likely require reworking some existing assumptions.

3 Likes
16

I think a way to specify custom invariants on a type would be most useful if it's assert_unchecked whenever using the type (combined with automatically inserted asserts that ensure that the inserted assert_uncheckeds can't possilby fail – unfortunately I'm not clear on the details of how this would work, especially with respect to how it interacts with unsafe code).

The advantage of this is that, in addition to catching coding mistakes in which the invariant is broken, it also improves performance because the compiler can assume the invariants rather than rechecking them every time.

1 Like
17

How confident are you in this invariant?

Because to me when I see it, I think of the contracts work where you run an SMT solver to prove that the invariant holds, not that you'd repeatedly assert it all over the place.

(Especially since, to me, the most important invariants are the ones you can't assert.)

3 Likes
18

Instead of an attribute, wouldn't it make more sense to make this a trait?

impl Invariant for InvariantType {
    fn invariant(&self) {
        assert!(some_condition_on(self.foo, self.bar));
    }
}
1 Like
19

How would this be implemented? It seems totally infeasible, because every reference to anything (e.g. &mut u8) would need to carry with it at runtime some information about invariants to verify on every access.

1 Like
20

Would it need to be runtime information? Didn't we manage to get rid of the explicit drop flag logic with smarter compilation? Why not do the same with inserting calls to the invariant verifier? Usage of &T where T: Freeze could also elide such calls.