From c3b3ea0e274020d9dbb324b6e2c88b67a76c6346 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 15 May 2025 12:42:23 +0200 Subject: [PATCH 01/11] update type of nullifierKeyCommitment Resource field --- BaseLayer/ResourceMachine.juvix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/BaseLayer/ResourceMachine.juvix b/BaseLayer/ResourceMachine.juvix index 269b79c..585c60e 100644 --- a/BaseLayer/ResourceMachine.juvix +++ b/BaseLayer/ResourceMachine.juvix @@ -273,7 +273,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; } From f083de7e644a7c81906789df2a148f909731e4b5 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 15 May 2025 22:59:11 +0200 Subject: [PATCH 02/11] fix NullifierKeyCommitment.fromByteArray --- Applib/Identities.juvix | 4 ++-- BaseLayer/ResourceMachine.juvix | 34 +++++++++++++++++++++++++-------- juvix.lock.yaml | 2 +- 3 files changed, 29 insertions(+), 11 deletions(-) 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/BaseLayer/ResourceMachine.juvix b/BaseLayer/ResourceMachine.juvix index 585c60e..b5bb01c 100644 --- a/BaseLayer/ResourceMachine.juvix +++ b/BaseLayer/ResourceMachine.juvix @@ -230,19 +230,36 @@ 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 " + ++ 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 +277,7 @@ with NullifierKeyCommitment-ToJson : ToJson NullifierKeyCommitment := ToJson.mk@{ toJson : NullifierKeyCommitment -> Json - | (mk b) := ToJson.toJson b; + | (privateMk b) := ToJson.toJson b; }; end; @@ -283,7 +300,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/juvix.lock.yaml b/juvix.lock.yaml index 7a68875..e56209e 100644 --- a/juvix.lock.yaml +++ b/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 From 315e42360dd1d33ac70de0cb395f3d17c578d325 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 15 May 2025 23:13:47 +0200 Subject: [PATCH 03/11] remove show --- BaseLayer/ResourceMachine.juvix | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/BaseLayer/ResourceMachine.juvix b/BaseLayer/ResourceMachine.juvix index b5bb01c..f26bcea 100644 --- a/BaseLayer/ResourceMachine.juvix +++ b/BaseLayer/ResourceMachine.juvix @@ -248,11 +248,15 @@ with (ByteArray.toList b ++ replicate (sub size numBytes) 0)) | else := failwith - ("NullifierKeyCommitment.fromByteArray expects a ByteArray of at most " - ++ show size - ++ " bytes. It was given one with " - ++ show numBytes - ++ " bytes"); + "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; From fb02a128ecce78c19b56a54e463228d35a7e0a94 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 16 May 2025 08:24:26 +0200 Subject: [PATCH 04/11] fix generation of random bytes --- Anoma/Builtin/System.juvix | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) 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; From 03744a46650d3041341f3ad56c030412b3913028 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 16 May 2025 08:31:12 +0200 Subject: [PATCH 05/11] guard Nonce.fromByteArray --- BaseLayer/ResourceMachine.juvix | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/BaseLayer/ResourceMachine.juvix b/BaseLayer/ResourceMachine.juvix index f26bcea..262a155 100644 --- a/BaseLayer/ResourceMachine.juvix +++ b/BaseLayer/ResourceMachine.juvix @@ -207,9 +207,14 @@ 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 := failwith "Nonce.fromByteArray incorrect size"; + + from32SizedByteArray : ByteArray -> Nonce := fromByteArray; toAnomaAtom : Nonce -> AnomaAtom | (privateMk nonce) := toAnomaContents nonce; From 49ed9f9e8afa14e030878a0c2845eb0e2d3ee68c Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Sat, 17 May 2025 09:10:38 +0200 Subject: [PATCH 06/11] print bytearray size --- BaseLayer/ResourceMachine.juvix | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/BaseLayer/ResourceMachine.juvix b/BaseLayer/ResourceMachine.juvix index 262a155..19e37bb 100644 --- a/BaseLayer/ResourceMachine.juvix +++ b/BaseLayer/ResourceMachine.juvix @@ -2,7 +2,7 @@ module BaseLayer.ResourceMachine; import BaseLayer.AnomaAtom open public; 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; @@ -212,7 +212,10 @@ with fromByteArray (b : ByteArray) : Nonce := if | ByteArray.size b == size := privateMk b - | else := failwith "Nonce.fromByteArray incorrect size"; + | else := + trace "bytearraysize: " + >-> trace (ByteArray.size b) + >-> failwith "Nonce.fromByteArray incorrect size"; from32SizedByteArray : ByteArray -> Nonce := fromByteArray; From 2041ec51155cf4bede3abcb210a85ab0e9053df2 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Sun, 18 May 2025 09:11:49 +0200 Subject: [PATCH 07/11] add recursiveNatToString --- Applib/Show.juvix | 25 +++++++++++++++++++++++++ BaseLayer/ResourceMachine.juvix | 6 +++++- 2 files changed, 30 insertions(+), 1 deletion(-) create mode 100644 Applib/Show.juvix diff --git a/Applib/Show.juvix b/Applib/Show.juvix new file mode 100644 index 0000000..f452a9b --- /dev/null +++ b/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); diff --git a/BaseLayer/ResourceMachine.juvix b/BaseLayer/ResourceMachine.juvix index 19e37bb..475794a 100644 --- a/BaseLayer/ResourceMachine.juvix +++ b/BaseLayer/ResourceMachine.juvix @@ -1,6 +1,7 @@ module BaseLayer.ResourceMachine; import BaseLayer.AnomaAtom open public; +import Applib.Show open; import Anoma.Encode open; import Stdlib.Debug open; import Anoma.Builtin.System open; @@ -215,7 +216,10 @@ with | else := trace "bytearraysize: " >-> trace (ByteArray.size b) - >-> failwith "Nonce.fromByteArray incorrect size"; + >-> failwith + ("Nonce.fromByteArray incorrect size. Was passed a bytearray with size " + ++ recursiveNatToString (ByteArray.size b) + ++ "."); from32SizedByteArray : ByteArray -> Nonce := fromByteArray; From 259645a5f412b204d2fa41fa37f33186c9347a4a Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 20 May 2025 16:14:56 +0200 Subject: [PATCH 08/11] export Applib.Show --- Applib.juvix | 2 +- Package.juvix | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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/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 := From 29bf50606189461b652de6c4312f665cce620159 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 20 May 2025 16:44:17 +0200 Subject: [PATCH 09/11] remove comment and update lockfile --- BaseLayer/ResourceMachine.juvix | 8 -------- juvix.lock.yaml | 2 +- 2 files changed, 1 insertion(+), 9 deletions(-) diff --git a/BaseLayer/ResourceMachine.juvix b/BaseLayer/ResourceMachine.juvix index 475794a..bf3a0f3 100644 --- a/BaseLayer/ResourceMachine.juvix +++ b/BaseLayer/ResourceMachine.juvix @@ -262,14 +262,6 @@ with 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; diff --git a/juvix.lock.yaml b/juvix.lock.yaml index e56209e..3916ea8 100644 --- a/juvix.lock.yaml +++ b/juvix.lock.yaml @@ -2,7 +2,7 @@ # Do not edit this file manually. version: 2 -checksum: 9f8c353b8e12e7ceba849eefbe83ebbf630ae274456ada63527fe377d95d4786 +checksum: 7a1c0a81eaeccccd15bd8132ec0eb5238f610b3aec8ac13993ab49331c8d3d0e dependencies: - git: name: anoma_juvix-stdlib From 5bfd5a4cb8b8aa43a82f14673327002ced725cbe Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 20 May 2025 16:48:26 +0200 Subject: [PATCH 10/11] remove trace --- BaseLayer/ResourceMachine.juvix | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/BaseLayer/ResourceMachine.juvix b/BaseLayer/ResourceMachine.juvix index bf3a0f3..50f6144 100644 --- a/BaseLayer/ResourceMachine.juvix +++ b/BaseLayer/ResourceMachine.juvix @@ -3,10 +3,10 @@ module BaseLayer.ResourceMachine; import BaseLayer.AnomaAtom open public; import Applib.Show open; import Anoma.Encode open; -import Stdlib.Debug 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; @@ -214,9 +214,7 @@ with if | ByteArray.size b == size := privateMk b | else := - trace "bytearraysize: " - >-> trace (ByteArray.size b) - >-> failwith + failwith ("Nonce.fromByteArray incorrect size. Was passed a bytearray with size " ++ recursiveNatToString (ByteArray.size b) ++ "."); From 5a660bc9520d9c4b0cd30e567b3d851e7fefed07 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 20 May 2025 16:49:23 +0200 Subject: [PATCH 11/11] improve error message --- Applib/Show.juvix | 3 ++- BaseLayer/ResourceMachine.juvix | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Applib/Show.juvix b/Applib/Show.juvix index f452a9b..863eb87 100644 --- a/Applib/Show.juvix +++ b/Applib/Show.juvix @@ -1,6 +1,7 @@ module Applib.Show; import Stdlib.Prelude open; +import Stdlib.Debug.Fail open; import Stdlib.Math open; --- non-builtin equivalent of ;natToString; @@ -19,7 +20,7 @@ recursiveNatToString (n : Nat) : String := | d == 7 := "7" | d == 8 := "8" | d == 9 := "9" - | else := "impossible"; + | 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 50f6144..2b2d0cc 100644 --- a/BaseLayer/ResourceMachine.juvix +++ b/BaseLayer/ResourceMachine.juvix @@ -258,7 +258,7 @@ with (ByteArray.toList b ++ replicate (sub size numBytes) 0)) | else := failwith - "NullifierKeyCommitment.fromByteArray expects a ByteArray of at most 32 bytes"; + ("NullifierKeyCommitment.fromByteArray expects a ByteArray of at most 32 bytes. Was given a ByteArray of length " ++ recursiveNatToString numBytes); toAnomaAtom : NullifierKeyCommitment -> AnomaAtom := toByteArray >> toAnomaContents;