refactor: simplified exports

Anoma/Delta.juvix

@@ -1,7 +1,7 @@
 module Anoma.Delta;
 
 import Anoma.Math as Math open;
-import Anoma.Utils open using {MISSING_DEFINITION; MISSING_ANOMA_BUILTIN; ANOMA_BACKEND_IMPLEMENTATION};
+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.

Anoma/Identity/External.juvix

@@ -2,7 +2,7 @@ module Anoma.Identity.External;
 
 import Stdlib.Prelude open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
-import Anoma.Utils open using {MISSING_DEFINITION; MISSING_ANOMA_BUILTIN};
+import Anoma.Utils open;
 
 --- A fixed-size data type describing an external identity.
 type ExternalIdentity := mkExternalIdentity {unExternalIdentity : MISSING_DEFINITION};

Anoma/Identity/Internal.juvix

@@ -2,7 +2,7 @@ module Anoma.Identity.Internal;
 
 import Stdlib.Prelude open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
-import Anoma.Utils open using {MISSING_DEFINITION; MISSING_ANOMA_BUILTIN};
+import Anoma.Utils open;
 
 --- A fixed-size data type describing an internal identity.
 type InternalIdentity := mkInternalIdentity {unInternalIdentity : MISSING_DEFINITION};

Anoma/Identity/Signing/Types.juvix

@@ -3,7 +3,7 @@ module Anoma.Identity.Signing.Types;
 import Stdlib.Prelude open;
 import Anoma.Identity.Internal open;
 import Anoma.Identity.External open;
-import Anoma.Utils open using {MISSING_DEFINITION; MISSING_ANOMA_BUILTIN};
+import Anoma.Utils open;
 
 type Signature := mkSignature {unSignature : MISSING_DEFINITION};
 

Anoma/Proving/ComplianceProof.juvix

@@ -4,7 +4,7 @@ module Anoma.Proving.ComplianceProof;
 import Stdlib.Prelude open;
 import Anoma.Proving.Types as Parametrized open using {module Compliance};
 import Anoma.Proving.System as Parametrized open using {ProvingSystem};
-import Anoma.Utils open using {MISSING_ANOMA_BUILTIN};
+import Anoma.Utils open;
 
 ProofRecord : Type :=
   Parametrized.ProofRecord Compliance.Proof Compliance.VerifyingKey Compliance.Witness;

Anoma/Proving/DeltaProof.juvix

@@ -4,7 +4,7 @@ module Anoma.Proving.DeltaProof;
 import Stdlib.Prelude open;
 import Anoma.Proving.Types as Parametrized open using {module Delta};
 import Anoma.Proving.System as Parametrized open using {ProvingSystem};
-import Anoma.Utils open using {MISSING_ANOMA_BUILTIN; ANOMA_BACKEND_IMPLEMENTATION};
+import Anoma.Utils open;
 
 ProofRecord : Type := Parametrized.ProofRecord Delta.Proof Delta.VerifyingKey Delta.Witness;
 

Anoma/Proving/ProofRecordSet.juvix

@@ -7,7 +7,7 @@ import Anoma.Proving.ComplianceProof as ComplianceProof open;
 import Anoma.Proving.ResourceLogicProof as ResourceLogicProof open;
 import Anoma.Proving.DeltaProof as DeltaProof open;
 import Anoma.Proving.Types open;
-import Anoma.Utils open using {MISSING_ANOMA_BUILTIN};
+import Anoma.Utils open;
 
 --- A proof record set.
 type ProofRecordSet :=

Anoma/Proving/ResourceLogicProof.juvix

@@ -4,7 +4,7 @@ module Anoma.Proving.ResourceLogicProof;
 import Stdlib.Prelude open;
 import Anoma.Proving.Types as Parametrized open using {module ResourceLogic};
 import Anoma.Proving.System as Parametrized open using {ProvingSystem};
-import Anoma.Utils open using {MISSING_ANOMA_BUILTIN};
+import Anoma.Utils open;
 
 ProofRecord : Type :=
   Parametrized.ProofRecord ResourceLogic.Proof ResourceLogic.VerifyingKey ResourceLogic.Witness;

Anoma/Proving/Types.juvix

@@ -6,7 +6,7 @@ import Data.Set as Set open using {Set};
 import Anoma.Resource.Object open using {Resource};
 import Anoma.Resource.Types open using {Commitment; Nullifier};
 import Anoma.Transaction.AppData open using {AppData};
-import Anoma.Utils open using {UNUSED; MISSING_DEFINITION};
+import Anoma.Utils open;
 
 --- A record describing a proof record, a map entry constituted by a VerifyingKey as the lookup-key
 --- and a Proof and associated Witness as the value.

Anoma/Resource/Computable/Commitment.juvix

@@ -4,7 +4,7 @@ import Stdlib.Prelude open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
 import Anoma.Resource.Types open using {Commitment};
 import Anoma.Resource.Object open using {Resource};
-import Anoma.Utils open using {MISSING_ANOMA_BUILTIN};
+import Anoma.Utils open;
 
 --- Computes the ;Commitment; of a ;Resource;.
 commitment (resource : Resource) : Commitment := MISSING_ANOMA_BUILTIN;

Anoma/Resource/Computable/Delta.juvix

@@ -4,7 +4,7 @@ import Anoma.Delta open using {Delta};
 import Anoma.Resource.Object open using {Resource; module Resource};
 import Anoma.Resource.Types open using {Kind; Quantity};
 import Anoma.Resource.Computable.Kind as Computable open;
-import Anoma.Utils open using {MISSING_ANOMA_BUILTIN};
+import Anoma.Utils open;
 
 module ResourceDeltaInternal;
   --- The delta function as defined in the RM specs.

Anoma/Resource/Computable/Kind.juvix

@@ -2,7 +2,7 @@ module Anoma.Resource.Computable.Kind;
 
 import Anoma.Resource.Object open using {Resource; module Resource};
 import Anoma.Resource.Types open using {LogicRef; LabelRef; Kind};
-import Anoma.Utils open using {MISSING_ANOMA_BUILTIN};
+import Anoma.Utils open;
 
 module KindInternal;
   --- The kind function as defined in the RM specs.

Anoma/Resource/Computable/Nullifier.juvix

@@ -4,7 +4,7 @@ import Stdlib.Prelude open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
 import Anoma.Resource.Types open using {Nullifier; NullifierKey};
 import Anoma.Resource.Object open using {Resource};
-import Anoma.Utils open using {MISSING_ANOMA_BUILTIN};
+import Anoma.Utils open;
 
 --- Computes the ;Nullifier; of a ;Resource; given a ;NullifierKey;.
 nullifier (resource : Resource) (nullifierKey : NullifierKey) : Nullifier := MISSING_ANOMA_BUILTIN;

Anoma/Resource/Label.juvix

@@ -1,8 +1,7 @@
 module Anoma.Resource.Label;
 
-import Anoma.Utils open using {Ref; mkRef};
 import Anoma.Resource.Types open using {Label; LabelRef};
-import Anoma.Utils open using {MISSING_JUVIX_IMPLEMENTATION};
+import Anoma.Utils open;
 
 --- Computes the ;LabelRef; from the ;Label;.
 labelToRef (label : Label) : LabelRef := MISSING_JUVIX_IMPLEMENTATION;

Anoma/Resource/Logic.juvix

@@ -1,10 +1,9 @@
 module Anoma.Resource.Logic;
 
 import Stdlib.Prelude open;
-import Anoma.Utils open using {Ref; mkRef};
 import Anoma.Resource.Types open using {LogicRef};
 import Anoma.Proving.Types open using {module ResourceLogic};
-import Anoma.Utils open using {MISSING_ANOMA_BUILTIN};
+import Anoma.Utils open;
 
 --- The resource logic function signature.
 Logic : Type :=

Anoma/Resource/Types.juvix

@@ -2,7 +2,7 @@ module Anoma.Resource.Types;
 
 import Stdlib.Prelude open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
-import Anoma.Utils open using {MISSING_DEFINITION; MISSING_ANOMA_BUILTIN};
+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.

Anoma/Resource/Value.juvix

@@ -1,8 +1,7 @@
 module Anoma.Resource.Value;
 
-import Anoma.Utils open using {Ref; mkRef};
 import Anoma.Resource.Types open using {Value; ValueRef};
-import Anoma.Utils open using {MISSING_JUVIX_IMPLEMENTATION};
+import Anoma.Utils open;
 
 --- Computes the ;ValueRef; from the ;Value;.
 valueToRef (value : Value) : ValueRef := MISSING_JUVIX_IMPLEMENTATION;

Anoma/State/CommitmentTree.juvix

@@ -6,7 +6,7 @@ import Stdlib.Prelude open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
 import Data.Set as Set open using {Set};
 import Anoma.Resource.Types as Resource open using {Commitment};
-import Anoma.Utils open using {MISSING_DEFINITION};
+import Anoma.Utils open;
 
 --- A state root of the commitment tree.
 type Root := mkRoot {unRoot : MISSING_DEFINITION};

Anoma/Transaction/Action.juvix

@@ -7,7 +7,7 @@ import Anoma.Resource as Resource open;
 import Anoma.Proving.Types open using {ProofRecord};
 import Anoma.Proving.ProofRecordSet as ProofRecordSet open using {ProofRecordSet};
 import Anoma.Transaction.AppData open using {AppData};
-import Anoma.Utils open using {MISSING_ANOMA_BUILTIN};
+import Anoma.Utils open;
 
 --- The record describing an action and defining the proof context.
 --- Proofs includes resource logic and compliance proofs of created and consumed resources.

Anoma/Transaction/AppData.juvix

@@ -3,7 +3,7 @@ module Anoma.Transaction.AppData;
 import Stdlib.Prelude open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
 import Data.Set as Set open using {Set};
-import Anoma.Utils open using {MISSING_DEFINITION};
+import Anoma.Utils open;
 
 --- A fixed-size data type encoding the lookup key of application.
 type AppDataKey := mkAppDataKey {unAppDataKey : MISSING_DEFINITION};

Anoma/Transaction/Delta.juvix

@@ -1,8 +1,8 @@
 module Anoma.Transaction.Delta;
 
 import Anoma.Delta open using {Delta};
-import Anoma.Utils open using {MISSING_ANOMA_BUILTIN};
 import Anoma.Transaction.Object open using {Transaction};
+import Anoma.Utils open;
 
 --- Computes the ;Transaction; ;Delta;.
 delta (transaction : Transaction) : Delta := MISSING_ANOMA_BUILTIN;

Anoma/Transaction/InformationFlow.juvix

@@ -4,7 +4,7 @@ import Stdlib.Prelude open;
 import Data.Set as Set open using {Set; toList; member?};
 import Anoma.Identity open using {ExternalIdentity};
 import Anoma.Transaction.Object open using {Transaction};
-import Anoma.Utils open using {MISSING_DEFINITION; NOT_REQUIRED};
+import Anoma.Utils open;
 
 --- The information flow predicate function type definition.
 InformationFlowControlPredicate : Type := (tx : Transaction) -> (id : ExternalIdentity) -> Bool;

Anoma/Transaction/Metadata.juvix

@@ -4,7 +4,7 @@ import Stdlib.Prelude open;
 import Anoma.Transaction.Object as Transaction open using {Transaction};
 import Anoma.Transaction.Preference as Preference open using {Preference; composePreferences};
 import Anoma.Transaction.InformationFlow open using {InformationFlowControlPredicate};
-import Anoma.Utils open using {NOT_REQUIRED};
+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.

Anoma/Transaction/Object.juvix

@@ -7,7 +7,7 @@ import Anoma.State.CommitmentTree as CommitmentTree;
 import Anoma.Transaction.Action open using {Action};
 import Anoma.Delta as Delta open using {Delta};
 import Anoma.Proving.DeltaProof as DeltaProof;
-import Anoma.Utils open using {MISSING_ANOMA_BUILTIN};
+import Anoma.Utils open;
 
 --- A record describing a transaction object, the entity constituting a state transition in Anoma.
 positive

Anoma/Transaction/Preference.juvix

@@ -1,7 +1,7 @@
 module Anoma.Transaction.Preference;
 
 import Anoma.Transaction.Object open using {Transaction};
-import Anoma.Utils open using {MISSING_DEFINITION; NOT_REQUIRED};
+import Anoma.Utils open;
 
 --- A fixed-size type describing the unit interval `[0,1]`.
 type UnitInterval := mkUnitInterval {unUnitInterval : MISSING_DEFINITION};