diff --git a/Anoma/Delta.juvix b/Anoma/Delta.juvix index f5fa4b0..1ac3f57 100644 --- a/Anoma/Delta.juvix +++ b/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. diff --git a/Anoma/Identity/External.juvix b/Anoma/Identity/External.juvix index 16c3c50..fc80b05 100644 --- a/Anoma/Identity/External.juvix +++ b/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}; diff --git a/Anoma/Identity/Internal.juvix b/Anoma/Identity/Internal.juvix index e463b58..5b47c37 100644 --- a/Anoma/Identity/Internal.juvix +++ b/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}; diff --git a/Anoma/Identity/Signing/Types.juvix b/Anoma/Identity/Signing/Types.juvix index 5e7db71..cf20b96 100644 --- a/Anoma/Identity/Signing/Types.juvix +++ b/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}; diff --git a/Anoma/Proving/ComplianceProof.juvix b/Anoma/Proving/ComplianceProof.juvix index 94a245c..2c399ad 100644 --- a/Anoma/Proving/ComplianceProof.juvix +++ b/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; diff --git a/Anoma/Proving/DeltaProof.juvix b/Anoma/Proving/DeltaProof.juvix index efe7832..7eda5ad 100644 --- a/Anoma/Proving/DeltaProof.juvix +++ b/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; diff --git a/Anoma/Proving/ProofRecordSet.juvix b/Anoma/Proving/ProofRecordSet.juvix index 8dd6d56..3553175 100644 --- a/Anoma/Proving/ProofRecordSet.juvix +++ b/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 := diff --git a/Anoma/Proving/ResourceLogicProof.juvix b/Anoma/Proving/ResourceLogicProof.juvix index e126ae6..c9417ae 100644 --- a/Anoma/Proving/ResourceLogicProof.juvix +++ b/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; diff --git a/Anoma/Proving/Types.juvix b/Anoma/Proving/Types.juvix index 8c8575c..8432715 100644 --- a/Anoma/Proving/Types.juvix +++ b/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. diff --git a/Anoma/Resource/Computable/Commitment.juvix b/Anoma/Resource/Computable/Commitment.juvix index 4f5f0af..2b0d1c2 100644 --- a/Anoma/Resource/Computable/Commitment.juvix +++ b/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; diff --git a/Anoma/Resource/Computable/Delta.juvix b/Anoma/Resource/Computable/Delta.juvix index afe6b39..12850f3 100644 --- a/Anoma/Resource/Computable/Delta.juvix +++ b/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. diff --git a/Anoma/Resource/Computable/Kind.juvix b/Anoma/Resource/Computable/Kind.juvix index 3885c28..b6d98e5 100644 --- a/Anoma/Resource/Computable/Kind.juvix +++ b/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. diff --git a/Anoma/Resource/Computable/Nullifier.juvix b/Anoma/Resource/Computable/Nullifier.juvix index 952df56..95e2b97 100644 --- a/Anoma/Resource/Computable/Nullifier.juvix +++ b/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; diff --git a/Anoma/Resource/Label.juvix b/Anoma/Resource/Label.juvix index 2e3f51b..205bc2c 100644 --- a/Anoma/Resource/Label.juvix +++ b/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; diff --git a/Anoma/Resource/Logic.juvix b/Anoma/Resource/Logic.juvix index 56c4840..9b1357d 100644 --- a/Anoma/Resource/Logic.juvix +++ b/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 := diff --git a/Anoma/Resource/Types.juvix b/Anoma/Resource/Types.juvix index e5aa9f2..02de1b4 100644 --- a/Anoma/Resource/Types.juvix +++ b/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. diff --git a/Anoma/Resource/Value.juvix b/Anoma/Resource/Value.juvix index 83635b8..1328360 100644 --- a/Anoma/Resource/Value.juvix +++ b/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; diff --git a/Anoma/State/CommitmentTree.juvix b/Anoma/State/CommitmentTree.juvix index 756b3d7..ea28271 100644 --- a/Anoma/State/CommitmentTree.juvix +++ b/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}; diff --git a/Anoma/Transaction/Action.juvix b/Anoma/Transaction/Action.juvix index a7fd349..263dc2c 100644 --- a/Anoma/Transaction/Action.juvix +++ b/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. diff --git a/Anoma/Transaction/AppData.juvix b/Anoma/Transaction/AppData.juvix index 1152bfa..56c7d6e 100644 --- a/Anoma/Transaction/AppData.juvix +++ b/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}; diff --git a/Anoma/Transaction/Delta.juvix b/Anoma/Transaction/Delta.juvix index 21394d1..bc4a01f 100644 --- a/Anoma/Transaction/Delta.juvix +++ b/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; diff --git a/Anoma/Transaction/InformationFlow.juvix b/Anoma/Transaction/InformationFlow.juvix index 7772cd6..fa53da1 100644 --- a/Anoma/Transaction/InformationFlow.juvix +++ b/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; diff --git a/Anoma/Transaction/Metadata.juvix b/Anoma/Transaction/Metadata.juvix index 674e175..fd4a560 100644 --- a/Anoma/Transaction/Metadata.juvix +++ b/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. diff --git a/Anoma/Transaction/Object.juvix b/Anoma/Transaction/Object.juvix index de04059..a75d83d 100644 --- a/Anoma/Transaction/Object.juvix +++ b/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 diff --git a/Anoma/Transaction/Preference.juvix b/Anoma/Transaction/Preference.juvix index b893536..6ac234b 100644 --- a/Anoma/Transaction/Preference.juvix +++ b/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};