Cryptol.TypeCheck.Solver.InfNat

This module defines natural numbers with an additional infinity element, and various arithmetic operators on them.

Documentation

data Nat'

Natural numbers with an infinity element

Constructors

Nat Integer

Inf

Instances

Eq Nat'

Ord Nat'

Show Nat'

fromNat :: Nat' -> Maybe Integer

nAdd :: Nat' -> Nat' -> Nat'

nMul :: Nat' -> Nat' -> Nat'

Some algerbaic properties of interest:

1 * x = x
x * (y * z) = (x * y) * z
0 * x = 0
x * y = y * x
x * (a + b) = x * a + x * b

nExp :: Nat' -> Nat' -> Nat'

Some algeibraic properties of interest:

x ^ 0        = 1
x ^ (n + 1)  = x * (x ^ n)
x ^ (m + n)  = (x ^ m) * (x ^ n)
x ^ (m * n)  = (x ^ m) ^ n

nMin :: Nat' -> Nat' -> Nat'

nMax :: Nat' -> Nat' -> Nat'

nSub :: Nat' -> Nat' -> Maybe Nat'

nSub x y = Just z iff z is the unique value such that Add y z = Just x.

nDiv :: Nat' -> Nat' -> Maybe Nat'

Rounds down.

y * q + r = x
x / y     = q with remainder r
0 <= r && r < y

We don't allow Inf in the first argument for two reasons: 1. It matches the behavior of nMod, 2. The well-formedness constraints can be expressed as a conjunction.

nMod :: Nat' -> Nat' -> Maybe Nat'

nLg2 :: Nat' -> Nat'

Rounds up. lg2 x = y, iff y is the smallest number such that x <= 2 ^ y

nWidth :: Nat' -> Nat'

nWidth n is number of bits needed to represent all numbers from 0 to n, inclusive. nWidth x = nLg2 (x + 1).

nLenFromThen :: Nat' -> Nat' -> Nat' -> Maybe Nat'

nLenFromThenTo :: Nat' -> Nat' -> Nat' -> Maybe Nat'

genLog :: Integer -> Integer -> Maybe (Integer, Bool)

Compute the logarithm of a number in the given base, rounded down to the closest integer. The boolean indicates if we the result is exact (i.e., True means no rounding happened, False means we rounded down). The logarithm base is the second argument.

widthInteger :: Integer -> Integer

Compute the number of bits required to represent the given integer.