cryptol 2.10.0 → 2.11.0

raw patch · 81 files changed

+3775/−2648 lines, 81 filesdep +extradep +optparse-applicativedep +temporarydep ~basedep ~containersdep ~directorynew-component:exe:check-exercisesPVP ok

version bump matches the API change (PVP)

Dependencies added: extra, optparse-applicative, temporary

Dependency ranges changed: base, containers, directory, filepath, libBF, mtl, process, sbv, text, what4

API changes (from Hackage documentation)

Files

• CHANGES.md +50/−0
• cryptol.cabal +31/−8
• cryptol/CheckExercises.hs +371/−0
• cryptol/Main.hs +31/−8
• cryptol/REPL/Haskeline.hs +52/−31
• cryptol/REPL/Logo.hs +2/−0
• lib/Cryptol.cry +18/−2
• lib/Float.cry +48/−4
• src/Cryptol/Backend.hs +65/−50
• src/Cryptol/Backend/Concrete.hs +51/−20
• src/Cryptol/Backend/FloatHelpers.hs +23/−93
• src/Cryptol/Backend/Monad.hs +156/−95
• src/Cryptol/Backend/SBV.hs +58/−36
• src/Cryptol/Backend/What4.hs +41/−26
• src/Cryptol/Backend/What4/SFloat.hs +0/−362
• src/Cryptol/Eval.hs +139/−82
• src/Cryptol/Eval/Concrete.hs +159/−361
• src/Cryptol/Eval/Env.hs +16/−16
• src/Cryptol/Eval/Generic.hs +627/−278
• src/Cryptol/Eval/Prims.hs +39/−0
• src/Cryptol/Eval/Reference.lhs +56/−14
• src/Cryptol/Eval/SBV.hs +14/−150
• src/Cryptol/Eval/Type.hs +45/−11
• src/Cryptol/Eval/Value.hs +179/−73
• src/Cryptol/Eval/What4.hs +73/−251
• src/Cryptol/IR/FreeVars.hs +4/−6
• src/Cryptol/ModuleSystem.hs +6/−8
• src/Cryptol/ModuleSystem/Base.hs +24/−11
• src/Cryptol/ModuleSystem/Env.hs +6/−0
• src/Cryptol/ModuleSystem/InstantiateModule.hs +3/−2
• src/Cryptol/ModuleSystem/Monad.hs +52/−16
• src/Cryptol/ModuleSystem/Name.hs +0/−4
• src/Cryptol/ModuleSystem/Renamer.hs +14/−11
• src/Cryptol/Parser.y +20/−12
• src/Cryptol/Parser/AST.hs +31/−8
• src/Cryptol/Parser/Lexer.x +5/−1
• src/Cryptol/Parser/LexerUtils.hs +4/−0
• src/Cryptol/Parser/Names.hs +5/−2
• src/Cryptol/Parser/NoPat.hs +24/−13
• src/Cryptol/Parser/ParserUtils.hs +115/−53
• src/Cryptol/Parser/Position.hs +5/−1
• src/Cryptol/REPL/Command.hs +310/−204
• src/Cryptol/REPL/Monad.hs +90/−40
• src/Cryptol/REPL/Trie.hs +6/−5
• src/Cryptol/Symbolic.hs +70/−44
• src/Cryptol/Symbolic/SBV.hs +48/−16
• src/Cryptol/Symbolic/What4.hs +25/−17
• src/Cryptol/Testing/Random.hs +67/−42
• src/Cryptol/Transform/AddModParams.hs +8/−11
• src/Cryptol/Transform/MonoValues.hs +1/−0
• src/Cryptol/Transform/Specialize.hs +4/−3
• src/Cryptol/TypeCheck.hs +5/−1
• src/Cryptol/TypeCheck/AST.hs +8/−2
• src/Cryptol/TypeCheck/CheckModuleInstance.hs +1/−1
• src/Cryptol/TypeCheck/Default.hs +6/−3
• src/Cryptol/TypeCheck/Depends.hs +8/−11
• src/Cryptol/TypeCheck/Error.hs +32/−5
• src/Cryptol/TypeCheck/Infer.hs +39/−12
• src/Cryptol/TypeCheck/InferTypes.hs +32/−2
• src/Cryptol/TypeCheck/Instantiate.hs +3/−3
• src/Cryptol/TypeCheck/Kind.hs +13/−14
• src/Cryptol/TypeCheck/Monad.hs +56/−15
• src/Cryptol/TypeCheck/Parseable.hs +1/−0
• src/Cryptol/TypeCheck/Sanity.hs +28/−7
• src/Cryptol/TypeCheck/SimpType.hs +1/−0
• src/Cryptol/TypeCheck/SimpleSolver.hs +2/−0
• src/Cryptol/TypeCheck/Solver/Class.hs +76/−4
• src/Cryptol/TypeCheck/Solver/Improve.hs +2/−1
• src/Cryptol/TypeCheck/Solver/SMT.hs +22/−19
• src/Cryptol/TypeCheck/Solver/Selector.hs +11/−14
• src/Cryptol/TypeCheck/Solver/Utils.hs +3/−0
• src/Cryptol/TypeCheck/Subst.hs +4/−1
• src/Cryptol/TypeCheck/TCon.hs +4/−3
• src/Cryptol/TypeCheck/Type.hs +56/−16
• src/Cryptol/TypeCheck/TypeMap.hs +15/−3
• src/Cryptol/TypeCheck/TypeOf.hs +8/−4
• src/Cryptol/TypeCheck/TypePat.hs +6/−1
• src/Cryptol/TypeCheck/Unify.hs +3/−0
• src/Cryptol/Utils/PP.hs +32/−0
• src/GitRev.hs +0/−1
• utils/CryHtml.hs +7/−4

@@ -1,3 +1,53 @@+# 2.11.0++## Language changes++* The `newtype` construct, which has existed in the interpreter in an+  incomplete and undocumented form for quite a while, is now fullly+  supported. The construct is documented in section 1.22 of [Programming+  Cryptol](https://cryptol.net/files/ProgrammingCryptol.pdf). Note,+  however, that the `cryptol-remote-api` RPC server currently does not+  include full support for referring to `newtype` names, though it can+  work with implementations that use `newtype` internally.++## New features++* By default, the interpreter will now track source locations of+  expressions being evaluated, and retain call stack information.+  This information is incorporated into error messages arising from+  runtime errors. This additional bookkeeping incurs significant+  runtime overhead, but may be disabled using the `--no-call-stacks`+  command-line option.++* The `:exhaust` command now works for floating-point types and the+  `:check` command now uses more representative sampling of+  floating-point input values to test.++* The `cryptol-remote-api` RPC server now has methods corresponding to+  the `:prove` and `:sat` commands in the REPL.++* The `cryptol-eval-server` executable is a new, stateless server+  providing a subset of the functionality of `cryptol-remote-api`+  dedicated entirely to invoking Cryptol functions on concrete inputs.++## Internal changes++* A single running instance of the SMT solver used for type checking+  (Z3) is now used to check a larger number of type correctness queries.+  This means that fewer solver instances are invoked, and type checking+  should generally be faster.++* The Cryptol interpreter now builds against `libBF` version 0.6, which+  fixes a few bugs in the evaluation of floating-point operations.++## Bug fixes++* Closed issues #118, #398, #426, #470, #491, #567, #594, #639, #656,+  #698, #743, #810, #858, #870, #905, #915, #917, #962, #973, #975,+  #980, #984, #986, #990, #996, #997, #1002, #1006, #1009, #1012, #1024,+  #1030, #1035, #1036, #1039, #1040, #1044, #1045, #1049, #1050, #1051,+  #1052, #1063, #1092, #1093, #1094, and #1100.+ # 2.10.0  ## Language changes

@@ -1,6 +1,6 @@ Cabal-version:       2.4 Name:                cryptol-Version:             2.10.0+Version:             2.11.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@@ -25,7 +25,7 @@ source-repository this   type:     git   location: https://github.com/GaloisInc/cryptol.git-  tag:      2.10.0+  tag:      2.11.0   flag static@@ -56,7 +56,7 @@                        GraphSCC          >= 1.0.4,                        heredoc           >= 0.2,                        integer-gmp       >= 1.0 && < 1.1,-                       libBF             >= 0.5.1,+                       libBF             >= 0.6 && < 0.7,                        MemoTrie          >= 0.6 && < 0.7,                        monad-control     >= 1.0,                        monadLib          >= 3.7.2,@@ -64,7 +64,7 @@                        pretty            >= 1.1,                        process           >= 1.2,                        random            >= 1.0.1,-                       sbv               >= 8.6 && < 8.8,+                       sbv               >= 8.6 && < 8.13,                        simple-smt        >= 0.7.1,                        stm               >= 2.4,                        strict,@@ -74,7 +74,7 @@                        mtl               >= 2.2.1,                        time              >= 1.6.0.1,                        panic             >= 0.3,-                       what4             >= 1.0 && < 1.1+                       what4             >= 1.1 && < 1.2    Build-tool-depends:  alex:alex, happy:happy   hs-source-dirs:      src@@ -164,12 +164,12 @@                        Cryptol.Backend.Monad,                        Cryptol.Backend.SBV,                        Cryptol.Backend.What4,-                       Cryptol.Backend.What4.SFloat,                         Cryptol.Eval,                        Cryptol.Eval.Concrete,                        Cryptol.Eval.Env,                        Cryptol.Eval.Generic,+                       Cryptol.Eval.Prims,                        Cryptol.Eval.Reference,                        Cryptol.Eval.SBV,                        Cryptol.Eval.Type,@@ -232,7 +232,8 @@      ghc-options: -Wno-redundant-constraints    if os(linux) && flag(static)-      ld-options:      -static -pthread+      ld-options: -static -pthread+      ghc-options: -optl-fuse-ld=bfd  executable cryptol-html   Default-language:@@ -242,6 +243,27 @@   build-depends: base, text, cryptol, blaze-html   GHC-options: -Wall +  if os(linux) && flag(static)+      ld-options: -static -pthread+      ghc-options: -optl-fuse-ld=bfd++executable check-exercises+  Default-language:+    Haskell2010+  Main-is:             CheckExercises.hs+  hs-source-dirs:      cryptol+  build-depends:       ansi-terminal+                     , base+                     , containers+                     , directory+                     , extra+                     , filepath+                     , mtl+                     , optparse-applicative+                     , process+                     , temporary+                     , text+  GHC-options: -Wall benchmark cryptol-bench   type:                exitcode-stdio-1.0   main-is:             Main.hs@@ -251,7 +273,8 @@   if impl(ghc >= 8.0.1)      ghc-options: -Wno-redundant-constraints   if os(linux) && flag(static)-      ld-options:      -static -pthread+      ld-options: -static -pthread+      ghc-options: -optl-fuse-ld=bfd   build-depends:       base                      , criterion                      , cryptol

@@ -0,0 +1,371 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ViewPatterns #-}++module Main(main) where++import Control.Monad.State+import Options.Applicative+import Data.Char (isSpace, isAlpha)+import Data.Foldable (traverse_)+import Data.List (isInfixOf, isPrefixOf, stripPrefix)+import Data.Maybe (fromMaybe)+import qualified Data.Sequence as Seq+import Numeric.Natural+import qualified System.Process as P+import System.Directory+import System.Exit+import System.IO.Temp+import Data.Foldable (toList)++data Opts = Opts { latexFile :: FilePath+                   -- ^ The latex file we are going to check+                 , cryptolExe :: Maybe FilePath+                   -- ^ Path to cryptol executable (default: cabal v2-exec cryptol)+                 , tempDir :: Maybe FilePath+                   -- ^ Path to store temporary files and log files+                 }+  deriving Show++optsParser :: Parser Opts+optsParser = Opts+  <$> strArgument (  help "path to latex file"+                  <> metavar "PATH"+                  )+  <*> ( optional $ strOption+        (  long "exe"+        <> short 'e'+        <> metavar "PATH"+        <> help "Path to cryptol executable (defaults to 'cabal v2-exec cryptol')"+        ) )+  <*> ( optional $ strOption+        (  long "log-dir"+        <> short 'l'+        <> metavar "PATH"+        <> help "Directory for log files in case of failure (defaults to .)"+        ) )++-- | Trim whitespace off both ends of a string+trim :: String -> String+trim = f . f+   where f = reverse . dropWhile isSpace++----------------------------------------------------------------------+-- LaTeX processing state monad+--+-- We process the text-by-line. The behavior of the state monad on a line is+-- governed by the mode it is currently in. The current mode dictates how to+-- interpret each line, and which mode to transition to next.+--+-- There are four modes: AwaitingReplMode, ReplinMode, ReploutMode, and+-- ReplPromptMode. Below we describe the behavior of each mode.+--+-- AwaitingReplMode: When in this mode, we are anticipating "replin" or+-- "replout" lines; that is, lines that will be issued as input to the repl or+-- expected as output from the repl.. When we see a \begin{replinVerb}, we+-- transition to ReplinMode. When we see a \begin{reploutVerb}, we transition to+-- ReploutMode. When we see a \begin{replPromptVerb}, we transition to+-- ReplPromptMode. When we see an inline \replin{..} command, we add the content+-- to the list of replin lines without changing modes. When we see an inline+-- \replout{..} command, we add the content to the list of replout lines without+-- changing modes.+--+-- ReplinMode: When in this mode, we are inside of a "\begin{replinVerb}"+-- section. When we see a \end{replinVerb} line, we transition to+-- AwaitingReplMode. Otherwise, we simply add the entire line to the list of+-- replin lines.+--+-- ReploutMode: Like ReplinMode, except we add each line to the expected output.+--+-- ReplPromptMode: A combination of ReplinMode and ReploutMode. Each line is+-- either added to input or expected output. If the line starts with a prompt+-- like "Cryptol>" or "Float>", it is added to expected input. Otherwise it is+-- added to expected output.++data PMode = AwaitingReplMode+           | ReplinMode+           | ReploutMode+           | ReplPromptMode+  deriving (Eq, Show)++data Line = Line { lineNum :: Natural+                 , lineText :: String+                 }+  deriving (Eq, Show)++-- | REPL input and expected output, with line number annotations.+data ReplData = ReplData { rdReplin  :: Seq.Seq Line+                         , rdReplout :: Seq.Seq Line+                         }+  deriving (Eq, Show)++-- | Latex processing state+data PState = PState { pMode              :: PMode+                       -- ^ current mode+                     , pCompletedReplData :: Seq.Seq ReplData+                       -- ^ list of all completed REPL input/output pairs to be+                       -- validated (thus far)+                     , pReplin            :: Seq.Seq Line+                       -- ^ list of replin lines (so far) for unfinished ReplData+                     , pReplout           :: Seq.Seq Line+                       -- ^ list of replout lines (so far) for unfinished ReplData+                     , pCurrentLine       :: Natural+                     }+  deriving (Eq, Show)++initPState :: PState+initPState = PState AwaitingReplMode Seq.empty Seq.empty Seq.empty 1++-- | P monad for reading in lines+type P = State PState++first3  :: (a -> a') -> (a, b, c) -> (a', b, c)+first3 f (a, b, c) = (f a, b, c)++-- | Like 'stripPrefix', but takes a list of prefixes rather than a single+-- prefix. Returns the first prefix that matches the start of the list along+-- with the remainder of the list.+stripPrefixOneOf :: Eq a => [[a]] -> [a] -> Maybe ([a], [a])+stripPrefixOneOf [] _ = Nothing+stripPrefixOneOf (p:ps) as = case stripPrefix p as of+  Nothing -> stripPrefixOneOf ps as+  Just as' -> Just (p, as')++-- | Like 'stripInfix', but takes a list of infixes. Returns the infix that+-- matches at the earliest index.+stripInfixOneOf :: Eq a => [[a]] -> [a] -> Maybe ([a], [a], [a])+stripInfixOneOf needles haystack+  | Just (needle, suffix) <- stripPrefixOneOf needles haystack+  = Just ([], needle, suffix)+stripInfixOneOf _ [] = Nothing+stripInfixOneOf needles (x:xs) = first3 (x:) <$> stripInfixOneOf needles xs++data InlineRepl = InlineReplin | InlineReplout++-- | Extracts the first inline repl command returns the type of command, its+-- contents, and the remainder of the string.+inlineRepl :: String -> Maybe (InlineRepl, String, String)+inlineRepl s+  | Just (_, ir, s1) <- stripInfixOneOf [ "\\replin|"+                                        , "\\replout|"+                                        , "\\hidereplin|"+                                        , "\\hidereplout|"] s+  , (s2, s3) <- break (=='|') s1 = case ir of+      "\\replin|" -> Just (InlineReplin, s2, s3)+      "\\replout|" -> Just (InlineReplout, s2, s3)+      "\\hidereplin|" -> Just (InlineReplin, s2, s3)+      "\\hidereplout|" -> Just (InlineReplout, s2, s3)+      _ -> error "PANIC: CheckExercises.inlineRepl"+  | otherwise = Nothing++addReplData :: P ()+addReplData = do+  replin <- gets pReplin+  replout <- gets pReplout+  completedReplData <- gets pCompletedReplData+  let completedReplData' = completedReplData Seq.|> ReplData replin replout+  when (not (Seq.null replin && Seq.null replout)) $+    modify' $ \st -> st { pCompletedReplData = completedReplData'+                        , pReplin = Seq.empty+                        , pReplout = Seq.empty+                        }++addReplin :: String -> P ()+addReplin s = do+  ln <- gets pCurrentLine+  replin <- gets pReplin+  modify' $ \st -> st { pReplin = replin Seq.|> Line ln s }++addReplout :: String -> P ()+addReplout s = do+  ln <- gets pCurrentLine+  replout <- gets pReplout+  modify' $ \st -> st { pReplout = replout Seq.|> Line ln s }++nextLine :: P ()+nextLine = modify' $ \st -> st { pCurrentLine = pCurrentLine st + 1 }++stripPrompt :: String -> Maybe String+stripPrompt s = case span isAlpha s of+  (_:_, '>':s') -> Just s'+  _ -> Nothing++-- | The main function for our monad. Input is a single line.+processLine :: String -> P ()+processLine s = do+  let s_nocomment = takeWhile (not . (== '%')) s+      s_nowhitespace = filter (not . isSpace) s_nocomment+  m <- gets pMode+  ln <- gets pCurrentLine+  case m of+    AwaitingReplMode+      | "\\begin{replinVerb}" `isInfixOf` s_nowhitespace -> do+          modify' $ \st -> st { pMode = ReplinMode }+          nextLine+      | "\\begin{reploutVerb}" `isInfixOf` s_nowhitespace -> do+          modify' $ \st -> st { pMode = ReploutMode }+          nextLine+      | "\\begin{replPrompt}" `isInfixOf` s_nowhitespace -> do+          modify' $ \st -> st { pMode = ReplPromptMode }+          nextLine+      | "\\restartrepl" `isInfixOf` s_nowhitespace -> do+          -- This is a command that acts as the barrier between discrete+          -- input/output pairs. When we see it, we commit the current pair,+          -- begin a brand new pair, and advance to the next line.+          addReplData+          nextLine+      | Just (InlineReplin, cmd, rst) <- inlineRepl s -> do+          addReplin cmd+          processLine rst+      | Just (InlineReplout, cmd, rst) <- inlineRepl s -> do+          addReplout cmd+          processLine rst+      | otherwise -> nextLine+    ReplinMode+      | "\\end{replinVerb}" `isInfixOf` s_nowhitespace -> do+          -- Switching from ingesting repl input to awaiting repl input.+          modify' $ \st -> st { pMode = AwaitingReplMode }+          nextLine+      | otherwise -> do+          -- Ingest the current line, and stay in ReplinMode.+          replin <- gets pReplin+          let replin' = replin Seq.|> Line ln s -- use the full input since %+                                                -- isn't a comment in verbatim+                                                -- mode.+          modify' $ \st -> st { pReplin = replin' }+          nextLine+    ReploutMode+      | "\\end{reploutVerb}" `isInfixOf` s_nowhitespace -> do+          -- Switching from ingesting repl output to awaiting repl output.+          modify' $ \st -> st { pMode = AwaitingReplMode }+          nextLine+      | otherwise -> do+          -- Ingest the current line, and stay in ReploutMode.+          replout <- gets pReplout+          let replout' = replout Seq.|> Line ln s -- use the full input since %+                                                  -- isn't a comment in verbatim+                                                  -- mode.+          modify' $ \st -> st { pReplout = replout' }+          nextLine+    ReplPromptMode+      | "\\end{replPrompt}" `isInfixOf` s_nowhitespace -> do+          -- Switching from ingesting repl input/output to awaiting repl+          -- input.+          modify' $ \st -> st { pMode = AwaitingReplMode }+          nextLine+      | Just input <- stripPrompt (trim s) -> do+          replin <- gets pReplin+          let input' = trim input+              replin' = replin Seq.|> Line ln input' -- use the full input since+                                                     -- % isn't a comment in+                                                     -- verbatim mode.+          modify $ \st -> st { pReplin = replin' }+          nextLine+      | otherwise -> do+          replout <- gets pReplout+          let replout' = replout Seq.|> Line ln s -- use the full input since %+                                                  -- isn't a comment in verbatim+                                                  -- mode.+          modify $ \st -> st { pReplout = replout' }+          nextLine++main :: IO ()+main = do+  opts <- execParser p+  allLines <- lines <$> readFile (latexFile opts)+  let PState {..} = flip execState initPState $ do+        -- Process every line+        traverse_ processLine allLines+        -- Insert the final ReplData upon completion+        addReplData+  let allReplData = toList pCompletedReplData+      dir = fromMaybe "." (tempDir opts)++  forM_ allReplData $ \rd -> do+    let inText = unlines $ fmap (trim . lineText) $ toList $ rdReplin rd+        inFileNameTemplate = "in.icry"+    inFile <- writeTempFile dir inFileNameTemplate inText++    let exe = fromMaybe "./cry run" (cryptolExe opts)++    if Seq.null (rdReplout rd)+      then do let cryCmd = (P.shell (exe ++ " --interactive-batch " ++ inFile ++ " -e"))+              (cryEC, cryOut, _) <- P.readCreateProcessWithExitCode cryCmd ""+++              Line lnReplinStart _ Seq.:<| _ <- return $ rdReplin rd+              _ Seq.:|> Line lnReplinEnd _ <- return $ rdReplin rd+              case cryEC of+                ExitFailure _ -> do+                  putStrLn $ "REPL error (replin lines " +++                    show lnReplinStart ++ "-" ++ show lnReplinEnd ++ ")."+                  putStr cryOut+                  exitFailure+                ExitSuccess -> do+                  -- remove temporary input file+                  removeFile inFile+      else do let outExpectedText = unlines $ filter (not . null) $+                    fmap (trim . lineText) $ toList $ rdReplout rd+                  outExpectedFileNameTemplate = "out-expected.icry"+                  outFileNameTemplate = "out.icry"+                  cryCmd = (P.shell (exe ++ " --interactive-batch " ++ inFile))+              outExpectedFile <- writeTempFile dir outExpectedFileNameTemplate outExpectedText+              outFile <- emptyTempFile dir outFileNameTemplate++              (_, cryOut, _) <- P.readCreateProcessWithExitCode cryCmd ""++              -- remove temporary input file+              removeFile inFile++              let outText = unlines $ filter (not . null) $ trim <$> (dropWhile ("Loading module" `isPrefixOf`) $ lines cryOut)++              writeFile outFile outText++              let diffCmd = (P.shell ("diff -u " ++ outExpectedFile ++ " " ++ outFile))++              (diffEC, diffOut, _) <- P.readCreateProcessWithExitCode diffCmd ""+              case diffEC of+                ExitSuccess -> do+                  -- Remove temporary output files+                  removeFile outExpectedFile+                  removeFile outFile+                ExitFailure _ -> do+                  Line lnReplinStart _ Seq.:<| _ <- return $ rdReplin rd+                  _ Seq.:|> Line lnReplinEnd _ <- return $ rdReplin rd+                  Line lnReploutStart _ Seq.:<| _ <- return $ rdReplout rd+                  _ Seq.:|> Line lnReploutEnd _ <- return $ rdReplout rd++                  putStrLn $ "REPL output mismatch in " ++ latexFile opts+                  putStrLn $ "  (replin lines " +++                    show lnReplinStart ++ "-" ++ show lnReplinEnd +++                    ", replout lines " ++ show lnReploutStart ++ "-" +++                    show lnReploutEnd ++ ")."+                  putStrLn $ "Diff output:"+                  putStr diffOut++                  let outExpectedFileName = dir ++ "/" ++ outExpectedFileNameTemplate+                      outFileName = dir ++ "/" ++ outFileNameTemplate++                  putStrLn ""+                  putStrLn $ "Expected output written to: " ++ outExpectedFileName+                  putStrLn $ "Actual output written to: " ++ outFileName++                  -- Write to log files+                  writeFile outExpectedFileName outExpectedText+                  writeFile outFileName outText++                  -- Remove temporary output files and exit+                  removeFile outExpectedFile+                  removeFile outFile+                  exitFailure++  putStrLn $ "Successfully checked " ++ show (length allReplData) ++ " repl examples in " ++ latexFile opts++  return ()++  where p = info (optsParser <**> helper)+            ( fullDesc+              <> progDesc "Test the exercises in a cryptol LaTeX file"+              <> header "check-exercises -- test cryptol exercises"+            )

@@ -26,7 +26,6 @@ import Cryptol.Version (displayVersion)  import Control.Monad (when)-import Data.Maybe (isJust) import GHC.IO.Encoding (setLocaleEncoding, utf8) import System.Console.GetOpt     (OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo)@@ -47,7 +46,8 @@   { optLoad            :: [FilePath]   , optVersion         :: Bool   , optHelp            :: Bool-  , optBatch           :: Maybe FilePath+  , optBatch           :: ReplMode+  , optCallStacks      :: Bool   , optCommands        :: [String]   , optColorMode       :: ColorMode   , optCryptolrc       :: Cryptolrc@@ -61,7 +61,8 @@   { optLoad            = []   , optVersion         = False   , optHelp            = False-  , optBatch           = Nothing+  , optBatch           = InteractiveRepl+  , optCallStacks      = True   , optCommands        = []   , optColorMode       = AutoColor   , optCryptolrc       = CryrcDefault@@ -75,6 +76,9 @@   [ Option "b" ["batch"] (ReqArg setBatchScript "FILE")     "run the script provided and exit" +  , Option "" ["interactive-batch"] (ReqArg setInteractiveBatchScript "FILE")+    "run the script provided and exit, but behave as if running an interactive session"+   , Option "e" ["stop-on-error"] (NoArg setStopOnError)     "stop script execution as soon as an error occurs." @@ -95,6 +99,9 @@   , Option "h" ["help"] (NoArg setHelp)     "display this message" +  , Option "" ["no-call-stacks"] (NoArg setNoCallStacks)+    "Disable tracking of call stack information, which reduces interpreter overhead"+   , Option "" ["no-unicode-logo"] (NoArg setNoUnicodeLogo)     "Don't use unicode characters in the REPL logo" @@ -124,8 +131,12 @@  -- | Set a batch script to be run. setBatchScript :: String -> OptParser Options-setBatchScript path = modify $ \ opts -> opts { optBatch = Just path }+setBatchScript path = modify $ \ opts -> opts { optBatch = Batch path } +-- | Set an interactive batch script+setInteractiveBatchScript :: String -> OptParser Options+setInteractiveBatchScript path = modify $ \ opts -> opts { optBatch = InteractiveBatch path }+ -- | Set the color mode of the terminal output. setColorMode :: String -> OptParser Options setColorMode "auto"   = modify $ \ opts -> opts { optColorMode = AutoColor }@@ -149,6 +160,10 @@ setCryrcDisabled :: OptParser Options setCryrcDisabled  = modify $ \ opts -> opts { optCryptolrc = CryrcDisabled } +-- | Disable call stack tracking+setNoCallStacks :: OptParser Options+setNoCallStacks = modify $ \opts -> opts { optCallStacks = False }+ -- | Add another file to read as a @.cryptolrc@ file, unless @.cryptolrc@ -- files have been disabled addCryrc :: String -> OptParser Options@@ -180,9 +195,15 @@             , "addition to the default locations"             ]           )+        , ( "EDITOR"+          , [ "Sets the editor executable to use when opening an editor"+            , "via the `:edit` command"+            ]+          )         , ( "SBV_{ABC,BOOLECTOR,CVC4,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"             ]           )         ]@@ -206,6 +227,7 @@           (opts', mCleanup) <- setupCmdScript opts           status <- repl (optCryptolrc opts')                          (optBatch opts')+                         (optCallStacks opts')                          (optStopOnError opts')                          (setupREPL opts')           case mCleanup of@@ -225,9 +247,9 @@       (path, h) <- openTempFile tmpdir "cmds.icry"       hPutStr h (unlines cmds)       hClose h-      when (isJust (optBatch opts)) $+      when (optBatch opts /= InteractiveRepl) $         putStrLn "[warning] --command argument specified; ignoring batch file"-      return (opts { optBatch = Just path }, Just path)+      return (opts { optBatch = InteractiveBatch path }, Just path)  setupREPL :: Options -> REPL () setupREPL opts = do@@ -261,9 +283,10 @@   setUpdateREPLTitle (shouldSetREPLTitle >>= \b -> when b setREPLTitle)   updateREPLTitle   case optBatch opts of-    Nothing -> return ()     -- add the directory containing the batch file to the module search path-    Just file -> prependSearchPath [ takeDirectory file ]+    Batch file -> prependSearchPath [ takeDirectory file ]+    _ -> return ()+   case optLoad opts of     []  -> loadPrelude `REPL.catch` \x -> io $ print $ pp x     [l] -> loadCmd l `REPL.catch` \x -> do

@@ -29,7 +29,6 @@ import           Data.Char (isAlphaNum, isSpace) import           Data.Function (on) import           Data.List (isPrefixOf,nub,sortBy,sort)-import           Data.Maybe(isJust) import qualified Data.Set as Set import qualified Data.Text as T (unpack) import           System.Console.ANSI (setTitle, hSupportsANSI)@@ -44,42 +43,57 @@ 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 :: Maybe FilePath -> Bool -> REPL CommandExitCode-crySession mbBatch stopOnError =+crySession :: ReplMode -> Bool -> REPL CommandExitCode+crySession replMode stopOnError =   do settings <- io (setHistoryFile (replSettings isBatch))-     let act = runInputTBehavior behavior settings (withInterrupt loop)+     let act = runInputTBehavior behavior settings (withInterrupt (loop 1))      if isBatch then asBatch act else act   where-  (isBatch,behavior) = case mbBatch of-    Nothing   -> (False,defaultBehavior)-    Just path -> (True,useFile path)+  (isBatch,behavior) = case replMode of+    InteractiveRepl       -> (False, defaultBehavior)+    Batch path            -> (True,  useFile path)+    InteractiveBatch path -> (False, useFile path) -  loop :: InputT REPL CommandExitCode-  loop =+  loop :: Int -> InputT REPL CommandExitCode+  loop lineNum =     do ln <- getInputLines =<< MTL.lift getPrompt        case ln of          NoMoreLines -> return CommandOk          Interrupted            | isBatch && stopOnError -> return CommandError-           | otherwise -> loop-         NextLine line-           | all isSpace line -> loop-           | otherwise        -> doCommand line+           | otherwise -> loop lineNum+         NextLine ls+           | all (all isSpace) ls -> loop (lineNum + length ls)+           | otherwise            -> doCommand lineNum ls -  doCommand txt =-    case parseCommand findCommandExact txt of-      Nothing | isBatch && stopOnError  -> return CommandError-              | otherwise -> loop -- say somtething?+  run lineNum cmd =+    case replMode of+      InteractiveRepl    -> runCommand lineNum Nothing cmd+      InteractiveBatch _ -> runCommand lineNum Nothing cmd+      Batch path         -> runCommand lineNum (Just path) cmd++  doCommand lineNum txt =+    case parseCommand findCommandExact (unlines txt) of+      Nothing | isBatch && stopOnError -> return CommandError+              | otherwise -> loop (lineNum + length txt)  -- say somtething?       Just cmd -> join $ MTL.lift $-        do status <- handleInterrupt (handleCtrlC CommandError) (runCommand cmd)+        do status <- handleInterrupt (handleCtrlC CommandError) (run lineNum cmd)            case status of              CommandError | isBatch && stopOnError -> return (return status)              _ -> do goOn <- shouldContinue-                     return (if goOn then loop else return status)+                     return (if goOn then loop (lineNum + length txt) else return status)  -data NextLine = NextLine String | NoMoreLines | Interrupted+data NextLine = NextLine [String] | NoMoreLines | Interrupted  getInputLines :: String -> InputT REPL NextLine getInputLines = handleInterrupt (MTL.lift (handleCtrlC Interrupted)) . loop []@@ -91,7 +105,7 @@          Nothing -> return NoMoreLines          Just l            | not (null l) && last l == '\\' -> loop (init l : ls) newPropmpt-           | otherwise -> return $ NextLine $ unlines $ reverse $ l : ls+           | otherwise -> return $ NextLine $ reverse $ l : ls  loadCryRC :: Cryptolrc -> REPL CommandExitCode loadCryRC cryrc =@@ -106,25 +120,32 @@        let file = dir </> ".cryptolrc"        present <- io (doesFileExist file)        if present-         then crySession (Just file) True+         then crySession (Batch file) True          else check others    loadMany []       = return CommandOk-  loadMany (f : fs) = do status <- crySession (Just f) True+  loadMany (f : fs) = do status <- crySession (Batch f) True                          case status of                            CommandOk -> loadMany fs                            _         -> return status  -- | Haskeline-specific repl implementation.-repl :: Cryptolrc -> Maybe FilePath -> Bool -> REPL () -> IO CommandExitCode-repl cryrc mbBatch stopOnError begin =-  runREPL (isJust mbBatch) stdoutLogger $-  do status <- loadCryRC cryrc-     case status of-       CommandOk -> begin >> crySession mbBatch stopOnError-       _         -> return status+repl :: Cryptolrc -> ReplMode -> Bool -> Bool -> REPL () -> IO CommandExitCode+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+       case status of+         CommandOk -> begin >> crySession replMode stopOnError+         _         -> return status  -- | Try to set the history file. setHistoryFile :: Settings REPL -> IO (Settings REPL)@@ -201,7 +222,7 @@ cryptolCommand :: CompletionFunc REPL cryptolCommand cursor@(l,r)   | ":" `isPrefixOf` l'-  , Just (cmd,rest) <- splitCommand l' = case nub (findCommand cmd) of+  , Just (_,cmd,rest) <- splitCommand l' = case nub (findCommand cmd) of        [c] | null rest && not (any isSpace l') -> do             return (l, cmdComp cmd c)

@@ -14,6 +14,8 @@ import Cryptol.Version (commitShortHash,commitDirty) import Data.Version (showVersion) import System.Console.ANSI+import Prelude ()+import Prelude.Compat   type Version = String

@@ -168,6 +168,13 @@ primitive type Literal : # -> * -> Prop  /**+ * 'LiteralLessThan n a' asserts that the type 'a' contains all the+ * natural numbers strictly below 'n'.  Note that we may have 'n = inf',+ * in which case the type 'a' must be unbounded.+ */+primitive type LiteralLessThan : # -> * -> Prop++/**  * The value corresponding to a numeric type.  */ primitive number : {val, rep} Literal val rep => rep@@ -195,6 +202,15 @@                                     [1 + (last - first)]a  /**+ * A possibly infinite sequence counting up from 'first' up to (but not including) 'bound'.+ *+ * Note that if 'first' = 'bound' then the sequence will be empty.+ */+primitive fromToLessThan :+  {first, bound, a} (fin first, bound >= first, LiteralLessThan bound a) => [bound - first]a+++/**  * A finite arithmetic sequence starting with 'first' and 'next',  * stopping when the values reach or would skip over 'last'.  *@@ -879,8 +895,8 @@  * Declarations of the form 'x @ i = e' are syntactic sugar for  * 'x = generate (\i -> e)'.  */-generate : {n, a, ix} (fin n, n >= 1, Integral ix, Literal (n-1) ix) => (ix -> a) -> [n]a-generate f = [ f i | i <- [0 .. n-1] ]+generate : {n, a, ix} (Integral ix, LiteralLessThan n ix) => (ix -> a) -> [n]a+generate f = [ f i | i <- [0 .. <n] ]   // GF_2^n polynomial computations -------------------------------------------

@@ -79,6 +79,7 @@ primitive   fpPosInf : {e,p} ValidFloat e p => Float e p +/** Negative infinity. */ fpNegInf : {e,p} ValidFloat e p => Float e p fpNegInf = - fpPosInf @@ -133,13 +134,33 @@  infix 20 =.= +/** Test if this value is not-a-number (NaN). */+primitive fpIsNaN : {e,p} ValidFloat e p => Float e p -> Bool -/* Returns true for numbers that are not an infinity or NaN. */-primitive-  fpIsFinite : {e,p} ValidFloat e p => Float e p -> Bool+/** Test if this value is positive or negative infinity. */+primitive fpIsInf : {e,p} ValidFloat e p => Float e p -> Bool +/** Test if this value is positive or negative zero. */+primitive fpIsZero : {e,p} ValidFloat e p => Float e p -> Bool +/** Test if this value is negative. */+primitive fpIsNeg : {e,p} ValidFloat e p => Float e p -> Bool +/** Test if this value is normal (not NaN, not infinite, not zero, and not subnormal). */+primitive fpIsNormal : {e,p} ValidFloat e p => Float e p -> Bool++/**+ * Test if this value is subnormal.  Subnormal values are nonzero+ * values with magnitudes smaller than can be represented with the+ * normal implicit leading bit convention.+ */+primitive fpIsSubnormal : {e,p} ValidFloat e p => Float e p -> Bool++/* Returns true for numbers that are not an infinity or NaN. */+fpIsFinite : {e,p} ValidFloat e p => Float e p -> Bool+fpIsFinite f = ~ (fpIsNaN f \/ fpIsInf f )++ /* ----------------------------------------------------------------------  * Arithmetic  * ---------------------------------------------------------------------- */@@ -165,7 +186,31 @@   fpDiv : {e,p} ValidFloat e p =>     RoundingMode -> Float e p -> Float e p -> Float e p +/**+ * Fused-multiply-add.  'fpFMA r x y z' computes the value '(x*y)+z',+ * rounding the result according to mode 'r' only after performing both+ * operations.+ */+primitive+  fpFMA : {e,p} ValidFloat e p =>+    RoundingMode -> Float e p -> Float e p -> Float e p -> Float e p +/**+ * Absolute value of a floating-point value.+ */+primitive+  fpAbs : {e,p} ValidFloat e p =>+    Float e p -> Float e p++/**+ * Square root of a floating-point value.  The square root of+ * a negative value yiels NaN, except that the sqaure root of+ * '-0.0' is '-0.0'.+ */+primitive+  fpSqrt : {e,p} ValidFloat e p =>+    RoundingMode -> Float e p -> Float e p+ /* ------------------------------------------------------------ *  * Rationals                                                    *  * ------------------------------------------------------------ */@@ -181,4 +226,3 @@ primitive   fpFromRational : {e,p} ValidFloat e p =>     RoundingMode -> Rational -> Float e p-

@@ -27,39 +27,32 @@   , rationalLessThan   , rationalGreaterThan   , iteRational-  , ppRational   ) where  import Control.Monad.IO.Class import Data.Kind (Type)-import Data.Ratio ( (%), numerator, denominator )  import Cryptol.Backend.FloatHelpers (BF)-import Cryptol.Backend.Monad ( PPOpts(..), EvalError(..) )-import Cryptol.TypeCheck.AST(Name)-import Cryptol.Utils.PP-+import Cryptol.Backend.Monad+  ( EvalError(..), CallStack, pushCallFrame )+import Cryptol.ModuleSystem.Name(Name)+import Cryptol.Parser.Position  invalidIndex :: Backend sym => sym -> Integer -> SEval sym a-invalidIndex sym = raiseError sym . InvalidIndex . Just+invalidIndex sym i = raiseError sym (InvalidIndex (Just i))  cryUserError :: Backend sym => sym -> String -> SEval sym a-cryUserError sym = raiseError sym . UserError+cryUserError sym msg = raiseError sym (UserError msg)  cryNoPrimError :: Backend sym => sym -> Name -> SEval sym a-cryNoPrimError sym = raiseError sym . NoPrim-+cryNoPrimError sym nm = raiseError sym (NoPrim nm)  {-# INLINE sDelay #-} -- | Delay the given evaluation computation, returning a thunk --   which will run the computation when forced.  Raise a loop --   error if the resulting thunk is forced during its own evaluation.-sDelay :: Backend sym => sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)-sDelay sym msg m =-  let msg'  = maybe "" ("while evaluating "++) msg-      retry = raiseError sym (LoopError msg')-   in sDelayFill sym m retry-+sDelay :: Backend sym => sym -> SEval sym a -> SEval sym (SEval sym a)+sDelay sym m = sDelayFill sym m Nothing ""  -- | Representation of rational numbers. --     Invariant: denominator is not 0@@ -198,16 +191,6 @@ iteRational sym p (SRational a b) (SRational c d) =   SRational <$> iteInteger sym p a c <*> iteInteger sym p b d -ppRational :: Backend sym => sym -> PPOpts -> SRational sym -> Doc-ppRational sym opts (SRational n d)-  | Just ni <- integerAsLit sym n-  , Just di <- integerAsLit sym d-  = let q = ni % di in-      text "(ratio" <+> integer (numerator q) <+> (integer (denominator q) <> text ")")--  | otherwise-  = text "(ratio" <+> ppInteger sym opts n <+> (ppInteger sym opts d <> text ")")- -- | This type class defines a collection of operations on bits, words and integers that --   are necessary to define generic evaluator primitives that operate on both concrete --   and symbolic values uniformly.@@ -234,13 +217,27 @@   --   which will run the computation when forced.  Run the 'retry'   --   computation instead if the resulting thunk is forced during   --   its own evaluation.-  sDelayFill :: sym -> SEval sym a -> SEval sym a -> SEval sym (SEval sym a)+  sDelayFill :: sym -> SEval sym a -> Maybe (SEval sym a) -> String -> SEval sym (SEval sym a)    -- | Begin evaluating the given computation eagerly in a separate thread   --   and return a thunk which will await the completion of the given computation   --   when forced.   sSpark :: sym -> SEval sym a -> SEval sym (SEval sym a) +  -- | Push a call frame on to the current call stack while evaluating the given action+  sPushFrame :: sym -> Name -> Range -> SEval sym a -> SEval sym a+  sPushFrame sym nm rng m = sModifyCallStack sym (pushCallFrame nm rng) m++  -- | Use the given call stack while evaluating the given action+  sWithCallStack :: sym -> CallStack -> SEval sym a -> SEval sym a+  sWithCallStack sym stk m = sModifyCallStack sym (\_ -> stk) m++  -- | Apply the given function to the current call stack while evaluating the given action+  sModifyCallStack :: sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a++  -- | Retrieve the current evaluation call stack+  sGetCallStack :: sym -> SEval sym CallStack+   -- | Merge the two given computations according to the predicate.   mergeEval ::      sym ->@@ -257,21 +254,6 @@   -- | Indiciate that an error condition exists   raiseError :: sym -> EvalError -> SEval sym a --  -- ==== Pretty printing  ====-  -- | Pretty-print an individual bit-  ppBit :: sym -> SBit sym -> Doc--  -- | Pretty-print a word value-  ppWord :: sym -> PPOpts -> SWord sym -> Doc--  -- | Pretty-print an integer value-  ppInteger :: sym -> PPOpts -> SInteger sym -> Doc--  -- | Pretty-print a floating-point value-  ppFloat :: sym -> PPOpts -> SFloat sym -> Doc--   -- ==== Identifying literal values ====    -- | Determine if this symbolic bit is a boolean literal@@ -291,6 +273,9 @@   -- | Determine if this symbolic integer is a literal   integerAsLit :: sym -> SInteger sym -> Maybe Integer +  -- | Determine if this symbolic floating-point value is a literal+  fpAsLit :: sym -> SFloat sym -> Maybe BF+   -- ==== Creating literal values ====    -- | Construct a literal bit value from a boolean.@@ -325,6 +310,7 @@   iteBit :: sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)   iteWord :: sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)   iteInteger :: sym -> SBit sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)+  iteFloat :: sym -> SBit sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)    -- ==== Bit operations ====   bitEq  :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)@@ -333,7 +319,6 @@   bitXor :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)   bitComplement :: sym -> SBit sym -> SEval sym (SBit sym) -   -- ==== Word operations ====    -- | Extract the numbered bit from the word.@@ -674,7 +659,7 @@     SInteger sym ->     SEval sym (SBit sym) -  -- | Multiplicitive inverse in (Z n).+  -- | Multiplicative inverse in (Z n).   --   PRECONDITION: the modulus is a prime   znRecip ::     sym ->@@ -689,21 +674,51 @@    fpLogicalEq   :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym) +  fpNaN    :: sym -> Integer {- ^ exponent bits -} -> Integer {- ^ precision bits -} -> SEval sym (SFloat sym)+  fpPosInf :: sym -> Integer {- ^ exponent bits -} -> Integer {- ^ precision bits -} -> SEval sym (SFloat sym)+   fpPlus, fpMinus, fpMult, fpDiv :: FPArith2 sym-  fpNeg :: sym -> SFloat sym -> SEval sym (SFloat sym)+  fpNeg, fpAbs :: sym -> SFloat sym -> SEval sym (SFloat sym)+  fpSqrt :: sym -> SWord sym -> SFloat sym -> SEval sym (SFloat sym) +  fpFMA :: sym -> SWord sym -> SFloat sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)++  fpIsZero, fpIsNeg, fpIsNaN, fpIsInf, fpIsNorm, fpIsSubnorm :: sym -> SFloat sym -> SEval sym (SBit sym)++  fpToBits :: sym -> SFloat sym -> SEval sym (SWord sym)+  fpFromBits ::+    sym ->+    Integer {- ^ exponent bits -} ->+    Integer {- ^ precision bits -} ->+    SWord sym ->+    SEval sym (SFloat sym)+   fpToInteger ::     sym ->     String {- ^ Name of the function for error reporting -} ->-    SWord sym {-^ Rounding mode -} ->-    SFloat sym -> SEval sym (SInteger sym)+    SWord sym {- ^ Rounding mode -} ->+    SFloat sym ->+    SEval sym (SInteger sym)    fpFromInteger ::     sym ->-    Integer         {- exp width -} ->-    Integer         {- prec width -} ->+    Integer         {- ^ exp width -} ->+    Integer         {- ^ prec width -} ->     SWord sym       {- ^ rounding mode -} ->-    SInteger sym    {- ^ the integeer to use -} ->+    SInteger sym    {- ^ the integer to use -} ->+    SEval sym (SFloat sym)++  fpToRational ::+    sym ->+    SFloat sym ->+    SEval sym (SRational sym)++  fpFromRational ::+    sym ->+    Integer         {- ^ exp width -} ->+    Integer         {- ^ prec width -} ->+    SWord sym       {- ^ rounding mode -} ->+    SRational sym ->     SEval sym (SFloat sym)  type FPArith2 sym =

@@ -37,6 +37,7 @@  import qualified Control.Exception as X import Data.Bits+import Data.Ratio import Numeric (showIntAtBase) import qualified LibBF as FP import qualified GHC.Integer.GMP.Internals as Integer@@ -136,10 +137,12 @@   type SFloat Concrete = FP.BF   type SEval Concrete = Eval -  raiseError _ err = io (X.throwIO err)+  raiseError _ err =+    do stk <- getCallStack+       io (X.throwIO (EvalErrorEx stk err))    assertSideCondition _ True _ = return ()-  assertSideCondition _ False err = io (X.throwIO err)+  assertSideCondition sym False err = raiseError sym err    wordLen _ (BV w _) = w   wordAsChar _ (BV _ x) = Just $! integerToChar x@@ -160,15 +163,8 @@   sDeclareHole _ = blackhole   sDelayFill _ = delayFill   sSpark _ = evalSpark--  ppBit _ b | b         = text "True"-            | otherwise = text "False"--  ppWord _ = ppBV--  ppInteger _ _opts i = integer i--  ppFloat _ = FP.fpPP+  sModifyCallStack _ f m = modifyCallStack f m+  sGetCallStack _ = getCallStack    bitLit _ b = b   bitAsLit _ b = Just b@@ -182,6 +178,7 @@   iteBit _ b x y  = pure $! if b then x else y   iteWord _ b x y = pure $! if b then x else y   iteInteger _ b x y = pure $! if b then x else y+  iteFloat _ b x y   = pure $! if b then x else y    wordLit _ w i = pure $! mkBv w i   wordAsLit _ (BV w i) = Just (w,i)@@ -331,6 +328,11 @@   ------------------------------------------------------------------------   -- Floating Point   fpLit _sym e p rat     = pure (FP.fpLit e p rat)++  fpNaN _sym e p         = pure (FP.BF e p FP.bfNaN)+  fpPosInf _sym e p      = pure (FP.BF e p FP.bfPosInf)++  fpAsLit _ f            = Just f   fpExactLit _sym bf     = pure bf   fpEq _sym x y          = pure (FP.bfValue x == FP.bfValue y)   fpLogicalEq _sym x y   = pure (FP.bfCompare (FP.bfValue x) (FP.bfValue y) == EQ)@@ -340,17 +342,51 @@   fpMinus = fpBinArith FP.bfSub   fpMult  = fpBinArith FP.bfMul   fpDiv   = fpBinArith FP.bfDiv-  fpNeg _ x = pure x { FP.bfValue = FP.bfNeg (FP.bfValue x) }+  fpNeg _ x = pure $! x { FP.bfValue = FP.bfNeg (FP.bfValue x) }++  fpAbs _ x = pure $! x { FP.bfValue = FP.bfAbs (FP.bfValue x) }+  fpSqrt sym r x =+    do r' <- fpRoundMode sym r+       let opts = FP.fpOpts (FP.bfExpWidth x) (FP.bfPrecWidth x) r'+       pure $! x{ FP.bfValue = FP.fpCheckStatus (FP.bfSqrt opts (FP.bfValue x)) }++  fpFMA sym r x y z =+    do r' <- fpRoundMode sym r+       let opts = FP.fpOpts (FP.bfExpWidth x) (FP.bfPrecWidth x) r'+       pure $! x { FP.bfValue = FP.fpCheckStatus (FP.bfFMA opts (FP.bfValue x) (FP.bfValue y) (FP.bfValue z)) }++  fpIsZero _ x = pure (FP.bfIsZero (FP.bfValue x))+  fpIsNeg _ x  = pure (FP.bfIsNeg (FP.bfValue x))+  fpIsNaN _ x  = pure (FP.bfIsNaN (FP.bfValue x))+  fpIsInf _ x  = pure (FP.bfIsInf (FP.bfValue x))+  fpIsNorm _ x =+    let opts = FP.fpOpts (FP.bfExpWidth x) (FP.bfPrecWidth x) FP.NearEven+     in pure (FP.bfIsNormal opts (FP.bfValue x))+  fpIsSubnorm _ x =+    let opts = FP.fpOpts (FP.bfExpWidth x) (FP.bfPrecWidth x) FP.NearEven+     in pure (FP.bfIsSubnormal opts (FP.bfValue x))++  fpFromBits _sym e p bv = pure (FP.floatFromBits e p (bvVal bv))+  fpToBits _sym (FP.BF e p v) = pure (mkBv (e+p) (FP.floatToBits e p v))+   fpFromInteger sym e p r x =-    do opts <- FP.fpOpts e p <$> fpRoundMode sym r+    do r' <- fpRoundMode sym r        pure FP.BF { FP.bfExpWidth = e                   , FP.bfPrecWidth = p                   , FP.bfValue = FP.fpCheckStatus $-                                 FP.bfRoundInt opts (FP.bfFromInteger x)+                                 FP.bfRoundInt r' (FP.bfFromInteger x)                   }   fpToInteger = fpCvtToInteger +  fpFromRational sym e p r x =+    do mode <- fpRoundMode sym r+       pure (FP.floatFromRational e p mode (sNum x % sDenom x)) +  fpToRational sym fp =+      case FP.floatToRational "fpToRational" fp of+        Left err -> raiseError sym err+        Right r  -> pure $ SRational { sNum = numerator r, sDenom = denominator r }+ {-# INLINE liftBinIntMod #-} liftBinIntMod :: Monad m =>   (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer -> m Integer@@ -371,7 +407,7 @@ fpBinArith fun = \sym r x y ->   do opts <- FP.fpOpts (FP.bfExpWidth x) (FP.bfPrecWidth x)                                                   <$> fpRoundMode sym r-     pure x { FP.bfValue = FP.fpCheckStatus+     pure $! x { FP.bfValue = FP.fpCheckStatus                                 (fun opts (FP.bfValue x) (FP.bfValue y)) }  fpCvtToInteger ::@@ -391,8 +427,3 @@   case FP.fpRound (bvVal w) of     Left err -> raiseError sym err     Right a  -> pure a-----

@@ -2,22 +2,19 @@ {-# Language BangPatterns #-} module Cryptol.Backend.FloatHelpers where +import Data.Char (isDigit) import Data.Ratio(numerator,denominator)-import Data.Int(Int64)-import Data.Bits(testBit,setBit,shiftL,shiftR,(.&.),(.|.)) import LibBF  import Cryptol.Utils.PP import Cryptol.Utils.Panic(panic)-import Cryptol.Backend.Monad( EvalError(..)-                         , PPOpts(..), PPFloatFormat(..), PPFloatExp(..)-                         )+import Cryptol.Backend.Monad( EvalError(..) )   data BF = BF-  { bfExpWidth  :: Integer-  , bfPrecWidth :: Integer-  , bfValue     :: BigFloat+  { bfExpWidth  :: !Integer+  , bfPrecWidth :: !Integer+  , bfValue     :: !BigFloat   }  @@ -86,19 +83,32 @@   str = bfToString base fmt num   fmt = addPrefix <> showRnd NearEven <>         case useFPFormat opts of-          FloatFree e -> withExp e $ showFreeMin+          FloatFree e -> withExp e $ showFree                                    $ Just $ fromInteger precW           FloatFixed n e -> withExp e $ showFixed $ fromIntegral n           FloatFrac n    -> showFrac $ fromIntegral n    -- non-base 10 literals are not overloaded so we add an explicit-  -- .0 if one is not present. +  -- .0 if one is not present.  Moreover, we trim any extra zeros+  -- that appear in a decimal representation.   hacStr-    | base == 10 || elem '.' str = str+    | base == 10   = trimZeros+    | elem '.' str = str     | otherwise = case break (== 'p') str of                     (xs,ys) -> xs ++ ".0" ++ ys +  trimZeros =+    case break (== '.') str of+      (xs,'.':ys) ->+        case break (not . isDigit) ys of+          (frac, suffix) -> xs ++ '.' : processFraction frac ++ suffix+      _ -> str +  processFraction frac =+    case dropWhile (== '0') (reverse frac) of+      [] -> "0"+      zs -> reverse zs+ -- | Make a literal fpLit ::   Integer     {- ^ Exponent width -} ->@@ -152,97 +162,17 @@                               ["Unexpected rounding mode", show r]  -- floatFromBits ::    Integer {- ^ Exponent width -} ->   Integer {- ^ Precision widht -} ->   Integer {- ^ Raw bits -} ->   BF-floatFromBits e p bv = BF { bfValue = floatFromBits' e p bv+floatFromBits e p bv = BF { bfValue = bfFromBits (fpOpts e p NearEven) bv                            , bfExpWidth = e, bfPrecWidth = p }  ---- | Make a float using "raw" bits.-floatFromBits' ::-  Integer {- ^ Exponent width -} ->-  Integer {- ^ Precision widht -} ->-  Integer {- ^ Raw bits -} ->-  BigFloat--floatFromBits' e p bits-  | expoBiased == 0 && mant == 0 =            -- zero-    if isNeg then bfNegZero else bfPosZero--  | expoBiased == eMask && mant ==  0 =       -- infinity-    if isNeg then bfNegInf else bfPosInf--  | expoBiased == eMask = bfNaN               -- NaN--  | expoBiased == 0 =                         -- Subnormal-    case bfMul2Exp opts (bfFromInteger mant) (expoVal + 1) of-      (num,Ok) -> if isNeg then bfNeg num else num-      (_,s)    -> panic "floatFromBits" [ "Unexpected status: " ++ show s ]--  | otherwise =                               -- Normal-    case bfMul2Exp opts (bfFromInteger mantVal) expoVal of-      (num,Ok) -> if isNeg then bfNeg num else num-      (_,s)    -> panic "floatFromBits" [ "Unexpected status: " ++ show s ]--  where-  opts       = expBits e' <> precBits (p' + 1) <> allowSubnormal--  e'         = fromInteger e                               :: Int-  p'         = fromInteger p - 1                           :: Int-  eMask      = (1 `shiftL` e') - 1                         :: Int64-  pMask      = (1 `shiftL` p') - 1                         :: Integer--  isNeg      = testBit bits (e' + p')--  mant       = pMask .&. bits                              :: Integer-  mantVal    = mant `setBit` p'                            :: Integer-  -- accounts for the implicit 1 bit--  expoBiased = eMask .&. fromInteger (bits `shiftR` p')    :: Int64-  bias       = eMask `shiftR` 1                            :: Int64-  expoVal    = expoBiased - bias - fromIntegral p'         :: Int64-- -- | Turn a float into raw bits. -- @NaN@ is represented as a positive "quiet" @NaN@ -- (most significant bit in the significand is set, the rest of it is 0) floatToBits :: Integer -> Integer -> BigFloat -> Integer-floatToBits e p bf =  (isNeg      `shiftL` (e' + p'))-                  .|. (expBiased  `shiftL` p')-                  .|. (mant       `shiftL` 0)-  where-  e' = fromInteger e     :: Int-  p' = fromInteger p - 1 :: Int--  eMask = (1 `shiftL` e') - 1   :: Integer-  pMask = (1 `shiftL` p') - 1   :: Integer--  (isNeg, expBiased, mant) =-    case bfToRep bf of-      BFNaN       -> (0,  eMask, 1 `shiftL` (p' - 1))-      BFRep s num -> (sign, be, ma)-        where-        sign = case s of-                Neg -> 1-                Pos -> 0--        (be,ma) =-          case num of-            Zero     -> (0,0)-            Num i ev-              | ex == 0   -> (0, i `shiftL` (p' - m  -1))-              | otherwise -> (ex, (i `shiftL` (p' - m)) .&. pMask)-              where-              m    = msb 0 i - 1-              bias = eMask `shiftR` 1-              ex   = toInteger ev + bias + toInteger m--            Inf -> (eMask,0)--  msb !n j = if j == 0 then n else msb (n+1) (j `shiftR` 1)+floatToBits e p bf = bfToBits (fpOpts e p NearEven) bf

@@ -1,6 +1,6 @@ -- |--- Module      :  Cryptol.Eval.Monad--- Copyright   :  (c) 2013-2016 Galois, Inc.+-- Module      :  Cryptol.Backend.Monad+-- Copyright   :  (c) 2013-2020 Galois, Inc. -- License     :  BSD3 -- Maintainer  :  cryptol@galois.com -- Stability   :  provisional@@ -16,80 +16,97 @@ ( -- * Evaluation monad   Eval(..) , runEval-, EvalOpts(..)-, PPOpts(..)-, asciiMode-, PPFloatFormat(..)-, PPFloatExp(..)-, defaultPPOpts , io , delayFill , ready , blackhole , evalSpark , maybeReady+  -- * Call stacks+, CallStack+, getCallStack+, withCallStack+, modifyCallStack+, combineCallStacks+, pushCallFrame+, displayCallStack   -- * Error reporting , Unsupported(..) , EvalError(..)+, EvalErrorEx(..) , evalPanic , wordTooWide-, typeCannotBeDemoted+, WordTooWide(..) ) where  import           Control.Concurrent import           Control.Concurrent.STM  import           Control.Monad-import qualified Control.Monad.Fail as Fail-import           Control.Monad.Fix import           Control.Monad.IO.Class+import           Data.Foldable (toList)+import           Data.Sequence (Seq)+import qualified Data.Sequence as Seq import           Data.Typeable (Typeable) import qualified Control.Exception as X  +import Cryptol.Parser.Position import Cryptol.Utils.Panic import Cryptol.Utils.PP-import Cryptol.Utils.Logger(Logger)-import Cryptol.TypeCheck.AST(Type,Name)+import Cryptol.TypeCheck.AST(Name)  -- | A computation that returns an already-evaluated value. ready :: a -> Eval a ready a = Ready a --- | How to pretty print things when evaluating-data PPOpts = PPOpts-  { useAscii     :: Bool-  , useBase      :: Int-  , useInfLength :: Int-  , useFPBase    :: Int-  , useFPFormat  :: PPFloatFormat-  } -asciiMode :: PPOpts -> Integer -> Bool-asciiMode opts width = useAscii opts && (width == 7 || width == 8)+-- | The type of dynamic call stacks for the interpreter.+--   New frames are pushed onto the right side of the sequence.+type CallStack = Seq (Name, Range) -data PPFloatFormat =-    FloatFixed Int PPFloatExp -- ^ Use this many significant digis-  | FloatFrac Int             -- ^ Show this many digits after floating point-  | FloatFree PPFloatExp      -- ^ Use the correct number of digits+-- | Pretty print a call stack with each call frame on a separate+--   line, with most recent call frames at the top.+displayCallStack :: CallStack -> Doc+displayCallStack = vcat . map f . toList . Seq.reverse+  where+  f (nm,rng)+    | rng == emptyRange = pp nm+    | otherwise = pp nm <+> text "called at" <+> pp rng -data PPFloatExp = ForceExponent -- ^ Always show an exponent-                | AutoExponent  -- ^ Only show exponent when needed +-- | Combine the call stack of a function value with the call+--   stack of the current calling context.  This algorithm is+--   the same one GHC uses to compute profiling calling contexts.+--+--   The algorithm is as follows.+--+--        ccs ++> ccsfn  =  ccs ++ dropCommonPrefix ccs ccsfn+--+--      where+--+--        dropCommonPrefix A B+--           -- returns the suffix of B after removing any prefix common+--           -- to both A and B.+combineCallStacks ::+  CallStack {- ^ call stack of the application context -} ->+  CallStack {- ^ call stack of the function being applied -} ->+  CallStack+combineCallStacks appstk fnstk = appstk <> dropCommonPrefix appstk fnstk+  where+  dropCommonPrefix _  Seq.Empty = Seq.Empty+  dropCommonPrefix Seq.Empty fs = fs+  dropCommonPrefix (a Seq.:<| as) xs@(f Seq.:<| fs)+    | a == f    = dropCommonPrefix as fs+    | otherwise = xs -defaultPPOpts :: PPOpts-defaultPPOpts = PPOpts { useAscii = False, useBase = 10, useInfLength = 5-                       , useFPBase = 16-                       , useFPFormat = FloatFree AutoExponent-                       }+-- | Add a call frame to the top of a call stack+pushCallFrame :: Name -> Range -> CallStack -> CallStack+pushCallFrame nm rng stk@( _ Seq.:|> (nm',rng'))+  | nm == nm', rng == rng' = stk+pushCallFrame nm rng stk = stk Seq.:|> (nm,rng)  --- | Some options for evalutaion-data EvalOpts = EvalOpts-  { evalLogger :: Logger    -- ^ Where to print stuff (e.g., for @trace@)-  , evalPPOpts :: PPOpts    -- ^ How to pretty print things.-  }- -- | The monad for Cryptol evaluation. --   A computation is either "ready", which means it represents --   only trivial computation, or is an "eval" action which must@@ -97,7 +114,7 @@ --   represents a delayed, shared computation. data Eval a    = Ready !a-   | Eval !(IO a)+   | Eval !(CallStack -> IO a)    | Thunk !(TVar (ThunkState a))  -- | This datastructure tracks the lifecycle of a thunk.@@ -107,7 +124,7 @@ --   cryptol expression that is bound to a name, and is not --   already obviously a value (and in a few other places as --   well) will get turned into a thunk in order to avoid---   recomputations.  These thunks will start in the `Unforced`+--   recomputation.  These thunks will start in the `Unforced` --   state, and have a backup computation that just raises --   the `LoopError` exception. --@@ -129,16 +146,20 @@ data ThunkState a   = Void !String        -- ^ This thunk has not yet been initialized-  | Unforced !(IO a) !(IO a)+  | Unforced !(IO a) !(Maybe (IO a)) !String !CallStack        -- ^ This thunk has not yet been forced.  We keep track of the "main"-       --   computation to run and a "backup" computation to run if we+       --   computation to run and an optional "backup" computation to run if we        --   detect a tight loop when evaluating the first one.-  | UnderEvaluation !ThreadId !(IO a)+       --   The final two arguments are used to throw a loop exception+       --   if the backup computation also causes a tight loop.+  | UnderEvaluation !ThreadId !(Maybe (IO a)) !String !CallStack        -- ^ This thunk is currently being evaluated by the thread with the given-       --   thread ID.  We track the "backup" computation to run if we detect+       --   thread ID.  We track an optional "backup" computation to run if we detect        --   a tight loop evaluating this thunk.  If the thunk is being evaluated        --   by some other thread, the current thread will await its completion.-  | ForcedErr !EvalError+       --   The final two arguments are used to throw a loop exception+       --   if the backup computation also causes a tight loop.+  | ForcedErr !EvalErrorEx        -- ^ This thunk has been forced, and its evaluation results in an exception   | Forced !a        -- ^ This thunk has been forced to the given value@@ -148,7 +169,7 @@ --   it requires no computation to return. maybeReady :: Eval a -> Eval (Maybe a) maybeReady (Ready a) = pure (Just a)-maybeReady (Thunk tv) = Eval $+maybeReady (Thunk tv) = Eval $ \_ ->   readTVarIO tv >>= \case      Forced a -> pure (Just a)      _ -> pure Nothing@@ -163,11 +184,13 @@ --   its own evaluation. delayFill ::   Eval a {- ^ Computation to delay -} ->-  Eval a {- ^ Backup computation to run if a tight loop is detected -} ->+  Maybe (Eval a) {- ^ Optional backup computation to run if a tight loop is detected -} ->+  String {- ^ message for the <<loop>> exception if a tight loop is detected -} ->   Eval (Eval a)-delayFill e@(Ready _) _  = return e-delayFill e@(Thunk _) _  = return e-delayFill (Eval x) backup = Eval (Thunk <$> newTVarIO (Unforced x (runEval backup)))+delayFill e@(Ready _) _ _ = return e+delayFill e@(Thunk _) _ _ = return e+delayFill (Eval x) backup msg =+  Eval (\stk -> Thunk <$> newTVarIO (Unforced (x stk) (runEval stk <$> backup) msg stk))  -- | Begin executing the given operation in a separate thread, --   returning a thunk which will await the completion of@@ -183,24 +206,24 @@ -- been forced.  If so, return the result.  Otherwise, -- fork a thread to force this computation and return -- the thunk.-evalSpark (Thunk tv)  = Eval $+evalSpark (Thunk tv)  = Eval $ \_stk ->   readTVarIO tv >>= \case     Forced x     -> return (Ready x)-    ForcedErr ex -> return (Eval (X.throwIO ex))+    ForcedErr ex -> return (Eval $ \_ -> (X.throwIO ex))     _ ->        do _ <- forkIO (sparkThunk tv)           return (Thunk tv)  -- If the computation is nontrivial but not already a thunk, -- create a thunk and fork a thread to force it.-evalSpark (Eval x) = Eval $-  do tv <- newTVarIO (Unforced x (X.throwIO (LoopError "")))+evalSpark (Eval x) = Eval $ \stk ->+  do tv <- newTVarIO (Unforced (x stk) Nothing "" stk)      _ <- forkIO (sparkThunk tv)      return (Thunk tv)   -- | To the work of forcing a thunk. This is the worker computation---   that is foked off via @evalSpark@.+--   that is forked off via @evalSpark@. sparkThunk :: TVar (ThunkState a) -> IO () sparkThunk tv =   do tid <- myThreadId@@ -212,13 +235,13 @@               do st <- readTVar tv                  case st of                    Void _ -> retry-                   Unforced _ backup -> writeTVar tv (UnderEvaluation tid backup)+                   Unforced _ backup msg stk -> writeTVar tv (UnderEvaluation tid backup msg stk)                    _ -> return ()                  return st      -- If we successfully claimed the thunk to work on, run the computation and      -- update the thunk state with the result.      case st of-       Unforced work _ ->+       Unforced work _ _ _ ->          X.try work >>= \case            Left err -> atomically (writeTVar tv (ForcedErr err))            Right a  -> atomically (writeTVar tv (Forced a))@@ -232,10 +255,10 @@ blackhole ::   String {- ^ A name to associate with this thunk. -} ->   Eval (Eval a, Eval a -> Eval ())-blackhole msg = Eval $+blackhole msg = Eval $ \stk ->   do tv <- newTVarIO (Void msg)      let set (Ready x)  = io $ atomically (writeTVar tv (Forced x))-         set m          = io $ atomically (writeTVar tv (Unforced (runEval m) (X.throwIO (LoopError msg))))+         set m          = io $ atomically (writeTVar tv (Unforced (runEval stk m) Nothing msg stk))      return (Thunk tv, set)  -- | Force a thunk to get the result.@@ -254,16 +277,19 @@                   case res of                     -- In this case, we claim the thunk.  Update the state to indicate                     -- that we are working on it.-                    Unforced _ backup -> writeTVar tv (UnderEvaluation tid backup)+                    Unforced _ backup msg stk -> writeTVar tv (UnderEvaluation tid backup msg stk)                      -- In this case, the thunk is already being evaluated.  If it is                     -- under evaluation by this thread, we have to run the backup computation,                     -- and "consume" it by updating the backup computation to one that throws                     -- a loop error.  If some other thread is evaluating, reset the                     -- transaction to await completion of the thunk.-                    UnderEvaluation t _-                      | tid == t  -> writeTVar tv (UnderEvaluation tid (X.throwIO (LoopError "")))-                      | otherwise -> retry -- wait, if some other thread is evaualting+                    UnderEvaluation t backup msg stk+                      | tid == t  ->+                          case backup of+                            Just _  -> writeTVar tv (UnderEvaluation tid Nothing msg stk)+                            Nothing -> writeTVar tv (ForcedErr (EvalErrorEx stk (LoopError msg)))+                      | otherwise -> retry -- wait, if some other thread is evaluating                     _ -> return ()                    -- Return the original thunk state so we can decide what work to do@@ -283,25 +309,43 @@            Void msg -> evalPanic "unDelay" ["Thunk forced before it was initialized", msg]            Forced x -> pure x            ForcedErr e -> X.throwIO e-           UnderEvaluation _ backup -> doWork backup -- this thread was already evaluating this thunk-           Unforced work _ -> doWork work+           -- this thread was already evaluating this thunk+           UnderEvaluation _ (Just backup) _ _ -> doWork backup+           UnderEvaluation _ Nothing msg stk -> X.throwIO (EvalErrorEx stk (LoopError msg))+           Unforced work _ _ _ -> doWork work +-- | Get the current call stack+getCallStack :: Eval CallStack+getCallStack = Eval (\stk -> pure stk)++-- | Execute the action with the given call stack+withCallStack :: CallStack -> Eval a -> Eval a+withCallStack stk m = Eval (\_ -> runEval stk m)++-- | Run the given action with a modify call stack+modifyCallStack :: (CallStack -> CallStack) -> Eval a -> Eval a+modifyCallStack f m =+  Eval $ \stk ->+    do let stk' = f stk+       -- putStrLn $ unwords ["Pushing call stack", show (displayCallStack stk')]+       runEval stk' m+ -- | Execute the given evaluation action.-runEval :: Eval a -> IO a-runEval (Ready a)  = return a-runEval (Eval x)   = x-runEval (Thunk tv) = unDelay tv+runEval :: CallStack -> Eval a -> IO a+runEval _   (Ready a)  = return a+runEval stk (Eval x)   = x stk+runEval _   (Thunk tv) = unDelay tv  {-# INLINE evalBind #-} evalBind :: Eval a -> (a -> Eval b) -> Eval b evalBind (Ready a) f  = f a-evalBind (Eval x) f   = Eval (x >>= runEval . f)-evalBind (Thunk x) f  = Eval (unDelay x >>= runEval . f)+evalBind (Eval x)  f  = Eval (\stk -> x stk >>= runEval stk . f)+evalBind (Thunk x) f  = Eval (\stk -> unDelay x >>= runEval stk . f)  instance Functor Eval where   fmap f (Ready x)   = Ready (f x)-  fmap f (Eval m)    = Eval (f <$> m)-  fmap f (Thunk tv)  = Eval (f <$> unDelay tv)+  fmap f (Eval m)    = Eval (\stk -> f <$> m stk)+  fmap f (Thunk tv)  = Eval (\_   -> f <$> unDelay tv)   {-# INLINE fmap #-}  instance Applicative Eval where@@ -316,18 +360,12 @@   {-# INLINE return #-}   {-# INLINE (>>=) #-} -instance Fail.MonadFail Eval where-  fail x = Eval (fail x)- instance MonadIO Eval where   liftIO = io -instance MonadFix Eval where-  mfix f = Eval $ mfix (\x -> runEval (f x))- -- | Lift an 'IO' computation into the 'Eval' monad. io :: IO a -> Eval a-io m = Eval m+io m = Eval (\_stk -> m) {-# INLINE io #-}  @@ -341,37 +379,53 @@ -- | Data type describing errors that can occur during evaluation. data EvalError   = InvalidIndex (Maybe Integer)  -- ^ Out-of-bounds index-  | TypeCannotBeDemoted Type      -- ^ Non-numeric type passed to @number@ function   | DivideByZero                  -- ^ Division or modulus by 0   | NegativeExponent              -- ^ Exponentiation by negative integer   | LogNegative                   -- ^ Logarithm of a negative integer-  | WordTooWide Integer           -- ^ Bitvector too large   | UserError String              -- ^ Call to the Cryptol @error@ primitive   | LoopError String              -- ^ Detectable nontermination   | NoPrim Name                   -- ^ Primitive with no implementation   | BadRoundingMode Integer       -- ^ Invalid rounding mode   | BadValue String               -- ^ Value outside the domain of a partial function.-    deriving (Typeable,Show)+    deriving Typeable  instance PP EvalError where   ppPrec _ e = case e of     InvalidIndex (Just i) -> text "invalid sequence index:" <+> integer i     InvalidIndex Nothing  -> text "invalid sequence index"-    TypeCannotBeDemoted t -> text "type cannot be demoted:" <+> pp t     DivideByZero -> text "division by 0"     NegativeExponent -> text "negative exponent"     LogNegative -> text "logarithm of negative"-    WordTooWide w ->-      text "word too wide for memory:" <+> integer w <+> text "bits"     UserError x -> text "Run-time error:" <+> text x-    LoopError x -> text "<<loop>>" <+> text x+    LoopError x -> vcat [ text "<<loop>>" <+> text x+                        , text "This usually occurs due to an improper recursive definition,"+                        , text "but may also result from retrying a previously interrupted"+                        , text "computation (e.g., after CTRL^C). In that case, you may need to"+                        , text "`:reload` the current module to reset to a good state."+                        ]     BadRoundingMode r -> "invalid rounding mode" <+> integer r     BadValue x -> "invalid input for" <+> backticks (text x)     NoPrim x -> text "unimplemented primitive:" <+> pp x -instance X.Exception EvalError+instance Show EvalError where+  show = show . pp +data EvalErrorEx =+  EvalErrorEx CallStack EvalError+ deriving Typeable +instance PP EvalErrorEx where+  ppPrec _ (EvalErrorEx stk ex) = vcat ([ pp ex ] ++ callStk)++   where+    callStk | Seq.null stk = []+            | otherwise = [ text "-- Backtrace --", displayCallStack stk ]++instance Show EvalErrorEx where+  show = show . pp++instance X.Exception EvalErrorEx+ data Unsupported   = UnsupportedSymbolicOp String  -- ^ Operation cannot be supported in the symbolic simulator     deriving (Typeable,Show)@@ -382,13 +436,20 @@  instance X.Exception Unsupported ---- | For things like @`(inf)@ or @`(0-1)@.-typeCannotBeDemoted :: Type -> a-typeCannotBeDemoted t = X.throw (TypeCannotBeDemoted t)- -- | For when we know that a word is too wide and will exceed gmp's -- limits (though words approaching this size will probably cause the -- system to crash anyway due to lack of memory). wordTooWide :: Integer -> a wordTooWide w = X.throw (WordTooWide w)++data WordTooWide = WordTooWide Integer -- ^ Bitvector too large+ deriving Typeable++instance PP WordTooWide where+  ppPrec _ (WordTooWide w) =+      text "word too wide for memory:" <+> integer w <+> text "bits"++instance Show WordTooWide where+  show = show . pp++instance X.Exception WordTooWide

@@ -6,6 +6,7 @@ -- Stability   :  provisional -- Portability :  portable +{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}@@ -43,14 +44,14 @@ import qualified Data.SBV.Internals as SBV  import Cryptol.Backend-import Cryptol.Backend.Concrete ( integerToChar, ppBV, BV(..) )+import Cryptol.Backend.Concrete ( integerToChar ) import Cryptol.Backend.Monad   ( Eval(..), blackhole, delayFill, evalSpark-  , EvalError(..), Unsupported(..)+  , EvalError(..), EvalErrorEx(..), Unsupported(..)+  , modifyCallStack, getCallStack   )  import Cryptol.Utils.Panic (panic)-import Cryptol.Utils.PP  data SBV =   SBV@@ -73,23 +74,30 @@ literalSWord :: Int -> Integer -> SWord SBV literalSWord w i = svInteger (KBounded False w) i +svMkSymVar_ :: Maybe Quantifier -> Kind -> Maybe String -> SBV.State -> IO SVal+#if MIN_VERSION_sbv(8,8,0)+svMkSymVar_ = svMkSymVar . SBV.NonQueryVar+#else+svMkSymVar_ = svMkSymVar+#endif+ freshBV_ :: SBV -> Int -> IO (SWord SBV) freshBV_ (SBV stateVar _) w =-  withMVar stateVar (svMkSymVar Nothing (KBounded False w) Nothing)+  withMVar stateVar (svMkSymVar_ Nothing (KBounded False w) Nothing)  freshSBool_ :: SBV -> IO (SBit SBV) freshSBool_ (SBV stateVar _) =-  withMVar stateVar (svMkSymVar Nothing KBool Nothing)+  withMVar stateVar (svMkSymVar_ Nothing KBool Nothing)  freshSInteger_ :: SBV -> IO (SInteger SBV) freshSInteger_ (SBV stateVar _) =-  withMVar stateVar (svMkSymVar Nothing KUnbounded Nothing)+  withMVar stateVar (svMkSymVar_ Nothing KUnbounded Nothing)   -- SBV Evaluation monad -------------------------------------------------------  data SBVResult a-  = SBVError !EvalError+  = SBVError !EvalErrorEx   | SBVResult !SVal !a -- safety predicate and result  instance Functor SBVResult where@@ -146,17 +154,19 @@   type SFloat SBV = ()        -- XXX: not implemented   type SEval SBV = SBVEval -  raiseError _ err = SBVEval (pure (SBVError err))+  raiseError _ err = SBVEval $+    do stk <- getCallStack+       pure (SBVError (EvalErrorEx stk err)) -  assertSideCondition _ cond err-    | Just False <- svAsBool cond = SBVEval (pure (SBVError err))+  assertSideCondition sym cond err+    | Just False <- svAsBool cond = raiseError sym err     | otherwise = SBVEval (pure (SBVResult cond ()))    isReady _ (SBVEval (Ready _)) = True   isReady _ _ = False -  sDelayFill _ m retry = SBVEval $-    do m' <- delayFill (sbvEval m) (sbvEval retry)+  sDelayFill _ m retry msg = SBVEval $+    do m' <- delayFill (sbvEval m) (sbvEval <$> retry) msg        pure (pure (SBVEval m'))    sSpark _ m = SBVEval $@@ -167,6 +177,11 @@     do (hole, fill) <- blackhole msg        pure (pure (SBVEval hole, \m -> SBVEval (fmap pure $ fill (sbvEval m)))) +  sModifyCallStack _ f (SBVEval m) = SBVEval $+    modifyCallStack f m++  sGetCallStack _ = SBVEval (pure <$> getCallStack)+   mergeEval _sym f c mx my = SBVEval $     do rx <- sbvEval mx        ry <- sbvEval my@@ -187,16 +202,6 @@   wordLen _ v = toInteger (intSizeOf v)   wordAsChar _ v = integerToChar <$> svAsInteger v -  ppBit _ v-     | Just b <- svAsBool v = text $! if b then "True" else "False"-     | otherwise            = text "?"-  ppWord sym opts v-     | Just x <- svAsInteger v = ppBV opts (BV (wordLen sym v) x)-     | otherwise               = text "[?]"-  ppInteger _ _opts v-     | Just x <- svAsInteger v = integer x-     | otherwise               = text "[?]"-   iteBit _ b x y = pure $! svSymbolicMerge KBool True b x y   iteWord _ b x y = pure $! svSymbolicMerge (kindOf x) True b x y   iteInteger _ b x y = pure $! svSymbolicMerge KUnbounded True b x y@@ -319,20 +324,37 @@   znNegate sym m a  = sModNegate sym m a   znRecip = sModRecip -  ppFloat _ _ _           = text "[?]"-  fpExactLit _ _          = unsupported "fpExactLit"-  fpLit _ _ _ _           = unsupported "fpLit"-  fpLogicalEq _ _ _       = unsupported "fpLogicalEq"-  fpEq _ _ _              = unsupported "fpEq"-  fpLessThan _ _ _        = unsupported "fpLessThan"-  fpGreaterThan _ _ _     = unsupported "fpGreaterThan"-  fpPlus _ _ _ _          = unsupported "fpPlus"-  fpMinus _ _ _ _         = unsupported "fpMinus"-  fpMult _  _ _ _         = unsupported "fpMult"-  fpDiv _ _ _ _           = unsupported "fpDiv"-  fpNeg _ _               = unsupported "fpNeg"-  fpFromInteger _ _ _ _ _ = unsupported "fpFromInteger"-  fpToInteger _ _ _ _     = unsupported "fpToInteger"+  fpAsLit _ _               = Nothing+  iteFloat _ _ _ _          = unsupported "iteFloat"+  fpNaN _ _ _               = unsupported "fpNaN"+  fpPosInf _ _ _            = unsupported "fpPosInf"+  fpExactLit _ _            = unsupported "fpExactLit"+  fpLit _ _ _ _             = unsupported "fpLit"+  fpLogicalEq _ _ _         = unsupported "fpLogicalEq"+  fpEq _ _ _                = unsupported "fpEq"+  fpLessThan _ _ _          = unsupported "fpLessThan"+  fpGreaterThan _ _ _       = unsupported "fpGreaterThan"+  fpPlus _ _ _ _            = unsupported "fpPlus"+  fpMinus _ _ _ _           = unsupported "fpMinus"+  fpMult _ _ _ _            = unsupported "fpMult"+  fpDiv _ _ _ _             = unsupported "fpDiv"+  fpAbs _ _                 = unsupported "fpAbs"+  fpSqrt _ _ _              = unsupported "fpSqrt"+  fpFMA _ _ _ _ _           = unsupported "fpFMA"+  fpNeg _ _                 = unsupported "fpNeg"+  fpFromInteger _ _ _ _ _   = unsupported "fpFromInteger"+  fpToInteger _ _ _ _       = unsupported "fpToInteger"+  fpIsZero _ _              = unsupported "fpIsZero"+  fpIsInf _ _               = unsupported "fpIsInf"+  fpIsNeg _ _               = unsupported "fpIsNeg"+  fpIsNaN _ _               = unsupported "fpIsNaN"+  fpIsNorm _ _              = unsupported "fpIsNorm"+  fpIsSubnorm _ _           = unsupported "fpIsSubnorm"+  fpToBits _ _              = unsupported "fpToBits"+  fpFromBits _ _ _ _        = unsupported "fpFromBits"+  fpToRational _ _          = unsupported "fpToRational"+  fpFromRational _ _ _ _ _  = unsupported "fpFromRational"+  unsupported :: String -> SEval SBV a unsupported x = liftIO (X.throw (UnsupportedSymbolicOp x))

@@ -32,18 +32,16 @@  import qualified What4.Interface as W4 import qualified What4.SWord as SW--import qualified Cryptol.Backend.What4.SFloat as FP+import qualified What4.SFloat as FP  import Cryptol.Backend-import Cryptol.Backend.Concrete( BV(..), ppBV ) import Cryptol.Backend.FloatHelpers import Cryptol.Backend.Monad-   ( Eval(..), EvalError(..), Unsupported(..)-   , delayFill, blackhole, evalSpark+   ( Eval(..), EvalError(..), EvalErrorEx(..)+   , Unsupported(..), delayFill, blackhole, evalSpark+   , modifyCallStack, getCallStack    ) import Cryptol.Utils.Panic-import Cryptol.Utils.PP   data What4 sym =@@ -72,7 +70,7 @@  -- | The symbolic value we computed. data W4Result sym a-  = W4Error !EvalError+  = W4Error !EvalErrorEx     -- ^ A malformed value    | W4Result !(W4.Pred sym) !a@@ -186,7 +184,9 @@  -- | A fully undefined symbolic value evalError :: W4.IsSymExprBuilder sym => EvalError -> W4Eval sym a-evalError err = W4Eval (pure (W4Error err))+evalError err = W4Eval $ W4Conn $ \_sym ->+  do stk <- getCallStack+     pure (W4Error (EvalErrorEx stk err))  -------------------------------------------------------------------------------- @@ -220,17 +220,21 @@       Ready _ -> True       _ -> False -  sDelayFill _ m retry =+  sDelayFill _ m retry msg =     total     do sym <- getSym-       doEval (w4Thunk <$> delayFill (w4Eval m sym) (w4Eval retry sym))+       doEval (w4Thunk <$> delayFill (w4Eval m sym) (w4Eval <$> retry <*> pure sym) msg)    sSpark _ m =     total     do sym   <- getSym        doEval (w4Thunk <$> evalSpark (w4Eval m sym)) +  sModifyCallStack _ f (W4Eval (W4Conn m)) =+    W4Eval (W4Conn \sym -> modifyCallStack f (m sym)) +  sGetCallStack _ = total (doEval getCallStack)+   sDeclareHole _ msg =     total     do (hole, fill) <- doEval (blackhole msg)@@ -288,25 +292,10 @@    integerAsLit _ v = W4.asInteger v -  ppBit _ v-    | Just b <- W4.asConstantPred v = text $! if b then "True" else "False"-    | otherwise                     = text "?"--  ppWord _ opts v-    | Just x <- SW.bvAsUnsignedInteger v-    = ppBV opts (BV (SW.bvWidth v) x)--    | otherwise = text "[?]"--  ppInteger _ _opts v-    | Just x <- W4.asInteger v = integer x-    | otherwise = text "[?]"--  ppFloat _ _opts _ = text "[?]"-   iteBit sym c x y = liftIO (W4.itePred (w4 sym) c x y)   iteWord sym c x y = liftIO (SW.bvIte (w4 sym) c x y)   iteInteger sym c x y = liftIO (W4.intIte (w4 sym) c x y)+  iteFloat sym p x y = liftIO (FP.fpIte (w4 sym) p x y)    bitEq  sym x y = liftIO (W4.eqPred (w4 sym) x y)   bitAnd sym x y = liftIO (W4.andPred (w4 sym) x y)@@ -443,10 +432,18 @@   --------------------------------------------------------------    fpLit sym e p r = liftIO $ FP.fpFromRationalLit (w4 sym) e p r+  fpAsLit _ f = BF e p <$> FP.fpAsLit f+    where (e,p) = FP.fpSize f    fpExactLit sym BF{ bfExpWidth = e, bfPrecWidth = p, bfValue = bf } =     liftIO (FP.fpFromBinary (w4 sym) e p =<< SW.bvLit (w4 sym) (e+p) (floatToBits e p bf)) +  fpNaN sym e p = liftIO (FP.fpNaN (w4 sym) e p)+  fpPosInf sym e p = liftIO (FP.fpPosInf (w4 sym) e p)++  fpToBits sym f = liftIO (FP.fpToBinary (w4 sym) f)+  fpFromBits sym e p w = liftIO (FP.fpFromBinary (w4 sym) e p w)+   fpEq          sym x y = liftIO $ FP.fpEqIEEE (w4 sym) x y   fpLessThan    sym x y = liftIO $ FP.fpLtIEEE (w4 sym) x y   fpGreaterThan sym x y = liftIO $ FP.fpGtIEEE (w4 sym) x y@@ -458,12 +455,30 @@   fpDiv   = fpBinArith FP.fpDiv    fpNeg sym x = liftIO $ FP.fpNeg (w4 sym) x+  fpAbs sym x = liftIO $ FP.fpAbs (w4 sym) x+  fpSqrt sym r x =+    do rm <- fpRoundingMode sym r+       liftIO $ FP.fpSqrt (w4 sym) rm x +  fpFMA sym r x y z =+    do rm <- fpRoundingMode sym r+       liftIO $ FP.fpFMA (w4 sym) rm x y z++  fpIsZero sym x = liftIO $ FP.fpIsZero (w4 sym) x+  fpIsNeg sym x = liftIO $ FP.fpIsNeg (w4 sym) x+  fpIsNaN sym x = liftIO $ FP.fpIsNaN (w4 sym) x+  fpIsInf sym x = liftIO $ FP.fpIsInf (w4 sym) x+  fpIsNorm sym x = liftIO $ FP.fpIsNorm (w4 sym) x+  fpIsSubnorm sym x = liftIO $ FP.fpIsSubnorm (w4 sym) x+   fpFromInteger sym e p r x =     do rm <- fpRoundingMode sym r        liftIO $ FP.fpFromInteger (w4 sym) e p rm x    fpToInteger = fpCvtToInteger++  fpFromRational = fpCvtFromRational+  fpToRational = fpCvtToRational  sModAdd :: W4.IsSymExprBuilder sym =>   sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)

@@ -1,362 +0,0 @@-{-# Language DataKinds #-}-{-# Language FlexibleContexts #-}-{-# Language GADTs #-}-{-# Language RankNTypes #-}-{-# Language TypeApplications #-}-{-# Language TypeOperators #-}--- | Working with floats of dynamic sizes.--- This should probably be moved to What4 one day.-module Cryptol.Backend.What4.SFloat-  ( -- * Interface-    SFloat(..)-  , fpReprOf-  , fpSize-  , fpRepr--    -- * Constants-  , fpFresh-  , fpNaN-  , fpPosInf-  , fpFromRationalLit--    -- * Interchange formats-  , fpFromBinary-  , fpToBinary--    -- * Relations-  , SFloatRel-  , fpEq-  , fpEqIEEE-  , fpLtIEEE-  , fpGtIEEE--    -- * Arithmetic-  , SFloatBinArith-  , fpNeg-  , fpAdd-  , fpSub-  , fpMul-  , fpDiv--    -- * Conversions-  , fpRound-  , fpToReal-  , fpFromReal-  , fpFromRational-  , fpToRational-  , fpFromInteger--    -- * Queries-  , fpIsInf, fpIsNaN--  -- * Exceptions-  , UnsupportedFloat(..)-  , FPTypeError(..)-  ) where--import Control.Exception--import Data.Parameterized.Some-import Data.Parameterized.NatRepr--import What4.BaseTypes-import What4.Panic(panic)-import What4.SWord-import What4.Interface---- | Symbolic floating point numbers.-data SFloat sym where-  SFloat :: IsExpr (SymExpr sym) => SymFloat sym fpp -> SFloat sym---------------------------------------------------------------------------------------- | This exception is thrown if the operations try to create a--- floating point value we do not support-data UnsupportedFloat =-  UnsupportedFloat { fpWho :: String, exponentBits, precisionBits :: Integer }-  deriving Show----- | Throw 'UnsupportedFloat' exception-unsupported ::-  String  {- ^ Label -} ->-  Integer {- ^ Exponent width -} ->-  Integer {- ^ Precision width -} ->-  IO a-unsupported l e p =-  throwIO UnsupportedFloat { fpWho         = l-                           , exponentBits  = e-                           , precisionBits = p }--instance Exception UnsupportedFloat---- | This exceptoin is throws if the types don't match.-data FPTypeError =-  FPTypeError { fpExpected :: Some BaseTypeRepr-              , fpActual   :: Some BaseTypeRepr-              }-    deriving Show--instance Exception FPTypeError--fpTypeMismatch :: BaseTypeRepr t1 -> BaseTypeRepr t2 -> IO a-fpTypeMismatch expect actual =-  throwIO FPTypeError { fpExpected = Some expect-                      , fpActual   = Some actual-                      }-fpTypeError :: FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a-fpTypeError t1 t2 =-  fpTypeMismatch (BaseFloatRepr t1) (BaseFloatRepr t2)-------------------------------------------------------------------------------------- | Construct the 'FloatPrecisionRepr' with the given parameters.-fpRepr ::-  Integer {- ^ Exponent width -} ->-  Integer {- ^ Precision width -} ->-  Maybe (Some FloatPrecisionRepr)-fpRepr iE iP =-  do Some e    <- someNat iE-     LeqProof  <- testLeq (knownNat @2) e-     Some p    <- someNat iP-     LeqProof  <- testLeq (knownNat @2) p-     pure (Some (FloatingPointPrecisionRepr e p))--fpReprOf ::-  IsExpr (SymExpr sym) => sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp-fpReprOf _ e =-  case exprType e of-    BaseFloatRepr r -> r--fpSize :: SFloat sym -> (Integer,Integer)-fpSize (SFloat f) =-  case exprType f of-    BaseFloatRepr (FloatingPointPrecisionRepr e p) -> (intValue e, intValue p)-------------------------------------------------------------------------------------- Constants---- | A fresh variable of the given type.-fpFresh ::-  IsSymExprBuilder sym =>-  sym ->-  Integer ->-  Integer ->-  IO (SFloat sym)-fpFresh sym e p-  | Just (Some fpp) <- fpRepr e p =-    SFloat <$> freshConstant sym emptySymbol (BaseFloatRepr fpp)-  | otherwise = unsupported "fpFresh" e p---- | Not a number-fpNaN ::-  IsExprBuilder sym =>-  sym ->-  Integer {- ^ Exponent width -} ->-  Integer {- ^ Precision width -} ->-  IO (SFloat sym)-fpNaN sym e p-  | Just (Some fpp) <- fpRepr e p = SFloat <$> floatNaN sym fpp-  | otherwise = unsupported "fpNaN" e p----- | Positive infinity-fpPosInf ::-  IsExprBuilder sym =>-  sym ->-  Integer {- ^ Exponent width -} ->-  Integer {- ^ Precision width -} ->-  IO (SFloat sym)-fpPosInf sym e p-  | Just (Some fpp) <- fpRepr e p = SFloat <$> floatPInf sym fpp-  | otherwise = unsupported "fpPosInf" e p---- | A floating point number corresponding to the given rations.-fpFromRationalLit ::-  IsExprBuilder sym =>-  sym ->-  Integer {- ^ Exponent width -} ->-  Integer {- ^ Precision width -} ->-  Rational ->-  IO (SFloat sym)-fpFromRationalLit sym e p r-  | Just (Some fpp) <- fpRepr e p = SFloat <$> floatLit sym fpp r-  | otherwise = unsupported "fpFromRational" e p----- | Make a floating point number with the given bit representation.-fpFromBinary ::-  IsExprBuilder sym =>-  sym ->-  Integer {- ^ Exponent width -} ->-  Integer {- ^ Precision width -} ->-  SWord sym ->-  IO (SFloat sym)-fpFromBinary sym e p swe-  | DBV sw <- swe-  , Just (Some fpp) <- fpRepr e p-  , FloatingPointPrecisionRepr ew pw <- fpp-  , let expectW = addNat ew pw-  , actual@(BaseBVRepr actualW)  <- exprType sw =-    case testEquality expectW actualW of-      Just Refl -> SFloat <$> floatFromBinary sym fpp sw-      Nothing -- we want to report type correct type errors! :-)-        | Just LeqProof <- testLeq (knownNat @1) expectW ->-                fpTypeMismatch (BaseBVRepr expectW) actual-        | otherwise -> panic "fpFromBits" [ "1 >= 2" ]-  | otherwise = unsupported "fpFromBits" e p--fpToBinary :: IsExprBuilder sym => sym -> SFloat sym -> IO (SWord sym)-fpToBinary sym (SFloat f)-  | FloatingPointPrecisionRepr e p <- fpReprOf sym f-  , Just LeqProof <- testLeq (knownNat @1) (addNat e p)-    = DBV <$> floatToBinary sym f-  | otherwise = panic "fpToBinary" [ "we messed up the types" ]-------------------------------------------------------------------------------------- Arithmetic--fpNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym)-fpNeg sym (SFloat fl) = SFloat <$> floatNeg sym fl--fpBinArith ::-  IsExprBuilder sym =>-  (forall t.-      sym ->-      RoundingMode ->-      SymFloat sym t ->-      SymFloat sym t ->-      IO (SymFloat sym t)-  ) ->-  sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym)-fpBinArith fun sym r (SFloat x) (SFloat y) =-  let t1 = sym `fpReprOf` x-      t2 = sym `fpReprOf` y-  in-  case testEquality t1 t2 of-    Just Refl -> SFloat <$> fun sym r x y-    _         -> fpTypeError t1 t2--type SFloatBinArith sym =-  sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym)--fpAdd :: IsExprBuilder sym => SFloatBinArith sym-fpAdd = fpBinArith floatAdd--fpSub :: IsExprBuilder sym => SFloatBinArith sym-fpSub = fpBinArith floatSub--fpMul :: IsExprBuilder sym => SFloatBinArith sym-fpMul = fpBinArith floatMul--fpDiv :: IsExprBuilder sym => SFloatBinArith sym-fpDiv = fpBinArith floatDiv---------------------------------------------------------------------------------------fpRel ::-  IsExprBuilder sym =>-  (forall t.-    sym ->-    SymFloat sym t ->-    SymFloat sym t ->-    IO (Pred sym)-  ) ->-  sym -> SFloat sym -> SFloat sym -> IO (Pred sym)-fpRel fun sym (SFloat x) (SFloat y) =-  let t1 = sym `fpReprOf` x-      t2 = sym `fpReprOf` y-  in-  case testEquality t1 t2 of-    Just Refl -> fun sym x y-    _         -> fpTypeError t1 t2-----type SFloatRel sym =-  sym -> SFloat sym -> SFloat sym -> IO (Pred sym)--fpEq :: IsExprBuilder sym => SFloatRel sym-fpEq = fpRel floatEq--fpEqIEEE :: IsExprBuilder sym => SFloatRel sym-fpEqIEEE = fpRel floatFpEq--fpLtIEEE :: IsExprBuilder sym => SFloatRel sym-fpLtIEEE = fpRel floatLt--fpGtIEEE :: IsExprBuilder sym => SFloatRel sym-fpGtIEEE = fpRel floatGt------------------------------------------------------------------------------------fpRound ::-  IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)-fpRound sym r (SFloat x) = SFloat <$> floatRound sym r x---- | This is undefined on "special" values (NaN,infinity)-fpToReal :: IsExprBuilder sym => sym -> SFloat sym -> IO (SymReal sym)-fpToReal sym (SFloat x) = floatToReal sym x--fpFromReal ::-  IsExprBuilder sym =>-  sym -> Integer -> Integer -> RoundingMode -> SymReal sym -> IO (SFloat sym)-fpFromReal sym e p r x-  | Just (Some repr) <- fpRepr e p = SFloat <$> realToFloat sym repr r x-  | otherwise = unsupported "fpFromReal" e p---fpFromInteger ::-  IsExprBuilder sym =>-  sym -> Integer -> Integer -> RoundingMode -> SymInteger sym -> IO (SFloat sym)-fpFromInteger sym e p r x = fpFromReal sym e p r =<< integerToReal sym x---fpFromRational ::-  IsExprBuilder sym =>-  sym -> Integer -> Integer -> RoundingMode ->-  SymInteger sym -> SymInteger sym -> IO (SFloat sym)-fpFromRational sym e p r x y =-  do num <- integerToReal sym x-     den <- integerToReal sym y-     res <- realDiv sym num den-     fpFromReal sym e p r res--{- | Returns a predicate and two integers, @x@ and @y@.-If the the predicate holds, then @x / y@ is a rational representing-the floating point number. Assumes the FP number is not one of the-special ones that has no real representation. -}-fpToRational ::-  IsSymExprBuilder sym =>-  sym ->-  SFloat sym ->-  IO (Pred sym, SymInteger sym, SymInteger sym)-fpToRational sym fp =-  do r    <- fpToReal sym fp-     x    <- freshConstant sym emptySymbol BaseIntegerRepr-     y    <- freshConstant sym emptySymbol BaseIntegerRepr-     num  <- integerToReal sym x-     den  <- integerToReal sym y-     res  <- realDiv sym num den-     same <- realEq sym r res-     pure (same, x, y)-------------------------------------------------------------------------------------fpIsInf :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)-fpIsInf sym (SFloat x) = floatIsInf sym x--fpIsNaN :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)-fpIsNaN sym (SFloat x) = floatIsNaN sym x---

@@ -27,10 +27,13 @@   , emptyEnv   , evalExpr   , evalDecls+  , evalNewtypeDecls   , evalSel   , evalSetSel   , EvalError(..)+  , EvalErrorEx(..)   , Unsupported(..)+  , WordTooWide(..)   , forceValue   ) where @@ -39,9 +42,11 @@ import Cryptol.Backend.Monad import Cryptol.Eval.Generic ( iteValue ) import Cryptol.Eval.Env+import Cryptol.Eval.Prims import Cryptol.Eval.Type import Cryptol.Eval.Value import Cryptol.ModuleSystem.Name+import Cryptol.Parser.Position import Cryptol.Parser.Selector(ppSelector) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))@@ -63,9 +68,10 @@ type EvalEnv = GenEvalEnv Concrete  type EvalPrims sym =-  ( Backend sym, ?evalPrim :: PrimIdent -> Maybe (Either Expr (GenValue sym)) )+  ( Backend sym, ?callStacks :: Bool, ?evalPrim :: PrimIdent -> Maybe (Either Expr (Prim sym)) ) -type ConcPrims = ?evalPrim :: PrimIdent -> Maybe (Either Expr (GenValue Concrete))+type ConcPrims =+  (?callStacks :: Bool, ?evalPrim :: PrimIdent -> Maybe (Either Expr (Prim Concrete)))  -- Expression Evaluation ------------------------------------------------------- @@ -85,10 +91,10 @@   Module         {- ^ Module containing declarations to evaluate -} ->   GenEvalEnv sym {- ^ Environment to extend -} ->   SEval sym (GenEvalEnv sym)-moduleEnv sym m env = evalDecls sym (mDecls m) =<< evalNewtypes sym (mNewtypes m) env+moduleEnv sym m env = evalDecls sym (mDecls m) =<< evalNewtypeDecls sym (mNewtypes m) env  {-# SPECIALIZE evalExpr ::-  ConcPrims =>+  (?range :: Range, ConcPrims) =>   Concrete ->   GenEvalEnv Concrete ->   Expr ->@@ -99,13 +105,17 @@ --   by the `EvalPrims` class, which defines the behavior of bits and words, in --   addition to providing implementations for all the primitives. evalExpr ::-  EvalPrims sym =>+  (?range :: Range, EvalPrims sym) =>   sym ->   GenEvalEnv sym  {- ^ Evaluation environment -} ->   Expr          {- ^ Expression to evaluate -} ->   SEval sym (GenValue sym) evalExpr sym env expr = case expr of +  ELocated r e ->+    let ?range = r in+    evalExpr sym env e+   -- Try to detect when the user has directly written a finite sequence of   -- literal bit values and pack these into a word.   EList es ty@@ -115,22 +125,22 @@         return $ VWord len $           case tryFromBits sym vs of             Just w  -> WordVal <$> w-            Nothing -> do xs <- mapM (sDelay sym Nothing) vs-                          return $ LargeBitsVal len $ finiteSeqMap sym xs+            Nothing -> do xs <- mapM (sDelay sym) vs+                          return $ LargeBitsVal len $ finiteSeqMap xs     | otherwise -> {-# SCC "evalExpr->EList" #-} do-        xs <- mapM (sDelay sym Nothing) vs-        return $ VSeq len $ finiteSeqMap sym xs+        xs <- mapM (sDelay sym) vs+        return $ VSeq len $ finiteSeqMap xs    where     tyv = evalValType (envTypes env) ty     vs  = map eval es     len = genericLength es    ETuple es -> {-# SCC "evalExpr->ETuple" #-} do-     xs <- mapM (sDelay sym Nothing . eval) es+     xs <- mapM (sDelay sym . eval) es      return $ VTuple xs    ERec fields -> {-# SCC "evalExpr->ERec" #-} do-     xs <- traverse (sDelay sym Nothing . eval) fields+     xs <- traverse (sDelay sym . eval) fields      return $ VRecord xs    ESel e sel -> {-# SCC "evalExpr->ESel" #-} do@@ -153,7 +163,15 @@    EVar n -> {-# SCC "evalExpr->EVar" #-} do     case lookupVar n env of-      Just val -> val+      Just (Left p)+        | ?callStacks -> sPushFrame sym n ?range (cacheCallStack sym =<< evalPrim sym n p)+        | otherwise   -> evalPrim sym n p+      Just (Right val)+        | ?callStacks ->+            case nameInfo n of+              Declared{} -> sPushFrame sym n ?range (cacheCallStack sym =<< val)+              Parameter  -> cacheCallStack sym =<< val+        | otherwise -> val       Nothing  -> do         envdoc <- ppEnv sym defaultPPOpts env         panic "[Eval] evalExpr"@@ -163,14 +181,14 @@    ETAbs tv b -> {-# SCC "evalExpr->ETAbs" #-}     case tpKind tv of-      KType -> return $ VPoly    $ \ty -> evalExpr sym (bindType (tpVar tv) (Right ty) env) b-      KNum  -> return $ VNumPoly $ \n  -> evalExpr sym (bindType (tpVar tv) (Left n) env) b+      KType -> tlam sym $ \ty -> evalExpr sym (bindType (tpVar tv) (Right ty) env) b+      KNum  -> nlam sym $ \n  -> evalExpr sym (bindType (tpVar tv) (Left n) env) b       k     -> panic "[Eval] evalExpr" ["invalid kind on type abstraction", show k]    ETApp e ty -> {-# SCC "evalExpr->ETApp" #-} do     eval e >>= \case-      VPoly f     -> f $! (evalValType (envTypes env) ty)-      VNumPoly f  -> f $! (evalNumType (envTypes env) ty)+      f@VPoly{}    -> fromVPoly sym f    $! (evalValType (envTypes env) ty)+      f@VNumPoly{} -> fromVNumPoly sym f $! (evalNumType (envTypes env) ty)       val     -> do vdoc <- ppV val                     panic "[Eval] evalExpr"                       ["expected a polymorphic value"@@ -179,13 +197,13 @@    EApp f v -> {-# SCC "evalExpr->EApp" #-} do     eval f >>= \case-      VFun f' -> f' (eval v)-      it      -> do itdoc <- ppV it-                    panic "[Eval] evalExpr" ["not a function", show itdoc ]+      f'@VFun {} -> fromVFun sym f' (eval v)+      it         -> do itdoc <- ppV it+                       panic "[Eval] evalExpr" ["not a function", show itdoc ]    EAbs n _ty b -> {-# SCC "evalExpr->EAbs" #-}-    return $ VFun (\v -> do env' <- bindVar sym n v env-                            evalExpr sym env' b)+    lam sym (\v -> do env' <- bindVar sym n v env+                      evalExpr sym env' b)    -- XXX these will likely change once there is an evidence value   EProofAbs _ e -> eval e@@ -202,9 +220,31 @@   ppV = ppValue sym defaultPPOpts  +-- | Capure the current call stack from the evaluation monad and+--   annotate function values.  When arguments are later applied+--   to the function, the call stacks will be combined together.+cacheCallStack ::+  Backend sym =>+  sym ->+  GenValue sym ->+  SEval sym (GenValue sym)+cacheCallStack sym v = case v of+  VFun fnstk f ->+    do stk <- sGetCallStack sym+       pure (VFun (combineCallStacks stk fnstk) f)+  VPoly fnstk f ->+    do stk <- sGetCallStack sym+       pure (VPoly (combineCallStacks stk fnstk) f)+  VNumPoly fnstk f ->+    do stk <- sGetCallStack sym+       pure (VNumPoly (combineCallStacks stk fnstk) f)++  -- non-function types don't get annotated+  _ -> pure v+ -- Newtypes -------------------------------------------------------------------- -{-# SPECIALIZE evalNewtypes ::+{-# SPECIALIZE evalNewtypeDecls ::   ConcPrims =>   Concrete ->   Map.Map Name Newtype ->@@ -212,28 +252,34 @@   SEval Concrete (GenEvalEnv Concrete)   #-} -evalNewtypes ::+evalNewtypeDecls ::   EvalPrims sym =>   sym ->   Map.Map Name Newtype ->   GenEvalEnv sym ->   SEval sym (GenEvalEnv sym)-evalNewtypes sym nts env = foldM (flip (evalNewtype sym)) env $ Map.elems nts+evalNewtypeDecls sym nts env = foldM (flip (evalNewtypeDecl sym)) env $ Map.elems nts  -- | Introduce the constructor function for a newtype.-evalNewtype ::+evalNewtypeDecl ::   EvalPrims sym =>   sym ->   Newtype ->   GenEvalEnv sym ->   SEval sym (GenEvalEnv sym)-evalNewtype sym nt = bindVar sym (ntName nt) (return (foldr tabs con (ntParams nt)))+evalNewtypeDecl _sym nt = pure . bindVarDirect (ntName nt) (foldr tabs con (ntParams nt))   where-  tabs _tp body = tlam (\ _ -> body)-  con           = VFun id-{-# INLINE evalNewtype #-}+  con           = PFun PPrim +  tabs tp body =+    case tpKind tp of+      KType -> PTyPoly  (\ _ -> body)+      KNum  -> PNumPoly (\ _ -> body)+      k -> evalPanic "evalNewtypeDecl" ["illegal newtype parameter kind", show (pp k)] +{-# INLINE evalNewtypeDecl #-}++ -- Declarations ----------------------------------------------------------------  {-# SPECIALIZE evalDecls ::@@ -274,7 +320,7 @@       -- declare a "hole" for each declaration       -- and extend the evaluation environment       holes <- mapM (declHole sym) ds-      let holeEnv = IntMap.fromList $ [ (nameUnique nm, h) | (nm,_,h,_) <- holes ]+      let holeEnv = IntMap.fromList $ [ (nameUnique nm, Right h) | (nm,_,h,_) <- holes ]       let env' = env `mappend` emptyEnv{ envVars = holeEnv }        -- evaluate the declaration bodies, building a new evaluation environment@@ -318,12 +364,16 @@   SEval sym () fillHole sym env (nm, sch, _, fill) = do   case lookupVar nm env of-    Nothing -> evalPanic "fillHole" ["Recursive definition not completed", show (ppLocName nm)]-    Just v-     | isValueType env sch -> fill =<< sDelayFill sym v (etaDelay sym (show (ppLocName nm)) env sch v)-     | otherwise           -> fill (etaDelay sym (show (ppLocName nm)) env sch v)+    Just (Right v)+     | isValueType env sch ->+               fill =<< sDelayFill sym v+                          (Just (etaDelay sym env sch v))+                          (show (ppLocName nm)) +     | otherwise -> fill (etaDelay sym env sch v) +    _ -> evalPanic "fillHole" ["Recursive definition not completed", show (ppLocName nm)]+ -- | 'Value' types are non-polymorphic types recursive constructed from --   bits, finite sequences, tuples and records.  Types of this form can --   be implemented rather more efficiently than general types because we can@@ -337,6 +387,7 @@   go (TVSeq _ x)  = go x   go (TVTuple xs) = and (map go xs)   go (TVRec xs)   = and (fmap go xs)+  go (TVNewtype _ _ xs) = and (fmap go xs)   go _            = False  isValueType _ _ = False@@ -357,14 +408,13 @@   SEval sym (GenValue sym) ->   SEval sym (WordValue sym) etaWord sym n val = do-  w <- sDelay sym Nothing (fromWordVal "during eta-expansion" =<< val)-  xs <- memoMap $ IndexSeqMap $ \i ->+  w <- sDelay sym (fromWordVal "during eta-expansion" =<< val)+  xs <- memoMap sym $ IndexSeqMap $ \i ->           do w' <- w; VBit <$> indexWordValue sym w' i   pure $ LargeBitsVal n xs  {-# SPECIALIZE etaDelay ::   Concrete ->-  String ->   GenEvalEnv Concrete ->   Schema ->   SEval Concrete (GenValue Concrete) ->@@ -380,23 +430,24 @@ etaDelay ::   Backend sym =>   sym ->-  String ->   GenEvalEnv sym ->   Schema ->   SEval sym (GenValue sym) ->   SEval sym (GenValue sym)-etaDelay sym msg env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0+etaDelay sym env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0   where-  goTpVars env []     val = go (evalValType (envTypes env) tp0) val+  goTpVars env []     val =+     do stk <- sGetCallStack sym+        go stk (evalValType (envTypes env) tp0) val   goTpVars env (v:vs) val =     case tpKind v of-      KType -> return $ VPoly $ \t ->-                  goTpVars (bindType (tpVar v) (Right t) env) vs ( ($t) . fromVPoly =<< val )-      KNum  -> return $ VNumPoly $ \n ->-                  goTpVars (bindType (tpVar v) (Left n) env) vs ( ($n) . fromVNumPoly =<< val )+      KType -> tlam sym $ \t ->+                  goTpVars (bindType (tpVar v) (Right t) env) vs ( ($t) . fromVPoly sym =<< val )+      KNum  -> nlam sym $ \n ->+                  goTpVars (bindType (tpVar v) (Left n) env) vs ( ($n) . fromVNumPoly sym =<< val )       k     -> panic "[Eval] etaDelay" ["invalid kind on type abstraction", show k] -  go tp x | isReady sym x = x >>= \case+  go stk tp x | isReady sym x = x >>= \case       VBit{}      -> x       VInteger{}  -> x       VWord{}     -> x@@ -404,33 +455,39 @@       VFloat{}    -> x       VSeq n xs ->         case tp of-          TVSeq _nt el -> return $ VSeq n $ IndexSeqMap $ \i -> go el (lookupSeqMap xs i)+          TVSeq _nt el -> return $ VSeq n $ IndexSeqMap $ \i -> go stk el (lookupSeqMap xs i)           _ -> evalPanic "type mismatch during eta-expansion" ["Expected sequence type, but got " ++ show tp]        VStream xs ->         case tp of-          TVStream el -> return $ VStream $ IndexSeqMap $ \i -> go el (lookupSeqMap xs i)+          TVStream el -> return $ VStream $ IndexSeqMap $ \i -> go stk el (lookupSeqMap xs i)           _ -> evalPanic "type mismatch during eta-expansion" ["Expected stream type, but got " ++ show tp]        VTuple xs ->         case tp of-          TVTuple ts | length ts == length xs -> return $ VTuple (zipWith go ts xs)+          TVTuple ts | length ts == length xs -> return $ VTuple (zipWith (go stk) ts xs)           _ -> evalPanic "type mismatch during eta-expansion" ["Expected tuple type with " ++ show (length xs)                                    ++ " elements, but got " ++ show tp]        VRecord fs ->         case tp of+          TVNewtype _ _ fts ->+            do let res = zipRecords (\_ v t -> go stk t v) fs fts+               case res of+                 Left (Left f)  -> evalPanic "type mismatch during eta-expansion" ["missing field " ++ show f]+                 Left (Right f) -> evalPanic "type mismatch during eta-expansion" ["unexpected field " ++ show f]+                 Right fs' -> return (VRecord fs')           TVRec fts ->-            do let res = zipRecords (\_ v t -> go t v) fs fts+            do let res = zipRecords (\_ v t -> go stk t v) fs fts                case res of                  Left (Left f)  -> evalPanic "type mismatch during eta-expansion" ["missing field " ++ show f]                  Left (Right f) -> evalPanic "type mismatch during eta-expansion" ["unexpected field " ++ show f]                  Right fs' -> return (VRecord fs')           _ -> evalPanic "type mismatch during eta-expansion" ["Expected record type, but got " ++ show tp] -      VFun f ->+      f@VFun{} ->         case tp of-          TVFun _t1 t2 -> return $ VFun $ \a -> go t2 (f a)+          TVFun _t1 t2 -> lam sym $ \a -> go stk t2 (fromVFun sym f a)           _ -> evalPanic "type mismatch during eta-expansion" ["Expected function type but got " ++ show tp]        VPoly{} ->@@ -439,7 +496,7 @@       VNumPoly{} ->         evalPanic "type mismatch during eta-expansion" ["Encountered numeric polymorphic value"] -  go tp v =+  go stk tp v = sWithCallStack sym stk $     case tp of       TVBit -> v       TVInteger -> v@@ -449,40 +506,41 @@       TVArray{} -> v        TVSeq n TVBit ->-          do w <- sDelayFill sym (fromWordVal "during eta-expansion" =<< v) (etaWord sym n v)+          do w <- sDelayFill sym (fromWordVal "during eta-expansion" =<< v) (Just (etaWord sym n v)) ""              return $ VWord n w        TVSeq n el ->-          do x' <- sDelay sym (Just msg) (fromSeq "during eta-expansion" =<< v)+          do x' <- sDelay sym (fromSeq "during eta-expansion" =<< v)              return $ VSeq n $ IndexSeqMap $ \i -> do-               go el (flip lookupSeqMap i =<< x')+               go stk el (flip lookupSeqMap i =<< x')        TVStream el ->-          do x' <- sDelay sym (Just msg) (fromSeq "during eta-expansion" =<< v)+          do x' <- sDelay sym (fromSeq "during eta-expansion" =<< v)              return $ VStream $ IndexSeqMap $ \i ->-               go el (flip lookupSeqMap i =<< x')+               go stk el (flip lookupSeqMap i =<< x')        TVFun _t1 t2 ->-          do v' <- sDelay sym (Just msg) (fromVFun <$> v)-             return $ VFun $ \a -> go t2 ( ($a) =<< v' )+          do v' <- sDelay sym (fromVFun sym <$> v)+             lam sym $ \a -> go stk t2 ( ($a) =<< v' )        TVTuple ts ->           do let n = length ts-             v' <- sDelay sym (Just msg) (fromVTuple <$> v)+             v' <- sDelay sym (fromVTuple <$> v)              return $ VTuple $-                [ go t =<< (flip genericIndex i <$> v')+                [ go stk t =<< (flip genericIndex i <$> v')                 | i <- [0..(n-1)]                 | t <- ts                 ]        TVRec fs ->-          do v' <- sDelay sym (Just msg) (fromVRecord <$> v)+          do v' <- sDelay sym (fromVRecord <$> v)              let err f = evalPanic "expected record value with field" [show f]-             let eta f t = go t =<< (fromMaybe (err f) . lookupField f <$> v')+             let eta f t = go stk t =<< (fromMaybe (err f) . lookupField f <$> v')              return $ VRecord (mapWithFieldName eta fs)        TVAbstract {} -> v +      TVNewtype _ _ body -> go stk (TVRec body) v  {-# SPECIALIZE declHole ::   Concrete ->@@ -504,7 +562,7 @@   where   nm = dName d   sch = dSignature d-  msg = unwords ["<<loop>> while evaluating", show (pp nm)]+  msg = unwords ["while evaluating", show (pp nm)]   -- | Evaluate a declaration, extending the evaluation environment.@@ -522,10 +580,11 @@   Decl            {- ^ The declaration to evaluate -} ->   SEval sym (GenEvalEnv sym) evalDecl sym renv env d =+  let ?range = nameLoc (dName d) in   case dDefinition d of     DPrim ->       case ?evalPrim =<< asPrim (dName d) of-        Just (Right v) -> pure (bindVarDirect (dName d) v env)+        Just (Right p) -> pure $ bindVarDirect (dName d) p env         Just (Left ex) -> bindVar sym (dName d) (evalExpr sym renv ex) env         Nothing        -> bindVar sym (dName d) (cryNoPrimError sym (dName d)) env @@ -535,7 +594,6 @@ -- Selectors -------------------------------------------------------------------  {-# SPECIALIZE evalSel ::-  ConcPrims =>   Concrete ->   GenValue Concrete ->   Selector ->@@ -546,7 +604,7 @@ --   tuple and record selections pointwise down into other value constructs --   (e.g., streams and functions). evalSel ::-  EvalPrims sym =>+  Backend sym =>   sym ->   GenValue sym ->   Selector ->@@ -584,12 +642,11 @@                               [ "Unexpected value in list selection"                               , show vdoc ] {-# SPECIALIZE evalSetSel ::-  ConcPrims =>   Concrete -> TValue ->   GenValue Concrete -> Selector -> SEval Concrete (GenValue Concrete) -> SEval Concrete (GenValue Concrete)   #-} evalSetSel :: forall sym.-  EvalPrims sym =>+  Backend sym =>   sym ->   TValue ->   GenValue sym -> Selector -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)@@ -645,7 +702,7 @@ data ListEnv sym = ListEnv   { leVars   :: !(IntMap.IntMap (Integer -> SEval sym (GenValue sym)))       -- ^ Bindings whose values vary by position-  , leStatic :: !(IntMap.IntMap (SEval sym (GenValue sym)))+  , leStatic :: !(IntMap.IntMap (Either (Prim sym) (SEval sym (GenValue sym))))       -- ^ Bindings whose values are constant   , leTypes  :: !TypeEnv   }@@ -654,14 +711,14 @@   l <> r = ListEnv     { leVars   = IntMap.union (leVars  l)  (leVars  r)     , leStatic = IntMap.union (leStatic l) (leStatic r)-    , leTypes  = IntMap.union (leTypes l)  (leTypes r)+    , leTypes  = leTypes l <> leTypes r     }  instance Monoid (ListEnv sym) where   mempty = ListEnv     { leVars   = IntMap.empty     , leStatic = IntMap.empty-    , leTypes  = IntMap.empty+    , leTypes  = mempty     }    mappend l r = l <> r@@ -680,7 +737,7 @@ --   locations. evalListEnv :: ListEnv sym -> Integer -> GenEvalEnv sym evalListEnv (ListEnv vm st tm) i =-    let v = fmap ($i) vm+    let v = fmap (Right . ($i)) vm      in EvalEnv{ envVars = IntMap.union v st                , envTypes = tm                }@@ -698,7 +755,7 @@ -- List Comprehensions ---------------------------------------------------------  {-# SPECIALIZE evalComp ::-  ConcPrims =>+  (?range :: Range, ConcPrims) =>   Concrete ->   GenEvalEnv Concrete ->   Nat'           ->@@ -709,7 +766,7 @@   #-} -- | Evaluate a comprehension. evalComp ::-  EvalPrims sym =>+  (?range :: Range, EvalPrims sym) =>   sym ->   GenEvalEnv sym {- ^ Starting evaluation environment -} ->   Nat'           {- ^ Length of the comprehension -} ->@@ -719,11 +776,11 @@   SEval sym (GenValue sym) evalComp sym env len elty body ms =        do lenv <- mconcat <$> mapM (branchEnvs sym (toListEnv env)) ms-          mkSeq len elty <$> memoMap (IndexSeqMap $ \i -> do+          mkSeq len elty <$> memoMap sym (IndexSeqMap $ \i -> do               evalExpr sym (evalListEnv lenv i) body)  {-# SPECIALIZE branchEnvs ::-  ConcPrims =>+  (?range :: Range, ConcPrims) =>   Concrete ->   ListEnv Concrete ->   [Match] ->@@ -732,7 +789,7 @@ -- | Turn a list of matches into the final environments for each iteration of -- the branch. branchEnvs ::-  EvalPrims sym =>+  (?range :: Range, EvalPrims sym) =>   sym ->   ListEnv sym ->   [Match] ->@@ -740,7 +797,7 @@ branchEnvs sym env matches = foldM (evalMatch sym) env matches  {-# SPECIALIZE evalMatch ::-  ConcPrims =>+  (?range :: Range, ConcPrims) =>   Concrete ->   ListEnv Concrete ->   Match ->@@ -749,7 +806,7 @@  -- | Turn a match into the list of environments it represents. evalMatch ::-  EvalPrims sym =>+  (?range :: Range, EvalPrims sym) =>   sym ->   ListEnv sym ->   Match ->@@ -762,7 +819,7 @@       -- Select from a sequence of finite length.  This causes us to 'stutter'       -- through our previous choices `nLen` times.       Nat nLen -> do-        vss <- memoMap $ IndexSeqMap $ \i -> evalExpr sym (evalListEnv lenv i) expr+        vss <- memoMap sym $ IndexSeqMap $ \i -> evalExpr sym (evalListEnv lenv i) expr         let stutter xs = \i -> xs (i `div` nLen)         let lenv' = lenv { leVars = fmap stutter (leVars lenv) }         let vs i = do let (q, r) = i `divMod` nLen@@ -778,7 +835,7 @@       -- `leVars` elements of the comprehension environment into `leStatic` elements       -- by selecting out the 0th element.       Inf -> do-        let allvars = IntMap.union (fmap ($0) (leVars lenv)) (leStatic lenv)+        let allvars = IntMap.union (fmap (Right . ($0)) (leVars lenv)) (leStatic lenv)         let lenv' = lenv { leVars   = IntMap.empty                          , leStatic = allvars                          }

@@ -25,9 +25,9 @@   , toExpr   ) where -import Control.Monad (join, guard, zipWithM, foldM)+import Control.Monad (guard, zipWithM, foldM, mzero) import Data.Bits (Bits(..))-import Data.Ratio((%),numerator,denominator)+import Data.Ratio(numerator,denominator) import Data.Word(Word32, Word64) import MonadLib( ChoiceT, findOne, lift ) import qualified LibBF as FP@@ -44,6 +44,7 @@ import Cryptol.Backend.Monad  import Cryptol.Eval.Generic hiding (logicShift)+import Cryptol.Eval.Prims import Cryptol.Eval.Type import Cryptol.Eval.Value import qualified Cryptol.SHA as SHA@@ -54,7 +55,6 @@ import Cryptol.Utils.Panic (panic) import Cryptol.Utils.Ident (PrimIdent,prelPrim,floatPrim,suiteBPrim,primeECPrim) import Cryptol.Utils.PP-import Cryptol.Utils.Logger(logPrint) import Cryptol.Utils.RecordMap  type Value = GenValue Concrete@@ -63,57 +63,68 @@  -- | Given an expected type, returns an expression that evaluates to -- this value, if we can determine it.-toExpr :: PrimMap -> AST.Type -> Value -> Eval (Maybe AST.Expr)+toExpr :: PrimMap -> TValue -> Value -> Eval (Maybe AST.Expr) toExpr prims t0 v0 = findOne (go t0 v0)   where    prim n = ePrim prims (prelPrim n)  -  go :: AST.Type -> Value -> ChoiceT Eval Expr+  go :: TValue -> Value -> ChoiceT Eval Expr   go ty val =-    case val of-      VRecord vfs ->-        do tfs <- maybe mismatch pure (tIsRec ty)-           -- NB, vfs first argument to keep their display order+    case (ty,val) of+      (TVRec tfs, VRecord vfs) ->+        do -- NB, vfs first argument to keep their display order            res <- zipRecordsM (\_lbl v t -> go t =<< lift v) vfs tfs            case res of              Left _ -> mismatch -- different fields              Right efs -> pure (ERec efs)-      VTuple tvs ->-        do ts <- maybe mismatch pure (tIsTuple ty)-           guard (length ts == length tvs)++      (TVNewtype nt ts tfs, VRecord vfs) ->+        do -- NB, vfs first argument to keep their display order+           res <- zipRecordsM (\_lbl v t -> go t =<< lift v) vfs tfs+           case res of+             Left _ -> mismatch -- different fields+             Right efs ->+               let f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ntName nt)) ts+                in pure (EApp f (ERec efs))++      (TVTuple ts, VTuple tvs) ->+        do guard (length ts == length tvs)            ETuple <$> (zipWithM go ts =<< lift (sequence tvs))-      VBit b ->+      (TVBit, VBit b) ->         pure (prim (if b then "True" else "False"))-      VInteger i ->-        -- This works uniformly for values of type Integer or Z n-        pure $ ETApp (ETApp (prim "number") (tNum i)) ty-      VRational (SRational n d) ->+      (TVInteger, VInteger i) ->+        pure $ ETApp (ETApp (prim "number") (tNum i)) tInteger+      (TVIntMod n, VInteger i) ->+        pure $ ETApp (ETApp (prim "number") (tNum i)) (tIntMod (tNum n))++      (TVRational, VRational (SRational n d)) ->         do let n' = ETApp (ETApp (prim "number") (tNum n)) tInteger            let d' = ETApp (ETApp (prim "number") (tNum d)) tInteger            pure $ EApp (EApp (prim "ratio") n') d'-      VFloat i ->-        do (eT, pT) <- maybe mismatch pure (tIsFloat ty)-           pure (floatToExpr prims eT pT (bfValue i))-      VSeq n svs ->-        do (_a, b) <- maybe mismatch pure (tIsSeq ty)-           ses <- traverse (go b) =<< lift (sequence (enumerateSeqMap n svs))-           pure $ EList ses b-      VWord _ wval ->++      (TVFloat e p, VFloat i) ->+           pure (floatToExpr prims (tNum e) (tNum p) (bfValue i))+      (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) ->         do BV _ v <- lift (asWordVal Concrete =<< wval)-           pure $ ETApp (ETApp (prim "number") (tNum v)) ty-      VStream _  -> fail "cannot construct infinite expressions"-      VFun _     -> fail "cannot convert function values to expressions"-      VPoly _    -> fail "cannot convert polymorphic values to expressions"-      VNumPoly _ -> fail "cannot convert polymorphic values to expressions"+           pure $ ETApp (ETApp (prim "number") (tNum v)) (tWord (tNum n))++      (_,VStream{})  -> mzero+      (_,VFun{})     -> mzero+      (_,VPoly{})    -> mzero+      (_,VNumPoly{}) -> mzero+      _ -> mismatch     where       mismatch :: forall a. ChoiceT Eval a       mismatch =         do doc <- lift (ppValue Concrete defaultPPOpts val)            panic "Cryptol.Eval.Concrete.toExpr"              ["type mismatch:"-             , pretty ty+             , pretty (tValTy ty)              , render doc              ] @@ -139,153 +150,18 @@  -- Primitives ------------------------------------------------------------------ -primTable :: EvalOpts -> Map PrimIdent Value-primTable eOpts = let sym = Concrete in-  Map.union (floatPrims sym) $+primTable :: IO EvalOpts -> Map PrimIdent (Prim Concrete)+primTable getEOpts = let sym = Concrete in+  Map.union (genericPrimTable sym getEOpts) $+  Map.union (genericFloatTable sym) $   Map.union suiteBPrims $   Map.union primeECPrims $    Map.fromList $ map (\(n, v) -> (prelPrim n, v)) -  [ -- Literals-    ("True"       , VBit (bitLit sym True))-  , ("False"      , VBit (bitLit sym False))-  , ("number"     , {-# SCC "Prelude::number" #-}-                    ecNumberV sym)-  , ("ratio"      , {-# SCC "Prelude::ratio" #-}-                    ratioV sym)-  , ("fraction"   , ecFractionV sym)---    -- Zero-  , ("zero"       , {-# SCC "Prelude::zero" #-}-                    VPoly (zeroV sym))--    -- Logic-  , ("&&"         , {-# SCC "Prelude::(&&)" #-}-                    binary (andV sym))-  , ("||"         , {-# SCC "Prelude::(||)" #-}-                    binary (orV sym))-  , ("^"          , {-# SCC "Prelude::(^)" #-}-                    binary (xorV sym))-  , ("complement" , {-# SCC "Prelude::complement" #-}-                    unary  (complementV sym))--    -- Ring-  , ("fromInteger", {-# SCC "Prelude::fromInteger" #-}-                    fromIntegerV sym)-  , ("+"          , {-# SCC "Prelude::(+)" #-}-                    binary (addV sym))-  , ("-"          , {-# SCC "Prelude::(-)" #-}-                    binary (subV sym))-  , ("*"          , {-# SCC "Prelude::(*)" #-}-                    binary (mulV sym))-  , ("negate"     , {-# SCC "Prelude::negate" #-}-                    unary (negateV sym))--    -- Integral-  , ("toInteger"  , {-# SCC "Prelude::toInteger" #-}-                    toIntegerV sym)-  , ("/"          , {-# SCC "Prelude::(/)" #-}-                    binary (divV sym))-  , ("%"          , {-# SCC "Prelude::(%)" #-}-                    binary (modV sym))-  , ("^^"         , {-# SCC "Prelude::(^^)" #-}-                    expV sym)-  , ("infFrom"    , {-# SCC "Prelude::infFrom" #-}-                    infFromV sym)-  , ("infFromThen", {-# SCC "Prelude::infFromThen" #-}-                    infFromThenV sym)--    -- Field-  , ("recip"      , {-# SCC "Prelude::recip" #-}-                    recipV sym)-  , ("/."         , {-# SCC "Prelude::(/.)" #-}-                    fieldDivideV sym)--    -- Round-  , ("floor"      , {-# SCC "Prelude::floor" #-}-                    unary (floorV sym))-  , ("ceiling"    , {-# SCC "Prelude::ceiling" #-}-                    unary (ceilingV sym))-  , ("trunc"      , {-# SCC "Prelude::trunc" #-}-                    unary (truncV sym))-  , ("roundAway"  , {-# SCC "Prelude::roundAway" #-}-                    unary (roundAwayV sym))-  , ("roundToEven", {-# SCC "Prelude::roundToEven" #-}-                    unary (roundToEvenV sym))--    -- Bitvector specific operations-  , ("/$"         , {-# SCC "Prelude::(/$)" #-}-                    sdivV sym)-  , ("%$"         , {-# SCC "Prelude::(%$)" #-}-                    smodV sym)-  , ("lg2"        , {-# SCC "Prelude::lg2" #-}-                    lg2V sym)-  , (">>$"        , {-# SCC "Prelude::(>>$)" #-}+  [ (">>$"        , {-# SCC "Prelude::(>>$)" #-}                     sshrV) -    -- Cmp-  , ("<"          , {-# SCC "Prelude::(<)" #-}-                    binary (lessThanV sym))-  , (">"          , {-# SCC "Prelude::(>)" #-}-                    binary (greaterThanV sym))-  , ("<="         , {-# SCC "Prelude::(<=)" #-}-                    binary (lessThanEqV sym))-  , (">="         , {-# SCC "Prelude::(>=)" #-}-                    binary (greaterThanEqV sym))-  , ("=="         , {-# SCC "Prelude::(==)" #-}-                    binary (eqV sym))-  , ("!="         , {-# SCC "Prelude::(!=)" #-}-                    binary (distinctV sym))--    -- SignedCmp-  , ("<$"         , {-# SCC "Prelude::(<$)" #-}-                    binary (signedLessThanV sym))--    -- Finite enumerations-  , ("fromTo"     , {-# SCC "Prelude::fromTo" #-}-                    fromToV sym)-  , ("fromThenTo" , {-# SCC "Prelude::fromThenTo" #-}-                    fromThenToV sym)--    -- Sequence manipulations-  , ("#"          , {-# SCC "Prelude::(#)" #-}-                    nlam $ \ front ->-                    nlam $ \ back  ->-                    tlam $ \ elty  ->-                    lam  $ \ l     -> return $-                    lam  $ \ r     -> join (ccatV sym front back elty <$> l <*> r))---  , ("join"       , {-# SCC "Prelude::join" #-}-                    nlam $ \ parts ->-                    nlam $ \ (finNat' -> each)  ->-                    tlam $ \ a     ->-                    lam  $ \ x     ->-                      joinV sym parts each a =<< x)--  , ("split"      , {-# SCC "Prelude::split" #-}-                    ecSplitV sym)--  , ("splitAt"    , {-# SCC "Prelude::splitAt" #-}-                    nlam $ \ front ->-                    nlam $ \ back  ->-                    tlam $ \ a     ->-                    lam  $ \ x     ->-                       splitAtV sym front back a =<< x)--  , ("reverse"    , {-# SCC "Prelude::reverse" #-}-                    nlam $ \_a ->-                    tlam $ \_b ->-                     lam $ \xs -> reverseV sym =<< xs)--  , ("transpose"  , {-# SCC "Prelude::transpose" #-}-                    nlam $ \a ->-                    nlam $ \b ->-                    tlam $ \c ->-                     lam $ \xs -> transposeV sym a b c =<< xs)-     -- Shifts and rotates   , ("<<"         , {-# SCC "Prelude::(<<)" #-}                     logicShift shiftLW shiftLS)@@ -308,56 +184,12 @@   , ("updateEnd"  , {-# SCC "Prelude::updateEnd" #-}                     updatePrim sym updateBack_word updateBack) -    -- Misc-  , ("foldl"      , {-# SCC "Prelude::foldl" #-}-                    foldlV sym)--  , ("foldl'"     , {-# SCC "Prelude::foldl'" #-}-                    foldl'V sym)--  , ("deepseq"    , {-# SCC "Prelude::deepseq" #-}-                    tlam $ \_a ->-                    tlam $ \_b ->-                     lam $ \x -> pure $-                     lam $ \y ->-                       do _ <- forceValue =<< x-                          y)--  , ("parmap"     , {-# SCC "Prelude::parmap" #-}-                    parmapV sym)--  , ("fromZ"      , {-# SCC "Prelude::fromZ" #-}-                    fromZV sym)--  , ("error"      , {-# SCC "Prelude::error" #-}-                      tlam $ \a ->-                      nlam $ \_ ->-                       lam $ \s -> errorV sym a =<< (valueToString sym =<< s))--  , ("random"      , {-# SCC "Prelude::random" #-}-                     tlam $ \a ->-                     wlam sym $ \(bvVal -> x) -> randomV sym a x)--  , ("trace"       , {-# SCC "Prelude::trace" #-}-                     nlam $ \_n ->-                     tlam $ \_a ->-                     tlam $ \_b ->-                      lam $ \s -> return $-                      lam $ \x -> return $-                      lam $ \y -> do-                         msg <- valueToString sym =<< s-                         let EvalOpts { evalPPOpts, evalLogger } = eOpts-                         doc <- ppValue sym evalPPOpts =<< x-                         yv <- y-                         io $ logPrint evalLogger-                             $ if null msg then doc else text msg <+> doc-                         return yv)-    , ("pmult",-        ilam $ \u ->-        ilam $ \v ->-          wlam Concrete $ \(BV _ x) -> return $-          wlam Concrete $ \(BV _ y) ->+        PFinPoly \u ->+        PFinPoly \v ->+        PWordFun \(BV _ x) ->+        PWordFun \(BV _ y) ->+        PPrim             let z = if u <= v then                       F2.pmult (fromInteger (u+1)) x y                     else@@ -365,56 +197,62 @@              in return . VWord (1+u+v) . pure . WordVal . mkBv (1+u+v) $! z)     , ("pmod",-        ilam $ \_u ->-        ilam $ \v ->-        wlam Concrete $ \(BV w x) -> return $-        wlam Concrete $ \(BV _ m) ->+        PFinPoly \_u ->+        PFinPoly \v ->+        PWordFun \(BV w x) ->+        PWordFun \(BV _ m) ->+        PPrim           do assertSideCondition sym (m /= 0) DivideByZero              return . VWord v . pure . WordVal . mkBv v $! F2.pmod (fromInteger w) x m)    , ("pdiv",-        ilam $ \_u ->-        ilam $ \_v ->-        wlam Concrete $ \(BV w x) -> return $-        wlam Concrete $ \(BV _ m) ->+        PFinPoly \_u ->+        PFinPoly \_v ->+        PWordFun \(BV w x) ->+        PWordFun \(BV _ m) ->+        PPrim           do assertSideCondition sym (m /= 0) DivideByZero              return . VWord w . pure . WordVal . mkBv w $! F2.pdiv (fromInteger w) x m)   ]  -primeECPrims :: Map.Map PrimIdent Value+primeECPrims :: Map.Map PrimIdent (Prim Concrete) primeECPrims = Map.fromList $ map (\(n,v) -> (primeECPrim n, v))   [ ("ec_double", {-# SCC "PrimeEC::ec_double" #-}-       ilam $ \p ->-        lam $ \s ->+       PFinPoly \p ->+       PFun     \s ->+       PPrim           do s' <- toProjectivePoint =<< s              let r = PrimeEC.ec_double (PrimeEC.primeModulus p) s'              fromProjectivePoint $! r)    , ("ec_add_nonzero", {-# SCC "PrimeEC::ec_add_nonzero" #-}-       ilam $ \p ->-        lam $ \s -> pure $-        lam $ \t ->+       PFinPoly \p ->+       PFun     \s ->+       PFun     \t ->+       PPrim            do s' <- toProjectivePoint =<< s              t' <- toProjectivePoint =<< t              let r = PrimeEC.ec_add_nonzero (PrimeEC.primeModulus p) s' t'              fromProjectivePoint $! r)    , ("ec_mult", {-# SCC "PrimeEC::ec_mult" #-}-       ilam $ \p ->-        lam $ \d -> pure $-        lam $ \s ->+       PFinPoly \p ->+       PFun     \d ->+       PFun     \s ->+       PPrim           do d' <- fromVInteger <$> d              s' <- toProjectivePoint =<< s              let r = PrimeEC.ec_mult (PrimeEC.primeModulus p) d' s'              fromProjectivePoint $! r)    , ("ec_twin_mult", {-# SCC "PrimeEC::ec_twin_mult" #-}-       ilam $ \p ->-        lam $ \d0 -> pure $-        lam $ \s  -> pure $-        lam $ \d1 -> pure $-        lam $ \t  ->+       PFinPoly \p  ->+       PFun     \d0 ->+       PFun     \s  ->+       PFun     \d1 ->+       PFun     \t  ->+       PPrim           do d0' <- fromVInteger <$> d0              s'  <- toProjectivePoint =<< s              d1' <- fromVInteger <$> d1@@ -436,59 +274,64 @@   -suiteBPrims :: Map.Map PrimIdent Value+suiteBPrims :: Map.Map PrimIdent (Prim Concrete) suiteBPrims = Map.fromList $ map (\(n, v) -> (suiteBPrim n, v))   [ ("processSHA2_224", {-# SCC "SuiteB::processSHA2_224" #-}-                      ilam $ \n ->-                       lam $ \xs ->-                         do blks <- enumerateSeqMap n . fromVSeq <$> xs-                            (SHA.SHA256S w0 w1 w2 w3 w4 w5 w6 _) <--                               foldM (\st blk -> seq st (SHA.processSHA256Block st <$> (toSHA256Block =<< blk)))-                                     SHA.initialSHA224State blks-                            let f :: Word32 -> Eval Value-                                f = pure . VWord 32 . pure . WordVal . BV 32 . toInteger-                                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6])-                            seq zs (pure (VSeq 7 zs)))+     PFinPoly \n ->+     PFun     \xs ->+     PPrim+        do blks <- enumerateSeqMap n . fromVSeq <$> xs+           (SHA.SHA256S w0 w1 w2 w3 w4 w5 w6 _) <-+              foldM (\st blk -> seq st (SHA.processSHA256Block st <$> (toSHA256Block =<< blk)))+                    SHA.initialSHA224State blks+           let f :: Word32 -> Eval Value+               f = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+               zs = finiteSeqMap (map f [w0,w1,w2,w3,w4,w5,w6])+           seq zs (pure (VSeq 7 zs)))    , ("processSHA2_256", {-# SCC "SuiteB::processSHA2_256" #-}-                      ilam $ \n ->-                       lam $ \xs ->-                         do blks <- enumerateSeqMap n . fromVSeq <$> xs-                            (SHA.SHA256S w0 w1 w2 w3 w4 w5 w6 w7) <--                              foldM (\st blk -> seq st (SHA.processSHA256Block st <$> (toSHA256Block =<< blk)))-                                    SHA.initialSHA256State blks-                            let f :: Word32 -> Eval Value-                                f = pure . VWord 32 . pure . WordVal . BV 32 . toInteger-                                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6,w7])-                            seq zs (pure (VSeq 8 zs)))+     PFinPoly \n ->+     PFun     \xs ->+     PPrim+        do blks <- enumerateSeqMap n . fromVSeq <$> xs+           (SHA.SHA256S w0 w1 w2 w3 w4 w5 w6 w7) <-+             foldM (\st blk -> seq st (SHA.processSHA256Block st <$> (toSHA256Block =<< blk)))+                   SHA.initialSHA256State blks+           let f :: Word32 -> Eval Value+               f = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+               zs = finiteSeqMap (map f [w0,w1,w2,w3,w4,w5,w6,w7])+           seq zs (pure (VSeq 8 zs)))    , ("processSHA2_384", {-# SCC "SuiteB::processSHA2_384" #-}-                      ilam $ \n ->-                       lam $ \xs ->-                         do blks <- enumerateSeqMap n . fromVSeq <$> xs-                            (SHA.SHA512S w0 w1 w2 w3 w4 w5 _ _) <--                              foldM (\st blk -> seq st (SHA.processSHA512Block st <$> (toSHA512Block =<< blk)))-                                    SHA.initialSHA384State blks-                            let f :: Word64 -> Eval Value-                                f = pure . VWord 64 . pure . WordVal . BV 64 . toInteger-                                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5])-                            seq zs (pure (VSeq 6 zs)))+     PFinPoly \n ->+     PFun     \xs ->+     PPrim+        do blks <- enumerateSeqMap n . fromVSeq <$> xs+           (SHA.SHA512S w0 w1 w2 w3 w4 w5 _ _) <-+             foldM (\st blk -> seq st (SHA.processSHA512Block st <$> (toSHA512Block =<< blk)))+                   SHA.initialSHA384State blks+           let f :: Word64 -> Eval Value+               f = pure . VWord 64 . pure . WordVal . BV 64 . toInteger+               zs = finiteSeqMap (map f [w0,w1,w2,w3,w4,w5])+           seq zs (pure (VSeq 6 zs)))    , ("processSHA2_512", {-# SCC "SuiteB::processSHA2_512" #-}-                      ilam $ \n ->-                       lam $ \xs ->-                         do blks <- enumerateSeqMap n . fromVSeq <$> xs-                            (SHA.SHA512S w0 w1 w2 w3 w4 w5 w6 w7) <--                              foldM (\st blk -> seq st (SHA.processSHA512Block st <$> (toSHA512Block =<< blk)))-                                    SHA.initialSHA512State blks-                            let f :: Word64 -> Eval Value-                                f = pure . VWord 64 . pure . WordVal . BV 64 . toInteger-                                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6,w7])-                            seq zs (pure (VSeq 8 zs)))+     PFinPoly \n ->+     PFun     \xs ->+     PPrim+        do blks <- enumerateSeqMap n . fromVSeq <$> xs+           (SHA.SHA512S w0 w1 w2 w3 w4 w5 w6 w7) <-+             foldM (\st blk -> seq st (SHA.processSHA512Block st <$> (toSHA512Block =<< blk)))+                   SHA.initialSHA512State blks+           let f :: Word64 -> Eval Value+               f = pure . VWord 64 . pure . WordVal . BV 64 . toInteger+               zs = finiteSeqMap (map f [w0,w1,w2,w3,w4,w5,w6,w7])+           seq zs (pure (VSeq 8 zs)))    , ("AESKeyExpand", {-# SCC "SuiteB::AESKeyExpand" #-}-      ilam $ \k ->-       lam $ \seed ->+      PFinPoly \k ->+      PFun     \seed ->+      PPrim          do ss <- fromVSeq <$> seed             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESInfKeyExpand" =<< lookupSeqMap ss i)@@ -497,10 +340,11 @@             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))))+            pure (VSeq len (finiteSeqMap (map fromWord ws))))    , ("AESInvMixColumns", {-# SCC "SuiteB::AESInvMixColumns" #-}-      lam $ \st ->+      PFun \st ->+      PPrim          do ss <- fromVSeq <$> st             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESInvMixColumns" =<< lookupSeqMap ss i)@@ -508,10 +352,11 @@                 fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger             ws <- mapM toWord [0,1,2,3]             let ws' = AES.invMixColumns ws-            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')+            pure . VSeq 4 . finiteSeqMap . map fromWord $ ws')    , ("AESEncRound", {-# SCC "SuiteB::AESEncRound" #-}-      lam $ \st ->+      PFun \st ->+      PPrim          do ss <- fromVSeq <$> st             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESEncRound" =<< lookupSeqMap ss i)@@ -519,10 +364,11 @@                 fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger             ws <- mapM toWord [0,1,2,3]             let ws' = AES.aesRound ws-            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')+            pure . VSeq 4 . finiteSeqMap . map fromWord $ ws')    , ("AESEncFinalRound", {-# SCC "SuiteB::AESEncFinalRound" #-}-      lam $ \st ->+     PFun \st ->+     PPrim          do ss <- fromVSeq <$> st             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESEncFinalRound" =<< lookupSeqMap ss i)@@ -530,10 +376,11 @@                 fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger             ws <- mapM toWord [0,1,2,3]             let ws' = AES.aesFinalRound ws-            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')+            pure . VSeq 4 . finiteSeqMap . map fromWord $ ws')    , ("AESDecRound", {-# SCC "SuiteB::AESDecRound" #-}-      lam $ \st ->+      PFun \st ->+      PPrim          do ss <- fromVSeq <$> st             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESDecRound" =<< lookupSeqMap ss i)@@ -541,10 +388,11 @@                 fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger             ws <- mapM toWord [0,1,2,3]             let ws' = AES.aesInvRound ws-            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')+            pure . VSeq 4 . finiteSeqMap . map fromWord $ ws')    , ("AESDecFinalRound", {-# SCC "SuiteB::AESDecFinalRound" #-}-      lam $ \st ->+     PFun \st ->+     PPrim          do ss <- fromVSeq <$> st             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESDecFinalRound" =<< lookupSeqMap ss i)@@ -552,7 +400,7 @@                 fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger             ws <- mapM toWord [0,1,2,3]             let ws' = AES.aesInvFinalRound ws-            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')+            pure . VSeq 4 . finiteSeqMap . map fromWord $ ws')   ]  @@ -603,12 +451,13 @@  -------------------------------------------------------------------------------- -sshrV :: Value+sshrV :: Prim Concrete sshrV =-  nlam $ \_n ->-  tlam $ \ix ->-  wlam Concrete $ \(BV w x) -> return $-  lam $ \y ->+  PNumPoly \_n ->+  PTyPoly  \ix ->+  PWordFun \(BV w x) ->+  PFun     \y ->+  PPrim    do idx <- y >>= asIndex Concrete ">>$" ix >>= \case                  Left idx -> pure idx                  Right wv -> bvVal <$> asWordVal Concrete wv@@ -618,14 +467,15 @@               -- ^ The function may assume its arguments are masked.               -- It is responsible for masking its result if needed.            -> (Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete)-           -> Value-logicShift opW opS-  = nlam $ \ a ->-    tlam $ \ _ix ->-    tlam $ \ c ->-     lam  $ \ l -> return $-     lam  $ \ r -> do-        i <- r >>= \case+           -> Prim Concrete+logicShift opW opS =+  PNumPoly \a ->+  PTyPoly  \_ix ->+  PTyPoly  \c ->+  PFun     \l ->+  PFun     \r ->+  PPrim+     do i <- r >>= \case           VInteger i -> pure i           VWord _ wval -> bvVal <$> (asWordVal Concrete =<< wval)           _ -> evalPanic "logicShift" ["not an index"]@@ -795,55 +645,3 @@ updateBack_word (Nat n) _eltTy bs (Right w) val = do   idx <- bvVal <$> asWordVal Concrete w   updateWordValue Concrete bs (n - idx - 1) (fromVBit <$> val)---floatPrims :: Concrete -> Map PrimIdent Value-floatPrims sym = Map.fromList [ (floatPrim i,v) | (i,v) <- nonInfixTable ]-  where-  (~>) = (,)-  nonInfixTable =-    [ "fpNaN"       ~> ilam \e -> ilam \p ->-                        VFloat BF { bfValue = FP.bfNaN-                                  , bfExpWidth = e, bfPrecWidth = p }--    , "fpPosInf"    ~> ilam \e -> ilam \p ->-                       VFloat BF { bfValue = FP.bfPosInf-                                 , bfExpWidth = e, bfPrecWidth = p }--    , "fpFromBits"  ~> ilam \e -> ilam \p -> wlam sym \bv ->-                       pure $ VFloat $ floatFromBits e p $ bvVal bv--    , "fpToBits"    ~> ilam \e -> ilam \p -> flam \x ->-                       pure $ word sym (e + p)-                            $ floatToBits e p-                            $ bfValue x-    , "=.="         ~> ilam \_ -> ilam \_ -> flam \x -> pure $ flam \y ->-                       pure $ VBit-                            $ bitLit sym-                            $ FP.bfCompare (bfValue x) (bfValue y) == EQ--    , "fpIsFinite"  ~> ilam \_ -> ilam \_ -> flam \x ->-                       pure $ VBit $ bitLit sym $ FP.bfIsFinite $ bfValue x--      -- From Backend class-    , "fpAdd"      ~> fpBinArithV sym fpPlus-    , "fpSub"      ~> fpBinArithV sym fpMinus-    , "fpMul"      ~> fpBinArithV sym fpMult-    , "fpDiv"      ~> fpBinArithV sym fpDiv--    , "fpFromRational" ~>-      ilam \e -> ilam \p -> wlam sym \r -> pure $ lam \x ->-        do rat <- fromVRational <$> x-           VFloat <$> do mode <- fpRoundMode sym r-                         pure $ floatFromRational e p mode-                              $ sNum rat % sDenom rat-    , "fpToRational" ~>-      ilam \_e -> ilam \_p -> flam \fp ->-      case floatToRational "fpToRational" fp of-        Left err -> raiseError sym err-        Right r  -> pure $-                      VRational-                        SRational { sNum = numerator r, sDenom = denominator r }-    ]--

@@ -16,8 +16,7 @@  import Cryptol.Backend -import Cryptol.Backend.Monad( PPOpts )-+import Cryptol.Eval.Prims import Cryptol.Eval.Type import Cryptol.Eval.Value import Cryptol.ModuleSystem.Name@@ -25,7 +24,6 @@ import Cryptol.TypeCheck.Solver.InfNat import Cryptol.Utils.PP - import qualified Data.IntMap.Strict as IntMap import Data.Semigroup @@ -37,29 +35,31 @@ -- Evaluation Environment ------------------------------------------------------  data GenEvalEnv sym = EvalEnv-  { envVars       :: !(IntMap.IntMap (SEval sym (GenValue sym)))+  { envVars       :: !(IntMap.IntMap (Either (Prim sym) (SEval sym (GenValue sym))))   , envTypes      :: !TypeEnv   } deriving Generic  instance Semigroup (GenEvalEnv sym) where   l <> r = EvalEnv     { envVars     = IntMap.union (envVars l) (envVars r)-    , envTypes    = IntMap.union (envTypes l) (envTypes r)+    , envTypes    = envTypes l <> envTypes r     }  instance Monoid (GenEvalEnv sym) where   mempty = EvalEnv     { envVars       = IntMap.empty-    , envTypes      = IntMap.empty+    , envTypes      = mempty     }-   mappend l r = l <> r  ppEnv :: Backend sym => sym -> PPOpts -> GenEvalEnv sym -> SEval sym Doc ppEnv sym opts env = brackets . fsep <$> mapM bind (IntMap.toList (envVars env))   where-   bind (k,v) = do vdoc <- ppValue sym opts =<< v-                   return (int k <+> text "->" <+> vdoc)+   bind (k,Left _) =+      do return (int k <+> text "<<prim>>")+   bind (k,Right v) =+      do vdoc <- ppValue sym opts =<< v+         return (int k <+> text "->" <+> vdoc)  -- | Evaluation environment with no bindings emptyEnv :: GenEvalEnv sym@@ -75,32 +75,32 @@   SEval sym (GenEvalEnv sym) bindVar sym n val env = do   let nm = show $ ppLocName n-  val' <- sDelay sym (Just nm) val-  return $ env{ envVars = IntMap.insert (nameUnique n) val' (envVars env) }+  val' <- sDelayFill sym val Nothing nm+  return $ env{ envVars = IntMap.insert (nameUnique n) (Right val') (envVars env) }  -- | Bind a variable to a value in the evaluation environment, without --   creating a thunk. bindVarDirect ::   Backend sym =>   Name ->-  GenValue sym ->+  Prim sym ->   GenEvalEnv sym ->   GenEvalEnv sym bindVarDirect n val env = do-  env{ envVars = IntMap.insert (nameUnique n) (pure val) (envVars env) }+  env{ envVars = IntMap.insert (nameUnique n) (Left val) (envVars env) }  -- | Lookup a variable in the environment. {-# INLINE lookupVar #-}-lookupVar :: Name -> GenEvalEnv sym -> Maybe (SEval sym (GenValue sym))+lookupVar :: Name -> GenEvalEnv sym -> Maybe (Either (Prim sym) (SEval sym (GenValue sym))) lookupVar n env = IntMap.lookup (nameUnique n) (envVars env)  -- | Bind a type variable of kind *. {-# INLINE bindType #-} bindType :: TVar -> Either Nat' TValue -> GenEvalEnv sym -> GenEvalEnv sym-bindType p ty env = env { envTypes = IntMap.insert (tvUnique p) ty (envTypes env) }+bindType p ty env = env{ envTypes = bindTypeVar p ty (envTypes env) }  -- | Lookup a type variable. {-# INLINE lookupType #-} lookupType :: TVar -> GenEvalEnv sym -> Maybe (Either Nat' TValue)-lookupType p env = IntMap.lookup (tvUnique p) (envTypes env)+lookupType p env = lookupTypeVar p (envTypes env) 

@@ -11,6 +11,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE Rank2Types #-}@@ -27,24 +28,28 @@ import System.Random.TF.Gen (seedTFGen)  import Data.Bits (testBit, (.&.), shiftR)- import Data.Maybe (fromMaybe)+import qualified Data.Map.Strict as Map+import Data.Map(Map) import Data.Ratio ((%))  import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),nMul,widthInteger) import Cryptol.Backend import Cryptol.Backend.Concrete (Concrete(..))-import Cryptol.Backend.Monad ( Eval, evalPanic, EvalError(..), Unsupported(..) )+import Cryptol.Backend.Monad( Eval, evalPanic, EvalError(..), Unsupported(..) ) import Cryptol.Testing.Random( randomValue ) +import Cryptol.Eval.Prims import Cryptol.Eval.Type import Cryptol.Eval.Value+import Cryptol.Utils.Ident (PrimIdent, prelPrim, floatPrim)+import Cryptol.Utils.Logger(logPrint) import Cryptol.Utils.Panic (panic)+import Cryptol.Utils.PP import Cryptol.Utils.RecordMap  - {-# SPECIALIZE mkLit :: Concrete -> TValue -> Integer -> Eval (GenValue Concrete)   #-} @@ -63,14 +68,15 @@     _                            -> evalPanic "Cryptol.Eval.Prim.evalConst"                                     [ "Invalid type for number" ] -{-# SPECIALIZE ecNumberV :: Concrete -> GenValue Concrete+{-# SPECIALIZE ecNumberV :: Concrete -> Prim Concrete   #-}  -- | Make a numeric constant.-ecNumberV :: Backend sym => sym -> GenValue sym+ecNumberV :: Backend sym => sym -> Prim sym ecNumberV sym =-  nlam $ \valT ->-  VPoly $ \ty ->+  PNumPoly \valT ->+  PTyPoly \ty ->+  PPrim   case valT of     Nat v -> mkLit sym ty v     _ -> evalPanic "Cryptol.Eval.Prim.evalConst"@@ -80,32 +86,38 @@              ]  - {-# SPECIALIZE intV :: Concrete -> Integer -> TValue -> Eval (GenValue Concrete)   #-} intV :: Backend sym => sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)-intV sym i = ringNullary sym (\w -> wordFromInt sym w i) (pure i) (\m -> intToZn sym m i) (intToRational sym i)-            (\e p -> fpRndMode sym >>= \r -> fpFromInteger sym e p r i)+intV sym i =+  ringNullary sym+    (\w -> wordFromInt sym w i)+    (pure i)+    (\m -> intToZn sym m i)+    (intToRational sym i)+    (\e p -> fpRndMode sym >>= \r -> fpFromInteger sym e p r i) -{-# SPECIALIZE ratioV :: Concrete -> GenValue Concrete #-}-ratioV :: Backend sym => sym -> GenValue sym+{-# SPECIALIZE ratioV :: Concrete -> Prim Concrete #-}+ratioV :: Backend sym => sym -> Prim sym ratioV sym =-  lam $ \x -> return $-  lam $ \y ->+  PFun   \x ->+  PFun   \y ->+  PPrim     do x' <- fromVInteger <$> x        y' <- fromVInteger <$> y        VRational <$> ratio sym x' y' -{-# SPECIALIZE ecFractionV :: Concrete -> GenValue Concrete+{-# SPECIALIZE ecFractionV :: Concrete -> Prim Concrete   #-}-ecFractionV :: Backend sym => sym -> GenValue sym+ecFractionV :: Backend sym => sym -> Prim sym ecFractionV sym =-  ilam  \n ->-  ilam  \d ->-  ilam  \_r ->-  VPoly \ty ->+  PFinPoly \n  ->+  PFinPoly \d  ->+  PFinPoly \_r ->+  PTyPoly  \ty ->+  PPrim     case ty of-      TVFloat e p -> VFloat    <$> fpLit sym e p (n % d)+      TVFloat e p -> VFloat <$> fpLit sym e p (n % d)       TVRational ->         do x <- integerLit sym n            y <- integerLit sym d@@ -116,34 +128,38 @@   -{-# SPECIALIZE fromZV :: Concrete -> GenValue Concrete #-}-fromZV :: Backend sym => sym -> GenValue sym+{-# SPECIALIZE fromZV :: Concrete -> Prim Concrete #-}+fromZV :: Backend sym => sym -> Prim sym fromZV sym =-  nlam $ \(finNat' -> n) ->-  lam $ \v -> VInteger <$> (znToInt sym n . fromVInteger =<< v)+  PFinPoly \n ->+  PFun     \v ->+  PPrim+    (VInteger <$> (znToInt sym n . fromVInteger =<< v))  -- Operation Lifting -----------------------------------------------------------   type Binary sym = TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym) -{-# SPECIALIZE binary :: Binary Concrete -> GenValue Concrete+{-# SPECIALIZE binary :: Binary Concrete -> Prim Concrete   #-}-binary :: Backend sym => Binary sym -> GenValue sym-binary f = tlam $ \ ty ->-            lam $ \ a  -> return $-            lam $ \ b  -> do-               --io $ putStrLn "Entering a binary function"-               join (f ty <$> a <*> b)+binary :: Backend sym => Binary sym -> Prim sym+binary f = PTyPoly \ty ->+           PFun    \a  ->+           PFun    \b  ->+           PPrim $+             do x <- a+                y <- b+                f ty x y  type Unary sym = TValue -> GenValue sym -> SEval sym (GenValue sym) -{-# SPECIALIZE unary :: Unary Concrete -> GenValue Concrete+{-# SPECIALIZE unary :: Unary Concrete -> Prim Concrete   #-}-unary :: Backend sym => Unary sym -> GenValue sym-unary f = tlam $ \ ty ->-           lam $ \ a  -> f ty =<< a-+unary :: Backend sym => Unary sym -> Prim sym+unary f = PTyPoly \ty ->+          PFun    \a  ->+          PPrim (f ty =<< a)  type BinWord sym = Integer -> SWord sym -> SWord sym -> SEval sym (SWord sym) @@ -200,37 +216,41 @@       | isTBit a -> do                   lw <- fromVWord sym "ringLeft" l                   rw <- fromVWord sym "ringRight" r-                  return $ VWord w (WordVal <$> opw w lw rw)-      | otherwise -> VSeq w <$> (join (zipSeqMap (loop a) <$>+                  stk <- sGetCallStack sym+                  return $ VWord w (WordVal <$> (sWithCallStack sym stk (opw w lw rw)))+      | otherwise -> VSeq w <$> (join (zipSeqMap sym (loop a) <$>                                       (fromSeq "ringBinary left" l) <*>                                       (fromSeq "ringBinary right" r)))      TVStream a ->       -- streams-      VStream <$> (join (zipSeqMap (loop a) <$>+      VStream <$> (join (zipSeqMap sym (loop a) <$>                              (fromSeq "ringBinary left" l) <*>                              (fromSeq "ringBinary right" r)))      -- functions     TVFun _ ety ->-      return $ lam $ \ x -> loop' ety (fromVFun l x) (fromVFun r x)+      lam sym $ \ x -> loop' ety (fromVFun sym l x) (fromVFun sym r x)      -- tuples     TVTuple tys ->-      do ls <- mapM (sDelay sym Nothing) (fromVTuple l)-         rs <- mapM (sDelay sym Nothing) (fromVTuple r)+      do ls <- mapM (sDelay sym) (fromVTuple l)+         rs <- mapM (sDelay sym) (fromVTuple r)          return $ VTuple (zipWith3 loop' tys ls rs)      -- records     TVRec fs ->       do VRecord <$>             traverseRecordMap-              (\f fty -> sDelay sym Nothing (loop' fty (lookupRecord f l) (lookupRecord f r)))+              (\f fty -> sDelay sym (loop' fty (lookupRecord f l) (lookupRecord f r)))               fs      TVAbstract {} ->       evalPanic "ringBinary" ["Abstract type not in `Ring`"] +    TVNewtype {} ->+      evalPanic "ringBinary" ["Newtype not in `Ring`"]+ type UnaryWord sym = Integer -> SWord sym -> SEval sym (SWord sym)  @@ -282,30 +302,34 @@       -- words and finite sequences       | isTBit a -> do               wx <- fromVWord sym "ringUnary" v-              return $ VWord w (WordVal <$> opw w wx)-      | otherwise -> VSeq w <$> (mapSeqMap (loop a) =<< fromSeq "ringUnary" v)+              stk <- sGetCallStack sym+              return $ VWord w (WordVal <$> sWithCallStack sym stk (opw w wx))+      | otherwise -> VSeq w <$> (mapSeqMap sym (loop a) =<< fromSeq "ringUnary" v)      TVStream a ->-      VStream <$> (mapSeqMap (loop a) =<< fromSeq "ringUnary" v)+      VStream <$> (mapSeqMap sym (loop a) =<< fromSeq "ringUnary" v)      -- functions     TVFun _ ety ->-      return $ lam $ \ y -> loop' ety (fromVFun v y)+      lam sym $ \ y -> loop' ety (fromVFun sym v y)      -- tuples     TVTuple tys ->-      do as <- mapM (sDelay sym Nothing) (fromVTuple v)+      do as <- mapM (sDelay sym) (fromVTuple v)          return $ VTuple (zipWith loop' tys as)      -- records     TVRec fs ->       VRecord <$>         traverseRecordMap-          (\f fty -> sDelay sym Nothing (loop' fty (lookupRecord f v)))+          (\f fty -> sDelay sym (loop' fty (lookupRecord f v)))           fs      TVAbstract {} -> evalPanic "ringUnary" ["Abstract type not in `Ring`"] +    TVNewtype {} -> evalPanic "ringUnary" ["Newtype not in `Ring`"]++ {-# SPECIALIZE ringNullary ::   Concrete ->   (Integer -> SEval Concrete (SWord Concrete)) ->@@ -346,30 +370,35 @@          TVSeq w a           -- words and finite sequences-          | isTBit a -> pure $ VWord w $ (WordVal <$> opw w)+          | isTBit a ->+             do stk <- sGetCallStack sym+                pure $ VWord w $ (WordVal <$> sWithCallStack sym stk (opw w))           | otherwise ->-             do v <- sDelay sym Nothing (loop a)-                pure $ VSeq w $ IndexSeqMap $ const v+             do v <- sDelay sym (loop a)+                pure $ VSeq w $ IndexSeqMap \_i -> v          TVStream a ->-             do v <- sDelay sym Nothing (loop a)-                pure $ VStream $ IndexSeqMap $ const v+             do v <- sDelay sym (loop a)+                pure $ VStream $ IndexSeqMap \_i -> v          TVFun _ b ->-             do v <- sDelay sym Nothing (loop b)-                pure $ lam $ const $ v+             do v <- sDelay sym (loop b)+                lam sym (const v)          TVTuple tys ->-             do xs <- mapM (sDelay sym Nothing . loop) tys+             do xs <- mapM (sDelay sym . loop) tys                 pure $ VTuple xs          TVRec fs ->-             do xs <- traverse (sDelay sym Nothing . loop) fs+             do xs <- traverse (sDelay sym . loop) fs                 pure $ VRecord xs          TVAbstract {} ->           evalPanic "ringNullary" ["Abstract type not in `Ring`"] +        TVNewtype {} ->+          evalPanic "ringNullary" ["Newtype not in `Ring`"]+ {-# SPECIALIZE integralBinary :: Concrete -> BinWord Concrete ->       (SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->       Binary Concrete@@ -390,7 +419,8 @@       | isTBit a ->           do wl <- fromVWord sym "integralBinary left" l              wr <- fromVWord sym "integralBinary right" r-             return $ VWord w (WordVal <$> opw w wl wr)+             stk <- sGetCallStack sym+             return $ VWord w (WordVal <$> sWithCallStack sym stk (opw w wl wr))      _ -> evalPanic "integralBinary" [show ty ++ " not int class `Integral`"] @@ -398,15 +428,16 @@ --------------------------------------------------------------------------- -- Ring -{-# SPECIALIZE fromIntegerV :: Concrete -> GenValue Concrete+{-# SPECIALIZE fromIntegerV :: Concrete -> Prim Concrete   #-} -- | Convert an unbounded integer to a value in Ring-fromIntegerV :: Backend sym => sym -> GenValue sym+fromIntegerV :: Backend sym => sym -> Prim sym fromIntegerV sym =-  tlam $ \ a ->-  lam  $ \ v ->-  do i <- fromVInteger <$> v-     intV sym i a+  PTyPoly \a ->+  PFun    \v ->+  PPrim+    do i <- fromVInteger <$> v+       intV sym i a  {-# INLINE addV #-} addV :: Backend sym => sym -> Binary sym@@ -458,13 +489,14 @@     opw _w x y = wordDiv sym x y     opi x y = intDiv sym x y -{-# SPECIALIZE expV :: Concrete -> GenValue Concrete #-}-expV :: Backend sym => sym -> GenValue sym+{-# SPECIALIZE expV :: Concrete -> Prim Concrete #-}+expV :: Backend sym => sym -> Prim sym expV sym =-  tlam $ \aty ->-  tlam $ \ety ->-   lam $ \am -> return $-   lam $ \em ->+  PTyPoly \aty ->+  PTyPoly \ety ->+  PFun    \am ->+  PFun    \em ->+  PPrim      do a <- am         e <- em         case ety of@@ -522,12 +554,13 @@     opw _w x y = wordMod sym x y     opi x y = intMod sym x y -{-# SPECIALIZE toIntegerV :: Concrete -> GenValue Concrete #-}+{-# SPECIALIZE toIntegerV :: Concrete -> Prim Concrete #-} -- | Convert a word to a non-negative integer.-toIntegerV :: Backend sym => sym -> GenValue sym+toIntegerV :: Backend sym => sym -> Prim sym toIntegerV sym =-  tlam $ \a ->-  lam $ \v ->+  PTyPoly \a ->+  PFun    \v ->+  PPrim     case a of       TVSeq _w el | isTBit el ->         VInteger <$> (wordToInt sym =<< (fromVWord sym "toInteger" =<< v))@@ -537,11 +570,12 @@ ----------------------------------------------------------------------------- -- Field -{-# SPECIALIZE recipV :: Concrete -> GenValue Concrete #-}-recipV :: Backend sym => sym -> GenValue sym+{-# SPECIALIZE recipV :: Concrete -> Prim Concrete #-}+recipV :: Backend sym => sym -> Prim sym recipV sym =-  tlam $ \a ->-  lam $ \x ->+  PTyPoly \a ->+  PFun    \x ->+  PPrim     case a of       TVRational -> VRational <$> (rationalRecip sym . fromVRational =<< x)       TVFloat e p ->@@ -552,12 +586,13 @@       TVIntMod m -> VInteger <$> (znRecip sym m . fromVInteger =<< x)       _ -> evalPanic "recip"  [show a ++ "is not a Field"] -{-# SPECIALIZE fieldDivideV :: Concrete -> GenValue Concrete #-}-fieldDivideV :: Backend sym => sym -> GenValue sym+{-# SPECIALIZE fieldDivideV :: Concrete -> Prim Concrete #-}+fieldDivideV :: Backend sym => sym -> Prim sym fieldDivideV sym =-  tlam $ \a ->-  lam $ \x -> return $-  lam $ \y ->+  PTyPoly \a ->+  PFun    \x ->+  PFun    \y ->+  PPrim     case a of       TVRational ->         do x' <- fromVRational <$> x@@ -656,27 +691,27 @@ -- Bitvector signed div and modulus  {-# INLINE lg2V #-}-lg2V :: Backend sym => sym -> GenValue sym+lg2V :: Backend sym => sym -> Prim sym lg2V sym =-  nlam $ \(finNat' -> w) ->-  wlam sym $ \x -> return $-  VWord w (WordVal <$> wordLg2 sym x)+  PFinPoly \w ->+  PWordFun \x ->+  PVal (VWord w (WordVal <$> wordLg2 sym x)) -{-# SPECIALIZE sdivV :: Concrete -> GenValue Concrete #-}-sdivV :: Backend sym => sym -> GenValue sym+{-# SPECIALIZE sdivV :: Concrete -> Prim Concrete #-}+sdivV :: Backend sym => sym -> Prim sym sdivV sym =-  nlam $ \(finNat' -> w) ->-  wlam sym $ \x -> return $-  wlam sym $ \y -> return $-  VWord w (WordVal <$> wordSignedDiv sym x y)+  PFinPoly \w ->+  PWordFun \x ->+  PWordFun \y ->+  PVal (VWord w (WordVal <$> wordSignedDiv sym x y)) -{-# SPECIALIZE smodV :: Concrete -> GenValue Concrete #-}-smodV :: Backend sym => sym -> GenValue sym+{-# SPECIALIZE smodV :: Concrete -> Prim Concrete #-}+smodV :: Backend sym => sym -> Prim sym smodV sym  =-  nlam $ \(finNat' -> w) ->-  wlam sym $ \x -> return $-  wlam sym $ \y -> return $-  VWord w (WordVal <$> wordSignedMod sym x y)+  PFinPoly \w ->+  PWordFun \x ->+  PWordFun \y ->+  PVal (VWord w (WordVal <$> wordSignedMod sym x y))  -- Cmp ------------------------------------------------------------------------- @@ -733,6 +768,9 @@         TVAbstract {} -> evalPanic "cmpValue"                           [ "Abstract type not in `Cmp`" ] +        TVNewtype {} -> evalPanic "cmpValue"+                          [ "Newtype not in `Cmp`" ]+     cmpValues (t : ts) (x1 : xs1) (x2 : xs2) k =       do x1' <- x1          x2' <- x2@@ -879,30 +917,32 @@   TVSeq w ety       | isTBit ety -> pure $ word sym w 0       | otherwise  ->-           do z <- sDelay sym Nothing (zeroV sym ety)-              pure $ VSeq w (IndexSeqMap $ const z)+           do z <- sDelay sym (zeroV sym ety)+              pure $ VSeq w (IndexSeqMap \_i -> z)    TVStream ety ->-     do z <- sDelay sym Nothing (zeroV sym ety)-        pure $ VStream (IndexSeqMap $ const z)+     do z <- sDelay sym (zeroV sym ety)+        pure $ VStream (IndexSeqMap \_i -> z)    -- functions   TVFun _ bty ->-     do z <- sDelay sym Nothing (zeroV sym bty)-        pure $ lam (const z)+     do z <- sDelay sym (zeroV sym bty)+        lam sym (const z)    -- tuples   TVTuple tys ->-      do xs <- mapM (sDelay sym Nothing . zeroV sym) tys+      do xs <- mapM (sDelay sym . zeroV sym) tys          pure $ VTuple xs    -- records   TVRec fields ->-      do xs <- traverse (sDelay sym Nothing . zeroV sym) fields+      do xs <- traverse (sDelay sym . zeroV sym) fields          pure $ VRecord xs    TVAbstract {} -> evalPanic "zeroV" [ "Abstract type not in `Zero`" ] +  TVNewtype {} -> evalPanic "zeroV" [ "Newtype not in `Zero`" ]+ --  | otherwise = evalPanic "zeroV" ["invalid type for zero"]  {-# INLINE joinWordVal #-}@@ -936,7 +976,7 @@  where  loop :: SEval sym (WordValue sym) -> [SEval sym (GenValue sym)] -> SEval sym (GenValue sym)  loop !wv [] =-    VWord (nParts * nEach) <$> sDelay sym Nothing wv+    VWord (nParts * nEach) <$> sDelay sym wv  loop !wv (w : ws) =     w >>= \case       VWord _ w' ->@@ -1038,24 +1078,24 @@   case back of      Nat rightWidth | aBit -> do-          ws <- sDelay sym Nothing (splitWordVal sym leftWidth rightWidth =<< fromWordVal "splitAtV" val)+          ws <- sDelay sym (splitWordVal sym leftWidth rightWidth =<< fromWordVal "splitAtV" val)           return $ VTuple                    [ VWord leftWidth  . pure . fst <$> ws                    , VWord rightWidth . pure . snd <$> ws                    ]      Inf | aBit -> do-       vs <- sDelay sym Nothing (fromSeq "splitAtV" val)-       ls <- sDelay sym Nothing (fst . splitSeqMap leftWidth <$> vs)-       rs <- sDelay sym Nothing (snd . splitSeqMap leftWidth <$> vs)+       vs <- sDelay sym (fromSeq "splitAtV" val)+       ls <- sDelay sym (fst . splitSeqMap leftWidth <$> vs)+       rs <- sDelay sym (snd . splitSeqMap leftWidth <$> vs)        return $ VTuple [ return $ VWord leftWidth (LargeBitsVal leftWidth <$> ls)                        , VStream <$> rs                        ]      _ -> do-       vs <- sDelay sym Nothing (fromSeq "splitAtV" val)-       ls <- sDelay sym Nothing (fst . splitSeqMap leftWidth <$> vs)-       rs <- sDelay sym Nothing (snd . splitSeqMap leftWidth <$> vs)+       vs <- sDelay sym (fromSeq "splitAtV" val)+       ls <- sDelay sym (fst . splitSeqMap leftWidth <$> vs)+       rs <- sDelay sym (snd . splitSeqMap leftWidth <$> vs)        return $ VTuple [ VSeq leftWidth <$> ls                        , mkSeq back a <$> rs                        ]@@ -1093,19 +1133,20 @@ {-# INLINE ecSplitV #-}  -- | Split implementation.-ecSplitV :: Backend sym => sym -> GenValue sym+ecSplitV :: Backend sym => sym -> Prim sym ecSplitV sym =-  nlam $ \ parts ->-  nlam $ \ each  ->-  tlam $ \ a     ->-  lam  $ \ val ->+  PNumPoly \parts ->+  PNumPoly \each ->+  PTyPoly  \a ->+  PFun     \val ->+  PPrim     case (parts, each) of        (Nat p, Nat e) | isTBit a -> do           ~(VWord _ val') <- val           return $ VSeq p $ IndexSeqMap $ \i ->             pure $ VWord e (extractWordVal sym e ((p-i-1)*e) =<< val')        (Inf, Nat e) | isTBit a -> do-          val' <- sDelay sym Nothing (fromSeq "ecSplitV" =<< val)+          val' <- sDelay sym (fromSeq "ecSplitV" =<< val)           return $ VStream $ IndexSeqMap $ \i ->             return $ VWord e $ return $ LargeBitsVal e $ IndexSeqMap $ \j ->               let idx = i*e + toInteger j@@ -1113,13 +1154,13 @@                       xs <- val'                       lookupSeqMap xs idx        (Nat p, Nat e) -> do-          val' <- sDelay sym Nothing (fromSeq "ecSplitV" =<< val)+          val' <- sDelay sym (fromSeq "ecSplitV" =<< val)           return $ VSeq p $ IndexSeqMap $ \i ->             return $ VSeq e $ IndexSeqMap $ \j -> do               xs <- val'               lookupSeqMap xs (e * i + j)        (Inf  , Nat e) -> do-          val' <- sDelay sym Nothing (fromSeq "ecSplitV" =<< val)+          val' <- sDelay sym (fromSeq "ecSplitV" =<< val)           return $ VStream $ IndexSeqMap $ \i ->             return $ VSeq e $ IndexSeqMap $ \j -> do               xs <- val'@@ -1157,7 +1198,8 @@   | isTBit c, Nat na <- a = -- Fin a => [a][b]Bit -> [b][a]Bit       return $ bseq $ IndexSeqMap $ \bi ->         return $ VWord na $ return $ LargeBitsVal na $ IndexSeqMap $ \ai ->-         do ys <- flip lookupSeqMap (toInteger ai) =<< fromSeq "transposeV" xs+         do xs' <- fromSeq "transposeV" xs+            ys <- lookupSeqMap xs' ai             case ys of               VStream ys' -> lookupSeqMap ys' bi               VWord _ wv  -> VBit <$> (flip (indexWordValue sym) bi =<< wv)@@ -1166,7 +1208,8 @@   | isTBit c, Inf <- a = -- [inf][b]Bit -> [b][inf]Bit       return $ bseq $ IndexSeqMap $ \bi ->         return $ VStream $ IndexSeqMap $ \ai ->-         do ys <- flip lookupSeqMap ai =<< fromSeq "transposeV" xs+         do xs' <- fromSeq "transposeV" xs+            ys  <- lookupSeqMap xs' ai             case ys of               VStream ys' -> lookupSeqMap ys' bi               VWord _ wv  -> VBit <$> (flip (indexWordValue sym) bi =<< wv)@@ -1175,8 +1218,9 @@   | otherwise = -- [a][b]c -> [b][a]c       return $ bseq $ IndexSeqMap $ \bi ->         return $ aseq $ IndexSeqMap $ \ai -> do-          ys  <- flip lookupSeqMap ai =<< fromSeq "transposeV 1" xs-          z   <- flip lookupSeqMap bi =<< fromSeq "transposeV 2" ys+          xs' <- fromSeq "transposeV 1" xs+          ys  <- fromSeq "transposeV 2" =<< lookupSeqMap xs' ai+          z   <- lookupSeqMap ys bi           return z   where@@ -1206,7 +1250,7 @@   return $ VWord (m+n) (join (joinWordVal sym <$> l <*> r))  ccatV sym _front _back _elty (VWord m l) (VStream r) = do-  l' <- sDelay sym Nothing l+  l' <- sDelay sym l   return $ VStream $ IndexSeqMap $ \i ->     if i < m then       VBit <$> (flip (indexWordValue sym) i =<< l')@@ -1214,8 +1258,8 @@       lookupSeqMap r (i-m)  ccatV sym front back elty l r = do-       l'' <- sDelay sym Nothing (fromSeq "ccatV left" l)-       r'' <- sDelay sym Nothing (fromSeq "ccatV right" r)+       l'' <- sDelay sym (fromSeq "ccatV left" l)+       r'' <- sDelay sym (fromSeq "ccatV right" r)        let Nat n = front        mkSeq (evalTF TCAdd [front,back]) elty <$> return (IndexSeqMap $ \i ->         if i < n then do@@ -1238,7 +1282,7 @@ wordValLogicOp _sym _ wop (WordVal w1) (WordVal w2) = WordVal <$> wop w1 w2  wordValLogicOp sym bop _ w1 w2 = LargeBitsVal (wordValueSize sym w1) <$> zs-     where zs = memoMap $ IndexSeqMap $ \i -> join (op <$> (lookupSeqMap xs i) <*> (lookupSeqMap ys i))+     where zs = memoMap sym $ IndexSeqMap $ \i -> join (op <$> (lookupSeqMap xs i) <*> (lookupSeqMap ys i))            xs = asBitsMap sym w1            ys = asBitsMap sym w2            op x y = VBit <$> (bop (fromVBit x) (fromVBit y))@@ -1281,7 +1325,7 @@     TVSeq w aty          -- words          | isTBit aty-              -> do v <- sDelay sym Nothing $ join+              -> do v <- sDelay sym $ join                             (wordValLogicOp sym opb opw <$>                                     fromWordVal "logicBinary l" l <*>                                     fromWordVal "logicBinary r" r)@@ -1289,41 +1333,45 @@           -- finite sequences          | otherwise -> VSeq w <$>-                           (join (zipSeqMap (loop aty) <$>+                           (join (zipSeqMap sym (loop aty) <$>                                     (fromSeq "logicBinary left" l)                                     <*> (fromSeq "logicBinary right" r)))      TVStream aty ->-        VStream <$> (join (zipSeqMap (loop aty) <$>+        VStream <$> (join (zipSeqMap sym (loop aty) <$>                           (fromSeq "logicBinary left" l) <*>                           (fromSeq "logicBinary right" r)))      TVTuple etys -> do-        ls <- mapM (sDelay sym Nothing) (fromVTuple l)-        rs <- mapM (sDelay sym Nothing) (fromVTuple r)+        ls <- mapM (sDelay sym) (fromVTuple l)+        rs <- mapM (sDelay sym) (fromVTuple r)         return $ VTuple $ zipWith3 loop' etys ls rs      TVFun _ bty ->-        return $ lam $ \ a -> loop' bty (fromVFun l a) (fromVFun r a)+        lam sym $ \ a -> loop' bty (fromVFun sym l a) (fromVFun sym r a)      TVRec fields ->       VRecord <$>         traverseRecordMap-          (\f fty -> sDelay sym Nothing (loop' fty (lookupRecord f l) (lookupRecord f r)))+          (\f fty -> sDelay sym (loop' fty (lookupRecord f l) (lookupRecord f r)))           fields      TVAbstract {} -> evalPanic "logicBinary"                         [ "Abstract type not in `Logic`" ] +    TVNewtype {} -> evalPanic "logicBinary"+                        [ "Newtype not in `Logic`" ]+ {-# INLINE wordValUnaryOp #-} wordValUnaryOp ::   Backend sym =>+  sym ->   (SBit sym -> SEval sym (SBit sym)) ->   (SWord sym -> SEval sym (SWord sym)) ->   WordValue sym ->   SEval sym (WordValue sym)-wordValUnaryOp _ wop (WordVal w)  = WordVal <$> (wop w)-wordValUnaryOp bop _ (LargeBitsVal n xs) = LargeBitsVal n <$> mapSeqMap f xs+wordValUnaryOp _ _ wop (WordVal w)  = WordVal <$> (wop w)+wordValUnaryOp sym bop _ (LargeBitsVal n xs) = LargeBitsVal n <$> mapSeqMap sym f xs   where f x = VBit <$> (bop (fromVBit x))  {-# SPECIALIZE logicUnary ::@@ -1357,32 +1405,33 @@     TVSeq w ety          -- words          | isTBit ety-              -> do v <- sDelay sym Nothing (wordValUnaryOp opb opw =<< fromWordVal "logicUnary" val)+              -> do v <- sDelay sym (wordValUnaryOp sym opb opw =<< fromWordVal "logicUnary" val)                     return $ VWord w v           -- finite sequences          | otherwise-              -> VSeq w <$> (mapSeqMap (loop ety) =<< fromSeq "logicUnary" val)+              -> VSeq w <$> (mapSeqMap sym (loop ety) =<< fromSeq "logicUnary" val)           -- streams     TVStream ety ->-         VStream <$> (mapSeqMap (loop ety) =<< fromSeq "logicUnary" val)+         VStream <$> (mapSeqMap sym (loop ety) =<< fromSeq "logicUnary" val)      TVTuple etys ->-      do as <- mapM (sDelay sym Nothing) (fromVTuple val)+      do as <- mapM (sDelay sym) (fromVTuple val)          return $ VTuple (zipWith loop' etys as)      TVFun _ bty ->-      return $ lam $ \ a -> loop' bty (fromVFun val a)+      lam sym $ \ a -> loop' bty (fromVFun sym val a)      TVRec fields ->       VRecord <$>         traverseRecordMap-          (\f fty -> sDelay sym Nothing (loop' fty (lookupRecord f val)))+          (\f fty -> sDelay sym (loop' fty (lookupRecord f val)))           fields      TVAbstract {} -> evalPanic "logicUnary" [ "Abstract type not in `Logic`" ] +    TVNewtype {} -> evalPanic "logicUnary" [ "Newtype not in `Logic`" ]  {-# SPECIALIZE bitsValueLessThan ::   Concrete ->@@ -1471,14 +1520,15 @@   (Nat' -> TValue -> SeqMap sym -> TValue -> SInteger sym -> SEval sym (GenValue sym)) ->   (Nat' -> TValue -> SeqMap sym -> TValue -> [SBit sym] -> SEval sym (GenValue sym)) ->   (Nat' -> TValue -> SeqMap sym -> TValue -> SWord sym -> SEval sym (GenValue sym)) ->-  GenValue sym+  Prim sym indexPrim sym int_op bits_op word_op =-  nlam $ \ len  ->-  tlam $ \ eltTy ->-  tlam $ \ ix ->-   lam $ \ xs  -> return $-   lam $ \ idx  -> do-      vs <- xs >>= \case+  PNumPoly \len ->+  PTyPoly  \eltTy ->+  PTyPoly  \ix ->+  PFun     \xs ->+  PFun     \idx ->+  PPrim+   do vs <- xs >>= \case                VWord _ w  -> w >>= \w' -> return $ IndexSeqMap (\i -> VBit <$> indexWordValue sym w' i)                VSeq _ vs  -> return vs                VStream vs -> return vs@@ -1486,7 +1536,7 @@       idx' <- asIndex sym "index" ix =<< idx       assertIndexInBounds sym len idx'       case idx' of-        Left i                    -> int_op len eltTy vs ix i+        Left i                    -> int_op  len eltTy vs ix i         Right (WordVal w')        -> word_op len eltTy vs ix w'         Right (LargeBitsVal m bs) -> bits_op len eltTy vs ix =<< traverse (fromVBit <$>) (enumerateSeqMap m bs) @@ -1497,31 +1547,33 @@   sym ->   (Nat' -> TValue -> WordValue sym -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (WordValue sym)) ->   (Nat' -> TValue -> SeqMap sym    -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (SeqMap sym)) ->-  GenValue sym+  Prim sym updatePrim sym updateWord updateSeq =-  nlam $ \len ->-  tlam $ \eltTy ->-  tlam $ \ix ->-  lam $ \xs  -> return $-  lam $ \idx -> return $-  lam $ \val -> do-    idx' <- asIndex sym "update" ix =<< idx-    assertIndexInBounds sym len idx'-    xs >>= \case-      VWord l w  -> do w' <- sDelay sym Nothing w-                       return $ VWord l (w' >>= \w'' -> updateWord len eltTy w'' idx' val)-      VSeq l vs  -> VSeq l  <$> updateSeq len eltTy vs idx' val-      VStream vs -> VStream <$> updateSeq len eltTy vs idx' val-      _ -> evalPanic "Expected sequence value" ["updatePrim"]+  PNumPoly \len ->+  PTyPoly  \eltTy ->+  PTyPoly  \ix ->+  PFun     \xs ->+  PFun     \idx ->+  PFun     \val ->+  PPrim+   do idx' <- asIndex sym "update" ix =<< idx+      assertIndexInBounds sym len idx'+      xs >>= \case+        VWord l w  -> do w' <- sDelay sym w+                         return $ VWord l (w' >>= \w'' -> updateWord len eltTy w'' idx' val)+        VSeq l vs  -> VSeq l  <$> updateSeq len eltTy vs idx' val+        VStream vs -> VStream <$> updateSeq len eltTy vs idx' val+        _ -> evalPanic "Expected sequence value" ["updatePrim"]  {-# INLINE fromToV #-}  -- @[ 0 .. 10 ]@-fromToV :: Backend sym => sym -> GenValue sym+fromToV :: Backend sym => sym -> Prim sym fromToV sym =-  nlam $ \ first ->-  nlam $ \ lst   ->-  tlam $ \ ty    ->+  PNumPoly \first ->+  PNumPoly \lst ->+  PTyPoly  \ty ->+  PVal     let !f = mkLit sym ty in     case (first, lst) of       (Nat first', Nat lst') ->@@ -1529,16 +1581,32 @@         in VSeq len $ IndexSeqMap $ \i -> f (first' + i)       _ -> evalPanic "fromToV" ["invalid arguments"] +{-# INLINE fromToLessThanV #-}++-- @[ 0 .. <10 ]@+fromToLessThanV :: Backend sym => sym -> Prim sym+fromToLessThanV sym =+  PFinPoly \first ->+  PNumPoly \bound ->+  PTyPoly  \ty ->+  PVal+    let !f = mkLit sym ty+        ss = IndexSeqMap $ \i -> f (first + i)+    in case bound of+         Inf        -> VStream ss+         Nat bound' -> VSeq (bound' - first) ss+ {-# INLINE fromThenToV #-}  -- @[ 0, 1 .. 10 ]@-fromThenToV :: Backend sym => sym -> GenValue sym+fromThenToV :: Backend sym => sym -> Prim sym fromThenToV sym =-  nlam $ \ first ->-  nlam $ \ next  ->-  nlam $ \ lst   ->-  tlam $ \ ty    ->-  nlam $ \ len   ->+  PNumPoly \first ->+  PNumPoly \next  ->+  PNumPoly \lst   ->+  PTyPoly  \ty    ->+  PNumPoly \len   ->+  PVal     let !f = mkLit sym ty in     case (first, next, lst, len) of       (Nat first', Nat next', Nat _lst', Nat len') ->@@ -1547,31 +1615,33 @@       _ -> evalPanic "fromThenToV" ["invalid arguments"]  {-# INLINE infFromV #-}-infFromV :: Backend sym => sym -> GenValue sym+infFromV :: Backend sym => sym -> Prim sym infFromV sym =-  tlam $ \ ty ->-  lam  $ \ x ->-  do mx <- sDelay sym Nothing x-     return $ VStream $ IndexSeqMap $ \i ->-       do x' <- mx-          i' <- integerLit sym i-          addV sym ty x' =<< intV sym i' ty+  PTyPoly \ty ->+  PFun    \x ->+  PPrim+    do mx <- sDelay sym x+       return $ VStream $ IndexSeqMap $ \i ->+         do x' <- mx+            i' <- integerLit sym i+            addV sym ty x' =<< intV sym i' ty  {-# INLINE infFromThenV #-}-infFromThenV :: Backend sym => sym -> GenValue sym+infFromThenV :: Backend sym => sym -> Prim sym infFromThenV sym =-  tlam $ \ ty ->-  lam $ \ first -> return $-  lam $ \ next ->-  do mxd <- sDelay sym Nothing-             (do x <- first-                 y <- next-                 d <- subV sym ty y x-                 pure (x,d))-     return $ VStream $ IndexSeqMap $ \i -> do-       (x,d) <- mxd-       i' <- integerLit sym i-       addV sym ty x =<< mulV sym ty d =<< intV sym i' ty+  PTyPoly \ty ->+  PFun    \first ->+  PFun    \next ->+  PPrim+    do mxd <- sDelay sym+               (do x <- first+                   y <- next+                   d <- subV sym ty y x+                   pure (x,d))+       return $ VStream $ IndexSeqMap $ \i -> do+         (x,d) <- mxd+         i' <- integerLit sym i+         addV sym ty x =<< mulV sym ty d =<< intV sym i' ty  -- Shifting --------------------------------------------------- @@ -1596,7 +1666,7 @@      | otherwise     = do x_shft <- shift_op x (2 ^ length bs)-         x' <- memoMap (mergeSeqMap sym b x_shft x)+         x' <- memoMap sym (mergeSeqMap sym b x_shft x)          go x' bs  {-# INLINE shiftLeftReindex #-}@@ -1670,13 +1740,14 @@      {- ^ reindexing operation for positive indices (sequence size, starting index, shift amount -} ->   (Nat' -> Integer -> Integer -> Maybe Integer)      {- ^ reindexing operation for negative indices (sequence size, starting index, shift amount -} ->-  GenValue sym+  Prim sym logicShift sym nm shrinkRange wopPos wopNeg reindexPos reindexNeg =-  nlam $ \m ->-  tlam $ \ix ->-  tlam $ \a ->-  VFun $ \xs -> return $-  VFun $ \y ->+  PNumPoly \m ->+  PTyPoly  \ix ->+  PTyPoly  \a ->+  PFun     \xs ->+  PFun     \y ->+  PPrim     do xs' <- xs        y' <- asIndex sym "shift" ix =<< y        case y' of@@ -1701,7 +1772,7 @@    SEval sym (GenValue sym) intShifter sym nm wop reindex m ix a xs idx =    do let shiftOp vs shft =-              memoMap $ IndexSeqMap $ \i ->+              memoMap sym $ IndexSeqMap $ \i ->                 case reindex m i shft of                   Nothing -> zeroV sym a                   Just i' -> lookupSeqMap vs i'@@ -1737,7 +1808,7 @@    SEval sym (GenValue sym) wordShifter sym nm wop reindex m a xs idx =   let shiftOp vs shft =-          memoMap $ IndexSeqMap $ \i ->+          memoMap sym $ IndexSeqMap $ \i ->             case reindex m i shft of               Nothing -> zeroV sym a               Just i' -> lookupSeqMap vs i'@@ -1789,37 +1860,38 @@   TValue ->   String ->   SEval sym (GenValue sym)-errorV sym ty msg = case ty of-  -- bits-  TVBit -> cryUserError sym msg-  TVInteger -> cryUserError sym msg-  TVIntMod _ -> cryUserError sym msg-  TVRational -> cryUserError sym msg-  TVArray{} -> cryUserError sym msg-  TVFloat {} -> cryUserError sym msg+errorV sym ty0 msg =+     do stk <- sGetCallStack sym+        loop stk ty0+  where+  err stk = sWithCallStack sym stk (cryUserError sym msg) -  -- sequences-  TVSeq w ety-     | isTBit ety -> return $ VWord w $ return $ LargeBitsVal w $ IndexSeqMap $ \_ -> cryUserError sym msg-     | otherwise  -> return $ VSeq w (IndexSeqMap $ \_ -> errorV sym ety msg)+  loop stk = \case+       TVBit -> err stk+       TVInteger -> err stk+       TVIntMod _ -> err stk+       TVRational -> err stk+       TVArray{} -> err stk+       TVFloat {} -> err stk -  TVStream ety ->-    return $ VStream (IndexSeqMap $ \_ -> errorV sym ety msg)+       -- sequences+       TVSeq w ety+          | isTBit ety -> return $ VWord w $ return $ LargeBitsVal w $ IndexSeqMap $ \_ -> err stk+          | otherwise  -> return $ VSeq w $ IndexSeqMap $ \_ -> loop stk ety -  -- functions-  TVFun _ bty ->-    return $ lam (\ _ -> errorV sym bty msg)+       TVStream ety -> return $ VStream $ IndexSeqMap $ \_ -> loop stk ety -  -- tuples-  TVTuple tys ->-    return $ VTuple (map (\t -> errorV sym t msg) tys)+       -- functions+       TVFun _ bty -> lam sym (\ _ -> loop stk bty) -  -- records-  TVRec fields ->-    return $ VRecord $ fmap (\t -> errorV sym t msg) $ fields+       -- tuples+       TVTuple tys -> return $ VTuple (map (\t -> loop stk t) tys) -  TVAbstract {} -> cryUserError sym msg+       -- records+       TVRec fields -> return $ VRecord $ fmap (\t -> loop stk t) $ fields +       TVAbstract {} -> err stk+       TVNewtype {} -> err stk  {-# INLINE valueToChar #-} @@ -1862,7 +1934,7 @@ mergeWord sym c (WordVal w1) (WordVal w2) =   WordVal <$> iteWord sym c w1 w2 mergeWord sym c w1 w2 =-  LargeBitsVal (wordValueSize sym w1) <$> memoMap (mergeSeqMap sym c (asBitsMap sym w1) (asBitsMap sym w2))+  LargeBitsVal (wordValueSize sym w1) <$> memoMap sym (mergeSeqMap sym c (asBitsMap sym w1) (asBitsMap sym w2))  {-# INLINE mergeWord' #-} mergeWord' :: Backend sym =>@@ -1900,11 +1972,12 @@     (VBit b1     , VBit b2     ) -> VBit <$> iteBit sym c b1 b2     (VInteger i1 , VInteger i2 ) -> VInteger <$> iteInteger sym c i1 i2     (VRational q1, VRational q2) -> VRational <$> iteRational sym c q1 q2+    (VFloat f1   , VFloat f2)    -> VFloat <$> iteFloat sym c f1 f2     (VWord n1 w1 , VWord n2 w2 ) | n1 == n2 -> pure $ VWord n1 $ mergeWord' sym c w1 w2-    (VSeq n1 vs1 , VSeq n2 vs2 ) | n1 == n2 -> VSeq n1 <$> memoMap (mergeSeqMap sym c vs1 vs2)-    (VStream vs1 , VStream vs2 ) -> VStream <$> memoMap (mergeSeqMap sym c vs1 vs2)-    (VFun f1     , VFun f2     ) -> pure $ VFun $ \x -> mergeValue' sym c (f1 x) (f2 x)-    (VPoly f1    , VPoly f2    ) -> pure $ VPoly $ \x -> mergeValue' sym c (f1 x) (f2 x)+    (VSeq n1 vs1 , VSeq n2 vs2 ) | n1 == n2 -> VSeq n1 <$> memoMap sym (mergeSeqMap sym c vs1 vs2)+    (VStream vs1 , VStream vs2 ) -> VStream <$> memoMap sym (mergeSeqMap sym c vs1 vs2)+    (f1@VFun{}   , f2@VFun{}   ) -> lam sym $ \x -> mergeValue' sym c (fromVFun sym f1 x) (fromVFun sym f2 x)+    (f1@VPoly{}  , f2@VPoly{}  ) -> tlam sym $ \x -> mergeValue' sym c (fromVPoly sym f1 x) (fromVPoly sym f2 x)     (_           , _           ) -> panic "Cryptol.Eval.Generic"                                   [ "mergeValue: incompatible values" ] @@ -1921,53 +1994,55 @@   -foldlV :: Backend sym => sym -> GenValue sym+foldlV :: Backend sym => sym -> Prim sym foldlV sym =-  ilam $ \_n ->-  tlam $ \_a ->-  tlam $ \_b ->-  lam $ \f -> pure $-  lam $ \z -> pure $-  lam $ \v ->-    v >>= \case+  PNumPoly \_n ->+  PTyPoly  \_a ->+  PTyPoly  \_b ->+  PFun     \f ->+  PFun     \z ->+  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)       _ -> panic "Cryptol.Eval.Generic.foldlV" ["Expected finite sequence"]   where   go0 _f a [] = a   go0 f a bs =-    do f' <- fromVFun <$> f+    do f' <- fromVFun sym <$> f        go1 f' a bs    go1 _f a [] = a   go1 f a (b:bs) =-    do f' <- fromVFun <$> (f a)+    do f' <- fromVFun sym <$> (f a)        go1 f (f' b) bs -foldl'V :: Backend sym => sym -> GenValue sym+foldl'V :: Backend sym => sym -> Prim sym foldl'V sym =-  ilam $ \_n ->-  tlam $ \_a ->-  tlam $ \_b ->-  lam $ \f -> pure $-  lam $ \z -> pure $-  lam $ \v ->-    v >>= \case+  PNumPoly \_n ->+  PTyPoly  \_a ->+  PTyPoly  \_b ->+  PFun     \f ->+  PFun     \z ->+  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)       _ -> panic "Cryptol.Eval.Generic.foldlV" ["Expected finite sequence"]   where   go0 _f a [] = a   go0 f a bs =-    do f' <- fromVFun <$> f-       a' <- sDelay sym Nothing a+    do f' <- fromVFun sym <$> f+       a' <- sDelay sym a        forceValue =<< a'        go1 f' a' bs    go1 _f a [] = a   go1 f a (b:bs) =-    do f' <- fromVFun <$> (f a)-       a' <- sDelay sym Nothing (f' b)+    do f' <- fromVFun sym <$> (f a)+       a' <- sDelay sym (f' b)        forceValue =<< a'        go1 f a' bs @@ -1994,14 +2069,15 @@ -------------------------------------------------------------------------------- -- Experimental parallel primitives -parmapV :: Backend sym => sym -> GenValue sym+parmapV :: Backend sym => sym -> Prim sym parmapV sym =-  tlam $ \_a ->-  tlam $ \_b ->-  ilam $ \_n ->-  lam $ \f -> pure $-  lam $ \xs ->-    do f' <- fromVFun <$> f+  PTyPoly \_a ->+  PTyPoly \_b ->+  PFinPoly \_n ->+  PFun \f ->+  PFun \xs ->+  PPrim+    do f' <- fromVFun sym <$> f        xs' <- xs        case xs' of           VWord n w ->@@ -2022,25 +2098,35 @@   SeqMap sym ->   SEval sym (SeqMap sym) sparkParMap sym f n m =-  finiteSeqMap sym <$> mapM (sSpark sym . g) (enumerateSeqMap n m)+  finiteSeqMap <$> mapM (sSpark sym . g) (enumerateSeqMap n m)  where  g x =-   do z <- sDelay sym Nothing (f x)+   do z <- sDelay sym (f x)       forceValue =<< z       z  -------------------------------------------------------------------------------- -- Floating Point Operations +-- | A helper for definitng floating point constants.+fpConst ::+  Backend sym =>+  (Integer -> Integer -> SEval sym (SFloat sym)) ->+  Prim sym+fpConst mk =+  PFinPoly \e ->+  PNumPoly \ ~(Nat p) ->+  PPrim (VFloat <$> mk e p)+ -- | Make a Cryptol value for a binary arithmetic function.-fpBinArithV :: Backend sym => sym -> FPArith2 sym -> GenValue sym+fpBinArithV :: Backend sym => sym -> FPArith2 sym -> Prim sym fpBinArithV sym fun =-  ilam \_ ->-  ilam \_ ->-  wlam sym \r ->-  pure $ flam \x ->-  pure $ flam \y ->-  VFloat <$> fun sym r x y+  PFinPoly  \_e ->+  PFinPoly  \_p ->+  PWordFun  \r ->+  PFloatFun \x ->+  PFloatFun \y ->+  PPrim (VFloat <$> fun sym r x y)  -- | Rounding mode used in FP operations that do not specify it explicitly. fpRndMode, fpRndRNE, fpRndRNA, fpRndRTP, fpRndRTN, fpRndRTZ ::@@ -2051,3 +2137,266 @@ fpRndRTP sym = wordLit sym 3 2 {- to +inf -} fpRndRTN sym = wordLit sym 3 3 {- to -inf -} fpRndRTZ sym = wordLit sym 3 4 {- to 0    -}+++{-# SPECIALIZE genericFloatTable :: Concrete -> Map PrimIdent (Prim Concrete) #-}++genericFloatTable :: Backend sym => sym -> Map PrimIdent (Prim sym)+genericFloatTable sym =+  let (~>) = (,) in+  Map.fromList $ map (\(n, v) -> (floatPrim n, v))+    [ "fpNaN"       ~> fpConst (fpNaN sym)+    , "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 -> PVal+                            $ VWord (e+p)+                            $ WordVal <$> fpToBits sym x+    , "=.="         ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x -> PFloatFun \y ->+                       PPrim (VBit <$> fpLogicalEq sym x y)++    , "fpIsNaN"     ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x ->+                       PPrim (VBit <$> fpIsNaN sym x)+    , "fpIsInf"     ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x ->+                       PPrim (VBit <$> fpIsInf sym x)+    , "fpIsZero"    ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x ->+                       PPrim (VBit <$> fpIsZero sym x)+    , "fpIsNeg"     ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x ->+                       PPrim (VBit <$> fpIsNeg sym x)+    , "fpIsNormal"  ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x ->+                       PPrim (VBit <$> fpIsNorm sym x)+    , "fpIsSubnormal" ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x ->+                         PPrim (VBit <$> fpIsSubnorm sym x)++    , "fpAdd"       ~> fpBinArithV sym fpPlus+    , "fpSub"       ~> fpBinArithV sym fpMinus+    , "fpMul"       ~> fpBinArithV sym fpMult+    , "fpDiv"       ~> fpBinArithV sym fpDiv+    , "fpFMA"       ~> PFinPoly \_ -> PFinPoly \_ -> PWordFun \r ->+                       PFloatFun \x -> PFloatFun \y -> PFloatFun \z ->+                       PPrim (VFloat <$> fpFMA sym r x y z)++    , "fpAbs"       ~> PFinPoly \_ -> PFinPoly \_ ->+                       PFloatFun \x ->+                       PPrim (VFloat <$> fpAbs sym x)++    , "fpSqrt"      ~> PFinPoly \_ -> PFinPoly \_ ->+                       PWordFun \r -> PFloatFun \x ->+                       PPrim (VFloat <$> fpSqrt sym r x)++    , "fpToRational" ~>+       PFinPoly \_e -> PFinPoly \_p -> PFloatFun \x ->+       PPrim (VRational <$> fpToRational sym x)++    , "fpFromRational" ~>+       PFinPoly \e -> PFinPoly \p -> PWordFun \r -> PFun \x ->+       PPrim+         do rat <- fromVRational <$> x+            VFloat <$> fpFromRational sym e p r rat++    ]+++{-# SPECIALIZE genericPrimTable :: Concrete -> IO EvalOpts -> Map PrimIdent (Prim Concrete) #-}++genericPrimTable :: Backend sym => sym -> IO EvalOpts -> Map PrimIdent (Prim sym)+genericPrimTable sym getEOpts =+  Map.fromList $ map (\(n, v) -> (prelPrim n, v))++  [ -- Literals+    ("True"       , PVal $ VBit (bitLit sym True))+  , ("False"      , PVal $ VBit (bitLit sym False))+  , ("number"     , {-# SCC "Prelude::number" #-}+                    ecNumberV sym)+  , ("ratio"      , {-# SCC "Prelude::ratio" #-}+                    ratioV sym)+  , ("fraction"   , ecFractionV sym)++    -- Zero+  , ("zero"       , {-# SCC "Prelude::zero" #-}+                    PTyPoly \ty ->+                    PPrim (zeroV sym ty))++    -- Logic+  , ("&&"         , {-# SCC "Prelude::(&&)" #-}+                    binary (andV sym))+  , ("||"         , {-# SCC "Prelude::(||)" #-}+                    binary (orV sym))+  , ("^"          , {-# SCC "Prelude::(^)" #-}+                    binary (xorV sym))+  , ("complement" , {-# SCC "Prelude::complement" #-}+                    unary  (complementV sym))++    -- Ring+  , ("fromInteger", {-# SCC "Prelude::fromInteger" #-}+                    fromIntegerV sym)+  , ("+"          , {-# SCC "Prelude::(+)" #-}+                    binary (addV sym))+  , ("-"          , {-# SCC "Prelude::(-)" #-}+                    binary (subV sym))+  , ("*"          , {-# SCC "Prelude::(*)" #-}+                    binary (mulV sym))+  , ("negate"     , {-# SCC "Prelude::negate" #-}+                    unary (negateV sym))++    -- Integral+  , ("toInteger"  , {-# SCC "Prelude::toInteger" #-}+                    toIntegerV sym)+  , ("/"          , {-# SCC "Prelude::(/)" #-}+                    binary (divV sym))+  , ("%"          , {-# SCC "Prelude::(%)" #-}+                    binary (modV sym))+  , ("^^"         , {-# SCC "Prelude::(^^)" #-}+                    expV sym)+  , ("infFrom"    , {-# SCC "Prelude::infFrom" #-}+                    infFromV sym)+  , ("infFromThen", {-# SCC "Prelude::infFromThen" #-}+                    infFromThenV sym)++    -- Field+  , ("recip"      , {-# SCC "Prelude::recip" #-}+                    recipV sym)+  , ("/."         , {-# SCC "Prelude::(/.)" #-}+                    fieldDivideV sym)++    -- Round+  , ("floor"      , {-# SCC "Prelude::floor" #-}+                    unary (floorV sym))+  , ("ceiling"    , {-# SCC "Prelude::ceiling" #-}+                    unary (ceilingV sym))+  , ("trunc"      , {-# SCC "Prelude::trunc" #-}+                    unary (truncV sym))+  , ("roundAway"  , {-# SCC "Prelude::roundAway" #-}+                    unary (roundAwayV sym))+  , ("roundToEven", {-# SCC "Prelude::roundToEven" #-}+                    unary (roundToEvenV sym))++    -- Bitvector specific operations+  , ("/$"         , {-# SCC "Prelude::(/$)" #-}+                    sdivV sym)+  , ("%$"         , {-# SCC "Prelude::(%$)" #-}+                    smodV sym)+  , ("lg2"        , {-# SCC "Prelude::lg2" #-}+                    lg2V sym)++    -- Cmp+  , ("<"          , {-# SCC "Prelude::(<)" #-}+                    binary (lessThanV sym))+  , (">"          , {-# SCC "Prelude::(>)" #-}+                    binary (greaterThanV sym))+  , ("<="         , {-# SCC "Prelude::(<=)" #-}+                    binary (lessThanEqV sym))+  , (">="         , {-# SCC "Prelude::(>=)" #-}+                    binary (greaterThanEqV sym))+  , ("=="         , {-# SCC "Prelude::(==)" #-}+                    binary (eqV sym))+  , ("!="         , {-# SCC "Prelude::(!=)" #-}+                    binary (distinctV sym))++    -- SignedCmp+  , ("<$"         , {-# SCC "Prelude::(<$)" #-}+                    binary (signedLessThanV sym))++    -- Finite enumerations+  , ("fromTo"     , {-# SCC "Prelude::fromTo" #-}+                    fromToV sym)++  , ("fromThenTo" , {-# SCC "Prelude::fromThenTo" #-}+                    fromThenToV sym)++  , ("fromToLessThan"+                  , {-# SCC "Prelude::fromToLessThan" #-}+                    fromToLessThanV sym)++    -- Sequence manipulations+  , ("#"          , {-# SCC "Prelude::(#)" #-}+                    PFinPoly \front ->+                    PNumPoly \back  ->+                    PTyPoly  \elty  ->+                    PFun \l ->+                    PFun \r ->+                    PPrim (join (ccatV sym (Nat front) back elty <$> l <*> r)))++  , ("join"       , {-# SCC "Prelude::join" #-}+                    PNumPoly \parts ->+                    PFinPoly \each  ->+                    PTyPoly  \a     ->+                    PStrict  \x   ->+                    PPrim $ joinV sym parts each a x)++  , ("split"      , {-# SCC "Prelude::split" #-}+                    ecSplitV sym)++  , ("splitAt"    , {-# SCC "Prelude::splitAt" #-}+                    PNumPoly \front ->+                    PNumPoly \back  ->+                    PTyPoly  \a     ->+                    PStrict  \x   ->+                    PPrim $ splitAtV sym front back a x)++  , ("reverse"    , {-# SCC "Prelude::reverse" #-}+                    PFinPoly \_a ->+                    PTyPoly  \_b ->+                    PStrict  \xs ->+                    PPrim $ reverseV sym xs)++  , ("transpose"  , {-# SCC "Prelude::transpose" #-}+                    PNumPoly \a ->+                    PNumPoly \b ->+                    PTyPoly  \c ->+                    PStrict  \xs ->+                    PPrim $ transposeV sym a b c xs)++    -- Misc++    -- {at,len} (fin len) => [len][8] -> at+  , ("error"      , {-# SCC "Prelude::error" #-}+                     PTyPoly  \a ->+                     PFinPoly \_ ->+                     PStrict  \s ->+                     PPrim (errorV sym a =<< valueToString sym s))++  , ("trace"       , {-# SCC "Prelude::trace" #-}+                     PNumPoly \_n ->+                     PTyPoly  \_a ->+                     PTyPoly  \_b ->+                     PFun     \s ->+                     PFun     \x ->+                     PFun     \y ->+                     PPrim+                      do msg <- valueToString sym =<< s+                         EvalOpts { evalPPOpts, evalLogger } <- liftIO getEOpts+                         doc <- ppValue sym evalPPOpts =<< x+                         liftIO $ logPrint evalLogger+                             $ if null msg then doc else text msg <+> doc+                         y)++  , ("random"      , {-# SCC "Prelude::random" #-}+                     PTyPoly  \a ->+                     PWordFun \x ->+                     PPrim+                       case wordAsLit sym x of+                         Just (_,i)  -> randomV sym a i+                         Nothing -> liftIO (X.throw (UnsupportedSymbolicOp "random")))++  , ("foldl"      , {-# SCC "Prelude::foldl" #-}+                    foldlV sym)++  , ("foldl'"     , {-# SCC "Prelude::foldl'" #-}+                    foldl'V sym)++  , ("deepseq"    , {-# SCC "Prelude::deepseq" #-}+                    PTyPoly \_a ->+                    PTyPoly \_b ->+                    PFun \x ->+                    PFun \y ->+                    PPrim do _ <- forceValue =<< x+                             y)++  , ("parmap"     , {-# SCC "Prelude::parmap" #-}+                    parmapV sym)++  , ("fromZ"      , {-# SCC "Prelude::fromZ" #-}+                    fromZV sym)++  ]

@@ -0,0 +1,39 @@+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE LambdaCase #-}+module Cryptol.Eval.Prims where++import Cryptol.Backend+import Cryptol.Eval.Type+import Cryptol.Eval.Value+import Cryptol.ModuleSystem.Name+import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))+import Cryptol.Utils.Panic++-- | This type provides a lightweight syntactic framework for defining+--   Cryptol primitives.  The main purpose of this type is to provide+--   an abstraction barrier that insulates the definitions of primitives+--   from possible changes in the representation of values.+data Prim sym+  = PFun (SEval sym (GenValue sym) -> Prim sym)+  | PStrict (GenValue sym -> Prim sym)+  | PWordFun (SWord sym -> Prim sym)+  | PFloatFun (SFloat sym -> Prim sym)+  | PTyPoly (TValue -> Prim sym)+  | PNumPoly (Nat' -> Prim sym)+  | PFinPoly (Integer -> Prim sym)+  | PPrim (SEval sym (GenValue sym))+  | PVal (GenValue sym)++-- | Evaluate a primitive into a value computation+evalPrim :: Backend sym => sym -> Name -> Prim sym -> SEval sym (GenValue sym)+evalPrim sym nm p = case p of+  PFun f      -> lam sym (evalPrim sym nm . f)+  PStrict f   -> lam sym (\x -> evalPrim sym nm . f =<< x)+  PWordFun f  -> lam sym (\x -> evalPrim sym nm . f =<< (fromVWord sym (show nm) =<< x))+  PFloatFun f -> flam sym (evalPrim sym nm . f)+  PTyPoly f   -> tlam sym (evalPrim sym nm . f)+  PNumPoly f  -> nlam sym (evalPrim sym nm . f)+  PFinPoly f  -> nlam sym (\case Inf -> panic "PFin" ["Unexpected `inf`", show nm];+                                 Nat n -> evalPrim sym nm (f n))+  PPrim m     -> m+  PVal v      -> pure v

@@ -28,7 +28,6 @@ > import Data.Ord (comparing) > import Data.Map (Map) > import qualified Data.Map as Map-> import qualified Data.IntMap as IntMap > import qualified Data.Text as T (pack) > import LibBF (BigFloat) > import qualified LibBF as FP@@ -39,8 +38,9 @@ > import Cryptol.TypeCheck.AST > import Cryptol.Backend.FloatHelpers (BF(..)) > import qualified Cryptol.Backend.FloatHelpers as FP-> import Cryptol.Backend.Monad (EvalError(..), PPOpts(..))-> import Cryptol.Eval.Type (TValue(..), isTBit, evalValType, evalNumType, TypeEnv)+> import Cryptol.Backend.Monad (EvalError(..))+> import Cryptol.Eval.Type+>   (TValue(..), isTBit, evalValType, evalNumType, TypeEnv, bindTypeVar) > import Cryptol.Eval.Concrete (mkBv, ppBV, lg2) > import Cryptol.Utils.Ident (Ident,PrimIdent, prelPrim, floatPrim) > import Cryptol.Utils.Panic (panic)@@ -48,7 +48,7 @@ > import Cryptol.Utils.RecordMap > > import qualified Cryptol.ModuleSystem as M-> import qualified Cryptol.ModuleSystem.Env as M (loadedModules)+> import qualified Cryptol.ModuleSystem.Env as M (loadedModules,loadedNewtypes)  Overview ========@@ -250,14 +250,14 @@ > > instance Semigroup Env where >   l <> r = Env->     { envVars  = Map.union (envVars  l) (envVars  r)->     , envTypes = IntMap.union (envTypes l) (envTypes r)+>     { envVars  = envVars  l <> envVars  r+>     , envTypes = envTypes l <> envTypes r  >     } > > instance Monoid Env where >   mempty = Env->     { envVars  = Map.empty->     , envTypes = IntMap.empty+>     { envVars  = mempty+>     , envTypes = mempty >     } >   mappend l r = l <> r >@@ -267,7 +267,7 @@ > > -- | Bind a type variable of kind # or *. > bindType :: TVar -> Either Nat' TValue -> Env -> Env-> bindType p ty env = env { envTypes = IntMap.insert (tvUnique p) ty (envTypes env) }+> bindType p ty env = env { envTypes = bindTypeVar p ty (envTypes env) }   Evaluation@@ -284,6 +284,8 @@ > evalExpr env expr = >   case expr of >+>     ELocated _ e -> evalExpr env e+> >     EList es _ty  -> >       pure $ VList (Nat (genericLength es)) [ evalExpr env e | e <- es ] >@@ -340,13 +342,15 @@ ---------  Apply the the given selector form to the given value.+Note that record selectors work uniformly on both record+types and on newtypes.  > evalSel :: Selector -> Value -> E Value > evalSel sel val = >   case sel of >     TupleSel n _  -> tupleSel n val >     RecordSel n _ -> recordSel n val->     ListSel n _  -> listSel n val+>     ListSel n _   -> listSel n val >   where >     tupleSel n v = >       case v of@@ -366,12 +370,15 @@   Update the given value using the given selector and new value.+Note that record selectors work uniformly on both record+types and on newtypes.  > evalSet :: TValue -> E Value -> Selector -> E Value -> E Value > evalSet tyv val sel fval = >   case (tyv, sel) of >     (TVTuple ts, TupleSel n _) -> updTupleAt ts n >     (TVRec fs, RecordSel n _)  -> updRecAt fs n+>     (TVNewtype _ _ fs, RecordSel n _) -> updRecAt fs n >     (TVSeq len _, ListSel n _) -> updSeqAt len n >     (_, _) -> evalPanic "evalSet" ["type/selector mismatch", show tyv, show sel] >   where@@ -463,7 +470,8 @@ >          -> Expr        -- ^ Head expression of the comprehension >          -> [[Match]]   -- ^ List of parallel comprehension branches >          -> E Value-> evalComp env expr branches = pure $ VList len [ evalExpr e expr | e <- envs ]+> evalComp env expr branches =+>     pure $ VList len [ evalExpr e expr | e <- envs ] >   where >     -- Generate a new environment for each iteration of each >     -- parallel branch.@@ -504,8 +512,27 @@ >   case dDefinition d of >     DPrim   -> (dName d, pure (evalPrim (dName d))) >     DExpr e -> (dName d, evalExpr env e)+> +Newtypes+-------- +At runtime, newtypes values are represented in exactly+the same way as records.  The constructor function for+newtypes is thus basically just an identity function+that consumes and ignores its type arguments.++> evalNewtypeDecl :: Env -> Newtype -> Env+> evalNewtypeDecl env nt = bindVar (ntName nt, pure val) env +>   where+>     val = foldr tabs con (ntParams nt)+>     con = VFun (\x -> x)+>     tabs tp body =+>       case tpKind tp of+>         KType -> VPoly (\_ -> pure body)+>         KNum  -> VNumPoly (\_ -> pure body)+>         k -> evalPanic "evalNewtypeDecl" ["illegal newtype parameter kind", show k]+ Primitives ========== @@ -909,7 +936,7 @@ >                               | (f, fty) <- canonicalFields fields ] > zero (TVFun _ bty)  = VFun (\_ -> pure (zero bty)) > zero (TVAbstract{}) = evalPanic "zero" ["Abstract type not in `Zero`"]-+> zero (TVNewtype{})  = evalPanic "zero" ["Newtype not in `Zero`"]  Literals --------@@ -978,6 +1005,7 @@ >         TVRational   -> evalPanic "logicUnary" ["Rational not in class Logic"] >         TVFloat{}    -> evalPanic "logicUnary" ["Float not in class Logic"] >         TVAbstract{} -> evalPanic "logicUnary" ["Abstract type not in `Logic`"]+>         TVNewtype{}  -> evalPanic "logicUnary" ["Newtype not in `Logic`"]  > logicBinary :: (Bool -> Bool -> Bool) -> TValue -> E Value -> E Value -> E Value > logicBinary op = go@@ -1016,6 +1044,7 @@ >         TVRational   -> evalPanic "logicBinary" ["Rational not in class Logic"] >         TVFloat{}    -> evalPanic "logicBinary" ["Float not in class Logic"] >         TVAbstract{} -> evalPanic "logicBinary" ["Abstract type not in `Logic`"]+>         TVNewtype{}  -> evalPanic "logicBinary" ["Newtype not in `Logic`"]   Ring Arithmetic@@ -1063,6 +1092,8 @@ >           pure $ VRecord [ (f, go fty) | (f, fty) <- canonicalFields fs ] >         TVAbstract {} -> >           evalPanic "arithNullary" ["Abstract type not in `Ring`"]+>         TVNewtype {} ->+>           evalPanic "arithNullary" ["Newtype type not in `Ring`"]  > ringUnary :: >   (Integer -> E Integer) ->@@ -1101,6 +1132,8 @@ >                             | (f, fty) <- canonicalFields fs ] >         TVAbstract {} -> >           evalPanic "arithUnary" ["Abstract type not in `Ring`"]+>         TVNewtype {} ->+>           evalPanic "arithUnary" ["Newtype not in `Ring`"]  > ringBinary :: >   (Integer -> Integer -> E Integer) ->@@ -1149,6 +1182,8 @@ >                | (f, fty) <- canonicalFields fs ] >         TVAbstract {} -> >           evalPanic "arithBinary" ["Abstract type not in class `Ring`"]+>         TVNewtype {} ->+>           evalPanic "arithBinary" ["Newtype not in class `Ring`"]   Integral@@ -1325,6 +1360,8 @@ >          lexList (zipWith3 lexCompare tys ls rs) >     TVAbstract {} -> >       evalPanic "lexCompare" ["Abstract type not in `Cmp`"]+>     TVNewtype {} ->+>       evalPanic "lexCompare" ["Newtype not in `Cmp`"] > > lexList :: [E Ordering] -> E Ordering > lexList [] = pure EQ@@ -1379,6 +1416,8 @@ >          lexList (zipWith3 lexSignedCompare tys ls rs) >     TVAbstract {} -> >       evalPanic "lexSignedCompare" ["Abstract type not in `Cmp`"]+>     TVNewtype {} ->+>       evalPanic "lexSignedCompare" ["Newtype type not in `Cmp`"]   Sequences@@ -1690,7 +1729,10 @@ running the reference evaluator on an expression.  > evaluate :: Expr -> M.ModuleCmd (E Value)-> evaluate expr (_, _, modEnv) = return (Right (evalExpr env expr, modEnv), [])+> evaluate expr minp = return (Right (val, modEnv), []) >   where+>     modEnv = M.minpModuleEnv minp >     extDgs = concatMap mDecls (M.loadedModules modEnv)->     env = foldl evalDeclGroup mempty extDgs+>     nts    = Map.elems (M.loadedNewtypes modEnv)+>     env    = foldl evalDeclGroup (foldl evalNewtypeDecl mempty nts) extDgs+>     val    = evalExpr env expr

@@ -6,6 +6,7 @@ -- Stability   :  provisional -- Portability :  portable +{-# LANGUAGE BlockArguments #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}@@ -21,7 +22,6 @@   ) where  import qualified Control.Exception as X-import           Control.Monad (join) import           Control.Monad.IO.Class (MonadIO(..)) import           Data.Bits (bit, shiftL) import qualified Data.Map as Map@@ -33,8 +33,9 @@ import Cryptol.Backend.Monad ( EvalError(..), Unsupported(..) ) import Cryptol.Backend.SBV -import Cryptol.Eval.Type (TValue(..), finNat')+import Cryptol.Eval.Type (TValue(..)) import Cryptol.Eval.Generic+import Cryptol.Eval.Prims import Cryptol.Eval.Value import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), widthInteger) import Cryptol.Utils.Ident@@ -46,106 +47,12 @@ -- Primitives ------------------------------------------------------------------  -- See also Cryptol.Eval.Concrete.primTable-primTable :: SBV -> Map.Map PrimIdent Value-primTable sym =+primTable :: SBV -> IO EvalOpts -> Map.Map PrimIdent (Prim SBV)+primTable sym getEOpts =+  Map.union (genericPrimTable sym getEOpts) $   Map.fromList $ map (\(n, v) -> (prelPrim (T.pack n), v)) -  [ -- Literals-    ("True"        , VBit (bitLit sym True))-  , ("False"       , VBit (bitLit sym False))-  , ("number"      , ecNumberV sym) -- Converts a numeric type into its corresponding value.-                                    -- { val, rep } (Literal val rep) => rep-  , ("fraction"     , ecFractionV sym)-  , ("ratio"       , ratioV sym)--    -- Zero-  , ("zero"        , VPoly (zeroV sym))--    -- Logic-  , ("&&"          , binary (andV sym))-  , ("||"          , binary (orV sym))-  , ("^"           , binary (xorV sym))-  , ("complement"  , unary  (complementV sym))--    -- Ring-  , ("fromInteger" , fromIntegerV sym)-  , ("+"           , binary (addV sym))-  , ("-"           , binary (subV sym))-  , ("negate"      , unary (negateV sym))-  , ("*"           , binary (mulV sym))--    -- Integral-  , ("toInteger"   , toIntegerV sym)-  , ("/"           , binary (divV sym))-  , ("%"           , binary (modV sym))-  , ("^^"          , expV sym)-  , ("infFrom"     , infFromV sym)-  , ("infFromThen" , infFromThenV sym)--    -- Field-  , ("recip"       , recipV sym)-  , ("/."          , fieldDivideV sym)--    -- Round-  , ("floor"       , unary (floorV sym))-  , ("ceiling"     , unary (ceilingV sym))-  , ("trunc"       , unary (truncV sym))-  , ("roundAway"   , unary (roundAwayV sym))-  , ("roundToEven" , unary (roundToEvenV sym))--    -- Word operations-  , ("/$"          , sdivV sym)-  , ("%$"          , smodV sym)-  , ("lg2"         , lg2V sym)-  , (">>$"         , sshrV sym)--    -- Cmp-  , ("<"           , binary (lessThanV sym))-  , (">"           , binary (greaterThanV sym))-  , ("<="          , binary (lessThanEqV sym))-  , (">="          , binary (greaterThanEqV sym))-  , ("=="          , binary (eqV sym))-  , ("!="          , binary (distinctV sym))--    -- SignedCmp-  , ("<$"          , binary (signedLessThanV sym))--    -- Finite enumerations-  , ("fromTo"      , fromToV sym)-  , ("fromThenTo"  , fromThenToV sym)--    -- Sequence manipulations-  , ("#"          , -- {a,b,d} (fin a) => [a] d -> [b] d -> [a + b] d-     nlam $ \ front ->-     nlam $ \ back  ->-     tlam $ \ elty  ->-     lam  $ \ l     -> return $-     lam  $ \ r     -> join (ccatV sym front back elty <$> l <*> r))--  , ("join"       ,-     nlam $ \ parts ->-     nlam $ \ (finNat' -> each)  ->-     tlam $ \ a     ->-     lam  $ \ x     ->-       joinV sym parts each a =<< x)--  , ("split"       , ecSplitV sym)--  , ("splitAt"    ,-     nlam $ \ front ->-     nlam $ \ back  ->-     tlam $ \ a     ->-     lam  $ \ x     ->-       splitAtV sym front back a =<< x)--  , ("reverse"    , nlam $ \_a ->-                    tlam $ \_b ->-                     lam $ \xs -> reverseV sym =<< xs)--  , ("transpose"  , nlam $ \a ->-                    nlam $ \b ->-                    tlam $ \c ->-                     lam $ \xs -> transposeV sym a b c =<< xs)+  [ (">>$"         , sshrV sym)      -- Shifts and rotates   , ("<<"          , logicShift sym "<<"@@ -179,52 +86,8 @@   , ("update"      , updatePrim sym (updateFrontSym_word sym) (updateFrontSym sym))   , ("updateEnd"   , updatePrim sym (updateBackSym_word sym) (updateBackSym sym)) -    -- Misc--  , ("fromZ"       , fromZV sym)--  , ("foldl"       , foldlV sym)-  , ("foldl'"      , foldl'V sym)--  , ("deepseq"     ,-      tlam $ \_a ->-      tlam $ \_b ->-       lam $ \x -> pure $-       lam $ \y ->-         do _ <- forceValue =<< x-            y)--  , ("parmap"      , parmapV sym)--    -- {at,len} (fin len) => [len][8] -> at-  , ("error"       ,-      tlam $ \a ->-      nlam $ \_ ->-      VFun $ \s -> errorV sym a =<< (valueToString sym =<< s))--  , ("random"      ,-      tlam $ \a ->-      wlam sym $ \x ->-         case integerAsLit sym x of-           Just i  -> randomV sym a i-           Nothing -> cryUserError sym "cannot evaluate 'random' with symbolic inputs")--     -- The trace function simply forces its first two-     -- values before returing the third in the symbolic-     -- evaluator.-  , ("trace",-      nlam $ \_n ->-      tlam $ \_a ->-      tlam $ \_b ->-       lam $ \s -> return $-       lam $ \x -> return $-       lam $ \y -> do-         _ <- s-         _ <- x-         y)   ] - indexFront ::   SBV ->   Nat' ->@@ -468,13 +331,14 @@        go f (WordVal x :vs) = go (f . (x:)) vs        go _f (LargeBitsVal _ _ : _) = Nothing -sshrV :: SBV -> Value+sshrV :: SBV -> Prim SBV sshrV sym =-  nlam $ \n ->-  tlam $ \ix ->-  wlam sym $ \x -> return $-  lam $ \y ->-   y >>= asIndex sym ">>$" ix >>= \case+  PNumPoly \n ->+  PTyPoly  \ix ->+  PWordFun \x ->+  PStrict  \y ->+  PPrim $+   asIndex sym ">>$" ix y >>= \case      Left idx ->        do let w = toInteger (SBV.intSizeOf x)           let pneg = svLessThan idx (svInteger KUnbounded 0)

@@ -11,7 +11,7 @@ {-# LANGUAGE DeriveGeneric #-} module Cryptol.Eval.Type where -import Cryptol.Backend.Monad (evalPanic, typeCannotBeDemoted)+import Cryptol.Backend.Monad (evalPanic) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.PP(pp) import Cryptol.TypeCheck.Solver.InfNat@@ -38,8 +38,11 @@   | TVTuple [TValue]          -- ^ @ (a, b, c )@   | TVRec (RecordMap Ident TValue) -- ^ @ { x : a, y : b, z : c } @   | TVFun TValue TValue       -- ^ @ a -> b @+  | TVNewtype Newtype+              [Either Nat' TValue]+              (RecordMap Ident TValue)     -- ^ a named newtype   | TVAbstract UserTC [Either Nat' TValue] -- ^ an abstract type-    deriving (Generic, NFData)+    deriving (Generic, NFData, Eq)  -- | Convert a type value back into a regular type tValTy :: TValue -> Type@@ -56,13 +59,17 @@     TVTuple ts  -> tTuple (map tValTy ts)     TVRec fs    -> tRec (fmap tValTy fs)     TVFun t1 t2 -> tFun (tValTy t1) (tValTy t2)-    TVAbstract u vs -> tAbstract u (map arg vs)-      where arg x = case x of-                      Left Inf     -> tInf-                      Left (Nat n) -> tNum n-                      Right v      -> tValTy v+    TVNewtype nt vs _ -> tNewtype nt (map tNumValTy vs)+    TVAbstract u vs -> tAbstract u (map tNumValTy vs) +tNumTy :: Nat' -> Type+tNumTy Inf     = tInf+tNumTy (Nat n) = tNum n +tNumValTy :: Either Nat' TValue -> Type+tNumValTy = either tNumTy tValTy++ instance Show TValue where   showsPrec p v = showsPrec p (tValTy v) @@ -90,20 +97,38 @@  -- Type Evaluation ------------------------------------------------------------- -type TypeEnv = IntMap.IntMap (Either Nat' TValue)+newtype TypeEnv =+  TypeEnv+  { envTypeMap  :: IntMap.IntMap (Either Nat' TValue) } +instance Monoid TypeEnv where+  mempty = TypeEnv mempty +instance Semigroup TypeEnv where+  l <> r = TypeEnv+    { envTypeMap  = IntMap.union (envTypeMap l) (envTypeMap r) }++lookupTypeVar :: TVar -> TypeEnv -> Maybe (Either Nat' TValue)+lookupTypeVar tv env = IntMap.lookup (tvUnique tv) (envTypeMap env)++bindTypeVar :: TVar -> Either Nat' TValue -> TypeEnv -> TypeEnv+bindTypeVar tv ty env = env{ envTypeMap = IntMap.insert (tvUnique tv) ty (envTypeMap env) }+ -- | Evaluation for types (kind * or #). evalType :: TypeEnv -> Type -> Either Nat' TValue evalType env ty =   case ty of     TVar tv ->-      case IntMap.lookup (tvUnique tv) env of+      case lookupTypeVar tv env of         Just v -> v         Nothing -> evalPanic "evalType" ["type variable not bound", show tv]      TUser _ _ ty'  -> evalType env ty'     TRec fields    -> Right $ TVRec (fmap val fields)++    TNewtype nt ts -> Right $ TVNewtype nt tvs $ evalNewtypeBody env nt tvs+        where tvs = map (evalType env) ts+     TCon (TC c) ts ->       case (c, ts) of         (TCBit, [])     -> Right $ TVBit@@ -128,7 +153,6 @@                 , "*** Name: " ++ show (pp u)                 ] -        -- FIXME: What about TCNewtype?         _ -> evalPanic "evalType" ["not a value type", show ty]     TCon (TF f) ts      -> Left $ evalTF f (map num ts)     TCon (PC p) _       -> evalPanic "evalType" ["invalid predicate symbol", show p]@@ -142,6 +166,16 @@                Inf   -> evalPanic "evalType"                                   ["Expecting a finite size, but got `inf`"] +-- | Evaluate the body of a newtype, given evaluated arguments+evalNewtypeBody :: TypeEnv -> Newtype -> [Either Nat' TValue] -> RecordMap Ident TValue+evalNewtypeBody env0 nt args = fmap (evalValType env') (ntFields nt)+  where+  env' = loop env0 (ntParams nt) args++  loop env [] [] = env+  loop env (p:ps) (a:as) = loop (bindTypeVar (TVBound p) a env) ps as+  loop _ _ _ = evalPanic "evalNewtype" ["type parameter/argument mismatch"]+ -- | Evaluation for value types (kind *). evalValType :: TypeEnv -> Type -> TValue evalValType env ty =@@ -175,5 +209,5 @@   | otherwise  = evalPanic "evalTF"                         ["Unexpected type function:", show ty] -  where mb = fromMaybe (typeCannotBeDemoted ty)+  where mb = fromMaybe (evalPanic "evalTF" ["type cannot be demoted", show (pp ty)])         ty = TCon (TF f) (map tNat' vs)

@@ -30,10 +30,11 @@   , forceValue   , Backend(..)   , asciiMode++  , EvalOpts(..)     -- ** Value introduction operations   , word   , lam-  , wlam   , flam   , tlam   , nlam@@ -95,16 +96,21 @@ import Data.Bits import Data.IORef import Data.Map.Strict (Map)+import Data.Ratio import qualified Data.Map.Strict as Map import MonadLib+import Numeric (showIntAtBase)  import Cryptol.Backend import qualified Cryptol.Backend.Arch as Arch-import Cryptol.Backend.Monad ( PPOpts(..), evalPanic, wordTooWide, defaultPPOpts, asciiMode )+import Cryptol.Backend.Monad+  ( evalPanic, wordTooWide, CallStack, combineCallStacks )+import Cryptol.Backend.FloatHelpers (fpPP) import Cryptol.Eval.Type  import Cryptol.TypeCheck.Solver.InfNat(Nat'(..)) import Cryptol.Utils.Ident (Ident)+import Cryptol.Utils.Logger(Logger) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.PP import Cryptol.Utils.RecordMap@@ -113,6 +119,12 @@  import GHC.Generics (Generic) +-- | Some options for evalutaion+data EvalOpts = EvalOpts+  { evalLogger :: Logger    -- ^ Where to print stuff (e.g., for @trace@)+  , evalPPOpts :: PPOpts    -- ^ How to pretty print things.+  }+ -- Values ----------------------------------------------------------------------  -- | A sequence map represents a mapping from nonnegative integer indices@@ -135,22 +147,22 @@ largeBitSize = 1 `shiftL` 48  -- | Generate a finite sequence map from a list of values-finiteSeqMap :: Backend sym => sym -> [SEval sym (GenValue sym)] -> SeqMap sym-finiteSeqMap sym xs =+finiteSeqMap :: [SEval sym (GenValue sym)] -> SeqMap sym+finiteSeqMap xs =    UpdateSeqMap       (Map.fromList (zip [0..] xs))-      (invalidIndex sym)+      (\i -> panic "finiteSeqMap" ["Out of bounds access of finite seq map", "length: " ++ show (length xs), show i])  -- | Generate an infinite sequence map from a stream of values-infiniteSeqMap :: Backend sym => [SEval sym (GenValue sym)] -> SEval sym (SeqMap sym)-infiniteSeqMap xs =+infiniteSeqMap :: Backend sym => sym -> [SEval sym (GenValue sym)] -> SEval sym (SeqMap sym)+infiniteSeqMap sym xs =    -- TODO: use an int-trie?-   memoMap (IndexSeqMap $ \i -> genericIndex xs i)+   memoMap sym (IndexSeqMap $ \i -> genericIndex xs i)  -- | Create a finite list of length @n@ of the values from @[0..n-1]@ in --   the given the sequence emap. enumerateSeqMap :: (Integral n) => n -> SeqMap sym -> [SEval sym (GenValue sym)]-enumerateSeqMap n m = [ lookupSeqMap m i | i <- [0 .. (toInteger n)-1] ]+enumerateSeqMap n m = [ lookupSeqMap m  i | i <- [0 .. (toInteger n)-1] ]  -- | Create an infinite stream of all the values in a sequence map streamSeqMap :: SeqMap sym -> [SEval sym (GenValue sym)]@@ -191,17 +203,18 @@  -- | Given a sequence map, return a new sequence map that is memoized using --   a finite map memo table.-memoMap :: (MonadIO m, Backend sym) => SeqMap sym -> m (SeqMap sym)-memoMap x = do+memoMap :: Backend sym => sym -> SeqMap sym -> SEval sym (SeqMap sym)+memoMap sym x = do+  stk <- sGetCallStack sym   cache <- liftIO $ newIORef $ Map.empty-  return $ IndexSeqMap (memo cache)+  return $ IndexSeqMap (memo cache stk)    where-  memo cache i = do+  memo cache stk i = do     mz <- liftIO (Map.lookup i <$> readIORef cache)     case mz of       Just z  -> return z-      Nothing -> doEval cache i+      Nothing -> sWithCallStack sym stk (doEval cache i)    doEval cache i = do     v <- lookupSeqMap x i@@ -212,20 +225,22 @@ --   sequence maps. zipSeqMap ::   Backend sym =>+  sym ->   (GenValue sym -> GenValue sym -> SEval sym (GenValue sym)) ->   SeqMap sym ->   SeqMap sym ->   SEval sym (SeqMap sym)-zipSeqMap f x y =-  memoMap (IndexSeqMap $ \i -> join (f <$> lookupSeqMap x i <*> lookupSeqMap y i))+zipSeqMap sym f x y =+  memoMap sym (IndexSeqMap $ \i -> join (f <$> lookupSeqMap x i <*> lookupSeqMap y i))  -- | Apply the given function to each value in the given sequence map mapSeqMap ::   Backend sym =>+  sym ->   (GenValue sym -> SEval sym (GenValue sym)) ->   SeqMap sym -> SEval sym (SeqMap sym)-mapSeqMap f x =-  memoMap (IndexSeqMap $ \i -> f =<< lookupSeqMap x i)+mapSeqMap sym f x =+  memoMap sym (IndexSeqMap $ \i -> f =<< lookupSeqMap x i)  -- | For efficiency reasons, we handle finite sequences of bits as special cases --   in the evaluator.  In cases where we know it is safe to do so, we prefer to@@ -280,7 +295,8 @@  -- | Produce a new 'WordValue' from the one given by updating the @i@th bit with the --   given bit value.-updateWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym) -> SEval sym (WordValue sym)+updateWordValue :: Backend sym =>+  sym -> WordValue sym -> Integer -> SEval sym (SBit sym) -> SEval sym (WordValue sym) updateWordValue sym (WordVal w) idx b    | idx < 0 || idx >= wordLen sym w = invalidIndex sym idx    | isReady sym b = WordVal <$> (wordUpdate sym w idx =<< b)@@ -308,9 +324,9 @@                                                --   Invariant: VSeq is never a sequence of bits   | VWord !Integer !(SEval sym (WordValue sym))  -- ^ @ [n]Bit @   | VStream !(SeqMap sym)                   -- ^ @ [inf]a @-  | VFun (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -- ^ functions-  | VPoly (TValue -> SEval sym (GenValue sym))   -- ^ polymorphic values (kind *)-  | VNumPoly (Nat' -> SEval sym (GenValue sym))  -- ^ polymorphic values (kind #)+  | VFun  CallStack (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -- ^ functions+  | VPoly CallStack (TValue -> SEval sym (GenValue sym))   -- ^ polymorphic values (kind *)+  | VNumPoly CallStack (Nat' -> SEval sym (GenValue sym))  -- ^ polymorphic values (kind #)  deriving Generic  @@ -331,9 +347,9 @@   VFloat f    -> seq f (return ())   VWord _ wv  -> forceWordValue =<< wv   VStream _   -> return ()-  VFun _      -> return ()-  VPoly _     -> return ()-  VNumPoly _  -> return ()+  VFun{}      -> return ()+  VPoly{}     -> return ()+  VNumPoly{}  -> return ()   @@ -348,9 +364,9 @@     VSeq n _   -> "seq:" ++ show n     VWord n _  -> "word:"  ++ show n     VStream _  -> "stream"-    VFun _     -> "fun"-    VPoly _    -> "poly"-    VNumPoly _ -> "numpoly"+    VFun{}     -> "fun"+    VPoly{}    -> "poly"+    VNumPoly{} -> "numpoly"   -- Pretty Printing -------------------------------------------------------------@@ -371,10 +387,10 @@       ppField (f,r) = pp f <+> char '=' <+> r     VTuple vals        -> do vals' <- traverse (>>=loop) vals                              return $ parens (sep (punctuate comma vals'))-    VBit b             -> return $ ppBit x b-    VInteger i         -> return $ ppInteger x opts i-    VRational q        -> return $ ppRational x opts q-    VFloat i           -> return $ ppFloat x opts i+    VBit b             -> ppSBit x b+    VInteger i         -> ppSInteger x i+    VRational q        -> ppSRational x q+    VFloat i           -> ppSFloat x opts i     VSeq sz vals       -> ppWordSeq sz vals     VWord _ wv         -> ppWordVal =<< wv     VStream vals       -> do vals' <- traverse (>>=loop) $ enumerateSeqMap (useInfLength opts) vals@@ -382,12 +398,12 @@                                    $ punctuate comma                                    ( vals' ++ [text "..."]                                    )-    VFun _             -> return $ text "<function>"-    VPoly _            -> return $ text "<polymorphic value>"-    VNumPoly _         -> return $ text "<polymorphic value>"+    VFun{}             -> return $ text "<function>"+    VPoly{}            -> return $ text "<polymorphic value>"+    VNumPoly{}         -> return $ text "<polymorphic value>"    ppWordVal :: WordValue sym -> SEval sym Doc-  ppWordVal w = ppWord x opts <$> asWordVal x w+  ppWordVal w = ppSWord x opts =<< asWordVal x w    ppWordSeq :: Integer -> SeqMap sym -> SEval sym Doc   ppWordSeq sz vals = do@@ -399,11 +415,102 @@         -> do vs <- traverse (fromVWord x "ppWordSeq") ws               case traverse (wordAsChar x) vs of                 Just str -> return $ text (show str)-                _ -> return $ brackets (fsep (punctuate comma $ map (ppWord x opts) vs))+                _ -> do vs' <- mapM (ppSWord x opts) vs+                        return $ brackets (fsep (punctuate comma vs'))       _ -> do ws' <- traverse loop ws               return $ brackets (fsep (punctuate comma ws')) +ppSBit :: Backend sym => sym -> SBit sym -> SEval sym Doc+ppSBit sym b =+  case bitAsLit sym b of+    Just True  -> pure (text "True")+    Just False -> pure (text "False")+    Nothing    -> pure (text "?") +ppSInteger :: Backend sym => sym -> SInteger sym -> SEval sym Doc+ppSInteger sym x =+  case integerAsLit sym x of+    Just i  -> pure (integer i)+    Nothing -> pure (text "[?]")++ppSFloat :: Backend sym => sym -> PPOpts -> SFloat sym -> SEval sym Doc+ppSFloat sym opts x =+  case fpAsLit sym x of+    Just fp -> pure (fpPP opts fp)+    Nothing -> pure (text "[?]")++ppSRational :: Backend sym => sym -> SRational sym -> SEval sym Doc+ppSRational sym (SRational n d)+  | Just ni <- integerAsLit sym n+  , Just di <- integerAsLit sym d+  = let q = ni % di in+      pure (text "(ratio" <+> integer (numerator q) <+> (integer (denominator q) <> text ")"))++  | otherwise+  = do n' <- ppSInteger sym n+       d' <- ppSInteger sym d+       pure (text "(ratio" <+> n' <+> (d' <> text ")"))++ppSWord :: Backend sym => sym -> PPOpts -> SWord sym -> SEval sym Doc+ppSWord sym opts bv+  | asciiMode opts width =+      case wordAsLit sym bv of+        Just (_,i) -> pure (text (show (toEnum (fromInteger i) :: Char)))+        Nothing    -> pure (text "?")++  | otherwise =+      case wordAsLit sym bv of+        Just (_,i) ->+          let val = value i in+          pure (prefix (length val) <.> text val)+        Nothing+          | base == 2  -> sliceDigits 1 "0b"+          | base == 8  -> sliceDigits 3 "0o"+          | base == 16 -> sliceDigits 4 "0x"+          | otherwise  -> pure (text "[?]")++  where+  width = wordLen sym bv++  base = if useBase opts > 36 then 10 else useBase opts++  padding bitsPerDigit len = text (replicate padLen '0')+    where+    padLen | m > 0     = d + 1+           | otherwise = d++    (d,m) = (fromInteger width - (len * bitsPerDigit))+                   `divMod` bitsPerDigit++  prefix len = case base of+    2  -> text "0b" <.> padding 1 len+    8  -> text "0o" <.> padding 3 len+    10 -> empty+    16 -> text "0x" <.> padding 4 len+    _  -> text "0"  <.> char '<' <.> int base <.> char '>'++  value i = showIntAtBase (toInteger base) (digits !!) i ""+  digits  = "0123456789abcdefghijklmnopqrstuvwxyz"++  toDigit w =+    case wordAsLit sym w of+      Just (_,i) | i <= 36 -> digits !! fromInteger i+      _ -> '?'++  sliceDigits bits pfx =+    do ws <- goDigits bits [] bv+       let ds = map toDigit ws+       pure (text pfx <.> text ds)++  goDigits bits ds w+    | wordLen sym w > bits =+        do (hi,lo) <- splitWord sym (wordLen sym w - bits) bits w+           goDigits bits (lo:ds) hi++    | wordLen sym w > 0 = pure (w:ds)++    | otherwise          = pure ds+ -- Value Constructors ----------------------------------------------------------  -- | Create a packed word of n bits.@@ -413,45 +520,41 @@   | otherwise                = VWord n (WordVal <$> wordLit sym n i)  -lam :: (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -> GenValue sym-lam  = VFun---- | Functions that assume word inputs-wlam :: Backend sym => sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym-wlam sym f = VFun (\arg -> arg >>= fromVWord sym "wlam" >>= f)+-- | Construct a function value+lam :: Backend sym => sym -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)+lam sym f = VFun <$> sGetCallStack sym <*> pure f  -- | Functions that assume floating point inputs-flam :: Backend sym =>-        (SFloat sym -> SEval sym (GenValue sym)) -> GenValue sym-flam f = VFun (\arg -> arg >>= f . fromVFloat)--+flam :: Backend sym => sym ->+        (SFloat sym -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)+flam sym f = VFun <$> sGetCallStack sym <*> pure (\arg -> arg >>= f . fromVFloat)  -- | A type lambda that expects a 'Type'.-tlam :: Backend sym => (TValue -> GenValue sym) -> GenValue sym-tlam f = VPoly (return . f)+tlam :: Backend sym => sym -> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)+tlam sym f = VPoly <$> sGetCallStack sym <*> pure f  -- | A type lambda that expects a 'Type' of kind #.-nlam :: Backend sym => (Nat' -> GenValue sym) -> GenValue sym-nlam f = VNumPoly (return . f)+nlam :: Backend sym => sym -> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)+nlam sym f = VNumPoly <$> sGetCallStack sym <*> pure f  -- | A type lambda that expects a finite numeric type.-ilam :: Backend sym => (Integer -> GenValue sym) -> GenValue sym-ilam f = nlam (\n -> case n of-                       Nat i -> f i-                       Inf   -> panic "ilam" [ "Unexpected `inf`" ])+ilam :: Backend sym => sym -> (Integer -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)+ilam sym f =+   nlam sym (\n -> case n of+                     Nat i -> f i+                     Inf   -> panic "ilam" [ "Unexpected `inf`" ])  -- | Generate a stream.-toStream :: Backend sym => [GenValue sym] -> SEval sym (GenValue sym)-toStream vs =-   VStream <$> infiniteSeqMap (map pure vs)+toStream :: Backend sym => sym -> [GenValue sym] -> SEval sym (GenValue sym)+toStream sym vs =+   VStream <$> infiniteSeqMap sym (map pure vs)  toFinSeq ::   Backend sym =>   sym -> Integer -> TValue -> [GenValue sym] -> GenValue sym toFinSeq sym len elty vs    | isTBit elty = VWord len (WordVal <$> packWord sym (map fromVBit vs))-   | otherwise   = VSeq len $ finiteSeqMap sym (map pure vs)+   | otherwise   = VSeq len $ finiteSeqMap (map pure vs)  -- | Construct either a finite sequence, or a stream.  In the finite case, -- record whether or not the elements were bits, to aid pretty-printing.@@ -460,7 +563,7 @@   sym -> Nat' -> TValue -> [GenValue sym] -> SEval sym (GenValue sym) toSeq sym len elty vals = case len of   Nat n -> return $ toFinSeq sym n elty vals-  Inf   -> toStream vals+  Inf   -> toStream sym vals   -- | Construct either a finite sequence, or a stream.  In the finite case,@@ -537,22 +640,25 @@   go _ (_ : _) = Nothing  -- | Extract a function from a value.-fromVFun :: GenValue sym -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))-fromVFun val = case val of-  VFun f -> f-  _      -> evalPanic "fromVFun" ["not a function"]+fromVFun :: Backend sym => sym -> GenValue sym -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))+fromVFun sym val = case val of+  VFun fnstk f ->+    \x -> sModifyCallStack sym (\stk -> combineCallStacks stk fnstk) (f x)+  _ -> evalPanic "fromVFun" ["not a function"]  -- | Extract a polymorphic function from a value.-fromVPoly :: GenValue sym -> (TValue -> SEval sym (GenValue sym))-fromVPoly val = case val of-  VPoly f -> f-  _       -> evalPanic "fromVPoly" ["not a polymorphic value"]+fromVPoly :: Backend sym => sym -> GenValue sym -> (TValue -> SEval sym (GenValue sym))+fromVPoly sym val = case val of+  VPoly fnstk f ->+    \x -> sModifyCallStack sym (\stk -> combineCallStacks stk fnstk) (f x)+  _ -> evalPanic "fromVPoly" ["not a polymorphic value"]  -- | Extract a polymorphic function from a value.-fromVNumPoly :: GenValue sym -> (Nat' -> SEval sym (GenValue sym))-fromVNumPoly val = case val of-  VNumPoly f -> f-  _          -> evalPanic "fromVNumPoly" ["not a polymorphic value"]+fromVNumPoly :: Backend sym => sym -> GenValue sym -> (Nat' -> SEval sym (GenValue sym))+fromVNumPoly sym val = case val of+  VNumPoly fnstk f ->+    \x -> sModifyCallStack sym (\stk -> combineCallStacks stk fnstk) (f x)+  _  -> evalPanic "fromVNumPoly" ["not a polymorphic value"]  -- | Extract a tuple from a value. fromVTuple :: GenValue sym -> [SEval sym (GenValue sym)]

@@ -18,22 +18,20 @@ module Cryptol.Eval.What4   ( Value   , primTable-  , floatPrims   ) where  import qualified Control.Exception as X import           Control.Concurrent.MVar-import           Control.Monad (join,foldM)+import           Control.Monad (foldM) import           Control.Monad.IO.Class import           Data.Bits import qualified Data.Map as Map-import           Data.Map (Map) import qualified Data.Set as Set import           Data.Text (Text) import qualified Data.Text as Text import           Data.Parameterized.Context-import           Data.Parameterized.Some import           Data.Parameterized.TraversableFC+import           Data.Parameterized.Some import qualified Data.BitVector.Sized as BV  import qualified What4.Interface as W4@@ -43,10 +41,10 @@ import Cryptol.Backend import Cryptol.Backend.Monad ( EvalError(..), Unsupported(..) ) import Cryptol.Backend.What4-import qualified Cryptol.Backend.What4.SFloat as W4  import Cryptol.Eval.Generic-import Cryptol.Eval.Type (finNat', TValue(..))+import Cryptol.Eval.Prims+import Cryptol.Eval.Type (TValue(..)) import Cryptol.Eval.Value  import qualified Cryptol.SHA as SHA@@ -60,111 +58,17 @@ type Value sym = GenValue (What4 sym)  -- See also Cryptol.Prims.Eval.primTable-primTable :: W4.IsSymExprBuilder sym => What4 sym -> Map.Map PrimIdent (Value sym)-primTable sym =+primTable :: W4.IsSymExprBuilder sym => What4 sym -> IO EvalOpts -> Map.Map PrimIdent (Prim (What4 sym))+primTable sym getEOpts =   let w4sym = w4 sym in-  Map.union (floatPrims sym) $   Map.union (suiteBPrims sym) $   Map.union (primeECPrims sym) $+  Map.union (genericFloatTable sym) $+  Map.union (genericPrimTable sym getEOpts) $    Map.fromList $ map (\(n, v) -> (prelPrim n, v)) -  [ -- Literals-    ("True"        , VBit (bitLit sym True))-  , ("False"       , VBit (bitLit sym False))-  , ("number"      , ecNumberV sym) -- Converts a numeric type into its corresponding value.-                                    -- { val, rep } (Literal val rep) => rep-  , ("fraction"    , ecFractionV sym)-  , ("ratio"       , ratioV sym)--    -- Zero-  , ("zero"        , VPoly (zeroV sym))--    -- Logic-  , ("&&"          , binary (andV sym))-  , ("||"          , binary (orV sym))-  , ("^"           , binary (xorV sym))-  , ("complement"  , unary  (complementV sym))--    -- Ring-  , ("fromInteger" , fromIntegerV sym)-  , ("+"           , binary (addV sym))-  , ("-"           , binary (subV sym))-  , ("negate"      , unary (negateV sym))-  , ("*"           , binary (mulV sym))--    -- Integral-  , ("toInteger"   , toIntegerV sym)-  , ("/"           , binary (divV sym))-  , ("%"           , binary (modV sym))-  , ("^^"          , expV sym)-  , ("infFrom"     , infFromV sym)-  , ("infFromThen" , infFromThenV sym)--    -- Field-  , ("recip"       , recipV sym)-  , ("/."          , fieldDivideV sym)--    -- Round-  , ("floor"       , unary (floorV sym))-  , ("ceiling"     , unary (ceilingV sym))-  , ("trunc"       , unary (truncV sym))-  , ("roundAway"   , unary (roundAwayV sym))-  , ("roundToEven" , unary (roundToEvenV sym))--    -- Word operations-  , ("/$"          , sdivV sym)-  , ("%$"          , smodV sym)-  , ("lg2"         , lg2V sym)-  , (">>$"         , sshrV sym)--    -- Cmp-  , ("<"           , binary (lessThanV sym))-  , (">"           , binary (greaterThanV sym))-  , ("<="          , binary (lessThanEqV sym))-  , (">="          , binary (greaterThanEqV sym))-  , ("=="          , binary (eqV sym))-  , ("!="          , binary (distinctV sym))--    -- SignedCmp-  , ("<$"          , binary (signedLessThanV sym))--    -- Finite enumerations-  , ("fromTo"      , fromToV sym)-  , ("fromThenTo"  , fromThenToV sym)--    -- Sequence manipulations-  , ("#"          , -- {a,b,d} (fin a) => [a] d -> [b] d -> [a + b] d-     nlam $ \ front ->-     nlam $ \ back  ->-     tlam $ \ elty  ->-     lam  $ \ l     -> return $-     lam  $ \ r     -> join (ccatV sym front back elty <$> l <*> r))--  , ("join"       ,-     nlam $ \ parts ->-     nlam $ \ (finNat' -> each)  ->-     tlam $ \ a     ->-     lam  $ \ x     ->-       joinV sym parts each a =<< x)--  , ("split"       , ecSplitV sym)--  , ("splitAt"    ,-     nlam $ \ front ->-     nlam $ \ back  ->-     tlam $ \ a     ->-     lam  $ \ x     ->-       splitAtV sym front back a =<< x)--  , ("reverse"    , nlam $ \_a ->-                    tlam $ \_b ->-                     lam $ \xs -> reverseV sym =<< xs)--  , ("transpose"  , nlam $ \a ->-                    nlam $ \b ->-                    tlam $ \c ->-                     lam $ \xs -> transposeV sym a b c =<< xs)+  [ (">>$"         , sshrV sym)      -- Shifts and rotates   , ("<<"          , logicShift sym "<<"  shiftShrink@@ -187,52 +91,9 @@   , ("update"      , updatePrim sym (updateFrontSym_word sym) (updateFrontSym sym))   , ("updateEnd"   , updatePrim sym (updateBackSym_word sym)  (updateBackSym sym)) -    -- Misc--  , ("foldl"       , foldlV sym)-  , ("foldl'"      , foldl'V sym)--  , ("deepseq"     ,-      tlam $ \_a ->-      tlam $ \_b ->-       lam $ \x -> pure $-       lam $ \y ->-         do _ <- forceValue =<< x-            y)--  , ("parmap"      , parmapV sym)--  , ("fromZ"       , fromZV sym)--    -- {at,len} (fin len) => [len][8] -> at-  , ("error"       ,-      tlam $ \a ->-      nlam $ \_ ->-      VFun $ \s -> errorV sym a =<< (valueToString sym =<< s))--  , ("random"      ,-      tlam $ \a ->-      wlam sym $ \x ->-         case wordAsLit sym x of-           Just (_,i)  -> randomV sym a i-           Nothing -> cryUserError sym "cannot evaluate 'random' with symbolic inputs")--     -- The trace function simply forces its first two-     -- values before returing the third in the symbolic-     -- evaluator.-  , ("trace",-      nlam $ \_n ->-      tlam $ \_a ->-      tlam $ \_b ->-       lam $ \s -> return $-       lam $ \x -> return $-       lam $ \y -> do-         _ <- s-         _ <- x-         y)   ] -primeECPrims :: W4.IsSymExprBuilder sym => What4 sym -> Map.Map PrimIdent (Value sym)+primeECPrims :: W4.IsSymExprBuilder sym => What4 sym -> Map.Map PrimIdent (Prim (What4 sym)) primeECPrims sym = Map.fromList $ [ (primeECPrim n, v) | (n,v) <- prims ]  where  (~>) = (,)@@ -240,8 +101,9 @@  prims =   [ -- {p} (prime p, p > 3) => ProjectivePoint p -> ProjectivePoint p     "ec_double" ~>-      ilam \p ->-       lam \s ->+      PFinPoly \p ->+      PFun     \s ->+      PPrim          do p' <- integerLit sym p             s' <- toProjectivePoint sym =<< s             addUninterpWarning sym "Prime ECC"@@ -252,9 +114,10 @@      -- {p} (prime p, p > 3) => ProjectivePoint p -> ProjectivePoint p -> ProjectivePoint p   , "ec_add_nonzero" ~>-      ilam \p ->-       lam \s -> pure $-       lam \t ->+      PFinPoly \p ->+      PFun     \s ->+      PFun     \t ->+      PPrim          do p' <- integerLit sym p             s' <- toProjectivePoint sym =<< s             t' <- toProjectivePoint sym =<< t@@ -266,9 +129,10 @@      -- {p} (prime p, p > 3) => Z p -> ProjectivePoint p -> ProjectivePoint p   , "ec_mult" ~>-      ilam \p ->-       lam \k -> pure $-       lam \s ->+      PFinPoly \p ->+      PFun     \k ->+      PFun     \s ->+      PPrim          do p' <- integerLit sym p             k' <- fromVInteger <$> k             s' <- toProjectivePoint sym =<< s@@ -280,11 +144,12 @@      -- {p} (prime p, p > 3) => Z p -> ProjectivePoint p -> Z p -> ProjectivePoint p -> ProjectivePoint p   , "ec_twin_mult" ~>-      ilam \p ->-       lam \j -> pure $-       lam \s -> pure $-       lam \k -> pure $-       lam \t ->+      PFinPoly \p ->+      PFun     \j ->+      PFun     \s ->+      PFun     \k ->+      PFun     \t ->+      PPrim          do p' <- integerLit sym p             j' <- fromVInteger <$> j             s' <- toProjectivePoint sym =<< s@@ -299,7 +164,6 @@             fromProjectivePoint sym z   ] - type ProjectivePoint = W4.BaseStructType (EmptyCtx ::> W4.BaseIntegerType ::> W4.BaseIntegerType ::> W4.BaseIntegerType)  projectivePointRepr :: W4.BaseTypeRepr ProjectivePoint@@ -321,37 +185,44 @@      z <- VInteger <$> W4.structField (w4 sym) p (natIndex @2)      pure $ VRecord $ recordFromFields [ (packIdent "x",pure x), (packIdent "y",pure y),(packIdent "z",pure z) ] -suiteBPrims :: W4.IsSymExprBuilder sym => What4 sym -> Map.Map PrimIdent (Value sym)++suiteBPrims :: W4.IsSymExprBuilder sym => What4 sym -> Map.Map PrimIdent (Prim (What4 sym)) suiteBPrims sym = Map.fromList $ [ (suiteBPrim n, v) | (n,v) <- prims ]  where  (~>) = (,)   prims =   [ "AESEncRound" ~>-       lam \st ->+       PFun \st ->+       PPrim          do addUninterpWarning sym "AES encryption"             applyAESStateFunc sym "AESEncRound" =<< st   , "AESEncFinalRound" ~>-       lam \st ->+       PFun \st ->+       PPrim          do addUninterpWarning sym "AES encryption"             applyAESStateFunc sym "AESEncFinalRound" =<< st   , "AESDecRound" ~>-       lam \st ->+       PFun \st ->+       PPrim          do addUninterpWarning sym "AES decryption"             applyAESStateFunc sym "AESDecRound" =<< st   , "AESDecFinalRound" ~>-       lam \st ->+       PFun \st ->+       PPrim          do addUninterpWarning sym "AES decryption"             applyAESStateFunc sym "AESDecFinalRound" =<< st   , "AESInvMixColumns" ~>-       lam \st ->+       PFun \st ->+       PPrim          do addUninterpWarning sym "AES key expansion"             applyAESStateFunc sym "AESInvMixColumns" =<< st      -- {k} (fin k, k >= 4, 8 >= k) => [k][32] -> [4*(k+7)][32]   , "AESKeyExpand" ~>-       ilam \k ->-        lam \st ->+       PFinPoly \k ->+       PFun     \st ->+       PPrim           do ss <- fromVSeq <$> st              -- pack the arguments into a k-tuple of 32-bit values              Some ws <- generateSomeM (fromInteger k) (\i -> Some <$> toWord32 sym "AESKeyExpand" ss (toInteger i))@@ -368,12 +239,13 @@                case intIndex (fromInteger i) (size ret) of                  Just (Some idx) | Just W4.Refl <- W4.testEquality (ret!idx) (W4.BaseBVRepr (W4.knownNat @32)) ->                    fromWord32 =<< liftIO (W4.structField (w4 sym) z idx)-                 _ -> invalidIndex sym i+                 _ -> evalPanic "AESKeyExpand" ["Index out of range", show k, show i]      -- {n} (fin n) => [n][16][32] -> [7][32]   , "processSHA2_224" ~>-    ilam \n ->-     lam \xs ->+    PFinPoly \n ->+    PFun     \xs ->+    PPrim        do blks <- enumerateSeqMap n . fromVSeq <$> xs           addUninterpWarning sym "SHA-224"           initSt <- liftIO (mkSHA256InitialState sym SHA.initialSHA224State)@@ -384,13 +256,14 @@                 do z <- liftIO $ W4.structField (w4 sym) finalSt idx                    case W4.testEquality (W4.exprType z) (W4.BaseBVRepr (W4.knownNat @32)) of                      Just W4.Refl -> fromWord32 z-                     Nothing -> invalidIndex sym i-              Nothing -> invalidIndex sym i+                     Nothing -> evalPanic "processSHA2_224" ["Index out of range", show i]+              Nothing -> evalPanic "processSHA2_224" ["Index out of range", show i]      -- {n} (fin n) => [n][16][32] -> [8][32]   , "processSHA2_256" ~>-    ilam \n ->-     lam \xs ->+    PFinPoly \n ->+    PFun     \xs ->+    PPrim        do blks <- enumerateSeqMap n . fromVSeq <$> xs           addUninterpWarning sym "SHA-256"           initSt <- liftIO (mkSHA256InitialState sym SHA.initialSHA256State)@@ -401,13 +274,14 @@                 do z <- liftIO $ W4.structField (w4 sym) finalSt idx                    case W4.testEquality (W4.exprType z) (W4.BaseBVRepr (W4.knownNat @32)) of                      Just W4.Refl -> fromWord32 z-                     Nothing -> invalidIndex sym i-              Nothing -> invalidIndex sym i+                     Nothing -> evalPanic "processSHA2_256" ["Index out of range", show i]+              Nothing -> evalPanic "processSHA2_256" ["Index out of range", show i]      -- {n} (fin n) => [n][16][64] -> [6][64]   , "processSHA2_384" ~>-    ilam \n ->-     lam \xs ->+    PFinPoly \n ->+    PFun     \xs ->+    PPrim        do blks <- enumerateSeqMap n . fromVSeq <$> xs           addUninterpWarning sym "SHA-384"           initSt <- liftIO (mkSHA512InitialState sym SHA.initialSHA384State)@@ -418,13 +292,14 @@                 do z <- liftIO $ W4.structField (w4 sym) finalSt idx                    case W4.testEquality (W4.exprType z) (W4.BaseBVRepr (W4.knownNat @64)) of                      Just W4.Refl -> fromWord64 z-                     Nothing -> invalidIndex sym i-              Nothing -> invalidIndex sym i+                     Nothing -> evalPanic "processSHA2_384" ["Index out of range", show i]+              Nothing -> evalPanic "processSHA2_384" ["Index out of range", show i]      -- {n} (fin n) => [n][16][64] -> [8][64]   , "processSHA2_512" ~>-    ilam \n ->-     lam \xs ->+    PFinPoly \n ->+    PFun     \xs ->+    PPrim        do blks <- enumerateSeqMap n . fromVSeq <$> xs           addUninterpWarning sym "SHA-512"           initSt <- liftIO (mkSHA512InitialState sym SHA.initialSHA512State)@@ -435,8 +310,8 @@                 do z <- liftIO $ W4.structField (w4 sym) finalSt idx                    case W4.testEquality (W4.exprType z) (W4.BaseBVRepr (W4.knownNat @64)) of                      Just W4.Refl -> fromWord64 z-                     Nothing -> invalidIndex sym i-              Nothing -> invalidIndex sym i+                     Nothing -> evalPanic "processSHA2_512" ["Index out of range", show i]+              Nothing -> evalPanic "processSHA2_512" ["Index out of range", show i]   ]  @@ -626,7 +501,7 @@           | i == 1 -> fromWord32 =<< liftIO (W4.structField (w4 sym) z (natIndex @1))           | i == 2 -> fromWord32 =<< liftIO (W4.structField (w4 sym) z (natIndex @2))           | i == 3 -> fromWord32 =<< liftIO (W4.structField (w4 sym) z (natIndex @3))-          | otherwise -> invalidIndex sym i+          | otherwise -> evalPanic "applyAESStateFunc" ["Index out of range", show funNm, show i]   where    nm = Text.unpack funNm@@ -636,13 +511,14 @@    argCtx = W4.knownRepr  -sshrV :: W4.IsSymExprBuilder sym => What4 sym -> Value sym+sshrV :: W4.IsSymExprBuilder sym => What4 sym -> Prim (What4 sym) sshrV sym =-  nlam $ \(Nat n) ->-  tlam $ \ix ->-  wlam sym $ \x -> return $-  lam $ \y ->-    y >>= asIndex sym ">>$" ix >>= \case+  PFinPoly \n ->+  PTyPoly  \ix ->+  PWordFun \x ->+  PStrict  \y ->+  PPrim $+    asIndex sym ">>$" ix y >>= \case        Left i ->          do pneg <- intLessThan sym i =<< integerLit sym 0             zneg <- do i' <- shiftShrink sym (Nat n) ix =<< intNegate sym i@@ -864,7 +740,7 @@     WordVal w | Just j <- SW.bvAsUnsignedInteger w ->       return $ updateSeqMap vs j val     _ ->-      memoMap $ IndexSeqMap $ \i ->+      memoMap sym $ IndexSeqMap $ \i ->       do b <- wordValueEqualsInteger sym wv i          iteValue sym b val (lookupSeqMap vs i) @@ -891,7 +767,7 @@     WordVal w | Just j <- SW.bvAsUnsignedInteger w ->       return $ updateSeqMap vs (n - 1 - j) val     _ ->-      memoMap $ IndexSeqMap $ \i ->+      memoMap sym $ IndexSeqMap $ \i ->       do b <- wordValueEqualsInteger sym wv (n - 1 - i)          iteValue sym b val (lookupSeqMap vs i) @@ -980,57 +856,3 @@      _ -> LargeBitsVal (wordValueSize sym wv) <$>            updateBackSym sym (Nat n) eltTy (asBitsMap sym bv) (Right wv) val------- | Table of floating point primitives-floatPrims :: W4.IsSymExprBuilder sym => What4 sym -> Map PrimIdent (Value sym)-floatPrims sym =-  Map.fromList [ (floatPrim i,v) | (i,v) <- nonInfixTable ]-  where-  w4sym = w4 sym-  (~>) = (,)--  nonInfixTable =-    [ "fpNaN"       ~> fpConst (W4.fpNaN w4sym)-    , "fpPosInf"    ~> fpConst (W4.fpPosInf w4sym)-    , "fpFromBits"  ~> ilam \e -> ilam \p -> wlam sym \w ->-                       VFloat <$> liftIO (W4.fpFromBinary w4sym e p w)-    , "fpToBits"    ~> ilam \e -> ilam \p -> flam \x ->-                       pure $ VWord (e+p)-                            $ WordVal <$> liftIO (W4.fpToBinary w4sym x)-    , "=.="         ~> ilam \_ -> ilam \_ -> flam \x -> pure $ flam \y ->-                       VBit <$> liftIO (W4.fpEq w4sym x y)-    , "fpIsFinite"  ~> ilam \_ -> ilam \_ -> flam \x ->-                       VBit <$> liftIO do inf <- W4.fpIsInf w4sym x-                                          nan <- W4.fpIsNaN w4sym x-                                          weird <- W4.orPred w4sym inf nan-                                          W4.notPred w4sym weird--    , "fpAdd"       ~> fpBinArithV sym fpPlus-    , "fpSub"       ~> fpBinArithV sym fpMinus-    , "fpMul"       ~> fpBinArithV sym fpMult-    , "fpDiv"       ~> fpBinArithV sym fpDiv--    , "fpFromRational" ~>-       ilam \e -> ilam \p -> wlam sym \r -> pure $ lam \x ->-       do rat <- fromVRational <$> x-          VFloat <$> fpCvtFromRational sym e p r rat--    , "fpToRational" ~>-       ilam \_e -> ilam \_p -> flam \fp ->-       VRational <$> fpCvtToRational sym fp-    ]------ | A helper for definitng floating point constants.-fpConst ::-  W4.IsSymExprBuilder sym =>-  (Integer -> Integer -> IO (W4.SFloat sym)) ->-  Value sym-fpConst mk =-     ilam \ e ->- VNumPoly \ ~(Nat p) ->- VFloat <$> liftIO (mk e p)

@@ -99,6 +99,7 @@ instance FreeVars Expr where   freeVars expr =     case expr of+      ELocated _r t     -> freeVars t       EList es t        -> freeVars es <> freeVars t       ETuple es         -> freeVars es       ERec fs           -> freeVars (recordElements fs)@@ -139,7 +140,7 @@        TUser _ _ t -> freeVars t       TRec fs     -> freeVars (recordElements fs)-+      TNewtype nt ts -> freeVars nt <> freeVars ts  instance FreeVars TVar where   freeVars tv = case tv of@@ -147,14 +148,11 @@                   _         -> mempty  instance FreeVars TCon where-  freeVars tc =-    case tc of-     TC (TCNewtype (UserTC n _)) -> mempty { tyDeps = Set.singleton n }-     _ -> mempty+  freeVars _tc = mempty  instance FreeVars Newtype where   freeVars nt = foldr rmTParam base (ntParams nt)-    where base = freeVars (ntConstraints nt) <> freeVars (map snd (ntFields nt))+    where base = freeVars (ntConstraints nt) <> freeVars (recordElements (ntFields nt))   --------------------------------------------------------------------------------