refactor: restructuring

Anoma/ProvingSystem/ComplianceProof.juvix

@@ -0,0 +1,34 @@
+--- An instantiation of a Proving System for Delta proofs.
+module Anoma.ProvingSystem.ComplianceProof;
+
+import Stdlib.Prelude open using {Bool};
+import Anoma.ProvingSystem.Types as Parametrized;
+
+axiom Proof : Type;
+
+axiom VerifyingKey : Type;
+
+axiom ProvingKey : Type;
+
+--- TODO Can this types be replaced with definitions from `Anoma.State.CommitmentTree` and `Anoma.State.NullifierSet`?
+axiom Instance : Type;
+
+--- TODO Can this types be replaced with definitions from `Anoma.State.CommitmentTree` and `Anoma.State.NullifierSet`?
+axiom Witness : Type;
+
+ProofRecord : Type := Parametrized.ProofRecord Proof VerifyingKey Witness;
+
+axiom prove : (provingKey : ProvingKey)
+  -> (publicInputs : Instance)
+  -> (privateInputs : Witness)
+  -> Proof;
+
+axiom verify : (proofRecord : ProofRecord) -> Bool;
+
+instance
+Compliance-ProvingSystem
+  : Parametrized.ProvingSystem Proof VerifyingKey ProvingKey Witness Instance :=
+  Parametrized.mkProvingSystem@{
+    prove;
+    verify
+  };

Anoma/ProvingSystem/DeltaProof.juvix

@@ -0,0 +1,36 @@
+--- An instantiation of a Proving System for Delta proofs.
+module Anoma.ProvingSystem.DeltaProof;
+
+import Stdlib.Prelude open using {Bool};
+import Anoma.ProvingSystem.Types as Parametrized;
+
+axiom Proof : Type;
+
+axiom VerifyingKey : Type;
+
+axiom ProvingKey : Type;
+
+--- TODO Can this types be replaced with definitions from `Anoma.Transaction.Delta`?
+axiom Instance : Type;
+
+--- TODO Can this types be replaced with definitions from `Anoma.Transaction.Delta`?
+axiom Witness : Type;
+
+ProofRecord : Type := Parametrized.ProofRecord Proof VerifyingKey Witness;
+
+axiom prove : (provingKey : ProvingKey)
+  -> (publicInputs : Instance)
+  -> (privateInputs : Witness)
+  -> Proof;
+
+axiom verify : (proofRecord : ProofRecord) -> Bool;
+
+instance
+Delta-ProvingSystem : Parametrized.ProvingSystem Proof VerifyingKey ProvingKey Witness Instance :=
+  Parametrized.mkProvingSystem@{
+    prove;
+    verify
+  };
+
+--- Aggregates two  delta ;ProofRecord;s.
+axiom aggregate : (p1 p2 : ProofRecord) -> ProofRecord;

Anoma/ProvingSystem/ResourceLogicProof.juvix

@@ -0,0 +1,36 @@
+module Anoma.ProvingSystem.ResourceLogicProof;
+
+import Stdlib.Prelude open using {Bool};
+import Anoma.ProvingSystem.Types as Parametrized;
+import Anoma.Resource.Logic as ResourceLogic;
+
+--- A fixed-size data type encoding the resource logic proof.
+axiom Proof : Type;
+
+--- A fixed-size data type encoding the verifying key of the resource logic proof.
+axiom VerifyingKey : Type;
+
+--- A fixed-size data type encoding the proving key of the resource logic proof.
+axiom ProvingKey : Type;
+
+ProofRecord : Type := Parametrized.ProofRecord Proof VerifyingKey ResourceLogic.Witness;
+
+axiom prove : (provingKey : ProvingKey)
+  -> (publicInputs : ResourceLogic.Instance)
+  -> (privateInputs : ResourceLogic.Witness)
+  -> Proof;
+
+axiom verify : (proofRecord : ProofRecord) -> Bool;
+
+instance
+ResourceLogic-ProvingSystem
+  : Parametrized.ProvingSystem
+    Proof
+    VerifyingKey
+    ProvingKey
+    ResourceLogic.Witness
+    ResourceLogic.Instance :=
+  Parametrized.mkProvingSystem@{
+    prove;
+    verify
+  };

Anoma/Proving/System.juvix → Anoma/ProvingSystem/Types.juvix

@@ -1,8 +1,21 @@
-module Anoma.Proving.System;
+module Anoma.ProvingSystem.Types;
 
-import Stdlib.Prelude open using {Bool};
-import Anoma.Proving.Types open using {ProofRecord};
-import Anoma.Resource.Index as Resource open using {Instance; Witness};
+import Stdlib.Prelude open using {Pair; Bool};
+
+--- 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.
+ProofRecord (Proof VerifyingKey Witness : Type) : Type := Pair VerifyingKey (Pair Proof Witness);
+
+--- A set of ProofRecords.
+---
+--- Each ProofRecord in the set may be parameterized with different types for
+--- Proof, VerifyingKey and Witness, allowing for heterogeneous ProofRecords
+--- within the set. It's not currently possible to represent such a set in Juvix.
+axiom ProofRecordSet : Type;
+
+module ProofRecordSet;
+  axiom empty : ProofRecordSet;
+end;
 
 --- The interface of the resource machine proving system.
 --- Proof : A fixed-size data type encoding a proof.
@@ -23,35 +36,3 @@ type ProvingSystem Proof VerifyingKey ProvingKey Witness Instance :=
     --- Verfies a ;ProofRecord;.
     verify : (proofRecord : ProofRecord Proof VerifyingKey Witness) -> Bool
   };
-
---- An instantiation of a Proving System for Delta proofs.
-module Delta;
-  import Anoma.Proving.Types as T;
-
-  axiom Proof : Type;
-
-  axiom VerifyingKey : Type;
-
-  axiom ProvingKey : Type;
-
-  axiom Witness : Type;
-
-  axiom Instance : Type;
-
-  ProofRecord : Type := T.ProofRecord Proof VerifyingKey Witness;
-
-  axiom prove : (provingKey : ProvingKey)
-    -> (publicInputs : Instance)
-    -> (privateInputs : Witness)
-    -> Proof;
-
-  axiom verify : (proofRecord : ProofRecord) -> Bool;
-
-  instance
-  DeltaProvingSystem : ProvingSystem Proof VerifyingKey ProvingKey Witness Instance :=
-    mkProvingSystem@{
-      prove;
-      verify
-    };
-
-end;

Anoma/Transaction/Action.juvix

@@ -4,7 +4,7 @@ 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 open using {Resource};
-import Anoma.Proving.Types open using {ProofRecord; ProofRecordSet; module ProofRecordSet};
+import Anoma.ProvingSystem.Types open using {ProofRecord; ProofRecordSet; module ProofRecordSet};
 
 module AppDataInternal;
   --- A fixed-size data type encoding the lookup key of application data being part of an action.

Anoma/Transaction/Types.juvix

@@ -8,8 +8,8 @@ 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;
-import Anoma.Proving.System open;
+import Anoma.ProvingSystem.Types open;
+import Anoma.ProvingSystem.DeltaProof as DeltaProof;
 
 --- A record describing a transaction object, the entity constituting a state transition in Anoma.
 positive
@@ -18,15 +18,15 @@ type Transaction :=
     roots : Set CommitmentTree.Root;
     actions : Set Action;
     delta : Delta;
-    deltaProof : Delta.ProofRecord;
+    deltaProof : DeltaProof.ProofRecord
   };
 
 --- The ;Transaction; object constructor signature.
 Constructor : Type :=
   (roots : Set CommitmentTree.Root)
     -> (actions : Set Action)
     -> (delta : Delta)
-    -> (deltaProof : Delta.ProofRecord)
+    -> (deltaProof : DeltaProof.ProofRecord)
     -> Transaction;
 
 --- Compses two ;Transaction; objects.
@@ -50,9 +50,9 @@ compose (tx1 tx2 : Transaction) : Transaction :=
     -- };
     deltaProof :=
       DeltaProof.aggregate@{
-        Witness := Delta.Witness;
-        Proof := Delta.Proof;
-        VerifyingKey := Delta.VerifyingKey;
+        Witness := DeltaProof.Witness;
+        Proof := DeltaProof.Proof;
+        VerifyingKey := DeltaProof.VerifyingKey;
         p1 := Transaction.deltaProof tx1;
         p2 := Transaction.deltaProof tx2
       }