Extracting numerators/denominators of Rational values

[RyanGlScott]

Currently, Cryptol offers a way to construct a Rational value from a numerator and a denominator:

cryptol/lib/Cryptol.cry

Line 780 in 0985325

primitive ratio : Integer -> Integer -> Rational

It does not offer convenient ways to extract the numerator or the denominator from an existing Rational value, however. That is, there are no functions of these types:

primitive numerator : Rational -> Integer
primitive denominator : Rational -> Integer

This issue tracks whether we should add such functions or not.

What's the risk?

At first glance, it seems like it should be straightforward to implement these. Before we return the numerator or denominator, we need to ensure that they are normalized so that, e.g., numerator (ratio 6 10) == 3 and denominator (ratio 6 10) == 5. To do so, we can compute the greatest common divisor (gcd) of both Integers and divide them by the gcd. For instance, the gcd of 6 and 10 is 2, and indeed we have that 6/2 == 3 and 10/2 == 5.

This plan will work well for concrete Rational values, but what about symbolic Rational values? (Recall that these can arise when :prove-ing properties about Rationals.) It is unclear to me how to implement gcd in a way such that SMT solvers can efficiently reason about it. The usual, recursive definition of gcd is:

gcd x y = gcd' (abs x) (abs y)
  where
    gcd' a b =
      if b == 0
      then a
      else gcd' b (a % b)

This is recursive in the gcd's second argument, but the termination criteria is not very obvious. As such, I suspect that most SMT solvers would infinitely loop if it had to reason about any properties involving gcd.

Accept the risk?

If we can't make numerator/denominator work efficiently for symbolic Rationals, then perhaps we could still add these operations, but prominently advertise that they are not designed to work well with :prove. Would that be an unusual thing to do? I'm not aware of any other Cryptol primitives that are anti–SMT reasoning to quite the same extent, but perhaps I'm just not aware of them.

Don't risk it?

If we decide that adding numerator/denominator is a bad idea, then at the very least, we should document this choice somewhere, as the topic of deconstructing Rational values comes up quite frequently. Perhaps the documentation for Rational would be a good place for this.

[weaversa]

@auricratio once made a symbolically terminating gcd in Cryptol...