Verus panicked at rust_verify/src/lifetime_generate.rs:1757:21

[y1ca1]

Tried my best to get this (un)minimized repro. (See the comment below for a cleaner repro)

use vstd::prelude::*;
verus! {

pub trait Foo {
    type T<'a>;
}

pub trait From<T> {

}

pub trait Mapper<S: From<Self::U>> {
    type U: From<S>;
}

pub struct MapFoo<F, M>(F, M);

impl<F, M> Foo for MapFoo<F, M> where
    F: Foo,
    for <'a>M: Mapper<F::T<'a>>,
    for <'a>F::T<'a>: From<<M as Mapper<F::T<'a>>>::U>,
    for <'a><M as Mapper<F::T<'a>>>::U: From<F::T<'a>>,
 {
    type T<'a> = <M as Mapper<F::T<'a>>>::U; // panic
    // type T<'a> = F::T<'a>; // also panic 
}

fn main();

} // verus!

Verus outputs:

❯ RUST_BACKTRACE=1 verus foo.rs
thread 'rustc' panicked at rust_verify/src/lifetime_generate.rs:1757:21:
assertion failed: bound_vars.is_empty()
stack backtrace:
   0: _rust_begin_unwind
   1: core::panicking::panic_fmt
   2: core::panicking::panic
   3: rust_verify::lifetime_generate::erase_mir_generics
   4: rust_verify::lifetime_generate::erase_impl_assocs
   5: rust_verify::lifetime_generate::State::reach_datatype
   6: rust_verify::lifetime_generate::gen_check_tracked_lifetimes
   7: rust_verify::lifetime::check_tracked_lifetimes
   8: rustc_middle::ty::context::GlobalCtxt::enter
   9: <rust_verify::verifier::VerifierCallbacksEraseMacro as rustc_driver_impl::Callbacks>::after_expansion
  10: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#0}::{closure#0}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_span::ErrorGuar
anteed>>
  11: rustc_span::create_session_globals_then::<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_interface::interface::run_compiler<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_driver
_impl::run_compiler::{closure#0}>::{closure#0}>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

Tested with Verus: ❯ verus --version Verus Version: 0.2024.06.10.c7f9cd5 Profile: release Platform: macos_aarch64 Toolchain: 1.76.0-aarch64-apple-darwin

❯ verus --version
Verus
  Version: 0.2024.06.10.6fa6786
  Profile: release
  Platform: macos_aarch64
  Toolchain: 1.76.0-aarch64-apple-darwin

[y1ca1]

Ok, this is a much cleaner repro:

use vstd::prelude::*;

verus! {

pub trait Bar {
    type U<'a>;

}

pub trait Foo<S> where
    S: for<'a> Bar<U<'a> = Self::T<'a>>,
 {
    type T<'a>;
}

fn main();
} // verus!

[Chris-Hawblitzel]

Can you try the lifetime-for branch?

[y1ca1]

Thanks for the fix! I tried the branch and found some other issues:

The original code now verifies:

use vstd::prelude::*;

verus! {

pub trait Bar {
    type U<'a>;

}

pub trait Foo<S> where
    S: for<'a> Bar<U<'a> = Self::T<'a>>,
 {
    type T<'a>;
}

fn main();
} // verus!

---

❯ verus foo.rs
verification results:: 1 verified, 0 errors

But if we add an associated function to the trait Foo that refers to the associated type, some peculiar error messages show up:

use vstd::prelude::*;

verus! {

pub trait Bar {
    type U<'a>;

}

pub trait Foo<S>
    where
        S: for<'a> Bar<U<'a> = Self::T<'a>>,
 {
    type T<'a>;

    fn foo<'a>(&self, s: &'a [u8]) -> (res: Result<Self::T<'a>, ()>); // errs Verus
    // fn foo_<'a>(&self, o: Self::T<'a>); // also errs
}

fn main();
} // verus!

---

❯ verus foo.rs
error: lifetime name `'a29_a` shadows a lifetime name that is already in scope
  --> foo.rs:17:12
   |
17 |     fn foo<'a>(&self, s: &'a [u8]) -> (res: Result<Self::T<'a>, ()>);
   |            ^^^^^^
18 |     // fn foo_<'a>(&self, o: Self::T<'a>);
   |                           ^^^^^^

error: lifetime name `'a29_a` shadows a lifetime name that is already in scope
  --> foo.rs:17:12
   |
17 |       fn foo<'a>(&self, s: &'a [u8]) -> (res: Result<Self::T<'a>, ()>);
   |              ^^^^^^
...
22 |   fn main();
   |  _________^
23 | | } // verus!
   | |___^

error: trait takes 0 lifetime arguments but 1 lifetime argument was supplied
 --> foo.rs:23:7
  |
1 | | use vstd::prelude::*;
  | |_
...
23|   } // verus!
  |  _______^

error: missing generics for associated type `T25_Bar::A24_U`
 --> <crate attribute>:1:10
  |
1 | allow(internal_features)
  |          ^^^^^

error: trait takes 0 lifetime arguments but 1 lifetime argument was supplied

error: missing generics for associated type `T25_Bar::A24_U`

error: binding for associated type `A24_U` references lifetime `'a29_a`, which does not appear in the trait input types

error: aborting due to 7 previous errors

note: This error was found in Verus pass: ownership checking of tracked code

error: aborting due to 8 previous errors

P.S. The code type-checks in Rust.

[Chris-Hawblitzel]

Can you try now?

[y1ca1]

Thanks again for the fix! However, I found another peculiar error reported and likely a bug:

use vstd::prelude::*;

verus! {

trait Bar<S>: View {
    type T;
}

trait Foo {
    type U<'a>;
}

struct S<F>(F);

impl<F> View for S<F> where F: Foo, for <'a>F::U<'a>: View {
    type V = S<F>;

    spec fn view(&self) -> Self::V;
}

fn main();

} // verus!

---

❯ verus src/main.rs
error: use of undeclared lifetime name `'b38_a`
  --> /Users/yicai/Research/with-B.P./repos/verus/source/vstd/seq.rs:31:18
   |
31 | pub struct Seq<A> {
   |                  ^

error: aborting due to 1 previous error

note: This error was found in Verus pass: ownership checking of tracked code

error: aborting due to 2 previous errors

However, when removing the seemingly unrelated code (the trait Bar):

use vstd::prelude::*;

verus! {

trait Foo {
    type U<'a>;
}

struct S<F>(F);

impl<F> View for S<F> where F: Foo, for <'a>F::U<'a>: View {
    type V = S<F>;

    spec fn view(&self) -> Self::V;
}

fn main();

} // verus!

Or using a custom View trait for the unrelated code:

trait MyView {
    type V;

    spec fn view(&self) -> Self::V;
}

trait Bar<S>: MyView {
    type T;
}
...

---

❯ verus src/main.rs
verification results:: 1 verified, 0 errors

Or replacing the impl View with a blank impl:

use vstd::prelude::*;

verus! {

trait Bar<S>: View {
    type T;
}

trait Foo {
    type U<'a>;
}

struct S<F>(F);

impl<F> S<F> where F: Foo, for <'a>F::U<'a>: View {

}

fn main();

} // verus!

---

❯ verus src/main.rs
verification results:: 1 verified, 0 errors

Maybe something to do with the vstd View trait?

[Chris-Hawblitzel]

Can you try again now?

[y1ca1]

Thanks! Here is a new bug:

use vstd::prelude::*;

verus! {

trait TT {
    type A<'a>;

    fn f<'a>(s: Self::A<'a>);
}

struct Foo<M>(M);

impl<M> Foo<M> where
    for<'a> M: TT<A<'a> = &'a [u8]>,
{
    fn foo<'a>(&self, s: &'a [u8])
    {
        M::f(s)
    }
}

fn main();
} // verus!

---

❯ verus src/main.rs
error: mismatched types
  --> src/main.rs:18:14
   |
18 |         M::f(s)
   |              ^

error: aborting due to 1 previous error

note: This error was found in Verus pass: ownership checking of tracked code

error: aborting due to 2 previous errors

The above code type-checks in Rust.

Plus FWIW, changing the function to spec makes Verus panic:

use vstd::prelude::*;

verus! {

trait TT {
    type A<'a>;

    spec fn f<'a>(s: Self::A<'a>);
}

struct Foo<M>(M);

impl<M> Foo<M> where
    for<'a> M: TT<A<'a> = &'a [u8]>,
{
    spec fn foo<'a>(&self, s: &'a [u8])
    {
        M::f(s)
    }
}

fn main();
} // verus!

---

❯ verus src/main.rs
thread '<unnamed>' panicked at rust_verify/src/verifier.rs:522:17:
internal error: ill-typed AIR code: error 'error 'in equality, left expression has type tuple%0. and right expression has different type Poly' in expression '(= (main!impl&%0.foo.? M&. M& self! s!) (main!TT.f.? M&. M& s!))'' in ex
pression '(=>
 (fuel_bool fuel%main!impl&%0.foo.)
 (forall ((M&. Dcr) (M& Type) (self! Poly) (s! Poly)) (!
   (= (main!impl&%0.foo.? M&. M& self! s!) (main!TT.f.? M&. M& s!))
   :pattern ((main!impl&%0.foo.? M&. M& self! s!))
   :qid internal_main!impl&__0.foo.?_definition
   :skolemid skolem_internal_main!impl&__0.foo.?_definition
)))'
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread '<unnamed>' panicked at rust_verify/src/verifier.rs:1949:29:
worker thread panicked

Finally, a proof fn is good:

use vstd::prelude::*;

verus! {

trait TT {
    type A<'a>;

    proof fn f<'a>(s: Self::A<'a>);
}

struct Foo<M>(M);

impl<M> Foo<M> where
    for<'a> M: TT<A<'a> = &'a [u8]>,
{
    proof fn foo<'a>(&self, s: &'a [u8])
    {
        M::f(s)
    }
}

fn main();
} // verus!

---

❯ verus src/main.rs
verification results:: 2 verified, 0 errors

[Chris-Hawblitzel]

I put the spec fn foo issue in https://github.com/verus-lang/verus/issues/1108 . The other issue should be fixed. Can you try it now?

[y1ca1]

Thanks! I played with it and found another interesting bug:

use vstd::prelude::*;
verus!{
trait Foo
{
    type R<'a>;
    fn foo<'a>(&self, s: &'a [u8]) -> Self::R<'a>;
}

trait Bar<Other>
where
    Self: Foo,
    Other: Foo,
{
    fn bar(&self, other: &Other);
}

impl<U1, U2, V1, V2> Bar<Pair<U2, V2>> for Pair<U1, V1>
where
    U1: Foo,
    U2: for<'a> Foo<R<'a> = ()>,
    V1: Foo,
    V2: Foo,
{
    fn bar(&self, c: &Pair<U2, V2>) {
    }
}

struct Pair<S, T>(S, T);

impl<S, T> Foo for Pair<S, T>
where
    S: Foo,
    T: Foo,
{
    type R<'a> = T::R<'a>;
    fn foo<'a>(&self, s: &'a [u8]) -> Self::R<'a> {
        self.1.foo(s)
    }
}

}
fn main() {}

---

❯ verus src/main.rs
error: mismatched types
  --> src/main.rs:37:39
   |
37 |     fn foo<'a>(&self, s: &'a [u8]) -> Self::R<'a> {
   |                                       ^^^^^^^^^^^
38 |         self.1.foo(s)
   |                ^^^^^^

error: aborting due to 1 previous error

note: This error was found in Verus pass: ownership checking of tracked code

error: aborting due to 2 previous errors

The type error disappears If we move struct Pair<S, T>(S, T); above impl Bar for Pair:

...
struct Pair<S, T>(S, T);

impl<U1, U2, V1, V2> Bar<Pair<U2, V2>> for Pair<U1, V1>
where
    U1: Foo,
    U2: for<'a> Foo<R<'a> = ()>,
    V1: Foo,
    V2: Foo,
{
    fn bar(&self, c: &Pair<U2, V2>) {
    }
}
...

---

❯ verus src/main.rs
verification results:: 2 verified, 0 errors

[Chris-Hawblitzel]

Ok, try now.

[y1ca1]

Ok, try now.

Thanks! Will try it when I get a chance.

[y1ca1]

All works!!

Thanks to the series of fixes, I migrated our codebase from using trait generic lifetime (trait Trait<'a>) to the more expressive and fine-grained generic associated type (GAT). Can't thank you enough!