feat: add identity definition from the specs

Anoma/Identity/Object.juvix

@@ -1,28 +1,261 @@
 module Anoma.Identity.Object;
 
 import Stdlib.Prelude open;
-import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
-import Anoma.Identity.External open;
-import Anoma.Identity.Internal open;
+import Stdlib.Data.Nat as Nat open using {Nat; +; *; <=} public;
+import Stdlib.Trait.Eq as Eq open using {==} public;
+import Stdlib.Trait.Ord as Ord open using {Ordering; Equal} public;
 
---- A record describing an identity.
---- NOTE: For the private testnet, this deviates from the specs https://specs.anoma.net/v2/system_architecture/identity/identity.html.
-type Identity :=
+type OrdKey (OrdKey : Type) := mkOrdkey@{compare : OrdKey -> OrdKey -> Ordering};
+
+type HASH (OrdKeyType Hashable : Type) :=
+  mkHASH@{
+    ordKey : OrdKey OrdKeyType;
+    hash : Hashable -> OrdKeyType
+  };
+
+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
+  };
+
+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@{
-    external : ExternalIdentity;
-    internal : InternalIdentity
+    internalIdentity : InternalIdentity
+      SignerType
+      InternalSignable
+      InternalCommitment
+      DecryptorType
+      InternalPlaintext
+      InternalCiphertext;
+    externalIdentity : ExternalIdentity
+      VerifierOrdKeyType
+      VerifierType
+      ExternalSignable
+      ExternalCommitment
+      EncryptorOrdKeyType
+      EncryptorType
+      ExternalPlaintext
+      ExternalCiphertext
   };
 
-module IdentityInternal;
-  --- Compares two ;Identity; objects.
-  compare (lhs rhs : Identity) : Ordering :=
-    Ord.cmp (Identity.external lhs) (Identity.external rhs);
+type SignsFor (OrdKey VerifierType Signable Commitment Evidence : Type) :=
+  mkSignsFor@{
+    verifier : Verifier OrdKey VerifierType Signable Commitment;
+    signsFor : Evidence -> Pair VerifierType VerifierType -> Bool
+  };
 
-  --- Implements the ;Ord; trait for ;Identity;.
-  instance
-  Identity-Ord : Ord Identity := mkOrd compare;
+type ReadsFor (OrdKey EncryptorType Plaintext Ciphertext Evidence : Type) :=
+  mkReadsFor@{
+    encryptor : Encryptor OrdKey EncryptorType Plaintext Ciphertext;
+    readsFor : Evidence -> Pair EncryptorType EncryptorType -> Bool
+  };
+
+type ComposeHashable (VerifierType : Type) (MapCon : Type -> Type) :=
+  mkComposeHashable@{
+    threshold : Nat;
+    weights : MapCon (Pair Nat VerifierType)
+  };
+
+type ThresholdCompose (OrdKey : Type) (MapCon : Type
+  -> Type) (VerifierType Signable Commitment SignerType VerifierHashOrdKeyType : Type) :=
+  mkThresholdCompose@{
+    map : OrdMap OrdKey MapCon;
+    underlyingVerifier : Verifier OrdKey VerifierType Signable Commitment;
+    underlyingSigner : Signer SignerType Signable Commitment;
+    verifierHash : HASH VerifierHashOrdKeyType (ComposeHashable VerifierType MapCon);
+    sign : MapCon SignerType -> Signable -> MapCon Commitment;
+    verify : ComposeHashable VerifierType MapCon -> Signable -> MapCon Commitment -> Bool;
+    signerCompose : List (Pair VerifierType SignerType) -> MapCon SignerType;
+    verifierCompose : Nat -> List (Pair Nat VerifierType) -> ComposeHashable VerifierType MapCon;
+    verifierAnd : VerifierType -> VerifierType -> ComposeHashable VerifierType MapCon;
+    verifierOr : VerifierType -> VerifierType -> ComposeHashable VerifierType MapCon
+  };
+
+projectVerifier
+  {MapCon : Type -> Type}
+  {OrdKey VerifierType Signable Commitment SignerType VerifierHashOrdKeyType : Type}
+  (tc : ThresholdCompose
+    OrdKey
+    MapCon
+    VerifierType
+    Signable
+    Commitment
+    SignerType
+    VerifierHashOrdKeyType)
+  : Verifier
+    VerifierHashOrdKeyType
+    (ComposeHashable VerifierType MapCon)
+    Signable
+    (MapCon Commitment) :=
+  mkVerifier@{
+    verify := ThresholdCompose.verify tc;
+    verifierHash := ThresholdCompose.verifierHash tc
+  };
+
+ThresholdComposeFunctor
+  {MapCon : Type -> Type}
+  {OrdKey VerifierType Signable Commitment SignerType VerifierHashOrdKeyType : Type}
+  (verifier : Verifier OrdKey VerifierType Signable Commitment)
+  (signer : Signer SignerType Signable Commitment)
+  (mapIn : OrdMap OrdKey MapCon)
+  (thresholdComposeHash : HASH VerifierHashOrdKeyType (ComposeHashable VerifierType MapCon))
+  : ThresholdCompose
+    OrdKey
+    MapCon
+    VerifierType
+    Signable
+    Commitment
+    SignerType
+    VerifierHashOrdKeyType :=
+  mkThresholdCompose@{
+    map := mapIn;
+    underlyingVerifier := verifier;
+    underlyingSigner := signer;
+    verifierHash := thresholdComposeHash;
+    sign := \ {s m := OrdMap.map map \ {i := Signer.sign underlyingSigner i m} s};
+    verify :=
+      \ {| (mkComposeHashable t ws) s c :=
+        t
+          <= OrdMap.foldl
+            map
+            \ {(x, y) := x + y}
+            0
+            (OrdMap.intersectWith
+              map
+              \ {| ((w, v), x) := ite (Verifier.verify underlyingVerifier v s x) w 0}
+              (ws, c))};
+    signerCompose :=
+      \ {l :=
+        foldl
+          \ {m (v, s) :=
+            OrdMap.insert map (m, HASH.hash (Verifier.verifierHash underlyingVerifier) v, s)}
+          (OrdMap.empty map)
 
-  --- Implements the ;Eq; trait for ;Identity;.
-  instance
-  Identity-Eq : Eq Identity := fromOrdToEq;
-end;
+          l};
+    verifierCompose :=
+      \ {threshold weights :=
+        mkComposeHashable
+          threshold
+          (foldl
+            \ {m (w, v) :=
+              OrdMap.insert map (m, HASH.hash (Verifier.verifierHash underlyingVerifier) v, w, v)}
+            (OrdMap.empty map)
+            weights)};
+    verifierAnd := \ {x y := verifierCompose 2 [1, x; 1, y]};
+    verifierOr := \ {x y := verifierCompose 1 [1, x; 1, y]}
+  };
+
+type ThresholdComposeSignsFor (OrdKey VerifierType Signable Commitment Evidence : Type) (MapCon : Type
+  -> Type) VerifierHashOrdKeyType :=
+  mkThresholdComposeSignsFor@{
+    underlyingSignsFor : SignsFor OrdKey VerifierType Signable Commitment Evidence;
+    verifier : ThresholdCompose
+      OrdKey
+      MapCon
+      VerifierType
+      Signable
+      Commitment
+      VerifierType
+      VerifierHashOrdKeyType;
+    signsFor : Evidence
+      -> Pair (ComposeHashable VerifierType MapCon) (ComposeHashable VerifierType MapCon)
+      -> Bool
+  };
+
+projectSignsFor
+  {OrdKey VerifierType Signable Commitment Evidence : Type}
+  {MapCon : Type -> Type}
+  {VerifierHashOrdKeyType : Type}
+  (tc : ThresholdComposeSignsFor
+    OrdKey
+    VerifierType
+    Signable
+    Commitment
+    Evidence
+    MapCon
+    VerifierHashOrdKeyType)
+  : SignsFor
+    VerifierHashOrdKeyType
+    (ComposeHashable VerifierType MapCon)
+    Signable
+    (MapCon Commitment)
+    Evidence :=
+  mkSignsFor@{
+    verifier := projectVerifier (ThresholdComposeSignsFor.verifier tc);
+    signsFor := ThresholdComposeSignsFor.signsFor tc
+  };
+
+ThresholdComposeSignsForFunctor
+  {OrdKey VerifierType Signable Commitment Evidence : Type}
+  {MapCon : Type -> Type}
+  {VerifierHashOrdKeyType : Type}
+  (S : SignsFor OrdKey VerifierType Signable Commitment Evidence)
+  (signer : Signer VerifierType Signable Commitment)
+  (map : OrdMap OrdKey MapCon)
+  (thresholdComposeHash : HASH VerifierHashOrdKeyType (ComposeHashable VerifierType MapCon))
+  : ThresholdComposeSignsFor
+    OrdKey
+    VerifierType
+    Signable
+    Commitment
+    Evidence
+    MapCon
+    VerifierHashOrdKeyType :=
+  mkThresholdComposeSignsFor@{
+    underlyingSignsFor := S;
+    verifier :=
+      ThresholdComposeFunctor
+        (SignsFor.verifier underlyingSignsFor)
+        signer
+        map
+        thresholdComposeHash;
+    signsFor :=
+      \ {e (mkComposeHashable t0 w0, mkComposeHashable t1 w1) :=
+        OrdMap.all
+          map
+          \ {(w, v) :=
+            w * t1
+              <= OrdMap.foldl
+                  map
+                  \ {((x, v1), s) := ite (SignsFor.signsFor underlyingSignsFor e (v, v1)) (x + s) s}
+                  0
+                  w1
+                * t0}
+          w0}
+  };