Add explicit types for signed/unsigned words

[yav]

Currently Cryptol uses sequences of bits to represent signed and unsigned numbers, and relies on separate operators when semantics differ between signed and unsigned values. It might be useful to add explicit signed/unsigned word types, and ose the types to determine the correct operator instead (i.e., mirror what most other programming languages do).

Implementing this should not require a lot of changes, as these new types can coexist with existing types, and we could relevant coercion functions to/from bit sequences.

[RyanGlScott]

Just to make sure I understand what is being proposed here, you want to introduce something like:

primitive Unsigned : # -> *
primitive Signed : # -> *

So that you can write types like Unsigned 8 or Signed 8?

Is the idea to introduce separate operators that are specific to Unsigned/Signed, or is the plan to allow re-using existing operators? For instance, could you use the Cmp operators ((<=), (<), etc.) on both Unsigned and Signed, and each one would use unsigned/signed comparisons? (The documentation for (<=) et al. currently indicates that they always use unsigned arithmetic, but obviously this wouldn't be true if we allowed to use them for Signed values.)

[yav]

Yes, something like that. Not sure if they need to be primitives, and what they should be called. The idea is to introduce additional instances for these types, so that one can use the ordinary operators.

Btw if the docs say the <= always use unsigned arithmetic, we should fix them---that's only true for sequences of bits, other types (e.g., integers, rationsal, float) can be compared and they can be signed.

[RyanGlScott]

OK. I suppose then we would just give Unsigned a Cmp instance (but not a SignedCmp instance) and give Signed a SignedCmp instance (but not a Cmp instance).

Btw if the docs say the <= always use unsigned arithmetic

Ah, sorry, I didn't read the surrounding context:

cryptol/lib/Cryptol.cry

Lines 571 to 576 in 82a1fe8

	/**
	* Less-than or equal of two comparable arguments.
	*
	* Bitvectors are compared using unsigned arithmetic.
	*/
	primitive (<=) : {a} (Cmp a) => a -> a -> Bit

This does specify that this applies to bitvectors specifically.

[sauclovian-g]

It would also be nice to have this for SAW, because currently we're in a position where it's easy to get accidental signedness errors handling code in languages that do distinguish signed and unsigned. See GaloisInc/saw-script#3115