feat: move builtin definitions from the transparent instance

Anoma/Builtin/ByteArray.juvix

@@ -0,0 +1,32 @@
+module Anoma.Builtin.ByteArray;
+
+import Stdlib.Prelude open hiding {length};
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+
+builtin bytearray
+axiom ByteArray : Type;
+
+builtin bytearray-from-list-byte
+axiom mkByteArray : List Byte -> ByteArray;
+
+builtin bytearray-length
+axiom length : ByteArray -> Nat;
+
+module ByteArrayInternal;
+  syntax alias AnomaByteArray := Nat;
+
+  builtin anoma-bytearray-to-anoma-contents
+  axiom toAnomaByteArray : ByteArray -> AnomaByteArray;
+
+  instance
+  ByteArray-Ord : Ord ByteArray :=
+    let
+      prod (b : ByteArray) : _ := length b, toAnomaByteArray b;
+    in mkOrd@{
+         cmp (lhs rhs : ByteArray) : Ordering := Ord.cmp (prod lhs) (prod rhs);
+       };
+
+  --- Implements the ;Eq; trait for ;ByteArray;.
+  instance
+  ByteArray-Eq : Eq ByteArray := fromOrdToEq;
+end;

Anoma/Builtin/System.juvix

@@ -0,0 +1,95 @@
+module Anoma.Builtin.System;
+
+import Stdlib.Prelude open;
+import Anoma.Builtin.ByteArray open;
+
+module Internal;
+  syntax alias PublicKey := ByteArray;
+  syntax alias PrivateKey := ByteArray;
+
+  syntax alias Signature := ByteArray;
+  syntax alias SignedMessage := ByteArray;
+end;
+
+--- Encodes a value into a natural number.
+builtin anoma-encode
+axiom anomaEncode : {Value : Type}
+  -- | The value to encode.
+  -> Value
+  -- | The encoded natural number.
+  -> Nat;
+
+--- Decodes a value from a natural number.
+builtin anoma-decode
+axiom anomaDecode : {Value : Type}
+  -- | The natural number to decode.
+  -> Nat
+  -- | The decoded value.
+  -> Value;
+
+--- Signs a message with a private key and returns a signed message.
+builtin anoma-sign
+axiom anomaSign : {Message : Type}
+  -- | The message to sign.
+  -> Message
+  -- | The signing private key.
+  -> Internal.PrivateKey
+  -- | The resulting signed message.
+  -> Internal.SignedMessage;
+
+--- Signs a message with a private key and returns the signature.
+builtin anoma-sign-detached
+axiom anomaSignDetached : {Message : Type}
+  -- | The message to sign.
+  -> Message
+  -- | The signing private key.
+  -> Internal.PrivateKey
+  -- The resulting signature
+  -> Internal.Signature;
+
+--- Verifies a signature against a message and public key.
+builtin anoma-verify-detached
+axiom anomaVerifyDetached : {Message : Type}
+  -- | The signature to verify.
+  -> Internal.Signature
+  -- | The message to verify against.
+  -> Message
+  -- | The signer public key to verify against.
+  -> Internal.PublicKey
+  -- | The verification result.
+  -> Bool;
+
+--- Verifies a signature against a message and public key and return the message on success.
+builtin anoma-verify-with-message
+axiom anomaVerifyWithMessage : {Message : Type}
+  -- | The signed message to verify.
+  -> Internal.SignedMessage
+  -- | The signer public key to verify against.
+  -> Internal.PublicKey
+  -- | The original message.
+  -> Maybe Message;
+
+--- 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;

juvix.lock.yaml

@@ -1,8 +1,8 @@
-# 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
-checksum: 2b4ceed787050a25e74294448dc1bcdd9683916bc5bed83bbcbf6e652897308d
+checksum: aee7ca6999521d60319bcb414911575aab7ff59e369c9c4677da9563a6299942
 dependencies:
 - git:
     name: anoma_juvix-stdlib