I'm using verusdoc to generate documentation for our verification project. However, the verusdoc does not support the display of the ensures and requiresfor verus_spec.

Here is an example:

The method BoxRef::deref_target is

    /// Dereferences `self` to get a reference to `T` with the lifetime `'a`.
    #[verus_spec(ret => ensures *ret == self.value())]
    pub fn deref_target(&self) -> &'a T {

and the documentation only shows

impl<'a, T> BoxRef<'a, T>
  pub exec fn deref_target(&self) -> &'a T
    Dereferences self to get a reference to T with the lifetime 'a.

The ensures *ret == self.value() specification is not shown anywhere in the generated docs.

https://asterinas.github.io/vostd/ostd/sync/non_null/struct.BoxRef.html#method.deref_target