Update resource type and fix NullifierKeyCommitment.fromByteArray

Anoma/Builtin/System.juvix

@@ -99,15 +99,7 @@ axiom pseudoRandomNumberGeneratorSplit : PRNG -> Pair PRNG PRNG;
 --- @param The generator to use.
 --- @return A pair containing the random number and the advanced PRNG.
 builtin anoma-random-next-bytes
-axiom pseudoRandomNumberGeneratorNextBits : Nat -> PRNG -> Pair ByteArray 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.
-pseudoRandomNumberGeneratorNextBytes
-  (bytesSize : Nat) (prng : PRNG) : Pair ByteArray PRNG :=
-  pseudoRandomNumberGeneratorNextBits (bytesSize * 8) prng;
+axiom pseudoRandomNumberGeneratorNextBytes : (bytesSize : Nat) -> PRNG -> Pair ByteArray PRNG;
 
 builtin anoma-is-nullifier
 axiom isNullifier : Nat -> Bool;

Applib.juvix

@@ -12,7 +12,7 @@ import Anoma.Builtin.System open using {
 } public;
 
 import BaseLayer open public;
-
+import Applib.Show open public;
 import Applib.Helpers open public;
 import Applib.Identities open public;
 import Applib.Authorization as Authorization public;

Applib/Identities.juvix

@@ -16,7 +16,7 @@ module ExternalIdentity;
     (externalIdentity : ExternalIdentity) : NullifierKeyCommitment :=
     externalIdentity
       |> ExternalIdentity.toByteArray
-      |> NullifierKeyCommitment.mk;
+      |> NullifierKeyCommitment.fromByteArray;
 end;
 
 toNullifierKey (identity : Identity) : NullifierKey :=
@@ -88,7 +88,7 @@ module Universal;
   nullifierKeyCommitment : NullifierKeyCommitment :=
     externalIdentity
       |> ExternalIdentity.toByteArray
-      |> NullifierKeyCommitment.mk;
+      |> NullifierKeyCommitment.fromByteArray;
 end;
 
 module Alice;

Applib/Show.juvix

@@ -0,0 +1,25 @@
+module Applib.Show;
+
+import Stdlib.Prelude open;
+import Stdlib.Math open;
+
+--- non-builtin equivalent of ;natToString;
+terminating
+recursiveNatToString (n : Nat) : String :=
+  let
+    showDigit (d : Nat) : String :=
+      if
+        | d == 0 := "0"
+        | d == 1 := "1"
+        | d == 2 := "2"
+        | d == 3 := "3"
+        | d == 4 := "4"
+        | d == 5 := "5"
+        | d == 6 := "6"
+        | d == 7 := "7"
+        | d == 8 := "8"
+        | d == 9 := "9"
+        | else := "impossible";
+  in if
+    | n < 10 := showDigit n
+    | else := recursiveNatToString (div n 10) ++ showDigit (mod n 10);

BaseLayer/ResourceMachine.juvix

@@ -1,8 +1,9 @@
 module BaseLayer.ResourceMachine;
 
 import BaseLayer.AnomaAtom open public;
+import Applib.Show open;
 import Anoma.Encode open;
-import Stdlib.Debug.Fail open;
+import Stdlib.Debug open;
 import Anoma.Builtin.System open;
 import Anoma.Builtin.ByteArray open;
 import Stdlib.Prelude open;
@@ -207,9 +208,20 @@ with
 
   size : Nat := 32;
 
-  fromAnomaAtom : AnomaAtom -> Nonce := fromAnomaContents size >> privateMk;
+  fromAnomaAtom : AnomaAtom -> Nonce := fromAnomaContents size >> fromByteArray;
 
-  from32SizedByteArray : ByteArray -> Nonce := privateMk;
+  fromByteArray (b : ByteArray) : Nonce :=
+    if
+      | ByteArray.size b == size := privateMk b
+      | else :=
+        trace "bytearraysize: "
+          >-> trace (ByteArray.size b)
+          >-> failwith
+            ("Nonce.fromByteArray incorrect size. Was passed a bytearray with size "
+              ++ recursiveNatToString (ByteArray.size b)
+              ++ ".");
+
+  from32SizedByteArray : ByteArray -> Nonce := fromByteArray;
 
   toAnomaAtom : Nonce -> AnomaAtom
     | (privateMk nonce) := toAnomaContents nonce;
@@ -230,19 +242,40 @@ end;
 
 --- The nullifier key type describing a secret required to compute the ;Nullifier; of a resource
 -- dev: if this has to interact with anoma, replace ByteArray with AnomaAtom
-type NullifierKeyCommitment := mk ByteArray
+type NullifierKeyCommitment := privateMk ByteArray
 with
   -- TODO use universal instead of zero
-  zero : NullifierKeyCommitment :=
-    NullifierKeyCommitment.mk (ByteArray.zero size);
-
-  fromByteArray : ByteArray -> NullifierKeyCommitment := mk;
+  zero : NullifierKeyCommitment := privateMk (ByteArray.zero size);
+
+  --- 𝒪(1) Converts a ;ByteArray; into a ;NullifierKeyCommitment;.
+  --- It will crash if the ;ByteArray; has more than 32 (;NullifierKeyCommitment.size;) bytes.
+  fromByteArray (b : ByteArray) : NullifierKeyCommitment :=
+    let
+      numBytes := ByteArray.size b;
+    in if
+      | numBytes == size := privateMk b
+      | numBytes < size :=
+        privateMk
+          (ByteArray.fromList
+            (ByteArray.toList b ++ replicate (sub size numBytes) 0))
+      | else :=
+        failwith
+          "NullifierKeyCommitment.fromByteArray expects a ByteArray of at most 32 bytes";
+
+  -- TODO support Show in Nock so that we can show the actual size
+  -- failwith
+  --   ("NullifierKeyCommitment.fromByteArray expects a ByteArray of at most "
+  --     ++ show size
+  --     ++ " bytes. It was given one with "
+  --     ++ show numBytes
+  --     ++ " bytes");
 
   toAnomaAtom : NullifierKeyCommitment -> AnomaAtom :=
     toByteArray >> toAnomaContents;
 
+  --- 𝒪(1) The returned ;ByteArray; has always 32 (;NullifierKeyCommitment.size;) bytes
   toByteArray : NullifierKeyCommitment -> ByteArray
-    | (mk b) := b;
+    | (privateMk b) := b;
 
   size : Nat := 32;
 
@@ -260,7 +293,7 @@ with
   NullifierKeyCommitment-ToJson : ToJson NullifierKeyCommitment :=
     ToJson.mk@{
       toJson : NullifierKeyCommitment -> Json
-        | (mk b) := ToJson.toJson b;
+        | (privateMk b) := ToJson.toJson b;
     };
 end;
 
@@ -273,7 +306,7 @@ type Resource :=
     quantity : Nat;
     ephemeral : Bool;
     nonce : Nonce;
-    nullifierKeyCommitment : AnomaAtom;
+    nullifierKeyCommitment : NullifierKeyCommitment;
     --- Currently unused. It is safe to set it to 0
     unusedRandSeed : Nat;
   }
@@ -283,7 +316,8 @@ with
 
   module Transparent;
     nullifier : Resource -> Nullifier :=
-      NullifiableResource.Transparent.mk >> NullifiableResource.nullifier NullifierKey.Transparent.mk;
+      NullifiableResource.Transparent.mk
+        >> NullifiableResource.nullifier NullifierKey.Transparent.mk;
   end;
 end;
 

Package.juvix

@@ -8,7 +8,7 @@ package : Package :=
     version :=
       mkVersion@{
         major := 0;
-        minor := 12;
+        minor := 13;
         patch := 0;
       };
     dependencies :=

juvix.lock.yaml

@@ -2,7 +2,7 @@
 # Do not edit this file manually.
 
 version: 2
-checksum: 5c11471c6f7b80ce9559cafebe1537073dc5cb6bba44bbf364862c2a821bef49
+checksum: 9f8c353b8e12e7ceba849eefbe83ebbf630ae274456ada63527fe377d95d4786
 dependencies:
 - git:
     name: anoma_juvix-stdlib