module arch.node.types.identities;

import arch.node.types.crypto open public;
import prelude open;

Types for network identities¶

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

Basic Types¶

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;

DecryptionKey¶

DecryptionKey : Type := ByteString;

SigningKey¶

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;

emptyCommitment¶

An empty commitment.

axiom emptyCommitment : Commitment;

Network Identifiers¶

NodeID¶

Cryptographic node identity.

syntax alias NodeID := ExternalID;

TopicID¶

Cryptographic topic identity.

syntax alias TopicID := ExternalID;

PublisherID¶

Cryptographic identity of a publisher in a pub/sub topic.

syntax alias PublisherID := ExternalID;

DomainID¶

Cryptographic domain identity.

syntax alias DomainID := ExternalID;

MemberID¶

Cryptographic identity of a member in a domain.

syntax alias MemberID := ExternalID;

ChunkID¶

Cryptographic content addressed hash digest of a data chunk.

syntax alias ChunkID := Digest;

Engine Related Types¶

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

isLocalEngineID¶

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

isRemoteEngineID¶

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

nameGen¶

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

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

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

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

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

axiom IdentityNameEvidenceCmpDummy
  : IdentityNameEvidence -> IdentityNameEvidence -> Ordering;

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

Ordering Aliases¶

type TransactionLabel ReadLabel WriteLabel :=
  mkTransactionLabel@{
    read : List ReadLabel;
    write : List WriteLabel;
  };

TxFingerprint¶

syntax alias TxFingerprint := Nat;

TransactionCandidate¶

type TransactionCandidate ReadLabel WriteLabel Executable :=
  mkTransactionCandidate@{
    label : TransactionLabel ReadLabel WriteLabel;
    executable : Executable;
  };

NarwhalBlock¶

syntax alias NarwhalBlock := String;

BatchNumber¶

syntax alias BatchNumber := Nat;

WallClockTime¶

syntax alias WallClockTime := Nat;

keyToShard¶

Up to v0.2, the specification assumes a fixed/static assignment from keys of the key-value storage to engine IDs of shards that are responsible for mangaging the values associated to keys.

axiom keyToShard {KVSKey} : KVSKey -> EngineID;