| License | BSD-style |
|---|---|
| Maintainer | Vincent Hanquez <vincent@snarc.org> |
| Stability | experimental |
| Portability | Good |
| Safe Haskell | None |
| Language | Haskell2010 |
Crypto.Number.Nat
Description
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
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.
Synopsis
- type IsDivisibleBy8 bitLen = IsDiv8 bitLen bitLen ~ 'True
- type IsAtMost (bitlen :: Nat) (n :: Nat) = IsLE bitlen n (bitlen <=? n) ~ 'True
- type IsAtLeast (bitlen :: Nat) (n :: Nat) = IsGE bitlen n (n <=? bitlen) ~ 'True
- isDivisibleBy8 :: KnownNat n => proxy n -> Maybe (IsDiv8 n n :~: 'True)
- isAtMost :: (KnownNat value, KnownNat bound) => proxy value -> proxy' bound -> Maybe ((value <=? bound) :~: 'True)
- isAtLeast :: (KnownNat value, KnownNat bound) => proxy value -> proxy' bound -> Maybe ((bound <=? value) :~: 'True)
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