On 6/3/25 4:09 PM, Ville Voutilainen via Std-Proposals wrote:
> On Tue, 3 Jun 2025 at 19:24, Tom Honermann<tom_at_[hidden]> wrote:
>
>> I think something like the following suffices for what was proposed.
>>
>> double compute_sqrt(double arg) pre (arg > 0.0); inline double sqrt(double arg) { if (arg < -0.0) returnstd::numeric_limits<double>:: quiet_NaN(); if (arg == 0.0 /* or is +/- infinity or is a NaN*/) return arg; return compute_sqrt(arg); } double get_definite_positive_value() post(r: r >= 0.0); double f() { double d = get_definite_positive_value(); return sqrt(d); }
>>
>> I understand that this doesn't address (some of) what the proposer wanted since it requires that the checks to be optimized away are exposed in the TU where the call is made. However, that constraint is also present in the technical specifications of the proposal.
> When does that make a program containing those pre/post run faster
> than a program that doesn't contain them?

Per [basic.contract.eval]p5 in the P2900 <https://wg21.link/p2900>
proposed wording, an implementation is not required to evaluate a
contract predicate if it has some other means of knowing what the result
of evaluation would be. A conforming implementation can elide checks
when it has already identified constraints on the possible values a
variable may hold such that a predicate evaluation would be unnecessary.
This can occur when:

  * The possible values are constrained by static analysis (e.g., a data
    flow analysis of get_definite_positive_value()), or
  * The possible values are constrained by a previous evaluation (e.g.,
    the evaluation of the postcondition of
    get_definite_positive_value()), or
  * The possible values are constrained by an [[assume(expr)]]
    attribute. For example:
    double g() {
       double d = get_definite_positive_value();
       [[assume(d > 0.0)]];
       return sqrt(d);
    }

A non-conforming implementation can also provide an assume semantic
whether or not WG21 approves of it.

The checks that the post author wanted to elide in this example are not
contract checks; they are just typical condition checks and their
evaluation is subject to the as-if rule. Explicit preconditions and
postconditions inject facts (subject to verification) that may be used
by an optimizer accordingly. I'm sure you recall SG21 discussion, and
even some implementation reporting, regarding the potential for such
injected facts to improve code generation and performance even when a
checking contract semantic is selected. The presence of preconditions
and postconditions can constrain the possible executions of the program
such that some subset of all potential condition evaluations can be elided.

On, and I now see that I messed up the postcondition for
get_definite_positive_value(). That should, of course, have been:

    double get_definite_positive_value()
       post(r: r > 0.0);

Tom.