docs: added judoc comments

Anoma/Proving/System.juvix

@@ -4,9 +4,17 @@ import Stdlib.Prelude open using {Bool};
 import Anoma.Proving.Types open using {ProvingKey; Proof; ProofRecord};
 import Anoma.Resource.Index as Resource open using {Instance; Witness};
 
+--- The interface of the resource machine proving system.
 trait
 type ProvingSystem :=
   mkProvingSystem {
-    prove : ProvingKey -> Resource.Instance -> Resource.Witness -> Proof;
-    verify : ProofRecord -> Bool
+    --- Creates a ;Proof; given a ;ProvingKey;, public inputs (;Resource.Instance;), and
+    --- private inputs (;Resource.Witness;).
+    prove : (provingKey : ProvingKey)
+      -> (publicInputs : Resource.Instance)
+      -> (privateInputs : Resource.Witness)
+      -> Proof;
+
+    --- Verfies a ;ProofRecord;.
+    verify : (proofRecord : ProofRecord) -> Bool
   };

Anoma/Resource/Computable/Commitment.juvix

@@ -2,6 +2,7 @@ module Anoma.Resource.Computable.Commitment;
 
 import Stdlib.Prelude open using {Eq; Ord; Ordering; mkOrd};
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+import Data.Set as Set open using {Set};
 import Anoma.Resource.Types open using {Resource};
 
 axiom Commitment : Type;
@@ -10,8 +11,11 @@ axiom Commitment : Type;
 axiom commitment : (resource : Resource) -> Commitment;
 
 module CommitmentInternal;
-  axiom compare : Commitment -> Commitment -> Ordering;
+  --- Compares two ;Commitment; and returns their ;Ordering;.
+  axiom compare : (lhs rhs : Commitment) -> Ordering;
 
+  --- Implements the ;Ord; trait for ;Commitment;.
+  --- NOTE: This is required for using them in ;Set;.
   instance
   Commitment-Ord : Ord Commitment :=
     mkOrd@{

Anoma/Resource/Computable/Delta.juvix

@@ -5,9 +5,13 @@ import Anoma.Resource.Types as Resource open using {Resource; Quantity};
 import Anoma.Resource.Computable.Kind as Computable open;
 
 module ResourceDeltaInternal;
+  --- The delta function as defined in the RM specs.
+  --- NOTE: This definition does not specify that the ;Kind; and ;Quantity; arguments
+  --- must come from the same ;Resource; although this must be the case.
   axiom delta : (kind : Kind) -> (quantity : Quantity) -> Delta;
 end;
 
+--- Computes the ;Delta; value of a given ;Resource;.
 delta (resource : Resource) : Delta :=
   ResourceDeltaInternal.delta@{
     kind := Computable.kind resource;

Anoma/Resource/Computable/Kind.juvix

@@ -7,9 +7,13 @@ import Anoma.Resource.Label open using {LabelRef};
 axiom Kind : Type;
 
 module KindInternal;
+  --- The kind function as defined in the RM specs.
+  --- NOTE: This definition does not specify that the ;LogicRef; and ;LabelRef; arguments
+  --- must come from the same ;Resource; although this must be the case.
   axiom kind : (logicRef : LogicRef) -> (labelRef : LabelRef) -> Kind;
 end;
 
+--- Computes the ;Kind; value of a given ;Resource;.
 kind (resource : Resource) : Kind :=
   KindInternal.kind@{
     logicRef := Resource.logicRef resource;

Anoma/Resource/Computable/Nullifier.juvix

@@ -2,17 +2,23 @@ module Anoma.Resource.Computable.Nullifier;
 
 import Stdlib.Prelude open using {Eq; Ord; Ordering; mkOrd};
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+import Data.Set as Set open using {Set};
 import Anoma.Resource.Types open using {Resource};
 
 axiom Nullifier : Type;
 
 axiom NullifierKey : Type;
 
+--- Computes the ;Nullifier; of a ;Resource; given a ;NullifierKey;.
+--- TODO: Should this function verify that the `Resource.nullifierKeyCommitment` can be derived from the `nullifierKey`?
 axiom nullifier : (resource : Resource) -> (nullifierKey : NullifierKey) -> Nullifier;
 
 module NullfierInternal;
-  axiom compare : Nullifier -> Nullifier -> Ordering;
+  --- Compares two ;Nullifier; and returns their ;Ordering;.
+  axiom compare : (lhs rhs : Nullifier) -> Ordering;
 
+  --- Implements the ;Ord; trait for ;Nullifier;.
+  --- NOTE: This is required for using them in ;Set;.
   instance
   Nullifier-Ord : Ord Nullifier :=
     mkOrd@{

Anoma/State/CommitmentTree.juvix

@@ -2,25 +2,37 @@ module Anoma.State.CommitmentTree;
 
 import Stdlib.Prelude open using {Maybe; Bool; Eq; Ord; Ordering; mkOrd};
 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};
 
 axiom Root : Type;
 
 axiom Path : Type;
 
+--- The interface of the resource machine commitment tree.
 positive
 trait
 type CommitmentTree :=
   mkCommitmentTree {
+    --- Adds a ;Resource.Commitment; to the ;CommitmentTree; and returns the ;Path;.
     add : CommitmentTree -> Resource.Commitment -> Path;
+
+    --- Returns the ;Path; of a ;Resource.Commitment; in the ;CommitmentTree;, or nothing if it does not exist.
     path : CommitmentTree -> Resource.Commitment -> Maybe Path;
+
+    --- Verifies a ;Path; of a ;Resource.Commitment; in the ;CommitmentTree;.
     verify : Resource.Commitment -> Path -> Root -> Bool;
+
+    --- Returns the ;Root; of the ;CommitmentTree;.
     root : CommitmentTree -> Root
   };
 
 module RootInternal;
-  axiom compare : Root -> Root -> Ordering;
+  --- Compares two ;Root;s and returns their ;Ordering;.
+  axiom compare : (lhs rhs : Root) -> Ordering;
 
+  --- Implements the ;Ord; trait for ;Root;.
+  --- NOTE: This is required for using them in ;Set;.
   instance
   Root-Ord : Ord Root :=
     mkOrd@{
@@ -31,6 +43,5 @@ module RootInternal;
   Root-Eq : Eq Root := fromOrdToEq;
 end;
 
--- TODO
--- How to deal with timestamps in the commitment tree?
+-- TODO: Do we need to express timestamps in the commitment tree?
 -- https://specs.anoma.net/v2/system_architecture/state/resource_machine/rm_def/storage.html

Anoma/State/Machine.juvix

@@ -3,10 +3,21 @@ module Anoma.State.Machine;
 import Stdlib.Prelude open using {Bool};
 import Anoma.Transaction.Index as Transaction open using {Transaction};
 
+--- The interface of the resource machine.
 trait
 type Machine :=
   mkMachine {
+    --- Creates a ;Transaction; with the the ;Transaction.Constructor;.
+    --- TODO Clarify why this is needed.
     create : Transaction.Constructor;
-    compose : Transaction -> Transaction -> Transaction;
-    verify : Transaction -> Bool
+
+    --- Composes two ;Transaction;s with the transa
+    compose : (tx1 tx2 : Transaction) -> Transaction;
+
+    --- Verifies a ;Transaction; by checking that the
+    --- - resource logic proofs
+    --- - compliance proofs
+    --- - delta proof (a.k.a., balance proof)
+    --- is valid.
+    verify : (tx : Transaction) -> Bool
   };

Anoma/State/NullifierSet.juvix

@@ -3,6 +3,7 @@ module Anoma.State.NullifierSet;
 import Stdlib.Prelude open using {Bool};
 import Anoma.Resource.Computable.Nullifier as Resource open using {Nullifier};
 
+--- The interface of the resource machine nullifier set.
 trait
 type NullifierSet :=
   mkAccumulator {

Anoma/Transaction/Types.juvix

@@ -16,7 +16,12 @@ type Transaction :=
     deltaProof : ProofRecord
   };
 
-Constructor : Type := Set CommitmentTree.Root -> Set Action -> Delta -> ProofRecord -> Transaction;
+Constructor : Type :=
+  (roots : Set CommitmentTree.Root)
+    -> (actions : Set Action)
+    -> (delta : Delta)
+    -> (deltaProof : ProofRecord)
+    -> Transaction;
 
 compose (tx1 tx2 : Transaction) : Transaction :=
   mkTransaction@{