Datatypes well-formedness checks may be overly conservative

[y1ca1]

Issue 1: Verus might not be checking datatypes transitively:

Ok:

enum Foo {
    V1(u8),
    V2(Bar),
}

struct Bar(u8, Box<Foo>, u8);

Err:

enum Either<A, B> {
    Left(A),
    Right(B),
}
struct Foo(Either<u8, Bar>);

struct Bar(u8, Box<Foo>, u8);

Verus reports:

error: datatype must have at least one non-recursive variant
  --> /playground/src/main.rs:21:1
   |
21 | struct Bar(u8, Box<Foo>, u8);
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Similarly, if Vec is wrapped Verus fails to see the well-formed datatype definition:
Ok:

struct Foo(Either<u8, Bar>);

struct Bar(u8, Vec<Foo>, u8);

Err:

struct VecWrapper<T>(Vec<T>);

struct Foo(Either<u8, Bar>);

struct Bar(u8, VecWrapper<Foo>, u8);

Issue 2: Verus might be overly conservative:

Consider a sensible use case of mutually recursive functions (modeling "lazy datatypes"):

ghost struct LazyFoo(u8, spec_fn() -> LazyBar);
ghost struct LazyBar(u8, spec_fn() -> LazyFoo);

spec fn lazy_foo() -> LazyFoo {
    LazyFoo(0, || lazy_bar())
}

spec fn lazy_bar() -> LazyBar {
    LazyBar(0, || lazy_foo())
}

Verus gives:

error: datatype must have at least one non-recursive variant
  --> /playground/src/main.rs:24:1
   |
24 | struct LazyBar(u8, spec_fn() -> LazyFoo);
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Such pattern can perfectly occur in exec code (though not directly due to the lack of function pointers in Verus, but possible with custom traits).

---

Relevant comments from Travis a while back: From #1360: .

[y1ca1]

Repro link.

[utaal]

@y1ca1 is it correct that both issues are not soundness issues, in particular: in the first case we're only rejecting cases that we could be allowing?

[y1ca1]

@y1ca1 is it correct that both issues are not soundness issues, in particular: in the first case we're only rejecting cases that we could be allowing?

Correct. It's more like completeness issues.