SAWCore Rational support

[RyanGlScott]

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

• Redefining the Rational type as a SAWCore primitive, along with the associated ratio, numerator, and denominator operations.

• Moving much of the Rational machinery to Prelude.sawcore, where it can be used across all saw-core backends (and not just cryptol-saw-core).

• Renaming Rational-related operations from, e.g., addRational to rationalAdd. This is more consistent with how other types name their operations using the <type name><operation> template (e.g., intAdd).

• Filling out all Cryptol instances for Rational in cryptol-saw-core.

This implementation comes with the caveat that symbolic Rational values do not enforce the precondition that their denominators are zero. In order to do this robustly, we will need to address #2433 first.

Fixes #3047.

[RyanGlScott]

The saw-core-rocq failures are because I do not define an Inhabited instance for Rationals. That, in turn, has led me to realize that I need to choose a concrete type to use when translating the primitive Rational type to Rocq. I suppose Q would be a good choice for this, but I'll want to make sure that the code for constructing Q values in saw-core-rocq actually typechecks. Until I have time to do so, I'll mark this as a draft.

[brianhuffman]

Are we sure this is what we want? If (for example) numerator (ratio 2 4) is not equal to numerator (ratio 1 2), then this means that can't have Eq Rational (ratio 2 4) (ratio 1 2) as a theorem without violating soundness. It also doesn't match the evaluation semantics in Cryptol.

[RyanGlScott]

numerator and denominator don't exist in Cryptol (GaloisInc/cryptol#1738), so I'm not sure how to respond to your "doesn't match the evaluation semantics in Cryptol" comment.

You are correct that misuse of numerator/denominator could violate soundness. That being said, I'm genuinely not sure how else to do this! All of the Rational operations need some way to access the numerator and denominator, and have some sort of primitive operation (with suitable documentation about potential pitfalls) was the best way I could think of.

[RyanGlScott]

Some alternative approaches:

• Define a primitive "recursor" for Rational that gives access to the underlying Integers in the callback. This is still unsound (you could define numerator and denominator on top of this recursor), but perhaps more difficult to misuse.
• Convert all Rational operations into primitives, and then define them all in saw-core. This would avoid needing to expose numerator/denominator to users, but it adds more trusted code to saw-core.

[brianhuffman]

My comment about "doesn't match Cryptol" was just about the ratio function by itself: In Cryptol ratio 1 2 and ratio 2 4 are identical, while in this proposed SAWCore implementation they are not.

I can think of two possible implementations that would be sound:

• Keep the numerator and denominator functions, but have them return the numerator and denominator of a reduced fraction. For example, numerator (ratio 2 4) = 1 and denominator (ratio 2 4) = 2.
• Define a primitive recursor for Rational that takes a function f : Integer -> Integer -> a (which gets called with the numerator and denominator) and also a proof that f respects the appropriate equivalence relation. In practice, this proof would not need to be inspected in order to evaluate the recursor, so we could introduce axioms for such proofs as needed.

[RyanGlScott]

In Cryptol ratio 1 2 and ratio 2 4 are identical, while in this proposed SAWCore implementation they are not.

To split hairs a bit: they are not identical in Cryptol, as Cryptol does not reduce the numerator or denominator when constructing Rational values. (See this code.) They are, however, equivalent up to the equivalence relation provided by Cryptol's (==) function, as (==) over Rationals is careful to compute equality in a way that works regardless of whether the numerator or denominator are reduced or not. (See this code.) The SAWCore rationalEq function that I added here mirrors that approach.

I agree that adopting this approach while simultaneously offering the ability to view the numerator/denominator un-reduced is a real problem.

• Keep the numerator and denominator functions, but have them return the numerator and denominator of a reduced fraction. For example, numerator (ratio 2 4) = 1 and denominator (ratio 2 4) = 2.

I am somewhat reluctant to do this, as I suspect that this will impose fairly non-trivial proof goals. See the discussion on GaloisInc/cryptol#1738. The only way I know how to do this is by implementing a gcd function via something like the Euclidean algorithm, and some experimentation suggests that this usually results in difficult-to-reason-about goals for SMT solvers.

• Define a primitive recursor for Rational that takes a function f : Integer -> Integer -> a (which gets called with the numerator and denominator) and also a proof that f respects the appropriate equivalence relation. In practice, this proof would not need to be inspected in order to evaluate the recursor, so we could introduce axioms for such proofs as needed.

Can you elaborate more on this option? What would such a proof look like?

[RyanGlScott]

I see. This approach would have the advantage of not needing to declare each Rational operation as a primitive, but on the other hand, I would be surprised if we were able to construct each proof term directly in SAWCore (intMul is a primitive, and therefore won't reduce). As such, I suspect we'd have to declare a new axiom corresponding to each Rational operation, which is arguably just much work as making each Rational operation a primitive to begin with.

[brianhuffman]

I guess it really depends on whether you could define the Rational primitives such that all SAW backends could share the same primitive implementation. If it turns out that we need separate implementations of Rational primitives in every SAW backend, that would be a big headache for maintenance and testing. But maybe we can define them generically in terms of the Integer operations, which wouldn't be so bad.

[sauclovian-g]

A possible further problem is that if we don't carry the thing around in lowest terms, we don't have a reliable way to use alternate definitions of equality. (See for example #2041.) Are we expecting to lower to a solver implementation of rationals, or to integer logic?

[RyanGlScott]

This mirrors Cryptol in that Rational operations are implemented in terms of integer logic.

[sauclovian-g]

In that case we probably either need to normalize after every operation, or give up on using hard equality. While we could conceivably do that by giving SAWCore a way to have alternate definitions of equality, there are reasons that e.g. Rocq doesn't. Which means we need to address #2041 so we can lower Cryptol Eq on rationals to something other than ==.

Unless someone's come up with a clever encoding of rationals that solves this problem. Someone did finally for finite maps a while back.