style: formatting

Anoma/Delta.juvix

@@ -5,7 +5,7 @@ import Anoma.Utils open;
 
 --- A fixed-size data type encoding the additively homomorphic and kind distinct ;Delta;.
 --- NOTE: For the private testnet, the requirement can be relaxed by allowing ;Delta; to be dynamically-sized.
-type Delta := mkDelta {unDelta : MISSING_DEFINITION};
+type Delta := mkDelta@{unDelta : MISSING_DEFINITION};
 
 --- The ;Delta; value zero.
 zero : Delta := MISSING_ANOMA_BUILTIN;

Anoma/Identity/External.juvix

@@ -5,7 +5,7 @@ import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
 import Anoma.Utils open;
 
 --- A fixed-size data type describing an external identity.
-type ExternalIdentity := mkExternalIdentity {unExternalIdentity : MISSING_DEFINITION};
+type ExternalIdentity := mkExternalIdentity@{unExternalIdentity : MISSING_DEFINITION};
 
 module ExternalIdentityInternal;
   --- Compares two ;ExternalIdentity; objects.

Anoma/Identity/Internal.juvix

@@ -5,7 +5,7 @@ import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
 import Anoma.Utils open;
 
 --- A fixed-size data type describing an internal identity.
-type InternalIdentity := mkInternalIdentity {unInternalIdentity : MISSING_DEFINITION};
+type InternalIdentity := mkInternalIdentity@{unInternalIdentity : MISSING_DEFINITION};
 
 module InternalIdentityInternal;
   --- Compares two ;InternalIdentity; objects.

Anoma/Identity/Object.juvix

@@ -8,7 +8,7 @@ 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 {
+  mkIdentity@{
     external : ExternalIdentity;
     internal : InternalIdentity
   };

Anoma/Identity/Signing/Types.juvix

@@ -5,7 +5,7 @@ import Anoma.Identity.Internal open;
 import Anoma.Identity.External open;
 import Anoma.Utils open;
 
-type Signature := mkSignature {unSignature : MISSING_DEFINITION};
+type Signature := mkSignature@{unSignature : MISSING_DEFINITION};
 
 {-# inline: true #-}
 verify
@@ -33,7 +33,7 @@ sign
 
 --- TODO Consider deleting the definitions below.
 module NonDetached;
-  type SignedMessage := mkSignedMessage {unSignedMessage : MISSING_DEFINITION};
+  type SignedMessage := mkSignedMessage@{unSignedMessage : MISSING_DEFINITION};
 
   {-# inline: true #-}
   verify (signedMessage : SignedMessage) (externalIdentity : ExternalIdentity) : Bool :=

Anoma/Math.juvix

@@ -6,7 +6,7 @@ import Stdlib.Data.Set as Set open using {Set; union; intersection};
 --- A trait describing additive homomorphicity.
 trait
 type AdditivelyHomomorphic T :=
-  mkAdditivelyHomomorphic {--- Adds two types implementing the ;AdditivelyHomomorphic; trait.
+  mkAdditivelyHomomorphic@{--- Adds two types implementing the ;AdditivelyHomomorphic; trait.
   add : (v1 v2 : T) -> T};
 
 --- Implements the ;Eq; trait for ;AdditivelyHomomorphic; types.
@@ -17,7 +17,7 @@ Property-AdditivelyHomomorphic
 --- A trait describing kind distinctness.
 trait
 type KindDistinct T :=
-  mkKindDistinct {--- Adds two types implementing the ;KindDistinct; trait.
+  mkKindDistinct@{--- Adds two types implementing the ;KindDistinct; trait.
   add : (v1 v2 : T) -> T};
 
 --- Computes the disjoint union of two ;Set;s.

Anoma/Proving/ComplianceProof.juvix

@@ -7,7 +7,7 @@ import Anoma.Proving.Types open using {module Compliance};
 import Anoma.Utils open;
 
 type ProofRecord :=
-  mkProofRecord {
+  mkProofRecord@{
     proof : Compliance.Proof;
     verifyingKey : Compliance.VerifyingKey;
     instance : Compliance.Instance

Anoma/Proving/DeltaProof.juvix

@@ -7,7 +7,7 @@ import Anoma.Proving.Types open using {module Delta};
 import Anoma.Utils open;
 
 type ProofRecord :=
-  mkProofRecord {
+  mkProofRecord@{
     proof : Delta.Proof;
     verifyingKey : Delta.VerifyingKey;
     instance : Delta.Instance

Anoma/Proving/LogicProof.juvix

@@ -7,7 +7,7 @@ import Anoma.Proving.Types open using {module Logic};
 import Anoma.Utils open;
 
 type ProofRecord :=
-  mkProofRecord {
+  mkProofRecord@{
     proof : Logic.Proof;
     verifyingKey : Logic.VerifyingKey;
     instance : Logic.Instance

Anoma/Resource/Object.juvix

@@ -6,7 +6,7 @@ import Anoma.Resource.Types open;
 
 --- A record describing a resource, the atomic unit of state in the Anoma state model.
 type Resource :=
-  mkResource {
+  mkResource@{
     logicRef : LogicRef;
     labelRef : LabelRef;
     valueRef : ValueRef;

Anoma/Resource/Types.juvix

@@ -6,48 +6,48 @@ import Anoma.Utils open;
 
 --- A fixed-size data type encoding the reference to the resource logic function.
 --- NOTE: For the private testnet, the requirement can be relaxed by allowing ;LogicRef; to be dynamically-sized.
-type LogicRef := mkLogicRef {unLogicRef : MISSING_DEFINITION};
+type LogicRef := mkLogicRef@{unLogicRef : MISSING_DEFINITION};
 
 --- A fixed-size data type encoding the reference to the resource label field.
 --- NOTE: For the private testnet, the requirement can be relaxed by allowing ;LabelRef; to be dynamically-sized.
-type LabelRef := mkLabelRef {unLabelRef : MISSING_DEFINITION};
+type LabelRef := mkLabelRef@{unLabelRef : MISSING_DEFINITION};
 
 --- A fixed-size data type encoding the reference to the resource value field.
 --- NOTE: For the private testnet, the requirement can be relaxed by allowing ;ValueRef; to be dynamically-sized.
-type ValueRef := mkValueRef {unValueRef : MISSING_DEFINITION};
+type ValueRef := mkValueRef@{unValueRef : MISSING_DEFINITION};
 
 --- A fixed-size data type encoding the quantity of a resource.
-type Quantity := mkQuantity {unQuantity : MISSING_DEFINITION};
+type Quantity := mkQuantity@{unQuantity : MISSING_DEFINITION};
 
 --- A fixed-size data type encoding the public commitment to the private nullifier key.
 type NullifierKeyCommitment :=
-  mkNullifierKeyCommitment {unNullifierKeyCommitment : MISSING_DEFINITION};
+  mkNullifierKeyCommitment@{unNullifierKeyCommitment : MISSING_DEFINITION};
 
 --- A fixed-size data type encoding a number to be used once ensuring that the resource commitment is unique.
 --- NOTE: This should be a number having an at most negligible chance of repeating is sufficient, e.g., a pseudo-random number.
-type Nonce := mkNonce {unNonce : MISSING_DEFINITION};
+type Nonce := mkNonce@{unNonce : MISSING_DEFINITION};
 
 --- A fixed-size data type encoding a randomness seed.
 --- NOTE: This seed provides pseudo randomness and cannot be expected to provide true randomness.
-type RandSeed := mkRandSeed {unRandSeed : MISSING_DEFINITION};
+type RandSeed := mkRandSeed@{unRandSeed : MISSING_DEFINITION};
 
 --- The resource label type.
-type Label := mkLabel {unLabel : MISSING_DEFINITION};
+type Label := mkLabel@{unLabel : MISSING_DEFINITION};
 
 --- The resource value type.
-type Value := mkValue {unValue : MISSING_DEFINITION};
+type Value := mkValue@{unValue : MISSING_DEFINITION};
 
 --- The resource kind type.
-type Kind := mkKind {unKind : MISSING_DEFINITION};
+type Kind := mkKind@{unKind : MISSING_DEFINITION};
 
 --- The resource commitment type.
-type Commitment := mkCommitment {unCommitment : MISSING_DEFINITION};
+type Commitment := mkCommitment@{unCommitment : MISSING_DEFINITION};
 
 --- The resource nullifier type.
-type Nullifier := mkNullifier {unNullifier : MISSING_DEFINITION};
+type Nullifier := mkNullifier@{unNullifier : MISSING_DEFINITION};
 
 --- The nullifier key type describing a secret required to compute the ;Nullifier; of a resource
-type NullifierKey := mkNullifierKey {unNullifierKey : MISSING_DEFINITION};
+type NullifierKey := mkNullifierKey@{unNullifierKey : MISSING_DEFINITION};
 
 module LogicRefInternal;
   --- Compares two ;LogicRef; objects.

Anoma/State/CommitmentTree.juvix

@@ -9,16 +9,16 @@ import Anoma.Resource.Types as Resource open using {Commitment};
 import Anoma.Utils open;
 
 --- A state root of the commitment tree.
-type Root := mkRoot {unRoot : MISSING_DEFINITION};
+type Root := mkRoot@{unRoot : MISSING_DEFINITION};
 
 --- A path in the commitment tree.
-type Path := mkPath {unPath : MISSING_DEFINITION};
+type Path := mkPath@{unPath : MISSING_DEFINITION};
 
 --- The interface of the commitment tree.
 positive
 trait
 type CommitmentTree :=
-  mkCommitmentTree {
+  mkCommitmentTree@{
     --- Adds a ;Resource.Commitment; to the ;CommitmentTree; and returns the ;Path;.
     add : (tree : CommitmentTree) -> (commitment : Resource.Commitment) -> Path;
 

Anoma/State/NullifierSet.juvix

@@ -8,7 +8,7 @@ import Anoma.Resource.Types as Resource open using {Nullifier};
 --- The interface of the nullifier set.
 trait
 type NullifierSet :=
-  mkNullifierSet {
+  mkNullifierSet@{
     --- Adds a ;Resource.Nullifier; to the ;NullifierSet;.
     --- TODO Wait for the specs to rename this from `write` to `add`.
     add : (nullifier : Resource.Nullifier) -> NullifierSet;

Anoma/State/ResourceMachine.juvix

@@ -11,7 +11,7 @@ import Anoma.Proving.ProofRecord open using {ProofRecord};
 --- The resource machine interface.
 trait
 type ResourceMachine :=
-  mkResourceMachine {
+  mkResourceMachine@{
     --- Creates a ;Transaction;.
     create : (roots : Set CommitmentTree.Root)
       -> (actions : Set Action)

Anoma/Transaction/Action.juvix

@@ -15,7 +15,7 @@ import Anoma.Utils open;
 --- - existence of consumed ;Resource;s in the commitment tree
 --- - non-existence of consumed ;Resource;s in the nullifier set.
 type Action :=
-  mkAction {
+  mkAction@{
     commitments : Set Resource.Commitment;
     nullifiers : Set Resource.Nullifier;
     proofRecords : Set ProofRecord;

Anoma/Transaction/AppData.juvix

@@ -6,14 +6,14 @@ import Stdlib.Data.Set as Set open using {Set};
 import Anoma.Utils open;
 
 --- A fixed-size data type encoding the lookup key of application.
-type AppDataKey := mkAppDataKey {unAppDataKey : MISSING_DEFINITION};
+type AppDataKey := mkAppDataKey@{unAppDataKey : MISSING_DEFINITION};
 
 --- A fixed-size data type encoding the lookup value of application data.
-type AppDataValue := mkAppDataValue {unAppDataValue : MISSING_DEFINITION};
+type AppDataValue := mkAppDataValue@{unAppDataValue : MISSING_DEFINITION};
 
 --- A type describing an app data map entry.
 type AppDataEntry :=
-  mkAppDataEntry {
+  mkAppDataEntry@{
     key : AppDataKey;
     value : AppDataValue
   };

Anoma/Transaction/Metadata.juvix

@@ -9,14 +9,14 @@ import Anoma.Utils open;
 --- The metadata that can be associated with a ;Transaction;.
 --- The metadata that can used by actors to identify preferrable ;Transaction;s and specify information flow control properties.
 type Metadata :=
-  mkMetadata {
+  mkMetadata@{
     preference : Preference;
     informationFlowControlPredicate : InformationFlowControlPredicate
   };
 
 --- A composite structure containing a ;Transaction; with ;Metadata;
 type TransactionWithMetadata :=
-  createWithMetadata {
+  createWithMetadata@{
     transaction : Transaction;
     metadata : Metadata
   };

Anoma/Transaction/Object.juvix

@@ -12,7 +12,7 @@ import Anoma.Utils open;
 --- A record describing a transaction object, the entity constituting a state transition in Anoma.
 positive
 type Transaction :=
-  mkTransaction {
+  mkTransaction@{
     roots : Set CommitmentTree.Root;
     actions : Set Action;
     delta : Delta;

Anoma/Transaction/Preference.juvix

@@ -4,7 +4,7 @@ import Anoma.Transaction.Object open using {Transaction};
 import Anoma.Utils open;
 
 --- A fixed-size type describing the unit interval `[0,1]`.
-type UnitInterval := mkUnitInterval {unUnitInterval : MISSING_DEFINITION};
+type UnitInterval := mkUnitInterval@{unUnitInterval : MISSING_DEFINITION};
 
 --- The preference function signature.
 Preference : Type := (tx : Transaction) -> UnitInterval;

Anoma/Utils.juvix

@@ -31,7 +31,7 @@ ANOMA_BACKEND_IMPLEMENTATION : {A : Type} → A :=
 --- dynamically-sized.
 trait
 type Ref DataType RefType :=
-  mkRef {
+  mkRef@{
     toRef : DataType -> RefType;
     fromRef : RefType -> DataType
   };