Trusted pervasive (vstd) types should be `: Structural`

[marshtompsxd]

Hi verus team, I was trying to check the equality of two structs that contain Option like this:

#[allow(unused_imports)]
use builtin_macros::*;
#[allow(unused_imports)]
use builtin::{ensures};

mod pervasive;
#[allow(unused_imports)]
use pervasive::{*, option::Option, map::*};

impl std::cmp::PartialEq for Option<u32> {
    #[verifier(external)]
    fn eq(&self, other: &Self) -> bool {
        match (self, other) {
            (Option::Some(a), Option::Some(b)) => a == b,
            (Option::None, Option::None) => true,
            _ => false,
        }
    }
}

impl std::cmp::Eq for Option<u32> {}

#[derive(Structural, PartialEq, Eq)]
pub struct MyStructA {
    pub content: Option<u32>,
}

fn MyFun() {
    let s1 = MyStructA{content:Option::Some(1)};
    let s2 = MyStructA{content:Option::Some(1)};
    assert(s1 == s2);
}

fn main() { }

However, verus reports the error:

error[E0277]: the trait bound `pervasive::option::Option<u32>: builtin::Structural` is not satisfied
   --> rust_verify/example/myexample.rs:23:10
    |
23  | #[derive(Structural, PartialEq, Eq)]
    |          ^^^^^^^^^^ the trait `builtin::Structural` is not implemented for `pervasive::option::Option<u32>`
    |
note: required by a bound in `builtin::AssertParamIsStructural`
   --> /Users/xudongs/verus/source/builtin/src/lib.rs:328:39
    |
328 | pub struct AssertParamIsStructural<T: Structural + ?Sized> {
    |                                       ^^^^^^^^^^ required by this bound in `builtin::AssertParamIsStructural`
    = note: this error originates in the derive macro `Structural` (in Nightly builds, run with -Z macro-backtrace for more info)

error: aborting due to previous error

For more information about this error, try `rustc --explain E0277`.
verification results:: verified: 0 errors: 0

My understanding about the equality check is:

1. [derive(Structural)] is necessary for the struct we want to check equality for

2. if the struct has #[derive(Structural)], every field in this struct has to have #[derive(Structural)] as well

If both 1 and 2 are true, what would be the best way to check the equality of a struct that contains Option fields?

[marshtompsxd]

I changed assert(s1 == s2); to assert(equal(s1, s2)); and it works.

Just curious, what is the difference between == and equal in the context of proof code?

[tjhance]

equal is guaranteed to always be "equality at the level of the SMT encoding"

== is just the usual Rust == operator, which may or may not have the above property. If it does have that property (called Structural), then == is allowed in proof/spec code, where it thereby means the same thing as equal.

I'm not sure why Option isn't already marked Structural - I think it probably could be without any issues. @utaal is that right?

[utaal]

[Triaged at the Verus all-hands.] This should not matter for spec code anymore, as it already becomes SpecEq.

Consider other names: SmtEq, LogicalEq, SolverEq.

It should be implemented as a #[verifier(external)] impl for Option, Result, etc.