Modify how the arguments are passed to the anoma node (#3258)

![image](https://github.com/user-attachments/assets/bd683eed-bdb5-4370-a05e-1c3bc4aea650)

app/Commands/Dev/Anoma/Base.hs

@@ -3,6 +3,9 @@ module Commands.Dev.Anoma.Base where
 import Anoma.Effect (Anoma)
 import Anoma.Effect qualified as Anoma
 import Commands.Base hiding (Atom)
+import Commands.Dev.Anoma.Prove.Options.ProveArg
+import Data.ByteString.Base64 qualified as Base64
+import Juvix.Compiler.Nockma.Encoding.ByteString
 import Juvix.Compiler.Nockma.Pretty
 import Juvix.Compiler.Nockma.Translation.FromSource qualified as Nockma
 
@@ -26,28 +29,29 @@ data ParsedArgsMode
 runNock ::
   forall r.
   (Members '[Error SimpleError, Anoma] r, Members AppEffects r) =>
-  ParsedArgsMode ->
   AppPath File ->
-  Maybe (AppPath File) ->
+  [ProveArg] ->
   Sem r Anoma.RunNockmaResult
-runNock argsMode programFile margsFile = do
-  afile <- fromAppPathFile programFile
-  argsFile <- mapM fromAppPathFile margsFile
-  parsedArgs <- runAppError @JuvixError $ do
-    let argsParser = case argsMode of
-          ParsedArgsModeJammedOrPretty -> Nockma.cueJammedFileOrPretty
-          ParsedArgsModePretty -> Nockma.parsePrettyTerm
-    mapM argsParser argsFile
-  parsedTerm <- runAppError @JuvixError (Nockma.cueJammedFileOrPretty afile)
-  cellOrFail parsedTerm (go (maybe [] unfoldList parsedArgs))
+runNock programFile pargs = do
+  argsfile <- fromAppPathFile programFile
+  parsedTerm <- runAppError @JuvixError (Nockma.cueJammedFileOrPretty argsfile)
+  args <- mapM proveArgToTerm pargs
+  Anoma.runNockma
+    Anoma.RunNockmaInput
+      { _runNockmaProgram = parsedTerm,
+        _runNockmaArgs = args
+      }
+
+proveArgToTerm :: forall r. (Members '[Error SimpleError, Files, App] r) => ProveArg -> Sem r (Term Natural)
+proveArgToTerm = \case
+  ProveArgNat n -> return (toNock n)
+  ProveArgBytes n -> fromAppPathFile n >>= readFileBS' >>= fromBytes
+  ProveArgBase64 n -> do
+    bs <- Base64.decodeLenient <$> (fromAppPathFile n >>= readFileBS')
+    fromBytes bs
   where
-    go :: [Term Natural] -> Term Natural -> Sem r Anoma.RunNockmaResult
-    go args t =
-      Anoma.runNockma
-        Anoma.RunNockmaInput
-          { _runNockmaProgram = t,
-            _runNockmaArgs = args
-          }
+    fromBytes :: ByteString -> Sem r (Term Natural)
+    fromBytes b = TermAtom <$> asSimpleErrorShow @NockNaturalNaturalError (byteStringToAtom @Natural b)
 
 -- | Calls Anoma.Protobuf.Mempool.AddTransaction
 addTransaction ::

app/Commands/Dev/Anoma/Prove.hs

@@ -10,7 +10,7 @@ import Juvix.Compiler.Nockma.Pretty hiding (Path)
 
 runCommand :: forall r. (Members (Anoma ': Error SimpleError ': AppEffects) r) => ProveOptions -> Sem r ()
 runCommand opts = do
-  res <- runNock ParsedArgsModePretty (opts ^. proveFile) (opts ^. proveArgs)
+  res <- runNock (opts ^. proveFile) (opts ^. proveArgs)
   let traces = res ^. runNockmaTraces
   forM_ traces (renderStdOutLn . ppOutDefault)
   let provedCode = Encoding.jamToByteString (res ^. runNockmaResult)

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

@@ -1,10 +1,15 @@
-module Commands.Dev.Anoma.Prove.Options where
+module Commands.Dev.Anoma.Prove.Options
+  ( module Commands.Dev.Anoma.Prove.Options,
+    module Commands.Dev.Anoma.Prove.Options.ProveArg,
+  )
+where
 
+import Commands.Dev.Anoma.Prove.Options.ProveArg
 import CommonOptions
 
 data ProveOptions = ProveOptions
   { _proveFile :: AppPath File,
-    _proveArgs :: Maybe (AppPath File),
+    _proveArgs :: [ProveArg],
     _proveOutputFile :: Maybe (AppPath File)
   }
   deriving stock (Data)
@@ -14,6 +19,6 @@ makeLenses ''ProveOptions
 parseProveOptions :: Parser ProveOptions
 parseProveOptions = do
   _proveFile <- parseInputFile FileExtNockma
-  _proveArgs <- optional anomaArgsOpt
+  _proveArgs <- many parseProveArg
   _proveOutputFile <- optional parseGenericOutputFile
   pure ProveOptions {..}

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

@@ -0,0 +1,83 @@
+module Commands.Dev.Anoma.Prove.Options.ProveArg
+  ( ProveArg (..),
+    parseProveArg,
+  )
+where
+
+import Commands.Dev.Anoma.Prove.Options.ProveArgTag
+import CommonOptions
+import Juvix.Data.IntegerWithBase
+import Juvix.Parser.Lexer
+import Juvix.Prelude.Parsing hiding (many, option)
+
+type Parse = Parsec Void Text
+
+newtype ProveArg' = ProveArg'
+  { _proveArg :: Sigma ProveArgTag ProveArgTypeSym0
+  }
+
+data ProveArg
+  = ProveArgNat Natural
+  | ProveArgBase64 (AppPath File)
+  | ProveArgBytes (AppPath File)
+  deriving stock (Data)
+
+parseProveArg :: Parser ProveArg
+parseProveArg = fromProveArg' <$> parseProveArg'
+  where
+    fromProveArg' :: ProveArg' -> ProveArg
+    fromProveArg' (ProveArg' (ty :&: a)) = case ty of
+      SProveArgTagNat -> ProveArgNat a
+      SProveArgTagBase64 -> ProveArgBase64 a
+      SProveArgTagBytes -> ProveArgBytes a
+
+parseProveArg' :: Parser ProveArg'
+parseProveArg' =
+  option
+    pp
+    ( long "arg"
+        <> completer (listCompleter [show a <> ":" | a <- allElements @ProveArgTag])
+        <> metavar "ARG_TYPE:ARG"
+        <> helpDoc ("An argument to the program:" <> line <> proveArgTagHelp)
+    )
+  where
+    pProveArgTag :: Parse ProveArgTag
+    pProveArgTag =
+      choice
+        [ chunk (show a) $> a
+          | a :: ProveArgTag <- allElements
+        ]
+
+    pAppPath :: Parse (AppPath File)
+    pAppPath = do
+      i <- mkPrepath . unpack <$> takeRest
+      return
+        AppPath
+          { _pathIsInput = True,
+            _pathPath = i
+          }
+
+    pProveArg' :: Parse ProveArg'
+    pProveArg' = do
+      dty <- pProveArgTag
+      withSomeSing dty $ \ty -> do
+        chunk ":"
+        a <- pProveArgType ty
+        return (ProveArg' (ty :&: a))
+
+    pProveArgType :: SProveArgTag t -> Parse (ProveArgType t)
+    pProveArgType p = do
+      ret <- case p of
+        SProveArgTagBytes -> pAppPath
+        SProveArgTagBase64 -> pAppPath
+        SProveArgTagNat -> do
+          off <- getOffset
+          i <- (^. withLocParam . integerWithBaseValue) <$> integerWithBase'
+          if
+              | i < 0 -> parseFailure off "Expected a non-negative integer"
+              | otherwise -> return (fromIntegral i)
+      eof
+      return ret
+
+    pp :: ReadM ProveArg'
+    pp = eitherReader $ \strInput -> parseHelper pProveArg' (pack strInput)

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

@@ -0,0 +1,42 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Commands.Dev.Anoma.Prove.Options.ProveArgTag where
+
+import CommonOptions
+import Prelude qualified
+
+data ProveArgTag
+  = ProveArgTagNat
+  | ProveArgTagBase64
+  | ProveArgTagBytes
+  deriving stock (Eq, Bounded, Enum, Data)
+
+instance Show ProveArgTag where
+  show = \case
+    ProveArgTagNat -> "nat"
+    ProveArgTagBase64 -> "base64"
+    ProveArgTagBytes -> "bytes"
+
+type ProveArgType :: ProveArgTag -> GHCType
+type family ProveArgType s = res where
+  ProveArgType 'ProveArgTagNat = Natural
+  ProveArgType 'ProveArgTagBase64 = AppPath File
+  ProveArgType 'ProveArgTagBytes = AppPath File
+
+$(genDefunSymbols [''ProveArgType])
+$(genSingletons [''ProveArgTag])
+
+proveArgTagHelp :: AnsiDoc
+proveArgTagHelp = itemize (tagHelp <$> allElements)
+  where
+    tagHelp :: ProveArgTag -> AnsiDoc
+    tagHelp t =
+      let mvar, explain :: AnsiDoc
+          (mvar, explain) = first sty $ case t of
+            ProveArgTagNat -> ("NATURAL", "is passed verbatim as a nockma atom")
+            ProveArgTagBase64 -> ("FILE", "is a file with a base64 encoded nockma atom")
+            ProveArgTagBytes -> ("FILE", "is a file with a byte encoded nockma atom")
+          sty = annotate (bold <> colorDull Blue)
+          tagvar :: AnsiDoc
+          tagvar = sty (show t <> ":" <> mvar)
+       in tagvar <+> "where" <+> mvar <+> explain

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

@@ -3,18 +3,19 @@ module Commands.Dev.Nockma.Run.Anoma where
 import Anoma.Effect
 import Commands.Base hiding (Atom)
 import Commands.Dev.Anoma.Base
+import Commands.Dev.Anoma.Prove.Options.ProveArg
 import Juvix.Compiler.Nockma.Pretty
 
 data RunCommandArgs = RunCommandArgs
-  { _runCommandArgsFile :: Maybe (AppPath File),
+  { _runCommandArgs :: [ProveArg],
     _runCommandProgramFile :: AppPath File
   }
 
 makeLenses ''RunCommandArgs
 
 runInAnoma :: forall r. (Members '[Error SimpleError, Anoma] r, Members AppEffects r) => RunCommandArgs -> Sem r ()
 runInAnoma runArgs = do
-  res <- runNock ParsedArgsModeJammedOrPretty (runArgs ^. runCommandProgramFile) (runArgs ^. runCommandArgsFile)
+  res <- runNock (runArgs ^. runCommandProgramFile) (runArgs ^. runCommandArgs)
   let traces = res ^. runNockmaTraces
   renderStdOutLn (annotate AnnImportant $ "Traces (" <> show (length traces) <> "):")
   forM_ traces $ \tr ->

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

@@ -15,5 +15,5 @@ runCommand opts = do
     runArgs =
       RunCommandArgs
         { _runCommandProgramFile = opts ^. nockmaRunEphemeralFile,
-          _runCommandArgsFile = opts ^. nockmaRunEphemeralArgs
+          _runCommandArgs = opts ^. nockmaRunEphemeralArgs
         }

app/Commands/Dev/Nockma/Run/EphemeralClient/Options.hs

@@ -1,11 +1,12 @@
 module Commands.Dev.Nockma.Run.EphemeralClient.Options where
 
+import Commands.Dev.Anoma.Prove.Options.ProveArg
 import CommonOptions
 
 data NockmaRunEphemeralClientOptions = NockmaRunEphemeralClientOptions
   { _nockmaRunEphemeralFile :: AppPath File,
     _nockmaRunEphemeralAnomaDir :: AppPath Dir,
-    _nockmaRunEphemeralArgs :: Maybe (AppPath File)
+    _nockmaRunEphemeralArgs :: [ProveArg]
   }
   deriving stock (Data)
 
@@ -14,6 +15,6 @@ makeLenses ''NockmaRunEphemeralClientOptions
 parseNockmaRunEphemeralClientOptions :: Parser NockmaRunEphemeralClientOptions
 parseNockmaRunEphemeralClientOptions = do
   _nockmaRunEphemeralFile <- parseInputFile FileExtNockma
-  _nockmaRunEphemeralArgs <- optional anomaArgsOpt
+  _nockmaRunEphemeralArgs <- many parseProveArg
   _nockmaRunEphemeralAnomaDir <- anomaDirOpt
   pure NockmaRunEphemeralClientOptions {..}

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

@@ -20,5 +20,5 @@ runCommand opts =
     runArgs =
       RunCommandArgs
         { _runCommandProgramFile = opts ^. nockmaRunWithClientFile,
-          _runCommandArgsFile = opts ^. nockmaRunWithClientArgs
+          _runCommandArgs = opts ^. nockmaRunWithClientArgs
         }

app/Commands/Dev/Nockma/Run/WithClient/Options.hs

@@ -1,13 +1,14 @@
 module Commands.Dev.Nockma.Run.WithClient.Options where
 
+import Commands.Dev.Anoma.Prove.Options.ProveArg
 import CommonOptions
 
 data NockmaRunWithClientOptions = NockmaRunWithClientOptions
   { _nockmaRunWithClientFile :: AppPath File,
     _nockmaRunWithClientGrpcPort :: Int,
     _nockmaRunWithClientNodeId :: Text,
     _nockmaRunWithClientUrl :: String,
-    _nockmaRunWithClientArgs :: Maybe (AppPath File)
+    _nockmaRunWithClientArgs :: [ProveArg]
   }
   deriving stock (Data)
 
@@ -16,7 +17,7 @@ makeLenses ''NockmaRunWithClientOptions
 parseNockmaRunWithClientOptions :: Parser NockmaRunWithClientOptions
 parseNockmaRunWithClientOptions = do
   _nockmaRunWithClientFile <- parseInputFile FileExtNockma
-  _nockmaRunWithClientArgs <- optional anomaArgsOpt
+  _nockmaRunWithClientArgs <- many parseProveArg
   _nockmaRunWithClientGrpcPort <-
     option
       (fromIntegral <$> naturalNumberOpt)

app/CommonOptions.hs

@@ -226,17 +226,15 @@ fieldSizeOpt = eitherReader aux
       "cairo" -> Right $ Just cairoFieldSize
       "small" -> Right $ Just smallFieldSize
       _ ->
-        mapRight Just
-          . either Left checkAllowed
-          $ maybe (Left $ s <> " is not a valid field size") Right (readMaybe s :: Maybe Natural)
+        mapRight Just (checkAllowed =<< maybe (Left $ s <> " is not a valid field size") Right (readMaybe s :: Maybe Natural))
 
     checkAllowed :: Natural -> Either String Natural
     checkAllowed n
       | n `elem` allowedFieldSizes = Right n
       | otherwise = Left $ Prelude.show n <> " is not a recognized field size"
 
 enumHelp :: forall a. (Bounded a, Enum a, Show a) => (a -> AnsiDoc) -> AnsiDoc
-enumHelp showHelp = vsep ["• " <> annotate bold (show x) <> ": " <> showHelp x | x <- allElements]
+enumHelp showHelp = itemize [annotate bold (show x) <> ": " <> showHelp x | x <- allElements]
 
 enumReader :: forall a. (Bounded a, Enum a, Show a) => Proxy a -> ReadM a
 enumReader _ = eitherReader $ \val ->

src/Juvix/Compiler/Concrete/Data.hs

@@ -14,6 +14,7 @@ module Juvix.Compiler.Concrete.Data
     module Juvix.Compiler.Concrete.Data.IsOpenShort,
     module Juvix.Compiler.Concrete.Data.LocalModuleOrigin,
     module Juvix.Data.NameId,
+    module Juvix.Data.IntegerWithBase,
   )
 where
 
@@ -30,5 +31,6 @@ import Juvix.Compiler.Concrete.Data.PublicAnn
 import Juvix.Compiler.Concrete.Data.ScopedName qualified
 import Juvix.Compiler.Concrete.Data.VisibilityAnn
 import Juvix.Compiler.Store.Scoped.Data.InfoTable
+import Juvix.Data.IntegerWithBase
 import Juvix.Data.NameId
 import Juvix.Data.NameKind