Reenable datatype invariants

[zgrannan]

No description provided.

[vakaras]

@zgrannan I thought a bit about the possible implementation of type invariants and I think that the cleanest way of integrating them into the refactored system would be by renaming the new TypeDecl into TypeDeclKind and adding a new TypeDecl:

struct TypeDecl {
  kind: TypeDeclKind,
  user_invariant: Box<Expression>,
}

Let me know if you have any questions or need help.

[Aurel300]

@vakaras Is the new TypeDecl a misnomer then? If these types are meant to be passed around similarly to ty::Ty or (the old) vir::Type, they are not declarations.

[fpoli]

Why the Box? It seems unnecessary.

[vakaras]

@vakaras <https://github.com/vakaras> Is the new TypeDecl a misnomer then? If these types are meant to be passed around similarly to ty::Ty or (the old) vir::Type, they are not *declarations*.

It is a declaration. The thing passed around is `vir::high::Type`.

…

[vakaras]

Why the Box? It seems unnecessary.

Yes, mixed up code.

…

[fpoli]

Why the Box? It seems unnecessary.
Yes, mixed up code.
…

If it turns out to be needed to cut a mutual recursion with the expression definition then I prefer it over Box<TypeDecl>.

[JonasAlaif]

So I've been thinking about this a little, particularly with adding "dependent parameters" expressed as const generics. The classic use case with a Type Alias is the following:

#[invariant(_ < s.len())]
type Index<const s: &[u32]> = usize;
fn foo(s: &[i32], i: Index<{s}>) -> i32 { s[i] }

Porting this from my work on Type Aliases to Datatypes wouldn't be so difficult, and it seems to be a super nice solution to the invariants-func.rs example:

#[invariant(self.invariants_enabled ==> self.value <= 100)]
struct Percentage {
    invariants_enabled: bool,
    value: u8,
}
fn print_percentage(percentage: &Percentage) { }

#[requires(percentage.invariants_enabled)]
fn adjust_percentage(percentage: &mut Percentage) {
    percentage.value += 10; // temporarily break invariant

    percentage.invariants_enabled = false;
    print_percentage(percentage);
    percentage.invariants_enabled = true;

    percentage.value -= 10; // restore invariant
}

Would instead be:

#[invariant(invariants_enabled ==> self.value <= 100)]
struct Percentage<const invariants_enabled: bool> {
    value: u8,
}
fn print_percentage(percentage: &Percentage<{false}>) { }

fn adjust_percentage(percentage: &mut Percentage<{true}>) {
    percentage.value += 10; // temporarily break invariant

    print_percentage(percentage);

    percentage.value -= 10; // restore invariant
}

However, my current solution requires the whole thing be wrapped in a prusti!{} macro to find all of the {true} and {false} arguments and hide them from the type system - even though the current Rust const generics support bool types. So an even nicer solution would be to try to write this as 'valid' Rust:

#![feature(const_generics_defaults)]

#[invariant(invariants_enabled ==> self.value <= 100)]
struct Percentage<const invariants_enabled: bool = true> {
    value: u8,
}
fn print_percentage(percentage: &Percentage<false>) {}

fn adjust_percentage(percentage: &mut Percentage) {
    percentage.value += 10; // temporarily break invariant

    print_percentage(percentage as &Percentage<false>);

    percentage.value -= 10; // restore invariant
}

The only snag is that we cannot percentage as &Percentage<false> - I don't know const generics well enough; the only thing I could come up with is creating a new instance: &Percentage::<false> { value: percentage.value }, but that kinda defeats the purpose.

Edit: @vakaras suggested &Percentage::<false> { ..percentage } which actually seems to me as a viable option. For us to support this the invariant macro would have to not panic when processing const generics struct S<const x: bool = true> {} and Prusti would have to include support for const generics.

[zgrannan]

@vakaras
I recall a few weeks ago this was blocked because the datatype invariants encoding uses:

prusti-dev/prusti-viper/src/encoder/encoder.rs

Lines 625 to 637 in 2bce0c8

	pub fn encode_assertion(
	&self,
	assertion: &typed::Assertion<'tcx>,
	mir: &mir::Body<'tcx>,
	pre_label: Option<&str>,
	target_args: &[vir::Expr],
	target_return: Option<&vir::Expr>,
	targets_are_values: bool,
	assertion_location: Option<mir::BasicBlock>,
	error: ErrorCtxt,
	parent_def_id: ProcedureDefId,
	tymap: &SubstMap<'tcx>,
	) -> SpannedEncodingResult<vir::Expr> {

which returns a vir::Expr, but the type invariant encoder:

prusti-dev/prusti-viper/src/encoder/mir/types/encoder.rs

Line 525 in 2bce0c8

pub fn encode_invariant_def(self, invariant_name: &str) -> EncodingResult<vir::FunctionDecl> {

needs the body to be vir::Expression, and there is no way to go from polymorphic vir to high vir.

Is this still the case?

[vakaras]

Is this still the case?

Yes. And I doubt that #756 will be enough to fix that.

[Aurel300]

I rebased this. I think the last comment still kind of applies. More specifically, I see:

• mir::types::MirTypeEncoderInterface::encode_type_invariant_def_poly into which I rebased the implementation in this PR. This function returns a vir_poly function and is never used.
• high::types::HighTypeEncoderInterface::encode_type_invariant_use/def which is currently a stub. The first one is actually used from the procedure encoder. However, even though these are in high/types, they also return a String and a vir_poly::FunctionIdentifier, respectively.

So… should I just remove the encode_type_invariant_def_poly and move it into high?

[vakaras]

I rebased this. I think the last comment still kind of applies. More specifically, I see:

* `mir::types::MirTypeEncoderInterface::encode_type_invariant_def_poly` into which I rebased the implementation in this PR. This function returns a `vir_poly` function and is never used.

* `high::types::HighTypeEncoderInterface::encode_type_invariant_use/def` which is currently a stub. The first one is actually used from the procedure encoder. However, even though these are in `high/types`, they also return a `String` and a `vir_poly::FunctionIdentifier`, respectively.

So… should I just remove the encode_type_invariant_def_poly and move it into high?

Seems like that would be the easiest option.

[JonasAlaif]

It seems that after the rebase, things don't work at all atm (i.e. things behave as if there was no invariant annotation)

[Aurel300]

@JonasAlaif I do have some WIP for this locally, but I want to wait until after #899, because invariants with generics were not nice.

[Aurel300]

bors r+

(@vakaras I'll add the trusted flag shortly)

[bors]

Build succeeded:

• all-tests (macos-latest)
• all-tests (ubuntu-latest)
• all-tests (windows-latest)
• clippy-check
• fmt-check
• purification-tests
• test-crates