Stated math.h postconditions are stronger than actual implementations

[wandernauta]

The included math.h header promises a number of things about the result value of floating point mathematical functions in the C math library, which means that e.g. this (silly) C program verifies and fails:

#include <assert.h>
#include <math.h>

int main() {
    double e = exp(1.0);
    assert(e == 2.7182818284);
}

$ ./fl
fl: fl.c:6: main: Assertion `e == 2.7182818284' failed.
Aborted (core dumped)

However, the C standard does not specify accuracy requirements for functions like exp (including if IEEE 754/IEC 60559 conformance is claimed), letting implementations make their own performance/accuracy tradeoffs.

In practice, the exact bits in the result can depend on the choice of compiler, C library, and hardware, as well as runtime configuration. In this example (with x86-64 gcc) the actual program comes up with a more mathematically accurate result than the one in VerCors math.h, but it is not required to; certainly, it is not required to come up with exactly the result implied by the @ensures clause.

In addition, some function contracts promise a number result, while they can (or must) actually return not-a-number, so this verifies and fails:

#include <assert.h>
#include <math.h>

int main() {
    double nan = sin(pow(-0.5, 0.5));
    assert(nan >= -1);
}

$ ./n
n: n.c:6: main: Assertion `nan >= -1' failed.
Aborted (core dumped)

For soundness, it may be better to not promise anything about these functions, not even that they are pure.

(Something similar would in theory apply to the +, -, *, /, and square root operations, but that could just be documented as "we assume IEEE 754 and default floating-point environment" or similar.)

[bobismijnnaam]

Just to be complete: making these functions pure is indeed a bad idea because they change error state (https://en.cppreference.com/w/c/numeric/math/sin, "Error handling").

Putting some bounds in the contract shouldn't be too dangerous, right? Provided the edge cases are encoded in the contract as well.

I think floats and doubles are currently encoded as mathematical real numbers. Making the contracts of these functions less precise could make that glaring inconsistency less dangerous.

[wandernauta]

Yeah, it's mostly the ensures \result == something clauses that worry me, both on the trig functions as well as the rounding functions. If done carefully, having some bounds on the result should be alright.

For instance, experimentally it looks like all implementations of sinf I can find do indeed return results inside [-1, 1] for all finite numbers (so not nan not +inf not -inf); I don't have a chapter-and-verse reference to a spec that guarantees this, but it doesn't seem like a weird thing to assume of a software or hardware implementation.

Bounds with "half of VerCors' definition of π" or similar as one of the endpoints are risky: M_PI is not standard, and the results for asinf(1) and asinf(-1) exceed the stated bounds on my machine.

[bobismijnnaam]

all implementations of sinf I can find do indeed return results inside [-1, 1]

The way it is phrased on cppreference makes me think that this bound is indeed in the standard (would be nice to have a citation, though).

Bounds with "half of VerCors' definition of π" or similar as one of the endpoints are risky: M_PI is not standard, and the results for asinf(1) and asinf(-1) exceed the stated bounds on my machine.

Agree, let's not do that.