Merge remote-tracking branch 'origin/master' into wip/cs

HACKING.md

@@ -0,0 +1,273 @@
+# Cryptol development
+
+This document explains our standards for developing Cryptol. Our goals
+are to have a development process that:
+
+- Consistently yields reliable software artifacts
+- Quickly incorporates improvements and gets them into user hands
+- Allows new contributors to have an immediate impact
+
+It describes our methods and practices for:
+
+- Testing and continuous integration
+- Organizing, branching, and merging this repository
+- Producing and publishing release artifacts
+- **TODO**: documentation
+- **TODO**: feature/release planning, ticket assignment, etc
+
+This is a living document that is not (and possibly cannot be)
+comprehensive. If something is missing or unclear, or if you have
+suggestions for improving our processes, please file an issue or open
+a pull request.
+
+# Testing
+
+Cryptol primarily uses golden testing on the Cryptol interpreter
+executable. These tests provide the interpreter with input and then
+check the output against an expected output file. We make at least one
+test for each new issue, and keep the accumulated tests in our suite
+as regression tests. The test suite itself is written using the
+`test-framework` library, so it can readily output XML for consumption
+by Jenkins and other CI systems.
+
+## Running tests
+
+To run the test suite, run `make test` from the root of the
+repository. By default, you'll get output on the console for each test
+that fails, either with an explanation for why it failed, or a command
+line you can paste in order to compare the test results against the
+expected output.
+
+The `make test` target invokes the `cryptol-test-runner` executable,
+which is defined in the `/tests/` directory. It is invoked with the
+location of the `cryptol` executable, an output directory, and
+standard `test-framework` command line arguments. The `test` target in
+the `Makefile` provides a template for how to invoke it if you need to
+use advanced parameters.
+
+## Creaing a new test
+
+A test consists at minimum of an `.icry` file, which is a batch-mode
+file for the interpreter, and an `.icry.stdout` file, which contains
+expected output (the "golden" file). As opposed to `.cry` Cryptol
+source files, `.icry` files are run by the interpreter line-by-line as
+if a user has typed each one in and pressed Enter.
+
+Frequently, one creates an `.icry` file by interactively producing a
+desired behavior in the interpreter, and then copying the relevant
+lines of input into the file. Remember that, as with unit testing,
+golden testing will only test the examples you give it, so make sure
+your examples exercise many instances and corner cases of the bug or
+feature.
+
+## Expected test failures
+
+We try to keep as few failing tests as possible in the `master`
+branch. Usually tests for new features are merged into the `master`
+branch in a working state. However if a new bug is reported, we often
+write tests for it before it is fixed, particularly if it will take
+some time to implement the fix.
+
+To prevent confusion over which tests ought and ought not to be
+failing, we add an `.icry.fails` file with an explanatory message
+alongside the `.icry` script that defines the test. This will usually
+reference an issue number, so that anyone running the test suite will
+understand that the reason for the failure is not _their_ changes, but
+rather a known issue that is already being handled.
+
+### Example
+
+Issue #6 was a feature request to add let-binding to the
+interpreter. @dylanmc gave an example of the input he wanted to be
+able to enter, so we created a file `/tests/issues/issue006.icry`
+with the contents:
+
+    :let timesTwo x = x * 2
+    :let double x = x + x
+    :prove \x = timesTwo x == double x
+
+We might not yet know what the expected output should be, so we
+created a dummy file `/tests/issues/issue006.icry.stdout`:
+
+    TODO: once implemented, do something sensible here
+
+Since this is not the output we got when running the `.icry` file,
+this was now a failing test. To prevent confusion, we marked that it
+was expected to fail by putting creating a
+`/tests/issues/issue006.icry.fails` file with a reference to the
+issue:
+
+    In development, see issue #6
+
+As the issue progressed and we refined the design, @acfoltzer
+implemented the `let` feature and came up with some additional
+examples that stretch the legs of the feature further, so we updated
+our `.icry` file, this time loading a supplemental `.cry` file so we
+could test behavior within a module context.
+
+`issue006.cry`:
+
+    f : [32] -> [32]
+    f x = x + 2
+
+    g : [32] -> [32]
+    g x = f x + 1
+
+`issue006.icry`:
+
+    :l issue006.cry
+    g 5
+    let f x = 0
+    g 5
+    (f : [32] -> [32]) 5
+    let f x = if (x : [32]) == 0 then 1 else x * (f (x - 1))
+    f 5
+    let h x = g x
+    h 5
+
+Since the feature was now implemented, we could also produce expected
+output. The easiest way to do this is to interpret the `.icry` file
+using the `-b` flag outside of the test runner, see if the results
+look as expected, and then save those results as the new
+`.icry.stdout`:
+
+    # start with a fresh build
+    % make
+    ...
+    # tests are run from within the directory of the .icry file
+    % cd tests/issues
+    % ../../.cabal-sandbox/bin/cryptol -b issue006.icry
+    Loading module Cryptol
+    Loading module Cryptol
+    Loading module Main
+    0x00000008
+    0x00000008
+    0x00000000
+    0x00000078
+    0x00000008
+
+At this point, it's very important to compare the results you see
+against the results you expect from the inputs in the `.icry`
+script. Since the results looked correct, we piped the same command
+into the matching `.icry.stdout` file and removed the `.icry.fails`
+file:
+
+    % ../../.cabal-sandbox/bin/cryptol -b issue006.icry.stdout
+    % rm issue006.icry.fails
+
+Now the test case `issue006` passes, and will (hopefully!) break if
+the let-binding feature breaks.
+
+# Repository organization and practices
+
+The top-level repository directories are:
+
+- `/cryptol`: Haskell sources for the front-end `cryptol` executable
+  and read-eval-print loop
+- `/docs`: LaTeX and Markdown sources for the Cryptol documentation
+- `/examples`: Cryptol sources implementing several interesting
+  algorithms
+- `/lib`: Cryptol standard library sources
+- `/notebook`: Experimental Cryptol IPython Notebook implementation
+- `/sbv`: Haskell sources for the `sbv` library, derived from Levent
+  Erkok's [`sbv` library](http://leventerkok.github.io/sbv/) (see
+  `/sbv/LICENSE`)
+- `/src`: Haskell sources for the `cryptol` library (the bulk of the
+  implementation)
+- `/tests`: Haskell sources for the Cryptol regression test suite, as
+  well as the Cryptol sources and expected outputs that comprise that
+  suite
+
+## Branching and merging
+
+Within the `GaloisInc/cryptol` repository, we use the
+[git-flow model](http://nvie.com/posts/a-successful-git-branching-model/)
+for branches and merging. Our version has two notable differences:
+
+1. Our `master` (rather than `develop`) branch serves as the cutting
+   edge development branch, and our `release` (rather than `master`)
+   branch is where only pristine, tagged releases are committed.
+
+2. We use `wip` (work-in-progress) branches as a centralized storage
+   place for (usually individual) work in progress. Whereas a
+   `feature` branch is expected to be relatively stable, all bets are
+   off with a `wip` branch. Typically `wip` branches are not actually
+   merged directly into `master`, but instead are rebased into a new
+   branch where the history is cleaned up before merging into
+   `master`.
+
+In short:
+
+- Any substantial new features should be developed on a branch
+  prefixed with `feature/`, and then merged into `master` when
+  completed.
+- When we reach a feature freeze for a release, we create a new branch
+  prefixed with `release/`, for example `release/2.1.0`. When the
+  release is made, we merge those changes back into `master` and make
+  a snapshot commit on the `release` branch.
+- If a critical bug emerges in already-released software, we create a
+  branch off of the relevant `release` branch commit prefixed with
+  `hotfix/2.1.1`. When the hotfix is complete, we merge those changes
+  back into `master` and make a snapshot commit on the `release`
+  branch.
+
+# Releases
+
+We take the stability and reliability of our releases very
+seriously. To that end, our release process is based on principles of
+_automation_, _reproducibility_, and _assurance_ (**TODO**: assurance
+the right word here?).
+
+Automation is essential for reducing the possibility of human
+error. The checklist for a successful release is fairly lengthy, and
+most of the steps need not be done by hand. The real points of
+judgment for an individual release are deciding _when_ the codebase is
+ready to be released, not _how_ it is released.
+
+Reproducibility is essential for fixing bugs both in hotfixes and
+future mainline development. If we cannot reproduce the circumstances
+of a release, we might not be able to reproduce bugs that are reported
+by users of that release. Bugs are often very particular about the
+environment where they will arise, so it is critical to make the
+environment of a release consistent.
+
+Assurance is crucial due to the nature of development done with
+Cryptol. When people use Cryptol to develop the next generations of
+trustworthy systems, we want them to be sure the software was built by
+the Cryptol developers, and was not corrupted during download or
+replaced by a malicious third party. To this end, we sign our releases
+with a [GPG key](http://www.cryptol.net/files/Galois.asc). (**TODO**:
+OMG is this really not https?!)
+
+## Cutting releases
+
+**TODO**: make this relevant to folks outside Galois; right now the
+ build farm exists within the Galois network only, and Galois also
+ controls the release signing key.
+
+The release process is:
+
+1. Make sure the `release/n.n.n` branch is in a release/ready state,
+   with successful build artifacts across all platforms on the
+   relevant Jenkins job. **TODO**: get a Jenkins job running per
+   release branch, rather than just `master`.
+1. Merge the `release/n.n.n` branch into the pristine `release` branch
+   and add a git tag.
+1. Merge the `release/n.n.n` branch back into `master` for future
+   development, and delete the `release/n.n.n` branch.
+1. Run the `cryptol-release` Jenkins job to create a draft
+   release. Specify the build number with the successful artifacts,
+   the textual version tag (e.g., "2.1.0"), whether it's a prerelease
+   (e.g., an alpha), and keep the `DRAFT` option checked.
+1. On the Github page for the draft release and add a changelog
+   (**TODO**: how do we generate changelogs?).
+1. (**TODO**: this part of the process needs to be better and
+   automated) Download the successfully-built artifacts _from
+   Jenkins_, and in the same directory run the script
+   `/release-infrastructure/sign.sh` from the `cryptol-internal.git`
+   repository. You must have the correct GPG key (D3103D7E) for this
+   to work.
+1. Upload the `.sig` files to the draft release on Github.
+1. Publish the release and announce it (**TODO**: compile mailing
+   lists, social media outlets, etc where we should make sure to
+   announce)

Makefile

@@ -2,6 +2,7 @@ UNAME   := $(shell uname -s)
 ARCH    := $(shell uname -m)
 
 TESTS ?= issues regression renamer
+TEST_DIFF ?= meld
 
 CABAL_FLAGS ?= -j
 
@@ -67,11 +68,15 @@ ${CS_BIN}/happy: | ${CS}
 src/GitRev.hs:
 	sh configure
 
-# It would be nice to refine these dependencies some in order to avoid
+
-# unnecessary rebuilds, but for now it's safest to just always cabal
+CRYPTOL_DEPS := \
-# install.
+  $(shell find src cryptol \( -name \*.hs -or -name \*.x -or -name \*.y \) -print) \
-.PHONY: ${CS_BIN}/cryptol
+  $(shell find lib -name \*.cry)
-${CS_BIN}/cryptol: ${CS_BIN}/alex ${CS_BIN}/happy | ${CS}
+
+print-%:
+	@echo $* = $($*)
+
+${CS_BIN}/cryptol: ${CS_BIN}/alex ${CS_BIN}/happy $(CRYPTOL_DEPS) | ${CS}
 	$(CABAL) install .
 
 ${CS_BIN}/cryptolnb: ${CS_BIN}/alex ${CS_BIN}/happy | ${CS}
@@ -127,6 +132,7 @@ test: ${CS_BIN}/cryptol-test-runner
 	  -r output                                                        \
 	  -T --hide-successes                                              \
 	  -T --jxml=$(call adjust-path,$(CURDIR)/results.xml)              \
+	  $(if $(TEST_DIFF),-p $(TEST_DIFF),)                              \
 	)
 
 .PHONY: notebook

README.md

@@ -153,10 +153,12 @@ send email to <cryptol@galois.com>.
 
 ## Developers
 
-If you plan to do development work on the Cryptol interpreter, please
+If you'd like to get involved with Cryptol development, see the list
-make a fork of the GitHub repository and send along pull
+of
-requests. This makes it easier for us to track development and to
+[low-hanging fruit](https://github.com/GaloisInc/cryptol/labels/low-hanging%20fruit). These
-incorporate your changes.
+are tasks which should be straightforward to implement. Make a
+fork of this GitHub repository and send along pull requests, and we'll
+be happy to incorporate your changes.
 
 ### Repository Structure
 

cryptol.cabal

@@ -117,6 +117,7 @@ library
                        Cryptol.Transform.Specialize,
 
                        Cryptol.Eval,
+                       Cryptol.Eval.Arch,
                        Cryptol.Eval.Env,
                        Cryptol.Eval.Error,
                        Cryptol.Eval.Type,

cryptol/REPL/Command.hs

@@ -304,13 +304,13 @@ qcCmd qcMode str =
   prt msg   = io (putStr msg >> hFlush stdout)
   prtLn msg = io (putStrLn msg >> hFlush stdout)
 
-  ppProgress this tot =
+  ppProgress this tot = unlessBatch $
     let percent = show (div (100 * this) tot) ++ "%"
         width   = length percent
         pad     = replicate (totProgressWidth - width) ' '
     in prt (pad ++ percent)
 
-  del n       = prt (replicate n '\BS')
+  del n       = unlessBatch $ prt (replicate n '\BS')
   delTesting  = del (length testingMsg)
   delProgress = del totProgressWidth
 

sbv/Data/SBV.hs

@@ -157,6 +157,8 @@ module Data.SBV (
   , Polynomial(..), crcBV, crc
   -- ** Conditionals: Mergeable values
   , Mergeable(..), ite, iteLazy, sBranch
+  -- ** Conditional symbolic simulation
+  , sAssert, sAssertCont
   -- ** Symbolic equality
   , EqSymbolic(..)
   -- ** Symbolic ordering
@@ -195,6 +197,10 @@ module Data.SBV (
   -- ** Checking constraint vacuity
   , isVacuous, isVacuousWith
 
+  -- * Checking safety
+  -- $safeIntro
+  , safe, safeWith, SExecutable(..)
+
   -- * Proving properties using multiple solvers
   -- $multiIntro
   , proveWithAll, proveWithAny, satWithAll, satWithAny, allSatWithAll, allSatWithAny
@@ -212,7 +218,7 @@ module Data.SBV (
 
   -- ** Inspecting proof results
   -- $resultTypes
-  , ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..)
+  , ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..), SafeResult(..)
 
   -- ** Programmable model extraction
   -- $programmableExtraction
@@ -488,6 +494,46 @@ Note that the function 'sbvAvailableSolvers' will return all the installed solve
 used as the first argument to all these functions, if you simply want to try all available solvers on a machine.
 -}
 
+{- $safeIntro
+
+The 'sAssert' and 'sAssertCont' functions allow users to introduce invariants through-out their code to make sure
+certain properties hold at all times. This is another mechanism to provide further documentation/contract info
+into SBV code. The functions 'safe' and 'safeWith' can then be used to statically discharge these proof assumptions.
+If a violation is found, SBV will print a model showing which inputs lead to the invariant being violated.
+
+Here's a simple example. Let's assume we have a function that does subtraction, and requires it's
+first argument to be larger than the second:
+
+>>> let sub x y = sAssert "sub: x >= y must hold!" (x .>= y) (x - y)
+
+Clearly, this function is not safe, as there's nothing that ensures us to pass a larger second argument.
+If we try to prove a theorem regarding sub, we'll get an exception:
+
+>>> prove $ \x y -> sub x y .>= (0 :: SInt16)
+*** Exception: Assertion failure: "sub: x >= y must hold!"
+  s0 = -32768 :: SInt16
+  s1 = -32767 :: SInt16
+
+Of course, we can use, 'safe' to statically see if such a violation is possible before we attempt a proof:
+
+>>> safe (sub :: SInt8 -> SInt8 -> SInt8)
+Assertion failure: "sub: x >= y must hold!"
+  s0 = -128 :: SInt8
+  s1 = -127 :: SInt8
+
+What happens if we make sure to arrange for this invariant? Consider this version:
+
+>>> let safeSub x y = ite (x .>= y) (sub x y) (sub y x)
+
+Clearly, 'safeSub' must be safe. And indeed, SBV can prove that:
+
+>>> safe (safeSub :: SInt8 -> SInt8 -> SInt8)
+No safety violations detected.
+
+Note how we used 'sub' and 'safeSub' polymorphically. We only need to monomorphise our types when a proof
+attempt is done, as we did in the 'safe' calls.
+-}
+
 {- $optimizeIntro
 Symbolic optimization. A call of the form:
 

sbv/Data/SBV/BitVectors/Data.hs

@@ -32,7 +32,7 @@ module Data.SBV.BitVectors.Data
  , sbvToSW, sbvToSymSW, forceSWArg
  , SBVExpr(..), newExpr
  , cache, Cached, uncache, uncacheAI, HasKind(..)
- , Op(..), NamedSymVar, UnintKind(..), getTableIndex, SBVPgm(..), Symbolic, runSymbolic, runSymbolic', State, getPathCondition, extendPathCondition
+ , Op(..), NamedSymVar, UnintKind(..), getTableIndex, SBVPgm(..), Symbolic, SExecutable(..), runSymbolic, runSymbolic', State, getPathCondition, extendPathCondition
  , inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..)
  , Logic(..), SMTLibLogic(..)
  , getTraceInfo, getConstraints, addConstraint
@@ -57,11 +57,11 @@ import Data.IORef           (IORef, newIORef, modifyIORef, readIORef, writeIORef
 import Data.List            (intercalate, sortBy)
 import Data.Maybe           (isJust, fromJust)
 
-import qualified Data.IntMap   as IMap (IntMap, empty, size, toAscList, lookup, insert, insertWith)
+import qualified Data.IntMap       as IMap (IntMap, empty, size, toAscList, lookup, insert, insertWith)
-import qualified Data.Map      as Map  (Map, empty, toList, size, insert, lookup)
+import qualified Data.Map          as Map  (Map, empty, toList, size, insert, lookup)
-import qualified Data.Set      as Set  (Set, empty, toList, insert)
+import qualified Data.Set          as Set  (Set, empty, toList, insert)
-import qualified Data.Foldable as F    (toList)
+import qualified Data.Foldable     as F    (toList)
-import qualified Data.Sequence as S    (Seq, empty, (|>))
+import qualified Data.Sequence     as S    (Seq, empty, (|>))
 
 import System.Exit           (ExitCode(..))
 import System.Mem.StableName
@@ -1301,6 +1301,9 @@ instance NFData SMTResult where
 instance NFData SMTModel where
   rnf (SMTModel assocs unints uarrs) = rnf assocs `seq` rnf unints `seq` rnf uarrs `seq` ()
 
+instance NFData SMTScript where
+  rnf (SMTScript b m) = rnf b `seq` rnf m `seq` ()
+
 -- | SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the
 -- user can override this choice using the 'useLogic' parameter to the configuration. This is especially handy if
 -- one is experimenting with custom logics that might be supported on new solvers.
@@ -1372,7 +1375,7 @@ data SMTConfig = SMTConfig {
        , timing         :: Bool             -- ^ Print timing information on how long different phases took (construction, solving, etc.)
        , sBranchTimeOut :: Maybe Int        -- ^ How much time to give to the solver for each call of 'sBranch' check. (In seconds. Default: No limit.)
        , timeOut        :: Maybe Int        -- ^ How much time to give to the solver. (In seconds. Default: No limit.)
-       , printBase      :: Int              -- ^ Print integral literals in this base (2, 8, and 10, and 16 are supported.)
+       , printBase      :: Int              -- ^ Print integral literals in this base (2, 8, 10, and 16 are supported.)
        , printRealPrec  :: Int              -- ^ Print algebraic real values with this precision. (SReal, default: 16)
        , solverTweaks   :: [String]         -- ^ Additional lines of script to give to the solver (user specified)
        , satCmd         :: String           -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics.
@@ -1434,3 +1437,100 @@ data SMTSolver = SMTSolver {
 
 instance Show SMTSolver where
    show = show . name
+
+-- | Symbolically executable program fragments. This class is mainly used for 'safe' calls, and is sufficently populated internally to cover most use
+-- cases. Users can extend it as they wish to allow 'safe' checks for SBV programs that return/take types that are user-defined.
+class SExecutable a where
+   sName_ :: a -> Symbolic ()
+   sName  :: [String] -> a -> Symbolic ()
+
+instance NFData a => SExecutable (Symbolic a) where
+   sName_   a = a >>= \r -> rnf r `seq` return ()
+   sName []   = sName_
+   sName xs   = error $ "SBV.SExecutable.sName: Extra unmapped name(s): " ++ intercalate ", " xs
+
+instance NFData a => SExecutable (SBV a) where
+   sName_   v = sName_ (output v)
+   sName xs v = sName xs (output v)
+
+-- Unit output
+instance SExecutable () where
+   sName_   () = sName_   (output ())
+   sName xs () = sName xs (output ())
+
+-- List output
+instance (NFData a, SymWord a) => SExecutable [SBV a] where
+   sName_   vs = sName_   (output vs)
+   sName xs vs = sName xs (output vs)
+
+-- 2 Tuple output
+instance (NFData a, SymWord a, NFData b, SymWord b) => SExecutable (SBV a, SBV b) where
+  sName_ (a, b) = sName_ (output a >> output b)
+  sName _       = sName_
+
+-- 3 Tuple output
+instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c) => SExecutable (SBV a, SBV b, SBV c) where
+  sName_ (a, b, c) = sName_ (output a >> output b >> output c)
+  sName _          = sName_
+
+-- 4 Tuple output
+instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d) => SExecutable (SBV a, SBV b, SBV c, SBV d) where
+  sName_ (a, b, c, d) = sName_ (output a >> output b >> output c >> output c >> output d)
+  sName _             = sName_
+
+-- 5 Tuple output
+instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e) where
+  sName_ (a, b, c, d, e) = sName_ (output a >> output b >> output c >> output d >> output e)
+  sName _                = sName_
+
+-- 6 Tuple output
+instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) where
+  sName_ (a, b, c, d, e, f) = sName_ (output a >> output b >> output c >> output d >> output e >> output f)
+  sName _                   = sName_
+
+-- 7 Tuple output
+instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f, NFData g, SymWord g) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) where
+  sName_ (a, b, c, d, e, f, g) = sName_ (output a >> output b >> output c >> output d >> output e >> output f >> output g)
+  sName _                      = sName_
+
+-- Functions
+instance (SymWord a, SExecutable p) => SExecutable (SBV a -> p) where
+   sName_        k = forall_   >>= \a -> sName_   $ k a
+   sName (s:ss)  k = forall s  >>= \a -> sName ss $ k a
+   sName []      k = sName_ k
+
+-- 2 Tuple input
+instance (SymWord a, SymWord b, SExecutable p) => SExecutable ((SBV a, SBV b) -> p) where
+  sName_        k = forall_  >>= \a -> sName_   $ \b -> k (a, b)
+  sName (s:ss)  k = forall s >>= \a -> sName ss $ \b -> k (a, b)
+  sName []      k = sName_ k
+
+-- 3 Tuple input
+instance (SymWord a, SymWord b, SymWord c, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c) -> p) where
+  sName_       k  = forall_  >>= \a -> sName_   $ \b c -> k (a, b, c)
+  sName (s:ss) k  = forall s >>= \a -> sName ss $ \b c -> k (a, b, c)
+  sName []     k  = sName_ k
+
+-- 4 Tuple input
+instance (SymWord a, SymWord b, SymWord c, SymWord d, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d) -> p) where
+  sName_        k = forall_  >>= \a -> sName_   $ \b c d -> k (a, b, c, d)
+  sName (s:ss)  k = forall s >>= \a -> sName ss $ \b c d -> k (a, b, c, d)
+  sName []      k = sName_ k
+
+-- 5 Tuple input
+instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where
+  sName_        k = forall_  >>= \a -> sName_   $ \b c d e -> k (a, b, c, d, e)
+  sName (s:ss)  k = forall s >>= \a -> sName ss $ \b c d e -> k (a, b, c, d, e)
+  sName []      k = sName_ k
+
+-- 6 Tuple input
+instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where
+  sName_        k = forall_  >>= \a -> sName_   $ \b c d e f -> k (a, b, c, d, e, f)
+  sName (s:ss)  k = forall s >>= \a -> sName ss $ \b c d e f -> k (a, b, c, d, e, f)
+  sName []      k = sName_ k
+
+-- 7 Tuple input
+instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where
+  sName_        k = forall_  >>= \a -> sName_   $ \b c d e f g -> k (a, b, c, d, e, f, g)
+  sName (s:ss)  k = forall s >>= \a -> sName ss $ \b c d e f g -> k (a, b, c, d, e, f, g)
+  sName []      k = sName_ k

sbv/Data/SBV/BitVectors/Model.hs

@@ -22,7 +22,7 @@
 
 module Data.SBV.BitVectors.Model (
     Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), SIntegral
-  , ite, iteLazy, sBranch, sbvTestBit, sbvPopCount, setBitTo, sbvShiftLeft, sbvShiftRight, sbvSignedShiftArithRight
+  , ite, iteLazy, sBranch, sAssert, sAssertCont, sbvTestBit, sbvPopCount, setBitTo, sbvShiftLeft, sbvShiftRight, sbvSignedShiftArithRight
   , sbvRotateLeft, sbvRotateRight, mkUninterpreted
   , allEqual, allDifferent, inRange, sElem, oneIf, blastBE, blastLE, fullAdder, fullMultiplier
   , lsb, msb, genVar, genVar_, forall, forall_, exists, exists_
@@ -43,6 +43,10 @@ import Data.List       (genericLength, genericIndex, unzip4, unzip5, unzip6, unz
 import Data.Maybe      (fromMaybe)
 import Data.Word       (Word8, Word16, Word32, Word64)
 
+import qualified Data.Map as M
+
+import qualified Control.Exception as C
+
 import Test.QuickCheck                           (Testable(..), Arbitrary(..))
 import qualified Test.QuickCheck         as QC   (whenFail)
 import qualified Test.QuickCheck.Monadic as QC   (monadicIO, run)
@@ -52,10 +56,8 @@ import Data.SBV.BitVectors.AlgReals
 import Data.SBV.BitVectors.Data
 import Data.SBV.Utils.Boolean
 
--- The following two imports are only needed because of the doctest expressions we have. Sigh..
+import Data.SBV.Provers.Prover (isSBranchFeasibleInState, isConditionSatisfiable, isVacuous, prove, defaultSMTCfg)
--- It might be a good idea to reorg some of the content to avoid this.
+import Data.SBV.SMT.SMT (SafeResult(..), SatResult(..), ThmResult, getModelDictionary)
-import Data.SBV.Provers.Prover (isSBranchFeasibleInState, isVacuous, prove)
-import Data.SBV.SMT.SMT (ThmResult)
 
 -- | Newer versions of GHC (Starting with 7.8 I think), distinguishes between FiniteBits and Bits classes.
 -- We should really use FiniteBitSize for SBV which would make things better. In the interim, just work
@@ -1136,7 +1138,19 @@ instance SDivisible SInt8 where
   sDivMod  = liftDMod
 
 liftQRem :: (SymWord a, Num a, SDivisible a) => SBV a -> SBV a -> (SBV a, SBV a)
-liftQRem x y = ite (y .== z) (z, x) (qr x y)
+liftQRem x y
+  | isConcreteZero x
+  = (x, x)
+  | isConcreteOne y
+  = (x, z)
+{-------------------------------
+ - N.B. The seemingly innocuous variant when y == -1 only holds if the type is signed;
+ - and also is problematic around the minBound.. So, we refrain from that optimization
+  | isConcreteOnes y
+  = (-x, z)
+--------------------------------}
+  | True
+  = ite (y .== z) (z, x) (qr x y)
   where qr (SBV sgnsz (Left a)) (SBV _ (Left b)) = let (q, r) = sQuotRem a b in (SBV sgnsz (Left q), SBV sgnsz (Left r))
         qr a@(SBV sgnsz _)      b                = (SBV sgnsz (Right (cache (mk Quot))), SBV sgnsz (Right (cache (mk Rem))))
                 where mk o st = do sw1 <- sbvToSW st a
@@ -1146,7 +1160,19 @@ liftQRem x y = ite (y .== z) (z, x) (qr x y)
 
 -- Conversion from quotRem (truncate to 0) to divMod (truncate towards negative infinity)
 liftDMod :: (SymWord a, Num a, SDivisible a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)
-liftDMod x y = ite (y .== z) (z, x) $ ite (signum r .== negate (signum y)) (q-1, r+y) qr
+liftDMod x y
+  | isConcreteZero x
+  = (x, x)
+  | isConcreteOne y
+  = (x, z)
+{-------------------------------
+ - N.B. The seemingly innocuous variant when y == -1 only holds if the type is signed;
+ - and also is problematic around the minBound.. So, we refrain from that optimization
+  | isConcreteOnes y
+  = (-x, z)
+--------------------------------}
+  | True
+  = ite (y .== z) (z, x) $ ite (signum r .== negate (signum y)) (q-1, r+y) qr
    where qr@(q, r) = x `sQuotRem` y
          z = sbvFromInteger (kindOf x) 0
 
@@ -1249,6 +1275,33 @@ sBranch t a b
   | True                  = symbolicMerge False c a b
   where c = reduceInPathCondition t
 
+-- | Symbolic assert. Check that the given boolean condition is always true in the given path.
+-- Otherwise symbolic simulation will stop with a run-time error.
+sAssert :: Mergeable a => String -> SBool -> a -> a
+sAssert msg = sAssertCont msg defCont
+  where defCont _   Nothing   = C.throw (SafeAlwaysFails  msg)
+        defCont cfg (Just md) = C.throw (SafeFailsInModel msg cfg (SMTModel (M.toList md) [] []))
+
+-- | Symbolic assert with a programmable continuation. Check that the given boolean condition is always true in the given path.
+-- Otherwise symbolic simulation will transfer the failing model to the given continuation. The
+-- continuation takes the @SMTConfig@, and a possible model: If it receives @Nothing@, then it means that the condition
+-- fails for all assignments to inputs. Otherwise, it'll receive @Just@ a dictionary that maps the
+-- input variables to the appropriate @CW@ values that exhibit the failure. Note that the continuation
+-- has no option but to display the result in some fashion and call error, due to its restricted type.
+sAssertCont :: Mergeable a => String -> (forall b. SMTConfig -> Maybe (M.Map String CW) -> b) -> SBool -> a -> a
+sAssertCont msg cont t a
+  | Just r <- unliteral t = if r then a else cont defaultSMTCfg Nothing
+  | True                  = symbolicMerge False cond a (die ["SBV.error: Internal-error, cannot happen: Reached false branch in checked s-Assert."])
+  where k     = kindOf t
+        cond  = SBV k $ Right $ cache c
+        die m = error $ intercalate "\n" $ ("Assertion failure: " ++ show msg) : m
+        c st  = do let pc  = getPathCondition st
+                       chk = pc &&& bnot t
+                   mbModel <- isConditionSatisfiable st chk
+                   case mbModel of
+                     Just (r@(SatResult (Satisfiable cfg _))) -> cont cfg $ Just $ getModelDictionary r
+                     _                                        -> return trueSW
+
 -- SBV
 instance SymWord a => Mergeable (SBV a) where
     symbolicMerge force t a b
@@ -1662,16 +1715,16 @@ instance (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymW
                  kg = kindOf (undefined :: g)
                  kh = kindOf (undefined :: h)
                  result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6)
-                          | True = do newUninterpreted st nm (SBVType [kh, kg, kf, ke, kd, kc, kb, ka]) (fst `fmap` mbCgData)
+                           | True = do newUninterpreted st nm (SBVType [kh, kg, kf, ke, kd, kc, kb, ka]) (fst `fmap` mbCgData)
-                                      sw0 <- sbvToSW st arg0
+                                       sw0 <- sbvToSW st arg0
-                                      sw1 <- sbvToSW st arg1
+                                       sw1 <- sbvToSW st arg1
-                                      sw2 <- sbvToSW st arg2
+                                       sw2 <- sbvToSW st arg2
-                                      sw3 <- sbvToSW st arg3
+                                       sw3 <- sbvToSW st arg3
-                                      sw4 <- sbvToSW st arg4
+                                       sw4 <- sbvToSW st arg4
-                                      sw5 <- sbvToSW st arg5
+                                       sw5 <- sbvToSW st arg5
-                                      sw6 <- sbvToSW st arg6
+                                       sw6 <- sbvToSW st arg6
-                                      mapM_ forceSWArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6]
+                                       mapM_ forceSWArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6]
-                                      newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5, sw6]
+                                       newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5, sw6]
 
 -- Uncurried functions of two arguments
 instance (SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) where

sbv/Data/SBV/Bridge/Boolector.hs

@@ -21,8 +21,8 @@
 module Data.SBV.Bridge.Boolector (
   -- * Boolector specific interface
   sbvCurrentSolver
-  -- ** Proving and checking satisfiability
+  -- ** Proving, checking satisfiability, and safety
-  , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable
+  , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable
   -- ** Optimization routines
   , optimize, minimize, maximize
   -- * Non-Boolector specific SBV interface
@@ -30,7 +30,7 @@ module Data.SBV.Bridge.Boolector (
   , module Data.SBV
   ) where
 
-import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)
+import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)
 
 -- | Current solver instance, pointing to cvc4.
 sbvCurrentSolver :: SMTConfig
@@ -48,6 +48,12 @@ sat :: Provable a
     -> IO SatResult     -- ^ Response of the SMT Solver, containing the model if found
 sat = satWith sbvCurrentSolver
 
+-- | Check safety, i.e., prove that all 'sAssert' conditions are statically true in all paths
+safe :: SExecutable a
+     => a               -- ^ Program to check the safety of
+     -> IO SafeResult   -- ^ Response of the SMT solver, containing the unsafe model if found
+safe = safeWith sbvCurrentSolver
+
 -- | Find all satisfying solutions, using the CVC4 SMT solver
 allSat :: Provable a
        => a                -- ^ Property to check

sbv/Data/SBV/Bridge/CVC4.hs

@@ -21,8 +21,8 @@
 module Data.SBV.Bridge.CVC4 (
   -- * CVC4 specific interface
   sbvCurrentSolver
-  -- ** Proving and checking satisfiability
+  -- ** Proving, checking satisfiability, and safety
-  , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable
+  , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable
   -- ** Optimization routines
   , optimize, minimize, maximize
   -- * Non-CVC4 specific SBV interface
@@ -30,7 +30,7 @@ module Data.SBV.Bridge.CVC4 (
   , module Data.SBV
   ) where
 
-import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)
+import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)
 
 -- | Current solver instance, pointing to cvc4.
 sbvCurrentSolver :: SMTConfig
@@ -48,6 +48,12 @@ sat :: Provable a
     -> IO SatResult     -- ^ Response of the SMT Solver, containing the model if found
 sat = satWith sbvCurrentSolver
 
+-- | Check safety, i.e., prove that all 'sAssert' conditions are statically true in all paths
+safe :: SExecutable a
+     => a               -- ^ Program to check the safety of
+     -> IO SafeResult   -- ^ Response of the SMT solver, containing the unsafe model if found
+safe = safeWith sbvCurrentSolver
+
 -- | Find all satisfying solutions, using the CVC4 SMT solver
 allSat :: Provable a
        => a                -- ^ Property to check

sbv/Data/SBV/Bridge/MathSAT.hs

@@ -21,8 +21,8 @@
 module Data.SBV.Bridge.MathSAT (
   -- * MathSAT specific interface
   sbvCurrentSolver
-  -- ** Proving and checking satisfiability
+  -- ** Proving, checking satisfiability, and safety
-  , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable
+  , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable
   -- ** Optimization routines
   , optimize, minimize, maximize
   -- * Non-MathSAT specific SBV interface
@@ -30,7 +30,7 @@ module Data.SBV.Bridge.MathSAT (
   , module Data.SBV
   ) where
 
-import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)
+import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)
 
 -- | Current solver instance, pointing to cvc4.
 sbvCurrentSolver :: SMTConfig
@@ -48,6 +48,12 @@ sat :: Provable a
     -> IO SatResult     -- ^ Response of the SMT Solver, containing the model if found
 sat = satWith sbvCurrentSolver
 
+-- | Check safety, i.e., prove that all 'sAssert' conditions are statically true in all paths
+safe :: SExecutable a
+     => a               -- ^ Program to check the safety of
+     -> IO SafeResult   -- ^ Response of the SMT solver, containing the unsafe model if found
+safe = safeWith sbvCurrentSolver
+
 -- | Find all satisfying solutions, using the CVC4 SMT solver
 allSat :: Provable a
        => a                -- ^ Property to check

sbv/Data/SBV/Bridge/Yices.hs

@@ -21,8 +21,8 @@
 module Data.SBV.Bridge.Yices (
   -- * Yices specific interface
   sbvCurrentSolver
-  -- ** Proving and checking satisfiability
+  -- ** Proving, checking satisfiability, and safety
-  , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable
+  , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable
   -- ** Optimization routines
   , optimize, minimize, maximize
   -- * Non-Yices specific SBV interface
@@ -30,7 +30,7 @@ module Data.SBV.Bridge.Yices (
   , module Data.SBV
   ) where
 
-import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)
+import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)
 
 -- | Current solver instance, pointing to yices.
 sbvCurrentSolver :: SMTConfig
@@ -48,6 +48,12 @@ sat :: Provable a
     -> IO SatResult     -- ^ Response of the SMT Solver, containing the model if found
 sat = satWith sbvCurrentSolver
 
+-- | Check safety, i.e., prove that all 'sAssert' conditions are statically true in all paths
+safe :: SExecutable a
+     => a               -- ^ Program to check the safety of
+     -> IO SafeResult   -- ^ Response of the SMT solver, containing the unsafe model if found
+safe = safeWith sbvCurrentSolver
+
 -- | Find all satisfying solutions, using the Yices SMT solver
 allSat :: Provable a
        => a                -- ^ Property to check

sbv/Data/SBV/Bridge/Z3.hs

@@ -21,8 +21,8 @@
 module Data.SBV.Bridge.Z3 (
   -- * Z3 specific interface
   sbvCurrentSolver
-  -- ** Proving and checking satisfiability
+  -- ** Proving, checking satisfiability, and safety
-  , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable
+  , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable
   -- ** Optimization routines
   , optimize, minimize, maximize
   -- * Non-Z3 specific SBV interface
@@ -30,7 +30,7 @@ module Data.SBV.Bridge.Z3 (
   , module Data.SBV
   ) where
 
-import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)
+import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)
 
 -- | Current solver instance, pointing to z3.
 sbvCurrentSolver :: SMTConfig
@@ -48,6 +48,12 @@ sat :: Provable a
     -> IO SatResult     -- ^ Response of the SMT Solver, containing the model if found
 sat = satWith sbvCurrentSolver
 
+-- | Check safety, i.e., prove that all 'sAssert' conditions are statically true in all paths
+safe :: SExecutable a
+     => a               -- ^ Program to check the safety of
+     -> IO SafeResult   -- ^ Response of the SMT solver, containing the unsafe model if found
+safe = safeWith sbvCurrentSolver
+
 -- | Find all satisfying solutions, using the Z3 SMT solver
 allSat :: Provable a
        => a                -- ^ Property to check

sbv/Data/SBV/Compilers/C.hs

@@ -487,10 +487,21 @@ ppExpr cfg consts (SBVApp op opArgs) = p op (map (showSW cfg consts) opArgs)
                   , (Equal, "=="), (NotEqual, "!="), (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<="), (GreaterEq, ">=")
                   , (And, "&"), (Or, "|"), (XOr, "^")
                   ]
+        uninterpret "squareRoot" as = let f = case kindOf (head opArgs) of
+                                               KFloat  -> text "sqrtf"
+                                               KDouble -> text "sqrt"
+                                               k       -> die $ "squareRoot on unexpected kind: " ++ show k
+                                      in f <> parens (fsep (punctuate comma as))
+        uninterpret "fusedMA"    as = let f = case kindOf (head opArgs) of
+                                                KFloat  -> text "fmaf"
+                                                KDouble -> text "fma"
+                                                k       -> die $ "fusedMA on unexpected kind: " ++ show k
+                                      in f <> parens (fsep (punctuate comma as))
+        uninterpret s []            = text "/* Uninterpreted constant */" <+> text s
+        uninterpret s as            = text "/* Uninterpreted function */" <+> text s <> parens (fsep (punctuate comma as))
         p (ArrRead _)       _  = tbd "User specified arrays (ArrRead)"
         p (ArrEq _ _)       _  = tbd "User specified arrays (ArrEq)"
-        p (Uninterpreted s) [] = text "/* Uninterpreted constant */" <+> text s
+        p (Uninterpreted s) as = uninterpret s as
-        p (Uninterpreted s) as = text "/* Uninterpreted function */" <+> text s <> parens (fsep (punctuate comma as))
         p (Extract i j) [a]    = extract i j (head opArgs) a
         p Join [a, b]          = join (let (s1 : s2 : _) = opArgs in (s1, s2, a, b))
         p (Rol i) [a]          = rotate True  i a (head opArgs)

sbv/Data/SBV/Provers/Boolector.hs

@@ -79,7 +79,7 @@ extractMap inps _modelMap solverLines =
         -- Boolector outputs in a non-parenthesized way; and also puts x's for don't care bits:
         cvt :: String -> String
         cvt s = case words s of
-                  [var, val] -> "((" ++ var ++ " #b" ++ map tr val ++ "))"
+                  [_, val, var] -> "((" ++ var ++ " #b" ++ map tr val ++ "))"
-                  _          -> s -- good-luck..
+                  _             -> s -- good-luck..
           where tr 'x' = '0'
                 tr x   = x

sbv/Data/SBV/Provers/Prover.hs

@@ -13,13 +13,15 @@
 {-# LANGUAGE FlexibleInstances    #-}
 {-# LANGUAGE OverlappingInstances #-}
 {-# LANGUAGE BangPatterns         #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
 
 module Data.SBV.Provers.Prover (
          SMTSolver(..), SMTConfig(..), Predicate, Provable(..)
-       , ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..)
+       , ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..), SafeResult(..)
        , isSatisfiable, isSatisfiableWith, isTheorem, isTheoremWith
        , prove, proveWith
        , sat, satWith
+       , safe, safeWith
        , allSat, allSatWith
        , isVacuous, isVacuousWith
        , SatModel(..), Modelable(..), displayModels, extractModels
@@ -27,18 +29,21 @@ module Data.SBV.Provers.Prover (
        , boolector, cvc4, yices, z3, mathSAT, defaultSMTCfg
        , compileToSMTLib, generateSMTBenchmarks
        , isSBranchFeasibleInState
+       , isConditionSatisfiable
        ) where
 
 import Control.Monad       (when, unless)
 import Control.Monad.Trans (liftIO)
 import Data.List           (intercalate)
-import Data.Maybe          (mapMaybe, fromMaybe)
+import Data.Maybe          (mapMaybe, fromMaybe, isJust)
 import System.FilePath     (addExtension, splitExtension)
 import System.Time         (getClockTime)
 import System.IO.Unsafe    (unsafeInterleaveIO)
 
 import qualified Data.Set as Set (Set, toList)
 
+import qualified Control.Exception as C
+
 import Data.SBV.BitVectors.Data
 import Data.SBV.SMT.SMT
 import Data.SBV.SMT.SMTLib
@@ -232,6 +237,10 @@ prove = proveWith defaultSMTCfg
 sat :: Provable a => a -> IO SatResult
 sat = satWith defaultSMTCfg
 
+-- | Check if a given definition is safe; i.e., if all 'sAssert' conditions can be proven to hold.
+safe :: SExecutable a => a -> IO SafeResult
+safe = safeWith defaultSMTCfg
+
 -- | Return all satisfying assignments for a predicate, equivalent to @'allSatWith' 'defaultSMTCfg'@.
 -- Satisfying assignments are constructed lazily, so they will be available as returned by the solver
 -- and on demand.
@@ -326,6 +335,19 @@ satWith :: Provable a => SMTConfig -> a -> IO SatResult
 satWith config a = simulate cvt config True [] a >>= callSolver True "Checking Satisfiability.." SatResult config
   where cvt = if useSMTLib2 config then toSMTLib2 else toSMTLib1
 
+-- | Check if a given definition is safe using the given solver configuration; i.e., if all 'sAssert' conditions can be proven to hold.
+safeWith :: SExecutable a => SMTConfig -> a -> IO SafeResult
+safeWith config a = C.catchJust choose checkSafe return
+  where checkSafe = do let msg = when (verbose config) . putStrLn . ("** " ++)
+                           isTiming = timing config
+                       msg "Starting safety checking symbolic simulation.."
+                       res <- timeIf isTiming "problem construction" $ runSymbolic (False, Just config) $ sName_ a >>= output
+                       msg $ "Generated symbolic trace:\n" ++ show res
+                       return SafeNeverFails
+        choose e@(SafeNeverFails{})   = Just e
+        choose e@(SafeAlwaysFails{})  = Just e
+        choose e@(SafeFailsInModel{}) = Just e
+
 -- | Determine if the constraints are vacuous using the given SMT-solver
 isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool
 isVacuousWith config a = do
@@ -443,17 +465,35 @@ isSBranchFeasibleInState st branch cond = do
        let cfg = let pickedConfig = fromMaybe defaultSMTCfg (getSBranchRunConfig st)
                  in pickedConfig { timeOut = sBranchTimeOut pickedConfig }
            msg = when (verbose cfg) . putStrLn . ("** " ++)
-       sw <- sbvToSW st cond
+       check <- internalSATCheck cfg st cond ("sBranch: Checking " ++ show branch ++ " feasibility")
-       () <- forceSWArg sw
-       Result ki tr uic is cs ts as uis ax asgn cstr _ <- liftIO $ extractSymbolicSimulationState st
-       let -- Construct the corresponding sat-checker for the branch. Note that we need to
-           -- forget about the quantifiers and just use an "exist", as we're looking for a
-           -- point-satisfiability check here; whatever the original program was.
-           pgm = Result ki tr uic [(EX, n) | (_, n) <- is] cs ts as uis ax asgn cstr [sw]
-           cvt = if useSMTLib2 cfg then toSMTLib2 else toSMTLib1
-       check <- runProofOn cvt cfg True [] pgm >>= callSolver True ("sBranch: Checking " ++ show branch ++ " feasibility") SatResult cfg
        res <- case check of
                 SatResult (Unsatisfiable _) -> return False
                 _                           -> return True   -- No risks, even if it timed-our or anything else, we say it's feasible
        msg $ "sBranch: Conclusion: " ++ if res then "Feasible" else "Unfeasible"
        return res
+
+-- | Check if a boolean condition is satisfiable in the current state. If so, it returns such a satisfying assignment
+isConditionSatisfiable :: State -> SBool -> IO (Maybe SatResult)
+isConditionSatisfiable st cond = do
+       let cfg  = fromMaybe defaultSMTCfg (getSBranchRunConfig st)
+           msg  = when (verbose cfg) . putStrLn . ("** " ++)
+       check <- internalSATCheck cfg st cond "sAssert: Checking satisfiability"
+       res <- case check of
+                r@(SatResult (Satisfiable{})) -> return $ Just r
+                SatResult (Unsatisfiable _)   -> return Nothing
+                _                             -> error $ "sAssert: Unexpected external result: " ++ show check
+       msg $ "sAssert: Conclusion: " ++ if isJust res then "Satisfiable" else "Unsatisfiable"
+       return res
+
+-- | Check the boolean SAT of an internal condition in the current execution state
+internalSATCheck :: SMTConfig -> State -> SBool -> String -> IO SatResult
+internalSATCheck cfg st cond msg = do
+   sw <- sbvToSW st cond
+   () <- forceSWArg sw
+   Result ki tr uic is cs ts as uis ax asgn cstr _ <- liftIO $ extractSymbolicSimulationState st
+   let -- Construct the corresponding sat-checker for the branch. Note that we need to
+       -- forget about the quantifiers and just use an "exist", as we're looking for a
+       -- point-satisfiability check here; whatever the original program was.
+       pgm = Result ki tr uic [(EX, n) | (_, n) <- is] cs ts as uis ax asgn cstr [sw]
+       cvt = if useSMTLib2 cfg then toSMTLib2 else toSMTLib1
+   runProofOn cvt cfg True [] pgm >>= callSolver True msg SatResult cfg

sbv/Data/SBV/SMT/SMT.hs

@@ -10,12 +10,14 @@
 -----------------------------------------------------------------------------
 
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DeriveDataTypeable  #-}
 
 module Data.SBV.SMT.SMT where
 
 import qualified Control.Exception as C
 
 import Control.Concurrent (newEmptyMVar, takeMVar, putMVar, forkIO)
+import Control.DeepSeq    (NFData(..))
 import Control.Monad      (when, zipWithM)
 import Data.Char          (isSpace)
 import Data.Int           (Int8, Int16, Int32, Int64)
@@ -27,6 +29,7 @@ import System.Exit        (ExitCode(..))
 import System.IO          (hClose, hFlush, hPutStr, hGetContents, hGetLine)
 
 import qualified Data.Map as M
+import Data.Typeable
 
 import Data.SBV.BitVectors.AlgReals
 import Data.SBV.BitVectors.Data
@@ -84,6 +87,22 @@ instance Show AllSatResult where
                            Satisfiable{} -> True
                            _             -> False
 
+-- | The result of an 'sAssert' call
+data SafeResult = SafeNeverFails
+                | SafeAlwaysFails  String
+                | SafeFailsInModel String SMTConfig SMTModel
+                deriving Typeable
+
+-- | The show instance for SafeResult. Note that this is for display purposes only,
+-- user programs are likely to pattern match on the output and proceed accordingly.
+instance Show SafeResult where
+   show SafeNeverFails              = "No safety violations detected."
+   show (SafeAlwaysFails s)         = intercalate "\n" ["Assertion failure: " ++ show s, "*** Fails in all assignments to inputs"]
+   show (SafeFailsInModel s cfg md) = intercalate "\n" ["Assertion failure: " ++ show s, showModel cfg md]
+
+-- | If a 'prove' or 'sat' call comes accross an 'sAssert' call that fails, they will throw a 'SafeResult' as an exception.
+instance C.Exception SafeResult
+
 -- | Instances of 'SatModel' can be automatically extracted from models returned by the
 -- solvers. The idea is that the sbv infrastructure provides a stream of 'CW''s (constant-words)
 -- coming from the solver, and the type @a@ is interpreted based on these constants. Many typical
@@ -352,11 +371,15 @@ pipeProcess cfg execName opts script cleanErrs = do
         let nm = show (name (solver cfg))
         mbExecPath <- findExecutable execName
         case mbExecPath of
-          Nothing -> return $ Left $ "Unable to locate executable for " ++ nm
+          Nothing       -> return $ Left $ "Unable to locate executable for " ++ nm
-                                   ++ "\nExecutable specified: " ++ show execName
+                                        ++ "\nExecutable specified: " ++ show execName
-          Just execPath -> do (ec, contents, allErrors) <- runSolver cfg execPath opts script
+          Just execPath ->
-                              let errors = dropWhile isSpace (cleanErrs allErrors)
+                   do solverResult <- dispatchSolver cfg execPath opts script
-                              case (null errors, xformExitCode (solver cfg) ec) of
+                      case solverResult of
+                        Left s                          -> return $ Left s
+                        Right (ec, contents, allErrors) ->
+                          let errors = dropWhile isSpace (cleanErrs allErrors)
+                          in case (null errors, xformExitCode (solver cfg) ec) of
                                 (True, ExitSuccess)  -> return $ Right $ map clean (filter (not . null) (lines contents))
                                 (_, ec')             -> let errors' = if null errors
                                                                       then (if null (dropWhile isSpace contents)
@@ -400,6 +423,14 @@ standardSolver config script cleanErrs failure success = do
       Left e   -> return $ failure (lines e)
       Right xs -> return $ success (mergeSExpr xs)
 
+-- | Wrap the solver call to protect against any exceptions
+dispatchSolver :: SMTConfig -> FilePath -> [String] -> SMTScript -> IO (Either String (ExitCode, String, String))
+dispatchSolver cfg execPath opts script = rnf script `seq` (Right `fmap` runSolver cfg execPath opts script) `C.catch` (\(e::C.SomeException) -> bad (show e))
+  where bad s = return $ Left $ unlines [ "Failed to start the external solver: " ++ s
+                                        , "Make sure you can start " ++ show execPath
+                                        , "from the command line without issues."
+                                        ]
+
 -- | A variant of 'readProcessWithExitCode'; except it knows about continuation strings
 -- and can speak SMT-Lib2 (just a little).
 runSolver :: SMTConfig -> FilePath -> [String] -> SMTScript -> IO (ExitCode, String, String)

sbv/Data/SBV/SMT/SMTLib1.hs

@@ -210,11 +210,14 @@ cvtExp (SBVApp (ArrRead i) [a]) = "(select array_" ++ show i ++ " " ++ show a ++
 cvtExp (SBVApp (Uninterpreted nm) [])   = "uninterpreted_" ++ nm
 cvtExp (SBVApp (Uninterpreted nm) args) = "(uninterpreted_" ++ nm ++ " " ++ unwords (map show args) ++ ")"
 cvtExp inp@(SBVApp op args)
+  | allBools, Just f <- lookup op boolComps
+  = f (map show args)
   | Just f <- lookup op smtOpTable
-  = f (any hasSign args) (all isBoolean args) (map show args)
+  = f (any hasSign args) allBools (map show args)
   | True
   = error $ "SBV.SMT.SMTLib1.cvtExp: impossible happened; can't translate: " ++ show inp
-  where lift2  o _ _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")"
+  where allBools = all isBoolean args
+        lift2  o _ _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")"
         lift2  o _ _ sbvs   = error $ "SBV.SMTLib1.cvtExp.lift2: Unexpected arguments: "   ++ show (o, sbvs)
         lift2S oU oS sgn isB sbvs
           | sgn
@@ -240,6 +243,18 @@ cvtExp inp@(SBVApp op args)
           | True
           = "(= " ++ lift2 "bvcomp" sgn isB sbvs ++ " bv1[1])"
         neq sgn isB sbvs = "(not " ++ eq sgn isB sbvs ++ ")"
+        -- Boolean comparisons.. SMTLib's bool type doesn't do comparisons, but Haskell does.. Sigh
+        boolComps      = [ (LessThan,      blt)
+                         , (GreaterThan,   blt . swp)
+                         , (LessEq,        blq)
+                         , (GreaterEq,     blq . swp)
+                         ]
+                       where blt [x, y] = "(and (not " ++ x ++ ") " ++ y ++ ")"
+                             blt xs     = error $ "SBV.SMT.SMTLib1.boolComps.blt: Impossible happened, incorrect arity (expected 2): " ++ show xs
+                             blq [x, y] = "(or (not " ++ x ++ ") " ++ y ++ ")"
+                             blq xs     = error $ "SBV.SMT.SMTLib1.boolComps.blq: Impossible happened, incorrect arity (expected 2): " ++ show xs
+                             swp [x, y] = [y, x]
+                             swp xs     = error $ "SBV.SMT.SMTLib1.boolComps.swp: Impossible happened, incorrect arity (expected 2): " ++ show xs
         smtOpTable = [ (Plus,          lift2   "bvadd")
                      , (Minus,         lift2   "bvsub")
                      , (Times,         lift2   "bvmul")

sbv/Data/SBV/SMT/SMTLib2.hs

@@ -442,6 +442,8 @@ cvtExp rm skolemMap tableMap expr@(SBVApp _ arguments) = sh expr
         sh inp@(SBVApp op args)
           | intOp, Just f <- lookup op smtOpIntTable
           = f True (map ssw args)
+          | boolOp, Just f <- lookup op boolComps
+          = f (map ssw args)
           | bvOp, Just f <- lookup op smtOpBVTable
           = f (any hasSign args) (map ssw args)
           | realOp, Just f <- lookup op smtOpRealTable
@@ -464,6 +466,18 @@ cvtExp rm skolemMap tableMap expr@(SBVApp _ arguments) = sh expr
                                 , (LessEq,        lift2S  "bvule" "bvsle")
                                 , (GreaterEq,     lift2S  "bvuge" "bvsge")
                                 ]
+                -- Boolean comparisons.. SMTLib's bool type doesn't do comparisons, but Haskell does.. Sigh
+                boolComps      = [ (LessThan,      blt)
+                                 , (GreaterThan,   blt . swp)
+                                 , (LessEq,        blq)
+                                 , (GreaterEq,     blq . swp)
+                                 ]
+                               where blt [x, y] = "(and (not " ++ x ++ ") " ++ y ++ ")"
+                                     blt xs     = error $ "SBV.SMT.SMTLib2.boolComps.blt: Impossible happened, incorrect arity (expected 2): " ++ show xs
+                                     blq [x, y] = "(or (not " ++ x ++ ") " ++ y ++ ")"
+                                     blq xs     = error $ "SBV.SMT.SMTLib2.boolComps.blq: Impossible happened, incorrect arity (expected 2): " ++ show xs
+                                     swp [x, y] = [y, x]
+                                     swp xs     = error $ "SBV.SMT.SMTLib2.boolComps.swp: Impossible happened, incorrect arity (expected 2): " ++ show xs
                 smtOpRealTable =  smtIntRealShared
                                ++ [ (Quot,        lift2WM "/")
                                   ]

src/Cryptol/Eval.hs

@@ -43,7 +43,7 @@ evalExpr env expr = case expr of
 
   ECon con -> evalECon con
 
-  EList es ty -> evalList env es (evalType env ty)
+  EList es ty -> VSeq (isTBit (evalType env ty)) (map (evalExpr env) es)
 
   ETuple es -> VTuple (map eval es)
 
@@ -208,15 +208,3 @@ evalMatch env m = case m of
   -- they are typechecked that way; the read environment to evalDecl is the same
   -- as the environment to bind a new name in.
   Let d -> [evalDecl env d env]
-
-
--- Lists -----------------------------------------------------------------------
-
--- | Evaluate a list literal, optionally packing them into a word.
-evalList :: EvalEnv -> [Expr] -> TValue -> Value
-evalList env es ty = toPackedSeq w ty (map (evalExpr env) es)
-  where
-  w = TValue $ tNum $ length es
-
-
-

src/Cryptol/Eval/Arch.hs

@@ -0,0 +1,26 @@
+-- |
+-- Module      :  $Header$
+-- Copyright   :  (c) 2014 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
+#error unknown max width for gmp on this architecture
+#endif

src/Cryptol/Eval/Error.hs

@@ -30,6 +30,7 @@ data EvalError
   = InvalidIndex Integer
   | TypeCannotBeDemoted Type
   | DivideByZero
+  | WordTooWide Integer
   | UserError String
     deriving (Typeable,Show)
 
@@ -38,6 +39,8 @@ instance PP EvalError where
     InvalidIndex i -> text "invalid sequence index:" <+> integer i
     TypeCannotBeDemoted t -> text "type cannot be demoted:" <+> pp t
     DivideByZero -> text "division by 0"
+    WordTooWide w ->
+      text "word too wide for memory:" <+> integer w <+> text "bits"
     UserError x -> text "Run-time error:" <+> text x
 
 instance X.Exception EvalError
@@ -54,6 +57,12 @@ typeCannotBeDemoted t = X.throw (TypeCannotBeDemoted t)
 divideByZero :: a
 divideByZero = X.throw DivideByZero
 
+-- | 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)
+
 -- | For `error`
 cryUserError :: String -> a
 cryUserError msg = X.throw (UserError msg)

src/Cryptol/Eval/Value.hs

@@ -9,10 +9,12 @@
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE Safe #-}
 
 module Cryptol.Eval.Value where
 
+import qualified Cryptol.Eval.Arch as Arch
 import Cryptol.Eval.Error
 import Cryptol.Prims.Syntax (ECon(..))
 import Cryptol.TypeCheck.AST
@@ -77,6 +79,10 @@ finTValue tval =
 data BV = BV !Integer !Integer -- ^ width, value
                                -- The value may contain junk bits
 
+-- | Smart constructor for 'BV's that checks for the width limit
+mkBv :: Integer -> Integer -> BV
+mkBv w i | w >= Arch.maxBigIntWidth = wordTooWide w
+         | otherwise = BV w i
 
 -- | Generic value type, parameterized by bit and word types.
 data GenValue b w
@@ -183,35 +189,45 @@ ppWord opts (BV width i)
 
 -- Big-endian Words ------------------------------------------------------------
 
+class BitWord b w where
+
+  -- | 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 :: [b] -> w
+
+  -- | 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 :: w -> [b]
+
+
 mask :: Integer  -- ^ Bit-width
      -> Integer  -- ^ Value
      -> Integer  -- ^ Masked result
-mask w i = i .&. ((1 `shiftL` fromInteger w) - 1)
+mask w i | w >= Arch.maxBigIntWidth = wordTooWide w
+         | otherwise                = i .&. ((1 `shiftL` fromInteger w) - 1)
 
 
--- NOTE this assumes that the sequence of bits is big-endian and finite, so the
+instance BitWord Bool BV where
--- first element of the list will be the most significant bit.
-packWord :: [Bool] -> BV
-packWord bits = BV (toInteger w) a
-  where
-  w = length bits
-  a = foldl set 0 (zip [w - 1, w - 2 .. 0] bits)
-  set acc (n,b) | b         = setBit acc n
-                | otherwise = acc
 
--- NOTE this produces a list of bits that represent a big-endian word, so the
+  packWord bits = BV (toInteger w) a
--- most significant bit is the first element of the list.
+    where
-unpackWord :: BV -> [Bool]
+      w = case length bits of
-unpackWord (BV w a) = [ testBit a n | n <- [w' - 1, w' - 2 .. 0] ]
+            len | toInteger len >= Arch.maxBigIntWidth -> wordTooWide (toInteger len)
-  where
+                | otherwise                  -> len
-  w' = fromInteger w
+      a = foldl set 0 (zip [w - 1, w - 2 .. 0] bits)
+      set acc (n,b) | b         = setBit acc n
+                    | otherwise = acc
+
+  unpackWord (BV w a) = [ testBit a n | n <- [w' - 1, w' - 2 .. 0] ]
+    where
+      w' = fromInteger w
 
 
 -- Value Constructors ----------------------------------------------------------
 
 -- | Create a packed word of n bits.
 word :: Integer -> Integer -> Value
-word n i = VWord (BV n (mask n i))
+word n i = VWord (mkBv n (mask n i))
 
 lam :: (GenValue b w -> GenValue b w) -> GenValue b w
 lam  = VFun
@@ -265,7 +281,7 @@ fromVBit val = case val of
   _      -> evalPanic "fromVBit" ["not a Bit"]
 
 -- | Extract a sequence.
-fromSeq :: Value -> [Value]
+fromSeq :: BitWord b w => GenValue b w -> [GenValue b w]
 fromSeq val = case val of
   VSeq _ vs  -> vs
   VWord bv   -> map VBit (unpackWord bv)
@@ -277,12 +293,11 @@ fromStr = map (toEnum . fromInteger . fromWord) . fromSeq
 
 -- | Extract a packed word.
 -- Note that this does not clean-up any junk bits in the word.
-fromVWord :: Value -> BV
+fromVWord :: BitWord b w => GenValue b w -> w
 fromVWord val = case val of
   VWord bv                -> bv -- this should always mask
   VSeq isWord bs | isWord -> packWord (map fromVBit bs)
-  _                       -> evalPanic "fromVWord"
+  _                       -> evalPanic "fromVWord" ["not a word"]
-                              ["not a word", show $ ppValue defaultPPOpts val]
 
 vWordLen :: Value -> Maybe Integer
 vWordLen val = case val of

src/Cryptol/ModuleSystem/Renamer.hs

@@ -36,49 +36,80 @@ import qualified Data.Map as Map
 
 -- Errors ----------------------------------------------------------------------
 
--- XXX make these located
 data RenamerError
   = MultipleSyms (Located QName) [NameOrigin]
     -- ^ Multiple imported symbols contain this name
-  | UnboundSym (Located QName)
+
-    -- ^ Symbol is not bound to any definition
+  | UnboundExpr (Located QName)
+    -- ^ Expression name is not bound to any definition
+
+  | UnboundType (Located QName)
+    -- ^ Type name is not bound to any definition
+
   | OverlappingSyms [NameOrigin]
     -- ^ An environment has produced multiple overlapping symbols
 
-  | BuiltInTypeDecl QName
+  | ExpectedValue (Located QName)
-    -- ^ This is a built-in type name, and user may not shadow it.
+    -- ^ When a value is expected from the naming environment, but one or more
+    -- types exist instead.
+
+  | ExpectedType (Located QName)
+    -- ^ When a type is missing from the naming environment, but one or more
+    -- values exist with the same name.
     deriving (Show)
 
 instance PP RenamerError where
   ppPrec _ e = case e of
 
     MultipleSyms lqn qns ->
-      hang (text "[error] Multiple definitions for symbol:" <+> pp lqn)
+      hang (text "[error] at" <+> pp (srcRange lqn))
-         4 (vcat (map pp qns))
+         4 $ (text "Multiple definitions for symbol:" <+> pp (thing lqn))
+          $$ vcat (map pp qns)
 
-    UnboundSym lqn ->
+    UnboundExpr lqn ->
-      text "[error] unbound symbol:" <+> pp lqn
+      hang (text "[error] at" <+> pp (srcRange lqn))
+         4 (text "Value not in scope:" <+> pp (thing lqn))
+
+    UnboundType lqn ->
+      hang (text "[error] at" <+> pp (srcRange lqn))
+         4 (text "Type not in scope:" <+> pp (thing lqn))
 
-    -- XXX these really need to be located
     OverlappingSyms qns ->
-      hang (text "[error] Overlapping symbols defined:")
+      hang (text "[error]")
-         4 (vcat (map pp qns))
+         4 $ text "Overlapping symbols defined:"
+          $$ vcat (map pp qns)
 
-    BuiltInTypeDecl q ->
+    ExpectedValue lqn ->
-      hang (text "[error] Built-in type name may not be shadowed:")
+      hang (text "[error] at" <+> pp (srcRange lqn))
-         4 (pp q)
+         4 (fsep [ text "Expected a value named", quotes (pp (thing lqn))
+                 , text "but found a type instead"
+                 , text "Did you mean `(" <> pp (thing lqn) <> text")?" ])
+
+    ExpectedType lqn ->
+      hang (text "[error] at" <+> pp (srcRange lqn))
+         4 (fsep [ text "Expected a type named", quotes (pp (thing lqn))
+                 , text "but found a value instead" ])
 
 -- Warnings --------------------------------------------------------------------
 
 data RenamerWarning
-  = SymbolShadowed [NameOrigin] [NameOrigin]
+  = SymbolShadowed NameOrigin [NameOrigin]
     deriving (Show)
 
 instance PP RenamerWarning where
-  ppPrec _ (SymbolShadowed original new) =
+  ppPrec _ (SymbolShadowed new originals) =
-    hang (text "[warning] This binding for" <+> commaSep (map pp original)
+    hang (text "[warning] at" <+> loc)
-              <+> text "shadows the existing binding")
+       4 $ fsep [ text "This binding for" <+> sym
-       4 (vcat (map pp new))
+                , text "shadows the existing binding" <> plural <+> text "from" ]
+        $$ vcat (map pp originals)
+
+    where
+    plural | length originals > 1 = char 's'
+           | otherwise            = empty
+
+    (loc,sym) = case new of
+                  Local lqn   -> (pp (srcRange lqn), pp (thing lqn))
+                  Imported qn -> (empty, pp qn)
 
 
 -- Renaming Monad --------------------------------------------------------------
@@ -158,37 +189,35 @@ shadowNames names m = RenameM $ do
   let ro' = ro { roNames = env `shadowing` roNames ro }
   local ro' (unRenameM m)
 
--- | Generate warnings when the the left environment shadows things defined in
+-- | Generate warnings when the left environment shadows things defined in
 -- the right.  Additionally, generate errors when two names overlap in the
 -- left environment.
 checkEnv :: NamingEnv -> NamingEnv -> Out
-checkEnv l r = Map.foldlWithKey (step False neExprs) mempty (neExprs l)
+checkEnv l r = Map.foldlWithKey (step neExprs) mempty (neExprs l)
-     `mappend` Map.foldlWithKey (step True neTypes) mempty (neTypes l)
+     `mappend` Map.foldlWithKey (step neTypes) mempty (neTypes l)
   where
 
-  step isType prj acc k ns = acc `mappend` Out
+  step prj acc k ns = acc `mappend` mempty
     { oWarnings = case Map.lookup k (prj r) of
         Nothing -> []
-        Just os -> [SymbolShadowed (map origin os) (map origin ns)]
+        Just os -> [SymbolShadowed (origin (head ns)) (map origin os)]
     , oErrors   = containsOverlap ns
-    } `mappend`
+    }
-      checkValidDecl isType k
-
-  containsOverlap ns = case ns of
-    [_] -> []
-    []  -> panic "Renamer" ["Invalid naming environment"]
-    _   -> [OverlappingSyms (map origin ns)]
-
-  checkValidDecl True nm@(QName _ (Name "width")) =
-    mempty { oErrors = [BuiltInTypeDecl nm] }
-  checkValidDecl _ _ = mempty
 
+-- | Check the RHS of a single name rewrite for conflicting sources.
+containsOverlap :: HasQName a => [a] -> [RenamerError]
+containsOverlap [_] = []
+containsOverlap []  = panic "Renamer" ["Invalid naming environment"]
+containsOverlap ns  = [OverlappingSyms (map origin ns)]
 
 -- | Throw errors for any names that overlap in a rewrite environment.
 checkNamingEnv :: NamingEnv -> ([RenamerError],[RenamerWarning])
-checkNamingEnv env = (oErrors out, oWarnings out)
+checkNamingEnv env = (out, [])
   where
-  out = checkEnv env mempty
+  out    = Map.foldr check outTys (neExprs env)
+  outTys = Map.foldr check mempty (neTypes env)
+
+  check ns acc = containsOverlap ns ++ acc
 
 
 -- Renaming --------------------------------------------------------------------
@@ -258,7 +287,13 @@ renameExpr qn = do
          return qn
     Nothing   ->
       do n <- located qn
-         record (UnboundSym n)
+
+         case Map.lookup qn (neTypes (roNames ro)) of
+           -- types existed with the name of the value expected
+           Just _ -> record (ExpectedValue n)
+
+           -- the value is just missing
+           Nothing -> record (UnboundExpr n)
          return qn
 
 renameType :: QName -> RenameM QName
@@ -273,7 +308,15 @@ renameType qn = do
          return qn
     Nothing   ->
       do n <- located qn
-         record (UnboundSym n)
+
+         case Map.lookup qn (neExprs (roNames ro)) of
+
+           -- values exist with the same name, so throw a different error
+           Just _ -> record (ExpectedType n)
+
+           -- no terms with the same name, so the type is just unbound
+           Nothing -> record (UnboundType n)
+
          return qn
 
 -- | Rename a schema, assuming that none of its type variables are already in
@@ -377,6 +420,7 @@ instance Rename Expr where
     ESel e' s     -> ESel    <$> rename e' <*> pure s
     EList es      -> EList   <$> rename es
     EFromTo s n e'-> EFromTo <$> rename s  <*> rename n  <*> rename e'
+    EInfFrom a b  -> EInfFrom<$> rename a  <*> rename b
     EComp e' bs   -> do bs' <- mapM renameMatch bs
                         shadowNames (namingEnv bs')
                             (EComp <$> rename e' <*> pure bs')

src/Cryptol/Parser.y

@@ -510,8 +510,8 @@ list_expr                      :: { Expr }
   | expr ',' expr '..'            {% eFromTo $4 $1 (Just $3) Nothing    }
   | expr ',' expr '..' expr       {% eFromTo $4 $1 (Just $3) (Just $5)  }
 
-  | expr '...'                    { EApp (ECon ECInfFrom) $1 }
+  | expr '...'                    { EInfFrom $1 Nothing                 }
-  | expr ',' expr '...'           { EApp (EApp (ECon ECInfFromThen) $1) $3 }
+  | expr ',' expr '...'           { EInfFrom $1 (Just $3)               }
 
 
 list_alts                      :: { [[Match]] }

src/Cryptol/Parser/AST.hs

@@ -253,6 +253,7 @@ data Expr     = EVar QName                      -- ^ @ x @
               | ESel Expr Selector              -- ^ @ e.l @
               | EList [Expr]                    -- ^ @ [1,2,3] @
               | EFromTo Type (Maybe Type) (Maybe Type)   -- ^ @[1, 5 ..  117 ] @
+              | EInfFrom Expr (Maybe Expr)      -- ^ @ [1, 3 ...] @
               | EComp Expr [[Match]]            -- ^ @ [ 1 | x <- xs ] @
               | EApp Expr Expr                  -- ^ @ f x @
               | EAppT Expr [TypeInst]           -- ^ @ f `{x = 8}, f`{8} @
@@ -665,6 +666,8 @@ instance PP Expr where
       EFromTo e1 e2 e3 -> brackets (pp e1 <> step <+> text ".." <+> end)
         where step = maybe empty (\e -> comma <+> pp e) e2
               end  = maybe empty pp e3
+      EInfFrom e1 e2 -> brackets (pp e1 <> step <+> text "...")
+        where step = maybe empty (\e -> comma <+> pp e) e2
       EComp e mss   -> brackets (pp e <+> vcat (map arm mss))
         where arm ms = text "|" <+> commaSep (map pp ms)
       ETypeVal t    -> text "`" <> ppPrec 5 t     -- XXX
@@ -893,6 +896,7 @@ instance NoPos Expr where
       ESel x y      -> ESel     (noPos x) y
       EList x       -> EList    (noPos x)
       EFromTo x y z -> EFromTo  (noPos x) (noPos y) (noPos z)
+      EInfFrom x y  -> EInfFrom (noPos x) (noPos y)
       EComp x y     -> EComp    (noPos x) (noPos y)
       EApp  x y     -> EApp     (noPos x) (noPos y)
       EAppT x y     -> EAppT    (noPos x) (noPos y)

src/Cryptol/Parser/LexerUtils.hs

@@ -15,6 +15,7 @@ import Cryptol.Utils.PP
 import Cryptol.Utils.Panic
 
 import Data.Char(toLower)
+import Data.List(foldl')
 import Data.Word(Word8)
 import Codec.Binary.UTF8.String(encodeChar)
 
@@ -156,8 +157,7 @@ emitS t cfg p s z  = emit (t s) cfg p s z
 numToken :: Integer -> String -> TokenT
 numToken rad ds = Num (toVal ds) (fromInteger rad) (length ds)
   where
-  toVal = sum . zipWith (\n x -> rad^n * x) [0 :: Integer ..]
+  toVal = foldl' (\x c -> rad * x + toDig c) 0
-              . map toDig . reverse
   toDig = if rad == 16 then fromHexDigit else fromDecDigit
 
 fromDecDigit   :: Char -> Integer

src/Cryptol/Parser/Names.hs

@@ -84,6 +84,7 @@ namesE expr =
     ESel e _      -> namesE e
     EList es      -> Set.unions (map namesE es)
     EFromTo _ _ _ -> Set.empty
+    EInfFrom e e' -> Set.union (namesE e) (maybe Set.empty namesE e')
     EComp e arms  -> let (dss,uss) = unzip (map namesArm arms)
                      in Set.union (boundNames (concat dss) (namesE e))
                                   (Set.unions uss)
@@ -194,6 +195,7 @@ tnamesE expr =
     EList es      -> Set.unions (map tnamesE es)
     EFromTo a b c -> Set.union (tnamesT a)
                      (Set.union (maybe Set.empty tnamesT b) (maybe Set.empty tnamesT c))
+    EInfFrom e e' -> Set.union (tnamesE e) (maybe Set.empty tnamesE e')
     EComp e mss   -> Set.union (tnamesE e) (Set.unions (map tnamesM (concat mss)))
     EApp e1 e2    -> Set.union (tnamesE e1) (tnamesE e2)
     EAppT e fs    -> Set.union (tnamesE e) (Set.unions (map tnamesTI fs))

src/Cryptol/Parser/NoPat.hs

@@ -25,6 +25,7 @@ import           Control.Applicative(Applicative(..),(<$>))
 import           Data.Maybe(maybeToList)
 import           Data.Either(partitionEithers)
 import qualified Data.Map as Map
+import           Data.Traversable(traverse)
 
 
 class RemovePatterns t where
@@ -147,6 +148,7 @@ noPatE expr =
     ESel e s      -> ESel    <$> noPatE e <*> return s
     EList es      -> EList   <$> mapM noPatE es
     EFromTo {}    -> return expr
+    EInfFrom e e' -> EInfFrom <$> noPatE e <*> traverse noPatE e'
     EComp e mss   -> EComp  <$> noPatE e <*> mapM noPatArm mss
     EApp e1 e2    -> EApp   <$> noPatE e1 <*> noPatE e2
     EAppT e ts    -> EAppT  <$> noPatE e <*> return ts

src/Cryptol/Prims/Eval.hs

@@ -20,10 +20,11 @@ module Cryptol.Prims.Eval where
 import Cryptol.Prims.Syntax (ECon(..))
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),fromNat,genLog, nMul)
+import qualified Cryptol.Eval.Arch as Arch
 import Cryptol.Eval.Error
-import Cryptol.Testing.Random (randomValue)
-import Cryptol.Eval.Value
 import Cryptol.Eval.Type(evalTF)
+import Cryptol.Eval.Value
+import Cryptol.Testing.Random (randomValue)
 import Cryptol.Utils.Panic (panic)
 
 import Data.List (sortBy,transpose,genericTake,genericReplicate,genericSplitAt,genericIndex)
@@ -208,7 +209,7 @@ ecDemoteV :: Value
 ecDemoteV = tlam $ \valT ->
             tlam $ \bitT ->
             case (numTValue valT, numTValue bitT) of
-              (Nat v, Nat bs) -> VWord (BV bs v)
+              (Nat v, Nat bs) -> VWord (mkBv bs v)
               _ -> evalPanic "Cryptol.Eval.Prim.evalConst"
                        ["Unexpected Inf in constant."
                        , show valT
@@ -310,7 +311,7 @@ arithBinary op = loop
     | Just (len,a) <- isTSeq ty = case numTValue len of
 
       -- words and finite sequences
-      Nat w | isTBit a  -> VWord (BV w (op w (fromWord l) (fromWord r)))
+      Nat w | isTBit a  -> VWord (mkBv w (op w (fromWord l) (fromWord r)))
             | otherwise -> VSeq False (zipWith (loop a) (fromSeq l) (fromSeq r))
 
       -- streams
@@ -341,7 +342,7 @@ arithUnary op = loop
     | Just (len,a) <- isTSeq ty = case numTValue len of
 
       -- words and finite sequences
-      Nat w | isTBit a  -> VWord (BV w (op (fromWord x)))
+      Nat w | isTBit a  -> VWord (mkBv w (op (fromWord x)))
             | otherwise -> VSeq False (map (loop a) (fromSeq x))
 
       Inf -> toStream (map (loop a) (fromSeq x))
@@ -539,7 +540,7 @@ logicBinary op = loop
       case numTValue len of
 
          -- words or finite sequences
-         Nat w | isTBit aty -> VWord (BV w (op (fromWord l) (fromWord r)))
+         Nat w | isTBit aty -> VWord (mkBv w (op (fromWord l) (fromWord r)))
                | otherwise -> VSeq False (zipWith (loop aty) (fromSeq l)
                                                              (fromSeq r))
 
@@ -573,7 +574,7 @@ logicUnary op = loop
       case numTValue len of
 
          -- words or finite sequences
-         Nat w | isTBit ety -> VWord (BV w (op (fromWord val)))
+         Nat w | isTBit ety -> VWord (mkBv w (op (fromWord val)))
                | otherwise -> VSeq False (map (loop ety) (fromSeq val))
 
          -- streams
@@ -722,6 +723,8 @@ fromThenV  =
   tlamN $ \ bits  ->
   tlamN $ \ len   ->
     case (first, next, len, bits) of
+      (_         , _        , _       , Nat bits')
+        | bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
       (Nat first', Nat next', Nat len', Nat bits') ->
         let nums = enumFromThen first' next'
          in VSeq False (genericTake len' (map (VWord . BV bits') nums))
@@ -734,7 +737,8 @@ fromToV  =
   tlamN $ \ lst   ->
   tlamN $ \ bits  ->
     case (first, lst, bits) of
-
+      (_         , _       , Nat bits')
+        | bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
       (Nat first', Nat lst', Nat bits') ->
         let nums = enumFromThenTo first' (first' + 1) lst'
             len  = 1 + (lst' - first')
@@ -751,7 +755,8 @@ fromThenToV  =
   tlamN $ \ bits  ->
   tlamN $ \ len   ->
     case (first, next, lst, len, bits) of
-
+      (_         , _        , _       , _       , Nat bits')
+        | bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
       (Nat first', Nat next', Nat lst', Nat len', Nat bits') ->
         let nums = enumFromThenTo first' next' lst'
          in VSeq False (genericTake len' (map (VWord . BV bits') nums))

src/Cryptol/Symbolic/Prims.hs

@@ -97,7 +97,7 @@ evalECon econ =
       VFun $ \xs ->
       VFun $ \y ->
         case xs of
-          VWord x -> VWord (SBV.sbvShiftLeft x (fromWord y))
+          VWord x -> VWord (SBV.sbvShiftLeft x (fromVWord y))
           _ -> selectV shl y
             where
               shl :: Integer -> Value
@@ -114,7 +114,7 @@ evalECon econ =
       VFun $ \xs ->
       VFun $ \y ->
         case xs of
-          VWord x -> VWord (SBV.sbvShiftRight x (fromWord y))
+          VWord x -> VWord (SBV.sbvShiftRight x (fromVWord y))
           _ -> selectV shr y
             where
               shr :: Integer -> Value
@@ -131,7 +131,7 @@ evalECon econ =
       VFun $ \xs ->
       VFun $ \y ->
         case xs of
-          VWord x -> VWord (SBV.sbvRotateLeft x (fromWord y))
+          VWord x -> VWord (SBV.sbvRotateLeft x (fromVWord y))
           _ -> selectV rol y
             where
               rol :: Integer -> Value
@@ -145,7 +145,7 @@ evalECon econ =
       VFun $ \xs ->
       VFun $ \y ->
         case xs of
-          VWord x -> VWord (SBV.sbvRotateRight x (fromWord y))
+          VWord x -> VWord (SBV.sbvRotateRight x (fromVWord y))
           _ -> selectV ror y
             where
               ror :: Integer -> Value
@@ -206,7 +206,7 @@ evalECon econ =
       VFun $ \xs ->
       VFun $ \ys ->
         let err = zeroV a -- default for out-of-bounds accesses
-        in mapV (selectV (\i -> nthV err xs i)) ys
+        in mapV (isTBit a) (selectV (\i -> nthV err xs i)) ys
 
     ECAtBack      -> -- {n,a,i} (fin n, fin i) => [n]a -> [i] -> a
       tlam $ \(finTValue -> n) ->
@@ -225,7 +225,7 @@ evalECon econ =
       VFun $ \xs ->
       VFun $ \ys ->
         let err = zeroV a -- default for out-of-bounds accesses
-        in mapV (selectV (\i -> nthV err xs (n - 1 - i))) ys
+        in mapV (isTBit a) (selectV (\i -> nthV err xs (n - 1 - i))) ys
 
     ECFromThen   -> fromThenV
     ECFromTo     -> fromToV
@@ -233,13 +233,13 @@ evalECon econ =
 
     ECInfFrom    ->
       tlam $ \(finTValue -> bits)  ->
-       lam $ \(fromWord  -> first) ->
+       lam $ \(fromVWord  -> first) ->
       toStream [ VWord (first + SBV.literal (bv (fromInteger bits) i)) | i <- [0 ..] ]
 
     ECInfFromThen -> -- {a} (fin a) => [a] -> [a] -> [inf][a]
       tlam $ \_ ->
-       lam $ \(fromWord -> first) ->
+       lam $ \(fromVWord -> first) ->
-       lam $ \(fromWord -> next) ->
+       lam $ \(fromVWord -> next) ->
       toStream (map VWord (iterate (+ (next - first)) first))
 
     -- {at,len} (fin len) => [len][8] -> at
@@ -315,17 +315,17 @@ nthV err v n =
                                     VBit (SBV.sbvTestBit x i)
     _                       -> err
 
-mapV :: (Value -> Value) -> Value -> Value
+mapV :: Bool -> (Value -> Value) -> Value -> Value
-mapV f v =
+mapV isBit f v =
   case v of
-    VSeq b xs  -> VSeq b (map f xs)
+    VSeq _ xs  -> VSeq isBit (map f xs)
     VStream xs -> VStream (map f xs)
     _          -> panic "Cryptol.Symbolic.Prims.mapV" [ "non-mappable value" ]
 
 catV :: Value -> Value -> Value
 catV xs          (VStream ys) = VStream (fromSeq xs ++ ys)
-catV (VWord x)   ys           = VWord (cat x (fromWord ys))
+catV (VWord x)   ys           = VWord (cat x (fromVWord ys))
-catV xs          (VWord y)    = VWord (cat (fromWord xs) y)
+catV xs          (VWord y)    = VWord (cat (fromVWord xs) y)
 catV (VSeq b xs) (VSeq _ ys)  = VSeq b (xs ++ ys)
 catV _ _ = panic "Cryptol.Symbolic.Prims.catV" [ "non-concatenable value" ]
 
@@ -395,7 +395,7 @@ arithBinary op = loop . toTypeVal
     loop ty l r =
       case ty of
         TVBit         -> evalPanic "arithBinop" ["Invalid arguments"]
-        TVSeq _ TVBit -> VWord (op (fromWord l) (fromWord r))
+        TVSeq _ TVBit -> VWord (op (fromVWord l) (fromVWord r))
         TVSeq _ t     -> VSeq False (zipWith (loop t) (fromSeq l) (fromSeq r))
         TVStream t    -> VStream (zipWith (loop t) (fromSeq l) (fromSeq r))
         TVTuple ts    -> VTuple (zipWith3 loop ts (fromVTuple l) (fromVTuple r))
@@ -409,7 +409,7 @@ arithUnary op = loop . toTypeVal
     loop ty v =
       case ty of
         TVBit         -> evalPanic "arithUnary" ["Invalid arguments"]
-        TVSeq _ TVBit -> VWord (op (fromWord v))
+        TVSeq _ TVBit -> VWord (op (fromVWord v))
         TVSeq _ t     -> VSeq False (map (loop t) (fromSeq v))
         TVStream t    -> VStream (map (loop t) (fromSeq v))
         TVTuple ts    -> VTuple (zipWith loop ts (fromVTuple v))
@@ -451,8 +451,8 @@ cmpValue fb fw = cmp
                                         [ "Functions are not comparable" ]
         (VPoly {}   , VPoly {}   ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
                                         [ "Polymorphic values are not comparable" ]
-        (VWord w1   , _          ) -> fw w1 (fromWord v2) k
+        (VWord w1   , _          ) -> fw w1 (fromVWord v2) k
-        (_          , VWord w2   ) -> fw (fromWord v1) w2 k
+        (_          , VWord w2   ) -> fw (fromVWord v1) w2 k
         (_          , _          ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
                                         [ "type mismatch" ]
 
@@ -543,7 +543,7 @@ logicBinary bop op = loop . toTypeVal
     loop ty l r =
       case ty of
         TVBit         -> VBit (bop (fromVBit l) (fromVBit r))
-        TVSeq _ TVBit -> VWord (op (fromWord l) (fromWord r))
+        TVSeq _ TVBit -> VWord (op (fromVWord l) (fromVWord r))
         TVSeq _ t     -> VSeq False (zipWith (loop t) (fromSeq l) (fromSeq r))
         TVStream t    -> VStream (zipWith (loop t) (fromSeq l) (fromSeq r))
         TVTuple ts    -> VTuple (zipWith3 loop ts (fromVTuple l) (fromVTuple r))
@@ -556,7 +556,7 @@ logicUnary bop op = loop . toTypeVal
     loop ty v =
       case ty of
         TVBit         -> VBit (bop (fromVBit v))
-        TVSeq _ TVBit -> VWord (op (fromWord v))
+        TVSeq _ TVBit -> VWord (op (fromVWord v))
         TVSeq _ t     -> VSeq False (map (loop t) (fromSeq v))
         TVStream t    -> VStream (map (loop t) (fromSeq v))
         TVTuple ts    -> VTuple (zipWith loop ts (fromVTuple v))

src/Cryptol/Symbolic/Value.hs

@@ -8,6 +8,7 @@
 
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 
 module Cryptol.Symbolic.Value
@@ -15,7 +16,7 @@ module Cryptol.Symbolic.Value
   , TValue, numTValue, toNumTValue, finTValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq
   , GenValue(..), lam, tlam, toStream, toFinSeq, toSeq
   , fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord
-  , fromSeq, fromWord
+  , fromSeq, fromVWord
   , evalPanic
   )
   where
@@ -23,8 +24,8 @@ module Cryptol.Symbolic.Value
 import Data.Bits (bitSize)
 
 import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq,
-                           GenValue(..), lam, tlam, toStream, toFinSeq, toSeq,
+                           GenValue(..), BitWord(..), lam, tlam, toStream, toFinSeq, toSeq, fromSeq,
-                           fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord)
+                           fromVBit, fromVWord, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord)
 import Cryptol.Symbolic.BitVector
 import Cryptol.Utils.Panic (panic)
 
@@ -44,11 +45,11 @@ instance Mergeable Value where
       (VBit b1    , VBit b2    ) -> VBit $ symbolicMerge f c b1 b2
       (VWord w1   , VWord w2   ) -> VWord $ symbolicMerge f c w1 w2
       (VSeq b1 vs1, VSeq _ vs2 ) -> VSeq b1 $ symbolicMerge f c vs1 vs2
-      (VStream vs1, VStream vs2) -> VStream $ symbolicMerge f c vs1 vs2
+      (VStream vs1, VStream vs2) -> VStream $ mergeStream vs1 vs2
       (VFun f1    , VFun f2    ) -> VFun $ symbolicMerge f c f1 f2
       (VPoly f1   , VPoly f2   ) -> VPoly $ symbolicMerge f c f1 f2
-      (VWord w1   , _          ) -> VWord $ symbolicMerge f c w1 (fromWord v2)
+      (VWord w1   , _          ) -> VWord $ symbolicMerge f c w1 (fromVWord v2)
-      (_          , VWord w2   ) -> VWord $ symbolicMerge f c (fromWord v1) w2
+      (_          , VWord w2   ) -> VWord $ symbolicMerge f c (fromVWord v1) w2
       (_          , _          ) -> panic "Cryptol.Symbolic.Value"
                                       [ "symbolicMerge: incompatible values" ]
     where
@@ -56,25 +57,14 @@ instance Mergeable Value where
         | n1 == n2  = (n1, symbolicMerge f c x1 x2)
         | otherwise = panic "Cryptol.Symbolic.Value"
                         [ "symbolicMerge.mergeField: incompatible values" ]
+      mergeStream xs ys =
+        symbolicMerge f c (head xs) (head ys) : mergeStream (tail xs) (tail ys)
 
 -- Big-endian Words ------------------------------------------------------------
 
-unpackWord :: SWord -> [SBool]
+instance BitWord SBool SWord where
-unpackWord s = [ sbvTestBit s i | i <- reverse [0 .. bitSize s - 1] ]
+  packWord bs = Data.SBV.fromBitsBE bs
-
+  unpackWord w = [ sbvTestBit w i | i <- reverse [0 .. bitSize w - 1] ]
--- Constructors and Accessors --------------------------------------------------
-
-fromWord :: Value -> SWord
-fromWord (VWord s) = s
-fromWord v = Data.SBV.fromBitsBE (map fromVBit (fromSeq v))
-
--- | Extract a sequence.
-fromSeq :: Value -> [Value]
-fromSeq v = case v of
-  VSeq _ vs  -> vs
-  VWord s    -> map VBit (unpackWord s)
-  VStream vs -> vs
-  _          -> evalPanic "fromSeq" ["not a sequence"]
 
 -- Errors ----------------------------------------------------------------------
 

src/Cryptol/TypeCheck/Infer.hs

@@ -133,6 +133,7 @@ appTys expr ts =
     P.ESel      {} -> mono
     P.EList     {} -> mono
     P.EFromTo   {} -> mono
+    P.EInfFrom  {} -> mono
     P.EComp     {} -> mono
     P.EApp      {} -> mono
     P.EIf       {} -> mono
@@ -249,6 +250,12 @@ inferE expr =
                 | (x,y) <- ("first",t1) : fs
                 ]
 
+    P.EInfFrom e1 Nothing ->
+      inferE $ P.EApp (P.ECon ECInfFrom) e1
+
+    P.EInfFrom e1 (Just e2) ->
+      inferE $ P.EApp (P.EApp (P.ECon ECInfFromThen) e1) e2
+
     P.EComp e mss ->
       do (mss', dss, ts) <- unzip3 `fmap` zipWithM inferCArm [ 1 .. ] mss
          w      <- smallest ts

src/Cryptol/TypeCheck/InferTypes.hs

@@ -405,7 +405,7 @@ instance PP (WithNames Error) where
       TypeVariableEscaped t xs ->
         nested (text "The type" <+> ppWithNames names t <+>
                 text "is not sufficiently polymorphic.")
-               (text "It may not depend on quantified variables:" <+>
+               (text "It cannot depend on quantified variables:" <+>
                 sep (punctuate comma (map (ppWithNames names) xs)))
 
       NotForAll x t ->

src/Cryptol/TypeCheck/Monad.hs

@@ -33,6 +33,7 @@ import           Data.Set (Set)
 import           Data.List(find)
 import           Data.Maybe(mapMaybe)
 import           MonadLib
+import qualified Control.Applicative as A
 import           Control.Monad.Fix(MonadFix(..))
 import           Data.Functor
 
@@ -179,6 +180,10 @@ data RW = RW
 instance Functor InferM where
   fmap f (IM m) = IM (fmap f m)
 
+instance A.Applicative InferM where
+  pure  = return
+  (<*>) = ap
+
 instance Monad InferM where
   return x      = IM (return x)
   fail x        = IM (fail x)
@@ -295,10 +300,18 @@ newGoalName = newName $ \s -> let x = seedGoal s
 
 -- | Generate a new free type variable.
 newTVar :: Doc -> Kind -> InferM TVar
-newTVar src k =
+newTVar src k = newTVar' src Set.empty k
+
+-- | Generate a new free type variable that depends on these additional
+-- type parameters.
+newTVar' :: Doc -> Set TVar -> Kind -> InferM TVar
+newTVar' src extraBound k =
   do bound <- getBoundInScope
+     let vs = Set.union extraBound bound
      newName $ \s -> let x = seedTVar s
-                     in (TVFree x k bound src, s { seedTVar = x + 1 })
+                     in (TVFree x k vs src, s { seedTVar = x + 1 })
+
+
 
 -- | Generate a new free type variable.
 newTParam :: Maybe QName -> Kind -> InferM TParam
@@ -551,6 +564,10 @@ data KRW = KRW { typeParams :: Map QName Kind -- ^ kinds of (known) vars.
 instance Functor KindM where
   fmap f (KM m) = KM (fmap f m)
 
+instance A.Applicative KindM where
+  pure  = return
+  (<*>) = ap
+
 instance Monad KindM where
   return x      = KM (return x)
   fail x        = KM (fail x)
@@ -604,7 +621,10 @@ kRecordWarning w = kInInferM $ recordWarning w
 
 -- | Generate a fresh unification variable of the given kind.
 kNewType :: Doc -> Kind -> KindM Type
-kNewType src k = kInInferM $ newType src k
+kNewType src k =
+  do tps <- KM $ do vs <- asks lazyTVars
+                    return $ Set.fromList [ tv | TVar tv <- Map.elems vs ]
+     kInInferM $ TVar `fmap` newTVar' src tps k
 
 -- | Lookup the definition of a type synonym.
 kLookupTSyn :: QName -> KindM (Maybe TySyn)

src/Cryptol/TypeCheck/Solver/Eval.hs

@@ -468,9 +468,7 @@ tfWidth _ ty
   , TCon (TF TCExp) [ TCon (TC (TCNum 2)) _, t2 ] <- t1 = Just t2
 
 tfWidth _ t
-  | Just (Nat 0)   <- arg = return $ tNum (0 :: Int)
+  | Just (Nat x)   <- arg = return $ tNum (widthInteger x)
-  | Just (Nat x)   <- arg = do (n,_) <- genLog x 2
-                               return $ tNum $ n + 1
   | Just Inf <- arg       = Just tInf
   | otherwise             = Nothing
 

src/Cryptol/TypeCheck/Solver/InfNat.hs

@@ -12,6 +12,7 @@
 {-# LANGUAGE Safe #-}
 module Cryptol.TypeCheck.Solver.InfNat where
 
+import Data.Bits
 import Cryptol.Utils.Panic
 
 -- | Natural numbers with an infinity element
@@ -123,11 +124,7 @@ nLg2 (Nat n)  = case genLog n 2 of
 -- from 0 to n, inclusive. @nWidth x = nLg2 (x + 1)@.
 nWidth :: Nat' -> Nat'
 nWidth Inf      = Inf
-nWidth (Nat 0)  = Nat 0
+nWidth (Nat n)  = Nat (widthInteger n)
-nWidth (Nat n)  = case genLog n 2 of
-                    Just (x,_) -> Nat (x + 1)
-                    Nothing -> panic "Cryptol.TypeCheck.Solver.InfNat.nWidth"
-                                 [ "genLog returned Nothing" ]
 
 
 {- | @length ([ x, y .. ] : [_][w])@
@@ -186,4 +183,13 @@ genLog x base = Just (exactLoop 0 x)
     | otherwise = let s1 = s + 1 in s1 `seq` underLoop s1 (div i base)
 
 
+-- | Compute the number of bits required to represent the given integer.
+widthInteger :: Integer -> Integer
+widthInteger x = go' 0 (if x < 0 then complement x else x)
+  where
+    go s 0 = s
+    go s n = let s' = s + 1 in s' `seq` go s' (n `shiftR` 1)
 
+    go' s n
+      | n < bit 32 = go s n
+      | otherwise  = let s' = s + 32 in s' `seq` go' s' (n `shiftR` 32)

tests/Main.hs

@@ -22,7 +22,8 @@ import System.FilePath
     ((</>),(<.>),takeExtension,splitFileName,splitDirectories,pathSeparator
     ,isRelative)
 import System.Process
-    (createProcess,CreateProcess(..),StdStream(..),proc,waitForProcess)
+    (createProcess,CreateProcess(..),StdStream(..),proc,waitForProcess
+    ,readProcessWithExitCode)
 import System.IO
     (hGetContents,IOMode(..),withFile,SeekMode(..),Handle,hSetBuffering
     ,BufferMode(..))
@@ -56,7 +57,7 @@ data Options = Options
   , optHelp      :: Bool
   , optResultDir :: FilePath
   , optTests     :: [TestStrategy]
-  , optDiff      :: String
+  , optDiff      :: Maybe String
   } deriving (Show)
 
 defaultOptions :: Options
@@ -66,14 +67,14 @@ defaultOptions  = Options
   , optHelp      = False
   , optResultDir = "output"
   , optTests     = []
-  , optDiff      = "meld"
+  , optDiff      = Nothing
   }
 
 setHelp :: Endo Options
 setHelp  = Endo (\ opts -> opts { optHelp = True } )
 
 setDiff :: String -> Endo Options
-setDiff diff = Endo (\opts -> opts { optDiff = diff })
+setDiff diff = Endo (\opts -> opts { optDiff = Just diff })
 
 setCryptol :: String -> Endo Options
 setCryptol path = Endo (\ opts -> opts { optCryptol = path } )
@@ -192,11 +193,19 @@ generateAssertion opts dir file = testCase file $ do
         Right _ -> assertFailure $
             "Test completed successfully.  Please remove " ++ knownFailureFile
     | otherwise =
-      assertFailure $
+      case mbKnown of
-        case mbKnown of
+
-          Left (X.SomeException {}) ->
+        Left (X.SomeException {})
-                                  unwords [ optDiff opts, goldFile, resultOut ]
+          | Just prog <- optDiff opts ->
-          Right fail_msg -> fail_msg
+            do goldFile' <- canonicalizePath goldFile
+               assertFailure (unwords [ prog, goldFile', "\\\n    ", resultOut ])
+
+          | otherwise ->
+            do goldFile' <- canonicalizePath goldFile
+               (_,out,_) <- readProcessWithExitCode "diff" [ goldFile', resultOut ] ""
+               assertFailure out
+
+        Right fail_msg -> assertFailure fail_msg
 
 -- Test Discovery --------------------------------------------------------------
 

tests/issues/T146.cry

@@ -0,0 +1,14 @@
+mk_curve_ops f = undefined
+  where
+    c = { field = f
+        , v1    = ec_v1 f
+        , v2    = ec_v2 c
+        }
+
+ec_v1 : {fv} { v0: fv } -> fv
+ec_v1 = undefined
+
+ec_v2 : {fv} _ -> fv
+ec_v2 p = p.field.v0
+  where _ = p.field.v0
+

tests/issues/T146.icry

@@ -0,0 +1 @@
+:l T146.cry

tests/issues/T146.icry.fails

@@ -0,0 +1 @@
+Known problem. See #146.

tests/issues/issue073.icry

@@ -0,0 +1,3 @@
+1 : [(2^^37)-0x100]
+let f x y = (x : [(2^^37)-(2^^5)]) + y
+f zero zero

tests/issues/issue073.icry.stdout

@@ -0,0 +1,5 @@
+Loading module Cryptol
+
+word too wide for memory: 137438953216 bits
+
+word too wide for memory: 137438953440 bits

tests/issues/issue093.icry.stdout

@@ -3,7 +3,7 @@ Loading module Cryptol
 Loading module Main
 property t0 Using exhaustive testing.
   0%passed 1 tests.
-QED
+Q.E.D.
 property t1 Using random testing.
 testing...  0%  1%  2%  3%  4%  5%  6%  7%  8%  9% 10% 11% 12% 13% 14% 15% 16% 17% 18% 19% 20% 21% 22% 23% 24% 25% 26% 27% 28% 29% 30% 31% 32% 33% 34% 35% 36% 37% 38% 39% 40% 41% 42% 43% 44% 45% 46% 47% 48% 49% 50% 51% 52% 53% 54% 55% 56% 57% 58% 59% 60% 61% 62% 63% 64% 65% 66% 67% 68% 69% 70% 71% 72% 73% 74% 75% 76% 77% 78% 79% 80% 81% 82% 83% 84% 85% 86% 87% 88% 89% 90% 91% 92% 93% 94% 95% 96% 97% 98% 99%passed 100 tests.
 Coverage: 0.00% (100 of 2^^32 values)

tests/issues/issue094.icry.stdout

@@ -1,7 +1,7 @@
 Loading module Cryptol
 Using random testing.
-testing...  0%  1%  2%  3%  4%  5%  6%  7%  8%  9% 10% 11% 12% 13% 14% 15% 16% 17% 18% 19% 20% 21% 22% 23% 24% 25% 26% 27% 28% 29% 30% 31% 32% 33% 34% 35% 36% 37% 38% 39% 40% 41% 42% 43% 44% 45% 46% 47% 48% 49% 50% 51% 52% 53% 54% 55% 56% 57% 58% 59% 60% 61% 62% 63% 64% 65% 66% 67% 68% 69% 70% 71% 72% 73% 74% 75% 76% 77% 78% 79% 80% 81% 82% 83% 84% 85% 86% 87% 88% 89% 90% 91% 92% 93% 94% 95% 96% 97% 98% 99%passed 100 tests.
+testing...passed 100 tests.
 Coverage: 39.06% (100 of 256 values)
 Using exhaustive testing.
-  0%  0%  0%  1%  1%  1%  2%  2%  3%  3%  3%  4%  4%  5%  5%  5%  6%  6%  7%  7%  7%  8%  8%  8%  9%  9% 10% 10% 10% 11% 11% 12% 12% 12% 13% 13% 14% 14% 14% 15% 15% 16% 16% 16% 17% 17% 17% 18% 18% 19% 19% 19% 20% 20% 21% 21% 21% 22% 22% 23% 23% 23% 24% 24% 25% 25% 25% 26% 26% 26% 27% 27% 28% 28% 28% 29% 29% 30% 30% 30% 31% 31% 32% 32% 32% 33% 33% 33% 34% 34% 35% 35% 35% 36% 36% 37% 37% 37% 38% 38% 39% 39% 39% 40% 40% 41% 41% 41% 42% 42% 42% 43% 43% 44% 44% 44% 45% 45% 46% 46% 46% 47% 47% 48% 48% 48% 49% 49% 50% 50% 50% 51% 51% 51% 52% 52% 53% 53% 53% 54% 54% 55% 55% 55% 56% 56% 57% 57% 57% 58% 58% 58% 59% 59% 60% 60% 60% 61% 61% 62% 62% 62% 63% 63% 64% 64% 64% 65% 65% 66% 66% 66% 67% 67% 67% 68% 68% 69% 69% 69% 70% 70% 71% 71% 71% 72% 72% 73% 73% 73% 74% 74% 75% 75% 75% 76% 76% 76% 77% 77% 78% 78% 78% 79% 79% 80% 80% 80% 81% 81% 82% 82% 82% 83% 83% 83% 84% 84% 85% 85% 85% 86% 86% 87% 87% 87% 88% 88% 89% 89% 89% 90% 90% 91% 91% 91% 92% 92% 92% 93% 93% 94% 94% 94% 95% 95% 96% 96% 96% 97% 97% 98% 98% 98% 99% 99%passed 256 tests.
+passed 256 tests.
-QED
+Q.E.D.

tests/issues/issue103.icry.stdout

@@ -2,5 +2,5 @@ Loading module Cryptol
 
 Run-time error: undefined
 Using exhaustive testing.
-  0%
+
 invalid sequence index: 1

tests/issues/issue128.cry

@@ -0,0 +1,4 @@
+copy : [inf] -> [inf]
+copy ([b] # x) = if b then [True] # copy x else [False] # copy x
+
+property ok = copy ([True] # zero) @ 0

tests/issues/issue128.icry

@@ -0,0 +1,3 @@
+:l issue128.cry
+:check ok
+:prove ok

tests/issues/issue128.icry.stdout

@@ -0,0 +1,7 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+Using exhaustive testing.
+passed 1 tests.
+Q.E.D.
+Q.E.D.

tests/issues/issue130.cry

@@ -0,0 +1,10 @@
+parity xs = ys!0
+  where ys = [False] # [y ^ x | x <- xs | y <- ys ]
+
+foldl1 f xs = ys!0
+  where ys = [xs@0] # [ f y x | y <- ys | x <- tail xs ]
+
+par = foldl1 (^)
+
+parOK : {n} [n+1] -> Bit
+property parOK x = par x == parity x

tests/issues/issue130.icry

@@ -0,0 +1,3 @@
+:l issue130.cry
+:check parOK`{2}
+:prove parOK`{2}

tests/issues/issue130.icry.stdout

@@ -0,0 +1,7 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+Using exhaustive testing.
+passed 8 tests.
+Q.E.D.
+Q.E.D.

tests/issues/issue133.cry

@@ -1,5 +1,3 @@
-example1 : {a} (a >= 1, 2 >= a) => [16*a][8] -> [16][8]
+gcd : [8] -> [8] -> [8]
-example1 k = drop`{16} ((zero : [16*(2 - a)][8]) #k)
+gcd a b = if(b == 0) then a
-
+          else gcd b (a%b)
-example2 : {a} (a >= 1, 2 >= a) => [16*a][8] -> [16][8]
-example2 k = drop`{16} (zero # k)

tests/issues/issue133.icry

@@ -1,3 +1,3 @@
 :load issue133.cry
-:type example1
+:exhaust \x -> gcd 0 x == x
-:type example2
+:prove \x -> gcd 0 x == x

tests/issues/issue133.icry.stdout

@@ -1,5 +1,7 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-example1 : {a} (a >= 1, 2 >= a) => [16 * a][8] -> [16][8]
+Using exhaustive testing.
-example2 : {a} (a >= 1, 2 >= a) => [16 * a][8] -> [16][8]
+passed 256 tests.
+Q.E.D.
+Q.E.D.

tests/issues/issue135.icry

@@ -0,0 +1,2 @@
+:sat \(x : Bit) (y : Bit) -> x < y
+:prove \(x : Bit) (y : Bit) -> x <= y || y <= x

tests/issues/issue135.icry.stdout

@@ -0,0 +1,3 @@
+Loading module Cryptol
+(\(x : Bit) (y : Bit) -> x < y) False True = True
+Q.E.D.

tests/issues/issue152.icry.stdout

@@ -1,56 +1,56 @@
 Loading module Cryptol
-0xf432e198
+0xf7e937b5
-[0xdbf8eedb6bd59796, 0x9749e08c37d123ee, 0x3b79a2a98701e9ae,
+[0xd4d4cc91cd7a9857, 0x4f3d263304e8ca85, 0x6723eafdcc46836f,
- 0x1a34d8f4efee5604, 0xfb0983cd5d80e611, ...]
+ 0x20e6c946662f2183, 0x6a760db62889b212, ...]
-[[0xaa, 0x2c, 0x08, 0xd7, 0x7a, 0xc3, 0xa9, 0xc8, 0xa7, 0xfe, 0x71,
+[[0x01, 0x83, 0x5f, 0x2e, 0xd1, 0x1a, 0x00, 0x1f, 0xfe, 0x55, 0xc8,
-  0x3f, 0x76, 0x8e, 0x47, 0x73, 0x82, 0x53, 0x33, 0x32, 0xaf, 0x66,
+  0x96, 0xcd, 0xe5, 0x9e, 0xca, 0xd9, 0xaa, 0x8a, 0x89, 0x06, 0xbd,
-  0x19, 0xe9, 0x50, 0xe4, 0x56, 0x37, 0x34, 0x91, 0x14, 0x08],
+  0x70, 0x40, 0xa7, 0x3b, 0xad, 0x8e, 0x8b, 0xe8, 0x6b, 0x5f],
- [0x5a, 0x83, 0xba, 0x1a, 0x48, 0xeb, 0xd7, 0x2c, 0xeb, 0x8c, 0xae,
+ [0xb1, 0xda, 0x11, 0x71, 0x9f, 0x42, 0x2e, 0x83, 0x42, 0xe3, 0x05,
-  0x54, 0x97, 0xa9, 0x11, 0x84, 0x2b, 0x07, 0x4e, 0x80, 0xe5, 0x1f,
+  0xab, 0xee, 0x00, 0x68, 0xdb, 0x82, 0x5e, 0xa5, 0xd7, 0x3c, 0x76,
-  0x42, 0x62, 0x6b, 0x82, 0x98, 0xed, 0x11, 0x3e, 0x44, 0xf6],
+  0x99, 0xb9, 0xc2, 0xd9, 0xef, 0x44, 0x68, 0x95, 0x9b, 0x4d],
- [0xd4, 0x7b, 0x0b, 0x91, 0x19, 0x21, 0x6d, 0xde, 0x04, 0x62, 0x1a,
+ [0x2b, 0xd2, 0x62, 0xe8, 0x70, 0x78, 0xc4, 0x35, 0x5b, 0xb9, 0x71,
-  0x64, 0x62, 0xac, 0x36, 0xd4, 0x44, 0x5e, 0xa4, 0xf4, 0x20, 0x9a,
+  0xbb, 0xb9, 0x03, 0x8d, 0x2b, 0x9b, 0xb5, 0xfb, 0x4b, 0x77, 0xf1,
-  0x96, 0x52, 0x13, 0x24, 0x70, 0x83, 0x86, 0xac, 0xbb, 0xe6],
+  0xed, 0xa9, 0x6a, 0x7b, 0xc7, 0xda, 0xdd, 0x03, 0x12, 0x3d],
- [0x0a, 0x99, 0x74, 0x3e, 0xa1, 0x8e, 0xe2, 0xba, 0x81, 0xa0, 0xbd,
+ [0x61, 0xf0, 0xcb, 0x95, 0xf8, 0xe5, 0x39, 0x11, 0xd8, 0xf7, 0x14,
-  0x6a, 0xe9, 0x9a, 0xbc, 0xc4, 0x5d, 0x13, 0xe2, 0x0b, 0xc0, 0xf4,
+  0xc1, 0x40, 0xf1, 0x13, 0x1b, 0xb4, 0x6a, 0x39, 0x62, 0x17, 0x4b,
-  0x35, 0x34, 0xc4, 0x26, 0xce, 0x01, 0xf9, 0x5e, 0xe9, 0x1b],
+  0x8c, 0x8b, 0x1b, 0x7d, 0x25, 0x58, 0x50, 0xb5, 0x40, 0x72],
- [0x5c, 0xa9, 0xb1, 0xd4, 0xa3, 0xab, 0x9f, 0x2e, 0x50, 0x1d, 0xe0,
+ [0xb3, 0x00, 0x08, 0x2b, 0xfa, 0x02, 0xf6, 0x85, 0xa7, 0x74, 0x37,
-  0xf2, 0x4d, 0xd6, 0x1c, 0xb7, 0x0d, 0xd6, 0x86, 0x14, 0x7b, 0xd2,
+  0x49, 0xa4, 0x2d, 0x73, 0x0e, 0x64, 0x2d, 0xdd, 0x6b, 0xd2, 0x29,
-  0x44, 0x83, 0x91, 0x75, 0x22, 0xec, 0x32, 0x68, 0x16, 0x94],
+  0x9b, 0xda, 0xe8, 0xcc, 0x79, 0x43, 0x89, 0xbf, 0x6d, 0xeb],
- [0x99, 0x36, 0xff, 0xc2, 0x00, 0x61, 0xe2, 0x84, 0xd2, 0xe6, 0xf7,
+ [0xf0, 0x8d, 0x56, 0x19, 0x57, 0xb8, 0x39, 0xdb, 0x29, 0x3d, 0x4e,
-  0x94, 0xf3, 0x96, 0xe8, 0x1f, 0xd4, 0x70, 0xf9, 0x03, 0x04, 0x6b,
+  0xeb, 0x4a, 0xed, 0x3f, 0x76, 0x2b, 0xc7, 0x50, 0x5a, 0x5b, 0xc2,
-  0x51, 0xcf, 0x8c, 0x8b, 0xbd, 0x29, 0x7a, 0x81, 0x1d, 0x6b],
+  0xa8, 0x26, 0xe3, 0xe2, 0x14, 0x80, 0xd1, 0xd8, 0x74, 0xc2],
- [0xc3, 0xea, 0x2a, 0x4a, 0xf5, 0x90, 0x98, 0xa0, 0x40, 0x4e, 0xea,
+ [0x1a, 0x41, 0x81, 0xa1, 0x4c, 0xe7, 0xef, 0xf7, 0x97, 0xa5, 0x41,
-  0xbb, 0x58, 0x20, 0x9f, 0x91, 0x3d, 0x6d, 0x70, 0xcf, 0x43, 0xf4,
+  0x12, 0xaf, 0x77, 0xf6, 0xe8, 0x94, 0xc4, 0xc7, 0x26, 0x9a, 0x4b,
-  0xa3, 0x12, 0x99, 0x8e, 0x6c, 0xcd, 0x56, 0xa0, 0xe9, 0x1e],
+  0xfa, 0x69, 0xf0, 0xe5, 0xc3, 0x24, 0xad, 0xf7, 0x40, 0x75],
- [0x80, 0xb3, 0xa4, 0xca, 0x62, 0x8a, 0xcd, 0x34, 0x73, 0xa9, 0x0c,
+ [0xd7, 0x0a, 0xfb, 0x21, 0xb9, 0xe1, 0x24, 0x8b, 0xca, 0x00, 0x63,
-  0x62, 0xed, 0x8f, 0x99, 0x72, 0x9a, 0x40, 0xfb, 0x95, 0xd5, 0x85,
+  0xb9, 0x44, 0xe6, 0xf0, 0xc9, 0xf1, 0x97, 0x52, 0xec, 0x2c, 0xdc,
-  0xe0, 0xf9, 0x8e, 0x50, 0x8c, 0x96, 0x2b, 0xc7, 0x7c, 0x5a],
+  0x37, 0x50, 0xe5, 0xa7, 0xe3, 0xed, 0x82, 0x1e, 0xd3, 0xb1],
- [0xca, 0x1d, 0xcf, 0xcd, 0x44, 0xd8, 0xc7, 0x95, 0xe4, 0xb7, 0x27,
+ [0x21, 0x74, 0x26, 0x24, 0x9b, 0x2f, 0x1e, 0xec, 0x3b, 0x0e, 0x7e,
-  0xa9, 0xd7, 0x6a, 0xc3, 0x16, 0x29, 0xf9, 0x81, 0x71, 0x3c, 0xc1,
+  0x00, 0x2e, 0xc1, 0x1a, 0x6d, 0x80, 0x50, 0xd8, 0xc8, 0x93, 0x18,
-  0x57, 0xc8, 0xda, 0x51, 0xe6, 0x12, 0x66, 0xd2, 0x97, 0x8e],
+  0xae, 0x1f, 0x31, 0xa8, 0x3d, 0x69, 0xbd, 0x29, 0xee, 0xe5],
- [0xba, 0xfb, 0x31, 0x91, 0xcb, 0x57, 0xd1, 0xb5, 0x35, 0x5c, 0xd1,
+ [0x11, 0x52, 0x88, 0xe8, 0x22, 0xae, 0x28, 0x0c, 0x8c, 0xb3, 0x28,
-  0x45, 0x6b, 0x88, 0x39, 0x28, 0x13, 0xb5, 0x6d, 0xe1, 0x75, 0xf9,
+  0x9c, 0xc2, 0xdf, 0x90, 0x7f, 0x6a, 0x0c, 0xc4, 0x38, 0xcc, 0x50,
-  0xc4, 0xb3, 0x98, 0xea, 0x24, 0xd1, 0x5d, 0xa7, 0x22, 0x37],
+  0x1b, 0x0a, 0xef, 0x41, 0x7b, 0x28, 0xb4, 0xfe, 0x79, 0x8e],
- [0x3b, 0xa3, 0xdd, 0xda, 0x73, 0xcf, 0x8f, 0x0d, 0xea, 0x2f, 0x79,
+ [0x92, 0xfa, 0x34, 0x31, 0xca, 0x26, 0xe6, 0x64, 0x41, 0x86, 0xd0,
-  0xb7, 0x07, 0xc9, 0x71, 0x82, 0x00, 0x9a, 0xa5, 0x4d, 0xd4, 0x64,
+  0x0e, 0x5e, 0x20, 0xc8, 0xd9, 0x57, 0xf1, 0xfc, 0xa4, 0x2b, 0xbb,
-  0xe3, 0xbd, 0x22, 0x29, 0xe1, 0x30, 0xd1, 0x9a, 0x96, 0x49],
+  0x3a, 0x14, 0x79, 0x80, 0x38, 0x87, 0x28, 0xf1, 0xed, 0xa0],
- [0xd8, 0xac, 0x92, 0x67, 0xa9, 0x82, 0xfd, 0x36, 0x50, 0x3d, 0x60,
+ [0x2f, 0x03, 0xe9, 0xbe, 0x00, 0xd9, 0x54, 0x8d, 0xa7, 0x94, 0xb7,
-  0x1d, 0x19, 0xeb, 0x4e, 0x42, 0x71, 0x3a, 0xb4, 0xc7, 0x40, 0x6a,
+  0x74, 0x70, 0x42, 0xa5, 0x99, 0xc8, 0x91, 0x0b, 0x1e, 0x97, 0xc1,
-  0x0c, 0xbb, 0xad, 0xb3, 0x4c, 0x47, 0xee, 0x6c, 0x36, 0x1d],
+  0x63, 0x12, 0x04, 0x0a, 0xa3, 0x9e, 0x45, 0xc3, 0x8d, 0x74],
- [0xd0, 0x2b, 0xaa, 0x04, 0xca, 0x5b, 0xa4, 0x3b, 0xbc, 0x17, 0x56,
+ [0x27, 0x82, 0x01, 0x5b, 0x21, 0xb2, 0xfb, 0x92, 0x13, 0x6e, 0xad,
-  0x1b, 0x81, 0x8f, 0xce, 0xfe, 0x74, 0xae, 0xee, 0xd0, 0x07, 0xeb,
+  0x72, 0xd8, 0xe6, 0x25, 0x55, 0xcb, 0x05, 0x45, 0x27, 0x5e, 0x42,
-  0xf9, 0x08, 0x6b, 0xf8, 0xba, 0x4c, 0xad, 0x04, 0x01, 0xc0],
+  0x50, 0x5f, 0xc2, 0x4f, 0x11, 0xa3, 0x04, 0x5b, 0x58, 0x17],
- [0x4d, 0x04, 0x7b, 0x0a, 0xcc, 0xa3, 0x7f, 0x5d, 0xa0, 0x87, 0x30,
+ [0xa4, 0x5b, 0xd2, 0x61, 0x23, 0xfa, 0xd6, 0xb4, 0xf7, 0xde, 0x87,
-  0x67, 0x0b, 0xa9, 0x0c, 0xe6, 0x32, 0x45, 0xb8, 0x52, 0x02, 0x6d,
+  0xbe, 0x62, 0x00, 0x63, 0x3d, 0x89, 0x9c, 0x0f, 0xa9, 0x59, 0xc4,
-  0xfa, 0xdf, 0xad, 0x18, 0xd6, 0xc5, 0xe6, 0x7b, 0xb9, 0xd4],
+  0x51, 0x36, 0x04, 0x6f, 0x2d, 0x1c, 0x3d, 0xd2, 0x10, 0x2b],
- [0x0c, 0xaa, 0xfa, 0xcf, 0x98, 0xc7, 0x90, 0x3a, 0x11, 0x1e, 0x5c,
+ [0x63, 0x01, 0x51, 0x26, 0xef, 0x1e, 0xe7, 0x91, 0x68, 0x75, 0xb3,
-  0x8b, 0x72, 0x81, 0x82, 0x9e, 0x59, 0x91, 0x76, 0x96, 0x41, 0x09,
+  0xe2, 0xc9, 0xd8, 0xd9, 0xf5, 0xb0, 0xe8, 0xcd, 0xed, 0x98, 0x60,
-  0x55, 0x27, 0x9f, 0xae, 0xbd, 0x86, 0x7c, 0xc9, 0x84, 0xc7],
+  0xac, 0x7e, 0xf6, 0x05, 0x14, 0xdd, 0xd3, 0x20, 0xdb, 0x1e],
- [0xa5, 0x6a, 0xe2, 0xf5, 0x4f, 0x5d, 0x07, 0x00, 0x8d, 0x14, 0x7c,
+ [0xfc, 0xc1, 0x39, 0x4c, 0xa6, 0xb4, 0x5e, 0x57, 0xe4, 0x6b, 0xd3,
-  0xe6, 0xd8, 0x1a, 0x1a, 0x1e, 0x85, 0x07, 0x86, 0x23, 0x64, 0x20,
+  0x3d, 0x2f, 0x71, 0x71, 0x75, 0xdc, 0x5e, 0xdd, 0x7a, 0xbb, 0x77,
-  0x89, 0xd7, 0x2e, 0x80, 0x71, 0xcf, 0x2a, 0x3c, 0x5d, 0x22]]
+  0xe0, 0x2e, 0x85, 0xd7, 0xc8, 0x26, 0x81, 0x93, 0xb4, 0x79]]
-(0xf432e198, 0x2add)
+(0xf7e937b5, 0x2b34)
-{x = 0xa155580c, y = 0x8353}
+{x = 0x5a314507, y = 0x83aa}
 0x00000000
-0x7ea4fc59
+0x45beaedf

tests/issues/trac133.cry

@@ -0,0 +1,5 @@
+example1 : {a} (a >= 1, 2 >= a) => [16*a][8] -> [16][8]
+example1 k = drop`{16} ((zero : [16*(2 - a)][8]) #k)
+
+example2 : {a} (a >= 1, 2 >= a) => [16*a][8] -> [16][8]
+example2 k = drop`{16} (zero # k)

tests/issues/trac133.icry

@@ -0,0 +1,3 @@
+:load trac133.cry
+:type example1
+:type example2

tests/issues/trac133.icry.stdout

@@ -0,0 +1,5 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+example1 : {a} (a >= 1, 2 >= a) => [16 * a][8] -> [16][8]
+example2 : {a} (a >= 1, 2 >= a) => [16 * a][8] -> [16][8]

tests/regression/check09.icry.stdout

@@ -1,14 +1,18 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-[warning] This binding for (at check09.cry:4:1--4:6, Main::initL) shadows the existing binding
+[warning] at check09.cry:22:5--22:10
-    (at check09.cry:22:5--22:10, initL)
+    This binding for initL shadows the existing binding from
-[warning] This binding for (at check09.cry:3:1--3:6, Main::initS) shadows the existing binding
+    (at check09.cry:4:1--4:6, Main::initL)
-    (at check09.cry:21:5--21:10, initS)
+[warning] at check09.cry:21:5--21:10
-[warning] This binding for (at check09.cry:8:1--8:3, Main::ls) shadows the existing binding
+    This binding for initS shadows the existing binding from
-    (at check09.cry:27:5--27:7, ls)
+    (at check09.cry:3:1--3:6, Main::initS)
-[warning] This binding for (at check09.cry:5:1--5:3, Main::ss) shadows the existing binding
+[warning] at check09.cry:27:5--27:7
-    (at check09.cry:23:5--23:7, ss)
+    This binding for ls shadows the existing binding from
+    (at check09.cry:8:1--8:3, Main::ls)
+[warning] at check09.cry:23:5--23:7
+    This binding for ss shadows the existing binding from
+    (at check09.cry:5:1--5:3, Main::ss)
 [warning] at check09.cry:17:1--30:54:
   Defaulting 4th type parameter
              of expression (@@)

tests/regression/check25.icry.stdout

@@ -1,8 +1,9 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module check25
-[warning] This binding for (at check25.cry:3:1--3:3, check25::tz) shadows the existing binding
+[warning] at check25.cry:6:9--6:11
-    (at check25.cry:6:9--6:11, tz)
+    This binding for tz shadows the existing binding from
+    (at check25.cry:3:1--3:3, check25::tz)
 [warning] at check25.cry:1:1--8:19:
   Defaulting 1st type parameter
              of expression check25::tx

tests/renamer/comp02.icry.stdout

@@ -2,9 +2,11 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module comp02
 
-[error] Overlapping symbols defined:
+[error]
+    Overlapping symbols defined:
     (at comp02.cry:4:12--4:13, a)
     (at comp02.cry:5:12--5:13, a)
-[error] Multiple definitions for symbol: (at comp02.cry:4:8--4:9, a)
+[error] at comp02.cry:4:8--4:9
+    Multiple definitions for symbol: a
     (at comp02.cry:4:12--4:13, a)
     (at comp02.cry:5:12--5:13, a)