SAWCore Float support

[RyanGlScott]

This adds basic support for Cryptol's Float type in SAWCore. At a glance, this involves the following:

• Flesh out the floating-point primitives in the SAWCore prelude to cover all of the corresponding primitives in Cryptol's Float.cry module, as well as any additional primitives needed to support What4-related floating-point operations. Also add corresponding Cryptol-oriented functions to cryptol-saw-core's Cryptol.sawcore.

• Add Float support for the concrete and What4 backends. (Support in the AIG, RME, and SBV backends is left as future work.)

• Add saw-core-rocq support for Float by building on top of the Flocq library in Rocq.

One limitation of the current implementation is that certain partial operations do not enforce their preconditions properly (e.g., fpToRational's precondition that the input is finite and non-NaN). In order to do this robustly, we will need to address #2433 first.

Fixes #1237.

[sauclovian-g]

Can you add a comment there that points back here to help make sure the magic numbers stay in sync?

[RyanGlScott]

Add a comment to lib/Float.cry in the cryptol repo, you mean?

[sauclovian-g]

Hmm. Yes, I guess. Even more so given that it's in another repository. Something like "If you change this numbering, you must also change downstream references to it in SAW (SAWCore.FloatHelpers) and ..."

Ideally nobody ever will but...

[RyanGlScott]

I should note here for the sake of completeness: strictly speaking, we don't have to encode rounding modes as bitvectors. I mainly did this for the sake of convenience, as we need to define SAWCore primitives mentioning rounding mode arguments, and there already exists machinery for defining primitives with bitvector arguments. If we wanted, we could instead define RoundingMode like this:

data RoundingMode : sort 0 where {
  RoundNearestEven : RoundingMode;
  RoundNearestAway : RoundingMode;
  RoundPositive : RoundingMode;
  RoundNegative : RoundingMode;
  RoundZero : RoundingMode;
}

And then the correspondence between SAWCore rounding modes and LibBF rounding modes would become much more obvious. The flip side is that we'd have to figure out how to thread through a user-defined data type like RoundingMode through to SAWCore's primitive machinery. (I'm sure that this is possible, although I'd need to figure out how to do it.) Alternatively, we could define a primitive SAWCore Value for rounding modes, similarly to how we have VNat values (for SAWCore's Nat data type) and VBool values (for SAWCore's Bool data type).

[sauclovian-g]

I was just at PLDI where people were talking about round-to-odd; we might want to add it, though not necessarily right now. FWIW

[RyanGlScott]

If we wanted to support round-to-odd, then we would first need to update libBF-hs and what4, as SAW ultimately dispatches to those libraries to perform the rounding. On the libBF-hs side, this would require patching the LibBF C library. On the what4 side, this would require us to do something a bit more clever than what SMT-LIB's FloatingPoint theory offers, as the pre-baked rounding modes that it includes does not cover round-to-odd. (Both of these are doable, but would take some work.)

[sauclovian-g]

If things play out as I was hearing, some of that may happen for us upstream, eventually. For now maybe it's enough to just keep it in mind for later. Maybe we should reserve the code number.