0 / 0 = -nan

Stream: lean4

[Mario Carneiro]

I was about to write a docstring explaining that 0 / 0 = 0 over most types, but on float, 0 / 0 = -nan, which is fun... For the record, division by zero on Float looks like this:

• a / 0 = inf, a / -0 = -inf if a > 0 or a = inf
• a / 0 = -inf, a / -0 = inf if a < 0 or a = -inf
• 0 / 0 = -0 / 0 = 0 / -0 = -0 / -0 = -nan
• nan / 0 = nan, nan / -0 = nan
• -nan / 0 = -nan, -nan / -0 = -nan

it's actually impressive how many patterns this fails to have

[James Gallicchio]

It's also a bit weird that it doesn't match IEEE floats (which don't have a notion of sign for NaN afaik, like nan = -nan)

[Mario Carneiro]

IEEE floats have signed nan

[Mario Carneiro]

they have a lot more nan stuff too, there's qNaN and sNaN and a huge payload

[Mario Carneiro]

like nan = -nan

That's yet another pattern that nan fails to have, a fairly famous one: not only nan != -nan, also nan != nan

[Mario Carneiro]

As far as I can tell, this is not standards conforming: 0 / 0 should be positive NaN (the sign bit should be the xor of the input signs), and it is positive in most languages I can test

[Mario Carneiro]

...except for C and C++ double, which at least explains the behavior

[Julian Berman]

I get nan here on macOS FWIW for 0/0 with clang++ -- some hasty googling though says this may have to do with SSE (and that disabling it may change whether you get + or - nan)

[Mario Carneiro]

oh, that's even better. I think that leads to yet another way to prove false using native_decide:

theorem foo : (toString (0 / 0 : Float)).length = 4 := by native_decide

if I save this in an olean file and you load it then you could prove that the expression is equal to 3 instead

[Mario Carneiro]

although I suppose the same is true about System.Platform.getNumBits:

example : (System.Platform.getNumBits ()).1 = 64 := by native_decide

[Mac]

Mario Carneiro said:

if I save this in an olean file and you load it then you could prove that the expression is equal to 3 instead

oleans are platform dependent, so using oleans cross-platform is expected to fail

[Gabriel Ebner]

The only platform-dependent part is whether it's 32-bit or 64-bit (and endianness, but that's not a practical concern nowadays when everything is little-endian). In fact, for mathlib we will certainly need to use oleans built on another platform (i.e., they're built on Linux/amd64 but used on macOS/aarch64 or Windows/amd64). It's completely infeasible to build mathlib for every OS+processor combination.

[Sebastian Ullrich]

In fact, we ship the macOS/Linux aarch64 cross builds with Linux x64 .oleans

[Sebastian Ullrich]

Related advertisement: we are still looking for volunteers for extending https://github.com/gebner/oleanparser with support for translating .oleans across architectures, in particular x64 to wasm32! At least it doesn't look like we've gotten all that closer to wasm64 https://webassembly.org/roadmap/

[Mac]

Gabriel Ebner said:

The only platform-dependent part is whether it's 32-bit or 64-bit (and endianness, but that's not a practical concern nowadays when everything is little-endian). In fact, for mathlib we will certainly need to use oleans built on another platform (i.e., they're built on Linux/amd64 but used on macOS/aarch64 or Windows/amd64). It's completely infeasible to build mathlib for every OS+processor combination.

I know this is the idea, but Leo was not a fan. He made it very clear to me when implementing cloud builds that Lean is not intended to support cross-platform use of built oleans (and, as such, the cloud build strategy is currently designed to prevent this). At least, that is what I got out of our conversation.

[Mac]

I am also not sure I agree with your experience on the cross-platform support for oleans. When I build oleans with WSL they do not work on Windows and when I build Windows oleans they do not work on WSL.

[Marc Huisinga]

Speaking about 32 bit platforms, is it possible that the to_offset overflow could be caused more easily on a 32 bit platform, or am I missing something?

[Marc Huisinga]

Ah, Gabriel's estimate may already assume 32 bit. My bad.

[Sebastian Ullrich]

unsigned is 32 bit in both cases, yes

[Sebastian Ullrich]

I.e. it's actually better on 32 bit because even if objects are only half the size, there's not nearly enough address space for the overflow

[Joseph Myers]

Mario Carneiro said:

As far as I can tell, this is not standards conforming: 0 / 0 should be positive NaN (the sign bit should be the xor of the input signs), and it is positive in most languages I can test

"When either an input or result is a NaN, this standard does not interpret the sign of a NaN. However,
operations on bit strings — copy, negate, abs, copySign — specify the sign bit of a NaN result, sometimes
based upon the sign bit of a NaN operand. The logical predicates totalOrder and isSignMinus are also
affected by the sign bit of a NaN operand. For all other operations, this standard does not specify the sign
bit of a NaN result, even when there is only one input NaN, or when the NaN is produced from an invalid
operation." (IEEE 754-2019, 6.3).

[pcpthm]

Idea: model Float as a quotient type where all NaN bit patterns are treated as the same.
It should be zero-cost after compilation.

WASM allows nondeterministic NaN bit pattern <https://github.com/WebAssembly/design/blob/main/Rationale.md#nan-bit-pattern-nondeterminism>.

[James Gallicchio]

Joseph Myers said:

" For all other operations, this standard does not specify the sign
bit of a NaN result, even when there is only one input NaN, or when the NaN is produced from an invalid
operation." (IEEE 754-2019, 6.3).

Yeah, I meant judgmental equality when I said nan = -nan in IEEE :joy: but I think judgmental equality doesn't really matter for floats since they are opaque. Arguably one fix to this problem is to have Float.toString print nan regardless of the sign bit :)

[Mario Carneiro]

I agree that using a quotient type would make the most sense. The type itself is not exposed to lean, so changing it to be "morally" a quotient type wouldn't change anything, except that as James says this would make Float.toString not a function anymore, so it should canonicalize NaNs first.

[Mario Carneiro]

While testing the other float functions to see what else "leaks" the nan sign bit or payload bits, I found this interesting behavior:

def Float.nan : Float :=
  if (0 / 0 : Float).toString == "nan" then 0/0 else -(0/0)

#eval Float.nan.toUInt8 -- 0
#eval Float.nan.toUInt16 -- 0
#eval Float.nan.toUInt32 -- 0
#eval Float.nan.toUInt64 -- 9223372036854775808
#eval (-Float.nan).toUInt64 -- 9223372036854775808

It's apparently not sensitive to the sign of the nan so it's not a portability problem, but it's still weird... (FYI 9223372036854775808 is 2^63.)

[pcpthm]

Reminded an old Rust soundness issue https://github.com/rust-lang/rust/issues/10184

[Mario Carneiro]

The C spec, unsurprisingly, declares that all float -> int conversions are UB when not representable in the target type, so this is definitely not a safe function to expose

[Mario Carneiro]

yep, that's exactly what I think is happening here

[James Gallicchio]

we could probably expose toUIntX?instead?

[Mario Carneiro]

I'm inclined to make it saturate for finite numbers and infinities and return 0 on nans... but first I have to figure out how to write that in conforming C