cryptol 2.9.1 → 2.10.0

raw patch · 91 files changed

+10784/−6930 lines, 91 filesdep +MemoTriedep +ghc-primdep +integer-gmpdep ~sbvPVP ok

version bump matches the API change (PVP)

Dependencies added: MemoTrie, ghc-prim, integer-gmp, stm

Dependency ranges changed: sbv

API changes (from Hackage documentation)

Files

• CHANGES.md +58/−0
• cryptol.cabal +29/−56
• lib/Cryptol.cry +72/−46
• lib/Cryptol/Reference.cry +46/−0
• lib/PrimeEC.cry +162/−0
• lib/SuiteB.cry +236/−0
• src/Cryptol/AES.hs +493/−0
• src/Cryptol/Backend.hs +714/−0
• src/Cryptol/Backend/Arch.hs +30/−0
• src/Cryptol/Backend/Concrete.hs +398/−0
• src/Cryptol/Backend/FloatHelpers.hs +248/−0
• src/Cryptol/Backend/Monad.hs +394/−0
• src/Cryptol/Backend/SBV.hs +457/−0
• src/Cryptol/Backend/What4.hs +666/−0
• src/Cryptol/Backend/What4/SFloat.hs +362/−0
• src/Cryptol/Eval.hs +30/−28
• src/Cryptol/Eval/Arch.hs +0/−30
• src/Cryptol/Eval/Backend.hs +0/−705
• src/Cryptol/Eval/Concrete.hs +338/−18
• src/Cryptol/Eval/Concrete/Float.hs +0/−69
• src/Cryptol/Eval/Concrete/FloatHelpers.hs +0/−252
• src/Cryptol/Eval/Concrete/Value.hs +0/−390
• src/Cryptol/Eval/Env.hs +17/−15
• src/Cryptol/Eval/Generic.hs +94/−7
• src/Cryptol/Eval/Monad.hs +0/−272
• src/Cryptol/Eval/Reference.lhs +1689/−1644
• src/Cryptol/Eval/SBV.hs +87/−449
• src/Cryptol/Eval/Type.hs +10/−11
• src/Cryptol/Eval/Value.hs +9/−11
• src/Cryptol/Eval/What4.hs +863/−24
• src/Cryptol/Eval/What4/Float.hs +0/−68
• src/Cryptol/Eval/What4/SFloat.hs +0/−361
• src/Cryptol/Eval/What4/Value.hs +0/−975
• src/Cryptol/F2.hs +48/−0
• src/Cryptol/IR/FreeVars.hs +1/−1
• src/Cryptol/ModuleSystem.hs +1/−1
• src/Cryptol/ModuleSystem/Base.hs +31/−24
• src/Cryptol/ModuleSystem/InstantiateModule.hs +3/−1
• src/Cryptol/ModuleSystem/Interface.hs +2/−1
• src/Cryptol/ModuleSystem/Monad.hs +14/−14
• src/Cryptol/ModuleSystem/Name.hs +1/−1
• src/Cryptol/Parser.y +28/−27
• src/Cryptol/Parser/AST.hs +25/−23
• src/Cryptol/Parser/Lexer.x +8/−25
• src/Cryptol/Parser/LexerUtils.hs +123/−42
• src/Cryptol/Parser/NoPat.hs +4/−3
• src/Cryptol/Parser/ParserUtils.hs +59/−37
• src/Cryptol/Prelude.hs +12/−0
• src/Cryptol/PrimeEC.hs +574/−0
• src/Cryptol/REPL/Command.hs +134/−113
• src/Cryptol/REPL/Monad.hs +3/−18
• src/Cryptol/SHA.hs +564/−0
• src/Cryptol/Symbolic.hs +211/−1
• src/Cryptol/Symbolic/SBV.hs +97/−127
• src/Cryptol/Symbolic/What4.hs +150/−216
• src/Cryptol/Testing/Random.hs +166/−218
• src/Cryptol/Transform/AddModParams.hs +1/−1
• src/Cryptol/Transform/MonoValues.hs +1/−1
• src/Cryptol/Transform/Specialize.hs +1/−1
• src/Cryptol/TypeCheck.hs +17/−4
• src/Cryptol/TypeCheck/AST.hs +8/−8
• src/Cryptol/TypeCheck/CheckModuleInstance.hs +13/−11
• src/Cryptol/TypeCheck/Default.hs +29/−26
• src/Cryptol/TypeCheck/Depends.hs +7/−6
• src/Cryptol/TypeCheck/Error.hs +293/−75
• src/Cryptol/TypeCheck/Infer.hs +111/−96
• src/Cryptol/TypeCheck/InferTypes.hs +11/−2
• src/Cryptol/TypeCheck/Instantiate.hs +5/−3
• src/Cryptol/TypeCheck/Kind.hs +8/−7
• src/Cryptol/TypeCheck/Monad.hs +39/−37
• src/Cryptol/TypeCheck/Parseable.hs +1/−1
• src/Cryptol/TypeCheck/Sanity.hs +8/−7
• src/Cryptol/TypeCheck/SimpType.hs +16/−13
• src/Cryptol/TypeCheck/SimpleSolver.hs +6/−3
• src/Cryptol/TypeCheck/Solve.hs +74/−28
• src/Cryptol/TypeCheck/Solver/Class.hs +57/−119
• src/Cryptol/TypeCheck/Solver/Numeric.hs +47/−34
• src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs +1/−2
• src/Cryptol/TypeCheck/Solver/SMT.hs +0/−3
• src/Cryptol/TypeCheck/Solver/Selector.hs +5/−4
• src/Cryptol/TypeCheck/Solver/Types.hs +5/−2
• src/Cryptol/TypeCheck/Subst.hs +76/−36
• src/Cryptol/TypeCheck/TCon.hs +8/−11
• src/Cryptol/TypeCheck/Type.hs +139/−54
• src/Cryptol/TypeCheck/TypeMap.hs +4/−2
• src/Cryptol/TypeCheck/TypeOf.hs +1/−1
• src/Cryptol/TypeCheck/TypePat.hs +3/−3
• src/Cryptol/Utils/Ident.hs +21/−2
• src/Cryptol/Utils/Misc.hs +4/−3
• src/GitRev.hs +1/−0
• utils/CryHtml.hs +2/−0

@@ -1,3 +1,61 @@+# 2.10.0++## Language changes++* Cryptol now supports primality checking at the type level. The+  type-level predicate `prime` is true when its parameter passes the+  Miller-Rabin probabilistic primality test implemented in the GMP+  library.++* The `Z p` type is now a `Field` when `p` is prime, allowing additional+  operations on `Z p` values.++* The literals `0` and `1` can now be used at type `Bit`, as+  alternatives for `False` and `True`, respectively.++## New features++* The interpreter now includes a number of primitive functions that+  allow faster execution of a number of common cryptographic functions,+  including the core operations of AES and SHA-2, operations on GF(2)+  polynomials (the existing `pmod`, `pdiv`, and `pmult` functions), and+  some operations on prime field elliptic curves. These functions are+  useful for implementing higher-level algorithms, such as many+  post-quantum schemes, with more acceptable performance than possible+  when running a top-to-bottom Cryptol implementation in the+  interpreter.++  For a full list of the new primitives, see the new Cryptol+  [`SuiteB`](https://github.com/GaloisInc/cryptol/blob/master/lib/SuiteB.cry)+  and+  [`PrimeEC`](https://github.com/GaloisInc/cryptol/blob/master/lib/PrimeEC.cry)+  modules.++* The REPL now allows lines containing only comments, making it easier+  to copy and paste examples.++* The interpreter has generally improved performance overall.++* Several error messages are more comprehensible and less verbose.++* Cryptol releases and nightly builds now include an RPC server+  alongside the REPL. This provides an alternative interface to the same+  interpreter and proof engine available from the REPL, but is+  better-suited to programmatic use. Details on the protocol used by the+  server are available+  [here](https://github.com/GaloisInc/argo/blob/master/docs/Protocol.rst).+  A Python client for this protocol is available+  [here](https://github.com/GaloisInc/argo/tree/master/python).++* Windows builds are now distributed as both `.tar.gz` and `.msi` files.++## Bug Fixes++* Closed issues #98, #485, #713, #744, #746, #787, #796, #803, #818,+  #826, #838, #856, #873, #875, #876, #877, #879, #880, #881, #883,+  #886, #887, #888, #892, #894, #901, #910, #913, #924, #926, #931,+  #933, #937, #939, #946, #948, #953, #956, #958, and #969.+ # 2.9.1  ## Language changes

@@ -1,8 +1,9 @@+Cabal-version:       2.4 Name:                cryptol-Version:             2.9.1+Version:             2.10.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+License:             BSD-3-Clause License-file:        LICENSE Author:              Galois, Inc. Maintainer:          cryptol@galois.com@@ -11,11 +12,10 @@ Copyright:           2013-2020 Galois Inc. Category:            Language Build-type:          Simple-Cabal-version:       1.18 extra-source-files:  bench/data/*.cry                      CHANGES.md -data-files:          *.cry *.z3+data-files:          **/*.cry **/*.z3 data-dir:            lib  source-repository head@@ -25,8 +25,9 @@ source-repository this   type:     git   location: https://github.com/GaloisInc/cryptol.git-  tag:      2.9.1+  tag:      2.10.0 + flag static   default: False   description: Create a statically-linked binary@@ -35,11 +36,6 @@   default: True   description: Don't use the Cabal-provided data directory for looking up Cryptol libraries. This is useful when the data directory can't be known ahead of time, like for a relocatable distribution. --- Note: the Cryptol server needs to be updated to some new APIs.---flag server---  default: False---  description: Build with the ZeroMQ/JSON cryptol-server executable- library   Default-language:     Haskell2010@@ -56,17 +52,21 @@                        exceptions,                        filepath          >= 1.3,                        gitrev            >= 1.0,+                       ghc-prim,                        GraphSCC          >= 1.0.4,                        heredoc           >= 0.2,+                       integer-gmp       >= 1.0 && < 1.1,                        libBF             >= 0.5.1,+                       MemoTrie          >= 0.6 && < 0.7,                        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.6,+                       sbv               >= 8.6 && < 8.8,                        simple-smt        >= 0.7.1,+                       stm               >= 2.4,                        strict,                        text              >= 1.1,                        tf-random         >= 0.5,@@ -76,7 +76,7 @@                        panic             >= 0.3,                        what4             >= 1.0 && < 1.1 -  Build-tools:         alex, happy+  Build-tool-depends:  alex:alex, happy:happy   hs-source-dirs:      src    Exposed-modules:     Cryptol.Parser,@@ -157,25 +157,30 @@                         Cryptol.IR.FreeVars, +                       Cryptol.Backend,+                       Cryptol.Backend.Arch,+                       Cryptol.Backend.Concrete,+                       Cryptol.Backend.FloatHelpers,+                       Cryptol.Backend.Monad,+                       Cryptol.Backend.SBV,+                       Cryptol.Backend.What4,+                       Cryptol.Backend.What4.SFloat,+                        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.AES,+                       Cryptol.F2,+                       Cryptol.SHA,+                       Cryptol.PrimeEC,+                        Cryptol.Testing.Random,                         Cryptol.Symbolic,@@ -196,8 +201,6 @@   if impl(ghc >= 8.0.1)      ghc-options: -Wno-redundant-constraints -  ghc-prof-options: -O2 -fprof-auto-top-   if flag(relocatable)       cpp-options: -DRELOCATABLE @@ -206,10 +209,13 @@     Haskell2010   Main-is:             Main.hs   hs-source-dirs:      cryptol+  Autogen-modules:     Paths_cryptol+   Other-modules:       OptParser,                        REPL.Haskeline,                        REPL.Logo,                        Paths_cryptol+   build-depends:       ansi-terminal                      , base                      , base-compat@@ -225,8 +231,6 @@   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 @@ -237,37 +241,6 @@   hs-source-dirs: utils   build-depends: base, text, cryptol, blaze-html   GHC-options: -Wall---- Note: the Cryptol server needs to be updated to some new APIs.---executable cryptol-server---  main-is:             Main.hs---  hs-source-dirs:      cryptol-server---  other-modules:       Cryptol.Aeson---  default-language:    Haskell2010---  default-extensions:  OverloadedStrings---  GHC-options:         -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m"---  if impl(ghc >= 8.0.1)---     ghc-options: -Wno-redundant-constraints---  if os(linux) && flag(static)---      ld-options:      -static -pthread---  if flag(server)---     build-depends: aeson >= 0.10---                  , aeson-pretty >= 0.7---                  , base---                  , base-compat---                  , bytestring >= 0.10---                  , containers---                  , cryptol---                  , filepath---                  , monad-control---                  , optparse-applicative >= 0.12---                  , text---                  , transformers---                  , unix---                  , unordered-containers >= 0.2---                  , zeromq4-haskell >= 0.6---  else---      buildable: False  benchmark cryptol-bench   type:                exitcode-stdio-1.0

@@ -44,6 +44,9 @@  * 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.+ *+ * If the modulus 'n' is prime, 'Z n' also+ * supports computing inverses and forms a field.  */ primitive type {n : #} (fin n, n >= 1) => Z n : * @@ -80,6 +83,9 @@ /** Assert that a numeric type is a proper natural number (not 'inf'). */ primitive type fin : # -> Prop +/** Assert that a numeric type is a prime number. */+primitive type prime : # -> Prop+ /** Add numeric types. */ primitive type (+) : # -> # -> # @@ -111,7 +117,8 @@ primitive type width : # -> #  /**- * Define the base 2 logarithm function in terms of width+ * The ceiling of the base-2 logarithm of a numeric type.+ * We define 'lg2 n = width (n - 1)' for nonzero n, and 'lg2 0 = 0'.  */ type lg2 n = width (max n 1 - 1) @@ -656,10 +663,8 @@ primitive (>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]  /**- * Log base two.- *- * For words, computes the ceiling of log, base 2, of a number.- *  We set 'lg2 0 = 0'+ * The ceiling of the base-2 logarithm of an unsigned bitvector.+ * We set 'lg2 0 = 0'.  */ primitive lg2 : {n} (fin n) => [n] -> [n] @@ -883,60 +888,56 @@ /**  * Performs multiplication of polynomials over GF(2).  */-pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]-pmult x y = last zs-  where-    zs = [0] # [ (z << 1) ^ (if yi then 0 # x else 0) | yi <- y | z <- zs ]+primitive pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]  /**  * Performs division of polynomials over GF(2).  */-pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]-pdiv x y = [ z ! degree | z <- zs ]-  where-    degree : [width v]-    degree = last (ds : [1 + v]_)-      where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]--    reduce : [v] -> [v]-    reduce u = if u ! degree then u ^ y else u--    zs : [u][v]-    zs = [ tail (reduce z # [xi]) | z <- [0] # zs | xi <- x ]+primitive pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]  /**  * Performs modulus of polynomials over GF(2).  */-pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]-pmod x y = if y == 0 then 0/0 else last zs-  where-    degree : [width v]-    degree = last (ds : [2 + v]_)-      where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]--    reduce : [1 + v] -> [1 + v]-    reduce u = if u ! degree then u ^ y else u--    powers : [inf][1 + v]-    powers = [reduce 1] # [ reduce (p << 1) | p <- powers ]--    zs = [0] # [ z ^ (if xi then tail p else 0) | xi <- reverse x | p <- powers | z <- zs ]-+primitive pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]  // Experimental primitives ------------------------------------------------------------  /**  * Parallel map.  The given function is applied to each element in the  * given finite seqeuence, and the results are computed in parallel.+ * The values in the resulting sequence are reduced to normal form,+ * as is done with the deepseq operation.  *+ * The Eq constraint restricts this operation to types+ * where reduction to normal form makes sense.+ *  * This function is experimental.  */-primitive parmap : {a, b, n} (fin n) => (a -> b) -> [n]a -> [n]b+primitive parmap : {a, b, n} (Eq b, fin n) => (a -> b) -> [n]a -> [n]b   // Utility operations -----------------------------------------------------------------  /**+ * A strictness-increasing operation.  The first operand+ * is reduced to normal form before evaluating the second+ * argument.+ *+ * The Eq constraint restricts this operation to types+ * where reduction to normal form makes sense.+ */+primitive deepseq : {a, b} Eq a => a -> b -> b++/**+ * Reduce to normal form.+ *+ * The Eq constraint restricts this operation to types+ * where reduction to normal form makes sense.+ */+rnf : {a} Eq a => a -> a+rnf x = deepseq x x++/**  * Raise a run-time error with the given message.  * This function can be called at any type.  */@@ -1009,13 +1010,13 @@  * Conjunction after applying a predicate to all elements.  */ all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit-all f xs = and (map f xs)+all f xs = foldl' (/\) True (map f xs)  /**  * Disjunction after applying a predicate to all elements.  */ any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit-any f xs = or (map f xs)+any f xs = foldl' (\/) False (map f xs)  /**  * Map a function over a sequence.@@ -1028,24 +1029,49 @@  *  * foldl (+) 0 [1,2,3] = ((0 + 1) + 2) + 3  */-foldl : {n, a, b} (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]+primitive foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a  /**+ * Functional left fold, with strict evaluation of the accumulator value.+ * The accumulator is reduced to normal form at each step.  The Eq constraint+ * restricts the accumulator to types where reduction to normal form makes sense.+ *+ * foldl' (+) 0 [1,2,3] = ((0 + 1) + 2) + 3+ */+primitive foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a++/**  * Functional right fold.  *  * foldr (-) 0 [1,2,3] = 0 - (1 - (2 - 3))  */ foldr : {n, a, b} (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]+foldr f acc xs = foldl g acc (reverse xs)+  where g b a = f a b  /**+ * Functional right fold, with strict evaluation of the accumulator value.+ * The accumulator is reduced to weak head normal form at each step.+ *+ * foldr' (-) 0 [1,2,3] = 0 - (1 - (2 - 3))+ */+foldr' : {n, a, b} (fin n, Eq b) => (a -> b -> b) -> b -> [n]a -> b+foldr' f acc xs = foldl' g acc (reverse xs)+  where g b a = f a b++/**  * Compute the sum of the values in the sequence.  */-sum : {n, a} (fin n, Ring a) => [n]a -> a-sum xs = foldl (+) (fromInteger 0) xs+sum : {n, a} (fin n, Eq a, Ring a) => [n]a -> a+sum xs = foldl' (+) (fromInteger 0) xs+++/**+ * Compute the product of the values in the sequence.+ */+product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a+product xs = foldl' (*) (fromInteger 1) xs+  /**  * Scan left is like a foldl that also emits the intermediate values.

@@ -0,0 +1,46 @@+module Cryptol::Reference where++/**+ * Performs multiplication of polynomials over GF(2).+ * Reference implementation.+ */+pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]+pmult x y = last zs+  where+    zs = [0] # [ (z << 1) ^ (if yi then 0 # x else 0) | yi <- y | z <- zs ]++/**+ * Performs division of polynomials over GF(2).+ * Reference implementation.+ */+pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]+pdiv x y = [ z ! degree | z <- zs ]+  where+    degree : [width v]+    degree = last (ds : [1 + v]_)+      where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]++    reduce : [v] -> [v]+    reduce u = if u ! degree then u ^ y else u++    zs : [u][v]+    zs = [ tail (reduce z # [xi]) | z <- [0] # zs | xi <- x ]++/**+ * Performs modulus of polynomials over GF(2).+ * Reference implementation.+ */+pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]+pmod x y = if y == 0 then 0/0 else last zs+  where+    degree : [width v]+    degree = last (ds : [2 + v]_)+      where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]++    reduce : [1 + v] -> [1 + v]+    reduce u = if u ! degree then u ^ y else u++    powers : [inf][1 + v]+    powers = [reduce 1] # [ reduce (p << 1) | p <- powers ]++    zs = [0] # [ z ^ (if xi then tail p else 0) | xi <- reverse x | p <- powers | z <- zs ]

@@ -0,0 +1,162 @@+module PrimeEC where++/**+ * The type of points of an elliptic curve in affine coordinates.+ * The coefficients are taken from the prime field 'Z p' with 'p > 3'.+ * This is intended to represent all the "normal" points+ * on the curve, which satisfy 'x^^3 == y^^2 - 3x + b', + * for some curve parameter 'b'.  This type cannot represent+ * the special projective "point at infinity".+ */+type AffinePoint p =+  { x : Z p+  , y : Z p+  }++/**+ * The type of points of an elliptic curve in (homogeneous)+ * projective coordinates.  The coefficients are taken from the+ * prime field 'Z p' with 'p > 3'. These points should be understood as+ * representatives of equivalence classes of points, where two representatives+ * 'S' and 'T' are equivalent iff one is a scalar multiple of the other. That+ * is, 'S' and 'T' are equivalent iff there exists some 'k' where+ * 'S.x == k*T.x /\ S.y == k*T.y /\ S.z == k*T.z'.  Finally, the+ * vector with all coordinates equal to 0 is excluded and does not+ * represent any point.+ *+ * Note that all the affine points are easily embedded into projective+ * coordinates by simply setting the `z` coordinate to 1, and the "point at+ * infinity" is represented by any point with 'z == 0'.  Further, for any+ * projective point with 'z != 0', we can compute the corresponding affine+ * point by simply multiplying the x and y coordinates by the inverse of z.+ */+type ProjectivePoint p =+  { x : Z p+  , y : Z p+  , z : Z p+  }++/**+ * 'ec_is_point_affine b S' checks that the supposed affine elliptic curve+ * point 'S' in fact lies on the curve defined by the curve parameter 'b'.  Here,+ * and throughout this module, we assume the curve parameter 'a' is equal to+ * '-3'.  Precisely, this function checks the following condition:+ *+ *     S.y^^2 == S.x^^3 - 3*S.x + b+ */+ec_is_point_affine : {p} (prime p, p > 3) => Z p -> AffinePoint p -> Bit+ec_is_point_affine b S = S.y^^2 == S.x^^3 - (3*S.x) + b+++/**+ * 'ec_is_nonsingular' checks that the given curve parameter 'b' gives rise to+ * a non-singular elliptic curve, appropriate for use in ECC.+ *+ * Precisely, this checks that '4*a^^3 + 27*b^^2 != 0 mod p'.  Here, and+ * throughout this module, we assume 'a = -3'.+ */+ec_is_nonsingular : {p} (prime p, p > 3) => Z p -> Bit+ec_is_nonsingular b = (fromInteger 4) * a^^3 + (fromInteger 27) * b^^2 != 0+  where a = -3 : Z p++/**+ * Returns true if the given point is the identity "point at infinity."+ * This is true whenever the 'z' coordinate is 0, but one of the 'x' or+ * 'y' coordinates is nonzero.+ */+ec_is_identity : {p} (prime p, p > 3) => ProjectivePoint p -> Bit+ec_is_identity S = S.z == 0 /\ ~(S.x == 0 /\ S.y == 0)++/**+ * Test two projective points for equality, up to the equivalence relation+ * on projective points.+ */+ec_equal : {p} (prime p, p > 3) => ProjectivePoint p -> ProjectivePoint p -> Bit+ec_equal S T =+  (S.z == 0 /\ T.z == 0) \/+  (S.z != 0 /\ T.z != 0 /\ ec_affinify S == ec_affinify T)++/**+ * Compute a projective representative for the given affine point.+ */+ec_projectify : {p} (prime p, p > 3) => AffinePoint p -> ProjectivePoint p+ec_projectify R = { x = R.x, y = R.y, z = 1 }++/**+ * Compute the affine point corresponding to the given projective point.+ * This results in an error if the 'z' component of the given point is 0,+ * in which case there is no corresponding affine point.+ */+ec_affinify : {p} (prime p, p > 3) => ProjectivePoint p -> AffinePoint p+ec_affinify S =+ if S.z == 0 then error "Cannot affinify the point at infinity" else R+    where+      R = {x = lambda^^2 * S.x, y = lambda^^3 * S.y }+      lambda = recip S.z++/**+ * Coerce an integer modulo 'p' to a bitvector. This will reduce the value+ * modulo '2^^a' if necessary.+ */+ZtoBV : {p, a} (fin p, p >= 1, fin a) => Z p -> [a]+ZtoBV x = fromInteger (fromZ x)++/**+ * Coerce a bitvector value to an integer modulo 'p'.  This will+ * reduce the value modulo 'p' if necessary.+ */+BVtoZ : {p, a} (fin p, p >= 1, fin a) => [a] -> Z p+BVtoZ x = fromInteger (toInteger x)++/**+ * Given a projective point 'S', compute '2S = S+S'.+ */+primitive ec_double : {p} (prime p, p > 3) =>+  ProjectivePoint p -> ProjectivePoint p++/**+ * Given two projective points 'S' and 'T' where neither is the identity,+ * compute 'S+T'. If the points are not known to be distinct from the point+ * at infinity, use 'ec_add' instead.+ */+primitive ec_add_nonzero : {p} (prime p, p > 3) =>+  ProjectivePoint p -> ProjectivePoint p -> ProjectivePoint p++/**+ * Given a projective point 'S', compute its negation, '-S'+ */+ec_negate : {p} (prime p, p > 3) => ProjectivePoint p -> ProjectivePoint p+ec_negate S = { x = S.x, y = -S.y, z = S.z }++/**+ * Given two projective points 'S' and 'T' compute 'S+T'.+ */+ec_add : {p} (prime p, p > 3) =>+  ProjectivePoint p -> ProjectivePoint p -> ProjectivePoint p+ec_add S T =+  if S.z == 0 then T+   | T.z == 0 then S+   else R+ where R = ec_add_nonzero S T++/**+ * Given two projective points 'S' and 'T' compute 'S-T'.+ */+ec_sub : {p} (prime p, p > 3) =>+  ProjectivePoint p -> ProjectivePoint p -> ProjectivePoint p+ec_sub S T = ec_add S U+ where U = { x = T.x, y = -T.y, z = T.z }++/**+ * Given a scalar value 'k' and a projective point 'S', compute the+ * scalar multiplication 'kS'.+ */+primitive ec_mult : {p} (prime p, p > 3) =>+  Z p -> ProjectivePoint p -> ProjectivePoint p++/**+ * Given a scalar value 'j' and a projective point 'S', and another scalar+ * value 'k' and point 'T', compute the "twin" scalar multiplication 'jS + kT'.+ */+primitive ec_twin_mult : {p} (prime p, p > 3) =>+  Z p -> ProjectivePoint p -> Z p -> ProjectivePoint p -> ProjectivePoint p

@@ -0,0 +1,236 @@+module SuiteB where++/***** AES ******/++/**+ * Key schedule parameter setting for AES-128+ */+type AES128 = 4++/**+ * Key schedule parameter setting for AES-192+ */+type AES192 = 6++/**+ * Key schedule parameter setting for AES-256+ */+type AES256 = 8++/**+ * Element of an AES key schedule for use in a particular round+ */+type AESRoundKey = [4][32]++/**+ * Expanded encryption key schedule for AES+ */+type AESEncryptKeySchedule k =+  { aesEncInitialKey : AESRoundKey+  , aesEncRoundKeys  : [k+5]AESRoundKey+  , aesEncFinalKey   : AESRoundKey+  }++/**+ * Expanded decryption key schedule for AES+ */+type AESDecryptKeySchedule k =+  { aesDecInitialKey : AESRoundKey+  , aesDecRoundKeys  : [k+5]AESRoundKey+  , aesDecFinalKey   : AESRoundKey+  }++/**+ * Encryption key expansion for AES-128.+ *   See FIPS 197, section 5.2.+ */+aes128EncryptSchedule : [128] -> AESEncryptKeySchedule AES128+aes128EncryptSchedule = aesExpandEncryptSchedule++/**+ * Decryption key expansion for AES-128, for use in the "equivalent inverse cypher".+ *   See FIPS 197, sections 5.2 and 5.3.5.+ */+aes128DecryptSchedule : [128] -> AESDecryptKeySchedule AES128+aes128DecryptSchedule = aesExpandDecryptSchedule++/**+ * Encryption and decryption key schedules for AES-128.+ * If you will need both schedules, it is slightly more efficient+ * to call this function than to compute the two schedules separately.+ *   See FIPS 197, sections 5.2 and 5.3.5.+ */+aes128Schedules : [128] -> (AESEncryptKeySchedule AES128, AESDecryptKeySchedule AES128)+aes128Schedules = aesExpandSchedules++/**+ * Encryption key expansion for AES-192.+ *   See FIPS 197, section 5.2.+ */+aes192EncryptSchedule : [192] -> AESEncryptKeySchedule AES192+aes192EncryptSchedule = aesExpandEncryptSchedule++/**+ * Decryption key expansion for AES-192, for use in the "equivalent inverse cypher".+ *   See FIPS 197, sections 5.2 and 5.3.5.+ */+aes192DecryptSchedule : [192] -> AESDecryptKeySchedule AES192+aes192DecryptSchedule = aesExpandDecryptSchedule++/**+ * Encryption and decryption key schedules for AES-192.+ * If you will need both schedules, it is slightly more efficient+ * to call this function than to compute the two schedules separately.+ *   See FIPS 197, sections 5.2 and 5.3.5.+ */+aes192Schedules : [192] -> (AESEncryptKeySchedule AES192, AESDecryptKeySchedule AES192)+aes192Schedules = aesExpandSchedules+++/**+ * Encryption key expansion for AES-256.+ *   See FIPS 197, section 5.2+ */+aes256EncryptSchedule : [256] -> AESEncryptKeySchedule AES256+aes256EncryptSchedule = aesExpandEncryptSchedule++/**+ * Decryption key expansion for AES-256, for use in the "equivalent inverse cypher".+ *   See FIPS 197, sections 5.2 and 5.3.5.+ */+aes256DecryptSchedule : [256] -> AESDecryptKeySchedule AES256+aes256DecryptSchedule = aesExpandDecryptSchedule++/**+ * Encryption and decryption key schedules for AES-256.+ * If you will need both schedules, it is slightly more efficient+ * to call this function than to compute the two schedules separately.+ *   See FIPS 197, sections 5.2 and 5.3.5.+ */+aes256Schedules : [256] -> (AESEncryptKeySchedule AES256, AESDecryptKeySchedule AES256)+aes256Schedules = aesExpandSchedules++/**+ * AES block encryption algorithm.+ *   See FIPS 197, section 5.1.+ */+aesEncryptBlock : {k} (fin k) => AESEncryptKeySchedule k -> [128] -> [128]+aesEncryptBlock schedule plaintext = rnf (join final)+  where+  final = (AESEncFinalRound (rds!0)) ^ schedule.aesEncFinalKey++  rds = [ schedule.aesEncInitialKey ^ split plaintext ] #+        [ AESEncRound r ^ rdk+        | rdk <- schedule.aesEncRoundKeys+        | r   <- rds+        ]++/**+ * AES block decryption algorithm, via the "equivalent inverse cypher".+ *   See FIPS 197, section 5.3.5.+ */+aesDecryptBlock : {k} (fin k) => AESDecryptKeySchedule k -> [128] -> [128]+aesDecryptBlock schedule cyphertext = rnf (join final)+  where+  final = (AESDecFinalRound (rds!0)) ^ schedule.aesDecFinalKey++  rds = [ split cyphertext ^ schedule.aesDecInitialKey ] #+        [ AESDecRound r ^ rdk+        | rdk <- schedule.aesDecRoundKeys+        | r   <- rds+        ]++private+    aesExpandEncryptSchedule : {k} (fin k, k >= 4, 8 >= k) => [k * 32] -> AESEncryptKeySchedule k+    aesExpandEncryptSchedule key = rnf+         { aesEncInitialKey = ks @  0+         , aesEncRoundKeys  = ks @@ [ 1 .. k+5 ]+         , aesEncFinalKey   = ks @  `(k+6)+         }+      where+      ks : [k+7]AESRoundKey+      ks = groupBy`{4} (AESKeyExpand`{k} (split key))++    aesEncToDecSchedule : {k} (fin k) => AESEncryptKeySchedule k -> AESDecryptKeySchedule k+    aesEncToDecSchedule enc = rnf+       { aesDecInitialKey = enc.aesEncFinalKey+       , aesDecRoundKeys  = map AESInvMixColumns (reverse (enc.aesEncRoundKeys))+       , aesDecFinalKey   = enc.aesEncInitialKey+       }++    aesExpandDecryptSchedule : {k} (fin k, k >= 4, 8 >= k) => [k * 32] -> AESDecryptKeySchedule k+    aesExpandDecryptSchedule key = aesEncToDecSchedule (aesExpandEncryptSchedule key)++    aesExpandSchedules : {k} (fin k, k >= 4, 8 >= k) => [k * 32] -> (AESEncryptKeySchedule k, AESDecryptKeySchedule k)+    aesExpandSchedules key = (encS, aesEncToDecSchedule encS)+      where encS = aesExpandEncryptSchedule key++    primitive AESEncRound      : [4][32] -> [4][32]+    primitive AESEncFinalRound : [4][32] -> [4][32]+    primitive AESDecRound      : [4][32] -> [4][32]+    primitive AESDecFinalRound : [4][32] -> [4][32]+    primitive AESInvMixColumns : [4][32] -> [4][32]+    primitive AESKeyExpand     : {k} (fin k, k >= 4, 8 >= k) => [k][32] -> [4*(k+7)][32]+++/***** SHA2 *****/++/**+ * The SHA-224 secure hash algorithm.  See FIPS 180-4, section 6.3.+ */+sha224 : {L} (fin L) => [L] -> [224]+sha224 msg = join (processSHA2_224 (sha2blocks`{32} msg))++/**+ * The SHA-256 secure hash algorithm.  See FIPS 180-4, section 6.2.2.+ */+sha256 : {L} (fin L) => [L] -> [256]+sha256 msg = join (processSHA2_256 (sha2blocks`{32} msg))++/**+ * The SHA-384 secure hash algorithm.  See FIPS 180-4, section 6.5.+ */+sha384 : {L} (fin L) => [L] -> [384]+sha384 msg = join (processSHA2_384 (sha2blocks`{64} msg))++/**+ * The SHA-512 secure hash algorithm.  See FIPS 180-4, section 6.4.+ */+sha512 : {L} (fin L) => [L] -> [512]+sha512 msg = join (processSHA2_512 (sha2blocks`{64} msg))++private+    type sha2_block_size w = 16 * w+    type sha2_num_blocks w L = (L+1+2*w) /^ sha2_block_size w+    type sha2_padded_size w L = sha2_num_blocks w L * sha2_block_size w++    sha2pad : {w, L} (fin w, fin L, w >= 1) => [L] -> [sha2_padded_size w L]+    sha2pad M = M # 0b1 # zero # ((fromInteger `L) : [2*w])++    sha2blocks : {w, L} (fin w, fin L, w >= 1) =>+      [L] -> [sha2_num_blocks w L][16][w]+    sha2blocks msg = [ split x | x <- split (sha2pad`{w} msg) ]++    /**+     * Apply the SHA224 hash algorithm to a sequence of SHA256-size blocks,+     * which are assumed to already be correctly padded.+     */+    primitive processSHA2_224 : {n} (fin n) => [n][16][32] -> [7][32]++    /**+     * Apply the SHA256 hash algorithm to a sequence of SHA256-size blocks,+     * which are assumed to already be correctly padded.+     */+    primitive processSHA2_256 : {n} (fin n) => [n][16][32] -> [8][32]++    /**+     * Apply the SHA384 hash algorithm to a sequence of SHA512-size blocks,+     * which are assumed to already be correctly padded.+     */+    primitive processSHA2_384 : {n} (fin n) => [n][16][64] -> [6][64]++    /**+     * Apply the SHA512 hash algorithm to a sequence of SHA512-size blocks,+     * which are assumed to already be correctly padded.+     */+    primitive processSHA2_512 : {n} (fin n) => [n][16][64] -> [8][64]

@@ -0,0 +1,493 @@+-----------------------------------------------------------------------------+-- |+-- Module    : Cryptol.AES+-- Copyright : (c) Levent Erkok+-- License   : BSD3+-- Maintainer: erkokl@gmail.com+-- Stability : experimental+--+-- A TBox-based implementation of AES primitives, based on+-- the AES example code from SBV.  Here we've stripped out+-- everything except the basic primitives needed, which+-- essentially boil down to table table lookups in most cases.+-----------------------------------------------------------------------------+{-# LANGUAGE ParallelListComp #-}+module Cryptol.AES+  ( State+  , Key+  , keyExpansionWords+  , invMixColumns+  , aesRound+  , aesFinalRound+  , aesInvRound+  , aesInvFinalRound+  ) where++import Data.Bits+import Data.List (transpose, genericDrop, genericTake)+import Data.Word (Word8, Word32)++-- | An element of the Galois Field 2^8, which are essentially polynomials with+-- maximum degree 7. They are conveniently represented as values between 0 and 255.+type GF28 = Word8++-----------------------------------------------------------------------------+-- ** Types and basic operations+-----------------------------------------------------------------------------+-- | AES state. The state consists of four 32-bit words, each of which is in turn treated+-- as four GF28's, i.e., 4 bytes. The T-Box implementation keeps the four-bytes together+-- for efficient representation.+type State = [Word32]++-- | The key, which can be 128, 192, or 256 bits. Represented as a sequence of 32-bit words.+type Key = [Word32]++-- | Rotating a state row by a fixed amount to the right.+rotR :: [GF28] -> Int -> [GF28]+rotR [a, b, c, d] 1 = [d, a, b, c]+rotR [a, b, c, d] 2 = [c, d, a, b]+rotR [a, b, c, d] 3 = [b, c, d, a]+rotR xs           i = error $ "rotR: Unexpected input: " ++ show (xs, i)+++toBytes :: Word32 -> [Word8]+toBytes w = [b0,b1,b2,b3]+  where+  b0 = fromIntegral (w `shiftR` 24)+  b1 = fromIntegral (w `shiftR` 16)+  b2 = fromIntegral (w `shiftR`  8)+  b3 = fromIntegral  w++fromBytes :: [Word8] -> Word32+fromBytes [b0,b1,b2,b3] = w+  where+  w = ((fromIntegral b0) `shiftL` 24) .|.+      ((fromIntegral b1) `shiftL` 16) .|.+      ((fromIntegral b2) `shiftL`  8) .|.+       (fromIntegral b3)+fromBytes bs = error ("Unexpected list length in fromBytes: " ++ show (length bs))+++-----------------------------------------------------------------------------+-- ** GF28 multiplication tables+-----------------------------------------------------------------------------++-- GF(2^8) multiplication by 0x0e+mETable :: [GF28]+mETable =+  [0x00, 0x0e, 0x1c, 0x12, 0x38, 0x36, 0x24, 0x2a, 0x70, 0x7e, 0x6c,+   0x62, 0x48, 0x46, 0x54, 0x5a, 0xe0, 0xee, 0xfc, 0xf2, 0xd8, 0xd6,+   0xc4, 0xca, 0x90, 0x9e, 0x8c, 0x82, 0xa8, 0xa6, 0xb4, 0xba, 0xdb,+   0xd5, 0xc7, 0xc9, 0xe3, 0xed, 0xff, 0xf1, 0xab, 0xa5, 0xb7, 0xb9,+   0x93, 0x9d, 0x8f, 0x81, 0x3b, 0x35, 0x27, 0x29, 0x03, 0x0d, 0x1f,+   0x11, 0x4b, 0x45, 0x57, 0x59, 0x73, 0x7d, 0x6f, 0x61, 0xad, 0xa3,+   0xb1, 0xbf, 0x95, 0x9b, 0x89, 0x87, 0xdd, 0xd3, 0xc1, 0xcf, 0xe5,+   0xeb, 0xf9, 0xf7, 0x4d, 0x43, 0x51, 0x5f, 0x75, 0x7b, 0x69, 0x67,+   0x3d, 0x33, 0x21, 0x2f, 0x05, 0x0b, 0x19, 0x17, 0x76, 0x78, 0x6a,+   0x64, 0x4e, 0x40, 0x52, 0x5c, 0x06, 0x08, 0x1a, 0x14, 0x3e, 0x30,+   0x22, 0x2c, 0x96, 0x98, 0x8a, 0x84, 0xae, 0xa0, 0xb2, 0xbc, 0xe6,+   0xe8, 0xfa, 0xf4, 0xde, 0xd0, 0xc2, 0xcc, 0x41, 0x4f, 0x5d, 0x53,+   0x79, 0x77, 0x65, 0x6b, 0x31, 0x3f, 0x2d, 0x23, 0x09, 0x07, 0x15,+   0x1b, 0xa1, 0xaf, 0xbd, 0xb3, 0x99, 0x97, 0x85, 0x8b, 0xd1, 0xdf,+   0xcd, 0xc3, 0xe9, 0xe7, 0xf5, 0xfb, 0x9a, 0x94, 0x86, 0x88, 0xa2,+   0xac, 0xbe, 0xb0, 0xea, 0xe4, 0xf6, 0xf8, 0xd2, 0xdc, 0xce, 0xc0,+   0x7a, 0x74, 0x66, 0x68, 0x42, 0x4c, 0x5e, 0x50, 0x0a, 0x04, 0x16,+   0x18, 0x32, 0x3c, 0x2e, 0x20, 0xec, 0xe2, 0xf0, 0xfe, 0xd4, 0xda,+   0xc8, 0xc6, 0x9c, 0x92, 0x80, 0x8e, 0xa4, 0xaa, 0xb8, 0xb6, 0x0c,+   0x02, 0x10, 0x1e, 0x34, 0x3a, 0x28, 0x26, 0x7c, 0x72, 0x60, 0x6e,+   0x44, 0x4a, 0x58, 0x56, 0x37, 0x39, 0x2b, 0x25, 0x0f, 0x01, 0x13,+   0x1d, 0x47, 0x49, 0x5b, 0x55, 0x7f, 0x71, 0x63, 0x6d, 0xd7, 0xd9,+   0xcb, 0xc5, 0xef, 0xe1, 0xf3, 0xfd, 0xa7, 0xa9, 0xbb, 0xb5, 0x9f,+   0x91, 0x83, 0x8d]++-- GF(2^8) multiplication by 0x0b+mBTable :: [GF28]+mBTable =+  [0x00, 0x0b, 0x16, 0x1d, 0x2c, 0x27, 0x3a, 0x31, 0x58, 0x53, 0x4e,+   0x45, 0x74, 0x7f, 0x62, 0x69, 0xb0, 0xbb, 0xa6, 0xad, 0x9c, 0x97,+   0x8a, 0x81, 0xe8, 0xe3, 0xfe, 0xf5, 0xc4, 0xcf, 0xd2, 0xd9, 0x7b,+   0x70, 0x6d, 0x66, 0x57, 0x5c, 0x41, 0x4a, 0x23, 0x28, 0x35, 0x3e,+   0x0f, 0x04, 0x19, 0x12, 0xcb, 0xc0, 0xdd, 0xd6, 0xe7, 0xec, 0xf1,+   0xfa, 0x93, 0x98, 0x85, 0x8e, 0xbf, 0xb4, 0xa9, 0xa2, 0xf6, 0xfd,+   0xe0, 0xeb, 0xda, 0xd1, 0xcc, 0xc7, 0xae, 0xa5, 0xb8, 0xb3, 0x82,+   0x89, 0x94, 0x9f, 0x46, 0x4d, 0x50, 0x5b, 0x6a, 0x61, 0x7c, 0x77,+   0x1e, 0x15, 0x08, 0x03, 0x32, 0x39, 0x24, 0x2f, 0x8d, 0x86, 0x9b,+   0x90, 0xa1, 0xaa, 0xb7, 0xbc, 0xd5, 0xde, 0xc3, 0xc8, 0xf9, 0xf2,+   0xef, 0xe4, 0x3d, 0x36, 0x2b, 0x20, 0x11, 0x1a, 0x07, 0x0c, 0x65,+   0x6e, 0x73, 0x78, 0x49, 0x42, 0x5f, 0x54, 0xf7, 0xfc, 0xe1, 0xea,+   0xdb, 0xd0, 0xcd, 0xc6, 0xaf, 0xa4, 0xb9, 0xb2, 0x83, 0x88, 0x95,+   0x9e, 0x47, 0x4c, 0x51, 0x5a, 0x6b, 0x60, 0x7d, 0x76, 0x1f, 0x14,+   0x09, 0x02, 0x33, 0x38, 0x25, 0x2e, 0x8c, 0x87, 0x9a, 0x91, 0xa0,+   0xab, 0xb6, 0xbd, 0xd4, 0xdf, 0xc2, 0xc9, 0xf8, 0xf3, 0xee, 0xe5,+   0x3c, 0x37, 0x2a, 0x21, 0x10, 0x1b, 0x06, 0x0d, 0x64, 0x6f, 0x72,+   0x79, 0x48, 0x43, 0x5e, 0x55, 0x01, 0x0a, 0x17, 0x1c, 0x2d, 0x26,+   0x3b, 0x30, 0x59, 0x52, 0x4f, 0x44, 0x75, 0x7e, 0x63, 0x68, 0xb1,+   0xba, 0xa7, 0xac, 0x9d, 0x96, 0x8b, 0x80, 0xe9, 0xe2, 0xff, 0xf4,+   0xc5, 0xce, 0xd3, 0xd8, 0x7a, 0x71, 0x6c, 0x67, 0x56, 0x5d, 0x40,+   0x4b, 0x22, 0x29, 0x34, 0x3f, 0x0e, 0x05, 0x18, 0x13, 0xca, 0xc1,+   0xdc, 0xd7, 0xe6, 0xed, 0xf0, 0xfb, 0x92, 0x99, 0x84, 0x8f, 0xbe,+   0xb5, 0xa8, 0xa3]+++-- GF(2^8) multiplication by 0x0d+mDTable :: [GF28]+mDTable =+  [0x00, 0x0d, 0x1a, 0x17, 0x34, 0x39, 0x2e, 0x23, 0x68, 0x65, 0x72,+   0x7f, 0x5c, 0x51, 0x46, 0x4b, 0xd0, 0xdd, 0xca, 0xc7, 0xe4, 0xe9,+   0xfe, 0xf3, 0xb8, 0xb5, 0xa2, 0xaf, 0x8c, 0x81, 0x96, 0x9b, 0xbb,+   0xb6, 0xa1, 0xac, 0x8f, 0x82, 0x95, 0x98, 0xd3, 0xde, 0xc9, 0xc4,+   0xe7, 0xea, 0xfd, 0xf0, 0x6b, 0x66, 0x71, 0x7c, 0x5f, 0x52, 0x45,+   0x48, 0x03, 0x0e, 0x19, 0x14, 0x37, 0x3a, 0x2d, 0x20, 0x6d, 0x60,+   0x77, 0x7a, 0x59, 0x54, 0x43, 0x4e, 0x05, 0x08, 0x1f, 0x12, 0x31,+   0x3c, 0x2b, 0x26, 0xbd, 0xb0, 0xa7, 0xaa, 0x89, 0x84, 0x93, 0x9e,+   0xd5, 0xd8, 0xcf, 0xc2, 0xe1, 0xec, 0xfb, 0xf6, 0xd6, 0xdb, 0xcc,+   0xc1, 0xe2, 0xef, 0xf8, 0xf5, 0xbe, 0xb3, 0xa4, 0xa9, 0x8a, 0x87,+   0x90, 0x9d, 0x06, 0x0b, 0x1c, 0x11, 0x32, 0x3f, 0x28, 0x25, 0x6e,+   0x63, 0x74, 0x79, 0x5a, 0x57, 0x40, 0x4d, 0xda, 0xd7, 0xc0, 0xcd,+   0xee, 0xe3, 0xf4, 0xf9, 0xb2, 0xbf, 0xa8, 0xa5, 0x86, 0x8b, 0x9c,+   0x91, 0x0a, 0x07, 0x10, 0x1d, 0x3e, 0x33, 0x24, 0x29, 0x62, 0x6f,+   0x78, 0x75, 0x56, 0x5b, 0x4c, 0x41, 0x61, 0x6c, 0x7b, 0x76, 0x55,+   0x58, 0x4f, 0x42, 0x09, 0x04, 0x13, 0x1e, 0x3d, 0x30, 0x27, 0x2a,+   0xb1, 0xbc, 0xab, 0xa6, 0x85, 0x88, 0x9f, 0x92, 0xd9, 0xd4, 0xc3,+   0xce, 0xed, 0xe0, 0xf7, 0xfa, 0xb7, 0xba, 0xad, 0xa0, 0x83, 0x8e,+   0x99, 0x94, 0xdf, 0xd2, 0xc5, 0xc8, 0xeb, 0xe6, 0xf1, 0xfc, 0x67,+   0x6a, 0x7d, 0x70, 0x53, 0x5e, 0x49, 0x44, 0x0f, 0x02, 0x15, 0x18,+   0x3b, 0x36, 0x21, 0x2c, 0x0c, 0x01, 0x16, 0x1b, 0x38, 0x35, 0x22,+   0x2f, 0x64, 0x69, 0x7e, 0x73, 0x50, 0x5d, 0x4a, 0x47, 0xdc, 0xd1,+   0xc6, 0xcb, 0xe8, 0xe5, 0xf2, 0xff, 0xb4, 0xb9, 0xae, 0xa3, 0x80,+   0x8d, 0x9a, 0x97]++-- GF(2^8) multiplication by 0x09+m9Table :: [GF28]+m9Table =+  [0x00, 0x09, 0x12, 0x1b, 0x24, 0x2d, 0x36, 0x3f, 0x48, 0x41, 0x5a,+   0x53, 0x6c, 0x65, 0x7e, 0x77, 0x90, 0x99, 0x82, 0x8b, 0xb4, 0xbd,+   0xa6, 0xaf, 0xd8, 0xd1, 0xca, 0xc3, 0xfc, 0xf5, 0xee, 0xe7, 0x3b,+   0x32, 0x29, 0x20, 0x1f, 0x16, 0x0d, 0x04, 0x73, 0x7a, 0x61, 0x68,+   0x57, 0x5e, 0x45, 0x4c, 0xab, 0xa2, 0xb9, 0xb0, 0x8f, 0x86, 0x9d,+   0x94, 0xe3, 0xea, 0xf1, 0xf8, 0xc7, 0xce, 0xd5, 0xdc, 0x76, 0x7f,+   0x64, 0x6d, 0x52, 0x5b, 0x40, 0x49, 0x3e, 0x37, 0x2c, 0x25, 0x1a,+   0x13, 0x08, 0x01, 0xe6, 0xef, 0xf4, 0xfd, 0xc2, 0xcb, 0xd0, 0xd9,+   0xae, 0xa7, 0xbc, 0xb5, 0x8a, 0x83, 0x98, 0x91, 0x4d, 0x44, 0x5f,+   0x56, 0x69, 0x60, 0x7b, 0x72, 0x05, 0x0c, 0x17, 0x1e, 0x21, 0x28,+   0x33, 0x3a, 0xdd, 0xd4, 0xcf, 0xc6, 0xf9, 0xf0, 0xeb, 0xe2, 0x95,+   0x9c, 0x87, 0x8e, 0xb1, 0xb8, 0xa3, 0xaa, 0xec, 0xe5, 0xfe, 0xf7,+   0xc8, 0xc1, 0xda, 0xd3, 0xa4, 0xad, 0xb6, 0xbf, 0x80, 0x89, 0x92,+   0x9b, 0x7c, 0x75, 0x6e, 0x67, 0x58, 0x51, 0x4a, 0x43, 0x34, 0x3d,+   0x26, 0x2f, 0x10, 0x19, 0x02, 0x0b, 0xd7, 0xde, 0xc5, 0xcc, 0xf3,+   0xfa, 0xe1, 0xe8, 0x9f, 0x96, 0x8d, 0x84, 0xbb, 0xb2, 0xa9, 0xa0,+   0x47, 0x4e, 0x55, 0x5c, 0x63, 0x6a, 0x71, 0x78, 0x0f, 0x06, 0x1d,+   0x14, 0x2b, 0x22, 0x39, 0x30, 0x9a, 0x93, 0x88, 0x81, 0xbe, 0xb7,+   0xac, 0xa5, 0xd2, 0xdb, 0xc0, 0xc9, 0xf6, 0xff, 0xe4, 0xed, 0x0a,+   0x03, 0x18, 0x11, 0x2e, 0x27, 0x3c, 0x35, 0x42, 0x4b, 0x50, 0x59,+   0x66, 0x6f, 0x74, 0x7d, 0xa1, 0xa8, 0xb3, 0xba, 0x85, 0x8c, 0x97,+   0x9e, 0xe9, 0xe0, 0xfb, 0xf2, 0xcd, 0xc4, 0xdf, 0xd6, 0x31, 0x38,+   0x23, 0x2a, 0x15, 0x1c, 0x07, 0x0e, 0x79, 0x70, 0x6b, 0x62, 0x5d,+   0x54, 0x4f, 0x46]+++-- GF(2^8) multiplication by 0x02+m2Table :: [GF28]+m2Table =+  [0x00, 0x02, 0x04, 0x06, 0x08, 0x0a, 0x0c, 0x0e, 0x10, 0x12, 0x14,+   0x16, 0x18, 0x1a, 0x1c, 0x1e, 0x20, 0x22, 0x24, 0x26, 0x28, 0x2a,+   0x2c, 0x2e, 0x30, 0x32, 0x34, 0x36, 0x38, 0x3a, 0x3c, 0x3e, 0x40,+   0x42, 0x44, 0x46, 0x48, 0x4a, 0x4c, 0x4e, 0x50, 0x52, 0x54, 0x56,+   0x58, 0x5a, 0x5c, 0x5e, 0x60, 0x62, 0x64, 0x66, 0x68, 0x6a, 0x6c,+   0x6e, 0x70, 0x72, 0x74, 0x76, 0x78, 0x7a, 0x7c, 0x7e, 0x80, 0x82,+   0x84, 0x86, 0x88, 0x8a, 0x8c, 0x8e, 0x90, 0x92, 0x94, 0x96, 0x98,+   0x9a, 0x9c, 0x9e, 0xa0, 0xa2, 0xa4, 0xa6, 0xa8, 0xaa, 0xac, 0xae,+   0xb0, 0xb2, 0xb4, 0xb6, 0xb8, 0xba, 0xbc, 0xbe, 0xc0, 0xc2, 0xc4,+   0xc6, 0xc8, 0xca, 0xcc, 0xce, 0xd0, 0xd2, 0xd4, 0xd6, 0xd8, 0xda,+   0xdc, 0xde, 0xe0, 0xe2, 0xe4, 0xe6, 0xe8, 0xea, 0xec, 0xee, 0xf0,+   0xf2, 0xf4, 0xf6, 0xf8, 0xfa, 0xfc, 0xfe, 0x1b, 0x19, 0x1f, 0x1d,+   0x13, 0x11, 0x17, 0x15, 0x0b, 0x09, 0x0f, 0x0d, 0x03, 0x01, 0x07,+   0x05, 0x3b, 0x39, 0x3f, 0x3d, 0x33, 0x31, 0x37, 0x35, 0x2b, 0x29,+   0x2f, 0x2d, 0x23, 0x21, 0x27, 0x25, 0x5b, 0x59, 0x5f, 0x5d, 0x53,+   0x51, 0x57, 0x55, 0x4b, 0x49, 0x4f, 0x4d, 0x43, 0x41, 0x47, 0x45,+   0x7b, 0x79, 0x7f, 0x7d, 0x73, 0x71, 0x77, 0x75, 0x6b, 0x69, 0x6f,+   0x6d, 0x63, 0x61, 0x67, 0x65, 0x9b, 0x99, 0x9f, 0x9d, 0x93, 0x91,+   0x97, 0x95, 0x8b, 0x89, 0x8f, 0x8d, 0x83, 0x81, 0x87, 0x85, 0xbb,+   0xb9, 0xbf, 0xbd, 0xb3, 0xb1, 0xb7, 0xb5, 0xab, 0xa9, 0xaf, 0xad,+   0xa3, 0xa1, 0xa7, 0xa5, 0xdb, 0xd9, 0xdf, 0xdd, 0xd3, 0xd1, 0xd7,+   0xd5, 0xcb, 0xc9, 0xcf, 0xcd, 0xc3, 0xc1, 0xc7, 0xc5, 0xfb, 0xf9,+   0xff, 0xfd, 0xf3, 0xf1, 0xf7, 0xf5, 0xeb, 0xe9, 0xef, 0xed, 0xe3,+   0xe1, 0xe7, 0xe5]++-- GF(2^8) multiplication by 0x03+m3Table :: [GF28]+m3Table =+  [0x00, 0x03, 0x06, 0x05, 0x0c, 0x0f, 0x0a, 0x09, 0x18, 0x1b, 0x1e,+   0x1d, 0x14, 0x17, 0x12, 0x11, 0x30, 0x33, 0x36, 0x35, 0x3c, 0x3f,+   0x3a, 0x39, 0x28, 0x2b, 0x2e, 0x2d, 0x24, 0x27, 0x22, 0x21, 0x60,+   0x63, 0x66, 0x65, 0x6c, 0x6f, 0x6a, 0x69, 0x78, 0x7b, 0x7e, 0x7d,+   0x74, 0x77, 0x72, 0x71, 0x50, 0x53, 0x56, 0x55, 0x5c, 0x5f, 0x5a,+   0x59, 0x48, 0x4b, 0x4e, 0x4d, 0x44, 0x47, 0x42, 0x41, 0xc0, 0xc3,+   0xc6, 0xc5, 0xcc, 0xcf, 0xca, 0xc9, 0xd8, 0xdb, 0xde, 0xdd, 0xd4,+   0xd7, 0xd2, 0xd1, 0xf0, 0xf3, 0xf6, 0xf5, 0xfc, 0xff, 0xfa, 0xf9,+   0xe8, 0xeb, 0xee, 0xed, 0xe4, 0xe7, 0xe2, 0xe1, 0xa0, 0xa3, 0xa6,+   0xa5, 0xac, 0xaf, 0xaa, 0xa9, 0xb8, 0xbb, 0xbe, 0xbd, 0xb4, 0xb7,+   0xb2, 0xb1, 0x90, 0x93, 0x96, 0x95, 0x9c, 0x9f, 0x9a, 0x99, 0x88,+   0x8b, 0x8e, 0x8d, 0x84, 0x87, 0x82, 0x81, 0x9b, 0x98, 0x9d, 0x9e,+   0x97, 0x94, 0x91, 0x92, 0x83, 0x80, 0x85, 0x86, 0x8f, 0x8c, 0x89,+   0x8a, 0xab, 0xa8, 0xad, 0xae, 0xa7, 0xa4, 0xa1, 0xa2, 0xb3, 0xb0,+   0xb5, 0xb6, 0xbf, 0xbc, 0xb9, 0xba, 0xfb, 0xf8, 0xfd, 0xfe, 0xf7,+   0xf4, 0xf1, 0xf2, 0xe3, 0xe0, 0xe5, 0xe6, 0xef, 0xec, 0xe9, 0xea,+   0xcb, 0xc8, 0xcd, 0xce, 0xc7, 0xc4, 0xc1, 0xc2, 0xd3, 0xd0, 0xd5,+   0xd6, 0xdf, 0xdc, 0xd9, 0xda, 0x5b, 0x58, 0x5d, 0x5e, 0x57, 0x54,+   0x51, 0x52, 0x43, 0x40, 0x45, 0x46, 0x4f, 0x4c, 0x49, 0x4a, 0x6b,+   0x68, 0x6d, 0x6e, 0x67, 0x64, 0x61, 0x62, 0x73, 0x70, 0x75, 0x76,+   0x7f, 0x7c, 0x79, 0x7a, 0x3b, 0x38, 0x3d, 0x3e, 0x37, 0x34, 0x31,+   0x32, 0x23, 0x20, 0x25, 0x26, 0x2f, 0x2c, 0x29, 0x2a, 0x0b, 0x08,+   0x0d, 0x0e, 0x07, 0x04, 0x01, 0x02, 0x13, 0x10, 0x15, 0x16, 0x1f,+   0x1c, 0x19, 0x1a]+++-- table-lookup versions of gf28Mult with the constants used in invMixColumns+-- and TBox construction++m2 :: GF28 -> GF28+m2 i = m2Table !! fromIntegral i++m3 :: GF28 -> GF28+m3 i = m3Table !! fromIntegral i++mE :: GF28 -> GF28+mE i = mETable !! fromIntegral i++mB :: GF28 -> GF28+mB i = mBTable !! fromIntegral i++mD :: GF28 -> GF28+mD i = mDTable !! fromIntegral i++m9 :: GF28 -> GF28+m9 i = m9Table !! fromIntegral i++-----------------------------------------------------------------------------+-- ** The key schedule+-----------------------------------------------------------------------------++-- | The @InvMixColumns@ transformation, as described in Section 5.3.3 of the standard. Note+-- that this transformation is only used explicitly during key-expansion in the T-Box implementation+-- of AES.+invMixColumns :: State -> State+invMixColumns state = map fromBytes $ transpose $ mmult (map toBytes state)+ where dot f   = foldr1 xor . zipWith ($) f+       mmult :: [[Word8]] -> [[Word8]]+       mmult n = [map (dot r) n | r <- [ [mE, mB, mD, m9]+                                       , [m9, mE, mB, mD]+                                       , [mD, m9, mE, mB]+                                       , [mB, mD, m9, mE]+                                       ]]++keyExpansionWords :: Integer -> Key -> [Word32]+keyExpansionWords nk key = genericTake (4*(nk+7)) keys+   where keys :: [Word32]+         keys = key ++ [nextWord i prev old | i <- [nk ..] | prev <- genericDrop (nk-1) keys | old <- keys]++         nextWord :: Integer -> Word32 -> Word32 -> Word32+         nextWord i prev old+           | i `mod` nk == 0           = old `xor` subWordRcon (prev `rotateL` 8) (roundConstants !! fromInteger (i `div` nk))+           | i `mod` nk == 4 && nk > 6 = old `xor` subWordRcon prev 0+           | True                      = old `xor` prev++         subWordRcon :: Word32 -> GF28 -> Word32+         subWordRcon w rc = fromBytes [a `xor` rc, b, c, d]+            where [a, b, c, d] = map sbox $ toBytes w+++-- | Definition of round-constants, as specified in Section 5.2 of the AES standard.+--   We only need up to the 11th value for AES-128, and fewer than that for AES-192+--   and AES-256.+roundConstants :: [GF28]+roundConstants = [0,1,2,4,8,16,32,64,128,27,54]++-----------------------------------------------------------------------------+-- ** The S-box transformation+-----------------------------------------------------------------------------++sboxTable :: [GF28]+sboxTable =+  [0x63, 0x7c, 0x77, 0x7b, 0xf2, 0x6b, 0x6f, 0xc5, 0x30, 0x01, 0x67,+   0x2b, 0xfe, 0xd7, 0xab, 0x76, 0xca, 0x82, 0xc9, 0x7d, 0xfa, 0x59,+   0x47, 0xf0, 0xad, 0xd4, 0xa2, 0xaf, 0x9c, 0xa4, 0x72, 0xc0, 0xb7,+   0xfd, 0x93, 0x26, 0x36, 0x3f, 0xf7, 0xcc, 0x34, 0xa5, 0xe5, 0xf1,+   0x71, 0xd8, 0x31, 0x15, 0x04, 0xc7, 0x23, 0xc3, 0x18, 0x96, 0x05,+   0x9a, 0x07, 0x12, 0x80, 0xe2, 0xeb, 0x27, 0xb2, 0x75, 0x09, 0x83,+   0x2c, 0x1a, 0x1b, 0x6e, 0x5a, 0xa0, 0x52, 0x3b, 0xd6, 0xb3, 0x29,+   0xe3, 0x2f, 0x84, 0x53, 0xd1, 0x00, 0xed, 0x20, 0xfc, 0xb1, 0x5b,+   0x6a, 0xcb, 0xbe, 0x39, 0x4a, 0x4c, 0x58, 0xcf, 0xd0, 0xef, 0xaa,+   0xfb, 0x43, 0x4d, 0x33, 0x85, 0x45, 0xf9, 0x02, 0x7f, 0x50, 0x3c,+   0x9f, 0xa8, 0x51, 0xa3, 0x40, 0x8f, 0x92, 0x9d, 0x38, 0xf5, 0xbc,+   0xb6, 0xda, 0x21, 0x10, 0xff, 0xf3, 0xd2, 0xcd, 0x0c, 0x13, 0xec,+   0x5f, 0x97, 0x44, 0x17, 0xc4, 0xa7, 0x7e, 0x3d, 0x64, 0x5d, 0x19,+   0x73, 0x60, 0x81, 0x4f, 0xdc, 0x22, 0x2a, 0x90, 0x88, 0x46, 0xee,+   0xb8, 0x14, 0xde, 0x5e, 0x0b, 0xdb, 0xe0, 0x32, 0x3a, 0x0a, 0x49,+   0x06, 0x24, 0x5c, 0xc2, 0xd3, 0xac, 0x62, 0x91, 0x95, 0xe4, 0x79,+   0xe7, 0xc8, 0x37, 0x6d, 0x8d, 0xd5, 0x4e, 0xa9, 0x6c, 0x56, 0xf4,+   0xea, 0x65, 0x7a, 0xae, 0x08, 0xba, 0x78, 0x25, 0x2e, 0x1c, 0xa6,+   0xb4, 0xc6, 0xe8, 0xdd, 0x74, 0x1f, 0x4b, 0xbd, 0x8b, 0x8a, 0x70,+   0x3e, 0xb5, 0x66, 0x48, 0x03, 0xf6, 0x0e, 0x61, 0x35, 0x57, 0xb9,+   0x86, 0xc1, 0x1d, 0x9e, 0xe1, 0xf8, 0x98, 0x11, 0x69, 0xd9, 0x8e,+   0x94, 0x9b, 0x1e, 0x87, 0xe9, 0xce, 0x55, 0x28, 0xdf, 0x8c, 0xa1,+   0x89, 0x0d, 0xbf, 0xe6, 0x42, 0x68, 0x41, 0x99, 0x2d, 0x0f, 0xb0,+   0x54, 0xbb, 0x16]++-- | The AES sbox transformation+sbox :: GF28 -> GF28+sbox i = sboxTable !! fromIntegral i++-----------------------------------------------------------------------------+-- ** The inverse S-box transformation+-----------------------------------------------------------------------------++unSBoxTable :: [GF28]+unSBoxTable =+  [0x52, 0x09, 0x6a, 0xd5, 0x30, 0x36, 0xa5, 0x38, 0xbf, 0x40, 0xa3,+   0x9e, 0x81, 0xf3, 0xd7, 0xfb, 0x7c, 0xe3, 0x39, 0x82, 0x9b, 0x2f,+   0xff, 0x87, 0x34, 0x8e, 0x43, 0x44, 0xc4, 0xde, 0xe9, 0xcb, 0x54,+   0x7b, 0x94, 0x32, 0xa6, 0xc2, 0x23, 0x3d, 0xee, 0x4c, 0x95, 0x0b,+   0x42, 0xfa, 0xc3, 0x4e, 0x08, 0x2e, 0xa1, 0x66, 0x28, 0xd9, 0x24,+   0xb2, 0x76, 0x5b, 0xa2, 0x49, 0x6d, 0x8b, 0xd1, 0x25, 0x72, 0xf8,+   0xf6, 0x64, 0x86, 0x68, 0x98, 0x16, 0xd4, 0xa4, 0x5c, 0xcc, 0x5d,+   0x65, 0xb6, 0x92, 0x6c, 0x70, 0x48, 0x50, 0xfd, 0xed, 0xb9, 0xda,+   0x5e, 0x15, 0x46, 0x57, 0xa7, 0x8d, 0x9d, 0x84, 0x90, 0xd8, 0xab,+   0x00, 0x8c, 0xbc, 0xd3, 0x0a, 0xf7, 0xe4, 0x58, 0x05, 0xb8, 0xb3,+   0x45, 0x06, 0xd0, 0x2c, 0x1e, 0x8f, 0xca, 0x3f, 0x0f, 0x02, 0xc1,+   0xaf, 0xbd, 0x03, 0x01, 0x13, 0x8a, 0x6b, 0x3a, 0x91, 0x11, 0x41,+   0x4f, 0x67, 0xdc, 0xea, 0x97, 0xf2, 0xcf, 0xce, 0xf0, 0xb4, 0xe6,+   0x73, 0x96, 0xac, 0x74, 0x22, 0xe7, 0xad, 0x35, 0x85, 0xe2, 0xf9,+   0x37, 0xe8, 0x1c, 0x75, 0xdf, 0x6e, 0x47, 0xf1, 0x1a, 0x71, 0x1d,+   0x29, 0xc5, 0x89, 0x6f, 0xb7, 0x62, 0x0e, 0xaa, 0x18, 0xbe, 0x1b,+   0xfc, 0x56, 0x3e, 0x4b, 0xc6, 0xd2, 0x79, 0x20, 0x9a, 0xdb, 0xc0,+   0xfe, 0x78, 0xcd, 0x5a, 0xf4, 0x1f, 0xdd, 0xa8, 0x33, 0x88, 0x07,+   0xc7, 0x31, 0xb1, 0x12, 0x10, 0x59, 0x27, 0x80, 0xec, 0x5f, 0x60,+   0x51, 0x7f, 0xa9, 0x19, 0xb5, 0x4a, 0x0d, 0x2d, 0xe5, 0x7a, 0x9f,+   0x93, 0xc9, 0x9c, 0xef, 0xa0, 0xe0, 0x3b, 0x4d, 0xae, 0x2a, 0xf5,+   0xb0, 0xc8, 0xeb, 0xbb, 0x3c, 0x83, 0x53, 0x99, 0x61, 0x17, 0x2b,+   0x04, 0x7e, 0xba, 0x77, 0xd6, 0x26, 0xe1, 0x69, 0x14, 0x63, 0x55,+   0x21, 0x0c, 0x7d]++-- | The inverse s-box transformation.+unSBox :: GF28 -> GF28+unSBox i = unSBoxTable !! fromIntegral i+++-----------------------------------------------------------------------------+-- ** Tables for T-Box encryption+-----------------------------------------------------------------------------++-- | T-box table generation function for encryption+t0Func :: GF28 -> [GF28]+t0Func a = [ m2 s, s, s, m3 s]+  where s = sbox a++-- | First look-up table used in encryption+t0 :: GF28 -> Word32+t0 i = t0Table !! fromIntegral i++t0Table :: [Word32]+t0Table = [fromBytes (t0Func a)          | a <- [0..255]]++-- | Second look-up table used in encryption+t1 :: GF28 -> Word32+t1 i = t1Table !! fromIntegral i++t1Table :: [Word32]+t1Table = [fromBytes (t0Func a `rotR` 1) | a <- [0..255]]++-- | Third look-up table used in encryption+t2 :: GF28 -> Word32+t2 i = t2Table !! fromIntegral i++t2Table :: [Word32]+t2Table = [fromBytes (t0Func a `rotR` 2) | a <- [0..255]]++-- | Fourth look-up table used in encryption+t3 :: GF28 -> Word32+t3 i = t3Table !! fromIntegral i++t3Table :: [Word32]+t3Table = [fromBytes (t0Func a `rotR` 3) | a <- [0..255]]++-----------------------------------------------------------------------------+-- ** Tables for T-Box decryption+-----------------------------------------------------------------------------++-- | T-box table generating function for decryption+u0Func :: GF28 -> [GF28]+u0Func a = [ mE s, m9 s, mD s, mB s ]+ where s = unSBox a++-- | First look-up table used in decryption+u0 :: GF28 -> Word32+u0 i = u0Table !! fromIntegral i++u0Table :: [Word32]+u0Table = [fromBytes (u0Func a)          | a <- [0..255]]++-- | Second look-up table used in decryption+u1 :: GF28 -> Word32+u1 i = u1Table !! fromIntegral i++u1Table :: [Word32]+u1Table = [fromBytes (u0Func a `rotR` 1) | a <- [0..255]]++-- | Third look-up table used in decryption+u2 :: GF28 -> Word32+u2 i = u2Table !! fromIntegral i++u2Table :: [Word32]+u2Table = [fromBytes (u0Func a `rotR` 2) | a <- [0..255]]++-- | Fourth look-up table used in decryption+u3 :: GF28 -> Word32+u3 i = u3Table !! fromIntegral i++u3Table :: [Word32]+u3Table = [fromBytes (u0Func a `rotR` 3) | a <- [0..255]]++-----------------------------------------------------------------------------+-- ** AES rounds+-----------------------------------------------------------------------------++aesRound :: State -> State+aesRound s = d+  where d = map f [0..3]+        a = map toBytes s+        f j = e0 `xor` e1 `xor` e2 `xor` e3+              where e0 = t0 (a !! ((j+0) `mod` 4) !! 0)+                    e1 = t1 (a !! ((j+1) `mod` 4) !! 1)+                    e2 = t2 (a !! ((j+2) `mod` 4) !! 2)+                    e3 = t3 (a !! ((j+3) `mod` 4) !! 3)++aesFinalRound :: State -> State+aesFinalRound s = d+  where d = map f [0..3]+        a = map toBytes s+        f j = fromBytes [ sbox (a !! ((j+0) `mod` 4) !! 0)+                        , sbox (a !! ((j+1) `mod` 4) !! 1)+                        , sbox (a !! ((j+2) `mod` 4) !! 2)+                        , sbox (a !! ((j+3) `mod` 4) !! 3)+                        ]++aesInvRound :: State -> State+aesInvRound s = d+  where d = map f [0..3]+        a = map toBytes s+        f j = e0 `xor` e1 `xor` e2 `xor` e3+              where e0 = u0 (a !! ((j+0) `mod` 4) !! 0)+                    e1 = u1 (a !! ((j+3) `mod` 4) !! 1)+                    e2 = u2 (a !! ((j+2) `mod` 4) !! 2)+                    e3 = u3 (a !! ((j+1) `mod` 4) !! 3)++aesInvFinalRound :: State -> State+aesInvFinalRound s = d+  where d = map f [0..3]+        a = map toBytes s+        f j = fromBytes [ unSBox (a !! ((j+0) `mod` 4) !! 0)+                        , unSBox (a !! ((j+3) `mod` 4) !! 1)+                        , unSBox (a !! ((j+2) `mod` 4) !! 2)+                        , unSBox (a !! ((j+1) `mod` 4) !! 3)+                        ]

@@ -0,0 +1,714 @@+{-# Language FlexibleContexts #-}+{-# Language TypeFamilies #-}+module Cryptol.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.Backend.FloatHelpers (BF)+import Cryptol.Backend.Monad ( PPOpts(..), EvalError(..) )+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)++  -- | Construct a floating point value from the given bit-precise+  --   floating-point representation.+  fpExactLit :: sym -> BF -> 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)++  -- | Multiplicitive inverse in (Z n).+  --   PRECONDITION: the modulus is a prime+  znRecip ::+    sym ->+    Integer {- ^ modulus -} ->+    SInteger sym ->+    SEval sym (SInteger 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)++  fpLogicalEq   :: 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,30 @@+-- |+-- Module      :  Cryptol.Eval.Arch+-- Copyright   :  (c) 2014-2016 Galois, Inc.+-- License     :  BSD3+-- Maintainer  :  cryptol@galois.com+-- Stability   :  provisional+-- Portability :  portable+--+-- Architecture-specific parts of the concrete evaluator go here.+{-# LANGUAGE CPP #-}+module Cryptol.Backend.Arch where++-- | This is the widest word we can have before gmp will fail to+-- allocate and bring down the whole program. According to+-- <https://gmplib.org/list-archives/gmp-bugs/2009-July/001538.html>+-- the sizes are 2^32-1 for 32-bit, and 2^37 for 64-bit, however+-- experiments show that it's somewhere under 2^37 at least on 64-bit+-- Mac OS X.+maxBigIntWidth :: Integer+#if i386_HOST_ARCH+maxBigIntWidth = 2^(32 :: Integer) - 0x1+#elif x86_64_HOST_ARCH+maxBigIntWidth = 2^(37 :: Integer) - 0x100+#else+-- Because GHC doesn't seem to define a CPP macro that will portably+-- tell us the bit width we're compiling for, fall back on a safe choice+-- for other architectures. If we care about large words on another+-- architecture, we can add a special case for it.+maxBigIntWidth = 2^(32 :: Integer) - 0x1+#endif

@@ -0,0 +1,398 @@+-- |+-- Module      :  Cryptol.Backend.Concrete+-- 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 ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}+module Cryptol.Backend.Concrete+  ( BV(..)+  , binBV+  , unaryBV+  , bvVal+  , ppBV+  , mkBv+  , mask+  , signedBV+  , signedValue+  , integerToChar+  , lg2+  , Concrete(..)+  , liftBinIntMod+  , fpBinArith+  , fpRoundMode+  ) where++import qualified Control.Exception as X+import Data.Bits+import Numeric (showIntAtBase)+import qualified LibBF as FP+import qualified GHC.Integer.GMP.Internals as Integer++import qualified Cryptol.Backend.Arch as Arch+import qualified Cryptol.Backend.FloatHelpers as FP+import Cryptol.Backend+import Cryptol.Backend.Monad+import Cryptol.TypeCheck.Solver.InfNat (genLog)+import Cryptol.Utils.Panic (panic)+import Cryptol.Utils.PP++data Concrete = Concrete deriving Show++-- | 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++  -- NB: under the precondition that `m` is prime,+  -- the only values for which no inverse exists are+  -- congruent to 0 modulo m.+  znRecip sym m x+    | r == 0    = raiseError sym DivideByZero+    | otherwise = pure r+   where+     r = Integer.recipModInteger x m++  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)+  fpExactLit _sym bf     = pure bf+  fpEq _sym x y          = pure (FP.bfValue x == FP.bfValue y)+  fpLogicalEq _sym x y   = pure (FP.bfCompare (FP.bfValue x) (FP.bfValue y) == EQ)+  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+++++

@@ -0,0 +1,248 @@+{-# Language BlockArguments, OverloadedStrings #-}+{-# Language BangPatterns #-}+module Cryptol.Backend.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.Backend.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,394 @@+-- |+-- Module      :  Cryptol.Eval.Monad+-- Copyright   :  (c) 2013-2016 Galois, Inc.+-- License     :  BSD3+-- Maintainer  :  cryptol@galois.com+-- Stability   :  provisional+-- Portability :  portable++{-# LANGUAGE Safe #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}++module Cryptol.Backend.Monad+( -- * Evaluation monad+  Eval(..)+, runEval+, EvalOpts(..)+, PPOpts(..)+, asciiMode+, PPFloatFormat(..)+, PPFloatExp(..)+, defaultPPOpts+, io+, delayFill+, ready+, blackhole+, evalSpark+, maybeReady+  -- * Error reporting+, Unsupported(..)+, EvalError(..)+, evalPanic+, wordTooWide+, typeCannotBeDemoted+) where++import           Control.Concurrent+import           Control.Concurrent.STM++import           Control.Monad+import qualified Control.Monad.Fail as Fail+import           Control.Monad.Fix+import           Control.Monad.IO.Class+import           Data.Typeable (Typeable)+import qualified Control.Exception as X+++import Cryptol.Utils.Panic+import Cryptol.Utils.PP+import Cryptol.Utils.Logger(Logger)+import Cryptol.TypeCheck.AST(Type,Name)++-- | A computation that returns an already-evaluated value.+ready :: a -> Eval a+ready a = Ready a++-- | How to pretty print things when evaluating+data PPOpts = PPOpts+  { useAscii     :: Bool+  , useBase      :: Int+  , useInfLength :: Int+  , useFPBase    :: Int+  , useFPFormat  :: PPFloatFormat+  }++asciiMode :: PPOpts -> Integer -> Bool+asciiMode opts width = useAscii opts && (width == 7 || width == 8)++data PPFloatFormat =+    FloatFixed Int PPFloatExp -- ^ Use this many significant digis+  | FloatFrac Int             -- ^ Show this many digits after floating point+  | FloatFree PPFloatExp      -- ^ Use the correct number of digits++data PPFloatExp = ForceExponent -- ^ Always show an exponent+                | AutoExponent  -- ^ Only show exponent when needed+++defaultPPOpts :: PPOpts+defaultPPOpts = PPOpts { useAscii = False, useBase = 10, useInfLength = 5+                       , useFPBase = 16+                       , useFPFormat = FloatFree AutoExponent+                       }+++-- | Some options for evalutaion+data EvalOpts = EvalOpts+  { evalLogger :: Logger    -- ^ Where to print stuff (e.g., for @trace@)+  , evalPPOpts :: PPOpts    -- ^ How to pretty print things.+  }++-- | The monad for Cryptol evaluation.+--   A computation is either "ready", which means it represents+--   only trivial computation, or is an "eval" action which must+--   be computed to get the answer, or it is a "thunk", which+--   represents a delayed, shared computation.+data Eval a+   = Ready !a+   | Eval !(IO a)+   | Thunk !(TVar (ThunkState a))++-- | This datastructure tracks the lifecycle of a thunk.+--+--   Thunks are used for basically three use cases.  First,+--   we use thunks to preserve sharing.  Basically every+--   cryptol expression that is bound to a name, and is not+--   already obviously a value (and in a few other places as+--   well) will get turned into a thunk in order to avoid+--   recomputations.  These thunks will start in the `Unforced`+--   state, and have a backup computation that just raises+--   the `LoopError` exception.+--+--   Secondly, thunks are used to cut cycles when evaluating+--   recursive definition groups.  Every named clause in a+--   recursive definition is thunked so that the value can appear+--   in its definition.  Such thunks start in the `Void` state,+--   as they must exist before we have a definition to assign them.+--   Forcing a thunk in the `Void` state is a programmer error (panic).+--   Once the body of a definition is ready, we replace the+--   thunk with the relevant computation, going to the `Unforced` state.+--+--   In the third case, we are using thunks to provide an optimistic+--   shortcut for evaluation.  In these cases we first try to run a+--   computation that is stricter than the semantics actually allows.+--   If it succeeds, all is well an we continue.  However, if it tight+--   loops, we fall back on a lazier (and generally more expensive)+--   version, which is the "backup" computation referred to above.+data ThunkState a+  = Void !String+       -- ^ This thunk has not yet been initialized+  | Unforced !(IO a) !(IO a)+       -- ^ This thunk has not yet been forced.  We keep track of the "main"+       --   computation to run and a "backup" computation to run if we+       --   detect a tight loop when evaluating the first one.+  | UnderEvaluation !ThreadId !(IO a)+       -- ^ This thunk is currently being evaluated by the thread with the given+       --   thread ID.  We track the "backup" computation to run if we detect+       --   a tight loop evaluating this thunk.  If the thunk is being evaluated+       --   by some other thread, the current thread will await its completion.+  | ForcedErr !EvalError+       -- ^ This thunk has been forced, and its evaluation results in an exception+  | Forced !a+       -- ^ This thunk has been forced to the given value+++-- | Test if a value is "ready", which means that+--   it requires no computation to return.+maybeReady :: Eval a -> Eval (Maybe a)+maybeReady (Ready a) = pure (Just a)+maybeReady (Thunk tv) = Eval $+  readTVarIO tv >>= \case+     Forced a -> pure (Just a)+     _ -> pure Nothing+maybeReady (Eval _) = pure Nothing+++{-# INLINE delayFill #-}++-- | 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.+delayFill ::+  Eval a {- ^ Computation to delay -} ->+  Eval a {- ^ Backup computation to run if a tight loop is detected -} ->+  Eval (Eval a)+delayFill e@(Ready _) _  = return e+delayFill e@(Thunk _) _  = return e+delayFill (Eval x) backup = Eval (Thunk <$> newTVarIO (Unforced x (runEval backup)))++-- | Begin executing the given operation in a separate thread,+--   returning a thunk which will await the completion of+--   the computation when forced.+evalSpark ::+  Eval a ->+  Eval (Eval a)++-- Ready computations need no additional evaluation.+evalSpark e@(Ready _) = return e++-- A thunked computation might already have+-- been forced.  If so, return the result.  Otherwise,+-- fork a thread to force this computation and return+-- the thunk.+evalSpark (Thunk tv)  = Eval $+  readTVarIO tv >>= \case+    Forced x     -> return (Ready x)+    ForcedErr ex -> return (Eval (X.throwIO ex))+    _ ->+       do _ <- forkIO (sparkThunk tv)+          return (Thunk tv)++-- If the computation is nontrivial but not already a thunk,+-- create a thunk and fork a thread to force it.+evalSpark (Eval x) = Eval $+  do tv <- newTVarIO (Unforced x (X.throwIO (LoopError "")))+     _ <- forkIO (sparkThunk tv)+     return (Thunk tv)+++-- | To the work of forcing a thunk. This is the worker computation+--   that is foked off via @evalSpark@.+sparkThunk :: TVar (ThunkState a) -> IO ()+sparkThunk tv =+  do tid <- myThreadId+     -- Try to claim the thunk.  If it is still in the @Void@ state, wait+     -- until it is in some other state.  If it is @Unforced@ claim the thunk.+     -- Otherwise, it is already evaluated or under evaluation by another thread,+     -- and we have no work to do.+     st <- atomically $+              do st <- readTVar tv+                 case st of+                   Void _ -> retry+                   Unforced _ backup -> writeTVar tv (UnderEvaluation tid backup)+                   _ -> return ()+                 return st+     -- If we successfully claimed the thunk to work on, run the computation and+     -- update the thunk state with the result.+     case st of+       Unforced work _ ->+         X.try work >>= \case+           Left err -> atomically (writeTVar tv (ForcedErr err))+           Right a  -> atomically (writeTVar tv (Forced a))+       _ -> return ()+++-- | 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.+blackhole ::+  String {- ^ A name to associate with this thunk. -} ->+  Eval (Eval a, Eval a -> Eval ())+blackhole msg = Eval $+  do tv <- newTVarIO (Void msg)+     let set (Ready x)  = io $ atomically (writeTVar tv (Forced x))+         set m          = io $ atomically (writeTVar tv (Unforced (runEval m) (X.throwIO (LoopError msg))))+     return (Thunk tv, set)++-- | Force a thunk to get the result.+unDelay :: TVar (ThunkState a) -> IO a+unDelay tv =+  -- First, check if the thunk is in an evaluated state,+  -- and return the value if so.+  readTVarIO tv >>= \case+    Forced x -> pure x+    ForcedErr e -> X.throwIO e+    _ ->+      -- Otherwise, try to claim the thunk to work on.+      do tid <- myThreadId+         res <- atomically $ do+                  res <- readTVar tv+                  case res of+                    -- In this case, we claim the thunk.  Update the state to indicate+                    -- that we are working on it.+                    Unforced _ backup -> writeTVar tv (UnderEvaluation tid backup)++                    -- In this case, the thunk is already being evaluated.  If it is+                    -- under evaluation by this thread, we have to run the backup computation,+                    -- and "consume" it by updating the backup computation to one that throws+                    -- a loop error.  If some other thread is evaluating, reset the+                    -- transaction to await completion of the thunk.+                    UnderEvaluation t _+                      | tid == t  -> writeTVar tv (UnderEvaluation tid (X.throwIO (LoopError "")))+                      | otherwise -> retry -- wait, if some other thread is evaualting+                    _ -> return ()++                  -- Return the original thunk state so we can decide what work to do+                  -- after the transaction completes.+                  return res++         -- helper for actually doing the work+         let doWork work =+               X.try work >>= \case+                 Left ex -> do atomically (writeTVar tv (ForcedErr ex))+                               X.throwIO ex+                 Right a -> do atomically (writeTVar tv (Forced a))+                               return a++         -- Now, examine the thunk state and decide what to do.+         case res of+           Void msg -> evalPanic "unDelay" ["Thunk forced before it was initialized", msg]+           Forced x -> pure x+           ForcedErr e -> X.throwIO e+           UnderEvaluation _ backup -> doWork backup -- this thread was already evaluating this thunk+           Unforced work _ -> doWork work++-- | Execute the given evaluation action.+runEval :: Eval a -> IO a+runEval (Ready a)  = return a+runEval (Eval x)   = x+runEval (Thunk tv) = unDelay tv++{-# INLINE evalBind #-}+evalBind :: Eval a -> (a -> Eval b) -> Eval b+evalBind (Ready a) f  = f a+evalBind (Eval x) f   = Eval (x >>= runEval . f)+evalBind (Thunk x) f  = Eval (unDelay x >>= runEval . f)++instance Functor Eval where+  fmap f (Ready x)   = Ready (f x)+  fmap f (Eval m)    = Eval (f <$> m)+  fmap f (Thunk tv)  = Eval (f <$> unDelay tv)+  {-# INLINE fmap #-}++instance Applicative Eval where+  pure  = return+  (<*>) = ap+  {-# INLINE pure #-}+  {-# INLINE (<*>) #-}++instance Monad Eval where+  return = Ready+  (>>=)  = evalBind+  {-# INLINE return #-}+  {-# INLINE (>>=) #-}++instance Fail.MonadFail Eval where+  fail x = Eval (fail x)++instance MonadIO Eval where+  liftIO = io++instance MonadFix Eval where+  mfix f = Eval $ mfix (\x -> runEval (f x))++-- | Lift an 'IO' computation into the 'Eval' monad.+io :: IO a -> Eval a+io m = Eval m+{-# INLINE io #-}+++-- Errors ----------------------------------------------------------------------++-- | Panic from an @Eval@ context.+evalPanic :: HasCallStack => String -> [String] -> a+evalPanic cxt = panic ("[Eval] " ++ cxt)+++-- | Data type describing errors that can occur during evaluation.+data EvalError+  = InvalidIndex (Maybe Integer)  -- ^ Out-of-bounds index+  | TypeCannotBeDemoted Type      -- ^ Non-numeric type passed to @number@ function+  | DivideByZero                  -- ^ Division or modulus by 0+  | NegativeExponent              -- ^ Exponentiation by negative integer+  | LogNegative                   -- ^ Logarithm of a negative integer+  | WordTooWide Integer           -- ^ Bitvector too large+  | UserError String              -- ^ Call to the Cryptol @error@ primitive+  | LoopError String              -- ^ Detectable nontermination+  | NoPrim Name                   -- ^ Primitive with no implementation+  | BadRoundingMode Integer       -- ^ Invalid rounding mode+  | BadValue String               -- ^ Value outside the domain of a partial function.+    deriving (Typeable,Show)++instance PP EvalError where+  ppPrec _ e = case e of+    InvalidIndex (Just i) -> text "invalid sequence index:" <+> integer i+    InvalidIndex Nothing  -> text "invalid sequence index"+    TypeCannotBeDemoted t -> text "type cannot be demoted:" <+> pp t+    DivideByZero -> text "division by 0"+    NegativeExponent -> text "negative exponent"+    LogNegative -> text "logarithm of negative"+    WordTooWide w ->+      text "word too wide for memory:" <+> integer w <+> text "bits"+    UserError x -> text "Run-time error:" <+> text x+    LoopError x -> text "<<loop>>" <+> text x+    BadRoundingMode r -> "invalid rounding mode" <+> integer r+    BadValue x -> "invalid input for" <+> backticks (text x)+    NoPrim x -> text "unimplemented primitive:" <+> pp x++instance X.Exception EvalError+++data Unsupported+  = UnsupportedSymbolicOp String  -- ^ Operation cannot be supported in the symbolic simulator+    deriving (Typeable,Show)++instance PP Unsupported where+  ppPrec _ e = case e of+    UnsupportedSymbolicOp nm -> text "operation can not be supported on symbolic values:" <+> text nm++instance X.Exception Unsupported+++-- | For things like @`(inf)@ or @`(0-1)@.+typeCannotBeDemoted :: Type -> a+typeCannotBeDemoted t = X.throw (TypeCannotBeDemoted t)++-- | For when we know that a word is too wide and will exceed gmp's+-- limits (though words approaching this size will probably cause the+-- system to crash anyway due to lack of memory).+wordTooWide :: Integer -> a+wordTooWide w = X.throw (WordTooWide w)

@@ -0,0 +1,457 @@+-- |+-- Module      :  Cryptol.Backend.SBV+-- Copyright   :  (c) 2013-2016 Galois, Inc.+-- License     :  BSD3+-- Maintainer  :  cryptol@galois.com+-- Stability   :  provisional+-- Portability :  portable++{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE ViewPatterns #-}+module Cryptol.Backend.SBV+  ( SBV(..), SBVEval(..), SBVResult(..)+  , literalSWord+  , freshSBool_+  , freshBV_+  , freshSInteger_+  , addDefEqn+  , ashr+  , lshr+  , shl+  , evalPanic+  , svFromInteger+  , svToInteger+  ) where++import qualified Control.Exception as X+import           Control.Concurrent.MVar+import           Control.Monad.IO.Class (MonadIO(..))+import           Data.Bits (bit, complement)+import           Data.List (foldl')++import qualified GHC.Integer.GMP.Internals as Integer++import Data.SBV.Dynamic as SBV+import qualified Data.SBV.Internals as SBV++import Cryptol.Backend+import Cryptol.Backend.Concrete ( integerToChar, ppBV, BV(..) )+import Cryptol.Backend.Monad+  ( Eval(..), blackhole, delayFill, evalSpark+  , EvalError(..), Unsupported(..)+  )++import Cryptol.Utils.Panic (panic)+import Cryptol.Utils.PP++data SBV =+  SBV+  { sbvStateVar     :: MVar (SBV.State)+  , sbvDefRelations :: MVar SVal+  }++-- Utility operations -------------------------------------------------------------++fromBitsLE :: [SBit SBV] -> SWord SBV+fromBitsLE bs = foldl' f (literalSWord 0 0) bs+  where f w b = svJoin (svToWord1 b) w++packSBV :: [SBit SBV] -> SWord SBV+packSBV bs = fromBitsLE (reverse bs)++unpackSBV :: SWord SBV -> [SBit SBV]+unpackSBV x = [ svTestBit x i | i <- reverse [0 .. intSizeOf x - 1] ]++literalSWord :: Int -> Integer -> SWord SBV+literalSWord w i = svInteger (KBounded False w) i++freshBV_ :: SBV -> Int -> IO (SWord SBV)+freshBV_ (SBV stateVar _) w =+  withMVar stateVar (svMkSymVar Nothing (KBounded False w) Nothing)++freshSBool_ :: SBV -> IO (SBit SBV)+freshSBool_ (SBV stateVar _) =+  withMVar stateVar (svMkSymVar Nothing KBool Nothing)++freshSInteger_ :: SBV -> IO (SInteger SBV)+freshSInteger_ (SBV stateVar _) =+  withMVar stateVar (svMkSymVar Nothing KUnbounded Nothing)+++-- SBV Evaluation monad -------------------------------------------------------++data SBVResult a+  = SBVError !EvalError+  | SBVResult !SVal !a -- safety predicate and result++instance Functor SBVResult where+  fmap _ (SBVError err) = SBVError err+  fmap f (SBVResult p x) = SBVResult p (f x)++instance Applicative SBVResult where+  pure = SBVResult svTrue+  SBVError err <*> _ = SBVError err+  _ <*> SBVError err = SBVError err+  SBVResult p1 f <*> SBVResult p2 x = SBVResult (svAnd p1 p2) (f x)++instance Monad SBVResult where+  return = pure+  SBVError err >>= _ = SBVError err+  SBVResult px x >>= m =+    case m x of+      SBVError err   -> SBVError err+      SBVResult pm z -> SBVResult (svAnd px pm) z++newtype SBVEval a = SBVEval{ sbvEval :: Eval (SBVResult a) }+  deriving (Functor)++instance Applicative SBVEval where+  pure = SBVEval . pure . pure+  f <*> x = SBVEval $+    do f' <- sbvEval f+       x' <- sbvEval x+       pure (f' <*> x')++instance Monad SBVEval where+  return = pure+  x >>= f = SBVEval $+    sbvEval x >>= \case+      SBVError err -> pure (SBVError err)+      SBVResult px x' ->+        sbvEval (f x') >>= \case+          SBVError err -> pure (SBVError err)+          SBVResult pz z -> pure (SBVResult (svAnd px pz) z)++instance MonadIO SBVEval where+  liftIO m = SBVEval $ fmap pure (liftIO m)+++addDefEqn :: SBV -> SVal -> IO ()+addDefEqn (SBV _ relsVar) b = modifyMVar_ relsVar (pure . svAnd b)++-- Symbolic Big-endian Words -------------------------------------------------------++instance Backend SBV where+  type SBit SBV = SVal+  type SWord SBV = SVal+  type SInteger SBV = SVal+  type SFloat SBV = ()        -- XXX: not implemented+  type SEval SBV = SBVEval++  raiseError _ err = SBVEval (pure (SBVError err))++  assertSideCondition _ cond err+    | Just False <- svAsBool cond = SBVEval (pure (SBVError err))+    | otherwise = SBVEval (pure (SBVResult cond ()))++  isReady _ (SBVEval (Ready _)) = True+  isReady _ _ = False++  sDelayFill _ m retry = SBVEval $+    do m' <- delayFill (sbvEval m) (sbvEval retry)+       pure (pure (SBVEval m'))++  sSpark _ m = SBVEval $+    do m' <- evalSpark (sbvEval m)+       pure (pure (SBVEval m'))++  sDeclareHole _ msg = SBVEval $+    do (hole, fill) <- blackhole msg+       pure (pure (SBVEval hole, \m -> SBVEval (fmap pure $ fill (sbvEval m))))++  mergeEval _sym f c mx my = SBVEval $+    do rx <- sbvEval mx+       ry <- sbvEval my+       case (rx, ry) of+         (SBVError err, SBVError _) ->+           pure $ SBVError err -- arbitrarily choose left error to report+         (SBVError _, SBVResult p y) ->+           pure $ SBVResult (svAnd (svNot c) p) y+         (SBVResult p x, SBVError _) ->+           pure $ SBVResult (svAnd c p) x+         (SBVResult px x, SBVResult py y) ->+           do zr <- sbvEval (f c x y)+              case zr of+                SBVError err -> pure $ SBVError err+                SBVResult pz z ->+                  pure $ SBVResult (svAnd (svIte c px py) pz) z++  wordLen _ v = toInteger (intSizeOf v)+  wordAsChar _ v = integerToChar <$> svAsInteger v++  ppBit _ v+     | Just b <- svAsBool v = text $! if b then "True" else "False"+     | otherwise            = text "?"+  ppWord sym opts v+     | Just x <- svAsInteger v = ppBV opts (BV (wordLen sym v) x)+     | otherwise               = text "[?]"+  ppInteger _ _opts v+     | Just x <- svAsInteger v = integer x+     | otherwise               = text "[?]"++  iteBit _ b x y = pure $! svSymbolicMerge KBool True b x y+  iteWord _ b x y = pure $! svSymbolicMerge (kindOf x) True b x y+  iteInteger _ b x y = pure $! svSymbolicMerge KUnbounded True b x y++  bitAsLit _ b = svAsBool b+  wordAsLit _ w =+    case svAsInteger w of+      Just x -> Just (toInteger (intSizeOf w), x)+      Nothing -> Nothing+  integerAsLit _ v = svAsInteger v++  bitLit _ b     = svBool b+  wordLit _ n x  = pure $! literalSWord (fromInteger n) x+  integerLit _ x = pure $! svInteger KUnbounded x++  bitEq  _ x y = pure $! svEqual x y+  bitOr  _ x y = pure $! svOr x y+  bitAnd _ x y = pure $! svAnd x y+  bitXor _ x y = pure $! svXOr x y+  bitComplement _ x = pure $! svNot x++  wordBit _ x idx = pure $! svTestBit x (intSizeOf x - 1 - fromInteger idx)++  wordUpdate _ x idx b = pure $! svSymbolicMerge (kindOf x) False b wtrue wfalse+    where+     i' = intSizeOf x - 1 - fromInteger idx+     wtrue  = x `svOr`  svInteger (kindOf x) (bit i' :: Integer)+     wfalse = x `svAnd` svInteger (kindOf x) (complement (bit i' :: Integer))++  packWord _ bs  = pure $! packSBV bs+  unpackWord _ x = pure $! unpackSBV x++  wordEq _ x y = pure $! svEqual x y+  wordLessThan _ x y = pure $! svLessThan x y+  wordGreaterThan _ x y = pure $! svGreaterThan x y++  wordSignedLessThan _ x y = pure $! svLessThan sx sy+    where sx = svSign x+          sy = svSign y++  joinWord _ x y = pure $! svJoin x y++  splitWord _ _leftW rightW w = pure+    ( svExtract (intSizeOf w - 1) (fromInteger rightW) w+    , svExtract (fromInteger rightW - 1) 0 w+    )++  extractWord _ len start w =+    pure $! svExtract (fromInteger start + fromInteger len - 1) (fromInteger start) w++  wordAnd _ a b = pure $! svAnd a b+  wordOr  _ a b = pure $! svOr a b+  wordXor _ a b = pure $! svXOr a b+  wordComplement _ a = pure $! svNot a++  wordPlus  _ a b = pure $! svPlus a b+  wordMinus _ a b = pure $! svMinus a b+  wordMult  _ a b = pure $! svTimes a b+  wordNegate _ a  = pure $! svUNeg a++  wordDiv sym a b =+    do let z = literalSWord (intSizeOf b) 0+       assertSideCondition sym (svNot (svEqual b z)) DivideByZero+       pure $! svQuot a b++  wordMod sym a b =+    do let z = literalSWord (intSizeOf b) 0+       assertSideCondition sym (svNot (svEqual b z)) DivideByZero+       pure $! svRem a b++  wordSignedDiv sym a b =+    do let z = literalSWord (intSizeOf b) 0+       assertSideCondition sym (svNot (svEqual b z)) DivideByZero+       pure $! signedQuot a b++  wordSignedMod sym a b =+    do let z = literalSWord (intSizeOf b) 0+       assertSideCondition sym (svNot (svEqual b z)) DivideByZero+       pure $! signedRem a b++  wordLg2 _ a = sLg2 a++  wordToInt _ x = pure $! svToInteger x+  wordFromInt _ w i = pure $! svFromInteger w i++  intEq _ a b = pure $! svEqual a b+  intLessThan _ a b = pure $! svLessThan a b+  intGreaterThan _ a b = pure $! svGreaterThan a b++  intPlus  _ a b = pure $! svPlus a b+  intMinus _ a b = pure $! svMinus a b+  intMult  _ a b = pure $! svTimes a b+  intNegate _ a  = pure $! SBV.svUNeg a++  intDiv sym a b =+    do let z = svInteger KUnbounded 0+       assertSideCondition sym (svNot (svEqual b z)) DivideByZero+       let p = svLessThan z b+       pure $! svSymbolicMerge KUnbounded True p (svQuot a b) (svQuot (svUNeg a) (svUNeg b))+  intMod sym a b =+    do let z = svInteger KUnbounded 0+       assertSideCondition sym (svNot (svEqual b z)) DivideByZero+       let p = svLessThan z b+       pure $! svSymbolicMerge KUnbounded True p (svRem a b) (svUNeg (svRem (svUNeg a) (svUNeg b)))++  -- NB, we don't do reduction here+  intToZn _ _m a = pure a++  znToInt _ 0 _ = evalPanic "znToInt" ["0 modulus not allowed"]+  znToInt _ m a =+    do let m' = svInteger KUnbounded m+       pure $! svRem a m'++  znEq _ 0 _ _ = evalPanic "znEq" ["0 modulus not allowed"]+  znEq sym m a b = svDivisible sym m (SBV.svMinus a b)++  znPlus  sym m a b = sModAdd sym m a b+  znMinus sym m a b = sModSub sym m a b+  znMult  sym m a b = sModMult sym m a b+  znNegate sym m a  = sModNegate sym m a+  znRecip = sModRecip++  ppFloat _ _ _           = text "[?]"+  fpExactLit _ _          = unsupported "fpExactLit"+  fpLit _ _ _ _           = unsupported "fpLit"+  fpLogicalEq _ _ _       = unsupported "fpLogicalEq"+  fpEq _ _ _              = unsupported "fpEq"+  fpLessThan _ _ _        = unsupported "fpLessThan"+  fpGreaterThan _ _ _     = unsupported "fpGreaterThan"+  fpPlus _ _ _ _          = unsupported "fpPlus"+  fpMinus _ _ _ _         = unsupported "fpMinus"+  fpMult _  _ _ _         = unsupported "fpMult"+  fpDiv _ _ _ _           = unsupported "fpDiv"+  fpNeg _ _               = unsupported "fpNeg"+  fpFromInteger _ _ _ _ _ = unsupported "fpFromInteger"+  fpToInteger _ _ _ _     = unsupported "fpToInteger"++unsupported :: String -> SEval SBV a+unsupported x = liftIO (X.throw (UnsupportedSymbolicOp x))+++svToInteger :: SWord SBV -> SInteger SBV+svToInteger w =+  case svAsInteger w of+    Nothing -> svFromIntegral KUnbounded w+    Just x  -> svInteger KUnbounded x++svFromInteger :: Integer -> SInteger SBV -> SWord SBV+svFromInteger 0 _ = literalSWord 0 0+svFromInteger n i =+  case svAsInteger i of+    Nothing -> svFromIntegral (KBounded False (fromInteger n)) i+    Just x  -> literalSWord (fromInteger n) x++-- Errors ----------------------------------------------------------------------++evalPanic :: String -> [String] -> a+evalPanic cxt = panic ("[SBV] " ++ cxt)+++sModAdd :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)+sModAdd _ 0 _ _ = evalPanic "sModAdd" ["0 modulus not allowed"]+sModAdd sym modulus x y =+  case (SBV.svAsInteger x, SBV.svAsInteger y) of+    (Just i, Just j) -> integerLit sym ((i + j) `mod` modulus)+    _                -> pure $ SBV.svPlus x y++sModSub :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)+sModSub _ 0 _ _ = evalPanic "sModSub" ["0 modulus not allowed"]+sModSub sym modulus x y =+  case (SBV.svAsInteger x, SBV.svAsInteger y) of+    (Just i, Just j) -> integerLit sym ((i - j) `mod` modulus)+    _                -> pure $ SBV.svMinus x y++sModNegate :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)+sModNegate _ 0 _ = evalPanic "sModNegate" ["0 modulus not allowed"]+sModNegate sym modulus x =+  case SBV.svAsInteger x of+    Just i -> integerLit sym ((negate i) `mod` modulus)+    _      -> pure $ SBV.svUNeg x++sModMult :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)+sModMult _ 0 _ _ = evalPanic "sModMult" ["0 modulus not allowed"]+sModMult sym modulus x y =+  case (SBV.svAsInteger x, SBV.svAsInteger y) of+    (Just i, Just j) -> integerLit sym ((i * j) `mod` modulus)+    _                -> pure $ SBV.svTimes x y++-- Create a fresh constant and assert that it is the+-- multiplicitive inverse of x; return the constant.+-- Such an inverse must exist under the precondition+-- that the modulus is prime and the input is nonzero.+sModRecip ::+  SBV ->+  Integer {- ^ modulus: must be prime -} ->+  SInteger SBV ->+  SEval SBV (SInteger SBV)+sModRecip _sym 0 _ = panic "sModRecip" ["0 modulus not allowed"]+sModRecip sym m x+  -- If the input is concrete, evaluate the answer+  | Just xi <- svAsInteger x+  = let r = Integer.recipModInteger xi m+     in if r == 0 then raiseError sym DivideByZero else integerLit sym r++  -- If the input is symbolic, create a new symbolic constant+  -- and assert that it is the desired multiplicitive inverse.+  -- Such an inverse will exist under the precondition that+  -- the modulus is prime, and as long as the input is nonzero.+  | otherwise+  = do divZero <- svDivisible sym m x+       assertSideCondition sym (svNot divZero) DivideByZero++       z <- liftIO (freshSInteger_ sym)+       let xz = svTimes x z+       rel <- znEq sym m xz (svInteger KUnbounded 1)+       let range = svAnd (svLessThan (svInteger KUnbounded 0) z)+                         (svLessThan z (svInteger KUnbounded m))+       liftIO (addDefEqn sym (svAnd range (svOr divZero rel)))++       return z++-- | Ceiling (log_2 x)+sLg2 :: SWord SBV -> SEval SBV (SWord SBV)+sLg2 x = pure $ go 0+  where+    lit n = literalSWord (SBV.intSizeOf x) n+    go i | i < SBV.intSizeOf x = SBV.svIte (SBV.svLessEq x (lit (2^i))) (lit (toInteger i)) (go (i + 1))+         | otherwise           = lit (toInteger i)++svDivisible :: SBV -> Integer -> SInteger SBV -> SEval SBV (SBit SBV)+svDivisible sym m x =+  do m' <- integerLit sym m+     z  <- integerLit sym 0+     pure $ SBV.svEqual (SBV.svRem x m') z++signedQuot :: SWord SBV -> SWord SBV -> SWord SBV+signedQuot x y = SBV.svUnsign (SBV.svQuot (SBV.svSign x) (SBV.svSign y))++signedRem :: SWord SBV -> SWord SBV -> SWord SBV+signedRem x y = SBV.svUnsign (SBV.svRem (SBV.svSign x) (SBV.svSign y))++ashr :: SVal -> SVal -> SVal+ashr x idx =+  case SBV.svAsInteger idx of+    Just i  -> SBV.svUnsign (SBV.svShr (SBV.svSign x) (fromInteger i))+    Nothing -> SBV.svUnsign (SBV.svShiftRight (SBV.svSign x) idx)++lshr :: SVal -> SVal -> SVal+lshr x idx =+  case SBV.svAsInteger idx of+    Just i -> SBV.svShr x (fromInteger i)+    Nothing -> SBV.svShiftRight x idx++shl :: SVal -> SVal -> SVal+shl x idx =+  case SBV.svAsInteger idx of+    Just i  -> SBV.svShl x (fromInteger i)+    Nothing -> SBV.svShiftLeft x idx

@@ -0,0 +1,666 @@+-- |+-- Module      :  Cryptol.Backend.What4+-- Copyright   :  (c) 2020 Galois, Inc.+-- License     :  BSD3+-- Maintainer  :  cryptol@galois.com++{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}+module Cryptol.Backend.What4 where+++import qualified Control.Exception as X+import           Control.Concurrent.MVar+import           Control.Monad (foldM,ap,liftM)+import           Control.Monad.IO.Class+import           Data.Bits (bit)+import qualified Data.BitVector.Sized as BV+import           Data.List+import           Data.Map (Map)+import           Data.Set (Set)+import           Data.Text (Text)+import           Data.Parameterized.NatRepr+import           Data.Parameterized.Some++import qualified GHC.Integer.GMP.Internals as Integer++import qualified What4.Interface as W4+import qualified What4.SWord as SW++import qualified Cryptol.Backend.What4.SFloat as FP++import Cryptol.Backend+import Cryptol.Backend.Concrete( BV(..), ppBV )+import Cryptol.Backend.FloatHelpers+import Cryptol.Backend.Monad+   ( Eval(..), EvalError(..), Unsupported(..)+   , delayFill, blackhole, evalSpark+   )+import Cryptol.Utils.Panic+import Cryptol.Utils.PP+++data What4 sym =+  What4+  { w4  :: sym+  , w4defs :: MVar (W4.Pred sym)+  , w4funs :: MVar (What4FunCache sym)+  , w4uninterpWarns :: MVar (Set Text)+  }++type What4FunCache sym = Map Text (SomeSymFn sym)++data SomeSymFn sym =+  forall args ret. SomeSymFn (W4.SymFn sym args ret)++{- | This is the monad used for symbolic evaluation. It adds to+aspects to 'Eval'---'WConn' keeps track of the backend and collects+definitional predicates, and 'W4Eval` adds support for partially+defined values -}+newtype W4Eval sym a = W4Eval { evalPartial :: W4Conn sym (W4Result sym a) }++{- | This layer has the symbolic back-end, and can keep track of definitional+predicates used when working with uninterpreted constants defined+via a property. -}+newtype W4Conn sym a = W4Conn { evalConn :: sym -> Eval a }++-- | The symbolic value we computed.+data W4Result sym a+  = W4Error !EvalError+    -- ^ A malformed value++  | W4Result !(W4.Pred sym) !a+    -- ^ safety predicate and result: the result only makes sense when+    -- the predicate holds.+++--------------------------------------------------------------------------------+-- Moving between the layers++w4Eval :: W4Eval sym a -> sym -> Eval (W4Result sym a)+w4Eval (W4Eval (W4Conn m)) = m++w4Thunk :: Eval (W4Result sym a) -> W4Eval sym a+w4Thunk m = W4Eval (W4Conn \_ -> m)++-- | A value with no context.+doEval :: W4.IsSymExprBuilder sym => Eval a -> W4Conn sym a+doEval m = W4Conn \_sym -> m++-- | A total value.+total :: W4.IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a+total m = W4Eval+  do sym <- getSym+     W4Result (W4.backendPred sym True) <$> m++--------------------------------------------------------------------------------+-- Operations in WConn++instance W4.IsSymExprBuilder sym => Functor (W4Conn sym) where+  fmap = liftM++instance W4.IsSymExprBuilder sym => Applicative (W4Conn sym) where+  pure   = doEval . pure+  (<*>)  = ap++instance W4.IsSymExprBuilder sym => Monad (W4Conn sym) where+  m1 >>= f = W4Conn \sym ->+    do res1 <- evalConn m1 sym+       evalConn (f res1) sym++instance W4.IsSymExprBuilder sym => MonadIO (W4Conn sym) where+  liftIO = doEval . liftIO++-- | Access the symbolic back-end+getSym :: W4Conn sym sym+getSym = W4Conn \sym -> pure sym++-- | Record a definition.+--addDef :: W4.Pred sym -> W4Conn sym ()+--addDef p = W4Conn \_ -> pure W4Defs { w4Defs = p, w4Result = () }++-- | Compute conjunction.+w4And :: W4.IsSymExprBuilder sym =>+         W4.Pred sym -> W4.Pred sym -> W4Conn sym (W4.Pred sym)+w4And p q =+  do sym <- getSym+     liftIO (W4.andPred sym p q)++-- | Compute negation.+w4Not :: W4.IsSymExprBuilder sym => W4.Pred sym -> W4Conn sym (W4.Pred sym)+w4Not p =+  do sym <- getSym+     liftIO (W4.notPred sym p)++-- | Compute if-then-else.+w4ITE :: W4.IsSymExprBuilder sym =>+         W4.Pred sym -> W4.Pred sym -> W4.Pred sym -> W4Conn sym (W4.Pred sym)+w4ITE ifP ifThen ifElse =+  do sym <- getSym+     liftIO (W4.itePred sym ifP ifThen ifElse)++++--------------------------------------------------------------------------------+-- Operations in W4Eval++instance W4.IsSymExprBuilder sym => Functor (W4Eval sym) where+  fmap = liftM++instance W4.IsSymExprBuilder sym => Applicative (W4Eval sym) where+  pure  = total . pure+  (<*>) = ap++instance W4.IsSymExprBuilder sym => Monad (W4Eval sym) where+  m1 >>= f = W4Eval+    do res1 <- evalPartial m1+       case res1 of+         W4Error err -> pure (W4Error err)+         W4Result px x' ->+           do res2 <- evalPartial (f x')+              case res2 of+                W4Result py y ->+                  do pz <- w4And px py+                     pure (W4Result pz y)+                W4Error _ -> pure res2++instance W4.IsSymExprBuilder sym => MonadIO (W4Eval sym) where+  liftIO = total . liftIO+++-- | Add a definitional equation.+-- This will always be asserted when we make queries to the solver.+addDefEqn :: W4.IsSymExprBuilder sym => What4 sym -> W4.Pred sym -> W4Eval sym ()+addDefEqn sym p =+  liftIO (modifyMVar_ (w4defs sym) (W4.andPred (w4 sym) p))++-- | Add s safety condition.+addSafety :: W4.IsSymExprBuilder sym => W4.Pred sym -> W4Eval sym ()+addSafety p = W4Eval (pure (W4Result p ()))++-- | A fully undefined symbolic value+evalError :: W4.IsSymExprBuilder sym => EvalError -> W4Eval sym a+evalError err = W4Eval (pure (W4Error err))++--------------------------------------------------------------------------------+++assertBVDivisor :: W4.IsSymExprBuilder sym => What4 sym -> SW.SWord sym -> W4Eval sym ()+assertBVDivisor sym x =+  do p <- liftIO (SW.bvIsNonzero (w4 sym) x)+     assertSideCondition sym p DivideByZero++assertIntDivisor ::+  W4.IsSymExprBuilder sym => What4 sym -> W4.SymInteger sym -> W4Eval sym ()+assertIntDivisor sym x =+  do p <- liftIO (W4.notPred (w4 sym) =<< W4.intEq (w4 sym) x =<< W4.intLit (w4 sym) 0)+     assertSideCondition sym p DivideByZero++instance W4.IsSymExprBuilder sym => Backend (What4 sym) where+  type SBit (What4 sym)     = W4.Pred sym+  type SWord (What4 sym)    = SW.SWord sym+  type SInteger (What4 sym) = W4.SymInteger sym+  type SFloat (What4 sym)   = FP.SFloat sym+  type SEval (What4 sym)    = W4Eval sym++  raiseError _ = evalError++  assertSideCondition _ cond err+    | Just False <- W4.asConstantPred cond = evalError err+    | otherwise = addSafety cond++  isReady sym m =+    case w4Eval m (w4 sym) of+      Ready _ -> True+      _ -> False++  sDelayFill _ m retry =+    total+    do sym <- getSym+       doEval (w4Thunk <$> delayFill (w4Eval m sym) (w4Eval retry sym))++  sSpark _ m =+    total+    do sym   <- getSym+       doEval (w4Thunk <$> evalSpark (w4Eval m sym))+++  sDeclareHole _ msg =+    total+    do (hole, fill) <- doEval (blackhole msg)+       pure ( w4Thunk hole+            , \m -> total+                    do sym <- getSym+                       doEval (fill (w4Eval m sym))+            )++  mergeEval _sym f c mx my = W4Eval+    do rx <- evalPartial mx+       ry <- evalPartial my+       case (rx, ry) of++         (W4Error err, W4Error _) ->+           pure (W4Error err) -- arbitrarily choose left error to report++         (W4Error _, W4Result p y) ->+           do p' <- w4And p =<< w4Not c+              pure (W4Result p' y)++         (W4Result p x, W4Error _) ->+           do p' <- w4And p c+              pure (W4Result p' x)++         (W4Result px x, W4Result py y) ->+           do zr <- evalPartial (f c x y)+              case zr of+                W4Error err -> pure $ W4Error err+                W4Result pz z ->+                  do p' <- w4And pz =<< w4ITE c px py+                     pure (W4Result p' z)++  wordAsChar _ bv+    | SW.bvWidth bv == 8 = toEnum . fromInteger <$> SW.bvAsUnsignedInteger bv+    | otherwise = Nothing++  wordLen _ bv = SW.bvWidth bv++  bitLit sym b = W4.backendPred (w4 sym) b+  bitAsLit _ v = W4.asConstantPred v++  wordLit sym intw i+    | Just (Some w) <- someNat intw+    = case isPosNat w of+        Nothing -> pure $ SW.ZBV+        Just LeqProof -> SW.DBV <$> liftIO (W4.bvLit (w4 sym) w (BV.mkBV w i))+    | otherwise = panic "what4: wordLit" ["invalid bit width:", show intw ]++  wordAsLit _ v+    | Just x <- SW.bvAsUnsignedInteger v = Just (SW.bvWidth v, x)+    | otherwise = Nothing++  integerLit sym i = liftIO (W4.intLit (w4 sym) i)++  integerAsLit _ v = W4.asInteger v++  ppBit _ v+    | Just b <- W4.asConstantPred v = text $! if b then "True" else "False"+    | otherwise                     = text "?"++  ppWord _ opts v+    | Just x <- SW.bvAsUnsignedInteger v+    = ppBV opts (BV (SW.bvWidth v) x)++    | otherwise = text "[?]"++  ppInteger _ _opts v+    | Just x <- W4.asInteger v = integer x+    | otherwise = text "[?]"++  ppFloat _ _opts _ = text "[?]"++  iteBit sym c x y = liftIO (W4.itePred (w4 sym) c x y)+  iteWord sym c x y = liftIO (SW.bvIte (w4 sym) c x y)+  iteInteger sym c x y = liftIO (W4.intIte (w4 sym) c x y)++  bitEq  sym x y = liftIO (W4.eqPred (w4 sym) x y)+  bitAnd sym x y = liftIO (W4.andPred (w4 sym) x y)+  bitOr  sym x y = liftIO (W4.orPred (w4 sym) x y)+  bitXor sym x y = liftIO (W4.xorPred (w4 sym) x y)+  bitComplement sym x = liftIO (W4.notPred (w4 sym) x)++  wordBit sym bv idx = liftIO (SW.bvAtBE (w4 sym) bv idx)+  wordUpdate sym bv idx b = liftIO (SW.bvSetBE (w4 sym) bv idx b)++  packWord sym bs =+    do z <- wordLit sym (genericLength bs) 0+       let f w (idx,b) = wordUpdate sym w idx b+       foldM f z (zip [0..] bs)++  unpackWord sym bv = liftIO $+    mapM (SW.bvAtBE (w4 sym) bv) [0 .. SW.bvWidth bv-1]++  joinWord sym x y = liftIO $ SW.bvJoin (w4 sym) x y++  splitWord _sym 0 _ bv = pure (SW.ZBV, bv)+  splitWord _sym _ 0 bv = pure (bv, SW.ZBV)+  splitWord sym lw rw bv = liftIO $+    do l <- SW.bvSliceBE (w4 sym) 0 lw bv+       r <- SW.bvSliceBE (w4 sym) lw rw bv+       return (l, r)++  extractWord sym bits idx bv =+    liftIO $ SW.bvSliceLE (w4 sym) idx bits bv++  wordEq                sym x y = liftIO (SW.bvEq  (w4 sym) x y)+  wordLessThan          sym x y = liftIO (SW.bvult (w4 sym) x y)+  wordGreaterThan       sym x y = liftIO (SW.bvugt (w4 sym) x y)+  wordSignedLessThan    sym x y = liftIO (SW.bvslt (w4 sym) x y)++  wordOr  sym x y = liftIO (SW.bvOr  (w4 sym) x y)+  wordAnd sym x y = liftIO (SW.bvAnd (w4 sym) x y)+  wordXor sym x y = liftIO (SW.bvXor (w4 sym) x y)+  wordComplement sym x = liftIO (SW.bvNot (w4 sym) x)++  wordPlus   sym x y = liftIO (SW.bvAdd (w4 sym) x y)+  wordMinus  sym x y = liftIO (SW.bvSub (w4 sym) x y)+  wordMult   sym x y = liftIO (SW.bvMul (w4 sym) x y)+  wordNegate sym x   = liftIO (SW.bvNeg (w4 sym) x)+  wordLg2    sym x   = sLg2 (w4 sym) x+ +  wordDiv sym x y =+     do assertBVDivisor sym y+        liftIO (SW.bvUDiv (w4 sym) x y)+  wordMod sym x y =+     do assertBVDivisor sym y+        liftIO (SW.bvURem (w4 sym) x y)+  wordSignedDiv sym x y =+     do assertBVDivisor sym y+        liftIO (SW.bvSDiv (w4 sym) x y)+  wordSignedMod sym x y =+     do assertBVDivisor sym y+        liftIO (SW.bvSRem (w4 sym) x y)++  wordToInt sym x = liftIO (SW.bvToInteger (w4 sym) x)+  wordFromInt sym width i = liftIO (SW.integerToBV (w4 sym) i width)++  intPlus   sym x y  = liftIO $ W4.intAdd (w4 sym) x y+  intMinus  sym x y  = liftIO $ W4.intSub (w4 sym) x y+  intMult   sym x y  = liftIO $ W4.intMul (w4 sym) x y+  intNegate sym x    = liftIO $ W4.intNeg (w4 sym) x++  -- NB: What4's division operation provides SMTLib's euclidean division,+  -- which doesn't match the round-to-neg-infinity semantics of Cryptol,+  -- so we have to do some work to get the desired semantics.+  intDiv sym x y =+    do assertIntDivisor sym y+       liftIO $ do+         neg <- liftIO (W4.intLt (w4 sym) y =<< W4.intLit (w4 sym) 0)+         case W4.asConstantPred neg of+           Just False -> W4.intDiv (w4 sym) x y+           Just True  ->+              do xneg <- W4.intNeg (w4 sym) x+                 yneg <- W4.intNeg (w4 sym) y+                 W4.intDiv (w4 sym) xneg yneg+           Nothing ->+              do xneg <- W4.intNeg (w4 sym) x+                 yneg <- W4.intNeg (w4 sym) y+                 zneg <- W4.intDiv (w4 sym) xneg yneg+                 z    <- W4.intDiv (w4 sym) x y+                 W4.intIte (w4 sym) neg zneg z++  -- NB: What4's division operation provides SMTLib's euclidean division,+  -- which doesn't match the round-to-neg-infinity semantics of Cryptol,+  -- so we have to do some work to get the desired semantics.+  intMod sym x y =+    do assertIntDivisor sym y+       liftIO $ do+         neg <- liftIO (W4.intLt (w4 sym) y =<< W4.intLit (w4 sym) 0)+         case W4.asConstantPred neg of+           Just False -> W4.intMod (w4 sym) x y+           Just True  ->+              do xneg <- W4.intNeg (w4 sym) x+                 yneg <- W4.intNeg (w4 sym) y+                 W4.intNeg (w4 sym) =<< W4.intMod (w4 sym) xneg yneg+           Nothing ->+              do xneg <- W4.intNeg (w4 sym) x+                 yneg <- W4.intNeg (w4 sym) y+                 z    <- W4.intMod (w4 sym) x y+                 zneg <- W4.intNeg (w4 sym) =<< W4.intMod (w4 sym) xneg yneg+                 W4.intIte (w4 sym) neg zneg z++  intEq sym x y = liftIO $ W4.intEq (w4 sym) x y+  intLessThan sym x y = liftIO $ W4.intLt (w4 sym) x y+  intGreaterThan sym x y = liftIO $ W4.intLt (w4 sym) y x++  -- NB, we don't do reduction here on symbolic values+  intToZn sym m x+    | Just xi <- W4.asInteger x+    = liftIO $ W4.intLit (w4 sym) (xi `mod` m)++    | otherwise+    = pure x++  znToInt _ 0 _ = evalPanic "znToInt" ["0 modulus not allowed"]+  znToInt sym m x = liftIO (W4.intMod (w4 sym) x =<< W4.intLit (w4 sym) m)++  znEq _ 0 _ _ = evalPanic "znEq" ["0 modulus not allowed"]+  znEq sym m x y = liftIO $+     do diff <- W4.intSub (w4 sym) x y+        W4.intDivisible (w4 sym) diff (fromInteger m)++  znPlus   sym m x y = liftIO $ sModAdd (w4 sym) m x y+  znMinus  sym m x y = liftIO $ sModSub (w4 sym) m x y+  znMult   sym m x y = liftIO $ sModMult (w4 sym) m x y+  znNegate sym m x   = liftIO $ sModNegate (w4 sym) m x+  znRecip = sModRecip++  --------------------------------------------------------------++  fpLit sym e p r = liftIO $ FP.fpFromRationalLit (w4 sym) e p r++  fpExactLit sym BF{ bfExpWidth = e, bfPrecWidth = p, bfValue = bf } =+    liftIO (FP.fpFromBinary (w4 sym) e p =<< SW.bvLit (w4 sym) (e+p) (floatToBits e p bf))++  fpEq          sym x y = liftIO $ FP.fpEqIEEE (w4 sym) x y+  fpLessThan    sym x y = liftIO $ FP.fpLtIEEE (w4 sym) x y+  fpGreaterThan sym x y = liftIO $ FP.fpGtIEEE (w4 sym) x y+  fpLogicalEq   sym x y = liftIO $ FP.fpEq (w4 sym) x y++  fpPlus  = fpBinArith FP.fpAdd+  fpMinus = fpBinArith FP.fpSub+  fpMult  = fpBinArith FP.fpMul+  fpDiv   = fpBinArith FP.fpDiv++  fpNeg sym x = liftIO $ FP.fpNeg (w4 sym) x++  fpFromInteger sym e p r x =+    do rm <- fpRoundingMode sym r+       liftIO $ FP.fpFromInteger (w4 sym) e p rm x++  fpToInteger = fpCvtToInteger++sModAdd :: W4.IsSymExprBuilder sym =>+  sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)+sModAdd _sym 0 _ _ = evalPanic "sModAdd" ["0 modulus not allowed"]+sModAdd sym m x y+  | Just xi <- W4.asInteger x+  , Just yi <- W4.asInteger y+  = W4.intLit sym ((xi+yi) `mod` m)++  | otherwise+  = W4.intAdd sym x y++sModSub :: W4.IsSymExprBuilder sym =>+  sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)+sModSub _sym 0 _ _ = evalPanic "sModSub" ["0 modulus not allowed"]+sModSub sym m x y+  | Just xi <- W4.asInteger x+  , Just yi <- W4.asInteger y+  = W4.intLit sym ((xi-yi) `mod` m)++  | otherwise+  = W4.intSub sym x y+++sModMult :: W4.IsSymExprBuilder sym =>+  sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)+sModMult _sym 0 _ _ = evalPanic "sModMult" ["0 modulus not allowed"]+sModMult sym m x y+  | Just xi <- W4.asInteger x+  , Just yi <- W4.asInteger y+  = W4.intLit sym ((xi*yi) `mod` m)++  | otherwise+  = W4.intMul sym x y++sModNegate :: W4.IsSymExprBuilder sym =>+  sym -> Integer -> W4.SymInteger sym -> IO (W4.SymInteger sym)+sModNegate _sym 0 _ = evalPanic "sModMult" ["0 modulus not allowed"]+sModNegate sym m x+  | Just xi <- W4.asInteger x+  = W4.intLit sym ((negate xi) `mod` m)++  | otherwise+  = W4.intNeg sym x+++-- | Try successive powers of 2 to find the first that dominates the input.+--   We could perhaps reduce to using CLZ instead...+sLg2 :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SEval (What4 sym) (SW.SWord sym)+sLg2 sym x = liftIO $ go 0+  where+  w = SW.bvWidth x+  lit n = SW.bvLit sym w (toInteger n)++  go i | toInteger i < w =+       do p <- SW.bvule sym x =<< lit (bit i)+          lazyIte (SW.bvIte sym) p (lit i) (go (i+1))++  -- base case, should only happen when i = w+  go i = lit i++++-- Errors ----------------------------------------------------------------------++evalPanic :: String -> [String] -> a+evalPanic cxt = panic ("[What4] " ++ cxt)++lazyIte ::+  (W4.IsExpr p, Monad m) =>+  (p W4.BaseBoolType -> a -> a -> m a) ->+  p W4.BaseBoolType ->+  m a ->+  m a ->+  m a+lazyIte f c mx my+  | Just b <- W4.asConstantPred c = if b then mx else my+  | otherwise =+      do x <- mx+         y <- my+         f c x y++w4bvShl  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)+w4bvShl sym x y = liftIO $ SW.bvShl sym x y++w4bvLshr  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)+w4bvLshr sym x y = liftIO $ SW.bvLshr sym x y++w4bvAshr :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)+w4bvAshr sym x y = liftIO $ SW.bvAshr sym x y++w4bvRol  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)+w4bvRol sym x y = liftIO $ SW.bvRol sym x y++w4bvRor  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)+w4bvRor sym x y = liftIO $ SW.bvRor sym x y++++fpRoundingMode ::+  W4.IsSymExprBuilder sym =>+  What4 sym -> SWord (What4 sym) -> SEval (What4 sym) W4.RoundingMode+fpRoundingMode sym v =+  case wordAsLit sym v of+    Just (_w,i) ->+      case i of+        0 -> pure W4.RNE+        1 -> pure W4.RNA+        2 -> pure W4.RTP+        3 -> pure W4.RTN+        4 -> pure W4.RTZ+        x -> raiseError sym (BadRoundingMode x)+    _ -> liftIO $ X.throwIO $ UnsupportedSymbolicOp "rounding mode"++fpBinArith ::+  W4.IsSymExprBuilder sym =>+  FP.SFloatBinArith sym ->+  What4 sym ->+  SWord (What4 sym) ->+  SFloat (What4 sym) ->+  SFloat (What4 sym) ->+  SEval (What4 sym) (SFloat (What4 sym))+fpBinArith fun = \sym r x y ->+  do m <- fpRoundingMode sym r+     liftIO (fun (w4 sym) m x y)+++fpCvtToInteger ::+  (W4.IsSymExprBuilder sy, sym ~ What4 sy) =>+  sym -> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)+fpCvtToInteger sym fun r x =+  do grd <- liftIO+              do bad1 <- FP.fpIsInf (w4 sym) x+                 bad2 <- FP.fpIsNaN (w4 sym) x+                 W4.notPred (w4 sym) =<< W4.orPred (w4 sym) bad1 bad2+     assertSideCondition sym grd (BadValue fun)+     rnd  <- fpRoundingMode sym r+     liftIO+       do y <- FP.fpToReal (w4 sym) x+          case rnd of+            W4.RNE -> W4.realRoundEven (w4 sym) y+            W4.RNA -> W4.realRound (w4 sym) y+            W4.RTP -> W4.realCeil (w4 sym) y+            W4.RTN -> W4.realFloor (w4 sym) y+            W4.RTZ -> W4.realTrunc (w4 sym) y+++fpCvtToRational ::+  (W4.IsSymExprBuilder sy, sym ~ What4 sy) =>+  sym -> SFloat sym -> SEval sym (SRational sym)+fpCvtToRational sym fp =+  do grd <- liftIO+            do bad1 <- FP.fpIsInf (w4 sym) fp+               bad2 <- FP.fpIsNaN (w4 sym) fp+               W4.notPred (w4 sym) =<< W4.orPred (w4 sym) bad1 bad2+     assertSideCondition sym grd (BadValue "fpToRational")+     (rel,x,y) <- liftIO (FP.fpToRational (w4 sym) fp)+     addDefEqn sym =<< liftIO (W4.impliesPred (w4 sym) grd rel)+     ratio sym x y++fpCvtFromRational ::+  (W4.IsSymExprBuilder sy, sym ~ What4 sy) =>+  sym -> Integer -> Integer -> SWord sym ->+  SRational sym -> SEval sym (SFloat sym)+fpCvtFromRational sym e p r rat =+  do rnd <- fpRoundingMode sym r+     liftIO (FP.fpFromRational (w4 sym) e p rnd (sNum rat) (sDenom rat))++-- Create a fresh constant and assert that it is the+-- multiplicitive inverse of x; return the constant.+-- Such an inverse must exist under the precondition+-- that the modulus is prime and the input is nonzero.+sModRecip ::+  W4.IsSymExprBuilder sym =>+  What4 sym ->+  Integer ->+  W4.SymInteger sym ->+  W4Eval sym (W4.SymInteger sym)+sModRecip _sym 0 _ = panic "sModRecip" ["0 modulus not allowed"]+sModRecip sym m x+  -- If the input is concrete, evaluate the answer+  | Just xi <- W4.asInteger x+  = let r = Integer.recipModInteger xi m+     in if r == 0 then raiseError sym DivideByZero else integerLit sym r++  -- If the input is symbolic, create a new symbolic constant+  -- and assert that it is the desired multiplicitive inverse.+  -- Such an inverse will exist under the precondition that+  -- the modulus is prime, and as long as the input is nonzero.+  | otherwise+  = do divZero <- liftIO (W4.intDivisible (w4 sym) x (fromInteger m))+       ok <- liftIO (W4.notPred (w4 sym) divZero)+       assertSideCondition sym ok DivideByZero++       z <- liftIO (W4.freshBoundedInt (w4 sym) W4.emptySymbol (Just 1) (Just (m-1)))+       xz <- liftIO (W4.intMul (w4 sym) x z)+       rel <- znEq sym m xz =<< liftIO (W4.intLit (w4 sym) 1)+       addDefEqn sym =<< liftIO (W4.orPred (w4 sym) divZero rel)++       return z

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

@@ -13,7 +13,6 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ParallelListComp #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE Safe #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE ViewPatterns #-} @@ -35,11 +34,11 @@   , forceValue   ) where -import Cryptol.Eval.Backend-import Cryptol.Eval.Concrete( Concrete(..) )+import Cryptol.Backend+import Cryptol.Backend.Concrete( Concrete(..) )+import Cryptol.Backend.Monad import Cryptol.Eval.Generic ( iteValue ) import Cryptol.Eval.Env-import Cryptol.Eval.Monad import Cryptol.Eval.Type import Cryptol.Eval.Value import Cryptol.ModuleSystem.Name@@ -54,6 +53,7 @@ import           Control.Monad import           Data.List import           Data.Maybe+import qualified Data.IntMap.Strict as IntMap import qualified Data.Map.Strict as Map import           Data.Semigroup @@ -63,10 +63,9 @@ type EvalEnv = GenEvalEnv Concrete  type EvalPrims sym =-  ( Backend sym, ?evalPrim :: PrimIdent -> Maybe (GenValue sym) )+  ( Backend sym, ?evalPrim :: PrimIdent -> Maybe (Either Expr (GenValue sym)) ) -type ConcPrims =-  ?evalPrim :: PrimIdent -> Maybe (GenValue Concrete)+type ConcPrims = ?evalPrim :: PrimIdent -> Maybe (Either Expr (GenValue Concrete))  -- Expression Evaluation ------------------------------------------------------- @@ -138,9 +137,10 @@      e' <- eval e      evalSel sym e' sel -  ESet e sel v -> {-# SCC "evalExpr->ESet" #-}+  ESet ty e sel v -> {-# SCC "evalExpr->ESet" #-}     do e' <- eval e-       evalSetSel sym e' sel (eval v)+       let tyv = evalValType (envTypes env) ty+       evalSetSel sym tyv e' sel (eval v)    EIf c t f -> {-# SCC "evalExpr->EIf" #-} do      b <- fromVBit <$> eval c@@ -157,7 +157,7 @@       Nothing  -> do         envdoc <- ppEnv sym defaultPPOpts env         panic "[Eval] evalExpr"-                     ["var `" ++ show (pp n) ++ "` is not defined"+                     ["var `" ++ show (pp n) ++ "` (" ++ show (nameUnique n) ++ ") is not defined"                      , show envdoc                      ] @@ -274,7 +274,7 @@       -- declare a "hole" for each declaration       -- and extend the evaluation environment       holes <- mapM (declHole sym) ds-      let holeEnv = Map.fromList $ [ (nm,h) | (nm,_,h,_) <- holes ]+      let holeEnv = IntMap.fromList $ [ (nameUnique nm, h) | (nm,_,h,_) <- holes ]       let env' = env `mappend` emptyEnv{ envVars = holeEnv }        -- evaluate the declaration bodies, building a new evaluation environment@@ -326,7 +326,7 @@  -- | 'Value' types are non-polymorphic types recursive constructed from --   bits, finite sequences, tuples and records.  Types of this form can---   be implemented rather more efficently than general types because we can+--   be implemented rather more efficiently 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 sym -> Schema -> Bool@@ -525,8 +525,9 @@   case dDefinition d of     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+        Just (Right v) -> pure (bindVarDirect (dName d) v env)+        Just (Left ex) -> bindVar sym (dName d) (evalExpr sym renv ex) env+        Nothing        -> bindVar sym (dName d) (cryNoPrimError sym (dName d)) env      DExpr e -> bindVar sym (dName d) (evalExpr sym renv e) env @@ -584,14 +585,15 @@                               , show vdoc ] {-# SPECIALIZE evalSetSel ::   ConcPrims =>-  Concrete ->+  Concrete -> TValue ->   GenValue Concrete -> Selector -> SEval Concrete (GenValue Concrete) -> SEval Concrete (GenValue Concrete)   #-} evalSetSel :: forall sym.   EvalPrims sym =>   sym ->+  TValue ->   GenValue sym -> Selector -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)-evalSetSel sym e sel v =+evalSetSel sym _tyv e sel v =   case sel of     TupleSel n _  -> setTuple n     RecordSel n _ -> setRecord n@@ -641,25 +643,25 @@ -- name is bound to a list of values, one for each element in the list -- comprehension. data ListEnv sym = ListEnv-  { leVars   :: !(Map.Map Name (Integer -> SEval sym (GenValue sym)))+  { leVars   :: !(IntMap.IntMap (Integer -> SEval sym (GenValue sym)))       -- ^ Bindings whose values vary by position-  , leStatic :: !(Map.Map Name (SEval sym (GenValue sym)))+  , leStatic :: !(IntMap.IntMap (SEval sym (GenValue sym)))       -- ^ Bindings whose values are constant   , leTypes  :: !TypeEnv   }  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)+    { leVars   = IntMap.union (leVars  l)  (leVars  r)+    , leStatic = IntMap.union (leStatic l) (leStatic r)+    , leTypes  = IntMap.union (leTypes l)  (leTypes r)     }  instance Monoid (ListEnv sym) where   mempty = ListEnv-    { leVars   = Map.empty-    , leStatic = Map.empty-    , leTypes  = Map.empty+    { leVars   = IntMap.empty+    , leStatic = IntMap.empty+    , leTypes  = IntMap.empty     }    mappend l r = l <> r@@ -679,7 +681,7 @@ evalListEnv :: ListEnv sym -> Integer -> GenEvalEnv sym evalListEnv (ListEnv vm st tm) i =     let v = fmap ($i) vm-     in EvalEnv{ envVars = Map.union v st+     in EvalEnv{ envVars = IntMap.union v st                , envTypes = tm                } {-# INLINE evalListEnv #-}@@ -690,7 +692,7 @@   (Integer -> SEval sym (GenValue sym)) ->   ListEnv sym ->   ListEnv sym-bindVarList n vs lenv = lenv { leVars = Map.insert n vs (leVars lenv) }+bindVarList n vs lenv = lenv { leVars = IntMap.insert (nameUnique n) vs (leVars lenv) } {-# INLINE bindVarList #-}  -- List Comprehensions ---------------------------------------------------------@@ -776,8 +778,8 @@       -- `leVars` elements of the comprehension environment into `leStatic` elements       -- by selecting out the 0th element.       Inf -> do-        let allvars = Map.union (fmap ($0) (leVars lenv)) (leStatic lenv)-        let lenv' = lenv { leVars   = Map.empty+        let allvars = IntMap.union (fmap ($0) (leVars lenv)) (leStatic lenv)+        let lenv' = lenv { leVars   = IntMap.empty                          , leStatic = allvars                          }         let env   = EvalEnv allvars (leTypes lenv)

@@ -1,30 +0,0 @@--- |--- Module      :  Cryptol.Eval.Arch--- Copyright   :  (c) 2014-2016 Galois, Inc.--- License     :  BSD3--- Maintainer  :  cryptol@galois.com--- Stability   :  provisional--- Portability :  portable------ Architecture-specific parts of the concrete evaluator go here.-{-# LANGUAGE CPP #-}-module Cryptol.Eval.Arch where---- | This is the widest word we can have before gmp will fail to--- allocate and bring down the whole program. According to--- <https://gmplib.org/list-archives/gmp-bugs/2009-July/001538.html>--- the sizes are 2^32-1 for 32-bit, and 2^37 for 64-bit, however--- experiments show that it's somewhere under 2^37 at least on 64-bit--- Mac OS X.-maxBigIntWidth :: Integer-#if i386_HOST_ARCH-maxBigIntWidth = 2^(32 :: Integer) - 0x1-#elif x86_64_HOST_ARCH-maxBigIntWidth = 2^(37 :: Integer) - 0x100-#else--- Because GHC doesn't seem to define a CPP macro that will portably--- tell us the bit width we're compiling for, fall back on a safe choice--- for other architectures. If we care about large words on another--- architecture, we can add a special case for it.-maxBigIntWidth = 2^(32 :: Integer) - 0x1-#endif

@@ -1,705 +0,0 @@-{-# 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)-----

@@ -7,49 +7,57 @@ -- Portability :  portable  {-# LANGUAGE BangPatterns #-}+{-# LANGUAGE BlockArguments #-} {-# 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+  ( module Cryptol.Backend.Concrete+  , Value+  , primTable   , toExpr   ) where -import Control.Monad (join, guard, zipWithM)+import Control.Monad (join, guard, zipWithM, foldM) import Data.Bits (Bits(..))-import Data.Ratio(numerator,denominator)+import Data.Ratio((%),numerator,denominator)+import Data.Word(Word32, Word64) import MonadLib( ChoiceT, findOne, lift ) import qualified LibBF as FP+import qualified Cryptol.F2 as F2  import qualified Data.Map.Strict as Map+import Data.Map(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.Backend+import Cryptol.Backend.Concrete+import Cryptol.Backend.FloatHelpers+import Cryptol.Backend.Monad+ import Cryptol.Eval.Generic hiding (logicShift)-import Cryptol.Eval.Monad import Cryptol.Eval.Type import Cryptol.Eval.Value+import qualified Cryptol.SHA as SHA+import qualified Cryptol.AES as AES+import qualified Cryptol.PrimeEC as PrimeEC 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.Ident (PrimIdent,prelPrim,floatPrim,suiteBPrim,primeECPrim) import Cryptol.Utils.PP import Cryptol.Utils.Logger(logPrint) import Cryptol.Utils.RecordMap +type Value = GenValue Concrete  -- Value to Expression conversion ---------------------------------------------- @@ -131,12 +139,12 @@  -- Primitives ------------------------------------------------------------------ -evalPrim :: PrimIdent -> Maybe Value-evalPrim prim = Map.lookup prim primTable--primTable :: Map.Map PrimIdent Value-primTable = let sym = Concrete in+primTable :: EvalOpts -> Map PrimIdent Value+primTable eOpts = let sym = Concrete in   Map.union (floatPrims sym) $+  Map.union suiteBPrims $+  Map.union primeECPrims $+   Map.fromList $ map (\(n, v) -> (prelPrim n, v))    [ -- Literals@@ -301,6 +309,20 @@                     updatePrim sym updateBack_word updateBack)      -- Misc+  , ("foldl"      , {-# SCC "Prelude::foldl" #-}+                    foldlV sym)++  , ("foldl'"     , {-# SCC "Prelude::foldl'" #-}+                    foldl'V sym)++  , ("deepseq"    , {-# SCC "Prelude::deepseq" #-}+                    tlam $ \_a ->+                    tlam $ \_b ->+                     lam $ \x -> pure $+                     lam $ \y ->+                       do _ <- forceValue =<< x+                          y)+   , ("parmap"     , {-# SCC "Prelude::parmap" #-}                     parmapV sym) @@ -324,15 +346,261 @@                       lam $ \x -> return $                       lam $ \y -> do                          msg <- valueToString sym =<< s-                         EvalOpts { evalPPOpts, evalLogger } <- getEvalOpts+                         let EvalOpts { evalPPOpts, evalLogger } = eOpts                          doc <- ppValue sym evalPPOpts =<< x                          yv <- y                          io $ logPrint evalLogger                              $ if null msg then doc else text msg <+> doc                          return yv)++   , ("pmult",+        ilam $ \u ->+        ilam $ \v ->+          wlam Concrete $ \(BV _ x) -> return $+          wlam Concrete $ \(BV _ y) ->+            let z = if u <= v then+                      F2.pmult (fromInteger (u+1)) x y+                    else+                      F2.pmult (fromInteger (v+1)) y x+             in return . VWord (1+u+v) . pure . WordVal . mkBv (1+u+v) $! z)++   , ("pmod",+        ilam $ \_u ->+        ilam $ \v ->+        wlam Concrete $ \(BV w x) -> return $+        wlam Concrete $ \(BV _ m) ->+          do assertSideCondition sym (m /= 0) DivideByZero+             return . VWord v . pure . WordVal . mkBv v $! F2.pmod (fromInteger w) x m)++  , ("pdiv",+        ilam $ \_u ->+        ilam $ \_v ->+        wlam Concrete $ \(BV w x) -> return $+        wlam Concrete $ \(BV _ m) ->+          do assertSideCondition sym (m /= 0) DivideByZero+             return . VWord w . pure . WordVal . mkBv w $! F2.pdiv (fromInteger w) x m)   ]  +primeECPrims :: Map.Map PrimIdent Value+primeECPrims = Map.fromList $ map (\(n,v) -> (primeECPrim n, v))+  [ ("ec_double", {-# SCC "PrimeEC::ec_double" #-}+       ilam $ \p ->+        lam $ \s ->+          do s' <- toProjectivePoint =<< s+             let r = PrimeEC.ec_double (PrimeEC.primeModulus p) s'+             fromProjectivePoint $! r)++  , ("ec_add_nonzero", {-# SCC "PrimeEC::ec_add_nonzero" #-}+       ilam $ \p ->+        lam $ \s -> pure $+        lam $ \t ->+          do s' <- toProjectivePoint =<< s+             t' <- toProjectivePoint =<< t+             let r = PrimeEC.ec_add_nonzero (PrimeEC.primeModulus p) s' t'+             fromProjectivePoint $! r)++  , ("ec_mult", {-# SCC "PrimeEC::ec_mult" #-}+       ilam $ \p ->+        lam $ \d -> pure $+        lam $ \s ->+          do d' <- fromVInteger <$> d+             s' <- toProjectivePoint =<< s+             let r = PrimeEC.ec_mult (PrimeEC.primeModulus p) d' s'+             fromProjectivePoint $! r)++  , ("ec_twin_mult", {-# SCC "PrimeEC::ec_twin_mult" #-}+       ilam $ \p ->+        lam $ \d0 -> pure $+        lam $ \s  -> pure $+        lam $ \d1 -> pure $+        lam $ \t  ->+          do d0' <- fromVInteger <$> d0+             s'  <- toProjectivePoint =<< s+             d1' <- fromVInteger <$> d1+             t'  <- toProjectivePoint =<< t+             let r = PrimeEC.ec_twin_mult (PrimeEC.primeModulus p) d0' s' d1' t'+             fromProjectivePoint $! r)+  ]++toProjectivePoint :: Value -> Eval PrimeEC.ProjectivePoint+toProjectivePoint v = PrimeEC.ProjectivePoint <$> f "x" <*> f "y" <*> f "z"+  where+   f nm = PrimeEC.integerToBigNat . fromVInteger <$> lookupRecord nm v++fromProjectivePoint :: PrimeEC.ProjectivePoint -> Eval Value+fromProjectivePoint (PrimeEC.ProjectivePoint x y z) =+   pure . VRecord . recordFromFields $ [("x", f x), ("y", f y), ("z", f z)]+  where+   f i = pure (VInteger (PrimeEC.bigNatToInteger i))++++suiteBPrims :: Map.Map PrimIdent Value+suiteBPrims = Map.fromList $ map (\(n, v) -> (suiteBPrim n, v))+  [ ("processSHA2_224", {-# SCC "SuiteB::processSHA2_224" #-}+                      ilam $ \n ->+                       lam $ \xs ->+                         do blks <- enumerateSeqMap n . fromVSeq <$> xs+                            (SHA.SHA256S w0 w1 w2 w3 w4 w5 w6 _) <-+                               foldM (\st blk -> seq st (SHA.processSHA256Block st <$> (toSHA256Block =<< blk)))+                                     SHA.initialSHA224State blks+                            let f :: Word32 -> Eval Value+                                f = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+                                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6])+                            seq zs (pure (VSeq 7 zs)))++  , ("processSHA2_256", {-# SCC "SuiteB::processSHA2_256" #-}+                      ilam $ \n ->+                       lam $ \xs ->+                         do blks <- enumerateSeqMap n . fromVSeq <$> xs+                            (SHA.SHA256S w0 w1 w2 w3 w4 w5 w6 w7) <-+                              foldM (\st blk -> seq st (SHA.processSHA256Block st <$> (toSHA256Block =<< blk)))+                                    SHA.initialSHA256State blks+                            let f :: Word32 -> Eval Value+                                f = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+                                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6,w7])+                            seq zs (pure (VSeq 8 zs)))++  , ("processSHA2_384", {-# SCC "SuiteB::processSHA2_384" #-}+                      ilam $ \n ->+                       lam $ \xs ->+                         do blks <- enumerateSeqMap n . fromVSeq <$> xs+                            (SHA.SHA512S w0 w1 w2 w3 w4 w5 _ _) <-+                              foldM (\st blk -> seq st (SHA.processSHA512Block st <$> (toSHA512Block =<< blk)))+                                    SHA.initialSHA384State blks+                            let f :: Word64 -> Eval Value+                                f = pure . VWord 64 . pure . WordVal . BV 64 . toInteger+                                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5])+                            seq zs (pure (VSeq 6 zs)))++  , ("processSHA2_512", {-# SCC "SuiteB::processSHA2_512" #-}+                      ilam $ \n ->+                       lam $ \xs ->+                         do blks <- enumerateSeqMap n . fromVSeq <$> xs+                            (SHA.SHA512S w0 w1 w2 w3 w4 w5 w6 w7) <-+                              foldM (\st blk -> seq st (SHA.processSHA512Block st <$> (toSHA512Block =<< blk)))+                                    SHA.initialSHA512State blks+                            let f :: Word64 -> Eval Value+                                f = pure . VWord 64 . pure . WordVal . BV 64 . toInteger+                                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6,w7])+                            seq zs (pure (VSeq 8 zs)))++  , ("AESKeyExpand", {-# SCC "SuiteB::AESKeyExpand" #-}+      ilam $ \k ->+       lam $ \seed ->+         do ss <- fromVSeq <$> seed+            let toWord :: Integer -> Eval Word32+                toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESInfKeyExpand" =<< lookupSeqMap ss i)+            let fromWord :: Word32 -> Eval Value+                fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+            kws <- mapM toWord [0 .. k-1]+            let ws = AES.keyExpansionWords k kws+            let len = 4*(k+7)+            pure (VSeq len (finiteSeqMap Concrete (map fromWord ws))))++  , ("AESInvMixColumns", {-# SCC "SuiteB::AESInvMixColumns" #-}+      lam $ \st ->+         do ss <- fromVSeq <$> st+            let toWord :: Integer -> Eval Word32+                toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESInvMixColumns" =<< lookupSeqMap ss i)+            let fromWord :: Word32 -> Eval Value+                fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+            ws <- mapM toWord [0,1,2,3]+            let ws' = AES.invMixColumns ws+            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')++  , ("AESEncRound", {-# SCC "SuiteB::AESEncRound" #-}+      lam $ \st ->+         do ss <- fromVSeq <$> st+            let toWord :: Integer -> Eval Word32+                toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESEncRound" =<< lookupSeqMap ss i)+            let fromWord :: Word32 -> Eval Value+                fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+            ws <- mapM toWord [0,1,2,3]+            let ws' = AES.aesRound ws+            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')++  , ("AESEncFinalRound", {-# SCC "SuiteB::AESEncFinalRound" #-}+      lam $ \st ->+         do ss <- fromVSeq <$> st+            let toWord :: Integer -> Eval Word32+                toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESEncFinalRound" =<< lookupSeqMap ss i)+            let fromWord :: Word32 -> Eval Value+                fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+            ws <- mapM toWord [0,1,2,3]+            let ws' = AES.aesFinalRound ws+            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')++  , ("AESDecRound", {-# SCC "SuiteB::AESDecRound" #-}+      lam $ \st ->+         do ss <- fromVSeq <$> st+            let toWord :: Integer -> Eval Word32+                toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESDecRound" =<< lookupSeqMap ss i)+            let fromWord :: Word32 -> Eval Value+                fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+            ws <- mapM toWord [0,1,2,3]+            let ws' = AES.aesInvRound ws+            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')++  , ("AESDecFinalRound", {-# SCC "SuiteB::AESDecFinalRound" #-}+      lam $ \st ->+         do ss <- fromVSeq <$> st+            let toWord :: Integer -> Eval Word32+                toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESDecFinalRound" =<< lookupSeqMap ss i)+            let fromWord :: Word32 -> Eval Value+                fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+            ws <- mapM toWord [0,1,2,3]+            let ws' = AES.aesInvFinalRound ws+            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')+  ]+++toSHA256Block :: Value -> Eval SHA.SHA256Block+toSHA256Block blk =+  do let ws = fromVSeq blk+     let toWord i = fromInteger . bvVal <$> (fromVWord Concrete "toSHA256Block" =<< lookupSeqMap ws i)+     SHA.SHA256Block <$>+        (toWord 0) <*>+        (toWord 1) <*>+        (toWord 2) <*>+        (toWord 3) <*>+        (toWord 4) <*>+        (toWord 5) <*>+        (toWord 6) <*>+        (toWord 7) <*>+        (toWord 8) <*>+        (toWord 9) <*>+        (toWord 10) <*>+        (toWord 11) <*>+        (toWord 12) <*>+        (toWord 13) <*>+        (toWord 14) <*>+        (toWord 15)+++toSHA512Block :: Value -> Eval SHA.SHA512Block+toSHA512Block blk =+  do let ws = fromVSeq blk+     let toWord i = fromInteger . bvVal <$> (fromVWord Concrete "toSHA512Block" =<< lookupSeqMap ws i)+     SHA.SHA512Block <$>+        (toWord 0) <*>+        (toWord 1) <*>+        (toWord 2) <*>+        (toWord 3) <*>+        (toWord 4) <*>+        (toWord 5) <*>+        (toWord 6) <*>+        (toWord 7) <*>+        (toWord 8) <*>+        (toWord 9) <*>+        (toWord 10) <*>+        (toWord 11) <*>+        (toWord 12) <*>+        (toWord 13) <*>+        (toWord 14) <*>+        (toWord 15)+ --------------------------------------------------------------------------------  sshrV :: Value@@ -527,3 +795,55 @@ updateBack_word (Nat n) _eltTy bs (Right w) val = do   idx <- bvVal <$> asWordVal Concrete w   updateWordValue Concrete bs (n - idx - 1) (fromVBit <$> val)+++floatPrims :: Concrete -> Map PrimIdent Value+floatPrims sym = Map.fromList [ (floatPrim i,v) | (i,v) <- nonInfixTable ]+  where+  (~>) = (,)+  nonInfixTable =+    [ "fpNaN"       ~> ilam \e -> ilam \p ->+                        VFloat BF { bfValue = FP.bfNaN+                                  , bfExpWidth = e, bfPrecWidth = p }++    , "fpPosInf"    ~> ilam \e -> ilam \p ->+                       VFloat BF { bfValue = FP.bfPosInf+                                 , bfExpWidth = e, bfPrecWidth = p }++    , "fpFromBits"  ~> ilam \e -> ilam \p -> wlam sym \bv ->+                       pure $ VFloat $ floatFromBits e p $ bvVal bv++    , "fpToBits"    ~> ilam \e -> ilam \p -> flam \x ->+                       pure $ word sym (e + p)+                            $ floatToBits e p+                            $ bfValue x+    , "=.="         ~> ilam \_ -> ilam \_ -> flam \x -> pure $ flam \y ->+                       pure $ VBit+                            $ bitLit sym+                            $ FP.bfCompare (bfValue x) (bfValue y) == EQ++    , "fpIsFinite"  ~> ilam \_ -> ilam \_ -> flam \x ->+                       pure $ VBit $ bitLit sym $ FP.bfIsFinite $ bfValue x++      -- From Backend class+    , "fpAdd"      ~> fpBinArithV sym fpPlus+    , "fpSub"      ~> fpBinArithV sym fpMinus+    , "fpMul"      ~> fpBinArithV sym fpMult+    , "fpDiv"      ~> fpBinArithV sym fpDiv++    , "fpFromRational" ~>+      ilam \e -> ilam \p -> wlam sym \r -> pure $ lam \x ->+        do rat <- fromVRational <$> x+           VFloat <$> do mode <- fpRoundMode sym r+                         pure $ floatFromRational e p mode+                              $ sNum rat % sDenom rat+    , "fpToRational" ~>+      ilam \_e -> ilam \_p -> flam \fp ->+      case floatToRational "fpToRational" fp of+        Left err -> raiseError sym err+        Right r  -> pure $+                      VRational+                        SRational { sNum = numerator r, sDenom = denominator r }+    ]++

@@ -1,69 +0,0 @@-{-# 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 }-    ]--

@@ -1,252 +0,0 @@-{-# 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)----

@@ -1,390 +0,0 @@--- |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-----