Use ByteArray for Anoma cryptographic builtins

src/Juvix/Compiler/Builtins/Anoma.hs

@@ -50,12 +50,12 @@ registerAnomaVerifyDetached f = do
       u = ExpressionUniverse smallUniverseNoLoc
       l = getLoc f
   decodeT <- freshVar l "signedDataT"
-  nat <- getBuiltinName (getLoc f) BuiltinNat
+  byteArray <- getBuiltinName (getLoc f) BuiltinByteArray
   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")
+    ((ftype ==% (u <>--> byteArray --> decodeT --> byteArray --> bool_)) freeVars)
+    (error "anomaVerifyDetached must be of type {A : Type} -> ByteArray -> A -> ByteArray -> Bool")
   registerBuiltin BuiltinAnomaVerifyDetached (f ^. axiomName)
 
 registerAnomaSign :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
@@ -64,11 +64,11 @@ registerAnomaSign f = do
       u = ExpressionUniverse smallUniverseNoLoc
       l = getLoc f
   dataT <- freshVar l "dataT"
-  nat <- getBuiltinName (getLoc f) BuiltinNat
+  byteArray <- getBuiltinName (getLoc f) BuiltinByteArray
   let freeVars = HashSet.fromList [dataT]
   unless
-    ((ftype ==% (u <>--> dataT --> nat --> nat)) freeVars)
-    (error "anomaSign must be of type {A : Type} -> A -> Nat -> Nat")
+    ((ftype ==% (u <>--> dataT --> byteArray --> byteArray)) freeVars)
+    (error "anomaSign must be of type {A : Type} -> A -> ByteArray -> ByteArray")
   registerBuiltin BuiltinAnomaSign (f ^. axiomName)
 
 registerAnomaVerifyWithMessage :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
@@ -77,12 +77,12 @@ registerAnomaVerifyWithMessage f = do
       u = ExpressionUniverse smallUniverseNoLoc
       l = getLoc f
   dataT <- freshVar l "dataT"
-  nat <- getBuiltinName (getLoc f) BuiltinNat
+  byteArray <- getBuiltinName (getLoc f) BuiltinByteArray
   maybe_ <- getBuiltinName (getLoc f) BuiltinMaybe
   let freeVars = HashSet.fromList [dataT]
   unless
-    ((ftype ==% (u <>--> nat --> nat --> maybe_ @@ dataT)) freeVars)
-    (error "anomaVerify must be of type {A : Type} -> Nat -> Nat -> Maybe A")
+    ((ftype ==% (u <>--> byteArray --> byteArray --> maybe_ @@ dataT)) freeVars)
+    (error "anomaVerify must be of type {A : Type} -> byteArray -> byteArray -> Maybe A")
   registerBuiltin BuiltinAnomaVerifyWithMessage (f ^. axiomName)
 
 registerAnomaSignDetached :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
@@ -91,9 +91,9 @@ registerAnomaSignDetached f = do
       u = ExpressionUniverse smallUniverseNoLoc
       l = getLoc f
   dataT <- freshVar l "dataT"
-  nat <- getBuiltinName (getLoc f) BuiltinNat
+  byteArray <- getBuiltinName (getLoc f) BuiltinByteArray
   let freeVars = HashSet.fromList [dataT]
   unless
-    ((ftype ==% (u <>--> dataT --> nat --> nat)) freeVars)
-    (error "anomaSignDetached must be of type {A : Type} -> A -> Nat -> Nat")
+    ((ftype ==% (u <>--> dataT --> byteArray --> byteArray)) freeVars)
+    (error "anomaSignDetached must be of type {A : Type} -> A -> ByteArray -> ByteArray")
   registerBuiltin BuiltinAnomaSignDetached (f ^. axiomName)

src/Juvix/Compiler/Core/Evaluator.hs

@@ -390,9 +390,9 @@ geval opts herr tab env0 = eval' env0
                   | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
                       mkBuiltinApp' OpAnomaVerifyDetached [v1, v2, v3]
                   | otherwise ->
-                      case (integerFromNode v1, integerFromNode v3) of
-                        (Just i1, Just i3) -> verifyDetached i1 v2 i3
-                        _ -> err "OpAnomaVerifyDetached: first and third arguments must be integers"
+                      case (byteStringFromNode v1, byteStringFromNode v3) of
+                        (Just bs1, Just bs3) -> verifyDetached bs1 v2 bs3
+                        _ -> err "OpAnomaVerifyDetached: first and third arguments must be bytearrays"
         {-# INLINE anomaVerifyDetachedOp #-}
 
         anomaSignOp :: [Node] -> Node
@@ -402,9 +402,9 @@ geval opts herr tab env0 = eval' env0
            in if
                   | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
                       mkBuiltinApp' OpAnomaSign [v1, v2]
-                  | otherwise -> case integerFromNode v2 of
-                      Just i -> sign v1 i
-                      Nothing -> err "anomaSignOp: second argument not an integer"
+                  | otherwise -> case byteStringFromNode v2 of
+                      Just bs -> sign v1 bs
+                      Nothing -> err "anomaSignOp: second argument not an bytearray"
         {-# INLINE anomaSignOp #-}
 
         anomaSignDetachedOp :: [Node] -> Node
@@ -414,9 +414,9 @@ geval opts herr tab env0 = eval' env0
            in if
                   | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
                       mkBuiltinApp' OpAnomaSignDetached [v1, v2]
-                  | otherwise -> case integerFromNode v2 of
+                  | otherwise -> case byteStringFromNode v2 of
                       Just i -> signDetached v1 i
-                      Nothing -> err "anomaSignDetachedOp: second argument not an integer"
+                      Nothing -> err "anomaSignDetachedOp: second argument not a bytearray"
         {-# INLINE anomaSignDetachedOp #-}
 
         anomaVerifyWithMessageOp :: [Node] -> Node
@@ -427,9 +427,9 @@ geval opts herr tab env0 = eval' env0
                   | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
                       mkBuiltinApp' OpAnomaVerifyWithMessage [v1, v2]
                   | otherwise ->
-                      case (integerFromNode v1, integerFromNode v2) of
-                        (Just i1, Just i2) -> verify i1 i2
-                        _ -> err "anomaVerifyWithMessageOp: both arguments are not integers"
+                      case (byteStringFromNode v1, byteStringFromNode v2) of
+                        (Just bs1, Just bs2) -> verify bs1 bs2
+                        _ -> err "anomaVerifyWithMessageOp: both arguments are not bytearrays"
         {-# INLINE anomaVerifyWithMessageOp #-}
 
         poseidonHashOp :: [Node] -> Node
@@ -483,96 +483,100 @@ geval opts herr tab env0 = eval' env0
             decodeErr = err "failed to decode Integer"
         {-# INLINE decodeByteString #-}
 
-        sign :: Node -> Integer -> Node
-        sign !messageNode !secretKeyInt =
+        sign :: Node -> ByteString -> Node
+        sign !messageNode !secretKeyBs =
           let !message = serializeNode messageNode
-              !secretKey = secretKeyFromInteger secretKeyInt
-           in nodeFromInteger (Encoding.encodeByteString (E.sign secretKey message))
+              !secretKey = E.SecretKey secretKeyBs
+           in nodeFromByteString (E.sign secretKey message)
         {-# INLINE sign #-}
 
-        verify :: Integer -> Integer -> Node
-        verify !signedMessageInt !publicKeyInt =
-          let !signedMessage = decodeByteString signedMessageInt
-              !publicKey = publicKeyFromInteger publicKeyInt
+        verify :: ByteString -> ByteString -> Node
+        verify !signedMessage !publicKeyBs =
+          let !publicKey = E.PublicKey publicKeyBs
            in if
                   | E.verify publicKey signedMessage -> nodeMaybeJust (deserializeNode (E.removeSignature signedMessage))
                   | otherwise -> nodeMaybeNothing
         {-# INLINE verify #-}
 
-        signDetached :: Node -> Integer -> Node
-        signDetached !messageNode !secretKeyInt =
+        signDetached :: Node -> ByteString -> Node
+        signDetached !messageNode !secretKeyBs =
           let !message = serializeNode messageNode
-              !secretKey = secretKeyFromInteger secretKeyInt
+              !secretKey = E.SecretKey secretKeyBs
               (E.Signature !sig) = E.dsign secretKey message
-           in nodeFromInteger (Encoding.encodeByteString sig)
+           in nodeFromByteString sig
         {-# INLINE signDetached #-}
 
-        verifyDetached :: Integer -> Node -> Integer -> Node
-        verifyDetached !signatureInt !messageNode !publicKeyInt =
-          let !sig = E.Signature (decodeByteString signatureInt)
+        verifyDetached :: ByteString -> Node -> ByteString -> Node
+        verifyDetached !signatureBs !messageNode !publicKeyBs =
+          let !sig = E.Signature signatureBs
               !message = serializeNode messageNode
-              !publicKey = publicKeyFromInteger publicKeyInt
+              !publicKey = E.PublicKey publicKeyBs
            in nodeFromBool (E.dverify publicKey message sig)
         {-# INLINE verifyDetached #-}
 
         uint8FromIntOp :: [Node] -> Node
         uint8FromIntOp =
           unary $ \node ->
             let !v = eval' env node
-             in nodeFromUInt8
-                  . fromIntegral
-                  . fromMaybe (evalError "expected integer" v)
-                  . integerFromNode
-                  $ v
+             in if
+                    | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                        mkBuiltinApp' OpUInt8FromInt [v]
+                    | otherwise ->
+                        nodeFromUInt8
+                          . fromIntegral
+                          . fromMaybe (evalError "expected integer" v)
+                          . integerFromNode
+                          $ v
         {-# INLINE uint8FromIntOp #-}
 
         uint8ToIntOp :: [Node] -> Node
         uint8ToIntOp =
           unary $ \node ->
             let !v = eval' env node
-             in nodeFromInteger
-                  . toInteger
-                  . fromMaybe (evalError "expected uint8" v)
-                  . uint8FromNode
-                  $ v
+             in if
+                    | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                        mkBuiltinApp' OpUInt8ToInt [v]
+                    | otherwise ->
+                        nodeFromInteger
+                          . toInteger
+                          . fromMaybe (evalError "expected uint8" v)
+                          . uint8FromNode
+                          $ v
         {-# INLINE uint8ToIntOp #-}
 
         byteArrayFromListByteOp :: [Node] -> Node
         byteArrayFromListByteOp =
           unary $ \node ->
             let !v = eval' env node
-             in nodeFromByteString
-                  . BS.pack
-                  . fromMaybe (evalError "expected list byte" v)
-                  . listUInt8FromNode
-                  $ v
+             in if
+                    | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                        mkBuiltinApp' OpByteArrayFromListByte [v]
+                    | otherwise ->
+                        nodeFromByteString
+                          . BS.pack
+                          . fromMaybe (evalError "expected list byte" v)
+                          . listUInt8FromNode
+                          $ v
         {-# INLINE byteArrayFromListByteOp #-}
 
         byteArrayLengthOp :: [Node] -> Node
         byteArrayLengthOp =
           unary $ \node ->
             let !v = eval' env node
-             in nodeFromInteger
-                  . fromIntegral
-                  . BS.length
-                  . fromMaybe (evalError "expected bytearray" v)
-                  . byteArrayFromNode
-                  $ v
+             in if
+                    | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                        mkBuiltinApp' OpByteArrayLength [v]
+                    | otherwise ->
+                        nodeFromInteger
+                          . fromIntegral
+                          . BS.length
+                          . fromMaybe (evalError "ByteArrayLengthOp expected bytestring" v)
+                          . byteStringFromNode
+                          $ v
         {-# INLINE byteArrayLengthOp #-}
 
     {-# INLINE applyBuiltin #-}
 
-    -- secretKey, publicKey are not encoded with their length as
-    -- a bytestring in order to be compatible with Anoma sign. Therefore the
-    -- expected length of each must be specified.
-    secretKeyFromInteger :: Integer -> E.SecretKey
-    secretKeyFromInteger = E.SecretKey . Encoding.integerToByteStringLELen 64
-    {-# INLINE secretKeyFromInteger #-}
-
-    publicKeyFromInteger :: Integer -> E.PublicKey
-    publicKeyFromInteger = E.PublicKey . Encoding.integerToByteStringLELen 32
-    {-# INLINE publicKeyFromInteger #-}
-
     nodeFromInteger :: Integer -> Node
     nodeFromInteger !int = mkConstant' (ConstInteger int)
     {-# INLINE nodeFromInteger #-}
@@ -642,11 +646,11 @@ geval opts herr tab env0 = eval' env0
       _ -> Nothing
     {-# INLINE uint8FromNode #-}
 
-    byteArrayFromNode :: Node -> Maybe ByteString
-    byteArrayFromNode = \case
+    byteStringFromNode :: Node -> Maybe ByteString
+    byteStringFromNode = \case
       NCst (Constant _ (ConstByteArray b)) -> Just b
       _ -> Nothing
-    {-# INLINE byteArrayFromNode #-}
+    {-# INLINE byteStringFromNode #-}
 
     listUInt8FromNode :: Node -> Maybe [Word8]
     listUInt8FromNode = \case

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

@@ -3,7 +3,16 @@ module Juvix.Compiler.Nockma.Encoding.Ed25519 where
 import Data.ByteString qualified as BS
 import Juvix.Prelude.Base
 
+signatureLength :: Int
+signatureLength = 64
+
+publicKeyLength :: Int
+publicKeyLength = 32
+
+privateKeyLength :: Int
+privateKeyLength = 64
+
 -- | 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
+removeSignature = BS.drop signatureLength

src/Juvix/Compiler/Nockma/Evaluator.hs

@@ -259,6 +259,9 @@ evalProfile inistack initerm =
               let xs = checkTermToList args'
               let len = integerToNatural (toInteger (length xs))
               TermAtom . mkEmptyAtom <$> fromNatural len
+            StdlibLengthBytes -> case args' of
+              TermAtom a -> TermAtom <$> goLengthBytes a
+              _ -> error "expected an atom"
           where
             goCat :: Atom a -> Atom a -> Sem r (Term a)
             goCat arg1 arg2 = TermAtom . setAtomHint AtomHintString <$> atomConcatenateBytes arg1 arg2
@@ -268,6 +271,11 @@ evalProfile inistack initerm =
               bs <- mapM nockNatural (checkTermToListAtom c)
               byteStringToAtom (BS.pack (fromIntegral <$> bs))
 
+            goLengthBytes :: Atom a -> Sem r (Atom a)
+            goLengthBytes x = do
+              bs <- atomToByteString x
+              return (mkEmptyAtom (fromIntegral (BS.length bs)))
+
             checkTermToList :: Term a -> [Term a]
             checkTermToList = \case
               TermAtom x ->
@@ -284,15 +292,6 @@ evalProfile inistack initerm =
                   TermAtom x -> x
                   TermCell {} -> error "expect list element to be an atom"
 
-            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 <$> atomToByteStringLen signatureLength sigT

src/Juvix/Compiler/Nockma/StdlibFunction.hs

@@ -29,6 +29,13 @@ stdlibPath = \case
   StdlibLengthList -> [nock| [9 1.406 0 31] |]
   -- Obtained from the urbit dojo using:
   --
+  -- =>  anoma  !=(~(met block 3))
+  --
+  -- The `3` here is because we want to treat each atom as sequences of 2^3
+  -- bits, i.e bytes.
+  StdlibLengthBytes -> [nock| [8 [9 10 0 7] 9 190 10 [6 7 [0 3] 1 3] 0 2] |]
+  -- Obtained from the urbit dojo using:
+  --
   -- =>  anoma  !=(~(cat block 3))
   --
   -- The `3` here is because we want to treat each atom as sequences of 2^3

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

@@ -23,6 +23,7 @@ instance Pretty StdlibFunction where
     StdlibCatBytes -> "cat"
     StdlibFoldBytes -> "fold-bytes"
     StdlibLengthList -> "length-list"
+    StdlibLengthBytes -> "length-bytes"
 
 data StdlibFunction
   = StdlibDec
@@ -43,6 +44,7 @@ data StdlibFunction
   | StdlibCatBytes
   | StdlibFoldBytes
   | StdlibLengthList
+  | StdlibLengthBytes
   deriving stock (Show, Lift, Eq, Bounded, Enum, Generic)
 
 instance Hashable StdlibFunction