cryptol 3.2.0 → 3.3.0

raw patch · 64 files changed

+3084/−1057 lines, 64 filesdep +cryptohash-sha256dep +heredocdep +tastydep −cryptohash-sha1dep ~basedep ~base-compatdep ~directorynew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies added: cryptohash-sha256, heredoc, tasty, tasty-hunit, toml-parser

Dependencies removed: cryptohash-sha1

Dependency ranges changed: base, base-compat, directory, filepath, haskeline, simple-smt, what4

API changes (from Hackage documentation)

Files

• CHANGES.md +88/−0
• api-tests/Main.hs +114/−0
• cryptol-repl-internal/REPL/Haskeline.hs +401/−0
• cryptol-repl-internal/REPL/Logo.hs +75/−0
• cryptol.cabal +75/−24
• cryptol/Main.hs +73/−22
• cryptol/REPL/Haskeline.hs +0/−356
• cryptol/REPL/Logo.hs +0/−75
• lib/CryptolTC.z3 +13/−4
• src/Cryptol/Backend.hs +8/−1
• src/Cryptol/Backend/Concrete.hs +3/−1
• src/Cryptol/Backend/SBV.hs +2/−1
• src/Cryptol/Backend/What4.hs +2/−1
• src/Cryptol/Backend/WordValue.hs +10/−0
• src/Cryptol/Eval.hs +9/−8
• src/Cryptol/Eval/Concrete.hs +24/−24
• src/Cryptol/Eval/FFI.hs +14/−2
• src/Cryptol/Eval/Generic.hs +110/−95
• src/Cryptol/Eval/Reference.lhs +33/−1
• src/Cryptol/Eval/SBV.hs +1/−1
• src/Cryptol/Eval/Value.hs +94/−27
• src/Cryptol/Eval/What4.hs +8/−8
• src/Cryptol/IR/FreeVars.hs +2/−1
• src/Cryptol/ModuleSystem/Base.hs +59/−27
• src/Cryptol/ModuleSystem/Env.hs +35/−16
• src/Cryptol/ModuleSystem/Fingerprint.hs +30/−14
• src/Cryptol/ModuleSystem/Monad.hs +26/−13
• src/Cryptol/ModuleSystem/Renamer.hs +8/−2
• src/Cryptol/Parser.y +4/−4
• src/Cryptol/Parser/AST.hs +63/−4
• src/Cryptol/Parser/ExpandPropGuards.hs +1/−1
• src/Cryptol/Parser/Names.hs +2/−2
• src/Cryptol/Parser/NoInclude.hs +12/−10
• src/Cryptol/Parser/NoPat.hs +8/−8
• src/Cryptol/Parser/ParserUtils.hs +38/−26
• src/Cryptol/Parser/Position.hs +4/−0
• src/Cryptol/Project.hs +244/−0
• src/Cryptol/Project/Cache.hs +130/−0
• src/Cryptol/Project/Config.hs +75/−0
• src/Cryptol/Project/Monad.hs +214/−0
• src/Cryptol/Project/WildMatch.hs +110/−0
• src/Cryptol/REPL/Command.hs +228/−103
• src/Cryptol/REPL/Monad.hs +49/−8
• src/Cryptol/Symbolic.hs +4/−3
• src/Cryptol/Symbolic/SBV.hs +75/−13
• src/Cryptol/Symbolic/What4.hs +74/−24
• src/Cryptol/Testing/Random.hs +11/−11
• src/Cryptol/TypeCheck.hs +1/−1
• src/Cryptol/TypeCheck/AST.hs +30/−6
• src/Cryptol/TypeCheck/Error.hs +44/−12
• src/Cryptol/TypeCheck/Infer.hs +83/−17
• src/Cryptol/TypeCheck/InferTypes.hs +67/−7
• src/Cryptol/TypeCheck/ModuleBacktickInstance.hs +1/−1
• src/Cryptol/TypeCheck/Monad.hs +9/−4
• src/Cryptol/TypeCheck/SimpType.hs +43/−10
• src/Cryptol/TypeCheck/Solve.hs +8/−10
• src/Cryptol/TypeCheck/Solver/Numeric.hs +13/−4
• src/Cryptol/TypeCheck/Solver/SMT.hs +38/−9
• src/Cryptol/TypeCheck/Subst.hs +1/−1
• src/Cryptol/TypeCheck/Type.hs +2/−2
• src/Cryptol/TypeCheck/TypePat.hs +4/−1
• src/Cryptol/Utils/Ident.hs +66/−28
• src/Cryptol/Utils/PP.hs +7/−3
• src/Cryptol/Utils/Patterns.hs +4/−0

@@ -1,3 +1,91 @@+# 3.3.0 -- 2025-03-21++## Language changes++## Bug fixes++* Fix a bug where setting at timeout would cause+  sbv-yices, sbv-cvc4 and sbc-cvc5 to crash.+  Uses a deadman timer workaround for yices, due+  to a [known issue](https://github.com/LeventErkok/sbv/issues/735).+  ([#1808](https://github.com/GaloisInc/cryptol/issues/1808))++* Update Yices build in CI to fix a crash when running+  test `issue_1807.icry` on Mac OS X (ARM64).+  ([what4-solvers #58](https://github.com/GaloisInc/what4-solvers/issues/58))++* Fix a bug where using a timeout with a subset of the what4 solvers+  would cause a runtime error. Includes a version bump for what4 to address+  a nondeterministic crash when using timeouts with cvc4/5.+  ([what4 PR #288](https://github.com/GaloisInc/what4/pull/288))+  ([#1807](https://github.com/GaloisInc/cryptol/issues/1807))++* Fix #1437, enforce the VSeq invariant that it is not a sequence of bits.+  Replaces the VSeq constructor with a view-only pattern, and smart constructors+  `mkSeq` and `finSeq`.+  ([#1437](https://github.com/GaloisInc/cryptol/issues/1437))++* Fix #1740, removes duplicated width from word values.+  Note that since this changes the types, it may require changes to libraries+  depending on Cryptol.++* Fix a bug in which splitting a `[0]` value into type `[inf][0]` would panic.+  ([#1749](https://github.com/GaloisInc/cryptol/issues/1749))++* Fix a bug in which the free variables of types mentioning newtypes or enums+  were incorrectly computed.+  ([#1773](https://github.com/GaloisInc/cryptol/issues/1773))++* The reference evaluator now evaluates the `toSignedInteger` and `deepseq`+  primitives instead of panicking.++* Fix a bug in which `a ^^ (x ^^ y)` could be incorrectly simplified to+  `a ^^ (x * y)` at the type level.+  ([#1799](https://github.com/GaloisInc/cryptol/issues/1799))++## New features++* Improved error messages during type inference for bindings.+  Adds a specific error message for when a binding has+  more arguments than expected, given its type signature.+  ([#1744](https://github.com/GaloisInc/cryptol/issues/1744))++* Improved warning messages for non-exhaustive guards.+  Warnings are now ordered by source location.+  ([#1798](https://github.com/GaloisInc/cryptol/issues/1798))++* More aggressive exhaustivity check that is less dependent on+  guard ordering.+  ([#1796](https://github.com/GaloisInc/cryptol/issues/1796))++* Improved error messages mentioning module parameters+  ([#1560](https://github.com/GaloisInc/cryptol/issues/1560))++* Improved the naming convention for anonymous modules generated by the+  module system ([#1810](https://github.com/GaloisInc/cryptol/issues/1810))++* REPL command `:dumptests <FILE> <EXPR>` updated to write to stdout when+  invoked as `:dumptests - <EXPR>` allowing for easier experimentation and+  testing.++* The REPL properly supports tab completion for the `:t` and `:check` commands.+  ([#1780](https://github.com/GaloisInc/cryptol/issues/1780))++* Add support for incrementally loading projects via cryptol's `--project`+  flag as documented in the reference manual.+  ([#1641](https://github.com/GaloisInc/cryptol/issues/1641))++* Add support for the Bitwuzla SMT solver, which can be selected with+  `:set prover=bitwuzla`. If you want to specify a What4 or SBV backend, you can+  use `:set prover=w4-bitwuzla` or `:set prover=sbv-bitwuzla`, respectively.+  ([#1786](https://github.com/GaloisInc/cryptol/issues/1786))++* Add a REPL option `tcSmtFile` that allows writing typechecker-related SMT+  solver interactions to a file.++* The typechecker can now simplify types of the form `width (2^^n)` to `n + 1`.+  ([#1802](https://github.com/GaloisInc/cryptol/issues/1802))+ # 3.2.0 -- 2024-08-20  ## Language changes

@@ -0,0 +1,114 @@+{-# LANGUAGE ScopedTypeVariables #-}+module Main (main) where++import Data.Foldable (traverse_)+import System.Console.Haskeline.Completion (Completion(..))+import Test.Tasty+import Test.Tasty.HUnit++import qualified Cryptol.REPL.Command as REPL+import qualified Cryptol.REPL.Monad as REPL+import Cryptol.REPL.Monad (REPL)+import Cryptol.Utils.Logger (quietLogger)+import Cryptol.Utils.PP (pp)++import REPL.Haskeline (cryptolCommand)++main :: IO ()+main = defaultMain $+  testGroup "Cryptol API tests"+    [ testGroup "Tab completion tests" $+      map (uncurry replTabCompletionTestCase)+        [ (":ch", ":check")+        , (":check", ":check")+        , (":check ", ":check ")+        , (":check rev", ":check reverse")+        , (":check-docstrings", ":check-docstrings ")+        , (":check-docstrings ", ":check-docstrings ")+        , (":t", ":t")+        , (":t rev", ":t reverse")+        , (":time", ":time ")+        , (":time ", ":time ")+        , (":time rev", ":time reverse")+        , (":type", ":type ")+        , (":type ", ":type ")+        , (":type rev", ":type reverse")+        ]+    ]++-- | Assert a property in the 'REPL' monad and turn it into a test case.+replTestCase :: TestName -> REPL () -> TestTree+replTestCase name replAssertion =+  testCase name $+  REPL.runREPL+    False       -- Don't use batch mode+    False       -- Disable call stacks+    quietLogger -- Ignore all log messages+    replAssertion++-- | Assert that the REPL will tab-complete the given input in one specific way.+replTabCompletionTestCase ::+  -- | The input before the cursor just prior to hitting the tab key.+  String ->+  -- | The expected terminal input after hitting the tab key. Note that although+  -- this is specified as a single 'String', this may actually correspond to+  -- multiple Haskeline 'Completion's under the hood. See the comments below for+  -- details on how multiple 'Completion's are resolved to a single 'String'.+  String ->+  TestTree+replTabCompletionTestCase beforeTab afterTabExpected =+  replTestCase (show beforeTab ++ " --> " ++ show afterTabExpected) $+  do -- Load the prelude so that the REPL knows how to tab-complete prelude+     -- definitions.+     REPL.loadPrelude+     -- Perform the actual tab completion. (Oddly, Haskeline requires that the+     -- input to the left of the cursor should be reversed.)+     (_input, completions) <- cryptolCommand (reverse beforeTab, "")+     -- Check that the results match what is expected. We have to do a bit of+     -- additional work that Haskeline does not do:+     --+     -- 1. If there is exactly one Completion and its replacement value is+     --    empty, then Haskeline will add a space character to the end of the+     --    input on the terminal. Oddly, this space character is /not/ added in+     --    the Completion itself. As such, we have to add this ourselves.+     --+     -- 2. If there are multiple completions, then Haskeline will complete the+     --    terminal input up to the longest common prefix of all the+     --    completions' replacement strings. As such, we compute this longest+     --    common prefix ourselves.+     REPL.io $+       case completions of+         [] -> assertFailure "Expected tab completions, but received none"+         [completion] ->+           do assertFinished completion+              let replace = replacement completion+                  afterTabActual+                    | null replace = -- See (1) above+                                     beforeTab ++ " "+                    | otherwise    = beforeTab ++ replace+              afterTabExpected @=? afterTabActual+         _:_ ->+           do traverse_ assertFinished completions+              let replaceLcp =+                    -- See (2) above+                    longestCommonPrefix (map replacement completions)+                  afterTabActual = beforeTab ++ replaceLcp+              afterTabExpected @=? afterTabActual+  `REPL.catch`+    -- If something goes wrong run running the REPL, report it as a test+    -- failure.+    \x -> REPL.io $ assertFailure $ show $ pp x+  where+    assertFinished :: Completion -> Assertion+    assertFinished completion =+      assertBool ("Tab completion for " ++ display completion ++ " finished")+                 (isFinished completion)++-- | Compute the longest common prefix in a list of lists.+longestCommonPrefix :: forall a. Eq a => [[a]] -> [a]+longestCommonPrefix [] = []+longestCommonPrefix s = foldr1 lcp s+  where+    lcp :: [a] -> [a] -> [a]+    lcp xs ys = map fst $ takeWhile (uncurry (==))+                        $ zip xs ys

@@ -0,0 +1,401 @@+-- |+-- Module      :  REPL.Haskeline+-- Copyright   :  (c) 2013-2016 Galois, Inc.+-- License     :  BSD3+-- Maintainer  :  cryptol@galois.com+-- Stability   :  provisional+-- Portability :  portable++{-# LANGUAGE CPP #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE BangPatterns #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}++module REPL.Haskeline where++import qualified Cryptol.Project as Project+import           Cryptol.REPL.Command+import           Cryptol.REPL.Monad+import           Cryptol.REPL.Trie+import           Cryptol.Utils.PP hiding ((</>))+import           Cryptol.Utils.Logger(stdoutLogger)+import           Cryptol.Utils.Ident(modNameToText, interactiveName)++import qualified Control.Exception as X+import           Control.Monad (guard, join)+import qualified Control.Monad.Trans.Class as MTL+#if !MIN_VERSION_haskeline(0,8,0)+import           Control.Monad.Trans.Control+#endif+import           Data.Char (isAlphaNum, isSpace)+import           Data.Function (on)+import           Data.List (isPrefixOf,nub,sortBy,sort)+import qualified Data.Set as Set+import qualified Data.Text as T (unpack)+import           System.Console.ANSI (setTitle, hSupportsANSI)+import           System.Console.Haskeline+import           System.Directory ( doesFileExist+                                  , getHomeDirectory+                                  , getCurrentDirectory)+import           System.FilePath ((</>))+import           System.IO (stdout)++import           Prelude ()+import           Prelude.Compat+import Cryptol.Project.Monad (LoadProjectMode)+++data ReplMode+  = InteractiveRepl -- ^ Interactive terminal session+  | Batch FilePath  -- ^ Execute from a batch file+  | InteractiveBatch FilePath+     -- ^ Execute from a batch file, but behave as though+     --   lines are entered in an interactive session.+ deriving (Show, Eq)++-- | One REPL invocation, either from a file or from the terminal.+crySession :: ReplMode -> Bool -> REPL CommandResult+crySession replMode stopOnError =+  do settings <- io (setHistoryFile (replSettings isBatch))+     let act = runInputTBehavior behavior settings (withInterrupt (loop True 1))+     if isBatch then asBatch act else act+  where+  (isBatch,behavior) = case replMode of+    InteractiveRepl       -> (False, defaultBehavior)+    Batch path            -> (True,  useFile path)+    InteractiveBatch path -> (False, useFile path)++  loop :: Bool -> Int -> InputT REPL CommandResult+  loop !success !lineNum =+    do ln <- getInputLines =<< MTL.lift getPrompt+       case ln of+         NoMoreLines -> return emptyCommandResult { crSuccess = success }+         Interrupted+           | isBatch && stopOnError -> return emptyCommandResult { crSuccess = False }+           | otherwise -> loop success lineNum+         NextLine ls+           | all (all isSpace) ls -> loop success (lineNum + length ls)+           | otherwise            -> doCommand success lineNum ls++  run lineNum cmd =+    case replMode of+      InteractiveRepl    -> runCommand lineNum Nothing cmd+      InteractiveBatch _ -> runCommand lineNum Nothing cmd+      Batch path         -> runCommand lineNum (Just path) cmd++  doCommand success lineNum txt =+    case parseCommand findCommandExact (unlines txt) of+      Nothing | isBatch && stopOnError -> return emptyCommandResult { crSuccess = False }+              | otherwise -> loop False (lineNum + length txt)  -- say somtething?+      Just cmd -> join $ MTL.lift $+        do status <- handleInterrupt (handleCtrlC emptyCommandResult { crSuccess = False }) (run lineNum cmd)+           case crSuccess status of+             False | isBatch && stopOnError -> return (return status)+             _ -> do goOn <- shouldContinue+                     return (if goOn then loop (crSuccess status && success) (lineNum + length txt) else return status)+++data NextLine = NextLine [String] | NoMoreLines | Interrupted++getInputLines :: String -> InputT REPL NextLine+getInputLines = handleInterrupt (MTL.lift (handleCtrlC Interrupted)) . loop []+  where+  loop ls prompt =+    do mb <- fmap (filter (/= '\r')) <$> getInputLine prompt+       let newPropmpt = map (\_ -> ' ') prompt+       case mb of+         Nothing -> return NoMoreLines+         Just l+           | not (null l) && last l == '\\' -> loop (init l : ls) newPropmpt+           | otherwise -> return $ NextLine $ reverse $ l : ls++loadCryRC :: Cryptolrc -> REPL CommandResult+loadCryRC cryrc =+  case cryrc of+    CryrcDisabled   -> return emptyCommandResult+    CryrcDefault    -> check [ getCurrentDirectory, getHomeDirectory ]+    CryrcFiles opts -> loadMany opts+  where+  check [] = return emptyCommandResult+  check (place : others) =+    do dir <- io place+       let file = dir </> ".cryptolrc"+       present <- io (doesFileExist file)+       if present+         then crySession (Batch file) True+         else check others++  loadMany []       = return emptyCommandResult+  loadMany (f : fs) = do status <- crySession (Batch f) True+                         if crSuccess status+                           then loadMany fs+                           else return status++-- | Haskeline-specific repl implementation.+repl ::+  Cryptolrc ->+  Maybe Project.Config ->+  LoadProjectMode {- ^ refresh project -} ->+  ReplMode -> Bool -> Bool -> REPL () -> IO CommandResult+repl cryrc projectConfig loadProjectMode replMode callStacks stopOnError begin =+  runREPL isBatch callStacks stdoutLogger replAction++ where+  -- this flag is used to suppress the logo and prompts+  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 do+          begin+          case projectConfig of+            Just config -> loadProjectREPL loadProjectMode config+            Nothing     -> crySession replMode stopOnError+       else return status++-- | Try to set the history file.+setHistoryFile :: Settings REPL -> IO (Settings REPL)+setHistoryFile ss =+  do dir <- getHomeDirectory+     return ss { historyFile = Just (dir </> ".cryptol_history") }+   `X.catch` \(X.SomeException {}) -> return ss++-- | Haskeline settings for the REPL.+replSettings :: Bool -> Settings REPL+replSettings isBatch = Settings+  { complete       = cryptolCommand+  , historyFile    = Nothing+  , autoAddHistory = not isBatch+  }++-- .cryptolrc ------------------------------------------------------------------++-- | Configuration of @.cryptolrc@ file behavior. The default option+-- searches the following locations in order, and evaluates the first+-- file that exists in batch mode on interpreter startup:+--+-- 1. $PWD/.cryptolrc+-- 2. $HOME/.cryptolrc+--+-- If files are specified, they will all be evaluated, but none of the+-- default files will be (unless they are explicitly specified).+--+-- The disabled option inhibits any reading of any .cryptolrc files.+data Cryptolrc =+    CryrcDefault+  | CryrcDisabled+  | CryrcFiles [FilePath]+  deriving (Show)++-- Utilities -------------------------------------------------------------------++#if !MIN_VERSION_haskeline(0,8,0)+instance MonadException REPL where+  controlIO f = join $ liftBaseWith $ \f' ->+    f $ RunIO $ \m -> restoreM <$> (f' m)+#endif++-- Titles ----------------------------------------------------------------------++mkTitle :: Maybe LoadedModule -> String+mkTitle lm = maybe "" (\ m -> pretty m ++ " - ") (lName =<< lm)+          ++ "cryptol"++setREPLTitle :: REPL ()+setREPLTitle = do+  lm <- getLoadedMod+  io (setTitle (mkTitle lm))++-- | In certain environments like Emacs, we shouldn't set the terminal+-- title. Note: this does not imply we can't use color output. We can+-- use ANSI color sequences in places like Emacs, but not terminal+-- codes.+--+-- This checks that @'stdout'@ is a proper terminal handle, and that the+-- terminal mode is not @dumb@, which is set by Emacs and others.+shouldSetREPLTitle :: REPL Bool+shouldSetREPLTitle = io (hSupportsANSI stdout)++-- | Whether we can display color titles. This checks that @'stdout'@+-- is a proper terminal handle, and that the terminal mode is not+-- @dumb@, which is set by Emacs and others.+canDisplayColor :: REPL Bool+canDisplayColor = io (hSupportsANSI stdout)++-- Completion ------------------------------------------------------------------++-- | Completion for cryptol commands.+cryptolCommand :: CompletionFunc REPL+cryptolCommand cursor@(l,r)+  | ":" `isPrefixOf` l'+  , Just (_,cmd,rest) <- splitCommand l' = case nub (findCommand cmd) of++      [c] | cursorRightAfterCmd rest ->+            return (l, cmdComp cmd c)+          | otherwise ->+            completeCmdArgument cmd rest c++      cmds+        -- If the command name is a prefix of multiple commands, then as a+        -- special case, check if (1) the name matches one command exactly, and+        -- (2) there is already some input for an argument. If so, proceed to+        -- tab-complete that argument. This ensures that something like+        -- `:check rev` will complete to `:check reverse`, even though the+        -- command name `:check` is a prefix for both the `:check` and+        -- `:check-docstrings` commands (#1781).+        | [c] <- nub (findCommandExact cmd)+        , not (cursorRightAfterCmd rest) ->+          completeCmdArgument cmd rest c++        | otherwise ->+          return (l, concat [ cmdComp l' c | c <- cmds ])+  -- Complete all : commands when the line is just a :+  | ":" == l' = return (l, concat [ cmdComp l' c | c <- nub (findCommand ":") ])+  | otherwise = completeExpr cursor+  where+  l' = sanitize (reverse l)++  -- Check if the cursor is positioned immediately after the input for the+  -- command, without any command arguments typed in after the command's name.+  cursorRightAfterCmd ::+    String+      {- The rest of the input after the command. -} ->+    Bool+  cursorRightAfterCmd rest = null rest && not (any isSpace l')++  -- Perform tab completion for a single argument to a command.+  completeCmdArgument ::+    String+      {- The name of the command as a String. -} ->+    String+      {- The rest of the input after the command. -} ->+    CommandDescr+      {- The description of the command. -} ->+    REPL (String, [Completion])+  completeCmdArgument cmd rest c =+    do (rest',cs) <- cmdArgument (cBody c) (reverse (sanitize rest),r)+       return (unwords [rest', reverse cmd],cs)++-- | Generate completions from a REPL command definition.+cmdComp :: String -> CommandDescr -> [Completion]+cmdComp prefix c = do+  cName <- cNames c+  guard (prefix `isPrefixOf` cName)+  return $ nameComp prefix cName++-- | Dispatch to a completion function based on the kind of completion the+-- command is expecting.+cmdArgument :: CommandBody -> CompletionFunc REPL+cmdArgument ct cursor@(l,_) = case ct of+  ExprArg     _ -> completeExpr cursor+  DeclsArg    _ -> (completeExpr +++ completeType) cursor+  ExprTypeArg _ -> (completeExpr +++ completeType) cursor+  ModNameArg _  -> completeModName cursor+  FilenameArg _ -> completeFilename cursor+  ShellArg _    -> completeFilename cursor+  OptionArg _   -> completeOption cursor+  HelpArg     _ -> completeHelp cursor+  NoArg       _ -> return (l,[])+  FileExprArg _ -> completeExpr cursor++-- | Additional keywords to suggest in the REPL+--   autocompletion list.+keywords :: [String]+keywords =+  [ "else"+  , "if"+  , "let"+  , "then"+  , "where"+  ]++-- | Complete a name from the expression environment.+completeExpr :: CompletionFunc REPL+completeExpr (l,_) = do+  ns <- (keywords++) <$> getExprNames+  let n    = reverse (takeIdent l)+      vars = sort $ filter (n `isPrefixOf`) ns+  return (l,map (nameComp n) vars)++-- | Complete a name from the type synonym environment.+completeType :: CompletionFunc REPL+completeType (l,_) = do+  ns <- getTypeNames+  let n    = reverse (takeIdent l)+      vars = filter (n `isPrefixOf`) ns+  return (l,map (nameComp n) vars)++-- | Complete a name for which we can show REPL help documentation.+completeHelp :: CompletionFunc REPL+completeHelp (l, _) = do+  ns1 <- getExprNames+  ns2 <- getTypeNames+  let ns3 = concatMap cNames (nub (findCommand ":"))+  let ns = Set.toAscList (Set.fromList (ns1 ++ ns2)) ++ ns3+  let n    = reverse l+  case break isSpace n of+    (":set", _ : n') ->+      do let n'' = dropWhile isSpace n'+         let vars = map optName (lookupTrie (dropWhile isSpace n') userOptions)+         return (l, map (nameComp n'') vars)+    _                ->+      do let vars = filter (n `isPrefixOf`) ns+         return (l, map (nameComp n) vars)+++-- | Complete a name from the list of loaded modules.+completeModName :: CompletionFunc REPL+completeModName (l, _) = do+  ms <- getModNames+  let ns   = map (T.unpack . modNameToText) (interactiveName : ms)+      n    = reverse (takeWhile (not . isSpace) l)+      vars = filter (n `isPrefixOf`) ns+  return (l, map (nameComp n) vars)++-- | Generate a completion from a prefix and a name.+nameComp :: String -> String -> Completion+nameComp prefix c = Completion+  { replacement = drop (length prefix) c+  , display     = c+  , isFinished  = True+  }++-- | Return longest identifier (possibly a qualified name) that is a+-- prefix of the given string+takeIdent :: String -> String+takeIdent (c : cs) | isIdentChar c = c : takeIdent cs+takeIdent (':' : ':' : cs) = ':' : ':' : takeIdent cs+takeIdent _ = []++isIdentChar :: Char -> Bool+isIdentChar c = isAlphaNum c || c `elem` "_\'"++-- | Join two completion functions together, merging and sorting their results.+(+++) :: CompletionFunc REPL -> CompletionFunc REPL -> CompletionFunc REPL+(as +++ bs) cursor = do+  (_,acs) <- as cursor+  (_,bcs) <- bs cursor+  return (fst cursor, sortBy (compare `on` replacement) (acs ++ bcs))+++-- | Complete an option from the options environment.+--+-- XXX this can do better, as it has access to the expected form of the value+completeOption :: CompletionFunc REPL+completeOption cursor@(l,_) = return (fst cursor, map comp opts)+  where+  n        = reverse l+  opts     = lookupTrie n userOptions+  comp opt = Completion+    { replacement = drop (length n) (optName opt)+    , display     = optName opt+    , isFinished  = False+    }

@@ -0,0 +1,75 @@+-- |+-- Module      :  REPL.Logo+-- Copyright   :  (c) 2013-2016 Galois, Inc.+-- License     :  BSD3+-- Maintainer  :  cryptol@galois.com+-- Stability   :  provisional+-- Portability :  portable++module REPL.Logo where++import Cryptol.REPL.Monad+import Cryptol.Utils.Panic (panic)+import Paths_cryptol (version)++import Cryptol.Version (commitShortHash,commitDirty)+import Data.Version (showVersion)+import System.Console.ANSI+import Prelude ()+import Prelude.Compat+++type Version = String++type Logo = [String]++-- | The list of 'String's returned by the @mk@ function should be non-empty.+logo :: Bool -> (String -> [String]) -> Logo+logo useColor mk =+     [ sgr [SetColor Foreground Dull  White] ++ l | l <- ws ]+  ++ [ sgr [SetColor Foreground Vivid Blue ] ++ l | l <- vs ]+  ++ [ sgr [SetColor Foreground Dull  Blue ] ++ l | l <- ds ]+  ++ [ sgr [Reset] ]+  where+  sgr | useColor  = setSGRCode+      | otherwise = const []+  hashText | commitShortHash == "UNKNOWN" = ""+           | otherwise = " (" ++ commitShortHash +++                                 (if commitDirty then ", modified)" else ")")+  versionText = "version " ++ showVersion version ++ hashText+  ver = sgr [SetColor Foreground Dull White]+        ++ replicate (lineLen - 20 - length versionText) ' '+        ++ versionText ++ "\n"+        ++ "https://cryptol.net  :? for help"+  ls        = mk ver+  slen      = length ls `div` 3+  (ws,rest) = splitAt slen ls+  (vs,ds)   = splitAt slen rest+  line      = case ls of+                line':_ -> line'+                [] -> panic "logo" ["empty lines"]+  lineLen   = length line++displayLogo :: Bool -> Bool -> REPL ()+displayLogo useColor useUnicode =+  unlessBatch (io (mapM_ putStrLn (logo useColor (if useUnicode then logo2 else logo1))))++logo1 :: String -> [String]+logo1 ver =+    [ "                        _        _"+    , "   ___ _ __ _   _ _ __ | |_ ___ | |"+    , "  / __| \'__| | | | \'_ \\| __/ _ \\| |"+    , " | (__| |  | |_| | |_) | || (_) | |"+    , "  \\___|_|   \\__, | .__/ \\__\\___/|_|"+    , "            |___/|_| " ++ ver+    ]++logo2 :: String -> [String]+logo2 ver =+    [ "┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  "+    , "┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  "+    , "┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸"+    , ver+    ]++

@@ -1,21 +1,22 @@ Cabal-version:       2.4 Name:                cryptol-Version:             3.2.0+Version:             3.3.0 Synopsis:            Cryptol: The Language of Cryptography Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>. License:             BSD-3-Clause License-file:        LICENSE Author:              Galois, Inc. Maintainer:          cryptol@galois.com-Homepage:            http://www.cryptol.net/+Homepage:            https://tools.galois.com/cryptol Bug-reports:         https://github.com/GaloisInc/cryptol/issues-Copyright:           2013-2022 Galois Inc.+Copyright:           2013-2025 Galois Inc. Category:            Language Build-type:          Simple extra-source-files:  bench/data/*.cry-                     CHANGES.md                      lib/*.cry lib/*.z3 +extra-doc-files:     CHANGES.md+ data-files:          **/*.cry **/*.z3 data-dir:            lib @@ -27,7 +28,7 @@   type:     git   location: https://github.com/GaloisInc/cryptol.git   -- add a tag on release branches-  tag: 3.2.0+  tag: 3.3.0   flag static@@ -54,7 +55,7 @@                        array             >= 0.4,                        containers        >= 0.5,                        criterion-measurement,-                       cryptohash-sha1   >= 0.11 && < 0.12,+                       cryptohash-sha256 >= 0.11 && < 0.12,                        deepseq           >= 1.3,                        directory         >= 1.2.2.0,                        exceptions,@@ -63,6 +64,7 @@                        gitrev            >= 1.0,                        ghc-prim,                        GraphSCC          >= 1.0.4,+                       heredoc           >= 0.2,                        language-c99,                        language-c99-simple,                        libBF             >= 0.6 && < 0.7,@@ -75,17 +77,18 @@                        pretty-show,                        process           >= 1.2,                        sbv               >= 9.1 && < 10.11,-                       simple-smt        >= 0.9.7,+                       simple-smt        >= 0.9.8,                        stm               >= 2.4,                        strict,                        text              >= 1.1,                        tf-random         >= 0.5,+                       toml-parser       >= 2.0 && <2.1,                        transformers-base >= 0.4,                        vector,                        mtl               >= 2.2.1,                        time              >= 1.6.0.1,                        panic             >= 0.3,-                       what4             >= 1.4 && < 1.7+                       what4             >= 1.6 && < 1.8    if impl(ghc >= 9.0)     build-depends:     ghc-bignum        >= 1.0 && < 1.4@@ -238,8 +241,15 @@                        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+                       Cryptol.Project.WildMatch++  Autogen-modules:     Paths_cryptol   Other-modules:       Cryptol.Parser.LexerUtils,                        Cryptol.Parser.ParserUtils,                        Cryptol.Prelude,@@ -254,20 +264,24 @@   if flag(relocatable)       cpp-options: -DRELOCATABLE -executable cryptol-  Default-language:-    Haskell2010-  Main-is:             Main.hs-  hs-source-dirs:      cryptol+-- The portions of the Cryptol REPL that are specific to the Cryptol executable.+-- We factor this out into a separate internal library because (1) it has some+-- dependencies (e.g., ansi-terminal and haskeline) that the Cryptol library+-- does not need to depend on, and (2) we want to be able to test this code in+-- the cryptol-api-tests test suite.+library cryptol-repl-internal+  exposed-modules:     REPL.Haskeline+                       REPL.Logo   Autogen-modules:     Paths_cryptol--  Other-modules:       OptParser,-                       REPL.Haskeline,-                       REPL.Logo,-                       Paths_cryptol-+  Other-modules:       Paths_cryptol+  hs-source-dirs:      cryptol-repl-internal+  default-language:    Haskell2010+  GHC-options:         -Wall -O2+  if os(linux) && flag(static)+      ld-options: -static -pthread+      ghc-options: -optl-fuse-ld=bfd   build-depends:       ansi-terminal-                     , base+                     , base >= 4.9 && < 5                      , base-compat                      , containers                      , cryptol@@ -278,6 +292,19 @@                      , monad-control                      , text                      , transformers++executable cryptol+  Default-language:+    Haskell2010+  Main-is:             Main.hs+  hs-source-dirs:      cryptol+  Other-modules:       OptParser+  build-depends:       base >= 4.9 && < 5+                     , base-compat+                     , cryptol+                     , cryptol-repl-internal+                     , directory+                     , filepath   GHC-options:         -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m" -O2   if impl(ghc >= 8.0.1)      ghc-options: -Wno-redundant-constraints@@ -291,7 +318,11 @@     Haskell2010   main-is: CryHtml.hs   hs-source-dirs: utils-  build-depends: base, text, cryptol, blaze-html+  build-depends:+     base >= 4.9 && < 5,+     text,+     cryptol,+     blaze-html   GHC-options: -Wall    if os(linux) && flag(static)@@ -304,7 +335,7 @@   Main-is:             CheckExercises.hs   hs-source-dirs:      cryptol   build-depends:       ansi-terminal-                     , base+                     , base >= 4.9 && < 5                      , containers                      , directory                      , extra@@ -315,6 +346,26 @@                      , temporary                      , text   GHC-options: -Wall++-- Test cases that require the use of the Cryptol API to test effectively. Most+-- other test cases should be added to the integration tests (which only require+-- the Cryptol executable and/or the REPL) under tests/.+test-suite cryptol-api-tests+  type:                exitcode-stdio-1.0+  main-is:             Main.hs+  hs-source-dirs:      api-tests+  default-language:    Haskell2010+  GHC-options:         -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m" -O2+  if os(linux) && flag(static)+      ld-options: -static -pthread+      ghc-options: -optl-fuse-ld=bfd+  build-depends:       base >= 4.9 && < 5+                     , cryptol+                     , cryptol-repl-internal+                     , haskeline+                     , tasty+                     , tasty-hunit+ benchmark cryptol-bench   type:                exitcode-stdio-1.0   main-is:             Main.hs@@ -326,7 +377,7 @@   if os(linux) && flag(static)       ld-options: -static -pthread       ghc-options: -optl-fuse-ld=bfd-  build-depends:       base+  build-depends:       base >= 4.9 && < 5                      , criterion                      , cryptol                      , deepseq

@@ -8,6 +8,7 @@  {-# LANGUAGE CPP #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} module Main where @@ -18,6 +19,7 @@                    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.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,8 @@   , optVersion         :: Bool   , optHelp            :: Bool   , optBatch           :: ReplMode+  , optProject         :: Maybe FilePath+  , optProjectRefresh  :: Project.LoadProjectMode   , optCallStacks      :: Bool   , optCommands        :: [String]   , optColorMode       :: ColorMode@@ -62,6 +67,8 @@   , optVersion         = False   , optHelp            = False   , optBatch           = InteractiveRepl+  , optProject         = Nothing+  , optProjectRefresh  = Project.ModifiedMode   , optCallStacks      = True   , optCommands        = []   , optColorMode       = AutoColor@@ -79,6 +86,16 @@   , 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 "" ["refresh-project"] (NoArg setProjectRefresh)+    "Ignore a pre-existing cache file when loading a project."++  , Option "" ["untested-project"] (NoArg setProjectUntested)+    "Load all project files that don't have a test result."+   , Option "e" ["stop-on-error"] (NoArg setStopOnError)     "stop script execution as soon as an error occurs." @@ -137,6 +154,15 @@ setInteractiveBatchScript :: String -> OptParser Options setInteractiveBatchScript path = modify $ \ opts -> opts { optBatch = InteractiveBatch path } +setProject :: String -> OptParser Options+setProject path = modify $ \opts -> opts { optProject = Just path }++setProjectRefresh :: OptParser Options+setProjectRefresh = modify $ \opts -> opts { optProjectRefresh = Project.RefreshMode }++setProjectUntested :: OptParser Options+setProjectUntested = modify $ \opts -> opts { optProjectRefresh = Project.UntestedMode }+ -- | Set the color mode of the terminal output. setColorMode :: String -> OptParser Options setColorMode "auto"   = modify $ \ opts -> opts { optColorMode = AutoColor }@@ -200,7 +226,7 @@             , "via the `:edit` command"             ]           )-        , ( "SBV_{ABC,BOOLECTOR,CVC4,CVC5,MATHSAT,YICES,Z3}_OPTIONS"+        , ( "SBV_{ABC,BITWUZLA,BOOLECTOR,CVC4,CVC5,MATHSAT,YICES,Z3}_OPTIONS"           , [ "A string of command-line arguments to be passed to the"             , "corresponding solver invoked for `:sat` and `:prove`"             , "when using a prover via SBV"@@ -225,11 +251,14 @@       | 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+                         (optProjectRefresh opts'')+                         (optBatch opts'')+                         (optCallStacks opts'')+                         (optStopOnError opts'')+                         (setupREPL opts'')           case mCleanup of             Nothing -> return ()             Just cmdFile -> removeFile cmdFile@@ -249,8 +278,28 @@       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   mCryptolPath <- io $ lookupEnv "CRYPTOLPATH"@@ -281,18 +330,20 @@     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."

@@ -1,356 +0,0 @@--- |--- Module      :  REPL.Haskeline--- Copyright   :  (c) 2013-2016 Galois, Inc.--- License     :  BSD3--- Maintainer  :  cryptol@galois.com--- Stability   :  provisional--- Portability :  portable--{-# LANGUAGE CPP #-}-{-# LANGUAGE MultiWayIf #-}-{-# LANGUAGE PatternGuards #-}-{-# LANGUAGE BangPatterns #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}--module REPL.Haskeline where--import           Cryptol.REPL.Command-import           Cryptol.REPL.Monad-import           Cryptol.REPL.Trie-import           Cryptol.Utils.PP hiding ((</>))-import           Cryptol.Utils.Logger(stdoutLogger)-import           Cryptol.Utils.Ident(modNameToText, interactiveName)--import qualified Control.Exception as X-import           Control.Monad (guard, join)-import qualified Control.Monad.Trans.Class as MTL-#if !MIN_VERSION_haskeline(0,8,0)-import           Control.Monad.Trans.Control-#endif-import           Data.Char (isAlphaNum, isSpace)-import           Data.Function (on)-import           Data.List (isPrefixOf,nub,sortBy,sort)-import qualified Data.Set as Set-import qualified Data.Text as T (unpack)-import           System.Console.ANSI (setTitle, hSupportsANSI)-import           System.Console.Haskeline-import           System.Directory ( doesFileExist-                                  , getHomeDirectory-                                  , getCurrentDirectory)-import           System.FilePath ((</>))-import           System.IO (stdout)--import           Prelude ()-import           Prelude.Compat---data ReplMode-  = InteractiveRepl -- ^ Interactive terminal session-  | Batch FilePath  -- ^ Execute from a batch file-  | InteractiveBatch FilePath-     -- ^ Execute from a batch file, but behave as though-     --   lines are entered in an interactive session.- deriving (Show, Eq)---- | One REPL invocation, either from a file or from the terminal.-crySession :: ReplMode -> Bool -> REPL CommandResult-crySession replMode stopOnError =-  do settings <- io (setHistoryFile (replSettings isBatch))-     let act = runInputTBehavior behavior settings (withInterrupt (loop True 1))-     if isBatch then asBatch act else act-  where-  (isBatch,behavior) = case replMode of-    InteractiveRepl       -> (False, defaultBehavior)-    Batch path            -> (True,  useFile path)-    InteractiveBatch path -> (False, useFile path)--  loop :: Bool -> Int -> InputT REPL CommandResult-  loop !success !lineNum =-    do ln <- getInputLines =<< MTL.lift getPrompt-       case ln of-         NoMoreLines -> return emptyCommandResult { crSuccess = success }-         Interrupted-           | isBatch && stopOnError -> return emptyCommandResult { crSuccess = False }-           | otherwise -> loop success lineNum-         NextLine ls-           | all (all isSpace) ls -> loop success (lineNum + length ls)-           | otherwise            -> doCommand success lineNum ls--  run lineNum cmd =-    case replMode of-      InteractiveRepl    -> runCommand lineNum Nothing cmd-      InteractiveBatch _ -> runCommand lineNum Nothing cmd-      Batch path         -> runCommand lineNum (Just path) cmd--  doCommand success lineNum txt =-    case parseCommand findCommandExact (unlines txt) of-      Nothing | isBatch && stopOnError -> return emptyCommandResult { crSuccess = False }-              | otherwise -> loop False (lineNum + length txt)  -- say somtething?-      Just cmd -> join $ MTL.lift $-        do status <- handleInterrupt (handleCtrlC emptyCommandResult { crSuccess = False }) (run lineNum cmd)-           case crSuccess status of-             False | isBatch && stopOnError -> return (return status)-             _ -> do goOn <- shouldContinue-                     return (if goOn then loop (crSuccess status && success) (lineNum + length txt) else return status)---data NextLine = NextLine [String] | NoMoreLines | Interrupted--getInputLines :: String -> InputT REPL NextLine-getInputLines = handleInterrupt (MTL.lift (handleCtrlC Interrupted)) . loop []-  where-  loop ls prompt =-    do mb <- fmap (filter (/= '\r')) <$> getInputLine prompt-       let newPropmpt = map (\_ -> ' ') prompt-       case mb of-         Nothing -> return NoMoreLines-         Just l-           | not (null l) && last l == '\\' -> loop (init l : ls) newPropmpt-           | otherwise -> return $ NextLine $ reverse $ l : ls--loadCryRC :: Cryptolrc -> REPL CommandResult-loadCryRC cryrc =-  case cryrc of-    CryrcDisabled   -> return emptyCommandResult-    CryrcDefault    -> check [ getCurrentDirectory, getHomeDirectory ]-    CryrcFiles opts -> loadMany opts-  where-  check [] = return emptyCommandResult-  check (place : others) =-    do dir <- io place-       let file = dir </> ".cryptolrc"-       present <- io (doesFileExist file)-       if present-         then crySession (Batch file) True-         else check others--  loadMany []       = return emptyCommandResult-  loadMany (f : fs) = do status <- crySession (Batch f) True-                         if crSuccess status-                           then loadMany fs-                           else return status---- | Haskeline-specific repl implementation.-repl :: Cryptolrc -> ReplMode -> Bool -> Bool -> REPL () -> IO CommandResult-repl cryrc 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--  replAction =-    do status <- loadCryRC cryrc-       if crSuccess status-         then begin >> crySession replMode stopOnError-         else return status---- | Try to set the history file.-setHistoryFile :: Settings REPL -> IO (Settings REPL)-setHistoryFile ss =-  do dir <- getHomeDirectory-     return ss { historyFile = Just (dir </> ".cryptol_history") }-   `X.catch` \(X.SomeException {}) -> return ss---- | Haskeline settings for the REPL.-replSettings :: Bool -> Settings REPL-replSettings isBatch = Settings-  { complete       = cryptolCommand-  , historyFile    = Nothing-  , autoAddHistory = not isBatch-  }---- .cryptolrc ---------------------------------------------------------------------- | Configuration of @.cryptolrc@ file behavior. The default option--- searches the following locations in order, and evaluates the first--- file that exists in batch mode on interpreter startup:------ 1. $PWD/.cryptolrc--- 2. $HOME/.cryptolrc------ If files are specified, they will all be evaluated, but none of the--- default files will be (unless they are explicitly specified).------ The disabled option inhibits any reading of any .cryptolrc files.-data Cryptolrc =-    CryrcDefault-  | CryrcDisabled-  | CryrcFiles [FilePath]-  deriving (Show)---- Utilities ---------------------------------------------------------------------#if !MIN_VERSION_haskeline(0,8,0)-instance MonadException REPL where-  controlIO f = join $ liftBaseWith $ \f' ->-    f $ RunIO $ \m -> restoreM <$> (f' m)-#endif---- Titles ------------------------------------------------------------------------mkTitle :: Maybe LoadedModule -> String-mkTitle lm = maybe "" (\ m -> pretty m ++ " - ") (lName =<< lm)-          ++ "cryptol"--setREPLTitle :: REPL ()-setREPLTitle = do-  lm <- getLoadedMod-  io (setTitle (mkTitle lm))---- | In certain environments like Emacs, we shouldn't set the terminal--- title. Note: this does not imply we can't use color output. We can--- use ANSI color sequences in places like Emacs, but not terminal--- codes.------ This checks that @'stdout'@ is a proper terminal handle, and that the--- terminal mode is not @dumb@, which is set by Emacs and others.-shouldSetREPLTitle :: REPL Bool-shouldSetREPLTitle = io (hSupportsANSI stdout)---- | Whether we can display color titles. This checks that @'stdout'@--- is a proper terminal handle, and that the terminal mode is not--- @dumb@, which is set by Emacs and others.-canDisplayColor :: REPL Bool-canDisplayColor = io (hSupportsANSI stdout)---- Completion ---------------------------------------------------------------------- | Completion for cryptol commands.-cryptolCommand :: CompletionFunc REPL-cryptolCommand cursor@(l,r)-  | ":" `isPrefixOf` l'-  , Just (_,cmd,rest) <- splitCommand l' = case nub (findCommand cmd) of--      [c] | null rest && not (any isSpace l') -> do-            return (l, cmdComp cmd c)-          | otherwise -> do-            (rest',cs) <- cmdArgument (cBody c) (reverse (sanitize rest),r)-            return (unwords [rest', reverse cmd],cs)--      cmds ->-        return (l, concat [ cmdComp l' c | c <- cmds ])-  -- Complete all : commands when the line is just a :-  | ":" == l' = return (l, concat [ cmdComp l' c | c <- nub (findCommand ":") ])-  | otherwise = completeExpr cursor-  where-  l' = sanitize (reverse l)---- | Generate completions from a REPL command definition.-cmdComp :: String -> CommandDescr -> [Completion]-cmdComp prefix c = do-  cName <- cNames c-  guard (prefix `isPrefixOf` cName)-  return $ nameComp prefix cName---- | Dispatch to a completion function based on the kind of completion the--- command is expecting.-cmdArgument :: CommandBody -> CompletionFunc REPL-cmdArgument ct cursor@(l,_) = case ct of-  ExprArg     _ -> completeExpr cursor-  DeclsArg    _ -> (completeExpr +++ completeType) cursor-  ExprTypeArg _ -> (completeExpr +++ completeType) cursor-  ModNameArg _  -> completeModName cursor-  FilenameArg _ -> completeFilename cursor-  ShellArg _    -> completeFilename cursor-  OptionArg _   -> completeOption cursor-  HelpArg     _ -> completeHelp cursor-  NoArg       _ -> return (l,[])-  FileExprArg _ -> completeExpr cursor---- | Additional keywords to suggest in the REPL---   autocompletion list.-keywords :: [String]-keywords =-  [ "else"-  , "if"-  , "let"-  , "then"-  , "where"-  ]---- | Complete a name from the expression environment.-completeExpr :: CompletionFunc REPL-completeExpr (l,_) = do-  ns <- (keywords++) <$> getExprNames-  let n    = reverse (takeIdent l)-      vars = sort $ filter (n `isPrefixOf`) ns-  return (l,map (nameComp n) vars)---- | Complete a name from the type synonym environment.-completeType :: CompletionFunc REPL-completeType (l,_) = do-  ns <- getTypeNames-  let n    = reverse (takeIdent l)-      vars = filter (n `isPrefixOf`) ns-  return (l,map (nameComp n) vars)---- | Complete a name for which we can show REPL help documentation.-completeHelp :: CompletionFunc REPL-completeHelp (l, _) = do-  ns1 <- getExprNames-  ns2 <- getTypeNames-  let ns3 = concatMap cNames (nub (findCommand ":"))-  let ns = Set.toAscList (Set.fromList (ns1 ++ ns2)) ++ ns3-  let n    = reverse l-  case break isSpace n of-    (":set", _ : n') ->-      do let n'' = dropWhile isSpace n'-         let vars = map optName (lookupTrie (dropWhile isSpace n') userOptions)-         return (l, map (nameComp n'') vars)-    _                ->-      do let vars = filter (n `isPrefixOf`) ns-         return (l, map (nameComp n) vars)----- | Complete a name from the list of loaded modules.-completeModName :: CompletionFunc REPL-completeModName (l, _) = do-  ms <- getModNames-  let ns   = map (T.unpack . modNameToText) (interactiveName : ms)-      n    = reverse (takeWhile (not . isSpace) l)-      vars = filter (n `isPrefixOf`) ns-  return (l, map (nameComp n) vars)---- | Generate a completion from a prefix and a name.-nameComp :: String -> String -> Completion-nameComp prefix c = Completion-  { replacement = drop (length prefix) c-  , display     = c-  , isFinished  = True-  }---- | Return longest identifier (possibly a qualified name) that is a--- prefix of the given string-takeIdent :: String -> String-takeIdent (c : cs) | isIdentChar c = c : takeIdent cs-takeIdent (':' : ':' : cs) = ':' : ':' : takeIdent cs-takeIdent _ = []--isIdentChar :: Char -> Bool-isIdentChar c = isAlphaNum c || c `elem` "_\'"---- | Join two completion functions together, merging and sorting their results.-(+++) :: CompletionFunc REPL -> CompletionFunc REPL -> CompletionFunc REPL-(as +++ bs) cursor = do-  (_,acs) <- as cursor-  (_,bcs) <- bs cursor-  return (fst cursor, sortBy (compare `on` replacement) (acs ++ bcs))----- | Complete an option from the options environment.------ XXX this can do better, as it has access to the expected form of the value-completeOption :: CompletionFunc REPL-completeOption cursor@(l,_) = return (fst cursor, map comp opts)-  where-  n        = reverse l-  opts     = lookupTrie n userOptions-  comp opt = Completion-    { replacement = drop (length n) (optName opt)-    , display     = optName opt-    , isFinished  = False-    }

@@ -1,75 +0,0 @@--- |--- Module      :  REPL.Logo--- Copyright   :  (c) 2013-2016 Galois, Inc.--- License     :  BSD3--- Maintainer  :  cryptol@galois.com--- Stability   :  provisional--- Portability :  portable--module REPL.Logo where--import Cryptol.REPL.Monad-import Cryptol.Utils.Panic (panic)-import Paths_cryptol (version)--import Cryptol.Version (commitShortHash,commitDirty)-import Data.Version (showVersion)-import System.Console.ANSI-import Prelude ()-import Prelude.Compat---type Version = String--type Logo = [String]---- | The list of 'String's returned by the @mk@ function should be non-empty.-logo :: Bool -> (String -> [String]) -> Logo-logo useColor mk =-     [ sgr [SetColor Foreground Dull  White] ++ l | l <- ws ]-  ++ [ sgr [SetColor Foreground Vivid Blue ] ++ l | l <- vs ]-  ++ [ sgr [SetColor Foreground Dull  Blue ] ++ l | l <- ds ]-  ++ [ sgr [Reset] ]-  where-  sgr | useColor  = setSGRCode-      | otherwise = const []-  hashText | commitShortHash == "UNKNOWN" = ""-           | otherwise = " (" ++ commitShortHash ++-                                 (if commitDirty then ", modified)" else ")")-  versionText = "version " ++ showVersion version ++ hashText-  ver = sgr [SetColor Foreground Dull White]-        ++ replicate (lineLen - 20 - length versionText) ' '-        ++ versionText ++ "\n"-        ++ "https://cryptol.net  :? for help"-  ls        = mk ver-  slen      = length ls `div` 3-  (ws,rest) = splitAt slen ls-  (vs,ds)   = splitAt slen rest-  line      = case ls of-                line':_ -> line'-                [] -> panic "logo" ["empty lines"]-  lineLen   = length line--displayLogo :: Bool -> Bool -> REPL ()-displayLogo useColor useUnicode =-  unlessBatch (io (mapM_ putStrLn (logo useColor (if useUnicode then logo2 else logo1))))--logo1 :: String -> [String]-logo1 ver =-    [ "                        _        _"-    , "   ___ _ __ _   _ _ __ | |_ ___ | |"-    , "  / __| \'__| | | | \'_ \\| __/ _ \\| |"-    , " | (__| |  | |_| | |_) | || (_) | |"-    , "  \\___|_|   \\__, | .__/ \\__\\___/|_|"-    , "            |___/|_| " ++ ver-    ]--logo2 :: String -> [String]-logo2 ver =-    [ "┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  "-    , "┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  "-    , "┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸"-    , ver-    ]--

@@ -75,6 +75,15 @@   (cryBool true) ) ++(declare-fun cryPrimeUnknown (Int) Bool)++(define-fun cryPrime ((x InfNat)) MaybeBool+  (ite (isErr x) cryErrProp+    (cryBool (and (isFin x) (cryPrimeUnknown (value x)))))+)++ ; ------------------------------------------------------------------------------ ; Basic Cryptol assume/assert @@ -327,14 +336,14 @@  ; (declare-fun L () InfNat) ; (declare-fun w () InfNat)-; +; ; (assert (cryVar L)) ; (assert (cryVar w))-; +; ; (assert (cryAssume (cryFin w))) ; (assert (cryAssume (cryGeq w (cryNat 1)))) ; (assert (cryAssume (cryGeq (cryMul (cryNat 2) w) (cryWidth L))))-; +; ; (assert (cryProve ;   (cryGeq ;     (cryMul@@ -343,7 +352,7 @@ ;         (cryMul (cryNat 16) w)) ;       (cryMul (cryNat 16) w)) ;     (cryAdd (cryNat 1) (cryAdd L (cryMul (cryNat 2) w))))))-; +; ; (check-sat)  

@@ -1,7 +1,9 @@ {-# Language FlexibleContexts #-} {-# Language TypeFamilies #-}+{-# Language ScopedTypeVariables #-} module Cryptol.Backend   ( Backend(..)+  , wordLen   , sDelay   , invalidIndex   , cryUserError@@ -36,6 +38,7 @@ import qualified Control.Exception as X import Control.Monad.IO.Class import Data.Kind (Type)+import Data.Proxy(Proxy(..))  import Cryptol.Backend.FloatHelpers (BF) import Cryptol.Backend.Monad@@ -295,7 +298,7 @@   bitAsLit :: sym -> SBit sym -> Maybe Bool    -- | The number of bits in a word value.-  wordLen :: sym -> SWord sym -> Integer+  wordLen' :: proxy sym -> SWord sym -> Integer    -- | Determine if this symbolic word is a literal.   --   If so, return the bit width and value.@@ -813,3 +816,7 @@   SFloat sym ->   SFloat sym ->   SEval sym (SFloat sym)++wordLen :: forall sym. Backend sym => sym -> SWord sym -> Integer+wordLen _ x = wordLen' (Proxy :: Proxy sym) x+{-# INLINE wordLen #-}

@@ -144,7 +144,9 @@   assertSideCondition _ True _ = return ()   assertSideCondition sym False err = raiseError sym err -  wordLen _ (BV w _) = w+  wordLen' _ (BV w _) = w+  {-# INLINE wordLen' #-}+     wordAsChar _ (BV _ x) = Just $! integerToChar x    wordBit _ (BV w x) idx = pure $! testBit x (fromInteger (w - 1 - idx))

@@ -201,7 +201,8 @@                 SBVResult pz z ->                   pure $ SBVResult (svAnd (svIte c px py) pz) z -  wordLen _ v = toInteger (intSizeOf v)+  wordLen' _ v = toInteger (intSizeOf v)+  {-# INLINE wordLen' #-}   wordAsChar _ v = integerToChar <$> svAsInteger v    iteBit _ b x y = pure $! svSymbolicMerge KBool True b x y

@@ -273,7 +273,8 @@     | SW.bvWidth bv == 8 = toEnum . fromInteger <$> SW.bvAsUnsignedInteger bv     | otherwise = Nothing -  wordLen _ bv = SW.bvWidth bv+  wordLen' _ bv = SW.bvWidth bv+  {-# INLINE wordLen' #-}    bitLit sym b = W4.backendPred (w4 sym) b   bitAsLit _ v = W4.asConstantPred v

@@ -25,6 +25,7 @@   ( -- * WordValue     WordValue   , wordVal+  , wordValWidth   , bitmapWordVal   , asWordList   , asWordVal@@ -59,6 +60,7 @@  import Control.Monad (unless) import Data.Bits+import Data.Proxy(Proxy(..)) import GHC.Generics (Generic)  import Cryptol.Backend@@ -96,6 +98,14 @@        !(SEval sym (SWord sym)) -- ^ Thunk for packing the word        !(SeqMap sym (SBit sym)) -- ^  deriving (Generic)++wordValWidth :: forall sym. Backend sym => WordValue sym -> Integer+wordValWidth val =+  case val of+    ThunkWordVal n _ -> n+    WordVal sv -> wordLen' (Proxy :: Proxy sym) sv+    BitmapVal n _ _ -> n+{-# INLINE wordValWidth #-}  wordVal :: SWord sym -> WordValue sym wordVal = WordVal

@@ -130,14 +130,14 @@     -- NB, even if the list cannot be packed, we must use `VWord`     -- when the element type is `Bit`.     | isTBit tyv -> {-# SCC "evalExpr->Elist/bit" #-}-        VWord len <$>+        VWord <$>           (tryFromBits sym vs >>= \case              Just w  -> pure (wordVal w)              Nothing -> do xs <- mapM (\x -> sDelay sym (fromVBit <$> x)) vs                            bitmapWordVal sym len $ finiteSeqMap sym xs)     | otherwise -> {-# SCC "evalExpr->EList" #-} do         xs <- mapM (sDelay sym) vs-        return $ VSeq len $ finiteSeqMap sym xs+        mkSeq sym (Nat len) tyv $ finiteSeqMap sym xs    where     tyv = evalValType (envTypes env) ty     vs  = map eval es@@ -594,7 +594,7 @@     case v of       VSeq _ vs       -> lookupSeqMap vs (toInteger n)       VStream vs      -> lookupSeqMap vs (toInteger n)-      VWord _ wv      -> VBit <$> indexWordValue sym wv (toInteger n)+      VWord wv        -> VBit <$> indexWordValue sym wv (toInteger n)       _               -> do vdoc <- ppValue sym defaultPPOpts val                             evalPanic "Cryptol.Eval.evalSel"                               [ "Unexpected value in list selection"@@ -608,7 +608,7 @@   sym ->   TValue ->   GenValue sym -> Selector -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)-evalSetSel sym _tyv e sel v =+evalSetSel sym tyv e sel v =   case sel of     TupleSel n _  -> setTuple n     RecordSel n _ -> setRecord n@@ -641,9 +641,10 @@    setList n =     case e of-      VSeq i mp  -> pure $ VSeq i  $ updateSeqMap mp n v+      VSeq i mp | TVSeq _ elty <- tyv -> +        mkSeq sym (Nat i) elty $ updateSeqMap mp n v       VStream mp -> pure $ VStream $ updateSeqMap mp n v-      VWord i m  -> VWord i <$> updateWordValue sym m n asBit+      VWord m    -> VWord <$> updateWordValue sym m n asBit       _ -> bad "Sequence update on a non-sequence."    asBit = do res <- v@@ -781,7 +782,7 @@         let lenv' = lenv { leVars = fmap stutter (leVars lenv) }         let vs i = do let (q, r) = i `divMod` nLen                       lookupSeqMap vss q >>= \case-                        VWord _ w   -> VBit <$> indexWordValue sym w r+                        VWord w     -> VBit <$> indexWordValue sym w r                         VSeq _ xs'  -> lookupSeqMap xs' r                         VStream xs' -> lookupSeqMap xs' r                         _           -> evalPanic "evalMatch" ["Not a list value"]@@ -795,7 +796,7 @@         let env = EvalEnv (leStatic lenv) (leTypes lenv)         xs <- evalExpr sym env expr         let vs i = case xs of-                     VWord _ w   -> VBit <$> indexWordValue sym w i+                     VWord w     -> VBit <$> indexWordValue sym w i                      VSeq _ xs'  -> lookupSeqMap xs' i                      VStream xs' -> lookupSeqMap xs' i                      _           -> evalPanic "evalMatch" ["Not a list value"]

@@ -134,7 +134,7 @@       (TVSeq _ b, VSeq n svs) ->         do ses <- traverse (go b) =<< lift (sequence (enumerateSeqMap n svs))            pure $ EList ses (tValTy b)-      (TVSeq n TVBit, VWord _ wval) ->+      (TVSeq n TVBit, VWord wval) ->         do BV _ v <- lift (asWordVal Concrete wval)            pure $ ETApp (ETApp (prim "number") (tNum v)) (tWord (tNum n)) @@ -206,7 +206,7 @@                       F2.pmult (fromInteger (u+1)) x y                     else                       F2.pmult (fromInteger (v+1)) y x-             in return . VWord (1+u+v) . wordVal . mkBv (1+u+v) $! z)+             in return . VWord . wordVal . mkBv (1+u+v) $! z)     , ("pmod",         PFinPoly \_u ->@@ -215,7 +215,7 @@         PWordFun \(BV _ m) ->         PPrim           do assertSideCondition sym (m /= 0) DivideByZero-             return . VWord v . wordVal . mkBv v $! F2.pmod (fromInteger w) x m)+             return . VWord . wordVal . mkBv v $! F2.pmod (fromInteger w) x m)    , ("pdiv",         PFinPoly \_u ->@@ -224,7 +224,7 @@         PWordFun \(BV _ m) ->         PPrim           do assertSideCondition sym (m /= 0) DivideByZero-             return . VWord w . wordVal . mkBv w $! F2.pdiv (fromInteger w) x m)+             return . VWord . wordVal . mkBv w $! F2.pdiv (fromInteger w) x m)   ]  @@ -297,9 +297,9 @@               foldM (\st blk -> seq st (SHA.processSHA256Block st <$> (toSHA256Block =<< blk)))                     SHA.initialSHA224State blks            let f :: Word32 -> Eval Value-               f = pure . VWord 32 . wordVal . BV 32 . toInteger+               f = pure . VWord . wordVal . BV 32 . toInteger                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6])-           seq zs (pure (VSeq 7 zs)))+           seq zs (wordSeq Concrete 7 32 zs))    , ("processSHA2_256", {-# SCC "SuiteB::processSHA2_256" #-}      PFinPoly \n ->@@ -310,9 +310,9 @@              foldM (\st blk -> seq st (SHA.processSHA256Block st <$> (toSHA256Block =<< blk)))                    SHA.initialSHA256State blks            let f :: Word32 -> Eval Value-               f = pure . VWord 32 . wordVal . BV 32 . toInteger+               f = pure . VWord . wordVal . BV 32 . toInteger                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6,w7])-           seq zs (pure (VSeq 8 zs)))+           seq zs (wordSeq Concrete 8 32 zs))    , ("processSHA2_384", {-# SCC "SuiteB::processSHA2_384" #-}      PFinPoly \n ->@@ -323,9 +323,9 @@              foldM (\st blk -> seq st (SHA.processSHA512Block st <$> (toSHA512Block =<< blk)))                    SHA.initialSHA384State blks            let f :: Word64 -> Eval Value-               f = pure . VWord 64 . wordVal . BV 64 . toInteger+               f = pure . VWord . wordVal . BV 64 . toInteger                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5])-           seq zs (pure (VSeq 6 zs)))+           seq zs (wordSeq Concrete 6 64 zs))    , ("processSHA2_512", {-# SCC "SuiteB::processSHA2_512" #-}      PFinPoly \n ->@@ -336,9 +336,9 @@              foldM (\st blk -> seq st (SHA.processSHA512Block st <$> (toSHA512Block =<< blk)))                    SHA.initialSHA512State blks            let f :: Word64 -> Eval Value-               f = pure . VWord 64 . wordVal . BV 64 . toInteger+               f = pure . VWord . wordVal . BV 64 . toInteger                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6,w7])-           seq zs (pure (VSeq 8 zs)))+           seq zs (wordSeq Concrete 8 64 zs))    , ("AESKeyExpand", {-# SCC "SuiteB::AESKeyExpand" #-}       PFinPoly \k ->@@ -348,11 +348,11 @@             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESInfKeyExpand" =<< lookupSeqMap ss i)             let fromWord :: Word32 -> Eval Value-                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger+                fromWord = pure . VWord . wordVal . BV 32 . toInteger             kws <- mapM toWord [0 .. k-1]             let ws = AES.keyExpansionWords k kws             let len = 4*(k+7)-            pure (VSeq len (finiteSeqMap Concrete (map fromWord ws))))+            wordSeq Concrete len 32 (finiteSeqMap Concrete (map fromWord ws)))    , ("AESInvMixColumns", {-# SCC "SuiteB::AESInvMixColumns" #-}       PFun \st ->@@ -361,10 +361,10 @@             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESInvMixColumns" =<< lookupSeqMap ss i)             let fromWord :: Word32 -> Eval Value-                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger+                fromWord = pure . VWord . wordVal . BV 32 . toInteger             ws <- mapM toWord [0,1,2,3]             let ws' = AES.invMixColumns ws-            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')+            wordSeq Concrete 4 32 (finiteSeqMap Concrete . map fromWord $ ws'))    , ("AESEncRound", {-# SCC "SuiteB::AESEncRound" #-}       PFun \st ->@@ -373,10 +373,10 @@             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESEncRound" =<< lookupSeqMap ss i)             let fromWord :: Word32 -> Eval Value-                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger+                fromWord = pure . VWord . wordVal . BV 32 . toInteger             ws <- mapM toWord [0,1,2,3]             let ws' = AES.aesRound ws-            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')+            wordSeq Concrete 4 32 (finiteSeqMap Concrete . map fromWord $ ws'))    , ("AESEncFinalRound", {-# SCC "SuiteB::AESEncFinalRound" #-}      PFun \st ->@@ -385,10 +385,10 @@             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESEncFinalRound" =<< lookupSeqMap ss i)             let fromWord :: Word32 -> Eval Value-                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger+                fromWord = pure . VWord . wordVal . BV 32 . toInteger             ws <- mapM toWord [0,1,2,3]             let ws' = AES.aesFinalRound ws-            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')+            wordSeq Concrete 4 32 (finiteSeqMap Concrete . map fromWord $ ws'))    , ("AESDecRound", {-# SCC "SuiteB::AESDecRound" #-}       PFun \st ->@@ -397,10 +397,10 @@             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESDecRound" =<< lookupSeqMap ss i)             let fromWord :: Word32 -> Eval Value-                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger+                fromWord = pure . VWord . wordVal . BV 32 . toInteger             ws <- mapM toWord [0,1,2,3]             let ws' = AES.aesInvRound ws-            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')+            wordSeq Concrete 4 32 . finiteSeqMap Concrete . map fromWord $ ws')    , ("AESDecFinalRound", {-# SCC "SuiteB::AESDecFinalRound" #-}      PFun \st ->@@ -409,10 +409,10 @@             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESDecFinalRound" =<< lookupSeqMap ss i)             let fromWord :: Word32 -> Eval Value-                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger+                fromWord = pure . VWord . wordVal . BV 32 . toInteger             ws <- mapM toWord [0,1,2,3]             let ws' = AES.aesInvFinalRound ws-            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')+            wordSeq Concrete 4 32 . finiteSeqMap Concrete . map fromWord $ ws')   ]  

@@ -51,6 +51,7 @@ import           Cryptol.Eval.Type import           Cryptol.Eval.Value import           Cryptol.ModuleSystem.Name+import           Cryptol.TypeCheck.Solver.InfNat import           Cryptol.Utils.Ident import           Cryptol.Utils.RecordMap @@ -269,6 +270,14 @@     let totalSize = fromInteger (product sizes)         getResult marshal ptr = do           getRetAsOutArgs gr [SomeFFIArg ptr]+          let tyv = case bt of+                FFIBasicVal bv -> case bv of+                  FFIWord len _ -> TVSeq len TVBit+                  FFIFloat e p _ -> TVFloat e p+                FFIBasicRef br -> case br of+                  FFIInteger Nothing -> TVInteger+                  FFIInteger (Just z) -> TVIntMod $ evalFinType z+                  FFIRational -> TVRational            let build (n:ns) !i = do                 -- We need to be careful to actually run this here and not just@@ -276,8 +285,11 @@                 -- will read from the array after it is deallocated.                 vs <- for [0 .. fromInteger n - 1] \j ->                   build ns (i * fromInteger n + j)-                pure (VSeq n (finiteSeqMap Concrete (map pure vs)))-              build [] !i = peekElemOff ptr i >>= runEval stk . marshal+                runEval stk $ +                  mkSeq Concrete (Nat n) tyv (finiteSeqMap Concrete (map pure vs))+              build [] !i = do+                e <- peekElemOff ptr i+                runEval stk (marshal e)            build sizes 0 

@@ -222,10 +222,12 @@                   lw <- fromVWord sym "ringLeft" l                   rw <- fromVWord sym "ringRight" r                   stk <- sGetCallStack sym-                  VWord w . wordVal <$> (sWithCallStack sym stk (opw w lw rw))-      | otherwise -> VSeq w <$> (join (zipSeqMap sym (loop a) (Nat w) <$>-                                      (fromSeq "ringBinary left" l) <*>-                                      (fromSeq "ringBinary right" r)))+                  VWord . wordVal <$> (sWithCallStack sym stk (opw w lw rw))+      | otherwise -> do+        vals <- (join (zipSeqMap sym (loop a) (Nat w) <$>+                  (fromSeq "ringBinary left" l) <*>+                  (fromSeq "ringBinary right" r)))+        mkSeq sym (Nat w) a vals      TVStream a ->       -- streams@@ -305,8 +307,10 @@       | isTBit a -> do               wx <- fromVWord sym "ringUnary" v               stk <- sGetCallStack sym-              VWord w . wordVal <$> sWithCallStack sym stk (opw w wx)-      | otherwise -> VSeq w <$> (mapSeqMap sym (loop a) (Nat w) =<< fromSeq "ringUnary" v)+              VWord . wordVal <$> sWithCallStack sym stk (opw w wx)+      | otherwise -> do+              vals <- mapSeqMap sym (loop a) (Nat w) =<< fromSeq "ringUnary" v+              mkSeq sym (Nat w) a vals      TVStream a ->       VStream <$> (mapSeqMap sym (loop a) Inf =<< fromSeq "ringUnary" v)@@ -372,10 +376,10 @@           -- words and finite sequences           | isTBit a ->              do stk <- sGetCallStack sym-                VWord w . wordVal <$> sWithCallStack sym stk (opw w)+                VWord . wordVal <$> sWithCallStack sym stk (opw w)           | otherwise ->              do v <- sDelay sym (loop a)-                pure $ VSeq w $ indexSeqMap \_i -> v+                mkSeq sym (Nat w) a $ indexSeqMap \_i -> v          TVStream a ->              do v <- sDelay sym (loop a)@@ -417,7 +421,7 @@           do wl <- fromVWord sym "integralBinary left" l              wr <- fromVWord sym "integralBinary right" r              stk <- sGetCallStack sym-             VWord w . wordVal <$> sWithCallStack sym stk (opw w wl wr)+             VWord . wordVal <$> sWithCallStack sym stk (opw w wl wr)      _ -> evalPanic "integralBinary" [show ty ++ " not int class `Integral`"] @@ -690,25 +694,25 @@ {-# INLINE lg2V #-} lg2V :: Backend sym => sym -> Prim sym lg2V sym =-  PFinPoly \w ->+  PFinPoly \_w ->   PWordFun \x ->-  PPrim (VWord w . wordVal <$> wordLg2 sym x)+  PPrim (VWord . wordVal <$> wordLg2 sym x)  {-# SPECIALIZE sdivV :: Concrete -> Prim Concrete #-} sdivV :: Backend sym => sym -> Prim sym sdivV sym =-  PFinPoly \w ->+  PFinPoly \_w ->   PWordFun \x ->   PWordFun \y ->-  PPrim (VWord w . wordVal <$> wordSignedDiv sym x y)+  PPrim (VWord . wordVal <$> wordSignedDiv sym x y)  {-# SPECIALIZE smodV :: Concrete -> Prim Concrete #-} smodV :: Backend sym => sym -> Prim sym smodV sym  =-  PFinPoly \w ->+  PFinPoly \_w ->   PWordFun \x ->   PWordFun \y ->-  PPrim (VWord w . wordVal <$> wordSignedMod sym x y)+  PPrim (VWord . wordVal <$> wordSignedMod sym x y)  {-# SPECIALIZE toSignedIntegerV :: Concrete -> Prim Concrete #-} toSignedIntegerV :: Backend sym => sym -> Prim sym@@ -920,7 +924,7 @@       | isTBit ety -> word sym w 0       | otherwise  ->            do z <- sDelay sym (zeroV sym ety)-              pure $ VSeq w (indexSeqMap \_i -> z)+              mkSeq sym (Nat w) ety (indexSeqMap \_i -> z)    TVStream ety ->      do z <- sDelay sym (zeroV sym ety)@@ -969,7 +973,7 @@ joinSeq sym (Nat parts) each TVBit val   = do w <- delayWordValue sym (parts*each)               (joinWords sym parts each . fmap (fromWordVal "joinV") =<< val)-       pure (VWord (parts*each) w)+       pure (VWord w)  -- infinite sequence of words joinSeq sym Inf each TVBit val@@ -980,19 +984,15 @@          VBit <$> indexWordValue sym ys r  -- finite or infinite sequence of non-words-joinSeq _sym parts each _a val-  = return $ vSeq $ indexSeqMap $ \i -> do+joinSeq sym parts each a val+  = mkSeq sym len a $ indexSeqMap $ \i -> do       let (q,r) = divMod i each       xs <- val       ys <- fromSeq "join seq" =<< lookupSeqMap xs q       lookupSeqMap ys r   where   len = parts `nMul` (Nat each)-  vSeq = case len of-           Inf    -> VStream-           Nat n  -> VSeq n - {-# INLINE joinV #-}  -- | Join a sequence of sequences into a single sequence.@@ -1024,15 +1024,15 @@       case back of         Nat back' | isTBit a ->           do w <- delayWordValue sym front' (takeWordVal sym front' back' =<< (fromWordVal "takeV" <$> val))-             pure (VWord front' w)+             pure (VWord w)          Inf | isTBit a ->           do w <- delayWordValue sym front' (bitmapWordVal sym front' . fmap fromVBit =<< (fromSeq "takeV" =<< val))-             pure (VWord front' w)+             pure (VWord w)          _ ->           do xs <- delaySeqMap sym (fromSeq "takeV" =<< val)-             pure (VSeq front' xs)+             mkSeq sym (Nat front') a xs  {-# INLINE dropV #-} dropV ::@@ -1047,7 +1047,7 @@   case back of     Nat back' | isTBit a ->       do w <- delayWordValue sym back' (dropWordVal sym front back' =<< (fromWordVal "dropV" <$> val))-         pure (VWord back' w)+         pure (VWord w)      _ ->       do xs <- delaySeqMap sym (dropSeqMap front <$> (fromSeq "dropV" =<< val))@@ -1065,32 +1065,49 @@   SEval sym (GenValue sym) ->   SEval sym (GenValue sym) splitV sym parts each a val =-    case (parts, each) of-       (Nat p, e) | isTBit a -> do-          val' <- sDelay sym (fromWordVal "splitV" <$> val)-          return $ VSeq p $ indexSeqMap $ \i ->-            VWord e <$> (extractWordVal sym e ((p-i-1)*e) =<< val')-       (Inf, e) | isTBit a -> do-          val' <- sDelay sym (fromSeq "splitV" =<< val)-          return $ VStream $ indexSeqMap $ \i ->-            VWord e <$> bitmapWordVal sym e (indexSeqMap $ \j ->-              let idx = i*e + toInteger j-               in idx `seq` do-                      xs <- val'-                      fromVBit <$> lookupSeqMap xs idx)-       (Nat p, e) -> do-          val' <- sDelay sym (fromSeq "splitV" =<< val)-          return $ VSeq p $ indexSeqMap $ \i ->-            return $ VSeq e $ indexSeqMap $ \j -> do-              xs <- val'-              lookupSeqMap xs (e * i + j)-       (Inf  , e) -> do-          val' <- sDelay sym (fromSeq "splitV" =<< val)-          return $ VStream $ indexSeqMap $ \i ->-            return $ VSeq e $ indexSeqMap $ \j -> do+  case parts of+    Nat p+     | isTBit a ->+       do val' <- sDelay sym (fromWordVal "splitV" <$> val)+          mkSeq sym (Nat p) tyv $ indexSeqMap $ \i ->+            VWord <$> (extractWordVal sym each ((p-i-1)*each) =<< val')+     | otherwise ->+       do val' <- sDelay sym (fromSeq "splitV" =<< val)+          mkSeq sym (Nat p) tyv $ indexSeqMap $ \i ->+            mkSeq sym (Nat each) a $ indexSeqMap $ \j -> do               xs <- val'-              lookupSeqMap xs (e * i + j)+              lookupSeqMap xs (each * i + j) +    Inf+      -- The return type is [inf][each], (where each is non-zero) and `val` is+      -- of type [inf * each], or [inf]. Therefore, `val` is a stream.+      | isTBit a, each /= 0 ->+        do val' <- sDelay sym (fromSeq "splitV" =<< val)+           return $ VStream $ indexSeqMap $ \i ->+             VWord <$> bitmapWordVal sym each (indexSeqMap $ \j ->+               let idx = i*each + toInteger j+                in idx `seq` do+                       xs <- val'+                       fromVBit <$> lookupSeqMap xs idx)+      -- The return type is [inf][0], and `val` is of type [inf * 0], or [0].+      -- Therefore, `val` is a word. We need to special-case this, because the+      -- case directly above this one will panic if `val` is not a stream due to+      -- the use of `fromSeq` (#1749).+      --+      -- Because `val` is an empty sequence, there is no need to split it apart.+      -- Instead, we can just return a stream with infinite copies of `val`.+      | isTBit a, each == 0 ->+        return $ VStream $ indexSeqMap $ \_i -> val+      -- If `a` is not `Bit`, then `val` must be a sequence or a stream (and not+      -- a word).+      | otherwise ->+        do val' <- sDelay sym (fromSeq "splitV" =<< val)+           return $ VStream $ indexSeqMap $ \i ->+             mkSeq sym (Nat each) a $ indexSeqMap $ \j -> do+               xs <- val'+               lookupSeqMap xs (each * i + j)+  where+    tyv = TVSeq each TVBit  {-# INLINE reverseV #-} @@ -1104,11 +1121,11 @@  reverseV sym n TVBit val =   do w <- delayWordValue sym n (reverseWordVal sym . fromWordVal "reverseV" =<< val)-     pure (VWord n w)+     pure (VWord w) -reverseV sym n _a val =+reverseV sym n a val =   do xs <- delaySeqMap sym (reverseSeqMap n <$> (fromSeq "reverseV" =<< val))-     pure (VSeq n xs)+     mkSeq sym (Nat n) a xs   {-# INLINE transposeV #-}@@ -1123,42 +1140,38 @@   SEval sym (GenValue sym) transposeV sym a b c xs   | isTBit c, Nat na <- a = -- Fin a => [a][b]Bit -> [b][a]Bit-      return $ bseq $ indexSeqMap $ \bi ->-        VWord na <$> bitmapWordVal sym na (indexSeqMap $ \ai ->+      bseq $ indexSeqMap $ \bi ->+        VWord <$> bitmapWordVal sym na (indexSeqMap $ \ai ->          do xs' <- fromSeq "transposeV" xs             ys <- lookupSeqMap xs' ai             case ys of               VStream ys' -> fromVBit <$> lookupSeqMap ys' bi-              VWord _ wv  -> indexWordValue sym wv bi+              VWord wv    -> indexWordValue sym wv bi               _ -> evalPanic "transpose" ["expected sequence of bits"])    | isTBit c, Inf <- a = -- [inf][b]Bit -> [b][inf]Bit-      return $ bseq $ indexSeqMap $ \bi ->+      bseq $ indexSeqMap $ \bi ->         return $ VStream $ indexSeqMap $ \ai ->          do xs' <- fromSeq "transposeV" xs             ys  <- lookupSeqMap xs' ai             case ys of               VStream ys' -> lookupSeqMap ys' bi-              VWord _ wv  -> VBit <$> indexWordValue sym wv bi+              VWord wv    -> VBit <$> indexWordValue sym wv bi               _ -> evalPanic "transpose" ["expected sequence of bits"]    | otherwise = -- [a][b]c -> [b][a]c-      return $ bseq $ indexSeqMap $ \bi ->-        return $ aseq $ indexSeqMap $ \ai -> do+      bseq $ indexSeqMap $ \bi ->+        aseq $ indexSeqMap $ \ai -> do           xs' <- fromSeq "transposeV 1" xs           ys  <- fromSeq "transposeV 2" =<< lookupSeqMap xs' ai           z   <- lookupSeqMap ys bi           return z   where-  bseq =-        case b of-          Nat nb -> VSeq nb-          Inf    -> VStream-  aseq =-        case a of-          Nat na -> VSeq na-          Inf    -> VStream+  bseq = case b of+    Nat n -> mkSeq sym b (TVSeq n c)+    Inf -> mkSeq sym b (TVStream c)+  aseq = mkSeq sym a c   {-# INLINE ccatV #-}@@ -1179,10 +1192,10 @@      mr <- isReady sym r      case (ml, mr) of        (Just l', Just r') ->-         VWord (front+back) <$>+         VWord <$>            joinWordVal sym (fromWordVal "ccatV left" l') (fromWordVal "ccatV right" r')        _ ->-         VWord (front+back) <$> delayWordValue sym (front+back)+         VWord <$> delayWordValue sym (front+back)                 (do l' <- fromWordVal "ccatV left"  <$> l                     r' <- fromWordVal "ccatV right" <$> r                     joinWordVal sym l' r')@@ -1250,17 +1263,19 @@     TVSeq w aty          -- words          | isTBit aty-              -> VWord w <$> delayWordValue sym w+              -> VWord <$> delayWordValue sym w                                (wordValLogicOp sym opb opw                                     (fromWordVal "logicBinary l" l)                                     (fromWordVal "logicBinary r" r))           -- finite sequences-         | otherwise -> VSeq w <$>-                           (join (zipSeqMap sym (loop aty) (Nat w) <$>-                                    (fromSeq "logicBinary left" l)-                                    <*> (fromSeq "logicBinary right" r)))+         | otherwise -> do+            vals <- join (zipSeqMap sym (loop aty) (Nat w) <$>+                              (fromSeq "logicBinary left" l)+                              <*> (fromSeq "logicBinary right" r))+            mkSeq sym (Nat w) aty vals +     TVStream aty ->         VStream <$> (join (zipSeqMap sym (loop aty) Inf <$>                           (fromSeq "logicBinary left" l) <*>@@ -1314,11 +1329,11 @@     TVSeq w ety          -- words          | isTBit ety-              -> VWord w <$> delayWordValue sym w (wordValUnaryOp sym opb opw (fromWordVal "logicUnary" val))+              -> VWord <$> delayWordValue sym w (wordValUnaryOp sym opb opw (fromWordVal "logicUnary" val))           -- finite sequences          | otherwise-              -> VSeq w <$> (mapSeqMap sym (loop ety) (Nat w) =<< fromSeq "logicUnary" val)+              -> mkSeq sym (Nat w) ety =<< (mapSeqMap sym (loop ety) (Nat w) =<< fromSeq "logicUnary" val)           -- streams     TVStream ety ->@@ -1388,7 +1403,7 @@   PFun     \idx ->   PPrim    do vs <- xs >>= \case-               VWord _ w  -> return $ indexSeqMap (\i -> VBit <$> indexWordValue sym w i)+               VWord w    -> return $ indexSeqMap (\i -> VBit <$> indexWordValue sym w i)                VSeq _ vs  -> return vs                VStream vs -> return vs                _ -> evalPanic "Expected sequence value" ["indexPrim"]@@ -1421,9 +1436,9 @@    do idx' <- asIndex sym "update" ix <$> idx       assertIndexInBounds sym len idx'       case (len, eltTy) of-        (Nat n, TVBit) -> VWord n <$> delayWordValue sym n+        (Nat n, TVBit) -> VWord <$> delayWordValue sym n                              (do w <- fromWordVal "updatePrim" <$> xs; updateWord len eltTy w idx' val)-        (Nat n, _    ) -> VSeq n <$> delaySeqMap sym+        (Nat n, _    ) -> mkSeq sym (Nat n) eltTy =<< delaySeqMap sym                              (do vs <- fromSeq "updatePrim" =<< xs; updateSeq len eltTy vs idx' val)         (Inf  , _    ) -> VStream <$> delaySeqMap sym                              (do vs <- fromSeq "updatePrim" =<< xs; updateSeq len eltTy vs idx' val)@@ -1644,8 +1659,8 @@    SEval sym (GenValue sym) intShifter sym nm wop reindex m a xs idx =   case xs of-    VWord w x  -> VWord w <$> shiftWordByInteger sym wop (reindex m) x idx-    VSeq w vs  -> VSeq w  <$> shiftSeqByInteger sym (mergeValue sym) (reindex m) (zeroV sym a) m vs idx+    VWord x    -> VWord   <$> shiftWordByInteger sym wop (reindex m) x idx+    VSeq w vs  -> mkSeq sym (Nat w) a =<< shiftSeqByInteger sym (mergeValue sym) (reindex m) (zeroV sym a) m vs idx     VStream vs -> VStream <$> shiftSeqByInteger sym (mergeValue sym) (reindex m) (zeroV sym a) m vs idx     _ -> evalPanic "expected sequence value in shift operation" [nm] @@ -1663,8 +1678,8 @@    SEval sym (GenValue sym) wordShifter sym nm wop reindex m a xs idx =   case xs of-    VWord w x  -> VWord w <$> shiftWordByWord sym wop (reindex m) x idx-    VSeq w vs  -> VSeq w  <$> shiftSeqByWord sym (mergeValue sym) (reindex m) (zeroV sym a) (Nat w) vs idx+    VWord x    -> VWord   <$> shiftWordByWord sym wop (reindex m) x idx+    VSeq w vs  -> mkSeq sym (Nat w) a =<< shiftSeqByWord sym (mergeValue sym) (reindex m) (zeroV sym a) (Nat w) vs idx     VStream vs -> VStream <$> shiftSeqByWord sym (mergeValue sym) (reindex m) (zeroV sym a) Inf     vs idx     _ -> evalPanic "expected sequence value in shift operation" [nm] @@ -1697,7 +1712,7 @@     case asIndex sym ">>$" ix y of        Left i ->          do pneg <- intLessThan sym i =<< integerLit sym 0-            VWord n <$> mergeWord' sym+            VWord <$> mergeWord' sym               pneg               (do i' <- shiftShrink sym (Nat n) ix =<< intNegate sym i                   amt <- wordFromInt sym n i'@@ -1708,7 +1723,7 @@         Right wv ->          do amt <- asWordVal sym wv-            VWord n . wordVal <$> wordSignedShiftRight sym x amt+            VWord . wordVal <$> wordSignedShiftRight sym x amt  -- Miscellaneous --------------------------------------------------------------- @@ -1734,7 +1749,7 @@ --   and return the associated character, if it is concrete. --   Otherwise, return a '?' character valueToChar :: Backend sym => sym -> GenValue sym -> SEval sym Char-valueToChar sym (VWord 8 wval) =+valueToChar sym (VWord wval) | wordValWidth wval == 8 =   do w <- asWordVal sym wval      pure $! fromMaybe '?' (wordAsChar sym w) valueToChar _ _ = evalPanic "valueToChar" ["Not an 8-bit bitvector"]@@ -1756,8 +1771,8 @@   PStrict  \v ->   PPrim     case v of-      VSeq n m    -> go0 f z (enumerateSeqMap n m)-      VWord _n wv -> go0 f z . map (pure . VBit) =<< (enumerateWordValue sym wv)+      VSeq n m  -> go0 f z (enumerateSeqMap n m)+      VWord  wv -> go0 f z . map (pure . VBit) =<< (enumerateWordValue sym wv)       _ -> panic "Cryptol.Eval.Generic.foldlV" ["Expected finite sequence"]   where   go0 _f a [] = a@@ -1781,7 +1796,7 @@   PPrim     case v of       VSeq n m    -> go0 f z (enumerateSeqMap n m)-      VWord _n wv -> go0 f z . map (pure . VBit) =<< (enumerateWordValue sym wv)+      VWord wv    -> go0 f z . map (pure . VBit) =<< (enumerateWordValue sym wv)       _ -> panic "Cryptol.Eval.Generic.foldlV" ["Expected finite sequence"]   where   go0 _f a [] = a@@ -1811,7 +1826,7 @@   PPrim     do sm <- case v of             VSeq _ m   -> scan n f z m-            VWord _ wv -> scan n f z (VBit <$> asBitsMap sym wv)+            VWord wv   -> scan n f z (VBit <$> asBitsMap sym wv)             VStream m  -> scan n f z m             _ -> panic "Cryptol.Eval.Generic.scanlV" ["Expected sequence"]        mkSeq sym (nAdd (Nat 1) n) a sm@@ -1869,7 +1884,7 @@        xs' <- xs        m <-          case xs' of-           VWord _n w ->+           VWord w ->              let m = asBitsMap sym w in              sparkParMap sym (\x -> f' (VBit <$> x)) n m            VSeq _n m ->@@ -1938,8 +1953,8 @@     , "fpPosInf"    ~> fpConst (fpPosInf sym)     , "fpFromBits"  ~> PFinPoly \e -> PFinPoly \p -> PWordFun \w ->                        PPrim (VFloat <$> fpFromBits sym e p w)-    , "fpToBits"    ~> PFinPoly \e -> PFinPoly \p -> PFloatFun \x -> PPrim-                            (VWord (e+p) . wordVal <$> fpToBits sym x)+    , "fpToBits"    ~> PFinPoly \_e -> PFinPoly \_p -> PFloatFun \x -> PPrim+                            (VWord . wordVal <$> fpToBits sym x)     , "=.="         ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x -> PFloatFun \y ->                        PPrim (VBit <$> fpLogicalEq sym x y)