refactor: use failwith instead of axiom

Anoma/Delta.juvix

@@ -1,15 +1,17 @@
 module Anoma.Delta;
 
 import Anoma.Math as Math open;
+import Anoma.Utils open using {MISSING_DEFINITION; MISSING_ANOMA_BUILTIN; ANOMA_BACKEND_IMPLEMENTATION};
 
---- A fixed-size data type encoding the resource delta.
-axiom Delta : Type;
-
---- Adds two ;Delta; values.
-axiom addDelta : (d1 d2 : Delta) -> Delta;
+--- A fixed-size data type encoding the additively homomorphic and kind distinct ;Delta;.
+--- NOTE: For the private testnet, the requirement can be relaxed by allowing ;Delta; to be dynamically-sized.
+type Delta := mkDelta {unDelta : MISSING_DEFINITION};
 
 --- The ;Delta; value zero.
-axiom zero : Delta;
+zero : Delta := MISSING_ANOMA_BUILTIN;
+
+--- Adds two ;Delta; values.
+addDelta (d1 d2 : Delta) : Delta := ANOMA_BACKEND_IMPLEMENTATION;
 
 --- Implements the ;Math.AdditivelyHomomorphic; trait for ;Delta;.
 instance

Anoma/Identity/External.juvix

@@ -2,13 +2,14 @@ module Anoma.Identity.External;
 
 import Stdlib.Prelude open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+import Anoma.Utils open using {MISSING_DEFINITION; MISSING_ANOMA_BUILTIN};
 
 --- A fixed-size data type describing an external identity.
-axiom ExternalIdentity : Type;
+type ExternalIdentity := mkExternalIdentity {unExternalIdentity : MISSING_DEFINITION};
 
 module ExternalIdentityInternal;
   --- Compares two ;ExternalIdentity; objects.
-  axiom compare : (lhs rhs : ExternalIdentity) -> Ordering;
+  compare (lhs rhs : ExternalIdentity) : Ordering := MISSING_ANOMA_BUILTIN;
 
   --- Implements the ;Ord; trait for ;ExternalIdentity;.
   instance

Anoma/Identity/Internal.juvix

@@ -2,13 +2,14 @@ module Anoma.Identity.Internal;
 
 import Stdlib.Prelude open;
 import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+import Anoma.Utils open using {MISSING_DEFINITION; MISSING_ANOMA_BUILTIN};
 
 --- A fixed-size data type describing an internal identity.
-axiom InternalIdentity : Type;
+type InternalIdentity := mkInternalIdentity {unInternalIdentity : MISSING_DEFINITION};
 
 module InternalIdentityInternal;
   --- Compares two ;InternalIdentity; objects.
-  axiom compare : (lhs rhs : InternalIdentity) -> Ordering;
+  compare (lhs rhs : InternalIdentity) : Ordering := MISSING_ANOMA_BUILTIN;
 
   --- Implements the ;Ord; trait for ;InternalIdentity;.
   instance

Anoma/Identity/Signing/Types.juvix

@@ -3,49 +3,61 @@ module Anoma.Identity.Signing.Types;
 import Stdlib.Prelude open;
 import Anoma.Identity.Internal open;
 import Anoma.Identity.External open;
+import Anoma.Utils open using {MISSING_DEFINITION; MISSING_ANOMA_BUILTIN};
 
-axiom Signature : Type;
-
-axiom verify : {Message : Type}
-  -- | The signature to verify.
-  -> Signature
-  -- | The message to verify against.
-  -> Message
-  -- | The signer external identity to verify against.
-  -> ExternalIdentity
-  -- | The verification result.
-  -> Bool;
-
-axiom sign : {Message : Type}
-  -- | The message to sign.
-  -> Message
-  -- | The signing internal identity .
-  -> InternalIdentity
-  -- | The resulting signature
-  -> Signature;
-
---- TODO Consider deleting the definitions below..
-module NonDetached;
-  axiom SignedMessage : Type;
-
-  verify (signedMessage : SignedMessage) (externalIdentity : ExternalIdentity) : Bool :=
-    case verifyWithMessage {Unit} signedMessage externalIdentity of
-      | just _ := true
-      | nothing := false;
+type Signature := mkSignature {unSignature : MISSING_DEFINITION};
 
-  axiom verifyWithMessage : {Message : Type}
-    -- | The signed message to verify.
-    -> SignedMessage
+{-# inline: true #-}
+verify
+  : {Message : Type}
+    -- | The signature to verify.
+    -> Signature
+    -- | The message to verify against.
+    -> Message
     -- | The signer external identity to verify against.
     -> ExternalIdentity
-    -- | The original message.
-    -> Maybe Message;
+    -- | The verification result.
+    -> Bool
+  | (mkSignature signature) message externalIdentity := MISSING_ANOMA_BUILTIN;
 
-  axiom sign : {Message : Type}
+{-# inline: true #-}
+sign
+  : {Message : Type}
     -- | The message to sign.
     -> Message
     -- | The signing internal identity.
     -> InternalIdentity
-    -- | The resulting signed message.
-    -> SignedMessage;
+    -- | The resulting signature
+    -> Signature
+  | message internalIdentity := MISSING_ANOMA_BUILTIN;
+
+--- TODO Consider deleting the definitions below.
+module NonDetached;
+  type SignedMessage := mkSignedMessage {unSignedMessage : MISSING_DEFINITION};
+
+  {-# inline: true #-}
+  verify (signedMessage : SignedMessage) (externalIdentity : ExternalIdentity) : Bool :=
+    MISSING_ANOMA_BUILTIN;
+
+  {-# inline: true #-}
+  verifyWithMessage
+    : {Message : Type}
+      -- | The signed message to verify.
+      -> SignedMessage
+      -- | The signer external identity to verify against.
+      -> ExternalIdentity
+      -- | The original message.
+      -> Maybe Message
+    | (mkSignedMessage signedMessage) externalIdentity := MISSING_ANOMA_BUILTIN;
+
+  {-# inline: true #-}
+  sign
+    : {Message : Type}
+      -- | The message to sign.
+      -> Message
+      -- | The signing internal identity.
+      -> InternalIdentity
+      -- | The resulting signed message.
+      -> SignedMessage
+    | message internalIdentity := MISSING_ANOMA_BUILTIN;
 end;

Anoma/Proving/ComplianceProof.juvix

@@ -4,16 +4,18 @@ module Anoma.Proving.ComplianceProof;
 import Stdlib.Prelude open;
 import Anoma.Proving.Types as Parametrized open using {module Compliance};
 import Anoma.Proving.System as Parametrized open using {ProvingSystem};
+import Anoma.Utils open using {MISSING_ANOMA_BUILTIN};
 
 ProofRecord : Type :=
   Parametrized.ProofRecord Compliance.Proof Compliance.VerifyingKey Compliance.Witness;
 
-axiom prove : (provingKey : Compliance.ProvingKey)
-  -> (publicInputs : Compliance.Instance)
-  -> (privateInputs : Compliance.Witness)
-  -> Compliance.Proof;
+prove
+  (provingKey : Compliance.ProvingKey)
+  (publicInputs : Compliance.Instance)
+  (privateInputs : Compliance.Witness)
+  : Compliance.Proof := MISSING_ANOMA_BUILTIN;
 
-axiom verify : (proofRecord : ProofRecord) -> Bool;
+verify (proofRecord : ProofRecord) : Bool := MISSING_ANOMA_BUILTIN;
 
 instance
 Compliance-ProvingSystem

Anoma/Proving/DeltaProof.juvix

@@ -4,15 +4,17 @@ module Anoma.Proving.DeltaProof;
 import Stdlib.Prelude open;
 import Anoma.Proving.Types as Parametrized open using {module Delta};
 import Anoma.Proving.System as Parametrized open using {ProvingSystem};
+import Anoma.Utils open using {MISSING_ANOMA_BUILTIN; ANOMA_BACKEND_IMPLEMENTATION};
 
 ProofRecord : Type := Parametrized.ProofRecord Delta.Proof Delta.VerifyingKey Delta.Witness;
 
-axiom prove : (provingKey : Delta.ProvingKey)
-  -> (publicInputs : Delta.Instance)
-  -> (privateInputs : Delta.Witness)
-  -> Delta.Proof;
+prove
+  (provingKey : Delta.ProvingKey)
+  (publicInputs : Delta.Instance)
+  (privateInputs : Delta.Witness)
+  : Delta.Proof := MISSING_ANOMA_BUILTIN;
 
-axiom verify : (proofRecord : ProofRecord) -> Bool;
+verify (proofRecord : ProofRecord) : Bool := MISSING_ANOMA_BUILTIN;
 
 instance
 Delta-ProvingSystem
@@ -28,4 +30,4 @@ Delta-ProvingSystem
   };
 
 --- Aggregates two  delta ;ProofRecord;s.
-axiom aggregate : (p1 p2 : ProofRecord) -> ProofRecord;
+aggregate (p1 p2 : ProofRecord) : ProofRecord := ANOMA_BACKEND_IMPLEMENTATION;

Anoma/Proving/ProofRecordSet.juvix

@@ -7,6 +7,7 @@ import Anoma.Proving.ComplianceProof as ComplianceProof open;
 import Anoma.Proving.ResourceLogicProof as ResourceLogicProof open;
 import Anoma.Proving.DeltaProof as DeltaProof open;
 import Anoma.Proving.Types open;
+import Anoma.Utils open using {MISSING_ANOMA_BUILTIN};
 
 --- A proof record set.
 type ProofRecordSet :=
@@ -24,18 +25,9 @@ empty : ProofRecordSet :=
     deltaProof := nothing
   };
 
---- Verifies a ;ProofRecordSet; ;nothing;.
+--- Verifies a ;ProofRecordSet;.
 --- NOTE: At verification time, a proof record set must contain exactly one ;DeltaProof.ProofRecord;.
-verify (proofRecords : ProofRecordSet) : Bool :=
-  case ProofRecordSet.deltaProof proofRecords of {
-    | just deltaProof := DeltaProof.verify deltaProof
-    -- At verification time, this is must not be ;nothing;.
-    | nothing := false
-  }
-    && all (p in Set.toList (ProofRecordSet.complianceProofs proofRecords))
-         {ComplianceProof.verify p}
-    && all (p in Set.toList (ProofRecordSet.resourceLogicProofs proofRecords))
-         {ResourceLogicProof.verify p};
+verifyProofRecords (proofRecords : ProofRecordSet) : Bool := MISSING_ANOMA_BUILTIN;
 
 module ProofRecordSetInternal;
   --- Compares two ;ProofRecordSet; objects.

Anoma/Proving/ResourceLogicProof.juvix

@@ -4,16 +4,18 @@ module Anoma.Proving.ResourceLogicProof;
 import Stdlib.Prelude open;
 import Anoma.Proving.Types as Parametrized open using {module ResourceLogic};
 import Anoma.Proving.System as Parametrized open using {ProvingSystem};
+import Anoma.Utils open using {MISSING_ANOMA_BUILTIN};
 
 ProofRecord : Type :=
   Parametrized.ProofRecord ResourceLogic.Proof ResourceLogic.VerifyingKey ResourceLogic.Witness;
 
-axiom prove : (provingKey : ResourceLogic.ProvingKey)
-  -> (publicInputs : ResourceLogic.Instance)
-  -> (privateInputs : ResourceLogic.Witness)
-  -> ResourceLogic.Proof;
+prove
+  (provingKey : ResourceLogic.ProvingKey)
+  (publicInputs : ResourceLogic.Instance)
+  (privateInputs : ResourceLogic.Witness)
+  : ResourceLogic.Proof := MISSING_ANOMA_BUILTIN;
 
-axiom verify : (proofRecord : ProofRecord) -> Bool;
+verify (proofRecord : ProofRecord) : Bool := MISSING_ANOMA_BUILTIN;
 
 instance
 ResourceLogic-ProvingSystem

Anoma/Proving/System.juvix

@@ -1,7 +1,7 @@
 module Anoma.Proving.System;
 
 import Stdlib.Prelude open;
-import Anoma.Proving.Types open;
+import Anoma.Proving.Types open using {ProofRecord};
 
 --- The interface of the resource machine proving system.
 --- Proof: A fixed-size data type encoding a proof.