An assert is just a fancy `if condition { panic(message) }`. If the optimizer can show that condition is always false, the panic is declared as dead code and eliminated. The post uses that to get the compiler to remove all panics to reduce the binary size. But you can also just check if panic code was generated (or associated code linked in), and if it was then the optimizer wasn't able to show that your assert can't happen.
Of course this doesn't prove that the assert will happen. You would have to execute the code for that. But you can treat the fact that the optimizer couldn't eliminate your assert as failure, showing that either your code violates the assert, your preconditions in combination with the code aren't enough to show that the assert isn't violated, or the whole thing was too complicated for the optimizer to figure out and you have to restructure some code
Ah, I see what you are saying. Yes, if the optimizer is able to eliminate the postcondition check, I agree that it would constitute a proof that the code upholds the invariant.
The big question is how much real-world code the optimizer would be capable of "solving" in this way.
I wonder if most algorithms would eventually be solvable if you keep breaking them down into smaller pieces. Or if some would have some step of irreducible complexity that the optimizer cannot figure out, now matter how much you break it down.
> Functions that require some amount of optimization to prove that they do not panic may no longer compile in debug mode after being marked #[no_panic].
So you’re probably going to have to protect this with a cfg_attr to only apply the no_panic in release only.
To be clear, the optimizer doesn’t uphold the post condition. It just says “the post condition is usable to elide other checks”. But if the condition itself is incorrect, the compiler will STILL elide those checks. If the compiler could prove the condition on its own it would have done so. That’s why that assert is named unchecked and is itself unsafe!
To be clear as there’s a lot of nuance. Assert unchecked is telling the compiler the condition must always hold. The optimizer and compiler don’t make any assumption about the assert. That information is then used by the compiler to optimize away checks it otherwise would have to do (eg making sure an Option is Some if you call unwrap).
If you have an assumption that gives unhelpful information, the optimizer will emit panic code. Worse, if the assumption is incorrect, then the compiler can easily miscompile the code (both in terms of UB because of an incorrectly omitted panic path AND because it can miscompile surprising deductions you didn’t think of that your assumption enables).
I would use the assume crate for this before this got standardized but very carefully in carefully profiled hotspots. Wrapping it in a safe call as in this article would have been unthinkable - the unsafe needs to live exactly where you are making the assumption, there’s no safety provided by the wrapper. Indeed I see this a lot where the safety is spuriously added at the function call boundary instead of making the safety the responsibility of the caller when your function wrapper doesn’t actually guarantee any of the safety invariants hold.
> Wrapping it in a safe call as in this article would have been unthinkable - the unsafe needs to live exactly where you are making the assumption, there’s no safety provided by the wrapper.
I want to be sure I understand your meaning. In your analysis, if the check_invariant function was marked unsafe, would the code be acceptable in your eyes?
Unsafe is the P0. I'd avoid this approach wholesale UNLESS it was a critical hot path with no other way to get safe Rust to elide the check (hint - you'd be surprised how much gets elided in idiomatic Rust). Basically, this is a nice sharp knife in the toolbox to know about and so sharp I'd rarely use it.
Of course this doesn't prove that the assert will happen. You would have to execute the code for that. But you can treat the fact that the optimizer couldn't eliminate your assert as failure, showing that either your code violates the assert, your preconditions in combination with the code aren't enough to show that the assert isn't violated, or the whole thing was too complicated for the optimizer to figure out and you have to restructure some code