Add Why3 verification of float behavior

[mborland]

Discussion with Jenna is that we should treat our functions like a black box with defined inputs and output. It's ok if we overflow internally, etc. so long as we can prove that on output we halt forward progress in an unacceptable state. This handling is derived by the policy, but all the logic is shared.