Skip to content

v2.2.0
Compare
Choose a tag to compare
@acfoltzer acfoltzer released this 24 Mar 18:52
v2.2.0
0536d0f

Cryptol 2.2.0

General Improvements Made

  • Added two flags to cryptol.cabal:
    • relocatable: ignores the library path baked in at compile time with the expectation that that path will not necessarily be valid in the installed environment (good for building tarball-style binary distributions)
    • self-contained: compiles the contents of the Cryptol prelude into the executable so that it can be reconstituted if the prelude is not found in the usual library path (good for applications using Cryptol as a Cabal library rather than using the Cryptol Makefile)
  • Changed the parser so that UTF-8 is always the encoding for Cryptol source files; it had previously depended on the locale settings on the user's computer which caused headaches when collaborating
  • Improved the way the type checker generates and discharges goals so that more information is used from explicit signatures and fewer unification operations are required, improving speed and precision of type inference (#16)
  • Merged changes in Cryptol's SBV fork upstream and switched to using the Hackage version of the library (#35)
  • Overhauled the Makefile and the way distributions are configured and built (#127, #161, #169)
  • Prepared Cryptol for a Hackage release (#18)
  • Redid the way the interpreter looks for modules to load, making it more portable and flexible for various types of installation scenarios (#127, 13a385d, 3d275ea)
  • Split off the experimental ICryptol notebook into a separate project (9923b6f)
  • Unified some of the concrete and symbolic evaluator code

Features Added

  • Added a "smoke test" on startup to check for the presence of CVC4 and give an informative error message if it's not found (#112)
  • Added abc as a prover option in the interpreter
  • Added binding of counterexamples and satisfying assignments to the it interpreter variable (#19)
  • Added support for multiple satisfying assignments from :sat by setting the satNum interpreter variable (#19, #72)
  • Added support for .cryptolrc files, batch scripts in either the current directory or the user's home directory that are automatically read and executed when the interpreter starts (#97)
  • Added the CRYPTOLPATH environment variable so that custom locations can be searched when loading modules (#127)
  • Added warnShadowing interpreter option, on by default, to control whether warnings about shadowed variables appear
  • Made local bindings without type signatures (like those in where clauses) monomorphic by default, though this behavior can be overridden using the mono-binds interpreter variable; in many cases this improves the quality of inferred types and makes more programs typecheck

Documentation Improved

  • Added documentation to explain mono-binds when introducing where clauses
  • Began documenting development and release practices in HACKING.md
  • Cleaned up and updated README.md to account for recent changes and the spinoff of ICryptol
  • Updated :sat examples to use satNum rather than manually adding clauses for additional counterexamples

Examples Added

Bugs Squished

  • Added a guard to help prevent GMP core dumps when creating extremely large bitvectors (#73)
  • Added the filename of the module being parsed when reporting a parser error (#168)
  • Changed precedence of xor (^) to bring it in line with Haskell and other languages
  • Fixed cases where evaluation was overly strict for sequences of bits (#130)
  • Fixed crash in symbolic simulation of (!!) and (@@) (#148)
  • Fixed empty modules being rejected (#167)
  • Fixed handling of Fin constraints when calling the solver during typechecking (#58, #140)
  • Fixed implementation of (#) in symbolic simulation (#131)
  • Fixed modules not being properly reloaded
  • Fixed pretty-printing of infinite enumerations ([x...] and [x,y...])
  • Fixed punctuation of Q.E.D. (#132)
  • Fixed symbolic rotation by rotation amounts greater than the width of a word (#160)
  • Improved and fixed specification of Salsa20
  • Improved clarity of renamer errors (#125)
  • Improved handling of :check progress bars for batch mode and when interrupted by an exception or Ctrl-C (#114)
  • Improved performance of symbolic simulation primitives applied to very large bitvectors (#189)
  • Improved performance when parsing and typechecking large integer literals (#139)
  • Refined how we present output from check, :sat and :prove, particularly when no arguments are given (#117)
  • Removed extra strictness from symbolic simulation of streams (#128)
  • Switched to Template Haskell for generating git revision info in the banner and panic messages, reducing the frequency of rebuilds triggered when using Cryptol as a library
  • Various SBV fixes (#133, #135)
Assets 10
Loading