Add module Crypto.Number.Nat

This new module exposes type constraints required by some hash
algorithms and provides functions to check whether the constraints are
satisfied with runtime values.

Resolves #256.

Crypto/Internal/Nat.hs

@@ -9,6 +9,7 @@ module Crypto.Internal.Nat
     , type IsAtMost, type IsAtLeast
     , byteLen
     , integralNatVal
+    , type IsDiv8
     , type Div8
     , type Mod8
     ) where
@@ -207,4 +208,6 @@ type family Mod8 (n :: Nat) where
     Mod8 63 = 7
     Mod8 n = Mod8 (n - 64)
 
+-- | ensure the given `bitlen` is divisible by 8
+--
 type IsDivisibleBy8 bitLen = IsDiv8 bitLen bitLen ~ 'True

Crypto/Number/Nat.hs

@@ -0,0 +1,63 @@
+-- |
+-- Module      : Crypto.Number.Nat
+-- License     : BSD-style
+-- Maintainer  : Vincent Hanquez <vincent@snarc.org>
+-- Stability   : experimental
+-- Portability : Good
+--
+-- 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.
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+module Crypto.Number.Nat
+    ( type IsDivisibleBy8
+    , type IsAtMost, type IsAtLeast
+    , isDivisibleBy8
+    , isAtMost
+    , isAtLeast
+    ) where
+
+import           Data.Type.Equality
+import           GHC.TypeLits
+import           Unsafe.Coerce (unsafeCoerce)
+
+import           Crypto.Internal.Nat
+
+-- | get a runtime proof that the constraint @'IsDivisibleBy8' n@ is satified
+isDivisibleBy8 :: KnownNat n => proxy n -> Maybe (IsDiv8 n n :~: 'True)
+isDivisibleBy8 n
+    | mod (natVal n) 8 == 0 = Just (unsafeCoerce Refl)
+    | otherwise             = Nothing
+
+-- | get a runtime proof that the constraint @'IsAtMost' value bound@ is
+-- satified
+isAtMost :: (KnownNat value, KnownNat bound)
+         => proxy value -> proxy' bound -> Maybe ((value <=? bound) :~: 'True)
+isAtMost x y
+    | natVal x <= natVal y  = Just (unsafeCoerce Refl)
+    | otherwise             = Nothing
+
+-- | get a runtime proof that the constraint @'IsAtLeast' value bound@ is
+-- satified
+isAtLeast :: (KnownNat value, KnownNat bound)
+          => proxy value -> proxy' bound -> Maybe ((bound <=? value) :~: 'True)
+isAtLeast = flip isAtMost

cryptonite.cabal

@@ -130,6 +130,7 @@ Library
                      Crypto.Number.F2m
                      Crypto.Number.Generate
                      Crypto.Number.ModArithmetic
+                     Crypto.Number.Nat
                      Crypto.Number.Prime
                      Crypto.Number.Serialize
                      Crypto.Number.Serialize.Internal