From: Thorsten Ottosen I guess p. 34 (Intervals) provides some hints to how we write such a careful predicate. If I understand this correctly, then we should at least use bounds that are exactly representable in the type involved.
I'm afraid the bounds are not enough, the values would also have to have exact representation. But the section indeed provides a hint -- maybe the problem could be somehow solved if we have a function float exact(float) that, given a floating point value (that may have greater precision because of caching in a register), returns a value that is truncated (has exactly the precision of float, not greater). Does it sound sensible? Anyway, I think the solution to reliable FP arithmetic is too general to make it a part of this library. This should be addressed by a dedicated library, and then Constrained Value library could make a use of it. Best regards, Robert