Default trait method implementation blocked by no_method_body()

[marshtompsxd]

Hi Verus team,

I am trying to implement some traits with default method implementation like

pub trait MyTrait {
    open spec fn get_key(&self) -> ObjectKey {
        ......
    }
}

However, Verus reports that

error: trait method declaration body must end with call to no_method_body()
  --> src/spec/kubernetes_core_resources.rs:22:15
   |
22 |     open spec fn get_key(&self) -> ObjectKey {
   |               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: aborting due to previous error

And it seems that I cannot have any statements before/after no_method_body().

I am wondering is there a way to have default trait implementation for spec/exec function in Verus now?

[utaal]

This is currently unsupported, I believe; spec functions in trait definitions are only intended to be defined by implementers. Can you share more of what you're trying to accomplish? There may be another formulation that works and that we support.

/cc @Chris-Hawblitzel

[utaal]

This is still currently unsupported, but we now emit a sensible error message. Closing, as this is probably on the roadmap at some point.