-- |
-- Module      : Crypto.Number.Nat
-- License     : BSD-style
-- Maintainer  : Vincent Hanquez <[email protected]>
-- 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
    | forall a. Integral a => a -> a -> a
mod (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy n
n) Integer
8 forall a. Eq a => a -> a -> Bool
== Integer
0 = forall a. a -> Maybe a
Just (forall a b. a -> b
unsafeCoerce forall {k} (a :: k). a :~: a
Refl)
    | Bool
otherwise             = 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
    | forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy value
x forall a. Ord a => a -> a -> Bool
<= forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy' bound
y  = forall a. a -> Maybe a
Just (forall a b. a -> b
unsafeCoerce forall {k} (a :: k). a :~: a
Refl)
    | Bool
otherwise             = 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (value :: Nat) (bound :: Nat) (proxy :: Nat -> *)
       (proxy' :: Nat -> *).
(KnownNat value, KnownNat bound) =>
proxy value -> proxy' bound -> Maybe ((value <=? bound) :~: 'True)
isAtMost