chore: update deps

Anoma/Builtin/ByteArray.juvix

@@ -26,7 +26,6 @@ module ByteArrayInternal;
          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

@@ -13,61 +13,67 @@ 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;
+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;
+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;
+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;
+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;
+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;
+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

Anoma/Compliance/Types.juvix

@@ -1,18 +1,33 @@
 module Anoma.Compliance.Types;
 
 import Stdlib.Prelude open;
-import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+
 import Anoma.Utils open;
 
-type Proof := mkProof@{unProof : MISSING_DEFINITION};
+type Proof :=
+  mkProof@{
+    unProof : MISSING_DEFINITION;
+  };
 
-type VerifyingKey := mkVerifyingKey@{unVerifyingKey : MISSING_DEFINITION};
+type VerifyingKey :=
+  mkVerifyingKey@{
+    unVerifyingKey : MISSING_DEFINITION;
+  };
 
-type ProvingKey := mkProvingKey@{unProvingKey : MISSING_DEFINITION};
+type ProvingKey :=
+  mkProvingKey@{
+    unProvingKey : MISSING_DEFINITION;
+  };
 
-type Instance := mkInstance@{unInstance : MISSING_DEFINITION};
+type Instance :=
+  mkInstance@{
+    unInstance : MISSING_DEFINITION;
+  };
 
-type Witness := mkWitness@{unWitness : MISSING_DEFINITION};
+type Witness :=
+  mkWitness@{
+    unWitness : MISSING_DEFINITION;
+  };
 
 type ProofRecord :=
   mkProofRecord@{
@@ -21,75 +36,32 @@ type ProofRecord :=
     instance : Instance;
   };
 
-module ProofInternal;
-  --- Compares two ;Proof; objects.
-  compare (lhs rhs : Proof) : Ordering :=
-    Ord.cmp (Proof.unProof lhs) (Proof.unProof rhs);
-
-  --- Implements the ;Ord; trait for ;Proof;.
-  instance
-  Proof-Ord : Ord Proof := mkOrd compare;
-
-  --- Implements the ;Eq; trait for ;Proof;.
-  instance
-  Proof-Eq : Eq Proof := fromOrdToEq;
-end;
-
-module VerifyingKeyInternal;
-  --- Compares two ;VerifyingKey; objects.
-  compare (lhs rhs : VerifyingKey) : Ordering :=
-    Ord.cmp (VerifyingKey.unVerifyingKey lhs) (VerifyingKey.unVerifyingKey rhs);
-
-  --- Implements the ;Ord; trait for ;VerifyingKey;.
-  instance
-  VerifyingKey-Ord : Ord VerifyingKey := mkOrd compare;
-
-  --- Implements the ;Eq; trait for ;VerifyingKey;.
-  instance
-  VerifyingKey-Eq : Eq VerifyingKey := fromOrdToEq;
-end;
-
-module InstanceInternal;
-  --- Compares two ;Instance; objects.
-  compare (lhs rhs : Instance) : Ordering :=
-    Ord.cmp (Instance.unInstance lhs) (Instance.unInstance rhs);
-
-  --- Implements the ;Ord; trait for ;Instance;.
-  instance
-  Instance-Ord : Ord Instance := mkOrd compare;
-
-  --- Implements the ;Eq; trait for ;Instance;.
-  instance
-  Instance-Eq : Eq Instance := fromOrdToEq;
-end;
-
-module WitnessInternal;
-  --- Compares two ;Witness; objects.
-  compare (lhs rhs : Witness) : Ordering :=
-    Ord.cmp (Witness.unWitness lhs) (Witness.unWitness rhs);
-
-  --- Implements the ;Ord; trait for ;Witness;.
-  instance
-  Witness-Ord : Ord Witness := mkOrd compare;
-
-  --- Implements the ;Eq; trait for ;Witness;.
-  instance
-  Witness-Eq : Eq Witness := fromOrdToEq;
-end;
-
-module ProofRecordInternal;
-  --- Compares two ;ProofRecord; objects.
-  compare (lhs rhs : ProofRecord) : Ordering :=
-    let
-      prod (p : ProofRecord) : _ :=
-        ProofRecord.proof p, ProofRecord.verifyingKey p, ProofRecord.instance p;
-    in Ord.cmp (prod lhs) (prod rhs);
-
-  --- Implements the ;Ord; trait for ;ProofRecord;.
-  instance
-  ProofRecord-Ord : Ord ProofRecord := mkOrd compare;
-
-  --- Implements the ;Eq; trait for ;ProofRecord;.
-  instance
-  ProofRecord-Eq : Eq ProofRecord := fromOrdToEq;
-end;
+deriving instance
+Proof-Ord : Ord Proof;
+
+deriving instance
+Proof-Eq : Eq Proof;
+
+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;
+
+deriving instance
+ProofRecord-Ord : Ord ProofRecord;
+
+deriving instance
+ProofRecord-Eq : Eq ProofRecord;