algebraic operators for floats stable in next rust - supported?

[xd009642]

Next stable release will stabilise things like https://doc.rust-lang.org/nightly/std/primitive.f32.html#method.algebraic_add which are akin to -ffast-math in C and C++. They're slightly stricter than ffast-math so NaN and INF won't result in UB and I think denormals are normalised to zero, but they can made the numerics weakly deterministic and allow things like reordering etc.

I'm planning on switching a bunch of my code to use these where it should be safe, but now I'm wondering if I'm wrong can kani catch it?

[SebTardif]

@xd009642

I'm planning on switching a bunch of my code to use these where it should be safe, but now I'm wondering if I'm wrong can kani catch it?

Short answer: do not treat Kani as a check that algebraic_add (and friends) are safe to switch to. It can still help with IEEE-shaped bugs around the call. It will not model the extra freedom those operators give LLVM.

f32::algebraic_add is not IEEE +. It is a rustc/LLVM op with algebraic flags (reassociate, contract, reciprocal, and similar). The compiler may rewrite (a + b) + c into a + (b + c) or fuse a multiply-add. That rewrite is the point of the API, and it is also where a "this should be safe" assumption dies.

Kani lowers Rust to GOTO/CBMC and models ordinary float ops as bit-precise IEEE values. The feature-support notes already say that even IEEE sin/cos/sqrt are over-approximated (a nondeterministic value in range), which makes Kani a poor fit for numeric-precision properties. Algebraic operators go the other way: the concrete IEEE path is stricter than what the compiler is allowed to do. A proof over IEEE + does not imply the same proof after reassociation.

What Kani can still catch:

• panics, overflows, and assertions on values you compute after an algebraic op, under IEEE semantics of the un-rewritten expression
• NaN/Inf cases you assert on, if the intrinsic is compiled as a normal float add (these ops are specified not to turn NaN/Inf into UB)

What it will not catch:

• a property that only fails after the compiler reorders or contracts operations
• a weakly deterministic result that depends on LLVM's rewrite

I would write a five-line harness that calls algebraic_add on kani::any() inputs and see what Kani does. If there is no intrinsic override yet, an unsupported path is compiled as assert(false) when reachable, which shows up as a failure rather than a silent miss. Use that as a smoke test that the op is modeled, not as evidence that switching is safe.

For the "is this rewrite allowed" question, you want a paper proof of the algebraic identity you rely on, or a tool that checks the identity over reals with explicit reassociation. Kani's strength here is still the surrounding Rust (bounds, panics, decoder invariants), not the fast-math contract.

[feliperodri]

I ran the smoke test @SebastienTardif suggested, on main today:

#![feature(float_algebraic)]

#[kani::proof]
fn check_algebraic_add() {
    let a: f32 = kani::any();
    let b: f32 = kani::any();
    kani::assume(a.is_finite() && b.is_finite());
    assert!(a.algebraic_add(b) == a + b);
}

Check 1: core::f32::<impl f32>::algebraic_add.unsupported_construct.1
  - Status: FAILURE
  - Description: "fadd_algebraic is not currently supported by Kani."
VERIFICATION:- FAILED

So the concrete answer to "can Kani catch it?" is: not today, and not silently. The f*_algebraic intrinsics aren't modeled, so any reachable call is reported as an unsupported construct and verification fails, so you won't get a false "SUCCESS" out of code that uses them. (Only the older _fast family is handled; fadd_fast/fsub_fast are supported, fmul_fast/fdiv_fast partially see #809.)

Adding support is straightforward and we should do it. But it's worth being clear about what it would buy you, because @SebastienTardif's main point stands: the natural modeling is plain IEEE +, and that is stricter than what LLVM is permitted to do. A proof that passes under IEEE semantics does not establish that reassociation or fusing a multiply-add preserves your property, which is exactly the assumption you're asking about. Faithfully modeling the freedom would mean nondeterministically choosing among the permitted rewrites, and that's a real design question, not a missing-intrinsic fix.

Practically: Kani is a good fit for the Rust around the arithmetic (panics, bounds, unwraps, decoder invariants, overflow on values you derive from the result), and a poor fit for "is this algebraic identity safe to let the compiler exploit." For the latter you want a paper proof of the identity, or a tool that reasons over reals with explicit reassociation.

I'd appreciate if you could open a tracking issue for f*_algebraic support and link it here.

[xd009642]

Mainly I have a bounded range of possible inputs to a function and some asserts that the values don't leave an expected output range or result in inf/nan. Changes in accuracy due to reordering etc don't matter in this domain

[xd009642]

Issue raised. I'm on my phone so it was a bit of a faff but I can fill in more detail tomorrow if desired: #4736