cryptol-2.7.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.TypeCheck.Solver.InfNat

Description

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

Synopsis

Documentation

data Nat' Source #

Natural numbers with an infinity element

Constructors

Nat Integer 
Inf 
Instances
Eq Nat' Source # 
Instance details

Defined in Cryptol.TypeCheck.Solver.InfNat

Methods

(==) :: Nat' -> Nat' -> Bool #

(/=) :: Nat' -> Nat' -> Bool #

Ord Nat' Source # 
Instance details

Defined in Cryptol.TypeCheck.Solver.InfNat

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 # 
Instance details

Defined in Cryptol.TypeCheck.Solver.InfNat

Methods

showsPrec :: Int -> Nat' -> ShowS #

show :: Nat' -> String #

showList :: [Nat'] -> ShowS #

Generic Nat' Source # 
Instance details

Defined in Cryptol.TypeCheck.Solver.InfNat

Associated Types

type Rep Nat' :: Type -> Type #

Methods

from :: Nat' -> Rep Nat' x #

to :: Rep Nat' x -> Nat' #

NFData Nat' Source # 
Instance details

Defined in Cryptol.TypeCheck.Solver.InfNat

Methods

rnf :: Nat' -> () #

type Rep Nat' Source # 
Instance details

Defined in Cryptol.TypeCheck.Solver.InfNat

type Rep Nat' = D1 (MetaData "Nat'" "Cryptol.TypeCheck.Solver.InfNat" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (C1 (MetaCons "Nat" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer)) :+: C1 (MetaCons "Inf" PrefixI False) (U1 :: Type -> Type))

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

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.

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

nCeilDiv msgLen blockSize computes the least n such that msgLen <= blockSize * n. It is undefined when blockSize = 0. It is also undefined when either input is infinite; perhaps this could be relaxed later.

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

nCeilMod msgLen blockSize computes the least k such that blockSize divides msgLen + k. It is undefined when blockSize = 0. It is also undefined when either input is infinite; perhaps this could be relaxed later.

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).

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.