Cryptol Files

Language changes

None

Bug fixes

• Fix a bug where setting at timeout would cause sbv-yices, sbv-cvc4 and sbc-cvc5 to crash. Uses a deadman timer workaround for yices, due to a known issue. (#1808)

• Update Yices build in CI to fix a crash when running test issue_1807.icry on Mac OS X (ARM64). (what4-solvers [#58])

• Fix a bug where using a timeout with a subset of the what4 solvers would cause a runtime error. Includes a version bump for what4 to address a nondeterministic crash when using timeouts with cvc4/5. (what4 PR [#288]) (#1807)

• Fix [#1437], enforce the VSeq invariant that it is not a sequence of bits. Replaces the VSeq constructor with a view-only pattern, and smart constructors mkSeq and finSeq. (#1437)

• Fix [#1740], removes duplicated width from word values. Note that since this changes the types, it may require changes to libraries depending on Cryptol.

• Fix a bug in which splitting a [0] value into type [inf][0] would panic. (#1749)

• Fix a bug in which the free variables of types mentioning newtypes or enums were incorrectly computed. (#1773)

• The reference evaluator now evaluates the toSignedInteger and deepseq primitives instead of panicking.

• Fix a bug in which a ^^ (x ^^ y) could be incorrectly simplified to a ^^ (x * y) at the type level. (#1799)

New features

• Improved error messages during type inference for bindings. Adds a specific error message for when a binding has more arguments than expected, given its type signature. (#1744)

• Improved warning messages for non-exhaustive guards. Warnings are now ordered by source location. (#1798)

• More aggressive exhaustivity check that is less dependent on guard ordering. (#1796)

• Improved error messages mentioning module parameters (#1560)

• Improved the naming convention for anonymous modules generated by the module system (#1810)

• REPL command :dumptests <FILE> <EXPR> updated to write to stdout when invoked as :dumptests - <EXPR> allowing for easier experimentation and testing.

• The REPL properly supports tab completion for the :t and :check commands. (#1780)

• Add support for incrementally loading projects via cryptol's --project flag as documented in the reference manual. (#1641)

• Add support for the Bitwuzla SMT solver, which can be selected with :set prover=bitwuzla. If you want to specify a What4 or SBV backend, you can use :set prover=w4-bitwuzla or :set prover=sbv-bitwuzla, respectively. (#1786)

• Add a REPL option tcSmtFile that allows writing typechecker-related SMT solver interactions to a file.

• The typechecker can now simplify types of the form width (2^^n) to n + 1. (#1802)