Add builtin ByteArray type (#2933)

This PR adds support for a builtin `ByteArray` type and associated
functions for constructing a `ByteArray` from a list of bytes and a
function to query the size of the `ByteArray`. It is only available in
the Anoma backend.

In Core / Tree, ByteArray constant is stored using a Haskell ByteString.

In Anoma the ByteArray is stored as a cell where the head is the length
of the ByteArray and the tail is an integer is an integer formed by
concatenating the bytes in the array using little-endian byte ordering.

The Nock for constructing a `ByteArray` uses the `length`, `add`,
`folder` and `lsh` functions from the Anoma hoon stdlib. See the [code
comment](https://github.com/anoma/juvix/blob/fa068a30e749f34b2c78451378869df7622ea9fe/src/Juvix/Compiler/Nockma/StdlibFunction.hs#L37)
for more details.

Example:

```
module test082;

import Stdlib.Prelude open;
import Stdlib.Debug.Trace open;

builtin bytearray
axiom ByteArray : Type;

builtin bytearray-from-list-byte
axiom mkByteArray : List Byte -> ByteArray;

builtin bytearray-size
axiom size : ByteArray -> Nat;

bs0 : ByteArray := mkByteArray [];

bs1 : ByteArray := mkByteArray [0x0; 0x0; 0x0];

bs2 : ByteArray := mkByteArray [0x1; 0x0; 0x0; 0x0];

bs3 : ByteArray := mkByteArray [0x2; 0x1];

bs4 : ByteArray := mkByteArray [0x100];

main : ByteArray :=
  trace (size bs0)
   >-> trace bs0
   >-> trace (size bs1)
    >-> trace bs1
    >-> trace (size bs2)
    >-> trace bs2
    >-> trace (size bs3)
    >-> trace bs3
    >-> trace (size bs4)
    >-> bs4;
```

Output using `tests/Anoma/Compilation/positive/test082.juvix`

```
$ juvix compile anoma -g test082.juvix
$ juvix dev nockma run test082.pretty.nockma
0
[0 0]
3
[3 0]
4
[4 1]
2
[2 258]
1
[1 0]
```

src/Juvix/Compiler/Asm/Extra/Memory.hs

@@ -110,6 +110,7 @@ getConstantType = \case
   ConstUnit -> TyUnit
   ConstVoid -> TyVoid
   ConstUInt8 {} -> mkTypeUInt8
+  ConstByteArray {} -> TyByteArray
 
 getValueType' :: (Member (Error AsmError) r) => Maybe Location -> InfoTable -> Memory -> Value -> Sem r Type
 getValueType' loc tab mem = \case

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

@@ -39,6 +39,7 @@ genCode fi =
       Tree.Binop x -> goBinop isTail x
       Tree.Unop x -> goUnop isTail x
       Tree.Cairo x -> goCairo isTail x
+      Tree.ByteArray {} -> error "ByteArray instructions are not supported in the Asm backend"
       Tree.Anoma {} -> error "Anoma instructions are not supported in the Asm backend"
       Tree.Constant x -> goConstant isTail x
       Tree.MemRef x -> goMemRef isTail x

src/Juvix/Compiler/Backend/C/Translation/FromReg.hs

@@ -350,6 +350,7 @@ fromRegInstr bNoStack info = \case
       Reg.ConstUnit -> macroVar "OBJ_UNIT"
       Reg.ConstVoid -> macroVar "OBJ_VOID"
       Reg.ConstUInt8 x -> macroCall "make_smallint" [integer x]
+      Reg.ConstByteArray {} -> impossible
 
     fromPrealloc :: Reg.InstrPrealloc -> Statement
     fromPrealloc Reg.InstrPrealloc {..} =

src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs

@@ -251,6 +251,7 @@ fromRegInstr info = \case
       Reg.ConstUnit -> mkVar "OBJ_UNIT"
       Reg.ConstVoid -> mkVar "OBJ_VOID"
       Reg.ConstUInt8 x -> mkCall "make_smallint" [mkInteger x]
+      Reg.ConstByteArray {} -> impossible
 
     fromAlloc :: Reg.InstrAlloc -> [Statement]
     fromAlloc Reg.InstrAlloc {..} =

src/Juvix/Compiler/Builtins.hs

@@ -13,12 +13,14 @@ module Juvix.Compiler.Builtins
     module Juvix.Compiler.Builtins.Anoma,
     module Juvix.Compiler.Builtins.Cairo,
     module Juvix.Compiler.Builtins.Byte,
+    module Juvix.Compiler.Builtins.ByteArray,
   )
 where
 
 import Juvix.Compiler.Builtins.Anoma
 import Juvix.Compiler.Builtins.Bool
 import Juvix.Compiler.Builtins.Byte
+import Juvix.Compiler.Builtins.ByteArray
 import Juvix.Compiler.Builtins.Cairo
 import Juvix.Compiler.Builtins.Control
 import Juvix.Compiler.Builtins.Debug

src/Juvix/Compiler/Builtins/ByteArray.hs

@@ -0,0 +1,27 @@
+module Juvix.Compiler.Builtins.ByteArray where
+
+import Juvix.Compiler.Builtins.Effect
+import Juvix.Compiler.Internal.Extra
+import Juvix.Prelude
+
+registerByteArray :: (Member Builtins r) => AxiomDef -> Sem r ()
+registerByteArray d = do
+  unless (isSmallUniverse' (d ^. axiomType)) (error "ByteArray should be in the small universe")
+  registerBuiltin BuiltinByteArray (d ^. axiomName)
+
+registerByteArrayFromListByte :: (Member Builtins r) => AxiomDef -> Sem r ()
+registerByteArrayFromListByte d = do
+  let loc = getLoc d
+  byte_ <- getBuiltinName loc BuiltinByte
+  list_ <- getBuiltinName loc BuiltinList
+  byteArray <- getBuiltinName loc BuiltinByteArray
+  unless (d ^. axiomType == (list_ @@ byte_ --> byteArray)) (error "bytearray-from-list-byte has the wrong type")
+  registerBuiltin BuiltinByteArrayFromListByte (d ^. axiomName)
+
+registerByteArrayLength :: (Member Builtins r) => AxiomDef -> Sem r ()
+registerByteArrayLength d = do
+  let loc = getLoc d
+  byteArray <- getBuiltinName loc BuiltinByteArray
+  nat_ <- getBuiltinName loc BuiltinNat
+  unless (d ^. axiomType == (byteArray --> nat_)) (error "bytearray-length has the wrong type")
+  registerBuiltin BuiltinByteArrayLength (d ^. axiomName)

src/Juvix/Compiler/Casm/Translation/FromReg.hs

@@ -250,6 +250,7 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI
           Reg.ConstVoid -> 0
           Reg.ConstString {} -> unsupported "strings"
           Reg.ConstUInt8 {} -> unsupported "uint8"
+          Reg.ConstByteArray {} -> unsupported "bytearray"
 
         mkLoad :: Reg.ConstrField -> Sem r RValue
         mkLoad Reg.ConstrField {..} = do

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

@@ -222,6 +222,9 @@ data BuiltinAxiom
   | BuiltinByteEq
   | BuiltinByteToNat
   | BuiltinByteFromNat
+  | BuiltinByteArray
+  | BuiltinByteArrayFromListByte
+  | BuiltinByteArrayLength
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
 
 instance HasNameKind BuiltinAxiom where
@@ -263,7 +266,9 @@ instance HasNameKind BuiltinAxiom where
     BuiltinByteEq -> KNameFunction
     BuiltinByteToNat -> KNameFunction
     BuiltinByteFromNat -> KNameFunction
-
+    BuiltinByteArray -> KNameInductive
+    BuiltinByteArrayFromListByte -> KNameFunction
+    BuiltinByteArrayLength -> KNameFunction
   getNameKindPretty :: BuiltinAxiom -> NameKind
   getNameKindPretty = getNameKind
 
@@ -312,6 +317,9 @@ instance Pretty BuiltinAxiom where
     BuiltinByteEq -> Str.byteEq
     BuiltinByteToNat -> Str.byteToNat
     BuiltinByteFromNat -> Str.byteFromNat
+    BuiltinByteArray -> Str.byteArray
+    BuiltinByteArrayFromListByte -> Str.byteArrayFromListByte
+    BuiltinByteArrayLength -> Str.byteArrayLength
 
 data BuiltinType
   = BuiltinTypeInductive BuiltinInductive

src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs

@@ -288,6 +288,17 @@ declareMaybeBuiltins = do
       (tagJust, "just", mkPi' mkDynamic', Just BuiltinMaybeJust)
     ]
 
+declareListBuiltins :: (Member InfoTableBuilder r) => Sem r ()
+declareListBuiltins = do
+  tagNil <- freshTag
+  tagCons <- freshTag
+  declareInductiveBuiltins
+    "BuiltinList"
+    (Just (BuiltinTypeInductive BuiltinList))
+    [ (tagNil, "builtinListNil", mkPis' [mkSmallUniv], Just BuiltinListNil),
+      (tagCons, "builtinListCons", \x -> mkPis' [mkSmallUniv, mkDynamic', x] x, Just BuiltinListCons)
+    ]
+
 reserveLiteralIntToNatSymbol :: (Member InfoTableBuilder r) => Sem r ()
 reserveLiteralIntToNatSymbol = do
   sym <- freshSymbol

src/Juvix/Compiler/Core/Evaluator.hs

@@ -2,6 +2,7 @@ module Juvix.Compiler.Core.Evaluator where
 
 import Control.Exception qualified as Exception
 import Crypto.Sign.Ed25519 qualified as E
+import Data.ByteString qualified as BS
 import Data.HashMap.Strict qualified as HashMap
 import Data.Serialize qualified as S
 import GHC.Base (seq)
@@ -215,6 +216,8 @@ geval opts herr tab env0 = eval' env0
       OpRandomEcPoint -> randomEcPointOp
       OpUInt8ToInt -> uint8ToIntOp
       OpUInt8FromInt -> uint8FromIntOp
+      OpByteArrayFromListByte -> byteArrayFromListByteOp
+      OpByteArrayLength -> byteArrayLengthOp
       where
         err :: Text -> a
         err msg = evalError msg n
@@ -533,6 +536,30 @@ geval opts herr tab env0 = eval' env0
                   . 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
+        {-# 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
+        {-# INLINE byteArrayLengthOp #-}
+
     {-# INLINE applyBuiltin #-}
 
     -- secretKey, publicKey are not encoded with their length as
@@ -558,6 +585,10 @@ geval opts herr tab env0 = eval' env0
     nodeFromUInt8 !w = mkConstant' (ConstUInt8 w)
     {-# INLINE nodeFromUInt8 #-}
 
+    nodeFromByteString :: ByteString -> Node
+    nodeFromByteString !b = mkConstant' (ConstByteArray b)
+    {-# INLINE nodeFromByteString #-}
+
     nodeFromBool :: Bool -> Node
     nodeFromBool b = mkConstr' (BuiltinTag tag) []
       where
@@ -567,10 +598,10 @@ geval opts herr tab env0 = eval' env0
     {-# INLINE nodeFromBool #-}
 
     mkBuiltinConstructor :: BuiltinConstructor -> [Node] -> Maybe Node
-    mkBuiltinConstructor ctor args =
-      (\tag -> mkConstr' tag args)
-        . (^. constructorTag)
-        <$> lookupTabBuiltinConstructor tab ctor
+    mkBuiltinConstructor ctor args = (\tag -> mkConstr' tag args) <$> builtinConstructorTag ctor
+
+    builtinConstructorTag :: BuiltinConstructor -> Maybe Tag
+    builtinConstructorTag ctor = (^. constructorTag) <$> lookupTabBuiltinConstructor tab ctor
 
     nodeMaybeNothing :: Node
     nodeMaybeNothing =
@@ -611,6 +642,29 @@ geval opts herr tab env0 = eval' env0
       _ -> Nothing
     {-# INLINE uint8FromNode #-}
 
+    byteArrayFromNode :: Node -> Maybe ByteString
+    byteArrayFromNode = \case
+      NCst (Constant _ (ConstByteArray b)) -> Just b
+      _ -> Nothing
+    {-# INLINE byteArrayFromNode #-}
+
+    listUInt8FromNode :: Node -> Maybe [Word8]
+    listUInt8FromNode = \case
+      NCtr (Constr _ t xs) -> do
+        consTag <- builtinConstructorTag BuiltinListCons
+        nilTag <- builtinConstructorTag BuiltinListNil
+        if
+            | t == nilTag -> return []
+            | t == consTag -> case (filter (not . isType') xs) of
+                (hd : tl) -> do
+                  uint8Hd <- uint8FromNode hd
+                  uint8Tl <- concatMapM listUInt8FromNode tl
+                  return (uint8Hd : uint8Tl)
+                _ -> Nothing
+            | otherwise -> Nothing
+      _ -> Nothing
+    {-# INLINE listUInt8FromNode #-}
+
     printNode :: Node -> Text
     printNode = \case
       NCst (Constant _ (ConstString s)) -> s

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

@@ -200,6 +200,12 @@ mkTypeUInt8 i = mkTypePrim i primitiveUInt8
 mkTypeUInt8' :: Type
 mkTypeUInt8' = mkTypeUInt8 Info.empty
 
+mkTypeByteArray :: Info -> Type
+mkTypeByteArray i = mkTypePrim i PrimByteArray
+
+mkTypeByteArray' :: Type
+mkTypeByteArray' = mkTypeByteArray Info.empty
+
 mkDynamic :: Info -> Type
 mkDynamic i = NDyn (DynamicTy i)
 

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

@@ -435,6 +435,8 @@ builtinOpArgTypes = \case
   OpRandomEcPoint -> []
   OpUInt8ToInt -> [mkTypeUInt8']
   OpUInt8FromInt -> [mkTypeInteger']
+  OpByteArrayFromListByte -> [mkDynamic']
+  OpByteArrayLength -> [mkTypeByteArray']
 
 translateCase :: (Node -> Node -> Node -> a) -> a -> Case -> a
 translateCase translateIfFun dflt Case {..} = case _caseBranches of

src/Juvix/Compiler/Core/Keywords.hs

@@ -19,6 +19,8 @@ import Juvix.Data.Keyword.All
     kwBind,
     kwBottom,
     kwBuiltin,
+    kwByteArrayFromListByte,
+    kwByteArrayLength,
     kwCase,
     kwColon,
     kwComma,

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

@@ -38,6 +38,8 @@ data BuiltinOp
   | OpRandomEcPoint
   | OpUInt8ToInt
   | OpUInt8FromInt
+  | OpByteArrayFromListByte
+  | OpByteArrayLength
   deriving stock (Eq, Generic)
 
 instance Serialize BuiltinOp
@@ -94,6 +96,8 @@ builtinOpArgsNum = \case
   OpRandomEcPoint -> 0
   OpUInt8ToInt -> 1
   OpUInt8FromInt -> 1
+  OpByteArrayFromListByte -> 1
+  OpByteArrayLength -> 1
 
 builtinConstrArgsNum :: BuiltinDataTag -> Int
 builtinConstrArgsNum = \case
@@ -139,13 +143,18 @@ builtinIsFoldable = \case
   OpRandomEcPoint -> False
   OpUInt8ToInt -> True
   OpUInt8FromInt -> True
+  OpByteArrayFromListByte -> False
+  OpByteArrayLength -> False
 
 builtinIsCairo :: BuiltinOp -> Bool
 builtinIsCairo op = op `elem` builtinsCairo
 
 builtinIsAnoma :: BuiltinOp -> Bool
 builtinIsAnoma op = op `elem` builtinsAnoma
 
+builtinIsByteArray :: BuiltinOp -> Bool
+builtinIsByteArray op = op `elem` builtinsByteArray
+
 builtinsString :: [BuiltinOp]
 builtinsString = [OpStrConcat, OpStrToInt, OpShow]
 
@@ -165,3 +174,6 @@ builtinsAnoma =
 
 builtinsUInt8 :: [BuiltinOp]
 builtinsUInt8 = [OpUInt8FromInt, OpUInt8ToInt]
+
+builtinsByteArray :: [BuiltinOp]
+builtinsByteArray = [OpByteArrayFromListByte, OpByteArrayLength]

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

@@ -39,6 +39,7 @@ data ConstantValue
   | ConstField !FField
   | ConstString !Text
   | ConstUInt8 !Word8
+  | ConstByteArray !ByteString
   deriving stock (Eq, Generic)
 
 -- | Info about a single binder. Associated with Lambda, Pi, Let, Case or Match.

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

@@ -15,6 +15,7 @@ data Primitive
   | PrimBool PrimBoolInfo
   | PrimString
   | PrimField
+  | PrimByteArray
   deriving stock (Eq, Generic)
 
 primitiveUInt8 :: Primitive