Cryptol Projects

cryptol-remote-api/src/CryptolServer.hs

@@ -195,6 +195,6 @@ validateServerState =
         InMem{} -> continue
         InFile file ->
           do fp <- fingerprintFile file
-             if fp == Just (fiFingerprint (lmFileInfo lm))
+             if fp == Right (fiFingerprint (lmFileInfo lm))
                then continue
                else return False

cryptol-remote-api/src/CryptolServer/FileDeps.hs

@@ -9,6 +9,7 @@ module CryptolServer.FileDeps
 import Data.Text (Text)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
+import qualified Data.Map.Strict as Map
 
 import qualified Data.Aeson as JSON
 import Data.Aeson (FromJSON(..),ToJSON(..),(.=),(.:))
@@ -67,7 +68,7 @@ instance ToJSON FileDeps where
                            InFile f  -> toJSON f
                            InMem l _ -> JSON.object [ "internal" .= l ]
       , "fingerprint" .= fingerprintHexString (fiFingerprint fi)
-      , "includes"    .= Set.toList (fiIncludeDeps fi)
+      , "includes"    .= Map.keys (fiIncludeDeps fi)
       , "imports"     .= map (show . pp) (Set.toList (fiImportDeps fi))
       , "foreign"     .= Map.toList (fiForeignDeps fi)
       ]

cryptol.cabal

@@ -63,6 +63,7 @@ library
                        gitrev            >= 1.0,
                        ghc-prim,
                        GraphSCC          >= 1.0.4,
+                       heredoc           >= 0.2,
                        language-c99,
                        language-c99-simple,
                        libBF             >= 0.6 && < 0.7,
@@ -80,6 +81,7 @@ library
                        strict,
                        text              >= 1.1,
                        tf-random         >= 0.5,
+                       toml-parser       >= 2.0 && <2.1,
                        transformers-base >= 0.4,
                        vector,
                        mtl               >= 2.2.1,
@@ -238,7 +240,12 @@ library
                        Cryptol.REPL.Help,
                        Cryptol.REPL.Browse,
                        Cryptol.REPL.Monad,
-                       Cryptol.REPL.Trie
+                       Cryptol.REPL.Trie,
+
+                       Cryptol.Project
+                       Cryptol.Project.Config
+                       Cryptol.Project.Monad
+                       Cryptol.Project.Cache
 
   Other-modules:       Cryptol.Parser.LexerUtils,
                        Cryptol.Parser.ParserUtils,

cryptol/Main.hs

@@ -8,6 +8,7 @@
 
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 module Main where
 
@@ -18,6 +19,7 @@ import Cryptol.REPL.Monad (REPL,updateREPLTitle,setUpdateREPLTitle,
                    io,prependSearchPath,setSearchPath,parseSearchPath)
 import qualified Cryptol.REPL.Monad as REPL
 import Cryptol.ModuleSystem.Env(ModulePath(..))
+import qualified Cryptol.Project as Project
 
 import REPL.Haskeline
 import REPL.Logo
@@ -26,6 +28,7 @@ import Cryptol.Utils.PP
 import Cryptol.Version (displayVersion)
 
 import Control.Monad (when, void)
+import Data.Maybe (isJust, isNothing)
 import GHC.IO.Encoding (setLocaleEncoding, utf8)
 import System.Console.GetOpt
     (OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo)
@@ -47,6 +50,7 @@ data Options = Options
   , optVersion         :: Bool
   , optHelp            :: Bool
   , optBatch           :: ReplMode
+  , optProject         :: Maybe FilePath
   , optCallStacks      :: Bool
   , optCommands        :: [String]
   , optColorMode       :: ColorMode
@@ -62,6 +66,7 @@ defaultOptions  = Options
   , optVersion         = False
   , optHelp            = False
   , optBatch           = InteractiveRepl
+  , optProject         = Nothing
   , optCallStacks      = True
   , optCommands        = []
   , optColorMode       = AutoColor
@@ -79,6 +84,10 @@ options  =
   , Option "" ["interactive-batch"] (ReqArg setInteractiveBatchScript "FILE")
     "run the script provided and exit, but behave as if running an interactive session"
 
+  , Option "p" ["project"] (ReqArg setProject "CRYPROJECT")
+    ("Load and verify a Cryptol project using the provided project "
+      ++ "configuration file or directory containing 'cryproject.toml'")
+
   , Option "e" ["stop-on-error"] (NoArg setStopOnError)
     "stop script execution as soon as an error occurs."
 
@@ -137,6 +146,9 @@ setBatchScript path = modify $ \ opts -> opts { optBatch = Batch path }
 setInteractiveBatchScript :: String -> OptParser Options
 setInteractiveBatchScript path = modify $ \ opts -> opts { optBatch = InteractiveBatch path }
 
+setProject :: String -> OptParser Options
+setProject path = modify $ \opts -> opts { optProject = Just path }
+
 -- | Set the color mode of the terminal output.
 setColorMode :: String -> OptParser Options
 setColorMode "auto"   = modify $ \ opts -> opts { optColorMode = AutoColor }
@@ -225,11 +237,13 @@ main  = do
       | optVersion opts -> displayVersion putStrLn
       | otherwise       -> do
           (opts', mCleanup) <- setupCmdScript opts
-          status <- repl (optCryptolrc opts')
-                         (optBatch opts')
-                         (optCallStacks opts')
-                         (optStopOnError opts')
-                         (setupREPL opts')
+          (opts'', mConfig) <- setupProject opts'
+          status <- repl (optCryptolrc opts'')
+                         mConfig
+                         (optBatch opts'')
+                         (optCallStacks opts'')
+                         (optStopOnError opts'')
+                         (setupREPL opts'')
           case mCleanup of
             Nothing -> return ()
             Just cmdFile -> removeFile cmdFile
@@ -249,7 +263,27 @@ setupCmdScript opts =
       hClose h
       when (optBatch opts /= InteractiveRepl) $
         putStrLn "[warning] --command argument specified; ignoring batch file"
-      return (opts { optBatch = InteractiveBatch path }, Just path)
+      when (isJust (optProject opts)) $
+        putStrLn $
+          "[warning] --command argument specified; "
+          ++ "ignoring project configuration file"
+      return
+        ( opts { optBatch = InteractiveBatch path, optProject = Nothing }
+        , Just path )
+
+setupProject :: Options -> IO (Options, Maybe Project.Config)
+setupProject opts =
+  case optProject opts of
+    Nothing -> pure (opts, Nothing)
+    Just path -> do
+      when (optBatch opts /= InteractiveRepl) $
+        putStrLn "[warning] --project argument specified; ignoring batch file"
+      Project.loadConfig path >>= \case
+        Left err -> do
+          print $ pp err
+          exitFailure
+        Right config ->
+          pure (opts { optBatch = InteractiveRepl }, Just config)
 
 setupREPL :: Options -> REPL ()
 setupREPL opts = do
@@ -281,18 +315,20 @@ setupREPL opts = do
     Batch file -> prependSearchPath [ takeDirectory file ]
     _ -> return ()
 
-  case optLoad opts of
-    []  -> loadPrelude `REPL.catch` \x -> io $ print $ pp x
-    [l] -> void (loadCmd l) `REPL.catch` \x -> do
-             io $ print $ pp x
-             -- If the requested file fails to load, load the prelude instead...
-             loadPrelude `REPL.catch` \y -> do
-               io $ print $ pp y
-             -- ... but make sure the loaded module is set to the file
-             -- we tried, instead of the Prelude
-             REPL.setEditPath l
-             REPL.setLoadedMod REPL.LoadedModule
-               { REPL.lFocus = Nothing
-               , REPL.lPath = InFile l
-               }
-    _   -> io $ putStrLn "Only one file may be loaded at the command line."
+  when (isNothing (optProject opts)) $
+    case optLoad opts of
+      []  -> loadPrelude `REPL.catch` \x -> io $ print $ pp x
+      [l] -> void (loadCmd l) `REPL.catch` \x -> do
+              io $ print $ pp x
+              -- If the requested file fails to load,
+              -- load the prelude instead...
+              loadPrelude `REPL.catch` \y -> do
+                io $ print $ pp y
+              -- ... but make sure the loaded module is set to the file
+              -- we tried, instead of the Prelude
+              REPL.setEditPath l
+              REPL.setLoadedMod REPL.LoadedModule
+                { REPL.lFocus = Nothing
+                , REPL.lPath = InFile l
+                }
+      _   -> io $ putStrLn "Only one file may be loaded at the command line."

cryptol/REPL/Haskeline.hs

@@ -14,6 +14,7 @@
 
 module REPL.Haskeline where
 
+import qualified Cryptol.Project as Project
 import           Cryptol.REPL.Command
 import           Cryptol.REPL.Monad
 import           Cryptol.REPL.Trie
@@ -131,22 +132,29 @@ loadCryRC cryrc =
                            else return status
 
 -- | Haskeline-specific repl implementation.
-repl :: Cryptolrc -> ReplMode -> Bool -> Bool -> REPL () -> IO CommandResult
-repl cryrc replMode callStacks stopOnError begin =
+repl :: Cryptolrc -> Maybe Project.Config -> ReplMode -> Bool -> Bool -> REPL () -> IO CommandResult
+repl cryrc projectConfig replMode callStacks stopOnError begin =
   runREPL isBatch callStacks stdoutLogger replAction
 
  where
   -- this flag is used to suppress the logo and prompts
-  isBatch = case replMode of
-              InteractiveRepl -> False
-              Batch _ -> True
-              InteractiveBatch _ -> True
+  isBatch =
+    case projectConfig of
+      Just _ -> True
+      Nothing ->
+        case replMode of
+          InteractiveRepl -> False
+          Batch _ -> True
+          InteractiveBatch _ -> True
 
   replAction =
     do status <- loadCryRC cryrc
-       if crSuccess status
-         then begin >> crySession replMode stopOnError
-         else return status
+       if crSuccess status then do
+          begin
+          case projectConfig of
+            Just config -> loadProjectREPL config
+            Nothing     -> crySession replMode stopOnError
+       else return status
 
 -- | Try to set the history file.
 setHistoryFile :: Settings REPL -> IO (Settings REPL)

examples/AE.cry

@@ -5,6 +5,7 @@ Implementation of the algorithms from the paper
   "Automated Analysis and Synthesis of Authenticated Encryption Schemes"
   by Viet Tung Hoang, Jonathan Katz, and Alex J. Malozemoff
 */
+module AE where
 
 parameter
   type A : *          // State type