Support Anoma stdlib API verifyDetached

package.yaml

@@ -58,6 +58,7 @@ dependencies:
   - deepseq == 1.5.*
   - directory == 1.3.*
   - dlist == 1.0.*
+  - ed25519 == 0.0.*
   - edit-distance == 0.2.*
   - effectful == 2.3.*
   - effectful-core == 2.3.*

src/Juvix/Compiler/Builtins/Anoma.hs

@@ -43,3 +43,17 @@ registerAnomaDecode f = do
     ((ftype ==% (u <>--> nat --> decodeT)) freeVars)
     (error "anomaEncode must be of type {A : Type} -> Nat -> A")
   registerBuiltin BuiltinAnomaDecode (f ^. axiomName)
+
+registerAnomaVerifyDetached :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
+registerAnomaVerifyDetached f = do
+  let ftype = f ^. axiomType
+      u = ExpressionUniverse smallUniverseNoLoc
+      l = getLoc f
+  decodeT <- freshVar l "signedDataT"
+  nat <- getBuiltinName (getLoc f) BuiltinNat
+  bool_ <- getBuiltinName (getLoc f) BuiltinBool
+  let freeVars = HashSet.fromList [decodeT]
+  unless
+    ((ftype ==% (u <>--> nat --> decodeT --> nat --> bool_)) freeVars)
+    (error "anomaVerifyDetached must be of type {A : Type} -> Nat -> A -> Nat -> Bool")
+  registerBuiltin BuiltinAnomaVerifyDetached (f ^. axiomName)

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

@@ -190,6 +190,7 @@ data BuiltinAxiom
   | BuiltinAnomaGet
   | BuiltinAnomaEncode
   | BuiltinAnomaDecode
+  | BuiltinAnomaVerifyDetached
   | BuiltinPoseidon
   | BuiltinEcOp
   | BuiltinRandomEcPoint
@@ -227,6 +228,7 @@ instance Pretty BuiltinAxiom where
     BuiltinAnomaGet -> Str.anomaGet
     BuiltinAnomaEncode -> Str.anomaEncode
     BuiltinAnomaDecode -> Str.anomaDecode
+    BuiltinAnomaVerifyDetached -> Str.anomaVerifyDetached
     BuiltinPoseidon -> Str.cairoPoseidon
     BuiltinEcOp -> Str.cairoEcOp
     BuiltinRandomEcPoint -> Str.cairoRandomEcPoint

src/Juvix/Compiler/Core/Evaluator.hs

@@ -193,6 +193,7 @@ geval opts herr ctx env0 = eval' env0
       OpAnomaGet -> anomaGetOp
       OpAnomaEncode -> anomaEncodeOp
       OpAnomaDecode -> anomaDecodeOp
+      OpAnomaVerifyDetached -> anomaVerifyDetachedOp
       OpPoseidonHash -> poseidonHashOp
       OpEc -> ecOp
       OpRandomEcPoint -> randomEcPointOp
@@ -357,6 +358,15 @@ geval opts herr ctx env0 = eval' env0
                   err "unsupported builtin operation: OpAnomaDecode"
         {-# INLINE anomaDecodeOp #-}
 
+        anomaVerifyDetachedOp :: [Node] -> Node
+        anomaVerifyDetachedOp = checkApply $ \arg1 arg2 arg3 ->
+          if
+              | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                  mkBuiltinApp' OpAnomaVerifyDetached (eval' env <$> [arg1, arg2, arg3])
+              | otherwise ->
+                  err "unsupported builtin operation: OpAnomaVerifyDetached"
+        {-# INLINE anomaVerifyDetachedOp #-}
+
         poseidonHashOp :: [Node] -> Node
         poseidonHashOp = unary $ \arg ->
           if
@@ -563,3 +573,17 @@ toCoreError loc (EvalError {..}) =
       _coreErrorNode = _evalErrorNode,
       _coreErrorLoc = fromMaybe loc (lookupLocation =<< _evalErrorNode)
     }
+
+-- | A class that provides a function `checkApply` that applies a function to a
+-- list of arguments and fails if the length of the arguments list is not equal
+-- to the arity of the function.
+class CheckApplyType a t where
+  checkApply :: t -> [a] -> a
+
+instance CheckApplyType a a where
+  checkApply f [] = f
+  checkApply _ _ = error "too many arguments for operator"
+
+instance (CheckApplyType a r) => CheckApplyType a (a -> r) where
+  checkApply f (x : xs) = checkApply (f x) xs
+  checkApply _ [] = error "too few arguments for operator"

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

@@ -426,6 +426,7 @@ builtinOpArgTypes = \case
   OpAnomaGet -> [mkDynamic']
   OpAnomaEncode -> [mkDynamic']
   OpAnomaDecode -> [mkDynamic']
+  OpAnomaVerifyDetached -> [mkDynamic', mkDynamic', mkDynamic']
   OpPoseidonHash -> [mkDynamic']
   OpEc -> [mkDynamic', mkTypeField', mkDynamic']
   OpRandomEcPoint -> []

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

@@ -29,6 +29,7 @@ data BuiltinOp
   | OpAnomaGet
   | OpAnomaEncode
   | OpAnomaDecode
+  | OpAnomaVerifyDetached
   | OpPoseidonHash
   | OpEc
   | OpRandomEcPoint
@@ -75,6 +76,7 @@ builtinOpArgsNum = \case
   OpAnomaGet -> 1
   OpAnomaEncode -> 1
   OpAnomaDecode -> 1
+  OpAnomaVerifyDetached -> 3
   OpPoseidonHash -> 1
   OpEc -> 3
   OpRandomEcPoint -> 0
@@ -114,6 +116,7 @@ builtinIsFoldable = \case
   OpAnomaGet -> False
   OpAnomaEncode -> False
   OpAnomaDecode -> False
+  OpAnomaVerifyDetached -> False
   OpPoseidonHash -> False
   OpEc -> False
   OpRandomEcPoint -> False
@@ -131,4 +134,4 @@ builtinsCairo :: [BuiltinOp]
 builtinsCairo = [OpPoseidonHash, OpEc, OpRandomEcPoint]
 
 builtinsAnoma :: [BuiltinOp]
-builtinsAnoma = [OpAnomaGet, OpAnomaEncode, OpAnomaDecode]
+builtinsAnoma = [OpAnomaGet, OpAnomaEncode, OpAnomaDecode, OpAnomaVerifyDetached]

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

@@ -55,6 +55,7 @@ instance PrettyCode BuiltinOp where
     OpAnomaGet -> return primAnomaGet
     OpAnomaEncode -> return primAnomaEncode
     OpAnomaDecode -> return primAnomaDecode
+    OpAnomaVerifyDetached -> return primAnomaVerifyDetached
     OpPoseidonHash -> return primPoseidonHash
     OpEc -> return primEc
     OpRandomEcPoint -> return primRandomEcPoint
@@ -809,6 +810,9 @@ primAnomaEncode = primitive Str.anomaEncode
 primAnomaDecode :: Doc Ann
 primAnomaDecode = primitive Str.anomaDecode
 
+primAnomaVerifyDetached :: Doc Ann
+primAnomaVerifyDetached = primitive Str.anomaVerifyDetached
+
 primPoseidonHash :: Doc Ann
 primPoseidonHash = primitive Str.cairoPoseidon
 

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

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

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

@@ -579,6 +579,7 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinAnomaGet -> return ()
       Internal.BuiltinAnomaEncode -> return ()
       Internal.BuiltinAnomaDecode -> return ()
+      Internal.BuiltinAnomaVerifyDetached -> return ()
       Internal.BuiltinPoseidon -> return ()
       Internal.BuiltinEcOp -> return ()
       Internal.BuiltinRandomEcPoint -> return ()
@@ -706,12 +707,28 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
               (mkLambda' (mkVar' 0) (mkBuiltinApp' OpAnomaEncode [mkVar' 0]))
           )
       Internal.BuiltinAnomaDecode -> do
-        natName <- getNatName
-        natSym <- getNatSymbol
+        natType <- getNatType
+        registerAxiomDef
+          ( mkLambda'
+              mkSmallUniv
+              (mkLambda' natType (mkBuiltinApp' OpAnomaDecode [mkVar' 0]))
+          )
+      -- ((ftype ==% (u <>--> nat --> decodeT --> nat --> bool_)) freeVars)
+      Internal.BuiltinAnomaVerifyDetached -> do
+        natType <- getNatType
         registerAxiomDef
           ( mkLambda'
-              (mkTypeConstr (setInfoName natName mempty) natSym [])
-              (mkLambda' (mkVar' 0) (mkBuiltinApp' OpAnomaDecode [mkVar' 0]))
+              mkSmallUniv
+              ( mkLambda'
+                  natType
+                  ( mkLambda'
+                      (mkVar' 0)
+                      ( mkLambda'
+                          natType
+                          (mkBuiltinApp' OpAnomaVerifyDetached [mkVar' 2, mkVar' 1, mkVar' 0])
+                      )
+                  )
+              )
           )
       Internal.BuiltinPoseidon -> do
         psName <- getPoseidonStateName
@@ -739,6 +756,12 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
     getNatName :: Sem r Text
     getNatName = (^. inductiveName) <$> getBuiltinInductiveInfo BuiltinNat
 
+    getNatType :: Sem r Type
+    getNatType = do
+      natName <- getNatName
+      natSym <- getNatSymbol
+      return (mkTypeConstr (setInfoName natName mempty) natSym [])
+
     getIntName :: Sem r Text
     getIntName = (^. inductiveName) <$> getBuiltinInductiveInfo BuiltinInt
 
@@ -1113,6 +1136,7 @@ goApplication a = do
         Just Internal.BuiltinAnomaGet -> app
         Just Internal.BuiltinAnomaEncode -> app
         Just Internal.BuiltinAnomaDecode -> app
+        Just Internal.BuiltinAnomaVerifyDetached -> app
         Just Internal.BuiltinPoseidon -> app
         Just Internal.BuiltinEcOp -> app
         Just Internal.BuiltinRandomEcPoint -> app

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

@@ -98,6 +98,7 @@ fromCore fsize tab =
         BuiltinAnomaGet -> False
         BuiltinAnomaEncode -> False
         BuiltinAnomaDecode -> False
+        BuiltinAnomaVerifyDetached -> False
         BuiltinPoseidon -> False
         BuiltinEcOp -> False
         BuiltinRandomEcPoint -> False

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

@@ -571,6 +571,7 @@ registerBuiltinAxiom d = \case
   BuiltinAnomaGet -> registerAnomaGet d
   BuiltinAnomaEncode -> registerAnomaEncode d
   BuiltinAnomaDecode -> registerAnomaDecode d
+  BuiltinAnomaVerifyDetached -> registerAnomaVerifyDetached d
   BuiltinPoseidon -> registerPoseidon d
   BuiltinEcOp -> registerEcOp d
   BuiltinRandomEcPoint -> registerRandomEcPoint d

src/Juvix/Compiler/Nockma/Encoding.hs

@@ -1,8 +1,10 @@
 module Juvix.Compiler.Nockma.Encoding
   ( module Juvix.Compiler.Nockma.Encoding.Jam,
     module Juvix.Compiler.Nockma.Encoding.Cue,
+    module Juvix.Compiler.Nockma.Encoding.ByteString,
   )
 where
 
+import Juvix.Compiler.Nockma.Encoding.ByteString
 import Juvix.Compiler.Nockma.Encoding.Cue
 import Juvix.Compiler.Nockma.Encoding.Jam

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

@@ -0,0 +1,21 @@
+module Juvix.Compiler.Nockma.Encoding.ByteString where
+
+import Data.Bit
+import Juvix.Compiler.Nockma.Encoding.Base
+import Juvix.Compiler.Nockma.Language
+import Juvix.Prelude.Base
+
+atomToByteString :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => Atom a -> Sem r ByteString
+atomToByteString am = do
+  n <- nockNatural am
+  return (cloneToByteString . integerToVectorBits . toInteger $ n)
+
+byteStringToAtom :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => ByteString -> Sem r (Atom a)
+byteStringToAtom bs = do
+  a <- fromNatural . fromInteger . vectorBitsToInteger . cloneFromByteString $ bs
+  return
+    ( Atom
+        { _atomInfo = emptyAtomInfo,
+          _atom = a
+        }
+    )

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

@@ -72,7 +72,7 @@ consumeLength = do
   if
       | lenOfLen == 0 -> return 0
       | otherwise -> do
-          -- The mist significant bit of the length is omitted
+          -- The most significant bit of the length is omitted
           let lenBits = lenOfLen - 1
           foldlM go (bit lenBits) [0 .. lenBits - 1]
   where

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

@@ -43,7 +43,7 @@ writeLength len = do
 writeAtomTag :: (Member BitWriter r) => Sem r ()
 writeAtomTag = writeZero
 
--- | Write the cell tag 0b01 to the output
+-- | Write the cell tag 0b10 to the output
 writeCellTag :: (Member BitWriter r) => Sem r ()
 writeCellTag = writeOne >> writeZero
 

src/Juvix/Compiler/Nockma/Evaluator.hs

@@ -6,6 +6,7 @@ module Juvix.Compiler.Nockma.Evaluator
   )
 where
 
+import Crypto.Sign.Ed25519
 import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Nockma.Encoding
 import Juvix.Compiler.Nockma.Encoding qualified as Encoding
@@ -236,6 +237,17 @@ evalProfile inistack initerm =
                 r <- Encoding.cueEither a
                 either (throwDecodingFailed args') return r
               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)]"
+          where
+            goVerifyDetached :: Atom a -> Atom a -> Atom a -> Sem r (Term a)
+            goVerifyDetached sigT messageT pubKeyT = do
+              sig <- Signature <$> atomToByteString sigT
+              pubKey <- PublicKey <$> atomToByteString pubKeyT
+              message <- atomToByteString messageT
+              let res = dverify pubKey message sig
+              return (TermAtom (nockBool res))
 
         goAutoConsCell :: AutoConsCell a -> Sem r (Term a)
         goAutoConsCell c = do

src/Juvix/Compiler/Nockma/StdlibFunction.hs

@@ -22,3 +22,4 @@ stdlibPath = \case
   StdlibPow2 -> [nock| [9 4 0 7] |]
   StdlibEncode -> [nock| [9 22 0 3] |]
   StdlibDecode -> [nock| [9 94 0 3] |]
+  StdlibVerifyDetached -> [nock| [9 22 0 1] |]

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

@@ -16,6 +16,7 @@ instance Pretty StdlibFunction where
     StdlibPow2 -> "pow2"
     StdlibEncode -> "encode"
     StdlibDecode -> "decode"
+    StdlibVerifyDetached -> "verify-detached"
 
 data StdlibFunction
   = StdlibDec
@@ -29,6 +30,7 @@ data StdlibFunction
   | StdlibPow2
   | StdlibEncode
   | StdlibDecode
+  | StdlibVerifyDetached
   deriving stock (Show, Lift, Eq, Bounded, Enum, Generic)
 
 instance Hashable StdlibFunction

src/Juvix/Compiler/Nockma/Translation/FromTree.hs

@@ -424,8 +424,9 @@ compile = \case
       args <- mapM compile _nodeAnomaArgs
       case _nodeAnomaOpcode of
         Tree.OpAnomaGet -> goAnomaGet args
-        Tree.OpAnomaEncode -> goAnomaEncode args
-        Tree.OpAnomaDecode -> goAnomaDecode args
+        Tree.OpAnomaEncode -> return (goAnomaEncode args)
+        Tree.OpAnomaDecode -> return (goAnomaDecode args)
+        Tree.OpAnomaVerifyDetached -> return (goAnomaVerifyDetached args)
 
     goUnop :: Tree.NodeUnop -> Sem r (Term Natural)
     goUnop Tree.NodeUnop {..} = do
@@ -450,11 +451,16 @@ compile = \case
       let arg = remakeList [getFieldInSubject AnomaGetOrder, foldTermsOrNil key]
       return (OpScry # (OpQuote # nockNilTagged "OpScry-typehint") # arg)
 
-    goAnomaEncode :: [Term Natural] -> Sem r (Term Natural)
-    goAnomaEncode args = return (callStdlib StdlibEncode args)
+    goAnomaEncode :: [Term Natural] -> Term Natural
+    goAnomaEncode = callStdlib StdlibEncode
 
-    goAnomaDecode :: [Term Natural] -> Sem r (Term Natural)
-    goAnomaDecode args = return (callStdlib StdlibDecode args)
+    goAnomaDecode :: [Term Natural] -> Term Natural
+    goAnomaDecode = callStdlib StdlibDecode
+
+    goAnomaVerifyDetached :: [Term Natural] -> Term Natural
+    goAnomaVerifyDetached = \case
+      [sig, message, pubKey] -> callStdlib StdlibVerifyDetached [sig, goAnomaEncode [message], pubKey]
+      _ -> impossible
 
     goTrace :: Term Natural -> Sem r (Term Natural)
     goTrace arg = do

src/Juvix/Compiler/Tree/Keywords.hs

@@ -12,6 +12,7 @@ import Juvix.Data.Keyword.All
     kwAnomaDecode,
     kwAnomaEncode,
     kwAnomaGet,
+    kwAnomaVerifyDetached,
     kwArgsNum,
     kwAtoi,
     kwBr,
@@ -78,6 +79,7 @@ allKeywords =
          kwAnomaGet,
          kwAnomaDecode,
          kwAnomaEncode,
+         kwAnomaVerifyDetached,
          kwPoseidon,
          kwEcOp,
          kwRandomEcPoint

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

@@ -56,4 +56,6 @@ data AnomaOp
     OpAnomaEncode
   | -- | Decode a value from an Anoma atom
     OpAnomaDecode
+  | -- | Verify a cryptogtaphic signature of an Anoma value
+    OpAnomaVerifyDetached
   deriving stock (Eq)

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

@@ -245,6 +245,7 @@ instance PrettyCode AnomaOp where
     OpAnomaGet -> Str.anomaGet
     OpAnomaEncode -> Str.anomaEncode
     OpAnomaDecode -> Str.anomaDecode
+    OpAnomaVerifyDetached -> Str.anomaVerifyDetached
 
 instance PrettyCode UnaryOpcode where
   ppCode = \case

src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs

@@ -14,6 +14,7 @@ checkNoAnoma = walkT checkNode
         OpAnomaGet -> unsupportedErr "OpAnomaGet"
         OpAnomaEncode -> unsupportedErr "OpAnomaEncode"
         OpAnomaDecode -> unsupportedErr "OpAnomaDecode"
+        OpAnomaVerifyDetached -> unsupportedErr "OpAnomaVerifyDetached"
         where
           unsupportedErr :: Text -> Sem r ()
           unsupportedErr opName =