Equality

[utaal]

Recording the conclusion of offline discussion with @Chris-Hawblitzel:

• SpecEq implies Eq and means that == is smt equal in a spec context;
• Structural implies Eq and means that exec == is smt equal, Structural also implies SpecEq. Structural is restricted to types with only exec fields.
• SpecEq is auto-derived (a-la Send) for #[spec] and #[proof] types, and can be manually derived for #[exec] type as long as the type doesn’t implement Eq (because of the coherence rules, we’re guaranteed that the Eq implementation, if any, is in the same compilation unit as the type).

[utaal]

We don't have a separate SpecEq trait for this. The verus! macro turns == into smt equality in spec contexts.