Skip to content

v2.1.0
Compare
Choose a tag to compare
@acfoltzer acfoltzer released this 16 Oct 20:40
v2.1.0
b394f1b

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)
Assets 14
Loading