License	BSD-style
Maintainer	Vincent Hanquez <vincent@snarc.org>
Stability	experimental
Portability	Good
Safe Haskell	None
Language	Haskell2010

Crypto.Number.Nat

Description

Numbers at type level.

This module provides extensions to GHC.TypeLits and GHC.TypeNats useful to work with cryptographic algorithms parameterized with a variable bit length. Constraints like IsDivisibleBy8 n ensure that the type-level parameter is applicable to the algorithm.

Functions are also provided to test whether constraints are satisfied from values known at runtime. The following example shows how to discharge IsDivisibleBy8 in a computation fn requiring this constraint:

withDivisibleBy8 :: Integer
                 -> (forall proxy n . (KnownNat n, IsDivisibleBy8 n) => proxy n -> a)
                 -> Maybe a
withDivisibleBy8 len fn = do
    SomeNat p <- someNatVal len
    Refl <- isDivisibleBy8 p
    pure (fn p)

Function withDivisibleBy8 above returns Nothing when the argument len is negative or not divisible by 8.

Synopsis

type IsDivisibleBy8 bitLen = IsDiv8 bitLen bitLen ~ ' True
type IsAtMost (bitlen :: Nat ) (n :: Nat ) = IsLE bitlen n (bitlen <=? n) ~ ' True
type IsAtLeast (bitlen :: Nat ) (n :: Nat ) = IsGE bitlen n (n <=? bitlen) ~ ' True
isDivisibleBy8 :: KnownNat n => proxy n -> Maybe (IsDiv8 n n :~: ' True )
isAtMost :: ( KnownNat value, KnownNat bound) => proxy value -> proxy' bound -> Maybe ((value <=? bound) :~: ' True )
isAtLeast :: ( KnownNat value, KnownNat bound) => proxy value -> proxy' bound -> Maybe ((bound <=? value) :~: ' True )

Documentation

type IsDivisibleBy8 bitLen = IsDiv8 bitLen bitLen ~ ' True Source #

ensure the given bitlen is divisible by 8

type IsAtMost (bitlen :: Nat ) (n :: Nat ) = IsLE bitlen n (bitlen <=? n) ~ ' True Source #

ensure the given bitlen is lesser or equal to n

type IsAtLeast (bitlen :: Nat ) (n :: Nat ) = IsGE bitlen n (n <=? bitlen) ~ ' True Source #

ensure the given bitlen is greater or equal to n

isDivisibleBy8 :: KnownNat n => proxy n -> Maybe (IsDiv8 n n :~: ' True ) Source #

get a runtime proof that the constraint IsDivisibleBy8 n is satified

isAtMost :: ( KnownNat value, KnownNat bound) => proxy value -> proxy' bound -> Maybe ((value <=? bound) :~: ' True ) Source #

get a runtime proof that the constraint IsAtMost value bound is satified

isAtLeast :: ( KnownNat value, KnownNat bound) => proxy value -> proxy' bound -> Maybe ((bound <=? value) :~: ' True ) Source #

get a runtime proof that the constraint IsAtLeast value bound is satified