Skip to content

Commit

Permalink
fix: name clashes
Browse files Browse the repository at this point in the history
  • Loading branch information
heueristik committed Oct 1, 2024
1 parent 594def0 commit db5f54a
Show file tree
Hide file tree
Showing 7 changed files with 30 additions and 30 deletions.
2 changes: 1 addition & 1 deletion Anoma/Identity/Types.juvix → Anoma/Identity/Object.juvix
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
module Anoma.Identity.Types;
module Anoma.Identity.Object;

import Stdlib.Prelude open;
import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
Expand Down
8 changes: 4 additions & 4 deletions Anoma/State/ResourceMachine.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module Anoma.State.ResourceMachine;

import Stdlib.Prelude open;
import Data.Set as Set open using {Set};
import Anoma.Transaction.Object as Transaction open using {Transaction; create; compose; verify};
import Anoma.Transaction.Object as Transaction open using {Transaction; mkTransaction; composeTransactions; verifyTransaction};
import Anoma.State.CommitmentTree as CommitmentTree open using {Root};
import Anoma.Transaction.Action as Action open;
import Anoma.Delta as Delta open using {Delta};
Expand Down Expand Up @@ -32,7 +32,7 @@ type ResourceMachine :=
instance
Concrete-ResourceMachine : ResourceMachine :=
mkResourceMachine@{
create := Transaction.create;
compose := Transaction.compose;
verify := Transaction.verify
create := Transaction.mkTransaction;
compose := Transaction.composeTransactions;
verify := Transaction.verifyTransaction
};
14 changes: 7 additions & 7 deletions Anoma/Transaction/Action.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ import Anoma.Transaction.AppData open using {AppData};
--- - existence of consumed ;Resource;s in the commitment tree
--- - non-existence of consumed ;Resource;s in the nullifier set.
type Action :=
create {
mkAction {
commitments : Set Resource.Commitment;
nullifiers : Set Resource.Nullifier;
proofs : ProofRecordSet;
Expand All @@ -28,7 +28,7 @@ type DisjointSetError :=
| NonDisjointNullifiersError (Set Resource.Nullifier);

--- Composes two ;Action; objects.
compose (a1 a2 : Action) : Result DisjointSetError Action :=
composeActions (a1 a2 : Action) : Result DisjointSetError Action :=
case
disjointUnion (Action.commitments a1) (Action.commitments a2)
, disjointUnion (Action.nullifiers a1) (Action.nullifiers a2)
Expand All @@ -37,23 +37,23 @@ compose (a1 a2 : Action) : Result DisjointSetError Action :=
| _, error duplicatedNullifiers := error (NonDisjointNullifiersError duplicatedNullifiers)
| ok commitments, ok nullifiers :=
ok
create@{
mkAction@{
commitments;
nullifiers;
appData := union (Action.appData a1) (Action.appData a2);
proofs := ProofRecordSet.empty
};

--- Verifies an ;Action; by verifying all proofs in the ;ProofRecordSet;.
verify (a : Action) : Bool := ProofRecordSet.verify (Action.proofs a);
verifyAction (a : Action) : Bool := ProofRecordSet.verify (Action.proofs a);

module ActionInternal;
--- Compares two ;Action; objects.
compare (lhs rhs : Action) : Ordering :=
let
compare (lhs rhs : Action) : Ordering :=
let
prod (a : Action) : _ :=
Action.commitments a, Action.nullifiers a, Action.proofs a, Action.appData a;
in Ord.cmp (prod lhs) (prod rhs);
in Ord.cmp (prod lhs) (prod rhs);

--- Implements the ;Ord; trait for ;Action;.
instance
Expand Down
12 changes: 6 additions & 6 deletions Anoma/Transaction/Index.juvix
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
module Anoma.Transaction.Index;

import Anoma.Transaction.Action open public;
import Anoma.Transaction.AppData open public;
import Anoma.Transaction.Delta open public;
import Anoma.Transaction.InformationFlow open public;
import Anoma.Transaction.Metadata open public;
import Anoma.Transaction.Action open public;
import Anoma.Transaction.AppData open public;
import Anoma.Transaction.Delta open public;
import Anoma.Transaction.InformationFlow open public;
import Anoma.Transaction.Metadata open public;
import Anoma.Transaction.Preference open public;
import Anoma.Transaction.Object open public;
import Anoma.Transaction.Object open public;
12 changes: 6 additions & 6 deletions Anoma/Transaction/Metadata.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module Anoma.Transaction.Metadata;

import Stdlib.Prelude open;
import Anoma.Transaction.Object as Transaction open using {Transaction};
import Anoma.Transaction.Preference as Preference open using {Preference; compose};
import Anoma.Transaction.Preference as Preference open using {Preference; composePreferences};
import Anoma.Transaction.InformationFlow open using {InformationFlowControlPredicate};

--- The metadata that can be associated with a ;Transaction;.
Expand All @@ -24,20 +24,20 @@ type TransactionWithMetadata :=

--- Composes two ;TransactionWithMetadata; objects.
--- NOTE: For the private testnet, this is not required yet.
compose (txwm1 txwm2 : TransactionWithMetadata) : TransactionWithMetadata :=
composeTransactionsWithMetadata (txwm1 txwm2 : TransactionWithMetadata) : TransactionWithMetadata :=
let
meta1 := TransactionWithMetadata.metadata txwm1;
meta2 := TransactionWithMetadata.metadata txwm2;
in createWithMetadata@{
transaction :=
Transaction.compose@{
Transaction.composeTransactions@{
tx1 := TransactionWithMetadata.transaction txwm1;
tx2 := TransactionWithMetadata.transaction txwm2
};
metadata :=
mkMetadata@{
preference :=
Preference.compose@{
Preference.composePreferences@{
f1 := Metadata.preference meta1;
f2 := Metadata.preference meta2
};
Expand All @@ -49,5 +49,5 @@ compose (txwm1 txwm2 : TransactionWithMetadata) : TransactionWithMetadata :=
};

--- Verifies a ;TransactionWithMetadata;.
verify (txwm : TransactionWithMetadata) : Bool :=
Transaction.verify (TransactionWithMetadata.transaction txwm);
verifyTransactionWithMetadata (txwm : TransactionWithMetadata) : Bool :=
Transaction.verifyTransaction (TransactionWithMetadata.transaction txwm);
10 changes: 5 additions & 5 deletions Anoma/Transaction/Object.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -13,25 +13,25 @@ import Anoma.Proving.DeltaProof as DeltaProof;
--- A record describing a transaction object, the entity constituting a state transition in Anoma.
positive
type Transaction :=
create {
mkTransaction {
roots : Set CommitmentTree.Root;
actions : Set Action;
delta : Delta;
deltaProof : DeltaProof.ProofRecord
};

--- Composes two ;Transaction; objects.
compose (tx1 tx2 : Transaction) : Transaction :=
create@{
composeTransactions (tx1 tx2 : Transaction) : Transaction :=
mkTransaction@{
roots := union (Transaction.roots tx1) (Transaction.roots tx2);
actions := union (Transaction.actions tx1) (Transaction.actions tx2);
delta := AdditivelyHomomorphic.add (Transaction.delta tx1) (Transaction.delta tx2);
deltaProof := DeltaProof.aggregate (Transaction.deltaProof tx1) (Transaction.deltaProof tx2)
};

--- Verifies a ;Transaction;.
verify (tx : Transaction) : Bool :=
all (a in Set.toList (Transaction.actions tx)) {Action.verify a}
verifyTransaction (tx : Transaction) : Bool :=
all (a in Set.toList (Transaction.actions tx)) {Action.verifyAction a}
&& DeltaProof.verify (Transaction.deltaProof tx);

--- Returns the ;Resource.Commitment; ;Set; of all ;Action;s in a ;Transaction; or the intersection ;Set;.
Expand Down
2 changes: 1 addition & 1 deletion Anoma/Transaction/Preference.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -9,4 +9,4 @@ axiom UnitInterval : Type;
Preference : Type := (tx : Transaction) -> UnitInterval;

--- The preference function composition function.
axiom compose : (f1 f2 : Preference) -> Preference;
axiom composePreferences : (f1 f2 : Preference) -> Preference;

0 comments on commit db5f54a

Please sign in to comment.