Cryptol Files

Language changes

• When running validation commands (:check, :prove, :exhaust, etc.) without an explicit argument, we now run only the properties in the currently focused module. This is a change in behavior, because previously we used to run all properties in the currently opened file. This change is only noticable when working with nested modules. The new behavior works better when these commands are used from docstrings (e.g., with the new behavior, writing :check on a submodule, will only check the properties in that submodule, as expected).

• When running the :check-docstrings command, Bit properties (e.g. property p = True) will be checked with :exhaust, unless their docstrings contain code blocks understood by :check-docstrings. (#1842)

• foreign function declarations now support an optional calling convention keyword. See the manual section for more information.

• Add an abstract calling convention, where Cryptol values are marshalled using an abstract interface. See the manual section for more information.

• Allow an explicit ; separator between case branches. This change removes the unreachable code in the grammar for case and where expressions with explicit { and } that was never reachable due to the way the layout rule worked.

• Add w4-rme prover. This prover works on goals using booleans and bit vectors. It's particularly suited to problems using Galois field arithmetic. It does not call out to an external solver. Use :set prover = w4-rme to enable it.

Bug fixes

• Fix a discrepency between the behavior of :check-docstrings when run on the REPL vs. when run with a project. (#1903)

• Fix [#1696], which corrected an incorrect simplification rule, leading to panics.

• Allow changing the tcSolver setting to non-Z3 solvers (e.g., CVC5) without crashing. (#1874)

• Fix browsing of main modules. crashing. (#1874)

New Features

• New REPL command :saw to run SAW on a SAW file, usable in docstrings. #1835