Limitation in Annotating Function Contracts for Pointers to dyn Trait

[xsxszab]

Description
While this issue is not a direct bug in Kani, it impacts the usability of Kani in scenarios involving pointers to dyn Trait. Specifically, in challenge 3 of the verify-rust-std repository, we encountered this issue while verifying function contracts for <dyn Trait> pointee types.
Consider the following example:

trait TestTrait {}
struct TestStruct {value: i64,}
impl TestTrait for TestStruct {}

let test_struct = TestStruct { value: 42 };
let trait_object: &dyn TestTrait = &test_struct;
let test_ptr: *const dyn TestTrait = trait_object;
unsafe {test_ptr.byte_offset(2);}

This code runs successfully and calls the byte_offset method on a pointer to dyn TestTrait. However, when trying to annotate this method using the #[kani::proof_for_contract] attribute, as shown below:

#[kani::proof_for_contract(<*const dyn TestTrait>::byte_offset)]

The following compilation error occurs:

Failed to resolve `<*const dyn TestTrait>::byte_offset` for `proof_for_contract`: Expected a type, but found trait object paths `dyn TestTrait`

Analysis
The issue appears to stem from a limitation in Rust, where attributes can only accept constant expressions and cannot handle dynamic dispatch. Since dyn Trait involves dynamic dispatch, Rust cannot resolve it in the attribute's context.
To work around this, we have adopted the following approach:

• Instead of annotating the method with pointers to dyn Trait, we annotate it with its concrete base type:

#[kani::proof_for_contract(<*const TestStruct>::byte_offset)]

While this workaround works, it diverges from the intent of verifying the contract directly for <*const dyn Trait>::byte_offset.

Questions

1. Is the described workaround of annotating with the base type acceptable from Kani's perspective?
2. Is there an alternative approach or future support planned that would enable direct annotation for pointers to dyn Trait?