Add anoma-bytearray-{to, from}-anoma-contents builtins

The anoma-bytearray-{to, from}-anoma-contents are intended to be used
temporarily to convert to/from atoms representing ByteArrays.

We represent ByteArrays in nock as a cell:

```
[size contents]
```

Where `size` is the size of the ByteArray and `contents` is an Atom
representing the bytes in LSB ordering.

The `size` is required in general because the encoding of ByteArrays to
Atoms is ambiguous. For example the ByteArrays [0x01; 0x00] and [0x01]
are represente by `1`.

Some Anoma ByteArrays like keys and signatures are represented using on
the `contents` atom because the size is constant.

Users of Anoma APIs have to strip / add size information from ByteArrays
depending on where the data is used. The new builtins provide this facility.

These builtins are temporary because it's been agreed with Anoma
engineering team to change the Anoma APIs to make the ByteArray
representation uniform, i.e always represent ByteArrays using `[size
content]`. When this is implemented in Anoma Node we can remove these builtins.

```
builtin anoma-bytearray-to-anoma-contents
axiom toAnomaContents : ByteArray -> Nat;

builtin anoma-bytearray-from-anoma-contents
axiom fromAnomaContents :
  -- | The size of the ByteArray
  Nat
  -- | The contents of the ByteArray
  -> Nat
  -- | The resulting ByteArray
  -> ByteArray;
```

src/Juvix/Compiler/Builtins/Anoma.hs

@@ -97,3 +97,23 @@ registerAnomaSignDetached f = do
     ((ftype ==% (u <>--> dataT --> byteArray --> byteArray)) freeVars)
     (error "anomaSignDetached must be of type {A : Type} -> A -> ByteArray -> ByteArray")
   registerBuiltin BuiltinAnomaSignDetached (f ^. axiomName)
+
+registerByteArrayToAnomaContents :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
+registerByteArrayToAnomaContents f = do
+  let loc = getLoc f
+  byteArray <- getBuiltinName loc BuiltinByteArray
+  nat_ <- getBuiltinName loc BuiltinNat
+  unless
+    (f ^. axiomType == (byteArray --> nat_))
+    (error "toAnomaContents must be of type ByteArray -> Nat")
+  registerBuiltin BuiltinAnomaByteArrayToAnomaContents (f ^. axiomName)
+
+registerByteArrayFromAnomaContents :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
+registerByteArrayFromAnomaContents f = do
+  let loc = getLoc f
+  byteArray <- getBuiltinName loc BuiltinByteArray
+  nat_ <- getBuiltinName loc BuiltinNat
+  unless
+    (f ^. axiomType == (nat_ --> nat_ --> byteArray))
+    (error "fromAnomaContents must be of type Nat -> Nat -> ByteArray")
+  registerBuiltin BuiltinAnomaByteArrayFromAnomaContents (f ^. axiomName)

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

@@ -215,6 +215,8 @@ data BuiltinAxiom
   | BuiltinAnomaSign
   | BuiltinAnomaSignDetached
   | BuiltinAnomaVerifyWithMessage
+  | BuiltinAnomaByteArrayToAnomaContents
+  | BuiltinAnomaByteArrayFromAnomaContents
   | BuiltinPoseidon
   | BuiltinEcOp
   | BuiltinRandomEcPoint
@@ -259,6 +261,8 @@ instance HasNameKind BuiltinAxiom where
     BuiltinAnomaSign -> KNameFunction
     BuiltinAnomaSignDetached -> KNameFunction
     BuiltinAnomaVerifyWithMessage -> KNameFunction
+    BuiltinAnomaByteArrayToAnomaContents -> KNameFunction
+    BuiltinAnomaByteArrayFromAnomaContents -> KNameFunction
     BuiltinPoseidon -> KNameFunction
     BuiltinEcOp -> KNameFunction
     BuiltinRandomEcPoint -> KNameFunction
@@ -310,6 +314,8 @@ instance Pretty BuiltinAxiom where
     BuiltinAnomaSignDetached -> Str.anomaSignDetached
     BuiltinAnomaSign -> Str.anomaSign
     BuiltinAnomaVerifyWithMessage -> Str.anomaVerifyWithMessage
+    BuiltinAnomaByteArrayToAnomaContents -> Str.anomaByteArrayToAnomaContents
+    BuiltinAnomaByteArrayFromAnomaContents -> Str.anomaByteArrayFromAnomaContents
     BuiltinPoseidon -> Str.cairoPoseidon
     BuiltinEcOp -> Str.cairoEcOp
     BuiltinRandomEcPoint -> Str.cairoRandomEcPoint

src/Juvix/Compiler/Core/Evaluator.hs

@@ -16,6 +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.Ed25519 qualified as E
 import Juvix.Compiler.Store.Core.Extra qualified as Store
 import Juvix.Data.Field
@@ -211,6 +212,8 @@ geval opts herr tab env0 = eval' env0
       OpAnomaSign -> anomaSignOp
       OpAnomaSignDetached -> anomaSignDetachedOp
       OpAnomaVerifyWithMessage -> anomaVerifyWithMessageOp
+      OpAnomaByteArrayToAnomaContents -> anomaByteArrayToAnomaContents
+      OpAnomaByteArrayFromAnomaContents -> anomaByteArrayFromAnomaContents
       OpPoseidonHash -> poseidonHashOp
       OpEc -> ecOp
       OpRandomEcPoint -> randomEcPointOp
@@ -432,6 +435,31 @@ geval opts herr tab env0 = eval' env0
                         _ -> err "anomaVerifyWithMessageOp: both arguments are not bytearrays"
         {-# INLINE anomaVerifyWithMessageOp #-}
 
+        anomaByteArrayToAnomaContents :: [Node] -> Node
+        anomaByteArrayToAnomaContents = checkApply $ \arg ->
+          let !v = eval' env arg
+           in if
+                  | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                      mkBuiltinApp' OpAnomaByteArrayToAnomaContents [v]
+                  | otherwise ->
+                      case (byteStringFromNode v) of
+                        (Just bs) -> nodeFromInteger (byteStringToIntegerLE bs)
+                        _ -> err "anomaByteArrayToAnomaContents: expected argument to be a bytearray"
+        {-# INLINE anomaByteArrayToAnomaContents #-}
+
+        anomaByteArrayFromAnomaContents :: [Node] -> Node
+        anomaByteArrayFromAnomaContents = checkApply $ \arg1 arg2 ->
+          let !v1 = eval' env arg1
+              !v2 = eval' env arg2
+           in if
+                  | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                      mkBuiltinApp' OpAnomaByteArrayFromAnomaContents [v1, v2]
+                  | otherwise ->
+                      case (integerFromNode v1, integerFromNode v2) of
+                        (Just i1, Just i2) -> nodeFromByteString (integerToByteStringLELen (fromIntegral i1) i2)
+                        _ -> err "anomaByteArrayFromAnomaContents: expected both argmuments to be integers"
+        {-# INLINE anomaByteArrayFromAnomaContents #-}
+
         poseidonHashOp :: [Node] -> Node
         poseidonHashOp = unary $ \arg ->
           if

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

@@ -430,6 +430,8 @@ builtinOpArgTypes = \case
   OpAnomaSign -> [mkDynamic', mkDynamic']
   OpAnomaSignDetached -> [mkDynamic', mkDynamic']
   OpAnomaVerifyWithMessage -> [mkDynamic', mkDynamic']
+  OpAnomaByteArrayToAnomaContents -> [mkDynamic']
+  OpAnomaByteArrayFromAnomaContents -> [mkTypeInteger', mkTypeInteger']
   OpPoseidonHash -> [mkDynamic']
   OpEc -> [mkDynamic', mkTypeField', mkDynamic']
   OpRandomEcPoint -> []

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

@@ -33,6 +33,8 @@ data BuiltinOp
   | OpAnomaSign
   | OpAnomaSignDetached
   | OpAnomaVerifyWithMessage
+  | OpAnomaByteArrayToAnomaContents
+  | OpAnomaByteArrayFromAnomaContents
   | OpPoseidonHash
   | OpEc
   | OpRandomEcPoint
@@ -91,6 +93,8 @@ builtinOpArgsNum = \case
   OpAnomaSign -> 2
   OpAnomaSignDetached -> 2
   OpAnomaVerifyWithMessage -> 2
+  OpAnomaByteArrayToAnomaContents -> 1
+  OpAnomaByteArrayFromAnomaContents -> 2
   OpPoseidonHash -> 1
   OpEc -> 3
   OpRandomEcPoint -> 0
@@ -138,6 +142,8 @@ builtinIsFoldable = \case
   OpAnomaSign -> False
   OpAnomaSignDetached -> False
   OpAnomaVerifyWithMessage -> False
+  OpAnomaByteArrayToAnomaContents -> False
+  OpAnomaByteArrayFromAnomaContents -> False
   OpPoseidonHash -> False
   OpEc -> False
   OpRandomEcPoint -> False
@@ -169,7 +175,9 @@ builtinsAnoma =
     OpAnomaVerifyDetached,
     OpAnomaSign,
     OpAnomaVerifyWithMessage,
-    OpAnomaSignDetached
+    OpAnomaSignDetached,
+    OpAnomaByteArrayToAnomaContents,
+    OpAnomaByteArrayFromAnomaContents
   ]
 
 builtinsUInt8 :: [BuiltinOp]

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

@@ -60,6 +60,8 @@ instance PrettyCode BuiltinOp where
     OpAnomaSign -> return primAnomaSign
     OpAnomaSignDetached -> return primAnomaSignDetached
     OpAnomaVerifyWithMessage -> return primAnomaVerifyWithMessage
+    OpAnomaByteArrayToAnomaContents -> return primAnomaByteArrayToAnomaContents
+    OpAnomaByteArrayFromAnomaContents -> return primAnomaByteArrayFromAnomaContents
     OpPoseidonHash -> return primPoseidonHash
     OpEc -> return primEc
     OpRandomEcPoint -> return primRandomEcPoint
@@ -875,6 +877,12 @@ primAnomaSignDetached = primitive Str.anomaSignDetached
 primAnomaVerifyWithMessage :: Doc Ann
 primAnomaVerifyWithMessage = primitive Str.anomaVerifyWithMessage
 
+primAnomaByteArrayToAnomaContents :: Doc Ann
+primAnomaByteArrayToAnomaContents = primitive Str.anomaByteArrayToAnomaContents
+
+primAnomaByteArrayFromAnomaContents :: Doc Ann
+primAnomaByteArrayFromAnomaContents = primitive Str.anomaByteArrayFromAnomaContents
+
 primPoseidonHash :: Doc Ann
 primPoseidonHash = primitive Str.cairoPoseidon
 

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

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

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

@@ -616,6 +616,8 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinAnomaSign -> return ()
       Internal.BuiltinAnomaSignDetached -> return ()
       Internal.BuiltinAnomaVerifyWithMessage -> return ()
+      BuiltinAnomaByteArrayToAnomaContents -> return ()
+      BuiltinAnomaByteArrayFromAnomaContents -> return ()
       Internal.BuiltinPoseidon -> return ()
       Internal.BuiltinEcOp -> return ()
       Internal.BuiltinRandomEcPoint -> return ()
@@ -811,6 +813,18 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
                   )
               )
           )
+      Internal.BuiltinAnomaByteArrayToAnomaContents ->
+        registerAxiomDef (mkLambda' mkDynamic' (mkBuiltinApp' OpAnomaByteArrayToAnomaContents [mkVar' 0]))
+      Internal.BuiltinAnomaByteArrayFromAnomaContents -> do
+        natType <- getNatType
+        registerAxiomDef
+          ( mkLambda'
+              natType
+              ( mkLambda'
+                  natType
+                  (mkBuiltinApp' OpAnomaByteArrayFromAnomaContents [mkVar' 1, mkVar' 0])
+              )
+          )
       Internal.BuiltinPoseidon -> do
         psName <- getPoseidonStateName
         psSym <- getPoseidonStateSymbol
@@ -1233,6 +1247,8 @@ goApplication a = do
         Just Internal.BuiltinAnomaSign -> app
         Just Internal.BuiltinAnomaSignDetached -> app
         Just Internal.BuiltinAnomaVerifyWithMessage -> app
+        Just Internal.BuiltinAnomaByteArrayToAnomaContents -> app
+        Just Internal.BuiltinAnomaByteArrayFromAnomaContents -> app
         Just Internal.BuiltinPoseidon -> app
         Just Internal.BuiltinEcOp -> app
         Just Internal.BuiltinRandomEcPoint -> app

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

@@ -105,6 +105,8 @@ fromCore fsize tab =
         BuiltinAnomaSign -> False
         BuiltinAnomaSignDetached -> False
         BuiltinAnomaVerifyWithMessage -> False
+        BuiltinAnomaByteArrayToAnomaContents -> False
+        BuiltinAnomaByteArrayFromAnomaContents -> False
         BuiltinPoseidon -> False
         BuiltinEcOp -> False
         BuiltinRandomEcPoint -> False

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

@@ -584,6 +584,8 @@ registerBuiltinAxiom d = \case
   BuiltinAnomaSign -> registerAnomaSign d
   BuiltinAnomaSignDetached -> registerAnomaSignDetached d
   BuiltinAnomaVerifyWithMessage -> registerAnomaVerifyWithMessage d
+  BuiltinAnomaByteArrayToAnomaContents -> registerByteArrayToAnomaContents d
+  BuiltinAnomaByteArrayFromAnomaContents -> registerByteArrayFromAnomaContents d
   BuiltinPoseidon -> registerPoseidon d
   BuiltinEcOp -> registerEcOp d
   BuiltinRandomEcPoint -> registerRandomEcPoint d

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

@@ -495,6 +495,8 @@ compile = \case
         Tree.OpAnomaSign -> return (goAnomaSign args)
         Tree.OpAnomaVerifyWithMessage -> return (goAnomaVerifyWithMessage args)
         Tree.OpAnomaSignDetached -> return (goAnomaSignDetached args)
+        Tree.OpAnomaByteArrayFromAnomaContents -> return (goAnomaByteArrayFromAnomaContents args)
+        Tree.OpAnomaByteArrayToAnomaContents -> return (goAnomaByteArrayToAnomaContents args)
 
     goByteArrayOp :: Tree.NodeByteArray -> Sem r (Term Natural)
     goByteArrayOp Tree.NodeByteArray {..} = do
@@ -591,6 +593,16 @@ compile = \case
           )
       _ -> impossible
 
+    goAnomaByteArrayToAnomaContents :: [Term Natural] -> Term Natural
+    goAnomaByteArrayToAnomaContents = \case
+      [ba] -> byteArrayPayload "bytearryToAnomaContents-payload" ba
+      _ -> impossible
+
+    goAnomaByteArrayFromAnomaContents :: [Term Natural] -> Term Natural
+    goAnomaByteArrayFromAnomaContents = \case
+      [len, contents] -> mkByteArray len contents
+      _ -> impossible
+
     -- Conceptually this function is:
     -- anomaDecode <$> verify signedMessage pubKey
     --

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

@@ -96,4 +96,8 @@ data AnomaOp
     OpAnomaVerifyWithMessage
   | -- | Produce a cryptographic signature of an Anoma value
     OpAnomaSignDetached
+  | -- | Construct an Anoma atom from a ByteArray with LSB ordering
+    OpAnomaByteArrayToAnomaContents
+  | -- | Construct a ByteArray from the bytes of an Anoma atom with LSB ordering
+    OpAnomaByteArrayFromAnomaContents
   deriving stock (Eq)

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

@@ -291,6 +291,8 @@ instance PrettyCode AnomaOp where
     OpAnomaSign -> Str.anomaSign
     OpAnomaVerifyWithMessage -> Str.anomaVerifyWithMessage
     OpAnomaSignDetached -> Str.anomaSignDetached
+    OpAnomaByteArrayFromAnomaContents -> Str.anomaByteArrayFromAnomaContents
+    OpAnomaByteArrayToAnomaContents -> Str.anomaByteArrayToAnomaContents
 
 instance PrettyCode UnaryOpcode where
   ppCode = \case

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

@@ -18,6 +18,8 @@ checkNoAnoma = walkT checkNode
         OpAnomaSign -> unsupportedErr "OpAnomaSign"
         OpAnomaSignDetached -> unsupportedErr "OpAnomaSignDetached"
         OpAnomaVerifyWithMessage -> unsupportedErr "OpAnomaVerifyWithMessage"
+        OpAnomaByteArrayFromAnomaContents -> unsupportedErr "OpAnomaByteArrayFromAnomaContents"
+        OpAnomaByteArrayToAnomaContents -> unsupportedErr "OpAnomaByteArrayToAnomaContents"
         where
           unsupportedErr :: Text -> Sem r ()
           unsupportedErr opName =

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

@@ -339,6 +339,8 @@ genCode infoTable fi =
       Core.OpAnomaSign -> OpAnomaSign
       Core.OpAnomaSignDetached -> OpAnomaSignDetached
       Core.OpAnomaVerifyWithMessage -> OpAnomaVerifyWithMessage
+      Core.OpAnomaByteArrayToAnomaContents -> OpAnomaByteArrayToAnomaContents
+      Core.OpAnomaByteArrayFromAnomaContents -> OpAnomaByteArrayFromAnomaContents
       _ -> impossible
 
     getArgsNum :: Symbol -> Int

src/Juvix/Extra/Strings.hs

@@ -374,6 +374,12 @@ anomaSignDetached = "anoma-sign-detached"
 anomaVerifyWithMessage :: (IsString s) => s
 anomaVerifyWithMessage = "anoma-verify-with-message"
 
+anomaByteArrayToAnomaContents :: (IsString s) => s
+anomaByteArrayToAnomaContents = "anoma-bytearray-to-anoma-contents"
+
+anomaByteArrayFromAnomaContents :: (IsString s) => s
+anomaByteArrayFromAnomaContents = "anoma-bytearray-from-anoma-contents"
+
 builtinSeq :: (IsString s) => s
 builtinSeq = "seq"
 

test/Anoma/Compilation/Positive.hs

@@ -630,5 +630,17 @@ allTests =
             [nock| [2 258] |],
             [nock| 1 |],
             [nock| [1 0] |]
+          ],
+      mkAnomaCallTest
+        "Test083: Anoma ByteArray"
+        $(mkRelDir ".")
+        $(mkRelFile "test083.juvix")
+        []
+        $ checkOutput
+          [ [nock| [[0 0] 0] |],
+            [nock| [[3 0] 0] |],
+            [nock| [[4 1] 1] |],
+            [nock| [[2 258] 258] |],
+            [nock| [[1 0] 0] |]
           ]
     ]