Support Anoma stdlib sign-detached API (#2798)

This PR adds support for the Anoma stdlib `sign-detached` API.

```
builtin anoma-sign-detached
axiom anomaSignDetached : {A : Type}
  -- message to sign
  -> A
  -- private key
  -> Nat
 -- signature
  -> Nat;
```

This corresponds to the
[sign_detached](https://hexdocs.pm/enacl/enacl.html#sign_detached-2)
libsodium API.

This is requried to support to new Anoma nullifier format:


anoma/anoma@d6a6145

Previously resource nullifiers were defined using `anomaSign`:

```
nullifier (r : Resource) (secretKey : Nat) : Nat :=
  anomaSign (anomaEncode (nullifierHeader, r)) secretKey;
```

They are now defined using `anomaSignDetached`:

```
nullifier (r : Resource) (secretKey : Nat) : Nat :=
  let encodedResource : Nat := anomaEncode (nullifierHeader, r) in
  anomaEncode (encodedResource , anomaSignDetached encodedResource secretKey);
```

This is so that a logic function can access the nullified resources
directly from the `nullifier` field.

## Evaluator Note

When decoding a public key, private key or signature from an integer
atom to a bytestring it's important to pad the bytestring to the
appropriate number of bytes. For example a private key must be 64 bytes
but the corresponding encoded integer may fit into 63 bytes or fewer
bytes (depending on leading zeros). This PR also fixes this issue by
adding a
[`atomToByteStringLen`](https://github.com/anoma/juvix/blob/c68c7187b1bbb5f751c1fc5e4c2154dde59b81e9/src/Juvix/Compiler/Nockma/Encoding/ByteString.hs#L14)
function with also accepts the expected size of the resulting
bytestring.

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")
   ]