cryptol 2.8.0 → 2.9.0

raw patch · 101 files changed

+12826/−5962 lines, 101 filesdep +asyncdep +bv-sizeddep +exceptionsdep ~basedep ~base-compatdep ~haskelinePVP ok

version bump matches the API change (PVP)

Dependencies added: async, bv-sized, exceptions, libBF, parameterized-utils, what4

Dependency ranges changed: base, base-compat, haskeline, sbv

API changes (from Hackage documentation)

Files

• CHANGES.md +125/−16
• LICENSE +1/−1
• bench/Main.hs +30/−20
• bench/data/PreludeWithExtras.cry +0/−501
• cryptol.cabal +38/−20
• cryptol/Main.hs +12/−1
• cryptol/REPL/Haskeline.hs +8/−3
• cryptol/REPL/Logo.hs +5/−3
• lib/Array.cry +13/−0
• lib/Cryptol.cry +490/−244
• lib/Float.cry +184/−0
• src/Cryptol/Eval.hs +352/−195
• src/Cryptol/Eval/Backend.hs +705/−0
• src/Cryptol/Eval/Concrete.hs +529/−0
• src/Cryptol/Eval/Concrete/Float.hs +69/−0
• src/Cryptol/Eval/Concrete/FloatHelpers.hs +252/−0
• src/Cryptol/Eval/Concrete/Value.hs +390/−0
• src/Cryptol/Eval/Env.hs +30/−25
• src/Cryptol/Eval/Generic.hs +1965/−0
• src/Cryptol/Eval/Monad.hs +70/−58
• src/Cryptol/Eval/Reference.lhs +593/−191
• src/Cryptol/Eval/SBV.hs +850/−0
• src/Cryptol/Eval/Type.hs +17/−3
• src/Cryptol/Eval/Value.hs +288/−540
• src/Cryptol/Eval/What4.hs +197/−0
• src/Cryptol/Eval/What4/Float.hs +68/−0
• src/Cryptol/Eval/What4/SFloat.hs +361/−0
• src/Cryptol/Eval/What4/Value.hs +975/−0
• src/Cryptol/IR/FreeVars.hs +9/−13
• src/Cryptol/ModuleSystem.hs +16/−13
• src/Cryptol/ModuleSystem/Base.hs +41/−26
• src/Cryptol/ModuleSystem/Env.hs +105/−43
• src/Cryptol/ModuleSystem/Exports.hs +0/−1
• src/Cryptol/ModuleSystem/Fingerprint.hs +0/−1
• src/Cryptol/ModuleSystem/InstantiateModule.hs +2/−3
• src/Cryptol/ModuleSystem/Interface.hs +11/−3
• src/Cryptol/ModuleSystem/Monad.hs +32/−16
• src/Cryptol/ModuleSystem/Name.hs +18/−11
• src/Cryptol/ModuleSystem/NamingEnv.hs +27/−21
• src/Cryptol/ModuleSystem/Renamer.hs +103/−101
• src/Cryptol/Parser.y +21/−20
• src/Cryptol/Parser/AST.hs +52/−15
• src/Cryptol/Parser/Fixity.hs +0/−50
• src/Cryptol/Parser/Lexer.x +16/−3
• src/Cryptol/Parser/LexerUtils.hs +38/−3
• src/Cryptol/Parser/Name.hs +2/−1
• src/Cryptol/Parser/Names.hs +7/−5
• src/Cryptol/Parser/NoInclude.hs +36/−12
• src/Cryptol/Parser/NoPat.hs +6/−12
• src/Cryptol/Parser/ParserUtils.hs +56/−13
• src/Cryptol/Parser/Position.hs +2/−2
• src/Cryptol/Parser/Unlit.hs +2/−2
• src/Cryptol/Parser/Utils.hs +2/−2
• src/Cryptol/Prelude.hs +13/−4
• src/Cryptol/Prims/Eval.hs +0/−1519
• src/Cryptol/REPL/Command.hs +472/−171
• src/Cryptol/REPL/Monad.hs +129/−77
• src/Cryptol/Symbolic.hs +65/−298
• src/Cryptol/Symbolic/Prims.hs +0/−623
• src/Cryptol/Symbolic/SBV.hs +553/−0
• src/Cryptol/Symbolic/Value.hs +0/−250
• src/Cryptol/Symbolic/What4.hs +621/−0
• src/Cryptol/Testing/Concrete.hs +0/−187
• src/Cryptol/Testing/Random.hs +331/−68
• src/Cryptol/Transform/AddModParams.hs +4/−3
• src/Cryptol/Transform/MonoValues.hs +37/−38
• src/Cryptol/Transform/Specialize.hs +17/−20
• src/Cryptol/TypeCheck/AST.hs +13/−13
• src/Cryptol/TypeCheck/CheckModuleInstance.hs +1/−1
• src/Cryptol/TypeCheck/Default.hs +49/−16
• src/Cryptol/TypeCheck/Error.hs +26/−8
• src/Cryptol/TypeCheck/Infer.hs +47/−54
• src/Cryptol/TypeCheck/InferTypes.hs +41/−19
• src/Cryptol/TypeCheck/Kind.hs +7/−7
• src/Cryptol/TypeCheck/Monad.hs +22/−27
• src/Cryptol/TypeCheck/Parseable.hs +3/−2
• src/Cryptol/TypeCheck/Sanity.hs +11/−16
• src/Cryptol/TypeCheck/SimpType.hs +19/−18
• src/Cryptol/TypeCheck/SimpleSolver.hs +17/−5
• src/Cryptol/TypeCheck/Solve.hs +66/−40
• src/Cryptol/TypeCheck/Solver/Class.hs +373/−90
• src/Cryptol/TypeCheck/Solver/Improve.hs +9/−7
• src/Cryptol/TypeCheck/Solver/Numeric.hs +9/−8
• src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs +6/−6
• src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs +10/−2
• src/Cryptol/TypeCheck/Solver/Selector.hs +3/−2
• src/Cryptol/TypeCheck/Solver/Types.hs +13/−1
• src/Cryptol/TypeCheck/Solver/Utils.hs +6/−6
• src/Cryptol/TypeCheck/Subst.hs +47/−13
• src/Cryptol/TypeCheck/TCon.hs +54/−5
• src/Cryptol/TypeCheck/Type.hs +160/−63
• src/Cryptol/TypeCheck/TypeMap.hs +12/−7
• src/Cryptol/TypeCheck/TypeOf.hs +5/−4
• src/Cryptol/TypeCheck/TypePat.hs +2/−9
• src/Cryptol/TypeCheck/Unify.hs +19/−25
• src/Cryptol/Utils/Fixity.hs +55/−0
• src/Cryptol/Utils/Ident.hs +34/−0
• src/Cryptol/Utils/PP.hs +17/−16
• src/Cryptol/Utils/Patterns.hs +4/−1
• src/Cryptol/Utils/RecordMap.hs +202/−0
• utils/CryHtml.hs +1/−0

@@ -1,3 +1,127 @@+# 2.9.0++## Language changes++* Removed the `Arith` class. Replaced it instead with more specialized+  numeric classes: `Ring`, `Integral`, `Field`, and `Round`.  `Ring`+  is the closest analogue to the old `Arith` class; it contains the+  `fromInteger`, `(+)`, `(*)`, `(-)` and `negate` methods.  `Ring`+  contains all the base arithmetic types in Cryptol, and lifts+  pointwise over tuples, sequences and functions, just as `Arith` did.++  The new `Integral` class now contains the integer division and+  modulus methods (`(/)` and `(%)`), and the sequence indexing,+  sequence update and shifting operations are generalized over+  `Integral`.  The `toInteger` operation is also generalized over this+  class.  `Integral` contains the bitvector types and `Integer`.++  The new `Field` class contains types representing mathematical+  fields (or types that are approximately fields). It is currently+  inhabited by the new `Rational` type, and the `Float`+  family of types.  It will  eventually also contain the+  `Real` type. It has the operation `recip` for reciprocal+  and `(/.)` for field division (not to be confused for `(/)`,+  which is Euclidean integral division).++  There is also a new `Round` class for types that can sensibly be+  rounded to integers.  This class has the methods `floor`, `ceiling`,+  `trunc`, `roundToEven`  and `roundAway` for performing different+  kinds of integer rounding.  `Rational` and `Float` inhabit `Round`.++  The type of `(^^)` is modified to be+  `{a, e} (Ring a, Integral e) => a -> e -> a`. This makes it clear+  that the semantics are iterated multiplication, which makes sense+  in any ring.++  Finally, the `lg2`, `(/$)` and `(%$)` methods of Arith have+  had their types specialized so they operate only on bitvectors.++* Added an `Eq` class, and moved the equality operations+  from `Cmp` into `Eq`. The `Z` type becomes a member of `Eq`+  but not `Cmp`.++* Added a base `Rational` type.  It is implemented as a pair of+  integers, quotiented in the usual way.  As such, it reduces to the+  theory of integers and requires no new solver support (beyond+  nonlinear integer arithmetic).  `Rational` inhabits the new+  `Field` and `Round` classes.  Rational values can be+  constructed using the `ratio` function, or via `fromInteger`.++* The `generate` function (and thus `x @ i= e` definitions) has had+  its type specialized so the index type is always `Integer`.++* The new typeclasses are arranged into a class hierarchy, and the+  typechecker will use that information to infer superclass instances+  from subclasses.++* Added a family of base types, `Float e p`, for working with+  floating point numbers.  The parameters control the precision of+  the numbers, with `e` being the number of bits to use in the exponent+  and `p-1` being the number of bits to use in the mantissa.+  The `Float` family of types may be used through the usual overloaded+  functionality in Cryptol, and there is a new built-in module called+  `Float`, which contains functionality specific to floating point numbers.++* Add a way to write fractional literals in base 2,8,10, and 16.+  Fractional literals are overloaded, and may be used for different types+  (currently `Rational` and the `Float` family).  Fractional literal in base+  2,8,and 16 must be precise, and will be rejected statically if they cannot be+  represented exactly.  Fractional literals in base 10 are rounded to the+  nearest even representable number.++* Changes to the defaulting algorithm. The new algorithm only applies+  to constraints arising from literals (i.e., `Literal` and `FLiteral`+  constraints).  The guiding principle is that we now default these+  to one of the infinite precision types `Integer` or `Rational`.+  `Literal` constraints are defaulted to `Integer`, unless the corresponding+  type also has `Field` constraint, in which case we use `Rational`.+  Fractional literal constraints are always defaulted to `Rational.+++## New features++* Document the behavior of lifted selectors.++* Added support for symbolic simulation via the `What4` library+  in addition to the previous method based on `SBV`. The What4+  symbolic simulator is used when selecting solvers with the `w4`+  prefix, such as `w4-z3`, `w4-cvc4`, `w4-yices`, etc.+  The `SBV` and `What4` libraries make different tradeoffs in how+  they represent formulae. You may find one works better than another+  for the same problem, even with the same solver.++* More detailed information about the status of various symbols+  in the output of the `:browse` command (issue #688).++* The `:safe` command will attempt to prove that a given Cryptol+  term is safe; in other words, that it will not encounter a run-time+  error for all inputs. Run-time errors arise from things like+  division-by-zero, index-out-of-bounds situations and+  explicit calls to `error` or `assert`.++* The `:prove` and `:sat` commands now incorporate safety predicates+  by default. In a `:sat` call, models will only be found that do not+  cause run-time errors. For `:prove` calls, the safety conditions are+  added as additional proof goals.  The prior behavior+  (which ignored safety conditions) can be restored using+  `:set ignore-safety = on`.++* Improvements to the `any` prover. It will now shut down external+  prover processes correctly when one finds a solution. It will also+  wait for the first _successful_ result to be returned from a prover,+  instead of failing as soon as one prover fails.++* An experimental `parmap` primitive that applies a function to a+  sequence of arguments and computes the results in parallel.  This+  operation should be considered experimental and may significantly+  change or disappear in the future, and could possibly uncover+  unknown race conditions in the interpreter.++## Bug fixes++* Closed issues #346, #444, #614, #617, #636, #660, #662, #663, #664, #667, #670,+  #702, #711, #712, #716, #723, #725, #731+ # 2.8.0 (September 4, 2019)  ## New features@@ -22,7 +146,7 @@         f : {a} (fin a, a >= 1) => [a] -> [a]          f : {a} (fin a) => (a >= 1) => [a] -> [a]-        + * Added a mechanism for user-defined type constraint operators, and use   this to define the new type constraint synonyms (<) and (>) (issues   #400, #618).@@ -109,18 +233,3 @@ of functions that they expand to (issue #568).  * Closed issues #498, #547, #551, #562, and #563.--## Solver versions--Cryptol can interact with a variety of external SMT solvers to-support the `:prove` and `:sat` commands, and requires Z3 for its-type checker. Many versions of these solvers will work correctly, but-for Yices and Z3 we recommend the following specific versions.--* Z3 4.7.1-* Yices 2.6.1--For Yices, this is the latest version at the time of this writing.-For Z3, it is not, and the latest versions (4.8.x) include changes-that cause some examples that previously succeeded to time out when-type checking.

@@ -1,4 +1,4 @@-Copyright (c) 2013-2019 Galois Inc.+Copyright (c) 2013-2020 Galois Inc. All rights reserved.  Redistribution and use in source and binary forms, with or without

@@ -6,18 +6,21 @@ -- Stability   :  provisional -- Portability :  portable +{-# LANGUAGE ImplicitParams #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} module Main where +import           Control.DeepSeq ( force )+import           Control.Monad.IO.Class( liftIO ) import qualified Data.Text    as T import qualified Data.Text.IO as T import           System.FilePath ((</>)) import qualified System.Directory   as Dir  import qualified Cryptol.Eval as E-import qualified Cryptol.Eval.Monad as E import qualified Cryptol.Eval.Value as E+import qualified Cryptol.Eval.Concrete as C  import qualified Cryptol.ModuleSystem.Base      as M import qualified Cryptol.ModuleSystem.Env       as M@@ -29,8 +32,7 @@ import qualified Cryptol.Parser.AST       as P import qualified Cryptol.Parser.NoInclude as P -import qualified Cryptol.Symbolic as S-import qualified Cryptol.Symbolic.Value as S+import qualified Cryptol.Eval.SBV as S  import qualified Cryptol.TypeCheck     as T import qualified Cryptol.TypeCheck.AST as T@@ -48,7 +50,6 @@   defaultMain [     bgroup "parser" [         parser "Prelude" "lib/Cryptol.cry"-      , parser "PreludeWithExtras" "bench/data/PreludeWithExtras.cry"       , parser "BigSequence" "bench/data/BigSequence.cry"       , parser "BigSequenceHex" "bench/data/BigSequenceHex.cry"       , parser "AES" "bench/data/AES.cry"@@ -56,7 +57,6 @@       ]    , bgroup "typechecker" [         tc cd "Prelude" "lib/Cryptol.cry"-      , tc cd "PreludeWithExtras" "bench/data/PreludeWithExtras.cry"       , tc cd "BigSequence" "bench/data/BigSequence.cry"       , tc cd "BigSequenceHex" "bench/data/BigSequenceHex.cry"       , tc cd "AES" "bench/data/AES.cry"@@ -107,21 +107,25 @@                 }             Right pm = P.parseModule cfg bytes         menv <- M.initialModuleEnv-        (Right ((prims, scm, tcEnv), menv'), _) <- M.runModuleM (evOpts,menv) $ withLib $ do+        (eres, _) <-  M.runModuleM (evOpts,menv) $ withLib $ do           -- code from `loadModule` and `checkModule` in           -- `Cryptol.ModuleSystem.Base`           let pm' = M.addPrelude pm           M.loadDeps pm'-          Right nim <- M.io (P.removeIncludesModule path pm')+          enim <- M.io (P.removeIncludesModule path pm')+          nim <- either (error "Failed to remove includes") return enim           npm <- M.noPat nim           (tcEnv,declsEnv,scm) <- M.renameModule npm           prims <- if P.thing (P.mName pm) == I.preludeName                    then return (M.toPrimMap declsEnv)                    else M.getPrimMap           return (prims, scm, tcEnv)-        return (prims, scm, tcEnv, menv')+        case eres of+          Right ((prims, scm, tcEnv), menv') ->+            return (prims, scm, tcEnv, menv')+          Left _ -> error $ "Failed to load " ++ name   in env setup $ \ ~(prims, scm, tcEnv, menv) ->-    bench name $ nfIO $ M.runModuleM (evOpts,menv) $ withLib $ do+    bench name $ whnfIO $ M.runModuleM (evOpts,menv) $ withLib $ do       let act = M.TCAction { M.tcAction = T.tcModule                            , M.tcLinter = M.moduleLinter (P.thing (P.mName scm))                            , M.tcPrims  = prims@@ -133,17 +137,20 @@   let withLib = M.withPrependedSearchPath [cd </> "lib"] in   let setup = do         menv <- M.initialModuleEnv-        (Right (texpr, menv'), _) <- M.runModuleM (evOpts,menv) $ withLib $ do+        (eres, _) <-  M.runModuleM (evOpts,menv) $ withLib $ do           m <- M.loadModuleByPath path           M.setFocusedModule (T.mName m)           let Right pexpr = P.parseExpr expr           (_, texpr, _) <- M.checkExpr pexpr           return texpr-        return (texpr, menv')+        case eres of+          Right (texpr, menv') -> return (texpr, menv')+          Left _ ->  error $ "Failed to load " ++ name   in env setup $ \ ~(texpr, menv) ->     bench name $ nfIO $ E.runEval evOpts $ do-      env' <- E.evalDecls (S.allDeclGroups menv) mempty-      (e :: E.Value) <- E.evalExpr env' texpr+      let ?evalPrim = C.evalPrim+      env' <- E.evalDecls C.Concrete (M.allDeclGroups menv) mempty+      (e :: C.Value) <- E.evalExpr C.Concrete env' texpr       E.forceValue e  @@ -152,16 +159,19 @@   let withLib = M.withPrependedSearchPath [cd </> "lib"] in   let setup = do         menv <- M.initialModuleEnv-        (Right (texpr, menv'), _) <- M.runModuleM (evOpts,menv) $ withLib $ do+        (eres, _) <-  M.runModuleM (evOpts,menv) $ withLib $ do           m <- M.loadModuleByPath path           M.setFocusedModule (T.mName m)           let Right pexpr = P.parseExpr expr           (_, texpr, _) <- M.checkExpr pexpr           return texpr-        return (texpr, menv')+        case eres of+          Right (texpr, menv') -> return (texpr, menv')+          Left _ ->  error $ "Failed to load " ++ name   in env setup $ \ ~(texpr, menv) ->-    bench name $ nfIO $ E.runEval evOpts $ do-      env' <- E.evalDecls (S.allDeclGroups menv) mempty-      (e :: S.Value) <- E.evalExpr env' texpr-      E.io $ SBV.generateSMTBenchmark False $-         return (S.fromVBit e)+    bench name $ whnfIO $ fmap force E.runEval evOpts $ S.sbvEval $ do+      let ?evalPrim = S.evalPrim+      env' <- E.evalDecls S.SBV (M.allDeclGroups menv) mempty+      (e :: S.Value) <- E.evalExpr S.SBV env' texpr+      liftIO $ SBV.generateSMTBenchmark False $+         return (E.fromVBit e)

@@ -1,501 +0,0 @@-/*- * Copyright (c) 2013-2016 Galois, Inc.- * Distributed under the terms of the BSD3 license (see LICENSE file)- */--module Cryptol where--/**- * The value corresponding to a numeric type.- */-primitive number : {val, bits} (fin val, fin bits, bits >= width val) => [bits]--infixr 10 ||-infixr 20 &&-infix  30 ==, ===, !=, !==-infix  40 >, >=, <, <=-infixl 50 ^-infixr 60 #-infixl 70 <<, <<<, >>, >>>-infixl 80 +, --infixl 90 *, /, %-infixr 95 ^^-infixl 100 @, @@, !, !!--/**- * Add two values.- *  * For words, addition uses modulo arithmetic.- *  * Structured values are added element-wise.- */-primitive (+) : {a} (Arith a) => a -> a -> a--/**- * For words, subtraction uses modulo arithmetic.- * Structured values are subtracted element-wise. Defined as:- * a - b = a + negate b- * See also: `negate'.- */-primitive (-) : {a} (Arith a) => a -> a -> a--/**- * For words, multiplies two words, modulus 2^^a.- * Structured values are multiplied element-wise.- */-primitive (*) : {a} (Arith a) => a -> a -> a--/**- * For words, divides two words, modulus 2^^a.- * Structured values are divided element-wise.- */-primitive (/) : {a} (Arith a) => a -> a -> a--/**- * For words, takes the modulus of two words, modulus 2^^a.- * Over structured values, operates element-wise.- * Be careful, as this will often give unexpected results due to interaction of- * the two moduli.- */-primitive (%) : {a} (Arith a) => a -> a -> a--/**- * For words, takes the exponent of two words, modulus 2^^a.- * Over structured values, operates element-wise.- * Be careful, due to its fast-growing nature, exponentiation is prone to- * interacting poorly with defaulting.- */-primitive (^^) : {a} (Arith a) => a -> a -> a--/**- * Log base two.- *- * For words, computes the ceiling of log, base 2, of a number.- * Over structured values, operates element-wise.- */-primitive lg2 : {a} (Arith a) => a -> a---type Bool = Bit--/**- * The constant True. Corresponds to the bit value 1.- */-primitive True  : Bit--/**- * The constant False. Corresponds to the bit value 0.- */-primitive False : Bit--/**- * Returns the twos complement of its argument.- * Over structured values, operates element-wise.- * negate a = ~a + 1- */-primitive negate : {a} (Arith a) => a -> a--/**- * Binary complement.- */-primitive complement : {a} a -> a--/**- * Operator form of binary complement.- */-(~) : {a} a -> a-(~) = complement--/**- * Less-than. Only works on comparable arguments.- */-primitive (<) : {a} (Cmp a) => a -> a -> Bit--/**- * Greater-than of two comparable arguments.- */-primitive (>) : {a} (Cmp a) => a -> a -> Bit--/**- * Less-than or equal of two comparable arguments.- */-primitive (<=) : {a} (Cmp a) => a -> a -> Bit--/**- * Greater-than or equal of two comparable arguments.- */-primitive (>=) : {a} (Cmp a) => a -> a -> Bit--/**- * Compares any two values of the same type for equality.- */-primitive (==) : {a} (Cmp a) => a -> a -> Bit--/**- * Compares any two values of the same type for inequality.- */-primitive (!=) : {a} (Cmp a) => a -> a -> Bit--/**- * Compare the outputs of two functions for equality- */-(===) : {a,b} (Cmp b) => (a -> b) -> (a -> b) -> (a -> Bit)-f === g = \ x -> f x == g x--/**- * Compare the outputs of two functions for inequality- */-(!==) : {a,b} (Cmp b) => (a -> b) -> (a -> b) -> (a -> Bit)-f !== g = \x -> f x != g x--/**- * Returns the smaller of two comparable arguments.- */-min : {a} (Cmp a) => a -> a -> a-min x y = if x < y then x else y--/**- * Returns the greater of two comparable arguments.- */-max : {a} (Cmp a) => a -> a -> a-max x y = if x > y then x else y--/**- * Logical `and' over bits. Extends element-wise over sequences, tuples.- */-primitive (&&) : {a} a -> a -> a--/**- * Logical `or' over bits. Extends element-wise over sequences, tuples.- */-primitive (||) : {a} a -> a -> a--/**- * Logical `exclusive or' over bits. Extends element-wise over sequences, tuples.- */-primitive (^) : {a} a -> a -> a--/**- * Gives an arbitrary shaped value whose bits are all False.- * ~zero likewise gives an arbitrary shaped value whose bits are all True.- */-primitive zero : {a} a--/**- * Left shift.  The first argument is the sequence to shift, the second is the- * number of positions to shift by.-*/-primitive (<<) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c--/**- * Right shift.  The first argument is the sequence to shift, the second is the- * number of positions to shift by.- */-primitive (>>) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c--/**- * Left rotate.  The first argument is the sequence to rotate, the second is the- * number of positions to rotate by.- */-primitive (<<<) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c--/**- * Right rotate.  The first argument is the sequence to rotate, the second is- * the number of positions to rotate by.- */-primitive (>>>) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c--primitive (#) : {front, back, a} (fin front) => [front]a -> [back]a-                                             -> [front + back] a---/**- * Split a sequence into a tuple of sequences.- */-primitive splitAt : {front, back, a} (fin front) => [front + back]a-                                                 -> ([front]a, [back]a)-/**- * Joins sequences.- */-primitive join : {parts, each, a} (fin each) => [parts][each]a-                                             -> [parts * each]a--/**- * Splits a sequence into 'parts' groups with 'each' elements.- */-primitive split : {parts, each, a} (fin each) => [parts * each]a-                                              -> [parts][each]a--/**- * Reverses the elements in a sequence.- */-primitive reverse : {a, b} (fin a) => [a]b -> [a]b--/**- * Transposes an [a][b] matrix into a [b][a] matrix.- */-primitive transpose : {a, b, c} [a][b]c -> [b][a]c--/**- * Index operator.  The first argument is a sequence.  The second argument is- * the zero-based index of the element to select from the sequence.- */-primitive (@) : {a, b, c} (fin c) => [a]b -> [c] -> b--/**- * Bulk index operator.  The first argument is a sequence.  The second argument- * is a sequence of the zero-based indices of the elements to select.- */-primitive (@@) : {a, b, c, d} (fin d) => [a]b -> [c][d] -> [c]b--/**- * Reverse index operator.  The first argument is a finite sequence.  The second- * argument is the zero-based index of the element to select, starting from the- * end of the sequence.- */-primitive (!) : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b--/**- * Bulk reverse index operator.  The first argument is a finite sequence.  The- * second argument is a sequence of the zero-based indices of the elements to- z select, starting from the end of the sequence.- */-primitive (!!) : {a, b, c, d} (fin a, fin d) => [a]b -> [c][d] -> [c]b--primitive fromTo : {first, last, bits} (fin last, fin bits, last >= first,-                              bits >= width last) => [1 + (last - first)][bits]--primitive fromThenTo : {first, next, last, bits, len} (fin first, fin next,-                        fin last, fin bits, bits >= width first,-                        bits >= width next, bits >= width last,-                        lengthFromThenTo first next last == len) => [len][bits]--primitive infFrom : {bits} (fin bits) => [bits] -> [inf][bits]--primitive infFromThen : {bits} (fin bits) => [bits] -> [bits] -> [inf][bits]--primitive error : {at, len} (fin len) => [len][8] -> at---/**- * Performs multiplication of polynomials over GF(2).- */-primitive pmult : {a, b} (fin a, fin b) => [a] -> [b] -> [max 1 (a + b) - 1]--/**- * Performs division of polynomials over GF(2).- */-primitive pdiv : {a, b} (fin a, fin b) => [a] -> [b] -> [a]--/**- * Performs modulus of polynomials over GF(2).- */-primitive pmod : {a, b} (fin a, fin b) => [a] -> [1 + b] -> [b]--/**- * Generates random values from a seed.  When called with a function, currently- * generates a function that always returns zero.- */-primitive random : {a} [256] -> a--type String n = [n][8]-type Word n = [n]-type Char   = [8]--take : {front,back,elem} (fin front) => [front + back] elem -> [front] elem-take (x # _) = x--drop : {front,back,elem} (fin front) => [front + back] elem -> [back] elem-drop ((_ : [front] _) # y) = y--tail : {a, b} [1 + a]b -> [a]b-tail xs = drop`{1} xs--width : {bits,len,elem} (fin len, fin bits, bits >= width len) => [len] elem -> [bits]-width _ = `len--undefined : {a} a-undefined = error "undefined"--groupBy : {each,parts,elem} (fin each) =>-  [parts * each] elem -> [parts][each]elem-groupBy = split`{parts=parts}--/**- * Define the base 2 logarithm function in terms of width- */-type lg2 n = width (max n 1 - 1)--/**- * Debugging function for tracing.  The first argument is a string,- * which is prepended to the printed value of the second argument.- * This combined string is then printed when the trace function is- * evaluated.  The return value is equal to the third argument.- *- * The exact timing and number of times the trace message is printed- * depend on the internal details of the Cryptol evaluation order,- * which are unspecified.  Thus, the output produced by this- * operation may be difficult to predict.- */-primitive trace : {n, a, b} [n][8] -> a -> b -> b--/**- * Debugging function for tracing values.  The first argument is a string,- * which is prepended to the printed value of the second argument.- * This combined string is then printed when the trace function is- * evaluated.  The return value is equal to the second argument.- *- * The exact timing and number of times the trace message is printed- * depend on the internal details of the Cryptol evaluation order,- * which are unspecified.  Thus, the output produced by this- * operation may be difficult to predict.- */-traceVal : {n, a} [n][8] -> a -> a-traceVal msg x = trace msg x x--/*- * Copyright (c) 2016 Galois, Inc.- * Distributed under the terms of the BSD3 license (see LICENSE file)- *- * This module contains definitions that we wish to eventually promote- * into the Prelude, but which currently cause typechecking of the- * Prelude to take too long (see #299)- */--infixr 5 ==>--/**- * Logical implication- */-(==>) : Bit -> Bit -> Bit-a ==> b = if a then b else True--/**- * Logical negation- */-not : {a} a -> a-not a = ~ a--/**- * Conjunction- */-and : {n} (fin n) => [n]Bit -> Bit-and xs = ~zero == xs--/**- * Disjunction- */-or : {n} (fin n) => [n]Bit -> Bit-or xs = zero != xs--/**- * Conjunction after applying a predicate to all elements.- */-all : {a,n} (fin n) => (a -> Bit) -> [n]a -> Bit-all f xs = and (map f xs)--/**- * Disjunction after applying a predicate to all elements.- */-any : {a,n} (fin n) => (a -> Bit) -> [n]a -> Bit-any f xs = or (map f xs)--/**- * Map a function over an array.- */-map : {a, b, n} (a -> b) -> [n]a -> [n]b-map f xs = [f x | x <- xs]--/**- * Functional left fold.- *- * foldl (+) 0 [1,2,3] = ((0 + 1) + 2) + 3- */-foldl : {a, b, n} (fin n) => (a -> b -> a) -> a -> [n]b -> a-foldl f acc xs = ys ! 0- where ys = [acc] # [f a x | a <- ys | x <- xs]--/**- * Functional right fold.- *- * foldr (-) 0 [1,2,3] = 0 - (1 - (2 - 3))- */-foldr : {a,b,n} (fin n) => (a -> b -> b) -> b -> [n]a -> b-foldr f acc xs = ys ! 0- where ys = [acc] # [f x a | a <- ys | x <- reverse xs]--/**- * Compute the sum of the words in the array.- */-sum : {a,n} (fin n, Arith a) => [n]a -> a-sum xs = foldl (+) zero xs--/**- * Scan left is like a fold that emits the intermediate values.- */-scanl : {b, a, n}  (b -> a -> b) -> b -> [n]a -> [n+1]b-scanl f acc xs = ys- where-  ys = [acc] # [f a x | a <- ys | x <- xs]--/**- * Scan right- */-scanr : {a,b,n} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b-scanr f acc xs = reverse ys-    where-     ys = [acc] # [f x a | a <- ys | x <- reverse xs]--/**- * Zero extension- */-extend : {total,n} (fin total, fin n, total >= n) => [n]Bit -> [total]Bit-extend n = zero # n--/**- * Signed extension. `extendSigned 0bwxyz : [8] == 0bwwwwwxyz`.- */-extendSigned : {total,n} (fin total, fin n, n >= 1, total >= n+1) => [n]Bit -> [total]Bit-extendSigned  xs = repeat (xs @ 0) # xs--/**- * Repeat a value.- */-repeat : {n, a} a -> [n]a-repeat x = [ x | _ <- zero ]--/**- * `elem x xs` Returns true if x is equal to a value in xs.- */-elem : {n,a} (fin n, Cmp a) => a -> [n]a -> Bit-elem a xs = any (\x -> x == a) xs--/**- * Create a list of tuples from two lists.- */-zip : {a,b,n} [n]a -> [n]b -> [n](a,b)-zip xs ys = [(x,y) | x <- xs | y <- ys]--/**- * Create a list by applying the function to each pair of elements in the input.- * lists- */-zipWith : {a,b,c,n} (a -> b -> c) -> [n]a -> [n]b -> [n]c-zipWith f xs ys = [f x y | x <- xs | y <- ys]--/**- * Transform a function into uncurried form.- */-uncurry : {a,b,c} (a -> b -> c) -> (a,b) -> c-uncurry f = \(a,b) -> f a b--/**- * Transform a function into curried form.- */-curry : {a,b,c} ((a, b) -> c) -> a -> b -> c-curry f = \a b -> f (a,b)--/**- * Map a function iteratively over a seed value, producing an infinite- * list of successive function applications.- */-iterate : { a } (a -> a) -> a -> [inf]a-iterate f x = [x] # [ f v | v <- iterate f x ]

@@ -1,5 +1,5 @@ Name:                cryptol-Version:             2.8.0+Version:             2.9.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:             BSD3@@ -8,7 +8,7 @@ Maintainer:          cryptol@galois.com Homepage:            http://www.cryptol.net/ Bug-reports:         https://github.com/GaloisInc/cryptol/issues-Copyright:           2013-2019 Galois Inc.+Copyright:           2013-2020 Galois Inc. Category:            Language Build-type:          Simple Cabal-version:       1.18@@ -25,7 +25,7 @@ source-repository this   type:     git   location: https://github.com/GaloisInc/cryptol.git-  tag:      2.8.0+  tag:      2.9.0  flag static   default: False@@ -44,42 +44,44 @@   Default-language:     Haskell2010   Build-depends:       base              >= 4.8 && < 5,-                       base-compat       >= 0.6 && < 0.11,+                       async             >= 2.2 && < 2.3,+                       base-compat       >= 0.6 && < 0.12,+                       bv-sized          >= 1.0 && < 1.1,                        bytestring        >= 0.10,                        array             >= 0.4,                        containers        >= 0.5,                        cryptohash-sha1   >= 0.11 && < 0.12,                        deepseq           >= 1.3,                        directory         >= 1.2.2.0,+                       exceptions,                        filepath          >= 1.3,                        gitrev            >= 1.0,                        GraphSCC          >= 1.0.4,                        heredoc           >= 0.2,+                       libBF             >= 0.5.1,                        monad-control     >= 1.0,                        monadLib          >= 3.7.2,+                       parameterized-utils >= 2.0.2,                        pretty            >= 1.1,                        process           >= 1.2,                        random            >= 1.0.1,-                       sbv               >= 8.1,+                       sbv               >= 8.6,                        simple-smt        >= 0.7.1,                        strict,                        text              >= 1.1,                        tf-random         >= 0.5,                        transformers-base >= 0.4,                        mtl               >= 2.2.1,-                       time >= 1.6.0.1,-                       panic >= 0.3-+                       time              >= 1.6.0.1,+                       panic             >= 0.3,+                       what4             >= 1.0 && < 1.1    Build-tools:         alex, happy   hs-source-dirs:      src -  Exposed-modules:     Cryptol.Prims.Eval,--                       Cryptol.Parser,+  Exposed-modules:     Cryptol.Parser,                        Cryptol.Parser.Lexer,                        Cryptol.Parser.AST,-                       Cryptol.Parser.Fixity,                        Cryptol.Parser.Position,                        Cryptol.Parser.Names,                        Cryptol.Parser.Name,@@ -89,7 +91,9 @@                        Cryptol.Parser.Utils,                        Cryptol.Parser.Unlit, +                       Cryptol.Utils.Fixity,                        Cryptol.Utils.Ident,+                       Cryptol.Utils.RecordMap,                        Cryptol.Utils.PP,                        Cryptol.Utils.Panic,                        Cryptol.Utils.Debug,@@ -155,18 +159,28 @@                         Cryptol.Eval,                        Cryptol.Eval.Arch,+                       Cryptol.Eval.Backend,+                       Cryptol.Eval.Concrete,+                       Cryptol.Eval.Concrete.Float,+                       Cryptol.Eval.Concrete.FloatHelpers,+                       Cryptol.Eval.Concrete.Value,                        Cryptol.Eval.Env,+                       Cryptol.Eval.Generic,                        Cryptol.Eval.Monad,                        Cryptol.Eval.Reference,+                       Cryptol.Eval.SBV,                        Cryptol.Eval.Type,                        Cryptol.Eval.Value,+                       Cryptol.Eval.What4,+                       Cryptol.Eval.What4.Value,+                       Cryptol.Eval.What4.Float,+                       Cryptol.Eval.What4.SFloat, -                       Cryptol.Testing.Concrete,                        Cryptol.Testing.Random,                         Cryptol.Symbolic,-                       Cryptol.Symbolic.Prims,-                       Cryptol.Symbolic.Value,+                       Cryptol.Symbolic.SBV,+                       Cryptol.Symbolic.What4,                         Cryptol.REPL.Command,                        Cryptol.REPL.Monad,@@ -178,10 +192,12 @@                        Paths_cryptol,                        GitRev -  GHC-options:         -Wall -fsimpl-tick-factor=140+  GHC-options:         -Wall -fsimpl-tick-factor=140 -O2   if impl(ghc >= 8.0.1)      ghc-options: -Wno-redundant-constraints +  ghc-prof-options: -O2 -fprof-auto-top+   if flag(relocatable)       cpp-options: -DRELOCATABLE @@ -201,14 +217,16 @@                      , cryptol                      , directory                      , filepath-                     , haskeline+                     , haskeline >= 0.7 && < 0.9                      , monad-control                      , text                      , transformers-  GHC-options:         -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m"+  GHC-options:         -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m" -O2   if impl(ghc >= 8.0.1)      ghc-options: -Wno-redundant-constraints +  ghc-prof-options: -O2 -fprof-auto-top+   if os(linux) && flag(static)       ld-options:      -static -pthread @@ -256,7 +274,7 @@   main-is:             Main.hs   hs-source-dirs:      bench   default-language:    Haskell2010-  GHC-options:         -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m"+  GHC-options:         -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m" -O2   if impl(ghc >= 8.0.1)      ghc-options: -Wno-redundant-constraints   if os(linux) && flag(static)@@ -267,5 +285,5 @@                      , deepseq                      , directory                      , filepath-                     , sbv >= 8.1+                     , sbv                      , text

@@ -55,6 +55,7 @@   , optCryptolrc       :: Cryptolrc   , optCryptolPathOnly :: Bool   , optStopOnError     :: Bool+  , optNoUnicodeLogo   :: Bool   } deriving (Show)  defaultOptions :: Options@@ -68,6 +69,7 @@   , optCryptolrc       = CryrcDefault   , optCryptolPathOnly = False   , optStopOnError     = False+  , optNoUnicodeLogo   = False   }  options :: [OptDescr (OptParser Options)]@@ -95,6 +97,9 @@   , Option "h" ["help"] (NoArg setHelp)     "display this message" +  , Option "" ["no-unicode-logo"] (NoArg setNoUnicodeLogo)+    "Don't use unicode characters in the REPL logo"+   , Option ""  ["ignore-cryptolrc"] (NoArg setCryrcDisabled)     "disable reading of .cryptolrc files" @@ -130,6 +135,10 @@ setColorMode "always" = modify $ \ opts -> opts { optColorMode = AlwaysColor } setColorMode x        = OptFailure ["invalid color mode: " ++ x ++ "\n"] +-- | Disable unicde characters in the REPL logo+setNoUnicodeLogo :: OptParser Options+setNoUnicodeLogo = modify $ \opts -> opts { optNoUnicodeLogo = True }+ -- | Signal that version should be displayed. setVersion :: OptParser Options setVersion  = modify $ \ opts -> opts { optVersion = True }@@ -257,7 +266,9 @@     AlwaysColor -> return True     NoColor     -> return False     AutoColor   -> canDisplayColor-  displayLogo color++  let useUnicode = not (optNoUnicodeLogo opts)+  displayLogo color useUnicode    setUpdateREPLTitle (shouldSetREPLTitle >>= \b -> when b setREPLTitle)   updateREPLTitle

@@ -6,6 +6,7 @@ -- Stability   :  provisional -- Portability :  portable +{-# LANGUAGE CPP #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE PatternGuards #-} {-# OPTIONS_GHC -fno-warn-orphans #-}@@ -22,20 +23,22 @@ import qualified Control.Exception as X import           Control.Monad (guard, join) import qualified Control.Monad.Trans.Class as MTL+#if !MIN_VERSION_haskeline(0,8,0) import           Control.Monad.Trans.Control+#endif import           Data.Char (isAlphaNum, isSpace)-import           Data.Maybe(isJust) 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.IO (stdout) import           System.Console.ANSI (setTitle, hSupportsANSI) import           System.Console.Haskeline import           System.Directory ( doesFileExist                                   , getHomeDirectory                                   , getCurrentDirectory) import           System.FilePath ((</>))+import           System.IO (stdout)  import           Prelude () import           Prelude.Compat@@ -128,7 +131,7 @@ setHistoryFile ss =   do dir <- getHomeDirectory      return ss { historyFile = Just (dir </> ".cryptol_history") }-   `X.catch` \(SomeException {}) -> return ss+   `X.catch` \(X.SomeException {}) -> return ss  -- | Haskeline settings for the REPL. replSettings :: Bool -> Settings REPL@@ -159,9 +162,11 @@  -- Utilities ------------------------------------------------------------------- +#if !MIN_VERSION_haskeline(0,8,0) instance MonadException REPL where   controlIO f = join $ liftBaseWith $ \f' ->     f $ RunIO $ \m -> restoreM <$> (f' m)+#endif  -- Titles ---------------------------------------------------------------------- 

@@ -35,15 +35,17 @@   versionText = "version " ++ showVersion version ++ hashText   ver = sgr [SetColor Foreground Dull White]         ++ replicate (lineLen - 20 - length versionText) ' '-        ++ versionText+        ++ versionText ++ "\n"+        ++ "https://cryptol.net  :? for help"   ls        = mk ver   slen      = length ls `div` 3   (ws,rest) = splitAt slen ls   (vs,ds)   = splitAt slen rest   lineLen   = length (head ls) -displayLogo :: Bool -> REPL ()-displayLogo useColor = unlessBatch (io (mapM_ putStrLn (logo useColor logo2)))+displayLogo :: Bool -> Bool -> REPL ()+displayLogo useColor useUnicode =+  unlessBatch (io (mapM_ putStrLn (logo useColor (if useUnicode then logo2 else logo1))))  logo1 :: String -> [String] logo1 ver =

@@ -0,0 +1,13 @@+/*+ * Copyright (c) 2020 Galois, Inc.+ * Distributed under the terms of the BSD3 license (see LICENSE file)+ */++module Array where++primitive type Array : * -> * -> *++primitive arrayConstant : {a, b} b -> (Array a b)+primitive arrayLookup : {a, b} (Array a b) -> a -> b+primitive arrayUpdate : {a, b} (Array a b) -> a -> b -> (Array a b)+

@@ -1,21 +1,10 @@ /*- * Copyright (c) 2013-2016 Galois, Inc.+ * Copyright (c) 2013-2020 Galois, Inc.  * Distributed under the terms of the BSD3 license (see LICENSE file)  */  module Cryptol where -/**- * The value corresponding to a numeric type.- */-primitive number : {val, rep} Literal val rep => rep--/**- * An alternative name for 'number', present for backward compatibility.- */-demote : {val, rep} Literal val rep => rep-demote = number`{val}- infixr  5 ==> infixr 10 \/ infixr 15 /\@@ -31,10 +20,8 @@ infixr 95 ^^ infixl 100 @, @@, !, !! -// ----------------------------------------------------------------------------- -/** A numeric type representing infinity. */-primitive type inf : #+// Base types -----------------------------------------------------------------------  /** The type of boolean values. */ primitive type Bit : *@@ -42,11 +29,45 @@ /** The type of unbounded integers. */ primitive type Integer : * -/** 'Z n' is the type of integers, modulo 'n'. */+/**+ * 'Z n' is the type of integers, modulo 'n'.+ *+ * The values of 'Z n' may be thought of as equivalance+ * classes of integers according to the equivalence+ * 'x ~ y' iff 'n' divides 'x - y'.  'Z n' naturally+ * forms a ring, but does not support integral division+ * or indexing.+ *+ * However, you may use the 'fromZ' operation+ * to project values in 'Z n' into the integers if such operations+ * are required.  This will compute the reduced representative+ * of the equivalance class. In other words, 'fromZ' computes+ * the (unique) integer value 'i'  where '0 <= i < n' and+ * 'i' is in the given equivalance class.+ */ primitive type {n : #} (fin n, n >= 1) => Z n : * +/**+ * 'Rational' is the type of rational numbers.+ * Rational numbers form a Field (and thus a Ring).+ *+ * The 'ratio' operation may be used to directly create+ * rational values from as a ratio of integers, or+ * the 'fromInteger' method and the field operations+ * can be used.+ */+primitive type Rational : * +type Bool = Bit+type Word n = [n]+type Char = [8]+type String n = [n]Char +// Numeric operators and constraints ----------------------------------------------++/** A numeric type representing infinity. */+primitive type inf : #+ /** Assert that two numeric types are equal. */ primitive type (==) : # -> # -> Prop @@ -57,40 +78,20 @@ primitive type (>=) : # -> # -> Prop  /** Assert that a numeric type is a proper natural number (not 'inf'). */-primitive type fin : * -> Prop--/** Value types that have a notion of 'zero'. */-primitive type Zero : * -> Prop--/** Value types that support logical operations. */-primitive type Logic : * -> Prop--/** Value types that support arithmetic. */-primitive type Arith : * -> Prop--/** Value types that support unsigned comparisons. */-primitive type Cmp : * -> Prop--/** Value types that support signed comparisons. */-primitive type SignedCmp : * -> Prop--/** 'Literal n a' asserts that type 'a' contains the number 'n'. */-primitive type Literal : # -> * -> Prop--+primitive type fin : # -> Prop  /** Add numeric types. */ primitive type (+) : # -> # -> # +/** Multiply numeric types. */+primitive type (*) : # -> # -> #+ /** Subtract numeric types. */ primitive type   {m : #, n : # }   (fin n, m >= n) =>   m - n : # -/** Multiply numeric types. */-primitive type (*) : # -> # -> #- /** Divide numeric types, rounding down. */ primitive type   { m : #, n : # }@@ -109,6 +110,11 @@ /** The number of bits required to represent the value of a numeric type. */ primitive type width : # -> # +/**+ * Define the base 2 logarithm function in terms of width+ */+type lg2 n = width (max n 1 - 1)+ /** The smaller of two numeric types. */ primitive type min : # -> # -> # @@ -133,11 +139,6 @@   (fin start, fin next, fin last, start != next) =>   lengthFromThenTo start next last : # ----// ------------------------------------------------------------------------------ /**  * Assert that the first numeric type is less than or equal to the second.  */@@ -153,12 +154,132 @@  */ type constraint i < j = j >= i + 1 ++// The Literal class ----------------------------------------------------++/** 'Literal n a' asserts that type 'a' contains the number 'n'. */+primitive type Literal : # -> * -> Prop+ /**+ * The value corresponding to a numeric type.+ */+primitive number : {val, rep} Literal val rep => rep++/**+ * An alternative name for 'number', present for backward compatibility.+ */+demote : {val, rep} Literal val rep => rep+demote = number`{val}++/**+ * Return the length of a sequence.  Note that the result depends only+ * on the type of the argument, not its value.+ */+length : {n, a, b} (fin n, Literal n b) => [n]a -> b+length _ = `n++/**+ * A finite sequence counting up from 'first' to 'last'.+ *+ * '[a..b]' is syntactic sugar for 'fromTo`{first=a,last=b}'.+ */+primitive fromTo : {first, last, a} (fin last, last >= first,+                                    Literal first a, Literal last a) =>+                                    [1 + (last - first)]a++/**+ * A finite arithmetic sequence starting with 'first' and 'next',+ * stopping when the values reach or would skip over 'last'.+ *+ * '[a,b..c]' is syntactic sugar for 'fromThenTo`{first=a,next=b,last=c}'.+ */+primitive fromThenTo : {first, next, last, a, len}+                       ( fin first, fin next, fin last+                       , Literal first a, Literal next a, Literal last a+                       , first != next+                       , lengthFromThenTo first next last == len) => [len]a++// Fractional Literals ---------------------++/** 'FLiteral m n r a' asserts that the type `a' contains the+fraction `m/n`.  The flag `r` indicates if we should round (`r >= 1`)+or report an error if the number can't be represented exactly. */+primitive type FLiteral : # -> # -> # -> * -> Prop++/** A fractional literal corresponding to `m/n` */+primitive+  fraction : { m, n, r, a } FLiteral m n r a => a++++++++// The Zero class -------------------------------------------------------++/** Value types that have a notion of 'zero'. */+primitive type Zero : * -> Prop++/**+ * Gives an arbitrary shaped value whose bits are all False.+ * ~zero likewise gives an arbitrary shaped value whose bits are all True.+ */+primitive zero : {a} (Zero a) => a+++// The Logic class ------------------------------------------------------++/** Value types that support logical operations. */+primitive type Logic : * -> Prop++/**+ * Logical 'and' over bits. Extends element-wise over sequences, tuples.+ */+primitive (&&) : {a} (Logic a) => a -> a -> a++/**+ * Logical 'or' over bits. Extends element-wise over sequences, tuples.+ */+primitive (||) : {a} (Logic a) => a -> a -> a++/**+ * Logical 'exclusive or' over bits. Extends element-wise over sequences, tuples.+ */+primitive (^) : {a} (Logic a) => a -> a -> a++/**+ * Bitwise complement. The prefix notation '~ x'+ * is syntactic sugar for 'complement x'.+ */+primitive complement : {a} (Logic a) => a -> a+++// The Ring class -------------------------------------------------------++/**+ * Value types that support ring addition and multiplication.+ *+ * Floating-point values are only approximately a ring, but+ * nonetheless inhabit this class.+ */+primitive type Ring : * -> Prop++/**+ * Converts an unbounded integer to a value in a Ring. When converting+ * to the bitvector type [n], the value is reduced modulo 2^^n. Likewise,+ * when converting to Z n, the value is reduced modulo n.  When converting+ * to a floating-point value, the value is rounded to the nearest+ * representable value.+ */+primitive fromInteger : {a} (Ring a) => Integer -> a++/**  * Add two values.  *  * For type [n], addition is modulo 2^^n.  *  * Structured values are added element-wise.  */-primitive (+) : {a} (Arith a) => a -> a -> a+primitive (+) : {a} (Ring a) => a -> a -> a  /**  * Subtract two values.@@ -167,128 +288,218 @@  *  * Satisfies 'a - b = a + negate b'.  * See also: 'negate'.  */-primitive (-) : {a} (Arith a) => a -> a -> a+primitive (-) : {a} (Ring a) => a -> a -> a  /**  * Multiply two values.  *  * For type [n], multiplication is modulo 2^^n.  *  * Structured values are multiplied element-wise.  */-primitive (*) : {a} (Arith a) => a -> a -> a+primitive (*) : {a} (Ring a) => a -> a -> a  /**- * Divide two values, rounding down.+ * Returns the additive inverse of its argument.+ * Over structured values, operates element-wise.+ * The prefix notation '- x' is syntactic sugar+ * for 'negate x'.+ *+ * Satisfies 'a + negate a = 0'.+ * Satisfies 'negate a = ~a + 1' for bitvector values.+ */+primitive negate : {a} (Ring a) => a -> a+++// The Integral class -------------------------------------------------++/**+ * Value types that correspond to a segment of the+ * integers. These types support integer division and+ * modulus, indexing into sequences, and enumeration.+ */+primitive type Integral : * -> Prop++/**+ * Divide two values, rounding down (toward negative infinity).  *  * For type [n], the arguments are treated as unsigned.- *  * Structured values are divided element-wise.  *  * Division by zero is undefined.  */-primitive (/) : {a} (Arith a) => a -> a -> a+primitive (/) : {a} (Integral a) => a -> a -> a  /**  * Compute the remainder from dividing two values.  *  * For type [n], the arguments are treated as unsigned.- *  * Structured values are combined element-wise.  *  * Remainder of division by zero is undefined.  *  * Satisfies 'x % y == x - (x / y) * y'.  */-primitive (%) : {a} (Arith a) => a -> a -> a+primitive (%) : {a} (Integral a) => a -> a -> a  /**- * Compute the exponentiation of two values.- *  * For type [n], the exponent is treated as unsigned,- *    and the result is reduced modulo 2^^n.- *  * For type Integer, negative powers are undefined.- *  * Structured values are combined element-wise.+ * Converts a value of an integral type to an integer.  */-primitive (^^) : {a} (Arith a) => a -> a -> a+primitive toInteger : {a} (Integral a) => a -> Integer  /**- * Log base two.- *- * For words, computes the ceiling of log, base 2, of a number.- * Over structured values, operates element-wise.+ * Compute the exponentiation of a value in a ring.+ *  * For type [n], the exponent is treated as unsigned.+ *  * It is an error to raise a value to a negative integer exponent.+ *  * Satisfies: 'x ^^ 0 == fromInteger 1'+ *  * Satisfies: 'x ^^ e == x * x ^^ (e-1)' when 'e > 0'.  */-primitive lg2 : {a} (Arith a) => a -> a+primitive (^^) : {a, e} (Ring a, Integral e) => a -> e -> a +/**+ * An infinite sequence counting up from the given starting value.+ * '[x...]' is syntactic sugar for 'infFrom x'.+ */+primitive infFrom : {a} (Integral a) => a -> [inf]a -type Bool = Bit+/**+ * An infinite arithmetic sequence starting with the given two values.+ * '[x,y...]' is syntactic sugar for 'infFromThen x y'.+ */+primitive infFromThen : {a} (Integral a) => a -> a -> [inf]a ++// The Field class -------------------------------------------------+ /**- * The constant True. Corresponds to the bit value 1.+ * Value types that correspond to a field; that is,+ * a ring also posessing multiplicative inverses for+ * non-zero elements.+ *+ * Floating-point values are only approximately a field,+ * but nonetheless inhabit this class.  */-primitive True  : Bit+primitive type Field : * -> Prop  /**- * The constant False. Corresponds to the bit value 0.+ * Reciprocal+ *+ * Compute the multiplicative inverse of an element of a field.+ * The reciprocal of 0 is undefined.  */-primitive False : Bit+primitive recip : {a} (Field a) => a -> a  /**- * Returns the two's complement of its argument.- * Over structured values, operates element-wise.- * The prefix notation '- x' is syntactic sugar- * for 'negate x'.- * Satisfies 'negate a = ~a + 1'.+ * Field division+ *+ * The division operation in a field.+ * Satisfies 'x /. y == x * (recip y)'+ *+ * Field division by 0 is undefined.  */-primitive negate : {a} (Arith a) => a -> a+primitive (/.) : {a} (Field a) => a -> a -> a ++// The Round class -------------------------------------------------++/** Value types that can be rounded to integer values. */+primitive type Round : * -> Prop+ /**- * Bitwise complement. The prefix notation '~ x'- * is syntactic sugar for 'complement x'.+ * Ceiling function.+ *+ * Given 'x', compute the smallest integer 'i'+ * such that 'x <= i'.  */-primitive complement : {a} (Logic a) => a -> a+primitive ceiling : {a} (Round a) => a -> Integer  /**- * Less-than. Only works on comparable arguments.+ * Floor function.  *- * Bitvectors are compared using unsigned arithmetic.+ * Given 'x', compute the largest integer 'i'+ * such that 'i <= x'.  */-primitive (<) : {a} (Cmp a) => a -> a -> Bit+primitive floor : {a} (Round a) => a -> Integer  /**- * Greater-than of two comparable arguments.+ * Truncate the value toward 0.  *- * Bitvectors are compared using unsigned arithmetic.+ * Given 'x' compute the nearest integer between+ * 'x' and 0.  For nonnegative 'x', this is floor,+ * and for negative 'x' this is ceiling.  */-primitive (>) : {a} (Cmp a) => a -> a -> Bit+primitive trunc : {a} (Round a) => a -> Integer  /**- * Less-than or equal of two comparable arguments.+ * Round to the nearest integer, ties away from 0.  *- * Bitvectors are compared using unsigned arithmetic.+ * Ties are broken away from 0.  For nonnegative 'x'+ * this is 'floor (x + 0.5)'.  For negative 'x' this+ * is 'ceiling (x - 0.5)'.  */-primitive (<=) : {a} (Cmp a) => a -> a -> Bit+primitive roundAway : {a} (Round a) => a -> Integer  /**- * Greater-than or equal of two comparable arguments.+ * Round to the nearest integer, ties to even.  *- * Bitvectors are compared using unsigned arithmetic.+ * Ties are broken to the nearest even integer.  */-primitive (>=) : {a} (Cmp a) => a -> a -> Bit+primitive roundToEven : {a} (Round a) => a -> Integer ++// The Eq class ----------------------------------------------------++/** Value types that support equality comparisons. */+primitive type Eq : * -> Prop+ /**  * Compares any two values of the same type for equality.  */-primitive (==) : {a} (Cmp a) => a -> a -> Bit+primitive (==) : {a} (Eq a) => a -> a -> Bit  /**  * Compares any two values of the same type for inequality.  */-primitive (!=) : {a} (Cmp a) => a -> a -> Bit+primitive (!=) : {a} (Eq a) => a -> a -> Bit  /**  * Compare the outputs of two functions for equality.  */-(===) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> (a -> Bit)+(===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit) f === g = \ x -> f x == g x  /**  * Compare the outputs of two functions for inequality.  */-(!==) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> (a -> Bit)+(!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit) f !== g = \x -> f x != g x ++// The Cmp class ---------------------------------------------------++/** Value types that support equality and ordering comparisons. */+primitive type Cmp : * -> Prop+ /**+ * Less-than. Only works on comparable arguments.+ *+ * Bitvectors are compared using unsigned arithmetic.+ */+primitive (<) : {a} (Cmp a) => a -> a -> Bit++/**+ * Greater-than of two comparable arguments.+ *+ * Bitvectors are compared using unsigned arithmetic.+ */+primitive (>) : {a} (Cmp a) => a -> a -> Bit++/**+ * Less-than or equal of two comparable arguments.+ *+ * Bitvectors are compared using unsigned arithmetic.+ */+primitive (<=) : {a} (Cmp a) => a -> a -> Bit++/**+ * Greater-than or equal of two comparable arguments.+ *+ * Bitvectors are compared using unsigned arithmetic.+ */+primitive (>=) : {a} (Cmp a) => a -> a -> Bit++/**  * Returns the smaller of two comparable arguments.  * Bitvectors are compared using unsigned arithmetic.  */@@ -302,7 +513,20 @@ max : {a} (Cmp a) => a -> a -> a max x y = if x > y then x else y +/**+ * Compute the absolute value of a value from an ordered ring.+ * Bitvector values are considered unsigned, so this is+ * the identity function on [n].+ */+abs : {a} (Cmp a, Ring a) => a -> a+abs x = if x < fromInteger 0 then negate x else x ++// The SignedCmp class ----------------------------------------------++/** Value types that support signed comparisons. */+primitive type SignedCmp : * -> Prop+ /**  * 2's complement signed less-than.  */@@ -326,47 +550,18 @@ (>=$) : {a} (SignedCmp a) => a -> a -> Bit x >=$ y = ~(x <$ y) -/**- * 2's complement signed division.  Division rounds toward 0.- */-primitive (/$) : {a} (Arith a) => a -> a -> a -/**- * 2's complement signed remainder.  Division rounds toward 0.- */-primitive (%$) : {a} (Arith a) => a -> a -> a--/**- * Unsigned carry.  Returns true if the unsigned addition of the given- * bitvector arguments would result in an unsigned overflow.- */-primitive carry : {n} (fin n) => [n] -> [n] -> Bit--/**- * Signed carry.  Returns true if the 2's complement signed addition of the- * given bitvector arguments would result in a signed overflow.- */-primitive scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit--/**- * Signed borrow.  Returns true if the 2's complement signed subtraction of the- * given bitvector arguments would result in a signed overflow.- */-sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit-sborrow x y = ( x <$ (x-y) ) ^ y@0+// Bit specific operations ----------------------------------------  /**- * Zero extension of a bitvector.+ * The constant True. Corresponds to the bit value 1.  */-zext : {m, n} (fin m, m >= n) => [n] -> [m]-zext x = zero # x+primitive True  : Bit  /**- * Sign extension of a bitvector.+ * The constant False. Corresponds to the bit value 0.  */-sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]-sext x = newbits # x-  where newbits = if x@0 then ~zero else zero+primitive False : Bit  /**  * Short-cutting boolean conjunction function.@@ -392,76 +587,103 @@ (==>) : Bit -> Bit -> Bit a ==> b = if a then b else True -/**- * Logical 'and' over bits. Extends element-wise over sequences, tuples.- */-primitive (&&) : {a} (Logic a) => a -> a -> a +// Bitvector specific operations ----------------------------------+ /**- * Logical 'or' over bits. Extends element-wise over sequences, tuples.+ * 2's complement signed division.  Division rounds toward 0.+ *  Division by 0 is undefined.+ *+ *  * Satisfies 'x == x %$ y + (x /$ y) * y' for 'y != 0'.  */-primitive (||) : {a} (Logic a) => a -> a -> a+primitive (/$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n]  /**- * Logical 'exclusive or' over bits. Extends element-wise over sequences, tuples.+ * 2's complement signed remainder.  Division rounds toward 0.+ * Division by 0 is undefined.  Satisfies the following for 'y != 0'+ *+ *  * 'x %$ y == x - (x /$ y) * y'.+ *  * 'x >=$ 0 ==> x %$ y >=$ 0'+ *  * 'x <=$ 0 ==> x %$ y <=$ 0'  */-primitive (^) : {a} (Logic a) => a -> a -> a+primitive (%$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n]  /**- * Gives an arbitrary shaped value whose bits are all False.- * ~zero likewise gives an arbitrary shaped value whose bits are all True.+ * Unsigned carry.  Returns true if the unsigned addition of the given+ * bitvector arguments would result in an unsigned overflow.  */-primitive zero : {a} (Zero a) => a+carry : {n} (fin n) => [n] -> [n] -> Bit+carry x y = (x + y) < x  /**- * Converts a bitvector to a non-negative integer in the range 0 to 2^^n-1.+ * Signed carry.  Returns true if the 2's complement signed addition of the+ * given bitvector arguments would result in a signed overflow.  */-primitive toInteger : {bits} (fin bits) => [bits] -> Integer+scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit+scarry x y = (sx == sy) && (sx != sz)+  where+    z  = x + y+    sx = x@0+    sy = y@0+    sz = z@0  /**- * Converts an unbounded integer to another arithmetic type. When converting- * to the bitvector type [n], the value is reduced modulo 2^^n.+ * Signed borrow.  Returns true if the 2's complement signed subtraction of the+ * given bitvector arguments would result in a signed overflow.  */-primitive fromInteger : {a} (Arith a) => Integer -> a+sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit+sborrow x y = ( x <$ (x-y) ) ^ y@0  /**- * Converts an integer modulo n to an unbounded integer in the range 0 to n-1.+ * Zero extension of a bitvector.  */-primitive fromZ : {n} (fin n, n >= 1) => Z n -> Integer+zext : {m, n} (fin m, m >= n) => [n] -> [m]+zext x = zero # x  /**- * Left shift.  The first argument is the sequence to shift, the second is the- * number of positions to shift by.-*/-primitive (<<) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a+ * Sign extension of a bitvector.+ */+sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]+sext x = newbits # x+  where newbits = if x@0 then ~zero else zero  /**- * Right shift.  The first argument is the sequence to shift, the second is the- * number of positions to shift by.+ * 2's complement signed (arithmetic) right shift.  The first argument+ * is the sequence to shift (considered as a signed value),+ * the second argument is the number of positions to shift+ * by (considered as an unsigned value).  */-primitive (>>) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a+primitive (>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]  /**- * Left rotate.  The first argument is the sequence to rotate, the second is the- * number of positions to rotate by.+ * Log base two.+ *+ * For words, computes the ceiling of log, base 2, of a number.+ *  We set 'lg2 0 = 0'  */-primitive (<<<) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a+primitive lg2 : {n} (fin n) => [n] -> [n] ++// Rational specific operations ----------------------------------------------+ /**- * Right rotate.  The first argument is the sequence to rotate, the second is- * the number of positions to rotate by.+ * Compute the ratio of two integers as a rational.+ * Ratio is undefined if the denominator is 0.+ *+ * 'ratio x y = (fromInteger x /. fromInteger y) : Rational'  */-primitive (>>>) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a+primitive ratio : Integer -> Integer -> Rational ++// Zn specific operations ----------------------------------------------------+ /**- * 2's complement signed (arithmetic) right shift.  The first argument- * is the sequence to shift (considered as a signed value),- * the second argument is the number of positions to shift- * by (considered as an unsigned value).+ * Converts an integer modulo n to an unbounded integer in the range 0 to n-1.  */-primitive (>>$) : {n, ix} (fin n, n >= 1, fin ix) => [n] -> [ix] -> [n]+primitive fromZ : {n} (fin n, n >= 1) => Z n -> Integer  +// Sequence operations -------------------------------------------------------  /**  * Concatenates two sequences.  On bitvectors, the most-significant bits@@ -502,17 +724,80 @@  */ primitive transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a + /**+ * Select the first (left-most) 'front' elements of a sequence.+ */+take : {front, back, a} (fin front) => [front + back]a -> [front]a+take (x # _) = x++/**+ * Select all the elements after (to the right of) the 'front' elements of a sequence.+ */+drop : {front, back, a} (fin front) => [front + back]a -> [back]a+drop ((_ : [front] _) # y) = y++/**+ * Drop the first (left-most) element of a sequence.+ */+tail : {n, a} [1 + n]a -> [n]a+tail xs = drop`{1} xs++/**+ * Return the first (left-most) element of a sequence.+ */+head : {n, a} [1 + n]a -> a+head xs = xs @ 0++/**+ * Return the right-most element of a sequence.+ */+last : {n, a} (fin n) => [1 + n]a -> a+last xs = xs ! 0++/**+ * Same as 'split', but with a different type argument order.+ * Take a sequence of elements and break it into 'parts' sequences+ * of 'each' elements.+ */+groupBy : {each, parts, a} (fin each) => [parts * each]a -> [parts][each]a+groupBy = split`{parts=parts}++/**+ * Left shift.  The first argument is the sequence to shift, the second is the+ * number of positions to shift by.+ */+primitive (<<) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a++/**+ * Right shift.  The first argument is the sequence to shift, the second is the+ * number of positions to shift by.+ */+primitive (>>) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a++/**+ * Left rotate.  The first argument is the sequence to rotate, the second is the+ * number of positions to rotate by.+ */+primitive (<<<) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a++/**+ * Right rotate.  The first argument is the sequence to rotate, the second is+ * the number of positions to rotate by.+ */+primitive (>>>) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a++/**  * Index operator.  The first argument is a sequence.  The second argument is  * the zero-based index of the element to select from the sequence.  */-primitive (@) : {n, a, ix} (fin ix) => [n]a -> [ix] -> a+primitive (@) : {n, a, ix} (Integral ix) => [n]a -> ix -> a  /**  * Bulk index operator.  The first argument is a sequence.  The second argument  * is a sequence of the zero-based indices of the elements to select.  */-(@@) : {n, k, ix, a} (fin ix) => [n]a -> [k][ix] -> [k]a+(@@) : {n, k, ix, a} (Integral ix) => [n]a -> [k]ix -> [k]a xs @@ is = [ xs @ i | i <- is ]  /**@@ -520,14 +805,14 @@  * argument is the zero-based index of the element to select, starting from the  * end of the sequence.  */-primitive (!) : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a+primitive (!) : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a  /**  * Bulk reverse index operator.  The first argument is a finite sequence.  The  * second argument is a sequence of the zero-based indices of the elements to  * select, starting from the end of the sequence.  */-(!!) : {n, k, ix, a} (fin n, fin ix) => [n]a -> [k][ix] -> [k]a+(!!) : {n, k, ix, a} (fin n, Integral ix) => [n]a -> [k]ix -> [k]a xs !! is = [ xs ! i | i <- is ]  /**@@ -537,7 +822,7 @@  * The third argument is the new element.  The return value is the  * initial sequence updated so that the indicated index has the given value.  */-primitive update : {n, a, ix} (fin ix) => [n]a -> [ix] -> a -> [n]a+primitive update : {n, a, ix} (Integral ix) => [n]a -> ix -> a -> [n]a  /**  * Update the given sequence with new value at the given index position.@@ -546,7 +831,7 @@  * The third argument is the new element.  The return value is the  * initial sequence updated so that the indicated index has the given value.  */-primitive updateEnd : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a -> [n]a+primitive updateEnd : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a -> [n]a  /**  * Perform a series of updates to a sequence.  The first argument is@@ -555,7 +840,7 @@  * This function applies the 'update' function in sequence with the  * given update pairs.  */-updates : {n, k, ix, a} (fin ix, fin k) => [n]a -> [k][ix] -> [k]a -> [n]a+updates : {n, k, ix, a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a updates xs0 idxs vals = xss!0  where    xss = [ xs0 ] #@@ -572,7 +857,7 @@  * This function applies the 'updateEnd' function in sequence with the  * given update pairs.  */-updatesEnd : {n, k, ix, a} (fin n, fin ix, fin k) => [n]a -> [k][ix] -> [k]a -> [n]a+updatesEnd : {n, k, ix, a} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a updatesEnd xs0 idxs vals = xss!0  where    xss = [ xs0 ] #@@ -583,50 +868,17 @@          ]  /**- * A finite sequence counting up from 'first' to 'last'.- *- * '[a..b]' is syntactic sugar for 'fromTo`{first=a,last=b}'.- */-primitive fromTo : {first, last, a} (fin last, last >= first, Literal last a) =>-                                    [1 + (last - first)]a--/**- * A finite arithmetic sequence starting with 'first' and 'next',- * stopping when the values reach or would skip over 'last'.- *- * '[a,b..c]' is syntactic sugar for 'fromThenTo`{first=a,next=b,last=c}'.- */-primitive fromThenTo : {first, next, last, a, len}-                       ( fin first, fin next, fin last-                       , Literal first a, Literal next a, Literal last a-                       , first != next-                       , lengthFromThenTo first next last == len) => [len]a--/**- * An infinite sequence counting up from the given starting value.- * '[x...]' is syntactic sugar for 'infFrom x'.- */-primitive infFrom : {a} (Arith a) => a -> [inf]a--/**- * An infinite arithmetic sequence starting with the given two values.- * '[x,y...]' is syntactic sugar for 'infFromThen x y'.- */-primitive infFromThen : {a} (Arith a) => a -> a -> [inf]a--/**  * Produce a sequence using a generating function.  * Satisfies 'generate f @ i == f i' for all 'i' between '0' and 'n-1'.  *  * Declarations of the form 'x @ i = e' are syntactic sugar for  * 'x = generate (\i -> e)'.  */-generate : {n, ix, a}-  (fin ix, n >= 1, ix >= width (n - 1)) => ([ix] -> a) -> [n]a+generate : {n, a} (fin n, n >= 1) => (Integer -> a) -> [n]a generate f = [ f i | i <- [0 .. n-1] ] -primitive error : {a, len} (fin len) => [len][8] -> a +// GF_2^n polynomial computations -------------------------------------------  /**  * Performs multiplication of polynomials over GF(2).@@ -670,54 +922,46 @@      zs = [0] # [ z ^ (if xi then tail p else 0) | xi <- reverse x | p <- powers | z <- zs ] -/**- * Generates random values from a seed.  When called with a function, currently- * generates a function that always returns zero.- */-primitive random : {a} [256] -> a -type String n = [n][8]-type Word n = [n]-type Char   = [8]--take : {front, back, a} (fin front) => [front + back]a -> [front]a-take (x # _) = x--drop : {front, back, a} (fin front) => [front + back]a -> [back]a-drop ((_ : [front] _) # y) = y--tail : {n, a} [1 + n]a -> [n]a-tail xs = drop`{1} xs+// Experimental primitives ------------------------------------------------------------  /**- * Return the left-most element of a sequence.+ * Parallel map.  The given function is applied to each element in the+ * given finite seqeuence, and the results are computed in parallel.+ *+ * This function is experimental.  */-head : {n, a} [1 + n]a -> a-head xs = xs @ 0+primitive parmap : {a, b, n} (fin n) => (a -> b) -> [n]a -> [n]b ++// Utility operations -----------------------------------------------------------------+ /**- * Return the right-most element of a sequence.+ * Raise a run-time error with the given message.+ * This function can be called at any type.  */-last : {n, a} (fin n) => [1 + n]a -> a-last xs = xs ! 0+primitive error : {a, n} (fin n) => String n -> a  /**- * Return the length of a sequence.  Note that the result depends only- * on the type of the argument, not its value.+ * Raise a run-time error with a generic message.+ * This function can be called at any type.  */-length : {n, a, b} (fin n, Literal n b) => [n]a -> b-length _ = `n- undefined : {a} a undefined = error "undefined" -groupBy : {each, parts, a} (fin each) => [parts * each]a -> [parts][each]a-groupBy = split`{parts=parts}+/**+ * Assert that the given condition holds, and raise an error+ * with the given message if it does not.  If the condition+ * holds, return the third argument unchanged.+ */+assert : {a, n} (fin n) => Bit -> String n -> a -> a+assert pred msg x = if pred then x else error msg  /**- * Define the base 2 logarithm function in terms of width+ * Generates random values from a seed.  When called with a function, currently+ * generates a function that always returns zero.  */-type lg2 n = width (max n 1 - 1)+primitive random : {a} [256] -> a  /**  * Debugging function for tracing.  The first argument is a string,@@ -730,7 +974,7 @@  * which are unspecified.  Thus, the output produced by this  * operation may be difficult to predict.  */-primitive trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b+primitive trace : {n, a, b} (fin n) => String n -> a -> b -> b  /**  * Debugging function for tracing values.  The first argument is a string,@@ -743,9 +987,10 @@  * which are unspecified.  Thus, the output produced by this  * operation may be difficult to predict.  */-traceVal : {n, a} (fin n) => [n][8] -> a -> a+traceVal : {n, a} (fin n) => String n -> a -> a traceVal msg x = trace msg x x + /* Functions previously in Cryptol::Extras */  /**@@ -799,7 +1044,7 @@ /**  * Compute the sum of the values in the sequence.  */-sum : {n, a} (fin n, Arith a) => [n]a -> a+sum : {n, a} (fin n, Ring a) => [n]a -> a sum xs = foldl (+) (fromInteger 0) xs  /**@@ -825,7 +1070,7 @@ /**  * 'elem x xs' returns true if x is equal to a value in xs.  */-elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit+elem : {n, a} (fin n, Eq a) => a -> [n]a -> Bit elem a xs = any (\x -> x == a) xs  /**@@ -857,4 +1102,5 @@  * list of successive function applications.  */ iterate : {a} (a -> a) -> a -> [inf]a-iterate f x = [x] # [ f v | v <- iterate f x ]+iterate f x = xs+  where xs = [x] # [ f v | v <- xs ]

@@ -0,0 +1,184 @@+module Float where++primitive type ValidFloat : # -> # -> Prop++/** IEEE-754 floating point numbers. */+primitive type { exponent : #, precision : #}+  ValidFloat exponent precision => Float exponent precision : *++/** An abbreviation for common 16-bit floating point numbers. */+type Float16  = Float 5 11++/** An abbreviation for common 32-bit floating point numbers. */+type Float32  = Float 8 24++/** An abbreviation for common 64-bit floating point numbers. */+type Float64  = Float 11 53++/** An abbreviation for common 128-bit floating point numbers. */+type Float128 = Float 15 113++/** An abbreviation for common 256-bit floating point numbers. */+type Float256 = Float 19 237++++/* ----------------------------------------------------------------------+ * Rounding modes (this should be an enumeration type, when we add these)+ *---------------------------------------------------------------------- */++/**+ * A 'RoundingMode' is used to specify the precise behavior of some+ * floating point primitives.+ *+ * There are five valid 'RoundingMode' values:+ *  * roundNearestEven+ *  * roundNearestAway+ *  * roundPositive+ *  * roundNegative+ *  * roundZero+ */+type RoundingMode = [3]++/** Round toward nearest, ties go to even. */+roundNearestEven, rne : RoundingMode+roundNearestEven = 0+rne              = roundNearestEven++/** Round toward nearest, ties away from zero. */+roundNearestAway, rna : RoundingMode+roundNearestAway  = 1+rna               = roundNearestAway++/** Round toward positive infinity. */+roundPositive, rtp : RoundingMode+roundPositive     = 2+rtp               = roundPositive++/** Round toward negative infinity. */+roundNegative, rtn : RoundingMode+roundNegative     = 3+rtn               = roundNegative++/** Round toward zero. */+roundZero, rtz : RoundingMode+roundZero         = 4+rtz               = roundZero++++/* ----------------------------------------------------------------------+ * Constants+ * ---------------------------------------------------------------------- */++/** Not a number. */+primitive+  fpNaN : {e,p} ValidFloat e p => Float e p++/** Positive infinity. */+primitive+  fpPosInf : {e,p} ValidFloat e p => Float e p++fpNegInf : {e,p} ValidFloat e p => Float e p+fpNegInf = - fpPosInf++/** Positive zero. */+fpPosZero : {e,p} ValidFloat e p => Float e p+fpPosZero = zero++/** Negative zero. */+fpNegZero : {e,p} ValidFloat e p => Float e p+fpNegZero = - fpPosZero+++// Binary representations++/** A floating point number using the exact bit pattern,+in IEEE interchange format with layout:++  (sign : [1]) # (biased_exponent : [e]) # (significand : [p-1])+*/+primitive+  fpFromBits : {e,p} ValidFloat e p => [e + p] -> Float e p++/** Export a floating point number in IEEE interchange format with layout:++  (sign : [1]) # (biased_exponent : [e]) # (significand : [p-1])++NaN is represented as:+  * positive:           sign        == 0+  * quiet with no info: significand == 0b1 # 0+*/+primitive+  fpToBits : {e,p} ValidFloat e p => Float e p -> [e + p]++++++/* ----------------------------------------------------------------------+ * Predicates+ * ----------------------------------------------------------------------+ */++// Operations in `Cmp` use IEEE reasoning.++/** Check if two floating point numbers are representationally the same.+In particular, the following hold:+    *    NaN       =.= NaN+    * ~ (pfNegZero =.= fpPosZero)+*/+primitive+  (=.=) : {e,p} ValidFloat e p => Float e p -> Float e p -> Bool++infix 20 =.=+++/* Returns true for numbers that are not an infinity or NaN. */+primitive+  fpIsFinite : {e,p} ValidFloat e p => Float e p -> Bool++++/* ----------------------------------------------------------------------+ * Arithmetic+ * ---------------------------------------------------------------------- */+++/** Add floating point numbers using the given rounding mode. */+primitive+  fpAdd : {e,p} ValidFloat e p =>+    RoundingMode -> Float e p -> Float e p -> Float e p++/** Subtract floating point numbers using the given rounding mode. */+primitive+  fpSub : {e,p} ValidFloat e p =>+    RoundingMode -> Float e p -> Float e p -> Float e p++/** Multiply floating point numbers using the given rounding mode. */+primitive+  fpMul : {e,p} ValidFloat e p =>+    RoundingMode -> Float e p -> Float e p -> Float e p++/** Divide floating point numbers using the given rounding mode. */+primitive+  fpDiv : {e,p} ValidFloat e p =>+    RoundingMode -> Float e p -> Float e p -> Float e p+++/* ------------------------------------------------------------ *+ * Rationals                                                    *+ * ------------------------------------------------------------ */++/** Convert a floating point number to a rational.+It is an error to use this with infinity or NaN **/+primitive+  fpToRational : {e,p} ValidFloat e p =>+    Float e p -> Rational++/** Convert a rational to a floating point number, using the+given rounding mode, if the number cannot be represented exactly. */+primitive+  fpFromRational : {e,p} ValidFloat e p =>+    RoundingMode -> Rational -> Float e p+

@@ -6,13 +6,16 @@ -- Stability   :  provisional -- Portability :  portable +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DoAndIfThenElse #-}+{-# LANGUAGE ImplicitParams #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ParallelListComp #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE Safe #-} {-# LANGUAGE PatternGuards #-}+{-# LANGUAGE ViewPatterns #-}  module Cryptol.Eval (     moduleEnv@@ -28,22 +31,27 @@   , evalSel   , evalSetSel   , EvalError(..)+  , Unsupported(..)   , forceValue   ) where +import Cryptol.Eval.Backend+import Cryptol.Eval.Concrete( Concrete(..) )+import Cryptol.Eval.Generic ( iteValue ) import Cryptol.Eval.Env import Cryptol.Eval.Monad import Cryptol.Eval.Type import Cryptol.Eval.Value-import Cryptol.Parser.Selector(ppSelector) import Cryptol.ModuleSystem.Name+import Cryptol.Parser.Selector(ppSelector) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))+import Cryptol.Utils.Ident import Cryptol.Utils.Panic (panic) import Cryptol.Utils.PP+import Cryptol.Utils.RecordMap  import           Control.Monad-import qualified Data.Sequence as Seq import           Data.List import           Data.Maybe import qualified Data.Map.Strict as Map@@ -52,26 +60,52 @@ import Prelude () import Prelude.Compat -type EvalEnv = GenEvalEnv Bool BV Integer+type EvalEnv = GenEvalEnv Concrete +type EvalPrims sym =+  ( Backend sym, ?evalPrim :: PrimIdent -> Maybe (GenValue sym) )++type ConcPrims =+  ?evalPrim :: PrimIdent -> Maybe (GenValue Concrete)+ -- Expression Evaluation ------------------------------------------------------- +{-# SPECIALIZE moduleEnv ::+  ConcPrims =>+  Concrete ->+  Module ->+  GenEvalEnv Concrete ->+  SEval Concrete (GenEvalEnv Concrete)+  #-}+ -- | Extend the given evaluation environment with all the declarations --   contained in the given module.-moduleEnv :: EvalPrims b w i-          => Module           -- ^ Module containing declarations to evaluate-          -> GenEvalEnv b w i -- ^ Environment to extend-          -> Eval (GenEvalEnv b w i)-moduleEnv m env = evalDecls (mDecls m) =<< evalNewtypes (mNewtypes m) env+moduleEnv ::+  EvalPrims sym =>+  sym ->+  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 +{-# SPECIALIZE evalExpr ::+  ConcPrims =>+  Concrete ->+  GenEvalEnv Concrete ->+  Expr ->+  SEval Concrete (GenValue Concrete)+  #-}+ -- | Evaluate a Cryptol expression to a value.  This evaluator is parameterized --   by the `EvalPrims` class, which defines the behavior of bits and words, in --   addition to providing implementations for all the primitives.-evalExpr :: EvalPrims b w i-         => GenEvalEnv b w i   -- ^ Evaluation environment-         -> Expr               -- ^ Expression to evaluate-         -> Eval (GenValue b w i)-evalExpr env expr = case expr of+evalExpr ::+  EvalPrims sym =>+  sym ->+  GenEvalEnv sym  {- ^ Evaluation environment -} ->+  Expr          {- ^ Expression to evaluate -} ->+  SEval sym (GenValue sym)+evalExpr sym env expr = case expr of    -- Try to detect when the user has directly written a finite sequence of   -- literal bit values and pack these into a word.@@ -80,51 +114,48 @@     -- when the element type is `Bit`.     | isTBit tyv -> {-# SCC "evalExpr->Elist/bit" #-}         return $ VWord len $-          case tryFromBits vs of-            Just w  -> return $ WordVal w-            Nothing -> do xs <- mapM (delay Nothing) vs-                          return $ BitsVal $ Seq.fromList $ map (fromVBit <$>) xs+          case tryFromBits sym vs of+            Just w  -> WordVal <$> w+            Nothing -> do xs <- mapM (sDelay sym Nothing) vs+                          return $ LargeBitsVal len $ finiteSeqMap sym xs     | otherwise -> {-# SCC "evalExpr->EList" #-} do-        xs <- mapM (delay Nothing) vs-        return $ VSeq len $ finiteSeqMap xs+        xs <- mapM (sDelay sym Nothing) vs+        return $ VSeq len $ finiteSeqMap sym xs    where     tyv = evalValType (envTypes env) ty-    vs  = map (evalExpr env) es+    vs  = map eval es     len = genericLength es    ETuple es -> {-# SCC "evalExpr->ETuple" #-} do-     xs <- mapM (delay Nothing . eval) es+     xs <- mapM (sDelay sym Nothing . eval) es      return $ VTuple xs    ERec fields -> {-# SCC "evalExpr->ERec" #-} do-     xs <- sequence [ do thk <- delay Nothing (eval e)-                         return (f, thk)-                    | (f, e) <- fields-                    ]+     xs <- traverse (sDelay sym Nothing . eval) fields      return $ VRecord xs    ESel e sel -> {-# SCC "evalExpr->ESel" #-} do-     x <- eval e-     evalSel x sel+     e' <- eval e+     evalSel sym e' sel    ESet e sel v -> {-# SCC "evalExpr->ESet" #-}-    do x <- eval e-       evalSetSel x sel (eval v)+    do e' <- eval e+       evalSetSel sym e' sel (eval v)    EIf c t f -> {-# SCC "evalExpr->EIf" #-} do      b <- fromVBit <$> eval c-     iteValue b (eval t) (eval f)+     iteValue sym b (eval t) (eval f)    EComp n t h gs -> {-# SCC "evalExpr->EComp" #-} do       let len  = evalNumType (envTypes env) n       let elty = evalValType (envTypes env) t-      evalComp env len elty h gs+      evalComp sym env len elty h gs    EVar n -> {-# SCC "evalExpr->EVar" #-} do     case lookupVar n env of       Just val -> val       Nothing  -> do-        envdoc <- ppEnv defaultPPOpts env+        envdoc <- ppEnv sym defaultPPOpts env         panic "[Eval] evalExpr"                      ["var `" ++ show (pp n) ++ "` is not defined"                      , show envdoc@@ -132,8 +163,8 @@    ETAbs tv b -> {-# SCC "evalExpr->ETAbs" #-}     case tpKind tv of-      KType -> return $ VPoly    $ \ty -> evalExpr (bindType (tpVar tv) (Right ty) env) b-      KNum  -> return $ VNumPoly $ \n  -> evalExpr (bindType (tpVar tv) (Left n) env) b+      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       k     -> panic "[Eval] evalExpr" ["invalid kind on type abstraction", show k]    ETApp e ty -> {-# SCC "evalExpr->ETApp" #-} do@@ -146,87 +177,128 @@                       , show vdoc, show (pp e), show (pp ty)                       ] -  EApp f x -> {-# SCC "evalExpr->EApp" #-} do+  EApp f v -> {-# SCC "evalExpr->EApp" #-} do     eval f >>= \case-      VFun f' -> f' (eval x)+      VFun f' -> 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 n v env-                            evalExpr env' b)+    return $ VFun (\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 -> evalExpr env e-  EProofApp e   -> evalExpr env e+  EProofAbs _ e -> eval e+  EProofApp e   -> eval e    EWhere e ds -> {-# SCC "evalExpr->EWhere" #-} do-     env' <- evalDecls ds env-     evalExpr env' e+     env' <- evalDecls sym ds env+     evalExpr sym env' e    where    {-# INLINE eval #-}-  eval = evalExpr env-  ppV = ppValue defaultPPOpts+  eval = evalExpr sym env+  ppV = ppValue sym defaultPPOpts   -- Newtypes -------------------------------------------------------------------- -evalNewtypes :: EvalPrims b w i-             => Map.Map Name Newtype-             -> GenEvalEnv b w i-             -> Eval (GenEvalEnv b w i)-evalNewtypes nts env = foldM (flip evalNewtype) env $ Map.elems nts+{-# SPECIALIZE evalNewtypes ::+  ConcPrims =>+  Concrete ->+  Map.Map Name Newtype ->+  GenEvalEnv Concrete ->+  SEval Concrete (GenEvalEnv Concrete)+  #-} +evalNewtypes ::+  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+ -- | Introduce the constructor function for a newtype.-evalNewtype :: EvalPrims b w i-            => Newtype-            -> GenEvalEnv b w i-            -> Eval (GenEvalEnv b w i)-evalNewtype nt = bindVar (ntName nt) (return (foldr tabs con (ntParams nt)))+evalNewtype ::+  EvalPrims sym =>+  sym ->+  Newtype ->+  GenEvalEnv sym ->+  SEval sym (GenEvalEnv sym)+evalNewtype sym nt = bindVar sym (ntName nt) (return (foldr tabs con (ntParams nt)))   where   tabs _tp body = tlam (\ _ -> body)   con           = VFun id+{-# INLINE evalNewtype #-}   -- Declarations ---------------------------------------------------------------- +{-# SPECIALIZE evalDecls ::+  ConcPrims =>+  Concrete ->+  [DeclGroup] ->+  GenEvalEnv Concrete ->+  SEval Concrete (GenEvalEnv Concrete)+  #-}+ -- | Extend the given evaluation environment with the result of evaluating the --   given collection of declaration groups.-evalDecls :: EvalPrims b w i-          => [DeclGroup]         -- ^ Declaration groups to evaluate-          -> GenEvalEnv b w i    -- ^ Environment to extend-          -> Eval (GenEvalEnv b w i)-evalDecls dgs env = foldM evalDeclGroup env dgs+evalDecls ::+  EvalPrims sym =>+  sym ->+  [DeclGroup]   {- ^ Declaration groups to evaluate -} ->+  GenEvalEnv sym  {- ^ Environment to extend -} ->+  SEval sym (GenEvalEnv sym)+evalDecls x dgs env = foldM (evalDeclGroup x) env dgs -evalDeclGroup :: EvalPrims b w i-              => GenEvalEnv b w i-              -> DeclGroup-              -> Eval (GenEvalEnv b w i)-evalDeclGroup env dg = do+{-# SPECIALIZE evalDeclGroup ::+  ConcPrims =>+  Concrete ->+  GenEvalEnv Concrete ->+  DeclGroup ->+  SEval Concrete (GenEvalEnv Concrete)+  #-}++evalDeclGroup ::+  EvalPrims sym =>+  sym ->+  GenEvalEnv sym ->+  DeclGroup ->+  SEval sym (GenEvalEnv sym)+evalDeclGroup sym env dg = do   case dg of     Recursive ds -> do       -- declare a "hole" for each declaration       -- and extend the evaluation environment-      holes <- mapM declHole ds+      holes <- mapM (declHole sym) ds       let holeEnv = Map.fromList $ [ (nm,h) | (nm,_,h,_) <- holes ]       let env' = env `mappend` emptyEnv{ envVars = holeEnv }        -- evaluate the declaration bodies, building a new evaluation environment-      env'' <- foldM (evalDecl env') env ds+      env'' <- foldM (evalDecl sym env') env ds        -- now backfill the holes we declared earlier using the definitions       -- calculated in the previous step-      mapM_ (fillHole env'') holes+      mapM_ (fillHole sym env'') holes        -- return the map containing the holes       return env'      NonRecursive d -> do-      evalDecl env env d+      evalDecl sym env env d  ++{-# SPECIALIZE fillHole ::+  Concrete ->+  GenEvalEnv Concrete ->+  (Name, Schema, SEval Concrete (GenValue Concrete), SEval Concrete (GenValue Concrete) -> SEval Concrete ()) ->+  SEval Concrete ()+  #-}+ -- | This operation is used to complete the process of setting up recursive declaration --   groups.  It 'backfills' previously-allocated thunk values with the actual evaluation --   procedure for the body of recursive definitions.@@ -237,16 +309,19 @@ --   to this is to force an eta-expansion procedure on all recursive definitions. --   However, for the so-called 'Value' types we can instead optimistically use the 'delayFill' --   operation and only fall back on full eta expansion if the thunk is double-forced.-fillHole :: BitWord b w i-         => GenEvalEnv b w i-         -> (Name, Schema, Eval (GenValue b w i), Eval (GenValue b w i) -> Eval ())-         -> Eval ()-fillHole env (nm, sch, _, fill) = do++fillHole ::+  Backend sym =>+  sym ->+  GenEvalEnv sym ->+  (Name, Schema, SEval sym (GenValue sym), SEval sym (GenValue sym) -> SEval sym ()) ->+  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 x-     | isValueType env sch -> fill =<< delayFill x (etaDelay (show (ppLocName nm)) env sch x)-     | otherwise           -> fill (etaDelay (show (ppLocName nm)) env sch x)+    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)   -- | 'Value' types are non-polymorphic types recursive constructed from@@ -254,29 +329,47 @@ --   be implemented rather more efficently than general types because we can --   rely on the 'delayFill' operation to build a thunk that falls back on performing --   eta-expansion rather than doing it eagerly.-isValueType :: GenEvalEnv b w i -> Schema -> Bool+isValueType :: GenEvalEnv sym -> Schema -> Bool isValueType env Forall{ sVars = [], sProps = [], sType = t0 }    = go (evalValType (envTypes env) t0)  where   go TVBit = True   go (TVSeq _ x)  = go x   go (TVTuple xs) = and (map go xs)-  go (TVRec xs)   = and (map (go . snd) xs)+  go (TVRec xs)   = and (fmap go xs)   go _            = False  isValueType _ _ = False  +{-# SPECIALIZE etaWord  ::+  Concrete ->+  Integer ->+  SEval Concrete (GenValue Concrete) ->+  SEval Concrete (WordValue Concrete)+  #-}+ -- | Eta-expand a word value.  This forces an unpacked word representation.-etaWord  :: BitWord b w i-         => Integer-         -> Eval (GenValue b w i)-         -> Eval (WordValue b w i)-etaWord n x = do-  w <- delay Nothing (fromWordVal "during eta-expansion" =<< x)-  return $ BitsVal $ Seq.fromFunction (fromInteger n) $ \i ->-    do w' <- w; indexWordValue w' (toInteger i)+etaWord  ::+  Backend sym =>+  sym ->+  Integer ->+  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 ->+          do w' <- w; VBit <$> indexWordValue sym w' i+  pure $ LargeBitsVal n xs +{-# SPECIALIZE etaDelay ::+  Concrete ->+  String ->+  GenEvalEnv Concrete ->+  Schema ->+  SEval Concrete (GenValue Concrete) ->+  SEval Concrete (GenValue Concrete)+  #-}  -- | Given a simulator value and its type, fully eta-expand the value.  This --   is a type-directed pass that always produces a canonical value of the@@ -284,28 +377,29 @@ --   the correct evaluation semantics of recursive definitions.  Otherwise, --   expressions that should be expected to produce well-defined values in the --   denotational semantics will fail to terminate instead.-etaDelay :: BitWord b w i-         => String-         -> GenEvalEnv b w i-         -> Schema-         -> Eval (GenValue b w i)-         -> Eval (GenValue b w i)-etaDelay msg env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0+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   where-  goTpVars env []     x = go (evalValType (envTypes env) tp0) x-  goTpVars env (v:vs) x =+  goTpVars env []     val = go (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 =<< x )+                  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 =<< x )+                  goTpVars (bindType (tpVar v) (Left n) env) vs ( ($n) . fromVNumPoly =<< val )       k     -> panic "[Eval] etaDelay" ["invalid kind on type abstraction", show k] -  go tp (Ready x) =-    case x of-      VBit _     -> return x-      VInteger _ -> return x-      VWord _ _  -> return x+  go tp x | isReady sym x = x >>= \case+      VBit _     -> x+      VInteger _ -> x+      VWord _ _  -> x       VSeq n xs         | TVSeq _nt el <- tp         -> return $ VSeq n $ IndexSeqMap $ \i -> go el (lookupSeqMap xs i)@@ -320,11 +414,11 @@        VRecord fs         | TVRec fts <- tp-        -> return $ VRecord $-             let err f = evalPanic "expected record value with field" [show f] in-             [ (f, go (fromMaybe (err f) (lookup f fts)) y)-             | (f, y) <- fs-             ]+        -> do let res = zipRecords (\_ v t -> go 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')        VFun f         | TVFun _t1 t2 <- tp@@ -332,58 +426,67 @@        _ -> evalPanic "type mismatch during eta-expansion" [] -  go tp x =+  go tp v =     case tp of-      TVBit -> x-      TVInteger -> x-      TVIntMod _ -> x+      TVBit -> v+      TVInteger -> v+      TVFloat {} -> v+      TVIntMod _ -> v+      TVRational -> v+      TVArray{} -> v        TVSeq n TVBit ->-          do w <- delayFill (fromWordVal "during eta-expansion" =<< x) (etaWord n x)+          do w <- sDelayFill sym (fromWordVal "during eta-expansion" =<< v) (etaWord sym n v)              return $ VWord n w        TVSeq n el ->-          do x' <- delay (Just msg) (fromSeq "during eta-expansion" =<< x)+          do x' <- sDelay sym (Just msg) (fromSeq "during eta-expansion" =<< v)              return $ VSeq n $ IndexSeqMap $ \i -> do                go el (flip lookupSeqMap i =<< x')        TVStream el ->-          do x' <- delay (Just msg) (fromSeq "during eta-expansion" =<< x)+          do x' <- sDelay sym (Just msg) (fromSeq "during eta-expansion" =<< v)              return $ VStream $ IndexSeqMap $ \i ->                go el (flip lookupSeqMap i =<< x')        TVFun _t1 t2 ->-          do x' <- delay (Just msg) (fromVFun <$> x)-             return $ VFun $ \a -> go t2 ( ($a) =<< x' )+          do v' <- sDelay sym (Just msg) (fromVFun <$> v)+             return $ VFun $ \a -> go t2 ( ($a) =<< v' )        TVTuple ts ->           do let n = length ts-             x' <- delay (Just msg) (fromVTuple <$> x)+             v' <- sDelay sym (Just msg) (fromVTuple <$> v)              return $ VTuple $-                [ go t =<< (flip genericIndex i <$> x')+                [ go t =<< (flip genericIndex i <$> v')                 | i <- [0..(n-1)]                 | t <- ts                 ]        TVRec fs ->-          do x' <- delay (Just msg) (fromVRecord <$> x)+          do v' <- sDelay sym (Just msg) (fromVRecord <$> v)              let err f = evalPanic "expected record value with field" [show f]-             return $ VRecord $-                [ (f, go t =<< (fromMaybe (err f) . lookup f <$> x'))-                | (f,t) <- fs-                ]+             let eta f t = go t =<< (fromMaybe (err f) . lookupField f <$> v')+             return $ VRecord (mapWithFieldName eta fs) -      TVAbstract {} -> x+      TVAbstract {} -> v  -declHole :: Decl-         -> Eval (Name, Schema, Eval (GenValue b w i), Eval (GenValue b w i) -> Eval ())-declHole d =+{-# SPECIALIZE declHole ::+  Concrete ->+  Decl ->+  SEval Concrete+    (Name, Schema, SEval Concrete (GenValue Concrete), SEval Concrete (GenValue Concrete) -> SEval Concrete ())+  #-}++declHole ::+  Backend sym =>+  sym -> Decl -> SEval sym (Name, Schema, SEval sym (GenValue sym), SEval sym (GenValue sym) -> SEval sym ())+declHole sym d =   case dDefinition d of     DPrim   -> evalPanic "Unexpected primitive declaration in recursive group"                          [show (ppLocName nm)]     DExpr _ -> do-      (hole, fill) <- blackhole msg+      (hole, fill) <- sDeclareHole sym msg       return (nm, sch, hole, fill)   where   nm = dName d@@ -398,31 +501,43 @@ --   handle the subtle name-binding issues that arise from recursive --   definitions.  The 'read only' environment is used to bring recursive --   names into scope while we are still defining them.-evalDecl :: EvalPrims b w i-         => GenEvalEnv b w i  -- ^ A 'read only' environment for use in declaration bodies-         -> GenEvalEnv b w i  -- ^ An evaluation environment to extend with the given declaration-         -> Decl              -- ^ The declaration to evaluate-         -> Eval (GenEvalEnv b w i)-evalDecl renv env d =+evalDecl ::+  EvalPrims sym =>+  sym ->+  GenEvalEnv sym  {- ^ A 'read only' environment for use in declaration bodies -} ->+  GenEvalEnv sym  {- ^ An evaluation environment to extend with the given declaration -} ->+  Decl            {- ^ The declaration to evaluate -} ->+  SEval sym (GenEvalEnv sym)+evalDecl sym renv env d =   case dDefinition d of-    DPrim   -> case evalPrim d of-                 Just v  -> pure (bindVarDirect (dName d) v env)-                 Nothing -> bindVar (dName d) (cryNoPrimError (dName d)) env+    DPrim ->+      case ?evalPrim =<< asPrim (dName d) of+        Just v  -> pure (bindVarDirect (dName d) v env)+        Nothing -> bindVar sym (dName d) (cryNoPrimError sym (dName d)) env -    DExpr e -> bindVar (dName d) (evalExpr renv e) env+    DExpr e -> bindVar sym (dName d) (evalExpr sym renv e) env   -- Selectors ------------------------------------------------------------------- +{-# SPECIALIZE evalSel ::+  ConcPrims =>+  Concrete ->+  GenValue Concrete ->+  Selector ->+  SEval Concrete (GenValue Concrete)+  #-}+ -- | Apply the the given "selector" form to the given value.  This function pushes --   tuple and record selections pointwise down into other value constructs --   (e.g., streams and functions).-evalSel :: forall b w i-         . EvalPrims b w i-        => GenValue b w i-        -> Selector-        -> Eval (GenValue b w i)-evalSel val sel = case sel of+evalSel ::+  EvalPrims sym =>+  sym ->+  GenValue sym ->+  Selector ->+  SEval sym (GenValue sym)+evalSel sym val sel = case sel of    TupleSel n _  -> tupleSel n val   RecordSel n _ -> recordSel n val@@ -432,7 +547,7 @@   tupleSel n v =     case v of       VTuple vs       -> vs !! n-      _               -> do vdoc <- ppValue defaultPPOpts v+      _               -> do vdoc <- ppValue sym defaultPPOpts v                             evalPanic "Cryptol.Eval.evalSel"                               [ "Unexpected value in tuple selection"                               , show vdoc ]@@ -440,7 +555,7 @@   recordSel n v =     case v of       VRecord {}      -> lookupRecord n v-      _               -> do vdoc <- ppValue defaultPPOpts v+      _               -> do vdoc <- ppValue sym defaultPPOpts v                             evalPanic "Cryptol.Eval.evalSel"                               [ "Unexpected value in record selection"                               , show vdoc ]@@ -449,26 +564,32 @@     case v of       VSeq _ vs       -> lookupSeqMap vs (toInteger n)       VStream vs      -> lookupSeqMap vs (toInteger n)-      VWord _ wv      -> VBit <$> (flip indexWordValue (toInteger n) =<< wv)-      _               -> do vdoc <- ppValue defaultPPOpts val+      VWord _ wv      -> VBit <$> (flip (indexWordValue sym) (toInteger n) =<< wv)+      _               -> do vdoc <- ppValue sym defaultPPOpts val                             evalPanic "Cryptol.Eval.evalSel"                               [ "Unexpected value in list selection"                               , show vdoc ]--evalSetSel :: forall b w i. EvalPrims b w i =>-  GenValue b w i -> Selector -> Eval (GenValue b w i) -> Eval (GenValue b w i)-evalSetSel e x v =-  case x of+{-# SPECIALIZE evalSetSel ::+  ConcPrims =>+  Concrete ->+  GenValue Concrete -> Selector -> SEval Concrete (GenValue Concrete) -> SEval Concrete (GenValue Concrete)+  #-}+evalSetSel :: forall sym.+  EvalPrims sym =>+  sym ->+  GenValue sym -> Selector -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)+evalSetSel sym e sel v =+  case sel of     TupleSel n _  -> setTuple n     RecordSel n _ -> setRecord n     ListSel ix _  -> setList (toInteger ix)    where   bad msg =-    do ed <- ppValue defaultPPOpts e+    do ed <- ppValue sym defaultPPOpts e        evalPanic "Cryptol.Eval.evalSetSel"           [ msg-          , "Selector: " ++ show (ppSelector x)+          , "Selector: " ++ show (ppSelector sel)           , "Value: " ++ show ed           ] @@ -483,9 +604,9 @@   setRecord n =     case e of       VRecord xs ->-        case break ((n ==) . fst) xs of-          (as, (i,_) : bs) -> pure (VRecord (as ++ (i,v) : bs))-          _ -> bad "Missing field in record update."+        case adjustField n (\_ -> v) xs of+          Just xs' -> pure (VRecord xs')+          Nothing -> bad "Missing field in record update."       _ -> bad "Record update on a non-record."    setList n =@@ -493,7 +614,7 @@       VSeq i mp  -> pure $ VSeq i  $ updateSeqMap mp n v       VStream mp -> pure $ VStream $ updateSeqMap mp n v       VWord i m  -> pure $ VWord i $ do m1 <- m-                                        updateWordValue m1 n asBit+                                        updateWordValue sym m1 n asBit       _ -> bad "Sequence update on a non-sequence."    asBit = do res <- v@@ -506,22 +627,22 @@ -- | Evaluation environments for list comprehensions: Each variable -- name is bound to a list of values, one for each element in the list -- comprehension.-data ListEnv b w i = ListEnv-  { leVars   :: !(Map.Map Name (Integer -> Eval (GenValue b w i)))+data ListEnv sym = ListEnv+  { leVars   :: !(Map.Map Name (Integer -> SEval sym (GenValue sym)))       -- ^ Bindings whose values vary by position-  , leStatic :: !(Map.Map Name (Eval (GenValue b w i)))+  , leStatic :: !(Map.Map Name (SEval sym (GenValue sym)))       -- ^ Bindings whose values are constant   , leTypes  :: !TypeEnv   } -instance Semigroup (ListEnv b w i) where+instance Semigroup (ListEnv sym) where   l <> r = ListEnv     { leVars   = Map.union (leVars  l)  (leVars  r)     , leStatic = Map.union (leStatic l) (leStatic r)     , leTypes  = Map.union (leTypes l)  (leTypes r)     } -instance Monoid (ListEnv b w i) where+instance Monoid (ListEnv sym) where   mempty = ListEnv     { leVars   = Map.empty     , leStatic = Map.empty@@ -530,59 +651,95 @@    mappend l r = l <> r -toListEnv :: GenEvalEnv b w i -> ListEnv b w i+toListEnv :: GenEvalEnv sym -> ListEnv sym toListEnv e =   ListEnv   { leVars   = mempty   , leStatic = envVars e   , leTypes  = envTypes e   }+{-# INLINE toListEnv #-}  -- | Evaluate a list environment at a position. --   This choses a particular value for the varying --   locations.-evalListEnv :: ListEnv b w i -> Integer -> GenEvalEnv b w i+evalListEnv :: ListEnv sym -> Integer -> GenEvalEnv sym evalListEnv (ListEnv vm st tm) i =     let v = fmap ($i) vm      in EvalEnv{ envVars = Map.union v st                , envTypes = tm                }+{-# INLINE evalListEnv #-} -bindVarList :: Name-            -> (Integer -> Eval (GenValue b w i))-            -> ListEnv b w i-            -> ListEnv b w i++bindVarList ::+  Name ->+  (Integer -> SEval sym (GenValue sym)) ->+  ListEnv sym ->+  ListEnv sym bindVarList n vs lenv = lenv { leVars = Map.insert n vs (leVars lenv) }+{-# INLINE bindVarList #-}  -- List Comprehensions --------------------------------------------------------- +{-# SPECIALIZE evalComp ::+  ConcPrims =>+  Concrete ->+  GenEvalEnv Concrete ->+  Nat'           ->+  TValue         ->+  Expr           ->+  [[Match]]      ->+  SEval Concrete (GenValue Concrete)+  #-} -- | Evaluate a comprehension.-evalComp :: EvalPrims b w i-         => GenEvalEnv b w i -- ^ Starting evaluation environment-         -> Nat'             -- ^ Length of the comprehension-         -> TValue           -- ^ Type of the comprehension elements-         -> Expr             -- ^ Head expression of the comprehension-         -> [[Match]]        -- ^ List of parallel comprehension branches-         -> Eval (GenValue b w i)-evalComp env len elty body ms =-       do lenv <- mconcat <$> mapM (branchEnvs (toListEnv env)) ms+evalComp ::+  EvalPrims sym =>+  sym ->+  GenEvalEnv sym {- ^ Starting evaluation environment -} ->+  Nat'           {- ^ Length of the comprehension -} ->+  TValue         {- ^ Type of the comprehension elements -} ->+  Expr           {- ^ Head expression of the comprehension -} ->+  [[Match]]      {- ^ List of parallel comprehension branches -} ->+  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-              evalExpr (evalListEnv lenv i) body)+              evalExpr sym (evalListEnv lenv i) body) +{-# SPECIALIZE branchEnvs ::+  ConcPrims =>+  Concrete ->+  ListEnv Concrete ->+  [Match] ->+  SEval Concrete (ListEnv Concrete)+  #-} -- | Turn a list of matches into the final environments for each iteration of -- the branch.-branchEnvs :: EvalPrims b w i-           => ListEnv b w i-           -> [Match]-           -> Eval (ListEnv b w i)-branchEnvs env matches = foldM evalMatch env matches+branchEnvs ::+  EvalPrims sym =>+  sym ->+  ListEnv sym ->+  [Match] ->+  SEval sym (ListEnv sym)+branchEnvs sym env matches = foldM (evalMatch sym) env matches +{-# SPECIALIZE evalMatch ::+  ConcPrims =>+  Concrete ->+  ListEnv Concrete ->+  Match ->+  SEval Concrete (ListEnv Concrete)+  #-}+ -- | Turn a match into the list of environments it represents.-evalMatch :: EvalPrims b w i-          => ListEnv b w i-          -> Match-          -> Eval (ListEnv b w i)-evalMatch lenv m = case m of+evalMatch ::+  EvalPrims sym =>+  sym ->+  ListEnv sym ->+  Match ->+  SEval sym (ListEnv sym)+evalMatch sym lenv m = case m of    -- many envs   From n l _ty expr ->@@ -590,12 +747,12 @@       -- 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 (evalListEnv lenv i) expr+        vss <- memoMap $ 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                       lookupSeqMap vss q >>= \case-                        VWord _ w   -> VBit <$> (flip indexWordValue r =<< w)+                        VWord _ w   -> VBit <$> (flip (indexWordValue sym) r =<< w)                         VSeq _ xs'  -> lookupSeqMap xs' r                         VStream xs' -> lookupSeqMap xs' r                         _           -> evalPanic "evalMatch" ["Not a list value"]@@ -611,9 +768,9 @@                          , leStatic = allvars                          }         let env   = EvalEnv allvars (leTypes lenv)-        xs <- evalExpr env expr+        xs <- evalExpr sym env expr         let vs i = case xs of-                     VWord _ w   -> VBit <$> (flip indexWordValue i =<< w)+                     VWord _ w   -> VBit <$> (flip (indexWordValue sym) i =<< w)                      VSeq _ xs'  -> lookupSeqMap xs' i                      VStream xs' -> lookupSeqMap xs' i                      _           -> evalPanic "evalMatch" ["Not a list value"]@@ -630,4 +787,4 @@       f env =           case dDefinition d of             DPrim   -> evalPanic "evalMatch" ["Unexpected local primitive"]-            DExpr e -> evalExpr env e+            DExpr e -> evalExpr sym env e

@@ -0,0 +1,705 @@+{-# Language FlexibleContexts #-}+{-# Language TypeFamilies #-}+module Cryptol.Eval.Backend+  ( Backend(..)+  , sDelay+  , invalidIndex+  , cryUserError+  , cryNoPrimError+  , FPArith2++    -- * Rationals+  , SRational(..)+  , intToRational+  , ratio+  , rationalAdd+  , rationalSub+  , rationalNegate+  , rationalMul+  , rationalRecip+  , rationalDivide+  , rationalFloor+  , rationalCeiling+  , rationalTrunc+  , rationalRoundAway+  , rationalRoundToEven+  , rationalEq+  , rationalLessThan+  , rationalGreaterThan+  , iteRational+  , ppRational+  ) where++import Control.Monad.IO.Class+import Data.Kind (Type)+import Data.Ratio ( (%), numerator, denominator )++import Cryptol.Eval.Monad+import Cryptol.TypeCheck.AST(Name)+import Cryptol.Utils.PP+++invalidIndex :: Backend sym => sym -> Integer -> SEval sym a+invalidIndex sym = raiseError sym . InvalidIndex . Just++cryUserError :: Backend sym => sym -> String -> SEval sym a+cryUserError sym = raiseError sym . UserError++cryNoPrimError :: Backend sym => sym -> Name -> SEval sym a+cryNoPrimError sym = raiseError sym . NoPrim+++{-# 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+++-- | Representation of rational numbers.+--     Invariant: denominator is not 0+data SRational sym =+  SRational+  { sNum :: SInteger sym+  , sDenom :: SInteger sym+  }++intToRational :: Backend sym => sym -> SInteger sym -> SEval sym (SRational sym)+intToRational sym x = SRational x <$> (integerLit sym 1)++ratio :: Backend sym => sym -> SInteger sym -> SInteger sym -> SEval sym (SRational sym)+ratio sym n d =+  do pz  <- bitComplement sym =<< intEq sym d =<< integerLit sym 0+     assertSideCondition sym pz DivideByZero+     pure (SRational n d)++rationalRecip :: Backend sym => sym -> SRational sym -> SEval sym (SRational sym)+rationalRecip sym (SRational a b) = ratio sym b a++rationalDivide :: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)+rationalDivide sym x y = rationalMul sym x =<< rationalRecip sym y++rationalFloor :: Backend sym => sym -> SRational sym -> SEval sym (SInteger sym)+ -- NB, relies on integer division being round-to-negative-inf division+rationalFloor sym (SRational n d) = intDiv sym n d++rationalCeiling :: Backend sym => sym -> SRational sym -> SEval sym (SInteger sym)+rationalCeiling sym r = intNegate sym =<< rationalFloor sym =<< rationalNegate sym r++rationalTrunc :: Backend sym => sym -> SRational sym -> SEval sym (SInteger sym)+rationalTrunc sym r =+  do p <- rationalLessThan sym r =<< intToRational sym =<< integerLit sym 0+     cr <- rationalCeiling sym r+     fr <- rationalFloor sym r+     iteInteger sym p cr fr++rationalRoundAway :: Backend sym => sym -> SRational sym -> SEval sym (SInteger sym)+rationalRoundAway sym r =+  do p <- rationalLessThan sym r =<< intToRational sym =<< integerLit sym 0+     half <- SRational <$> integerLit sym 1 <*> integerLit sym 2+     cr <- rationalCeiling sym =<< rationalSub sym r half+     fr <- rationalFloor sym =<< rationalAdd sym r half+     iteInteger sym p cr fr++rationalRoundToEven :: Backend sym => sym -> SRational sym -> SEval sym (SInteger sym)+rationalRoundToEven sym r =+  do lo <- rationalFloor sym r+     hi <- intPlus sym lo =<< integerLit sym 1+     -- NB: `diff` will be nonnegative because `lo <= r`+     diff <- rationalSub sym r =<< intToRational sym lo+     half <- SRational <$> integerLit sym 1 <*> integerLit sym 2++     ite (rationalLessThan sym diff half) (pure lo) $+       ite (rationalGreaterThan sym diff half) (pure hi) $+         ite (isEven lo) (pure lo) (pure hi)++ where+ isEven x =+   do parity <- intMod sym x =<< integerLit sym 2+      intEq sym parity =<< integerLit sym 0++ ite x t e =+   do x' <- x+      case bitAsLit sym x' of+        Just True -> t+        Just False -> e+        Nothing ->+          do t' <- t+             e' <- e+             iteInteger sym x' t' e'+++rationalAdd :: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)+rationalAdd sym (SRational a b) (SRational c d) =+  do ad <- intMult sym a d+     bc <- intMult sym b c+     bd <- intMult sym b d+     ad_bc <- intPlus sym ad bc+     pure (SRational ad_bc bd)++rationalSub :: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)+rationalSub sym (SRational a b) (SRational c d) =+  do ad <- intMult sym a d+     bc <- intMult sym b c+     bd <- intMult sym b d+     ad_bc <- intMinus sym ad bc+     pure (SRational ad_bc bd)++rationalNegate :: Backend sym => sym -> SRational sym -> SEval sym (SRational sym)+rationalNegate sym (SRational a b) =+  do aneg <- intNegate sym a+     pure (SRational aneg b)++rationalMul :: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)+rationalMul sym (SRational a b) (SRational c d) =+  do ac <- intMult sym a c+     bd <- intMult sym b d+     pure (SRational ac bd)++rationalEq :: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)+rationalEq sym (SRational a b) (SRational c d) =+  do ad <- intMult sym a d+     bc <- intMult sym b c+     intEq sym ad bc++normalizeSign :: Backend sym => sym -> SRational sym -> SEval sym (SRational sym)+normalizeSign sym (SRational a b) =+  do p <- intLessThan sym b =<< integerLit sym 0+     case bitAsLit sym p of+       Just False -> pure (SRational a b)+       Just True  ->+         do aneg <- intNegate sym a+            bneg <- intNegate sym b+            pure (SRational aneg bneg)+       Nothing ->+         do aneg <- intNegate sym a+            bneg <- intNegate sym b+            a' <- iteInteger sym p aneg a+            b' <- iteInteger sym p bneg b+            pure (SRational a' b')++rationalLessThan:: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)+rationalLessThan sym x y =+  do SRational a b <- normalizeSign sym x+     SRational c d <- normalizeSign sym y+     ad <- intMult sym a d+     bc <- intMult sym b c+     intLessThan sym ad bc++rationalGreaterThan:: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)+rationalGreaterThan sym = flip (rationalLessThan sym)++iteRational :: Backend sym => sym -> SBit sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)+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.+class MonadIO (SEval sym) => Backend sym where+  type SBit sym :: Type+  type SWord sym :: Type+  type SInteger sym :: Type+  type SFloat sym :: Type+  type SEval sym :: Type -> Type++  -- ==== Evaluation monad operations ====++  -- | Check if an operation is "ready", which means its+  --   evaluation will be trivial.+  isReady :: sym -> SEval sym a -> Bool++  -- | Produce a thunk value which can be filled with its associated computation+  --   after the fact.  A preallocated thunk is returned, along with an operation to+  --   fill the thunk with the associated computation.+  --   This is used to implement recursive declaration groups.+  sDeclareHole :: sym -> String -> SEval sym (SEval sym a, SEval sym a -> SEval sym ())++  -- | Delay the given evaluation computation, returning a thunk+  --   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)++  -- | 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)++  -- | Merge the two given computations according to the predicate.+  mergeEval ::+     sym ->+     (SBit sym -> a -> a -> SEval sym a) {- ^ A merge operation on values -} ->+     SBit sym {- ^ The condition -} ->+     SEval sym a {- ^ The "then" computation -} ->+     SEval sym a {- ^ The "else" computation -} ->+     SEval sym a++  -- | Assert that a condition must hold, and indicate what sort of+  --   error is indicated if the condition fails.+  assertSideCondition :: sym -> SBit sym -> EvalError -> SEval sym ()++  -- | 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+  bitAsLit :: sym -> SBit sym -> Maybe Bool++  -- | The number of bits in a word value.+  wordLen :: sym -> SWord sym -> Integer++  -- | Determine if this symbolic word is a literal.+  --   If so, return the bit width and value.+  wordAsLit :: sym -> SWord sym -> Maybe (Integer, Integer)++  -- | Attempt to render a word value as an ASCII character.  Return 'Nothing'+  --   if the character value is unknown (e.g., for symbolic values).+  wordAsChar :: sym -> SWord sym -> Maybe Char++  -- | Determine if this symbolic integer is a literal+  integerAsLit :: sym -> SInteger sym -> Maybe Integer++  -- ==== Creating literal values ====++  -- | Construct a literal bit value from a boolean.+  bitLit :: sym -> Bool -> SBit sym++  -- | Construct a literal word value given a bit width and a value.+  wordLit ::+    sym ->+    Integer {- ^ Width -} ->+    Integer {- ^ Value -} ->+    SEval sym (SWord sym)++  -- | Construct a literal integer value from the given integer.+  integerLit ::+    sym ->+    Integer {- ^ Value -} ->+    SEval sym (SInteger sym)++  -- | Construct a floating point value from the given rational.+  fpLit ::+    sym ->+    Integer  {- ^ exponent bits -} ->+    Integer  {- ^ precision bits -} ->+    Rational {- ^ The rational -} ->+    SEval sym (SFloat sym)++  -- ==== If/then/else operations ====+  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)+++  -- ==== Bit operations ====+  bitEq  :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)+  bitOr  :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)+  bitAnd :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)+  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.+  --+  --   NOTE: this assumes that the sequence of bits is big-endian and finite, so the+  --   bit numbered 0 is the most significant bit.+  wordBit ::+    sym ->+    SWord sym ->+    Integer {- ^ Bit position to extract -} ->+    SEval sym (SBit sym)++  -- | Update the numbered bit in the word.+  --+  --   NOTE: this assumes that the sequence of bits is big-endian and finite, so the+  --   bit numbered 0 is the most significant bit.+  wordUpdate ::+    sym ->+    SWord sym ->+    Integer {- ^ Bit position to update -} ->+    SBit sym ->+    SEval sym (SWord sym)++  -- | Construct a word value from a finite sequence of bits.+  --   NOTE: this assumes that the sequence of bits is big-endian and finite, so the+  --   first element of the list will be the most significant bit.+  packWord ::+    sym ->+    [SBit sym] ->+    SEval sym (SWord sym)++  -- | Deconstruct a packed word value in to a finite sequence of bits.+  --   NOTE: this produces a list of bits that represent a big-endian word, so+  --   the most significant bit is the first element of the list.+  unpackWord ::+    sym ->+    SWord sym ->+    SEval sym [SBit sym]++  -- | Construct a packed word of the specified width from an integer value.+  wordFromInt ::+    sym ->+    Integer {- ^ bit-width -} ->+    SInteger sym ->+    SEval sym (SWord sym)++  -- | Concatenate the two given word values.+  --   NOTE: the first argument represents the more-significant bits+  joinWord ::+    sym ->+    SWord sym ->+    SWord sym ->+    SEval sym (SWord sym)++  -- | Take the most-significant bits, and return+  --   those bits and the remainder.  The first element+  --   of the pair is the most significant bits.+  --   The two integer sizes must sum to the length of the given word value.+  splitWord ::+    sym ->+    Integer {- ^ left width -} ->+    Integer {- ^ right width -} ->+    SWord sym ->+    SEval sym (SWord sym, SWord sym)++  -- | Extract a subsequence of bits from a packed word value.+  --   The first integer argument is the number of bits in the+  --   resulting word.  The second integer argument is the+  --   number of less-significant digits to discard.  Stated another+  --   way, the operation @extractWord n i w@ is equivalent to+  --   first shifting @w@ right by @i@ bits, and then truncating to+  --   @n@ bits.+  extractWord ::+    sym ->+    Integer {- ^ Number of bits to take -} ->+    Integer {- ^ starting bit -} ->+    SWord sym ->+    SEval sym (SWord sym)++  -- | Bitwise OR+  wordOr ::+    sym ->+    SWord sym ->+    SWord sym ->+    SEval sym (SWord sym)++  -- | Bitwise AND+  wordAnd ::+    sym ->+    SWord sym ->+    SWord sym ->+    SEval sym (SWord sym)++  -- | Bitwise XOR+  wordXor ::+    sym ->+    SWord sym ->+    SWord sym ->+    SEval sym (SWord sym)++  -- | Bitwise complement+  wordComplement ::+    sym ->+    SWord sym ->+    SEval sym (SWord sym)++  -- | 2's complement addition of packed words.  The arguments must have+  --   equal bit width, and the result is of the same width. Overflow is silently+  --   discarded.+  wordPlus ::+    sym ->+    SWord sym ->+    SWord sym ->+    SEval sym (SWord sym)++  -- | 2's complement subtraction of packed words.  The arguments must have+  --   equal bit width, and the result is of the same width. Overflow is silently+  --   discarded.+  wordMinus ::+    sym ->+    SWord sym ->+    SWord sym ->+    SEval sym (SWord sym)++  -- | 2's complement multiplication of packed words.  The arguments must have+  --   equal bit width, and the result is of the same width. The high bits of the+  --   multiplication are silently discarded.+  wordMult ::+    sym ->+    SWord sym ->+    SWord sym ->+    SEval sym (SWord sym)++  -- | 2's complement unsigned division of packed words.  The arguments must have+  --   equal bit width, and the result is of the same width.  It is illegal to+  --   call with a second argument concretely equal to 0.+  wordDiv ::+    sym ->+    SWord sym ->+    SWord sym ->+    SEval sym (SWord sym)++  -- | 2's complement unsigned modulus of packed words.  The arguments must have+  --   equal bit width, and the result is of the same width.  It is illegal to+  --   call with a second argument concretely equal to 0.+  wordMod ::+    sym ->+    SWord sym ->+    SWord sym ->+    SEval sym (SWord sym)++  -- | 2's complement signed division of packed words.  The arguments must have+  --   equal bit width, and the result is of the same width.  It is illegal to+  --   call with a second argument concretely equal to 0.+  wordSignedDiv ::+    sym ->+    SWord sym ->+    SWord sym ->+    SEval sym (SWord sym)++  -- | 2's complement signed modulus of packed words.  The arguments must have+  --   equal bit width, and the result is of the same width.  It is illegal to+  --   call with a second argument concretely equal to 0.+  wordSignedMod ::+    sym ->+    SWord sym ->+    SWord sym ->+    SEval sym (SWord sym)++  -- | 2's complement negation of bitvectors+  wordNegate ::+    sym ->+    SWord sym ->+    SEval sym (SWord sym)++  -- | Compute rounded-up log-2 of the input+  wordLg2 ::+    sym ->+    SWord sym ->+    SEval sym (SWord sym)++  -- | Test if two words are equal.  Arguments must have the same width.+  wordEq ::+    sym ->+    SWord sym ->+    SWord sym ->+    SEval sym (SBit sym)++  -- | Signed less-than comparison on words.  Arguments must have the same width.+  wordSignedLessThan ::+    sym ->+    SWord sym ->+    SWord sym ->+    SEval sym (SBit sym)++  -- | Unsigned less-than comparison on words.  Arguments must have the same width.+  wordLessThan ::+    sym ->+    SWord sym ->+    SWord sym ->+    SEval sym (SBit sym)++  -- | Unsigned greater-than comparison on words.  Arguments must have the same width.+  wordGreaterThan ::+    sym ->+    SWord sym ->+    SWord sym ->+    SEval sym (SBit sym)++  -- | Construct an integer value from the given packed word.+  wordToInt ::+    sym ->+    SWord sym ->+    SEval sym (SInteger sym)++  -- ==== Integer operations ====++  -- | Addition of unbounded integers.+  intPlus ::+    sym ->+    SInteger sym ->+    SInteger sym ->+    SEval sym (SInteger sym)++  -- | Negation of unbounded integers+  intNegate ::+    sym ->+    SInteger sym ->+    SEval sym (SInteger sym)++  -- | Subtraction of unbounded integers.+  intMinus ::+    sym ->+    SInteger sym ->+    SInteger sym ->+    SEval sym (SInteger sym)++  -- | Multiplication of unbounded integers.+  intMult ::+    sym ->+    SInteger sym ->+    SInteger sym ->+    SEval sym (SInteger sym)++  -- | Integer division, rounding down. It is illegal to+  --   call with a second argument concretely equal to 0.+  --   Same semantics as Haskell's @div@ operation.+  intDiv ::+    sym ->+    SInteger sym ->+    SInteger sym ->+    SEval sym (SInteger sym)++  -- | Integer modulus, with division rounding down. It is illegal to+  --   call with a second argument concretely equal to 0.+  --   Same semantics as Haskell's @mod@ operation.+  intMod ::+    sym ->+    SInteger sym ->+    SInteger sym ->+    SEval sym (SInteger sym)++  -- | Equality comparison on integers+  intEq ::+    sym ->+    SInteger sym ->+    SInteger sym ->+    SEval sym (SBit sym)++  -- | Less-than comparison on integers+  intLessThan ::+    sym ->+    SInteger sym ->+    SInteger sym ->+    SEval sym (SBit sym)++  -- | Greater-than comparison on integers+  intGreaterThan ::+    sym ->+    SInteger sym ->+    SInteger sym ->+    SEval sym (SBit sym)+++  -- ==== Operations on Z_n ====++  -- | Turn an integer into a value in Z_n+  intToZn ::+    sym ->+    Integer {- ^ modulus -} ->+    SInteger sym ->+    SEval sym (SInteger sym)++  -- | Transform a Z_n value into an integer, ensuring the value is properly+  --   reduced modulo n+  znToInt ::+    sym ->+    Integer {- ^ modulus -} ->+    SInteger sym ->+    SEval sym (SInteger sym)++  -- | Addition of integers modulo n, for a concrete positive integer n.+  znPlus ::+    sym ->+    Integer {- ^ modulus -} ->+    SInteger sym ->+    SInteger sym ->+    SEval sym (SInteger sym)++  -- | Additive inverse of integers modulo n+  znNegate ::+    sym ->+    Integer {- ^ modulus -} ->+    SInteger sym ->+    SEval sym (SInteger sym)++  -- | Subtraction of integers modulo n, for a concrete positive integer n.+  znMinus ::+    sym ->+    Integer {- ^ modulus -} ->+    SInteger sym ->+    SInteger sym ->+    SEval sym (SInteger sym)++  -- | Multiplication of integers modulo n, for a concrete positive integer n.+  znMult ::+    sym ->+    Integer {- ^ modulus -} ->+    SInteger sym ->+    SInteger sym ->+    SEval sym (SInteger sym)++  -- | Equality test of integers modulo n+  znEq ::+    sym ->+    Integer {- ^ modulus -} ->+    SInteger sym ->+    SInteger sym ->+    SEval sym (SBit sym)++  -- == Float Operations ==+  fpEq          :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)+  fpLessThan    :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)+  fpGreaterThan :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)++  fpPlus, fpMinus, fpMult, fpDiv :: FPArith2 sym+  fpNeg :: sym -> SFloat 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)++  fpFromInteger ::+    sym ->+    Integer         {- exp width -} ->+    Integer         {- prec width -} ->+    SWord sym       {- ^ rounding mode -} ->+    SInteger sym    {- ^ the integeer to use -} ->+    SEval sym (SFloat sym)++type FPArith2 sym =+  sym ->+  SWord sym ->+  SFloat sym ->+  SFloat sym ->+  SEval sym (SFloat sym)+++++

@@ -0,0 +1,529 @@+-- |+-- Module      :  Cryptol.Eval.Concrete+-- Copyright   :  (c) 2013-2020 Galois, Inc.+-- License     :  BSD3+-- Maintainer  :  cryptol@galois.com+-- Stability   :  provisional+-- Portability :  portable++{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}+module Cryptol.Eval.Concrete+  ( module Cryptol.Eval.Concrete.Value+  , evalPrim+  , toExpr+  ) where++import Control.Monad (join,guard,zipWithM,mzero)+import Data.Bits (Bits(..))+import Data.Ratio(numerator,denominator)+import MonadLib( ChoiceT, findOne, lift )+import qualified LibBF as FP++import qualified Data.Map.Strict as Map++import Cryptol.TypeCheck.Solver.InfNat (Nat'(..))+import Cryptol.Eval.Backend+import Cryptol.Eval.Concrete.Float(floatPrims)+import Cryptol.Eval.Concrete.FloatHelpers(bfValue)+import Cryptol.Eval.Concrete.Value+import Cryptol.Eval.Generic hiding (logicShift)+import Cryptol.Eval.Monad+import Cryptol.Eval.Type+import Cryptol.Eval.Value+import Cryptol.ModuleSystem.Name+import Cryptol.Testing.Random (randomV)+import Cryptol.TypeCheck.AST as AST+import Cryptol.Utils.Panic (panic)+import Cryptol.Utils.Ident (PrimIdent,prelPrim,floatPrim)+import Cryptol.Utils.PP+import Cryptol.Utils.Logger(logPrint)+import Cryptol.Utils.RecordMap+++-- Value to Expression conversion ----------------------------------------------++-- | Given an expected type, returns an expression that evaluates to+-- this value, if we can determine it.+--+-- XXX: View patterns would probably clean up this definition a lot.+toExpr :: PrimMap -> AST.Type -> 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 ty val = case (tNoUser ty, val) of+    (TRec 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 _ -> mzero -- different fields+        Right efs -> pure (ERec efs)+    (TCon (TC (TCTuple tl)) ts, VTuple tvs) -> do+      guard (tl == (length tvs))+      ETuple `fmap` (zipWithM go ts =<< lift (sequence tvs))+    (TCon (TC TCBit) [], VBit True ) -> return (prim "True")+    (TCon (TC TCBit) [], VBit False) -> return (prim "False")+    (TCon (TC TCInteger) [], VInteger i) ->+      return $ ETApp (ETApp (prim "number") (tNum i)) ty+    (TCon (TC TCIntMod) [_n], VInteger i) ->+      return $ ETApp (ETApp (prim "number") (tNum i)) ty+    (TCon (TC TCRational) [], VRational (SRational n d)) ->+      do let n' = ETApp (ETApp (prim "number") (tNum n)) (TCon (TC TCInteger) [])+             d' = ETApp (ETApp (prim "number") (tNum d)) (TCon (TC TCInteger) [])+         return $ EApp (EApp (prim "ratio") n') d'+    (TCon (TC TCFloat) [eT,pT], VFloat i) ->+      pure (floatToExpr prims eT pT (bfValue i))++    (TCon (TC TCSeq) [a,b], VSeq 0 _) -> do+      guard (a == tZero)+      return $ EList [] b+    (TCon (TC TCSeq) [a,b], VSeq n svs) -> do+      guard (a == tNum n)+      ses <- mapM (go b) =<< lift (sequence (enumerateSeqMap n svs))+      return $ EList ses b+    (TCon (TC TCSeq) [a,(TCon (TC TCBit) [])], VWord _ wval) -> do+      BV w v <- lift (asWordVal Concrete =<< wval)+      guard (a == tNum w)+      return $ 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"+    _ -> do doc <- lift (ppValue Concrete defaultPPOpts val)+            panic "Cryptol.Eval.Concrete.toExpr"+             ["type mismatch:"+             , pretty ty+             , render doc+             ]++floatToExpr :: PrimMap -> AST.Type -> AST.Type -> FP.BigFloat -> AST.Expr+floatToExpr prims eT pT f =+  case FP.bfToRep f of+    FP.BFNaN -> mkP "fpNaN"+    FP.BFRep sign num ->+      case (sign,num) of+        (FP.Pos, FP.Zero)   -> mkP "fpPosZero"+        (FP.Neg, FP.Zero)   -> mkP "fpNegZero"+        (FP.Pos, FP.Inf)    -> mkP "fpPosInf"+        (FP.Neg, FP.Inf)    -> mkP "fpNegInf"+        (_, FP.Num m e) ->+            let r = toRational m * (2 ^^ e)+            in EProofApp $ ePrim prims (prelPrim "fraction")+                          `ETApp` tNum (numerator r)+                          `ETApp` tNum (denominator r)+                          `ETApp` tNum (0 :: Int)+                          `ETApp` tFloat eT pT+  where+  mkP n = EProofApp $ ePrim prims (floatPrim n) `ETApp` eT `ETApp` pT++-- Primitives ------------------------------------------------------------------++evalPrim :: PrimIdent -> Maybe Value+evalPrim prim = Map.lookup prim primTable++primTable :: Map.Map PrimIdent Value+primTable = let sym = Concrete in+  Map.union (floatPrims sym) $+  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::(>>$)" #-}+                    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)+  , (">>"         , {-# SCC "Prelude::(>>)" #-}+                    logicShift shiftRW shiftRS)+  , ("<<<"        , {-# SCC "Prelude::(<<<)" #-}+                    logicShift rotateLW rotateLS)+  , (">>>"        , {-# SCC "Prelude::(>>>)" #-}+                    logicShift rotateRW rotateRS)++    -- Indexing and updates+  , ("@"          , {-# SCC "Prelude::(@)" #-}+                    indexPrim sym indexFront_int indexFront_bits indexFront)+  , ("!"          , {-# SCC "Prelude::(!)" #-}+                    indexPrim sym indexBack_int indexBack_bits indexBack)++  , ("update"     , {-# SCC "Prelude::update" #-}+                    updatePrim sym updateFront_word updateFront)++  , ("updateEnd"  , {-# SCC "Prelude::updateEnd" #-}+                    updatePrim sym updateBack_word updateBack)++    -- Misc+  , ("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+                         EvalOpts { evalPPOpts, evalLogger } <- getEvalOpts+                         doc <- ppValue sym evalPPOpts =<< x+                         yv <- y+                         io $ logPrint evalLogger+                             $ if null msg then doc else text msg <+> doc+                         return yv)+  ]+++--------------------------------------------------------------------------------++sshrV :: Value+sshrV =+  nlam $ \_n ->+  tlam $ \ix ->+  wlam Concrete $ \(BV w x) -> return $+  lam $ \y ->+   do idx <- y >>= asIndex Concrete ">>$" ix >>= \case+                 Left idx -> pure idx+                 Right wv -> bvVal <$> asWordVal Concrete wv+      return $ VWord w $ pure $ WordVal $ mkBv w $ signedShiftRW w x idx++logicShift :: (Integer -> Integer -> Integer -> Integer)+              -- ^ 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+          VInteger i -> pure i+          VWord _ wval -> bvVal <$> (asWordVal Concrete =<< wval)+          _ -> evalPanic "logicShift" ["not an index"]+        l >>= \case+          VWord w wv -> return $ VWord w $ wv >>= \case+                          WordVal (BV _ x) -> return $ WordVal (BV w (opW w x i))+                          LargeBitsVal n xs -> return $ LargeBitsVal n $ opS (Nat n) c xs i++          _ -> mkSeq a c <$> (opS a c <$> (fromSeq "logicShift" =<< l) <*> return i)++-- Left shift for words.+shiftLW :: Integer -> Integer -> Integer -> Integer+shiftLW w ival by+  | by <  0   = shiftRW w ival (negate by)+  | by >= w   = 0+  | by > toInteger (maxBound :: Int) = panic "shiftLW" ["Shift amount too large", show by]+  | otherwise = mask w (shiftL ival (fromInteger by))++-- Right shift for words+shiftRW :: Integer -> Integer -> Integer -> Integer+shiftRW w ival by+  | by <  0   = shiftLW w ival (negate by)+  | by >= w   = 0+  | by > toInteger (maxBound :: Int) = panic "shiftRW" ["Shift amount too large", show by]+  | otherwise = shiftR ival (fromInteger by)++-- signed right shift for words+signedShiftRW :: Integer -> Integer -> Integer -> Integer+signedShiftRW w ival by+  | by < 0    = shiftLW w ival (negate by)+  | otherwise =+     let by' = min w by in+     if by' > toInteger (maxBound :: Int) then+       panic "signedShiftRW" ["Shift amount too large", show by]+     else+       shiftR (signedValue w ival) (fromInteger by')++shiftLS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete+shiftLS w ety vs by+  | by < 0 = shiftRS w ety vs (negate by)++shiftLS w ety vs by = IndexSeqMap $ \i ->+  case w of+    Nat len+      | i+by < len -> lookupSeqMap vs (i+by)+      | i    < len -> zeroV Concrete ety+      | otherwise  -> evalPanic "shiftLS" ["Index out of bounds"]+    Inf            -> lookupSeqMap vs (i+by)++shiftRS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete+shiftRS w ety vs by+  | by < 0 = shiftLS w ety vs (negate by)++shiftRS w ety vs by = IndexSeqMap $ \i ->+  case w of+    Nat len+      | i >= by   -> lookupSeqMap vs (i-by)+      | i < len   -> zeroV Concrete ety+      | otherwise -> evalPanic "shiftLS" ["Index out of bounds"]+    Inf+      | i >= by   -> lookupSeqMap vs (i-by)+      | otherwise -> zeroV Concrete ety+++-- XXX integer doesn't implement rotateL, as there's no bit bound+rotateLW :: Integer -> Integer -> Integer -> Integer+rotateLW 0 i _  = i+rotateLW w i by = mask w $ (i `shiftL` b) .|. (i `shiftR` (fromInteger w - b))+  where b = fromInteger (by `mod` w)++rotateLS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete+rotateLS w _ vs by = IndexSeqMap $ \i ->+  case w of+    Nat len -> lookupSeqMap vs ((by + i) `mod` len)+    _ -> panic "Cryptol.Eval.Prim.rotateLS" [ "unexpected infinite sequence" ]++-- XXX integer doesn't implement rotateR, as there's no bit bound+rotateRW :: Integer -> Integer -> Integer -> Integer+rotateRW 0 i _  = i+rotateRW w i by = mask w $ (i `shiftR` b) .|. (i `shiftL` (fromInteger w - b))+  where b = fromInteger (by `mod` w)++rotateRS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete+rotateRS w _ vs by = IndexSeqMap $ \i ->+  case w of+    Nat len -> lookupSeqMap vs ((len - by + i) `mod` len)+    _ -> panic "Cryptol.Eval.Prim.rotateRS" [ "unexpected infinite sequence" ]+++-- Sequence Primitives ---------------------------------------------------------++indexFront :: Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value+indexFront _mblen _a vs _ix (bvVal -> ix) = lookupSeqMap vs ix++indexFront_bits :: Nat' -> TValue -> SeqMap Concrete -> TValue -> [Bool] -> Eval Value+indexFront_bits mblen a vs ix bs = indexFront mblen a vs ix =<< packWord Concrete bs++indexFront_int :: Nat' -> TValue -> SeqMap Concrete -> TValue -> Integer -> Eval Value+indexFront_int _mblen _a vs _ix idx = lookupSeqMap vs idx++indexBack :: Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value+indexBack mblen a vs ix (bvVal -> idx) = indexBack_int mblen a vs ix idx++indexBack_bits :: Nat' -> TValue -> SeqMap Concrete -> TValue -> [Bool] -> Eval Value+indexBack_bits mblen a vs ix bs = indexBack mblen a vs ix =<< packWord Concrete bs++indexBack_int :: Nat' -> TValue -> SeqMap Concrete -> TValue -> Integer -> Eval Value+indexBack_int mblen _a vs _ix idx =+  case mblen of+    Nat len -> lookupSeqMap vs (len - idx - 1)+    Inf     -> evalPanic "indexBack" ["unexpected infinite sequence"]++updateFront ::+  Nat'               {- ^ length of the sequence -} ->+  TValue             {- ^ type of values in the sequence -} ->+  SeqMap Concrete    {- ^ sequence to update -} ->+  Either Integer (WordValue Concrete) {- ^ index -} ->+  Eval Value         {- ^ new value at index -} ->+  Eval (SeqMap Concrete)+updateFront _len _eltTy vs (Left idx) val = do+  return $ updateSeqMap vs idx val++updateFront _len _eltTy vs (Right w) val = do+  idx <- bvVal <$> asWordVal Concrete w+  return $ updateSeqMap vs idx val++updateFront_word ::+  Nat'               {- ^ length of the sequence -} ->+  TValue             {- ^ type of values in the sequence -} ->+  WordValue Concrete {- ^ bit sequence to update -} ->+  Either Integer (WordValue Concrete) {- ^ index -} ->+  Eval Value         {- ^ new value at index -} ->+  Eval (WordValue Concrete)+updateFront_word _len _eltTy bs (Left idx) val = do+  updateWordValue Concrete bs idx (fromVBit <$> val)++updateFront_word _len _eltTy bs (Right w) val = do+  idx <- bvVal <$> asWordVal Concrete w+  updateWordValue Concrete bs idx (fromVBit <$> val)++updateBack ::+  Nat'               {- ^ length of the sequence -} ->+  TValue             {- ^ type of values in the sequence -} ->+  SeqMap Concrete    {- ^ sequence to update -} ->+  Either Integer (WordValue Concrete) {- ^ index -} ->+  Eval Value         {- ^ new value at index -} ->+  Eval (SeqMap Concrete)+updateBack Inf _eltTy _vs _w _val =+  evalPanic "Unexpected infinite sequence in updateEnd" []+updateBack (Nat n) _eltTy vs (Left idx) val = do+  return $ updateSeqMap vs (n - idx - 1) val+updateBack (Nat n) _eltTy vs (Right w) val = do+  idx <- bvVal <$> asWordVal Concrete w+  return $ updateSeqMap vs (n - idx - 1) val++updateBack_word ::+  Nat'               {- ^ length of the sequence -} ->+  TValue             {- ^ type of values in the sequence -} ->+  WordValue Concrete {- ^ bit sequence to update -} ->+  Either Integer (WordValue Concrete) {- ^ index -} ->+  Eval Value         {- ^ new value at index -} ->+  Eval (WordValue Concrete)+updateBack_word Inf _eltTy _bs _w _val =+  evalPanic "Unexpected infinite sequence in updateEnd" []+updateBack_word (Nat n) _eltTy bs (Left idx) val = do+  updateWordValue Concrete bs (n - idx - 1) (fromVBit <$> val)+updateBack_word (Nat n) _eltTy bs (Right w) val = do+  idx <- bvVal <$> asWordVal Concrete w+  updateWordValue Concrete bs (n - idx - 1) (fromVBit <$> val)

@@ -0,0 +1,69 @@+{-# Language BlockArguments #-}+{-# Language OverloadedStrings #-}+-- | Concrete evaluations for floating point primitives.+module Cryptol.Eval.Concrete.Float where++import Data.Map(Map)+import Data.Ratio((%),numerator,denominator)+import qualified Data.Map as Map+import LibBF++import Cryptol.Utils.Ident(PrimIdent, floatPrim)+import Cryptol.Eval.Value+import Cryptol.Eval.Generic+import Cryptol.Eval.Concrete.Value+import Cryptol.Eval.Backend(SRational(..))+import Cryptol.Eval.Concrete.FloatHelpers++++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 = bfNaN+                                  , bfExpWidth = e, bfPrecWidth = p }++    , "fpPosInf"    ~> ilam \e -> ilam \p ->+                       VFloat BF { bfValue = 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+                            $ bfCompare (bfValue x) (bfValue y) == EQ++    , "fpIsFinite"  ~> ilam \_ -> ilam \_ -> flam \x ->+                       pure $ VBit $ bitLit sym $ 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 }+    ]++

@@ -0,0 +1,252 @@+{-# Language BlockArguments, OverloadedStrings #-}+{-# Language BangPatterns #-}+module Cryptol.Eval.Concrete.FloatHelpers where++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.Eval.Monad( EvalError(..)+                         , PPOpts(..), PPFloatFormat(..), PPFloatExp(..)+                         )+++data BF = BF+  { bfExpWidth  :: Integer+  , bfPrecWidth :: Integer+  , bfValue     :: BigFloat+  }+++-- | Make LibBF options for the given precision and rounding mode.+fpOpts :: Integer -> Integer -> RoundMode -> BFOpts+fpOpts e p r =+  case ok of+    Just opts -> opts+    Nothing   -> panic "floatOpts" [ "Invalid Float size"+                                   , "exponent: " ++ show e+                                   , "precision: " ++ show p+                                   ]+  where+  ok = do eb <- rng expBits expBitsMin expBitsMax e+          pb <- rng precBits precBitsMin precBitsMax p+          pure (eb <> pb <> allowSubnormal <> rnd r)++  rng f a b x = if toInteger a <= x && x <= toInteger b+                  then Just (f (fromInteger x))+                  else Nothing++++-- | Mapping from the rounding modes defined in the `Float.cry` to+-- the rounding modes of `LibBF`.+fpRound :: Integer -> Either EvalError RoundMode+fpRound n =+  case n of+    0 -> Right NearEven+    1 -> Right NearAway+    2 -> Right ToPosInf+    3 -> Right ToNegInf+    4 -> Right ToZero+    _ -> Left (BadRoundingMode n)++-- | Check that we didn't get an unexpected status.+fpCheckStatus :: (BigFloat,Status) -> BigFloat+fpCheckStatus (r,s) =+  case s of+    MemError  -> panic "checkStatus" [ "libBF: Memory error" ]+    _         -> r+++-- | Pretty print a float+fpPP :: PPOpts -> BF -> Doc+fpPP opts bf =+  case bfSign num of+    Nothing -> "fpNaN"+    Just s+      | bfIsFinite num -> text hacStr+      | otherwise ->+        case s of+          Pos -> "fpPosInf"+          Neg -> "fpNegInf"+  where+  num = bfValue bf+  precW = bfPrecWidth bf++  base  = useFPBase opts++  withExp :: PPFloatExp -> ShowFmt -> ShowFmt+  withExp e f = case e of+                  AutoExponent -> f+                  ForceExponent -> f <> forceExp++  str = bfToString base fmt num+  fmt = addPrefix <> showRnd NearEven <>+        case useFPFormat opts of+          FloatFree e -> withExp e $ showFreeMin+                                   $ 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. +  hacStr+    | base == 10 || elem '.' str = str+    | otherwise = case break (== 'p') str of+                    (xs,ys) -> xs ++ ".0" ++ ys+++-- | Make a literal+fpLit ::+  Integer     {- ^ Exponent width -} ->+  Integer     {- ^ Precision width -} ->+  Rational ->+  BF+fpLit e p rat = floatFromRational e p NearEven rat++-- | Make a floating point number from a rational, using the given rounding mode+floatFromRational :: Integer -> Integer -> RoundMode -> Rational -> BF+floatFromRational e p r rat =+  BF { bfExpWidth = e+     , bfPrecWidth = p+     , bfValue = fpCheckStatus+                 if den == 1 then bfRoundFloat opts num+                             else bfDiv opts num (bfFromInteger den)+     }+  where+  opts  = fpOpts e p r++  num   = bfFromInteger (numerator rat)+  den   = denominator rat+++-- | Convert a floating point number to a rational, if possible.+floatToRational :: String -> BF -> Either EvalError Rational+floatToRational fun bf =+  case bfToRep (bfValue bf) of+    BFNaN -> Left (BadValue fun)+    BFRep s num ->+      case num of+        Inf  -> Left (BadValue fun)+        Zero -> Right 0+        Num i ev -> Right case s of+                            Pos -> ab+                            Neg -> negate ab+          where ab = fromInteger i * (2 ^^ ev)+++-- | Convert a floating point number to an integer, if possible.+floatToInteger :: String -> RoundMode -> BF -> Either EvalError Integer+floatToInteger fun r fp =+  do rat <- floatToRational fun fp+     pure case r of+            NearEven -> round rat+            NearAway -> if rat > 0 then ceiling rat else floor rat+            ToPosInf -> ceiling rat+            ToNegInf -> floor rat+            ToZero   -> truncate rat+            _        -> panic "fpCvtToInteger"+                              ["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+                          , 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)++++

@@ -0,0 +1,390 @@+-- |fpToInteger r e p f+-- Module      :  Cryptol.Eval.Concrete.Value+-- Copyright   :  (c) 2013-2020 Galois, Inc.+-- License     :  BSD3+-- Maintainer  :  cryptol@galois.com+-- Stability   :  provisional+-- Portability :  portable++{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}+module Cryptol.Eval.Concrete.Value+  ( BV(..)+  , binBV+  , unaryBV+  , bvVal+  , ppBV+  , mkBv+  , mask+  , signedBV+  , signedValue+  , integerToChar+  , lg2+  , Value+  , Concrete(..)+  , liftBinIntMod+  , fpBinArith+  , fpRoundMode+  ) where++import qualified Control.Exception as X+import Data.Bits+import Numeric (showIntAtBase)+import qualified LibBF as FP++import qualified Cryptol.Eval.Arch as Arch+import qualified Cryptol.Eval.Concrete.FloatHelpers as FP+import Cryptol.Eval.Monad+import Cryptol.Eval.Value+import Cryptol.TypeCheck.Solver.InfNat (genLog)+import Cryptol.Utils.Panic (panic)+import Cryptol.Utils.PP++data Concrete = Concrete deriving Show++type Value = GenValue Concrete++-- | Concrete bitvector values: width, value+-- Invariant: The value must be within the range 0 .. 2^width-1+data BV = BV !Integer !Integer++instance Show BV where+  show = show . bvVal++-- | Apply an integer function to the values of bitvectors.+--   This function assumes both bitvectors are the same width.+binBV :: Applicative m => (Integer -> Integer -> Integer) -> BV -> BV -> m BV+binBV f (BV w x) (BV _ y) = pure $! mkBv w (f x y)+{-# INLINE binBV #-}++-- | Apply an integer function to the values of a bitvector.+--   This function assumes the function will not require masking.+unaryBV :: (Integer -> Integer) -> BV -> BV+unaryBV f (BV w x) = mkBv w $! f x+{-# INLINE unaryBV #-}++bvVal :: BV -> Integer+bvVal (BV _w x) = x+{-# INLINE bvVal #-}++-- | Smart constructor for 'BV's that checks for the width limit+mkBv :: Integer -> Integer -> BV+mkBv w i = BV w (mask w i)++signedBV :: BV -> Integer+signedBV (BV i x) = signedValue i x++signedValue :: Integer -> Integer -> Integer+signedValue i x = if testBit x (fromInteger (i-1)) then x - (bit (fromInteger i)) else x++integerToChar :: Integer -> Char+integerToChar = toEnum . fromInteger++lg2 :: Integer -> Integer+lg2 i = case genLog i 2 of+  Just (i',isExact) | isExact   -> i'+                    | otherwise -> i' + 1+  Nothing                       -> 0+++ppBV :: PPOpts -> BV -> Doc+ppBV opts (BV width i)+  | base > 36 = integer i -- not sure how to rule this out+  | asciiMode opts width = text (show (toEnum (fromInteger i) :: Char))+  | otherwise = prefix <.> text value+  where+  base = useBase opts++  padding bitsPerDigit = text (replicate padLen '0')+    where+    padLen | m > 0     = d + 1+           | otherwise = d++    (d,m) = (fromInteger width - (length value * bitsPerDigit))+                   `divMod` bitsPerDigit++  prefix = case base of+    2  -> text "0b" <.> padding 1+    8  -> text "0o" <.> padding 3+    10 -> empty+    16 -> text "0x" <.> padding 4+    _  -> text "0"  <.> char '<' <.> int base <.> char '>'++  value  = showIntAtBase (toInteger base) (digits !!) i ""+  digits = "0123456789abcdefghijklmnopqrstuvwxyz"++-- Concrete Big-endian Words ------------------------------------------------------------++mask ::+  Integer  {- ^ Bit-width -} ->+  Integer  {- ^ Value -} ->+  Integer  {- ^ Masked result -}+mask w i | w >= Arch.maxBigIntWidth = wordTooWide w+         | otherwise                = i .&. (bit (fromInteger w) - 1)++instance Backend Concrete where+  type SBit Concrete = Bool+  type SWord Concrete = BV+  type SInteger Concrete = Integer+  type SFloat Concrete = FP.BF+  type SEval Concrete = Eval++  raiseError _ err = io (X.throwIO err)++  assertSideCondition _ True _ = return ()+  assertSideCondition _ False err = io (X.throwIO err)++  wordLen _ (BV w _) = w+  wordAsChar _ (BV _ x) = Just $! integerToChar x++  wordBit _ (BV w x) idx = pure $! testBit x (fromInteger (w - 1 - idx))++  wordUpdate _ (BV w x) idx True  = pure $! BV w (setBit   x (fromInteger (w - 1 - idx)))+  wordUpdate _ (BV w x) idx False = pure $! BV w (clearBit x (fromInteger (w - 1 - idx)))++  isReady _ (Ready _) = True+  isReady _ _ = False++  mergeEval _sym f c mx my =+    do x <- mx+       y <- my+       f c x y++  sDeclareHole _ = blackhole+  sDelayFill _ = delayFill+  sSpark _ = evalSpark++  ppBit _ b | b         = text "True"+            | otherwise = text "False"++  ppWord _ = ppBV++  ppInteger _ _opts i = integer i++  ppFloat _ = FP.fpPP++  bitLit _ b = b+  bitAsLit _ b = Just b++  bitEq _  x y = pure $! x == y+  bitOr _  x y = pure $! x .|. y+  bitAnd _ x y = pure $! x .&. y+  bitXor _ x y = pure $! x `xor` y+  bitComplement _ x = pure $! complement x++  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++  wordLit _ w i = pure $! mkBv w i+  wordAsLit _ (BV w i) = Just (w,i)+  integerLit _ i = pure i+  integerAsLit _ = Just++  wordToInt _ (BV _ x) = pure x+  wordFromInt _ w x = pure $! mkBv w x++  packWord _ bits = pure $! BV (toInteger w) a+    where+      w = case length bits of+            len | toInteger len >= Arch.maxBigIntWidth -> wordTooWide (toInteger len)+                | otherwise                  -> len+      a = foldl setb 0 (zip [w - 1, w - 2 .. 0] bits)+      setb acc (n,b) | b         = setBit acc n+                     | otherwise = acc++  unpackWord _ (BV w a) = pure [ testBit a n | n <- [w' - 1, w' - 2 .. 0] ]+    where+      w' = fromInteger w++  joinWord _ (BV i x) (BV j y) =+    pure $! BV (i + j) (shiftL x (fromInteger j) + y)++  splitWord _ leftW rightW (BV _ x) =+    pure ( BV leftW (x `shiftR` (fromInteger rightW)), mkBv rightW x )++  extractWord _ n i (BV _ x) = pure $! mkBv n (x `shiftR` (fromInteger i))++  wordEq _ (BV i x) (BV j y)+    | i == j = pure $! x == y+    | otherwise = panic "Attempt to compare words of different sizes: wordEq" [show i, show j]++  wordSignedLessThan _ (BV i x) (BV j y)+    | i == j = pure $! signedValue i x < signedValue i y+    | otherwise = panic "Attempt to compare words of different sizes: wordSignedLessThan" [show i, show j]++  wordLessThan _ (BV i x) (BV j y)+    | i == j = pure $! x < y+    | otherwise = panic "Attempt to compare words of different sizes: wordLessThan" [show i, show j]++  wordGreaterThan _ (BV i x) (BV j y)+    | i == j = pure $! x > y+    | otherwise = panic "Attempt to compare words of different sizes: wordGreaterThan" [show i, show j]++  wordAnd _ (BV i x) (BV j y)+    | i == j = pure $! mkBv i (x .&. y)+    | otherwise = panic "Attempt to AND words of different sizes: wordPlus" [show i, show j]++  wordOr _ (BV i x) (BV j y)+    | i == j = pure $! mkBv i (x .|. y)+    | otherwise = panic "Attempt to OR words of different sizes: wordPlus" [show i, show j]++  wordXor _ (BV i x) (BV j y)+    | i == j = pure $! mkBv i (x `xor` y)+    | otherwise = panic "Attempt to XOR words of different sizes: wordPlus" [show i, show j]++  wordComplement _ (BV i x) = pure $! mkBv i (complement x)++  wordPlus _ (BV i x) (BV j y)+    | i == j = pure $! mkBv i (x+y)+    | otherwise = panic "Attempt to add words of different sizes: wordPlus" [show i, show j]++  wordNegate _ (BV i x) = pure $! mkBv i (negate x)++  wordMinus _ (BV i x) (BV j y)+    | i == j = pure $! mkBv i (x-y)+    | otherwise = panic "Attempt to subtract words of different sizes: wordMinus" [show i, show j]++  wordMult _ (BV i x) (BV j y)+    | i == j = pure $! mkBv i (x*y)+    | otherwise = panic "Attempt to multiply words of different sizes: wordMult" [show i, show j]++  wordDiv sym (BV i x) (BV j y)+    | i == 0 && j == 0 = pure $! mkBv 0 0+    | i == j =+        do assertSideCondition sym (y /= 0) DivideByZero+           pure $! mkBv i (x `div` y)+    | otherwise = panic "Attempt to divide words of different sizes: wordDiv" [show i, show j]++  wordMod sym (BV i x) (BV j y)+    | i == 0 && j == 0 = pure $! mkBv 0 0+    | i == j =+        do assertSideCondition sym (y /= 0) DivideByZero+           pure $! mkBv i (x `mod` y)+    | otherwise = panic "Attempt to mod words of different sizes: wordMod" [show i, show j]++  wordSignedDiv sym (BV i x) (BV j y)+    | i == 0 && j == 0 = pure $! mkBv 0 0+    | i == j =+        do assertSideCondition sym (y /= 0) DivideByZero+           let sx = signedValue i x+               sy = signedValue i y+           pure $! mkBv i (sx `quot` sy)+    | otherwise = panic "Attempt to divide words of different sizes: wordSignedDiv" [show i, show j]++  wordSignedMod sym (BV i x) (BV j y)+    | i == 0 && j == 0 = pure $! mkBv 0 0+    | i == j =+        do assertSideCondition sym (y /= 0) DivideByZero+           let sx = signedValue i x+               sy = signedValue i y+           pure $! mkBv i (sx `rem` sy)+    | otherwise = panic "Attempt to mod words of different sizes: wordSignedMod" [show i, show j]++  wordLg2 _ (BV i x) = pure $! mkBv i (lg2 x)++  intEq _ x y = pure $! x == y+  intLessThan _ x y = pure $! x < y+  intGreaterThan _ x y = pure $! x > y++  intPlus  _ x y = pure $! x + y+  intMinus _ x y = pure $! x - y+  intNegate _ x  = pure $! negate x+  intMult  _ x y = pure $! x * y+  intDiv sym x y =+    do assertSideCondition sym (y /= 0) DivideByZero+       pure $! x `div` y+  intMod sym x y =+    do assertSideCondition sym (y /= 0) DivideByZero+       pure $! x `mod` y++  intToZn _ 0 _ = evalPanic "intToZn" ["0 modulus not allowed"]+  intToZn _ m x = pure $! x `mod` m++  -- NB: requires we maintain the invariant that+  --     Z_n is in reduced form+  znToInt _ _m x = pure x+  znEq _ _m x y = pure $! x == y++  znPlus  _ = liftBinIntMod (+)+  znMinus _ = liftBinIntMod (-)+  znMult  _ = liftBinIntMod (*)+  znNegate _ 0 _ = evalPanic "znNegate" ["0 modulus not allowed"]+  znNegate _ m x = pure $! (negate x) `mod` m++  ------------------------------------------------------------------------+  -- Floating Point+  fpLit _sym e p rat     = pure (FP.fpLit e p rat)+  fpEq _sym x y          = pure (FP.bfValue x == FP.bfValue y)+  fpLessThan _sym x y    = pure (FP.bfValue x <  FP.bfValue y)+  fpGreaterThan _sym x y = pure (FP.bfValue x >  FP.bfValue y)+  fpPlus  = fpBinArith FP.bfAdd+  fpMinus = fpBinArith FP.bfSub+  fpMult  = fpBinArith FP.bfMul+  fpDiv   = fpBinArith FP.bfDiv+  fpNeg _ x = pure x { FP.bfValue = FP.bfNeg (FP.bfValue x) }+  fpFromInteger sym e p r x =+    do opts <- FP.fpOpts e p <$> fpRoundMode sym r+       pure FP.BF { FP.bfExpWidth = e+                  , FP.bfPrecWidth = p+                  , FP.bfValue = FP.fpCheckStatus $+                                 FP.bfRoundInt opts (FP.bfFromInteger x)+                  }+  fpToInteger = fpCvtToInteger+++{-# INLINE liftBinIntMod #-}+liftBinIntMod :: Monad m =>+  (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer -> m Integer+liftBinIntMod op m x y+  | m == 0    = evalPanic "znArithmetic" ["0 modulus not allowed"]+  | otherwise = pure $ (op x y) `mod` m++++{-# INLINE fpBinArith #-}+fpBinArith ::+  (FP.BFOpts -> FP.BigFloat -> FP.BigFloat -> (FP.BigFloat, FP.Status)) ->+  Concrete ->+  SWord Concrete  {- ^ Rouding mode -} ->+  SFloat Concrete ->+  SFloat Concrete ->+  SEval Concrete (SFloat Concrete)+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+                                (fun opts (FP.bfValue x) (FP.bfValue y)) }++fpCvtToInteger ::+  Concrete ->+  String ->+  SWord Concrete {- ^ Rounding mode -} ->+  SFloat Concrete ->+  SEval Concrete (SInteger Concrete)+fpCvtToInteger sym fun rnd flt =+  do mode <- fpRoundMode sym rnd+     case FP.floatToInteger fun mode flt of+       Right i -> pure i+       Left err -> raiseError sym err++fpRoundMode :: Concrete -> SWord Concrete -> SEval Concrete FP.RoundMode+fpRoundMode sym w =+  case FP.fpRound (bvVal w) of+    Left err -> raiseError sym err+    Right a  -> pure a+++++

@@ -14,7 +14,8 @@ {-# LANGUAGE DeriveGeneric #-} module Cryptol.Eval.Env where -import Cryptol.Eval.Monad( Eval, delay, ready, PPOpts )+import Cryptol.Eval.Backend+import Cryptol.Eval.Monad( PPOpts ) import Cryptol.Eval.Type import Cryptol.Eval.Value import Cryptol.ModuleSystem.Name@@ -27,25 +28,24 @@ import Data.Semigroup  import GHC.Generics (Generic)-import Control.DeepSeq  import Prelude () import Prelude.Compat  -- Evaluation Environment ------------------------------------------------------ -data GenEvalEnv b w i = EvalEnv-  { envVars       :: !(Map.Map Name (Eval (GenValue b w i)))+data GenEvalEnv sym = EvalEnv+  { envVars       :: !(Map.Map Name (SEval sym (GenValue sym)))   , envTypes      :: !TypeEnv-  } deriving (Generic, NFData)+  } deriving Generic -instance Semigroup (GenEvalEnv b w i) where+instance Semigroup (GenEvalEnv sym) where   l <> r = EvalEnv     { envVars     = Map.union (envVars     l) (envVars     r)     , envTypes    = Map.union (envTypes    l) (envTypes    r)     } -instance Monoid (GenEvalEnv b w i) where+instance Monoid (GenEvalEnv sym) where   mempty = EvalEnv     { envVars       = Map.empty     , envTypes      = Map.empty@@ -53,47 +53,52 @@    mappend l r = l <> r -ppEnv :: BitWord b w i => PPOpts -> GenEvalEnv b w i -> Eval Doc-ppEnv opts env = brackets . fsep <$> mapM bind (Map.toList (envVars env))+ppEnv :: Backend sym => sym -> PPOpts -> GenEvalEnv sym -> SEval sym Doc+ppEnv sym opts env = brackets . fsep <$> mapM bind (Map.toList (envVars env))   where-   bind (k,v) = do vdoc <- ppValue opts =<< v+   bind (k,v) = do vdoc <- ppValue sym opts =<< v                    return (pp k <+> text "->" <+> vdoc)  -- | Evaluation environment with no bindings-emptyEnv :: GenEvalEnv b w i+emptyEnv :: GenEvalEnv sym emptyEnv  = mempty  -- | Bind a variable in the evaluation environment.-bindVar :: Name-        -> Eval (GenValue b w i)-        -> GenEvalEnv b w i-        -> Eval (GenEvalEnv b w i)-bindVar n val env = do+bindVar ::+  Backend sym =>+  sym ->+  Name ->+  SEval sym (GenValue sym) ->+  GenEvalEnv sym ->+  SEval sym (GenEvalEnv sym)+bindVar sym n val env = do   let nm = show $ ppLocName n-  val' <- delay (Just nm) val+  val' <- sDelay sym (Just nm) val   return $ env{ envVars = Map.insert n val' (envVars env) }  -- | Bind a variable to a value in the evaluation environment, without --   creating a thunk.-bindVarDirect :: Name-              -> GenValue b w i-              -> GenEvalEnv b w i-              -> GenEvalEnv b w i+bindVarDirect ::+  Backend sym =>+  Name ->+  GenValue sym ->+  GenEvalEnv sym ->+  GenEvalEnv sym bindVarDirect n val env = do-  env{ envVars = Map.insert n (ready val) (envVars env) }+  env{ envVars = Map.insert n (pure val) (envVars env) }  -- | Lookup a variable in the environment. {-# INLINE lookupVar #-}-lookupVar :: Name -> GenEvalEnv b w i -> Maybe (Eval (GenValue b w i))+lookupVar :: Name -> GenEvalEnv sym -> Maybe (SEval sym (GenValue sym)) lookupVar n env = Map.lookup n (envVars env)  -- | Bind a type variable of kind *. {-# INLINE bindType #-}-bindType :: TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i+bindType :: TVar -> Either Nat' TValue -> GenEvalEnv sym -> GenEvalEnv sym bindType p ty env = env { envTypes = Map.insert p ty (envTypes env) }  -- | Lookup a type variable. {-# INLINE lookupType #-}-lookupType :: TVar -> GenEvalEnv b w i -> Maybe (Either Nat' TValue)+lookupType :: TVar -> GenEvalEnv sym -> Maybe (Either Nat' TValue) lookupType p env = Map.lookup p (envTypes env) 

@@ -0,0 +1,1965 @@+-- |+-- Module      :  Cryptol.Eval.Generic+-- Copyright   :  (c) 2013-2020 Galois, Inc.+-- License     :  BSD3+-- Maintainer  :  cryptol@galois.com+-- Stability   :  provisional+-- Portability :  portable++{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE BangPatterns #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Cryptol.Eval.Generic where++import qualified Control.Exception as X+import Control.Monad.IO.Class (MonadIO(..))+import Control.Monad (join, unless)++import Data.Bits (testBit)+import Data.Maybe (fromMaybe)+import Data.Ratio ((%))++import Cryptol.TypeCheck.AST+import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),nMul,widthInteger)+import Cryptol.Eval.Backend+import Cryptol.Eval.Concrete.Value (Concrete(..))+import Cryptol.Eval.Monad+import Cryptol.Eval.Type+import Cryptol.Eval.Value+import Cryptol.Utils.Panic (panic)+import Cryptol.Utils.RecordMap++++{-# SPECIALIZE mkLit :: Concrete -> TValue -> Integer -> Eval (GenValue Concrete)+  #-}++-- | Make a numeric literal value at the given type.+mkLit :: Backend sym => sym -> TValue -> Integer -> SEval sym (GenValue sym)+mkLit sym ty i =+  case ty of+    TVInteger                    -> VInteger <$> integerLit sym i+    TVIntMod m+      | m == 0                   -> evalPanic "mkLit" ["0 modulus not allowed"]+      | otherwise                -> VInteger <$> integerLit sym (i `mod` m)+    TVFloat e p                  -> VFloat <$> fpLit sym e p (fromInteger i)+    TVSeq w TVBit                -> pure $ word sym w i+    TVRational                   -> VRational <$> (intToRational sym =<< integerLit sym i)+    _                            -> evalPanic "Cryptol.Eval.Prim.evalConst"+                                    [ "Invalid type for number" ]++{-# SPECIALIZE ecNumberV :: Concrete -> GenValue Concrete+  #-}++-- | Make a numeric constant.+ecNumberV :: Backend sym => sym -> GenValue sym+ecNumberV sym =+  nlam $ \valT ->+  VPoly $ \ty ->+  case valT of+    Nat v -> mkLit sym ty v+    _ -> evalPanic "Cryptol.Eval.Prim.evalConst"+             ["Unexpected Inf in constant."+             , show valT+             , show ty+             ]++++{-# 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)++{-# SPECIALIZE ratioV :: Concrete -> GenValue Concrete #-}+ratioV :: Backend sym => sym -> GenValue sym+ratioV sym =+  lam $ \x -> return $+  lam $ \y ->+    do x' <- fromVInteger <$> x+       y' <- fromVInteger <$> y+       VRational <$> ratio sym x' y'++{-# SPECIALIZE ecFractionV :: Concrete -> GenValue Concrete+  #-}+ecFractionV :: Backend sym => sym -> GenValue sym+ecFractionV sym =+  ilam  \n ->+  ilam  \d ->+  ilam  \_r ->+  VPoly \ty ->+    case ty of+      TVFloat e p -> VFloat    <$> fpLit sym e p (n % d)+      TVRational ->+        do x <- integerLit sym n+           y <- integerLit sym d+           VRational <$> ratio sym x y++      _ -> evalPanic "ecFractionV"+            [ "Unexpected `FLiteral` type: " ++ show ty ]++++{-# SPECIALIZE fromZV :: Concrete -> GenValue Concrete #-}+fromZV :: Backend sym => sym -> GenValue sym+fromZV sym =+  nlam $ \(finNat' -> n) ->+  lam $ \v -> 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+  #-}+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)++type Unary sym = TValue -> GenValue sym -> SEval sym (GenValue sym)++{-# SPECIALIZE unary :: Unary Concrete -> GenValue Concrete+  #-}+unary :: Backend sym => Unary sym -> GenValue sym+unary f = tlam $ \ ty ->+           lam $ \ a  -> f ty =<< a+++type BinWord sym = Integer -> SWord sym -> SWord sym -> SEval sym (SWord sym)++{-# SPECIALIZE ringBinary :: Concrete -> BinWord Concrete ->+      (SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->+      (Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->+      (SRational Concrete -> SRational Concrete -> SEval Concrete (SRational Concrete)) ->+      (SFloat Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)) ->+      Binary Concrete+  #-}++ringBinary :: forall sym.+  Backend sym =>+  sym ->+  BinWord sym ->+  (SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->+  (Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->+  (SRational sym -> SRational sym -> SEval sym (SRational sym)) ->+  (SFloat sym -> SFloat sym -> SEval sym (SFloat sym)) ->+  Binary sym+ringBinary sym opw opi opz opq opfp = loop+  where+  loop' :: TValue+        -> SEval sym (GenValue sym)+        -> SEval sym (GenValue sym)+        -> SEval sym (GenValue sym)+  loop' ty l r = join (loop ty <$> l <*> r)++  loop :: TValue+       -> GenValue sym+       -> GenValue sym+       -> SEval sym (GenValue sym)+  loop ty l r = case ty of+    TVBit ->+      evalPanic "ringBinary" ["Bit not in class Ring"]++    TVInteger ->+      VInteger <$> opi (fromVInteger l) (fromVInteger r)++    TVIntMod n ->+      VInteger <$> opz n (fromVInteger l) (fromVInteger r)++    TVFloat {} ->+      VFloat <$> opfp (fromVFloat l) (fromVFloat r)++    TVRational ->+      VRational <$> opq (fromVRational l) (fromVRational r)++    TVArray{} ->+      evalPanic "arithBinary" ["Array not in class Ring"]++    TVSeq w a+      -- words and finite sequences+      | 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) <$>+                                      (fromSeq "ringBinary left" l) <*>+                                      (fromSeq "ringBinary right" r)))++    TVStream a ->+      -- streams+      VStream <$> (join (zipSeqMap (loop a) <$>+                             (fromSeq "ringBinary left" l) <*>+                             (fromSeq "ringBinary right" r)))++    -- functions+    TVFun _ ety ->+      return $ lam $ \ x -> loop' ety (fromVFun l x) (fromVFun r x)++    -- tuples+    TVTuple tys ->+      do ls <- mapM (sDelay sym Nothing) (fromVTuple l)+         rs <- mapM (sDelay sym Nothing) (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)))+              fs++    TVAbstract {} ->+      evalPanic "ringBinary" ["Abstract type not in `Ring`"]++type UnaryWord sym = Integer -> SWord sym -> SEval sym (SWord sym)+++{-# SPECIALIZE ringUnary ::+  Concrete ->+  UnaryWord Concrete ->+  (SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->+  (Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->+  (SRational Concrete -> SEval Concrete (SRational Concrete)) ->+  (SFloat Concrete -> SEval Concrete (SFloat Concrete)) ->+  Unary Concrete+  #-}+ringUnary :: forall sym.+  Backend sym =>+  sym ->+  UnaryWord sym ->+  (SInteger sym -> SEval sym (SInteger sym)) ->+  (Integer -> SInteger sym -> SEval sym (SInteger sym)) ->+  (SRational sym -> SEval sym (SRational sym)) ->+  (SFloat sym -> SEval sym (SFloat sym)) ->+  Unary sym+ringUnary sym opw opi opz opq opfp = loop+  where+  loop' :: TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)+  loop' ty v = loop ty =<< v++  loop :: TValue -> GenValue sym -> SEval sym (GenValue sym)+  loop ty v = case ty of++    TVBit ->+      evalPanic "ringUnary" ["Bit not in class Ring"]++    TVInteger ->+      VInteger <$> opi (fromVInteger v)++    TVIntMod n ->+      VInteger <$> opz n (fromVInteger v)++    TVFloat {} ->+      VFloat <$> opfp (fromVFloat v)++    TVRational ->+      VRational <$> opq (fromVRational v)++    TVArray{} ->+      evalPanic "arithUnary" ["Array not in class Ring"]++    TVSeq w a+      -- 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)++    TVStream a ->+      VStream <$> (mapSeqMap (loop a) =<< fromSeq "ringUnary" v)++    -- functions+    TVFun _ ety ->+      return $ lam $ \ y -> loop' ety (fromVFun v y)++    -- tuples+    TVTuple tys ->+      do as <- mapM (sDelay sym Nothing) (fromVTuple v)+         return $ VTuple (zipWith loop' tys as)++    -- records+    TVRec fs ->+      VRecord <$>+        traverseRecordMap+          (\f fty -> sDelay sym Nothing (loop' fty (lookupRecord f v)))+          fs++    TVAbstract {} -> evalPanic "ringUnary" ["Abstract type not in `Ring`"]++{-# SPECIALIZE ringNullary ::+  Concrete ->+  (Integer -> SEval Concrete (SWord Concrete)) ->+  SEval Concrete (SInteger Concrete) ->+  (Integer -> SEval Concrete (SInteger Concrete)) ->+  SEval Concrete (SRational Concrete) ->+  (Integer -> Integer -> SEval Concrete (SFloat Concrete)) ->+  TValue ->+  SEval Concrete (GenValue Concrete)+  #-}++ringNullary :: forall sym.+  Backend sym =>+  sym ->+  (Integer -> SEval sym (SWord sym)) ->+  SEval sym (SInteger sym) ->+  (Integer -> SEval sym (SInteger sym)) ->+  SEval sym (SRational sym) ->+  (Integer -> Integer -> SEval sym (SFloat sym)) ->+  TValue ->+  SEval sym (GenValue sym)+ringNullary sym opw opi opz opq opfp = loop+  where+    loop :: TValue -> SEval sym (GenValue sym)+    loop ty =+      case ty of+        TVBit -> evalPanic "ringNullary" ["Bit not in class Ring"]++        TVInteger -> VInteger <$> opi++        TVIntMod n -> VInteger <$> opz n++        TVFloat e p -> VFloat <$> opfp e p++        TVRational -> VRational <$> opq++        TVArray{} -> evalPanic "arithNullary" ["Array not in class Ring"]++        TVSeq w a+          -- words and finite sequences+          | isTBit a -> pure $ VWord w $ (WordVal <$> opw w)+          | otherwise ->+             do v <- sDelay sym Nothing (loop a)+                pure $ VSeq w $ IndexSeqMap $ const v++        TVStream a ->+             do v <- sDelay sym Nothing (loop a)+                pure $ VStream $ IndexSeqMap $ const v++        TVFun _ b ->+             do v <- sDelay sym Nothing (loop b)+                pure $ lam $ const $ v++        TVTuple tys ->+             do xs <- mapM (sDelay sym Nothing . loop) tys+                pure $ VTuple xs++        TVRec fs ->+             do xs <- traverse (sDelay sym Nothing . loop) fs+                pure $ VRecord xs++        TVAbstract {} ->+          evalPanic "ringNullary" ["Abstract type not in `Ring`"]++{-# SPECIALIZE integralBinary :: Concrete -> BinWord Concrete ->+      (SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->+      Binary Concrete+  #-}++integralBinary :: forall sym.+  Backend sym =>+  sym ->+  BinWord sym ->+  (SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->+  Binary sym+integralBinary sym opw opi ty l r = case ty of+    TVInteger ->+      VInteger <$> opi (fromVInteger l) (fromVInteger r)++    -- bitvectors+    TVSeq w a+      | isTBit a ->+          do wl <- fromVWord sym "integralBinary left" l+             wr <- fromVWord sym "integralBinary right" r+             return $ VWord w (WordVal <$> opw w wl wr)++    _ -> evalPanic "integralBinary" [show ty ++ " not int class `Integral`"]+++---------------------------------------------------------------------------+-- Ring++{-# SPECIALIZE fromIntegerV :: Concrete -> GenValue Concrete+  #-}+-- | Convert an unbounded integer to a value in Ring+fromIntegerV :: Backend sym => sym -> GenValue sym+fromIntegerV sym =+  tlam $ \ a ->+  lam  $ \ v ->+  do i <- fromVInteger <$> v+     intV sym i a++{-# INLINE addV #-}+addV :: Backend sym => sym -> Binary sym+addV sym = ringBinary sym opw opi opz opq opfp+  where+    opw _w x y = wordPlus sym x y+    opi x y = intPlus sym x y+    opz m x y = znPlus sym m x y+    opq x y = rationalAdd sym x y+    opfp x y = fpRndMode sym >>= \r -> fpPlus sym r x y++{-# INLINE subV #-}+subV :: Backend sym => sym -> Binary sym+subV sym = ringBinary sym opw opi opz opq opfp+  where+    opw _w x y = wordMinus sym x y+    opi x y = intMinus sym x y+    opz m x y = znMinus sym m x y+    opq x y = rationalSub sym x y+    opfp x y = fpRndMode sym >>= \r -> fpMinus sym r x y++{-# INLINE negateV #-}+negateV :: Backend sym => sym -> Unary sym+negateV sym = ringUnary sym opw opi opz opq opfp+  where+    opw _w x = wordNegate sym x+    opi x = intNegate sym x+    opz m x = znNegate sym m x+    opq x = rationalNegate sym x+    opfp x = fpNeg sym x++{-# INLINE mulV #-}+mulV :: Backend sym => sym -> Binary sym+mulV sym = ringBinary sym opw opi opz opq opfp+  where+    opw _w x y = wordMult sym x y+    opi x y = intMult sym x y+    opz m x y = znMult sym m x y+    opq x y = rationalMul sym x y+    opfp x y = fpRndMode sym >>= \r -> fpMult sym r x y++--------------------------------------------------+-- Integral++{-# INLINE divV #-}+divV :: Backend sym => sym -> Binary sym+divV sym = integralBinary sym opw opi+  where+    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+expV sym =+  tlam $ \aty ->+  tlam $ \ety ->+   lam $ \am -> return $+   lam $ \em ->+     do a <- am+        e <- em+        case ety of+          TVInteger ->+            let ei = fromVInteger e in+            case integerAsLit sym ei of+              Just n+                | n == 0 ->+                   do onei <- integerLit sym 1+                      intV sym onei aty++                | n > 0 ->+                    do ebits <- enumerateIntBits' sym n ei+                       computeExponent sym aty a ebits++                | otherwise -> raiseError sym NegativeExponent++              Nothing -> liftIO (X.throw (UnsupportedSymbolicOp "integer exponentiation"))++          TVSeq _w el | isTBit el ->+            do ebits <- enumerateWordValue sym =<< fromWordVal "(^^)" e+               computeExponent sym aty a ebits++          _ -> evalPanic "expV" [show ety ++ " not int class `Integral`"]+++{-# SPECIALIZE computeExponent ::+      Concrete -> TValue -> GenValue Concrete -> [SBit Concrete] -> SEval Concrete (GenValue Concrete)+  #-}+computeExponent :: Backend sym =>+  sym -> TValue -> GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)+computeExponent sym aty a bs0 =+  do onei <- integerLit sym 1+     one <- intV sym onei aty+     loop one (dropLeadingZeros bs0)++ where+ dropLeadingZeros [] = []+ dropLeadingZeros (b:bs)+   | Just False <- bitAsLit sym b = dropLeadingZeros bs+   | otherwise = (b:bs)++ loop acc [] = return acc+ loop acc (b:bs) =+   do sq <- mulV sym aty acc acc+      acc' <- iteValue sym b+                (mulV sym aty a sq)+                (pure sq)+      loop acc' bs++{-# INLINE modV #-}+modV :: Backend sym => sym -> Binary sym+modV sym = integralBinary sym opw opi+  where+    opw _w x y = wordMod sym x y+    opi x y = intMod sym x y++{-# SPECIALIZE toIntegerV :: Concrete -> GenValue Concrete #-}+-- | Convert a word to a non-negative integer.+toIntegerV :: Backend sym => sym -> GenValue sym+toIntegerV sym =+  tlam $ \a ->+  lam $ \v ->+    case a of+      TVSeq _w el | isTBit el ->+        VInteger <$> (wordToInt sym =<< (fromVWord sym "toInteger" =<< v))+      TVInteger -> v+      _ -> evalPanic "toInteger" [show a ++ " not in class `Integral`"]++-----------------------------------------------------------------------------+-- Field++{-# SPECIALIZE recipV :: Concrete -> GenValue Concrete #-}+recipV :: Backend sym => sym -> GenValue sym+recipV sym =+  tlam $ \a ->+  lam $ \x ->+    case a of+      TVRational -> VRational <$> (rationalRecip sym . fromVRational =<< x)+      TVFloat e p ->+        do one <- fpLit sym e p 1+           r   <- fpRndMode sym+           xv  <- fromVFloat <$> x+           VFloat <$> fpDiv sym r one xv++      _ -> evalPanic "recip"  [show a ++ "is not a Field"]++{-# SPECIALIZE fieldDivideV :: Concrete -> GenValue Concrete #-}+fieldDivideV :: Backend sym => sym -> GenValue sym+fieldDivideV sym =+  tlam $ \a ->+  lam $ \x -> return $+  lam $ \y ->+    case a of+      TVRational ->+        do x' <- fromVRational <$> x+           y' <- fromVRational <$> y+           VRational <$> rationalDivide sym x' y'+      TVFloat _e _p ->+        do xv <- fromVFloat <$> x+           yv <- fromVFloat <$> y+           r  <- fpRndMode sym+           VFloat <$> fpDiv sym r xv yv+      _ -> evalPanic "recip"  [show a ++ "is not a Field"]++--------------------------------------------------------------+-- Round++{-# SPECIALIZE roundOp ::+  Concrete ->+  String ->+  (SRational Concrete -> SEval Concrete (SInteger Concrete)) ->+  (SFloat Concrete -> SEval Concrete (SInteger Concrete)) ->+  Unary Concrete #-}++roundOp ::+  Backend sym =>+  sym ->+  String ->+  (SRational sym -> SEval sym (SInteger sym)) ->+  (SFloat sym -> SEval sym (SInteger sym)) ->+  Unary sym+roundOp _sym nm qop opfp ty v =+  case ty of+    TVRational  -> VInteger <$> (qop (fromVRational v))+    TVFloat _ _ -> VInteger <$> opfp (fromVFloat v)+    _ -> evalPanic nm [show ty ++ " is not a Field"]++{-# INLINE floorV #-}+floorV :: Backend sym => sym -> Unary sym+floorV sym = roundOp sym "floor" opq opfp+  where+  opq = rationalFloor sym+  opfp = \x -> fpRndRTN sym >>= \r -> fpToInteger sym "floor" r x++{-# INLINE ceilingV #-}+ceilingV :: Backend sym => sym -> Unary sym+ceilingV sym = roundOp sym "ceiling" opq opfp+  where+  opq = rationalCeiling sym+  opfp = \x -> fpRndRTP sym >>= \r -> fpToInteger sym "ceiling" r x++{-# INLINE truncV #-}+truncV :: Backend sym => sym -> Unary sym+truncV sym = roundOp sym "trunc" opq opfp+  where+  opq = rationalTrunc sym+  opfp = \x -> fpRndRTZ sym >>= \r -> fpToInteger sym "trunc" r x++{-# INLINE roundAwayV #-}+roundAwayV :: Backend sym => sym -> Unary sym+roundAwayV sym = roundOp sym "roundAway" opq opfp+  where+  opq = rationalRoundAway sym+  opfp = \x -> fpRndRNA sym >>= \r -> fpToInteger sym "roundAway" r x++{-# INLINE roundToEvenV #-}+roundToEvenV :: Backend sym => sym -> Unary sym+roundToEvenV sym = roundOp sym "roundToEven" opq opfp+  where+  opq = rationalRoundToEven sym+  opfp = \x -> fpRndRNE sym >>= \r -> fpToInteger sym "roundToEven" r x++--------------------------------------------------------------+-- Logic++{-# INLINE andV #-}+andV :: Backend sym => sym -> Binary sym+andV sym = logicBinary sym (bitAnd sym) (wordAnd sym)++{-# INLINE orV #-}+orV :: Backend sym => sym -> Binary sym+orV sym = logicBinary sym (bitOr sym) (wordOr sym)++{-# INLINE xorV #-}+xorV :: Backend sym => sym -> Binary sym+xorV sym = logicBinary sym (bitXor sym) (wordXor sym)++{-# INLINE complementV #-}+complementV :: Backend sym => sym -> Unary sym+complementV sym = logicUnary sym (bitComplement sym) (wordComplement sym)++-- Bitvector signed div and modulus++{-# INLINE lg2V #-}+lg2V :: Backend sym => sym -> GenValue sym+lg2V sym =+  nlam $ \(finNat' -> w) ->+  wlam sym $ \x -> return $+  VWord w (WordVal <$> wordLg2 sym x)++{-# SPECIALIZE sdivV :: Concrete -> GenValue Concrete #-}+sdivV :: Backend sym => sym -> GenValue sym+sdivV sym =+  nlam $ \(finNat' -> w) ->+  wlam sym $ \x -> return $+  wlam sym $ \y -> return $+  VWord w (WordVal <$> wordSignedDiv sym x y)++{-# SPECIALIZE smodV :: Concrete -> GenValue Concrete #-}+smodV :: Backend sym => sym -> GenValue sym+smodV sym  =+  nlam $ \(finNat' -> w) ->+  wlam sym $ \x -> return $+  wlam sym $ \y -> return $+  VWord w (WordVal <$> wordSignedMod sym x y)++-- Cmp -------------------------------------------------------------------------++{-# SPECIALIZE cmpValue ::+  Concrete ->+  (SBit Concrete -> SBit Concrete -> SEval Concrete a -> SEval Concrete a) ->+  (SWord Concrete -> SWord Concrete -> SEval Concrete a -> SEval Concrete a) ->+  (SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) ->+  (Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) ->+  (SRational Concrete -> SRational Concrete -> SEval Concrete a -> SEval Concrete a) ->+  (SFloat Concrete -> SFloat Concrete -> SEval Concrete a -> SEval Concrete a) ->+  (TValue -> GenValue Concrete -> GenValue Concrete -> SEval Concrete a -> SEval Concrete a)+  #-}++cmpValue ::+  Backend sym =>+  sym ->+  (SBit sym -> SBit sym -> SEval sym a -> SEval sym a) ->+  (SWord sym -> SWord sym -> SEval sym a -> SEval sym a) ->+  (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) ->+  (Integer -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) ->+  (SRational sym -> SRational sym -> SEval sym a -> SEval sym a) ->+  (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a) ->+  (TValue -> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a)+cmpValue sym fb fw fi fz fq ff = cmp+  where+    cmp ty v1 v2 k =+      case ty of+        TVBit         -> fb (fromVBit v1) (fromVBit v2) k+        TVInteger     -> fi (fromVInteger v1) (fromVInteger v2) k+        TVFloat _ _   -> ff (fromVFloat v1) (fromVFloat v2) k+        TVIntMod n    -> fz n (fromVInteger v1) (fromVInteger v2) k+        TVRational    -> fq (fromVRational v1) (fromVRational v2) k+        TVArray{}     -> panic "Cryptol.Prims.Value.cmpValue"+                               [ "Arrays are not comparable" ]+        TVSeq n t+          | isTBit t  -> do w1 <- fromVWord sym "cmpValue" v1+                            w2 <- fromVWord sym "cmpValue" v2+                            fw w1 w2 k+          | otherwise -> cmpValues (repeat t)+                           (enumerateSeqMap n (fromVSeq v1))+                           (enumerateSeqMap n (fromVSeq v2))+                           k+        TVStream _    -> panic "Cryptol.Prims.Value.cmpValue"+                                [ "Infinite streams are not comparable" ]+        TVFun _ _     -> panic "Cryptol.Prims.Value.cmpValue"+                               [ "Functions are not comparable" ]+        TVTuple tys   -> cmpValues tys (fromVTuple v1) (fromVTuple v2) k+        TVRec fields  -> cmpValues+                            (recordElements fields)+                            (recordElements (fromVRecord v1))+                            (recordElements (fromVRecord v2))+                            k+        TVAbstract {} -> evalPanic "cmpValue"+                          [ "Abstract type not in `Cmp`" ]++    cmpValues (t : ts) (x1 : xs1) (x2 : xs2) k =+      do x1' <- x1+         x2' <- x2+         cmp t x1' x2' (cmpValues ts xs1 xs2 k)+    cmpValues _ _ _ k = k+++{-# INLINE bitLessThan #-}+bitLessThan :: Backend sym => sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)+bitLessThan sym x y =+  do xnot <- bitComplement sym x+     bitAnd sym xnot y++{-# INLINE bitGreaterThan #-}+bitGreaterThan :: Backend sym => sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)+bitGreaterThan sym x y = bitLessThan sym y x++{-# INLINE valEq #-}+valEq :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)+valEq sym ty v1 v2 = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure $ bitLit sym True)+  where+  fb x y k   = eqCombine sym (bitEq  sym x y) k+  fw x y k   = eqCombine sym (wordEq sym x y) k+  fi x y k   = eqCombine sym (intEq  sym x y) k+  fz m x y k = eqCombine sym (znEq sym m x y) k+  fq x y k   = eqCombine sym (rationalEq sym x y) k+  ff x y k   = eqCombine sym (fpEq sym x y) k++{-# INLINE valLt #-}+valLt :: Backend sym =>+  sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)+valLt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure final)+  where+  fb x y k   = lexCombine sym (bitLessThan  sym x y) (bitEq  sym x y) k+  fw x y k   = lexCombine sym (wordLessThan sym x y) (wordEq sym x y) k+  fi x y k   = lexCombine sym (intLessThan  sym x y) (intEq  sym x y) k+  fz _ _ _ _ = panic "valLt" ["Z_n is not in `Cmp`"]+  fq x y k   = lexCombine sym (rationalLessThan sym x y) (rationalEq sym x y) k+  ff x y k   = lexCombine sym (fpLessThan   sym x y) (fpEq   sym x y) k++{-# INLINE valGt #-}+valGt :: Backend sym =>+  sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)+valGt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure final)+  where+  fb x y k   = lexCombine sym (bitGreaterThan  sym x y) (bitEq  sym x y) k+  fw x y k   = lexCombine sym (wordGreaterThan sym x y) (wordEq sym x y) k+  fi x y k   = lexCombine sym (intGreaterThan  sym x y) (intEq  sym x y) k+  fz _ _ _ _ = panic "valGt" ["Z_n is not in `Cmp`"]+  fq x y k   = lexCombine sym (rationalGreaterThan sym x y) (rationalEq sym x y) k+  ff x y k   = lexCombine sym (fpGreaterThan   sym x y) (fpEq   sym x y) k++{-# INLINE eqCombine #-}+eqCombine :: Backend sym =>+  sym ->+  SEval sym (SBit sym) ->+  SEval sym (SBit sym) ->+  SEval sym (SBit sym)+eqCombine sym eq k = join (bitAnd sym <$> eq <*> k)++{-# INLINE lexCombine #-}+lexCombine :: Backend sym =>+  sym ->+  SEval sym (SBit sym) ->+  SEval sym (SBit sym) ->+  SEval sym (SBit sym) ->+  SEval sym (SBit sym)+lexCombine sym cmp eq k =+  do c <- cmp+     e <- eq+     bitOr sym c =<< bitAnd sym e =<< k++{-# INLINE eqV #-}+eqV :: Backend sym => sym -> Binary sym+eqV sym ty v1 v2 = VBit <$> valEq sym ty v1 v2++{-# INLINE distinctV #-}+distinctV :: Backend sym => sym -> Binary sym+distinctV sym ty v1 v2 = VBit <$> (bitComplement sym =<< valEq sym ty v1 v2)++{-# INLINE lessThanV #-}+lessThanV :: Backend sym => sym -> Binary sym+lessThanV sym ty v1 v2 = VBit <$> valLt sym ty v1 v2 (bitLit sym False)++{-# INLINE lessThanEqV #-}+lessThanEqV :: Backend sym => sym -> Binary sym+lessThanEqV sym ty v1 v2 = VBit <$> valLt sym ty v1 v2 (bitLit sym True)++{-# INLINE greaterThanV #-}+greaterThanV :: Backend sym => sym -> Binary sym+greaterThanV sym ty v1 v2 = VBit <$> valGt sym ty v1 v2 (bitLit sym False)++{-# INLINE greaterThanEqV #-}+greaterThanEqV :: Backend sym => sym -> Binary sym+greaterThanEqV sym ty v1 v2 = VBit <$> valGt sym ty v1 v2 (bitLit sym True)++{-# INLINE signedLessThanV #-}+signedLessThanV :: Backend sym => sym -> Binary sym+signedLessThanV sym ty v1 v2 = VBit <$> cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure $ bitLit sym False)+  where+  fb _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on bit type"]+  fw x y k   = lexCombine sym (wordSignedLessThan sym x y) (wordEq sym x y) k+  fi _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on Integer type"]+  fz m _ _ _ = panic "signedLessThan" ["Attempted to perform signed comparison on Z_" ++ show m ++ " type"]+  fq _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on Rational type"]+  ff _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on Float"]++++{-# SPECIALIZE zeroV ::+  Concrete ->+  TValue ->+  SEval Concrete (GenValue Concrete)+  #-}+zeroV :: forall sym.+  Backend sym =>+  sym ->+  TValue ->+  SEval sym (GenValue sym)+zeroV sym ty = case ty of++  -- bits+  TVBit ->+    pure (VBit (bitLit sym False))++  -- integers+  TVInteger ->+    VInteger <$> integerLit sym 0++  -- integers mod n+  TVIntMod _ ->+    VInteger <$> integerLit sym 0++  TVRational ->+    VRational <$> (intToRational sym =<< integerLit sym 0)++  TVArray{} -> evalPanic "zeroV" ["Array not in class Zero"]++  -- floating point+  TVFloat e p ->+    VFloat <$> fpLit sym e p 0++  -- sequences+  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)++  TVStream ety ->+     do z <- sDelay sym Nothing (zeroV sym ety)+        pure $ VStream (IndexSeqMap $ const z)++  -- functions+  TVFun _ bty ->+     do z <- sDelay sym Nothing (zeroV sym bty)+        pure $ lam (const z)++  -- tuples+  TVTuple tys ->+      do xs <- mapM (sDelay sym Nothing . zeroV sym) tys+         pure $ VTuple xs++  -- records+  TVRec fields ->+      do xs <- traverse (sDelay sym Nothing . zeroV sym) fields+         pure $ VRecord xs++  TVAbstract {} -> evalPanic "zeroV" [ "Abstract type not in `Zero`" ]++--  | otherwise = evalPanic "zeroV" ["invalid type for zero"]++{-# INLINE joinWordVal #-}+joinWordVal :: Backend sym => sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)+joinWordVal sym (WordVal w1) (WordVal w2)+  | wordLen sym w1 + wordLen sym w2 < largeBitSize+  = WordVal <$> joinWord sym w1 w2+joinWordVal sym w1 w2+  = pure $ LargeBitsVal (n1+n2) (concatSeqMap n1 (asBitsMap sym w1) (asBitsMap sym w2))+ where n1 = wordValueSize sym w1+       n2 = wordValueSize sym w2+++{-# SPECIALIZE joinWords ::+  Concrete ->+  Integer ->+  Integer ->+  SeqMap Concrete ->+  SEval Concrete (GenValue Concrete)+  #-}+joinWords :: forall sym.+  Backend sym =>+  sym ->+  Integer ->+  Integer ->+  SeqMap sym ->+  SEval sym (GenValue sym)+joinWords sym nParts nEach xs =+  loop (WordVal <$> wordLit sym 0 0) (enumerateSeqMap nParts xs)++ where+ loop :: SEval sym (WordValue sym) -> [SEval sym (GenValue sym)] -> SEval sym (GenValue sym)+ loop !wv [] =+    VWord (nParts * nEach) <$> sDelay sym Nothing wv+ loop !wv (w : ws) =+    w >>= \case+      VWord _ w' ->+        loop (join (joinWordVal sym <$> wv <*> w')) ws+      _ -> evalPanic "joinWords: expected word value" []++{-# SPECIALIZE joinSeq ::+  Concrete ->+  Nat' ->+  Integer ->+  TValue ->+  SeqMap Concrete ->+  SEval Concrete (GenValue Concrete)+  #-}+joinSeq ::+  Backend sym =>+  sym ->+  Nat' ->+  Integer ->+  TValue ->+  SeqMap sym ->+  SEval sym (GenValue sym)++-- Special case for 0 length inner sequences.+joinSeq sym _parts 0 a _xs+  = zeroV sym (TVSeq 0 a)++-- finite sequence of words+joinSeq sym (Nat parts) each TVBit xs+  | parts * each < largeBitSize+  = joinWords sym parts each xs+  | otherwise+  = do let zs = IndexSeqMap $ \i ->+                  do let (q,r) = divMod i each+                     ys <- fromWordVal "join seq" =<< lookupSeqMap xs q+                     VBit <$> indexWordValue sym ys r+       return $ VWord (parts * each) $ pure $ LargeBitsVal (parts * each) zs++-- infinite sequence of words+joinSeq sym Inf each TVBit xs+  = return $ VStream $ IndexSeqMap $ \i ->+      do let (q,r) = divMod i each+         ys <- fromWordVal "join seq" =<< lookupSeqMap xs q+         VBit <$> indexWordValue sym ys r++-- finite or infinite sequence of non-words+joinSeq _sym parts each _a xs+  = return $ vSeq $ IndexSeqMap $ \i -> do+      let (q,r) = divMod i each+      ys <- fromSeq "join seq" =<< lookupSeqMap xs q+      lookupSeqMap ys r+  where+  len = parts `nMul` (Nat each)+  vSeq = case len of+           Inf    -> VStream+           Nat n  -> VSeq n+++{-# INLINE joinV #-}++-- | Join a sequence of sequences into a single sequence.+joinV ::+  Backend sym =>+  sym ->+  Nat' ->+  Integer ->+  TValue ->+  GenValue sym ->+  SEval sym (GenValue sym)+joinV sym parts each a val = joinSeq sym parts each a =<< fromSeq "joinV" val+++{-# INLINE splitWordVal #-}++splitWordVal ::+  Backend sym =>+  sym ->+  Integer ->+  Integer ->+  WordValue sym ->+  SEval sym (WordValue sym, WordValue sym)+splitWordVal sym leftWidth rightWidth (WordVal w) =+  do (lw, rw) <- splitWord sym leftWidth rightWidth w+     pure (WordVal lw, WordVal rw)+splitWordVal _ leftWidth rightWidth (LargeBitsVal _n xs) =+  let (lxs, rxs) = splitSeqMap leftWidth xs+   in pure (LargeBitsVal leftWidth lxs, LargeBitsVal rightWidth rxs)++{-# INLINE splitAtV #-}+splitAtV ::+  Backend sym =>+  sym ->+  Nat' ->+  Nat' ->+  TValue ->+  GenValue sym ->+  SEval sym (GenValue sym)+splitAtV sym front back a val =+  case back of++    Nat rightWidth | aBit -> do+          ws <- sDelay sym Nothing (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)+       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)+       return $ VTuple [ VSeq leftWidth <$> ls+                       , mkSeq back a <$> rs+                       ]++  where+  aBit = isTBit a++  leftWidth = case front of+    Nat n -> n+    _     -> evalPanic "splitAtV" ["invalid `front` len"]+++{-# INLINE extractWordVal #-}++-- | Extract a subsequence of bits from a @WordValue@.+--   The first integer argument is the number of bits in the+--   resulting word.  The second integer argument is the+--   number of less-significant digits to discard.  Stated another+--   way, the operation `extractWordVal n i w` is equivalent to+--   first shifting `w` right by `i` bits, and then truncating to+--   `n` bits.+extractWordVal ::+  Backend sym =>+  sym ->+  Integer ->+  Integer ->+  WordValue sym ->+  SEval sym (WordValue sym)+extractWordVal sym len start (WordVal w) =+   WordVal <$> extractWord sym len start w+extractWordVal _ len start (LargeBitsVal n xs) =+   let xs' = dropSeqMap (n - start - len) xs+    in pure $ LargeBitsVal len xs'++{-# INLINE ecSplitV #-}++-- | Split implementation.+ecSplitV :: Backend sym => sym -> GenValue sym+ecSplitV sym =+  nlam $ \ parts ->+  nlam $ \ each  ->+  tlam $ \ a     ->+  lam  $ \ val ->+    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)+          return $ VStream $ IndexSeqMap $ \i ->+            return $ VWord e $ return $ LargeBitsVal e $ IndexSeqMap $ \j ->+              let idx = i*e + toInteger j+               in idx `seq` do+                      xs <- val'+                      lookupSeqMap xs idx+       (Nat p, Nat e) -> do+          val' <- sDelay sym Nothing (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)+          return $ VStream $ IndexSeqMap $ \i ->+            return $ VSeq e $ IndexSeqMap $ \j -> do+              xs <- val'+              lookupSeqMap xs (e * i + j)+       _              -> evalPanic "splitV" ["invalid type arguments to split"]++{-# INLINE reverseV #-}++reverseV :: forall sym.+  Backend sym =>+  sym ->+  GenValue sym ->+  SEval sym (GenValue sym)+reverseV _ (VSeq n xs) =+  return $ VSeq n $ reverseSeqMap n xs+reverseV sym (VWord n x) = return (VWord n (revword <$> x))+ where+ revword wv =+   let m = wordValueSize sym wv in+   LargeBitsVal m $ reverseSeqMap m $ asBitsMap sym wv+reverseV _ _ =+  evalPanic "reverseV" ["Not a finite sequence"]++{-# INLINE transposeV #-}++transposeV ::+  Backend sym =>+  sym ->+  Nat' ->+  Nat' ->+  TValue ->+  GenValue sym ->+  SEval sym (GenValue sym)+transposeV sym a b c xs+  | isTBit c, Nat na <- a = -- Fin a => [a][b]Bit -> [b][a]Bit+      return $ bseq $ IndexSeqMap $ \bi ->+        return $ VWord na $ return $ LargeBitsVal na $ IndexSeqMap $ \ai ->+         do ys <- flip lookupSeqMap (toInteger ai) =<< fromSeq "transposeV" xs+            case ys of+              VStream ys' -> lookupSeqMap ys' bi+              VWord _ wv  -> VBit <$> (flip (indexWordValue sym) bi =<< wv)+              _ -> evalPanic "transpose" ["expected sequence of bits"]++  | 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+            case ys of+              VStream ys' -> lookupSeqMap ys' bi+              VWord _ wv  -> VBit <$> (flip (indexWordValue sym) bi =<< wv)+              _ -> evalPanic "transpose" ["expected sequence of bits"]++  | 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+          return z++ where+  bseq =+        case b of+          Nat nb -> VSeq nb+          Inf    -> VStream+  aseq =+        case a of+          Nat na -> VSeq na+          Inf    -> VStream+++{-# INLINE ccatV #-}++ccatV ::+  Backend sym =>+  sym ->+  Nat' ->+  Nat' ->+  TValue ->+  (GenValue sym) ->+  (GenValue sym) ->+  SEval sym (GenValue sym)++ccatV sym _front _back _elty (VWord m l) (VWord n r) =+  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+  return $ VStream $ IndexSeqMap $ \i ->+    if i < m then+      VBit <$> (flip (indexWordValue sym) i =<< l')+    else+      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)+       let Nat n = front+       mkSeq (evalTF TCAdd [front,back]) elty <$> return (IndexSeqMap $ \i ->+        if i < n then do+         ls <- l''+         lookupSeqMap ls i+        else do+         rs <- r''+         lookupSeqMap rs (i-n))++{-# INLINE wordValLogicOp #-}++wordValLogicOp ::+  Backend sym =>+  sym ->+  (SBit sym -> SBit sym -> SEval sym (SBit sym)) ->+  (SWord sym -> SWord sym -> SEval sym (SWord sym)) ->+  WordValue sym ->+  WordValue sym ->+  SEval sym (WordValue sym)+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))+           xs = asBitsMap sym w1+           ys = asBitsMap sym w2+           op x y = VBit <$> (bop (fromVBit x) (fromVBit y))++{-# SPECIALIZE logicBinary ::+  Concrete ->+  (SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)) ->+  (SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)) ->+  Binary Concrete+  #-}++-- | Merge two values given a binop.  This is used for and, or and xor.+logicBinary :: forall sym.+  Backend sym =>+  sym ->+  (SBit sym -> SBit sym -> SEval sym (SBit sym)) ->+  (SWord sym -> SWord sym -> SEval sym (SWord sym)) ->+  Binary sym+logicBinary sym opb opw = loop+  where+  loop' :: TValue+        -> SEval sym (GenValue sym)+        -> SEval sym (GenValue sym)+        -> SEval sym (GenValue sym)+  loop' ty l r = join (loop ty <$> l <*> r)++  loop :: TValue+        -> GenValue sym+        -> GenValue sym+        -> SEval sym (GenValue sym)++  loop ty l r = case ty of+    TVBit -> VBit <$> (opb (fromVBit l) (fromVBit r))+    TVInteger -> evalPanic "logicBinary" ["Integer not in class Logic"]+    TVIntMod _ -> evalPanic "logicBinary" ["Z not in class Logic"]+    TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]+    TVArray{} -> evalPanic "logicBinary" ["Array not in class Logic"]++    TVFloat {}  -> evalPanic "logicBinary" ["Float not in class Logic"]+    TVSeq w aty+         -- words+         | isTBit aty+              -> do v <- sDelay sym Nothing $ join+                            (wordValLogicOp sym opb opw <$>+                                    fromWordVal "logicBinary l" l <*>+                                    fromWordVal "logicBinary r" r)+                    return $ VWord w v++         -- finite sequences+         | otherwise -> VSeq w <$>+                           (join (zipSeqMap (loop aty) <$>+                                    (fromSeq "logicBinary left" l)+                                    <*> (fromSeq "logicBinary right" r)))++    TVStream aty ->+        VStream <$> (join (zipSeqMap (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)+        return $ VTuple $ zipWith3 loop' etys ls rs++    TVFun _ bty ->+        return $ lam $ \ a -> loop' bty (fromVFun l a) (fromVFun r a)++    TVRec fields ->+      VRecord <$>+        traverseRecordMap+          (\f fty -> sDelay sym Nothing (loop' fty (lookupRecord f l) (lookupRecord f r)))+          fields++    TVAbstract {} -> evalPanic "logicBinary"+                        [ "Abstract type not in `Logic`" ]++{-# INLINE wordValUnaryOp #-}+wordValUnaryOp ::+  Backend 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+  where f x = VBit <$> (bop (fromVBit x))++{-# SPECIALIZE logicUnary ::+  Concrete ->+  (SBit Concrete -> SEval Concrete (SBit Concrete)) ->+  (SWord Concrete -> SEval Concrete (SWord Concrete)) ->+  Unary Concrete+  #-}++logicUnary :: forall sym.+  Backend sym =>+  sym ->+  (SBit sym -> SEval sym (SBit sym)) ->+  (SWord sym -> SEval sym (SWord sym)) ->+  Unary sym+logicUnary sym opb opw = loop+  where+  loop' :: TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)+  loop' ty val = loop ty =<< val++  loop :: TValue -> GenValue sym -> SEval sym (GenValue sym)+  loop ty val = case ty of+    TVBit -> VBit <$> (opb (fromVBit val))++    TVInteger -> evalPanic "logicUnary" ["Integer not in class Logic"]+    TVIntMod _ -> evalPanic "logicUnary" ["Z not in class Logic"]+    TVFloat {} -> evalPanic "logicUnary" ["Float not in class Logic"]+    TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]+    TVArray{} -> evalPanic "logicUnary" ["Array not in class Logic"]++    TVSeq w ety+         -- words+         | isTBit ety+              -> do v <- sDelay sym Nothing (wordValUnaryOp opb opw =<< fromWordVal "logicUnary" val)+                    return $ VWord w v++         -- finite sequences+         | otherwise+              -> VSeq w <$> (mapSeqMap (loop ety) =<< fromSeq "logicUnary" val)++         -- streams+    TVStream ety ->+         VStream <$> (mapSeqMap (loop ety) =<< fromSeq "logicUnary" val)++    TVTuple etys ->+      do as <- mapM (sDelay sym Nothing) (fromVTuple val)+         return $ VTuple (zipWith loop' etys as)++    TVFun _ bty ->+      return $ lam $ \ a -> loop' bty (fromVFun val a)++    TVRec fields ->+      VRecord <$>+        traverseRecordMap+          (\f fty -> sDelay sym Nothing (loop' fty (lookupRecord f val)))+          fields++    TVAbstract {} -> evalPanic "logicUnary" [ "Abstract type not in `Logic`" ]+++{-# SPECIALIZE bitsValueLessThan ::+  Concrete ->+  Integer ->+  [SBit Concrete] ->+  Integer ->+  SEval Concrete (SBit Concrete)+  #-}+bitsValueLessThan ::+  Backend sym =>+  sym ->+  Integer {- ^ bit-width -} ->+  [SBit sym] {- ^ big-endian list of index bits -} ->+  Integer {- ^ Upper bound to test against -} ->+  SEval sym (SBit sym)+bitsValueLessThan sym _w [] _n = pure $ bitLit sym False+bitsValueLessThan sym w (b:bs) n+  | nbit =+      do notb <- bitComplement sym b+         bitOr sym notb =<< bitsValueLessThan sym (w-1) bs n+  | otherwise =+      do notb <- bitComplement sym b+         bitAnd sym notb =<< bitsValueLessThan sym (w-1) bs n+ where+ nbit = testBit n (fromInteger (w-1))+++{-# INLINE assertIndexInBounds #-}+assertIndexInBounds ::+  Backend sym =>+  sym ->+  Nat' {- ^ Sequence size bounds -} ->+  Either (SInteger sym) (WordValue sym) {- ^ Index value -} ->+  SEval sym ()++-- Can't index out of bounds for an infinite sequence+assertIndexInBounds _sym Inf _ =+  return ()++-- Can't index out of bounds for a sequence that is+-- longer than the expressible index values+assertIndexInBounds sym (Nat n) (Right idx)+  | n >= 2^(wordValueSize sym idx)+  = return ()++-- If the index is concrete, test it directly+assertIndexInBounds sym (Nat n) (Left idx)+  | Just i <- integerAsLit sym idx+  = unless (i < n) (raiseError sym (InvalidIndex (Just i)))++-- If the index is concrete, test it directly+assertIndexInBounds sym (Nat n) (Right (WordVal idx))+  | Just (_w,i) <- wordAsLit sym idx+  = unless (i < n) (raiseError sym (InvalidIndex (Just i)))++-- If the index is an integer, test that it+-- is less than the concrete value of n.+assertIndexInBounds sym (Nat n) (Left idx) =+  do n' <- integerLit sym n+     p <- intLessThan sym idx n'+     assertSideCondition sym p (InvalidIndex Nothing)++-- If the index is a packed word, test that it+-- is less than the concrete value of n, which+-- fits into w bits because of the above test.+assertIndexInBounds sym (Nat n) (Right (WordVal idx)) =+  do n' <- wordLit sym (wordLen sym idx) n+     p <- wordLessThan sym idx n'+     assertSideCondition sym p (InvalidIndex Nothing)++-- If the index is an unpacked word, force all the bits+-- and compute the unsigned less-than test directly.+assertIndexInBounds sym (Nat n) (Right (LargeBitsVal w bits)) =+  do bitsList <- traverse (fromVBit <$>) (enumerateSeqMap w bits)+     p <- bitsValueLessThan sym w bitsList n+     assertSideCondition sym p (InvalidIndex Nothing)+++-- | Indexing operations.++{-# INLINE indexPrim #-}+indexPrim ::+  Backend sym =>+  sym ->+  (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+indexPrim sym int_op bits_op word_op =+  nlam $ \ len  ->+  tlam $ \ eltTy ->+  tlam $ \ ix ->+   lam $ \ xs  -> return $+   lam $ \ idx  -> do+      vs <- xs >>= \case+               VWord _ w  -> w >>= \w' -> return $ IndexSeqMap (\i -> VBit <$> indexWordValue sym w' i)+               VSeq _ vs  -> return vs+               VStream vs -> return vs+               _ -> evalPanic "Expected sequence value" ["indexPrim"]+      idx' <- asIndex sym "index" ix =<< idx+      assertIndexInBounds sym len idx'+      case idx' of+        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)++{-# INLINE updatePrim #-}++updatePrim ::+  Backend sym =>+  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+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"]++{-# INLINE fromToV #-}++-- @[ 0 .. 10 ]@+fromToV :: Backend sym => sym -> GenValue sym+fromToV sym =+  nlam $ \ first ->+  nlam $ \ lst   ->+  tlam $ \ ty    ->+    let !f = mkLit sym ty in+    case (first, lst) of+      (Nat first', Nat lst') ->+        let len = 1 + (lst' - first')+        in VSeq len $ IndexSeqMap $ \i -> f (first' + i)+      _ -> evalPanic "fromToV" ["invalid arguments"]++{-# INLINE fromThenToV #-}++-- @[ 0, 1 .. 10 ]@+fromThenToV :: Backend sym => sym -> GenValue sym+fromThenToV sym =+  nlam $ \ first ->+  nlam $ \ next  ->+  nlam $ \ lst   ->+  tlam $ \ ty    ->+  nlam $ \ len   ->+    let !f = mkLit sym ty in+    case (first, next, lst, len) of+      (Nat first', Nat next', Nat _lst', Nat len') ->+        let diff = next' - first'+        in VSeq len' $ IndexSeqMap $ \i -> f (first' + i*diff)+      _ -> evalPanic "fromThenToV" ["invalid arguments"]++{-# INLINE infFromV #-}+infFromV :: Backend sym => sym -> GenValue 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++{-# INLINE infFromThenV #-}+infFromThenV :: Backend sym => sym -> GenValue 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++-- Shifting ---------------------------------------------------++barrelShifter :: Backend sym =>+  sym ->+  (SeqMap sym -> Integer -> SEval sym (SeqMap sym))+     {- ^ concrete shifting operation -} ->+  SeqMap sym  {- ^ initial value -} ->+  [SBit sym]  {- ^ bits of shift amount, in big-endian order -} ->+  SEval sym (SeqMap sym)+barrelShifter sym shift_op = go+  where+  go x [] = return x++  go x (b:bs)+    | Just True <- bitAsLit sym b+    = do x_shft <- shift_op x (2 ^ length bs)+         go x_shft bs++    | Just False <- bitAsLit sym b+    = do go x bs++    | otherwise+    = do x_shft <- shift_op x (2 ^ length bs)+         x' <- memoMap (mergeSeqMap sym b x_shft x)+         go x' bs++{-# INLINE shiftLeftReindex #-}+shiftLeftReindex :: Nat' -> Integer -> Integer -> Maybe Integer+shiftLeftReindex sz i shft =+   case sz of+     Nat n | i+shft >= n -> Nothing+     _                   -> Just (i+shft)++{-# INLINE shiftRightReindex #-}+shiftRightReindex :: Nat' -> Integer -> Integer -> Maybe Integer+shiftRightReindex _sz i shft =+   if i-shft < 0 then Nothing else Just (i-shft)++{-# INLINE rotateLeftReindex #-}+rotateLeftReindex :: Nat' -> Integer -> Integer -> Maybe Integer+rotateLeftReindex sz i shft =+   case sz of+     Inf -> evalPanic "cannot rotate infinite sequence" []+     Nat n -> Just ((i+shft) `mod` n)++{-# INLINE rotateRightReindex #-}+rotateRightReindex :: Nat' -> Integer -> Integer -> Maybe Integer+rotateRightReindex sz i shft =+   case sz of+     Inf -> evalPanic "cannot rotate infinite sequence" []+     Nat n -> Just ((i+n-shft) `mod` n)++-- | Compute the list of bits in an integer in big-endian order.+--   Fails if neither the sequence length nor the type value+--   provide an upper bound for the integer.+enumerateIntBits :: Backend sym =>+  sym ->+  Nat' ->+  TValue ->+  SInteger sym ->+  SEval sym [SBit sym]+enumerateIntBits sym (Nat n) _ idx = enumerateIntBits' sym n idx+enumerateIntBits _sym Inf _ _ = liftIO (X.throw (UnsupportedSymbolicOp "unbounded integer shifting"))++-- | Compute the list of bits in an integer in big-endian order.+--   The integer argument is a concrete upper bound for+--   the symbolic integer.+enumerateIntBits' :: Backend sym =>+  sym ->+  Integer ->+  SInteger sym ->+  SEval sym [SBit sym]+enumerateIntBits' sym n idx =+  do w <- wordFromInt sym (widthInteger n) idx+     unpackWord sym w++-- | Generic implementation of shifting.+--   Uses the provided word-level operation to perform the shift, when+--   possible.  Otherwise falls back on a barrel shifter that uses+--   the provided reindexing operation to implement the concrete+--   shifting operations.  The reindex operation is given the size+--   of the sequence, the requested index value for the new output sequence,+--   and the amount to shift.  The return value is an index into the original+--   sequence if in bounds, and Nothing otherwise.+logicShift :: Backend sym =>+  sym ->+  String ->+  (sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))+     {- ^ operation for range reduction on integers -} ->+  (SWord sym -> SWord sym -> SEval sym (SWord sym))+     {- ^ word shift operation for positive indices -} ->+  (SWord sym -> SWord sym -> SEval sym (SWord sym))+     {- ^ word shift operation for negative indices -} ->+  (Nat' -> Integer -> Integer -> Maybe Integer)+     {- ^ 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+logicShift sym nm shrinkRange wopPos wopNeg reindexPos reindexNeg =+  nlam $ \m ->+  tlam $ \ix ->+  tlam $ \a ->+  VFun $ \xs -> return $+  VFun $ \y ->+    do xs' <- xs+       y' <- asIndex sym "shift" ix =<< y+       case y' of+         Left int_idx ->+           do pneg <- intLessThan sym int_idx =<< integerLit sym 0+              iteValue sym pneg+                (intShifter sym nm wopNeg reindexNeg m ix a xs' =<< shrinkRange sym m ix =<< intNegate sym int_idx)+                (intShifter sym nm wopPos reindexPos m ix a xs' =<< shrinkRange sym m ix int_idx)+         Right idx ->+           wordShifter sym nm wopPos reindexPos m a xs' idx++intShifter :: Backend sym =>+   sym ->+   String ->+   (SWord sym -> SWord sym -> SEval sym (SWord sym)) ->+   (Nat' -> Integer -> Integer -> Maybe Integer) ->+   Nat' ->+   TValue ->+   TValue ->+   GenValue sym ->+   SInteger sym ->+   SEval sym (GenValue sym)+intShifter sym nm wop reindex m ix a xs idx =+   do let shiftOp vs shft =+              memoMap $ IndexSeqMap $ \i ->+                case reindex m i shft of+                  Nothing -> zeroV sym a+                  Just i' -> lookupSeqMap vs i'+      case xs of+        VWord w x ->+           return $ VWord w $ do+             x >>= \case+               WordVal x' -> WordVal <$> (wop x' =<< wordFromInt sym w idx)+               LargeBitsVal n bs0 ->+                 do idx_bits <- enumerateIntBits sym m ix idx+                    LargeBitsVal n <$> barrelShifter sym shiftOp bs0 idx_bits++        VSeq w vs0 ->+           do idx_bits <- enumerateIntBits sym m ix idx+              VSeq w <$> barrelShifter sym shiftOp vs0 idx_bits++        VStream vs0 ->+           do idx_bits <- enumerateIntBits sym m ix idx+              VStream <$> barrelShifter sym shiftOp vs0 idx_bits++        _ -> evalPanic "expected sequence value in shift operation" [nm]+++wordShifter :: Backend sym =>+   sym ->+   String ->+   (SWord sym -> SWord sym -> SEval sym (SWord sym)) ->+   (Nat' -> Integer -> Integer -> Maybe Integer) ->+   Nat' ->+   TValue ->+   GenValue sym ->+   WordValue sym ->+   SEval sym (GenValue sym)+wordShifter sym nm wop reindex m a xs idx =+  let shiftOp vs shft =+          memoMap $ IndexSeqMap $ \i ->+            case reindex m i shft of+              Nothing -> zeroV sym a+              Just i' -> lookupSeqMap vs i'+   in case xs of+        VWord w x ->+           return $ VWord w $ do+             x >>= \case+               WordVal x' -> WordVal <$> (wop x' =<< asWordVal sym idx)+               LargeBitsVal n bs0 ->+                 do idx_bits <- enumerateWordValue sym idx+                    LargeBitsVal n <$> barrelShifter sym shiftOp bs0 idx_bits++        VSeq w vs0 ->+           do idx_bits <- enumerateWordValue sym idx+              VSeq w <$> barrelShifter sym shiftOp vs0 idx_bits++        VStream vs0 ->+           do idx_bits <- enumerateWordValue sym idx+              VStream <$> barrelShifter sym shiftOp vs0 idx_bits++        _ -> evalPanic "expected sequence value in shift operation" [nm]+++shiftShrink :: Backend sym => sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)+shiftShrink _sym Inf _ x = return x+shiftShrink sym (Nat w) _ x =+  do w' <- integerLit sym w+     p  <- intLessThan sym w' x+     iteInteger sym p w' x++rotateShrink :: Backend sym => sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)+rotateShrink _sym Inf _ _ = panic "rotateShrink" ["expected finite sequence in rotate"]+rotateShrink sym (Nat 0) _ _ = integerLit sym 0+rotateShrink sym (Nat w) _ x =+  do w' <- integerLit sym w+     intMod sym x w'++-- Miscellaneous ---------------------------------------------------------------++{-# SPECIALIZE errorV ::+  Concrete ->+  TValue ->+  String ->+  SEval Concrete (GenValue Concrete)+  #-}+errorV :: forall sym.+  Backend sym =>+  sym ->+  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++  -- 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)++  TVStream ety ->+    return $ VStream (IndexSeqMap $ \_ -> errorV sym ety msg)++  -- functions+  TVFun _ bty ->+    return $ lam (\ _ -> errorV sym bty msg)++  -- tuples+  TVTuple tys ->+    return $ VTuple (map (\t -> errorV sym t msg) tys)++  -- records+  TVRec fields ->+    return $ VRecord $ fmap (\t -> errorV sym t msg) $ fields++  TVAbstract {} -> cryUserError sym msg+++{-# INLINE valueToChar #-}++-- | Expect a word value.  Mask it to an 8-bits ASCII value+--   and return the associated character, if it is concrete.+--   Otherwise, return a '?' character+valueToChar :: Backend sym => sym -> GenValue sym -> SEval sym Char+valueToChar sym (VWord 8 wval) =+  do w <- asWordVal sym =<< wval+     pure $! fromMaybe '?' (wordAsChar sym w)+valueToChar _ _ = evalPanic "valueToChar" ["Not an 8-bit bitvector"]++{-# INLINE valueToString #-}++valueToString :: Backend sym => sym -> GenValue sym -> SEval sym String+valueToString sym (VSeq n vals) = traverse (valueToChar sym =<<) (enumerateSeqMap n vals)+valueToString _ _ = evalPanic "valueToString" ["Not a finite sequence"]++-- Merge and if/then/else++{-# INLINE iteValue #-}+iteValue :: Backend sym =>+  sym ->+  SBit sym ->+  SEval sym (GenValue sym) ->+  SEval sym (GenValue sym) ->+  SEval sym (GenValue sym)+iteValue sym b x y+  | Just True  <- bitAsLit sym b = x+  | Just False <- bitAsLit sym b = y+  | otherwise = mergeValue' sym b x y++{-# INLINE mergeWord #-}+mergeWord :: Backend sym =>+  sym ->+  SBit sym ->+  WordValue sym ->+  WordValue sym ->+  SEval sym (WordValue sym)+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))++{-# INLINE mergeWord' #-}+mergeWord' :: Backend sym =>+  sym ->+  SBit sym ->+  SEval sym (WordValue sym) ->+  SEval sym (WordValue sym) ->+  SEval sym (WordValue sym)+mergeWord' sym = mergeEval sym (mergeWord sym)++{-# INLINE mergeValue' #-}+mergeValue' :: Backend sym =>+  sym ->+  SBit sym ->+  SEval sym (GenValue sym) ->+  SEval sym (GenValue sym) ->+  SEval sym (GenValue sym)+mergeValue' sym = mergeEval sym (mergeValue sym)++mergeValue :: Backend sym =>+  sym ->+  SBit sym ->+  GenValue sym ->+  GenValue sym ->+  SEval sym (GenValue sym)+mergeValue sym c v1 v2 =+  case (v1, v2) of+    (VRecord fs1 , VRecord fs2 ) ->+      do let res = zipRecords (\_lbl -> mergeValue' sym c) fs1 fs2+         case res of+           Left f -> panic "Cryptol.Eval.Generic" [ "mergeValue: incompatible record values", show f ]+           Right r -> pure (VRecord r)+    (VTuple vs1  , VTuple vs2  ) | length vs1 == length vs2  ->+                                  pure $ VTuple $ zipWith (mergeValue' sym c) vs1 vs2+    (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+    (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)+    (_           , _           ) -> panic "Cryptol.Eval.Generic"+                                  [ "mergeValue: incompatible values" ]++{-# INLINE mergeSeqMap #-}+mergeSeqMap :: Backend sym =>+  sym ->+  SBit sym ->+  SeqMap sym ->+  SeqMap sym ->+  SeqMap sym+mergeSeqMap sym c x y =+  IndexSeqMap $ \i ->+    iteValue sym c (lookupSeqMap x i) (lookupSeqMap y i)+++--------------------------------------------------------------------------------+-- Experimental parallel primitives++parmapV :: Backend sym => sym -> GenValue sym+parmapV sym =+  tlam $ \_a ->+  tlam $ \_b ->+  ilam $ \_n ->+  lam $ \f -> pure $+  lam $ \xs ->+    do f' <- fromVFun <$> f+       xs' <- xs+       case xs' of+          VWord n w ->+            do m <- asBitsMap sym <$> w+               m' <- sparkParMap sym f' n m+               pure (VWord n (pure (LargeBitsVal n m')))+          VSeq n m ->+            VSeq n <$> sparkParMap sym f' n m++          _ -> panic "parmapV" ["expected sequence!"]+++sparkParMap ::+  Backend sym =>+  sym ->+  (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) ->+  Integer ->+  SeqMap sym ->+  SEval sym (SeqMap sym)+sparkParMap sym f n m =+  finiteSeqMap sym <$> mapM (sSpark sym . f) (enumerateSeqMap n m)++--------------------------------------------------------------------------------+-- Floating Point Operations++-- | Make a Cryptol value for a binary arithmetic function.+fpBinArithV :: Backend sym => sym -> FPArith2 sym -> GenValue sym+fpBinArithV sym fun =+  ilam \_ ->+  ilam \_ ->+  wlam sym \r ->+  pure $ flam \x ->+  pure $ flam \y ->+  VFloat <$> fun sym r x y++-- | Rounding mode used in FP operations that do not specify it explicitly.+fpRndMode, fpRndRNE, fpRndRNA, fpRndRTP, fpRndRTN, fpRndRTZ ::+   Backend sym => sym -> SEval sym (SWord sym)+fpRndMode    = fpRndRNE+fpRndRNE sym = wordLit sym 3 0 {- to nearest, ties to even -}+fpRndRNA sym = wordLit sym 3 1 {- to nearest, ties to away from 0 -}+fpRndRTP sym = wordLit sym 3 2 {- to +inf -}+fpRndRTN sym = wordLit sym 3 3 {- to -inf -}+fpRndRTZ sym = wordLit sym 3 4 {- to 0    -}