refactor: make CustomInputs a map

Anoma/Generic/ProofRecord.juvix

@@ -29,7 +29,6 @@ module ProofRecordInternal;
           | LogicProofRecord _, DeltaProofRecord _ := LessThan
           | DeltaProofRecord _, _ := GreaterThan;
     };
-
 end;
 
 --- NOTE: At verification time, a proof record set must contain exactly one ;Delta.ProofRecord;.

Anoma/Logic/Types.juvix

@@ -8,6 +8,7 @@ import Anoma.Resource.Object open using {Resource};
 import Anoma.Resource.Types open using {Commitment; Nullifier};
 import Anoma.Resource.Tag open using {Tag};
 import Anoma.Transaction.AppData open using {AppData};
+import Anoma.Transaction.CustomInputs open using {CustomInputs};
 import Anoma.Utils open;
 
 type Proof := mkProof@{unProof : MISSING_DEFINITION};
@@ -25,10 +26,6 @@ type Instance :=
     appData : AppData;
   };
 
---- Custom inputs of the resource logic function proof being defined on the application level.
---- NOTE: For the private testnet, this can be of type ;AppData;.
-type CustomInputs := mkCustomInputs@{unCustomInputs : MISSING_DEFINITION};
-
 --- The private inputs (Witness) of the resource logic function proof.
 type Witness :=
   mkWitness@{
@@ -47,20 +44,6 @@ type ProofRecord :=
     instance : Instance;
   };
 
-module CustomInputsInternal;
-  --- Compares two ;CustomInputs; objects.
-  compare (lhs rhs : CustomInputs) : Ordering :=
-    Ord.cmp (CustomInputs.unCustomInputs lhs) (CustomInputs.unCustomInputs rhs);
-
-  --- Implements the ;Ord; trait for ;Proof;.
-  instance
-  CustomInputs-Ord : Ord CustomInputs := mkOrd compare;
-
-  --- Implements the ;Eq; trait for ;CustomInputs;.
-  instance
-  CustomInputs-Eq : Eq CustomInputs := fromOrdToEq;
-end;
-
 module ProofInternal;
   --- Compares two ;Proof; objects.
   compare (lhs rhs : Proof) : Ordering :=

Anoma/Transaction.juvix

@@ -2,4 +2,5 @@ module Anoma.Transaction;
 
 import Anoma.Transaction.Action open public;
 import Anoma.Transaction.AppData open public;
+import Anoma.Transaction.CustomInputs open public;
 import Anoma.Transaction.Object open public;

Anoma/Transaction/AppData.juvix

@@ -9,10 +9,10 @@ import Anoma.Utils open;
 --- A data type encoding the deletion criterion.
 -- TODO Add enumeration from the specs.
 type DeletionCriterion :=
-  | DeleteAfterBlock MISSING_DEFINITION
-  | DeleteAfterTimestamp MISSING_DEFINITION
-  | DeleteAfterSignatureOverData MISSING_DEFINITION
-  | DeleteAfterPredicates MISSING_DEFINITION
+  | AfterBlock MISSING_DEFINITION
+  | AfterTimestamp MISSING_DEFINITION
+  | AfterSignatureOverData MISSING_DEFINITION
+  | AfterPredicates MISSING_DEFINITION
   | StoreForever MISSING_DEFINITION;
 
 --- A data type encoding the lookup key of application.
@@ -25,6 +25,18 @@ type AppDataValue :=
 --- A type describing an app data map.
 AppData : Type := Map AppDataKey AppDataValue;
 
+module DeletionCriterionInternal;
+  axiom compare : DeletionCriterion -> DeletionCriterion -> Ordering;
+
+  --- Implements the ;Ord; trait for ;DeletionCriterion;.
+  instance
+  DeletionCriterion-Ord : Ord DeletionCriterion := mkOrd compare;
+
+  --- Implements the ;Eq; trait for ;DeletionCriterion;.
+  instance
+  DeletionCriterion-Eq : Eq DeletionCriterion := fromOrdToEq;
+end;
+
 --- A module implementing traits for ;AppDataKey;.
 module AppDataKeyInternal;
   --- Compares two ;AppDataKey;s.
@@ -39,3 +51,18 @@ module AppDataKeyInternal;
   instance
   AppDataKey-Eq : Eq AppDataKey := fromOrdToEq;
 end;
+
+--- A module implementing traits for ;AppDataValue;.
+module AppDataValueInternal;
+  --- Compares two ;AppDataValue;s.
+  compare (lhs rhs : AppDataValue) : Ordering :=
+    Ord.cmp (AppDataValue.unAppDataValue lhs) (AppDataValue.unAppDataValue rhs);
+
+  --- Implements the ;Ord; trait for ;AppDataValue;.
+  instance
+  AppDataValue-Ord : Ord AppDataValue := mkOrd compare;
+
+  --- Implements the ;Eq; trait for ;AppDataValue;.
+  instance
+  AppDataValue-Eq : Eq AppDataValue := fromOrdToEq;
+end;

Anoma/Transaction/CustomInputs.juvix

@@ -0,0 +1,50 @@
+module Anoma.Transaction.CustomInputs;
+
+import Stdlib.Prelude open;
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+import Stdlib.Data.Map as Map open using {Map};
+import Anoma.Builtin.ByteArray open using {ByteArray};
+import Anoma.Utils open;
+
+--- A data type encoding the lookup key of application.
+type CustomInputsKey := mkCustomInputsKey@{unCustomInputsKey : ByteArray};
+
+--- A data type encoding the lookup value of application data.
+type CustomInputsValue := mkCustomInputsValue@{unCustomInputsValue : ByteArray};
+
+--- A type describing an app data map.
+CustomInputs : Type := Map CustomInputsKey CustomInputsValue;
+
+--- A module implementing traits for ;CustomInputsKey;.
+module CustomInputsKeyInternal;
+  --- Compares two ;CustomInputsKey;s.
+  compare (lhs rhs : CustomInputsKey) : Ordering :=
+    Ord.cmp
+      (CustomInputsKey.unCustomInputsKey lhs)
+      (CustomInputsKey.unCustomInputsKey rhs);
+
+  --- Implements the ;Ord; trait for ;CustomInputsKey;.
+  instance
+  CustomInputsKey-Ord : Ord CustomInputsKey := mkOrd compare;
+
+  --- Implements the ;Eq; trait for ;CustomInputsKey;.
+  instance
+  CustomInputsKey-Eq : Eq CustomInputsKey := fromOrdToEq;
+end;
+
+--- A module implementing traits for ;CustomInputsValue;.
+module CustomInputsValueInternal;
+  --- Compares two ;CustomInputsValue;s.
+  compare (lhs rhs : CustomInputsValue) : Ordering :=
+    Ord.cmp
+      (CustomInputsValue.unCustomInputsValue lhs)
+      (CustomInputsValue.unCustomInputsValue rhs);
+
+  --- Implements the ;Ord; trait for ;CustomInputsValue;.
+  instance
+  CustomInputsValue-Ord : Ord CustomInputsValue := mkOrd compare;
+
+  --- Implements the ;Eq; trait for ;CustomInputsValue;.
+  instance
+  CustomInputsValue-Eq : Eq CustomInputsValue := fromOrdToEq;
+end;