Imposing pre-condition when implementing traits?

[nokunish]

When implementing traits for different structs, is there a way to impose pre/post-conditions? For instance, if I want to have a peek function,

pub trait OptionExt {
    fn peek(&self) -> usize;
}

and want to change the implementations for different structs, i.e)

*Option::is_some() marked as pure in extern_spec*

impl OptionExt for Option<usize> 
{   
    #[requires(self.is_some())]
    fn peek(&self) -> usize {
        match self {
            Some(t) => *t,
            None => unreachable!(),
        }
    }
}

struct S1(usize);
impl OptionExt for Option<S1> 
{       
    #[requires(self.is_some())]
    fn peek(&self) -> usize {
        match self {
            Some(t) => (*t).0,
            None => unreachable!(),
        }
    }
}

imposing the pre-conditions produce the error message: [E0407] method `prusti_pre_item_peek_12b6ae9173184c988f5f37adfc66f4a9` is not a member of trait `OptionExt` [Note] not a member of trait `OptionExt` Although I could have peek functions that takes in a reference to the struct objects instead, is there a way to verify the program when implementing traits?

[Aurel300]

Using specifications within trait impl blocks requires that you annotate the impl block with #[refine_trait_spec]. This is not yet documented, but will be.