License | BSD-style |
---|---|
Maintainer | Vincent Hanquez <vincent@snarc.org> |
Stability | experimental |
Portability | Good |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
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
ensure that the type-level
parameter is applicable to the algorithm.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 Source #
ensure the given bitlen
is divisible by 8
type IsAtMost (bitlen :: Nat) (n :: Nat) = IsLE bitlen n (bitlen <=? n) ~ 'True Source #
ensure the given bitlen
is lesser or equal to n
type IsAtLeast (bitlen :: Nat) (n :: Nat) = IsGE bitlen n (n <=? bitlen) ~ 'True Source #
ensure the given bitlen
is greater or equal to n
isDivisibleBy8 :: KnownNat n => proxy n -> Maybe (IsDiv8 n n :~: 'True) Source #
get a runtime proof that the constraint
is satifiedIsDivisibleBy8
n