Hi Jonathan,

On Sat, Feb 28, 2026 at 2:05 AM Jonathan Grant <jg_at_[hidden]> wrote:

> Hello Peter
> Many thanks for your time looking into this, my notes below.
>
> On 22/02/2026 22:20, Peter Bindels wrote:
> > If I can raise a different angle to your proposal...
> >
> > Suppose we have C++26 contracts. We'll assume the compiler is always
> using the enforce semantic, and compiles code to always expect all
> contracts to use the enforce semantic. The compiler is allowed to eliminate
> contract checks if it can show they can never be reached (under regular
> as-if rule). Given a function with a contract that has preconditions that
> make all subsequent calls have only redundant contract checks, it could
> eliminate all of those checks under as-if rule (since the function couldn't
> have been entered in those cases). That means that if your code ends up
> having no unprovable contract checks, it will end up without any
> relocations to the contract violation handler. You could link to a standard
> library that does not have such a handler, making any such unproven -
> not-eliminated - contract check a link-time failure.
> >
>
> That sounds good, yes, as-if rule optimization will likely remove all
> validated checks as they don't generate any code. So won't need a contract
> violation handler as you say to link to.
>
> The a few ways to stop a single compile I am aware of that can work for
> compile_assert:
> * compiler error attribute
> * emit invalid asm("oops");
> * refer to a symbol which is missing so linker fails.
>
> Yes, my understanding is that the compiler will likely optimize out
> redundant later checks of the same thing if the control flow is clear.
>
May I clarify, I didn't think any C++26 contract implementation has hard
> compiler_assert style enforce semantics? My understanding is that they are
> runtime checks like assert()?
>

They are metadata on a function boundary, also called ghost data. One
typical use of them is to convert them into runtime checks on a function
boundary, but that's definitely not the only one (see P3267 chapter 2.5-2.7
for a few ideas on what else you could do).

If you do convert them to runtime assertion checks, then if any such check
remains until link time or past link-time optimization, then you are
guaranteed that something wasn't proven always-true up to that point, so
you can (at your choice) just not have a runtime handler for it to link to,
and fail the link.


> * I did make an example of C++ Contracts using compile_assert, so that the
> Contracts were all evaluated at compile time. That is the pre()
> contract_assert() and post(). Of course not all programs are this simple.
> If I was using Contracts, I would prefer to use at compile time.
>
> https://github.com/jonnygrant/compile_assert/blob/main/testsuite/main25_a.cpp
>
> If I needed Contracts at runtime (DbC) I could follow the same pattern,
> add a runtime_pre(), runtime_post() and runtime_contract().
>
> > Would that accomplish the same thing your feature does?
>
> My understanding is a link failure (not finding the contract violation
> handler) would mean at least one failing contract remained, but we might
> not know which contract failed as the diagnostic, or can we specify
> different violation handler functions? like callbacks in C!
>

That is definitely true - but the linker already has all the knowledge it
needs to display which line of code where caused that symbol relocation to
exist. It's in the DWARF or the PDB data. Not telling the user is a choice.


> > On a second angle, what about having the ability (similar to what Jan
> Schultke proposed earlier) to mark a function as [[mustprove]] ? In that
> case we're requesting the compiler or static analyzer to check the function
> whether all contract checks in the function could be eliminated assuming
> they were enforced - and if not, to fail the compilation. This limits the
> blast radius in case a given check can be proven in some places but not
> others, as it refers to a specific function (instance) being compiled
> instead of to a given contract check. That, applied in the critical places,
> would seem to solve the same problem as your compile_assert.
> >
> > What's your view on these alternate approaches?
>
> I'm grateful for you sharing.
>
> I believe I missed that [[mustprove]] proposal, may I kindly ask if you
> could share a link?
>

As I wrote about 2 lines further down, "I haven't sent these out before, as
they are IMO not things suitable for standardization.".


> Would be tricky for some functions to [[mustprove]] constraints. They
> might call handle_contract_violation() at runtime.
>

The goal of mustprove is to require that all child function precontracts,
the functions' own postcontracts, and local implicit contracts (thinking
P3100 style) can be proven to never happen, assuming that the called
functions' postcontracts and the functions' own precontracts were
satisfied. Any other calls to handle_contract_violation are not related to
this. But it's an idea, it's not quite worked out in detail, and I already
know it's not going to be suitable for C++ standard adoption - if anything,
as a general name to align this request between compilers but without
specifying exactly what it does. It also requires a few bits of future
research & other properties being worked out, among others [[reproducible]]
and [[unsequenced]] to give more space for the compiler to eliminate
function calls to unseen functions, as well as research into pointer and
reference annotations (see clang's lifetimebound for one) that allow us to
provide functions with precontracts indicating lifetime matching the
implicit contracts that p3100 would introduce, so that those could also be
eliminated.


> Could you give an example of a contract check being proven and eliminated
> in once place but not in another? I'd like to understand better.
> compile_assert() is a little like that contract_assert() within the body
> of a function, although compile_assert only ever runs at compile time().
>
> > I haven't sent these out before, as they are IMO not things suitable for
> standardization. They are both reliant on however well your compiler does
> optimization and analysis. While your specific compilers can do this
> reliably to some point, and can be expected to keep up its ability to
> validate such things in the future, we can not require all compilers to do
> some specific analysis - or to limit its analysis to a given set of
> optimizations that could be required of all compilers. At best, we could
> ask for a standard name for such an attribute so that compilers could all
> understand the request the same way, but the implementation should be QoI,
> where compilers can provide either zero support by always failing all of
> those requests, or maximal support by making the compiler find
> counterexamples in case it cannot prove a given set, potentially to the
> point of almost halting progress entirely, depending on the situation the
> user is in.
> > Regards,
> > Peter Bindels
>
> You're completely right that different compilers have different strengths,
> and not all compilers may be able to prove complex conditions. On
> reflection I thought it's better to only aim to standardize the syntax of
> compile_assert(expression, message) and leave the extent of the
> implementation to the compiler. Although I have a working solution using
> the macro, so we have enough to do many things already (I've not yet found
> a limitation!)
>

Having a standard name is a good idea if we have multiple implementations
of it with fundamentally the same behavior that we can align behind a
single name. So far having just yours is not a good reason to make a
standard name, no matter how good it is.

For a simple example that I know we can never require anything to prove:

int collatz_length(uint64_t value) {
if (value == 1) return 0;
if (value & 1) {
assert(value < std::numeric_limits<uint64_t>::max() / 3);
return collatz_length(3*value + 1) + 1;
} else {
return collatz_length(value >> 1) + 1;
}
}

If you call this with a value between 1 and numeric_limits<int32_t>::max()
the assert is guaranteed to never fire, but nobody has been able to prove
this other than exhaustively - which is not realistic to require any
compiler to do. That, while the function itself only contains basic
mathematics, nothing complicated.

Regards,
Peter Bindels