Asserts for floating point tests

[sunfishcode]

assert_eq uses ocaml's <> which returns false for -0 <> 0 and true for NaN <> x ∀x. This is the usual behavior, but for our floating point unit tests we have unusual needs: we do actually need to distinguish between -0 and 0, test for specific NaNs sometimes, and test for any NaN sometimes. What do people think of adding the following?

• assert_eq_bits - like assert_eq, but reinterpret-casts both operands as same-size integers first
• assert_nan - has one operand and asserts that it is a NaN (of any kind)

[rossberg]

I'd suggest simply changing the implementation of assert_eq to use the stricter equality operator. Or is there any reason to ever use IEEE equality in the tests we want to write?

As for NaN tests, it is easy to express that in WASM itself, so I don't think we need to extend the assertion language just for that either.

[rossberg]

Btw, once your new float implementations land, = and <> on those types will automatically mean bitwise equality. So maybe it isn't even necessary to change anything here.

[sunfishcode]

You're right; there is no need for the looser equality in our tests. It just feels weird to me to give eq a subtly different meaning in this context than it has in wasm itself.

As for NaN tests, it seems like it will be quite inconvenient to express any-NaN tests in terms of assert_eq regardless of whether it's the strict or loose version. The strict one tests for a specific bit pattern when we want to accept many, and the loose version requires we name the value so that we can reference it twice and form x <> x. Or are you proposing we add NaN test functions inside the wasm modules themselves?

[sunfishcode]

BTW, you're right that = and <> now automatically do bitwise equality with my float implementations. How does that work, given that the types are abstract?

[sunfishcode]

Ah, I found a blog post which explains it.

[jfbastien]

Agreed with what I think @rossberg-chromium is saying on NaNs: this should be done with a wasm function, e.g.: assert(is_nan(v)).

[rossberg]

BTW, you're right that = and <> now automatically do bitwise equality with
my float implementations. How does that work, given that the types are
abstract?

In Ocaml, equality is generic, and does the "right" thing depending on the
runtime type of the value.

That actually is quite a dubious semantics, given that IEEE defines a
completely broken notion of equality for floats (which is not even close to
being an equivalence relation). And as you observed, it also breaks
abstraction. I'd prefer what e.g. SML does, where IEEE equality is a
separate operator.

[sunfishcode]

Ok, I now have an implementation of assert_eq_bits and assert_nan, and tests that use them (test/float32.wasm and test/float64.wasm), in this branch:

https://github.com/WebAssembly/spec/tree/float-tests

It's still experimental (the final version may not actually want to weigh in at 17 MiB of tests, etc.) but I think this demonstrates some nice properties of assert_eq_bits and assert_nan:

• It avoids using = and <> on Float32.t and Float64.t values. Even if OCaml makes this work, it breaks the encapsulation of abstract types.
• It avoids ambiguity on the term eq with respect to floating point types.
• Each assert line in the test files test/float32.wasm and test/float64.wasm makes exactly one call into the wasm module, and does nothing but check the result value.
• It issues a human-readable error message when floating-point types are used for an integer assert, or integer types are used for a floating point assert.

What do people think?

[sunfishcode]

#81 implements this and is now merged.