pub trait DerefSpec: Deref {
// Required methods
spec fn deref_spec(&self) -> &<Self as Deref>::Target;
proof fn deref_spec_eq(&self);
}Expand description
This is a workaround to add an uninterpreted specification of Deref trait, as Deref is included in Verus but does not have spec functions. It may change if Verus adds native support for spec functions in the Deref trait.
Required Methods§
Sourcespec fn deref_spec(&self) -> &<Self as Deref>::Target
spec fn deref_spec(&self) -> &<Self as Deref>::Target
Sourceproof fn deref_spec_eq(&self)
proof fn deref_spec_eq(&self)
ensures
forall |output| {
call_ensures(Self::deref, (self,), output) ==> self.deref_spec() == output
},