module arch.node.types.identities;

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

Signable : Type := ByteString;

Plaintext : Type := ByteString;

Ciphertext : Type := ByteString;

DecryptionKey : Type := ByteString;

SigningKey : Type := ByteString;

syntax alias ExternalID := PublicKey;
syntax alias InternalID := PrivateKey;

Identity : Type := Pair ExternalID InternalID;

syntax alias Commitment := Signature;

axiom emptyCommitment : Commitment;

syntax alias NodeID := ExternalID;
syntax alias TopicID := ExternalID;
syntax alias PublisherID := ExternalID;
syntax alias DomainID := ExternalID;
syntax alias MemberID := ExternalID;
syntax alias ChunkID := Digest;
syntax alias EngineName := String;
syntax alias ExternalIdentity := EngineName;

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

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

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

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

type IDParams :=
  | Ed25519
  | Secp256k1
  | BLS;

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

type Capabilities :=
  | CapabilityCommit
  | CapabilityDecrypt
  | CapabilityCommitAndDecrypt;

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

axiom IdentityNameCmpDummy : IdentityName -> IdentityName -> Ordering;

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

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

axiom ReadsForCmpDummy : ReadsForEvidence -> ReadsForEvidence -> Ordering;

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

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

axiom SignsForCmpDummy : SignsForEvidence -> SignsForEvidence -> Ordering;

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

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

axiom IdentityNameEvidenceCmpDummy
  : IdentityNameEvidence -> IdentityNameEvidence -> Ordering;

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

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

syntax alias TxFingerprint := Nat;

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

syntax alias NarwhalBlock := String;
syntax alias BatchNumber := Nat;
syntax alias WallClockTime := Nat;

-- Map each key to its shard
axiom keyToShard {KVSKey} : KVSKey -> EngineID;