How to write spec for new type implementing Add?

[TheodoreEhrenborg]

Minimal example:

use vstd::prelude::*;

verus! {

pub struct Foo(u64);

impl core::ops::Add for Foo {
    type Output = Foo;

    fn add(self, other: Foo) -> Foo {
        assume(self.0 + other.0 < 1000); // To hide overflow error
        Foo(self.0 + other.0)
    }
}

fn main() {
}

} // verus!

Error message:

[rust_verify/src/verifier.rs:100:17] &note = "failed this postcondition"
[rust_verify/src/verifier.rs:100:17] &sp.as_string = "vstd/std_specs/ops.rs:70:25: 70:66 (#2446)"
error: postcondition not satisfied

verification results:: 1 verified, 1 errors
error: aborting due to 1 previous error

Version:

╰─>$ verus --version
Verus
  Version: 0.2025.10.05.bf8e97e
  Profile: release
  Platform: linux_x86_64
  Toolchain: 1.88.0-x86_64-unknown-linux-gnu

[parno]

Unfortunately, this isn't well documented at the moment. I dug into the tests to find a comparable example. That suggests something along these lines, which works on when I test it locally:

pub struct Foo(pub u64);

impl vstd::std_specs::ops::AddSpecImpl<Foo> for Foo {
     // Does the implementation of this trait obey basic addition principles
    open spec fn obeys_add_spec() -> bool {
        true
    }
   // Pre-condition of add
    open spec fn add_req(self, rhs: Foo) -> bool {
        self.0 + rhs.0 < 1000 // To prevent overflow 
    }
    // Postcondition of add
    open spec fn add_spec(self, rhs: Foo) -> Foo {
        Foo((self.0 + rhs.0) as u64)
    }
}

impl core::ops::Add for Foo {
    type Output = Foo;

    fn add(self, other: Foo) -> Foo {
        Foo(self.0 + other.0)
    }
}

[TheodoreEhrenborg]

Thanks, this is really helpful. I've tried this in our codebase and it works 🎉 . Two questions:

• The pre/post-conditions go in impl vstd::std_specs::ops::AddSpecImpl<Foo>, and not impl core::ops::Add?
• What happens if obeys_add_spec is false?

[parno]

Great, I'm glad it's working in your codebase! In answer to your questions:

1. Yes, that's correct. Because Add is an existing trait that's defined in another crate, we define additional spec functions in a new trait (AddSpec), and then for additional complicated reasons, have an associated name (AddSpecImpl) that you use to give your definitions for those spec functions. If you're interested in more details, here's the original discussion, and the more updated discussion in the PR that added support for external trait extensions.
2. I don't think there would ever be a need to explicitly set obeys_add_spec. This is an encoding "trick" we use when writing specs for external traits. Because there are many existing (unverified) implementations of the trait, we don't actually know if all of them behave sensibly (i.e., obey the various properties we expect). For example, someone might implement Eq in a way that isn't transitive. So when we add postconditions to trait functions, they all have the form ensures obeys_foo() ==> nice_property. If Verus doesn't know that obeys_foo() is true, then it won't give you any of the nice properties. You can set obeys_foo() to be true when you implement the trait in verified code (which then obliges you to prove that the nice properties hold), or you can add an explicit assumption that obeys_foo() is true for a particular unverified implementation of the trait, but that at least means that you're making a conscious decision to take the risk that the implementation might be buggy.

[TheodoreEhrenborg]

Does anything bad happen if obeys_mul_spec is false? We've done that here because proving a constructive spec expression for the output of mul is difficult, and we instead just put a nonconstructive ensures statement on mul

[parno]

Does anything bad happen if obeys_mul_spec is false?

It means you're not obliged to prove whatever generic ensures clause the Mul trait specifies; i.e., Verus won't tell you if you got something wrong there, nor will the caller be able to assume it. If your manually added ensures clause is sufficient for your purposes, however, that's probably okay.