Support Anoma stdlib sign-detached API

This is requried to support to new Anoma nullifier format:

anoma/anoma@d6a6145

src/Juvix/Compiler/Builtins/Anoma.hs

@@ -83,3 +83,16 @@ registerAnomaVerify f = do
     ((ftype ==% (u <>--> nat --> nat --> dataT)) freeVars)
     (error "anomaVerify must be of type {A : Type} -> Nat -> Nat -> A")
   registerBuiltin BuiltinAnomaVerify (f ^. axiomName)
+
+registerAnomaSignDetached :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
+registerAnomaSignDetached 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 "anomaSignDetached must be of type {A : Type} -> A -> Nat -> Nat")
+  registerBuiltin BuiltinAnomaSignDetached (f ^. axiomName)

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

@@ -200,6 +200,7 @@ data BuiltinAxiom
   | BuiltinAnomaDecode
   | BuiltinAnomaVerifyDetached
   | BuiltinAnomaSign
+  | BuiltinAnomaSignDetached
   | BuiltinAnomaVerify
   | BuiltinPoseidon
   | BuiltinEcOp
@@ -241,6 +242,7 @@ instance Pretty BuiltinAxiom where
     BuiltinAnomaEncode -> Str.anomaEncode
     BuiltinAnomaDecode -> Str.anomaDecode
     BuiltinAnomaVerifyDetached -> Str.anomaVerifyDetached
+    BuiltinAnomaSignDetached -> Str.anomaSignDetached
     BuiltinAnomaSign -> Str.anomaSign
     BuiltinAnomaVerify -> Str.anomaVerify
     BuiltinPoseidon -> Str.cairoPoseidon

src/Juvix/Compiler/Core/Evaluator.hs

@@ -195,6 +195,7 @@ geval opts herr ctx env0 = eval' env0
       OpAnomaDecode -> anomaDecodeOp
       OpAnomaVerifyDetached -> anomaVerifyDetachedOp
       OpAnomaSign -> anomaSignOp
+      OpAnomaSignDetached -> anomaSignDetachedOp
       OpAnomaVerify -> anomaVerifyOp
       OpPoseidonHash -> poseidonHashOp
       OpEc -> ecOp
@@ -378,6 +379,15 @@ geval opts herr ctx env0 = eval' env0
                   err "unsupported builtin operation: OpAnomaSign"
         {-# INLINE anomaSignOp #-}
 
+        anomaSignDetachedOp :: [Node] -> Node
+        anomaSignDetachedOp = checkApply $ \arg1 arg2 ->
+          if
+              | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                  mkBuiltinApp' OpAnomaSignDetached (eval' env <$> [arg1, arg2])
+              | otherwise ->
+                  err "unsupported builtin operation: OpAnomaSignDetached"
+        {-# INLINE anomaSignDetachedOp #-}
+
         anomaVerifyOp :: [Node] -> Node
         anomaVerifyOp = checkApply $ \arg1 arg2 ->
           if

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

@@ -428,6 +428,7 @@ builtinOpArgTypes = \case
   OpAnomaDecode -> [mkDynamic']
   OpAnomaVerifyDetached -> [mkDynamic', mkDynamic', mkDynamic']
   OpAnomaSign -> [mkDynamic', mkDynamic']
+  OpAnomaSignDetached -> [mkDynamic', mkDynamic']
   OpAnomaVerify -> [mkDynamic', mkDynamic']
   OpPoseidonHash -> [mkDynamic']
   OpEc -> [mkDynamic', mkTypeField', mkDynamic']

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

@@ -31,6 +31,7 @@ data BuiltinOp
   | OpAnomaDecode
   | OpAnomaVerifyDetached
   | OpAnomaSign
+  | OpAnomaSignDetached
   | OpAnomaVerify
   | OpPoseidonHash
   | OpEc
@@ -84,6 +85,7 @@ builtinOpArgsNum = \case
   OpAnomaDecode -> 1
   OpAnomaVerifyDetached -> 3
   OpAnomaSign -> 2
+  OpAnomaSignDetached -> 2
   OpAnomaVerify -> 2
   OpPoseidonHash -> 1
   OpEc -> 3
@@ -126,6 +128,7 @@ builtinIsFoldable = \case
   OpAnomaDecode -> False
   OpAnomaVerifyDetached -> False
   OpAnomaSign -> False
+  OpAnomaSignDetached -> False
   OpAnomaVerify -> False
   OpPoseidonHash -> False
   OpEc -> False
@@ -150,5 +153,6 @@ builtinsAnoma =
     OpAnomaDecode,
     OpAnomaVerifyDetached,
     OpAnomaSign,
-    OpAnomaVerify
+    OpAnomaVerify,
+    OpAnomaSignDetached
   ]

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

@@ -57,6 +57,7 @@ instance PrettyCode BuiltinOp where
     OpAnomaDecode -> return primAnomaDecode
     OpAnomaVerifyDetached -> return primAnomaVerifyDetached
     OpAnomaSign -> return primAnomaSign
+    OpAnomaSignDetached -> return primAnomaSignDetached
     OpAnomaVerify -> return primAnomaVerify
     OpPoseidonHash -> return primPoseidonHash
     OpEc -> return primEc
@@ -815,6 +816,9 @@ primAnomaVerifyDetached = primitive Str.anomaVerifyDetached
 primAnomaSign :: Doc Ann
 primAnomaSign = primitive Str.anomaSign
 
+primAnomaSignDetached :: Doc Ann
+primAnomaSignDetached = primitive Str.anomaSignDetached
+
 primAnomaVerify :: Doc Ann
 primAnomaVerify = primitive Str.anomaVerify
 

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

@@ -71,6 +71,7 @@ computeNodeTypeInfo md = umapL go
           OpAnomaDecode -> Info.getNodeType node
           OpAnomaVerifyDetached -> Info.getNodeType node
           OpAnomaSign -> Info.getNodeType node
+          OpAnomaSignDetached -> Info.getNodeType node
           OpAnomaVerify -> Info.getNodeType node
           OpPoseidonHash -> case _builtinAppArgs of
             [arg] -> Info.getNodeType arg

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

@@ -588,6 +588,7 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinAnomaDecode -> return ()
       Internal.BuiltinAnomaVerifyDetached -> return ()
       Internal.BuiltinAnomaSign -> return ()
+      Internal.BuiltinAnomaSignDetached -> return ()
       Internal.BuiltinAnomaVerify -> return ()
       Internal.BuiltinPoseidon -> return ()
       Internal.BuiltinEcOp -> return ()
@@ -751,6 +752,19 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
                   )
               )
           )
+      Internal.BuiltinAnomaSignDetached -> do
+        natType <- getNatType
+        registerAxiomDef
+          ( mkLambda'
+              mkSmallUniv
+              ( mkLambda'
+                  (mkVar' 0)
+                  ( mkLambda'
+                      natType
+                      (mkBuiltinApp' OpAnomaSignDetached [mkVar' 1, mkVar' 0])
+                  )
+              )
+          )
       Internal.BuiltinAnomaVerify -> do
         natType <- getNatType
         registerAxiomDef
@@ -1172,6 +1186,7 @@ goApplication a = do
         Just Internal.BuiltinAnomaDecode -> app
         Just Internal.BuiltinAnomaVerifyDetached -> app
         Just Internal.BuiltinAnomaSign -> app
+        Just Internal.BuiltinAnomaSignDetached -> app
         Just Internal.BuiltinAnomaVerify -> app
         Just Internal.BuiltinPoseidon -> app
         Just Internal.BuiltinEcOp -> app

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

@@ -100,6 +100,7 @@ fromCore fsize tab =
         BuiltinAnomaDecode -> False
         BuiltinAnomaVerifyDetached -> False
         BuiltinAnomaSign -> False
+        BuiltinAnomaSignDetached -> False
         BuiltinAnomaVerify -> False
         BuiltinPoseidon -> False
         BuiltinEcOp -> False

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

@@ -573,6 +573,7 @@ registerBuiltinAxiom d = \case
   BuiltinAnomaDecode -> registerAnomaDecode d
   BuiltinAnomaVerifyDetached -> registerAnomaVerifyDetached d
   BuiltinAnomaSign -> registerAnomaSign d
+  BuiltinAnomaSignDetached -> registerAnomaSignDetached d
   BuiltinAnomaVerify -> registerAnomaVerify d
   BuiltinPoseidon -> registerPoseidon d
   BuiltinEcOp -> registerEcOp d

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

@@ -6,9 +6,14 @@ import Data.ByteString.Builder qualified as BS
 import Juvix.Compiler.Nockma.Language
 import Juvix.Prelude.Base
 
+-- | Encode an atom to little-endian bytes
 atomToByteString :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => Atom a -> Sem r ByteString
 atomToByteString = fmap naturalToByteString . nockNatural
 
+-- | Encode an atom to little-endian bytes, padded with zeros up to a specified length
+atomToByteStringLen :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => Int -> Atom a -> Sem r ByteString
+atomToByteStringLen len = fmap (padByteString len) . atomToByteString
+
 byteStringToAtom :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => ByteString -> Sem r (Atom a)
 byteStringToAtom = fmap mkEmptyAtom . fromNatural . byteStringToNatural
 
@@ -48,3 +53,9 @@ mkEmptyAtom x =
     { _atomInfo = emptyAtomInfo,
       _atom = x
     }
+
+-- | Pad a ByteString with zeros up to a specified length
+padByteString :: Int -> ByteString -> ByteString
+padByteString n bs
+  | BS.length bs >= n = bs
+  | otherwise = BS.append bs (BS.replicate (n - BS.length bs) 0)

src/Juvix/Compiler/Nockma/Evaluator.hs

@@ -244,6 +244,9 @@ evalProfile inistack initerm =
             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)]"
+            StdlibSignDetached -> case args' of
+              TCell (TermAtom message) (TermAtom privKey) -> goSignDetached 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)]"
@@ -254,24 +257,41 @@ evalProfile inistack initerm =
             goCat :: Atom a -> Atom a -> Sem r (Term a)
             goCat arg1 arg2 = TermAtom . setAtomHint AtomHintString <$> atomConcatenateBytes arg1 arg2
 
+            signatureLength :: Int
+            signatureLength = 64
+
+            publicKeyLength :: Int
+            publicKeyLength = 32
+
+            privateKeyLength :: Int
+            privateKeyLength = 64
+
             goVerifyDetached :: Atom a -> Atom a -> Atom a -> Sem r (Term a)
             goVerifyDetached sigT messageT pubKeyT = do
-              sig <- Signature <$> atomToByteString sigT
-              pubKey <- PublicKey <$> atomToByteString pubKeyT
+              sig <- Signature <$> atomToByteStringLen signatureLength sigT
+              pubKey <- PublicKey <$> atomToByteStringLen publicKeyLength pubKeyT
               message <- atomToByteString messageT
               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
+              privKey <- SecretKey <$> atomToByteStringLen privateKeyLength privKeyT
               message <- atomToByteString messageT
               res <- byteStringToAtom (sign privKey message)
               return (TermAtom res)
 
+            goSignDetached :: Atom a -> Atom a -> Sem r (Term a)
+            goSignDetached messageT privKeyT = do
+              privKey <- SecretKey <$> atomToByteStringLen privateKeyLength privKeyT
+              message <- atomToByteString messageT
+              let (Signature sig) = dsign privKey message
+              res <- byteStringToAtom sig
+              return (TermAtom res)
+
             goVerify :: Atom a -> Atom a -> Sem r (Term a)
             goVerify signedMessageT pubKeyT = do
-              pubKey <- PublicKey <$> atomToByteString pubKeyT
+              pubKey <- PublicKey <$> atomToByteStringLen publicKeyLength pubKeyT
               signedMessage <- atomToByteString signedMessageT
               if
                   | verify pubKey signedMessage -> TermAtom <$> byteStringToAtom (removeSignature signedMessage)

src/Juvix/Compiler/Nockma/StdlibFunction.hs

@@ -24,6 +24,7 @@ stdlibPath = \case
   StdlibDecode -> [nock| [9 94 0 3] |]
   StdlibVerifyDetached -> [nock| [9 22 0 1] |]
   StdlibSign -> [nock| [9 10 0 1] |]
+  StdlibSignDetached -> [nock| [9 23 0 1] |]
   StdlibVerify -> [nock| [9 4 0 1] |]
   -- Obtained from the urbit dojo using:
   --

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

@@ -18,6 +18,7 @@ instance Pretty StdlibFunction where
     StdlibDecode -> "decode"
     StdlibVerifyDetached -> "verify-detached"
     StdlibSign -> "sign"
+    StdlibSignDetached -> "sign-detached"
     StdlibVerify -> "verify"
     StdlibCatBytes -> "cat"
 
@@ -35,6 +36,7 @@ data StdlibFunction
   | StdlibDecode
   | StdlibVerifyDetached
   | StdlibSign
+  | StdlibSignDetached
   | StdlibVerify
   | StdlibCatBytes
   deriving stock (Show, Lift, Eq, Bounded, Enum, Generic)

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

@@ -438,6 +438,7 @@ compile = \case
         Tree.OpAnomaVerifyDetached -> return (goAnomaVerifyDetached args)
         Tree.OpAnomaSign -> return (goAnomaSign args)
         Tree.OpAnomaVerify -> return (goAnomaVerify args)
+        Tree.OpAnomaSignDetached -> return (goAnomaSignDetached args)
 
     goUnop :: Tree.NodeUnop -> Sem r (Term Natural)
     goUnop Tree.NodeUnop {..} = do
@@ -478,6 +479,11 @@ compile = \case
       [message, privKey] -> callStdlib StdlibSign [goAnomaEncode [message], privKey]
       _ -> impossible
 
+    goAnomaSignDetached :: [Term Natural] -> Term Natural
+    goAnomaSignDetached = \case
+      [message, privKey] -> callStdlib StdlibSignDetached [goAnomaEncode [message], privKey]
+      _ -> impossible
+
     goAnomaVerify :: [Term Natural] -> Term Natural
     goAnomaVerify = \case
       [signedMessage, pubKey] -> callStdlib StdlibDecode [callStdlib StdlibVerify [signedMessage, pubKey]]

src/Juvix/Compiler/Tree/Keywords.hs

@@ -13,6 +13,7 @@ import Juvix.Data.Keyword.All
     kwAnomaEncode,
     kwAnomaGet,
     kwAnomaSign,
+    kwAnomaSignDetached,
     kwAnomaVerify,
     kwAnomaVerifyDetached,
     kwArgsNum,
@@ -83,6 +84,7 @@ allKeywords =
          kwAnomaEncode,
          kwAnomaVerifyDetached,
          kwAnomaSign,
+         kwAnomaSignDetached,
          kwAnomaVerify,
          kwPoseidon,
          kwEcOp,

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

@@ -62,4 +62,6 @@ data AnomaOp
     OpAnomaSign
   | -- | Verify a signature obtained from OpAnomaSign using a public key
     OpAnomaVerify
+  | -- | Produce a cryptographic signature of an Anoma value
+    OpAnomaSignDetached
   deriving stock (Eq)

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

@@ -248,6 +248,7 @@ instance PrettyCode AnomaOp where
     OpAnomaVerifyDetached -> Str.anomaVerifyDetached
     OpAnomaSign -> Str.anomaSign
     OpAnomaVerify -> Str.anomaVerify
+    OpAnomaSignDetached -> Str.anomaSignDetached
 
 instance PrettyCode UnaryOpcode where
   ppCode = \case

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

@@ -16,6 +16,7 @@ checkNoAnoma = walkT checkNode
         OpAnomaDecode -> unsupportedErr "OpAnomaDecode"
         OpAnomaVerifyDetached -> unsupportedErr "OpAnomaVerifyDetached"
         OpAnomaSign -> unsupportedErr "OpAnomaSign"
+        OpAnomaSignDetached -> unsupportedErr "OpAnomaSignDetached"
         OpAnomaVerify -> unsupportedErr "OpAnomaVerify"
         where
           unsupportedErr :: Text -> Sem r ()

src/Juvix/Compiler/Tree/Translation/FromCore.hs

@@ -318,6 +318,7 @@ genCode infoTable fi =
       Core.OpAnomaDecode -> OpAnomaDecode
       Core.OpAnomaVerifyDetached -> OpAnomaVerifyDetached
       Core.OpAnomaSign -> OpAnomaSign
+      Core.OpAnomaSignDetached -> OpAnomaSignDetached
       Core.OpAnomaVerify -> OpAnomaVerify
       _ -> impossible
 

src/Juvix/Compiler/Tree/Translation/FromSource.hs

@@ -128,6 +128,7 @@ parseAnoma =
     <|> parseAnoma' kwAnomaEncode OpAnomaEncode
     <|> parseAnoma' kwAnomaVerifyDetached OpAnomaVerifyDetached
     <|> parseAnoma' kwAnomaSign OpAnomaSign
+    <|> parseAnoma' kwAnomaSignDetached OpAnomaSignDetached
     <|> parseAnoma' kwAnomaVerify OpAnomaVerify
 
 parseAnoma' ::

src/Juvix/Data/Keyword/All.hs

@@ -457,6 +457,9 @@ kwAnomaVerifyDetached = asciiKw Str.anomaVerifyDetached
 kwAnomaSign :: Keyword
 kwAnomaSign = asciiKw Str.anomaSign
 
+kwAnomaSignDetached :: Keyword
+kwAnomaSignDetached = asciiKw Str.anomaSignDetached
+
 kwAnomaVerify :: Keyword
 kwAnomaVerify = asciiKw Str.anomaVerify
 

src/Juvix/Extra/Strings.hs

@@ -344,6 +344,9 @@ anomaVerifyDetached = "anoma-verify-detached"
 anomaSign :: (IsString s) => s
 anomaSign = "anoma-sign"
 
+anomaSignDetached :: (IsString s) => s
+anomaSignDetached = "anoma-sign-detached"
+
 anomaVerify :: (IsString s) => s
 anomaVerify = "anoma-verify"
 

test/Tree/Transformation/CheckNoAnoma.hs

@@ -83,5 +83,9 @@ tests =
     Eval.NegTest
       "anomaVerify"
       $(mkRelDir ".")
-      $(mkRelFile "test014.jvt")
+      $(mkRelFile "test014.jvt"),
+    Eval.NegTest
+      "anomaSignDetached"
+      $(mkRelDir ".")
+      $(mkRelFile "test015.jvt")
   ]