Cryptographic primitives¶
PublicKey¶
Public key for public-key cryptography.
type PublicKey := | Curve25519PubKey ByteString;
publicKeyEq : PublicKey -> PublicKey -> Bool
| (PublicKey.Curve25519PubKey s1) (PublicKey.Curve25519PubKey s2) := s1 == s2;
instance
PublicKeyEq : Eq PublicKey :=
Eq.mk@{
isEqual := publicKeyEq;
};
instance
PublicKeyOrd : Ord PublicKey :=
Ord.mk@{
compare := \{_ _ := Equal};
};
PrivateKey¶
Private key for public-key cryptography.
type PrivateKey := | Curve25519PrivKey ByteString;
instance
PrivateKeyOrd : Ord PrivateKey :=
Ord.mk@{
compare := \{_ _ := Equal};
};
SecretKey¶
Secret key for secret-key cryptography.
type SecretKey := | ChaCha20Key;
Signature¶
Cryptographic signature.
type Signature := | Ed25519Signature ByteString;
Digest¶
Message digest. Output of a cryptographic hash function.
type Digest := | Blake3Digest ByteString;