Identities

Juvix imports

module node_architecture.types.identities;

import node_architecture.types.crypto open;
import prelude open;

Types for network identities

Types in this section are used to represent identities within the network.

ExternalID

A unique identifier, such as a public key, represented as a natural number.

syntax alias ExternalID := PublicKey;

InternalID

A unique identifier, such as a private key, used internally within the network, represented as a natural number.

syntax alias InternalID := PrivateKey;

Identity

A pair combining an ExternalID and an InternalID, representing the complete identity of an entity within the network.

Identity : Type := Pair ExternalID InternalID;

Commitment

A cryptographic signature, or commitment. Signed by an internal identity and verifiable by an external identity.

syntax alias Commitment := Signature;

NodeID

Cryptographic node identity.

syntax alias NodeID := ExternalID;

TopicID

Cryptographic topic identity.

syntax alias TopicID := ExternalID;

DomainID

Cryptographic domain identity.

syntax alias DomainID := ExternalID;

EngineName

Engine instance name. An opaque string that is unique to the local node.

syntax alias EngineName := String;

EngineID

Engine instance identity. A pair of an optional node identity (when remote) and an engine instance name (which may not be present, stands for anonymous engine).

Info

We assume that the engine instance name is unique within the node.

EngineID : Type := Pair (Option NodeID) (Option EngineName);

unknownEngineID : EngineID := mkPair none none;

isLocalEngineID (eid : EngineID) : Bool :=
  case eid of
    | mkPair none _ := true
    | _ := false;

isRemoteEngineID (eid : EngineID) : Bool := not (isLocalEngineID eid);