saw-remote-api/feat: add docs, argo submodule bump (#1017)

* saw-remote-api/feat: add docs, argo submodule bump

* PR comment fixes, colocate docs with their methods

* PR requested tweak

* chore: add missing doc for saveTerm

* build fixes

Author: Andrew Kent

deps/argo

@@ -1,11 +1,9 @@
 {-# LANGUAGE OverloadedStrings #-}
 module Main (main) where
 
-import qualified Data.Aeson as JSON
-import Data.Text (Text)
-
 import Argo
 import Argo.DefaultMain
+import qualified Argo.Doc as Doc
 
 import SAWServer
 import SAWServer.CryptolSetup
@@ -20,32 +18,79 @@ import SAWServer.SetOption
 
 main :: IO ()
 main =
-  do theApp <- mkApp initialState sawMethods
+  do theApp <- mkApp "SAW RPC Server" serverDocs initialState sawMethods
      defaultMain description theApp
 
+serverDocs :: [Doc.Block]
+serverDocs =
+  [ Doc.Section "Summary" $ [ Doc.Paragraph
+    [Doc.Text "A remote server for ",
+     Doc.Link (Doc.URL "https://saw.galois.com/") "SAW",
+     Doc.Text " for verifying programs with a featureset similar to SAWScript."]]]
+
 description :: String
 description =
   "An RPC server for SAW."
 
-sawMethods :: [(Text, MethodType, JSON.Value -> Method SAWState JSON.Value)]
+sawMethods :: [AppMethod SAWState]
 sawMethods =
   -- Cryptol
-  [ ("SAW/Cryptol/load module",  Command, method cryptolLoadModule)
-  , ("SAW/Cryptol/load file",    Command, method cryptolLoadFile)
-  , ("SAW/Cryptol/save term",    Command, method saveTerm)
+  [ method
+     "SAW/Cryptol/load module"
+     Command
+     cryptolLoadModuleDescr
+     cryptolLoadModule
+  , method
+     "SAW/Cryptol/load file"
+     Command
+     cryptolLoadFileDescr
+     cryptolLoadFile
+  , method
+     "SAW/Cryptol/save term"
+     Command
+     saveTermDescr
+     saveTerm
   -- JVM
   {-
-  , ("SAW/JVM/load class",       Command, method jvmLoadClass)
-  , ("SAW/JVM/verify",           Command, method jvmVerify)
-  , ("SAW/JVM/assume",           Command, method jvmAssume)
+  , method "SAW/JVM/load class" Command (Doc.Paragraph [Doc.Text "TODO"]) jvmLoadClass
+  , method "SAW/JVM/verify"     Command (Doc.Paragraph [Doc.Text "TODO"]) jvmVerify
+  , method "SAW/JVM/assume"     Command (Doc.Paragraph [Doc.Text "TODO"]) jvmAssume
   -}
   -- LLVM
-  , ("SAW/LLVM/load module",     Command, method llvmLoadModule)
-  , ("SAW/LLVM/verify",          Command, method llvmVerify)
-  , ("SAW/LLVM/verify x86",      Command, method llvmVerifyX86)
-  , ("SAW/LLVM/assume",          Command, method llvmAssume)
+  , method
+     "SAW/LLVM/load module"
+     Command
+     llvmLoadModuleDescr
+     llvmLoadModule
+  , method
+     "SAW/LLVM/verify"
+     Command
+     llvmVerifyDescr
+     llvmVerify
+  , method
+     "SAW/LLVM/verify x86"
+     Command
+     llvmVerifyX86Descr
+     llvmVerifyX86
+  , method
+     "SAW/LLVM/assume"
+     Command
+     llvmAssumeDescr
+     llvmAssume
   -- General
-  , ("SAW/make simpset",         Command, method makeSimpset)
-  , ("SAW/prove",                Command, method prove)
-  , ("SAW/set option",           Command, method setOption)
+  , method
+     "SAW/make simpset"
+     Command
+     makeSimpsetDescr
+     makeSimpset
+  , method
+     "SAW/prove"
+     Command
+     proveDescr
+     prove
+  , method
+     "SAW/set option"
+     Command
+     setOptionDescr
+     setOption
   ]

saw-remote-api/saw-remote-api/Main.hs

@@ -4,7 +4,9 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 module SAWServer.CryptolSetup
   ( cryptolLoadFile
+  , cryptolLoadFileDescr
   , cryptolLoadModule
+  , cryptolLoadModuleDescr
   ) where
 
 import Control.Exception (SomeException, try)
@@ -19,10 +21,15 @@ import SAWScript.Value (biSharedContext, rwCryptol)
 import qualified Verifier.SAW.CryptolEnv as CEnv
 
 import Argo
+import qualified Argo.Doc as Doc
 import SAWServer
 import SAWServer.Exceptions
 import SAWServer.OK
 
+cryptolLoadModuleDescr :: Doc.Block
+cryptolLoadModuleDescr =
+  Doc.Paragraph [Doc.Text "Load the specified Cryptol module."]
+
 cryptolLoadModule :: CryptolLoadModuleParams -> Method SAWState OK
 cryptolLoadModule (CryptolLoadModuleParams modName) =
   do sc <- biSharedContext . view sawBIC <$> getState
@@ -46,6 +53,18 @@ instance FromJSON CryptolLoadModuleParams where
     withObject "params for \"SAW/Cryptol setup/load module\"" $ \o ->
     CryptolLoadModuleParams . textToModName <$> o .: "module name"
 
+instance Doc.DescribedParams CryptolLoadModuleParams where
+  parameterFieldDescription =
+    [ ("module name",
+       Doc.Paragraph [Doc.Text "Name of module to load."])
+    ]
+
+
+cryptolLoadFileDescr :: Doc.Block
+cryptolLoadFileDescr =
+  Doc.Paragraph [Doc.Text "Load the given file as a Cryptol module."]
+
+
 cryptolLoadFile :: CryptolLoadFileParams -> Method SAWState OK
 cryptolLoadFile (CryptolLoadFileParams fileName) =
   do sc <- biSharedContext . view sawBIC <$> getState
@@ -68,3 +87,9 @@ instance FromJSON CryptolLoadFileParams where
   parseJSON =
     withObject "params for \"SAW/Cryptol setup/load file\"" $ \o ->
     CryptolLoadFileParams . T.unpack <$> o .: "file"
+
+instance Doc.DescribedParams CryptolLoadFileParams where
+  parameterFieldDescription =
+    [ ("file",
+       Doc.Paragraph [Doc.Text "File to load as a Cryptol module."])
+    ]

saw-remote-api/src/SAWServer/CryptolSetup.hs

@@ -37,6 +37,7 @@ import Verifier.SAW.CryptolEnv (CryptolEnv)
 import Verifier.SAW.TypedTerm (TypedTerm)
 
 import Argo
+import qualified Argo.Doc as Doc
 import SAWServer
 import SAWServer.Data.Contract
 import SAWServer.Data.SetupValue ()
@@ -58,6 +59,12 @@ instance FromJSON StartJVMSetupParams where
     withObject "params for \"SAW/Crucible setup\"" $ \o ->
     StartJVMSetupParams <$> o .: "name"
 
+instance Doc.DescribedParams StartJVMSetupParams where
+  parameterFieldDescription =
+    [ ("name",
+       Doc.Paragraph [Doc.Text "The name of the item to setup on the server."])
+    ]
+
 data ServerSetupVal = Val (SetupValue CJ.JVM)
 
 -- TODO: this is an extra layer of indirection that could be collapsed, but is easy to implement for now.
@@ -187,3 +194,11 @@ jvmLoadClass (JVMLoadClassParams serverName cname) =
          do c <- tl $ loadJavaClass cname
             setServerVal serverName c
             ok
+
+instance Doc.DescribedParams JVMLoadClassParams where
+  parameterFieldDescription =
+    [ ("name",
+        Doc.Paragraph [Doc.Text "The name of the class on the server."])
+    , ("class",
+      Doc.Paragraph [Doc.Text "The java class to load."])
+    ]

saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs

@@ -10,6 +10,7 @@
 module SAWServer.LLVMCrucibleSetup
   ( startLLVMCrucibleSetup
   , llvmLoadModule
+  , llvmLoadModuleDescr
   , Contract(..)
   , ContractVar(..)
   , Allocated(..)
@@ -51,6 +52,7 @@ import Verifier.SAW.CryptolEnv (CryptolEnv)
 import Verifier.SAW.TypedTerm (TypedTerm)
 
 import Argo
+import qualified Argo.Doc as Doc
 import SAWServer
 import SAWServer.Data.Contract
 import SAWServer.Data.LLVMType (JSONLLVMType, llvmType)
@@ -192,6 +194,19 @@ instance FromJSON LLVMLoadModuleParams where
     withObject "params for \"SAW/LLVM/load module\"" $ \o ->
     LLVMLoadModuleParams <$> o .: "name" <*> o .: "bitcode file"
 
+
+instance Doc.DescribedParams LLVMLoadModuleParams where
+  parameterFieldDescription =
+    [ ("name",
+        Doc.Paragraph [Doc.Text "The name to refer to the loaded module by later."])
+    , ("bitcode file",
+       Doc.Paragraph [Doc.Text "The file containing the bitcode LLVM module to load."])
+    ]
+
+llvmLoadModuleDescr :: Doc.Block
+llvmLoadModuleDescr =
+  Doc.Paragraph [Doc.Text "Load the specified LLVM module."]
+
 llvmLoadModule :: LLVMLoadModuleParams -> Method SAWState OK
 llvmLoadModule (LLVMLoadModuleParams serverName fileName) =
   do tasks <- view sawTask <$> getState

saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs

@@ -2,8 +2,11 @@
 
 module SAWServer.LLVMVerify
   ( llvmVerify
+  , llvmVerifyDescr
   , llvmVerifyX86
+  , llvmVerifyX86Descr
   , llvmAssume
+  , llvmAssumeDescr
   ) where
 
 import Prelude hiding (mod)
@@ -14,6 +17,7 @@ import SAWScript.Crucible.LLVM.X86
 import SAWScript.Value (rwCryptol)
 
 import Argo
+import qualified Argo.Doc as Doc
 import CryptolServer.Data.Expression
 import SAWServer
 import SAWServer.Data.Contract
@@ -49,13 +53,36 @@ llvmVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract scr
             setServerVal lemmaName res
             ok
 
+
+
+llvmVerifyDescr :: Doc.Block
+llvmVerifyDescr =
+  Doc.Paragraph [Doc.Text "Verify the named LLVM function meets its specification."]
+
 llvmVerify :: VerifyParams JSONLLVMType -> Method SAWState OK
 llvmVerify = llvmVerifyAssume VerifyContract
 
+
+
+
+
+llvmAssumeDescr :: Doc.Block
+llvmAssumeDescr =
+  Doc.Paragraph [Doc.Text $ "Assume the function meets its specification."]
+
 llvmAssume :: AssumeParams JSONLLVMType -> Method SAWState OK
 llvmAssume (AssumeParams modName fun contract lemmaName) =
   llvmVerifyAssume AssumeContract (VerifyParams modName fun [] False contract (ProofScript []) lemmaName)
 
+
+
+
+
+llvmVerifyX86Descr :: Doc.Block
+llvmVerifyX86Descr =
+  Doc.Paragraph [ Doc.Text "Verify an x86 function from an ELF file for use as"
+                , Doc.Text " an override in an LLVM verification meets its specification."]
+
 llvmVerifyX86 :: X86VerifyParams JSONLLVMType -> Method SAWState OK
 llvmVerifyX86 (X86VerifyParams modName objName fun globals _lemmaNames checkSat contract script lemmaName) =
   do tasks <- view sawTask <$> getState

saw-remote-api/src/SAWServer/LLVMVerify.hs

@@ -1,6 +1,7 @@
 module SAWServer.NoParams (NoParams(..)) where
 
 import Data.Aeson
+import qualified Argo.Doc as Doc
 
 data NoParams = NoParams
 
@@ -9,3 +10,6 @@ instance ToJSON NoParams where
 
 instance FromJSON NoParams where
   parseJSON = withObject "no parameters" (const (pure NoParams))
+
+instance Doc.DescribedParams NoParams where
+  parameterFieldDescription = []

saw-remote-api/src/SAWServer/NoParams.hs

@@ -4,7 +4,9 @@ module SAWServer.ProofScript
   ( ProofScript(..)
   , interpretProofScript
   , makeSimpset
+  , makeSimpsetDescr
   , prove
+  , proveDescr
   ) where
 
 import Control.Applicative
@@ -13,6 +15,7 @@ import Data.Aeson
 import Data.Text (Text)
 
 import Argo
+import qualified Argo.Doc as Doc
 import qualified SAWScript.Builtins as SB
 import qualified SAWScript.Value as SV
 import SAWServer
@@ -83,6 +86,19 @@ instance FromJSON MakeSimpsetParams where
     MakeSimpsetParams <$> o .: "elements"
                       <*> o .: "result"
 
+instance Doc.DescribedParams MakeSimpsetParams where
+  parameterFieldDescription =
+    [ ("elements",
+       Doc.Paragraph [Doc.Text "The items to include in the simpset."])
+    , ("result",
+       Doc.Paragraph [Doc.Text "The name to assign to this simpset."])
+    ]
+
+
+makeSimpsetDescr :: Doc.Block
+makeSimpsetDescr =
+  Doc.Paragraph [Doc.Text "Create a simplification rule set from the given rules."]
+
 makeSimpset :: MakeSimpsetParams -> Method SAWState OK
 makeSimpset params = do
   let add ss n = do
@@ -107,6 +123,14 @@ instance FromJSON ProveParams where
     ProveParams <$> o .: "script"
                 <*> o .: "term"
 
+instance Doc.DescribedParams ProveParams where
+  parameterFieldDescription =
+    [ ("script",
+       Doc.Paragraph [Doc.Text "Script to use to prove the term."])
+    , ("term",
+       Doc.Paragraph [Doc.Text "The term to interpret as a theorm and prove."])
+    ]
+
 --data CexValue = CexValue String TypedTerm
 
 data ProveResult
@@ -121,6 +145,12 @@ instance ToJSON ProveResult where
   toJSON ProofInvalid {-cex-} =
     object [ "status" .= ("invalid" :: Text) ] -- , "counterexample" .= cex]
 
+
+proveDescr :: Doc.Block
+proveDescr =
+  Doc.Paragraph [ Doc.Text "Attempt to prove the given term representing a"
+                , Doc.Text " theorem, given a proof script context."]
+
 prove :: ProveParams -> Method SAWState ProveResult
 prove params = do
   t <- getTerm (ppTermName params)