feat: add identity definition from the specs

Anoma/Identity.juvix

@@ -3,18 +3,71 @@ module Anoma.Identity;
 import Stdlib.Prelude open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
 
---- A fixed-size data type describing an external identity.
-axiom ExternalIdentity : Type;
+type OrdKey (OrdKey : Type) := mkOrdkey {compare : OrdKey -> OrdKey -> Ordering};
 
-module ExternalIdentityInternal;
-  --- Compares two ;ExternalIdentity; objects.
-  axiom compare : (lhs rhs : ExternalIdentity) -> Ordering;
+type HASH (OrdKeyType Hashable : Type) :=
+  mkHASH {
+    ordKey : OrdKey OrdKeyType;
+    hash : Hashable -> OrdKeyType
+  };
 
-  --- Implements the ;Ord; trait for ;ExternalIdentity;.
-  instance
-  ExternalIdentity-Ord : Ord ExternalIdentity := mkOrd compare;
+type OrdMap (OrdKeyType : Type) (MapCon : Type -> Type) :=
+  mkOrdMap {
+    ordKey : OrdKey OrdKeyType;
+    empty : {a : Type} -> MapCon a;
+    map : {a b : Type} -> (a -> b) -> MapCon a -> MapCon b;
+    insert : {a : Type} -> Pair (MapCon a) (Pair OrdKeyType a) -> MapCon a;
+    foldl : {a b : Type} -> (Pair a b -> b) -> b -> MapCon a -> b;
+    intersectWith : {a b c : Type} -> (Pair a b -> c) -> Pair (MapCon a) (MapCon b) -> MapCon c;
+    all : {a : Type} -> (a -> Bool) -> MapCon a -> Bool
+  };
 
-  --- Implements the ;Eq; trait for ;ExternalIdentity;.
-  instance
-  ExternalIdentity-Eq : Eq ExternalIdentity := fromOrdToEq;
-end;
+type Signer (SignerType Signable Commitment : Type) :=
+  mkSigner {sign : SignerType -> Signable -> Commitment};
+
+type Decryptor (DecryptorType Plaintext Ciphertext : Type) :=
+  mkDecryptor {decrypt : DecryptorType -> Ciphertext -> Maybe Plaintext};
+
+type InternalIdentity (SignerType Signable Commitment DecryptorType Plaintext Ciphertext : Type) :=
+  mkInternalIdentity {
+    signer : Signer SignerType Signable Commitment;
+    decryptor : Decryptor DecryptorType Plaintext Ciphertext
+  };
+
+type Verifier (OrdKey VerifierType Signable Commitment : Type) :=
+  mkVerifier {
+    verify : VerifierType -> Signable -> Commitment -> Bool;
+    verifierHash : HASH OrdKey VerifierType
+  };
+
+type Encryptor (OrdKey EncryptorType Plaintext Ciphertext : Type) :=
+  mkEncryptor {
+    encrypt : EncryptorType -> Plaintext -> Ciphertext;
+    encryptorHash : HASH OrdKey EncryptorType
+  };
+
+type ExternalIdentity (VerifierOrdKeyType VerifierType Signable Commitment EncryptorOrdKeyType EncryptorType Plaintext Ciphertext : Type) :=
+  mkExternalIdentity {
+    verifier : Verifier VerifierOrdKeyType VerifierType Signable Commitment;
+    encryptor : Encryptor EncryptorOrdKeyType EncryptorType Plaintext Ciphertext
+  };
+
+type Identity (SignerType InternalSignable InternalCommitment DecryptorType InternalCiphertext InternalPlaintext VerifierOrdKeyType VerifierType ExternalSignable ExternalCommitment EncryptorOrdKeyType EncryptorType ExternalPlaintext ExternalCiphertext : Type) :=
+  mkIdentity {
+    internalIdentity : InternalIdentity
+      SignerType
+      InternalSignable
+      InternalCommitment
+      DecryptorType
+      InternalPlaintext
+      InternalCiphertext;
+    externalIdentity : ExternalIdentity
+      VerifierOrdKeyType
+      VerifierType
+      ExternalSignable
+      ExternalCommitment
+      EncryptorOrdKeyType
+      EncryptorType
+      ExternalPlaintext
+      ExternalCiphertext
+  };