module arch.node.types.identities;

import arch.node.types.crypto open public;
import arch.system.state.resource_machine.notes.nockma open;
import arch.system.state.resource_machine.notes.nockma_runnable open;

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 :=
  | LocalMemory
  | LocalConnection@{
      subtype : String;
    }
  | RemoteConnection@{
      externalIdentity : ExternalIdentity;
    };

type Capabilities :=
  | Commit
  | Decrypt
  | CommitAndDecrypt;

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

axiom IdentityNameCmpDummy : IdentityName -> IdentityName -> Ordering;

instance
IdentityNameOrd : Ord IdentityName :=
  Ord.mk@{
    compare := IdentityNameCmpDummy;
  };

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

axiom ReadsForCmpDummy : ReadsForEvidence -> ReadsForEvidence -> Ordering;

instance
ReadsForOrd : Ord ReadsForEvidence :=
  Ord.mk@{
    compare := ReadsForCmpDummy;
  };

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

axiom SignsForCmpDummy : SignsForEvidence -> SignsForEvidence -> Ordering;

instance
SignsForOrd : Ord SignsForEvidence :=
  Ord.mk@{
    compare := SignsForCmpDummy;
  };

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

axiom IdentityNameEvidenceCmpDummy
  : IdentityNameEvidence -> IdentityNameEvidence -> Ordering;

instance
IdentityNameEvidenceOrd : Ord IdentityNameEvidence :=
  Ord.mk@{
    compare := 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;
syntax alias KVSKey := Nat;
syntax alias KVSDatum := Nat;
syntax alias ProgramState := NockmaProgramState;
syntax alias Executable := Noun;