From 2e006421a57aca22a54e7d769a10dd709073cee1 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Thu, 21 Mar 2024 15:44:14 +0000
Subject: [PATCH] Support nockma scry (#2678)

This PR adds support for Anoma/Nockma scry OP. It is used for obtaining
values from the Anoma storage (key value store). See the [linked
issue](https://github.com/anoma/juvix/issues/2672) for details on scry.

This PR adds support for scry to the Nockma language and compilation
from the frontend via a builtin: `anoma-get`:

```
builtin anoma-get
axiom anomaGet : {Value Key : Type} -> Key -> Value
```

In the backend, the `Value` and `Key` types could be anything, they will
depend on choices of Anoma applications. The type of the returned
`Value` is unchecked. It's currently the responsibility of the user to
match the annotated type with the type of data in storage.

We will not put this builtin in the standard library. It will be exposed
in the anoma-juvix library. It's likely that the frontend `anomaGet`
function will evolve as we use it to write Anoma applications and learn
how they work.

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

---------

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
---
 .../Compiler/Asm/Translation/FromTree.hs      |  1 +
 src/Juvix/Compiler/Builtins.hs                |  2 +
 src/Juvix/Compiler/Builtins/Anoma.hs          | 19 ++++++
 src/Juvix/Compiler/Concrete/Data/Builtins.hs  |  2 +
 src/Juvix/Compiler/Core/Evaluator.hs          |  1 +
 src/Juvix/Compiler/Core/Extra/Utils.hs        |  1 +
 src/Juvix/Compiler/Core/Language/Builtins.hs  |  2 +
 src/Juvix/Compiler/Core/Pretty/Base.hs        |  4 ++
 .../Core/Transformation/ComputeTypeInfo.hs    |  1 +
 .../Compiler/Core/Translation/FromInternal.hs | 11 +++
 .../Core/Translation/Stripped/FromCore.hs     |  1 +
 .../Internal/Translation/FromConcrete.hs      |  1 +
 src/Juvix/Compiler/Nockma/EvalCompiled.hs     |  1 +
 src/Juvix/Compiler/Nockma/Evaluator.hs        | 17 ++++-
 src/Juvix/Compiler/Nockma/Evaluator/Error.hs  | 33 +++++++++
 .../Compiler/Nockma/Evaluator/Storage.hs      | 12 ++++
 src/Juvix/Compiler/Nockma/Language.hs         | 31 +++++++--
 .../Compiler/Nockma/StdlibFunction/Base.hs    |  4 +-
 .../Compiler/Nockma/Translation/FromTree.hs   |  4 ++
 .../Compiler/Tree/Data/TransformationId.hs    |  4 +-
 .../Tree/Data/TransformationId/Strings.hs     |  3 +
 src/Juvix/Compiler/Tree/Evaluator.hs          |  1 +
 src/Juvix/Compiler/Tree/EvaluatorEff.hs       |  1 +
 src/Juvix/Compiler/Tree/Keywords.hs           |  4 +-
 src/Juvix/Compiler/Tree/Language.hs           |  2 +
 src/Juvix/Compiler/Tree/Pretty/Base.hs        |  1 +
 src/Juvix/Compiler/Tree/Transformation.hs     |  2 +
 .../Tree/Transformation/CheckNoAnoma.hs       | 23 +++++++
 .../Compiler/Tree/Transformation/Validate.hs  |  1 +
 .../Compiler/Tree/Translation/FromCore.hs     |  1 +
 .../Compiler/Tree/Translation/FromSource.hs   |  1 +
 src/Juvix/Data/Irrelevant.hs                  |  3 +
 src/Juvix/Data/Keyword/All.hs                 |  3 +
 src/Juvix/Extra/Strings.hs                    |  3 +
 test/Anoma/Compilation/Positive.hs            | 30 +++++++--
 test/Compilation/Base.hs                      |  5 +-
 test/Nockma/Eval/Positive.hs                  | 37 ++++++++--
 test/Tree/Transformation.hs                   |  4 +-
 test/Tree/Transformation/CheckNoAnoma.hs      | 67 +++++++++++++++++++
 .../Anoma/Compilation/positive/test074.juvix  | 10 +++
 tests/Tree/negative/test009.jvt               |  5 ++
 41 files changed, 334 insertions(+), 25 deletions(-)
 create mode 100644 src/Juvix/Compiler/Builtins/Anoma.hs
 create mode 100644 src/Juvix/Compiler/Nockma/Evaluator/Storage.hs
 create mode 100644 src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs
 create mode 100644 test/Tree/Transformation/CheckNoAnoma.hs
 create mode 100644 tests/Anoma/Compilation/positive/test074.juvix
 create mode 100644 tests/Tree/negative/test009.jvt

diff --git a/src/Juvix/Compiler/Asm/Translation/FromTree.hs b/src/Juvix/Compiler/Asm/Translation/FromTree.hs
index f0619b9af5..e007289f78 100644
--- a/src/Juvix/Compiler/Asm/Translation/FromTree.hs
+++ b/src/Juvix/Compiler/Asm/Translation/FromTree.hs
@@ -227,6 +227,7 @@ genCode fi =
       Tree.PrimUnop op' -> mkUnop op'
       Tree.OpTrace -> mkInstr Trace
       Tree.OpFail -> mkInstr Failure
+      Tree.OpAnomaGet -> impossible
 
     snocReturn :: Bool -> Code' -> Code'
     snocReturn True code = DL.snoc code (mkInstr Return)
diff --git a/src/Juvix/Compiler/Builtins.hs b/src/Juvix/Compiler/Builtins.hs
index 00a2d1e8d7..afcc1f7ac1 100644
--- a/src/Juvix/Compiler/Builtins.hs
+++ b/src/Juvix/Compiler/Builtins.hs
@@ -9,9 +9,11 @@ module Juvix.Compiler.Builtins
     module Juvix.Compiler.Builtins.Field,
     module Juvix.Compiler.Builtins.Debug,
     module Juvix.Compiler.Builtins.Control,
+    module Juvix.Compiler.Builtins.Anoma,
   )
 where
 
+import Juvix.Compiler.Builtins.Anoma
 import Juvix.Compiler.Builtins.Bool
 import Juvix.Compiler.Builtins.Control
 import Juvix.Compiler.Builtins.Debug
diff --git a/src/Juvix/Compiler/Builtins/Anoma.hs b/src/Juvix/Compiler/Builtins/Anoma.hs
new file mode 100644
index 0000000000..b86882e143
--- /dev/null
+++ b/src/Juvix/Compiler/Builtins/Anoma.hs
@@ -0,0 +1,19 @@
+module Juvix.Compiler.Builtins.Anoma where
+
+import Data.HashSet qualified as HashSet
+import Juvix.Compiler.Builtins.Effect
+import Juvix.Compiler.Internal.Extra
+import Juvix.Prelude
+
+registerAnomaGet :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
+registerAnomaGet f = do
+  let ftype = f ^. axiomType
+      u = ExpressionUniverse smallUniverseNoLoc
+      l = getLoc f
+  keyT <- freshVar l "keyT"
+  valueT <- freshVar l "valueT"
+  let freeVars = HashSet.fromList [keyT, valueT]
+  unless
+    ((ftype ==% (u <>--> u <>--> keyT --> valueT)) freeVars)
+    (error "anomaGet must be of type {Value Key : Type} -> Key -> Value")
+  registerBuiltin BuiltinAnomaGet (f ^. axiomName)
diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
index df4a6c936c..b84e95ac9d 100644
--- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
@@ -177,6 +177,7 @@ data BuiltinAxiom
   | BuiltinFail
   | BuiltinIntToString
   | BuiltinIntPrint
+  | BuiltinAnomaGet
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
 
 instance Hashable BuiltinAxiom
@@ -208,6 +209,7 @@ instance Pretty BuiltinAxiom where
     BuiltinFail -> Str.fail_
     BuiltinIntToString -> Str.intToString
     BuiltinIntPrint -> Str.intPrint
+    BuiltinAnomaGet -> Str.anomaGet
 
 data BuiltinType
   = BuiltinTypeInductive BuiltinInductive
diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index 932b8398be..30082de5e5 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/src/Juvix/Compiler/Core/Evaluator.hs
@@ -187,6 +187,7 @@ geval opts herr ctx env0 = eval' env0
       OpSeq -> seqOp
       OpFail -> failOp
       OpTrace -> traceOp
+      OpAnomaGet -> err "unsupported op: OpAnomaGet"
       where
         err :: Text -> a
         err msg = evalError msg n
diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs
index e8479a8751..d89d747bbc 100644
--- a/src/Juvix/Compiler/Core/Extra/Utils.hs
+++ b/src/Juvix/Compiler/Core/Extra/Utils.hs
@@ -423,6 +423,7 @@ builtinOpArgTypes = \case
   OpSeq -> [mkDynamic', mkDynamic']
   OpTrace -> [mkDynamic']
   OpFail -> [mkTypeString']
+  OpAnomaGet -> [mkDynamic']
 
 translateCase :: (Node -> Node -> Node -> a) -> a -> Case -> a
 translateCase translateIfFun dflt Case {..} = case _caseBranches of
diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs
index 5df7f075fc..f4a9556619 100644
--- a/src/Juvix/Compiler/Core/Language/Builtins.hs
+++ b/src/Juvix/Compiler/Core/Language/Builtins.hs
@@ -26,6 +26,7 @@ data BuiltinOp
   | OpSeq
   | OpTrace
   | OpFail
+  | OpAnomaGet
   deriving stock (Eq, Generic)
 
 instance Serialize BuiltinOp
@@ -66,6 +67,7 @@ builtinOpArgsNum = \case
   OpSeq -> 2
   OpTrace -> 1
   OpFail -> 1
+  OpAnomaGet -> 1
 
 builtinConstrArgsNum :: BuiltinDataTag -> Int
 builtinConstrArgsNum = \case
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index f81018b08e..62a1caae91 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -52,6 +52,7 @@ instance PrettyCode BuiltinOp where
     OpSeq -> return primSeq
     OpTrace -> return primTrace
     OpFail -> return primFail
+    OpAnomaGet -> return primAnomaGet
 
 instance PrettyCode BuiltinDataTag where
   ppCode = \case
@@ -794,6 +795,9 @@ primSeq = primitive Str.seqq_
 primFail :: Doc Ann
 primFail = primitive Str.fail_
 
+primAnomaGet :: Doc Ann
+primAnomaGet = primitive Str.anomaGet
+
 primTrace :: Doc Ann
 primTrace = primitive Str.trace_
 
diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
index e7fd8c2812..ffb64429b6 100644
--- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
+++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
@@ -66,6 +66,7 @@ computeNodeTypeInfo md = umapL go
             [arg] -> Info.getNodeType arg
             _ -> error "incorrect trace builtin application"
           OpFail -> Info.getNodeType node
+          OpAnomaGet -> Info.getNodeType node
       NCtr Constr {..} ->
         let ci = lookupConstructorInfo md _constrTag
             ii = lookupInductiveInfo md (ci ^. constructorInductive)
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
index b355a49d8f..7aa39821d5 100644
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@@ -577,6 +577,7 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinFieldDiv -> return ()
       Internal.BuiltinFieldFromInt -> return ()
       Internal.BuiltinFieldToNat -> return ()
+      Internal.BuiltinAnomaGet -> return ()
 
     registerInductiveAxiom :: Maybe BuiltinAxiom -> [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> Sem r ()
     registerInductiveAxiom ax ctrs = do
@@ -685,6 +686,15 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
         intName <- getIntName
         intSym <- getIntSymbol
         registerAxiomDef $ writeLambda (mkTypeConstr (setInfoName intName mempty) intSym [])
+      Internal.BuiltinAnomaGet ->
+        registerAxiomDef
+          ( mkLambda'
+              mkSmallUniv
+              ( mkLambda'
+                  mkSmallUniv
+                  (mkLambda' (mkVar' 0) (mkBuiltinApp' OpAnomaGet [mkVar' 0]))
+              )
+          )
 
     axiomType' :: Sem r Type
     axiomType' = fromTopIndex (goType (a ^. Internal.axiomType))
@@ -1060,6 +1070,7 @@ goApplication a = do
             [x] -> return $ mkBuiltinApp' OpFieldFromInt [x]
             _ -> app
         Just Internal.BuiltinFieldToNat -> app
+        Just Internal.BuiltinAnomaGet -> app
         Nothing -> app
     Internal.ExpressionIden (Internal.IdenFunction n) -> do
       funInfoBuiltin <- Internal.getFunctionBuiltinInfo n
diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
index 96e34872d1..ecccaa562b 100644
--- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
+++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
@@ -93,6 +93,7 @@ fromCore fsize tab =
         BuiltinFail -> False
         BuiltinIntToString -> False
         BuiltinIntPrint -> False
+        BuiltinAnomaGet -> False
       BuiltinTypeInductive i -> case i of
         BuiltinList -> True
         BuiltinNat -> False
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index fd4a45ddf9..7feebb8a97 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -587,6 +587,7 @@ registerBuiltinAxiom d = \case
   BuiltinFail -> registerFail d
   BuiltinIntToString -> registerIntToString d
   BuiltinIntPrint -> registerIntPrint d
+  BuiltinAnomaGet -> registerAnomaGet d
 
 goInductive ::
   (Members '[Reader EntryPoint, Reader DefaultArgsStack, NameIdGen, Reader Pragmas, Builtins, Error ScoperError, State ConstructorInfos, Reader S.InfoTable] r) =>
diff --git a/src/Juvix/Compiler/Nockma/EvalCompiled.hs b/src/Juvix/Compiler/Nockma/EvalCompiled.hs
index e802712d52..52272ae7ae 100644
--- a/src/Juvix/Compiler/Nockma/EvalCompiled.hs
+++ b/src/Juvix/Compiler/Nockma/EvalCompiled.hs
@@ -10,6 +10,7 @@ evalCompiledNock' stack mainTerm = do
   evalT <-
     runError @(ErrNockNatural Natural)
       . runError @(NockEvalError Natural)
+      . runReader @(Storage Natural) emptyStorage
       $ eval stack mainTerm
   case evalT of
     Left e -> error (show e)
diff --git a/src/Juvix/Compiler/Nockma/Evaluator.hs b/src/Juvix/Compiler/Nockma/Evaluator.hs
index bd523c9820..59b57f8aed 100644
--- a/src/Juvix/Compiler/Nockma/Evaluator.hs
+++ b/src/Juvix/Compiler/Nockma/Evaluator.hs
@@ -2,11 +2,14 @@ module Juvix.Compiler.Nockma.Evaluator
   ( module Juvix.Compiler.Nockma.Evaluator,
     module Juvix.Compiler.Nockma.Evaluator.Error,
     module Juvix.Compiler.Nockma.Evaluator.Options,
+    module Juvix.Compiler.Nockma.Evaluator.Storage,
   )
 where
 
+import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Nockma.Evaluator.Error
 import Juvix.Compiler.Nockma.Evaluator.Options
+import Juvix.Compiler.Nockma.Evaluator.Storage
 import Juvix.Compiler.Nockma.Language
 import Juvix.Prelude hiding (Atom, Path)
 
@@ -102,7 +105,7 @@ programAssignments mprog =
 -- | The stack provided in the replExpression has priority
 evalRepl ::
   forall r a.
-  (Integral a, Members '[Reader EvalOptions, Error (NockEvalError a), Error (ErrNockNatural a)] r, NockNatural a) =>
+  (Hashable a, Integral a, Members '[Reader EvalOptions, Error (NockEvalError a), Error (ErrNockNatural a)] r, NockNatural a) =>
   (Term a -> Sem r ()) ->
   Maybe (Program a) ->
   Maybe (Term a) ->
@@ -115,7 +118,7 @@ evalRepl handleTrace mprog defaultStack expr = do
       t' <- fromReplTerm namedTerms (w ^. withStackStack)
       return (Just t', w ^. withStackTerm)
   stack <- maybe errNoStack return mstack
-  fromReplTerm namedTerms t >>= runOutputSem @(Term a) handleTrace . eval stack
+  fromReplTerm namedTerms t >>= runOutputSem @(Term a) handleTrace . runReader @(Storage a) emptyStorage . eval stack
   where
     errNoStack :: Sem r x
     errNoStack = throw @(NockEvalError a) (ErrNoStack NoStack)
@@ -125,7 +128,7 @@ evalRepl handleTrace mprog defaultStack expr = do
 
 eval ::
   forall s a.
-  (Integral a, Members '[Reader EvalOptions, Output (Term a), Error (NockEvalError a), Error (ErrNockNatural a)] s, NockNatural a) =>
+  (Hashable a, Integral a, Members '[Reader (Storage a), Reader EvalOptions, Output (Term a), Error (NockEvalError a), Error (ErrNockNatural a)] s, NockNatural a) =>
   Term a ->
   Term a ->
   Sem s (Term a)
@@ -210,6 +213,7 @@ eval inistack initerm =
           OpCall -> goOpCall
           OpReplace -> goOpReplace
           OpHint -> goOpHint
+          OpScry -> goOpScry
           OpTrace -> goOpTrace
           where
             crumb crumbTag =
@@ -317,3 +321,10 @@ eval inistack initerm =
               cellTerm <- withCrumb (crumb crumbDecodeFirst) (asCell (c ^. operatorCellTerm))
               t1' <- evalArg crumbEvalFirst stack (cellTerm ^. cellLeft)
               evalArg crumbEvalSecond t1' (cellTerm ^. cellRight)
+
+            goOpScry :: Sem r (Term a)
+            goOpScry = do
+              Cell' typeFormula subFormula _ <- withCrumb (crumb crumbDecodeFirst) (asCell (c ^. operatorCellTerm))
+              void (evalArg crumbEvalFirst stack typeFormula)
+              key <- evalArg crumbEvalSecond stack subFormula
+              fromMaybeM (throwKeyNotInStorage key) (HashMap.lookup key <$> asks (^. storageKeyValueData))
diff --git a/src/Juvix/Compiler/Nockma/Evaluator/Error.hs b/src/Juvix/Compiler/Nockma/Evaluator/Error.hs
index c0f80bd26d..77689ae0e7 100644
--- a/src/Juvix/Compiler/Nockma/Evaluator/Error.hs
+++ b/src/Juvix/Compiler/Nockma/Evaluator/Error.hs
@@ -1,10 +1,13 @@
 module Juvix.Compiler.Nockma.Evaluator.Error
   ( module Juvix.Compiler.Nockma.Evaluator.Error,
     module Juvix.Compiler.Nockma.Evaluator.Crumbs,
+    module Juvix.Compiler.Nockma.Evaluator.Storage,
   )
 where
 
+import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Nockma.Evaluator.Crumbs
+import Juvix.Compiler.Nockma.Evaluator.Storage
 import Juvix.Compiler.Nockma.Language
 import Juvix.Compiler.Nockma.Pretty.Base
 import Juvix.Prelude hiding (Atom, Path)
@@ -17,6 +20,7 @@ data NockEvalError a
     ErrNoStack NoStack
   | -- TODO perhaps this should be a repl error type
     ErrAssignmentNotFound Text
+  | ErrKeyNotInStorage (KeyNotInStorage a)
 
 newtype GenericNockEvalError = GenericNockEvalError
   { _genericNockEvalErrorMessage :: AnsiText
@@ -41,6 +45,11 @@ data InvalidPath a = InvalidPath
     _invalidPathPath :: Path
   }
 
+data KeyNotInStorage a = KeyNotInStorage
+  { _keyNotInStorageKey :: Term a,
+    _keyNotInStorageStorage :: Storage a
+  }
+
 data NoStack = NoStack
 
 throwInvalidPath :: (Members '[Error (NockEvalError a), Reader EvalCtx] r) => Term a -> Path -> Sem r x
@@ -74,6 +83,16 @@ throwExpectedAtom a = do
           _expectedAtomCell = a
         }
 
+throwKeyNotInStorage :: (Members '[Reader (Storage a), Error (NockEvalError a)] r) => Term a -> Sem r x
+throwKeyNotInStorage k = do
+  s <- ask
+  throw $
+    ErrKeyNotInStorage
+      KeyNotInStorage
+        { _keyNotInStorageKey = k,
+          _keyNotInStorageStorage = s
+        }
+
 instance PrettyCode NoStack where
   ppCode _ = return "Missing stack"
 
@@ -98,6 +117,19 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (ExpectedCell a) where
     let cell = annotate AnnImportant "cell"
     return (ctx <> "Expected a" <+> cell <+> "but got:" <> line <> atm)
 
+instance (PrettyCode a, NockNatural a) => PrettyCode (KeyNotInStorage a) where
+  ppCode :: forall r. (Member (Reader Options) r) => KeyNotInStorage a -> Sem r (Doc Ann)
+  ppCode KeyNotInStorage {..} = do
+    tm <- ppCode _keyNotInStorageKey
+    hashMapKvs <- vsep <$> mapM combineKeyValue (HashMap.toList (_keyNotInStorageStorage ^. storageKeyValueData))
+    return ("The key" <+> tm <+> "is not found in the storage." <> line <> "Storage contains the following key value pairs:" <> line <> hashMapKvs)
+    where
+      combineKeyValue :: (Term a, Term a) -> Sem r (Doc Ann)
+      combineKeyValue (t1, t2) = do
+        pt1 <- ppCode t1
+        pt2 <- ppCode t2
+        return (pt1 <+> ":=" <+> pt2)
+
 instance (PrettyCode a, NockNatural a) => PrettyCode (NockEvalError a) where
   ppCode = \case
     ErrInvalidPath e -> ppCode e
@@ -105,3 +137,4 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (NockEvalError a) where
     ErrExpectedCell e -> ppCode e
     ErrNoStack e -> ppCode e
     ErrAssignmentNotFound e -> return (pretty e)
+    ErrKeyNotInStorage e -> ppCode e
diff --git a/src/Juvix/Compiler/Nockma/Evaluator/Storage.hs b/src/Juvix/Compiler/Nockma/Evaluator/Storage.hs
new file mode 100644
index 0000000000..57b5505205
--- /dev/null
+++ b/src/Juvix/Compiler/Nockma/Evaluator/Storage.hs
@@ -0,0 +1,12 @@
+module Juvix.Compiler.Nockma.Evaluator.Storage where
+
+import Juvix.Compiler.Nockma.Language
+import Juvix.Prelude.Base
+
+newtype Storage a = Storage
+  {_storageKeyValueData :: HashMap (Term a) (Term a)}
+
+emptyStorage :: (Hashable a) => Storage a
+emptyStorage = Storage {_storageKeyValueData = mempty}
+
+makeLenses ''Storage
diff --git a/src/Juvix/Compiler/Nockma/Language.hs b/src/Juvix/Compiler/Nockma/Language.hs
index f078105260..d80c3eb1a5 100644
--- a/src/Juvix/Compiler/Nockma/Language.hs
+++ b/src/Juvix/Compiler/Nockma/Language.hs
@@ -47,38 +47,50 @@ data Assignment a = Assignment
 data Term a
   = TermAtom (Atom a)
   | TermCell (Cell a)
-  deriving stock (Show, Eq, Lift)
+  deriving stock (Show, Eq, Lift, Generic)
+
+instance (Hashable a) => Hashable (Term a)
 
 data StdlibCall a = StdlibCall
   { _stdlibCallFunction :: StdlibFunction,
     _stdlibCallArgs :: Term a
   }
-  deriving stock (Show, Eq, Lift)
+  deriving stock (Show, Eq, Lift, Generic)
+
+instance (Hashable a) => Hashable (StdlibCall a)
 
 data CellInfo a = CellInfo
   { _cellInfoLoc :: Irrelevant (Maybe Interval),
     _cellInfoCall :: Maybe (StdlibCall a)
   }
-  deriving stock (Show, Eq, Lift)
+  deriving stock (Show, Eq, Lift, Generic)
+
+instance (Hashable a) => Hashable (CellInfo a)
 
 data Cell a = Cell'
   { _cellLeft :: Term a,
     _cellRight :: Term a,
     _cellInfo :: CellInfo a
   }
-  deriving stock (Show, Eq, Lift)
+  deriving stock (Show, Eq, Lift, Generic)
+
+instance (Hashable a) => Hashable (Cell a)
 
 data AtomInfo = AtomInfo
   { _atomInfoHint :: Maybe AtomHint,
     _atomInfoLoc :: Irrelevant (Maybe Interval)
   }
-  deriving stock (Show, Eq, Lift)
+  deriving stock (Show, Eq, Lift, Generic)
+
+instance Hashable AtomInfo
 
 data Atom a = Atom
   { _atom :: a,
     _atomInfo :: AtomInfo
   }
-  deriving stock (Show, Eq, Lift)
+  deriving stock (Show, Eq, Lift, Generic)
+
+instance (Hashable a) => Hashable (Atom a)
 
 data AtomHint
   = AtomHintOp
@@ -86,7 +98,9 @@ data AtomHint
   | AtomHintBool
   | AtomHintNil
   | AtomHintVoid
-  deriving stock (Show, Eq, Lift)
+  deriving stock (Show, Eq, Lift, Generic)
+
+instance Hashable AtomHint
 
 data NockOp
   = OpAddress
@@ -101,6 +115,7 @@ data NockOp
   | OpCall
   | OpReplace
   | OpHint
+  | OpScry
   | OpTrace
   deriving stock (Bounded, Enum, Eq, Generic)
 
@@ -120,6 +135,7 @@ instance Pretty NockOp where
     OpCall -> "call"
     OpReplace -> "replace"
     OpHint -> "hint"
+    OpScry -> "scry"
     OpTrace -> "trace"
 
 textToStdlibFunctionMap :: HashMap Text StdlibFunction
@@ -214,6 +230,7 @@ serializeOp = \case
   OpCall -> 9
   OpReplace -> 10
   OpHint -> 11
+  OpScry -> 12
   OpTrace -> 100
 
 class (NockmaEq a) => NockNatural a where
diff --git a/src/Juvix/Compiler/Nockma/StdlibFunction/Base.hs b/src/Juvix/Compiler/Nockma/StdlibFunction/Base.hs
index e07905059f..311f9b3813 100644
--- a/src/Juvix/Compiler/Nockma/StdlibFunction/Base.hs
+++ b/src/Juvix/Compiler/Nockma/StdlibFunction/Base.hs
@@ -25,4 +25,6 @@ data StdlibFunction
   | StdlibLt
   | StdlibLe
   | StdlibPow2
-  deriving stock (Show, Lift, Eq, Bounded, Enum)
+  deriving stock (Show, Lift, Eq, Bounded, Enum, Generic)
+
+instance Hashable StdlibFunction
diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
index fe6d35dddc..8dc11b65e0 100644
--- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
+++ b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
@@ -360,6 +360,7 @@ compile = \case
         Tree.PrimUnop op -> return $ goPrimUnop op arg
         Tree.OpFail -> return crash
         Tree.OpTrace -> goTrace arg
+        Tree.OpAnomaGet -> goAnomaGet arg
 
     goPrimUnop :: Tree.UnaryOp -> Term Natural -> Term Natural
     goPrimUnop op arg = case op of
@@ -371,6 +372,9 @@ compile = \case
       Tree.OpIntToField -> fieldErr
       Tree.OpFieldToInt -> fieldErr
 
+    goAnomaGet :: Term Natural -> Sem r (Term Natural)
+    goAnomaGet arg = return (OpScry # (OpQuote # nockNil') # arg)
+
     goTrace :: Term Natural -> Sem r (Term Natural)
     goTrace arg = do
       enabled <- asks (^. compilerOptions . compilerOptionsEnableTrace)
diff --git a/src/Juvix/Compiler/Tree/Data/TransformationId.hs b/src/Juvix/Compiler/Tree/Data/TransformationId.hs
index afbe62c2e7..93f8c22beb 100644
--- a/src/Juvix/Compiler/Tree/Data/TransformationId.hs
+++ b/src/Juvix/Compiler/Tree/Data/TransformationId.hs
@@ -12,6 +12,7 @@ data TransformationId
   | TempHeight
   | FilterUnreachable
   | Validate
+  | CheckNoAnoma
   deriving stock (Data, Bounded, Enum, Show)
 
 data PipelineId
@@ -26,7 +27,7 @@ toNockmaTransformations :: [TransformationId]
 toNockmaTransformations = [Validate, Apply, FilterUnreachable, TempHeight]
 
 toAsmTransformations :: [TransformationId]
-toAsmTransformations = [Validate]
+toAsmTransformations = [Validate, CheckNoAnoma]
 
 toCairoAsmTransformations :: [TransformationId]
 toCairoAsmTransformations = [Validate, Apply, FilterUnreachable]
@@ -41,6 +42,7 @@ instance TransformationId' TransformationId where
     TempHeight -> strTempHeight
     FilterUnreachable -> strFilterUnreachable
     Validate -> strValidate
+    CheckNoAnoma -> strCheckNoAnoma
 
 instance PipelineId' TransformationId PipelineId where
   pipelineText :: PipelineId -> Text
diff --git a/src/Juvix/Compiler/Tree/Data/TransformationId/Strings.hs b/src/Juvix/Compiler/Tree/Data/TransformationId/Strings.hs
index 1e8aa131ff..ababa4da2f 100644
--- a/src/Juvix/Compiler/Tree/Data/TransformationId/Strings.hs
+++ b/src/Juvix/Compiler/Tree/Data/TransformationId/Strings.hs
@@ -31,3 +31,6 @@ strFilterUnreachable = "filter-unreachable"
 
 strValidate :: Text
 strValidate = "validate"
+
+strCheckNoAnoma :: Text
+strCheckNoAnoma = "check-no-anoma"
diff --git a/src/Juvix/Compiler/Tree/Evaluator.hs b/src/Juvix/Compiler/Tree/Evaluator.hs
index 97080ae1b5..e349027ad8 100644
--- a/src/Juvix/Compiler/Tree/Evaluator.hs
+++ b/src/Juvix/Compiler/Tree/Evaluator.hs
@@ -73,6 +73,7 @@ hEval hout tab = eval' [] mempty
                 PrimUnop op -> eitherToError $ evalUnop tab op v
                 OpTrace -> goTrace v
                 OpFail -> goFail v
+                OpAnomaGet -> evalError "Unsupported op: OpAnomaGet"
 
         goFail :: Value -> Value
         goFail v = evalError ("failure: " <> printValue tab v)
diff --git a/src/Juvix/Compiler/Tree/EvaluatorEff.hs b/src/Juvix/Compiler/Tree/EvaluatorEff.hs
index 03a25519b7..f8562d43d0 100644
--- a/src/Juvix/Compiler/Tree/EvaluatorEff.hs
+++ b/src/Juvix/Compiler/Tree/EvaluatorEff.hs
@@ -68,6 +68,7 @@ eval tab = runReader emptyEvalCtx . eval'
             PrimUnop op -> eitherToError $ evalUnop tab op v
             OpTrace -> goTrace v
             OpFail -> goFail v
+            OpAnomaGet -> evalError "Unsupported op: OpAnomaGet"
 
         goFail :: Value -> Sem r' Value
         goFail v = evalError ("failure: " <> printValue tab v)
diff --git a/src/Juvix/Compiler/Tree/Keywords.hs b/src/Juvix/Compiler/Tree/Keywords.hs
index f965bd6aa7..900df036b8 100644
--- a/src/Juvix/Compiler/Tree/Keywords.hs
+++ b/src/Juvix/Compiler/Tree/Keywords.hs
@@ -9,6 +9,7 @@ import Juvix.Compiler.Tree.Keywords.Base
 import Juvix.Data.Keyword.All
   ( kwAdd_,
     kwAlloc,
+    kwAnomaGet,
     kwArgsNum,
     kwAtoi,
     kwBr,
@@ -68,5 +69,6 @@ allKeywords =
          kwCCall,
          kwBr,
          kwCase,
-         kwSave
+         kwSave,
+         kwAnomaGet
        ]
diff --git a/src/Juvix/Compiler/Tree/Language.hs b/src/Juvix/Compiler/Tree/Language.hs
index 94a7bf65eb..7516afa1f2 100644
--- a/src/Juvix/Compiler/Tree/Language.hs
+++ b/src/Juvix/Compiler/Tree/Language.hs
@@ -66,6 +66,8 @@ data UnaryOpcode
     OpTrace
   | -- | Interrupt execution with a runtime error printing the argument.
     OpFail
+  | -- | Get a value by key from Anoma storage
+    OpAnomaGet
 
 data NodeBinop = NodeBinop
   { _nodeBinopInfo :: NodeInfo,
diff --git a/src/Juvix/Compiler/Tree/Pretty/Base.hs b/src/Juvix/Compiler/Tree/Pretty/Base.hs
index a0d102502d..9e143f6194 100644
--- a/src/Juvix/Compiler/Tree/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Tree/Pretty/Base.hs
@@ -239,6 +239,7 @@ instance PrettyCode UnaryOpcode where
     PrimUnop x -> ppCode x
     OpTrace -> return $ primitive Str.instrTrace
     OpFail -> return $ primitive Str.instrFailure
+    OpAnomaGet -> return $ primitive Str.anomaGet
 
 instance PrettyCode NodeUnop where
   ppCode NodeUnop {..} = do
diff --git a/src/Juvix/Compiler/Tree/Transformation.hs b/src/Juvix/Compiler/Tree/Transformation.hs
index 7f58941f89..a1876de891 100644
--- a/src/Juvix/Compiler/Tree/Transformation.hs
+++ b/src/Juvix/Compiler/Tree/Transformation.hs
@@ -10,6 +10,7 @@ import Juvix.Compiler.Tree.Data.TransformationId
 import Juvix.Compiler.Tree.Error
 import Juvix.Compiler.Tree.Transformation.Apply
 import Juvix.Compiler.Tree.Transformation.Base
+import Juvix.Compiler.Tree.Transformation.CheckNoAnoma
 import Juvix.Compiler.Tree.Transformation.FilterUnreachable
 import Juvix.Compiler.Tree.Transformation.Identity
 import Juvix.Compiler.Tree.Transformation.TempHeight
@@ -27,3 +28,4 @@ applyTransformations ts tbl = foldM (flip appTrans) tbl ts
       TempHeight -> return . computeTempHeight
       FilterUnreachable -> return . filterUnreachable
       Validate -> mapError (JuvixError @TreeError) . validate
+      CheckNoAnoma -> \tbl' -> mapError (JuvixError @TreeError) (checkNoAnoma tbl') $> tbl'
diff --git a/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs b/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs
new file mode 100644
index 0000000000..21b6d424c6
--- /dev/null
+++ b/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs
@@ -0,0 +1,23 @@
+module Juvix.Compiler.Tree.Transformation.CheckNoAnoma where
+
+import Juvix.Compiler.Tree.Data.InfoTable
+import Juvix.Compiler.Tree.Error
+import Juvix.Compiler.Tree.Extra.Recursors
+import Juvix.Compiler.Tree.Transformation.Base
+
+checkNoAnoma :: forall r. (Member (Error TreeError) r) => InfoTable -> Sem r ()
+checkNoAnoma = walkT checkNode
+  where
+    checkNode :: Symbol -> Node -> Sem r ()
+    checkNode _ = \case
+      Unop NodeUnop {..} -> case _nodeUnopOpcode of
+        OpAnomaGet ->
+          throw
+            TreeError
+              { _treeErrorMsg = "OpAnomaGet is unsupported",
+                _treeErrorLoc = _nodeUnopInfo ^. nodeInfoLocation
+              }
+        OpFail -> return ()
+        OpTrace -> return ()
+        PrimUnop {} -> return ()
+      _ -> return ()
diff --git a/src/Juvix/Compiler/Tree/Transformation/Validate.hs b/src/Juvix/Compiler/Tree/Transformation/Validate.hs
index 62f99bb7e1..ca95afe38b 100644
--- a/src/Juvix/Compiler/Tree/Transformation/Validate.hs
+++ b/src/Juvix/Compiler/Tree/Transformation/Validate.hs
@@ -64,6 +64,7 @@ inferType tab funInfo = goInfer mempty
       PrimUnop x -> checkPrimUnop x
       OpTrace -> goInfer bl _nodeUnopArg
       OpFail -> checkUnop TyDynamic TyDynamic
+      OpAnomaGet -> checkUnop TyDynamic TyDynamic
       where
         loc = _nodeUnopInfo ^. nodeInfoLocation
 
diff --git a/src/Juvix/Compiler/Tree/Translation/FromCore.hs b/src/Juvix/Compiler/Tree/Translation/FromCore.hs
index 8488ab30ca..220f1f7ff5 100644
--- a/src/Juvix/Compiler/Tree/Translation/FromCore.hs
+++ b/src/Juvix/Compiler/Tree/Translation/FromCore.hs
@@ -288,6 +288,7 @@ genCode infoTable fi =
       Core.OpFieldToInt -> PrimUnop OpFieldToInt
       Core.OpTrace -> OpTrace
       Core.OpFail -> OpFail
+      Core.OpAnomaGet -> OpAnomaGet
       _ -> impossible
 
     getArgsNum :: Symbol -> Int
diff --git a/src/Juvix/Compiler/Tree/Translation/FromSource.hs b/src/Juvix/Compiler/Tree/Translation/FromSource.hs
index ee11a5d802..199e6f57b7 100644
--- a/src/Juvix/Compiler/Tree/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Tree/Translation/FromSource.hs
@@ -106,6 +106,7 @@ parseUnop =
     <|> parseUnaryOp kwTrace OpTrace
     <|> parseUnaryOp kwFail OpFail
     <|> parseUnaryOp kwArgsNum (PrimUnop OpArgsNum)
+    <|> parseUnaryOp kwAnomaGet (OpAnomaGet)
 
 parseUnaryOp ::
   (Members '[Reader ParserSig, InfoTableBuilder, State LocalParams] r) =>
diff --git a/src/Juvix/Data/Irrelevant.hs b/src/Juvix/Data/Irrelevant.hs
index 8b7c948b1e..f859e2739b 100644
--- a/src/Juvix/Data/Irrelevant.hs
+++ b/src/Juvix/Data/Irrelevant.hs
@@ -45,4 +45,7 @@ instance Applicative Irrelevant where
 instance Monad Irrelevant where
   (Irrelevant mx) >>= f = f mx
 
+instance Hashable (Irrelevant a) where
+  hashWithSalt _ _ = 0
+
 makeLenses ''Irrelevant
diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs
index c8df62273a..9e7a7b7fde 100644
--- a/src/Juvix/Data/Keyword/All.hs
+++ b/src/Juvix/Data/Keyword/All.hs
@@ -433,6 +433,9 @@ kwRet = asciiKw Str.ret
 kwLive :: Keyword
 kwLive = asciiKw Str.live
 
+kwAnomaGet :: Keyword
+kwAnomaGet = asciiKw Str.anomaGet
+
 delimBraceL :: Keyword
 delimBraceL = mkDelim Str.braceL
 
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index 295f595820..c7a2c1b3a9 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@@ -308,6 +308,9 @@ fromInt = "from-int"
 intPrint :: (IsString s) => s
 intPrint = "int-print"
 
+anomaGet :: (IsString s) => s
+anomaGet = "anoma-get"
+
 builtinSeq :: (IsString s) => s
 builtinSeq = "seq"
 
diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs
index b27f42717f..17e8a922f6 100644
--- a/test/Anoma/Compilation/Positive.hs
+++ b/test/Anoma/Compilation/Positive.hs
@@ -1,6 +1,7 @@
 module Anoma.Compilation.Positive where
 
 import Base
+import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Backend (Target (TargetAnoma))
 import Juvix.Compiler.Nockma.Evaluator
 import Juvix.Compiler.Nockma.Language
@@ -14,8 +15,8 @@ import Nockma.Eval.Positive
 root :: Prelude.Path Abs Dir
 root = relToProject $(mkRelDir "tests/Anoma/Compilation/positive")
 
-mkAnomaCallTest' :: Bool -> Text -> Prelude.Path Rel Dir -> Prelude.Path Rel File -> [Term Natural] -> Check () -> TestTree
-mkAnomaCallTest' enableDebug _testName relRoot mainFile args _testCheck =
+mkAnomaCallTest' :: Bool -> Storage Natural -> Text -> Prelude.Path Rel Dir -> Prelude.Path Rel File -> [Term Natural] -> Check () -> TestTree
+mkAnomaCallTest' enableDebug _testProgramStorage _testName relRoot mainFile args _testCheck =
   testCase (unpack _testName) (mkTestIO >>= mkNockmaAssertion)
   where
     mkTestIO :: IO Test
@@ -27,6 +28,7 @@ mkAnomaCallTest' enableDebug _testName relRoot mainFile args _testCheck =
         return compiledMain
       let _testProgramFormula = anomaCall args
           _testEvalOptions = defaultEvalOptions
+          _testAssertEvalError :: Maybe (NockEvalError Natural -> Assertion) = Nothing
       return Test {..}
 
     withRootCopy :: (Prelude.Path Abs Dir -> IO a) -> IO a
@@ -43,10 +45,10 @@ mkAnomaCallTest' enableDebug _testName relRoot mainFile args _testCheck =
       (^. pipelineResult) . snd <$> testRunIO entryPoint upToAnoma
 
 mkAnomaCallTestNoTrace :: Text -> Prelude.Path Rel Dir -> Prelude.Path Rel File -> [Term Natural] -> Check () -> TestTree
-mkAnomaCallTestNoTrace = mkAnomaCallTest' False
+mkAnomaCallTestNoTrace = mkAnomaCallTest' False emptyStorage
 
 mkAnomaCallTest :: Text -> Prelude.Path Rel Dir -> Prelude.Path Rel File -> [Term Natural] -> Check () -> TestTree
-mkAnomaCallTest = mkAnomaCallTest' True
+mkAnomaCallTest = mkAnomaCallTest' True emptyStorage
 
 checkNatOutput :: [Natural] -> Check ()
 checkNatOutput = checkOutput . fmap toNock
@@ -523,5 +525,23 @@ allTests =
         $(mkRelDir "test073")
         $(mkRelFile "test073.juvix")
         []
-        $ checkNatOutput [11]
+        $ checkNatOutput [11],
+      let k1 :: Term Natural = [nock| 333 |]
+          v1 :: Term Natural = [nock| 222 |]
+          k2 :: Term Natural = [nock| [1 2 3 nil] |]
+          v2 :: Term Natural = [nock| [4 5 6 nil] |]
+       in mkAnomaCallTest'
+            True
+            ( Storage
+                ( HashMap.fromList
+                    [ (k1, v1),
+                      (k2, v2)
+                    ]
+                )
+            )
+            "Test074: Builtin anomaGet"
+            $(mkRelDir ".")
+            $(mkRelFile "test074.juvix")
+            [OpQuote # k1, OpQuote # k2]
+            $ checkOutput [v1, v2]
     ]
diff --git a/test/Compilation/Base.hs b/test/Compilation/Base.hs
index 5c673efab1..5cc0270046 100644
--- a/test/Compilation/Base.hs
+++ b/test/Compilation/Base.hs
@@ -51,6 +51,9 @@ compileErrorAssertion root' mainFile step = do
   step "Translate to JuvixCore"
   entryPoint <- testDefaultEntryPointIO root' mainFile
   PipelineResult {..} <- snd <$> testRunIO entryPoint upToCore
-  case run $ runReader Core.defaultCoreOptions $ runError @JuvixError $ Core.toStored' (_pipelineResult ^. Core.coreResultModule) >>= Core.toStripped' Core.CheckExec of
+  case run
+    . runReader Core.defaultCoreOptions
+    . runError @JuvixError
+    $ Core.toStored' (_pipelineResult ^. Core.coreResultModule) >>= Core.toStripped' Core.CheckExec of
     Left _ -> assertBool "" True
     Right _ -> assertFailure "no error"
diff --git a/test/Nockma/Eval/Positive.hs b/test/Nockma/Eval/Positive.hs
index a493af0e1d..f0402a68df 100644
--- a/test/Nockma/Eval/Positive.hs
+++ b/test/Nockma/Eval/Positive.hs
@@ -1,6 +1,7 @@
 module Nockma.Eval.Positive where
 
 import Base hiding (Path, testName)
+import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Core.Language.Base (defaultSymbol)
 import Juvix.Compiler.Nockma.Evaluator
 import Juvix.Compiler.Nockma.Language
@@ -13,6 +14,8 @@ type Check = Sem '[Reader [Term Natural], Reader (Term Natural), EmbedIO]
 
 data Test = Test
   { _testEvalOptions :: EvalOptions,
+    _testAssertEvalError :: Maybe (NockEvalError Natural -> Assertion),
+    _testProgramStorage :: Storage Natural,
     _testName :: Text,
     _testProgramSubject :: Term Natural,
     _testProgramFormula :: Term Natural,
@@ -29,13 +32,18 @@ mkNockmaAssertion Test {..} = do
           . runOutputList @(Term Natural)
           . runError @(ErrNockNatural Natural)
           . runError @(NockEvalError Natural)
+          . runReader @(Storage Natural) _testProgramStorage
           $ eval _testProgramSubject _testProgramFormula
 
   case evalResult of
     Left natErr -> assertFailure ("Evaluation error: " <> show natErr)
-    Right r -> case r of
-      Left evalErr -> assertFailure ("Evaluation error: " <> unpack (ppTrace evalErr))
-      Right res -> runM (runReader res (runReader traces _testCheck))
+    Right r -> case _testAssertEvalError of
+      Nothing -> case r of
+        Left evalErr -> assertFailure ("Evaluation error: " <> unpack (ppTrace evalErr))
+        Right res -> runM (runReader res (runReader traces _testCheck))
+      Just checkErrFn -> case r of
+        Left evalErr -> checkErrFn evalErr
+        Right {} -> assertFailure "expected error"
 
 allTests :: TestTree
 allTests =
@@ -91,8 +99,20 @@ compilerTest n mainFun _testCheck _evalInterceptStdlibCalls =
       opts = CompilerOptions {_compilerOptionsEnableTrace = False}
       Cell _testProgramSubject _testProgramFormula = runCompilerWithJuvix opts mempty [] f
       _testEvalOptions = EvalOptions {..}
+      _testProgramStorage :: Storage Natural = emptyStorage
+      _testAssertEvalError :: Maybe (NockEvalError Natural -> Assertion) = Nothing
    in Test {..}
 
+withAssertErrKeyNotInStorage :: Test -> Test
+withAssertErrKeyNotInStorage Test {..} =
+  let _testAssertEvalError :: Maybe (NockEvalError Natural -> Assertion) = Just f
+   in Test {..}
+  where
+    f :: NockEvalError Natural -> Assertion
+    f = \case
+      ErrKeyNotInStorage {} -> return ()
+      _ -> assertFailure "Expected ErrKeyNotInStorage error"
+
 anomaTest :: Text -> Term Natural -> [Term Natural] -> Check () -> Bool -> Test
 anomaTest n mainFun args _testCheck _evalInterceptStdlibCalls =
   let f =
@@ -110,11 +130,16 @@ anomaTest n mainFun args _testCheck _evalInterceptStdlibCalls =
       _testProgramSubject = TermCell (runCompilerWithAnoma opts mempty [] f)
 
       _testProgramFormula = anomaCall args
+      _testProgramStorage :: Storage Natural = emptyStorage
       _testEvalOptions = EvalOptions {..}
+      _testAssertEvalError :: Maybe (NockEvalError Natural -> Assertion) = Nothing
    in Test {..}
 
+testWithStorage :: [(Term Natural, Term Natural)] -> Text -> Term Natural -> Term Natural -> Check () -> Test
+testWithStorage s = Test defaultEvalOptions Nothing (Storage (HashMap.fromList s))
+
 test :: Text -> Term Natural -> Term Natural -> Check () -> Test
-test = Test defaultEvalOptions
+test = testWithStorage []
 
 anomaCallingConventionTests :: [Test]
 anomaCallingConventionTests =
@@ -158,5 +183,7 @@ unitTests =
     test "push" [nock| [0 1] |] [nock| [push [[suc [@ L]] [@ S]]] |] (eqNock [nock| [1 0 1] |]),
     test "call" [nock| [quote 1] |] [nock| [call [S [@ S]]] |] (eqNock [nock| 1 |]),
     test "replace" [nock| [0 1] |] [nock| [replace [[L [quote 1]] [@ S]]] |] (eqNock [nock| [1 1] |]),
-    test "hint" [nock| [0 1] |] [nock| [hint [nil [trace [quote 2] [quote 3]]] [quote 1]] |] (eqTraces [[nock| 2 |]] >> eqNock [nock| 1 |])
+    test "hint" [nock| [0 1] |] [nock| [hint [nil [trace [quote 2] [quote 3]]] [quote 1]] |] (eqTraces [[nock| 2 |]] >> eqNock [nock| 1 |]),
+    testWithStorage [([nock| 111 |], [nock| 222 |])] "scry" [nock| nil |] [nock| [scry [quote nil] [quote 111]] |] (eqNock [nock| 222 |]),
+    withAssertErrKeyNotInStorage $ testWithStorage [([nock| 333 |], [nock| 222 |]), ([nock| 3 |], [nock| 222 |])] "scry" [nock| nil |] [nock| [scry [quote nil] [quote 111]] |] (eqNock [nock| 222 |])
   ]
diff --git a/test/Tree/Transformation.hs b/test/Tree/Transformation.hs
index cf252bcb94..03147269e8 100644
--- a/test/Tree/Transformation.hs
+++ b/test/Tree/Transformation.hs
@@ -2,6 +2,7 @@ module Tree.Transformation where
 
 import Base
 import Tree.Transformation.Apply qualified as Apply
+import Tree.Transformation.CheckNoAnoma qualified as CheckNoAnoma
 import Tree.Transformation.Identity qualified as Identity
 import Tree.Transformation.Reachability qualified as Reachability
 
@@ -11,5 +12,6 @@ allTests =
     "JuvixTree transformations"
     [ Identity.allTests,
       Apply.allTests,
-      Reachability.allTests
+      Reachability.allTests,
+      CheckNoAnoma.allTests
     ]
diff --git a/test/Tree/Transformation/CheckNoAnoma.hs b/test/Tree/Transformation/CheckNoAnoma.hs
new file mode 100644
index 0000000000..032ae515b0
--- /dev/null
+++ b/test/Tree/Transformation/CheckNoAnoma.hs
@@ -0,0 +1,67 @@
+module Tree.Transformation.CheckNoAnoma where
+
+import Base
+import Juvix.Compiler.Tree.Error
+import Juvix.Compiler.Tree.Transformation as Tree
+import Juvix.Compiler.Tree.Translation.FromSource
+import Juvix.Data.PPOutput
+import Tree.Eval.Negative qualified as Eval
+
+data CheckNoAnomaTest = CheckNoAnomaTest
+  { _testEval :: Eval.NegTest
+  }
+
+fromTest :: CheckNoAnomaTest -> TestTree
+fromTest = mkTest . toTestDescr
+
+root :: Path Abs Dir
+root = relToProject $(mkRelDir "tests/Tree/negative/")
+
+treeEvalTransformationErrorAssertion ::
+  Path Abs File ->
+  [TransformationId] ->
+  (JuvixError -> IO ()) ->
+  (String -> IO ()) ->
+  Assertion
+treeEvalTransformationErrorAssertion mainFile trans checkError step = do
+  step "Parse"
+  s <- readFile mainFile
+  case runParser mainFile s of
+    Left err -> assertFailure (show (pretty err))
+    Right tab0 -> do
+      step "Validate"
+      case run $ runError @JuvixError $ applyTransformations [Validate] tab0 of
+        Left err -> assertFailure (show (pretty (fromJuvixError @GenericError err)))
+        Right tab1 -> do
+          unless (null trans) $
+            step "Transform"
+          case run $ runError @JuvixError $ applyTransformations trans tab1 of
+            Left e -> checkError e
+            Right {} -> assertFailure "Expected error"
+
+toTestDescr :: CheckNoAnomaTest -> TestDescr
+toTestDescr CheckNoAnomaTest {..} =
+  let Eval.NegTest {..} = _testEval
+      tRoot = root <//> _relDir
+      file' = tRoot <//> _file
+      checkError :: JuvixError -> IO ()
+      checkError e =
+        unless
+          (isJust (fromJuvixError @TreeError e))
+          (assertFailure (unpack ("Expected TreeError. got: " <> renderTextDefault e)))
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Steps $ treeEvalTransformationErrorAssertion file' [CheckNoAnoma] checkError
+        }
+
+allTests :: TestTree
+allTests = testGroup "CheckNoAnoma" (map (fromTest . CheckNoAnomaTest) tests)
+
+tests :: [Eval.NegTest]
+tests =
+  [ Eval.NegTest
+      "anomaGet"
+      $(mkRelDir ".")
+      $(mkRelFile "test009.jvt")
+  ]
diff --git a/tests/Anoma/Compilation/positive/test074.juvix b/tests/Anoma/Compilation/positive/test074.juvix
new file mode 100644
index 0000000000..a70294efe2
--- /dev/null
+++ b/tests/Anoma/Compilation/positive/test074.juvix
@@ -0,0 +1,10 @@
+module test074;
+
+import Stdlib.Prelude open;
+import Stdlib.Debug.Trace open;
+
+builtin anoma-get
+axiom anomaGet : {Value Key : Type} -> Key -> Value;
+
+main (k1 : Nat) (k2 : List Nat) : List Nat :=
+  trace (anomaGet {Nat} k1) >>> anomaGet k2;
diff --git a/tests/Tree/negative/test009.jvt b/tests/Tree/negative/test009.jvt
new file mode 100644
index 0000000000..39e5008270
--- /dev/null
+++ b/tests/Tree/negative/test009.jvt
@@ -0,0 +1,5 @@
+-- calling unsupported anoma-get
+
+function main() : * {
+  anoma-get(1)
+}