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;

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;

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 (eid : EngineID) : Bool :=
  case eid of
    | mkPair none _ := true
    | _ := false;

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

Engine Helper Functions¶

nameGen (str : String) (name : EngineName) (addr : EngineID) : EngineName :=
  name ++str "_" ++str str ++str "_" ++str snd 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;
    };

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¶

syntax alias KVSKey := String;

syntax alias ReadLabel := KVSKey;

syntax alias WriteLabel := KVSKey;

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

syntax alias KVSDatum := String;

syntax alias TxFingerprint := Nat;

type ProgramState :=
  mkProgramState@{
    data : ByteString;
    halted : Bool;
  };

syntax alias Executable := ByteString;

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

syntax alias NarwhalBlock := String;

syntax alias BatchNumber := Nat;

syntax alias WallClockTime := Nat;

Don't know a better place to put this.

axiom keyToShard : KVSKey -> EngineID;