Towards Verified, Constant-Time Floating-Point Operations