Skip to content
Juvix imports 

module arch.node.types.identities;

import Stdlib.Data.String.Base open;
import Stdlib.Trait.Ord open using {Ordering; Ord; mkOrd};
import arch.node.types.crypto open;
import prelude open;

Types for network identities

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

Basic Types

ByteString

A basic type for representing binary data.

ByteString : Type := Nat;

emptyByteString : ByteString := 0;

Signable

A type representing data that can be cryptographically signed.

Signable : Type := ByteString;

Plaintext

Raw unencrypted data.

Plaintext : Type := ByteString;

Ciphertext

Encrypted data.

Ciphertext : Type := ByteString;

Cryptographic Keys

DecryptionKey : Type := ByteString;

SigningKey : Type := ByteString;

Identity Types

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.

syntax alias InternalID := PrivateKey;

Identity

A pair combining an ExternalID and an InternalID.

Identity : Type := Pair ExternalID InternalID;

Commitment

A cryptographic signature or commitment.

syntax alias Commitment := Signature;

axiom emptyCommitment : Commitment;

Network Identifiers

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 as an opaque string.

syntax alias EngineName := String;

ExternalIdentity

An alias for engine name.

syntax alias ExternalIdentity := EngineName;

EngineID

Engine instance identity combining node identity and engine name.

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);

Engine Helper Functions

nameStr (name : EngineID) : String :=
  case snd name of
    | none := ""
    | some s := s;

nameGen (str : String) (name : EngineName) (addr : EngineID) : EngineName :=
  name ++str "_" ++str str ++str "_" ++str nameStr addr;

String Comparison

axiom stringCmp : String -> String -> Ordering;

instance
StringOrd : Ord String :=
  mkOrd@{
    cmp := stringCmp
  };

Identity Parameters and Capabilities

IDParams

Supported identity parameter types.

type IDParams :=
  | Ed25519
  | Secp256k1
  | BLS;

Backend

Backend connection types.

type Backend :=
  | BackendLocalMemory
  | BackendLocalConnection {subtype : String}
  | BackendRemoteConnection {externalIdentity : ExternalIdentity};

Capabilities

Available identity capabilities.

type Capabilities :=
  | CapabilityCommit
  | CapabilityDecrypt
  | CapabilityCommitAndDecrypt;

Identity Evidence Types

IdentityName

Hierarchical identity naming structure.

type IdentityName :=
  | LocalName {name : String}
  | DotName {
      parent : ExternalIdentity;
      child : String
    };
Instances 

axiom IdentityNameCmpDummy : IdentityName -> IdentityName -> Ordering;

instance
IdentityNameOrd : Ord IdentityName :=
  mkOrd@{
    cmp := IdentityNameCmpDummy
  };

ReadsForEvidence

Evidence of read permissions between identities.

type ReadsForEvidence :=
  mkReadsForEvidence {
    fromIdentity : ExternalIdentity;
    toIdentity : ExternalIdentity;
    proof : ByteString
  };
Instances 

axiom ReadsForCmpDummy : ReadsForEvidence -> ReadsForEvidence -> Ordering;

instance
ReadsForOrd : Ord ReadsForEvidence :=
  mkOrd@{
    cmp := ReadsForCmpDummy
  };

SignsForEvidence

Evidence of signing permissions between identities.

type SignsForEvidence :=
  mkSignsForEvidence {
    fromIdentity : ExternalIdentity;
    toIdentity : ExternalIdentity;
    proof : ByteString
  };
Instances 

axiom SignsForCmpDummy : SignsForEvidence -> SignsForEvidence -> Ordering;

instance
SignsForOrd : Ord SignsForEvidence :=
  mkOrd@{
    cmp := SignsForCmpDummy
  };

IdentityNameEvidence

Evidence linking identity names to external identities.

type IdentityNameEvidence :=
  mkIdentityNameEvidence {
    identityName : IdentityName;
    externalIdentity : ExternalIdentity;
    proof : ByteString
  };
Instances 

axiom IdentityNameEvidenceCmpDummy : IdentityNameEvidence
  -> IdentityNameEvidence
  -> Ordering;

instance
IdentityNameEvidenceOrd : Ord IdentityNameEvidence :=
  mkOrd@{
    cmp := IdentityNameEvidenceCmpDummy
  };