Merge branch 'base'

Anoma.juvix

@@ -0,0 +1,21 @@
+module Anoma;
+
+-- import Anoma.Random open public;
+-- import Anoma.Primitives open public;
+import Anoma.Resource open public;
+import Anoma.Transaction open public;
+import Anoma.Identity open public;
+import Anoma.Builtin.ByteArray open public;
+import Anoma.Generic.ProofRecord open public;
+-- import Anoma.Compliance as Compliance public;
+import Anoma.Logic as Logic public;
+import Anoma.Delta as Delta public;
+import Anoma.Logic open using {Logic} public;
+import Anoma.Delta open using {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;
+
+import Anoma.Builtin.System open using {anomaEncode; anomaDecode} public;

Anoma/Builtin/ByteArray.juvix

@@ -0,0 +1,37 @@
+module Anoma.Builtin.ByteArray;
+
+import Stdlib.Prelude open;
+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 size : ByteArray -> Nat;
+
+builtin anoma-bytearray-to-anoma-contents
+axiom toAnomaContents : ByteArray -> Nat;
+
+builtin anoma-bytearray-from-anoma-contents
+axiom fromAnomaContents : Nat -> Nat -> ByteArray;
+
+instance
+ByteArray-Ord : Ord ByteArray :=
+  let
+    prod (b : ByteArray) : _ := size b, toAnomaContents b;
+  in mkOrd@{
+       cmp (lhs rhs : ByteArray) : Ordering := Ord.cmp (prod lhs) (prod rhs);
+     };
+
+instance
+ByteArray-Eq : Eq ByteArray := fromOrdToEq;
+
+zero (length : Nat) : ByteArray :=
+  mkByteArray
+    replicate@{
+      resultLength := length;
+      value := 0x0;
+    };

Anoma/Builtin/System.juvix

@@ -0,0 +1,102 @@
+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.
+-- TODO Conversion should be handled on the base layer.
+builtin anoma-random-generator-init
+axiom pseudoRandomNumberGeneratorInit : Nat -> PseudoRandomNumberGenerator;
+
+--- 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/Delta.juvix

@@ -0,0 +1,4 @@
+module Anoma.Delta;
+
+import Anoma.Delta.Types open public;
+-- import Anoma.Delta.ProvingSystem open public;

Anoma/Delta/Types.juvix

@@ -0,0 +1,54 @@
+module Anoma.Delta.Types;
+
+import Stdlib.Prelude open;
+-- import Anoma.Math open;
+import Anoma.Utils open;
+import Anoma.Builtin.System open;
+
+import BaseLayer.ResourceMachine as B;
+
+open B using {Delta} public;
+
+type VerifyingKey :=
+  mkVerifyingKey@{
+    unVerifyingKey : UNUSED;
+  };
+
+type ProvingKey :=
+  mkProvingKey@{
+    unProvingKey : UNUSED;
+  };
+
+type Instance :=
+  mkInstance@{
+    unInstance : UNUSED;
+  };
+
+type Witness :=
+  mkWitness@{
+    unWitness : UNUSED;
+  };
+
+--- The ;Delta; value zero.
+zero : Delta := STILL_MISSING_ANOMA_BUILTIN;
+
+--- Adds two ;Delta; values.
+addDelta (d1 d2 : Delta) : Delta := ANOMA_BACKEND_IMPLEMENTATION;
+
+deriving instance
+VerifyingKey-Ord : Ord VerifyingKey;
+
+deriving instance
+VerifyingKey-Eq : Eq VerifyingKey;
+
+deriving instance
+Instance-Ord : Ord Instance;
+
+deriving instance
+Instance-Eq : Eq Instance;
+
+deriving instance
+Witness-Ord : Ord Witness;
+
+deriving instance
+Witness-Eq : Eq Witness;

Anoma/Generic/ProofRecord.juvix

@@ -0,0 +1,13 @@
+module Anoma.Generic.ProofRecord;
+
+import Stdlib.Prelude open;
+
+import Anoma.Logic.Types as Logic;
+import Anoma.Delta.Types as Delta;
+import Anoma.Utils open;
+
+--- A wrapper type for all of the supported proof record types.
+type ProofRecord :=
+  | ComplianceProofRecord
+  | LogicProofRecord Logic.ProofRecord
+  | DeltaProofRecord;

Anoma/Identity.juvix

@@ -0,0 +1,6 @@
+module Anoma.Identity;
+
+import Anoma.Identity.External open public;
+import Anoma.Identity.Internal open public;
+import Anoma.Identity.Object open public;
+import Anoma.Identity.Signing.Types open public;

Anoma/Identity/External.juvix

@@ -0,0 +1,25 @@
+module Anoma.Identity.External;
+
+import Stdlib.Prelude open;
+import Anoma.Builtin.ByteArray open using {ByteArray; toAnomaContents};
+
+--- A fixed-size data type describing an external identity.
+type ExternalIdentity :=
+  mkExternalIdentity@{
+    unExternalIdentity : ByteArray;
+  };
+
+deriving instance
+ExternalIdentity-Ord : Ord ExternalIdentity;
+
+deriving instance
+ExternalIdentity-Eq : Eq ExternalIdentity;
+
+instance
+ExternalIdentity-Show : Show ExternalIdentity :=
+  mkShow
+    \{iden :=
+      iden
+        |> ExternalIdentity.unExternalIdentity
+        |> toAnomaContents
+        |> natToString};

Anoma/Identity/Internal.juvix

@@ -0,0 +1,36 @@
+module Anoma.Identity.Internal;
+
+import Stdlib.Prelude open;
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+import Anoma.Builtin.ByteArray open using {ByteArray; toAnomaContents};
+
+--- A fixed-size data type describing an internal identity.
+type InternalIdentity :=
+  mkInternalIdentity@{
+    unInternalIdentity : ByteArray;
+  };
+
+module InternalIdentityInternal;
+  --- Compares two ;InternalIdentity; objects.
+  compare (lhs rhs : InternalIdentity) : Ordering :=
+    Ord.cmp
+      (InternalIdentity.unInternalIdentity lhs)
+      (InternalIdentity.unInternalIdentity rhs);
+
+  --- Implements the ;Ord; trait for ;InternalIdentity;.
+  instance
+  InternalIdentity-Ord : Ord InternalIdentity := mkOrd compare;
+
+  --- Implements the ;Eq; trait for ;InternalIdentity;.
+  instance
+  InternalIdentity-Eq : Eq InternalIdentity := fromOrdToEq;
+end;
+
+instance
+InternalIdentity-Show : Show InternalIdentity :=
+  mkShow
+    \{id :=
+      id
+        |> InternalIdentity.unInternalIdentity
+        |> toAnomaContents
+        |> natToString};

Anoma/Identity/Object.juvix

@@ -0,0 +1,40 @@
+module Anoma.Identity.Object;
+
+import Stdlib.Prelude open;
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+import Anoma.Identity.External open;
+import Anoma.Identity.Internal open;
+
+--- A record describing an identity.
+--- NOTE: For the private testnet, this deviates from the specs https://specs.anoma.net/v2/system_architecture/identity/identity.html.
+type Identity :=
+  mkIdentity@{
+    external : ExternalIdentity;
+    internal : InternalIdentity;
+  };
+
+module IdentityInternal;
+  --- Compares two ;Identity; objects.
+  compare (lhs rhs : Identity) : Ordering :=
+    Ord.cmp (Identity.external lhs) (Identity.external rhs);
+
+  --- Implements the ;Ord; trait for ;Identity;.
+  instance
+  Identity-Ord : Ord Identity := mkOrd compare;
+
+  --- Implements the ;Eq; trait for ;Identity;.
+  instance
+  Identity-Eq : Eq Identity := fromOrdToEq;
+end;
+
+instance
+Identity-Show : Show Identity :=
+  mkShow
+    \{id :=
+      "{"
+        ++str "external : "
+        ++str (id |> Identity.external |> Show.show)
+        ++str ", "
+        ++str "internal : "
+        ++str (id |> Identity.internal |> Show.show)
+        ++str "}"};

Anoma/Identity/Signing/Types.juvix

@@ -0,0 +1,27 @@
+module Anoma.Identity.Signing.Types;
+
+import Stdlib.Prelude open;
+import Anoma.Identity.Internal open;
+import Anoma.Identity.External open;
+import Anoma.Builtin.ByteArray as ByteArray open;
+import Anoma.Builtin.System as SystemBuiltins open;
+
+type Signature :=
+  mkSignature@{
+    unSignature : ByteArray;
+  };
+
+{-# inline: true #-}
+sign
+  : {Message : Type}
+    -- | The message to sign.
+    -> (message : Message)
+    -- | The signing internal identity.
+    -> (signer : InternalIdentity)
+    -- | The resulting signature
+    -> Signature
+  | message internalIdentity :=
+    SystemBuiltins.anomaSign
+        message
+        (InternalIdentity.unInternalIdentity internalIdentity)
+      |> mkSignature;

Anoma/Logic.juvix

@@ -0,0 +1,4 @@
+module Anoma.Logic;
+
+import Anoma.Logic.Types open public;
+import Anoma.Logic.ProvingSystem open public;

Anoma/Logic/ProvingSystem.juvix

@@ -0,0 +1,13 @@
+module Anoma.Logic.ProvingSystem;
+
+import Anoma.Logic.Types open;
+import BaseLayer.ResourceMachine as B;
+import Anoma.Resource.Object open;
+import Stdlib.Prelude open;
+
+prove
+  (provingKey : ProvingKey)
+  (publicInputs : Instance)
+  (privateInputs : Witness)
+  : Proof :=
+  proofLogic (ProvingKey.unProvingKey provingKey) (publicInputs, privateInputs);