How do I enforce an invariant on a struct?

[finegeometer]

Suppose I have this code:

#[derive(Copy, Clone)]
struct Vector(i32, i32);

impl Vector {
    fn neg(self) -> Self {
        Self(-self.0, -self.1)
    }
}

I would like to specify that v : Vector is valid iff neither v.0 nor v.1 are i32::MIN. That way, the overflow checks will pass.

How do I do this?

---

If this is possible, the syntax should be documented somewhere. I can't find it, after several hours of searching. If it is not possible, then that fact should be documented somewhere. I automatically assumed that it would be possible, so I wasted several hours searching.

---

~There is a workaround~:

use prusti_contracts::*;

#[derive(Copy, Clone)]
struct Vector(i32, i32);

impl Vector {
    #[pure]
    fn valid(self) -> bool {
        self.0 != i32::MIN && self.1 != i32::MIN
    }

    #[requires(self.valid())]
    #[ensures(self.valid())]
    fn neg(self) -> Self {
        Self(-self.0, -self.1)
    }
}

~But this workaround would fail if neg was in an impl std::ops::Neg for Vector.~

Edit: I just noticed that Prusti is giving me an error when I attempt this workaround. But VSCode won't tell me the error message, and I haven't installed the command-line version of Prusti.

[fpoli]

Thanks for the report! With the workaround it seems that you hit a Prusti bug which originates from the following line:

https://github.com/viperproject/prusti-dev/blob/e85739dadbcce2fbee46f8a2f0f904d7c819a618/prusti-viper/src/encoder/type_encoder.rs#L152

@cmatheja have you already seen this? I'll at least replace that panic with an internal error message.

Regarding the difference between the command-line version of Prusti and VSCode, can it be that in VSCode you are using the "latest release" build channel and not "latest dev"? See https://github.com/viperproject/prusti-assistant#configuration.

[Aurel300]

Thanks for the report.

The feature you are looking for, type invariants, is something we used to support in Prusti. The syntax would be #[invariant(...)] attached to the struct. However, this was broken (by the recent compiler upgrade I think), and the user guide was written after, so it is not documented. We plan on adding this back.

Your program has one syntax error i32.MIN should be i32::MIN.

Other than that, this fails when trying to create a snapshot of the type … But I see @fpoli has just replied and tagged Christoph already :) Anyway, the snapshot encoding should be supported for this for sure, since it only contains i32 fields.

[finegeometer]

Thank you!

Your program has one syntax error: i32.MIN should be i32::MIN.

Not surprising, I retyped the program rather than copy-pasting. (I don't remember why.) So typos were likely.

Regarding the difference between the command-line version of Prusti and VSCode, can it be that in VSCode you are using the "latest release" build channel and not "latest dev"? See https://github.com/viperproject/prusti-assistant#configuration.

No, I have "prusti-assistant.buildChannel": "Nightly".

When I say "VSCode won't tell me the error message", here is what I mean:

• VSCode reports one error.
• That error is: Prusti encountered an error. See other reported errors and the log (View -> Output -> Prusti Assistant ...) for more details.
• The log is empty, except for a report of the command it ran...

Wait a minute. That means I can try it on the command line!

Ok, I get this:

thread 'rustc' panicked at 'internal error: entered unreachable code', prusti-viper/src/encoder/type_encoder.rs:124:21
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

error: internal compiler error: unexpected panic

Which is a different unreachable!() than the one @fpoli pointed to.

[Aurel300]

Which is a different unreachable!() than the one @fpoli pointed to.

It is a different line, but unfortunately the unreachable!() is reached for the same reason, which is the failure to encode a snapshot.

[fpoli]

The panic should be fixed by #322.

[Pointerbender]

type invariants, is something we used to support in Prusti. The syntax would be #[invariant(...)] attached to the struct. However, this was broken (by the recent compiler upgrade I think), and the user guide was written after, so it is not documented. We plan on adding this back.

This sounds really useful. Is there an expected timeline for when struct invariants will be added back to Prusti? Alternatively, is there a work-around currently available on the nightly build? Thanks!

[vakaras]

type invariants, is something we used to support in Prusti. The syntax would be #[invariant(...)] attached to the struct. However, this was broken (by the recent compiler upgrade I think), and the user guide was written after, so it is not documented. We plan on adding this back.

This sounds really useful. Is there an expected timeline for when struct invariants will be added back to Prusti?

@zgrannan?

Alternatively, is there a work-around currently available on the nightly build? Thanks!

The workaround with self.valid() should work on the current nightly.

[zgrannan]

I'm not quite sure when the invariants will be ready; although I have a WIP PR here: https://github.com/viperproject/prusti-dev/pull/686.

There is still one failing test, and also I know that it doesn't work well when a struct invariant exists as part of an enum type. Also I suspect it does not work well with generics.

[nokunish]

Hi, I've also been having troubles with the type-invariant flags.

If #[invariant(..)] is the only flag, Prusti doesn't seem to recognize it.

#[invariant(self.0 < 100)]  
pub struct ID(usize);

impl ID {
    fn duplicate(&self) -> &Self {
        self.clone()
    }
}

(this produces:

[Prusti: unsupported feature] Type invariants need to be enabled with the feature flag `enable_type_invariants.)

However, when there are other flags that are imposed on the same struct,

#[invariant(self.id < 100)]    
#[derive(Clone)] 
pub struct Item<T>
    where T: Clone
{
    id: usize,
    val: T 
}

impl<T> Item<T> 
    where T: Clone
{
    fn duplicate(&self) -> Self {
        self.clone()
    }
}

it then seems to ignore the other flags (i.e. we get the error message: [E0277] the trait bound `T: std::clone::Clone` is not satisfied. [Note] the trait `std::clone::Clone` is not implemented for `T` instead)