cryptol-2.2.6: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2015 Galois, Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.TypeCheck.Solver.InfNat

Description

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

Synopsis

- data Nat'
  - = Nat Integer
  - | Inf
- fromNat :: Nat' -> Maybe Integer
- nAdd :: Nat' -> Nat' -> Nat'
- nMul :: Nat' -> Nat' -> Nat'
- nExp :: Nat' -> Nat' -> Nat'
- nMin :: Nat' -> Nat' -> Nat'
- nMax :: Nat' -> Nat' -> Nat'
- nSub :: Nat' -> Nat' -> Maybe Nat'
- nDiv :: Nat' -> Nat' -> Maybe Nat'
- nMod :: Nat' -> Nat' -> Maybe Nat'
- nLg2 :: Nat' -> Nat'
- nWidth :: Nat' -> Nat'
- nLenFromThen :: Nat' -> Nat' -> Nat' -> Maybe Nat'
- nLenFromThenTo :: Nat' -> Nat' -> Nat' -> Maybe Nat'
- genLog :: Integer -> Integer -> Maybe (Integer, Bool)
- widthInteger :: Integer -> Integer

# Documentation

data Nat' Source

Natural numbers with an infinity element

Constructors

Nat Integer |
Inf |

Instances

Eq Nat' Source |
Ord Nat' Source |
Show Nat' Source |

fromNat :: Nat' -> Maybe Integer Source

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

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

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' Source

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' Source

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

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

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

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

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' Source

nLg2 :: Nat' -> Nat' Source

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

nWidth :: Nat' -> Nat' Source

`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' Source

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

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

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 Source

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