From 3f1d47fc7cac787139986c40d1ae66a98efdc86d Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Sun, 3 Mar 2024 16:48:25 +0100
Subject: [PATCH 01/10] Add scry (Nockma op 12) to Nockma language

---
 src/Juvix/Compiler/Nockma/Language.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Juvix/Compiler/Nockma/Language.hs b/src/Juvix/Compiler/Nockma/Language.hs
index f078105260..978b15b18e 100644
--- a/src/Juvix/Compiler/Nockma/Language.hs
+++ b/src/Juvix/Compiler/Nockma/Language.hs
@@ -101,6 +101,7 @@ data NockOp
   | OpCall
   | OpReplace
   | OpHint
+  | OpScry
   | OpTrace
   deriving stock (Bounded, Enum, Eq, Generic)
 
@@ -120,6 +121,7 @@ instance Pretty NockOp where
     OpCall -> "call"
     OpReplace -> "replace"
     OpHint -> "hint"
+    OpScry -> "scry"
     OpTrace -> "trace"
 
 textToStdlibFunctionMap :: HashMap Text StdlibFunction
@@ -214,6 +216,7 @@ serializeOp = \case
   OpCall -> 9
   OpReplace -> 10
   OpHint -> 11
+  OpScry -> 12
   OpTrace -> 100
 
 class (NockmaEq a) => NockNatural a where

From 3b6d37dafaf31c9f3f86defacf00771c158f5789 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Sun, 3 Mar 2024 16:49:03 +0100
Subject: [PATCH 02/10] Add Hashable instance for Nockma Term and dependents

---
 src/Juvix/Compiler/Nockma/Language.hs         | 28 ++++++++++++++-----
 .../Compiler/Nockma/StdlibFunction/Base.hs    |  4 ++-
 src/Juvix/Data/Irrelevant.hs                  |  3 ++
 3 files changed, 27 insertions(+), 8 deletions(-)

diff --git a/src/Juvix/Compiler/Nockma/Language.hs b/src/Juvix/Compiler/Nockma/Language.hs
index 978b15b18e..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
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/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

From 8ceee2a7f8c88666803d18bb34cfc6072f697ff6 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Sun, 3 Mar 2024 16:49:32 +0100
Subject: [PATCH 03/10] Evaluate Nockma scry/op12 and add a test

---
 src/Juvix/Compiler/Nockma/EvalCompiled.hs      |  1 +
 src/Juvix/Compiler/Nockma/Evaluator.hs         | 17 ++++++++++++++---
 src/Juvix/Compiler/Nockma/Evaluator/Storage.hs | 12 ++++++++++++
 test/Anoma/Compilation/Positive.hs             |  1 +
 test/Nockma/Eval/Positive.hs                   | 13 +++++++++++--
 5 files changed, 39 insertions(+), 5 deletions(-)
 create mode 100644 src/Juvix/Compiler/Nockma/Evaluator/Storage.hs

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..8aebca6f95 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)
+              subResult <- evalArg crumbEvalSecond stack subFormula
+              HashMap.lookupDefault impossible subResult <$> asks (^. storageKeyValueData)
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/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs
index b27f42717f..59c4e34500 100644
--- a/test/Anoma/Compilation/Positive.hs
+++ b/test/Anoma/Compilation/Positive.hs
@@ -27,6 +27,7 @@ mkAnomaCallTest' enableDebug _testName relRoot mainFile args _testCheck =
         return compiledMain
       let _testProgramFormula = anomaCall args
           _testEvalOptions = defaultEvalOptions
+          _testProgramStorage :: Storage Natural = emptyStorage
       return Test {..}
 
     withRootCopy :: (Prelude.Path Abs Dir -> IO a) -> IO a
diff --git a/test/Nockma/Eval/Positive.hs b/test/Nockma/Eval/Positive.hs
index a493af0e1d..4fdb07bc33 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,7 @@ type Check = Sem '[Reader [Term Natural], Reader (Term Natural), EmbedIO]
 
 data Test = Test
   { _testEvalOptions :: EvalOptions,
+    _testProgramStorage :: Storage Natural,
     _testName :: Text,
     _testProgramSubject :: Term Natural,
     _testProgramFormula :: Term Natural,
@@ -29,6 +31,7 @@ mkNockmaAssertion Test {..} = do
           . runOutputList @(Term Natural)
           . runError @(ErrNockNatural Natural)
           . runError @(NockEvalError Natural)
+          . runReader @(Storage Natural) _testProgramStorage
           $ eval _testProgramSubject _testProgramFormula
 
   case evalResult of
@@ -91,6 +94,7 @@ compilerTest n mainFun _testCheck _evalInterceptStdlibCalls =
       opts = CompilerOptions {_compilerOptionsEnableTrace = False}
       Cell _testProgramSubject _testProgramFormula = runCompilerWithJuvix opts mempty [] f
       _testEvalOptions = EvalOptions {..}
+      _testProgramStorage :: Storage Natural = emptyStorage
    in Test {..}
 
 anomaTest :: Text -> Term Natural -> [Term Natural] -> Check () -> Bool -> Test
@@ -110,11 +114,15 @@ anomaTest n mainFun args _testCheck _evalInterceptStdlibCalls =
       _testProgramSubject = TermCell (runCompilerWithAnoma opts mempty [] f)
 
       _testProgramFormula = anomaCall args
+      _testProgramStorage :: Storage Natural = emptyStorage
       _testEvalOptions = EvalOptions {..}
    in Test {..}
 
+testWithStorage :: [(Term Natural, Term Natural)] -> Text -> Term Natural -> Term Natural -> Check () -> Test
+testWithStorage s = Test defaultEvalOptions (Storage (HashMap.fromList s))
+
 test :: Text -> Term Natural -> Term Natural -> Check () -> Test
-test = Test defaultEvalOptions
+test = testWithStorage []
 
 anomaCallingConventionTests :: [Test]
 anomaCallingConventionTests =
@@ -158,5 +166,6 @@ 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 |])
   ]

From 36a2dc8a368d03d997430dacd1870225d25fe5b6 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Sun, 3 Mar 2024 19:40:33 +0100
Subject: [PATCH 04/10] Make missing storage key an evaluation error

---
 src/Juvix/Compiler/Nockma/Evaluator.hs       |  4 +--
 src/Juvix/Compiler/Nockma/Evaluator/Error.hs | 33 ++++++++++++++++++++
 test/Anoma/Compilation/Positive.hs           |  1 +
 test/Nockma/Eval/Positive.hs                 | 28 ++++++++++++++---
 4 files changed, 59 insertions(+), 7 deletions(-)

diff --git a/src/Juvix/Compiler/Nockma/Evaluator.hs b/src/Juvix/Compiler/Nockma/Evaluator.hs
index 8aebca6f95..59b57f8aed 100644
--- a/src/Juvix/Compiler/Nockma/Evaluator.hs
+++ b/src/Juvix/Compiler/Nockma/Evaluator.hs
@@ -326,5 +326,5 @@ eval inistack initerm =
             goOpScry = do
               Cell' typeFormula subFormula _ <- withCrumb (crumb crumbDecodeFirst) (asCell (c ^. operatorCellTerm))
               void (evalArg crumbEvalFirst stack typeFormula)
-              subResult <- evalArg crumbEvalSecond stack subFormula
-              HashMap.lookupDefault impossible subResult <$> asks (^. storageKeyValueData)
+              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..ddae3b4f10 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/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs
index 59c4e34500..40cbfdbff2 100644
--- a/test/Anoma/Compilation/Positive.hs
+++ b/test/Anoma/Compilation/Positive.hs
@@ -28,6 +28,7 @@ mkAnomaCallTest' enableDebug _testName relRoot mainFile args _testCheck =
       let _testProgramFormula = anomaCall args
           _testEvalOptions = defaultEvalOptions
           _testProgramStorage :: Storage Natural = emptyStorage
+          _testAssertEvalError :: Maybe (NockEvalError Natural -> Assertion) = Nothing
       return Test {..}
 
     withRootCopy :: (Prelude.Path Abs Dir -> IO a) -> IO a
diff --git a/test/Nockma/Eval/Positive.hs b/test/Nockma/Eval/Positive.hs
index 4fdb07bc33..f0402a68df 100644
--- a/test/Nockma/Eval/Positive.hs
+++ b/test/Nockma/Eval/Positive.hs
@@ -14,6 +14,7 @@ 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,
@@ -36,9 +37,13 @@ mkNockmaAssertion Test {..} = do
 
   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 =
@@ -95,8 +100,19 @@ compilerTest n mainFun _testCheck _evalInterceptStdlibCalls =
       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 =
@@ -116,10 +132,11 @@ anomaTest n mainFun args _testCheck _evalInterceptStdlibCalls =
       _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 (Storage (HashMap.fromList s))
+testWithStorage s = Test defaultEvalOptions Nothing (Storage (HashMap.fromList s))
 
 test :: Text -> Term Natural -> Term Natural -> Check () -> Test
 test = testWithStorage []
@@ -167,5 +184,6 @@ unitTests =
     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 |]),
-    testWithStorage [([nock| 111 |], [nock| 222 |])] "scry" [nock| nil |] [nock| [scry [quote nil] [quote 111]] |] (eqNock [nock| 222 |])
+    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 |])
   ]

From aff33fb9f8ff9187313a8a62b9364e2cdea6d26c Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Tue, 19 Mar 2024 16:06:51 +0000
Subject: [PATCH 05/10] Add builtin anoma-get

This builtin calls Anoma/Nockma scry
---
 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 +
 .../Compiler/Nockma/Translation/FromTree.hs   |  4 ++++
 src/Juvix/Compiler/Tree/Evaluator.hs          |  1 +
 src/Juvix/Compiler/Tree/EvaluatorEff.hs       |  1 +
 src/Juvix/Compiler/Tree/Language.hs           |  2 ++
 src/Juvix/Compiler/Tree/Pretty/Base.hs        |  1 +
 .../Compiler/Tree/Transformation/Validate.hs  |  1 +
 .../Compiler/Tree/Translation/FromCore.hs     |  1 +
 src/Juvix/Extra/Strings.hs                    |  3 +++
 test/Anoma/Compilation/Positive.hs            | 20 +++++++++++++------
 20 files changed, 73 insertions(+), 6 deletions(-)
 create mode 100644 src/Juvix/Compiler/Builtins/Anoma.hs

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/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/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/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/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/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 40cbfdbff2..3579ab18b9 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,7 +28,6 @@ mkAnomaCallTest' enableDebug _testName relRoot mainFile args _testCheck =
         return compiledMain
       let _testProgramFormula = anomaCall args
           _testEvalOptions = defaultEvalOptions
-          _testProgramStorage :: Storage Natural = emptyStorage
           _testAssertEvalError :: Maybe (NockEvalError Natural -> Assertion) = Nothing
       return Test {..}
 
@@ -45,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
@@ -525,5 +525,13 @@ allTests =
         $(mkRelDir "test073")
         $(mkRelFile "test073.juvix")
         []
-        $ checkNatOutput [11]
+        $ checkNatOutput [11],
+      mkAnomaCallTest'
+        True
+        (Storage (HashMap.fromList [([nock| 333 |], [nock| 222 |])]))
+        "Test074: Builtin anomaGet"
+        $(mkRelDir ".")
+        $(mkRelFile "test074.juvix")
+        [nockNatLiteral 333]
+        $ checkNatOutput [222]
     ]

From e01032bc43c98d71d06ac73a1613fd67e73468ce Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Tue, 19 Mar 2024 16:37:46 +0000
Subject: [PATCH 06/10] Show that lists can be stored / retrieved using scry

---
 test/Anoma/Compilation/Positive.hs | 26 ++++++++++++++++++--------
 1 file changed, 18 insertions(+), 8 deletions(-)

diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs
index 3579ab18b9..17e8a922f6 100644
--- a/test/Anoma/Compilation/Positive.hs
+++ b/test/Anoma/Compilation/Positive.hs
@@ -526,12 +526,22 @@ allTests =
         $(mkRelFile "test073.juvix")
         []
         $ checkNatOutput [11],
-      mkAnomaCallTest'
-        True
-        (Storage (HashMap.fromList [([nock| 333 |], [nock| 222 |])]))
-        "Test074: Builtin anomaGet"
-        $(mkRelDir ".")
-        $(mkRelFile "test074.juvix")
-        [nockNatLiteral 333]
-        $ checkNatOutput [222]
+      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]
     ]

From e7e9e8ea1a703ba03a599d0906975401c07626c4 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Tue, 19 Mar 2024 16:41:40 +0000
Subject: [PATCH 07/10] OpAnomaGet is unsupported in JuvixAsm

---
 src/Juvix/Compiler/Asm/Translation/FromTree.hs | 1 +
 1 file changed, 1 insertion(+)

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)

From 4b02b1ac08c0afe8877ad7ce20895572191233e9 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Tue, 19 Mar 2024 17:14:18 +0000
Subject: [PATCH 08/10] Update src/Juvix/Compiler/Nockma/Evaluator/Error.hs

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
---
 src/Juvix/Compiler/Nockma/Evaluator/Error.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Juvix/Compiler/Nockma/Evaluator/Error.hs b/src/Juvix/Compiler/Nockma/Evaluator/Error.hs
index ddae3b4f10..77689ae0e7 100644
--- a/src/Juvix/Compiler/Nockma/Evaluator/Error.hs
+++ b/src/Juvix/Compiler/Nockma/Evaluator/Error.hs
@@ -121,7 +121,7 @@ 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)))
+    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)

From c97f27d672462d3cb1137e03047f8aa289e558e5 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Wed, 20 Mar 2024 08:48:55 +0000
Subject: [PATCH 09/10] Add missing file

---
 tests/Anoma/Compilation/positive/test074.juvix | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 tests/Anoma/Compilation/positive/test074.juvix

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;

From 90205162f2a589e7a2202d69fd9218813ce0a118 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Wed, 20 Mar 2024 12:09:16 +0000
Subject: [PATCH 10/10] Add a Tree transform to check that anoma-get is not
 used

Apply this transformation to the Tree->Asm translation.
---
 .../Compiler/Tree/Data/TransformationId.hs    |  4 +-
 .../Tree/Data/TransformationId/Strings.hs     |  3 +
 src/Juvix/Compiler/Tree/Keywords.hs           |  4 +-
 src/Juvix/Compiler/Tree/Transformation.hs     |  2 +
 .../Tree/Transformation/CheckNoAnoma.hs       | 23 +++++++
 .../Compiler/Tree/Translation/FromSource.hs   |  1 +
 src/Juvix/Data/Keyword/All.hs                 |  3 +
 test/Compilation/Base.hs                      |  5 +-
 test/Tree/Transformation.hs                   |  4 +-
 test/Tree/Transformation/CheckNoAnoma.hs      | 67 +++++++++++++++++++
 tests/Tree/negative/test009.jvt               |  5 ++
 11 files changed, 117 insertions(+), 4 deletions(-)
 create mode 100644 src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs
 create mode 100644 test/Tree/Transformation/CheckNoAnoma.hs
 create mode 100644 tests/Tree/negative/test009.jvt

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/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/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/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/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/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/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/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)
+}