Panic with opaque associated function

[hayley-leblanc]

I have an associated spec function I'd like to make opaque but I'm having trouble doing so. I initially tried something like this:

trait Foo {
    #[verifier::opaque]
    spec fn do_something() -> nat;
}

because I want all implementations to be opaque, but this results in the following error: error: opaque has no effect on a function without a body, so I assume this is not meant to be supported.

However, making an implementation opaque and then revealing it, e.g.,

impl Foo for u64 {
    #[verifier::opaque]
    spec fn do_something() -> nat { 0 }
}

fn test() {
    reveal(u64::do_something);
}

results in a panic:

thread 'rustc' panicked at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/compiler/rustc_hir/src/def.rs:645:45:
attempted .def_id() on invalid res: PrimTy(Uint(U64))

Some minimal code that reproduces this is at this playground link: https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=ef04f2b2e7422abceec947cc93bea554 which uses version 2024.07.15 6e30b8a