Basic Syntax

Declarations

f x = x + y + z

Type Signatures

f,g : {a,b} (fin a) => [a] b

Numeric Constraint Guards

A declaration with a signature can use numeric constraint guards, which are used to change the behavior of a functoin depending on its numeric type parameters. For example:

len : {n} (fin n) => [n]a -> Integer
len xs | n == 0 => 0
       | n >  0 => 1 + len (drop `{1} xs)

Each behavior starts with | and lists some constraints on the numeric parameters to a declaration. When applied, the function will use the first definition that satisfies the provided numeric parameters.

Numeric constraint guards are quite similar to an if expression, except that decisions are based on types rather than values. There is also an important difference to simply using demotion and an actual if statement:

len' : {n} (fin n) => [n]a -> Integer
len' xs = if `n == 0 => 0
           | `n >  0 => 1 + len (drop `{1} xs)

The definition of len' is rejected, because the value based if expression does provide the type based fact n >= 1 which is required by drop `{1} xs, while in len, the type-checker locally-assumes the constraint n > 0 in that constraint-guarded branch and so it can in fact determine that n >= 1.

Requirements:

Numeric constraint guards only support constraints over numeric literals, such as fin, <=, ==, etc. Type constraint aliases can also be used as long as they only constrain numeric literals.
The numeric constraint guards of a declaration should be exhaustive. The type-checker will attempt to prove that the set of constraint guards is exhaustive, but if it can’t then it will issue a non-exhaustive constraint guards warning. This warning is controlled by the environmental option warnNonExhaustiveConstraintGuards.
Each constraint guard is checked independently of the others, and there are no implict assumptions that the previous behaviors do not match— instead the programmer needs to specify all constraints explicitly in the guard.

Layout

Groups of declarations are organized based on indentation. Declarations with the same indentation belong to the same group. Lines of text that are indented more than the beginning of a declaration belong to that declaration, while lines of text that are indented less terminate a group of declarations. Consider, for example, the following Cryptol declarations:

f x = x + y + z
  where
  y = x * x
  z = x + y

g y = y

This group has two declarations, one for f and one for g. All the lines between f and g that are indented more than f belong to f. The same principle applies to the declarations in the where block of f, which defines two more local names, y and z.

Comments

Cryptol supports block comments, which start with /* and end with */, and line comments, which start with // and terminate at the end of the line. Block comments may be nested arbitrarily.

/* This is a block comment */
// This is a line comment
/* This is a /* Nested */ block comment */

Todo

Document /** */

Identifiers

Cryptol identifiers consist of one or more characters. The first character must be either an English letter or underscore (_). The following characters may be an English letter, a decimal digit, underscore (_), or a prime ('). Some identifiers have special meaning in the language, so they may not be used in programmer-defined names (see Keywords and Built-in Operators).

Examples of identifiers

name    name1    name'    longer_name
Name    Name2    Name''   longerName

Keywords and Built-in Operators

The following identifiers have special meanings in Cryptol, and may not be used for programmer defined names:

Keywords

as              extern      include      interface      parameter      property      where
by              hiding      infix        let            pragma         submodule     else
constraint      if          infixl       module         primitive      then
down            import      infixr       newtype        private        type

The following table contains Cryptol’s operators and their associativity with lowest precedence operators first, and highest precedence last.

Operator precedences
Operator	Associativity
`==>`	right
`\/`	right
`/\`	right
`==` `!=` `===` `!==`	not associative
`>` `<` `<=` `>=` `<$` `>$` `<=$` `>=$`	not associative
`\|\|`	right
`^`	left
`&&`	right
`#`	right
`>>` `<<` `>>>` `<<<` `>>$`	left
`+` `-`	left
`*` `/` `%` `/$` `%$`	left
`^^`	right
`@` `@@` `!` `!!`	left
(unary) `-` `~`	right

Built-in Type-level Operators

Cryptol includes a variety of operators that allow computations on the numeric types used to specify the sizes of sequences.

Type-level operators
Operator	Meaning
`+`	Addition
`-`	Subtraction
`*`	Multiplication
`/`	Division
`/^`	Ceiling division (`/` rounded up)
`%`	Modulus
`%^`	Ceiling modulus (compute padding)
`^^`	Exponentiation
`lg2`	Ceiling logarithm (base 2)
`width`	Bit width (equal to `lg2(n+1)`)
`max`	Maximum
`min`	Minimum

Numeric Literals

Numeric literals may be written in binary, octal, decimal, or hexadecimal notation. The base of a literal is determined by its prefix: 0b for binary, 0o for octal, no special prefix for decimal, and 0x for hexadecimal.

Examples of literals

254                 // Decimal literal
0254                // Decimal literal
0b11111110          // Binary literal
0o376               // Octal literal
0xFE                // Hexadecimal literal
0xfe                // Hexadecimal literal

Numeric literals in binary, octal, or hexadecimal notation result in bit sequences of a fixed length (i.e., they have type [n] for some n). The length is determined by the base and the number of digits in the literal. Decimal literals are overloaded, and so the type is inferred from context in which the literal is used. Examples:

Literals and their types

0b1010              // : [4],   1 * number of digits
0o1234              // : [12],  3 * number of digits
0x1234              // : [16],  4 * number of digits

10                  // : {a}. (Literal 10 a) => a
                    // a = Integer or [n] where n >= width 10

Numeric literals may also be written as polynomials by writing a polynomial expression in terms of x between an opening <| and a closing |>. Numeric literals in polynomial notation result in bit sequences of length one more than the degree of the polynomial. Examples:

Polynomial literals

<| x^^6 + x^^4 + x^^2 + x^^1 + 1 |>  // : [7], equal to 0b1010111
<| x^^4 + x^^3 + x |>                // : [5], equal to 0b11010

Cryptol also supports fractional literals using binary (prefix 0b), octal (prefix 0o), decimal (no prefix), and hexadecimal (prefix ox) digits. A fractional literal must contain a . and may optionally have an exponent. The base of the exponent for binary, octal, and hexadecimal literals is 2 and the exponent is marked using the symbol p. Decimal fractional literals use exponent base 10, and the symbol e. Examples:

Fractional literals

10.2
10.2e3            // 10.2 * 10^3
0x30.1            // 3 * 64 + 1/16
0x30.1p4          // (3 * 64 + 1/16) * 2^4

All fractional literals are overloaded and may be used with types that support fractional numbers (e.g., Rational, and the Float family of types).

Some types (e.g. the Float family) cannot represent all fractional literals precisely. Such literals are rejected statically when using binary, octal, or hexadecimal notation. When using decimal notation, the literal is rounded to the closest representable even number.

All numeric literals may also include _, which has no effect on the literal value but may be used to improve readability. Here are some examples:

Using _

0b_0000_0010
0x_FFFF_FFEA