feat: improve definitions

ARM.juvix

@@ -2,6 +2,6 @@ module ARM;
 
 import Anoma.Resource.Index as Resource public;
 import Anoma.Transaction.Index as Transaction public;
-import Anoma.Identity as Identity public;
+import Anoma.Identity.Index as Identity public;
 import Anoma.Delta as Delta public;
 import Anoma.Utils as Utils public;

Anoma/Identity/External.juvix

@@ -0,0 +1,20 @@
+module Anoma.Identity.External;
+
+import Stdlib.Prelude open;
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+
+--- A fixed-size data type describing an external identity.
+axiom ExternalIdentity : Type;
+
+module ExternalIdentityInternal;
+  --- Compares two ;ExternalIdentity; objects.
+  axiom compare : (lhs rhs : ExternalIdentity) -> Ordering;
+
+  --- Implements the ;Ord; trait for ;ExternalIdentity;.
+  instance
+  ExternalIdentity-Ord : Ord ExternalIdentity := mkOrd compare;
+
+  --- Implements the ;Eq; trait for ;ExternalIdentity;.
+  instance
+  ExternalIdentity-Eq : Eq ExternalIdentity := fromOrdToEq;
+end;

Anoma/Identity/Index.juvix

@@ -0,0 +1,5 @@
+module Anoma.Identity.Index;
+
+import Anoma.Identity.External open using {ExternalIdentity} public;
+import Anoma.Identity.Internal open using {InternalIdentity} public;
+import Anoma.Identity.Signing.Types open using {Signature; sign; verify} public;

Anoma/Identity/Internal.juvix

@@ -0,0 +1,20 @@
+module Anoma.Identity.Internal;
+
+import Stdlib.Prelude open;
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+
+--- A fixed-size data type describing an internal identity.
+axiom InternalIdentity : Type;
+
+module InternalIdentityInternal;
+  --- Compares two ;InternalIdentity; objects.
+  axiom compare : (lhs rhs : InternalIdentity) -> Ordering;
+
+  --- Implements the ;Ord; trait for ;InternalIdentity;.
+  instance
+  InternalIdentity-Ord : Ord InternalIdentity := mkOrd compare;
+
+  --- Implements the ;Eq; trait for ;InternalIdentity;.
+  instance
+  InternalIdentity-Eq : Eq InternalIdentity := fromOrdToEq;
+end;

Anoma/Identity/Signing/Types.juvix

@@ -0,0 +1,31 @@
+module Anoma.Identity.Signing.Types;
+
+import Stdlib.Prelude open;
+import Anoma.Identity.Internal open;
+import Anoma.Identity.External open;
+
+axiom Signature : Type;
+
+axiom verify : {Message : Type}
+  -> (signature : Signature)
+  -> (message : Message)
+  -> (external : ExternalIdentity)
+  -> Bool;
+
+axiom sign : {Message : Type} -> (message : Message) -> (internal : InternalIdentity) -> Signature;
+
+module NonDetached;
+  axiom SignedMessage : Type;
+
+  axiom verify : (signedMessage : SignedMessage) -> (external : ExternalIdentity) -> Bool;
+
+  axiom verifyWithMessage : {Message : Type}
+    -> (signedMessage : SignedMessage)
+    -> (external : ExternalIdentity)
+    -> Maybe Message;
+
+  axiom sign : {Message : Type}
+    -> (message : Message)
+    -> (internal : InternalIdentity)
+    -> SignedMessage;
+end;

Anoma/Identity/Types.juvix

@@ -0,0 +1,28 @@
+module Anoma.Identity.Types;
+
+import Stdlib.Prelude open;
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+import Anoma.Identity.External open;
+import Anoma.Identity.Internal open;
+
+--- 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 :=
+  mkIdentity {
+    external : ExternalIdentity;
+    internal : InternalIdentity
+  };
+
+module IdentityInternal;
+  --- Compares two ;Identity; objects.
+  compare (lhs rhs : Identity) : Ordering :=
+    Ord.cmp (Identity.external lhs) (Identity.external rhs);
+
+  --- Implements the ;Ord; trait for ;Identity;.
+  instance
+  Identity-Ord : Ord Identity := mkOrd compare;
+
+  --- Implements the ;Eq; trait for ;Identity;.
+  instance
+  Identity-Eq : Eq Identity := fromOrdToEq;
+end;

Anoma/Transaction/InformationFlow.juvix

@@ -2,7 +2,7 @@ module Anoma.Transaction.InformationFlow;
 
 import Stdlib.Prelude open;
 import Data.Set as Set open using {Set; toList; member?};
-import Anoma.Identity open using {ExternalIdentity};
+import Anoma.Identity.Index as Identity open using {ExternalIdentity};
 import Anoma.Transaction.Object open using {Transaction};
 
 --- The information flow predicate function type definition.