Changelog History
Page 1

v2.13.0 Changes
Language changes
 β‘οΈ Update the implementation of the Prelude function
sortBy
to use a merge sort instead of an insertion sort. This improves the both asymptotic and observed performance on sorting tasks.
π» UI improvements
 "Type mismatch" errors now show a context giving more information
about the location of the error. The context is shown when the
part of the types match, but then some nested types do not.
For example, when mathching
{ a : [8], b : [8] }
with{ a : [8], b : [16] }
the error will be8
does not match16
and the context will be{ b : [ERROR] _ }
indicating that the error is in the length of the sequence of fieldb
.
π Bug fixes
π The What4 backend now properly supports Boolector 3.2.2 or later.
π Make error message locations more precise in some cases (issue #1299).
π Make
:reload
behave as expected after loading a module with:module
(issue #1313).π Make
include
paths work as expected when nested within anotherinclude
(issue #1321).π Fix a panic that occurred when loading dependencies before
include
s are resolved (issue #1330).Closed issues #1098, #1280, and #1347.
π Merged pull requests #1233, #1300, #1301, #1302, #1303, #1305, #1306, #1307,
1308, #1311, #1312, #1317, #1319, #1323, #1326, #1331, #1333, #1336, #1337,
1338, #1342, #1346, #1348, and #1349.
 β‘οΈ Update the implementation of the Prelude function

v2.12.0 Changes
Language changes
β‘οΈ Updates to the layout rule. We simplified the specification and made some minor changes, in particular:
 Paren blocks nested in a layout block need to respect the indentation if the layout block
 We allow nested layout blocks to have the same indentation, which is
convenient when writing
private
declarations as they don't need to be indented as long as they are at the end of the file.
π New enumeration forms
[x .. y by n]
,[x .. <y by n]
,[x .. y down by n]
and[x .. >y down by n]
have been implemented. These new forms let the user explicitly specify the stride for an enumeration, as opposed to the previous[x, y .. z]
form (where the stride was computed fromx
andy
).Nested modules are now available (from pull request #1048). For example, the following is now valid Cryptol:
module SubmodTest where import submodule B as C submodule A where propA = C::y > 5 submodule B where y : Integer y = 42
π New features
What4 prover backends now feature an improved multiSAT procedure which is significantly faster than the old algorithm. Thanks to Levent ErkoΜk for the suggestion.
There is a new
w4abc
solver option, which communicates to ABC as an external process via What4.π Expanded support for declaration forms in the REPL. You can now define infix operators, type synonyms and mutuallyrecursive functions, and state signatures and fixity declarations. Multiple declarations can be combined into a single line by separating them with
;
, which is necessary for stating a signature together with a definition, etc.There is a new
:set path
REPL option that provides an alternative toCRYPTOLPATH
for controlling where to search for imported modules (issue #631).π The
cryptolremoteapi
server now natively supports HTTPS (issue1008),
newtype
values (issue #1033), and safety checking (issue1166).
π Releases optionally include solvers (issue #1111). See the
*withsolvers*
files in the assets list for this release.
π Bug fixes
Closed issues #422, #436, #619, #631, #633, #640, #680, #734, #735,
759, #760, #764, #849, #996, #1000, #1008, #1019, #1032, #1033,
1034, #1043, #1047, #1060, #1064, #1083, #1084, #1087, #1102, #1111,
1113, #1117, #1125, #1133, #1142, #1144, #1145, #1146, #1157, #1160,
1163, #1166, #1169, #1175, #1179, #1182, #1190, #1191, #1196, #1197,
1204, #1209, #1210, #1213, #1216, #1223, #1226, #1238, #1239, #1240,
1241, #1250, #1256, #1259, #1261, #1266, #1274, #1275, #1283, and
1291.
π Merged pull requests #1048, #1128, #1129, #1130, #1131, #1135, #1136,
1137, #1139, #1148, #1149, #1150, #1152, #1154, #1156, #1158, #1159,
1161, #1164, #1165, #1168, #1170, #1171, #1172, #1173, #1174, #1176,
1181, #1183, #1186, #1188, #1192, #1193, #1194, #1195, #1199, #1200,
1202, #1203, #1205, #1207, #1211, #1214, #1215, #1218, #1219, #1221,
1224, #1225, #1227, #1228, #1230, #1231, #1232, #1234, #1242, #1243,
1244, #1245, #1246, #1247, #1248, #1251, #1252, #1254, #1255, #1258,
1263, #1265, #1268, #1269, #1270, #1271, #1272, #1273, #1276, #1281,
1282, #1284, #1285, #1286, #1287, #1288, #1293, #1294, and #1295.

v2.11.0 Changes
Language changes
 The
newtype
construct, which has existed in the interpreter in an incomplete and undocumented form for quite a while, is now fullly supported. The construct is documented in section 1.22 of Programming Cryptol. Note, however, that thecryptolremoteapi
RPC server currently does not include full support for referring tonewtype
names, though it can work with implementations that usenewtype
internally.
π New features
0οΈβ£ By default, the interpreter will now track source locations of expressions being evaluated, and retain call stack information. This information is incorporated into error messages arising from runtime errors. This additional bookkeeping incurs significant runtime overhead, but may be disabled using the
nocallstacks
commandline option.The
:exhaust
command now works for floatingpoint types and the:check
command now uses more representative sampling of floatingpoint input values to test.The
cryptolremoteapi
RPC server now has methods corresponding to the:prove
and:sat
commands in the REPL.The
cryptolevalserver
executable is a new, stateless server providing a subset of the functionality ofcryptolremoteapi
dedicated entirely to invoking Cryptol functions on concrete inputs.
Internal changes
A single running instance of the SMT solver used for type checking (Z3) is now used to check a larger number of type correctness queries. This means that fewer solver instances are invoked, and type checking should generally be faster.
π The Cryptol interpreter now builds against
libBF
version 0.6, which fixes a few bugs in the evaluation of floatingpoint operations.
π Bug fixes
 Closed issues #118, #398, #426, #470, #491, #567, #594, #639, #656, #698, #743, #810, #858, #870, #905, #915, #917, #962, #973, #975, #980, #984, #986, #990, #996, #997, #1002, #1006, #1009, #1012, #1024, #1030, #1035, #1036, #1039, #1040, #1044, #1045, #1049, #1050, #1051, #1052, #1063, #1092, #1093, #1094, and #1100.
 The

v2.10.0 Changes
November 19, 2020Language changes
β Cryptol now supports primality checking at the type level. The typelevel predicate
prime
is true when its parameter passes the MillerRabin probabilistic primality test implemented in the GMP library.The
Z p
type is now aField
whenp
is prime, allowing additional operations onZ p
values.The literals
0
and1
can now be used at typeBit
, as alternatives forFalse
andTrue
, respectively.π New features
π The interpreter now includes a number of primitive functions that allow faster execution of a number of common cryptographic functions, including the core operations of AES and SHA2, operations on GF(2) polynomials (the existing
pmod
,pdiv
, andpmult
functions), and some operations on prime field elliptic curves. These functions are useful for implementing higherlevel algorithms, such as many postquantum schemes, with more acceptable performance than possible when running a toptobottom Cryptol implementation in the interpreter.π For a full list of the new primitives, see the new Cryptol
SuiteB
andPrimeEC
modules.The REPL now allows lines containing only comments, making it easier to copy and paste examples.
π The interpreter has generally improved performance overall.
Several error messages are more comprehensible and less verbose.
π Cryptol releases and nightly builds now include an RPC server alongside the REPL. This provides an alternative interface to the same interpreter and proof engine available from the REPL, but is bettersuited to programmatic use. Details on the protocol used by the server are available here. A Python client for this protocol is available here.
π Windows builds are now distributed as both
.tar.gz
and.msi
files.π Bug Fixes

v2.9.1 Changes
September 01, 2020 
v2.9.0 Changes
July 29, 2020Language changes
β Removed the
Arith
class. Replaced it instead with more specialized numeric classes:Ring
,Integral
,Field
, andRound
.Ring
is the closest analogue to the oldArith
class; it contains thefromInteger
,(+)
,(*)
,()
andnegate
methods.Ring
contains all the base arithmetic types in Cryptol, and lifts pointwise over tuples, sequences and functions, just asArith
did.β‘οΈ The new
Integral
class now contains the integer division and modulus methods ((/)
and(%)
), and the sequence indexing, sequence update and shifting operations are generalized overIntegral
. ThetoInteger
operation is also generalized over this class.Integral
contains the bitvector types andInteger
.The new
Field
class contains types representing mathematical fields (or types that are approximately fields). It is currently inhabited by the newRational
type, and theFloat
family of types. It will eventually also contain theReal
type. It has the operationrecip
for reciprocal and(/.)
for field division (not to be confused for(/)
, which is Euclidean integral division).There is also a new
Round
class for types that can sensibly be rounded to integers. This class has the methodsfloor
,ceiling
,trunc
,roundToEven
androundAway
for performing different kinds of integer rounding.Rational
andFloat
inhabitRound
.The type of
(^^)
is modified to be{a, e} (Ring a, Integral e) => a > e > a
. This makes it clear that the semantics are iterated multiplication, which makes sense in any ring.Finally, the
lg2
,(/$)
and(%$)
methods ofArith
have had their types specialized so they operate only on bitvectors.β Added an
Eq
class, and moved the equality operations fromCmp
intoEq
. TheZ
type becomes a member ofEq
but notCmp
.β Added a base
Rational
type. It is implemented as a pair of integers, quotiented in the usual way. As such, it reduces to the theory of integers and requires no new solver support (beyond nonlinear integer arithmetic).Rational
inhabits the newField
andRound
classes. Rational values can be constructed using theratio
function, or viafromInteger
.The
generate
function (and thusx @ i= e
definitions) has had its type specialized so the index type is alwaysInteger
.The new typeclasses are arranged into a class hierarchy, and the typechecker will use that information to infer superclass instances from subclasses.
β Added a family of base types,
Float e p
, for working with floating point numbers. The parameters control the precision of the numbers, withe
being the number of bits to use in the exponent andp1
being the number of bits to use in the mantissa. TheFloat
family of types may be used through the usual overloaded functionality in Cryptol, and there is a new builtin module calledFloat
, which contains functionality specific to floating point numbers.β Add a way to write fractional literals in base 2,8,10, and 16. Fractional literals are overloaded, and may be used for different types (currently
Rational
and theFloat
family). Fractional literal in base 2,8,and 16 must be precise, and will be rejected statically if they cannot be represented exactly. Fractional literals in base 10 are rounded to the nearest even representable number.π Changes to the defaulting algorithm. The new algorithm only applies to constraints arising from literals (i.e.,
Literal
andFLiteral
constraints). The guiding principle is that we now default these to one of the infinite precision typesInteger
orRational
.Literal
constraints are defaulted toInteger
, unless the corresponding type also hasField
constraint, in which case we useRational
. Fractional literal constraints are always defaulted to `Rational.π New features
Document the behavior of lifted selectors.
β Added support for symbolic simulation via the
What4
library in addition to the previous method based onSBV
. The What4 symbolic simulator is used when selecting solvers with thew4
prefix, such asw4z3
,w4cvc4
,w4yices
, etc. TheSBV
andWhat4
libraries make different tradeoffs in how they represent formulae. You may find one works better than another for the same problem, even with the same solver.More detailed information about the status of various symbols in the output of the
:browse
command (issue #688).The
:safe
command will attempt to prove that a given Cryptol term is safe; in other words, that it will not encounter a runtime error for all inputs. Runtime errors arise from things like divisionbyzero, indexoutofbounds situations and explicit calls toerror
orassert
.βͺ The
:prove
and:sat
commands now incorporate safety predicates by default. In a:sat
call, models will only be found that do not cause runtime errors. For:prove
calls, the safety conditions are added as additional proof goals. The prior behavior (which ignored safety conditions) can be restored using:set ignoresafety = on
.Improvements to the
any
prover. It will now shut down external prover processes correctly when one finds a solution. It will also wait for the first successful result to be returned from a prover, instead of failing as soon as one prover fails.An experimental
parmap
primitive that applies a function to a sequence of arguments and computes the results in parallel. This operation should be considered experimental and may significantly change or disappear in the future, and could possibly uncover unknown race conditions in the interpreter.π Bug fixes

v2.8.0 Changes
September 04, 2019π New features
β Added support for indexing on the lefthand sides of declarations, record field constructors, and record updaters (issue #577). This builds on a new prelude function called
generate
, where the new syntaxx @ i = e
is sugar forx = generate (\i > e)
.β Added support for element type ascriptions on sequence enumerations. The syntax
[a,b..c:t]
indicates that the elements should be of typet
.Added support for wildcards in sequence enumerations. For example, the syntax
[1 .. _] : [3][8]
yields[0x01, 0x02, 0x03]
. It can also be used polymorphically. For example, the most general type of[1 .. _]
is{n, a} (n >= 1, Literal n a, fin n) => [n]a
π Changed the syntax of type signatures to allow multiple constraint arrows in type schemas (issue #599). The following are now equivalent:
f : {a} (fin a, a >= 1) => [a] > [a] f : {a} (fin a) => (a >= 1) => [a] > [a]
β Added a mechanism for userdefined type constraint operators, and use this to define the new type constraint synonyms (<) and (>) (issues #400, #618).
β Added support for primitive type declarations. The prelude now uses this mechanism to declare all of the basic types.
β Added support for Haskellstyle "block arguments", reducing the need for parentheses in some cases. For example,
generate (\i > i +1)
can now be writtengenerate \i > i + 1
.π Improved shadowing errors (part of the fix for issue #569).
π Bug fixes

v2.7.0 Changes
April 30, 2019π New features
β Added syntax for record updates (see #399 for details of implemented and planned features).
β‘οΈ Updated the
:browse
command to list module parameters (issue #586).β Added support for test vector creation (the
:dumptests
command). This feature computes a list of random inputs and outputs for the given expression of function type and saves it to a file. This is useful for generating tests from a trusted Cryptol specification to apply to an implementation written in another language.π₯ Breaking changes
β Removed the
[x..]
construct from the language (issue #574). It was shorthand for[x..2^^n1]
for a bit vector of sizen
, which was often not what the user intended. Users should instead write either[x..y]
or[x...]
, to construct a smaller range or a lazy sequence, respectively.π Renamed the valuelevel
width
function tolength
, and generalized its type (issue #550). It does not behave identically to the typelevelwidth
operator, which led to confusion. The namelength
matches more closely with similar functions in other languages.π Bug fixes
π Improved type checking performance of decimal literals.
π Improved type checking of
/^
and%^
(issues #581, #582).π Improved performance of sequence updates with the
update
primitive (issue #579).π Fixed elapsed time printed by
:prove
and:sat
(issue #572).π Fixed SMTLib formulas generated for right shifts (issue #566).
π Fixed crash when importing nonparameterized modules with the backtick prefix (issue #565).
π Improved performance of symbolic execution for
Z n
(issue #554).π Fixed interpretation of the
satNum
option so finding multiple solutions doesn't run forever (issue #553).π Improved type checking of the
length
function (issue #548).π Improved error message when trying to prove properties in parameterized modules (issue #545).
β Stopped warning about defaulting at the REPL when
warnDefaulting
is set tofalse
(issue #543).π Fixed builds on nonx86 architectures (issue #542).
π Made browsing of interactivelybound identifiers work better (issue #538).
Fixed a bug that allowed changing the semantics of the
_ # _
pattern and the
and~
operators by creating local definitions of functions that they expand to (issue #568).Closed issues #498, #547, #551, #562, and #563.
Solver versions
π Cryptol can interact with a variety of external SMT solvers to support the
:prove
and:sat
commands, and requires Z3 for its type checker. Many versions of these solvers will work correctly, but for Yices and Z3 we recommend the following specific versions. Z3 4.7.1
 Yices 2.6.1
β For Yices, this is the latest version at the time of this writing. For Z3, it is not, and the latest versions (4.8.x) include changes that cause some examples that previously succeeded to time out when type checking.

v2.6.0 Changes
August 01, 2018π 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 publickey 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 commonlyused constraints.
Signed operations now exist for arithmetic (
/$
and%$
), comparison (>$
,<$
,<=$
, and>=$
), and shifting (>>$
).Operations for chaining arithmetic now exist. The
carry
function returnsTrue
if addition of its arguments would result in unsigned overflow, thescarry
function does the same for signed overflow, and thesborrow
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 fixedsize 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
:extractcoq
command will export the currentlydefined 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 thePrelude
, now that it typechecks more quickly. Removing aCryptol::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 thezero
primitive, andSignedCmp
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
, andZ n
.π Type checker and interpreter performance is generally better. Please report regressions as issues on GitHub.
The
:help
command now works with builtin types, commands, and:set
options.β Defaulting warnings and error messages use more meaningful variable names.
π Many bugs have been fixed.

v2.5.0 Changes
July 25, 2017Cryptol 2.5.0
π This release includes a rewritten interpreter which is generally faster and has fewer strictnessrelated edge cases, major enhancements to the performance of the type checker, and a variety of smaller additions and bug fixes.
β Added
π New
update
andupdates
functions provide an efficient, builtin
way to replace elements of a vector.π New
trace
andtraceVal
functions print messages as they are being
evaluated, which can be helpful for debugging.π New shortcutting operators
/\
,\/
and==>
now exist. The older
&&
and
operators are strict, and have higher precedence.π New experimental
:eval
command evaluates an expression using
a reference interpreter, which we created to ultimately serve as the
official definition of the Cryptol semantics. This interpreter is less
π efficient than the normal one, but written in a very direct style meant
to clearly describe the meaning of each language construct. For this
π release, the semantics of the reference interpreter are not considered
final and still subject to change.π New
proverstats
setting in the REPL, when enabled, causes the
π¨:prove
and:sat
commands to print information about the time taken
and prover used to coplete a proof.The
:help
command now shows information about precedence and fixity
of operators.The
cryptol
executable returns a nonzero exit code when proofs
fail.π New prelude function:
iterate
π New example: MISTY1
π Changed
π The main Cryptol interpreter has been rewritten in monadic style,
which allows much greater control over the order of evaluation, and
π generally improves performance.π The typechecker has had a major overhaul, improving performance
dramatically in many cases.π Overall, performance is generally better.
π New command line option
color
makes use of color text output
π§ configurable.π¨ With
:set ascii=on
, the REPL now prints quotation marks around
strings.Cryptol now depends on version 7.0 or greater of the SBV library.
π Fixes
π Fix an off by one error in the implementation of
split
.π Fix a typo in the implementation of the
>>
operator.π Fix the
pdiv
andpmod
primitives in the special case where the
length of the dividend is less than the degree of the divisor polynomial.π Fix an issue where literal sequences of bit values were being
incorrectly reversed.π Various documentation fixes.