Skip to content

2.6.0
Compare
Choose a tag to compare
@atomb atomb released this 01 Aug 15:34
· 3 commits to release/2.6.0 since this release
2.6.0
9b97c74

This release includes several significant language additions, including unbounded integers and parameterized modules, along with many smaller improvements and bug fixes.

Added

  • Cryptol now has types for unbounded integers (Integer) and, relatedly, integers modulo a constant value (Z n), which can be used for more natural encodings of many public-key algorithms, among many other use cases.

  • Modules can now take types and values (including functions) as parameters. Importing modules can instantiate these parameters, and proofs about parameterized modules can leave parameters abstract (and therefore prove properties for all possible concrete parameters).

  • Constraint synonyms can be used to group together collections of commonly-used constraints.

  • Signed operations now exist for arithmetic (/$ and %$), comparison (>$, <$, <=$, and >=$), and shifting (>>$).

  • Operations for chaining arithmetic now exist. The carry function returns True if addition of its arguments would result in unsigned overflow, the scarry function does the same for signed overflow, and the sborrow function checks for overflow on signed subtraction.

  • The new type operators /^ and %^ perform ceiling division and modulus, respectively. These can be particularly useful in computing the number of fixed-size blocks needed to store a message of a
    particular size, for instance, or conversely to compute the amount of padding needed to fill up an integral number of blocks.

  • The new type operator != allows the constraint that two types are not equal.

  • The experimental new :extract-coq command will export the currently-defined environment in a form usable with the Coq definition of Cryptol's operational semantics.

  • The new :ast command prints out the internal form of the AST for a given expression.

  • Underscores are allowed in numeric literals, and can be used to group digits for greater readability.

Changed

  • The Cryptol::Extras module has been merged with the Prelude, now that it type-checks more quickly. Removing a Cryptol::Extras import should be enough to get older modules to work with this release.

  • Several new type classes now exist: Logic for bitwise logical operations, Zero for the zero primitive, and SignedCmp for signed comparison operations. Some functions with explicit type signatures may now require additional constraints.

  • Numeric literals and enumerations can now be used with any type that is a member of the new Literal class, which includes [n], Integer, and Z n.

  • Type checker and interpreter performance is generally better. Please report regressions as issues on GitHub.

  • The :help command now works with built-in types, commands, and :set options.

  • Defaulting warnings and error messages use more meaningful variable names.

  • Many bugs have been fixed.

Assets 12
Loading