diff --git a/Anoma/Builtin/System.juvix b/Anoma/Builtin/System.juvix index c54df24..bbf4c59 100644 --- a/Anoma/Builtin/System.juvix +++ b/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; diff --git a/Applib.juvix b/Applib.juvix index 3a5679c..7aee043 100644 --- a/Applib.juvix +++ b/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; diff --git a/Applib/Identities.juvix b/Applib/Identities.juvix index 2b5be34..70f0ba0 100644 --- a/Applib/Identities.juvix +++ b/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; diff --git a/Applib/Show.juvix b/Applib/Show.juvix new file mode 100644 index 0000000..863eb87 --- /dev/null +++ b/Applib/Show.juvix @@ -0,0 +1,26 @@ +module Applib.Show; + +import Stdlib.Prelude open; +import Stdlib.Debug.Fail 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 := failwith "impossible"; + in if + | n < 10 := showDigit n + | else := recursiveNatToString (div n 10) ++ showDigit (mod n 10); diff --git a/BaseLayer/ResourceMachine.juvix b/BaseLayer/ResourceMachine.juvix index 269b79c..2b2d0cc 100644 --- a/BaseLayer/ResourceMachine.juvix +++ b/BaseLayer/ResourceMachine.juvix @@ -1,11 +1,12 @@ module BaseLayer.ResourceMachine; import BaseLayer.AnomaAtom open public; +import Applib.Show open; import Anoma.Encode open; -import Stdlib.Debug.Fail open; import Anoma.Builtin.System open; import Anoma.Builtin.ByteArray open; import Stdlib.Prelude open; +import Stdlib.Debug.Fail open; import Stdlib.Data.Map as Map open; import Anoma.Primitives.FixedSize open; import Anoma.Data.Json open; @@ -207,9 +208,18 @@ with size : Nat := 32; - fromAnomaAtom : AnomaAtom -> Nonce := fromAnomaContents size >> privateMk; + fromAnomaAtom : AnomaAtom -> Nonce := fromAnomaContents size >> fromByteArray; + + fromByteArray (b : ByteArray) : Nonce := + if + | ByteArray.size b == size := privateMk b + | else := + failwith + ("Nonce.fromByteArray incorrect size. Was passed a bytearray with size " + ++ recursiveNatToString (ByteArray.size b) + ++ "."); - from32SizedByteArray : ByteArray -> Nonce := privateMk; + from32SizedByteArray : ByteArray -> Nonce := fromByteArray; toAnomaAtom : Nonce -> AnomaAtom | (privateMk nonce) := toAnomaContents nonce; @@ -230,19 +240,32 @@ 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. Was given a ByteArray of length " ++ recursiveNatToString numBytes); 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 +283,7 @@ with NullifierKeyCommitment-ToJson : ToJson NullifierKeyCommitment := ToJson.mk@{ toJson : NullifierKeyCommitment -> Json - | (mk b) := ToJson.toJson b; + | (privateMk b) := ToJson.toJson b; }; end; @@ -273,7 +296,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 +306,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; diff --git a/Package.juvix b/Package.juvix index cb75216..7b7afee 100644 --- a/Package.juvix +++ b/Package.juvix @@ -8,7 +8,7 @@ package : Package := version := mkVersion@{ major := 0; - minor := 12; + minor := 13; patch := 0; }; dependencies := diff --git a/juvix.lock.yaml b/juvix.lock.yaml index 7a68875..3916ea8 100644 --- a/juvix.lock.yaml +++ b/juvix.lock.yaml @@ -2,7 +2,7 @@ # Do not edit this file manually. version: 2 -checksum: 5c11471c6f7b80ce9559cafebe1537073dc5cb6bba44bbf364862c2a821bef49 +checksum: 7a1c0a81eaeccccd15bd8132ec0eb5238f610b3aec8ac13993ab49331c8d3d0e dependencies: - git: name: anoma_juvix-stdlib