Crypto.Number.Nat

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.

Documentation

type IsDivisibleBy8 bitLen = IsDiv8 bitLen bitLen ~ 'True

ensure the given bitlen is divisible by 8

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

ensure the given bitlen is lesser or equal to n

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

ensure the given bitlen is greater or equal to n

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

get a runtime proof that the constraint IsDivisibleBy8 n is satified

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

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)

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