Add support for anoma-decode builtin (#2775)

This PR adds support for the `anoma-decode` builtin

```
builtin anoma-decode
axiom anomaDecode : {A : Type} -> Nat -> A
```

Adds:
* An implementation of the `cue` function in Haskell
* Unit tests for `cue`
* A benchmark for `cue` applied to the Anoma / nockma stdlib

Benchmark results:

```
      cue (jam stdlib): OK
        36.0 ms ± 2.0 ms
```

Closes:
*  https://github.com/anoma/juvix/issues/2764

bench2/Benchmark/Nockma/Encoding.hs

@@ -6,11 +6,16 @@ import Juvix.Compiler.Nockma.Stdlib (stdlib)
 import Juvix.Prelude.Base
 import Test.Tasty.Bench
 
+jamStdlib :: Natural
+jamStdlib = runJam stdlib
+
 bm :: Benchmark
 bm =
   bgroup
     "Jam"
-    [bench "jam stdlib" $ nf runJam stdlib]
+    [ bench "jam stdlib" $ nf runJam stdlib,
+      bench "cue (jam stdlib)" $ nf runCue jamStdlib
+    ]
 
 runJam :: Term Natural -> Natural
 runJam =
@@ -19,3 +24,18 @@ runJam =
     . run
     . runError @NockNaturalNaturalError
     . jam
+
+mkAtom :: Natural -> Atom Natural
+mkAtom n =
+  Atom
+    { _atomInfo = emptyAtomInfo,
+      _atom = n
+    }
+
+runCue :: Natural -> Term Natural
+runCue =
+  run
+    . runErrorNoCallStackWith @NockNaturalNaturalError (const (error "NockNaturalNaturalError"))
+    . runErrorNoCallStackWith @DecodingError (const (error "decoding failed"))
+    . cue
+    . mkAtom

package.yaml

@@ -55,6 +55,7 @@ dependencies:
   - cereal == 0.5.*
   - containers == 0.6.*
   - cryptohash-sha256 == 0.11.*
+  - deepseq == 1.5.*
   - directory == 1.3.*
   - dlist == 1.0.*
   - edit-distance == 0.2.*

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

@@ -235,6 +235,7 @@ genCode fi =
       Tree.OpFail -> mkInstr Failure
       Tree.OpAnomaGet -> impossible
       Tree.OpAnomaEncode -> impossible
+      Tree.OpAnomaDecode -> impossible
 
     snocReturn :: Bool -> Code' -> Code'
     snocReturn True code = DL.snoc code (mkInstr Return)

src/Juvix/Compiler/Builtins/Anoma.hs

@@ -30,3 +30,16 @@ registerAnomaEncode f = do
     ((ftype ==% (u <>--> encodeT --> nat)) freeVars)
     (error "anomaEncode must be of type {A : Type} -> A -> Nat")
   registerBuiltin BuiltinAnomaEncode (f ^. axiomName)
+
+registerAnomaDecode :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
+registerAnomaDecode f = do
+  let ftype = f ^. axiomType
+      u = ExpressionUniverse smallUniverseNoLoc
+      l = getLoc f
+  decodeT <- freshVar l "decodeT"
+  nat <- getBuiltinName (getLoc f) BuiltinNat
+  let freeVars = HashSet.fromList [decodeT]
+  unless
+    ((ftype ==% (u <>--> nat --> decodeT)) freeVars)
+    (error "anomaEncode must be of type {A : Type} -> Nat -> A")
+  registerBuiltin BuiltinAnomaDecode (f ^. axiomName)

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

@@ -189,6 +189,7 @@ data BuiltinAxiom
   | BuiltinIntPrint
   | BuiltinAnomaGet
   | BuiltinAnomaEncode
+  | BuiltinAnomaDecode
   | BuiltinPoseidon
   | BuiltinEcOp
   | BuiltinRandomEcPoint
@@ -225,6 +226,7 @@ instance Pretty BuiltinAxiom where
     BuiltinIntPrint -> Str.intPrint
     BuiltinAnomaGet -> Str.anomaGet
     BuiltinAnomaEncode -> Str.anomaEncode
+    BuiltinAnomaDecode -> Str.anomaDecode
     BuiltinPoseidon -> Str.cairoPoseidon
     BuiltinEcOp -> Str.cairoEcOp
     BuiltinRandomEcPoint -> Str.cairoRandomEcPoint

src/Juvix/Compiler/Core/Evaluator.hs

@@ -192,6 +192,7 @@ geval opts herr ctx env0 = eval' env0
       OpTrace -> traceOp
       OpAnomaGet -> anomaGetOp
       OpAnomaEncode -> anomaEncodeOp
+      OpAnomaDecode -> anomaDecodeOp
       OpPoseidonHash -> poseidonHashOp
       OpEc -> ecOp
       OpRandomEcPoint -> randomEcPointOp
@@ -344,9 +345,18 @@ geval opts herr ctx env0 = eval' env0
               | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
                   mkBuiltinApp' OpAnomaEncode [eval' env arg]
               | otherwise ->
-                  err "unsupported builtin operation: OpAnomaGet"
+                  err "unsupported builtin operation: OpAnomaEncode"
         {-# INLINE anomaEncodeOp #-}
 
+        anomaDecodeOp :: [Node] -> Node
+        anomaDecodeOp = unary $ \arg ->
+          if
+              | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                  mkBuiltinApp' OpAnomaDecode [eval' env arg]
+              | otherwise ->
+                  err "unsupported builtin operation: OpAnomaDecode"
+        {-# INLINE anomaDecodeOp #-}
+
         poseidonHashOp :: [Node] -> Node
         poseidonHashOp = unary $ \arg ->
           if

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

@@ -425,6 +425,7 @@ builtinOpArgTypes = \case
   OpFail -> [mkTypeString']
   OpAnomaGet -> [mkDynamic']
   OpAnomaEncode -> [mkDynamic']
+  OpAnomaDecode -> [mkDynamic']
   OpPoseidonHash -> [mkDynamic']
   OpEc -> [mkDynamic', mkTypeField', mkDynamic']
   OpRandomEcPoint -> []

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

@@ -28,6 +28,7 @@ data BuiltinOp
   | OpFail
   | OpAnomaGet
   | OpAnomaEncode
+  | OpAnomaDecode
   | OpPoseidonHash
   | OpEc
   | OpRandomEcPoint
@@ -73,6 +74,7 @@ builtinOpArgsNum = \case
   OpFail -> 1
   OpAnomaGet -> 1
   OpAnomaEncode -> 1
+  OpAnomaDecode -> 1
   OpPoseidonHash -> 1
   OpEc -> 3
   OpRandomEcPoint -> 0
@@ -111,6 +113,7 @@ builtinIsFoldable = \case
   OpFail -> False
   OpAnomaGet -> False
   OpAnomaEncode -> False
+  OpAnomaDecode -> False
   OpPoseidonHash -> False
   OpEc -> False
   OpRandomEcPoint -> False
@@ -125,4 +128,4 @@ builtinsCairo :: [BuiltinOp]
 builtinsCairo = [OpPoseidonHash, OpEc, OpRandomEcPoint]
 
 builtinsAnoma :: [BuiltinOp]
-builtinsAnoma = [OpAnomaGet, OpAnomaEncode]
+builtinsAnoma = [OpAnomaGet, OpAnomaEncode, OpAnomaDecode]

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

@@ -54,6 +54,7 @@ instance PrettyCode BuiltinOp where
     OpFail -> return primFail
     OpAnomaGet -> return primAnomaGet
     OpAnomaEncode -> return primAnomaEncode
+    OpAnomaDecode -> return primAnomaDecode
     OpPoseidonHash -> return primPoseidonHash
     OpEc -> return primEc
     OpRandomEcPoint -> return primRandomEcPoint
@@ -805,6 +806,9 @@ primAnomaGet = primitive Str.anomaGet
 primAnomaEncode :: Doc Ann
 primAnomaEncode = primitive Str.anomaEncode
 
+primAnomaDecode :: Doc Ann
+primAnomaDecode = primitive Str.anomaDecode
+
 primPoseidonHash :: Doc Ann
 primPoseidonHash = primitive Str.cairoPoseidon
 

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

@@ -68,6 +68,7 @@ computeNodeTypeInfo md = umapL go
           OpFail -> Info.getNodeType node
           OpAnomaGet -> Info.getNodeType node
           OpAnomaEncode -> Info.getNodeType node
+          OpAnomaDecode -> Info.getNodeType node
           OpPoseidonHash -> case _builtinAppArgs of
             [arg] -> Info.getNodeType arg
             _ -> error "incorrect poseidon builtin application"

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

@@ -578,6 +578,7 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinFieldToNat -> return ()
       Internal.BuiltinAnomaGet -> return ()
       Internal.BuiltinAnomaEncode -> return ()
+      Internal.BuiltinAnomaDecode -> return ()
       Internal.BuiltinPoseidon -> return ()
       Internal.BuiltinEcOp -> return ()
       Internal.BuiltinRandomEcPoint -> return ()
@@ -704,6 +705,14 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
               mkSmallUniv
               (mkLambda' (mkVar' 0) (mkBuiltinApp' OpAnomaEncode [mkVar' 0]))
           )
+      Internal.BuiltinAnomaDecode -> do
+        natName <- getNatName
+        natSym <- getNatSymbol
+        registerAxiomDef
+          ( mkLambda'
+              (mkTypeConstr (setInfoName natName mempty) natSym [])
+              (mkLambda' (mkVar' 0) (mkBuiltinApp' OpAnomaDecode [mkVar' 0]))
+          )
       Internal.BuiltinPoseidon -> do
         psName <- getPoseidonStateName
         psSym <- getPoseidonStateSymbol
@@ -1103,6 +1112,7 @@ goApplication a = do
         Just Internal.BuiltinFieldToNat -> app
         Just Internal.BuiltinAnomaGet -> app
         Just Internal.BuiltinAnomaEncode -> app
+        Just Internal.BuiltinAnomaDecode -> app
         Just Internal.BuiltinPoseidon -> app
         Just Internal.BuiltinEcOp -> app
         Just Internal.BuiltinRandomEcPoint -> app

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

@@ -97,6 +97,7 @@ fromCore fsize tab =
         BuiltinIntPrint -> False
         BuiltinAnomaGet -> False
         BuiltinAnomaEncode -> False
+        BuiltinAnomaDecode -> False
         BuiltinPoseidon -> False
         BuiltinEcOp -> False
         BuiltinRandomEcPoint -> False

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

@@ -570,6 +570,7 @@ registerBuiltinAxiom d = \case
   BuiltinIntPrint -> registerIntPrint d
   BuiltinAnomaGet -> registerAnomaGet d
   BuiltinAnomaEncode -> registerAnomaEncode d
+  BuiltinAnomaDecode -> registerAnomaDecode d
   BuiltinPoseidon -> registerPoseidon d
   BuiltinEcOp -> registerEcOp d
   BuiltinRandomEcPoint -> registerRandomEcPoint d

src/Juvix/Compiler/Nockma/Encoding.hs

@@ -1,6 +1,8 @@
 module Juvix.Compiler.Nockma.Encoding
   ( module Juvix.Compiler.Nockma.Encoding.Jam,
+    module Juvix.Compiler.Nockma.Encoding.Cue,
   )
 where
 
+import Juvix.Compiler.Nockma.Encoding.Cue
 import Juvix.Compiler.Nockma.Encoding.Jam

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

@@ -24,13 +24,11 @@ integerToVectorBits = run . execBitWriter . writeIntegral
 -- | Computes the number of bits required to store the argument in binary
 -- NB: 0 is encoded to the empty bit vector (as specified by the Hoon serialization spec), so 0 has bit length 0.
 bitLength :: forall a. (Integral a) => a -> Int
-bitLength = \case
-  0 -> 0
-  n -> go (fromIntegral n) 0
-    where
-      go :: Integer -> Int -> Int
-      go 0 acc = acc
-      go x acc = go (x `shiftR` 1) (acc + 1)
+bitLength =
+  length
+    . takeWhile (/= 0)
+    . iterate (`shiftR` 1)
+    . toInteger
 
 -- | Decode a vector of bits (ordered from least to most significant bits) to an integer
 vectorBitsToInteger :: Bit.Vector Bit -> Integer

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

@@ -0,0 +1,307 @@
+module Juvix.Compiler.Nockma.Encoding.Cue where
+
+import Data.Bit as Bit
+import Data.Bits
+import Juvix.Compiler.Nockma.Encoding.Base
+import Juvix.Compiler.Nockma.Encoding.Effect.BitReader
+import Juvix.Compiler.Nockma.Language
+import Juvix.Compiler.Nockma.Pretty.Base
+import Juvix.Prelude.Base
+import VectorBuilder.Builder as Builder
+import VectorBuilder.Vector
+
+data CueState a = CueState
+  { _cueStateCache :: HashMap Int (Term a)
+  }
+
+initCueState :: CueState a
+initCueState =
+  CueState
+    { _cueStateCache = mempty
+    }
+
+data CueEnv = CueEnv
+  {_cueEnvStartPos :: Int}
+
+initCueEnv :: CueEnv
+initCueEnv = CueEnv {_cueEnvStartPos = 0}
+
+makeLenses ''CueState
+makeLenses ''CueEnv
+
+data DecodingError
+  = DecodingErrorInvalidTag
+  | DecodingErrorCacheMiss
+  | DecodingErrorInvalidLength
+  | DecodingErrorExpectedAtom
+  | DecodingErrorInvalidAtom
+  | DecodingErrorInvalidBackref
+  deriving stock (Show)
+
+instance PrettyCode DecodingError where
+  ppCode = \case
+    DecodingErrorInvalidTag -> return "Invalid tag"
+    DecodingErrorCacheMiss -> return "Cache miss"
+    DecodingErrorInvalidLength -> return "Invalid length"
+    DecodingErrorExpectedAtom -> return "Expected atom"
+    DecodingErrorInvalidAtom -> return "Invalid atom"
+    DecodingErrorInvalidBackref -> return "Invalid backref"
+
+-- | Register the start of processing a new entity
+registerElementStart ::
+  ( Members
+      '[ BitReader,
+         Reader CueEnv
+       ]
+      r
+  ) =>
+  Sem r a ->
+  Sem r a
+registerElementStart sem = do
+  pos <- getCurrentPosition
+  local (set cueEnvStartPos pos) sem
+
+-- | Convert a BitReadError to a DecodingError
+handleBitError :: (Member (Error DecodingError) r) => DecodingError -> Sem (Error BitReadError ': r) x -> Sem r x
+handleBitError e = mapError @_ @_ @BitReadError (const e)
+
+-- | Consume the encoded length from the input bits
+consumeLength :: forall r. (Members '[BitReader, Error DecodingError] r) => Sem r Int
+consumeLength = do
+  lenOfLen <- handleBitError DecodingErrorInvalidLength countBitsUntilOne
+  if
+      | lenOfLen == 0 -> return 0
+      | otherwise -> do
+          -- The mist significant bit of the length is omitted
+          let lenBits = lenOfLen - 1
+          foldlM go (bit lenBits) [0 .. lenBits - 1]
+  where
+    go :: Int -> Int -> Sem r Int
+    go acc n = do
+      Bit b <- handleBitError DecodingErrorInvalidLength nextBit
+      return $
+        if
+            | b -> setBit acc n
+            | otherwise -> acc
+
+-- | Consume a nock integer from the input bits
+consumeInteger ::
+  forall r.
+  ( Members
+      '[ BitReader,
+         Error DecodingError
+       ]
+      r
+  ) =>
+  DecodingError ->
+  Int ->
+  Sem r Integer
+consumeInteger e len
+  | len == 0 = return 0
+  | otherwise =
+      vectorBitsToInteger
+        . build
+        . foldable
+        <$> handleBitError e (nextBits len)
+
+data JamTag = JamTagAtom | JamTagCell | JamTagBackref
+
+-- | Consume a nock tag from the input bits
+consumeTag ::
+  forall r.
+  ( Members
+      '[ BitReader,
+         Error DecodingError
+       ]
+      r
+  ) =>
+  Sem r JamTag
+consumeTag = do
+  Bit b0 <- nextBit'
+  if
+      | b0 -> do
+          Bit b1 <- nextBit'
+          if
+              | b1 -> return JamTagBackref
+              | otherwise -> return JamTagCell
+      | otherwise -> return JamTagAtom
+  where
+    nextBit' :: Sem r Bit
+    nextBit' = handleBitError DecodingErrorInvalidTag nextBit
+
+cacheCueTerm ::
+  forall a r.
+  ( Members
+      '[ State (CueState a),
+         Reader CueEnv
+       ]
+      r
+  ) =>
+  Term a ->
+  Sem r ()
+cacheCueTerm t = do
+  pos <- asks (^. cueEnvStartPos)
+  modify' (set (cueStateCache . at pos) (Just t))
+
+lookupCueCache ::
+  ( Members
+      '[ Error DecodingError,
+         State (CueState a)
+       ]
+      r
+  ) =>
+  Int ->
+  Sem r (Term a)
+lookupCueCache pos =
+  fromMaybeM
+    (throw DecodingErrorCacheMiss)
+    (gets (^. cueStateCache . at pos))
+
+-- | Transform an atom to a vector of bits
+atomToBits ::
+  forall a r.
+  ( NockNatural a,
+    Member (Error (ErrNockNatural' a)) r
+  ) =>
+  Atom a ->
+  Sem r (Bit.Vector Bit)
+atomToBits a' = do
+  n <- nockNatural' a'
+  return (integerToVectorBits @Integer (fromIntegral n))
+
+-- | Transfor a vector of bits to a decoded term
+cueFromBits ::
+  forall a r.
+  ( NockNatural a,
+    Members
+      '[ Error DecodingError,
+         Error (ErrNockNatural' a)
+       ]
+      r
+  ) =>
+  Bit.Vector Bit ->
+  Sem r (Term a)
+cueFromBits v = evalBitReader v (evalState (initCueState @a) (runReader initCueEnv cueFromBitsSem))
+
+cueFromBitsSem ::
+  forall a r.
+  ( NockNatural a,
+    Members
+      '[ BitReader,
+         Error DecodingError,
+         State (CueState a),
+         Reader CueEnv,
+         Error (ErrNockNatural' a)
+       ]
+      r
+  ) =>
+  Sem r (Term a)
+cueFromBitsSem = registerElementStart $ do
+  tag <- consumeTag
+  case tag of
+    JamTagAtom -> goAtom
+    JamTagBackref -> goBackref
+    JamTagCell -> goCell
+  where
+    goAtom :: Sem r (Term a)
+    goAtom = do
+      a <- TermAtom <$> consumeAtom
+      cacheCueTerm a
+      return a
+
+    goBackref :: Sem r (Term a)
+    goBackref = do
+      a <- consumeNatAtom
+      idx <- maybe (throw DecodingErrorInvalidBackref) return (safeNaturalToInt (a ^. atom))
+      lookupCueCache idx
+
+    goCell :: Sem r (Term a)
+    goCell = do
+      _cellLeft <- cueFromBitsSem
+      _cellRight <- cueFromBitsSem
+      let cell = TermCell (Cell' {_cellInfo = emptyCellInfo, ..})
+      cacheCueTerm cell
+      return cell
+
+    consumeNatAtom :: Sem r (Atom Natural)
+    consumeNatAtom = do
+      len <- consumeLength
+      if
+          | len == 0 -> return (Atom 0 emptyAtomInfo)
+          | otherwise -> do
+              a <- consumeInteger DecodingErrorInvalidAtom len
+              return (Atom (fromInteger a) emptyAtomInfo)
+
+    consumeAtom :: Sem r (Atom a)
+    consumeAtom = do
+      len <- consumeLength
+      if
+          | len == 0 -> do
+              z <- fromNatural' @a 0
+              return (Atom z emptyAtomInfo)
+          | otherwise -> do
+              a <- consumeInteger DecodingErrorInvalidAtom len
+              n <- fromNatural' (fromInteger a)
+              return (Atom n emptyAtomInfo)
+
+-- | Decode an nock Atom to a nock term
+cue ::
+  forall a r.
+  ( NockNatural a,
+    Members
+      '[ Error DecodingError,
+         Error (ErrNockNatural a)
+       ]
+      r
+  ) =>
+  Atom a ->
+  Sem r (Term a)
+cue a' =
+  runErrorNoCallStackWith @(ErrNockNatural' a)
+    (\(ErrNockNatural' e) -> throw e)
+    (cue' a')
+
+-- | A variant of cue with `ErrNockNatural` wrapped in a newtype to disambiguate it from DecodingError
+cue' ::
+  forall a r.
+  ( NockNatural a,
+    Members
+      '[ Error DecodingError,
+         Error (ErrNockNatural' a)
+       ]
+      r
+  ) =>
+  Atom a ->
+  Sem r (Term a)
+cue' a' = atomToBits a' >>= cueFromBits
+
+cueEither ::
+  -- NB: The signature returns the DecodingError in an Either to avoid
+  -- overlapping instances with `ErrNockNatural a` when errors are handled. See
+  -- the comment above `ErrNockNatural' a` for more explanation.
+  forall a r.
+  ( NockNatural a,
+    Member (Error (ErrNockNatural a)) r
+  ) =>
+  Atom a ->
+  Sem r (Either DecodingError (Term a))
+cueEither =
+  runErrorNoCallStackWith @(ErrNockNatural' a) (\(ErrNockNatural' e) -> throw e)
+    . runErrorNoCallStack @DecodingError
+    . cue'
+
+{- `ErrNockNatural a` must be wrapped in a newtype to avoid overlapping instances
+with `DecodingError` when errors are handled before the type variable `a` is
+resolved.
+
+When handling an error with `runError` before `a` is resolved, the compiler
+cannot distinguish between `Error (ErrNockNatural a)` and `Error DecodingError`.
+For some `a` it's possible that `ErrNockNatural a` is equal to `DecodingError`.
+-}
+newtype ErrNockNatural' a = ErrNockNatural' (ErrNockNatural a)
+
+fromNatural' :: forall a r. (NockNatural a, Member (Error (ErrNockNatural' a)) r) => Natural -> Sem r a
+fromNatural' = mapError (ErrNockNatural' @a) . fromNatural
+
+nockNatural' :: forall a r. (NockNatural a, Member (Error (ErrNockNatural' a)) r) => Atom a -> Sem r Natural
+nockNatural' = mapError (ErrNockNatural' @a) . nockNatural

src/Juvix/Compiler/Nockma/Encoding/Effect/BitReader.hs

@@ -0,0 +1,58 @@
+module Juvix.Compiler.Nockma.Encoding.Effect.BitReader where
+
+import Data.Bit as Bit
+import Data.Vector.Unboxed qualified as U
+import Effectful (Eff)
+import Juvix.Prelude.Base
+
+data BitReadError = BitReadErrorNoMoreBits
+
+data BitReader :: Effect where
+  -- makeSem ''BitReader has a type error if Sem is used instead of Eff
+  NextBit :: (Member (Error BitReadError) r) => BitReader (Eff r) Bit
+  GetCurrentPosition :: BitReader m Int
+
+makeSem ''BitReader
+
+nextBits :: (Members '[BitReader, Error BitReadError] r) => Int -> Sem r [Bit]
+nextBits n = replicateM n nextBit
+
+countBitsUntil :: forall r. (Members '[BitReader, Error BitReadError] r) => (Bit -> Bool) -> Sem r Int
+countBitsUntil p = go 0
+  where
+    go :: Int -> Sem r Int
+    go n = do
+      b <- nextBit
+      if
+          | p b -> return n
+          | otherwise -> go (n + 1)
+
+countBitsUntilOne :: (Members '[BitReader, Error BitReadError] r) => Sem r Int
+countBitsUntilOne = countBitsUntil (== Bit True)
+
+data ReaderState = ReaderState
+  { _readerStateBits :: Bit.Vector Bit,
+    _readerStateCurrentPos :: Int
+  }
+
+makeLenses ''ReaderState
+
+initReaderState :: Bit.Vector Bit -> ReaderState
+initReaderState bits =
+  ReaderState
+    { _readerStateBits = bits,
+      _readerStateCurrentPos = 0
+    }
+
+evalBitReader :: Bit.Vector Bit -> Sem (BitReader ': r) a -> Sem r a
+evalBitReader v = evalState (initReaderState v) . re
+
+re :: Sem (BitReader ': r) a -> Sem (State ReaderState ': r) a
+re = interpretTopH $ \env -> \case
+  GetCurrentPosition -> gets (^. readerStateCurrentPos)
+  NextBit -> do
+    bits <- gets (^. readerStateBits)
+    pos <- gets (^. readerStateCurrentPos)
+    case bits U.!? pos of
+      Just b -> modify' (over readerStateCurrentPos (+ 1)) >> return b
+      Nothing -> localSeqUnlift env $ \unlift -> unlift (throw BitReadErrorNoMoreBits)

src/Juvix/Compiler/Nockma/Evaluator.hs

@@ -7,6 +7,7 @@ module Juvix.Compiler.Nockma.Evaluator
 where
 
 import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Nockma.Encoding
 import Juvix.Compiler.Nockma.Encoding qualified as Encoding
 import Juvix.Compiler.Nockma.Evaluator.Error
 import Juvix.Compiler.Nockma.Evaluator.Options
@@ -230,6 +231,11 @@ evalProfile inistack initerm =
             StdlibLe -> binCmp (<=)
             StdlibPow2 -> unaArith (2 ^)
             StdlibEncode -> TermAtom <$> Encoding.jam args'
+            StdlibDecode -> case args' of
+              TermAtom a -> do
+                r <- Encoding.cueEither a
+                either (throwDecodingFailed args') return r
+              TermCell {} -> throwDecodingFailed args' DecodingErrorExpectedAtom
 
         goAutoConsCell :: AutoConsCell a -> Sem r (Term a)
         goAutoConsCell c = do

src/Juvix/Compiler/Nockma/Evaluator/Error.hs

@@ -6,6 +6,7 @@ module Juvix.Compiler.Nockma.Evaluator.Error
 where
 
 import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Nockma.Encoding
 import Juvix.Compiler.Nockma.Evaluator.Crumbs
 import Juvix.Compiler.Nockma.Evaluator.Storage
 import Juvix.Compiler.Nockma.Language
@@ -22,6 +23,7 @@ data NockEvalError a
   | -- TODO perhaps this should be a repl error type
     ErrAssignmentNotFound Text
   | ErrKeyNotInStorage (KeyNotInStorage a)
+  | ErrDecodingFailed (DecodingFailed a)
 
 newtype GenericNockEvalError = GenericNockEvalError
   { _genericNockEvalErrorMessage :: AnsiText
@@ -58,6 +60,12 @@ data InvalidNockOp a = InvalidNockOp
 
 data NoStack = NoStack
 
+data DecodingFailed a = DecodingFailed
+  { _decodingFailedCtx :: EvalCtx,
+    _decodingFailedTerm :: Term a,
+    _decodingFailedReason :: DecodingError
+  }
+
 throwInvalidNockOp :: (Members '[Error (NockEvalError a), Reader EvalCtx] r) => Atom a -> Sem r x
 throwInvalidNockOp a = do
   ctx <- ask
@@ -109,6 +117,17 @@ throwKeyNotInStorage k = do
           _keyNotInStorageStorage = s
         }
 
+throwDecodingFailed :: (Members '[Error (NockEvalError a), Reader EvalCtx] r) => Term a -> DecodingError -> Sem r x
+throwDecodingFailed a e = do
+  ctx <- ask
+  throw $
+    ErrDecodingFailed
+      DecodingFailed
+        { _decodingFailedCtx = ctx,
+          _decodingFailedTerm = a,
+          _decodingFailedReason = e
+        }
+
 instance PrettyCode NoStack where
   ppCode _ = return "Missing stack"
 
@@ -152,6 +171,13 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (KeyNotInStorage a) where
         pt2 <- ppCode t2
         return (pt1 <+> ":=" <+> pt2)
 
+instance (PrettyCode a, NockNatural a) => PrettyCode (DecodingFailed a) where
+  ppCode DecodingFailed {..} = do
+    t <- ppCode _decodingFailedTerm
+    ctx <- ppCtx _decodingFailedCtx
+    r <- ppCode _decodingFailedReason
+    return (ctx <> "Decoding the term" <+> t <+> "failed with reason:" <> line <> r)
+
 instance (PrettyCode a, NockNatural a) => PrettyCode (NockEvalError a) where
   ppCode = \case
     ErrInvalidPath e -> ppCode e
@@ -161,3 +187,4 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (NockEvalError a) where
     ErrNoStack e -> ppCode e
     ErrAssignmentNotFound e -> return (pretty e)
     ErrKeyNotInStorage e -> ppCode e
+    ErrDecodingFailed e -> ppCode e

src/Juvix/Compiler/Nockma/Language.hs

@@ -51,6 +51,8 @@ data Term a
 
 instance (Hashable a) => Hashable (Term a)
 
+instance (NFData a) => NFData (Term a)
+
 data StdlibCall a = StdlibCall
   { _stdlibCallFunction :: StdlibFunction,
     _stdlibCallArgs :: Term a
@@ -59,6 +61,8 @@ data StdlibCall a = StdlibCall
 
 instance (Hashable a) => Hashable (StdlibCall a)
 
+instance (NFData a) => NFData (StdlibCall a)
+
 newtype Tag = Tag
   { _unTag :: Text
   }
@@ -66,6 +70,8 @@ newtype Tag = Tag
 
 instance Hashable Tag
 
+instance NFData Tag
+
 data CellInfo a = CellInfo
   { _cellInfoLoc :: Irrelevant (Maybe Interval),
     _cellInfoTag :: Maybe Tag,
@@ -75,6 +81,8 @@ data CellInfo a = CellInfo
 
 instance (Hashable a) => Hashable (CellInfo a)
 
+instance (NFData a) => NFData (CellInfo a)
+
 data Cell a = Cell'
   { _cellLeft :: Term a,
     _cellRight :: Term a,
@@ -84,6 +92,8 @@ data Cell a = Cell'
 
 instance (Hashable a) => Hashable (Cell a)
 
+instance (NFData a) => NFData (Cell a)
+
 data AtomInfo = AtomInfo
   { _atomInfoHint :: Maybe AtomHint,
     _atomInfoTag :: Maybe Tag,
@@ -93,6 +103,8 @@ data AtomInfo = AtomInfo
 
 instance Hashable AtomInfo
 
+instance NFData AtomInfo
+
 data Atom a = Atom
   { _atom :: a,
     _atomInfo :: AtomInfo
@@ -101,6 +113,8 @@ data Atom a = Atom
 
 instance (Hashable a) => Hashable (Atom a)
 
+instance (NFData a) => NFData (Atom a)
+
 data AtomHint
   = AtomHintOp
   | AtomHintPath
@@ -112,6 +126,8 @@ data AtomHint
 
 instance Hashable AtomHint
 
+instance NFData AtomHint
+
 data NockOp
   = OpAddress
   | OpQuote

src/Juvix/Compiler/Nockma/StdlibFunction.hs

@@ -21,3 +21,4 @@ stdlibPath = \case
   StdlibLt -> [nock| [9 343 0 31] |]
   StdlibPow2 -> [nock| [9 4 0 3] |]
   StdlibEncode -> [nock| [9 22 0 1] |]
+  StdlibDecode -> [nock| [9 94 0 1] |]

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

@@ -15,6 +15,7 @@ instance Pretty StdlibFunction where
     StdlibLe -> "<="
     StdlibPow2 -> "pow2"
     StdlibEncode -> "encode"
+    StdlibDecode -> "decode"
 
 data StdlibFunction
   = StdlibDec
@@ -27,6 +28,9 @@ data StdlibFunction
   | StdlibLe
   | StdlibPow2
   | StdlibEncode
+  | StdlibDecode
   deriving stock (Show, Lift, Eq, Bounded, Enum, Generic)
 
 instance Hashable StdlibFunction
+
+instance NFData StdlibFunction

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

@@ -427,6 +427,7 @@ compile = \case
         Tree.OpTrace -> goTrace arg
         Tree.OpAnomaGet -> goAnomaGet arg
         Tree.OpAnomaEncode -> goAnomaEncode arg
+        Tree.OpAnomaDecode -> goAnomaDecode arg
 
     goPrimUnop :: Tree.UnaryOp -> Term Natural -> Term Natural
     goPrimUnop op arg = case op of
@@ -446,6 +447,9 @@ compile = \case
     goAnomaEncode :: Term Natural -> Sem r (Term Natural)
     goAnomaEncode arg = return (callStdlib StdlibEncode [arg])
 
+    goAnomaDecode :: Term Natural -> Sem r (Term Natural)
+    goAnomaDecode arg = return (callStdlib StdlibDecode [arg])
+
     goTrace :: Term Natural -> Sem r (Term Natural)
     goTrace arg = do
       enabled <- asks (^. compilerOptions . compilerOptionsEnableTrace)

src/Juvix/Compiler/Tree/Evaluator.hs

@@ -76,6 +76,7 @@ hEval hout tab = eval' [] mempty
                 OpFail -> goFail v
                 OpAnomaGet -> evalError "Unsupported op: OpAnomaGet"
                 OpAnomaEncode -> evalError "Unsupported op: OpAnomaEncode"
+                OpAnomaDecode -> evalError "Unsupported op: OpAnomaDecode"
 
         goFail :: Value -> Value
         goFail v = evalError ("failure: " <> printValue tab v)

src/Juvix/Compiler/Tree/EvaluatorEff.hs

@@ -71,6 +71,7 @@ eval tab = runReader emptyEvalCtx . eval'
             OpFail -> goFail v
             OpAnomaGet -> evalError "Unsupported op: OpAnomaGet"
             OpAnomaEncode -> evalError "Unsupported op: OpAnomaEncode"
+            OpAnomaDecode -> evalError "Unsupported op: OpAnomaDecode"
 
         goFail :: Value -> Sem r' Value
         goFail v = evalError ("failure: " <> printValue tab v)

src/Juvix/Compiler/Tree/Language.hs

@@ -71,6 +71,8 @@ data UnaryOpcode
     OpAnomaGet
   | -- | Encode a value to an Anoma atom
     OpAnomaEncode
+  | -- | Decode a value from an Anoma atom
+    OpAnomaDecode
 
 data NodeBinop = NodeBinop
   { _nodeBinopInfo :: NodeInfo,

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

@@ -247,6 +247,7 @@ instance PrettyCode UnaryOpcode where
     OpFail -> return $ primitive Str.instrFailure
     OpAnomaGet -> return $ primitive Str.anomaGet
     OpAnomaEncode -> return $ primitive Str.anomaEncode
+    OpAnomaDecode -> return $ primitive Str.anomaDecode
 
 instance PrettyCode NodeUnop where
   ppCode NodeUnop {..} = do

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

@@ -13,6 +13,7 @@ checkNoAnoma = walkT checkNode
       Unop NodeUnop {..} -> case _nodeUnopOpcode of
         OpAnomaGet -> unsupportedErr "OpAnomaGet"
         OpAnomaEncode -> unsupportedErr "OpAnomaEncode"
+        OpAnomaDecode -> unsupportedErr "OpAnomaDecode"
         OpFail -> return ()
         OpTrace -> return ()
         PrimUnop {} -> return ()

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

@@ -67,6 +67,7 @@ inferType tab funInfo = goInfer mempty
       OpFail -> checkUnop TyDynamic TyDynamic
       OpAnomaGet -> checkUnop TyDynamic TyDynamic
       OpAnomaEncode -> checkUnop TyDynamic TyDynamic
+      OpAnomaDecode -> checkUnop TyDynamic TyDynamic
       where
         loc = _nodeUnopInfo ^. nodeInfoLocation
 

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

@@ -297,6 +297,7 @@ genCode infoTable fi =
       Core.OpFail -> OpFail
       Core.OpAnomaGet -> OpAnomaGet
       Core.OpAnomaEncode -> OpAnomaEncode
+      Core.OpAnomaDecode -> OpAnomaDecode
       _ -> impossible
 
     genCairoOp :: Core.BuiltinOp -> CairoOp

src/Juvix/Data/Irrelevant.hs

@@ -13,6 +13,8 @@ newtype Irrelevant a = Irrelevant
   }
   deriving stock (Generic, Data, Lift)
 
+instance (NFData a) => NFData (Irrelevant a)
+
 instance (Serialize a) => Serialize (Irrelevant a) where
   put (Irrelevant x) = S.put x
   get = Irrelevant <$> S.get

src/Juvix/Data/Loc.hs

@@ -12,6 +12,8 @@ newtype Pos = Pos {_unPos :: Word64}
 
 instance Serialize Pos
 
+instance NFData Pos
+
 instance Semigroup Pos where
   Pos x <> Pos y = Pos (x + y)
 
@@ -32,6 +34,8 @@ instance Hashable FileLoc
 
 instance Serialize FileLoc
 
+instance NFData FileLoc
+
 instance Ord FileLoc where
   compare (FileLoc l c o) (FileLoc l' c' o') = compare (l, c, o) (l', c', o')
 
@@ -78,6 +82,8 @@ instance Hashable Interval
 
 instance Serialize Interval
 
+instance NFData Interval
+
 class HasLoc t where
   getLoc :: t -> Interval
 

src/Juvix/Extra/Strings.hs

@@ -332,6 +332,9 @@ anomaGet = "anoma-get"
 anomaEncode :: (IsString s) => s
 anomaEncode = "anoma-encode"
 
+anomaDecode :: (IsString s) => s
+anomaDecode = "anoma-decode"
+
 builtinSeq :: (IsString s) => s
 builtinSeq = "seq"
 

src/Juvix/Prelude/Base/Foundation.hs

@@ -56,6 +56,7 @@ module Juvix.Prelude.Base.Foundation
     module Text.Show,
     module Control.Monad.Catch,
     module Control.Monad.Zip,
+    module Control.DeepSeq,
     Data,
     Text,
     pack,
@@ -73,6 +74,7 @@ module Juvix.Prelude.Base.Foundation
 where
 
 import Control.Applicative
+import Control.DeepSeq (NFData)
 import Control.Monad.Catch (ExitCase (..), MonadMask, MonadThrow, generalBracket, throwM)
 import Control.Monad.Extra hiding (fail, forM, mconcatMapM, whileJustM)
 import Control.Monad.Extra qualified as Monad

test/Anoma/Compilation/Positive.hs

@@ -549,5 +549,16 @@ allTests =
         $(mkRelDir ".")
         $(mkRelFile "test075.juvix")
         []
-        $ checkNatOutput [2, 84081, 4657, 12]
+        $ checkNatOutput [2, 84081, 4657, 12],
+      mkAnomaCallTest
+        "Test076: Anoma decode"
+        $(mkRelDir ".")
+        $(mkRelFile "test076.juvix")
+        []
+        $ checkOutput
+          [ [nock| 0 |],
+            [nock| [1 2 0] |],
+            [nock| [1 2] |],
+            [nock| false |]
+          ]
     ]

test/Nockma/Eval/Positive.hs

@@ -7,6 +7,7 @@ import Juvix.Compiler.Nockma.Anoma
 import Juvix.Compiler.Nockma.Evaluator
 import Juvix.Compiler.Nockma.Language
 import Juvix.Compiler.Nockma.Pretty
+import Juvix.Compiler.Nockma.Stdlib (stdlib)
 import Juvix.Compiler.Nockma.Translation.FromSource.QQ
 import Juvix.Compiler.Nockma.Translation.FromTree
 
@@ -90,11 +91,23 @@ compilerTest :: Text -> Term Natural -> Check () -> Bool -> Test
 compilerTest n mainFun _testCheck _evalInterceptStdlibCalls =
   anomaTest n mainFun [] _testCheck _evalInterceptStdlibCalls
 
-serializationTest :: Text -> Term Natural -> Term Natural -> Test
-serializationTest n jamTerm cueTerm =
-  let _testCheck :: Check () = eqNock cueTerm
-      mainFun :: Term Natural = callStdlib StdlibEncode [OpQuote # jamTerm]
-   in anomaTest n mainFun [] _testCheck True
+serializationTest :: Term Natural -> Term Natural -> [Test]
+serializationTest jamTerm cueTerm =
+  let jamCheck :: Check () = eqNock cueTerm
+      jamCall :: Term Natural = callStdlib StdlibEncode [OpQuote # jamTerm]
+      cueCall :: Term Natural = callStdlib StdlibDecode [OpQuote # cueTerm]
+      cueCheck :: Check () = eqNock jamTerm
+      ppJamTerm :: Text = ppPrint jamTerm
+      ppCueTerm :: Text = ppPrint cueTerm
+   in [ anomaTest ("jam " <> ppJamTerm <> " == " <> ppCueTerm) jamCall [] jamCheck True,
+        anomaTest ("cue " <> ppCueTerm <> " == " <> ppJamTerm) cueCall [] cueCheck True
+      ]
+
+-- | Test decode (encode t) = t
+serializationIdTest :: Text -> Term Natural -> Test
+serializationIdTest n jamTerm =
+  let call :: Term Natural = callStdlib StdlibDecode [callStdlib StdlibEncode [OpQuote # jamTerm]]
+   in anomaTest (n <> ": " <> "cue . jam = id") call [] (eqNock jamTerm) True
 
 withAssertErrKeyNotInStorage :: Test -> Test
 withAssertErrKeyNotInStorage Test {..} =
@@ -154,24 +167,60 @@ anomaCallingConventionTests =
 
 serializationTests :: [Test]
 serializationTests =
-  [ serializationTest "jam 0" [nock| 0 |] [nock| 2 |],
-    serializationTest "jam 1" [nock| 1 |] [nock| 12 |],
-    serializationTest "jam 2" [nock| 2 |] [nock| 72 |],
-    serializationTest "jam 19" [nock| 19 |] [nock| 2480 |],
-    serializationTest "jam 581.949.002" [nock| 581.949.002 |] [nock| 1.191.831.557.952 |],
-    serializationTest "jam [1 19]" [nock| [0 19] |] [nock| 39689 |],
-    serializationTest "jam [1 1]" [nock| [1 1] |] [nock| 817 |],
-    serializationTest "jam [10.000 10.000]" [nock| [10.000 10.000] |] [nock| 4.952.983.169 |],
-    serializationTest "jam [999.999.999 999.999.999]" [nock| [999.999.999 999.999.999] |] [nock| 1.301.217.674.263.809 |],
-    serializationTest "jam [222 444 888]" [nock| [222 444 888] |] [nock| 250.038.217.192.960.129 |],
-    serializationTest "jam [[107 110] [107 110]]" [nock| [[107 110] [107 110]] |] [nock| 635.080.761.093 |],
-    serializationTest "jam [0 1 2 3 4 5 6 7 8 9 10]" [nock| [0 1 2 3 4 5 6 7 8 9 10] |] [nock| 25.681.224.503.728.653.597.984.370.231.065 |],
-    serializationTest "jam [99 100 101 102 103 104 0]" [nock| [99 100 101 102 103 104 0] |] [nock| 223.372.995.869.285.333.705.242.560.449 |],
-    serializationTest "jam [[222 444 888] [222 444 888]]" [nock| [[222 444 888] [222 444 888]] |] [nock| 170.479.614.045.978.345.989 |],
-    serializationTest "jam [[0 1] [1 2] [2 3] [3 4] 0]" [nock| [[0 1] [1 2] [2 3] [3 4] 0] |] [nock| 11.976.248.475.217.237.797 |],
-    serializationTest "jam [[0 1] [1 2] [2 3] [3 4] [4 5] [5 6] [6 7] [7 8] [8 9] 0]" [nock| [[0 1] [1 2] [2 3] [3 4] [4 5] [5 6] [6 7] [7 8] [8 9] 0] |] [nock| 7.694.087.033.387.855.647.747.387.855.514.468.399.947.749.137.782.565 |],
-    serializationTest "jam [[0 1] [2 3] [4 5] [6 7] [8 9] [10 11] [12 13] [14 15] [16 17] [18 19] [20 21] 0] " [nock| [[0 1] [2 3] [4 5] [6 7] [8 9] [10 11] [12 13] [14 15] [16 17] [18 19] [20 21] 0] |] [nock| 308.947.677.754.874.070.959.300.747.182.056.036.528.545.493.781.368.831.595.479.491.505.523.344.414.501 |]
-  ]
+  serializationIdTest
+    "stdlib"
+    stdlib
+    : serializationTest
+      [nock| 0 |]
+      [nock| 2 |]
+      <> serializationTest
+        [nock| 1 |]
+        [nock| 12 |]
+      <> serializationTest
+        [nock| 2 |]
+        [nock| 72 |]
+      <> serializationTest
+        [nock| 19 |]
+        [nock| 2480 |]
+      <> serializationTest
+        [nock| 581.949.002 |]
+        [nock| 1.191.831.557.952 |]
+      <> serializationTest
+        [nock| [0 19] |]
+        [nock| 39689 |]
+      <> serializationTest
+        [nock| [1 1] |]
+        [nock| 817 |]
+      <> serializationTest
+        [nock| [10.000 10.000] |]
+        [nock| 4.952.983.169 |]
+      <> serializationTest
+        [nock| [999.999.999 999.999.999] |]
+        [nock| 1.301.217.674.263.809 |]
+      <> serializationTest
+        [nock| [222 444 888] |]
+        [nock| 250.038.217.192.960.129 |]
+      <> serializationTest
+        [nock| [[107 110] [107 110]] |]
+        [nock| 635.080.761.093 |]
+      <> serializationTest
+        [nock| [0 1 2 3 4 5 6 7 8 9 10] |]
+        [nock| 25.681.224.503.728.653.597.984.370.231.065 |]
+      <> serializationTest
+        [nock| [99 100 101 102 103 104 0] |]
+        [nock| 223.372.995.869.285.333.705.242.560.449 |]
+      <> serializationTest
+        [nock| [[222 444 888] [222 444 888]] |]
+        [nock| 170.479.614.045.978.345.989 |]
+      <> serializationTest
+        [nock| [[0 1] [1 2] [2 3] [3 4] 0] |]
+        [nock| 11.976.248.475.217.237.797 |]
+      <> serializationTest
+        [nock| [[0 1] [1 2] [2 3] [3 4] [4 5] [5 6] [6 7] [7 8] [8 9] 0] |]
+        [nock| 7.694.087.033.387.855.647.747.387.855.514.468.399.947.749.137.782.565 |]
+      <> serializationTest
+        [nock| [[0 1] [2 3] [4 5] [6 7] [8 9] [10 11] [12 13] [14 15] [16 17] [18 19] [20 21] 0] |]
+        [nock| 308.947.677.754.874.070.959.300.747.182.056.036.528.545.493.781.368.831.595.479.491.505.523.344.414.501 |]
 
 juvixCallingConventionTests :: [Test]
 juvixCallingConventionTests =

tests/Anoma/Compilation/positive/test076.juvix

@@ -0,0 +1,17 @@
+module test076;
+
+import Stdlib.Prelude open;
+import Stdlib.Debug.Trace open;
+
+builtin anoma-decode
+axiom anomaDecode : {A : Type} -> Nat -> A;
+
+main : Bool :=
+  -- cue 2 == 0
+  trace (anomaDecode {Nat} 2)
+  -- cue 84081 == [1 2 0]
+  >>> trace (anomaDecode {List Nat} 84081)
+  -- cue 4657 == [1 2]
+  >>> trace (anomaDecode {Nat × Nat} 4657)
+  -- cue 12 == 1
+  >>> anomaDecode {Bool} 12;