Models for sine and cosine builtins should be more precise

[adpaco-aws]

The current models for sine/cosine are too over-approximated: They return 0/1 if the argument is 0, and a nondeterministic value -1 and 1 otherwise. I think this is confusing for everyone who has used them (see an example in model-checking/kani#1342), and they can be improved so they provide more precise results for special values the same way it's done for 0. Additionally, the returned interval can also be narrowed between these special values.

[tautschnig]

While I, of course, agree that those models are over-approximations: what is the bar when the implementation would be considered sufficiently precise? Asking in another way: what performance price are you willing to pay?

[adpaco-aws]

The smallest radian value defined for f64 constants is FRAC_PI_8 (i.e., PI/8). I believe that providing exact (pre-computed) values from [0, 2*PI] in increments of PI/8 (and symbolic intervals for any number in between) would not be too costly and a significant improvement. What do you think?

[martin-cs]

@adpaco-aws it sounds reasonable but i think we need to answer @tautschnig 's question. From looking at this I think the key issues are:

1. What do you regard as "exact"? The computation that goes float -> real -> compute in real -> nearest float? The system implementation of sin, cos, etc.
2. What kind of accuracy do you want? cos(x) == 1.0 and sin(x) == 0.0 for lots of small values of x. Is that accurate? Over 1.0p+26f or so even the most accurate implementation of sinf will oscillate chaotically. How do you feel about rare cases being very very inaccurate?
3. Are you expecting to have any kind of mathematical properties like sin(x) == sin(x + 2*M_PI) or sin(x) \in [-1,1] or local monotonicity?

If you want accurate then you have to use the system implementations. There are too many weirdnesses and corner cases to be bit accurate any other way. This will almost certainly be too expensive.

If you want to be performant then you will need to do some kind of approximation. The key question is what kind of guarantees you can give about that.

[adpaco-aws]

Hi @martin-cs, sorry for the delay in getting back to you.

To be clear, I'm not saying we use system implementations. I agree those will be too expensive.

What I'm proposing is that we extend the current model to provide more precise results. At present, this test represents all properties we can prove about sinf32. The case where x = 0 is what I consider an "exact" value, the point here is that the same can be done for other key values. For example, we could add an additional assumption in the current model to prove sin(PI/2) == 1.0:

#[kani::proof]
fn sine_const_frac_pi_2() {
    let x = std::f32::consts::FRAC_PI_2;
    let sine = unsafe { std::intrinsics::sinf32(x) };
    assert!(fp_equals(sine, 1.0));
}

Same goes for intervals, which could be more fine-grained than the [-1.0, 1.0] interval always returned by the current model. This would allow us to write more constrained properties like:

#[kani::proof]
fn sine_range_frac_pi_2() {
    let x: f32 = kani::any();
    kani::assume(x.is_finite());
    kani::assume(x >= 0.0 && x <= std::f32::consts::FRAC_PI_2);
    let sine = unsafe { std::intrinsics::sinf32(x) };
    assert!(sine < 1.0 || fp_equals(sine, 1.0));
    assert!(sine > 0.0 || fp_equals(sine, 0.0));
}

AFAIK this would just be a matter of adding further assumptions to the current model. Do you think this could affect performance?

[martin-cs]

@adpaco-aws my apologies for the delay in getting back to you.

Will it affect performance : probably.
Will it affect performance in a significant way : it really depends on what assumptions you are adding.

My bigger concern is how you are picking these assumptions. Are they properties of the mathematical sine? The "ideal" implementation of sine (the mathematical sine rounded to the nearest floating-point number in the appropriate format)? Or the system implementation of sine? If it's the system one, then, which system because different platforms and different compiler options will do different things? These do not necessarily have the same properties.

[jimgrundy]

It should be possible to write a nondeterministic sin and cos model that returns a result constrained to have the properties you want. I would encourage you to write that model and contribute it.