Add some examples that use floating-point operations

We should demonstrate the copilot-verifier is capable of handling of specifications that make use of floating-point operations. A good first milestone is the Heater example from the copilot repo (not to be confused with copilot-verifier's own Heater example, which avoids the use of floating-point). At the moment, if you try running copilot-verifier on this Heater example, it will fail to prove these goals:

Details

=====
== Running the HeaterCelsius example...
=====

Generated "results/heaterCelsius/heaterCelsius.c"
Compiled heaterCelsius into results/heaterCelsius/crux~heaterCelsius.bc
Translated bitcode into Crucible
Generating proof state data
Computing initial state verification conditions
Proving initial state verification conditions
All obligations proved by concrete simplification
Computing step bisimulation verification conditions
Proving step bisimulation verification conditions
Proved 0 of 4 total goals
[Crux] Found counterexample for verification goal
[Crux]   results/heaterCelsius/heaterCelsius.c:30:6: error: in step
[Crux]   Mismatch between Copilot value and crucible value
[Crux]   XFloat let -- :1:0
[Crux]       v15 = floatMul RNE (bvToFloat RNE ctemperature_r0@13:bv) 0x0.969697
[Crux]    in floatSub RNE v15 0x32
[Crux]   FloatRepr SingleFloatRepr
[Crux] 
[Crux] 
[Crux] Found counterexample for verification goal
[Crux]   results/heaterCelsius/heaterCelsius.c:33:6: error: in step
[Crux]   Mismatch between Copilot value and crucible value
[Crux]   XFloat let -- :1:0
[Crux]       v15 = floatMul RNE (bvToFloat RNE ctemperature_r0@13:bv) 0x0.969697
[Crux]    in floatSub RNE v15 0x32
[Crux]   FloatRepr SingleFloatRepr
[Crux] 
[Crux] 
[Crux] Found counterexample for verification goal
[Crux]   internal: error: in <>
[Crux]   Trigger guard equality condition: "heaton"
[Crux]   Details:
[Crux]     let -- :1:0
[Crux]         v15 = floatMul RNE (bvToFloat RNE ctemperature_r0@13:bv) 0x0.969697
[Crux]      in not (floatLt (floatSub RNE v15 0x32) 0x12)
[Crux] 
[Crux] Found counterexample for verification goal
[Crux]   internal: error: in <>
[Crux]   Trigger guard equality condition: "heatoff"
[Crux]   Details:
[Crux]     let -- :1:0
[Crux]         v15 = floatMul RNE (bvToFloat RNE ctemperature_r0@13:bv) 0x0.969697
[Crux]      in not (floatLt 0x15 (floatSub RNE v15 0x32))

If we get that working, we can become more ambitious and try to verify examples that use transcendental functions, such as this Trig example. That will first require incorporating GaloisInc/what4#160 into crucible-llvm and overriding the necessary functions in LLVM. I have a WIP branch for this here.

The well-clear violation example (WCV) would also be good; it doesn't use any special functions I think, so it should be easier to get going than Trig.

Use `SymInterpretedFloat`s in `XExpr`

GaloisInc/copilot-1#1 and GaloisInc/crucible#889 are first steps in this direction. Some remaining tasks that may need to be completed before we can actually verify floating-point examples in copilot-verifier are:

In copilot-theorem, there are a number of operations that convert from floating-point values to reals, perform an operation on them, then convert the result back to a floating-point value. (See Use SymInterpretedFloats in XExpr GaloisInc/copilot-1#1 (comment).) With Special functions GaloisInc/what4#160 and Add pow (x^y) as a SpecialFunction GaloisInc/what4#163, this should no longer be necessary, as we can just use special functions directly.
copilot makes use of pow ~~and logb~~ (EDIT: logb isn't needed after all, see Add some examples that use floating-point operations #3 (comment)), which currently do not have SpecialFunction support in what4. We should add these and propagate them up into crucible and copilot-theorem.
There are some "constructed" operations in copilot-theorem that are implemented as compositions of lower-level floating-point primitives from what4, such as Abs. (See Use SymInterpretedFloats in XExpr GaloisInc/copilot-1#1 (comment).) We should verify that these behave as expected.

Use `SymInterpretedFloat`s in `XExpr` (#1)

On second thought, we likely don't need an override for logb. Although copilot has a Logb constructor, it actually compiles down to the log function, which crucible-llvm already supports. In that case, I believe the only missing piece of functionality is pow. I've submitted the first steps towards supporting that in GaloisInc/what4#163 and GaloisInc/crucible#901.