    -- |
    -- 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 :: forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Maybe (IsDiv8 n n :~: 'True)
    isDivisibleBy8 proxy n
    n
        | Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    mod (proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy n
    n) Integer
    8 Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 = (IsDiv8 n n :~: 'True) -> Maybe (IsDiv8 n n :~: 'True)
    forall a. a -> Maybe a
    Just ((ZonkAny 3 :~: ZonkAny 3) -> IsDiv8 n n :~: 'True
    forall a b. a -> b
    unsafeCoerce ZonkAny 3 :~: ZonkAny 3
    forall {k} (a :: k). a :~: a
    Refl)
        | Bool
    otherwise             = Maybe (IsDiv8 n n :~: 'True)
    forall a. Maybe a
    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 :: forall (value :: Nat) (bound :: Nat) (proxy :: Nat -> *)
           (proxy' :: Nat -> *).
    (KnownNat value, KnownNat bound) =>
    proxy value -> proxy' bound -> Maybe ((value <=? bound) :~: 'True)
    isAtMost proxy value
    x proxy' bound
    y
        | proxy value -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy value
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= proxy' bound -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy' bound
    y  = (OrdCond (CmpNat value bound) 'True 'True 'False :~: 'True)
    -> Maybe
         (OrdCond (CmpNat value bound) 'True 'True 'False :~: 'True)
    forall a. a -> Maybe a
    Just ((ZonkAny 1 :~: ZonkAny 1)
    -> OrdCond (CmpNat value bound) 'True 'True 'False :~: 'True
    forall a b. a -> b
    unsafeCoerce ZonkAny 1 :~: ZonkAny 1
    forall {k} (a :: k). a :~: a
    Refl)
        | Bool
    otherwise             = Maybe (OrdCond (CmpNat value bound) 'True 'True 'False :~: 'True)
    Maybe (OrdCond (Compare value bound) 'True 'True 'False :~: 'True)
    forall a. Maybe a
    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 :: forall (value :: Nat) (bound :: Nat) (proxy :: Nat -> *)
           (proxy' :: Nat -> *).
    (KnownNat value, KnownNat bound) =>
    proxy value -> proxy' bound -> Maybe ((bound <=? value) :~: 'True)
    isAtLeast = (proxy' bound
     -> proxy value
     -> Maybe
          (OrdCond (CmpNat bound value) 'True 'True 'False :~: 'True))
    -> proxy value
    -> proxy' bound
    -> Maybe
         (OrdCond (CmpNat bound value) 'True 'True 'False :~: 'True)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip proxy' bound
    -> proxy value
    -> Maybe
         (OrdCond (CmpNat bound value) 'True 'True 'False :~: 'True)
    proxy' bound
    -> proxy value
    -> Maybe
         (OrdCond (Compare bound value) 'True 'True 'False :~: 'True)
    forall (value :: Nat) (bound :: Nat) (proxy :: Nat -> *)
           (proxy' :: Nat -> *).
    (KnownNat value, KnownNat bound) =>
    proxy value -> proxy' bound -> Maybe ((value <=? bound) :~: 'True)
    isAtMost