Skip to content
Juvix imports

module arch.node.types.crypto;

import prelude open;

Cryptographic primitives

PublicKey

Public key for public-key cryptography.

type PublicKey := | Curve25519PubKey ByteString;
Auxiliary Juvix code

deriving instance
PublicKeyEq : Eq PublicKey;

instance
PublicKeyOrd : Ord PublicKey :=
mkOrd@{
cmp := \{ := Equal};
};

PrivateKey

PrivateKey

Private key for public-key cryptography.

type PrivateKey := | Curve25519PrivKey ByteString;
Auxiliary Juvix code

deriving instance
PrivateKeyEq : Eq PrivateKey;

instance
PrivateKeyOrd : Ord PrivateKey :=
mkOrd@{
cmp := \{ := Equal};
};

SecretKey

Secret key for secret-key cryptography.

type SecretKey := | ChaCha20Key;
Auxiliary Juvix code

deriving instance
SecretKeyEq : Eq SecretKey;

deriving instance
SecretKeyOrd : Ord SecretKey;

Signature

Cryptographic signature.

type Signature := | Ed25519Signature ByteString;

Digest

Message digest. Output of a cryptographic hash function.

type Digest := | Blake3Digest ByteString;

hash

axiom hash {A} : A -> Digest;
Auxiliary Juvix code

deriving instance
DigestEq : Eq Digest;

instance
DigestOrd : Ord Digest :=
mkOrd@{
cmp := \{(Blake3Digest a) (Blake3Digest b) := Equal};
};