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

• MKRAND RBG (#69)
• RC4 (#134)

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)

Cryptol 2.1.0

Language Semantics

• Changed indexing of tuples to be 0-based, rather than 1-based (#82)

Cryptol> (True, False).0
True
Cryptol> (True, False).1
False

Testing, SAT, and Prove

• Added :exhaust command for exhaustive testing (previously possible only by setting the tests variable high enough for full coverage) (#94)
• Added any solver which runs all available solvers in parallel and returns the first result (#7)
• Added offline mode for generating SMTLIB output, rather than invoking a solver (#85)
• Added support for Boolector and MathSAT solvers
• Improved distribution of :check cases (#86)
• Improved performance and stability of the Cryptol symbolic simulator

REPL

• Added let-binding to the REPL (#6)

Cryptol> let f x = x + 2
Cryptol> let g x = f x + 1
Cryptol> g 5 : [32]
8
Cryptol> let f x = 0
Cryptol> g 5 : [32]
8

• Added short versions of : commands (listed in :help output); the old behavior of entering a prefix of a command still works but is overridden when the prefix is also another command (#90, #99)
• Added the variable it to the REPL, which is always bound to the value of the previously-evaluated expression or to the counterexample/satisfying assignment of a :sat or :prove

Cryptol> 1+1 : [1]
0x0
Cryptol> it
0x0
Cryptol> :t it
it : [1]

• Changed default base to 16 (#89)
• Minor UI improvements to the REPL
• When :check and :prove are run without an argument, all property declarations in the current module are now checked or proved (#93)

Documentation

• Improved handling of fenced code in literate Cryptol Markdown files
• Many improvements to documentation and the Programming Cryptol book

Examples

• FNV-1a non-cryptographic hash
• Keccak hash
• ZUC cipher
• Malicious SHA

Bugs

• Fixed bug in Salsa20 example
• Fixed crash when complementing infinite sequences (#65)
• Fixed crash with large index sizes (#111)
• Fixed handling of layout blocks ended by parentheses or curly braces (#81)
• Fixed how we find the Cryptol.cry prelude file (#113)
• Fixed minor typos and editing errors
• Fixed some crashes during Cryptol Symbolic simulation (#101)
• Fixed various bugs in the type system constraint solver
• Handle exceptions properly when running :check (#103)
• Improved build system portability and compatibility (#23, #71)
• Modules are now only loaded once per load command (#10)
• Pretty-printer for Cryptol expressions now correctly parenthesizes infix operators
• The @, !, and !! operators now require finite-sized indexes (#111)

Version 2.1.0-alpha1.

Release of version 2.0.0