-- |
-- 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 :: 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 ((Any :~: Any) -> IsDiv8 n n :~: 'True
forall a b. a -> b
unsafeCoerce Any :~: Any
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 :: 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  = ((value <=? bound) :~: 'True)
-> Maybe ((value <=? bound) :~: 'True)
forall a. a -> Maybe a
Just ((Any :~: Any) -> (value <=? bound) :~: 'True
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl)
    | Bool
otherwise             = Maybe ((value <=? bound) :~: '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 :: proxy value -> proxy' bound -> Maybe ((bound <=? value) :~: 'True)
isAtLeast = (proxy' bound
 -> proxy value -> Maybe ((bound <=? value) :~: 'True))
-> proxy value
-> proxy' bound
-> Maybe ((bound <=? value) :~: 'True)
forall a b c. (a -> b -> c) -> b -> a -> c
flip proxy' bound -> proxy value -> Maybe ((bound <=? value) :~: 'True)
forall (value :: Nat) (bound :: Nat) (proxy :: Nat -> *)
       (proxy' :: Nat -> *).
(KnownNat value, KnownNat bound) =>
proxy value -> proxy' bound -> Maybe ((value <=? bound) :~: 'True)
isAtMost