That is the way contracts /should/ work, IMHO, but not the way that they
/do/ work. Having had Tony Hoare as the head of department during my
university education, it is a great disappointment to me that C++
contracts look like Hoare logic pre-conditions and post-conditions, but
are actually more like glorified assert macros.
(I am aware that opinions differ, and the folks behind C++ contracts -
specifications and implementations - are smart, experienced developers
who have thought long and hard about this all. This is disappointment
and frustration with what I think this feature could have been, from my
own viewpoint of how I personally want to write code. Maybe what I want
would not be possible or practical in the very wide context of general
C++ development.)
To me, the obvious point of declaring "foo" to have pre() and post()
blocks is that the caller of "foo" should have optional checks that
"pre" holds, the implementation of "foo" should be written and optimised
with the assumption that "pre" holds, the implementation of "foo" should
have optional checks that "post" holds, and the caller of "foo" should
be written and optimised with the assumption that "post" holds.
C++ contracts get a lot of this wrong. Checking is done in the function
definition, which is the wrong place for pre-conditions - if a
pre-condition does not hold, the problem lies in the caller, not the
callee. (Of course the callee can optionally check too, as part of
fault-finding and debugging, or at API boundaries where the caller is
not trusted.)
C++26 contracts do not get this wrong. It is implementation defined which evaluation semantics can be selected, which of the options is actually used at runtime, and where the checks happen. The only thing the standard says is that if the evaluation semantic says it checks the contract, that the program execution is equal to as-if the program checks it every time, potentially multiple times per function entry. That allows it to check it zero times, if the compiler is sufficiently convinced the contract holds in all possible cases.
Specifically, your compiler can implement the pre-checks on caller side, and the post-checks on callee side, and if it knows that these are always run with a terminating semantic use that information in optimizing. Current compilers do not implement an ABI that exposes this, and there are known issues with having such an ABI, but there's nothing in their specification that precludes it.
The specific ABI problems are that if you have a function with contracts, that the simple "have an entrypoint past the check with a @post-check tag" breaks if the contracts seen by the caller and callee aren't necessarily the same. Technically an ODR violation, but practically a major issue, since one side then doesn't check contract A but the other side assumes contract B. A possible solution could be seen in the direction of encoding the full contract into the ABI, but that breaks down as soon as you have opaque functions, and is very complicated in case of lambdas. In environments where this ODR violation isn't a runtime issue, like those where both halves are always rebuilt if changed, this problem does not exist and such an ABI gives you exactly what you ask for.
And despite having written out these conditions, and
checked them, the compiler still can't rely on them being true for
optimisation purposes - you have to write [[assume]] again.
Only if you configure the compiler to not enforce the contracts. And if you tell it not to enforce it you're now forcing UB back in.
Having the
pre-condition checks in the wrong place also means that you can't use
"enforce" semantics while testing and debugging a translation unit or
module before switching to "ignored" for code that you are sure is
correct - control of contract evaluation semantics is also in the wrong
place.
I'm not convinced ignore is a semantic people should use for much if anything at all ever. It should be a once-in-ten-thousand kind of semantic, to be used when you have a discovered-to-be-broken contract in a build that you cannot rebuild for some other reason. Similarly, observe should be rarely used, and only if you need to check a contract is fine in an environment where a mistake in a new check that passed all unit tests can still not be trusted enough.
At best, C++ contracts are a replacement for "assert" macros on API
boundary functions - IMHO they have missed the opportunity for being a
general tool towards safer and more efficient coding.
Having a convenient way to "assume" that contracts hold would definitely
be useful. I am not sure what the best syntax would be (or to be more
honest, I haven't a clue about the best syntax), but what I would like
to see is a way to do:
1. In the function's declaration, say that the caller must check the
pre-condition.
2. In the function's declaration, say that the caller can assume the
post-condition holds when optimising.
3. Let the function implementation assume the pre-condition holds. This
could be either as a general "it always holds" indication, but might be
better as a "assume pre-conditions hold at this point in the function
implementation". That could allow certain specific checks before the
assumption.
You get 1, 2 and 3 by telling your compiler to only allow enforce or quick-enforce. The default in the compilers I've used that support contracts is enforce, so that gives them the rights to do this already. It's not implemented that way because nobody has picked it up so far.
4. Let callers and callees override or dictate the contract enforcement
semantics, and do so separately for pre and post conditions.
As of yet implementation specified, and in almost all cases you want it to be enforce anyway, especially as the compiler can then use that to optimize. But if you do want that, then look at P3400 and see if that provides the handles you want for configuration.
WRT OP's question, you are basically asking for an `assume` semantic that does not check the pre- and post-conditions, and that just assumes they'll hold. This has been discussed numerous times already; if you can search the archives please do so. In practice, I find that enforce and quick_enforce basically do what assume would do, except without the gap around "I checked this and had a mistake, so now my software is hackable anyway". I'd rather spend the time to improve the compiler's ability to eliminate contracts that it finds always-true, than giving users a footgun tool to attempt the same. That said, there are some places where users can indeed prove something true, but the compiler cannot (in reasonable time), and for those an assume semantic would be good.
If you're motivated to do so, write the paper to add the assume semantic and defend that we should indeed have this footgun. There's precedent already in [[assume]], [[likely]] and [[unlikely]], which can be used correctly but by far most users wouldn't.