Add juvix dev anoma prove

app/Commands/Dev/Anoma.hs

@@ -4,14 +4,40 @@ module Commands.Dev.Anoma
   )
 where
 
+import Anoma.Client.Config
+import Anoma.Effect.Base
 import Commands.Base
+import Commands.Dev.Anoma.Client
 import Commands.Dev.Anoma.Options
+import Commands.Dev.Anoma.Prove qualified as Prove
+import Commands.Dev.Anoma.Prove.Options
 import Commands.Dev.Anoma.Start qualified as Start
-import Commands.Dev.Anoma.Status qualified as Status
-import Commands.Dev.Anoma.Stop qualified as Stop
+import Juvix.Data.CodeAnn
+import Juvix.Data.Yaml qualified as Y
 
-runCommand :: (Members AppEffects r) => AnomaCommand -> Sem r ()
-runCommand = \case
-  AnomaCommandStart opts -> Start.runCommand opts
-  AnomaCommandStatus -> Status.runCommand
-  AnomaCommandStop -> Stop.runCommand
+runCommand :: forall r. (Members AppEffects r) => AnomaCommand -> Sem r ()
+runCommand =
+  runAppError @SimpleError . \case
+    AnomaCommandStart opts -> Start.runCommand opts
+    AnomaCommandStatus -> checkRunning >>= renderStdOutLn . ppCodeAnn
+    AnomaCommandStop -> checkRunning >>= stopClient >> removeConfig
+    AnomaCommandProve opts -> do
+      host <- getHostConfig (opts ^. proveClientInfo)
+      runAnomaWithClient host (Prove.runCommand opts)
+  where
+    checkRunning :: (Members (Error SimpleError ': AppEffects) x) => Sem x ClientConfig
+    checkRunning = fromMaybeM (logInfo "The Anoma client is not running" >> exitFailure) checkClientRunning
+
+    getHostConfig :: (Members (Error SimpleError ': AppEffects) x) => Maybe (AppPath File) -> Sem x AnomaClientInfo
+    getHostConfig = \case
+      Just p -> fromAppFile p >>= readClientInfo
+      Nothing -> (^. clientConfigHost) <$> checkRunning
+
+    readClientInfo :: (Members '[Files, Error SimpleError] x) => Path Abs File -> Sem x AnomaClientInfo
+    readClientInfo fp = do
+      let pathName = pack (toFilePath fp)
+      unlessM (fileExists' fp) (throw (SimpleError (mkAnsiText ("Config file: " <> pathName <> " does not exist"))))
+      bs <- readFileBS' fp
+      case Y.decodeEither bs of
+        Left err -> throw (SimpleError (mkAnsiText (Y.prettyPrintParseException err <> "\n" <> toFilePath fp)))
+        Right a -> return a

app/Commands/Dev/Anoma/Base.hs

@@ -0,0 +1,25 @@
+module Commands.Dev.Anoma.Base where
+
+import Anoma.Effect
+import Commands.Base hiding (Atom)
+import Juvix.Compiler.Nockma.Pretty
+import Juvix.Compiler.Nockma.Translation.FromSource qualified as Nockma
+
+-- | Calls Anoma.Protobuf.NockService.Prove
+runNock :: forall r. (Members '[Error SimpleError, Anoma] r, Members AppEffects r) => AppPath File -> Maybe (AppPath File) -> Sem r RunNockmaResult
+runNock programFile margsFile = do
+  afile <- fromAppPathFile programFile
+  argsFile <- mapM fromAppPathFile margsFile
+  parsedArgs <- runAppError @JuvixError (mapM Nockma.cueJammedFileOrPretty argsFile)
+  parsedTerm <- runAppError @JuvixError (Nockma.cueJammedFileOrPretty afile)
+  case parsedTerm of
+    TermAtom {} -> exitFailMsg "Expected nockma input to be a cell"
+    t@(TermCell {}) -> go t (maybe [] unfoldList parsedArgs)
+  where
+    go :: Term Natural -> [Term Natural] -> Sem r RunNockmaResult
+    go t args =
+      runNockma
+        RunNockmaInput
+          { _runNockmaProgram = t,
+            _runNockmaArgs = args
+          }

app/Commands/Dev/Anoma/Options.hs

@@ -1,12 +1,14 @@
 module Commands.Dev.Anoma.Options where
 
+import Commands.Dev.Anoma.Prove.Options
 import Commands.Dev.Anoma.Start.Options
 import CommonOptions
 
 data AnomaCommand
   = AnomaCommandStart StartOptions
   | AnomaCommandStatus
   | AnomaCommandStop
+  | AnomaCommandProve ProveOptions
   deriving stock (Data)
 
 parseAnomaCommand :: Parser AnomaCommand
@@ -15,7 +17,8 @@ parseAnomaCommand =
     ( mconcat
         [ commandStart,
           commandStatus,
-          commandStop
+          commandStop,
+          commandProve
         ]
     )
   where
@@ -45,3 +48,32 @@ parseAnomaCommand =
           info
             (pure AnomaCommandStop)
             (progDesc "Stop the Anoma client")
+
+    commandProve :: Mod CommandFields AnomaCommand
+    commandProve = command "prove" runInfo
+      where
+        runInfo :: ParserInfo AnomaCommand
+        runInfo =
+          info
+            (AnomaCommandProve <$> parseProveOptions)
+            ( headerDoc
+                ( Just
+                    ( vsep
+                        [ "The prove command submits a Nockma program to the Anoma.Protobuf.NockService.Prove gRPC endpoint.",
+                          "",
+                          "By default, the gRPC request is made to the client that is started by juvix dev anoma start.",
+                          "Use the -c/--config option to use a different Anoma client.",
+                          "The config file format is:",
+                          "",
+                          "url: <ANOMA_CLIENT_URL>",
+                          "port: <ANOMA_CLIENT_GRPC_PORT>",
+                          "",
+                          "The gRPC response (a Nockma program) is saved to a file named <input>.proved.nockma, where <input> is the base name of the input file.",
+                          "Use the -o/--output option to specify a custom output filename.",
+                          "",
+                          "If the program generates traces, they will be written to standard output."
+                        ]
+                    )
+                )
+                <> progDesc "Submit a Nockma program to Anoma.Protobuf.NockService.Prove"
+            )

app/Commands/Dev/Anoma/Prove.hs

@@ -0,0 +1,27 @@
+module Commands.Dev.Anoma.Prove where
+
+import Anoma.Effect.Base
+import Anoma.Effect.RunNockma
+import Commands.Base
+import Commands.Dev.Anoma.Base
+import Commands.Dev.Anoma.Prove.Options
+import Juvix.Compiler.Nockma.Encoding.Jam qualified as Encoding
+import Juvix.Compiler.Nockma.Pretty hiding (Path)
+
+runCommand :: forall r. (Members (Anoma ': Error SimpleError ': AppEffects) r) => ProveOptions -> Sem r ()
+runCommand opts = do
+  res <- runNock (opts ^. proveFile) (opts ^. proveArgs)
+  let traces = res ^. runNockmaTraces
+  forM_ traces (renderStdOutLn . ppOutDefault)
+  let provedCode = Encoding.jamToByteString (res ^. runNockmaResult)
+  outputFile <- getOutputFile (opts ^. proveOutputFile)
+  writeFileBS outputFile provedCode
+  where
+    getOutputFile :: (Member App x) => Maybe (AppPath File) -> Sem x (Path Abs File)
+    getOutputFile = \case
+      Just out -> fromAppFile out
+      Nothing -> do
+        invokeDir <- askInvokeDir
+        programFilePath <- fromAppFile (opts ^. proveFile)
+        let baseOutputFile = invokeDir <//> filename programFilePath
+        return (replaceExtensions' (".proved" :| [".nockma"]) baseOutputFile)

app/Commands/Dev/Anoma/Prove/Options.hs

@@ -0,0 +1,21 @@
+module Commands.Dev.Anoma.Prove.Options where
+
+import CommonOptions
+
+data ProveOptions = ProveOptions
+  { _proveFile :: AppPath File,
+    _proveArgs :: Maybe (AppPath File),
+    _proveClientInfo :: Maybe (AppPath File),
+    _proveOutputFile :: Maybe (AppPath File)
+  }
+  deriving stock (Data)
+
+makeLenses ''ProveOptions
+
+parseProveOptions :: Parser ProveOptions
+parseProveOptions = do
+  _proveFile <- parseInputFile FileExtNockma
+  _proveArgs <- optional anomaArgsOpt
+  _proveClientInfo <- optional anomaClientConfigOpt
+  _proveOutputFile <- optional parseGenericOutputFile
+  pure ProveOptions {..}

app/Commands/Dev/Nockma/Run/Anoma.hs

@@ -2,8 +2,8 @@ module Commands.Dev.Nockma.Run.Anoma where
 
 import Anoma.Effect
 import Commands.Base hiding (Atom)
+import Commands.Dev.Anoma.Base
 import Juvix.Compiler.Nockma.Pretty
-import Juvix.Compiler.Nockma.Translation.FromSource qualified as Nockma
 
 data RunCommandArgs = RunCommandArgs
   { _runCommandArgsFile :: Maybe (AppPath File),
@@ -14,25 +14,10 @@ makeLenses ''RunCommandArgs
 
 runInAnoma :: forall r. (Members '[Error SimpleError, Anoma] r, Members AppEffects r) => RunCommandArgs -> Sem r ()
 runInAnoma runArgs = do
-  afile <- fromAppPathFile (runArgs ^. runCommandProgramFile)
-  argsFile <- mapM fromAppPathFile (runArgs ^. runCommandArgsFile)
-  parsedArgs <- runAppError @JuvixError (mapM Nockma.cueJammedFileOrPretty argsFile)
-  parsedTerm <- runAppError @JuvixError (Nockma.cueJammedFileOrPretty afile)
-  case parsedTerm of
-    TermAtom {} -> exitFailMsg "Expected nockma input to be a cell"
-    t@(TermCell {}) -> go t (maybe [] unfoldList parsedArgs)
-  where
-    go :: Term Natural -> [Term Natural] -> Sem r ()
-    go t args = do
-      res <-
-        runNockma
-          RunNockmaInput
-            { _runNockmaProgram = t,
-              _runNockmaArgs = args
-            }
-      let traces = res ^. runNockmaTraces
-      renderStdOutLn (annotate AnnImportant $ "Traces (" <> show (length traces) <> "):")
-      forM_ traces $ \tr ->
-        renderStdOutLn (ppPrint tr)
-      renderStdOutLn (annotate AnnImportant "Result:")
-      renderStdOutLn (ppPrint (res ^. runNockmaResult))
+  res <- runNock (runArgs ^. runCommandProgramFile) (runArgs ^. runCommandArgsFile)
+  let traces = res ^. runNockmaTraces
+  renderStdOutLn (annotate AnnImportant $ "Traces (" <> show (length traces) <> "):")
+  forM_ traces $ \tr ->
+    renderStdOutLn (ppOutDefault tr)
+  renderStdOutLn (annotate AnnImportant "Result:")
+  renderStdOutLn (ppOutDefault (res ^. runNockmaResult))

app/CommonOptions.hs

@@ -102,7 +102,20 @@ anomaArgsOpt = do
       somePreFileOpt
       ( long "args"
           <> metavar "ARGS_FILE"
-          <> help "Path to file containing args. The args file should contain a list (i.e. to pass 2 and [1 4] as args, the contents should be [2 [1 4] 0])."
+          <> help "Path to a file containing args. The args file should contain a list (i.e. to pass 2 and [1 4] as args, the contents should be [2 [1 4] 0])."
+          <> action "file"
+      )
+  pure AppPath {_pathIsInput = True, ..}
+
+anomaClientConfigOpt :: Parser (AppPath File)
+anomaClientConfigOpt = do
+  _pathPath <-
+    option
+      somePreFileOpt
+      ( long "config"
+          <> short 'c'
+          <> metavar "CONFIG_FILE"
+          <> help "A path to an Anoma client configuration file"
           <> action "file"
       )
   pure AppPath {_pathIsInput = True, ..}

src/Anoma/Client/Config.hs

@@ -30,10 +30,8 @@ $( deriveJSON
 
 instance PrettyCodeAnn ClientConfig where
   ppCodeAnn c =
-    "Anoma client info:"
-      <> line
-      -- The output of YAML encoding has a trailing newline
-      <> pretty (T.dropWhileEnd (== '\n') (decodeUtf8 (Y.encode c)))
+    -- The output of YAML encoding has a trailing newline
+    pretty (T.dropWhileEnd (== '\n') (decodeUtf8 (Y.encode c)))
 
 configPath :: (Member Files r) => Sem r (Path Abs File)
 configPath = (<//> clientConfigPath) <$> globalAnomaClient