Cryptol Files

Administrative changes

• The binary builds are now built with GHC 9.8 rather than 9.6.

Language changes

• Allow arbitrary expressions in the head of a record update, previously we were restricted to atomic expressions. (#2127)

• Primitives arrayCopy, arraySet, and arrayRangeEqual from the built-in Array module now have types with fin constraints. (#2037)

• Add typechecker simplification rule: max(a,a) == a (#1923)

• Allow comma separate parameters in functor parameter blocks (#556)

• Nested modules and imports of sub-modules may only be used in the declarations that follow them. We now add implicit imports for all submodules uniformly (previously we did not add implicit imports for functor instantiations). (#1992)

• Defining two or more parameter blocks within the same module will now raise an error. To migrate an existing module that uses multiple parameter blocks, put all of the parameters under a single parameter block before they are used. (#1992)

• The REPL now contains some debug flags for dumping the results of intermediate Cryptol passes. (#2000)

• The REPL now supports multi-line definition blocks, delimited by :{ and :}. Everything between the delimiters is processed as a group of top-level declarations, without needing \ continuations or a leading let, which makes pasting definitions easier. (#2105)

• Add a timeout for individual typechecker SMT queries, configurable with the tcTimeout REPL option. Timed-out solver processes are killed and replaced. (#2117)

• Support prime constraints in numeric constraint guards. (#1658)

• Parameter values of a functor instance are now accessible through a virtual submodule named after the parameter (e.g., M::I::x). (#1699)

• Interfaces may now be parameterized by other interfaces (interface functors). (#1582)

• Add module aliases for giving short names to existing modules, functors, or interfaces. (#1591)

• Add new foldWhile primitive, which can optionally break early while folding. (#2028)

• Add a notPrime constraint. (#2089)

• Add the following typechecker simplification rules:

• K1 != K2 ^^ t ~~> t != logBase K2 K1
• K1 ^^ t >= K2 ~~> t >= logBase K2 K1
• K1 ^^ t > K2 ~~> t > logBase K2 K1
• K1 >= K2 ^^ t ~~> logBase K2 K1 >= t
• K1 > K2 ^^ t ~~> logBase K2 K1 > t

Bug fixes

• Fix a panic in the reference evaluator (:eval) when evaluating a numeric literal at type Bit, e.g. :eval 1 : Bool. The reference evaluator now agrees with the concrete evaluator, treating a nonzero literal as True and zero as False.

• Fix pretty printing of types in errors messages (#2019)

• Fix interface constraint scoping. Interface constraints are kept in the order they were declared, but will be floated as early as possible. (#1690)

• Fix incorrect module context computation for nested functors. (#1872) (#1898)

• Don't consider schemas with trivial True constraints to be polymorphic. (#1576)

• Don't panic when evaluating parameterized definitions at the REPL after a type error. (#2011)

• Fix a bug in coreLint that would trigger a panic when checking record updates on newtype values. (#2025)

• Fix a bug that would cause Bitwuzla-based provers to fail when reasoning about enums. (#2027)

• Fix a bug where calling roundAway on floating-point values would return incorrect results on concrete values. (#2044)

• Fix the reference evaluator panicking on primitives whose reference implementation is written in Cryptol. (#2070)

• Fix a bug in which numeric constraint guards that include "trivial" constraints (e.g., n == n) could generate ill-typed code. (#2093)

• Fix a bug in which evaluating fpToBits (fromInteger i : Float e p) could crash if the float size was smaller than a double-precision float. (#2108)

• Change how :load adjusts the module search path; see :help :load. (#2115)

API changes

• Add isValidIdent to Cryptol.Parser.LexerUtils, which checks if a name is a valid Cryptol identifier. (#2036)

• Add pIsNeq to Cryptol.TypeCheck.Type, which recognizes if a Cryptol constraint is headed by a not-equal (!=) operator. (#2038)

• Cryptol.TypeCheck.Solver.InfNat.genLog now takes the log base as the first argument instead of the second argument. This better reflects the intuition that genLog base x mirrors the mathematical notation log_{base}(x).