Error: use of undeclared lifetime name

[clemsys]

Hi all,

I am currently trying to use Verus to verify Linux Rust kernel modules. When running Verus on the following (minimal) code

use kernel::{error::Result, prelude::*, types::ForeignOwnable, ThisModule};
use vstd::prelude::*;

verus! {
    #[verifier(external_body)]
    #[verifier::reject_recursive_types(T)]
    pub struct MyXArray<T: ForeignOwnable>(Vec<T>);

    fn foo(tree: MyXArray<Box<u8>>) {}
}

I get the following error (the 2 errors reported are exactly the same):

error: use of undeclared lifetime name `'a33_a`
  --> drivers/block/rnull.rs:28:39
   |
28 | pub struct MyXArray<T: ForeignOwnable>(Vec<T>);
   |                                       ^

error: aborting due to 2 previous errors

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

I tried to understand what's going on. When printing the content of the variable rust_code from the function checked_tracked_lifetimes in rust_verify/src/lifetime.rs, I get the following:

// ...

impl<A1_T, > T30_ForeignOwnable for Box<A1_T, > where A1_T: 'static,  {
    type A29_Borrowed = &'a33_a A1_T;
    type A32_BorrowedMut = &'a33_a  mut A1_T;
}

// ...

It thus makes sense that the rustc borrow checker complains about the undeclared lifetime 'a33_a. However, the above code generated by verus seems wrong to me because the original code contains lifetime annotations for type Borrowed<'a> and type BorrowdMut<'a>:

// Code from types.rs

pub trait ForeignOwnable: Sized {
    /// Type used to immutably borrow a value that is currently foreign-owned.
    type Borrowed<'a>;

    /// Type used to mutably borrow a value that is currently foreign-owned.
    type BorrowedMut<'a>;

    // ...
}

// ...

impl<T: 'static> ForeignOwnable for Box<T> {
    type Borrowed<'a> = &'a T;
    type BorrowedMut<'a> = &'a mut T;

    // ...
}

I am not sure if this is a bug in Verus or if I am missing something. Could you please help me understand what's going on? Thanks in advance!

[tjhance]

Yes it looks like a Verus bug. The generated code ought to have the declaration for 'a33_a same as the original code has the declaration for 'a.

[clemsys]

Thanks, that's good to know ! I've put everything in one file and made it even more minimal to make it easier for you to reproduce the bug:

use vstd::prelude::*;

pub trait Borrowable {
    type Borrowed<'a>;
}

impl Borrowable for u8 {
    type Borrowed<'a> = &'a u8;
}

verus! {
    #[verifier(reject_recursive_types(T))]
    pub struct Container<T: Borrowable>(T);
}

Here is the error message:

error: use of undeclared lifetime name `'a27_a`
  --> src/main.rs:13:40
   |
13 |     pub struct Container<T: Borrowable>(T);
   |                                        ^

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

And here is the corresponding content of the variable rust_code from the function checked_tracked_lifetimes in rust_verify/src/lifetime.rs:

// ...

trait T25_Borrowable {
    type A24_Borrowed;
}

struct D23_Container<A1_T, >(
    A1_T,
) where A1_T: T25_Borrowable, ;

impl T25_Borrowable for u8 {
    type A24_Borrowed = &'a27_a u8;
}

I also tried to add a lifetime to the trait to see if it would solve the problem but it just gave me a new error:

use std::marker::PhantomData;
use vstd::prelude::*;

pub trait Borrowable<'a> {
    type Borrowed: 'a;
}

impl<'a> Borrowable<'a> for u8 {
    type Borrowed = &'a u8;
}

verus! {
    #[verifier(reject_recursive_types(T))]
    pub struct Container<'a, T: Borrowable<'a>>(T, PhantomData<&'a T>);
}

Here is the error:

error: missing lifetime specifier
  --> src/main.rs:14:48
   |
14 |     pub struct Container<'a, T: Borrowable<'a>>(T, PhantomData<&'a T>);
   |                                                ^

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

And here is the corresponding content of the variable rust_code from the function checked_tracked_lifetimes in rust_verify/src/lifetime.rs:

// ...

trait T27_Borrowable<'a23_a, > {
    type A26_Borrowed : 'a23_a;
}

struct D25_Container<'a23_a, A1_T, >(
    A1_T,
    D24_PhantomData<&'a23_a A1_T, >,
) where A1_T: T27_Borrowable, A1_T: 'a23_a, ;

struct D24_PhantomData<A1_T, >(
    PhantomData<A1_T>,
);
impl<A1_T, > Clone for D24_PhantomData<A1_T, > { fn clone(&self) -> Self { panic!() } }
impl<A1_T, > Copy for D24_PhantomData<A1_T, > {}

impl<'a23_a, > T27_Borrowable<'a23_a, > for u8 {
    type A26_Borrowed = &'a23_a u8;
}

[clemsys]

Finally, when I put everything inside the verus! block, verus tells me that generics on associated types are not yet supported so they might as well be unsupported when the trait and the corresponding impl are written outside the verus! block.

use vstd::prelude::*;

verus! {
    pub trait Borrowable {
        type Borrowed<'a>;
    }

    impl Borrowable for u8 {
        type Borrowed<'a> = &'a u8;
    }

    #[verifier(reject_recursive_types(T))]
    pub struct Container<T: Borrowable>(T);
}

Error:

error: The verifier does not yet support the following Rust feature: unsupported generics on associated type
  --> src/main.rs:8:5
   |
8  | /     impl Borrowable for u8 {
9  | |         type Borrowed<'a> = &'a u8;
10 | |     }
   | |_____^

error: aborting due to 1 previous error