Support Anoma stdlib APIs sign and verify (#2788)

This PR adds support for the Anoma stdlib `sign` and `verify` APIs.

```
builtin anoma-sign
axiom anomaSign : {A : Type}
  -- message to sign
  -> A
  -- secret key
  -> Nat
  -- signed message
  -> Nat;

builtin anoma-verify
axiom anomaVerify : {A : Type}
  -- signed message to verify 
  -> Nat 
  -- public key
  -> Nat 
  -- message with signature removed
  -> A;
```

These correspond to the
[`sign`](https://hexdocs.pm/enacl/enacl.html#sign-2) and
[`sign_open`](https://hexdocs.pm/enacl/enacl.html#sign_open-2) APIs from
libsodium respectively.

If signature verification fails in `anomaVerify`, the Anoma program
exits. We copy this behaviour in the evaluator by throwing an error in
this case.

## Notes

The Haskell Ed25519 library does not support `sign_open`. Its
verification function returns Bool, i.e it checks that the signature is
valid. The signed message is simply the concatenation of the signature
(64 bytes) and the original message so I added a function to remove the
signature from a signed message.

src/Juvix/Compiler/Builtins/Anoma.hs

@@ -57,3 +57,29 @@ registerAnomaVerifyDetached f = do
     ((ftype ==% (u <>--> nat --> decodeT --> nat --> bool_)) freeVars)
     (error "anomaVerifyDetached must be of type {A : Type} -> Nat -> A -> Nat -> Bool")
   registerBuiltin BuiltinAnomaVerifyDetached (f ^. axiomName)
+
+registerAnomaSign :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
+registerAnomaSign f = do
+  let ftype = f ^. axiomType
+      u = ExpressionUniverse smallUniverseNoLoc
+      l = getLoc f
+  dataT <- freshVar l "dataT"
+  nat <- getBuiltinName (getLoc f) BuiltinNat
+  let freeVars = HashSet.fromList [dataT]
+  unless
+    ((ftype ==% (u <>--> dataT --> nat --> nat)) freeVars)
+    (error "anomaSign must be of type {A : Type} -> A -> Nat -> Nat")
+  registerBuiltin BuiltinAnomaSign (f ^. axiomName)
+
+registerAnomaVerify :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
+registerAnomaVerify f = do
+  let ftype = f ^. axiomType
+      u = ExpressionUniverse smallUniverseNoLoc
+      l = getLoc f
+  dataT <- freshVar l "dataT"
+  nat <- getBuiltinName (getLoc f) BuiltinNat
+  let freeVars = HashSet.fromList [dataT]
+  unless
+    ((ftype ==% (u <>--> nat --> nat --> dataT)) freeVars)
+    (error "anomaVerify must be of type {A : Type} -> Nat -> Nat -> A")
+  registerBuiltin BuiltinAnomaVerify (f ^. axiomName)

src/Juvix/Compiler/Concrete/Data/Builtins.hs

@@ -191,6 +191,8 @@ data BuiltinAxiom
   | BuiltinAnomaEncode
   | BuiltinAnomaDecode
   | BuiltinAnomaVerifyDetached
+  | BuiltinAnomaSign
+  | BuiltinAnomaVerify
   | BuiltinPoseidon
   | BuiltinEcOp
   | BuiltinRandomEcPoint
@@ -229,6 +231,8 @@ instance Pretty BuiltinAxiom where
     BuiltinAnomaEncode -> Str.anomaEncode
     BuiltinAnomaDecode -> Str.anomaDecode
     BuiltinAnomaVerifyDetached -> Str.anomaVerifyDetached
+    BuiltinAnomaSign -> Str.anomaSign
+    BuiltinAnomaVerify -> Str.anomaVerify
     BuiltinPoseidon -> Str.cairoPoseidon
     BuiltinEcOp -> Str.cairoEcOp
     BuiltinRandomEcPoint -> Str.cairoRandomEcPoint

src/Juvix/Compiler/Core/Evaluator.hs

@@ -194,6 +194,8 @@ geval opts herr ctx env0 = eval' env0
       OpAnomaEncode -> anomaEncodeOp
       OpAnomaDecode -> anomaDecodeOp
       OpAnomaVerifyDetached -> anomaVerifyDetachedOp
+      OpAnomaSign -> anomaSignOp
+      OpAnomaVerify -> anomaVerifyOp
       OpPoseidonHash -> poseidonHashOp
       OpEc -> ecOp
       OpRandomEcPoint -> randomEcPointOp
@@ -367,6 +369,24 @@ geval opts herr ctx env0 = eval' env0
                   err "unsupported builtin operation: OpAnomaVerifyDetached"
         {-# INLINE anomaVerifyDetachedOp #-}
 
+        anomaSignOp :: [Node] -> Node
+        anomaSignOp = checkApply $ \arg1 arg2 ->
+          if
+              | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                  mkBuiltinApp' OpAnomaSign (eval' env <$> [arg1, arg2])
+              | otherwise ->
+                  err "unsupported builtin operation: OpAnomaSign"
+        {-# INLINE anomaSignOp #-}
+
+        anomaVerifyOp :: [Node] -> Node
+        anomaVerifyOp = checkApply $ \arg1 arg2 ->
+          if
+              | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                  mkBuiltinApp' OpAnomaVerify (eval' env <$> [arg1, arg2])
+              | otherwise ->
+                  err "unsupported builtin operation: OpAnomaVerify"
+        {-# INLINE anomaVerifyOp #-}
+
         poseidonHashOp :: [Node] -> Node
         poseidonHashOp = unary $ \arg ->
           if

src/Juvix/Compiler/Core/Extra/Utils.hs

@@ -427,6 +427,8 @@ builtinOpArgTypes = \case
   OpAnomaEncode -> [mkDynamic']
   OpAnomaDecode -> [mkDynamic']
   OpAnomaVerifyDetached -> [mkDynamic', mkDynamic', mkDynamic']
+  OpAnomaSign -> [mkDynamic', mkDynamic']
+  OpAnomaVerify -> [mkDynamic', mkDynamic']
   OpPoseidonHash -> [mkDynamic']
   OpEc -> [mkDynamic', mkTypeField', mkDynamic']
   OpRandomEcPoint -> []

src/Juvix/Compiler/Core/Language/Builtins.hs

@@ -30,6 +30,8 @@ data BuiltinOp
   | OpAnomaEncode
   | OpAnomaDecode
   | OpAnomaVerifyDetached
+  | OpAnomaSign
+  | OpAnomaVerify
   | OpPoseidonHash
   | OpEc
   | OpRandomEcPoint
@@ -77,6 +79,8 @@ builtinOpArgsNum = \case
   OpAnomaEncode -> 1
   OpAnomaDecode -> 1
   OpAnomaVerifyDetached -> 3
+  OpAnomaSign -> 2
+  OpAnomaVerify -> 2
   OpPoseidonHash -> 1
   OpEc -> 3
   OpRandomEcPoint -> 0
@@ -117,6 +121,8 @@ builtinIsFoldable = \case
   OpAnomaEncode -> False
   OpAnomaDecode -> False
   OpAnomaVerifyDetached -> False
+  OpAnomaSign -> False
+  OpAnomaVerify -> False
   OpPoseidonHash -> False
   OpEc -> False
   OpRandomEcPoint -> False
@@ -134,4 +140,11 @@ builtinsCairo :: [BuiltinOp]
 builtinsCairo = [OpPoseidonHash, OpEc, OpRandomEcPoint]
 
 builtinsAnoma :: [BuiltinOp]
-builtinsAnoma = [OpAnomaGet, OpAnomaEncode, OpAnomaDecode, OpAnomaVerifyDetached]
+builtinsAnoma =
+  [ OpAnomaGet,
+    OpAnomaEncode,
+    OpAnomaDecode,
+    OpAnomaVerifyDetached,
+    OpAnomaSign,
+    OpAnomaVerify
+  ]

src/Juvix/Compiler/Core/Pretty/Base.hs

@@ -56,6 +56,8 @@ instance PrettyCode BuiltinOp where
     OpAnomaEncode -> return primAnomaEncode
     OpAnomaDecode -> return primAnomaDecode
     OpAnomaVerifyDetached -> return primAnomaVerifyDetached
+    OpAnomaSign -> return primAnomaSign
+    OpAnomaVerify -> return primAnomaVerify
     OpPoseidonHash -> return primPoseidonHash
     OpEc -> return primEc
     OpRandomEcPoint -> return primRandomEcPoint
@@ -813,6 +815,12 @@ primAnomaDecode = primitive Str.anomaDecode
 primAnomaVerifyDetached :: Doc Ann
 primAnomaVerifyDetached = primitive Str.anomaVerifyDetached
 
+primAnomaSign :: Doc Ann
+primAnomaSign = primitive Str.anomaSign
+
+primAnomaVerify :: Doc Ann
+primAnomaVerify = primitive Str.anomaVerify
+
 primPoseidonHash :: Doc Ann
 primPoseidonHash = primitive Str.cairoPoseidon
 

src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs

@@ -70,6 +70,8 @@ computeNodeTypeInfo md = umapL go
           OpAnomaEncode -> Info.getNodeType node
           OpAnomaDecode -> Info.getNodeType node
           OpAnomaVerifyDetached -> Info.getNodeType node
+          OpAnomaSign -> Info.getNodeType node
+          OpAnomaVerify -> Info.getNodeType node
           OpPoseidonHash -> case _builtinAppArgs of
             [arg] -> Info.getNodeType arg
             _ -> error "incorrect poseidon builtin application"

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -580,6 +580,8 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinAnomaEncode -> return ()
       Internal.BuiltinAnomaDecode -> return ()
       Internal.BuiltinAnomaVerifyDetached -> return ()
+      Internal.BuiltinAnomaSign -> return ()
+      Internal.BuiltinAnomaVerify -> return ()
       Internal.BuiltinPoseidon -> return ()
       Internal.BuiltinEcOp -> return ()
       Internal.BuiltinRandomEcPoint -> return ()
@@ -713,7 +715,6 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
               mkSmallUniv
               (mkLambda' natType (mkBuiltinApp' OpAnomaDecode [mkVar' 0]))
           )
-      -- ((ftype ==% (u <>--> nat --> decodeT --> nat --> bool_)) freeVars)
       Internal.BuiltinAnomaVerifyDetached -> do
         natType <- getNatType
         registerAxiomDef
@@ -730,6 +731,32 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
                   )
               )
           )
+      Internal.BuiltinAnomaSign -> do
+        natType <- getNatType
+        registerAxiomDef
+          ( mkLambda'
+              mkSmallUniv
+              ( mkLambda'
+                  (mkVar' 0)
+                  ( mkLambda'
+                      natType
+                      (mkBuiltinApp' OpAnomaSign [mkVar' 1, mkVar' 0])
+                  )
+              )
+          )
+      Internal.BuiltinAnomaVerify -> do
+        natType <- getNatType
+        registerAxiomDef
+          ( mkLambda'
+              mkSmallUniv
+              ( mkLambda'
+                  natType
+                  ( mkLambda'
+                      natType
+                      (mkBuiltinApp' OpAnomaVerify [mkVar' 1, mkVar' 0])
+                  )
+              )
+          )
       Internal.BuiltinPoseidon -> do
         psName <- getPoseidonStateName
         psSym <- getPoseidonStateSymbol
@@ -1137,6 +1164,8 @@ goApplication a = do
         Just Internal.BuiltinAnomaEncode -> app
         Just Internal.BuiltinAnomaDecode -> app
         Just Internal.BuiltinAnomaVerifyDetached -> app
+        Just Internal.BuiltinAnomaSign -> app
+        Just Internal.BuiltinAnomaVerify -> app
         Just Internal.BuiltinPoseidon -> app
         Just Internal.BuiltinEcOp -> app
         Just Internal.BuiltinRandomEcPoint -> app

src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs

@@ -99,6 +99,8 @@ fromCore fsize tab =
         BuiltinAnomaEncode -> False
         BuiltinAnomaDecode -> False
         BuiltinAnomaVerifyDetached -> False
+        BuiltinAnomaSign -> False
+        BuiltinAnomaVerify -> False
         BuiltinPoseidon -> False
         BuiltinEcOp -> False
         BuiltinRandomEcPoint -> False

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -572,6 +572,8 @@ registerBuiltinAxiom d = \case
   BuiltinAnomaEncode -> registerAnomaEncode d
   BuiltinAnomaDecode -> registerAnomaDecode d
   BuiltinAnomaVerifyDetached -> registerAnomaVerifyDetached d
+  BuiltinAnomaSign -> registerAnomaSign d
+  BuiltinAnomaVerify -> registerAnomaVerify d
   BuiltinPoseidon -> registerPoseidon d
   BuiltinEcOp -> registerEcOp d
   BuiltinRandomEcPoint -> registerRandomEcPoint d

src/Juvix/Compiler/Nockma/Encoding/Ed25519.hs

@@ -0,0 +1,9 @@
+module Juvix.Compiler.Nockma.Encoding.Ed25519 where
+
+import Data.ByteString qualified as BS
+import Juvix.Prelude.Base
+
+-- | Remove the Ed25519 signature from a signed message.
+-- The signaure of an Ed25519 message is the first 64 bytes of the signed message.
+removeSignature :: ByteString -> ByteString
+removeSignature = BS.drop 64

src/Juvix/Compiler/Nockma/Evaluator.hs

@@ -10,6 +10,7 @@ import Crypto.Sign.Ed25519
 import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Nockma.Encoding
 import Juvix.Compiler.Nockma.Encoding qualified as Encoding
+import Juvix.Compiler.Nockma.Encoding.Ed25519
 import Juvix.Compiler.Nockma.Evaluator.Error
 import Juvix.Compiler.Nockma.Evaluator.Options
 import Juvix.Compiler.Nockma.Evaluator.Storage
@@ -239,7 +240,13 @@ evalProfile inistack initerm =
               TermCell {} -> throwDecodingFailed args' DecodingErrorExpectedAtom
             StdlibVerifyDetached -> case args' of
               TCell (TermAtom sig) (TCell (TermAtom message) (TermAtom pubKey)) -> goVerifyDetached sig message pubKey
-              _ -> error "expected a term of the form [signature (atom) message (term) public_key (atom)]"
+              _ -> error "expected a term of the form [signature (atom) message (encoded term) public_key (atom)]"
+            StdlibSign -> case args' of
+              TCell (TermAtom message) (TermAtom privKey) -> goSign message privKey
+              _ -> error "expected a term of the form [message (encoded term) private_key (atom)]"
+            StdlibVerify -> case args' of
+              TCell (TermAtom signedMessage) (TermAtom pubKey) -> goVerify signedMessage pubKey
+              _ -> error "expected a term of the form [signedMessage (atom) public_key (atom)]"
           where
             goVerifyDetached :: Atom a -> Atom a -> Atom a -> Sem r (Term a)
             goVerifyDetached sigT messageT pubKeyT = do
@@ -249,6 +256,21 @@ evalProfile inistack initerm =
               let res = dverify pubKey message sig
               return (TermAtom (nockBool res))
 
+            goSign :: Atom a -> Atom a -> Sem r (Term a)
+            goSign messageT privKeyT = do
+              privKey <- SecretKey <$> atomToByteString privKeyT
+              message <- atomToByteString messageT
+              res <- byteStringToAtom (sign privKey message)
+              return (TermAtom res)
+
+            goVerify :: Atom a -> Atom a -> Sem r (Term a)
+            goVerify signedMessageT pubKeyT = do
+              pubKey <- PublicKey <$> atomToByteString pubKeyT
+              signedMessage <- atomToByteString signedMessageT
+              if
+                  | verify pubKey signedMessage -> TermAtom <$> byteStringToAtom (removeSignature signedMessage)
+                  | otherwise -> throwVerificationFailed signedMessageT pubKeyT
+
         goAutoConsCell :: AutoConsCell a -> Sem r (Term a)
         goAutoConsCell c = do
           let w a =

src/Juvix/Compiler/Nockma/Evaluator/Error.hs

@@ -24,6 +24,7 @@ data NockEvalError a
     ErrAssignmentNotFound Text
   | ErrKeyNotInStorage (KeyNotInStorage a)
   | ErrDecodingFailed (DecodingFailed a)
+  | ErrVerificationFailed (VerificationFailed a)
 
 newtype GenericNockEvalError = GenericNockEvalError
   { _genericNockEvalErrorMessage :: AnsiText
@@ -66,6 +67,12 @@ data DecodingFailed a = DecodingFailed
     _decodingFailedReason :: DecodingError
   }
 
+data VerificationFailed a = VerificationFailed
+  { _verificationFailedCtx :: EvalCtx,
+    _verificationFailedMessage :: Atom a,
+    _verificationFailedPublicKey :: Atom a
+  }
+
 throwInvalidNockOp :: (Members '[Error (NockEvalError a), Reader EvalCtx] r) => Atom a -> Sem r x
 throwInvalidNockOp a = do
   ctx <- ask
@@ -128,6 +135,17 @@ throwDecodingFailed a e = do
           _decodingFailedReason = e
         }
 
+throwVerificationFailed :: (Members '[Error (NockEvalError a), Reader EvalCtx] r) => Atom a -> Atom a -> Sem r x
+throwVerificationFailed m k = do
+  ctx <- ask
+  throw $
+    ErrVerificationFailed
+      VerificationFailed
+        { _verificationFailedCtx = ctx,
+          _verificationFailedMessage = m,
+          _verificationFailedPublicKey = k
+        }
+
 instance PrettyCode NoStack where
   ppCode _ = return "Missing stack"
 
@@ -178,6 +196,22 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (DecodingFailed a) where
     r <- ppCode _decodingFailedReason
     return (ctx <> "Decoding the term" <+> t <+> "failed with reason:" <> line <> r)
 
+instance (PrettyCode a, NockNatural a) => PrettyCode (VerificationFailed a) where
+  ppCode VerificationFailed {..} = do
+    m <- ppCode _verificationFailedMessage
+    ctx <- ppCtx _verificationFailedCtx
+    k <- ppCode _verificationFailedPublicKey
+    return
+      ( ctx
+          <> "Signature verification failed for message atom:"
+          <> line
+          <> m
+          <> line
+          <> "and public key atom:"
+          <> line
+          <> k
+      )
+
 instance (PrettyCode a, NockNatural a) => PrettyCode (NockEvalError a) where
   ppCode = \case
     ErrInvalidPath e -> ppCode e
@@ -188,3 +222,4 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (NockEvalError a) where
     ErrAssignmentNotFound e -> return (pretty e)
     ErrKeyNotInStorage e -> ppCode e
     ErrDecodingFailed e -> ppCode e
+    ErrVerificationFailed e -> ppCode e

src/Juvix/Compiler/Nockma/StdlibFunction.hs

@@ -23,3 +23,5 @@ stdlibPath = \case
   StdlibEncode -> [nock| [9 22 0 3] |]
   StdlibDecode -> [nock| [9 94 0 3] |]
   StdlibVerifyDetached -> [nock| [9 22 0 1] |]
+  StdlibSign -> [nock| [9 10 0 1] |]
+  StdlibVerify -> [nock| [9 4 0 1] |]

src/Juvix/Compiler/Nockma/StdlibFunction/Base.hs

@@ -17,6 +17,8 @@ instance Pretty StdlibFunction where
     StdlibEncode -> "encode"
     StdlibDecode -> "decode"
     StdlibVerifyDetached -> "verify-detached"
+    StdlibSign -> "sign"
+    StdlibVerify -> "verify"
 
 data StdlibFunction
   = StdlibDec
@@ -31,6 +33,8 @@ data StdlibFunction
   | StdlibEncode
   | StdlibDecode
   | StdlibVerifyDetached
+  | StdlibSign
+  | StdlibVerify
   deriving stock (Show, Lift, Eq, Bounded, Enum, Generic)
 
 instance Hashable StdlibFunction