Merge branch 'instantiation/transparent' into feature/randomness

Anoma/Builtin/ByteArray.juvix

@@ -3,9 +3,6 @@ module Anoma.Builtin.ByteArray;
 import Stdlib.Prelude open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
 
-trait
-type FixedSize T := mkFixedSize@{sizeOf : Nat};
-
 builtin bytearray
 axiom ByteArray : Type;
 

Anoma/Primitives.juvix

@@ -0,0 +1,3 @@
+module Anoma.Primitives;
+
+import Anoma.Primitives.FixedSize open public;

Anoma/Primitives/FixedSize.juvix

@@ -0,0 +1,6 @@
+module Anoma.Primitives.FixedSize;
+
+import Stdlib.Prelude open;
+
+trait
+type FixedSize T := mkFixedSize@{byteSize : Nat};

Anoma/Random.juvix

@@ -1,8 +1,8 @@
 module Anoma.Random;
 
 import Stdlib.Prelude open;
+import Anoma.Primitives.FixedSize open;
 import Anoma.Builtin.ByteArray as ByteArray open using {ByteArray};
-import Anoma.Builtin.ByteArray open;
 import Anoma.Builtin.System as SystemBuiltins;
 import Anoma.Builtin.System open using {
   PseudoRandomNumberGenerator;
@@ -73,7 +73,7 @@ generateNextNonce (generator : PRNG) : Pair Nonce PRNG :=
     fun := ByteArray.toAnomaEncoded >> mkNonce;
     pair :=
       prngNextBytes@{
-        bytesSize := FixedSize.sizeOf {Nonce};
+        bytesSize := FixedSize.byteSize {Nonce};
         generator;
       };
   };
@@ -87,7 +87,7 @@ generateNextNonces (n : Nat) (generator : PRNG) : Pair (List Nonce) PRNG :=
     pair : Pair (List ByteArray) PRNG :=
       prngNextNBytes@{
         n;
-        bytesSize := FixedSize.sizeOf {Nonce};
+        bytesSize := FixedSize.byteSize {Nonce};
         generator;
       };
     fun := ByteArray.toAnomaEncoded >> mkNonce;

Anoma/Resource/Types.juvix

@@ -2,13 +2,9 @@ module Anoma.Resource.Types;
 
 import Stdlib.Prelude open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
-import Anoma.Builtin.ByteArray open using {
-  ByteArray;
-  FixedSize;
-  mkFixedSize;
-  AnomaEncoded;
-};
+import Anoma.Builtin.ByteArray open using {ByteArray; AnomaEncoded};
 import Anoma.Builtin.System open using {anomaEncode; AnomaOpaque};
+import Anoma.Primitives.FixedSize open;
 import Anoma.Utils open;
 
 --- A fixed-size data type encoding the reference to the resource logic function.
@@ -161,6 +157,11 @@ module QuantityInternal;
 end;
 
 module NullifierKeyCommitmentInternal;
+  --- Implements the ;FixedSize; trait for ;NullifierKeyCommitment;.
+  instance
+  NullifierKeyCommitment-FixedSize : FixedSize NullifierKeyCommitment :=
+    mkFixedSize 32;
+
   --- Compares two ;NullifierKeyCommitment; objects.
   compare (lhs rhs : NullifierKeyCommitment) : Ordering :=
     Ord.cmp
@@ -177,6 +178,7 @@ module NullifierKeyCommitmentInternal;
 end;
 
 module NonceInternal;
+  --- Implements the ;FixedSize; trait for ;Nonce;.
   instance
   Nonce-FixedSize : FixedSize Nonce := mkFixedSize 32;
 
@@ -194,6 +196,8 @@ module NonceInternal;
 end;
 
 module RandSeedInternal;
+  --- Implements the ;FixedSize; trait for ;RandSeed;.
+  instance
   RandSeed-FixedSize : FixedSize RandSeed := mkFixedSize 32;
 
   --- Compares two ;RandSeed; objects.
@@ -234,3 +238,20 @@ module NullifierInternal;
   instance
   Nullifier-Eq : Eq Nullifier := fromOrdToEq;
 end;
+
+module NullifierKeyInternal;
+  --- Implements the ;FixedSize; trait for ;NullifierKey;.
+  instance
+  NullifierKey-FixedSize : FixedSize NullifierKey := mkFixedSize 64;
+
+  --- Compares two ;NullifierKey; and returns their ;Ordering;.
+  compare (lhs rhs : NullifierKey) : Ordering := STILL_MISSING_ANOMA_BUILTIN;
+
+  --- Implements the ;Ord; trait for ;Nullifier;.
+  instance
+  NullifierKey-Ord : Ord NullifierKey := mkOrd compare;
+
+  --- Implements the ;Eq; trait for ;Nullifier;.
+  instance
+  NullifierKey-Eq : Eq NullifierKey := fromOrdToEq;
+end;

Anoma/Utils.juvix

@@ -11,6 +11,8 @@ UNUSED : Type := Unit;
 --- NOTE: This can be used in instantiated interfaces for type parameters that are not unknown.
 STILL_MISSING_DEFINITION : Type := Unit;
 
+MISSING_SIZE : Nat := 0;
+
 --- A placeholder for an implementation that is not required for the private testnet.
 NOT_REQUIRED : {A : Type} → A :=
   failwith "THIS IS NOT REQUIRED FOR THE PRIVATE TESTNET";