Soft-float math library

[eduardosm]

I recently published a Rust floating point math library which implements math operations (sqrt, sin, exp, log...) for both native floating point and soft-floats. When using soft-floats, all operations should produce consistent results regardless of target-specific hard-float subtleties.

Miri could use it to avoid some "host floats" FIXMEs. It that is ok, I'll be glad to create a PR.

[RalfJung]

That sounds like a cool library!

However, I am always hesitant to add new dependencies to the rustc workspace, so I think I'd prefer to wait a bit and see how it develops. Also, note that we already have a softfloat library, apfloat -- can your library work with the apfloat types? I see apfloat as a dependency so maybe the answer is yes?

[eduardosm]

My library exposes two soft-float types (single and double precision). They internally use rustc_apfloat, but it is an implementation detail, not exposed in the public API. Lossless interoperability is possible through to_bits / from_bits.

[RalfJung]

For Miri it would be a lot nicer if it worked generically on any apfloat type. That would allow reducing code duplication between the f32 and f64 code paths, and will become crucial as we add more support for f16 and f128.

[RalfJung]

Looking at the library API docs, I am wondering about two more things:

• It says "with an error of less than 1 ULP". However, I think this is not equivalent to saying "rounded to the nearest representable number (using some specific round mode)". There are generally two results that are less than 1 ULP away from the infinite-precision result (one "rounding up" and one "rounding down"). So there is still some amount of underspecification here, right?
• Rust doesn't make precision guarantees for these so we'd probably want to disturb the result a bit non-deterministically. ;)

[eduardosm]

For Miri it would be a lot nicer if it worked generically on any apfloat type.

You mean any type that implements the rustc_apfloat::Float trait? That would require arbitrary precision algorithms. Although my implementation is mostly generic, certain parts of the algorithms (such as polynomial approximation or certain constants) are specialized for single and double precision.

Note that direct interoperability with apfloat would generate friction when a new semver-incompatible version of apfloat is released (Miri wouldn't be able to use the new version until my library does).

• It says "with an error of less than 1 ULP".

Indeed, rounding to nearest would be up to 0.5 ULP. I decided to stick with 1 ULP because doing better is quite hard and I believe it is good enough for most applications that use single or double precision floating point. I only guarantee 0.5 ULP for sqrt.

So yes, there is underspecification, but results should be cross-platform reproducible when using soft-float.

• Rust doesn't make precision guarantees for these so we'd probably want to disturb the result a bit non-deterministically. ;)

That would use -Zmiri-seed, right? So it would be deterministic non-determinism 😄.

[RalfJung]

You mean any type that implements the rustc_apfloat::Float trait? That would require arbitrary precision algorithms. Although my implementation is mostly generic, certain parts of the algorithms (such as polynomial approximation or certain constants) are specialized for single and double precision.

Not necessarily any type, as long as the 4 we need work. ;)
We'd want to be able to write functions like this, and ideally use the existing conversion functions to call them, like here.

I did notice, however, that your crate already has a trait. So potentially we could handle this on the Miri side, with something like

trait FpMath {
  type M: fpmath::FloatMath;

  fn into_fp_math(self) -> Self::M;
  fn from_fp_math(Self::M) -> Self;
}

impl FpMath for rustc_apfloat::ieee::Single {
  type M = fpmath::SoftF32;

  // Implement conversion methods.
}

That should only be a few dozen lines total, once, for all 4 types, so seems acceptable.

Note that direct interoperability with apfloat would generate friction when a new semver-incompatible version of apfloat is released (Miri wouldn't be able to use the new version until my library does).

That's a fair point. Not sure how likely such an apfloat release is.

I only guarantee 0.5 ULP for sqrt.

sqrt is the one I am most interested in, since that's the only one where Rust guarantees maximal precision and we use hard floats. It should be fine since we are, in turn, using Rust on the host side where infinite precision should be guaranteed... but it is not very satisfying.

IMO sqrt should really be in apfloat.^^

That would use -Zmiri-seed, right? So it would be deterministic non-determinism 😄.

Yes. :)

[RalfJung]

"an error of less than 0.5 ULP" is impossible, though, when the result is exactly between two representable numbers, right?

[eduardosm]

I did notice, however, that your crate already has a trait. So potentially we could handle this on the Miri side, with something like

That looks reasonable.

"an error of less than 0.5 ULP" is impossible, though, when the result is exactly between two representable numbers, right?

Right, an error of exactly 0.5 ULP is a tied rounding.

However, considering that floating point numbers are rational non-recurring numbers, the result of the square root will be either (besides special cases like NaN):

• Non-recurring rational. In this case the result will have half significant digits (or bits), so the error is zero.
• Irrational. That means it will have an infinite amount of non-zero significant digits, which means that rounding will never tie (and thus, error will never be exactly 0.5 ULP).

[RalfJung]

What is a "non-recurring rational"? The only thing I found online is "Non - recurring numbers are those in Mathematics that do not repeat their values after a decimal point" and that can't be right.

But if I understand the argument correctly, then it is -- if the output is a rational (which indeed it must be for the "tied" case), then it is a rational with smaller magnitude than the input, so more precision is available than with the input, so we can't run out of precision?

[eduardosm]

What is a "non-recurring rational"? The only thing I found online is "Non - recurring numbers are those in Mathematics that do not repeat their values after a decimal point" and that can't be right.

Since a recurring rational is a number with an infinite amount of digits with a repeating pattern (e.g. 1/33 = 0.03030303030303...), a non-recurring rational is a number with a finite amount of digits.

But if I understand the argument correctly, then it is -- if the output is a rational (which indeed it must be for the "tied" case), then it is a rational with smaller magnitude than the input, so more precision is available than with the input, so we can't run out of precision?

You can reason with the opposite operation (squaring). When you calculate the square of a number, the result will have around twice the amount of digits.

[RalfJung]

a non-recurring rational is a number with a finite amount of digits.

That's a very strange definition. Is it common? I've never encountered it before.

The way I learned things, a number like 0.25 has a recurring decimal expansion -- it has infinitely many 0 at the end.

[eduardosm]

I hadn't thought of the case where the recurring part is just zeros.

So to be clear, what I wanted to express in #3898 (comment) with "non-recurring rational" is a number with a finite amount of non-zero digits.