Split up Arith?

[robdockins]

While working on some simulator internals, it occurs to me that we should maybe think about reorganizing the Arith class. Currently Arith contains the following operations:

primitive (+) : {a} (Arith a) => a -> a -> a
primitive (-) : {a} (Arith a) => a -> a -> a
primitive (*) : {a} (Arith a) => a -> a -> a
primitive negate : {a} (Arith a) => a -> a
primitive (/) : {a} (Arith a) => a -> a -> a
primitive (%) : {a} (Arith a) => a -> a -> a
primitive (/$) : {a} (Arith a) => a -> a -> a
primitive (%$) : {a} (Arith a) => a -> a -> a
primitive (^^) : {a} (Arith a) => a -> a -> a
primitive lg2 : {a} (Arith a) => a -> a
primitive fromInteger : {a} (Arith a) => Integer -> a
primitive negate : {a} (Arith a) => a -> a
primitive infFrom : {a} (Arith a) => a -> [inf]a
primitive infFromThen : {a} (Arith a) => a -> a -> [inf]a

These were are all sensible operations when Cryptol basically only contained bitvectors as primitive types. However, with the addition of Z and (especially) Z_n types and the planned addition of floating point and real types, it's really unclear that this grouping still makes sense.

Problems worth discussing:

• The division operations on Z_n don't make much sense, as those types naturally only have the structure of a ring. Moreover, even when n is a prime, I'm pretty sure the division we offer doesn't match the multiplicative inverse structure of the prime field.
• I really am not sure the signed division and modulus operations make much sense on base types other than bitvectors.
• The exponentiation operator probably has too general a type. I think what we want here is an iterated multiplication operator (with type a -> [n] -> a) rather than, say, the exp operator on real numbers.
• Likewise the type of lg2 is probably too general, and maybe doesn't make much sense at some types (again Z_n is a little strange here, and floating point types will be odd as well).
• The enumeration operations can get very strange when applied to floating point values, as can be seen from the corresponding Haskell operations.

[atomb]

I can confirm that the division operation on Z p for prime p does not match the multiplicative inverse structure of the prime field. I implemented some prime field arithmetic code that would have have been cleaner with built-in division but had to use multiplication by the inverse because the / operator didn't do that.

In that same code, we needed to do exponentiation with a different exponent type than base type. So, while it didn't necessarily have to be a -> [n] -> a, some variant of a -> b -> a would have been nice.

And, yes, I agree that many of these operations don't make sense for floats and reals.

[brianhuffman]

I agree that type of the exponentiation operator ^^ is too general. This causes trouble in the symbolic backends, where we can only translate x ^^ y on type Integer or Z n when y is concrete. Using type a -> [n] -> a would be nice because we can define it in Cryptol (not as a primitive) with a square-and-multiply algorithm, and in that form it can be handled by all the symbolic backends.

[brianhuffman]

I also think that lg2, /$ and %$ really only make sense for bitvectors, and that their types should be specialized accordingly.

[yav]

Agreed. I even thought we removed lg2 in favor of width, which is what you mean 99% anyway?

[brianhuffman]

We removed lg2 at the type level, and width is only at the type level.

[brianhuffman]

As for enumeration operators: The weirdness in Haskell's list enumerations on floats has to do with deciding when to cut off at the end; we won't have that problem here, as all the Arith-overloaded enumerations in Cryptol are inifinite.

There is one bit of weirdness we'll have to deal with for float enumerations in Cryptol: For [x...], we'll have to decide whether this means iterate (+1) x or [ x + fromInteger n | n <- [0...] ]; at magnitudes where the gaps between representable numbers are 1 or more this can make a difference.

[yav]

Ah yes, got confused. I don't know that I've ever used the value level lg2.

[brianhuffman]

A quick search through the cryptol-specs repo doesn't turn up any value-level uses of lg2. (There are a few type-level uses of lg2, though, where lg2 is now defined as a type synonym in terms of width.)

I don't expect I would ever need to use value-level lg2, and I can't imagine anyone needing it at any non-bitvector type. If we specialized it to type [n] -> [n], we could remove it as a primitive and just define it in the Cryptol prelude; this would ease the maintenance burden whenever we want to implement a new backend or extend Cryptol with new primitive types.

[yav]

I am not sure that we need to support enumerations on floats, and we probably should have a separate class for them.

Half-baked idea: we've also talked about adding a class to generalize indexing, and I wonder if the enum* operations should go into that same class, with instances for all the "intergral types" (bits, Integer, and Z)

[robdockins]

OK, here's a straw proposal (names subject to bike-shedding, obviously):

• Have a Ring class, containing fromInteger, (+), (-), negate, and (*).
• Have a EuclideanDomain class containing (/), (%), (/$) and (%$). These will have "round down" and "round to zero" behavior, respectively. It will contains Integer, [n] and (maybe) Z_0.
• Define (^^) to have type {a, n} (Ring a, fin n) => a -> [n] -> a
• Remove or define lg2 at type {n} (fin n) => [n] -> [n]
• Define an Integral class. This represents base types that have an order-faithful embedding into the integers. It contains [n], Integer and Z_n. This class will have toInteger, infFrom and infFromThen, and may also be the class constraint for indexing operations.

We may also want another class for field (and field-like) division, which will contain reals, floats and Z_p (for prime p).

For backwards-compatibility, perhaps make Arith a synonym for the conjunction of EuclideanDomain and Integral

[brianhuffman]

I like most of @robdockins's proposal, except that I would prefer not to give (/$) and (%$) the same generic type as (/) and (%).

On bitvector types, (/) and (/$) (similarly (%) and (%$)) don't actually differ in their rounding modes; they differ only in whether they treat their arguments as signed. They agree with each other 100% on the common portions of their input domains. No types other than bitvectors have this signed/unsigned duality, so no types other than bitvectors should have separate signed and unsigned versions of arithmetic operators.

[robdockins]

Closed via #724