Can the standard library rely on stated but unenforceable invariants of traits like TotalOrd?

[huonw]

Some traits like TotalOrd and TotalEq have invariants (like a < b || a == b || a > b for all a and b for TotalOrd). These can be stated in documentation but not enforced by the compiler or in the type system.

Some algorithms (e.g. a sort, or a data structure) may wish to rely on these stated invariants in a way that means a violation could be memory unsafe. E.g. a highly-optimised sort might run out of bounds when a comparison function is incorrect in exactly the right (well, wrong) way. Being safe in the face of incorrectness can come at the cost of efficiency by being forced to use a slower algorithm, or perform bounds checks etc.

Nominating.

[emberian]

I think this is a bit of a sticky issue, but safe code should never cause memory unsafety, ever. If relying on those assumptions would cause memory unsafety, they should be marked unsafe.

[eddyb]

As a very wild suggestion:

if prove!((a < b) ^ (a == b) ^ (a > b) forall a, b in T) {
    /* fast implementation */
} else {
    /* potentially slower implementation */
}

cc @regehr might as well toy with the idea if we have access to the tools

[regehr]

This is really interesting. I have been playing with the design of something similar to this -- an interface between optimizer and prover for Rust. I need to think on it more. Thanks for ccing me.

[brson]

P-low, not 1.0

[thestinger]

There's a simple solution to this, so I don't think it needs to be an issue. Add a default method #[inline(always)] unsafe fn is_correct() -> bool { false } and correct implementations can override it. It's even backwards compatible to do this for a trait.