cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2016 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
- nEq :: Maybe Nat' -> Maybe Nat' -> Bool
- nGt :: Maybe Nat' -> Maybe Nat' -> Bool
- nFin :: Maybe Nat' -> Bool
- 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
- rootExact :: Integer -> Integer -> Maybe Integer
- genRoot :: Integer -> Integer -> Maybe (Integer, Bool)

# Documentation

data Nat' Source #

Natural numbers with an infinity element

Constructors

Nat Integer |
Inf |

Instances

Eq Nat' Source # |
Methods (==) :: Nat' -> Nat' -> Bool # (/=) :: Nat' -> Nat' -> Bool #
Ord Nat' Source # |
Methods compare :: Nat' -> Nat' -> Ordering # (<) :: Nat' -> Nat' -> Bool # (<=) :: Nat' -> Nat' -> Bool # (>) :: Nat' -> Nat' -> Bool # (>=) :: Nat' -> Nat' -> Bool # max :: Nat' -> Nat' -> Nat' # min :: Nat' -> Nat' -> Nat' #
Show Nat' Source # |
Methods showsPrec :: Int -> Nat' -> ShowS # show :: Nat' -> String # showList :: [Nat'] -> ShowS #
Generic Nat' Source # |
Associated Types type Rep Nat' :: * -> * # Methods from :: Nat' -> Rep Nat' x # to :: Rep Nat' x -> Nat' #
NFData Nat' Source # |
Methods rnf :: Nat' -> () #
type Rep Nat' Source # |
type Rep Nat' = D1 (MetaData "Nat'" "Cryptol.TypeCheck.Solver.InfNat" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "Nat" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer))) (C1 (MetaCons "Inf" PrefixI False) U1))

fromNat :: Nat' -> Maybe Integer Source #

nEq :: Maybe Nat' -> Maybe Nat' -> Bool Source #

nGt :: Maybe Nat' -> Maybe Nat' -> Bool Source #

nFin :: Maybe Nat' -> Bool Source #

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

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

Some algebraic 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 algebraic 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 #

`length ([ x, y .. ] : [_][w])` We don't check that the second element fits in `w` many bits as the second element may not be part of the list. For example, the length of `[ 0 .. ] : [_][0]` is `nLenFromThen 0 1 0`, which should evaluate to 1.

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

    length [ x, y .. z ]

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.

rootExact :: Integer -> Integer -> Maybe Integer Source #

Compute the exact root of a natural number. The second argument specifies which root we are computing.

genRoot :: Integer -> Integer -> Maybe (Integer, Bool) Source #

Compute the the n-th root of a natural number, rounded down to the closest natural number. The boolean indicates if the result is exact (i.e., True means no rounding was done, False means rounded down). The second argument specifies which root we are computing.