docs: added more judoc comments

Anoma/Proving/Types.juvix

@@ -3,12 +3,19 @@ module Anoma.Proving.Types;
 import Stdlib.Prelude open using {Pair};
 import Anoma.Resource.Index as Resource open using {Witness};
 
+--- A fixed-size data type encoding a proof.
 axiom Proof : Type;
 
+--- A fixed-size data type encoding a verifying key containing the data,
+--- along with a ;Resource.Witness;, to verify a proof.
 axiom VerifyingKey : Type;
 
+--- A fixed-size data type encoding a proving key containing the data,
+--- along with a ;Resource.Instance; and ;Resource.Witness;, to produce a proof.
 axiom ProvingKey : Type;
 
+--- A record describing a proof record, a map entry constituted by a ;VerifyingKey; as the lookup-key
+--- and a ;Proof; and associated ;Resource.Witness; as the value.
 ProofRecord : Type := Pair VerifyingKey (Pair Proof Resource.Witness);
 
 module DeltaProof;

Anoma/Resource/Computable/Commitment.juvix

@@ -22,6 +22,7 @@ module CommitmentInternal;
       cmp := compare
     };
 
+  --- Implements the ;Eq; trait for ;Commitment;.
   instance
   Commitment-Eq : Eq Commitment := fromOrdToEq;
 end;

Anoma/Resource/Computable/Nullifier.juvix

@@ -25,6 +25,7 @@ module NullfierInternal;
       cmp := compare
     };
 
+  --- Implements the ;Eq; trait for ;Nullifier;.
   instance
   Nullifier-Eq : Eq Nullifier := fromOrdToEq;
 end;

Anoma/Resource/Label.juvix

@@ -8,6 +8,7 @@ axiom Label : Type;
 --- NOTE: For the private testnet, this is allowed to be the identity function.
 axiom labelRef : Label -> LabelRef;
 
+--- Implements the ;Ref; trait for ;Label;.
 instance
 Label-Ref : Ref Label LabelRef :=
   mkRef@{

Anoma/Resource/Logic.juvix

@@ -13,6 +13,7 @@ Logic : Type := Tag -> Instance -> Witness -> Bool;
 --- NOTE: For the private testnet, this is allowed to be the identity function.
 axiom logicRef : Logic -> LogicRef;
 
+--- Implements the ;Ref; trait for ;Logic;.
 instance
 Logic-Ref : Ref Logic LogicRef :=
   mkRef@{

Anoma/Resource/Types.juvix

@@ -14,14 +14,21 @@ axiom LabelRef : Type;
 --- NOTE: For the private testnet, the requirement can be relaxed by allowing ;ValueRef; to be dynamically-sized.
 axiom ValueRef : Type;
 
+--- A fixed-size data type encoding the quantity of a resource.
 axiom Quantity : Type;
 
+--- A fixed-size data type encoding the public commitment to the private nullifier key.
 axiom NullifierKeyCommitment : Type;
 
+--- A fixed-size data type encoding a number to be used once,
+--- NOTE: A value having an at most negligible chance of repeating is sufficient.
 axiom Nonce : Type;
 
+--- A fixed-size data type encoding a randomness seed.
+--- NOTE: This seed provides pseudo randomness and cannot be expected to provide true randomness.
 axiom RandSeed : Type;
 
+--- A record describing a resource, the atomic unit of state in the Anoma state model.
 type Resource :=
   mkResource {
     logicRef : LogicRef;

Anoma/Resource/Value.juvix

@@ -8,6 +8,7 @@ axiom Value : Type;
 --- NOTE: For the private testnet, this is allowed to be the identity function.
 axiom valueRef : Value -> ValueRef;
 
+--- Implements the ;Ref; trait for ;Value;.
 instance
 Value-Ref : Ref Value ValueRef :=
   mkRef@{

Anoma/State/CommitmentTree.juvix

@@ -5,8 +5,10 @@ import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
 import Data.Set as Set open using {Set};
 import Anoma.Resource.Computable.Commitment as Resource open using {Commitment};
 
+--- A state root of the resource machine commitment tree.
 axiom Root : Type;
 
+--- A path in the resource machine commitment tree.
 axiom Path : Type;
 
 --- The interface of the resource machine commitment tree.
@@ -39,6 +41,7 @@ module RootInternal;
       cmp := compare
     };
 
+  --- Implements the ;Eq; trait for ;Root;.
   instance
   Root-Eq : Eq Root := fromOrdToEq;
 end;

Anoma/State/NullifierSet.juvix

@@ -6,7 +6,10 @@ import Anoma.Resource.Computable.Nullifier as Resource open using {Nullifier};
 --- The interface of the resource machine nullifier set.
 trait
 type NullifierSet :=
-  mkAccumulator {
+  mkNullifierSet {
+    --- Adds a ;Resource.Nullifier; to the ;NullifierSet;.
     add : Resource.Nullifier -> NullifierSet;
+
+    --- Checks if a ;Resource.Nullifier; exists in the ;NullifierSet;.
     exists : Resource.Nullifier -> Bool
   };

Anoma/Transaction/Action.juvix

@@ -8,39 +8,52 @@ import Anoma.Resource.Index as Resource open using {Resource};
 import Anoma.Proving.Types open using {ProofRecord};
 
 module AppDataInternal;
+  --- A fixed-size data type encoding the lookup key of application data being part of an action.
   axiom AppDataKey : Type;
 
+  --- A fixed-size data type encoding the lookup value of application data being part of an action.
   axiom AppDataValue : Type;
 
+  --- Compares two ;AppDataKey;s.
   axiom compareAppDataKey : AppDataKey -> AppDataKey -> Ordering;
 
+  --- Compares two ;AppDataValue;s.
   axiom compareAppDataValue : AppDataValue -> AppDataValue -> Ordering;
 
+  --- Implements the ;Ord; trait for ;AppDataKey;.
   instance
   AppDataKey-Ord : Ord AppDataKey :=
     mkOrd@{
       cmp := compareAppDataKey
     };
 
+  --- Implements the ;Eq; trait for ;AppDataKey;.
   instance
   AppDataKey-Eq : Eq AppDataKey := fromOrdToEq;
 
+  --- Implements the ;Ord; trait for ;AppDataValue;.
   instance
   AppDataValue-Ord : Ord AppDataValue :=
     mkOrd@{
       cmp := compareAppDataValue
     };
 
+  --- Implements the ;Eq; trait for ;AppDataValue;.
   instance
   AppDataValue-Eq : Eq AppDataValue := fromOrdToEq;
 
-  AppDataMapEntry : Type := Pair AppDataKey AppDataValue;
+  --- A type describing an app data map entry.
+  AppDataEntry : Type := Pair AppDataKey AppDataValue;
 
-  AppDataMap : Type := Set AppDataMapEntry;
+  --- A type describing an app data map.
+  AppData : Type := Set AppDataEntry;
 end;
 
-open AppDataInternal using {AppDataMap as AppData} public;
+open AppDataInternal using {AppData} public;
 
+--- The record describing an action and defining the proof context.
+--- A proof created in the context of an action is assumed to have guaranteed
+--- access only to the resources associated with the action.
 type Action :=
   mkAction {
     commitments : Set Resource.Commitment;
@@ -49,6 +62,7 @@ type Action :=
     appData : AppData
   };
 
+--- Composes two ;Action; objects.
 compose (a1 a2 : Action) : Action :=
   mkAction@{
     commitments :=
@@ -61,24 +75,27 @@ compose (a1 a2 : Action) : Action :=
         s1 := Action.nullifiers a1;
         s2 := Action.nullifiers a2
       };
-    -- TODO Proofs must be recomputed. Should this happen as part of `compose`?
-    proofs := Set.empty;
     appData :=
       union@{
         s1 := Action.appData a1;
         s2 := Action.appData a2
-      }
+      };
+    -- TODO Proofs must be recomputed. Should this happen as part of `compose`?
+    proofs := Set.empty
   };
 
 module ActionInternal;
-  axiom compare : Action -> Action -> Ordering;
+  --- Compares two ;Action; objects.
+  axiom compare : (a1 a2 : Action) -> Ordering;
 
+  --- Implements the ;Ord; trait for ;Action;.
   instance
   Action-Ord : Ord Action :=
     mkOrd@{
       cmp := compare
     };
 
+  --- Implements the ;Eq; trait for ;Action;.
   instance
   Action-Eq : Eq Action := fromOrdToEq;
 end;

Anoma/Transaction/Delta.juvix

@@ -3,51 +3,19 @@ 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 using {Delta; zero};
-import Anoma.Transaction.Types open;
-import Anoma.Transaction.Action open;
+import Anoma.Transaction.Types open using {Transaction; commitmentSet; nullfierSet};
 import Anoma.Resource.Index as Resource open using {Resource};
 import Anoma.MathProperty as MathProperty open;
 
-module TransactionDeltaInternal;
-  isInCommitmentSet (resource : Resource) (transaction : Transaction) : Bool :=
-    let
-      actions : List Action := Set.toList (Transaction.actions transaction);
-      cm : Resource.Commitment := Resource.commitment resource;
-      cms : Set Resource.Commitment :=
-        for (acc := Set.empty) (a in actions) {union acc (Action.commitments a)};
-    in member? cm cms;
-
-  isInNullifierSet
-    (resource : Resource)
-    (nullifierKey : Resource.NullifierKey)
-    (transaction : Transaction)
-    : Bool :=
-    let
-      actions : Set Action := Transaction.actions transaction;
-      nf : Resource.Nullifier :=
-        Resource.nullifier@{
-          resource;
-          nullifierKey
-        };
-      nfs : Set Resource.Nullifier :=
-        for (acc := Set.empty) (a in actions) {union acc (Action.nullifiers a)};
-    in member? nf nfs;
-end;
-
+--- Computes the ;Delta; of a ;Resource; ;Set; being part of a ;Transaction;.
 delta
   (resources : Set Resource)
   (nullifierKey : Resource.NullifierKey)
   (transaction : Transaction)
   : Delta :=
   for (acc := zero) (r in resources)
     {if
-      | TransactionDeltaInternal.isInCommitmentSet@{
-          resource := r;
-          transaction
-        }
-        || TransactionDeltaInternal.isInNullifierSet@{
-          resource := r;
-          nullifierKey;
-          transaction
-        } := AdditivelyHomomorphic.add acc (Resource.delta r)
+      | member? (Resource.commitment r) (commitmentSet transaction)
+        || member? (Resource.nullifier r nullifierKey) (nullfierSet transaction) :=
+        AdditivelyHomomorphic.add acc (Resource.delta r)
       | else := acc};

Anoma/Transaction/Types.juvix

@@ -1,12 +1,16 @@
 module Anoma.Transaction.Types;
 
 import Data.Set as Set open using {Set; union};
-import Anoma.Transaction.Action open using {Action; compose};
+import Stdlib.Prelude open using {for};
+import Anoma.Resource.Computable.Commitment as Resource open using {Commitment};
+import Anoma.Resource.Computable.Nullifier as Resource open using {Nullifier};
 import Anoma.State.CommitmentTree as CommitmentTree open using {Root};
+import Anoma.Transaction.Action as Action open;
 import Anoma.Delta as Delta open using {Delta};
 import Anoma.MathProperty open;
 import Anoma.Proving.Types open;
 
+--- A record describing a transaction object, the entity constituting a state transition in Anoma.
 positive
 type Transaction :=
   mkTransaction {
@@ -16,13 +20,15 @@ type Transaction :=
     deltaProof : ProofRecord
   };
 
+--- The ;Transaction; object constructor signature.
 Constructor : Type :=
   (roots : Set CommitmentTree.Root)
     -> (actions : Set Action)
     -> (delta : Delta)
     -> (deltaProof : ProofRecord)
     -> Transaction;
 
+--- Compses two ;Transaction; objects.
 compose (tx1 tx2 : Transaction) : Transaction :=
   mkTransaction@{
     roots :=
@@ -47,3 +53,9 @@ compose (tx1 tx2 : Transaction) : Transaction :=
         p2 := Transaction.deltaProof tx2
       }
   };
+
+commitmentSet (transaction : Transaction) : Set Resource.Commitment :=
+  for (acc := Set.empty) (a in Transaction.actions transaction) {union acc (Action.commitments a)};
+
+nullfierSet (transaction : Transaction) : Set Resource.Nullifier :=
+  for (acc := Set.empty) (a in Transaction.actions transaction) {union acc (Action.nullifiers a)};