refactor

Anoma/Identity.juvix

@@ -0,0 +1,21 @@
+module Anoma.Identity;
+
+import Stdlib.Prelude open using {Eq; Ord; Ordering; mkOrd};
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+
+axiom ExternalIdentity : Type;
+
+axiom self : ExternalIdentity;
+
+module ExternalIdentityInternal;
+  axiom compare : ExternalIdentity -> ExternalIdentity -> Ordering;
+
+  instance
+  ExternalIdentity-Ord : Ord ExternalIdentity :=
+    mkOrd@{
+      cmp := compare
+    };
+
+  instance
+  ExternalIdentity-Eq : Eq ExternalIdentity := fromOrdToEq;
+end;

Anoma/Resource/Computable/Commitment.juvix

@@ -1,20 +1,22 @@
 module Anoma.Resource.Computable.Commitment;
 
-import Stdlib.Prelude open;
+import Stdlib.Prelude open using {Eq; Ord; Ordering; mkOrd};
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
 import Anoma.Resource.Types open;
 
 axiom Commitment : Type;
 
 axiom commitment : (resource : Resource) -> Commitment;
 
-axiom compare : Commitment -> Commitment -> Ordering;
+module CommitmentInternal;
+  axiom compare : Commitment -> Commitment -> Ordering;
 
-instance
-Commitment-Ord : Ord Commitment :=
-  mkOrd@{
-    cmp := compare
-  };
+  instance
+  Commitment-Ord : Ord Commitment :=
+    mkOrd@{
+      cmp := compare
+    };
 
-instance
-Commitment-Eq : Eq Commitment := fromOrdToEq;
+  instance
+  Commitment-Eq : Eq Commitment := fromOrdToEq;
+end;

Anoma/Resource/Computable/Delta.juvix

@@ -4,12 +4,12 @@ import Anoma.Delta open;
 import Anoma.Resource.Types open;
 import Anoma.Resource.Computable.Kind as Computable open;
 
-module Internal;
+module ResourceDeltaInternal;
   axiom delta : (kind : Kind) -> (quantity : Quantity) -> Delta;
 end;
 
 delta (resource : Resource) : Delta :=
-  Internal.delta@{
+  ResourceDeltaInternal.delta@{
     kind := Computable.kind resource;
     quantity := Resource.quantity resource
   };

Anoma/Resource/Computable/Kind.juvix

@@ -6,12 +6,12 @@ import Anoma.Resource.Label open;
 
 axiom Kind : Type;
 
-module Internal;
+module KindInternal;
   axiom kind : (logicRef : LogicRef) -> (labelRef : LabelRef) -> Kind;
 end;
 
 kind (resource : Resource) : Kind :=
-  Internal.kind@{
+  KindInternal.kind@{
     logicRef := Resource.logicRef resource;
     labelRef := Resource.labelRef resource
   };

Anoma/Resource/Computable/Nullifier.juvix

@@ -1,6 +1,6 @@
 module Anoma.Resource.Computable.Nullifier;
 
-import Stdlib.Prelude open;
+import Stdlib.Prelude open using {Eq; Ord; Ordering; mkOrd};
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
 import Anoma.Resource.Types open;
 
@@ -10,13 +10,15 @@ axiom NullifierKey : Type;
 
 axiom nullifier : (resource : Resource) -> (nullifierKey : NullifierKey) -> Nullifier;
 
-axiom compare : Nullifier -> Nullifier -> Ordering;
+module NullfierInternal;
+  axiom compare : Nullifier -> Nullifier -> Ordering;
 
-instance
-Nullifier-Ord : Ord Nullifier :=
-  mkOrd@{
-    cmp := compare
-  };
+  instance
+  Nullifier-Ord : Ord Nullifier :=
+    mkOrd@{
+      cmp := compare
+    };
 
-instance
-Nullifier-Eq : Eq Nullifier := fromOrdToEq;
+  instance
+  Nullifier-Eq : Eq Nullifier := fromOrdToEq;
+end;

Anoma/State/CommitmentTree.juvix

@@ -1,6 +1,7 @@
 module Anoma.State.CommitmentTree;
 
-import Stdlib.Prelude open using {Maybe; Bool};
+import Stdlib.Prelude open using {Maybe; Bool; Eq; Ord; Ordering; mkOrd};
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
 import Anoma.Resource.Index as Resource;
 
 axiom Root : Type;
@@ -16,3 +17,16 @@ type CommitmentTree :=
     verify : Resource.Commitment -> Path -> Root -> Bool;
     root : CommitmentTree -> Root
   };
+
+module RootInternal;
+  axiom compare : Root -> Root -> Ordering;
+
+  instance
+  Root-Ord : Ord Root :=
+    mkOrd@{
+      cmp := compare
+    };
+
+  instance
+  Root-Eq : Eq Root := fromOrdToEq;
+end;

Anoma/Transaction/Action.juvix

@@ -1,21 +1,84 @@
 module Anoma.Transaction.Action;
 
-import Stdlib.Prelude open using {Pair};
-import Data.Set as Set open using {Set};
+import Stdlib.Prelude open using {Pair; Eq; Ord; Ordering; mkOrd};
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+import Data.Set as Set open using {Set; union};
 
 import Anoma.Resource.Index as Resource;
 import Anoma.Proving.Types as Proving open;
 
-axiom AppDataKeyType : Type;
+module AppDataInternal;
+  axiom AppDataKey : Type;
 
-axiom AppDataValueType : Type;
+  axiom AppDataValue : Type;
 
-AppDataMap : Type := Set (Pair AppDataKeyType AppDataValueType);
+  axiom compareAppDataKey : AppDataKey -> AppDataKey -> Ordering;
+
+  axiom compareAppDataValue : AppDataValue -> AppDataValue -> Ordering;
+
+  instance
+  AppDataKey-Ord : Ord AppDataKey :=
+    mkOrd@{
+      cmp := compareAppDataKey
+    };
+
+  instance
+  AppDataKey-Eq : Eq AppDataKey := fromOrdToEq;
+
+  instance
+  AppDataValue-Ord : Ord AppDataValue :=
+    mkOrd@{
+      cmp := compareAppDataValue
+    };
+
+  instance
+  AppDataValue-Eq : Eq AppDataValue := fromOrdToEq;
+
+  AppDataMapEntry : Type := Pair AppDataKey AppDataValue;
+
+  AppDataMap : Type := Set AppDataMapEntry;
+end;
+
+open AppDataInternal using {AppDataMap as AppData} public;
 
 type Action :=
   mkAction {
     commitments : Set Resource.Commitment;
     nullifiers : Set Resource.Nullifier;
     proofs : Set Proving.ProofRecord;
-    appData : AppDataMap
+    appData : AppData
+  };
+
+compose (a1 a2 : Action) : Action :=
+  mkAction@{
+    commitments :=
+      union@{
+        s1 := Action.commitments a1;
+        s2 := Action.commitments a2
+      };
+    nullifiers :=
+      union@{
+        s1 := Action.nullifiers a1;
+        s2 := Action.nullifiers a2
+      };
+    -- TODO Proofs must be recomputed
+    proofs := Set.empty;
+    appData :=
+      union@{
+        s1 := Action.appData a1;
+        s2 := Action.appData a2
+      }
   };
+
+module ActionInternal;
+  axiom compare : Action -> Action -> Ordering;
+
+  instance
+  Action-Ord : Ord Action :=
+    mkOrd@{
+      cmp := compare
+    };
+
+  instance
+  Action-Eq : Eq Action := fromOrdToEq;
+end;

Anoma/Transaction/Delta.juvix

@@ -2,14 +2,13 @@ module Anoma.Transaction.Delta;
 
 import Stdlib.Prelude open using {Bool; List; for; ||};
 import Data.Set as Set open using {Set; union; member?};
-
 import Anoma.Delta as Delta open;
 import Anoma.Transaction.Types open;
 import Anoma.Transaction.Action open;
 import Anoma.Resource.Index as Resource open;
 import Anoma.MathProperty as MathProperty open;
 
-module Internal;
+module TransactionDeltaInternal;
   isInCommitmentSet (resource : Resource) (transaction : Transaction) : Bool :=
     let
       actions : List Action := Set.toList (Transaction.actions transaction);
@@ -32,7 +31,6 @@ module Internal;
         };
       nfs : Set Resource.Nullifier :=
         for (acc := Set.empty) (a in actions) {union acc (Action.nullifiers a)};
-
     in member? nf nfs;
 end;
 
@@ -43,11 +41,11 @@ delta
   : Delta :=
   for (acc := Delta.zero) (r in resources)
     {if
-      | Internal.isInCommitmentSet@{
+      | TransactionDeltaInternal.isInCommitmentSet@{
           resource := r;
           transaction
         }
-        || Internal.isInNullifierSet@{
+        || TransactionDeltaInternal.isInNullifierSet@{
           resource := r;
           nullifierKey;
           transaction

Anoma/Transaction/Index.juvix

@@ -1,5 +1,8 @@
 module Anoma.Transaction.Index;
 
-import Anoma.Transaction.Types open public;
-import Anoma.Transaction.Action open public;
-import Anoma.Transaction.Delta open public;
+import Anoma.Transaction.Types open using {Transaction; Constructor} public;
+import Anoma.Transaction.Preference open using {Preference};
+import Anoma.Transaction.InformationFlow open using {InformationFlowControlPredicate};
+import Anoma.Transaction.Metadata open using {TransactionWithMetadata; Metadata} public;
+import Anoma.Transaction.Action open using {Action; compose};
+import Anoma.Transaction.Delta open using {delta};

Anoma/Transaction/InformationFlow.juvix

@@ -0,0 +1,32 @@
+module Anoma.Transaction.InformationFlow;
+
+import Stdlib.Prelude open;
+import Data.Set as Set open using {Set; toList; member?};
+
+import Anoma.Identity open;
+import Anoma.Transaction.Types as Transaction open;
+
+InformationFlowControlPredicate : Type := (tx : Transaction) -> (id : ExternalIdentity) -> Bool;
+
+axiom Hash : Type;
+
+type BaseData :=
+  | AllowAny
+  | AllowOnly (Set ExternalIdentity)
+  | RequireShielded (Set Hash)
+  -- TODO Use ;Set; instead of ;List;
+  | And (List BaseData)
+  | Or (List BaseData);
+
+terminating
+basePredicate (baseData : BaseData) : InformationFlowControlPredicate :=
+  case baseData of
+    | None := \ {_ _ := true}
+    | AllowOnly identites := \ {_ self := member? self identites}
+    {-
+        TODO How to deal with hashes?
+        | RequireShielded hashes := \ {tx _ := not (any (h in hashes) member? h ??)}
+        -}
+    | RequireShielded hashes := \ {_ _ := false}
+    | And predicates := \ {tx id := all (p in predicates) basePredicate p tx id}
+    | Or predicates := \ {tx id := any (p in predicates) basePredicate p tx id};

Anoma/Transaction/Metadata.juvix

@@ -0,0 +1,39 @@
+module Anoma.Transaction.Metadata;
+
+import Stdlib.Prelude open using {&&};
+import Anoma.Transaction.Types as Transaction open;
+import Anoma.Transaction.Preference as Preference open;
+import Anoma.Transaction.InformationFlow open;
+
+type Metadata :=
+  mkMetadata {
+    preference : Preference;
+    informationFlowControlPredicate : InformationFlowControlPredicate
+  };
+
+type TransactionWithMetadata :=
+  mkTransactionWithMetadata {
+    transaction : Transaction;
+    metadata : Metadata
+  };
+
+compose (txwm1 txwm2 : TransactionWithMetadata) : TransactionWithMetadata :=
+  let
+    meta1 := TransactionWithMetadata.metadata txwm1;
+    meta2 := TransactionWithMetadata.metadata txwm2;
+    pref1 := Metadata.preference meta1;
+    pref2 := Metadata.preference meta2;
+    ifcp1 := Metadata.informationFlowControlPredicate meta1;
+    ifcp2 := Metadata.informationFlowControlPredicate meta2;
+  in mkTransactionWithMetadata@{
+    transaction :=
+      Transaction.compose@{
+        tx1 := TransactionWithMetadata.transaction txwm1;
+        tx2 := TransactionWithMetadata.transaction txwm2
+      };
+    metadata :=
+      mkMetadata@{
+        preference := Preference.composition pref1 pref2;
+        informationFlowControlPredicate := \ {tx id := ifcp1 tx id && ifcp2 tx id}
+      }
+  };

Anoma/Transaction/Preference.juvix

@@ -0,0 +1,9 @@
+module Anoma.Transaction.Preference;
+
+import Anoma.Transaction.Types as Transaction open;
+
+axiom UnitInterval : Type;
+
+Preference : Type := Transaction -> UnitInterval;
+
+axiom composition : Preference -> Preference -> Preference;