michael-roe

I'd don't entirely understand how HOL4's IEEE 754 theory works, but looking at https://github.com/HOL-Theorem-Prover/HOL/blob/62a0f78a20c8e8202d35e4cbbd397c8d70a3ad00/src/float/ieeeScript.sml it looks like is_nan and is_infinity are defined, but copysign and unordered aren't.

On floating point comparison operators: the result of a comparison can be less than, greater than, equal or unordered (4 possibilities). That gives 2**4 = 16 possible binary operators. You...

The L3 language lacks FP64_Unordered too, so in the L3 model of MIPS floating point I had to provide a definition for it: (https://github.com/acjf3/l3mips/blob/master/src/l3/fpu/instructions.spec)

By way of illustration, here is a rough attempt at a double to hexadecimal string function, written in Standard ML of New Jersey rather than CakeML. It doesn't handle denormalised...

This might also be an issue for some security proofs. Some people like to do confidentiality proofs that show the program doesn't learn any information it isn't supposed to have...

See also this blog post: https://trust-in-soft.com/blog/2020/04/06/gcc-always-assumes-aligned-pointer-accesses/

@jdemel: Thanks! I agree it could be the same issue. We ought to fix this, even if it needs an incompatible change to the API.

Even without this patch, we can build on MIPS. Some kernels don't work on MIPS, because of the ABI issue with complex numbers. The intent of this patch is to...

That seems ok to me. Do you want me to include that text in a revised version of this PR, or can it just go in as a separate commit?

I'm thinking about creating a pull request for this, but I'm trying to get cpu_features working on non-x86 architectures first, so I can test on a CPU that has popcount...