Resource Machine v0.2 (#87)

* mk refactor

* style

* error message

* sync

* wip

* more types

* rc1

* update Package version

* update Helpers

* update juvix lock

* fixes

* add FixedSize Nonce

* v0.10.0-rc3

* Resource.mk

* rc 4

* rc 5

* rc 6

* use AnomaAtom rc7

* rc8

* push missing file

* rc9

* lock

* rc10

* selftag rc11

* appdata list rc12

* fixed size identities

* rc13

* update dependencies rc14

Author: janmasrovira

Anoma.juvix

@@ -1,12 +1,12 @@
 module Anoma;
 
-import Anoma.Resource open public;
 import Anoma.Identity open public;
+import Anoma.Data open public;
 import Anoma.Builtin.ByteArray open public;
 import Anoma.Delta as Delta public;
 import Anoma.Delta open using {Delta} public;
 import Anoma.Random open public;
 import Anoma.Utils as Utils public;
 import Anoma.Encode open public;
-import Anoma.State.CommitmentTree open public;
+import BaseLayer.ResourceMachine open public;
 import Anoma.Builtin.System open using {isNullifier; isCommitment} public;

Anoma/Builtin/ByteArray.juvix

@@ -1,32 +1,48 @@
 module Anoma.Builtin.ByteArray;
 
 import Stdlib.Prelude open;
+import BaseLayer.AnomaAtom open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
 
-builtin bytearray
-axiom ByteArray : Type;
+module ByteArray;
+  builtin bytearray
+  axiom ByteArray : Type;
 
-builtin bytearray-from-list-byte
-axiom mkByteArray : List Byte -> ByteArray;
+  builtin bytearray-from-list-byte
+  axiom mk : List Byte -> ByteArray;
 
-builtin bytearray-length
-axiom size : ByteArray -> Nat;
+  zero (length : Nat) : ByteArray := mk (replicate length 0x0);
 
-builtin anoma-bytearray-to-anoma-contents
-axiom toAnomaContents : ByteArray -> Nat;
+  --- The number of bytes in the ;ByteArray;
+  builtin bytearray-length
+  axiom size : ByteArray -> Nat;
 
-builtin anoma-bytearray-from-anoma-contents
-axiom fromAnomaContents : Nat -> Nat -> ByteArray;
+  builtin anoma-bytearray-to-anoma-contents
+  axiom rawToAnomaContents : ByteArray -> Nat;
+
+  toAnomaContents : ByteArray -> AnomaAtom :=
+    rawToAnomaContents >> AnomaAtom.fromNat;
+
+  builtin anoma-bytearray-from-anoma-contents
+  axiom rawFromAnomaContents (size : Nat) (contents : Nat) : ByteArray;
+
+  fromAnomaContents (size : Nat) (contents : AnomaAtom) : ByteArray :=
+    rawFromAnomaContents@{
+      size;
+      contents := AnomaAtom.toNat contents;
+    };
+end;
+
+open ByteArray using {ByteArray; fromAnomaContents; toAnomaContents} public;
 
 instance
 ByteArray-Ord : Ord ByteArray :=
   let
-    prod (b : ByteArray) : _ := size b, toAnomaContents b;
-  in mkOrd@{
-       cmp (lhs rhs : ByteArray) : Ordering := Ord.cmp (prod lhs) (prod rhs);
+    prod (b : ByteArray) : _ := ByteArray.size b, toAnomaContents b;
+  in Ord.mk@{
+       compare (lhs rhs : ByteArray) : Ordering :=
+         Ord.compare (prod lhs) (prod rhs);
      };
 
 instance
 ByteArray-Eq : Eq ByteArray := fromOrdToEq;
-
-zero (length : Nat) : ByteArray := mkByteArray (replicate length 0x0);

Anoma/Data.juvix

@@ -0,0 +1,3 @@
+module Anoma.Data;
+
+import Anoma.Data.RandSeed open public;

Anoma/Data/RandSeed.juvix

@@ -0,0 +1,33 @@
+module Anoma.Data.RandSeed;
+
+import Stdlib.Prelude open;
+import Anoma.Builtin.System open;
+import Anoma.Builtin.ByteArray open;
+import BaseLayer.AnomaAtom open;
+import Anoma.Primitives.FixedSize open;
+
+--- A fixed-size data type encoding a randomness seed.
+--- NOTE: This seed provides pseudo randomness and cannot be expected to provide true randomness.
+type RandSeed :=
+  internalMk@{
+    unRandSeed : ByteArray;
+  } with
+  toByteArray : RandSeed -> ByteArray := unRandSeed;
+  fromByteArray : ByteArray  -> RandSeed := internalMk;
+end;
+
+instance
+RandSeed-FixedSize : FixedSize RandSeed := FixedSize.mk 32;
+
+instance
+RandSeetFromNaturalI : FromNatural RandSeed :=
+  mkFromNatural@{
+    fromNat (n : Nat) : RandSeed :=
+      RandSeed.fromByteArray (fromAnomaContents (FixedSize.byteSize {RandSeed}) (AnomaAtom.fromNat n));
+  };
+
+deriving instance
+RandSeed-Ord : Ord RandSeed;
+
+deriving instance
+RandSeed-Eq : Eq RandSeed;

Anoma/Delta/Types.juvix

@@ -9,22 +9,22 @@ import BaseLayer.ResourceMachine as B;
 open B using {Delta} public;
 
 type VerifyingKey :=
-  mkVerifyingKey@{
+  mk@{
     unVerifyingKey : UNUSED;
   };
 
 type ProvingKey :=
-  mkProvingKey@{
+  mk@{
     unProvingKey : UNUSED;
   };
 
 type Instance :=
-  mkInstance@{
+  mk@{
     unInstance : UNUSED;
   };
 
 type Witness :=
-  mkWitness@{
+  mk@{
     unWitness : UNUSED;
   };
 

Anoma/Encode.juvix

@@ -3,25 +3,20 @@ module Anoma.Encode;
 import Stdlib.Prelude open;
 import Anoma.Builtin.System open;
 
-module Encode;
-  module Internal;
-    type Encoded A := mkEncoded Nat;
-  end;
-
-  open Internal using {Encoded} public;
+type Encoded A := internalMk Nat
+with
+  coerceFromNat {A} : Nat -> Encoded A := internalMk;
 
   decode {A} : (encoded : Encoded A) -> A
-    | (Internal.mkEncoded n) := builtinAnomaDecode n;
+    | (internalMk n) := builtinAnomaDecode n;
 
-  encode {A} (obj : A) : Encoded A :=
-    Internal.mkEncoded (builtinAnomaEncode obj);
+  encode {A} (obj : A) : Encoded A := internalMk (builtinAnomaEncode obj);
 
   deriving instance
   Encoded-Ord {A} : Ord (Encoded A);
 
   deriving instance
   Encoded-Eq {A} : Eq (Encoded A);
-
 end;
 
-open Encode using {Encoded; decode; encode} public;
+open Encoded using {decode; encode} public;

Anoma/Identity/External.juvix

@@ -1,21 +1,36 @@
 module Anoma.Identity.External;
 
 import Stdlib.Prelude open;
-import Anoma.Builtin.ByteArray open using {ByteArray; toAnomaContents};
+import BaseLayer.AnomaAtom open;
+import Anoma.Primitives.FixedSize open;
+import Anoma.Builtin.ByteArray open using {
+  ByteArray;
+  toAnomaContents;
+  fromAnomaContents;
+};
+
+--- A fixed-size data type describing an external identity.
+type ExternalIdentity :=
+  mk@{
+    unExternalIdentity : ByteArray;
+  }
+with
+  fromByteArray : ByteArray -> ExternalIdentity := ExternalIdentity.mk;
+
+  fromAnomaAtom : AnomaAtom -> ExternalIdentity :=
+    fromAnomaContents size >> fromByteArray;
 
-module ExternalIdentity;
-  --- A fixed-size data type describing an external identity.
-  type ExternalIdentity :=
-    mkExternalIdentity@{
-      unExternalIdentity : ByteArray;
-    };
+  instance
+  ExternalIdentity-FixedSize : FixedSize ExternalIdentity := FixedSize.mk size;
 
-  fromByteArray : ByteArray -> ExternalIdentity := mkExternalIdentity;
+  size : Nat := 32;
 
   toByteArray : ExternalIdentity -> ByteArray :=
     ExternalIdentity.unExternalIdentity;
 
-  toNat : ExternalIdentity -> Nat := toByteArray >> toAnomaContents;
+  toAnomaAtom : ExternalIdentity -> AnomaAtom := toByteArray >> toAnomaContents;
+
+  toNat : ExternalIdentity -> Nat := toAnomaAtom >> AnomaAtom.toNat;
 
   deriving instance
   ExternalIdentity-Ord : Ord ExternalIdentity;
@@ -25,7 +40,5 @@ module ExternalIdentity;
 
   instance
   ExternalIdentity-Show : Show ExternalIdentity :=
-    mkShow \{iden := "<<ExternalIdentity>>"};
+    Show.mk \{iden := "<<ExternalIdentity>>"};
 end;
-
-open ExternalIdentity using {ExternalIdentity} public;

Anoma/Identity/Internal.juvix

@@ -1,41 +1,54 @@
 module Anoma.Identity.Internal;
 
 import Stdlib.Prelude open;
+import BaseLayer.AnomaAtom open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
-import Anoma.Builtin.ByteArray open using {ByteArray; toAnomaContents};
+import Anoma.Primitives.FixedSize open;
+import Anoma.Builtin.ByteArray open using {
+  ByteArray;
+  fromAnomaContents;
+  toAnomaContents;
+};
+
+--- A fixed-size data type describing an internal identity.
+type InternalIdentity :=
+  mk@{
+    unInternalIdentity : ByteArray;
+  }
+with
+  fromByteArray : ByteArray -> InternalIdentity := InternalIdentity.mk;
+
+  fromAnomaAtom : AnomaAtom -> InternalIdentity :=
+    fromAnomaContents size >> fromByteArray;
 
-module InternalIdentity;
-  --- A fixed-size data type describing an internal identity.
-  type InternalIdentity :=
-    mkInternalIdentity@{
-      unInternalIdentity : ByteArray;
-    };
+  instance
+  InternalIdentity-FixedSize : FixedSize InternalIdentity := FixedSize.mk size;
 
-  fromByteArray : ByteArray -> InternalIdentity := mkInternalIdentity;
+  size : Nat := 32;
 
   toByteArray : InternalIdentity -> ByteArray :=
     InternalIdentity.unInternalIdentity;
 
-  toNat : InternalIdentity -> Nat := toByteArray >> toAnomaContents;
+  toAnomaAtom : InternalIdentity -> AnomaAtom := toByteArray >> toAnomaContents;
+
+  toNat : InternalIdentity -> Nat := toAnomaAtom >> AnomaAtom.toNat;
 
   --- Compares two ;InternalIdentity; objects.
   compare (lhs rhs : InternalIdentity) : Ordering :=
-    Ord.cmp
+    Ord.compare
       (InternalIdentity.unInternalIdentity lhs)
       (InternalIdentity.unInternalIdentity rhs);
 
   --- Implements the ;Ord; trait for ;InternalIdentity;.
   instance
-  InternalIdentity-Ord : Ord InternalIdentity := mkOrd compare;
+  InternalIdentity-Ord : Ord InternalIdentity := Ord.mk compare;
 
   --- Implements the ;Eq; trait for ;InternalIdentity;.
   instance
   InternalIdentity-Eq : Eq InternalIdentity := fromOrdToEq;
 end;
 
-open InternalIdentity using {InternalIdentity} public;
-
 --- The Anoma backend does not support converting natural numbers to strings
 instance
 InternalIdentity-Show : Show InternalIdentity :=
-  mkShow \{id := "<<InternalIdentity>>"};
+  Show.mk \{id := "<<InternalIdentity>>"};

Anoma/Identity/Object.juvix

@@ -8,28 +8,29 @@ 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@{
+  mk@{
     external : ExternalIdentity;
     internal : InternalIdentity;
-  };
+  }
+with
+  module Internal;
+    --- Compares two ;Identity; objects.
+    compare (lhs rhs : Identity) : Ordering :=
+      Ord.compare (Identity.external lhs) (Identity.external rhs);
 
-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 := Ord.mk compare;
 
-  --- 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;
+    --- Implements the ;Eq; trait for ;Identity;.
+    instance
+    Identity-Eq : Eq Identity := fromOrdToEq;
+  end;
 end;
 
 instance
 Identity-Show : Show Identity :=
-  mkShow
+  Show.mk
     \{id :=
       "{"
         ++str "external : "

Anoma/Identity/Signing/Types.juvix

@@ -7,7 +7,7 @@ import Anoma.Builtin.ByteArray as ByteArray open;
 import Anoma.Builtin.System as SystemBuiltins open;
 
 type Signature :=
-  mkSignature@{
+  mk@{
     unSignature : ByteArray;
   };
 
@@ -24,4 +24,4 @@ sign
     SystemBuiltins.anomaSignDetached
         message
         (InternalIdentity.toByteArray internalIdentity)
-      |> mkSignature;
+      |> Signature.mk;