I’d like to be able to optionally enable expensive pre-/postcondition checks in std.
I define “expensive” as tests that change the algorithmic complexity of the operations. It is hard to know whether a precondition check might do this because most of the algorithms do not have a bound on their complexity, but we can often guess when this happens.
Example: slice.binary_search requires the input slice to be sorted, otherwise the result is unspecified. The complexity of the binary_search method is not guaranteed by the standard library, but we can expect it to be O(log N). However, to verify the precondition, we would need to check whether the slice is sorted making the algorithm O(N). Because we change the complexity from O(log N) to O(N), this test is expensive. It also makes binary_searchO(N) kind of pointless, so we cannot enable it on debug builds by default. Still, being able to verify these preconditions in some builds can still be useful.
So… I would like to be able to enable these kind of tests on std. A strawman proposal could be to:
add a expensive_assert! macro to std
allow users to configure std with different features (and make easy to compile different versions of std and use them via cargo)
add expensive_assert!(input_slice.is_sorted()) to binary_search
Note: currently std doesn’t have any algorithms to check whether a sequence is sorted, but there is an issue for that.
/// Do a thing.
///
/// With expensive assertions turned on, does O(n) validation.
// FIXME that's weird, the scaling for expensive asserts
// actually looks more quadratic? _/o\_
fn algo_a(n: u32) {
exensive_assert!(/* test of cost O(n) */);
// run crate_b::algo_b sqrt(n) times
}
in crate_b...
fn algo_b(n: u32) {
exensive_assert!(/* test of cost O(n) */);
// run crate_c::algo_c sqrt(n) times
}
in crate_c...
fn algo_c(n: u32) {
exensive_assert!(/* test of cost O(n) */);
// do a thing sqrt(n) times
}
In the specific case of binary search one could opportunistically verify that lower bound <= upper bound at each step. So while that would increase cost it wouldn’t be a log n -> n blowup.
99% of algorithms in std do not offer any complexity guarantees what so ever, so currently, reasoning about the complexity of any algorithm combination in Rust is an act of faith
we can just document that if an user enables the expensive_asserts feature in std, all complexity guarantees are off. I don’t think it is worth it to document the complexity guarantees of the algorithms when this feature is on, because that limits us in which checks we are able to add, which might result in having to add another very_expensive_assert! flag in the future (or having to rank the expensive_assert!(A_BIT_EXPENSIVE/REALLY_EXPENSIVE/..., condition) ).
nobody is proposing this to be enabled by default neither in debug nor in release, it would be a separate feature flag that one would need to
@the8472 Checks that do not blow up the complexity of an algorithm can be probably added as debug_assert!s without much discussion (as long as they aren’t extremely expensive). That check would probably fit that. But here I am talking only about checks that do not fit this description.
Having said this, the check you propose is “better than nothing”, but it does not guarantee that the precondition is satisfied, and hence the output can still be unspecified.
Sure, but “better than nothing” is already an improvement on what we have today with the tools we have today and with much smaller impact than what is proposed here.
I think a better usecase would be in order. Where do you see this being useful? I think nobody is going to run their software with those checks enabled by default. Especially if such kind of checks get littered throughout the standard library and you might end up with some inadvertent quadratic blowups.
Or to put it a different way, shouldn’t we first try to pluck low-hanging fruits by seeing if we can add cheap but non-exhaustive preconditions before we add expensive ones?
Sure, but “better than nothing” is already an improvement on what we have today with the tools we have today and with much smaller impact than what is proposed here.
The check that you propose adds close to zero value (it doesn't guarantee anything at all), while having a cost, that is, it would need to be a debug_assert! check, which means that users would need to deal with two versions of the standard library and all their dependencies, one compiled with debug_assert! and one without.
Once we are there we might just offer a fortified build with checks that actually address the problems that they were supposed to solve.
I think nobody is going to run their software with those checks enabled by default. [...] Where do you see this being useful?
I'll run them in all my debug builds by default during development to catch logic errors early.
Especially if such kind of checks get littered throughout the standard library and you might end up with some inadvertent quadratic blowups.
I don't care about worse algorithmic complexity in debug builds as long as doing so adds some value. If the checks are very expensive, like this one, I would like to be able to opt into them, but that's about it. Also, given the current state of the complexity guarantees of the standard library algorithms, it would seem that many don't care about this on release either.
I’m not sure if I really like exaustive testing. Assuming every function in std has pre/post-condition checks, not only the run time in debug build would be worse, but also the compilation time (this is bad because debug builds are supposed to be fast) since the line count would probably be increased by a non negligible factor. On the other hand, it would be interesting to design a set of attributes that would integrate with a code proving tool (eg Why3). This approach would probably mesh up quite well with other ambitious Rust projects like Miri and RustBelt.
I think language support for contracts (or similar) would go a long way in what you propose. With contracts we don’t need to do the expensive checks in standard if the user can prove that they are satisfied (e.g. by pushing the is_sorted trait to user code, where the user can hoist it out of a loop, and as long as it doesn’t mutate the slice, doing binary_search inside the loop can be proven to satisfy the precondition.