Add `even`/`odd` functions to the Cryptol prelude

[RyanGlScott]

I propose that we add the following functions to the Cryptol prelude:

even : {a} (Integral a) => a -> Bit
odd : {a} (Integral a) => a -> Bit

These are inspired by Haskell's even and odd functions. These are useful in a variety of settings, and as evidence of this, cryptol-specs already defines its own isEven function, which has a type very similar to the one proposed for even above.

In Cryptol, the only Integral instances are [n] and Integer, so it suffices to come up with even/odd implementations for these two types. Here are some prototypes of what these might look like:

intEven : Integer -> Bit
intEven x = ~(last (fromInteger x : [1]))

intEvenAlt : Integer -> Bit
intEvenAlt x = (x % 2) == 0

intOdd : Integer -> Bit
intOdd x = last (fromInteger x : [1])

intOddAlt : Integer -> Bit
intOddAlt x = (x % 2) == 1

wordEven : {n} (fin n) => [n] -> Bit
wordEven x
  | n == 0 => True
  | n >= 1 => ~(last x)

wordEvenAlt : {n} (fin n) => [n] -> Bit
wordEvenAlt x
  | n == 0 => True
  | n == 1 => x == 0
  | n >= 2 => (x % 2) == 0

wordOdd : {n} (fin n) => [n] -> Bit
wordOdd x
  | n == 0 => False
  | n >= 1 => last x

wordOddAlt : {n} (fin n) => [n] -> Bit
wordOddAlt x
  | n == 0 => False
  | n == 1 => x == 1
  | n >= 2 => (x % 2) == 1

For each type and operation, I defined an operation that checks if the last bit is set (e.g., wordEven and intEven), as well as an alternative version that is defined in terms of modular division (e.g., wordEvenAlt and intEvenAlt). Although these definitions are equivalent, some testing suggests that the versions which check if the last bit is set are more efficient than the alternative versions. For instance, I couldn't find any SMT solver that was able to prove the following properties:

evenAltWordToInt : [64] -> Bit
property evenAltWordToInt x = wordEvenAlt x == intEvenAlt (toInteger x)

oddAltWordToInt : [64] -> Bit
property oddAltWordToInt x = wordOddAlt x == intOddAlt (toInteger x)