Safe Haskell	Safe-Inferred
Language	Haskell2010

ZkFold.Symbolic.Algorithms.Hash.Blake2b

Synopsis

pow2 :: forall a. FromConstant Natural a => Natural -> a
shiftUIntR :: forall b. Symbolic b => UInt 64 Auto b -> Natural -> UInt 64 Auto b
shiftUIntL :: forall b. Symbolic b => UInt 64 Auto b -> Natural -> UInt 64 Auto b
xorUInt :: forall c. Symbolic c => UInt 64 Auto c -> UInt 64 Auto c -> UInt 64 Auto c
data Blake2bCtx c = Blake2bCtx {
- h :: Vector (UInt 64 Auto c)
- m :: Vector (UInt 64 Auto c)
- t :: (Natural, Natural)
}
rotr64 :: Symbolic c => (UInt 64 Auto c, Natural) -> UInt 64 Auto c
b2b_g :: forall c. Symbolic c => Vector (UInt 64 Auto c) -> (Int, Int, Int, Int, UInt 64 Auto c, UInt 64 Auto c) -> Vector (UInt 64 Auto c)
blake2b_compress :: forall c. Symbolic c => Blake2bCtx c -> Bool -> Vector (UInt 64 Auto c)
blake2b' :: forall bb' kk' ll' nn' c. (Symbolic c, KnownNat bb', KnownNat kk', KnownNat ll', KnownNat nn') => [Vector (UInt 64 Auto c)] -> ByteString (8 * nn') c
type ExtensionBits inputLen = 8 * (128 - Mod inputLen 128)
type ExtendedInputByteString inputLen c = ByteString ((8 * inputLen) + ExtensionBits inputLen) c
withExtensionBits :: forall n {r}. KnownNat n => (KnownNat (ExtensionBits n) => r) -> r
withExtendedInputByteString :: forall n {r}. KnownNat n => (KnownNat ((8 * n) + ExtensionBits n) => r) -> r
with8nLessExt :: forall n {r}. KnownNat n => ((8 * n) <= ((8 * n) + ExtensionBits n) => r) -> r
with8n :: forall n {r}. KnownNat n => (KnownNat (8 * n) => r) -> r
blake2bDivConstraint :: forall n. Dict ((Div ((8 * n) + ExtensionBits n) 64 * 64) ~ ((8 * n) + ExtensionBits n))
withBlake2bDivConstraint :: forall n {r}. ((Div ((8 * n) + ExtensionBits n) 64 * 64) ~ ((8 * n) + ExtensionBits n) => r) -> r
withConstraints :: forall n {r}. KnownNat n => ((KnownNat (8 * n), KnownNat (ExtensionBits n), KnownNat ((8 * n) + ExtensionBits n), (8 * n) <= ((8 * n) + ExtensionBits n), (Div ((8 * n) + ExtensionBits n) 64 * 64) ~ ((8 * n) + ExtensionBits n)) => r) -> r
blake2b :: forall keyLen inputLen outputLen c n. (Symbolic c, KnownNat keyLen, KnownNat inputLen, KnownNat outputLen, n ~ ((8 * inputLen) + ExtensionBits inputLen)) => Natural -> ByteString (8 * inputLen) c -> ByteString (8 * outputLen) c
blake2b_224 :: forall inputLen c. (Symbolic c, KnownNat inputLen) => ByteString (8 * inputLen) c -> ByteString 224 c
blake2b_256 :: forall inputLen c. (Symbolic c, KnownNat inputLen) => ByteString (8 * inputLen) c -> ByteString 256 c
blake2b_512 :: forall inputLen c. (Symbolic c, KnownNat inputLen) => ByteString (8 * inputLen) c -> ByteString 512 c

Documentation

pow2 :: forall a. FromConstant Natural a => Natural -> a Source #

BLAKE2b Cryptographic hash. Reference: https://tools.ietf.org/html/rfc7693

shiftUIntR :: forall b. Symbolic b => UInt 64 Auto b -> Natural -> UInt 64 Auto b Source #

shiftUIntL :: forall b. Symbolic b => UInt 64 Auto b -> Natural -> UInt 64 Auto b Source #

xorUInt :: forall c. Symbolic c => UInt 64 Auto c -> UInt 64 Auto c -> UInt 64 Auto c Source #

data Blake2bCtx c Source #

state context

Constructors

Blake2bCtx
Fields h :: Vector (UInt 64 Auto c) m :: Vector (UInt 64 Auto c) t :: (Natural, Natural)

rotr64 :: Symbolic c => (UInt 64 Auto c, Natural) -> UInt 64 Auto c Source #

Cyclic right rotation.

b2b_g :: forall c. Symbolic c => Vector (UInt 64 Auto c) -> (Int, Int, Int, Int, UInt 64 Auto c, UInt 64 Auto c) -> Vector (UInt 64 Auto c) Source #

Little-endian byte access.

blake2b_compress :: forall c. Symbolic c => Blake2bCtx c -> Bool -> Vector (UInt 64 Auto c) Source #

Compression function. "last" flag indicates the last block.

blake2b' :: forall bb' kk' ll' nn' c. (Symbolic c, KnownNat bb', KnownNat kk', KnownNat ll', KnownNat nn') => [Vector (UInt 64 Auto c)] -> ByteString (8 * nn') c Source #

type ExtensionBits inputLen = 8 * (128 - Mod inputLen 128) Source #

type ExtendedInputByteString inputLen c = ByteString ((8 * inputLen) + ExtensionBits inputLen) c Source #

withExtensionBits :: forall n {r}. KnownNat n => (KnownNat (ExtensionBits n) => r) -> r Source #

withExtendedInputByteString :: forall n {r}. KnownNat n => (KnownNat ((8 * n) + ExtensionBits n) => r) -> r Source #

with8nLessExt :: forall n {r}. KnownNat n => ((8 * n) <= ((8 * n) + ExtensionBits n) => r) -> r Source #

with8n :: forall n {r}. KnownNat n => (KnownNat (8 * n) => r) -> r Source #

blake2bDivConstraint :: forall n. Dict ((Div ((8 * n) + ExtensionBits n) 64 * 64) ~ ((8 * n) + ExtensionBits n)) Source #

withBlake2bDivConstraint :: forall n {r}. ((Div ((8 * n) + ExtensionBits n) 64 * 64) ~ ((8 * n) + ExtensionBits n) => r) -> r Source #

withConstraints :: forall n {r}. KnownNat n => ((KnownNat (8 * n), KnownNat (ExtensionBits n), KnownNat ((8 * n) + ExtensionBits n), (8 * n) <= ((8 * n) + ExtensionBits n), (Div ((8 * n) + ExtensionBits n) 64 * 64) ~ ((8 * n) + ExtensionBits n)) => r) -> r Source #

blake2b :: forall keyLen inputLen outputLen c n. (Symbolic c, KnownNat keyLen, KnownNat inputLen, KnownNat outputLen, n ~ ((8 * inputLen) + ExtensionBits inputLen)) => Natural -> ByteString (8 * inputLen) c -> ByteString (8 * outputLen) c Source #

blake2b_224 :: forall inputLen c. (Symbolic c, KnownNat inputLen) => ByteString (8 * inputLen) c -> ByteString 224 c Source #

Hash a ByteString using the Blake2b-224 hash function.

blake2b_256 :: forall inputLen c. (Symbolic c, KnownNat inputLen) => ByteString (8 * inputLen) c -> ByteString 256 c Source #

Hash a ByteString using the Blake2b-256 hash function.

blake2b_512 :: forall inputLen c. (Symbolic c, KnownNat inputLen) => ByteString (8 * inputLen) c -> ByteString 512 c Source #

Hash a ByteString using the Blake2b-256 hash function.