michael-roe

At this point, I don't yet have an opinion on whether the HOL4 defintion is right or not. But I do have a reason for caring about it. We're testing...

Interesting, one of the test cases we get by tandem execution of a CPU against a simulator his something close to this: nmsub.s of all (positive) zeros on RISC-V.

Ok, so I now have a program that will take test cases generated from IBM;s FPGEN formal model and turn them into theorems for HOL4 to prove. I am not...

Thanks for the reply! Checking the sign of the zeros is what I'm going to do next. I agree that the sign of zero is (probably) where the bug is.

Ok, I now have some failing test cases. IBM's FPgen has: b32*+ =0 i +1.000000P-126 -1.2801D9P-113 -Zero -> -Zero xu but ... val f1 = `` : (23,8)float``; val f2...

The new Isabelle code looks right to me.

Do you want to have a try at fixing this bug? I can test it if someone else proposes a fix.

So, this bug is HOL4's floating point is not very likely to matter for real programs, but here is a moderately realistic program (in Standard ML) where it matters: fun...

I have just run the fused-multiply-add tests from IBM's FPgen against your revised float_mul_add, and all the tests now pass. So I think we have fixed the bug in float_mul_add....

At the moment, I can't get floating point arithmetic to work at all. But assuming I get past that issue, CakeML is missing several important operations that are in IEEE...