diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
index 7c66fc1c23..61ae8f7b6c 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -56,7 +56,9 @@ goModule onlyTypes infoTable Internal.Module {..} =
   Theory
     { _theoryName = over nameText toIsabelleName $ over namePretty toIsabelleName _moduleName,
       _theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports),
-      _theoryStatements = concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
+      _theoryStatements = case _modulePragmas ^. pragmasIsabelleIgnore of
+        Just (PragmaIsabelleIgnore True) -> []
+        _ -> concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
     }
   where
     toIsabelleName :: Text -> Text
@@ -75,13 +77,18 @@ goModule onlyTypes infoTable Internal.Module {..} =
     goMutualBlock :: Internal.MutualBlock -> [Statement]
     goMutualBlock Internal.MutualBlock {..} =
       filter (\stmt -> not onlyTypes || isTypeDef stmt) $
-        map goMutualStatement (toList _mutualStatements)
+        mapMaybe goMutualStatement (toList _mutualStatements)
 
-    goMutualStatement :: Internal.MutualStatement -> Statement
+    checkNotIgnored :: Pragmas -> a -> Maybe a
+    checkNotIgnored pragmas x = case pragmas ^. pragmasIsabelleIgnore of
+      Just (PragmaIsabelleIgnore True) -> Nothing
+      _ -> Just x
+
+    goMutualStatement :: Internal.MutualStatement -> Maybe Statement
     goMutualStatement = \case
-      Internal.StatementInductive x -> goInductiveDef x
-      Internal.StatementFunction x -> goFunctionDef x
-      Internal.StatementAxiom x -> goAxiomDef x
+      Internal.StatementInductive x -> checkNotIgnored (x ^. Internal.inductivePragmas) $ goInductiveDef x
+      Internal.StatementFunction x -> checkNotIgnored (x ^. Internal.funDefPragmas) $ goFunctionDef x
+      Internal.StatementAxiom x -> checkNotIgnored (x ^. Internal.axiomPragmas) $ goAxiomDef x
 
     goInductiveDef :: Internal.InductiveDef -> Statement
     goInductiveDef Internal.InductiveDef {..}
diff --git a/src/Juvix/Compiler/Builtins/Anoma.hs b/src/Juvix/Compiler/Builtins/Anoma.hs
index 8bd67b9b2e..ec1868f4be 100644
--- a/src/Juvix/Compiler/Builtins/Anoma.hs
+++ b/src/Juvix/Compiler/Builtins/Anoma.hs
@@ -87,3 +87,23 @@ checkAnomaSignDetached f = do
   unless
     ((ftype ==% (u <>--> dataT --> byteArray --> byteArray)) freeVars)
     $ builtinsErrorText (getLoc f) "anomaSignDetached must be of type {A : Type} -> A -> ByteArray -> ByteArray"
+
+checkAnomaByteArrayToAnomaContents :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkAnomaByteArrayToAnomaContents f = do
+  let ftype = f ^. axiomType
+      l = getLoc f
+  byteArray <- getBuiltinNameScoper l BuiltinByteArray
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless
+    (ftype == (byteArray --> nat_))
+    $ builtinsErrorText l "toAnomaContents must be of type ByteArray -> Nat"
+
+checkAnomaByteArrayFromAnomaContents :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkAnomaByteArrayFromAnomaContents f = do
+  let ftype = f ^. axiomType
+      l = getLoc f
+  byteArray <- getBuiltinNameScoper l BuiltinByteArray
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless
+    (ftype == (nat_ --> nat_ --> byteArray))
+    $ builtinsErrorText l "fromAnomaContents must be of type Nat -> Nat -> ByteArray"
diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
index 5884fdb780..e10b8e78a8 100644
--- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
@@ -221,6 +221,8 @@ data BuiltinAxiom
   | BuiltinAnomaSign
   | BuiltinAnomaSignDetached
   | BuiltinAnomaVerifyWithMessage
+  | BuiltinAnomaByteArrayToAnomaContents
+  | BuiltinAnomaByteArrayFromAnomaContents
   | BuiltinPoseidon
   | BuiltinEcOp
   | BuiltinRandomEcPoint
@@ -265,6 +267,8 @@ instance HasNameKind BuiltinAxiom where
     BuiltinAnomaSign -> KNameFunction
     BuiltinAnomaSignDetached -> KNameFunction
     BuiltinAnomaVerifyWithMessage -> KNameFunction
+    BuiltinAnomaByteArrayToAnomaContents -> KNameFunction
+    BuiltinAnomaByteArrayFromAnomaContents -> KNameFunction
     BuiltinPoseidon -> KNameFunction
     BuiltinEcOp -> KNameFunction
     BuiltinRandomEcPoint -> KNameFunction
@@ -316,6 +320,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
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 0d042f7725..7ccf1414f3 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -1687,7 +1687,7 @@ checkSections sec = topBindings helper
                                   _projectionKind = kind,
                                   _projectionFieldBuiltin = field ^. fieldBuiltin,
                                   _projectionDoc = field ^. fieldDoc,
-                                  _projectionPragmas = field ^. fieldPragmas
+                                  _projectionPragmas = combinePragmas (i ^. inductivePragmas) (field ^. fieldPragmas)
                                 }
                               where
                                 kind :: ProjectionKind
@@ -1695,6 +1695,19 @@ checkSections sec = topBindings helper
                                   ExplicitField -> ProjectionExplicit
                                   ImplicitInstanceField -> ProjectionCoercion
 
+                                combinePragmas :: Maybe ParsedPragmas -> Maybe ParsedPragmas -> Maybe ParsedPragmas
+                                combinePragmas p1 p2 = case (p1, p2) of
+                                  (Nothing, Nothing) -> Nothing
+                                  (Just p, Nothing) -> Just p
+                                  (Nothing, Just p) -> Just p
+                                  (Just p1', Just p2') ->
+                                    Just
+                                      ( over
+                                          (withLocParam . withSourceValue . pragmasIsabelleIgnore)
+                                          (\i2 -> i2 <|> (p1' ^. withLocParam . withSourceValue . pragmasIsabelleIgnore))
+                                          p2'
+                                      )
+
                             getFields :: Sem (Fail ': s') [RecordStatement 'Parsed]
                             getFields = case i ^. inductiveConstructors of
                               c :| [] -> case c ^. constructorRhs of
diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index 1448a15339..21bc538477 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs
index a57b0c4e26..d133dc8f67 100644
--- a/src/Juvix/Compiler/Core/Extra/Utils.hs
+++ b/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 -> []
diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs
index e4c1cb3d3b..c6c81a1bee 100644
--- a/src/Juvix/Compiler/Core/Language/Builtins.hs
+++ b/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]
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index 987f877be1..433567ce9d 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/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
 
diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
index b180ad5763..812c60dcd6 100644
--- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
+++ b/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"
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
index 14e76454c2..819ccf009f 100644
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
index 6c25d41b0b..e87799c5af 100644
--- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 0461e0a86a..b2edf6ea9b 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -585,6 +585,8 @@ checkBuiltinAxiom d b = localBuiltins $ case b of
   BuiltinAnomaSign -> checkAnomaSign d
   BuiltinAnomaSignDetached -> checkAnomaSignDetached d
   BuiltinAnomaVerifyWithMessage -> checkAnomaVerifyWithMessage d
+  BuiltinAnomaByteArrayFromAnomaContents -> checkAnomaByteArrayFromAnomaContents d
+  BuiltinAnomaByteArrayToAnomaContents -> checkAnomaByteArrayToAnomaContents d
   BuiltinPoseidon -> checkPoseidon d
   BuiltinEcOp -> checkEcOp d
   BuiltinRandomEcPoint -> checkRandomEcPoint d
diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
index 51dbed4187..31081dc833 100644
--- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
+++ b/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
     --
diff --git a/src/Juvix/Compiler/Tree/Language/Builtins.hs b/src/Juvix/Compiler/Tree/Language/Builtins.hs
index 3145026a2a..4802d90a28 100644
--- a/src/Juvix/Compiler/Tree/Language/Builtins.hs
+++ b/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)
diff --git a/src/Juvix/Compiler/Tree/Pretty/Base.hs b/src/Juvix/Compiler/Tree/Pretty/Base.hs
index abdec2bd81..59433b8cdb 100644
--- a/src/Juvix/Compiler/Tree/Pretty/Base.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs b/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs
index 5ddfb1ae13..ca91ab57f9 100644
--- a/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs
+++ b/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 =
diff --git a/src/Juvix/Compiler/Tree/Translation/FromCore.hs b/src/Juvix/Compiler/Tree/Translation/FromCore.hs
index 52e5ead2bf..a5d578299a 100644
--- a/src/Juvix/Compiler/Tree/Translation/FromCore.hs
+++ b/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
diff --git a/src/Juvix/Data/Pragmas.hs b/src/Juvix/Data/Pragmas.hs
index ad0690e065..641692887e 100644
--- a/src/Juvix/Data/Pragmas.hs
+++ b/src/Juvix/Data/Pragmas.hs
@@ -71,6 +71,11 @@ newtype PragmaIsabelleFunction = PragmaIsabelleFunction
   }
   deriving stock (Show, Eq, Ord, Data, Generic)
 
+newtype PragmaIsabelleIgnore = PragmaIsabelleIgnore
+  { _pragmaIsabelleIgnore :: Bool
+  }
+  deriving stock (Show, Eq, Ord, Data, Generic)
+
 data Pragmas = Pragmas
   { _pragmasInline :: Maybe PragmaInline,
     _pragmasUnroll :: Maybe PragmaUnroll,
@@ -82,7 +87,8 @@ data Pragmas = Pragmas
     _pragmasSpecialiseBy :: Maybe PragmaSpecialiseBy,
     _pragmasEval :: Maybe PragmaEval,
     _pragmasIsabelleOperator :: Maybe PragmaIsabelleOperator,
-    _pragmasIsabelleFunction :: Maybe PragmaIsabelleFunction
+    _pragmasIsabelleFunction :: Maybe PragmaIsabelleFunction,
+    _pragmasIsabelleIgnore :: Maybe PragmaIsabelleIgnore
   }
   deriving stock (Show, Eq, Ord, Data, Generic)
 
@@ -121,6 +127,8 @@ instance Hashable PragmaIsabelleOperator
 
 instance Hashable PragmaIsabelleFunction
 
+instance Hashable PragmaIsabelleIgnore
+
 instance Hashable Pragmas
 
 instance Serialize PragmaInline
@@ -171,6 +179,10 @@ instance Serialize PragmaIsabelleFunction
 
 instance NFData PragmaIsabelleFunction
 
+instance Serialize PragmaIsabelleIgnore
+
+instance NFData PragmaIsabelleIgnore
+
 instance Serialize Pragmas
 
 instance NFData Pragmas
@@ -201,6 +213,7 @@ instance FromJSON Pragmas where
         _pragmasEval <- keyMay "eval" parseEval
         _pragmasIsabelleOperator <- keyMay "isabelle-operator" parseIsabelleOperator
         _pragmasIsabelleFunction <- keyMay "isabelle-function" parseIsabelleFunction
+        _pragmasIsabelleIgnore <- keyMay "isabelle-ignore" parseIsabelleIgnore
         return Pragmas {..}
 
       parseInline :: Parse YamlError PragmaInline
@@ -273,6 +286,11 @@ instance FromJSON Pragmas where
         _pragmaIsabelleFunctionName <- key "name" asText
         return PragmaIsabelleFunction {..}
 
+      parseIsabelleIgnore :: Parse YamlError PragmaIsabelleIgnore
+      parseIsabelleIgnore = do
+        _pragmaIsabelleIgnore <- asBool
+        return PragmaIsabelleIgnore {..}
+
       parseSpecialiseArg :: Parse YamlError PragmaSpecialiseArg
       parseSpecialiseArg =
         (SpecialiseArgNum <$> asIntegral)
@@ -316,7 +334,8 @@ instance Semigroup Pragmas where
         _pragmasSpecialiseArgs = p2 ^. pragmasSpecialiseArgs <|> p1 ^. pragmasSpecialiseArgs,
         _pragmasSpecialiseBy = p2 ^. pragmasSpecialiseBy <|> p1 ^. pragmasSpecialiseBy,
         _pragmasIsabelleOperator = p2 ^. pragmasIsabelleOperator,
-        _pragmasIsabelleFunction = p2 ^. pragmasIsabelleFunction
+        _pragmasIsabelleFunction = p2 ^. pragmasIsabelleFunction,
+        _pragmasIsabelleIgnore = p2 ^. pragmasIsabelleIgnore <|> p1 ^. pragmasIsabelleIgnore
       }
 
 instance Monoid Pragmas where
@@ -332,7 +351,8 @@ instance Monoid Pragmas where
         _pragmasSpecialiseBy = Nothing,
         _pragmasEval = Nothing,
         _pragmasIsabelleOperator = Nothing,
-        _pragmasIsabelleFunction = Nothing
+        _pragmasIsabelleFunction = Nothing,
+        _pragmasIsabelleIgnore = Nothing
       }
 
 adjustPragmaInline :: Int -> PragmaInline -> PragmaInline
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index fa064e51b9..7fe7156802 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/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"
 
diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs
index 91d414f485..3f53eb01ba 100644
--- a/test/Anoma/Compilation/Positive.hs
+++ b/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] |]
           ]
     ]
diff --git a/tests/Anoma/Compilation/positive/test083.juvix b/tests/Anoma/Compilation/positive/test083.juvix
new file mode 100644
index 0000000000..683558e2e5
--- /dev/null
+++ b/tests/Anoma/Compilation/positive/test083.juvix
@@ -0,0 +1,41 @@
+module test083;
+
+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-length
+axiom size : ByteArray -> Nat;
+
+builtin anoma-bytearray-to-anoma-contents
+axiom toAnomaContents : ByteArray -> Nat;
+
+builtin anoma-bytearray-from-anoma-contents
+axiom fromAnomaContents : Nat -> Nat -> ByteArray;
+
+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];
+
+testByteArray (ba : ByteArray) : Pair ByteArray Nat :=
+  let
+    anomaContents := toAnomaContents ba;
+  in fromAnomaContents (size ba) anomaContents, anomaContents;
+
+main : Pair ByteArray Nat :=
+  trace (testByteArray bs0)
+    >-> trace (testByteArray bs1)
+    >-> trace (testByteArray bs2)
+    >-> trace (testByteArray bs3)
+    >-> testByteArray bs4;
diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix
index 69d15bdb4e..0cd881bc34 100644
--- a/tests/positive/Isabelle/Program.juvix
+++ b/tests/positive/Isabelle/Program.juvix
@@ -91,6 +91,7 @@ type Either' A B := Left' A | Right' B;
 
 -- Records
 
+{-# isabelle-ignore: true #-}
 type R := mkR {
   r1 : Nat;
   r2 : Nat;
diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy
index df548c13df..e9c72431aa 100644
--- a/tests/positive/Isabelle/isabelle/Program.thy
+++ b/tests/positive/Isabelle/isabelle/Program.thy
@@ -99,16 +99,6 @@ datatype ('A, 'B) Either'
   = Left' 'A |
     Right' 'B
 
-record R =
-  r1 :: nat
-  r2 :: nat
-
-fun r1 :: "R \<Rightarrow> nat" where
-  "r1 (mkR r1' r2') = r1'"
-
-fun r2 :: "R \<Rightarrow> nat" where
-  "r2 (mkR r1' r2') = r2'"
-
 fun bf :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
   "bf b1 b2 = (\<not> (b1 \<and> b2))"