Support compilation of Anoma transactions in nockma backend (#2693)

When we first implemented the Nockma backend we wrongly assumed that the only entry point for Juvix compiled Nockma modules would be the main function. Using this assumption we could add a setup step in the main function that put the Anoma stdlib and compiled functions from the Juvix module in a static place in the Nockma subject. References to the Anoma stdlib and functions in the module could then be resolved statically. However, one of the use cases for Juvix -> Nockma compilation is for Anoma to run logic functions that are fields of a transaction. So the user writes a Juvix program with main function that returns a transaction. The result of the main function is passed to Anoma. When Anoma calls the logic function on a field of the transaction, the setup part of the main function is not run so the subject is not in the required state. In fact, the logic function is not even callable by Anoma because non-main functions in the Juvix module use a calling convention that assumes the subject has a particular shape. This PR solves the problem by making all functions in the Juvix module use the Anoma calling convention. We make all compiled closures (including, for example, the logic functions stored on resources in a transaction) self contained, i.e they contain the functions library and anoma standard library. Modules that contain many closures produce large nockma output files which slows down the evaluator. This will need to be fixed in the future either with Nockma compression ([jam serialization](https://developers.urbit.org/reference/hoon/stdlib/2p)) or otherwise. But it does not block the compilation and execution of Anoma transactions. Other fixes / additions: * Extra tracing. You can now annotate output cells with a tag that will be displayed in the output * Unittests for listToTuple, appendRights helper functions * Fixes for the nockma parser when parsing 'pretty nockma', specifically stdlib calls, tags and functions_library atom. * Adds `juvix dev nock run` command that can run a program output with the `anoma` target. * Remove the `nockma` target. As described above we always use the Anoma calling convention so there's no need for a separate target for the 'juvix calling convention' * Adds a `--profile` flag to `juvix dev nock run` which outputs a count of Nockma ops used in the evaluation * In tests we no longer serialise the compiled program to force full evaluation of the compiled code. We added a negative test to check that strings are not allowed in Nockma/Anoma programs, it is output in a file `OUTPUT.profile` and has the following form: ``` quote : 15077 apply : 0 isCell : 0 suc : 0 = : 4517 if : 5086 seq : 5086 push : 0 call : 4896 replace : 1 hint : 8 scry : 0 trace : 0 ``` --------- Co-authored-by: Jan Mas Rovira <[email protected]>
anoma · Mar 22, 2024 · b981405 · b981405
1 parent 2e00642
commit b981405
Show file tree

Hide file tree

Showing 37 changed files with 752 additions and 354 deletions.
diff --git a/app/Commands/Compile.hs b/app/Commands/Compile.hs
@@ -27,7 +27,6 @@ runCommand opts@CompileOptions {..} = do
     TargetTree -> Compile.runTreePipeline arg
     TargetAsm -> Compile.runAsmPipeline arg
     TargetReg -> Compile.runRegPipeline arg
-    TargetNockma -> Compile.runNockmaPipeline arg
     TargetAnoma -> Compile.runAnomaPipeline arg
     TargetCasm -> Compile.runCasmPipeline arg
 

diff --git a/app/Commands/Dev/Asm/Compile.hs b/app/Commands/Dev/Asm/Compile.hs
@@ -70,7 +70,6 @@ runCommand opts = do
       TargetNative64 -> return Backend.TargetCNative64
       TargetReg -> return Backend.TargetReg
       TargetCasm -> return Backend.TargetCairo
-      TargetNockma -> err "Nockma"
       TargetAnoma -> err "Anoma"
       TargetTree -> err "JuvixTree"
       TargetGeb -> err "GEB"

diff --git a/app/Commands/Dev/Core/Compile.hs b/app/Commands/Dev/Core/Compile.hs
@@ -21,7 +21,6 @@ runCommand opts = do
     TargetAsm -> runAsmPipeline arg
     TargetReg -> runRegPipeline arg
     TargetTree -> runTreePipeline arg
-    TargetNockma -> runNockmaPipeline arg
     TargetAnoma -> runAnomaPipeline arg
     TargetCasm -> runCasmPipeline arg
   where

diff --git a/app/Commands/Dev/Core/Compile/Base.hs b/app/Commands/Dev/Core/Compile/Base.hs
@@ -2,6 +2,7 @@ module Commands.Dev.Core.Compile.Base where
 
 import Commands.Base
 import Commands.Dev.Core.Compile.Options
+import Commands.Dev.Tree.Compile.Base (outputAnomaResult)
 import Commands.Extra.Compile qualified as Compile
 import Juvix.Compiler.Asm.Pretty qualified as Asm
 import Juvix.Compiler.Backend qualified as Backend
@@ -12,7 +13,6 @@ import Juvix.Compiler.Casm.Data.Result qualified as Casm
 import Juvix.Compiler.Casm.Pretty qualified as Casm
 import Juvix.Compiler.Core.Data.Module qualified as Core
 import Juvix.Compiler.Core.Data.TransformationId qualified as Core
-import Juvix.Compiler.Nockma.Pretty qualified as Nockma
 import Juvix.Compiler.Reg.Pretty qualified as Reg
 import Juvix.Compiler.Tree.Pretty qualified as Tree
 import Juvix.Prelude.Pretty
@@ -46,7 +46,6 @@ getEntry PipelineArg {..} = do
       TargetAsm -> Backend.TargetAsm
       TargetReg -> Backend.TargetReg
       TargetTree -> Backend.TargetTree
-      TargetNockma -> Backend.TargetNockma
       TargetAnoma -> Backend.TargetAnoma
       TargetCasm -> Backend.TargetCairo
 
@@ -147,19 +146,6 @@ runTreePipeline pa@PipelineArg {..} = do
   let code = Tree.ppPrint tab' tab'
   writeFileEnsureLn treeFile code
 
-runNockmaPipeline :: (Members '[EmbedIO, App, TaggedLock] r) => PipelineArg -> Sem r ()
-runNockmaPipeline pa@PipelineArg {..} = do
-  entryPoint <- getEntry pa
-  nockmaFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
-  r <-
-    runReader entryPoint
-      . runError @JuvixError
-      . coreToNockma
-      $ _pipelineArgModule
-  tab' <- getRight r
-  let code = Nockma.ppSerialize tab'
-  writeFileEnsureLn nockmaFile code
-
 runAnomaPipeline :: (Members '[EmbedIO, App, TaggedLock] r) => PipelineArg -> Sem r ()
 runAnomaPipeline pa@PipelineArg {..} = do
   entryPoint <- getEntry pa
@@ -169,9 +155,8 @@ runAnomaPipeline pa@PipelineArg {..} = do
       . runError @JuvixError
       . coreToAnoma
       $ _pipelineArgModule
-  tab' <- getRight r
-  let code = Nockma.ppSerialize tab'
-  writeFileEnsureLn nockmaFile code
+  res <- getRight r
+  outputAnomaResult nockmaFile res
 
 runCasmPipeline :: (Members '[EmbedIO, App, TaggedLock] r) => PipelineArg -> Sem r ()
 runCasmPipeline pa@PipelineArg {..} = do

diff --git a/app/Commands/Dev/Nockma.hs b/app/Commands/Dev/Nockma.hs
@@ -5,9 +5,11 @@ import Commands.Dev.Nockma.Eval as Eval
 import Commands.Dev.Nockma.Format as Format
 import Commands.Dev.Nockma.Options
 import Commands.Dev.Nockma.Repl as Repl
+import Commands.Dev.Nockma.Run as Run
 
 runCommand :: forall r. (Members '[EmbedIO, App] r) => NockmaCommand -> Sem r ()
 runCommand = \case
   NockmaRepl opts -> Repl.runCommand opts
   NockmaEval opts -> Eval.runCommand opts
   NockmaFormat opts -> Format.runCommand opts
+  NockmaRun opts -> Run.runCommand opts
diff --git a/app/Commands/Dev/Nockma/Eval.hs b/app/Commands/Dev/Nockma/Eval.hs
@@ -3,7 +3,7 @@ module Commands.Dev.Nockma.Eval where
 import Commands.Base hiding (Atom)
 import Commands.Dev.Nockma.Eval.Options
 import Juvix.Compiler.Nockma.EvalCompiled
-import Juvix.Compiler.Nockma.Evaluator.Options
+import Juvix.Compiler.Nockma.Evaluator
 import Juvix.Compiler.Nockma.Pretty
 import Juvix.Compiler.Nockma.Translation.FromSource qualified as Nockma
 
@@ -14,11 +14,14 @@ runCommand opts = do
   case parsedTerm of
     Left err -> exitJuvixError (JuvixError err)
     Right (TermCell c) -> do
-      res <-
-        runReader defaultEvalOptions
+      (counts, res) <-
+        runOpCounts
+          . runReader defaultEvalOptions
           . runOutputSem @(Term Natural) (say . ppTrace)
           $ evalCompiledNock' (c ^. cellLeft) (c ^. cellRight)
       putStrLn (ppPrint res)
+      let statsFile = replaceExtension' ".profile" afile
+      writeFileEnsureLn statsFile (prettyText counts)
     Right TermAtom {} -> exitFailMsg "Expected nockma input to be a cell"
   where
     file :: AppPath File

diff --git a/app/Commands/Dev/Nockma/Eval/Options.hs b/app/Commands/Dev/Nockma/Eval/Options.hs
@@ -2,8 +2,9 @@ module Commands.Dev.Nockma.Eval.Options where
 
 import CommonOptions
 
-newtype NockmaEvalOptions = NockmaEvalOptions
-  { _nockmaEvalFile :: AppPath File
+data NockmaEvalOptions = NockmaEvalOptions
+  { _nockmaEvalFile :: AppPath File,
+    _nockmaEvalProfile :: Bool
   }
   deriving stock (Data)
 
@@ -12,4 +13,9 @@ makeLenses ''NockmaEvalOptions
 parseNockmaEvalOptions :: Parser NockmaEvalOptions
 parseNockmaEvalOptions = do
   _nockmaEvalFile <- parseInputFile FileExtNockma
+  _nockmaEvalProfile <-
+    switch
+      ( long "profile"
+          <> help "Report evaluator profiling statistics"
+      )
   pure NockmaEvalOptions {..}
diff --git a/app/Commands/Dev/Nockma/Options.hs b/app/Commands/Dev/Nockma/Options.hs
@@ -3,12 +3,14 @@ module Commands.Dev.Nockma.Options where
 import Commands.Dev.Nockma.Eval.Options
 import Commands.Dev.Nockma.Format.Options
 import Commands.Dev.Nockma.Repl.Options
+import Commands.Dev.Nockma.Run.Options
 import CommonOptions
 
 data NockmaCommand
   = NockmaRepl NockmaReplOptions
   | NockmaEval NockmaEvalOptions
   | NockmaFormat NockmaFormatOptions
+  | NockmaRun NockmaRunOptions
   deriving stock (Data)
 
 parseNockmaCommand :: Parser NockmaCommand
@@ -17,9 +19,19 @@ parseNockmaCommand =
     mconcat
       [ commandRepl,
         commandFromAsm,
-        commandFormat
+        commandFormat,
+        commandRun
       ]
   where
+    commandRun :: Mod CommandFields NockmaCommand
+    commandRun = command "run" runInfo
+      where
+        runInfo :: ParserInfo NockmaCommand
+        runInfo =
+          info
+            (NockmaRun <$> parseNockmaRunOptions)
+            (progDesc "Run an Anoma program. It should be used with artefacts obtained from compilation with the anoma target.")
+
     commandFromAsm :: Mod CommandFields NockmaCommand
     commandFromAsm = command "eval" fromAsmInfo
       where

diff --git a/app/Commands/Dev/Nockma/Run.hs b/app/Commands/Dev/Nockma/Run.hs
@@ -0,0 +1,37 @@
+module Commands.Dev.Nockma.Run where
+
+import Commands.Base hiding (Atom)
+import Commands.Dev.Nockma.Run.Options
+import Juvix.Compiler.Nockma.Anoma
+import Juvix.Compiler.Nockma.EvalCompiled
+import Juvix.Compiler.Nockma.Evaluator
+import Juvix.Compiler.Nockma.Pretty
+import Juvix.Compiler.Nockma.Translation.FromSource qualified as Nockma
+import Juvix.Parser.Error
+
+runCommand :: forall r. (Members '[EmbedIO, App] r) => NockmaRunOptions -> Sem r ()
+runCommand opts = do
+  afile <- fromAppPathFile inputFile
+  argsFile <- mapM fromAppPathFile (opts ^. nockmaRunArgs)
+  parsedArgs <- mapM (Nockma.parseTermFile >=> checkParsed) argsFile
+  parsedTerm <- Nockma.parseTermFile afile >>= checkParsed
+  case parsedTerm of
+    t@(TermCell {}) -> do
+      let formula = anomaCallTuple parsedArgs
+      (counts, res) <-
+        runOpCounts
+          . runReader defaultEvalOptions
+          . runOutputSem @(Term Natural) (say . ppTrace)
+          $ evalCompiledNock' t formula
+      putStrLn (ppPrint res)
+      let statsFile = replaceExtension' ".profile" afile
+      writeFileEnsureLn statsFile (prettyText counts)
+    TermAtom {} -> exitFailMsg "Expected nockma input to be a cell"
+  where
+    inputFile :: AppPath File
+    inputFile = opts ^. nockmaRunFile
+
+    checkParsed :: Either MegaparsecError (Term Natural) -> Sem r (Term Natural)
+    checkParsed = \case
+      Left err -> exitJuvixError (JuvixError err)
+      Right tm -> return tm
diff --git a/app/Commands/Dev/Nockma/Run/Options.hs b/app/Commands/Dev/Nockma/Run/Options.hs
@@ -0,0 +1,32 @@
+module Commands.Dev.Nockma.Run.Options where
+
+import CommonOptions
+
+data NockmaRunOptions = NockmaRunOptions
+  { _nockmaRunFile :: AppPath File,
+    _nockmaRunProfile :: Bool,
+    _nockmaRunArgs :: Maybe (AppPath File)
+  }
+  deriving stock (Data)
+
+makeLenses ''NockmaRunOptions
+
+parseNockmaRunOptions :: Parser NockmaRunOptions
+parseNockmaRunOptions = do
+  _nockmaRunFile <- parseInputFile FileExtNockma
+  _nockmaRunArgs <- optional $ do
+    _pathPath <-
+      option
+        somePreFileOpt
+        ( long "args"
+            <> metavar "ARGS_FILE"
+            <> help "Path to file containing args"
+            <> action "file"
+        )
+    pure AppPath {_pathIsInput = True, ..}
+  _nockmaRunProfile <-
+    switch
+      ( long "profile"
+          <> help "Report evaluator profiling statistics"
+      )
+  pure NockmaRunOptions {..}
diff --git a/app/Commands/Dev/Reg/Compile.hs b/app/Commands/Dev/Reg/Compile.hs
@@ -59,7 +59,6 @@ runCommand opts = do
       TargetNative64 -> return Backend.TargetCNative64
       TargetCasm -> return Backend.TargetCairo
       TargetReg -> err "JuvixReg"
-      TargetNockma -> err "Nockma"
       TargetAnoma -> err "Anoma"
       TargetTree -> err "JuvixTree"
       TargetGeb -> err "GEB"

diff --git a/app/Commands/Dev/Tree/Compile.hs b/app/Commands/Dev/Tree/Compile.hs
@@ -20,7 +20,6 @@ runCommand opts = do
     TargetAsm -> runAsmPipeline arg
     TargetReg -> runRegPipeline arg
     TargetTree -> return ()
-    TargetNockma -> runNockmaPipeline arg
     TargetAnoma -> runAnomaPipeline arg
     TargetCasm -> runCasmPipeline arg
   where

diff --git a/app/Commands/Dev/Tree/Compile/Base.hs b/app/Commands/Dev/Tree/Compile/Base.hs
@@ -9,6 +9,7 @@ import Juvix.Compiler.Backend.C qualified as C
 import Juvix.Compiler.Casm.Data.Result qualified as Casm
 import Juvix.Compiler.Casm.Pretty qualified as Casm
 import Juvix.Compiler.Nockma.Pretty qualified as Nockma
+import Juvix.Compiler.Nockma.Translation.FromTree qualified as Nockma
 import Juvix.Compiler.Reg.Pretty qualified as Reg
 import Juvix.Compiler.Tree.Data.InfoTable qualified as Tree
 import Juvix.Prelude.Pretty
@@ -41,7 +42,6 @@ getEntry PipelineArg {..} = do
       TargetAsm -> Backend.TargetAsm
       TargetReg -> Backend.TargetReg
       TargetTree -> Backend.TargetTree
-      TargetNockma -> Backend.TargetNockma
       TargetAnoma -> Backend.TargetAnoma
       TargetCasm -> Backend.TargetCairo
 
@@ -104,19 +104,6 @@ runRegPipeline pa@PipelineArg {..} = do
   let code = Reg.ppPrint tab' tab'
   writeFileEnsureLn regFile code
 
-runNockmaPipeline :: (Members '[EmbedIO, App, TaggedLock] r) => PipelineArg -> Sem r ()
-runNockmaPipeline pa@PipelineArg {..} = do
-  entryPoint <- getEntry pa
-  nockmaFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
-  r <-
-    runReader entryPoint
-      . runError @JuvixError
-      . treeToNockma
-      $ _pipelineArgTable
-  tab' <- getRight r
-  let code = Nockma.ppSerialize tab'
-  writeFileEnsureLn nockmaFile code
-
 runAnomaPipeline :: (Members '[EmbedIO, App, TaggedLock] r) => PipelineArg -> Sem r ()
 runAnomaPipeline pa@PipelineArg {..} = do
   entryPoint <- getEntry pa
@@ -126,9 +113,15 @@ runAnomaPipeline pa@PipelineArg {..} = do
       . runError @JuvixError
       . treeToAnoma
       $ _pipelineArgTable
-  tab' <- getRight r
-  let code = Nockma.ppSerialize tab'
+  res <- getRight r
+  outputAnomaResult nockmaFile res
+
+outputAnomaResult :: (Members '[EmbedIO, App] r) => Path Abs File -> Nockma.AnomaResult -> Sem r ()
+outputAnomaResult nockmaFile Nockma.AnomaResult {..} = do
+  let code = Nockma.ppSerialize _anomaClosure
+      prettyNockmaFile = replaceExtensions' [".pretty", ".nockma"] nockmaFile
   writeFileEnsureLn nockmaFile code
+  writeFileEnsureLn prettyNockmaFile (Nockma.ppPrint _anomaClosure)
 
 runCasmPipeline :: (Members '[EmbedIO, App, TaggedLock] r) => PipelineArg -> Sem r ()
 runCasmPipeline pa@PipelineArg {..} = do

diff --git a/app/Commands/Dev/Tree/Compile/Options.hs b/app/Commands/Dev/Tree/Compile/Options.hs
@@ -14,8 +14,8 @@ treeSupportedTargets =
       TargetNative64,
       TargetAsm,
       TargetReg,
-      TargetNockma,
-      TargetCasm
+      TargetCasm,
+      TargetAnoma
     ]
 
 parseTreeCompileOptions :: Parser CompileOptions

diff --git a/app/Commands/Extra/Compile.hs b/app/Commands/Extra/Compile.hs
@@ -35,7 +35,6 @@ runCompile inputFile o = do
     TargetAsm -> return (Right ())
     TargetReg -> return (Right ())
     TargetTree -> return (Right ())
-    TargetNockma -> return (Right ())
     TargetAnoma -> return (Right ())
     TargetCasm -> return (Right ())
 
@@ -55,7 +54,6 @@ prepareRuntime buildDir o = do
     TargetAsm -> return ()
     TargetReg -> return ()
     TargetTree -> return ()
-    TargetNockma -> return ()
     TargetAnoma -> return ()
     TargetCasm -> return ()
   where
@@ -119,8 +117,6 @@ outputFile opts inputFile =
           replaceExtension' juvixRegFileExt baseOutputFile
         TargetTree ->
           replaceExtension' juvixTreeFileExt baseOutputFile
-        TargetNockma ->
-          replaceExtension' nockmaFileExt baseOutputFile
         TargetAnoma ->
           replaceExtension' nockmaFileExt baseOutputFile
         TargetCasm ->

diff --git a/app/Commands/Extra/Compile/Options.hs b/app/Commands/Extra/Compile/Options.hs
@@ -13,7 +13,6 @@ data CompileTarget
   | TargetAsm
   | TargetReg
   | TargetTree
-  | TargetNockma
   | TargetAnoma
   | TargetCasm
   deriving stock (Eq, Data, Bounded, Enum)
@@ -28,7 +27,6 @@ instance Show CompileTarget where
     TargetAsm -> "asm"
     TargetReg -> "reg"
     TargetTree -> "tree"
-    TargetNockma -> "nockma"
     TargetAnoma -> "anoma"
     TargetCasm -> "casm"
 

diff --git a/src/Juvix/Compiler/Backend.hs b/src/Juvix/Compiler/Backend.hs
@@ -12,7 +12,6 @@ data Target
   | TargetAsm
   | TargetReg
   | TargetTree
-  | TargetNockma
   | TargetAnoma
   | TargetCairo
   deriving stock (Data, Eq, Show)
@@ -94,8 +93,6 @@ getLimits tgt debug = case tgt of
       }
   TargetTree ->
     defaultLimits
-  TargetNockma ->
-    defaultLimits
   TargetAnoma ->
     defaultLimits
   TargetCairo ->