Panic with raw pointer operations in default trait method

[hayley-leblanc]

Hi all,

The following trait (minimized from the original code):

trait Serializable : Sized {
    fn serialized_len() -> (out: u64);
    
    #[verifier::external_body]
    fn as_bytes(&self) 
    {
        let ptr = self as *const Self as *const u8;
        let slice = unsafe {
            std::slice::from_raw_parts(ptr, Self::serialized_len() as usize)
        };
    }
}

Triggers the following panic:

thread 'rustc' panicked at rust_verify/src/lifetime_generate.rs:1574:38:
no entry found for key

The initial version of the code had as_bytes with a postcondition involving some other Serializable methods and returning a slice; I thought one or both of those things might be related to the panic, but it still occurs in the code shown above with the postcondition and return value removed.

The same error does not occur in a non-default implementation or in a regular function.

The code that triggers the panic can also be found here https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=e96b6ad0f673da4557efbba97d07a01b. I've also included a commented-out version of the same trait that does not have a default as_bytes implementation + an implementation that do not trigger the panic.