Add frontend support for Anoma stdlib sha256 (#3109)

This PR adds frontend support for Anoma stdlib sha256 function (aka
`shax` in Nock).

* Closes #2901

The new builtin can be declared as follows:

```
builtin anoma-sha256
axiom anomaSha256 : Nat -> ByteArray;
```

The intention is that it wraps a call to anomaEncode as follows:

```
sha256 {A} (a : A) : ByteArray := anomaSha256 (anomaEncode a);
```

### Fix for atom to ByteString

This PR also includes a commit
6205dc9
to fix an issue with functions like `integerToByteArray` when called
with negative integers (the solution is to change the argument types to
Natural, as this is all we need for Anoma).

src/Juvix/Compiler/Builtins/Anoma.hs

@@ -107,3 +107,13 @@ checkAnomaByteArrayFromAnomaContents f = do
   unless
     (ftype == (nat_ --> nat_ --> byteArray))
     $ builtinsErrorText l "fromAnomaContents must be of type Nat -> Nat -> ByteArray"
+
+checkAnomaSha256 :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkAnomaSha256 f = do
+  let ftype = f ^. axiomType
+      l = getLoc f
+  byteArray <- getBuiltinNameScoper l BuiltinByteArray
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless
+    (ftype == (nat_ --> byteArray))
+    $ builtinsErrorText l "anomaSha256 must be of type Nat -> ByteArray"

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

@@ -227,6 +227,7 @@ data BuiltinAxiom
   | BuiltinAnomaVerifyWithMessage
   | BuiltinAnomaByteArrayToAnomaContents
   | BuiltinAnomaByteArrayFromAnomaContents
+  | BuiltinAnomaSha256
   | BuiltinPoseidon
   | BuiltinEcOp
   | BuiltinRandomEcPoint
@@ -273,6 +274,7 @@ instance HasNameKind BuiltinAxiom where
     BuiltinAnomaVerifyWithMessage -> KNameFunction
     BuiltinAnomaByteArrayToAnomaContents -> KNameFunction
     BuiltinAnomaByteArrayFromAnomaContents -> KNameFunction
+    BuiltinAnomaSha256 -> KNameFunction
     BuiltinPoseidon -> KNameFunction
     BuiltinEcOp -> KNameFunction
     BuiltinRandomEcPoint -> KNameFunction
@@ -326,6 +328,7 @@ instance Pretty BuiltinAxiom where
     BuiltinAnomaVerifyWithMessage -> Str.anomaVerifyWithMessage
     BuiltinAnomaByteArrayToAnomaContents -> Str.anomaByteArrayToAnomaContents
     BuiltinAnomaByteArrayFromAnomaContents -> Str.anomaByteArrayFromAnomaContents
+    BuiltinAnomaSha256 -> Str.anomaSha256
     BuiltinPoseidon -> Str.cairoPoseidon
     BuiltinEcOp -> Str.cairoEcOp
     BuiltinRandomEcPoint -> Str.cairoRandomEcPoint

src/Juvix/Compiler/Core/Evaluator.hs

@@ -16,7 +16,7 @@ import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Info.NoDisplayInfo
 import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Nockma.Encoding qualified as Encoding
-import Juvix.Compiler.Nockma.Encoding.ByteString (byteStringToIntegerLE, integerToByteStringLELen)
+import Juvix.Compiler.Nockma.Encoding.ByteString (byteStringToIntegerLE, naturalToByteStringLELen)
 import Juvix.Compiler.Nockma.Encoding.Ed25519 qualified as E
 import Juvix.Compiler.Store.Core.Extra qualified as Store
 import Juvix.Data.Field
@@ -227,6 +227,7 @@ geval opts herr tab env0 = eval' env0
       OpAnomaVerifyWithMessage -> anomaVerifyWithMessageOp
       OpAnomaByteArrayToAnomaContents -> anomaByteArrayToAnomaContents
       OpAnomaByteArrayFromAnomaContents -> anomaByteArrayFromAnomaContents
+      OpAnomaSha256 -> anomaSha256
       OpPoseidonHash -> poseidonHashOp
       OpEc -> ecOp
       OpRandomEcPoint -> randomEcPointOp
@@ -484,10 +485,22 @@ geval opts herr tab env0 = eval' env0
                       mkBuiltinApp' OpAnomaByteArrayFromAnomaContents [v1, v2]
                   | otherwise ->
                       case (integerFromNode v1, integerFromNode v2) of
-                        (Just i1, Just i2) -> nodeFromByteString (integerToByteStringLELen (fromIntegral i1) i2)
+                        (Just i1, Just i2) -> nodeFromByteString (naturalToByteStringLELen (fromIntegral i1) (fromIntegral i2))
                         _ -> err "anomaByteArrayFromAnomaContents: expected both argmuments to be integers"
         {-# INLINE anomaByteArrayFromAnomaContents #-}
 
+        anomaSha256 :: [Node] -> Node
+        anomaSha256 = checkApply $ \arg ->
+          let !v = eval' env arg
+           in if
+                  | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                      mkBuiltinApp' OpAnomaSha256 [v]
+                  | otherwise ->
+                      case integerFromNode v of
+                        Just i -> nodeFromByteString (Encoding.sha256Natural (fromIntegral i))
+                        _ -> err "anomaSha256: expected 1 integer argument"
+        {-# INLINE anomaSha256 #-}
+
         poseidonHashOp :: [Node] -> Node
         poseidonHashOp = unary $ \arg ->
           if

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

@@ -185,6 +185,7 @@ isDebugOp = \case
       OpFail -> True
       OpSeq -> True
       OpAssert -> True
+      OpAnomaSha256 -> False
       OpAnomaByteArrayFromAnomaContents -> False
       OpAnomaByteArrayToAnomaContents -> False
       OpAnomaDecode -> False
@@ -480,6 +481,7 @@ builtinOpArgTypes = \case
   OpAnomaVerifyWithMessage -> [mkDynamic', mkDynamic']
   OpAnomaByteArrayToAnomaContents -> [mkDynamic']
   OpAnomaByteArrayFromAnomaContents -> [mkTypeInteger', mkTypeInteger']
+  OpAnomaSha256 -> [mkTypeInteger']
   OpPoseidonHash -> [mkDynamic']
   OpEc -> [mkDynamic', mkTypeField', mkDynamic']
   OpRandomEcPoint -> []

src/Juvix/Compiler/Core/Keywords.hs

@@ -10,6 +10,7 @@ import Juvix.Data.Keyword.All
   ( delimSemicolon,
     kwAnomaDecode,
     kwAnomaEncode,
+    kwAnomaSha256,
     kwAnomaSign,
     kwAnomaSignDetached,
     kwAnomaVerifyDetached,

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

@@ -39,6 +39,7 @@ data BuiltinOp
   | OpAnomaVerifyWithMessage
   | OpAnomaByteArrayToAnomaContents
   | OpAnomaByteArrayFromAnomaContents
+  | OpAnomaSha256
   | OpPoseidonHash
   | OpEc
   | OpRandomEcPoint
@@ -112,6 +113,7 @@ builtinOpArgsNum = \case
   OpAnomaVerifyWithMessage -> 2
   OpAnomaByteArrayToAnomaContents -> 1
   OpAnomaByteArrayFromAnomaContents -> 2
+  OpAnomaSha256 -> 1
   OpPoseidonHash -> 1
   OpEc -> 3
   OpRandomEcPoint -> 0
@@ -162,6 +164,7 @@ builtinIsFoldable = \case
   OpAnomaVerifyWithMessage -> False
   OpAnomaByteArrayToAnomaContents -> False
   OpAnomaByteArrayFromAnomaContents -> False
+  OpAnomaSha256 -> False
   OpPoseidonHash -> False
   OpEc -> False
   OpRandomEcPoint -> False
@@ -195,7 +198,8 @@ builtinsAnoma =
     OpAnomaVerifyWithMessage,
     OpAnomaSignDetached,
     OpAnomaByteArrayToAnomaContents,
-    OpAnomaByteArrayFromAnomaContents
+    OpAnomaByteArrayFromAnomaContents,
+    OpAnomaSha256
   ]
 
 builtinsUInt8 :: [BuiltinOp]

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

@@ -63,6 +63,7 @@ instance PrettyCode BuiltinOp where
     OpAnomaVerifyWithMessage -> return primAnomaVerifyWithMessage
     OpAnomaByteArrayToAnomaContents -> return primAnomaByteArrayToAnomaContents
     OpAnomaByteArrayFromAnomaContents -> return primAnomaByteArrayFromAnomaContents
+    OpAnomaSha256 -> return primAnomaSha256
     OpPoseidonHash -> return primPoseidonHash
     OpEc -> return primEc
     OpRandomEcPoint -> return primRandomEcPoint
@@ -904,6 +905,9 @@ primAnomaByteArrayToAnomaContents = primitive Str.anomaByteArrayToAnomaContents
 primAnomaByteArrayFromAnomaContents :: Doc Ann
 primAnomaByteArrayFromAnomaContents = primitive Str.anomaByteArrayFromAnomaContents
 
+primAnomaSha256 :: Doc Ann
+primAnomaSha256 = primitive Str.anomaSha256
+
 primPoseidonHash :: Doc Ann
 primPoseidonHash = primitive Str.cairoPoseidon
 

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

@@ -80,6 +80,7 @@ computeNodeTypeInfo md = umapL go
           OpAnomaVerifyWithMessage -> Info.getNodeType node
           OpAnomaByteArrayFromAnomaContents -> Info.getNodeType node
           OpAnomaByteArrayToAnomaContents -> mkTypeInteger'
+          OpAnomaSha256 -> mkTypeByteArray'
           OpPoseidonHash -> case _builtinAppArgs of
             [arg] -> Info.getNodeType arg
             _ -> error "incorrect poseidon builtin application"

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

@@ -644,8 +644,9 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinAnomaSign -> return ()
       Internal.BuiltinAnomaSignDetached -> return ()
       Internal.BuiltinAnomaVerifyWithMessage -> return ()
-      BuiltinAnomaByteArrayToAnomaContents -> return ()
-      BuiltinAnomaByteArrayFromAnomaContents -> return ()
+      Internal.BuiltinAnomaByteArrayToAnomaContents -> return ()
+      Internal.BuiltinAnomaByteArrayFromAnomaContents -> return ()
+      Internal.BuiltinAnomaSha256 -> return ()
       Internal.BuiltinPoseidon -> return ()
       Internal.BuiltinEcOp -> return ()
       Internal.BuiltinRandomEcPoint -> return ()
@@ -853,6 +854,13 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
                   (mkBuiltinApp' OpAnomaByteArrayFromAnomaContents [mkVar' 1, mkVar' 0])
               )
           )
+      Internal.BuiltinAnomaSha256 -> do
+        natType <- getNatType
+        registerAxiomDef
+          ( mkLambda'
+              natType
+              (mkBuiltinApp' OpAnomaSha256 [mkVar' 0])
+          )
       Internal.BuiltinPoseidon -> do
         psName <- getPoseidonStateName
         psSym <- getPoseidonStateSymbol
@@ -1276,6 +1284,7 @@ goApplication a = do
         Just Internal.BuiltinAnomaVerifyWithMessage -> app
         Just Internal.BuiltinAnomaByteArrayToAnomaContents -> app
         Just Internal.BuiltinAnomaByteArrayFromAnomaContents -> app
+        Just Internal.BuiltinAnomaSha256 -> app
         Just Internal.BuiltinPoseidon -> app
         Just Internal.BuiltinEcOp -> app
         Just Internal.BuiltinRandomEcPoint -> app

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

@@ -584,6 +584,7 @@ builtinAppExpr varsNum vars = do
       <|> (kw kwAnomaVerifyDetached $> OpAnomaVerifyDetached)
       <|> (kw kwByteArrayFromListByte $> OpByteArrayFromListByte)
       <|> (kw kwByteArrayLength $> OpByteArrayLength)
+      <|> (kw kwAnomaSha256 $> OpAnomaSha256)
   args <- P.many (atom varsNum vars)
   return $ mkBuiltinApp' op args
 

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

@@ -109,6 +109,7 @@ fromCore fsize tab =
         BuiltinAnomaVerifyWithMessage -> False
         BuiltinAnomaByteArrayToAnomaContents -> False
         BuiltinAnomaByteArrayFromAnomaContents -> False
+        BuiltinAnomaSha256 -> False
         BuiltinPoseidon -> False
         BuiltinEcOp -> False
         BuiltinRandomEcPoint -> False

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

@@ -600,6 +600,7 @@ checkBuiltinAxiom d b = localBuiltins $ case b of
   BuiltinAnomaVerifyWithMessage -> checkAnomaVerifyWithMessage d
   BuiltinAnomaByteArrayFromAnomaContents -> checkAnomaByteArrayFromAnomaContents d
   BuiltinAnomaByteArrayToAnomaContents -> checkAnomaByteArrayToAnomaContents d
+  BuiltinAnomaSha256 -> checkAnomaSha256 d
   BuiltinPoseidon -> checkPoseidon d
   BuiltinEcOp -> checkEcOp d
   BuiltinRandomEcPoint -> checkRandomEcPoint d

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

@@ -1,9 +1,11 @@
 module Juvix.Compiler.Nockma.Encoding.ByteString where
 
+import Crypto.Hash.SHA256 qualified as SHA256
 import Data.Bit (Bit)
 import Data.Bit qualified as Bit
 import Data.Bits
 import Data.ByteString qualified as BS
+import Data.ByteString.Base16 qualified as Base16
 import Data.ByteString.Builder qualified as BS
 import Juvix.Compiler.Nockma.Encoding.Base
 import Juvix.Compiler.Nockma.Encoding.Effect.BitReader
@@ -19,14 +21,17 @@ atomToByteString = fmap naturalToByteString . nockNatural
 atomToByteStringLen :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => Int -> Atom a -> Sem r ByteString
 atomToByteStringLen len = fmap (padByteString len) . atomToByteString
 
+sha256Atom :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => Atom a -> Sem r ByteString
+sha256Atom = fmap sha256Natural . nockNatural
+
 byteStringToAtom :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => ByteString -> Sem r (Atom a)
 byteStringToAtom = fmap mkEmptyAtom . fromNatural . byteStringToNatural
 
 byteStringToNatural :: ByteString -> Natural
 byteStringToNatural = fromInteger . byteStringToIntegerLE
 
 naturalToByteString :: Natural -> ByteString
-naturalToByteString = integerToByteStringLE . toInteger
+naturalToByteString = naturalToByteStringLE
 
 byteStringToIntegerLE :: ByteString -> Integer
 byteStringToIntegerLE = BS.foldr (\b acc -> acc `shiftL` 8 .|. fromIntegral b) 0
@@ -50,16 +55,16 @@ byteStringToIntegerLEChunked = foldr' go 0 . map (first byteStringChunkToInteger
     byteStringChunkToInteger :: ByteString -> Integer
     byteStringChunkToInteger = BS.foldr' (\b acc -> acc `shiftL` 8 .|. fromIntegral b) 0
 
-integerToByteStringLE :: Integer -> ByteString
-integerToByteStringLE = BS.toStrict . BS.toLazyByteString . go
+naturalToByteStringLE :: Natural -> ByteString
+naturalToByteStringLE = BS.toStrict . BS.toLazyByteString . go
   where
-    go :: Integer -> BS.Builder
+    go :: Natural -> BS.Builder
     go = \case
       0 -> mempty
       n -> BS.word8 (fromIntegral n) <> go (n `shiftR` 8)
 
-integerToByteStringLELen :: Int -> Integer -> ByteString
-integerToByteStringLELen len = padByteString len . integerToByteStringLE
+naturalToByteStringLELen :: Int -> Natural -> ByteString
+naturalToByteStringLELen len = padByteString len . naturalToByteStringLE
 
 textToNatural :: Text -> Natural
 textToNatural = byteStringToNatural . encodeUtf8
@@ -113,3 +118,9 @@ decodeByteString i = evalBitReader (integerToVectorBits i) go
 -- | decode a ByteString that was encoded using `encodeByteString` with a default that's used if decoding fails.
 decodeByteStringWithDefault :: ByteString -> Integer -> ByteString
 decodeByteStringWithDefault d = fromRight d . run . runErrorNoCallStack @BitReadError . decodeByteString
+
+sha256Natural :: Natural -> ByteString
+sha256Natural =
+  Base16.encode
+    . SHA256.hash
+    . naturalToByteStringLE

src/Juvix/Compiler/Nockma/Evaluator.hs

@@ -268,10 +268,16 @@ evalProfile inistack initerm =
             -- Use the raw nock code for curry. The nock stdlib curry function is
             -- small. There's no benefit in implementing it separately in the evaluator.
             StdlibCurry -> nonInterceptCall
+            StdlibSha256 -> case args' of
+              TermAtom a -> TermAtom <$> goSha256 a
+              _ -> error "StdlibSha256 expects to be called with an atom"
           where
             goCat :: Atom a -> Atom a -> Sem r (Term a)
             goCat arg1 arg2 = TermAtom . setAtomHint AtomHintString <$> atomConcatenateBytes arg1 arg2
 
+            goSha256 :: Atom a -> Sem r (Atom a)
+            goSha256 a = Encoding.sha256Atom a >>= byteStringToAtom
+
             goFoldBytes :: Term a -> Sem r (Atom a)
             goFoldBytes c = do
               bs <- mapM nockNatural (checkTermToListAtom c)

src/Juvix/Compiler/Nockma/StdlibFunction.hs

@@ -32,6 +32,8 @@ stdlibPath = \case
   StdlibVerify -> [nock| [9 4 0 7] |]
   StdlibLengthList -> [nock| [9 1.406 0 127] |]
   StdlibCurry -> [nock| [9 4 0 127] |]
+  -- sha256 is called shax in hoon
+  StdlibSha256 -> [nock| [9 22 0 3] |]
   -- Obtained from the urbit dojo using:
   --
   -- =>  anoma  !=(~(met block 3))

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

@@ -25,6 +25,7 @@ instance Pretty StdlibFunction where
     StdlibLengthList -> "length-list"
     StdlibLengthBytes -> "length-bytes"
     StdlibCurry -> "curry"
+    StdlibSha256 -> "sha256"
 
 data StdlibFunction
   = StdlibDec
@@ -47,6 +48,7 @@ data StdlibFunction
   | StdlibLengthList
   | StdlibLengthBytes
   | StdlibCurry
+  | StdlibSha256
   deriving stock (Show, Lift, Eq, Bounded, Enum, Generic)
 
 instance Hashable StdlibFunction

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

@@ -566,6 +566,7 @@ compile = \case
         Tree.OpAnomaSignDetached -> goAnomaSignDetached args
         Tree.OpAnomaByteArrayFromAnomaContents -> return (goAnomaByteArrayFromAnomaContents args)
         Tree.OpAnomaByteArrayToAnomaContents -> return (goAnomaByteArrayToAnomaContents args)
+        Tree.OpAnomaSha256 -> goAnomaSha256 args
 
     goByteArrayOp :: Tree.NodeByteArray -> Sem r (Term Natural)
     goByteArrayOp Tree.NodeByteArray {..} = do
@@ -688,6 +689,14 @@ compile = \case
       [len, contents] -> mkByteArray len contents
       _ -> impossible
 
+    goAnomaSha256 :: [Term Natural] -> Sem r (Term Natural)
+    goAnomaSha256 arg = do
+      stdcall <- callStdlib StdlibSha256 arg
+      return $ mkByteArray (nockNatLiteral (integerToNatural sha256HashLength)) stdcall
+      where
+        sha256HashLength :: Integer
+        sha256HashLength = 64
+
     -- Conceptually this function is:
     -- anomaDecode <$> verify signedMessage pubKey
     --

src/Juvix/Compiler/Tree/Keywords.hs

@@ -14,6 +14,7 @@ import Juvix.Data.Keyword.All
     kwAnomaDecode,
     kwAnomaEncode,
     kwAnomaGet,
+    kwAnomaSha256,
     kwAnomaSign,
     kwAnomaSignDetached,
     kwAnomaVerifyDetached,

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

@@ -100,4 +100,6 @@ data AnomaOp
     OpAnomaByteArrayToAnomaContents
   | -- | Construct a ByteArray from the bytes of an Anoma atom with LSB ordering
     OpAnomaByteArrayFromAnomaContents
+  | -- | Hash a value using SHA256
+    OpAnomaSha256
   deriving stock (Eq)

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

@@ -286,6 +286,7 @@ instance PrettyCode AnomaOp where
     OpAnomaSignDetached -> Str.anomaSignDetached
     OpAnomaByteArrayFromAnomaContents -> Str.anomaByteArrayFromAnomaContents
     OpAnomaByteArrayToAnomaContents -> Str.anomaByteArrayToAnomaContents
+    OpAnomaSha256 -> Str.anomaSha256
 
 instance PrettyCode UnaryOpcode where
   ppCode = \case

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

@@ -20,6 +20,7 @@ checkNoAnoma = walkT checkNode
         OpAnomaVerifyWithMessage -> unsupportedErr "OpAnomaVerifyWithMessage"
         OpAnomaByteArrayFromAnomaContents -> unsupportedErr "OpAnomaByteArrayFromAnomaContents"
         OpAnomaByteArrayToAnomaContents -> unsupportedErr "OpAnomaByteArrayToAnomaContents"
+        OpAnomaSha256 -> unsupportedErr "OpAnomaSha256"
         where
           unsupportedErr :: Text -> Sem r ()
           unsupportedErr opName =

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

@@ -351,6 +351,7 @@ genCode infoTable fi =
       Core.OpAnomaVerifyWithMessage -> OpAnomaVerifyWithMessage
       Core.OpAnomaByteArrayToAnomaContents -> OpAnomaByteArrayToAnomaContents
       Core.OpAnomaByteArrayFromAnomaContents -> OpAnomaByteArrayFromAnomaContents
+      Core.OpAnomaSha256 -> OpAnomaSha256
       _ -> impossible
 
     getArgsNum :: Symbol -> Int

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

@@ -155,6 +155,7 @@ parseAnoma =
     <|> parseAnoma' kwAnomaVerifyWithMessage OpAnomaVerifyWithMessage
     <|> parseAnoma' kwAnomaByteArrayToAnomaContents OpAnomaByteArrayToAnomaContents
     <|> parseAnoma' kwAnomaByteArrayFromAnomaContents OpAnomaByteArrayFromAnomaContents
+    <|> parseAnoma' kwAnomaSha256 OpAnomaSha256
 
 parseAnoma' ::
   (Members '[Reader ParserSig, InfoTableBuilder, State LocalParams] r) =>