feat: add randomness support (#27)

* refactor: naming

* feat: add randomness support

* docs: fix typo in comment

* revert: move to applib

* Revert "revert: move to applib"

This reverts commit 852a82e.

* feat: add rand seed generation and default value

* feat: add generateNonces and remove generateRandSeed

* feat: add FixedSize trait

* feat: add convenience methods

* refactor: naming

* feat: add nonce pair function

* revert: delete outdated constant

* refactor: naming

Anoma.juvix

@@ -11,5 +11,6 @@ import Anoma.Delta as Delta public;
 import Anoma.Logic open using {Logic} public;
 import Anoma.Delta open using {Delta} public;
 import Anoma.State open public;
+import Anoma.Random open public;
 
 import Anoma.Utils as Utils public;

Anoma/Builtin/ByteArray.juvix

@@ -12,20 +12,20 @@ axiom mkByteArray : List Byte -> ByteArray;
 builtin bytearray-length
 axiom length : ByteArray -> Nat;
 
--- TODO: Everything below needs to be removed.
-syntax alias AnomaContents := Nat;
+-- TODO Should be moved into base.
+syntax alias AnomaByteArray := Nat;
 
 builtin anoma-bytearray-to-anoma-contents
-axiom toAnomaContents : ByteArray -> AnomaContents;
+axiom toAnomaByteArray : ByteArray -> AnomaByteArray;
 
 builtin anoma-bytearray-from-anoma-contents
-axiom fromAnomaContents : Nat -> AnomaContents -> ByteArray;
+axiom fromAnomaByteArray : Nat -> AnomaByteArray -> ByteArray;
 
 --- Implements the ;Ord; trait for ;ByteArray;.
 instance
 ByteArray-Ord : Ord ByteArray :=
   mkOrd@{
-    cmp := Ord.cmp on toAnomaContents;
+    cmp := Ord.cmp on toAnomaByteArray;
   };
 
 --- Implements the ;Eq; trait for ;ByteArray;.

Anoma/Builtin/System.juvix

@@ -11,12 +11,15 @@ module Internal;
   syntax alias SignedMessage := ByteArray;
 end;
 
--- TODO Add builtin.
--- builtin anoma-opaque
--- axiom AnomaOpaque : Type;
--- In the backend this can be any noun.
+-- TODO Remove.
 axiom AnomaOpaque : Type;
 
+instance
+AnomaOpaque-Ord : Ord AnomaOpaque :=
+  mkOrd@{
+    cmp := Ord.cmp on anomaEncode;
+  };
+
 --- Encodes a value into a natural number.
 builtin anoma-encode
 axiom anomaEncode : {Value : Type}
@@ -28,7 +31,7 @@ axiom anomaEncode : {Value : Type}
 --- Decodes a value from a natural number.
 builtin anoma-decode
 axiom anomaDecode : {Value : Type}
-  -- | The natural number to decode .
+  -- | The natural number to decode.
   -> Nat
   -- | The decoded value.
   -> Value;
@@ -75,8 +78,27 @@ axiom anomaVerifyWithMessage : {Message : Type}
   -- | The original message.
   -> Maybe Message;
 
-instance
-AnomaOpaque-Ord : Ord AnomaOpaque :=
-  mkOrd@{
-    cmp := Ord.cmp on anomaEncode;
-  };
+--- A type describing a pure pseudo-random number generator (PRNG).
+builtin anoma-random-generator
+axiom PseudoRandomNumberGenerator : Type;
+
+syntax alias PRNG := PseudoRandomNumberGenerator;
+
+--- Creates and initializes a pure PRNG with a seed.
+--- @param The seed.
+--- @return The initialized PRNG.
+builtin anoma-random-generator-init
+axiom pseudoRandomNumberGeneratorInit : Nat -> PRNG;
+
+--- Returns two distinct PRNGs.
+--- @param The generator to split.
+--- @return A pair of two distinct PRNGs.
+builtin anoma-random-generator-split
+axiom pseudoRandomNumberGeneratorSplit : PRNG -> Pair PRNG PRNG;
+
+--- Generates a random number and returns the a
+--- @param The number of output bytes to generate.
+--- @param The generator to use.
+--- @return A pair containing the random number and the advanced PRNG.
+builtin anoma-random-next-bytes
+axiom pseudoRandomNumberGeneratorNextBytes : Nat -> PRNG -> Pair ByteArray PRNG;

Anoma/Identity/External.juvix

@@ -2,7 +2,7 @@ module Anoma.Identity.External;
 
 import Stdlib.Prelude open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
-import Anoma.Builtin.ByteArray open using {ByteArray; toAnomaContents};
+import Anoma.Builtin.ByteArray as ByteArray open using {ByteArray};
 
 --- A fixed-size data type describing an external identity.
 type ExternalIdentity := mkExternalIdentity@{unExternalIdentity : ByteArray};
@@ -29,5 +29,5 @@ ExternalIdentity-Show : Show ExternalIdentity :=
     \{id :=
       id
         |> ExternalIdentity.unExternalIdentity
-        |> toAnomaContents
+        |> ByteArray.toAnomaByteArray
         |> natToString};

Anoma/Identity/Internal.juvix

@@ -2,7 +2,7 @@ module Anoma.Identity.Internal;
 
 import Stdlib.Prelude open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
-import Anoma.Builtin.ByteArray open using {ByteArray; toAnomaContents};
+import Anoma.Builtin.ByteArray as ByteArray open using {ByteArray};
 
 --- A fixed-size data type describing an internal identity.
 type InternalIdentity := mkInternalIdentity@{unInternalIdentity : ByteArray};
@@ -29,5 +29,5 @@ InternalIdentity-Show : Show InternalIdentity :=
     \{id :=
       id
         |> InternalIdentity.unInternalIdentity
-        |> toAnomaContents
+        |> ByteArray.toAnomaByteArray
         |> natToString};

Anoma/Random.juvix

@@ -0,0 +1,127 @@
+module Anoma.Random;
+
+import Stdlib.Prelude open;
+import Anoma.Primitives.FixedSize open;
+import Anoma.Builtin.ByteArray as ByteArray open using {ByteArray};
+import Anoma.Builtin.System as SystemBuiltins;
+import Anoma.Builtin.System open using {
+  PseudoRandomNumberGenerator;
+  PRNG;
+} public;
+import Anoma.Resource.Types open using {
+  Nonce;
+  mkNonce;
+  RandSeed;
+  mkRandSeed;
+  module RandSeed;
+};
+
+--- Creates and initializes a pure PRNG with a seed.
+--- @param seed The seed.
+--- @return The initialized PRNG.
+{-# inline: true #-}
+pseudoRandomNumberGeneratorInit (randSeed : RandSeed) : PRNG :=
+  SystemBuiltins.pseudoRandomNumberGeneratorInit (RandSeed.unRandSeed randSeed);
+
+syntax alias prngInit := pseudoRandomNumberGeneratorInit;
+
+--- Returns two distinct PRNGs.
+--- @param generator The generator to split.
+--- @return A pair of two distinct PRNGs.
+{-# inline: true #-}
+pseudoRandomNumberGeneratorSplit (generator : PRNG) : Pair PRNG PRNG :=
+  SystemBuiltins.pseudoRandomNumberGeneratorSplit generator;
+
+syntax alias prngSplit := pseudoRandomNumberGeneratorSplit;
+
+--- Generates pseudo-random bytes ;ByteArray; of the specified size and returns the updated PRNG.
+--- @param bytesSize The number of output bytes to generate.
+--- @param generator The generator to use.
+--- @return A pair containing the random number and the advanced PRNG.
+{-# inline: true #-}
+pseudoRandomNumberGeneratorNextBytes
+  (bytesSize : Nat) (generator : PRNG) : Pair ByteArray PRNG :=
+  SystemBuiltins.pseudoRandomNumberGeneratorNextBytes bytesSize generator;
+
+syntax alias prngNextBytes := pseudoRandomNumberGeneratorNextBytes;
+
+--- Generate a ;List; of `n` pseudo-random ;ByteArray;s of size `bytesSize` starting
+--- with a given `generator`.
+--- @param n The the number of nonces to generate.
+--- @param generator The generator to use.
+--- @return A pair containing the random byte arrays and the advanced PRNG.
+pseudoRandomNumberGeneratorNextNBytes
+  (n : Nat) (bytesSize : Nat) (generator : PRNG) : Pair (List ByteArray) PRNG :=
+  let
+    update (acc : Pair (List ByteArray) PRNG) : Pair (List ByteArray) PRNG :=
+      let
+        next :=
+          prngNextBytes@{
+            bytesSize;
+            generator := snd acc;
+          };
+      in fst next :: fst acc, snd next;
+  in iterate n update ([], generator);
+
+syntax alias prngNextNBytes := pseudoRandomNumberGeneratorNextNBytes;
+
+--- Generates a pseudo-random nonce ;Nonce; and returns the updated PRNG.
+--- @param generator The generator to use.
+--- @return A pair containing the random number and the advanced PRNG.
+generateNextNonce (generator : PRNG) : Pair Nonce PRNG :=
+  first@{
+    fun := ByteArray.toAnomaByteArray >> mkNonce;
+    pair :=
+      prngNextBytes@{
+        bytesSize := FixedSize.byteSize {Nonce};
+        generator;
+      };
+  };
+
+--- Generates a ;List; of pseudo-random nonces ;Nonce; and returns the updated PRNG.
+--- @param n The the number of nonces to generate.
+--- @param generator The generator to use.
+--- @return A pair containing the nonces and the advanced PRNG.
+generateNextNonces (n : Nat) (generator : PRNG) : Pair (List Nonce) PRNG :=
+  let
+    pair : Pair (List ByteArray) PRNG :=
+      prngNextNBytes@{
+        n;
+        bytesSize := FixedSize.byteSize {Nonce};
+        generator;
+      };
+    fun := ByteArray.toAnomaByteArray >> mkNonce;
+    nonces := map fun (fst pair);
+  in nonces, snd pair;
+
+--- Generates a pseudo-random nonce from a randomness seed.
+--- @param randSeed The randomness seed for the PRNG.
+--- @return The nonce.
+generateNonce (randSeed : RandSeed) : Nonce :=
+  fst
+    generateNextNonce@{
+      generator := prngInit randSeed;
+    };
+
+--- Generates a pair of pseudo-random nonces from a randomness seed.
+--- @param randSeed The randomness seed for the PRNG.
+--- @return The pair of nonces.
+generateNoncePair (randSeed : RandSeed) : Pair Nonce Nonce :=
+  let
+    nonceAndPrng := generateNextNonce (prngInit (randSeed));
+    nonce1 := fst nonceAndPrng;
+    nonce2 := fst (generateNextNonce (snd nonceAndPrng));
+  in nonce1, nonce2;
+
+--- Generates a list of pseudo-random nonces from a randomness seed.
+--- @param n The the number of nonces to generate.
+--- @param randSeed The randomness seed for the PRNG.
+--- @return The list of nonces.
+generateNonces (n : Nat) (randSeed : RandSeed) : List Nonce :=
+  fst
+    generateNextNonces@{
+      n;
+      generator := prngInit randSeed;
+    };
+
+UnusedRandSeed : RandSeed := mkRandSeed 0;

Anoma/Resource/Types.juvix

@@ -2,7 +2,7 @@ module Anoma.Resource.Types;
 
 import Stdlib.Prelude open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
-import Anoma.Builtin.ByteArray open using {ByteArray};
+import Anoma.Builtin.ByteArray open using {ByteArray; AnomaByteArray};
 import Anoma.Builtin.System open using {anomaEncode; AnomaOpaque};
 import Anoma.Primitives.FixedSize open;
 import Anoma.Utils open;
@@ -24,15 +24,15 @@ type Quantity := mkQuantity@{unQuantity : Nat};
 
 --- A fixed-size data type encoding the public commitment to the private nullifier key.
 type NullifierKeyCommitment :=
-  mkNullifierKeyCommitment@{unNullifierKeyCommitment : ByteArray};
+  mkNullifierKeyCommitment@{unNullifierKeyCommitment : AnomaByteArray};
 
 --- A fixed-size data type encoding a number to be used once ensuring that the resource commitment is unique.
---- NOTE: This should be a number having an at most negligible chance of repeating is sufficient, e.g., a pseudo-random number.
-type Nonce := mkNonce@{unNonce : Nat};
+--- NOTE: This should be a number having an at most negligible chance of repeating, e.g., a pseudo-random number.
+type Nonce := mkNonce@{unNonce : AnomaByteArray};
 
 --- 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 := mkRandSeed@{unRandSeed : Nat};
+type RandSeed := mkRandSeed@{unRandSeed : AnomaByteArray};
 
 --- The resource label type.
 type Label := mkLabel@{unLabel : Nat};

juvix.lock.yaml

@@ -1,4 +1,4 @@
-# This file was autogenerated by Juvix version 0.6.6.
+# This file was autogenerated by Juvix version 0.6.7.
 # Do not edit this file manually.
 
 version: 2